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