[isabelle] Code generator "eq" instances



I'm trying to understand how to safely generate Haskell code from HOL, where I want the Haskell code to be an instance of the Eq class, but with my own definition of the (==) method. I want Isabelle to enforce that my definition of (==) is sound, i.e. it implements logical equality.

So I'm trying to make my datatype an instance of the eq class, but I'm running into an error when using the function package to make the corresponding definition. Here's an example theory file:

theory Silly
imports Main
begin

datatype silly = Silly int

instantiation silly :: eq
begin

fun "eq_class.eq" where
  "eq (Silly n) (Silly m) = (m - n = 0)"

instance ..

end


The "fun" command returns the error

  *** Bad name binding "eq_class.eq"
  *** At command "fun".

Am I, in fact, doing something silly here?

Thanks,
-john


Attachment: smime.p7s
Description: S/MIME cryptographic signature



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