Email Gateway (Aug 18 2022 at 18:03): Email Gateway (Aug 18 2022 at 18:03):From: Victor Porton <porton@narod.ru>
The following self-contradictory theory (Two definitions contradict to each other.) verifies by Isabelle 2011. Where is the error?!
theory test
imports HOL Main
begin
typedecl tag
consts t1::tag
consts t2::tag
definition "f (t1, x) = t1"
definition "f (t1, x) = t2"
end
Email Gateway (Aug 18 2022 at 18:03):From: Tjark Weber <webertj@in.tum.de>
Victor,
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,
Tjark
Email Gateway (Aug 18 2022 at 18:04):From: Victor Porton <porton@narod.ru>
Oh, sorry, after restart of Emacs it does not verify. It is a bug in ProofGeneral.
Email Gateway (Aug 18 2022 at 18:04):From: Victor Porton <porton@narod.ru>
Oh, sorry, after restart of Emacs it does not verify. It is a bug in ProofGeneral.
Email Gateway (Aug 18 2022 at 18:04):From: David Aspinall <David.Aspinall@ed.ac.uk>
Oh, sorry, after restart of Emacs it does not verify. It is a bug in ProofGeneral.
If that's true, please report a repeatable test case at
http://proofgeneral.inf.ed.ac.uk/trac
Thanks, - David.
Last updated: Apr 26 2024 at 12:28 UTC