author | haftmann |
Wed, 22 Nov 2006 10:20:15 +0100 | |
changeset 21455 | b6be1d1b66c5 |
parent 21404 | eb85850d3eb7 |
child 21810 | b2d23672b003 |
permissions | -rw-r--r-- |
13957 | 1 |
(* Title : NSCA.thy |
2 |
Author : Jacques D. Fleuriot |
|
3 |
Copyright : 2001,2002 University of Edinburgh |
|
4 |
*) |
|
5 |
||
14408 | 6 |
header{*Non-Standard Complex Analysis*} |
13957 | 7 |
|
15131 | 8 |
theory NSCA |
15140 | 9 |
imports NSComplex |
15131 | 10 |
begin |
13957 | 11 |
|
19765 | 12 |
definition |
13957 | 13 |
(* standard complex numbers reagarded as an embedded subset of NS complex *) |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20724
diff
changeset
|
14 |
SComplex :: "hcomplex set" where |
19765 | 15 |
"SComplex = {x. \<exists>r. x = hcomplex_of_complex r}" |
13957 | 16 |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20724
diff
changeset
|
17 |
definition |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20724
diff
changeset
|
18 |
stc :: "hcomplex => hcomplex" where |
14408 | 19 |
--{* standard part map*} |
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
20 |
"stc x = (SOME r. x \<in> HFinite & r:SComplex & r @= x)" |
14408 | 21 |
|
22 |
||
23 |
subsection{*Closure Laws for SComplex, the Standard Complex Numbers*} |
|
24 |
||
25 |
lemma SComplex_add: "[| x \<in> SComplex; y \<in> SComplex |] ==> x + y \<in> SComplex" |
|
26 |
apply (simp add: SComplex_def, safe) |
|
27 |
apply (rule_tac x = "r + ra" in exI, simp) |
|
28 |
done |
|
29 |
||
30 |
lemma SComplex_mult: "[| x \<in> SComplex; y \<in> SComplex |] ==> x * y \<in> SComplex" |
|
31 |
apply (simp add: SComplex_def, safe) |
|
32 |
apply (rule_tac x = "r * ra" in exI, simp) |
|
33 |
done |
|
34 |
||
35 |
lemma SComplex_inverse: "x \<in> SComplex ==> inverse x \<in> SComplex" |
|
36 |
apply (simp add: SComplex_def) |
|
17373
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17318
diff
changeset
|
37 |
apply (blast intro: star_of_inverse [symmetric]) |
14408 | 38 |
done |
39 |
||
40 |
lemma SComplex_divide: "[| x \<in> SComplex; y \<in> SComplex |] ==> x/y \<in> SComplex" |
|
14430
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14408
diff
changeset
|
41 |
by (simp add: SComplex_mult SComplex_inverse divide_inverse) |
14408 | 42 |
|
43 |
lemma SComplex_minus: "x \<in> SComplex ==> -x \<in> SComplex" |
|
44 |
apply (simp add: SComplex_def) |
|
17373
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17318
diff
changeset
|
45 |
apply (blast intro: star_of_minus [symmetric]) |
14408 | 46 |
done |
47 |
||
48 |
lemma SComplex_minus_iff [simp]: "(-x \<in> SComplex) = (x \<in> SComplex)" |
|
49 |
apply auto |
|
50 |
apply (erule_tac [2] SComplex_minus) |
|
51 |
apply (drule SComplex_minus, auto) |
|
52 |
done |
|
53 |
||
54 |
lemma SComplex_diff: "[| x \<in> SComplex; y \<in> SComplex |] ==> x - y \<in> SComplex" |
|
55 |
by (simp add: diff_minus SComplex_add) |
|
56 |
||
57 |
lemma SComplex_add_cancel: |
|
58 |
"[| x + y \<in> SComplex; y \<in> SComplex |] ==> x \<in> SComplex" |
|
59 |
by (drule SComplex_diff, assumption, simp) |
|
60 |
||
61 |
lemma SReal_hcmod_hcomplex_of_complex [simp]: |
|
62 |
"hcmod (hcomplex_of_complex r) \<in> Reals" |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
63 |
by (auto simp add: hcmod SReal_def star_of_def) |
14408 | 64 |
|
65 |
lemma SReal_hcmod_number_of [simp]: "hcmod (number_of w ::hcomplex) \<in> Reals" |
|
17373
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17318
diff
changeset
|
66 |
apply (subst star_of_number_of [symmetric]) |
14408 | 67 |
apply (rule SReal_hcmod_hcomplex_of_complex) |
68 |
done |
|
69 |
||
70 |
lemma SReal_hcmod_SComplex: "x \<in> SComplex ==> hcmod x \<in> Reals" |
|
71 |
by (auto simp add: SComplex_def) |
|
72 |
||
73 |
lemma SComplex_hcomplex_of_complex [simp]: "hcomplex_of_complex x \<in> SComplex" |
|
74 |
by (simp add: SComplex_def) |
|
75 |
||
76 |
lemma SComplex_number_of [simp]: "(number_of w ::hcomplex) \<in> SComplex" |
|
17373
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17318
diff
changeset
|
77 |
apply (subst star_of_number_of [symmetric]) |
14408 | 78 |
apply (rule SComplex_hcomplex_of_complex) |
79 |
done |
|
80 |
||
81 |
lemma SComplex_divide_number_of: |
|
82 |
"r \<in> SComplex ==> r/(number_of w::hcomplex) \<in> SComplex" |
|
14430
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14408
diff
changeset
|
83 |
apply (simp only: divide_inverse) |
14408 | 84 |
apply (blast intro!: SComplex_number_of SComplex_mult SComplex_inverse) |
85 |
done |
|
86 |
||
87 |
lemma SComplex_UNIV_complex: |
|
88 |
"{x. hcomplex_of_complex x \<in> SComplex} = (UNIV::complex set)" |
|
89 |
by (simp add: SComplex_def) |
|
90 |
||
91 |
lemma SComplex_iff: "(x \<in> SComplex) = (\<exists>y. x = hcomplex_of_complex y)" |
|
92 |
by (simp add: SComplex_def) |
|
93 |
||
94 |
lemma hcomplex_of_complex_image: |
|
95 |
"hcomplex_of_complex `(UNIV::complex set) = SComplex" |
|
96 |
by (auto simp add: SComplex_def) |
|
97 |
||
98 |
lemma inv_hcomplex_of_complex_image: "inv hcomplex_of_complex `SComplex = UNIV" |
|
99 |
apply (auto simp add: SComplex_def) |
|
100 |
apply (rule inj_hcomplex_of_complex [THEN inv_f_f, THEN subst], blast) |
|
101 |
done |
|
102 |
||
103 |
lemma SComplex_hcomplex_of_complex_image: |
|
104 |
"[| \<exists>x. x: P; P \<le> SComplex |] ==> \<exists>Q. P = hcomplex_of_complex ` Q" |
|
105 |
apply (simp add: SComplex_def, blast) |
|
106 |
done |
|
107 |
||
108 |
lemma SComplex_SReal_dense: |
|
109 |
"[| x \<in> SComplex; y \<in> SComplex; hcmod x < hcmod y |
|
110 |
|] ==> \<exists>r \<in> Reals. hcmod x< r & r < hcmod y" |
|
111 |
apply (auto intro: SReal_dense simp add: SReal_hcmod_SComplex) |
|
112 |
done |
|
113 |
||
114 |
lemma SComplex_hcmod_SReal: |
|
115 |
"z \<in> SComplex ==> hcmod z \<in> Reals" |
|
20686 | 116 |
by (auto simp add: SComplex_def) |
14408 | 117 |
|
118 |
lemma SComplex_zero [simp]: "0 \<in> SComplex" |
|
17373
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17318
diff
changeset
|
119 |
by (simp add: SComplex_def) |
14408 | 120 |
|
121 |
lemma SComplex_one [simp]: "1 \<in> SComplex" |
|
17373
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17318
diff
changeset
|
122 |
by (simp add: SComplex_def) |
14408 | 123 |
|
124 |
(* |
|
125 |
Goalw [SComplex_def,SReal_def] "hcmod z \<in> Reals ==> z \<in> SComplex" |
|
126 |
by (res_inst_tac [("z","z")] eq_Abs_hcomplex 1); |
|
127 |
by (auto_tac (claset(),simpset() addsimps [hcmod,hypreal_of_real_def, |
|
128 |
hcomplex_of_complex_def,cmod_def])); |
|
129 |
*) |
|
130 |
||
131 |
||
132 |
subsection{*The Finite Elements form a Subring*} |
|
133 |
||
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
134 |
lemma SComplex_subset_HFinite [simp]: "SComplex \<le> HFinite" |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
135 |
apply (auto simp add: SComplex_def HFinite_def) |
14408 | 136 |
apply (rule_tac x = "1 + hcmod (hcomplex_of_complex r) " in bexI) |
137 |
apply (auto intro: SReal_add) |
|
138 |
done |
|
139 |
||
140 |
lemma HFinite_hcmod_hcomplex_of_complex [simp]: |
|
141 |
"hcmod (hcomplex_of_complex r) \<in> HFinite" |
|
142 |
by (auto intro!: SReal_subset_HFinite [THEN subsetD]) |
|
143 |
||
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
144 |
lemma HFinite_hcomplex_of_complex: "hcomplex_of_complex x \<in> HFinite" |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
145 |
by (rule HFinite_star_of) |
14408 | 146 |
|
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
147 |
lemma HFinite_hcmod_iff: "(x \<in> HFinite) = (hcmod x \<in> HFinite)" |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
148 |
by (simp add: HFinite_def) |
14408 | 149 |
|
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
150 |
lemma HFinite_bounded_hcmod: |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
151 |
"[|x \<in> HFinite; y \<le> hcmod x; 0 \<le> y |] ==> y: HFinite" |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
152 |
by (auto intro: HFinite_bounded simp add: HFinite_hcmod_iff) |
14408 | 153 |
|
154 |
||
155 |
subsection{*The Complex Infinitesimals form a Subring*} |
|
156 |
||
157 |
lemma hcomplex_sum_of_halves: "x/(2::hcomplex) + x/(2::hcomplex) = x" |
|
158 |
by auto |
|
159 |
||
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
160 |
lemma Infinitesimal_hcmod_iff: |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
161 |
"(z \<in> Infinitesimal) = (hcmod z \<in> Infinitesimal)" |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
162 |
by (simp add: Infinitesimal_def) |
14408 | 163 |
|
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
164 |
lemma HInfinite_hcmod_iff: "(z \<in> HInfinite) = (hcmod z \<in> HInfinite)" |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
165 |
by (simp add: HInfinite_def) |
14408 | 166 |
|
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
167 |
lemma HFinite_diff_Infinitesimal_hcmod: |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
168 |
"x \<in> HFinite - Infinitesimal ==> hcmod x \<in> HFinite - Infinitesimal" |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
169 |
by (simp add: HFinite_hcmod_iff Infinitesimal_hcmod_iff) |
14408 | 170 |
|
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
171 |
lemma hcmod_less_Infinitesimal: |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
172 |
"[| e \<in> Infinitesimal; hcmod x < hcmod e |] ==> x \<in> Infinitesimal" |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
173 |
by (auto elim: hrabs_less_Infinitesimal simp add: Infinitesimal_hcmod_iff) |
14408 | 174 |
|
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
175 |
lemma hcmod_le_Infinitesimal: |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
176 |
"[| e \<in> Infinitesimal; hcmod x \<le> hcmod e |] ==> x \<in> Infinitesimal" |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
177 |
by (auto elim: hrabs_le_Infinitesimal simp add: Infinitesimal_hcmod_iff) |
14408 | 178 |
|
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
179 |
lemma Infinitesimal_interval_hcmod: |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
180 |
"[| e \<in> Infinitesimal; |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
181 |
e' \<in> Infinitesimal; |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
182 |
hcmod e' < hcmod x ; hcmod x < hcmod e |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
183 |
|] ==> x \<in> Infinitesimal" |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
184 |
by (auto intro: Infinitesimal_interval simp add: Infinitesimal_hcmod_iff) |
14408 | 185 |
|
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
186 |
lemma Infinitesimal_interval2_hcmod: |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
187 |
"[| e \<in> Infinitesimal; |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
188 |
e' \<in> Infinitesimal; |
14408 | 189 |
hcmod e' \<le> hcmod x ; hcmod x \<le> hcmod e |
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
190 |
|] ==> x \<in> Infinitesimal" |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
191 |
by (auto intro: Infinitesimal_interval2 simp add: Infinitesimal_hcmod_iff) |
14408 | 192 |
|
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
193 |
lemma Infinitesimal_hcomplex_of_complex_mult: |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
194 |
"x \<in> Infinitesimal ==> x * hcomplex_of_complex r \<in> Infinitesimal" |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
195 |
by (auto intro!: Infinitesimal_HFinite_mult simp add: Infinitesimal_hcmod_iff hcmod_mult) |
14408 | 196 |
|
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
197 |
lemma Infinitesimal_hcomplex_of_complex_mult2: |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
198 |
"x \<in> Infinitesimal ==> hcomplex_of_complex r * x \<in> Infinitesimal" |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
199 |
by (auto intro!: Infinitesimal_HFinite_mult2 simp add: Infinitesimal_hcmod_iff hcmod_mult) |
14408 | 200 |
|
201 |
||
202 |
subsection{*The ``Infinitely Close'' Relation*} |
|
203 |
||
204 |
(* |
|
205 |
Goalw [capprox_def,approx_def] "(z @c= w) = (hcmod z @= hcmod w)" |
|
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
206 |
by (auto_tac (claset(),simpset() addsimps [Infinitesimal_hcmod_iff])); |
14408 | 207 |
*) |
208 |
||
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
209 |
lemma approx_mult_subst_SComplex: |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
210 |
"[| u @= x*hcomplex_of_complex v; x @= y |] |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
211 |
==> u @= y*hcomplex_of_complex v" |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
212 |
by (auto intro: approx_mult_subst2) |
14408 | 213 |
|
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
214 |
lemma approx_hcomplex_of_complex_HFinite: |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
215 |
"x @= hcomplex_of_complex D ==> x \<in> HFinite" |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
216 |
by (rule approx_star_of_HFinite) |
14408 | 217 |
|
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
218 |
lemma approx_mult_hcomplex_of_complex: |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
219 |
"[|a @= hcomplex_of_complex b; c @= hcomplex_of_complex d |] |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
220 |
==> a*c @= hcomplex_of_complex b * hcomplex_of_complex d" |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
221 |
by (rule approx_mult_star_of) |
14408 | 222 |
|
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
223 |
lemma approx_SComplex_mult_cancel_zero: |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
224 |
"[| a \<in> SComplex; a \<noteq> 0; a*x @= 0 |] ==> x @= 0" |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
225 |
apply (drule SComplex_inverse [THEN SComplex_subset_HFinite [THEN subsetD]]) |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
226 |
apply (auto dest: approx_mult2 simp add: mult_assoc [symmetric]) |
14408 | 227 |
done |
228 |
||
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
229 |
lemma approx_mult_SComplex1: "[| a \<in> SComplex; x @= 0 |] ==> x*a @= 0" |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
230 |
by (auto dest: SComplex_subset_HFinite [THEN subsetD] approx_mult1) |
14408 | 231 |
|
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
232 |
lemma approx_mult_SComplex2: "[| a \<in> SComplex; x @= 0 |] ==> a*x @= 0" |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
233 |
by (auto dest: SComplex_subset_HFinite [THEN subsetD] approx_mult2) |
14408 | 234 |
|
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
235 |
lemma approx_mult_SComplex_zero_cancel_iff [simp]: |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
236 |
"[|a \<in> SComplex; a \<noteq> 0 |] ==> (a*x @= 0) = (x @= 0)" |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
237 |
by (blast intro: approx_SComplex_mult_cancel_zero approx_mult_SComplex2) |
14408 | 238 |
|
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
239 |
lemma approx_SComplex_mult_cancel: |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
240 |
"[| a \<in> SComplex; a \<noteq> 0; a* w @= a*z |] ==> w @= z" |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
241 |
apply (drule SComplex_inverse [THEN SComplex_subset_HFinite [THEN subsetD]]) |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
242 |
apply (auto dest: approx_mult2 simp add: mult_assoc [symmetric]) |
14408 | 243 |
done |
244 |
||
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
245 |
lemma approx_SComplex_mult_cancel_iff1 [simp]: |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
246 |
"[| a \<in> SComplex; a \<noteq> 0|] ==> (a* w @= a*z) = (w @= z)" |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
247 |
by (auto intro!: approx_mult2 SComplex_subset_HFinite [THEN subsetD] |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
248 |
intro: approx_SComplex_mult_cancel) |
14408 | 249 |
|
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
250 |
lemma approx_hcmod_approx_zero: "(x @= y) = (hcmod (y - x) @= 0)" |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
251 |
apply (subst hcmod_diff_commute) |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
252 |
apply (simp add: approx_def Infinitesimal_hcmod_iff diff_minus) |
14408 | 253 |
done |
254 |
||
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
255 |
lemma approx_approx_zero_iff: "(x @= 0) = (hcmod x @= 0)" |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
256 |
by (simp add: approx_hcmod_approx_zero) |
14408 | 257 |
|
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
258 |
lemma approx_minus_zero_cancel_iff [simp]: "(-x @= 0) = (x @= 0)" |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
259 |
by (simp add: approx_def) |
14408 | 260 |
|
261 |
lemma Infinitesimal_hcmod_add_diff: |
|
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
262 |
"u @= 0 ==> hcmod(x + u) - hcmod x \<in> Infinitesimal" |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
263 |
apply (drule approx_approx_zero_iff [THEN iffD1]) |
14408 | 264 |
apply (rule_tac e = "hcmod u" and e' = "- hcmod u" in Infinitesimal_interval2) |
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
265 |
apply (auto simp add: mem_infmal_iff [symmetric] diff_def) |
14408 | 266 |
apply (rule_tac c1 = "hcmod x" in add_le_cancel_left [THEN iffD1]) |
267 |
apply (auto simp add: diff_minus [symmetric]) |
|
268 |
done |
|
269 |
||
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
270 |
lemma approx_hcmod_add_hcmod: "u @= 0 ==> hcmod(x + u) @= hcmod x" |
14408 | 271 |
apply (rule approx_minus_iff [THEN iffD2]) |
272 |
apply (auto intro: Infinitesimal_hcmod_add_diff simp add: mem_infmal_iff [symmetric] diff_minus [symmetric]) |
|
273 |
done |
|
274 |
||
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
275 |
lemma approx_hcmod_approx: "x @= y ==> hcmod x @= hcmod y" |
14408 | 276 |
by (auto intro: approx_hcmod_add_hcmod |
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
277 |
dest!: bex_Infinitesimal_iff2 [THEN iffD2] |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
278 |
simp add: mem_infmal_iff) |
13957 | 279 |
|
280 |
||
14408 | 281 |
subsection{*Zero is the Only Infinitesimal Complex Number*} |
282 |
||
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
283 |
lemma Infinitesimal_less_SComplex: |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
284 |
"[| x \<in> SComplex; y \<in> Infinitesimal; 0 < hcmod x |] ==> hcmod y < hcmod x" |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
285 |
by (auto intro: Infinitesimal_less_SReal SComplex_hcmod_SReal simp add: Infinitesimal_hcmod_iff) |
14408 | 286 |
|
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
287 |
lemma SComplex_Int_Infinitesimal_zero: "SComplex Int Infinitesimal = {0}" |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
288 |
by (auto simp add: SComplex_def Infinitesimal_hcmod_iff) |
14408 | 289 |
|
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
290 |
lemma SComplex_Infinitesimal_zero: |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
291 |
"[| x \<in> SComplex; x \<in> Infinitesimal|] ==> x = 0" |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
292 |
by (cut_tac SComplex_Int_Infinitesimal_zero, blast) |
14408 | 293 |
|
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
294 |
lemma SComplex_HFinite_diff_Infinitesimal: |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
295 |
"[| x \<in> SComplex; x \<noteq> 0 |] ==> x \<in> HFinite - Infinitesimal" |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
296 |
by (auto dest: SComplex_Infinitesimal_zero SComplex_subset_HFinite [THEN subsetD]) |
14408 | 297 |
|
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
298 |
lemma hcomplex_of_complex_HFinite_diff_Infinitesimal: |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
299 |
"hcomplex_of_complex x \<noteq> 0 |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
300 |
==> hcomplex_of_complex x \<in> HFinite - Infinitesimal" |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
301 |
by (rule SComplex_HFinite_diff_Infinitesimal, auto) |
14408 | 302 |
|
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
303 |
lemma hcomplex_of_complex_Infinitesimal_iff_0: |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
304 |
"(hcomplex_of_complex x \<in> Infinitesimal) = (x=0)" |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
305 |
by (rule star_of_Infinitesimal_iff_0) |
14408 | 306 |
|
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
307 |
lemma number_of_not_Infinitesimal [simp]: |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
308 |
"number_of w \<noteq> (0::hcomplex) ==> (number_of w::hcomplex) \<notin> Infinitesimal" |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
309 |
by (fast dest: SComplex_number_of [THEN SComplex_Infinitesimal_zero]) |
14408 | 310 |
|
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
311 |
lemma approx_SComplex_not_zero: |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
312 |
"[| y \<in> SComplex; x @= y; y\<noteq> 0 |] ==> x \<noteq> 0" |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
313 |
by (auto dest: SComplex_Infinitesimal_zero approx_sym [THEN mem_infmal_iff [THEN iffD2]]) |
14408 | 314 |
|
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
315 |
lemma SComplex_approx_iff: |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
316 |
"[|x \<in> SComplex; y \<in> SComplex|] ==> (x @= y) = (x = y)" |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
317 |
by (auto simp add: SComplex_def) |
14408 | 318 |
|
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
319 |
lemma number_of_Infinitesimal_iff [simp]: |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
320 |
"((number_of w :: hcomplex) \<in> Infinitesimal) = |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
321 |
(number_of w = (0::hcomplex))" |
14408 | 322 |
apply (rule iffI) |
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
323 |
apply (fast dest: SComplex_number_of [THEN SComplex_Infinitesimal_zero]) |
14408 | 324 |
apply (simp (no_asm_simp)) |
325 |
done |
|
326 |
||
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
327 |
lemma hcomplex_of_complex_approx_iff: |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
328 |
"(hcomplex_of_complex k @= hcomplex_of_complex m) = (k = m)" |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
329 |
by (rule star_of_approx_iff) |
14408 | 330 |
|
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
331 |
lemma hcomplex_of_complex_approx_number_of_iff [simp]: |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
332 |
"(hcomplex_of_complex k @= number_of w) = (k = number_of w)" |
14408 | 333 |
by (subst hcomplex_of_complex_approx_iff [symmetric], auto) |
334 |
||
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
335 |
lemma approx_unique_complex: |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
336 |
"[| r \<in> SComplex; s \<in> SComplex; r @= x; s @= x|] ==> r = s" |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
337 |
by (blast intro: SComplex_approx_iff [THEN iffD1] approx_trans2) |
14408 | 338 |
|
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
339 |
lemma hcomplex_approxD1: |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
340 |
"star_n X @= star_n Y |
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
341 |
==> star_n (%n. Re(X n)) @= star_n (%n. Re(Y n))" |
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
342 |
apply (simp (no_asm) add: approx_FreeUltrafilterNat_iff2, safe) |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
343 |
apply (drule approx_minus_iff [THEN iffD1]) |
20563 | 344 |
apply (simp add: star_n_diff mem_infmal_iff [symmetric] Infinitesimal_hcmod_iff hcmod Infinitesimal_FreeUltrafilterNat_iff2) |
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset
|
345 |
apply (drule_tac x = m in spec) |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset
|
346 |
apply (erule ultra, rule FreeUltrafilterNat_all, clarify) |
20563 | 347 |
apply (rule_tac y="cmod (X n - Y n)" in order_le_less_trans) |
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset
|
348 |
apply (case_tac "X n") |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset
|
349 |
apply (case_tac "Y n") |
20563 | 350 |
apply (auto simp add: complex_diff complex_mod |
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset
|
351 |
simp del: realpow_Suc) |
14408 | 352 |
done |
353 |
||
354 |
(* same proof *) |
|
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
355 |
lemma hcomplex_approxD2: |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
356 |
"star_n X @= star_n Y |
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
357 |
==> star_n (%n. Im(X n)) @= star_n (%n. Im(Y n))" |
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
358 |
apply (simp (no_asm) add: approx_FreeUltrafilterNat_iff2, safe) |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
359 |
apply (drule approx_minus_iff [THEN iffD1]) |
20563 | 360 |
apply (simp add: star_n_diff mem_infmal_iff [symmetric] Infinitesimal_hcmod_iff hcmod Infinitesimal_FreeUltrafilterNat_iff2) |
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset
|
361 |
apply (drule_tac x = m in spec) |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset
|
362 |
apply (erule ultra, rule FreeUltrafilterNat_all, clarify) |
20563 | 363 |
apply (rule_tac y="cmod (X n - Y n)" in order_le_less_trans) |
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset
|
364 |
apply (case_tac "X n") |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset
|
365 |
apply (case_tac "Y n") |
20563 | 366 |
apply (auto simp add: complex_diff complex_mod |
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset
|
367 |
simp del: realpow_Suc) |
14408 | 368 |
done |
369 |
||
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
370 |
lemma hcomplex_approxI: |
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
371 |
"[| star_n (%n. Re(X n)) @= star_n (%n. Re(Y n)); |
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
372 |
star_n (%n. Im(X n)) @= star_n (%n. Im(Y n)) |
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
373 |
|] ==> star_n X @= star_n Y" |
14408 | 374 |
apply (drule approx_minus_iff [THEN iffD1]) |
375 |
apply (drule approx_minus_iff [THEN iffD1]) |
|
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
376 |
apply (rule approx_minus_iff [THEN iffD2]) |
20563 | 377 |
apply (auto simp add: mem_infmal_iff [symmetric] mem_infmal_iff [symmetric] star_n_diff Infinitesimal_hcmod_iff hcmod Infinitesimal_FreeUltrafilterNat_iff) |
14408 | 378 |
apply (drule_tac x = "u/2" in spec) |
379 |
apply (drule_tac x = "u/2" in spec, auto, ultra) |
|
380 |
apply (case_tac "X x") |
|
381 |
apply (case_tac "Y x") |
|
20563 | 382 |
apply (auto simp add: complex_diff complex_mod snd_conv fst_conv numeral_2_eq_2) |
14408 | 383 |
apply (rename_tac a b c d) |
20563 | 384 |
apply (subgoal_tac "sqrt (abs (a - c) ^ 2 + abs (b - d) ^ 2) < u") |
14408 | 385 |
apply (rule_tac [2] lemma_sqrt_hcomplex_capprox, auto) |
386 |
apply (simp add: power2_eq_square) |
|
387 |
done |
|
388 |
||
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
389 |
lemma approx_approx_iff: |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
390 |
"(star_n X @= star_n Y) = |
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
391 |
(star_n (%n. Re(X n)) @= star_n (%n. Re(Y n)) & |
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
392 |
star_n (%n. Im(X n)) @= star_n (%n. Im(Y n)))" |
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
393 |
apply (blast intro: hcomplex_approxI hcomplex_approxD1 hcomplex_approxD2) |
14408 | 394 |
done |
395 |
||
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
396 |
lemma hcomplex_of_hypreal_approx_iff [simp]: |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
397 |
"(hcomplex_of_hypreal x @= hcomplex_of_hypreal z) = (x @= z)" |
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
398 |
apply (cases x, cases z) |
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
399 |
apply (simp add: hcomplex_of_hypreal approx_approx_iff) |
14408 | 400 |
done |
401 |
||
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
402 |
lemma HFinite_HFinite_Re: |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
403 |
"star_n X \<in> HFinite |
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
404 |
==> star_n (%n. Re(X n)) \<in> HFinite" |
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
405 |
apply (auto simp add: HFinite_hcmod_iff hcmod HFinite_FreeUltrafilterNat_iff) |
14408 | 406 |
apply (rule_tac x = u in exI, ultra) |
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset
|
407 |
apply (case_tac "X x") |
14408 | 408 |
apply (auto simp add: complex_mod numeral_2_eq_2 simp del: realpow_Suc) |
409 |
apply (rule ccontr, drule linorder_not_less [THEN iffD1]) |
|
410 |
apply (drule order_less_le_trans, assumption) |
|
411 |
apply (drule real_sqrt_ge_abs1 [THEN [2] order_less_le_trans]) |
|
412 |
apply (auto simp add: numeral_2_eq_2 [symmetric]) |
|
413 |
done |
|
414 |
||
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
415 |
lemma HFinite_HFinite_Im: |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
416 |
"star_n X \<in> HFinite |
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
417 |
==> star_n (%n. Im(X n)) \<in> HFinite" |
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
418 |
apply (auto simp add: HFinite_hcmod_iff hcmod HFinite_FreeUltrafilterNat_iff) |
14408 | 419 |
apply (rule_tac x = u in exI, ultra) |
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset
|
420 |
apply (case_tac "X x") |
14408 | 421 |
apply (auto simp add: complex_mod simp del: realpow_Suc) |
422 |
apply (rule ccontr, drule linorder_not_less [THEN iffD1]) |
|
423 |
apply (drule order_less_le_trans, assumption) |
|
424 |
apply (drule real_sqrt_ge_abs2 [THEN [2] order_less_le_trans], auto) |
|
425 |
done |
|
426 |
||
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
427 |
lemma HFinite_Re_Im_HFinite: |
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
428 |
"[| star_n (%n. Re(X n)) \<in> HFinite; |
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
429 |
star_n (%n. Im(X n)) \<in> HFinite |
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
430 |
|] ==> star_n X \<in> HFinite" |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
431 |
apply (auto simp add: HFinite_hcmod_iff hcmod HFinite_FreeUltrafilterNat_iff) |
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset
|
432 |
apply (rename_tac u v) |
14408 | 433 |
apply (rule_tac x = "2* (u + v) " in exI) |
434 |
apply ultra |
|
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset
|
435 |
apply (case_tac "X x") |
14408 | 436 |
apply (auto simp add: complex_mod numeral_2_eq_2 simp del: realpow_Suc) |
437 |
apply (subgoal_tac "0 < u") |
|
438 |
prefer 2 apply arith |
|
439 |
apply (subgoal_tac "0 < v") |
|
440 |
prefer 2 apply arith |
|
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset
|
441 |
apply (subgoal_tac "sqrt (abs (Re (X x)) ^ 2 + abs (Im (X x)) ^ 2) < 2*u + 2*v") |
20432
07ec57376051
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20256
diff
changeset
|
442 |
apply (rule_tac [2] lemma_sqrt_hcomplex_capprox, auto) |
14408 | 443 |
apply (simp add: power2_eq_square) |
444 |
done |
|
445 |
||
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
446 |
lemma HFinite_HFinite_iff: |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
447 |
"(star_n X \<in> HFinite) = |
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
448 |
(star_n (%n. Re(X n)) \<in> HFinite & |
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
449 |
star_n (%n. Im(X n)) \<in> HFinite)" |
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
450 |
by (blast intro: HFinite_Re_Im_HFinite HFinite_HFinite_Im HFinite_HFinite_Re) |
14408 | 451 |
|
452 |
lemma SComplex_Re_SReal: |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
453 |
"star_n X \<in> SComplex |
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
454 |
==> star_n (%n. Re(X n)) \<in> Reals" |
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
455 |
apply (auto simp add: SComplex_def SReal_def star_of_def star_n_eq_iff) |
14408 | 456 |
apply (rule_tac x = "Re r" in exI, ultra) |
457 |
done |
|
458 |
||
459 |
lemma SComplex_Im_SReal: |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
460 |
"star_n X \<in> SComplex |
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
461 |
==> star_n (%n. Im(X n)) \<in> Reals" |
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
462 |
apply (auto simp add: SComplex_def SReal_def star_of_def star_n_eq_iff) |
14408 | 463 |
apply (rule_tac x = "Im r" in exI, ultra) |
464 |
done |
|
465 |
||
466 |
lemma Reals_Re_Im_SComplex: |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
467 |
"[| star_n (%n. Re(X n)) \<in> Reals; |
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
468 |
star_n (%n. Im(X n)) \<in> Reals |
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
469 |
|] ==> star_n X \<in> SComplex" |
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
470 |
apply (auto simp add: SComplex_def SReal_def star_of_def star_n_eq_iff) |
14408 | 471 |
apply (rule_tac x = "Complex r ra" in exI, ultra) |
472 |
done |
|
473 |
||
474 |
lemma SComplex_SReal_iff: |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
475 |
"(star_n X \<in> SComplex) = |
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
476 |
(star_n (%n. Re(X n)) \<in> Reals & |
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
477 |
star_n (%n. Im(X n)) \<in> Reals)" |
14408 | 478 |
by (blast intro: SComplex_Re_SReal SComplex_Im_SReal Reals_Re_Im_SComplex) |
479 |
||
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
480 |
lemma Infinitesimal_Infinitesimal_iff: |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
481 |
"(star_n X \<in> Infinitesimal) = |
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
482 |
(star_n (%n. Re(X n)) \<in> Infinitesimal & |
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
483 |
star_n (%n. Im(X n)) \<in> Infinitesimal)" |
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
484 |
by (simp add: mem_infmal_iff star_n_zero_num approx_approx_iff) |
14408 | 485 |
|
17300 | 486 |
lemma eq_Abs_star_EX: |
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
487 |
"(\<exists>t. P t) = (\<exists>X. P (star_n X))" |
17429
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
17373
diff
changeset
|
488 |
by (rule ex_star_eq) |
14408 | 489 |
|
17300 | 490 |
lemma eq_Abs_star_Bex: |
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
491 |
"(\<exists>t \<in> A. P t) = (\<exists>X. star_n X \<in> A & P (star_n X))" |
17429
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
17373
diff
changeset
|
492 |
by (simp add: Bex_def ex_star_eq) |
14408 | 493 |
|
494 |
(* Here we go - easy proof now!! *) |
|
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
495 |
lemma stc_part_Ex: "x:HFinite ==> \<exists>t \<in> SComplex. x @= t" |
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
496 |
apply (cases x) |
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
497 |
apply (auto simp add: HFinite_HFinite_iff eq_Abs_star_Bex SComplex_SReal_iff approx_approx_iff) |
14408 | 498 |
apply (drule st_part_Ex, safe)+ |
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
499 |
apply (rule_tac x = t in star_cases) |
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
500 |
apply (rule_tac x = ta in star_cases, auto) |
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
501 |
apply (rule_tac x = "%n. Complex (Xa n) (Xb n) " in exI) |
14408 | 502 |
apply auto |
503 |
done |
|
504 |
||
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
505 |
lemma stc_part_Ex1: "x:HFinite ==> EX! t. t \<in> SComplex & x @= t" |
14408 | 506 |
apply (drule stc_part_Ex, safe) |
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
507 |
apply (drule_tac [2] approx_sym, drule_tac [2] approx_sym, drule_tac [2] approx_sym) |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
508 |
apply (auto intro!: approx_unique_complex) |
14408 | 509 |
done |
510 |
||
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
511 |
lemmas hcomplex_of_complex_approx_inverse = |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
512 |
hcomplex_of_complex_HFinite_diff_Infinitesimal [THEN [2] approx_inverse] |
14408 | 513 |
|
514 |
||
515 |
subsection{*Theorems About Monads*} |
|
516 |
||
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
517 |
lemma monad_zero_hcmod_iff: "(x \<in> monad 0) = (hcmod x:monad 0)" |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
518 |
by (simp add: Infinitesimal_monad_zero_iff [symmetric] Infinitesimal_hcmod_iff) |
14408 | 519 |
|
520 |
||
521 |
subsection{*Theorems About Standard Part*} |
|
522 |
||
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
523 |
lemma stc_approx_self: "x \<in> HFinite ==> stc x @= x" |
14408 | 524 |
apply (simp add: stc_def) |
525 |
apply (frule stc_part_Ex, safe) |
|
526 |
apply (rule someI2) |
|
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
527 |
apply (auto intro: approx_sym) |
14408 | 528 |
done |
529 |
||
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
530 |
lemma stc_SComplex: "x \<in> HFinite ==> stc x \<in> SComplex" |
14408 | 531 |
apply (simp add: stc_def) |
532 |
apply (frule stc_part_Ex, safe) |
|
533 |
apply (rule someI2) |
|
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
534 |
apply (auto intro: approx_sym) |
14408 | 535 |
done |
536 |
||
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
537 |
lemma stc_HFinite: "x \<in> HFinite ==> stc x \<in> HFinite" |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
538 |
by (erule stc_SComplex [THEN SComplex_subset_HFinite [THEN subsetD]]) |
14408 | 539 |
|
20724 | 540 |
lemma stc_unique: "\<lbrakk>y \<in> SComplex; y \<approx> x\<rbrakk> \<Longrightarrow> stc x = y" |
541 |
apply (frule SComplex_subset_HFinite [THEN subsetD]) |
|
542 |
apply (drule (1) approx_HFinite) |
|
543 |
apply (unfold stc_def) |
|
14408 | 544 |
apply (rule some_equality) |
20724 | 545 |
apply (auto intro: approx_unique_complex) |
546 |
done |
|
547 |
||
548 |
lemma stc_SComplex_eq [simp]: "x \<in> SComplex ==> stc x = x" |
|
549 |
apply (erule stc_unique) |
|
550 |
apply (rule approx_refl) |
|
14408 | 551 |
done |
552 |
||
553 |
lemma stc_hcomplex_of_complex: |
|
554 |
"stc (hcomplex_of_complex x) = hcomplex_of_complex x" |
|
555 |
by auto |
|
556 |
||
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
557 |
lemma stc_eq_approx: |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
558 |
"[| x \<in> HFinite; y \<in> HFinite; stc x = stc y |] ==> x @= y" |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
559 |
by (auto dest!: stc_approx_self elim!: approx_trans3) |
14408 | 560 |
|
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
561 |
lemma approx_stc_eq: |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
562 |
"[| x \<in> HFinite; y \<in> HFinite; x @= y |] ==> stc x = stc y" |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
563 |
by (blast intro: approx_trans approx_trans2 SComplex_approx_iff [THEN iffD1] |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
564 |
dest: stc_approx_self stc_SComplex) |
13957 | 565 |
|
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
566 |
lemma stc_eq_approx_iff: |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
567 |
"[| x \<in> HFinite; y \<in> HFinite|] ==> (x @= y) = (stc x = stc y)" |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
568 |
by (blast intro: approx_stc_eq stc_eq_approx) |
14408 | 569 |
|
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
570 |
lemma stc_Infinitesimal_add_SComplex: |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
571 |
"[| x \<in> SComplex; e \<in> Infinitesimal |] ==> stc(x + e) = x" |
20724 | 572 |
apply (erule stc_unique) |
573 |
apply (erule Infinitesimal_add_approx_self) |
|
14408 | 574 |
done |
575 |
||
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
576 |
lemma stc_Infinitesimal_add_SComplex2: |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
577 |
"[| x \<in> SComplex; e \<in> Infinitesimal |] ==> stc(e + x) = x" |
20724 | 578 |
apply (erule stc_unique) |
579 |
apply (erule Infinitesimal_add_approx_self2) |
|
14408 | 580 |
done |
581 |
||
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
582 |
lemma HFinite_stc_Infinitesimal_add: |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
583 |
"x \<in> HFinite ==> \<exists>e \<in> Infinitesimal. x = stc(x) + e" |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
584 |
by (blast dest!: stc_approx_self [THEN approx_sym] bex_Infinitesimal_iff2 [THEN iffD2]) |
14408 | 585 |
|
586 |
lemma stc_add: |
|
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
587 |
"[| x \<in> HFinite; y \<in> HFinite |] ==> stc (x + y) = stc(x) + stc(y)" |
20724 | 588 |
by (simp add: stc_unique stc_SComplex stc_approx_self approx_add SComplex_add) |
14408 | 589 |
|
590 |
lemma stc_number_of [simp]: "stc (number_of w) = number_of w" |
|
591 |
by (rule SComplex_number_of [THEN stc_SComplex_eq]) |
|
592 |
||
593 |
lemma stc_zero [simp]: "stc 0 = 0" |
|
594 |
by simp |
|
595 |
||
596 |
lemma stc_one [simp]: "stc 1 = 1" |
|
597 |
by simp |
|
598 |
||
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
599 |
lemma stc_minus: "y \<in> HFinite ==> stc(-y) = -stc(y)" |
20724 | 600 |
by (simp add: stc_unique stc_SComplex stc_approx_self approx_minus) |
14408 | 601 |
|
602 |
lemma stc_diff: |
|
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
603 |
"[| x \<in> HFinite; y \<in> HFinite |] ==> stc (x-y) = stc(x) - stc(y)" |
20724 | 604 |
by (simp add: stc_unique stc_SComplex stc_approx_self approx_diff SComplex_diff) |
14408 | 605 |
|
606 |
lemma stc_mult: |
|
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
607 |
"[| x \<in> HFinite; y \<in> HFinite |] |
14408 | 608 |
==> stc (x * y) = stc(x) * stc(y)" |
20724 | 609 |
by (simp add: stc_unique stc_SComplex stc_approx_self approx_mult_HFinite SComplex_mult) |
14408 | 610 |
|
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
611 |
lemma stc_Infinitesimal: "x \<in> Infinitesimal ==> stc x = 0" |
20724 | 612 |
by (simp add: stc_unique mem_infmal_iff) |
14408 | 613 |
|
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
614 |
lemma stc_not_Infinitesimal: "stc(x) \<noteq> 0 ==> x \<notin> Infinitesimal" |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
615 |
by (fast intro: stc_Infinitesimal) |
14408 | 616 |
|
617 |
lemma stc_inverse: |
|
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
618 |
"[| x \<in> HFinite; stc x \<noteq> 0 |] |
14408 | 619 |
==> stc(inverse x) = inverse (stc x)" |
20724 | 620 |
apply (drule stc_not_Infinitesimal) |
621 |
apply (simp add: stc_unique stc_SComplex stc_approx_self approx_inverse SComplex_inverse) |
|
14408 | 622 |
done |
623 |
||
624 |
lemma stc_divide [simp]: |
|
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
625 |
"[| x \<in> HFinite; y \<in> HFinite; stc y \<noteq> 0 |] |
14408 | 626 |
==> stc(x/y) = (stc x) / (stc y)" |
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
627 |
by (simp add: divide_inverse stc_mult stc_not_Infinitesimal HFinite_inverse stc_inverse) |
14408 | 628 |
|
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
629 |
lemma stc_idempotent [simp]: "x \<in> HFinite ==> stc(stc(x)) = stc(x)" |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
630 |
by (blast intro: stc_HFinite stc_approx_self approx_stc_eq) |
14408 | 631 |
|
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
632 |
lemma HFinite_HFinite_hcomplex_of_hypreal: |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
633 |
"z \<in> HFinite ==> hcomplex_of_hypreal z \<in> HFinite" |
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
634 |
apply (cases z) |
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
635 |
apply (simp add: hcomplex_of_hypreal HFinite_HFinite_iff star_n_zero_num [symmetric]) |
14408 | 636 |
done |
637 |
||
638 |
lemma SComplex_SReal_hcomplex_of_hypreal: |
|
639 |
"x \<in> Reals ==> hcomplex_of_hypreal x \<in> SComplex" |
|
20724 | 640 |
by (auto simp add: SReal_def Standard_def hcomplex_of_hypreal_def |
20557
81dd3679f92c
complex_of_real abbreviates of_real::real=>complex;
huffman
parents:
20552
diff
changeset
|
641 |
simp del: star_of_of_real) |
14408 | 642 |
|
643 |
lemma stc_hcomplex_of_hypreal: |
|
644 |
"z \<in> HFinite ==> stc(hcomplex_of_hypreal z) = hcomplex_of_hypreal (st z)" |
|
20724 | 645 |
apply (rule stc_unique) |
646 |
apply (rule SComplex_SReal_hcomplex_of_hypreal) |
|
647 |
apply (erule st_SReal) |
|
648 |
apply (simp add: hcomplex_of_hypreal_approx_iff st_approx_self) |
|
14408 | 649 |
done |
650 |
||
651 |
(* |
|
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
652 |
Goal "x \<in> HFinite ==> hcmod(stc x) = st(hcmod x)" |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
653 |
by (dtac stc_approx_self 1) |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
654 |
by (auto_tac (claset(),simpset() addsimps [bex_Infinitesimal_iff2 RS sym])); |
14408 | 655 |
|
656 |
||
657 |
approx_hcmod_add_hcmod |
|
658 |
*) |
|
659 |
||
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
660 |
lemma Infinitesimal_hcnj_iff [simp]: |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
661 |
"(hcnj z \<in> Infinitesimal) = (z \<in> Infinitesimal)" |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
662 |
by (simp add: Infinitesimal_hcmod_iff) |
14408 | 663 |
|
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
664 |
lemma HInfinite_HInfinite_iff: |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
665 |
"(star_n X \<in> HInfinite) = |
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
666 |
(star_n (%n. Re(X n)) \<in> HInfinite | |
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
667 |
star_n (%n. Im(X n)) \<in> HInfinite)" |
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
668 |
by (simp add: HInfinite_HFinite_iff HFinite_HFinite_iff) |
14408 | 669 |
|
670 |
text{*These theorems should probably be deleted*} |
|
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
671 |
lemma hcomplex_split_Infinitesimal_iff: |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
672 |
"(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y \<in> Infinitesimal) = |
14408 | 673 |
(x \<in> Infinitesimal & y \<in> Infinitesimal)" |
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
674 |
apply (cases x, cases y) |
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
675 |
apply (simp add: iii_def star_of_def star_n_add star_n_mult hcomplex_of_hypreal Infinitesimal_Infinitesimal_iff) |
14408 | 676 |
done |
677 |
||
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
678 |
lemma hcomplex_split_HFinite_iff: |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
679 |
"(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y \<in> HFinite) = |
14408 | 680 |
(x \<in> HFinite & y \<in> HFinite)" |
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
681 |
apply (cases x, cases y) |
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
682 |
apply (simp add: iii_def star_of_def star_n_add star_n_mult hcomplex_of_hypreal HFinite_HFinite_iff) |
14408 | 683 |
done |
684 |
||
685 |
lemma hcomplex_split_SComplex_iff: |
|
686 |
"(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y \<in> SComplex) = |
|
687 |
(x \<in> Reals & y \<in> Reals)" |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
688 |
apply (cases x, cases y) |
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
689 |
apply (simp add: iii_def star_of_def star_n_add star_n_mult hcomplex_of_hypreal SComplex_SReal_iff) |
14408 | 690 |
done |
691 |
||
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
692 |
lemma hcomplex_split_HInfinite_iff: |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
693 |
"(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y \<in> HInfinite) = |
14408 | 694 |
(x \<in> HInfinite | y \<in> HInfinite)" |
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
695 |
apply (cases x, cases y) |
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
696 |
apply (simp add: iii_def star_of_def star_n_add star_n_mult hcomplex_of_hypreal HInfinite_HInfinite_iff) |
14408 | 697 |
done |
698 |
||
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
699 |
lemma hcomplex_split_approx_iff: |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
700 |
"(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y @= |
14408 | 701 |
hcomplex_of_hypreal x' + iii * hcomplex_of_hypreal y') = |
702 |
(x @= x' & y @= y')" |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
703 |
apply (cases x, cases y, cases x', cases y') |
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
704 |
apply (simp add: iii_def star_of_def star_n_add star_n_mult hcomplex_of_hypreal approx_approx_iff) |
14408 | 705 |
done |
706 |
||
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
707 |
lemma complex_seq_to_hcomplex_Infinitesimal: |
14408 | 708 |
"\<forall>n. cmod (X n - x) < inverse (real (Suc n)) ==> |
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
709 |
star_n X - hcomplex_of_complex x \<in> Infinitesimal" |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
710 |
by (rule real_seq_to_hypreal_Infinitesimal [folded diff_def]) |
14408 | 711 |
|
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
712 |
lemma Infinitesimal_hcomplex_of_hypreal_epsilon [simp]: |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
713 |
"hcomplex_of_hypreal epsilon \<in> Infinitesimal" |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
714 |
by (simp add: Infinitesimal_hcmod_iff) |
14408 | 715 |
|
716 |
lemma hcomplex_of_complex_approx_zero_iff [simp]: |
|
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
717 |
"(hcomplex_of_complex z @= 0) = (z = 0)" |
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
718 |
by (simp add: star_of_zero [symmetric] del: star_of_zero) |
14408 | 719 |
|
720 |
lemma hcomplex_of_complex_approx_zero_iff2 [simp]: |
|
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
721 |
"(0 @= hcomplex_of_complex z) = (z = 0)" |
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
722 |
by (simp add: star_of_zero [symmetric] del: star_of_zero) |
14408 | 723 |
|
13957 | 724 |
end |