src/HOL/Isar_Examples/Drinker.thy
author wenzelm
Tue Oct 20 19:37:09 2009 +0200 (2009-10-20)
changeset 33026 8f35633c4922
parent 31758 src/HOL/Isar_examples/Drinker.thy@3edd5f813f01
child 37671 fa53d267dab3
permissions -rw-r--r--
modernized session Isar_Examples;
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@16356
    11
text {*
wenzelm@16531
    12
  Here is another example of classical reasoning: the Drinker's
wenzelm@16531
    13
  Principle says that for some person, if he is drunk, everybody else
wenzelm@16531
    14
  is drunk!
wenzelm@16531
    15
wenzelm@16531
    16
  We first prove a classical part of de-Morgan's law.
wenzelm@16356
    17
*}
wenzelm@16356
    18
wenzelm@16531
    19
lemma deMorgan:
wenzelm@16531
    20
  assumes "\<not> (\<forall>x. P x)"
wenzelm@16531
    21
  shows "\<exists>x. \<not> P x"
wenzelm@16531
    22
  using prems
wenzelm@16531
    23
proof (rule contrapos_np)
wenzelm@16531
    24
  assume a: "\<not> (\<exists>x. \<not> P x)"
wenzelm@16531
    25
  show "\<forall>x. P x"
wenzelm@16356
    26
  proof
wenzelm@16356
    27
    fix x
wenzelm@16356
    28
    show "P x"
wenzelm@16356
    29
    proof (rule classical)
wenzelm@16531
    30
      assume "\<not> P x"
wenzelm@16531
    31
      then have "\<exists>x. \<not> P x" ..
wenzelm@16531
    32
      with a show ?thesis by contradiction
wenzelm@16356
    33
    qed
wenzelm@16356
    34
  qed
wenzelm@16356
    35
qed
wenzelm@16356
    36
wenzelm@16356
    37
theorem Drinker's_Principle: "\<exists>x. drunk x \<longrightarrow> (\<forall>x. drunk x)"
wenzelm@16356
    38
proof cases
wenzelm@16356
    39
  fix a assume "\<forall>x. drunk x"
wenzelm@16356
    40
  then have "drunk a \<longrightarrow> (\<forall>x. drunk x)" ..
wenzelm@16356
    41
  then show ?thesis ..
wenzelm@16356
    42
next
wenzelm@16356
    43
  assume "\<not> (\<forall>x. drunk x)"
wenzelm@16531
    44
  then have "\<exists>x. \<not> drunk x" by (rule deMorgan)
wenzelm@16356
    45
  then obtain a where a: "\<not> drunk a" ..
wenzelm@16356
    46
  have "drunk a \<longrightarrow> (\<forall>x. drunk x)"
wenzelm@16356
    47
  proof
wenzelm@16356
    48
    assume "drunk a"
wenzelm@16356
    49
    with a show "\<forall>x. drunk x" by (contradiction)
wenzelm@16356
    50
  qed
wenzelm@16356
    51
  then show ?thesis ..
wenzelm@16356
    52
qed
wenzelm@16356
    53
wenzelm@16356
    54
end