*To*: <hupel at in.tum.de>, <isabelle-users at cl.cam.ac.uk>*Subject*: Re: [isabelle] Adding a code equation for a class parameter*From*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Date*: Wed, 9 Oct 2013 16:07:02 +0200*In-reply-to*: <203748e087e982fecb9a43948d0a99d8-EhVcX1hCQQpcRwURGhY3AF9BdAJSS1xcXF9EBlw1WENZS1kNVkFyBktcXjBeQk0DXFhfSFBV-webmailer1@server02.webmailer.hosteurope.de>*References*: <203748e087e982fecb9a43948d0a99d8-EhVcX1hCQQpcRwURGhY3AF9BdAJSS1xcXF9EBlw1WENZS1kNVkFyBktcXjBeQk0DXFhfSFBV-webmailer1@server02.webmailer.hosteurope.de>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:24.0) Gecko/20100101 Thunderbird/24.0

Hi Lars,

declare plus_natt.simps [code] lemma [code]: "x + Z = x" by (induct x) auto

Best, Andreas On 09/10/13 15:54, Lars Hupel wrote:

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

**Follow-Ups**:**Re: [isabelle] Adding a code equation for a class parameter***From:*Lars Hupel

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

- Previous by Date: Re: [isabelle] Adding a code equation for a class parameter
- Next by Date: Re: [isabelle] Isabelle2013-1-RC2 available for testing
- Previous by Thread: Re: [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