src/HOL/Isar_examples/Drinker.thy
author wenzelm
Thu Jun 09 23:33:28 2005 +0200 (2005-06-09)
changeset 16356 94011cf701a4
child 16417 9bc16273c2d4
permissions -rw-r--r--
added Isar_examples/Drinker.thy;
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
wenzelm@16356
     8
theory Drinker = Main:
wenzelm@16356
     9
wenzelm@16356
    10
text {*
wenzelm@16356
    11
 Two parts of de-Morgan's law -- one intuitionistic and one classical:
wenzelm@16356
    12
*}
wenzelm@16356
    13
wenzelm@16356
    14
lemma deMorgan1: "\<not> (\<exists>x. P x) \<Longrightarrow> \<forall>x. \<not> P x"
wenzelm@16356
    15
proof -
wenzelm@16356
    16
  assume a: "\<not> (\<exists>x. P x)"
wenzelm@16356
    17
  show ?thesis
wenzelm@16356
    18
  proof
wenzelm@16356
    19
    fix x
wenzelm@16356
    20
    show "\<not> P x"
wenzelm@16356
    21
    proof
wenzelm@16356
    22
      assume "P x"
wenzelm@16356
    23
      then have "\<exists>x. P x" ..
wenzelm@16356
    24
      with a show False by contradiction
wenzelm@16356
    25
    qed
wenzelm@16356
    26
  qed
wenzelm@16356
    27
qed
wenzelm@16356
    28
wenzelm@16356
    29
lemma deMorgan2: "\<not> (\<forall>x. P x) \<Longrightarrow> \<exists>x. \<not> P x"
wenzelm@16356
    30
proof (rule classical)
wenzelm@16356
    31
  assume a: "\<not> (\<forall>x. P x)"
wenzelm@16356
    32
  assume b: "\<not> (\<exists>x. \<not> P x)"
wenzelm@16356
    33
  have "\<forall>x. P x"
wenzelm@16356
    34
  proof
wenzelm@16356
    35
    fix x
wenzelm@16356
    36
    show "P x"
wenzelm@16356
    37
    proof (rule classical)
wenzelm@16356
    38
      assume c: "\<not> P x"
wenzelm@16356
    39
      from b have "\<forall>x. \<not> \<not> P x" by (rule deMorgan1)
wenzelm@16356
    40
      then have "\<not> \<not> P x" ..
wenzelm@16356
    41
      with c show ?thesis by contradiction
wenzelm@16356
    42
    qed
wenzelm@16356
    43
  qed
wenzelm@16356
    44
  with a show ?thesis by contradiction
wenzelm@16356
    45
qed
wenzelm@16356
    46
wenzelm@16356
    47
text {*
wenzelm@16356
    48
 Here is another example of classical reasoning: the Drinker's
wenzelm@16356
    49
 Principle says that for some person, if he is drunk, everybody else
wenzelm@16356
    50
 is drunk!
wenzelm@16356
    51
*}
wenzelm@16356
    52
wenzelm@16356
    53
theorem Drinker's_Principle: "\<exists>x. drunk x \<longrightarrow> (\<forall>x. drunk x)"
wenzelm@16356
    54
proof cases
wenzelm@16356
    55
  fix a assume "\<forall>x. drunk x"
wenzelm@16356
    56
  then have "drunk a \<longrightarrow> (\<forall>x. drunk x)" ..
wenzelm@16356
    57
  then show ?thesis ..
wenzelm@16356
    58
next
wenzelm@16356
    59
  assume "\<not> (\<forall>x. drunk x)"
wenzelm@16356
    60
  then have "\<exists>x. \<not> drunk x" by (rule deMorgan2)
wenzelm@16356
    61
  then obtain a where a: "\<not> drunk a" ..
wenzelm@16356
    62
  have "drunk a \<longrightarrow> (\<forall>x. drunk x)"
wenzelm@16356
    63
  proof
wenzelm@16356
    64
    assume "drunk a"
wenzelm@16356
    65
    with a show "\<forall>x. drunk x" by (contradiction)
wenzelm@16356
    66
  qed
wenzelm@16356
    67
  then show ?thesis ..
wenzelm@16356
    68
qed
wenzelm@16356
    69
wenzelm@16356
    70
end