1.1 --- a/src/HOL/ex/Dedekind_Real.thy Tue Nov 05 09:45:00 2013 +0100
1.2 +++ b/src/HOL/ex/Dedekind_Real.thy Tue Nov 05 09:45:02 2013 +0100
1.3 @@ -1506,7 +1506,6 @@
1.4 instance real :: linorder
1.5 by (intro_classes, rule real_le_linear)
1.6
1.7 -
1.8 lemma real_le_eq_diff: "(x \<le> y) = (x-y \<le> (0::real))"
1.9 apply (cases x, cases y)
1.10 apply (auto simp add: real_le real_zero_def real_diff_def real_add real_minus
1.11 @@ -1657,7 +1656,6 @@
1.12 lemma real_less_all_real2: "~ 0 < y ==> \<forall>x. y < real_of_preal x"
1.13 by (blast intro!: real_less_all_preal linorder_not_less [THEN iffD1])
1.14
1.15 -
1.16 subsection {* Completeness of Positive Reals *}
1.17
1.18 text {*
1.19 @@ -1759,107 +1757,23 @@
1.20 qed
1.21
1.22 text {*
1.23 - \medskip Completeness properties using @{text "isUb"}, @{text "isLub"} etc.
1.24 -*}
1.25 -
1.26 -lemma posreals_complete:
1.27 - assumes positive_S: "\<forall>x \<in> S. 0 < x"
1.28 - and not_empty_S: "\<exists>x. x \<in> S"
1.29 - and upper_bound_Ex: "\<exists>u. isUb (UNIV::real set) S u"
1.30 - shows "\<exists>t. isLub (UNIV::real set) S t"
1.31 -proof
1.32 - let ?pS = "{w. real_of_preal w \<in> S}"
1.33 -
1.34 - obtain u where "isUb UNIV S u" using upper_bound_Ex ..
1.35 - hence sup: "\<forall>x \<in> S. x \<le> u" by (simp add: isUb_def setle_def)
1.36 -
1.37 - obtain x where x_in_S: "x \<in> S" using not_empty_S ..
1.38 - hence x_gt_zero: "0 < x" using positive_S by simp
1.39 - have "x \<le> u" using sup and x_in_S ..
1.40 - hence "0 < u" using x_gt_zero by arith
1.41 -
1.42 - then obtain pu where u_is_pu: "u = real_of_preal pu"
1.43 - by (auto simp add: real_gt_zero_preal_Ex)
1.44 -
1.45 - have pS_less_pu: "\<forall>pa \<in> ?pS. pa \<le> pu"
1.46 - proof
1.47 - fix pa
1.48 - assume "pa \<in> ?pS"
1.49 - then obtain a where a: "a \<in> S" "a = real_of_preal pa"
1.50 - by simp
1.51 - then have "a \<le> u" using sup by simp
1.52 - with a show "pa \<le> pu"
1.53 - using sup and u_is_pu by (simp add: real_of_preal_le_iff)
1.54 - qed
1.55 -
1.56 - have "\<forall>y \<in> S. y \<le> real_of_preal (psup ?pS)"
1.57 - proof
1.58 - fix y
1.59 - assume y_in_S: "y \<in> S"
1.60 - hence "0 < y" using positive_S by simp
1.61 - then obtain py where y_is_py: "y = real_of_preal py"
1.62 - by (auto simp add: real_gt_zero_preal_Ex)
1.63 - hence py_in_pS: "py \<in> ?pS" using y_in_S by simp
1.64 - with pS_less_pu have "py \<le> psup ?pS"
1.65 - by (rule preal_psup_le)
1.66 - thus "y \<le> real_of_preal (psup ?pS)"
1.67 - using y_is_py by (simp add: real_of_preal_le_iff)
1.68 - qed
1.69 -
1.70 - moreover {
1.71 - fix x
1.72 - assume x_ub_S: "\<forall>y\<in>S. y \<le> x"
1.73 - have "real_of_preal (psup ?pS) \<le> x"
1.74 - proof -
1.75 - obtain "s" where s_in_S: "s \<in> S" using not_empty_S ..
1.76 - hence s_pos: "0 < s" using positive_S by simp
1.77 -
1.78 - hence "\<exists> ps. s = real_of_preal ps" by (simp add: real_gt_zero_preal_Ex)
1.79 - then obtain "ps" where s_is_ps: "s = real_of_preal ps" ..
1.80 - hence ps_in_pS: "ps \<in> {w. real_of_preal w \<in> S}" using s_in_S by simp
1.81 -
1.82 - from x_ub_S have "s \<le> x" using s_in_S ..
1.83 - hence "0 < x" using s_pos by simp
1.84 - hence "\<exists> px. x = real_of_preal px" by (simp add: real_gt_zero_preal_Ex)
1.85 - then obtain "px" where x_is_px: "x = real_of_preal px" ..
1.86 -
1.87 - have "\<forall>pe \<in> ?pS. pe \<le> px"
1.88 - proof
1.89 - fix pe
1.90 - assume "pe \<in> ?pS"
1.91 - hence "real_of_preal pe \<in> S" by simp
1.92 - hence "real_of_preal pe \<le> x" using x_ub_S by simp
1.93 - thus "pe \<le> px" using x_is_px by (simp add: real_of_preal_le_iff)
1.94 - qed
1.95 -
1.96 - moreover have "?pS \<noteq> {}" using ps_in_pS by auto
1.97 - ultimately have "(psup ?pS) \<le> px" by (simp add: psup_le_ub)
1.98 - thus "real_of_preal (psup ?pS) \<le> x" using x_is_px by (simp add: real_of_preal_le_iff)
1.99 - qed
1.100 - }
1.101 - ultimately show "isLub UNIV S (real_of_preal (psup ?pS))"
1.102 - by (simp add: isLub_def leastP_def isUb_def setle_def setge_def)
1.103 -qed
1.104 -
1.105 -text {*
1.106 - \medskip reals Completeness (again!)
1.107 + \medskip Completeness
1.108 *}
1.109
1.110 lemma reals_complete:
1.111 + fixes S :: "real set"
1.112 assumes notempty_S: "\<exists>X. X \<in> S"
1.113 - and exists_Ub: "\<exists>Y. isUb (UNIV::real set) S Y"
1.114 - shows "\<exists>t. isLub (UNIV :: real set) S t"
1.115 + and exists_Ub: "bdd_above S"
1.116 + shows "\<exists>x. (\<forall>s\<in>S. s \<le> x) \<and> (\<forall>y. (\<forall>s\<in>S. s \<le> y) \<longrightarrow> x \<le> y)"
1.117 proof -
1.118 obtain X where X_in_S: "X \<in> S" using notempty_S ..
1.119 - obtain Y where Y_isUb: "isUb (UNIV::real set) S Y"
1.120 - using exists_Ub ..
1.121 + obtain Y where Y_isUb: "\<forall>s\<in>S. s \<le> Y"
1.122 + using exists_Ub by (auto simp: bdd_above_def)
1.123 let ?SHIFT = "{z. \<exists>x \<in>S. z = x + (-X) + 1} \<inter> {x. 0 < x}"
1.124
1.125 {
1.126 fix x
1.127 - assume "isUb (UNIV::real set) S x"
1.128 - hence S_le_x: "\<forall> y \<in> S. y <= x"
1.129 - by (simp add: isUb_def setle_def)
1.130 + assume S_le_x: "\<forall>s\<in>S. s \<le> x"
1.131 {
1.132 fix s
1.133 assume "s \<in> {z. \<exists>x\<in>S. z = x + - X + 1}"
1.134 @@ -1868,86 +1782,74 @@
1.135 then have "x1 \<le> x" using S_le_x by simp
1.136 with x1 have "s \<le> x + - X + 1" by arith
1.137 }
1.138 - then have "isUb (UNIV::real set) ?SHIFT (x + (-X) + 1)"
1.139 - by (auto simp add: isUb_def setle_def)
1.140 + then have "\<forall>s\<in>?SHIFT. s \<le> x + (-X) + 1"
1.141 + by auto
1.142 } note S_Ub_is_SHIFT_Ub = this
1.143
1.144 - hence "isUb UNIV ?SHIFT (Y + (-X) + 1)" using Y_isUb by simp
1.145 - hence "\<exists>Z. isUb UNIV ?SHIFT Z" ..
1.146 + have *: "\<forall>s\<in>?SHIFT. s \<le> Y + (-X) + 1" using Y_isUb by (rule S_Ub_is_SHIFT_Ub)
1.147 + have "\<forall>s\<in>?SHIFT. s < Y + (-X) + 2"
1.148 + proof
1.149 + fix s assume "s\<in>?SHIFT"
1.150 + with * have "s \<le> Y + (-X) + 1" by simp
1.151 + also have "\<dots> < Y + (-X) + 2" by simp
1.152 + finally show "s < Y + (-X) + 2" .
1.153 + qed
1.154 moreover have "\<forall>y \<in> ?SHIFT. 0 < y" by auto
1.155 moreover have shifted_not_empty: "\<exists>u. u \<in> ?SHIFT"
1.156 using X_in_S and Y_isUb by auto
1.157 - ultimately obtain t where t_is_Lub: "isLub UNIV ?SHIFT t"
1.158 - using posreals_complete [of ?SHIFT] by blast
1.159 + ultimately obtain t where t_is_Lub: "\<forall>y. (\<exists>x\<in>?SHIFT. y < x) = (y < t)"
1.160 + using posreal_complete [of ?SHIFT] unfolding bdd_above_def by blast
1.161
1.162 show ?thesis
1.163 proof
1.164 - show "isLub UNIV S (t + X + (-1))"
1.165 - proof (rule isLubI2)
1.166 - {
1.167 - fix x
1.168 - assume "isUb (UNIV::real set) S x"
1.169 - hence "isUb (UNIV::real set) (?SHIFT) (x + (-X) + 1)"
1.170 - using S_Ub_is_SHIFT_Ub by simp
1.171 - hence "t \<le> (x + (-X) + 1)"
1.172 - using t_is_Lub by (simp add: isLub_le_isUb)
1.173 - hence "t + X + -1 \<le> x" by arith
1.174 - }
1.175 - then show "(t + X + -1) <=* Collect (isUb UNIV S)"
1.176 - by (simp add: setgeI)
1.177 + show "(\<forall>s\<in>S. s \<le> (t + X + (-1))) \<and> (\<forall>y. (\<forall>s\<in>S. s \<le> y) \<longrightarrow> (t + X + (-1)) \<le> y)"
1.178 + proof safe
1.179 + fix x
1.180 + assume "\<forall>s\<in>S. s \<le> x"
1.181 + hence "\<forall>s\<in>?SHIFT. s \<le> x + (-X) + 1"
1.182 + using S_Ub_is_SHIFT_Ub by simp
1.183 + then have "\<not> x + (-X) + 1 < t"
1.184 + by (subst t_is_Lub[rule_format, symmetric]) (simp add: not_less)
1.185 + thus "t + X + -1 \<le> x" by arith
1.186 next
1.187 - show "isUb UNIV S (t + X + -1)"
1.188 - proof -
1.189 - {
1.190 - fix y
1.191 - assume y_in_S: "y \<in> S"
1.192 - have "y \<le> t + X + -1"
1.193 - proof -
1.194 - obtain "u" where u_in_shift: "u \<in> ?SHIFT" using shifted_not_empty ..
1.195 - hence "\<exists> x \<in> S. u = x + - X + 1" by simp
1.196 - then obtain "x" where x_and_u: "u = x + - X + 1" ..
1.197 - have u_le_t: "u \<le> t" using u_in_shift and t_is_Lub by (simp add: isLubD2)
1.198 + fix y
1.199 + assume y_in_S: "y \<in> S"
1.200 + obtain "u" where u_in_shift: "u \<in> ?SHIFT" using shifted_not_empty ..
1.201 + hence "\<exists> x \<in> S. u = x + - X + 1" by simp
1.202 + then obtain "x" where x_and_u: "u = x + - X + 1" ..
1.203 + have u_le_t: "u \<le> t"
1.204 + proof (rule dense_le)
1.205 + fix x assume "x < u" then have "x < t"
1.206 + using u_in_shift t_is_Lub by auto
1.207 + then show "x \<le> t" by simp
1.208 + qed
1.209
1.210 - show ?thesis
1.211 - proof cases
1.212 - assume "y \<le> x"
1.213 - moreover have "x = u + X + - 1" using x_and_u by arith
1.214 - moreover have "u + X + - 1 \<le> t + X + -1" using u_le_t by arith
1.215 - ultimately show "y \<le> t + X + -1" by arith
1.216 - next
1.217 - assume "~(y \<le> x)"
1.218 - hence x_less_y: "x < y" by arith
1.219 + show "y \<le> t + X + -1"
1.220 + proof cases
1.221 + assume "y \<le> x"
1.222 + moreover have "x = u + X + - 1" using x_and_u by arith
1.223 + moreover have "u + X + - 1 \<le> t + X + -1" using u_le_t by arith
1.224 + ultimately show "y \<le> t + X + -1" by arith
1.225 + next
1.226 + assume "~(y \<le> x)"
1.227 + hence x_less_y: "x < y" by arith
1.228
1.229 - have "x + (-X) + 1 \<in> ?SHIFT" using x_and_u and u_in_shift by simp
1.230 - hence "0 < x + (-X) + 1" by simp
1.231 - hence "0 < y + (-X) + 1" using x_less_y by arith
1.232 - hence "y + (-X) + 1 \<in> ?SHIFT" using y_in_S by simp
1.233 - hence "y + (-X) + 1 \<le> t" using t_is_Lub by (simp add: isLubD2)
1.234 - thus ?thesis by simp
1.235 - qed
1.236 - qed
1.237 - }
1.238 - then show ?thesis by (simp add: isUb_def setle_def)
1.239 + have "x + (-X) + 1 \<in> ?SHIFT" using x_and_u and u_in_shift by simp
1.240 + hence "0 < x + (-X) + 1" by simp
1.241 + hence "0 < y + (-X) + 1" using x_less_y by arith
1.242 + hence *: "y + (-X) + 1 \<in> ?SHIFT" using y_in_S by simp
1.243 + have "y + (-X) + 1 \<le> t"
1.244 + proof (rule dense_le)
1.245 + fix x assume "x < y + (-X) + 1" then have "x < t"
1.246 + using * t_is_Lub by auto
1.247 + then show "x \<le> t" by simp
1.248 + qed
1.249 + thus ?thesis by simp
1.250 qed
1.251 qed
1.252 qed
1.253 qed
1.254
1.255 -text{*A version of the same theorem without all those predicates!*}
1.256 -lemma reals_complete2:
1.257 - fixes S :: "(real set)"
1.258 - assumes "\<exists>y. y\<in>S" and "\<exists>(x::real). \<forall>y\<in>S. y \<le> x"
1.259 - shows "\<exists>x. (\<forall>y\<in>S. y \<le> x) &
1.260 - (\<forall>z. ((\<forall>y\<in>S. y \<le> z) --> x \<le> z))"
1.261 -proof -
1.262 - have "\<exists>x. isLub UNIV S x"
1.263 - by (rule reals_complete)
1.264 - (auto simp add: isLub_def isUb_def leastP_def setle_def setge_def assms)
1.265 - thus ?thesis
1.266 - by (metis UNIV_I isLub_isUb isLub_le_isUb isUbD isUb_def setleI)
1.267 -qed
1.268 -
1.269 -
1.270 subsection {* The Archimedean Property of the Reals *}
1.271
1.272 theorem reals_Archimedean:
1.273 @@ -1969,34 +1871,30 @@
1.274 by (rule mult_right_mono)
1.275 thus "x * of_nat (Suc n) \<le> 1" by (simp del: of_nat_Suc)
1.276 qed
1.277 - hence "{z. \<exists>n. z = x * (of_nat (Suc n))} *<= 1"
1.278 - by (simp add: setle_def del: of_nat_Suc, safe, rule spec)
1.279 - hence "isUb (UNIV::real set) {z. \<exists>n. z = x * (of_nat (Suc n))} 1"
1.280 - by (simp add: isUbI)
1.281 - hence "\<exists>Y. isUb (UNIV::real set) {z. \<exists>n. z = x* (of_nat (Suc n))} Y" ..
1.282 - moreover have "\<exists>X. X \<in> {z. \<exists>n. z = x* (of_nat (Suc n))}" by auto
1.283 - ultimately have "\<exists>t. isLub UNIV {z. \<exists>n. z = x * of_nat (Suc n)} t"
1.284 - by (simp add: reals_complete)
1.285 - then obtain "t" where
1.286 - t_is_Lub: "isLub UNIV {z. \<exists>n. z = x * of_nat (Suc n)} t" ..
1.287 + hence 2: "bdd_above {z. \<exists>n. z = x * (of_nat (Suc n))}"
1.288 + by (auto intro!: bdd_aboveI[of _ 1])
1.289 + have 1: "\<exists>X. X \<in> {z. \<exists>n. z = x* (of_nat (Suc n))}" by auto
1.290 + obtain t where
1.291 + upper: "\<And>z. z \<in> {z. \<exists>n. z = x * of_nat (Suc n)} \<Longrightarrow> z \<le> t" and
1.292 + least: "\<And>y. (\<And>a. a \<in> {z. \<exists>n. z = x * of_nat (Suc n)} \<Longrightarrow> a \<le> y) \<Longrightarrow> t \<le> y"
1.293 + using reals_complete[OF 1 2] by auto
1.294
1.295 - have "\<forall>n::nat. x * of_nat n \<le> t + - x"
1.296 - proof
1.297 - fix n
1.298 - from t_is_Lub have "x * of_nat (Suc n) \<le> t"
1.299 - by (simp add: isLubD2)
1.300 - hence "x * (of_nat n) + x \<le> t"
1.301 - by (simp add: distrib_left)
1.302 - thus "x * (of_nat n) \<le> t + - x" by arith
1.303 +
1.304 + have "t \<le> t + - x"
1.305 + proof (rule least)
1.306 + fix a assume a: "a \<in> {z. \<exists>n. z = x * (of_nat (Suc n))}"
1.307 + have "\<forall>n::nat. x * of_nat n \<le> t + - x"
1.308 + proof
1.309 + fix n
1.310 + have "x * of_nat (Suc n) \<le> t"
1.311 + by (simp add: upper)
1.312 + hence "x * (of_nat n) + x \<le> t"
1.313 + by (simp add: distrib_left)
1.314 + thus "x * (of_nat n) \<le> t + - x" by arith
1.315 + qed hence "\<forall>m. x * of_nat (Suc m) \<le> t + - x" by (simp del: of_nat_Suc)
1.316 + with a show "a \<le> t + - x"
1.317 + by auto
1.318 qed
1.319 -
1.320 - hence "\<forall>m. x * of_nat (Suc m) \<le> t + - x" by (simp del: of_nat_Suc)
1.321 - hence "{z. \<exists>n. z = x * (of_nat (Suc n))} *<= (t + - x)"
1.322 - by (auto simp add: setle_def)
1.323 - hence "isUb (UNIV::real set) {z. \<exists>n. z = x * (of_nat (Suc n))} (t + (-x))"
1.324 - by (simp add: isUbI)
1.325 - hence "t \<le> t + - x"
1.326 - using t_is_Lub by (simp add: isLub_le_isUb)
1.327 thus False using x_pos by arith
1.328 qed
1.329