Re: [isabelle] Combining BNF and Quotient

Hi Andreas,

Am 07.03.2013 um 08:32 schrieb Andreas Lochbihler <andreas.lochbihler at>:

> 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?

If you go for the "quotient -> BNF" direction, there are a couple of things you can do.

1. The "wrap_data" command derives all the characteristic lemmas that are common for datatypes and codatatypes. It is somewhat similar to "rep_datatype" but not quite, because it has nothing to do with (co)induction and (co)recursion, only constructors, discriminators, and selectors. Here's an example of its use

    wrap_data [Nil, Cons] list_case [] [[], [hd, tl]] [[hd: undefined, tl: Nil]]
    apply -
    apply (erule list.exhaust, assumption)
    apply (rule list.inject)
    apply (rule list.distinct)
    apply (rule list.cases)+


Here "Nil", "Cons", and "list_case" must already exist, whereas "hd" and "tl" are defined by the command. The syntax is

    wrap_data <constructors> <case> <discriminator names> <selector names> <default values>

(see "bnf_wrap.ML" for details). With a bit of ML, you could export the properties of codatatypes and their (co)iterators/recursors under the familiar names given by "codata". Ideally, we would rename "wrap_data" to, say, "wrap_pre_data" and provide additionally "wrap_data" and "wrap_codata" to finish the job. Perhaps you could help us design good interfaces for this pair, since you apparently would need "wrap_codata".

2. If you want to do (co)recursion through one of the "tllist" type arguments, you will need to register the type as a BNF. For this there currently is only one way, namely "bnf_def", which you already used before for the "option" type IIRC.

I hope this helps.



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