[isabelle] general commands for rewritting real expressions



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.