Re: [isabelle] a simplifier question 3

> >
> >     lemma "(x::real) ^ (4::nat) = x ^ (1+1+1+(1::nat))"
> >     by (simp only : algebra_simps)
> The arithmetic solvers cannot deal with powers, so they cannot solve
> this goal.
> I didn't expect them to deal with powers, I expected them to do (linear)
in a sub expression. everything here happens inside the exponent.
there are cases where they are able to do that, for example in

    lemma "(2*(x::real)+2*y)^(2*x+2*y) = (2*(x+y))^(2*(x+y))"
    by (simp only:algebra_simps)

so I was surprised they didn't succeed here.

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.