|
33026
|
1 |
(* Title: HOL/Isar_Examples/Drinker.thy
|
|
16356
|
2 |
Author: Makarius
|
|
|
3 |
*)
|
|
|
4 |
|
|
58882
|
5 |
section \<open>The Drinker's Principle\<close>
|
|
16356
|
6 |
|
|
31758
|
7 |
theory Drinker
|
|
|
8 |
imports Main
|
|
|
9 |
begin
|
|
16356
|
10 |
|
|
58614
|
11 |
text \<open>Here is another example of classical reasoning: the Drinker's
|
|
16531
|
12 |
Principle says that for some person, if he is drunk, everybody else
|
|
|
13 |
is drunk!
|
|
|
14 |
|
|
58614
|
15 |
We first prove a classical part of de-Morgan's law.\<close>
|
|
16356
|
16 |
|
|
37671
|
17 |
lemma de_Morgan:
|
|
16531
|
18 |
assumes "\<not> (\<forall>x. P x)"
|
|
|
19 |
shows "\<exists>x. \<not> P x"
|
|
47960
|
20 |
proof (rule classical)
|
|
|
21 |
assume "\<not> (\<exists>x. \<not> P x)"
|
|
|
22 |
have "\<forall>x. P x"
|
|
16356
|
23 |
proof
|
|
37671
|
24 |
fix x show "P x"
|
|
16356
|
25 |
proof (rule classical)
|
|
16531
|
26 |
assume "\<not> P x"
|
|
|
27 |
then have "\<exists>x. \<not> P x" ..
|
|
58614
|
28 |
with \<open>\<not> (\<exists>x. \<not> P x)\<close> show ?thesis by contradiction
|
|
16356
|
29 |
qed
|
|
|
30 |
qed
|
|
58614
|
31 |
with \<open>\<not> (\<forall>x. P x)\<close> show ?thesis by contradiction
|
|
16356
|
32 |
qed
|
|
|
33 |
|
|
|
34 |
theorem Drinker's_Principle: "\<exists>x. drunk x \<longrightarrow> (\<forall>x. drunk x)"
|
|
|
35 |
proof cases
|
|
|
36 |
fix a assume "\<forall>x. drunk x"
|
|
|
37 |
then have "drunk a \<longrightarrow> (\<forall>x. drunk x)" ..
|
|
|
38 |
then show ?thesis ..
|
|
|
39 |
next
|
|
|
40 |
assume "\<not> (\<forall>x. drunk x)"
|
|
37671
|
41 |
then have "\<exists>x. \<not> drunk x" by (rule de_Morgan)
|
|
16356
|
42 |
then obtain a where a: "\<not> drunk a" ..
|
|
|
43 |
have "drunk a \<longrightarrow> (\<forall>x. drunk x)"
|
|
|
44 |
proof
|
|
|
45 |
assume "drunk a"
|
|
37671
|
46 |
with a show "\<forall>x. drunk x" by contradiction
|
|
16356
|
47 |
qed
|
|
|
48 |
then show ?thesis ..
|
|
|
49 |
qed
|
|
|
50 |
|
|
|
51 |
end
|