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 ?;
     1 (*  Title:      HOL/Isar_examples/Peirce.thy
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Muenchen
     4 *)
     5 
     6 theory Peirce = Main:;
     7 
     8 text {* Peirce's law: examples of classical proof. *};
     9 
    10 theorem "((A --> B) --> A) --> A";
    11 proof;
    12   assume aba: "(A --> B) --> A";
    13   show A;
    14   proof (rule classical);
    15     assume "~ A";
    16     have "A --> B";
    17     proof;
    18       assume A;
    19       thus B; by contradiction;
    20     qed;
    21     with aba; show A; ..;
    22   qed;
    23 qed;
    24 
    25 
    26 theorem "((A --> B) --> A) --> A";
    27 proof;
    28   assume aba: "(A --> B) --> A";
    29   show A;
    30   proof (rule classical);
    31     presume "A --> B";
    32     with aba; show A; ..;
    33   next;
    34     assume not_a: "~ A";
    35     show "A --> B";
    36     proof;
    37       assume A;
    38       with not_a; show B; ..;
    39     qed;
    40   qed;
    41 qed;
    42 
    43 
    44 end;