Re: [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
Description: Scratch.thy



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