[isabelle] Question about fun definitions and unfold



Here is a simple function declaration and lemma.:

fun f::"nat => nat"
where
"f n  = (if n = 0
           then (1::nat)
           else f (n - 1))"

declare f.simps [simp del]

lemma "f (f n) = (1::nat)"
(* apply(simp) --- loops without declare, with declare does nothing useful *)
(* apply(unfold f.simps) -- loops with and without declare *)

I thought I could prevent the looping with unfold. How come this does not work?

Thanks,
Tim




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