# Re: [isabelle] a simplifier question 3

Hallo,
"(2*(x::real)+2*y)^(2*x+2*y) = (2*(x+y))^(2*(x+y))"
gets rewritten with algebra_simps (which contains, among other things, distributivity) to
"(real x * 2 + real y * 2) ^ (x * 2 + y * 2) =
(real x * 2 + real y * 2) ^ (x * 2 + y * 2)"
which is trivially true. The decision procedure for linear arithmetic has nothing to do with this. You can see that when you write
lemma "(2*(x::real)+2*y)^(2*x+2*y) = (2*(x+y))^(2*(x+y))"
unfolding algebra_simps
The linear arithmetic simproc handles equations and inequalities involving linear arithmetic, i.e. it applies to something of the form "2*x = x + x", never to something like "2*x" alone.
An equation like "(x::real) ^ (4::nat) = x ^ (1+1+1+(1::nat))" is not in the supported fragment because, clearly, the power operation is not linear. This particular problem can be reduced to the (trivially) linear problem "(4::nat) = 1+1+1+1", but the simplifier does not âknowâ that. For the simproc to apply, the simplifier would first have to set up the goal "(4::nat) = 1+1+1+1", and it does not do that, because that is just not how the simplifier works.
Cheers,
Manuel

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*