src/HOL/Isar_examples/Drinker.thy

added Isar_examples/Drinker.thy;

(*  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