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}
(8) 
S  M  T  W  T  F  S 




1

2

3

4

5

6

7

8

9

10

11

12

13

14
(3) 
15

16

17

18

19

20

21

22

23
(6) 
24
(4) 
25

26

27

28

29
(2) 
30



From: JeanRaymond Abrial <jabrial@in...>  20090429 03:55:07

Dear Nastaran, This is the way to do it. You may have had a syntax error for another reason. Given a binary relation r, the reverse (or converse, or inverse) of r is denoted by r~ Cheers, JeanRaymond On Apr 29, 2009, at 3:55 AM, Nastaran Shafiei wrote: > Hello, > > I was wondering how I can define the reverse of a function in Rodin. I > tried using the character "~" right after the function name but I get > syntax error. > > Thanks, > Nastaran > >  > This message was sent using IMP, the Internet Messaging Program. > > >  > Register Now & Save for Velocity, the Web Performance & Operations > Conference from O'Reilly Media. Velocity features a full day of > expertled, handson workshops and two days of sessions from industry > leaders in dedicated Performance & Operations tracks. Use code > vel09scf > and Save an extra 15% before 5/3. http://p.sf.net/sfu/velocityconf > _______________________________________________ > Rodinbsharpuser mailing list > Rodinbsharpuser@... > https://lists.sourceforge.net/lists/listinfo/rodinbsharpuser 
From: Nastaran Shafiei <nastaran@cs...>  20090429 02:37:13

Hello, I was wondering how I can define the reverse of a function in Rodin. I tried using the character "~" right after the function name but I get syntax error. Thanks, Nastaran  This message was sent using IMP, the Internet Messaging Program. 
From: Jonathan S. Ostroff <jonathan@yo...>  20090424 15:06:15

It would be great to have more information about the provers and prover strategy. Thanks for producing such a nice tool. Jonathan Original Message From: Matthias Schmalz [mailto:Matthias.Schmalz@...] Sent: Friday, April 24, 2009 4:38 AM To: User Rodin Bsharp Subject: Re: [Rodinbsharpuser] Subset and finiteness BEGIN PGP SIGNED MESSAGE Hash: SHA1 Ken, I am not aware of any documentation, and I agree with you that such documentation would be very useful. I realize that not so many people know what is going on inside the provers. So I will write a wikipage about it. Cheers, Matthias Ken Robinson schrieb: > Matthias, > > On 24/04/2009, at 01:47 AM, Matthias Schmalz wrote: > >> Unfortunately, the problem of finding a smallest set of required >> hypotheses is at least as hard as finding a proof  undecidable. >> Currently, there are three ways to select hypotheses: P0 or newPP >> restricted selects the hypotheses you see. >> P1 or newPP lassoo applies one lassoo operation and passes the >> result to >> the prover. The lassoo operation adds any hypothesis that has a common >> free symbol with some hypothesis that you could see before. >> PP and newPP select all hypotheses. >> My experience is, if you have a larger model, then only the first >> way  >> selecting the required hypotheses manually  works well. >> >> It would be interesting to think about some mechanisms that select the >> hypothesis in a smarter way than now. >> >> I hope you have a better prover experience in the future, > > Yes, thanks, and I do realise that there is no solution to finding a > proof. Unfortunately, for me at least, the provers and the prover > interface in Rodin is a black box. It's not clear what each set of > provers does differently one learns by trial and error and it's > certainly not clear "what happens" when you "run" a prover, and by > that I mean how the hypotheses are handled, etc. > > Is there any documentation on any of this? > > Cheers, > > Ken > >   > Crystal Reports  New Free Runtime and 30 Day Trial > Check out the new simplified licensign option that enables unlimited > royaltyfree distribution of the report engine for externally facing > server and web deployment. > http://p.sf.net/sfu/businessobjects > _______________________________________________ > Rodinbsharpuser mailing list > Rodinbsharpuser@... > https://lists.sourceforge.net/lists/listinfo/rodinbsharpuser BEGIN PGP SIGNATURE Version: GnuPG v1.4.6 (GNU/Linux) Comment: Using GnuPG with Mozilla  http://enigmail.mozdev.org iD8DBQFJ8XpiczhznXSdWggRAvtkAJ0aFC+RWKT7LGVekX/7b7efyflSuwCgoLuT EZsDFHlTbFQuSFbr3njXlUU= =BgbE END PGP SIGNATURE   Crystal Reports  New Free Runtime and 30 Day Trial Check out the new simplified licensign option that enables unlimited royaltyfree distribution of the report engine for externally facing server and web deployment. http://p.sf.net/sfu/businessobjects _______________________________________________ Rodinbsharpuser mailing list Rodinbsharpuser@... https://lists.sourceforge.net/lists/listinfo/rodinbsharpuser 
From: Ken Robinson <kenr@cs...>  20090424 08:50:36

