src/HOL/Isar_Examples/Drinker.thy
 changeset 33026 8f35633c4922 parent 31758 3edd5f813f01 child 37671 fa53d267dab3
```     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/HOL/Isar_Examples/Drinker.thy	Tue Oct 20 19:37:09 2009 +0200
1.3 @@ -0,0 +1,54 @@
1.4 +(*  Title:      HOL/Isar_Examples/Drinker.thy
1.5 +    Author:     Makarius
1.6 +*)
1.7 +
1.8 +header {* The Drinker's Principle *}
1.9 +
1.10 +theory Drinker
1.11 +imports Main
1.12 +begin
1.13 +
1.14 +text {*
1.15 +  Here is another example of classical reasoning: the Drinker's
1.16 +  Principle says that for some person, if he is drunk, everybody else
1.17 +  is drunk!
1.18 +
1.19 +  We first prove a classical part of de-Morgan's law.
1.20 +*}
1.21 +
1.22 +lemma deMorgan:
1.23 +  assumes "\<not> (\<forall>x. P x)"
1.24 +  shows "\<exists>x. \<not> P x"
1.25 +  using prems
1.26 +proof (rule contrapos_np)
1.27 +  assume a: "\<not> (\<exists>x. \<not> P x)"
1.28 +  show "\<forall>x. P x"
1.29 +  proof
1.30 +    fix x
1.31 +    show "P x"
1.32 +    proof (rule classical)
1.33 +      assume "\<not> P x"
1.34 +      then have "\<exists>x. \<not> P x" ..
1.35 +      with a show ?thesis by contradiction
1.36 +    qed
1.37 +  qed
1.38 +qed
1.39 +
1.40 +theorem Drinker's_Principle: "\<exists>x. drunk x \<longrightarrow> (\<forall>x. drunk x)"
1.41 +proof cases
1.42 +  fix a assume "\<forall>x. drunk x"
1.43 +  then have "drunk a \<longrightarrow> (\<forall>x. drunk x)" ..
1.44 +  then show ?thesis ..
1.45 +next
1.46 +  assume "\<not> (\<forall>x. drunk x)"
1.47 +  then have "\<exists>x. \<not> drunk x" by (rule deMorgan)
1.48 +  then obtain a where a: "\<not> drunk a" ..
1.49 +  have "drunk a \<longrightarrow> (\<forall>x. drunk x)"
1.50 +  proof
1.51 +    assume "drunk a"
1.52 +    with a show "\<forall>x. drunk x" by (contradiction)
1.53 +  qed
1.54 +  then show ?thesis ..
1.55 +qed
1.56 +
1.57 +end
```