# Theory Drinker

```(*  Title:      HOL/Examples/Drinker.thy
Author:     Makarius
*)

section ‹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
assume "∀x. drunk x"
then have "drunk a ⟶ (∀x. drunk x)" for a ..
then show ?thesis ..
next
assume "¬ (∀x. drunk x)"
then have "∃x. ¬ drunk x" by (rule de_Morgan)
then obtain a where "¬ drunk a" ..
have "drunk a ⟶ (∀x. drunk x)"
proof
assume "drunk a"
with ‹¬ drunk a› show "∀x. drunk x" by contradiction
qed
then show ?thesis ..
qed

end
```