Re: [isabelle] nat_code Equation



Am 30.11.2012 15:47, schrieb René Thiemann:
> I would imagine a much simpler equation where
> the proof is also simple.
> 
> lemma [code]: "nat k = (if k ≤ 0 then 0 else Suc (nat (k - 1)))"
> proof (cases k)
>   case (nonneg n)
>   show ?thesis unfolding nonneg
>     by (induct n, auto)
> qed simp

Why not something tail-recursive, which, under the assumption that the
compiler cannot optimize the above into something tail-recursive, should
perform even better (probably except for Haskell):

fun nat' :: "int ⇒ nat ⇒ nat" where
  "nat' k accu = (if k ≤ 0 then accu else nat' (k - 1) (Suc accu))"

lemma nat'_correct:
  "nat' k l = nat k + l"
proof (cases k)
  case (nonneg n)
  show ?thesis unfolding nonneg
    by (induct n arbitrary: l) simp_all
qed simp

lemma [code]: "nat k = nat' k 0"
unfolding nat'_correct by simp

- René

-- 
René Neumann

Institut für Informatik (I7)
Technische Universität München
Boltzmannstr. 3
85748 Garching b. München

Tel: +49-89-289-17232
Office: MI 03.11.055

Attachment: smime.p7s
Description: S/MIME Kryptografische Unterschrift



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