Re: [isabelle] the definition of minus



We use the traditional definition, which embodies the principle that subtraction consists of repeated application of the predecessor function. Yours does have advantages, however. For example, it is tail recursive. When this work was done, code generation was not even envisaged.
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.






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