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




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