header {* The Drinker's Principle *}

theory Drinker

imports Main

begin

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!

We first prove a classical part of de-Morgan's law. *}

lemma de_Morgan:

assumes "¬ (∀x. P x)"

shows "∃x. ¬ P x"

proof (rule classical)

assume "¬ (∃x. ¬ P x)"

have "∀x. P x"

proof

fix x show "P x"

proof (rule classical)

assume "¬ P x"

then have "∃x. ¬ P x" ..

with `¬ (∃x. ¬ P x)` show ?thesis by contradiction

qed

qed

with `¬ (∀x. P x)` show ?thesis by contradiction

qed

theorem Drinker's_Principle: "∃x. drunk x --> (∀x. drunk x)"

proof cases

fix a assume "∀x. drunk x"

then have "drunk a --> (∀x. drunk x)" ..

then show ?thesis ..

next

assume "¬ (∀x. drunk x)"

then have "∃x. ¬ drunk x" by (rule de_Morgan)

then obtain a where a: "¬ drunk a" ..

have "drunk a --> (∀x. drunk x)"

proof

assume "drunk a"

with a show "∀x. drunk x" by contradiction

qed

then show ?thesis ..

qed

end