src/HOL/Complex/CStar.thy
author nipkow
Mon Aug 16 14:22:27 2004 +0200 (2004-08-16)
changeset 15131 c69542757a4d
parent 14469 c7674b7034f5
child 15140 322485b816ac
permissions -rw-r--r--
New theory header syntax.
     1 (*  Title       : CStar.thy
     2     Author      : Jacques D. Fleuriot
     3     Copyright   : 2001 University of Edinburgh
     4 *)
     5 
     6 header{*Star-transforms in NSA, Extending Sets of Complex Numbers
     7       and Complex Functions*}
     8 
     9 theory CStar
    10 import NSCA
    11 begin
    12 
    13 constdefs
    14 
    15     (* nonstandard extension of sets *)
    16     starsetC :: "complex set => hcomplex set"          ("*sc* _" [80] 80)
    17     "*sc* A  == {x. \<forall>X \<in> Rep_hcomplex(x). {n. X n \<in> A} \<in> FreeUltrafilterNat}"
    18 
    19     (* internal sets *)
    20     starsetC_n :: "(nat => complex set) => hcomplex set"  ("*scn* _" [80] 80)
    21     "*scn* As  == {x. \<forall>X \<in> Rep_hcomplex(x). 
    22                       {n. X n \<in> (As n)} \<in> FreeUltrafilterNat}"
    23 
    24     InternalCSets :: "hcomplex set set"
    25     "InternalCSets == {X. \<exists>As. X = *scn* As}"
    26 
    27     (* star transform of functions f: Complex --> Complex *)
    28 
    29     starfunC :: "(complex => complex) => hcomplex => hcomplex"
    30                 ("*fc* _" [80] 80)
    31     "*fc* f  == 
    32         (%x. Abs_hcomplex(\<Union>X \<in> Rep_hcomplex(x). hcomplexrel``{%n. f (X n)}))"
    33 
    34     starfunC_n :: "(nat => (complex => complex)) => hcomplex => hcomplex"
    35                   ("*fcn* _" [80] 80)
    36     "*fcn* F  == 
    37       (%x. Abs_hcomplex(\<Union>X \<in> Rep_hcomplex(x). hcomplexrel``{%n. (F n)(X n)}))"
    38 
    39     InternalCFuns :: "(hcomplex => hcomplex) set"
    40     "InternalCFuns == {X. \<exists>F. X = *fcn* F}"
    41 
    42 
    43     (* star transform of functions f: Real --> Complex *)
    44 
    45     starfunRC :: "(real => complex) => hypreal => hcomplex"
    46                  ("*fRc* _" [80] 80)
    47     "*fRc* f  == (%x. Abs_hcomplex(\<Union>X \<in> Rep_hypreal(x). hcomplexrel``{%n. f (X n)}))"
    48 
    49     starfunRC_n :: "(nat => (real => complex)) => hypreal => hcomplex"
    50                    ("*fRcn* _" [80] 80)
    51     "*fRcn* F  == (%x. Abs_hcomplex(\<Union>X \<in> Rep_hypreal(x). hcomplexrel``{%n. (F n)(X n)}))"
    52 
    53     InternalRCFuns :: "(hypreal => hcomplex) set"
    54     "InternalRCFuns == {X. \<exists>F. X = *fRcn* F}"
    55 
    56     (* star transform of functions f: Complex --> Real; needed for Re and Im parts *)
    57 
    58     starfunCR :: "(complex => real) => hcomplex => hypreal"
    59                  ("*fcR* _" [80] 80)
    60     "*fcR* f  == (%x. Abs_hypreal(\<Union>X \<in> Rep_hcomplex(x). hyprel``{%n. f (X n)}))"
    61 
    62     starfunCR_n :: "(nat => (complex => real)) => hcomplex => hypreal"
    63                    ("*fcRn* _" [80] 80)
    64     "*fcRn* F  == (%x. Abs_hypreal(\<Union>X \<in> Rep_hcomplex(x). hyprel``{%n. (F n)(X n)}))"
    65 
    66     InternalCRFuns :: "(hcomplex => hypreal) set"
    67     "InternalCRFuns == {X. \<exists>F. X = *fcRn* F}"
    68 
    69 
    70 subsection{*Properties of the *-Transform Applied to Sets of Reals*}
    71 
    72 lemma STARC_complex_set [simp]: "*sc*(UNIV::complex set) = (UNIV)"
    73 by (simp add: starsetC_def)
    74 declare STARC_complex_set
    75 
    76 lemma STARC_empty_set: "*sc* {} = {}"
    77 by (simp add: starsetC_def)
    78 declare STARC_empty_set [simp]
    79 
    80 lemma STARC_Un: "*sc* (A Un B) = *sc* A Un *sc* B"
    81 apply (auto simp add: starsetC_def)
    82 apply (drule bspec, assumption)
    83 apply (rule_tac z = x in eq_Abs_hcomplex, simp, ultra)
    84 apply (blast intro: FreeUltrafilterNat_subset)+
    85 done
    86 
    87 lemma starsetC_n_Un: "*scn* (%n. (A n) Un (B n)) = *scn* A Un *scn* B"
    88 apply (auto simp add: starsetC_n_def)
    89 apply (drule_tac x = Xa in bspec)
    90 apply (rule_tac [2] z = x in eq_Abs_hcomplex)
    91 apply (auto dest!: bspec, ultra+)
    92 done
    93 
    94 lemma InternalCSets_Un:
    95      "[| X \<in> InternalCSets; Y \<in> InternalCSets |] ==> (X Un Y) \<in> InternalCSets"
    96 by (auto simp add:  InternalCSets_def starsetC_n_Un [symmetric])
    97 
    98 lemma STARC_Int: "*sc* (A Int B) = *sc* A Int *sc* B"
    99 apply (auto simp add: starsetC_def)
   100 prefer 3 apply (blast intro: FreeUltrafilterNat_Int FreeUltrafilterNat_subset)
   101 apply (blast intro: FreeUltrafilterNat_subset)+
   102 done
   103 
   104 lemma starsetC_n_Int: "*scn* (%n. (A n) Int (B n)) = *scn* A Int *scn* B"
   105 apply (auto simp add: starsetC_n_def)
   106 apply (auto dest!: bspec, ultra+)
   107 done
   108 
   109 lemma InternalCSets_Int:
   110     "[| X \<in> InternalCSets; Y \<in> InternalCSets |] ==> (X Int Y) \<in> InternalCSets"
   111 by (auto simp add: InternalCSets_def starsetC_n_Int [symmetric])
   112 
   113 lemma STARC_Compl: "*sc* -A = -( *sc* A)"
   114 apply (auto simp add: starsetC_def)
   115 apply (rule_tac z = x in eq_Abs_hcomplex)
   116 apply (rule_tac [2] z = x in eq_Abs_hcomplex)
   117 apply (auto dest!: bspec, ultra+)
   118 done
   119 
   120 lemma starsetC_n_Compl: "*scn* ((%n. - A n)) = -( *scn* A)"
   121 apply (auto simp add: starsetC_n_def)
   122 apply (rule_tac z = x in eq_Abs_hcomplex)
   123 apply (rule_tac [2] z = x in eq_Abs_hcomplex)
   124 apply (auto dest!: bspec, ultra+)
   125 done
   126 
   127 lemma InternalCSets_Compl: "X :InternalCSets ==> -X \<in> InternalCSets"
   128 by (auto simp add: InternalCSets_def starsetC_n_Compl [symmetric])
   129 
   130 lemma STARC_mem_Compl: "x \<notin> *sc* F ==> x \<in> *sc* (- F)"
   131 by (simp add: STARC_Compl)
   132 
   133 lemma STARC_diff: "*sc* (A - B) = *sc* A - *sc* B"
   134 by (simp add: Diff_eq STARC_Int STARC_Compl)
   135 
   136 lemma starsetC_n_diff:
   137       "*scn* (%n. (A n) - (B n)) = *scn* A - *scn* B"
   138 apply (auto simp add: starsetC_n_def)
   139 apply (rule_tac [2] z = x in eq_Abs_hcomplex)
   140 apply (rule_tac [3] z = x in eq_Abs_hcomplex)
   141 apply (auto dest!: bspec, ultra+)
   142 done
   143 
   144 lemma InternalCSets_diff:
   145      "[| X \<in> InternalCSets; Y \<in> InternalCSets |] ==> (X - Y) \<in> InternalCSets"
   146 by (auto simp add: InternalCSets_def starsetC_n_diff [symmetric])
   147 
   148 lemma STARC_subset: "A \<le> B ==> *sc* A \<le> *sc* B"
   149 apply (simp add: starsetC_def)
   150 apply (blast intro: FreeUltrafilterNat_subset)+
   151 done
   152 
   153 lemma STARC_mem: "a \<in> A ==> hcomplex_of_complex a \<in> *sc* A"
   154 apply (simp add: starsetC_def hcomplex_of_complex_def)
   155 apply (auto intro: FreeUltrafilterNat_subset)
   156 done
   157 
   158 lemma STARC_hcomplex_of_complex_image_subset:
   159     "hcomplex_of_complex ` A \<le> *sc* A"
   160 apply (auto simp add: starsetC_def hcomplex_of_complex_def)
   161 apply (blast intro: FreeUltrafilterNat_subset)
   162 done
   163 
   164 lemma STARC_SComplex_subset: "SComplex \<le> *sc* (UNIV:: complex set)"
   165 by auto
   166 
   167 lemma STARC_hcomplex_of_complex_Int:
   168      "*sc* X Int SComplex = hcomplex_of_complex ` X"
   169 apply (auto simp add: starsetC_def hcomplex_of_complex_def SComplex_def)
   170 apply (fold hcomplex_of_complex_def)
   171 apply (rule imageI, rule ccontr)
   172 apply (drule bspec)
   173 apply (rule lemma_hcomplexrel_refl)
   174 prefer 2 apply (blast intro: FreeUltrafilterNat_subset, auto)
   175 done
   176 
   177 lemma lemma_not_hcomplexA:
   178      "x \<notin> hcomplex_of_complex ` A ==> \<forall>y \<in> A. x \<noteq> hcomplex_of_complex y"
   179 by auto
   180 
   181 lemma starsetC_starsetC_n_eq: "*sc* X = *scn* (%n. X)"
   182 by (simp add: starsetC_n_def starsetC_def)
   183 
   184 lemma InternalCSets_starsetC_n [simp]: "( *sc* X) \<in> InternalCSets"
   185 by (auto simp add: InternalCSets_def starsetC_starsetC_n_eq)
   186 
   187 lemma InternalCSets_UNIV_diff:
   188     "X \<in> InternalCSets ==> UNIV - X \<in> InternalCSets"
   189 by (auto intro: InternalCSets_Compl)
   190 
   191 text{*Nonstandard extension of a set (defined using a constant sequence) as a special case of an internal set*}
   192 
   193 lemma starsetC_n_starsetC: "\<forall>n. (As n = A) ==> *scn* As = *sc* A"
   194 by (simp add:starsetC_n_def starsetC_def)
   195 
   196 
   197 subsection{*Theorems about Nonstandard Extensions of Functions*}
   198 
   199 lemma starfunC_n_starfunC: "\<forall>n. (F n = f) ==> *fcn* F = *fc* f"
   200 by (simp add: starfunC_n_def starfunC_def)
   201 
   202 lemma starfunRC_n_starfunRC: "\<forall>n. (F n = f) ==> *fRcn* F = *fRc* f"
   203 by (simp add: starfunRC_n_def starfunRC_def)
   204 
   205 lemma starfunCR_n_starfunCR: "\<forall>n. (F n = f) ==> *fcRn* F = *fcR* f"
   206 by (simp add: starfunCR_n_def starfunCR_def)
   207 
   208 lemma starfunC_congruent:
   209       "congruent hcomplexrel (%X. hcomplexrel``{%n. f (X n)})"
   210 apply (auto simp add: hcomplexrel_iff congruent_def, ultra)
   211 done
   212 
   213 (* f::complex => complex *)
   214 lemma starfunC:
   215       "( *fc* f) (Abs_hcomplex(hcomplexrel``{%n. X n})) =
   216        Abs_hcomplex(hcomplexrel `` {%n. f (X n)})"
   217 apply (simp add: starfunC_def)
   218 apply (rule arg_cong [where f = Abs_hcomplex])
   219 apply (auto iff add: hcomplexrel_iff, ultra)
   220 done
   221 
   222 lemma starfunRC:
   223       "( *fRc* f) (Abs_hypreal(hyprel``{%n. X n})) =
   224        Abs_hcomplex(hcomplexrel `` {%n. f (X n)})"
   225 apply (simp add: starfunRC_def)
   226 apply (rule arg_cong [where f = Abs_hcomplex], auto, ultra)
   227 done
   228 
   229 lemma starfunCR:
   230       "( *fcR* f) (Abs_hcomplex(hcomplexrel``{%n. X n})) =
   231        Abs_hypreal(hyprel `` {%n. f (X n)})"
   232 apply (simp add: starfunCR_def)
   233 apply (rule arg_cong [where f = Abs_hypreal])
   234 apply (auto iff add: hcomplexrel_iff, ultra)
   235 done
   236 
   237 (**  multiplication: ( *f) x ( *g) = *(f x g) **)
   238 
   239 lemma starfunC_mult: "( *fc* f) z * ( *fc* g) z = ( *fc* (%x. f x * g x)) z"
   240 apply (rule_tac z = z in eq_Abs_hcomplex)
   241 apply (auto simp add: starfunC hcomplex_mult)
   242 done
   243 declare starfunC_mult [symmetric, simp]
   244 
   245 lemma starfunRC_mult:
   246     "( *fRc* f) z * ( *fRc* g) z = ( *fRc* (%x. f x * g x)) z"
   247 apply (cases z)
   248 apply (simp add: starfunRC hcomplex_mult)
   249 done
   250 declare starfunRC_mult [symmetric, simp]
   251 
   252 lemma starfunCR_mult:
   253     "( *fcR* f) z * ( *fcR* g) z = ( *fcR* (%x. f x * g x)) z"
   254 apply (rule_tac z = z in eq_Abs_hcomplex)
   255 apply (simp add: starfunCR hypreal_mult)
   256 done
   257 declare starfunCR_mult [symmetric, simp]
   258 
   259 (**  addition: ( *f) + ( *g) = *(f + g)  **)
   260 
   261 lemma starfunC_add: "( *fc* f) z + ( *fc* g) z = ( *fc* (%x. f x + g x)) z"
   262 apply (rule_tac z = z in eq_Abs_hcomplex)
   263 apply (simp add: starfunC hcomplex_add)
   264 done
   265 declare starfunC_add [symmetric, simp]
   266 
   267 lemma starfunRC_add: "( *fRc* f) z + ( *fRc* g) z = ( *fRc* (%x. f x + g x)) z"
   268 apply (cases z)
   269 apply (simp add: starfunRC hcomplex_add)
   270 done
   271 declare starfunRC_add [symmetric, simp]
   272 
   273 lemma starfunCR_add: "( *fcR* f) z + ( *fcR* g) z = ( *fcR* (%x. f x + g x)) z"
   274 apply (rule_tac z = z in eq_Abs_hcomplex)
   275 apply (simp add: starfunCR hypreal_add)
   276 done
   277 declare starfunCR_add [symmetric, simp]
   278 
   279 (**  uminus **)
   280 lemma starfunC_minus [simp]: "( *fc* (%x. - f x)) x = - ( *fc* f) x"
   281 apply (rule_tac z = x in eq_Abs_hcomplex)
   282 apply (simp add: starfunC hcomplex_minus)
   283 done
   284 
   285 lemma starfunRC_minus [simp]: "( *fRc* (%x. - f x)) x = - ( *fRc* f) x"
   286 apply (cases x)
   287 apply (simp add: starfunRC hcomplex_minus)
   288 done
   289 
   290 lemma starfunCR_minus [simp]: "( *fcR* (%x. - f x)) x = - ( *fcR* f) x"
   291 apply (rule_tac z = x in eq_Abs_hcomplex)
   292 apply (simp add: starfunCR hypreal_minus)
   293 done
   294 
   295 (**  addition: ( *f) - ( *g) = *(f - g)  **)
   296 
   297 lemma starfunC_diff: "( *fc* f) y  - ( *fc* g) y = ( *fc* (%x. f x - g x)) y"
   298 by (simp add: diff_minus)
   299 declare starfunC_diff [symmetric, simp]
   300 
   301 lemma starfunRC_diff:
   302     "( *fRc* f) y  - ( *fRc* g) y = ( *fRc* (%x. f x - g x)) y"
   303 by (simp add: diff_minus)
   304 declare starfunRC_diff [symmetric, simp]
   305 
   306 lemma starfunCR_diff:
   307   "( *fcR* f) y  - ( *fcR* g) y = ( *fcR* (%x. f x - g x)) y"
   308 by (simp add: diff_minus)
   309 declare starfunCR_diff [symmetric, simp]
   310 
   311 (**  composition: ( *f) o ( *g) = *(f o g) **)
   312 
   313 lemma starfunC_o2: "(%x. ( *fc* f) (( *fc* g) x)) = *fc* (%x. f (g x))"
   314 apply (rule ext)
   315 apply (rule_tac z = x in eq_Abs_hcomplex)
   316 apply (simp add: starfunC)
   317 done
   318 
   319 lemma starfunC_o: "( *fc* f) o ( *fc* g) = ( *fc* (f o g))"
   320 by (simp add: o_def starfunC_o2)
   321 
   322 lemma starfunC_starfunRC_o2:
   323     "(%x. ( *fc* f) (( *fRc* g) x)) = *fRc* (%x. f (g x))"
   324 apply (rule ext)
   325 apply (rule_tac z = x in eq_Abs_hypreal)
   326 apply (simp add: starfunRC starfunC)
   327 done
   328 
   329 lemma starfun_starfunCR_o2:
   330     "(%x. ( *f* f) (( *fcR* g) x)) = *fcR* (%x. f (g x))"
   331 apply (rule ext)
   332 apply (rule_tac z = x in eq_Abs_hcomplex)
   333 apply (simp add: starfunCR starfun)
   334 done
   335 
   336 lemma starfunC_starfunRC_o: "( *fc* f) o ( *fRc* g) = ( *fRc* (f o g))"
   337 by (simp add: o_def starfunC_starfunRC_o2)
   338 
   339 lemma starfun_starfunCR_o: "( *f* f) o ( *fcR* g) = ( *fcR* (f o g))"
   340 by (simp add: o_def starfun_starfunCR_o2)
   341 
   342 lemma starfunC_const_fun [simp]: "( *fc* (%x. k)) z = hcomplex_of_complex k"
   343 apply (cases z)
   344 apply (simp add: starfunC hcomplex_of_complex_def)
   345 done
   346 
   347 lemma starfunRC_const_fun [simp]: "( *fRc* (%x. k)) z = hcomplex_of_complex k"
   348 apply (cases z)
   349 apply (simp add: starfunRC hcomplex_of_complex_def)
   350 done
   351 
   352 lemma starfunCR_const_fun [simp]: "( *fcR* (%x. k)) z = hypreal_of_real k"
   353 apply (cases z)
   354 apply (simp add: starfunCR hypreal_of_real_def)
   355 done
   356 
   357 lemma starfunC_inverse: "inverse (( *fc* f) x) = ( *fc* (%x. inverse (f x))) x"
   358 apply (cases x)
   359 apply (simp add: starfunC hcomplex_inverse)
   360 done
   361 declare starfunC_inverse [symmetric, simp]
   362 
   363 lemma starfunRC_inverse:
   364     "inverse (( *fRc* f) x) = ( *fRc* (%x. inverse (f x))) x"
   365 apply (cases x)
   366 apply (simp add: starfunRC hcomplex_inverse)
   367 done
   368 declare starfunRC_inverse [symmetric, simp]
   369 
   370 lemma starfunCR_inverse:
   371     "inverse (( *fcR* f) x) = ( *fcR* (%x. inverse (f x))) x"
   372 apply (cases x)
   373 apply (simp add: starfunCR hypreal_inverse)
   374 done
   375 declare starfunCR_inverse [symmetric, simp]
   376 
   377 lemma starfunC_eq [simp]:
   378     "( *fc* f) (hcomplex_of_complex a) = hcomplex_of_complex (f a)"
   379 by (simp add: starfunC hcomplex_of_complex_def)
   380 
   381 lemma starfunRC_eq [simp]:
   382     "( *fRc* f) (hypreal_of_real a) = hcomplex_of_complex (f a)"
   383 by (simp add: starfunRC hcomplex_of_complex_def hypreal_of_real_def)
   384 
   385 lemma starfunCR_eq [simp]:
   386     "( *fcR* f) (hcomplex_of_complex a) = hypreal_of_real (f a)"
   387 by (simp add: starfunCR hcomplex_of_complex_def hypreal_of_real_def)
   388 
   389 lemma starfunC_capprox:
   390     "( *fc* f) (hcomplex_of_complex a) @c= hcomplex_of_complex (f a)"
   391 by auto
   392 
   393 lemma starfunRC_capprox:
   394     "( *fRc* f) (hypreal_of_real a) @c= hcomplex_of_complex (f a)"
   395 by auto
   396 
   397 lemma starfunCR_approx:
   398     "( *fcR* f) (hcomplex_of_complex a) @= hypreal_of_real (f a)"
   399 by auto
   400 
   401 (*
   402 Goal "( *fcNat* (%n. z ^ n)) N = (hcomplex_of_complex z) hcpow N"
   403 *)
   404 
   405 lemma starfunC_hcpow: "( *fc* (%z. z ^ n)) Z = Z hcpow hypnat_of_nat n"
   406 apply (cases Z)
   407 apply (simp add: hcpow starfunC hypnat_of_nat_eq)
   408 done
   409 
   410 lemma starfunC_lambda_cancel:
   411     "( *fc* (%h. f (x + h))) y  = ( *fc* f) (hcomplex_of_complex  x + y)"
   412 apply (cases y)
   413 apply (simp add: starfunC hcomplex_of_complex_def hcomplex_add)
   414 done
   415 
   416 lemma starfunCR_lambda_cancel:
   417     "( *fcR* (%h. f (x + h))) y  = ( *fcR* f) (hcomplex_of_complex  x + y)"
   418 apply (cases y)
   419 apply (simp add: starfunCR hcomplex_of_complex_def hcomplex_add)
   420 done
   421 
   422 lemma starfunRC_lambda_cancel:
   423     "( *fRc* (%h. f (x + h))) y  = ( *fRc* f) (hypreal_of_real x + y)"
   424 apply (cases y)
   425 apply (simp add: starfunRC hypreal_of_real_def hypreal_add)
   426 done
   427 
   428 lemma starfunC_lambda_cancel2:
   429     "( *fc* (%h. f(g(x + h)))) y = ( *fc* (f o g)) (hcomplex_of_complex x + y)"
   430 apply (cases y)
   431 apply (simp add: starfunC hcomplex_of_complex_def hcomplex_add)
   432 done
   433 
   434 lemma starfunCR_lambda_cancel2:
   435     "( *fcR* (%h. f(g(x + h)))) y = ( *fcR* (f o g)) (hcomplex_of_complex x + y)"
   436 apply (cases y)
   437 apply (simp add: starfunCR hcomplex_of_complex_def hcomplex_add)
   438 done
   439 
   440 lemma starfunRC_lambda_cancel2:
   441     "( *fRc* (%h. f(g(x + h)))) y = ( *fRc* (f o g)) (hypreal_of_real x + y)"
   442 apply (cases y)
   443 apply (simp add: starfunRC hypreal_of_real_def hypreal_add)
   444 done
   445 
   446 lemma starfunC_mult_CFinite_capprox:
   447     "[| ( *fc* f) y @c= l; ( *fc* g) y @c= m; l: CFinite; m: CFinite |]
   448      ==>  ( *fc* (%x. f x * g x)) y @c= l * m"
   449 apply (drule capprox_mult_CFinite, assumption+)
   450 apply (auto intro: capprox_sym [THEN [2] capprox_CFinite])
   451 done
   452 
   453 lemma starfunCR_mult_HFinite_capprox:
   454     "[| ( *fcR* f) y @= l; ( *fcR* g) y @= m; l: HFinite; m: HFinite |]
   455      ==>  ( *fcR* (%x. f x * g x)) y @= l * m"
   456 apply (drule approx_mult_HFinite, assumption+)
   457 apply (auto intro: approx_sym [THEN [2] approx_HFinite])
   458 done
   459 
   460 lemma starfunRC_mult_CFinite_capprox:
   461     "[| ( *fRc* f) y @c= l; ( *fRc* g) y @c= m; l: CFinite; m: CFinite |]
   462      ==>  ( *fRc* (%x. f x * g x)) y @c= l * m"
   463 apply (drule capprox_mult_CFinite, assumption+)
   464 apply (auto intro: capprox_sym [THEN [2] capprox_CFinite])
   465 done
   466 
   467 lemma starfunC_add_capprox:
   468     "[| ( *fc* f) y @c= l; ( *fc* g) y @c= m |]
   469      ==>  ( *fc* (%x. f x + g x)) y @c= l + m"
   470 by (auto intro: capprox_add)
   471 
   472 lemma starfunRC_add_capprox:
   473     "[| ( *fRc* f) y @c= l; ( *fRc* g) y @c= m |]
   474      ==>  ( *fRc* (%x. f x + g x)) y @c= l + m"
   475 by (auto intro: capprox_add)
   476 
   477 lemma starfunCR_add_approx:
   478     "[| ( *fcR* f) y @= l; ( *fcR* g) y @= m
   479                |] ==>  ( *fcR* (%x. f x + g x)) y @= l + m"
   480 by (auto intro: approx_add)
   481 
   482 lemma starfunCR_cmod: "*fcR* cmod = hcmod"
   483 apply (rule ext)
   484 apply (rule_tac z = x in eq_Abs_hcomplex)
   485 apply (simp add: starfunCR hcmod)
   486 done
   487 
   488 lemma starfunC_inverse_inverse: "( *fc* inverse) x = inverse(x)"
   489 apply (cases x)
   490 apply (simp add: starfunC hcomplex_inverse)
   491 done
   492 
   493 lemma starfunC_divide: "( *fc* f) y  / ( *fc* g) y = ( *fc* (%x. f x / g x)) y"
   494 by (simp add: divide_inverse)
   495 declare starfunC_divide [symmetric, simp]
   496 
   497 lemma starfunCR_divide:
   498   "( *fcR* f) y  / ( *fcR* g) y = ( *fcR* (%x. f x / g x)) y"
   499 by (simp add: divide_inverse)
   500 declare starfunCR_divide [symmetric, simp]
   501 
   502 lemma starfunRC_divide:
   503   "( *fRc* f) y  / ( *fRc* g) y = ( *fRc* (%x. f x / g x)) y"
   504 by (simp add: divide_inverse)
   505 declare starfunRC_divide [symmetric, simp]
   506 
   507 
   508 subsection{*Internal Functions - Some Redundancy With *Fc* Now*}
   509 
   510 lemma starfunC_n_congruent:
   511       "congruent hcomplexrel (%X. hcomplexrel``{%n. f n (X n)})"
   512 by (auto simp add: congruent_def hcomplexrel_iff, ultra)
   513 
   514 lemma starfunC_n:
   515      "( *fcn* f) (Abs_hcomplex(hcomplexrel``{%n. X n})) =
   516       Abs_hcomplex(hcomplexrel `` {%n. f n (X n)})"
   517 apply (simp add: starfunC_n_def)
   518 apply (rule arg_cong [where f = Abs_hcomplex])
   519 apply (auto iff add: hcomplexrel_iff, ultra)
   520 done
   521 
   522 (**  multiplication: ( *fn) x ( *gn) = *(fn x gn) **)
   523 
   524 lemma starfunC_n_mult:
   525     "( *fcn* f) z * ( *fcn* g) z = ( *fcn* (% i x. f i x * g i x)) z"
   526 apply (cases z)
   527 apply (simp add: starfunC_n hcomplex_mult)
   528 done
   529 
   530 (**  addition: ( *fn) + ( *gn) = *(fn + gn) **)
   531 
   532 lemma starfunC_n_add:
   533     "( *fcn* f) z + ( *fcn* g) z = ( *fcn* (%i x. f i x + g i x)) z"
   534 apply (cases z)
   535 apply (simp add: starfunC_n hcomplex_add)
   536 done
   537 
   538 (** uminus **)
   539 
   540 lemma starfunC_n_minus: "- ( *fcn* g) z = ( *fcn* (%i x. - g i x)) z"
   541 apply (cases z)
   542 apply (simp add: starfunC_n hcomplex_minus)
   543 done
   544 
   545 (** subtraction: ( *fn) - ( *gn) = *(fn - gn) **)
   546 
   547 lemma starfunNat_n_diff:
   548    "( *fcn* f) z - ( *fcn* g) z = ( *fcn* (%i x. f i x - g i x)) z"
   549 by (simp add: diff_minus  starfunC_n_add starfunC_n_minus)
   550 
   551 (** composition: ( *fn) o ( *gn) = *(fn o gn) **)
   552 
   553 lemma starfunC_n_const_fun [simp]:
   554      "( *fcn* (%i x. k)) z = hcomplex_of_complex  k"
   555 apply (cases z)
   556 apply (simp add: starfunC_n hcomplex_of_complex_def)
   557 done
   558 
   559 lemma starfunC_n_eq [simp]:
   560     "( *fcn* f) (hcomplex_of_complex n) = Abs_hcomplex(hcomplexrel `` {%i. f i n})"
   561 by (simp add: starfunC_n hcomplex_of_complex_def)
   562 
   563 lemma starfunC_eq_iff: "(( *fc* f) = ( *fc* g)) = (f = g)"
   564 apply auto
   565 apply (rule ext, rule ccontr)
   566 apply (drule_tac x = "hcomplex_of_complex (x) " in fun_cong)
   567 apply (simp add: starfunC hcomplex_of_complex_def)
   568 done
   569 
   570 lemma starfunRC_eq_iff: "(( *fRc* f) = ( *fRc* g)) = (f = g)"
   571 apply auto
   572 apply (rule ext, rule ccontr)
   573 apply (drule_tac x = "hypreal_of_real (x) " in fun_cong)
   574 apply auto
   575 done
   576 
   577 lemma starfunCR_eq_iff: "(( *fcR* f) = ( *fcR* g)) = (f = g)"
   578 apply auto
   579 apply (rule ext, rule ccontr)
   580 apply (drule_tac x = "hcomplex_of_complex (x) " in fun_cong)
   581 apply auto
   582 done
   583 
   584 lemma starfunC_eq_Re_Im_iff:
   585     "(( *fc* f) x = z) = ((( *fcR* (%x. Re(f x))) x = hRe (z)) &
   586                           (( *fcR* (%x. Im(f x))) x = hIm (z)))"
   587 apply (cases x, cases z)
   588 apply (auto simp add: starfunCR starfunC hIm hRe complex_Re_Im_cancel_iff, ultra+)
   589 done
   590 
   591 lemma starfunC_approx_Re_Im_iff:
   592     "(( *fc* f) x @c= z) = ((( *fcR* (%x. Re(f x))) x @= hRe (z)) &
   593                             (( *fcR* (%x. Im(f x))) x @= hIm (z)))"
   594 apply (cases x, cases z)
   595 apply (simp add: starfunCR starfunC hIm hRe capprox_approx_iff)
   596 done
   597 
   598 lemma starfunC_Idfun_capprox:
   599     "x @c= hcomplex_of_complex a ==> ( *fc* (%x. x)) x @c= hcomplex_of_complex  a"
   600 apply (cases x)
   601 apply (simp add: starfunC)
   602 done
   603 
   604 lemma starfunC_Id [simp]: "( *fc* (%x. x)) x = x"
   605 apply (cases x)
   606 apply (simp add: starfunC)
   607 done
   608 
   609 ML
   610 {*
   611 val STARC_complex_set = thm "STARC_complex_set";
   612 val STARC_empty_set = thm "STARC_empty_set";
   613 val STARC_Un = thm "STARC_Un";
   614 val starsetC_n_Un = thm "starsetC_n_Un";
   615 val InternalCSets_Un = thm "InternalCSets_Un";
   616 val STARC_Int = thm "STARC_Int";
   617 val starsetC_n_Int = thm "starsetC_n_Int";
   618 val InternalCSets_Int = thm "InternalCSets_Int";
   619 val STARC_Compl = thm "STARC_Compl";
   620 val starsetC_n_Compl = thm "starsetC_n_Compl";
   621 val InternalCSets_Compl = thm "InternalCSets_Compl";
   622 val STARC_mem_Compl = thm "STARC_mem_Compl";
   623 val STARC_diff = thm "STARC_diff";
   624 val starsetC_n_diff = thm "starsetC_n_diff";
   625 val InternalCSets_diff = thm "InternalCSets_diff";
   626 val STARC_subset = thm "STARC_subset";
   627 val STARC_mem = thm "STARC_mem";
   628 val STARC_hcomplex_of_complex_image_subset = thm "STARC_hcomplex_of_complex_image_subset";
   629 val STARC_SComplex_subset = thm "STARC_SComplex_subset";
   630 val STARC_hcomplex_of_complex_Int = thm "STARC_hcomplex_of_complex_Int";
   631 val lemma_not_hcomplexA = thm "lemma_not_hcomplexA";
   632 val starsetC_starsetC_n_eq = thm "starsetC_starsetC_n_eq";
   633 val InternalCSets_starsetC_n = thm "InternalCSets_starsetC_n";
   634 val InternalCSets_UNIV_diff = thm "InternalCSets_UNIV_diff";
   635 val starsetC_n_starsetC = thm "starsetC_n_starsetC";
   636 val starfunC_n_starfunC = thm "starfunC_n_starfunC";
   637 val starfunRC_n_starfunRC = thm "starfunRC_n_starfunRC";
   638 val starfunCR_n_starfunCR = thm "starfunCR_n_starfunCR";
   639 val starfunC_congruent = thm "starfunC_congruent";
   640 val starfunC = thm "starfunC";
   641 val starfunRC = thm "starfunRC";
   642 val starfunCR = thm "starfunCR";
   643 val starfunC_mult = thm "starfunC_mult";
   644 val starfunRC_mult = thm "starfunRC_mult";
   645 val starfunCR_mult = thm "starfunCR_mult";
   646 val starfunC_add = thm "starfunC_add";
   647 val starfunRC_add = thm "starfunRC_add";
   648 val starfunCR_add = thm "starfunCR_add";
   649 val starfunC_minus = thm "starfunC_minus";
   650 val starfunRC_minus = thm "starfunRC_minus";
   651 val starfunCR_minus = thm "starfunCR_minus";
   652 val starfunC_diff = thm "starfunC_diff";
   653 val starfunRC_diff = thm "starfunRC_diff";
   654 val starfunCR_diff = thm "starfunCR_diff";
   655 val starfunC_o2 = thm "starfunC_o2";
   656 val starfunC_o = thm "starfunC_o";
   657 val starfunC_starfunRC_o2 = thm "starfunC_starfunRC_o2";
   658 val starfun_starfunCR_o2 = thm "starfun_starfunCR_o2";
   659 val starfunC_starfunRC_o = thm "starfunC_starfunRC_o";
   660 val starfun_starfunCR_o = thm "starfun_starfunCR_o";
   661 val starfunC_const_fun = thm "starfunC_const_fun";
   662 val starfunRC_const_fun = thm "starfunRC_const_fun";
   663 val starfunCR_const_fun = thm "starfunCR_const_fun";
   664 val starfunC_inverse = thm "starfunC_inverse";
   665 val starfunRC_inverse = thm "starfunRC_inverse";
   666 val starfunCR_inverse = thm "starfunCR_inverse";
   667 val starfunC_eq = thm "starfunC_eq";
   668 val starfunRC_eq = thm "starfunRC_eq";
   669 val starfunCR_eq = thm "starfunCR_eq";
   670 val starfunC_capprox = thm "starfunC_capprox";
   671 val starfunRC_capprox = thm "starfunRC_capprox";
   672 val starfunCR_approx = thm "starfunCR_approx";
   673 val starfunC_hcpow = thm "starfunC_hcpow";
   674 val starfunC_lambda_cancel = thm "starfunC_lambda_cancel";
   675 val starfunCR_lambda_cancel = thm "starfunCR_lambda_cancel";
   676 val starfunRC_lambda_cancel = thm "starfunRC_lambda_cancel";
   677 val starfunC_lambda_cancel2 = thm "starfunC_lambda_cancel2";
   678 val starfunCR_lambda_cancel2 = thm "starfunCR_lambda_cancel2";
   679 val starfunRC_lambda_cancel2 = thm "starfunRC_lambda_cancel2";
   680 val starfunC_mult_CFinite_capprox = thm "starfunC_mult_CFinite_capprox";
   681 val starfunCR_mult_HFinite_capprox = thm "starfunCR_mult_HFinite_capprox";
   682 val starfunRC_mult_CFinite_capprox = thm "starfunRC_mult_CFinite_capprox";
   683 val starfunC_add_capprox = thm "starfunC_add_capprox";
   684 val starfunRC_add_capprox = thm "starfunRC_add_capprox";
   685 val starfunCR_add_approx = thm "starfunCR_add_approx";
   686 val starfunCR_cmod = thm "starfunCR_cmod";
   687 val starfunC_inverse_inverse = thm "starfunC_inverse_inverse";
   688 val starfunC_divide = thm "starfunC_divide";
   689 val starfunCR_divide = thm "starfunCR_divide";
   690 val starfunRC_divide = thm "starfunRC_divide";
   691 val starfunC_n_congruent = thm "starfunC_n_congruent";
   692 val starfunC_n = thm "starfunC_n";
   693 val starfunC_n_mult = thm "starfunC_n_mult";
   694 val starfunC_n_add = thm "starfunC_n_add";
   695 val starfunC_n_minus = thm "starfunC_n_minus";
   696 val starfunNat_n_diff = thm "starfunNat_n_diff";
   697 val starfunC_n_const_fun = thm "starfunC_n_const_fun";
   698 val starfunC_n_eq = thm "starfunC_n_eq";
   699 val starfunC_eq_iff = thm "starfunC_eq_iff";
   700 val starfunRC_eq_iff = thm "starfunRC_eq_iff";
   701 val starfunCR_eq_iff = thm "starfunCR_eq_iff";
   702 val starfunC_eq_Re_Im_iff = thm "starfunC_eq_Re_Im_iff";
   703 val starfunC_approx_Re_Im_iff = thm "starfunC_approx_Re_Im_iff";
   704 val starfunC_Idfun_capprox = thm "starfunC_Idfun_capprox";
   705 val starfunC_Id = thm "starfunC_Id";
   706 *}
   707 
   708 end