*To*: John Matthews <matthews at galois.com>, isabelle-users <isabelle-users at cl.cam.ac.uk>*Subject*: Re: [isabelle] Code generator "eq" instances*From*: Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>*Date*: Mon, 14 Jun 2010 08:50:31 +0200*In-reply-to*: <9B3C0442-5B9F-4EE9-A395-A5F193DD5CAF@galois.com>*Organization*: TU München, Lehrstuhl Software and Systems Engineering*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> <9B3C0442-5B9F-4EE9-A395-A5F193DD5CAF@galois.com>*User-agent*: Mozilla/5.0 (X11; U; Linux i686; en-US; rv:1.9.1.9) Gecko/20100423 Thunderbird/3.0.4

Hi John, > 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. thanks for pointing this out. > I may have spoke too soon: trying your [code del] trick didn't work. Here's the exact lemma I used: > > lemma [code del]: > "eq_class.eq (Queue xs) (Queue ys) \<longleftrightarrow> xs = ys" > by (simp add: eq_equals) > > But I still get the same error when trying to generate Haskell code. I've also attached the two theory files. Unfortunately I did not give names to those theorems (but I have convinced myself that it should be done) -- identifying theorems by proposition only is brittle. In such situations use the following: lemma [code, code del]: "(eq_class.eq :: 'a queue => _) = eq_class.eq" by (rule refl) This inserts a code equations which will subsume all others syntactically, and deletes it immediately afterwards, leaving no code equations at all. An alternative is the list_of_queue approach I described in an earlier e-mail: >> 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**

**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

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

- Previous by Date: Re: [isabelle] power class instantiation
- Next by Date: Re: [isabelle] Code generator: overloaded numeric constants
- Previous by Thread: Re: [isabelle] Code generator "eq" instances
- Next by Thread: [isabelle] safe for boolean equality
- 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