Hi Jasmin, On 07/30/2013 05:40 PM, Jasmin Christian Blanchette wrote:
A rough, optimistic time plan follows.
[...]
Wow, I'm looking forward to it! Let me quickly review the dependencies of the function package on the datatype package: - The package registers a datatype interpretation to generate congruence rules the case combinator for each type. - The pattern splitting code and the pat_completeness method both retrieves the constructors for a given type, using Datatype.get_constrs. - The pat_completeness method also uses the exhaust theorem. - partial_function also destructs the case combinator and looks up rewrite rules for it. - The automated pattern proofs implicitly invoked by "fun" (essentially, the "auto" method) rely implicitly on various things in the simpset, in particular the distinctness and injectivity simp rules. This is the only situation where freeness is used. - The generation of size functions (which was moved into the Function/ subdirectory at some point, but without any real reason) is extremely cryptic. This is mostly because it does a too complex task, essentially reversing the nested-to-mutual conversion in this particular instance. It appears that this should be re-done completely based on the infrastructure of the new package, and it would probably become much simpler. In summary, except for the size functions which are somewhat special (and only used for termination proofs), the function package never uses any inductiveness and would happily swallow codatatypes as well. Thus, I would propose to model the concept of a "type made of constructors" explicitly as a declaration which other tools can look up and add further interpretations to (in the sense of datatype interpretations). The function package would only depend on that. If I understand correctly, that declaration would essentially be rep_datatype without the induction rule. The function package (and I assume other tools, such as case syntax generation) can only rely on that and thus treat datatypes and codadatypes uniformly. But, according to your schedule, these considerations become important only after the coming release, so I'll shut up for the moment.
The corecursive counterpart to "fun", corecursion up-to, is something Andrei urges us to work on, but where Dmitry and I are applying the brakes because of the pile of work that remains to be done on the new (co)datatype package before we can consider adding such nice features. In fact, inspired by Leino et al.'s (co)recursion mixture in Dafny [*], Andrei has some ideas to support some recursion in conjuction with corecursion up-to.
I'd like to learn about corecursion up-to, which I have not come across so far. Are there any good references for this? Or should I rather have a beer with Andrei?
Alex _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev