[isabelle] Nonlinear arithmetic for real numbers


I am having difficulty proving the following:

lemma "(1::real) * (1::real) = (1::real)"; 

lemma "(1::real) / (1::real) = (1::real)";

The "arith" tactic does not support multiplication, as
explained in previous messages.  What is the recommended
approach to reasoning about multiplication of reals?  I've
just begun to incorporate the theory of real numbers into my
work, so explicit proof steps would be especially helpful.  

Thank you,

Justin S. Davis
Formal Methods Group @ UIUC

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