1 (* Title: Real/Hyperreal/HyperOrd.thy
2 Author: Jacques D. Fleuriot
3 Copyright: 2000 University of Edinburgh
4 Description: Type "hypreal" is a linear order and also
5 satisfies plus_ac0: + is an AC-operator with zero
8 theory HyperOrd = HyperDef:
12 Method.ctxt_args (fn ctxt =>
13 Method.METHOD (fn facts =>
14 fuf_tac (Classical.get_local_claset ctxt,
15 Simplifier.get_local_simpset ctxt) 1)) *}
16 "free ultrafilter tactic"
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)) *}
26 instance hypreal :: order
29 rule hypreal_le_refl hypreal_le_trans hypreal_le_anti_sym
32 instance hypreal :: linorder
33 by (intro_classes, rule hypreal_le_linear)
35 instance hypreal :: plus_ac0
38 rule hypreal_add_commute hypreal_add_assoc hypreal_add_zero_left)+)
40 (**** The simproc abel_cancel ****)
42 (*** Two lemmas needed for the simprocs ***)
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)
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])
59 val hypreal_add_cancel_21 = thm "hypreal_add_cancel_21";
60 val hypreal_add_cancel_end = thm "hypreal_add_cancel_end";
62 structure Hyperreal_Cancel_Data =
65 val eq_reflection = eq_reflection
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
80 val eq_diff_eq = hypreal_eq_diff_eq
81 val eqI_rules = [hypreal_less_eqI, hypreal_eq_eqI, hypreal_le_eqI]
83 #1 (HOLogic.dest_bin "op =" HOLogic.boolT
84 (HOLogic.dest_Trueprop (concl_of th)))
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]
94 structure Hyperreal_Cancel = Abel_Cancel (Hyperreal_Cancel_Data);
96 Addsimprocs [Hyperreal_Cancel.sum_conv, Hyperreal_Cancel.rel_conv];
99 lemma hypreal_minus_diff_eq: "- (z - y) = y - (z::hypreal)"
100 apply (simp (no_asm))
102 declare hypreal_minus_diff_eq [simp]
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)
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+)
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)
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)
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))
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)
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)
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)
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)
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)
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)
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)
176 (*** Monotonicity results ***)
178 lemma hypreal_add_right_cancel_less: "(v+z < w+z) = (v < (w::hypreal))"
179 apply (simp (no_asm))
182 lemma hypreal_add_left_cancel_less: "(z+v < z+w) = (v < (w::hypreal))"
183 apply (simp (no_asm))
186 declare hypreal_add_right_cancel_less [simp]
187 hypreal_add_left_cancel_less [simp]
189 lemma hypreal_add_right_cancel_le: "(v+z <= w+z) = (v <= (w::hypreal))"
190 apply (simp (no_asm))
193 lemma hypreal_add_left_cancel_le: "(z+v <= z+w) = (v <= (w::hypreal))"
194 apply (simp (no_asm))
197 declare hypreal_add_right_cancel_le [simp] hypreal_add_left_cancel_le [simp]
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)
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)
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)
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))
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)
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)
228 lemma hypreal_less_add_right_cancel: "(A::hypreal) + C < B + C ==> A < B"
229 apply (simp (no_asm_use))
232 lemma hypreal_less_add_left_cancel: "(C::hypreal) + A < C + B ==> A < B"
233 apply (simp (no_asm_use))
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)
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)
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])
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)
253 declare hypreal_le_square [simp]
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)
260 declare hypreal_less_minus_square [simp]
262 lemma hypreal_mult_0_less: "(0*x<r)=((0::hypreal)<r)"
263 apply (simp (no_asm))
266 lemma hypreal_mult_less_mono1: "[| (0::hypreal) < z; x < y |] ==> x*z < y*z"
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)
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)
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)
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)
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)
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)
301 lemma hypreal_inverse_gt_0: "0 < x ==> 0 < inverse (x::hypreal)"
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)
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)
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)
326 declare hypreal_self_le_add_pos [simp]
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)
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)
340 declare hypreal_self_le_add_pos2 [simp]
343 (*----------------------------------------------------------------------------
344 Existence of infinite hyperreal number
345 ----------------------------------------------------------------------------*)
347 lemma Rep_hypreal_omega: "Rep_hypreal(omega) : hypreal"
349 apply (unfold omega_def)
350 apply (rule Rep_hypreal)
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 *)
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])
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)
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])
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)
373 (* existence of infinitesimal number also not *)
374 (* corresponding to any real number *)
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)
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])
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)
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])
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)
396 lemma hypreal_epsilon_not_zero: "epsilon ~= 0"
397 by (unfold epsilon_def hypreal_zero_def, auto)
399 lemma hypreal_epsilon_inverse_omega: "epsilon = inverse(omega)"
400 by (simp add: hypreal_inverse omega_def epsilon_def)
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)
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)
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)
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)
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)
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)
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)
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)
446 (*----------------------------------------------------------------------------
447 Some convenient biconditionals for products of signs
448 ----------------------------------------------------------------------------*)
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)
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)
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)
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])
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)
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";