author | paulson |
Tue, 10 Feb 2004 12:02:11 +0100 | |
changeset 14378 | 69c4d5997669 |
parent 14371 | c78c7da09519 |
permissions | -rw-r--r-- |
13958 | 1 |
(* Title : HTranscendental.ML |
2 |
Author : Jacques D. Fleuriot |
|
3 |
Copyright : 2001 University of Edinburgh |
|
4 |
Description : Nonstandard extensions of transcendental functions |
|
5 |
*) |
|
6 |
||
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14334
diff
changeset
|
7 |
val hpowr_Suc= thm"hpowr_Suc"; |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14334
diff
changeset
|
8 |
|
13958 | 9 |
(*-------------------------------------------------------------------------*) |
10 |
(* NS extension of square root function *) |
|
11 |
(*-------------------------------------------------------------------------*) |
|
12 |
||
13 |
Goal "( *f* sqrt) 0 = 0"; |
|
14 |
by (auto_tac (claset(),simpset() addsimps [starfun,hypreal_zero_num])); |
|
15 |
qed "STAR_sqrt_zero"; |
|
16 |
Addsimps [STAR_sqrt_zero]; |
|
17 |
||
18 |
Goal "( *f* sqrt) 1 = 1"; |
|
19 |
by (auto_tac (claset(),simpset() addsimps [starfun,hypreal_one_num])); |
|
20 |
qed "STAR_sqrt_one"; |
|
21 |
Addsimps [STAR_sqrt_one]; |
|
22 |
||
23 |
Goal "(( *f* sqrt)(x) ^ 2 = x) = (0 <= x)"; |
|
24 |
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); |
|
25 |
by (auto_tac (claset(),simpset() addsimps [hypreal_le, |
|
26 |
hypreal_zero_num, starfun,hrealpow,real_sqrt_pow2_iff] |
|
27 |
delsimps [hpowr_Suc,realpow_Suc])); |
|
28 |
qed "hypreal_sqrt_pow2_iff"; |
|
29 |
||
30 |
Goal "0 < x ==> ( *f* sqrt) (x) ^ 2 = x"; |
|
31 |
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); |
|
32 |
by (auto_tac (claset() addIs [FreeUltrafilterNat_subset, |
|
33 |
real_sqrt_gt_zero_pow2],simpset() addsimps |
|
34 |
[hypreal_less,starfun,hrealpow,hypreal_zero_num] |
|
35 |
delsimps [hpowr_Suc,realpow_Suc])); |
|
36 |
qed "hypreal_sqrt_gt_zero_pow2"; |
|
37 |
||
38 |
Goal "0 < x ==> 0 < ( *f* sqrt) (x) ^ 2"; |
|
39 |
by (forward_tac [hypreal_sqrt_gt_zero_pow2] 1); |
|
40 |
by (Auto_tac); |
|
41 |
qed "hypreal_sqrt_pow2_gt_zero"; |
|
42 |
||
43 |
Goal "0 < x ==> ( *f* sqrt) (x) ~= 0"; |
|
44 |
by (forward_tac [hypreal_sqrt_pow2_gt_zero] 1); |
|
14322 | 45 |
by (auto_tac (claset(),simpset() addsimps [numeral_2_eq_2])); |
13958 | 46 |
qed "hypreal_sqrt_not_zero"; |
47 |
||
48 |
Goal "0 < x ==> inverse (( *f* sqrt)(x)) ^ 2 = inverse x"; |
|
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14334
diff
changeset
|
49 |
by (cut_inst_tac [("n1","2"),("a1","( *f* sqrt) x")] (power_inverse RS sym) 1); |
13958 | 50 |
by (auto_tac (claset() addDs [hypreal_sqrt_gt_zero_pow2],simpset())); |
51 |
qed "hypreal_inverse_sqrt_pow2"; |
|
52 |
||
53 |
Goalw [hypreal_zero_def] |
|
54 |
"[|0 < x; 0 <y |] ==> \ |
|
55 |
\ ( *f* sqrt)(x*y) = ( *f* sqrt)(x) * ( *f* sqrt)(y)"; |
|
56 |
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); |
|
57 |
by (res_inst_tac [("z","y")] eq_Abs_hypreal 1); |
|
58 |
by (auto_tac (claset(),simpset() addsimps [starfun, |
|
59 |
hypreal_mult,hypreal_less,hypreal_zero_num])); |
|
60 |
by (ultra_tac (claset() addIs [real_sqrt_mult_distrib],simpset()) 1); |
|
61 |
qed "hypreal_sqrt_mult_distrib"; |
|
62 |
||
63 |
Goal "[|0<=x; 0<=y |] ==> \ |
|
64 |
\ ( *f* sqrt)(x*y) = ( *f* sqrt)(x) * ( *f* sqrt)(y)"; |
|
65 |
by (auto_tac (claset() addIs [hypreal_sqrt_mult_distrib], |
|
14370 | 66 |
simpset() addsimps [order_le_less])); |
13958 | 67 |
qed "hypreal_sqrt_mult_distrib2"; |
68 |
||
69 |
Goal "0 < x ==> (( *f* sqrt)(x) @= 0) = (x @= 0)"; |
|
70 |
by (auto_tac (claset(),simpset() addsimps [mem_infmal_iff RS sym])); |
|
71 |
by (rtac (hypreal_sqrt_gt_zero_pow2 RS subst) 1); |
|
72 |
by (auto_tac (claset() addIs [Infinitesimal_mult] |
|
14322 | 73 |
addSDs [(hypreal_sqrt_gt_zero_pow2 RS ssubst)],simpset() addsimps [numeral_2_eq_2])); |
13958 | 74 |
qed "hypreal_sqrt_approx_zero"; |
75 |
Addsimps [hypreal_sqrt_approx_zero]; |
|
76 |
||
77 |
Goal "0 <= x ==> (( *f* sqrt)(x) @= 0) = (x @= 0)"; |
|
14331 | 78 |
by (auto_tac (claset(), simpset() addsimps [order_le_less])); |
13958 | 79 |
qed "hypreal_sqrt_approx_zero2"; |
80 |
Addsimps [hypreal_sqrt_approx_zero2]; |
|
81 |
||
82 |
Goal "(( *f* sqrt)(x*x + y*y + z*z) @= 0) = (x*x + y*y + z*z @= 0)"; |
|
83 |
by (rtac hypreal_sqrt_approx_zero2 1); |
|
84 |
by (REPEAT(rtac hypreal_le_add_order 1)); |
|
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14334
diff
changeset
|
85 |
by (auto_tac (claset(), simpset() addsimps [zero_le_square])); |
13958 | 86 |
qed "hypreal_sqrt_sum_squares"; |
87 |
Addsimps [hypreal_sqrt_sum_squares]; |
|
88 |
||
89 |
Goal "(( *f* sqrt)(x*x + y*y) @= 0) = (x*x + y*y @= 0)"; |
|
90 |
by (rtac hypreal_sqrt_approx_zero2 1); |
|
91 |
by (rtac hypreal_le_add_order 1); |
|
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14334
diff
changeset
|
92 |
by (auto_tac (claset(), simpset() addsimps [zero_le_square])); |
13958 | 93 |
qed "hypreal_sqrt_sum_squares2"; |
94 |
Addsimps [hypreal_sqrt_sum_squares2]; |
|
95 |
||
96 |
Goal "0 < x ==> 0 < ( *f* sqrt)(x)"; |
|
97 |
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); |
|
98 |
by (auto_tac (claset(),simpset() addsimps |
|
99 |
[starfun,hypreal_zero_def,hypreal_less,hypreal_zero_num])); |
|
100 |
by (ultra_tac (claset() addIs [real_sqrt_gt_zero], simpset()) 1); |
|
101 |
qed "hypreal_sqrt_gt_zero"; |
|
102 |
||
103 |
Goal "0 <= x ==> 0 <= ( *f* sqrt)(x)"; |
|
104 |
by (auto_tac (claset() addIs [hypreal_sqrt_gt_zero], |
|
14370 | 105 |
simpset() addsimps [order_le_less ])); |
13958 | 106 |
qed "hypreal_sqrt_ge_zero"; |
107 |
||
108 |
Goal "( *f* sqrt)(x ^ 2) = abs(x)"; |
|
109 |
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); |
|
110 |
by (auto_tac (claset(),simpset() addsimps [starfun, |
|
14322 | 111 |
hypreal_hrabs,hypreal_mult,numeral_2_eq_2])); |
13958 | 112 |
qed "hypreal_sqrt_hrabs"; |
113 |
Addsimps [hypreal_sqrt_hrabs]; |
|
114 |
||
115 |
Goal "( *f* sqrt)(x*x) = abs(x)"; |
|
116 |
by (rtac (hrealpow_two RS subst) 1); |
|
14322 | 117 |
by (rtac (numeral_2_eq_2 RS subst) 1); |
13958 | 118 |
by (rtac hypreal_sqrt_hrabs 1); |
119 |
qed "hypreal_sqrt_hrabs2"; |
|
120 |
Addsimps [hypreal_sqrt_hrabs2]; |
|
121 |
||
122 |
Goal "( *f* sqrt)(x pow (hypnat_of_nat 2)) = abs(x)"; |
|
123 |
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); |
|
124 |
by (auto_tac (claset(),simpset() addsimps [starfun, |
|
14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14371
diff
changeset
|
125 |
hypreal_hrabs,hypnat_of_nat_eq,hyperpow])); |
13958 | 126 |
qed "hypreal_sqrt_hyperpow_hrabs"; |
127 |
Addsimps [hypreal_sqrt_hyperpow_hrabs]; |
|
128 |
||
129 |
Goal "[| x: HFinite; 0 <= x |] ==> st(( *f* sqrt) x) = ( *f* sqrt)(st x)"; |
|
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14334
diff
changeset
|
130 |
by (res_inst_tac [("n","1")] power_inject_base 1); |
13958 | 131 |
by (auto_tac (claset() addSIs [st_zero_le,hypreal_sqrt_ge_zero],simpset())); |
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14334
diff
changeset
|
132 |
by (rtac (st_mult RS subst) 1); |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14334
diff
changeset
|
133 |
by (rtac (hypreal_sqrt_mult_distrib2 RS subst) 3); |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14334
diff
changeset
|
134 |
by (rtac (hypreal_sqrt_mult_distrib2 RS subst) 5); |
13958 | 135 |
by (auto_tac (claset(), simpset() addsimps [st_hrabs,st_zero_le])); |
136 |
by (ALLGOALS(rtac (HFinite_square_iff RS iffD1))); |
|
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14334
diff
changeset
|
137 |
by (auto_tac (claset(), |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14334
diff
changeset
|
138 |
simpset() addsimps [hypreal_sqrt_mult_distrib2 RS sym] |
13958 | 139 |
delsimps [HFinite_square_iff])); |
140 |
qed "st_hypreal_sqrt"; |
|
141 |
||
142 |
Goal "x <= ( *f* sqrt)(x ^ 2 + y ^ 2)"; |
|
143 |
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); |
|
144 |
by (res_inst_tac [("z","y")] eq_Abs_hypreal 1); |
|
145 |
by (auto_tac (claset(),simpset() addsimps [starfun,hypreal_add, |
|
146 |
hrealpow,hypreal_le] delsimps [hpowr_Suc,realpow_Suc])); |
|
147 |
qed "hypreal_sqrt_sum_squares_ge1"; |
|
148 |
Addsimps [hypreal_sqrt_sum_squares_ge1]; |
|
149 |
||
150 |
Goal "[| 0 <= x; x : HFinite |] ==> ( *f* sqrt) x : HFinite"; |
|
14370 | 151 |
by (auto_tac (claset(),simpset() addsimps [order_le_less])); |
13958 | 152 |
by (rtac (HFinite_square_iff RS iffD1) 1); |
153 |
by (dtac hypreal_sqrt_gt_zero_pow2 1); |
|
14322 | 154 |
by (auto_tac (claset(),simpset() addsimps [numeral_2_eq_2])); |
13958 | 155 |
qed "HFinite_hypreal_sqrt"; |
156 |
||
157 |
Goal "[| 0 <= x; ( *f* sqrt) x : HFinite |] ==> x : HFinite"; |
|
14370 | 158 |
by (auto_tac (claset(),simpset() addsimps [order_le_less])); |
13958 | 159 |
by (dtac (HFinite_square_iff RS iffD2) 1); |
160 |
by (dtac hypreal_sqrt_gt_zero_pow2 1); |
|
14322 | 161 |
by (auto_tac (claset(),simpset() addsimps [numeral_2_eq_2] delsimps [HFinite_square_iff])); |
13958 | 162 |
qed "HFinite_hypreal_sqrt_imp_HFinite"; |
163 |
||
164 |
Goal "0 <= x ==> (( *f* sqrt) x : HFinite) = (x : HFinite)"; |
|
165 |
by (blast_tac (claset() addIs [HFinite_hypreal_sqrt, |
|
166 |
HFinite_hypreal_sqrt_imp_HFinite]) 1); |
|
167 |
qed "HFinite_hypreal_sqrt_iff"; |
|
168 |
Addsimps [HFinite_hypreal_sqrt_iff]; |
|
169 |
||
170 |
Goal "(( *f* sqrt)(x*x + y*y) : HFinite) = (x*x + y*y : HFinite)"; |
|
171 |
by (rtac HFinite_hypreal_sqrt_iff 1); |
|
172 |
by (rtac hypreal_le_add_order 1); |
|
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14334
diff
changeset
|
173 |
by (auto_tac (claset(), simpset() addsimps [zero_le_square])); |
13958 | 174 |
qed "HFinite_sqrt_sum_squares"; |
175 |
Addsimps [HFinite_sqrt_sum_squares]; |
|
176 |
||
177 |
Goal "[| 0 <= x; x : Infinitesimal |] ==> ( *f* sqrt) x : Infinitesimal"; |
|
14370 | 178 |
by (auto_tac (claset(),simpset() addsimps [order_le_less])); |
13958 | 179 |
by (rtac (Infinitesimal_square_iff RS iffD2) 1); |
180 |
by (dtac hypreal_sqrt_gt_zero_pow2 1); |
|
14322 | 181 |
by (auto_tac (claset(),simpset() addsimps [numeral_2_eq_2])); |
13958 | 182 |
qed "Infinitesimal_hypreal_sqrt"; |
183 |
||
184 |
Goal "[| 0 <= x; ( *f* sqrt) x : Infinitesimal |] ==> x : Infinitesimal"; |
|
14370 | 185 |
by (auto_tac (claset(),simpset() addsimps [order_le_less])); |
13958 | 186 |
by (dtac (Infinitesimal_square_iff RS iffD1) 1); |
187 |
by (dtac hypreal_sqrt_gt_zero_pow2 1); |
|
14322 | 188 |
by (auto_tac (claset(),simpset() addsimps [numeral_2_eq_2] |
13958 | 189 |
delsimps [Infinitesimal_square_iff RS sym])); |
190 |
qed "Infinitesimal_hypreal_sqrt_imp_Infinitesimal"; |
|
191 |
||
192 |
Goal "0 <= x ==> (( *f* sqrt) x : Infinitesimal) = (x : Infinitesimal)"; |
|
193 |
by (blast_tac (claset() addIs [Infinitesimal_hypreal_sqrt_imp_Infinitesimal, |
|
194 |
Infinitesimal_hypreal_sqrt]) 1); |
|
195 |
qed "Infinitesimal_hypreal_sqrt_iff"; |
|
196 |
Addsimps [Infinitesimal_hypreal_sqrt_iff]; |
|
197 |
||
198 |
Goal "(( *f* sqrt)(x*x + y*y) : Infinitesimal) = (x*x + y*y : Infinitesimal)"; |
|
199 |
by (rtac Infinitesimal_hypreal_sqrt_iff 1); |
|
200 |
by (rtac hypreal_le_add_order 1); |
|
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14334
diff
changeset
|
201 |
by (auto_tac (claset(), simpset() addsimps [zero_le_square])); |
13958 | 202 |
qed "Infinitesimal_sqrt_sum_squares"; |
203 |
Addsimps [Infinitesimal_sqrt_sum_squares]; |
|
204 |
||
205 |
Goal "[| 0 <= x; x : HInfinite |] ==> ( *f* sqrt) x : HInfinite"; |
|
14370 | 206 |
by (auto_tac (claset(),simpset() addsimps [order_le_less])); |
13958 | 207 |
by (rtac (HInfinite_square_iff RS iffD1) 1); |
208 |
by (dtac hypreal_sqrt_gt_zero_pow2 1); |
|
14322 | 209 |
by (auto_tac (claset(),simpset() addsimps [numeral_2_eq_2])); |
13958 | 210 |
qed "HInfinite_hypreal_sqrt"; |
211 |
||
212 |
Goal "[| 0 <= x; ( *f* sqrt) x : HInfinite |] ==> x : HInfinite"; |
|
14370 | 213 |
by (auto_tac (claset(),simpset() addsimps [order_le_less])); |
13958 | 214 |
by (dtac (HInfinite_square_iff RS iffD2) 1); |
215 |
by (dtac hypreal_sqrt_gt_zero_pow2 1); |
|
14322 | 216 |
by (auto_tac (claset(),simpset() addsimps [numeral_2_eq_2] |
13958 | 217 |
delsimps [HInfinite_square_iff])); |
218 |
qed "HInfinite_hypreal_sqrt_imp_HInfinite"; |
|
219 |
||
220 |
Goal "0 <= x ==> (( *f* sqrt) x : HInfinite) = (x : HInfinite)"; |
|
221 |
by (blast_tac (claset() addIs [HInfinite_hypreal_sqrt, |
|
222 |
HInfinite_hypreal_sqrt_imp_HInfinite]) 1); |
|
223 |
qed "HInfinite_hypreal_sqrt_iff"; |
|
224 |
Addsimps [HInfinite_hypreal_sqrt_iff]; |
|
225 |
||
226 |
Goal "(( *f* sqrt)(x*x + y*y) : HInfinite) = (x*x + y*y : HInfinite)"; |
|
227 |
by (rtac HInfinite_hypreal_sqrt_iff 1); |
|
228 |
by (rtac hypreal_le_add_order 1); |
|
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14334
diff
changeset
|
229 |
by (auto_tac (claset(), simpset() addsimps [zero_le_square])); |
13958 | 230 |
qed "HInfinite_sqrt_sum_squares"; |
231 |
Addsimps [HInfinite_sqrt_sum_squares]; |
|
232 |
||
233 |
Goal "sumhr (0, whn, %n. inverse (real (fact n)) * x ^ n) : HFinite"; |
|
234 |
by (auto_tac (claset() addSIs [NSBseq_HFinite_hypreal,NSconvergent_NSBseq], |
|
235 |
simpset() addsimps [starfunNat_sumr RS sym,starfunNat,hypnat_omega_def, |
|
236 |
convergent_NSconvergent_iff RS sym, summable_convergent_sumr_iff RS sym, |
|
237 |
summable_exp])); |
|
238 |
qed "HFinite_exp"; |
|
239 |
Addsimps [HFinite_exp]; |
|
240 |
||
241 |
Goalw [exphr_def] "exphr 0 = 1"; |
|
242 |
by (res_inst_tac [("n1","1")] (sumhr_split_add RS subst) 1); |
|
243 |
by (res_inst_tac [("t","1")] (hypnat_add_zero_left RS subst) 2); |
|
244 |
by (rtac hypnat_one_less_hypnat_omega 1); |
|
245 |
by (auto_tac (claset(),simpset() addsimps [sumhr,hypnat_zero_def,starfunNat, |
|
246 |
hypnat_one_def,hypnat_add,hypnat_omega_def,hypreal_add] |
|
247 |
delsimps [hypnat_add_zero_left])); |
|
248 |
by (simp_tac (simpset() addsimps [hypreal_one_num RS sym]) 1); |
|
249 |
qed "exphr_zero"; |
|
250 |
Addsimps [exphr_zero]; |
|
251 |
||
252 |
Goalw [coshr_def] "coshr 0 = 1"; |
|
253 |
by (res_inst_tac [("n1","1")] (sumhr_split_add RS subst) 1); |
|
254 |
by (res_inst_tac [("t","1")] (hypnat_add_zero_left RS subst) 2); |
|
255 |
by (rtac hypnat_one_less_hypnat_omega 1); |
|
256 |
by (auto_tac (claset(),simpset() addsimps [sumhr,hypnat_zero_def,starfunNat, |
|
257 |
hypnat_one_def,hypnat_add,hypnat_omega_def,st_add RS sym, |
|
258 |
(hypreal_one_def RS meta_eq_to_obj_eq) RS sym, |
|
259 |
(hypreal_zero_def RS meta_eq_to_obj_eq) RS sym] delsimps [hypnat_add_zero_left])); |
|
260 |
qed "coshr_zero"; |
|
261 |
Addsimps [coshr_zero]; |
|
262 |
||
263 |
Goalw [hypreal_zero_def,hypreal_one_def] "( *f* exp) 0 @= 1"; |
|
264 |
by (auto_tac (claset(),simpset() addsimps [starfun,hypreal_one_num])); |
|
265 |
qed "STAR_exp_zero_approx_one"; |
|
266 |
Addsimps [STAR_exp_zero_approx_one]; |
|
267 |
||
268 |
Goal "x: Infinitesimal ==> ( *f* exp) x @= 1"; |
|
269 |
by (case_tac "x = 0" 1); |
|
270 |
by (cut_inst_tac [("x","0")] DERIV_exp 2); |
|
271 |
by (auto_tac (claset(),simpset() addsimps [NSDERIV_DERIV_iff RS sym, |
|
272 |
nsderiv_def])); |
|
273 |
by (dres_inst_tac [("x","x")] bspec 1); |
|
274 |
by Auto_tac; |
|
275 |
by (dres_inst_tac [("c","x")] approx_mult1 1); |
|
276 |
by (auto_tac (claset() addIs [Infinitesimal_subset_HFinite RS subsetD], |
|
277 |
simpset() addsimps [hypreal_mult_assoc])); |
|
278 |
by (res_inst_tac [("d","-1")] approx_add_right_cancel 1); |
|
279 |
by (rtac (approx_sym RSN (2,approx_trans2)) 1); |
|
280 |
by (auto_tac (claset(),simpset() addsimps [mem_infmal_iff])); |
|
281 |
qed "STAR_exp_Infinitesimal"; |
|
282 |
||
283 |
Goal "( *f* exp) epsilon @= 1"; |
|
284 |
by (auto_tac (claset() addIs [STAR_exp_Infinitesimal],simpset())); |
|
285 |
qed "STAR_exp_epsilon"; |
|
286 |
Addsimps [STAR_exp_epsilon]; |
|
287 |
||
288 |
Goal "( *f* exp)(x + y) = ( *f* exp) x * ( *f* exp) y"; |
|
289 |
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); |
|
290 |
by (res_inst_tac [("z","y")] eq_Abs_hypreal 1); |
|
291 |
by (auto_tac (claset(),simpset() addsimps [starfun,hypreal_add, |
|
292 |
hypreal_mult,exp_add])); |
|
293 |
qed "STAR_exp_add"; |
|
294 |
||
295 |
Goalw [exphr_def] "exphr x = hypreal_of_real (exp x)"; |
|
296 |
by (rtac (st_hypreal_of_real RS subst) 1); |
|
297 |
by (rtac approx_st_eq 1); |
|
298 |
by Auto_tac; |
|
299 |
by (rtac (approx_minus_iff RS iffD2) 1); |
|
300 |
by (auto_tac (claset(),simpset() addsimps [mem_infmal_iff RS sym, |
|
301 |
hypreal_of_real_def,hypnat_zero_def,hypnat_omega_def,sumhr, |
|
302 |
hypreal_minus,hypreal_add])); |
|
303 |
by (rtac NSLIMSEQ_zero_Infinitesimal_hypreal 1); |
|
304 |
by (cut_inst_tac [("x3","x")] (exp_converges RS ((sums_def RS |
|
305 |
meta_eq_to_obj_eq) RS iffD1)) 1); |
|
306 |
by (dres_inst_tac [("b","- exp x")] (LIMSEQ_const RSN (2,LIMSEQ_add)) 1); |
|
307 |
by (auto_tac (claset(),simpset() addsimps [LIMSEQ_NSLIMSEQ_iff])); |
|
308 |
qed "exphr_hypreal_of_real_exp_eq"; |
|
309 |
||
310 |
Goal "0 <= x ==> (1 + x) <= ( *f* exp) x"; |
|
311 |
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); |
|
312 |
by (auto_tac (claset(),simpset() addsimps [starfun,hypreal_add, |
|
313 |
hypreal_le,hypreal_zero_num,hypreal_one_num])); |
|
314 |
by (Ultra_tac 1); |
|
315 |
qed "starfun_exp_ge_add_one_self"; |
|
316 |
Addsimps [starfun_exp_ge_add_one_self]; |
|
317 |
||
318 |
(* exp (oo) is infinite *) |
|
319 |
Goal "[| x : HInfinite; 0 <= x |] ==> ( *f* exp) x : HInfinite"; |
|
320 |
by (ftac starfun_exp_ge_add_one_self 1); |
|
321 |
by (rtac HInfinite_ge_HInfinite 1); |
|
322 |
by (rtac hypreal_le_trans 2); |
|
323 |
by (TRYALL(assume_tac) THEN Simp_tac 1); |
|
324 |
qed "starfun_exp_HInfinite"; |
|
325 |
||
326 |
Goal "( *f* exp) (-x) = inverse(( *f* exp) x)"; |
|
327 |
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); |
|
328 |
by (auto_tac (claset(),simpset() addsimps [starfun,hypreal_inverse, |
|
329 |
hypreal_minus,exp_minus])); |
|
330 |
qed "starfun_exp_minus"; |
|
331 |
||
332 |
(* exp (-oo) is infinitesimal *) |
|
333 |
Goal "[| x : HInfinite; x <= 0 |] ==> ( *f* exp) x : Infinitesimal"; |
|
334 |
by (subgoal_tac "EX y. x = - y" 1); |
|
335 |
by (res_inst_tac [("x","- x")] exI 2); |
|
336 |
by (auto_tac (claset() addSIs [HInfinite_inverse_Infinitesimal, |
|
337 |
starfun_exp_HInfinite] addIs [(starfun_exp_minus RS ssubst)], |
|
338 |
simpset() addsimps [HInfinite_minus_iff])); |
|
339 |
qed "starfun_exp_Infinitesimal"; |
|
340 |
||
341 |
Goal "0 < x ==> 1 < ( *f* exp) x"; |
|
342 |
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); |
|
343 |
by (auto_tac (claset(),simpset() addsimps [starfun,hypreal_one_num, |
|
344 |
hypreal_zero_num,hypreal_less])); |
|
345 |
by (Ultra_tac 1); |
|
346 |
qed "starfun_exp_gt_one"; |
|
347 |
Addsimps [starfun_exp_gt_one]; |
|
348 |
||
349 |
(* needs derivative of inverse function |
|
350 |
TRY a NS one today!!! |
|
351 |
||
352 |
Goal "x @= 1 ==> ( *f* ln) x @= 1"; |
|
353 |
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); |
|
354 |
by (auto_tac (claset(),simpset() addsimps [hypreal_one_def])); |
|
355 |
||
356 |
||
357 |
Goalw [nsderiv_def] "0r < x ==> NSDERIV ln x :> inverse x"; |
|
358 |
||
359 |
*) |
|
360 |
||
361 |
||
362 |
Goal "( *f* ln) (( *f* exp) x) = x"; |
|
363 |
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); |
|
364 |
by (auto_tac (claset(),simpset() addsimps [starfun])); |
|
365 |
qed "starfun_ln_exp"; |
|
366 |
Addsimps [starfun_ln_exp]; |
|
367 |
||
368 |
Goal "(( *f* exp)(( *f* ln) x) = x) = (0 < x)"; |
|
369 |
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); |
|
370 |
by (auto_tac (claset(),simpset() addsimps [starfun, |
|
371 |
hypreal_zero_num,hypreal_less])); |
|
372 |
qed "starfun_exp_ln_iff"; |
|
373 |
Addsimps [starfun_exp_ln_iff]; |
|
374 |
||
375 |
Goal "( *f* exp) u = x ==> ( *f* ln) x = u"; |
|
376 |
by (auto_tac (claset(),simpset() addsimps [starfun])); |
|
377 |
qed "starfun_exp_ln_eq"; |
|
378 |
||
379 |
Goal "0 < x ==> ( *f* ln) x < x"; |
|
380 |
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); |
|
381 |
by (auto_tac (claset(),simpset() addsimps [starfun, |
|
382 |
hypreal_zero_num,hypreal_less])); |
|
383 |
by (Ultra_tac 1); |
|
384 |
qed "starfun_ln_less_self"; |
|
385 |
Addsimps [starfun_ln_less_self]; |
|
386 |
||
387 |
Goal "1 <= x ==> 0 <= ( *f* ln) x"; |
|
388 |
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); |
|
389 |
by (auto_tac (claset(),simpset() addsimps [starfun, |
|
390 |
hypreal_zero_num,hypreal_le,hypreal_one_num])); |
|
391 |
by (Ultra_tac 1); |
|
392 |
qed "starfun_ln_ge_zero"; |
|
393 |
Addsimps [starfun_ln_ge_zero]; |
|
394 |
||
395 |
Goal "1 < x ==> 0 < ( *f* ln) x"; |
|
396 |
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); |
|
397 |
by (auto_tac (claset(),simpset() addsimps [starfun, |
|
398 |
hypreal_zero_num,hypreal_less,hypreal_one_num])); |
|
399 |
by (Ultra_tac 1); |
|
400 |
qed "starfun_ln_gt_zero"; |
|
401 |
Addsimps [starfun_ln_gt_zero]; |
|
402 |
||
403 |
Goal "[| 0 < x; x ~= 1 |] ==> ( *f* ln) x ~= 0"; |
|
404 |
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); |
|
405 |
by (auto_tac (claset(),simpset() addsimps [starfun, |
|
406 |
hypreal_zero_num,hypreal_less,hypreal_one_num])); |
|
407 |
by (ultra_tac (claset() addIs [ccontr] addDs [ln_not_eq_zero],simpset()) 1); |
|
408 |
qed "starfun_ln_not_eq_zero"; |
|
409 |
Addsimps [starfun_ln_not_eq_zero]; |
|
410 |
||
411 |
Goal "[| x: HFinite; 1 <= x |] ==> ( *f* ln) x : HFinite"; |
|
412 |
by (rtac HFinite_bounded 1); |
|
413 |
by (rtac order_less_imp_le 2); |
|
414 |
by (rtac starfun_ln_less_self 2); |
|
415 |
by (rtac order_less_le_trans 2); |
|
416 |
by Auto_tac; |
|
417 |
qed "starfun_ln_HFinite"; |
|
418 |
||
419 |
Goal "0 < x ==> ( *f* ln) (inverse x) = -( *f* ln) x"; |
|
420 |
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); |
|
421 |
by (auto_tac (claset(),simpset() addsimps [starfun, |
|
422 |
hypreal_zero_num,hypreal_minus,hypreal_inverse, |
|
423 |
hypreal_less])); |
|
424 |
by (Ultra_tac 1); |
|
425 |
by (auto_tac (claset(),simpset() addsimps [ln_inverse])); |
|
426 |
qed "starfun_ln_inverse"; |
|
427 |
||
428 |
Goal "x : HFinite ==> ( *f* exp) x : HFinite"; |
|
429 |
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); |
|
430 |
by (auto_tac (claset(),simpset() addsimps [starfun, |
|
431 |
HFinite_FreeUltrafilterNat_iff])); |
|
432 |
by (rtac bexI 1 THEN rtac lemma_hyprel_refl 2); |
|
433 |
by Auto_tac; |
|
434 |
by (res_inst_tac [("x","exp u")] exI 1); |
|
435 |
by (Ultra_tac 1 THEN arith_tac 1); |
|
436 |
qed "starfun_exp_HFinite"; |
|
437 |
||
438 |
Goal "[|x: Infinitesimal; z: HFinite |] ==> ( *f* exp) (z + x) @= ( *f* exp) z"; |
|
439 |
by (simp_tac (simpset() addsimps [STAR_exp_add]) 1); |
|
440 |
by (ftac STAR_exp_Infinitesimal 1); |
|
441 |
by (dtac approx_mult2 1); |
|
442 |
by (auto_tac (claset() addIs [starfun_exp_HFinite],simpset())); |
|
443 |
qed "starfun_exp_add_HFinite_Infinitesimal_approx"; |
|
444 |
||
445 |
(* using previous result to get to result *) |
|
446 |
Goal "[| x : HInfinite; 0 < x |] ==> ( *f* ln) x : HInfinite"; |
|
447 |
by (rtac ccontr 1 THEN dtac (HFinite_HInfinite_iff RS iffD2) 1); |
|
448 |
by (dtac starfun_exp_HFinite 1); |
|
449 |
by (auto_tac (claset(),simpset() addsimps [starfun_exp_ln_iff RS iffD2, |
|
450 |
HFinite_HInfinite_iff])); |
|
451 |
qed "starfun_ln_HInfinite"; |
|
452 |
||
453 |
Goal "x : HInfinite ==> ( *f* exp) x : HInfinite | ( *f* exp) x : Infinitesimal"; |
|
454 |
by (cut_inst_tac [("x","x")] (CLAIM "x <= (0::hypreal) | 0 <= x") 1); |
|
455 |
by (auto_tac (claset() addIs [starfun_exp_HInfinite,starfun_exp_Infinitesimal], |
|
456 |
simpset())); |
|
457 |
qed "starfun_exp_HInfinite_Infinitesimal_disj"; |
|
458 |
||
459 |
(* check out this proof!!! *) |
|
460 |
Goal "[| x : HFinite - Infinitesimal; 0 < x |] ==> ( *f* ln) x : HFinite"; |
|
461 |
by (rtac ccontr 1 THEN dtac (HInfinite_HFinite_iff RS iffD2) 1); |
|
462 |
by (dtac starfun_exp_HInfinite_Infinitesimal_disj 1); |
|
463 |
by (auto_tac (claset(),simpset() addsimps [starfun_exp_ln_iff RS sym, |
|
464 |
HInfinite_HFinite_iff] delsimps [starfun_exp_ln_iff])); |
|
465 |
qed "starfun_ln_HFinite_not_Infinitesimal"; |
|
466 |
||
467 |
(* we do proof by considering ln of 1/x *) |
|
468 |
Goal "[| x : Infinitesimal; 0 < x |] ==> ( *f* ln) x : HInfinite"; |
|
469 |
by (dtac Infinitesimal_inverse_HInfinite 1); |
|
14334 | 470 |
by (ftac positive_imp_inverse_positive 1); |
13958 | 471 |
by (dtac starfun_ln_HInfinite 2); |
472 |
by (auto_tac (claset(),simpset() addsimps [starfun_ln_inverse, |
|
473 |
HInfinite_minus_iff])); |
|
474 |
qed "starfun_ln_Infinitesimal_HInfinite"; |
|
475 |
||
476 |
Goal "[| 0 < x; x < 1 |] ==> ( *f* ln) x < 0"; |
|
477 |
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); |
|
478 |
by (auto_tac (claset(),simpset() addsimps [hypreal_zero_num, |
|
479 |
hypreal_one_num,hypreal_less,starfun])); |
|
480 |
by (ultra_tac (claset() addIs [ln_less_zero],simpset()) 1); |
|
481 |
qed "starfun_ln_less_zero"; |
|
482 |
||
483 |
Goal "[| x : Infinitesimal; 0 < x |] ==> ( *f* ln) x < 0"; |
|
484 |
by (auto_tac (claset() addSIs [starfun_ln_less_zero],simpset() |
|
485 |
addsimps [Infinitesimal_def])); |
|
486 |
by (dres_inst_tac [("x","1")] bspec 1); |
|
487 |
by (auto_tac (claset(),simpset() addsimps [hrabs_def])); |
|
488 |
qed "starfun_ln_Infinitesimal_less_zero"; |
|
489 |
||
490 |
Goal "[| x : HInfinite; 0 < x |] ==> 0 < ( *f* ln) x"; |
|
491 |
by (auto_tac (claset() addSIs [starfun_ln_gt_zero],simpset() |
|
492 |
addsimps [HInfinite_def])); |
|
493 |
by (dres_inst_tac [("x","1")] bspec 1); |
|
494 |
by (auto_tac (claset(),simpset() addsimps [hrabs_def])); |
|
495 |
qed "starfun_ln_HInfinite_gt_zero"; |
|
496 |
||
497 |
(* |
|
498 |
Goalw [NSLIM_def] "(%h. ((x powr h) - 1) / h) -- 0 --NS> ln x"; |
|
499 |
*) |
|
500 |
||
501 |
Goal "sumhr (0, whn, %n. (if even(n) then 0 else \ |
|
502 |
\ ((- 1) ^ ((n - 1) div 2))/(real (fact n))) * x ^ n) \ |
|
503 |
\ : HFinite"; |
|
504 |
by (auto_tac (claset() addSIs [NSBseq_HFinite_hypreal,NSconvergent_NSBseq], |
|
505 |
simpset() addsimps [starfunNat_sumr RS sym,starfunNat,hypnat_omega_def, |
|
506 |
convergent_NSconvergent_iff RS sym, summable_convergent_sumr_iff RS sym])); |
|
507 |
by (rtac (CLAIM "1 = Suc 0" RS ssubst) 1); |
|
508 |
by (rtac summable_sin 1); |
|
509 |
qed "HFinite_sin"; |
|
510 |
Addsimps [HFinite_sin]; |
|
511 |
||
512 |
Goal "( *f* sin) 0 = 0"; |
|
513 |
by (auto_tac (claset(),simpset() addsimps [starfun,hypreal_zero_num])); |
|
514 |
qed "STAR_sin_zero"; |
|
515 |
Addsimps [STAR_sin_zero]; |
|
516 |
||
517 |
Goal "x : Infinitesimal ==> ( *f* sin) x @= x"; |
|
518 |
by (case_tac "x = 0" 1); |
|
519 |
by (cut_inst_tac [("x","0")] DERIV_sin 2); |
|
520 |
by (auto_tac (claset(),simpset() addsimps [NSDERIV_DERIV_iff RS sym, |
|
521 |
nsderiv_def,hypreal_of_real_zero])); |
|
522 |
by (dres_inst_tac [("x","x")] bspec 1); |
|
523 |
by Auto_tac; |
|
524 |
by (dres_inst_tac [("c","x")] approx_mult1 1); |
|
525 |
by (auto_tac (claset() addIs [Infinitesimal_subset_HFinite RS subsetD], |
|
526 |
simpset() addsimps [hypreal_mult_assoc])); |
|
527 |
qed "STAR_sin_Infinitesimal"; |
|
528 |
Addsimps [STAR_sin_Infinitesimal]; |
|
529 |
||
530 |
Goal "sumhr (0, whn, %n. (if even(n) then \ |
|
531 |
\ ((- 1) ^ (n div 2))/(real (fact n)) else \ |
|
532 |
\ 0) * x ^ n) : HFinite"; |
|
533 |
by (auto_tac (claset() addSIs [NSBseq_HFinite_hypreal,NSconvergent_NSBseq], |
|
534 |
simpset() addsimps [starfunNat_sumr RS sym,starfunNat,hypnat_omega_def, |
|
535 |
convergent_NSconvergent_iff RS sym, summable_convergent_sumr_iff RS sym, |
|
536 |
summable_cos])); |
|
537 |
qed "HFinite_cos"; |
|
538 |
Addsimps [HFinite_cos]; |
|
539 |
||
540 |
Goal "( *f* cos) 0 = 1"; |
|
541 |
by (auto_tac (claset(),simpset() addsimps [starfun,hypreal_zero_num, |
|
542 |
hypreal_one_num])); |
|
543 |
qed "STAR_cos_zero"; |
|
544 |
Addsimps [STAR_cos_zero]; |
|
545 |
||
546 |
Goal "x : Infinitesimal ==> ( *f* cos) x @= 1"; |
|
547 |
by (case_tac "x = 0" 1); |
|
548 |
by (cut_inst_tac [("x","0")] DERIV_cos 2); |
|
549 |
by (auto_tac (claset(),simpset() addsimps [NSDERIV_DERIV_iff RS sym, |
|
550 |
nsderiv_def,hypreal_of_real_zero])); |
|
551 |
by (dres_inst_tac [("x","x")] bspec 1); |
|
552 |
by (auto_tac (claset(),simpset() addsimps [hypreal_of_real_zero, |
|
553 |
hypreal_of_real_one])); |
|
554 |
by (dres_inst_tac [("c","x")] approx_mult1 1); |
|
555 |
by (auto_tac (claset() addIs [Infinitesimal_subset_HFinite RS subsetD], |
|
556 |
simpset() addsimps [hypreal_mult_assoc,hypreal_of_real_one])); |
|
557 |
by (res_inst_tac [("d","-1")] approx_add_right_cancel 1); |
|
558 |
by Auto_tac; |
|
559 |
qed "STAR_cos_Infinitesimal"; |
|
560 |
Addsimps [STAR_cos_Infinitesimal]; |
|
561 |
||
562 |
Goal "( *f* tan) 0 = 0"; |
|
563 |
by (auto_tac (claset(),simpset() addsimps [starfun,hypreal_zero_num])); |
|
564 |
qed "STAR_tan_zero"; |
|
565 |
Addsimps [STAR_tan_zero]; |
|
566 |
||
567 |
Goal "x : Infinitesimal ==> ( *f* tan) x @= x"; |
|
568 |
by (case_tac "x = 0" 1); |
|
569 |
by (cut_inst_tac [("x","0")] DERIV_tan 2); |
|
570 |
by (auto_tac (claset(),simpset() addsimps [NSDERIV_DERIV_iff RS sym, |
|
571 |
nsderiv_def,hypreal_of_real_zero])); |
|
572 |
by (dres_inst_tac [("x","x")] bspec 1); |
|
573 |
by Auto_tac; |
|
574 |
by (dres_inst_tac [("c","x")] approx_mult1 1); |
|
575 |
by (auto_tac (claset() addIs [Infinitesimal_subset_HFinite RS subsetD], |
|
576 |
simpset() addsimps [hypreal_mult_assoc])); |
|
577 |
qed "STAR_tan_Infinitesimal"; |
|
578 |
||
579 |
Goal "x : Infinitesimal ==> ( *f* sin) x * ( *f* cos) x @= x"; |
|
580 |
by (rtac (simplify (simpset()) (read_instantiate |
|
581 |
[("d","1")] approx_mult_HFinite)) 1); |
|
582 |
by (auto_tac (claset(),simpset() addsimps [Infinitesimal_subset_HFinite |
|
583 |
RS subsetD])); |
|
584 |
qed "STAR_sin_cos_Infinitesimal_mult"; |
|
585 |
||
586 |
Goal "hypreal_of_real pi : HFinite"; |
|
587 |
by (Simp_tac 1); |
|
588 |
qed "HFinite_pi"; |
|
589 |
||
590 |
(* lemmas *) |
|
591 |
||
592 |
Goal "N : HNatInfinite \ |
|
593 |
\ ==> hypreal_of_real a = \ |
|
594 |
\ hypreal_of_hypnat N * (inverse(hypreal_of_hypnat N) * hypreal_of_real a)"; |
|
595 |
by (auto_tac (claset(),simpset() addsimps [hypreal_mult_assoc RS sym, |
|
596 |
HNatInfinite_not_eq_zero])); |
|
597 |
val lemma_split_hypreal_of_real = result(); |
|
598 |
||
599 |
Goal "[|x : Infinitesimal; x ~= 0 |] ==> ( *f* sin) x/x @= 1"; |
|
600 |
by (cut_inst_tac [("x","0")] DERIV_sin 1); |
|
601 |
by (auto_tac (claset(),simpset() addsimps [NSDERIV_DERIV_iff RS sym, |
|
602 |
nsderiv_def,hypreal_of_real_zero,hypreal_of_real_one])); |
|
603 |
qed "STAR_sin_Infinitesimal_divide"; |
|
604 |
||
605 |
(*------------------------------------------------------------------------*) |
|
606 |
(* sin* (1/n) * 1/(1/n) @= 1 for n = oo *) |
|
607 |
(*------------------------------------------------------------------------*) |
|
608 |
||
609 |
Goal "n : HNatInfinite \ |
|
610 |
\ ==> ( *f* sin) (inverse (hypreal_of_hypnat n))/(inverse (hypreal_of_hypnat n)) @= 1"; |
|
611 |
by (rtac STAR_sin_Infinitesimal_divide 1); |
|
14371
c78c7da09519
Conversion of HyperNat to Isar format and its declaration as a semiring
paulson
parents:
14370
diff
changeset
|
612 |
by (auto_tac (claset(),simpset() addsimps [HNatInfinite_not_eq_zero])); |
13958 | 613 |
val lemma_sin_pi = result(); |
614 |
||
615 |
Goal "n : HNatInfinite \ |
|
616 |
\ ==> ( *f* sin) (inverse (hypreal_of_hypnat n)) * hypreal_of_hypnat n @= 1"; |
|
617 |
by (forward_tac [lemma_sin_pi] 1); |
|
618 |
by (auto_tac (claset(),simpset() addsimps [hypreal_divide_def])); |
|
619 |
qed "STAR_sin_inverse_HNatInfinite"; |
|
620 |
||
621 |
Goalw [hypreal_divide_def] |
|
622 |
"N : HNatInfinite \ |
|
623 |
\ ==> hypreal_of_real pi/(hypreal_of_hypnat N) : Infinitesimal"; |
|
624 |
by (auto_tac (claset() addIs [Infinitesimal_HFinite_mult2],simpset())); |
|
625 |
qed "Infinitesimal_pi_divide_HNatInfinite"; |
|
626 |
||
627 |
Goal "N : HNatInfinite \ |
|
628 |
\ ==> hypreal_of_real pi/(hypreal_of_hypnat N) ~= 0"; |
|
14371
c78c7da09519
Conversion of HyperNat to Isar format and its declaration as a semiring
paulson
parents:
14370
diff
changeset
|
629 |
by (auto_tac (claset(),simpset() addsimps [HNatInfinite_not_eq_zero])); |
13958 | 630 |
qed "pi_divide_HNatInfinite_not_zero"; |
631 |
Addsimps [pi_divide_HNatInfinite_not_zero]; |
|
632 |
||
633 |
Goal "n : HNatInfinite \ |
|
634 |
\ ==> ( *f* sin) (hypreal_of_real pi/(hypreal_of_hypnat n)) * hypreal_of_hypnat n \ |
|
635 |
\ @= hypreal_of_real pi"; |
|
636 |
by (ftac ([Infinitesimal_pi_divide_HNatInfinite,pi_divide_HNatInfinite_not_zero] |
|
637 |
MRS STAR_sin_Infinitesimal_divide) 1); |
|
638 |
by (auto_tac (claset(),simpset() addsimps [hypreal_inverse_distrib])); |
|
639 |
by (res_inst_tac [("a","inverse(hypreal_of_real pi)")] approx_SReal_mult_cancel 1); |
|
14331 | 640 |
by (auto_tac (claset() addIs [SReal_inverse],simpset() addsimps [hypreal_divide_def] @ mult_ac)); |
13958 | 641 |
qed "STAR_sin_pi_divide_HNatInfinite_approx_pi"; |
642 |
||
643 |
Goal "n : HNatInfinite \ |
|
644 |
\ ==> hypreal_of_hypnat n * \ |
|
645 |
\ ( *f* sin) (hypreal_of_real pi/(hypreal_of_hypnat n)) \ |
|
646 |
\ @= hypreal_of_real pi"; |
|
647 |
by (rtac (hypreal_mult_commute RS subst) 1); |
|
648 |
by (etac STAR_sin_pi_divide_HNatInfinite_approx_pi 1); |
|
649 |
qed "STAR_sin_pi_divide_HNatInfinite_approx_pi2"; |
|
650 |
||
651 |
(*** more theorems ***) |
|
652 |
||
653 |
Goalw [real_divide_def] |
|
654 |
"N : HNatInfinite \ |
|
655 |
\ ==> ( *fNat* (%x. pi / real x)) N : Infinitesimal"; |
|
656 |
by (auto_tac (claset() addSIs [Infinitesimal_HFinite_mult2], |
|
657 |
simpset() addsimps [starfunNat_mult RS sym,starfunNat_inverse RS sym, |
|
658 |
starfunNat_real_of_nat])); |
|
659 |
qed "starfunNat_pi_divide_n_Infinitesimal"; |
|
660 |
||
661 |
Goal "N : HNatInfinite ==> \ |
|
662 |
\ ( *f* sin) (( *fNat* (%x. pi / real x)) N) @= \ |
|
663 |
\ hypreal_of_real pi/(hypreal_of_hypnat N)"; |
|
664 |
by (auto_tac (claset() addSIs [STAR_sin_Infinitesimal, |
|
665 |
Infinitesimal_HFinite_mult2],simpset() addsimps [starfunNat_mult RS sym, |
|
666 |
hypreal_divide_def,real_divide_def,starfunNat_inverse_real_of_nat_eq])); |
|
667 |
qed "STAR_sin_pi_divide_n_approx"; |
|
668 |
||
669 |
(*** move to NSA ***) |
|
670 |
Goalw [hypnat_zero_def] "(n <= (0::hypnat)) = (n = 0)"; |
|
671 |
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1); |
|
672 |
by (auto_tac (claset(),simpset() addsimps [hypnat_le])); |
|
673 |
qed "hypnat_le_zero_cancel"; |
|
674 |
AddIffs [hypnat_le_zero_cancel]; |
|
675 |
||
676 |
Goal "N : HNatInfinite ==> 0 < hypreal_of_hypnat N"; |
|
677 |
by (rtac ccontr 1); |
|
14371
c78c7da09519
Conversion of HyperNat to Isar format and its declaration as a semiring
paulson
parents:
14370
diff
changeset
|
678 |
by (auto_tac (claset(), |
c78c7da09519
Conversion of HyperNat to Isar format and its declaration as a semiring
paulson
parents:
14370
diff
changeset
|
679 |
simpset() addsimps [hypreal_of_hypnat_zero RS sym, linorder_not_less])); |
13958 | 680 |
qed "HNatInfinite_hypreal_of_hypnat_gt_zero"; |
681 |
||
682 |
bind_thm ("HNatInfinite_hypreal_of_hypnat_not_eq_zero", |
|
683 |
HNatInfinite_hypreal_of_hypnat_gt_zero RS hypreal_not_refl2 RS not_sym); |
|
684 |
(*** END: move to NSA ***) |
|
685 |
||
686 |
Goalw [NSLIMSEQ_def] "(%n. real n * sin (pi / real n)) ----NS> pi"; |
|
687 |
by (auto_tac (claset(),simpset() addsimps [starfunNat_mult RS sym, |
|
688 |
starfunNat_real_of_nat])); |
|
689 |
by (res_inst_tac [("f1","sin")] (starfun_stafunNat_o2 RS subst) 1); |
|
690 |
by (auto_tac (claset(),simpset() addsimps [starfunNat_mult RS sym, |
|
691 |
starfunNat_real_of_nat,real_divide_def])); |
|
692 |
by (res_inst_tac [("f1","inverse")] (starfun_stafunNat_o2 RS subst) 1); |
|
693 |
by (auto_tac (claset() addDs [STAR_sin_pi_divide_HNatInfinite_approx_pi], |
|
694 |
simpset() addsimps [starfunNat_real_of_nat,hypreal_mult_commute, |
|
695 |
symmetric hypreal_divide_def])); |
|
696 |
qed "NSLIMSEQ_sin_pi"; |
|
697 |
||
698 |
Goalw [NSLIMSEQ_def] "(%n. cos (pi / real n))----NS> 1"; |
|
699 |
by Auto_tac; |
|
700 |
by (res_inst_tac [("f1","cos")] (starfun_stafunNat_o2 RS subst) 1); |
|
701 |
by (rtac STAR_cos_Infinitesimal 1); |
|
702 |
by (auto_tac (claset() addSIs [Infinitesimal_HFinite_mult2], |
|
703 |
simpset() addsimps [starfunNat_mult RS sym,real_divide_def, |
|
704 |
starfunNat_inverse RS sym,starfunNat_real_of_nat])); |
|
705 |
qed "NSLIMSEQ_cos_one"; |
|
706 |
||
707 |
Goal "(%n. real n * sin (pi / real n) * cos (pi / real n)) ----NS> pi"; |
|
708 |
by (rtac (simplify (simpset()) |
|
709 |
([NSLIMSEQ_sin_pi,NSLIMSEQ_cos_one] MRS NSLIMSEQ_mult)) 1); |
|
710 |
qed "NSLIMSEQ_sin_cos_pi"; |
|
711 |
||
712 |
(*------------------------------------------------------------------------*) |
|
713 |
(* A familiar approximation to cos x when x is small *) |
|
714 |
(*------------------------------------------------------------------------*) |
|
715 |
||
716 |
Goal "x : Infinitesimal ==> ( *f* cos) x @= 1 - x ^ 2"; |
|
717 |
by (rtac (STAR_cos_Infinitesimal RS approx_trans) 1); |
|
718 |
by (auto_tac (claset(),simpset() addsimps [Infinitesimal_approx_minus RS sym, |
|
14322 | 719 |
hypreal_diff_def,hypreal_add_assoc RS sym,numeral_2_eq_2])); |
13958 | 720 |
qed "STAR_cos_Infinitesimal_approx"; |
721 |
||
722 |
(* move to NSA *) |
|
723 |
Goalw [hypreal_divide_def] |
|
724 |
"[| x : Infinitesimal; y : Reals; y ~= 0 |] ==> x/y : Infinitesimal"; |
|
725 |
by (auto_tac (claset() addSIs [Infinitesimal_HFinite_mult] |
|
726 |
addSDs [SReal_inverse RS (SReal_subset_HFinite RS subsetD)],simpset())); |
|
727 |
qed "Infinitesimal_SReal_divide"; |
|
728 |
||
729 |
Goal "x : Infinitesimal ==> ( *f* cos) x @= 1 - (x ^ 2)/2"; |
|
730 |
by (rtac (STAR_cos_Infinitesimal RS approx_trans) 1); |
|
731 |
by (auto_tac (claset() addIs [Infinitesimal_SReal_divide], |
|
732 |
simpset() addsimps [Infinitesimal_approx_minus RS sym, |
|
14322 | 733 |
numeral_2_eq_2])); |
13958 | 734 |
qed "STAR_cos_Infinitesimal_approx2"; |
735 |
||
736 |
||
737 |
||
738 |
||
739 |