# HG changeset patch
# User wenzelm
# Date 1118352808 -7200
# Node ID 94011cf701a4dc3f346a28db675716e61c54c785
# Parent  06059ee940b6119e4a2a6b05755d5409368335c5
added Isar_examples/Drinker.thy;

diff -r 06059ee940b6 -r 94011cf701a4 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Thu Jun 09 16:58:03 2005 +0200
+++ b/src/HOL/IsaMakefile	Thu Jun 09 23:33:28 2005 +0200
@@ -593,7 +593,7 @@
 HOL-Isar_examples: HOL $(LOG)/HOL-Isar_examples.gz
 
 $(LOG)/HOL-Isar_examples.gz: $(OUT)/HOL Isar_examples/BasicLogic.thy \
-  Isar_examples/Cantor.ML Isar_examples/Cantor.thy \
+  Isar_examples/Cantor.ML Isar_examples/Cantor.thy Isar_examples/Drinker.thy \
   Isar_examples/ExprCompiler.thy Isar_examples/Fibonacci.thy \
   Isar_examples/Group.thy Isar_examples/Hoare.thy Isar_examples/HoareEx.thy \
   Isar_examples/KnasterTarski.thy Isar_examples/MutilatedCheckerboard.thy \
diff -r 06059ee940b6 -r 94011cf701a4 src/HOL/Isar_examples/Drinker.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Isar_examples/Drinker.thy	Thu Jun 09 23:33:28 2005 +0200
@@ -0,0 +1,70 @@
+(*  Title:      HOL/Isar_examples/Drinker.thy
+    ID:         $Id$
+    Author:     Makarius
+*)
+
+header {* The Drinker's Principle *}
+
+theory Drinker = Main:
+
+text {*
+ Two parts of de-Morgan's law -- one intuitionistic and one classical:
+*}
+
+lemma deMorgan1: "\<not> (\<exists>x. P x) \<Longrightarrow> \<forall>x. \<not> P x"
+proof -
+  assume a: "\<not> (\<exists>x. P x)"
+  show ?thesis
+  proof
+    fix x
+    show "\<not> P x"
+    proof
+      assume "P x"
+      then have "\<exists>x. P x" ..
+      with a show False by contradiction
+    qed
+  qed
+qed
+
+lemma deMorgan2: "\<not> (\<forall>x. P x) \<Longrightarrow> \<exists>x. \<not> P x"
+proof (rule classical)
+  assume a: "\<not> (\<forall>x. P x)"
+  assume b: "\<not> (\<exists>x. \<not> P x)"
+  have "\<forall>x. P x"
+  proof
+    fix x
+    show "P x"
+    proof (rule classical)
+      assume c: "\<not> P x"
+      from b have "\<forall>x. \<not> \<not> P x" by (rule deMorgan1)
+      then have "\<not> \<not> P x" ..
+      with c show ?thesis by contradiction
+    qed
+  qed
+  with a show ?thesis by contradiction
+qed
+
+text {*
+ Here is another example of classical reasoning: the Drinker's
+ Principle says that for some person, if he is drunk, everybody else
+ is drunk!
+*}
+
+theorem Drinker's_Principle: "\<exists>x. drunk x \<longrightarrow> (\<forall>x. drunk x)"
+proof cases
+  fix a assume "\<forall>x. drunk x"
+  then have "drunk a \<longrightarrow> (\<forall>x. drunk x)" ..
+  then show ?thesis ..
+next
+  assume "\<not> (\<forall>x. drunk x)"
+  then have "\<exists>x. \<not> drunk x" by (rule deMorgan2)
+  then obtain a where a: "\<not> drunk a" ..
+  have "drunk a \<longrightarrow> (\<forall>x. drunk x)"
+  proof
+    assume "drunk a"
+    with a show "\<forall>x. drunk x" by (contradiction)
+  qed
+  then show ?thesis ..
+qed
+
+end
diff -r 06059ee940b6 -r 94011cf701a4 src/HOL/Isar_examples/ROOT.ML
--- a/src/HOL/Isar_examples/ROOT.ML	Thu Jun 09 16:58:03 2005 +0200
+++ b/src/HOL/Isar_examples/ROOT.ML	Thu Jun 09 23:33:28 2005 +0200
@@ -8,6 +8,7 @@
 time_use_thy "BasicLogic";
 time_use_thy "Cantor";
 time_use_thy "Peirce";
+time_use_thy "Drinker";
 time_use_thy "ExprCompiler";
 time_use_thy "Group";
 time_use_thy "Summation";