1 (* Title: HOL/Ring_and_Field.thy
3 Author: Gertrud Bauer and Markus Wenzel, TU Muenchen
4 Lawrence C Paulson, University of Cambridge
5 Revised and splitted into Ring_and_Field.thy and Group.thy
6 by Steven Obua, TU Muenchen, in May 2004
7 License: GPL (GNU GENERAL PUBLIC LICENSE)
10 header {* (Ordered) Rings and Fields *}
12 theory Ring_and_Field = OrderedGroup:
15 The theory of partially ordered rings is taken from the books:
17 \item \emph{Lattice Theory} by Garret Birkhoff, American Mathematical Society 1979
18 \item \emph{Partially Ordered Algebraic Systems}, Pergamon Press 1963
20 Most of the used notions can also be looked up in
22 \item \emph{www.mathworld.com} by Eric Weisstein et. al.
23 \item \emph{Algebra I} by van der Waerden, Springer.
27 axclass semiring \<subseteq> ab_semigroup_add, semigroup_mult
28 left_distrib: "(a + b) * c = a * c + b * c"
29 right_distrib: "a * (b + c) = a * b + a * c"
31 axclass semiring_0 \<subseteq> semiring, comm_monoid_add
33 axclass comm_semiring \<subseteq> ab_semigroup_add, ab_semigroup_mult
34 mult_commute: "a * b = b * a"
35 distrib: "(a + b) * c = a * c + b * c"
37 instance comm_semiring \<subseteq> semiring
40 show "(a + b) * c = a * c + b * c" by (simp add: distrib)
41 have "a * (b + c) = (b + c) * a" by (simp add: mult_ac)
42 also have "... = b * a + c * a" by (simp only: distrib)
43 also have "... = a * b + a * c" by (simp add: mult_ac)
44 finally show "a * (b + c) = a * b + a * c" by blast
47 axclass comm_semiring_0 \<subseteq> comm_semiring, comm_monoid_add
49 instance comm_semiring_0 \<subseteq> semiring_0 ..
51 axclass axclass_0_neq_1 \<subseteq> zero, one
52 zero_neq_one [simp]: "0 \<noteq> 1"
54 axclass semiring_1 \<subseteq> axclass_0_neq_1, semiring_0, monoid_mult
56 axclass comm_semiring_1 \<subseteq> axclass_0_neq_1, comm_semiring_0, comm_monoid_mult (* previously almost_semiring *)
58 instance comm_semiring_1 \<subseteq> semiring_1 ..
60 axclass axclass_no_zero_divisors \<subseteq> zero, times
61 no_zero_divisors: "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> a * b \<noteq> 0"
63 axclass comm_semiring_1_cancel \<subseteq> comm_semiring_1, cancel_ab_semigroup_add (* previously semiring *)
65 axclass ring \<subseteq> semiring, ab_group_add
67 instance ring \<subseteq> semiring_0 ..
69 axclass comm_ring \<subseteq> comm_semiring_0, ab_group_add
71 instance comm_ring \<subseteq> ring ..
73 instance comm_ring \<subseteq> comm_semiring_0 ..
75 axclass ring_1 \<subseteq> ring, semiring_1
77 axclass comm_ring_1 \<subseteq> comm_ring, comm_semiring_1 (* previously ring *)
79 instance comm_ring_1 \<subseteq> ring_1 ..
81 instance comm_ring_1 \<subseteq> comm_semiring_1_cancel ..
83 axclass idom \<subseteq> comm_ring_1, axclass_no_zero_divisors
85 axclass field \<subseteq> comm_ring_1, inverse
86 left_inverse [simp]: "a \<noteq> 0 ==> inverse a * a = 1"
87 divide_inverse: "a / b = a * inverse b"
89 lemma mult_zero_left [simp]: "0 * a = (0::'a::{semiring_0, cancel_semigroup_add})"
91 have "0*a + 0*a = 0*a + 0"
92 by (simp add: left_distrib [symmetric])
94 by (simp only: add_left_cancel)
97 lemma mult_zero_right [simp]: "a * 0 = (0::'a::{semiring_0, cancel_semigroup_add})"
99 have "a*0 + a*0 = a*0 + 0"
100 by (simp add: right_distrib [symmetric])
102 by (simp only: add_left_cancel)
105 lemma field_mult_eq_0_iff [simp]: "(a*b = (0::'a::field)) = (a = 0 | b = 0)"
107 assume "a=0" thus ?thesis by simp
109 assume anz [simp]: "a\<noteq>0"
111 hence "inverse a * (a * b) = 0" by simp
112 hence "b = 0" by (simp (no_asm_use) add: mult_assoc [symmetric])}
113 thus ?thesis by force
116 instance field \<subseteq> idom
117 by (intro_classes, simp)
119 axclass division_by_zero \<subseteq> zero, inverse
120 inverse_zero [simp]: "inverse 0 = 0"
122 subsection {* Distribution rules *}
124 theorems ring_distrib = right_distrib left_distrib
126 text{*For the @{text combine_numerals} simproc*}
127 lemma combine_common_factor:
128 "a*e + (b*e + c) = (a+b)*e + (c::'a::semiring)"
129 by (simp add: left_distrib add_ac)
131 lemma minus_mult_left: "- (a * b) = (-a) * (b::'a::ring)"
132 apply (rule equals_zero_I)
133 apply (simp add: left_distrib [symmetric])
136 lemma minus_mult_right: "- (a * b) = a * -(b::'a::ring)"
137 apply (rule equals_zero_I)
138 apply (simp add: right_distrib [symmetric])
141 lemma minus_mult_minus [simp]: "(- a) * (- b) = a * (b::'a::ring)"
142 by (simp add: minus_mult_left [symmetric] minus_mult_right [symmetric])
144 lemma minus_mult_commute: "(- a) * b = a * (- b::'a::ring)"
145 by (simp add: minus_mult_left [symmetric] minus_mult_right [symmetric])
147 lemma right_diff_distrib: "a * (b - c) = a * b - a * (c::'a::ring)"
148 by (simp add: right_distrib diff_minus
149 minus_mult_left [symmetric] minus_mult_right [symmetric])
151 lemma left_diff_distrib: "(a - b) * c = a * c - b * (c::'a::ring)"
152 by (simp add: left_distrib diff_minus
153 minus_mult_left [symmetric] minus_mult_right [symmetric])
155 axclass pordered_semiring \<subseteq> semiring_0, pordered_ab_semigroup_add
156 mult_left_mono: "a <= b \<Longrightarrow> 0 <= c \<Longrightarrow> c * a <= c * b"
157 mult_right_mono: "a <= b \<Longrightarrow> 0 <= c \<Longrightarrow> a * c <= b * c"
159 axclass pordered_cancel_semiring \<subseteq> pordered_semiring, cancel_ab_semigroup_add
161 axclass ordered_semiring_strict \<subseteq> semiring_0, ordered_cancel_ab_semigroup_add
162 mult_strict_left_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b"
163 mult_strict_right_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> a * c < b * c"
165 instance ordered_semiring_strict \<subseteq> pordered_cancel_semiring
167 apply (case_tac "a < b & 0 < c")
168 apply (auto simp add: mult_strict_left_mono order_less_le)
169 apply (auto simp add: mult_strict_left_mono order_le_less)
170 apply (simp add: mult_strict_right_mono)
173 axclass pordered_comm_semiring \<subseteq> comm_semiring_0, pordered_ab_semigroup_add
174 mult_mono: "a <= b \<Longrightarrow> 0 <= c \<Longrightarrow> c * a <= c * b"
176 axclass pordered_cancel_comm_semiring \<subseteq> pordered_comm_semiring, cancel_ab_semigroup_add
178 instance pordered_cancel_comm_semiring \<subseteq> pordered_comm_semiring ..
180 axclass ordered_comm_semiring_strict \<subseteq> comm_semiring_0, ordered_cancel_ab_semigroup_add
181 mult_strict_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b"
183 instance pordered_comm_semiring \<subseteq> pordered_semiring
184 by (intro_classes, insert mult_mono, simp_all add: mult_commute, blast+)
186 instance pordered_cancel_comm_semiring \<subseteq> pordered_cancel_semiring ..
188 instance ordered_comm_semiring_strict \<subseteq> ordered_semiring_strict
189 by (intro_classes, insert mult_strict_mono, simp_all add: mult_commute, blast+)
191 instance ordered_comm_semiring_strict \<subseteq> pordered_cancel_comm_semiring
192 apply (intro_classes)
193 apply (case_tac "a < b & 0 < c")
194 apply (auto simp add: mult_strict_left_mono order_less_le)
195 apply (auto simp add: mult_strict_left_mono order_le_less)
198 axclass pordered_ring \<subseteq> ring, pordered_semiring
200 instance pordered_ring \<subseteq> pordered_ab_group_add ..
202 instance pordered_ring \<subseteq> pordered_cancel_semiring ..
204 axclass lordered_ring \<subseteq> pordered_ring, lordered_ab_group_abs
206 axclass axclass_abs_if \<subseteq> minus, ord, zero
207 abs_if: "abs a = (if (a < 0) then (-a) else a)"
209 axclass ordered_ring_strict \<subseteq> ring, ordered_semiring_strict, axclass_abs_if
211 instance ordered_ring_strict \<subseteq> lordered_ab_group ..
213 instance ordered_ring_strict \<subseteq> lordered_ring
214 by (intro_classes, simp add: abs_if join_eq_if)
216 axclass pordered_comm_ring \<subseteq> comm_ring, pordered_comm_semiring
218 axclass ordered_semidom \<subseteq> comm_semiring_1_cancel, ordered_comm_semiring_strict (* previously ordered_semiring *)
219 zero_less_one [simp]: "0 < 1"
221 axclass ordered_idom \<subseteq> comm_ring_1, ordered_comm_semiring_strict, axclass_abs_if (* previously ordered_ring *)
223 instance ordered_idom \<subseteq> ordered_ring_strict ..
225 axclass ordered_field \<subseteq> field, ordered_idom
228 "(a*e + c = b*e + d) = ((a-b)*e + c = (d::'a::ring))"
229 apply (simp add: diff_minus left_distrib)
230 apply (simp add: diff_minus left_distrib add_ac)
231 apply (simp add: compare_rls minus_mult_left [symmetric])
235 "(a*e + c = b*e + d) = (c = (b-a)*e + (d::'a::ring))"
236 apply (simp add: diff_minus left_distrib add_ac)
237 apply (simp add: compare_rls minus_mult_left [symmetric])
241 "(a*e + c < b*e + d) = ((a-b)*e + c < (d::'a::pordered_ring))"
242 apply (simp add: diff_minus left_distrib add_ac)
243 apply (simp add: compare_rls minus_mult_left [symmetric])
247 "(a*e + c < b*e + d) = (c < (b-a)*e + (d::'a::pordered_ring))"
248 apply (simp add: diff_minus left_distrib add_ac)
249 apply (simp add: compare_rls minus_mult_left [symmetric])
253 "(a*e + c \<le> b*e + d) = ((a-b)*e + c \<le> (d::'a::pordered_ring))"
254 apply (simp add: diff_minus left_distrib add_ac)
255 apply (simp add: compare_rls minus_mult_left [symmetric])
259 "(a*e + c \<le> b*e + d) = (c \<le> (b-a)*e + (d::'a::pordered_ring))"
260 apply (simp add: diff_minus left_distrib add_ac)
261 apply (simp add: compare_rls minus_mult_left [symmetric])
264 subsection {* Ordering Rules for Multiplication *}
266 lemma mult_left_le_imp_le:
267 "[|c*a \<le> c*b; 0 < c|] ==> a \<le> (b::'a::ordered_semiring_strict)"
268 by (force simp add: mult_strict_left_mono linorder_not_less [symmetric])
270 lemma mult_right_le_imp_le:
271 "[|a*c \<le> b*c; 0 < c|] ==> a \<le> (b::'a::ordered_semiring_strict)"
272 by (force simp add: mult_strict_right_mono linorder_not_less [symmetric])
274 lemma mult_left_less_imp_less:
275 "[|c*a < c*b; 0 \<le> c|] ==> a < (b::'a::ordered_semiring_strict)"
276 by (force simp add: mult_left_mono linorder_not_le [symmetric])
278 lemma mult_right_less_imp_less:
279 "[|a*c < b*c; 0 \<le> c|] ==> a < (b::'a::ordered_semiring_strict)"
280 by (force simp add: mult_right_mono linorder_not_le [symmetric])
282 lemma mult_strict_left_mono_neg:
283 "[|b < a; c < 0|] ==> c * a < c * (b::'a::ordered_ring_strict)"
284 apply (drule mult_strict_left_mono [of _ _ "-c"])
285 apply (simp_all add: minus_mult_left [symmetric])
288 lemma mult_left_mono_neg:
289 "[|b \<le> a; c \<le> 0|] ==> c * a \<le> c * (b::'a::pordered_ring)"
290 apply (drule mult_left_mono [of _ _ "-c"])
291 apply (simp_all add: minus_mult_left [symmetric])
294 lemma mult_strict_right_mono_neg:
295 "[|b < a; c < 0|] ==> a * c < b * (c::'a::ordered_ring_strict)"
296 apply (drule mult_strict_right_mono [of _ _ "-c"])
297 apply (simp_all add: minus_mult_right [symmetric])
300 lemma mult_right_mono_neg:
301 "[|b \<le> a; c \<le> 0|] ==> a * c \<le> (b::'a::pordered_ring) * c"
302 apply (drule mult_right_mono [of _ _ "-c"])
304 apply (simp_all add: minus_mult_right [symmetric])
307 subsection{* Products of Signs *}
309 lemma mult_pos: "[| (0::'a::ordered_semiring_strict) < a; 0 < b |] ==> 0 < a*b"
310 by (drule mult_strict_left_mono [of 0 b], auto)
312 lemma mult_pos_le: "[| (0::'a::pordered_cancel_semiring) \<le> a; 0 \<le> b |] ==> 0 \<le> a*b"
313 by (drule mult_left_mono [of 0 b], auto)
315 lemma mult_pos_neg: "[| (0::'a::ordered_semiring_strict) < a; b < 0 |] ==> a*b < 0"
316 by (drule mult_strict_left_mono [of b 0], auto)
318 lemma mult_pos_neg_le: "[| (0::'a::pordered_cancel_semiring) \<le> a; b \<le> 0 |] ==> a*b \<le> 0"
319 by (drule mult_left_mono [of b 0], auto)
321 lemma mult_pos_neg2: "[| (0::'a::ordered_semiring_strict) < a; b < 0 |] ==> b*a < 0"
322 by (drule mult_strict_right_mono[of b 0], auto)
324 lemma mult_pos_neg2_le: "[| (0::'a::pordered_cancel_semiring) \<le> a; b \<le> 0 |] ==> b*a \<le> 0"
325 by (drule mult_right_mono[of b 0], auto)
327 lemma mult_neg: "[| a < (0::'a::ordered_ring_strict); b < 0 |] ==> 0 < a*b"
328 by (drule mult_strict_right_mono_neg, auto)
330 lemma mult_neg_le: "[| a \<le> (0::'a::pordered_ring); b \<le> 0 |] ==> 0 \<le> a*b"
331 by (drule mult_right_mono_neg[of a 0 b ], auto)
333 lemma zero_less_mult_pos:
334 "[| 0 < a*b; 0 < a|] ==> 0 < (b::'a::ordered_semiring_strict)"
335 apply (case_tac "b\<le>0")
336 apply (auto simp add: order_le_less linorder_not_less)
337 apply (drule_tac mult_pos_neg [of a b])
338 apply (auto dest: order_less_not_sym)
341 lemma zero_less_mult_pos2:
342 "[| 0 < b*a; 0 < a|] ==> 0 < (b::'a::ordered_semiring_strict)"
343 apply (case_tac "b\<le>0")
344 apply (auto simp add: order_le_less linorder_not_less)
345 apply (drule_tac mult_pos_neg2 [of a b])
346 apply (auto dest: order_less_not_sym)
349 lemma zero_less_mult_iff:
350 "((0::'a::ordered_ring_strict) < a*b) = (0 < a & 0 < b | a < 0 & b < 0)"
351 apply (auto simp add: order_le_less linorder_not_less mult_pos mult_neg)
352 apply (blast dest: zero_less_mult_pos)
353 apply (blast dest: zero_less_mult_pos2)
356 text{*A field has no "zero divisors", and this theorem holds without the
357 assumption of an ordering. See @{text field_mult_eq_0_iff} below.*}
358 lemma mult_eq_0_iff [simp]: "(a*b = (0::'a::ordered_ring_strict)) = (a = 0 | b = 0)"
359 apply (case_tac "a < 0")
360 apply (auto simp add: linorder_not_less order_le_less linorder_neq_iff)
361 apply (force dest: mult_strict_right_mono_neg mult_strict_right_mono)+
364 lemma zero_le_mult_iff:
365 "((0::'a::ordered_ring_strict) \<le> a*b) = (0 \<le> a & 0 \<le> b | a \<le> 0 & b \<le> 0)"
366 by (auto simp add: eq_commute [of 0] order_le_less linorder_not_less
369 lemma mult_less_0_iff:
370 "(a*b < (0::'a::ordered_ring_strict)) = (0 < a & b < 0 | a < 0 & 0 < b)"
371 apply (insert zero_less_mult_iff [of "-a" b])
372 apply (force simp add: minus_mult_left[symmetric])
376 "(a*b \<le> (0::'a::ordered_ring_strict)) = (0 \<le> a & b \<le> 0 | a \<le> 0 & 0 \<le> b)"
377 apply (insert zero_le_mult_iff [of "-a" b])
378 apply (force simp add: minus_mult_left[symmetric])
381 lemma split_mult_pos_le: "(0 \<le> a & 0 \<le> b) | (a \<le> 0 & b \<le> 0) \<Longrightarrow> 0 \<le> a * (b::_::pordered_ring)"
382 by (auto simp add: mult_pos_le mult_neg_le)
384 lemma split_mult_neg_le: "(0 \<le> a & b \<le> 0) | (a \<le> 0 & 0 \<le> b) \<Longrightarrow> a * b \<le> (0::_::pordered_cancel_semiring)"
385 by (auto simp add: mult_pos_neg_le mult_pos_neg2_le)
387 lemma zero_le_square: "(0::'a::ordered_ring_strict) \<le> a*a"
388 by (simp add: zero_le_mult_iff linorder_linear)
390 text{*Proving axiom @{text zero_less_one} makes all @{text ordered_semidom}
391 theorems available to members of @{term ordered_idom} *}
393 instance ordered_idom \<subseteq> ordered_semidom
395 have "(0::'a) \<le> 1*1" by (rule zero_le_square)
396 thus "(0::'a) < 1" by (simp add: order_le_less)
399 instance ordered_ring_strict \<subseteq> axclass_no_zero_divisors
400 by (intro_classes, simp)
402 instance ordered_idom \<subseteq> idom ..
404 text{*All three types of comparision involving 0 and 1 are covered.*}
406 declare zero_neq_one [THEN not_sym, simp]
408 lemma zero_le_one [simp]: "(0::'a::ordered_semidom) \<le> 1"
409 by (rule zero_less_one [THEN order_less_imp_le])
411 lemma not_one_le_zero [simp]: "~ (1::'a::ordered_semidom) \<le> 0"
412 by (simp add: linorder_not_le)
414 lemma not_one_less_zero [simp]: "~ (1::'a::ordered_semidom) < 0"
415 by (simp add: linorder_not_less)
417 subsection{*More Monotonicity*}
419 lemma mult_left_mono_neg:
420 "[|b \<le> a; c \<le> 0|] ==> c * a \<le> c * (b::'a::pordered_ring)"
421 apply (drule mult_left_mono [of _ _ "-c"])
422 apply (simp_all add: minus_mult_left [symmetric])
425 lemma mult_right_mono_neg:
426 "[|b \<le> a; c \<le> 0|] ==> a * c \<le> b * (c::'a::pordered_ring)"
427 apply (drule mult_right_mono [of _ _ "-c"])
428 apply (simp_all add: minus_mult_right [symmetric])
431 text{*Strict monotonicity in both arguments*}
432 lemma mult_strict_mono:
433 "[|a<b; c<d; 0<b; 0\<le>c|] ==> a * c < b * (d::'a::ordered_semiring_strict)"
434 apply (case_tac "c=0")
435 apply (simp add: mult_pos)
436 apply (erule mult_strict_right_mono [THEN order_less_trans])
437 apply (force simp add: order_le_less)
438 apply (erule mult_strict_left_mono, assumption)
441 text{*This weaker variant has more natural premises*}
442 lemma mult_strict_mono':
443 "[| a<b; c<d; 0 \<le> a; 0 \<le> c|] ==> a * c < b * (d::'a::ordered_semiring_strict)"
444 apply (rule mult_strict_mono)
445 apply (blast intro: order_le_less_trans)+
449 "[|a \<le> b; c \<le> d; 0 \<le> b; 0 \<le> c|]
450 ==> a * c \<le> b * (d::'a::pordered_semiring)"
451 apply (erule mult_right_mono [THEN order_trans], assumption)
452 apply (erule mult_left_mono, assumption)
455 lemma less_1_mult: "[| 1 < m; 1 < n |] ==> 1 < m*(n::'a::ordered_semidom)"
456 apply (insert mult_strict_mono [of 1 m 1 n])
457 apply (simp add: order_less_trans [OF zero_less_one])
460 subsection{*Cancellation Laws for Relationships With a Common Factor*}
462 text{*Cancellation laws for @{term "c*a < c*b"} and @{term "a*c < b*c"},
463 also with the relations @{text "\<le>"} and equality.*}
465 lemma mult_less_cancel_right:
466 "(a*c < b*c) = ((0 < c & a < b) | (c < 0 & b < (a::'a::ordered_ring_strict)))"
467 apply (case_tac "c = 0")
468 apply (auto simp add: linorder_neq_iff mult_strict_right_mono
469 mult_strict_right_mono_neg)
470 apply (auto simp add: linorder_not_less
471 linorder_not_le [symmetric, of "a*c"]
472 linorder_not_le [symmetric, of a])
473 apply (erule_tac [!] notE)
474 apply (auto simp add: order_less_imp_le mult_right_mono
478 lemma mult_less_cancel_left:
479 "(c*a < c*b) = ((0 < c & a < b) | (c < 0 & b < (a::'a::ordered_ring_strict)))"
480 apply (case_tac "c = 0")
481 apply (auto simp add: linorder_neq_iff mult_strict_left_mono
482 mult_strict_left_mono_neg)
483 apply (auto simp add: linorder_not_less
484 linorder_not_le [symmetric, of "c*a"]
485 linorder_not_le [symmetric, of a])
486 apply (erule_tac [!] notE)
487 apply (auto simp add: order_less_imp_le mult_left_mono
491 lemma mult_le_cancel_right:
492 "(a*c \<le> b*c) = ((0<c --> a\<le>b) & (c<0 --> b \<le> (a::'a::ordered_ring_strict)))"
493 by (simp add: linorder_not_less [symmetric] mult_less_cancel_right)
495 lemma mult_le_cancel_left:
496 "(c*a \<le> c*b) = ((0<c --> a\<le>b) & (c<0 --> b \<le> (a::'a::ordered_ring_strict)))"
497 by (simp add: linorder_not_less [symmetric] mult_less_cancel_left)
499 lemma mult_less_imp_less_left:
500 assumes less: "c*a < c*b" and nonneg: "0 \<le> c"
501 shows "a < (b::'a::ordered_semiring_strict)"
504 hence "b \<le> a" by (simp add: linorder_not_less)
505 hence "c*b \<le> c*a" by (rule mult_left_mono)
506 with this and less show False
507 by (simp add: linorder_not_less [symmetric])
510 lemma mult_less_imp_less_right:
511 assumes less: "a*c < b*c" and nonneg: "0 <= c"
512 shows "a < (b::'a::ordered_semiring_strict)"
515 hence "b \<le> a" by (simp add: linorder_not_less)
516 hence "b*c \<le> a*c" by (rule mult_right_mono)
517 with this and less show False
518 by (simp add: linorder_not_less [symmetric])
521 text{*Cancellation of equalities with a common factor*}
522 lemma mult_cancel_right [simp]:
523 "(a*c = b*c) = (c = (0::'a::ordered_ring_strict) | a=b)"
524 apply (cut_tac linorder_less_linear [of 0 c])
525 apply (force dest: mult_strict_right_mono_neg mult_strict_right_mono
526 simp add: linorder_neq_iff)
529 text{*These cancellation theorems require an ordering. Versions are proved
530 below that work for fields without an ordering.*}
531 lemma mult_cancel_left [simp]:
532 "(c*a = c*b) = (c = (0::'a::ordered_ring_strict) | a=b)"
533 apply (cut_tac linorder_less_linear [of 0 c])
534 apply (force dest: mult_strict_left_mono_neg mult_strict_left_mono
535 simp add: linorder_neq_iff)
538 text{*This list of rewrites decides ring equalities by ordered rewriting.*}
539 lemmas ring_eq_simps =
541 left_distrib right_distrib left_diff_distrib right_diff_distrib
543 add_diff_eq diff_add_eq diff_diff_eq diff_diff_eq2
544 diff_eq_eq eq_diff_eq
547 subsection {* Fields *}
549 lemma right_inverse [simp]:
550 assumes not0: "a \<noteq> 0" shows "a * inverse (a::'a::field) = 1"
552 have "a * inverse a = inverse a * a" by (simp add: mult_ac)
553 also have "... = 1" using not0 by simp
554 finally show ?thesis .
557 lemma right_inverse_eq: "b \<noteq> 0 ==> (a / b = 1) = (a = (b::'a::field))"
559 assume neq: "b \<noteq> 0"
561 hence "a = (a / b) * b" by (simp add: divide_inverse mult_ac)
562 also assume "a / b = 1"
563 finally show "a = b" by simp
566 with neq show "a / b = 1" by (simp add: divide_inverse)
570 lemma nonzero_inverse_eq_divide: "a \<noteq> 0 ==> inverse (a::'a::field) = 1/a"
571 by (simp add: divide_inverse)
573 lemma divide_self [simp]: "a \<noteq> 0 ==> a / (a::'a::field) = 1"
574 by (simp add: divide_inverse)
576 lemma divide_zero [simp]: "a / 0 = (0::'a::{field,division_by_zero})"
577 by (simp add: divide_inverse)
579 lemma divide_zero_left [simp]: "0/a = (0::'a::field)"
580 by (simp add: divide_inverse)
582 lemma inverse_eq_divide: "inverse (a::'a::field) = 1/a"
583 by (simp add: divide_inverse)
585 lemma add_divide_distrib: "(a+b)/(c::'a::field) = a/c + b/c"
586 by (simp add: divide_inverse left_distrib)
589 text{*Compared with @{text mult_eq_0_iff}, this version removes the requirement
591 lemma field_mult_eq_0_iff [simp]: "(a*b = (0::'a::field)) = (a = 0 | b = 0)"
593 assume "a=0" thus ?thesis by simp
595 assume anz [simp]: "a\<noteq>0"
597 hence "inverse a * (a * b) = 0" by simp
598 hence "b = 0" by (simp (no_asm_use) add: mult_assoc [symmetric])}
599 thus ?thesis by force
602 text{*Cancellation of equalities with a common factor*}
603 lemma field_mult_cancel_right_lemma:
604 assumes cnz: "c \<noteq> (0::'a::field)"
608 have "(a * c) * inverse c = (b * c) * inverse c"
611 by (simp add: mult_assoc cnz)
614 lemma field_mult_cancel_right [simp]:
615 "(a*c = b*c) = (c = (0::'a::field) | a=b)"
617 assume "c=0" thus ?thesis by simp
620 thus ?thesis by (force dest: field_mult_cancel_right_lemma)
623 lemma field_mult_cancel_left [simp]:
624 "(c*a = c*b) = (c = (0::'a::field) | a=b)"
625 by (simp add: mult_commute [of c] field_mult_cancel_right)
627 lemma nonzero_imp_inverse_nonzero: "a \<noteq> 0 ==> inverse a \<noteq> (0::'a::field)"
629 assume ianz: "inverse a = 0"
630 assume "a \<noteq> 0"
631 hence "1 = a * inverse a" by simp
632 also have "... = 0" by (simp add: ianz)
633 finally have "1 = (0::'a::field)" .
634 thus False by (simp add: eq_commute)
638 subsection{*Basic Properties of @{term inverse}*}
640 lemma inverse_zero_imp_zero: "inverse a = 0 ==> a = (0::'a::field)"
642 apply (blast dest: nonzero_imp_inverse_nonzero)
645 lemma inverse_nonzero_imp_nonzero:
646 "inverse a = 0 ==> a = (0::'a::field)"
648 apply (blast dest: nonzero_imp_inverse_nonzero)
651 lemma inverse_nonzero_iff_nonzero [simp]:
652 "(inverse a = 0) = (a = (0::'a::{field,division_by_zero}))"
653 by (force dest: inverse_nonzero_imp_nonzero)
655 lemma nonzero_inverse_minus_eq:
656 assumes [simp]: "a\<noteq>0" shows "inverse(-a) = -inverse(a::'a::field)"
658 have "-a * inverse (- a) = -a * - inverse a"
661 by (simp only: field_mult_cancel_left, simp)
664 lemma inverse_minus_eq [simp]:
665 "inverse(-a) = -inverse(a::'a::{field,division_by_zero})";
667 assume "a=0" thus ?thesis by (simp add: inverse_zero)
670 thus ?thesis by (simp add: nonzero_inverse_minus_eq)
673 lemma nonzero_inverse_eq_imp_eq:
674 assumes inveq: "inverse a = inverse b"
675 and anz: "a \<noteq> 0"
676 and bnz: "b \<noteq> 0"
677 shows "a = (b::'a::field)"
679 have "a * inverse b = a * inverse a"
681 hence "(a * inverse b) * b = (a * inverse a) * b"
684 by (simp add: mult_assoc anz bnz)
687 lemma inverse_eq_imp_eq:
688 "inverse a = inverse b ==> a = (b::'a::{field,division_by_zero})"
689 apply (case_tac "a=0 | b=0")
690 apply (force dest!: inverse_zero_imp_zero
691 simp add: eq_commute [of "0::'a"])
692 apply (force dest!: nonzero_inverse_eq_imp_eq)
695 lemma inverse_eq_iff_eq [simp]:
696 "(inverse a = inverse b) = (a = (b::'a::{field,division_by_zero}))"
697 by (force dest!: inverse_eq_imp_eq)
699 lemma nonzero_inverse_inverse_eq:
700 assumes [simp]: "a \<noteq> 0" shows "inverse(inverse (a::'a::field)) = a"
702 have "(inverse (inverse a) * inverse a) * a = a"
703 by (simp add: nonzero_imp_inverse_nonzero)
705 by (simp add: mult_assoc)
708 lemma inverse_inverse_eq [simp]:
709 "inverse(inverse (a::'a::{field,division_by_zero})) = a"
711 assume "a=0" thus ?thesis by simp
714 thus ?thesis by (simp add: nonzero_inverse_inverse_eq)
717 lemma inverse_1 [simp]: "inverse 1 = (1::'a::field)"
719 have "inverse 1 * 1 = (1::'a::field)"
720 by (rule left_inverse [OF zero_neq_one [symmetric]])
724 lemma nonzero_inverse_mult_distrib:
725 assumes anz: "a \<noteq> 0"
726 and bnz: "b \<noteq> 0"
727 shows "inverse(a*b) = inverse(b) * inverse(a::'a::field)"
729 have "inverse(a*b) * (a * b) * inverse(b) = inverse(b)"
730 by (simp add: field_mult_eq_0_iff anz bnz)
731 hence "inverse(a*b) * a = inverse(b)"
732 by (simp add: mult_assoc bnz)
733 hence "inverse(a*b) * a * inverse(a) = inverse(b) * inverse(a)"
736 by (simp add: mult_assoc anz)
739 text{*This version builds in division by zero while also re-orienting
740 the right-hand side.*}
741 lemma inverse_mult_distrib [simp]:
742 "inverse(a*b) = inverse(a) * inverse(b::'a::{field,division_by_zero})"
744 assume "a \<noteq> 0 & b \<noteq> 0"
745 thus ?thesis by (simp add: nonzero_inverse_mult_distrib mult_commute)
747 assume "~ (a \<noteq> 0 & b \<noteq> 0)"
748 thus ?thesis by force
751 text{*There is no slick version using division by zero.*}
753 "[|a \<noteq> 0; b \<noteq> 0|]
754 ==> inverse a + inverse b = (a+b) * inverse a * inverse (b::'a::field)"
755 apply (simp add: left_distrib mult_assoc)
756 apply (simp add: mult_commute [of "inverse a"])
757 apply (simp add: mult_assoc [symmetric] add_commute)
760 lemma inverse_divide [simp]:
761 "inverse (a/b) = b / (a::'a::{field,division_by_zero})"
762 by (simp add: divide_inverse mult_commute)
764 lemma nonzero_mult_divide_cancel_left:
765 assumes [simp]: "b\<noteq>0" and [simp]: "c\<noteq>0"
766 shows "(c*a)/(c*b) = a/(b::'a::field)"
768 have "(c*a)/(c*b) = c * a * (inverse b * inverse c)"
769 by (simp add: field_mult_eq_0_iff divide_inverse
770 nonzero_inverse_mult_distrib)
771 also have "... = a * inverse b * (inverse c * c)"
772 by (simp only: mult_ac)
773 also have "... = a * inverse b"
776 by (simp add: divide_inverse)
779 lemma mult_divide_cancel_left:
780 "c\<noteq>0 ==> (c*a) / (c*b) = a / (b::'a::{field,division_by_zero})"
781 apply (case_tac "b = 0")
782 apply (simp_all add: nonzero_mult_divide_cancel_left)
785 lemma nonzero_mult_divide_cancel_right:
786 "[|b\<noteq>0; c\<noteq>0|] ==> (a*c) / (b*c) = a/(b::'a::field)"
787 by (simp add: mult_commute [of _ c] nonzero_mult_divide_cancel_left)
789 lemma mult_divide_cancel_right:
790 "c\<noteq>0 ==> (a*c) / (b*c) = a / (b::'a::{field,division_by_zero})"
791 apply (case_tac "b = 0")
792 apply (simp_all add: nonzero_mult_divide_cancel_right)
795 (*For ExtractCommonTerm*)
796 lemma mult_divide_cancel_eq_if:
798 (if c=0 then 0 else a / (b::'a::{field,division_by_zero}))"
799 by (simp add: mult_divide_cancel_left)
801 lemma divide_1 [simp]: "a/1 = (a::'a::field)"
802 by (simp add: divide_inverse)
804 lemma times_divide_eq_right [simp]: "a * (b/c) = (a*b) / (c::'a::field)"
805 by (simp add: divide_inverse mult_assoc)
807 lemma times_divide_eq_left: "(b/c) * a = (b*a) / (c::'a::field)"
808 by (simp add: divide_inverse mult_ac)
810 lemma divide_divide_eq_right [simp]:
811 "a / (b/c) = (a*c) / (b::'a::{field,division_by_zero})"
812 by (simp add: divide_inverse mult_ac)
814 lemma divide_divide_eq_left [simp]:
815 "(a / b) / (c::'a::{field,division_by_zero}) = a / (b*c)"
816 by (simp add: divide_inverse mult_assoc)
819 subsection {* Division and Unary Minus *}
821 lemma nonzero_minus_divide_left: "b \<noteq> 0 ==> - (a/b) = (-a) / (b::'a::field)"
822 by (simp add: divide_inverse minus_mult_left)
824 lemma nonzero_minus_divide_right: "b \<noteq> 0 ==> - (a/b) = a / -(b::'a::field)"
825 by (simp add: divide_inverse nonzero_inverse_minus_eq minus_mult_right)
827 lemma nonzero_minus_divide_divide: "b \<noteq> 0 ==> (-a)/(-b) = a / (b::'a::field)"
828 by (simp add: divide_inverse nonzero_inverse_minus_eq)
830 lemma minus_divide_left: "- (a/b) = (-a) / (b::'a::field)"
831 by (simp add: divide_inverse minus_mult_left [symmetric])
833 lemma minus_divide_right: "- (a/b) = a / -(b::'a::{field,division_by_zero})"
834 by (simp add: divide_inverse minus_mult_right [symmetric])
837 text{*The effect is to extract signs from divisions*}
838 declare minus_divide_left [symmetric, simp]
839 declare minus_divide_right [symmetric, simp]
841 text{*Also, extract signs from products*}
842 declare minus_mult_left [symmetric, simp]
843 declare minus_mult_right [symmetric, simp]
845 lemma minus_divide_divide [simp]:
846 "(-a)/(-b) = a / (b::'a::{field,division_by_zero})"
847 apply (case_tac "b=0", simp)
848 apply (simp add: nonzero_minus_divide_divide)
851 lemma diff_divide_distrib: "(a-b)/(c::'a::field) = a/c - b/c"
852 by (simp add: diff_minus add_divide_distrib)
855 subsection {* Ordered Fields *}
857 lemma positive_imp_inverse_positive:
858 assumes a_gt_0: "0 < a" shows "0 < inverse (a::'a::ordered_field)"
860 have "0 < a * inverse a"
861 by (simp add: a_gt_0 [THEN order_less_imp_not_eq2] zero_less_one)
863 by (simp add: a_gt_0 [THEN order_less_not_sym] zero_less_mult_iff)
866 lemma negative_imp_inverse_negative:
867 "a < 0 ==> inverse a < (0::'a::ordered_field)"
868 by (insert positive_imp_inverse_positive [of "-a"],
869 simp add: nonzero_inverse_minus_eq order_less_imp_not_eq)
871 lemma inverse_le_imp_le:
872 assumes invle: "inverse a \<le> inverse b"
874 shows "b \<le> (a::'a::ordered_field)"
875 proof (rule classical)
878 by (simp add: linorder_not_le)
880 by (blast intro: apos order_less_trans)
881 hence "a * inverse a \<le> a * inverse b"
882 by (simp add: apos invle order_less_imp_le mult_left_mono)
883 hence "(a * inverse a) * b \<le> (a * inverse b) * b"
884 by (simp add: bpos order_less_imp_le mult_right_mono)
886 by (simp add: mult_assoc apos bpos order_less_imp_not_eq2)
889 lemma inverse_positive_imp_positive:
890 assumes inv_gt_0: "0 < inverse a"
891 and [simp]: "a \<noteq> 0"
892 shows "0 < (a::'a::ordered_field)"
894 have "0 < inverse (inverse a)"
895 by (rule positive_imp_inverse_positive)
897 by (simp add: nonzero_inverse_inverse_eq)
900 lemma inverse_positive_iff_positive [simp]:
901 "(0 < inverse a) = (0 < (a::'a::{ordered_field,division_by_zero}))"
902 apply (case_tac "a = 0", simp)
903 apply (blast intro: inverse_positive_imp_positive positive_imp_inverse_positive)
906 lemma inverse_negative_imp_negative:
907 assumes inv_less_0: "inverse a < 0"
908 and [simp]: "a \<noteq> 0"
909 shows "a < (0::'a::ordered_field)"
911 have "inverse (inverse a) < 0"
912 by (rule negative_imp_inverse_negative)
914 by (simp add: nonzero_inverse_inverse_eq)
917 lemma inverse_negative_iff_negative [simp]:
918 "(inverse a < 0) = (a < (0::'a::{ordered_field,division_by_zero}))"
919 apply (case_tac "a = 0", simp)
920 apply (blast intro: inverse_negative_imp_negative negative_imp_inverse_negative)
923 lemma inverse_nonnegative_iff_nonnegative [simp]:
924 "(0 \<le> inverse a) = (0 \<le> (a::'a::{ordered_field,division_by_zero}))"
925 by (simp add: linorder_not_less [symmetric])
927 lemma inverse_nonpositive_iff_nonpositive [simp]:
928 "(inverse a \<le> 0) = (a \<le> (0::'a::{ordered_field,division_by_zero}))"
929 by (simp add: linorder_not_less [symmetric])
932 subsection{*Anti-Monotonicity of @{term inverse}*}
934 lemma less_imp_inverse_less:
935 assumes less: "a < b"
937 shows "inverse b < inverse (a::'a::ordered_field)"
939 assume "~ inverse b < inverse a"
940 hence "inverse a \<le> inverse b"
941 by (simp add: linorder_not_less)
943 by (simp add: linorder_not_less inverse_le_imp_le [OF _ apos])
945 by (rule notE [OF _ less])
948 lemma inverse_less_imp_less:
949 "[|inverse a < inverse b; 0 < a|] ==> b < (a::'a::ordered_field)"
950 apply (simp add: order_less_le [of "inverse a"] order_less_le [of "b"])
951 apply (force dest!: inverse_le_imp_le nonzero_inverse_eq_imp_eq)
954 text{*Both premises are essential. Consider -1 and 1.*}
955 lemma inverse_less_iff_less [simp]:
957 ==> (inverse a < inverse b) = (b < (a::'a::ordered_field))"
958 by (blast intro: less_imp_inverse_less dest: inverse_less_imp_less)
960 lemma le_imp_inverse_le:
961 "[|a \<le> b; 0 < a|] ==> inverse b \<le> inverse (a::'a::ordered_field)"
962 by (force simp add: order_le_less less_imp_inverse_less)
964 lemma inverse_le_iff_le [simp]:
966 ==> (inverse a \<le> inverse b) = (b \<le> (a::'a::ordered_field))"
967 by (blast intro: le_imp_inverse_le dest: inverse_le_imp_le)
970 text{*These results refer to both operands being negative. The opposite-sign
971 case is trivial, since inverse preserves signs.*}
972 lemma inverse_le_imp_le_neg:
973 "[|inverse a \<le> inverse b; b < 0|] ==> b \<le> (a::'a::ordered_field)"
974 apply (rule classical)
975 apply (subgoal_tac "a < 0")
976 prefer 2 apply (force simp add: linorder_not_le intro: order_less_trans)
977 apply (insert inverse_le_imp_le [of "-b" "-a"])
978 apply (simp add: order_less_imp_not_eq nonzero_inverse_minus_eq)
981 lemma less_imp_inverse_less_neg:
982 "[|a < b; b < 0|] ==> inverse b < inverse (a::'a::ordered_field)"
983 apply (subgoal_tac "a < 0")
984 prefer 2 apply (blast intro: order_less_trans)
985 apply (insert less_imp_inverse_less [of "-b" "-a"])
986 apply (simp add: order_less_imp_not_eq nonzero_inverse_minus_eq)
989 lemma inverse_less_imp_less_neg:
990 "[|inverse a < inverse b; b < 0|] ==> b < (a::'a::ordered_field)"
991 apply (rule classical)
992 apply (subgoal_tac "a < 0")
994 apply (force simp add: linorder_not_less intro: order_le_less_trans)
995 apply (insert inverse_less_imp_less [of "-b" "-a"])
996 apply (simp add: order_less_imp_not_eq nonzero_inverse_minus_eq)
999 lemma inverse_less_iff_less_neg [simp]:
1001 ==> (inverse a < inverse b) = (b < (a::'a::ordered_field))"
1002 apply (insert inverse_less_iff_less [of "-b" "-a"])
1003 apply (simp del: inverse_less_iff_less
1004 add: order_less_imp_not_eq nonzero_inverse_minus_eq)
1007 lemma le_imp_inverse_le_neg:
1008 "[|a \<le> b; b < 0|] ==> inverse b \<le> inverse (a::'a::ordered_field)"
1009 by (force simp add: order_le_less less_imp_inverse_less_neg)
1011 lemma inverse_le_iff_le_neg [simp]:
1013 ==> (inverse a \<le> inverse b) = (b \<le> (a::'a::ordered_field))"
1014 by (blast intro: le_imp_inverse_le_neg dest: inverse_le_imp_le_neg)
1017 subsection{*Inverses and the Number One*}
1019 lemma one_less_inverse_iff:
1020 "(1 < inverse x) = (0 < x & x < (1::'a::{ordered_field,division_by_zero}))"proof cases
1022 with inverse_less_iff_less [OF zero_less_one, of x]
1023 show ?thesis by simp
1025 assume notless: "~ (0 < x)"
1026 have "~ (1 < inverse x)"
1028 assume "1 < inverse x"
1029 also with notless have "... \<le> 0" by (simp add: linorder_not_less)
1030 also have "... < 1" by (rule zero_less_one)
1031 finally show False by auto
1033 with notless show ?thesis by simp
1036 lemma inverse_eq_1_iff [simp]:
1037 "(inverse x = 1) = (x = (1::'a::{field,division_by_zero}))"
1038 by (insert inverse_eq_iff_eq [of x 1], simp)
1040 lemma one_le_inverse_iff:
1041 "(1 \<le> inverse x) = (0 < x & x \<le> (1::'a::{ordered_field,division_by_zero}))"
1042 by (force simp add: order_le_less one_less_inverse_iff zero_less_one
1045 lemma inverse_less_1_iff:
1046 "(inverse x < 1) = (x \<le> 0 | 1 < (x::'a::{ordered_field,division_by_zero}))"
1047 by (simp add: linorder_not_le [symmetric] one_le_inverse_iff)
1049 lemma inverse_le_1_iff:
1050 "(inverse x \<le> 1) = (x \<le> 0 | 1 \<le> (x::'a::{ordered_field,division_by_zero}))"
1051 by (simp add: linorder_not_less [symmetric] one_less_inverse_iff)
1054 subsection{*Division and Signs*}
1056 lemma zero_less_divide_iff:
1057 "((0::'a::{ordered_field,division_by_zero}) < a/b) = (0 < a & 0 < b | a < 0 & b < 0)"
1058 by (simp add: divide_inverse zero_less_mult_iff)
1060 lemma divide_less_0_iff:
1061 "(a/b < (0::'a::{ordered_field,division_by_zero})) =
1062 (0 < a & b < 0 | a < 0 & 0 < b)"
1063 by (simp add: divide_inverse mult_less_0_iff)
1065 lemma zero_le_divide_iff:
1066 "((0::'a::{ordered_field,division_by_zero}) \<le> a/b) =
1067 (0 \<le> a & 0 \<le> b | a \<le> 0 & b \<le> 0)"
1068 by (simp add: divide_inverse zero_le_mult_iff)
1070 lemma divide_le_0_iff:
1071 "(a/b \<le> (0::'a::{ordered_field,division_by_zero})) =
1072 (0 \<le> a & b \<le> 0 | a \<le> 0 & 0 \<le> b)"
1073 by (simp add: divide_inverse mult_le_0_iff)
1075 lemma divide_eq_0_iff [simp]:
1076 "(a/b = 0) = (a=0 | b=(0::'a::{field,division_by_zero}))"
1077 by (simp add: divide_inverse field_mult_eq_0_iff)
1080 subsection{*Simplification of Inequalities Involving Literal Divisors*}
1082 lemma pos_le_divide_eq: "0 < (c::'a::ordered_field) ==> (a \<le> b/c) = (a*c \<le> b)"
1085 hence "(a \<le> b/c) = (a*c \<le> (b/c)*c)"
1086 by (simp add: mult_le_cancel_right order_less_not_sym [OF less])
1087 also have "... = (a*c \<le> b)"
1088 by (simp add: order_less_imp_not_eq2 [OF less] divide_inverse mult_assoc)
1089 finally show ?thesis .
1093 lemma neg_le_divide_eq: "c < (0::'a::ordered_field) ==> (a \<le> b/c) = (b \<le> a*c)"
1096 hence "(a \<le> b/c) = ((b/c)*c \<le> a*c)"
1097 by (simp add: mult_le_cancel_right order_less_not_sym [OF less])
1098 also have "... = (b \<le> a*c)"
1099 by (simp add: order_less_imp_not_eq [OF less] divide_inverse mult_assoc)
1100 finally show ?thesis .
1105 (if 0 < c then a*c \<le> b
1106 else if c < 0 then b \<le> a*c
1107 else a \<le> (0::'a::{ordered_field,division_by_zero}))"
1108 apply (case_tac "c=0", simp)
1109 apply (force simp add: pos_le_divide_eq neg_le_divide_eq linorder_neq_iff)
1112 lemma pos_divide_le_eq: "0 < (c::'a::ordered_field) ==> (b/c \<le> a) = (b \<le> a*c)"
1115 hence "(b/c \<le> a) = ((b/c)*c \<le> a*c)"
1116 by (simp add: mult_le_cancel_right order_less_not_sym [OF less])
1117 also have "... = (b \<le> a*c)"
1118 by (simp add: order_less_imp_not_eq2 [OF less] divide_inverse mult_assoc)
1119 finally show ?thesis .
1122 lemma neg_divide_le_eq: "c < (0::'a::ordered_field) ==> (b/c \<le> a) = (a*c \<le> b)"
1125 hence "(b/c \<le> a) = (a*c \<le> (b/c)*c)"
1126 by (simp add: mult_le_cancel_right order_less_not_sym [OF less])
1127 also have "... = (a*c \<le> b)"
1128 by (simp add: order_less_imp_not_eq [OF less] divide_inverse mult_assoc)
1129 finally show ?thesis .
1134 (if 0 < c then b \<le> a*c
1135 else if c < 0 then a*c \<le> b
1136 else 0 \<le> (a::'a::{ordered_field,division_by_zero}))"
1137 apply (case_tac "c=0", simp)
1138 apply (force simp add: pos_divide_le_eq neg_divide_le_eq linorder_neq_iff)
1142 lemma pos_less_divide_eq:
1143 "0 < (c::'a::ordered_field) ==> (a < b/c) = (a*c < b)"
1146 hence "(a < b/c) = (a*c < (b/c)*c)"
1147 by (simp add: mult_less_cancel_right order_less_not_sym [OF less])
1148 also have "... = (a*c < b)"
1149 by (simp add: order_less_imp_not_eq2 [OF less] divide_inverse mult_assoc)
1150 finally show ?thesis .
1153 lemma neg_less_divide_eq:
1154 "c < (0::'a::ordered_field) ==> (a < b/c) = (b < a*c)"
1157 hence "(a < b/c) = ((b/c)*c < a*c)"
1158 by (simp add: mult_less_cancel_right order_less_not_sym [OF less])
1159 also have "... = (b < a*c)"
1160 by (simp add: order_less_imp_not_eq [OF less] divide_inverse mult_assoc)
1161 finally show ?thesis .
1164 lemma less_divide_eq:
1166 (if 0 < c then a*c < b
1167 else if c < 0 then b < a*c
1168 else a < (0::'a::{ordered_field,division_by_zero}))"
1169 apply (case_tac "c=0", simp)
1170 apply (force simp add: pos_less_divide_eq neg_less_divide_eq linorder_neq_iff)
1173 lemma pos_divide_less_eq:
1174 "0 < (c::'a::ordered_field) ==> (b/c < a) = (b < a*c)"
1177 hence "(b/c < a) = ((b/c)*c < a*c)"
1178 by (simp add: mult_less_cancel_right order_less_not_sym [OF less])
1179 also have "... = (b < a*c)"
1180 by (simp add: order_less_imp_not_eq2 [OF less] divide_inverse mult_assoc)
1181 finally show ?thesis .
1184 lemma neg_divide_less_eq:
1185 "c < (0::'a::ordered_field) ==> (b/c < a) = (a*c < b)"
1188 hence "(b/c < a) = (a*c < (b/c)*c)"
1189 by (simp add: mult_less_cancel_right order_less_not_sym [OF less])
1190 also have "... = (a*c < b)"
1191 by (simp add: order_less_imp_not_eq [OF less] divide_inverse mult_assoc)
1192 finally show ?thesis .
1195 lemma divide_less_eq:
1197 (if 0 < c then b < a*c
1198 else if c < 0 then a*c < b
1199 else 0 < (a::'a::{ordered_field,division_by_zero}))"
1200 apply (case_tac "c=0", simp)
1201 apply (force simp add: pos_divide_less_eq neg_divide_less_eq linorder_neq_iff)
1204 lemma nonzero_eq_divide_eq: "c\<noteq>0 ==> ((a::'a::field) = b/c) = (a*c = b)"
1206 assume [simp]: "c\<noteq>0"
1207 have "(a = b/c) = (a*c = (b/c)*c)"
1208 by (simp add: field_mult_cancel_right)
1209 also have "... = (a*c = b)"
1210 by (simp add: divide_inverse mult_assoc)
1211 finally show ?thesis .
1215 "((a::'a::{field,division_by_zero}) = b/c) = (if c\<noteq>0 then a*c = b else a=0)"
1216 by (simp add: nonzero_eq_divide_eq)
1218 lemma nonzero_divide_eq_eq: "c\<noteq>0 ==> (b/c = (a::'a::field)) = (b = a*c)"
1220 assume [simp]: "c\<noteq>0"
1221 have "(b/c = a) = ((b/c)*c = a*c)"
1222 by (simp add: field_mult_cancel_right)
1223 also have "... = (b = a*c)"
1224 by (simp add: divide_inverse mult_assoc)
1225 finally show ?thesis .
1229 "(b/c = (a::'a::{field,division_by_zero})) = (if c\<noteq>0 then b = a*c else a=0)"
1230 by (force simp add: nonzero_divide_eq_eq)
1232 subsection{*Cancellation Laws for Division*}
1234 lemma divide_cancel_right [simp]:
1235 "(a/c = b/c) = (c = 0 | a = (b::'a::{field,division_by_zero}))"
1236 apply (case_tac "c=0", simp)
1237 apply (simp add: divide_inverse field_mult_cancel_right)
1240 lemma divide_cancel_left [simp]:
1241 "(c/a = c/b) = (c = 0 | a = (b::'a::{field,division_by_zero}))"
1242 apply (case_tac "c=0", simp)
1243 apply (simp add: divide_inverse field_mult_cancel_left)
1246 subsection {* Division and the Number One *}
1248 text{*Simplify expressions equated with 1*}
1249 lemma divide_eq_1_iff [simp]:
1250 "(a/b = 1) = (b \<noteq> 0 & a = (b::'a::{field,division_by_zero}))"
1251 apply (case_tac "b=0", simp)
1252 apply (simp add: right_inverse_eq)
1256 lemma one_eq_divide_iff [simp]:
1257 "(1 = a/b) = (b \<noteq> 0 & a = (b::'a::{field,division_by_zero}))"
1258 by (simp add: eq_commute [of 1])
1260 lemma zero_eq_1_divide_iff [simp]:
1261 "((0::'a::{ordered_field,division_by_zero}) = 1/a) = (a = 0)"
1262 apply (case_tac "a=0", simp)
1263 apply (auto simp add: nonzero_eq_divide_eq)
1266 lemma one_divide_eq_0_iff [simp]:
1267 "(1/a = (0::'a::{ordered_field,division_by_zero})) = (a = 0)"
1268 apply (case_tac "a=0", simp)
1269 apply (insert zero_neq_one [THEN not_sym])
1270 apply (auto simp add: nonzero_divide_eq_eq)
1273 text{*Simplify expressions such as @{text "0 < 1/x"} to @{text "0 < x"}*}
1274 declare zero_less_divide_iff [of "1", simp]
1275 declare divide_less_0_iff [of "1", simp]
1276 declare zero_le_divide_iff [of "1", simp]
1277 declare divide_le_0_iff [of "1", simp]
1280 subsection {* Ordering Rules for Division *}
1282 lemma divide_strict_right_mono:
1283 "[|a < b; 0 < c|] ==> a / c < b / (c::'a::ordered_field)"
1284 by (simp add: order_less_imp_not_eq2 divide_inverse mult_strict_right_mono
1285 positive_imp_inverse_positive)
1287 lemma divide_right_mono:
1288 "[|a \<le> b; 0 \<le> c|] ==> a/c \<le> b/(c::'a::{ordered_field,division_by_zero})"
1289 by (force simp add: divide_strict_right_mono order_le_less)
1292 text{*The last premise ensures that @{term a} and @{term b}
1293 have the same sign*}
1294 lemma divide_strict_left_mono:
1295 "[|b < a; 0 < c; 0 < a*b|] ==> c / a < c / (b::'a::ordered_field)"
1296 by (force simp add: zero_less_mult_iff divide_inverse mult_strict_left_mono
1297 order_less_imp_not_eq order_less_imp_not_eq2
1298 less_imp_inverse_less less_imp_inverse_less_neg)
1300 lemma divide_left_mono:
1301 "[|b \<le> a; 0 \<le> c; 0 < a*b|] ==> c / a \<le> c / (b::'a::ordered_field)"
1302 apply (subgoal_tac "a \<noteq> 0 & b \<noteq> 0")
1304 apply (force simp add: zero_less_mult_iff order_less_imp_not_eq)
1305 apply (case_tac "c=0", simp add: divide_inverse)
1306 apply (force simp add: divide_strict_left_mono order_le_less)
1309 lemma divide_strict_left_mono_neg:
1310 "[|a < b; c < 0; 0 < a*b|] ==> c / a < c / (b::'a::ordered_field)"
1311 apply (subgoal_tac "a \<noteq> 0 & b \<noteq> 0")
1313 apply (force simp add: zero_less_mult_iff order_less_imp_not_eq)
1314 apply (drule divide_strict_left_mono [of _ _ "-c"])
1315 apply (simp_all add: mult_commute nonzero_minus_divide_left [symmetric])
1318 lemma divide_strict_right_mono_neg:
1319 "[|b < a; c < 0|] ==> a / c < b / (c::'a::ordered_field)"
1320 apply (drule divide_strict_right_mono [of _ _ "-c"], simp)
1321 apply (simp add: order_less_imp_not_eq nonzero_minus_divide_right [symmetric])
1325 subsection {* Ordered Fields are Dense *}
1327 lemma less_add_one: "a < (a+1::'a::ordered_semidom)"
1329 have "a+0 < (a+1::'a::ordered_semidom)"
1330 by (blast intro: zero_less_one add_strict_left_mono)
1331 thus ?thesis by simp
1334 lemma zero_less_two: "0 < (1+1::'a::ordered_semidom)"
1335 by (blast intro: order_less_trans zero_less_one less_add_one)
1337 lemma less_half_sum: "a < b ==> a < (a+b) / (1+1::'a::ordered_field)"
1338 by (simp add: zero_less_two pos_less_divide_eq right_distrib)
1340 lemma gt_half_sum: "a < b ==> (a+b)/(1+1::'a::ordered_field) < b"
1341 by (simp add: zero_less_two pos_divide_less_eq right_distrib)
1343 lemma dense: "a < b ==> \<exists>r::'a::ordered_field. a < r & r < b"
1344 by (blast intro!: less_half_sum gt_half_sum)
1346 subsection {* Absolute Value *}
1348 lemma abs_one [simp]: "abs 1 = (1::'a::ordered_idom)"
1349 by (simp add: abs_if zero_less_one [THEN order_less_not_sym])
1351 lemma abs_le_mult: "abs (a * b) \<le> (abs a) * (abs (b::'a::lordered_ring))"
1353 let ?x = "pprt a * pprt b - pprt a * nprt b - nprt a * pprt b + nprt a * nprt b"
1354 let ?y = "pprt a * pprt b + pprt a * nprt b + nprt a * pprt b + nprt a * nprt b"
1355 have a: "(abs a) * (abs b) = ?x"
1356 by (simp only: abs_prts[of a] abs_prts[of b] ring_eq_simps)
1359 have bh: "\<lbrakk>u = a; v = b\<rbrakk> \<Longrightarrow> u * v = ?y"
1360 apply (subst prts[of u], subst prts[of v])
1361 apply (simp add: left_distrib right_distrib add_ac)
1364 note b = this[OF refl[of a] refl[of b]]
1365 note addm = add_mono[of "0::'a" _ "0::'a", simplified]
1366 note addm2 = add_mono[of _ "0::'a" _ "0::'a", simplified]
1367 have xy: "- ?x <= ?y"
1368 apply (simp add: compare_rls)
1369 apply (rule add_le_imp_le_left[of "-(pprt a * nprt b + nprt a * pprt b)"])
1370 apply (simp add: add_ac)
1372 let ?r = "nprt a * nprt b +(nprt a * nprt b + (nprt a * pprt b + (pprt a * nprt b + (pprt a * pprt b + (pprt a * pprt b +
1373 (- (nprt a * pprt b) + - (pprt a * nprt b)))))))"
1374 let ?rr = "nprt a * nprt b + nprt a * nprt b + ((nprt a * pprt b) + (- (nprt a * pprt b))) + ((pprt a * nprt b) + - (pprt a * nprt b))
1375 + pprt a * pprt b + pprt a * pprt b"
1376 have a:"?r = ?rr" by (simp only: add_ac)
1380 apply (simp_all add: mult_neg_le mult_pos_le)
1382 with a show "0 <= ?r" by simp
1385 apply (simp add: add_ac)
1386 apply (simp add: compare_rls)
1387 apply (rule add_le_imp_le_right[of _ "-(pprt a * pprt b)"])
1388 apply (simp add: add_ac)
1389 apply (rule addm2, (simp add: mult_pos_neg_le mult_pos_neg2_le)+)+
1391 have i1: "a*b <= abs a * abs b" by (simp only: a b yx)
1392 have i2: "- (abs a * abs b) <= a*b" by (simp only: a b xy)
1394 apply (rule abs_leI)
1395 apply (simp add: i1)
1396 apply (simp add: i2[simplified minus_le_iff])
1401 assumes "(0 \<le> a \<or> a \<le> 0) \<and> (0 \<le> b \<or> b \<le> 0)"
1402 shows "abs (a*b) = abs a * abs (b::'a::lordered_ring)"
1404 have s: "(0 <= a*b) | (a*b <= 0)"
1406 apply (rule_tac split_mult_pos_le)
1407 apply (rule_tac contrapos_np[of "a*b <= 0"])
1409 apply (rule_tac split_mult_neg_le)
1410 apply (insert prems)
1413 have mulprts: "a * b = (pprt a + nprt a) * (pprt b + nprt b)"
1414 by (simp add: prts[symmetric])
1419 apply (simp_all add: mulprts abs_prts)
1420 apply (insert prems)
1421 apply (auto simp add: ring_eq_simps iff2imp[OF zero_le_iff_zero_nprt] iff2imp[OF le_zero_iff_zero_pprt]
1422 iff2imp[OF le_zero_iff_pprt_id] iff2imp[OF zero_le_iff_nprt_id] order_antisym mult_pos_neg_le[of a b] mult_pos_neg2_le[of b a])
1425 assume "~(0 <= a*b)"
1426 with s have "a*b <= 0" by simp
1428 apply (simp_all add: mulprts abs_prts)
1429 apply (insert prems)
1430 apply (auto simp add: ring_eq_simps iff2imp[OF zero_le_iff_zero_nprt] iff2imp[OF le_zero_iff_zero_pprt]
1431 iff2imp[OF le_zero_iff_pprt_id] iff2imp[OF zero_le_iff_nprt_id] order_antisym mult_pos_le[of a b] mult_neg_le[of a b])
1436 lemma abs_mult: "abs (a * b) = abs a * abs (b::'a::ordered_idom)"
1437 by (simp add: abs_eq_mult linorder_linear)
1439 lemma abs_mult_self: "abs a * abs a = a * (a::'a::ordered_idom)"
1440 by (simp add: abs_if)
1442 lemma nonzero_abs_inverse:
1443 "a \<noteq> 0 ==> abs (inverse (a::'a::ordered_field)) = inverse (abs a)"
1444 apply (auto simp add: linorder_neq_iff abs_if nonzero_inverse_minus_eq
1445 negative_imp_inverse_negative)
1446 apply (blast intro: positive_imp_inverse_positive elim: order_less_asym)
1449 lemma abs_inverse [simp]:
1450 "abs (inverse (a::'a::{ordered_field,division_by_zero})) =
1452 apply (case_tac "a=0", simp)
1453 apply (simp add: nonzero_abs_inverse)
1456 lemma nonzero_abs_divide:
1457 "b \<noteq> 0 ==> abs (a / (b::'a::ordered_field)) = abs a / abs b"
1458 by (simp add: divide_inverse abs_mult nonzero_abs_inverse)
1461 "abs (a / (b::'a::{ordered_field,division_by_zero})) = abs a / abs b"
1462 apply (case_tac "b=0", simp)
1463 apply (simp add: nonzero_abs_divide)
1466 lemma abs_mult_less:
1467 "[| abs a < c; abs b < d |] ==> abs a * abs b < c*(d::'a::ordered_idom)"
1469 assume ac: "abs a < c"
1470 hence cpos: "0<c" by (blast intro: order_le_less_trans abs_ge_zero)
1472 thus ?thesis by (simp add: ac cpos mult_strict_mono)
1475 lemma eq_minus_self_iff: "(a = -a) = (a = (0::'a::ordered_idom))"
1476 by (force simp add: order_eq_iff le_minus_self_iff minus_le_self_iff)
1478 lemma less_minus_self_iff: "(a < -a) = (a < (0::'a::ordered_idom))"
1479 by (simp add: order_less_le le_minus_self_iff eq_minus_self_iff)
1481 lemma abs_less_iff: "(abs a < b) = (a < b & -a < (b::'a::ordered_idom))"
1482 apply (simp add: order_less_le abs_le_iff)
1483 apply (auto simp add: abs_if minus_le_self_iff eq_minus_self_iff)
1484 apply (simp add: le_minus_self_iff linorder_neq_iff)
1487 text{*Moving this up spoils many proofs using @{text mult_le_cancel_right}*}
1488 declare times_divide_eq_left [simp]
1491 val left_distrib = thm "left_distrib";
1492 val right_distrib = thm "right_distrib";
1493 val mult_commute = thm "mult_commute";
1494 val distrib = thm "distrib";
1495 val zero_neq_one = thm "zero_neq_one";
1496 val no_zero_divisors = thm "no_zero_divisors";
1497 val left_inverse = thm "left_inverse";
1498 val divide_inverse = thm "divide_inverse";
1499 val mult_zero_left = thm "mult_zero_left";
1500 val mult_zero_right = thm "mult_zero_right";
1501 val field_mult_eq_0_iff = thm "field_mult_eq_0_iff";
1502 val inverse_zero = thm "inverse_zero";
1503 val ring_distrib = thms "ring_distrib";
1504 val combine_common_factor = thm "combine_common_factor";
1505 val minus_mult_left = thm "minus_mult_left";
1506 val minus_mult_right = thm "minus_mult_right";
1507 val minus_mult_minus = thm "minus_mult_minus";
1508 val minus_mult_commute = thm "minus_mult_commute";
1509 val right_diff_distrib = thm "right_diff_distrib";
1510 val left_diff_distrib = thm "left_diff_distrib";
1511 val mult_left_mono = thm "mult_left_mono";
1512 val mult_right_mono = thm "mult_right_mono";
1513 val mult_strict_left_mono = thm "mult_strict_left_mono";
1514 val mult_strict_right_mono = thm "mult_strict_right_mono";
1515 val mult_mono = thm "mult_mono";
1516 val mult_strict_mono = thm "mult_strict_mono";
1517 val abs_if = thm "abs_if";
1518 val zero_less_one = thm "zero_less_one";
1519 val eq_add_iff1 = thm "eq_add_iff1";
1520 val eq_add_iff2 = thm "eq_add_iff2";
1521 val less_add_iff1 = thm "less_add_iff1";
1522 val less_add_iff2 = thm "less_add_iff2";
1523 val le_add_iff1 = thm "le_add_iff1";
1524 val le_add_iff2 = thm "le_add_iff2";
1525 val mult_left_le_imp_le = thm "mult_left_le_imp_le";
1526 val mult_right_le_imp_le = thm "mult_right_le_imp_le";
1527 val mult_left_less_imp_less = thm "mult_left_less_imp_less";
1528 val mult_right_less_imp_less = thm "mult_right_less_imp_less";
1529 val mult_strict_left_mono_neg = thm "mult_strict_left_mono_neg";
1530 val mult_left_mono_neg = thm "mult_left_mono_neg";
1531 val mult_strict_right_mono_neg = thm "mult_strict_right_mono_neg";
1532 val mult_right_mono_neg = thm "mult_right_mono_neg";
1533 val mult_pos = thm "mult_pos";
1534 val mult_pos_le = thm "mult_pos_le";
1535 val mult_pos_neg = thm "mult_pos_neg";
1536 val mult_pos_neg_le = thm "mult_pos_neg_le";
1537 val mult_pos_neg2 = thm "mult_pos_neg2";
1538 val mult_pos_neg2_le = thm "mult_pos_neg2_le";
1539 val mult_neg = thm "mult_neg";
1540 val mult_neg_le = thm "mult_neg_le";
1541 val zero_less_mult_pos = thm "zero_less_mult_pos";
1542 val zero_less_mult_pos2 = thm "zero_less_mult_pos2";
1543 val zero_less_mult_iff = thm "zero_less_mult_iff";
1544 val mult_eq_0_iff = thm "mult_eq_0_iff";
1545 val zero_le_mult_iff = thm "zero_le_mult_iff";
1546 val mult_less_0_iff = thm "mult_less_0_iff";
1547 val mult_le_0_iff = thm "mult_le_0_iff";
1548 val split_mult_pos_le = thm "split_mult_pos_le";
1549 val split_mult_neg_le = thm "split_mult_neg_le";
1550 val zero_le_square = thm "zero_le_square";
1551 val zero_le_one = thm "zero_le_one";
1552 val not_one_le_zero = thm "not_one_le_zero";
1553 val not_one_less_zero = thm "not_one_less_zero";
1554 val mult_left_mono_neg = thm "mult_left_mono_neg";
1555 val mult_right_mono_neg = thm "mult_right_mono_neg";
1556 val mult_strict_mono = thm "mult_strict_mono";
1557 val mult_strict_mono' = thm "mult_strict_mono'";
1558 val mult_mono = thm "mult_mono";
1559 val less_1_mult = thm "less_1_mult";
1560 val mult_less_cancel_right = thm "mult_less_cancel_right";
1561 val mult_less_cancel_left = thm "mult_less_cancel_left";
1562 val mult_le_cancel_right = thm "mult_le_cancel_right";
1563 val mult_le_cancel_left = thm "mult_le_cancel_left";
1564 val mult_less_imp_less_left = thm "mult_less_imp_less_left";
1565 val mult_less_imp_less_right = thm "mult_less_imp_less_right";
1566 val mult_cancel_right = thm "mult_cancel_right";
1567 val mult_cancel_left = thm "mult_cancel_left";
1568 val ring_eq_simps = thms "ring_eq_simps";
1569 val right_inverse = thm "right_inverse";
1570 val right_inverse_eq = thm "right_inverse_eq";
1571 val nonzero_inverse_eq_divide = thm "nonzero_inverse_eq_divide";
1572 val divide_self = thm "divide_self";
1573 val divide_zero = thm "divide_zero";
1574 val divide_zero_left = thm "divide_zero_left";
1575 val inverse_eq_divide = thm "inverse_eq_divide";
1576 val add_divide_distrib = thm "add_divide_distrib";
1577 val field_mult_eq_0_iff = thm "field_mult_eq_0_iff";
1578 val field_mult_cancel_right_lemma = thm "field_mult_cancel_right_lemma";
1579 val field_mult_cancel_right = thm "field_mult_cancel_right";
1580 val field_mult_cancel_left = thm "field_mult_cancel_left";
1581 val nonzero_imp_inverse_nonzero = thm "nonzero_imp_inverse_nonzero";
1582 val inverse_zero_imp_zero = thm "inverse_zero_imp_zero";
1583 val inverse_nonzero_imp_nonzero = thm "inverse_nonzero_imp_nonzero";
1584 val inverse_nonzero_iff_nonzero = thm "inverse_nonzero_iff_nonzero";
1585 val nonzero_inverse_minus_eq = thm "nonzero_inverse_minus_eq";
1586 val inverse_minus_eq = thm "inverse_minus_eq";
1587 val nonzero_inverse_eq_imp_eq = thm "nonzero_inverse_eq_imp_eq";
1588 val inverse_eq_imp_eq = thm "inverse_eq_imp_eq";
1589 val inverse_eq_iff_eq = thm "inverse_eq_iff_eq";
1590 val nonzero_inverse_inverse_eq = thm "nonzero_inverse_inverse_eq";
1591 val inverse_inverse_eq = thm "inverse_inverse_eq";
1592 val inverse_1 = thm "inverse_1";
1593 val nonzero_inverse_mult_distrib = thm "nonzero_inverse_mult_distrib";
1594 val inverse_mult_distrib = thm "inverse_mult_distrib";
1595 val inverse_add = thm "inverse_add";
1596 val inverse_divide = thm "inverse_divide";
1597 val nonzero_mult_divide_cancel_left = thm "nonzero_mult_divide_cancel_left";
1598 val mult_divide_cancel_left = thm "mult_divide_cancel_left";
1599 val nonzero_mult_divide_cancel_right = thm "nonzero_mult_divide_cancel_right";
1600 val mult_divide_cancel_right = thm "mult_divide_cancel_right";
1601 val mult_divide_cancel_eq_if = thm "mult_divide_cancel_eq_if";
1602 val divide_1 = thm "divide_1";
1603 val times_divide_eq_right = thm "times_divide_eq_right";
1604 val times_divide_eq_left = thm "times_divide_eq_left";
1605 val divide_divide_eq_right = thm "divide_divide_eq_right";
1606 val divide_divide_eq_left = thm "divide_divide_eq_left";
1607 val nonzero_minus_divide_left = thm "nonzero_minus_divide_left";
1608 val nonzero_minus_divide_right = thm "nonzero_minus_divide_right";
1609 val nonzero_minus_divide_divide = thm "nonzero_minus_divide_divide";
1610 val minus_divide_left = thm "minus_divide_left";
1611 val minus_divide_right = thm "minus_divide_right";
1612 val minus_divide_divide = thm "minus_divide_divide";
1613 val diff_divide_distrib = thm "diff_divide_distrib";
1614 val positive_imp_inverse_positive = thm "positive_imp_inverse_positive";
1615 val negative_imp_inverse_negative = thm "negative_imp_inverse_negative";
1616 val inverse_le_imp_le = thm "inverse_le_imp_le";
1617 val inverse_positive_imp_positive = thm "inverse_positive_imp_positive";
1618 val inverse_positive_iff_positive = thm "inverse_positive_iff_positive";
1619 val inverse_negative_imp_negative = thm "inverse_negative_imp_negative";
1620 val inverse_negative_iff_negative = thm "inverse_negative_iff_negative";
1621 val inverse_nonnegative_iff_nonnegative = thm "inverse_nonnegative_iff_nonnegative";
1622 val inverse_nonpositive_iff_nonpositive = thm "inverse_nonpositive_iff_nonpositive";
1623 val less_imp_inverse_less = thm "less_imp_inverse_less";
1624 val inverse_less_imp_less = thm "inverse_less_imp_less";
1625 val inverse_less_iff_less = thm "inverse_less_iff_less";
1626 val le_imp_inverse_le = thm "le_imp_inverse_le";
1627 val inverse_le_iff_le = thm "inverse_le_iff_le";
1628 val inverse_le_imp_le_neg = thm "inverse_le_imp_le_neg";
1629 val less_imp_inverse_less_neg = thm "less_imp_inverse_less_neg";
1630 val inverse_less_imp_less_neg = thm "inverse_less_imp_less_neg";
1631 val inverse_less_iff_less_neg = thm "inverse_less_iff_less_neg";
1632 val le_imp_inverse_le_neg = thm "le_imp_inverse_le_neg";
1633 val inverse_le_iff_le_neg = thm "inverse_le_iff_le_neg";
1634 val one_less_inverse_iff = thm "one_less_inverse_iff";
1635 val inverse_eq_1_iff = thm "inverse_eq_1_iff";
1636 val one_le_inverse_iff = thm "one_le_inverse_iff";
1637 val inverse_less_1_iff = thm "inverse_less_1_iff";
1638 val inverse_le_1_iff = thm "inverse_le_1_iff";
1639 val zero_less_divide_iff = thm "zero_less_divide_iff";
1640 val divide_less_0_iff = thm "divide_less_0_iff";
1641 val zero_le_divide_iff = thm "zero_le_divide_iff";
1642 val divide_le_0_iff = thm "divide_le_0_iff";
1643 val divide_eq_0_iff = thm "divide_eq_0_iff";
1644 val pos_le_divide_eq = thm "pos_le_divide_eq";
1645 val neg_le_divide_eq = thm "neg_le_divide_eq";
1646 val le_divide_eq = thm "le_divide_eq";
1647 val pos_divide_le_eq = thm "pos_divide_le_eq";
1648 val neg_divide_le_eq = thm "neg_divide_le_eq";
1649 val divide_le_eq = thm "divide_le_eq";
1650 val pos_less_divide_eq = thm "pos_less_divide_eq";
1651 val neg_less_divide_eq = thm "neg_less_divide_eq";
1652 val less_divide_eq = thm "less_divide_eq";
1653 val pos_divide_less_eq = thm "pos_divide_less_eq";
1654 val neg_divide_less_eq = thm "neg_divide_less_eq";
1655 val divide_less_eq = thm "divide_less_eq";
1656 val nonzero_eq_divide_eq = thm "nonzero_eq_divide_eq";
1657 val eq_divide_eq = thm "eq_divide_eq";
1658 val nonzero_divide_eq_eq = thm "nonzero_divide_eq_eq";
1659 val divide_eq_eq = thm "divide_eq_eq";
1660 val divide_cancel_right = thm "divide_cancel_right";
1661 val divide_cancel_left = thm "divide_cancel_left";
1662 val divide_eq_1_iff = thm "divide_eq_1_iff";
1663 val one_eq_divide_iff = thm "one_eq_divide_iff";
1664 val zero_eq_1_divide_iff = thm "zero_eq_1_divide_iff";
1665 val one_divide_eq_0_iff = thm "one_divide_eq_0_iff";
1666 val divide_strict_right_mono = thm "divide_strict_right_mono";
1667 val divide_right_mono = thm "divide_right_mono";
1668 val divide_strict_left_mono = thm "divide_strict_left_mono";
1669 val divide_left_mono = thm "divide_left_mono";
1670 val divide_strict_left_mono_neg = thm "divide_strict_left_mono_neg";
1671 val divide_strict_right_mono_neg = thm "divide_strict_right_mono_neg";
1672 val less_add_one = thm "less_add_one";
1673 val zero_less_two = thm "zero_less_two";
1674 val less_half_sum = thm "less_half_sum";
1675 val gt_half_sum = thm "gt_half_sum";
1676 val dense = thm "dense";
1677 val abs_one = thm "abs_one";
1678 val abs_le_mult = thm "abs_le_mult";
1679 val abs_eq_mult = thm "abs_eq_mult";
1680 val abs_mult = thm "abs_mult";
1681 val abs_mult_self = thm "abs_mult_self";
1682 val nonzero_abs_inverse = thm "nonzero_abs_inverse";
1683 val abs_inverse = thm "abs_inverse";
1684 val nonzero_abs_divide = thm "nonzero_abs_divide";
1685 val abs_divide = thm "abs_divide";
1686 val abs_mult_less = thm "abs_mult_less";
1687 val eq_minus_self_iff = thm "eq_minus_self_iff";
1688 val less_minus_self_iff = thm "less_minus_self_iff";
1689 val abs_less_iff = thm "abs_less_iff";