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.