[isabelle] a simplifier question 3



hi.

again I'm nitpicking with simplifier details.
in the following the first proof works while the second doesn't,
and I don't understand why.

theory tmp
imports Complex_Main
begin

    lemma "(4::nat) = 1+1+1+1"
    by (simp only : algebra_simps)

    lemma "(x::real) ^ (4::nat) = x ^ (1+1+1+(1::nat))"
    by (simp only : algebra_simps)

end

the second proof fails even if I replace 'only' with 'add'.
I know that the second lemma can be proved with
    by (simp add:eval_nat_numeral)
but I'm trying to use the simplifier with as little simp rules as possible.
the reason is that applying it to expressions that contain something like
"2^(2^100)" might get the computer stuck, and the 'only' seems to protect
from it.
if u have a different solution to this problem I'd be happy to hear as well.


thnx



-- 
I can't see very far,
I must be standing on the shoulders of midgets.



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