Email Gateway (Aug 18 2022 at 09:29): Email Gateway (Aug 18 2022 at 09:29):From: Francisco Jose Chaves Alonso <francisco.jose.chaves.alonso@ens-lyon.fr>
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@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
Email Gateway (Aug 18 2022 at 09:30):From: Amine Chaieb <chaieb@informatik.tu-muenchen.de>
Hi,
Strange. When i write
thm mult_mono
I get the theorem (So Isabelle finds it in the Database)
and
apply (rule mult_mono)
returns
goal (lemma, 4 subgoals):
NB: I don't have the defs of Lb and Ub...
Which Version are you using?
Where can I find the theorems for prove
inequalities of reals?
Generally Ring_and_Fields.thy is the right place to look in. What i often
Do is also to use the theorem search facility, see Section 5.14 of the
Tutorial (http://isabelle.in.tum.de/dist/Isabelle/doc/tutorial.pdf).
Hope it helps.
Amine.
Email Gateway (Aug 18 2022 at 09:30):From: Francisco Jose Chaves Alonso <francisco.jose.chaves.alonso@ens-lyon.fr>
Thanks Amine
I was using the 2003 version.
Francisco
-- Francisco José Cháves (ENS-LIP)
mailto: Francisco.Jose.Chaves.Alonso@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
Last updated: May 03 2024 at 04:19 UTC