*To*: Lukas Bulwahn <lukas.bulwahn at gmail.com>, noam neer <noamneer at gmail.com>*Subject*: Re: [isabelle] general commands for rewritting real expressions*From*: "Nagashima, Yutaka" <Yutaka.Nagashima at uibk.ac.at>*Date*: Wed, 27 Jun 2018 09:05:53 +0000*Accept-language*: en-AU, de-AT, en-US*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <CAKXUXMxGm8FOBc7RJ=3Wk_HdBrV42erUOYudqueC=2prnuttvQ@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>, <CAKXUXMxGm8FOBc7RJ=3Wk_HdBrV42erUOYudqueC=2prnuttvQ@mail.gmail.com>*Thread-index*: AQHUC2eBlLjTKp2q70ygPAnoS4Okz6Rw6hgAgALlMNg=*Thread-topic*: [isabelle] general commands for rewritting real expressions

Hi Noam, If neither "try" or "try0" tries hard enough, why don't you try "try_hard" from PSL [1]. Alternatively, you can write your own proof strategy: strategy ForNoam = Thens [Ors [Auto, Simp, User <simp add: field_simps>, User <simp add: devide_simps>, User <simp add: arith>, User <simp add: algebra>, User <simp add: ac_simps>, User <simp add: algebra_simps>, Hammer ], IsSolved ] and apply this strategy as follows: lemma "True (*just an example*)" find_proof ForNoam oops Essentially, this strategy keeps applying - auto, - simp, - simp add: field_simps, - simp add: devide_simps, - simp add: arith, - simp add: algebra, - simp add: algebra_simps, - sledgehammer until one of them discharges your proof obligation. If one of them discharges your proof obligation, PSL shows that proof method with the corresponding arguments in the output window. To use PSL, you have to download its source code form GitHub [2] and import "PSL.thy" using the "import" command as usual with the right path to "PSL.thy". It is just a theory file. So, installation should be easy. The drawback of this approach is that it can be pretty slow at finding a proof script. But if it finds a proof script, the proof script shown in the output window tends to be efficient. I attached a small example file (Scratch.thy). [1] documentation (Springer or arXiv): https://doi.org/10.1007/978-3-319-63046-5_32 https://arxiv.org/pdf/1606.02941.pdf [2] source code: https://github.com/data61/PSL/releases/tag/v0.1.1 Regards, Yutaka ________________________________________ From: cl-isabelle-users-bounces at lists.cam.ac.uk [cl-isabelle-users-bounces at lists.cam.ac.uk] on behalf of Lukas Bulwahn [lukas.bulwahn at gmail.com] Sent: Monday, 25 June 2018 4:31 PM To: noam neer Cc: isabelle-users Subject: Re: [isabelle] general commands for rewritting real expressions 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

**Attachment:
Scratch.thy**

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

**Re: [isabelle] general commands for rewritting real expressions***From:*Lukas Bulwahn

- Previous by Date: Re: [isabelle] make_string
- Next by Date: Re: [isabelle] HOL+ZF context
- Previous by Thread: Re: [isabelle] general commands for rewritting real expressions
- Next by Thread: [isabelle] new AFP entry: Pell's Equation
- 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