[isabelle] unknow theorem



Hello

I am using the HOL-Complex logic and I want to prove

[| 0 <= Lb X; 0 <= Lb Y; Lb X <= x; x <= Ub X; Lb Y <= y; y <= Ub Y |]
    ==> Lb X * Lb Y <= x * y

where all terms are of type real.

I find the lemma "mult_mono" in the Ring_and_Field theory of HOL logic,
(at http://www.cl.cam.ac.uk/~lp15/Isabelle/dist/library/HOL/Ring_and_Field.html)
but when I tried to use it, isabelle answers:

*** Error in method "HOL.rule":
*** Unknown theorem(s) "mult_mono"
*** At command "apply".

How can I do for use that theorem? Where can I find the theorems for prove
inequalities of reals?

Thanks

Francisco
-- Francisco José Cháves (ENS-LIP)
mailto: Francisco.Jose.Chaves.Alonso at ens-lyon.fr
http://perso.ens-lyon.fr/francisco.jose.chaves.alonso
ENS de Lyon - 46, allee d'Italie - 69364 Lyon Cedex 07 - FRANCE
Phone: (+33) 4 72 72 84 36






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