1.1 --- a/src/HOL/Library/ContNotDenum.thy Tue Nov 05 09:45:00 2013 +0100
1.2 +++ b/src/HOL/Library/ContNotDenum.thy Tue Nov 05 09:45:02 2013 +0100
1.3 @@ -131,17 +131,15 @@
1.4
1.5 -- "A denotes the set of all left-most points of all the intervals ..."
1.6 moreover obtain A where Adef: "A = ?g ` \<nat>" by simp
1.7 - ultimately have "\<exists>x. x\<in>A"
1.8 + ultimately have "A \<noteq> {}"
1.9 proof -
1.10 have "(0::nat) \<in> \<nat>" by simp
1.11 - moreover have "?g 0 = ?g 0" by simp
1.12 - ultimately have "?g 0 \<in> ?g ` \<nat>" by (rule rev_image_eqI)
1.13 - with Adef have "?g 0 \<in> A" by simp
1.14 - thus ?thesis ..
1.15 + with Adef show ?thesis
1.16 + by blast
1.17 qed
1.18
1.19 -- "Now show that A is bounded above ..."
1.20 - moreover have "\<exists>y. isUb (UNIV::real set) A y"
1.21 + moreover have "bdd_above A"
1.22 proof -
1.23 {
1.24 fix n
1.25 @@ -177,18 +175,11 @@
1.26 obtain a and b where "f 0 = closed_int a b" and alb: "a \<le> b" by blast
1.27 ultimately have "\<forall>n. ?g n \<in> closed_int a b" by auto
1.28 with alb have "\<forall>n. ?g n \<le> b" using closed_int_most by blast
1.29 - with Adef have "\<forall>y\<in>A. y\<le>b" by auto
1.30 - hence "A *<= b" by (unfold setle_def)
1.31 - moreover have "b \<in> (UNIV::real set)" by simp
1.32 - ultimately have "A *<= b \<and> b \<in> (UNIV::real set)" by simp
1.33 - hence "isUb (UNIV::real set) A b" by (unfold isUb_def)
1.34 - thus ?thesis by auto
1.35 + with Adef show "bdd_above A" by auto
1.36 qed
1.37 - -- "by the Axiom Of Completeness, A has a least upper bound ..."
1.38 - ultimately have "\<exists>t. isLub UNIV A t" by (rule reals_complete)
1.39
1.40 -- "denote this least upper bound as t ..."
1.41 - then obtain t where tdef: "isLub UNIV A t" ..
1.42 + def tdef: t == "Sup A"
1.43
1.44 -- "and finally show that this least upper bound is in all the intervals..."
1.45 have "\<forall>n. t \<in> f n"
1.46 @@ -229,82 +220,76 @@
1.47 with Adef have "(?g n) \<in> A" by auto
1.48 ultimately show ?thesis by simp
1.49 qed
1.50 - with tdef show "a \<le> t" by (rule isLubD2)
1.51 + with `bdd_above A` show "a \<le> t"
1.52 + unfolding tdef by (intro cSup_upper)
1.53 qed
1.54 moreover have "t \<le> b"
1.55 - proof -
1.56 - have "isUb UNIV A b"
1.57 - proof -
1.58 + unfolding tdef
1.59 + proof (rule cSup_least)
1.60 + {
1.61 + from alb int have
1.62 + ain: "b\<in>f n \<and> (\<forall>x\<in>f n. x \<le> b)" using closed_int_most by blast
1.63 +
1.64 + have subsetd: "\<forall>m. \<forall>n. f (n + m) \<subseteq> f n"
1.65 + proof (rule allI, induct_tac m)
1.66 + show "\<forall>n. f (n + 0) \<subseteq> f n" by simp
1.67 + next
1.68 + fix m n
1.69 + assume pp: "\<forall>p. f (p + n) \<subseteq> f p"
1.70 + {
1.71 + fix p
1.72 + from pp have "f (p + n) \<subseteq> f p" by simp
1.73 + moreover from subset have "f (Suc (p + n)) \<subseteq> f (p + n)" by auto
1.74 + hence "f (p + (Suc n)) \<subseteq> f (p + n)" by simp
1.75 + ultimately have "f (p + (Suc n)) \<subseteq> f p" by simp
1.76 + }
1.77 + thus "\<forall>p. f (p + Suc n) \<subseteq> f p" ..
1.78 + qed
1.79 + have subsetm: "\<forall>\<alpha> \<beta>. \<alpha> \<ge> \<beta> \<longrightarrow> (f \<alpha>) \<subseteq> (f \<beta>)"
1.80 + proof ((rule allI)+, rule impI)
1.81 + fix \<alpha>::nat and \<beta>::nat
1.82 + assume "\<beta> \<le> \<alpha>"
1.83 + hence "\<exists>k. \<alpha> = \<beta> + k" by (simp only: le_iff_add)
1.84 + then obtain k where "\<alpha> = \<beta> + k" ..
1.85 + moreover
1.86 + from subsetd have "f (\<beta> + k) \<subseteq> f \<beta>" by simp
1.87 + ultimately show "f \<alpha> \<subseteq> f \<beta>" by auto
1.88 + qed
1.89 +
1.90 + fix m
1.91 {
1.92 - from alb int have
1.93 - ain: "b\<in>f n \<and> (\<forall>x\<in>f n. x \<le> b)" using closed_int_most by blast
1.94 -
1.95 - have subsetd: "\<forall>m. \<forall>n. f (n + m) \<subseteq> f n"
1.96 - proof (rule allI, induct_tac m)
1.97 - show "\<forall>n. f (n + 0) \<subseteq> f n" by simp
1.98 - next
1.99 - fix m n
1.100 - assume pp: "\<forall>p. f (p + n) \<subseteq> f p"
1.101 - {
1.102 - fix p
1.103 - from pp have "f (p + n) \<subseteq> f p" by simp
1.104 - moreover from subset have "f (Suc (p + n)) \<subseteq> f (p + n)" by auto
1.105 - hence "f (p + (Suc n)) \<subseteq> f (p + n)" by simp
1.106 - ultimately have "f (p + (Suc n)) \<subseteq> f p" by simp
1.107 - }
1.108 - thus "\<forall>p. f (p + Suc n) \<subseteq> f p" ..
1.109 - qed
1.110 - have subsetm: "\<forall>\<alpha> \<beta>. \<alpha> \<ge> \<beta> \<longrightarrow> (f \<alpha>) \<subseteq> (f \<beta>)"
1.111 - proof ((rule allI)+, rule impI)
1.112 - fix \<alpha>::nat and \<beta>::nat
1.113 - assume "\<beta> \<le> \<alpha>"
1.114 - hence "\<exists>k. \<alpha> = \<beta> + k" by (simp only: le_iff_add)
1.115 - then obtain k where "\<alpha> = \<beta> + k" ..
1.116 - moreover
1.117 - from subsetd have "f (\<beta> + k) \<subseteq> f \<beta>" by simp
1.118 - ultimately show "f \<alpha> \<subseteq> f \<beta>" by auto
1.119 - qed
1.120 -
1.121 - fix m
1.122 - {
1.123 - assume "m \<ge> n"
1.124 - with subsetm have "f m \<subseteq> f n" by simp
1.125 - with ain have "\<forall>x\<in>f m. x \<le> b" by auto
1.126 - moreover
1.127 - from gdef have "?g m \<in> f m \<and> (\<forall>x\<in>f m. ?g m \<le> x)" by simp
1.128 - ultimately have "?g m \<le> b" by auto
1.129 - }
1.130 + assume "m \<ge> n"
1.131 + with subsetm have "f m \<subseteq> f n" by simp
1.132 + with ain have "\<forall>x\<in>f m. x \<le> b" by auto
1.133 moreover
1.134 - {
1.135 - assume "\<not>(m \<ge> n)"
1.136 - hence "m < n" by simp
1.137 - with subsetm have sub: "(f n) \<subseteq> (f m)" by simp
1.138 - from closed obtain ma and mb where
1.139 - "f m = closed_int ma mb \<and> ma \<le> mb" by blast
1.140 - hence one: "ma \<le> mb" and fm: "f m = closed_int ma mb" by auto
1.141 - from one alb sub fm int have "ma \<le> b" using closed_subset by blast
1.142 - moreover have "(?g m) = ma"
1.143 - proof -
1.144 - from gdef have "?g m \<in> f m \<and> (\<forall>x\<in>f m. ?g m \<le> x)" ..
1.145 - moreover from one have
1.146 - "ma \<in> closed_int ma mb \<and> (\<forall>x\<in>closed_int ma mb. ma \<le> x)"
1.147 - by (rule closed_int_least)
1.148 - with fm have "ma\<in>f m \<and> (\<forall>x\<in>f m. ma \<le> x)" by simp
1.149 - ultimately have "ma \<le> ?g m \<and> ?g m \<le> ma" by auto
1.150 - thus "?g m = ma" by auto
1.151 - qed
1.152 - ultimately have "?g m \<le> b" by simp
1.153 - }
1.154 - ultimately have "?g m \<le> b" by (rule case_split)
1.155 + from gdef have "?g m \<in> f m \<and> (\<forall>x\<in>f m. ?g m \<le> x)" by simp
1.156 + ultimately have "?g m \<le> b" by auto
1.157 }
1.158 - with Adef have "\<forall>y\<in>A. y\<le>b" by auto
1.159 - hence "A *<= b" by (unfold setle_def)
1.160 - moreover have "b \<in> (UNIV::real set)" by simp
1.161 - ultimately have "A *<= b \<and> b \<in> (UNIV::real set)" by simp
1.162 - thus "isUb (UNIV::real set) A b" by (unfold isUb_def)
1.163 - qed
1.164 - with tdef show "t \<le> b" by (rule isLub_le_isUb)
1.165 - qed
1.166 + moreover
1.167 + {
1.168 + assume "\<not>(m \<ge> n)"
1.169 + hence "m < n" by simp
1.170 + with subsetm have sub: "(f n) \<subseteq> (f m)" by simp
1.171 + from closed obtain ma and mb where
1.172 + "f m = closed_int ma mb \<and> ma \<le> mb" by blast
1.173 + hence one: "ma \<le> mb" and fm: "f m = closed_int ma mb" by auto
1.174 + from one alb sub fm int have "ma \<le> b" using closed_subset by blast
1.175 + moreover have "(?g m) = ma"
1.176 + proof -
1.177 + from gdef have "?g m \<in> f m \<and> (\<forall>x\<in>f m. ?g m \<le> x)" ..
1.178 + moreover from one have
1.179 + "ma \<in> closed_int ma mb \<and> (\<forall>x\<in>closed_int ma mb. ma \<le> x)"
1.180 + by (rule closed_int_least)
1.181 + with fm have "ma\<in>f m \<and> (\<forall>x\<in>f m. ma \<le> x)" by simp
1.182 + ultimately have "ma \<le> ?g m \<and> ?g m \<le> ma" by auto
1.183 + thus "?g m = ma" by auto
1.184 + qed
1.185 + ultimately have "?g m \<le> b" by simp
1.186 + }
1.187 + ultimately have "?g m \<le> b" by (rule case_split)
1.188 + }
1.189 + with Adef show "\<And>y. y \<in> A \<Longrightarrow> y \<le> b" by auto
1.190 + qed fact
1.191 ultimately have "t \<in> closed_int a b" by (rule closed_mem)
1.192 with int show "t \<in> f n" by simp
1.193 qed