author wenzelm Wed Jun 22 19:41:16 2005 +0200 (2005-06-22) changeset 16531 9b442d0e5c0c parent 16530 3e493fa130a3 child 16532 e248ffc956c7
improved proof;
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.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.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.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