Re: [isabelle] Code generator "eq" instances

Hi Florian,

That makes sense, thanks.

In Section 2.5 ("Datatypes") of the codegen tutorial, when you talk about the code_datatype command you might want to mention that the user has to explicitly [code del] any definitions that use the old versions of the constructors, including automatically generated definitions like eq_class.eq. You might even want to consider adding some text showing how to add the concrete equality method for the AQueue example, but that would be more work. :)

Also, in the isar_ref manual, the syntax diagram for code_datatype is incorrect: It should take a list of consts, not a single const.


On Jun 11, 2010, at 11:29 PM, Florian Haftmann wrote:

Hi John,

What I'm really trying to do is generate a specialized equality method
for your amortized queue code generation example. So I've defined the
abstract version of the queue type as a single linked list, with the
corresponding queue method definitions:

 lemma eq_AQueue[code]:
"eq_class.eq (AQueue xs ys) (AQueue xs' ys') = (ys @ rev xs = ys' @
rev xs')"
 by (auto simp add: AQueue_def eq_class.eq)

the problem is that the old equation using Queue is still kept as code
equations;  you can either delete it explicitly:

 lemma [code del]:
   "eq_class.eq (Queue xs) (Queue ys) <--> xs = ys"

Or, which is perhaps more elegant, define an explicit conversion from
queues to lists:

 primrec list_of_queue :: "'a queue \<Rightarrow> 'a list" where
   "list_of_queue (Queue xs) = xs"

 lemma list_of_AQueue [code]:
   "list_of_queue (AQueue xs ys) = ys @ rev xs"
   by (simp add: AQueue_def)

 lemma [code]:
   "HOL.eq q1 q2 \<longleftrightarrow>
     HOL.eq (list_of_queue q1) (list_of_queue q2)"
   by (auto simp add: eq intro: queue_eqI)

Then the old code equation is dropped since it is syntactically subsumed.

Hope this helps,



PGP available:

Attachment: smime.p7s
Description: S/MIME cryptographic signature

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