Re: [isabelle] Combining BNF and Quotient
Am 07.03.2013 um 08:32 schrieb Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>:
> 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 (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