*To*: Manuel Eberl <eberlm at in.tum.de>*Subject*: Re: [isabelle] a simplifier question 3*From*: noam neer <noamneer at gmail.com>*Date*: Sat, 4 Jul 2015 00:14:37 +0300*Cc*: "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <5588F18A.2070609@in.tum.de>*References*: <CAGOKs083x+=RbnkcybwRdxcgX5h-ATmjo7hGJUS3rqKTr-2mqQ@mail.gmail.com> <5587BD18.2080504@in.tum.de> <CAGOKs08t=okLAqAfGzC_20UHVgzA6Rv7_s0Jc3db=Hmj0R2BsQ@mail.gmail.com> <5588F18A.2070609@in.tum.de>

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.

- Previous by Date: [isabelle] calling document build from Scala
- Next by Date: [isabelle] libisabelle: embedding on Java-side
- Previous by Thread: Re: [isabelle] calling document build from Scala
- Next by Thread: [isabelle] libisabelle: embedding on Java-side
- Cl-isabelle-users July 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