src/HOL/Isar_examples/Peirce.thy
author wenzelm
Fri, 16 Apr 1999 17:44:29 +0200
changeset 6444 2ebe9e630cab
child 6493 3489490c948d
permissions -rw-r--r--
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.

(*  Title:      HOL/Isar_examples/Peirce.thy
    ID:         $Id$
    Author:     Markus Wenzel, TU Muenchen

Peirce's law: some examples of classical proof.
*)

theory Peirce = Main:;

lemmas it[elim!] = mp notE;	(* FIXME elim!! *)


lemma Peirce's_law: "((A --> B) --> A) --> A";
proof;
  assume ABA: "(A --> B) --> A";
  show A;
  proof (rule classical);
    assume notA: "~ A";

    have AB: "A --> B";
    proof;
      assume A: A;
      from notA A; show B; ..;
    qed;

    from ABA AB; show A; ..;
  qed;
qed;


lemma Peirce's_law: "((A --> B) --> A) --> A";
proof;
  assume ABA: "(A --> B) --> A";
  show A;
  proof (rule classical);

    assume AB: "A --> B";
    from ABA AB; show A; ..;

    next;
    assume notA: "~ A";
    show "A --> B";
    proof;
      assume A: A;
      from notA A; show B; ..;
    qed;
  qed;
qed;


end;