Re: [isabelle] Code generator "eq" instances

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

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