Email Gateway (Aug 18 2022 at 18:23): Email Gateway (Aug 18 2022 at 18:23):From: John Munroe <munddr@gmail.com>
Hi all,
Given
axiomatization
c :: real and
d :: real
where ax1 : "c > 0"
and ax2 : "d > 0"
does anyone know how to prove
lemma "c * d > 0"?
It seems using the facts ax1 ax2 isn't sufficient.
Thanks in Advance.
John
Email Gateway (Aug 18 2022 at 18:23):From: Mathieu Giorgino <mathieu.giorgino@irit.fr>
Le Mardi 20 Septembre 2011 10:12:10 John Munroe a écrit :
Hello John,
Invoking Sledgehammer (with command "sledgehammer") immediately gives a
solution:
by (metis ax1 ax2 real_mult_order)
which can then be rewritten:
by (simp add: real_mult_order[OF ax1 ax2])
or even:
by (rule real_mult_order[OF ax1 ax2])
Email Gateway (Aug 18 2022 at 18:24):From: Mathieu Giorgino <mathieu.giorgino@irit.fr>
Le Mardi 20 Septembre 2011 10:12:10 John Munroe a écrit :
Hello John,
Invoking Sledgehammer (with command "sledgehammer") immediately gives a
solution:
by (metis ax1 ax2 real_mult_order)
which can then be rewritten:
by (simp add: real_mult_order[OF ax1 ax2])
or even:
by (rule real_mult_order[OF ax1 ax2])
Email Gateway (Aug 18 2022 at 18:24):From: John Munroe <munddr@gmail.com>
Oh, I almost forgot about sledgehammer. Thanks!
On Tuesday, September 20, 2011, Mathieu Giorgino <mathieu.giorgino@irit.fr>
wrote:
Le Mardi 20 Septembre 2011 10:12:10 John Munroe a écrit :
Hi all,
>
Given
>
>
axiomatization
c :: real and
d :: real
where ax1 : "c > 0"
and ax2 : "d > 0"
>
does anyone know how to prove
>
lemma "c * d > 0"?
>
It seems using the facts ax1 ax2 isn't sufficient.
>
Thanks in Advance.
>
John
Hello John,
Invoking Sledgehammer (with command "sledgehammer") immediately gives a
solution:by (metis ax1 ax2 real_mult_order)
which can then be rewritten:
by (simp add: real_mult_order[OF ax1 ax2])
or even:
by (rule real_mult_order[OF ax1 ax2])
- Mathieu
Email Gateway (Aug 18 2022 at 18:24):From: Makarius <makarius@sketis.net>
On Tue, 20 Sep 2011, Mathieu Giorgino wrote:
Le Mardi 20 Septembre 2011 10:12:10 John Munroe a écrit :
Hi all,
Given
axiomatization
c :: real and
d :: real
where ax1 : "c > 0"
and ax2 : "d > 0"does anyone know how to prove
lemma "c * d > 0"?
It seems using the facts ax1 ax2 isn't sufficient.
Just a stylistic note: raw axiomatizations affect the foundation of the
logic, and can easily produce global inconsistency, where eveything breaks
down.
In Isabelle/Isar local experimentation can be done within a proof context.
Since Isabelle2011 there is also a stand-alone command for that:
'notepad'. Here is the example in that style:
notepad
begin
fix c :: real
fix d :: real
assume *: "c > 0"
assume **: "d > 0"
have "c * d > 0" sorry
end
Now you can proceed as suggested before ...
Invoking Sledgehammer (with command "sledgehammer") immediately gives a
solution:
by (metis ax1 ax2 real_mult_order)which can then be rewritten:
by (simp add: real_mult_order[OF ax1 ax2])or even:
by (rule real_mult_order[OF ax1 ax2])
Makarius
Last updated: Apr 24 2024 at 20:16 UTC