You can subscribe to this list here.
2009 
_{Jan}
(10) 
_{Feb}
(57) 
_{Mar}
(16) 
_{Apr}
(15) 
_{May}
(31) 
_{Jun}
(17) 
_{Jul}
(10) 
_{Aug}
(18) 
_{Sep}
(20) 
_{Oct}
(31) 
_{Nov}
(6) 
_{Dec}
(7) 

2010 
_{Jan}
(21) 
_{Feb}
(40) 
_{Mar}
(35) 
_{Apr}
(14) 
_{May}
(21) 
_{Jun}
(6) 
_{Jul}
(33) 
_{Aug}
(97) 
_{Sep}
(55) 
_{Oct}
(37) 
_{Nov}
(35) 
_{Dec}
(23) 
2011 
_{Jan}
(9) 
_{Feb}
(9) 
_{Mar}
(57) 
_{Apr}
(21) 
_{May}
(4) 
_{Jun}
(6) 
_{Jul}
(12) 
_{Aug}
(13) 
_{Sep}
(18) 
_{Oct}
(9) 
_{Nov}
(11) 
_{Dec}
(3) 
2012 
_{Jan}
(45) 
_{Feb}
(18) 
_{Mar}
(18) 
_{Apr}
(14) 
_{May}
(11) 
_{Jun}
(14) 
_{Jul}
(3) 
_{Aug}
(6) 
_{Sep}
(2) 
_{Oct}
(16) 
_{Nov}
(31) 
_{Dec}
(10) 
2013 
_{Jan}
(29) 
_{Feb}
(7) 
_{Mar}
(21) 
_{Apr}
(52) 
_{May}
(32) 
_{Jun}
(8) 
_{Jul}
(9) 
_{Aug}
(9) 
_{Sep}
(7) 
_{Oct}
(22) 
_{Nov}
(12) 
_{Dec}

2014 
_{Jan}
(36) 
_{Feb}
(11) 
_{Mar}
(11) 
_{Apr}
(18) 
_{May}
(8) 
_{Jun}
(19) 
_{Jul}
(15) 
_{Aug}
(22) 
_{Sep}
(11) 
_{Oct}
(8) 
_{Nov}
(4) 
_{Dec}
(14) 
2015 
_{Jan}
(2) 
_{Feb}
(4) 
_{Mar}
(10) 
_{Apr}
(7) 
_{May}
(11) 
_{Jun}
(17) 
_{Jul}
(1) 
_{Aug}

_{Sep}

_{Oct}

_{Nov}

_{Dec}

S  M  T  W  T  F  S 




1

2

3
(1) 
4

5

6

7

8
(10) 
9

10

11

12

13

14

15
(1) 
16

17
(1) 
18

19

20
(1) 
21

22

23

24
(1) 
25
(2) 
26
(1) 
27

28

29




From: Michael Leuschel <leuschel@cs...>  20120226 06:40:04

Hi Jonathan, On 26 Feb 2012, at 03:39, Jonathan S. Ostroff wrote: > > I am attaching my model of a supermarket (taken from Ken Robinson's book) > but with some revisions. I see now: the issue is that you have three variables being initialized nondeterminisically: > shelf :: ORDER >  > price :: PRODUCT > NAT >  > cash :: NAT Before finding another solution for price, ProB will first enumerate all solutions to cash. So, increasing MAXINT won't help; actually to the contrary as there will be more solutions for cash. If you set MAXINT to 3 and increasing the number of initializations computed to 50 will give you more interesting solutions for price. If you also want interesting solutions to shelf, you need to set the number of initializations even higher. For example, setting the number of initializations to 500 will give you as 500th solution the values below in the screenshots below. A future version of ProB may support a more random enumeration algorithm (the difficulty is doing this efficiently and ensuring completeness for model checking). > The problem is that > in some cases it makes the proofs harder and also nondeterministic You can also create a refinement of your machine just for animation purposes:  in the refinement you can alter the INITIALISATION or give names to the products You could also add a new event: MY_INITIALISATION which gives more concrete values to price, cash and shelf. This should not alter provability of the rest of the machine (you will have to prove the event itself correct, though.) > I have not yet tried exporting to ProB. Presumably I must first install ProB > to do this? No, not for exporting ;) Later to manipulate the .eventb file, yes. You should download the standalone version of ProB from http://www.stups.uniduesseldorf.de/ProB/index.php5/Download Greetings, Michael 
From: Michael Leuschel <leuschel@cs...>  20120225 08:26:51

