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

Andrei Popescu uuomul at yahoo.com
Tue Aug 6 12:12:48 CEST 2013

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:  


There have been many later developments, including very recent work by Stefan Milius: 
(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 
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, 

More information about the isabelle-dev mailing list