[isabelle] Adding a code equation for a class parameter



(Referring to both Isabelle2013 and Isabelle2013-1-RC2.)

Assume the following clone of the `nat` datatype and its obvious
instantiations for `zero` and `plus`, along with some auxiliary
definitions:

  datatype natt = Z | S natt

  instantiation natt :: "{zero,plus}" begin

  definition zero_natt_def:
  "0 = Z"

  primrec plus_natt where
  "Z + x = x" |
  "(S m) + n = S (m + n)"

  instance ..

  end

  fun f :: "'a::plus ⇒ 'a" where
  "f x = x + x"

  definition "i ≡ f (S Z)"

Now, exporting code for `i` works as expected, and

  value [code] i

correctly yields `S (S Z)`.

However, if I add this code equation:

  lemma [code]: "x + Z = x"
  by (induct x) auto

... the generated code looks fishy (there is no warning of "subsumed code
equations" or the like):

  export_code i in SML

  fun plus_natta x Z = x;

Invoking `value [code] i` again produces an error:

  Warning: Matches are not exhaustive.
  fun plus_natta x Z = x
  At (line 23 of "generated code")
  Exception- Match raised

(Side note: `value [simp] i` fails to produce a normal form too, it just
prints `S Z + S Z`.)

I have no idea why that happens. Is what I'm trying to do even supported?
I couldn't find a hint in the type class tutorial (nor in the code
generation tutorial).




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