Hi Jonathan, On 20 Feb 2012, at 05:53, Jonathan S. Ostroff wrote: > I am trying out the latest version of ProB with Rodin, and I forget how to > change initialization from the default to ones of my choice. > > Suppose we have some variable whose type is PRODUCT > NAT (i.e. a bag > really). The default generated by ProB is {PRODUCT1 > 0, PRODUCT2 >0} as > the initial value. I would like to have, say, {PRODUCT1 > 5, PRODUCT2 > >3}. There are several solutions. It would be good if you send me the model so that I can better help you.  One solution is to change the initialization and write x:= {PRODUCT1 > 5, PRODUCT > 3}.  Another solution is to export your model to ProB Classic and then use the command "Animate > Execute Operation …". Here you can provide additional predicates/values for the various applicable operations/events. (I have just added a tutorial page for exporting to ProB Classic here http://www.stups.uniduesseldorf.de/ProB/index.php5/Tutorial_Rodin_Exporting).  Finally, ProB should enumerate possible solutions for the initialization. The number of initializations computed can be controlled by a preference. You need to set the value high enough to see your desired option appear. However, this may be impractical due to the high number of possible initializations and due to the way ProB currently enumerates these solutions. The tutorial page is maybe of help to you: http://www.stups.uniduesseldorf.de/ProB/index.php5/Tutorial_Setup_Phases. > > A right click on the initial event does provides a show dialog option, but I > cannot see how to change the value of the NAT. You cannot change the value of NAT. However, in case ProB has to find solutions for variables/constants of type NAT and in case the value cannot be inferred by other means, ProB will (usually) enumerate between 0 and MAXINT. You can set the value of MAXINT in the ProB preferences dialog. > Also, can I change PRODUCT1 > To something simpler like p1? You can do so by changing PRODUCT into an enumerated set in the context. You can then give the elements of PRODUCT whatever names you want. > > Is there more documentation for ProB under Rodin? There is a bit of information here: http://www.stups.uniduesseldorf.de/ProB/index.php5/Tutorial In particular:  http://www.stups.uniduesseldorf.de/ProB/index.php5/Tutorial_Rodin_First_Step  http://www.stups.uniduesseldorf.de/ProB/index.php5/Tutorial_Rodin_Parameters However, I just realized that for some reason the pictures have disappeared from the Wiki. We will investigate. Greetings, Michael 
From: Michael Leuschel <leuschel@cs...>  20120225 08:26:43

On 25 Feb 2012, at 08:36, Michael Leuschel wrote: > It would be good if you send me the model so that I can better help you. > >  One solution is to change the initialization and write x:= {PRODUCT1 > 5, PRODUCT > 3}. >  Another solution is to export your model to ProB Classic and then use the command "Animate > Execute Operation …". I just realized (just after sending the previous email) that the above will require that you first change PRODUCT into an enumerated set: this way you can talk about individual elements. Otherwise you will need to produce more convoluted initialization statements ( x: ( x: PRODUCT >> {3,5}) or x :: PRODUCT >> {3,5} for example) or predicates. If you send me the model, I can send you a solution. Greetings, Michael 
From: Matthias Schmalz <Matthias.S<chmalz@in...>  20120224 13:02:47

This mail concerns the Isabelle tutorial of the Rodin workshop on Monday. Unfortunately, I do not have the email addresses of all attendees. Please forward it to people who might attend the tutorial. Sorry for the inconvenience if you don't attend. Dear all, on Monday, I plan to give two tutorials on my Isabelle plugin: a "handson" tutorial and a "listen and watch" tutorial. In the handson tutorial, you will use my toolchain to improve the automated theorem proving capabilities of Rodin. For this tutorial, some familiarity with Isabelle would be useful; you don't have to be a hardcore professional, but you should not use Isabelle for the first time. If you plan to attend the handson tutorial, it is important that you install the required software beforehand. The installation is not difficult, but it takes some time and you have to download hundreds of megabytes. Instructions below. Sorry for the late notice. In the "listen and watch" tutorial, I will develop some of these theorem prover improvements by myself and you will listen and watch. I will proceed slowly and explain every step. You can also point out your favorite weakness of Rodin's automated theorem provers and I will try to fix it in an online fashion. (I may however fail to do so :)) I am looking forward to see you on Monday! Matthias P.s.: Installation instructions for the handson tutorial:  Download and unzip Rodin 2.4, start it at least once. http://sourceforge.net/projects/rodinbsharp/ Make sure to satisfy the requirements mentioned in the release notes: http://wiki.eventb.org/index.php/Rodin_Platform_2.4_Release_Notes#Requirements__Compatibility  Use Rodin's installation facility to install my plugin. Detailed instructions on: http://wiki.eventb.org/index.php/Export_to_Isabelle Note that we will use version 0.6.x during the tutorial, which I will release tomorrow. Nevertheless, it pays off to install 0.5.0, because an update to 0.6.x from 0.5.0 is much faster than a fresh installation.  Download and unpack isabelle20111: http://isabelle.in.tum.de/download.html *Make sure that you have all the softare that is listed in the requirements section of your system.*  Once, version 0.6.x of Isabelle for Rodin has been released, you may want to install it according to the instructions (to be announced). But we can also do that during the tutorial. 
From: Jonathan S. Ostroff <jonathan@yo...>  20120220 04:54:07

I am trying out the latest version of ProB with Rodin, and I forget how to change initialization from the default to ones of my choice. Suppose we have some variable whose type is PRODUCT > NAT (i.e. a bag really). The default generated by ProB is {PRODUCT1 > 0, PRODUCT2 >0} as the initial value. I would like to have, say, {PRODUCT1 > 5, PRODUCT2 >3}. A right click on the initial event does provides a show dialog option, but I cannot see how to change the value of the NAT. Also, can I change PRODUCT1 To something simpler like p1? Is there more documentation for ProB under Rodin? Thank you in advance, Jonathan 
From: Yoann Guyot <yoann.guyot@sy...>  20120217 15:22:29

Dear Rodin Users, I am delighted to announce the release of the SMT Solvers Plugin for Rodin v2.4. It can be installed from the main Rodin update site : http://rodinbsharp.sourceforge.net/updates. You will find all needed instructions on its dedicated page of the EventB wiki : http://wiki.eventb.org/index.php/SMT_Plugin. Best regards,   Yoann GUYOT Tél. : (+33)(0)1 76 60 40 28 Ingénieur Modélisation et Preuves SYSTEREL  Standard / Fax : (+33)(0)4 42 90 41 20 / 29 site : http://www.systerel.fr  
From: Michael Jastram <michael@ja...>  20120215 09:22:01

Dear all, Would you buy a print copy of the Rodin Handbook? Please tell us via [1]. You may be aware that the Rodin Handbook project [2] is soon coming to an end. Currently, is is only available digitally. If there is enough interest, we could also make the handbook available via a printondemand service (probably Amazon). But we would only do this if there is enough demand. We are kindly asking you to answer a short questionnaire (1 mandatory and 3 optional questions) to help us estimate demand [1]. Thank you for taking your time! Best wishes,  The Rodin Handbook Team [1] http://kwiksurveys.com?s=LJDEOJ_58d45059 [2] http://handbook.eventb.org/  Michael Jastram (http://www.jastram.de, +49 (162) 274 83 94) Geschäftsführer, Formal Mind GmbH (http://formalmind.com) Wissenschaftler, Heinrich Heine Universität Düsseldorf (http://www.stups.uniduesseldorf.de) 1. Vorsitzender, rheinjug e.V. (http://www.rheinjug.de) 
From: <kimmo.varpaaniemi@ko...>  20120208 14:25:15

Hello, I've got used to handle cardinalities in interactive proofs but still thought that almost any "simple" property could be made autoprovable by means of some sequence of autoprovable theorems. To my disappointment, in the considered case I only managed to create the context that is displayed below in Camille format. All theorems except thm16 get discharged automatically. Manual discharging of thm16 is easy though requires backtracking in order to cancel an "unrequested rewriting" of a cardinality of a union. With best regards, Kimmo Varpaaniemi context C constants xs x sets X axioms @axm1 finite(X) @axm2 xs ⊆ X theorem @thm1 finite(X ∖ X) theorem @thm2 card(X ∖ X) = 0 theorem @thm3 (x ∈ xs) ⇒ (finite({x})) theorem @thm4 (x ∈ xs) ⇒ (card({x}) = 1) theorem @thm5 (x ∈ xs) ⇒ (finite(xs)) theorem @thm6 (x ∈ xs) ⇒ (finite(xs ∖ {x})) theorem @thm7 (x ∈ xs) ⇒ (finite((xs ∖ {x}) ∪ {x})) theorem @thm8 (x ∈ xs) ⇒ (finite((xs ∖ {x}) ∩ {x})) theorem @thm9 (x ∈ xs) ⇒ ((xs ∖ {x}) ∩ {x} = X ∖ X) theorem @thm10 (x ∈ xs) ⇒ (card((xs ∖ {x}) ∩ {x}) = card(X ∖ X)) theorem @thm11 (x ∈ xs) ⇒ (card((xs ∖ {x}) ∩ {x}) = 0) theorem @thm12 (x ∈ xs) ⇒ (card((xs ∖ {x}) ∪ {x}) = card(xs ∖ {x}) + card({x}) − card((xs ∖ {x}) ∩ {x})) theorem @thm13 (x ∈ xs) ⇒ (card((xs ∖ {x}) ∪ {x}) = card(xs ∖ {x}) + 1) theorem @thm14 (x ∈ xs) ⇒ (card(xs ∖ {x}) = card((xs ∖ {x}) ∪ {x}) − 1) theorem @thm15 (x ∈ xs) ⇒ ((xs ∖ {x}) ∪ {x} = xs) theorem @thm16 (x ∈ xs) ⇒ (card((xs ∖ {x}) ∪ {x}) = card(xs)) theorem @thm17 (x ∈ xs) ⇒ (card(xs ∖ {x}) = card(xs) − 1) end Ken Robinson [kenr@...] kirjoitti: > Dear Son, Pierre, Matthias and Rodin Users, > > Thank you Son and Pierre and Matthias for your solutions. (Son's corrected by Matthias) > > I want to try to make it clear here what I am driving at. > > I have previously discharged the PO that I mentioned in my initial email, however the proof was not contained in the project I was reviewing and "cleaning up". > > I spent a bit of time on producing a proof and then decided that the experience was painful and undesirable. Either than or I was an idiot. > > Both Son/Matthias and Pierre's solutions and also their experience does not incline me to change my mind. Don't get me wrong: they are nice proofs, but it is important to keep an eye on "what is being proved". > > I don't use "axiom" lightly and I am not suggesting a particular axiom or a set of axioms. > > What I am saying is that when you are trying to convince people that EventB is an important tool for modelling designs, they are far from impressed to find and remember that they will probably find this very early in their use of Rodin that > > x : xs => card(xs \ {x}) = card(xs)  1 > > is not auto proved, or at least easily proved to be a big put off. > > There is something "axiomatic" about that assertion. > > If that isn't easily proved then what about the other POs coming from the more complex requirements that they want to model? > > Luckily, many of the "more complex" POs are discharged more easily than the above! > > Unless they involve "card"! :) > > I sent off the earlier email to see what sort of reaction I would get. > > I've just seen Matthias's later email on using Isabelle. > > That probably is comforting. > > Further note: one of the things that makes life difficult at the moment is that it is not always clear why something can's be discharged. > > OK, silly statement: that is always true about proof, but it is a special case when the lemma is "obviously true". > > My whole concern here is with "credibility". > > Thanks, > > Ken > > On 08/02/2012, at 22:33 PM, Hoang, Thai Son wrote: > > > Dear Ken, > > I just realised that I did not push my last reply to the mailing list. > > I just did some experiment with cardinality. I can prove the your theorem with the following axiom which I think should be some definition for cardinality. > > !n,s.s <: X => card(s) = n <=> (#f.f : 1..n >>> s) > > I've been down this road before with cardinality. > > Cheers, > > Son > > > > On 8 Feb 2012, at 12:00, Thai Son Hoang wrote: > > > >> Hi Ken, > >> On 8 Feb 2012, at 11:13, Ken Robinson wrote: > >> > >>> Hello everyone, > >>> > >>> I fear this email will demonstrate that I am an idiot, but here goes. > >>> > >> > >> You are certainly not. > >> > >>> My problems with card are long standing and persistent. > >>> > >> > >> It is the same feeling for me. > >> > >>> As usual I am cleaning up on POs that are undischarged under the new Rodin, 2.4. > >>> > >> > >> I assume that you they are undischarged with the old Rodin as well. > >> > >>> As usual I am having trouble with card. > >>> > >>> For example: > >>> > >>> SETS > >>> X > >>> finite X > >>> > >>> xs <: X > >>> > >>> Prove > >>> x : xs => card(xs \ {x}) = card(xs)  1 > >>> > >>> So far this has resisted all my efforts to discharge it. > >>> > >>> and I've been this way before. > >>> > >>> I hope, and will be grateful, if someone can demonstrate a proof. > >>> > >>> And I'm hoping it will show that I am an idiot. > >>> > >>> If not then I think this is a worry, as to many this poses a serious credibility problem for EventB. > >>> > >>> Without knowing the EventB axioms, this would appear to be axiomatic to most people. > >>> > >>> I will be grateful for any resolution of my ineptitude. > >>> > >> > >> You are probably want to the following feature request which has not been implemented. > >> http://sourceforge.net/tracker/index.php?func=detail&aid=3191061&group_id=108850&atid=651672 > >> But I think the main problem is a missing "definition" for cardinality, something along the line of the following request. > >> http://sourceforge.net/tracker/index.php?func=detail&aid=2922308&group_id=108850&atid=651672 > >> Cheers, > >> Son > > > >  > > Thai Son Hoang > > CNB F105.2 > > ETH Zentrum, Zurich, Switzerland > > Tel: +41 44 632 85 94 > > Fax: +41 44 632 11 72 > > <CardinalityRodin2.4.0.zip> > > Keep Your Developer Skills Current with LearnDevNow! > > The most comprehensive online learning library for Microsoft developers > > is just $99.99! Visual Studio, SharePoint, SQL  plus HTML5, CSS3, MVC3, > > Metro Style Apps, more. Free future releases when you subscribe now! > > http://p.sf.net/sfu/learndevnowd2d_______________________________________________ > > Rodinbsharpuser mailing list > > Rodinbsharpuser@... > > https://lists.sourceforge.net/lists/listinfo/rodinbsharpuser > > >  > Keep Your Developer Skills Current with LearnDevNow! > The most comprehensive online learning library for Microsoft developers > is just $99.99! Visual Studio, SharePoint, SQL  plus HTML5, CSS3, MVC3, > Metro Style Apps, more. Free future releases when you subscribe now! > http://p.sf.net/sfu/learndevnowd2d > _______________________________________________ > Rodinbsharpuser mailing list > Rodinbsharpuser@... > https://lists.sourceforge.net/lists/listinfo/rodinbsharpuser > 
From: Pierre Casteran <pierre.casteran@la...>  20120208 14:00:07

