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