Matthias, On 24/04/2009, at 18:37 PM, Matthias Schmalz wrote: > I am not aware of any documentation, and I agree with you that such > documentation would be very useful. > I realize that not so many people know what is going on inside the > provers. > So I will write a wikipage about it. That would be great. Thanks, Ken > Ken Robinson schrieb: >> Matthias, >> >> On 24/04/2009, at 01:47 AM, Matthias Schmalz wrote: >> >>> Unfortunately, the problem of finding a smallest set of required >>> hypotheses is at least as hard as finding a proof  undecidable. >>> Currently, there are three ways to select hypotheses: P0 or newPP >>> restricted selects the hypotheses you see. >>> P1 or newPP lassoo applies one lassoo operation and passes the >>> result to >>> the prover. The lassoo operation adds any hypothesis that has a >>> common >>> free symbol with some hypothesis that you could see before. >>> PP and newPP select all hypotheses. >>> My experience is, if you have a larger model, then only the first >>> way  >>> selecting the required hypotheses manually  works well. >>> >>> It would be interesting to think about some mechanisms that select >>> the >>> hypothesis in a smarter way than now. >>> >>> I hope you have a better prover experience in the future, >> >> Yes, thanks, and I do realise that there is no solution to finding a >> proof. Unfortunately, for me at least, the provers and the prover >> interface in Rodin is a black box. It's not clear what each set of >> provers does differently one learns by trial and error and it's >> certainly not clear "what happens" when you "run" a prover, and by >> that I mean how the hypotheses are handled, etc. >> >> Is there any documentation on any of this? >> >> Cheers, >> >> Ken >> >>  >> Crystal Reports  New Free Runtime and 30 Day Trial >> Check out the new simplified licensign option that enables unlimited >> royaltyfree distribution of the report engine for externally >> facing >> server and web deployment. >> http://p.sf.net/sfu/businessobjects >> _______________________________________________ >> Rodinbsharpuser mailing list >> Rodinbsharpuser@... >> https://lists.sourceforge.net/lists/listinfo/rodinbsharpuser > BEGIN PGP SIGNATURE > Version: GnuPG v1.4.6 (GNU/Linux) > Comment: Using GnuPG with Mozilla  http://enigmail.mozdev.org > > iD8DBQFJ8XpiczhznXSdWggRAvtkAJ0aFC+RWKT7LGVekX/7b7efyflSuwCgoLuT > EZsDFHlTbFQuSFbr3njXlUU= > =BgbE > END PGP SIGNATURE > >  > Crystal Reports  New Free Runtime and 30 Day Trial > Check out the new simplified licensign option that enables unlimited > royaltyfree distribution of the report engine for externally > facing > server and web deployment. > http://p.sf.net/sfu/businessobjects > _______________________________________________ > Rodinbsharpuser mailing list > Rodinbsharpuser@... > https://lists.sourceforge.net/lists/listinfo/rodinbsharpuser 
From: Matthias Schmalz <Matthias.S<chmalz@in...>  20090424 08:38:22

