|
1 (* Title : HOL/Real/Hyperreal/Hyper.ML |
|
2 ID : $Id$ |
|
3 Author : Jacques D. Fleuriot |
|
4 Copyright : 1998 University of Cambridge |
|
5 Description : Ultrapower construction of hyperreals |
|
6 *) |
|
7 |
|
8 (*------------------------------------------------------------------------ |
|
9 Proof that the set of naturals is not finite |
|
10 ------------------------------------------------------------------------*) |
|
11 |
|
12 (*** based on James' proof that the set of naturals is not finite ***) |
|
13 Goal "finite (A::nat set) --> (? n. !m. Suc (n + m) ~: A)"; |
|
14 by (rtac impI 1); |
|
15 by (eres_inst_tac [("F","A")] finite_induct 1); |
|
16 by (Blast_tac 1 THEN etac exE 1); |
|
17 by (res_inst_tac [("x","n + x")] exI 1); |
|
18 by (rtac allI 1 THEN eres_inst_tac [("x","x + m")] allE 1); |
|
19 by (auto_tac (claset(), simpset() addsimps add_ac)); |
|
20 by (auto_tac (claset(), |
|
21 simpset() addsimps [add_assoc RS sym, |
|
22 less_add_Suc2 RS less_not_refl2])); |
|
23 qed_spec_mp "finite_exhausts"; |
|
24 |
|
25 Goal "finite (A :: nat set) --> (? n. n ~:A)"; |
|
26 by (rtac impI 1 THEN dtac finite_exhausts 1); |
|
27 by (Blast_tac 1); |
|
28 qed_spec_mp "finite_not_covers"; |
|
29 |
|
30 Goal "~ finite(UNIV:: nat set)"; |
|
31 by (fast_tac (claset() addSDs [finite_exhausts]) 1); |
|
32 qed "not_finite_nat"; |
|
33 |
|
34 (*------------------------------------------------------------------------ |
|
35 Existence of free ultrafilter over the naturals and proof of various |
|
36 properties of the FreeUltrafilterNat- an arbitrary free ultrafilter |
|
37 ------------------------------------------------------------------------*) |
|
38 |
|
39 Goal "EX U. U: FreeUltrafilter (UNIV::nat set)"; |
|
40 by (rtac (not_finite_nat RS FreeUltrafilter_Ex) 1); |
|
41 qed "FreeUltrafilterNat_Ex"; |
|
42 |
|
43 Goalw [FreeUltrafilterNat_def] |
|
44 "FreeUltrafilterNat: FreeUltrafilter(UNIV:: nat set)"; |
|
45 by (rtac (FreeUltrafilterNat_Ex RS exE) 1); |
|
46 by (rtac selectI2 1 THEN ALLGOALS(assume_tac)); |
|
47 qed "FreeUltrafilterNat_mem"; |
|
48 Addsimps [FreeUltrafilterNat_mem]; |
|
49 |
|
50 Goalw [FreeUltrafilterNat_def] "finite x ==> x ~: FreeUltrafilterNat"; |
|
51 by (rtac (FreeUltrafilterNat_Ex RS exE) 1); |
|
52 by (rtac selectI2 1 THEN assume_tac 1); |
|
53 by (blast_tac (claset() addDs [mem_FreeUltrafiltersetD1]) 1); |
|
54 qed "FreeUltrafilterNat_finite"; |
|
55 |
|
56 Goal "x: FreeUltrafilterNat ==> ~ finite x"; |
|
57 by (blast_tac (claset() addDs [FreeUltrafilterNat_finite]) 1); |
|
58 qed "FreeUltrafilterNat_not_finite"; |
|
59 |
|
60 Goalw [FreeUltrafilterNat_def] "{} ~: FreeUltrafilterNat"; |
|
61 by (rtac (FreeUltrafilterNat_Ex RS exE) 1); |
|
62 by (rtac selectI2 1 THEN assume_tac 1); |
|
63 by (blast_tac (claset() addDs [FreeUltrafilter_Ultrafilter, |
|
64 Ultrafilter_Filter,Filter_empty_not_mem]) 1); |
|
65 qed "FreeUltrafilterNat_empty"; |
|
66 Addsimps [FreeUltrafilterNat_empty]; |
|
67 |
|
68 Goal "[| X: FreeUltrafilterNat; Y: FreeUltrafilterNat |] \ |
|
69 \ ==> X Int Y : FreeUltrafilterNat"; |
|
70 by (cut_facts_tac [FreeUltrafilterNat_mem] 1); |
|
71 by (blast_tac (claset() addDs [FreeUltrafilter_Ultrafilter, |
|
72 Ultrafilter_Filter,mem_FiltersetD1]) 1); |
|
73 qed "FreeUltrafilterNat_Int"; |
|
74 |
|
75 Goal "[| X: FreeUltrafilterNat; X <= Y |] \ |
|
76 \ ==> Y : FreeUltrafilterNat"; |
|
77 by (cut_facts_tac [FreeUltrafilterNat_mem] 1); |
|
78 by (blast_tac (claset() addDs [FreeUltrafilter_Ultrafilter, |
|
79 Ultrafilter_Filter,mem_FiltersetD2]) 1); |
|
80 qed "FreeUltrafilterNat_subset"; |
|
81 |
|
82 Goal "X: FreeUltrafilterNat ==> -X ~: FreeUltrafilterNat"; |
|
83 by (Step_tac 1); |
|
84 by (dtac FreeUltrafilterNat_Int 1 THEN assume_tac 1); |
|
85 by Auto_tac; |
|
86 qed "FreeUltrafilterNat_Compl"; |
|
87 |
|
88 Goal "X~: FreeUltrafilterNat ==> -X : FreeUltrafilterNat"; |
|
89 by (cut_facts_tac [FreeUltrafilterNat_mem RS (FreeUltrafilter_iff RS iffD1)] 1); |
|
90 by (Step_tac 1 THEN dres_inst_tac [("x","X")] bspec 1); |
|
91 by (auto_tac (claset(),simpset() addsimps [UNIV_diff_Compl])); |
|
92 qed "FreeUltrafilterNat_Compl_mem"; |
|
93 |
|
94 Goal "(X ~: FreeUltrafilterNat) = (-X: FreeUltrafilterNat)"; |
|
95 by (blast_tac (claset() addDs [FreeUltrafilterNat_Compl, |
|
96 FreeUltrafilterNat_Compl_mem]) 1); |
|
97 qed "FreeUltrafilterNat_Compl_iff1"; |
|
98 |
|
99 Goal "(X: FreeUltrafilterNat) = (-X ~: FreeUltrafilterNat)"; |
|
100 by (auto_tac (claset(), |
|
101 simpset() addsimps [FreeUltrafilterNat_Compl_iff1 RS sym])); |
|
102 qed "FreeUltrafilterNat_Compl_iff2"; |
|
103 |
|
104 Goal "(UNIV::nat set) : FreeUltrafilterNat"; |
|
105 by (rtac (FreeUltrafilterNat_mem RS FreeUltrafilter_Ultrafilter RS |
|
106 Ultrafilter_Filter RS mem_FiltersetD4) 1); |
|
107 qed "FreeUltrafilterNat_UNIV"; |
|
108 Addsimps [FreeUltrafilterNat_UNIV]; |
|
109 |
|
110 Goal "{n::nat. True}: FreeUltrafilterNat"; |
|
111 by (subgoal_tac "{n::nat. True} = (UNIV::nat set)" 1); |
|
112 by Auto_tac; |
|
113 qed "FreeUltrafilterNat_Nat_set"; |
|
114 Addsimps [FreeUltrafilterNat_Nat_set]; |
|
115 |
|
116 Goal "{n. P(n) = P(n)} : FreeUltrafilterNat"; |
|
117 by (Simp_tac 1); |
|
118 qed "FreeUltrafilterNat_Nat_set_refl"; |
|
119 AddIs [FreeUltrafilterNat_Nat_set_refl]; |
|
120 |
|
121 Goal "{n::nat. P} : FreeUltrafilterNat ==> P"; |
|
122 by (rtac ccontr 1); |
|
123 by (rotate_tac 1 1); |
|
124 by (Asm_full_simp_tac 1); |
|
125 qed "FreeUltrafilterNat_P"; |
|
126 |
|
127 Goal "{n. P(n)} : FreeUltrafilterNat ==> EX n. P(n)"; |
|
128 by (rtac ccontr 1 THEN rotate_tac 1 1); |
|
129 by (Asm_full_simp_tac 1); |
|
130 qed "FreeUltrafilterNat_Ex_P"; |
|
131 |
|
132 Goal "ALL n. P(n) ==> {n. P(n)} : FreeUltrafilterNat"; |
|
133 by (auto_tac (claset() addIs [FreeUltrafilterNat_Nat_set],simpset())); |
|
134 qed "FreeUltrafilterNat_all"; |
|
135 |
|
136 (*----------------------------------------- |
|
137 Define and use Ultrafilter tactics |
|
138 -----------------------------------------*) |
|
139 use "fuf.ML"; |
|
140 |
|
141 |
|
142 |
|
143 (*------------------------------------------------------ |
|
144 Now prove one further property of our free ultrafilter |
|
145 -------------------------------------------------------*) |
|
146 Goal "X Un Y: FreeUltrafilterNat \ |
|
147 \ ==> X: FreeUltrafilterNat | Y: FreeUltrafilterNat"; |
|
148 by Auto_tac; |
|
149 by (Ultra_tac 1); |
|
150 qed "FreeUltrafilterNat_Un"; |
|
151 |
|
152 (*------------------------------------------------------------------------ |
|
153 Properties of hyprel |
|
154 ------------------------------------------------------------------------*) |
|
155 |
|
156 (** Proving that hyprel is an equivalence relation **) |
|
157 (** Natural deduction for hyprel **) |
|
158 |
|
159 Goalw [hyprel_def] |
|
160 "((X,Y): hyprel) = ({n. X n = Y n}: FreeUltrafilterNat)"; |
|
161 by (Fast_tac 1); |
|
162 qed "hyprel_iff"; |
|
163 |
|
164 Goalw [hyprel_def] |
|
165 "{n. X n = Y n}: FreeUltrafilterNat ==> (X,Y): hyprel"; |
|
166 by (Fast_tac 1); |
|
167 qed "hyprelI"; |
|
168 |
|
169 Goalw [hyprel_def] |
|
170 "p: hyprel --> (EX X Y. \ |
|
171 \ p = (X,Y) & {n. X n = Y n} : FreeUltrafilterNat)"; |
|
172 by (Fast_tac 1); |
|
173 qed "hyprelE_lemma"; |
|
174 |
|
175 val [major,minor] = goal thy |
|
176 "[| p: hyprel; \ |
|
177 \ !!X Y. [| p = (X,Y); {n. X n = Y n}: FreeUltrafilterNat\ |
|
178 \ |] ==> Q |] ==> Q"; |
|
179 by (cut_facts_tac [major RS (hyprelE_lemma RS mp)] 1); |
|
180 by (REPEAT (eresolve_tac [asm_rl,exE,conjE,minor] 1)); |
|
181 qed "hyprelE"; |
|
182 |
|
183 AddSIs [hyprelI]; |
|
184 AddSEs [hyprelE]; |
|
185 |
|
186 Goalw [hyprel_def] "(x,x): hyprel"; |
|
187 by (auto_tac (claset(),simpset() addsimps |
|
188 [FreeUltrafilterNat_Nat_set])); |
|
189 qed "hyprel_refl"; |
|
190 |
|
191 Goal "{n. X n = Y n} = {n. Y n = X n}"; |
|
192 by Auto_tac; |
|
193 qed "lemma_perm"; |
|
194 |
|
195 Goalw [hyprel_def] "(x,y): hyprel --> (y,x):hyprel"; |
|
196 by (auto_tac (claset() addIs [lemma_perm RS subst],simpset())); |
|
197 qed_spec_mp "hyprel_sym"; |
|
198 |
|
199 Goalw [hyprel_def] |
|
200 "(x,y): hyprel --> (y,z):hyprel --> (x,z):hyprel"; |
|
201 by Auto_tac; |
|
202 by (Ultra_tac 1); |
|
203 qed_spec_mp "hyprel_trans"; |
|
204 |
|
205 Goalw [equiv_def, refl_def, sym_def, trans_def] |
|
206 "equiv {x::nat=>real. True} hyprel"; |
|
207 by (auto_tac (claset() addSIs [hyprel_refl] |
|
208 addSEs [hyprel_sym,hyprel_trans] |
|
209 delrules [hyprelI,hyprelE], |
|
210 simpset() addsimps [FreeUltrafilterNat_Nat_set])); |
|
211 qed "equiv_hyprel"; |
|
212 |
|
213 val equiv_hyprel_iff = |
|
214 [TrueI, TrueI] MRS |
|
215 ([CollectI, CollectI] MRS |
|
216 (equiv_hyprel RS eq_equiv_class_iff)); |
|
217 |
|
218 Goalw [hypreal_def,hyprel_def,quotient_def] "hyprel^^{x}:hypreal"; |
|
219 by (Blast_tac 1); |
|
220 qed "hyprel_in_hypreal"; |
|
221 |
|
222 Goal "inj_on Abs_hypreal hypreal"; |
|
223 by (rtac inj_on_inverseI 1); |
|
224 by (etac Abs_hypreal_inverse 1); |
|
225 qed "inj_on_Abs_hypreal"; |
|
226 |
|
227 Addsimps [equiv_hyprel_iff,inj_on_Abs_hypreal RS inj_on_iff, |
|
228 hyprel_iff, hyprel_in_hypreal, Abs_hypreal_inverse]; |
|
229 |
|
230 Addsimps [equiv_hyprel RS eq_equiv_class_iff]; |
|
231 val eq_hyprelD = equiv_hyprel RSN (2,eq_equiv_class); |
|
232 |
|
233 Goal "inj(Rep_hypreal)"; |
|
234 by (rtac inj_inverseI 1); |
|
235 by (rtac Rep_hypreal_inverse 1); |
|
236 qed "inj_Rep_hypreal"; |
|
237 |
|
238 Goalw [hyprel_def] "x: hyprel ^^ {x}"; |
|
239 by (Step_tac 1); |
|
240 by (auto_tac (claset() addSIs [FreeUltrafilterNat_Nat_set],simpset())); |
|
241 qed "lemma_hyprel_refl"; |
|
242 |
|
243 Addsimps [lemma_hyprel_refl]; |
|
244 |
|
245 Goalw [hypreal_def] "{} ~: hypreal"; |
|
246 by (auto_tac (claset() addSEs [quotientE], simpset())); |
|
247 qed "hypreal_empty_not_mem"; |
|
248 |
|
249 Addsimps [hypreal_empty_not_mem]; |
|
250 |
|
251 Goal "Rep_hypreal x ~= {}"; |
|
252 by (cut_inst_tac [("x","x")] Rep_hypreal 1); |
|
253 by Auto_tac; |
|
254 qed "Rep_hypreal_nonempty"; |
|
255 |
|
256 Addsimps [Rep_hypreal_nonempty]; |
|
257 |
|
258 (*------------------------------------------------------------------------ |
|
259 hypreal_of_real: the injection from real to hypreal |
|
260 ------------------------------------------------------------------------*) |
|
261 |
|
262 Goal "inj(hypreal_of_real)"; |
|
263 by (rtac injI 1); |
|
264 by (rewtac hypreal_of_real_def); |
|
265 by (dtac (inj_on_Abs_hypreal RS inj_onD) 1); |
|
266 by (REPEAT (rtac hyprel_in_hypreal 1)); |
|
267 by (dtac eq_equiv_class 1); |
|
268 by (rtac equiv_hyprel 1); |
|
269 by (Fast_tac 1); |
|
270 by (rtac ccontr 1 THEN rotate_tac 1 1); |
|
271 by Auto_tac; |
|
272 qed "inj_hypreal_of_real"; |
|
273 |
|
274 val [prem] = goal thy |
|
275 "(!!x y. z = Abs_hypreal(hyprel^^{x}) ==> P) ==> P"; |
|
276 by (res_inst_tac [("x1","z")] |
|
277 (rewrite_rule [hypreal_def] Rep_hypreal RS quotientE) 1); |
|
278 by (dres_inst_tac [("f","Abs_hypreal")] arg_cong 1); |
|
279 by (res_inst_tac [("x","x")] prem 1); |
|
280 by (asm_full_simp_tac (simpset() addsimps [Rep_hypreal_inverse]) 1); |
|
281 qed "eq_Abs_hypreal"; |
|
282 |
|
283 (**** hypreal_minus: additive inverse on hypreal ****) |
|
284 |
|
285 Goalw [congruent_def] |
|
286 "congruent hyprel (%X. hyprel^^{%n. - (X n)})"; |
|
287 by Safe_tac; |
|
288 by (ALLGOALS Ultra_tac); |
|
289 qed "hypreal_minus_congruent"; |
|
290 |
|
291 (*Resolve th against the corresponding facts for hypreal_minus*) |
|
292 val hypreal_minus_ize = RSLIST [equiv_hyprel, hypreal_minus_congruent]; |
|
293 |
|
294 Goalw [hypreal_minus_def] |
|
295 "- (Abs_hypreal(hyprel^^{%n. X n})) = Abs_hypreal(hyprel ^^ {%n. -(X n)})"; |
|
296 by (res_inst_tac [("f","Abs_hypreal")] arg_cong 1); |
|
297 by (simp_tac (simpset() addsimps |
|
298 [hyprel_in_hypreal RS Abs_hypreal_inverse,hypreal_minus_ize UN_equiv_class]) 1); |
|
299 qed "hypreal_minus"; |
|
300 |
|
301 Goal "- (- z) = (z::hypreal)"; |
|
302 by (res_inst_tac [("z","z")] eq_Abs_hypreal 1); |
|
303 by (asm_simp_tac (simpset() addsimps [hypreal_minus]) 1); |
|
304 qed "hypreal_minus_minus"; |
|
305 |
|
306 Addsimps [hypreal_minus_minus]; |
|
307 |
|
308 Goal "inj(%r::hypreal. -r)"; |
|
309 by (rtac injI 1); |
|
310 by (dres_inst_tac [("f","uminus")] arg_cong 1); |
|
311 by (asm_full_simp_tac (simpset() addsimps [hypreal_minus_minus]) 1); |
|
312 qed "inj_hypreal_minus"; |
|
313 |
|
314 Goalw [hypreal_zero_def] "-0hr = 0hr"; |
|
315 by (simp_tac (simpset() addsimps [hypreal_minus]) 1); |
|
316 qed "hypreal_minus_zero"; |
|
317 |
|
318 Addsimps [hypreal_minus_zero]; |
|
319 |
|
320 Goal "(-x = 0hr) = (x = 0hr)"; |
|
321 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); |
|
322 by (auto_tac (claset(),simpset() addsimps [hypreal_zero_def, |
|
323 hypreal_minus] @ real_add_ac)); |
|
324 qed "hypreal_minus_zero_iff"; |
|
325 |
|
326 Addsimps [hypreal_minus_zero_iff]; |
|
327 (**** hrinv: multiplicative inverse on hypreal ****) |
|
328 |
|
329 Goalw [congruent_def] |
|
330 "congruent hyprel (%X. hyprel^^{%n. if X n = 0r then 0r else rinv(X n)})"; |
|
331 by (Auto_tac THEN Ultra_tac 1); |
|
332 qed "hypreal_hrinv_congruent"; |
|
333 |
|
334 (* Resolve th against the corresponding facts for hrinv *) |
|
335 val hypreal_hrinv_ize = RSLIST [equiv_hyprel, hypreal_hrinv_congruent]; |
|
336 |
|
337 Goalw [hrinv_def] |
|
338 "hrinv (Abs_hypreal(hyprel^^{%n. X n})) = \ |
|
339 \ Abs_hypreal(hyprel ^^ {%n. if X n = 0r then 0r else rinv(X n)})"; |
|
340 by (res_inst_tac [("f","Abs_hypreal")] arg_cong 1); |
|
341 by (simp_tac (simpset() addsimps |
|
342 [hyprel_in_hypreal RS Abs_hypreal_inverse,hypreal_hrinv_ize UN_equiv_class]) 1); |
|
343 qed "hypreal_hrinv"; |
|
344 |
|
345 Goal "z ~= 0hr ==> hrinv (hrinv z) = z"; |
|
346 by (res_inst_tac [("z","z")] eq_Abs_hypreal 1); |
|
347 by (rotate_tac 1 1); |
|
348 by (asm_full_simp_tac (simpset() addsimps |
|
349 [hypreal_hrinv,hypreal_zero_def] setloop (split_tac [expand_if])) 1); |
|
350 by (ultra_tac (claset() addDs [rinv_not_zero,real_rinv_rinv],simpset()) 1); |
|
351 qed "hypreal_hrinv_hrinv"; |
|
352 |
|
353 Addsimps [hypreal_hrinv_hrinv]; |
|
354 |
|
355 Goalw [hypreal_one_def] "hrinv(1hr) = 1hr"; |
|
356 by (full_simp_tac (simpset() addsimps [hypreal_hrinv, |
|
357 real_zero_not_eq_one RS not_sym] |
|
358 setloop (split_tac [expand_if])) 1); |
|
359 qed "hypreal_hrinv_1"; |
|
360 Addsimps [hypreal_hrinv_1]; |
|
361 |
|
362 (**** hyperreal addition: hypreal_add ****) |
|
363 |
|
364 Goalw [congruent2_def] |
|
365 "congruent2 hyprel (%X Y. hyprel^^{%n. X n + Y n})"; |
|
366 by Safe_tac; |
|
367 by (ALLGOALS(Ultra_tac)); |
|
368 qed "hypreal_add_congruent2"; |
|
369 |
|
370 (*Resolve th against the corresponding facts for hyppreal_add*) |
|
371 val hypreal_add_ize = RSLIST [equiv_hyprel, hypreal_add_congruent2]; |
|
372 |
|
373 Goalw [hypreal_add_def] |
|
374 "Abs_hypreal(hyprel^^{%n. X n}) + Abs_hypreal(hyprel^^{%n. Y n}) = \ |
|
375 \ Abs_hypreal(hyprel^^{%n. X n + Y n})"; |
|
376 by (asm_simp_tac |
|
377 (simpset() addsimps [hypreal_add_ize UN_equiv_class2]) 1); |
|
378 qed "hypreal_add"; |
|
379 |
|
380 Goal "(z::hypreal) + w = w + z"; |
|
381 by (res_inst_tac [("z","z")] eq_Abs_hypreal 1); |
|
382 by (res_inst_tac [("z","w")] eq_Abs_hypreal 1); |
|
383 by (asm_simp_tac (simpset() addsimps (real_add_ac @ [hypreal_add])) 1); |
|
384 qed "hypreal_add_commute"; |
|
385 |
|
386 Goal "((z1::hypreal) + z2) + z3 = z1 + (z2 + z3)"; |
|
387 by (res_inst_tac [("z","z1")] eq_Abs_hypreal 1); |
|
388 by (res_inst_tac [("z","z2")] eq_Abs_hypreal 1); |
|
389 by (res_inst_tac [("z","z3")] eq_Abs_hypreal 1); |
|
390 by (asm_simp_tac (simpset() addsimps [hypreal_add, real_add_assoc]) 1); |
|
391 qed "hypreal_add_assoc"; |
|
392 |
|
393 (*For AC rewriting*) |
|
394 Goal "(x::hypreal)+(y+z)=y+(x+z)"; |
|
395 by (rtac (hypreal_add_commute RS trans) 1); |
|
396 by (rtac (hypreal_add_assoc RS trans) 1); |
|
397 by (rtac (hypreal_add_commute RS arg_cong) 1); |
|
398 qed "hypreal_add_left_commute"; |
|
399 |
|
400 (* hypreal addition is an AC operator *) |
|
401 val hypreal_add_ac = [hypreal_add_assoc,hypreal_add_commute, |
|
402 hypreal_add_left_commute]; |
|
403 |
|
404 Goalw [hypreal_zero_def] "0hr + z = z"; |
|
405 by (res_inst_tac [("z","z")] eq_Abs_hypreal 1); |
|
406 by (asm_full_simp_tac (simpset() addsimps |
|
407 [hypreal_add]) 1); |
|
408 qed "hypreal_add_zero_left"; |
|
409 |
|
410 Goal "z + 0hr = z"; |
|
411 by (simp_tac (simpset() addsimps |
|
412 [hypreal_add_zero_left,hypreal_add_commute]) 1); |
|
413 qed "hypreal_add_zero_right"; |
|
414 |
|
415 Goalw [hypreal_zero_def] "z + -z = 0hr"; |
|
416 by (res_inst_tac [("z","z")] eq_Abs_hypreal 1); |
|
417 by (asm_full_simp_tac (simpset() addsimps [hypreal_minus, |
|
418 hypreal_add]) 1); |
|
419 qed "hypreal_add_minus"; |
|
420 |
|
421 Goal "-z + z = 0hr"; |
|
422 by (simp_tac (simpset() addsimps |
|
423 [hypreal_add_commute,hypreal_add_minus]) 1); |
|
424 qed "hypreal_add_minus_left"; |
|
425 |
|
426 Addsimps [hypreal_add_minus,hypreal_add_minus_left, |
|
427 hypreal_add_zero_left,hypreal_add_zero_right]; |
|
428 |
|
429 Goal "? y. (x::hypreal) + y = 0hr"; |
|
430 by (fast_tac (claset() addIs [hypreal_add_minus]) 1); |
|
431 qed "hypreal_minus_ex"; |
|
432 |
|
433 Goal "?! y. (x::hypreal) + y = 0hr"; |
|
434 by (auto_tac (claset() addIs [hypreal_add_minus],simpset())); |
|
435 by (dres_inst_tac [("f","%x. ya+x")] arg_cong 1); |
|
436 by (asm_full_simp_tac (simpset() addsimps [hypreal_add_assoc RS sym]) 1); |
|
437 by (asm_full_simp_tac (simpset() addsimps [hypreal_add_commute]) 1); |
|
438 qed "hypreal_minus_ex1"; |
|
439 |
|
440 Goal "?! y. y + (x::hypreal) = 0hr"; |
|
441 by (auto_tac (claset() addIs [hypreal_add_minus_left],simpset())); |
|
442 by (dres_inst_tac [("f","%x. x+ya")] arg_cong 1); |
|
443 by (asm_full_simp_tac (simpset() addsimps [hypreal_add_assoc]) 1); |
|
444 by (asm_full_simp_tac (simpset() addsimps [hypreal_add_commute]) 1); |
|
445 qed "hypreal_minus_left_ex1"; |
|
446 |
|
447 Goal "x + y = 0hr ==> x = -y"; |
|
448 by (cut_inst_tac [("z","y")] hypreal_add_minus_left 1); |
|
449 by (res_inst_tac [("x1","y")] (hypreal_minus_left_ex1 RS ex1E) 1); |
|
450 by (Blast_tac 1); |
|
451 qed "hypreal_add_minus_eq_minus"; |
|
452 |
|
453 Goal "? y::hypreal. x = -y"; |
|
454 by (cut_inst_tac [("x","x")] hypreal_minus_ex 1); |
|
455 by (etac exE 1 THEN dtac hypreal_add_minus_eq_minus 1); |
|
456 by (Fast_tac 1); |
|
457 qed "hypreal_as_add_inverse_ex"; |
|
458 |
|
459 Goal "-(x + (y::hypreal)) = -x + -y"; |
|
460 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); |
|
461 by (res_inst_tac [("z","y")] eq_Abs_hypreal 1); |
|
462 by (auto_tac (claset(),simpset() addsimps [hypreal_minus, |
|
463 hypreal_add,real_minus_add_distrib])); |
|
464 qed "hypreal_minus_add_distrib"; |
|
465 |
|
466 Goal "-(y + -(x::hypreal)) = x + -y"; |
|
467 by (simp_tac (simpset() addsimps [hypreal_minus_add_distrib, |
|
468 hypreal_add_commute]) 1); |
|
469 qed "hypreal_minus_distrib1"; |
|
470 |
|
471 Goal "(x + - (y::hypreal)) + (y + - z) = x + -z"; |
|
472 by (res_inst_tac [("w1","y")] (hypreal_add_commute RS subst) 1); |
|
473 by (simp_tac (simpset() addsimps [hypreal_add_left_commute, |
|
474 hypreal_add_assoc]) 1); |
|
475 by (simp_tac (simpset() addsimps [hypreal_add_commute]) 1); |
|
476 qed "hypreal_add_minus_cancel1"; |
|
477 |
|
478 Goal "((x::hypreal) + y = x + z) = (y = z)"; |
|
479 by (Step_tac 1); |
|
480 by (dres_inst_tac [("f","%t.-x + t")] arg_cong 1); |
|
481 by (asm_full_simp_tac (simpset() addsimps [hypreal_add_assoc RS sym]) 1); |
|
482 qed "hypreal_add_left_cancel"; |
|
483 |
|
484 Goal "z + (x + (y + -z)) = x + (y::hypreal)"; |
|
485 by (simp_tac (simpset() addsimps hypreal_add_ac) 1); |
|
486 qed "hypreal_add_minus_cancel2"; |
|
487 Addsimps [hypreal_add_minus_cancel2]; |
|
488 |
|
489 Goal "y + -(x + y) = -(x::hypreal)"; |
|
490 by (full_simp_tac (simpset() addsimps [hypreal_minus_add_distrib]) 1); |
|
491 by (rtac (hypreal_add_left_commute RS subst) 1); |
|
492 by (Full_simp_tac 1); |
|
493 qed "hypreal_add_minus_cancel"; |
|
494 Addsimps [hypreal_add_minus_cancel]; |
|
495 |
|
496 Goal "y + -(y + x) = -(x::hypreal)"; |
|
497 by (simp_tac (simpset() addsimps [hypreal_minus_add_distrib, |
|
498 hypreal_add_assoc RS sym]) 1); |
|
499 qed "hypreal_add_minus_cancelc"; |
|
500 Addsimps [hypreal_add_minus_cancelc]; |
|
501 |
|
502 Goal "(z + -x) + (y + -z) = (y + -(x::hypreal))"; |
|
503 by (full_simp_tac (simpset() addsimps [hypreal_minus_add_distrib |
|
504 RS sym, hypreal_add_left_cancel] @ hypreal_add_ac) 1); |
|
505 qed "hypreal_add_minus_cancel3"; |
|
506 Addsimps [hypreal_add_minus_cancel3]; |
|
507 |
|
508 Goal "(y + (x::hypreal)= z + x) = (y = z)"; |
|
509 by (simp_tac (simpset() addsimps [hypreal_add_commute, |
|
510 hypreal_add_left_cancel]) 1); |
|
511 qed "hypreal_add_right_cancel"; |
|
512 |
|
513 Goal "z + (y + -z) = (y::hypreal)"; |
|
514 by (simp_tac (simpset() addsimps hypreal_add_ac) 1); |
|
515 qed "hypreal_add_minus_cancel4"; |
|
516 Addsimps [hypreal_add_minus_cancel4]; |
|
517 |
|
518 Goal "z + (w + (x + (-z + y))) = w + x + (y::hypreal)"; |
|
519 by (simp_tac (simpset() addsimps hypreal_add_ac) 1); |
|
520 qed "hypreal_add_minus_cancel5"; |
|
521 Addsimps [hypreal_add_minus_cancel5]; |
|
522 |
|
523 |
|
524 (**** hyperreal multiplication: hypreal_mult ****) |
|
525 |
|
526 Goalw [congruent2_def] |
|
527 "congruent2 hyprel (%X Y. hyprel^^{%n. X n * Y n})"; |
|
528 by Safe_tac; |
|
529 by (ALLGOALS(Ultra_tac)); |
|
530 qed "hypreal_mult_congruent2"; |
|
531 |
|
532 (*Resolve th against the corresponding facts for hypreal_mult*) |
|
533 val hypreal_mult_ize = RSLIST [equiv_hyprel, hypreal_mult_congruent2]; |
|
534 |
|
535 Goalw [hypreal_mult_def] |
|
536 "Abs_hypreal(hyprel^^{%n. X n}) * Abs_hypreal(hyprel^^{%n. Y n}) = \ |
|
537 \ Abs_hypreal(hyprel^^{%n. X n * Y n})"; |
|
538 by (asm_simp_tac |
|
539 (simpset() addsimps [hypreal_mult_ize UN_equiv_class2]) 1); |
|
540 qed "hypreal_mult"; |
|
541 |
|
542 Goal "(z::hypreal) * w = w * z"; |
|
543 by (res_inst_tac [("z","z")] eq_Abs_hypreal 1); |
|
544 by (res_inst_tac [("z","w")] eq_Abs_hypreal 1); |
|
545 by (asm_simp_tac (simpset() addsimps ([hypreal_mult] @ real_mult_ac)) 1); |
|
546 qed "hypreal_mult_commute"; |
|
547 |
|
548 Goal "((z1::hypreal) * z2) * z3 = z1 * (z2 * z3)"; |
|
549 by (res_inst_tac [("z","z1")] eq_Abs_hypreal 1); |
|
550 by (res_inst_tac [("z","z2")] eq_Abs_hypreal 1); |
|
551 by (res_inst_tac [("z","z3")] eq_Abs_hypreal 1); |
|
552 by (asm_simp_tac (simpset() addsimps [hypreal_mult,real_mult_assoc]) 1); |
|
553 qed "hypreal_mult_assoc"; |
|
554 |
|
555 qed_goal "hypreal_mult_left_commute" thy |
|
556 "(z1::hypreal) * (z2 * z3) = z2 * (z1 * z3)" |
|
557 (fn _ => [rtac (hypreal_mult_commute RS trans) 1, rtac (hypreal_mult_assoc RS trans) 1, |
|
558 rtac (hypreal_mult_commute RS arg_cong) 1]); |
|
559 |
|
560 (* hypreal multiplication is an AC operator *) |
|
561 val hypreal_mult_ac = [hypreal_mult_assoc, hypreal_mult_commute, |
|
562 hypreal_mult_left_commute]; |
|
563 |
|
564 Goalw [hypreal_one_def] "1hr * z = z"; |
|
565 by (res_inst_tac [("z","z")] eq_Abs_hypreal 1); |
|
566 by (asm_full_simp_tac (simpset() addsimps [hypreal_mult]) 1); |
|
567 qed "hypreal_mult_1"; |
|
568 |
|
569 Goal "z * 1hr = z"; |
|
570 by (simp_tac (simpset() addsimps [hypreal_mult_commute, |
|
571 hypreal_mult_1]) 1); |
|
572 qed "hypreal_mult_1_right"; |
|
573 |
|
574 Goalw [hypreal_zero_def] "0hr * z = 0hr"; |
|
575 by (res_inst_tac [("z","z")] eq_Abs_hypreal 1); |
|
576 by (asm_full_simp_tac (simpset() addsimps [hypreal_mult,real_mult_0]) 1); |
|
577 qed "hypreal_mult_0"; |
|
578 |
|
579 Goal "z * 0hr = 0hr"; |
|
580 by (simp_tac (simpset() addsimps [hypreal_mult_commute, |
|
581 hypreal_mult_0]) 1); |
|
582 qed "hypreal_mult_0_right"; |
|
583 |
|
584 Addsimps [hypreal_mult_0,hypreal_mult_0_right]; |
|
585 |
|
586 Goal "-(x * y) = -x * (y::hypreal)"; |
|
587 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); |
|
588 by (res_inst_tac [("z","y")] eq_Abs_hypreal 1); |
|
589 by (auto_tac (claset(),simpset() addsimps [hypreal_minus, |
|
590 hypreal_mult,real_minus_mult_eq1] |
|
591 @ real_mult_ac @ real_add_ac)); |
|
592 qed "hypreal_minus_mult_eq1"; |
|
593 |
|
594 Goal "-(x * y) = (x::hypreal) * -y"; |
|
595 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); |
|
596 by (res_inst_tac [("z","y")] eq_Abs_hypreal 1); |
|
597 by (auto_tac (claset(),simpset() addsimps [hypreal_minus, |
|
598 hypreal_mult,real_minus_mult_eq2] |
|
599 @ real_mult_ac @ real_add_ac)); |
|
600 qed "hypreal_minus_mult_eq2"; |
|
601 |
|
602 Goal "-x*-y = x*(y::hypreal)"; |
|
603 by (full_simp_tac (simpset() addsimps [hypreal_minus_mult_eq2 RS sym, |
|
604 hypreal_minus_mult_eq1 RS sym]) 1); |
|
605 qed "hypreal_minus_mult_cancel"; |
|
606 |
|
607 Addsimps [hypreal_minus_mult_cancel]; |
|
608 |
|
609 Goal "-x*y = (x::hypreal)*-y"; |
|
610 by (full_simp_tac (simpset() addsimps [hypreal_minus_mult_eq2 RS sym, |
|
611 hypreal_minus_mult_eq1 RS sym]) 1); |
|
612 qed "hypreal_minus_mult_commute"; |
|
613 |
|
614 |
|
615 (*----------------------------------------------------------------------------- |
|
616 A few more theorems |
|
617 ----------------------------------------------------------------------------*) |
|
618 Goal "(z::hypreal) + v = z' + v' ==> z + (v + w) = z' + (v' + w)"; |
|
619 by (asm_simp_tac (simpset() addsimps [hypreal_add_assoc RS sym]) 1); |
|
620 qed "hypreal_add_assoc_cong"; |
|
621 |
|
622 Goal "(z::hypreal) + (v + w) = v + (z + w)"; |
|
623 by (REPEAT (ares_tac [hypreal_add_commute RS hypreal_add_assoc_cong] 1)); |
|
624 qed "hypreal_add_assoc_swap"; |
|
625 |
|
626 Goal "((z1::hypreal) + z2) * w = (z1 * w) + (z2 * w)"; |
|
627 by (res_inst_tac [("z","z1")] eq_Abs_hypreal 1); |
|
628 by (res_inst_tac [("z","z2")] eq_Abs_hypreal 1); |
|
629 by (res_inst_tac [("z","w")] eq_Abs_hypreal 1); |
|
630 by (asm_simp_tac (simpset() addsimps [hypreal_mult,hypreal_add, |
|
631 real_add_mult_distrib]) 1); |
|
632 qed "hypreal_add_mult_distrib"; |
|
633 |
|
634 val hypreal_mult_commute'= read_instantiate [("z","w")] hypreal_mult_commute; |
|
635 |
|
636 Goal "(w::hypreal) * (z1 + z2) = (w * z1) + (w * z2)"; |
|
637 by (simp_tac (simpset() addsimps [hypreal_mult_commute',hypreal_add_mult_distrib]) 1); |
|
638 qed "hypreal_add_mult_distrib2"; |
|
639 |
|
640 val hypreal_mult_simps = [hypreal_mult_1, hypreal_mult_1_right]; |
|
641 Addsimps hypreal_mult_simps; |
|
642 |
|
643 (*** one and zero are distinct ***) |
|
644 Goalw [hypreal_zero_def,hypreal_one_def] "0hr ~= 1hr"; |
|
645 by (auto_tac (claset(),simpset() addsimps [real_zero_not_eq_one])); |
|
646 qed "hypreal_zero_not_eq_one"; |
|
647 |
|
648 (*** existence of inverse ***) |
|
649 Goalw [hypreal_one_def,hypreal_zero_def] |
|
650 "x ~= 0hr ==> x*hrinv(x) = 1hr"; |
|
651 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); |
|
652 by (rotate_tac 1 1); |
|
653 by (asm_full_simp_tac (simpset() addsimps [hypreal_hrinv, |
|
654 hypreal_mult] setloop (split_tac [expand_if])) 1); |
|
655 by (dtac FreeUltrafilterNat_Compl_mem 1); |
|
656 by (blast_tac (claset() addSIs [real_mult_inv_right, |
|
657 FreeUltrafilterNat_subset]) 1); |
|
658 qed "hypreal_mult_hrinv"; |
|
659 |
|
660 Goal "x ~= 0hr ==> hrinv(x)*x = 1hr"; |
|
661 by (asm_simp_tac (simpset() addsimps [hypreal_mult_hrinv, |
|
662 hypreal_mult_commute]) 1); |
|
663 qed "hypreal_mult_hrinv_left"; |
|
664 |
|
665 Goal "x ~= 0hr ==> ? y. (x::hypreal) * y = 1hr"; |
|
666 by (fast_tac (claset() addDs [hypreal_mult_hrinv]) 1); |
|
667 qed "hypreal_hrinv_ex"; |
|
668 |
|
669 Goal "x ~= 0hr ==> ? y. y * (x::hypreal) = 1hr"; |
|
670 by (fast_tac (claset() addDs [hypreal_mult_hrinv_left]) 1); |
|
671 qed "hypreal_hrinv_left_ex"; |
|
672 |
|
673 Goal "x ~= 0hr ==> ?! y. (x::hypreal) * y = 1hr"; |
|
674 by (auto_tac (claset() addIs [hypreal_mult_hrinv],simpset())); |
|
675 by (dres_inst_tac [("f","%x. ya*x")] arg_cong 1); |
|
676 by (asm_full_simp_tac (simpset() addsimps [hypreal_mult_assoc RS sym]) 1); |
|
677 by (asm_full_simp_tac (simpset() addsimps [hypreal_mult_commute]) 1); |
|
678 qed "hypreal_hrinv_ex1"; |
|
679 |
|
680 Goal "x ~= 0hr ==> ?! y. y * (x::hypreal) = 1hr"; |
|
681 by (auto_tac (claset() addIs [hypreal_mult_hrinv_left],simpset())); |
|
682 by (dres_inst_tac [("f","%x. x*ya")] arg_cong 1); |
|
683 by (asm_full_simp_tac (simpset() addsimps [hypreal_mult_assoc]) 1); |
|
684 by (asm_full_simp_tac (simpset() addsimps [hypreal_mult_commute]) 1); |
|
685 qed "hypreal_hrinv_left_ex1"; |
|
686 |
|
687 Goal "[| y~= 0hr; x * y = 1hr |] ==> x = hrinv y"; |
|
688 by (forw_inst_tac [("x","y")] hypreal_mult_hrinv_left 1); |
|
689 by (res_inst_tac [("x1","y")] (hypreal_hrinv_left_ex1 RS ex1E) 1); |
|
690 by (assume_tac 1); |
|
691 by (Blast_tac 1); |
|
692 qed "hypreal_mult_inv_hrinv"; |
|
693 |
|
694 Goal "x ~= 0hr ==> ? y. x = hrinv y"; |
|
695 by (forw_inst_tac [("x","x")] hypreal_hrinv_left_ex 1); |
|
696 by (etac exE 1 THEN |
|
697 forw_inst_tac [("x","y")] hypreal_mult_inv_hrinv 1); |
|
698 by (res_inst_tac [("x","y")] exI 2); |
|
699 by Auto_tac; |
|
700 qed "hypreal_as_inverse_ex"; |
|
701 |
|
702 Goal "(c::hypreal) ~= 0hr ==> (c*a=c*b) = (a=b)"; |
|
703 by Auto_tac; |
|
704 by (dres_inst_tac [("f","%x. x*hrinv c")] arg_cong 1); |
|
705 by (asm_full_simp_tac (simpset() addsimps [hypreal_mult_hrinv] @ hypreal_mult_ac) 1); |
|
706 qed "hypreal_mult_left_cancel"; |
|
707 |
|
708 Goal "(c::hypreal) ~= 0hr ==> (a*c=b*c) = (a=b)"; |
|
709 by (Step_tac 1); |
|
710 by (dres_inst_tac [("f","%x. x*hrinv c")] arg_cong 1); |
|
711 by (asm_full_simp_tac (simpset() addsimps [hypreal_mult_hrinv] @ hypreal_mult_ac) 1); |
|
712 qed "hypreal_mult_right_cancel"; |
|
713 |
|
714 Goalw [hypreal_zero_def] "x ~= 0hr ==> hrinv(x) ~= 0hr"; |
|
715 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); |
|
716 by (rotate_tac 1 1); |
|
717 by (asm_full_simp_tac (simpset() addsimps [hypreal_hrinv, |
|
718 hypreal_mult] setloop (split_tac [expand_if])) 1); |
|
719 by (dtac FreeUltrafilterNat_Compl_mem 1 THEN Clarify_tac 1); |
|
720 by (ultra_tac (claset() addIs [ccontr] addDs |
|
721 [rinv_not_zero],simpset()) 1); |
|
722 qed "hrinv_not_zero"; |
|
723 |
|
724 Addsimps [hypreal_mult_hrinv,hypreal_mult_hrinv_left]; |
|
725 |
|
726 Goal "[| x ~= 0hr; y ~= 0hr |] ==> x * y ~= 0hr"; |
|
727 by (Step_tac 1); |
|
728 by (dres_inst_tac [("f","%z. hrinv x*z")] arg_cong 1); |
|
729 by (asm_full_simp_tac (simpset() addsimps [hypreal_mult_assoc RS sym]) 1); |
|
730 qed "hypreal_mult_not_0"; |
|
731 |
|
732 bind_thm ("hypreal_mult_not_0E",hypreal_mult_not_0 RS notE); |
|
733 |
|
734 Goal "x ~= 0hr ==> x * x ~= 0hr"; |
|
735 by (blast_tac (claset() addDs [hypreal_mult_not_0]) 1); |
|
736 qed "hypreal_mult_self_not_zero"; |
|
737 |
|
738 Goal "[| x ~= 0hr; y ~= 0hr |] ==> hrinv(x*y) = hrinv(x)*hrinv(y)"; |
|
739 by (res_inst_tac [("c1","x")] (hypreal_mult_left_cancel RS iffD1) 1); |
|
740 by (auto_tac (claset(),simpset() addsimps [hypreal_mult_assoc RS sym, |
|
741 hypreal_mult_not_0])); |
|
742 by (res_inst_tac [("c1","y")] (hypreal_mult_right_cancel RS iffD1) 1); |
|
743 by (auto_tac (claset(),simpset() addsimps [hypreal_mult_not_0] @ hypreal_mult_ac)); |
|
744 by (auto_tac (claset(),simpset() addsimps [hypreal_mult_assoc RS sym,hypreal_mult_not_0])); |
|
745 qed "hrinv_mult_eq"; |
|
746 |
|
747 Goal "x ~= 0hr ==> hrinv(-x) = -hrinv(x)"; |
|
748 by (res_inst_tac [("c1","-x")] (hypreal_mult_right_cancel RS iffD1) 1); |
|
749 by Auto_tac; |
|
750 qed "hypreal_minus_hrinv"; |
|
751 |
|
752 Goal "[| x ~= 0hr; y ~= 0hr |] \ |
|
753 \ ==> hrinv(x*y) = hrinv(x)*hrinv(y)"; |
|
754 by (forw_inst_tac [("y","y")] hypreal_mult_not_0 1 THEN assume_tac 1); |
|
755 by (res_inst_tac [("c1","x")] (hypreal_mult_left_cancel RS iffD1) 1); |
|
756 by (auto_tac (claset(),simpset() addsimps [hypreal_mult_assoc RS sym])); |
|
757 by (res_inst_tac [("c1","y")] (hypreal_mult_left_cancel RS iffD1) 1); |
|
758 by (auto_tac (claset(),simpset() addsimps [hypreal_mult_left_commute])); |
|
759 by (asm_simp_tac (simpset() addsimps [hypreal_mult_assoc RS sym]) 1); |
|
760 qed "hypreal_hrinv_distrib"; |
|
761 |
|
762 (*------------------------------------------------------------------ |
|
763 Theorems for ordering |
|
764 ------------------------------------------------------------------*) |
|
765 |
|
766 (* prove introduction and elimination rules for hypreal_less *) |
|
767 |
|
768 Goalw [hypreal_less_def] |
|
769 "P < (Q::hypreal) = (EX X Y. X : Rep_hypreal(P) & \ |
|
770 \ Y : Rep_hypreal(Q) & \ |
|
771 \ {n. X n < Y n} : FreeUltrafilterNat)"; |
|
772 by (Fast_tac 1); |
|
773 qed "hypreal_less_iff"; |
|
774 |
|
775 Goalw [hypreal_less_def] |
|
776 "[| {n. X n < Y n} : FreeUltrafilterNat; \ |
|
777 \ X : Rep_hypreal(P); \ |
|
778 \ Y : Rep_hypreal(Q) |] ==> P < (Q::hypreal)"; |
|
779 by (Fast_tac 1); |
|
780 qed "hypreal_lessI"; |
|
781 |
|
782 |
|
783 Goalw [hypreal_less_def] |
|
784 "!! R1. [| R1 < (R2::hypreal); \ |
|
785 \ !!X Y. {n. X n < Y n} : FreeUltrafilterNat ==> P; \ |
|
786 \ !!X. X : Rep_hypreal(R1) ==> P; \ |
|
787 \ !!Y. Y : Rep_hypreal(R2) ==> P |] \ |
|
788 \ ==> P"; |
|
789 by Auto_tac; |
|
790 qed "hypreal_lessE"; |
|
791 |
|
792 Goalw [hypreal_less_def] |
|
793 "R1 < (R2::hypreal) ==> (EX X Y. {n. X n < Y n} : FreeUltrafilterNat & \ |
|
794 \ X : Rep_hypreal(R1) & \ |
|
795 \ Y : Rep_hypreal(R2))"; |
|
796 by (Fast_tac 1); |
|
797 qed "hypreal_lessD"; |
|
798 |
|
799 Goal "~ (R::hypreal) < R"; |
|
800 by (res_inst_tac [("z","R")] eq_Abs_hypreal 1); |
|
801 by (auto_tac (claset(),simpset() addsimps [hypreal_less_def])); |
|
802 by (Ultra_tac 1); |
|
803 qed "hypreal_less_not_refl"; |
|
804 |
|
805 (*** y < y ==> P ***) |
|
806 bind_thm("hypreal_less_irrefl",hypreal_less_not_refl RS notE); |
|
807 |
|
808 Goal "!!(x::hypreal). x < y ==> x ~= y"; |
|
809 by (auto_tac (claset(),simpset() addsimps [hypreal_less_not_refl])); |
|
810 qed "hypreal_not_refl2"; |
|
811 |
|
812 Goal "!!(R1::hypreal). [| R1 < R2; R2 < R3 |] ==> R1 < R3"; |
|
813 by (res_inst_tac [("z","R1")] eq_Abs_hypreal 1); |
|
814 by (res_inst_tac [("z","R2")] eq_Abs_hypreal 1); |
|
815 by (res_inst_tac [("z","R3")] eq_Abs_hypreal 1); |
|
816 by (auto_tac (claset() addSIs [exI],simpset() |
|
817 addsimps [hypreal_less_def])); |
|
818 by (ultra_tac (claset() addIs [real_less_trans],simpset()) 1); |
|
819 qed "hypreal_less_trans"; |
|
820 |
|
821 Goal "!! (R1::hypreal). [| R1 < R2; R2 < R1 |] ==> P"; |
|
822 by (dtac hypreal_less_trans 1 THEN assume_tac 1); |
|
823 by (asm_full_simp_tac (simpset() addsimps |
|
824 [hypreal_less_not_refl]) 1); |
|
825 qed "hypreal_less_asym"; |
|
826 |
|
827 (*-------------------------------------------------------- |
|
828 TODO: The following theorem should have been proved |
|
829 first and then used througout the proofs as it probably |
|
830 makes many of them more straightforward. |
|
831 -------------------------------------------------------*) |
|
832 Goalw [hypreal_less_def] |
|
833 "(Abs_hypreal(hyprel^^{%n. X n}) < \ |
|
834 \ Abs_hypreal(hyprel^^{%n. Y n})) = \ |
|
835 \ ({n. X n < Y n} : FreeUltrafilterNat)"; |
|
836 by (auto_tac (claset() addSIs [lemma_hyprel_refl],simpset())); |
|
837 by (Ultra_tac 1); |
|
838 qed "hypreal_less"; |
|
839 |
|
840 (*--------------------------------------------------------------------------------- |
|
841 Hyperreals as a linearly ordered field |
|
842 ---------------------------------------------------------------------------------*) |
|
843 (*** sum order ***) |
|
844 |
|
845 Goalw [hypreal_zero_def] |
|
846 "[| 0hr < x; 0hr < y |] ==> 0hr < x + y"; |
|
847 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); |
|
848 by (res_inst_tac [("z","y")] eq_Abs_hypreal 1); |
|
849 by (auto_tac (claset(),simpset() addsimps |
|
850 [hypreal_less_def,hypreal_add])); |
|
851 by (auto_tac (claset() addSIs [exI],simpset() addsimps |
|
852 [hypreal_less_def,hypreal_add])); |
|
853 by (ultra_tac (claset() addIs [real_add_order],simpset()) 1); |
|
854 qed "hypreal_add_order"; |
|
855 |
|
856 (*** mult order ***) |
|
857 |
|
858 Goalw [hypreal_zero_def] |
|
859 "[| 0hr < x; 0hr < y |] ==> 0hr < x * y"; |
|
860 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); |
|
861 by (res_inst_tac [("z","y")] eq_Abs_hypreal 1); |
|
862 by (auto_tac (claset() addSIs [exI],simpset() addsimps |
|
863 [hypreal_less_def,hypreal_mult])); |
|
864 by (ultra_tac (claset() addIs [real_mult_order],simpset()) 1); |
|
865 qed "hypreal_mult_order"; |
|
866 |
|
867 (*--------------------------------------------------------------------------------- |
|
868 Trichotomy of the hyperreals |
|
869 --------------------------------------------------------------------------------*) |
|
870 |
|
871 Goalw [hyprel_def] "? x. x: hyprel ^^ {%n. 0r}"; |
|
872 by (res_inst_tac [("x","%n. 0r")] exI 1); |
|
873 by (Step_tac 1); |
|
874 by (auto_tac (claset() addSIs [FreeUltrafilterNat_Nat_set],simpset())); |
|
875 qed "lemma_hyprel_0r_mem"; |
|
876 |
|
877 Goalw [hypreal_zero_def]"0hr < x | x = 0hr | x < 0hr"; |
|
878 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); |
|
879 by (auto_tac (claset(),simpset() addsimps [hypreal_less_def])); |
|
880 by (cut_facts_tac [lemma_hyprel_0r_mem] 1 THEN etac exE 1); |
|
881 by (dres_inst_tac [("x","xa")] spec 1); |
|
882 by (dres_inst_tac [("x","x")] spec 1); |
|
883 by (cut_inst_tac [("x","x")] lemma_hyprel_refl 1); |
|
884 by Auto_tac; |
|
885 by (dres_inst_tac [("x","x")] spec 1); |
|
886 by (dres_inst_tac [("x","xa")] spec 1); |
|
887 by Auto_tac; |
|
888 by (Ultra_tac 1); |
|
889 by (auto_tac (claset() addIs [real_linear_less2],simpset())); |
|
890 qed "hypreal_trichotomy"; |
|
891 |
|
892 val prems = Goal "[| 0hr < x ==> P; \ |
|
893 \ x = 0hr ==> P; \ |
|
894 \ x < 0hr ==> P |] ==> P"; |
|
895 by (cut_inst_tac [("x","x")] hypreal_trichotomy 1); |
|
896 by (REPEAT (eresolve_tac (disjE::prems) 1)); |
|
897 qed "hypreal_trichotomyE"; |
|
898 |
|
899 (*---------------------------------------------------------------------------- |
|
900 More properties of < |
|
901 ----------------------------------------------------------------------------*) |
|
902 Goal "!!(A::hypreal). A < B ==> A + C < B + C"; |
|
903 by (res_inst_tac [("z","A")] eq_Abs_hypreal 1); |
|
904 by (res_inst_tac [("z","B")] eq_Abs_hypreal 1); |
|
905 by (res_inst_tac [("z","C")] eq_Abs_hypreal 1); |
|
906 by (auto_tac (claset() addSIs [exI],simpset() addsimps |
|
907 [hypreal_less_def,hypreal_add])); |
|
908 by (Ultra_tac 1); |
|
909 qed "hypreal_add_less_mono1"; |
|
910 |
|
911 Goal "!!(A::hypreal). A < B ==> C + A < C + B"; |
|
912 by (auto_tac (claset() addIs [hypreal_add_less_mono1], |
|
913 simpset() addsimps [hypreal_add_commute])); |
|
914 qed "hypreal_add_less_mono2"; |
|
915 |
|
916 Goal "((x::hypreal) < y) = (0hr < y + -x)"; |
|
917 by (Step_tac 1); |
|
918 by (dres_inst_tac [("C","-x")] hypreal_add_less_mono1 1); |
|
919 by (dres_inst_tac [("C","x")] hypreal_add_less_mono1 2); |
|
920 by (auto_tac (claset(),simpset() addsimps [hypreal_add_assoc])); |
|
921 qed "hypreal_less_minus_iff"; |
|
922 |
|
923 Goal "((x::hypreal) < y) = (x + -y< 0hr)"; |
|
924 by (Step_tac 1); |
|
925 by (dres_inst_tac [("C","-y")] hypreal_add_less_mono1 1); |
|
926 by (dres_inst_tac [("C","y")] hypreal_add_less_mono1 2); |
|
927 by (auto_tac (claset(),simpset() addsimps [hypreal_add_assoc])); |
|
928 qed "hypreal_less_minus_iff2"; |
|
929 |
|
930 Goal "!!(y1 :: hypreal). [| z1 < y1; z2 < y2 |] ==> z1 + z2 < y1 + y2"; |
|
931 by (dtac (hypreal_less_minus_iff RS iffD1) 1); |
|
932 by (dtac (hypreal_less_minus_iff RS iffD1) 1); |
|
933 by (dtac hypreal_add_order 1 THEN assume_tac 1); |
|
934 by (thin_tac "0hr < y2 + - z2" 1); |
|
935 by (dres_inst_tac [("C","z1 + z2")] hypreal_add_less_mono1 1); |
|
936 by (auto_tac (claset(),simpset() addsimps |
|
937 [hypreal_minus_add_distrib RS sym] @ hypreal_add_ac)); |
|
938 qed "hypreal_add_less_mono"; |
|
939 |
|
940 Goal "((x::hypreal) = y) = (0hr = x + - y)"; |
|
941 by Auto_tac; |
|
942 by (res_inst_tac [("x1","-y")] (hypreal_add_right_cancel RS iffD1) 1); |
|
943 by Auto_tac; |
|
944 qed "hypreal_eq_minus_iff"; |
|
945 |
|
946 Goal "((x::hypreal) = y) = (0hr = y + - x)"; |
|
947 by Auto_tac; |
|
948 by (res_inst_tac [("x1","-x")] (hypreal_add_right_cancel RS iffD1) 1); |
|
949 by Auto_tac; |
|
950 qed "hypreal_eq_minus_iff2"; |
|
951 |
|
952 Goal "(x = y + z) = (x + -z = (y::hypreal))"; |
|
953 by (auto_tac (claset(),simpset() addsimps [hypreal_add_assoc])); |
|
954 qed "hypreal_eq_minus_iff3"; |
|
955 |
|
956 Goal "(x = z + y) = (x + -z = (y::hypreal))"; |
|
957 by (auto_tac (claset(),simpset() addsimps hypreal_add_ac)); |
|
958 qed "hypreal_eq_minus_iff4"; |
|
959 |
|
960 Goal "(x ~= a) = (x + -a ~= 0hr)"; |
|
961 by (auto_tac (claset() addDs [sym RS |
|
962 (hypreal_eq_minus_iff RS iffD2)],simpset())); |
|
963 qed "hypreal_not_eq_minus_iff"; |
|
964 |
|
965 (*** linearity ***) |
|
966 Goal "(x::hypreal) < y | x = y | y < x"; |
|
967 by (rtac (hypreal_eq_minus_iff2 RS ssubst) 1); |
|
968 by (res_inst_tac [("x1","x")] (hypreal_less_minus_iff RS ssubst) 1); |
|
969 by (res_inst_tac [("x1","y")] (hypreal_less_minus_iff2 RS ssubst) 1); |
|
970 by (rtac hypreal_trichotomyE 1); |
|
971 by Auto_tac; |
|
972 qed "hypreal_linear"; |
|
973 |
|
974 Goal "!!(x::hypreal). [| x < y ==> P; x = y ==> P; \ |
|
975 \ y < x ==> P |] ==> P"; |
|
976 by (cut_inst_tac [("x","x"),("y","y")] hypreal_linear 1); |
|
977 by Auto_tac; |
|
978 qed "hypreal_linear_less2"; |
|
979 |
|
980 (*------------------------------------------------------------------------------ |
|
981 Properties of <= |
|
982 ------------------------------------------------------------------------------*) |
|
983 (*------ hypreal le iff reals le a.e ------*) |
|
984 |
|
985 Goalw [hypreal_le_def,real_le_def] |
|
986 "(Abs_hypreal(hyprel^^{%n. X n}) <= \ |
|
987 \ Abs_hypreal(hyprel^^{%n. Y n})) = \ |
|
988 \ ({n. X n <= Y n} : FreeUltrafilterNat)"; |
|
989 by (auto_tac (claset(),simpset() addsimps [hypreal_less])); |
|
990 by (ALLGOALS(Ultra_tac)); |
|
991 qed "hypreal_le"; |
|
992 |
|
993 (*---------------------------------------------------------*) |
|
994 (*---------------------------------------------------------*) |
|
995 Goalw [hypreal_le_def] |
|
996 "~(w < z) ==> z <= (w::hypreal)"; |
|
997 by (assume_tac 1); |
|
998 qed "hypreal_leI"; |
|
999 |
|
1000 Goalw [hypreal_le_def] |
|
1001 "z<=w ==> ~(w<(z::hypreal))"; |
|
1002 by (assume_tac 1); |
|
1003 qed "hypreal_leD"; |
|
1004 |
|
1005 val hypreal_leE = make_elim hypreal_leD; |
|
1006 |
|
1007 Goal "(~(w < z)) = (z <= (w::hypreal))"; |
|
1008 by (fast_tac (claset() addSIs [hypreal_leI,hypreal_leD]) 1); |
|
1009 qed "hypreal_less_le_iff"; |
|
1010 |
|
1011 Goalw [hypreal_le_def] "~ z <= w ==> w<(z::hypreal)"; |
|
1012 by (Fast_tac 1); |
|
1013 qed "not_hypreal_leE"; |
|
1014 |
|
1015 Goalw [hypreal_le_def] "z < w ==> z <= (w::hypreal)"; |
|
1016 by (fast_tac (claset() addEs [hypreal_less_asym]) 1); |
|
1017 qed "hypreal_less_imp_le"; |
|
1018 |
|
1019 Goalw [hypreal_le_def] "!!(x::hypreal). x <= y ==> x < y | x = y"; |
|
1020 by (cut_facts_tac [hypreal_linear] 1); |
|
1021 by (fast_tac (claset() addEs [hypreal_less_irrefl,hypreal_less_asym]) 1); |
|
1022 qed "hypreal_le_imp_less_or_eq"; |
|
1023 |
|
1024 Goalw [hypreal_le_def] "z<w | z=w ==> z <=(w::hypreal)"; |
|
1025 by (cut_facts_tac [hypreal_linear] 1); |
|
1026 by (fast_tac (claset() addEs [hypreal_less_irrefl,hypreal_less_asym]) 1); |
|
1027 qed "hypreal_less_or_eq_imp_le"; |
|
1028 |
|
1029 Goal "(x <= (y::hypreal)) = (x < y | x=y)"; |
|
1030 by (REPEAT(ares_tac [iffI, hypreal_less_or_eq_imp_le, hypreal_le_imp_less_or_eq] 1)); |
|
1031 qed "hypreal_le_eq_less_or_eq"; |
|
1032 |
|
1033 Goal "w <= (w::hypreal)"; |
|
1034 by (simp_tac (simpset() addsimps [hypreal_le_eq_less_or_eq]) 1); |
|
1035 qed "hypreal_le_refl"; |
|
1036 Addsimps [hypreal_le_refl]; |
|
1037 |
|
1038 Goal "[| i <= j; j < k |] ==> i < (k::hypreal)"; |
|
1039 by (dtac hypreal_le_imp_less_or_eq 1); |
|
1040 by (fast_tac (claset() addIs [hypreal_less_trans]) 1); |
|
1041 qed "hypreal_le_less_trans"; |
|
1042 |
|
1043 Goal "!! (i::hypreal). [| i < j; j <= k |] ==> i < k"; |
|
1044 by (dtac hypreal_le_imp_less_or_eq 1); |
|
1045 by (fast_tac (claset() addIs [hypreal_less_trans]) 1); |
|
1046 qed "hypreal_less_le_trans"; |
|
1047 |
|
1048 Goal "[| i <= j; j <= k |] ==> i <= (k::hypreal)"; |
|
1049 by (EVERY1 [dtac hypreal_le_imp_less_or_eq, dtac hypreal_le_imp_less_or_eq, |
|
1050 rtac hypreal_less_or_eq_imp_le, fast_tac (claset() addIs [hypreal_less_trans])]); |
|
1051 qed "hypreal_le_trans"; |
|
1052 |
|
1053 Goal "[| z <= w; w <= z |] ==> z = (w::hypreal)"; |
|
1054 by (EVERY1 [dtac hypreal_le_imp_less_or_eq, dtac hypreal_le_imp_less_or_eq, |
|
1055 fast_tac (claset() addEs [hypreal_less_irrefl,hypreal_less_asym])]); |
|
1056 qed "hypreal_le_anti_sym"; |
|
1057 |
|
1058 Goal "[| 0hr < x; 0hr <= y |] ==> 0hr < x + y"; |
|
1059 by (auto_tac (claset() addDs [sym,hypreal_le_imp_less_or_eq] |
|
1060 addIs [hypreal_add_order],simpset())); |
|
1061 qed "hypreal_add_order_le"; |
|
1062 |
|
1063 (*------------------------------------------------------------------------ |
|
1064 ------------------------------------------------------------------------*) |
|
1065 |
|
1066 Goal "[| ~ y < x; y ~= x |] ==> x < (y::hypreal)"; |
|
1067 by (rtac not_hypreal_leE 1); |
|
1068 by (fast_tac (claset() addDs [hypreal_le_imp_less_or_eq]) 1); |
|
1069 qed "not_less_not_eq_hypreal_less"; |
|
1070 |
|
1071 Goal "(0hr < -R) = (R < 0hr)"; |
|
1072 by (Step_tac 1); |
|
1073 by (dres_inst_tac [("C","R")] hypreal_add_less_mono1 1); |
|
1074 by (dres_inst_tac [("C","-R")] hypreal_add_less_mono1 2); |
|
1075 by (auto_tac (claset(),simpset() addsimps [hypreal_add_assoc])); |
|
1076 qed "hypreal_minus_zero_less_iff"; |
|
1077 |
|
1078 Goal "(-R < 0hr) = (0hr < R)"; |
|
1079 by (Step_tac 1); |
|
1080 by (dres_inst_tac [("C","R")] hypreal_add_less_mono1 1); |
|
1081 by (dres_inst_tac [("C","-R")] hypreal_add_less_mono1 2); |
|
1082 by (auto_tac (claset(),simpset() addsimps [hypreal_add_assoc])); |
|
1083 qed "hypreal_minus_zero_less_iff2"; |
|
1084 |
|
1085 Goal "((x::hypreal) < y) = (-y < -x)"; |
|
1086 by (rtac (hypreal_less_minus_iff RS ssubst) 1); |
|
1087 by (res_inst_tac [("x1","x")] (hypreal_less_minus_iff RS ssubst) 1); |
|
1088 by (simp_tac (simpset() addsimps [hypreal_add_commute]) 1); |
|
1089 qed "hypreal_less_swap_iff"; |
|
1090 |
|
1091 Goal "(0hr < x) = (-x < x)"; |
|
1092 by (Step_tac 1); |
|
1093 by (rtac ccontr 2 THEN forward_tac |
|
1094 [hypreal_leI RS hypreal_le_imp_less_or_eq] 2); |
|
1095 by (Step_tac 2); |
|
1096 by (dtac (hypreal_minus_zero_less_iff RS iffD2) 2); |
|
1097 by (dres_inst_tac [("R2.0","-x")] hypreal_less_trans 2); |
|
1098 by (Auto_tac ); |
|
1099 by (forward_tac [hypreal_add_order] 1 THEN assume_tac 1); |
|
1100 by (dres_inst_tac [("C","-x"),("B","x + x")] hypreal_add_less_mono1 1); |
|
1101 by (auto_tac (claset(),simpset() addsimps [hypreal_add_assoc])); |
|
1102 qed "hypreal_gt_zero_iff"; |
|
1103 |
|
1104 Goal "(x < 0hr) = (x < -x)"; |
|
1105 by (rtac (hypreal_minus_zero_less_iff RS subst) 1); |
|
1106 by (rtac (hypreal_gt_zero_iff RS ssubst) 1); |
|
1107 by (Full_simp_tac 1); |
|
1108 qed "hypreal_lt_zero_iff"; |
|
1109 |
|
1110 Goalw [hypreal_le_def] "(0hr <= x) = (-x <= x)"; |
|
1111 by (auto_tac (claset(),simpset() addsimps [hypreal_lt_zero_iff RS sym])); |
|
1112 qed "hypreal_ge_zero_iff"; |
|
1113 |
|
1114 Goalw [hypreal_le_def] "(x <= 0hr) = (x <= -x)"; |
|
1115 by (auto_tac (claset(),simpset() addsimps [hypreal_gt_zero_iff RS sym])); |
|
1116 qed "hypreal_le_zero_iff"; |
|
1117 |
|
1118 Goal "[| x < 0hr; y < 0hr |] ==> 0hr < x * y"; |
|
1119 by (REPEAT(dtac (hypreal_minus_zero_less_iff RS iffD2) 1)); |
|
1120 by (dtac hypreal_mult_order 1 THEN assume_tac 1); |
|
1121 by (Asm_full_simp_tac 1); |
|
1122 qed "hypreal_mult_less_zero1"; |
|
1123 |
|
1124 Goal "[| 0hr <= x; 0hr <= y |] ==> 0hr <= x * y"; |
|
1125 by (REPEAT(dtac hypreal_le_imp_less_or_eq 1)); |
|
1126 by (auto_tac (claset() addIs [hypreal_mult_order, |
|
1127 hypreal_less_imp_le],simpset())); |
|
1128 qed "hypreal_le_mult_order"; |
|
1129 |
|
1130 Goal "[| x <= 0hr; y <= 0hr |] ==> 0hr <= x * y"; |
|
1131 by (rtac hypreal_less_or_eq_imp_le 1); |
|
1132 by (dtac hypreal_le_imp_less_or_eq 1 THEN etac disjE 1); |
|
1133 by Auto_tac; |
|
1134 by (dtac hypreal_le_imp_less_or_eq 1); |
|
1135 by (auto_tac (claset() addDs [hypreal_mult_less_zero1],simpset())); |
|
1136 qed "real_mult_le_zero1"; |
|
1137 |
|
1138 Goal "[| 0hr <= x; y < 0hr |] ==> x * y <= 0hr"; |
|
1139 by (rtac hypreal_less_or_eq_imp_le 1); |
|
1140 by (dtac hypreal_le_imp_less_or_eq 1 THEN etac disjE 1); |
|
1141 by Auto_tac; |
|
1142 by (dtac (hypreal_minus_zero_less_iff RS iffD2) 1); |
|
1143 by (rtac (hypreal_minus_zero_less_iff RS subst) 1); |
|
1144 by (blast_tac (claset() addDs [hypreal_mult_order] |
|
1145 addIs [hypreal_minus_mult_eq2 RS ssubst]) 1); |
|
1146 qed "hypreal_mult_le_zero"; |
|
1147 |
|
1148 Goal "[| 0hr < x; y < 0hr |] ==> x*y < 0hr"; |
|
1149 by (dtac (hypreal_minus_zero_less_iff RS iffD2) 1); |
|
1150 by (dtac hypreal_mult_order 1 THEN assume_tac 1); |
|
1151 by (rtac (hypreal_minus_zero_less_iff RS iffD1) 1); |
|
1152 by (asm_full_simp_tac (simpset() addsimps [hypreal_minus_mult_eq2]) 1); |
|
1153 qed "hypreal_mult_less_zero"; |
|
1154 |
|
1155 Goalw [hypreal_one_def,hypreal_zero_def,hypreal_less_def] "0hr < 1hr"; |
|
1156 by (res_inst_tac [("x","%n. 0r")] exI 1); |
|
1157 by (res_inst_tac [("x","%n. 1r")] exI 1); |
|
1158 by (auto_tac (claset(),simpset() addsimps [real_zero_less_one, |
|
1159 FreeUltrafilterNat_Nat_set])); |
|
1160 qed "hypreal_zero_less_one"; |
|
1161 |
|
1162 Goal "[| 0hr <= x; 0hr <= y |] ==> 0hr <= x + y"; |
|
1163 by (REPEAT(dtac hypreal_le_imp_less_or_eq 1)); |
|
1164 by (auto_tac (claset() addIs [hypreal_add_order, |
|
1165 hypreal_less_imp_le],simpset())); |
|
1166 qed "hypreal_le_add_order"; |
|
1167 |
|
1168 Goal "!!(q1::hypreal). q1 <= q2 ==> x + q1 <= x + q2"; |
|
1169 by (dtac hypreal_le_imp_less_or_eq 1); |
|
1170 by (Step_tac 1); |
|
1171 by (auto_tac (claset() addSIs [hypreal_le_refl, |
|
1172 hypreal_less_imp_le,hypreal_add_less_mono1], |
|
1173 simpset() addsimps [hypreal_add_commute])); |
|
1174 qed "hypreal_add_left_le_mono1"; |
|
1175 |
|
1176 Goal "!!(q1::hypreal). q1 <= q2 ==> q1 + x <= q2 + x"; |
|
1177 by (auto_tac (claset() addDs [hypreal_add_left_le_mono1], |
|
1178 simpset() addsimps [hypreal_add_commute])); |
|
1179 qed "hypreal_add_le_mono1"; |
|
1180 |
|
1181 Goal "!!k l::hypreal. [|i<=j; k<=l |] ==> i + k <= j + l"; |
|
1182 by (etac (hypreal_add_le_mono1 RS hypreal_le_trans) 1); |
|
1183 by (simp_tac (simpset() addsimps [hypreal_add_commute]) 1); |
|
1184 (*j moves to the end because it is free while k, l are bound*) |
|
1185 by (etac hypreal_add_le_mono1 1); |
|
1186 qed "hypreal_add_le_mono"; |
|
1187 |
|
1188 Goal "!!k l::hypreal. [|i<j; k<=l |] ==> i + k < j + l"; |
|
1189 by (auto_tac (claset() addSDs [hypreal_le_imp_less_or_eq] |
|
1190 addIs [hypreal_add_less_mono1,hypreal_add_less_mono],simpset())); |
|
1191 qed "hypreal_add_less_le_mono"; |
|
1192 |
|
1193 Goal "!!k l::hypreal. [|i<=j; k<l |] ==> i + k < j + l"; |
|
1194 by (auto_tac (claset() addSDs [hypreal_le_imp_less_or_eq] |
|
1195 addIs [hypreal_add_less_mono2,hypreal_add_less_mono],simpset())); |
|
1196 qed "hypreal_add_le_less_mono"; |
|
1197 |
|
1198 Goal "(0hr*x<r)=(0hr<r)"; |
|
1199 by (Simp_tac 1); |
|
1200 qed "hypreal_mult_0_less"; |
|
1201 |
|
1202 Goal "[| 0hr < z; x < y |] ==> x*z < y*z"; |
|
1203 by (rotate_tac 1 1); |
|
1204 by (dtac (hypreal_less_minus_iff RS iffD1) 1); |
|
1205 by (rtac (hypreal_less_minus_iff RS iffD2) 1); |
|
1206 by (dtac hypreal_mult_order 1 THEN assume_tac 1); |
|
1207 by (asm_full_simp_tac (simpset() addsimps [hypreal_add_mult_distrib2, |
|
1208 hypreal_minus_mult_eq2 RS sym, hypreal_mult_commute ]) 1); |
|
1209 qed "hypreal_mult_less_mono1"; |
|
1210 |
|
1211 Goal "[| 0hr<z; x<y |] ==> z*x<z*y"; |
|
1212 by (asm_simp_tac (simpset() addsimps [hypreal_mult_commute,hypreal_mult_less_mono1]) 1); |
|
1213 qed "hypreal_mult_less_mono2"; |
|
1214 |
|
1215 Goal "[| 0hr<=z; x<y |] ==> x*z<=y*z"; |
|
1216 by (EVERY1 [rtac hypreal_less_or_eq_imp_le, dtac hypreal_le_imp_less_or_eq]); |
|
1217 by (auto_tac (claset() addIs [hypreal_mult_less_mono1],simpset())); |
|
1218 qed "hypreal_mult_le_less_mono1"; |
|
1219 |
|
1220 Goal "[| 0hr<=z; x<y |] ==> z*x<=z*y"; |
|
1221 by (asm_simp_tac (simpset() addsimps [hypreal_mult_commute, |
|
1222 hypreal_mult_le_less_mono1]) 1); |
|
1223 qed "hypreal_mult_le_less_mono2"; |
|
1224 |
|
1225 Goal "[| 0hr<=z; x<=y |] ==> z*x<=z*y"; |
|
1226 by (dres_inst_tac [("x","x")] hypreal_le_imp_less_or_eq 1); |
|
1227 by (auto_tac (claset() addIs [hypreal_mult_le_less_mono2,hypreal_le_refl],simpset())); |
|
1228 qed "hypreal_mult_le_le_mono1"; |
|
1229 |
|
1230 val prem1::prem2::prem3::rest = goal thy |
|
1231 "[| 0hr<y; x<r; y*r<t*s |] ==> y*x<t*s"; |
|
1232 by (rtac ([([prem1,prem2] MRS hypreal_mult_less_mono2),prem3] MRS hypreal_less_trans) 1); |
|
1233 qed "hypreal_mult_less_trans"; |
|
1234 |
|
1235 Goal "[| 0hr<=y; x<r; y*r<t*s; 0hr<t*s|] ==> y*x<t*s"; |
|
1236 by (dtac hypreal_le_imp_less_or_eq 1); |
|
1237 by (fast_tac (HOL_cs addEs [(hypreal_mult_0_less RS iffD2),hypreal_mult_less_trans]) 1); |
|
1238 qed "hypreal_mult_le_less_trans"; |
|
1239 |
|
1240 Goal "[| 0hr <= y; x <= r; y*r < t*s; 0hr < t*s|] ==> y*x < t*s"; |
|
1241 by (dres_inst_tac [("x","x")] hypreal_le_imp_less_or_eq 1); |
|
1242 by (fast_tac (claset() addIs [hypreal_mult_le_less_trans]) 1); |
|
1243 qed "hypreal_mult_le_le_trans"; |
|
1244 |
|
1245 Goal "[| 0hr < r1; r1 <r2; 0hr < x; x < y|] \ |
|
1246 \ ==> r1 * x < r2 * y"; |
|
1247 by (dres_inst_tac [("x","x")] hypreal_mult_less_mono2 1); |
|
1248 by (dres_inst_tac [("R1.0","0hr")] hypreal_less_trans 2); |
|
1249 by (dres_inst_tac [("x","r1")] hypreal_mult_less_mono1 3); |
|
1250 by Auto_tac; |
|
1251 by (blast_tac (claset() addIs [hypreal_less_trans]) 1); |
|
1252 qed "hypreal_mult_less_mono"; |
|
1253 |
|
1254 Goal "[| 0hr < r1; r1 <r2; 0hr < y|] \ |
|
1255 \ ==> 0hr < r2 * y"; |
|
1256 by (dres_inst_tac [("R1.0","0hr")] hypreal_less_trans 1); |
|
1257 by (assume_tac 1); |
|
1258 by (blast_tac (claset() addIs [hypreal_mult_order]) 1); |
|
1259 qed "hypreal_mult_order_trans"; |
|
1260 |
|
1261 Goal "[| 0hr < r1; r1 <= r2; 0hr <= x; x <= y |] \ |
|
1262 \ ==> r1 * x <= r2 * y"; |
|
1263 by (rtac hypreal_less_or_eq_imp_le 1); |
|
1264 by (REPEAT(dtac hypreal_le_imp_less_or_eq 1)); |
|
1265 by (auto_tac (claset() addIs [hypreal_mult_less_mono, |
|
1266 hypreal_mult_less_mono1,hypreal_mult_less_mono2, |
|
1267 hypreal_mult_order_trans,hypreal_mult_order],simpset())); |
|
1268 qed "hypreal_mult_le_mono"; |
|
1269 |
|
1270 (*---------------------------------------------------------- |
|
1271 hypreal_of_real preserves field and order properties |
|
1272 -----------------------------------------------------------*) |
|
1273 Goalw [hypreal_of_real_def] |
|
1274 "hypreal_of_real ((z1::real) + z2) = \ |
|
1275 \ hypreal_of_real z1 + hypreal_of_real z2"; |
|
1276 by (asm_simp_tac (simpset() addsimps [hypreal_add, |
|
1277 hypreal_add_mult_distrib]) 1); |
|
1278 qed "hypreal_of_real_add"; |
|
1279 |
|
1280 Goalw [hypreal_of_real_def] |
|
1281 "hypreal_of_real ((z1::real) * z2) = hypreal_of_real z1 * hypreal_of_real z2"; |
|
1282 by (full_simp_tac (simpset() addsimps [hypreal_mult, |
|
1283 hypreal_add_mult_distrib2]) 1); |
|
1284 qed "hypreal_of_real_mult"; |
|
1285 |
|
1286 Goalw [hypreal_less_def,hypreal_of_real_def] |
|
1287 "(z1 < z2) = (hypreal_of_real z1 < hypreal_of_real z2)"; |
|
1288 by Auto_tac; |
|
1289 by (res_inst_tac [("x","%n. z1")] exI 1); |
|
1290 by (Step_tac 1); |
|
1291 by (res_inst_tac [("x","%n. z2")] exI 2); |
|
1292 by Auto_tac; |
|
1293 by (rtac FreeUltrafilterNat_P 1); |
|
1294 by (Ultra_tac 1); |
|
1295 qed "hypreal_of_real_less_iff"; |
|
1296 |
|
1297 Addsimps [hypreal_of_real_less_iff RS sym]; |
|
1298 |
|
1299 Goalw [hypreal_le_def,real_le_def] |
|
1300 "(z1 <= z2) = (hypreal_of_real z1 <= hypreal_of_real z2)"; |
|
1301 by Auto_tac; |
|
1302 qed "hypreal_of_real_le_iff"; |
|
1303 |
|
1304 Goalw [hypreal_of_real_def] "hypreal_of_real (-r) = - hypreal_of_real r"; |
|
1305 by (auto_tac (claset(),simpset() addsimps [hypreal_minus])); |
|
1306 qed "hypreal_of_real_minus"; |
|
1307 |
|
1308 Goal "0hr < x ==> 0hr < hrinv x"; |
|
1309 by (EVERY1[rtac ccontr, dtac hypreal_leI]); |
|
1310 by (forward_tac [hypreal_minus_zero_less_iff2 RS iffD2] 1); |
|
1311 by (forward_tac [hypreal_not_refl2 RS not_sym] 1); |
|
1312 by (dtac (hypreal_not_refl2 RS not_sym RS hrinv_not_zero) 1); |
|
1313 by (EVERY1[dtac hypreal_le_imp_less_or_eq, Step_tac]); |
|
1314 by (dtac hypreal_mult_less_zero1 1 THEN assume_tac 1); |
|
1315 by (auto_tac (claset() addIs [hypreal_zero_less_one RS hypreal_less_asym], |
|
1316 simpset() addsimps [hypreal_minus_mult_eq1 RS sym, |
|
1317 hypreal_minus_zero_less_iff])); |
|
1318 qed "hypreal_hrinv_gt_zero"; |
|
1319 |
|
1320 Goal "x < 0hr ==> hrinv x < 0hr"; |
|
1321 by (forward_tac [hypreal_not_refl2] 1); |
|
1322 by (dtac (hypreal_minus_zero_less_iff RS iffD2) 1); |
|
1323 by (rtac (hypreal_minus_zero_less_iff RS iffD1) 1); |
|
1324 by (dtac (hypreal_minus_hrinv RS sym) 1); |
|
1325 by (auto_tac (claset() addIs [hypreal_hrinv_gt_zero], |
|
1326 simpset())); |
|
1327 qed "hypreal_hrinv_less_zero"; |
|
1328 |
|
1329 Goalw [hypreal_of_real_def,hypreal_one_def] "hypreal_of_real 1r = 1hr"; |
|
1330 by (Step_tac 1); |
|
1331 qed "hypreal_of_real_one"; |
|
1332 |
|
1333 Goalw [hypreal_of_real_def,hypreal_zero_def] "hypreal_of_real 0r = 0hr"; |
|
1334 by (Step_tac 1); |
|
1335 qed "hypreal_of_real_zero"; |
|
1336 |
|
1337 Goal "(hypreal_of_real r = 0hr) = (r = 0r)"; |
|
1338 by (auto_tac (claset() addIs [FreeUltrafilterNat_P], |
|
1339 simpset() addsimps [hypreal_of_real_def, |
|
1340 hypreal_zero_def,FreeUltrafilterNat_Nat_set])); |
|
1341 qed "hypreal_of_real_zero_iff"; |
|
1342 |
|
1343 Goal "(hypreal_of_real r ~= 0hr) = (r ~= 0r)"; |
|
1344 by (full_simp_tac (simpset() addsimps [hypreal_of_real_zero_iff]) 1); |
|
1345 qed "hypreal_of_real_not_zero_iff"; |
|
1346 |
|
1347 Goal "r ~= 0r ==> hrinv (hypreal_of_real r) = \ |
|
1348 \ hypreal_of_real (rinv r)"; |
|
1349 by (res_inst_tac [("c1","hypreal_of_real r")] (hypreal_mult_left_cancel RS iffD1) 1); |
|
1350 by (etac (hypreal_of_real_not_zero_iff RS iffD2) 1); |
|
1351 by (forward_tac [hypreal_of_real_not_zero_iff RS iffD2] 1); |
|
1352 by (auto_tac (claset(),simpset() addsimps [hypreal_of_real_mult RS sym,hypreal_of_real_one])); |
|
1353 qed "hypreal_of_real_hrinv"; |
|
1354 |
|
1355 Goal "hypreal_of_real r ~= 0hr ==> hrinv (hypreal_of_real r) = \ |
|
1356 \ hypreal_of_real (rinv r)"; |
|
1357 by (etac (hypreal_of_real_not_zero_iff RS iffD1 RS hypreal_of_real_hrinv) 1); |
|
1358 qed "hypreal_of_real_hrinv2"; |
|
1359 |
|
1360 Goal "x+x=x*(1hr+1hr)"; |
|
1361 by (simp_tac (simpset() addsimps [hypreal_add_mult_distrib2]) 1); |
|
1362 qed "hypreal_add_self"; |
|
1363 |
|
1364 Goal "1hr < 1hr + 1hr"; |
|
1365 by (rtac (hypreal_less_minus_iff RS iffD2) 1); |
|
1366 by (full_simp_tac (simpset() addsimps [hypreal_zero_less_one, |
|
1367 hypreal_add_assoc]) 1); |
|
1368 qed "hypreal_one_less_two"; |
|
1369 |
|
1370 Goal "0hr < 1hr + 1hr"; |
|
1371 by (rtac ([hypreal_zero_less_one, |
|
1372 hypreal_one_less_two] MRS hypreal_less_trans) 1); |
|
1373 qed "hypreal_zero_less_two"; |
|
1374 |
|
1375 Goal "1hr + 1hr ~= 0hr"; |
|
1376 by (rtac (hypreal_zero_less_two RS hypreal_not_refl2 RS not_sym) 1); |
|
1377 qed "hypreal_two_not_zero"; |
|
1378 Addsimps [hypreal_two_not_zero]; |
|
1379 |
|
1380 Goal "x*hrinv(1hr + 1hr) + x*hrinv(1hr + 1hr) = x"; |
|
1381 by (rtac (hypreal_add_self RS ssubst) 1); |
|
1382 by (full_simp_tac (simpset() addsimps [hypreal_mult_assoc]) 1); |
|
1383 qed "hypreal_sum_of_halves"; |
|
1384 |
|
1385 Goal "z ~= 0hr ==> x*y = (x*hrinv(z))*(z*y)"; |
|
1386 by (asm_simp_tac (simpset() addsimps hypreal_mult_ac) 1); |
|
1387 qed "lemma_chain"; |
|
1388 |
|
1389 Goal "0hr < r ==> 0hr < r*hrinv(1hr+1hr)"; |
|
1390 by (dtac (hypreal_zero_less_two RS hypreal_hrinv_gt_zero |
|
1391 RS hypreal_mult_less_mono1) 1); |
|
1392 by Auto_tac; |
|
1393 qed "hypreal_half_gt_zero"; |
|
1394 |
|
1395 (* TODO: remove redundant 0hr < x *) |
|
1396 Goal "[| 0hr < r; 0hr < x; r < x |] ==> hrinv x < hrinv r"; |
|
1397 by (forward_tac [hypreal_hrinv_gt_zero] 1); |
|
1398 by (forw_inst_tac [("x","x")] hypreal_hrinv_gt_zero 1); |
|
1399 by (forw_inst_tac [("x","r"),("z","hrinv r")] hypreal_mult_less_mono1 1); |
|
1400 by (assume_tac 1); |
|
1401 by (asm_full_simp_tac (simpset() addsimps [hypreal_not_refl2 RS |
|
1402 not_sym RS hypreal_mult_hrinv]) 1); |
|
1403 by (forward_tac [hypreal_hrinv_gt_zero] 1); |
|
1404 by (forw_inst_tac [("x","1hr"),("z","hrinv x")] hypreal_mult_less_mono2 1); |
|
1405 by (assume_tac 1); |
|
1406 by (asm_full_simp_tac (simpset() addsimps [hypreal_not_refl2 RS |
|
1407 not_sym RS hypreal_mult_hrinv_left,hypreal_mult_assoc RS sym]) 1); |
|
1408 qed "hypreal_hrinv_less_swap"; |
|
1409 |
|
1410 Goal "[| 0hr < r; 0hr < x|] ==> (r < x) = (hrinv x < hrinv r)"; |
|
1411 by (auto_tac (claset() addIs [hypreal_hrinv_less_swap],simpset())); |
|
1412 by (res_inst_tac [("t","r")] (hypreal_hrinv_hrinv RS subst) 1); |
|
1413 by (etac (hypreal_not_refl2 RS not_sym) 1); |
|
1414 by (res_inst_tac [("t","x")] (hypreal_hrinv_hrinv RS subst) 1); |
|
1415 by (etac (hypreal_not_refl2 RS not_sym) 1); |
|
1416 by (auto_tac (claset() addIs [hypreal_hrinv_less_swap], |
|
1417 simpset() addsimps [hypreal_hrinv_gt_zero])); |
|
1418 qed "hypreal_hrinv_less_iff"; |
|
1419 |
|
1420 Goal "[| 0hr < z; x < y |] ==> x*hrinv(z) < y*hrinv(z)"; |
|
1421 by (blast_tac (claset() addSIs [hypreal_mult_less_mono1, |
|
1422 hypreal_hrinv_gt_zero]) 1); |
|
1423 qed "hypreal_mult_hrinv_less_mono1"; |
|
1424 |
|
1425 Goal "[| 0hr < z; x < y |] ==> hrinv(z)*x < hrinv(z)*y"; |
|
1426 by (blast_tac (claset() addSIs [hypreal_mult_less_mono2, |
|
1427 hypreal_hrinv_gt_zero]) 1); |
|
1428 qed "hypreal_mult_hrinv_less_mono2"; |
|
1429 |
|
1430 Goal "[| 0hr < z; x*z < y*z |] ==> x < y"; |
|
1431 by (forw_inst_tac [("x","x*z")] hypreal_mult_hrinv_less_mono1 1); |
|
1432 by (dtac (hypreal_not_refl2 RS not_sym) 2); |
|
1433 by (auto_tac (claset() addSDs [hypreal_mult_hrinv], |
|
1434 simpset() addsimps hypreal_mult_ac)); |
|
1435 qed "hypreal_less_mult_right_cancel"; |
|
1436 |
|
1437 Goal "[| 0hr < z; z*x < z*y |] ==> x < y"; |
|
1438 by (auto_tac (claset() addIs [hypreal_less_mult_right_cancel], |
|
1439 simpset() addsimps [hypreal_mult_commute])); |
|
1440 qed "hypreal_less_mult_left_cancel"; |
|
1441 |
|
1442 Goal "[| 0hr < r; 0hr < ra; \ |
|
1443 \ r < x; ra < y |] \ |
|
1444 \ ==> r*ra < x*y"; |
|
1445 by (forw_inst_tac [("R2.0","r")] hypreal_less_trans 1); |
|
1446 by (dres_inst_tac [("z","ra"),("x","r")] hypreal_mult_less_mono1 2); |
|
1447 by (dres_inst_tac [("z","x"),("x","ra")] hypreal_mult_less_mono2 3); |
|
1448 by (auto_tac (claset() addIs [hypreal_less_trans],simpset())); |
|
1449 qed "hypreal_mult_less_gt_zero"; |
|
1450 |
|
1451 Goal "[| 0hr < r; 0hr < ra; \ |
|
1452 \ r <= x; ra <= y |] \ |
|
1453 \ ==> r*ra <= x*y"; |
|
1454 by (REPEAT(dtac hypreal_le_imp_less_or_eq 1)); |
|
1455 by (rtac hypreal_less_or_eq_imp_le 1); |
|
1456 by (auto_tac (claset() addIs [hypreal_mult_less_mono1, |
|
1457 hypreal_mult_less_mono2,hypreal_mult_less_gt_zero], |
|
1458 simpset())); |
|
1459 qed "hypreal_mult_le_ge_zero"; |
|
1460 |
|
1461 Goal "? (x::hypreal). x < y"; |
|
1462 by (rtac (hypreal_add_zero_right RS subst) 1); |
|
1463 by (res_inst_tac [("x","y + -1hr")] exI 1); |
|
1464 by (auto_tac (claset() addSIs [hypreal_add_less_mono2], |
|
1465 simpset() addsimps [hypreal_minus_zero_less_iff2, |
|
1466 hypreal_zero_less_one] delsimps [hypreal_add_zero_right])); |
|
1467 qed "hypreal_less_Ex"; |
|
1468 |
|
1469 Goal "!!(A::hypreal). A + C < B + C ==> A < B"; |
|
1470 by (dres_inst_tac [("C","-C")] hypreal_add_less_mono1 1); |
|
1471 by (asm_full_simp_tac (simpset() addsimps [hypreal_add_assoc]) 1); |
|
1472 qed "hypreal_less_add_right_cancel"; |
|
1473 |
|
1474 Goal "!!(A::hypreal). C + A < C + B ==> A < B"; |
|
1475 by (dres_inst_tac [("C","-C")] hypreal_add_less_mono2 1); |
|
1476 by (asm_full_simp_tac (simpset() addsimps [hypreal_add_assoc RS sym]) 1); |
|
1477 qed "hypreal_less_add_left_cancel"; |
|
1478 |
|
1479 Goal "0hr <= x*x"; |
|
1480 by (res_inst_tac [("x","0hr"),("y","x")] hypreal_linear_less2 1); |
|
1481 by (auto_tac (claset() addIs [hypreal_mult_order, |
|
1482 hypreal_mult_less_zero1,hypreal_less_imp_le], |
|
1483 simpset())); |
|
1484 qed "hypreal_le_square"; |
|
1485 Addsimps [hypreal_le_square]; |
|
1486 |
|
1487 Goalw [hypreal_le_def] "- (x*x) <= 0hr"; |
|
1488 by (auto_tac (claset() addSDs [(hypreal_le_square RS |
|
1489 hypreal_le_less_trans)],simpset() addsimps |
|
1490 [hypreal_minus_zero_less_iff,hypreal_less_not_refl])); |
|
1491 qed "hypreal_less_minus_square"; |
|
1492 Addsimps [hypreal_less_minus_square]; |
|
1493 |
|
1494 Goal "[|x ~= 0hr; y ~= 0hr |] ==> \ |
|
1495 \ hrinv(x) + hrinv(y) = (x + y)*hrinv(x*y)"; |
|
1496 by (asm_full_simp_tac (simpset() addsimps [hypreal_hrinv_distrib, |
|
1497 hypreal_add_mult_distrib,hypreal_mult_assoc RS sym]) 1); |
|
1498 by (rtac (hypreal_mult_assoc RS ssubst) 1); |
|
1499 by (rtac (hypreal_mult_left_commute RS subst) 1); |
|
1500 by (asm_full_simp_tac (simpset() addsimps [hypreal_add_commute]) 1); |
|
1501 qed "hypreal_hrinv_add"; |
|
1502 |
|
1503 Goal "x = -x ==> x = 0hr"; |
|
1504 by (dtac (hypreal_eq_minus_iff RS iffD1 RS sym) 1); |
|
1505 by (Asm_full_simp_tac 1); |
|
1506 by (dtac (hypreal_add_self RS subst) 1); |
|
1507 by (rtac ccontr 1); |
|
1508 by (blast_tac (claset() addDs [hypreal_two_not_zero RSN |
|
1509 (2,hypreal_mult_not_0)]) 1); |
|
1510 qed "hypreal_self_eq_minus_self_zero"; |
|
1511 |
|
1512 Goal "(x + x = 0hr) = (x = 0hr)"; |
|
1513 by Auto_tac; |
|
1514 by (dtac (hypreal_add_self RS subst) 1); |
|
1515 by (rtac ccontr 1 THEN rtac hypreal_mult_not_0E 1); |
|
1516 by Auto_tac; |
|
1517 qed "hypreal_add_self_zero_cancel"; |
|
1518 Addsimps [hypreal_add_self_zero_cancel]; |
|
1519 |
|
1520 Goal "(x + x + y = y) = (x = 0hr)"; |
|
1521 by Auto_tac; |
|
1522 by (dtac (hypreal_eq_minus_iff RS iffD1) 1 THEN dtac sym 1); |
|
1523 by (auto_tac (claset(),simpset() addsimps [hypreal_add_assoc])); |
|
1524 qed "hypreal_add_self_zero_cancel2"; |
|
1525 Addsimps [hypreal_add_self_zero_cancel2]; |
|
1526 |
|
1527 Goal "(x + (x + y) = y) = (x = 0hr)"; |
|
1528 by (simp_tac (simpset() addsimps [hypreal_add_assoc RS sym]) 1); |
|
1529 qed "hypreal_add_self_zero_cancel2a"; |
|
1530 Addsimps [hypreal_add_self_zero_cancel2a]; |
|
1531 |
|
1532 Goal "(b = -a) = (-b = (a::hypreal))"; |
|
1533 by Auto_tac; |
|
1534 qed "hypreal_minus_eq_swap"; |
|
1535 |
|
1536 Goal "(-b = -a) = (b = (a::hypreal))"; |
|
1537 by (asm_full_simp_tac (simpset() addsimps |
|
1538 [hypreal_minus_eq_swap]) 1); |
|
1539 qed "hypreal_minus_eq_cancel"; |
|
1540 Addsimps [hypreal_minus_eq_cancel]; |
|
1541 |
|
1542 Goal "x < x + 1hr"; |
|
1543 by (cut_inst_tac [("C","x")] |
|
1544 (hypreal_zero_less_one RS hypreal_add_less_mono2) 1); |
|
1545 by (Asm_full_simp_tac 1); |
|
1546 qed "hypreal_less_self_add_one"; |
|
1547 Addsimps [hypreal_less_self_add_one]; |
|
1548 |
|
1549 Goal "((x::hypreal) + x = y + y) = (x = y)"; |
|
1550 by (auto_tac (claset() addIs [hypreal_two_not_zero RS |
|
1551 hypreal_mult_left_cancel RS iffD1],simpset() addsimps |
|
1552 [hypreal_add_mult_distrib])); |
|
1553 qed "hypreal_add_self_cancel"; |
|
1554 Addsimps [hypreal_add_self_cancel]; |
|
1555 |
|
1556 Goal "(y = x + - y + x) = (y = (x::hypreal))"; |
|
1557 by Auto_tac; |
|
1558 by (dres_inst_tac [("x1","y")] |
|
1559 (hypreal_add_right_cancel RS iffD2) 1); |
|
1560 by (auto_tac (claset(),simpset() addsimps hypreal_add_ac)); |
|
1561 qed "hypreal_add_self_minus_cancel"; |
|
1562 Addsimps [hypreal_add_self_minus_cancel]; |
|
1563 |
|
1564 Goal "(y = x + (- y + x)) = (y = (x::hypreal))"; |
|
1565 by (asm_full_simp_tac (simpset() addsimps |
|
1566 [hypreal_add_assoc RS sym])1); |
|
1567 qed "hypreal_add_self_minus_cancel2"; |
|
1568 Addsimps [hypreal_add_self_minus_cancel2]; |
|
1569 |
|
1570 Goal "z + -x = y + (y + (-x + -z)) = (y = (z::hypreal))"; |
|
1571 by Auto_tac; |
|
1572 by (dres_inst_tac [("x1","z")] |
|
1573 (hypreal_add_right_cancel RS iffD2) 1); |
|
1574 by (asm_full_simp_tac (simpset() addsimps |
|
1575 [hypreal_minus_add_distrib RS sym] @ hypreal_add_ac) 1); |
|
1576 by (asm_full_simp_tac (simpset() addsimps |
|
1577 [hypreal_add_assoc RS sym,hypreal_add_right_cancel]) 1); |
|
1578 qed "hypreal_add_self_minus_cancel3"; |
|
1579 Addsimps [hypreal_add_self_minus_cancel3]; |
|
1580 |
|
1581 (* check why this does not work without 2nd substiution anymore! *) |
|
1582 Goal "x < y ==> x < (x + y)*hrinv(1hr + 1hr)"; |
|
1583 by (dres_inst_tac [("C","x")] hypreal_add_less_mono2 1); |
|
1584 by (dtac (hypreal_add_self RS subst) 1); |
|
1585 by (dtac (hypreal_zero_less_two RS hypreal_hrinv_gt_zero RS |
|
1586 hypreal_mult_less_mono1) 1); |
|
1587 by (auto_tac (claset() addDs [hypreal_two_not_zero RS |
|
1588 (hypreal_mult_hrinv RS subst)],simpset() |
|
1589 addsimps [hypreal_mult_assoc])); |
|
1590 qed "hypreal_less_half_sum"; |
|
1591 |
|
1592 (* check why this does not work without 2nd substiution anymore! *) |
|
1593 Goal "x < y ==> (x + y)*hrinv(1hr + 1hr) < y"; |
|
1594 by (dres_inst_tac [("C","y")] hypreal_add_less_mono1 1); |
|
1595 by (dtac (hypreal_add_self RS subst) 1); |
|
1596 by (dtac (hypreal_zero_less_two RS hypreal_hrinv_gt_zero RS |
|
1597 hypreal_mult_less_mono1) 1); |
|
1598 by (auto_tac (claset() addDs [hypreal_two_not_zero RS |
|
1599 (hypreal_mult_hrinv RS subst)],simpset() |
|
1600 addsimps [hypreal_mult_assoc])); |
|
1601 qed "hypreal_gt_half_sum"; |
|
1602 |
|
1603 Goal "!!(x::hypreal). x < y ==> EX r. x < r & r < y"; |
|
1604 by (blast_tac (claset() addSIs [hypreal_less_half_sum, |
|
1605 hypreal_gt_half_sum]) 1); |
|
1606 qed "hypreal_dense"; |
|
1607 |
|
1608 Goal "(x * x = 0hr) = (x = 0hr)"; |
|
1609 by Auto_tac; |
|
1610 by (blast_tac (claset() addIs [hypreal_mult_not_0E]) 1); |
|
1611 qed "hypreal_mult_self_eq_zero_iff"; |
|
1612 Addsimps [hypreal_mult_self_eq_zero_iff]; |
|
1613 |
|
1614 Goal "(0hr = x * x) = (x = 0hr)"; |
|
1615 by (auto_tac (claset() addDs [sym],simpset())); |
|
1616 qed "hypreal_mult_self_eq_zero_iff2"; |
|
1617 Addsimps [hypreal_mult_self_eq_zero_iff2]; |
|
1618 |
|
1619 Goal "(x*x + y*y = 0hr) = (x = 0hr & y = 0hr)"; |
|
1620 by Auto_tac; |
|
1621 by (dtac (sym RS (hypreal_eq_minus_iff3 RS iffD1)) 1); |
|
1622 by (dtac (sym RS (hypreal_eq_minus_iff4 RS iffD1)) 2); |
|
1623 by (ALLGOALS(rtac ccontr)); |
|
1624 by (ALLGOALS(dtac hypreal_mult_self_not_zero)); |
|
1625 by (cut_inst_tac [("x1","x")] (hypreal_le_square |
|
1626 RS hypreal_le_imp_less_or_eq) 1); |
|
1627 by (cut_inst_tac [("x1","y")] (hypreal_le_square |
|
1628 RS hypreal_le_imp_less_or_eq) 2); |
|
1629 by (auto_tac (claset() addDs [sym],simpset())); |
|
1630 by (dres_inst_tac [("x1","y")] (hypreal_less_minus_square |
|
1631 RS hypreal_le_less_trans) 1); |
|
1632 by (dres_inst_tac [("x1","x")] (hypreal_less_minus_square |
|
1633 RS hypreal_le_less_trans) 2); |
|
1634 by (auto_tac (claset(),simpset() addsimps |
|
1635 [hypreal_less_not_refl])); |
|
1636 qed "hypreal_squares_add_zero_iff"; |
|
1637 Addsimps [hypreal_squares_add_zero_iff]; |
|
1638 |
|
1639 Goal "x * x ~= 0hr ==> 0hr < x* x + y*y + z*z"; |
|
1640 by (cut_inst_tac [("x1","x")] (hypreal_le_square |
|
1641 RS hypreal_le_imp_less_or_eq) 1); |
|
1642 by (auto_tac (claset() addSIs |
|
1643 [hypreal_add_order_le],simpset())); |
|
1644 qed "hypreal_sum_squares3_gt_zero"; |
|
1645 |
|
1646 Goal "x * x ~= 0hr ==> 0hr < y*y + x*x + z*z"; |
|
1647 by (dtac hypreal_sum_squares3_gt_zero 1); |
|
1648 by (auto_tac (claset(),simpset() addsimps hypreal_add_ac)); |
|
1649 qed "hypreal_sum_squares3_gt_zero2"; |
|
1650 |
|
1651 Goal "x * x ~= 0hr ==> 0hr < y*y + z*z + x*x"; |
|
1652 by (dtac hypreal_sum_squares3_gt_zero 1); |
|
1653 by (auto_tac (claset(),simpset() addsimps hypreal_add_ac)); |
|
1654 qed "hypreal_sum_squares3_gt_zero3"; |
|
1655 |
|
1656 Goal "(x*x + y*y + z*z = 0hr) = \ |
|
1657 \ (x = 0hr & y = 0hr & z = 0hr)"; |
|
1658 by Auto_tac; |
|
1659 by (ALLGOALS(rtac ccontr)); |
|
1660 by (ALLGOALS(dtac hypreal_mult_self_not_zero)); |
|
1661 by (auto_tac (claset() addDs [hypreal_not_refl2 RS not_sym, |
|
1662 hypreal_sum_squares3_gt_zero3,hypreal_sum_squares3_gt_zero, |
|
1663 hypreal_sum_squares3_gt_zero2],simpset() delsimps |
|
1664 [hypreal_mult_self_eq_zero_iff])); |
|
1665 qed "hypreal_three_squares_add_zero_iff"; |
|
1666 Addsimps [hypreal_three_squares_add_zero_iff]; |
|
1667 |
|
1668 Goal "(x::hypreal)*x <= x*x + y*y"; |
|
1669 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); |
|
1670 by (res_inst_tac [("z","y")] eq_Abs_hypreal 1); |
|
1671 by (auto_tac (claset(),simpset() addsimps |
|
1672 [hypreal_mult,hypreal_add,hypreal_le])); |
|
1673 qed "hypreal_self_le_add_pos"; |
|
1674 Addsimps [hypreal_self_le_add_pos]; |
|
1675 |
|
1676 Goal "(x::hypreal)*x <= x*x + y*y + z*z"; |
|
1677 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); |
|
1678 by (res_inst_tac [("z","y")] eq_Abs_hypreal 1); |
|
1679 by (res_inst_tac [("z","z")] eq_Abs_hypreal 1); |
|
1680 by (auto_tac (claset(),simpset() addsimps |
|
1681 [hypreal_mult,hypreal_add,hypreal_le, |
|
1682 real_le_add_order])); |
|
1683 qed "hypreal_self_le_add_pos2"; |
|
1684 Addsimps [hypreal_self_le_add_pos2]; |
|
1685 |
|
1686 (*--------------------------------------------------------------------------------- |
|
1687 Embedding of the naturals in the hyperreals |
|
1688 ---------------------------------------------------------------------------------*) |
|
1689 Goalw [hypreal_of_posnat_def] "hypreal_of_posnat 0 = 1hr"; |
|
1690 by (full_simp_tac (simpset() addsimps |
|
1691 [pnat_one_iff RS sym,real_of_preal_def]) 1); |
|
1692 by (fold_tac [real_one_def]); |
|
1693 by (rtac hypreal_of_real_one 1); |
|
1694 qed "hypreal_of_posnat_one"; |
|
1695 |
|
1696 Goalw [hypreal_of_posnat_def] "hypreal_of_posnat 1 = 1hr + 1hr"; |
|
1697 by (full_simp_tac (simpset() addsimps [real_of_preal_def,real_one_def, |
|
1698 hypreal_one_def,hypreal_add,hypreal_of_real_def,pnat_two_eq, |
|
1699 real_add,prat_of_pnat_add RS sym,preal_of_prat_add RS sym] @ pnat_add_ac) 1); |
|
1700 qed "hypreal_of_posnat_two"; |
|
1701 |
|
1702 Goalw [hypreal_of_posnat_def] |
|
1703 "hypreal_of_posnat n1 + hypreal_of_posnat n2 = \ |
|
1704 \ hypreal_of_posnat (n1 + n2) + 1hr"; |
|
1705 by (full_simp_tac (simpset() addsimps [hypreal_of_posnat_one RS sym, |
|
1706 hypreal_of_real_add RS sym,hypreal_of_posnat_def,real_of_preal_add RS sym, |
|
1707 preal_of_prat_add RS sym,prat_of_pnat_add RS sym,pnat_of_nat_add]) 1); |
|
1708 qed "hypreal_of_posnat_add"; |
|
1709 |
|
1710 Goal "hypreal_of_posnat (n + 1) = hypreal_of_posnat n + 1hr"; |
|
1711 by (res_inst_tac [("x1","1hr")] (hypreal_add_right_cancel RS iffD1) 1); |
|
1712 by (rtac (hypreal_of_posnat_add RS subst) 1); |
|
1713 by (full_simp_tac (simpset() addsimps [hypreal_of_posnat_two,hypreal_add_assoc]) 1); |
|
1714 qed "hypreal_of_posnat_add_one"; |
|
1715 |
|
1716 Goalw [real_of_posnat_def,hypreal_of_posnat_def] |
|
1717 "hypreal_of_posnat n = hypreal_of_real (real_of_posnat n)"; |
|
1718 by (rtac refl 1); |
|
1719 qed "hypreal_of_real_of_posnat"; |
|
1720 |
|
1721 Goalw [hypreal_of_posnat_def] |
|
1722 "(n < m) = (hypreal_of_posnat n < hypreal_of_posnat m)"; |
|
1723 by Auto_tac; |
|
1724 qed "hypreal_of_posnat_less_iff"; |
|
1725 |
|
1726 Addsimps [hypreal_of_posnat_less_iff RS sym]; |
|
1727 (*--------------------------------------------------------------------------------- |
|
1728 Existence of infinite hyperreal number |
|
1729 ---------------------------------------------------------------------------------*) |
|
1730 |
|
1731 Goal "hyprel^^{%n::nat. real_of_posnat n} : hypreal"; |
|
1732 by Auto_tac; |
|
1733 qed "hypreal_omega"; |
|
1734 |
|
1735 Goalw [omega_def] "Rep_hypreal(whr) : hypreal"; |
|
1736 by (rtac Rep_hypreal 1); |
|
1737 qed "Rep_hypreal_omega"; |
|
1738 |
|
1739 (* existence of infinite number not corresponding to any real number *) |
|
1740 (* use assumption that member FreeUltrafilterNat is not finite *) |
|
1741 (* a few lemmas first *) |
|
1742 |
|
1743 Goal "{n::nat. x = real_of_posnat n} = {} | \ |
|
1744 \ (? y. {n::nat. x = real_of_posnat n} = {y})"; |
|
1745 by (auto_tac (claset() addDs [inj_real_of_posnat RS injD],simpset())); |
|
1746 qed "lemma_omega_empty_singleton_disj"; |
|
1747 |
|
1748 Goal "finite {n::nat. x = real_of_posnat n}"; |
|
1749 by (cut_inst_tac [("x","x")] lemma_omega_empty_singleton_disj 1); |
|
1750 by Auto_tac; |
|
1751 qed "lemma_finite_omega_set"; |
|
1752 |
|
1753 Goalw [omega_def,hypreal_of_real_def] |
|
1754 "~ (? x. hypreal_of_real x = whr)"; |
|
1755 by (auto_tac (claset(),simpset() addsimps [lemma_finite_omega_set |
|
1756 RS FreeUltrafilterNat_finite])); |
|
1757 qed "not_ex_hypreal_of_real_eq_omega"; |
|
1758 |
|
1759 Goal "hypreal_of_real x ~= whr"; |
|
1760 by (cut_facts_tac [not_ex_hypreal_of_real_eq_omega] 1); |
|
1761 by Auto_tac; |
|
1762 qed "hypreal_of_real_not_eq_omega"; |
|
1763 |
|
1764 (* existence of infinitesimal number also not *) |
|
1765 (* corresponding to any real number *) |
|
1766 |
|
1767 Goal "{n::nat. x = rinv(real_of_posnat n)} = {} | \ |
|
1768 \ (? y. {n::nat. x = rinv(real_of_posnat n)} = {y})"; |
|
1769 by (Step_tac 1 THEN Step_tac 1); |
|
1770 by (auto_tac (claset() addIs [real_of_posnat_rinv_inj],simpset())); |
|
1771 qed "lemma_epsilon_empty_singleton_disj"; |
|
1772 |
|
1773 Goal "finite {n::nat. x = rinv(real_of_posnat n)}"; |
|
1774 by (cut_inst_tac [("x","x")] lemma_epsilon_empty_singleton_disj 1); |
|
1775 by Auto_tac; |
|
1776 qed "lemma_finite_epsilon_set"; |
|
1777 |
|
1778 Goalw [epsilon_def,hypreal_of_real_def] |
|
1779 "~ (? x. hypreal_of_real x = ehr)"; |
|
1780 by (auto_tac (claset(),simpset() addsimps [lemma_finite_epsilon_set |
|
1781 RS FreeUltrafilterNat_finite])); |
|
1782 qed "not_ex_hypreal_of_real_eq_epsilon"; |
|
1783 |
|
1784 Goal "hypreal_of_real x ~= ehr"; |
|
1785 by (cut_facts_tac [not_ex_hypreal_of_real_eq_epsilon] 1); |
|
1786 by Auto_tac; |
|
1787 qed "hypreal_of_real_not_eq_epsilon"; |
|
1788 |
|
1789 Goalw [epsilon_def,hypreal_zero_def] "ehr ~= 0hr"; |
|
1790 by (auto_tac (claset(),simpset() addsimps |
|
1791 [real_of_posnat_rinv_not_zero])); |
|
1792 qed "hypreal_epsilon_not_zero"; |
|
1793 |
|
1794 Goalw [omega_def,hypreal_zero_def] "whr ~= 0hr"; |
|
1795 by (Simp_tac 1); |
|
1796 qed "hypreal_omega_not_zero"; |
|
1797 |
|
1798 Goal "ehr = hrinv(whr)"; |
|
1799 by (asm_full_simp_tac (simpset() addsimps |
|
1800 [hypreal_hrinv,omega_def,epsilon_def] |
|
1801 setloop (split_tac [expand_if])) 1); |
|
1802 qed "hypreal_epsilon_hrinv_omega"; |
|
1803 |
|
1804 (*---------------------------------------------------------------- |
|
1805 Another embedding of the naturals in the |
|
1806 hyperreals (see hypreal_of_posnat) |
|
1807 ----------------------------------------------------------------*) |
|
1808 Goalw [hypreal_of_nat_def] "hypreal_of_nat 0 = 0hr"; |
|
1809 by (full_simp_tac (simpset() addsimps [hypreal_of_posnat_one]) 1); |
|
1810 qed "hypreal_of_nat_zero"; |
|
1811 |
|
1812 Goalw [hypreal_of_nat_def] "hypreal_of_nat 1 = 1hr"; |
|
1813 by (full_simp_tac (simpset() addsimps [hypreal_of_posnat_two, |
|
1814 hypreal_add_assoc]) 1); |
|
1815 qed "hypreal_of_nat_one"; |
|
1816 |
|
1817 Goalw [hypreal_of_nat_def] |
|
1818 "hypreal_of_nat n1 + hypreal_of_nat n2 = \ |
|
1819 \ hypreal_of_nat (n1 + n2)"; |
|
1820 by (full_simp_tac (simpset() addsimps hypreal_add_ac) 1); |
|
1821 by (simp_tac (simpset() addsimps [hypreal_of_posnat_add, |
|
1822 hypreal_add_assoc RS sym]) 1); |
|
1823 by (rtac (hypreal_add_commute RS subst) 1); |
|
1824 by (simp_tac (simpset() addsimps [hypreal_add_left_cancel, |
|
1825 hypreal_add_assoc]) 1); |
|
1826 qed "hypreal_of_nat_add"; |
|
1827 |
|
1828 Goal "hypreal_of_nat 2 = 1hr + 1hr"; |
|
1829 by (simp_tac (simpset() addsimps [hypreal_of_nat_one |
|
1830 RS sym,hypreal_of_nat_add]) 1); |
|
1831 qed "hypreal_of_nat_two"; |
|
1832 |
|
1833 Goalw [hypreal_of_nat_def] |
|
1834 "(n < m) = (hypreal_of_nat n < hypreal_of_nat m)"; |
|
1835 by (auto_tac (claset() addIs [hypreal_add_less_mono1],simpset())); |
|
1836 by (dres_inst_tac [("C","1hr")] hypreal_add_less_mono1 1); |
|
1837 by (full_simp_tac (simpset() addsimps [hypreal_add_assoc]) 1); |
|
1838 qed "hypreal_of_nat_less_iff"; |
|
1839 Addsimps [hypreal_of_nat_less_iff RS sym]; |
|
1840 |
|
1841 (* naturals embedded in hyperreals is an hyperreal *) |
|
1842 Goalw [hypreal_of_nat_def,real_of_nat_def] |
|
1843 "hypreal_of_nat m = Abs_hypreal(hyprel^^{%n. real_of_nat m})"; |
|
1844 by (auto_tac (claset(),simpset() addsimps [hypreal_of_real_def, |
|
1845 hypreal_of_real_of_posnat,hypreal_minus,hypreal_one_def,hypreal_add])); |
|
1846 qed "hypreal_of_nat_iff"; |
|
1847 |
|
1848 Goal "inj hypreal_of_nat"; |
|
1849 by (rtac injI 1); |
|
1850 by (auto_tac (claset() addSDs [FreeUltrafilterNat_P], |
|
1851 simpset() addsimps [hypreal_of_nat_iff, |
|
1852 real_add_right_cancel,inj_real_of_nat RS injD])); |
|
1853 qed "inj_hypreal_of_nat"; |
|
1854 |
|
1855 Goalw [hypreal_of_nat_def,hypreal_of_real_def,hypreal_of_posnat_def, |
|
1856 real_of_posnat_def,hypreal_one_def,real_of_nat_def] |
|
1857 "hypreal_of_nat n = hypreal_of_real (real_of_nat n)"; |
|
1858 by (simp_tac (simpset() addsimps [hypreal_add,hypreal_minus]) 1); |
|
1859 qed "hypreal_of_nat_real_of_nat"; |
|
1860 |
|
1861 |
|
1862 |
|
1863 |
|
1864 |
|
1865 |
|
1866 |
|
1867 |
|
1868 |
|
1869 |
|
1870 |
|
1871 |
|
1872 |
|
1873 |
|
1874 |
|
1875 |
|
1876 |
|
1877 |
|
1878 |
|
1879 |
|
1880 |
|
1881 |
|
1882 |
|
1883 |
|
1884 |
|
1885 |
|
1886 |
|
1887 |
|
1888 |
|
1889 |
|
1890 |
|
1891 |
|
1892 |
|
1893 |
|
1894 |
|
1895 |
|
1896 |
|
1897 |
|
1898 |
|
1899 |
|
1900 |
|
1901 |
|
1902 |
|
1903 |
|
1904 |
|
1905 |
|
1906 |
|
1907 |
|
1908 |
|
1909 |
|
1910 |
|
1911 |
|
1912 |
|
1913 |
|
1914 |
|
1915 |
|
1916 |
|
1917 |
|
1918 |
|
1919 |
|
1920 |
|
1921 |
|
1922 |
|
1923 |
|
1924 |
|
1925 |
|
1926 |
|
1927 |
|
1928 |
|
1929 |
|
1930 |
|
1931 |
|
1932 |
|
1933 |
|
1934 |
|
1935 |
|
1936 |
|
1937 |
|
1938 |
|
1939 |
|
1940 |
|
1941 |
|
1942 |
|
1943 |
|
1944 |
|
1945 |
|
1946 |
|
1947 |
|
1948 |
|
1949 |
|
1950 |
|
1951 |
|
1952 |
|
1953 |
|
1954 |
|
1955 |
|
1956 |
|
1957 |
|
1958 |
|
1959 |
|
1960 |
|
1961 |
|
1962 |
|
1963 |
|
1964 |
|
1965 |
|
1966 |
|
1967 |
|
1968 |
|
1969 |
|
1970 |
|
1971 |
|
1972 |
|
1973 |
|
1974 |
|
1975 |
|
1976 |
|
1977 |
|
1978 |
|
1979 |
|
1980 |
|
1981 |
|
1982 |
|
1983 |
|
1984 |
|
1985 |
|
1986 |
|
1987 |
|
1988 |
|
1989 |
|
1990 |
|
1991 |
|
1992 |
|
1993 |
|
1994 |
|
1995 |
|
1996 |
|
1997 |
|
1998 |
|
1999 |
|
2000 |
|
2001 |
|
2002 |
|
2003 |
|
2004 |
|
2005 |
|
2006 |
|
2007 |
|
2008 |
|
2009 |
|
2010 |
|
2011 |
|
2012 |
|
2013 |
|
2014 |
|
2015 |
|
2016 |
|
2017 |
|
2018 |
|
2019 |
|
2020 |
|
2021 |
|
2022 |
|
2023 |
|
2024 |
|
2025 |
|
2026 |
|
2027 |
|
2028 |
|
2029 |
|
2030 |
|
2031 |
|
2032 |
|
2033 |
|
2034 |
|
2035 |
|
2036 |
|
2037 |
|
2038 |
|
2039 |
|
2040 |
|
2041 |
|
2042 |
|
2043 |
|
2044 |
|
2045 |
|
2046 |
|
2047 |
|
2048 |
|
2049 |
|
2050 |
|
2051 |
|
2052 |
|
2053 |
|
2054 |
|
2055 |
|
2056 |
|
2057 |
|
2058 |
|
2059 |
|
2060 |
|
2061 |
|
2062 |
|
2063 |
|
2064 |
|
2065 |
|
2066 |
|
2067 |
|
2068 |
|
2069 |
|
2070 |
|
2071 |
|
2072 |
|
2073 |
|
2074 |
|
2075 |
|
2076 |
|
2077 |
|
2078 |
|
2079 |
|
2080 |
|
2081 |
|
2082 |
|
2083 |
|
2084 |
|
2085 |
|
2086 |
|
2087 |
|
2088 |
|
2089 |
|
2090 |
|
2091 |
|
2092 |
|
2093 |
|
2094 |
|
2095 |
|
2096 |
|
2097 |
|
2098 |
|
2099 |
|
2100 |
|
2101 |
|
2102 |
|
2103 |
|
2104 |
|
2105 |
|
2106 |
|
2107 |
|
2108 |
|
2109 |
|
2110 |
|
2111 |
|
2112 |
|
2113 |
|
2114 |
|
2115 |
|
2116 |
|
2117 |
|
2118 |
|
2119 |
|
2120 |
|
2121 |
|
2122 |
|
2123 |
|
2124 |
|
2125 |
|
2126 |
|
2127 |
|
2128 |
|
2129 |
|
2130 |
|
2131 |
|
2132 |
|
2133 |
|
2134 |
|
2135 |
|
2136 |
|
2137 |
|
2138 |
|
2139 |
|
2140 |
|
2141 |
|
2142 |
|
2143 |
|
2144 |
|
2145 |
|
2146 |
|
2147 |
|
2148 |
|
2149 |
|
2150 |
|
2151 |
|
2152 |
|
2153 |
|
2154 |
|
2155 |
|
2156 |
|
2157 |
|
2158 |
|
2159 |
|
2160 |
|
2161 |
|
2162 |
|
2163 |
|
2164 |
|
2165 |
|
2166 |
|
2167 |
|
2168 |
|
2169 |
|
2170 |
|
2171 |
|
2172 |
|
2173 |
|
2174 |
|
2175 |
|
2176 |
|
2177 |
|
2178 |
|
2179 |
|
2180 |
|
2181 |
|
2182 |
|
2183 |
|
2184 |
|
2185 |
|
2186 |
|
2187 |
|
2188 |
|
2189 |
|
2190 |
|
2191 |
|
2192 |
|
2193 |
|
2194 |
|
2195 |
|
2196 |
|
2197 |
|
2198 |
|
2199 |
|
2200 |
|
2201 |
|
2202 |
|
2203 |
|
2204 |
|
2205 |
|
2206 |
|
2207 |
|
2208 |
|
2209 |
|
2210 |
|
2211 |
|
2212 |
|
2213 |
|
2214 |
|
2215 |
|
2216 |
|
2217 |
|
2218 |
|
2219 |
|
2220 |
|
2221 |
|
2222 |
|
2223 |
|
2224 |
|
2225 |
|
2226 |
|
2227 |