There are manual examples in llistScript.sml and lbtreeScript.sml (both in src/llist). The predicate lrep_ok which characterises the subset of the representing type for "lazy lists" is coinductive. There are inversion and induction theorems proved for this constant. Something pretty similar is done for the "lazy binary trees" in lbtreeScript.sml.
Note how this manual form of definition (with a ∃) is dual to the way inductive constants like pred_set$FINITE is defined with ∀. Michael On 09/04/13 16:14, Ramana Kumar wrote: > Dear HOL users, > Is there any support in HOL for defining coinductive relations? > If not, is there at least an example where it was done "manually"? > If not, would anyone be interested in sketching out what would be required, > and > possibly working on it with me? Probably at least some of the Hol_reln > machinery > could be reused. > Cheers, > Ramana > ------------------------------------------------------------------------------ > Precog is a next-generation analytics platform capable of advanced > analytics on semi-structured data. The platform includes APIs for building > apps and a phenomenal toolset for data science. Developers can use > our toolset for easy data analysis & visualization. Get a free account! > http://www2.precog.com/precogplatform/slashdotnewsletter > _______________________________________________ > hol-info mailing list > [email protected] > https://lists.sourceforge.net/lists/listinfo/hol-info
signature.asc
Description: OpenPGP digital signature
------------------------------------------------------------------------------ Precog is a next-generation analytics platform capable of advanced analytics on semi-structured data. The platform includes APIs for building apps and a phenomenal toolset for data science. Developers can use our toolset for easy data analysis & visualization. Get a free account! http://www2.precog.com/precogplatform/slashdotnewsletter
_______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