BEGIN PGP SIGNED MESSAGE Hash: SHA1 Ken, I am not aware of any documentation, and I agree with you that such documentation would be very useful. I realize that not so many people know what is going on inside the provers. So I will write a wikipage about it. Cheers, Matthias Ken Robinson schrieb: > Matthias, > > On 24/04/2009, at 01:47 AM, Matthias Schmalz wrote: > >> Unfortunately, the problem of finding a smallest set of required >> hypotheses is at least as hard as finding a proof  undecidable. >> Currently, there are three ways to select hypotheses: P0 or newPP >> restricted selects the hypotheses you see. >> P1 or newPP lassoo applies one lassoo operation and passes the >> result to >> the prover. The lassoo operation adds any hypothesis that has a common >> free symbol with some hypothesis that you could see before. >> PP and newPP select all hypotheses. >> My experience is, if you have a larger model, then only the first >> way  >> selecting the required hypotheses manually  works well. >> >> It would be interesting to think about some mechanisms that select the >> hypothesis in a smarter way than now. >> >> I hope you have a better prover experience in the future, > > Yes, thanks, and I do realise that there is no solution to finding a > proof. Unfortunately, for me at least, the provers and the prover > interface in Rodin is a black box. It's not clear what each set of > provers does differently one learns by trial and error and it's > certainly not clear "what happens" when you "run" a prover, and by > that I mean how the hypotheses are handled, etc. > > Is there any documentation on any of this? > > Cheers, > > Ken > >  > Crystal Reports  New Free Runtime and 30 Day Trial > Check out the new simplified licensign option that enables unlimited > royaltyfree distribution of the report engine for externally facing > server and web deployment. > http://p.sf.net/sfu/businessobjects > _______________________________________________ > Rodinbsharpuser mailing list > Rodinbsharpuser@... > https://lists.sourceforge.net/lists/listinfo/rodinbsharpuser BEGIN PGP SIGNATURE Version: GnuPG v1.4.6 (GNU/Linux) Comment: Using GnuPG with Mozilla  http://enigmail.mozdev.org iD8DBQFJ8XpiczhznXSdWggRAvtkAJ0aFC+RWKT7LGVekX/7b7efyflSuwCgoLuT EZsDFHlTbFQuSFbr3njXlUU= =BgbE END PGP SIGNATURE 
From: Ken Robinson <kenr@cs...>  20090424 05:14:40

Matthias, On 24/04/2009, at 01:47 AM, Matthias Schmalz wrote: > Unfortunately, the problem of finding a smallest set of required > hypotheses is at least as hard as finding a proof  undecidable. > Currently, there are three ways to select hypotheses: P0 or newPP > restricted selects the hypotheses you see. > P1 or newPP lassoo applies one lassoo operation and passes the > result to > the prover. The lassoo operation adds any hypothesis that has a common > free symbol with some hypothesis that you could see before. > PP and newPP select all hypotheses. > My experience is, if you have a larger model, then only the first > way  > selecting the required hypotheses manually  works well. > > It would be interesting to think about some mechanisms that select the > hypothesis in a smarter way than now. > > I hope you have a better prover experience in the future, Yes, thanks, and I do realise that there is no solution to finding a proof. Unfortunately, for me at least, the provers and the prover interface in Rodin is a black box. It's not clear what each set of provers does differently one learns by trial and error and it's certainly not clear "what happens" when you "run" a prover, and by that I mean how the hypotheses are handled, etc. Is there any documentation on any of this? Cheers, Ken 
From: Matthias Schmalz <Matthias.S<chmalz@in...>  20090423 15:48:20

