equal
deleted
inserted
replaced
1 (* Title: HOL/Isar_Examples/Drinker.thy |
1 (* Title: HOL/Isar_Examples/Drinker.thy |
2 Author: Makarius |
2 Author: Makarius |
3 *) |
3 *) |
4 |
4 |
5 header {* The Drinker's Principle *} |
5 header \<open>The Drinker's Principle\<close> |
6 |
6 |
7 theory Drinker |
7 theory Drinker |
8 imports Main |
8 imports Main |
9 begin |
9 begin |
10 |
10 |
11 text {* Here is another example of classical reasoning: the Drinker's |
11 text \<open>Here is another example of classical reasoning: the Drinker's |
12 Principle says that for some person, if he is drunk, everybody else |
12 Principle says that for some person, if he is drunk, everybody else |
13 is drunk! |
13 is drunk! |
14 |
14 |
15 We first prove a classical part of de-Morgan's law. *} |
15 We first prove a classical part of de-Morgan's law.\<close> |
16 |
16 |
17 lemma de_Morgan: |
17 lemma de_Morgan: |
18 assumes "\<not> (\<forall>x. P x)" |
18 assumes "\<not> (\<forall>x. P x)" |
19 shows "\<exists>x. \<not> P x" |
19 shows "\<exists>x. \<not> P x" |
20 proof (rule classical) |
20 proof (rule classical) |
23 proof |
23 proof |
24 fix x show "P x" |
24 fix x show "P x" |
25 proof (rule classical) |
25 proof (rule classical) |
26 assume "\<not> P x" |
26 assume "\<not> P x" |
27 then have "\<exists>x. \<not> P x" .. |
27 then have "\<exists>x. \<not> P x" .. |
28 with `\<not> (\<exists>x. \<not> P x)` show ?thesis by contradiction |
28 with \<open>\<not> (\<exists>x. \<not> P x)\<close> show ?thesis by contradiction |
29 qed |
29 qed |
30 qed |
30 qed |
31 with `\<not> (\<forall>x. P x)` show ?thesis by contradiction |
31 with \<open>\<not> (\<forall>x. P x)\<close> show ?thesis by contradiction |
32 qed |
32 qed |
33 |
33 |
34 theorem Drinker's_Principle: "\<exists>x. drunk x \<longrightarrow> (\<forall>x. drunk x)" |
34 theorem Drinker's_Principle: "\<exists>x. drunk x \<longrightarrow> (\<forall>x. drunk x)" |
35 proof cases |
35 proof cases |
36 fix a assume "\<forall>x. drunk x" |
36 fix a assume "\<forall>x. drunk x" |