1(* Title: HOL/Nonstandard_Analysis/HyperDef.thy 2 Author: Jacques D. Fleuriot 3 Copyright: 1998 University of Cambridge 4 Conversion to Isar and new proofs by Lawrence C Paulson, 2004 5*) 6 7section \<open>Construction of Hyperreals Using Ultrafilters\<close> 8 9theory HyperDef 10 imports Complex_Main HyperNat 11begin 12 13type_synonym hypreal = "real star" 14 15abbreviation hypreal_of_real :: "real \<Rightarrow> real star" 16 where "hypreal_of_real \<equiv> star_of" 17 18abbreviation hypreal_of_hypnat :: "hypnat \<Rightarrow> hypreal" 19 where "hypreal_of_hypnat \<equiv> of_hypnat" 20 21definition omega :: hypreal ("\<omega>") 22 where "\<omega> = star_n (\<lambda>n. real (Suc n))" 23 \<comment> \<open>an infinite number \<open>= [<1, 2, 3, \<dots>>]\<close>\<close> 24 25definition epsilon :: hypreal ("\<epsilon>") 26 where "\<epsilon> = star_n (\<lambda>n. inverse (real (Suc n)))" 27 \<comment> \<open>an infinitesimal number \<open>= [<1, 1/2, 1/3, \<dots>>]\<close>\<close> 28 29 30subsection \<open>Real vector class instances\<close> 31 32instantiation star :: (scaleR) scaleR 33begin 34 definition star_scaleR_def [transfer_unfold]: "scaleR r \<equiv> *f* (scaleR r)" 35 instance .. 36end 37 38lemma Standard_scaleR [simp]: "x \<in> Standard \<Longrightarrow> scaleR r x \<in> Standard" 39 by (simp add: star_scaleR_def) 40 41lemma star_of_scaleR [simp]: "star_of (scaleR r x) = scaleR r (star_of x)" 42 by transfer (rule refl) 43 44instance star :: (real_vector) real_vector 45proof 46 fix a b :: real 47 show "\<And>x y::'a star. scaleR a (x + y) = scaleR a x + scaleR a y" 48 by transfer (rule scaleR_right_distrib) 49 show "\<And>x::'a star. scaleR (a + b) x = scaleR a x + scaleR b x" 50 by transfer (rule scaleR_left_distrib) 51 show "\<And>x::'a star. scaleR a (scaleR b x) = scaleR (a * b) x" 52 by transfer (rule scaleR_scaleR) 53 show "\<And>x::'a star. scaleR 1 x = x" 54 by transfer (rule scaleR_one) 55qed 56 57instance star :: (real_algebra) real_algebra 58proof 59 fix a :: real 60 show "\<And>x y::'a star. scaleR a x * y = scaleR a (x * y)" 61 by transfer (rule mult_scaleR_left) 62 show "\<And>x y::'a star. x * scaleR a y = scaleR a (x * y)" 63 by transfer (rule mult_scaleR_right) 64qed 65 66instance star :: (real_algebra_1) real_algebra_1 .. 67 68instance star :: (real_div_algebra) real_div_algebra .. 69 70instance star :: (field_char_0) field_char_0 .. 71 72instance star :: (real_field) real_field .. 73 74lemma star_of_real_def [transfer_unfold]: "of_real r = star_of (of_real r)" 75 by (unfold of_real_def, transfer, rule refl) 76 77lemma Standard_of_real [simp]: "of_real r \<in> Standard" 78 by (simp add: star_of_real_def) 79 80lemma star_of_of_real [simp]: "star_of (of_real r) = of_real r" 81 by transfer (rule refl) 82 83lemma of_real_eq_star_of [simp]: "of_real = star_of" 84proof 85 show "of_real r = star_of r" for r :: real 86 by transfer simp 87qed 88 89lemma Reals_eq_Standard: "(\<real> :: hypreal set) = Standard" 90 by (simp add: Reals_def Standard_def) 91 92 93subsection \<open>Injection from \<^typ>\<open>hypreal\<close>\<close> 94 95definition of_hypreal :: "hypreal \<Rightarrow> 'a::real_algebra_1 star" 96 where [transfer_unfold]: "of_hypreal = *f* of_real" 97 98lemma Standard_of_hypreal [simp]: "r \<in> Standard \<Longrightarrow> of_hypreal r \<in> Standard" 99 by (simp add: of_hypreal_def) 100 101lemma of_hypreal_0 [simp]: "of_hypreal 0 = 0" 102 by transfer (rule of_real_0) 103 104lemma of_hypreal_1 [simp]: "of_hypreal 1 = 1" 105 by transfer (rule of_real_1) 106 107lemma of_hypreal_add [simp]: "\<And>x y. of_hypreal (x + y) = of_hypreal x + of_hypreal y" 108 by transfer (rule of_real_add) 109 110lemma of_hypreal_minus [simp]: "\<And>x. of_hypreal (- x) = - of_hypreal x" 111 by transfer (rule of_real_minus) 112 113lemma of_hypreal_diff [simp]: "\<And>x y. of_hypreal (x - y) = of_hypreal x - of_hypreal y" 114 by transfer (rule of_real_diff) 115 116lemma of_hypreal_mult [simp]: "\<And>x y. of_hypreal (x * y) = of_hypreal x * of_hypreal y" 117 by transfer (rule of_real_mult) 118 119lemma of_hypreal_inverse [simp]: 120 "\<And>x. of_hypreal (inverse x) = 121 inverse (of_hypreal x :: 'a::{real_div_algebra, division_ring} star)" 122 by transfer (rule of_real_inverse) 123 124lemma of_hypreal_divide [simp]: 125 "\<And>x y. of_hypreal (x / y) = 126 (of_hypreal x / of_hypreal y :: 'a::{real_field, field} star)" 127 by transfer (rule of_real_divide) 128 129lemma of_hypreal_eq_iff [simp]: "\<And>x y. (of_hypreal x = of_hypreal y) = (x = y)" 130 by transfer (rule of_real_eq_iff) 131 132lemma of_hypreal_eq_0_iff [simp]: "\<And>x. (of_hypreal x = 0) = (x = 0)" 133 by transfer (rule of_real_eq_0_iff) 134 135 136subsection \<open>Properties of \<^term>\<open>starrel\<close>\<close> 137 138lemma lemma_starrel_refl [simp]: "x \<in> starrel `` {x}" 139 by (simp add: starrel_def) 140 141lemma starrel_in_hypreal [simp]: "starrel``{x}\<in>star" 142 by (simp add: star_def starrel_def quotient_def, blast) 143 144declare Abs_star_inject [simp] Abs_star_inverse [simp] 145declare equiv_starrel [THEN eq_equiv_class_iff, simp] 146 147 148subsection \<open>\<^term>\<open>hypreal_of_real\<close>: the Injection from \<^typ>\<open>real\<close> to \<^typ>\<open>hypreal\<close>\<close> 149 150lemma inj_star_of: "inj star_of" 151 by (rule inj_onI) simp 152 153lemma mem_Rep_star_iff: "X \<in> Rep_star x \<longleftrightarrow> x = star_n X" 154 by (cases x) (simp add: star_n_def) 155 156lemma Rep_star_star_n_iff [simp]: "X \<in> Rep_star (star_n Y) \<longleftrightarrow> eventually (\<lambda>n. Y n = X n) \<U>" 157 by (simp add: star_n_def) 158 159lemma Rep_star_star_n: "X \<in> Rep_star (star_n X)" 160 by simp 161 162 163subsection \<open>Properties of \<^term>\<open>star_n\<close>\<close> 164 165lemma star_n_add: "star_n X + star_n Y = star_n (\<lambda>n. X n + Y n)" 166 by (simp only: star_add_def starfun2_star_n) 167 168lemma star_n_minus: "- star_n X = star_n (\<lambda>n. -(X n))" 169 by (simp only: star_minus_def starfun_star_n) 170 171lemma star_n_diff: "star_n X - star_n Y = star_n (\<lambda>n. X n - Y n)" 172 by (simp only: star_diff_def starfun2_star_n) 173 174lemma star_n_mult: "star_n X * star_n Y = star_n (\<lambda>n. X n * Y n)" 175 by (simp only: star_mult_def starfun2_star_n) 176 177lemma star_n_inverse: "inverse (star_n X) = star_n (\<lambda>n. inverse (X n))" 178 by (simp only: star_inverse_def starfun_star_n) 179 180lemma star_n_le: "star_n X \<le> star_n Y = eventually (\<lambda>n. X n \<le> Y n) \<U>" 181 by (simp only: star_le_def starP2_star_n) 182 183lemma star_n_less: "star_n X < star_n Y = eventually (\<lambda>n. X n < Y n) \<U>" 184 by (simp only: star_less_def starP2_star_n) 185 186lemma star_n_zero_num: "0 = star_n (\<lambda>n. 0)" 187 by (simp only: star_zero_def star_of_def) 188 189lemma star_n_one_num: "1 = star_n (\<lambda>n. 1)" 190 by (simp only: star_one_def star_of_def) 191 192lemma star_n_abs: "\<bar>star_n X\<bar> = star_n (\<lambda>n. \<bar>X n\<bar>)" 193 by (simp only: star_abs_def starfun_star_n) 194 195lemma hypreal_omega_gt_zero [simp]: "0 < \<omega>" 196 by (simp add: omega_def star_n_zero_num star_n_less) 197 198 199subsection \<open>Existence of Infinite Hyperreal Number\<close> 200 201text \<open>Existence of infinite number not corresponding to any real number. 202 Use assumption that member \<^term>\<open>\<U>\<close> is not finite.\<close> 203 204lemma hypreal_of_real_not_eq_omega: "hypreal_of_real x \<noteq> \<omega>" 205proof - 206 have False if "\<forall>\<^sub>F n in \<U>. x = 1 + real n" for x 207 proof - 208 have "finite {n::nat. x = 1 + real n}" 209 by (simp add: finite_nat_set_iff_bounded_le) (metis add.commute nat_le_linear nat_le_real_less) 210 then show False 211 using FreeUltrafilterNat.finite that by blast 212 qed 213 then show ?thesis 214 by (auto simp add: omega_def star_of_def star_n_eq_iff) 215qed 216 217text \<open>Existence of infinitesimal number also not corresponding to any real number.\<close> 218 219lemma hypreal_of_real_not_eq_epsilon: "hypreal_of_real x \<noteq> \<epsilon>" 220proof - 221 have False if "\<forall>\<^sub>F n in \<U>. x = inverse (1 + real n)" for x 222 proof - 223 have "finite {n::nat. x = inverse (1 + real n)}" 224 by (simp add: finite_nat_set_iff_bounded_le) (metis add.commute inverse_inverse_eq linear nat_le_real_less of_nat_Suc) 225 then show False 226 using FreeUltrafilterNat.finite that by blast 227 qed 228 then show ?thesis 229 by (auto simp: epsilon_def star_of_def star_n_eq_iff) 230qed 231 232lemma epsilon_ge_zero [simp]: "0 \<le> \<epsilon>" 233 by (simp add: epsilon_def star_n_zero_num star_n_le) 234 235lemma epsilon_not_zero: "\<epsilon> \<noteq> 0" 236 using hypreal_of_real_not_eq_epsilon by force 237 238lemma epsilon_inverse_omega: "\<epsilon> = inverse \<omega>" 239 by (simp add: epsilon_def omega_def star_n_inverse) 240 241lemma epsilon_gt_zero: "0 < \<epsilon>" 242 by (simp add: epsilon_inverse_omega) 243 244 245subsection \<open>Embedding the Naturals into the Hyperreals\<close> 246 247abbreviation hypreal_of_nat :: "nat \<Rightarrow> hypreal" 248 where "hypreal_of_nat \<equiv> of_nat" 249 250lemma SNat_eq: "Nats = {n. \<exists>N. n = hypreal_of_nat N}" 251 by (simp add: Nats_def image_def) 252 253text \<open>Naturals embedded in hyperreals: is a hyperreal c.f. NS extension.\<close> 254 255lemma hypreal_of_nat: "hypreal_of_nat m = star_n (\<lambda>n. real m)" 256 by (simp add: star_of_def [symmetric]) 257 258declaration \<open> 259 K (Lin_Arith.add_simps @{thms star_of_zero star_of_one 260 star_of_numeral star_of_add 261 star_of_minus star_of_diff star_of_mult} 262 #> Lin_Arith.add_inj_thms @{thms star_of_le [THEN iffD2] 263 star_of_less [THEN iffD2] star_of_eq [THEN iffD2]} 264 #> Lin_Arith.add_inj_const (\<^const_name>\<open>StarDef.star_of\<close>, \<^typ>\<open>real \<Rightarrow> hypreal\<close>)) 265\<close> 266 267simproc_setup fast_arith_hypreal ("(m::hypreal) < n" | "(m::hypreal) \<le> n" | "(m::hypreal) = n") = 268 \<open>K Lin_Arith.simproc\<close> 269 270 271subsection \<open>Exponentials on the Hyperreals\<close> 272 273lemma hpowr_0 [simp]: "r ^ 0 = (1::hypreal)" 274 for r :: hypreal 275 by (rule power_0) 276 277lemma hpowr_Suc [simp]: "r ^ (Suc n) = r * (r ^ n)" 278 for r :: hypreal 279 by (rule power_Suc) 280 281lemma hrealpow_two: "r ^ Suc (Suc 0) = r * r" 282 for r :: hypreal 283 by simp 284 285lemma hrealpow_two_le [simp]: "0 \<le> r ^ Suc (Suc 0)" 286 for r :: hypreal 287 by (auto simp add: zero_le_mult_iff) 288 289lemma hrealpow_two_le_add_order [simp]: "0 \<le> u ^ Suc (Suc 0) + v ^ Suc (Suc 0)" 290 for u v :: hypreal 291 by (simp only: hrealpow_two_le add_nonneg_nonneg) 292 293lemma hrealpow_two_le_add_order2 [simp]: "0 \<le> u ^ Suc (Suc 0) + v ^ Suc (Suc 0) + w ^ Suc (Suc 0)" 294 for u v w :: hypreal 295 by (simp only: hrealpow_two_le add_nonneg_nonneg) 296 297lemma hypreal_add_nonneg_eq_0_iff: "0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> x + y = 0 \<longleftrightarrow> x = 0 \<and> y = 0" 298 for x y :: hypreal 299 by arith 300 301 302(* FIXME: DELETE THESE *) 303lemma hypreal_three_squares_add_zero_iff: "x * x + y * y + z * z = 0 \<longleftrightarrow> x = 0 \<and> y = 0 \<and> z = 0" 304 for x y z :: hypreal 305 by (simp only: zero_le_square add_nonneg_nonneg hypreal_add_nonneg_eq_0_iff) auto 306 307lemma hrealpow_three_squares_add_zero_iff [simp]: 308 "x ^ Suc (Suc 0) + y ^ Suc (Suc 0) + z ^ Suc (Suc 0) = 0 \<longleftrightarrow> x = 0 \<and> y = 0 \<and> z = 0" 309 for x y z :: hypreal 310 by (simp only: hypreal_three_squares_add_zero_iff hrealpow_two) 311 312(*FIXME: This and RealPow.abs_realpow_two should be replaced by an abstract 313 result proved in Rings or Fields*) 314lemma hrabs_hrealpow_two [simp]: "\<bar>x ^ Suc (Suc 0)\<bar> = x ^ Suc (Suc 0)" 315 for x :: hypreal 316 by (simp add: abs_mult) 317 318lemma two_hrealpow_ge_one [simp]: "(1::hypreal) \<le> 2 ^ n" 319 using power_increasing [of 0 n "2::hypreal"] by simp 320 321lemma hrealpow: "star_n X ^ m = star_n (\<lambda>n. (X n::real) ^ m)" 322 by (induct m) (auto simp: star_n_one_num star_n_mult) 323 324lemma hrealpow_sum_square_expand: 325 "(x + y) ^ Suc (Suc 0) = 326 x ^ Suc (Suc 0) + y ^ Suc (Suc 0) + (hypreal_of_nat (Suc (Suc 0))) * x * y" 327 for x y :: hypreal 328 by (simp add: distrib_left distrib_right) 329 330lemma power_hypreal_of_real_numeral: 331 "(numeral v :: hypreal) ^ n = hypreal_of_real ((numeral v) ^ n)" 332 by simp 333declare power_hypreal_of_real_numeral [of _ "numeral w", simp] for w 334 335lemma power_hypreal_of_real_neg_numeral: 336 "(- numeral v :: hypreal) ^ n = hypreal_of_real ((- numeral v) ^ n)" 337 by simp 338declare power_hypreal_of_real_neg_numeral [of _ "numeral w", simp] for w 339(* 340lemma hrealpow_HFinite: 341 fixes x :: "'a::{real_normed_algebra,power} star" 342 shows "x \<in> HFinite ==> x ^ n \<in> HFinite" 343apply (induct_tac "n") 344apply (auto simp add: power_Suc intro: HFinite_mult) 345done 346*) 347 348 349subsection \<open>Powers with Hypernatural Exponents\<close> 350 351text \<open>Hypernatural powers of hyperreals.\<close> 352definition pow :: "'a::power star \<Rightarrow> nat star \<Rightarrow> 'a star" (infixr "pow" 80) 353 where hyperpow_def [transfer_unfold]: "R pow N = ( *f2* (^)) R N" 354 355lemma Standard_hyperpow [simp]: "r \<in> Standard \<Longrightarrow> n \<in> Standard \<Longrightarrow> r pow n \<in> Standard" 356 by (simp add: hyperpow_def) 357 358lemma hyperpow: "star_n X pow star_n Y = star_n (\<lambda>n. X n ^ Y n)" 359 by (simp add: hyperpow_def starfun2_star_n) 360 361lemma hyperpow_zero [simp]: "\<And>n. (0::'a::{power,semiring_0} star) pow (n + (1::hypnat)) = 0" 362 by transfer simp 363 364lemma hyperpow_not_zero: "\<And>r n. r \<noteq> (0::'a::{field} star) \<Longrightarrow> r pow n \<noteq> 0" 365 by transfer (rule power_not_zero) 366 367lemma hyperpow_inverse: "\<And>r n. r \<noteq> (0::'a::field star) \<Longrightarrow> inverse (r pow n) = (inverse r) pow n" 368 by transfer (rule power_inverse [symmetric]) 369 370lemma hyperpow_hrabs: "\<And>r n. \<bar>r::'a::{linordered_idom} star\<bar> pow n = \<bar>r pow n\<bar>" 371 by transfer (rule power_abs [symmetric]) 372 373lemma hyperpow_add: "\<And>r n m. (r::'a::monoid_mult star) pow (n + m) = (r pow n) * (r pow m)" 374 by transfer (rule power_add) 375 376lemma hyperpow_one [simp]: "\<And>r. (r::'a::monoid_mult star) pow (1::hypnat) = r" 377 by transfer (rule power_one_right) 378 379lemma hyperpow_two: "\<And>r. (r::'a::monoid_mult star) pow (2::hypnat) = r * r" 380 by transfer (rule power2_eq_square) 381 382lemma hyperpow_gt_zero: "\<And>r n. (0::'a::{linordered_semidom} star) < r \<Longrightarrow> 0 < r pow n" 383 by transfer (rule zero_less_power) 384 385lemma hyperpow_ge_zero: "\<And>r n. (0::'a::{linordered_semidom} star) \<le> r \<Longrightarrow> 0 \<le> r pow n" 386 by transfer (rule zero_le_power) 387 388lemma hyperpow_le: "\<And>x y n. (0::'a::{linordered_semidom} star) < x \<Longrightarrow> x \<le> y \<Longrightarrow> x pow n \<le> y pow n" 389 by transfer (rule power_mono [OF _ order_less_imp_le]) 390 391lemma hyperpow_eq_one [simp]: "\<And>n. 1 pow n = (1::'a::monoid_mult star)" 392 by transfer (rule power_one) 393 394lemma hrabs_hyperpow_minus [simp]: "\<And>(a::'a::linordered_idom star) n. \<bar>(-a) pow n\<bar> = \<bar>a pow n\<bar>" 395 by transfer (rule abs_power_minus) 396 397lemma hyperpow_mult: "\<And>r s n. (r * s::'a::comm_monoid_mult star) pow n = (r pow n) * (s pow n)" 398 by transfer (rule power_mult_distrib) 399 400lemma hyperpow_two_le [simp]: "\<And>r. (0::'a::{monoid_mult,linordered_ring_strict} star) \<le> r pow 2" 401 by (auto simp add: hyperpow_two zero_le_mult_iff) 402 403lemma hyperpow_two_hrabs [simp]: "\<bar>x::'a::linordered_idom star\<bar> pow 2 = x pow 2" 404 by (simp add: hyperpow_hrabs) 405 406lemma hyperpow_two_gt_one: "\<And>r::'a::linordered_semidom star. 1 < r \<Longrightarrow> 1 < r pow 2" 407 by transfer simp 408 409lemma hyperpow_two_ge_one: "\<And>r::'a::linordered_semidom star. 1 \<le> r \<Longrightarrow> 1 \<le> r pow 2" 410 by transfer (rule one_le_power) 411 412lemma two_hyperpow_ge_one [simp]: "(1::hypreal) \<le> 2 pow n" 413 by (metis hyperpow_eq_one hyperpow_le one_le_numeral zero_less_one) 414 415lemma hyperpow_minus_one2 [simp]: "\<And>n. (- 1) pow (2 * n) = (1::hypreal)" 416 by transfer (rule power_minus1_even) 417 418lemma hyperpow_less_le: "\<And>r n N. (0::hypreal) \<le> r \<Longrightarrow> r \<le> 1 \<Longrightarrow> n < N \<Longrightarrow> r pow N \<le> r pow n" 419 by transfer (rule power_decreasing [OF order_less_imp_le]) 420 421lemma hyperpow_SHNat_le: 422 "0 \<le> r \<Longrightarrow> r \<le> (1::hypreal) \<Longrightarrow> N \<in> HNatInfinite \<Longrightarrow> \<forall>n\<in>Nats. r pow N \<le> r pow n" 423 by (auto intro!: hyperpow_less_le simp: HNatInfinite_iff) 424 425lemma hyperpow_realpow: "(hypreal_of_real r) pow (hypnat_of_nat n) = hypreal_of_real (r ^ n)" 426 by transfer (rule refl) 427 428lemma hyperpow_SReal [simp]: "(hypreal_of_real r) pow (hypnat_of_nat n) \<in> \<real>" 429 by (simp add: Reals_eq_Standard) 430 431lemma hyperpow_zero_HNatInfinite [simp]: "N \<in> HNatInfinite \<Longrightarrow> (0::hypreal) pow N = 0" 432 by (drule HNatInfinite_is_Suc, auto) 433 434lemma hyperpow_le_le: "(0::hypreal) \<le> r \<Longrightarrow> r \<le> 1 \<Longrightarrow> n \<le> N \<Longrightarrow> r pow N \<le> r pow n" 435 by (metis hyperpow_less_le le_less) 436 437lemma hyperpow_Suc_le_self2: "(0::hypreal) \<le> r \<Longrightarrow> r < 1 \<Longrightarrow> r pow (n + (1::hypnat)) \<le> r" 438 by (metis hyperpow_less_le hyperpow_one hypnat_add_self_le le_less) 439 440lemma hyperpow_hypnat_of_nat: "\<And>x. x pow hypnat_of_nat n = x ^ n" 441 by transfer (rule refl) 442 443lemma of_hypreal_hyperpow: 444 "\<And>x n. of_hypreal (x pow n) = (of_hypreal x::'a::{real_algebra_1} star) pow n" 445 by transfer (rule of_real_power) 446 447end 448