Re: [isabelle] A simple theorem



Oh, I almost forgot about sledgehammer. Thanks!

On Tuesday, September 20, 2011, Mathieu Giorgino <mathieu.giorgino at 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




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