[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

datatype silly = Silly int

instantiation silly :: eq

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

instance ..


The "fun" command returns the error

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

Am I, in fact, doing something silly here?


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

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