Re: [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?

unfold is brute-force unfolding, not stopped by if-then-else.
Please read the section 3.5.3 Simplication in the Tutorial, it explains
how to avoid your simp problems.

Tobias





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