Re: [isabelle] Surprisingly this verifies


On Sat, 2011-07-09 at 18:06 +0400, Victor Porton wrote:
> The following self-contradictory theory (Two definitions contradict to
> each other.) verifies by Isabelle 2011. Where is the error?!

Strange -- I get the following error message:

*** Bad arguments on lhs: "(t1, x)"
*** The error(s) above occurred in definition:
*** "f (t1, x) \<equiv> t1"
*** At command "definition"

Two more remarks:

> theory test
>   imports HOL Main

There is no need to import HOL.  In fact, you shouldn't.  Simply
importing Main will be sufficient.

> definition "f (t1, x) = t1"
> definition "f (t1, x) = t2"

These definitions are not contradictory; they merely imply t1 = t2.

Kind regards,

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