# [isabelle] a simplifier question 2

hi.
I have another simplifier question, possibly partly related to the previous
one.
again I have a proof that works-
theory tmp
imports Complex_Main
begin
lemma
fixes a::real
shows "a^6 = a^3 * a^3"
using [[simp_trace=true]]
using power_add [of a 3 3]
by simp
end
and two that don't. the first failed proof is
theory tmp
imports Complex_Main
begin
lemma
fixes a::real
shows "a^6 = a^3 * a^3"
using [[simp_trace=true]]
using power_add
by simp
end
where it seems strange that the smiplifier couldn't find by itself such a
simple substitution. the second failed proof is
theory tmp
imports Complex_Main
begin
lemma
fixes a::real
shows "a^6 = a^3 * a^3"
using [[simp_trace=true]]
by (simp add:power_add [of a 3 3])
end
is the explanation here the same as before, that in this way
"power_add [of a 3 3]" is not available to the linear arith component?
it seems that the simplifier could have done it by itself if it only knew
that "6=3+3". isn't there a way to inform it of this? it seems very
rudimentary.
thanx
--
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.*