[isabelle] the definition of minus



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.

thanks,
lucas

-- 
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.






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