Re: [isabelle] Combining BNF and Quotient



On 03/07/2013 08:32 AM, Andreas Lochbihler wrote:
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

Hi Andreas,

You can setup the Lifting package manually even for quotient types. Again by setup_lifting by providing the Quotient theorem (and optionally reflp theorem). See the documentation in The Isabelle/Isar Reference Manual. An example is in Word.thy. The command setup_lifting is not only for typedefs.

If you mean the Quotient package by Kaliszyk, Urban, I think you would have to go to the ML level (which doesn't exist, I know ;)) to setup the package manually.

Ondrej





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