BEGIN PGP SIGNED MESSAGE Hash: SHA1 Ken, Ken Robinson schrieb: > Matthias, > > On 24/04/2009, at 01:00 AM, Matthias Schmalz wrote: > > all available hypotheses are passed to ML. In your case, ML probably > gets distracted by irrelevant hypotheses. In Son's case there are no > irrelevant hypotheses. > It is hard to predict what newPP and PP can discharge. I would proceed > as follows: > 1. remove all hypotheses, but "products <: PRODUCT" > 2. try newPP (restricted) and P0. > 3. If that fails start to unfold the goal and try the automatic > provers > again and again. > 4. If some subgoals cannot be discharged, then please send them to us. > >> Thank you very much. That was a very useful lesson. I never realised >> the problem of having too many hypotheses. Once I removed all >> hypotheses except the critical one it discharged instantly. > >> I've always worked on the principle of "the more hypotheses, the >> better", and often that does seem to be the case. I realise that you >> only need some critical subset, but I guess the easy thing to do is to >> drag in as many as possible. Hmmm. > >> It's interesting that given a large set somehow the provers don't >> finally pick on the right hypotheses to use. There must be some >> limiting process involved? Unfortunately, the problem of finding a smallest set of required hypotheses is at least as hard as finding a proof  undecidable. Currently, there are three ways to select hypotheses: P0 or newPP restricted selects the hypotheses you see. P1 or newPP lassoo applies one lassoo operation and passes the result to the prover. The lassoo operation adds any hypothesis that has a common free symbol with some hypothesis that you could see before. PP and newPP select all hypotheses. My experience is, if you have a larger model, then only the first way  selecting the required hypotheses manually  works well. It would be interesting to think about some mechanisms that select the hypothesis in a smarter way than now. I hope you have a better prover experience in the future, Matthias BEGIN PGP SIGNATURE Version: GnuPG v1.4.6 (GNU/Linux) Comment: Using GnuPG with Mozilla  http://enigmail.mozdev.org iD8DBQFJ8I2nczhznXSdWggRAl5zAJ9B36hC56HvYW6sVPzh0c/XbudrsQCfWhRS 8xh/7Vi3o29chd+wgCfoJ2c= =EN9G END PGP SIGNATURE 
From: Ken Robinson <kenr@cs...>  20090423 15:28:59

