src/HOL/Complex/NSCA.thy
changeset 14408 0cc42bb96330
parent 14387 e96d5c42c4b0
child 14430 5cb24165a2e1
     1.1 --- a/src/HOL/Complex/NSCA.thy	Sat Feb 21 20:05:16 2004 +0100
     1.2 +++ b/src/HOL/Complex/NSCA.thy	Mon Feb 23 16:35:46 2004 +0100
     1.3 @@ -1,44 +1,1461 @@
     1.4  (*  Title       : NSCA.thy
     1.5      Author      : Jacques D. Fleuriot
     1.6      Copyright   : 2001,2002 University of Edinburgh
     1.7 -    Description : Infinite, infinitesimal complex number etc! 
     1.8  *)
     1.9  
    1.10 -NSCA = NSComplex + 
    1.11 +header{*Non-Standard Complex Analysis*}
    1.12  
    1.13 -consts   
    1.14 +theory NSCA = NSComplex:
    1.15  
    1.16 -    (* infinitely close *)
    1.17 -    "@c="     :: [hcomplex,hcomplex] => bool  (infixl 50)  
    1.18 +constdefs
    1.19  
    1.20 +    capprox    :: "[hcomplex,hcomplex] => bool"  (infixl "@c=" 50)  
    1.21 +      --{*the ``infinitely close'' relation*}
    1.22 +      "x @c= y == (x - y) \<in> CInfinitesimal"     
    1.23    
    1.24 -constdefs
    1.25     (* standard complex numbers reagarded as an embedded subset of NS complex *)
    1.26     SComplex  :: "hcomplex set"
    1.27 -   "SComplex == {x. EX r. x = hcomplex_of_complex r}"
    1.28 +   "SComplex == {x. \<exists>r. x = hcomplex_of_complex r}"
    1.29  
    1.30     CInfinitesimal  :: "hcomplex set"
    1.31 -   "CInfinitesimal == {x. ALL r: Reals. 0 < r --> hcmod x < r}"
    1.32 +   "CInfinitesimal == {x. \<forall>r \<in> Reals. 0 < r --> hcmod x < r}"
    1.33  
    1.34     CFinite :: "hcomplex set"
    1.35 -   "CFinite == {x. EX r: Reals. hcmod x < r}"
    1.36 +   "CFinite == {x. \<exists>r \<in> Reals. hcmod x < r}"
    1.37  
    1.38     CInfinite :: "hcomplex set"
    1.39 -   "CInfinite == {x. ALL r: Reals. r < hcmod x}"
    1.40 +   "CInfinite == {x. \<forall>r \<in> Reals. r < hcmod x}"
    1.41  
    1.42 -   (* standard part map *)  
    1.43 -   stc :: hcomplex => hcomplex
    1.44 -   "stc x == (@r. x : CFinite & r:SComplex & r @c= x)"
    1.45 +   stc :: "hcomplex => hcomplex"
    1.46 +    --{* standard part map*}
    1.47 +   "stc x == (@r. x \<in> CFinite & r:SComplex & r @c= x)"
    1.48  
    1.49 -   cmonad    :: hcomplex => hcomplex set
    1.50 +   cmonad    :: "hcomplex => hcomplex set"
    1.51     "cmonad x  == {y. x @c= y}"
    1.52  
    1.53 -   cgalaxy   :: hcomplex => hcomplex set
    1.54 -   "cgalaxy x == {y. (x - y) : CFinite}"
    1.55 +   cgalaxy   :: "hcomplex => hcomplex set"
    1.56 +   "cgalaxy x == {y. (x - y) \<in> CFinite}"
    1.57 +
    1.58 +
    1.59 +
    1.60 +subsection{*Closure Laws for SComplex, the Standard Complex Numbers*}
    1.61 +
    1.62 +lemma SComplex_add: "[| x \<in> SComplex; y \<in> SComplex |] ==> x + y \<in> SComplex"
    1.63 +apply (simp add: SComplex_def, safe)
    1.64 +apply (rule_tac x = "r + ra" in exI, simp)
    1.65 +done
    1.66 +
    1.67 +lemma SComplex_mult: "[| x \<in> SComplex; y \<in> SComplex |] ==> x * y \<in> SComplex"
    1.68 +apply (simp add: SComplex_def, safe)
    1.69 +apply (rule_tac x = "r * ra" in exI, simp)
    1.70 +done
    1.71 +
    1.72 +lemma SComplex_inverse: "x \<in> SComplex ==> inverse x \<in> SComplex"
    1.73 +apply (simp add: SComplex_def)
    1.74 +apply (blast intro: hcomplex_of_complex_inverse [symmetric])
    1.75 +done
    1.76 +
    1.77 +lemma SComplex_divide: "[| x \<in> SComplex;  y \<in> SComplex |] ==> x/y \<in> SComplex"
    1.78 +by (simp add: SComplex_mult SComplex_inverse divide_inverse_zero)
    1.79 +
    1.80 +lemma SComplex_minus: "x \<in> SComplex ==> -x \<in> SComplex"
    1.81 +apply (simp add: SComplex_def)
    1.82 +apply (blast intro: hcomplex_of_complex_minus [symmetric])
    1.83 +done
    1.84 +
    1.85 +lemma SComplex_minus_iff [simp]: "(-x \<in> SComplex) = (x \<in> SComplex)"
    1.86 +apply auto
    1.87 +apply (erule_tac [2] SComplex_minus)
    1.88 +apply (drule SComplex_minus, auto)
    1.89 +done
    1.90 +
    1.91 +lemma SComplex_diff: "[| x \<in> SComplex; y \<in> SComplex |] ==> x - y \<in> SComplex"
    1.92 +by (simp add: diff_minus SComplex_add) 
    1.93 +
    1.94 +lemma SComplex_add_cancel:
    1.95 +     "[| x + y \<in> SComplex; y \<in> SComplex |] ==> x \<in> SComplex"
    1.96 +by (drule SComplex_diff, assumption, simp)
    1.97 +
    1.98 +lemma SReal_hcmod_hcomplex_of_complex [simp]:
    1.99 +     "hcmod (hcomplex_of_complex r) \<in> Reals"
   1.100 +by (simp add: hcomplex_of_complex_def hcmod SReal_def hypreal_of_real_def)
   1.101 +
   1.102 +lemma SReal_hcmod_number_of [simp]: "hcmod (number_of w ::hcomplex) \<in> Reals"
   1.103 +apply (subst hcomplex_number_of [symmetric])
   1.104 +apply (rule SReal_hcmod_hcomplex_of_complex)
   1.105 +done
   1.106 +
   1.107 +lemma SReal_hcmod_SComplex: "x \<in> SComplex ==> hcmod x \<in> Reals"
   1.108 +by (auto simp add: SComplex_def)
   1.109 +
   1.110 +lemma SComplex_hcomplex_of_complex [simp]: "hcomplex_of_complex x \<in> SComplex"
   1.111 +by (simp add: SComplex_def)
   1.112 +
   1.113 +lemma SComplex_number_of [simp]: "(number_of w ::hcomplex) \<in> SComplex"
   1.114 +apply (subst hcomplex_number_of [symmetric])
   1.115 +apply (rule SComplex_hcomplex_of_complex)
   1.116 +done
   1.117 +
   1.118 +lemma SComplex_divide_number_of:
   1.119 +     "r \<in> SComplex ==> r/(number_of w::hcomplex) \<in> SComplex"
   1.120 +apply (simp only: divide_inverse_zero)
   1.121 +apply (blast intro!: SComplex_number_of SComplex_mult SComplex_inverse)
   1.122 +done
   1.123 +
   1.124 +lemma SComplex_UNIV_complex:
   1.125 +     "{x. hcomplex_of_complex x \<in> SComplex} = (UNIV::complex set)"
   1.126 +by (simp add: SComplex_def)
   1.127 +
   1.128 +lemma SComplex_iff: "(x \<in> SComplex) = (\<exists>y. x = hcomplex_of_complex y)"
   1.129 +by (simp add: SComplex_def)
   1.130 +
   1.131 +lemma hcomplex_of_complex_image:
   1.132 +     "hcomplex_of_complex `(UNIV::complex set) = SComplex"
   1.133 +by (auto simp add: SComplex_def)
   1.134 +
   1.135 +lemma inv_hcomplex_of_complex_image: "inv hcomplex_of_complex `SComplex = UNIV"
   1.136 +apply (auto simp add: SComplex_def)
   1.137 +apply (rule inj_hcomplex_of_complex [THEN inv_f_f, THEN subst], blast)
   1.138 +done
   1.139 +
   1.140 +lemma SComplex_hcomplex_of_complex_image: 
   1.141 +      "[| \<exists>x. x: P; P \<le> SComplex |] ==> \<exists>Q. P = hcomplex_of_complex ` Q"
   1.142 +apply (simp add: SComplex_def, blast)
   1.143 +done
   1.144 +
   1.145 +lemma SComplex_SReal_dense:
   1.146 +     "[| x \<in> SComplex; y \<in> SComplex; hcmod x < hcmod y  
   1.147 +      |] ==> \<exists>r \<in> Reals. hcmod x< r & r < hcmod y"
   1.148 +apply (auto intro: SReal_dense simp add: SReal_hcmod_SComplex)
   1.149 +done
   1.150 +
   1.151 +lemma SComplex_hcmod_SReal: 
   1.152 +      "z \<in> SComplex ==> hcmod z \<in> Reals"
   1.153 +apply (simp add: SComplex_def SReal_def)
   1.154 +apply (rule_tac z = z in eq_Abs_hcomplex)
   1.155 +apply (auto simp add: hcmod hypreal_of_real_def hcomplex_of_complex_def cmod_def)
   1.156 +apply (rule_tac x = "cmod r" in exI)
   1.157 +apply (simp add: cmod_def, ultra)
   1.158 +done
   1.159 +
   1.160 +lemma SComplex_zero [simp]: "0 \<in> SComplex"
   1.161 +by (simp add: SComplex_def hcomplex_of_complex_zero_iff)
   1.162 +
   1.163 +lemma SComplex_one [simp]: "1 \<in> SComplex"
   1.164 +by (simp add: SComplex_def hcomplex_of_complex_def hcomplex_one_def)
   1.165 +
   1.166 +(*
   1.167 +Goalw [SComplex_def,SReal_def] "hcmod z \<in> Reals ==> z \<in> SComplex"
   1.168 +by (res_inst_tac [("z","z")] eq_Abs_hcomplex 1);
   1.169 +by (auto_tac (claset(),simpset() addsimps [hcmod,hypreal_of_real_def,
   1.170 +    hcomplex_of_complex_def,cmod_def]));
   1.171 +*)
   1.172 +
   1.173 +
   1.174 +subsection{*The Finite Elements form a Subring*}
   1.175 +
   1.176 +lemma CFinite_add: "[|x \<in> CFinite; y \<in> CFinite|] ==> (x+y) \<in> CFinite"
   1.177 +apply (simp add: CFinite_def)
   1.178 +apply (blast intro!: SReal_add hcmod_add_less)
   1.179 +done
   1.180 +
   1.181 +lemma CFinite_mult: "[|x \<in> CFinite; y \<in> CFinite|] ==> x*y \<in> CFinite"
   1.182 +apply (simp add: CFinite_def)
   1.183 +apply (blast intro!: SReal_mult hcmod_mult_less)
   1.184 +done
   1.185 +
   1.186 +lemma CFinite_minus_iff [simp]: "(-x \<in> CFinite) = (x \<in> CFinite)"
   1.187 +by (simp add: CFinite_def)
   1.188 +
   1.189 +lemma SComplex_subset_CFinite [simp]: "SComplex \<le> CFinite"
   1.190 +apply (auto simp add: SComplex_def CFinite_def)
   1.191 +apply (rule_tac x = "1 + hcmod (hcomplex_of_complex r) " in bexI)
   1.192 +apply (auto intro: SReal_add)
   1.193 +done
   1.194 +
   1.195 +lemma HFinite_hcmod_hcomplex_of_complex [simp]:
   1.196 +     "hcmod (hcomplex_of_complex r) \<in> HFinite"
   1.197 +by (auto intro!: SReal_subset_HFinite [THEN subsetD])
   1.198 +
   1.199 +lemma CFinite_hcomplex_of_complex [simp]: "hcomplex_of_complex x \<in> CFinite"
   1.200 +by (auto intro!: SComplex_subset_CFinite [THEN subsetD])
   1.201 +
   1.202 +lemma CFiniteD: "x \<in> CFinite ==> \<exists>t \<in> Reals. hcmod x < t"
   1.203 +by (simp add: CFinite_def)
   1.204 +
   1.205 +lemma CFinite_hcmod_iff: "(x \<in> CFinite) = (hcmod x \<in> HFinite)"
   1.206 +by (simp add: CFinite_def HFinite_def)
   1.207 +
   1.208 +lemma CFinite_number_of [simp]: "number_of w \<in> CFinite"
   1.209 +by (rule SComplex_number_of [THEN SComplex_subset_CFinite [THEN subsetD]])
   1.210 +
   1.211 +lemma CFinite_bounded: "[|x \<in> CFinite; y \<le> hcmod x; 0 \<le> y |] ==> y: HFinite"
   1.212 +by (auto intro: HFinite_bounded simp add: CFinite_hcmod_iff)
   1.213 +
   1.214 +
   1.215 +subsection{*The Complex Infinitesimals form a Subring*}
   1.216 +	 
   1.217 +lemma CInfinitesimal_zero [iff]: "0 \<in> CInfinitesimal"
   1.218 +by (simp add: CInfinitesimal_def)
   1.219 +
   1.220 +lemma hcomplex_sum_of_halves: "x/(2::hcomplex) + x/(2::hcomplex) = x"
   1.221 +by auto
   1.222 +
   1.223 +lemma CInfinitesimal_hcmod_iff: 
   1.224 +   "(z \<in> CInfinitesimal) = (hcmod z \<in> Infinitesimal)"
   1.225 +by (simp add: CInfinitesimal_def Infinitesimal_def)
   1.226 +
   1.227 +lemma one_not_CInfinitesimal [simp]: "1 \<notin> CInfinitesimal"
   1.228 +by (simp add: CInfinitesimal_hcmod_iff)
   1.229 +
   1.230 +lemma CInfinitesimal_add:
   1.231 +     "[| x \<in> CInfinitesimal; y \<in> CInfinitesimal |] ==> (x+y) \<in> CInfinitesimal"
   1.232 +apply (auto simp add: CInfinitesimal_hcmod_iff)
   1.233 +apply (rule hrabs_le_Infinitesimal)
   1.234 +apply (rule_tac y = "hcmod y" in Infinitesimal_add, auto)
   1.235 +done
   1.236 +
   1.237 +lemma CInfinitesimal_minus_iff [simp]:
   1.238 +     "(-x:CInfinitesimal) = (x:CInfinitesimal)"
   1.239 +by (simp add: CInfinitesimal_def)
   1.240 +
   1.241 +lemma CInfinitesimal_diff:
   1.242 +     "[| x \<in> CInfinitesimal;  y \<in> CInfinitesimal |] ==> x-y \<in> CInfinitesimal"
   1.243 +by (simp add: diff_minus CInfinitesimal_add)
   1.244 +
   1.245 +lemma CInfinitesimal_mult:
   1.246 +     "[| x \<in> CInfinitesimal; y \<in> CInfinitesimal |] ==> x * y \<in> CInfinitesimal"
   1.247 +by (auto intro: Infinitesimal_mult simp add: CInfinitesimal_hcmod_iff hcmod_mult)
   1.248 +
   1.249 +lemma CInfinitesimal_CFinite_mult:
   1.250 +     "[| x \<in> CInfinitesimal; y \<in> CFinite |] ==> (x * y) \<in> CInfinitesimal"
   1.251 +by (auto intro: Infinitesimal_HFinite_mult simp add: CInfinitesimal_hcmod_iff CFinite_hcmod_iff hcmod_mult)
   1.252 +
   1.253 +lemma CInfinitesimal_CFinite_mult2:
   1.254 +     "[| x \<in> CInfinitesimal; y \<in> CFinite |] ==> (y * x) \<in> CInfinitesimal"
   1.255 +by (auto dest: CInfinitesimal_CFinite_mult simp add: hcomplex_mult_commute)
   1.256 +
   1.257 +lemma CInfinite_hcmod_iff: "(z \<in> CInfinite) = (hcmod z \<in> HInfinite)"
   1.258 +by (simp add: CInfinite_def HInfinite_def)
   1.259 +
   1.260 +lemma CInfinite_inverse_CInfinitesimal:
   1.261 +     "x \<in> CInfinite ==> inverse x \<in> CInfinitesimal"
   1.262 +by (auto intro: HInfinite_inverse_Infinitesimal simp add: CInfinitesimal_hcmod_iff CInfinite_hcmod_iff hcmod_hcomplex_inverse)
   1.263 +
   1.264 +lemma CInfinite_mult: "[|x \<in> CInfinite; y \<in> CInfinite|] ==> (x*y): CInfinite"
   1.265 +by (auto intro: HInfinite_mult simp add: CInfinite_hcmod_iff hcmod_mult)
   1.266 +
   1.267 +lemma CInfinite_minus_iff [simp]: "(-x \<in> CInfinite) = (x \<in> CInfinite)"
   1.268 +by (simp add: CInfinite_def)
   1.269 +
   1.270 +lemma CFinite_sum_squares:
   1.271 +     "[|a \<in> CFinite; b \<in> CFinite; c \<in> CFinite|]   
   1.272 +      ==> a*a + b*b + c*c \<in> CFinite"
   1.273 +by (auto intro: CFinite_mult CFinite_add)
   1.274 +
   1.275 +lemma not_CInfinitesimal_not_zero: "x \<notin> CInfinitesimal ==> x \<noteq> 0"
   1.276 +by auto
   1.277 +
   1.278 +lemma not_CInfinitesimal_not_zero2: "x \<in> CFinite - CInfinitesimal ==> x \<noteq> 0"
   1.279 +by auto
   1.280 +
   1.281 +lemma CFinite_diff_CInfinitesimal_hcmod:
   1.282 +     "x \<in> CFinite - CInfinitesimal ==> hcmod x \<in> HFinite - Infinitesimal"
   1.283 +by (simp add: CFinite_hcmod_iff CInfinitesimal_hcmod_iff)
   1.284 +
   1.285 +lemma hcmod_less_CInfinitesimal:
   1.286 +     "[| e \<in> CInfinitesimal; hcmod x < hcmod e |] ==> x \<in> CInfinitesimal"
   1.287 +by (auto intro: hrabs_less_Infinitesimal simp add: CInfinitesimal_hcmod_iff)
   1.288 +
   1.289 +lemma hcmod_le_CInfinitesimal:
   1.290 +     "[| e \<in> CInfinitesimal; hcmod x \<le> hcmod e |] ==> x \<in> CInfinitesimal"
   1.291 +by (auto intro: hrabs_le_Infinitesimal simp add: CInfinitesimal_hcmod_iff)
   1.292 +
   1.293 +lemma CInfinitesimal_interval:
   1.294 +     "[| e \<in> CInfinitesimal;  
   1.295 +          e' \<in> CInfinitesimal;  
   1.296 +          hcmod e' < hcmod x ; hcmod x < hcmod e  
   1.297 +       |] ==> x \<in> CInfinitesimal"
   1.298 +by (auto intro: Infinitesimal_interval simp add: CInfinitesimal_hcmod_iff)
   1.299 +
   1.300 +lemma CInfinitesimal_interval2:
   1.301 +     "[| e \<in> CInfinitesimal;  
   1.302 +         e' \<in> CInfinitesimal;  
   1.303 +         hcmod e' \<le> hcmod x ; hcmod x \<le> hcmod e  
   1.304 +      |] ==> x \<in> CInfinitesimal"
   1.305 +by (auto intro: Infinitesimal_interval2 simp add: CInfinitesimal_hcmod_iff)
   1.306 +
   1.307 +lemma not_CInfinitesimal_mult:
   1.308 +     "[| x \<notin> CInfinitesimal;  y \<notin> CInfinitesimal|] ==> (x*y) \<notin> CInfinitesimal"
   1.309 +apply (auto simp add: CInfinitesimal_hcmod_iff hcmod_mult)
   1.310 +apply (drule not_Infinitesimal_mult, auto)
   1.311 +done
   1.312 +
   1.313 +lemma CInfinitesimal_mult_disj:
   1.314 +     "x*y \<in> CInfinitesimal ==> x \<in> CInfinitesimal | y \<in> CInfinitesimal"
   1.315 +by (auto dest: Infinitesimal_mult_disj simp add: CInfinitesimal_hcmod_iff hcmod_mult)
   1.316 +
   1.317 +lemma CFinite_CInfinitesimal_diff_mult:
   1.318 +     "[| x \<in> CFinite - CInfinitesimal; y \<in> CFinite - CInfinitesimal |] 
   1.319 +      ==> x*y \<in> CFinite - CInfinitesimal"
   1.320 +by (blast dest: CFinite_mult not_CInfinitesimal_mult)
   1.321 +
   1.322 +lemma CInfinitesimal_subset_CFinite: "CInfinitesimal \<le> CFinite"
   1.323 +by (auto intro: Infinitesimal_subset_HFinite [THEN subsetD]
   1.324 +         simp add: CInfinitesimal_hcmod_iff CFinite_hcmod_iff)
   1.325 +
   1.326 +lemma CInfinitesimal_hcomplex_of_complex_mult:
   1.327 +     "x \<in> CInfinitesimal ==> x * hcomplex_of_complex r \<in> CInfinitesimal"
   1.328 +by (auto intro!: Infinitesimal_HFinite_mult simp add: CInfinitesimal_hcmod_iff hcmod_mult)
   1.329 +
   1.330 +lemma CInfinitesimal_hcomplex_of_complex_mult2:
   1.331 +     "x \<in> CInfinitesimal ==> hcomplex_of_complex r * x \<in> CInfinitesimal"
   1.332 +by (auto intro!: Infinitesimal_HFinite_mult2 simp add: CInfinitesimal_hcmod_iff hcmod_mult)
   1.333 +
   1.334 +
   1.335 +subsection{*The ``Infinitely Close'' Relation*}
   1.336 +
   1.337 +(*
   1.338 +Goalw [capprox_def,approx_def] "(z @c= w) = (hcmod z @= hcmod w)"
   1.339 +by (auto_tac (claset(),simpset() addsimps [CInfinitesimal_hcmod_iff]));
   1.340 +*)
   1.341 +
   1.342 +lemma mem_cinfmal_iff: "x:CInfinitesimal = (x @c= 0)"
   1.343 +by (simp add: CInfinitesimal_hcmod_iff capprox_def)
   1.344 +
   1.345 +lemma capprox_minus_iff: "(x @c= y) = (x + -y @c= 0)"
   1.346 +by (simp add: capprox_def diff_minus)
   1.347 +
   1.348 +lemma capprox_minus_iff2: "(x @c= y) = (-y + x @c= 0)"
   1.349 +by (simp add: capprox_def diff_minus add_commute)
   1.350 +
   1.351 +lemma capprox_refl [simp]: "x @c= x"
   1.352 +by (simp add: capprox_def)
   1.353 +
   1.354 +lemma capprox_sym: "x @c= y ==> y @c= x"
   1.355 +by (simp add: capprox_def CInfinitesimal_def hcmod_diff_commute)
   1.356 +
   1.357 +lemma capprox_trans: "[| x @c= y; y @c= z |] ==> x @c= z"
   1.358 +apply (simp add: capprox_def)
   1.359 +apply (drule CInfinitesimal_add, assumption)
   1.360 +apply (simp add: diff_minus)
   1.361 +done
   1.362 +
   1.363 +lemma capprox_trans2: "[| r @c= x; s @c= x |] ==> r @c= s"
   1.364 +by (blast intro: capprox_sym capprox_trans)
   1.365 +
   1.366 +lemma capprox_trans3: "[| x @c= r; x @c= s|] ==> r @c= s"
   1.367 +by (blast intro: capprox_sym capprox_trans)
   1.368 +
   1.369 +lemma number_of_capprox_reorient [simp]:
   1.370 +     "(number_of w @c= x) = (x @c= number_of w)"
   1.371 +by (blast intro: capprox_sym)
   1.372 +
   1.373 +lemma CInfinitesimal_capprox_minus: "(x-y \<in> CInfinitesimal) = (x @c= y)"
   1.374 +by (simp add: diff_minus capprox_minus_iff [symmetric] mem_cinfmal_iff)
   1.375 +
   1.376 +lemma capprox_monad_iff: "(x @c= y) = (cmonad(x)=cmonad(y))"
   1.377 +by (auto simp add: cmonad_def dest: capprox_sym elim!: capprox_trans equalityCE)
   1.378 +
   1.379 +lemma Infinitesimal_capprox:
   1.380 +     "[| x \<in> CInfinitesimal; y \<in> CInfinitesimal |] ==> x @c= y"
   1.381 +apply (simp add: mem_cinfmal_iff)
   1.382 +apply (blast intro: capprox_trans capprox_sym)
   1.383 +done
   1.384 +
   1.385 +lemma capprox_add: "[| a @c= b; c @c= d |] ==> a+c @c= b+d"
   1.386 +apply (simp add: capprox_def diff_minus) 
   1.387 +apply (rule minus_add_distrib [THEN ssubst])
   1.388 +apply (rule add_assoc [THEN ssubst])
   1.389 +apply (rule_tac b1 = c in add_left_commute [THEN subst])
   1.390 +apply (rule add_assoc [THEN subst])
   1.391 +apply (blast intro: CInfinitesimal_add)
   1.392 +done
   1.393 +
   1.394 +lemma capprox_minus: "a @c= b ==> -a @c= -b"
   1.395 +apply (rule capprox_minus_iff [THEN iffD2, THEN capprox_sym])
   1.396 +apply (drule capprox_minus_iff [THEN iffD1])
   1.397 +apply (simp add: add_commute)
   1.398 +done
   1.399 +
   1.400 +lemma capprox_minus2: "-a @c= -b ==> a @c= b"
   1.401 +by (auto dest: capprox_minus)
   1.402 +
   1.403 +lemma capprox_minus_cancel [simp]: "(-a @c= -b) = (a @c= b)"
   1.404 +by (blast intro: capprox_minus capprox_minus2)
   1.405 +
   1.406 +lemma capprox_add_minus: "[| a @c= b; c @c= d |] ==> a + -c @c= b + -d"
   1.407 +by (blast intro!: capprox_add capprox_minus)
   1.408 +
   1.409 +lemma capprox_mult1: 
   1.410 +      "[| a @c= b; c \<in> CFinite|] ==> a*c @c= b*c"
   1.411 +apply (simp add: capprox_def diff_minus)
   1.412 +apply (simp only: CInfinitesimal_CFinite_mult minus_mult_left hcomplex_add_mult_distrib [symmetric])
   1.413 +done
   1.414 +
   1.415 +lemma capprox_mult2: "[|a @c= b; c \<in> CFinite|] ==> c*a @c= c*b"
   1.416 +by (simp add: capprox_mult1 hcomplex_mult_commute)
   1.417 +
   1.418 +lemma capprox_mult_subst:
   1.419 +     "[|u @c= v*x; x @c= y; v \<in> CFinite|] ==> u @c= v*y"
   1.420 +by (blast intro: capprox_mult2 capprox_trans)
   1.421 +
   1.422 +lemma capprox_mult_subst2:
   1.423 +     "[| u @c= x*v; x @c= y; v \<in> CFinite |] ==> u @c= y*v"
   1.424 +by (blast intro: capprox_mult1 capprox_trans)
   1.425 +
   1.426 +lemma capprox_mult_subst_SComplex:
   1.427 +     "[| u @c= x*hcomplex_of_complex v; x @c= y |] 
   1.428 +      ==> u @c= y*hcomplex_of_complex v"
   1.429 +by (auto intro: capprox_mult_subst2)
   1.430 +
   1.431 +lemma capprox_eq_imp: "a = b ==> a @c= b"
   1.432 +by (simp add: capprox_def)
   1.433 +
   1.434 +lemma CInfinitesimal_minus_capprox: "x \<in> CInfinitesimal ==> -x @c= x"
   1.435 +by (blast intro: CInfinitesimal_minus_iff [THEN iffD2] mem_cinfmal_iff [THEN iffD1] capprox_trans2)
   1.436 +
   1.437 +lemma bex_CInfinitesimal_iff: "(\<exists>y \<in> CInfinitesimal. x - z = y) = (x @c= z)"
   1.438 +by (unfold capprox_def, blast)
   1.439 +
   1.440 +lemma bex_CInfinitesimal_iff2: "(\<exists>y \<in> CInfinitesimal. x = z + y) = (x @c= z)"
   1.441 +by (simp add: bex_CInfinitesimal_iff [symmetric], force)
   1.442 +
   1.443 +lemma CInfinitesimal_add_capprox:
   1.444 +     "[| y \<in> CInfinitesimal; x + y = z |] ==> x @c= z"
   1.445 +apply (rule bex_CInfinitesimal_iff [THEN iffD1])
   1.446 +apply (drule CInfinitesimal_minus_iff [THEN iffD2])
   1.447 +apply (simp add: eq_commute compare_rls)
   1.448 +done
   1.449 +
   1.450 +lemma CInfinitesimal_add_capprox_self: "y \<in> CInfinitesimal ==> x @c= x + y"
   1.451 +apply (rule bex_CInfinitesimal_iff [THEN iffD1])
   1.452 +apply (drule CInfinitesimal_minus_iff [THEN iffD2])
   1.453 +apply (simp add: eq_commute compare_rls)
   1.454 +done
   1.455 +
   1.456 +lemma CInfinitesimal_add_capprox_self2: "y \<in> CInfinitesimal ==> x @c= y + x"
   1.457 +by (auto dest: CInfinitesimal_add_capprox_self simp add: add_commute)
   1.458 +
   1.459 +lemma CInfinitesimal_add_minus_capprox_self:
   1.460 +     "y \<in> CInfinitesimal ==> x @c= x + -y"
   1.461 +by (blast intro!: CInfinitesimal_add_capprox_self CInfinitesimal_minus_iff [THEN iffD2])
   1.462 +
   1.463 +lemma CInfinitesimal_add_cancel:
   1.464 +     "[| y \<in> CInfinitesimal; x+y @c= z|] ==> x @c= z"
   1.465 +apply (drule_tac x = x in CInfinitesimal_add_capprox_self [THEN capprox_sym])
   1.466 +apply (erule capprox_trans3 [THEN capprox_sym], assumption)
   1.467 +done
   1.468 +
   1.469 +lemma CInfinitesimal_add_right_cancel:
   1.470 +     "[| y \<in> CInfinitesimal; x @c= z + y|] ==> x @c= z"
   1.471 +apply (drule_tac x = z in CInfinitesimal_add_capprox_self2 [THEN capprox_sym])
   1.472 +apply (erule capprox_trans3 [THEN capprox_sym])
   1.473 +apply (simp add: add_commute)
   1.474 +apply (erule capprox_sym)
   1.475 +done
   1.476 +
   1.477 +lemma capprox_add_left_cancel: "d + b  @c= d + c ==> b @c= c"
   1.478 +apply (drule capprox_minus_iff [THEN iffD1])
   1.479 +apply (simp add: minus_add_distrib capprox_minus_iff [symmetric] add_ac)
   1.480 +done
   1.481 +
   1.482 +lemma capprox_add_right_cancel: "b + d @c= c + d ==> b @c= c"
   1.483 +apply (rule capprox_add_left_cancel)
   1.484 +apply (simp add: add_commute)
   1.485 +done
   1.486 +
   1.487 +lemma capprox_add_mono1: "b @c= c ==> d + b @c= d + c"
   1.488 +apply (rule capprox_minus_iff [THEN iffD2])
   1.489 +apply (simp add: capprox_minus_iff [symmetric] add_ac)
   1.490 +done
   1.491 +
   1.492 +lemma capprox_add_mono2: "b @c= c ==> b + a @c= c + a"
   1.493 +apply (simp (no_asm_simp) add: add_commute capprox_add_mono1)
   1.494 +done
   1.495 +
   1.496 +lemma capprox_add_left_iff [iff]: "(a + b @c= a + c) = (b @c= c)"
   1.497 +by (fast elim: capprox_add_left_cancel capprox_add_mono1)
   1.498 +
   1.499 +lemma capprox_add_right_iff [iff]: "(b + a @c= c + a) = (b @c= c)"
   1.500 +by (simp add: add_commute)
   1.501 +
   1.502 +lemma capprox_CFinite: "[| x \<in> CFinite; x @c= y |] ==> y \<in> CFinite"
   1.503 +apply (drule bex_CInfinitesimal_iff2 [THEN iffD2], safe)
   1.504 +apply (drule CInfinitesimal_subset_CFinite [THEN subsetD, THEN CFinite_minus_iff [THEN iffD2]])
   1.505 +apply (drule CFinite_add)
   1.506 +apply (assumption, auto)
   1.507 +done
   1.508 +
   1.509 +lemma capprox_hcomplex_of_complex_CFinite:
   1.510 +     "x @c= hcomplex_of_complex D ==> x \<in> CFinite"
   1.511 +by (rule capprox_sym [THEN [2] capprox_CFinite], auto)
   1.512 +
   1.513 +lemma capprox_mult_CFinite:
   1.514 +     "[|a @c= b; c @c= d; b \<in> CFinite; d \<in> CFinite|] ==> a*c @c= b*d"
   1.515 +apply (rule capprox_trans)
   1.516 +apply (rule_tac [2] capprox_mult2)
   1.517 +apply (rule capprox_mult1)
   1.518 +prefer 2 apply (blast intro: capprox_CFinite capprox_sym, auto)
   1.519 +done
   1.520 +
   1.521 +lemma capprox_mult_hcomplex_of_complex:
   1.522 +     "[|a @c= hcomplex_of_complex b; c @c= hcomplex_of_complex d |]  
   1.523 +      ==> a*c @c= hcomplex_of_complex b * hcomplex_of_complex d"
   1.524 +apply (blast intro!: capprox_mult_CFinite capprox_hcomplex_of_complex_CFinite CFinite_hcomplex_of_complex)
   1.525 +done
   1.526 +
   1.527 +lemma capprox_SComplex_mult_cancel_zero:
   1.528 +     "[| a \<in> SComplex; a \<noteq> 0; a*x @c= 0 |] ==> x @c= 0"
   1.529 +apply (drule SComplex_inverse [THEN SComplex_subset_CFinite [THEN subsetD]])
   1.530 +apply (auto dest: capprox_mult2 simp add: hcomplex_mult_assoc [symmetric])
   1.531 +done
   1.532 +
   1.533 +lemma capprox_mult_SComplex1: "[| a \<in> SComplex; x @c= 0 |] ==> x*a @c= 0"
   1.534 +by (auto dest: SComplex_subset_CFinite [THEN subsetD] capprox_mult1)
   1.535 +
   1.536 +lemma capprox_mult_SComplex2: "[| a \<in> SComplex; x @c= 0 |] ==> a*x @c= 0"
   1.537 +by (auto dest: SComplex_subset_CFinite [THEN subsetD] capprox_mult2)
   1.538 +
   1.539 +lemma capprox_mult_SComplex_zero_cancel_iff [simp]:
   1.540 +     "[|a \<in> SComplex; a \<noteq> 0 |] ==> (a*x @c= 0) = (x @c= 0)"
   1.541 +by (blast intro: capprox_SComplex_mult_cancel_zero capprox_mult_SComplex2)
   1.542 +
   1.543 +lemma capprox_SComplex_mult_cancel:
   1.544 +     "[| a \<in> SComplex; a \<noteq> 0; a* w @c= a*z |] ==> w @c= z"
   1.545 +apply (drule SComplex_inverse [THEN SComplex_subset_CFinite [THEN subsetD]])
   1.546 +apply (auto dest: capprox_mult2 simp add: hcomplex_mult_assoc [symmetric])
   1.547 +done
   1.548 +
   1.549 +lemma capprox_SComplex_mult_cancel_iff1 [simp]:
   1.550 +     "[| a \<in> SComplex; a \<noteq> 0|] ==> (a* w @c= a*z) = (w @c= z)"
   1.551 +by (auto intro!: capprox_mult2 SComplex_subset_CFinite [THEN subsetD]
   1.552 +            intro: capprox_SComplex_mult_cancel)
   1.553 +
   1.554 +lemma capprox_hcmod_approx_zero: "(x @c= y) = (hcmod (y - x) @= 0)"
   1.555 +apply (rule capprox_minus_iff [THEN ssubst])
   1.556 +apply (simp add: capprox_def CInfinitesimal_hcmod_iff mem_infmal_iff diff_minus [symmetric] hcmod_diff_commute)
   1.557 +done
   1.558 +
   1.559 +lemma capprox_approx_zero_iff: "(x @c= 0) = (hcmod x @= 0)"
   1.560 +by (simp add: capprox_hcmod_approx_zero)
   1.561 +
   1.562 +lemma capprox_minus_zero_cancel_iff [simp]: "(-x @c= 0) = (x @c= 0)"
   1.563 +by (simp add: capprox_hcmod_approx_zero)
   1.564 +
   1.565 +lemma Infinitesimal_hcmod_add_diff:
   1.566 +     "u @c= 0 ==> hcmod(x + u) - hcmod x \<in> Infinitesimal"
   1.567 +apply (rule_tac e = "hcmod u" and e' = "- hcmod u" in Infinitesimal_interval2)
   1.568 +apply (auto dest: capprox_approx_zero_iff [THEN iffD1]
   1.569 +             simp add: mem_infmal_iff [symmetric] hypreal_diff_def)
   1.570 +apply (rule_tac c1 = "hcmod x" in add_le_cancel_left [THEN iffD1])
   1.571 +apply (auto simp add: diff_minus [symmetric])
   1.572 +done
   1.573 +
   1.574 +lemma approx_hcmod_add_hcmod: "u @c= 0 ==> hcmod(x + u) @= hcmod x"
   1.575 +apply (rule approx_minus_iff [THEN iffD2])
   1.576 +apply (auto intro: Infinitesimal_hcmod_add_diff simp add: mem_infmal_iff [symmetric] diff_minus [symmetric])
   1.577 +done
   1.578 +
   1.579 +lemma capprox_hcmod_approx: "x @c= y ==> hcmod x @= hcmod y"
   1.580 +by (auto intro: approx_hcmod_add_hcmod 
   1.581 +         dest!: bex_CInfinitesimal_iff2 [THEN iffD2]
   1.582 +         simp add: mem_cinfmal_iff)
   1.583  
   1.584  
   1.585 -defs  
   1.586 +subsection{*Zero is the Only Infinitesimal Complex Number*}
   1.587 +
   1.588 +lemma CInfinitesimal_less_SComplex:
   1.589 +   "[| x \<in> SComplex; y \<in> CInfinitesimal; 0 < hcmod x |] ==> hcmod y < hcmod x"
   1.590 +by (auto intro!: Infinitesimal_less_SReal SComplex_hcmod_SReal simp add: CInfinitesimal_hcmod_iff)
   1.591 +
   1.592 +lemma SComplex_Int_CInfinitesimal_zero: "SComplex Int CInfinitesimal = {0}"
   1.593 +apply (auto simp add: SComplex_def CInfinitesimal_hcmod_iff)
   1.594 +apply (cut_tac r = r in SReal_hcmod_hcomplex_of_complex)
   1.595 +apply (drule_tac A = Reals in IntI, assumption)
   1.596 +apply (subgoal_tac "hcmod (hcomplex_of_complex r) = 0")
   1.597 +apply simp
   1.598 +apply (simp add: SReal_Int_Infinitesimal_zero) 
   1.599 +done
   1.600 +
   1.601 +lemma SComplex_CInfinitesimal_zero:
   1.602 +     "[| x \<in> SComplex; x \<in> CInfinitesimal|] ==> x = 0"
   1.603 +by (cut_tac SComplex_Int_CInfinitesimal_zero, blast)
   1.604 +
   1.605 +lemma SComplex_CFinite_diff_CInfinitesimal:
   1.606 +     "[| x \<in> SComplex; x \<noteq> 0 |] ==> x \<in> CFinite - CInfinitesimal"
   1.607 +by (auto dest: SComplex_CInfinitesimal_zero SComplex_subset_CFinite [THEN subsetD])
   1.608 +
   1.609 +lemma hcomplex_of_complex_CFinite_diff_CInfinitesimal:
   1.610 +     "hcomplex_of_complex x \<noteq> 0 
   1.611 +      ==> hcomplex_of_complex x \<in> CFinite - CInfinitesimal"
   1.612 +by (rule SComplex_CFinite_diff_CInfinitesimal, auto)
   1.613 +
   1.614 +lemma hcomplex_of_complex_CInfinitesimal_iff_0 [iff]:
   1.615 +     "(hcomplex_of_complex x \<in> CInfinitesimal) = (x=0)"
   1.616 +apply (auto simp add: hcomplex_of_complex_zero)
   1.617 +apply (rule ccontr)
   1.618 +apply (rule hcomplex_of_complex_CFinite_diff_CInfinitesimal [THEN DiffD2], auto)
   1.619 +done
   1.620 +
   1.621 +lemma number_of_not_CInfinitesimal [simp]:
   1.622 +     "number_of w \<noteq> (0::hcomplex) ==> number_of w \<notin> CInfinitesimal"
   1.623 +by (fast dest: SComplex_number_of [THEN SComplex_CInfinitesimal_zero])
   1.624 +
   1.625 +lemma capprox_SComplex_not_zero:
   1.626 +     "[| y \<in> SComplex; x @c= y; y\<noteq> 0 |] ==> x \<noteq> 0"
   1.627 +by (auto dest: SComplex_CInfinitesimal_zero capprox_sym [THEN mem_cinfmal_iff [THEN iffD2]])
   1.628 +
   1.629 +lemma CFinite_diff_CInfinitesimal_capprox:
   1.630 +     "[| x @c= y; y \<in> CFinite - CInfinitesimal |]  
   1.631 +      ==> x \<in> CFinite - CInfinitesimal"
   1.632 +apply (auto intro: capprox_sym [THEN [2] capprox_CFinite] 
   1.633 +            simp add: mem_cinfmal_iff)
   1.634 +apply (drule capprox_trans3, assumption)
   1.635 +apply (blast dest: capprox_sym)
   1.636 +done
   1.637 +
   1.638 +lemma CInfinitesimal_ratio:
   1.639 +     "[| y \<noteq> 0;  y \<in> CInfinitesimal;  x/y \<in> CFinite |] ==> x \<in> CInfinitesimal"
   1.640 +apply (drule CInfinitesimal_CFinite_mult2, assumption)
   1.641 +apply (simp add: divide_inverse_zero hcomplex_mult_assoc)
   1.642 +done
   1.643 +
   1.644 +lemma SComplex_capprox_iff:
   1.645 +     "[|x \<in> SComplex; y \<in> SComplex|] ==> (x @c= y) = (x = y)"
   1.646 +apply auto
   1.647 +apply (simp add: capprox_def)
   1.648 +apply (subgoal_tac "x-y = 0", simp) 
   1.649 +apply (rule SComplex_CInfinitesimal_zero)
   1.650 +apply (simp add: SComplex_diff, assumption)
   1.651 +done
   1.652 +
   1.653 +lemma number_of_capprox_iff [simp]:
   1.654 +    "(number_of v @c= number_of w) = (number_of v = (number_of w :: hcomplex))"
   1.655 +by (rule SComplex_capprox_iff, auto)
   1.656 +
   1.657 +lemma number_of_CInfinitesimal_iff [simp]:
   1.658 +     "(number_of w \<in> CInfinitesimal) = (number_of w = (0::hcomplex))"
   1.659 +apply (rule iffI)
   1.660 +apply (fast dest: SComplex_number_of [THEN SComplex_CInfinitesimal_zero])
   1.661 +apply (simp (no_asm_simp))
   1.662 +done
   1.663 +
   1.664 +lemma hcomplex_of_complex_approx_iff [simp]:
   1.665 +     "(hcomplex_of_complex k @c= hcomplex_of_complex m) = (k = m)"
   1.666 +apply auto
   1.667 +apply (rule inj_hcomplex_of_complex [THEN injD])
   1.668 +apply (rule SComplex_capprox_iff [THEN iffD1], auto)
   1.669 +done
   1.670 +
   1.671 +lemma hcomplex_of_complex_capprox_number_of_iff [simp]:
   1.672 +     "(hcomplex_of_complex k @c= number_of w) = (k = number_of w)"
   1.673 +by (subst hcomplex_of_complex_approx_iff [symmetric], auto)
   1.674 +
   1.675 +lemma capprox_unique_complex:
   1.676 +     "[| r \<in> SComplex; s \<in> SComplex; r @c= x; s @c= x|] ==> r = s"
   1.677 +by (blast intro: SComplex_capprox_iff [THEN iffD1] capprox_trans2)
   1.678 +
   1.679 +lemma hcomplex_capproxD1:
   1.680 +     "Abs_hcomplex(hcomplexrel ``{%n. X n}) @c= Abs_hcomplex(hcomplexrel``{%n. Y n})  
   1.681 +      ==> Abs_hypreal(hyprel `` {%n. Re(X n)}) @=  
   1.682 +          Abs_hypreal(hyprel `` {%n. Re(Y n)})"
   1.683 +apply (auto simp add: approx_FreeUltrafilterNat_iff)
   1.684 +apply (drule capprox_minus_iff [THEN iffD1])
   1.685 +apply (auto simp add: hcomplex_minus hcomplex_add mem_cinfmal_iff [symmetric] CInfinitesimal_hcmod_iff hcmod Infinitesimal_FreeUltrafilterNat_iff2)
   1.686 +apply (drule_tac x = m in spec, ultra)
   1.687 +apply (rename_tac Z x)
   1.688 +apply (case_tac "X x")
   1.689 +apply (case_tac "Y x")
   1.690 +apply (auto simp add: complex_minus complex_add complex_mod
   1.691 +           simp del: realpow_Suc)
   1.692 +apply (rule_tac y="abs(Z x)" in order_le_less_trans)
   1.693 +apply (drule_tac t = "Z x" in sym)
   1.694 +apply (auto simp add: abs_eqI1 simp del: realpow_Suc)
   1.695 +done
   1.696 +
   1.697 +(* same proof *)
   1.698 +lemma hcomplex_capproxD2:
   1.699 +     "Abs_hcomplex(hcomplexrel ``{%n. X n}) @c= Abs_hcomplex(hcomplexrel``{%n. Y n})  
   1.700 +      ==> Abs_hypreal(hyprel `` {%n. Im(X n)}) @=  
   1.701 +          Abs_hypreal(hyprel `` {%n. Im(Y n)})"
   1.702 +apply (auto simp add: approx_FreeUltrafilterNat_iff)
   1.703 +apply (drule capprox_minus_iff [THEN iffD1])
   1.704 +apply (auto simp add: hcomplex_minus hcomplex_add mem_cinfmal_iff [symmetric] CInfinitesimal_hcmod_iff hcmod Infinitesimal_FreeUltrafilterNat_iff2)
   1.705 +apply (drule_tac x = m in spec, ultra)
   1.706 +apply (rename_tac Z x)
   1.707 +apply (case_tac "X x")
   1.708 +apply (case_tac "Y x")
   1.709 +apply (auto simp add: complex_minus complex_add complex_mod simp del: realpow_Suc)
   1.710 +apply (rule_tac y="abs(Z x)" in order_le_less_trans)
   1.711 +apply (drule_tac t = "Z x" in sym)
   1.712 +apply (auto simp add: abs_eqI1 simp del: realpow_Suc)
   1.713 +done
   1.714 +
   1.715 +lemma hcomplex_capproxI:
   1.716 +     "[| Abs_hypreal(hyprel `` {%n. Re(X n)}) @=  
   1.717 +         Abs_hypreal(hyprel `` {%n. Re(Y n)});  
   1.718 +         Abs_hypreal(hyprel `` {%n. Im(X n)}) @=  
   1.719 +         Abs_hypreal(hyprel `` {%n. Im(Y n)})  
   1.720 +      |] ==> Abs_hcomplex(hcomplexrel ``{%n. X n}) @c= Abs_hcomplex(hcomplexrel``{%n. Y n})"
   1.721 +apply (drule approx_minus_iff [THEN iffD1])
   1.722 +apply (drule approx_minus_iff [THEN iffD1])
   1.723 +apply (rule capprox_minus_iff [THEN iffD2])
   1.724 +apply (auto simp add: mem_cinfmal_iff [symmetric] mem_infmal_iff [symmetric] hypreal_minus hypreal_add hcomplex_minus hcomplex_add CInfinitesimal_hcmod_iff hcmod Infinitesimal_FreeUltrafilterNat_iff)
   1.725 +apply (rule bexI, rule_tac [2] lemma_hyprel_refl, auto)
   1.726 +apply (drule_tac x = "u/2" in spec)
   1.727 +apply (drule_tac x = "u/2" in spec, auto, ultra)
   1.728 +apply (drule sym, drule sym)
   1.729 +apply (case_tac "X x")
   1.730 +apply (case_tac "Y x")
   1.731 +apply (auto simp add: complex_minus complex_add complex_mod snd_conv fst_conv numeral_2_eq_2)
   1.732 +apply (rename_tac a b c d)
   1.733 +apply (subgoal_tac "sqrt (abs (a + - c) ^ 2 + abs (b + - d) ^ 2) < u")
   1.734 +apply (rule_tac [2] lemma_sqrt_hcomplex_capprox, auto)
   1.735 +apply (simp add: power2_eq_square)
   1.736 +done
   1.737 +
   1.738 +lemma capprox_approx_iff:
   1.739 +     "(Abs_hcomplex(hcomplexrel ``{%n. X n}) @c= Abs_hcomplex(hcomplexrel``{%n. Y n})) = 
   1.740 +       (Abs_hypreal(hyprel `` {%n. Re(X n)}) @= Abs_hypreal(hyprel `` {%n. Re(Y n)}) &  
   1.741 +        Abs_hypreal(hyprel `` {%n. Im(X n)}) @= Abs_hypreal(hyprel `` {%n. Im(Y n)}))"
   1.742 +apply (blast intro: hcomplex_capproxI hcomplex_capproxD1 hcomplex_capproxD2)
   1.743 +done
   1.744 +
   1.745 +lemma hcomplex_of_hypreal_capprox_iff [simp]:
   1.746 +     "(hcomplex_of_hypreal x @c= hcomplex_of_hypreal z) = (x @= z)"
   1.747 +apply (rule eq_Abs_hypreal [of x])
   1.748 +apply (rule eq_Abs_hypreal [of z])
   1.749 +apply (simp add: hcomplex_of_hypreal capprox_approx_iff)
   1.750 +done
   1.751 +
   1.752 +lemma CFinite_HFinite_Re:
   1.753 +     "Abs_hcomplex(hcomplexrel ``{%n. X n}) \<in> CFinite  
   1.754 +      ==> Abs_hypreal(hyprel `` {%n. Re(X n)}) \<in> HFinite"
   1.755 +apply (auto simp add: CFinite_hcmod_iff hcmod HFinite_FreeUltrafilterNat_iff)
   1.756 +apply (rule bexI, rule_tac [2] lemma_hyprel_refl)
   1.757 +apply (rule_tac x = u in exI, ultra)
   1.758 +apply (drule sym, case_tac "X x")
   1.759 +apply (auto simp add: complex_mod numeral_2_eq_2 simp del: realpow_Suc)
   1.760 +apply (rule ccontr, drule linorder_not_less [THEN iffD1])
   1.761 +apply (drule order_less_le_trans, assumption)
   1.762 +apply (drule real_sqrt_ge_abs1 [THEN [2] order_less_le_trans]) 
   1.763 +apply (auto simp add: numeral_2_eq_2 [symmetric]) 
   1.764 +done
   1.765 +
   1.766 +lemma CFinite_HFinite_Im:
   1.767 +     "Abs_hcomplex(hcomplexrel ``{%n. X n}) \<in> CFinite  
   1.768 +      ==> Abs_hypreal(hyprel `` {%n. Im(X n)}) \<in> HFinite"
   1.769 +apply (auto simp add: CFinite_hcmod_iff hcmod HFinite_FreeUltrafilterNat_iff)
   1.770 +apply (rule bexI, rule_tac [2] lemma_hyprel_refl)
   1.771 +apply (rule_tac x = u in exI, ultra)
   1.772 +apply (drule sym, case_tac "X x")
   1.773 +apply (auto simp add: complex_mod simp del: realpow_Suc)
   1.774 +apply (rule ccontr, drule linorder_not_less [THEN iffD1])
   1.775 +apply (drule order_less_le_trans, assumption)
   1.776 +apply (drule real_sqrt_ge_abs2 [THEN [2] order_less_le_trans], auto) 
   1.777 +done
   1.778 +
   1.779 +lemma HFinite_Re_Im_CFinite:
   1.780 +     "[| Abs_hypreal(hyprel `` {%n. Re(X n)}) \<in> HFinite;  
   1.781 +         Abs_hypreal(hyprel `` {%n. Im(X n)}) \<in> HFinite  
   1.782 +      |] ==> Abs_hcomplex(hcomplexrel ``{%n. X n}) \<in> CFinite"
   1.783 +apply (auto simp add: CFinite_hcmod_iff hcmod HFinite_FreeUltrafilterNat_iff)
   1.784 +apply (rename_tac Y Z u v)
   1.785 +apply (rule bexI, rule_tac [2] lemma_hyprel_refl)
   1.786 +apply (rule_tac x = "2* (u + v) " in exI)
   1.787 +apply ultra
   1.788 +apply (drule sym, case_tac "X x")
   1.789 +apply (auto simp add: complex_mod numeral_2_eq_2 simp del: realpow_Suc)
   1.790 +apply (subgoal_tac "0 < u")
   1.791 + prefer 2 apply arith
   1.792 +apply (subgoal_tac "0 < v")
   1.793 + prefer 2 apply arith
   1.794 +apply (subgoal_tac "sqrt (abs (Y x) ^ 2 + abs (Z x) ^ 2) < 2*u + 2*v")
   1.795 +apply (rule_tac [2] lemma_sqrt_hcomplex_capprox, auto)
   1.796 +apply (simp add: power2_eq_square)
   1.797 +done
   1.798 +
   1.799 +lemma CFinite_HFinite_iff:
   1.800 +     "(Abs_hcomplex(hcomplexrel ``{%n. X n}) \<in> CFinite) =  
   1.801 +      (Abs_hypreal(hyprel `` {%n. Re(X n)}) \<in> HFinite &  
   1.802 +       Abs_hypreal(hyprel `` {%n. Im(X n)}) \<in> HFinite)"
   1.803 +by (blast intro: HFinite_Re_Im_CFinite CFinite_HFinite_Im CFinite_HFinite_Re)
   1.804 +
   1.805 +lemma SComplex_Re_SReal:
   1.806 +     "Abs_hcomplex(hcomplexrel ``{%n. X n}) \<in> SComplex  
   1.807 +      ==> Abs_hypreal(hyprel `` {%n. Re(X n)}) \<in> Reals"
   1.808 +apply (auto simp add: SComplex_def hcomplex_of_complex_def SReal_def hypreal_of_real_def)
   1.809 +apply (rule_tac x = "Re r" in exI, ultra)
   1.810 +done
   1.811 +
   1.812 +lemma SComplex_Im_SReal:
   1.813 +     "Abs_hcomplex(hcomplexrel ``{%n. X n}) \<in> SComplex  
   1.814 +      ==> Abs_hypreal(hyprel `` {%n. Im(X n)}) \<in> Reals"
   1.815 +apply (auto simp add: SComplex_def hcomplex_of_complex_def SReal_def hypreal_of_real_def)
   1.816 +apply (rule_tac x = "Im r" in exI, ultra)
   1.817 +done
   1.818 +
   1.819 +lemma Reals_Re_Im_SComplex:
   1.820 +     "[| Abs_hypreal(hyprel `` {%n. Re(X n)}) \<in> Reals;  
   1.821 +         Abs_hypreal(hyprel `` {%n. Im(X n)}) \<in> Reals  
   1.822 +      |] ==> Abs_hcomplex(hcomplexrel ``{%n. X n}) \<in> SComplex"
   1.823 +apply (auto simp add: SComplex_def hcomplex_of_complex_def SReal_def hypreal_of_real_def)
   1.824 +apply (rule_tac x = "Complex r ra" in exI, ultra)
   1.825 +done
   1.826 +
   1.827 +lemma SComplex_SReal_iff:
   1.828 +     "(Abs_hcomplex(hcomplexrel ``{%n. X n}) \<in> SComplex) =  
   1.829 +      (Abs_hypreal(hyprel `` {%n. Re(X n)}) \<in> Reals &  
   1.830 +       Abs_hypreal(hyprel `` {%n. Im(X n)}) \<in> Reals)"
   1.831 +by (blast intro: SComplex_Re_SReal SComplex_Im_SReal Reals_Re_Im_SComplex)
   1.832 +
   1.833 +lemma CInfinitesimal_Infinitesimal_iff:
   1.834 +     "(Abs_hcomplex(hcomplexrel ``{%n. X n}) \<in> CInfinitesimal) =  
   1.835 +      (Abs_hypreal(hyprel `` {%n. Re(X n)}) \<in> Infinitesimal &  
   1.836 +       Abs_hypreal(hyprel `` {%n. Im(X n)}) \<in> Infinitesimal)"
   1.837 +by (simp add: mem_cinfmal_iff mem_infmal_iff hcomplex_zero_num hypreal_zero_num capprox_approx_iff)
   1.838 +
   1.839 +lemma eq_Abs_hcomplex_EX:
   1.840 +     "(\<exists>t. P t) = (\<exists>X. P (Abs_hcomplex(hcomplexrel `` {X})))"
   1.841 +apply auto
   1.842 +apply (rule_tac z = t in eq_Abs_hcomplex, auto)
   1.843 +done
   1.844 +
   1.845 +lemma eq_Abs_hcomplex_Bex:
   1.846 +     "(\<exists>t \<in> A. P t) = (\<exists>X. (Abs_hcomplex(hcomplexrel `` {X})) \<in> A &  
   1.847 +                         P (Abs_hcomplex(hcomplexrel `` {X})))"
   1.848 +apply auto
   1.849 +apply (rule_tac z = t in eq_Abs_hcomplex, auto)
   1.850 +done
   1.851 +
   1.852 +(* Here we go - easy proof now!! *)
   1.853 +lemma stc_part_Ex: "x:CFinite ==> \<exists>t \<in> SComplex. x @c= t"
   1.854 +apply (rule_tac z = x in eq_Abs_hcomplex)
   1.855 +apply (auto simp add: CFinite_HFinite_iff eq_Abs_hcomplex_Bex SComplex_SReal_iff capprox_approx_iff)
   1.856 +apply (drule st_part_Ex, safe)+
   1.857 +apply (rule_tac z = t in eq_Abs_hypreal)
   1.858 +apply (rule_tac z = ta in eq_Abs_hypreal, auto)
   1.859 +apply (rule_tac x = "%n. Complex (xa n) (xb n) " in exI)
   1.860 +apply auto
   1.861 +done
   1.862 +
   1.863 +lemma stc_part_Ex1: "x:CFinite ==> EX! t. t \<in> SComplex &  x @c= t"
   1.864 +apply (drule stc_part_Ex, safe)
   1.865 +apply (drule_tac [2] capprox_sym, drule_tac [2] capprox_sym, drule_tac [2] capprox_sym)
   1.866 +apply (auto intro!: capprox_unique_complex)
   1.867 +done
   1.868 +
   1.869 +lemma CFinite_Int_CInfinite_empty: "CFinite Int CInfinite = {}"
   1.870 +by (simp add: CFinite_def CInfinite_def, auto)
   1.871 +
   1.872 +lemma CFinite_not_CInfinite: "x \<in> CFinite ==> x \<notin> CInfinite"
   1.873 +by (insert CFinite_Int_CInfinite_empty, blast)
   1.874 +
   1.875 +text{*Not sure this is a good idea!*}
   1.876 +declare CFinite_Int_CInfinite_empty [simp]
   1.877 +
   1.878 +lemma not_CFinite_CInfinite: "x\<notin> CFinite ==> x \<in> CInfinite"
   1.879 +by (auto intro: not_HFinite_HInfinite simp add: CFinite_hcmod_iff CInfinite_hcmod_iff)
   1.880 +
   1.881 +lemma CInfinite_CFinite_disj: "x \<in> CInfinite | x \<in> CFinite"
   1.882 +by (blast intro: not_CFinite_CInfinite)
   1.883 +
   1.884 +lemma CInfinite_CFinite_iff: "(x \<in> CInfinite) = (x \<notin> CFinite)"
   1.885 +by (blast dest: CFinite_not_CInfinite not_CFinite_CInfinite)
   1.886 +
   1.887 +lemma CFinite_CInfinite_iff: "(x \<in> CFinite) = (x \<notin> CInfinite)"
   1.888 +by (simp add: CInfinite_CFinite_iff)
   1.889 +
   1.890 +lemma CInfinite_diff_CFinite_CInfinitesimal_disj:
   1.891 +     "x \<notin> CInfinitesimal ==> x \<in> CInfinite | x \<in> CFinite - CInfinitesimal"
   1.892 +by (fast intro: not_CFinite_CInfinite)
   1.893 +
   1.894 +lemma CFinite_inverse:
   1.895 +     "[| x \<in> CFinite; x \<notin> CInfinitesimal |] ==> inverse x \<in> CFinite"
   1.896 +apply (cut_tac x = "inverse x" in CInfinite_CFinite_disj)
   1.897 +apply (auto dest!: CInfinite_inverse_CInfinitesimal)
   1.898 +done
   1.899 +
   1.900 +lemma CFinite_inverse2: "x \<in> CFinite - CInfinitesimal ==> inverse x \<in> CFinite"
   1.901 +by (blast intro: CFinite_inverse)
   1.902 +
   1.903 +lemma CInfinitesimal_inverse_CFinite:
   1.904 +     "x \<notin> CInfinitesimal ==> inverse(x) \<in> CFinite"
   1.905 +apply (drule CInfinite_diff_CFinite_CInfinitesimal_disj)
   1.906 +apply (blast intro: CFinite_inverse CInfinite_inverse_CInfinitesimal CInfinitesimal_subset_CFinite [THEN subsetD])
   1.907 +done
   1.908 +
   1.909 +
   1.910 +lemma CFinite_not_CInfinitesimal_inverse:
   1.911 +     "x \<in> CFinite - CInfinitesimal ==> inverse x \<in> CFinite - CInfinitesimal"
   1.912 +apply (auto intro: CInfinitesimal_inverse_CFinite)
   1.913 +apply (drule CInfinitesimal_CFinite_mult2, assumption)
   1.914 +apply (simp add: not_CInfinitesimal_not_zero)
   1.915 +done
   1.916 +
   1.917 +lemma capprox_inverse:
   1.918 +     "[| x @c= y; y \<in>  CFinite - CInfinitesimal |] ==> inverse x @c= inverse y"
   1.919 +apply (frule CFinite_diff_CInfinitesimal_capprox, assumption)
   1.920 +apply (frule not_CInfinitesimal_not_zero2)
   1.921 +apply (frule_tac x = x in not_CInfinitesimal_not_zero2)
   1.922 +apply (drule CFinite_inverse2)+
   1.923 +apply (drule capprox_mult2, assumption, auto)
   1.924 +apply (drule_tac c = "inverse x" in capprox_mult1, assumption)
   1.925 +apply (auto intro: capprox_sym simp add: hcomplex_mult_assoc)
   1.926 +done
   1.927 +
   1.928 +lemmas hcomplex_of_complex_capprox_inverse =  hcomplex_of_complex_CFinite_diff_CInfinitesimal [THEN [2] capprox_inverse]
   1.929 +
   1.930 +lemma inverse_add_CInfinitesimal_capprox:
   1.931 +     "[| x \<in> CFinite - CInfinitesimal;  
   1.932 +         h \<in> CInfinitesimal |] ==> inverse(x + h) @c= inverse x"
   1.933 +by (auto intro: capprox_inverse capprox_sym CInfinitesimal_add_capprox_self)
   1.934 +
   1.935 +lemma inverse_add_CInfinitesimal_capprox2:
   1.936 +     "[| x \<in> CFinite - CInfinitesimal;  
   1.937 +         h \<in> CInfinitesimal |] ==> inverse(h + x) @c= inverse x"
   1.938 +apply (rule add_commute [THEN subst])
   1.939 +apply (blast intro: inverse_add_CInfinitesimal_capprox)
   1.940 +done
   1.941 +
   1.942 +lemma inverse_add_CInfinitesimal_approx_CInfinitesimal:
   1.943 +     "[| x \<in> CFinite - CInfinitesimal;  
   1.944 +         h \<in> CInfinitesimal |] ==> inverse(x + h) - inverse x @c= h"
   1.945 +apply (rule capprox_trans2)
   1.946 +apply (auto intro: inverse_add_CInfinitesimal_capprox 
   1.947 +       simp add: mem_cinfmal_iff diff_minus capprox_minus_iff [symmetric])
   1.948 +done
   1.949 +
   1.950 +lemma CInfinitesimal_square_iff [iff]:
   1.951 +     "(x*x \<in> CInfinitesimal) = (x \<in> CInfinitesimal)"
   1.952 +by (simp add: CInfinitesimal_hcmod_iff hcmod_mult)
   1.953 +
   1.954 +lemma capprox_CFinite_mult_cancel:
   1.955 +     "[| a \<in> CFinite-CInfinitesimal; a*w @c= a*z |] ==> w @c= z"
   1.956 +apply safe
   1.957 +apply (frule CFinite_inverse, assumption)
   1.958 +apply (drule not_CInfinitesimal_not_zero)
   1.959 +apply (auto dest: capprox_mult2 simp add: hcomplex_mult_assoc [symmetric])
   1.960 +done
   1.961 +
   1.962 +lemma capprox_CFinite_mult_cancel_iff1:
   1.963 +     "a \<in> CFinite-CInfinitesimal ==> (a * w @c= a * z) = (w @c= z)"
   1.964 +by (auto intro: capprox_mult2 capprox_CFinite_mult_cancel)
   1.965 +
   1.966 +
   1.967 +subsection{*Theorems About Monads*}
   1.968 +
   1.969 +lemma capprox_cmonad_iff: "(x @c= y) = (cmonad(x)=cmonad(y))"
   1.970 +apply (simp add: cmonad_def)
   1.971 +apply (auto dest: capprox_sym elim!: capprox_trans equalityCE)
   1.972 +done
   1.973 +
   1.974 +lemma CInfinitesimal_cmonad_eq:
   1.975 +     "e \<in> CInfinitesimal ==> cmonad (x+e) = cmonad x"
   1.976 +by (fast intro!: CInfinitesimal_add_capprox_self [THEN capprox_sym] capprox_cmonad_iff [THEN iffD1])
   1.977 +
   1.978 +lemma mem_cmonad_iff: "(u \<in> cmonad x) = (-u \<in> cmonad (-x))"
   1.979 +by (simp add: cmonad_def)
   1.980 +
   1.981 +lemma CInfinitesimal_cmonad_zero_iff: "(x:CInfinitesimal) = (x \<in> cmonad 0)"
   1.982 +by (auto intro: capprox_sym simp add: mem_cinfmal_iff cmonad_def)
   1.983 +
   1.984 +lemma cmonad_zero_minus_iff: "(x \<in> cmonad 0) = (-x \<in> cmonad 0)"
   1.985 +by (simp add: CInfinitesimal_cmonad_zero_iff [symmetric])
   1.986 +
   1.987 +lemma cmonad_zero_hcmod_iff: "(x \<in> cmonad 0) = (hcmod x:monad 0)"
   1.988 +by (simp add: CInfinitesimal_cmonad_zero_iff [symmetric] CInfinitesimal_hcmod_iff Infinitesimal_monad_zero_iff [symmetric])
   1.989 +
   1.990 +lemma mem_cmonad_self [simp]: "x \<in> cmonad x"
   1.991 +by (simp add: cmonad_def)
   1.992 +
   1.993 +
   1.994 +subsection{*Theorems About Standard Part*}
   1.995 +
   1.996 +lemma stc_capprox_self: "x \<in> CFinite ==> stc x @c= x"
   1.997 +apply (simp add: stc_def)
   1.998 +apply (frule stc_part_Ex, safe)
   1.999 +apply (rule someI2)
  1.1000 +apply (auto intro: capprox_sym)
  1.1001 +done
  1.1002 +
  1.1003 +lemma stc_SComplex: "x \<in> CFinite ==> stc x \<in> SComplex"
  1.1004 +apply (simp add: stc_def)
  1.1005 +apply (frule stc_part_Ex, safe)
  1.1006 +apply (rule someI2)
  1.1007 +apply (auto intro: capprox_sym)
  1.1008 +done
  1.1009 +
  1.1010 +lemma stc_CFinite: "x \<in> CFinite ==> stc x \<in> CFinite"
  1.1011 +by (erule stc_SComplex [THEN SComplex_subset_CFinite [THEN subsetD]])
  1.1012 +
  1.1013 +lemma stc_SComplex_eq [simp]: "x \<in> SComplex ==> stc x = x"
  1.1014 +apply (simp add: stc_def)
  1.1015 +apply (rule some_equality)
  1.1016 +apply (auto intro: SComplex_subset_CFinite [THEN subsetD])
  1.1017 +apply (blast dest: SComplex_capprox_iff [THEN iffD1])
  1.1018 +done
  1.1019 +
  1.1020 +lemma stc_hcomplex_of_complex:
  1.1021 +     "stc (hcomplex_of_complex x) = hcomplex_of_complex x"
  1.1022 +by auto
  1.1023 +
  1.1024 +lemma stc_eq_capprox:
  1.1025 +     "[| x \<in> CFinite; y \<in> CFinite; stc x = stc y |] ==> x @c= y"
  1.1026 +by (auto dest!: stc_capprox_self elim!: capprox_trans3)
  1.1027 +
  1.1028 +lemma capprox_stc_eq:
  1.1029 +     "[| x \<in> CFinite; y \<in> CFinite; x @c= y |] ==> stc x = stc y"
  1.1030 +by (blast intro: capprox_trans capprox_trans2 SComplex_capprox_iff [THEN iffD1]
  1.1031 +          dest: stc_capprox_self stc_SComplex)
  1.1032  
  1.1033 -   capprox_def  "x @c= y == (x - y) : CInfinitesimal"     
  1.1034 +lemma stc_eq_capprox_iff:
  1.1035 +     "[| x \<in> CFinite; y \<in> CFinite|] ==> (x @c= y) = (stc x = stc y)"
  1.1036 +by (blast intro: capprox_stc_eq stc_eq_capprox)
  1.1037 +
  1.1038 +lemma stc_CInfinitesimal_add_SComplex:
  1.1039 +     "[| x \<in> SComplex; e \<in> CInfinitesimal |] ==> stc(x + e) = x"
  1.1040 +apply (frule stc_SComplex_eq [THEN subst])
  1.1041 +prefer 2 apply assumption
  1.1042 +apply (frule SComplex_subset_CFinite [THEN subsetD])
  1.1043 +apply (frule CInfinitesimal_subset_CFinite [THEN subsetD])
  1.1044 +apply (drule stc_SComplex_eq)
  1.1045 +apply (rule capprox_stc_eq)
  1.1046 +apply (auto intro: CFinite_add simp add: CInfinitesimal_add_capprox_self [THEN capprox_sym])
  1.1047 +done
  1.1048 +
  1.1049 +lemma stc_CInfinitesimal_add_SComplex2:
  1.1050 +     "[| x \<in> SComplex; e \<in> CInfinitesimal |] ==> stc(e + x) = x"
  1.1051 +apply (rule add_commute [THEN subst])
  1.1052 +apply (blast intro!: stc_CInfinitesimal_add_SComplex)
  1.1053 +done
  1.1054 +
  1.1055 +lemma CFinite_stc_CInfinitesimal_add:
  1.1056 +     "x \<in> CFinite ==> \<exists>e \<in> CInfinitesimal. x = stc(x) + e"
  1.1057 +by (blast dest!: stc_capprox_self [THEN capprox_sym] bex_CInfinitesimal_iff2 [THEN iffD2])
  1.1058 +
  1.1059 +lemma stc_add:
  1.1060 +     "[| x \<in> CFinite; y \<in> CFinite |] ==> stc (x + y) = stc(x) + stc(y)"
  1.1061 +apply (frule CFinite_stc_CInfinitesimal_add)
  1.1062 +apply (frule_tac x = y in CFinite_stc_CInfinitesimal_add, safe)
  1.1063 +apply (subgoal_tac "stc (x + y) = stc ((stc x + e) + (stc y + ea))")
  1.1064 +apply (drule_tac [2] sym, drule_tac [2] sym)
  1.1065 + prefer 2 apply simp 
  1.1066 +apply (simp (no_asm_simp) add: add_ac)
  1.1067 +apply (drule stc_SComplex)+
  1.1068 +apply (drule SComplex_add, assumption)
  1.1069 +apply (drule CInfinitesimal_add, assumption)
  1.1070 +apply (rule add_assoc [THEN subst])
  1.1071 +apply (blast intro!: stc_CInfinitesimal_add_SComplex2)
  1.1072 +done
  1.1073 +
  1.1074 +lemma stc_number_of [simp]: "stc (number_of w) = number_of w"
  1.1075 +by (rule SComplex_number_of [THEN stc_SComplex_eq])
  1.1076 +
  1.1077 +lemma stc_zero [simp]: "stc 0 = 0"
  1.1078 +by simp
  1.1079 +
  1.1080 +lemma stc_one [simp]: "stc 1 = 1"
  1.1081 +by simp
  1.1082 +
  1.1083 +lemma stc_minus: "y \<in> CFinite ==> stc(-y) = -stc(y)"
  1.1084 +apply (frule CFinite_minus_iff [THEN iffD2])
  1.1085 +apply (rule hcomplex_add_minus_eq_minus)
  1.1086 +apply (drule stc_add [symmetric], assumption)
  1.1087 +apply (simp add: add_commute)
  1.1088 +done
  1.1089 +
  1.1090 +lemma stc_diff: 
  1.1091 +     "[| x \<in> CFinite; y \<in> CFinite |] ==> stc (x-y) = stc(x) - stc(y)"
  1.1092 +apply (simp add: diff_minus)
  1.1093 +apply (frule_tac y1 = y in stc_minus [symmetric])
  1.1094 +apply (drule_tac x1 = y in CFinite_minus_iff [THEN iffD2])
  1.1095 +apply (auto intro: stc_add)
  1.1096 +done
  1.1097 +
  1.1098 +lemma lemma_stc_mult:
  1.1099 +     "[| x \<in> CFinite; y \<in> CFinite;  
  1.1100 +         e \<in> CInfinitesimal;        
  1.1101 +         ea: CInfinitesimal |]    
  1.1102 +       ==> e*y + x*ea + e*ea: CInfinitesimal"
  1.1103 +apply (frule_tac x = e and y = y in CInfinitesimal_CFinite_mult)
  1.1104 +apply (frule_tac [2] x = ea and y = x in CInfinitesimal_CFinite_mult)
  1.1105 +apply (drule_tac [3] CInfinitesimal_mult)
  1.1106 +apply (auto intro: CInfinitesimal_add simp add: add_ac mult_ac)
  1.1107 +done
  1.1108 +
  1.1109 +lemma stc_mult:
  1.1110 +     "[| x \<in> CFinite; y \<in> CFinite |]  
  1.1111 +               ==> stc (x * y) = stc(x) * stc(y)"
  1.1112 +apply (frule CFinite_stc_CInfinitesimal_add)
  1.1113 +apply (frule_tac x = y in CFinite_stc_CInfinitesimal_add, safe)
  1.1114 +apply (subgoal_tac "stc (x * y) = stc ((stc x + e) * (stc y + ea))")
  1.1115 +apply (drule_tac [2] sym, drule_tac [2] sym)
  1.1116 + prefer 2 apply simp 
  1.1117 +apply (erule_tac V = "x = stc x + e" in thin_rl)
  1.1118 +apply (erule_tac V = "y = stc y + ea" in thin_rl)
  1.1119 +apply (simp add: hcomplex_add_mult_distrib right_distrib)
  1.1120 +apply (drule stc_SComplex)+
  1.1121 +apply (simp (no_asm_use) add: add_assoc)
  1.1122 +apply (rule stc_CInfinitesimal_add_SComplex)
  1.1123 +apply (blast intro!: SComplex_mult)
  1.1124 +apply (drule SComplex_subset_CFinite [THEN subsetD])+
  1.1125 +apply (rule add_assoc [THEN subst])
  1.1126 +apply (blast intro!: lemma_stc_mult)
  1.1127 +done
  1.1128 +
  1.1129 +lemma stc_CInfinitesimal: "x \<in> CInfinitesimal ==> stc x = 0"
  1.1130 +apply (rule stc_zero [THEN subst])
  1.1131 +apply (rule capprox_stc_eq)
  1.1132 +apply (auto intro: CInfinitesimal_subset_CFinite [THEN subsetD]
  1.1133 +                 simp add: mem_cinfmal_iff [symmetric])
  1.1134 +done
  1.1135 +
  1.1136 +lemma stc_not_CInfinitesimal: "stc(x) \<noteq> 0 ==> x \<notin> CInfinitesimal"
  1.1137 +by (fast intro: stc_CInfinitesimal)
  1.1138 +
  1.1139 +lemma stc_inverse:
  1.1140 +     "[| x \<in> CFinite; stc x \<noteq> 0 |]  
  1.1141 +      ==> stc(inverse x) = inverse (stc x)"
  1.1142 +apply (rule_tac c1 = "stc x" in hcomplex_mult_left_cancel [THEN iffD1])
  1.1143 +apply (auto simp add: stc_mult [symmetric] stc_not_CInfinitesimal CFinite_inverse)
  1.1144 +apply (subst right_inverse, auto)
  1.1145 +done
  1.1146 +
  1.1147 +lemma stc_divide [simp]:
  1.1148 +     "[| x \<in> CFinite; y \<in> CFinite; stc y \<noteq> 0 |]  
  1.1149 +      ==> stc(x/y) = (stc x) / (stc y)"
  1.1150 +by (simp add: divide_inverse_zero stc_mult stc_not_CInfinitesimal CFinite_inverse stc_inverse)
  1.1151 +
  1.1152 +lemma stc_idempotent [simp]: "x \<in> CFinite ==> stc(stc(x)) = stc(x)"
  1.1153 +by (blast intro: stc_CFinite stc_capprox_self capprox_stc_eq)
  1.1154 +
  1.1155 +lemma CFinite_HFinite_hcomplex_of_hypreal:
  1.1156 +     "z \<in> HFinite ==> hcomplex_of_hypreal z \<in> CFinite"
  1.1157 +apply (rule eq_Abs_hypreal [of z])
  1.1158 +apply (simp add: hcomplex_of_hypreal CFinite_HFinite_iff hypreal_zero_def [symmetric])
  1.1159 +done
  1.1160 +
  1.1161 +lemma SComplex_SReal_hcomplex_of_hypreal:
  1.1162 +     "x \<in> Reals ==>  hcomplex_of_hypreal x \<in> SComplex"
  1.1163 +apply (rule eq_Abs_hypreal [of x])
  1.1164 +apply (simp add: hcomplex_of_hypreal SComplex_SReal_iff hypreal_zero_def [symmetric])
  1.1165 +done
  1.1166 +
  1.1167 +lemma stc_hcomplex_of_hypreal: 
  1.1168 + "z \<in> HFinite ==> stc(hcomplex_of_hypreal z) = hcomplex_of_hypreal (st z)"
  1.1169 +apply (simp add: st_def stc_def)
  1.1170 +apply (frule st_part_Ex, safe)
  1.1171 +apply (rule someI2)
  1.1172 +apply (auto intro: approx_sym)
  1.1173 +apply (drule CFinite_HFinite_hcomplex_of_hypreal)
  1.1174 +apply (frule stc_part_Ex, safe)
  1.1175 +apply (rule someI2)
  1.1176 +apply (auto intro: capprox_sym intro!: capprox_unique_complex dest: SComplex_SReal_hcomplex_of_hypreal)
  1.1177 +done
  1.1178 +
  1.1179 +(*
  1.1180 +Goal "x \<in> CFinite ==> hcmod(stc x) = st(hcmod x)"
  1.1181 +by (dtac stc_capprox_self 1)
  1.1182 +by (auto_tac (claset(),simpset() addsimps [bex_CInfinitesimal_iff2 RS sym]));
  1.1183 +
  1.1184 +
  1.1185 +approx_hcmod_add_hcmod
  1.1186 +*)
  1.1187 +
  1.1188 +lemma CInfinitesimal_hcnj_iff [simp]:
  1.1189 +     "(hcnj z \<in> CInfinitesimal) = (z \<in> CInfinitesimal)"
  1.1190 +by (simp add: CInfinitesimal_hcmod_iff)
  1.1191 +
  1.1192 +lemma CInfinite_HInfinite_iff:
  1.1193 +     "(Abs_hcomplex(hcomplexrel ``{%n. X n}) \<in> CInfinite) =  
  1.1194 +      (Abs_hypreal(hyprel `` {%n. Re(X n)}) \<in> HInfinite |  
  1.1195 +       Abs_hypreal(hyprel `` {%n. Im(X n)}) \<in> HInfinite)"
  1.1196 +by (simp add: CInfinite_CFinite_iff HInfinite_HFinite_iff CFinite_HFinite_iff)
  1.1197 +
  1.1198 +text{*These theorems should probably be deleted*}
  1.1199 +lemma hcomplex_split_CInfinitesimal_iff:
  1.1200 +     "(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y \<in> CInfinitesimal) =  
  1.1201 +      (x \<in> Infinitesimal & y \<in> Infinitesimal)"
  1.1202 +apply (rule eq_Abs_hypreal [of x])
  1.1203 +apply (rule eq_Abs_hypreal [of y])
  1.1204 +apply (simp add: iii_def hcomplex_add hcomplex_mult hcomplex_of_hypreal CInfinitesimal_Infinitesimal_iff)
  1.1205 +done
  1.1206 +
  1.1207 +lemma hcomplex_split_CFinite_iff:
  1.1208 +     "(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y \<in> CFinite) =  
  1.1209 +      (x \<in> HFinite & y \<in> HFinite)"
  1.1210 +apply (rule eq_Abs_hypreal [of x])
  1.1211 +apply (rule eq_Abs_hypreal [of y])
  1.1212 +apply (simp add: iii_def hcomplex_add hcomplex_mult hcomplex_of_hypreal CFinite_HFinite_iff)
  1.1213 +done
  1.1214 +
  1.1215 +lemma hcomplex_split_SComplex_iff:
  1.1216 +     "(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y \<in> SComplex) =  
  1.1217 +      (x \<in> Reals & y \<in> Reals)"
  1.1218 +apply (rule eq_Abs_hypreal [of x])
  1.1219 +apply (rule eq_Abs_hypreal [of y])
  1.1220 +apply (simp add: iii_def hcomplex_add hcomplex_mult hcomplex_of_hypreal SComplex_SReal_iff)
  1.1221 +done
  1.1222 +
  1.1223 +lemma hcomplex_split_CInfinite_iff:
  1.1224 +     "(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y \<in> CInfinite) =  
  1.1225 +      (x \<in> HInfinite | y \<in> HInfinite)"
  1.1226 +apply (rule eq_Abs_hypreal [of x])
  1.1227 +apply (rule eq_Abs_hypreal [of y])
  1.1228 +apply (simp add: iii_def hcomplex_add hcomplex_mult hcomplex_of_hypreal CInfinite_HInfinite_iff)
  1.1229 +done
  1.1230 +
  1.1231 +lemma hcomplex_split_capprox_iff:
  1.1232 +     "(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y @c=  
  1.1233 +       hcomplex_of_hypreal x' + iii * hcomplex_of_hypreal y') =  
  1.1234 +      (x @= x' & y @= y')"
  1.1235 +apply (rule eq_Abs_hypreal [of x])
  1.1236 +apply (rule eq_Abs_hypreal [of y])
  1.1237 +apply (rule eq_Abs_hypreal [of x'])
  1.1238 +apply (rule eq_Abs_hypreal [of y'])
  1.1239 +apply (simp add: iii_def hcomplex_add hcomplex_mult hcomplex_of_hypreal capprox_approx_iff)
  1.1240 +done
  1.1241 +
  1.1242 +lemma complex_seq_to_hcomplex_CInfinitesimal:
  1.1243 +     "\<forall>n. cmod (X n - x) < inverse (real (Suc n)) ==>  
  1.1244 +      Abs_hcomplex(hcomplexrel``{X}) - hcomplex_of_complex x \<in> CInfinitesimal"
  1.1245 +apply (simp add: hcomplex_diff CInfinitesimal_hcmod_iff hcomplex_of_complex_def Infinitesimal_FreeUltrafilterNat_iff hcmod)
  1.1246 +apply (rule bexI, auto)
  1.1247 +apply (auto dest: FreeUltrafilterNat_inverse_real_of_posnat FreeUltrafilterNat_all FreeUltrafilterNat_Int intro: order_less_trans FreeUltrafilterNat_subset)
  1.1248 +done
  1.1249 +
  1.1250 +lemma CInfinitesimal_hcomplex_of_hypreal_epsilon [simp]:
  1.1251 +     "hcomplex_of_hypreal epsilon \<in> CInfinitesimal"
  1.1252 +by (simp add: CInfinitesimal_hcmod_iff)
  1.1253 +
  1.1254 +lemma hcomplex_of_complex_approx_zero_iff [simp]:
  1.1255 +     "(hcomplex_of_complex z @c= 0) = (z = 0)"
  1.1256 +by (simp add: hcomplex_of_complex_zero [symmetric]
  1.1257 +         del: hcomplex_of_complex_zero)
  1.1258 +
  1.1259 +lemma hcomplex_of_complex_approx_zero_iff2 [simp]:
  1.1260 +     "(0 @c= hcomplex_of_complex z) = (z = 0)"
  1.1261 +by (simp add: hcomplex_of_complex_zero [symmetric]
  1.1262 +         del: hcomplex_of_complex_zero)
  1.1263 +
  1.1264 +
  1.1265 +ML
  1.1266 +{*
  1.1267 +val SComplex_add = thm "SComplex_add";
  1.1268 +val SComplex_mult = thm "SComplex_mult";
  1.1269 +val SComplex_inverse = thm "SComplex_inverse";
  1.1270 +val SComplex_divide = thm "SComplex_divide";
  1.1271 +val SComplex_minus = thm "SComplex_minus";
  1.1272 +val SComplex_minus_iff = thm "SComplex_minus_iff";
  1.1273 +val SComplex_diff = thm "SComplex_diff";
  1.1274 +val SComplex_add_cancel = thm "SComplex_add_cancel";
  1.1275 +val SReal_hcmod_hcomplex_of_complex = thm "SReal_hcmod_hcomplex_of_complex";
  1.1276 +val SReal_hcmod_number_of = thm "SReal_hcmod_number_of";
  1.1277 +val SReal_hcmod_SComplex = thm "SReal_hcmod_SComplex";
  1.1278 +val SComplex_hcomplex_of_complex = thm "SComplex_hcomplex_of_complex";
  1.1279 +val SComplex_number_of = thm "SComplex_number_of";
  1.1280 +val SComplex_divide_number_of = thm "SComplex_divide_number_of";
  1.1281 +val SComplex_UNIV_complex = thm "SComplex_UNIV_complex";
  1.1282 +val SComplex_iff = thm "SComplex_iff";
  1.1283 +val hcomplex_of_complex_image = thm "hcomplex_of_complex_image";
  1.1284 +val inv_hcomplex_of_complex_image = thm "inv_hcomplex_of_complex_image";
  1.1285 +val SComplex_hcomplex_of_complex_image = thm "SComplex_hcomplex_of_complex_image";
  1.1286 +val SComplex_SReal_dense = thm "SComplex_SReal_dense";
  1.1287 +val SComplex_hcmod_SReal = thm "SComplex_hcmod_SReal";
  1.1288 +val SComplex_zero = thm "SComplex_zero";
  1.1289 +val SComplex_one = thm "SComplex_one";
  1.1290 +val CFinite_add = thm "CFinite_add";
  1.1291 +val CFinite_mult = thm "CFinite_mult";
  1.1292 +val CFinite_minus_iff = thm "CFinite_minus_iff";
  1.1293 +val SComplex_subset_CFinite = thm "SComplex_subset_CFinite";
  1.1294 +val HFinite_hcmod_hcomplex_of_complex = thm "HFinite_hcmod_hcomplex_of_complex";
  1.1295 +val CFinite_hcomplex_of_complex = thm "CFinite_hcomplex_of_complex";
  1.1296 +val CFiniteD = thm "CFiniteD";
  1.1297 +val CFinite_hcmod_iff = thm "CFinite_hcmod_iff";
  1.1298 +val CFinite_number_of = thm "CFinite_number_of";
  1.1299 +val CFinite_bounded = thm "CFinite_bounded";
  1.1300 +val CInfinitesimal_zero = thm "CInfinitesimal_zero";
  1.1301 +val hcomplex_sum_of_halves = thm "hcomplex_sum_of_halves";
  1.1302 +val CInfinitesimal_hcmod_iff = thm "CInfinitesimal_hcmod_iff";
  1.1303 +val one_not_CInfinitesimal = thm "one_not_CInfinitesimal";
  1.1304 +val CInfinitesimal_add = thm "CInfinitesimal_add";
  1.1305 +val CInfinitesimal_minus_iff = thm "CInfinitesimal_minus_iff";
  1.1306 +val CInfinitesimal_diff = thm "CInfinitesimal_diff";
  1.1307 +val CInfinitesimal_mult = thm "CInfinitesimal_mult";
  1.1308 +val CInfinitesimal_CFinite_mult = thm "CInfinitesimal_CFinite_mult";
  1.1309 +val CInfinitesimal_CFinite_mult2 = thm "CInfinitesimal_CFinite_mult2";
  1.1310 +val CInfinite_hcmod_iff = thm "CInfinite_hcmod_iff";
  1.1311 +val CInfinite_inverse_CInfinitesimal = thm "CInfinite_inverse_CInfinitesimal";
  1.1312 +val CInfinite_mult = thm "CInfinite_mult";
  1.1313 +val CInfinite_minus_iff = thm "CInfinite_minus_iff";
  1.1314 +val CFinite_sum_squares = thm "CFinite_sum_squares";
  1.1315 +val not_CInfinitesimal_not_zero = thm "not_CInfinitesimal_not_zero";
  1.1316 +val not_CInfinitesimal_not_zero2 = thm "not_CInfinitesimal_not_zero2";
  1.1317 +val CFinite_diff_CInfinitesimal_hcmod = thm "CFinite_diff_CInfinitesimal_hcmod";
  1.1318 +val hcmod_less_CInfinitesimal = thm "hcmod_less_CInfinitesimal";
  1.1319 +val hcmod_le_CInfinitesimal = thm "hcmod_le_CInfinitesimal";
  1.1320 +val CInfinitesimal_interval = thm "CInfinitesimal_interval";
  1.1321 +val CInfinitesimal_interval2 = thm "CInfinitesimal_interval2";
  1.1322 +val not_CInfinitesimal_mult = thm "not_CInfinitesimal_mult";
  1.1323 +val CInfinitesimal_mult_disj = thm "CInfinitesimal_mult_disj";
  1.1324 +val CFinite_CInfinitesimal_diff_mult = thm "CFinite_CInfinitesimal_diff_mult";
  1.1325 +val CInfinitesimal_subset_CFinite = thm "CInfinitesimal_subset_CFinite";
  1.1326 +val CInfinitesimal_hcomplex_of_complex_mult = thm "CInfinitesimal_hcomplex_of_complex_mult";
  1.1327 +val CInfinitesimal_hcomplex_of_complex_mult2 = thm "CInfinitesimal_hcomplex_of_complex_mult2";
  1.1328 +val mem_cinfmal_iff = thm "mem_cinfmal_iff";
  1.1329 +val capprox_minus_iff = thm "capprox_minus_iff";
  1.1330 +val capprox_minus_iff2 = thm "capprox_minus_iff2";
  1.1331 +val capprox_refl = thm "capprox_refl";
  1.1332 +val capprox_sym = thm "capprox_sym";
  1.1333 +val capprox_trans = thm "capprox_trans";
  1.1334 +val capprox_trans2 = thm "capprox_trans2";
  1.1335 +val capprox_trans3 = thm "capprox_trans3";
  1.1336 +val number_of_capprox_reorient = thm "number_of_capprox_reorient";
  1.1337 +val CInfinitesimal_capprox_minus = thm "CInfinitesimal_capprox_minus";
  1.1338 +val capprox_monad_iff = thm "capprox_monad_iff";
  1.1339 +val Infinitesimal_capprox = thm "Infinitesimal_capprox";
  1.1340 +val capprox_add = thm "capprox_add";
  1.1341 +val capprox_minus = thm "capprox_minus";
  1.1342 +val capprox_minus2 = thm "capprox_minus2";
  1.1343 +val capprox_minus_cancel = thm "capprox_minus_cancel";
  1.1344 +val capprox_add_minus = thm "capprox_add_minus";
  1.1345 +val capprox_mult1 = thm "capprox_mult1";
  1.1346 +val capprox_mult2 = thm "capprox_mult2";
  1.1347 +val capprox_mult_subst = thm "capprox_mult_subst";
  1.1348 +val capprox_mult_subst2 = thm "capprox_mult_subst2";
  1.1349 +val capprox_mult_subst_SComplex = thm "capprox_mult_subst_SComplex";
  1.1350 +val capprox_eq_imp = thm "capprox_eq_imp";
  1.1351 +val CInfinitesimal_minus_capprox = thm "CInfinitesimal_minus_capprox";
  1.1352 +val bex_CInfinitesimal_iff = thm "bex_CInfinitesimal_iff";
  1.1353 +val bex_CInfinitesimal_iff2 = thm "bex_CInfinitesimal_iff2";
  1.1354 +val CInfinitesimal_add_capprox = thm "CInfinitesimal_add_capprox";
  1.1355 +val CInfinitesimal_add_capprox_self = thm "CInfinitesimal_add_capprox_self";
  1.1356 +val CInfinitesimal_add_capprox_self2 = thm "CInfinitesimal_add_capprox_self2";
  1.1357 +val CInfinitesimal_add_minus_capprox_self = thm "CInfinitesimal_add_minus_capprox_self";
  1.1358 +val CInfinitesimal_add_cancel = thm "CInfinitesimal_add_cancel";
  1.1359 +val CInfinitesimal_add_right_cancel = thm "CInfinitesimal_add_right_cancel";
  1.1360 +val capprox_add_left_cancel = thm "capprox_add_left_cancel";
  1.1361 +val capprox_add_right_cancel = thm "capprox_add_right_cancel";
  1.1362 +val capprox_add_mono1 = thm "capprox_add_mono1";
  1.1363 +val capprox_add_mono2 = thm "capprox_add_mono2";
  1.1364 +val capprox_add_left_iff = thm "capprox_add_left_iff";
  1.1365 +val capprox_add_right_iff = thm "capprox_add_right_iff";
  1.1366 +val capprox_CFinite = thm "capprox_CFinite";
  1.1367 +val capprox_hcomplex_of_complex_CFinite = thm "capprox_hcomplex_of_complex_CFinite";
  1.1368 +val capprox_mult_CFinite = thm "capprox_mult_CFinite";
  1.1369 +val capprox_mult_hcomplex_of_complex = thm "capprox_mult_hcomplex_of_complex";
  1.1370 +val capprox_SComplex_mult_cancel_zero = thm "capprox_SComplex_mult_cancel_zero";
  1.1371 +val capprox_mult_SComplex1 = thm "capprox_mult_SComplex1";
  1.1372 +val capprox_mult_SComplex2 = thm "capprox_mult_SComplex2";
  1.1373 +val capprox_mult_SComplex_zero_cancel_iff = thm "capprox_mult_SComplex_zero_cancel_iff";
  1.1374 +val capprox_SComplex_mult_cancel = thm "capprox_SComplex_mult_cancel";
  1.1375 +val capprox_SComplex_mult_cancel_iff1 = thm "capprox_SComplex_mult_cancel_iff1";
  1.1376 +val capprox_hcmod_approx_zero = thm "capprox_hcmod_approx_zero";
  1.1377 +val capprox_approx_zero_iff = thm "capprox_approx_zero_iff";
  1.1378 +val capprox_minus_zero_cancel_iff = thm "capprox_minus_zero_cancel_iff";
  1.1379 +val Infinitesimal_hcmod_add_diff = thm "Infinitesimal_hcmod_add_diff";
  1.1380 +val approx_hcmod_add_hcmod = thm "approx_hcmod_add_hcmod";
  1.1381 +val capprox_hcmod_approx = thm "capprox_hcmod_approx";
  1.1382 +val CInfinitesimal_less_SComplex = thm "CInfinitesimal_less_SComplex";
  1.1383 +val SComplex_Int_CInfinitesimal_zero = thm "SComplex_Int_CInfinitesimal_zero";
  1.1384 +val SComplex_CInfinitesimal_zero = thm "SComplex_CInfinitesimal_zero";
  1.1385 +val SComplex_CFinite_diff_CInfinitesimal = thm "SComplex_CFinite_diff_CInfinitesimal";
  1.1386 +val hcomplex_of_complex_CFinite_diff_CInfinitesimal = thm "hcomplex_of_complex_CFinite_diff_CInfinitesimal";
  1.1387 +val hcomplex_of_complex_CInfinitesimal_iff_0 = thm "hcomplex_of_complex_CInfinitesimal_iff_0";
  1.1388 +val number_of_not_CInfinitesimal = thm "number_of_not_CInfinitesimal";
  1.1389 +val capprox_SComplex_not_zero = thm "capprox_SComplex_not_zero";
  1.1390 +val CFinite_diff_CInfinitesimal_capprox = thm "CFinite_diff_CInfinitesimal_capprox";
  1.1391 +val CInfinitesimal_ratio = thm "CInfinitesimal_ratio";
  1.1392 +val SComplex_capprox_iff = thm "SComplex_capprox_iff";
  1.1393 +val number_of_capprox_iff = thm "number_of_capprox_iff";
  1.1394 +val number_of_CInfinitesimal_iff = thm "number_of_CInfinitesimal_iff";
  1.1395 +val hcomplex_of_complex_approx_iff = thm "hcomplex_of_complex_approx_iff";
  1.1396 +val hcomplex_of_complex_capprox_number_of_iff = thm "hcomplex_of_complex_capprox_number_of_iff";
  1.1397 +val capprox_unique_complex = thm "capprox_unique_complex";
  1.1398 +val hcomplex_capproxD1 = thm "hcomplex_capproxD1";
  1.1399 +val hcomplex_capproxD2 = thm "hcomplex_capproxD2";
  1.1400 +val hcomplex_capproxI = thm "hcomplex_capproxI";
  1.1401 +val capprox_approx_iff = thm "capprox_approx_iff";
  1.1402 +val hcomplex_of_hypreal_capprox_iff = thm "hcomplex_of_hypreal_capprox_iff";
  1.1403 +val CFinite_HFinite_Re = thm "CFinite_HFinite_Re";
  1.1404 +val CFinite_HFinite_Im = thm "CFinite_HFinite_Im";
  1.1405 +val HFinite_Re_Im_CFinite = thm "HFinite_Re_Im_CFinite";
  1.1406 +val CFinite_HFinite_iff = thm "CFinite_HFinite_iff";
  1.1407 +val SComplex_Re_SReal = thm "SComplex_Re_SReal";
  1.1408 +val SComplex_Im_SReal = thm "SComplex_Im_SReal";
  1.1409 +val Reals_Re_Im_SComplex = thm "Reals_Re_Im_SComplex";
  1.1410 +val SComplex_SReal_iff = thm "SComplex_SReal_iff";
  1.1411 +val CInfinitesimal_Infinitesimal_iff = thm "CInfinitesimal_Infinitesimal_iff";
  1.1412 +val eq_Abs_hcomplex_Bex = thm "eq_Abs_hcomplex_Bex";
  1.1413 +val stc_part_Ex = thm "stc_part_Ex";
  1.1414 +val stc_part_Ex1 = thm "stc_part_Ex1";
  1.1415 +val CFinite_Int_CInfinite_empty = thm "CFinite_Int_CInfinite_empty";
  1.1416 +val CFinite_not_CInfinite = thm "CFinite_not_CInfinite";
  1.1417 +val not_CFinite_CInfinite = thm "not_CFinite_CInfinite";
  1.1418 +val CInfinite_CFinite_disj = thm "CInfinite_CFinite_disj";
  1.1419 +val CInfinite_CFinite_iff = thm "CInfinite_CFinite_iff";
  1.1420 +val CFinite_CInfinite_iff = thm "CFinite_CInfinite_iff";
  1.1421 +val CInfinite_diff_CFinite_CInfinitesimal_disj = thm "CInfinite_diff_CFinite_CInfinitesimal_disj";
  1.1422 +val CFinite_inverse = thm "CFinite_inverse";
  1.1423 +val CFinite_inverse2 = thm "CFinite_inverse2";
  1.1424 +val CInfinitesimal_inverse_CFinite = thm "CInfinitesimal_inverse_CFinite";
  1.1425 +val CFinite_not_CInfinitesimal_inverse = thm "CFinite_not_CInfinitesimal_inverse";
  1.1426 +val capprox_inverse = thm "capprox_inverse";
  1.1427 +val hcomplex_of_complex_capprox_inverse = thms "hcomplex_of_complex_capprox_inverse";
  1.1428 +val inverse_add_CInfinitesimal_capprox = thm "inverse_add_CInfinitesimal_capprox";
  1.1429 +val inverse_add_CInfinitesimal_capprox2 = thm "inverse_add_CInfinitesimal_capprox2";
  1.1430 +val inverse_add_CInfinitesimal_approx_CInfinitesimal = thm "inverse_add_CInfinitesimal_approx_CInfinitesimal";
  1.1431 +val CInfinitesimal_square_iff = thm "CInfinitesimal_square_iff";
  1.1432 +val capprox_CFinite_mult_cancel = thm "capprox_CFinite_mult_cancel";
  1.1433 +val capprox_CFinite_mult_cancel_iff1 = thm "capprox_CFinite_mult_cancel_iff1";
  1.1434 +val capprox_cmonad_iff = thm "capprox_cmonad_iff";
  1.1435 +val CInfinitesimal_cmonad_eq = thm "CInfinitesimal_cmonad_eq";
  1.1436 +val mem_cmonad_iff = thm "mem_cmonad_iff";
  1.1437 +val CInfinitesimal_cmonad_zero_iff = thm "CInfinitesimal_cmonad_zero_iff";
  1.1438 +val cmonad_zero_minus_iff = thm "cmonad_zero_minus_iff";
  1.1439 +val cmonad_zero_hcmod_iff = thm "cmonad_zero_hcmod_iff";
  1.1440 +val mem_cmonad_self = thm "mem_cmonad_self";
  1.1441 +val stc_capprox_self = thm "stc_capprox_self";
  1.1442 +val stc_SComplex = thm "stc_SComplex";
  1.1443 +val stc_CFinite = thm "stc_CFinite";
  1.1444 +val stc_SComplex_eq = thm "stc_SComplex_eq";
  1.1445 +val stc_hcomplex_of_complex = thm "stc_hcomplex_of_complex";
  1.1446 +val stc_eq_capprox = thm "stc_eq_capprox";
  1.1447 +val capprox_stc_eq = thm "capprox_stc_eq";
  1.1448 +val stc_eq_capprox_iff = thm "stc_eq_capprox_iff";
  1.1449 +val stc_CInfinitesimal_add_SComplex = thm "stc_CInfinitesimal_add_SComplex";
  1.1450 +val stc_CInfinitesimal_add_SComplex2 = thm "stc_CInfinitesimal_add_SComplex2";
  1.1451 +val CFinite_stc_CInfinitesimal_add = thm "CFinite_stc_CInfinitesimal_add";
  1.1452 +val stc_add = thm "stc_add";
  1.1453 +val stc_number_of = thm "stc_number_of";
  1.1454 +val stc_zero = thm "stc_zero";
  1.1455 +val stc_one = thm "stc_one";
  1.1456 +val stc_minus = thm "stc_minus";
  1.1457 +val stc_diff = thm "stc_diff";
  1.1458 +val lemma_stc_mult = thm "lemma_stc_mult";
  1.1459 +val stc_mult = thm "stc_mult";
  1.1460 +val stc_CInfinitesimal = thm "stc_CInfinitesimal";
  1.1461 +val stc_not_CInfinitesimal = thm "stc_not_CInfinitesimal";
  1.1462 +val stc_inverse = thm "stc_inverse";
  1.1463 +val stc_divide = thm "stc_divide";
  1.1464 +val stc_idempotent = thm "stc_idempotent";
  1.1465 +val CFinite_HFinite_hcomplex_of_hypreal = thm "CFinite_HFinite_hcomplex_of_hypreal";
  1.1466 +val SComplex_SReal_hcomplex_of_hypreal = thm "SComplex_SReal_hcomplex_of_hypreal";
  1.1467 +val stc_hcomplex_of_hypreal = thm "stc_hcomplex_of_hypreal";
  1.1468 +val CInfinitesimal_hcnj_iff = thm "CInfinitesimal_hcnj_iff";
  1.1469 +val CInfinite_HInfinite_iff = thm "CInfinite_HInfinite_iff";
  1.1470 +val hcomplex_split_CInfinitesimal_iff = thm "hcomplex_split_CInfinitesimal_iff";
  1.1471 +val hcomplex_split_CFinite_iff = thm "hcomplex_split_CFinite_iff";
  1.1472 +val hcomplex_split_SComplex_iff = thm "hcomplex_split_SComplex_iff";
  1.1473 +val hcomplex_split_CInfinite_iff = thm "hcomplex_split_CInfinite_iff";
  1.1474 +val hcomplex_split_capprox_iff = thm "hcomplex_split_capprox_iff";
  1.1475 +val complex_seq_to_hcomplex_CInfinitesimal = thm "complex_seq_to_hcomplex_CInfinitesimal";
  1.1476 +val CInfinitesimal_hcomplex_of_hypreal_epsilon = thm "CInfinitesimal_hcomplex_of_hypreal_epsilon";
  1.1477 +val hcomplex_of_complex_approx_zero_iff = thm "hcomplex_of_complex_approx_zero_iff";
  1.1478 +val hcomplex_of_complex_approx_zero_iff2 = thm "hcomplex_of_complex_approx_zero_iff2";
  1.1479 +*}
  1.1480 +
  1.1481   
  1.1482  end