[isabelle] Combining BNF and Quotient



Dear all,

I am trying to convert the Coinductive entry in the AFP to use the new BNF package for the type definitions. So far, the type the type ('a, 'b) tlist has been defined as a quotient of ('a llist * 'b), where 'a llist has been constructed directly in a coinductive style. Most definitions and lemmas about tllist are simply lifted versions of their 'a llist counterparts.

Now, I am wondering whether it is sensible to convert this to BNF or whether I should better stick to the current setup. Or can I have it both ways? Can I define tllist with the BNF package and then setup the quotient package manually (similar to what setup_lifting does for typedefs)? Or can I define the type via quotient_type and then declare to the BNF package that tllist is actually

codata ('a, b) tllist = TNil 'b | TCons 'a "('a, b') tllist"

(this would be similar to rep_datatype)? How could I achieve this? Is there some documentation or example around?

Thanks in advance for any suggestions,
Andreas





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.