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