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