*To*: noam neer <noamneer at gmail.com>*Subject*: Re: [isabelle] general commands for rewritting real expressions*From*: Lukas Bulwahn <lukas.bulwahn at gmail.com>*Date*: Mon, 25 Jun 2018 16:31:34 +0200*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>

Hi Noam, On Sun, Jun 24, 2018 at 4:54 AM, noam neer <noamneer at gmail.com> wrote: > > 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. > In addition to Larry's answer: I believe you should be made aware of try, try0 and sledgehammer, these commands invoke generally powerful methods; they are not silver bullets but are as automatic as it gets in Isabelle and in interactive theorem provers in general. Other than that, you have the right strategy of decomposing the goal, looking for useful theorems and trying to identify useful lemma sets, such as field_simps, divide_simps etc. Lukas

**Follow-Ups**:**Re: [isabelle] general commands for rewritting real expressions***From:*Eugene W. Stark

**Re: [isabelle] general commands for rewritting real expressions***From:*Nagashima, Yutaka

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

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