Re: [isabelle] Adding a code equation for a class parameter



My mail client mangled the Unicode symbols. I attached the theory file for
reproducing the problem.

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


-- 

Attachment: Scratch.thy
Description: Binary data



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