Re: [isabelle] a simplifier question 3


"(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.



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