I do not know why my message has been added some funny question marks. Neither "Many thanks for your enthusiasm!?" nor "Yes, let us definitely have a beer.?" contained any question marks in my sent message.
Andrei -------------------------------------------- On Tue, 8/6/13, [email protected] <[email protected]> wrote: ---------------------------------------------------------------------- Message: 1 Date: Tue, 6 Aug 2013 03:12:48 -0700 (PDT) From: Andrei Popescu <[email protected]> To: "[email protected]" <[email protected]> Subject: Re: [isabelle-dev] New (Co)datatypes: Status & Plan (FYI) Message-ID: <[email protected]> Content-Type: text/plain; charset=iso-8859-1 Hi Alex, Many thanks for your enthusiasm!? > I'd like to learn about corecursion up-to, which I have not come across so > far. Are there any good references for this? A good early account of the up-to techniques at the level of generality we are interested in is Bartels's generalized coinduction: http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.13.4178&rep=rep1&type=pdf There have been many later developments, including very recent work by Stefan Milius: http://www8.cs.fau.de/~milius/publications/papers.html (see there "Abstract GSOS rules and a Modular Treatment of Recursive Definitions") >> Or should I rather have a beer with Andrei? Yes, let us definitely have a beer.? Corec-up-to seems to mesh well with the function package. For now, what we can handle are function definitions such as the following, where nat_stream is the type of streams of naturals, + is either nat addition or componentwise nat-stream addition, and SCons is "stream cons". f : nat -> nat_stream where n > 10 ==> f n = f (n - 1) + SCons (f (n + 17)) | n <= 10 ==> f n = SCons (f (n + 13)) + SCons (f (n + 11) + f n) With the function package, we find that all (co)recursive calls become eventually guarded (in a properly uniform context), and then use corec-upto. Jasmin has ideas on how to go way beyond this, but let's see if "LCF" can keep up with him. :-) Best regards, Andrei ------------------------------ Message: 2 Date: Tue, 06 Aug 2013 16:41:02 +0200 From: Ren? Neumann <[email protected]> To: [email protected] Subject: [isabelle-dev] Mixfix-Syntax not recognized Message-ID: <[email protected]> Content-Type: text/plain; charset="utf-8" Hi, I'm currently on revision 8d8cb75ab20a, and mixfix-Syntax seems not recognized in all cases (it seems like the syntax is only recognized if the type is known, somewhat...). Toy-Example (? = \<^sup>) : begin definition foo :: "'a list ? nat" ("(_??)") where "foo xs = length xs" term "foo xs" -- "type nat (as expected)" term "xs??" -- "type 'a" term "(xs::'a list)??" -- "type nat (as expected)" lemma fixes xs :: "'a list" -- "learning, I explicitly fixed xs" shows "xs?? = length xs" -- "but still does not recognize ?" by (simp add: foo_def) -- "fails" end It works with Isabelle-2013, but already failed ~100 revisions ago in -dev (unfortunately forgot to write the exact revision down). It is probably related to the thread "Subscripts within identifiers", but I'm not definitly sure. Please just tell me, if I should test a couple more revisions - Ren? -- Ren? Neumann Institut f?r Informatik (I7) Technische Universit?t M?nchen Boltzmannstr. 3 85748 Garching b. M?nchen Tel: +49-89-289-17232 Office: MI 03.11.055 -------------- next part -------------- A non-text attachment was scrubbed... Name: smime.p7s Type: application/pkcs7-signature Size: 4782 bytes Desc: S/MIME Kryptografische Unterschrift URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20130806/942cf7d9/attachment-0001.p7s> ------------------------------ Message: 3 Date: Tue, 06 Aug 2013 17:17:45 +0200 From: Ren? Neumann <[email protected]> To: [email protected] Subject: Re: [isabelle-dev] Mixfix-Syntax not recognized Message-ID: <[email protected]> Content-Type: text/plain; charset="utf-8" Am 06.08.2013 16:41, schrieb Ren? Neumann: > Hi, > > I'm currently on revision 8d8cb75ab20a, and mixfix-Syntax seems not > recognized in all cases (it seems like the syntax is only recognized if > the type is known, somewhat...). > > Toy-Example (? = \<^sup>) : > > begin > definition foo :: "'a list ? nat" ("(_??)") where > "foo xs = length xs" > > term "foo xs" -- "type nat (as expected)" > term "xs??" -- "type 'a" > term "(xs::'a list)??" -- "type nat (as expected)" "xs ??" (note the space) works. - Ren? -- Ren? Neumann Institut f?r Informatik (I7) Technische Universit?t M?nchen Boltzmannstr. 3 85748 Garching b. M?nchen Tel: +49-89-289-17232 Office: MI 03.11.055 -------------- next part -------------- A non-text attachment was scrubbed... Name: smime.p7s Type: application/pkcs7-signature Size: 4782 bytes Desc: S/MIME Kryptografische Unterschrift URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20130806/5a30a15b/attachment.p7s> ------------------------------ Subject: Digest Footer _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ------------------------------ End of isabelle-dev Digest, Vol 75, Issue 12 ******************************************** _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
