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