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;
     1 (*  Title:      HOL/Isar_Examples/Drinker.thy
     2     Author:     Makarius
     3 *)
     4 
     5 header {* The Drinker's Principle *}
     6 
     7 theory Drinker
     8 imports Main
     9 begin
    10 
    11 text {*
    12   Here is another example of classical reasoning: the Drinker's
    13   Principle says that for some person, if he is drunk, everybody else
    14   is drunk!
    15 
    16   We first prove a classical part of de-Morgan's law.
    17 *}
    18 
    19 lemma deMorgan:
    20   assumes "\<not> (\<forall>x. P x)"
    21   shows "\<exists>x. \<not> P x"
    22   using prems
    23 proof (rule contrapos_np)
    24   assume a: "\<not> (\<exists>x. \<not> P x)"
    25   show "\<forall>x. P x"
    26   proof
    27     fix x
    28     show "P x"
    29     proof (rule classical)
    30       assume "\<not> P x"
    31       then have "\<exists>x. \<not> P x" ..
    32       with a show ?thesis by contradiction
    33     qed
    34   qed
    35 qed
    36 
    37 theorem Drinker's_Principle: "\<exists>x. drunk x \<longrightarrow> (\<forall>x. drunk x)"
    38 proof cases
    39   fix a assume "\<forall>x. drunk x"
    40   then have "drunk a \<longrightarrow> (\<forall>x. drunk x)" ..
    41   then show ?thesis ..
    42 next
    43   assume "\<not> (\<forall>x. drunk x)"
    44   then have "\<exists>x. \<not> drunk x" by (rule deMorgan)
    45   then obtain a where a: "\<not> drunk a" ..
    46   have "drunk a \<longrightarrow> (\<forall>x. drunk x)"
    47   proof
    48     assume "drunk a"
    49     with a show "\<forall>x. drunk x" by (contradiction)
    50   qed
    51   then show ?thesis ..
    52 qed
    53 
    54 end