# [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.*