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.

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

I noticed the definition to minus today (Isabelle2008):

primrec minus_nat
 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:

 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.