[isabelle-dev] New (Co)datatypes: Status & Plan (FYI)

[Andrei Popescu]

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, isabelle-dev-request at mailbroy.informatik.tu-muenchen.de <isabelle-dev-request at mailbroy.informatik.tu-muenchen.de> wrote:

 ----------------------------------------------------------------------
 
 Message: 1
 Date: Tue, 6 Aug 2013 03:12:48 -0700 (PDT)
 From: Andrei Popescu <uuomul at yahoo.com>
 To: "isabelle-dev at mailbroy.informatik.tu-muenchen.de"
     <isabelle-dev at mailbroy.informatik.tu-muenchen.de>
 Subject: Re: [isabelle-dev] New (Co)datatypes: Status &
 Plan (FYI)
 Message-ID:
     <1375783968.46010.YahooMailBasic at web120604.mail.ne1.yahoo.com>
 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 <rene.neumann at in.tum.de>
 To: isabelle-dev at mailbroy.informatik.tu-muenchen.de
 Subject: [isabelle-dev] Mixfix-Syntax not recognized
 Message-ID: <52010AFE.2010009 at in.tum.de>
 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 <rene.neumann at in.tum.de>
 To: isabelle-dev at mailbroy.informatik.tu-muenchen.de
 Subject: Re: [isabelle-dev] Mixfix-Syntax not recognized
 Message-ID: <52011399.2080103 at in.tum.de>
 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
 isabelle-dev at mailbroy.informatik.tu-muenchen.de
 https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
 
 
 ------------------------------
 
 End of isabelle-dev Digest, Vol 75, Issue 12
 ********************************************