*To*: noam neer <noamneer at gmail.com>*Subject*: Re: [isabelle] general commands for rewritting real expressions*From*: Lawrence Paulson <lp15 at cam.ac.uk>*Date*: Mon, 25 Jun 2018 12:47:17 +0100*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <CAGOKs09D6F9ypRUk+WToFpvjwUHFFyec6oR46LCcVnZfbYxzNA@mail.gmail.com>*References*: <CAGOKs08qjLj33-E4=hH2joGUOs_gAOT9e9Q-JskWmU5KVNEgyg@mail.gmail.com> <CAGOKs0_VVE6v6yvcypYZhmc5vtj2A_P7iwPcVaO-XsbbhdSzgg@mail.gmail.com> <CAGOKs0_08RJ05ayna+BqfyG8-K+uqqzeM+W9yfpWqtk0=LG6Qw@mail.gmail.com> <CAGOKs08xj1wGWNpfBLoLehZ68Y7+Rn7F5U=-BmXAWQi1F40Ghg@mail.gmail.com> <CAGOKs08S-uxnpN0_hV1p5GmO5Gtc-v5FBPpWNwrMgsZDb=mzuA@mail.gmail.com> <CAGOKs08S5RAkyAmbY-sEbX6MG=VcrqxbwGcsKab8iZ0j4oiszQ@mail.gmail.com> <CAGOKs09gshUKmQSg0oPVyW64UTdkCtcm7tdngo2WPMYXu3kiOQ@mail.gmail.com> <CAGOKs0_vLWFhb-7JORU=bZcp1zirqx6jgj_F1tMZPhe6iL8Kow@mail.gmail.com> <CAGOKs09bOzuC9EYrNoJNAoh-xD7EM74eSDa+KZnLQWPuxVo6Ow@mail.gmail.com> <CAGOKs0_NE+k6FL+1DP0Cy_va-1tJobybLGijaC9ymGAE5YPxDg@mail.gmail.com> <CAGOKs0-0Qv-hT3ucODzFScVE-Kjym1sqGDWcH7ir-WorFAFc2g@mail.gmail.com> <CAGOKs09uO1WXYAS8nwAwVJHY6TEmwMdFp5DX9LN7YRaMZ+vf6w@mail.gmail.com> <CAGOKs09D6F9ypRUk+WToFpvjwUHFFyec6oR46LCcVnZfbYxzNA@mail.gmail.com>

I'm afraid there is no magic bullet for this sort of problem. I often find divide_simps to be more effective than field_simps, but not here. It is obvious how to make that particular example easier to prove. In general though we are all struggling to prove obvious things. Larry Paulson > On 24 Jun 2018, at 03:54, noam neer <noamneer at gmail.com> wrote: > > Hi everybody. > > Whenever I have a rewriting problem (usually involving real expressions) I > try first few general commands like > by auto > by simp > by (simp add: field_simps) > by sledgehammer > > Sometimes none work, for example for > lemma "(x::real)>0 ==> > ((1+x)*(1+x)*(1+x) powr (1/3)) > = > 1+x" > > In such cases I sometimes decompose the problem to a few simpler ones, and > sometimes delve into the HOL libraries looking for something useful to add > to simp, possibly reversed. > > Since these solutions are somewhat tedious, my question is - are there > other general commands I can try at this point? Or maybe something like > 'field_simps' that is more appropriate for real expressions? Any advice > would be appreciated. > > Thanx.

**References**:**[isabelle] general commands for rewritting real expressions***From:*noam neer

- Previous by Date: Re: [isabelle] make_string
- Next by Date: Re: [isabelle] make_string
- Previous by Thread: [isabelle] general commands for rewritting real expressions
- Next by Thread: Re: [isabelle] general commands for rewritting real expressions
- Cl-isabelle-users June 2018 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