Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] unknow theorem

view this post on Zulip 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

view this post on Zulip 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):

  1. 0 Lb X; 0 Lb Y; Lb X x; x Ub X; Lb Y y; y Ub Y d Lb X x
  2. 0 Lb X; 0 Lb Y; Lb X x; x Ub X; Lb Y y; y Ub Y d Lb Y y
  3. 0 Lb X; 0 Lb Y; Lb X x; x Ub X; Lb Y y; y Ub Y d 0 x
  4. 0 Lb X; 0 Lb Y; Lb X x; x Ub X; Lb Y y; y Ub Y d 0 Lb Y

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.

view this post on Zulip 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: Nov 21 2024 at 12:39 UTC