Re: [isabelle] yet another simplifier question



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



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.