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