Re: [isabelle] Proving equivalence



Hi Steve,

As Tjark pointed out recently, axioms are evil. It just so happens
that both of your example axiomatizations are inconsistent. As you can
see:

lemma "(0::real) = 1"
using ax1 by metis

(The same proof works also for ax2.)

This might explain why metis can easily solve your lemma: because from
ax1 or ax2 metis can prove any equation between real numbers!

- Brian

On Tue, Jan 25, 2011 at 9:18 AM, Tjark Weber <webertj at in.tum.de> wrote:
> Steve,
>
> On Tue, 2011-01-25 at 16:51 +0000, Steve W wrote:
>> Auto can't find a proof. How come this is so difficult for auto? What
>> is the proper way to do this proof?
>
> both "by blast" and "by metis" succeed.  I didn't investigate why auto
> fails.
>
> Kind regards,
> Tjark
>
>
>





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