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"
    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: signature.asc
Description: OpenPGP digital signature

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