Matthias, On 24/04/2009, at 01:00 AM, Matthias Schmalz wrote: > BEGIN PGP SIGNED MESSAGE > > all available hypotheses are passed to ML. In your case, ML probably > gets distracted by irrelevant hypotheses. In Son's case there are no > irrelevant hypotheses. > It is hard to predict what newPP and PP can discharge. I would proceed > as follows: > 1. remove all hypotheses, but "products <: PRODUCT" > 2. try newPP (restricted) and P0. > 3. If that fails start to unfold the goal and try the automatic > provers > again and again. > 4. If some subgoals cannot be discharged, then please send them to us. Thank you very much. That was a very useful lesson. I never realised the problem of having too many hypotheses. Once I removed all hypotheses except the critical one it discharged instantly. I've always worked on the principle of "the more hypotheses, the better", and often that does seem to be the case. I realise that you only need some critical subset, but I guess the easy thing to do is to drag in as many as possible. Hmmm. It's interesting that given a large set somehow the provers don't finally pick on the right hypotheses to use. There must be some limiting process involved? Cheers, Ken > > > Best regards, > > Matthias > > Ken Robinson schrieb: >> Dear Son, >> >> Thanks for that, but ... >> >> On 23/04/2009, at 23:58 PM, Thai Son Hoang wrote: >> >>> Ken Robinson wrote: >>>> I can't find anything about this in the language document, but I am >>>> getting the impression that subset may be restricted to finite >>>> sets? >>>> >>>> I the following PO >>>> >>>> products +> NAT <: PRODUCT +> NAT >>>> >>>> where products is a fine subset of PRODUCT. >>>> >>>> It seems to me that the subset relation is reasonable, but I cannot >>>> get the Rodin provers to discharge it. >>>> >>>> If I replace NAT by a finite set then it does discharge, hence my >>>> conclusion above. >>>> >>>> Is that conclusion correct? >>>> >>>> I would not be asking this question if products was not finite: >>>> clearly there are elements in the rhs set that are not in the lhs >>>> set, >>>> so subset seems reasonable? >>>> >>> I have the following context, >>> CONTEXT >>> ctx >>> SETS >>> PRODUCT >>> CONSTANTS >>> products >>> AXIOMS >>> axm1 : products ⊆ PRODUCT >>> THEOREMS >>> thm1 : products ⇸ ℕ ⊆ PRODUCT ⇸ ℕ >>> END >>> >>> The theorem is proved interactively by clicking on the "<:" follows >>> by ML. >> >> Not when I do it. It doesn't discharge. >> >> But nevertheless you have removed any doubt about finiteness. The >> only difference between your example and mine is that products is a >> variable in mine, and in mine PRODUCT is declared as finite. >> >> More interesting is that in my case, even replacing NAT by a finite >> set, the lemma is not discharged by ml, it requires one of the npp >> provers. >> >> Must be some strange problem with my Rodin, or something. :( >> >> Cheers, >> >> Ken >> >>  >> Stay on top of everything new and different, both inside and >> around Java (TM) technology  register by April 22, and save >> $200 on the JavaOne (SM) conference, June 25, 2009, San Francisco. >> 300 plus technical and handson sessions. Register today. >> Use priority code J9JMT32. http://p.sf.net/sfu/p >> _______________________________________________ >> Rodinbsharpuser mailing list >> Rodinbsharpuser@... >> https://lists.sourceforge.net/lists/listinfo/rodinbsharpuser > BEGIN PGP SIGNATURE > Version: GnuPG v1.4.6 (GNU/Linux) > Comment: Using GnuPG with Mozilla  http://enigmail.mozdev.org > > iD8DBQFJ8IKnczhznXSdWggRAhGMAJ98T/rnkvCxnZifY6yyzvD09zaYvACgjilk > APhR5OdHdw1EqsnB2XImb+k= > =TpII > END PGP SIGNATURE > >  > Stay on top of everything new and different, both inside and > around Java (TM) technology  register by April 22, and save > $200 on the JavaOne (SM) conference, June 25, 2009, San Francisco. > 300 plus technical and handson sessions. Register today. > Use priority code J9JMT32. http://p.sf.net/sfu/p > _______________________________________________ > Rodinbsharpuser mailing list > Rodinbsharpuser@... > https://lists.sourceforge.net/lists/listinfo/rodinbsharpuser 
From: Matthias Schmalz <Matthias.S<chmalz@in...>  20090423 15:01:14

BEGIN PGP SIGNED MESSAGE Hash: SHA1 Ken, all available hypotheses are passed to ML. In your case, ML probably gets distracted by irrelevant hypotheses. In Son's case there are no irrelevant hypotheses. It is hard to predict what newPP and PP can discharge. I would proceed as follows: 1. remove all hypotheses, but "products <: PRODUCT" 2. try newPP (restricted) and P0. 3. If that fails start to unfold the goal and try the automatic provers again and again. 4. If some subgoals cannot be discharged, then please send them to us. Best regards, Matthias Ken Robinson schrieb: > Dear Son, > > Thanks for that, but ... > > On 23/04/2009, at 23:58 PM, Thai Son Hoang wrote: > >> Ken Robinson wrote: >>> I can't find anything about this in the language document, but I am >>> getting the impression that subset may be restricted to finite sets? >>> >>> I the following PO >>> >>> products +> NAT <: PRODUCT +> NAT >>> >>> where products is a fine subset of PRODUCT. >>> >>> It seems to me that the subset relation is reasonable, but I cannot >>> get the Rodin provers to discharge it. >>> >>> If I replace NAT by a finite set then it does discharge, hence my >>> conclusion above. >>> >>> Is that conclusion correct? >>> >>> I would not be asking this question if products was not finite: >>> clearly there are elements in the rhs set that are not in the lhs >>> set, >>> so subset seems reasonable? >>> >> I have the following context, >> CONTEXT >> ctx >> SETS >> PRODUCT >> CONSTANTS >> products >> AXIOMS >> axm1 : products ⊆ PRODUCT >> THEOREMS >> thm1 : products ⇸ ℕ ⊆ PRODUCT ⇸ ℕ >> END >> >> The theorem is proved interactively by clicking on the "<:" follows >> by ML. > > Not when I do it. It doesn't discharge. > > But nevertheless you have removed any doubt about finiteness. The > only difference between your example and mine is that products is a > variable in mine, and in mine PRODUCT is declared as finite. > > More interesting is that in my case, even replacing NAT by a finite > set, the lemma is not discharged by ml, it requires one of the npp > provers. > > Must be some strange problem with my Rodin, or something. :( > > Cheers, > > Ken > >  > Stay on top of everything new and different, both inside and > around Java (TM) technology  register by April 22, and save > $200 on the JavaOne (SM) conference, June 25, 2009, San Francisco. > 300 plus technical and handson sessions. Register today. > Use priority code J9JMT32. http://p.sf.net/sfu/p > _______________________________________________ > Rodinbsharpuser mailing list > Rodinbsharpuser@... > https://lists.sourceforge.net/lists/listinfo/rodinbsharpuser BEGIN PGP SIGNATURE Version: GnuPG v1.4.6 (GNU/Linux) Comment: Using GnuPG with Mozilla  http://enigmail.mozdev.org iD8DBQFJ8IKnczhznXSdWggRAhGMAJ98T/rnkvCxnZifY6yyzvD09zaYvACgjilk APhR5OdHdw1EqsnB2XImb+k= =TpII END PGP SIGNATURE 
From: Ken Robinson <kenr@cs...>  20090423 14:33:53

Dear Son, Thanks for that, but ... On 23/04/2009, at 23:58 PM, Thai Son Hoang wrote: > Ken Robinson wrote: >> I can't find anything about this in the language document, but I am >> getting the impression that subset may be restricted to finite sets? >> >> I the following PO >> >> products +> NAT <: PRODUCT +> NAT >> >> where products is a fine subset of PRODUCT. >> >> It seems to me that the subset relation is reasonable, but I cannot >> get the Rodin provers to discharge it. >> >> If I replace NAT by a finite set then it does discharge, hence my >> conclusion above. >> >> Is that conclusion correct? >> >> I would not be asking this question if products was not finite: >> clearly there are elements in the rhs set that are not in the lhs >> set, >> so subset seems reasonable? >> > > I have the following context, > CONTEXT > ctx > SETS > PRODUCT > CONSTANTS > products > AXIOMS > axm1 : products ⊆ PRODUCT > THEOREMS > thm1 : products ⇸ ℕ ⊆ PRODUCT ⇸ ℕ > END > > The theorem is proved interactively by clicking on the "<:" follows > by ML. Not when I do it. It doesn't discharge. But nevertheless you have removed any doubt about finiteness. The only difference between your example and mine is that products is a variable in mine, and in mine PRODUCT is declared as finite. More interesting is that in my case, even replacing NAT by a finite set, the lemma is not discharged by ml, it requires one of the npp provers. Must be some strange problem with my Rodin, or something. :( Cheers, Ken 
From: Thai Son Hoang <htson@in...>  20090423 13:59:50

Dear Ken, Ken Robinson wrote: > I can't find anything about this in the language document, but I am > getting the impression that subset may be restricted to finite sets? > > I the following PO > > products +> NAT <: PRODUCT +> NAT > > where products is a fine subset of PRODUCT. > > It seems to me that the subset relation is reasonable, but I cannot > get the Rodin provers to discharge it. > > If I replace NAT by a finite set then it does discharge, hence my > conclusion above. > > Is that conclusion correct? > > I would not be asking this question if products was not finite: > clearly there are elements in the rhs set that are not in the lhs set, > so subset seems reasonable? > I have the following context, CONTEXT ctx SETS PRODUCT CONSTANTS products AXIOMS axm1 : products ⊆ PRODUCT THEOREMS thm1 : products ⇸ ℕ ⊆ PRODUCT ⇸ ℕ END The theorem is proved interactively by clicking on the "<:" follows by ML. I do not know the actual consequence of this, but it seems like automatically expanding "<:" is not the strategy of existing provers. Cheers, Son P/S: I guess there is no problem with finiteness at all (even products is not finite). 
From: Ken Robinson <kenr@cs...>  20090423 13:50:21

I can't find anything about this in the language document, but I am getting the impression that subset may be restricted to finite sets? I the following PO products +> NAT <: PRODUCT +> NAT where products is a fine subset of PRODUCT. It seems to me that the subset relation is reasonable, but I cannot get the Rodin provers to discharge it. If I replace NAT by a finite set then it does discharge, hence my conclusion above. Is that conclusion correct? I would not be asking this question if products was not finite: clearly there are elements in the rhs set that are not in the lhs set, so subset seems reasonable? Cheers, Ken 
From: Laurent Voisin <laurent.voisin@sy...>  20090414 12:37:06

Pierre, this is an already known bug caused by a wrong design of the eventB explorer: https://sourceforge.net/tracker/index.php?func=detail&aid=2652410&group_id=108850&atid=651669 In the bug comments, you will find a small procedure for fixing this and having all machines appear linearly in the explorer. Laurent. Le 14 avr. 09 à 12:39, Pierre Castéran a écrit : > > It seems that there is a bug in the display of the components. > In fact the machine LinearSerach I didn't found was hidden as a > subcomponent > of a machine L0. > > P.C. > > > > > > Quoting "Pierre Castéran" <pierre.casteran@...>: > >> Hello, >> >> How to proceed to transfer projects from rodin 9.0 to rodin 9.2 ? >> >> I had a project which ran on 9.0, then exported it into a zip file >> and import it into rodin 9.2. >> >> Some machines and alrready proved PO disappeared and are >> unavailable in >> Rodin 9.2. Must I do it all again ? >> >> I have been tecahing rodin for more than a year, and at each change >> of >> version I had to type again machines and proofs, and I get tired of >> that. >> >> I attach the rodin 9.0 project here, which contains a machine >> LinearSearch >> which does not appear on the eventB and Proving perspective when >> imported into Rodin 9.2. >> Surprisingly, it appears in the Resources perspective. >> >> So, what is the correct upgrading procedure ????? >> >> >> Pierre Castéran > > > > Pierre Castéran > >  > This SF.net email is sponsored by: > High Quality Requirements in a Collaborative Environment. > Download a free trial of Rational Requirements Composer Now! > http://p.sf.net/sfu/wwwibmcom > _______________________________________________ > Rodinbsharpuser mailing list > Rodinbsharpuser@... > https://lists.sourceforge.net/lists/listinfo/rodinbsharpuser >  > Orange vous informe que cet email a ete controle par l'antivirus > mail. > Aucun virus connu a ce jour par nos services n'a ete detecte. > > 
From: Pierre Castéran <pierre.casteran@la...>  20090414 11:10:32

It seems that there is a bug in the display of the components. In fact the machine LinearSerach I didn't found was hidden as a subcomponent of a machine L0. P.C. Quoting "Pierre Castéran" <pierre.casteran@...>: > Hello, > > How to proceed to transfer projects from rodin 9.0 to rodin 9.2 ? > > I had a project which ran on 9.0, then exported it into a zip file > and import it into rodin 9.2. > > Some machines and alrready proved PO disappeared and are unavailable in > Rodin 9.2. Must I do it all again ? > > I have been tecahing rodin for more than a year, and at each change of > version I had to type again machines and proofs, and I get tired of that. > > I attach the rodin 9.0 project here, which contains a machine LinearSearch > which does not appear on the eventB and Proving perspective when > imported into Rodin 9.2. > Surprisingly, it appears in the Resources perspective. > > So, what is the correct upgrading procedure ????? > > > Pierre Castéran Pierre Castéran 
From: Pierre Castéran <pierre.casteran@la...>  20090414 10:53:50

Hello, How to proceed to transfer projects from rodin 9.0 to rodin 9.2 ? I had a project which ran on 9.0, then exported it into a zip file and import it into rodin 9.2. Some machines and alrready proved PO disappeared and are unavailable in Rodin 9.2. Must I do it all again ? I have been tecahing rodin for more than a year, and at each change of version I had to type again machines and proofs, and I get tired of that. I attach the rodin 9.0 project here, which contains a machine LinearSearch which does not appear on the eventB and Proving perspective when imported into Rodin 9.2. Surprisingly, it appears in the Resources perspective. So, what is the correct upgrading procedure ????? Pierre Castéran 