# Re: [isabelle] Code generator "eq" instances

```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"

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,
Florian

--

Home:
http://www.in.tum.de/~haftmann

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

```

Attachment: signature.asc
Description: OpenPGP digital signature

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