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