equal
deleted
inserted
replaced
1 (* Title: HOL/Isar_Examples/Drinker.thy |
|
2 Author: Makarius |
|
3 *) |
|
4 |
|
5 section \<open>The Drinker's Principle\<close> |
|
6 |
|
7 theory Drinker |
|
8 imports Main |
|
9 begin |
|
10 |
|
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! |
|
14 |
|
15 We first prove a classical part of de-Morgan's law. |
|
16 \<close> |
|
17 |
|
18 lemma de_Morgan: |
|
19 assumes "\<not> (\<forall>x. P x)" |
|
20 shows "\<exists>x. \<not> P x" |
|
21 proof (rule classical) |
|
22 assume "\<nexists>x. \<not> P x" |
|
23 have "\<forall>x. P x" |
|
24 proof |
|
25 fix x show "P x" |
|
26 proof (rule classical) |
|
27 assume "\<not> P x" |
|
28 then have "\<exists>x. \<not> P x" .. |
|
29 with \<open>\<nexists>x. \<not> P x\<close> show ?thesis by contradiction |
|
30 qed |
|
31 qed |
|
32 with \<open>\<not> (\<forall>x. P x)\<close> show ?thesis by contradiction |
|
33 qed |
|
34 |
|
35 theorem Drinker's_Principle: "\<exists>x. drunk x \<longrightarrow> (\<forall>x. drunk x)" |
|
36 proof cases |
|
37 assume "\<forall>x. drunk x" |
|
38 then have "drunk a \<longrightarrow> (\<forall>x. drunk x)" for a .. |
|
39 then show ?thesis .. |
|
40 next |
|
41 assume "\<not> (\<forall>x. drunk x)" |
|
42 then have "\<exists>x. \<not> drunk x" by (rule de_Morgan) |
|
43 then obtain a where "\<not> drunk a" .. |
|
44 have "drunk a \<longrightarrow> (\<forall>x. drunk x)" |
|
45 proof |
|
46 assume "drunk a" |
|
47 with \<open>\<not> drunk a\<close> show "\<forall>x. drunk x" by contradiction |
|
48 qed |
|
49 then show ?thesis .. |
|
50 qed |
|
51 |
|
52 end |
|