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;
```