3 Copyright: 2000 University of Edinburgh |
3 Copyright: 2000 University of Edinburgh |
4 Description: Type "hypreal" is a linear order and also |
4 Description: Type "hypreal" is a linear order and also |
5 satisfies plus_ac0: + is an AC-operator with zero |
5 satisfies plus_ac0: + is an AC-operator with zero |
6 *) |
6 *) |
7 |
7 |
8 HyperOrd = HyperDef + |
8 theory HyperOrd = HyperDef: |
9 |
9 |
10 instance hypreal :: order (hypreal_le_refl,hypreal_le_trans,hypreal_le_anti_sym,hypreal_less_le) |
10 |
11 instance hypreal :: linorder (hypreal_le_linear) |
11 method_setup fuf = {* |
12 |
12 Method.ctxt_args (fn ctxt => |
13 instance hypreal :: plus_ac0(hypreal_add_commute,hypreal_add_assoc,hypreal_add_zero_left) |
13 Method.METHOD (fn facts => |
|
14 fuf_tac (Classical.get_local_claset ctxt, |
|
15 Simplifier.get_local_simpset ctxt) 1)) *} |
|
16 "free ultrafilter tactic" |
|
17 |
|
18 method_setup ultra = {* |
|
19 Method.ctxt_args (fn ctxt => |
|
20 Method.METHOD (fn facts => |
|
21 ultra_tac (Classical.get_local_claset ctxt, |
|
22 Simplifier.get_local_simpset ctxt) 1)) *} |
|
23 "ultrafilter tactic" |
|
24 |
|
25 |
|
26 instance hypreal :: order |
|
27 by (intro_classes, |
|
28 (assumption | |
|
29 rule hypreal_le_refl hypreal_le_trans hypreal_le_anti_sym |
|
30 hypreal_less_le)+) |
|
31 |
|
32 instance hypreal :: linorder |
|
33 by (intro_classes, rule hypreal_le_linear) |
|
34 |
|
35 instance hypreal :: plus_ac0 |
|
36 by (intro_classes, |
|
37 (assumption | |
|
38 rule hypreal_add_commute hypreal_add_assoc hypreal_add_zero_left)+) |
|
39 |
|
40 (**** The simproc abel_cancel ****) |
|
41 |
|
42 (*** Two lemmas needed for the simprocs ***) |
|
43 |
|
44 (*Deletion of other terms in the formula, seeking the -x at the front of z*) |
|
45 lemma hypreal_add_cancel_21: "((x::hypreal) + (y + z) = y + u) = ((x + z) = u)" |
|
46 apply (subst hypreal_add_left_commute) |
|
47 apply (rule hypreal_add_left_cancel) |
|
48 done |
|
49 |
|
50 (*A further rule to deal with the case that |
|
51 everything gets cancelled on the right.*) |
|
52 lemma hypreal_add_cancel_end: "((x::hypreal) + (y + z) = y) = (x = -z)" |
|
53 apply (subst hypreal_add_left_commute) |
|
54 apply (rule_tac t = y in hypreal_add_zero_right [THEN subst], subst hypreal_add_left_cancel) |
|
55 apply (simp (no_asm) add: hypreal_eq_diff_eq [symmetric]) |
|
56 done |
|
57 |
|
58 ML{* |
|
59 val hypreal_add_cancel_21 = thm "hypreal_add_cancel_21"; |
|
60 val hypreal_add_cancel_end = thm "hypreal_add_cancel_end"; |
|
61 |
|
62 structure Hyperreal_Cancel_Data = |
|
63 struct |
|
64 val ss = HOL_ss |
|
65 val eq_reflection = eq_reflection |
|
66 |
|
67 val sg_ref = Sign.self_ref (Theory.sign_of (the_context ())) |
|
68 val T = Type("HyperDef.hypreal",[]) |
|
69 val zero = Const ("0", T) |
|
70 val restrict_to_left = restrict_to_left |
|
71 val add_cancel_21 = hypreal_add_cancel_21 |
|
72 val add_cancel_end = hypreal_add_cancel_end |
|
73 val add_left_cancel = hypreal_add_left_cancel |
|
74 val add_assoc = hypreal_add_assoc |
|
75 val add_commute = hypreal_add_commute |
|
76 val add_left_commute = hypreal_add_left_commute |
|
77 val add_0 = hypreal_add_zero_left |
|
78 val add_0_right = hypreal_add_zero_right |
|
79 |
|
80 val eq_diff_eq = hypreal_eq_diff_eq |
|
81 val eqI_rules = [hypreal_less_eqI, hypreal_eq_eqI, hypreal_le_eqI] |
|
82 fun dest_eqI th = |
|
83 #1 (HOLogic.dest_bin "op =" HOLogic.boolT |
|
84 (HOLogic.dest_Trueprop (concl_of th))) |
|
85 |
|
86 val diff_def = hypreal_diff_def |
|
87 val minus_add_distrib = hypreal_minus_add_distrib |
|
88 val minus_minus = hypreal_minus_minus |
|
89 val minus_0 = hypreal_minus_zero |
|
90 val add_inverses = [hypreal_add_minus, hypreal_add_minus_left] |
|
91 val cancel_simps = [hypreal_add_minus_cancelA, hypreal_minus_add_cancelA] |
|
92 end; |
|
93 |
|
94 structure Hyperreal_Cancel = Abel_Cancel (Hyperreal_Cancel_Data); |
|
95 |
|
96 Addsimprocs [Hyperreal_Cancel.sum_conv, Hyperreal_Cancel.rel_conv]; |
|
97 *} |
|
98 |
|
99 lemma hypreal_minus_diff_eq: "- (z - y) = y - (z::hypreal)" |
|
100 apply (simp (no_asm)) |
|
101 done |
|
102 declare hypreal_minus_diff_eq [simp] |
|
103 |
|
104 |
|
105 lemma hypreal_less_swap_iff: "((x::hypreal) < y) = (-y < -x)" |
|
106 apply (subst hypreal_less_minus_iff) |
|
107 apply (rule_tac x1 = x in hypreal_less_minus_iff [THEN ssubst]) |
|
108 apply (simp (no_asm) add: hypreal_add_commute) |
|
109 done |
|
110 |
|
111 lemma hypreal_gt_zero_iff: |
|
112 "((0::hypreal) < x) = (-x < x)" |
|
113 apply (unfold hypreal_zero_def) |
|
114 apply (rule_tac z = x in eq_Abs_hypreal) |
|
115 apply (auto simp add: hypreal_less hypreal_minus, ultra+) |
|
116 done |
|
117 |
|
118 lemma hypreal_add_less_mono1: "(A::hypreal) < B ==> A + C < B + C" |
|
119 apply (rule_tac z = A in eq_Abs_hypreal) |
|
120 apply (rule_tac z = B in eq_Abs_hypreal) |
|
121 apply (rule_tac z = C in eq_Abs_hypreal) |
|
122 apply (auto intro!: exI simp add: hypreal_less_def hypreal_add, ultra) |
|
123 done |
|
124 |
|
125 lemma hypreal_add_less_mono2: "!!(A::hypreal). A < B ==> C + A < C + B" |
|
126 by (auto intro: hypreal_add_less_mono1 simp add: hypreal_add_commute) |
|
127 |
|
128 lemma hypreal_lt_zero_iff: "(x < (0::hypreal)) = (x < -x)" |
|
129 apply (rule hypreal_minus_zero_less_iff [THEN subst]) |
|
130 apply (subst hypreal_gt_zero_iff) |
|
131 apply (simp (no_asm_use)) |
|
132 done |
|
133 |
|
134 lemma hypreal_add_order: "[| 0 < x; 0 < y |] ==> (0::hypreal) < x + y" |
|
135 apply (unfold hypreal_zero_def) |
|
136 apply (rule_tac z = x in eq_Abs_hypreal) |
|
137 apply (rule_tac z = y in eq_Abs_hypreal) |
|
138 apply (auto simp add: hypreal_less_def hypreal_add) |
|
139 apply (auto intro!: exI simp add: hypreal_less_def hypreal_add, ultra) |
|
140 done |
|
141 |
|
142 lemma hypreal_add_order_le: "[| 0 < x; 0 <= y |] ==> (0::hypreal) < x + y" |
|
143 by (auto dest: sym order_le_imp_less_or_eq intro: hypreal_add_order) |
|
144 |
|
145 lemma hypreal_mult_order: "[| 0 < x; 0 < y |] ==> (0::hypreal) < x * y" |
|
146 apply (unfold hypreal_zero_def) |
|
147 apply (rule_tac z = x in eq_Abs_hypreal) |
|
148 apply (rule_tac z = y in eq_Abs_hypreal) |
|
149 apply (auto intro!: exI simp add: hypreal_less_def hypreal_mult, ultra) |
|
150 apply (auto intro: real_mult_order) |
|
151 done |
|
152 |
|
153 lemma hypreal_mult_less_zero1: "[| x < 0; y < 0 |] ==> (0::hypreal) < x * y" |
|
154 apply (drule hypreal_minus_zero_less_iff [THEN iffD2])+ |
|
155 apply (drule hypreal_mult_order, assumption, simp) |
|
156 done |
|
157 |
|
158 lemma hypreal_mult_less_zero: "[| 0 < x; y < 0 |] ==> x*y < (0::hypreal)" |
|
159 apply (drule hypreal_minus_zero_less_iff [THEN iffD2]) |
|
160 apply (drule hypreal_mult_order, assumption) |
|
161 apply (rule hypreal_minus_zero_less_iff [THEN iffD1], simp) |
|
162 done |
|
163 |
|
164 lemma hypreal_zero_less_one: "0 < (1::hypreal)" |
|
165 apply (unfold hypreal_one_def hypreal_zero_def hypreal_less_def) |
|
166 apply (rule_tac x = "%n. 0" in exI) |
|
167 apply (rule_tac x = "%n. 1" in exI) |
|
168 apply (auto simp add: real_zero_less_one FreeUltrafilterNat_Nat_set) |
|
169 done |
|
170 |
|
171 lemma hypreal_le_add_order: "[| 0 <= x; 0 <= y |] ==> (0::hypreal) <= x + y" |
|
172 apply (drule order_le_imp_less_or_eq)+ |
|
173 apply (auto intro: hypreal_add_order order_less_imp_le) |
|
174 done |
|
175 |
|
176 (*** Monotonicity results ***) |
|
177 |
|
178 lemma hypreal_add_right_cancel_less: "(v+z < w+z) = (v < (w::hypreal))" |
|
179 apply (simp (no_asm)) |
|
180 done |
|
181 |
|
182 lemma hypreal_add_left_cancel_less: "(z+v < z+w) = (v < (w::hypreal))" |
|
183 apply (simp (no_asm)) |
|
184 done |
|
185 |
|
186 declare hypreal_add_right_cancel_less [simp] |
|
187 hypreal_add_left_cancel_less [simp] |
|
188 |
|
189 lemma hypreal_add_right_cancel_le: "(v+z <= w+z) = (v <= (w::hypreal))" |
|
190 apply (simp (no_asm)) |
|
191 done |
|
192 |
|
193 lemma hypreal_add_left_cancel_le: "(z+v <= z+w) = (v <= (w::hypreal))" |
|
194 apply (simp (no_asm)) |
|
195 done |
|
196 |
|
197 declare hypreal_add_right_cancel_le [simp] hypreal_add_left_cancel_le [simp] |
|
198 |
|
199 lemma hypreal_add_less_mono: "[| (z1::hypreal) < y1; z2 < y2 |] ==> z1 + z2 < y1 + y2" |
|
200 apply (drule hypreal_less_minus_iff [THEN iffD1]) |
|
201 apply (drule hypreal_less_minus_iff [THEN iffD1]) |
|
202 apply (drule hypreal_add_order, assumption) |
|
203 apply (erule_tac V = "0 < y2 + - z2" in thin_rl) |
|
204 apply (drule_tac C = "z1 + z2" in hypreal_add_less_mono1) |
|
205 apply (auto simp add: hypreal_minus_add_distrib [symmetric] |
|
206 hypreal_add_ac simp del: hypreal_minus_add_distrib) |
|
207 done |
|
208 |
|
209 lemma hypreal_add_left_le_mono1: "(q1::hypreal) <= q2 ==> x + q1 <= x + q2" |
|
210 apply (drule order_le_imp_less_or_eq) |
|
211 apply (auto intro: order_less_imp_le hypreal_add_less_mono1 simp add: hypreal_add_commute) |
|
212 done |
|
213 |
|
214 lemma hypreal_add_le_mono1: "(q1::hypreal) <= q2 ==> q1 + x <= q2 + x" |
|
215 by (auto dest: hypreal_add_left_le_mono1 simp add: hypreal_add_commute) |
|
216 |
|
217 lemma hypreal_add_le_mono: "[|(i::hypreal)<=j; k<=l |] ==> i + k <= j + l" |
|
218 apply (erule hypreal_add_le_mono1 [THEN order_trans]) |
|
219 apply (simp (no_asm)) |
|
220 done |
|
221 |
|
222 lemma hypreal_add_less_le_mono: "[|(i::hypreal)<j; k<=l |] ==> i + k < j + l" |
|
223 by (auto dest!: order_le_imp_less_or_eq intro: hypreal_add_less_mono1 hypreal_add_less_mono) |
|
224 |
|
225 lemma hypreal_add_le_less_mono: "[|(i::hypreal)<=j; k<l |] ==> i + k < j + l" |
|
226 by (auto dest!: order_le_imp_less_or_eq intro: hypreal_add_less_mono2 hypreal_add_less_mono) |
|
227 |
|
228 lemma hypreal_less_add_right_cancel: "(A::hypreal) + C < B + C ==> A < B" |
|
229 apply (simp (no_asm_use)) |
|
230 done |
|
231 |
|
232 lemma hypreal_less_add_left_cancel: "(C::hypreal) + A < C + B ==> A < B" |
|
233 apply (simp (no_asm_use)) |
|
234 done |
|
235 |
|
236 lemma hypreal_add_zero_less_le_mono: "[|r < x; (0::hypreal) <= y|] ==> r < x + y" |
|
237 by (auto dest: hypreal_add_less_le_mono) |
|
238 |
|
239 lemma hypreal_le_add_right_cancel: "!!(A::hypreal). A + C <= B + C ==> A <= B" |
|
240 apply (drule_tac x = "-C" in hypreal_add_le_mono1) |
|
241 apply (simp add: hypreal_add_assoc) |
|
242 done |
|
243 |
|
244 lemma hypreal_le_add_left_cancel: "!!(A::hypreal). C + A <= C + B ==> A <= B" |
|
245 apply (drule_tac x = "-C" in hypreal_add_left_le_mono1) |
|
246 apply (simp add: hypreal_add_assoc [symmetric]) |
|
247 done |
|
248 |
|
249 lemma hypreal_le_square: "(0::hypreal) <= x*x" |
|
250 apply (rule_tac x = 0 and y = x in hypreal_linear_less2) |
|
251 apply (auto intro: hypreal_mult_order hypreal_mult_less_zero1 order_less_imp_le) |
|
252 done |
|
253 declare hypreal_le_square [simp] |
|
254 |
|
255 lemma hypreal_less_minus_square: "- (x*x) <= (0::hypreal)" |
|
256 apply (unfold hypreal_le_def) |
|
257 apply (auto dest!: hypreal_le_square [THEN order_le_less_trans] |
|
258 simp add: hypreal_minus_zero_less_iff) |
|
259 done |
|
260 declare hypreal_less_minus_square [simp] |
|
261 |
|
262 lemma hypreal_mult_0_less: "(0*x<r)=((0::hypreal)<r)" |
|
263 apply (simp (no_asm)) |
|
264 done |
|
265 |
|
266 lemma hypreal_mult_less_mono1: "[| (0::hypreal) < z; x < y |] ==> x*z < y*z" |
|
267 apply (rotate_tac 1) |
|
268 apply (drule hypreal_less_minus_iff [THEN iffD1]) |
|
269 apply (rule hypreal_less_minus_iff [THEN iffD2]) |
|
270 apply (drule hypreal_mult_order, assumption) |
|
271 apply (simp add: hypreal_add_mult_distrib2 hypreal_mult_commute) |
|
272 done |
|
273 |
|
274 lemma hypreal_mult_less_mono2: "[| (0::hypreal)<z; x<y |] ==> z*x<z*y" |
|
275 apply (simp (no_asm_simp) add: hypreal_mult_commute hypreal_mult_less_mono1) |
|
276 done |
|
277 |
|
278 lemma hypreal_mult_le_less_mono1: "[| (0::hypreal)<=z; x<y |] ==> x*z<=y*z" |
|
279 apply (rule hypreal_less_or_eq_imp_le) |
|
280 apply (drule order_le_imp_less_or_eq) |
|
281 apply (auto intro: hypreal_mult_less_mono1) |
|
282 done |
|
283 |
|
284 lemma hypreal_mult_le_less_mono2: "[| (0::hypreal)<=z; x<y |] ==> z*x<=z*y" |
|
285 apply (simp (no_asm_simp) add: hypreal_mult_commute hypreal_mult_le_less_mono1) |
|
286 done |
|
287 |
|
288 lemma hypreal_mult_less_mono: "[| u<v; x<y; (0::hypreal) < v; 0 < x |] ==> u*x < v* y" |
|
289 apply (erule hypreal_mult_less_mono1 [THEN order_less_trans], assumption) |
|
290 apply (erule hypreal_mult_less_mono2, assumption) |
|
291 done |
|
292 |
|
293 (*UNUSED at present but possibly more useful than hypreal_mult_less_mono*) |
|
294 lemma hypreal_mult_less_mono': "[| x < y; r1 < r2; (0::hypreal) <= r1; 0 <= x|] ==> r1 * x < r2 * y" |
|
295 apply (subgoal_tac "0<r2") |
|
296 prefer 2 apply (blast intro: order_le_less_trans) |
|
297 apply (case_tac "x=0") |
|
298 apply (auto dest!: order_le_imp_less_or_eq intro: hypreal_mult_less_mono hypreal_mult_order) |
|
299 done |
|
300 |
|
301 lemma hypreal_inverse_gt_0: "0 < x ==> 0 < inverse (x::hypreal)" |
|
302 apply (rule ccontr) |
|
303 apply (drule hypreal_leI) |
|
304 apply (frule hypreal_minus_zero_less_iff2 [THEN iffD2]) |
|
305 apply (frule hypreal_not_refl2 [THEN not_sym]) |
|
306 apply (drule hypreal_not_refl2 [THEN not_sym, THEN hypreal_inverse_not_zero]) |
|
307 apply (drule order_le_imp_less_or_eq, safe) |
|
308 apply (drule hypreal_mult_less_zero1, assumption) |
|
309 apply (auto intro: hypreal_zero_less_one [THEN hypreal_less_asym] |
|
310 simp add: hypreal_minus_zero_less_iff) |
|
311 done |
|
312 |
|
313 lemma hypreal_inverse_less_0: "x < 0 ==> inverse (x::hypreal) < 0" |
|
314 apply (frule hypreal_not_refl2) |
|
315 apply (drule hypreal_minus_zero_less_iff [THEN iffD2]) |
|
316 apply (rule hypreal_minus_zero_less_iff [THEN iffD1]) |
|
317 apply (subst hypreal_minus_inverse [symmetric]) |
|
318 apply (auto intro: hypreal_inverse_gt_0) |
|
319 done |
|
320 |
|
321 lemma hypreal_self_le_add_pos: "(x::hypreal)*x <= x*x + y*y" |
|
322 apply (rule_tac z = x in eq_Abs_hypreal) |
|
323 apply (rule_tac z = y in eq_Abs_hypreal) |
|
324 apply (auto simp add: hypreal_mult hypreal_add hypreal_le) |
|
325 done |
|
326 declare hypreal_self_le_add_pos [simp] |
|
327 |
|
328 (*lcp: new lemma unfortunately needed...*) |
|
329 lemma minus_square_le_square: "-(x*x) <= (y*y::real)" |
|
330 apply (rule order_trans) |
|
331 apply (rule_tac [2] real_le_square, auto) |
|
332 done |
|
333 |
|
334 lemma hypreal_self_le_add_pos2: "(x::hypreal)*x <= x*x + y*y + z*z" |
|
335 apply (rule_tac z = x in eq_Abs_hypreal) |
|
336 apply (rule_tac z = y in eq_Abs_hypreal) |
|
337 apply (rule_tac z = z in eq_Abs_hypreal) |
|
338 apply (auto simp add: hypreal_mult hypreal_add hypreal_le minus_square_le_square) |
|
339 done |
|
340 declare hypreal_self_le_add_pos2 [simp] |
|
341 |
|
342 |
|
343 (*---------------------------------------------------------------------------- |
|
344 Existence of infinite hyperreal number |
|
345 ----------------------------------------------------------------------------*) |
|
346 |
|
347 lemma Rep_hypreal_omega: "Rep_hypreal(omega) : hypreal" |
|
348 |
|
349 apply (unfold omega_def) |
|
350 apply (rule Rep_hypreal) |
|
351 done |
|
352 |
|
353 (* existence of infinite number not corresponding to any real number *) |
|
354 (* use assumption that member FreeUltrafilterNat is not finite *) |
|
355 (* a few lemmas first *) |
|
356 |
|
357 lemma lemma_omega_empty_singleton_disj: "{n::nat. x = real n} = {} | |
|
358 (EX y. {n::nat. x = real n} = {y})" |
|
359 by (force dest: inj_real_of_nat [THEN injD]) |
|
360 |
|
361 lemma lemma_finite_omega_set: "finite {n::nat. x = real n}" |
|
362 by (cut_tac x = x in lemma_omega_empty_singleton_disj, auto) |
|
363 |
|
364 lemma not_ex_hypreal_of_real_eq_omega: |
|
365 "~ (EX x. hypreal_of_real x = omega)" |
|
366 apply (unfold omega_def hypreal_of_real_def) |
|
367 apply (auto simp add: real_of_nat_Suc diff_eq_eq [symmetric] lemma_finite_omega_set [THEN FreeUltrafilterNat_finite]) |
|
368 done |
|
369 |
|
370 lemma hypreal_of_real_not_eq_omega: "hypreal_of_real x ~= omega" |
|
371 by (cut_tac not_ex_hypreal_of_real_eq_omega, auto) |
|
372 |
|
373 (* existence of infinitesimal number also not *) |
|
374 (* corresponding to any real number *) |
|
375 |
|
376 lemma real_of_nat_inverse_inj: "inverse (real (x::nat)) = inverse (real y) ==> x = y" |
|
377 by (rule inj_real_of_nat [THEN injD], simp) |
|
378 |
|
379 lemma lemma_epsilon_empty_singleton_disj: "{n::nat. x = inverse(real(Suc n))} = {} | |
|
380 (EX y. {n::nat. x = inverse(real(Suc n))} = {y})" |
|
381 apply (auto simp add: inj_real_of_nat [THEN inj_eq]) |
|
382 done |
|
383 |
|
384 lemma lemma_finite_epsilon_set: "finite {n. x = inverse(real(Suc n))}" |
|
385 by (cut_tac x = x in lemma_epsilon_empty_singleton_disj, auto) |
|
386 |
|
387 lemma not_ex_hypreal_of_real_eq_epsilon: |
|
388 "~ (EX x. hypreal_of_real x = epsilon)" |
|
389 apply (unfold epsilon_def hypreal_of_real_def) |
|
390 apply (auto simp add: lemma_finite_epsilon_set [THEN FreeUltrafilterNat_finite]) |
|
391 done |
|
392 |
|
393 lemma hypreal_of_real_not_eq_epsilon: "hypreal_of_real x ~= epsilon" |
|
394 by (cut_tac not_ex_hypreal_of_real_eq_epsilon, auto) |
|
395 |
|
396 lemma hypreal_epsilon_not_zero: "epsilon ~= 0" |
|
397 by (unfold epsilon_def hypreal_zero_def, auto) |
|
398 |
|
399 lemma hypreal_epsilon_inverse_omega: "epsilon = inverse(omega)" |
|
400 by (simp add: hypreal_inverse omega_def epsilon_def) |
|
401 |
|
402 |
|
403 (* this proof is so much simpler than one for reals!! *) |
|
404 lemma hypreal_inverse_less_swap: "[| 0 < r; r < x |] ==> inverse x < inverse (r::hypreal)" |
|
405 apply (rule_tac z = x in eq_Abs_hypreal) |
|
406 apply (rule_tac z = r in eq_Abs_hypreal) |
|
407 apply (auto simp add: hypreal_inverse hypreal_less hypreal_zero_def, ultra) |
|
408 done |
|
409 |
|
410 lemma hypreal_inverse_less_iff: "[| 0 < r; 0 < x|] ==> (r < x) = (inverse x < inverse (r::hypreal))" |
|
411 apply (auto intro: hypreal_inverse_less_swap) |
|
412 apply (rule_tac t = r in hypreal_inverse_inverse [THEN subst]) |
|
413 apply (rule_tac t = x in hypreal_inverse_inverse [THEN subst]) |
|
414 apply (rule hypreal_inverse_less_swap) |
|
415 apply (auto simp add: hypreal_inverse_gt_0) |
|
416 done |
|
417 |
|
418 lemma hypreal_mult_inverse_less_mono1: "[| 0 < z; x < y |] ==> x * inverse z < y * inverse (z::hypreal)" |
|
419 by (blast intro!: hypreal_mult_less_mono1 hypreal_inverse_gt_0) |
|
420 |
|
421 lemma hypreal_mult_inverse_less_mono2: "[| 0 < z; x < y |] ==> inverse z * x < inverse (z::hypreal) * y" |
|
422 by (blast intro!: hypreal_mult_less_mono2 hypreal_inverse_gt_0) |
|
423 |
|
424 lemma hypreal_less_mult_right_cancel: "[| (0::hypreal) < z; x*z < y*z |] ==> x < y" |
|
425 apply (frule_tac x = "x*z" in hypreal_mult_inverse_less_mono1) |
|
426 apply (drule_tac [2] hypreal_not_refl2 [THEN not_sym]) |
|
427 apply (auto dest!: hypreal_mult_inverse simp add: hypreal_mult_ac) |
|
428 done |
|
429 |
|
430 lemma hypreal_less_mult_left_cancel: "[| (0::hypreal) < z; z*x < z*y |] ==> x < y" |
|
431 by (auto intro: hypreal_less_mult_right_cancel simp add: hypreal_mult_commute) |
|
432 |
|
433 lemma hypreal_mult_less_gt_zero: "[| 0 < r; (0::hypreal) < ra; r < x; ra < y |] ==> r*ra < x*y" |
|
434 apply (frule_tac y = r in order_less_trans) |
|
435 apply (drule_tac [2] z = ra and x = r in hypreal_mult_less_mono1) |
|
436 apply (drule_tac [3] z = x and x = ra in hypreal_mult_less_mono2) |
|
437 apply (auto intro: order_less_trans) |
|
438 done |
|
439 |
|
440 lemma hypreal_mult_le_ge_zero: "[| 0 < r; (0::hypreal) < ra; r <= x; ra <= y |] ==> r*ra <= x*y" |
|
441 apply (drule order_le_imp_less_or_eq)+ |
|
442 apply (rule hypreal_less_or_eq_imp_le) |
|
443 apply (auto intro: hypreal_mult_less_mono1 hypreal_mult_less_mono2 hypreal_mult_less_gt_zero) |
|
444 done |
|
445 |
|
446 (*---------------------------------------------------------------------------- |
|
447 Some convenient biconditionals for products of signs |
|
448 ----------------------------------------------------------------------------*) |
|
449 |
|
450 lemma hypreal_0_less_mult_iff: "((0::hypreal) < x*y) = (0 < x & 0 < y | x < 0 & y < 0)" |
|
451 apply (auto simp add: order_le_less linorder_not_less hypreal_mult_order hypreal_mult_less_zero1) |
|
452 apply (rule_tac [!] ccontr) |
|
453 apply (auto simp add: order_le_less linorder_not_less) |
|
454 apply (erule_tac [!] rev_mp) |
|
455 apply (drule_tac [!] hypreal_mult_less_zero) |
|
456 apply (auto dest: order_less_not_sym simp add: hypreal_mult_commute) |
|
457 done |
|
458 |
|
459 lemma hypreal_0_le_mult_iff: "((0::hypreal) <= x*y) = (0 <= x & 0 <= y | x <= 0 & y <= 0)" |
|
460 by (auto dest: hypreal_mult_zero_disj simp add: order_le_less linorder_not_less hypreal_0_less_mult_iff) |
|
461 |
|
462 lemma hypreal_mult_less_0_iff: "(x*y < (0::hypreal)) = (0 < x & y < 0 | x < 0 & 0 < y)" |
|
463 apply (auto simp add: hypreal_0_le_mult_iff linorder_not_le [symmetric]) |
|
464 apply (auto dest: order_less_not_sym simp add: linorder_not_le) |
|
465 done |
|
466 |
|
467 lemma hypreal_mult_le_0_iff: "(x*y <= (0::hypreal)) = (0 <= x & y <= 0 | x <= 0 & 0 <= y)" |
|
468 by (auto dest: order_less_not_sym simp add: hypreal_0_less_mult_iff linorder_not_less [symmetric]) |
|
469 |
|
470 lemma hypreal_mult_less_zero2: "[| (0::hypreal) < x; y < 0 |] ==> y*x < 0" |
|
471 by (auto simp add: hypreal_mult_commute hypreal_mult_less_zero) |
|
472 |
|
473 |
|
474 ML |
|
475 {* |
|
476 val hypreal_add_cancel_21 = thm"hypreal_add_cancel_21"; |
|
477 val hypreal_add_cancel_end = thm"hypreal_add_cancel_end"; |
|
478 val hypreal_minus_diff_eq = thm"hypreal_minus_diff_eq"; |
|
479 val hypreal_less_swap_iff = thm"hypreal_less_swap_iff"; |
|
480 val hypreal_gt_zero_iff = thm"hypreal_gt_zero_iff"; |
|
481 val hypreal_add_less_mono1 = thm"hypreal_add_less_mono1"; |
|
482 val hypreal_add_less_mono2 = thm"hypreal_add_less_mono2"; |
|
483 val hypreal_lt_zero_iff = thm"hypreal_lt_zero_iff"; |
|
484 val hypreal_add_order = thm"hypreal_add_order"; |
|
485 val hypreal_add_order_le = thm"hypreal_add_order_le"; |
|
486 val hypreal_mult_order = thm"hypreal_mult_order"; |
|
487 val hypreal_mult_less_zero1 = thm"hypreal_mult_less_zero1"; |
|
488 val hypreal_mult_less_zero = thm"hypreal_mult_less_zero"; |
|
489 val hypreal_zero_less_one = thm"hypreal_zero_less_one"; |
|
490 val hypreal_le_add_order = thm"hypreal_le_add_order"; |
|
491 val hypreal_add_right_cancel_less = thm"hypreal_add_right_cancel_less"; |
|
492 val hypreal_add_left_cancel_less = thm"hypreal_add_left_cancel_less"; |
|
493 val hypreal_add_right_cancel_le = thm"hypreal_add_right_cancel_le"; |
|
494 val hypreal_add_left_cancel_le = thm"hypreal_add_left_cancel_le"; |
|
495 val hypreal_add_less_mono = thm"hypreal_add_less_mono"; |
|
496 val hypreal_add_left_le_mono1 = thm"hypreal_add_left_le_mono1"; |
|
497 val hypreal_add_le_mono1 = thm"hypreal_add_le_mono1"; |
|
498 val hypreal_add_le_mono = thm"hypreal_add_le_mono"; |
|
499 val hypreal_add_less_le_mono = thm"hypreal_add_less_le_mono"; |
|
500 val hypreal_add_le_less_mono = thm"hypreal_add_le_less_mono"; |
|
501 val hypreal_less_add_right_cancel = thm"hypreal_less_add_right_cancel"; |
|
502 val hypreal_less_add_left_cancel = thm"hypreal_less_add_left_cancel"; |
|
503 val hypreal_add_zero_less_le_mono = thm"hypreal_add_zero_less_le_mono"; |
|
504 val hypreal_le_add_right_cancel = thm"hypreal_le_add_right_cancel"; |
|
505 val hypreal_le_add_left_cancel = thm"hypreal_le_add_left_cancel"; |
|
506 val hypreal_le_square = thm"hypreal_le_square"; |
|
507 val hypreal_less_minus_square = thm"hypreal_less_minus_square"; |
|
508 val hypreal_mult_0_less = thm"hypreal_mult_0_less"; |
|
509 val hypreal_mult_less_mono1 = thm"hypreal_mult_less_mono1"; |
|
510 val hypreal_mult_less_mono2 = thm"hypreal_mult_less_mono2"; |
|
511 val hypreal_mult_le_less_mono1 = thm"hypreal_mult_le_less_mono1"; |
|
512 val hypreal_mult_le_less_mono2 = thm"hypreal_mult_le_less_mono2"; |
|
513 val hypreal_mult_less_mono = thm"hypreal_mult_less_mono"; |
|
514 val hypreal_mult_less_mono' = thm"hypreal_mult_less_mono'"; |
|
515 val hypreal_inverse_gt_0 = thm"hypreal_inverse_gt_0"; |
|
516 val hypreal_inverse_less_0 = thm"hypreal_inverse_less_0"; |
|
517 val hypreal_self_le_add_pos = thm"hypreal_self_le_add_pos"; |
|
518 val minus_square_le_square = thm"minus_square_le_square"; |
|
519 val hypreal_self_le_add_pos2 = thm"hypreal_self_le_add_pos2"; |
|
520 val Rep_hypreal_omega = thm"Rep_hypreal_omega"; |
|
521 val lemma_omega_empty_singleton_disj = thm"lemma_omega_empty_singleton_disj"; |
|
522 val lemma_finite_omega_set = thm"lemma_finite_omega_set"; |
|
523 val not_ex_hypreal_of_real_eq_omega = thm"not_ex_hypreal_of_real_eq_omega"; |
|
524 val hypreal_of_real_not_eq_omega = thm"hypreal_of_real_not_eq_omega"; |
|
525 val real_of_nat_inverse_inj = thm"real_of_nat_inverse_inj"; |
|
526 val lemma_epsilon_empty_singleton_disj = thm"lemma_epsilon_empty_singleton_disj"; |
|
527 val lemma_finite_epsilon_set = thm"lemma_finite_epsilon_set"; |
|
528 val not_ex_hypreal_of_real_eq_epsilon = thm"not_ex_hypreal_of_real_eq_epsilon"; |
|
529 val hypreal_of_real_not_eq_epsilon = thm"hypreal_of_real_not_eq_epsilon"; |
|
530 val hypreal_epsilon_not_zero = thm"hypreal_epsilon_not_zero"; |
|
531 val hypreal_epsilon_inverse_omega = thm"hypreal_epsilon_inverse_omega"; |
|
532 val hypreal_inverse_less_swap = thm"hypreal_inverse_less_swap"; |
|
533 val hypreal_inverse_less_iff = thm"hypreal_inverse_less_iff"; |
|
534 val hypreal_mult_inverse_less_mono1 = thm"hypreal_mult_inverse_less_mono1"; |
|
535 val hypreal_mult_inverse_less_mono2 = thm"hypreal_mult_inverse_less_mono2"; |
|
536 val hypreal_less_mult_right_cancel = thm"hypreal_less_mult_right_cancel"; |
|
537 val hypreal_less_mult_left_cancel = thm"hypreal_less_mult_left_cancel"; |
|
538 val hypreal_mult_less_gt_zero = thm"hypreal_mult_less_gt_zero"; |
|
539 val hypreal_mult_le_ge_zero = thm"hypreal_mult_le_ge_zero"; |
|
540 val hypreal_0_less_mult_iff = thm"hypreal_0_less_mult_iff"; |
|
541 val hypreal_0_le_mult_iff = thm"hypreal_0_le_mult_iff"; |
|
542 val hypreal_mult_less_0_iff = thm"hypreal_mult_less_0_iff"; |
|
543 val hypreal_mult_le_0_iff = thm"hypreal_mult_le_0_iff"; |
|
544 val hypreal_mult_less_zero2 = thm"hypreal_mult_less_zero2"; |
|
545 *} |
14 |
546 |
15 end |
547 end |