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)"
    by simp

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:

> 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
>
>
>
>


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