1 (* Title : CStar.thy |
|
2 Author : Jacques D. Fleuriot |
|
3 Copyright : 2001 University of Edinburgh |
|
4 *) |
|
5 |
|
6 header{*Star-transforms in NSA, Extending Sets of Complex Numbers |
|
7 and Complex Functions*} |
|
8 |
|
9 theory CStar |
|
10 imports NSCA |
|
11 begin |
|
12 |
|
13 subsection{*Properties of the *-Transform Applied to Sets of Reals*} |
|
14 |
|
15 lemma STARC_hcomplex_of_complex_Int: |
|
16 "*s* X Int SComplex = hcomplex_of_complex ` X" |
|
17 by (auto simp add: Standard_def) |
|
18 |
|
19 lemma lemma_not_hcomplexA: |
|
20 "x \<notin> hcomplex_of_complex ` A ==> \<forall>y \<in> A. x \<noteq> hcomplex_of_complex y" |
|
21 by auto |
|
22 |
|
23 subsection{*Theorems about Nonstandard Extensions of Functions*} |
|
24 |
|
25 lemma starfunC_hcpow: "!!Z. ( *f* (%z. z ^ n)) Z = Z pow hypnat_of_nat n" |
|
26 by transfer (rule refl) |
|
27 |
|
28 lemma starfunCR_cmod: "*f* cmod = hcmod" |
|
29 by transfer (rule refl) |
|
30 |
|
31 subsection{*Internal Functions - Some Redundancy With *f* Now*} |
|
32 |
|
33 (** subtraction: ( *fn) - ( *gn) = *(fn - gn) **) |
|
34 (* |
|
35 lemma starfun_n_diff: |
|
36 "( *fn* f) z - ( *fn* g) z = ( *fn* (%i x. f i x - g i x)) z" |
|
37 apply (cases z) |
|
38 apply (simp add: starfun_n star_n_diff) |
|
39 done |
|
40 *) |
|
41 (** composition: ( *fn) o ( *gn) = *(fn o gn) **) |
|
42 |
|
43 lemma starfun_Re: "( *f* (\<lambda>x. Re (f x))) = (\<lambda>x. hRe (( *f* f) x))" |
|
44 by transfer (rule refl) |
|
45 |
|
46 lemma starfun_Im: "( *f* (\<lambda>x. Im (f x))) = (\<lambda>x. hIm (( *f* f) x))" |
|
47 by transfer (rule refl) |
|
48 |
|
49 lemma starfunC_eq_Re_Im_iff: |
|
50 "(( *f* f) x = z) = ((( *f* (%x. Re(f x))) x = hRe (z)) & |
|
51 (( *f* (%x. Im(f x))) x = hIm (z)))" |
|
52 by (simp add: hcomplex_hRe_hIm_cancel_iff starfun_Re starfun_Im) |
|
53 |
|
54 lemma starfunC_approx_Re_Im_iff: |
|
55 "(( *f* f) x @= z) = ((( *f* (%x. Re(f x))) x @= hRe (z)) & |
|
56 (( *f* (%x. Im(f x))) x @= hIm (z)))" |
|
57 by (simp add: hcomplex_approx_iff starfun_Re starfun_Im) |
|
58 |
|
59 end |
|