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