src/HOL/Isar_Examples/Drinker.thy
author hoelzl
Tue Mar 26 12:20:58 2013 +0100 (2013-03-26)
changeset 51526 155263089e7b
parent 49930 defce6616890
child 58614 7338eb25226c
permissions -rw-r--r--
move SEQ.thy and Lim.thy to Limits.thy
wenzelm@33026
     1
(*  Title:      HOL/Isar_Examples/Drinker.thy
wenzelm@16356
     2
    Author:     Makarius
wenzelm@16356
     3
*)
wenzelm@16356
     4
wenzelm@16356
     5
header {* The Drinker's Principle *}
wenzelm@16356
     6
wenzelm@31758
     7
theory Drinker
wenzelm@31758
     8
imports Main
wenzelm@31758
     9
begin
wenzelm@16356
    10
wenzelm@37671
    11
text {* Here is another example of classical reasoning: the Drinker's
wenzelm@16531
    12
  Principle says that for some person, if he is drunk, everybody else
wenzelm@16531
    13
  is drunk!
wenzelm@16531
    14
wenzelm@37671
    15
  We first prove a classical part of de-Morgan's law. *}
wenzelm@16356
    16
wenzelm@37671
    17
lemma de_Morgan:
wenzelm@16531
    18
  assumes "\<not> (\<forall>x. P x)"
wenzelm@16531
    19
  shows "\<exists>x. \<not> P x"
wenzelm@47960
    20
proof (rule classical)
wenzelm@47960
    21
  assume "\<not> (\<exists>x. \<not> P x)"
wenzelm@47960
    22
  have "\<forall>x. P x"
wenzelm@16356
    23
  proof
wenzelm@37671
    24
    fix x show "P x"
wenzelm@16356
    25
    proof (rule classical)
wenzelm@16531
    26
      assume "\<not> P x"
wenzelm@16531
    27
      then have "\<exists>x. \<not> P x" ..
wenzelm@47960
    28
      with `\<not> (\<exists>x. \<not> P x)` show ?thesis by contradiction
wenzelm@16356
    29
    qed
wenzelm@16356
    30
  qed
wenzelm@49930
    31
  with `\<not> (\<forall>x. P x)` show ?thesis by contradiction
wenzelm@16356
    32
qed
wenzelm@16356
    33
wenzelm@16356
    34
theorem Drinker's_Principle: "\<exists>x. drunk x \<longrightarrow> (\<forall>x. drunk x)"
wenzelm@16356
    35
proof cases
wenzelm@16356
    36
  fix a assume "\<forall>x. drunk x"
wenzelm@16356
    37
  then have "drunk a \<longrightarrow> (\<forall>x. drunk x)" ..
wenzelm@16356
    38
  then show ?thesis ..
wenzelm@16356
    39
next
wenzelm@16356
    40
  assume "\<not> (\<forall>x. drunk x)"
wenzelm@37671
    41
  then have "\<exists>x. \<not> drunk x" by (rule de_Morgan)
wenzelm@16356
    42
  then obtain a where a: "\<not> drunk a" ..
wenzelm@16356
    43
  have "drunk a \<longrightarrow> (\<forall>x. drunk x)"
wenzelm@16356
    44
  proof
wenzelm@16356
    45
    assume "drunk a"
wenzelm@37671
    46
    with a show "\<forall>x. drunk x" by contradiction
wenzelm@16356
    47
  qed
wenzelm@16356
    48
  then show ?thesis ..
wenzelm@16356
    49
qed
wenzelm@16356
    50
wenzelm@16356
    51
end