*To*: Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>*Subject*: Re: [isabelle] Code generator "eq" instances*From*: John Matthews <matthews at galois.com>*Date*: Sat, 12 Jun 2010 07:49:12 -0700*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <4C132960.2010100@informatik.tu-muenchen.de>*References*: <DB1C87A2-130B-4055-9F20-43667D59F76B@galois.com> <4C107FBD.2090706@informatik.tu-muenchen.de> <F7D99672-3DA3-4D1C-B45C-1117AD9703CE@galois.com> <4C132960.2010100@informatik.tu-muenchen.de>

Hi Florian, That makes sense, thanks.

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

Hi John,What I'm really trying to do is generate a specialized equalitymethodfor 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 syntacticallysubsumed.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:
smime.p7s**

**Follow-Ups**:**Re: [isabelle] Code generator "eq" instances***From:*John Matthews

**Re: [isabelle] Code generator "eq" instances***From:*Florian Haftmann

**References**:**[isabelle] Code generator "eq" instances***From:*John Matthews

**Re: [isabelle] Code generator "eq" instances***From:*Florian Haftmann

**Re: [isabelle] Code generator "eq" instances***From:*John Matthews

**Re: [isabelle] Code generator "eq" instances***From:*Florian Haftmann

- Previous by Date: Re: [isabelle] Code generator: overloaded numeric constants
- Next by Date: Re: [isabelle] Code generator "eq" instances
- Previous by Thread: Re: [isabelle] Code generator "eq" instances
- Next by Thread: Re: [isabelle] Code generator "eq" instances
- Cl-isabelle-users June 2010 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list