src/HOL/Isar_Examples/Drinker.thy
 author hoelzl Tue Mar 26 12:20:58 2013 +0100 (2013-03-26) changeset 51526 155263089e7b parent 49930 defce6616890 child 58614 7338eb25226c permissions -rw-r--r--
move SEQ.thy and Lim.thy to Limits.thy
 wenzelm@33026 1 (* Title: HOL/Isar_Examples/Drinker.thy wenzelm@16356 2 Author: Makarius wenzelm@16356 3 *) wenzelm@16356 4 wenzelm@16356 5 header {* The Drinker's Principle *} wenzelm@16356 6 wenzelm@31758 7 theory Drinker wenzelm@31758 8 imports Main wenzelm@31758 9 begin wenzelm@16356 10 wenzelm@37671 11 text {* 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@37671 15 We first prove a classical part of de-Morgan's law. *} wenzelm@16356 16 wenzelm@37671 17 lemma de_Morgan: wenzelm@16531 18 assumes "\ (\x. P x)" wenzelm@16531 19 shows "\x. \ P x" wenzelm@47960 20 proof (rule classical) wenzelm@47960 21 assume "\ (\x. \ P x)" wenzelm@47960 22 have "\x. P x" wenzelm@16356 23 proof wenzelm@37671 24 fix x show "P x" wenzelm@16356 25 proof (rule classical) wenzelm@16531 26 assume "\ P x" wenzelm@16531 27 then have "\x. \ P x" .. wenzelm@47960 28 with `\ (\x. \ P x)` show ?thesis by contradiction wenzelm@16356 29 qed wenzelm@16356 30 qed wenzelm@49930 31 with `\ (\x. P x)` show ?thesis by contradiction wenzelm@16356 32 qed wenzelm@16356 33 wenzelm@16356 34 theorem Drinker's_Principle: "\x. drunk x \ (\x. drunk x)" wenzelm@16356 35 proof cases wenzelm@16356 36 fix a assume "\x. drunk x" wenzelm@16356 37 then have "drunk a \ (\x. drunk x)" .. wenzelm@16356 38 then show ?thesis .. wenzelm@16356 39 next wenzelm@16356 40 assume "\ (\x. drunk x)" wenzelm@37671 41 then have "\x. \ drunk x" by (rule de_Morgan) wenzelm@16356 42 then obtain a where a: "\ drunk a" .. wenzelm@16356 43 have "drunk a \ (\x. drunk x)" wenzelm@16356 44 proof wenzelm@16356 45 assume "drunk a" wenzelm@37671 46 with a show "\x. drunk x" by contradiction wenzelm@16356 47 qed wenzelm@16356 48 then show ?thesis .. wenzelm@16356 49 qed wenzelm@16356 50 wenzelm@16356 51 end