Re: [isabelle] the definition of minus



Hi all,

> 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.

it is important to note that specifications are mainly for *definitional
construction* of things;  rules for generic tools (simplifier, code
generator) can be proven arbitrarily, which happens in this case abundantly.

	Florian

-- 

Home:
http://wwwbroy.in.tum.de/~haftmann

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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