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 :
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
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:
fix c :: real
fix d :: real
assume *: "c > 0"
assume **: "d > 0"
have "c * d > 0" sorry
Now you can proceed as suggested before ...
Invoking Sledgehammer (with command "sledgehammer") immediately gives a
by (metis ax1 ax2 real_mult_order)
which can then be rewritten:
by (simp add: real_mult_order[OF ax1 ax2])
by (rule real_mult_order[OF ax1 ax2])
This archive was generated by a fusion of
Pipermail (Mailman edition) and