Dear all, If the problem is to convince people of trusting a development made with Rodin, what you need is a possibility of showing explicitely which axioms were used in the proofs, just with a tool which can enumerate all nonproved statement in the proofs. It would be also very useful to have some way for the users to contribute some depository with theorems they think to be useful to other people (for instance a lot of theorems like Ken's, on cardinality). In combination with search tools (like "find all theorems that contain card and setdifference"), it would easier to finalize proofs. I use mainly the Coq proof assistant, but I think that Isabelle contains these tools too. About automation: tools like why3 are only proof obligation genaerators, which can send to a lot of automatic or interactive theorem provers. I would be very interested by such a tool for [Event]B that would be a generator of POs according to the mathematical model of contexts and machines, but letting other tools doing the proofs or helping the user in difficult steps. Please notice that I am not a big user of Rodin, and that my wish list contains perhaps some already existing items. In this case, I'm sorry for the noise. Best, Pierre Le 08/02/2012 14:16, Ken Robinson a écrit : > Dear Son, Pierre, Matthias and Rodin Users, > > Thank you Son and Pierre and Matthias for your solutions. (Son's corrected by Matthias) > > I want to try to make it clear here what I am driving at. > > I have previously discharged the PO that I mentioned in my initial email, however the proof was not contained in the project I was reviewing and "cleaning up". > > I spent a bit of time on producing a proof and then decided that the experience was painful and undesirable. Either than or I was an idiot. > > Both Son/Matthias and Pierre's solutions and also their experience does not incline me to change my mind. Don't get me wrong: they are nice proofs, but it is important to keep an eye on "what is being proved". > > I don't use "axiom" lightly and I am not suggesting a particular axiom or a set of axioms. > > What I am saying is that when you are trying to convince people that EventB is an important tool for modelling designs, they are far from impressed to find and remember that they will probably find this very early in their use of Rodin that > > x : xs => card(xs \ {x}) = card(xs)  1 > > is not auto proved, or at least easily proved to be a big put off. > > There is something "axiomatic" about that assertion. > > If that isn't easily proved then what about the other POs coming from the more complex requirements that they want to model? > > Luckily, many of the "more complex" POs are discharged more easily than the above! > > Unless they involve "card"! :) > > I sent off the earlier email to see what sort of reaction I would get. > > I've just seen Matthias's later email on using Isabelle. > > That probably is comforting. > > Further note: one of the things that makes life difficult at the moment is that it is not always clear why something can's be discharged. > > OK, silly statement: that is always true about proof, but it is a special case when the lemma is "obviously true". > > My whole concern here is with "credibility". > > Thanks, > > Ken > > On 08/02/2012, at 22:33 PM, Hoang, Thai Son wrote: > >> Dear Ken, >> I just realised that I did not push my last reply to the mailing list. >> I just did some experiment with cardinality. I can prove the your theorem with the following axiom which I think should be some definition for cardinality. >> !n,s.s<: X => card(s) = n<=> (#f.f : 1..n>>> s) >> I've been down this road before with cardinality. >> Cheers, >> Son >> >> On 8 Feb 2012, at 12:00, Thai Son Hoang wrote: >> >>> Hi Ken, >>> On 8 Feb 2012, at 11:13, Ken Robinson wrote: >>> >>>> Hello everyone, >>>> >>>> I fear this email will demonstrate that I am an idiot, but here goes. >>>> >>> >>> You are certainly not. >>> >>>> My problems with card are long standing and persistent. >>>> >>> >>> It is the same feeling for me. >>> >>>> As usual I am cleaning up on POs that are undischarged under the new Rodin, 2.4. >>>> >>> >>> I assume that you they are undischarged with the old Rodin as well. >>> >>>> As usual I am having trouble with card. >>>> >>>> For example: >>>> >>>> SETS >>>> X >>>> finite X >>>> >>>> xs<: X >>>> >>>> Prove >>>> x : xs => card(xs \ {x}) = card(xs)  1 >>>> >>>> So far this has resisted all my efforts to discharge it. >>>> >>>> and I've been this way before. >>>> >>>> I hope, and will be grateful, if someone can demonstrate a proof. >>>> >>>> And I'm hoping it will show that I am an idiot. >>>> >>>> If not then I think this is a worry, as to many this poses a serious credibility problem for EventB. >>>> >>>> Without knowing the EventB axioms, this would appear to be axiomatic to most people. >>>> >>>> I will be grateful for any resolution of my ineptitude. >>>> >>> >>> You are probably want to the following feature request which has not been implemented. >>> http://sourceforge.net/tracker/index.php?func=detail&aid=3191061&group_id=108850&atid=651672 >>> But I think the main problem is a missing "definition" for cardinality, something along the line of the following request. >>> http://sourceforge.net/tracker/index.php?func=detail&aid=2922308&group_id=108850&atid=651672 >>> Cheers, >>> Son >> >>  >> Thai Son Hoang >> CNB F105.2 >> ETH Zentrum, Zurich, Switzerland >> Tel: +41 44 632 85 94 >> Fax: +41 44 632 11 72 >> <CardinalityRodin2.4.0.zip> >> Keep Your Developer Skills Current with LearnDevNow! >> The most comprehensive online learning library for Microsoft developers >> is just $99.99! Visual Studio, SharePoint, SQL  plus HTML5, CSS3, MVC3, >> Metro Style Apps, more. Free future releases when you subscribe now! >> http://p.sf.net/sfu/learndevnowd2d_______________________________________________ >> Rodinbsharpuser mailing list >> Rodinbsharpuser@... >> https://lists.sourceforge.net/lists/listinfo/rodinbsharpuser > 
From: Ken Robinson <kenr@cs...>  20120208 13:14:01

Dear Son, Pierre, Matthias and Rodin Users, Thank you Son and Pierre and Matthias for your solutions. (Son's corrected by Matthias) I want to try to make it clear here what I am driving at. I have previously discharged the PO that I mentioned in my initial email, however the proof was not contained in the project I was reviewing and "cleaning up". I spent a bit of time on producing a proof and then decided that the experience was painful and undesirable. Either than or I was an idiot. Both Son/Matthias and Pierre's solutions and also their experience does not incline me to change my mind. Don't get me wrong: they are nice proofs, but it is important to keep an eye on "what is being proved". I don't use "axiom" lightly and I am not suggesting a particular axiom or a set of axioms. What I am saying is that when you are trying to convince people that EventB is an important tool for modelling designs, they are far from impressed to find and remember that they will probably find this very early in their use of Rodin that x : xs => card(xs \ {x}) = card(xs)  1 is not auto proved, or at least easily proved to be a big put off. There is something "axiomatic" about that assertion. If that isn't easily proved then what about the other POs coming from the more complex requirements that they want to model? Luckily, many of the "more complex" POs are discharged more easily than the above! Unless they involve "card"! :) I sent off the earlier email to see what sort of reaction I would get. I've just seen Matthias's later email on using Isabelle. That probably is comforting. Further note: one of the things that makes life difficult at the moment is that it is not always clear why something can's be discharged. OK, silly statement: that is always true about proof, but it is a special case when the lemma is "obviously true". My whole concern here is with "credibility". Thanks, Ken On 08/02/2012, at 22:33 PM, Hoang, Thai Son wrote: > Dear Ken, > I just realised that I did not push my last reply to the mailing list. > I just did some experiment with cardinality. I can prove the your theorem with the following axiom which I think should be some definition for cardinality. > !n,s.s <: X => card(s) = n <=> (#f.f : 1..n >>> s) > I've been down this road before with cardinality. > Cheers, > Son > > On 8 Feb 2012, at 12:00, Thai Son Hoang wrote: > >> Hi Ken, >> On 8 Feb 2012, at 11:13, Ken Robinson wrote: >> >>> Hello everyone, >>> >>> I fear this email will demonstrate that I am an idiot, but here goes. >>> >> >> You are certainly not. >> >>> My problems with card are long standing and persistent. >>> >> >> It is the same feeling for me. >> >>> As usual I am cleaning up on POs that are undischarged under the new Rodin, 2.4. >>> >> >> I assume that you they are undischarged with the old Rodin as well. >> >>> As usual I am having trouble with card. >>> >>> For example: >>> >>> SETS >>> X >>> finite X >>> >>> xs <: X >>> >>> Prove >>> x : xs => card(xs \ {x}) = card(xs)  1 >>> >>> So far this has resisted all my efforts to discharge it. >>> >>> and I've been this way before. >>> >>> I hope, and will be grateful, if someone can demonstrate a proof. >>> >>> And I'm hoping it will show that I am an idiot. >>> >>> If not then I think this is a worry, as to many this poses a serious credibility problem for EventB. >>> >>> Without knowing the EventB axioms, this would appear to be axiomatic to most people. >>> >>> I will be grateful for any resolution of my ineptitude. >>> >> >> You are probably want to the following feature request which has not been implemented. >> http://sourceforge.net/tracker/index.php?func=detail&aid=3191061&group_id=108850&atid=651672 >> But I think the main problem is a missing "definition" for cardinality, something along the line of the following request. >> http://sourceforge.net/tracker/index.php?func=detail&aid=2922308&group_id=108850&atid=651672 >> Cheers, >> Son > >  > Thai Son Hoang > CNB F105.2 > ETH Zentrum, Zurich, Switzerland > Tel: +41 44 632 85 94 > Fax: +41 44 632 11 72 > <CardinalityRodin2.4.0.zip> > Keep Your Developer Skills Current with LearnDevNow! > The most comprehensive online learning library for Microsoft developers > is just $99.99! Visual Studio, SharePoint, SQL  plus HTML5, CSS3, MVC3, > Metro Style Apps, more. Free future releases when you subscribe now! > http://p.sf.net/sfu/learndevnowd2d_______________________________________________ > Rodinbsharpuser mailing list > Rodinbsharpuser@... > https://lists.sourceforge.net/lists/listinfo/rodinbsharpuser 
From: Hoang, Thai Son <htson@in...>  20120208 13:00:40

Hi Pierre, You are right. It is very nice proof. The reason why I think of the axiom is that in some other example, I also need that. Cheers, Son On 8 Feb 2012, at 12:39, Pierre Casteran wrote: > Hi, Son, > > Did you need to assert a new axiom ? > In the following project, I proved Kens thm withous axioms, but a lot of effort (in changeme context) >  Thai Son Hoang CNB F105.2 ETH Zentrum, Zurich, Switzerland Tel: +41 44 632 85 94 Fax: +41 44 632 11 72 
From: Matthias Schmalz <Matthias.S<chmalz@in...>  20120208 12:49:34

Hi again, I just want to add that my Isabelle/HOL backend discharges Ken's theorem automatically. I regret that the plugin is not yet ready for a broader audience. I hope to release something by the end of the month. Matthias Am 08.02.2012 13:32, schrieb Matthias Schmalz: > Hi, > > just to keep that clear, the formula > > !n,s. s<: X => card(s) = n<=> (#f.f : 1..n>>> s) > > is not valid. Choose s as the empty set and n as 1. > Instead, it should be > > !n, s. s<: X& n : NAT => card(s) = n<=> (#f. f : 1..n>>> s). > > Ken, you are not an idiot. Reasoning about card is difficult, also in > other theorem provers. > > Best, > Matthias > > > Am 08.02.2012 12:33, schrieb Hoang, Thai Son: >> Dear Ken, >> I just realised that I did not push my last reply to the mailing list. >> I just did some experiment with cardinality. I can prove the your theorem with the following axiom which I think should be some definition for cardinality. >> !n,s.s<: X => card(s) = n<=> (#f.f : 1..n>>> s) >> I've been down this road before with cardinality. >> Cheers, >> Son >> >> On 8 Feb 2012, at 12:00, Thai Son Hoang wrote: >> >>> Hi Ken, >>> On 8 Feb 2012, at 11:13, Ken Robinson wrote: >>> >>>> Hello everyone, >>>> >>>> I fear this email will demonstrate that I am an idiot, but here goes. >>>> >>> >>> You are certainly not. >>> >>>> My problems with card are long standing and persistent. >>>> >>> >>> It is the same feeling for me. >>> >>>> As usual I am cleaning up on POs that are undischarged under the new Rodin, 2.4. >>>> >>> >>> I assume that you they are undischarged with the old Rodin as well. >>> >>>> As usual I am having trouble with card. >>>> >>>> For example: >>>> >>>> SETS >>>> X >>>> finite X >>>> >>>> xs<: X >>>> >>>> Prove >>>> x : xs => card(xs \ {x}) = card(xs)  1 >>>> >>>> So far this has resisted all my efforts to discharge it. >>>> >>>> and I've been this way before. >>>> >>>> I hope, and will be grateful, if someone can demonstrate a proof. >>>> >>>> And I'm hoping it will show that I am an idiot. >>>> >>>> If not then I think this is a worry, as to many this poses a serious credibility problem for EventB. >>>> >>>> Without knowing the EventB axioms, this would appear to be axiomatic to most people. >>>> >>>> I will be grateful for any resolution of my ineptitude. >>>> >>> >>> You are probably want to the following feature request which has not been implemented. >>> http://sourceforge.net/tracker/index.php?func=detail&aid=3191061&group_id=108850&atid=651672 >>> But I think the main problem is a missing "definition" for cardinality, something along the line of the following request. >>> http://sourceforge.net/tracker/index.php?func=detail&aid=2922308&group_id=108850&atid=651672 >>> Cheers, >>> Son >> >>  >> Thai Son Hoang >> CNB F105.2 >> ETH Zentrum, Zurich, Switzerland >> Tel: +41 44 632 85 94 >> Fax: +41 44 632 11 72 >> >> >> >>  >> Keep Your Developer Skills Current with LearnDevNow! >> The most comprehensive online learning library for Microsoft developers >> is just $99.99! Visual Studio, SharePoint, SQL  plus HTML5, CSS3, MVC3, >> Metro Style Apps, more. Free future releases when you subscribe now! >> http://p.sf.net/sfu/learndevnowd2d >> >> >> >> _______________________________________________ >> Rodinbsharpuser mailing list >> Rodinbsharpuser@... >> https://lists.sourceforge.net/lists/listinfo/rodinbsharpuser > >  > Keep Your Developer Skills Current with LearnDevNow! > The most comprehensive online learning library for Microsoft developers > is just $99.99! Visual Studio, SharePoint, SQL  plus HTML5, CSS3, MVC3, > Metro Style Apps, more. Free future releases when you subscribe now! > http://p.sf.net/sfu/learndevnowd2d > _______________________________________________ > Rodinbsharpuser mailing list > Rodinbsharpuser@... > https://lists.sourceforge.net/lists/listinfo/rodinbsharpuser 
From: Matthias Schmalz <Matthias.S<chmalz@in...>  20120208 12:32:22

Hi, just to keep that clear, the formula !n,s. s<: X => card(s) = n <=> (#f.f : 1..n>>> s) is not valid. Choose s as the empty set and n as 1. Instead, it should be !n, s. s <: X & n : NAT => card(s) = n <=> (#f. f : 1..n >>> s). Ken, you are not an idiot. Reasoning about card is difficult, also in other theorem provers. Best, Matthias Am 08.02.2012 12:33, schrieb Hoang, Thai Son: > Dear Ken, > I just realised that I did not push my last reply to the mailing list. > I just did some experiment with cardinality. I can prove the your theorem with the following axiom which I think should be some definition for cardinality. > !n,s.s<: X => card(s) = n<=> (#f.f : 1..n>>> s) > I've been down this road before with cardinality. > Cheers, > Son > > On 8 Feb 2012, at 12:00, Thai Son Hoang wrote: > >> Hi Ken, >> On 8 Feb 2012, at 11:13, Ken Robinson wrote: >> >>> Hello everyone, >>> >>> I fear this email will demonstrate that I am an idiot, but here goes. >>> >> >> You are certainly not. >> >>> My problems with card are long standing and persistent. >>> >> >> It is the same feeling for me. >> >>> As usual I am cleaning up on POs that are undischarged under the new Rodin, 2.4. >>> >> >> I assume that you they are undischarged with the old Rodin as well. >> >>> As usual I am having trouble with card. >>> >>> For example: >>> >>> SETS >>> X >>> finite X >>> >>> xs<: X >>> >>> Prove >>> x : xs => card(xs \ {x}) = card(xs)  1 >>> >>> So far this has resisted all my efforts to discharge it. >>> >>> and I've been this way before. >>> >>> I hope, and will be grateful, if someone can demonstrate a proof. >>> >>> And I'm hoping it will show that I am an idiot. >>> >>> If not then I think this is a worry, as to many this poses a serious credibility problem for EventB. >>> >>> Without knowing the EventB axioms, this would appear to be axiomatic to most people. >>> >>> I will be grateful for any resolution of my ineptitude. >>> >> >> You are probably want to the following feature request which has not been implemented. >> http://sourceforge.net/tracker/index.php?func=detail&aid=3191061&group_id=108850&atid=651672 >> But I think the main problem is a missing "definition" for cardinality, something along the line of the following request. >> http://sourceforge.net/tracker/index.php?func=detail&aid=2922308&group_id=108850&atid=651672 >> Cheers, >> Son > >  > Thai Son Hoang > CNB F105.2 > ETH Zentrum, Zurich, Switzerland > Tel: +41 44 632 85 94 > Fax: +41 44 632 11 72 > > > >  > Keep Your Developer Skills Current with LearnDevNow! > The most comprehensive online learning library for Microsoft developers > is just $99.99! Visual Studio, SharePoint, SQL  plus HTML5, CSS3, MVC3, > Metro Style Apps, more. Free future releases when you subscribe now! > http://p.sf.net/sfu/learndevnowd2d > > > > _______________________________________________ > Rodinbsharpuser mailing list > Rodinbsharpuser@... > https://lists.sourceforge.net/lists/listinfo/rodinbsharpuser 
From: nai11 <alexei.iliasov@ne...>  20120208 12:21:21

Hi all, this is an old and embarrsing problem. Almost nothing about cardinalities is provable without helper axiom. Among the list of inference rules on the wiki there are rules that would discharge these and similar condition but they are not present in the tool. ________________________________________ From: Hoang, Thai Son [htson@...] Sent: 08 February 2012 11:33 To: User Rodin Bsharp User Subject: Re: [Rodinbsharpuser] Ongoing problems with card Dear Ken, I just realised that I did not push my last reply to the mailing list. I just did some experiment with cardinality. I can prove the your theorem with the following axiom which I think should be some definition for cardinality. !n,s.s <: X => card(s) = n <=> (#f.f : 1..n >>> s) I've been down this road before with cardinality. Cheers, Son On 8 Feb 2012, at 12:00, Thai Son Hoang wrote: > Hi Ken, > On 8 Feb 2012, at 11:13, Ken Robinson wrote: > >> Hello everyone, >> >> I fear this email will demonstrate that I am an idiot, but here goes. >> > > You are certainly not. > >> My problems with card are long standing and persistent. >> > > It is the same feeling for me. > >> As usual I am cleaning up on POs that are undischarged under the new Rodin, 2.4. >> > > I assume that you they are undischarged with the old Rodin as well. > >> As usual I am having trouble with card. >> >> For example: >> >> SETS >> X >> finite X >> >> xs <: X >> >> Prove >> x : xs => card(xs \ {x}) = card(xs)  1 >> >> So far this has resisted all my efforts to discharge it. >> >> and I've been this way before. >> >> I hope, and will be grateful, if someone can demonstrate a proof. >> >> And I'm hoping it will show that I am an idiot. >> >> If not then I think this is a worry, as to many this poses a serious credibility problem for EventB. >> >> Without knowing the EventB axioms, this would appear to be axiomatic to most people. >> >> I will be grateful for any resolution of my ineptitude. >> > > You are probably want to the following feature request which has not been implemented. > http://sourceforge.net/tracker/index.php?func=detail&aid=3191061&group_id=108850&atid=651672 > But I think the main problem is a missing "definition" for cardinality, something along the line of the following request. > http://sourceforge.net/tracker/index.php?func=detail&aid=2922308&group_id=108850&atid=651672 > Cheers, > Son  Thai Son Hoang CNB F105.2 ETH Zentrum, Zurich, Switzerland Tel: +41 44 632 85 94 Fax: +41 44 632 11 72 
From: Pierre Casteran <pierre.casteran@la...>  20120208 11:40:02

Hi, Son, Did you need to assert a new axiom ? In the following project, I proved Kens thm withous axioms, but a lot of effort (in changeme context) Pierre Le 08/02/2012 12:33, Hoang, Thai Son a écrit : > Dear Ken, > I just realised that I did not push my last reply to the mailing list. > I just did some experiment with cardinality. I can prove the your theorem with the following axiom which I think should be some definition for cardinality. > !n,s.s<: X => card(s) = n<=> (#f.f : 1..n>>> s) > I've been down this road before with cardinality. > Cheers, > Son > > On 8 Feb 2012, at 12:00, Thai Son Hoang wrote: > >> Hi Ken, >> On 8 Feb 2012, at 11:13, Ken Robinson wrote: >> >>> Hello everyone, >>> >>> I fear this email will demonstrate that I am an idiot, but here goes. >>> >> >> You are certainly not. >> >>> My problems with card are long standing and persistent. >>> >> >> It is the same feeling for me. >> >>> As usual I am cleaning up on POs that are undischarged under the new Rodin, 2.4. >>> >> >> I assume that you they are undischarged with the old Rodin as well. >> >>> As usual I am having trouble with card. >>> >>> For example: >>> >>> SETS >>> X >>> finite X >>> >>> xs<: X >>> >>> Prove >>> x : xs => card(xs \ {x}) = card(xs)  1 >>> >>> So far this has resisted all my efforts to discharge it. >>> >>> and I've been this way before. >>> >>> I hope, and will be grateful, if someone can demonstrate a proof. >>> >>> And I'm hoping it will show that I am an idiot. >>> >>> If not then I think this is a worry, as to many this poses a serious credibility problem for EventB. >>> >>> Without knowing the EventB axioms, this would appear to be axiomatic to most people. >>> >>> I will be grateful for any resolution of my ineptitude. >>> >> >> You are probably want to the following feature request which has not been implemented. >> http://sourceforge.net/tracker/index.php?func=detail&aid=3191061&group_id=108850&atid=651672 >> But I think the main problem is a missing "definition" for cardinality, something along the line of the following request. >> http://sourceforge.net/tracker/index.php?func=detail&aid=2922308&group_id=108850&atid=651672 >> Cheers, >> Son > >  > Thai Son Hoang > CNB F105.2 > ETH Zentrum, Zurich, Switzerland > Tel: +41 44 632 85 94 > Fax: +41 44 632 11 72 > > > >  > Keep Your Developer Skills Current with LearnDevNow! > The most comprehensive online learning library for Microsoft developers > is just $99.99! Visual Studio, SharePoint, SQL  plus HTML5, CSS3, MVC3, > Metro Style Apps, more. Free future releases when you subscribe now! > http://p.sf.net/sfu/learndevnowd2d > > > > _______________________________________________ > Rodinbsharpuser mailing list > Rodinbsharpuser@... > https://lists.sourceforge.net/lists/listinfo/rodinbsharpuser 
From: Hoang, Thai Son <htson@in...>  20120208 11:33:16

Dear Ken, I just realised that I did not push my last reply to the mailing list. I just did some experiment with cardinality. I can prove the your theorem with the following axiom which I think should be some definition for cardinality. !n,s.s <: X => card(s) = n <=> (#f.f : 1..n >>> s) I've been down this road before with cardinality. Cheers, Son On 8 Feb 2012, at 12:00, Thai Son Hoang wrote: > Hi Ken, > On 8 Feb 2012, at 11:13, Ken Robinson wrote: > >> Hello everyone, >> >> I fear this email will demonstrate that I am an idiot, but here goes. >> > > You are certainly not. > >> My problems with card are long standing and persistent. >> > > It is the same feeling for me. > >> As usual I am cleaning up on POs that are undischarged under the new Rodin, 2.4. >> > > I assume that you they are undischarged with the old Rodin as well. > >> As usual I am having trouble with card. >> >> For example: >> >> SETS >> X >> finite X >> >> xs <: X >> >> Prove >> x : xs => card(xs \ {x}) = card(xs)  1 >> >> So far this has resisted all my efforts to discharge it. >> >> and I've been this way before. >> >> I hope, and will be grateful, if someone can demonstrate a proof. >> >> And I'm hoping it will show that I am an idiot. >> >> If not then I think this is a worry, as to many this poses a serious credibility problem for EventB. >> >> Without knowing the EventB axioms, this would appear to be axiomatic to most people. >> >> I will be grateful for any resolution of my ineptitude. >> > > You are probably want to the following feature request which has not been implemented. > http://sourceforge.net/tracker/index.php?func=detail&aid=3191061&group_id=108850&atid=651672 > But I think the main problem is a missing "definition" for cardinality, something along the line of the following request. > http://sourceforge.net/tracker/index.php?func=detail&aid=2922308&group_id=108850&atid=651672 > Cheers, > Son  Thai Son Hoang CNB F105.2 ETH Zentrum, Zurich, Switzerland Tel: +41 44 632 85 94 Fax: +41 44 632 11 72 
From: Ken Robinson <kenr@cs...>  20120208 10:26:15

Hello everyone, I fear this email will demonstrate that I am an idiot, but here goes. My problems with card are long standing and persistent. As usual I am cleaning up on POs that are undischarged under the new Rodin, 2.4. As usual I am having trouble with card. For example: SETS X finite X xs <: X Prove x : xs => card(xs \ {x}) = card(xs)  1 So far this has resisted all my efforts to discharge it. and I've been this way before. I hope, and will be grateful, if someone can demonstrate a proof. And I'm hoping it will show that I am an idiot. If not then I think this is a worry, as to many this poses a serious credibility problem for EventB. Without knowing the EventB axioms, this would appear to be axiomatic to most people. I will be grateful for any resolution of my ineptitude. Cheers, Ken Ken Robinson School of Computer Science & Engineering UNSW NSW 2052 CRICOS Provider No: 00098G This message is intended for the addressee named and may contain confidential information. If you are not the intended recipient, please delete it and notify the sender. Views expressed in this message are those of the individual sender and are not necessarily the views of UNSW. 
From: Nicolas Beauger <nicolas.beauger@sy...>  20120203 14:01:55

Dear Rodin users, Rodin 2.4 is now available, with new features described at: http://wiki.eventb.org/index.php/Rodin_Platform_2.4_Release_Notes Here is the download area on SourceForge: http://sourceforge.net/projects/rodinbsharp/files/Core_Rodin_Platform/2.4/ For this new release and subsequent ones, we also provide 64 bit binaries for Linux and Windows: we hope it will simplify the usage of Rodin for the many of you running 64 bit OSes. Happy modelling ! The Rodin Team 