1(* Title: HOL/Nonstandard_Analysis/NSCA.thy 2 Author: Jacques D. Fleuriot 3 Copyright: 2001, 2002 University of Edinburgh 4*) 5 6section\<open>Non-Standard Complex Analysis\<close> 7 8theory NSCA 9imports NSComplex HTranscendental 10begin 11 12abbreviation 13 (* standard complex numbers reagarded as an embedded subset of NS complex *) 14 SComplex :: "hcomplex set" where 15 "SComplex \<equiv> Standard" 16 17definition \<comment> \<open>standard part map\<close> 18 stc :: "hcomplex => hcomplex" where 19 "stc x = (SOME r. x \<in> HFinite \<and> r\<in>SComplex \<and> r \<approx> x)" 20 21 22subsection\<open>Closure Laws for SComplex, the Standard Complex Numbers\<close> 23 24lemma SComplex_minus_iff [simp]: "(-x \<in> SComplex) = (x \<in> SComplex)" 25 using Standard_minus by fastforce 26 27lemma SComplex_add_cancel: 28 "\<lbrakk>x + y \<in> SComplex; y \<in> SComplex\<rbrakk> \<Longrightarrow> x \<in> SComplex" 29 using Standard_diff by fastforce 30 31lemma SReal_hcmod_hcomplex_of_complex [simp]: 32 "hcmod (hcomplex_of_complex r) \<in> \<real>" 33 by (simp add: Reals_eq_Standard) 34 35lemma SReal_hcmod_numeral: "hcmod (numeral w ::hcomplex) \<in> \<real>" 36 by simp 37 38lemma SReal_hcmod_SComplex: "x \<in> SComplex \<Longrightarrow> hcmod x \<in> \<real>" 39 by (simp add: Reals_eq_Standard) 40 41lemma SComplex_divide_numeral: 42 "r \<in> SComplex \<Longrightarrow> r/(numeral w::hcomplex) \<in> SComplex" 43 by simp 44 45lemma SComplex_UNIV_complex: 46 "{x. hcomplex_of_complex x \<in> SComplex} = (UNIV::complex set)" 47 by simp 48 49lemma SComplex_iff: "(x \<in> SComplex) = (\<exists>y. x = hcomplex_of_complex y)" 50 by (simp add: Standard_def image_def) 51 52lemma hcomplex_of_complex_image: 53 "range hcomplex_of_complex = SComplex" 54 by (simp add: Standard_def) 55 56lemma inv_hcomplex_of_complex_image: "inv hcomplex_of_complex `SComplex = UNIV" 57by (auto simp add: Standard_def image_def) (metis inj_star_of inv_f_f) 58 59lemma SComplex_hcomplex_of_complex_image: 60 "\<lbrakk>\<exists>x. x \<in> P; P \<le> SComplex\<rbrakk> \<Longrightarrow> \<exists>Q. P = hcomplex_of_complex ` Q" 61 by (metis Standard_def subset_imageE) 62 63lemma SComplex_SReal_dense: 64 "\<lbrakk>x \<in> SComplex; y \<in> SComplex; hcmod x < hcmod y 65 \<rbrakk> \<Longrightarrow> \<exists>r \<in> Reals. hcmod x< r \<and> r < hcmod y" 66 by (simp add: SReal_dense SReal_hcmod_SComplex) 67 68 69subsection\<open>The Finite Elements form a Subring\<close> 70 71lemma HFinite_hcmod_hcomplex_of_complex [simp]: 72 "hcmod (hcomplex_of_complex r) \<in> HFinite" 73 by (auto intro!: SReal_subset_HFinite [THEN subsetD]) 74 75lemma HFinite_hcmod_iff [simp]: "hcmod x \<in> HFinite \<longleftrightarrow> x \<in> HFinite" 76 by (simp add: HFinite_def) 77 78lemma HFinite_bounded_hcmod: 79 "\<lbrakk>x \<in> HFinite; y \<le> hcmod x; 0 \<le> y\<rbrakk> \<Longrightarrow> y \<in> HFinite" 80 using HFinite_bounded HFinite_hcmod_iff by blast 81 82 83subsection\<open>The Complex Infinitesimals form a Subring\<close> 84 85lemma Infinitesimal_hcmod_iff: 86 "(z \<in> Infinitesimal) = (hcmod z \<in> Infinitesimal)" 87 by (simp add: Infinitesimal_def) 88 89lemma HInfinite_hcmod_iff: "(z \<in> HInfinite) = (hcmod z \<in> HInfinite)" 90 by (simp add: HInfinite_def) 91 92lemma HFinite_diff_Infinitesimal_hcmod: 93 "x \<in> HFinite - Infinitesimal \<Longrightarrow> hcmod x \<in> HFinite - Infinitesimal" 94 by (simp add: Infinitesimal_hcmod_iff) 95 96lemma hcmod_less_Infinitesimal: 97 "\<lbrakk>e \<in> Infinitesimal; hcmod x < hcmod e\<rbrakk> \<Longrightarrow> x \<in> Infinitesimal" 98 by (auto elim: hrabs_less_Infinitesimal simp add: Infinitesimal_hcmod_iff) 99 100lemma hcmod_le_Infinitesimal: 101 "\<lbrakk>e \<in> Infinitesimal; hcmod x \<le> hcmod e\<rbrakk> \<Longrightarrow> x \<in> Infinitesimal" 102 by (auto elim: hrabs_le_Infinitesimal simp add: Infinitesimal_hcmod_iff) 103 104 105subsection\<open>The ``Infinitely Close'' Relation\<close> 106 107lemma approx_SComplex_mult_cancel_zero: 108 "\<lbrakk>a \<in> SComplex; a \<noteq> 0; a*x \<approx> 0\<rbrakk> \<Longrightarrow> x \<approx> 0" 109 by (metis Infinitesimal_mult_disj SComplex_iff mem_infmal_iff star_of_Infinitesimal_iff_0 star_zero_def) 110 111lemma approx_mult_SComplex1: "\<lbrakk>a \<in> SComplex; x \<approx> 0\<rbrakk> \<Longrightarrow> x*a \<approx> 0" 112 using SComplex_iff approx_mult_subst_star_of by fastforce 113 114lemma approx_mult_SComplex2: "\<lbrakk>a \<in> SComplex; x \<approx> 0\<rbrakk> \<Longrightarrow> a*x \<approx> 0" 115 by (metis approx_mult_SComplex1 mult.commute) 116 117lemma approx_mult_SComplex_zero_cancel_iff [simp]: 118 "\<lbrakk>a \<in> SComplex; a \<noteq> 0\<rbrakk> \<Longrightarrow> (a*x \<approx> 0) = (x \<approx> 0)" 119 using approx_SComplex_mult_cancel_zero approx_mult_SComplex2 by blast 120 121lemma approx_SComplex_mult_cancel: 122 "\<lbrakk>a \<in> SComplex; a \<noteq> 0; a*w \<approx> a*z\<rbrakk> \<Longrightarrow> w \<approx> z" 123 by (metis approx_SComplex_mult_cancel_zero approx_minus_iff right_diff_distrib) 124 125lemma approx_SComplex_mult_cancel_iff1 [simp]: 126 "\<lbrakk>a \<in> SComplex; a \<noteq> 0\<rbrakk> \<Longrightarrow> (a*w \<approx> a*z) = (w \<approx> z)" 127 by (metis HFinite_star_of SComplex_iff approx_SComplex_mult_cancel approx_mult2) 128 129(* TODO: generalize following theorems: hcmod -> hnorm *) 130 131lemma approx_hcmod_approx_zero: "(x \<approx> y) = (hcmod (y - x) \<approx> 0)" 132 by (simp add: Infinitesimal_hcmod_iff approx_def hnorm_minus_commute) 133 134lemma approx_approx_zero_iff: "(x \<approx> 0) = (hcmod x \<approx> 0)" 135by (simp add: approx_hcmod_approx_zero) 136 137lemma approx_minus_zero_cancel_iff [simp]: "(-x \<approx> 0) = (x \<approx> 0)" 138by (simp add: approx_def) 139 140lemma Infinitesimal_hcmod_add_diff: 141 "u \<approx> 0 \<Longrightarrow> hcmod(x + u) - hcmod x \<in> Infinitesimal" 142 by (metis add.commute add.left_neutral approx_add_right_iff approx_def approx_hnorm) 143 144lemma approx_hcmod_add_hcmod: "u \<approx> 0 \<Longrightarrow> hcmod(x + u) \<approx> hcmod x" 145 using Infinitesimal_hcmod_add_diff approx_def by blast 146 147 148subsection\<open>Zero is the Only Infinitesimal Complex Number\<close> 149 150lemma Infinitesimal_less_SComplex: 151 "\<lbrakk>x \<in> SComplex; y \<in> Infinitesimal; 0 < hcmod x\<rbrakk> \<Longrightarrow> hcmod y < hcmod x" 152 by (auto intro: Infinitesimal_less_SReal SReal_hcmod_SComplex simp add: Infinitesimal_hcmod_iff) 153 154lemma SComplex_Int_Infinitesimal_zero: "SComplex Int Infinitesimal = {0}" 155 by (auto simp add: Standard_def Infinitesimal_hcmod_iff) 156 157lemma SComplex_Infinitesimal_zero: 158 "\<lbrakk>x \<in> SComplex; x \<in> Infinitesimal\<rbrakk> \<Longrightarrow> x = 0" 159 using SComplex_iff by auto 160 161lemma SComplex_HFinite_diff_Infinitesimal: 162 "\<lbrakk>x \<in> SComplex; x \<noteq> 0\<rbrakk> \<Longrightarrow> x \<in> HFinite - Infinitesimal" 163 using SComplex_iff by auto 164 165lemma numeral_not_Infinitesimal [simp]: 166 "numeral w \<noteq> (0::hcomplex) \<Longrightarrow> (numeral w::hcomplex) \<notin> Infinitesimal" 167 by (fast dest: Standard_numeral [THEN SComplex_Infinitesimal_zero]) 168 169lemma approx_SComplex_not_zero: 170 "\<lbrakk>y \<in> SComplex; x \<approx> y; y\<noteq> 0\<rbrakk> \<Longrightarrow> x \<noteq> 0" 171 by (auto dest: SComplex_Infinitesimal_zero approx_sym [THEN mem_infmal_iff [THEN iffD2]]) 172 173lemma SComplex_approx_iff: 174 "\<lbrakk>x \<in> SComplex; y \<in> SComplex\<rbrakk> \<Longrightarrow> (x \<approx> y) = (x = y)" 175 by (auto simp add: Standard_def) 176 177lemma approx_unique_complex: 178 "\<lbrakk>r \<in> SComplex; s \<in> SComplex; r \<approx> x; s \<approx> x\<rbrakk> \<Longrightarrow> r = s" 179 by (blast intro: SComplex_approx_iff [THEN iffD1] approx_trans2) 180 181subsection \<open>Properties of \<^term>\<open>hRe\<close>, \<^term>\<open>hIm\<close> and \<^term>\<open>HComplex\<close>\<close> 182 183lemma abs_hRe_le_hcmod: "\<And>x. \<bar>hRe x\<bar> \<le> hcmod x" 184 by transfer (rule abs_Re_le_cmod) 185 186lemma abs_hIm_le_hcmod: "\<And>x. \<bar>hIm x\<bar> \<le> hcmod x" 187 by transfer (rule abs_Im_le_cmod) 188 189lemma Infinitesimal_hRe: "x \<in> Infinitesimal \<Longrightarrow> hRe x \<in> Infinitesimal" 190 using Infinitesimal_hcmod_iff abs_hRe_le_hcmod hrabs_le_Infinitesimal by blast 191 192lemma Infinitesimal_hIm: "x \<in> Infinitesimal \<Longrightarrow> hIm x \<in> Infinitesimal" 193 using Infinitesimal_hcmod_iff abs_hIm_le_hcmod hrabs_le_Infinitesimal by blast 194 195lemma Infinitesimal_HComplex: 196 assumes x: "x \<in> Infinitesimal" and y: "y \<in> Infinitesimal" 197 shows "HComplex x y \<in> Infinitesimal" 198proof - 199 have "hcmod (HComplex 0 y) \<in> Infinitesimal" 200 by (simp add: hcmod_i y) 201 moreover have "hcmod (hcomplex_of_hypreal x) \<in> Infinitesimal" 202 using Infinitesimal_hcmod_iff Infinitesimal_of_hypreal_iff x by blast 203 ultimately have "hcmod (HComplex x y) \<in> Infinitesimal" 204 by (metis Infinitesimal_add Infinitesimal_hcmod_iff add.right_neutral hcomplex_of_hypreal_add_HComplex) 205 then show ?thesis 206 by (simp add: Infinitesimal_hnorm_iff) 207qed 208 209lemma hcomplex_Infinitesimal_iff: 210 "(x \<in> Infinitesimal) \<longleftrightarrow> (hRe x \<in> Infinitesimal \<and> hIm x \<in> Infinitesimal)" 211 using Infinitesimal_HComplex Infinitesimal_hIm Infinitesimal_hRe by fastforce 212 213lemma hRe_diff [simp]: "\<And>x y. hRe (x - y) = hRe x - hRe y" 214 by transfer simp 215 216lemma hIm_diff [simp]: "\<And>x y. hIm (x - y) = hIm x - hIm y" 217 by transfer simp 218 219lemma approx_hRe: "x \<approx> y \<Longrightarrow> hRe x \<approx> hRe y" 220 unfolding approx_def by (drule Infinitesimal_hRe) simp 221 222lemma approx_hIm: "x \<approx> y \<Longrightarrow> hIm x \<approx> hIm y" 223 unfolding approx_def by (drule Infinitesimal_hIm) simp 224 225lemma approx_HComplex: 226 "\<lbrakk>a \<approx> b; c \<approx> d\<rbrakk> \<Longrightarrow> HComplex a c \<approx> HComplex b d" 227 unfolding approx_def by (simp add: Infinitesimal_HComplex) 228 229lemma hcomplex_approx_iff: 230 "(x \<approx> y) = (hRe x \<approx> hRe y \<and> hIm x \<approx> hIm y)" 231 unfolding approx_def by (simp add: hcomplex_Infinitesimal_iff) 232 233lemma HFinite_hRe: "x \<in> HFinite \<Longrightarrow> hRe x \<in> HFinite" 234 using HFinite_bounded_hcmod abs_ge_zero abs_hRe_le_hcmod by blast 235 236lemma HFinite_hIm: "x \<in> HFinite \<Longrightarrow> hIm x \<in> HFinite" 237 using HFinite_bounded_hcmod abs_ge_zero abs_hIm_le_hcmod by blast 238 239lemma HFinite_HComplex: 240 assumes "x \<in> HFinite" "y \<in> HFinite" 241 shows "HComplex x y \<in> HFinite" 242proof - 243 have "HComplex x 0 \<in> HFinite" "HComplex 0 y \<in> HFinite" 244 using HFinite_hcmod_iff assms hcmod_i by fastforce+ 245 then have "HComplex x 0 + HComplex 0 y \<in> HFinite" 246 using HFinite_add by blast 247 then show ?thesis 248 by simp 249qed 250 251lemma hcomplex_HFinite_iff: 252 "(x \<in> HFinite) = (hRe x \<in> HFinite \<and> hIm x \<in> HFinite)" 253 using HFinite_HComplex HFinite_hIm HFinite_hRe by fastforce 254 255lemma hcomplex_HInfinite_iff: 256 "(x \<in> HInfinite) = (hRe x \<in> HInfinite \<or> hIm x \<in> HInfinite)" 257 by (simp add: HInfinite_HFinite_iff hcomplex_HFinite_iff) 258 259lemma hcomplex_of_hypreal_approx_iff [simp]: 260 "(hcomplex_of_hypreal x \<approx> hcomplex_of_hypreal z) = (x \<approx> z)" 261 by (simp add: hcomplex_approx_iff) 262 263(* Here we go - easy proof now!! *) 264lemma stc_part_Ex: 265 assumes "x \<in> HFinite" 266 shows "\<exists>t \<in> SComplex. x \<approx> t" 267proof - 268 let ?t = "HComplex (st (hRe x)) (st (hIm x))" 269 have "?t \<in> SComplex" 270 using HFinite_hIm HFinite_hRe Reals_eq_Standard assms st_SReal by auto 271 moreover have "x \<approx> ?t" 272 by (simp add: HFinite_hIm HFinite_hRe assms hcomplex_approx_iff st_HFinite st_eq_approx) 273 ultimately show ?thesis .. 274qed 275 276lemma stc_part_Ex1: "x \<in> HFinite \<Longrightarrow> \<exists>!t. t \<in> SComplex \<and> x \<approx> t" 277 using approx_sym approx_unique_complex stc_part_Ex by blast 278 279 280subsection\<open>Theorems About Monads\<close> 281 282lemma monad_zero_hcmod_iff: "(x \<in> monad 0) = (hcmod x \<in> monad 0)" 283 by (simp add: Infinitesimal_monad_zero_iff [symmetric] Infinitesimal_hcmod_iff) 284 285 286subsection\<open>Theorems About Standard Part\<close> 287 288lemma stc_approx_self: "x \<in> HFinite \<Longrightarrow> stc x \<approx> x" 289 unfolding stc_def 290 by (metis (no_types, lifting) approx_reorient someI_ex stc_part_Ex1) 291 292lemma stc_SComplex: "x \<in> HFinite \<Longrightarrow> stc x \<in> SComplex" 293 unfolding stc_def 294 by (metis (no_types, lifting) SComplex_iff approx_sym someI_ex stc_part_Ex) 295 296lemma stc_HFinite: "x \<in> HFinite \<Longrightarrow> stc x \<in> HFinite" 297 by (erule stc_SComplex [THEN Standard_subset_HFinite [THEN subsetD]]) 298 299lemma stc_unique: "\<lbrakk>y \<in> SComplex; y \<approx> x\<rbrakk> \<Longrightarrow> stc x = y" 300 by (metis SComplex_approx_iff SComplex_iff approx_monad_iff approx_star_of_HFinite stc_SComplex stc_approx_self) 301 302lemma stc_SComplex_eq [simp]: "x \<in> SComplex \<Longrightarrow> stc x = x" 303 by (simp add: stc_unique) 304 305lemma stc_eq_approx: 306 "\<lbrakk>x \<in> HFinite; y \<in> HFinite; stc x = stc y\<rbrakk> \<Longrightarrow> x \<approx> y" 307 by (auto dest!: stc_approx_self elim!: approx_trans3) 308 309lemma approx_stc_eq: 310 "\<lbrakk>x \<in> HFinite; y \<in> HFinite; x \<approx> y\<rbrakk> \<Longrightarrow> stc x = stc y" 311 by (metis approx_sym approx_trans3 stc_part_Ex1 stc_unique) 312 313lemma stc_eq_approx_iff: 314 "\<lbrakk>x \<in> HFinite; y \<in> HFinite\<rbrakk> \<Longrightarrow> (x \<approx> y) = (stc x = stc y)" 315 by (blast intro: approx_stc_eq stc_eq_approx) 316 317lemma stc_Infinitesimal_add_SComplex: 318 "\<lbrakk>x \<in> SComplex; e \<in> Infinitesimal\<rbrakk> \<Longrightarrow> stc(x + e) = x" 319 using Infinitesimal_add_approx_self stc_unique by blast 320 321lemma stc_Infinitesimal_add_SComplex2: 322 "\<lbrakk>x \<in> SComplex; e \<in> Infinitesimal\<rbrakk> \<Longrightarrow> stc(e + x) = x" 323 using Infinitesimal_add_approx_self2 stc_unique by blast 324 325lemma HFinite_stc_Infinitesimal_add: 326 "x \<in> HFinite \<Longrightarrow> \<exists>e \<in> Infinitesimal. x = stc(x) + e" 327 by (blast dest!: stc_approx_self [THEN approx_sym] bex_Infinitesimal_iff2 [THEN iffD2]) 328 329lemma stc_add: 330 "\<lbrakk>x \<in> HFinite; y \<in> HFinite\<rbrakk> \<Longrightarrow> stc (x + y) = stc(x) + stc(y)" 331 by (simp add: stc_unique stc_SComplex stc_approx_self approx_add) 332 333lemma stc_zero: "stc 0 = 0" 334 by simp 335 336lemma stc_one: "stc 1 = 1" 337 by simp 338 339lemma stc_minus: "y \<in> HFinite \<Longrightarrow> stc(-y) = -stc(y)" 340 by (simp add: stc_unique stc_SComplex stc_approx_self approx_minus) 341 342lemma stc_diff: 343 "\<lbrakk>x \<in> HFinite; y \<in> HFinite\<rbrakk> \<Longrightarrow> stc (x-y) = stc(x) - stc(y)" 344 by (simp add: stc_unique stc_SComplex stc_approx_self approx_diff) 345 346lemma stc_mult: 347 "\<lbrakk>x \<in> HFinite; y \<in> HFinite\<rbrakk> 348 \<Longrightarrow> stc (x * y) = stc(x) * stc(y)" 349 by (simp add: stc_unique stc_SComplex stc_approx_self approx_mult_HFinite) 350 351lemma stc_Infinitesimal: "x \<in> Infinitesimal \<Longrightarrow> stc x = 0" 352 by (simp add: stc_unique mem_infmal_iff) 353 354lemma stc_not_Infinitesimal: "stc(x) \<noteq> 0 \<Longrightarrow> x \<notin> Infinitesimal" 355 by (fast intro: stc_Infinitesimal) 356 357lemma stc_inverse: 358 "\<lbrakk>x \<in> HFinite; stc x \<noteq> 0\<rbrakk> \<Longrightarrow> stc(inverse x) = inverse (stc x)" 359 by (simp add: stc_unique stc_SComplex stc_approx_self approx_inverse stc_not_Infinitesimal) 360 361lemma stc_divide [simp]: 362 "\<lbrakk>x \<in> HFinite; y \<in> HFinite; stc y \<noteq> 0\<rbrakk> 363 \<Longrightarrow> stc(x/y) = (stc x) / (stc y)" 364 by (simp add: divide_inverse stc_mult stc_not_Infinitesimal HFinite_inverse stc_inverse) 365 366lemma stc_idempotent [simp]: "x \<in> HFinite \<Longrightarrow> stc(stc(x)) = stc(x)" 367 by (blast intro: stc_HFinite stc_approx_self approx_stc_eq) 368 369lemma HFinite_HFinite_hcomplex_of_hypreal: 370 "z \<in> HFinite \<Longrightarrow> hcomplex_of_hypreal z \<in> HFinite" 371 by (simp add: hcomplex_HFinite_iff) 372 373lemma SComplex_SReal_hcomplex_of_hypreal: 374 "x \<in> \<real> \<Longrightarrow> hcomplex_of_hypreal x \<in> SComplex" 375 by (simp add: Reals_eq_Standard) 376 377lemma stc_hcomplex_of_hypreal: 378 "z \<in> HFinite \<Longrightarrow> stc(hcomplex_of_hypreal z) = hcomplex_of_hypreal (st z)" 379 by (simp add: SComplex_SReal_hcomplex_of_hypreal st_SReal st_approx_self stc_unique) 380 381lemma hmod_stc_eq: 382 assumes "x \<in> HFinite" 383 shows "hcmod(stc x) = st(hcmod x)" 384 by (metis SReal_hcmod_SComplex approx_HFinite approx_hnorm assms st_unique stc_SComplex_eq stc_eq_approx_iff stc_part_Ex) 385 386lemma Infinitesimal_hcnj_iff [simp]: 387 "(hcnj z \<in> Infinitesimal) \<longleftrightarrow> (z \<in> Infinitesimal)" 388 by (simp add: Infinitesimal_hcmod_iff) 389 390end 391