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