Re: [isabelle] a simplifier question 3
this reply is just for clarification :
I didn't want to use the linear arithmetic part at all.
for example, here it seems the simplifier performs arithmetic rewrites
without it -
lemma "sin(4) = sin(1+1+1+1)"
so I wondered why when the sin() was replaced by x^() it didn't.
today I found that the following works -
lemma "(x::real)^(4) = x^(1+1+1+1)"
by (simp del: One_nat_def)
if the rule 'One_nat_def' isn't deleted the simplifier rewrites
x^(1+1+1+1) --> x*x*x*x
after which it gets stuck. so this seems to solve my problem.
(and if one wants to prevent the simplifier from overworking on terms
like "2^(2^100)", one can add "del: power_numeral".)
On Tue, Jun 23, 2015 at 8:41 AM, Manuel Eberl <eberlm at in.tum.de> wrote:
> "(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.
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