src/HOL/Nonstandard_Analysis/NSCA.thy
author haftmann
Mon Jun 05 15:59:41 2017 +0200 (2017-06-05)
changeset 66010 2f7d39285a1a
parent 63901 4ce989e962e0
child 67091 1393c2340eec
permissions -rw-r--r--
executable domain membership checks
     1 (*  Title:      HOL/Nonstandard_Analysis/NSCA.thy
     2     Author:     Jacques D. Fleuriot
     3     Copyright:  2001, 2002 University of Edinburgh
     4 *)
     5 
     6 section\<open>Non-Standard Complex Analysis\<close>
     7 
     8 theory NSCA
     9 imports NSComplex HTranscendental
    10 begin
    11 
    12 abbreviation
    13    (* standard complex numbers reagarded as an embedded subset of NS complex *)
    14    SComplex  :: "hcomplex set" where
    15    "SComplex \<equiv> Standard"
    16 
    17 definition \<comment>\<open>standard part map\<close>
    18   stc :: "hcomplex => hcomplex" where 
    19   "stc x = (SOME r. x \<in> HFinite & r:SComplex & r \<approx> x)"
    20 
    21 
    22 subsection\<open>Closure Laws for SComplex, the Standard Complex Numbers\<close>
    23 
    24 lemma SComplex_minus_iff [simp]: "(-x \<in> SComplex) = (x \<in> SComplex)"
    25 by (auto, drule Standard_minus, auto)
    26 
    27 lemma SComplex_add_cancel:
    28      "[| x + y \<in> SComplex; y \<in> SComplex |] ==> x \<in> SComplex"
    29 by (drule (1) Standard_diff, simp)
    30 
    31 lemma SReal_hcmod_hcomplex_of_complex [simp]:
    32      "hcmod (hcomplex_of_complex r) \<in> \<real>"
    33 by (simp add: Reals_eq_Standard)
    34 
    35 lemma SReal_hcmod_numeral [simp]: "hcmod (numeral w ::hcomplex) \<in> \<real>"
    36 by (simp add: Reals_eq_Standard)
    37 
    38 lemma SReal_hcmod_SComplex: "x \<in> SComplex ==> hcmod x \<in> \<real>"
    39 by (simp add: Reals_eq_Standard)
    40 
    41 lemma SComplex_divide_numeral:
    42      "r \<in> SComplex ==> r/(numeral w::hcomplex) \<in> SComplex"
    43 by simp
    44 
    45 lemma SComplex_UNIV_complex:
    46      "{x. hcomplex_of_complex x \<in> SComplex} = (UNIV::complex set)"
    47 by simp
    48 
    49 lemma SComplex_iff: "(x \<in> SComplex) = (\<exists>y. x = hcomplex_of_complex y)"
    50 by (simp add: Standard_def image_def)
    51 
    52 lemma hcomplex_of_complex_image:
    53      "hcomplex_of_complex `(UNIV::complex set) = SComplex"
    54 by (simp add: Standard_def)
    55 
    56 lemma inv_hcomplex_of_complex_image: "inv hcomplex_of_complex `SComplex = UNIV"
    57 by (auto simp add: Standard_def image_def) (metis inj_star_of inv_f_f)
    58 
    59 lemma SComplex_hcomplex_of_complex_image: 
    60       "[| \<exists>x. x: P; P \<le> SComplex |] ==> \<exists>Q. P = hcomplex_of_complex ` Q"
    61 apply (simp add: Standard_def, blast)
    62 done
    63 
    64 lemma SComplex_SReal_dense:
    65      "[| x \<in> SComplex; y \<in> SComplex; hcmod x < hcmod y  
    66       |] ==> \<exists>r \<in> Reals. hcmod x< r & r < hcmod y"
    67 apply (auto intro: SReal_dense simp add: SReal_hcmod_SComplex)
    68 done
    69 
    70 
    71 subsection\<open>The Finite Elements form a Subring\<close>
    72 
    73 lemma HFinite_hcmod_hcomplex_of_complex [simp]:
    74      "hcmod (hcomplex_of_complex r) \<in> HFinite"
    75 by (auto intro!: SReal_subset_HFinite [THEN subsetD])
    76 
    77 lemma HFinite_hcmod_iff: "(x \<in> HFinite) = (hcmod x \<in> HFinite)"
    78 by (simp add: HFinite_def)
    79 
    80 lemma HFinite_bounded_hcmod:
    81   "[|x \<in> HFinite; y \<le> hcmod x; 0 \<le> y |] ==> y: HFinite"
    82 by (auto intro: HFinite_bounded simp add: HFinite_hcmod_iff)
    83 
    84 
    85 subsection\<open>The Complex Infinitesimals form a Subring\<close>
    86 
    87 lemma hcomplex_sum_of_halves: "x/(2::hcomplex) + x/(2::hcomplex) = x"
    88 by auto
    89 
    90 lemma Infinitesimal_hcmod_iff: 
    91    "(z \<in> Infinitesimal) = (hcmod z \<in> Infinitesimal)"
    92 by (simp add: Infinitesimal_def)
    93 
    94 lemma HInfinite_hcmod_iff: "(z \<in> HInfinite) = (hcmod z \<in> HInfinite)"
    95 by (simp add: HInfinite_def)
    96 
    97 lemma HFinite_diff_Infinitesimal_hcmod:
    98      "x \<in> HFinite - Infinitesimal ==> hcmod x \<in> HFinite - Infinitesimal"
    99 by (simp add: HFinite_hcmod_iff Infinitesimal_hcmod_iff)
   100 
   101 lemma hcmod_less_Infinitesimal:
   102      "[| e \<in> Infinitesimal; hcmod x < hcmod e |] ==> x \<in> Infinitesimal"
   103 by (auto elim: hrabs_less_Infinitesimal simp add: Infinitesimal_hcmod_iff)
   104 
   105 lemma hcmod_le_Infinitesimal:
   106      "[| e \<in> Infinitesimal; hcmod x \<le> hcmod e |] ==> x \<in> Infinitesimal"
   107 by (auto elim: hrabs_le_Infinitesimal simp add: Infinitesimal_hcmod_iff)
   108 
   109 lemma Infinitesimal_interval_hcmod:
   110      "[| e \<in> Infinitesimal;  
   111           e' \<in> Infinitesimal;  
   112           hcmod e' < hcmod x ; hcmod x < hcmod e  
   113        |] ==> x \<in> Infinitesimal"
   114 by (auto intro: Infinitesimal_interval simp add: Infinitesimal_hcmod_iff)
   115 
   116 lemma Infinitesimal_interval2_hcmod:
   117      "[| e \<in> Infinitesimal;  
   118          e' \<in> Infinitesimal;  
   119          hcmod e' \<le> hcmod x ; hcmod x \<le> hcmod e  
   120       |] ==> x \<in> Infinitesimal"
   121 by (auto intro: Infinitesimal_interval2 simp add: Infinitesimal_hcmod_iff)
   122 
   123 
   124 subsection\<open>The ``Infinitely Close'' Relation\<close>
   125 
   126 (*
   127 Goalw [capprox_def,approx_def] "(z @c= w) = (hcmod z \<approx> hcmod w)"
   128 by (auto_tac (claset(),simpset() addsimps [Infinitesimal_hcmod_iff]));
   129 *)
   130 
   131 lemma approx_SComplex_mult_cancel_zero:
   132      "[| a \<in> SComplex; a \<noteq> 0; a*x \<approx> 0 |] ==> x \<approx> 0"
   133 apply (drule Standard_inverse [THEN Standard_subset_HFinite [THEN subsetD]])
   134 apply (auto dest: approx_mult2 simp add: mult.assoc [symmetric])
   135 done
   136 
   137 lemma approx_mult_SComplex1: "[| a \<in> SComplex; x \<approx> 0 |] ==> x*a \<approx> 0"
   138 by (auto dest: Standard_subset_HFinite [THEN subsetD] approx_mult1)
   139 
   140 lemma approx_mult_SComplex2: "[| a \<in> SComplex; x \<approx> 0 |] ==> a*x \<approx> 0"
   141 by (auto dest: Standard_subset_HFinite [THEN subsetD] approx_mult2)
   142 
   143 lemma approx_mult_SComplex_zero_cancel_iff [simp]:
   144      "[|a \<in> SComplex; a \<noteq> 0 |] ==> (a*x \<approx> 0) = (x \<approx> 0)"
   145 by (blast intro: approx_SComplex_mult_cancel_zero approx_mult_SComplex2)
   146 
   147 lemma approx_SComplex_mult_cancel:
   148      "[| a \<in> SComplex; a \<noteq> 0; a* w \<approx> a*z |] ==> w \<approx> z"
   149 apply (drule Standard_inverse [THEN Standard_subset_HFinite [THEN subsetD]])
   150 apply (auto dest: approx_mult2 simp add: mult.assoc [symmetric])
   151 done
   152 
   153 lemma approx_SComplex_mult_cancel_iff1 [simp]:
   154      "[| a \<in> SComplex; a \<noteq> 0|] ==> (a* w \<approx> a*z) = (w \<approx> z)"
   155 by (auto intro!: approx_mult2 Standard_subset_HFinite [THEN subsetD]
   156             intro: approx_SComplex_mult_cancel)
   157 
   158 (* TODO: generalize following theorems: hcmod -> hnorm *)
   159 
   160 lemma approx_hcmod_approx_zero: "(x \<approx> y) = (hcmod (y - x) \<approx> 0)"
   161 apply (subst hnorm_minus_commute)
   162 apply (simp add: approx_def Infinitesimal_hcmod_iff)
   163 done
   164 
   165 lemma approx_approx_zero_iff: "(x \<approx> 0) = (hcmod x \<approx> 0)"
   166 by (simp add: approx_hcmod_approx_zero)
   167 
   168 lemma approx_minus_zero_cancel_iff [simp]: "(-x \<approx> 0) = (x \<approx> 0)"
   169 by (simp add: approx_def)
   170 
   171 lemma Infinitesimal_hcmod_add_diff:
   172      "u \<approx> 0 ==> hcmod(x + u) - hcmod x \<in> Infinitesimal"
   173 apply (drule approx_approx_zero_iff [THEN iffD1])
   174 apply (rule_tac e = "hcmod u" and e' = "- hcmod u" in Infinitesimal_interval2)
   175 apply (auto simp add: mem_infmal_iff [symmetric])
   176 apply (rule_tac c1 = "hcmod x" in add_le_cancel_left [THEN iffD1])
   177 apply auto
   178 done
   179 
   180 lemma approx_hcmod_add_hcmod: "u \<approx> 0 ==> hcmod(x + u) \<approx> hcmod x"
   181 apply (rule approx_minus_iff [THEN iffD2])
   182 apply (auto intro: Infinitesimal_hcmod_add_diff simp add: mem_infmal_iff [symmetric])
   183 done
   184 
   185 
   186 subsection\<open>Zero is the Only Infinitesimal Complex Number\<close>
   187 
   188 lemma Infinitesimal_less_SComplex:
   189    "[| x \<in> SComplex; y \<in> Infinitesimal; 0 < hcmod x |] ==> hcmod y < hcmod x"
   190 by (auto intro: Infinitesimal_less_SReal SReal_hcmod_SComplex simp add: Infinitesimal_hcmod_iff)
   191 
   192 lemma SComplex_Int_Infinitesimal_zero: "SComplex Int Infinitesimal = {0}"
   193 by (auto simp add: Standard_def Infinitesimal_hcmod_iff)
   194 
   195 lemma SComplex_Infinitesimal_zero:
   196      "[| x \<in> SComplex; x \<in> Infinitesimal|] ==> x = 0"
   197 by (cut_tac SComplex_Int_Infinitesimal_zero, blast)
   198 
   199 lemma SComplex_HFinite_diff_Infinitesimal:
   200      "[| x \<in> SComplex; x \<noteq> 0 |] ==> x \<in> HFinite - Infinitesimal"
   201 by (auto dest: SComplex_Infinitesimal_zero Standard_subset_HFinite [THEN subsetD])
   202 
   203 lemma hcomplex_of_complex_HFinite_diff_Infinitesimal:
   204      "hcomplex_of_complex x \<noteq> 0 
   205       ==> hcomplex_of_complex x \<in> HFinite - Infinitesimal"
   206 by (rule SComplex_HFinite_diff_Infinitesimal, auto)
   207 
   208 lemma numeral_not_Infinitesimal [simp]:
   209      "numeral w \<noteq> (0::hcomplex) ==> (numeral w::hcomplex) \<notin> Infinitesimal"
   210 by (fast dest: Standard_numeral [THEN SComplex_Infinitesimal_zero])
   211 
   212 lemma approx_SComplex_not_zero:
   213      "[| y \<in> SComplex; x \<approx> y; y\<noteq> 0 |] ==> x \<noteq> 0"
   214 by (auto dest: SComplex_Infinitesimal_zero approx_sym [THEN mem_infmal_iff [THEN iffD2]])
   215 
   216 lemma SComplex_approx_iff:
   217      "[|x \<in> SComplex; y \<in> SComplex|] ==> (x \<approx> y) = (x = y)"
   218 by (auto simp add: Standard_def)
   219 
   220 lemma numeral_Infinitesimal_iff [simp]:
   221      "((numeral w :: hcomplex) \<in> Infinitesimal) =
   222       (numeral w = (0::hcomplex))"
   223 apply (rule iffI)
   224 apply (fast dest: Standard_numeral [THEN SComplex_Infinitesimal_zero])
   225 apply (simp (no_asm_simp))
   226 done
   227 
   228 lemma approx_unique_complex:
   229      "[| r \<in> SComplex; s \<in> SComplex; r \<approx> x; s \<approx> x|] ==> r = s"
   230 by (blast intro: SComplex_approx_iff [THEN iffD1] approx_trans2)
   231 
   232 subsection \<open>Properties of @{term hRe}, @{term hIm} and @{term HComplex}\<close>
   233 
   234 
   235 lemma abs_hRe_le_hcmod: "\<And>x. \<bar>hRe x\<bar> \<le> hcmod x"
   236 by transfer (rule abs_Re_le_cmod)
   237 
   238 lemma abs_hIm_le_hcmod: "\<And>x. \<bar>hIm x\<bar> \<le> hcmod x"
   239 by transfer (rule abs_Im_le_cmod)
   240 
   241 lemma Infinitesimal_hRe: "x \<in> Infinitesimal \<Longrightarrow> hRe x \<in> Infinitesimal"
   242 apply (rule InfinitesimalI2, simp)
   243 apply (rule order_le_less_trans [OF abs_hRe_le_hcmod])
   244 apply (erule (1) InfinitesimalD2)
   245 done
   246 
   247 lemma Infinitesimal_hIm: "x \<in> Infinitesimal \<Longrightarrow> hIm x \<in> Infinitesimal"
   248 apply (rule InfinitesimalI2, simp)
   249 apply (rule order_le_less_trans [OF abs_hIm_le_hcmod])
   250 apply (erule (1) InfinitesimalD2)
   251 done
   252 
   253 lemma real_sqrt_lessI: "\<lbrakk>0 < u; x < u\<^sup>2\<rbrakk> \<Longrightarrow> sqrt x < u"
   254 (* TODO: this belongs somewhere else *)
   255 by (frule real_sqrt_less_mono) simp
   256 
   257 lemma hypreal_sqrt_lessI:
   258   "\<And>x u. \<lbrakk>0 < u; x < u\<^sup>2\<rbrakk> \<Longrightarrow> ( *f* sqrt) x < u"
   259 by transfer (rule real_sqrt_lessI)
   260  
   261 lemma hypreal_sqrt_ge_zero: "\<And>x. 0 \<le> x \<Longrightarrow> 0 \<le> ( *f* sqrt) x"
   262 by transfer (rule real_sqrt_ge_zero)
   263 
   264 lemma Infinitesimal_sqrt:
   265   "\<lbrakk>x \<in> Infinitesimal; 0 \<le> x\<rbrakk> \<Longrightarrow> ( *f* sqrt) x \<in> Infinitesimal"
   266 apply (rule InfinitesimalI2)
   267 apply (drule_tac r="r\<^sup>2" in InfinitesimalD2, simp)
   268 apply (simp add: hypreal_sqrt_ge_zero)
   269 apply (rule hypreal_sqrt_lessI, simp_all)
   270 done
   271 
   272 lemma Infinitesimal_HComplex:
   273   "\<lbrakk>x \<in> Infinitesimal; y \<in> Infinitesimal\<rbrakk> \<Longrightarrow> HComplex x y \<in> Infinitesimal"
   274 apply (rule Infinitesimal_hcmod_iff [THEN iffD2])
   275 apply (simp add: hcmod_i)
   276 apply (rule Infinitesimal_add)
   277 apply (erule Infinitesimal_hrealpow, simp)
   278 apply (erule Infinitesimal_hrealpow, simp)
   279 done
   280 
   281 lemma hcomplex_Infinitesimal_iff:
   282   "(x \<in> Infinitesimal) = (hRe x \<in> Infinitesimal \<and> hIm x \<in> Infinitesimal)"
   283 apply (safe intro!: Infinitesimal_hRe Infinitesimal_hIm)
   284 apply (drule (1) Infinitesimal_HComplex, simp)
   285 done
   286 
   287 lemma hRe_diff [simp]: "\<And>x y. hRe (x - y) = hRe x - hRe y"
   288 by transfer simp
   289 
   290 lemma hIm_diff [simp]: "\<And>x y. hIm (x - y) = hIm x - hIm y"
   291 by transfer simp
   292 
   293 lemma approx_hRe: "x \<approx> y \<Longrightarrow> hRe x \<approx> hRe y"
   294 unfolding approx_def by (drule Infinitesimal_hRe) simp
   295 
   296 lemma approx_hIm: "x \<approx> y \<Longrightarrow> hIm x \<approx> hIm y"
   297 unfolding approx_def by (drule Infinitesimal_hIm) simp
   298 
   299 lemma approx_HComplex:
   300   "\<lbrakk>a \<approx> b; c \<approx> d\<rbrakk> \<Longrightarrow> HComplex a c \<approx> HComplex b d"
   301 unfolding approx_def by (simp add: Infinitesimal_HComplex)
   302 
   303 lemma hcomplex_approx_iff:
   304   "(x \<approx> y) = (hRe x \<approx> hRe y \<and> hIm x \<approx> hIm y)"
   305 unfolding approx_def by (simp add: hcomplex_Infinitesimal_iff)
   306 
   307 lemma HFinite_hRe: "x \<in> HFinite \<Longrightarrow> hRe x \<in> HFinite"
   308 apply (auto simp add: HFinite_def SReal_def)
   309 apply (rule_tac x="star_of r" in exI, simp)
   310 apply (erule order_le_less_trans [OF abs_hRe_le_hcmod])
   311 done
   312 
   313 lemma HFinite_hIm: "x \<in> HFinite \<Longrightarrow> hIm x \<in> HFinite"
   314 apply (auto simp add: HFinite_def SReal_def)
   315 apply (rule_tac x="star_of r" in exI, simp)
   316 apply (erule order_le_less_trans [OF abs_hIm_le_hcmod])
   317 done
   318 
   319 lemma HFinite_HComplex:
   320   "\<lbrakk>x \<in> HFinite; y \<in> HFinite\<rbrakk> \<Longrightarrow> HComplex x y \<in> HFinite"
   321 apply (subgoal_tac "HComplex x 0 + HComplex 0 y \<in> HFinite", simp)
   322 apply (rule HFinite_add)
   323 apply (simp add: HFinite_hcmod_iff hcmod_i)
   324 apply (simp add: HFinite_hcmod_iff hcmod_i)
   325 done
   326 
   327 lemma hcomplex_HFinite_iff:
   328   "(x \<in> HFinite) = (hRe x \<in> HFinite \<and> hIm x \<in> HFinite)"
   329 apply (safe intro!: HFinite_hRe HFinite_hIm)
   330 apply (drule (1) HFinite_HComplex, simp)
   331 done
   332 
   333 lemma hcomplex_HInfinite_iff:
   334   "(x \<in> HInfinite) = (hRe x \<in> HInfinite \<or> hIm x \<in> HInfinite)"
   335 by (simp add: HInfinite_HFinite_iff hcomplex_HFinite_iff)
   336 
   337 lemma hcomplex_of_hypreal_approx_iff [simp]:
   338      "(hcomplex_of_hypreal x \<approx> hcomplex_of_hypreal z) = (x \<approx> z)"
   339 by (simp add: hcomplex_approx_iff)
   340 
   341 lemma Standard_HComplex:
   342   "\<lbrakk>x \<in> Standard; y \<in> Standard\<rbrakk> \<Longrightarrow> HComplex x y \<in> Standard"
   343 by (simp add: HComplex_def)
   344 
   345 (* Here we go - easy proof now!! *)
   346 lemma stc_part_Ex: "x:HFinite ==> \<exists>t \<in> SComplex. x \<approx> t"
   347 apply (simp add: hcomplex_HFinite_iff hcomplex_approx_iff)
   348 apply (rule_tac x="HComplex (st (hRe x)) (st (hIm x))" in bexI)
   349 apply (simp add: st_approx_self [THEN approx_sym])
   350 apply (simp add: Standard_HComplex st_SReal [unfolded Reals_eq_Standard])
   351 done
   352 
   353 lemma stc_part_Ex1: "x:HFinite ==> \<exists>!t. t \<in> SComplex &  x \<approx> t"
   354 apply (drule stc_part_Ex, safe)
   355 apply (drule_tac [2] approx_sym, drule_tac [2] approx_sym, drule_tac [2] approx_sym)
   356 apply (auto intro!: approx_unique_complex)
   357 done
   358 
   359 lemmas hcomplex_of_complex_approx_inverse =
   360   hcomplex_of_complex_HFinite_diff_Infinitesimal [THEN [2] approx_inverse]
   361 
   362 
   363 subsection\<open>Theorems About Monads\<close>
   364 
   365 lemma monad_zero_hcmod_iff: "(x \<in> monad 0) = (hcmod x:monad 0)"
   366 by (simp add: Infinitesimal_monad_zero_iff [symmetric] Infinitesimal_hcmod_iff)
   367 
   368 
   369 subsection\<open>Theorems About Standard Part\<close>
   370 
   371 lemma stc_approx_self: "x \<in> HFinite ==> stc x \<approx> x"
   372 apply (simp add: stc_def)
   373 apply (frule stc_part_Ex, safe)
   374 apply (rule someI2)
   375 apply (auto intro: approx_sym)
   376 done
   377 
   378 lemma stc_SComplex: "x \<in> HFinite ==> stc x \<in> SComplex"
   379 apply (simp add: stc_def)
   380 apply (frule stc_part_Ex, safe)
   381 apply (rule someI2)
   382 apply (auto intro: approx_sym)
   383 done
   384 
   385 lemma stc_HFinite: "x \<in> HFinite ==> stc x \<in> HFinite"
   386 by (erule stc_SComplex [THEN Standard_subset_HFinite [THEN subsetD]])
   387 
   388 lemma stc_unique: "\<lbrakk>y \<in> SComplex; y \<approx> x\<rbrakk> \<Longrightarrow> stc x = y"
   389 apply (frule Standard_subset_HFinite [THEN subsetD])
   390 apply (drule (1) approx_HFinite)
   391 apply (unfold stc_def)
   392 apply (rule some_equality)
   393 apply (auto intro: approx_unique_complex)
   394 done
   395 
   396 lemma stc_SComplex_eq [simp]: "x \<in> SComplex ==> stc x = x"
   397 apply (erule stc_unique)
   398 apply (rule approx_refl)
   399 done
   400 
   401 lemma stc_hcomplex_of_complex:
   402      "stc (hcomplex_of_complex x) = hcomplex_of_complex x"
   403 by auto
   404 
   405 lemma stc_eq_approx:
   406      "[| x \<in> HFinite; y \<in> HFinite; stc x = stc y |] ==> x \<approx> y"
   407 by (auto dest!: stc_approx_self elim!: approx_trans3)
   408 
   409 lemma approx_stc_eq:
   410      "[| x \<in> HFinite; y \<in> HFinite; x \<approx> y |] ==> stc x = stc y"
   411 by (blast intro: approx_trans approx_trans2 SComplex_approx_iff [THEN iffD1]
   412           dest: stc_approx_self stc_SComplex)
   413 
   414 lemma stc_eq_approx_iff:
   415      "[| x \<in> HFinite; y \<in> HFinite|] ==> (x \<approx> y) = (stc x = stc y)"
   416 by (blast intro: approx_stc_eq stc_eq_approx)
   417 
   418 lemma stc_Infinitesimal_add_SComplex:
   419      "[| x \<in> SComplex; e \<in> Infinitesimal |] ==> stc(x + e) = x"
   420 apply (erule stc_unique)
   421 apply (erule Infinitesimal_add_approx_self)
   422 done
   423 
   424 lemma stc_Infinitesimal_add_SComplex2:
   425      "[| x \<in> SComplex; e \<in> Infinitesimal |] ==> stc(e + x) = x"
   426 apply (erule stc_unique)
   427 apply (erule Infinitesimal_add_approx_self2)
   428 done
   429 
   430 lemma HFinite_stc_Infinitesimal_add:
   431      "x \<in> HFinite ==> \<exists>e \<in> Infinitesimal. x = stc(x) + e"
   432 by (blast dest!: stc_approx_self [THEN approx_sym] bex_Infinitesimal_iff2 [THEN iffD2])
   433 
   434 lemma stc_add:
   435      "[| x \<in> HFinite; y \<in> HFinite |] ==> stc (x + y) = stc(x) + stc(y)"
   436 by (simp add: stc_unique stc_SComplex stc_approx_self approx_add)
   437 
   438 lemma stc_numeral [simp]: "stc (numeral w) = numeral w"
   439 by (rule Standard_numeral [THEN stc_SComplex_eq])
   440 
   441 lemma stc_zero [simp]: "stc 0 = 0"
   442 by simp
   443 
   444 lemma stc_one [simp]: "stc 1 = 1"
   445 by simp
   446 
   447 lemma stc_minus: "y \<in> HFinite ==> stc(-y) = -stc(y)"
   448 by (simp add: stc_unique stc_SComplex stc_approx_self approx_minus)
   449 
   450 lemma stc_diff: 
   451      "[| x \<in> HFinite; y \<in> HFinite |] ==> stc (x-y) = stc(x) - stc(y)"
   452 by (simp add: stc_unique stc_SComplex stc_approx_self approx_diff)
   453 
   454 lemma stc_mult:
   455      "[| x \<in> HFinite; y \<in> HFinite |]  
   456                ==> stc (x * y) = stc(x) * stc(y)"
   457 by (simp add: stc_unique stc_SComplex stc_approx_self approx_mult_HFinite)
   458 
   459 lemma stc_Infinitesimal: "x \<in> Infinitesimal ==> stc x = 0"
   460 by (simp add: stc_unique mem_infmal_iff)
   461 
   462 lemma stc_not_Infinitesimal: "stc(x) \<noteq> 0 ==> x \<notin> Infinitesimal"
   463 by (fast intro: stc_Infinitesimal)
   464 
   465 lemma stc_inverse:
   466      "[| x \<in> HFinite; stc x \<noteq> 0 |]  
   467       ==> stc(inverse x) = inverse (stc x)"
   468 apply (drule stc_not_Infinitesimal)
   469 apply (simp add: stc_unique stc_SComplex stc_approx_self approx_inverse)
   470 done
   471 
   472 lemma stc_divide [simp]:
   473      "[| x \<in> HFinite; y \<in> HFinite; stc y \<noteq> 0 |]  
   474       ==> stc(x/y) = (stc x) / (stc y)"
   475 by (simp add: divide_inverse stc_mult stc_not_Infinitesimal HFinite_inverse stc_inverse)
   476 
   477 lemma stc_idempotent [simp]: "x \<in> HFinite ==> stc(stc(x)) = stc(x)"
   478 by (blast intro: stc_HFinite stc_approx_self approx_stc_eq)
   479 
   480 lemma HFinite_HFinite_hcomplex_of_hypreal:
   481      "z \<in> HFinite ==> hcomplex_of_hypreal z \<in> HFinite"
   482 by (simp add: hcomplex_HFinite_iff)
   483 
   484 lemma SComplex_SReal_hcomplex_of_hypreal:
   485      "x \<in> \<real> ==>  hcomplex_of_hypreal x \<in> SComplex"
   486 apply (rule Standard_of_hypreal)
   487 apply (simp add: Reals_eq_Standard)
   488 done
   489 
   490 lemma stc_hcomplex_of_hypreal: 
   491  "z \<in> HFinite ==> stc(hcomplex_of_hypreal z) = hcomplex_of_hypreal (st z)"
   492 apply (rule stc_unique)
   493 apply (rule SComplex_SReal_hcomplex_of_hypreal)
   494 apply (erule st_SReal)
   495 apply (simp add: hcomplex_of_hypreal_approx_iff st_approx_self)
   496 done
   497 
   498 (*
   499 Goal "x \<in> HFinite ==> hcmod(stc x) = st(hcmod x)"
   500 by (dtac stc_approx_self 1)
   501 by (auto_tac (claset(),simpset() addsimps [bex_Infinitesimal_iff2 RS sym]));
   502 
   503 
   504 approx_hcmod_add_hcmod
   505 *)
   506 
   507 lemma Infinitesimal_hcnj_iff [simp]:
   508      "(hcnj z \<in> Infinitesimal) = (z \<in> Infinitesimal)"
   509 by (simp add: Infinitesimal_hcmod_iff)
   510 
   511 lemma Infinitesimal_hcomplex_of_hypreal_epsilon [simp]:
   512      "hcomplex_of_hypreal \<epsilon> \<in> Infinitesimal"
   513 by (simp add: Infinitesimal_hcmod_iff)
   514 
   515 end