summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Isar_Examples/Drinker.thy

author | blanchet |

Thu Sep 11 18:54:36 2014 +0200 (2014-09-11) | |

changeset 58306 | 117ba6cbe414 |

parent 49930 | defce6616890 |

child 58614 | 7338eb25226c |

permissions | -rw-r--r-- |

renamed 'rep_datatype' to 'old_rep_datatype' (HOL)

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

2 Author: Makarius

3 *)

5 header {* The Drinker's Principle *}

7 theory Drinker

8 imports Main

9 begin

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

15 We first prove a classical part of de-Morgan's law. *}

17 lemma de_Morgan:

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

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

20 proof (rule classical)

21 assume "\<not> (\<exists>x. \<not> P x)"

22 have "\<forall>x. P x"

23 proof

24 fix x show "P x"

25 proof (rule classical)

26 assume "\<not> P x"

27 then have "\<exists>x. \<not> P x" ..

28 with `\<not> (\<exists>x. \<not> P x)` show ?thesis by contradiction

29 qed

30 qed

31 with `\<not> (\<forall>x. P x)` show ?thesis by contradiction

32 qed

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)"

41 then have "\<exists>x. \<not> drunk x" by (rule de_Morgan)

42 then obtain a where a: "\<not> drunk a" ..

43 have "drunk a \<longrightarrow> (\<forall>x. drunk x)"

44 proof

45 assume "drunk a"

46 with a show "\<forall>x. drunk x" by contradiction

47 qed

48 then show ?thesis ..

49 qed

51 end