[isabelle] unknow theorem
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,
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?
-- Francisco José Cháves (ENS-LIP)
mailto: Francisco.Jose.Chaves.Alonso at ens-lyon.fr
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