Re: [isabelle] general commands for rewritting real expressions



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.





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