Re: [isabelle] Question about fun definitions and unfold
> Here is a simple function declaration and lemma.:
> fun f::"nat => nat"
> "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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and