*To*: Lucas Dixon <ldixon at inf.ed.ac.uk>*Subject*: Re: [isabelle] the definition of minus*From*: Lawrence Paulson <lp15 at cam.ac.uk>*Date*: Mon, 9 Mar 2009 16:14:29 +0000*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <49B53C4A.3060503@inf.ed.ac.uk>*References*: <49B53C4A.3060503@inf.ed.ac.uk>

Larry On 9 Mar 2009, at 15:56, Lucas Dixon wrote:

Hello, I noticed the definition to minus today (Isabelle2008): 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.

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

- Previous by Date: [isabelle] the definition of minus
- Next by Date: Re: [isabelle] the definition of minus
- Previous by Thread: [isabelle] the definition of minus
- Next by Thread: Re: [isabelle] the definition of minus
- 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