src/HOL/Isar_examples/Peirce.thy
author wenzelm
Fri Apr 16 17:44:29 1999 +0200 (1999-04-16)
changeset 6444 2ebe9e630cab
child 6493 3489490c948d
permissions -rw-r--r--
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm@6444
     1
(*  Title:      HOL/Isar_examples/Peirce.thy
wenzelm@6444
     2
    ID:         $Id$
wenzelm@6444
     3
    Author:     Markus Wenzel, TU Muenchen
wenzelm@6444
     4
wenzelm@6444
     5
Peirce's law: some examples of classical proof.
wenzelm@6444
     6
*)
wenzelm@6444
     7
wenzelm@6444
     8
theory Peirce = Main:;
wenzelm@6444
     9
wenzelm@6444
    10
lemmas it[elim!] = mp notE;	(* FIXME elim!! *)
wenzelm@6444
    11
wenzelm@6444
    12
wenzelm@6444
    13
lemma Peirce's_law: "((A --> B) --> A) --> A";
wenzelm@6444
    14
proof;
wenzelm@6444
    15
  assume ABA: "(A --> B) --> A";
wenzelm@6444
    16
  show A;
wenzelm@6444
    17
  proof (rule classical);
wenzelm@6444
    18
    assume notA: "~ A";
wenzelm@6444
    19
wenzelm@6444
    20
    have AB: "A --> B";
wenzelm@6444
    21
    proof;
wenzelm@6444
    22
      assume A: A;
wenzelm@6444
    23
      from notA A; show B; ..;
wenzelm@6444
    24
    qed;
wenzelm@6444
    25
wenzelm@6444
    26
    from ABA AB; show A; ..;
wenzelm@6444
    27
  qed;
wenzelm@6444
    28
qed;
wenzelm@6444
    29
wenzelm@6444
    30
wenzelm@6444
    31
lemma Peirce's_law: "((A --> B) --> A) --> A";
wenzelm@6444
    32
proof;
wenzelm@6444
    33
  assume ABA: "(A --> B) --> A";
wenzelm@6444
    34
  show A;
wenzelm@6444
    35
  proof (rule classical);
wenzelm@6444
    36
wenzelm@6444
    37
    assume AB: "A --> B";
wenzelm@6444
    38
    from ABA AB; show A; ..;
wenzelm@6444
    39
wenzelm@6444
    40
    next;
wenzelm@6444
    41
    assume notA: "~ A";
wenzelm@6444
    42
    show "A --> B";
wenzelm@6444
    43
    proof;
wenzelm@6444
    44
      assume A: A;
wenzelm@6444
    45
      from notA A; show B; ..;
wenzelm@6444
    46
    qed;
wenzelm@6444
    47
  qed;
wenzelm@6444
    48
qed;
wenzelm@6444
    49
wenzelm@6444
    50
wenzelm@6444
    51
end;