38 instance hypreal :: plus_ac0 |
38 instance hypreal :: plus_ac0 |
39 by (intro_classes, |
39 by (intro_classes, |
40 (assumption | |
40 (assumption | |
41 rule hypreal_add_commute hypreal_add_assoc hypreal_add_zero_left)+) |
41 rule hypreal_add_commute hypreal_add_assoc hypreal_add_zero_left)+) |
42 |
42 |
43 (**** The simproc abel_cancel ****) |
|
44 |
|
45 (*** Two lemmas needed for the simprocs ***) |
|
46 |
|
47 (*Deletion of other terms in the formula, seeking the -x at the front of z*) |
|
48 lemma hypreal_add_cancel_21: "((x::hypreal) + (y + z) = y + u) = ((x + z) = u)" |
|
49 apply (subst hypreal_add_left_commute) |
|
50 apply (rule hypreal_add_left_cancel) |
|
51 done |
|
52 |
|
53 (*A further rule to deal with the case that |
|
54 everything gets cancelled on the right.*) |
|
55 lemma hypreal_add_cancel_end: "((x::hypreal) + (y + z) = y) = (x = -z)" |
|
56 apply (subst hypreal_add_left_commute) |
|
57 apply (rule_tac t = y in hypreal_add_zero_right [THEN subst], subst hypreal_add_left_cancel) |
|
58 apply (simp (no_asm) add: hypreal_eq_diff_eq [symmetric]) |
|
59 done |
|
60 |
|
61 ML{* |
|
62 val hypreal_add_cancel_21 = thm "hypreal_add_cancel_21"; |
|
63 val hypreal_add_cancel_end = thm "hypreal_add_cancel_end"; |
|
64 |
|
65 structure Hyperreal_Cancel_Data = |
|
66 struct |
|
67 val ss = HOL_ss |
|
68 val eq_reflection = eq_reflection |
|
69 |
|
70 val sg_ref = Sign.self_ref (Theory.sign_of (the_context ())) |
|
71 val T = Type("HyperDef.hypreal",[]) |
|
72 val zero = Const ("0", T) |
|
73 val restrict_to_left = restrict_to_left |
|
74 val add_cancel_21 = hypreal_add_cancel_21 |
|
75 val add_cancel_end = hypreal_add_cancel_end |
|
76 val add_left_cancel = hypreal_add_left_cancel |
|
77 val add_assoc = hypreal_add_assoc |
|
78 val add_commute = hypreal_add_commute |
|
79 val add_left_commute = hypreal_add_left_commute |
|
80 val add_0 = hypreal_add_zero_left |
|
81 val add_0_right = hypreal_add_zero_right |
|
82 |
|
83 val eq_diff_eq = hypreal_eq_diff_eq |
|
84 val eqI_rules = [hypreal_less_eqI, hypreal_eq_eqI, hypreal_le_eqI] |
|
85 fun dest_eqI th = |
|
86 #1 (HOLogic.dest_bin "op =" HOLogic.boolT |
|
87 (HOLogic.dest_Trueprop (concl_of th))) |
|
88 |
|
89 val diff_def = hypreal_diff_def |
|
90 val minus_add_distrib = hypreal_minus_add_distrib |
|
91 val minus_minus = hypreal_minus_minus |
|
92 val minus_0 = hypreal_minus_zero |
|
93 val add_inverses = [hypreal_add_minus, hypreal_add_minus_left] |
|
94 val cancel_simps = [hypreal_add_minus_cancelA, hypreal_minus_add_cancelA] |
|
95 end; |
|
96 |
|
97 structure Hyperreal_Cancel = Abel_Cancel (Hyperreal_Cancel_Data); |
|
98 |
|
99 Addsimprocs [Hyperreal_Cancel.sum_conv, Hyperreal_Cancel.rel_conv]; |
|
100 *} |
|
101 |
|
102 lemma hypreal_minus_diff_eq: "- (z - y) = y - (z::hypreal)" |
|
103 apply (simp (no_asm)) |
|
104 done |
|
105 declare hypreal_minus_diff_eq [simp] |
|
106 |
|
107 |
|
108 lemma hypreal_less_swap_iff: "((x::hypreal) < y) = (-y < -x)" |
|
109 apply (subst hypreal_less_minus_iff) |
|
110 apply (rule_tac x1 = x in hypreal_less_minus_iff [THEN ssubst]) |
|
111 apply (simp (no_asm) add: hypreal_add_commute) |
|
112 done |
|
113 |
|
114 lemma hypreal_gt_zero_iff: |
|
115 "((0::hypreal) < x) = (-x < x)" |
|
116 apply (unfold hypreal_zero_def) |
|
117 apply (rule_tac z = x in eq_Abs_hypreal) |
|
118 apply (auto simp add: hypreal_less hypreal_minus, ultra+) |
|
119 done |
|
120 |
|
121 lemma hypreal_add_less_mono1: "(A::hypreal) < B ==> A + C < B + C" |
43 lemma hypreal_add_less_mono1: "(A::hypreal) < B ==> A + C < B + C" |
122 apply (rule_tac z = A in eq_Abs_hypreal) |
44 apply (rule_tac z = A in eq_Abs_hypreal) |
123 apply (rule_tac z = B in eq_Abs_hypreal) |
45 apply (rule_tac z = B in eq_Abs_hypreal) |
124 apply (rule_tac z = C in eq_Abs_hypreal) |
46 apply (rule_tac z = C in eq_Abs_hypreal) |
125 apply (auto intro!: exI simp add: hypreal_less_def hypreal_add, ultra) |
47 apply (auto intro!: exI simp add: hypreal_less_def hypreal_add, ultra) |
126 done |
48 done |
127 |
|
128 lemma hypreal_add_less_mono2: "!!(A::hypreal). A < B ==> C + A < C + B" |
|
129 by (auto intro: hypreal_add_less_mono1 simp add: hypreal_add_commute) |
|
130 |
|
131 lemma hypreal_lt_zero_iff: "(x < (0::hypreal)) = (x < -x)" |
|
132 apply (rule hypreal_minus_zero_less_iff [THEN subst]) |
|
133 apply (subst hypreal_gt_zero_iff) |
|
134 apply (simp (no_asm_use)) |
|
135 done |
|
136 |
|
137 lemma hypreal_add_order: "[| 0 < x; 0 < y |] ==> (0::hypreal) < x + y" |
|
138 apply (unfold hypreal_zero_def) |
|
139 apply (rule_tac z = x in eq_Abs_hypreal) |
|
140 apply (rule_tac z = y in eq_Abs_hypreal) |
|
141 apply (auto simp add: hypreal_less_def hypreal_add) |
|
142 apply (auto intro!: exI simp add: hypreal_less_def hypreal_add, ultra) |
|
143 done |
|
144 |
|
145 lemma hypreal_add_order_le: "[| 0 < x; 0 \<le> y |] ==> (0::hypreal) < x + y" |
|
146 by (auto dest: sym order_le_imp_less_or_eq intro: hypreal_add_order) |
|
147 |
49 |
148 lemma hypreal_mult_order: "[| 0 < x; 0 < y |] ==> (0::hypreal) < x * y" |
50 lemma hypreal_mult_order: "[| 0 < x; 0 < y |] ==> (0::hypreal) < x * y" |
149 apply (unfold hypreal_zero_def) |
51 apply (unfold hypreal_zero_def) |
150 apply (rule_tac z = x in eq_Abs_hypreal) |
52 apply (rule_tac z = x in eq_Abs_hypreal) |
151 apply (rule_tac z = y in eq_Abs_hypreal) |
53 apply (rule_tac z = y in eq_Abs_hypreal) |
152 apply (auto intro!: exI simp add: hypreal_less_def hypreal_mult, ultra) |
54 apply (auto intro!: exI simp add: hypreal_less_def hypreal_mult, ultra) |
153 apply (auto intro: real_mult_order) |
55 apply (auto intro: real_mult_order) |
154 done |
56 done |
155 |
57 |
156 lemma hypreal_mult_less_zero1: "[| x < 0; y < 0 |] ==> (0::hypreal) < x * y" |
|
157 apply (drule hypreal_minus_zero_less_iff [THEN iffD2])+ |
|
158 apply (drule hypreal_mult_order, assumption, simp) |
|
159 done |
|
160 |
|
161 lemma hypreal_mult_less_zero: "[| 0 < x; y < 0 |] ==> x*y < (0::hypreal)" |
|
162 apply (drule hypreal_minus_zero_less_iff [THEN iffD2]) |
|
163 apply (drule hypreal_mult_order, assumption) |
|
164 apply (rule hypreal_minus_zero_less_iff [THEN iffD1], simp) |
|
165 done |
|
166 |
|
167 lemma hypreal_zero_less_one: "0 < (1::hypreal)" |
|
168 apply (unfold hypreal_one_def hypreal_zero_def hypreal_less_def) |
|
169 apply (rule_tac x = "%n. 0" in exI) |
|
170 apply (rule_tac x = "%n. 1" in exI) |
|
171 apply (auto simp add: real_zero_less_one FreeUltrafilterNat_Nat_set) |
|
172 done |
|
173 |
|
174 lemma hypreal_le_add_order: "[| 0 \<le> x; 0 \<le> y |] ==> (0::hypreal) \<le> x + y" |
|
175 apply (drule order_le_imp_less_or_eq)+ |
|
176 apply (auto intro: hypreal_add_order order_less_imp_le) |
|
177 done |
|
178 |
|
179 (*** Monotonicity results ***) |
|
180 |
|
181 lemma hypreal_add_right_cancel_less: "(v+z < w+z) = (v < (w::hypreal))" |
|
182 apply (simp (no_asm)) |
|
183 done |
|
184 |
|
185 lemma hypreal_add_left_cancel_less: "(z+v < z+w) = (v < (w::hypreal))" |
|
186 apply (simp (no_asm)) |
|
187 done |
|
188 |
|
189 declare hypreal_add_right_cancel_less [simp] |
|
190 hypreal_add_left_cancel_less [simp] |
|
191 |
|
192 lemma hypreal_add_right_cancel_le: "(v+z \<le> w+z) = (v \<le> (w::hypreal))" |
|
193 apply (simp (no_asm)) |
|
194 done |
|
195 |
|
196 lemma hypreal_add_left_cancel_le: "(z+v \<le> z+w) = (v \<le> (w::hypreal))" |
|
197 apply (simp (no_asm)) |
|
198 done |
|
199 |
|
200 declare hypreal_add_right_cancel_le [simp] hypreal_add_left_cancel_le [simp] |
|
201 |
|
202 lemma hypreal_add_less_mono: "[| (z1::hypreal) < y1; z2 < y2 |] ==> z1 + z2 < y1 + y2" |
|
203 apply (drule hypreal_less_minus_iff [THEN iffD1]) |
|
204 apply (drule hypreal_less_minus_iff [THEN iffD1]) |
|
205 apply (drule hypreal_add_order, assumption) |
|
206 apply (erule_tac V = "0 < y2 + - z2" in thin_rl) |
|
207 apply (drule_tac C = "z1 + z2" in hypreal_add_less_mono1) |
|
208 apply (auto simp add: hypreal_minus_add_distrib [symmetric] |
|
209 hypreal_add_ac simp del: hypreal_minus_add_distrib) |
|
210 done |
|
211 |
|
212 lemma hypreal_add_left_le_mono1: "(q1::hypreal) \<le> q2 ==> x + q1 \<le> x + q2" |
58 lemma hypreal_add_left_le_mono1: "(q1::hypreal) \<le> q2 ==> x + q1 \<le> x + q2" |
213 apply (drule order_le_imp_less_or_eq) |
59 apply (drule order_le_imp_less_or_eq) |
214 apply (auto intro: order_less_imp_le hypreal_add_less_mono1 simp add: hypreal_add_commute) |
60 apply (auto intro: order_less_imp_le hypreal_add_less_mono1 simp add: hypreal_add_commute) |
215 done |
61 done |
216 |
|
217 lemma hypreal_add_le_mono1: "(q1::hypreal) \<le> q2 ==> q1 + x \<le> q2 + x" |
|
218 by (auto dest: hypreal_add_left_le_mono1 simp add: hypreal_add_commute) |
|
219 |
|
220 lemma hypreal_add_le_mono: "[|(i::hypreal)\<le>j; k\<le>l |] ==> i + k \<le> j + l" |
|
221 apply (erule hypreal_add_le_mono1 [THEN order_trans]) |
|
222 apply (simp (no_asm)) |
|
223 done |
|
224 |
|
225 lemma hypreal_add_less_le_mono: "[|(i::hypreal)<j; k\<le>l |] ==> i + k < j + l" |
|
226 by (auto dest!: order_le_imp_less_or_eq intro: hypreal_add_less_mono1 hypreal_add_less_mono) |
|
227 |
|
228 lemma hypreal_add_le_less_mono: "[|(i::hypreal)\<le>j; k<l |] ==> i + k < j + l" |
|
229 by (auto dest!: order_le_imp_less_or_eq intro: hypreal_add_less_mono2 hypreal_add_less_mono) |
|
230 |
|
231 lemma hypreal_less_add_right_cancel: "(A::hypreal) + C < B + C ==> A < B" |
|
232 apply (simp (no_asm_use)) |
|
233 done |
|
234 |
|
235 lemma hypreal_less_add_left_cancel: "(C::hypreal) + A < C + B ==> A < B" |
|
236 apply (simp (no_asm_use)) |
|
237 done |
|
238 |
|
239 lemma hypreal_add_zero_less_le_mono: "[|r < x; (0::hypreal) \<le> y|] ==> r < x + y" |
|
240 by (auto dest: hypreal_add_less_le_mono) |
|
241 |
|
242 lemma hypreal_le_add_right_cancel: "!!(A::hypreal). A + C \<le> B + C ==> A \<le> B" |
|
243 apply (drule_tac x = "-C" in hypreal_add_le_mono1) |
|
244 apply (simp add: hypreal_add_assoc) |
|
245 done |
|
246 |
|
247 lemma hypreal_le_add_left_cancel: "!!(A::hypreal). C + A \<le> C + B ==> A \<le> B" |
|
248 apply (drule_tac x = "-C" in hypreal_add_left_le_mono1) |
|
249 apply (simp add: hypreal_add_assoc [symmetric]) |
|
250 done |
|
251 |
|
252 lemma hypreal_le_square: "(0::hypreal) \<le> x*x" |
|
253 apply (rule_tac x = 0 and y = x in hypreal_linear_less2) |
|
254 apply (auto intro: hypreal_mult_order hypreal_mult_less_zero1 order_less_imp_le) |
|
255 done |
|
256 declare hypreal_le_square [simp] |
|
257 |
62 |
258 lemma hypreal_mult_less_mono1: "[| (0::hypreal) < z; x < y |] ==> x*z < y*z" |
63 lemma hypreal_mult_less_mono1: "[| (0::hypreal) < z; x < y |] ==> x*z < y*z" |
259 apply (rotate_tac 1) |
64 apply (rotate_tac 1) |
260 apply (drule hypreal_less_minus_iff [THEN iffD1]) |
65 apply (drule hypreal_less_minus_iff [THEN iffD1]) |
261 apply (rule hypreal_less_minus_iff [THEN iffD2]) |
66 apply (rule hypreal_less_minus_iff [THEN iffD2]) |
290 by (auto dest: order_le_less_trans simp add: hrabs_def linorder_not_le) |
95 by (auto dest: order_le_less_trans simp add: hrabs_def linorder_not_le) |
291 show "x \<noteq> 0 ==> inverse x * x = 1" by simp |
96 show "x \<noteq> 0 ==> inverse x * x = 1" by simp |
292 show "y \<noteq> 0 ==> x / y = x * inverse y" by (simp add: hypreal_divide_def) |
97 show "y \<noteq> 0 ==> x / y = x * inverse y" by (simp add: hypreal_divide_def) |
293 qed |
98 qed |
294 |
99 |
|
100 (*** Monotonicity results ***) |
|
101 |
|
102 lemma hypreal_add_right_cancel_less: "(v+z < w+z) = (v < (w::hypreal))" |
|
103 by (rule Ring_and_Field.add_less_cancel_right) |
|
104 |
|
105 lemma hypreal_add_left_cancel_less: "(z+v < z+w) = (v < (w::hypreal))" |
|
106 by (rule Ring_and_Field.add_less_cancel_left) |
|
107 |
|
108 lemma hypreal_add_right_cancel_le: "(v+z \<le> w+z) = (v \<le> (w::hypreal))" |
|
109 by (rule Ring_and_Field.add_le_cancel_right) |
|
110 |
|
111 lemma hypreal_add_left_cancel_le: "(z+v \<le> z+w) = (v \<le> (w::hypreal))" |
|
112 by (rule Ring_and_Field.add_le_cancel_left) |
|
113 |
|
114 lemma hypreal_add_less_mono: "[| (z1::hypreal) < y1; z2 < y2 |] ==> z1 + z2 < y1 + y2" |
|
115 by (rule Ring_and_Field.add_strict_mono) |
|
116 |
|
117 lemma hypreal_add_le_mono1: "(q1::hypreal) \<le> q2 ==> q1 + x \<le> q2 + x" |
|
118 by (rule Ring_and_Field.add_right_mono) |
|
119 |
|
120 lemma hypreal_add_le_mono: "[|(i::hypreal)\<le>j; k\<le>l |] ==> i + k \<le> j + l" |
|
121 by (rule Ring_and_Field.add_mono) |
|
122 |
|
123 lemma hypreal_add_less_le_mono: "[|(i::hypreal)<j; k\<le>l |] ==> i + k < j + l" |
|
124 by (auto dest!: order_le_imp_less_or_eq intro: hypreal_add_less_mono1 hypreal_add_less_mono) |
|
125 |
|
126 lemma hypreal_add_less_mono2: "!!(A::hypreal). A < B ==> C + A < C + B" |
|
127 by (auto intro: hypreal_add_less_mono1 simp add: hypreal_add_commute) |
|
128 |
|
129 lemma hypreal_add_le_less_mono: "[|(i::hypreal)\<le>j; k<l |] ==> i + k < j + l" |
|
130 apply (erule add_right_mono [THEN order_le_less_trans]) |
|
131 apply (erule add_strict_left_mono) |
|
132 done |
|
133 |
|
134 lemma hypreal_less_add_right_cancel: "(A::hypreal) + C < B + C ==> A < B" |
|
135 apply (simp (no_asm_use)) |
|
136 done |
|
137 |
|
138 lemma hypreal_less_add_left_cancel: "(C::hypreal) + A < C + B ==> A < B" |
|
139 apply (simp (no_asm_use)) |
|
140 done |
|
141 |
|
142 lemma hypreal_add_zero_less_le_mono: "[|r < x; (0::hypreal) \<le> y|] ==> r < x + y" |
|
143 by (auto dest: hypreal_add_less_le_mono) |
|
144 |
|
145 |
|
146 (**** The simproc abel_cancel ****) |
|
147 |
|
148 (*** Two lemmas needed for the simprocs ***) |
|
149 |
|
150 (*Deletion of other terms in the formula, seeking the -x at the front of z*) |
|
151 lemma hypreal_add_cancel_21: "((x::hypreal) + (y + z) = y + u) = ((x + z) = u)" |
|
152 apply (subst hypreal_add_left_commute) |
|
153 apply (rule hypreal_add_left_cancel) |
|
154 done |
|
155 |
|
156 (*A further rule to deal with the case that |
|
157 everything gets cancelled on the right.*) |
|
158 lemma hypreal_add_cancel_end: "((x::hypreal) + (y + z) = y) = (x = -z)" |
|
159 apply (subst hypreal_add_left_commute) |
|
160 apply (rule_tac t = y in hypreal_add_zero_right [THEN subst], subst hypreal_add_left_cancel) |
|
161 apply (simp (no_asm) add: hypreal_eq_diff_eq [symmetric]) |
|
162 done |
|
163 |
|
164 ML{* |
|
165 val hypreal_add_cancel_21 = thm "hypreal_add_cancel_21"; |
|
166 val hypreal_add_cancel_end = thm "hypreal_add_cancel_end"; |
|
167 |
|
168 structure Hyperreal_Cancel_Data = |
|
169 struct |
|
170 val ss = HOL_ss |
|
171 val eq_reflection = eq_reflection |
|
172 |
|
173 val sg_ref = Sign.self_ref (Theory.sign_of (the_context ())) |
|
174 val T = Type("HyperDef.hypreal",[]) |
|
175 val zero = Const ("0", T) |
|
176 val restrict_to_left = restrict_to_left |
|
177 val add_cancel_21 = hypreal_add_cancel_21 |
|
178 val add_cancel_end = hypreal_add_cancel_end |
|
179 val add_left_cancel = hypreal_add_left_cancel |
|
180 val add_assoc = hypreal_add_assoc |
|
181 val add_commute = hypreal_add_commute |
|
182 val add_left_commute = hypreal_add_left_commute |
|
183 val add_0 = hypreal_add_zero_left |
|
184 val add_0_right = hypreal_add_zero_right |
|
185 |
|
186 val eq_diff_eq = hypreal_eq_diff_eq |
|
187 val eqI_rules = [hypreal_less_eqI, hypreal_eq_eqI, hypreal_le_eqI] |
|
188 fun dest_eqI th = |
|
189 #1 (HOLogic.dest_bin "op =" HOLogic.boolT |
|
190 (HOLogic.dest_Trueprop (concl_of th))) |
|
191 |
|
192 val diff_def = hypreal_diff_def |
|
193 val minus_add_distrib = hypreal_minus_add_distrib |
|
194 val minus_minus = hypreal_minus_minus |
|
195 val minus_0 = hypreal_minus_zero |
|
196 val add_inverses = [hypreal_add_minus, hypreal_add_minus_left] |
|
197 val cancel_simps = [hypreal_add_minus_cancelA, hypreal_minus_add_cancelA] |
|
198 end; |
|
199 |
|
200 structure Hyperreal_Cancel = Abel_Cancel (Hyperreal_Cancel_Data); |
|
201 |
|
202 Addsimprocs [Hyperreal_Cancel.sum_conv, Hyperreal_Cancel.rel_conv]; |
|
203 *} |
|
204 |
|
205 lemma hypreal_le_add_right_cancel: "!!(A::hypreal). A + C \<le> B + C ==> A \<le> B" |
|
206 apply (drule_tac x = "-C" in hypreal_add_le_mono1) |
|
207 apply (simp add: hypreal_add_assoc) |
|
208 done |
|
209 |
|
210 lemma hypreal_le_add_left_cancel: "!!(A::hypreal). C + A \<le> C + B ==> A \<le> B" |
|
211 apply (drule_tac x = "-C" in hypreal_add_left_le_mono1) |
|
212 apply (simp add: hypreal_add_assoc [symmetric]) |
|
213 done |
|
214 |
|
215 lemma hypreal_mult_less_zero: "[| 0 < x; y < 0 |] ==> x*y < (0::hypreal)" |
|
216 apply (drule hypreal_minus_zero_less_iff [THEN iffD2]) |
|
217 apply (drule hypreal_mult_order, assumption) |
|
218 apply (rule hypreal_minus_zero_less_iff [THEN iffD1], simp) |
|
219 done |
|
220 |
|
221 lemma hypreal_mult_less_zero1: "[| x < 0; y < 0 |] ==> (0::hypreal) < x * y" |
|
222 apply (drule hypreal_minus_zero_less_iff [THEN iffD2])+ |
|
223 apply (drule hypreal_mult_order, assumption, simp) |
|
224 done |
|
225 |
|
226 lemma hypreal_le_square: "(0::hypreal) \<le> x*x" |
|
227 apply (rule_tac x = 0 and y = x in hypreal_linear_less2) |
|
228 apply (auto intro: hypreal_mult_order hypreal_mult_less_zero1 order_less_imp_le) |
|
229 done |
|
230 declare hypreal_le_square [simp] |
|
231 |
|
232 lemma hypreal_add_order: "[| 0 < x; 0 < y |] ==> (0::hypreal) < x + y" |
|
233 apply (erule order_less_trans) |
|
234 apply (drule hypreal_add_less_mono2, simp) |
|
235 done |
|
236 |
|
237 lemma hypreal_le_add_order: "[| 0 \<le> x; 0 \<le> y |] ==> (0::hypreal) \<le> x + y" |
|
238 apply (drule order_le_imp_less_or_eq)+ |
|
239 apply (auto intro: hypreal_add_order order_less_imp_le) |
|
240 done |
|
241 |
295 text{*The precondition could be weakened to @{term "0\<le>x"}*} |
242 text{*The precondition could be weakened to @{term "0\<le>x"}*} |
296 lemma hypreal_mult_less_mono: |
243 lemma hypreal_mult_less_mono: |
297 "[| u<v; x<y; (0::hypreal) < v; 0 < x |] ==> u*x < v* y" |
244 "[| u<v; x<y; (0::hypreal) < v; 0 < x |] ==> u*x < v* y" |
298 by (simp add: Ring_and_Field.mult_strict_mono order_less_imp_le) |
245 by (simp add: Ring_and_Field.mult_strict_mono order_less_imp_le) |
299 |
246 |
300 lemma hypreal_inverse_gt_0: "0 < x ==> 0 < inverse (x::hypreal)" |
247 lemma hypreal_inverse_gt_0: "0 < x ==> 0 < inverse (x::hypreal)" |
301 by (rule Ring_and_Field.positive_imp_inverse_positive) |
248 by (rule Ring_and_Field.positive_imp_inverse_positive) |
302 |
249 |
303 lemma hypreal_inverse_less_0: "x < 0 ==> inverse (x::hypreal) < 0" |
250 lemma hypreal_inverse_less_0: "x < 0 ==> inverse (x::hypreal) < 0" |
304 by (rule Ring_and_Field.negative_imp_inverse_negative) |
251 by (rule Ring_and_Field.negative_imp_inverse_negative) |
|
252 |
|
253 lemma hypreal_less_swap_iff: "((x::hypreal) < y) = (-y < -x)" |
|
254 apply (subst hypreal_less_minus_iff) |
|
255 apply (rule_tac x1 = x in hypreal_less_minus_iff [THEN ssubst]) |
|
256 apply (simp (no_asm) add: hypreal_add_commute) |
|
257 done |
|
258 |
|
259 lemma hypreal_gt_zero_iff: |
|
260 "((0::hypreal) < x) = (-x < x)" |
|
261 apply (unfold hypreal_zero_def) |
|
262 apply (rule_tac z = x in eq_Abs_hypreal) |
|
263 apply (auto simp add: hypreal_less hypreal_minus, ultra+) |
|
264 done |
|
265 |
|
266 lemma hypreal_lt_zero_iff: "(x < (0::hypreal)) = (x < -x)" |
|
267 apply (rule hypreal_minus_zero_less_iff [THEN subst]) |
|
268 apply (subst hypreal_gt_zero_iff) |
|
269 apply (simp (no_asm_use)) |
|
270 done |
305 |
271 |
306 |
272 |
307 (*---------------------------------------------------------------------------- |
273 (*---------------------------------------------------------------------------- |
308 Existence of infinite hyperreal number |
274 Existence of infinite hyperreal number |
309 ----------------------------------------------------------------------------*) |
275 ----------------------------------------------------------------------------*) |