*To*: Lars Noschinski <noschinl at in.tum.de>*Subject*: Re: [isabelle] a simplifier question 3*From*: noam neer <noamneer at gmail.com>*Date*: Tue, 23 Jun 2015 01:37:42 +0300*Cc*: "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <5587BD18.2080504@in.tum.de>*References*: <CAGOKs083x+=RbnkcybwRdxcgX5h-ATmjo7hGJUS3rqKTr-2mqQ@mail.gmail.com> <5587BD18.2080504@in.tum.de>

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

**Follow-Ups**:**Re: [isabelle] a simplifier question 3***From:*Manuel Eberl

**References**:**[isabelle] a simplifier question 3***From:*noam neer

**Re: [isabelle] a simplifier question 3***From:*Lars Noschinski

- Previous by Date: Re: [isabelle] Bug in Sledgehammer / cvc4
- Next by Date: Re: [isabelle] a simplifier question 3
- Previous by Thread: Re: [isabelle] a simplifier question 3
- Next by Thread: Re: [isabelle] a simplifier question 3
- Cl-isabelle-users June 2015 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list