# Re: [isabelle] A simple theorem

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

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