*To*: isabelle-users at cl.cam.ac.uk*Subject*: Re: [isabelle] Isar Proof*From*: "Dr. Brendan Patrick Mahony" <brendan.mahony at dsto.defence.gov.au>*Date*: Wed, 18 Jun 2008 17:16:01 +0930*Cc*: TIMOTHY KREMANN <twksoa262 at verizon.net>*In-reply-to*: <219881.17858.qm@web84005.mail.mud.yahoo.com>*References*: <219881.17858.qm@web84005.mail.mud.yahoo.com>

On 18/06/2008, at 8:11 AM, TIMOTHY KREMANN wrote: > 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 > 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 at 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.

**Follow-Ups**:**Re: [isabelle] Isar Proof***From:*Simon Winwood

**References**:**[isabelle] Isar Proof***From:*TIMOTHY KREMANN

- Previous by Date: [isabelle] Formal Methods in Use at Galois, an IJCAR Tutorial: Call for Participation
- Next by Date: Re: [isabelle] Isar Proof
- Previous by Thread: [isabelle] Isar Proof
- Next by Thread: Re: [isabelle] Isar Proof
- Cl-isabelle-users June 2008 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list