src/HOL/Isar_Examples/Drinker.thy
author blanchet
Thu Sep 11 18:54:36 2014 +0200 (2014-09-11)
changeset 58306 117ba6cbe414
parent 49930 defce6616890
child 58614 7338eb25226c
permissions -rw-r--r--
renamed 'rep_datatype' to 'old_rep_datatype' (HOL)
     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 {* 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 lemma de_Morgan:
    18   assumes "\<not> (\<forall>x. P x)"
    19   shows "\<exists>x. \<not> P x"
    20 proof (rule classical)
    21   assume "\<not> (\<exists>x. \<not> P x)"
    22   have "\<forall>x. P x"
    23   proof
    24     fix x show "P x"
    25     proof (rule classical)
    26       assume "\<not> P x"
    27       then have "\<exists>x. \<not> P x" ..
    28       with `\<not> (\<exists>x. \<not> P x)` show ?thesis by contradiction
    29     qed
    30   qed
    31   with `\<not> (\<forall>x. P x)` show ?thesis by contradiction
    32 qed
    33 
    34 theorem Drinker's_Principle: "\<exists>x. drunk x \<longrightarrow> (\<forall>x. drunk x)"
    35 proof cases
    36   fix a assume "\<forall>x. drunk x"
    37   then have "drunk a \<longrightarrow> (\<forall>x. drunk x)" ..
    38   then show ?thesis ..
    39 next
    40   assume "\<not> (\<forall>x. drunk x)"
    41   then have "\<exists>x. \<not> drunk x" by (rule de_Morgan)
    42   then obtain a where a: "\<not> drunk a" ..
    43   have "drunk a \<longrightarrow> (\<forall>x. drunk x)"
    44   proof
    45     assume "drunk a"
    46     with a show "\<forall>x. drunk x" by contradiction
    47   qed
    48   then show ?thesis ..
    49 qed
    50 
    51 end