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