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