Re: [isabelle] A simple theorem



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




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