Re: [isabelle] Question about fun definitions and unfold



The "unfold" method applies rewrite rules repeatedly, just like simp. (Internally "unfold" is actually implemented as a call to the simplifier, but with most of the fancy features disabled.)

To avoid the looping, you can either apply (subst f.simps), to rewrite exactly one step; or you can use unfold with an instantiated rule, e.g. apply (unfold f.simps [of n]).

Hope this helps,

- Brian

Quoting Tim Kremann <twkrema at orion.ncsc.mil>:

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.