1(* Title: HOL/Nonstandard_Analysis/NSA.thy 2 Author: Jacques D. Fleuriot, University of Cambridge 3 Author: Lawrence C Paulson, University of Cambridge 4*) 5 6section \<open>Infinite Numbers, Infinitesimals, Infinitely Close Relation\<close> 7 8theory NSA 9 imports HyperDef "HOL-Library.Lub_Glb" 10begin 11 12definition hnorm :: "'a::real_normed_vector star \<Rightarrow> real star" 13 where [transfer_unfold]: "hnorm = *f* norm" 14 15definition Infinitesimal :: "('a::real_normed_vector) star set" 16 where "Infinitesimal = {x. \<forall>r \<in> Reals. 0 < r \<longrightarrow> hnorm x < r}" 17 18definition HFinite :: "('a::real_normed_vector) star set" 19 where "HFinite = {x. \<exists>r \<in> Reals. hnorm x < r}" 20 21definition HInfinite :: "('a::real_normed_vector) star set" 22 where "HInfinite = {x. \<forall>r \<in> Reals. r < hnorm x}" 23 24definition approx :: "'a::real_normed_vector star \<Rightarrow> 'a star \<Rightarrow> bool" (infixl "\<approx>" 50) 25 where "x \<approx> y \<longleftrightarrow> x - y \<in> Infinitesimal" 26 \<comment> \<open>the ``infinitely close'' relation\<close> 27 28definition st :: "hypreal \<Rightarrow> hypreal" 29 where "st = (\<lambda>x. SOME r. x \<in> HFinite \<and> r \<in> \<real> \<and> r \<approx> x)" 30 \<comment> \<open>the standard part of a hyperreal\<close> 31 32definition monad :: "'a::real_normed_vector star \<Rightarrow> 'a star set" 33 where "monad x = {y. x \<approx> y}" 34 35definition galaxy :: "'a::real_normed_vector star \<Rightarrow> 'a star set" 36 where "galaxy x = {y. (x + -y) \<in> HFinite}" 37 38lemma SReal_def: "\<real> \<equiv> {x. \<exists>r. x = hypreal_of_real r}" 39 by (simp add: Reals_def image_def) 40 41 42subsection \<open>Nonstandard Extension of the Norm Function\<close> 43 44definition scaleHR :: "real star \<Rightarrow> 'a star \<Rightarrow> 'a::real_normed_vector star" 45 where [transfer_unfold]: "scaleHR = starfun2 scaleR" 46 47lemma Standard_hnorm [simp]: "x \<in> Standard \<Longrightarrow> hnorm x \<in> Standard" 48 by (simp add: hnorm_def) 49 50lemma star_of_norm [simp]: "star_of (norm x) = hnorm (star_of x)" 51 by transfer (rule refl) 52 53lemma hnorm_ge_zero [simp]: "\<And>x::'a::real_normed_vector star. 0 \<le> hnorm x" 54 by transfer (rule norm_ge_zero) 55 56lemma hnorm_eq_zero [simp]: "\<And>x::'a::real_normed_vector star. hnorm x = 0 \<longleftrightarrow> x = 0" 57 by transfer (rule norm_eq_zero) 58 59lemma hnorm_triangle_ineq: "\<And>x y::'a::real_normed_vector star. hnorm (x + y) \<le> hnorm x + hnorm y" 60 by transfer (rule norm_triangle_ineq) 61 62lemma hnorm_triangle_ineq3: "\<And>x y::'a::real_normed_vector star. \<bar>hnorm x - hnorm y\<bar> \<le> hnorm (x - y)" 63 by transfer (rule norm_triangle_ineq3) 64 65lemma hnorm_scaleR: "\<And>x::'a::real_normed_vector star. hnorm (a *\<^sub>R x) = \<bar>star_of a\<bar> * hnorm x" 66 by transfer (rule norm_scaleR) 67 68lemma hnorm_scaleHR: "\<And>a (x::'a::real_normed_vector star). hnorm (scaleHR a x) = \<bar>a\<bar> * hnorm x" 69 by transfer (rule norm_scaleR) 70 71lemma hnorm_mult_ineq: "\<And>x y::'a::real_normed_algebra star. hnorm (x * y) \<le> hnorm x * hnorm y" 72 by transfer (rule norm_mult_ineq) 73 74lemma hnorm_mult: "\<And>x y::'a::real_normed_div_algebra star. hnorm (x * y) = hnorm x * hnorm y" 75 by transfer (rule norm_mult) 76 77lemma hnorm_hyperpow: "\<And>(x::'a::{real_normed_div_algebra} star) n. hnorm (x pow n) = hnorm x pow n" 78 by transfer (rule norm_power) 79 80lemma hnorm_one [simp]: "hnorm (1::'a::real_normed_div_algebra star) = 1" 81 by transfer (rule norm_one) 82 83lemma hnorm_zero [simp]: "hnorm (0::'a::real_normed_vector star) = 0" 84 by transfer (rule norm_zero) 85 86lemma zero_less_hnorm_iff [simp]: "\<And>x::'a::real_normed_vector star. 0 < hnorm x \<longleftrightarrow> x \<noteq> 0" 87 by transfer (rule zero_less_norm_iff) 88 89lemma hnorm_minus_cancel [simp]: "\<And>x::'a::real_normed_vector star. hnorm (- x) = hnorm x" 90 by transfer (rule norm_minus_cancel) 91 92lemma hnorm_minus_commute: "\<And>a b::'a::real_normed_vector star. hnorm (a - b) = hnorm (b - a)" 93 by transfer (rule norm_minus_commute) 94 95lemma hnorm_triangle_ineq2: "\<And>a b::'a::real_normed_vector star. hnorm a - hnorm b \<le> hnorm (a - b)" 96 by transfer (rule norm_triangle_ineq2) 97 98lemma hnorm_triangle_ineq4: "\<And>a b::'a::real_normed_vector star. hnorm (a - b) \<le> hnorm a + hnorm b" 99 by transfer (rule norm_triangle_ineq4) 100 101lemma abs_hnorm_cancel [simp]: "\<And>a::'a::real_normed_vector star. \<bar>hnorm a\<bar> = hnorm a" 102 by transfer (rule abs_norm_cancel) 103 104lemma hnorm_of_hypreal [simp]: "\<And>r. hnorm (of_hypreal r::'a::real_normed_algebra_1 star) = \<bar>r\<bar>" 105 by transfer (rule norm_of_real) 106 107lemma nonzero_hnorm_inverse: 108 "\<And>a::'a::real_normed_div_algebra star. a \<noteq> 0 \<Longrightarrow> hnorm (inverse a) = inverse (hnorm a)" 109 by transfer (rule nonzero_norm_inverse) 110 111lemma hnorm_inverse: 112 "\<And>a::'a::{real_normed_div_algebra, division_ring} star. hnorm (inverse a) = inverse (hnorm a)" 113 by transfer (rule norm_inverse) 114 115lemma hnorm_divide: "\<And>a b::'a::{real_normed_field, field} star. hnorm (a / b) = hnorm a / hnorm b" 116 by transfer (rule norm_divide) 117 118lemma hypreal_hnorm_def [simp]: "\<And>r::hypreal. hnorm r = \<bar>r\<bar>" 119 by transfer (rule real_norm_def) 120 121lemma hnorm_add_less: 122 "\<And>(x::'a::real_normed_vector star) y r s. hnorm x < r \<Longrightarrow> hnorm y < s \<Longrightarrow> hnorm (x + y) < r + s" 123 by transfer (rule norm_add_less) 124 125lemma hnorm_mult_less: 126 "\<And>(x::'a::real_normed_algebra star) y r s. hnorm x < r \<Longrightarrow> hnorm y < s \<Longrightarrow> hnorm (x * y) < r * s" 127 by transfer (rule norm_mult_less) 128 129lemma hnorm_scaleHR_less: "\<bar>x\<bar> < r \<Longrightarrow> hnorm y < s \<Longrightarrow> hnorm (scaleHR x y) < r * s" 130 by (simp only: hnorm_scaleHR) (simp add: mult_strict_mono') 131 132 133subsection \<open>Closure Laws for the Standard Reals\<close> 134 135lemma Reals_add_cancel: "x + y \<in> \<real> \<Longrightarrow> y \<in> \<real> \<Longrightarrow> x \<in> \<real>" 136 by (drule (1) Reals_diff) simp 137 138lemma SReal_hrabs: "x \<in> \<real> \<Longrightarrow> \<bar>x\<bar> \<in> \<real>" 139 for x :: hypreal 140 by (simp add: Reals_eq_Standard) 141 142lemma SReal_hypreal_of_real [simp]: "hypreal_of_real x \<in> \<real>" 143 by (simp add: Reals_eq_Standard) 144 145lemma SReal_divide_numeral: "r \<in> \<real> \<Longrightarrow> r / (numeral w::hypreal) \<in> \<real>" 146 by simp 147 148text \<open>\<open>\<epsilon>\<close> is not in Reals because it is an infinitesimal\<close> 149lemma SReal_epsilon_not_mem: "\<epsilon> \<notin> \<real>" 150 by (auto simp: SReal_def hypreal_of_real_not_eq_epsilon [symmetric]) 151 152lemma SReal_omega_not_mem: "\<omega> \<notin> \<real>" 153 by (auto simp: SReal_def hypreal_of_real_not_eq_omega [symmetric]) 154 155lemma SReal_UNIV_real: "{x. hypreal_of_real x \<in> \<real>} = (UNIV::real set)" 156 by simp 157 158lemma SReal_iff: "x \<in> \<real> \<longleftrightarrow> (\<exists>y. x = hypreal_of_real y)" 159 by (simp add: SReal_def) 160 161lemma hypreal_of_real_image: "hypreal_of_real `(UNIV::real set) = \<real>" 162 by (simp add: Reals_eq_Standard Standard_def) 163 164lemma inv_hypreal_of_real_image: "inv hypreal_of_real ` \<real> = UNIV" 165 by (simp add: Reals_eq_Standard Standard_def inj_star_of) 166 167lemma SReal_dense: "x \<in> \<real> \<Longrightarrow> y \<in> \<real> \<Longrightarrow> x < y \<Longrightarrow> \<exists>r \<in> Reals. x < r \<and> r < y" 168 for x y :: hypreal 169 using dense by (fastforce simp add: SReal_def) 170 171 172subsection \<open>Set of Finite Elements is a Subring of the Extended Reals\<close> 173 174lemma HFinite_add: "x \<in> HFinite \<Longrightarrow> y \<in> HFinite \<Longrightarrow> x + y \<in> HFinite" 175 unfolding HFinite_def by (blast intro!: Reals_add hnorm_add_less) 176 177lemma HFinite_mult: "x \<in> HFinite \<Longrightarrow> y \<in> HFinite \<Longrightarrow> x * y \<in> HFinite" 178 for x y :: "'a::real_normed_algebra star" 179 unfolding HFinite_def by (blast intro!: Reals_mult hnorm_mult_less) 180 181lemma HFinite_scaleHR: "x \<in> HFinite \<Longrightarrow> y \<in> HFinite \<Longrightarrow> scaleHR x y \<in> HFinite" 182 by (auto simp: HFinite_def intro!: Reals_mult hnorm_scaleHR_less) 183 184lemma HFinite_minus_iff: "- x \<in> HFinite \<longleftrightarrow> x \<in> HFinite" 185 by (simp add: HFinite_def) 186 187lemma HFinite_star_of [simp]: "star_of x \<in> HFinite" 188 by (simp add: HFinite_def) (metis SReal_hypreal_of_real gt_ex star_of_less star_of_norm) 189 190lemma SReal_subset_HFinite: "(\<real>::hypreal set) \<subseteq> HFinite" 191 by (auto simp add: SReal_def) 192 193lemma HFiniteD: "x \<in> HFinite \<Longrightarrow> \<exists>t \<in> Reals. hnorm x < t" 194 by (simp add: HFinite_def) 195 196lemma HFinite_hrabs_iff [iff]: "\<bar>x\<bar> \<in> HFinite \<longleftrightarrow> x \<in> HFinite" 197 for x :: hypreal 198 by (simp add: HFinite_def) 199 200lemma HFinite_hnorm_iff [iff]: "hnorm x \<in> HFinite \<longleftrightarrow> x \<in> HFinite" 201 for x :: hypreal 202 by (simp add: HFinite_def) 203 204lemma HFinite_numeral [simp]: "numeral w \<in> HFinite" 205 unfolding star_numeral_def by (rule HFinite_star_of) 206 207text \<open>As always with numerals, \<open>0\<close> and \<open>1\<close> are special cases.\<close> 208 209lemma HFinite_0 [simp]: "0 \<in> HFinite" 210 unfolding star_zero_def by (rule HFinite_star_of) 211 212lemma HFinite_1 [simp]: "1 \<in> HFinite" 213 unfolding star_one_def by (rule HFinite_star_of) 214 215lemma hrealpow_HFinite: "x \<in> HFinite \<Longrightarrow> x ^ n \<in> HFinite" 216 for x :: "'a::{real_normed_algebra,monoid_mult} star" 217 by (induct n) (auto intro: HFinite_mult) 218 219lemma HFinite_bounded: 220 fixes x y :: hypreal 221 assumes "x \<in> HFinite" and y: "y \<le> x" "0 \<le> y" shows "y \<in> HFinite" 222proof (cases "x \<le> 0") 223 case True 224 then have "y = 0" 225 using y by auto 226 then show ?thesis 227 by simp 228next 229 case False 230 then show ?thesis 231 using assms le_less_trans by (auto simp: HFinite_def) 232qed 233 234 235subsection \<open>Set of Infinitesimals is a Subring of the Hyperreals\<close> 236 237lemma InfinitesimalI: "(\<And>r. r \<in> \<real> \<Longrightarrow> 0 < r \<Longrightarrow> hnorm x < r) \<Longrightarrow> x \<in> Infinitesimal" 238 by (simp add: Infinitesimal_def) 239 240lemma InfinitesimalD: "x \<in> Infinitesimal \<Longrightarrow> \<forall>r \<in> Reals. 0 < r \<longrightarrow> hnorm x < r" 241 by (simp add: Infinitesimal_def) 242 243lemma InfinitesimalI2: "(\<And>r. 0 < r \<Longrightarrow> hnorm x < star_of r) \<Longrightarrow> x \<in> Infinitesimal" 244 by (auto simp add: Infinitesimal_def SReal_def) 245 246lemma InfinitesimalD2: "x \<in> Infinitesimal \<Longrightarrow> 0 < r \<Longrightarrow> hnorm x < star_of r" 247 by (auto simp add: Infinitesimal_def SReal_def) 248 249lemma Infinitesimal_zero [iff]: "0 \<in> Infinitesimal" 250 by (simp add: Infinitesimal_def) 251 252lemma Infinitesimal_add: 253 assumes "x \<in> Infinitesimal" "y \<in> Infinitesimal" 254 shows "x + y \<in> Infinitesimal" 255proof (rule InfinitesimalI) 256 show "hnorm (x + y) < r" 257 if "r \<in> \<real>" and "0 < r" for r :: "real star" 258 proof - 259 have "hnorm x < r/2" "hnorm y < r/2" 260 using InfinitesimalD SReal_divide_numeral assms half_gt_zero that by blast+ 261 then show ?thesis 262 using hnorm_add_less by fastforce 263 qed 264qed 265 266lemma Infinitesimal_minus_iff [simp]: "- x \<in> Infinitesimal \<longleftrightarrow> x \<in> Infinitesimal" 267 by (simp add: Infinitesimal_def) 268 269lemma Infinitesimal_hnorm_iff: "hnorm x \<in> Infinitesimal \<longleftrightarrow> x \<in> Infinitesimal" 270 by (simp add: Infinitesimal_def) 271 272lemma Infinitesimal_hrabs_iff [iff]: "\<bar>x\<bar> \<in> Infinitesimal \<longleftrightarrow> x \<in> Infinitesimal" 273 for x :: hypreal 274 by (simp add: abs_if) 275 276lemma Infinitesimal_of_hypreal_iff [simp]: 277 "(of_hypreal x::'a::real_normed_algebra_1 star) \<in> Infinitesimal \<longleftrightarrow> x \<in> Infinitesimal" 278 by (subst Infinitesimal_hnorm_iff [symmetric]) simp 279 280lemma Infinitesimal_diff: "x \<in> Infinitesimal \<Longrightarrow> y \<in> Infinitesimal \<Longrightarrow> x - y \<in> Infinitesimal" 281 using Infinitesimal_add [of x "- y"] by simp 282 283lemma Infinitesimal_mult: 284 fixes x y :: "'a::real_normed_algebra star" 285 assumes "x \<in> Infinitesimal" "y \<in> Infinitesimal" 286 shows "x * y \<in> Infinitesimal" 287 proof (rule InfinitesimalI) 288 show "hnorm (x * y) < r" 289 if "r \<in> \<real>" and "0 < r" for r :: "real star" 290 proof - 291 have "hnorm x < 1" "hnorm y < r" 292 using assms that by (auto simp add: InfinitesimalD) 293 then show ?thesis 294 using hnorm_mult_less by fastforce 295 qed 296qed 297 298lemma Infinitesimal_HFinite_mult: 299 fixes x y :: "'a::real_normed_algebra star" 300 assumes "x \<in> Infinitesimal" "y \<in> HFinite" 301 shows "x * y \<in> Infinitesimal" 302proof (rule InfinitesimalI) 303 obtain t where "hnorm y < t" "t \<in> Reals" 304 using HFiniteD \<open>y \<in> HFinite\<close> by blast 305 then have "t > 0" 306 using hnorm_ge_zero le_less_trans by blast 307 show "hnorm (x * y) < r" 308 if "r \<in> \<real>" and "0 < r" for r :: "real star" 309 proof - 310 have "hnorm x < r/t" 311 by (meson InfinitesimalD Reals_divide \<open>hnorm y < t\<close> \<open>t \<in> \<real>\<close> assms(1) divide_pos_pos hnorm_ge_zero le_less_trans that) 312 then have "hnorm (x * y) < (r / t) * t" 313 using \<open>hnorm y < t\<close> hnorm_mult_less by blast 314 then show ?thesis 315 using \<open>0 < t\<close> by auto 316 qed 317qed 318 319lemma Infinitesimal_HFinite_scaleHR: 320 assumes "x \<in> Infinitesimal" "y \<in> HFinite" 321 shows "scaleHR x y \<in> Infinitesimal" 322proof (rule InfinitesimalI) 323 obtain t where "hnorm y < t" "t \<in> Reals" 324 using HFiniteD \<open>y \<in> HFinite\<close> by blast 325 then have "t > 0" 326 using hnorm_ge_zero le_less_trans by blast 327 show "hnorm (scaleHR x y) < r" 328 if "r \<in> \<real>" and "0 < r" for r :: "real star" 329 proof - 330 have "\<bar>x\<bar> * hnorm y < (r / t) * t" 331 by (metis InfinitesimalD Reals_divide \<open>0 < t\<close> \<open>hnorm y < t\<close> \<open>t \<in> \<real>\<close> assms(1) divide_pos_pos hnorm_ge_zero hypreal_hnorm_def mult_strict_mono' that) 332 then show ?thesis 333 by (simp add: \<open>0 < t\<close> hnorm_scaleHR less_imp_not_eq2) 334 qed 335qed 336 337lemma Infinitesimal_HFinite_mult2: 338 fixes x y :: "'a::real_normed_algebra star" 339 assumes "x \<in> Infinitesimal" "y \<in> HFinite" 340 shows "y * x \<in> Infinitesimal" 341proof (rule InfinitesimalI) 342 obtain t where "hnorm y < t" "t \<in> Reals" 343 using HFiniteD \<open>y \<in> HFinite\<close> by blast 344 then have "t > 0" 345 using hnorm_ge_zero le_less_trans by blast 346 show "hnorm (y * x) < r" 347 if "r \<in> \<real>" and "0 < r" for r :: "real star" 348 proof - 349 have "hnorm x < r/t" 350 by (meson InfinitesimalD Reals_divide \<open>hnorm y < t\<close> \<open>t \<in> \<real>\<close> assms(1) divide_pos_pos hnorm_ge_zero le_less_trans that) 351 then have "hnorm (y * x) < t * (r / t)" 352 using \<open>hnorm y < t\<close> hnorm_mult_less by blast 353 then show ?thesis 354 using \<open>0 < t\<close> by auto 355 qed 356qed 357 358lemma Infinitesimal_scaleR2: 359 assumes "x \<in> Infinitesimal" shows "a *\<^sub>R x \<in> Infinitesimal" 360 by (metis HFinite_star_of Infinitesimal_HFinite_mult2 Infinitesimal_hnorm_iff assms hnorm_scaleR hypreal_hnorm_def star_of_norm) 361 362lemma Compl_HFinite: "- HFinite = HInfinite" 363 proof - 364 have "r < hnorm x" if *: "\<And>s. s \<in> \<real> \<Longrightarrow> s \<le> hnorm x" and "r \<in> \<real>" 365 for x :: "'a star" and r :: hypreal 366 using * [of "r+1"] \<open>r \<in> \<real>\<close> by auto 367 then show ?thesis 368 by (auto simp add: HInfinite_def HFinite_def linorder_not_less) 369qed 370 371lemma HInfinite_inverse_Infinitesimal: 372 "x \<in> HInfinite \<Longrightarrow> inverse x \<in> Infinitesimal" 373 for x :: "'a::real_normed_div_algebra star" 374 by (simp add: HInfinite_def InfinitesimalI hnorm_inverse inverse_less_imp_less) 375 376lemma inverse_Infinitesimal_iff_HInfinite: 377 "x \<noteq> 0 \<Longrightarrow> inverse x \<in> Infinitesimal \<longleftrightarrow> x \<in> HInfinite" 378 for x :: "'a::real_normed_div_algebra star" 379 by (metis Compl_HFinite Compl_iff HInfinite_inverse_Infinitesimal InfinitesimalD Infinitesimal_HFinite_mult Reals_1 hnorm_one left_inverse less_irrefl zero_less_one) 380 381lemma HInfiniteI: "(\<And>r. r \<in> \<real> \<Longrightarrow> r < hnorm x) \<Longrightarrow> x \<in> HInfinite" 382 by (simp add: HInfinite_def) 383 384lemma HInfiniteD: "x \<in> HInfinite \<Longrightarrow> r \<in> \<real> \<Longrightarrow> r < hnorm x" 385 by (simp add: HInfinite_def) 386 387lemma HInfinite_mult: 388 fixes x y :: "'a::real_normed_div_algebra star" 389 assumes "x \<in> HInfinite" "y \<in> HInfinite" shows "x * y \<in> HInfinite" 390proof (rule HInfiniteI, simp only: hnorm_mult) 391 have "x \<noteq> 0" 392 using Compl_HFinite HFinite_0 assms by blast 393 show "r < hnorm x * hnorm y" 394 if "r \<in> \<real>" for r :: "real star" 395 proof - 396 have "r = r * 1" 397 by simp 398 also have "\<dots> < hnorm x * hnorm y" 399 by (meson HInfiniteD Reals_1 \<open>x \<noteq> 0\<close> assms le_numeral_extra(1) mult_strict_mono that zero_less_hnorm_iff) 400 finally show ?thesis . 401 qed 402qed 403 404lemma hypreal_add_zero_less_le_mono: "r < x \<Longrightarrow> 0 \<le> y \<Longrightarrow> r < x + y" 405 for r x y :: hypreal 406 by simp 407 408lemma HInfinite_add_ge_zero: "x \<in> HInfinite \<Longrightarrow> 0 \<le> y \<Longrightarrow> 0 \<le> x \<Longrightarrow> x + y \<in> HInfinite" 409 for x y :: hypreal 410 by (auto simp: abs_if add.commute HInfinite_def) 411 412lemma HInfinite_add_ge_zero2: "x \<in> HInfinite \<Longrightarrow> 0 \<le> y \<Longrightarrow> 0 \<le> x \<Longrightarrow> y + x \<in> HInfinite" 413 for x y :: hypreal 414 by (auto intro!: HInfinite_add_ge_zero simp add: add.commute) 415 416lemma HInfinite_add_gt_zero: "x \<in> HInfinite \<Longrightarrow> 0 < y \<Longrightarrow> 0 < x \<Longrightarrow> x + y \<in> HInfinite" 417 for x y :: hypreal 418 by (blast intro: HInfinite_add_ge_zero order_less_imp_le) 419 420lemma HInfinite_minus_iff: "- x \<in> HInfinite \<longleftrightarrow> x \<in> HInfinite" 421 by (simp add: HInfinite_def) 422 423lemma HInfinite_add_le_zero: "x \<in> HInfinite \<Longrightarrow> y \<le> 0 \<Longrightarrow> x \<le> 0 \<Longrightarrow> x + y \<in> HInfinite" 424 for x y :: hypreal 425 by (metis (no_types, lifting) HInfinite_add_ge_zero2 HInfinite_minus_iff add.inverse_distrib_swap neg_0_le_iff_le) 426 427lemma HInfinite_add_lt_zero: "x \<in> HInfinite \<Longrightarrow> y < 0 \<Longrightarrow> x < 0 \<Longrightarrow> x + y \<in> HInfinite" 428 for x y :: hypreal 429 by (blast intro: HInfinite_add_le_zero order_less_imp_le) 430 431lemma not_Infinitesimal_not_zero: "x \<notin> Infinitesimal \<Longrightarrow> x \<noteq> 0" 432 by auto 433 434lemma HFinite_diff_Infinitesimal_hrabs: 435 "x \<in> HFinite - Infinitesimal \<Longrightarrow> \<bar>x\<bar> \<in> HFinite - Infinitesimal" 436 for x :: hypreal 437 by blast 438 439lemma hnorm_le_Infinitesimal: "e \<in> Infinitesimal \<Longrightarrow> hnorm x \<le> e \<Longrightarrow> x \<in> Infinitesimal" 440 by (auto simp: Infinitesimal_def abs_less_iff) 441 442lemma hnorm_less_Infinitesimal: "e \<in> Infinitesimal \<Longrightarrow> hnorm x < e \<Longrightarrow> x \<in> Infinitesimal" 443 by (erule hnorm_le_Infinitesimal, erule order_less_imp_le) 444 445lemma hrabs_le_Infinitesimal: "e \<in> Infinitesimal \<Longrightarrow> \<bar>x\<bar> \<le> e \<Longrightarrow> x \<in> Infinitesimal" 446 for x :: hypreal 447 by (erule hnorm_le_Infinitesimal) simp 448 449lemma hrabs_less_Infinitesimal: "e \<in> Infinitesimal \<Longrightarrow> \<bar>x\<bar> < e \<Longrightarrow> x \<in> Infinitesimal" 450 for x :: hypreal 451 by (erule hnorm_less_Infinitesimal) simp 452 453lemma Infinitesimal_interval: 454 "e \<in> Infinitesimal \<Longrightarrow> e' \<in> Infinitesimal \<Longrightarrow> e' < x \<Longrightarrow> x < e \<Longrightarrow> x \<in> Infinitesimal" 455 for x :: hypreal 456 by (auto simp add: Infinitesimal_def abs_less_iff) 457 458lemma Infinitesimal_interval2: 459 "e \<in> Infinitesimal \<Longrightarrow> e' \<in> Infinitesimal \<Longrightarrow> e' \<le> x \<Longrightarrow> x \<le> e \<Longrightarrow> x \<in> Infinitesimal" 460 for x :: hypreal 461 by (auto intro: Infinitesimal_interval simp add: order_le_less) 462 463 464lemma lemma_Infinitesimal_hyperpow: "x \<in> Infinitesimal \<Longrightarrow> 0 < N \<Longrightarrow> \<bar>x pow N\<bar> \<le> \<bar>x\<bar>" 465 for x :: hypreal 466 apply (clarsimp simp: Infinitesimal_def) 467 by (metis Reals_1 abs_ge_zero hyperpow_Suc_le_self2 hyperpow_hrabs hypnat_gt_zero_iff2 zero_less_one) 468 469lemma Infinitesimal_hyperpow: "x \<in> Infinitesimal \<Longrightarrow> 0 < N \<Longrightarrow> x pow N \<in> Infinitesimal" 470 for x :: hypreal 471 using hrabs_le_Infinitesimal lemma_Infinitesimal_hyperpow by blast 472 473lemma hrealpow_hyperpow_Infinitesimal_iff: 474 "(x ^ n \<in> Infinitesimal) \<longleftrightarrow> x pow (hypnat_of_nat n) \<in> Infinitesimal" 475 by (simp only: hyperpow_hypnat_of_nat) 476 477lemma Infinitesimal_hrealpow: "x \<in> Infinitesimal \<Longrightarrow> 0 < n \<Longrightarrow> x ^ n \<in> Infinitesimal" 478 for x :: hypreal 479 by (simp add: hrealpow_hyperpow_Infinitesimal_iff Infinitesimal_hyperpow) 480 481lemma not_Infinitesimal_mult: 482 "x \<notin> Infinitesimal \<Longrightarrow> y \<notin> Infinitesimal \<Longrightarrow> x * y \<notin> Infinitesimal" 483 for x y :: "'a::real_normed_div_algebra star" 484 by (metis (no_types, lifting) inverse_Infinitesimal_iff_HInfinite ComplI Compl_HFinite Infinitesimal_HFinite_mult divide_inverse eq_divide_imp inverse_inverse_eq mult_zero_right) 485 486lemma Infinitesimal_mult_disj: "x * y \<in> Infinitesimal \<Longrightarrow> x \<in> Infinitesimal \<or> y \<in> Infinitesimal" 487 for x y :: "'a::real_normed_div_algebra star" 488 using not_Infinitesimal_mult by blast 489 490lemma HFinite_Infinitesimal_not_zero: "x \<in> HFinite-Infinitesimal \<Longrightarrow> x \<noteq> 0" 491 by blast 492 493lemma HFinite_Infinitesimal_diff_mult: 494 "x \<in> HFinite - Infinitesimal \<Longrightarrow> y \<in> HFinite - Infinitesimal \<Longrightarrow> x * y \<in> HFinite - Infinitesimal" 495 for x y :: "'a::real_normed_div_algebra star" 496 by (simp add: HFinite_mult not_Infinitesimal_mult) 497 498lemma Infinitesimal_subset_HFinite: "Infinitesimal \<subseteq> HFinite" 499 using HFinite_def InfinitesimalD Reals_1 zero_less_one by blast 500 501lemma Infinitesimal_star_of_mult: "x \<in> Infinitesimal \<Longrightarrow> x * star_of r \<in> Infinitesimal" 502 for x :: "'a::real_normed_algebra star" 503 by (erule HFinite_star_of [THEN [2] Infinitesimal_HFinite_mult]) 504 505lemma Infinitesimal_star_of_mult2: "x \<in> Infinitesimal \<Longrightarrow> star_of r * x \<in> Infinitesimal" 506 for x :: "'a::real_normed_algebra star" 507 by (erule HFinite_star_of [THEN [2] Infinitesimal_HFinite_mult2]) 508 509 510subsection \<open>The Infinitely Close Relation\<close> 511 512lemma mem_infmal_iff: "x \<in> Infinitesimal \<longleftrightarrow> x \<approx> 0" 513 by (simp add: Infinitesimal_def approx_def) 514 515lemma approx_minus_iff: "x \<approx> y \<longleftrightarrow> x - y \<approx> 0" 516 by (simp add: approx_def) 517 518lemma approx_minus_iff2: "x \<approx> y \<longleftrightarrow> - y + x \<approx> 0" 519 by (simp add: approx_def add.commute) 520 521lemma approx_refl [iff]: "x \<approx> x" 522 by (simp add: approx_def Infinitesimal_def) 523 524lemma approx_sym: "x \<approx> y \<Longrightarrow> y \<approx> x" 525 by (metis Infinitesimal_minus_iff approx_def minus_diff_eq) 526 527lemma approx_trans: 528 assumes "x \<approx> y" "y \<approx> z" shows "x \<approx> z" 529proof - 530 have "x - y \<in> Infinitesimal" "z - y \<in> Infinitesimal" 531 using assms approx_def approx_sym by auto 532 then have "x - z \<in> Infinitesimal" 533 using Infinitesimal_diff by force 534 then show ?thesis 535 by (simp add: approx_def) 536qed 537 538lemma approx_trans2: "r \<approx> x \<Longrightarrow> s \<approx> x \<Longrightarrow> r \<approx> s" 539 by (blast intro: approx_sym approx_trans) 540 541lemma approx_trans3: "x \<approx> r \<Longrightarrow> x \<approx> s \<Longrightarrow> r \<approx> s" 542 by (blast intro: approx_sym approx_trans) 543 544lemma approx_reorient: "x \<approx> y \<longleftrightarrow> y \<approx> x" 545 by (blast intro: approx_sym) 546 547text \<open>Reorientation simplification procedure: reorients (polymorphic) 548 \<open>0 = x\<close>, \<open>1 = x\<close>, \<open>nnn = x\<close> provided \<open>x\<close> isn't \<open>0\<close>, \<open>1\<close> or a numeral.\<close> 549simproc_setup approx_reorient_simproc 550 ("0 \<approx> x" | "1 \<approx> y" | "numeral w \<approx> z" | "- 1 \<approx> y" | "- numeral w \<approx> r") = 551\<open> 552 let val rule = @{thm approx_reorient} RS eq_reflection 553 fun proc phi ss ct = 554 case Thm.term_of ct of 555 _ $ t $ u => if can HOLogic.dest_number u then NONE 556 else if can HOLogic.dest_number t then SOME rule else NONE 557 | _ => NONE 558 in proc end 559\<close> 560 561lemma Infinitesimal_approx_minus: "x - y \<in> Infinitesimal \<longleftrightarrow> x \<approx> y" 562 by (simp add: approx_minus_iff [symmetric] mem_infmal_iff) 563 564lemma approx_monad_iff: "x \<approx> y \<longleftrightarrow> monad x = monad y" 565 apply (simp add: monad_def set_eq_iff) 566 using approx_reorient approx_trans by blast 567 568lemma Infinitesimal_approx: "x \<in> Infinitesimal \<Longrightarrow> y \<in> Infinitesimal \<Longrightarrow> x \<approx> y" 569 by (simp add: Infinitesimal_diff approx_def) 570 571lemma approx_add: "a \<approx> b \<Longrightarrow> c \<approx> d \<Longrightarrow> a + c \<approx> b + d" 572proof (unfold approx_def) 573 assume inf: "a - b \<in> Infinitesimal" "c - d \<in> Infinitesimal" 574 have "a + c - (b + d) = (a - b) + (c - d)" by simp 575 also have "... \<in> Infinitesimal" 576 using inf by (rule Infinitesimal_add) 577 finally show "a + c - (b + d) \<in> Infinitesimal" . 578qed 579 580lemma approx_minus: "a \<approx> b \<Longrightarrow> - a \<approx> - b" 581 by (metis approx_def approx_sym minus_diff_eq minus_diff_minus) 582 583lemma approx_minus2: "- a \<approx> - b \<Longrightarrow> a \<approx> b" 584 by (auto dest: approx_minus) 585 586lemma approx_minus_cancel [simp]: "- a \<approx> - b \<longleftrightarrow> a \<approx> b" 587 by (blast intro: approx_minus approx_minus2) 588 589lemma approx_add_minus: "a \<approx> b \<Longrightarrow> c \<approx> d \<Longrightarrow> a + - c \<approx> b + - d" 590 by (blast intro!: approx_add approx_minus) 591 592lemma approx_diff: "a \<approx> b \<Longrightarrow> c \<approx> d \<Longrightarrow> a - c \<approx> b - d" 593 using approx_add [of a b "- c" "- d"] by simp 594 595lemma approx_mult1: "a \<approx> b \<Longrightarrow> c \<in> HFinite \<Longrightarrow> a * c \<approx> b * c" 596 for a b c :: "'a::real_normed_algebra star" 597 by (simp add: approx_def Infinitesimal_HFinite_mult left_diff_distrib [symmetric]) 598 599lemma approx_mult2: "a \<approx> b \<Longrightarrow> c \<in> HFinite \<Longrightarrow> c * a \<approx> c * b" 600 for a b c :: "'a::real_normed_algebra star" 601 by (simp add: approx_def Infinitesimal_HFinite_mult2 right_diff_distrib [symmetric]) 602 603lemma approx_mult_subst: "u \<approx> v * x \<Longrightarrow> x \<approx> y \<Longrightarrow> v \<in> HFinite \<Longrightarrow> u \<approx> v * y" 604 for u v x y :: "'a::real_normed_algebra star" 605 by (blast intro: approx_mult2 approx_trans) 606 607lemma approx_mult_subst2: "u \<approx> x * v \<Longrightarrow> x \<approx> y \<Longrightarrow> v \<in> HFinite \<Longrightarrow> u \<approx> y * v" 608 for u v x y :: "'a::real_normed_algebra star" 609 by (blast intro: approx_mult1 approx_trans) 610 611lemma approx_mult_subst_star_of: "u \<approx> x * star_of v \<Longrightarrow> x \<approx> y \<Longrightarrow> u \<approx> y * star_of v" 612 for u x y :: "'a::real_normed_algebra star" 613 by (auto intro: approx_mult_subst2) 614 615lemma approx_eq_imp: "a = b \<Longrightarrow> a \<approx> b" 616 by (simp add: approx_def) 617 618lemma Infinitesimal_minus_approx: "x \<in> Infinitesimal \<Longrightarrow> - x \<approx> x" 619 by (blast intro: Infinitesimal_minus_iff [THEN iffD2] mem_infmal_iff [THEN iffD1] approx_trans2) 620 621lemma bex_Infinitesimal_iff: "(\<exists>y \<in> Infinitesimal. x - z = y) \<longleftrightarrow> x \<approx> z" 622 by (simp add: approx_def) 623 624lemma bex_Infinitesimal_iff2: "(\<exists>y \<in> Infinitesimal. x = z + y) \<longleftrightarrow> x \<approx> z" 625 by (force simp add: bex_Infinitesimal_iff [symmetric]) 626 627lemma Infinitesimal_add_approx: "y \<in> Infinitesimal \<Longrightarrow> x + y = z \<Longrightarrow> x \<approx> z" 628 using approx_sym bex_Infinitesimal_iff2 by blast 629 630lemma Infinitesimal_add_approx_self: "y \<in> Infinitesimal \<Longrightarrow> x \<approx> x + y" 631 by (simp add: Infinitesimal_add_approx) 632 633lemma Infinitesimal_add_approx_self2: "y \<in> Infinitesimal \<Longrightarrow> x \<approx> y + x" 634 by (auto dest: Infinitesimal_add_approx_self simp add: add.commute) 635 636lemma Infinitesimal_add_minus_approx_self: "y \<in> Infinitesimal \<Longrightarrow> x \<approx> x + - y" 637 by (blast intro!: Infinitesimal_add_approx_self Infinitesimal_minus_iff [THEN iffD2]) 638 639lemma Infinitesimal_add_cancel: "y \<in> Infinitesimal \<Longrightarrow> x + y \<approx> z \<Longrightarrow> x \<approx> z" 640 using Infinitesimal_add_approx approx_trans by blast 641 642lemma Infinitesimal_add_right_cancel: "y \<in> Infinitesimal \<Longrightarrow> x \<approx> z + y \<Longrightarrow> x \<approx> z" 643 by (metis Infinitesimal_add_approx_self approx_monad_iff) 644 645lemma approx_add_left_cancel: "d + b \<approx> d + c \<Longrightarrow> b \<approx> c" 646 by (metis add_diff_cancel_left bex_Infinitesimal_iff) 647 648lemma approx_add_right_cancel: "b + d \<approx> c + d \<Longrightarrow> b \<approx> c" 649 by (simp add: approx_def) 650 651lemma approx_add_mono1: "b \<approx> c \<Longrightarrow> d + b \<approx> d + c" 652 by (simp add: approx_add) 653 654lemma approx_add_mono2: "b \<approx> c \<Longrightarrow> b + a \<approx> c + a" 655 by (simp add: add.commute approx_add_mono1) 656 657lemma approx_add_left_iff [simp]: "a + b \<approx> a + c \<longleftrightarrow> b \<approx> c" 658 by (fast elim: approx_add_left_cancel approx_add_mono1) 659 660lemma approx_add_right_iff [simp]: "b + a \<approx> c + a \<longleftrightarrow> b \<approx> c" 661 by (simp add: add.commute) 662 663lemma approx_HFinite: "x \<in> HFinite \<Longrightarrow> x \<approx> y \<Longrightarrow> y \<in> HFinite" 664 by (metis HFinite_add Infinitesimal_subset_HFinite approx_sym subsetD bex_Infinitesimal_iff2) 665 666lemma approx_star_of_HFinite: "x \<approx> star_of D \<Longrightarrow> x \<in> HFinite" 667 by (rule approx_sym [THEN [2] approx_HFinite], auto) 668 669lemma approx_mult_HFinite: "a \<approx> b \<Longrightarrow> c \<approx> d \<Longrightarrow> b \<in> HFinite \<Longrightarrow> d \<in> HFinite \<Longrightarrow> a * c \<approx> b * d" 670 for a b c d :: "'a::real_normed_algebra star" 671 by (meson approx_HFinite approx_mult2 approx_mult_subst2 approx_sym) 672 673lemma scaleHR_left_diff_distrib: "\<And>a b x. scaleHR (a - b) x = scaleHR a x - scaleHR b x" 674 by transfer (rule scaleR_left_diff_distrib) 675 676lemma approx_scaleR1: "a \<approx> star_of b \<Longrightarrow> c \<in> HFinite \<Longrightarrow> scaleHR a c \<approx> b *\<^sub>R c" 677 unfolding approx_def 678 by (metis Infinitesimal_HFinite_scaleHR scaleHR_def scaleHR_left_diff_distrib star_scaleR_def starfun2_star_of) 679 680lemma approx_scaleR2: "a \<approx> b \<Longrightarrow> c *\<^sub>R a \<approx> c *\<^sub>R b" 681 by (simp add: approx_def Infinitesimal_scaleR2 scaleR_right_diff_distrib [symmetric]) 682 683lemma approx_scaleR_HFinite: "a \<approx> star_of b \<Longrightarrow> c \<approx> d \<Longrightarrow> d \<in> HFinite \<Longrightarrow> scaleHR a c \<approx> b *\<^sub>R d" 684 by (meson approx_HFinite approx_scaleR1 approx_scaleR2 approx_sym approx_trans) 685 686lemma approx_mult_star_of: "a \<approx> star_of b \<Longrightarrow> c \<approx> star_of d \<Longrightarrow> a * c \<approx> star_of b * star_of d" 687 for a c :: "'a::real_normed_algebra star" 688 by (blast intro!: approx_mult_HFinite approx_star_of_HFinite HFinite_star_of) 689 690lemma approx_SReal_mult_cancel_zero: 691 fixes a x :: hypreal 692 assumes "a \<in> \<real>" "a \<noteq> 0" "a * x \<approx> 0" shows "x \<approx> 0" 693proof - 694 have "inverse a \<in> HFinite" 695 using Reals_inverse SReal_subset_HFinite assms(1) by blast 696 then show ?thesis 697 using assms by (auto dest: approx_mult2 simp add: mult.assoc [symmetric]) 698qed 699 700lemma approx_mult_SReal1: "a \<in> \<real> \<Longrightarrow> x \<approx> 0 \<Longrightarrow> x * a \<approx> 0" 701 for a x :: hypreal 702 by (auto dest: SReal_subset_HFinite [THEN subsetD] approx_mult1) 703 704lemma approx_mult_SReal2: "a \<in> \<real> \<Longrightarrow> x \<approx> 0 \<Longrightarrow> a * x \<approx> 0" 705 for a x :: hypreal 706 by (auto dest: SReal_subset_HFinite [THEN subsetD] approx_mult2) 707 708lemma approx_mult_SReal_zero_cancel_iff [simp]: "a \<in> \<real> \<Longrightarrow> a \<noteq> 0 \<Longrightarrow> a * x \<approx> 0 \<longleftrightarrow> x \<approx> 0" 709 for a x :: hypreal 710 by (blast intro: approx_SReal_mult_cancel_zero approx_mult_SReal2) 711 712lemma approx_SReal_mult_cancel: 713 fixes a w z :: hypreal 714 assumes "a \<in> \<real>" "a \<noteq> 0" "a * w \<approx> a * z" shows "w \<approx> z" 715proof - 716 have "inverse a \<in> HFinite" 717 using Reals_inverse SReal_subset_HFinite assms(1) by blast 718 then show ?thesis 719 using assms by (auto dest: approx_mult2 simp add: mult.assoc [symmetric]) 720qed 721 722lemma approx_SReal_mult_cancel_iff1 [simp]: "a \<in> \<real> \<Longrightarrow> a \<noteq> 0 \<Longrightarrow> a * w \<approx> a * z \<longleftrightarrow> w \<approx> z" 723 for a w z :: hypreal 724 by (meson SReal_subset_HFinite approx_SReal_mult_cancel approx_mult2 subsetD) 725 726lemma approx_le_bound: 727 fixes z :: hypreal 728 assumes "z \<le> f" " f \<approx> g" "g \<le> z" shows "f \<approx> z" 729proof - 730 obtain y where "z \<le> g + y" and "y \<in> Infinitesimal" "f = g + y" 731 using assms bex_Infinitesimal_iff2 by auto 732 then have "z - g \<in> Infinitesimal" 733 using assms(3) hrabs_le_Infinitesimal by auto 734 then show ?thesis 735 by (metis approx_def approx_trans2 assms(2)) 736qed 737 738lemma approx_hnorm: "x \<approx> y \<Longrightarrow> hnorm x \<approx> hnorm y" 739 for x y :: "'a::real_normed_vector star" 740proof (unfold approx_def) 741 assume "x - y \<in> Infinitesimal" 742 then have "hnorm (x - y) \<in> Infinitesimal" 743 by (simp only: Infinitesimal_hnorm_iff) 744 moreover have "(0::real star) \<in> Infinitesimal" 745 by (rule Infinitesimal_zero) 746 moreover have "0 \<le> \<bar>hnorm x - hnorm y\<bar>" 747 by (rule abs_ge_zero) 748 moreover have "\<bar>hnorm x - hnorm y\<bar> \<le> hnorm (x - y)" 749 by (rule hnorm_triangle_ineq3) 750 ultimately have "\<bar>hnorm x - hnorm y\<bar> \<in> Infinitesimal" 751 by (rule Infinitesimal_interval2) 752 then show "hnorm x - hnorm y \<in> Infinitesimal" 753 by (simp only: Infinitesimal_hrabs_iff) 754qed 755 756 757subsection \<open>Zero is the Only Infinitesimal that is also a Real\<close> 758 759lemma Infinitesimal_less_SReal: "x \<in> \<real> \<Longrightarrow> y \<in> Infinitesimal \<Longrightarrow> 0 < x \<Longrightarrow> y < x" 760 for x y :: hypreal 761 using InfinitesimalD by fastforce 762 763lemma Infinitesimal_less_SReal2: "y \<in> Infinitesimal \<Longrightarrow> \<forall>r \<in> Reals. 0 < r \<longrightarrow> y < r" 764 for y :: hypreal 765 by (blast intro: Infinitesimal_less_SReal) 766 767lemma SReal_not_Infinitesimal: "0 < y \<Longrightarrow> y \<in> \<real> ==> y \<notin> Infinitesimal" 768 for y :: hypreal 769 by (auto simp add: Infinitesimal_def abs_if) 770 771lemma SReal_minus_not_Infinitesimal: "y < 0 \<Longrightarrow> y \<in> \<real> \<Longrightarrow> y \<notin> Infinitesimal" 772 for y :: hypreal 773 using Infinitesimal_minus_iff Reals_minus SReal_not_Infinitesimal neg_0_less_iff_less by blast 774 775lemma SReal_Int_Infinitesimal_zero: "\<real> Int Infinitesimal = {0::hypreal}" 776 proof - 777 have "x = 0" if "x \<in> \<real>" "x \<in> Infinitesimal" for x :: "real star" 778 using that SReal_minus_not_Infinitesimal SReal_not_Infinitesimal not_less_iff_gr_or_eq by blast 779 then show ?thesis 780 by auto 781qed 782 783lemma SReal_Infinitesimal_zero: "x \<in> \<real> \<Longrightarrow> x \<in> Infinitesimal \<Longrightarrow> x = 0" 784 for x :: hypreal 785 using SReal_Int_Infinitesimal_zero by blast 786 787lemma SReal_HFinite_diff_Infinitesimal: "x \<in> \<real> \<Longrightarrow> x \<noteq> 0 \<Longrightarrow> x \<in> HFinite - Infinitesimal" 788 for x :: hypreal 789 by (auto dest: SReal_Infinitesimal_zero SReal_subset_HFinite [THEN subsetD]) 790 791lemma hypreal_of_real_HFinite_diff_Infinitesimal: 792 "hypreal_of_real x \<noteq> 0 \<Longrightarrow> hypreal_of_real x \<in> HFinite - Infinitesimal" 793 by (rule SReal_HFinite_diff_Infinitesimal) auto 794 795lemma star_of_Infinitesimal_iff_0 [iff]: "star_of x \<in> Infinitesimal \<longleftrightarrow> x = 0" 796proof 797 show "x = 0" if "star_of x \<in> Infinitesimal" 798 proof - 799 have "hnorm (star_n (\<lambda>n. x)) \<in> Standard" 800 by (metis Reals_eq_Standard SReal_iff star_of_def star_of_norm) 801 then show ?thesis 802 by (metis InfinitesimalD2 less_irrefl star_of_norm that zero_less_norm_iff) 803 qed 804qed auto 805 806lemma star_of_HFinite_diff_Infinitesimal: "x \<noteq> 0 \<Longrightarrow> star_of x \<in> HFinite - Infinitesimal" 807 by simp 808 809lemma numeral_not_Infinitesimal [simp]: 810 "numeral w \<noteq> (0::hypreal) \<Longrightarrow> (numeral w :: hypreal) \<notin> Infinitesimal" 811 by (fast dest: Reals_numeral [THEN SReal_Infinitesimal_zero]) 812 813text \<open>Again: \<open>1\<close> is a special case, but not \<open>0\<close> this time.\<close> 814lemma one_not_Infinitesimal [simp]: 815 "(1::'a::{real_normed_vector,zero_neq_one} star) \<notin> Infinitesimal" 816 by (metis star_of_Infinitesimal_iff_0 star_one_def zero_neq_one) 817 818lemma approx_SReal_not_zero: "y \<in> \<real> \<Longrightarrow> x \<approx> y \<Longrightarrow> y \<noteq> 0 \<Longrightarrow> x \<noteq> 0" 819 for x y :: hypreal 820 using SReal_Infinitesimal_zero approx_sym mem_infmal_iff by auto 821 822lemma HFinite_diff_Infinitesimal_approx: 823 "x \<approx> y \<Longrightarrow> y \<in> HFinite - Infinitesimal \<Longrightarrow> x \<in> HFinite - Infinitesimal" 824 by (meson Diff_iff approx_HFinite approx_sym approx_trans3 mem_infmal_iff) 825 826text \<open>The premise \<open>y \<noteq> 0\<close> is essential; otherwise \<open>x / y = 0\<close> and we lose the 827 \<open>HFinite\<close> premise.\<close> 828lemma Infinitesimal_ratio: 829 "y \<noteq> 0 \<Longrightarrow> y \<in> Infinitesimal \<Longrightarrow> x / y \<in> HFinite \<Longrightarrow> x \<in> Infinitesimal" 830 for x y :: "'a::{real_normed_div_algebra,field} star" 831 using Infinitesimal_HFinite_mult by fastforce 832 833lemma Infinitesimal_SReal_divide: "x \<in> Infinitesimal \<Longrightarrow> y \<in> \<real> \<Longrightarrow> x / y \<in> Infinitesimal" 834 for x y :: hypreal 835 by (metis HFinite_star_of Infinitesimal_HFinite_mult Reals_inverse SReal_iff divide_inverse) 836 837 838section \<open>Standard Part Theorem\<close> 839 840text \<open> 841 Every finite \<open>x \<in> R*\<close> is infinitely close to a unique real number 842 (i.e. a member of \<open>Reals\<close>). 843\<close> 844 845 846subsection \<open>Uniqueness: Two Infinitely Close Reals are Equal\<close> 847 848lemma star_of_approx_iff [simp]: "star_of x \<approx> star_of y \<longleftrightarrow> x = y" 849 by (metis approx_def right_minus_eq star_of_Infinitesimal_iff_0 star_of_simps(2)) 850 851lemma SReal_approx_iff: "x \<in> \<real> \<Longrightarrow> y \<in> \<real> \<Longrightarrow> x \<approx> y \<longleftrightarrow> x = y" 852 for x y :: hypreal 853 by (meson Reals_diff SReal_Infinitesimal_zero approx_def approx_refl right_minus_eq) 854 855lemma numeral_approx_iff [simp]: 856 "(numeral v \<approx> (numeral w :: 'a::{numeral,real_normed_vector} star)) = (numeral v = (numeral w :: 'a))" 857 by (metis star_of_approx_iff star_of_numeral) 858 859text \<open>And also for \<open>0 \<approx> #nn\<close> and \<open>1 \<approx> #nn\<close>, \<open>#nn \<approx> 0\<close> and \<open>#nn \<approx> 1\<close>.\<close> 860lemma [simp]: 861 "(numeral w \<approx> (0::'a::{numeral,real_normed_vector} star)) = (numeral w = (0::'a))" 862 "((0::'a::{numeral,real_normed_vector} star) \<approx> numeral w) = (numeral w = (0::'a))" 863 "(numeral w \<approx> (1::'b::{numeral,one,real_normed_vector} star)) = (numeral w = (1::'b))" 864 "((1::'b::{numeral,one,real_normed_vector} star) \<approx> numeral w) = (numeral w = (1::'b))" 865 "\<not> (0 \<approx> (1::'c::{zero_neq_one,real_normed_vector} star))" 866 "\<not> (1 \<approx> (0::'c::{zero_neq_one,real_normed_vector} star))" 867 unfolding star_numeral_def star_zero_def star_one_def star_of_approx_iff 868 by (auto intro: sym) 869 870lemma star_of_approx_numeral_iff [simp]: "star_of k \<approx> numeral w \<longleftrightarrow> k = numeral w" 871 by (subst star_of_approx_iff [symmetric]) auto 872 873lemma star_of_approx_zero_iff [simp]: "star_of k \<approx> 0 \<longleftrightarrow> k = 0" 874 by (simp_all add: star_of_approx_iff [symmetric]) 875 876lemma star_of_approx_one_iff [simp]: "star_of k \<approx> 1 \<longleftrightarrow> k = 1" 877 by (simp_all add: star_of_approx_iff [symmetric]) 878 879lemma approx_unique_real: "r \<in> \<real> \<Longrightarrow> s \<in> \<real> \<Longrightarrow> r \<approx> x \<Longrightarrow> s \<approx> x \<Longrightarrow> r = s" 880 for r s :: hypreal 881 by (blast intro: SReal_approx_iff [THEN iffD1] approx_trans2) 882 883 884subsection \<open>Existence of Unique Real Infinitely Close\<close> 885 886subsubsection \<open>Lifting of the Ub and Lub Properties\<close> 887 888lemma hypreal_of_real_isUb_iff: "isUb \<real> (hypreal_of_real ` Q) (hypreal_of_real Y) = isUb UNIV Q Y" 889 for Q :: "real set" and Y :: real 890 by (simp add: isUb_def setle_def) 891 892lemma hypreal_of_real_isLub_iff: 893 "isLub \<real> (hypreal_of_real ` Q) (hypreal_of_real Y) = isLub (UNIV :: real set) Q Y" (is "?lhs = ?rhs") 894 for Q :: "real set" and Y :: real 895proof 896 assume ?lhs 897 then show ?rhs 898 by (simp add: isLub_def leastP_def) (metis hypreal_of_real_isUb_iff mem_Collect_eq setge_def star_of_le) 899next 900 assume ?rhs 901 then show ?lhs 902 apply (simp add: isLub_def leastP_def hypreal_of_real_isUb_iff setge_def) 903 by (metis SReal_iff hypreal_of_real_isUb_iff isUb_def star_of_le) 904qed 905 906lemma lemma_isUb_hypreal_of_real: "isUb \<real> P Y \<Longrightarrow> \<exists>Yo. isUb \<real> P (hypreal_of_real Yo)" 907 by (auto simp add: SReal_iff isUb_def) 908 909lemma lemma_isLub_hypreal_of_real: "isLub \<real> P Y \<Longrightarrow> \<exists>Yo. isLub \<real> P (hypreal_of_real Yo)" 910 by (auto simp add: isLub_def leastP_def isUb_def SReal_iff) 911 912lemma SReal_complete: 913 fixes P :: "hypreal set" 914 assumes "isUb \<real> P Y" "P \<subseteq> \<real>" "P \<noteq> {}" 915 shows "\<exists>t. isLub \<real> P t" 916proof - 917 obtain Q where "P = hypreal_of_real ` Q" 918 by (metis \<open>P \<subseteq> \<real>\<close> hypreal_of_real_image subset_imageE) 919 then show ?thesis 920 by (metis assms(1) \<open>P \<noteq> {}\<close> equals0I hypreal_of_real_isLub_iff hypreal_of_real_isUb_iff image_empty lemma_isUb_hypreal_of_real reals_complete) 921qed 922 923 924text \<open>Lemmas about lubs.\<close> 925 926lemma lemma_st_part_lub: 927 fixes x :: hypreal 928 assumes "x \<in> HFinite" 929 shows "\<exists>t. isLub \<real> {s. s \<in> \<real> \<and> s < x} t" 930proof - 931 obtain t where t: "t \<in> \<real>" "hnorm x < t" 932 using HFiniteD assms by blast 933 then have "isUb \<real> {s. s \<in> \<real> \<and> s < x} t" 934 by (simp add: abs_less_iff isUbI le_less_linear less_imp_not_less setleI) 935 moreover have "\<exists>y. y \<in> \<real> \<and> y < x" 936 using t by (rule_tac x = "-t" in exI) (auto simp add: abs_less_iff) 937 ultimately show ?thesis 938 using SReal_complete by fastforce 939qed 940 941lemma hypreal_setle_less_trans: "S *<= x \<Longrightarrow> x < y \<Longrightarrow> S *<= y" 942 for x y :: hypreal 943 by (meson le_less_trans less_imp_le setle_def) 944 945lemma hypreal_gt_isUb: "isUb R S x \<Longrightarrow> x < y \<Longrightarrow> y \<in> R \<Longrightarrow> isUb R S y" 946 for x y :: hypreal 947 using hypreal_setle_less_trans isUb_def by blast 948 949lemma lemma_SReal_ub: "x \<in> \<real> \<Longrightarrow> isUb \<real> {s. s \<in> \<real> \<and> s < x} x" 950 for x :: hypreal 951 by (auto intro: isUbI setleI order_less_imp_le) 952 953lemma lemma_SReal_lub: 954 fixes x :: hypreal 955 assumes "x \<in> \<real>" shows "isLub \<real> {s. s \<in> \<real> \<and> s < x} x" 956proof - 957 have "x \<le> y" if "isUb \<real> {s \<in> \<real>. s < x} y" for y 958 proof - 959 have "y \<in> \<real>" 960 using isUbD2a that by blast 961 show ?thesis 962 proof (cases x y rule: linorder_cases) 963 case greater 964 then obtain r where "y < r" "r < x" 965 using dense by blast 966 then show ?thesis 967 using isUbD [OF that] 968 by simp (meson SReal_dense \<open>y \<in> \<real>\<close> assms greater not_le) 969 qed auto 970 qed 971 with assms show ?thesis 972 by (simp add: isLubI2 isUbI setgeI setleI) 973qed 974 975lemma lemma_st_part_major: 976 fixes x r t :: hypreal 977 assumes x: "x \<in> HFinite" and r: "r \<in> \<real>" "0 < r" and t: "isLub \<real> {s. s \<in> \<real> \<and> s < x} t" 978 shows "\<bar>x - t\<bar> < r" 979proof - 980 have "t \<in> \<real>" 981 using isLubD1a t by blast 982 have lemma_st_part_gt_ub: "x < r \<Longrightarrow> r \<in> \<real> \<Longrightarrow> isUb \<real> {s. s \<in> \<real> \<and> s < x} r" 983 for r :: hypreal 984 by (auto dest: order_less_trans intro: order_less_imp_le intro!: isUbI setleI) 985 986 have "isUb \<real> {s \<in> \<real>. s < x} t" 987 by (simp add: t isLub_isUb) 988 then have "\<not> r + t < x" 989 by (metis (mono_tags, lifting) Reals_add \<open>t \<in> \<real>\<close> add_le_same_cancel2 isUbD leD mem_Collect_eq r) 990 then have "x - t \<le> r" 991 by simp 992 moreover have "\<not> x < t - r" 993 using lemma_st_part_gt_ub isLub_le_isUb \<open>t \<in> \<real>\<close> r t x by fastforce 994 then have "- (x - t) \<le> r" 995 by linarith 996 moreover have False if "x - t = r \<or> - (x - t) = r" 997 proof - 998 have "x \<in> \<real>" 999 by (metis \<open>t \<in> \<real>\<close> \<open>r \<in> \<real>\<close> that Reals_add_cancel Reals_minus_iff add_uminus_conv_diff) 1000 then have "isLub \<real> {s \<in> \<real>. s < x} x" 1001 by (rule lemma_SReal_lub) 1002 then show False 1003 using r t that x isLub_unique by force 1004 qed 1005 ultimately show ?thesis 1006 using abs_less_iff dual_order.order_iff_strict by blast 1007qed 1008 1009lemma lemma_st_part_major2: 1010 "x \<in> HFinite \<Longrightarrow> isLub \<real> {s. s \<in> \<real> \<and> s < x} t \<Longrightarrow> \<forall>r \<in> Reals. 0 < r \<longrightarrow> \<bar>x - t\<bar> < r" 1011 for x t :: hypreal 1012 by (blast dest!: lemma_st_part_major) 1013 1014 1015text\<open>Existence of real and Standard Part Theorem.\<close> 1016 1017lemma lemma_st_part_Ex: "x \<in> HFinite \<Longrightarrow> \<exists>t\<in>Reals. \<forall>r \<in> Reals. 0 < r \<longrightarrow> \<bar>x - t\<bar> < r" 1018 for x :: hypreal 1019 by (meson isLubD1a lemma_st_part_lub lemma_st_part_major2) 1020 1021lemma st_part_Ex: "x \<in> HFinite \<Longrightarrow> \<exists>t\<in>Reals. x \<approx> t" 1022 for x :: hypreal 1023 by (metis InfinitesimalI approx_def hypreal_hnorm_def lemma_st_part_Ex) 1024 1025text \<open>There is a unique real infinitely close.\<close> 1026lemma st_part_Ex1: "x \<in> HFinite \<Longrightarrow> \<exists>!t::hypreal. t \<in> \<real> \<and> x \<approx> t" 1027 by (meson SReal_approx_iff approx_trans2 st_part_Ex) 1028 1029 1030subsection \<open>Finite, Infinite and Infinitesimal\<close> 1031 1032lemma HFinite_Int_HInfinite_empty [simp]: "HFinite Int HInfinite = {}" 1033 using Compl_HFinite by blast 1034 1035lemma HFinite_not_HInfinite: 1036 assumes x: "x \<in> HFinite" shows "x \<notin> HInfinite" 1037 using Compl_HFinite x by blast 1038 1039lemma not_HFinite_HInfinite: "x \<notin> HFinite \<Longrightarrow> x \<in> HInfinite" 1040 using Compl_HFinite by blast 1041 1042lemma HInfinite_HFinite_disj: "x \<in> HInfinite \<or> x \<in> HFinite" 1043 by (blast intro: not_HFinite_HInfinite) 1044 1045lemma HInfinite_HFinite_iff: "x \<in> HInfinite \<longleftrightarrow> x \<notin> HFinite" 1046 by (blast dest: HFinite_not_HInfinite not_HFinite_HInfinite) 1047 1048lemma HFinite_HInfinite_iff: "x \<in> HFinite \<longleftrightarrow> x \<notin> HInfinite" 1049 by (simp add: HInfinite_HFinite_iff) 1050 1051lemma HInfinite_diff_HFinite_Infinitesimal_disj: 1052 "x \<notin> Infinitesimal \<Longrightarrow> x \<in> HInfinite \<or> x \<in> HFinite - Infinitesimal" 1053 by (fast intro: not_HFinite_HInfinite) 1054 1055lemma HFinite_inverse: "x \<in> HFinite \<Longrightarrow> x \<notin> Infinitesimal \<Longrightarrow> inverse x \<in> HFinite" 1056 for x :: "'a::real_normed_div_algebra star" 1057 using HInfinite_inverse_Infinitesimal not_HFinite_HInfinite by force 1058 1059lemma HFinite_inverse2: "x \<in> HFinite - Infinitesimal \<Longrightarrow> inverse x \<in> HFinite" 1060 for x :: "'a::real_normed_div_algebra star" 1061 by (blast intro: HFinite_inverse) 1062 1063text \<open>Stronger statement possible in fact.\<close> 1064lemma Infinitesimal_inverse_HFinite: "x \<notin> Infinitesimal \<Longrightarrow> inverse x \<in> HFinite" 1065 for x :: "'a::real_normed_div_algebra star" 1066 using HFinite_HInfinite_iff HInfinite_inverse_Infinitesimal by fastforce 1067 1068lemma HFinite_not_Infinitesimal_inverse: 1069 "x \<in> HFinite - Infinitesimal \<Longrightarrow> inverse x \<in> HFinite - Infinitesimal" 1070 for x :: "'a::real_normed_div_algebra star" 1071 using HFinite_Infinitesimal_not_zero HFinite_inverse2 Infinitesimal_HFinite_mult2 by fastforce 1072 1073lemma approx_inverse: 1074 fixes x y :: "'a::real_normed_div_algebra star" 1075 assumes "x \<approx> y" and y: "y \<in> HFinite - Infinitesimal" shows "inverse x \<approx> inverse y" 1076proof - 1077 have x: "x \<in> HFinite - Infinitesimal" 1078 using HFinite_diff_Infinitesimal_approx assms(1) y by blast 1079 with y HFinite_inverse2 have "inverse x \<in> HFinite" "inverse y \<in> HFinite" 1080 by blast+ 1081 then have "inverse y * x \<approx> 1" 1082 by (metis Diff_iff approx_mult2 assms(1) left_inverse not_Infinitesimal_not_zero y) 1083 then show ?thesis 1084 by (metis (no_types, lifting) DiffD2 HFinite_Infinitesimal_not_zero Infinitesimal_mult_disj x approx_def approx_sym left_diff_distrib left_inverse) 1085qed 1086 1087(*Used for NSLIM_inverse, NSLIMSEQ_inverse*) 1088lemmas star_of_approx_inverse = star_of_HFinite_diff_Infinitesimal [THEN [2] approx_inverse] 1089lemmas hypreal_of_real_approx_inverse = hypreal_of_real_HFinite_diff_Infinitesimal [THEN [2] approx_inverse] 1090 1091lemma inverse_add_Infinitesimal_approx: 1092 "x \<in> HFinite - Infinitesimal \<Longrightarrow> h \<in> Infinitesimal \<Longrightarrow> inverse (x + h) \<approx> inverse x" 1093 for x h :: "'a::real_normed_div_algebra star" 1094 by (auto intro: approx_inverse approx_sym Infinitesimal_add_approx_self) 1095 1096lemma inverse_add_Infinitesimal_approx2: 1097 "x \<in> HFinite - Infinitesimal \<Longrightarrow> h \<in> Infinitesimal \<Longrightarrow> inverse (h + x) \<approx> inverse x" 1098 for x h :: "'a::real_normed_div_algebra star" 1099 by (metis add.commute inverse_add_Infinitesimal_approx) 1100 1101lemma inverse_add_Infinitesimal_approx_Infinitesimal: 1102 "x \<in> HFinite - Infinitesimal \<Longrightarrow> h \<in> Infinitesimal \<Longrightarrow> inverse (x + h) - inverse x \<approx> h" 1103 for x h :: "'a::real_normed_div_algebra star" 1104 by (meson Infinitesimal_approx bex_Infinitesimal_iff inverse_add_Infinitesimal_approx) 1105 1106lemma Infinitesimal_square_iff: "x \<in> Infinitesimal \<longleftrightarrow> x * x \<in> Infinitesimal" 1107 for x :: "'a::real_normed_div_algebra star" 1108 using Infinitesimal_mult Infinitesimal_mult_disj by auto 1109declare Infinitesimal_square_iff [symmetric, simp] 1110 1111lemma HFinite_square_iff [simp]: "x * x \<in> HFinite \<longleftrightarrow> x \<in> HFinite" 1112 for x :: "'a::real_normed_div_algebra star" 1113 using HFinite_HInfinite_iff HFinite_mult HInfinite_mult by blast 1114 1115lemma HInfinite_square_iff [simp]: "x * x \<in> HInfinite \<longleftrightarrow> x \<in> HInfinite" 1116 for x :: "'a::real_normed_div_algebra star" 1117 by (auto simp add: HInfinite_HFinite_iff) 1118 1119lemma approx_HFinite_mult_cancel: "a \<in> HFinite - Infinitesimal \<Longrightarrow> a * w \<approx> a * z \<Longrightarrow> w \<approx> z" 1120 for a w z :: "'a::real_normed_div_algebra star" 1121 by (metis DiffD2 Infinitesimal_mult_disj bex_Infinitesimal_iff right_diff_distrib) 1122 1123lemma approx_HFinite_mult_cancel_iff1: "a \<in> HFinite - Infinitesimal \<Longrightarrow> a * w \<approx> a * z \<longleftrightarrow> w \<approx> z" 1124 for a w z :: "'a::real_normed_div_algebra star" 1125 by (auto intro: approx_mult2 approx_HFinite_mult_cancel) 1126 1127lemma HInfinite_HFinite_add_cancel: "x + y \<in> HInfinite \<Longrightarrow> y \<in> HFinite \<Longrightarrow> x \<in> HInfinite" 1128 using HFinite_add HInfinite_HFinite_iff by blast 1129 1130lemma HInfinite_HFinite_add: "x \<in> HInfinite \<Longrightarrow> y \<in> HFinite \<Longrightarrow> x + y \<in> HInfinite" 1131 by (metis (no_types, hide_lams) HFinite_HInfinite_iff HFinite_add HFinite_minus_iff add.commute add_minus_cancel) 1132 1133lemma HInfinite_ge_HInfinite: "x \<in> HInfinite \<Longrightarrow> x \<le> y \<Longrightarrow> 0 \<le> x \<Longrightarrow> y \<in> HInfinite" 1134 for x y :: hypreal 1135 by (auto intro: HFinite_bounded simp add: HInfinite_HFinite_iff) 1136 1137lemma Infinitesimal_inverse_HInfinite: "x \<in> Infinitesimal \<Longrightarrow> x \<noteq> 0 \<Longrightarrow> inverse x \<in> HInfinite" 1138 for x :: "'a::real_normed_div_algebra star" 1139 by (metis Infinitesimal_HFinite_mult not_HFinite_HInfinite one_not_Infinitesimal right_inverse) 1140 1141lemma HInfinite_HFinite_not_Infinitesimal_mult: 1142 "x \<in> HInfinite \<Longrightarrow> y \<in> HFinite - Infinitesimal \<Longrightarrow> x * y \<in> HInfinite" 1143 for x y :: "'a::real_normed_div_algebra star" 1144 by (metis (no_types, hide_lams) HFinite_HInfinite_iff HFinite_Infinitesimal_not_zero HFinite_inverse2 HFinite_mult mult.assoc mult.right_neutral right_inverse) 1145 1146lemma HInfinite_HFinite_not_Infinitesimal_mult2: 1147 "x \<in> HInfinite \<Longrightarrow> y \<in> HFinite - Infinitesimal \<Longrightarrow> y * x \<in> HInfinite" 1148 for x y :: "'a::real_normed_div_algebra star" 1149 by (metis Diff_iff HInfinite_HFinite_iff HInfinite_inverse_Infinitesimal Infinitesimal_HFinite_mult2 divide_inverse mult_zero_right nonzero_eq_divide_eq) 1150 1151lemma HInfinite_gt_SReal: "x \<in> HInfinite \<Longrightarrow> 0 < x \<Longrightarrow> y \<in> \<real> \<Longrightarrow> y < x" 1152 for x y :: hypreal 1153 by (auto dest!: bspec simp add: HInfinite_def abs_if order_less_imp_le) 1154 1155lemma HInfinite_gt_zero_gt_one: "x \<in> HInfinite \<Longrightarrow> 0 < x \<Longrightarrow> 1 < x" 1156 for x :: hypreal 1157 by (auto intro: HInfinite_gt_SReal) 1158 1159lemma not_HInfinite_one [simp]: "1 \<notin> HInfinite" 1160 by (simp add: HInfinite_HFinite_iff) 1161 1162lemma approx_hrabs_disj: "\<bar>x\<bar> \<approx> x \<or> \<bar>x\<bar> \<approx> -x" 1163 for x :: hypreal 1164 by (simp add: abs_if) 1165 1166 1167subsection \<open>Theorems about Monads\<close> 1168 1169lemma monad_hrabs_Un_subset: "monad \<bar>x\<bar> \<le> monad x \<union> monad (- x)" 1170 for x :: hypreal 1171 by (simp add: abs_if) 1172 1173lemma Infinitesimal_monad_eq: "e \<in> Infinitesimal \<Longrightarrow> monad (x + e) = monad x" 1174 by (fast intro!: Infinitesimal_add_approx_self [THEN approx_sym] approx_monad_iff [THEN iffD1]) 1175 1176lemma mem_monad_iff: "u \<in> monad x \<longleftrightarrow> - u \<in> monad (- x)" 1177 by (simp add: monad_def) 1178 1179lemma Infinitesimal_monad_zero_iff: "x \<in> Infinitesimal \<longleftrightarrow> x \<in> monad 0" 1180 by (auto intro: approx_sym simp add: monad_def mem_infmal_iff) 1181 1182lemma monad_zero_minus_iff: "x \<in> monad 0 \<longleftrightarrow> - x \<in> monad 0" 1183 by (simp add: Infinitesimal_monad_zero_iff [symmetric]) 1184 1185lemma monad_zero_hrabs_iff: "x \<in> monad 0 \<longleftrightarrow> \<bar>x\<bar> \<in> monad 0" 1186 for x :: hypreal 1187 using Infinitesimal_monad_zero_iff by blast 1188 1189lemma mem_monad_self [simp]: "x \<in> monad x" 1190 by (simp add: monad_def) 1191 1192 1193subsection \<open>Proof that \<^term>\<open>x \<approx> y\<close> implies \<^term>\<open>\<bar>x\<bar> \<approx> \<bar>y\<bar>\<close>\<close> 1194 1195lemma approx_subset_monad: "x \<approx> y \<Longrightarrow> {x, y} \<le> monad x" 1196 by (simp (no_asm)) (simp add: approx_monad_iff) 1197 1198lemma approx_subset_monad2: "x \<approx> y \<Longrightarrow> {x, y} \<le> monad y" 1199 using approx_subset_monad approx_sym by auto 1200 1201lemma mem_monad_approx: "u \<in> monad x \<Longrightarrow> x \<approx> u" 1202 by (simp add: monad_def) 1203 1204lemma approx_mem_monad: "x \<approx> u \<Longrightarrow> u \<in> monad x" 1205 by (simp add: monad_def) 1206 1207lemma approx_mem_monad2: "x \<approx> u \<Longrightarrow> x \<in> monad u" 1208 using approx_mem_monad approx_sym by blast 1209 1210lemma approx_mem_monad_zero: "x \<approx> y \<Longrightarrow> x \<in> monad 0 \<Longrightarrow> y \<in> monad 0" 1211 using approx_trans monad_def by blast 1212 1213lemma Infinitesimal_approx_hrabs: "x \<approx> y \<Longrightarrow> x \<in> Infinitesimal \<Longrightarrow> \<bar>x\<bar> \<approx> \<bar>y\<bar>" 1214 for x y :: hypreal 1215 using approx_hnorm by fastforce 1216 1217lemma less_Infinitesimal_less: "0 < x \<Longrightarrow> x \<notin> Infinitesimal \<Longrightarrow> e \<in> Infinitesimal \<Longrightarrow> e < x" 1218 for x :: hypreal 1219 using Infinitesimal_interval less_linear by blast 1220 1221lemma Ball_mem_monad_gt_zero: "0 < x \<Longrightarrow> x \<notin> Infinitesimal \<Longrightarrow> u \<in> monad x \<Longrightarrow> 0 < u" 1222 for u x :: hypreal 1223 by (metis bex_Infinitesimal_iff2 less_Infinitesimal_less less_add_same_cancel2 mem_monad_approx) 1224 1225lemma Ball_mem_monad_less_zero: "x < 0 \<Longrightarrow> x \<notin> Infinitesimal \<Longrightarrow> u \<in> monad x \<Longrightarrow> u < 0" 1226 for u x :: hypreal 1227 by (metis Ball_mem_monad_gt_zero approx_monad_iff less_asym linorder_neqE_linordered_idom mem_infmal_iff mem_monad_approx mem_monad_self) 1228 1229lemma lemma_approx_gt_zero: "0 < x \<Longrightarrow> x \<notin> Infinitesimal \<Longrightarrow> x \<approx> y \<Longrightarrow> 0 < y" 1230 for x y :: hypreal 1231 by (blast dest: Ball_mem_monad_gt_zero approx_subset_monad) 1232 1233lemma lemma_approx_less_zero: "x < 0 \<Longrightarrow> x \<notin> Infinitesimal \<Longrightarrow> x \<approx> y \<Longrightarrow> y < 0" 1234 for x y :: hypreal 1235 by (blast dest: Ball_mem_monad_less_zero approx_subset_monad) 1236 1237lemma approx_hrabs: "x \<approx> y \<Longrightarrow> \<bar>x\<bar> \<approx> \<bar>y\<bar>" 1238 for x y :: hypreal 1239 by (drule approx_hnorm) simp 1240 1241lemma approx_hrabs_zero_cancel: "\<bar>x\<bar> \<approx> 0 \<Longrightarrow> x \<approx> 0" 1242 for x :: hypreal 1243 using mem_infmal_iff by blast 1244 1245lemma approx_hrabs_add_Infinitesimal: "e \<in> Infinitesimal \<Longrightarrow> \<bar>x\<bar> \<approx> \<bar>x + e\<bar>" 1246 for e x :: hypreal 1247 by (fast intro: approx_hrabs Infinitesimal_add_approx_self) 1248 1249lemma approx_hrabs_add_minus_Infinitesimal: "e \<in> Infinitesimal ==> \<bar>x\<bar> \<approx> \<bar>x + -e\<bar>" 1250 for e x :: hypreal 1251 by (fast intro: approx_hrabs Infinitesimal_add_minus_approx_self) 1252 1253lemma hrabs_add_Infinitesimal_cancel: 1254 "e \<in> Infinitesimal \<Longrightarrow> e' \<in> Infinitesimal \<Longrightarrow> \<bar>x + e\<bar> = \<bar>y + e'\<bar> \<Longrightarrow> \<bar>x\<bar> \<approx> \<bar>y\<bar>" 1255 for e e' x y :: hypreal 1256 by (metis approx_hrabs_add_Infinitesimal approx_trans2) 1257 1258lemma hrabs_add_minus_Infinitesimal_cancel: 1259 "e \<in> Infinitesimal \<Longrightarrow> e' \<in> Infinitesimal \<Longrightarrow> \<bar>x + -e\<bar> = \<bar>y + -e'\<bar> \<Longrightarrow> \<bar>x\<bar> \<approx> \<bar>y\<bar>" 1260 for e e' x y :: hypreal 1261 by (meson Infinitesimal_minus_iff hrabs_add_Infinitesimal_cancel) 1262 1263 1264subsection \<open>More \<^term>\<open>HFinite\<close> and \<^term>\<open>Infinitesimal\<close> Theorems\<close> 1265 1266text \<open> 1267 Interesting slightly counterintuitive theorem: necessary 1268 for proving that an open interval is an NS open set. 1269\<close> 1270lemma Infinitesimal_add_hypreal_of_real_less: 1271 assumes "x < y" and u: "u \<in> Infinitesimal" 1272 shows "hypreal_of_real x + u < hypreal_of_real y" 1273proof - 1274 have "\<bar>u\<bar> < hypreal_of_real y - hypreal_of_real x" 1275 using InfinitesimalD \<open>x < y\<close> u by fastforce 1276 then show ?thesis 1277 by (simp add: abs_less_iff) 1278qed 1279 1280lemma Infinitesimal_add_hrabs_hypreal_of_real_less: 1281 "x \<in> Infinitesimal \<Longrightarrow> \<bar>hypreal_of_real r\<bar> < hypreal_of_real y \<Longrightarrow> 1282 \<bar>hypreal_of_real r + x\<bar> < hypreal_of_real y" 1283 by (metis Infinitesimal_add_hypreal_of_real_less approx_hrabs_add_Infinitesimal approx_sym bex_Infinitesimal_iff2 star_of_abs star_of_less) 1284 1285lemma Infinitesimal_add_hrabs_hypreal_of_real_less2: 1286 "x \<in> Infinitesimal \<Longrightarrow> \<bar>hypreal_of_real r\<bar> < hypreal_of_real y \<Longrightarrow> 1287 \<bar>x + hypreal_of_real r\<bar> < hypreal_of_real y" 1288 using Infinitesimal_add_hrabs_hypreal_of_real_less by fastforce 1289 1290lemma hypreal_of_real_le_add_Infininitesimal_cancel: 1291 assumes le: "hypreal_of_real x + u \<le> hypreal_of_real y + v" 1292 and u: "u \<in> Infinitesimal" and v: "v \<in> Infinitesimal" 1293 shows "hypreal_of_real x \<le> hypreal_of_real y" 1294proof (rule ccontr) 1295 assume "\<not> hypreal_of_real x \<le> hypreal_of_real y" 1296 then have "hypreal_of_real y + (v - u) < hypreal_of_real x" 1297 by (simp add: Infinitesimal_add_hypreal_of_real_less Infinitesimal_diff u v) 1298 then show False 1299 by (simp add: add_diff_eq add_le_imp_le_diff le leD) 1300qed 1301 1302lemma hypreal_of_real_le_add_Infininitesimal_cancel2: 1303 "u \<in> Infinitesimal \<Longrightarrow> v \<in> Infinitesimal \<Longrightarrow> 1304 hypreal_of_real x + u \<le> hypreal_of_real y + v \<Longrightarrow> x \<le> y" 1305 by (blast intro: star_of_le [THEN iffD1] intro!: hypreal_of_real_le_add_Infininitesimal_cancel) 1306 1307lemma hypreal_of_real_less_Infinitesimal_le_zero: 1308 "hypreal_of_real x < e \<Longrightarrow> e \<in> Infinitesimal \<Longrightarrow> hypreal_of_real x \<le> 0" 1309 by (metis Infinitesimal_interval eq_iff le_less_linear star_of_Infinitesimal_iff_0 star_of_eq_0) 1310 1311lemma Infinitesimal_add_not_zero: "h \<in> Infinitesimal \<Longrightarrow> x \<noteq> 0 \<Longrightarrow> star_of x + h \<noteq> 0" 1312 by (metis Infinitesimal_add_approx_self star_of_approx_zero_iff) 1313 1314lemma monad_hrabs_less: "y \<in> monad x \<Longrightarrow> 0 < hypreal_of_real e \<Longrightarrow> \<bar>y - x\<bar> < hypreal_of_real e" 1315 by (simp add: Infinitesimal_approx_minus approx_sym less_Infinitesimal_less mem_monad_approx) 1316 1317lemma mem_monad_SReal_HFinite: "x \<in> monad (hypreal_of_real a) \<Longrightarrow> x \<in> HFinite" 1318 using HFinite_star_of approx_HFinite mem_monad_approx by blast 1319 1320 1321subsection \<open>Theorems about Standard Part\<close> 1322 1323lemma st_approx_self: "x \<in> HFinite \<Longrightarrow> st x \<approx> x" 1324 by (metis (no_types, lifting) approx_refl approx_trans3 someI_ex st_def st_part_Ex st_part_Ex1) 1325 1326lemma st_SReal: "x \<in> HFinite \<Longrightarrow> st x \<in> \<real>" 1327 by (metis (mono_tags, lifting) approx_sym someI_ex st_def st_part_Ex) 1328 1329lemma st_HFinite: "x \<in> HFinite \<Longrightarrow> st x \<in> HFinite" 1330 by (erule st_SReal [THEN SReal_subset_HFinite [THEN subsetD]]) 1331 1332lemma st_unique: "r \<in> \<real> \<Longrightarrow> r \<approx> x \<Longrightarrow> st x = r" 1333 by (meson SReal_subset_HFinite approx_HFinite approx_unique_real st_SReal st_approx_self subsetD) 1334 1335lemma st_SReal_eq: "x \<in> \<real> \<Longrightarrow> st x = x" 1336 by (metis approx_refl st_unique) 1337 1338lemma st_hypreal_of_real [simp]: "st (hypreal_of_real x) = hypreal_of_real x" 1339 by (rule SReal_hypreal_of_real [THEN st_SReal_eq]) 1340 1341lemma st_eq_approx: "x \<in> HFinite \<Longrightarrow> y \<in> HFinite \<Longrightarrow> st x = st y \<Longrightarrow> x \<approx> y" 1342 by (auto dest!: st_approx_self elim!: approx_trans3) 1343 1344lemma approx_st_eq: 1345 assumes x: "x \<in> HFinite" and y: "y \<in> HFinite" and xy: "x \<approx> y" 1346 shows "st x = st y" 1347proof - 1348 have "st x \<approx> x" "st y \<approx> y" "st x \<in> \<real>" "st y \<in> \<real>" 1349 by (simp_all add: st_approx_self st_SReal x y) 1350 with xy show ?thesis 1351 by (fast elim: approx_trans approx_trans2 SReal_approx_iff [THEN iffD1]) 1352qed 1353 1354lemma st_eq_approx_iff: "x \<in> HFinite \<Longrightarrow> y \<in> HFinite \<Longrightarrow> x \<approx> y \<longleftrightarrow> st x = st y" 1355 by (blast intro: approx_st_eq st_eq_approx) 1356 1357lemma st_Infinitesimal_add_SReal: "x \<in> \<real> \<Longrightarrow> e \<in> Infinitesimal \<Longrightarrow> st (x + e) = x" 1358 by (simp add: Infinitesimal_add_approx_self st_unique) 1359 1360lemma st_Infinitesimal_add_SReal2: "x \<in> \<real> \<Longrightarrow> e \<in> Infinitesimal \<Longrightarrow> st (e + x) = x" 1361 by (metis add.commute st_Infinitesimal_add_SReal) 1362 1363lemma HFinite_st_Infinitesimal_add: "x \<in> HFinite \<Longrightarrow> \<exists>e \<in> Infinitesimal. x = st(x) + e" 1364 by (blast dest!: st_approx_self [THEN approx_sym] bex_Infinitesimal_iff2 [THEN iffD2]) 1365 1366lemma st_add: "x \<in> HFinite \<Longrightarrow> y \<in> HFinite \<Longrightarrow> st (x + y) = st x + st y" 1367 by (simp add: st_unique st_SReal st_approx_self approx_add) 1368 1369lemma st_numeral [simp]: "st (numeral w) = numeral w" 1370 by (rule Reals_numeral [THEN st_SReal_eq]) 1371 1372lemma st_neg_numeral [simp]: "st (- numeral w) = - numeral w" 1373 using st_unique by auto 1374 1375lemma st_0 [simp]: "st 0 = 0" 1376 by (simp add: st_SReal_eq) 1377 1378lemma st_1 [simp]: "st 1 = 1" 1379 by (simp add: st_SReal_eq) 1380 1381lemma st_neg_1 [simp]: "st (- 1) = - 1" 1382 by (simp add: st_SReal_eq) 1383 1384lemma st_minus: "x \<in> HFinite \<Longrightarrow> st (- x) = - st x" 1385 by (simp add: st_unique st_SReal st_approx_self approx_minus) 1386 1387lemma st_diff: "\<lbrakk>x \<in> HFinite; y \<in> HFinite\<rbrakk> \<Longrightarrow> st (x - y) = st x - st y" 1388 by (simp add: st_unique st_SReal st_approx_self approx_diff) 1389 1390lemma st_mult: "\<lbrakk>x \<in> HFinite; y \<in> HFinite\<rbrakk> \<Longrightarrow> st (x * y) = st x * st y" 1391 by (simp add: st_unique st_SReal st_approx_self approx_mult_HFinite) 1392 1393lemma st_Infinitesimal: "x \<in> Infinitesimal \<Longrightarrow> st x = 0" 1394 by (simp add: st_unique mem_infmal_iff) 1395 1396lemma st_not_Infinitesimal: "st(x) \<noteq> 0 \<Longrightarrow> x \<notin> Infinitesimal" 1397by (fast intro: st_Infinitesimal) 1398 1399lemma st_inverse: "x \<in> HFinite \<Longrightarrow> st x \<noteq> 0 \<Longrightarrow> st (inverse x) = inverse (st x)" 1400 by (simp add: approx_inverse st_SReal st_approx_self st_not_Infinitesimal st_unique) 1401 1402lemma st_divide [simp]: "x \<in> HFinite \<Longrightarrow> y \<in> HFinite \<Longrightarrow> st y \<noteq> 0 \<Longrightarrow> st (x / y) = st x / st y" 1403 by (simp add: divide_inverse st_mult st_not_Infinitesimal HFinite_inverse st_inverse) 1404 1405lemma st_idempotent [simp]: "x \<in> HFinite \<Longrightarrow> st (st x) = st x" 1406 by (blast intro: st_HFinite st_approx_self approx_st_eq) 1407 1408lemma Infinitesimal_add_st_less: 1409 "x \<in> HFinite \<Longrightarrow> y \<in> HFinite \<Longrightarrow> u \<in> Infinitesimal \<Longrightarrow> st x < st y \<Longrightarrow> st x + u < st y" 1410 by (metis Infinitesimal_add_hypreal_of_real_less SReal_iff st_SReal star_of_less) 1411 1412lemma Infinitesimal_add_st_le_cancel: 1413 "x \<in> HFinite \<Longrightarrow> y \<in> HFinite \<Longrightarrow> u \<in> Infinitesimal \<Longrightarrow> 1414 st x \<le> st y + u \<Longrightarrow> st x \<le> st y" 1415 by (meson Infinitesimal_add_st_less leD le_less_linear) 1416 1417lemma st_le: "x \<in> HFinite \<Longrightarrow> y \<in> HFinite \<Longrightarrow> x \<le> y \<Longrightarrow> st x \<le> st y" 1418 by (metis approx_le_bound approx_sym linear st_SReal st_approx_self st_part_Ex1) 1419 1420lemma st_zero_le: "0 \<le> x \<Longrightarrow> x \<in> HFinite \<Longrightarrow> 0 \<le> st x" 1421 by (metis HFinite_0 st_0 st_le) 1422 1423lemma st_zero_ge: "x \<le> 0 \<Longrightarrow> x \<in> HFinite \<Longrightarrow> st x \<le> 0" 1424 by (metis HFinite_0 st_0 st_le) 1425 1426lemma st_hrabs: "x \<in> HFinite \<Longrightarrow> \<bar>st x\<bar> = st \<bar>x\<bar>" 1427 by (simp add: order_class.order.antisym st_zero_ge linorder_not_le st_zero_le abs_if st_minus linorder_not_less) 1428 1429 1430subsection \<open>Alternative Definitions using Free Ultrafilter\<close> 1431 1432subsubsection \<open>\<^term>\<open>HFinite\<close>\<close> 1433 1434lemma HFinite_FreeUltrafilterNat: 1435 assumes "star_n X \<in> HFinite" 1436 shows "\<exists>u. eventually (\<lambda>n. norm (X n) < u) \<U>" 1437proof - 1438 obtain r where "hnorm (star_n X) < hypreal_of_real r" 1439 using HFiniteD SReal_iff assms by fastforce 1440 then have "\<forall>\<^sub>F n in \<U>. norm (X n) < r" 1441 by (simp add: hnorm_def star_n_less star_of_def starfun_star_n) 1442 then show ?thesis .. 1443qed 1444 1445lemma FreeUltrafilterNat_HFinite: 1446 assumes "eventually (\<lambda>n. norm (X n) < u) \<U>" 1447 shows "star_n X \<in> HFinite" 1448proof - 1449 have "hnorm (star_n X) < hypreal_of_real u" 1450 by (simp add: assms hnorm_def star_n_less star_of_def starfun_star_n) 1451 then show ?thesis 1452 by (meson HInfiniteD SReal_hypreal_of_real less_asym not_HFinite_HInfinite) 1453qed 1454 1455lemma HFinite_FreeUltrafilterNat_iff: 1456 "star_n X \<in> HFinite \<longleftrightarrow> (\<exists>u. eventually (\<lambda>n. norm (X n) < u) \<U>)" 1457 using FreeUltrafilterNat_HFinite HFinite_FreeUltrafilterNat by blast 1458 1459 1460subsubsection \<open>\<^term>\<open>HInfinite\<close>\<close> 1461 1462text \<open>Exclude this type of sets from free ultrafilter for Infinite numbers!\<close> 1463lemma FreeUltrafilterNat_const_Finite: 1464 "eventually (\<lambda>n. norm (X n) = u) \<U> \<Longrightarrow> star_n X \<in> HFinite" 1465 by (simp add: FreeUltrafilterNat_HFinite [where u = "u+1"] eventually_mono) 1466 1467lemma HInfinite_FreeUltrafilterNat: 1468 "star_n X \<in> HInfinite \<Longrightarrow> eventually (\<lambda>n. u < norm (X n)) \<U>" 1469 apply (drule HInfinite_HFinite_iff [THEN iffD1]) 1470 apply (simp add: HFinite_FreeUltrafilterNat_iff) 1471 apply (drule_tac x="u + 1" in spec) 1472 apply (simp add: FreeUltrafilterNat.eventually_not_iff[symmetric]) 1473 apply (auto elim: eventually_mono) 1474 done 1475 1476lemma FreeUltrafilterNat_HInfinite: 1477 assumes "\<And>u. eventually (\<lambda>n. u < norm (X n)) \<U>" 1478 shows "star_n X \<in> HInfinite" 1479proof - 1480 { fix u 1481 assume "\<forall>\<^sub>Fn in \<U>. norm (X n) < u" "\<forall>\<^sub>Fn in \<U>. u < norm (X n)" 1482 then have "\<forall>\<^sub>F x in \<U>. False" 1483 by eventually_elim auto 1484 then have False 1485 by (simp add: eventually_False FreeUltrafilterNat.proper) } 1486 then show ?thesis 1487 using HFinite_FreeUltrafilterNat HInfinite_HFinite_iff assms by blast 1488qed 1489 1490lemma HInfinite_FreeUltrafilterNat_iff: 1491 "star_n X \<in> HInfinite \<longleftrightarrow> (\<forall>u. eventually (\<lambda>n. u < norm (X n)) \<U>)" 1492 using HInfinite_FreeUltrafilterNat FreeUltrafilterNat_HInfinite by blast 1493 1494 1495subsubsection \<open>\<^term>\<open>Infinitesimal\<close>\<close> 1496 1497lemma ball_SReal_eq: "(\<forall>x::hypreal \<in> Reals. P x) \<longleftrightarrow> (\<forall>x::real. P (star_of x))" 1498 by (auto simp: SReal_def) 1499 1500 1501lemma Infinitesimal_FreeUltrafilterNat_iff: 1502 "(star_n X \<in> Infinitesimal) = (\<forall>u>0. eventually (\<lambda>n. norm (X n) < u) \<U>)" (is "?lhs = ?rhs") 1503proof 1504 assume ?lhs 1505 then show ?rhs 1506 apply (simp add: Infinitesimal_def ball_SReal_eq) 1507 apply (simp add: hnorm_def starfun_star_n star_of_def star_less_def starP2_star_n) 1508 done 1509next 1510 assume ?rhs 1511 then show ?lhs 1512 apply (simp add: Infinitesimal_def ball_SReal_eq) 1513 apply (simp add: hnorm_def starfun_star_n star_of_def star_less_def starP2_star_n) 1514 done 1515qed 1516 1517 1518text \<open>Infinitesimals as smaller than \<open>1/n\<close> for all \<open>n::nat (> 0)\<close>.\<close> 1519 1520lemma lemma_Infinitesimal: "(\<forall>r. 0 < r \<longrightarrow> x < r) \<longleftrightarrow> (\<forall>n. x < inverse (real (Suc n)))" 1521 by (meson inverse_positive_iff_positive less_trans of_nat_0_less_iff reals_Archimedean zero_less_Suc) 1522 1523lemma lemma_Infinitesimal2: 1524 "(\<forall>r \<in> Reals. 0 < r \<longrightarrow> x < r) \<longleftrightarrow> (\<forall>n. x < inverse(hypreal_of_nat (Suc n)))" 1525 apply safe 1526 apply (drule_tac x = "inverse (hypreal_of_real (real (Suc n))) " in bspec) 1527 apply simp_all 1528 using less_imp_of_nat_less apply fastforce 1529 apply (auto dest!: reals_Archimedean simp add: SReal_iff simp del: of_nat_Suc) 1530 apply (drule star_of_less [THEN iffD2]) 1531 apply simp 1532 apply (blast intro: order_less_trans) 1533 done 1534 1535 1536lemma Infinitesimal_hypreal_of_nat_iff: 1537 "Infinitesimal = {x. \<forall>n. hnorm x < inverse (hypreal_of_nat (Suc n))}" 1538 using Infinitesimal_def lemma_Infinitesimal2 by auto 1539 1540 1541subsection \<open>Proof that \<open>\<omega>\<close> is an infinite number\<close> 1542 1543text \<open>It will follow that \<open>\<epsilon>\<close> is an infinitesimal number.\<close> 1544 1545lemma Suc_Un_eq: "{n. n < Suc m} = {n. n < m} Un {n. n = m}" 1546 by (auto simp add: less_Suc_eq) 1547 1548 1549text \<open>Prove that any segment is finite and hence cannot belong to \<open>\<U>\<close>.\<close> 1550 1551lemma finite_real_of_nat_segment: "finite {n::nat. real n < real (m::nat)}" 1552 by auto 1553 1554lemma finite_real_of_nat_less_real: "finite {n::nat. real n < u}" 1555 apply (cut_tac x = u in reals_Archimedean2, safe) 1556 apply (rule finite_real_of_nat_segment [THEN [2] finite_subset]) 1557 apply (auto dest: order_less_trans) 1558 done 1559 1560lemma finite_real_of_nat_le_real: "finite {n::nat. real n \<le> u}" 1561 by (metis infinite_nat_iff_unbounded leD le_nat_floor mem_Collect_eq) 1562 1563lemma finite_rabs_real_of_nat_le_real: "finite {n::nat. \<bar>real n\<bar> \<le> u}" 1564 by (simp add: finite_real_of_nat_le_real) 1565 1566lemma rabs_real_of_nat_le_real_FreeUltrafilterNat: 1567 "\<not> eventually (\<lambda>n. \<bar>real n\<bar> \<le> u) \<U>" 1568 by (blast intro!: FreeUltrafilterNat.finite finite_rabs_real_of_nat_le_real) 1569 1570lemma FreeUltrafilterNat_nat_gt_real: "eventually (\<lambda>n. u < real n) \<U>" 1571proof - 1572 have "{n::nat. \<not> u < real n} = {n. real n \<le> u}" 1573 by auto 1574 then show ?thesis 1575 by (auto simp add: FreeUltrafilterNat.finite' finite_real_of_nat_le_real) 1576qed 1577 1578text \<open>The complement of \<open>{n. \<bar>real n\<bar> \<le> u} = {n. u < \<bar>real n\<bar>}\<close> is in 1579 \<open>\<U>\<close> by property of (free) ultrafilters.\<close> 1580 1581text \<open>\<^term>\<open>\<omega>\<close> is a member of \<^term>\<open>HInfinite\<close>.\<close> 1582theorem HInfinite_omega [simp]: "\<omega> \<in> HInfinite" 1583proof - 1584 have "\<forall>\<^sub>F n in \<U>. u < norm (1 + real n)" for u 1585 using FreeUltrafilterNat_nat_gt_real [of "u-1"] eventually_mono by fastforce 1586 then show ?thesis 1587 by (simp add: omega_def FreeUltrafilterNat_HInfinite) 1588qed 1589 1590 1591text \<open>Epsilon is a member of Infinitesimal.\<close> 1592 1593lemma Infinitesimal_epsilon [simp]: "\<epsilon> \<in> Infinitesimal" 1594 by (auto intro!: HInfinite_inverse_Infinitesimal HInfinite_omega 1595 simp add: epsilon_inverse_omega) 1596 1597lemma HFinite_epsilon [simp]: "\<epsilon> \<in> HFinite" 1598 by (auto intro: Infinitesimal_subset_HFinite [THEN subsetD]) 1599 1600lemma epsilon_approx_zero [simp]: "\<epsilon> \<approx> 0" 1601 by (simp add: mem_infmal_iff [symmetric]) 1602 1603text \<open>Needed for proof that we define a hyperreal \<open>[<X(n)] \<approx> hypreal_of_real a\<close> given 1604 that \<open>\<forall>n. |X n - a| < 1/n\<close>. Used in proof of \<open>NSLIM \<Rightarrow> LIM\<close>.\<close> 1605lemma real_of_nat_less_inverse_iff: "0 < u \<Longrightarrow> u < inverse (real(Suc n)) \<longleftrightarrow> real(Suc n) < inverse u" 1606 using less_imp_inverse_less by force 1607 1608lemma finite_inverse_real_of_posnat_gt_real: "0 < u \<Longrightarrow> finite {n. u < inverse (real (Suc n))}" 1609proof (simp only: real_of_nat_less_inverse_iff) 1610 have "{n. 1 + real n < inverse u} = {n. real n < inverse u - 1}" 1611 by fastforce 1612 then show "finite {n. real (Suc n) < inverse u}" 1613 using finite_real_of_nat_less_real [of "inverse u - 1"] 1614 by auto 1615qed 1616 1617lemma finite_inverse_real_of_posnat_ge_real: 1618 assumes "0 < u" 1619 shows "finite {n. u \<le> inverse (real (Suc n))}" 1620proof - 1621 have "\<forall>na. u \<le> inverse (1 + real na) \<longrightarrow> na \<le> ceiling (inverse u)" 1622 by (metis add.commute add1_zle_eq assms ceiling_mono ceiling_of_nat dual_order.order_iff_strict inverse_inverse_eq le_imp_inverse_le semiring_1_class.of_nat_simps(2)) 1623 then show ?thesis 1624 apply (auto simp add: finite_nat_set_iff_bounded_le) 1625 by (meson assms inverse_positive_iff_positive le_nat_iff less_imp_le zero_less_ceiling) 1626qed 1627 1628lemma inverse_real_of_posnat_ge_real_FreeUltrafilterNat: 1629 "0 < u \<Longrightarrow> \<not> eventually (\<lambda>n. u \<le> inverse(real(Suc n))) \<U>" 1630 by (blast intro!: FreeUltrafilterNat.finite finite_inverse_real_of_posnat_ge_real) 1631 1632lemma FreeUltrafilterNat_inverse_real_of_posnat: 1633 "0 < u \<Longrightarrow> eventually (\<lambda>n. inverse(real(Suc n)) < u) \<U>" 1634 by (drule inverse_real_of_posnat_ge_real_FreeUltrafilterNat) 1635 (simp add: FreeUltrafilterNat.eventually_not_iff not_le[symmetric]) 1636 1637text \<open>Example of an hypersequence (i.e. an extended standard sequence) 1638 whose term with an hypernatural suffix is an infinitesimal i.e. 1639 the whn'nth term of the hypersequence is a member of Infinitesimal\<close> 1640 1641lemma SEQ_Infinitesimal: "( *f* (\<lambda>n::nat. inverse(real(Suc n)))) whn \<in> Infinitesimal" 1642 by (simp add: hypnat_omega_def starfun_star_n star_n_inverse Infinitesimal_FreeUltrafilterNat_iff 1643 FreeUltrafilterNat_inverse_real_of_posnat del: of_nat_Suc) 1644 1645text \<open>Example where we get a hyperreal from a real sequence 1646 for which a particular property holds. The theorem is 1647 used in proofs about equivalence of nonstandard and 1648 standard neighbourhoods. Also used for equivalence of 1649 nonstandard ans standard definitions of pointwise 1650 limit.\<close> 1651 1652text \<open>\<open>|X(n) - x| < 1/n \<Longrightarrow> [<X n>] - hypreal_of_real x| \<in> Infinitesimal\<close>\<close> 1653lemma real_seq_to_hypreal_Infinitesimal: 1654 "\<forall>n. norm (X n - x) < inverse (real (Suc n)) \<Longrightarrow> star_n X - star_of x \<in> Infinitesimal" 1655 unfolding star_n_diff star_of_def Infinitesimal_FreeUltrafilterNat_iff star_n_inverse 1656 by (auto dest!: FreeUltrafilterNat_inverse_real_of_posnat 1657 intro: order_less_trans elim!: eventually_mono) 1658 1659lemma real_seq_to_hypreal_approx: 1660 "\<forall>n. norm (X n - x) < inverse (real (Suc n)) \<Longrightarrow> star_n X \<approx> star_of x" 1661 by (metis bex_Infinitesimal_iff real_seq_to_hypreal_Infinitesimal) 1662 1663lemma real_seq_to_hypreal_approx2: 1664 "\<forall>n. norm (x - X n) < inverse(real(Suc n)) \<Longrightarrow> star_n X \<approx> star_of x" 1665 by (metis norm_minus_commute real_seq_to_hypreal_approx) 1666 1667lemma real_seq_to_hypreal_Infinitesimal2: 1668 "\<forall>n. norm(X n - Y n) < inverse(real(Suc n)) \<Longrightarrow> star_n X - star_n Y \<in> Infinitesimal" 1669 unfolding Infinitesimal_FreeUltrafilterNat_iff star_n_diff 1670 by (auto dest!: FreeUltrafilterNat_inverse_real_of_posnat 1671 intro: order_less_trans elim!: eventually_mono) 1672 1673end 1674