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