src/HOL/Isar_examples/Drinker.thy
 author paulson Tue Jun 28 15:27:45 2005 +0200 (2005-06-28) changeset 16587 b34c8aa657a5 parent 16531 9b442d0e5c0c child 31758 3edd5f813f01 permissions -rw-r--r--
Constant "If" is now local
 wenzelm@16356 ` 1` ```(* Title: HOL/Isar_examples/Drinker.thy ``` wenzelm@16356 ` 2` ``` ID: \$Id\$ ``` wenzelm@16356 ` 3` ``` Author: Makarius ``` wenzelm@16356 ` 4` ```*) ``` wenzelm@16356 ` 5` wenzelm@16356 ` 6` ```header {* The Drinker's Principle *} ``` wenzelm@16356 ` 7` haftmann@16417 ` 8` ```theory Drinker imports Main begin ``` wenzelm@16356 ` 9` wenzelm@16356 ` 10` ```text {* ``` wenzelm@16531 ` 11` ``` Here is another example of classical reasoning: the Drinker's ``` wenzelm@16531 ` 12` ``` Principle says that for some person, if he is drunk, everybody else ``` wenzelm@16531 ` 13` ``` is drunk! ``` wenzelm@16531 ` 14` wenzelm@16531 ` 15` ``` We first prove a classical part of de-Morgan's law. ``` wenzelm@16356 ` 16` ```*} ``` wenzelm@16356 ` 17` wenzelm@16531 ` 18` ```lemma deMorgan: ``` wenzelm@16531 ` 19` ``` assumes "\ (\x. P x)" ``` wenzelm@16531 ` 20` ``` shows "\x. \ P x" ``` wenzelm@16531 ` 21` ``` using prems ``` wenzelm@16531 ` 22` ```proof (rule contrapos_np) ``` wenzelm@16531 ` 23` ``` assume a: "\ (\x. \ P x)" ``` wenzelm@16531 ` 24` ``` show "\x. P x" ``` wenzelm@16356 ` 25` ``` proof ``` wenzelm@16356 ` 26` ``` fix x ``` wenzelm@16356 ` 27` ``` show "P x" ``` wenzelm@16356 ` 28` ``` proof (rule classical) ``` wenzelm@16531 ` 29` ``` assume "\ P x" ``` wenzelm@16531 ` 30` ``` then have "\x. \ P x" .. ``` wenzelm@16531 ` 31` ``` with a show ?thesis by contradiction ``` wenzelm@16356 ` 32` ``` qed ``` wenzelm@16356 ` 33` ``` qed ``` wenzelm@16356 ` 34` ```qed ``` wenzelm@16356 ` 35` wenzelm@16356 ` 36` ```theorem Drinker's_Principle: "\x. drunk x \ (\x. drunk x)" ``` wenzelm@16356 ` 37` ```proof cases ``` wenzelm@16356 ` 38` ``` fix a assume "\x. drunk x" ``` wenzelm@16356 ` 39` ``` then have "drunk a \ (\x. drunk x)" .. ``` wenzelm@16356 ` 40` ``` then show ?thesis .. ``` wenzelm@16356 ` 41` ```next ``` wenzelm@16356 ` 42` ``` assume "\ (\x. drunk x)" ``` wenzelm@16531 ` 43` ``` then have "\x. \ drunk x" by (rule deMorgan) ``` wenzelm@16356 ` 44` ``` then obtain a where a: "\ drunk a" .. ``` wenzelm@16356 ` 45` ``` have "drunk a \ (\x. drunk x)" ``` wenzelm@16356 ` 46` ``` proof ``` wenzelm@16356 ` 47` ``` assume "drunk a" ``` wenzelm@16356 ` 48` ``` with a show "\x. drunk x" by (contradiction) ``` wenzelm@16356 ` 49` ``` qed ``` wenzelm@16356 ` 50` ``` then show ?thesis .. ``` wenzelm@16356 ` 51` ```qed ``` wenzelm@16356 ` 52` wenzelm@16356 ` 53` ```end ```