|
1 (* Title: Real/Hyperreal/HyperOrd.ML |
|
2 Author: Jacques D. Fleuriot |
|
3 Copyright: 1998 University of Cambridge |
|
4 2000 University of Edinburgh |
|
5 Description: Type "hypreal" is a linear order and also |
|
6 satisfies plus_ac0: + is an AC-operator with zero |
|
7 *) |
|
8 |
|
9 (**** The simproc abel_cancel ****) |
|
10 |
|
11 (*** Two lemmas needed for the simprocs ***) |
|
12 |
|
13 (*Deletion of other terms in the formula, seeking the -x at the front of z*) |
|
14 Goal "((x::hypreal) + (y + z) = y + u) = ((x + z) = u)"; |
|
15 by (stac hypreal_add_left_commute 1); |
|
16 by (rtac hypreal_add_left_cancel 1); |
|
17 qed "hypreal_add_cancel_21"; |
|
18 |
|
19 (*A further rule to deal with the case that |
|
20 everything gets cancelled on the right.*) |
|
21 Goal "((x::hypreal) + (y + z) = y) = (x = -z)"; |
|
22 by (stac hypreal_add_left_commute 1); |
|
23 by (res_inst_tac [("t", "y")] (hypreal_add_zero_right RS subst) 1 |
|
24 THEN stac hypreal_add_left_cancel 1); |
|
25 by (simp_tac (simpset() addsimps [hypreal_eq_diff_eq RS sym]) 1); |
|
26 qed "hypreal_add_cancel_end"; |
|
27 |
|
28 |
|
29 structure Hyperreal_Cancel_Data = |
|
30 struct |
|
31 val ss = HOL_ss |
|
32 val eq_reflection = eq_reflection |
|
33 |
|
34 val sg_ref = Sign.self_ref (Theory.sign_of (the_context ())) |
|
35 val T = Type("HyperDef.hypreal",[]) |
|
36 val zero = Const ("0", T) |
|
37 val restrict_to_left = restrict_to_left |
|
38 val add_cancel_21 = hypreal_add_cancel_21 |
|
39 val add_cancel_end = hypreal_add_cancel_end |
|
40 val add_left_cancel = hypreal_add_left_cancel |
|
41 val add_assoc = hypreal_add_assoc |
|
42 val add_commute = hypreal_add_commute |
|
43 val add_left_commute = hypreal_add_left_commute |
|
44 val add_0 = hypreal_add_zero_left |
|
45 val add_0_right = hypreal_add_zero_right |
|
46 |
|
47 val eq_diff_eq = hypreal_eq_diff_eq |
|
48 val eqI_rules = [hypreal_less_eqI, hypreal_eq_eqI, hypreal_le_eqI] |
|
49 fun dest_eqI th = |
|
50 #1 (HOLogic.dest_bin "op =" HOLogic.boolT |
|
51 (HOLogic.dest_Trueprop (concl_of th))) |
|
52 |
|
53 val diff_def = hypreal_diff_def |
|
54 val minus_add_distrib = hypreal_minus_add_distrib |
|
55 val minus_minus = hypreal_minus_minus |
|
56 val minus_0 = hypreal_minus_zero |
|
57 val add_inverses = [hypreal_add_minus, hypreal_add_minus_left] |
|
58 val cancel_simps = [hypreal_add_minus_cancelA, hypreal_minus_add_cancelA] |
|
59 end; |
|
60 |
|
61 structure Hyperreal_Cancel = Abel_Cancel (Hyperreal_Cancel_Data); |
|
62 |
|
63 Addsimprocs [Hyperreal_Cancel.sum_conv, Hyperreal_Cancel.rel_conv]; |
|
64 |
|
65 Goal "- (z - y) = y - (z::hypreal)"; |
|
66 by (Simp_tac 1); |
|
67 qed "hypreal_minus_diff_eq"; |
|
68 Addsimps [hypreal_minus_diff_eq]; |
|
69 |
|
70 |
|
71 Goal "((x::hypreal) < y) = (-y < -x)"; |
|
72 by (stac hypreal_less_minus_iff 1); |
|
73 by (res_inst_tac [("x1","x")] (hypreal_less_minus_iff RS ssubst) 1); |
|
74 by (simp_tac (simpset() addsimps [hypreal_add_commute]) 1); |
|
75 qed "hypreal_less_swap_iff"; |
|
76 |
|
77 Goalw [hypreal_zero_def] |
|
78 "((0::hypreal) < x) = (-x < x)"; |
|
79 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); |
|
80 by (auto_tac (claset(), simpset() addsimps [hypreal_less, hypreal_minus])); |
|
81 by (ALLGOALS(Ultra_tac)); |
|
82 qed "hypreal_gt_zero_iff"; |
|
83 |
|
84 Goal "(A::hypreal) < B ==> A + C < B + C"; |
|
85 by (res_inst_tac [("z","A")] eq_Abs_hypreal 1); |
|
86 by (res_inst_tac [("z","B")] eq_Abs_hypreal 1); |
|
87 by (res_inst_tac [("z","C")] eq_Abs_hypreal 1); |
|
88 by (auto_tac (claset() addSIs [exI], |
|
89 simpset() addsimps [hypreal_less_def,hypreal_add])); |
|
90 by (Ultra_tac 1); |
|
91 qed "hypreal_add_less_mono1"; |
|
92 |
|
93 Goal "!!(A::hypreal). A < B ==> C + A < C + B"; |
|
94 by (auto_tac (claset() addIs [hypreal_add_less_mono1], |
|
95 simpset() addsimps [hypreal_add_commute])); |
|
96 qed "hypreal_add_less_mono2"; |
|
97 |
|
98 Goal "(x < (0::hypreal)) = (x < -x)"; |
|
99 by (rtac (hypreal_minus_zero_less_iff RS subst) 1); |
|
100 by (stac hypreal_gt_zero_iff 1); |
|
101 by (Full_simp_tac 1); |
|
102 qed "hypreal_lt_zero_iff"; |
|
103 |
|
104 Goalw [hypreal_le_def] "((0::hypreal) <= x) = (-x <= x)"; |
|
105 by (auto_tac (claset(),simpset() addsimps [hypreal_lt_zero_iff RS sym])); |
|
106 qed "hypreal_ge_zero_iff"; |
|
107 |
|
108 Goalw [hypreal_le_def] "(x <= (0::hypreal)) = (x <= -x)"; |
|
109 by (auto_tac (claset(),simpset() addsimps [hypreal_gt_zero_iff RS sym])); |
|
110 qed "hypreal_le_zero_iff"; |
|
111 |
|
112 Goalw [hypreal_zero_def] |
|
113 "[| 0 < x; 0 < y |] ==> (0::hypreal) < x + y"; |
|
114 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); |
|
115 by (res_inst_tac [("z","y")] eq_Abs_hypreal 1); |
|
116 by (auto_tac (claset(),simpset() addsimps |
|
117 [hypreal_less_def,hypreal_add])); |
|
118 by (auto_tac (claset() addSIs [exI],simpset() addsimps |
|
119 [hypreal_less_def,hypreal_add])); |
|
120 by (ultra_tac (claset() addIs [real_add_order],simpset()) 1); |
|
121 qed "hypreal_add_order"; |
|
122 |
|
123 Goal "[| 0 < x; 0 <= y |] ==> (0::hypreal) < x + y"; |
|
124 by (auto_tac (claset() addDs [sym, order_le_imp_less_or_eq] |
|
125 addIs [hypreal_add_order], |
|
126 simpset())); |
|
127 qed "hypreal_add_order_le"; |
|
128 |
|
129 Goalw [hypreal_zero_def] |
|
130 "[| 0 < x; 0 < y |] ==> (0::hypreal) < x * y"; |
|
131 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); |
|
132 by (res_inst_tac [("z","y")] eq_Abs_hypreal 1); |
|
133 by (auto_tac (claset() addSIs [exI],simpset() addsimps |
|
134 [hypreal_less_def,hypreal_mult])); |
|
135 by (ultra_tac (claset() addIs [rename_numerals real_mult_order], |
|
136 simpset()) 1); |
|
137 qed "hypreal_mult_order"; |
|
138 |
|
139 Goal "[| x < 0; y < 0 |] ==> (0::hypreal) < x * y"; |
|
140 by (REPEAT(dtac (hypreal_minus_zero_less_iff RS iffD2) 1)); |
|
141 by (dtac hypreal_mult_order 1 THEN assume_tac 1); |
|
142 by (Asm_full_simp_tac 1); |
|
143 qed "hypreal_mult_less_zero1"; |
|
144 |
|
145 Goal "[| 0 <= x; 0 <= y |] ==> (0::hypreal) <= x * y"; |
|
146 by (REPEAT(dtac order_le_imp_less_or_eq 1)); |
|
147 by (auto_tac (claset() addIs [hypreal_mult_order, order_less_imp_le], |
|
148 simpset())); |
|
149 qed "hypreal_le_mult_order"; |
|
150 |
|
151 |
|
152 Goal "[| x <= 0; y <= 0 |] ==> (0::hypreal) <= x * y"; |
|
153 by (rtac hypreal_less_or_eq_imp_le 1); |
|
154 by (dtac order_le_imp_less_or_eq 1 THEN etac disjE 1); |
|
155 by Auto_tac; |
|
156 by (dtac order_le_imp_less_or_eq 1); |
|
157 by (auto_tac (claset() addDs [hypreal_mult_less_zero1],simpset())); |
|
158 qed "hypreal_mult_le_zero1"; |
|
159 |
|
160 Goal "[| 0 <= x; y < 0 |] ==> x * y <= (0::hypreal)"; |
|
161 by (rtac hypreal_less_or_eq_imp_le 1); |
|
162 by (dtac order_le_imp_less_or_eq 1 THEN etac disjE 1); |
|
163 by Auto_tac; |
|
164 by (dtac (hypreal_minus_zero_less_iff RS iffD2) 1); |
|
165 by (rtac (hypreal_minus_zero_less_iff RS subst) 1); |
|
166 by (blast_tac (claset() addDs [hypreal_mult_order] |
|
167 addIs [hypreal_minus_mult_eq2 RS ssubst]) 1); |
|
168 qed "hypreal_mult_le_zero"; |
|
169 |
|
170 Goal "[| 0 < x; y < 0 |] ==> x*y < (0::hypreal)"; |
|
171 by (dtac (hypreal_minus_zero_less_iff RS iffD2) 1); |
|
172 by (dtac hypreal_mult_order 1 THEN assume_tac 1); |
|
173 by (rtac (hypreal_minus_zero_less_iff RS iffD1) 1); |
|
174 by (Asm_full_simp_tac 1); |
|
175 qed "hypreal_mult_less_zero"; |
|
176 |
|
177 Goalw [hypreal_one_def,hypreal_zero_def,hypreal_less_def] "0 < 1hr"; |
|
178 by (res_inst_tac [("x","%n. #0")] exI 1); |
|
179 by (res_inst_tac [("x","%n. #1")] exI 1); |
|
180 by (auto_tac (claset(), |
|
181 simpset() addsimps [real_zero_less_one, FreeUltrafilterNat_Nat_set])); |
|
182 qed "hypreal_zero_less_one"; |
|
183 |
|
184 Goal "1hr < 1hr + 1hr"; |
|
185 by (rtac (hypreal_less_minus_iff RS iffD2) 1); |
|
186 by (full_simp_tac (simpset() addsimps [hypreal_zero_less_one, |
|
187 hypreal_add_assoc]) 1); |
|
188 qed "hypreal_one_less_two"; |
|
189 |
|
190 Goal "0 < 1hr + 1hr"; |
|
191 by (rtac ([hypreal_zero_less_one, |
|
192 hypreal_one_less_two] MRS order_less_trans) 1); |
|
193 qed "hypreal_zero_less_two"; |
|
194 |
|
195 Goal "1hr + 1hr ~= 0"; |
|
196 by (rtac (hypreal_zero_less_two RS hypreal_not_refl2 RS not_sym) 1); |
|
197 qed "hypreal_two_not_zero"; |
|
198 Addsimps [hypreal_two_not_zero]; |
|
199 |
|
200 Goal "[| 0 <= x; 0 <= y |] ==> (0::hypreal) <= x + y"; |
|
201 by (REPEAT(dtac order_le_imp_less_or_eq 1)); |
|
202 by (auto_tac (claset() addIs [hypreal_add_order, order_less_imp_le], |
|
203 simpset())); |
|
204 qed "hypreal_le_add_order"; |
|
205 |
|
206 (*** Monotonicity results ***) |
|
207 |
|
208 Goal "(v+z < w+z) = (v < (w::hypreal))"; |
|
209 by (Simp_tac 1); |
|
210 qed "hypreal_add_right_cancel_less"; |
|
211 |
|
212 Goal "(z+v < z+w) = (v < (w::hypreal))"; |
|
213 by (Simp_tac 1); |
|
214 qed "hypreal_add_left_cancel_less"; |
|
215 |
|
216 Addsimps [hypreal_add_right_cancel_less, |
|
217 hypreal_add_left_cancel_less]; |
|
218 |
|
219 Goal "(v+z <= w+z) = (v <= (w::hypreal))"; |
|
220 by (Simp_tac 1); |
|
221 qed "hypreal_add_right_cancel_le"; |
|
222 |
|
223 Goal "(z+v <= z+w) = (v <= (w::hypreal))"; |
|
224 by (Simp_tac 1); |
|
225 qed "hypreal_add_left_cancel_le"; |
|
226 |
|
227 Addsimps [hypreal_add_right_cancel_le, hypreal_add_left_cancel_le]; |
|
228 |
|
229 Goal "[| (z1::hypreal) < y1; z2 < y2 |] ==> z1 + z2 < y1 + y2"; |
|
230 by (dtac (hypreal_less_minus_iff RS iffD1) 1); |
|
231 by (dtac (hypreal_less_minus_iff RS iffD1) 1); |
|
232 by (dtac hypreal_add_order 1 THEN assume_tac 1); |
|
233 by (thin_tac "0 < y2 + - z2" 1); |
|
234 by (dres_inst_tac [("C","z1 + z2")] hypreal_add_less_mono1 1); |
|
235 by (auto_tac (claset(),simpset() addsimps |
|
236 [hypreal_minus_add_distrib RS sym] @ hypreal_add_ac |
|
237 delsimps [hypreal_minus_add_distrib])); |
|
238 qed "hypreal_add_less_mono"; |
|
239 |
|
240 Goal "(q1::hypreal) <= q2 ==> x + q1 <= x + q2"; |
|
241 by (dtac order_le_imp_less_or_eq 1); |
|
242 by (Step_tac 1); |
|
243 by (auto_tac (claset() addSIs [order_less_imp_le,hypreal_add_less_mono1], |
|
244 simpset() addsimps [hypreal_add_commute])); |
|
245 qed "hypreal_add_left_le_mono1"; |
|
246 |
|
247 Goal "(q1::hypreal) <= q2 ==> q1 + x <= q2 + x"; |
|
248 by (auto_tac (claset() addDs [hypreal_add_left_le_mono1], |
|
249 simpset() addsimps [hypreal_add_commute])); |
|
250 qed "hypreal_add_le_mono1"; |
|
251 |
|
252 Goal "[|(i::hypreal)<=j; k<=l |] ==> i + k <= j + l"; |
|
253 by (etac (hypreal_add_le_mono1 RS order_trans) 1); |
|
254 by (Simp_tac 1); |
|
255 qed "hypreal_add_le_mono"; |
|
256 |
|
257 Goal "[|(i::hypreal)<j; k<=l |] ==> i + k < j + l"; |
|
258 by (auto_tac (claset() addSDs [order_le_imp_less_or_eq] |
|
259 addIs [hypreal_add_less_mono1,hypreal_add_less_mono], |
|
260 simpset())); |
|
261 qed "hypreal_add_less_le_mono"; |
|
262 |
|
263 Goal "[|(i::hypreal)<=j; k<l |] ==> i + k < j + l"; |
|
264 by (auto_tac (claset() addSDs [order_le_imp_less_or_eq] |
|
265 addIs [hypreal_add_less_mono2,hypreal_add_less_mono], |
|
266 simpset())); |
|
267 qed "hypreal_add_le_less_mono"; |
|
268 |
|
269 Goal "(A::hypreal) + C < B + C ==> A < B"; |
|
270 by (Full_simp_tac 1); |
|
271 qed "hypreal_less_add_right_cancel"; |
|
272 |
|
273 Goal "(C::hypreal) + A < C + B ==> A < B"; |
|
274 by (Full_simp_tac 1); |
|
275 qed "hypreal_less_add_left_cancel"; |
|
276 |
|
277 Goal "[|r < x; (0::hypreal) <= y|] ==> r < x + y"; |
|
278 by (auto_tac (claset() addDs [hypreal_add_less_le_mono], |
|
279 simpset())); |
|
280 qed "hypreal_add_zero_less_le_mono"; |
|
281 |
|
282 Goal "!!(A::hypreal). A + C <= B + C ==> A <= B"; |
|
283 by (dres_inst_tac [("x","-C")] hypreal_add_le_mono1 1); |
|
284 by (asm_full_simp_tac (simpset() addsimps [hypreal_add_assoc]) 1); |
|
285 qed "hypreal_le_add_right_cancel"; |
|
286 |
|
287 Goal "!!(A::hypreal). C + A <= C + B ==> A <= B"; |
|
288 by (dres_inst_tac [("x","-C")] hypreal_add_left_le_mono1 1); |
|
289 by (asm_full_simp_tac (simpset() addsimps [hypreal_add_assoc RS sym]) 1); |
|
290 qed "hypreal_le_add_left_cancel"; |
|
291 |
|
292 Goal "(0::hypreal) <= x*x"; |
|
293 by (res_inst_tac [("x","0"),("y","x")] hypreal_linear_less2 1); |
|
294 by (auto_tac (claset() addIs [hypreal_mult_order, |
|
295 hypreal_mult_less_zero1,order_less_imp_le], |
|
296 simpset())); |
|
297 qed "hypreal_le_square"; |
|
298 Addsimps [hypreal_le_square]; |
|
299 |
|
300 Goalw [hypreal_le_def] "- (x*x) <= (0::hypreal)"; |
|
301 by (auto_tac (claset() addSDs [hypreal_le_square RS order_le_less_trans], |
|
302 simpset() addsimps [hypreal_minus_zero_less_iff])); |
|
303 qed "hypreal_less_minus_square"; |
|
304 Addsimps [hypreal_less_minus_square]; |
|
305 |
|
306 Goal "(0*x<r)=((0::hypreal)<r)"; |
|
307 by (Simp_tac 1); |
|
308 qed "hypreal_mult_0_less"; |
|
309 |
|
310 Goal "[| (0::hypreal) < z; x < y |] ==> x*z < y*z"; |
|
311 by (rotate_tac 1 1); |
|
312 by (dtac (hypreal_less_minus_iff RS iffD1) 1); |
|
313 by (rtac (hypreal_less_minus_iff RS iffD2) 1); |
|
314 by (dtac hypreal_mult_order 1 THEN assume_tac 1); |
|
315 by (asm_full_simp_tac (simpset() addsimps [hypreal_add_mult_distrib2, |
|
316 hypreal_mult_commute ]) 1); |
|
317 qed "hypreal_mult_less_mono1"; |
|
318 |
|
319 Goal "[| (0::hypreal)<z; x<y |] ==> z*x<z*y"; |
|
320 by (asm_simp_tac (simpset() addsimps [hypreal_mult_commute,hypreal_mult_less_mono1]) 1); |
|
321 qed "hypreal_mult_less_mono2"; |
|
322 |
|
323 Goal "[| (0::hypreal)<=z; x<y |] ==> x*z<=y*z"; |
|
324 by (EVERY1 [rtac hypreal_less_or_eq_imp_le, dtac order_le_imp_less_or_eq]); |
|
325 by (auto_tac (claset() addIs [hypreal_mult_less_mono1],simpset())); |
|
326 qed "hypreal_mult_le_less_mono1"; |
|
327 |
|
328 Goal "[| (0::hypreal)<=z; x<y |] ==> z*x<=z*y"; |
|
329 by (asm_simp_tac (simpset() addsimps [hypreal_mult_commute, |
|
330 hypreal_mult_le_less_mono1]) 1); |
|
331 qed "hypreal_mult_le_less_mono2"; |
|
332 |
|
333 Goal "[| (0::hypreal)<=z; x<=y |] ==> z*x<=z*y"; |
|
334 by (dres_inst_tac [("x","x")] order_le_imp_less_or_eq 1); |
|
335 by (auto_tac (claset() addIs [hypreal_mult_le_less_mono2], simpset())); |
|
336 qed "hypreal_mult_le_le_mono1"; |
|
337 |
|
338 val prem1::prem2::prem3::rest = goal thy |
|
339 "[| (0::hypreal)<y; x<r; y*r<t*s |] ==> y*x<t*s"; |
|
340 by (rtac ([[prem1,prem2] MRS hypreal_mult_less_mono2, prem3] |
|
341 MRS order_less_trans) 1); |
|
342 qed "hypreal_mult_less_trans"; |
|
343 |
|
344 Goal "[| 0<=y; x<r; y*r<t*s; (0::hypreal)<t*s|] ==> y*x<t*s"; |
|
345 by (dtac order_le_imp_less_or_eq 1); |
|
346 by (fast_tac (HOL_cs addEs [hypreal_mult_0_less RS iffD2, |
|
347 hypreal_mult_less_trans]) 1); |
|
348 qed "hypreal_mult_le_less_trans"; |
|
349 |
|
350 Goal "[| 0 <= y; x <= r; y*r < t*s; (0::hypreal) < t*s|] ==> y*x < t*s"; |
|
351 by (dres_inst_tac [("x","x")] order_le_imp_less_or_eq 1); |
|
352 by (fast_tac (claset() addIs [hypreal_mult_le_less_trans]) 1); |
|
353 qed "hypreal_mult_le_le_trans"; |
|
354 |
|
355 Goal "[| u<v; x<y; (0::hypreal) < v; 0 < x |] ==> u*x < v* y"; |
|
356 by (etac (hypreal_mult_less_mono1 RS order_less_trans) 1); |
|
357 by (assume_tac 1); |
|
358 by (etac hypreal_mult_less_mono2 1); |
|
359 by (assume_tac 1); |
|
360 qed "hypreal_mult_less_mono"; |
|
361 |
|
362 (*UNUSED at present but possibly more useful than hypreal_mult_less_mono*) |
|
363 Goal "[| x < y; r1 < r2; (0::hypreal) <= r1; 0 <= x|] ==> r1 * x < r2 * y"; |
|
364 by (subgoal_tac "0<r2" 1); |
|
365 by (blast_tac (claset() addIs [order_le_less_trans]) 2); |
|
366 by (case_tac "x=0" 1); |
|
367 by (auto_tac (claset() addSDs [order_le_imp_less_or_eq] |
|
368 addIs [hypreal_mult_less_mono, hypreal_mult_order], |
|
369 simpset())); |
|
370 qed "hypreal_mult_less_mono'"; |
|
371 |
|
372 Goal "0 < x ==> 0 < inverse (x::hypreal)"; |
|
373 by (EVERY1[rtac ccontr, dtac hypreal_leI]); |
|
374 by (forward_tac [hypreal_minus_zero_less_iff2 RS iffD2] 1); |
|
375 by (forward_tac [hypreal_not_refl2 RS not_sym] 1); |
|
376 by (dtac (hypreal_not_refl2 RS not_sym RS hypreal_inverse_not_zero) 1); |
|
377 by (EVERY1[dtac order_le_imp_less_or_eq, Step_tac]); |
|
378 by (dtac hypreal_mult_less_zero1 1 THEN assume_tac 1); |
|
379 by (auto_tac (claset() addIs [hypreal_zero_less_one RS hypreal_less_asym], |
|
380 simpset() addsimps [hypreal_minus_zero_less_iff])); |
|
381 qed "hypreal_inverse_gt_zero"; |
|
382 |
|
383 Goal "x < 0 ==> inverse (x::hypreal) < 0"; |
|
384 by (ftac hypreal_not_refl2 1); |
|
385 by (dtac (hypreal_minus_zero_less_iff RS iffD2) 1); |
|
386 by (rtac (hypreal_minus_zero_less_iff RS iffD1) 1); |
|
387 by (stac (hypreal_minus_inverse RS sym) 1); |
|
388 by (auto_tac (claset() addIs [hypreal_inverse_gt_zero], simpset())); |
|
389 qed "hypreal_inverse_less_zero"; |
|
390 |
|
391 Goal "[| 0 <= x; 0 <= y |] ==> (x+y = 0) = (x = 0 & y = (0::hypreal))"; |
|
392 by (auto_tac (claset() addIs [order_antisym], simpset())); |
|
393 qed "hypreal_add_nonneg_eq_0_iff"; |
|
394 |
|
395 Goal "(x*y = 0) = (x = 0 | y = (0::hypreal))"; |
|
396 by Auto_tac; |
|
397 by (blast_tac (claset() addDs [hypreal_mult_zero_disj]) 1); |
|
398 qed "hypreal_mult_is_0"; |
|
399 |
|
400 Goal "(x*x + y*y = 0) = (x = 0 & y = (0::hypreal))"; |
|
401 by (simp_tac (HOL_ss addsimps [hypreal_le_square, hypreal_add_nonneg_eq_0_iff, |
|
402 hypreal_mult_is_0]) 1); |
|
403 qed "hypreal_squares_add_zero_iff"; |
|
404 Addsimps [hypreal_squares_add_zero_iff]; |
|
405 |
|
406 Goal "(x*x + y*y + z*z = 0) = (x = 0 & y = 0 & z = (0::hypreal))"; |
|
407 by (simp_tac (HOL_ss addsimps [hypreal_le_square, hypreal_le_add_order, |
|
408 hypreal_add_nonneg_eq_0_iff, hypreal_mult_is_0]) 1); |
|
409 qed "hypreal_three_squares_add_zero_iff"; |
|
410 |
|
411 Goal "(x::hypreal)*x <= x*x + y*y"; |
|
412 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); |
|
413 by (res_inst_tac [("z","y")] eq_Abs_hypreal 1); |
|
414 by (auto_tac (claset(), |
|
415 simpset() addsimps [hypreal_mult,hypreal_add,hypreal_le])); |
|
416 qed "hypreal_self_le_add_pos"; |
|
417 Addsimps [hypreal_self_le_add_pos]; |
|
418 |
|
419 (*lcp: new lemma unfortunately needed...*) |
|
420 Goal "-(x*x) <= (y*y::real)"; |
|
421 by (rtac order_trans 1); |
|
422 by (rtac real_le_square 2); |
|
423 by Auto_tac; |
|
424 qed "minus_square_le_square"; |
|
425 |
|
426 Goal "(x::hypreal)*x <= x*x + y*y + z*z"; |
|
427 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); |
|
428 by (res_inst_tac [("z","y")] eq_Abs_hypreal 1); |
|
429 by (res_inst_tac [("z","z")] eq_Abs_hypreal 1); |
|
430 by (auto_tac (claset(), |
|
431 simpset() addsimps [hypreal_mult, hypreal_add, hypreal_le, |
|
432 minus_square_le_square])); |
|
433 qed "hypreal_self_le_add_pos2"; |
|
434 Addsimps [hypreal_self_le_add_pos2]; |
|
435 |
|
436 |
|
437 (*---------------------------------------------------------------------------- |
|
438 Embedding of the naturals in the hyperreals |
|
439 ----------------------------------------------------------------------------*) |
|
440 Goalw [hypreal_of_posnat_def] "hypreal_of_posnat 0 = 1hr"; |
|
441 by (full_simp_tac (simpset() addsimps |
|
442 [pnat_one_iff RS sym,real_of_preal_def]) 1); |
|
443 by (fold_tac [real_one_def]); |
|
444 by (simp_tac (simpset() addsimps [hypreal_of_real_one]) 1); |
|
445 qed "hypreal_of_posnat_one"; |
|
446 |
|
447 Goalw [hypreal_of_posnat_def] "hypreal_of_posnat 1 = 1hr + 1hr"; |
|
448 by (full_simp_tac (simpset() addsimps |
|
449 [real_of_preal_def, |
|
450 rename_numerals (real_one_def RS meta_eq_to_obj_eq), |
|
451 hypreal_add,hypreal_of_real_def,pnat_two_eq, |
|
452 hypreal_one_def, real_add, |
|
453 prat_of_pnat_add RS sym, preal_of_prat_add RS sym] @ |
|
454 pnat_add_ac) 1); |
|
455 qed "hypreal_of_posnat_two"; |
|
456 |
|
457 (*FIXME: delete this and all posnat*) |
|
458 Goalw [hypreal_of_posnat_def] |
|
459 "hypreal_of_posnat n1 + hypreal_of_posnat n2 = \ |
|
460 \ hypreal_of_posnat (n1 + n2) + 1hr"; |
|
461 by (full_simp_tac (HOL_ss addsimps [hypreal_of_posnat_one RS sym, |
|
462 hypreal_of_real_add RS sym,hypreal_of_posnat_def,real_of_preal_add RS sym, |
|
463 preal_of_prat_add RS sym,prat_of_pnat_add RS sym,pnat_of_nat_add]) 1); |
|
464 qed "hypreal_of_posnat_add"; |
|
465 |
|
466 Goal "hypreal_of_posnat (n + 1) = hypreal_of_posnat n + 1hr"; |
|
467 by (res_inst_tac [("x1","1hr")] (hypreal_add_right_cancel RS iffD1) 1); |
|
468 by (rtac (hypreal_of_posnat_add RS subst) 1); |
|
469 by (full_simp_tac (simpset() addsimps [hypreal_of_posnat_two,hypreal_add_assoc]) 1); |
|
470 qed "hypreal_of_posnat_add_one"; |
|
471 |
|
472 Goalw [real_of_posnat_def,hypreal_of_posnat_def] |
|
473 "hypreal_of_posnat n = hypreal_of_real (real_of_posnat n)"; |
|
474 by (rtac refl 1); |
|
475 qed "hypreal_of_real_of_posnat"; |
|
476 |
|
477 Goalw [hypreal_of_posnat_def] |
|
478 "(n < m) = (hypreal_of_posnat n < hypreal_of_posnat m)"; |
|
479 by Auto_tac; |
|
480 qed "hypreal_of_posnat_less_iff"; |
|
481 |
|
482 Addsimps [hypreal_of_posnat_less_iff RS sym]; |
|
483 (*--------------------------------------------------------------------------------- |
|
484 Existence of infinite hyperreal number |
|
485 ---------------------------------------------------------------------------------*) |
|
486 |
|
487 Goal "hyprel^^{%n::nat. real_of_posnat n} : hypreal"; |
|
488 by Auto_tac; |
|
489 qed "hypreal_omega"; |
|
490 |
|
491 Goalw [omega_def] "Rep_hypreal(whr) : hypreal"; |
|
492 by (rtac Rep_hypreal 1); |
|
493 qed "Rep_hypreal_omega"; |
|
494 |
|
495 (* existence of infinite number not corresponding to any real number *) |
|
496 (* use assumption that member FreeUltrafilterNat is not finite *) |
|
497 (* a few lemmas first *) |
|
498 |
|
499 Goal "{n::nat. x = real_of_posnat n} = {} | \ |
|
500 \ (EX y. {n::nat. x = real_of_posnat n} = {y})"; |
|
501 by (auto_tac (claset() addDs [inj_real_of_posnat RS injD],simpset())); |
|
502 qed "lemma_omega_empty_singleton_disj"; |
|
503 |
|
504 Goal "finite {n::nat. x = real_of_posnat n}"; |
|
505 by (cut_inst_tac [("x","x")] lemma_omega_empty_singleton_disj 1); |
|
506 by Auto_tac; |
|
507 qed "lemma_finite_omega_set"; |
|
508 |
|
509 Goalw [omega_def,hypreal_of_real_def] |
|
510 "~ (EX x. hypreal_of_real x = whr)"; |
|
511 by (auto_tac (claset(),simpset() addsimps [lemma_finite_omega_set |
|
512 RS FreeUltrafilterNat_finite])); |
|
513 qed "not_ex_hypreal_of_real_eq_omega"; |
|
514 |
|
515 Goal "hypreal_of_real x ~= whr"; |
|
516 by (cut_facts_tac [not_ex_hypreal_of_real_eq_omega] 1); |
|
517 by Auto_tac; |
|
518 qed "hypreal_of_real_not_eq_omega"; |
|
519 |
|
520 (* existence of infinitesimal number also not *) |
|
521 (* corresponding to any real number *) |
|
522 |
|
523 Goal "{n::nat. x = inverse(real_of_posnat n)} = {} | \ |
|
524 \ (EX y. {n::nat. x = inverse(real_of_posnat n)} = {y})"; |
|
525 by (Step_tac 1 THEN Step_tac 1); |
|
526 by (auto_tac (claset() addIs [real_of_posnat_inverse_inj],simpset())); |
|
527 qed "lemma_epsilon_empty_singleton_disj"; |
|
528 |
|
529 Goal "finite {n::nat. x = inverse(real_of_posnat n)}"; |
|
530 by (cut_inst_tac [("x","x")] lemma_epsilon_empty_singleton_disj 1); |
|
531 by Auto_tac; |
|
532 qed "lemma_finite_epsilon_set"; |
|
533 |
|
534 Goalw [epsilon_def,hypreal_of_real_def] |
|
535 "~ (EX x. hypreal_of_real x = ehr)"; |
|
536 by (auto_tac (claset(),simpset() addsimps [lemma_finite_epsilon_set |
|
537 RS FreeUltrafilterNat_finite])); |
|
538 qed "not_ex_hypreal_of_real_eq_epsilon"; |
|
539 |
|
540 Goal "hypreal_of_real x ~= ehr"; |
|
541 by (cut_facts_tac [not_ex_hypreal_of_real_eq_epsilon] 1); |
|
542 by Auto_tac; |
|
543 qed "hypreal_of_real_not_eq_epsilon"; |
|
544 |
|
545 Goalw [epsilon_def,hypreal_zero_def] "ehr ~= 0"; |
|
546 by (auto_tac (claset(), |
|
547 simpset() addsimps [rename_numerals real_of_posnat_not_eq_zero])); |
|
548 qed "hypreal_epsilon_not_zero"; |
|
549 |
|
550 Addsimps [rename_numerals real_of_posnat_not_eq_zero]; |
|
551 Goalw [omega_def,hypreal_zero_def] "whr ~= 0"; |
|
552 by (Simp_tac 1); |
|
553 qed "hypreal_omega_not_zero"; |
|
554 |
|
555 Goal "ehr = inverse(whr)"; |
|
556 by (asm_full_simp_tac (simpset() addsimps |
|
557 [hypreal_inverse, omega_def, epsilon_def]) 1); |
|
558 qed "hypreal_epsilon_inverse_omega"; |
|
559 |
|
560 (*---------------------------------------------------------------- |
|
561 Another embedding of the naturals in the |
|
562 hyperreals (see hypreal_of_posnat) |
|
563 ----------------------------------------------------------------*) |
|
564 Goalw [hypreal_of_nat_def] "hypreal_of_nat 0 = 0"; |
|
565 by (full_simp_tac (simpset() addsimps [hypreal_of_posnat_one]) 1); |
|
566 qed "hypreal_of_nat_zero"; |
|
567 |
|
568 Goalw [hypreal_of_nat_def] "hypreal_of_nat 1 = 1hr"; |
|
569 by (full_simp_tac (simpset() addsimps [hypreal_of_posnat_two, |
|
570 hypreal_add_assoc]) 1); |
|
571 qed "hypreal_of_nat_one"; |
|
572 |
|
573 Goalw [hypreal_of_nat_def] |
|
574 "hypreal_of_nat n1 + hypreal_of_nat n2 = hypreal_of_nat (n1 + n2)"; |
|
575 by (full_simp_tac (simpset() addsimps hypreal_add_ac) 1); |
|
576 by (simp_tac (simpset() addsimps [hypreal_of_posnat_add, |
|
577 hypreal_add_assoc RS sym]) 1); |
|
578 qed "hypreal_of_nat_add"; |
|
579 |
|
580 Goal "hypreal_of_nat 2 = 1hr + 1hr"; |
|
581 by (simp_tac (simpset() addsimps [hypreal_of_nat_one |
|
582 RS sym,hypreal_of_nat_add]) 1); |
|
583 qed "hypreal_of_nat_two"; |
|
584 |
|
585 Goalw [hypreal_of_nat_def] |
|
586 "(n < m) = (hypreal_of_nat n < hypreal_of_nat m)"; |
|
587 by (auto_tac (claset() addIs [hypreal_add_less_mono1],simpset())); |
|
588 qed "hypreal_of_nat_less_iff"; |
|
589 Addsimps [hypreal_of_nat_less_iff RS sym]; |
|
590 |
|
591 (*------------------------------------------------------------*) |
|
592 (* naturals embedded in hyperreals *) |
|
593 (* is a hyperreal c.f. NS extension *) |
|
594 (*------------------------------------------------------------*) |
|
595 |
|
596 Goalw [hypreal_of_nat_def,real_of_nat_def] |
|
597 "hypreal_of_nat m = Abs_hypreal(hyprel^^{%n. real_of_nat m})"; |
|
598 by (auto_tac (claset(),simpset() addsimps [hypreal_of_real_def, |
|
599 hypreal_of_real_of_posnat,hypreal_minus,hypreal_one_def,hypreal_add])); |
|
600 qed "hypreal_of_nat_iff"; |
|
601 |
|
602 Goal "inj hypreal_of_nat"; |
|
603 by (rtac injI 1); |
|
604 by (auto_tac (claset() addSDs [FreeUltrafilterNat_P], |
|
605 simpset() addsimps [split_if_mem1, hypreal_of_nat_iff, |
|
606 real_add_right_cancel,inj_real_of_nat RS injD])); |
|
607 qed "inj_hypreal_of_nat"; |
|
608 |
|
609 Goalw [hypreal_of_nat_def,hypreal_of_real_def,hypreal_of_posnat_def, |
|
610 real_of_posnat_def,hypreal_one_def,real_of_nat_def] |
|
611 "hypreal_of_nat n = hypreal_of_real (real_of_nat n)"; |
|
612 by (simp_tac (simpset() addsimps [hypreal_add,hypreal_minus]) 1); |
|
613 qed "hypreal_of_nat_real_of_nat"; |
|
614 |
|
615 Goal "hypreal_of_posnat (Suc n) = hypreal_of_posnat n + 1hr"; |
|
616 by (stac (hypreal_of_posnat_add_one RS sym) 1); |
|
617 by (Simp_tac 1); |
|
618 qed "hypreal_of_posnat_Suc"; |
|
619 |
|
620 Goalw [hypreal_of_nat_def] |
|
621 "hypreal_of_nat (Suc n) = hypreal_of_nat n + 1hr"; |
|
622 by (simp_tac (simpset() addsimps [hypreal_of_posnat_Suc] @ hypreal_add_ac) 1); |
|
623 qed "hypreal_of_nat_Suc"; |
|
624 |
|
625 (* this proof is so much simpler than one for reals!! *) |
|
626 Goal "[| 0 < r; r < x |] ==> inverse x < inverse (r::hypreal)"; |
|
627 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); |
|
628 by (res_inst_tac [("z","r")] eq_Abs_hypreal 1); |
|
629 by (auto_tac (claset(),simpset() addsimps [hypreal_inverse, |
|
630 hypreal_less,hypreal_zero_def])); |
|
631 by (ultra_tac (claset() addIs [real_inverse_less_swap],simpset()) 1); |
|
632 qed "hypreal_inverse_less_swap"; |
|
633 |
|
634 Goal "[| 0 < r; 0 < x|] ==> (r < x) = (inverse x < inverse (r::hypreal))"; |
|
635 by (auto_tac (claset() addIs [hypreal_inverse_less_swap],simpset())); |
|
636 by (res_inst_tac [("t","r")] (hypreal_inverse_inverse RS subst) 1); |
|
637 by (res_inst_tac [("t","x")] (hypreal_inverse_inverse RS subst) 1); |
|
638 by (rtac hypreal_inverse_less_swap 1); |
|
639 by (auto_tac (claset(), simpset() addsimps [hypreal_inverse_gt_zero])); |
|
640 qed "hypreal_inverse_less_iff"; |
|
641 |
|
642 Goal "[| 0 < z; x < y |] ==> x * inverse z < y * inverse (z::hypreal)"; |
|
643 by (blast_tac (claset() addSIs [hypreal_mult_less_mono1, |
|
644 hypreal_inverse_gt_zero]) 1); |
|
645 qed "hypreal_mult_inverse_less_mono1"; |
|
646 |
|
647 Goal "[| 0 < z; x < y |] ==> inverse z * x < inverse (z::hypreal) * y"; |
|
648 by (blast_tac (claset() addSIs [hypreal_mult_less_mono2, |
|
649 hypreal_inverse_gt_zero]) 1); |
|
650 qed "hypreal_mult_inverse_less_mono2"; |
|
651 |
|
652 Goal "[| (0::hypreal) < z; x*z < y*z |] ==> x < y"; |
|
653 by (forw_inst_tac [("x","x*z")] hypreal_mult_inverse_less_mono1 1); |
|
654 by (dtac (hypreal_not_refl2 RS not_sym) 2); |
|
655 by (auto_tac (claset() addSDs [hypreal_mult_inverse], |
|
656 simpset() addsimps hypreal_mult_ac)); |
|
657 qed "hypreal_less_mult_right_cancel"; |
|
658 |
|
659 Goal "[| (0::hypreal) < z; z*x < z*y |] ==> x < y"; |
|
660 by (auto_tac (claset() addIs [hypreal_less_mult_right_cancel], |
|
661 simpset() addsimps [hypreal_mult_commute])); |
|
662 qed "hypreal_less_mult_left_cancel"; |
|
663 |
|
664 Goal "[| 0 < r; (0::hypreal) < ra; r < x; ra < y |] ==> r*ra < x*y"; |
|
665 by (forw_inst_tac [("y","r")] order_less_trans 1); |
|
666 by (dres_inst_tac [("z","ra"),("x","r")] hypreal_mult_less_mono1 2); |
|
667 by (dres_inst_tac [("z","x"),("x","ra")] hypreal_mult_less_mono2 3); |
|
668 by (auto_tac (claset() addIs [order_less_trans], simpset())); |
|
669 qed "hypreal_mult_less_gt_zero"; |
|
670 |
|
671 Goal "[| 0 < r; (0::hypreal) < ra; r <= x; ra <= y |] ==> r*ra <= x*y"; |
|
672 by (REPEAT(dtac order_le_imp_less_or_eq 1)); |
|
673 by (rtac hypreal_less_or_eq_imp_le 1); |
|
674 by (auto_tac (claset() addIs [hypreal_mult_less_mono1, |
|
675 hypreal_mult_less_mono2,hypreal_mult_less_gt_zero], |
|
676 simpset())); |
|
677 qed "hypreal_mult_le_ge_zero"; |
|
678 |
|
679 (*---------------------------------------------------------------------------- |
|
680 Some convenient biconditionals for products of signs |
|
681 ----------------------------------------------------------------------------*) |
|
682 |
|
683 Goal "((0::hypreal) < x*y) = (0 < x & 0 < y | x < 0 & y < 0)"; |
|
684 by (auto_tac (claset(), |
|
685 simpset() addsimps [order_le_less, linorder_not_less, |
|
686 hypreal_mult_order, hypreal_mult_less_zero1])); |
|
687 by (ALLGOALS (rtac ccontr)); |
|
688 by (auto_tac (claset(), |
|
689 simpset() addsimps [order_le_less, linorder_not_less])); |
|
690 by (ALLGOALS (etac rev_mp)); |
|
691 by (ALLGOALS (dtac hypreal_mult_less_zero THEN' assume_tac)); |
|
692 by (auto_tac (claset() addDs [order_less_not_sym], |
|
693 simpset() addsimps [hypreal_mult_commute])); |
|
694 qed "hypreal_zero_less_mult_iff"; |
|
695 |
|
696 Goal "((0::hypreal) <= x*y) = (0 <= x & 0 <= y | x <= 0 & y <= 0)"; |
|
697 by (auto_tac (claset() addDs [hypreal_mult_zero_disj], |
|
698 simpset() addsimps [order_le_less, linorder_not_less, |
|
699 hypreal_zero_less_mult_iff])); |
|
700 qed "hypreal_zero_le_mult_iff"; |
|
701 |
|
702 Goal "(x*y < (0::hypreal)) = (0 < x & y < 0 | x < 0 & 0 < y)"; |
|
703 by (auto_tac (claset(), |
|
704 simpset() addsimps [hypreal_zero_le_mult_iff, |
|
705 linorder_not_le RS sym])); |
|
706 by (auto_tac (claset() addDs [order_less_not_sym], |
|
707 simpset() addsimps [linorder_not_le])); |
|
708 qed "hypreal_mult_less_zero_iff"; |
|
709 |
|
710 Goal "(x*y <= (0::hypreal)) = (0 <= x & y <= 0 | x <= 0 & 0 <= y)"; |
|
711 by (auto_tac (claset() addDs [order_less_not_sym], |
|
712 simpset() addsimps [hypreal_zero_less_mult_iff, |
|
713 linorder_not_less RS sym])); |
|
714 qed "hypreal_mult_le_zero_iff"; |
|
715 |