author | haftmann |
Wed, 02 Jul 2008 07:11:57 +0200 | |
changeset 27435 | b3f8e9bdf9a7 |
parent 27148 | 5b78e50adc49 |
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 |
22655 | 9 |
imports NSComplex "../Hyperreal/HTranscendental" |
15131 | 10 |
begin |
13957 | 11 |
|
21830 | 12 |
abbreviation |
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 |
21830 | 15 |
"SComplex \<equiv> Standard" |
13957 | 16 |
|
27435 | 17 |
definition --{* standard part map*} |
18 |
stc :: "hcomplex => hcomplex" where |
|
19 |
[code func del]: "stc x = (SOME r. x \<in> HFinite & r:SComplex & r @= x)" |
|
14408 | 20 |
|
21 |
||
22 |
subsection{*Closure Laws for SComplex, the Standard Complex Numbers*} |
|
23 |
||
24 |
lemma SComplex_minus_iff [simp]: "(-x \<in> SComplex) = (x \<in> SComplex)" |
|
22883
005be8dafce0
hcomplex_of_hypreal abbreviates of_hypreal; removed redundant lemmas
huffman
parents:
22655
diff
changeset
|
25 |
by (auto, drule Standard_minus, auto) |
14408 | 26 |
|
27 |
lemma SComplex_add_cancel: |
|
28 |
"[| x + y \<in> SComplex; y \<in> SComplex |] ==> x \<in> SComplex" |
|
22883
005be8dafce0
hcomplex_of_hypreal abbreviates of_hypreal; removed redundant lemmas
huffman
parents:
22655
diff
changeset
|
29 |
by (drule (1) Standard_diff, simp) |
14408 | 30 |
|
31 |
lemma SReal_hcmod_hcomplex_of_complex [simp]: |
|
32 |
"hcmod (hcomplex_of_complex r) \<in> Reals" |
|
21830 | 33 |
by (simp add: Reals_eq_Standard) |
14408 | 34 |
|
35 |
lemma SReal_hcmod_number_of [simp]: "hcmod (number_of w ::hcomplex) \<in> Reals" |
|
22883
005be8dafce0
hcomplex_of_hypreal abbreviates of_hypreal; removed redundant lemmas
huffman
parents:
22655
diff
changeset
|
36 |
by (simp add: Reals_eq_Standard) |
14408 | 37 |
|
38 |
lemma SReal_hcmod_SComplex: "x \<in> SComplex ==> hcmod x \<in> Reals" |
|
21830 | 39 |
by (simp add: Reals_eq_Standard) |
14408 | 40 |
|
41 |
lemma SComplex_divide_number_of: |
|
42 |
"r \<in> SComplex ==> r/(number_of w::hcomplex) \<in> SComplex" |
|
21830 | 43 |
by simp |
14408 | 44 |
|
45 |
lemma SComplex_UNIV_complex: |
|
46 |
"{x. hcomplex_of_complex x \<in> SComplex} = (UNIV::complex set)" |
|
21830 | 47 |
by simp |
14408 | 48 |
|
49 |
lemma SComplex_iff: "(x \<in> SComplex) = (\<exists>y. x = hcomplex_of_complex y)" |
|
21830 | 50 |
by (simp add: Standard_def image_def) |
14408 | 51 |
|
52 |
lemma hcomplex_of_complex_image: |
|
53 |
"hcomplex_of_complex `(UNIV::complex set) = SComplex" |
|
21830 | 54 |
by (simp add: Standard_def) |
14408 | 55 |
|
56 |
lemma inv_hcomplex_of_complex_image: "inv hcomplex_of_complex `SComplex = UNIV" |
|
21830 | 57 |
apply (auto simp add: Standard_def image_def) |
14408 | 58 |
apply (rule inj_hcomplex_of_complex [THEN inv_f_f, THEN subst], blast) |
59 |
done |
|
60 |
||
61 |
lemma SComplex_hcomplex_of_complex_image: |
|
62 |
"[| \<exists>x. x: P; P \<le> SComplex |] ==> \<exists>Q. P = hcomplex_of_complex ` Q" |
|
21830 | 63 |
apply (simp add: Standard_def, blast) |
14408 | 64 |
done |
65 |
||
66 |
lemma SComplex_SReal_dense: |
|
67 |
"[| x \<in> SComplex; y \<in> SComplex; hcmod x < hcmod y |
|
68 |
|] ==> \<exists>r \<in> Reals. hcmod x< r & r < hcmod y" |
|
69 |
apply (auto intro: SReal_dense simp add: SReal_hcmod_SComplex) |
|
70 |
done |
|
71 |
||
72 |
lemma SComplex_hcmod_SReal: |
|
73 |
"z \<in> SComplex ==> hcmod z \<in> Reals" |
|
21830 | 74 |
by (simp add: Reals_eq_Standard) |
14408 | 75 |
|
76 |
||
77 |
subsection{*The Finite Elements form a Subring*} |
|
78 |
||
79 |
lemma HFinite_hcmod_hcomplex_of_complex [simp]: |
|
80 |
"hcmod (hcomplex_of_complex r) \<in> HFinite" |
|
81 |
by (auto intro!: SReal_subset_HFinite [THEN subsetD]) |
|
82 |
||
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
83 |
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
|
84 |
by (simp add: HFinite_def) |
14408 | 85 |
|
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
86 |
lemma HFinite_bounded_hcmod: |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
87 |
"[|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
|
88 |
by (auto intro: HFinite_bounded simp add: HFinite_hcmod_iff) |
14408 | 89 |
|
90 |
||
91 |
subsection{*The Complex Infinitesimals form a Subring*} |
|
92 |
||
93 |
lemma hcomplex_sum_of_halves: "x/(2::hcomplex) + x/(2::hcomplex) = x" |
|
94 |
by auto |
|
95 |
||
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
96 |
lemma Infinitesimal_hcmod_iff: |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
97 |
"(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
|
98 |
by (simp add: Infinitesimal_def) |
14408 | 99 |
|
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
100 |
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
|
101 |
by (simp add: HInfinite_def) |
14408 | 102 |
|
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
103 |
lemma HFinite_diff_Infinitesimal_hcmod: |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
104 |
"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
|
105 |
by (simp add: HFinite_hcmod_iff Infinitesimal_hcmod_iff) |
14408 | 106 |
|
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
107 |
lemma hcmod_less_Infinitesimal: |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
108 |
"[| 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
|
109 |
by (auto elim: hrabs_less_Infinitesimal simp add: Infinitesimal_hcmod_iff) |
14408 | 110 |
|
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
111 |
lemma hcmod_le_Infinitesimal: |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
112 |
"[| 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
|
113 |
by (auto elim: hrabs_le_Infinitesimal simp add: Infinitesimal_hcmod_iff) |
14408 | 114 |
|
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
115 |
lemma Infinitesimal_interval_hcmod: |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
116 |
"[| e \<in> Infinitesimal; |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
117 |
e' \<in> Infinitesimal; |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
118 |
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
|
119 |
|] ==> x \<in> Infinitesimal" |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
120 |
by (auto intro: Infinitesimal_interval simp add: Infinitesimal_hcmod_iff) |
14408 | 121 |
|
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
122 |
lemma Infinitesimal_interval2_hcmod: |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
123 |
"[| e \<in> Infinitesimal; |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
124 |
e' \<in> Infinitesimal; |
14408 | 125 |
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
|
126 |
|] ==> x \<in> Infinitesimal" |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
127 |
by (auto intro: Infinitesimal_interval2 simp add: Infinitesimal_hcmod_iff) |
14408 | 128 |
|
129 |
||
130 |
subsection{*The ``Infinitely Close'' Relation*} |
|
131 |
||
132 |
(* |
|
133 |
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
|
134 |
by (auto_tac (claset(),simpset() addsimps [Infinitesimal_hcmod_iff])); |
14408 | 135 |
*) |
136 |
||
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
137 |
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
|
138 |
"[| a \<in> SComplex; a \<noteq> 0; a*x @= 0 |] ==> x @= 0" |
22883
005be8dafce0
hcomplex_of_hypreal abbreviates of_hypreal; removed redundant lemmas
huffman
parents:
22655
diff
changeset
|
139 |
apply (drule Standard_inverse [THEN Standard_subset_HFinite [THEN subsetD]]) |
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
140 |
apply (auto dest: approx_mult2 simp add: mult_assoc [symmetric]) |
14408 | 141 |
done |
142 |
||
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
143 |
lemma approx_mult_SComplex1: "[| a \<in> SComplex; x @= 0 |] ==> x*a @= 0" |
22883
005be8dafce0
hcomplex_of_hypreal abbreviates of_hypreal; removed redundant lemmas
huffman
parents:
22655
diff
changeset
|
144 |
by (auto dest: Standard_subset_HFinite [THEN subsetD] approx_mult1) |
14408 | 145 |
|
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
146 |
lemma approx_mult_SComplex2: "[| a \<in> SComplex; x @= 0 |] ==> a*x @= 0" |
22883
005be8dafce0
hcomplex_of_hypreal abbreviates of_hypreal; removed redundant lemmas
huffman
parents:
22655
diff
changeset
|
147 |
by (auto dest: Standard_subset_HFinite [THEN subsetD] approx_mult2) |
14408 | 148 |
|
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
149 |
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
|
150 |
"[|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
|
151 |
by (blast intro: approx_SComplex_mult_cancel_zero approx_mult_SComplex2) |
14408 | 152 |
|
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
153 |
lemma approx_SComplex_mult_cancel: |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
154 |
"[| a \<in> SComplex; a \<noteq> 0; a* w @= a*z |] ==> w @= z" |
22883
005be8dafce0
hcomplex_of_hypreal abbreviates of_hypreal; removed redundant lemmas
huffman
parents:
22655
diff
changeset
|
155 |
apply (drule Standard_inverse [THEN Standard_subset_HFinite [THEN subsetD]]) |
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
156 |
apply (auto dest: approx_mult2 simp add: mult_assoc [symmetric]) |
14408 | 157 |
done |
158 |
||
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
159 |
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
|
160 |
"[| a \<in> SComplex; a \<noteq> 0|] ==> (a* w @= a*z) = (w @= z)" |
22883
005be8dafce0
hcomplex_of_hypreal abbreviates of_hypreal; removed redundant lemmas
huffman
parents:
22655
diff
changeset
|
161 |
by (auto intro!: approx_mult2 Standard_subset_HFinite [THEN subsetD] |
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
162 |
intro: approx_SComplex_mult_cancel) |
14408 | 163 |
|
21810
b2d23672b003
generalized some lemmas; removed redundant lemmas; cleaned up some proofs
huffman
parents:
21404
diff
changeset
|
164 |
(* TODO: generalize following theorems: hcmod -> hnorm *) |
b2d23672b003
generalized some lemmas; removed redundant lemmas; cleaned up some proofs
huffman
parents:
21404
diff
changeset
|
165 |
|
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
166 |
lemma approx_hcmod_approx_zero: "(x @= y) = (hcmod (y - x) @= 0)" |
22883
005be8dafce0
hcomplex_of_hypreal abbreviates of_hypreal; removed redundant lemmas
huffman
parents:
22655
diff
changeset
|
167 |
apply (subst hnorm_minus_commute) |
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
168 |
apply (simp add: approx_def Infinitesimal_hcmod_iff diff_minus) |
14408 | 169 |
done |
170 |
||
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
171 |
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
|
172 |
by (simp add: approx_hcmod_approx_zero) |
14408 | 173 |
|
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
174 |
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
|
175 |
by (simp add: approx_def) |
14408 | 176 |
|
177 |
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
|
178 |
"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
|
179 |
apply (drule approx_approx_zero_iff [THEN iffD1]) |
14408 | 180 |
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
|
181 |
apply (auto simp add: mem_infmal_iff [symmetric] diff_def) |
14408 | 182 |
apply (rule_tac c1 = "hcmod x" in add_le_cancel_left [THEN iffD1]) |
183 |
apply (auto simp add: diff_minus [symmetric]) |
|
184 |
done |
|
185 |
||
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
186 |
lemma approx_hcmod_add_hcmod: "u @= 0 ==> hcmod(x + u) @= hcmod x" |
14408 | 187 |
apply (rule approx_minus_iff [THEN iffD2]) |
188 |
apply (auto intro: Infinitesimal_hcmod_add_diff simp add: mem_infmal_iff [symmetric] diff_minus [symmetric]) |
|
189 |
done |
|
190 |
||
13957 | 191 |
|
14408 | 192 |
subsection{*Zero is the Only Infinitesimal Complex Number*} |
193 |
||
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
194 |
lemma Infinitesimal_less_SComplex: |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
195 |
"[| 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
|
196 |
by (auto intro: Infinitesimal_less_SReal SComplex_hcmod_SReal simp add: Infinitesimal_hcmod_iff) |
14408 | 197 |
|
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
198 |
lemma SComplex_Int_Infinitesimal_zero: "SComplex Int Infinitesimal = {0}" |
21830 | 199 |
by (auto simp add: Standard_def Infinitesimal_hcmod_iff) |
14408 | 200 |
|
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
201 |
lemma SComplex_Infinitesimal_zero: |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
202 |
"[| 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
|
203 |
by (cut_tac SComplex_Int_Infinitesimal_zero, blast) |
14408 | 204 |
|
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
205 |
lemma SComplex_HFinite_diff_Infinitesimal: |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
206 |
"[| x \<in> SComplex; x \<noteq> 0 |] ==> x \<in> HFinite - Infinitesimal" |
22883
005be8dafce0
hcomplex_of_hypreal abbreviates of_hypreal; removed redundant lemmas
huffman
parents:
22655
diff
changeset
|
207 |
by (auto dest: SComplex_Infinitesimal_zero Standard_subset_HFinite [THEN subsetD]) |
14408 | 208 |
|
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
209 |
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
|
210 |
"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
|
211 |
==> 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
|
212 |
by (rule SComplex_HFinite_diff_Infinitesimal, auto) |
14408 | 213 |
|
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
214 |
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
|
215 |
"number_of w \<noteq> (0::hcomplex) ==> (number_of w::hcomplex) \<notin> Infinitesimal" |
22883
005be8dafce0
hcomplex_of_hypreal abbreviates of_hypreal; removed redundant lemmas
huffman
parents:
22655
diff
changeset
|
216 |
by (fast dest: Standard_number_of [THEN SComplex_Infinitesimal_zero]) |
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_SComplex_not_zero: |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
219 |
"[| 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
|
220 |
by (auto dest: SComplex_Infinitesimal_zero approx_sym [THEN mem_infmal_iff [THEN iffD2]]) |
14408 | 221 |
|
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
222 |
lemma SComplex_approx_iff: |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
223 |
"[|x \<in> SComplex; y \<in> SComplex|] ==> (x @= y) = (x = y)" |
21830 | 224 |
by (auto simp add: Standard_def) |
14408 | 225 |
|
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
226 |
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
|
227 |
"((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
|
228 |
(number_of w = (0::hcomplex))" |
14408 | 229 |
apply (rule iffI) |
22883
005be8dafce0
hcomplex_of_hypreal abbreviates of_hypreal; removed redundant lemmas
huffman
parents:
22655
diff
changeset
|
230 |
apply (fast dest: Standard_number_of [THEN SComplex_Infinitesimal_zero]) |
14408 | 231 |
apply (simp (no_asm_simp)) |
232 |
done |
|
233 |
||
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
234 |
lemma approx_unique_complex: |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
235 |
"[| 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
|
236 |
by (blast intro: SComplex_approx_iff [THEN iffD1] approx_trans2) |
14408 | 237 |
|
21839
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21830
diff
changeset
|
238 |
subsection {* Properties of @{term hRe}, @{term hIm} and @{term HComplex} *} |
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21830
diff
changeset
|
239 |
|
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21830
diff
changeset
|
240 |
|
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21830
diff
changeset
|
241 |
lemma abs_hRe_le_hcmod: "\<And>x. \<bar>hRe x\<bar> \<le> hcmod x" |
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21830
diff
changeset
|
242 |
by transfer (rule abs_Re_le_cmod) |
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21830
diff
changeset
|
243 |
|
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21830
diff
changeset
|
244 |
lemma abs_hIm_le_hcmod: "\<And>x. \<bar>hIm x\<bar> \<le> hcmod x" |
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21830
diff
changeset
|
245 |
by transfer (rule abs_Im_le_cmod) |
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21830
diff
changeset
|
246 |
|
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21830
diff
changeset
|
247 |
lemma Infinitesimal_hRe: "x \<in> Infinitesimal \<Longrightarrow> hRe x \<in> Infinitesimal" |
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21830
diff
changeset
|
248 |
apply (rule InfinitesimalI2, simp) |
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21830
diff
changeset
|
249 |
apply (rule order_le_less_trans [OF abs_hRe_le_hcmod]) |
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21830
diff
changeset
|
250 |
apply (erule (1) InfinitesimalD2) |
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21830
diff
changeset
|
251 |
done |
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21830
diff
changeset
|
252 |
|
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21830
diff
changeset
|
253 |
lemma Infinitesimal_hIm: "x \<in> Infinitesimal \<Longrightarrow> hIm x \<in> Infinitesimal" |
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21830
diff
changeset
|
254 |
apply (rule InfinitesimalI2, simp) |
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21830
diff
changeset
|
255 |
apply (rule order_le_less_trans [OF abs_hIm_le_hcmod]) |
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21830
diff
changeset
|
256 |
apply (erule (1) InfinitesimalD2) |
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21830
diff
changeset
|
257 |
done |
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21830
diff
changeset
|
258 |
|
22956
617140080e6a
define roots of negative reals so that many lemmas no longer require side conditions; simplification solves more goals than previously
huffman
parents:
22883
diff
changeset
|
259 |
lemma real_sqrt_lessI: "\<lbrakk>0 < u; x < u\<twosuperior>\<rbrakk> \<Longrightarrow> sqrt x < u" |
617140080e6a
define roots of negative reals so that many lemmas no longer require side conditions; simplification solves more goals than previously
huffman
parents:
22883
diff
changeset
|
260 |
(* TODO: this belongs somewhere else *) |
617140080e6a
define roots of negative reals so that many lemmas no longer require side conditions; simplification solves more goals than previously
huffman
parents:
22883
diff
changeset
|
261 |
by (frule real_sqrt_less_mono) simp |
21839
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21830
diff
changeset
|
262 |
|
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21830
diff
changeset
|
263 |
lemma hypreal_sqrt_lessI: |
22956
617140080e6a
define roots of negative reals so that many lemmas no longer require side conditions; simplification solves more goals than previously
huffman
parents:
22883
diff
changeset
|
264 |
"\<And>x u. \<lbrakk>0 < u; x < u\<twosuperior>\<rbrakk> \<Longrightarrow> ( *f* sqrt) x < u" |
21839
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21830
diff
changeset
|
265 |
by transfer (rule real_sqrt_lessI) |
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21830
diff
changeset
|
266 |
|
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21830
diff
changeset
|
267 |
lemma hypreal_sqrt_ge_zero: "\<And>x. 0 \<le> x \<Longrightarrow> 0 \<le> ( *f* sqrt) x" |
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21830
diff
changeset
|
268 |
by transfer (rule real_sqrt_ge_zero) |
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21830
diff
changeset
|
269 |
|
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21830
diff
changeset
|
270 |
lemma Infinitesimal_sqrt: |
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21830
diff
changeset
|
271 |
"\<lbrakk>x \<in> Infinitesimal; 0 \<le> x\<rbrakk> \<Longrightarrow> ( *f* sqrt) x \<in> Infinitesimal" |
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21830
diff
changeset
|
272 |
apply (rule InfinitesimalI2) |
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21830
diff
changeset
|
273 |
apply (drule_tac r="r\<twosuperior>" in InfinitesimalD2, simp) |
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21830
diff
changeset
|
274 |
apply (simp add: hypreal_sqrt_ge_zero) |
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21830
diff
changeset
|
275 |
apply (rule hypreal_sqrt_lessI, simp_all) |
14408 | 276 |
done |
277 |
||
21839
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21830
diff
changeset
|
278 |
lemma Infinitesimal_HComplex: |
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21830
diff
changeset
|
279 |
"\<lbrakk>x \<in> Infinitesimal; y \<in> Infinitesimal\<rbrakk> \<Longrightarrow> HComplex x y \<in> Infinitesimal" |
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21830
diff
changeset
|
280 |
apply (rule Infinitesimal_hcmod_iff [THEN iffD2]) |
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21830
diff
changeset
|
281 |
apply (simp add: hcmod_i) |
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21830
diff
changeset
|
282 |
apply (rule Infinitesimal_sqrt) |
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21830
diff
changeset
|
283 |
apply (rule Infinitesimal_add) |
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21830
diff
changeset
|
284 |
apply (erule Infinitesimal_hrealpow, simp) |
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21830
diff
changeset
|
285 |
apply (erule Infinitesimal_hrealpow, simp) |
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21830
diff
changeset
|
286 |
apply (rule add_nonneg_nonneg) |
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21830
diff
changeset
|
287 |
apply (rule zero_le_power2) |
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21830
diff
changeset
|
288 |
apply (rule zero_le_power2) |
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21830
diff
changeset
|
289 |
done |
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21830
diff
changeset
|
290 |
|
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21830
diff
changeset
|
291 |
lemma hcomplex_Infinitesimal_iff: |
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21830
diff
changeset
|
292 |
"(x \<in> Infinitesimal) = (hRe x \<in> Infinitesimal \<and> hIm x \<in> Infinitesimal)" |
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21830
diff
changeset
|
293 |
apply (safe intro!: Infinitesimal_hRe Infinitesimal_hIm) |
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21830
diff
changeset
|
294 |
apply (drule (1) Infinitesimal_HComplex, simp) |
14408 | 295 |
done |
296 |
||
21839
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21830
diff
changeset
|
297 |
lemma hRe_diff [simp]: "\<And>x y. hRe (x - y) = hRe x - hRe y" |
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21830
diff
changeset
|
298 |
by transfer (rule complex_Re_diff) |
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21830
diff
changeset
|
299 |
|
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21830
diff
changeset
|
300 |
lemma hIm_diff [simp]: "\<And>x y. hIm (x - y) = hIm x - hIm y" |
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21830
diff
changeset
|
301 |
by transfer (rule complex_Im_diff) |
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21830
diff
changeset
|
302 |
|
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21830
diff
changeset
|
303 |
lemma approx_hRe: "x \<approx> y \<Longrightarrow> hRe x \<approx> hRe y" |
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21830
diff
changeset
|
304 |
unfolding approx_def by (drule Infinitesimal_hRe) simp |
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21830
diff
changeset
|
305 |
|
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21830
diff
changeset
|
306 |
lemma approx_hIm: "x \<approx> y \<Longrightarrow> hIm x \<approx> hIm y" |
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21830
diff
changeset
|
307 |
unfolding approx_def by (drule Infinitesimal_hIm) simp |
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21830
diff
changeset
|
308 |
|
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21830
diff
changeset
|
309 |
lemma approx_HComplex: |
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21830
diff
changeset
|
310 |
"\<lbrakk>a \<approx> b; c \<approx> d\<rbrakk> \<Longrightarrow> HComplex a c \<approx> HComplex b d" |
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21830
diff
changeset
|
311 |
unfolding approx_def by (simp add: Infinitesimal_HComplex) |
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21830
diff
changeset
|
312 |
|
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21830
diff
changeset
|
313 |
lemma hcomplex_approx_iff: |
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21830
diff
changeset
|
314 |
"(x \<approx> y) = (hRe x \<approx> hRe y \<and> hIm x \<approx> hIm y)" |
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21830
diff
changeset
|
315 |
unfolding approx_def by (simp add: hcomplex_Infinitesimal_iff) |
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21830
diff
changeset
|
316 |
|
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21830
diff
changeset
|
317 |
lemma HFinite_hRe: "x \<in> HFinite \<Longrightarrow> hRe x \<in> HFinite" |
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21830
diff
changeset
|
318 |
apply (auto simp add: HFinite_def SReal_def) |
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21830
diff
changeset
|
319 |
apply (rule_tac x="star_of r" in exI, simp) |
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21830
diff
changeset
|
320 |
apply (erule order_le_less_trans [OF abs_hRe_le_hcmod]) |
14408 | 321 |
done |
322 |
||
21839
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21830
diff
changeset
|
323 |
lemma HFinite_hIm: "x \<in> HFinite \<Longrightarrow> hIm x \<in> HFinite" |
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21830
diff
changeset
|
324 |
apply (auto simp add: HFinite_def SReal_def) |
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21830
diff
changeset
|
325 |
apply (rule_tac x="star_of r" in exI, simp) |
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21830
diff
changeset
|
326 |
apply (erule order_le_less_trans [OF abs_hIm_le_hcmod]) |
14408 | 327 |
done |
328 |
||
21839
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21830
diff
changeset
|
329 |
lemma HFinite_HComplex: |
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21830
diff
changeset
|
330 |
"\<lbrakk>x \<in> HFinite; y \<in> HFinite\<rbrakk> \<Longrightarrow> HComplex x y \<in> HFinite" |
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21830
diff
changeset
|
331 |
apply (subgoal_tac "HComplex x 0 + HComplex 0 y \<in> HFinite", simp) |
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21830
diff
changeset
|
332 |
apply (rule HFinite_add) |
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21830
diff
changeset
|
333 |
apply (simp add: HFinite_hcmod_iff hcmod_i) |
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21830
diff
changeset
|
334 |
apply (simp add: HFinite_hcmod_iff hcmod_i) |
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21830
diff
changeset
|
335 |
done |
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21830
diff
changeset
|
336 |
|
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21830
diff
changeset
|
337 |
lemma hcomplex_HFinite_iff: |
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21830
diff
changeset
|
338 |
"(x \<in> HFinite) = (hRe x \<in> HFinite \<and> hIm x \<in> HFinite)" |
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21830
diff
changeset
|
339 |
apply (safe intro!: HFinite_hRe HFinite_hIm) |
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21830
diff
changeset
|
340 |
apply (drule (1) HFinite_HComplex, simp) |
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21830
diff
changeset
|
341 |
done |
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21830
diff
changeset
|
342 |
|
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21830
diff
changeset
|
343 |
lemma hcomplex_HInfinite_iff: |
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21830
diff
changeset
|
344 |
"(x \<in> HInfinite) = (hRe x \<in> HInfinite \<or> hIm x \<in> HInfinite)" |
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21830
diff
changeset
|
345 |
by (simp add: HInfinite_HFinite_iff hcomplex_HFinite_iff) |
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21830
diff
changeset
|
346 |
|
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
347 |
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
|
348 |
"(hcomplex_of_hypreal x @= hcomplex_of_hypreal z) = (x @= z)" |
21839
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21830
diff
changeset
|
349 |
by (simp add: hcomplex_approx_iff) |
14408 | 350 |
|
21839
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21830
diff
changeset
|
351 |
lemma Standard_HComplex: |
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21830
diff
changeset
|
352 |
"\<lbrakk>x \<in> Standard; y \<in> Standard\<rbrakk> \<Longrightarrow> HComplex x y \<in> Standard" |
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21830
diff
changeset
|
353 |
by (simp add: HComplex_def) |
14408 | 354 |
|
355 |
(* 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
|
356 |
lemma stc_part_Ex: "x:HFinite ==> \<exists>t \<in> SComplex. x @= t" |
21839
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21830
diff
changeset
|
357 |
apply (simp add: hcomplex_HFinite_iff hcomplex_approx_iff) |
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21830
diff
changeset
|
358 |
apply (rule_tac x="HComplex (st (hRe x)) (st (hIm x))" in bexI) |
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21830
diff
changeset
|
359 |
apply (simp add: st_approx_self [THEN approx_sym]) |
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21830
diff
changeset
|
360 |
apply (simp add: Standard_HComplex st_SReal [unfolded Reals_eq_Standard]) |
14408 | 361 |
done |
362 |
||
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
363 |
lemma stc_part_Ex1: "x:HFinite ==> EX! t. t \<in> SComplex & x @= t" |
14408 | 364 |
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
|
365 |
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
|
366 |
apply (auto intro!: approx_unique_complex) |
14408 | 367 |
done |
368 |
||
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
369 |
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
|
370 |
hcomplex_of_complex_HFinite_diff_Infinitesimal [THEN [2] approx_inverse] |
14408 | 371 |
|
372 |
||
373 |
subsection{*Theorems About Monads*} |
|
374 |
||
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
375 |
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
|
376 |
by (simp add: Infinitesimal_monad_zero_iff [symmetric] Infinitesimal_hcmod_iff) |
14408 | 377 |
|
378 |
||
379 |
subsection{*Theorems About Standard Part*} |
|
380 |
||
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
381 |
lemma stc_approx_self: "x \<in> HFinite ==> stc x @= x" |
14408 | 382 |
apply (simp add: stc_def) |
383 |
apply (frule stc_part_Ex, safe) |
|
384 |
apply (rule someI2) |
|
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
385 |
apply (auto intro: approx_sym) |
14408 | 386 |
done |
387 |
||
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
388 |
lemma stc_SComplex: "x \<in> HFinite ==> stc x \<in> SComplex" |
14408 | 389 |
apply (simp add: stc_def) |
390 |
apply (frule stc_part_Ex, safe) |
|
391 |
apply (rule someI2) |
|
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
392 |
apply (auto intro: approx_sym) |
14408 | 393 |
done |
394 |
||
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
395 |
lemma stc_HFinite: "x \<in> HFinite ==> stc x \<in> HFinite" |
22883
005be8dafce0
hcomplex_of_hypreal abbreviates of_hypreal; removed redundant lemmas
huffman
parents:
22655
diff
changeset
|
396 |
by (erule stc_SComplex [THEN Standard_subset_HFinite [THEN subsetD]]) |
14408 | 397 |
|
20724 | 398 |
lemma stc_unique: "\<lbrakk>y \<in> SComplex; y \<approx> x\<rbrakk> \<Longrightarrow> stc x = y" |
22883
005be8dafce0
hcomplex_of_hypreal abbreviates of_hypreal; removed redundant lemmas
huffman
parents:
22655
diff
changeset
|
399 |
apply (frule Standard_subset_HFinite [THEN subsetD]) |
20724 | 400 |
apply (drule (1) approx_HFinite) |
401 |
apply (unfold stc_def) |
|
14408 | 402 |
apply (rule some_equality) |
20724 | 403 |
apply (auto intro: approx_unique_complex) |
404 |
done |
|
405 |
||
406 |
lemma stc_SComplex_eq [simp]: "x \<in> SComplex ==> stc x = x" |
|
407 |
apply (erule stc_unique) |
|
408 |
apply (rule approx_refl) |
|
14408 | 409 |
done |
410 |
||
411 |
lemma stc_hcomplex_of_complex: |
|
412 |
"stc (hcomplex_of_complex x) = hcomplex_of_complex x" |
|
413 |
by auto |
|
414 |
||
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
415 |
lemma stc_eq_approx: |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
416 |
"[| 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
|
417 |
by (auto dest!: stc_approx_self elim!: approx_trans3) |
14408 | 418 |
|
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
419 |
lemma approx_stc_eq: |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
420 |
"[| 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
|
421 |
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
|
422 |
dest: stc_approx_self stc_SComplex) |
13957 | 423 |
|
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
424 |
lemma stc_eq_approx_iff: |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
425 |
"[| 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
|
426 |
by (blast intro: approx_stc_eq stc_eq_approx) |
14408 | 427 |
|
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
428 |
lemma stc_Infinitesimal_add_SComplex: |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
429 |
"[| x \<in> SComplex; e \<in> Infinitesimal |] ==> stc(x + e) = x" |
20724 | 430 |
apply (erule stc_unique) |
431 |
apply (erule Infinitesimal_add_approx_self) |
|
14408 | 432 |
done |
433 |
||
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
434 |
lemma stc_Infinitesimal_add_SComplex2: |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
435 |
"[| x \<in> SComplex; e \<in> Infinitesimal |] ==> stc(e + x) = x" |
20724 | 436 |
apply (erule stc_unique) |
437 |
apply (erule Infinitesimal_add_approx_self2) |
|
14408 | 438 |
done |
439 |
||
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
440 |
lemma HFinite_stc_Infinitesimal_add: |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
441 |
"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
|
442 |
by (blast dest!: stc_approx_self [THEN approx_sym] bex_Infinitesimal_iff2 [THEN iffD2]) |
14408 | 443 |
|
444 |
lemma stc_add: |
|
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
445 |
"[| x \<in> HFinite; y \<in> HFinite |] ==> stc (x + y) = stc(x) + stc(y)" |
22883
005be8dafce0
hcomplex_of_hypreal abbreviates of_hypreal; removed redundant lemmas
huffman
parents:
22655
diff
changeset
|
446 |
by (simp add: stc_unique stc_SComplex stc_approx_self approx_add) |
14408 | 447 |
|
448 |
lemma stc_number_of [simp]: "stc (number_of w) = number_of w" |
|
22883
005be8dafce0
hcomplex_of_hypreal abbreviates of_hypreal; removed redundant lemmas
huffman
parents:
22655
diff
changeset
|
449 |
by (rule Standard_number_of [THEN stc_SComplex_eq]) |
14408 | 450 |
|
451 |
lemma stc_zero [simp]: "stc 0 = 0" |
|
452 |
by simp |
|
453 |
||
454 |
lemma stc_one [simp]: "stc 1 = 1" |
|
455 |
by simp |
|
456 |
||
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
457 |
lemma stc_minus: "y \<in> HFinite ==> stc(-y) = -stc(y)" |
20724 | 458 |
by (simp add: stc_unique stc_SComplex stc_approx_self approx_minus) |
14408 | 459 |
|
460 |
lemma stc_diff: |
|
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
461 |
"[| x \<in> HFinite; y \<in> HFinite |] ==> stc (x-y) = stc(x) - stc(y)" |
22883
005be8dafce0
hcomplex_of_hypreal abbreviates of_hypreal; removed redundant lemmas
huffman
parents:
22655
diff
changeset
|
462 |
by (simp add: stc_unique stc_SComplex stc_approx_self approx_diff) |
14408 | 463 |
|
464 |
lemma stc_mult: |
|
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
465 |
"[| x \<in> HFinite; y \<in> HFinite |] |
14408 | 466 |
==> stc (x * y) = stc(x) * stc(y)" |
22883
005be8dafce0
hcomplex_of_hypreal abbreviates of_hypreal; removed redundant lemmas
huffman
parents:
22655
diff
changeset
|
467 |
by (simp add: stc_unique stc_SComplex stc_approx_self approx_mult_HFinite) |
14408 | 468 |
|
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
469 |
lemma stc_Infinitesimal: "x \<in> Infinitesimal ==> stc x = 0" |
20724 | 470 |
by (simp add: stc_unique mem_infmal_iff) |
14408 | 471 |
|
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
472 |
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
|
473 |
by (fast intro: stc_Infinitesimal) |
14408 | 474 |
|
475 |
lemma stc_inverse: |
|
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
476 |
"[| x \<in> HFinite; stc x \<noteq> 0 |] |
14408 | 477 |
==> stc(inverse x) = inverse (stc x)" |
20724 | 478 |
apply (drule stc_not_Infinitesimal) |
22883
005be8dafce0
hcomplex_of_hypreal abbreviates of_hypreal; removed redundant lemmas
huffman
parents:
22655
diff
changeset
|
479 |
apply (simp add: stc_unique stc_SComplex stc_approx_self approx_inverse) |
14408 | 480 |
done |
481 |
||
482 |
lemma stc_divide [simp]: |
|
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
483 |
"[| x \<in> HFinite; y \<in> HFinite; stc y \<noteq> 0 |] |
14408 | 484 |
==> 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
|
485 |
by (simp add: divide_inverse stc_mult stc_not_Infinitesimal HFinite_inverse stc_inverse) |
14408 | 486 |
|
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
487 |
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
|
488 |
by (blast intro: stc_HFinite stc_approx_self approx_stc_eq) |
14408 | 489 |
|
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
490 |
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
|
491 |
"z \<in> HFinite ==> hcomplex_of_hypreal z \<in> HFinite" |
21839
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21830
diff
changeset
|
492 |
by (simp add: hcomplex_HFinite_iff) |
14408 | 493 |
|
494 |
lemma SComplex_SReal_hcomplex_of_hypreal: |
|
495 |
"x \<in> Reals ==> hcomplex_of_hypreal x \<in> SComplex" |
|
22883
005be8dafce0
hcomplex_of_hypreal abbreviates of_hypreal; removed redundant lemmas
huffman
parents:
22655
diff
changeset
|
496 |
apply (rule Standard_of_hypreal) |
005be8dafce0
hcomplex_of_hypreal abbreviates of_hypreal; removed redundant lemmas
huffman
parents:
22655
diff
changeset
|
497 |
apply (simp add: Reals_eq_Standard) |
005be8dafce0
hcomplex_of_hypreal abbreviates of_hypreal; removed redundant lemmas
huffman
parents:
22655
diff
changeset
|
498 |
done |
14408 | 499 |
|
500 |
lemma stc_hcomplex_of_hypreal: |
|
501 |
"z \<in> HFinite ==> stc(hcomplex_of_hypreal z) = hcomplex_of_hypreal (st z)" |
|
20724 | 502 |
apply (rule stc_unique) |
503 |
apply (rule SComplex_SReal_hcomplex_of_hypreal) |
|
504 |
apply (erule st_SReal) |
|
505 |
apply (simp add: hcomplex_of_hypreal_approx_iff st_approx_self) |
|
14408 | 506 |
done |
507 |
||
508 |
(* |
|
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
509 |
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
|
510 |
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
|
511 |
by (auto_tac (claset(),simpset() addsimps [bex_Infinitesimal_iff2 RS sym])); |
14408 | 512 |
|
513 |
||
514 |
approx_hcmod_add_hcmod |
|
515 |
*) |
|
516 |
||
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
517 |
lemma Infinitesimal_hcnj_iff [simp]: |
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
518 |
"(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
|
519 |
by (simp add: Infinitesimal_hcmod_iff) |
14408 | 520 |
|
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset
|
521 |
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
|
522 |
"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
|
523 |
by (simp add: Infinitesimal_hcmod_iff) |
14408 | 524 |
|
13957 | 525 |
end |