src/HOL/Isar_examples/Peirce.thy
author wenzelm
Sat Sep 04 21:13:01 1999 +0200 (1999-09-04)
changeset 7480 0a0e0dbe1269
parent 7448 3ee96dccdd39
child 7740 2fbe5ce9845f
permissions -rw-r--r--
replaced ?? by ?;
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
wenzelm@6444
     6
theory Peirce = Main:;
wenzelm@6444
     7
wenzelm@6746
     8
text {* Peirce's law: examples of classical proof. *};
wenzelm@6444
     9
wenzelm@6493
    10
theorem "((A --> B) --> A) --> A";
wenzelm@6444
    11
proof;
wenzelm@6892
    12
  assume aba: "(A --> B) --> A";
wenzelm@6444
    13
  show A;
wenzelm@6444
    14
  proof (rule classical);
wenzelm@7448
    15
    assume "~ A";
wenzelm@7448
    16
    have "A --> B";
wenzelm@6444
    17
    proof;
wenzelm@7448
    18
      assume A;
wenzelm@7448
    19
      thus B; by contradiction;
wenzelm@6444
    20
    qed;
wenzelm@7448
    21
    with aba; show A; ..;
wenzelm@6444
    22
  qed;
wenzelm@6444
    23
qed;
wenzelm@6444
    24
wenzelm@6444
    25
wenzelm@6493
    26
theorem "((A --> B) --> A) --> A";
wenzelm@6444
    27
proof;
wenzelm@6892
    28
  assume aba: "(A --> B) --> A";
wenzelm@6444
    29
  show A;
wenzelm@6444
    30
  proof (rule classical);
wenzelm@7448
    31
    presume "A --> B";
wenzelm@7448
    32
    with aba; show A; ..;
wenzelm@6854
    33
  next;
wenzelm@6892
    34
    assume not_a: "~ A";
wenzelm@6444
    35
    show "A --> B";
wenzelm@6444
    36
    proof;
wenzelm@7448
    37
      assume A;
wenzelm@7448
    38
      with not_a; show B; ..;
wenzelm@6444
    39
    qed;
wenzelm@6444
    40
  qed;
wenzelm@6444
    41
qed;
wenzelm@6444
    42
wenzelm@6444
    43
wenzelm@6444
    44
end;