*To*: Lawrence Paulson <lp15 at cam.ac.uk>*Subject*: Re: [isabelle] yet another simplifier question*From*: noam neer <noamneer at gmail.com>*Date*: Sun, 6 Nov 2016 19:16:25 +0200*Cc*: Tobias Nipkow <nipkow at in.tum.de>, "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <BE52C37D-839B-41E5-AFCC-62DA5563D817@cam.ac.uk>*References*: <CAGOKs0_QVcuM1gVkD3kt3wnpSONdP-vFFzO+qcaA6MjDAH4Z9g@mail.gmail.com> <a0ba4baa-8d66-ce82-9092-e992ff31ea26@in.tum.de> <CAGOKs08vyp6s4DvU8tVedaXM=7RTkL9kRzWSwKCPoc7O-hjGiQ@mail.gmail.com> <BE52C37D-839B-41E5-AFCC-62DA5563D817@cam.ac.uk>

hi, I just experimented with sledgehammer for the first time. it seems quite impressive, but also a little unstable. sometimes it doesn't return any output, sometimes I get messages like "z3": Timed out. (and four more lines like this) and sometimes it does return a useful command. so it seems I always have to try it several times. is there a way to make it more stable? I'm using the default installation of Isabelle 2015 on win7. also, I bring here two examples for which sledgehammer failed repeatedly. what would be the simplest way to prove them? lemma fixes a::real assumes "a>0" shows "1/a - 1/(a+1) = 1/(a*(a+1))" oops lemma fixes a b c :: real assumes "a>0" shows "((a powr c) + (b powr c)) powr 2 = (a powr (2*c)) + 2*(a powr c)*(b powr c) + (b powr (2*c))" oops thnx, Noam On Sat, Nov 5, 2016 at 9:33 PM, Lawrence Paulson <lp15 at cam.ac.uk> wrote: > In such situations, you should try simplifying with > > apply (simp add: algebra_simps) > > It works in your example. Sledgehammer also solves your problem. > > There are many other useful packages of rules for such situations, > including field_simps and divide_simps. > > To be quite honest, I never try to trace the simplifier. The output is > simply too massive. I just try something else. > > Larry Paulson > > > On 5 Nov 2016, at 01:47, noam neer <noamneer at gmail.com> wrote: > > first I must admit I didn't know the simplifier can do things to sub > expressions besides application of identities. good to know that. > > > second, is there a documentation of what "field_combine_numerals" can and > can't do? for example to my surprise the following fails (and this was the > trigger to the original question) - > > lemma "sin((x::real) + y + x + y) = sin(2*x + 2*y)" > using [[simp_trace=true]] > by simp (* doesn't work *) > > > also, I must say that the simplifier's output is very hard to read. it > would have been much easier to understand it if there was some identation, > and if there was some declaration where the output of a simproc begins (I > assume much of the output before the produced rewrite rule also came from > the simproc.) can we request this for the next Isabelle revision ? > > >

**Follow-Ups**:**Re: [isabelle] yet another simplifier question***From:*Makarius

**Re: [isabelle] yet another simplifier question***From:*Lawrence Paulson

**References**:**[isabelle] yet another simplifier question***From:*noam neer

**Re: [isabelle] yet another simplifier question***From:*Tobias Nipkow

**Re: [isabelle] yet another simplifier question***From:*noam neer

**Re: [isabelle] yet another simplifier question***From:*Lawrence Paulson

- Previous by Date: Re: [isabelle] yet another simplifier question
- Next by Date: Re: [isabelle] yet another simplifier question
- Previous by Thread: Re: [isabelle] yet another simplifier question
- Next by Thread: Re: [isabelle] yet another simplifier question
- Cl-isabelle-users November 2016 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