wneuper/isa: src/HOL/NSA/NSCA.thy@71c8973a604b

     1 (*  Title       : NSA/NSCA.thy

     2     Author      : Jacques D. Fleuriot

     3     Copyright   : 2001,2002 University of Edinburgh

     4 *)

     6 header{*Non-Standard Complex Analysis*}

     8 theory NSCA

     9 imports NSComplex HTranscendental

    10 begin

    12 abbreviation

    13    (* standard complex numbers reagarded as an embedded subset of NS complex *)

    14    SComplex  :: "hcomplex set" where

    15    "SComplex \<equiv> Standard"

    17 definition --{* standard part map*}

    18   stc :: "hcomplex => hcomplex" where

    19   [code del]: "stc x = (SOME r. x \<in> HFinite & r:SComplex & r @= x)"

    22 subsection{*Closure Laws for SComplex, the Standard Complex Numbers*}

    24 lemma SComplex_minus_iff [simp]: "(-x \<in> SComplex) = (x \<in> SComplex)"

    25 by (auto, drule Standard_minus, auto)

    27 lemma SComplex_add_cancel:

    28      "[| x + y \<in> SComplex; y \<in> SComplex |] ==> x \<in> SComplex"

    29 by (drule (1) Standard_diff, simp)

    31 lemma SReal_hcmod_hcomplex_of_complex [simp]:

    32      "hcmod (hcomplex_of_complex r) \<in> Reals"

    33 by (simp add: Reals_eq_Standard)

    35 lemma SReal_hcmod_number_of [simp]: "hcmod (number_of w ::hcomplex) \<in> Reals"

    36 by (simp add: Reals_eq_Standard)

    38 lemma SReal_hcmod_SComplex: "x \<in> SComplex ==> hcmod x \<in> Reals"

    39 by (simp add: Reals_eq_Standard)

    41 lemma SComplex_divide_number_of:

    42      "r \<in> SComplex ==> r/(number_of w::hcomplex) \<in> SComplex"

    43 by simp

    45 lemma SComplex_UNIV_complex:

    46      "{x. hcomplex_of_complex x \<in> SComplex} = (UNIV::complex set)"

    47 by simp

    49 lemma SComplex_iff: "(x \<in> SComplex) = (\<exists>y. x = hcomplex_of_complex y)"

    50 by (simp add: Standard_def image_def)

    52 lemma hcomplex_of_complex_image:

    53      "hcomplex_of_complex `(UNIV::complex set) = SComplex"

    54 by (simp add: Standard_def)

    56 lemma inv_hcomplex_of_complex_image: "inv hcomplex_of_complex `SComplex = UNIV"

    57 apply (auto simp add: Standard_def image_def)

    58 apply (rule inj_hcomplex_of_complex [THEN inv_f_f, THEN subst], blast)

    59 done

    61 lemma SComplex_hcomplex_of_complex_image:

    62       "[| \<exists>x. x: P; P \<le> SComplex |] ==> \<exists>Q. P = hcomplex_of_complex ` Q"

    63 apply (simp add: Standard_def, blast)

    64 done

    66 lemma SComplex_SReal_dense:

    67      "[| x \<in> SComplex; y \<in> SComplex; hcmod x < hcmod y

    68       |] ==> \<exists>r \<in> Reals. hcmod x< r & r < hcmod y"

    69 apply (auto intro: SReal_dense simp add: SReal_hcmod_SComplex)

    70 done

    72 lemma SComplex_hcmod_SReal:

    73       "z \<in> SComplex ==> hcmod z \<in> Reals"

    74 by (simp add: Reals_eq_Standard)

    77 subsection{*The Finite Elements form a Subring*}

    79 lemma HFinite_hcmod_hcomplex_of_complex [simp]:

    80      "hcmod (hcomplex_of_complex r) \<in> HFinite"

    81 by (auto intro!: SReal_subset_HFinite [THEN subsetD])

    83 lemma HFinite_hcmod_iff: "(x \<in> HFinite) = (hcmod x \<in> HFinite)"

    84 by (simp add: HFinite_def)

    86 lemma HFinite_bounded_hcmod:

    87   "[|x \<in> HFinite; y \<le> hcmod x; 0 \<le> y |] ==> y: HFinite"

    88 by (auto intro: HFinite_bounded simp add: HFinite_hcmod_iff)

    91 subsection{*The Complex Infinitesimals form a Subring*}

    93 lemma hcomplex_sum_of_halves: "x/(2::hcomplex) + x/(2::hcomplex) = x"

    94 by auto

    96 lemma Infinitesimal_hcmod_iff:

    97    "(z \<in> Infinitesimal) = (hcmod z \<in> Infinitesimal)"

    98 by (simp add: Infinitesimal_def)

   100 lemma HInfinite_hcmod_iff: "(z \<in> HInfinite) = (hcmod z \<in> HInfinite)"

   101 by (simp add: HInfinite_def)

   103 lemma HFinite_diff_Infinitesimal_hcmod:

   104      "x \<in> HFinite - Infinitesimal ==> hcmod x \<in> HFinite - Infinitesimal"

   105 by (simp add: HFinite_hcmod_iff Infinitesimal_hcmod_iff)

   107 lemma hcmod_less_Infinitesimal:

   108      "[| e \<in> Infinitesimal; hcmod x < hcmod e |] ==> x \<in> Infinitesimal"

   109 by (auto elim: hrabs_less_Infinitesimal simp add: Infinitesimal_hcmod_iff)

   111 lemma hcmod_le_Infinitesimal:

   112      "[| e \<in> Infinitesimal; hcmod x \<le> hcmod e |] ==> x \<in> Infinitesimal"

   113 by (auto elim: hrabs_le_Infinitesimal simp add: Infinitesimal_hcmod_iff)

   115 lemma Infinitesimal_interval_hcmod:

   116      "[| e \<in> Infinitesimal;

   117           e' \<in> Infinitesimal;

   118           hcmod e' < hcmod x ; hcmod x < hcmod e

   119        |] ==> x \<in> Infinitesimal"

   120 by (auto intro: Infinitesimal_interval simp add: Infinitesimal_hcmod_iff)

   122 lemma Infinitesimal_interval2_hcmod:

   123      "[| e \<in> Infinitesimal;

   124          e' \<in> Infinitesimal;

   125          hcmod e' \<le> hcmod x ; hcmod x \<le> hcmod e

   126       |] ==> x \<in> Infinitesimal"

   127 by (auto intro: Infinitesimal_interval2 simp add: Infinitesimal_hcmod_iff)

   130 subsection{*The ``Infinitely Close'' Relation*}

   132 (*

   133 Goalw [capprox_def,approx_def] "(z @c= w) = (hcmod z @= hcmod w)"

   134 by (auto_tac (claset(),simpset() addsimps [Infinitesimal_hcmod_iff]));

   135 *)

   137 lemma approx_SComplex_mult_cancel_zero:

   138      "[| a \<in> SComplex; a \<noteq> 0; a*x @= 0 |] ==> x @= 0"

   139 apply (drule Standard_inverse [THEN Standard_subset_HFinite [THEN subsetD]])

   140 apply (auto dest: approx_mult2 simp add: mult_assoc [symmetric])

   141 done

   143 lemma approx_mult_SComplex1: "[| a \<in> SComplex; x @= 0 |] ==> x*a @= 0"

   144 by (auto dest: Standard_subset_HFinite [THEN subsetD] approx_mult1)

   146 lemma approx_mult_SComplex2: "[| a \<in> SComplex; x @= 0 |] ==> a*x @= 0"

   147 by (auto dest: Standard_subset_HFinite [THEN subsetD] approx_mult2)

   149 lemma approx_mult_SComplex_zero_cancel_iff [simp]:

   150      "[|a \<in> SComplex; a \<noteq> 0 |] ==> (a*x @= 0) = (x @= 0)"

   151 by (blast intro: approx_SComplex_mult_cancel_zero approx_mult_SComplex2)

   153 lemma approx_SComplex_mult_cancel:

   154      "[| a \<in> SComplex; a \<noteq> 0; a* w @= a*z |] ==> w @= z"

   155 apply (drule Standard_inverse [THEN Standard_subset_HFinite [THEN subsetD]])

   156 apply (auto dest: approx_mult2 simp add: mult_assoc [symmetric])

   157 done

   159 lemma approx_SComplex_mult_cancel_iff1 [simp]:

   160      "[| a \<in> SComplex; a \<noteq> 0|] ==> (a* w @= a*z) = (w @= z)"

   161 by (auto intro!: approx_mult2 Standard_subset_HFinite [THEN subsetD]

   162             intro: approx_SComplex_mult_cancel)

   164 (* TODO: generalize following theorems: hcmod -> hnorm *)

   166 lemma approx_hcmod_approx_zero: "(x @= y) = (hcmod (y - x) @= 0)"

   167 apply (subst hnorm_minus_commute)

   168 apply (simp add: approx_def Infinitesimal_hcmod_iff diff_minus)

   169 done

   171 lemma approx_approx_zero_iff: "(x @= 0) = (hcmod x @= 0)"

   172 by (simp add: approx_hcmod_approx_zero)

   174 lemma approx_minus_zero_cancel_iff [simp]: "(-x @= 0) = (x @= 0)"

   175 by (simp add: approx_def)

   177 lemma Infinitesimal_hcmod_add_diff:

   178      "u @= 0 ==> hcmod(x + u) - hcmod x \<in> Infinitesimal"

   179 apply (drule approx_approx_zero_iff [THEN iffD1])

   180 apply (rule_tac e = "hcmod u" and e' = "- hcmod u" in Infinitesimal_interval2)

   181 apply (auto simp add: mem_infmal_iff [symmetric] diff_def)

   182 apply (rule_tac c1 = "hcmod x" in add_le_cancel_left [THEN iffD1])

   183 apply (auto simp add: diff_minus [symmetric])

   184 done

   186 lemma approx_hcmod_add_hcmod: "u @= 0 ==> hcmod(x + u) @= hcmod x"

   187 apply (rule approx_minus_iff [THEN iffD2])

   188 apply (auto intro: Infinitesimal_hcmod_add_diff simp add: mem_infmal_iff [symmetric] diff_minus [symmetric])

   189 done

   192 subsection{*Zero is the Only Infinitesimal Complex Number*}

   194 lemma Infinitesimal_less_SComplex:

   195    "[| x \<in> SComplex; y \<in> Infinitesimal; 0 < hcmod x |] ==> hcmod y < hcmod x"

   196 by (auto intro: Infinitesimal_less_SReal SComplex_hcmod_SReal simp add: Infinitesimal_hcmod_iff)

   198 lemma SComplex_Int_Infinitesimal_zero: "SComplex Int Infinitesimal = {0}"

   199 by (auto simp add: Standard_def Infinitesimal_hcmod_iff)

   201 lemma SComplex_Infinitesimal_zero:

   202      "[| x \<in> SComplex; x \<in> Infinitesimal|] ==> x = 0"

   203 by (cut_tac SComplex_Int_Infinitesimal_zero, blast)

   205 lemma SComplex_HFinite_diff_Infinitesimal:

   206      "[| x \<in> SComplex; x \<noteq> 0 |] ==> x \<in> HFinite - Infinitesimal"

   207 by (auto dest: SComplex_Infinitesimal_zero Standard_subset_HFinite [THEN subsetD])

   209 lemma hcomplex_of_complex_HFinite_diff_Infinitesimal:

   210      "hcomplex_of_complex x \<noteq> 0

   211       ==> hcomplex_of_complex x \<in> HFinite - Infinitesimal"

   212 by (rule SComplex_HFinite_diff_Infinitesimal, auto)

   214 lemma number_of_not_Infinitesimal [simp]:

   215      "number_of w \<noteq> (0::hcomplex) ==> (number_of w::hcomplex) \<notin> Infinitesimal"

   216 by (fast dest: Standard_number_of [THEN SComplex_Infinitesimal_zero])

   218 lemma approx_SComplex_not_zero:

   219      "[| y \<in> SComplex; x @= y; y\<noteq> 0 |] ==> x \<noteq> 0"

   220 by (auto dest: SComplex_Infinitesimal_zero approx_sym [THEN mem_infmal_iff [THEN iffD2]])

   222 lemma SComplex_approx_iff:

   223      "[|x \<in> SComplex; y \<in> SComplex|] ==> (x @= y) = (x = y)"

   224 by (auto simp add: Standard_def)

   226 lemma number_of_Infinitesimal_iff [simp]:

   227      "((number_of w :: hcomplex) \<in> Infinitesimal) =

   228       (number_of w = (0::hcomplex))"

   229 apply (rule iffI)

   230 apply (fast dest: Standard_number_of [THEN SComplex_Infinitesimal_zero])

   231 apply (simp (no_asm_simp))

   232 done

   234 lemma approx_unique_complex:

   235      "[| r \<in> SComplex; s \<in> SComplex; r @= x; s @= x|] ==> r = s"

   236 by (blast intro: SComplex_approx_iff [THEN iffD1] approx_trans2)

   238 subsection {* Properties of @{term hRe}, @{term hIm} and @{term HComplex} *}

   241 lemma abs_hRe_le_hcmod: "\<And>x. \<bar>hRe x\<bar> \<le> hcmod x"

   242 by transfer (rule abs_Re_le_cmod)

   244 lemma abs_hIm_le_hcmod: "\<And>x. \<bar>hIm x\<bar> \<le> hcmod x"

   245 by transfer (rule abs_Im_le_cmod)

   247 lemma Infinitesimal_hRe: "x \<in> Infinitesimal \<Longrightarrow> hRe x \<in> Infinitesimal"

   248 apply (rule InfinitesimalI2, simp)

   249 apply (rule order_le_less_trans [OF abs_hRe_le_hcmod])

   250 apply (erule (1) InfinitesimalD2)

   251 done

   253 lemma Infinitesimal_hIm: "x \<in> Infinitesimal \<Longrightarrow> hIm x \<in> Infinitesimal"

   254 apply (rule InfinitesimalI2, simp)

   255 apply (rule order_le_less_trans [OF abs_hIm_le_hcmod])

   256 apply (erule (1) InfinitesimalD2)

   257 done

   259 lemma real_sqrt_lessI: "\<lbrakk>0 < u; x < u\<twosuperior>\<rbrakk> \<Longrightarrow> sqrt x < u"

   260 (* TODO: this belongs somewhere else *)

   261 by (frule real_sqrt_less_mono) simp

   263 lemma hypreal_sqrt_lessI:

   264   "\<And>x u. \<lbrakk>0 < u; x < u\<twosuperior>\<rbrakk> \<Longrightarrow> ( *f* sqrt) x < u"

   265 by transfer (rule real_sqrt_lessI)

   267 lemma hypreal_sqrt_ge_zero: "\<And>x. 0 \<le> x \<Longrightarrow> 0 \<le> ( *f* sqrt) x"

   268 by transfer (rule real_sqrt_ge_zero)

   270 lemma Infinitesimal_sqrt:

   271   "\<lbrakk>x \<in> Infinitesimal; 0 \<le> x\<rbrakk> \<Longrightarrow> ( *f* sqrt) x \<in> Infinitesimal"

   272 apply (rule InfinitesimalI2)

   273 apply (drule_tac r="r\<twosuperior>" in InfinitesimalD2, simp)

   274 apply (simp add: hypreal_sqrt_ge_zero)

   275 apply (rule hypreal_sqrt_lessI, simp_all)

   276 done

   278 lemma Infinitesimal_HComplex:

   279   "\<lbrakk>x \<in> Infinitesimal; y \<in> Infinitesimal\<rbrakk> \<Longrightarrow> HComplex x y \<in> Infinitesimal"

   280 apply (rule Infinitesimal_hcmod_iff [THEN iffD2])

   281 apply (simp add: hcmod_i)

   282 apply (rule Infinitesimal_add)

   283 apply (erule Infinitesimal_hrealpow, simp)

   284 apply (erule Infinitesimal_hrealpow, simp)

   285 done

   287 lemma hcomplex_Infinitesimal_iff:

   288   "(x \<in> Infinitesimal) = (hRe x \<in> Infinitesimal \<and> hIm x \<in> Infinitesimal)"

   289 apply (safe intro!: Infinitesimal_hRe Infinitesimal_hIm)

   290 apply (drule (1) Infinitesimal_HComplex, simp)

   291 done

   293 lemma hRe_diff [simp]: "\<And>x y. hRe (x - y) = hRe x - hRe y"

   294 by transfer (rule complex_Re_diff)

   296 lemma hIm_diff [simp]: "\<And>x y. hIm (x - y) = hIm x - hIm y"

   297 by transfer (rule complex_Im_diff)

   299 lemma approx_hRe: "x \<approx> y \<Longrightarrow> hRe x \<approx> hRe y"

   300 unfolding approx_def by (drule Infinitesimal_hRe) simp

   302 lemma approx_hIm: "x \<approx> y \<Longrightarrow> hIm x \<approx> hIm y"

   303 unfolding approx_def by (drule Infinitesimal_hIm) simp

   305 lemma approx_HComplex:

   306   "\<lbrakk>a \<approx> b; c \<approx> d\<rbrakk> \<Longrightarrow> HComplex a c \<approx> HComplex b d"

   307 unfolding approx_def by (simp add: Infinitesimal_HComplex)

   309 lemma hcomplex_approx_iff:

   310   "(x \<approx> y) = (hRe x \<approx> hRe y \<and> hIm x \<approx> hIm y)"

   311 unfolding approx_def by (simp add: hcomplex_Infinitesimal_iff)

   313 lemma HFinite_hRe: "x \<in> HFinite \<Longrightarrow> hRe 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_hRe_le_hcmod])

   317 done

   319 lemma HFinite_hIm: "x \<in> HFinite \<Longrightarrow> hIm x \<in> HFinite"

   320 apply (auto simp add: HFinite_def SReal_def)

   321 apply (rule_tac x="star_of r" in exI, simp)

   322 apply (erule order_le_less_trans [OF abs_hIm_le_hcmod])

   323 done

   325 lemma HFinite_HComplex:

   326   "\<lbrakk>x \<in> HFinite; y \<in> HFinite\<rbrakk> \<Longrightarrow> HComplex x y \<in> HFinite"

   327 apply (subgoal_tac "HComplex x 0 + HComplex 0 y \<in> HFinite", simp)

   328 apply (rule HFinite_add)

   329 apply (simp add: HFinite_hcmod_iff hcmod_i)

   330 apply (simp add: HFinite_hcmod_iff hcmod_i)

   331 done

   333 lemma hcomplex_HFinite_iff:

   334   "(x \<in> HFinite) = (hRe x \<in> HFinite \<and> hIm x \<in> HFinite)"

   335 apply (safe intro!: HFinite_hRe HFinite_hIm)

   336 apply (drule (1) HFinite_HComplex, simp)

   337 done

   339 lemma hcomplex_HInfinite_iff:

   340   "(x \<in> HInfinite) = (hRe x \<in> HInfinite \<or> hIm x \<in> HInfinite)"

   341 by (simp add: HInfinite_HFinite_iff hcomplex_HFinite_iff)

   343 lemma hcomplex_of_hypreal_approx_iff [simp]:

   344      "(hcomplex_of_hypreal x @= hcomplex_of_hypreal z) = (x @= z)"

   345 by (simp add: hcomplex_approx_iff)

   347 lemma Standard_HComplex:

   348   "\<lbrakk>x \<in> Standard; y \<in> Standard\<rbrakk> \<Longrightarrow> HComplex x y \<in> Standard"

   349 by (simp add: HComplex_def)

   351 (* Here we go - easy proof now!! *)

   352 lemma stc_part_Ex: "x:HFinite ==> \<exists>t \<in> SComplex. x @= t"

   353 apply (simp add: hcomplex_HFinite_iff hcomplex_approx_iff)

   354 apply (rule_tac x="HComplex (st (hRe x)) (st (hIm x))" in bexI)

   355 apply (simp add: st_approx_self [THEN approx_sym])

   356 apply (simp add: Standard_HComplex st_SReal [unfolded Reals_eq_Standard])

   357 done

   359 lemma stc_part_Ex1: "x:HFinite ==> EX! t. t \<in> SComplex &  x @= t"

   360 apply (drule stc_part_Ex, safe)

   361 apply (drule_tac [2] approx_sym, drule_tac [2] approx_sym, drule_tac [2] approx_sym)

   362 apply (auto intro!: approx_unique_complex)

   363 done

   365 lemmas hcomplex_of_complex_approx_inverse =

   366   hcomplex_of_complex_HFinite_diff_Infinitesimal [THEN [2] approx_inverse]

   369 subsection{*Theorems About Monads*}

   371 lemma monad_zero_hcmod_iff: "(x \<in> monad 0) = (hcmod x:monad 0)"

   372 by (simp add: Infinitesimal_monad_zero_iff [symmetric] Infinitesimal_hcmod_iff)

   375 subsection{*Theorems About Standard Part*}

   377 lemma stc_approx_self: "x \<in> HFinite ==> stc x @= x"

   378 apply (simp add: stc_def)

   379 apply (frule stc_part_Ex, safe)

   380 apply (rule someI2)

   381 apply (auto intro: approx_sym)

   382 done

   384 lemma stc_SComplex: "x \<in> HFinite ==> stc x \<in> SComplex"

   385 apply (simp add: stc_def)

   386 apply (frule stc_part_Ex, safe)

   387 apply (rule someI2)

   388 apply (auto intro: approx_sym)

   389 done

   391 lemma stc_HFinite: "x \<in> HFinite ==> stc x \<in> HFinite"

   392 by (erule stc_SComplex [THEN Standard_subset_HFinite [THEN subsetD]])

   394 lemma stc_unique: "\<lbrakk>y \<in> SComplex; y \<approx> x\<rbrakk> \<Longrightarrow> stc x = y"

   395 apply (frule Standard_subset_HFinite [THEN subsetD])

   396 apply (drule (1) approx_HFinite)

   397 apply (unfold stc_def)

   398 apply (rule some_equality)

   399 apply (auto intro: approx_unique_complex)

   400 done

   402 lemma stc_SComplex_eq [simp]: "x \<in> SComplex ==> stc x = x"

   403 apply (erule stc_unique)

   404 apply (rule approx_refl)

   405 done

   407 lemma stc_hcomplex_of_complex:

   408      "stc (hcomplex_of_complex x) = hcomplex_of_complex x"

   409 by auto

   411 lemma stc_eq_approx:

   412      "[| x \<in> HFinite; y \<in> HFinite; stc x = stc y |] ==> x @= y"

   413 by (auto dest!: stc_approx_self elim!: approx_trans3)

   415 lemma approx_stc_eq:

   416      "[| x \<in> HFinite; y \<in> HFinite; x @= y |] ==> stc x = stc y"

   417 by (blast intro: approx_trans approx_trans2 SComplex_approx_iff [THEN iffD1]

   418           dest: stc_approx_self stc_SComplex)

   420 lemma stc_eq_approx_iff:

   421      "[| x \<in> HFinite; y \<in> HFinite|] ==> (x @= y) = (stc x = stc y)"

   422 by (blast intro: approx_stc_eq stc_eq_approx)

   424 lemma stc_Infinitesimal_add_SComplex:

   425      "[| x \<in> SComplex; e \<in> Infinitesimal |] ==> stc(x + e) = x"

   426 apply (erule stc_unique)

   427 apply (erule Infinitesimal_add_approx_self)

   428 done

   430 lemma stc_Infinitesimal_add_SComplex2:

   431      "[| x \<in> SComplex; e \<in> Infinitesimal |] ==> stc(e + x) = x"

   432 apply (erule stc_unique)

   433 apply (erule Infinitesimal_add_approx_self2)

   434 done

   436 lemma HFinite_stc_Infinitesimal_add:

   437      "x \<in> HFinite ==> \<exists>e \<in> Infinitesimal. x = stc(x) + e"

   438 by (blast dest!: stc_approx_self [THEN approx_sym] bex_Infinitesimal_iff2 [THEN iffD2])

   440 lemma stc_add:

   441      "[| x \<in> HFinite; y \<in> HFinite |] ==> stc (x + y) = stc(x) + stc(y)"

   442 by (simp add: stc_unique stc_SComplex stc_approx_self approx_add)

   444 lemma stc_number_of [simp]: "stc (number_of w) = number_of w"

   445 by (rule Standard_number_of [THEN stc_SComplex_eq])

   447 lemma stc_zero [simp]: "stc 0 = 0"

   448 by simp

   450 lemma stc_one [simp]: "stc 1 = 1"

   451 by simp

   453 lemma stc_minus: "y \<in> HFinite ==> stc(-y) = -stc(y)"

   454 by (simp add: stc_unique stc_SComplex stc_approx_self approx_minus)

   456 lemma stc_diff:

   457      "[| x \<in> HFinite; y \<in> HFinite |] ==> stc (x-y) = stc(x) - stc(y)"

   458 by (simp add: stc_unique stc_SComplex stc_approx_self approx_diff)

   460 lemma stc_mult:

   461      "[| x \<in> HFinite; y \<in> HFinite |]

   462                ==> stc (x * y) = stc(x) * stc(y)"

   463 by (simp add: stc_unique stc_SComplex stc_approx_self approx_mult_HFinite)

   465 lemma stc_Infinitesimal: "x \<in> Infinitesimal ==> stc x = 0"

   466 by (simp add: stc_unique mem_infmal_iff)

   468 lemma stc_not_Infinitesimal: "stc(x) \<noteq> 0 ==> x \<notin> Infinitesimal"

   469 by (fast intro: stc_Infinitesimal)

   471 lemma stc_inverse:

   472      "[| x \<in> HFinite; stc x \<noteq> 0 |]

   473       ==> stc(inverse x) = inverse (stc x)"

   474 apply (drule stc_not_Infinitesimal)

   475 apply (simp add: stc_unique stc_SComplex stc_approx_self approx_inverse)

   476 done

   478 lemma stc_divide [simp]:

   479      "[| x \<in> HFinite; y \<in> HFinite; stc y \<noteq> 0 |]

   480       ==> stc(x/y) = (stc x) / (stc y)"

   481 by (simp add: divide_inverse stc_mult stc_not_Infinitesimal HFinite_inverse stc_inverse)

   483 lemma stc_idempotent [simp]: "x \<in> HFinite ==> stc(stc(x)) = stc(x)"

   484 by (blast intro: stc_HFinite stc_approx_self approx_stc_eq)

   486 lemma HFinite_HFinite_hcomplex_of_hypreal:

   487      "z \<in> HFinite ==> hcomplex_of_hypreal z \<in> HFinite"

   488 by (simp add: hcomplex_HFinite_iff)

   490 lemma SComplex_SReal_hcomplex_of_hypreal:

   491      "x \<in> Reals ==>  hcomplex_of_hypreal x \<in> SComplex"

   492 apply (rule Standard_of_hypreal)

   493 apply (simp add: Reals_eq_Standard)

   494 done

   496 lemma stc_hcomplex_of_hypreal:

   497  "z \<in> HFinite ==> stc(hcomplex_of_hypreal z) = hcomplex_of_hypreal (st z)"

   498 apply (rule stc_unique)

   499 apply (rule SComplex_SReal_hcomplex_of_hypreal)

   500 apply (erule st_SReal)

   501 apply (simp add: hcomplex_of_hypreal_approx_iff st_approx_self)

   502 done

   504 (*

   505 Goal "x \<in> HFinite ==> hcmod(stc x) = st(hcmod x)"

   506 by (dtac stc_approx_self 1)

   507 by (auto_tac (claset(),simpset() addsimps [bex_Infinitesimal_iff2 RS sym]));

   510 approx_hcmod_add_hcmod

   511 *)

   513 lemma Infinitesimal_hcnj_iff [simp]:

   514      "(hcnj z \<in> Infinitesimal) = (z \<in> Infinitesimal)"

   515 by (simp add: Infinitesimal_hcmod_iff)

   517 lemma Infinitesimal_hcomplex_of_hypreal_epsilon [simp]:

   518      "hcomplex_of_hypreal epsilon \<in> Infinitesimal"

   519 by (simp add: Infinitesimal_hcmod_iff)

   521 end

author	huffman
	Mon, 17 May 2010 18:59:59 -0700
changeset 36977	71c8973a604b
parent 28952	15a4b2cf8c34
child 37765	26bdfb7b680b
permissions	-rw-r--r--