improved proof;
authorwenzelm
Wed Jun 22 19:41:16 2005 +0200 (2005-06-22)
changeset 165319b442d0e5c0c
parent 16530 3e493fa130a3
child 16532 e248ffc956c7
improved proof;
src/HOL/Isar_examples/Drinker.thy
     1.1 --- a/src/HOL/Isar_examples/Drinker.thy	Wed Jun 22 19:41:15 2005 +0200
     1.2 +++ b/src/HOL/Isar_examples/Drinker.thy	Wed Jun 22 19:41:16 2005 +0200
     1.3 @@ -8,48 +8,31 @@
     1.4  theory Drinker imports Main begin
     1.5  
     1.6  text {*
     1.7 - Two parts of de-Morgan's law -- one intuitionistic and one classical:
     1.8 +  Here is another example of classical reasoning: the Drinker's
     1.9 +  Principle says that for some person, if he is drunk, everybody else
    1.10 +  is drunk!
    1.11 +
    1.12 +  We first prove a classical part of de-Morgan's law.
    1.13  *}
    1.14  
    1.15 -lemma deMorgan1: "\<not> (\<exists>x. P x) \<Longrightarrow> \<forall>x. \<not> P x"
    1.16 -proof -
    1.17 -  assume a: "\<not> (\<exists>x. P x)"
    1.18 -  show ?thesis
    1.19 -  proof
    1.20 -    fix x
    1.21 -    show "\<not> P x"
    1.22 -    proof
    1.23 -      assume "P x"
    1.24 -      then have "\<exists>x. P x" ..
    1.25 -      with a show False by contradiction
    1.26 -    qed
    1.27 -  qed
    1.28 -qed
    1.29 -
    1.30 -lemma deMorgan2: "\<not> (\<forall>x. P x) \<Longrightarrow> \<exists>x. \<not> P x"
    1.31 -proof (rule classical)
    1.32 -  assume a: "\<not> (\<forall>x. P x)"
    1.33 -  assume b: "\<not> (\<exists>x. \<not> P x)"
    1.34 -  have "\<forall>x. P x"
    1.35 +lemma deMorgan:
    1.36 +  assumes "\<not> (\<forall>x. P x)"
    1.37 +  shows "\<exists>x. \<not> P x"
    1.38 +  using prems
    1.39 +proof (rule contrapos_np)
    1.40 +  assume a: "\<not> (\<exists>x. \<not> P x)"
    1.41 +  show "\<forall>x. P x"
    1.42    proof
    1.43      fix x
    1.44      show "P x"
    1.45      proof (rule classical)
    1.46 -      assume c: "\<not> P x"
    1.47 -      from b have "\<forall>x. \<not> \<not> P x" by (rule deMorgan1)
    1.48 -      then have "\<not> \<not> P x" ..
    1.49 -      with c show ?thesis by contradiction
    1.50 +      assume "\<not> P x"
    1.51 +      then have "\<exists>x. \<not> P x" ..
    1.52 +      with a show ?thesis by contradiction
    1.53      qed
    1.54    qed
    1.55 -  with a show ?thesis by contradiction
    1.56  qed
    1.57  
    1.58 -text {*
    1.59 - Here is another example of classical reasoning: the Drinker's
    1.60 - Principle says that for some person, if he is drunk, everybody else
    1.61 - is drunk!
    1.62 -*}
    1.63 -
    1.64  theorem Drinker's_Principle: "\<exists>x. drunk x \<longrightarrow> (\<forall>x. drunk x)"
    1.65  proof cases
    1.66    fix a assume "\<forall>x. drunk x"
    1.67 @@ -57,7 +40,7 @@
    1.68    then show ?thesis ..
    1.69  next
    1.70    assume "\<not> (\<forall>x. drunk x)"
    1.71 -  then have "\<exists>x. \<not> drunk x" by (rule deMorgan2)
    1.72 +  then have "\<exists>x. \<not> drunk x" by (rule deMorgan)
    1.73    then obtain a where a: "\<not> drunk a" ..
    1.74    have "drunk a \<longrightarrow> (\<forall>x. drunk x)"
    1.75    proof