33026

1 
(* Title: HOL/Isar_Examples/Drinker.thy

16356

2 
Author: Makarius


3 
*)


4 


5 
header {* The Drinker's Principle *}


6 

31758

7 
theory Drinker


8 
imports Main


9 
begin

16356

10 

37671

11 
text {* 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 

37671

15 
We first prove a classical part of deMorgan's law. *}

16356

16 

37671

17 
lemma de_Morgan:

16531

18 
assumes "\<not> (\<forall>x. P x)"


19 
shows "\<exists>x. \<not> P x"

37671

20 
using assms

16531

21 
proof (rule contrapos_np)


22 
assume a: "\<not> (\<exists>x. \<not> P x)"


23 
show "\<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" ..


29 
with a show ?thesis by contradiction

16356

30 
qed


31 
qed


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
