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 +  
depthE b)"
    apply simp
    apply (induct_tac a)
    apply (simp_all add: depthE_bg_0)
done

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])
apply simp
done

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)

   Norbert





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