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
On 9 Mar 2009, at 15:56, Lucas Dixon wrote:
I noticed the definition to minus today (Isabelle2008):
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