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