src/HOL/Isar_examples/Drinker.thy
author paulson
Tue Jun 28 15:27:45 2005 +0200 (2005-06-28)
changeset 16587 b34c8aa657a5
parent 16531 9b442d0e5c0c
child 31758 3edd5f813f01
permissions -rw-r--r--
Constant "If" is now local
wenzelm@16356
     1
(*  Title:      HOL/Isar_examples/Drinker.thy
wenzelm@16356
     2
    ID:         $Id$
wenzelm@16356
     3
    Author:     Makarius
wenzelm@16356
     4
*)
wenzelm@16356
     5
wenzelm@16356
     6
header {* The Drinker's Principle *}
wenzelm@16356
     7
haftmann@16417
     8
theory Drinker imports Main begin
wenzelm@16356
     9
wenzelm@16356
    10
text {*
wenzelm@16531
    11
  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@16531
    15
  We first prove a classical part of de-Morgan's law.
wenzelm@16356
    16
*}
wenzelm@16356
    17
wenzelm@16531
    18
lemma deMorgan:
wenzelm@16531
    19
  assumes "\<not> (\<forall>x. P x)"
wenzelm@16531
    20
  shows "\<exists>x. \<not> P x"
wenzelm@16531
    21
  using prems
wenzelm@16531
    22
proof (rule contrapos_np)
wenzelm@16531
    23
  assume a: "\<not> (\<exists>x. \<not> P x)"
wenzelm@16531
    24
  show "\<forall>x. P x"
wenzelm@16356
    25
  proof
wenzelm@16356
    26
    fix x
wenzelm@16356
    27
    show "P x"
wenzelm@16356
    28
    proof (rule classical)
wenzelm@16531
    29
      assume "\<not> P x"
wenzelm@16531
    30
      then have "\<exists>x. \<not> P x" ..
wenzelm@16531
    31
      with a show ?thesis by contradiction
wenzelm@16356
    32
    qed
wenzelm@16356
    33
  qed
wenzelm@16356
    34
qed
wenzelm@16356
    35
wenzelm@16356
    36
theorem Drinker's_Principle: "\<exists>x. drunk x \<longrightarrow> (\<forall>x. drunk x)"
wenzelm@16356
    37
proof cases
wenzelm@16356
    38
  fix a assume "\<forall>x. drunk x"
wenzelm@16356
    39
  then have "drunk a \<longrightarrow> (\<forall>x. drunk x)" ..
wenzelm@16356
    40
  then show ?thesis ..
wenzelm@16356
    41
next
wenzelm@16356
    42
  assume "\<not> (\<forall>x. drunk x)"
wenzelm@16531
    43
  then have "\<exists>x. \<not> drunk x" by (rule deMorgan)
wenzelm@16356
    44
  then obtain a where a: "\<not> drunk a" ..
wenzelm@16356
    45
  have "drunk a \<longrightarrow> (\<forall>x. drunk x)"
wenzelm@16356
    46
  proof
wenzelm@16356
    47
    assume "drunk a"
wenzelm@16356
    48
    with a show "\<forall>x. drunk x" by (contradiction)
wenzelm@16356
    49
  qed
wenzelm@16356
    50
  then show ?thesis ..
wenzelm@16356
    51
qed
wenzelm@16356
    52
wenzelm@16356
    53
end