1(* Title: HOL/Nonstandard_Analysis/CStar.thy 2 Author: Jacques D. Fleuriot 3 Copyright: 2001 University of Edinburgh 4*) 5 6section \<open>Star-transforms in NSA, Extending Sets of Complex Numbers and Complex Functions\<close> 7 8theory CStar 9 imports NSCA 10begin 11 12subsection \<open>Properties of the \<open>*\<close>-Transform Applied to Sets of Reals\<close> 13 14lemma STARC_hcomplex_of_complex_Int: "*s* X \<inter> SComplex = hcomplex_of_complex ` X" 15 by (auto simp: Standard_def) 16 17lemma lemma_not_hcomplexA: "x \<notin> hcomplex_of_complex ` A \<Longrightarrow> \<forall>y \<in> A. x \<noteq> hcomplex_of_complex y" 18 by auto 19 20 21subsection \<open>Theorems about Nonstandard Extensions of Functions\<close> 22 23lemma starfunC_hcpow: "\<And>Z. ( *f* (\<lambda>z. z ^ n)) Z = Z pow hypnat_of_nat n" 24 by transfer (rule refl) 25 26lemma starfunCR_cmod: "*f* cmod = hcmod" 27 by transfer (rule refl) 28 29 30subsection \<open>Internal Functions - Some Redundancy With \<open>*f*\<close> Now\<close> 31 32(** subtraction: ( *fn) - ( *gn) = *(fn - gn) **) 33(* 34lemma starfun_n_diff: 35 "( *fn* f) z - ( *fn* g) z = ( *fn* (\<lambda>i x. f i x - g i x)) z" 36apply (cases z) 37apply (simp add: starfun_n star_n_diff) 38done 39*) 40(** composition: ( *fn) o ( *gn) = *(fn o gn) **) 41 42lemma starfun_Re: "( *f* (\<lambda>x. Re (f x))) = (\<lambda>x. hRe (( *f* f) x))" 43 by transfer (rule refl) 44 45lemma starfun_Im: "( *f* (\<lambda>x. Im (f x))) = (\<lambda>x. hIm (( *f* f) x))" 46 by transfer (rule refl) 47 48lemma starfunC_eq_Re_Im_iff: 49 "( *f* f) x = z \<longleftrightarrow> ( *f* (\<lambda>x. Re (f x))) x = hRe z \<and> ( *f* (\<lambda>x. Im (f x))) x = hIm z" 50 by (simp add: hcomplex_hRe_hIm_cancel_iff starfun_Re starfun_Im) 51 52lemma starfunC_approx_Re_Im_iff: 53 "( *f* f) x \<approx> z \<longleftrightarrow> ( *f* (\<lambda>x. Re (f x))) x \<approx> hRe z \<and> ( *f* (\<lambda>x. Im (f x))) x \<approx> hIm z" 54 by (simp add: hcomplex_approx_iff starfun_Re starfun_Im) 55 56end 57