*To*: isabelle-users at cl.cam.ac.uk*Subject*: Re: [isabelle] the definition of minus*From*: Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>*Date*: Mon, 09 Mar 2009 18:59:38 +0100*In-reply-to*: <49B53C4A.3060503@inf.ed.ac.uk>*Organization*: TU München, Lehrstuhl Software and Systems Engineering*References*: <49B53C4A.3060503@inf.ed.ac.uk>*User-agent*: Thunderbird 2.0.0.19 (X11/20090105)

Hi all, > primrec minus_nat > where > diff_0: "m - 0 = (m::nat)" > | diff_Suc: "m - Suc n = (case m - n of 0 => 0 | Suc k => k)" > > I was expecting it to be: > > primrec > diff_0: "0 - m = 0" > | diff_Suc: "(Suc m) - n = (case n of 0 => (Suc m) | Suc k => m - k)" > > which I think would produce better code and seems more "natural" to > me... so I thought I was probably missing some subtlety... I'd be > interested in any reasons for the Isabelle definition. it is important to note that specifications are mainly for *definitional construction* of things; rules for generic tools (simplifier, code generator) can be proven arbitrarily, which happens in this case abundantly. Florian -- Home: http://wwwbroy.in.tum.de/~haftmann PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

**Attachment:
signature.asc**

**References**:**[isabelle] the definition of minus***From:*Lucas Dixon

- Previous by Date: Re: [isabelle] the definition of minus
- Next by Date: [isabelle] 1 Postdoc and 1 PhD vacancy in the MathWiki project
- Previous by Thread: Re: [isabelle] the definition of minus
- Next by Thread: [isabelle] 1 Postdoc and 1 PhD vacancy in the MathWiki project
- Cl-isabelle-users March 2009 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