10751
|
1 |
(* Title : HyperPow.ML
|
|
2 |
Author : Jacques D. Fleuriot
|
|
3 |
Copyright : 1998 University of Cambridge
|
|
4 |
Description : Natural Powers of hyperreals theory
|
|
5 |
|
|
6 |
*)
|
|
7 |
|
|
8 |
Goal "(#0::hypreal) ^ (Suc n) = 0";
|
|
9 |
by (Auto_tac);
|
|
10 |
qed "hrealpow_zero";
|
|
11 |
Addsimps [hrealpow_zero];
|
|
12 |
|
|
13 |
Goal "r ~= (#0::hypreal) --> r ^ n ~= 0";
|
|
14 |
by (induct_tac "n" 1);
|
|
15 |
by Auto_tac;
|
|
16 |
qed_spec_mp "hrealpow_not_zero";
|
|
17 |
|
|
18 |
Goal "r ~= (#0::hypreal) --> inverse(r ^ n) = (inverse r) ^ n";
|
|
19 |
by (induct_tac "n" 1);
|
|
20 |
by (Auto_tac);
|
|
21 |
by (forw_inst_tac [("n","n")] hrealpow_not_zero 1);
|
|
22 |
by (auto_tac (claset(), simpset() addsimps [hypreal_inverse_distrib]));
|
|
23 |
qed_spec_mp "hrealpow_inverse";
|
|
24 |
|
|
25 |
Goal "abs (r::hypreal) ^ n = abs (r ^ n)";
|
|
26 |
by (induct_tac "n" 1);
|
|
27 |
by (auto_tac (claset(), simpset() addsimps [hrabs_mult]));
|
|
28 |
qed "hrealpow_hrabs";
|
|
29 |
|
|
30 |
Goal "(r::hypreal) ^ (n + m) = (r ^ n) * (r ^ m)";
|
|
31 |
by (induct_tac "n" 1);
|
|
32 |
by (auto_tac (claset(), simpset() addsimps hypreal_mult_ac));
|
|
33 |
qed "hrealpow_add";
|
|
34 |
|
|
35 |
Goal "(r::hypreal) ^ 1 = r";
|
|
36 |
by (Simp_tac 1);
|
|
37 |
qed "hrealpow_one";
|
|
38 |
Addsimps [hrealpow_one];
|
|
39 |
|
|
40 |
Goal "(r::hypreal) ^ 2 = r * r";
|
|
41 |
by (Simp_tac 1);
|
|
42 |
qed "hrealpow_two";
|
|
43 |
|
|
44 |
Goal "(#0::hypreal) <= r --> #0 <= r ^ n";
|
|
45 |
by (induct_tac "n" 1);
|
|
46 |
by (auto_tac (claset(), simpset() addsimps [hypreal_0_le_mult_iff]));
|
|
47 |
qed_spec_mp "hrealpow_ge_zero";
|
|
48 |
|
|
49 |
Goal "(#0::hypreal) < r --> #0 < r ^ n";
|
|
50 |
by (induct_tac "n" 1);
|
|
51 |
by (auto_tac (claset(), simpset() addsimps [hypreal_0_less_mult_iff]));
|
|
52 |
qed_spec_mp "hrealpow_gt_zero";
|
|
53 |
|
|
54 |
Goal "x <= y & (#0::hypreal) < x --> x ^ n <= y ^ n";
|
|
55 |
by (induct_tac "n" 1);
|
|
56 |
by (auto_tac (claset() addSIs [hypreal_mult_le_mono], simpset()));
|
|
57 |
by (asm_simp_tac (simpset() addsimps [hrealpow_ge_zero]) 1);
|
|
58 |
qed_spec_mp "hrealpow_le";
|
|
59 |
|
|
60 |
Goal "x < y & (#0::hypreal) < x & 0 < n --> x ^ n < y ^ n";
|
|
61 |
by (induct_tac "n" 1);
|
|
62 |
by (auto_tac (claset() addIs [hypreal_mult_less_mono,gr0I],
|
|
63 |
simpset() addsimps [hrealpow_gt_zero]));
|
|
64 |
qed "hrealpow_less";
|
|
65 |
|
|
66 |
Goal "#1 ^ n = (#1::hypreal)";
|
|
67 |
by (induct_tac "n" 1);
|
|
68 |
by (Auto_tac);
|
|
69 |
qed "hrealpow_eq_one";
|
|
70 |
Addsimps [hrealpow_eq_one];
|
|
71 |
|
|
72 |
Goal "abs(-(#1 ^ n)) = (#1::hypreal)";
|
|
73 |
by Auto_tac;
|
|
74 |
qed "hrabs_minus_hrealpow_one";
|
|
75 |
Addsimps [hrabs_minus_hrealpow_one];
|
|
76 |
|
|
77 |
Goal "abs(#-1 ^ n) = (#1::hypreal)";
|
|
78 |
by (induct_tac "n" 1);
|
|
79 |
by Auto_tac;
|
|
80 |
qed "hrabs_hrealpow_minus_one";
|
|
81 |
Addsimps [hrabs_hrealpow_minus_one];
|
|
82 |
|
|
83 |
Goal "((r::hypreal) * s) ^ n = (r ^ n) * (s ^ n)";
|
|
84 |
by (induct_tac "n" 1);
|
|
85 |
by (auto_tac (claset(), simpset() addsimps hypreal_mult_ac));
|
|
86 |
qed "hrealpow_mult";
|
|
87 |
|
|
88 |
Goal "(#0::hypreal) <= r ^ 2";
|
|
89 |
by (auto_tac (claset(), simpset() addsimps [hypreal_0_le_mult_iff]));
|
|
90 |
qed "hrealpow_two_le";
|
|
91 |
Addsimps [hrealpow_two_le];
|
|
92 |
|
|
93 |
Goal "(#0::hypreal) <= u ^ 2 + v ^ 2";
|
|
94 |
by (simp_tac (HOL_ss addsimps [hrealpow_two_le,
|
|
95 |
rename_numerals hypreal_le_add_order]) 1);
|
|
96 |
qed "hrealpow_two_le_add_order";
|
|
97 |
Addsimps [hrealpow_two_le_add_order];
|
|
98 |
|
|
99 |
Goal "(#0::hypreal) <= u ^ 2 + v ^ 2 + w ^ 2";
|
|
100 |
by (simp_tac (HOL_ss addsimps [hrealpow_two_le,
|
|
101 |
rename_numerals hypreal_le_add_order]) 1);
|
|
102 |
qed "hrealpow_two_le_add_order2";
|
|
103 |
Addsimps [hrealpow_two_le_add_order2];
|
|
104 |
|
|
105 |
Goal "(x ^ 2 + y ^ 2 + z ^ 2 = (#0::hypreal)) = (x = #0 & y = #0 & z = #0)";
|
|
106 |
by (simp_tac (HOL_ss addsimps
|
|
107 |
[rename_numerals hypreal_three_squares_add_zero_iff, hrealpow_two]) 1);
|
|
108 |
qed "hrealpow_three_squares_add_zero_iff";
|
|
109 |
Addsimps [hrealpow_three_squares_add_zero_iff];
|
|
110 |
|
|
111 |
Goal "abs(x ^ 2) = (x::hypreal) ^ 2";
|
|
112 |
by (auto_tac (claset(),
|
|
113 |
simpset() addsimps [hrabs_def, hypreal_0_le_mult_iff]));
|
|
114 |
qed "hrabs_hrealpow_two";
|
|
115 |
Addsimps [hrabs_hrealpow_two];
|
|
116 |
|
|
117 |
Goal "abs(x) ^ 2 = (x::hypreal) ^ 2";
|
|
118 |
by (simp_tac (simpset() addsimps [hrealpow_hrabs, hrabs_eqI1]
|
|
119 |
delsimps [hpowr_Suc]) 1);
|
|
120 |
qed "hrealpow_two_hrabs";
|
|
121 |
Addsimps [hrealpow_two_hrabs];
|
|
122 |
|
|
123 |
Goal "(#1::hypreal) < r ==> #1 < r ^ 2";
|
|
124 |
by (auto_tac (claset(), simpset() addsimps [hrealpow_two]));
|
|
125 |
by (res_inst_tac [("y","#1*#1")] order_le_less_trans 1);
|
|
126 |
by (rtac hypreal_mult_less_mono 2);
|
|
127 |
by Auto_tac;
|
|
128 |
qed "hrealpow_two_gt_one";
|
|
129 |
|
|
130 |
Goal "(#1::hypreal) <= r ==> #1 <= r ^ 2";
|
|
131 |
by (etac (order_le_imp_less_or_eq RS disjE) 1);
|
|
132 |
by (etac (hrealpow_two_gt_one RS order_less_imp_le) 1);
|
|
133 |
by Auto_tac;
|
|
134 |
qed "hrealpow_two_ge_one";
|
|
135 |
|
|
136 |
Goal "(#1::hypreal) <= #2 ^ n";
|
|
137 |
by (res_inst_tac [("y","#1 ^ n")] order_trans 1);
|
|
138 |
by (rtac hrealpow_le 2);
|
|
139 |
by (auto_tac (claset() addIs [order_less_imp_le],
|
|
140 |
simpset() addsimps [hypreal_zero_less_one, hypreal_one_less_two]));
|
|
141 |
qed "two_hrealpow_ge_one";
|
|
142 |
|
|
143 |
Goal "hypreal_of_nat n < #2 ^ n";
|
|
144 |
by (induct_tac "n" 1);
|
|
145 |
by (auto_tac (claset(),
|
|
146 |
simpset() addsimps [hypreal_of_nat_Suc,hypreal_of_nat_zero,
|
|
147 |
hypreal_zero_less_one,hypreal_add_mult_distrib,hypreal_of_nat_one]));
|
|
148 |
by (cut_inst_tac [("n","n")] two_hrealpow_ge_one 1);
|
|
149 |
by (arith_tac 1);
|
|
150 |
qed "two_hrealpow_gt";
|
|
151 |
Addsimps [two_hrealpow_gt,two_hrealpow_ge_one];
|
|
152 |
|
|
153 |
Goal "#-1 ^ (2*n) = (#1::hypreal)";
|
|
154 |
by (induct_tac "n" 1);
|
|
155 |
by (Auto_tac);
|
|
156 |
qed "hrealpow_minus_one";
|
|
157 |
|
|
158 |
Goal "#-1 ^ (n + n) = (#1::hypreal)";
|
|
159 |
by (induct_tac "n" 1);
|
|
160 |
by (Auto_tac);
|
|
161 |
qed "hrealpow_minus_one2";
|
|
162 |
Addsimps [hrealpow_minus_one2];
|
|
163 |
|
|
164 |
Goal "(-(x::hypreal)) ^ 2 = x ^ 2";
|
|
165 |
by (Auto_tac);
|
|
166 |
qed "hrealpow_minus_two";
|
|
167 |
Addsimps [hrealpow_minus_two];
|
|
168 |
|
|
169 |
Goal "(#0::hypreal) < r & r < #1 --> r ^ Suc n < r ^ n";
|
|
170 |
by (induct_tac "n" 1);
|
|
171 |
by (auto_tac (claset(),
|
|
172 |
simpset() addsimps [hypreal_mult_less_mono2]));
|
|
173 |
qed_spec_mp "hrealpow_Suc_less";
|
|
174 |
|
|
175 |
Goal "(#0::hypreal) <= r & r < #1 --> r ^ Suc n <= r ^ n";
|
|
176 |
by (induct_tac "n" 1);
|
|
177 |
by (auto_tac (claset() addIs [order_less_imp_le]
|
|
178 |
addSDs [order_le_imp_less_or_eq,hrealpow_Suc_less],
|
|
179 |
simpset() addsimps [hypreal_mult_less_mono2]));
|
|
180 |
qed_spec_mp "hrealpow_Suc_le";
|
|
181 |
|
|
182 |
Goal "Abs_hypreal(hyprel^^{%n. X n}) ^ m = Abs_hypreal(hyprel^^{%n. (X n) ^ m})";
|
|
183 |
by (induct_tac "m" 1);
|
|
184 |
by (auto_tac (claset(),
|
|
185 |
simpset() delsimps [one_eq_numeral_1]
|
|
186 |
addsimps [hypreal_one_def, hypreal_mult,
|
|
187 |
one_eq_numeral_1 RS sym]));
|
|
188 |
qed "hrealpow";
|
|
189 |
|
|
190 |
Goal "(x + (y::hypreal)) ^ 2 = \
|
|
191 |
\ x ^ 2 + y ^ 2 + (hypreal_of_nat 2)*x*y";
|
|
192 |
by (simp_tac (simpset() addsimps [hypreal_add_mult_distrib2,
|
|
193 |
hypreal_add_mult_distrib,hypreal_of_nat_two]
|
|
194 |
@ hypreal_add_ac @ hypreal_mult_ac) 1);
|
|
195 |
qed "hrealpow_sum_square_expand";
|
|
196 |
|
|
197 |
(*---------------------------------------------------------------
|
|
198 |
we'll prove the following theorem by going down to the
|
|
199 |
level of the ultrafilter and relying on the analogous
|
|
200 |
property for the real rather than prove it directly
|
|
201 |
using induction: proof is much simpler this way!
|
|
202 |
---------------------------------------------------------------*)
|
|
203 |
Goal "[|(#0::hypreal) <= x; #0 <= y;x ^ Suc n <= y ^ Suc n |] ==> x <= y";
|
|
204 |
by (full_simp_tac
|
|
205 |
(HOL_ss addsimps [zero_eq_numeral_0 RS sym, hypreal_zero_def]) 1);
|
|
206 |
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
|
|
207 |
by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
|
|
208 |
by (auto_tac (claset(),
|
|
209 |
simpset() addsimps [hrealpow,hypreal_le,hypreal_mult]));
|
|
210 |
by (ultra_tac (claset() addIs [realpow_increasing], simpset()) 1);
|
|
211 |
qed "hrealpow_increasing";
|
|
212 |
|
|
213 |
(*By antisymmetry with the above we conclude x=y, replacing the deleted
|
|
214 |
theorem hrealpow_Suc_cancel_eq*)
|
|
215 |
|
|
216 |
Goal "x : HFinite --> x ^ n : HFinite";
|
|
217 |
by (induct_tac "n" 1);
|
|
218 |
by (auto_tac (claset() addIs [HFinite_mult], simpset()));
|
|
219 |
qed_spec_mp "hrealpow_HFinite";
|
|
220 |
|
|
221 |
(*---------------------------------------------------------------
|
|
222 |
Hypernaturals Powers
|
|
223 |
--------------------------------------------------------------*)
|
|
224 |
Goalw [congruent_def]
|
|
225 |
"congruent hyprel \
|
|
226 |
\ (%X Y. hyprel^^{%n. ((X::nat=>real) n ^ (Y::nat=>nat) n)})";
|
|
227 |
by (safe_tac (claset() addSIs [ext]));
|
|
228 |
by (ALLGOALS(Fuf_tac));
|
|
229 |
qed "hyperpow_congruent";
|
|
230 |
|
|
231 |
Goalw [hyperpow_def]
|
|
232 |
"Abs_hypreal(hyprel^^{%n. X n}) pow Abs_hypnat(hypnatrel^^{%n. Y n}) = \
|
|
233 |
\ Abs_hypreal(hyprel^^{%n. X n ^ Y n})";
|
|
234 |
by (res_inst_tac [("f","Abs_hypreal")] arg_cong 1);
|
|
235 |
by (auto_tac (claset() addSIs [lemma_hyprel_refl,bexI],
|
|
236 |
simpset() addsimps [hyprel_in_hypreal RS
|
|
237 |
Abs_hypreal_inverse,equiv_hyprel,hyperpow_congruent]));
|
|
238 |
by (Fuf_tac 1);
|
|
239 |
qed "hyperpow";
|
|
240 |
|
|
241 |
Goalw [hypnat_one_def] "(#0::hypreal) pow (n + 1hn) = #0";
|
|
242 |
by (simp_tac (HOL_ss addsimps [zero_eq_numeral_0 RS sym, hypreal_zero_def]) 1);
|
|
243 |
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
|
|
244 |
by (auto_tac (claset(), simpset() addsimps [hyperpow,hypnat_add]));
|
|
245 |
qed "hyperpow_zero";
|
|
246 |
Addsimps [hyperpow_zero];
|
|
247 |
|
|
248 |
Goal "r ~= (#0::hypreal) --> r pow n ~= #0";
|
|
249 |
by (simp_tac (HOL_ss addsimps [zero_eq_numeral_0 RS sym, hypreal_zero_def]) 1);
|
|
250 |
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
|
|
251 |
by (res_inst_tac [("z","r")] eq_Abs_hypreal 1);
|
|
252 |
by (auto_tac (claset(), simpset() addsimps [hyperpow]));
|
|
253 |
by (dtac FreeUltrafilterNat_Compl_mem 1);
|
|
254 |
by (fuf_empty_tac (claset() addIs [realpow_not_zero RS notE],
|
|
255 |
simpset()) 1);
|
|
256 |
qed_spec_mp "hyperpow_not_zero";
|
|
257 |
|
|
258 |
Goal "r ~= (#0::hypreal) --> inverse(r pow n) = (inverse r) pow n";
|
|
259 |
by (simp_tac (HOL_ss addsimps [zero_eq_numeral_0 RS sym, hypreal_zero_def]) 1);
|
|
260 |
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
|
|
261 |
by (res_inst_tac [("z","r")] eq_Abs_hypreal 1);
|
|
262 |
by (auto_tac (claset() addSDs [FreeUltrafilterNat_Compl_mem],
|
|
263 |
simpset() addsimps [hypreal_inverse,hyperpow]));
|
|
264 |
by (rtac FreeUltrafilterNat_subset 1);
|
|
265 |
by (auto_tac (claset() addDs [realpow_not_zero]
|
|
266 |
addIs [realpow_inverse],
|
|
267 |
simpset()));
|
|
268 |
qed "hyperpow_inverse";
|
|
269 |
|
|
270 |
Goal "abs r pow n = abs (r pow n)";
|
|
271 |
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
|
|
272 |
by (res_inst_tac [("z","r")] eq_Abs_hypreal 1);
|
|
273 |
by (auto_tac (claset(),
|
|
274 |
simpset() addsimps [hypreal_hrabs, hyperpow,realpow_abs]));
|
|
275 |
qed "hyperpow_hrabs";
|
|
276 |
|
|
277 |
Goal "r pow (n + m) = (r pow n) * (r pow m)";
|
|
278 |
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
|
|
279 |
by (res_inst_tac [("z","m")] eq_Abs_hypnat 1);
|
|
280 |
by (res_inst_tac [("z","r")] eq_Abs_hypreal 1);
|
|
281 |
by (auto_tac (claset(),
|
|
282 |
simpset() addsimps [hyperpow,hypnat_add, hypreal_mult,realpow_add]));
|
|
283 |
qed "hyperpow_add";
|
|
284 |
|
|
285 |
Goalw [hypnat_one_def] "r pow 1hn = r";
|
|
286 |
by (res_inst_tac [("z","r")] eq_Abs_hypreal 1);
|
|
287 |
by (auto_tac (claset(), simpset() addsimps [hyperpow]));
|
|
288 |
qed "hyperpow_one";
|
|
289 |
Addsimps [hyperpow_one];
|
|
290 |
|
|
291 |
Goalw [hypnat_one_def]
|
|
292 |
"r pow (1hn + 1hn) = r * r";
|
|
293 |
by (res_inst_tac [("z","r")] eq_Abs_hypreal 1);
|
|
294 |
by (auto_tac (claset(),
|
|
295 |
simpset() addsimps [hyperpow,hypnat_add, hypreal_mult,realpow_two]));
|
|
296 |
qed "hyperpow_two";
|
|
297 |
|
|
298 |
Goal "(#0::hypreal) < r --> #0 < r pow n";
|
|
299 |
by (simp_tac (HOL_ss addsimps [zero_eq_numeral_0 RS sym, hypreal_zero_def]) 1);
|
|
300 |
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
|
|
301 |
by (res_inst_tac [("z","r")] eq_Abs_hypreal 1);
|
|
302 |
by (auto_tac (claset() addSEs [FreeUltrafilterNat_subset, realpow_gt_zero],
|
|
303 |
simpset() addsimps [hyperpow,hypreal_less, hypreal_le]));
|
|
304 |
qed_spec_mp "hyperpow_gt_zero";
|
|
305 |
|
|
306 |
Goal "(#0::hypreal) < r --> #0 <= r pow n";
|
|
307 |
by (blast_tac (claset() addSIs [hyperpow_gt_zero, order_less_imp_le]) 1);
|
|
308 |
qed_spec_mp "hyperpow_ge_zero";
|
|
309 |
|
|
310 |
Goal "(#0::hypreal) <= r --> #0 <= r pow n";
|
|
311 |
by (simp_tac (HOL_ss addsimps [zero_eq_numeral_0 RS sym, hypreal_zero_def]) 1);
|
|
312 |
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
|
|
313 |
by (res_inst_tac [("z","r")] eq_Abs_hypreal 1);
|
|
314 |
by (auto_tac (claset() addSEs [FreeUltrafilterNat_subset, realpow_ge_zero2],
|
|
315 |
simpset() addsimps [hyperpow,hypreal_le]));
|
|
316 |
qed "hyperpow_ge_zero2";
|
|
317 |
|
|
318 |
Goal "(#0::hypreal) < x & x <= y --> x pow n <= y pow n";
|
|
319 |
by (full_simp_tac
|
|
320 |
(HOL_ss addsimps [zero_eq_numeral_0 RS sym, hypreal_zero_def]) 1);
|
|
321 |
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
|
|
322 |
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
|
|
323 |
by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
|
|
324 |
by (auto_tac (claset() addIs [realpow_le,
|
|
325 |
(FreeUltrafilterNat_Int RS FreeUltrafilterNat_subset)],
|
|
326 |
simpset() addsimps [hyperpow,hypreal_le,hypreal_less]));
|
|
327 |
qed_spec_mp "hyperpow_le";
|
|
328 |
|
|
329 |
Goal "#1 pow n = (#1::hypreal)";
|
|
330 |
by (simp_tac (HOL_ss addsimps [one_eq_numeral_1 RS sym, hypreal_one_def]) 1);
|
|
331 |
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
|
|
332 |
by (auto_tac (claset(), simpset() addsimps [hyperpow]));
|
|
333 |
qed "hyperpow_eq_one";
|
|
334 |
Addsimps [hyperpow_eq_one];
|
|
335 |
|
|
336 |
Goal "abs(-(#1 pow n)) = (#1::hypreal)";
|
|
337 |
by (simp_tac (HOL_ss addsimps [one_eq_numeral_1 RS sym, hypreal_one_def]) 1);
|
|
338 |
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
|
|
339 |
by (auto_tac (claset(), simpset() addsimps [hyperpow,hypreal_hrabs]));
|
|
340 |
qed "hrabs_minus_hyperpow_one";
|
|
341 |
Addsimps [hrabs_minus_hyperpow_one];
|
|
342 |
|
|
343 |
Goal "abs(#-1 pow n) = (#1::hypreal)";
|
|
344 |
by (subgoal_tac "abs((-1hr) pow n) = 1hr" 1);
|
|
345 |
by (Asm_full_simp_tac 1);
|
|
346 |
by (simp_tac (HOL_ss addsimps [hypreal_one_def]) 1);
|
|
347 |
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
|
|
348 |
by (auto_tac (claset(),
|
|
349 |
simpset() addsimps [hyperpow,hypreal_minus,hypreal_hrabs]));
|
|
350 |
qed "hrabs_hyperpow_minus_one";
|
|
351 |
Addsimps [hrabs_hyperpow_minus_one];
|
|
352 |
|
|
353 |
Goal "(r * s) pow n = (r pow n) * (s pow n)";
|
|
354 |
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
|
|
355 |
by (res_inst_tac [("z","r")] eq_Abs_hypreal 1);
|
|
356 |
by (res_inst_tac [("z","s")] eq_Abs_hypreal 1);
|
|
357 |
by (auto_tac (claset(),
|
|
358 |
simpset() addsimps [hyperpow, hypreal_mult,realpow_mult]));
|
|
359 |
qed "hyperpow_mult";
|
|
360 |
|
|
361 |
Goal "(#0::hypreal) <= r pow (1hn + 1hn)";
|
|
362 |
by (auto_tac (claset(),
|
|
363 |
simpset() addsimps [hyperpow_two, hypreal_0_le_mult_iff]));
|
|
364 |
qed "hyperpow_two_le";
|
|
365 |
Addsimps [hyperpow_two_le];
|
|
366 |
|
|
367 |
Goal "abs(x pow (1hn + 1hn)) = x pow (1hn + 1hn)";
|
|
368 |
by (simp_tac (simpset() addsimps [hrabs_eqI1]) 1);
|
|
369 |
qed "hrabs_hyperpow_two";
|
|
370 |
Addsimps [hrabs_hyperpow_two];
|
|
371 |
|
|
372 |
Goal "abs(x) pow (1hn + 1hn) = x pow (1hn + 1hn)";
|
|
373 |
by (simp_tac (simpset() addsimps [hyperpow_hrabs,hrabs_eqI1]) 1);
|
|
374 |
qed "hyperpow_two_hrabs";
|
|
375 |
Addsimps [hyperpow_two_hrabs];
|
|
376 |
|
|
377 |
(*? very similar to hrealpow_two_gt_one *)
|
|
378 |
Goal "(#1::hypreal) < r ==> #1 < r pow (1hn + 1hn)";
|
|
379 |
by (auto_tac (claset(), simpset() addsimps [hyperpow_two]));
|
|
380 |
by (res_inst_tac [("y","#1*#1")] order_le_less_trans 1);
|
|
381 |
by (rtac hypreal_mult_less_mono 2);
|
|
382 |
by Auto_tac;
|
|
383 |
qed "hyperpow_two_gt_one";
|
|
384 |
|
|
385 |
Goal "(#1::hypreal) <= r ==> #1 <= r pow (1hn + 1hn)";
|
|
386 |
by (auto_tac (claset() addSDs [order_le_imp_less_or_eq]
|
|
387 |
addIs [hyperpow_two_gt_one,order_less_imp_le],
|
|
388 |
simpset()));
|
|
389 |
qed "hyperpow_two_ge_one";
|
|
390 |
|
|
391 |
Goal "(#1::hypreal) <= #2 pow n";
|
|
392 |
by (res_inst_tac [("y","#1 pow n")] order_trans 1);
|
|
393 |
by (rtac hyperpow_le 2);
|
|
394 |
by (auto_tac (claset() addIs [order_less_imp_le],
|
|
395 |
simpset() addsimps [hypreal_zero_less_one, hypreal_one_less_two]));
|
|
396 |
qed "two_hyperpow_ge_one";
|
|
397 |
Addsimps [two_hyperpow_ge_one];
|
|
398 |
|
|
399 |
Addsimps [simplify (simpset()) realpow_minus_one];
|
|
400 |
|
|
401 |
Goal "#-1 pow ((1hn + 1hn)*n) = (#1::hypreal)";
|
|
402 |
by (subgoal_tac "(-(1hr)) pow ((1hn + 1hn)*n) = 1hr" 1);
|
|
403 |
by (Asm_full_simp_tac 1);
|
|
404 |
by (simp_tac (HOL_ss addsimps [hypreal_one_def]) 1);
|
|
405 |
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
|
|
406 |
by (auto_tac (claset(),
|
|
407 |
simpset() addsimps [hyperpow, hypnat_add,hypreal_minus]));
|
|
408 |
qed "hyperpow_minus_one2";
|
|
409 |
Addsimps [hyperpow_minus_one2];
|
|
410 |
|
|
411 |
Goalw [hypnat_one_def]
|
|
412 |
"(#0::hypreal) < r & r < #1 --> r pow (n + 1hn) < r pow n";
|
|
413 |
by (full_simp_tac
|
|
414 |
(HOL_ss addsimps [zero_eq_numeral_0 RS sym, hypreal_zero_def,
|
|
415 |
one_eq_numeral_1 RS sym, hypreal_one_def]) 1);
|
|
416 |
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
|
|
417 |
by (res_inst_tac [("z","r")] eq_Abs_hypreal 1);
|
|
418 |
by (auto_tac (claset() addSDs [conjI RS realpow_Suc_less]
|
|
419 |
addEs [FreeUltrafilterNat_Int RS FreeUltrafilterNat_subset],
|
|
420 |
simpset() addsimps [hyperpow,hypreal_less,hypnat_add]));
|
|
421 |
qed_spec_mp "hyperpow_Suc_less";
|
|
422 |
|
|
423 |
Goalw [hypnat_one_def]
|
|
424 |
"#0 <= r & r < (#1::hypreal) --> r pow (n + 1hn) <= r pow n";
|
|
425 |
by (full_simp_tac
|
|
426 |
(HOL_ss addsimps [zero_eq_numeral_0 RS sym, hypreal_zero_def,
|
|
427 |
one_eq_numeral_1 RS sym, hypreal_one_def]) 1);
|
|
428 |
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
|
|
429 |
by (res_inst_tac [("z","r")] eq_Abs_hypreal 1);
|
|
430 |
by (auto_tac (claset() addSDs [conjI RS realpow_Suc_le] addEs
|
|
431 |
[FreeUltrafilterNat_Int RS FreeUltrafilterNat_subset ],
|
|
432 |
simpset() addsimps [hyperpow,hypreal_le,hypnat_add,
|
|
433 |
hypreal_less]));
|
|
434 |
qed_spec_mp "hyperpow_Suc_le";
|
|
435 |
|
|
436 |
Goalw [hypnat_one_def]
|
|
437 |
"(#0::hypreal) <= r & r < #1 & n < N --> r pow N <= r pow n";
|
|
438 |
by (full_simp_tac
|
|
439 |
(HOL_ss addsimps [zero_eq_numeral_0 RS sym, hypreal_zero_def,
|
|
440 |
one_eq_numeral_1 RS sym, hypreal_one_def]) 1);
|
|
441 |
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
|
|
442 |
by (res_inst_tac [("z","N")] eq_Abs_hypnat 1);
|
|
443 |
by (res_inst_tac [("z","r")] eq_Abs_hypreal 1);
|
|
444 |
by (auto_tac (claset(),
|
|
445 |
simpset() addsimps [hyperpow, hypreal_le,hypreal_less,hypnat_less]));
|
|
446 |
by (etac (FreeUltrafilterNat_Int RS FreeUltrafilterNat_subset) 1);
|
|
447 |
by (etac FreeUltrafilterNat_Int 1);
|
|
448 |
by (auto_tac (claset() addSDs [conjI RS realpow_less_le],
|
|
449 |
simpset()));
|
|
450 |
qed_spec_mp "hyperpow_less_le";
|
|
451 |
|
|
452 |
Goal "[| (#0::hypreal) <= r; r < #1 |] \
|
|
453 |
\ ==> ALL N n. n < N --> r pow N <= r pow n";
|
|
454 |
by (blast_tac (claset() addSIs [hyperpow_less_le]) 1);
|
|
455 |
qed "hyperpow_less_le2";
|
|
456 |
|
|
457 |
Goal "[| #0 <= r; r < (#1::hypreal); N : HNatInfinite |] \
|
|
458 |
\ ==> ALL n:SHNat. r pow N <= r pow n";
|
|
459 |
by (auto_tac (claset() addSIs [hyperpow_less_le],
|
|
460 |
simpset() addsimps [HNatInfinite_iff]));
|
|
461 |
qed "hyperpow_SHNat_le";
|
|
462 |
|
|
463 |
Goalw [hypreal_of_real_def,hypnat_of_nat_def]
|
|
464 |
"(hypreal_of_real r) pow (hypnat_of_nat n) = hypreal_of_real (r ^ n)";
|
|
465 |
by (auto_tac (claset(), simpset() addsimps [hyperpow]));
|
|
466 |
qed "hyperpow_realpow";
|
|
467 |
|
|
468 |
Goalw [SReal_def]
|
|
469 |
"(hypreal_of_real r) pow (hypnat_of_nat n) : SReal";
|
|
470 |
by (auto_tac (claset(), simpset() addsimps [hyperpow_realpow]));
|
|
471 |
qed "hyperpow_SReal";
|
|
472 |
Addsimps [hyperpow_SReal];
|
|
473 |
|
|
474 |
Goal "N : HNatInfinite ==> (#0::hypreal) pow N = 0";
|
|
475 |
by (dtac HNatInfinite_is_Suc 1);
|
|
476 |
by (Auto_tac);
|
|
477 |
qed "hyperpow_zero_HNatInfinite";
|
|
478 |
Addsimps [hyperpow_zero_HNatInfinite];
|
|
479 |
|
|
480 |
Goal "[| (#0::hypreal) <= r; r < #1; n <= N |] ==> r pow N <= r pow n";
|
|
481 |
by (dres_inst_tac [("y","N")] hypnat_le_imp_less_or_eq 1);
|
|
482 |
by (auto_tac (claset() addIs [hyperpow_less_le], simpset()));
|
|
483 |
qed "hyperpow_le_le";
|
|
484 |
|
|
485 |
Goal "[| (#0::hypreal) < r; r < #1 |] ==> r pow (n + 1hn) <= r";
|
|
486 |
by (dres_inst_tac [("n","1hn")] (order_less_imp_le RS hyperpow_le_le) 1);
|
|
487 |
by (Auto_tac);
|
|
488 |
qed "hyperpow_Suc_le_self";
|
|
489 |
|
|
490 |
Goal "[| (#0::hypreal) <= r; r < #1 |] ==> r pow (n + 1hn) <= r";
|
|
491 |
by (dres_inst_tac [("n","1hn")] hyperpow_le_le 1);
|
|
492 |
by (Auto_tac);
|
|
493 |
qed "hyperpow_Suc_le_self2";
|
|
494 |
|
|
495 |
Goalw [Infinitesimal_def]
|
|
496 |
"[| x : Infinitesimal; 0 < N |] ==> (abs x) pow N <= abs x";
|
|
497 |
by (auto_tac (claset() addSIs [hyperpow_Suc_le_self2],
|
|
498 |
simpset() addsimps [hyperpow_hrabs RS sym,
|
|
499 |
hypnat_gt_zero_iff2, hrabs_ge_zero,
|
|
500 |
hypreal_zero_less_one]));
|
|
501 |
qed "lemma_Infinitesimal_hyperpow";
|
|
502 |
|
|
503 |
Goal "[| x : Infinitesimal; 0 < N |] ==> x pow N : Infinitesimal";
|
|
504 |
by (rtac hrabs_le_Infinitesimal 1);
|
|
505 |
by (dtac Infinitesimal_hrabs 1);
|
|
506 |
by (auto_tac (claset() addSIs [lemma_Infinitesimal_hyperpow],
|
|
507 |
simpset() addsimps [hyperpow_hrabs RS sym]));
|
|
508 |
qed "Infinitesimal_hyperpow";
|
|
509 |
|
|
510 |
Goalw [hypnat_of_nat_def]
|
|
511 |
"(x ^ n : Infinitesimal) = (x pow (hypnat_of_nat n) : Infinitesimal)";
|
|
512 |
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
|
|
513 |
by (auto_tac (claset(), simpset() addsimps [hrealpow, hyperpow]));
|
|
514 |
qed "hrealpow_hyperpow_Infinitesimal_iff";
|
|
515 |
|
|
516 |
Goal "[| x : Infinitesimal; 0 < n |] ==> x ^ n : Infinitesimal";
|
|
517 |
by (auto_tac (claset() addSIs [Infinitesimal_hyperpow],
|
|
518 |
simpset() addsimps [hrealpow_hyperpow_Infinitesimal_iff,
|
|
519 |
hypnat_of_nat_less_iff,hypnat_of_nat_zero]
|
|
520 |
delsimps [hypnat_of_nat_less_iff RS sym]));
|
|
521 |
qed "Infinitesimal_hrealpow";
|