Re: [isabelle] recdef hint ignored
On Monday 17 October 2005 05:52, Reto Kramer wrote:
First, your lemma doesn't really state the truth
of the subgoal, because the subgoal concerns the constant matchE and
your lemma has variable of that name. Replaced it by this lemma,
which should work better with the simplifier:
lemma depth2E_bg_1 [simp]:
"Suc (depthE x + depthE y) < depthE (Diff x y) + (depthE a +
apply (induct_tac a)
apply (simp_all add: depthE_bg_0)
You have to present this lemma as a intro hint to recdef. I do not know why
it does not work as a simp hint.
The termination proof works now, but the resulting equations are still ugly.
This can be fixed by the following lemma:
lemma depthE_1_sum: "Suc 0 < depthE e1 + depthE e2"
apply (insert depthE_bg_0 [of e1])
apply (insert depthE_bg_0 [of e2])
Moreover, you have to tell the simplifier to look under the if-then-else and
the case distinction on the expressions to get the intended equations.
So here is the full bunch of hints.
(hints intro: depth2E_bg_1 recdef_simp: depthE_bg_0
cong: if_cong expr.case_cong
simp: depthE_bg_0 depthE_1_sum)
This archive was generated by a fusion of
Pipermail (Mailman edition) and