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) --> (EX n. ALL 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) --> (EX 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 someI2 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 someI2 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 someI2 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 "UNIV : FreeUltrafilterNat"; |
|
111 by Auto_tac; |
|
112 qed "FreeUltrafilterNat_Nat_set"; |
|
113 Addsimps [FreeUltrafilterNat_Nat_set]; |
|
114 |
|
115 Goal "{n. P(n) = P(n)} : FreeUltrafilterNat"; |
|
116 by (Simp_tac 1); |
|
117 qed "FreeUltrafilterNat_Nat_set_refl"; |
|
118 AddIs [FreeUltrafilterNat_Nat_set_refl]; |
|
119 |
|
120 Goal "{n::nat. P} : FreeUltrafilterNat ==> P"; |
|
121 by (rtac ccontr 1); |
|
122 by (rotate_tac 1 1); |
|
123 by (Asm_full_simp_tac 1); |
|
124 qed "FreeUltrafilterNat_P"; |
|
125 |
|
126 Goal "{n. P(n)} : FreeUltrafilterNat ==> EX n. P(n)"; |
|
127 by (rtac ccontr 1 THEN rotate_tac 1 1); |
|
128 by (Asm_full_simp_tac 1); |
|
129 qed "FreeUltrafilterNat_Ex_P"; |
|
130 |
|
131 Goal "ALL n. P(n) ==> {n. P(n)} : FreeUltrafilterNat"; |
|
132 by (auto_tac (claset() addIs [FreeUltrafilterNat_Nat_set], simpset())); |
|
133 qed "FreeUltrafilterNat_all"; |
|
134 |
|
135 (*------------------------------------------------------- |
|
136 Define and use Ultrafilter tactics |
|
137 -------------------------------------------------------*) |
|
138 use "fuf.ML"; |
|
139 |
|
140 (*------------------------------------------------------- |
|
141 Now prove one further property of our free ultrafilter |
|
142 -------------------------------------------------------*) |
|
143 Goal "X Un Y: FreeUltrafilterNat \ |
|
144 \ ==> X: FreeUltrafilterNat | Y: FreeUltrafilterNat"; |
|
145 by Auto_tac; |
|
146 by (Ultra_tac 1); |
|
147 qed "FreeUltrafilterNat_Un"; |
|
148 |
|
149 (*------------------------------------------------------- |
|
150 Properties of hyprel |
|
151 -------------------------------------------------------*) |
|
152 |
|
153 (** Proving that hyprel is an equivalence relation **) |
|
154 (** Natural deduction for hyprel **) |
|
155 |
|
156 Goalw [hyprel_def] |
|
157 "((X,Y): hyprel) = ({n. X n = Y n}: FreeUltrafilterNat)"; |
|
158 by (Fast_tac 1); |
|
159 qed "hyprel_iff"; |
|
160 |
|
161 Goalw [hyprel_def] |
|
162 "{n. X n = Y n}: FreeUltrafilterNat ==> (X,Y): hyprel"; |
|
163 by (Fast_tac 1); |
|
164 qed "hyprelI"; |
|
165 |
|
166 Goalw [hyprel_def] |
|
167 "p: hyprel --> (EX X Y. \ |
|
168 \ p = (X,Y) & {n. X n = Y n} : FreeUltrafilterNat)"; |
|
169 by (Fast_tac 1); |
|
170 qed "hyprelE_lemma"; |
|
171 |
|
172 val [major,minor] = goal (the_context ()) |
|
173 "[| p: hyprel; \ |
|
174 \ !!X Y. [| p = (X,Y); {n. X n = Y n}: FreeUltrafilterNat\ |
|
175 \ |] ==> Q |] ==> Q"; |
|
176 by (cut_facts_tac [major RS (hyprelE_lemma RS mp)] 1); |
|
177 by (REPEAT (eresolve_tac [asm_rl,exE,conjE,minor] 1)); |
|
178 qed "hyprelE"; |
|
179 |
|
180 AddSIs [hyprelI]; |
|
181 AddSEs [hyprelE]; |
|
182 |
|
183 Goalw [hyprel_def] "(x,x): hyprel"; |
|
184 by (auto_tac (claset(), |
|
185 simpset() addsimps [FreeUltrafilterNat_Nat_set])); |
|
186 qed "hyprel_refl"; |
|
187 |
|
188 Goal "{n. X n = Y n} = {n. Y n = X n}"; |
|
189 by Auto_tac; |
|
190 qed "lemma_perm"; |
|
191 |
|
192 Goalw [hyprel_def] "(x,y): hyprel --> (y,x):hyprel"; |
|
193 by (auto_tac (claset() addIs [lemma_perm RS subst], simpset())); |
|
194 qed_spec_mp "hyprel_sym"; |
|
195 |
|
196 Goalw [hyprel_def] |
|
197 "(x,y): hyprel --> (y,z):hyprel --> (x,z):hyprel"; |
|
198 by Auto_tac; |
|
199 by (Ultra_tac 1); |
|
200 qed_spec_mp "hyprel_trans"; |
|
201 |
|
202 Goalw [equiv_def, refl_def, sym_def, trans_def] "equiv UNIV hyprel"; |
|
203 by (auto_tac (claset() addSIs [hyprel_refl] |
|
204 addSEs [hyprel_sym,hyprel_trans] |
|
205 delrules [hyprelI,hyprelE], |
|
206 simpset() addsimps [FreeUltrafilterNat_Nat_set])); |
|
207 qed "equiv_hyprel"; |
|
208 |
|
209 (* (hyprel ^^ {x} = hyprel ^^ {y}) = ((x,y) : hyprel) *) |
|
210 bind_thm ("equiv_hyprel_iff", |
|
211 [equiv_hyprel, UNIV_I, UNIV_I] MRS eq_equiv_class_iff); |
|
212 |
|
213 Goalw [hypreal_def,hyprel_def,quotient_def] "hyprel^^{x}:hypreal"; |
|
214 by (Blast_tac 1); |
|
215 qed "hyprel_in_hypreal"; |
|
216 |
|
217 Goal "inj_on Abs_hypreal hypreal"; |
|
218 by (rtac inj_on_inverseI 1); |
|
219 by (etac Abs_hypreal_inverse 1); |
|
220 qed "inj_on_Abs_hypreal"; |
|
221 |
|
222 Addsimps [equiv_hyprel_iff,inj_on_Abs_hypreal RS inj_on_iff, |
|
223 hyprel_iff, hyprel_in_hypreal, Abs_hypreal_inverse]; |
|
224 |
|
225 Addsimps [equiv_hyprel RS eq_equiv_class_iff]; |
|
226 bind_thm ("eq_hyprelD", equiv_hyprel RSN (2,eq_equiv_class)); |
|
227 |
|
228 Goal "inj(Rep_hypreal)"; |
|
229 by (rtac inj_inverseI 1); |
|
230 by (rtac Rep_hypreal_inverse 1); |
|
231 qed "inj_Rep_hypreal"; |
|
232 |
|
233 Goalw [hyprel_def] "x: hyprel ^^ {x}"; |
|
234 by (Step_tac 1); |
|
235 by (auto_tac (claset() addSIs [FreeUltrafilterNat_Nat_set], simpset())); |
|
236 qed "lemma_hyprel_refl"; |
|
237 |
|
238 Addsimps [lemma_hyprel_refl]; |
|
239 |
|
240 Goalw [hypreal_def] "{} ~: hypreal"; |
|
241 by (auto_tac (claset() addSEs [quotientE], simpset())); |
|
242 qed "hypreal_empty_not_mem"; |
|
243 |
|
244 Addsimps [hypreal_empty_not_mem]; |
|
245 |
|
246 Goal "Rep_hypreal x ~= {}"; |
|
247 by (cut_inst_tac [("x","x")] Rep_hypreal 1); |
|
248 by Auto_tac; |
|
249 qed "Rep_hypreal_nonempty"; |
|
250 |
|
251 Addsimps [Rep_hypreal_nonempty]; |
|
252 |
|
253 (*------------------------------------------------------------------------ |
|
254 hypreal_of_real: the injection from real to hypreal |
|
255 ------------------------------------------------------------------------*) |
|
256 |
|
257 Goal "inj(hypreal_of_real)"; |
|
258 by (rtac injI 1); |
|
259 by (rewtac hypreal_of_real_def); |
|
260 by (dtac (inj_on_Abs_hypreal RS inj_onD) 1); |
|
261 by (REPEAT (rtac hyprel_in_hypreal 1)); |
|
262 by (dtac eq_equiv_class 1); |
|
263 by (rtac equiv_hyprel 1); |
|
264 by (Fast_tac 1); |
|
265 by (rtac ccontr 1 THEN rotate_tac 1 1); |
|
266 by Auto_tac; |
|
267 qed "inj_hypreal_of_real"; |
|
268 |
|
269 val [prem] = goal (the_context ()) |
|
270 "(!!x y. z = Abs_hypreal(hyprel^^{x}) ==> P) ==> P"; |
|
271 by (res_inst_tac [("x1","z")] |
|
272 (rewrite_rule [hypreal_def] Rep_hypreal RS quotientE) 1); |
|
273 by (dres_inst_tac [("f","Abs_hypreal")] arg_cong 1); |
|
274 by (res_inst_tac [("x","x")] prem 1); |
|
275 by (asm_full_simp_tac (simpset() addsimps [Rep_hypreal_inverse]) 1); |
|
276 qed "eq_Abs_hypreal"; |
|
277 |
|
278 (**** hypreal_minus: additive inverse on hypreal ****) |
|
279 |
|
280 Goalw [congruent_def] |
|
281 "congruent hyprel (%X. hyprel^^{%n. - (X n)})"; |
|
282 by Safe_tac; |
|
283 by (ALLGOALS Ultra_tac); |
|
284 qed "hypreal_minus_congruent"; |
|
285 |
|
286 Goalw [hypreal_minus_def] |
|
287 "- (Abs_hypreal(hyprel^^{%n. X n})) = Abs_hypreal(hyprel ^^ {%n. -(X n)})"; |
|
288 by (res_inst_tac [("f","Abs_hypreal")] arg_cong 1); |
|
289 by (simp_tac (simpset() addsimps |
|
290 [hyprel_in_hypreal RS Abs_hypreal_inverse, |
|
291 [equiv_hyprel, hypreal_minus_congruent] MRS UN_equiv_class]) 1); |
|
292 qed "hypreal_minus"; |
|
293 |
|
294 Goal "- (- z) = (z::hypreal)"; |
|
295 by (res_inst_tac [("z","z")] eq_Abs_hypreal 1); |
|
296 by (asm_simp_tac (simpset() addsimps [hypreal_minus]) 1); |
|
297 qed "hypreal_minus_minus"; |
|
298 |
|
299 Addsimps [hypreal_minus_minus]; |
|
300 |
|
301 Goal "inj(%r::hypreal. -r)"; |
|
302 by (rtac injI 1); |
|
303 by (dres_inst_tac [("f","uminus")] arg_cong 1); |
|
304 by (asm_full_simp_tac (simpset() addsimps [hypreal_minus_minus]) 1); |
|
305 qed "inj_hypreal_minus"; |
|
306 |
|
307 Goalw [hypreal_zero_def] "-0 = (0::hypreal)"; |
|
308 by (simp_tac (simpset() addsimps [hypreal_minus]) 1); |
|
309 qed "hypreal_minus_zero"; |
|
310 Addsimps [hypreal_minus_zero]; |
|
311 |
|
312 Goal "(-x = 0) = (x = (0::hypreal))"; |
|
313 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); |
|
314 by (auto_tac (claset(), |
|
315 simpset() addsimps [hypreal_zero_def, hypreal_minus, eq_commute] @ |
|
316 real_add_ac)); |
|
317 qed "hypreal_minus_zero_iff"; |
|
318 |
|
319 Addsimps [hypreal_minus_zero_iff]; |
|
320 |
|
321 |
|
322 (**** hyperreal addition: hypreal_add ****) |
|
323 |
|
324 Goalw [congruent2_def] |
|
325 "congruent2 hyprel (%X Y. hyprel^^{%n. X n + Y n})"; |
|
326 by Safe_tac; |
|
327 by (ALLGOALS(Ultra_tac)); |
|
328 qed "hypreal_add_congruent2"; |
|
329 |
|
330 Goalw [hypreal_add_def] |
|
331 "Abs_hypreal(hyprel^^{%n. X n}) + Abs_hypreal(hyprel^^{%n. Y n}) = \ |
|
332 \ Abs_hypreal(hyprel^^{%n. X n + Y n})"; |
|
333 by (simp_tac (simpset() addsimps |
|
334 [[equiv_hyprel, hypreal_add_congruent2] MRS UN_equiv_class2]) 1); |
|
335 qed "hypreal_add"; |
|
336 |
|
337 Goal "(z::hypreal) + w = w + z"; |
|
338 by (res_inst_tac [("z","z")] eq_Abs_hypreal 1); |
|
339 by (res_inst_tac [("z","w")] eq_Abs_hypreal 1); |
|
340 by (asm_simp_tac (simpset() addsimps (real_add_ac @ [hypreal_add])) 1); |
|
341 qed "hypreal_add_commute"; |
|
342 |
|
343 Goal "((z1::hypreal) + z2) + z3 = z1 + (z2 + z3)"; |
|
344 by (res_inst_tac [("z","z1")] eq_Abs_hypreal 1); |
|
345 by (res_inst_tac [("z","z2")] eq_Abs_hypreal 1); |
|
346 by (res_inst_tac [("z","z3")] eq_Abs_hypreal 1); |
|
347 by (asm_simp_tac (simpset() addsimps [hypreal_add, real_add_assoc]) 1); |
|
348 qed "hypreal_add_assoc"; |
|
349 |
|
350 (*For AC rewriting*) |
|
351 Goal "(x::hypreal)+(y+z)=y+(x+z)"; |
|
352 by (rtac (hypreal_add_commute RS trans) 1); |
|
353 by (rtac (hypreal_add_assoc RS trans) 1); |
|
354 by (rtac (hypreal_add_commute RS arg_cong) 1); |
|
355 qed "hypreal_add_left_commute"; |
|
356 |
|
357 (* hypreal addition is an AC operator *) |
|
358 bind_thms ("hypreal_add_ac", [hypreal_add_assoc,hypreal_add_commute, |
|
359 hypreal_add_left_commute]); |
|
360 |
|
361 Goalw [hypreal_zero_def] "(0::hypreal) + z = z"; |
|
362 by (res_inst_tac [("z","z")] eq_Abs_hypreal 1); |
|
363 by (asm_full_simp_tac (simpset() addsimps |
|
364 [hypreal_add]) 1); |
|
365 qed "hypreal_add_zero_left"; |
|
366 |
|
367 Goal "z + (0::hypreal) = z"; |
|
368 by (simp_tac (simpset() addsimps |
|
369 [hypreal_add_zero_left,hypreal_add_commute]) 1); |
|
370 qed "hypreal_add_zero_right"; |
|
371 |
|
372 Goalw [hypreal_zero_def] "z + -z = (0::hypreal)"; |
|
373 by (res_inst_tac [("z","z")] eq_Abs_hypreal 1); |
|
374 by (asm_full_simp_tac (simpset() addsimps [hypreal_minus, hypreal_add]) 1); |
|
375 qed "hypreal_add_minus"; |
|
376 |
|
377 Goal "-z + z = (0::hypreal)"; |
|
378 by (simp_tac (simpset() addsimps [hypreal_add_commute, hypreal_add_minus]) 1); |
|
379 qed "hypreal_add_minus_left"; |
|
380 |
|
381 Addsimps [hypreal_add_minus,hypreal_add_minus_left, |
|
382 hypreal_add_zero_left,hypreal_add_zero_right]; |
|
383 |
|
384 Goal "EX y. (x::hypreal) + y = 0"; |
|
385 by (fast_tac (claset() addIs [hypreal_add_minus]) 1); |
|
386 qed "hypreal_minus_ex"; |
|
387 |
|
388 Goal "EX! y. (x::hypreal) + y = 0"; |
|
389 by (auto_tac (claset() addIs [hypreal_add_minus], simpset())); |
|
390 by (dres_inst_tac [("f","%x. ya+x")] arg_cong 1); |
|
391 by (asm_full_simp_tac (simpset() addsimps [hypreal_add_assoc RS sym]) 1); |
|
392 by (asm_full_simp_tac (simpset() addsimps [hypreal_add_commute]) 1); |
|
393 qed "hypreal_minus_ex1"; |
|
394 |
|
395 Goal "EX! y. y + (x::hypreal) = 0"; |
|
396 by (auto_tac (claset() addIs [hypreal_add_minus_left], simpset())); |
|
397 by (dres_inst_tac [("f","%x. x+ya")] arg_cong 1); |
|
398 by (asm_full_simp_tac (simpset() addsimps [hypreal_add_assoc]) 1); |
|
399 by (asm_full_simp_tac (simpset() addsimps [hypreal_add_commute]) 1); |
|
400 qed "hypreal_minus_left_ex1"; |
|
401 |
|
402 Goal "x + y = (0::hypreal) ==> x = -y"; |
|
403 by (cut_inst_tac [("z","y")] hypreal_add_minus_left 1); |
|
404 by (res_inst_tac [("x1","y")] (hypreal_minus_left_ex1 RS ex1E) 1); |
|
405 by (Blast_tac 1); |
|
406 qed "hypreal_add_minus_eq_minus"; |
|
407 |
|
408 Goal "EX y::hypreal. x = -y"; |
|
409 by (cut_inst_tac [("x","x")] hypreal_minus_ex 1); |
|
410 by (etac exE 1 THEN dtac hypreal_add_minus_eq_minus 1); |
|
411 by (Fast_tac 1); |
|
412 qed "hypreal_as_add_inverse_ex"; |
|
413 |
|
414 Goal "-(x + (y::hypreal)) = -x + -y"; |
|
415 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); |
|
416 by (res_inst_tac [("z","y")] eq_Abs_hypreal 1); |
|
417 by (auto_tac (claset(), |
|
418 simpset() addsimps [hypreal_minus, hypreal_add, |
|
419 real_minus_add_distrib])); |
|
420 qed "hypreal_minus_add_distrib"; |
|
421 Addsimps [hypreal_minus_add_distrib]; |
|
422 |
|
423 Goal "-(y + -(x::hypreal)) = x + -y"; |
|
424 by (simp_tac (simpset() addsimps [hypreal_add_commute]) 1); |
|
425 qed "hypreal_minus_distrib1"; |
|
426 |
|
427 Goal "(x + - (y::hypreal)) + (y + - z) = x + -z"; |
|
428 by (res_inst_tac [("w1","y")] (hypreal_add_commute RS subst) 1); |
|
429 by (simp_tac (simpset() addsimps [hypreal_add_left_commute, |
|
430 hypreal_add_assoc]) 1); |
|
431 by (simp_tac (simpset() addsimps [hypreal_add_commute]) 1); |
|
432 qed "hypreal_add_minus_cancel1"; |
|
433 |
|
434 Goal "((x::hypreal) + y = x + z) = (y = z)"; |
|
435 by (Step_tac 1); |
|
436 by (dres_inst_tac [("f","%t.-x + t")] arg_cong 1); |
|
437 by (asm_full_simp_tac (simpset() addsimps [hypreal_add_assoc RS sym]) 1); |
|
438 qed "hypreal_add_left_cancel"; |
|
439 |
|
440 Goal "z + (x + (y + -z)) = x + (y::hypreal)"; |
|
441 by (simp_tac (simpset() addsimps hypreal_add_ac) 1); |
|
442 qed "hypreal_add_minus_cancel2"; |
|
443 Addsimps [hypreal_add_minus_cancel2]; |
|
444 |
|
445 Goal "y + -(x + y) = -(x::hypreal)"; |
|
446 by (Full_simp_tac 1); |
|
447 by (rtac (hypreal_add_left_commute RS subst) 1); |
|
448 by (Full_simp_tac 1); |
|
449 qed "hypreal_add_minus_cancel"; |
|
450 Addsimps [hypreal_add_minus_cancel]; |
|
451 |
|
452 Goal "y + -(y + x) = -(x::hypreal)"; |
|
453 by (simp_tac (simpset() addsimps [hypreal_add_assoc RS sym]) 1); |
|
454 qed "hypreal_add_minus_cancelc"; |
|
455 Addsimps [hypreal_add_minus_cancelc]; |
|
456 |
|
457 Goal "(z + -x) + (y + -z) = (y + -(x::hypreal))"; |
|
458 by (full_simp_tac |
|
459 (simpset() addsimps [hypreal_minus_add_distrib RS sym, |
|
460 hypreal_add_left_cancel] @ hypreal_add_ac |
|
461 delsimps [hypreal_minus_add_distrib]) 1); |
|
462 qed "hypreal_add_minus_cancel3"; |
|
463 Addsimps [hypreal_add_minus_cancel3]; |
|
464 |
|
465 Goal "(y + (x::hypreal)= z + x) = (y = z)"; |
|
466 by (simp_tac (simpset() addsimps [hypreal_add_commute, |
|
467 hypreal_add_left_cancel]) 1); |
|
468 qed "hypreal_add_right_cancel"; |
|
469 |
|
470 Goal "z + (y + -z) = (y::hypreal)"; |
|
471 by (simp_tac (simpset() addsimps hypreal_add_ac) 1); |
|
472 qed "hypreal_add_minus_cancel4"; |
|
473 Addsimps [hypreal_add_minus_cancel4]; |
|
474 |
|
475 Goal "z + (w + (x + (-z + y))) = w + x + (y::hypreal)"; |
|
476 by (simp_tac (simpset() addsimps hypreal_add_ac) 1); |
|
477 qed "hypreal_add_minus_cancel5"; |
|
478 Addsimps [hypreal_add_minus_cancel5]; |
|
479 |
|
480 Goal "z + ((- z) + w) = (w::hypreal)"; |
|
481 by (simp_tac (simpset() addsimps [hypreal_add_assoc RS sym]) 1); |
|
482 qed "hypreal_add_minus_cancelA"; |
|
483 |
|
484 Goal "(-z) + (z + w) = (w::hypreal)"; |
|
485 by (simp_tac (simpset() addsimps [hypreal_add_assoc RS sym]) 1); |
|
486 qed "hypreal_minus_add_cancelA"; |
|
487 |
|
488 Addsimps [hypreal_add_minus_cancelA, hypreal_minus_add_cancelA]; |
|
489 |
|
490 (**** hyperreal multiplication: hypreal_mult ****) |
|
491 |
|
492 Goalw [congruent2_def] |
|
493 "congruent2 hyprel (%X Y. hyprel^^{%n. X n * Y n})"; |
|
494 by Safe_tac; |
|
495 by (ALLGOALS(Ultra_tac)); |
|
496 qed "hypreal_mult_congruent2"; |
|
497 |
|
498 Goalw [hypreal_mult_def] |
|
499 "Abs_hypreal(hyprel^^{%n. X n}) * Abs_hypreal(hyprel^^{%n. Y n}) = \ |
|
500 \ Abs_hypreal(hyprel^^{%n. X n * Y n})"; |
|
501 by (simp_tac (simpset() addsimps |
|
502 [[equiv_hyprel, hypreal_mult_congruent2] MRS UN_equiv_class2]) 1); |
|
503 qed "hypreal_mult"; |
|
504 |
|
505 Goal "(z::hypreal) * w = w * z"; |
|
506 by (res_inst_tac [("z","z")] eq_Abs_hypreal 1); |
|
507 by (res_inst_tac [("z","w")] eq_Abs_hypreal 1); |
|
508 by (asm_simp_tac (simpset() addsimps ([hypreal_mult] @ real_mult_ac)) 1); |
|
509 qed "hypreal_mult_commute"; |
|
510 |
|
511 Goal "((z1::hypreal) * z2) * z3 = z1 * (z2 * z3)"; |
|
512 by (res_inst_tac [("z","z1")] eq_Abs_hypreal 1); |
|
513 by (res_inst_tac [("z","z2")] eq_Abs_hypreal 1); |
|
514 by (res_inst_tac [("z","z3")] eq_Abs_hypreal 1); |
|
515 by (asm_simp_tac (simpset() addsimps [hypreal_mult,real_mult_assoc]) 1); |
|
516 qed "hypreal_mult_assoc"; |
|
517 |
|
518 qed_goal "hypreal_mult_left_commute" (the_context ()) |
|
519 "(z1::hypreal) * (z2 * z3) = z2 * (z1 * z3)" |
|
520 (fn _ => [rtac (hypreal_mult_commute RS trans) 1, |
|
521 rtac (hypreal_mult_assoc RS trans) 1, |
|
522 rtac (hypreal_mult_commute RS arg_cong) 1]); |
|
523 |
|
524 (* hypreal multiplication is an AC operator *) |
|
525 bind_thms ("hypreal_mult_ac", [hypreal_mult_assoc, hypreal_mult_commute, |
|
526 hypreal_mult_left_commute]); |
|
527 |
|
528 Goalw [hypreal_one_def] "1hr * z = z"; |
|
529 by (res_inst_tac [("z","z")] eq_Abs_hypreal 1); |
|
530 by (asm_full_simp_tac (simpset() addsimps [hypreal_mult]) 1); |
|
531 qed "hypreal_mult_1"; |
|
532 |
|
533 Goal "z * 1hr = z"; |
|
534 by (simp_tac (simpset() addsimps [hypreal_mult_commute, |
|
535 hypreal_mult_1]) 1); |
|
536 qed "hypreal_mult_1_right"; |
|
537 |
|
538 Goalw [hypreal_zero_def] "0 * z = (0::hypreal)"; |
|
539 by (res_inst_tac [("z","z")] eq_Abs_hypreal 1); |
|
540 by (asm_full_simp_tac (simpset() addsimps [hypreal_mult,real_mult_0]) 1); |
|
541 qed "hypreal_mult_0"; |
|
542 |
|
543 Goal "z * 0 = (0::hypreal)"; |
|
544 by (simp_tac (simpset() addsimps [hypreal_mult_commute, hypreal_mult_0]) 1); |
|
545 qed "hypreal_mult_0_right"; |
|
546 |
|
547 Addsimps [hypreal_mult_0,hypreal_mult_0_right]; |
|
548 |
|
549 Goal "-(x * y) = -x * (y::hypreal)"; |
|
550 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); |
|
551 by (res_inst_tac [("z","y")] eq_Abs_hypreal 1); |
|
552 by (auto_tac (claset(), |
|
553 simpset() addsimps [hypreal_minus, hypreal_mult] |
|
554 @ real_mult_ac @ real_add_ac)); |
|
555 qed "hypreal_minus_mult_eq1"; |
|
556 |
|
557 Goal "-(x * y) = (x::hypreal) * -y"; |
|
558 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); |
|
559 by (res_inst_tac [("z","y")] eq_Abs_hypreal 1); |
|
560 by (auto_tac (claset(), simpset() addsimps [hypreal_minus, hypreal_mult] |
|
561 @ real_mult_ac @ real_add_ac)); |
|
562 qed "hypreal_minus_mult_eq2"; |
|
563 |
|
564 (*Pull negations out*) |
|
565 Addsimps [hypreal_minus_mult_eq2 RS sym, hypreal_minus_mult_eq1 RS sym]; |
|
566 |
|
567 Goal "-x*y = (x::hypreal)*-y"; |
|
568 by Auto_tac; |
|
569 qed "hypreal_minus_mult_commute"; |
|
570 |
|
571 (*----------------------------------------------------------------------------- |
|
572 A few more theorems |
|
573 ----------------------------------------------------------------------------*) |
|
574 Goal "(z::hypreal) + v = z' + v' ==> z + (v + w) = z' + (v' + w)"; |
|
575 by (asm_simp_tac (simpset() addsimps [hypreal_add_assoc RS sym]) 1); |
|
576 qed "hypreal_add_assoc_cong"; |
|
577 |
|
578 Goal "(z::hypreal) + (v + w) = v + (z + w)"; |
|
579 by (REPEAT (ares_tac [hypreal_add_commute RS hypreal_add_assoc_cong] 1)); |
|
580 qed "hypreal_add_assoc_swap"; |
|
581 |
|
582 Goal "((z1::hypreal) + z2) * w = (z1 * w) + (z2 * w)"; |
|
583 by (res_inst_tac [("z","z1")] eq_Abs_hypreal 1); |
|
584 by (res_inst_tac [("z","z2")] eq_Abs_hypreal 1); |
|
585 by (res_inst_tac [("z","w")] eq_Abs_hypreal 1); |
|
586 by (asm_simp_tac (simpset() addsimps [hypreal_mult,hypreal_add, |
|
587 real_add_mult_distrib]) 1); |
|
588 qed "hypreal_add_mult_distrib"; |
|
589 |
|
590 val hypreal_mult_commute'= read_instantiate [("z","w")] hypreal_mult_commute; |
|
591 |
|
592 Goal "(w::hypreal) * (z1 + z2) = (w * z1) + (w * z2)"; |
|
593 by (simp_tac (simpset() addsimps [hypreal_mult_commute',hypreal_add_mult_distrib]) 1); |
|
594 qed "hypreal_add_mult_distrib2"; |
|
595 |
|
596 bind_thms ("hypreal_mult_simps", [hypreal_mult_1, hypreal_mult_1_right]); |
|
597 Addsimps hypreal_mult_simps; |
|
598 |
|
599 (* 07/00 *) |
|
600 |
|
601 Goalw [hypreal_diff_def] "((z1::hypreal) - z2) * w = (z1 * w) - (z2 * w)"; |
|
602 by (simp_tac (simpset() addsimps [hypreal_add_mult_distrib]) 1); |
|
603 qed "hypreal_diff_mult_distrib"; |
|
604 |
|
605 Goal "(w::hypreal) * (z1 - z2) = (w * z1) - (w * z2)"; |
|
606 by (simp_tac (simpset() addsimps [hypreal_mult_commute', |
|
607 hypreal_diff_mult_distrib]) 1); |
|
608 qed "hypreal_diff_mult_distrib2"; |
|
609 |
|
610 (*** one and zero are distinct ***) |
|
611 Goalw [hypreal_zero_def,hypreal_one_def] "0 ~= 1hr"; |
|
612 by (auto_tac (claset(), simpset() addsimps [real_zero_not_eq_one])); |
|
613 qed "hypreal_zero_not_eq_one"; |
|
614 |
|
615 |
|
616 (**** multiplicative inverse on hypreal ****) |
|
617 |
|
618 Goalw [congruent_def] |
|
619 "congruent hyprel (%X. hyprel^^{%n. if X n = #0 then #0 else inverse(X n)})"; |
|
620 by (Auto_tac THEN Ultra_tac 1); |
|
621 qed "hypreal_inverse_congruent"; |
|
622 |
|
623 Goalw [hypreal_inverse_def] |
|
624 "inverse (Abs_hypreal(hyprel^^{%n. X n})) = \ |
|
625 \ Abs_hypreal(hyprel ^^ {%n. if X n = #0 then #0 else inverse(X n)})"; |
|
626 by (res_inst_tac [("f","Abs_hypreal")] arg_cong 1); |
|
627 by (simp_tac (simpset() addsimps |
|
628 [hyprel_in_hypreal RS Abs_hypreal_inverse, |
|
629 [equiv_hyprel, hypreal_inverse_congruent] MRS UN_equiv_class]) 1); |
|
630 qed "hypreal_inverse"; |
|
631 |
|
632 Goal "inverse 0 = (0::hypreal)"; |
|
633 by (simp_tac (simpset() addsimps [hypreal_inverse, hypreal_zero_def]) 1); |
|
634 qed "HYPREAL_INVERSE_ZERO"; |
|
635 |
|
636 Goal "a / (0::hypreal) = 0"; |
|
637 by (simp_tac |
|
638 (simpset() addsimps [hypreal_divide_def, HYPREAL_INVERSE_ZERO]) 1); |
|
639 qed "HYPREAL_DIVISION_BY_ZERO"; (*NOT for adding to default simpset*) |
|
640 |
|
641 fun hypreal_div_undefined_case_tac s i = |
|
642 case_tac s i THEN |
|
643 asm_simp_tac |
|
644 (simpset() addsimps [HYPREAL_DIVISION_BY_ZERO, HYPREAL_INVERSE_ZERO]) i; |
|
645 |
|
646 Goal "inverse (inverse (z::hypreal)) = z"; |
|
647 by (hypreal_div_undefined_case_tac "z=0" 1); |
|
648 by (res_inst_tac [("z","z")] eq_Abs_hypreal 1); |
|
649 by (asm_full_simp_tac (simpset() addsimps |
|
650 [hypreal_inverse, hypreal_zero_def]) 1); |
|
651 qed "hypreal_inverse_inverse"; |
|
652 Addsimps [hypreal_inverse_inverse]; |
|
653 |
|
654 Goalw [hypreal_one_def] "inverse(1hr) = 1hr"; |
|
655 by (full_simp_tac (simpset() addsimps [hypreal_inverse, |
|
656 real_zero_not_eq_one RS not_sym]) 1); |
|
657 qed "hypreal_inverse_1"; |
|
658 Addsimps [hypreal_inverse_1]; |
|
659 |
|
660 |
|
661 (*** existence of inverse ***) |
|
662 |
|
663 Goalw [hypreal_one_def,hypreal_zero_def] |
|
664 "x ~= 0 ==> x*inverse(x) = 1hr"; |
|
665 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); |
|
666 by (rotate_tac 1 1); |
|
667 by (asm_full_simp_tac (simpset() addsimps [hypreal_inverse, hypreal_mult]) 1); |
|
668 by (dtac FreeUltrafilterNat_Compl_mem 1); |
|
669 by (blast_tac (claset() addSIs [real_mult_inv_right, |
|
670 FreeUltrafilterNat_subset]) 1); |
|
671 qed "hypreal_mult_inverse"; |
|
672 |
|
673 Goal "x ~= 0 ==> inverse(x)*x = 1hr"; |
|
674 by (asm_simp_tac (simpset() addsimps [hypreal_mult_inverse, |
|
675 hypreal_mult_commute]) 1); |
|
676 qed "hypreal_mult_inverse_left"; |
|
677 |
|
678 Goal "(c::hypreal) ~= 0 ==> (c*a=c*b) = (a=b)"; |
|
679 by Auto_tac; |
|
680 by (dres_inst_tac [("f","%x. x*inverse c")] arg_cong 1); |
|
681 by (asm_full_simp_tac (simpset() addsimps [hypreal_mult_inverse] @ hypreal_mult_ac) 1); |
|
682 qed "hypreal_mult_left_cancel"; |
|
683 |
|
684 Goal "(c::hypreal) ~= 0 ==> (a*c=b*c) = (a=b)"; |
|
685 by (Step_tac 1); |
|
686 by (dres_inst_tac [("f","%x. x*inverse c")] arg_cong 1); |
|
687 by (asm_full_simp_tac (simpset() addsimps [hypreal_mult_inverse] @ hypreal_mult_ac) 1); |
|
688 qed "hypreal_mult_right_cancel"; |
|
689 |
|
690 Goalw [hypreal_zero_def] "x ~= 0 ==> inverse (x::hypreal) ~= 0"; |
|
691 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); |
|
692 by (asm_full_simp_tac (simpset() addsimps [hypreal_inverse, hypreal_mult]) 1); |
|
693 qed "hypreal_inverse_not_zero"; |
|
694 |
|
695 Addsimps [hypreal_mult_inverse,hypreal_mult_inverse_left]; |
|
696 |
|
697 Goal "[| x ~= 0; y ~= 0 |] ==> x * y ~= (0::hypreal)"; |
|
698 by (Step_tac 1); |
|
699 by (dres_inst_tac [("f","%z. inverse x*z")] arg_cong 1); |
|
700 by (asm_full_simp_tac (simpset() addsimps [hypreal_mult_assoc RS sym]) 1); |
|
701 qed "hypreal_mult_not_0"; |
|
702 |
|
703 bind_thm ("hypreal_mult_not_0E",hypreal_mult_not_0 RS notE); |
|
704 |
|
705 Goal "x*y = (0::hypreal) ==> x = 0 | y = 0"; |
|
706 by (auto_tac (claset() addIs [ccontr] addDs [hypreal_mult_not_0], |
|
707 simpset())); |
|
708 qed "hypreal_mult_zero_disj"; |
|
709 |
|
710 Goal "inverse(-x) = -inverse(x::hypreal)"; |
|
711 by (hypreal_div_undefined_case_tac "x=0" 1); |
|
712 by (rtac (hypreal_mult_right_cancel RS iffD1) 1); |
|
713 by (stac hypreal_mult_inverse_left 2); |
|
714 by Auto_tac; |
|
715 qed "hypreal_minus_inverse"; |
|
716 |
|
717 Goal "inverse(x*y) = inverse(x)*inverse(y::hypreal)"; |
|
718 by (hypreal_div_undefined_case_tac "x=0" 1); |
|
719 by (hypreal_div_undefined_case_tac "y=0" 1); |
|
720 by (forw_inst_tac [("y","y")] hypreal_mult_not_0 1 THEN assume_tac 1); |
|
721 by (res_inst_tac [("c1","x")] (hypreal_mult_left_cancel RS iffD1) 1); |
|
722 by (auto_tac (claset(), simpset() addsimps [hypreal_mult_assoc RS sym])); |
|
723 by (res_inst_tac [("c1","y")] (hypreal_mult_left_cancel RS iffD1) 1); |
|
724 by (auto_tac (claset(), simpset() addsimps [hypreal_mult_left_commute])); |
|
725 by (asm_simp_tac (simpset() addsimps [hypreal_mult_assoc RS sym]) 1); |
|
726 qed "hypreal_inverse_distrib"; |
|
727 |
|
728 (*------------------------------------------------------------------ |
|
729 Theorems for ordering |
|
730 ------------------------------------------------------------------*) |
|
731 |
|
732 (* prove introduction and elimination rules for hypreal_less *) |
|
733 |
|
734 Goalw [hypreal_less_def] |
|
735 "P < (Q::hypreal) = (EX X Y. X : Rep_hypreal(P) & \ |
|
736 \ Y : Rep_hypreal(Q) & \ |
|
737 \ {n. X n < Y n} : FreeUltrafilterNat)"; |
|
738 by (Fast_tac 1); |
|
739 qed "hypreal_less_iff"; |
|
740 |
|
741 Goalw [hypreal_less_def] |
|
742 "[| {n. X n < Y n} : FreeUltrafilterNat; \ |
|
743 \ X : Rep_hypreal(P); \ |
|
744 \ Y : Rep_hypreal(Q) |] ==> P < (Q::hypreal)"; |
|
745 by (Fast_tac 1); |
|
746 qed "hypreal_lessI"; |
|
747 |
|
748 |
|
749 Goalw [hypreal_less_def] |
|
750 "!! R1. [| R1 < (R2::hypreal); \ |
|
751 \ !!X Y. {n. X n < Y n} : FreeUltrafilterNat ==> P; \ |
|
752 \ !!X. X : Rep_hypreal(R1) ==> P; \ |
|
753 \ !!Y. Y : Rep_hypreal(R2) ==> P |] \ |
|
754 \ ==> P"; |
|
755 by Auto_tac; |
|
756 qed "hypreal_lessE"; |
|
757 |
|
758 Goalw [hypreal_less_def] |
|
759 "R1 < (R2::hypreal) ==> (EX X Y. {n. X n < Y n} : FreeUltrafilterNat & \ |
|
760 \ X : Rep_hypreal(R1) & \ |
|
761 \ Y : Rep_hypreal(R2))"; |
|
762 by (Fast_tac 1); |
|
763 qed "hypreal_lessD"; |
|
764 |
|
765 Goal "~ (R::hypreal) < R"; |
|
766 by (res_inst_tac [("z","R")] eq_Abs_hypreal 1); |
|
767 by (auto_tac (claset(), simpset() addsimps [hypreal_less_def])); |
|
768 by (Ultra_tac 1); |
|
769 qed "hypreal_less_not_refl"; |
|
770 |
|
771 (*** y < y ==> P ***) |
|
772 bind_thm("hypreal_less_irrefl",hypreal_less_not_refl RS notE); |
|
773 AddSEs [hypreal_less_irrefl]; |
|
774 |
|
775 Goal "!!(x::hypreal). x < y ==> x ~= y"; |
|
776 by (auto_tac (claset(), simpset() addsimps [hypreal_less_not_refl])); |
|
777 qed "hypreal_not_refl2"; |
|
778 |
|
779 Goal "!!(R1::hypreal). [| R1 < R2; R2 < R3 |] ==> R1 < R3"; |
|
780 by (res_inst_tac [("z","R1")] eq_Abs_hypreal 1); |
|
781 by (res_inst_tac [("z","R2")] eq_Abs_hypreal 1); |
|
782 by (res_inst_tac [("z","R3")] eq_Abs_hypreal 1); |
|
783 by (auto_tac (claset() addSIs [exI], simpset() addsimps [hypreal_less_def])); |
|
784 by (ultra_tac (claset() addIs [real_less_trans], simpset()) 1); |
|
785 qed "hypreal_less_trans"; |
|
786 |
|
787 Goal "!! (R1::hypreal). [| R1 < R2; R2 < R1 |] ==> P"; |
|
788 by (dtac hypreal_less_trans 1 THEN assume_tac 1); |
|
789 by (asm_full_simp_tac (simpset() addsimps |
|
790 [hypreal_less_not_refl]) 1); |
|
791 qed "hypreal_less_asym"; |
|
792 |
|
793 (*------------------------------------------------------- |
|
794 TODO: The following theorem should have been proved |
|
795 first and then used througout the proofs as it probably |
|
796 makes many of them more straightforward. |
|
797 -------------------------------------------------------*) |
|
798 Goalw [hypreal_less_def] |
|
799 "(Abs_hypreal(hyprel^^{%n. X n}) < \ |
|
800 \ Abs_hypreal(hyprel^^{%n. Y n})) = \ |
|
801 \ ({n. X n < Y n} : FreeUltrafilterNat)"; |
|
802 by (auto_tac (claset() addSIs [lemma_hyprel_refl], simpset())); |
|
803 by (Ultra_tac 1); |
|
804 qed "hypreal_less"; |
|
805 |
|
806 (*--------------------------------------------------------------------------------- |
|
807 Hyperreals as a linearly ordered field |
|
808 ---------------------------------------------------------------------------------*) |
|
809 (*** sum order |
|
810 Goalw [hypreal_zero_def] |
|
811 "[| 0 < x; 0 < y |] ==> (0::hypreal) < x + y"; |
|
812 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); |
|
813 by (res_inst_tac [("z","y")] eq_Abs_hypreal 1); |
|
814 by (auto_tac (claset(),simpset() addsimps |
|
815 [hypreal_less_def,hypreal_add])); |
|
816 by (auto_tac (claset() addSIs [exI],simpset() addsimps |
|
817 [hypreal_less_def,hypreal_add])); |
|
818 by (ultra_tac (claset() addIs [real_add_order],simpset()) 1); |
|
819 qed "hypreal_add_order"; |
|
820 ***) |
|
821 |
|
822 (*** mult order |
|
823 Goalw [hypreal_zero_def] |
|
824 "[| 0 < x; 0 < y |] ==> (0::hypreal) < x * y"; |
|
825 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); |
|
826 by (res_inst_tac [("z","y")] eq_Abs_hypreal 1); |
|
827 by (auto_tac (claset() addSIs [exI],simpset() addsimps |
|
828 [hypreal_less_def,hypreal_mult])); |
|
829 by (ultra_tac (claset() addIs [rename_numerals real_mult_order], |
|
830 simpset()) 1); |
|
831 qed "hypreal_mult_order"; |
|
832 ****) |
|
833 |
|
834 |
|
835 (*--------------------------------------------------------------------------------- |
|
836 Trichotomy of the hyperreals |
|
837 --------------------------------------------------------------------------------*) |
|
838 |
|
839 Goalw [hyprel_def] "EX x. x: hyprel ^^ {%n. #0}"; |
|
840 by (res_inst_tac [("x","%n. #0")] exI 1); |
|
841 by (Step_tac 1); |
|
842 by (auto_tac (claset() addSIs [FreeUltrafilterNat_Nat_set], simpset())); |
|
843 qed "lemma_hyprel_0r_mem"; |
|
844 |
|
845 Goalw [hypreal_zero_def]"0 < x | x = 0 | x < (0::hypreal)"; |
|
846 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); |
|
847 by (auto_tac (claset(),simpset() addsimps [hypreal_less_def])); |
|
848 by (cut_facts_tac [lemma_hyprel_0r_mem] 1 THEN etac exE 1); |
|
849 by (dres_inst_tac [("x","xa")] spec 1); |
|
850 by (dres_inst_tac [("x","x")] spec 1); |
|
851 by (cut_inst_tac [("x","x")] lemma_hyprel_refl 1); |
|
852 by Auto_tac; |
|
853 by (dres_inst_tac [("x","x")] spec 1); |
|
854 by (dres_inst_tac [("x","xa")] spec 1); |
|
855 by Auto_tac; |
|
856 by (Ultra_tac 1); |
|
857 by (auto_tac (claset() addIs [real_linear_less2],simpset())); |
|
858 qed "hypreal_trichotomy"; |
|
859 |
|
860 val prems = Goal "[| (0::hypreal) < x ==> P; \ |
|
861 \ x = 0 ==> P; \ |
|
862 \ x < 0 ==> P |] ==> P"; |
|
863 by (cut_inst_tac [("x","x")] hypreal_trichotomy 1); |
|
864 by (REPEAT (eresolve_tac (disjE::prems) 1)); |
|
865 qed "hypreal_trichotomyE"; |
|
866 |
|
867 (*---------------------------------------------------------------------------- |
|
868 More properties of < |
|
869 ----------------------------------------------------------------------------*) |
|
870 |
|
871 Goal "((x::hypreal) < y) = (0 < y + -x)"; |
|
872 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); |
|
873 by (res_inst_tac [("z","y")] eq_Abs_hypreal 1); |
|
874 by (auto_tac (claset(),simpset() addsimps [hypreal_add, |
|
875 hypreal_zero_def,hypreal_minus,hypreal_less])); |
|
876 by (ALLGOALS(Ultra_tac)); |
|
877 qed "hypreal_less_minus_iff"; |
|
878 |
|
879 Goal "((x::hypreal) < y) = (x + -y < 0)"; |
|
880 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); |
|
881 by (res_inst_tac [("z","y")] eq_Abs_hypreal 1); |
|
882 by (auto_tac (claset(),simpset() addsimps [hypreal_add, |
|
883 hypreal_zero_def,hypreal_minus,hypreal_less])); |
|
884 by (ALLGOALS(Ultra_tac)); |
|
885 qed "hypreal_less_minus_iff2"; |
|
886 |
|
887 Goal "((x::hypreal) = y) = (0 = x + - y)"; |
|
888 by Auto_tac; |
|
889 by (res_inst_tac [("x1","-y")] (hypreal_add_right_cancel RS iffD1) 1); |
|
890 by Auto_tac; |
|
891 qed "hypreal_eq_minus_iff"; |
|
892 |
|
893 Goal "((x::hypreal) = y) = (0 = y + - x)"; |
|
894 by Auto_tac; |
|
895 by (res_inst_tac [("x1","-x")] (hypreal_add_right_cancel RS iffD1) 1); |
|
896 by Auto_tac; |
|
897 qed "hypreal_eq_minus_iff2"; |
|
898 |
|
899 (* 07/00 *) |
|
900 Goal "(0::hypreal) - x = -x"; |
|
901 by (simp_tac (simpset() addsimps [hypreal_diff_def]) 1); |
|
902 qed "hypreal_diff_zero"; |
|
903 |
|
904 Goal "x - (0::hypreal) = x"; |
|
905 by (simp_tac (simpset() addsimps [hypreal_diff_def]) 1); |
|
906 qed "hypreal_diff_zero_right"; |
|
907 |
|
908 Goal "x - x = (0::hypreal)"; |
|
909 by (simp_tac (simpset() addsimps [hypreal_diff_def]) 1); |
|
910 qed "hypreal_diff_self"; |
|
911 |
|
912 Addsimps [hypreal_diff_zero, hypreal_diff_zero_right, hypreal_diff_self]; |
|
913 |
|
914 Goal "(x = y + z) = (x + -z = (y::hypreal))"; |
|
915 by (auto_tac (claset(),simpset() addsimps [hypreal_add_assoc])); |
|
916 qed "hypreal_eq_minus_iff3"; |
|
917 |
|
918 Goal "(x ~= a) = (x + -a ~= (0::hypreal))"; |
|
919 by (auto_tac (claset() addDs [sym RS (hypreal_eq_minus_iff RS iffD2)], |
|
920 simpset())); |
|
921 qed "hypreal_not_eq_minus_iff"; |
|
922 |
|
923 (*** linearity ***) |
|
924 Goal "(x::hypreal) < y | x = y | y < x"; |
|
925 by (stac hypreal_eq_minus_iff2 1); |
|
926 by (res_inst_tac [("x1","x")] (hypreal_less_minus_iff RS ssubst) 1); |
|
927 by (res_inst_tac [("x1","y")] (hypreal_less_minus_iff2 RS ssubst) 1); |
|
928 by (rtac hypreal_trichotomyE 1); |
|
929 by Auto_tac; |
|
930 qed "hypreal_linear"; |
|
931 |
|
932 Goal "((w::hypreal) ~= z) = (w<z | z<w)"; |
|
933 by (cut_facts_tac [hypreal_linear] 1); |
|
934 by (Blast_tac 1); |
|
935 qed "hypreal_neq_iff"; |
|
936 |
|
937 Goal "!!(x::hypreal). [| x < y ==> P; x = y ==> P; \ |
|
938 \ y < x ==> P |] ==> P"; |
|
939 by (cut_inst_tac [("x","x"),("y","y")] hypreal_linear 1); |
|
940 by Auto_tac; |
|
941 qed "hypreal_linear_less2"; |
|
942 |
|
943 (*------------------------------------------------------------------------------ |
|
944 Properties of <= |
|
945 ------------------------------------------------------------------------------*) |
|
946 (*------ hypreal le iff reals le a.e ------*) |
|
947 |
|
948 Goalw [hypreal_le_def,real_le_def] |
|
949 "(Abs_hypreal(hyprel^^{%n. X n}) <= \ |
|
950 \ Abs_hypreal(hyprel^^{%n. Y n})) = \ |
|
951 \ ({n. X n <= Y n} : FreeUltrafilterNat)"; |
|
952 by (auto_tac (claset(),simpset() addsimps [hypreal_less])); |
|
953 by (ALLGOALS(Ultra_tac)); |
|
954 qed "hypreal_le"; |
|
955 |
|
956 (*---------------------------------------------------------*) |
|
957 (*---------------------------------------------------------*) |
|
958 Goalw [hypreal_le_def] |
|
959 "~(w < z) ==> z <= (w::hypreal)"; |
|
960 by (assume_tac 1); |
|
961 qed "hypreal_leI"; |
|
962 |
|
963 Goalw [hypreal_le_def] |
|
964 "z<=w ==> ~(w<(z::hypreal))"; |
|
965 by (assume_tac 1); |
|
966 qed "hypreal_leD"; |
|
967 |
|
968 bind_thm ("hypreal_leE", make_elim hypreal_leD); |
|
969 |
|
970 Goal "(~(w < z)) = (z <= (w::hypreal))"; |
|
971 by (fast_tac (claset() addSIs [hypreal_leI,hypreal_leD]) 1); |
|
972 qed "hypreal_less_le_iff"; |
|
973 |
|
974 Goalw [hypreal_le_def] "~ z <= w ==> w<(z::hypreal)"; |
|
975 by (Fast_tac 1); |
|
976 qed "not_hypreal_leE"; |
|
977 |
|
978 Goalw [hypreal_le_def] "z < w ==> z <= (w::hypreal)"; |
|
979 by (fast_tac (claset() addEs [hypreal_less_asym]) 1); |
|
980 qed "hypreal_less_imp_le"; |
|
981 |
|
982 Goalw [hypreal_le_def] "!!(x::hypreal). x <= y ==> x < y | x = y"; |
|
983 by (cut_facts_tac [hypreal_linear] 1); |
|
984 by (fast_tac (claset() addEs [hypreal_less_irrefl,hypreal_less_asym]) 1); |
|
985 qed "hypreal_le_imp_less_or_eq"; |
|
986 |
|
987 Goalw [hypreal_le_def] "z<w | z=w ==> z <=(w::hypreal)"; |
|
988 by (cut_facts_tac [hypreal_linear] 1); |
|
989 by (fast_tac (claset() addEs [hypreal_less_irrefl,hypreal_less_asym]) 1); |
|
990 qed "hypreal_less_or_eq_imp_le"; |
|
991 |
|
992 Goal "(x <= (y::hypreal)) = (x < y | x=y)"; |
|
993 by (REPEAT(ares_tac [iffI, hypreal_less_or_eq_imp_le, hypreal_le_imp_less_or_eq] 1)); |
|
994 qed "hypreal_le_eq_less_or_eq"; |
|
995 val hypreal_le_less = hypreal_le_eq_less_or_eq; |
|
996 |
|
997 Goal "w <= (w::hypreal)"; |
|
998 by (simp_tac (simpset() addsimps [hypreal_le_eq_less_or_eq]) 1); |
|
999 qed "hypreal_le_refl"; |
|
1000 Addsimps [hypreal_le_refl]; |
|
1001 |
|
1002 (* Axiom 'linorder_linear' of class 'linorder': *) |
|
1003 Goal "(z::hypreal) <= w | w <= z"; |
|
1004 by (simp_tac (simpset() addsimps [hypreal_le_less]) 1); |
|
1005 by (cut_facts_tac [hypreal_linear] 1); |
|
1006 by (Blast_tac 1); |
|
1007 qed "hypreal_le_linear"; |
|
1008 |
|
1009 Goal "[| i <= j; j < k |] ==> i < (k::hypreal)"; |
|
1010 by (dtac hypreal_le_imp_less_or_eq 1); |
|
1011 by (fast_tac (claset() addIs [hypreal_less_trans]) 1); |
|
1012 qed "hypreal_le_less_trans"; |
|
1013 |
|
1014 Goal "!! (i::hypreal). [| i < j; j <= k |] ==> i < k"; |
|
1015 by (dtac hypreal_le_imp_less_or_eq 1); |
|
1016 by (fast_tac (claset() addIs [hypreal_less_trans]) 1); |
|
1017 qed "hypreal_less_le_trans"; |
|
1018 |
|
1019 Goal "[| i <= j; j <= k |] ==> i <= (k::hypreal)"; |
|
1020 by (EVERY1 [dtac hypreal_le_imp_less_or_eq, dtac hypreal_le_imp_less_or_eq, |
|
1021 rtac hypreal_less_or_eq_imp_le, fast_tac (claset() addIs [hypreal_less_trans])]); |
|
1022 qed "hypreal_le_trans"; |
|
1023 |
|
1024 Goal "[| z <= w; w <= z |] ==> z = (w::hypreal)"; |
|
1025 by (EVERY1 [dtac hypreal_le_imp_less_or_eq, dtac hypreal_le_imp_less_or_eq, |
|
1026 fast_tac (claset() addEs [hypreal_less_irrefl,hypreal_less_asym])]); |
|
1027 qed "hypreal_le_anti_sym"; |
|
1028 |
|
1029 Goal "[| ~ y < x; y ~= x |] ==> x < (y::hypreal)"; |
|
1030 by (rtac not_hypreal_leE 1); |
|
1031 by (fast_tac (claset() addDs [hypreal_le_imp_less_or_eq]) 1); |
|
1032 qed "not_less_not_eq_hypreal_less"; |
|
1033 |
|
1034 (* Axiom 'order_less_le' of class 'order': *) |
|
1035 Goal "(w::hypreal) < z = (w <= z & w ~= z)"; |
|
1036 by (simp_tac (simpset() addsimps [hypreal_le_def, hypreal_neq_iff]) 1); |
|
1037 by (blast_tac (claset() addIs [hypreal_less_asym]) 1); |
|
1038 qed "hypreal_less_le"; |
|
1039 |
|
1040 Goal "(0 < -R) = (R < (0::hypreal))"; |
|
1041 by (res_inst_tac [("z","R")] eq_Abs_hypreal 1); |
|
1042 by (auto_tac (claset(), |
|
1043 simpset() addsimps [hypreal_zero_def, hypreal_less,hypreal_minus])); |
|
1044 qed "hypreal_minus_zero_less_iff"; |
|
1045 Addsimps [hypreal_minus_zero_less_iff]; |
|
1046 |
|
1047 Goal "(-R < 0) = ((0::hypreal) < R)"; |
|
1048 by (res_inst_tac [("z","R")] eq_Abs_hypreal 1); |
|
1049 by (auto_tac (claset(), |
|
1050 simpset() addsimps [hypreal_zero_def, hypreal_less,hypreal_minus])); |
|
1051 by (ALLGOALS(Ultra_tac)); |
|
1052 qed "hypreal_minus_zero_less_iff2"; |
|
1053 |
|
1054 Goalw [hypreal_le_def] "((0::hypreal) <= -r) = (r <= (0::hypreal))"; |
|
1055 by (simp_tac (simpset() addsimps [hypreal_minus_zero_less_iff2]) 1); |
|
1056 qed "hypreal_minus_zero_le_iff"; |
|
1057 Addsimps [hypreal_minus_zero_le_iff]; |
|
1058 |
|
1059 (*---------------------------------------------------------- |
|
1060 hypreal_of_real preserves field and order properties |
|
1061 -----------------------------------------------------------*) |
|
1062 Goalw [hypreal_of_real_def] |
|
1063 "hypreal_of_real (z1 + z2) = hypreal_of_real z1 + hypreal_of_real z2"; |
|
1064 by (simp_tac (simpset() addsimps [hypreal_add, hypreal_add_mult_distrib]) 1); |
|
1065 qed "hypreal_of_real_add"; |
|
1066 Addsimps [hypreal_of_real_add]; |
|
1067 |
|
1068 Goalw [hypreal_of_real_def] |
|
1069 "hypreal_of_real (z1 * z2) = hypreal_of_real z1 * hypreal_of_real z2"; |
|
1070 by (simp_tac (simpset() addsimps [hypreal_mult, hypreal_add_mult_distrib2]) 1); |
|
1071 qed "hypreal_of_real_mult"; |
|
1072 Addsimps [hypreal_of_real_mult]; |
|
1073 |
|
1074 Goalw [hypreal_less_def,hypreal_of_real_def] |
|
1075 "(z1 < z2) = (hypreal_of_real z1 < hypreal_of_real z2)"; |
|
1076 by Auto_tac; |
|
1077 by (res_inst_tac [("x","%n. z1")] exI 1); |
|
1078 by (Step_tac 1); |
|
1079 by (res_inst_tac [("x","%n. z2")] exI 2); |
|
1080 by Auto_tac; |
|
1081 by (rtac FreeUltrafilterNat_P 1); |
|
1082 by (Ultra_tac 1); |
|
1083 qed "hypreal_of_real_less_iff"; |
|
1084 |
|
1085 Addsimps [hypreal_of_real_less_iff RS sym]; |
|
1086 |
|
1087 Goalw [hypreal_le_def,real_le_def] |
|
1088 "(z1 <= z2) = (hypreal_of_real z1 <= hypreal_of_real z2)"; |
|
1089 by Auto_tac; |
|
1090 qed "hypreal_of_real_le_iff"; |
|
1091 |
|
1092 Goalw [hypreal_of_real_def] "hypreal_of_real (-r) = - hypreal_of_real r"; |
|
1093 by (auto_tac (claset(),simpset() addsimps [hypreal_minus])); |
|
1094 qed "hypreal_of_real_minus"; |
|
1095 Addsimps [hypreal_of_real_minus]; |
|
1096 |
|
1097 (*DON'T insert this or the next one as default simprules. |
|
1098 They are used in both orientations and anyway aren't the ones we finally |
|
1099 need, which would use binary literals.*) |
|
1100 Goalw [hypreal_of_real_def,hypreal_one_def] "hypreal_of_real #1 = 1hr"; |
|
1101 by (Step_tac 1); |
|
1102 qed "hypreal_of_real_one"; |
|
1103 |
|
1104 Goalw [hypreal_of_real_def,hypreal_zero_def] "hypreal_of_real #0 = 0"; |
|
1105 by (Step_tac 1); |
|
1106 qed "hypreal_of_real_zero"; |
|
1107 |
|
1108 Goal "(hypreal_of_real r = 0) = (r = #0)"; |
|
1109 by (auto_tac (claset() addIs [FreeUltrafilterNat_P], |
|
1110 simpset() addsimps [hypreal_of_real_def, |
|
1111 hypreal_zero_def,FreeUltrafilterNat_Nat_set])); |
|
1112 qed "hypreal_of_real_zero_iff"; |
|
1113 AddIffs [hypreal_of_real_zero_iff]; |
|
1114 |
|
1115 |
|
1116 Goal "hypreal_of_real (inverse r) = inverse (hypreal_of_real r)"; |
|
1117 by (case_tac "r=#0" 1); |
|
1118 by (asm_simp_tac (simpset() addsimps [REAL_DIVIDE_ZERO, INVERSE_ZERO, |
|
1119 HYPREAL_INVERSE_ZERO, hypreal_of_real_zero]) 1); |
|
1120 by (res_inst_tac [("c1","hypreal_of_real r")] |
|
1121 (hypreal_mult_left_cancel RS iffD1) 1); |
|
1122 by (stac (hypreal_of_real_mult RS sym) 2); |
|
1123 by (auto_tac (claset(), simpset() addsimps [hypreal_of_real_one])); |
|
1124 qed "hypreal_of_real_inverse"; |
|
1125 Addsimps [hypreal_of_real_inverse]; |
|
1126 |
|
1127 Goal "hypreal_of_real (z1 / z2) = hypreal_of_real z1 / hypreal_of_real z2"; |
|
1128 by (simp_tac (simpset() addsimps [hypreal_divide_def, real_divide_def]) 1); |
|
1129 qed "hypreal_of_real_divide"; |
|
1130 Addsimps [hypreal_of_real_divide]; |
|
1131 |
|
1132 |
|
1133 (*** Division lemmas ***) |
|
1134 |
|
1135 Goal "(0::hypreal)/x = 0"; |
|
1136 by (simp_tac (simpset() addsimps [hypreal_divide_def]) 1); |
|
1137 qed "hypreal_zero_divide"; |
|
1138 |
|
1139 Goal "x/1hr = x"; |
|
1140 by (simp_tac (simpset() addsimps [hypreal_divide_def]) 1); |
|
1141 qed "hypreal_divide_one"; |
|
1142 Addsimps [hypreal_zero_divide, hypreal_divide_one]; |
|
1143 |
|
1144 Goal "(x::hypreal) * (y/z) = (x*y)/z"; |
|
1145 by (simp_tac (simpset() addsimps [hypreal_divide_def, hypreal_mult_assoc]) 1); |
|
1146 qed "hypreal_times_divide1_eq"; |
|
1147 |
|
1148 Goal "(y/z) * (x::hypreal) = (y*x)/z"; |
|
1149 by (simp_tac (simpset() addsimps [hypreal_divide_def]@hypreal_mult_ac) 1); |
|
1150 qed "hypreal_times_divide2_eq"; |
|
1151 |
|
1152 Addsimps [hypreal_times_divide1_eq, hypreal_times_divide2_eq]; |
|
1153 |
|
1154 Goal "(x::hypreal) / (y/z) = (x*z)/y"; |
|
1155 by (simp_tac (simpset() addsimps [hypreal_divide_def, hypreal_inverse_distrib]@ |
|
1156 hypreal_mult_ac) 1); |
|
1157 qed "hypreal_divide_divide1_eq"; |
|
1158 |
|
1159 Goal "((x::hypreal) / y) / z = x/(y*z)"; |
|
1160 by (simp_tac (simpset() addsimps [hypreal_divide_def, hypreal_inverse_distrib, |
|
1161 hypreal_mult_assoc]) 1); |
|
1162 qed "hypreal_divide_divide2_eq"; |
|
1163 |
|
1164 Addsimps [hypreal_divide_divide1_eq, hypreal_divide_divide2_eq]; |
|
1165 |
|
1166 (** As with multiplication, pull minus signs OUT of the / operator **) |
|
1167 |
|
1168 Goal "(-x) / (y::hypreal) = - (x/y)"; |
|
1169 by (simp_tac (simpset() addsimps [hypreal_divide_def]) 1); |
|
1170 qed "hypreal_minus_divide_eq"; |
|
1171 Addsimps [hypreal_minus_divide_eq]; |
|
1172 |
|
1173 Goal "(x / -(y::hypreal)) = - (x/y)"; |
|
1174 by (simp_tac (simpset() addsimps [hypreal_divide_def, hypreal_minus_inverse]) 1); |
|
1175 qed "hypreal_divide_minus_eq"; |
|
1176 Addsimps [hypreal_divide_minus_eq]; |
|
1177 |
|
1178 Goal "(x+y)/(z::hypreal) = x/z + y/z"; |
|
1179 by (simp_tac (simpset() addsimps [hypreal_divide_def, hypreal_add_mult_distrib]) 1); |
|
1180 qed "hypreal_add_divide_distrib"; |
|
1181 |
|
1182 |
|
1183 Goal "x+x=x*(1hr+1hr)"; |
|
1184 by (simp_tac (simpset() addsimps [hypreal_add_mult_distrib2]) 1); |
|
1185 qed "hypreal_add_self"; |
|
1186 |
|
1187 (*FIXME: DELETE (used in Lim.ML) *) |
|
1188 Goal "(z::hypreal) ~= 0 ==> x*y = (x*inverse(z))*(z*y)"; |
|
1189 by (asm_simp_tac (simpset() addsimps hypreal_mult_ac) 1); |
|
1190 qed "lemma_chain"; |
|
1191 |
|
1192 Goal "[|(x::hypreal) ~= 0; y ~= 0 |] ==> \ |
|
1193 \ inverse(x) + inverse(y) = (x + y)*inverse(x*y)"; |
|
1194 by (asm_full_simp_tac (simpset() addsimps [hypreal_inverse_distrib, |
|
1195 hypreal_add_mult_distrib,hypreal_mult_assoc RS sym]) 1); |
|
1196 by (stac hypreal_mult_assoc 1); |
|
1197 by (rtac (hypreal_mult_left_commute RS subst) 1); |
|
1198 by (asm_full_simp_tac (simpset() addsimps [hypreal_add_commute]) 1); |
|
1199 qed "hypreal_inverse_add"; |
|
1200 |
|
1201 Goal "x = -x ==> x = (0::hypreal)"; |
|
1202 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); |
|
1203 by (auto_tac (claset(),simpset() addsimps [hypreal_minus, |
|
1204 hypreal_zero_def])); |
|
1205 by (Ultra_tac 1); |
|
1206 qed "hypreal_self_eq_minus_self_zero"; |
|
1207 |
|
1208 Goal "(x + x = 0) = (x = (0::hypreal))"; |
|
1209 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); |
|
1210 by (auto_tac (claset(),simpset() addsimps [hypreal_add, |
|
1211 hypreal_zero_def])); |
|
1212 qed "hypreal_add_self_zero_cancel"; |
|
1213 Addsimps [hypreal_add_self_zero_cancel]; |
|
1214 |
|
1215 Goal "(x + x + y = y) = (x = (0::hypreal))"; |
|
1216 by Auto_tac; |
|
1217 by (dtac (hypreal_eq_minus_iff RS iffD1) 1 THEN dtac sym 1); |
|
1218 by (auto_tac (claset(),simpset() addsimps [hypreal_add_assoc])); |
|
1219 qed "hypreal_add_self_zero_cancel2"; |
|
1220 Addsimps [hypreal_add_self_zero_cancel2]; |
|
1221 |
|
1222 Goal "(x + (x + y) = y) = (x = (0::hypreal))"; |
|
1223 by (simp_tac (simpset() addsimps [hypreal_add_assoc RS sym]) 1); |
|
1224 qed "hypreal_add_self_zero_cancel2a"; |
|
1225 Addsimps [hypreal_add_self_zero_cancel2a]; |
|
1226 |
|
1227 Goal "(b = -a) = (-b = (a::hypreal))"; |
|
1228 by Auto_tac; |
|
1229 qed "hypreal_minus_eq_swap"; |
|
1230 |
|
1231 Goal "(-b = -a) = (b = (a::hypreal))"; |
|
1232 by (asm_full_simp_tac (simpset() addsimps |
|
1233 [hypreal_minus_eq_swap]) 1); |
|
1234 qed "hypreal_minus_eq_cancel"; |
|
1235 Addsimps [hypreal_minus_eq_cancel]; |
|
1236 |
|
1237 Goal "x < x + 1hr"; |
|
1238 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); |
|
1239 by (auto_tac (claset(),simpset() addsimps [hypreal_add, |
|
1240 hypreal_one_def,hypreal_less])); |
|
1241 qed "hypreal_less_self_add_one"; |
|
1242 Addsimps [hypreal_less_self_add_one]; |
|
1243 |
|
1244 Goal "((x::hypreal) + x = y + y) = (x = y)"; |
|
1245 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); |
|
1246 by (res_inst_tac [("z","y")] eq_Abs_hypreal 1); |
|
1247 by (auto_tac (claset(),simpset() addsimps [hypreal_add])); |
|
1248 by (ALLGOALS(Ultra_tac)); |
|
1249 qed "hypreal_add_self_cancel"; |
|
1250 Addsimps [hypreal_add_self_cancel]; |
|
1251 |
|
1252 Goal "(y = x + - y + x) = (y = (x::hypreal))"; |
|
1253 by Auto_tac; |
|
1254 by (dres_inst_tac [("x1","y")] |
|
1255 (hypreal_add_right_cancel RS iffD2) 1); |
|
1256 by (auto_tac (claset(),simpset() addsimps hypreal_add_ac)); |
|
1257 qed "hypreal_add_self_minus_cancel"; |
|
1258 Addsimps [hypreal_add_self_minus_cancel]; |
|
1259 |
|
1260 Goal "(y = x + (- y + x)) = (y = (x::hypreal))"; |
|
1261 by (asm_full_simp_tac (simpset() addsimps |
|
1262 [hypreal_add_assoc RS sym])1); |
|
1263 qed "hypreal_add_self_minus_cancel2"; |
|
1264 Addsimps [hypreal_add_self_minus_cancel2]; |
|
1265 |
|
1266 (* of course, can prove this by "transfer" as well *) |
|
1267 Goal "z + -x = y + (y + (-x + -z)) = (y = (z::hypreal))"; |
|
1268 by Auto_tac; |
|
1269 by (dres_inst_tac [("x1","z")] |
|
1270 (hypreal_add_right_cancel RS iffD2) 1); |
|
1271 by (asm_full_simp_tac (simpset() addsimps |
|
1272 [hypreal_minus_add_distrib RS sym] @ hypreal_add_ac |
|
1273 delsimps [hypreal_minus_add_distrib]) 1); |
|
1274 by (asm_full_simp_tac (simpset() addsimps |
|
1275 [hypreal_add_assoc RS sym,hypreal_add_right_cancel]) 1); |
|
1276 qed "hypreal_add_self_minus_cancel3"; |
|
1277 Addsimps [hypreal_add_self_minus_cancel3]; |
|
1278 |
|
1279 Goal "(x * x = 0) = (x = (0::hypreal))"; |
|
1280 by Auto_tac; |
|
1281 by (blast_tac (claset() addIs [hypreal_mult_not_0E]) 1); |
|
1282 qed "hypreal_mult_self_eq_zero_iff"; |
|
1283 Addsimps [hypreal_mult_self_eq_zero_iff]; |
|
1284 |
|
1285 Goalw [hypreal_diff_def] "(x<y) = (x-y < (0::hypreal))"; |
|
1286 by (rtac hypreal_less_minus_iff2 1); |
|
1287 qed "hypreal_less_eq_diff"; |
|
1288 |
|
1289 (*** Subtraction laws ***) |
|
1290 |
|
1291 Goal "x + (y - z) = (x + y) - (z::hypreal)"; |
|
1292 by (simp_tac (simpset() addsimps hypreal_diff_def::hypreal_add_ac) 1); |
|
1293 qed "hypreal_add_diff_eq"; |
|
1294 |
|
1295 Goal "(x - y) + z = (x + z) - (y::hypreal)"; |
|
1296 by (simp_tac (simpset() addsimps hypreal_diff_def::hypreal_add_ac) 1); |
|
1297 qed "hypreal_diff_add_eq"; |
|
1298 |
|
1299 Goal "(x - y) - z = x - (y + (z::hypreal))"; |
|
1300 by (simp_tac (simpset() addsimps hypreal_diff_def::hypreal_add_ac) 1); |
|
1301 qed "hypreal_diff_diff_eq"; |
|
1302 |
|
1303 Goal "x - (y - z) = (x + z) - (y::hypreal)"; |
|
1304 by (simp_tac (simpset() addsimps hypreal_diff_def::hypreal_add_ac) 1); |
|
1305 qed "hypreal_diff_diff_eq2"; |
|
1306 |
|
1307 Goal "(x-y < z) = (x < z + (y::hypreal))"; |
|
1308 by (stac hypreal_less_eq_diff 1); |
|
1309 by (res_inst_tac [("y1", "z")] (hypreal_less_eq_diff RS ssubst) 1); |
|
1310 by (simp_tac (simpset() addsimps hypreal_diff_def::hypreal_add_ac) 1); |
|
1311 qed "hypreal_diff_less_eq"; |
|
1312 |
|
1313 Goal "(x < z-y) = (x + (y::hypreal) < z)"; |
|
1314 by (stac hypreal_less_eq_diff 1); |
|
1315 by (res_inst_tac [("y1", "z-y")] (hypreal_less_eq_diff RS ssubst) 1); |
|
1316 by (simp_tac (simpset() addsimps hypreal_diff_def::hypreal_add_ac) 1); |
|
1317 qed "hypreal_less_diff_eq"; |
|
1318 |
|
1319 Goalw [hypreal_le_def] "(x-y <= z) = (x <= z + (y::hypreal))"; |
|
1320 by (simp_tac (simpset() addsimps [hypreal_less_diff_eq]) 1); |
|
1321 qed "hypreal_diff_le_eq"; |
|
1322 |
|
1323 Goalw [hypreal_le_def] "(x <= z-y) = (x + (y::hypreal) <= z)"; |
|
1324 by (simp_tac (simpset() addsimps [hypreal_diff_less_eq]) 1); |
|
1325 qed "hypreal_le_diff_eq"; |
|
1326 |
|
1327 Goalw [hypreal_diff_def] "(x-y = z) = (x = z + (y::hypreal))"; |
|
1328 by (auto_tac (claset(), simpset() addsimps [hypreal_add_assoc])); |
|
1329 qed "hypreal_diff_eq_eq"; |
|
1330 |
|
1331 Goalw [hypreal_diff_def] "(x = z-y) = (x + (y::hypreal) = z)"; |
|
1332 by (auto_tac (claset(), simpset() addsimps [hypreal_add_assoc])); |
|
1333 qed "hypreal_eq_diff_eq"; |
|
1334 |
|
1335 (*This list of rewrites simplifies (in)equalities by bringing subtractions |
|
1336 to the top and then moving negative terms to the other side. |
|
1337 Use with hypreal_add_ac*) |
|
1338 val hypreal_compare_rls = |
|
1339 [symmetric hypreal_diff_def, |
|
1340 hypreal_add_diff_eq, hypreal_diff_add_eq, hypreal_diff_diff_eq, hypreal_diff_diff_eq2, |
|
1341 hypreal_diff_less_eq, hypreal_less_diff_eq, hypreal_diff_le_eq, hypreal_le_diff_eq, |
|
1342 hypreal_diff_eq_eq, hypreal_eq_diff_eq]; |
|
1343 |
|
1344 |
|
1345 (** For the cancellation simproc. |
|
1346 The idea is to cancel like terms on opposite sides by subtraction **) |
|
1347 |
|
1348 Goal "(x::hypreal) - y = x' - y' ==> (x<y) = (x'<y')"; |
|
1349 by (stac hypreal_less_eq_diff 1); |
|
1350 by (res_inst_tac [("y1", "y")] (hypreal_less_eq_diff RS ssubst) 1); |
|
1351 by (Asm_simp_tac 1); |
|
1352 qed "hypreal_less_eqI"; |
|
1353 |
|
1354 Goal "(x::hypreal) - y = x' - y' ==> (y<=x) = (y'<=x')"; |
|
1355 by (dtac hypreal_less_eqI 1); |
|
1356 by (asm_simp_tac (simpset() addsimps [hypreal_le_def]) 1); |
|
1357 qed "hypreal_le_eqI"; |
|
1358 |
|
1359 Goal "(x::hypreal) - y = x' - y' ==> (x=y) = (x'=y')"; |
|
1360 by Safe_tac; |
|
1361 by (ALLGOALS |
|
1362 (asm_full_simp_tac |
|
1363 (simpset() addsimps [hypreal_eq_diff_eq, hypreal_diff_eq_eq]))); |
|
1364 qed "hypreal_eq_eqI"; |
|
1365 |
|