*To*: isabelle-users at cl.cam.ac.uk*Subject*: Re: [isabelle] Adding a code equation for a class parameter*From*: "Lars Hupel" <hupel at in.tum.de>*Date*: Wed, 9 Oct 2013 15:59:53 +0200*Importance*: Normal*In-reply-to*: <203748e087e982fecb9a43948d0a99d8-EhVcX1hCQQpcRwURGhY3AF9BdAJSS1xcXF9EBlw1WENZS1kNVkFyBktcXjBeQk0DXFhfSFBV-webmailer1@server02.webmailer.hosteurope.de>*References*: <203748e087e982fecb9a43948d0a99d8-EhVcX1hCQQpcRwURGhY3AF9BdAJSS1xcXF9EBlw1WENZS1kNVkFyBktcXjBeQk0DXFhfSFBV-webmailer1@server02.webmailer.hosteurope.de>*Reply-to*: hupel at in.tum.de*User-agent*: Host Europe Webmailer/1.0

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

**References**:**[isabelle] Adding a code equation for a class parameter***From:*Lars Hupel

- Previous by Date: Re: [isabelle] Isabelle2013-1-RC2 available for testing
- Next by Date: Re: [isabelle] Adding a code equation for a class parameter
- Previous by Thread: [isabelle] Adding a code equation for a class parameter
- Next by Thread: Re: [isabelle] Adding a code equation for a class parameter
- Cl-isabelle-users October 2013 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list