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