summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Library/ContNotDenum.thy

changeset 54263 | c4159fe6fa46 |

parent 53372 | f5a6313c7fe4 |

child 54797 | be020ec8560c |

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 - { 1.59 - from alb int have 1.60 - ain: "b\<in>f n \<and> (\<forall>x\<in>f n. x \<le> b)" using closed_int_most by blast 1.61 - 1.62 - have subsetd: "\<forall>m. \<forall>n. f (n + m) \<subseteq> f n" 1.63 - proof (rule allI, induct_tac m) 1.64 - show "\<forall>n. f (n + 0) \<subseteq> f n" by simp 1.65 - next 1.66 - fix m n 1.67 - assume pp: "\<forall>p. f (p + n) \<subseteq> f p" 1.68 - { 1.69 - fix p 1.70 - from pp have "f (p + n) \<subseteq> f p" by simp 1.71 - moreover from subset have "f (Suc (p + n)) \<subseteq> f (p + n)" by auto 1.72 - hence "f (p + (Suc n)) \<subseteq> f (p + n)" by simp 1.73 - ultimately have "f (p + (Suc n)) \<subseteq> f p" by simp 1.74 - } 1.75 - thus "\<forall>p. f (p + Suc n) \<subseteq> f p" .. 1.76 - qed 1.77 - have subsetm: "\<forall>\<alpha> \<beta>. \<alpha> \<ge> \<beta> \<longrightarrow> (f \<alpha>) \<subseteq> (f \<beta>)" 1.78 - proof ((rule allI)+, rule impI) 1.79 - fix \<alpha>::nat and \<beta>::nat 1.80 - assume "\<beta> \<le> \<alpha>" 1.81 - hence "\<exists>k. \<alpha> = \<beta> + k" by (simp only: le_iff_add) 1.82 - then obtain k where "\<alpha> = \<beta> + k" .. 1.83 - moreover 1.84 - from subsetd have "f (\<beta> + k) \<subseteq> f \<beta>" by simp 1.85 - ultimately show "f \<alpha> \<subseteq> f \<beta>" by auto 1.86 - qed 1.87 - 1.88 - fix m 1.89 + unfolding tdef 1.90 + proof (rule cSup_least) 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 - assume "m \<ge> n" 1.103 - with subsetm have "f m \<subseteq> f n" by simp 1.104 - with ain have "\<forall>x\<in>f m. x \<le> b" by auto 1.105 - moreover 1.106 - from gdef have "?g m \<in> f m \<and> (\<forall>x\<in>f m. ?g m \<le> x)" by simp 1.107 - ultimately have "?g m \<le> b" by auto 1.108 + fix p 1.109 + from pp have "f (p + n) \<subseteq> f p" by simp 1.110 + moreover from subset have "f (Suc (p + n)) \<subseteq> f (p + n)" by auto 1.111 + hence "f (p + (Suc n)) \<subseteq> f (p + n)" by simp 1.112 + ultimately have "f (p + (Suc n)) \<subseteq> f p" by simp 1.113 } 1.114 + thus "\<forall>p. f (p + Suc n) \<subseteq> f p" .. 1.115 + qed 1.116 + have subsetm: "\<forall>\<alpha> \<beta>. \<alpha> \<ge> \<beta> \<longrightarrow> (f \<alpha>) \<subseteq> (f \<beta>)" 1.117 + proof ((rule allI)+, rule impI) 1.118 + fix \<alpha>::nat and \<beta>::nat 1.119 + assume "\<beta> \<le> \<alpha>" 1.120 + hence "\<exists>k. \<alpha> = \<beta> + k" by (simp only: le_iff_add) 1.121 + then obtain k where "\<alpha> = \<beta> + k" .. 1.122 + moreover 1.123 + from subsetd have "f (\<beta> + k) \<subseteq> f \<beta>" by simp 1.124 + ultimately show "f \<alpha> \<subseteq> f \<beta>" by auto 1.125 + qed 1.126 + 1.127 + fix m 1.128 + { 1.129 + assume "m \<ge> n" 1.130 + with subsetm have "f m \<subseteq> f n" by simp 1.131 + with ain have "\<forall>x\<in>f m. x \<le> b" by auto 1.132 moreover 1.133 - { 1.134 - assume "\<not>(m \<ge> n)" 1.135 - hence "m < n" by simp 1.136 - with subsetm have sub: "(f n) \<subseteq> (f m)" by simp 1.137 - from closed obtain ma and mb where 1.138 - "f m = closed_int ma mb \<and> ma \<le> mb" by blast 1.139 - hence one: "ma \<le> mb" and fm: "f m = closed_int ma mb" by auto 1.140 - from one alb sub fm int have "ma \<le> b" using closed_subset by blast 1.141 - moreover have "(?g m) = ma" 1.142 - proof - 1.143 - from gdef have "?g m \<in> f m \<and> (\<forall>x\<in>f m. ?g m \<le> x)" .. 1.144 - moreover from one have 1.145 - "ma \<in> closed_int ma mb \<and> (\<forall>x\<in>closed_int ma mb. ma \<le> x)" 1.146 - by (rule closed_int_least) 1.147 - with fm have "ma\<in>f m \<and> (\<forall>x\<in>f m. ma \<le> x)" by simp 1.148 - ultimately have "ma \<le> ?g m \<and> ?g m \<le> ma" by auto 1.149 - thus "?g m = ma" by auto 1.150 - qed 1.151 - ultimately have "?g m \<le> b" by simp 1.152 - } 1.153 - ultimately have "?g m \<le> b" by (rule case_split) 1.154 + from gdef have "?g m \<in> f m \<and> (\<forall>x\<in>f m. ?g m \<le> x)" by simp 1.155 + ultimately have "?g m \<le> b" by auto 1.156 } 1.157 - with Adef have "\<forall>y\<in>A. y\<le>b" by auto 1.158 - hence "A *<= b" by (unfold setle_def) 1.159 - moreover have "b \<in> (UNIV::real set)" by simp 1.160 - ultimately have "A *<= b \<and> b \<in> (UNIV::real set)" by simp 1.161 - thus "isUb (UNIV::real set) A b" by (unfold isUb_def) 1.162 - qed 1.163 - with tdef show "t \<le> b" by (rule isLub_le_isUb) 1.164 - qed 1.165 + moreover 1.166 + { 1.167 + assume "\<not>(m \<ge> n)" 1.168 + hence "m < n" by simp 1.169 + with subsetm have sub: "(f n) \<subseteq> (f m)" by simp 1.170 + from closed obtain ma and mb where 1.171 + "f m = closed_int ma mb \<and> ma \<le> mb" by blast 1.172 + hence one: "ma \<le> mb" and fm: "f m = closed_int ma mb" by auto 1.173 + from one alb sub fm int have "ma \<le> b" using closed_subset by blast 1.174 + moreover have "(?g m) = ma" 1.175 + proof - 1.176 + from gdef have "?g m \<in> f m \<and> (\<forall>x\<in>f m. ?g m \<le> x)" .. 1.177 + moreover from one have 1.178 + "ma \<in> closed_int ma mb \<and> (\<forall>x\<in>closed_int ma mb. ma \<le> x)" 1.179 + by (rule closed_int_least) 1.180 + with fm have "ma\<in>f m \<and> (\<forall>x\<in>f m. ma \<le> x)" by simp 1.181 + ultimately have "ma \<le> ?g m \<and> ?g m \<le> ma" by auto 1.182 + thus "?g m = ma" by auto 1.183 + qed 1.184 + ultimately have "?g m \<le> b" by simp 1.185 + } 1.186 + ultimately have "?g m \<le> b" by (rule case_split) 1.187 + } 1.188 + with Adef show "\<And>y. y \<in> A \<Longrightarrow> y \<le> b" by auto 1.189 + qed fact 1.190 ultimately have "t \<in> closed_int a b" by (rule closed_mem) 1.191 with int show "t \<in> f n" by simp 1.192 qed