1(* Title: HOL/Real.thy 2 Author: Jacques D. Fleuriot, University of Edinburgh, 1998 3 Author: Larry Paulson, University of Cambridge 4 Author: Jeremy Avigad, Carnegie Mellon University 5 Author: Florian Zuleger, Johannes Hoelzl, and Simon Funke, TU Muenchen 6 Conversion to Isar and new proofs by Lawrence C Paulson, 2003/4 7 Construction of Cauchy Reals by Brian Huffman, 2010 8*) 9 10section \<open>Development of the Reals using Cauchy Sequences\<close> 11 12theory Real 13imports Rat 14begin 15 16text \<open> 17 This theory contains a formalization of the real numbers as equivalence 18 classes of Cauchy sequences of rationals. See 19 \<^file>\<open>~~/src/HOL/ex/Dedekind_Real.thy\<close> for an alternative construction using 20 Dedekind cuts. 21\<close> 22 23 24subsection \<open>Preliminary lemmas\<close> 25 26text\<open>Useful in convergence arguments\<close> 27lemma inverse_of_nat_le: 28 fixes n::nat shows "\<lbrakk>n \<le> m; n\<noteq>0\<rbrakk> \<Longrightarrow> 1 / of_nat m \<le> (1::'a::linordered_field) / of_nat n" 29 by (simp add: frac_le) 30 31lemma inj_add_left [simp]: "inj ((+) x)" 32 for x :: "'a::cancel_semigroup_add" 33 by (meson add_left_imp_eq injI) 34 35lemma inj_mult_left [simp]: "inj (( * ) x) \<longleftrightarrow> x \<noteq> 0" 36 for x :: "'a::idom" 37 by (metis injI mult_cancel_left the_inv_f_f zero_neq_one) 38 39lemma add_diff_add: "(a + c) - (b + d) = (a - b) + (c - d)" 40 for a b c d :: "'a::ab_group_add" 41 by simp 42 43lemma minus_diff_minus: "- a - - b = - (a - b)" 44 for a b :: "'a::ab_group_add" 45 by simp 46 47lemma mult_diff_mult: "(x * y - a * b) = x * (y - b) + (x - a) * b" 48 for x y a b :: "'a::ring" 49 by (simp add: algebra_simps) 50 51lemma inverse_diff_inverse: 52 fixes a b :: "'a::division_ring" 53 assumes "a \<noteq> 0" and "b \<noteq> 0" 54 shows "inverse a - inverse b = - (inverse a * (a - b) * inverse b)" 55 using assms by (simp add: algebra_simps) 56 57lemma obtain_pos_sum: 58 fixes r :: rat assumes r: "0 < r" 59 obtains s t where "0 < s" and "0 < t" and "r = s + t" 60proof 61 from r show "0 < r/2" by simp 62 from r show "0 < r/2" by simp 63 show "r = r/2 + r/2" by simp 64qed 65 66 67subsection \<open>Sequences that converge to zero\<close> 68 69definition vanishes :: "(nat \<Rightarrow> rat) \<Rightarrow> bool" 70 where "vanishes X \<longleftrightarrow> (\<forall>r>0. \<exists>k. \<forall>n\<ge>k. \<bar>X n\<bar> < r)" 71 72lemma vanishesI: "(\<And>r. 0 < r \<Longrightarrow> \<exists>k. \<forall>n\<ge>k. \<bar>X n\<bar> < r) \<Longrightarrow> vanishes X" 73 unfolding vanishes_def by simp 74 75lemma vanishesD: "vanishes X \<Longrightarrow> 0 < r \<Longrightarrow> \<exists>k. \<forall>n\<ge>k. \<bar>X n\<bar> < r" 76 unfolding vanishes_def by simp 77 78lemma vanishes_const [simp]: "vanishes (\<lambda>n. c) \<longleftrightarrow> c = 0" 79proof (cases "c = 0") 80 case True 81 then show ?thesis 82 by (simp add: vanishesI) 83next 84 case False 85 then show ?thesis 86 unfolding vanishes_def 87 using zero_less_abs_iff by blast 88qed 89 90lemma vanishes_minus: "vanishes X \<Longrightarrow> vanishes (\<lambda>n. - X n)" 91 unfolding vanishes_def by simp 92 93lemma vanishes_add: 94 assumes X: "vanishes X" 95 and Y: "vanishes Y" 96 shows "vanishes (\<lambda>n. X n + Y n)" 97proof (rule vanishesI) 98 fix r :: rat 99 assume "0 < r" 100 then obtain s t where s: "0 < s" and t: "0 < t" and r: "r = s + t" 101 by (rule obtain_pos_sum) 102 obtain i where i: "\<forall>n\<ge>i. \<bar>X n\<bar> < s" 103 using vanishesD [OF X s] .. 104 obtain j where j: "\<forall>n\<ge>j. \<bar>Y n\<bar> < t" 105 using vanishesD [OF Y t] .. 106 have "\<forall>n\<ge>max i j. \<bar>X n + Y n\<bar> < r" 107 proof clarsimp 108 fix n 109 assume n: "i \<le> n" "j \<le> n" 110 have "\<bar>X n + Y n\<bar> \<le> \<bar>X n\<bar> + \<bar>Y n\<bar>" 111 by (rule abs_triangle_ineq) 112 also have "\<dots> < s + t" 113 by (simp add: add_strict_mono i j n) 114 finally show "\<bar>X n + Y n\<bar> < r" 115 by (simp only: r) 116 qed 117 then show "\<exists>k. \<forall>n\<ge>k. \<bar>X n + Y n\<bar> < r" .. 118qed 119 120lemma vanishes_diff: 121 assumes "vanishes X" "vanishes Y" 122 shows "vanishes (\<lambda>n. X n - Y n)" 123 unfolding diff_conv_add_uminus by (intro vanishes_add vanishes_minus assms) 124 125lemma vanishes_mult_bounded: 126 assumes X: "\<exists>a>0. \<forall>n. \<bar>X n\<bar> < a" 127 assumes Y: "vanishes (\<lambda>n. Y n)" 128 shows "vanishes (\<lambda>n. X n * Y n)" 129proof (rule vanishesI) 130 fix r :: rat 131 assume r: "0 < r" 132 obtain a where a: "0 < a" "\<forall>n. \<bar>X n\<bar> < a" 133 using X by blast 134 obtain b where b: "0 < b" "r = a * b" 135 proof 136 show "0 < r / a" using r a by simp 137 show "r = a * (r / a)" using a by simp 138 qed 139 obtain k where k: "\<forall>n\<ge>k. \<bar>Y n\<bar> < b" 140 using vanishesD [OF Y b(1)] .. 141 have "\<forall>n\<ge>k. \<bar>X n * Y n\<bar> < r" 142 by (simp add: b(2) abs_mult mult_strict_mono' a k) 143 then show "\<exists>k. \<forall>n\<ge>k. \<bar>X n * Y n\<bar> < r" .. 144qed 145 146 147subsection \<open>Cauchy sequences\<close> 148 149definition cauchy :: "(nat \<Rightarrow> rat) \<Rightarrow> bool" 150 where "cauchy X \<longleftrightarrow> (\<forall>r>0. \<exists>k. \<forall>m\<ge>k. \<forall>n\<ge>k. \<bar>X m - X n\<bar> < r)" 151 152lemma cauchyI: "(\<And>r. 0 < r \<Longrightarrow> \<exists>k. \<forall>m\<ge>k. \<forall>n\<ge>k. \<bar>X m - X n\<bar> < r) \<Longrightarrow> cauchy X" 153 unfolding cauchy_def by simp 154 155lemma cauchyD: "cauchy X \<Longrightarrow> 0 < r \<Longrightarrow> \<exists>k. \<forall>m\<ge>k. \<forall>n\<ge>k. \<bar>X m - X n\<bar> < r" 156 unfolding cauchy_def by simp 157 158lemma cauchy_const [simp]: "cauchy (\<lambda>n. x)" 159 unfolding cauchy_def by simp 160 161lemma cauchy_add [simp]: 162 assumes X: "cauchy X" and Y: "cauchy Y" 163 shows "cauchy (\<lambda>n. X n + Y n)" 164proof (rule cauchyI) 165 fix r :: rat 166 assume "0 < r" 167 then obtain s t where s: "0 < s" and t: "0 < t" and r: "r = s + t" 168 by (rule obtain_pos_sum) 169 obtain i where i: "\<forall>m\<ge>i. \<forall>n\<ge>i. \<bar>X m - X n\<bar> < s" 170 using cauchyD [OF X s] .. 171 obtain j where j: "\<forall>m\<ge>j. \<forall>n\<ge>j. \<bar>Y m - Y n\<bar> < t" 172 using cauchyD [OF Y t] .. 173 have "\<forall>m\<ge>max i j. \<forall>n\<ge>max i j. \<bar>(X m + Y m) - (X n + Y n)\<bar> < r" 174 proof clarsimp 175 fix m n 176 assume *: "i \<le> m" "j \<le> m" "i \<le> n" "j \<le> n" 177 have "\<bar>(X m + Y m) - (X n + Y n)\<bar> \<le> \<bar>X m - X n\<bar> + \<bar>Y m - Y n\<bar>" 178 unfolding add_diff_add by (rule abs_triangle_ineq) 179 also have "\<dots> < s + t" 180 by (rule add_strict_mono) (simp_all add: i j *) 181 finally show "\<bar>(X m + Y m) - (X n + Y n)\<bar> < r" by (simp only: r) 182 qed 183 then show "\<exists>k. \<forall>m\<ge>k. \<forall>n\<ge>k. \<bar>(X m + Y m) - (X n + Y n)\<bar> < r" .. 184qed 185 186lemma cauchy_minus [simp]: 187 assumes X: "cauchy X" 188 shows "cauchy (\<lambda>n. - X n)" 189 using assms unfolding cauchy_def 190 unfolding minus_diff_minus abs_minus_cancel . 191 192lemma cauchy_diff [simp]: 193 assumes "cauchy X" "cauchy Y" 194 shows "cauchy (\<lambda>n. X n - Y n)" 195 using assms unfolding diff_conv_add_uminus by (simp del: add_uminus_conv_diff) 196 197lemma cauchy_imp_bounded: 198 assumes "cauchy X" 199 shows "\<exists>b>0. \<forall>n. \<bar>X n\<bar> < b" 200proof - 201 obtain k where k: "\<forall>m\<ge>k. \<forall>n\<ge>k. \<bar>X m - X n\<bar> < 1" 202 using cauchyD [OF assms zero_less_one] .. 203 show "\<exists>b>0. \<forall>n. \<bar>X n\<bar> < b" 204 proof (intro exI conjI allI) 205 have "0 \<le> \<bar>X 0\<bar>" by simp 206 also have "\<bar>X 0\<bar> \<le> Max (abs ` X ` {..k})" by simp 207 finally have "0 \<le> Max (abs ` X ` {..k})" . 208 then show "0 < Max (abs ` X ` {..k}) + 1" by simp 209 next 210 fix n :: nat 211 show "\<bar>X n\<bar> < Max (abs ` X ` {..k}) + 1" 212 proof (rule linorder_le_cases) 213 assume "n \<le> k" 214 then have "\<bar>X n\<bar> \<le> Max (abs ` X ` {..k})" by simp 215 then show "\<bar>X n\<bar> < Max (abs ` X ` {..k}) + 1" by simp 216 next 217 assume "k \<le> n" 218 have "\<bar>X n\<bar> = \<bar>X k + (X n - X k)\<bar>" by simp 219 also have "\<bar>X k + (X n - X k)\<bar> \<le> \<bar>X k\<bar> + \<bar>X n - X k\<bar>" 220 by (rule abs_triangle_ineq) 221 also have "\<dots> < Max (abs ` X ` {..k}) + 1" 222 by (rule add_le_less_mono) (simp_all add: k \<open>k \<le> n\<close>) 223 finally show "\<bar>X n\<bar> < Max (abs ` X ` {..k}) + 1" . 224 qed 225 qed 226qed 227 228lemma cauchy_mult [simp]: 229 assumes X: "cauchy X" and Y: "cauchy Y" 230 shows "cauchy (\<lambda>n. X n * Y n)" 231proof (rule cauchyI) 232 fix r :: rat assume "0 < r" 233 then obtain u v where u: "0 < u" and v: "0 < v" and "r = u + v" 234 by (rule obtain_pos_sum) 235 obtain a where a: "0 < a" "\<forall>n. \<bar>X n\<bar> < a" 236 using cauchy_imp_bounded [OF X] by blast 237 obtain b where b: "0 < b" "\<forall>n. \<bar>Y n\<bar> < b" 238 using cauchy_imp_bounded [OF Y] by blast 239 obtain s t where s: "0 < s" and t: "0 < t" and r: "r = a * t + s * b" 240 proof 241 show "0 < v/b" using v b(1) by simp 242 show "0 < u/a" using u a(1) by simp 243 show "r = a * (u/a) + (v/b) * b" 244 using a(1) b(1) \<open>r = u + v\<close> by simp 245 qed 246 obtain i where i: "\<forall>m\<ge>i. \<forall>n\<ge>i. \<bar>X m - X n\<bar> < s" 247 using cauchyD [OF X s] .. 248 obtain j where j: "\<forall>m\<ge>j. \<forall>n\<ge>j. \<bar>Y m - Y n\<bar> < t" 249 using cauchyD [OF Y t] .. 250 have "\<forall>m\<ge>max i j. \<forall>n\<ge>max i j. \<bar>X m * Y m - X n * Y n\<bar> < r" 251 proof clarsimp 252 fix m n 253 assume *: "i \<le> m" "j \<le> m" "i \<le> n" "j \<le> n" 254 have "\<bar>X m * Y m - X n * Y n\<bar> = \<bar>X m * (Y m - Y n) + (X m - X n) * Y n\<bar>" 255 unfolding mult_diff_mult .. 256 also have "\<dots> \<le> \<bar>X m * (Y m - Y n)\<bar> + \<bar>(X m - X n) * Y n\<bar>" 257 by (rule abs_triangle_ineq) 258 also have "\<dots> = \<bar>X m\<bar> * \<bar>Y m - Y n\<bar> + \<bar>X m - X n\<bar> * \<bar>Y n\<bar>" 259 unfolding abs_mult .. 260 also have "\<dots> < a * t + s * b" 261 by (simp_all add: add_strict_mono mult_strict_mono' a b i j *) 262 finally show "\<bar>X m * Y m - X n * Y n\<bar> < r" 263 by (simp only: r) 264 qed 265 then show "\<exists>k. \<forall>m\<ge>k. \<forall>n\<ge>k. \<bar>X m * Y m - X n * Y n\<bar> < r" .. 266qed 267 268lemma cauchy_not_vanishes_cases: 269 assumes X: "cauchy X" 270 assumes nz: "\<not> vanishes X" 271 shows "\<exists>b>0. \<exists>k. (\<forall>n\<ge>k. b < - X n) \<or> (\<forall>n\<ge>k. b < X n)" 272proof - 273 obtain r where "0 < r" and r: "\<forall>k. \<exists>n\<ge>k. r \<le> \<bar>X n\<bar>" 274 using nz unfolding vanishes_def by (auto simp add: not_less) 275 obtain s t where s: "0 < s" and t: "0 < t" and "r = s + t" 276 using \<open>0 < r\<close> by (rule obtain_pos_sum) 277 obtain i where i: "\<forall>m\<ge>i. \<forall>n\<ge>i. \<bar>X m - X n\<bar> < s" 278 using cauchyD [OF X s] .. 279 obtain k where "i \<le> k" and "r \<le> \<bar>X k\<bar>" 280 using r by blast 281 have k: "\<forall>n\<ge>k. \<bar>X n - X k\<bar> < s" 282 using i \<open>i \<le> k\<close> by auto 283 have "X k \<le> - r \<or> r \<le> X k" 284 using \<open>r \<le> \<bar>X k\<bar>\<close> by auto 285 then have "(\<forall>n\<ge>k. t < - X n) \<or> (\<forall>n\<ge>k. t < X n)" 286 unfolding \<open>r = s + t\<close> using k by auto 287 then have "\<exists>k. (\<forall>n\<ge>k. t < - X n) \<or> (\<forall>n\<ge>k. t < X n)" .. 288 then show "\<exists>t>0. \<exists>k. (\<forall>n\<ge>k. t < - X n) \<or> (\<forall>n\<ge>k. t < X n)" 289 using t by auto 290qed 291 292lemma cauchy_not_vanishes: 293 assumes X: "cauchy X" 294 and nz: "\<not> vanishes X" 295 shows "\<exists>b>0. \<exists>k. \<forall>n\<ge>k. b < \<bar>X n\<bar>" 296 using cauchy_not_vanishes_cases [OF assms] 297 by (elim ex_forward conj_forward asm_rl) auto 298 299lemma cauchy_inverse [simp]: 300 assumes X: "cauchy X" 301 and nz: "\<not> vanishes X" 302 shows "cauchy (\<lambda>n. inverse (X n))" 303proof (rule cauchyI) 304 fix r :: rat 305 assume "0 < r" 306 obtain b i where b: "0 < b" and i: "\<forall>n\<ge>i. b < \<bar>X n\<bar>" 307 using cauchy_not_vanishes [OF X nz] by blast 308 from b i have nz: "\<forall>n\<ge>i. X n \<noteq> 0" by auto 309 obtain s where s: "0 < s" and r: "r = inverse b * s * inverse b" 310 proof 311 show "0 < b * r * b" by (simp add: \<open>0 < r\<close> b) 312 show "r = inverse b * (b * r * b) * inverse b" 313 using b by simp 314 qed 315 obtain j where j: "\<forall>m\<ge>j. \<forall>n\<ge>j. \<bar>X m - X n\<bar> < s" 316 using cauchyD [OF X s] .. 317 have "\<forall>m\<ge>max i j. \<forall>n\<ge>max i j. \<bar>inverse (X m) - inverse (X n)\<bar> < r" 318 proof clarsimp 319 fix m n 320 assume *: "i \<le> m" "j \<le> m" "i \<le> n" "j \<le> n" 321 have "\<bar>inverse (X m) - inverse (X n)\<bar> = inverse \<bar>X m\<bar> * \<bar>X m - X n\<bar> * inverse \<bar>X n\<bar>" 322 by (simp add: inverse_diff_inverse nz * abs_mult) 323 also have "\<dots> < inverse b * s * inverse b" 324 by (simp add: mult_strict_mono less_imp_inverse_less i j b * s) 325 finally show "\<bar>inverse (X m) - inverse (X n)\<bar> < r" by (simp only: r) 326 qed 327 then show "\<exists>k. \<forall>m\<ge>k. \<forall>n\<ge>k. \<bar>inverse (X m) - inverse (X n)\<bar> < r" .. 328qed 329 330lemma vanishes_diff_inverse: 331 assumes X: "cauchy X" "\<not> vanishes X" 332 and Y: "cauchy Y" "\<not> vanishes Y" 333 and XY: "vanishes (\<lambda>n. X n - Y n)" 334 shows "vanishes (\<lambda>n. inverse (X n) - inverse (Y n))" 335proof (rule vanishesI) 336 fix r :: rat 337 assume r: "0 < r" 338 obtain a i where a: "0 < a" and i: "\<forall>n\<ge>i. a < \<bar>X n\<bar>" 339 using cauchy_not_vanishes [OF X] by blast 340 obtain b j where b: "0 < b" and j: "\<forall>n\<ge>j. b < \<bar>Y n\<bar>" 341 using cauchy_not_vanishes [OF Y] by blast 342 obtain s where s: "0 < s" and "inverse a * s * inverse b = r" 343 proof 344 show "0 < a * r * b" 345 using a r b by simp 346 show "inverse a * (a * r * b) * inverse b = r" 347 using a r b by simp 348 qed 349 obtain k where k: "\<forall>n\<ge>k. \<bar>X n - Y n\<bar> < s" 350 using vanishesD [OF XY s] .. 351 have "\<forall>n\<ge>max (max i j) k. \<bar>inverse (X n) - inverse (Y n)\<bar> < r" 352 proof clarsimp 353 fix n 354 assume n: "i \<le> n" "j \<le> n" "k \<le> n" 355 with i j a b have "X n \<noteq> 0" and "Y n \<noteq> 0" 356 by auto 357 then have "\<bar>inverse (X n) - inverse (Y n)\<bar> = inverse \<bar>X n\<bar> * \<bar>X n - Y n\<bar> * inverse \<bar>Y n\<bar>" 358 by (simp add: inverse_diff_inverse abs_mult) 359 also have "\<dots> < inverse a * s * inverse b" 360 by (intro mult_strict_mono' less_imp_inverse_less) (simp_all add: a b i j k n) 361 also note \<open>inverse a * s * inverse b = r\<close> 362 finally show "\<bar>inverse (X n) - inverse (Y n)\<bar> < r" . 363 qed 364 then show "\<exists>k. \<forall>n\<ge>k. \<bar>inverse (X n) - inverse (Y n)\<bar> < r" .. 365qed 366 367 368subsection \<open>Equivalence relation on Cauchy sequences\<close> 369 370definition realrel :: "(nat \<Rightarrow> rat) \<Rightarrow> (nat \<Rightarrow> rat) \<Rightarrow> bool" 371 where "realrel = (\<lambda>X Y. cauchy X \<and> cauchy Y \<and> vanishes (\<lambda>n. X n - Y n))" 372 373lemma realrelI [intro?]: "cauchy X \<Longrightarrow> cauchy Y \<Longrightarrow> vanishes (\<lambda>n. X n - Y n) \<Longrightarrow> realrel X Y" 374 by (simp add: realrel_def) 375 376lemma realrel_refl: "cauchy X \<Longrightarrow> realrel X X" 377 by (simp add: realrel_def) 378 379lemma symp_realrel: "symp realrel" 380 by (simp add: abs_minus_commute realrel_def symp_def vanishes_def) 381 382lemma transp_realrel: "transp realrel" 383 unfolding realrel_def 384 by (rule transpI) (force simp add: dest: vanishes_add) 385 386lemma part_equivp_realrel: "part_equivp realrel" 387 by (blast intro: part_equivpI symp_realrel transp_realrel realrel_refl cauchy_const) 388 389 390subsection \<open>The field of real numbers\<close> 391 392quotient_type real = "nat \<Rightarrow> rat" / partial: realrel 393 morphisms rep_real Real 394 by (rule part_equivp_realrel) 395 396lemma cr_real_eq: "pcr_real = (\<lambda>x y. cauchy x \<and> Real x = y)" 397 unfolding real.pcr_cr_eq cr_real_def realrel_def by auto 398 399lemma Real_induct [induct type: real]: (* TODO: generate automatically *) 400 assumes "\<And>X. cauchy X \<Longrightarrow> P (Real X)" 401 shows "P x" 402proof (induct x) 403 case (1 X) 404 then have "cauchy X" by (simp add: realrel_def) 405 then show "P (Real X)" by (rule assms) 406qed 407 408lemma eq_Real: "cauchy X \<Longrightarrow> cauchy Y \<Longrightarrow> Real X = Real Y \<longleftrightarrow> vanishes (\<lambda>n. X n - Y n)" 409 using real.rel_eq_transfer 410 unfolding real.pcr_cr_eq cr_real_def rel_fun_def realrel_def by simp 411 412lemma Domainp_pcr_real [transfer_domain_rule]: "Domainp pcr_real = cauchy" 413 by (simp add: real.domain_eq realrel_def) 414 415instantiation real :: field 416begin 417 418lift_definition zero_real :: "real" is "\<lambda>n. 0" 419 by (simp add: realrel_refl) 420 421lift_definition one_real :: "real" is "\<lambda>n. 1" 422 by (simp add: realrel_refl) 423 424lift_definition plus_real :: "real \<Rightarrow> real \<Rightarrow> real" is "\<lambda>X Y n. X n + Y n" 425 unfolding realrel_def add_diff_add 426 by (simp only: cauchy_add vanishes_add simp_thms) 427 428lift_definition uminus_real :: "real \<Rightarrow> real" is "\<lambda>X n. - X n" 429 unfolding realrel_def minus_diff_minus 430 by (simp only: cauchy_minus vanishes_minus simp_thms) 431 432lift_definition times_real :: "real \<Rightarrow> real \<Rightarrow> real" is "\<lambda>X Y n. X n * Y n" 433proof - 434 fix f1 f2 f3 f4 435 have "\<lbrakk>cauchy f1; cauchy f4; vanishes (\<lambda>n. f1 n - f2 n); vanishes (\<lambda>n. f3 n - f4 n)\<rbrakk> 436 \<Longrightarrow> vanishes (\<lambda>n. f1 n * (f3 n - f4 n) + f4 n * (f1 n - f2 n))" 437 by (simp add: vanishes_add vanishes_mult_bounded cauchy_imp_bounded) 438 then show "\<lbrakk>realrel f1 f2; realrel f3 f4\<rbrakk> \<Longrightarrow> realrel (\<lambda>n. f1 n * f3 n) (\<lambda>n. f2 n * f4 n)" 439 by (simp add: mult.commute realrel_def mult_diff_mult) 440qed 441 442lift_definition inverse_real :: "real \<Rightarrow> real" 443 is "\<lambda>X. if vanishes X then (\<lambda>n. 0) else (\<lambda>n. inverse (X n))" 444proof - 445 fix X Y 446 assume "realrel X Y" 447 then have X: "cauchy X" and Y: "cauchy Y" and XY: "vanishes (\<lambda>n. X n - Y n)" 448 by (simp_all add: realrel_def) 449 have "vanishes X \<longleftrightarrow> vanishes Y" 450 proof 451 assume "vanishes X" 452 from vanishes_diff [OF this XY] show "vanishes Y" 453 by simp 454 next 455 assume "vanishes Y" 456 from vanishes_add [OF this XY] show "vanishes X" 457 by simp 458 qed 459 then show "?thesis X Y" 460 by (simp add: vanishes_diff_inverse X Y XY realrel_def) 461qed 462 463definition "x - y = x + - y" for x y :: real 464 465definition "x div y = x * inverse y" for x y :: real 466 467lemma add_Real: "cauchy X \<Longrightarrow> cauchy Y \<Longrightarrow> Real X + Real Y = Real (\<lambda>n. X n + Y n)" 468 using plus_real.transfer by (simp add: cr_real_eq rel_fun_def) 469 470lemma minus_Real: "cauchy X \<Longrightarrow> - Real X = Real (\<lambda>n. - X n)" 471 using uminus_real.transfer by (simp add: cr_real_eq rel_fun_def) 472 473lemma diff_Real: "cauchy X \<Longrightarrow> cauchy Y \<Longrightarrow> Real X - Real Y = Real (\<lambda>n. X n - Y n)" 474 by (simp add: minus_Real add_Real minus_real_def) 475 476lemma mult_Real: "cauchy X \<Longrightarrow> cauchy Y \<Longrightarrow> Real X * Real Y = Real (\<lambda>n. X n * Y n)" 477 using times_real.transfer by (simp add: cr_real_eq rel_fun_def) 478 479lemma inverse_Real: 480 "cauchy X \<Longrightarrow> inverse (Real X) = (if vanishes X then 0 else Real (\<lambda>n. inverse (X n)))" 481 using inverse_real.transfer zero_real.transfer 482 unfolding cr_real_eq rel_fun_def by (simp split: if_split_asm, metis) 483 484instance 485proof 486 fix a b c :: real 487 show "a + b = b + a" 488 by transfer (simp add: ac_simps realrel_def) 489 show "(a + b) + c = a + (b + c)" 490 by transfer (simp add: ac_simps realrel_def) 491 show "0 + a = a" 492 by transfer (simp add: realrel_def) 493 show "- a + a = 0" 494 by transfer (simp add: realrel_def) 495 show "a - b = a + - b" 496 by (rule minus_real_def) 497 show "(a * b) * c = a * (b * c)" 498 by transfer (simp add: ac_simps realrel_def) 499 show "a * b = b * a" 500 by transfer (simp add: ac_simps realrel_def) 501 show "1 * a = a" 502 by transfer (simp add: ac_simps realrel_def) 503 show "(a + b) * c = a * c + b * c" 504 by transfer (simp add: distrib_right realrel_def) 505 show "(0::real) \<noteq> (1::real)" 506 by transfer (simp add: realrel_def) 507 have "vanishes (\<lambda>n. inverse (X n) * X n - 1)" if X: "cauchy X" "\<not> vanishes X" for X 508 proof (rule vanishesI) 509 fix r::rat 510 assume "0 < r" 511 obtain b k where "b>0" "\<forall>n\<ge>k. b < \<bar>X n\<bar>" 512 using X cauchy_not_vanishes by blast 513 then show "\<exists>k. \<forall>n\<ge>k. \<bar>inverse (X n) * X n - 1\<bar> < r" 514 using \<open>0 < r\<close> by force 515 qed 516 then show "a \<noteq> 0 \<Longrightarrow> inverse a * a = 1" 517 by transfer (simp add: realrel_def) 518 show "a div b = a * inverse b" 519 by (rule divide_real_def) 520 show "inverse (0::real) = 0" 521 by transfer (simp add: realrel_def) 522qed 523 524end 525 526 527subsection \<open>Positive reals\<close> 528 529lift_definition positive :: "real \<Rightarrow> bool" 530 is "\<lambda>X. \<exists>r>0. \<exists>k. \<forall>n\<ge>k. r < X n" 531proof - 532 have 1: "\<exists>r>0. \<exists>k. \<forall>n\<ge>k. r < Y n" 533 if *: "realrel X Y" and **: "\<exists>r>0. \<exists>k. \<forall>n\<ge>k. r < X n" for X Y 534 proof - 535 from * have XY: "vanishes (\<lambda>n. X n - Y n)" 536 by (simp_all add: realrel_def) 537 from ** obtain r i where "0 < r" and i: "\<forall>n\<ge>i. r < X n" 538 by blast 539 obtain s t where s: "0 < s" and t: "0 < t" and r: "r = s + t" 540 using \<open>0 < r\<close> by (rule obtain_pos_sum) 541 obtain j where j: "\<forall>n\<ge>j. \<bar>X n - Y n\<bar> < s" 542 using vanishesD [OF XY s] .. 543 have "\<forall>n\<ge>max i j. t < Y n" 544 proof clarsimp 545 fix n 546 assume n: "i \<le> n" "j \<le> n" 547 have "\<bar>X n - Y n\<bar> < s" and "r < X n" 548 using i j n by simp_all 549 then show "t < Y n" by (simp add: r) 550 qed 551 then show ?thesis using t by blast 552 qed 553 fix X Y assume "realrel X Y" 554 then have "realrel X Y" and "realrel Y X" 555 using symp_realrel by (auto simp: symp_def) 556 then show "?thesis X Y" 557 by (safe elim!: 1) 558qed 559 560lemma positive_Real: "cauchy X \<Longrightarrow> positive (Real X) \<longleftrightarrow> (\<exists>r>0. \<exists>k. \<forall>n\<ge>k. r < X n)" 561 using positive.transfer by (simp add: cr_real_eq rel_fun_def) 562 563lemma positive_zero: "\<not> positive 0" 564 by transfer auto 565 566lemma positive_add: 567 assumes "positive x" "positive y" shows "positive (x + y)" 568proof - 569 have *: "\<lbrakk>\<forall>n\<ge>i. a < x n; \<forall>n\<ge>j. b < y n; 0 < a; 0 < b; n \<ge> max i j\<rbrakk> 570 \<Longrightarrow> a+b < x n + y n" for x y and a b::rat and i j n::nat 571 by (simp add: add_strict_mono) 572 show ?thesis 573 using assms 574 by transfer (blast intro: * pos_add_strict) 575qed 576 577lemma positive_mult: 578 assumes "positive x" "positive y" shows "positive (x * y)" 579proof - 580 have *: "\<lbrakk>\<forall>n\<ge>i. a < x n; \<forall>n\<ge>j. b < y n; 0 < a; 0 < b; n \<ge> max i j\<rbrakk> 581 \<Longrightarrow> a*b < x n * y n" for x y and a b::rat and i j n::nat 582 by (simp add: mult_strict_mono') 583 show ?thesis 584 using assms 585 by transfer (blast intro: * mult_pos_pos) 586qed 587 588lemma positive_minus: "\<not> positive x \<Longrightarrow> x \<noteq> 0 \<Longrightarrow> positive (- x)" 589 apply transfer 590 apply (simp add: realrel_def) 591 apply (blast dest: cauchy_not_vanishes_cases) 592 done 593 594instantiation real :: linordered_field 595begin 596 597definition "x < y \<longleftrightarrow> positive (y - x)" 598 599definition "x \<le> y \<longleftrightarrow> x < y \<or> x = y" for x y :: real 600 601definition "\<bar>a\<bar> = (if a < 0 then - a else a)" for a :: real 602 603definition "sgn a = (if a = 0 then 0 else if 0 < a then 1 else - 1)" for a :: real 604 605instance 606proof 607 fix a b c :: real 608 show "\<bar>a\<bar> = (if a < 0 then - a else a)" 609 by (rule abs_real_def) 610 show "a < b \<longleftrightarrow> a \<le> b \<and> \<not> b \<le> a" 611 "a \<le> b \<Longrightarrow> b \<le> c \<Longrightarrow> a \<le> c" "a \<le> a" 612 "a \<le> b \<Longrightarrow> b \<le> a \<Longrightarrow> a = b" 613 "a \<le> b \<Longrightarrow> c + a \<le> c + b" 614 unfolding less_eq_real_def less_real_def 615 by (force simp add: positive_zero dest: positive_add)+ 616 show "sgn a = (if a = 0 then 0 else if 0 < a then 1 else - 1)" 617 by (rule sgn_real_def) 618 show "a \<le> b \<or> b \<le> a" 619 by (auto dest!: positive_minus simp: less_eq_real_def less_real_def) 620 show "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b" 621 unfolding less_real_def 622 by (force simp add: algebra_simps dest: positive_mult) 623qed 624 625end 626 627instantiation real :: distrib_lattice 628begin 629 630definition "(inf :: real \<Rightarrow> real \<Rightarrow> real) = min" 631 632definition "(sup :: real \<Rightarrow> real \<Rightarrow> real) = max" 633 634instance 635 by standard (auto simp add: inf_real_def sup_real_def max_min_distrib2) 636 637end 638 639lemma of_nat_Real: "of_nat x = Real (\<lambda>n. of_nat x)" 640 by (induct x) (simp_all add: zero_real_def one_real_def add_Real) 641 642lemma of_int_Real: "of_int x = Real (\<lambda>n. of_int x)" 643 by (cases x rule: int_diff_cases) (simp add: of_nat_Real diff_Real) 644 645lemma of_rat_Real: "of_rat x = Real (\<lambda>n. x)" 646proof (induct x) 647 case (Fract a b) 648 then show ?case 649 apply (simp add: Fract_of_int_quotient of_rat_divide) 650 apply (simp add: of_int_Real divide_inverse inverse_Real mult_Real) 651 done 652qed 653 654instance real :: archimedean_field 655proof 656 show "\<exists>z. x \<le> of_int z" for x :: real 657 proof (induct x) 658 case (1 X) 659 then obtain b where "0 < b" and b: "\<And>n. \<bar>X n\<bar> < b" 660 by (blast dest: cauchy_imp_bounded) 661 then have "Real X < of_int (\<lceil>b\<rceil> + 1)" 662 using 1 663 apply (simp add: of_int_Real less_real_def diff_Real positive_Real) 664 apply (rule_tac x=1 in exI) 665 apply (simp add: algebra_simps) 666 by (metis abs_ge_self le_less_trans le_of_int_ceiling less_le) 667 then show ?case 668 using less_eq_real_def by blast 669 qed 670qed 671 672instantiation real :: floor_ceiling 673begin 674 675definition [code del]: "\<lfloor>x::real\<rfloor> = (THE z. of_int z \<le> x \<and> x < of_int (z + 1))" 676 677instance 678proof 679 show "of_int \<lfloor>x\<rfloor> \<le> x \<and> x < of_int (\<lfloor>x\<rfloor> + 1)" for x :: real 680 unfolding floor_real_def using floor_exists1 by (rule theI') 681qed 682 683end 684 685 686subsection \<open>Completeness\<close> 687 688lemma not_positive_Real: 689 assumes "cauchy X" shows "\<not> positive (Real X) \<longleftrightarrow> (\<forall>r>0. \<exists>k. \<forall>n\<ge>k. X n \<le> r)" (is "?lhs = ?rhs") 690 unfolding positive_Real [OF assms] 691proof (intro iffI allI notI impI) 692 show "\<exists>k. \<forall>n\<ge>k. X n \<le> r" if r: "\<not> (\<exists>r>0. \<exists>k. \<forall>n\<ge>k. r < X n)" and "0 < r" for r 693 proof - 694 obtain s t where "s > 0" "t > 0" "r = s+t" 695 using \<open>r > 0\<close> obtain_pos_sum by blast 696 obtain k where k: "\<And>m n. \<lbrakk>m\<ge>k; n\<ge>k\<rbrakk> \<Longrightarrow> \<bar>X m - X n\<bar> < t" 697 using cauchyD [OF assms \<open>t > 0\<close>] by blast 698 obtain n where "n \<ge> k" "X n \<le> s" 699 by (meson r \<open>0 < s\<close> not_less) 700 then have "X l \<le> r" if "l \<ge> n" for l 701 using k [OF \<open>n \<ge> k\<close>, of l] that \<open>r = s+t\<close> by linarith 702 then show ?thesis 703 by blast 704 qed 705qed (meson le_cases not_le) 706 707lemma le_Real: 708 assumes "cauchy X" "cauchy Y" 709 shows "Real X \<le> Real Y = (\<forall>r>0. \<exists>k. \<forall>n\<ge>k. X n \<le> Y n + r)" 710 unfolding not_less [symmetric, where 'a=real] less_real_def 711 apply (simp add: diff_Real not_positive_Real assms) 712 apply (simp add: diff_le_eq ac_simps) 713 done 714 715lemma le_RealI: 716 assumes Y: "cauchy Y" 717 shows "\<forall>n. x \<le> of_rat (Y n) \<Longrightarrow> x \<le> Real Y" 718proof (induct x) 719 fix X 720 assume X: "cauchy X" and "\<forall>n. Real X \<le> of_rat (Y n)" 721 then have le: "\<And>m r. 0 < r \<Longrightarrow> \<exists>k. \<forall>n\<ge>k. X n \<le> Y m + r" 722 by (simp add: of_rat_Real le_Real) 723 then have "\<exists>k. \<forall>n\<ge>k. X n \<le> Y n + r" if "0 < r" for r :: rat 724 proof - 725 from that obtain s t where s: "0 < s" and t: "0 < t" and r: "r = s + t" 726 by (rule obtain_pos_sum) 727 obtain i where i: "\<forall>m\<ge>i. \<forall>n\<ge>i. \<bar>Y m - Y n\<bar> < s" 728 using cauchyD [OF Y s] .. 729 obtain j where j: "\<forall>n\<ge>j. X n \<le> Y i + t" 730 using le [OF t] .. 731 have "\<forall>n\<ge>max i j. X n \<le> Y n + r" 732 proof clarsimp 733 fix n 734 assume n: "i \<le> n" "j \<le> n" 735 have "X n \<le> Y i + t" 736 using n j by simp 737 moreover have "\<bar>Y i - Y n\<bar> < s" 738 using n i by simp 739 ultimately show "X n \<le> Y n + r" 740 unfolding r by simp 741 qed 742 then show ?thesis .. 743 qed 744 then show "Real X \<le> Real Y" 745 by (simp add: of_rat_Real le_Real X Y) 746qed 747 748lemma Real_leI: 749 assumes X: "cauchy X" 750 assumes le: "\<forall>n. of_rat (X n) \<le> y" 751 shows "Real X \<le> y" 752proof - 753 have "- y \<le> - Real X" 754 by (simp add: minus_Real X le_RealI of_rat_minus le) 755 then show ?thesis by simp 756qed 757 758lemma less_RealD: 759 assumes "cauchy Y" 760 shows "x < Real Y \<Longrightarrow> \<exists>n. x < of_rat (Y n)" 761 apply (erule contrapos_pp) 762 apply (simp add: not_less) 763 apply (erule Real_leI [OF assms]) 764 done 765 766lemma of_nat_less_two_power [simp]: "of_nat n < (2::'a::linordered_idom) ^ n" 767 apply (induct n) 768 apply simp 769 apply (metis add_le_less_mono mult_2 of_nat_Suc one_le_numeral one_le_power power_Suc) 770 done 771 772lemma complete_real: 773 fixes S :: "real set" 774 assumes "\<exists>x. x \<in> S" and "\<exists>z. \<forall>x\<in>S. x \<le> z" 775 shows "\<exists>y. (\<forall>x\<in>S. x \<le> y) \<and> (\<forall>z. (\<forall>x\<in>S. x \<le> z) \<longrightarrow> y \<le> z)" 776proof - 777 obtain x where x: "x \<in> S" using assms(1) .. 778 obtain z where z: "\<forall>x\<in>S. x \<le> z" using assms(2) .. 779 780 define P where "P x \<longleftrightarrow> (\<forall>y\<in>S. y \<le> of_rat x)" for x 781 obtain a where a: "\<not> P a" 782 proof 783 have "of_int \<lfloor>x - 1\<rfloor> \<le> x - 1" by (rule of_int_floor_le) 784 also have "x - 1 < x" by simp 785 finally have "of_int \<lfloor>x - 1\<rfloor> < x" . 786 then have "\<not> x \<le> of_int \<lfloor>x - 1\<rfloor>" by (simp only: not_le) 787 then show "\<not> P (of_int \<lfloor>x - 1\<rfloor>)" 788 unfolding P_def of_rat_of_int_eq using x by blast 789 qed 790 obtain b where b: "P b" 791 proof 792 show "P (of_int \<lceil>z\<rceil>)" 793 unfolding P_def of_rat_of_int_eq 794 proof 795 fix y assume "y \<in> S" 796 then have "y \<le> z" using z by simp 797 also have "z \<le> of_int \<lceil>z\<rceil>" by (rule le_of_int_ceiling) 798 finally show "y \<le> of_int \<lceil>z\<rceil>" . 799 qed 800 qed 801 802 define avg where "avg x y = x/2 + y/2" for x y :: rat 803 define bisect where "bisect = (\<lambda>(x, y). if P (avg x y) then (x, avg x y) else (avg x y, y))" 804 define A where "A n = fst ((bisect ^^ n) (a, b))" for n 805 define B where "B n = snd ((bisect ^^ n) (a, b))" for n 806 define C where "C n = avg (A n) (B n)" for n 807 have A_0 [simp]: "A 0 = a" unfolding A_def by simp 808 have B_0 [simp]: "B 0 = b" unfolding B_def by simp 809 have A_Suc [simp]: "\<And>n. A (Suc n) = (if P (C n) then A n else C n)" 810 unfolding A_def B_def C_def bisect_def split_def by simp 811 have B_Suc [simp]: "\<And>n. B (Suc n) = (if P (C n) then C n else B n)" 812 unfolding A_def B_def C_def bisect_def split_def by simp 813 814 have width: "B n - A n = (b - a) / 2^n" for n 815 proof (induct n) 816 case (Suc n) 817 then show ?case 818 by (simp add: C_def eq_divide_eq avg_def algebra_simps) 819 qed simp 820 have twos: "\<exists>n. y / 2 ^ n < r" if "0 < r" for y r :: rat 821 proof - 822 obtain n where "y / r < rat_of_nat n" 823 using \<open>0 < r\<close> reals_Archimedean2 by blast 824 then have "\<exists>n. y < r * 2 ^ n" 825 by (metis divide_less_eq less_trans mult.commute of_nat_less_two_power that) 826 then show ?thesis 827 by (simp add: divide_simps) 828 qed 829 have PA: "\<not> P (A n)" for n 830 by (induct n) (simp_all add: a) 831 have PB: "P (B n)" for n 832 by (induct n) (simp_all add: b) 833 have ab: "a < b" 834 using a b unfolding P_def 835 by (meson leI less_le_trans of_rat_less) 836 have AB: "A n < B n" for n 837 by (induct n) (simp_all add: ab C_def avg_def) 838 have "A i \<le> A j \<and> B j \<le> B i" if "i < j" for i j 839 using that 840 proof (induction rule: less_Suc_induct) 841 case (1 i) 842 then show ?case 843 apply (clarsimp simp add: C_def avg_def add_divide_distrib [symmetric]) 844 apply (rule AB [THEN less_imp_le]) 845 done 846 qed simp 847 then have A_mono: "A i \<le> A j" and B_mono: "B j \<le> B i" if "i \<le> j" for i j 848 by (metis eq_refl le_neq_implies_less that)+ 849 have cauchy_lemma: "cauchy X" if *: "\<And>n i. i\<ge>n \<Longrightarrow> A n \<le> X i \<and> X i \<le> B n" for X 850 proof (rule cauchyI) 851 fix r::rat 852 assume "0 < r" 853 then obtain k where k: "(b - a) / 2 ^ k < r" 854 using twos by blast 855 have "\<bar>X m - X n\<bar> < r" if "m\<ge>k" "n\<ge>k" for m n 856 proof - 857 have "\<bar>X m - X n\<bar> \<le> B k - A k" 858 by (simp add: * abs_rat_def diff_mono that) 859 also have "... < r" 860 by (simp add: k width) 861 finally show ?thesis . 862 qed 863 then show "\<exists>k. \<forall>m\<ge>k. \<forall>n\<ge>k. \<bar>X m - X n\<bar> < r" 864 by blast 865 qed 866 have "cauchy A" 867 by (rule cauchy_lemma) (meson AB A_mono B_mono dual_order.strict_implies_order less_le_trans) 868 have "cauchy B" 869 by (rule cauchy_lemma) (meson AB A_mono B_mono dual_order.strict_implies_order le_less_trans) 870 have "\<forall>x\<in>S. x \<le> Real B" 871 proof 872 fix x 873 assume "x \<in> S" 874 then show "x \<le> Real B" 875 using PB [unfolded P_def] \<open>cauchy B\<close> 876 by (simp add: le_RealI) 877 qed 878 moreover have "\<forall>z. (\<forall>x\<in>S. x \<le> z) \<longrightarrow> Real A \<le> z" 879 by (meson PA Real_leI P_def \<open>cauchy A\<close> le_cases order.trans) 880 moreover have "vanishes (\<lambda>n. (b - a) / 2 ^ n)" 881 proof (rule vanishesI) 882 fix r :: rat 883 assume "0 < r" 884 then obtain k where k: "\<bar>b - a\<bar> / 2 ^ k < r" 885 using twos by blast 886 have "\<forall>n\<ge>k. \<bar>(b - a) / 2 ^ n\<bar> < r" 887 proof clarify 888 fix n 889 assume n: "k \<le> n" 890 have "\<bar>(b - a) / 2 ^ n\<bar> = \<bar>b - a\<bar> / 2 ^ n" 891 by simp 892 also have "\<dots> \<le> \<bar>b - a\<bar> / 2 ^ k" 893 using n by (simp add: divide_left_mono) 894 also note k 895 finally show "\<bar>(b - a) / 2 ^ n\<bar> < r" . 896 qed 897 then show "\<exists>k. \<forall>n\<ge>k. \<bar>(b - a) / 2 ^ n\<bar> < r" .. 898 qed 899 then have "Real B = Real A" 900 by (simp add: eq_Real \<open>cauchy A\<close> \<open>cauchy B\<close> width) 901 ultimately show "\<exists>y. (\<forall>x\<in>S. x \<le> y) \<and> (\<forall>z. (\<forall>x\<in>S. x \<le> z) \<longrightarrow> y \<le> z)" 902 by force 903qed 904 905instantiation real :: linear_continuum 906begin 907 908subsection \<open>Supremum of a set of reals\<close> 909 910definition "Sup X = (LEAST z::real. \<forall>x\<in>X. x \<le> z)" 911definition "Inf X = - Sup (uminus ` X)" for X :: "real set" 912 913instance 914proof 915 show Sup_upper: "x \<le> Sup X" 916 if "x \<in> X" "bdd_above X" 917 for x :: real and X :: "real set" 918 proof - 919 from that obtain s where s: "\<forall>y\<in>X. y \<le> s" "\<And>z. \<forall>y\<in>X. y \<le> z \<Longrightarrow> s \<le> z" 920 using complete_real[of X] unfolding bdd_above_def by blast 921 then show ?thesis 922 unfolding Sup_real_def by (rule LeastI2_order) (auto simp: that) 923 qed 924 show Sup_least: "Sup X \<le> z" 925 if "X \<noteq> {}" and z: "\<And>x. x \<in> X \<Longrightarrow> x \<le> z" 926 for z :: real and X :: "real set" 927 proof - 928 from that obtain s where s: "\<forall>y\<in>X. y \<le> s" "\<And>z. \<forall>y\<in>X. y \<le> z \<Longrightarrow> s \<le> z" 929 using complete_real [of X] by blast 930 then have "Sup X = s" 931 unfolding Sup_real_def by (best intro: Least_equality) 932 also from s z have "\<dots> \<le> z" 933 by blast 934 finally show ?thesis . 935 qed 936 show "Inf X \<le> x" if "x \<in> X" "bdd_below X" 937 for x :: real and X :: "real set" 938 using Sup_upper [of "-x" "uminus ` X"] by (auto simp: Inf_real_def that) 939 show "z \<le> Inf X" if "X \<noteq> {}" "\<And>x. x \<in> X \<Longrightarrow> z \<le> x" 940 for z :: real and X :: "real set" 941 using Sup_least [of "uminus ` X" "- z"] by (force simp: Inf_real_def that) 942 show "\<exists>a b::real. a \<noteq> b" 943 using zero_neq_one by blast 944qed 945 946end 947 948 949subsection \<open>Hiding implementation details\<close> 950 951hide_const (open) vanishes cauchy positive Real 952 953declare Real_induct [induct del] 954declare Abs_real_induct [induct del] 955declare Abs_real_cases [cases del] 956 957lifting_update real.lifting 958lifting_forget real.lifting 959 960 961subsection \<open>More Lemmas\<close> 962 963text \<open>BH: These lemmas should not be necessary; they should be 964 covered by existing simp rules and simplification procedures.\<close> 965 966lemma real_mult_less_iff1 [simp]: "0 < z \<Longrightarrow> x * z < y * z \<longleftrightarrow> x < y" 967 for x y z :: real 968 by simp (* solved by linordered_ring_less_cancel_factor simproc *) 969 970lemma real_mult_le_cancel_iff1 [simp]: "0 < z \<Longrightarrow> x * z \<le> y * z \<longleftrightarrow> x \<le> y" 971 for x y z :: real 972 by simp (* solved by linordered_ring_le_cancel_factor simproc *) 973 974lemma real_mult_le_cancel_iff2 [simp]: "0 < z \<Longrightarrow> z * x \<le> z * y \<longleftrightarrow> x \<le> y" 975 for x y z :: real 976 by simp (* solved by linordered_ring_le_cancel_factor simproc *) 977 978 979subsection \<open>Embedding numbers into the Reals\<close> 980 981abbreviation real_of_nat :: "nat \<Rightarrow> real" 982 where "real_of_nat \<equiv> of_nat" 983 984abbreviation real :: "nat \<Rightarrow> real" 985 where "real \<equiv> of_nat" 986 987abbreviation real_of_int :: "int \<Rightarrow> real" 988 where "real_of_int \<equiv> of_int" 989 990abbreviation real_of_rat :: "rat \<Rightarrow> real" 991 where "real_of_rat \<equiv> of_rat" 992 993declare [[coercion_enabled]] 994 995declare [[coercion "of_nat :: nat \<Rightarrow> int"]] 996declare [[coercion "of_nat :: nat \<Rightarrow> real"]] 997declare [[coercion "of_int :: int \<Rightarrow> real"]] 998 999(* We do not add rat to the coerced types, this has often unpleasant side effects when writing 1000inverse (Suc n) which sometimes gets two coercions: of_rat (inverse (of_nat (Suc n))) *) 1001 1002declare [[coercion_map map]] 1003declare [[coercion_map "\<lambda>f g h x. g (h (f x))"]] 1004declare [[coercion_map "\<lambda>f g (x,y). (f x, g y)"]] 1005 1006declare of_int_eq_0_iff [algebra, presburger] 1007declare of_int_eq_1_iff [algebra, presburger] 1008declare of_int_eq_iff [algebra, presburger] 1009declare of_int_less_0_iff [algebra, presburger] 1010declare of_int_less_1_iff [algebra, presburger] 1011declare of_int_less_iff [algebra, presburger] 1012declare of_int_le_0_iff [algebra, presburger] 1013declare of_int_le_1_iff [algebra, presburger] 1014declare of_int_le_iff [algebra, presburger] 1015declare of_int_0_less_iff [algebra, presburger] 1016declare of_int_0_le_iff [algebra, presburger] 1017declare of_int_1_less_iff [algebra, presburger] 1018declare of_int_1_le_iff [algebra, presburger] 1019 1020lemma int_less_real_le: "n < m \<longleftrightarrow> real_of_int n + 1 \<le> real_of_int m" 1021proof - 1022 have "(0::real) \<le> 1" 1023 by (metis less_eq_real_def zero_less_one) 1024 then show ?thesis 1025 by (metis floor_of_int less_floor_iff) 1026qed 1027 1028lemma int_le_real_less: "n \<le> m \<longleftrightarrow> real_of_int n < real_of_int m + 1" 1029 by (meson int_less_real_le not_le) 1030 1031lemma real_of_int_div_aux: 1032 "(real_of_int x) / (real_of_int d) = 1033 real_of_int (x div d) + (real_of_int (x mod d)) / (real_of_int d)" 1034proof - 1035 have "x = (x div d) * d + x mod d" 1036 by auto 1037 then have "real_of_int x = real_of_int (x div d) * real_of_int d + real_of_int(x mod d)" 1038 by (metis of_int_add of_int_mult) 1039 then have "real_of_int x / real_of_int d = \<dots> / real_of_int d" 1040 by simp 1041 then show ?thesis 1042 by (auto simp add: add_divide_distrib algebra_simps) 1043qed 1044 1045lemma real_of_int_div: 1046 "d dvd n \<Longrightarrow> real_of_int (n div d) = real_of_int n / real_of_int d" for d n :: int 1047 by (simp add: real_of_int_div_aux) 1048 1049lemma real_of_int_div2: "0 \<le> real_of_int n / real_of_int x - real_of_int (n div x)" 1050proof (cases "x = 0") 1051 case False 1052 then show ?thesis 1053 by (metis diff_ge_0_iff_ge floor_divide_of_int_eq of_int_floor_le) 1054qed simp 1055 1056lemma real_of_int_div3: "real_of_int n / real_of_int x - real_of_int (n div x) \<le> 1" 1057 apply (simp add: algebra_simps) 1058 by (metis add.commute floor_correct floor_divide_of_int_eq less_eq_real_def of_int_1 of_int_add) 1059 1060lemma real_of_int_div4: "real_of_int (n div x) \<le> real_of_int n / real_of_int x" 1061 using real_of_int_div2 [of n x] by simp 1062 1063 1064subsection \<open>Embedding the Naturals into the Reals\<close> 1065 1066lemma real_of_card: "real (card A) = sum (\<lambda>x. 1) A" 1067 by simp 1068 1069lemma nat_less_real_le: "n < m \<longleftrightarrow> real n + 1 \<le> real m" 1070 by (metis discrete of_nat_1 of_nat_add of_nat_le_iff) 1071 1072lemma nat_le_real_less: "n \<le> m \<longleftrightarrow> real n < real m + 1" 1073 for m n :: nat 1074 by (meson nat_less_real_le not_le) 1075 1076lemma real_of_nat_div_aux: "real x / real d = real (x div d) + real (x mod d) / real d" 1077proof - 1078 have "x = (x div d) * d + x mod d" 1079 by auto 1080 then have "real x = real (x div d) * real d + real(x mod d)" 1081 by (metis of_nat_add of_nat_mult) 1082 then have "real x / real d = \<dots> / real d" 1083 by simp 1084 then show ?thesis 1085 by (auto simp add: add_divide_distrib algebra_simps) 1086qed 1087 1088lemma real_of_nat_div: "d dvd n \<Longrightarrow> real(n div d) = real n / real d" 1089 by (subst real_of_nat_div_aux) (auto simp add: dvd_eq_mod_eq_0 [symmetric]) 1090 1091lemma real_of_nat_div2: "0 \<le> real n / real x - real (n div x)" for n x :: nat 1092 apply (simp add: algebra_simps) 1093 by (metis floor_divide_of_nat_eq of_int_floor_le of_int_of_nat_eq) 1094 1095lemma real_of_nat_div3: "real n / real x - real (n div x) \<le> 1" for n x :: nat 1096proof (cases "x = 0") 1097 case False 1098 then show ?thesis 1099 by (metis of_int_of_nat_eq real_of_int_div3 zdiv_int) 1100qed auto 1101 1102lemma real_of_nat_div4: "real (n div x) \<le> real n / real x" for n x :: nat 1103 using real_of_nat_div2 [of n x] by simp 1104 1105 1106subsection \<open>The Archimedean Property of the Reals\<close> 1107 1108lemma real_arch_inverse: "0 < e \<longleftrightarrow> (\<exists>n::nat. n \<noteq> 0 \<and> 0 < inverse (real n) \<and> inverse (real n) < e)" 1109 using reals_Archimedean[of e] less_trans[of 0 "1 / real n" e for n::nat] 1110 by (auto simp add: field_simps cong: conj_cong simp del: of_nat_Suc) 1111 1112lemma reals_Archimedean3: "0 < x \<Longrightarrow> \<forall>y. \<exists>n. y < real n * x" 1113 by (auto intro: ex_less_of_nat_mult) 1114 1115lemma real_archimedian_rdiv_eq_0: 1116 assumes x0: "x \<ge> 0" 1117 and c: "c \<ge> 0" 1118 and xc: "\<And>m::nat. m > 0 \<Longrightarrow> real m * x \<le> c" 1119 shows "x = 0" 1120 by (metis reals_Archimedean3 dual_order.order_iff_strict le0 le_less_trans not_le x0 xc) 1121 1122 1123subsection \<open>Rationals\<close> 1124 1125lemma Rats_abs_iff[simp]: 1126 "\<bar>(x::real)\<bar> \<in> \<rat> \<longleftrightarrow> x \<in> \<rat>" 1127by(simp add: abs_real_def split: if_splits) 1128 1129lemma Rats_eq_int_div_int: "\<rat> = {real_of_int i / real_of_int j | i j. j \<noteq> 0}" (is "_ = ?S") 1130proof 1131 show "\<rat> \<subseteq> ?S" 1132 proof 1133 fix x :: real 1134 assume "x \<in> \<rat>" 1135 then obtain r where "x = of_rat r" 1136 unfolding Rats_def .. 1137 have "of_rat r \<in> ?S" 1138 by (cases r) (auto simp add: of_rat_rat) 1139 then show "x \<in> ?S" 1140 using \<open>x = of_rat r\<close> by simp 1141 qed 1142next 1143 show "?S \<subseteq> \<rat>" 1144 proof (auto simp: Rats_def) 1145 fix i j :: int 1146 assume "j \<noteq> 0" 1147 then have "real_of_int i / real_of_int j = of_rat (Fract i j)" 1148 by (simp add: of_rat_rat) 1149 then show "real_of_int i / real_of_int j \<in> range of_rat" 1150 by blast 1151 qed 1152qed 1153 1154lemma Rats_eq_int_div_nat: "\<rat> = { real_of_int i / real n | i n. n \<noteq> 0}" 1155proof (auto simp: Rats_eq_int_div_int) 1156 fix i j :: int 1157 assume "j \<noteq> 0" 1158 show "\<exists>(i'::int) (n::nat). real_of_int i / real_of_int j = real_of_int i' / real n \<and> 0 < n" 1159 proof (cases "j > 0") 1160 case True 1161 then have "real_of_int i / real_of_int j = real_of_int i / real (nat j) \<and> 0 < nat j" 1162 by simp 1163 then show ?thesis by blast 1164 next 1165 case False 1166 with \<open>j \<noteq> 0\<close> 1167 have "real_of_int i / real_of_int j = real_of_int (- i) / real (nat (- j)) \<and> 0 < nat (- j)" 1168 by simp 1169 then show ?thesis by blast 1170 qed 1171next 1172 fix i :: int and n :: nat 1173 assume "0 < n" 1174 then have "real_of_int i / real n = real_of_int i / real_of_int(int n) \<and> int n \<noteq> 0" 1175 by simp 1176 then show "\<exists>i' j. real_of_int i / real n = real_of_int i' / real_of_int j \<and> j \<noteq> 0" 1177 by blast 1178qed 1179 1180lemma Rats_abs_nat_div_natE: 1181 assumes "x \<in> \<rat>" 1182 obtains m n :: nat where "n \<noteq> 0" and "\<bar>x\<bar> = real m / real n" and "coprime m n" 1183proof - 1184 from \<open>x \<in> \<rat>\<close> obtain i :: int and n :: nat where "n \<noteq> 0" and "x = real_of_int i / real n" 1185 by (auto simp add: Rats_eq_int_div_nat) 1186 then have "\<bar>x\<bar> = real (nat \<bar>i\<bar>) / real n" by simp 1187 then obtain m :: nat where x_rat: "\<bar>x\<bar> = real m / real n" by blast 1188 let ?gcd = "gcd m n" 1189 from \<open>n \<noteq> 0\<close> have gcd: "?gcd \<noteq> 0" by simp 1190 let ?k = "m div ?gcd" 1191 let ?l = "n div ?gcd" 1192 let ?gcd' = "gcd ?k ?l" 1193 have "?gcd dvd m" .. 1194 then have gcd_k: "?gcd * ?k = m" 1195 by (rule dvd_mult_div_cancel) 1196 have "?gcd dvd n" .. 1197 then have gcd_l: "?gcd * ?l = n" 1198 by (rule dvd_mult_div_cancel) 1199 from \<open>n \<noteq> 0\<close> and gcd_l have "?gcd * ?l \<noteq> 0" by simp 1200 then have "?l \<noteq> 0" by (blast dest!: mult_not_zero) 1201 moreover 1202 have "\<bar>x\<bar> = real ?k / real ?l" 1203 proof - 1204 from gcd have "real ?k / real ?l = real (?gcd * ?k) / real (?gcd * ?l)" 1205 by (simp add: real_of_nat_div) 1206 also from gcd_k and gcd_l have "\<dots> = real m / real n" by simp 1207 also from x_rat have "\<dots> = \<bar>x\<bar>" .. 1208 finally show ?thesis .. 1209 qed 1210 moreover 1211 have "?gcd' = 1" 1212 proof - 1213 have "?gcd * ?gcd' = gcd (?gcd * ?k) (?gcd * ?l)" 1214 by (rule gcd_mult_distrib_nat) 1215 with gcd_k gcd_l have "?gcd * ?gcd' = ?gcd" by simp 1216 with gcd show ?thesis by auto 1217 qed 1218 then have "coprime ?k ?l" 1219 by (simp only: coprime_iff_gcd_eq_1) 1220 ultimately show ?thesis .. 1221qed 1222 1223 1224subsection \<open>Density of the Rational Reals in the Reals\<close> 1225 1226text \<open> 1227 This density proof is due to Stefan Richter and was ported by TN. The 1228 original source is \<^emph>\<open>Real Analysis\<close> by H.L. Royden. 1229 It employs the Archimedean property of the reals.\<close> 1230 1231lemma Rats_dense_in_real: 1232 fixes x :: real 1233 assumes "x < y" 1234 shows "\<exists>r\<in>\<rat>. x < r \<and> r < y" 1235proof - 1236 from \<open>x < y\<close> have "0 < y - x" by simp 1237 with reals_Archimedean obtain q :: nat where q: "inverse (real q) < y - x" and "0 < q" 1238 by blast 1239 define p where "p = \<lceil>y * real q\<rceil> - 1" 1240 define r where "r = of_int p / real q" 1241 from q have "x < y - inverse (real q)" 1242 by simp 1243 also from \<open>0 < q\<close> have "y - inverse (real q) \<le> r" 1244 by (simp add: r_def p_def le_divide_eq left_diff_distrib) 1245 finally have "x < r" . 1246 moreover from \<open>0 < q\<close> have "r < y" 1247 by (simp add: r_def p_def divide_less_eq diff_less_eq less_ceiling_iff [symmetric]) 1248 moreover have "r \<in> \<rat>" 1249 by (simp add: r_def) 1250 ultimately show ?thesis by blast 1251qed 1252 1253lemma of_rat_dense: 1254 fixes x y :: real 1255 assumes "x < y" 1256 shows "\<exists>q :: rat. x < of_rat q \<and> of_rat q < y" 1257 using Rats_dense_in_real [OF \<open>x < y\<close>] 1258 by (auto elim: Rats_cases) 1259 1260 1261subsection \<open>Numerals and Arithmetic\<close> 1262 1263declaration \<open> 1264 K (Lin_Arith.add_inj_thms [@{thm of_nat_le_iff} RS iffD2, @{thm of_nat_eq_iff} RS iffD2] 1265 (* not needed because x < (y::nat) can be rewritten as Suc x <= y: of_nat_less_iff RS iffD2 *) 1266 #> Lin_Arith.add_inj_thms [@{thm of_int_le_iff} RS iffD2, @{thm of_nat_eq_iff} RS iffD2] 1267 (* not needed because x < (y::int) can be rewritten as x + 1 <= y: of_int_less_iff RS iffD2 *) 1268 #> Lin_Arith.add_simps [@{thm of_nat_0}, @{thm of_nat_Suc}, @{thm of_nat_add}, 1269 @{thm of_nat_mult}, @{thm of_int_0}, @{thm of_int_1}, 1270 @{thm of_int_add}, @{thm of_int_minus}, @{thm of_int_diff}, 1271 @{thm of_int_mult}, @{thm of_int_of_nat_eq}, 1272 @{thm of_nat_numeral}, @{thm of_nat_numeral}, @{thm of_int_neg_numeral}] 1273 #> Lin_Arith.add_inj_const (@{const_name of_nat}, @{typ "nat \<Rightarrow> real"}) 1274 #> Lin_Arith.add_inj_const (@{const_name of_int}, @{typ "int \<Rightarrow> real"})) 1275\<close> 1276 1277 1278subsection \<open>Simprules combining \<open>x + y\<close> and \<open>0\<close>\<close> (* FIXME ARE THEY NEEDED? *) 1279 1280lemma real_add_minus_iff [simp]: "x + - a = 0 \<longleftrightarrow> x = a" 1281 for x a :: real 1282 by arith 1283 1284lemma real_add_less_0_iff: "x + y < 0 \<longleftrightarrow> y < - x" 1285 for x y :: real 1286 by auto 1287 1288lemma real_0_less_add_iff: "0 < x + y \<longleftrightarrow> - x < y" 1289 for x y :: real 1290 by auto 1291 1292lemma real_add_le_0_iff: "x + y \<le> 0 \<longleftrightarrow> y \<le> - x" 1293 for x y :: real 1294 by auto 1295 1296lemma real_0_le_add_iff: "0 \<le> x + y \<longleftrightarrow> - x \<le> y" 1297 for x y :: real 1298 by auto 1299 1300 1301subsection \<open>Lemmas about powers\<close> 1302 1303lemma two_realpow_ge_one: "(1::real) \<le> 2 ^ n" 1304 by simp 1305 1306(* FIXME: declare this [simp] for all types, or not at all *) 1307declare sum_squares_eq_zero_iff [simp] sum_power2_eq_zero_iff [simp] 1308 1309lemma real_minus_mult_self_le [simp]: "- (u * u) \<le> x * x" 1310 for u x :: real 1311 by (rule order_trans [where y = 0]) auto 1312 1313lemma realpow_square_minus_le [simp]: "- u\<^sup>2 \<le> x\<^sup>2" 1314 for u x :: real 1315 by (auto simp add: power2_eq_square) 1316 1317 1318subsection \<open>Density of the Reals\<close> 1319 1320lemma field_lbound_gt_zero: "0 < d1 \<Longrightarrow> 0 < d2 \<Longrightarrow> \<exists>e. 0 < e \<and> e < d1 \<and> e < d2" 1321 for d1 d2 :: "'a::linordered_field" 1322 by (rule exI [where x = "min d1 d2 / 2"]) (simp add: min_def) 1323 1324lemma field_less_half_sum: "x < y \<Longrightarrow> x < (x + y) / 2" 1325 for x y :: "'a::linordered_field" 1326 by auto 1327 1328lemma field_sum_of_halves: "x / 2 + x / 2 = x" 1329 for x :: "'a::linordered_field" 1330 by simp 1331 1332 1333subsection \<open>Floor and Ceiling Functions from the Reals to the Integers\<close> 1334 1335(* FIXME: theorems for negative numerals. Many duplicates, e.g. from Archimedean_Field.thy. *) 1336 1337lemma real_of_nat_less_numeral_iff [simp]: "real n < numeral w \<longleftrightarrow> n < numeral w" 1338 for n :: nat 1339 by (metis of_nat_less_iff of_nat_numeral) 1340 1341lemma numeral_less_real_of_nat_iff [simp]: "numeral w < real n \<longleftrightarrow> numeral w < n" 1342 for n :: nat 1343 by (metis of_nat_less_iff of_nat_numeral) 1344 1345lemma numeral_le_real_of_nat_iff [simp]: "numeral n \<le> real m \<longleftrightarrow> numeral n \<le> m" 1346 for m :: nat 1347 by (metis not_le real_of_nat_less_numeral_iff) 1348 1349lemma of_int_floor_cancel [simp]: "of_int \<lfloor>x\<rfloor> = x \<longleftrightarrow> (\<exists>n::int. x = of_int n)" 1350 by (metis floor_of_int) 1351 1352lemma floor_eq: "real_of_int n < x \<Longrightarrow> x < real_of_int n + 1 \<Longrightarrow> \<lfloor>x\<rfloor> = n" 1353 by linarith 1354 1355lemma floor_eq2: "real_of_int n \<le> x \<Longrightarrow> x < real_of_int n + 1 \<Longrightarrow> \<lfloor>x\<rfloor> = n" 1356 by (fact floor_unique) 1357 1358lemma floor_eq3: "real n < x \<Longrightarrow> x < real (Suc n) \<Longrightarrow> nat \<lfloor>x\<rfloor> = n" 1359 by linarith 1360 1361lemma floor_eq4: "real n \<le> x \<Longrightarrow> x < real (Suc n) \<Longrightarrow> nat \<lfloor>x\<rfloor> = n" 1362 by linarith 1363 1364lemma real_of_int_floor_ge_diff_one [simp]: "r - 1 \<le> real_of_int \<lfloor>r\<rfloor>" 1365 by linarith 1366 1367lemma real_of_int_floor_gt_diff_one [simp]: "r - 1 < real_of_int \<lfloor>r\<rfloor>" 1368 by linarith 1369 1370lemma real_of_int_floor_add_one_ge [simp]: "r \<le> real_of_int \<lfloor>r\<rfloor> + 1" 1371 by linarith 1372 1373lemma real_of_int_floor_add_one_gt [simp]: "r < real_of_int \<lfloor>r\<rfloor> + 1" 1374 by linarith 1375 1376lemma floor_divide_real_eq_div: 1377 assumes "0 \<le> b" 1378 shows "\<lfloor>a / real_of_int b\<rfloor> = \<lfloor>a\<rfloor> div b" 1379proof (cases "b = 0") 1380 case True 1381 then show ?thesis by simp 1382next 1383 case False 1384 with assms have b: "b > 0" by simp 1385 have "j = i div b" 1386 if "real_of_int i \<le> a" "a < 1 + real_of_int i" 1387 "real_of_int j * real_of_int b \<le> a" "a < real_of_int b + real_of_int j * real_of_int b" 1388 for i j :: int 1389 proof - 1390 from that have "i < b + j * b" 1391 by (metis le_less_trans of_int_add of_int_less_iff of_int_mult) 1392 moreover have "j * b < 1 + i" 1393 proof - 1394 have "real_of_int (j * b) < real_of_int i + 1" 1395 using \<open>a < 1 + real_of_int i\<close> \<open>real_of_int j * real_of_int b \<le> a\<close> by force 1396 then show "j * b < 1 + i" by linarith 1397 qed 1398 ultimately have "(j - i div b) * b \<le> i mod b" "i mod b < ((j - i div b) + 1) * b" 1399 by (auto simp: field_simps) 1400 then have "(j - i div b) * b < 1 * b" "0 * b < ((j - i div b) + 1) * b" 1401 using pos_mod_bound [OF b, of i] pos_mod_sign [OF b, of i] 1402 by linarith+ 1403 then show ?thesis using b unfolding mult_less_cancel_right by auto 1404 qed 1405 with b show ?thesis by (auto split: floor_split simp: field_simps) 1406qed 1407 1408lemma floor_one_divide_eq_div_numeral [simp]: 1409 "\<lfloor>1 / numeral b::real\<rfloor> = 1 div numeral b" 1410by (metis floor_divide_of_int_eq of_int_1 of_int_numeral) 1411 1412lemma floor_minus_one_divide_eq_div_numeral [simp]: 1413 "\<lfloor>- (1 / numeral b)::real\<rfloor> = - 1 div numeral b" 1414by (metis (mono_tags, hide_lams) div_minus_right minus_divide_right 1415 floor_divide_of_int_eq of_int_neg_numeral of_int_1) 1416 1417lemma floor_divide_eq_div_numeral [simp]: 1418 "\<lfloor>numeral a / numeral b::real\<rfloor> = numeral a div numeral b" 1419by (metis floor_divide_of_int_eq of_int_numeral) 1420 1421lemma floor_minus_divide_eq_div_numeral [simp]: 1422 "\<lfloor>- (numeral a / numeral b)::real\<rfloor> = - numeral a div numeral b" 1423by (metis divide_minus_left floor_divide_of_int_eq of_int_neg_numeral of_int_numeral) 1424 1425lemma of_int_ceiling_cancel [simp]: "of_int \<lceil>x\<rceil> = x \<longleftrightarrow> (\<exists>n::int. x = of_int n)" 1426 using ceiling_of_int by metis 1427 1428lemma ceiling_eq: "of_int n < x \<Longrightarrow> x \<le> of_int n + 1 \<Longrightarrow> \<lceil>x\<rceil> = n + 1" 1429 by (simp add: ceiling_unique) 1430 1431lemma of_int_ceiling_diff_one_le [simp]: "of_int \<lceil>r\<rceil> - 1 \<le> r" 1432 by linarith 1433 1434lemma of_int_ceiling_le_add_one [simp]: "of_int \<lceil>r\<rceil> \<le> r + 1" 1435 by linarith 1436 1437lemma ceiling_le: "x \<le> of_int a \<Longrightarrow> \<lceil>x\<rceil> \<le> a" 1438 by (simp add: ceiling_le_iff) 1439 1440lemma ceiling_divide_eq_div: "\<lceil>of_int a / of_int b\<rceil> = - (- a div b)" 1441 by (metis ceiling_def floor_divide_of_int_eq minus_divide_left of_int_minus) 1442 1443lemma ceiling_divide_eq_div_numeral [simp]: 1444 "\<lceil>numeral a / numeral b :: real\<rceil> = - (- numeral a div numeral b)" 1445 using ceiling_divide_eq_div[of "numeral a" "numeral b"] by simp 1446 1447lemma ceiling_minus_divide_eq_div_numeral [simp]: 1448 "\<lceil>- (numeral a / numeral b :: real)\<rceil> = - (numeral a div numeral b)" 1449 using ceiling_divide_eq_div[of "- numeral a" "numeral b"] by simp 1450 1451text \<open> 1452 The following lemmas are remnants of the erstwhile functions natfloor 1453 and natceiling. 1454\<close> 1455 1456lemma nat_floor_neg: "x \<le> 0 \<Longrightarrow> nat \<lfloor>x\<rfloor> = 0" 1457 for x :: real 1458 by linarith 1459 1460lemma le_nat_floor: "real x \<le> a \<Longrightarrow> x \<le> nat \<lfloor>a\<rfloor>" 1461 by linarith 1462 1463lemma le_mult_nat_floor: "nat \<lfloor>a\<rfloor> * nat \<lfloor>b\<rfloor> \<le> nat \<lfloor>a * b\<rfloor>" 1464 by (cases "0 \<le> a \<and> 0 \<le> b") 1465 (auto simp add: nat_mult_distrib[symmetric] nat_mono le_mult_floor) 1466 1467lemma nat_ceiling_le_eq [simp]: "nat \<lceil>x\<rceil> \<le> a \<longleftrightarrow> x \<le> real a" 1468 by linarith 1469 1470lemma real_nat_ceiling_ge: "x \<le> real (nat \<lceil>x\<rceil>)" 1471 by linarith 1472 1473lemma Rats_no_top_le: "\<exists>q \<in> \<rat>. x \<le> q" 1474 for x :: real 1475 by (auto intro!: bexI[of _ "of_nat (nat \<lceil>x\<rceil>)"]) linarith 1476 1477lemma Rats_no_bot_less: "\<exists>q \<in> \<rat>. q < x" for x :: real 1478 by (auto intro!: bexI[of _ "of_int (\<lfloor>x\<rfloor> - 1)"]) linarith 1479 1480 1481subsection \<open>Exponentiation with floor\<close> 1482 1483lemma floor_power: 1484 assumes "x = of_int \<lfloor>x\<rfloor>" 1485 shows "\<lfloor>x ^ n\<rfloor> = \<lfloor>x\<rfloor> ^ n" 1486proof - 1487 have "x ^ n = of_int (\<lfloor>x\<rfloor> ^ n)" 1488 using assms by (induct n arbitrary: x) simp_all 1489 then show ?thesis by (metis floor_of_int) 1490qed 1491 1492lemma floor_numeral_power [simp]: "\<lfloor>numeral x ^ n\<rfloor> = numeral x ^ n" 1493 by (metis floor_of_int of_int_numeral of_int_power) 1494 1495lemma ceiling_numeral_power [simp]: "\<lceil>numeral x ^ n\<rceil> = numeral x ^ n" 1496 by (metis ceiling_of_int of_int_numeral of_int_power) 1497 1498 1499subsection \<open>Implementation of rational real numbers\<close> 1500 1501text \<open>Formal constructor\<close> 1502 1503definition Ratreal :: "rat \<Rightarrow> real" 1504 where [code_abbrev, simp]: "Ratreal = real_of_rat" 1505 1506code_datatype Ratreal 1507 1508 1509text \<open>Quasi-Numerals\<close> 1510 1511lemma [code_abbrev]: 1512 "real_of_rat (numeral k) = numeral k" 1513 "real_of_rat (- numeral k) = - numeral k" 1514 "real_of_rat (rat_of_int a) = real_of_int a" 1515 by simp_all 1516 1517lemma [code_post]: 1518 "real_of_rat 0 = 0" 1519 "real_of_rat 1 = 1" 1520 "real_of_rat (- 1) = - 1" 1521 "real_of_rat (1 / numeral k) = 1 / numeral k" 1522 "real_of_rat (numeral k / numeral l) = numeral k / numeral l" 1523 "real_of_rat (- (1 / numeral k)) = - (1 / numeral k)" 1524 "real_of_rat (- (numeral k / numeral l)) = - (numeral k / numeral l)" 1525 by (simp_all add: of_rat_divide of_rat_minus) 1526 1527text \<open>Operations\<close> 1528 1529lemma zero_real_code [code]: "0 = Ratreal 0" 1530 by simp 1531 1532lemma one_real_code [code]: "1 = Ratreal 1" 1533 by simp 1534 1535instantiation real :: equal 1536begin 1537 1538definition "HOL.equal x y \<longleftrightarrow> x - y = 0" for x :: real 1539 1540instance by standard (simp add: equal_real_def) 1541 1542lemma real_equal_code [code]: "HOL.equal (Ratreal x) (Ratreal y) \<longleftrightarrow> HOL.equal x y" 1543 by (simp add: equal_real_def equal) 1544 1545lemma [code nbe]: "HOL.equal x x \<longleftrightarrow> True" 1546 for x :: real 1547 by (rule equal_refl) 1548 1549end 1550 1551lemma real_less_eq_code [code]: "Ratreal x \<le> Ratreal y \<longleftrightarrow> x \<le> y" 1552 by (simp add: of_rat_less_eq) 1553 1554lemma real_less_code [code]: "Ratreal x < Ratreal y \<longleftrightarrow> x < y" 1555 by (simp add: of_rat_less) 1556 1557lemma real_plus_code [code]: "Ratreal x + Ratreal y = Ratreal (x + y)" 1558 by (simp add: of_rat_add) 1559 1560lemma real_times_code [code]: "Ratreal x * Ratreal y = Ratreal (x * y)" 1561 by (simp add: of_rat_mult) 1562 1563lemma real_uminus_code [code]: "- Ratreal x = Ratreal (- x)" 1564 by (simp add: of_rat_minus) 1565 1566lemma real_minus_code [code]: "Ratreal x - Ratreal y = Ratreal (x - y)" 1567 by (simp add: of_rat_diff) 1568 1569lemma real_inverse_code [code]: "inverse (Ratreal x) = Ratreal (inverse x)" 1570 by (simp add: of_rat_inverse) 1571 1572lemma real_divide_code [code]: "Ratreal x / Ratreal y = Ratreal (x / y)" 1573 by (simp add: of_rat_divide) 1574 1575lemma real_floor_code [code]: "\<lfloor>Ratreal x\<rfloor> = \<lfloor>x\<rfloor>" 1576 by (metis Ratreal_def floor_le_iff floor_unique le_floor_iff 1577 of_int_floor_le of_rat_of_int_eq real_less_eq_code) 1578 1579 1580text \<open>Quickcheck\<close> 1581 1582definition (in term_syntax) 1583 valterm_ratreal :: "rat \<times> (unit \<Rightarrow> Code_Evaluation.term) \<Rightarrow> real \<times> (unit \<Rightarrow> Code_Evaluation.term)" 1584 where [code_unfold]: "valterm_ratreal k = Code_Evaluation.valtermify Ratreal {\<cdot>} k" 1585 1586notation fcomp (infixl "\<circ>>" 60) 1587notation scomp (infixl "\<circ>\<rightarrow>" 60) 1588 1589instantiation real :: random 1590begin 1591 1592definition 1593 "Quickcheck_Random.random i = Quickcheck_Random.random i \<circ>\<rightarrow> (\<lambda>r. Pair (valterm_ratreal r))" 1594 1595instance .. 1596 1597end 1598 1599no_notation fcomp (infixl "\<circ>>" 60) 1600no_notation scomp (infixl "\<circ>\<rightarrow>" 60) 1601 1602instantiation real :: exhaustive 1603begin 1604 1605definition 1606 "exhaustive_real f d = Quickcheck_Exhaustive.exhaustive (\<lambda>r. f (Ratreal r)) d" 1607 1608instance .. 1609 1610end 1611 1612instantiation real :: full_exhaustive 1613begin 1614 1615definition 1616 "full_exhaustive_real f d = Quickcheck_Exhaustive.full_exhaustive (\<lambda>r. f (valterm_ratreal r)) d" 1617 1618instance .. 1619 1620end 1621 1622instantiation real :: narrowing 1623begin 1624 1625definition 1626 "narrowing_real = Quickcheck_Narrowing.apply (Quickcheck_Narrowing.cons Ratreal) narrowing" 1627 1628instance .. 1629 1630end 1631 1632 1633subsection \<open>Setup for Nitpick\<close> 1634 1635declaration \<open> 1636 Nitpick_HOL.register_frac_type @{type_name real} 1637 [(@{const_name zero_real_inst.zero_real}, @{const_name Nitpick.zero_frac}), 1638 (@{const_name one_real_inst.one_real}, @{const_name Nitpick.one_frac}), 1639 (@{const_name plus_real_inst.plus_real}, @{const_name Nitpick.plus_frac}), 1640 (@{const_name times_real_inst.times_real}, @{const_name Nitpick.times_frac}), 1641 (@{const_name uminus_real_inst.uminus_real}, @{const_name Nitpick.uminus_frac}), 1642 (@{const_name inverse_real_inst.inverse_real}, @{const_name Nitpick.inverse_frac}), 1643 (@{const_name ord_real_inst.less_real}, @{const_name Nitpick.less_frac}), 1644 (@{const_name ord_real_inst.less_eq_real}, @{const_name Nitpick.less_eq_frac})] 1645\<close> 1646 1647lemmas [nitpick_unfold] = inverse_real_inst.inverse_real one_real_inst.one_real 1648 ord_real_inst.less_real ord_real_inst.less_eq_real plus_real_inst.plus_real 1649 times_real_inst.times_real uminus_real_inst.uminus_real 1650 zero_real_inst.zero_real 1651 1652 1653subsection \<open>Setup for SMT\<close> 1654 1655ML_file "Tools/SMT/smt_real.ML" 1656ML_file "Tools/SMT/z3_real.ML" 1657 1658lemma [z3_rule]: 1659 "0 + x = x" 1660 "x + 0 = x" 1661 "0 * x = 0" 1662 "1 * x = x" 1663 "-x = -1 * x" 1664 "x + y = y + x" 1665 for x y :: real 1666 by auto 1667 1668 1669subsection \<open>Setup for Argo\<close> 1670 1671ML_file "Tools/Argo/argo_real.ML" 1672 1673end 1674