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 _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
