Email Gateway (Aug 18 2022 at 12:03): Email Gateway (Aug 18 2022 at 12:03):From: TIMOTHY KREMANN <twksoa262@verizon.net>
lemma
"[| ALL x . (P (x::'a) => ~ Q x) /\
(P x => ~ R x) /\
(Q x => ~ R x);
EX x . P x;
EX x . Q x;
EX x . R x|] ==>
EX x y z. (~((x::'a) = y) /\
~( x = z) /\
~( y = z))"
apply(elim ex_forward)
apply(auto)
done
Can someone suggest an Isar equivalent for the above proof?
Thanks,
Tim
Email Gateway (Aug 18 2022 at 12:04):From: "Dr. Brendan Patrick Mahony" <brendan.mahony@dsto.defence.gov.au>
Perhaps something like:
lemma
assumes
a1: "\<forall> x. (P (x::'a) \<longrightarrow> \<not> Q x) \<and>
(P x \<longrightarrow> \<not> R x) \<and> (Q x \<longrightarrow>
\<not> R x)" and
a2: "\<exists> x. P x" and
a3: "\<exists> x. Q x" and
a4: "\<exists> x. R x"
shows
"\<exists> x y z. (((x::'a) \<noteq> y) \<and> (x \<noteq> z)
\<and> (y \<noteq> z))"
proof -
from a2 obtain a where b1: "P a"
by (auto)
from a3 obtain b where b2: "Q b"
by (auto)
from a4 obtain c where b3: "R c"
by (auto)
from a1 b1 b2 have "a \<noteq> b"
by (auto)
moreover
from a1 b1 b3 have "a \<noteq> c"
by (auto)
moreover
from a1 b2 b3 have "b \<noteq> c"
by (auto)
ultimately
show ?thesis
by (auto)
qed
Dr Brendan Mahony
C3I Division ph +61 8 8259 6046
Defence Science and Technology Organisation fx +61 8 8259 5589
Edinburgh, South Australia Brendan.Mahony@dsto.defence.gov.au
Important: This document remains the property of the Australian
Government Department of Defence and is subject to the jurisdiction
of the Crimes Act section 70. If you have received this document in
error, you are requested to contact the sender and delete the document.
IMPORTANT: This email remains the property of the Australian Defence Organisation and is subject to the jurisdiction of section 70 of the CRIMES ACT 1914. If you have received this email in error, you are requested to contact the sender and delete the email.
Email Gateway (Aug 18 2022 at 12:04):From: Tobias Nipkow <nipkow@in.tum.de>
I know this is not what you asked. But this goal can also be solved
automatically by the recent tactic "metis"
apply (metis)
although not by the older tactics blast and fast. The drawback of metis
is that you have to give it explicitly any additional lemmas beyond pure
logic that are needed. Here there are none.
Tobias
TIMOTHY KREMANN wrote:
Email Gateway (Aug 18 2022 at 12:04):From: Simon Winwood <sjw@cse.unsw.edu.au>
Or else using guess (with a good dose of auto :) ...
lemma
assumes all: "ALL x . (P (x::'a) \<longrightarrow> \<not> Q x) \<and> (P x \<longrightarrow> \<not> R x) \<and> (Q x \<longrightarrow> \<not> R x)"
and eP: "EX x . P x" and eQ: "EX x . Q x" and eR: "EX x . R x"
shows "EX x y z. (\<not>((x::'a) = y) \<and> \<not>( x = z) \<and> \<not>( y = z))"
proof -
from eP guess x ..
moreover from eQ guess y ..
moreover from eR guess z ..
ultimately have "x \<noteq> y" and "x \<noteq> z" and "y \<noteq> z" using all by auto
thus ?thesis by auto
qed
Simon
At Wed, 18 Jun 2008 17:16:01 +0930,
"Dr. Brendan Patrick Mahony" <brendan.mahony@dsto.defence.gov.au> wrote:
Last updated: May 03 2024 at 08:18 UTC