30 ==> ( *f* (\<lambda>z. if z = x then a else g z)) w = ( *f* g) w" |
30 ==> ( *f* (\<lambda>z. if z = x then a else g z)) w = ( *f* g) w" |
31 apply (cases w) |
31 apply (cases w) |
32 apply (simp add: star_of_def starfun star_n_eq_iff, ultra) |
32 apply (simp add: star_of_def starfun star_n_eq_iff, ultra) |
33 done |
33 done |
34 |
34 |
35 lemma starfun_capprox: |
|
36 "( *f* f) (hcomplex_of_complex a) @c= hcomplex_of_complex (f a)" |
|
37 by auto |
|
38 |
|
39 lemma starfunC_hcpow: "( *f* (%z. z ^ n)) Z = Z hcpow hypnat_of_nat n" |
35 lemma starfunC_hcpow: "( *f* (%z. z ^ n)) Z = Z hcpow hypnat_of_nat n" |
40 apply (cases Z) |
36 apply (cases Z) |
41 apply (simp add: hcpow starfun hypnat_of_nat_eq) |
37 apply (simp add: hcpow starfun hypnat_of_nat_eq) |
42 done |
38 done |
43 |
|
44 lemma starfun_mult_CFinite_capprox: |
|
45 "[| ( *f* f) y @c= l; ( *f* g) y @c= m; l: CFinite; m: CFinite |] |
|
46 ==> ( *f* (%x. f x * g x)) y @c= l * m" |
|
47 apply (drule capprox_mult_CFinite, assumption+) |
|
48 apply (auto intro: capprox_sym [THEN [2] capprox_CFinite]) |
|
49 done |
|
50 |
|
51 lemma starfun_add_capprox: |
|
52 "[| ( *f* f) y @c= l; ( *f* g) y @c= m |] |
|
53 ==> ( *f* (%x. f x + g x)) y @c= l + m" |
|
54 by (auto intro: capprox_add) |
|
55 |
39 |
56 lemma starfunCR_cmod: "*f* cmod = hcmod" |
40 lemma starfunCR_cmod: "*f* cmod = hcmod" |
57 apply (rule ext) |
41 apply (rule ext) |
58 apply (rule_tac x = x in star_cases) |
42 apply (rule_tac x = x in star_cases) |
59 apply (simp add: starfun hcmod) |
43 apply (simp add: starfun hcmod) |
77 apply (cases x, cases z) |
61 apply (cases x, cases z) |
78 apply (auto simp add: starfun hIm hRe complex_Re_Im_cancel_iff star_n_eq_iff, ultra+) |
62 apply (auto simp add: starfun hIm hRe complex_Re_Im_cancel_iff star_n_eq_iff, ultra+) |
79 done |
63 done |
80 |
64 |
81 lemma starfunC_approx_Re_Im_iff: |
65 lemma starfunC_approx_Re_Im_iff: |
82 "(( *f* f) x @c= z) = ((( *f* (%x. Re(f x))) x @= hRe (z)) & |
66 "(( *f* f) x @= z) = ((( *f* (%x. Re(f x))) x @= hRe (z)) & |
83 (( *f* (%x. Im(f x))) x @= hIm (z)))" |
67 (( *f* (%x. Im(f x))) x @= hIm (z)))" |
84 apply (cases x, cases z) |
68 apply (cases x, cases z) |
85 apply (simp add: starfun hIm hRe capprox_approx_iff) |
69 apply (simp add: starfun hIm hRe approx_approx_iff) |
86 done |
70 done |
87 |
71 |
88 lemma starfunC_Idfun_capprox: |
72 lemma starfunC_Idfun_approx: |
89 "x @c= hcomplex_of_complex a ==> ( *f* (%x. x)) x @c= hcomplex_of_complex a" |
73 "x @= hcomplex_of_complex a ==> ( *f* (%x. x)) x @= hcomplex_of_complex a" |
90 by simp |
74 by simp |
91 |
75 |
92 end |
76 end |