author | huffman |
Tue, 06 Sep 2005 20:53:27 +0200 | |
changeset 17292 | 5c613b64bf0a |
parent 15234 | ec91a90c604e |
child 17298 | ad73fb6144cf |
permissions | -rw-r--r-- |
13957 | 1 |
(* Title : CStar.thy |
2 |
Author : Jacques D. Fleuriot |
|
3 |
Copyright : 2001 University of Edinburgh |
|
4 |
*) |
|
5 |
||
14407 | 6 |
header{*Star-transforms in NSA, Extending Sets of Complex Numbers |
7 |
and Complex Functions*} |
|
8 |
||
15131 | 9 |
theory CStar |
15140 | 10 |
imports NSCA |
15131 | 11 |
begin |
13957 | 12 |
|
13 |
constdefs |
|
14 |
||
15 |
(* nonstandard extension of sets *) |
|
14407 | 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}" |
|
13957 | 18 |
|
19 |
(* internal sets *) |
|
14407 | 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 |
||
13957 | 24 |
InternalCSets :: "hcomplex set set" |
14407 | 25 |
"InternalCSets == {X. \<exists>As. X = *scn* As}" |
13957 | 26 |
|
27 |
(* star transform of functions f: Complex --> Complex *) |
|
28 |
||
14407 | 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)}))" |
|
13957 | 33 |
|
14407 | 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)}))" |
|
13957 | 38 |
|
14407 | 39 |
InternalCFuns :: "(hcomplex => hcomplex) set" |
40 |
"InternalCFuns == {X. \<exists>F. X = *fcn* F}" |
|
13957 | 41 |
|
42 |
||
43 |
(* star transform of functions f: Real --> Complex *) |
|
44 |
||
14407 | 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)}))" |
|
13957 | 48 |
|
14407 | 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)}))" |
|
13957 | 52 |
|
14407 | 53 |
InternalRCFuns :: "(hypreal => hcomplex) set" |
54 |
"InternalRCFuns == {X. \<exists>F. X = *fRcn* F}" |
|
13957 | 55 |
|
56 |
(* star transform of functions f: Complex --> Real; needed for Re and Im parts *) |
|
57 |
||
14407 | 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" |
|
17292 | 189 |
apply (subgoal_tac "UNIV - X = - X") |
14407 | 190 |
by (auto intro: InternalCSets_Compl) |
191 |
||
192 |
text{*Nonstandard extension of a set (defined using a constant sequence) as a special case of an internal set*} |
|
193 |
||
194 |
lemma starsetC_n_starsetC: "\<forall>n. (As n = A) ==> *scn* As = *sc* A" |
|
195 |
by (simp add:starsetC_n_def starsetC_def) |
|
196 |
||
197 |
||
198 |
subsection{*Theorems about Nonstandard Extensions of Functions*} |
|
199 |
||
200 |
lemma starfunC_n_starfunC: "\<forall>n. (F n = f) ==> *fcn* F = *fc* f" |
|
201 |
by (simp add: starfunC_n_def starfunC_def) |
|
202 |
||
203 |
lemma starfunRC_n_starfunRC: "\<forall>n. (F n = f) ==> *fRcn* F = *fRc* f" |
|
204 |
by (simp add: starfunRC_n_def starfunRC_def) |
|
205 |
||
206 |
lemma starfunCR_n_starfunCR: "\<forall>n. (F n = f) ==> *fcRn* F = *fcR* f" |
|
207 |
by (simp add: starfunCR_n_def starfunCR_def) |
|
208 |
||
209 |
lemma starfunC_congruent: |
|
15169 | 210 |
"(%X. hcomplexrel``{%n. f (X n)}) respects hcomplexrel" |
211 |
by (auto simp add: hcomplexrel_iff congruent_def, ultra) |
|
14407 | 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 |
||
15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15169
diff
changeset
|
222 |
lemma cstarfun_if_eq: |
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15169
diff
changeset
|
223 |
"w \<noteq> hcomplex_of_complex x |
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15169
diff
changeset
|
224 |
==> ( *fc* (\<lambda>z. if z = x then a else g z)) w = ( *fc* g) w" |
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15169
diff
changeset
|
225 |
apply (cases w) |
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15169
diff
changeset
|
226 |
apply (simp add: hcomplex_of_complex_def starfunC, ultra) |
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15169
diff
changeset
|
227 |
done |
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15169
diff
changeset
|
228 |
|
14407 | 229 |
lemma starfunRC: |
230 |
"( *fRc* f) (Abs_hypreal(hyprel``{%n. X n})) = |
|
231 |
Abs_hcomplex(hcomplexrel `` {%n. f (X n)})" |
|
232 |
apply (simp add: starfunRC_def) |
|
233 |
apply (rule arg_cong [where f = Abs_hcomplex], auto, ultra) |
|
234 |
done |
|
235 |
||
236 |
lemma starfunCR: |
|
237 |
"( *fcR* f) (Abs_hcomplex(hcomplexrel``{%n. X n})) = |
|
238 |
Abs_hypreal(hyprel `` {%n. f (X n)})" |
|
239 |
apply (simp add: starfunCR_def) |
|
240 |
apply (rule arg_cong [where f = Abs_hypreal]) |
|
241 |
apply (auto iff add: hcomplexrel_iff, ultra) |
|
242 |
done |
|
243 |
||
244 |
(** multiplication: ( *f) x ( *g) = *(f x g) **) |
|
245 |
||
246 |
lemma starfunC_mult: "( *fc* f) z * ( *fc* g) z = ( *fc* (%x. f x * g x)) z" |
|
247 |
apply (rule_tac z = z in eq_Abs_hcomplex) |
|
248 |
apply (auto simp add: starfunC hcomplex_mult) |
|
249 |
done |
|
250 |
declare starfunC_mult [symmetric, simp] |
|
251 |
||
252 |
lemma starfunRC_mult: |
|
253 |
"( *fRc* f) z * ( *fRc* g) z = ( *fRc* (%x. f x * g x)) z" |
|
14469 | 254 |
apply (cases z) |
14407 | 255 |
apply (simp add: starfunRC hcomplex_mult) |
256 |
done |
|
257 |
declare starfunRC_mult [symmetric, simp] |
|
258 |
||
259 |
lemma starfunCR_mult: |
|
260 |
"( *fcR* f) z * ( *fcR* g) z = ( *fcR* (%x. f x * g x)) z" |
|
261 |
apply (rule_tac z = z in eq_Abs_hcomplex) |
|
262 |
apply (simp add: starfunCR hypreal_mult) |
|
263 |
done |
|
264 |
declare starfunCR_mult [symmetric, simp] |
|
265 |
||
266 |
(** addition: ( *f) + ( *g) = *(f + g) **) |
|
267 |
||
268 |
lemma starfunC_add: "( *fc* f) z + ( *fc* g) z = ( *fc* (%x. f x + g x)) z" |
|
269 |
apply (rule_tac z = z in eq_Abs_hcomplex) |
|
270 |
apply (simp add: starfunC hcomplex_add) |
|
271 |
done |
|
272 |
declare starfunC_add [symmetric, simp] |
|
273 |
||
274 |
lemma starfunRC_add: "( *fRc* f) z + ( *fRc* g) z = ( *fRc* (%x. f x + g x)) z" |
|
14469 | 275 |
apply (cases z) |
14407 | 276 |
apply (simp add: starfunRC hcomplex_add) |
277 |
done |
|
278 |
declare starfunRC_add [symmetric, simp] |
|
279 |
||
280 |
lemma starfunCR_add: "( *fcR* f) z + ( *fcR* g) z = ( *fcR* (%x. f x + g x)) z" |
|
281 |
apply (rule_tac z = z in eq_Abs_hcomplex) |
|
282 |
apply (simp add: starfunCR hypreal_add) |
|
283 |
done |
|
284 |
declare starfunCR_add [symmetric, simp] |
|
285 |
||
286 |
(** uminus **) |
|
287 |
lemma starfunC_minus [simp]: "( *fc* (%x. - f x)) x = - ( *fc* f) x" |
|
288 |
apply (rule_tac z = x in eq_Abs_hcomplex) |
|
289 |
apply (simp add: starfunC hcomplex_minus) |
|
290 |
done |
|
291 |
||
292 |
lemma starfunRC_minus [simp]: "( *fRc* (%x. - f x)) x = - ( *fRc* f) x" |
|
14469 | 293 |
apply (cases x) |
14407 | 294 |
apply (simp add: starfunRC hcomplex_minus) |
295 |
done |
|
296 |
||
297 |
lemma starfunCR_minus [simp]: "( *fcR* (%x. - f x)) x = - ( *fcR* f) x" |
|
298 |
apply (rule_tac z = x in eq_Abs_hcomplex) |
|
299 |
apply (simp add: starfunCR hypreal_minus) |
|
300 |
done |
|
301 |
||
302 |
(** addition: ( *f) - ( *g) = *(f - g) **) |
|
303 |
||
304 |
lemma starfunC_diff: "( *fc* f) y - ( *fc* g) y = ( *fc* (%x. f x - g x)) y" |
|
305 |
by (simp add: diff_minus) |
|
306 |
declare starfunC_diff [symmetric, simp] |
|
307 |
||
308 |
lemma starfunRC_diff: |
|
309 |
"( *fRc* f) y - ( *fRc* g) y = ( *fRc* (%x. f x - g x)) y" |
|
310 |
by (simp add: diff_minus) |
|
311 |
declare starfunRC_diff [symmetric, simp] |
|
312 |
||
313 |
lemma starfunCR_diff: |
|
314 |
"( *fcR* f) y - ( *fcR* g) y = ( *fcR* (%x. f x - g x)) y" |
|
315 |
by (simp add: diff_minus) |
|
316 |
declare starfunCR_diff [symmetric, simp] |
|
317 |
||
318 |
(** composition: ( *f) o ( *g) = *(f o g) **) |
|
319 |
||
320 |
lemma starfunC_o2: "(%x. ( *fc* f) (( *fc* g) x)) = *fc* (%x. f (g x))" |
|
321 |
apply (rule ext) |
|
322 |
apply (rule_tac z = x in eq_Abs_hcomplex) |
|
323 |
apply (simp add: starfunC) |
|
324 |
done |
|
325 |
||
326 |
lemma starfunC_o: "( *fc* f) o ( *fc* g) = ( *fc* (f o g))" |
|
327 |
by (simp add: o_def starfunC_o2) |
|
328 |
||
329 |
lemma starfunC_starfunRC_o2: |
|
330 |
"(%x. ( *fc* f) (( *fRc* g) x)) = *fRc* (%x. f (g x))" |
|
331 |
apply (rule ext) |
|
332 |
apply (rule_tac z = x in eq_Abs_hypreal) |
|
333 |
apply (simp add: starfunRC starfunC) |
|
334 |
done |
|
335 |
||
336 |
lemma starfun_starfunCR_o2: |
|
337 |
"(%x. ( *f* f) (( *fcR* g) x)) = *fcR* (%x. f (g x))" |
|
338 |
apply (rule ext) |
|
339 |
apply (rule_tac z = x in eq_Abs_hcomplex) |
|
340 |
apply (simp add: starfunCR starfun) |
|
341 |
done |
|
342 |
||
343 |
lemma starfunC_starfunRC_o: "( *fc* f) o ( *fRc* g) = ( *fRc* (f o g))" |
|
344 |
by (simp add: o_def starfunC_starfunRC_o2) |
|
345 |
||
346 |
lemma starfun_starfunCR_o: "( *f* f) o ( *fcR* g) = ( *fcR* (f o g))" |
|
347 |
by (simp add: o_def starfun_starfunCR_o2) |
|
348 |
||
349 |
lemma starfunC_const_fun [simp]: "( *fc* (%x. k)) z = hcomplex_of_complex k" |
|
14469 | 350 |
apply (cases z) |
14407 | 351 |
apply (simp add: starfunC hcomplex_of_complex_def) |
352 |
done |
|
353 |
||
354 |
lemma starfunRC_const_fun [simp]: "( *fRc* (%x. k)) z = hcomplex_of_complex k" |
|
14469 | 355 |
apply (cases z) |
14407 | 356 |
apply (simp add: starfunRC hcomplex_of_complex_def) |
357 |
done |
|
358 |
||
359 |
lemma starfunCR_const_fun [simp]: "( *fcR* (%x. k)) z = hypreal_of_real k" |
|
14469 | 360 |
apply (cases z) |
14407 | 361 |
apply (simp add: starfunCR hypreal_of_real_def) |
362 |
done |
|
363 |
||
364 |
lemma starfunC_inverse: "inverse (( *fc* f) x) = ( *fc* (%x. inverse (f x))) x" |
|
14469 | 365 |
apply (cases x) |
14407 | 366 |
apply (simp add: starfunC hcomplex_inverse) |
367 |
done |
|
368 |
declare starfunC_inverse [symmetric, simp] |
|
369 |
||
370 |
lemma starfunRC_inverse: |
|
371 |
"inverse (( *fRc* f) x) = ( *fRc* (%x. inverse (f x))) x" |
|
14469 | 372 |
apply (cases x) |
14407 | 373 |
apply (simp add: starfunRC hcomplex_inverse) |
374 |
done |
|
375 |
declare starfunRC_inverse [symmetric, simp] |
|
376 |
||
377 |
lemma starfunCR_inverse: |
|
378 |
"inverse (( *fcR* f) x) = ( *fcR* (%x. inverse (f x))) x" |
|
14469 | 379 |
apply (cases x) |
14407 | 380 |
apply (simp add: starfunCR hypreal_inverse) |
381 |
done |
|
382 |
declare starfunCR_inverse [symmetric, simp] |
|
383 |
||
384 |
lemma starfunC_eq [simp]: |
|
385 |
"( *fc* f) (hcomplex_of_complex a) = hcomplex_of_complex (f a)" |
|
386 |
by (simp add: starfunC hcomplex_of_complex_def) |
|
387 |
||
388 |
lemma starfunRC_eq [simp]: |
|
389 |
"( *fRc* f) (hypreal_of_real a) = hcomplex_of_complex (f a)" |
|
390 |
by (simp add: starfunRC hcomplex_of_complex_def hypreal_of_real_def) |
|
13957 | 391 |
|
14407 | 392 |
lemma starfunCR_eq [simp]: |
393 |
"( *fcR* f) (hcomplex_of_complex a) = hypreal_of_real (f a)" |
|
394 |
by (simp add: starfunCR hcomplex_of_complex_def hypreal_of_real_def) |
|
395 |
||
396 |
lemma starfunC_capprox: |
|
397 |
"( *fc* f) (hcomplex_of_complex a) @c= hcomplex_of_complex (f a)" |
|
398 |
by auto |
|
399 |
||
400 |
lemma starfunRC_capprox: |
|
401 |
"( *fRc* f) (hypreal_of_real a) @c= hcomplex_of_complex (f a)" |
|
402 |
by auto |
|
403 |
||
404 |
lemma starfunCR_approx: |
|
405 |
"( *fcR* f) (hcomplex_of_complex a) @= hypreal_of_real (f a)" |
|
406 |
by auto |
|
407 |
||
408 |
(* |
|
409 |
Goal "( *fcNat* (%n. z ^ n)) N = (hcomplex_of_complex z) hcpow N" |
|
410 |
*) |
|
411 |
||
412 |
lemma starfunC_hcpow: "( *fc* (%z. z ^ n)) Z = Z hcpow hypnat_of_nat n" |
|
14469 | 413 |
apply (cases Z) |
14407 | 414 |
apply (simp add: hcpow starfunC hypnat_of_nat_eq) |
415 |
done |
|
416 |
||
417 |
lemma starfunC_lambda_cancel: |
|
418 |
"( *fc* (%h. f (x + h))) y = ( *fc* f) (hcomplex_of_complex x + y)" |
|
14469 | 419 |
apply (cases y) |
14407 | 420 |
apply (simp add: starfunC hcomplex_of_complex_def hcomplex_add) |
421 |
done |
|
422 |
||
423 |
lemma starfunCR_lambda_cancel: |
|
424 |
"( *fcR* (%h. f (x + h))) y = ( *fcR* f) (hcomplex_of_complex x + y)" |
|
14469 | 425 |
apply (cases y) |
14407 | 426 |
apply (simp add: starfunCR hcomplex_of_complex_def hcomplex_add) |
427 |
done |
|
428 |
||
429 |
lemma starfunRC_lambda_cancel: |
|
430 |
"( *fRc* (%h. f (x + h))) y = ( *fRc* f) (hypreal_of_real x + y)" |
|
14469 | 431 |
apply (cases y) |
14407 | 432 |
apply (simp add: starfunRC hypreal_of_real_def hypreal_add) |
433 |
done |
|
434 |
||
435 |
lemma starfunC_lambda_cancel2: |
|
436 |
"( *fc* (%h. f(g(x + h)))) y = ( *fc* (f o g)) (hcomplex_of_complex x + y)" |
|
14469 | 437 |
apply (cases y) |
14407 | 438 |
apply (simp add: starfunC hcomplex_of_complex_def hcomplex_add) |
439 |
done |
|
440 |
||
441 |
lemma starfunCR_lambda_cancel2: |
|
442 |
"( *fcR* (%h. f(g(x + h)))) y = ( *fcR* (f o g)) (hcomplex_of_complex x + y)" |
|
14469 | 443 |
apply (cases y) |
14407 | 444 |
apply (simp add: starfunCR hcomplex_of_complex_def hcomplex_add) |
445 |
done |
|
446 |
||
447 |
lemma starfunRC_lambda_cancel2: |
|
448 |
"( *fRc* (%h. f(g(x + h)))) y = ( *fRc* (f o g)) (hypreal_of_real x + y)" |
|
14469 | 449 |
apply (cases y) |
14407 | 450 |
apply (simp add: starfunRC hypreal_of_real_def hypreal_add) |
451 |
done |
|
452 |
||
453 |
lemma starfunC_mult_CFinite_capprox: |
|
454 |
"[| ( *fc* f) y @c= l; ( *fc* g) y @c= m; l: CFinite; m: CFinite |] |
|
455 |
==> ( *fc* (%x. f x * g x)) y @c= l * m" |
|
456 |
apply (drule capprox_mult_CFinite, assumption+) |
|
457 |
apply (auto intro: capprox_sym [THEN [2] capprox_CFinite]) |
|
458 |
done |
|
459 |
||
460 |
lemma starfunCR_mult_HFinite_capprox: |
|
461 |
"[| ( *fcR* f) y @= l; ( *fcR* g) y @= m; l: HFinite; m: HFinite |] |
|
462 |
==> ( *fcR* (%x. f x * g x)) y @= l * m" |
|
463 |
apply (drule approx_mult_HFinite, assumption+) |
|
464 |
apply (auto intro: approx_sym [THEN [2] approx_HFinite]) |
|
465 |
done |
|
466 |
||
467 |
lemma starfunRC_mult_CFinite_capprox: |
|
468 |
"[| ( *fRc* f) y @c= l; ( *fRc* g) y @c= m; l: CFinite; m: CFinite |] |
|
469 |
==> ( *fRc* (%x. f x * g x)) y @c= l * m" |
|
470 |
apply (drule capprox_mult_CFinite, assumption+) |
|
471 |
apply (auto intro: capprox_sym [THEN [2] capprox_CFinite]) |
|
472 |
done |
|
473 |
||
474 |
lemma starfunC_add_capprox: |
|
475 |
"[| ( *fc* f) y @c= l; ( *fc* g) y @c= m |] |
|
476 |
==> ( *fc* (%x. f x + g x)) y @c= l + m" |
|
477 |
by (auto intro: capprox_add) |
|
478 |
||
479 |
lemma starfunRC_add_capprox: |
|
480 |
"[| ( *fRc* f) y @c= l; ( *fRc* g) y @c= m |] |
|
481 |
==> ( *fRc* (%x. f x + g x)) y @c= l + m" |
|
482 |
by (auto intro: capprox_add) |
|
483 |
||
484 |
lemma starfunCR_add_approx: |
|
485 |
"[| ( *fcR* f) y @= l; ( *fcR* g) y @= m |
|
486 |
|] ==> ( *fcR* (%x. f x + g x)) y @= l + m" |
|
487 |
by (auto intro: approx_add) |
|
488 |
||
489 |
lemma starfunCR_cmod: "*fcR* cmod = hcmod" |
|
490 |
apply (rule ext) |
|
491 |
apply (rule_tac z = x in eq_Abs_hcomplex) |
|
492 |
apply (simp add: starfunCR hcmod) |
|
493 |
done |
|
494 |
||
495 |
lemma starfunC_inverse_inverse: "( *fc* inverse) x = inverse(x)" |
|
14469 | 496 |
apply (cases x) |
14407 | 497 |
apply (simp add: starfunC hcomplex_inverse) |
498 |
done |
|
499 |
||
500 |
lemma starfunC_divide: "( *fc* f) y / ( *fc* g) y = ( *fc* (%x. f x / g x)) y" |
|
14430
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14407
diff
changeset
|
501 |
by (simp add: divide_inverse) |
14407 | 502 |
declare starfunC_divide [symmetric, simp] |
503 |
||
504 |
lemma starfunCR_divide: |
|
505 |
"( *fcR* f) y / ( *fcR* g) y = ( *fcR* (%x. f x / g x)) y" |
|
14430
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14407
diff
changeset
|
506 |
by (simp add: divide_inverse) |
14407 | 507 |
declare starfunCR_divide [symmetric, simp] |
508 |
||
509 |
lemma starfunRC_divide: |
|
510 |
"( *fRc* f) y / ( *fRc* g) y = ( *fRc* (%x. f x / g x)) y" |
|
14430
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14407
diff
changeset
|
511 |
by (simp add: divide_inverse) |
14407 | 512 |
declare starfunRC_divide [symmetric, simp] |
513 |
||
514 |
||
515 |
subsection{*Internal Functions - Some Redundancy With *Fc* Now*} |
|
516 |
||
517 |
lemma starfunC_n_congruent: |
|
15169 | 518 |
"(%X. hcomplexrel``{%n. f n (X n)}) respects hcomplexrel" |
14407 | 519 |
by (auto simp add: congruent_def hcomplexrel_iff, ultra) |
520 |
||
521 |
lemma starfunC_n: |
|
522 |
"( *fcn* f) (Abs_hcomplex(hcomplexrel``{%n. X n})) = |
|
523 |
Abs_hcomplex(hcomplexrel `` {%n. f n (X n)})" |
|
524 |
apply (simp add: starfunC_n_def) |
|
525 |
apply (rule arg_cong [where f = Abs_hcomplex]) |
|
526 |
apply (auto iff add: hcomplexrel_iff, ultra) |
|
527 |
done |
|
528 |
||
529 |
(** multiplication: ( *fn) x ( *gn) = *(fn x gn) **) |
|
530 |
||
531 |
lemma starfunC_n_mult: |
|
532 |
"( *fcn* f) z * ( *fcn* g) z = ( *fcn* (% i x. f i x * g i x)) z" |
|
14469 | 533 |
apply (cases z) |
14407 | 534 |
apply (simp add: starfunC_n hcomplex_mult) |
535 |
done |
|
536 |
||
537 |
(** addition: ( *fn) + ( *gn) = *(fn + gn) **) |
|
538 |
||
539 |
lemma starfunC_n_add: |
|
540 |
"( *fcn* f) z + ( *fcn* g) z = ( *fcn* (%i x. f i x + g i x)) z" |
|
14469 | 541 |
apply (cases z) |
14407 | 542 |
apply (simp add: starfunC_n hcomplex_add) |
543 |
done |
|
544 |
||
545 |
(** uminus **) |
|
546 |
||
547 |
lemma starfunC_n_minus: "- ( *fcn* g) z = ( *fcn* (%i x. - g i x)) z" |
|
14469 | 548 |
apply (cases z) |
14407 | 549 |
apply (simp add: starfunC_n hcomplex_minus) |
550 |
done |
|
551 |
||
552 |
(** subtraction: ( *fn) - ( *gn) = *(fn - gn) **) |
|
13957 | 553 |
|
14407 | 554 |
lemma starfunNat_n_diff: |
555 |
"( *fcn* f) z - ( *fcn* g) z = ( *fcn* (%i x. f i x - g i x)) z" |
|
556 |
by (simp add: diff_minus starfunC_n_add starfunC_n_minus) |
|
557 |
||
558 |
(** composition: ( *fn) o ( *gn) = *(fn o gn) **) |
|
559 |
||
560 |
lemma starfunC_n_const_fun [simp]: |
|
561 |
"( *fcn* (%i x. k)) z = hcomplex_of_complex k" |
|
14469 | 562 |
apply (cases z) |
14407 | 563 |
apply (simp add: starfunC_n hcomplex_of_complex_def) |
564 |
done |
|
565 |
||
566 |
lemma starfunC_n_eq [simp]: |
|
567 |
"( *fcn* f) (hcomplex_of_complex n) = Abs_hcomplex(hcomplexrel `` {%i. f i n})" |
|
568 |
by (simp add: starfunC_n hcomplex_of_complex_def) |
|
569 |
||
570 |
lemma starfunC_eq_iff: "(( *fc* f) = ( *fc* g)) = (f = g)" |
|
571 |
apply auto |
|
572 |
apply (rule ext, rule ccontr) |
|
573 |
apply (drule_tac x = "hcomplex_of_complex (x) " in fun_cong) |
|
574 |
apply (simp add: starfunC hcomplex_of_complex_def) |
|
575 |
done |
|
576 |
||
577 |
lemma starfunRC_eq_iff: "(( *fRc* f) = ( *fRc* g)) = (f = g)" |
|
578 |
apply auto |
|
579 |
apply (rule ext, rule ccontr) |
|
580 |
apply (drule_tac x = "hypreal_of_real (x) " in fun_cong) |
|
581 |
apply auto |
|
582 |
done |
|
583 |
||
584 |
lemma starfunCR_eq_iff: "(( *fcR* f) = ( *fcR* g)) = (f = g)" |
|
585 |
apply auto |
|
586 |
apply (rule ext, rule ccontr) |
|
587 |
apply (drule_tac x = "hcomplex_of_complex (x) " in fun_cong) |
|
588 |
apply auto |
|
589 |
done |
|
590 |
||
591 |
lemma starfunC_eq_Re_Im_iff: |
|
592 |
"(( *fc* f) x = z) = ((( *fcR* (%x. Re(f x))) x = hRe (z)) & |
|
593 |
(( *fcR* (%x. Im(f x))) x = hIm (z)))" |
|
14469 | 594 |
apply (cases x, cases z) |
14407 | 595 |
apply (auto simp add: starfunCR starfunC hIm hRe complex_Re_Im_cancel_iff, ultra+) |
596 |
done |
|
597 |
||
598 |
lemma starfunC_approx_Re_Im_iff: |
|
599 |
"(( *fc* f) x @c= z) = ((( *fcR* (%x. Re(f x))) x @= hRe (z)) & |
|
600 |
(( *fcR* (%x. Im(f x))) x @= hIm (z)))" |
|
14469 | 601 |
apply (cases x, cases z) |
14407 | 602 |
apply (simp add: starfunCR starfunC hIm hRe capprox_approx_iff) |
603 |
done |
|
604 |
||
605 |
lemma starfunC_Idfun_capprox: |
|
606 |
"x @c= hcomplex_of_complex a ==> ( *fc* (%x. x)) x @c= hcomplex_of_complex a" |
|
14469 | 607 |
apply (cases x) |
14407 | 608 |
apply (simp add: starfunC) |
609 |
done |
|
610 |
||
611 |
lemma starfunC_Id [simp]: "( *fc* (%x. x)) x = x" |
|
14469 | 612 |
apply (cases x) |
14407 | 613 |
apply (simp add: starfunC) |
614 |
done |
|
13957 | 615 |
|
14407 | 616 |
ML |
617 |
{* |
|
618 |
val STARC_complex_set = thm "STARC_complex_set"; |
|
619 |
val STARC_empty_set = thm "STARC_empty_set"; |
|
620 |
val STARC_Un = thm "STARC_Un"; |
|
621 |
val starsetC_n_Un = thm "starsetC_n_Un"; |
|
622 |
val InternalCSets_Un = thm "InternalCSets_Un"; |
|
623 |
val STARC_Int = thm "STARC_Int"; |
|
624 |
val starsetC_n_Int = thm "starsetC_n_Int"; |
|
625 |
val InternalCSets_Int = thm "InternalCSets_Int"; |
|
626 |
val STARC_Compl = thm "STARC_Compl"; |
|
627 |
val starsetC_n_Compl = thm "starsetC_n_Compl"; |
|
628 |
val InternalCSets_Compl = thm "InternalCSets_Compl"; |
|
629 |
val STARC_mem_Compl = thm "STARC_mem_Compl"; |
|
630 |
val STARC_diff = thm "STARC_diff"; |
|
631 |
val starsetC_n_diff = thm "starsetC_n_diff"; |
|
632 |
val InternalCSets_diff = thm "InternalCSets_diff"; |
|
633 |
val STARC_subset = thm "STARC_subset"; |
|
634 |
val STARC_mem = thm "STARC_mem"; |
|
635 |
val STARC_hcomplex_of_complex_image_subset = thm "STARC_hcomplex_of_complex_image_subset"; |
|
636 |
val STARC_SComplex_subset = thm "STARC_SComplex_subset"; |
|
637 |
val STARC_hcomplex_of_complex_Int = thm "STARC_hcomplex_of_complex_Int"; |
|
638 |
val lemma_not_hcomplexA = thm "lemma_not_hcomplexA"; |
|
639 |
val starsetC_starsetC_n_eq = thm "starsetC_starsetC_n_eq"; |
|
640 |
val InternalCSets_starsetC_n = thm "InternalCSets_starsetC_n"; |
|
641 |
val InternalCSets_UNIV_diff = thm "InternalCSets_UNIV_diff"; |
|
642 |
val starsetC_n_starsetC = thm "starsetC_n_starsetC"; |
|
643 |
val starfunC_n_starfunC = thm "starfunC_n_starfunC"; |
|
644 |
val starfunRC_n_starfunRC = thm "starfunRC_n_starfunRC"; |
|
645 |
val starfunCR_n_starfunCR = thm "starfunCR_n_starfunCR"; |
|
646 |
val starfunC_congruent = thm "starfunC_congruent"; |
|
647 |
val starfunC = thm "starfunC"; |
|
648 |
val starfunRC = thm "starfunRC"; |
|
649 |
val starfunCR = thm "starfunCR"; |
|
650 |
val starfunC_mult = thm "starfunC_mult"; |
|
651 |
val starfunRC_mult = thm "starfunRC_mult"; |
|
652 |
val starfunCR_mult = thm "starfunCR_mult"; |
|
653 |
val starfunC_add = thm "starfunC_add"; |
|
654 |
val starfunRC_add = thm "starfunRC_add"; |
|
655 |
val starfunCR_add = thm "starfunCR_add"; |
|
656 |
val starfunC_minus = thm "starfunC_minus"; |
|
657 |
val starfunRC_minus = thm "starfunRC_minus"; |
|
658 |
val starfunCR_minus = thm "starfunCR_minus"; |
|
659 |
val starfunC_diff = thm "starfunC_diff"; |
|
660 |
val starfunRC_diff = thm "starfunRC_diff"; |
|
661 |
val starfunCR_diff = thm "starfunCR_diff"; |
|
662 |
val starfunC_o2 = thm "starfunC_o2"; |
|
663 |
val starfunC_o = thm "starfunC_o"; |
|
664 |
val starfunC_starfunRC_o2 = thm "starfunC_starfunRC_o2"; |
|
665 |
val starfun_starfunCR_o2 = thm "starfun_starfunCR_o2"; |
|
666 |
val starfunC_starfunRC_o = thm "starfunC_starfunRC_o"; |
|
667 |
val starfun_starfunCR_o = thm "starfun_starfunCR_o"; |
|
668 |
val starfunC_const_fun = thm "starfunC_const_fun"; |
|
669 |
val starfunRC_const_fun = thm "starfunRC_const_fun"; |
|
670 |
val starfunCR_const_fun = thm "starfunCR_const_fun"; |
|
671 |
val starfunC_inverse = thm "starfunC_inverse"; |
|
672 |
val starfunRC_inverse = thm "starfunRC_inverse"; |
|
673 |
val starfunCR_inverse = thm "starfunCR_inverse"; |
|
674 |
val starfunC_eq = thm "starfunC_eq"; |
|
675 |
val starfunRC_eq = thm "starfunRC_eq"; |
|
676 |
val starfunCR_eq = thm "starfunCR_eq"; |
|
677 |
val starfunC_capprox = thm "starfunC_capprox"; |
|
678 |
val starfunRC_capprox = thm "starfunRC_capprox"; |
|
679 |
val starfunCR_approx = thm "starfunCR_approx"; |
|
680 |
val starfunC_hcpow = thm "starfunC_hcpow"; |
|
681 |
val starfunC_lambda_cancel = thm "starfunC_lambda_cancel"; |
|
682 |
val starfunCR_lambda_cancel = thm "starfunCR_lambda_cancel"; |
|
683 |
val starfunRC_lambda_cancel = thm "starfunRC_lambda_cancel"; |
|
684 |
val starfunC_lambda_cancel2 = thm "starfunC_lambda_cancel2"; |
|
685 |
val starfunCR_lambda_cancel2 = thm "starfunCR_lambda_cancel2"; |
|
686 |
val starfunRC_lambda_cancel2 = thm "starfunRC_lambda_cancel2"; |
|
687 |
val starfunC_mult_CFinite_capprox = thm "starfunC_mult_CFinite_capprox"; |
|
688 |
val starfunCR_mult_HFinite_capprox = thm "starfunCR_mult_HFinite_capprox"; |
|
689 |
val starfunRC_mult_CFinite_capprox = thm "starfunRC_mult_CFinite_capprox"; |
|
690 |
val starfunC_add_capprox = thm "starfunC_add_capprox"; |
|
691 |
val starfunRC_add_capprox = thm "starfunRC_add_capprox"; |
|
692 |
val starfunCR_add_approx = thm "starfunCR_add_approx"; |
|
693 |
val starfunCR_cmod = thm "starfunCR_cmod"; |
|
694 |
val starfunC_inverse_inverse = thm "starfunC_inverse_inverse"; |
|
695 |
val starfunC_divide = thm "starfunC_divide"; |
|
696 |
val starfunCR_divide = thm "starfunCR_divide"; |
|
697 |
val starfunRC_divide = thm "starfunRC_divide"; |
|
698 |
val starfunC_n_congruent = thm "starfunC_n_congruent"; |
|
699 |
val starfunC_n = thm "starfunC_n"; |
|
700 |
val starfunC_n_mult = thm "starfunC_n_mult"; |
|
701 |
val starfunC_n_add = thm "starfunC_n_add"; |
|
702 |
val starfunC_n_minus = thm "starfunC_n_minus"; |
|
703 |
val starfunNat_n_diff = thm "starfunNat_n_diff"; |
|
704 |
val starfunC_n_const_fun = thm "starfunC_n_const_fun"; |
|
705 |
val starfunC_n_eq = thm "starfunC_n_eq"; |
|
706 |
val starfunC_eq_iff = thm "starfunC_eq_iff"; |
|
707 |
val starfunRC_eq_iff = thm "starfunRC_eq_iff"; |
|
708 |
val starfunCR_eq_iff = thm "starfunCR_eq_iff"; |
|
709 |
val starfunC_eq_Re_Im_iff = thm "starfunC_eq_Re_Im_iff"; |
|
710 |
val starfunC_approx_Re_Im_iff = thm "starfunC_approx_Re_Im_iff"; |
|
711 |
val starfunC_Idfun_capprox = thm "starfunC_Idfun_capprox"; |
|
712 |
val starfunC_Id = thm "starfunC_Id"; |
|
713 |
*} |
|
714 |
||
715 |
end |