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

[Andrei Popescu]

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