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,
Quoting Tim Kremann <twkrema at orion.ncsc.mil>:
Here is a simple function declaration and lemma.:
fun f::"nat => nat"
"f n = (if n = 0
else f (n - 1))"
declare f.simps [simp del]
lemma "f (f n) = (1::nat)"
(* apply(simp) --- loops without declare, with declare does nothing
(* apply(unfold f.simps) -- loops with and without declare *)
I thought I could prevent the looping with unfold. How come this does
This archive was generated by a fusion of
Pipermail (Mailman edition) and