src/HOL/Complex/NSCA.thy
author nipkow
Wed Aug 18 11:09:40 2004 +0200 (2004-08-18)
changeset 15140 322485b816ac
parent 15131 c69542757a4d
child 15229 1eb23f805c06
permissions -rw-r--r--
import -> imports
     1 (*  Title       : NSCA.thy
     2     Author      : Jacques D. Fleuriot
     3     Copyright   : 2001,2002 University of Edinburgh
     4 *)
     5 
     6 header{*Non-Standard Complex Analysis*}
     7 
     8 theory NSCA
     9 imports NSComplex
    10 begin
    11 
    12 constdefs
    13 
    14    CInfinitesimal  :: "hcomplex set"
    15    "CInfinitesimal == {x. \<forall>r \<in> Reals. 0 < r --> hcmod x < r}"
    16 
    17     capprox    :: "[hcomplex,hcomplex] => bool"  (infixl "@c=" 50)  
    18       --{*the ``infinitely close'' relation*}
    19       "x @c= y == (x - y) \<in> CInfinitesimal"     
    20   
    21    (* standard complex numbers reagarded as an embedded subset of NS complex *)
    22    SComplex  :: "hcomplex set"
    23    "SComplex == {x. \<exists>r. x = hcomplex_of_complex r}"
    24 
    25    CFinite :: "hcomplex set"
    26    "CFinite == {x. \<exists>r \<in> Reals. hcmod x < r}"
    27 
    28    CInfinite :: "hcomplex set"
    29    "CInfinite == {x. \<forall>r \<in> Reals. r < hcmod x}"
    30 
    31    stc :: "hcomplex => hcomplex"
    32     --{* standard part map*}
    33    "stc x == (@r. x \<in> CFinite & r:SComplex & r @c= x)"
    34 
    35    cmonad    :: "hcomplex => hcomplex set"
    36    "cmonad x  == {y. x @c= y}"
    37 
    38    cgalaxy   :: "hcomplex => hcomplex set"
    39    "cgalaxy x == {y. (x - y) \<in> CFinite}"
    40 
    41 
    42 
    43 subsection{*Closure Laws for SComplex, the Standard Complex Numbers*}
    44 
    45 lemma SComplex_add: "[| x \<in> SComplex; y \<in> SComplex |] ==> x + y \<in> SComplex"
    46 apply (simp add: SComplex_def, safe)
    47 apply (rule_tac x = "r + ra" in exI, simp)
    48 done
    49 
    50 lemma SComplex_mult: "[| x \<in> SComplex; y \<in> SComplex |] ==> x * y \<in> SComplex"
    51 apply (simp add: SComplex_def, safe)
    52 apply (rule_tac x = "r * ra" in exI, simp)
    53 done
    54 
    55 lemma SComplex_inverse: "x \<in> SComplex ==> inverse x \<in> SComplex"
    56 apply (simp add: SComplex_def)
    57 apply (blast intro: hcomplex_of_complex_inverse [symmetric])
    58 done
    59 
    60 lemma SComplex_divide: "[| x \<in> SComplex;  y \<in> SComplex |] ==> x/y \<in> SComplex"
    61 by (simp add: SComplex_mult SComplex_inverse divide_inverse)
    62 
    63 lemma SComplex_minus: "x \<in> SComplex ==> -x \<in> SComplex"
    64 apply (simp add: SComplex_def)
    65 apply (blast intro: hcomplex_of_complex_minus [symmetric])
    66 done
    67 
    68 lemma SComplex_minus_iff [simp]: "(-x \<in> SComplex) = (x \<in> SComplex)"
    69 apply auto
    70 apply (erule_tac [2] SComplex_minus)
    71 apply (drule SComplex_minus, auto)
    72 done
    73 
    74 lemma SComplex_diff: "[| x \<in> SComplex; y \<in> SComplex |] ==> x - y \<in> SComplex"
    75 by (simp add: diff_minus SComplex_add) 
    76 
    77 lemma SComplex_add_cancel:
    78      "[| x + y \<in> SComplex; y \<in> SComplex |] ==> x \<in> SComplex"
    79 by (drule SComplex_diff, assumption, simp)
    80 
    81 lemma SReal_hcmod_hcomplex_of_complex [simp]:
    82      "hcmod (hcomplex_of_complex r) \<in> Reals"
    83 by (simp add: hcomplex_of_complex_def hcmod SReal_def hypreal_of_real_def)
    84 
    85 lemma SReal_hcmod_number_of [simp]: "hcmod (number_of w ::hcomplex) \<in> Reals"
    86 apply (subst hcomplex_number_of [symmetric])
    87 apply (rule SReal_hcmod_hcomplex_of_complex)
    88 done
    89 
    90 lemma SReal_hcmod_SComplex: "x \<in> SComplex ==> hcmod x \<in> Reals"
    91 by (auto simp add: SComplex_def)
    92 
    93 lemma SComplex_hcomplex_of_complex [simp]: "hcomplex_of_complex x \<in> SComplex"
    94 by (simp add: SComplex_def)
    95 
    96 lemma SComplex_number_of [simp]: "(number_of w ::hcomplex) \<in> SComplex"
    97 apply (subst hcomplex_number_of [symmetric])
    98 apply (rule SComplex_hcomplex_of_complex)
    99 done
   100 
   101 lemma SComplex_divide_number_of:
   102      "r \<in> SComplex ==> r/(number_of w::hcomplex) \<in> SComplex"
   103 apply (simp only: divide_inverse)
   104 apply (blast intro!: SComplex_number_of SComplex_mult SComplex_inverse)
   105 done
   106 
   107 lemma SComplex_UNIV_complex:
   108      "{x. hcomplex_of_complex x \<in> SComplex} = (UNIV::complex set)"
   109 by (simp add: SComplex_def)
   110 
   111 lemma SComplex_iff: "(x \<in> SComplex) = (\<exists>y. x = hcomplex_of_complex y)"
   112 by (simp add: SComplex_def)
   113 
   114 lemma hcomplex_of_complex_image:
   115      "hcomplex_of_complex `(UNIV::complex set) = SComplex"
   116 by (auto simp add: SComplex_def)
   117 
   118 lemma inv_hcomplex_of_complex_image: "inv hcomplex_of_complex `SComplex = UNIV"
   119 apply (auto simp add: SComplex_def)
   120 apply (rule inj_hcomplex_of_complex [THEN inv_f_f, THEN subst], blast)
   121 done
   122 
   123 lemma SComplex_hcomplex_of_complex_image: 
   124       "[| \<exists>x. x: P; P \<le> SComplex |] ==> \<exists>Q. P = hcomplex_of_complex ` Q"
   125 apply (simp add: SComplex_def, blast)
   126 done
   127 
   128 lemma SComplex_SReal_dense:
   129      "[| x \<in> SComplex; y \<in> SComplex; hcmod x < hcmod y  
   130       |] ==> \<exists>r \<in> Reals. hcmod x< r & r < hcmod y"
   131 apply (auto intro: SReal_dense simp add: SReal_hcmod_SComplex)
   132 done
   133 
   134 lemma SComplex_hcmod_SReal: 
   135       "z \<in> SComplex ==> hcmod z \<in> Reals"
   136 apply (simp add: SComplex_def SReal_def)
   137 apply (rule_tac z = z in eq_Abs_hcomplex)
   138 apply (auto simp add: hcmod hypreal_of_real_def hcomplex_of_complex_def cmod_def)
   139 apply (rule_tac x = "cmod r" in exI)
   140 apply (simp add: cmod_def, ultra)
   141 done
   142 
   143 lemma SComplex_zero [simp]: "0 \<in> SComplex"
   144 by (simp add: SComplex_def hcomplex_of_complex_zero_iff)
   145 
   146 lemma SComplex_one [simp]: "1 \<in> SComplex"
   147 by (simp add: SComplex_def hcomplex_of_complex_def hcomplex_one_def)
   148 
   149 (*
   150 Goalw [SComplex_def,SReal_def] "hcmod z \<in> Reals ==> z \<in> SComplex"
   151 by (res_inst_tac [("z","z")] eq_Abs_hcomplex 1);
   152 by (auto_tac (claset(),simpset() addsimps [hcmod,hypreal_of_real_def,
   153     hcomplex_of_complex_def,cmod_def]));
   154 *)
   155 
   156 
   157 subsection{*The Finite Elements form a Subring*}
   158 
   159 lemma CFinite_add: "[|x \<in> CFinite; y \<in> CFinite|] ==> (x+y) \<in> CFinite"
   160 apply (simp add: CFinite_def)
   161 apply (blast intro!: SReal_add hcmod_add_less)
   162 done
   163 
   164 lemma CFinite_mult: "[|x \<in> CFinite; y \<in> CFinite|] ==> x*y \<in> CFinite"
   165 apply (simp add: CFinite_def)
   166 apply (blast intro!: SReal_mult hcmod_mult_less)
   167 done
   168 
   169 lemma CFinite_minus_iff [simp]: "(-x \<in> CFinite) = (x \<in> CFinite)"
   170 by (simp add: CFinite_def)
   171 
   172 lemma SComplex_subset_CFinite [simp]: "SComplex \<le> CFinite"
   173 apply (auto simp add: SComplex_def CFinite_def)
   174 apply (rule_tac x = "1 + hcmod (hcomplex_of_complex r) " in bexI)
   175 apply (auto intro: SReal_add)
   176 done
   177 
   178 lemma HFinite_hcmod_hcomplex_of_complex [simp]:
   179      "hcmod (hcomplex_of_complex r) \<in> HFinite"
   180 by (auto intro!: SReal_subset_HFinite [THEN subsetD])
   181 
   182 lemma CFinite_hcomplex_of_complex [simp]: "hcomplex_of_complex x \<in> CFinite"
   183 by (auto intro!: SComplex_subset_CFinite [THEN subsetD])
   184 
   185 lemma CFiniteD: "x \<in> CFinite ==> \<exists>t \<in> Reals. hcmod x < t"
   186 by (simp add: CFinite_def)
   187 
   188 lemma CFinite_hcmod_iff: "(x \<in> CFinite) = (hcmod x \<in> HFinite)"
   189 by (simp add: CFinite_def HFinite_def)
   190 
   191 lemma CFinite_number_of [simp]: "number_of w \<in> CFinite"
   192 by (rule SComplex_number_of [THEN SComplex_subset_CFinite [THEN subsetD]])
   193 
   194 lemma CFinite_bounded: "[|x \<in> CFinite; y \<le> hcmod x; 0 \<le> y |] ==> y: HFinite"
   195 by (auto intro: HFinite_bounded simp add: CFinite_hcmod_iff)
   196 
   197 
   198 subsection{*The Complex Infinitesimals form a Subring*}
   199 	 
   200 lemma CInfinitesimal_zero [iff]: "0 \<in> CInfinitesimal"
   201 by (simp add: CInfinitesimal_def)
   202 
   203 lemma hcomplex_sum_of_halves: "x/(2::hcomplex) + x/(2::hcomplex) = x"
   204 by auto
   205 
   206 lemma CInfinitesimal_hcmod_iff: 
   207    "(z \<in> CInfinitesimal) = (hcmod z \<in> Infinitesimal)"
   208 by (simp add: CInfinitesimal_def Infinitesimal_def)
   209 
   210 lemma one_not_CInfinitesimal [simp]: "1 \<notin> CInfinitesimal"
   211 by (simp add: CInfinitesimal_hcmod_iff)
   212 
   213 lemma CInfinitesimal_add:
   214      "[| x \<in> CInfinitesimal; y \<in> CInfinitesimal |] ==> (x+y) \<in> CInfinitesimal"
   215 apply (auto simp add: CInfinitesimal_hcmod_iff)
   216 apply (rule hrabs_le_Infinitesimal)
   217 apply (rule_tac y = "hcmod y" in Infinitesimal_add, auto)
   218 done
   219 
   220 lemma CInfinitesimal_minus_iff [simp]:
   221      "(-x:CInfinitesimal) = (x:CInfinitesimal)"
   222 by (simp add: CInfinitesimal_def)
   223 
   224 lemma CInfinitesimal_diff:
   225      "[| x \<in> CInfinitesimal;  y \<in> CInfinitesimal |] ==> x-y \<in> CInfinitesimal"
   226 by (simp add: diff_minus CInfinitesimal_add)
   227 
   228 lemma CInfinitesimal_mult:
   229      "[| x \<in> CInfinitesimal; y \<in> CInfinitesimal |] ==> x * y \<in> CInfinitesimal"
   230 by (auto intro: Infinitesimal_mult simp add: CInfinitesimal_hcmod_iff hcmod_mult)
   231 
   232 lemma CInfinitesimal_CFinite_mult:
   233      "[| x \<in> CInfinitesimal; y \<in> CFinite |] ==> (x * y) \<in> CInfinitesimal"
   234 by (auto intro: Infinitesimal_HFinite_mult simp add: CInfinitesimal_hcmod_iff CFinite_hcmod_iff hcmod_mult)
   235 
   236 lemma CInfinitesimal_CFinite_mult2:
   237      "[| x \<in> CInfinitesimal; y \<in> CFinite |] ==> (y * x) \<in> CInfinitesimal"
   238 by (auto dest: CInfinitesimal_CFinite_mult simp add: hcomplex_mult_commute)
   239 
   240 lemma CInfinite_hcmod_iff: "(z \<in> CInfinite) = (hcmod z \<in> HInfinite)"
   241 by (simp add: CInfinite_def HInfinite_def)
   242 
   243 lemma CInfinite_inverse_CInfinitesimal:
   244      "x \<in> CInfinite ==> inverse x \<in> CInfinitesimal"
   245 by (auto intro: HInfinite_inverse_Infinitesimal simp add: CInfinitesimal_hcmod_iff CInfinite_hcmod_iff hcmod_hcomplex_inverse)
   246 
   247 lemma CInfinite_mult: "[|x \<in> CInfinite; y \<in> CInfinite|] ==> (x*y): CInfinite"
   248 by (auto intro: HInfinite_mult simp add: CInfinite_hcmod_iff hcmod_mult)
   249 
   250 lemma CInfinite_minus_iff [simp]: "(-x \<in> CInfinite) = (x \<in> CInfinite)"
   251 by (simp add: CInfinite_def)
   252 
   253 lemma CFinite_sum_squares:
   254      "[|a \<in> CFinite; b \<in> CFinite; c \<in> CFinite|]   
   255       ==> a*a + b*b + c*c \<in> CFinite"
   256 by (auto intro: CFinite_mult CFinite_add)
   257 
   258 lemma not_CInfinitesimal_not_zero: "x \<notin> CInfinitesimal ==> x \<noteq> 0"
   259 by auto
   260 
   261 lemma not_CInfinitesimal_not_zero2: "x \<in> CFinite - CInfinitesimal ==> x \<noteq> 0"
   262 by auto
   263 
   264 lemma CFinite_diff_CInfinitesimal_hcmod:
   265      "x \<in> CFinite - CInfinitesimal ==> hcmod x \<in> HFinite - Infinitesimal"
   266 by (simp add: CFinite_hcmod_iff CInfinitesimal_hcmod_iff)
   267 
   268 lemma hcmod_less_CInfinitesimal:
   269      "[| e \<in> CInfinitesimal; hcmod x < hcmod e |] ==> x \<in> CInfinitesimal"
   270 by (auto intro: hrabs_less_Infinitesimal simp add: CInfinitesimal_hcmod_iff)
   271 
   272 lemma hcmod_le_CInfinitesimal:
   273      "[| e \<in> CInfinitesimal; hcmod x \<le> hcmod e |] ==> x \<in> CInfinitesimal"
   274 by (auto intro: hrabs_le_Infinitesimal simp add: CInfinitesimal_hcmod_iff)
   275 
   276 lemma CInfinitesimal_interval:
   277      "[| e \<in> CInfinitesimal;  
   278           e' \<in> CInfinitesimal;  
   279           hcmod e' < hcmod x ; hcmod x < hcmod e  
   280        |] ==> x \<in> CInfinitesimal"
   281 by (auto intro: Infinitesimal_interval simp add: CInfinitesimal_hcmod_iff)
   282 
   283 lemma CInfinitesimal_interval2:
   284      "[| e \<in> CInfinitesimal;  
   285          e' \<in> CInfinitesimal;  
   286          hcmod e' \<le> hcmod x ; hcmod x \<le> hcmod e  
   287       |] ==> x \<in> CInfinitesimal"
   288 by (auto intro: Infinitesimal_interval2 simp add: CInfinitesimal_hcmod_iff)
   289 
   290 lemma not_CInfinitesimal_mult:
   291      "[| x \<notin> CInfinitesimal;  y \<notin> CInfinitesimal|] ==> (x*y) \<notin> CInfinitesimal"
   292 apply (auto simp add: CInfinitesimal_hcmod_iff hcmod_mult)
   293 apply (drule not_Infinitesimal_mult, auto)
   294 done
   295 
   296 lemma CInfinitesimal_mult_disj:
   297      "x*y \<in> CInfinitesimal ==> x \<in> CInfinitesimal | y \<in> CInfinitesimal"
   298 by (auto dest: Infinitesimal_mult_disj simp add: CInfinitesimal_hcmod_iff hcmod_mult)
   299 
   300 lemma CFinite_CInfinitesimal_diff_mult:
   301      "[| x \<in> CFinite - CInfinitesimal; y \<in> CFinite - CInfinitesimal |] 
   302       ==> x*y \<in> CFinite - CInfinitesimal"
   303 by (blast dest: CFinite_mult not_CInfinitesimal_mult)
   304 
   305 lemma CInfinitesimal_subset_CFinite: "CInfinitesimal \<le> CFinite"
   306 by (auto intro: Infinitesimal_subset_HFinite [THEN subsetD]
   307          simp add: CInfinitesimal_hcmod_iff CFinite_hcmod_iff)
   308 
   309 lemma CInfinitesimal_hcomplex_of_complex_mult:
   310      "x \<in> CInfinitesimal ==> x * hcomplex_of_complex r \<in> CInfinitesimal"
   311 by (auto intro!: Infinitesimal_HFinite_mult simp add: CInfinitesimal_hcmod_iff hcmod_mult)
   312 
   313 lemma CInfinitesimal_hcomplex_of_complex_mult2:
   314      "x \<in> CInfinitesimal ==> hcomplex_of_complex r * x \<in> CInfinitesimal"
   315 by (auto intro!: Infinitesimal_HFinite_mult2 simp add: CInfinitesimal_hcmod_iff hcmod_mult)
   316 
   317 
   318 subsection{*The ``Infinitely Close'' Relation*}
   319 
   320 (*
   321 Goalw [capprox_def,approx_def] "(z @c= w) = (hcmod z @= hcmod w)"
   322 by (auto_tac (claset(),simpset() addsimps [CInfinitesimal_hcmod_iff]));
   323 *)
   324 
   325 lemma mem_cinfmal_iff: "x:CInfinitesimal = (x @c= 0)"
   326 by (simp add: CInfinitesimal_hcmod_iff capprox_def)
   327 
   328 lemma capprox_minus_iff: "(x @c= y) = (x + -y @c= 0)"
   329 by (simp add: capprox_def diff_minus)
   330 
   331 lemma capprox_minus_iff2: "(x @c= y) = (-y + x @c= 0)"
   332 by (simp add: capprox_def diff_minus add_commute)
   333 
   334 lemma capprox_refl [simp]: "x @c= x"
   335 by (simp add: capprox_def)
   336 
   337 lemma capprox_sym: "x @c= y ==> y @c= x"
   338 by (simp add: capprox_def CInfinitesimal_def hcmod_diff_commute)
   339 
   340 lemma capprox_trans: "[| x @c= y; y @c= z |] ==> x @c= z"
   341 apply (simp add: capprox_def)
   342 apply (drule CInfinitesimal_add, assumption)
   343 apply (simp add: diff_minus)
   344 done
   345 
   346 lemma capprox_trans2: "[| r @c= x; s @c= x |] ==> r @c= s"
   347 by (blast intro: capprox_sym capprox_trans)
   348 
   349 lemma capprox_trans3: "[| x @c= r; x @c= s|] ==> r @c= s"
   350 by (blast intro: capprox_sym capprox_trans)
   351 
   352 lemma number_of_capprox_reorient [simp]:
   353      "(number_of w @c= x) = (x @c= number_of w)"
   354 by (blast intro: capprox_sym)
   355 
   356 lemma CInfinitesimal_capprox_minus: "(x-y \<in> CInfinitesimal) = (x @c= y)"
   357 by (simp add: diff_minus capprox_minus_iff [symmetric] mem_cinfmal_iff)
   358 
   359 lemma capprox_monad_iff: "(x @c= y) = (cmonad(x)=cmonad(y))"
   360 by (auto simp add: cmonad_def dest: capprox_sym elim!: capprox_trans equalityCE)
   361 
   362 lemma Infinitesimal_capprox:
   363      "[| x \<in> CInfinitesimal; y \<in> CInfinitesimal |] ==> x @c= y"
   364 apply (simp add: mem_cinfmal_iff)
   365 apply (blast intro: capprox_trans capprox_sym)
   366 done
   367 
   368 lemma capprox_add: "[| a @c= b; c @c= d |] ==> a+c @c= b+d"
   369 apply (simp add: capprox_def diff_minus) 
   370 apply (rule minus_add_distrib [THEN ssubst])
   371 apply (rule add_assoc [THEN ssubst])
   372 apply (rule_tac b1 = c in add_left_commute [THEN subst])
   373 apply (rule add_assoc [THEN subst])
   374 apply (blast intro: CInfinitesimal_add)
   375 done
   376 
   377 lemma capprox_minus: "a @c= b ==> -a @c= -b"
   378 apply (rule capprox_minus_iff [THEN iffD2, THEN capprox_sym])
   379 apply (drule capprox_minus_iff [THEN iffD1])
   380 apply (simp add: add_commute)
   381 done
   382 
   383 lemma capprox_minus2: "-a @c= -b ==> a @c= b"
   384 by (auto dest: capprox_minus)
   385 
   386 lemma capprox_minus_cancel [simp]: "(-a @c= -b) = (a @c= b)"
   387 by (blast intro: capprox_minus capprox_minus2)
   388 
   389 lemma capprox_add_minus: "[| a @c= b; c @c= d |] ==> a + -c @c= b + -d"
   390 by (blast intro!: capprox_add capprox_minus)
   391 
   392 lemma capprox_mult1: 
   393       "[| a @c= b; c \<in> CFinite|] ==> a*c @c= b*c"
   394 apply (simp add: capprox_def diff_minus)
   395 apply (simp only: CInfinitesimal_CFinite_mult minus_mult_left hcomplex_add_mult_distrib [symmetric])
   396 done
   397 
   398 lemma capprox_mult2: "[|a @c= b; c \<in> CFinite|] ==> c*a @c= c*b"
   399 by (simp add: capprox_mult1 hcomplex_mult_commute)
   400 
   401 lemma capprox_mult_subst:
   402      "[|u @c= v*x; x @c= y; v \<in> CFinite|] ==> u @c= v*y"
   403 by (blast intro: capprox_mult2 capprox_trans)
   404 
   405 lemma capprox_mult_subst2:
   406      "[| u @c= x*v; x @c= y; v \<in> CFinite |] ==> u @c= y*v"
   407 by (blast intro: capprox_mult1 capprox_trans)
   408 
   409 lemma capprox_mult_subst_SComplex:
   410      "[| u @c= x*hcomplex_of_complex v; x @c= y |] 
   411       ==> u @c= y*hcomplex_of_complex v"
   412 by (auto intro: capprox_mult_subst2)
   413 
   414 lemma capprox_eq_imp: "a = b ==> a @c= b"
   415 by (simp add: capprox_def)
   416 
   417 lemma CInfinitesimal_minus_capprox: "x \<in> CInfinitesimal ==> -x @c= x"
   418 by (blast intro: CInfinitesimal_minus_iff [THEN iffD2] mem_cinfmal_iff [THEN iffD1] capprox_trans2)
   419 
   420 lemma bex_CInfinitesimal_iff: "(\<exists>y \<in> CInfinitesimal. x - z = y) = (x @c= z)"
   421 by (unfold capprox_def, blast)
   422 
   423 lemma bex_CInfinitesimal_iff2: "(\<exists>y \<in> CInfinitesimal. x = z + y) = (x @c= z)"
   424 by (simp add: bex_CInfinitesimal_iff [symmetric], force)
   425 
   426 lemma CInfinitesimal_add_capprox:
   427      "[| y \<in> CInfinitesimal; x + y = z |] ==> x @c= z"
   428 apply (rule bex_CInfinitesimal_iff [THEN iffD1])
   429 apply (drule CInfinitesimal_minus_iff [THEN iffD2])
   430 apply (simp add: eq_commute compare_rls)
   431 done
   432 
   433 lemma CInfinitesimal_add_capprox_self: "y \<in> CInfinitesimal ==> x @c= x + y"
   434 apply (rule bex_CInfinitesimal_iff [THEN iffD1])
   435 apply (drule CInfinitesimal_minus_iff [THEN iffD2])
   436 apply (simp add: eq_commute compare_rls)
   437 done
   438 
   439 lemma CInfinitesimal_add_capprox_self2: "y \<in> CInfinitesimal ==> x @c= y + x"
   440 by (auto dest: CInfinitesimal_add_capprox_self simp add: add_commute)
   441 
   442 lemma CInfinitesimal_add_minus_capprox_self:
   443      "y \<in> CInfinitesimal ==> x @c= x + -y"
   444 by (blast intro!: CInfinitesimal_add_capprox_self CInfinitesimal_minus_iff [THEN iffD2])
   445 
   446 lemma CInfinitesimal_add_cancel:
   447      "[| y \<in> CInfinitesimal; x+y @c= z|] ==> x @c= z"
   448 apply (drule_tac x = x in CInfinitesimal_add_capprox_self [THEN capprox_sym])
   449 apply (erule capprox_trans3 [THEN capprox_sym], assumption)
   450 done
   451 
   452 lemma CInfinitesimal_add_right_cancel:
   453      "[| y \<in> CInfinitesimal; x @c= z + y|] ==> x @c= z"
   454 apply (drule_tac x = z in CInfinitesimal_add_capprox_self2 [THEN capprox_sym])
   455 apply (erule capprox_trans3 [THEN capprox_sym])
   456 apply (simp add: add_commute)
   457 apply (erule capprox_sym)
   458 done
   459 
   460 lemma capprox_add_left_cancel: "d + b  @c= d + c ==> b @c= c"
   461 apply (drule capprox_minus_iff [THEN iffD1])
   462 apply (simp add: minus_add_distrib capprox_minus_iff [symmetric] add_ac)
   463 done
   464 
   465 lemma capprox_add_right_cancel: "b + d @c= c + d ==> b @c= c"
   466 apply (rule capprox_add_left_cancel)
   467 apply (simp add: add_commute)
   468 done
   469 
   470 lemma capprox_add_mono1: "b @c= c ==> d + b @c= d + c"
   471 apply (rule capprox_minus_iff [THEN iffD2])
   472 apply (simp add: capprox_minus_iff [symmetric] add_ac)
   473 done
   474 
   475 lemma capprox_add_mono2: "b @c= c ==> b + a @c= c + a"
   476 apply (simp (no_asm_simp) add: add_commute capprox_add_mono1)
   477 done
   478 
   479 lemma capprox_add_left_iff [iff]: "(a + b @c= a + c) = (b @c= c)"
   480 by (fast elim: capprox_add_left_cancel capprox_add_mono1)
   481 
   482 lemma capprox_add_right_iff [iff]: "(b + a @c= c + a) = (b @c= c)"
   483 by (simp add: add_commute)
   484 
   485 lemma capprox_CFinite: "[| x \<in> CFinite; x @c= y |] ==> y \<in> CFinite"
   486 apply (drule bex_CInfinitesimal_iff2 [THEN iffD2], safe)
   487 apply (drule CInfinitesimal_subset_CFinite [THEN subsetD, THEN CFinite_minus_iff [THEN iffD2]])
   488 apply (drule CFinite_add)
   489 apply (assumption, auto)
   490 done
   491 
   492 lemma capprox_hcomplex_of_complex_CFinite:
   493      "x @c= hcomplex_of_complex D ==> x \<in> CFinite"
   494 by (rule capprox_sym [THEN [2] capprox_CFinite], auto)
   495 
   496 lemma capprox_mult_CFinite:
   497      "[|a @c= b; c @c= d; b \<in> CFinite; d \<in> CFinite|] ==> a*c @c= b*d"
   498 apply (rule capprox_trans)
   499 apply (rule_tac [2] capprox_mult2)
   500 apply (rule capprox_mult1)
   501 prefer 2 apply (blast intro: capprox_CFinite capprox_sym, auto)
   502 done
   503 
   504 lemma capprox_mult_hcomplex_of_complex:
   505      "[|a @c= hcomplex_of_complex b; c @c= hcomplex_of_complex d |]  
   506       ==> a*c @c= hcomplex_of_complex b * hcomplex_of_complex d"
   507 apply (blast intro!: capprox_mult_CFinite capprox_hcomplex_of_complex_CFinite CFinite_hcomplex_of_complex)
   508 done
   509 
   510 lemma capprox_SComplex_mult_cancel_zero:
   511      "[| a \<in> SComplex; a \<noteq> 0; a*x @c= 0 |] ==> x @c= 0"
   512 apply (drule SComplex_inverse [THEN SComplex_subset_CFinite [THEN subsetD]])
   513 apply (auto dest: capprox_mult2 simp add: mult_assoc [symmetric])
   514 done
   515 
   516 lemma capprox_mult_SComplex1: "[| a \<in> SComplex; x @c= 0 |] ==> x*a @c= 0"
   517 by (auto dest: SComplex_subset_CFinite [THEN subsetD] capprox_mult1)
   518 
   519 lemma capprox_mult_SComplex2: "[| a \<in> SComplex; x @c= 0 |] ==> a*x @c= 0"
   520 by (auto dest: SComplex_subset_CFinite [THEN subsetD] capprox_mult2)
   521 
   522 lemma capprox_mult_SComplex_zero_cancel_iff [simp]:
   523      "[|a \<in> SComplex; a \<noteq> 0 |] ==> (a*x @c= 0) = (x @c= 0)"
   524 by (blast intro: capprox_SComplex_mult_cancel_zero capprox_mult_SComplex2)
   525 
   526 lemma capprox_SComplex_mult_cancel:
   527      "[| a \<in> SComplex; a \<noteq> 0; a* w @c= a*z |] ==> w @c= z"
   528 apply (drule SComplex_inverse [THEN SComplex_subset_CFinite [THEN subsetD]])
   529 apply (auto dest: capprox_mult2 simp add: mult_assoc [symmetric])
   530 done
   531 
   532 lemma capprox_SComplex_mult_cancel_iff1 [simp]:
   533      "[| a \<in> SComplex; a \<noteq> 0|] ==> (a* w @c= a*z) = (w @c= z)"
   534 by (auto intro!: capprox_mult2 SComplex_subset_CFinite [THEN subsetD]
   535             intro: capprox_SComplex_mult_cancel)
   536 
   537 lemma capprox_hcmod_approx_zero: "(x @c= y) = (hcmod (y - x) @= 0)"
   538 apply (rule capprox_minus_iff [THEN ssubst])
   539 apply (simp add: capprox_def CInfinitesimal_hcmod_iff mem_infmal_iff diff_minus [symmetric] hcmod_diff_commute)
   540 done
   541 
   542 lemma capprox_approx_zero_iff: "(x @c= 0) = (hcmod x @= 0)"
   543 by (simp add: capprox_hcmod_approx_zero)
   544 
   545 lemma capprox_minus_zero_cancel_iff [simp]: "(-x @c= 0) = (x @c= 0)"
   546 by (simp add: capprox_hcmod_approx_zero)
   547 
   548 lemma Infinitesimal_hcmod_add_diff:
   549      "u @c= 0 ==> hcmod(x + u) - hcmod x \<in> Infinitesimal"
   550 apply (rule_tac e = "hcmod u" and e' = "- hcmod u" in Infinitesimal_interval2)
   551 apply (auto dest: capprox_approx_zero_iff [THEN iffD1]
   552              simp add: mem_infmal_iff [symmetric] hypreal_diff_def)
   553 apply (rule_tac c1 = "hcmod x" in add_le_cancel_left [THEN iffD1])
   554 apply (auto simp add: diff_minus [symmetric])
   555 done
   556 
   557 lemma approx_hcmod_add_hcmod: "u @c= 0 ==> hcmod(x + u) @= hcmod x"
   558 apply (rule approx_minus_iff [THEN iffD2])
   559 apply (auto intro: Infinitesimal_hcmod_add_diff simp add: mem_infmal_iff [symmetric] diff_minus [symmetric])
   560 done
   561 
   562 lemma capprox_hcmod_approx: "x @c= y ==> hcmod x @= hcmod y"
   563 by (auto intro: approx_hcmod_add_hcmod 
   564          dest!: bex_CInfinitesimal_iff2 [THEN iffD2]
   565          simp add: mem_cinfmal_iff)
   566 
   567 
   568 subsection{*Zero is the Only Infinitesimal Complex Number*}
   569 
   570 lemma CInfinitesimal_less_SComplex:
   571    "[| x \<in> SComplex; y \<in> CInfinitesimal; 0 < hcmod x |] ==> hcmod y < hcmod x"
   572 by (auto intro!: Infinitesimal_less_SReal SComplex_hcmod_SReal simp add: CInfinitesimal_hcmod_iff)
   573 
   574 lemma SComplex_Int_CInfinitesimal_zero: "SComplex Int CInfinitesimal = {0}"
   575 apply (auto simp add: SComplex_def CInfinitesimal_hcmod_iff)
   576 apply (cut_tac r = r in SReal_hcmod_hcomplex_of_complex)
   577 apply (drule_tac A = Reals in IntI, assumption)
   578 apply (subgoal_tac "hcmod (hcomplex_of_complex r) = 0")
   579 apply simp
   580 apply (simp add: SReal_Int_Infinitesimal_zero) 
   581 done
   582 
   583 lemma SComplex_CInfinitesimal_zero:
   584      "[| x \<in> SComplex; x \<in> CInfinitesimal|] ==> x = 0"
   585 by (cut_tac SComplex_Int_CInfinitesimal_zero, blast)
   586 
   587 lemma SComplex_CFinite_diff_CInfinitesimal:
   588      "[| x \<in> SComplex; x \<noteq> 0 |] ==> x \<in> CFinite - CInfinitesimal"
   589 by (auto dest: SComplex_CInfinitesimal_zero SComplex_subset_CFinite [THEN subsetD])
   590 
   591 lemma hcomplex_of_complex_CFinite_diff_CInfinitesimal:
   592      "hcomplex_of_complex x \<noteq> 0 
   593       ==> hcomplex_of_complex x \<in> CFinite - CInfinitesimal"
   594 by (rule SComplex_CFinite_diff_CInfinitesimal, auto)
   595 
   596 lemma hcomplex_of_complex_CInfinitesimal_iff_0 [iff]:
   597      "(hcomplex_of_complex x \<in> CInfinitesimal) = (x=0)"
   598 apply (auto simp add: hcomplex_of_complex_zero)
   599 apply (rule ccontr)
   600 apply (rule hcomplex_of_complex_CFinite_diff_CInfinitesimal [THEN DiffD2], auto)
   601 done
   602 
   603 lemma number_of_not_CInfinitesimal [simp]:
   604      "number_of w \<noteq> (0::hcomplex) ==> number_of w \<notin> CInfinitesimal"
   605 by (fast dest: SComplex_number_of [THEN SComplex_CInfinitesimal_zero])
   606 
   607 lemma capprox_SComplex_not_zero:
   608      "[| y \<in> SComplex; x @c= y; y\<noteq> 0 |] ==> x \<noteq> 0"
   609 by (auto dest: SComplex_CInfinitesimal_zero capprox_sym [THEN mem_cinfmal_iff [THEN iffD2]])
   610 
   611 lemma CFinite_diff_CInfinitesimal_capprox:
   612      "[| x @c= y; y \<in> CFinite - CInfinitesimal |]  
   613       ==> x \<in> CFinite - CInfinitesimal"
   614 apply (auto intro: capprox_sym [THEN [2] capprox_CFinite] 
   615             simp add: mem_cinfmal_iff)
   616 apply (drule capprox_trans3, assumption)
   617 apply (blast dest: capprox_sym)
   618 done
   619 
   620 lemma CInfinitesimal_ratio:
   621      "[| y \<noteq> 0;  y \<in> CInfinitesimal;  x/y \<in> CFinite |] ==> x \<in> CInfinitesimal"
   622 apply (drule CInfinitesimal_CFinite_mult2, assumption)
   623 apply (simp add: divide_inverse mult_assoc)
   624 done
   625 
   626 lemma SComplex_capprox_iff:
   627      "[|x \<in> SComplex; y \<in> SComplex|] ==> (x @c= y) = (x = y)"
   628 apply auto
   629 apply (simp add: capprox_def)
   630 apply (subgoal_tac "x-y = 0", simp) 
   631 apply (rule SComplex_CInfinitesimal_zero)
   632 apply (simp add: SComplex_diff, assumption)
   633 done
   634 
   635 lemma number_of_capprox_iff [simp]:
   636     "(number_of v @c= number_of w) = (number_of v = (number_of w :: hcomplex))"
   637 by (rule SComplex_capprox_iff, auto)
   638 
   639 lemma number_of_CInfinitesimal_iff [simp]:
   640      "(number_of w \<in> CInfinitesimal) = (number_of w = (0::hcomplex))"
   641 apply (rule iffI)
   642 apply (fast dest: SComplex_number_of [THEN SComplex_CInfinitesimal_zero])
   643 apply (simp (no_asm_simp))
   644 done
   645 
   646 lemma hcomplex_of_complex_approx_iff [simp]:
   647      "(hcomplex_of_complex k @c= hcomplex_of_complex m) = (k = m)"
   648 apply auto
   649 apply (rule inj_hcomplex_of_complex [THEN injD])
   650 apply (rule SComplex_capprox_iff [THEN iffD1], auto)
   651 done
   652 
   653 lemma hcomplex_of_complex_capprox_number_of_iff [simp]:
   654      "(hcomplex_of_complex k @c= number_of w) = (k = number_of w)"
   655 by (subst hcomplex_of_complex_approx_iff [symmetric], auto)
   656 
   657 lemma capprox_unique_complex:
   658      "[| r \<in> SComplex; s \<in> SComplex; r @c= x; s @c= x|] ==> r = s"
   659 by (blast intro: SComplex_capprox_iff [THEN iffD1] capprox_trans2)
   660 
   661 lemma hcomplex_capproxD1:
   662      "Abs_hcomplex(hcomplexrel ``{%n. X n}) @c= Abs_hcomplex(hcomplexrel``{%n. Y n})  
   663       ==> Abs_hypreal(hyprel `` {%n. Re(X n)}) @=  
   664           Abs_hypreal(hyprel `` {%n. Re(Y n)})"
   665 apply (auto simp add: approx_FreeUltrafilterNat_iff)
   666 apply (drule capprox_minus_iff [THEN iffD1])
   667 apply (auto simp add: hcomplex_minus hcomplex_add mem_cinfmal_iff [symmetric] CInfinitesimal_hcmod_iff hcmod Infinitesimal_FreeUltrafilterNat_iff2)
   668 apply (drule_tac x = m in spec, ultra)
   669 apply (rename_tac Z x)
   670 apply (case_tac "X x")
   671 apply (case_tac "Y x")
   672 apply (auto simp add: complex_minus complex_add complex_mod
   673            simp del: realpow_Suc)
   674 apply (rule_tac y="abs(Z x)" in order_le_less_trans)
   675 apply (drule_tac t = "Z x" in sym)
   676 apply (auto simp add: abs_eqI1 simp del: realpow_Suc)
   677 done
   678 
   679 (* same proof *)
   680 lemma hcomplex_capproxD2:
   681      "Abs_hcomplex(hcomplexrel ``{%n. X n}) @c= Abs_hcomplex(hcomplexrel``{%n. Y n})  
   682       ==> Abs_hypreal(hyprel `` {%n. Im(X n)}) @=  
   683           Abs_hypreal(hyprel `` {%n. Im(Y n)})"
   684 apply (auto simp add: approx_FreeUltrafilterNat_iff)
   685 apply (drule capprox_minus_iff [THEN iffD1])
   686 apply (auto simp add: hcomplex_minus hcomplex_add mem_cinfmal_iff [symmetric] CInfinitesimal_hcmod_iff hcmod Infinitesimal_FreeUltrafilterNat_iff2)
   687 apply (drule_tac x = m in spec, ultra)
   688 apply (rename_tac Z x)
   689 apply (case_tac "X x")
   690 apply (case_tac "Y x")
   691 apply (auto simp add: complex_minus complex_add complex_mod simp del: realpow_Suc)
   692 apply (rule_tac y="abs(Z x)" in order_le_less_trans)
   693 apply (drule_tac t = "Z x" in sym)
   694 apply (auto simp add: abs_eqI1 simp del: realpow_Suc)
   695 done
   696 
   697 lemma hcomplex_capproxI:
   698      "[| Abs_hypreal(hyprel `` {%n. Re(X n)}) @=  
   699          Abs_hypreal(hyprel `` {%n. Re(Y n)});  
   700          Abs_hypreal(hyprel `` {%n. Im(X n)}) @=  
   701          Abs_hypreal(hyprel `` {%n. Im(Y n)})  
   702       |] ==> Abs_hcomplex(hcomplexrel ``{%n. X n}) @c= Abs_hcomplex(hcomplexrel``{%n. Y n})"
   703 apply (drule approx_minus_iff [THEN iffD1])
   704 apply (drule approx_minus_iff [THEN iffD1])
   705 apply (rule capprox_minus_iff [THEN iffD2])
   706 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)
   707 apply (rule bexI, rule_tac [2] lemma_hyprel_refl, auto)
   708 apply (drule_tac x = "u/2" in spec)
   709 apply (drule_tac x = "u/2" in spec, auto, ultra)
   710 apply (drule sym, drule sym)
   711 apply (case_tac "X x")
   712 apply (case_tac "Y x")
   713 apply (auto simp add: complex_minus complex_add complex_mod snd_conv fst_conv numeral_2_eq_2)
   714 apply (rename_tac a b c d)
   715 apply (subgoal_tac "sqrt (abs (a + - c) ^ 2 + abs (b + - d) ^ 2) < u")
   716 apply (rule_tac [2] lemma_sqrt_hcomplex_capprox, auto)
   717 apply (simp add: power2_eq_square)
   718 done
   719 
   720 lemma capprox_approx_iff:
   721      "(Abs_hcomplex(hcomplexrel ``{%n. X n}) @c= Abs_hcomplex(hcomplexrel``{%n. Y n})) = 
   722        (Abs_hypreal(hyprel `` {%n. Re(X n)}) @= Abs_hypreal(hyprel `` {%n. Re(Y n)}) &  
   723         Abs_hypreal(hyprel `` {%n. Im(X n)}) @= Abs_hypreal(hyprel `` {%n. Im(Y n)}))"
   724 apply (blast intro: hcomplex_capproxI hcomplex_capproxD1 hcomplex_capproxD2)
   725 done
   726 
   727 lemma hcomplex_of_hypreal_capprox_iff [simp]:
   728      "(hcomplex_of_hypreal x @c= hcomplex_of_hypreal z) = (x @= z)"
   729 apply (cases x, cases z)
   730 apply (simp add: hcomplex_of_hypreal capprox_approx_iff)
   731 done
   732 
   733 lemma CFinite_HFinite_Re:
   734      "Abs_hcomplex(hcomplexrel ``{%n. X n}) \<in> CFinite  
   735       ==> Abs_hypreal(hyprel `` {%n. Re(X n)}) \<in> HFinite"
   736 apply (auto simp add: CFinite_hcmod_iff hcmod HFinite_FreeUltrafilterNat_iff)
   737 apply (rule bexI, rule_tac [2] lemma_hyprel_refl)
   738 apply (rule_tac x = u in exI, ultra)
   739 apply (drule sym, case_tac "X x")
   740 apply (auto simp add: complex_mod numeral_2_eq_2 simp del: realpow_Suc)
   741 apply (rule ccontr, drule linorder_not_less [THEN iffD1])
   742 apply (drule order_less_le_trans, assumption)
   743 apply (drule real_sqrt_ge_abs1 [THEN [2] order_less_le_trans]) 
   744 apply (auto simp add: numeral_2_eq_2 [symmetric]) 
   745 done
   746 
   747 lemma CFinite_HFinite_Im:
   748      "Abs_hcomplex(hcomplexrel ``{%n. X n}) \<in> CFinite  
   749       ==> Abs_hypreal(hyprel `` {%n. Im(X n)}) \<in> HFinite"
   750 apply (auto simp add: CFinite_hcmod_iff hcmod HFinite_FreeUltrafilterNat_iff)
   751 apply (rule bexI, rule_tac [2] lemma_hyprel_refl)
   752 apply (rule_tac x = u in exI, ultra)
   753 apply (drule sym, case_tac "X x")
   754 apply (auto simp add: complex_mod simp del: realpow_Suc)
   755 apply (rule ccontr, drule linorder_not_less [THEN iffD1])
   756 apply (drule order_less_le_trans, assumption)
   757 apply (drule real_sqrt_ge_abs2 [THEN [2] order_less_le_trans], auto) 
   758 done
   759 
   760 lemma HFinite_Re_Im_CFinite:
   761      "[| Abs_hypreal(hyprel `` {%n. Re(X n)}) \<in> HFinite;  
   762          Abs_hypreal(hyprel `` {%n. Im(X n)}) \<in> HFinite  
   763       |] ==> Abs_hcomplex(hcomplexrel ``{%n. X n}) \<in> CFinite"
   764 apply (auto simp add: CFinite_hcmod_iff hcmod HFinite_FreeUltrafilterNat_iff)
   765 apply (rename_tac Y Z u v)
   766 apply (rule bexI, rule_tac [2] lemma_hyprel_refl)
   767 apply (rule_tac x = "2* (u + v) " in exI)
   768 apply ultra
   769 apply (drule sym, case_tac "X x")
   770 apply (auto simp add: complex_mod numeral_2_eq_2 simp del: realpow_Suc)
   771 apply (subgoal_tac "0 < u")
   772  prefer 2 apply arith
   773 apply (subgoal_tac "0 < v")
   774  prefer 2 apply arith
   775 apply (subgoal_tac "sqrt (abs (Y x) ^ 2 + abs (Z x) ^ 2) < 2*u + 2*v")
   776 apply (rule_tac [2] lemma_sqrt_hcomplex_capprox, auto)
   777 apply (simp add: power2_eq_square)
   778 done
   779 
   780 lemma CFinite_HFinite_iff:
   781      "(Abs_hcomplex(hcomplexrel ``{%n. X n}) \<in> CFinite) =  
   782       (Abs_hypreal(hyprel `` {%n. Re(X n)}) \<in> HFinite &  
   783        Abs_hypreal(hyprel `` {%n. Im(X n)}) \<in> HFinite)"
   784 by (blast intro: HFinite_Re_Im_CFinite CFinite_HFinite_Im CFinite_HFinite_Re)
   785 
   786 lemma SComplex_Re_SReal:
   787      "Abs_hcomplex(hcomplexrel ``{%n. X n}) \<in> SComplex  
   788       ==> Abs_hypreal(hyprel `` {%n. Re(X n)}) \<in> Reals"
   789 apply (auto simp add: SComplex_def hcomplex_of_complex_def SReal_def hypreal_of_real_def)
   790 apply (rule_tac x = "Re r" in exI, ultra)
   791 done
   792 
   793 lemma SComplex_Im_SReal:
   794      "Abs_hcomplex(hcomplexrel ``{%n. X n}) \<in> SComplex  
   795       ==> Abs_hypreal(hyprel `` {%n. Im(X n)}) \<in> Reals"
   796 apply (auto simp add: SComplex_def hcomplex_of_complex_def SReal_def hypreal_of_real_def)
   797 apply (rule_tac x = "Im r" in exI, ultra)
   798 done
   799 
   800 lemma Reals_Re_Im_SComplex:
   801      "[| Abs_hypreal(hyprel `` {%n. Re(X n)}) \<in> Reals;  
   802          Abs_hypreal(hyprel `` {%n. Im(X n)}) \<in> Reals  
   803       |] ==> Abs_hcomplex(hcomplexrel ``{%n. X n}) \<in> SComplex"
   804 apply (auto simp add: SComplex_def hcomplex_of_complex_def SReal_def hypreal_of_real_def)
   805 apply (rule_tac x = "Complex r ra" in exI, ultra)
   806 done
   807 
   808 lemma SComplex_SReal_iff:
   809      "(Abs_hcomplex(hcomplexrel ``{%n. X n}) \<in> SComplex) =  
   810       (Abs_hypreal(hyprel `` {%n. Re(X n)}) \<in> Reals &  
   811        Abs_hypreal(hyprel `` {%n. Im(X n)}) \<in> Reals)"
   812 by (blast intro: SComplex_Re_SReal SComplex_Im_SReal Reals_Re_Im_SComplex)
   813 
   814 lemma CInfinitesimal_Infinitesimal_iff:
   815      "(Abs_hcomplex(hcomplexrel ``{%n. X n}) \<in> CInfinitesimal) =  
   816       (Abs_hypreal(hyprel `` {%n. Re(X n)}) \<in> Infinitesimal &  
   817        Abs_hypreal(hyprel `` {%n. Im(X n)}) \<in> Infinitesimal)"
   818 by (simp add: mem_cinfmal_iff mem_infmal_iff hcomplex_zero_num hypreal_zero_num capprox_approx_iff)
   819 
   820 lemma eq_Abs_hcomplex_EX:
   821      "(\<exists>t. P t) = (\<exists>X. P (Abs_hcomplex(hcomplexrel `` {X})))"
   822 apply auto
   823 apply (rule_tac z = t in eq_Abs_hcomplex, auto)
   824 done
   825 
   826 lemma eq_Abs_hcomplex_Bex:
   827      "(\<exists>t \<in> A. P t) = (\<exists>X. (Abs_hcomplex(hcomplexrel `` {X})) \<in> A &  
   828                          P (Abs_hcomplex(hcomplexrel `` {X})))"
   829 apply auto
   830 apply (rule_tac z = t in eq_Abs_hcomplex, auto)
   831 done
   832 
   833 (* Here we go - easy proof now!! *)
   834 lemma stc_part_Ex: "x:CFinite ==> \<exists>t \<in> SComplex. x @c= t"
   835 apply (rule_tac z = x in eq_Abs_hcomplex)
   836 apply (auto simp add: CFinite_HFinite_iff eq_Abs_hcomplex_Bex SComplex_SReal_iff capprox_approx_iff)
   837 apply (drule st_part_Ex, safe)+
   838 apply (rule_tac z = t in eq_Abs_hypreal)
   839 apply (rule_tac z = ta in eq_Abs_hypreal, auto)
   840 apply (rule_tac x = "%n. Complex (xa n) (xb n) " in exI)
   841 apply auto
   842 done
   843 
   844 lemma stc_part_Ex1: "x:CFinite ==> EX! t. t \<in> SComplex &  x @c= t"
   845 apply (drule stc_part_Ex, safe)
   846 apply (drule_tac [2] capprox_sym, drule_tac [2] capprox_sym, drule_tac [2] capprox_sym)
   847 apply (auto intro!: capprox_unique_complex)
   848 done
   849 
   850 lemma CFinite_Int_CInfinite_empty: "CFinite Int CInfinite = {}"
   851 by (simp add: CFinite_def CInfinite_def, auto)
   852 
   853 lemma CFinite_not_CInfinite: "x \<in> CFinite ==> x \<notin> CInfinite"
   854 by (insert CFinite_Int_CInfinite_empty, blast)
   855 
   856 text{*Not sure this is a good idea!*}
   857 declare CFinite_Int_CInfinite_empty [simp]
   858 
   859 lemma not_CFinite_CInfinite: "x\<notin> CFinite ==> x \<in> CInfinite"
   860 by (auto intro: not_HFinite_HInfinite simp add: CFinite_hcmod_iff CInfinite_hcmod_iff)
   861 
   862 lemma CInfinite_CFinite_disj: "x \<in> CInfinite | x \<in> CFinite"
   863 by (blast intro: not_CFinite_CInfinite)
   864 
   865 lemma CInfinite_CFinite_iff: "(x \<in> CInfinite) = (x \<notin> CFinite)"
   866 by (blast dest: CFinite_not_CInfinite not_CFinite_CInfinite)
   867 
   868 lemma CFinite_CInfinite_iff: "(x \<in> CFinite) = (x \<notin> CInfinite)"
   869 by (simp add: CInfinite_CFinite_iff)
   870 
   871 lemma CInfinite_diff_CFinite_CInfinitesimal_disj:
   872      "x \<notin> CInfinitesimal ==> x \<in> CInfinite | x \<in> CFinite - CInfinitesimal"
   873 by (fast intro: not_CFinite_CInfinite)
   874 
   875 lemma CFinite_inverse:
   876      "[| x \<in> CFinite; x \<notin> CInfinitesimal |] ==> inverse x \<in> CFinite"
   877 apply (cut_tac x = "inverse x" in CInfinite_CFinite_disj)
   878 apply (auto dest!: CInfinite_inverse_CInfinitesimal)
   879 done
   880 
   881 lemma CFinite_inverse2: "x \<in> CFinite - CInfinitesimal ==> inverse x \<in> CFinite"
   882 by (blast intro: CFinite_inverse)
   883 
   884 lemma CInfinitesimal_inverse_CFinite:
   885      "x \<notin> CInfinitesimal ==> inverse(x) \<in> CFinite"
   886 apply (drule CInfinite_diff_CFinite_CInfinitesimal_disj)
   887 apply (blast intro: CFinite_inverse CInfinite_inverse_CInfinitesimal CInfinitesimal_subset_CFinite [THEN subsetD])
   888 done
   889 
   890 
   891 lemma CFinite_not_CInfinitesimal_inverse:
   892      "x \<in> CFinite - CInfinitesimal ==> inverse x \<in> CFinite - CInfinitesimal"
   893 apply (auto intro: CInfinitesimal_inverse_CFinite)
   894 apply (drule CInfinitesimal_CFinite_mult2, assumption)
   895 apply (simp add: not_CInfinitesimal_not_zero)
   896 done
   897 
   898 lemma capprox_inverse:
   899      "[| x @c= y; y \<in>  CFinite - CInfinitesimal |] ==> inverse x @c= inverse y"
   900 apply (frule CFinite_diff_CInfinitesimal_capprox, assumption)
   901 apply (frule not_CInfinitesimal_not_zero2)
   902 apply (frule_tac x = x in not_CInfinitesimal_not_zero2)
   903 apply (drule CFinite_inverse2)+
   904 apply (drule capprox_mult2, assumption, auto)
   905 apply (drule_tac c = "inverse x" in capprox_mult1, assumption)
   906 apply (auto intro: capprox_sym simp add: mult_assoc)
   907 done
   908 
   909 lemmas hcomplex_of_complex_capprox_inverse =
   910   hcomplex_of_complex_CFinite_diff_CInfinitesimal [THEN [2] capprox_inverse]
   911 
   912 lemma inverse_add_CInfinitesimal_capprox:
   913      "[| x \<in> CFinite - CInfinitesimal;  
   914          h \<in> CInfinitesimal |] ==> inverse(x + h) @c= inverse x"
   915 by (auto intro: capprox_inverse capprox_sym CInfinitesimal_add_capprox_self)
   916 
   917 lemma inverse_add_CInfinitesimal_capprox2:
   918      "[| x \<in> CFinite - CInfinitesimal;  
   919          h \<in> CInfinitesimal |] ==> inverse(h + x) @c= inverse x"
   920 apply (rule add_commute [THEN subst])
   921 apply (blast intro: inverse_add_CInfinitesimal_capprox)
   922 done
   923 
   924 lemma inverse_add_CInfinitesimal_approx_CInfinitesimal:
   925      "[| x \<in> CFinite - CInfinitesimal;  
   926          h \<in> CInfinitesimal |] ==> inverse(x + h) - inverse x @c= h"
   927 apply (rule capprox_trans2)
   928 apply (auto intro: inverse_add_CInfinitesimal_capprox 
   929        simp add: mem_cinfmal_iff diff_minus capprox_minus_iff [symmetric])
   930 done
   931 
   932 lemma CInfinitesimal_square_iff [iff]:
   933      "(x*x \<in> CInfinitesimal) = (x \<in> CInfinitesimal)"
   934 by (simp add: CInfinitesimal_hcmod_iff hcmod_mult)
   935 
   936 lemma capprox_CFinite_mult_cancel:
   937      "[| a \<in> CFinite-CInfinitesimal; a*w @c= a*z |] ==> w @c= z"
   938 apply safe
   939 apply (frule CFinite_inverse, assumption)
   940 apply (drule not_CInfinitesimal_not_zero)
   941 apply (auto dest: capprox_mult2 simp add: mult_assoc [symmetric])
   942 done
   943 
   944 lemma capprox_CFinite_mult_cancel_iff1:
   945      "a \<in> CFinite-CInfinitesimal ==> (a * w @c= a * z) = (w @c= z)"
   946 by (auto intro: capprox_mult2 capprox_CFinite_mult_cancel)
   947 
   948 
   949 subsection{*Theorems About Monads*}
   950 
   951 lemma capprox_cmonad_iff: "(x @c= y) = (cmonad(x)=cmonad(y))"
   952 apply (simp add: cmonad_def)
   953 apply (auto dest: capprox_sym elim!: capprox_trans equalityCE)
   954 done
   955 
   956 lemma CInfinitesimal_cmonad_eq:
   957      "e \<in> CInfinitesimal ==> cmonad (x+e) = cmonad x"
   958 by (fast intro!: CInfinitesimal_add_capprox_self [THEN capprox_sym] capprox_cmonad_iff [THEN iffD1])
   959 
   960 lemma mem_cmonad_iff: "(u \<in> cmonad x) = (-u \<in> cmonad (-x))"
   961 by (simp add: cmonad_def)
   962 
   963 lemma CInfinitesimal_cmonad_zero_iff: "(x:CInfinitesimal) = (x \<in> cmonad 0)"
   964 by (auto intro: capprox_sym simp add: mem_cinfmal_iff cmonad_def)
   965 
   966 lemma cmonad_zero_minus_iff: "(x \<in> cmonad 0) = (-x \<in> cmonad 0)"
   967 by (simp add: CInfinitesimal_cmonad_zero_iff [symmetric])
   968 
   969 lemma cmonad_zero_hcmod_iff: "(x \<in> cmonad 0) = (hcmod x:monad 0)"
   970 by (simp add: CInfinitesimal_cmonad_zero_iff [symmetric] CInfinitesimal_hcmod_iff Infinitesimal_monad_zero_iff [symmetric])
   971 
   972 lemma mem_cmonad_self [simp]: "x \<in> cmonad x"
   973 by (simp add: cmonad_def)
   974 
   975 
   976 subsection{*Theorems About Standard Part*}
   977 
   978 lemma stc_capprox_self: "x \<in> CFinite ==> stc x @c= x"
   979 apply (simp add: stc_def)
   980 apply (frule stc_part_Ex, safe)
   981 apply (rule someI2)
   982 apply (auto intro: capprox_sym)
   983 done
   984 
   985 lemma stc_SComplex: "x \<in> CFinite ==> stc x \<in> SComplex"
   986 apply (simp add: stc_def)
   987 apply (frule stc_part_Ex, safe)
   988 apply (rule someI2)
   989 apply (auto intro: capprox_sym)
   990 done
   991 
   992 lemma stc_CFinite: "x \<in> CFinite ==> stc x \<in> CFinite"
   993 by (erule stc_SComplex [THEN SComplex_subset_CFinite [THEN subsetD]])
   994 
   995 lemma stc_SComplex_eq [simp]: "x \<in> SComplex ==> stc x = x"
   996 apply (simp add: stc_def)
   997 apply (rule some_equality)
   998 apply (auto intro: SComplex_subset_CFinite [THEN subsetD])
   999 apply (blast dest: SComplex_capprox_iff [THEN iffD1])
  1000 done
  1001 
  1002 lemma stc_hcomplex_of_complex:
  1003      "stc (hcomplex_of_complex x) = hcomplex_of_complex x"
  1004 by auto
  1005 
  1006 lemma stc_eq_capprox:
  1007      "[| x \<in> CFinite; y \<in> CFinite; stc x = stc y |] ==> x @c= y"
  1008 by (auto dest!: stc_capprox_self elim!: capprox_trans3)
  1009 
  1010 lemma capprox_stc_eq:
  1011      "[| x \<in> CFinite; y \<in> CFinite; x @c= y |] ==> stc x = stc y"
  1012 by (blast intro: capprox_trans capprox_trans2 SComplex_capprox_iff [THEN iffD1]
  1013           dest: stc_capprox_self stc_SComplex)
  1014 
  1015 lemma stc_eq_capprox_iff:
  1016      "[| x \<in> CFinite; y \<in> CFinite|] ==> (x @c= y) = (stc x = stc y)"
  1017 by (blast intro: capprox_stc_eq stc_eq_capprox)
  1018 
  1019 lemma stc_CInfinitesimal_add_SComplex:
  1020      "[| x \<in> SComplex; e \<in> CInfinitesimal |] ==> stc(x + e) = x"
  1021 apply (frule stc_SComplex_eq [THEN subst])
  1022 prefer 2 apply assumption
  1023 apply (frule SComplex_subset_CFinite [THEN subsetD])
  1024 apply (frule CInfinitesimal_subset_CFinite [THEN subsetD])
  1025 apply (drule stc_SComplex_eq)
  1026 apply (rule capprox_stc_eq)
  1027 apply (auto intro: CFinite_add simp add: CInfinitesimal_add_capprox_self [THEN capprox_sym])
  1028 done
  1029 
  1030 lemma stc_CInfinitesimal_add_SComplex2:
  1031      "[| x \<in> SComplex; e \<in> CInfinitesimal |] ==> stc(e + x) = x"
  1032 apply (rule add_commute [THEN subst])
  1033 apply (blast intro!: stc_CInfinitesimal_add_SComplex)
  1034 done
  1035 
  1036 lemma CFinite_stc_CInfinitesimal_add:
  1037      "x \<in> CFinite ==> \<exists>e \<in> CInfinitesimal. x = stc(x) + e"
  1038 by (blast dest!: stc_capprox_self [THEN capprox_sym] bex_CInfinitesimal_iff2 [THEN iffD2])
  1039 
  1040 lemma stc_add:
  1041      "[| x \<in> CFinite; y \<in> CFinite |] ==> stc (x + y) = stc(x) + stc(y)"
  1042 apply (frule CFinite_stc_CInfinitesimal_add)
  1043 apply (frule_tac x = y in CFinite_stc_CInfinitesimal_add, safe)
  1044 apply (subgoal_tac "stc (x + y) = stc ((stc x + e) + (stc y + ea))")
  1045 apply (drule_tac [2] sym, drule_tac [2] sym)
  1046  prefer 2 apply simp 
  1047 apply (simp (no_asm_simp) add: add_ac)
  1048 apply (drule stc_SComplex)+
  1049 apply (drule SComplex_add, assumption)
  1050 apply (drule CInfinitesimal_add, assumption)
  1051 apply (rule add_assoc [THEN subst])
  1052 apply (blast intro!: stc_CInfinitesimal_add_SComplex2)
  1053 done
  1054 
  1055 lemma stc_number_of [simp]: "stc (number_of w) = number_of w"
  1056 by (rule SComplex_number_of [THEN stc_SComplex_eq])
  1057 
  1058 lemma stc_zero [simp]: "stc 0 = 0"
  1059 by simp
  1060 
  1061 lemma stc_one [simp]: "stc 1 = 1"
  1062 by simp
  1063 
  1064 lemma stc_minus: "y \<in> CFinite ==> stc(-y) = -stc(y)"
  1065 apply (frule CFinite_minus_iff [THEN iffD2])
  1066 apply (rule hcomplex_add_minus_eq_minus)
  1067 apply (drule stc_add [symmetric], assumption)
  1068 apply (simp add: add_commute)
  1069 done
  1070 
  1071 lemma stc_diff: 
  1072      "[| x \<in> CFinite; y \<in> CFinite |] ==> stc (x-y) = stc(x) - stc(y)"
  1073 apply (simp add: diff_minus)
  1074 apply (frule_tac y1 = y in stc_minus [symmetric])
  1075 apply (drule_tac x1 = y in CFinite_minus_iff [THEN iffD2])
  1076 apply (auto intro: stc_add)
  1077 done
  1078 
  1079 lemma lemma_stc_mult:
  1080      "[| x \<in> CFinite; y \<in> CFinite;  
  1081          e \<in> CInfinitesimal;        
  1082          ea: CInfinitesimal |]    
  1083        ==> e*y + x*ea + e*ea: CInfinitesimal"
  1084 apply (frule_tac x = e and y = y in CInfinitesimal_CFinite_mult)
  1085 apply (frule_tac [2] x = ea and y = x in CInfinitesimal_CFinite_mult)
  1086 apply (drule_tac [3] CInfinitesimal_mult)
  1087 apply (auto intro: CInfinitesimal_add simp add: add_ac mult_ac)
  1088 done
  1089 
  1090 lemma stc_mult:
  1091      "[| x \<in> CFinite; y \<in> CFinite |]  
  1092                ==> stc (x * y) = stc(x) * stc(y)"
  1093 apply (frule CFinite_stc_CInfinitesimal_add)
  1094 apply (frule_tac x = y in CFinite_stc_CInfinitesimal_add, safe)
  1095 apply (subgoal_tac "stc (x * y) = stc ((stc x + e) * (stc y + ea))")
  1096 apply (drule_tac [2] sym, drule_tac [2] sym)
  1097  prefer 2 apply simp 
  1098 apply (erule_tac V = "x = stc x + e" in thin_rl)
  1099 apply (erule_tac V = "y = stc y + ea" in thin_rl)
  1100 apply (simp add: hcomplex_add_mult_distrib right_distrib)
  1101 apply (drule stc_SComplex)+
  1102 apply (simp (no_asm_use) add: add_assoc)
  1103 apply (rule stc_CInfinitesimal_add_SComplex)
  1104 apply (blast intro!: SComplex_mult)
  1105 apply (drule SComplex_subset_CFinite [THEN subsetD])+
  1106 apply (rule add_assoc [THEN subst])
  1107 apply (blast intro!: lemma_stc_mult)
  1108 done
  1109 
  1110 lemma stc_CInfinitesimal: "x \<in> CInfinitesimal ==> stc x = 0"
  1111 apply (rule stc_zero [THEN subst])
  1112 apply (rule capprox_stc_eq)
  1113 apply (auto intro: CInfinitesimal_subset_CFinite [THEN subsetD]
  1114                  simp add: mem_cinfmal_iff [symmetric])
  1115 done
  1116 
  1117 lemma stc_not_CInfinitesimal: "stc(x) \<noteq> 0 ==> x \<notin> CInfinitesimal"
  1118 by (fast intro: stc_CInfinitesimal)
  1119 
  1120 lemma stc_inverse:
  1121      "[| x \<in> CFinite; stc x \<noteq> 0 |]  
  1122       ==> stc(inverse x) = inverse (stc x)"
  1123 apply (rule_tac c1 = "stc x" in hcomplex_mult_left_cancel [THEN iffD1])
  1124 apply (auto simp add: stc_mult [symmetric] stc_not_CInfinitesimal CFinite_inverse)
  1125 apply (subst right_inverse, auto)
  1126 done
  1127 
  1128 lemma stc_divide [simp]:
  1129      "[| x \<in> CFinite; y \<in> CFinite; stc y \<noteq> 0 |]  
  1130       ==> stc(x/y) = (stc x) / (stc y)"
  1131 by (simp add: divide_inverse stc_mult stc_not_CInfinitesimal CFinite_inverse stc_inverse)
  1132 
  1133 lemma stc_idempotent [simp]: "x \<in> CFinite ==> stc(stc(x)) = stc(x)"
  1134 by (blast intro: stc_CFinite stc_capprox_self capprox_stc_eq)
  1135 
  1136 lemma CFinite_HFinite_hcomplex_of_hypreal:
  1137      "z \<in> HFinite ==> hcomplex_of_hypreal z \<in> CFinite"
  1138 apply (cases z)
  1139 apply (simp add: hcomplex_of_hypreal CFinite_HFinite_iff hypreal_zero_def [symmetric])
  1140 done
  1141 
  1142 lemma SComplex_SReal_hcomplex_of_hypreal:
  1143      "x \<in> Reals ==>  hcomplex_of_hypreal x \<in> SComplex"
  1144 apply (cases x)
  1145 apply (simp add: hcomplex_of_hypreal SComplex_SReal_iff hypreal_zero_def [symmetric])
  1146 done
  1147 
  1148 lemma stc_hcomplex_of_hypreal: 
  1149  "z \<in> HFinite ==> stc(hcomplex_of_hypreal z) = hcomplex_of_hypreal (st z)"
  1150 apply (simp add: st_def stc_def)
  1151 apply (frule st_part_Ex, safe)
  1152 apply (rule someI2)
  1153 apply (auto intro: approx_sym)
  1154 apply (drule CFinite_HFinite_hcomplex_of_hypreal)
  1155 apply (frule stc_part_Ex, safe)
  1156 apply (rule someI2)
  1157 apply (auto intro: capprox_sym intro!: capprox_unique_complex dest: SComplex_SReal_hcomplex_of_hypreal)
  1158 done
  1159 
  1160 (*
  1161 Goal "x \<in> CFinite ==> hcmod(stc x) = st(hcmod x)"
  1162 by (dtac stc_capprox_self 1)
  1163 by (auto_tac (claset(),simpset() addsimps [bex_CInfinitesimal_iff2 RS sym]));
  1164 
  1165 
  1166 approx_hcmod_add_hcmod
  1167 *)
  1168 
  1169 lemma CInfinitesimal_hcnj_iff [simp]:
  1170      "(hcnj z \<in> CInfinitesimal) = (z \<in> CInfinitesimal)"
  1171 by (simp add: CInfinitesimal_hcmod_iff)
  1172 
  1173 lemma CInfinite_HInfinite_iff:
  1174      "(Abs_hcomplex(hcomplexrel ``{%n. X n}) \<in> CInfinite) =  
  1175       (Abs_hypreal(hyprel `` {%n. Re(X n)}) \<in> HInfinite |  
  1176        Abs_hypreal(hyprel `` {%n. Im(X n)}) \<in> HInfinite)"
  1177 by (simp add: CInfinite_CFinite_iff HInfinite_HFinite_iff CFinite_HFinite_iff)
  1178 
  1179 text{*These theorems should probably be deleted*}
  1180 lemma hcomplex_split_CInfinitesimal_iff:
  1181      "(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y \<in> CInfinitesimal) =  
  1182       (x \<in> Infinitesimal & y \<in> Infinitesimal)"
  1183 apply (cases x, cases y)
  1184 apply (simp add: iii_def hcomplex_add hcomplex_mult hcomplex_of_hypreal CInfinitesimal_Infinitesimal_iff)
  1185 done
  1186 
  1187 lemma hcomplex_split_CFinite_iff:
  1188      "(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y \<in> CFinite) =  
  1189       (x \<in> HFinite & y \<in> HFinite)"
  1190 apply (cases x, cases y)
  1191 apply (simp add: iii_def hcomplex_add hcomplex_mult hcomplex_of_hypreal CFinite_HFinite_iff)
  1192 done
  1193 
  1194 lemma hcomplex_split_SComplex_iff:
  1195      "(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y \<in> SComplex) =  
  1196       (x \<in> Reals & y \<in> Reals)"
  1197 apply (cases x, cases y)
  1198 apply (simp add: iii_def hcomplex_add hcomplex_mult hcomplex_of_hypreal SComplex_SReal_iff)
  1199 done
  1200 
  1201 lemma hcomplex_split_CInfinite_iff:
  1202      "(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y \<in> CInfinite) =  
  1203       (x \<in> HInfinite | y \<in> HInfinite)"
  1204 apply (cases x, cases y)
  1205 apply (simp add: iii_def hcomplex_add hcomplex_mult hcomplex_of_hypreal CInfinite_HInfinite_iff)
  1206 done
  1207 
  1208 lemma hcomplex_split_capprox_iff:
  1209      "(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y @c=  
  1210        hcomplex_of_hypreal x' + iii * hcomplex_of_hypreal y') =  
  1211       (x @= x' & y @= y')"
  1212 apply (cases x, cases y, cases x', cases y')
  1213 apply (simp add: iii_def hcomplex_add hcomplex_mult hcomplex_of_hypreal capprox_approx_iff)
  1214 done
  1215 
  1216 lemma complex_seq_to_hcomplex_CInfinitesimal:
  1217      "\<forall>n. cmod (X n - x) < inverse (real (Suc n)) ==>  
  1218       Abs_hcomplex(hcomplexrel``{X}) - hcomplex_of_complex x \<in> CInfinitesimal"
  1219 apply (simp add: hcomplex_diff CInfinitesimal_hcmod_iff hcomplex_of_complex_def Infinitesimal_FreeUltrafilterNat_iff hcmod)
  1220 apply (rule bexI, auto)
  1221 apply (auto dest: FreeUltrafilterNat_inverse_real_of_posnat FreeUltrafilterNat_all FreeUltrafilterNat_Int intro: order_less_trans FreeUltrafilterNat_subset)
  1222 done
  1223 
  1224 lemma CInfinitesimal_hcomplex_of_hypreal_epsilon [simp]:
  1225      "hcomplex_of_hypreal epsilon \<in> CInfinitesimal"
  1226 by (simp add: CInfinitesimal_hcmod_iff)
  1227 
  1228 lemma hcomplex_of_complex_approx_zero_iff [simp]:
  1229      "(hcomplex_of_complex z @c= 0) = (z = 0)"
  1230 by (simp add: hcomplex_of_complex_zero [symmetric]
  1231          del: hcomplex_of_complex_zero)
  1232 
  1233 lemma hcomplex_of_complex_approx_zero_iff2 [simp]:
  1234      "(0 @c= hcomplex_of_complex z) = (z = 0)"
  1235 by (simp add: hcomplex_of_complex_zero [symmetric]
  1236          del: hcomplex_of_complex_zero)
  1237 
  1238 
  1239 ML
  1240 {*
  1241 val SComplex_add = thm "SComplex_add";
  1242 val SComplex_mult = thm "SComplex_mult";
  1243 val SComplex_inverse = thm "SComplex_inverse";
  1244 val SComplex_divide = thm "SComplex_divide";
  1245 val SComplex_minus = thm "SComplex_minus";
  1246 val SComplex_minus_iff = thm "SComplex_minus_iff";
  1247 val SComplex_diff = thm "SComplex_diff";
  1248 val SComplex_add_cancel = thm "SComplex_add_cancel";
  1249 val SReal_hcmod_hcomplex_of_complex = thm "SReal_hcmod_hcomplex_of_complex";
  1250 val SReal_hcmod_number_of = thm "SReal_hcmod_number_of";
  1251 val SReal_hcmod_SComplex = thm "SReal_hcmod_SComplex";
  1252 val SComplex_hcomplex_of_complex = thm "SComplex_hcomplex_of_complex";
  1253 val SComplex_number_of = thm "SComplex_number_of";
  1254 val SComplex_divide_number_of = thm "SComplex_divide_number_of";
  1255 val SComplex_UNIV_complex = thm "SComplex_UNIV_complex";
  1256 val SComplex_iff = thm "SComplex_iff";
  1257 val hcomplex_of_complex_image = thm "hcomplex_of_complex_image";
  1258 val inv_hcomplex_of_complex_image = thm "inv_hcomplex_of_complex_image";
  1259 val SComplex_hcomplex_of_complex_image = thm "SComplex_hcomplex_of_complex_image";
  1260 val SComplex_SReal_dense = thm "SComplex_SReal_dense";
  1261 val SComplex_hcmod_SReal = thm "SComplex_hcmod_SReal";
  1262 val SComplex_zero = thm "SComplex_zero";
  1263 val SComplex_one = thm "SComplex_one";
  1264 val CFinite_add = thm "CFinite_add";
  1265 val CFinite_mult = thm "CFinite_mult";
  1266 val CFinite_minus_iff = thm "CFinite_minus_iff";
  1267 val SComplex_subset_CFinite = thm "SComplex_subset_CFinite";
  1268 val HFinite_hcmod_hcomplex_of_complex = thm "HFinite_hcmod_hcomplex_of_complex";
  1269 val CFinite_hcomplex_of_complex = thm "CFinite_hcomplex_of_complex";
  1270 val CFiniteD = thm "CFiniteD";
  1271 val CFinite_hcmod_iff = thm "CFinite_hcmod_iff";
  1272 val CFinite_number_of = thm "CFinite_number_of";
  1273 val CFinite_bounded = thm "CFinite_bounded";
  1274 val CInfinitesimal_zero = thm "CInfinitesimal_zero";
  1275 val hcomplex_sum_of_halves = thm "hcomplex_sum_of_halves";
  1276 val CInfinitesimal_hcmod_iff = thm "CInfinitesimal_hcmod_iff";
  1277 val one_not_CInfinitesimal = thm "one_not_CInfinitesimal";
  1278 val CInfinitesimal_add = thm "CInfinitesimal_add";
  1279 val CInfinitesimal_minus_iff = thm "CInfinitesimal_minus_iff";
  1280 val CInfinitesimal_diff = thm "CInfinitesimal_diff";
  1281 val CInfinitesimal_mult = thm "CInfinitesimal_mult";
  1282 val CInfinitesimal_CFinite_mult = thm "CInfinitesimal_CFinite_mult";
  1283 val CInfinitesimal_CFinite_mult2 = thm "CInfinitesimal_CFinite_mult2";
  1284 val CInfinite_hcmod_iff = thm "CInfinite_hcmod_iff";
  1285 val CInfinite_inverse_CInfinitesimal = thm "CInfinite_inverse_CInfinitesimal";
  1286 val CInfinite_mult = thm "CInfinite_mult";
  1287 val CInfinite_minus_iff = thm "CInfinite_minus_iff";
  1288 val CFinite_sum_squares = thm "CFinite_sum_squares";
  1289 val not_CInfinitesimal_not_zero = thm "not_CInfinitesimal_not_zero";
  1290 val not_CInfinitesimal_not_zero2 = thm "not_CInfinitesimal_not_zero2";
  1291 val CFinite_diff_CInfinitesimal_hcmod = thm "CFinite_diff_CInfinitesimal_hcmod";
  1292 val hcmod_less_CInfinitesimal = thm "hcmod_less_CInfinitesimal";
  1293 val hcmod_le_CInfinitesimal = thm "hcmod_le_CInfinitesimal";
  1294 val CInfinitesimal_interval = thm "CInfinitesimal_interval";
  1295 val CInfinitesimal_interval2 = thm "CInfinitesimal_interval2";
  1296 val not_CInfinitesimal_mult = thm "not_CInfinitesimal_mult";
  1297 val CInfinitesimal_mult_disj = thm "CInfinitesimal_mult_disj";
  1298 val CFinite_CInfinitesimal_diff_mult = thm "CFinite_CInfinitesimal_diff_mult";
  1299 val CInfinitesimal_subset_CFinite = thm "CInfinitesimal_subset_CFinite";
  1300 val CInfinitesimal_hcomplex_of_complex_mult = thm "CInfinitesimal_hcomplex_of_complex_mult";
  1301 val CInfinitesimal_hcomplex_of_complex_mult2 = thm "CInfinitesimal_hcomplex_of_complex_mult2";
  1302 val mem_cinfmal_iff = thm "mem_cinfmal_iff";
  1303 val capprox_minus_iff = thm "capprox_minus_iff";
  1304 val capprox_minus_iff2 = thm "capprox_minus_iff2";
  1305 val capprox_refl = thm "capprox_refl";
  1306 val capprox_sym = thm "capprox_sym";
  1307 val capprox_trans = thm "capprox_trans";
  1308 val capprox_trans2 = thm "capprox_trans2";
  1309 val capprox_trans3 = thm "capprox_trans3";
  1310 val number_of_capprox_reorient = thm "number_of_capprox_reorient";
  1311 val CInfinitesimal_capprox_minus = thm "CInfinitesimal_capprox_minus";
  1312 val capprox_monad_iff = thm "capprox_monad_iff";
  1313 val Infinitesimal_capprox = thm "Infinitesimal_capprox";
  1314 val capprox_add = thm "capprox_add";
  1315 val capprox_minus = thm "capprox_minus";
  1316 val capprox_minus2 = thm "capprox_minus2";
  1317 val capprox_minus_cancel = thm "capprox_minus_cancel";
  1318 val capprox_add_minus = thm "capprox_add_minus";
  1319 val capprox_mult1 = thm "capprox_mult1";
  1320 val capprox_mult2 = thm "capprox_mult2";
  1321 val capprox_mult_subst = thm "capprox_mult_subst";
  1322 val capprox_mult_subst2 = thm "capprox_mult_subst2";
  1323 val capprox_mult_subst_SComplex = thm "capprox_mult_subst_SComplex";
  1324 val capprox_eq_imp = thm "capprox_eq_imp";
  1325 val CInfinitesimal_minus_capprox = thm "CInfinitesimal_minus_capprox";
  1326 val bex_CInfinitesimal_iff = thm "bex_CInfinitesimal_iff";
  1327 val bex_CInfinitesimal_iff2 = thm "bex_CInfinitesimal_iff2";
  1328 val CInfinitesimal_add_capprox = thm "CInfinitesimal_add_capprox";
  1329 val CInfinitesimal_add_capprox_self = thm "CInfinitesimal_add_capprox_self";
  1330 val CInfinitesimal_add_capprox_self2 = thm "CInfinitesimal_add_capprox_self2";
  1331 val CInfinitesimal_add_minus_capprox_self = thm "CInfinitesimal_add_minus_capprox_self";
  1332 val CInfinitesimal_add_cancel = thm "CInfinitesimal_add_cancel";
  1333 val CInfinitesimal_add_right_cancel = thm "CInfinitesimal_add_right_cancel";
  1334 val capprox_add_left_cancel = thm "capprox_add_left_cancel";
  1335 val capprox_add_right_cancel = thm "capprox_add_right_cancel";
  1336 val capprox_add_mono1 = thm "capprox_add_mono1";
  1337 val capprox_add_mono2 = thm "capprox_add_mono2";
  1338 val capprox_add_left_iff = thm "capprox_add_left_iff";
  1339 val capprox_add_right_iff = thm "capprox_add_right_iff";
  1340 val capprox_CFinite = thm "capprox_CFinite";
  1341 val capprox_hcomplex_of_complex_CFinite = thm "capprox_hcomplex_of_complex_CFinite";
  1342 val capprox_mult_CFinite = thm "capprox_mult_CFinite";
  1343 val capprox_mult_hcomplex_of_complex = thm "capprox_mult_hcomplex_of_complex";
  1344 val capprox_SComplex_mult_cancel_zero = thm "capprox_SComplex_mult_cancel_zero";
  1345 val capprox_mult_SComplex1 = thm "capprox_mult_SComplex1";
  1346 val capprox_mult_SComplex2 = thm "capprox_mult_SComplex2";
  1347 val capprox_mult_SComplex_zero_cancel_iff = thm "capprox_mult_SComplex_zero_cancel_iff";
  1348 val capprox_SComplex_mult_cancel = thm "capprox_SComplex_mult_cancel";
  1349 val capprox_SComplex_mult_cancel_iff1 = thm "capprox_SComplex_mult_cancel_iff1";
  1350 val capprox_hcmod_approx_zero = thm "capprox_hcmod_approx_zero";
  1351 val capprox_approx_zero_iff = thm "capprox_approx_zero_iff";
  1352 val capprox_minus_zero_cancel_iff = thm "capprox_minus_zero_cancel_iff";
  1353 val Infinitesimal_hcmod_add_diff = thm "Infinitesimal_hcmod_add_diff";
  1354 val approx_hcmod_add_hcmod = thm "approx_hcmod_add_hcmod";
  1355 val capprox_hcmod_approx = thm "capprox_hcmod_approx";
  1356 val CInfinitesimal_less_SComplex = thm "CInfinitesimal_less_SComplex";
  1357 val SComplex_Int_CInfinitesimal_zero = thm "SComplex_Int_CInfinitesimal_zero";
  1358 val SComplex_CInfinitesimal_zero = thm "SComplex_CInfinitesimal_zero";
  1359 val SComplex_CFinite_diff_CInfinitesimal = thm "SComplex_CFinite_diff_CInfinitesimal";
  1360 val hcomplex_of_complex_CFinite_diff_CInfinitesimal = thm "hcomplex_of_complex_CFinite_diff_CInfinitesimal";
  1361 val hcomplex_of_complex_CInfinitesimal_iff_0 = thm "hcomplex_of_complex_CInfinitesimal_iff_0";
  1362 val number_of_not_CInfinitesimal = thm "number_of_not_CInfinitesimal";
  1363 val capprox_SComplex_not_zero = thm "capprox_SComplex_not_zero";
  1364 val CFinite_diff_CInfinitesimal_capprox = thm "CFinite_diff_CInfinitesimal_capprox";
  1365 val CInfinitesimal_ratio = thm "CInfinitesimal_ratio";
  1366 val SComplex_capprox_iff = thm "SComplex_capprox_iff";
  1367 val number_of_capprox_iff = thm "number_of_capprox_iff";
  1368 val number_of_CInfinitesimal_iff = thm "number_of_CInfinitesimal_iff";
  1369 val hcomplex_of_complex_approx_iff = thm "hcomplex_of_complex_approx_iff";
  1370 val hcomplex_of_complex_capprox_number_of_iff = thm "hcomplex_of_complex_capprox_number_of_iff";
  1371 val capprox_unique_complex = thm "capprox_unique_complex";
  1372 val hcomplex_capproxD1 = thm "hcomplex_capproxD1";
  1373 val hcomplex_capproxD2 = thm "hcomplex_capproxD2";
  1374 val hcomplex_capproxI = thm "hcomplex_capproxI";
  1375 val capprox_approx_iff = thm "capprox_approx_iff";
  1376 val hcomplex_of_hypreal_capprox_iff = thm "hcomplex_of_hypreal_capprox_iff";
  1377 val CFinite_HFinite_Re = thm "CFinite_HFinite_Re";
  1378 val CFinite_HFinite_Im = thm "CFinite_HFinite_Im";
  1379 val HFinite_Re_Im_CFinite = thm "HFinite_Re_Im_CFinite";
  1380 val CFinite_HFinite_iff = thm "CFinite_HFinite_iff";
  1381 val SComplex_Re_SReal = thm "SComplex_Re_SReal";
  1382 val SComplex_Im_SReal = thm "SComplex_Im_SReal";
  1383 val Reals_Re_Im_SComplex = thm "Reals_Re_Im_SComplex";
  1384 val SComplex_SReal_iff = thm "SComplex_SReal_iff";
  1385 val CInfinitesimal_Infinitesimal_iff = thm "CInfinitesimal_Infinitesimal_iff";
  1386 val eq_Abs_hcomplex_Bex = thm "eq_Abs_hcomplex_Bex";
  1387 val stc_part_Ex = thm "stc_part_Ex";
  1388 val stc_part_Ex1 = thm "stc_part_Ex1";
  1389 val CFinite_Int_CInfinite_empty = thm "CFinite_Int_CInfinite_empty";
  1390 val CFinite_not_CInfinite = thm "CFinite_not_CInfinite";
  1391 val not_CFinite_CInfinite = thm "not_CFinite_CInfinite";
  1392 val CInfinite_CFinite_disj = thm "CInfinite_CFinite_disj";
  1393 val CInfinite_CFinite_iff = thm "CInfinite_CFinite_iff";
  1394 val CFinite_CInfinite_iff = thm "CFinite_CInfinite_iff";
  1395 val CInfinite_diff_CFinite_CInfinitesimal_disj = thm "CInfinite_diff_CFinite_CInfinitesimal_disj";
  1396 val CFinite_inverse = thm "CFinite_inverse";
  1397 val CFinite_inverse2 = thm "CFinite_inverse2";
  1398 val CInfinitesimal_inverse_CFinite = thm "CInfinitesimal_inverse_CFinite";
  1399 val CFinite_not_CInfinitesimal_inverse = thm "CFinite_not_CInfinitesimal_inverse";
  1400 val capprox_inverse = thm "capprox_inverse";
  1401 val hcomplex_of_complex_capprox_inverse = thms "hcomplex_of_complex_capprox_inverse";
  1402 val inverse_add_CInfinitesimal_capprox = thm "inverse_add_CInfinitesimal_capprox";
  1403 val inverse_add_CInfinitesimal_capprox2 = thm "inverse_add_CInfinitesimal_capprox2";
  1404 val inverse_add_CInfinitesimal_approx_CInfinitesimal = thm "inverse_add_CInfinitesimal_approx_CInfinitesimal";
  1405 val CInfinitesimal_square_iff = thm "CInfinitesimal_square_iff";
  1406 val capprox_CFinite_mult_cancel = thm "capprox_CFinite_mult_cancel";
  1407 val capprox_CFinite_mult_cancel_iff1 = thm "capprox_CFinite_mult_cancel_iff1";
  1408 val capprox_cmonad_iff = thm "capprox_cmonad_iff";
  1409 val CInfinitesimal_cmonad_eq = thm "CInfinitesimal_cmonad_eq";
  1410 val mem_cmonad_iff = thm "mem_cmonad_iff";
  1411 val CInfinitesimal_cmonad_zero_iff = thm "CInfinitesimal_cmonad_zero_iff";
  1412 val cmonad_zero_minus_iff = thm "cmonad_zero_minus_iff";
  1413 val cmonad_zero_hcmod_iff = thm "cmonad_zero_hcmod_iff";
  1414 val mem_cmonad_self = thm "mem_cmonad_self";
  1415 val stc_capprox_self = thm "stc_capprox_self";
  1416 val stc_SComplex = thm "stc_SComplex";
  1417 val stc_CFinite = thm "stc_CFinite";
  1418 val stc_SComplex_eq = thm "stc_SComplex_eq";
  1419 val stc_hcomplex_of_complex = thm "stc_hcomplex_of_complex";
  1420 val stc_eq_capprox = thm "stc_eq_capprox";
  1421 val capprox_stc_eq = thm "capprox_stc_eq";
  1422 val stc_eq_capprox_iff = thm "stc_eq_capprox_iff";
  1423 val stc_CInfinitesimal_add_SComplex = thm "stc_CInfinitesimal_add_SComplex";
  1424 val stc_CInfinitesimal_add_SComplex2 = thm "stc_CInfinitesimal_add_SComplex2";
  1425 val CFinite_stc_CInfinitesimal_add = thm "CFinite_stc_CInfinitesimal_add";
  1426 val stc_add = thm "stc_add";
  1427 val stc_number_of = thm "stc_number_of";
  1428 val stc_zero = thm "stc_zero";
  1429 val stc_one = thm "stc_one";
  1430 val stc_minus = thm "stc_minus";
  1431 val stc_diff = thm "stc_diff";
  1432 val lemma_stc_mult = thm "lemma_stc_mult";
  1433 val stc_mult = thm "stc_mult";
  1434 val stc_CInfinitesimal = thm "stc_CInfinitesimal";
  1435 val stc_not_CInfinitesimal = thm "stc_not_CInfinitesimal";
  1436 val stc_inverse = thm "stc_inverse";
  1437 val stc_divide = thm "stc_divide";
  1438 val stc_idempotent = thm "stc_idempotent";
  1439 val CFinite_HFinite_hcomplex_of_hypreal = thm "CFinite_HFinite_hcomplex_of_hypreal";
  1440 val SComplex_SReal_hcomplex_of_hypreal = thm "SComplex_SReal_hcomplex_of_hypreal";
  1441 val stc_hcomplex_of_hypreal = thm "stc_hcomplex_of_hypreal";
  1442 val CInfinitesimal_hcnj_iff = thm "CInfinitesimal_hcnj_iff";
  1443 val CInfinite_HInfinite_iff = thm "CInfinite_HInfinite_iff";
  1444 val hcomplex_split_CInfinitesimal_iff = thm "hcomplex_split_CInfinitesimal_iff";
  1445 val hcomplex_split_CFinite_iff = thm "hcomplex_split_CFinite_iff";
  1446 val hcomplex_split_SComplex_iff = thm "hcomplex_split_SComplex_iff";
  1447 val hcomplex_split_CInfinite_iff = thm "hcomplex_split_CInfinite_iff";
  1448 val hcomplex_split_capprox_iff = thm "hcomplex_split_capprox_iff";
  1449 val complex_seq_to_hcomplex_CInfinitesimal = thm "complex_seq_to_hcomplex_CInfinitesimal";
  1450 val CInfinitesimal_hcomplex_of_hypreal_epsilon = thm "CInfinitesimal_hcomplex_of_hypreal_epsilon";
  1451 val hcomplex_of_complex_approx_zero_iff = thm "hcomplex_of_complex_approx_zero_iff";
  1452 val hcomplex_of_complex_approx_zero_iff2 = thm "hcomplex_of_complex_approx_zero_iff2";
  1453 *}
  1454 
  1455  
  1456 end