src/HOL/Ring_and_Field.thy
 author haftmann Thu Oct 18 09:20:58 2007 +0200 (2007-10-18) changeset 25078 a1ddc5206cb1 parent 25062 af5ef0d4d655 child 25152 bfde2f8c0f63 permissions -rw-r--r--
moved lemmas to OrderedGroup.thy
1 (*  Title:   HOL/Ring_and_Field.thy
2     ID:      $Id$
3     Author:  Gertrud Bauer, Steven Obua, Tobias Nipkow, Lawrence C Paulson, and Markus Wenzel,
4              with contributions by Jeremy Avigad
5 *)
7 header {* (Ordered) Rings and Fields *}
9 theory Ring_and_Field
10 imports OrderedGroup
11 begin
13 text {*
14   The theory of partially ordered rings is taken from the books:
15   \begin{itemize}
16   \item \emph{Lattice Theory} by Garret Birkhoff, American Mathematical Society 1979
17   \item \emph{Partially Ordered Algebraic Systems}, Pergamon Press 1963
18   \end{itemize}
19   Most of the used notions can also be looked up in
20   \begin{itemize}
21   \item \url{http://www.mathworld.com} by Eric Weisstein et. al.
22   \item \emph{Algebra I} by van der Waerden, Springer.
23   \end{itemize}
24 *}
26 class semiring = ab_semigroup_add + semigroup_mult +
27   assumes left_distrib: "(a + b) * c = a * c + b * c"
28   assumes right_distrib: "a * (b + c) = a * b + a * c"
30 class mult_zero = times + zero +
31   assumes mult_zero_left [simp]: "0 * a = 0"
32   assumes mult_zero_right [simp]: "a * 0 = 0"
34 class semiring_0 = semiring + comm_monoid_add + mult_zero
38 instance semiring_0_cancel \<subseteq> semiring_0
39 proof
40   fix a :: 'a
41   have "0 * a + 0 * a = 0 * a + 0"
42     by (simp add: left_distrib [symmetric])
43   thus "0 * a = 0"
46   have "a * 0 + a * 0 = a * 0 + 0"
47     by (simp add: right_distrib [symmetric])
48   thus "a * 0 = 0"
50 qed
52 class comm_semiring = ab_semigroup_add + ab_semigroup_mult +
53   assumes distrib: "(a + b) * c = a * c + b * c"
55 instance comm_semiring \<subseteq> semiring
56 proof
57   fix a b c :: 'a
58   show "(a + b) * c = a * c + b * c" by (simp add: distrib)
59   have "a * (b + c) = (b + c) * a" by (simp add: mult_ac)
60   also have "... = b * a + c * a" by (simp only: distrib)
61   also have "... = a * b + a * c" by (simp add: mult_ac)
62   finally show "a * (b + c) = a * b + a * c" by blast
63 qed
65 class comm_semiring_0 = comm_semiring + comm_monoid_add + mult_zero
67 instance comm_semiring_0 \<subseteq> semiring_0 ..
71 instance comm_semiring_0_cancel \<subseteq> semiring_0_cancel ..
73 instance comm_semiring_0_cancel \<subseteq> comm_semiring_0 ..
75 class zero_neq_one = zero + one +
76   assumes zero_neq_one [simp]: "0 \<noteq> 1"
78 class semiring_1 = zero_neq_one + semiring_0 + monoid_mult
80 class comm_semiring_1 = zero_neq_one + comm_semiring_0 + comm_monoid_mult
81   (*previously almost_semiring*)
83 instance comm_semiring_1 \<subseteq> semiring_1 ..
85 class no_zero_divisors = zero + times +
86   assumes no_zero_divisors: "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> a * b \<noteq> 0"
88 class semiring_1_cancel = semiring + comm_monoid_add + zero_neq_one
91 instance semiring_1_cancel \<subseteq> semiring_0_cancel ..
93 instance semiring_1_cancel \<subseteq> semiring_1 ..
95 class comm_semiring_1_cancel = comm_semiring + comm_monoid_add + comm_monoid_mult
98 instance comm_semiring_1_cancel \<subseteq> semiring_1_cancel ..
100 instance comm_semiring_1_cancel \<subseteq> comm_semiring_0_cancel ..
102 instance comm_semiring_1_cancel \<subseteq> comm_semiring_1 ..
104 class ring = semiring + ab_group_add
106 instance ring \<subseteq> semiring_0_cancel ..
108 class comm_ring = comm_semiring + ab_group_add
110 instance comm_ring \<subseteq> ring ..
112 instance comm_ring \<subseteq> comm_semiring_0_cancel ..
114 class ring_1 = ring + zero_neq_one + monoid_mult
116 instance ring_1 \<subseteq> semiring_1_cancel ..
118 class comm_ring_1 = comm_ring + zero_neq_one + comm_monoid_mult
119   (*previously ring*)
121 instance comm_ring_1 \<subseteq> ring_1 ..
123 instance comm_ring_1 \<subseteq> comm_semiring_1_cancel ..
125 class ring_no_zero_divisors = ring + no_zero_divisors
127 class ring_1_no_zero_divisors = ring_1 + ring_no_zero_divisors
129 class idom = comm_ring_1 + no_zero_divisors
131 instance idom \<subseteq> ring_1_no_zero_divisors ..
133 class division_ring = ring_1 + inverse +
134   assumes left_inverse [simp]:  "a \<noteq> 0 \<Longrightarrow> inverse a * a = 1"
135   assumes right_inverse [simp]: "a \<noteq> 0 \<Longrightarrow> a * inverse a = 1"
137 instance division_ring \<subseteq> ring_1_no_zero_divisors
138 proof
139   fix a b :: 'a
140   assume a: "a \<noteq> 0" and b: "b \<noteq> 0"
141   show "a * b \<noteq> 0"
142   proof
143     assume ab: "a * b = 0"
144     hence "0 = inverse a * (a * b) * inverse b"
145       by simp
146     also have "\<dots> = (inverse a * a) * (b * inverse b)"
147       by (simp only: mult_assoc)
148     also have "\<dots> = 1"
149       using a b by simp
150     finally show False
151       by simp
152   qed
153 qed
155 class field = comm_ring_1 + inverse +
156   assumes field_inverse:  "a \<noteq> 0 \<Longrightarrow> inverse a * a = 1"
157   assumes divide_inverse: "a / b = a * inverse b"
159 instance field \<subseteq> division_ring
160 proof
161   fix a :: 'a
162   assume "a \<noteq> 0"
163   thus "inverse a * a = 1" by (rule field_inverse)
164   thus "a * inverse a = 1" by (simp only: mult_commute)
165 qed
167 instance field \<subseteq> idom ..
169 class division_by_zero = zero + inverse +
170   assumes inverse_zero [simp]: "inverse 0 = 0"
173 subsection {* Distribution rules *}
175 text{*For the @{text combine_numerals} simproc*}
176 lemma combine_common_factor:
177      "a*e + (b*e + c) = (a+b)*e + (c::'a::semiring)"
180 lemma minus_mult_left: "- (a * b) = (-a) * (b::'a::ring)"
181 apply (rule equals_zero_I)
182 apply (simp add: left_distrib [symmetric])
183 done
185 lemma minus_mult_right: "- (a * b) = a * -(b::'a::ring)"
186 apply (rule equals_zero_I)
187 apply (simp add: right_distrib [symmetric])
188 done
190 lemma minus_mult_minus [simp]: "(- a) * (- b) = a * (b::'a::ring)"
191   by (simp add: minus_mult_left [symmetric] minus_mult_right [symmetric])
193 lemma minus_mult_commute: "(- a) * b = a * (- b::'a::ring)"
194   by (simp add: minus_mult_left [symmetric] minus_mult_right [symmetric])
196 lemma right_diff_distrib: "a * (b - c) = a * b - a * (c::'a::ring)"
197 by (simp add: right_distrib diff_minus
198               minus_mult_left [symmetric] minus_mult_right [symmetric])
200 lemma left_diff_distrib: "(a - b) * c = a * c - b * (c::'a::ring)"
201 by (simp add: left_distrib diff_minus
202               minus_mult_left [symmetric] minus_mult_right [symmetric])
204 lemmas ring_distribs =
205   right_distrib left_distrib left_diff_distrib right_diff_distrib
207 text{*This list of rewrites simplifies ring terms by multiplying
208 everything out and bringing sums and products into a canonical form
209 (by ordered rewriting). As a result it decides ring equalities but
210 also helps with inequalities. *}
211 lemmas ring_simps = group_simps ring_distribs
213 class mult_mono = times + zero + ord +
214   assumes mult_left_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b"
215   assumes mult_right_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a * c \<le> b * c"
217 class pordered_semiring = mult_mono + semiring_0 + pordered_ab_semigroup_add
219 class pordered_cancel_semiring = mult_mono + pordered_ab_semigroup_add
222 instance pordered_cancel_semiring \<subseteq> semiring_0_cancel ..
224 instance pordered_cancel_semiring \<subseteq> pordered_semiring ..
228 instance ordered_semiring \<subseteq> pordered_cancel_semiring ..
231   assumes mult_strict_left_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b"
232   assumes mult_strict_right_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> a * c < b * c"
234 instance ordered_semiring_strict \<subseteq> semiring_0_cancel ..
236 instance ordered_semiring_strict \<subseteq> ordered_semiring
237 proof
238   fix a b c :: 'a
239   assume A: "a \<le> b" "0 \<le> c"
240   from A show "c * a \<le> c * b"
241     unfolding order_le_less
242     using mult_strict_left_mono by auto
243   from A show "a * c \<le> b * c"
244     unfolding order_le_less
245     using mult_strict_right_mono by auto
246 qed
248 class mult_mono1 = times + zero + ord +
249   assumes mult_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b"
251 class pordered_comm_semiring = comm_semiring_0
254 class pordered_cancel_comm_semiring = comm_semiring_0_cancel
257 instance pordered_cancel_comm_semiring \<subseteq> pordered_comm_semiring ..
259 class ordered_comm_semiring_strict = comm_semiring_0 + ordered_cancel_ab_semigroup_add +
260   assumes mult_strict_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b"
262 instance pordered_comm_semiring \<subseteq> pordered_semiring
263 proof
264   fix a b c :: 'a
265   assume "a \<le> b" "0 \<le> c"
266   thus "c * a \<le> c * b" by (rule mult_mono)
267   thus "a * c \<le> b * c" by (simp only: mult_commute)
268 qed
270 instance pordered_cancel_comm_semiring \<subseteq> pordered_cancel_semiring ..
272 instance ordered_comm_semiring_strict \<subseteq> ordered_semiring_strict
273 proof
274   fix a b c :: 'a
275   assume "a < b" "0 < c"
276   thus "c * a < c * b" by (rule mult_strict_mono)
277   thus "a * c < b * c" by (simp only: mult_commute)
278 qed
280 instance ordered_comm_semiring_strict \<subseteq> pordered_cancel_comm_semiring
281 proof
282   fix a b c :: 'a
283   assume "a \<le> b" "0 \<le> c"
284   thus "c * a \<le> c * b"
285     unfolding order_le_less
286     using mult_strict_mono by auto
287 qed
289 class pordered_ring = ring + pordered_cancel_semiring
291 instance pordered_ring \<subseteq> pordered_ab_group_add ..
293 class lordered_ring = pordered_ring + lordered_ab_group_abs
295 instance lordered_ring \<subseteq> lordered_ab_group_meet ..
297 instance lordered_ring \<subseteq> lordered_ab_group_join ..
299 class abs_if = minus + ord + zero + abs +
300   assumes abs_if: "abs a = (if a < 0 then (uminus a) else a)"
302 class sgn_if = sgn + zero + one + minus + ord +
303   assumes sgn_if: "sgn x = (if x = 0 then 0 else if 0 < x then 1 else uminus 1)"
305 (* The "strict" suffix can be seen as describing the combination of ordered_ring and no_zero_divisors.
306    Basically, ordered_ring + no_zero_divisors = ordered_ring_strict.
307  *)
308 class ordered_ring = ring + ordered_semiring + lordered_ab_group + abs_if
310 instance ordered_ring \<subseteq> lordered_ring
311 proof
312   fix x :: 'a
313   show "\<bar>x\<bar> = sup x (- x)"
314     by (simp only: abs_if sup_eq_if)
315 qed
317 class ordered_ring_strict =
318   ring + ordered_semiring_strict + lordered_ab_group + abs_if
320 instance ordered_ring_strict \<subseteq> ordered_ring ..
322 class pordered_comm_ring = comm_ring + pordered_comm_semiring
324 instance pordered_comm_ring \<subseteq> pordered_ring ..
326 instance pordered_comm_ring \<subseteq> pordered_cancel_comm_semiring ..
328 class ordered_semidom = comm_semiring_1_cancel + ordered_comm_semiring_strict +
329   (*previously ordered_semiring*)
330   assumes zero_less_one [simp]: "0 < 1"
333   fixes a b c :: "'a\<Colon>ordered_semidom"
334   shows "0 < a \<Longrightarrow> b < c \<Longrightarrow> b < a + c"
335   using add_strict_mono [of 0 a b c] by simp
337 class ordered_idom =
338   comm_ring_1 +
339   ordered_comm_semiring_strict +
340   lordered_ab_group +
341   abs_if + sgn_if
342   (*previously ordered_ring*)
344 instance ordered_idom \<subseteq> ordered_ring_strict ..
346 instance ordered_idom \<subseteq> pordered_comm_ring ..
348 class ordered_field = field + ordered_idom
350 lemma linorder_neqE_ordered_idom:
351   fixes x y :: "'a :: ordered_idom"
352   assumes "x \<noteq> y" obtains "x < y" | "y < x"
353   using assms by (rule linorder_neqE)
356   "(a*e + c = b*e + d) = ((a-b)*e + c = (d::'a::ring))"
360   "(a*e + c = b*e + d) = (c = (b-a)*e + (d::'a::ring))"
364   "(a*e + c < b*e + d) = ((a-b)*e + c < (d::'a::pordered_ring))"
368   "(a*e + c < b*e + d) = (c < (b-a)*e + (d::'a::pordered_ring))"
372   "(a*e + c \<le> b*e + d) = ((a-b)*e + c \<le> (d::'a::pordered_ring))"
376   "(a*e + c \<le> b*e + d) = (c \<le> (b-a)*e + (d::'a::pordered_ring))"
380 subsection {* Ordering Rules for Multiplication *}
382 lemma mult_left_le_imp_le:
383   "[|c*a \<le> c*b; 0 < c|] ==> a \<le> (b::'a::ordered_semiring_strict)"
384 by (force simp add: mult_strict_left_mono linorder_not_less [symmetric])
386 lemma mult_right_le_imp_le:
387   "[|a*c \<le> b*c; 0 < c|] ==> a \<le> (b::'a::ordered_semiring_strict)"
388 by (force simp add: mult_strict_right_mono linorder_not_less [symmetric])
390 lemma mult_left_less_imp_less:
391   "[|c*a < c*b; 0 \<le> c|] ==> a < (b::'a::ordered_semiring)"
392 by (force simp add: mult_left_mono linorder_not_le [symmetric])
394 lemma mult_right_less_imp_less:
395   "[|a*c < b*c; 0 \<le> c|] ==> a < (b::'a::ordered_semiring)"
396 by (force simp add: mult_right_mono linorder_not_le [symmetric])
398 lemma mult_strict_left_mono_neg:
399   "[|b < a; c < 0|] ==> c * a < c * (b::'a::ordered_ring_strict)"
400 apply (drule mult_strict_left_mono [of _ _ "-c"])
401 apply (simp_all add: minus_mult_left [symmetric])
402 done
404 lemma mult_left_mono_neg:
405   "[|b \<le> a; c \<le> 0|] ==> c * a \<le>  c * (b::'a::pordered_ring)"
406 apply (drule mult_left_mono [of _ _ "-c"])
407 apply (simp_all add: minus_mult_left [symmetric])
408 done
410 lemma mult_strict_right_mono_neg:
411   "[|b < a; c < 0|] ==> a * c < b * (c::'a::ordered_ring_strict)"
412 apply (drule mult_strict_right_mono [of _ _ "-c"])
413 apply (simp_all add: minus_mult_right [symmetric])
414 done
416 lemma mult_right_mono_neg:
417   "[|b \<le> a; c \<le> 0|] ==> a * c \<le>  (b::'a::pordered_ring) * c"
418 apply (drule mult_right_mono [of _ _ "-c"])
419 apply (simp)
420 apply (simp_all add: minus_mult_right [symmetric])
421 done
424 subsection{* Products of Signs *}
426 lemma mult_pos_pos: "[| (0::'a::ordered_semiring_strict) < a; 0 < b |] ==> 0 < a*b"
427 by (drule mult_strict_left_mono [of 0 b], auto)
429 lemma mult_nonneg_nonneg: "[| (0::'a::pordered_cancel_semiring) \<le> a; 0 \<le> b |] ==> 0 \<le> a*b"
430 by (drule mult_left_mono [of 0 b], auto)
432 lemma mult_pos_neg: "[| (0::'a::ordered_semiring_strict) < a; b < 0 |] ==> a*b < 0"
433 by (drule mult_strict_left_mono [of b 0], auto)
435 lemma mult_nonneg_nonpos: "[| (0::'a::pordered_cancel_semiring) \<le> a; b \<le> 0 |] ==> a*b \<le> 0"
436 by (drule mult_left_mono [of b 0], auto)
438 lemma mult_pos_neg2: "[| (0::'a::ordered_semiring_strict) < a; b < 0 |] ==> b*a < 0"
439 by (drule mult_strict_right_mono[of b 0], auto)
441 lemma mult_nonneg_nonpos2: "[| (0::'a::pordered_cancel_semiring) \<le> a; b \<le> 0 |] ==> b*a \<le> 0"
442 by (drule mult_right_mono[of b 0], auto)
444 lemma mult_neg_neg: "[| a < (0::'a::ordered_ring_strict); b < 0 |] ==> 0 < a*b"
445 by (drule mult_strict_right_mono_neg, auto)
447 lemma mult_nonpos_nonpos: "[| a \<le> (0::'a::pordered_ring); b \<le> 0 |] ==> 0 \<le> a*b"
448 by (drule mult_right_mono_neg[of a 0 b ], auto)
450 lemma zero_less_mult_pos:
451      "[| 0 < a*b; 0 < a|] ==> 0 < (b::'a::ordered_semiring_strict)"
452 apply (cases "b\<le>0")
453  apply (auto simp add: order_le_less linorder_not_less)
454 apply (drule_tac mult_pos_neg [of a b])
455  apply (auto dest: order_less_not_sym)
456 done
458 lemma zero_less_mult_pos2:
459      "[| 0 < b*a; 0 < a|] ==> 0 < (b::'a::ordered_semiring_strict)"
460 apply (cases "b\<le>0")
461  apply (auto simp add: order_le_less linorder_not_less)
462 apply (drule_tac mult_pos_neg2 [of a b])
463  apply (auto dest: order_less_not_sym)
464 done
466 lemma zero_less_mult_iff:
467      "((0::'a::ordered_ring_strict) < a*b) = (0 < a & 0 < b | a < 0 & b < 0)"
468 apply (auto simp add: order_le_less linorder_not_less mult_pos_pos
469   mult_neg_neg)
470 apply (blast dest: zero_less_mult_pos)
471 apply (blast dest: zero_less_mult_pos2)
472 done
474 lemma mult_eq_0_iff [simp]:
475   fixes a b :: "'a::ring_no_zero_divisors"
476   shows "(a * b = 0) = (a = 0 \<or> b = 0)"
477 by (cases "a = 0 \<or> b = 0", auto dest: no_zero_divisors)
479 instance ordered_ring_strict \<subseteq> ring_no_zero_divisors
480 apply intro_classes
481 apply (auto simp add: linorder_not_less order_le_less linorder_neq_iff)
482 apply (force dest: mult_strict_right_mono_neg mult_strict_right_mono)+
483 done
485 lemma zero_le_mult_iff:
486      "((0::'a::ordered_ring_strict) \<le> a*b) = (0 \<le> a & 0 \<le> b | a \<le> 0 & b \<le> 0)"
487 by (auto simp add: eq_commute [of 0] order_le_less linorder_not_less
488                    zero_less_mult_iff)
490 lemma mult_less_0_iff:
491      "(a*b < (0::'a::ordered_ring_strict)) = (0 < a & b < 0 | a < 0 & 0 < b)"
492 apply (insert zero_less_mult_iff [of "-a" b])
493 apply (force simp add: minus_mult_left[symmetric])
494 done
496 lemma mult_le_0_iff:
497      "(a*b \<le> (0::'a::ordered_ring_strict)) = (0 \<le> a & b \<le> 0 | a \<le> 0 & 0 \<le> b)"
498 apply (insert zero_le_mult_iff [of "-a" b])
499 apply (force simp add: minus_mult_left[symmetric])
500 done
502 lemma split_mult_pos_le: "(0 \<le> a & 0 \<le> b) | (a \<le> 0 & b \<le> 0) \<Longrightarrow> 0 \<le> a * (b::_::pordered_ring)"
503 by (auto simp add: mult_nonneg_nonneg mult_nonpos_nonpos)
505 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)"
506 by (auto simp add: mult_nonneg_nonpos mult_nonneg_nonpos2)
508 lemma zero_le_square[simp]: "(0::'a::ordered_ring_strict) \<le> a*a"
509 by (simp add: zero_le_mult_iff linorder_linear)
511 lemma not_square_less_zero[simp]: "\<not> (a * a < (0::'a::ordered_ring_strict))"
514 text{*Proving axiom @{text zero_less_one} makes all @{text ordered_semidom}
515       theorems available to members of @{term ordered_idom} *}
517 instance ordered_idom \<subseteq> ordered_semidom
518 proof
519   have "(0::'a) \<le> 1*1" by (rule zero_le_square)
520   thus "(0::'a) < 1" by (simp add: order_le_less)
521 qed
523 instance ordered_idom \<subseteq> idom ..
525 text{*All three types of comparision involving 0 and 1 are covered.*}
527 lemmas one_neq_zero = zero_neq_one [THEN not_sym]
528 declare one_neq_zero [simp]
530 lemma zero_le_one [simp]: "(0::'a::ordered_semidom) \<le> 1"
531   by (rule zero_less_one [THEN order_less_imp_le])
533 lemma not_one_le_zero [simp]: "~ (1::'a::ordered_semidom) \<le> 0"
536 lemma not_one_less_zero [simp]: "~ (1::'a::ordered_semidom) < 0"
540 subsection{*More Monotonicity*}
542 text{*Strict monotonicity in both arguments*}
543 lemma mult_strict_mono:
544      "[|a<b; c<d; 0<b; 0\<le>c|] ==> a * c < b * (d::'a::ordered_semiring_strict)"
545 apply (cases "c=0")
547 apply (erule mult_strict_right_mono [THEN order_less_trans])
548  apply (force simp add: order_le_less)
549 apply (erule mult_strict_left_mono, assumption)
550 done
552 text{*This weaker variant has more natural premises*}
553 lemma mult_strict_mono':
554      "[| a<b; c<d; 0 \<le> a; 0 \<le> c|] ==> a * c < b * (d::'a::ordered_semiring_strict)"
555 apply (rule mult_strict_mono)
556 apply (blast intro: order_le_less_trans)+
557 done
559 lemma mult_mono:
560      "[|a \<le> b; c \<le> d; 0 \<le> b; 0 \<le> c|]
561       ==> a * c  \<le>  b * (d::'a::pordered_semiring)"
562 apply (erule mult_right_mono [THEN order_trans], assumption)
563 apply (erule mult_left_mono, assumption)
564 done
566 lemma mult_mono':
567      "[|a \<le> b; c \<le> d; 0 \<le> a; 0 \<le> c|]
568       ==> a * c  \<le>  b * (d::'a::pordered_semiring)"
569 apply (rule mult_mono)
570 apply (fast intro: order_trans)+
571 done
573 lemma less_1_mult: "[| 1 < m; 1 < n |] ==> 1 < m*(n::'a::ordered_semidom)"
574 apply (insert mult_strict_mono [of 1 m 1 n])
575 apply (simp add:  order_less_trans [OF zero_less_one])
576 done
578 lemma mult_less_le_imp_less: "(a::'a::ordered_semiring_strict) < b ==>
579     c <= d ==> 0 <= a ==> 0 < c ==> a * c < b * d"
580   apply (subgoal_tac "a * c < b * c")
581   apply (erule order_less_le_trans)
582   apply (erule mult_left_mono)
583   apply simp
584   apply (erule mult_strict_right_mono)
585   apply assumption
586 done
588 lemma mult_le_less_imp_less: "(a::'a::ordered_semiring_strict) <= b ==>
589     c < d ==> 0 < a ==> 0 <= c ==> a * c < b * d"
590   apply (subgoal_tac "a * c <= b * c")
591   apply (erule order_le_less_trans)
592   apply (erule mult_strict_left_mono)
593   apply simp
594   apply (erule mult_right_mono)
595   apply simp
596 done
599 subsection{*Cancellation Laws for Relationships With a Common Factor*}
601 text{*Cancellation laws for @{term "c*a < c*b"} and @{term "a*c < b*c"},
602    also with the relations @{text "\<le>"} and equality.*}
604 text{*These disjunction'' versions produce two cases when the comparison is
605  an assumption, but effectively four when the comparison is a goal.*}
607 lemma mult_less_cancel_right_disj:
608     "(a*c < b*c) = ((0 < c & a < b) | (c < 0 & b < (a::'a::ordered_ring_strict)))"
609 apply (cases "c = 0")
610 apply (auto simp add: linorder_neq_iff mult_strict_right_mono
611                       mult_strict_right_mono_neg)
612 apply (auto simp add: linorder_not_less
613                       linorder_not_le [symmetric, of "a*c"]
614                       linorder_not_le [symmetric, of a])
615 apply (erule_tac [!] notE)
616 apply (auto simp add: order_less_imp_le mult_right_mono
617                       mult_right_mono_neg)
618 done
620 lemma mult_less_cancel_left_disj:
621     "(c*a < c*b) = ((0 < c & a < b) | (c < 0 & b < (a::'a::ordered_ring_strict)))"
622 apply (cases "c = 0")
623 apply (auto simp add: linorder_neq_iff mult_strict_left_mono
624                       mult_strict_left_mono_neg)
625 apply (auto simp add: linorder_not_less
626                       linorder_not_le [symmetric, of "c*a"]
627                       linorder_not_le [symmetric, of a])
628 apply (erule_tac [!] notE)
629 apply (auto simp add: order_less_imp_le mult_left_mono
630                       mult_left_mono_neg)
631 done
634 text{*The conjunction of implication'' lemmas produce two cases when the
635 comparison is a goal, but give four when the comparison is an assumption.*}
637 lemma mult_less_cancel_right:
638   fixes c :: "'a :: ordered_ring_strict"
639   shows      "(a*c < b*c) = ((0 \<le> c --> a < b) & (c \<le> 0 --> b < a))"
640 by (insert mult_less_cancel_right_disj [of a c b], auto)
642 lemma mult_less_cancel_left:
643   fixes c :: "'a :: ordered_ring_strict"
644   shows      "(c*a < c*b) = ((0 \<le> c --> a < b) & (c \<le> 0 --> b < a))"
645 by (insert mult_less_cancel_left_disj [of c a b], auto)
647 lemma mult_le_cancel_right:
648      "(a*c \<le> b*c) = ((0<c --> a\<le>b) & (c<0 --> b \<le> (a::'a::ordered_ring_strict)))"
649 by (simp add: linorder_not_less [symmetric] mult_less_cancel_right_disj)
651 lemma mult_le_cancel_left:
652      "(c*a \<le> c*b) = ((0<c --> a\<le>b) & (c<0 --> b \<le> (a::'a::ordered_ring_strict)))"
653 by (simp add: linorder_not_less [symmetric] mult_less_cancel_left_disj)
655 lemma mult_less_imp_less_left:
656       assumes less: "c*a < c*b" and nonneg: "0 \<le> c"
657       shows "a < (b::'a::ordered_semiring_strict)"
658 proof (rule ccontr)
659   assume "~ a < b"
660   hence "b \<le> a" by (simp add: linorder_not_less)
661   hence "c*b \<le> c*a" using nonneg by (rule mult_left_mono)
662   with this and less show False
663     by (simp add: linorder_not_less [symmetric])
664 qed
666 lemma mult_less_imp_less_right:
667   assumes less: "a*c < b*c" and nonneg: "0 <= c"
668   shows "a < (b::'a::ordered_semiring_strict)"
669 proof (rule ccontr)
670   assume "~ a < b"
671   hence "b \<le> a" by (simp add: linorder_not_less)
672   hence "b*c \<le> a*c" using nonneg by (rule mult_right_mono)
673   with this and less show False
674     by (simp add: linorder_not_less [symmetric])
675 qed
677 text{*Cancellation of equalities with a common factor*}
678 lemma mult_cancel_right [simp,noatp]:
679   fixes a b c :: "'a::ring_no_zero_divisors"
680   shows "(a * c = b * c) = (c = 0 \<or> a = b)"
681 proof -
682   have "(a * c = b * c) = ((a - b) * c = 0)"
684   thus ?thesis
686 qed
688 lemma mult_cancel_left [simp,noatp]:
689   fixes a b c :: "'a::ring_no_zero_divisors"
690   shows "(c * a = c * b) = (c = 0 \<or> a = b)"
691 proof -
692   have "(c * a = c * b) = (c * (a - b) = 0)"
694   thus ?thesis
695     by simp
696 qed
699 subsubsection{*Special Cancellation Simprules for Multiplication*}
701 text{*These also produce two cases when the comparison is a goal.*}
703 lemma mult_le_cancel_right1:
704   fixes c :: "'a :: ordered_idom"
705   shows "(c \<le> b*c) = ((0<c --> 1\<le>b) & (c<0 --> b \<le> 1))"
706 by (insert mult_le_cancel_right [of 1 c b], simp)
708 lemma mult_le_cancel_right2:
709   fixes c :: "'a :: ordered_idom"
710   shows "(a*c \<le> c) = ((0<c --> a\<le>1) & (c<0 --> 1 \<le> a))"
711 by (insert mult_le_cancel_right [of a c 1], simp)
713 lemma mult_le_cancel_left1:
714   fixes c :: "'a :: ordered_idom"
715   shows "(c \<le> c*b) = ((0<c --> 1\<le>b) & (c<0 --> b \<le> 1))"
716 by (insert mult_le_cancel_left [of c 1 b], simp)
718 lemma mult_le_cancel_left2:
719   fixes c :: "'a :: ordered_idom"
720   shows "(c*a \<le> c) = ((0<c --> a\<le>1) & (c<0 --> 1 \<le> a))"
721 by (insert mult_le_cancel_left [of c a 1], simp)
723 lemma mult_less_cancel_right1:
724   fixes c :: "'a :: ordered_idom"
725   shows "(c < b*c) = ((0 \<le> c --> 1<b) & (c \<le> 0 --> b < 1))"
726 by (insert mult_less_cancel_right [of 1 c b], simp)
728 lemma mult_less_cancel_right2:
729   fixes c :: "'a :: ordered_idom"
730   shows "(a*c < c) = ((0 \<le> c --> a<1) & (c \<le> 0 --> 1 < a))"
731 by (insert mult_less_cancel_right [of a c 1], simp)
733 lemma mult_less_cancel_left1:
734   fixes c :: "'a :: ordered_idom"
735   shows "(c < c*b) = ((0 \<le> c --> 1<b) & (c \<le> 0 --> b < 1))"
736 by (insert mult_less_cancel_left [of c 1 b], simp)
738 lemma mult_less_cancel_left2:
739   fixes c :: "'a :: ordered_idom"
740   shows "(c*a < c) = ((0 \<le> c --> a<1) & (c \<le> 0 --> 1 < a))"
741 by (insert mult_less_cancel_left [of c a 1], simp)
743 lemma mult_cancel_right1 [simp]:
744   fixes c :: "'a :: ring_1_no_zero_divisors"
745   shows "(c = b*c) = (c = 0 | b=1)"
746 by (insert mult_cancel_right [of 1 c b], force)
748 lemma mult_cancel_right2 [simp]:
749   fixes c :: "'a :: ring_1_no_zero_divisors"
750   shows "(a*c = c) = (c = 0 | a=1)"
751 by (insert mult_cancel_right [of a c 1], simp)
753 lemma mult_cancel_left1 [simp]:
754   fixes c :: "'a :: ring_1_no_zero_divisors"
755   shows "(c = c*b) = (c = 0 | b=1)"
756 by (insert mult_cancel_left [of c 1 b], force)
758 lemma mult_cancel_left2 [simp]:
759   fixes c :: "'a :: ring_1_no_zero_divisors"
760   shows "(c*a = c) = (c = 0 | a=1)"
761 by (insert mult_cancel_left [of c a 1], simp)
764 text{*Simprules for comparisons where common factors can be cancelled.*}
765 lemmas mult_compare_simps =
766     mult_le_cancel_right mult_le_cancel_left
767     mult_le_cancel_right1 mult_le_cancel_right2
768     mult_le_cancel_left1 mult_le_cancel_left2
769     mult_less_cancel_right mult_less_cancel_left
770     mult_less_cancel_right1 mult_less_cancel_right2
771     mult_less_cancel_left1 mult_less_cancel_left2
772     mult_cancel_right mult_cancel_left
773     mult_cancel_right1 mult_cancel_right2
774     mult_cancel_left1 mult_cancel_left2
777 subsection {* Fields *}
779 lemma right_inverse_eq: "b \<noteq> 0 ==> (a / b = 1) = (a = (b::'a::field))"
780 proof
781   assume neq: "b \<noteq> 0"
782   {
783     hence "a = (a / b) * b" by (simp add: divide_inverse mult_ac)
784     also assume "a / b = 1"
785     finally show "a = b" by simp
786   next
787     assume "a = b"
788     with neq show "a / b = 1" by (simp add: divide_inverse)
789   }
790 qed
792 lemma nonzero_inverse_eq_divide: "a \<noteq> 0 ==> inverse (a::'a::field) = 1/a"
795 lemma divide_self[simp]: "a \<noteq> 0 ==> a / (a::'a::field) = 1"
798 lemma divide_zero [simp]: "a / 0 = (0::'a::{field,division_by_zero})"
801 lemma divide_self_if [simp]:
802      "a / (a::'a::{field,division_by_zero}) = (if a=0 then 0 else 1)"
805 lemma divide_zero_left [simp]: "0/a = (0::'a::field)"
808 lemma inverse_eq_divide: "inverse (a::'a::field) = 1/a"
811 lemma add_divide_distrib: "(a+b)/(c::'a::field) = a/c + b/c"
812 by (simp add: divide_inverse ring_distribs)
814 (* what ordering?? this is a straight instance of mult_eq_0_iff
815 text{*Compared with @{text mult_eq_0_iff}, this version removes the requirement
816       of an ordering.*}
817 lemma field_mult_eq_0_iff [simp]:
818   "(a*b = (0::'a::division_ring)) = (a = 0 | b = 0)"
819 by simp
820 *)
821 (* subsumed by mult_cancel lemmas on ring_no_zero_divisors
822 text{*Cancellation of equalities with a common factor*}
823 lemma field_mult_cancel_right_lemma:
824       assumes cnz: "c \<noteq> (0::'a::division_ring)"
825          and eq:  "a*c = b*c"
826         shows "a=b"
827 proof -
828   have "(a * c) * inverse c = (b * c) * inverse c"
830   thus "a=b"
831     by (simp add: mult_assoc cnz)
832 qed
834 lemma field_mult_cancel_right [simp]:
835      "(a*c = b*c) = (c = (0::'a::division_ring) | a=b)"
836 by simp
838 lemma field_mult_cancel_left [simp]:
839      "(c*a = c*b) = (c = (0::'a::division_ring) | a=b)"
840 by simp
841 *)
842 lemma nonzero_imp_inverse_nonzero:
843   "a \<noteq> 0 ==> inverse a \<noteq> (0::'a::division_ring)"
844 proof
845   assume ianz: "inverse a = 0"
846   assume "a \<noteq> 0"
847   hence "1 = a * inverse a" by simp
848   also have "... = 0" by (simp add: ianz)
849   finally have "1 = (0::'a::division_ring)" .
850   thus False by (simp add: eq_commute)
851 qed
854 subsection{*Basic Properties of @{term inverse}*}
856 lemma inverse_zero_imp_zero: "inverse a = 0 ==> a = (0::'a::division_ring)"
857 apply (rule ccontr)
858 apply (blast dest: nonzero_imp_inverse_nonzero)
859 done
861 lemma inverse_nonzero_imp_nonzero:
862    "inverse a = 0 ==> a = (0::'a::division_ring)"
863 apply (rule ccontr)
864 apply (blast dest: nonzero_imp_inverse_nonzero)
865 done
867 lemma inverse_nonzero_iff_nonzero [simp]:
868    "(inverse a = 0) = (a = (0::'a::{division_ring,division_by_zero}))"
869 by (force dest: inverse_nonzero_imp_nonzero)
871 lemma nonzero_inverse_minus_eq:
872       assumes [simp]: "a\<noteq>0"
873       shows "inverse(-a) = -inverse(a::'a::division_ring)"
874 proof -
875   have "-a * inverse (- a) = -a * - inverse a"
876     by simp
877   thus ?thesis
878     by (simp only: mult_cancel_left, simp)
879 qed
881 lemma inverse_minus_eq [simp]:
882    "inverse(-a) = -inverse(a::'a::{division_ring,division_by_zero})"
883 proof cases
884   assume "a=0" thus ?thesis by (simp add: inverse_zero)
885 next
886   assume "a\<noteq>0"
887   thus ?thesis by (simp add: nonzero_inverse_minus_eq)
888 qed
890 lemma nonzero_inverse_eq_imp_eq:
891       assumes inveq: "inverse a = inverse b"
892 	  and anz:  "a \<noteq> 0"
893 	  and bnz:  "b \<noteq> 0"
894 	 shows "a = (b::'a::division_ring)"
895 proof -
896   have "a * inverse b = a * inverse a"
898   hence "(a * inverse b) * b = (a * inverse a) * b"
899     by simp
900   thus "a = b"
901     by (simp add: mult_assoc anz bnz)
902 qed
904 lemma inverse_eq_imp_eq:
905   "inverse a = inverse b ==> a = (b::'a::{division_ring,division_by_zero})"
906 apply (cases "a=0 | b=0")
907  apply (force dest!: inverse_zero_imp_zero
908               simp add: eq_commute [of "0::'a"])
909 apply (force dest!: nonzero_inverse_eq_imp_eq)
910 done
912 lemma inverse_eq_iff_eq [simp]:
913   "(inverse a = inverse b) = (a = (b::'a::{division_ring,division_by_zero}))"
914 by (force dest!: inverse_eq_imp_eq)
916 lemma nonzero_inverse_inverse_eq:
917       assumes [simp]: "a \<noteq> 0"
918       shows "inverse(inverse (a::'a::division_ring)) = a"
919   proof -
920   have "(inverse (inverse a) * inverse a) * a = a"
922   thus ?thesis
924   qed
926 lemma inverse_inverse_eq [simp]:
927      "inverse(inverse (a::'a::{division_ring,division_by_zero})) = a"
928   proof cases
929     assume "a=0" thus ?thesis by simp
930   next
931     assume "a\<noteq>0"
932     thus ?thesis by (simp add: nonzero_inverse_inverse_eq)
933   qed
935 lemma inverse_1 [simp]: "inverse 1 = (1::'a::division_ring)"
936   proof -
937   have "inverse 1 * 1 = (1::'a::division_ring)"
938     by (rule left_inverse [OF zero_neq_one [symmetric]])
939   thus ?thesis  by simp
940   qed
942 lemma inverse_unique:
943   assumes ab: "a*b = 1"
944   shows "inverse a = (b::'a::division_ring)"
945 proof -
946   have "a \<noteq> 0" using ab by auto
947   moreover have "inverse a * (a * b) = inverse a" by (simp add: ab)
948   ultimately show ?thesis by (simp add: mult_assoc [symmetric])
949 qed
951 lemma nonzero_inverse_mult_distrib:
952       assumes anz: "a \<noteq> 0"
953           and bnz: "b \<noteq> 0"
954       shows "inverse(a*b) = inverse(b) * inverse(a::'a::division_ring)"
955   proof -
956   have "inverse(a*b) * (a * b) * inverse(b) = inverse(b)"
957     by (simp add: anz bnz)
958   hence "inverse(a*b) * a = inverse(b)"
959     by (simp add: mult_assoc bnz)
960   hence "inverse(a*b) * a * inverse(a) = inverse(b) * inverse(a)"
961     by simp
962   thus ?thesis
963     by (simp add: mult_assoc anz)
964   qed
966 text{*This version builds in division by zero while also re-orienting
967       the right-hand side.*}
968 lemma inverse_mult_distrib [simp]:
969      "inverse(a*b) = inverse(a) * inverse(b::'a::{field,division_by_zero})"
970   proof cases
971     assume "a \<noteq> 0 & b \<noteq> 0"
972     thus ?thesis
973       by (simp add: nonzero_inverse_mult_distrib mult_commute)
974   next
975     assume "~ (a \<noteq> 0 & b \<noteq> 0)"
976     thus ?thesis
977       by force
978   qed
981   "[|(a::'a::division_ring) \<noteq> 0; b \<noteq> 0|]
982    ==> inverse a + inverse b = inverse a * (a+b) * inverse b"
985 lemma division_ring_inverse_diff:
986   "[|(a::'a::division_ring) \<noteq> 0; b \<noteq> 0|]
987    ==> inverse a - inverse b = inverse a * (b-a) * inverse b"
990 text{*There is no slick version using division by zero.*}
992   "[|a \<noteq> 0;  b \<noteq> 0|]
993    ==> inverse a + inverse b = (a+b) * inverse a * inverse (b::'a::field)"
996 lemma inverse_divide [simp]:
997   "inverse (a/b) = b / (a::'a::{field,division_by_zero})"
998 by (simp add: divide_inverse mult_commute)
1001 subsection {* Calculations with fractions *}
1003 text{* There is a whole bunch of simp-rules just for class @{text
1004 field} but none for class @{text field} and @{text nonzero_divides}
1005 because the latter are covered by a simproc. *}
1007 lemma nonzero_mult_divide_mult_cancel_left[simp,noatp]:
1008 assumes [simp]: "b\<noteq>0" and [simp]: "c\<noteq>0" shows "(c*a)/(c*b) = a/(b::'a::field)"
1009 proof -
1010   have "(c*a)/(c*b) = c * a * (inverse b * inverse c)"
1011     by (simp add: divide_inverse nonzero_inverse_mult_distrib)
1012   also have "... =  a * inverse b * (inverse c * c)"
1013     by (simp only: mult_ac)
1014   also have "... =  a * inverse b"
1015     by simp
1016     finally show ?thesis
1018 qed
1020 lemma mult_divide_mult_cancel_left:
1021   "c\<noteq>0 ==> (c*a) / (c*b) = a / (b::'a::{field,division_by_zero})"
1022 apply (cases "b = 0")
1024 done
1026 lemma nonzero_mult_divide_mult_cancel_right [noatp]:
1027   "[|b\<noteq>0; c\<noteq>0|] ==> (a*c) / (b*c) = a/(b::'a::field)"
1028 by (simp add: mult_commute [of _ c] nonzero_mult_divide_mult_cancel_left)
1030 lemma mult_divide_mult_cancel_right:
1031   "c\<noteq>0 ==> (a*c) / (b*c) = a / (b::'a::{field,division_by_zero})"
1032 apply (cases "b = 0")
1034 done
1036 lemma divide_1 [simp]: "a/1 = (a::'a::field)"
1039 lemma times_divide_eq_right: "a * (b/c) = (a*b) / (c::'a::field)"
1040 by (simp add: divide_inverse mult_assoc)
1042 lemma times_divide_eq_left: "(b/c) * a = (b*a) / (c::'a::field)"
1043 by (simp add: divide_inverse mult_ac)
1045 lemmas times_divide_eq = times_divide_eq_right times_divide_eq_left
1047 lemma divide_divide_eq_right [simp,noatp]:
1048   "a / (b/c) = (a*c) / (b::'a::{field,division_by_zero})"
1049 by (simp add: divide_inverse mult_ac)
1051 lemma divide_divide_eq_left [simp,noatp]:
1052   "(a / b) / (c::'a::{field,division_by_zero}) = a / (b*c)"
1053 by (simp add: divide_inverse mult_assoc)
1055 lemma add_frac_eq: "(y::'a::field) ~= 0 ==> z ~= 0 ==>
1056     x / y + w / z = (x * z + w * y) / (y * z)"
1057 apply (subgoal_tac "x / y = (x * z) / (y * z)")
1058 apply (erule ssubst)
1059 apply (subgoal_tac "w / z = (w * y) / (y * z)")
1060 apply (erule ssubst)
1061 apply (rule add_divide_distrib [THEN sym])
1062 apply (subst mult_commute)
1063 apply (erule nonzero_mult_divide_mult_cancel_left [THEN sym])
1064 apply assumption
1065 apply (erule nonzero_mult_divide_mult_cancel_right [THEN sym])
1066 apply assumption
1067 done
1070 subsubsection{*Special Cancellation Simprules for Division*}
1072 lemma mult_divide_mult_cancel_left_if[simp,noatp]:
1073 fixes c :: "'a :: {field,division_by_zero}"
1074 shows "(c*a) / (c*b) = (if c=0 then 0 else a/b)"
1077 lemma nonzero_mult_divide_cancel_right[simp,noatp]:
1078   "b \<noteq> 0 \<Longrightarrow> a * b / b = (a::'a::field)"
1079 using nonzero_mult_divide_mult_cancel_right[of 1 b a] by simp
1081 lemma nonzero_mult_divide_cancel_left[simp,noatp]:
1082   "a \<noteq> 0 \<Longrightarrow> a * b / a = (b::'a::field)"
1083 using nonzero_mult_divide_mult_cancel_left[of 1 a b] by simp
1086 lemma nonzero_divide_mult_cancel_right[simp,noatp]:
1087   "\<lbrakk> a\<noteq>0; b\<noteq>0 \<rbrakk> \<Longrightarrow> b / (a * b) = 1/(a::'a::field)"
1088 using nonzero_mult_divide_mult_cancel_right[of a b 1] by simp
1090 lemma nonzero_divide_mult_cancel_left[simp,noatp]:
1091   "\<lbrakk> a\<noteq>0; b\<noteq>0 \<rbrakk> \<Longrightarrow> a / (a * b) = 1/(b::'a::field)"
1092 using nonzero_mult_divide_mult_cancel_left[of b a 1] by simp
1095 lemma nonzero_mult_divide_mult_cancel_left2[simp,noatp]:
1096   "[|b\<noteq>0; c\<noteq>0|] ==> (c*a) / (b*c) = a/(b::'a::field)"
1097 using nonzero_mult_divide_mult_cancel_left[of b c a] by(simp add:mult_ac)
1099 lemma nonzero_mult_divide_mult_cancel_right2[simp,noatp]:
1100   "[|b\<noteq>0; c\<noteq>0|] ==> (a*c) / (c*b) = a/(b::'a::field)"
1101 using nonzero_mult_divide_mult_cancel_right[of b c a] by(simp add:mult_ac)
1104 subsection {* Division and Unary Minus *}
1106 lemma nonzero_minus_divide_left: "b \<noteq> 0 ==> - (a/b) = (-a) / (b::'a::field)"
1107 by (simp add: divide_inverse minus_mult_left)
1109 lemma nonzero_minus_divide_right: "b \<noteq> 0 ==> - (a/b) = a / -(b::'a::field)"
1110 by (simp add: divide_inverse nonzero_inverse_minus_eq minus_mult_right)
1112 lemma nonzero_minus_divide_divide: "b \<noteq> 0 ==> (-a)/(-b) = a / (b::'a::field)"
1113 by (simp add: divide_inverse nonzero_inverse_minus_eq)
1115 lemma minus_divide_left: "- (a/b) = (-a) / (b::'a::field)"
1116 by (simp add: divide_inverse minus_mult_left [symmetric])
1118 lemma minus_divide_right: "- (a/b) = a / -(b::'a::{field,division_by_zero})"
1119 by (simp add: divide_inverse minus_mult_right [symmetric])
1122 text{*The effect is to extract signs from divisions*}
1123 lemmas divide_minus_left = minus_divide_left [symmetric]
1124 lemmas divide_minus_right = minus_divide_right [symmetric]
1125 declare divide_minus_left [simp]   divide_minus_right [simp]
1127 text{*Also, extract signs from products*}
1128 lemmas mult_minus_left = minus_mult_left [symmetric]
1129 lemmas mult_minus_right = minus_mult_right [symmetric]
1130 declare mult_minus_left [simp]   mult_minus_right [simp]
1132 lemma minus_divide_divide [simp]:
1133   "(-a)/(-b) = a / (b::'a::{field,division_by_zero})"
1134 apply (cases "b=0", simp)
1136 done
1138 lemma diff_divide_distrib: "(a-b)/(c::'a::field) = a/c - b/c"
1142   "(z::'a::field) \<noteq> 0 \<Longrightarrow> x + y/z = (z*x + y)/z"
1146   "(z::'a::field) \<noteq> 0 \<Longrightarrow> x/z + y = (x + z*y)/z"
1149 lemma diff_divide_eq_iff:
1150   "(z::'a::field) \<noteq> 0 \<Longrightarrow> x - y/z = (z*x - y)/z"
1153 lemma divide_diff_eq_iff:
1154   "(z::'a::field) \<noteq> 0 \<Longrightarrow> x/z - y = (x - z*y)/z"
1157 lemma nonzero_eq_divide_eq: "c\<noteq>0 ==> ((a::'a::field) = b/c) = (a*c = b)"
1158 proof -
1159   assume [simp]: "c\<noteq>0"
1160   have "(a = b/c) = (a*c = (b/c)*c)" by simp
1161   also have "... = (a*c = b)" by (simp add: divide_inverse mult_assoc)
1162   finally show ?thesis .
1163 qed
1165 lemma nonzero_divide_eq_eq: "c\<noteq>0 ==> (b/c = (a::'a::field)) = (b = a*c)"
1166 proof -
1167   assume [simp]: "c\<noteq>0"
1168   have "(b/c = a) = ((b/c)*c = a*c)"  by simp
1169   also have "... = (b = a*c)"  by (simp add: divide_inverse mult_assoc)
1170   finally show ?thesis .
1171 qed
1173 lemma eq_divide_eq:
1174   "((a::'a::{field,division_by_zero}) = b/c) = (if c\<noteq>0 then a*c = b else a=0)"
1177 lemma divide_eq_eq:
1178   "(b/c = (a::'a::{field,division_by_zero})) = (if c\<noteq>0 then b = a*c else a=0)"
1179 by (force simp add: nonzero_divide_eq_eq)
1181 lemma divide_eq_imp: "(c::'a::{division_by_zero,field}) ~= 0 ==>
1182     b = a * c ==> b / c = a"
1183   by (subst divide_eq_eq, simp)
1185 lemma eq_divide_imp: "(c::'a::{division_by_zero,field}) ~= 0 ==>
1186     a * c = b ==> a = b / c"
1187   by (subst eq_divide_eq, simp)
1190 lemmas field_eq_simps = ring_simps
1191   (* pull / out*)
1193   diff_divide_eq_iff divide_diff_eq_iff
1194   (* multiply eqn *)
1195   nonzero_eq_divide_eq nonzero_divide_eq_eq
1197   times_divide_eq_left times_divide_eq_right
1198 *)
1200 text{*An example:*}
1201 lemma fixes a b c d e f :: "'a::field"
1202 shows "\<lbrakk>a\<noteq>b; c\<noteq>d; e\<noteq>f \<rbrakk> \<Longrightarrow> ((a-b)*(c-d)*(e-f))/((c-d)*(e-f)*(a-b)) = 1"
1203 apply(subgoal_tac "(c-d)*(e-f)*(a-b) \<noteq> 0")
1205 apply(simp)
1206 done
1209 lemma diff_frac_eq: "(y::'a::field) ~= 0 ==> z ~= 0 ==>
1210     x / y - w / z = (x * z - w * y) / (y * z)"
1213 lemma frac_eq_eq: "(y::'a::field) ~= 0 ==> z ~= 0 ==>
1214     (x / y = w / z) = (x * z = w * y)"
1218 subsection {* Ordered Fields *}
1220 lemma positive_imp_inverse_positive:
1221 assumes a_gt_0: "0 < a"  shows "0 < inverse (a::'a::ordered_field)"
1222 proof -
1223   have "0 < a * inverse a"
1224     by (simp add: a_gt_0 [THEN order_less_imp_not_eq2] zero_less_one)
1225   thus "0 < inverse a"
1226     by (simp add: a_gt_0 [THEN order_less_not_sym] zero_less_mult_iff)
1227 qed
1229 lemma negative_imp_inverse_negative:
1230   "a < 0 ==> inverse a < (0::'a::ordered_field)"
1231 by (insert positive_imp_inverse_positive [of "-a"],
1234 lemma inverse_le_imp_le:
1235 assumes invle: "inverse a \<le> inverse b" and apos:  "0 < a"
1236 shows "b \<le> (a::'a::ordered_field)"
1237 proof (rule classical)
1238   assume "~ b \<le> a"
1239   hence "a < b"  by (simp add: linorder_not_le)
1240   hence bpos: "0 < b"  by (blast intro: apos order_less_trans)
1241   hence "a * inverse a \<le> a * inverse b"
1242     by (simp add: apos invle order_less_imp_le mult_left_mono)
1243   hence "(a * inverse a) * b \<le> (a * inverse b) * b"
1244     by (simp add: bpos order_less_imp_le mult_right_mono)
1245   thus "b \<le> a"  by (simp add: mult_assoc apos bpos order_less_imp_not_eq2)
1246 qed
1248 lemma inverse_positive_imp_positive:
1249 assumes inv_gt_0: "0 < inverse a" and nz: "a \<noteq> 0"
1250 shows "0 < (a::'a::ordered_field)"
1251 proof -
1252   have "0 < inverse (inverse a)"
1253     using inv_gt_0 by (rule positive_imp_inverse_positive)
1254   thus "0 < a"
1255     using nz by (simp add: nonzero_inverse_inverse_eq)
1256 qed
1258 lemma inverse_positive_iff_positive [simp]:
1259   "(0 < inverse a) = (0 < (a::'a::{ordered_field,division_by_zero}))"
1260 apply (cases "a = 0", simp)
1261 apply (blast intro: inverse_positive_imp_positive positive_imp_inverse_positive)
1262 done
1264 lemma inverse_negative_imp_negative:
1265 assumes inv_less_0: "inverse a < 0" and nz:  "a \<noteq> 0"
1266 shows "a < (0::'a::ordered_field)"
1267 proof -
1268   have "inverse (inverse a) < 0"
1269     using inv_less_0 by (rule negative_imp_inverse_negative)
1270   thus "a < 0" using nz by (simp add: nonzero_inverse_inverse_eq)
1271 qed
1273 lemma inverse_negative_iff_negative [simp]:
1274   "(inverse a < 0) = (a < (0::'a::{ordered_field,division_by_zero}))"
1275 apply (cases "a = 0", simp)
1276 apply (blast intro: inverse_negative_imp_negative negative_imp_inverse_negative)
1277 done
1279 lemma inverse_nonnegative_iff_nonnegative [simp]:
1280   "(0 \<le> inverse a) = (0 \<le> (a::'a::{ordered_field,division_by_zero}))"
1281 by (simp add: linorder_not_less [symmetric])
1283 lemma inverse_nonpositive_iff_nonpositive [simp]:
1284   "(inverse a \<le> 0) = (a \<le> (0::'a::{ordered_field,division_by_zero}))"
1285 by (simp add: linorder_not_less [symmetric])
1287 lemma ordered_field_no_lb: "\<forall> x. \<exists>y. y < (x::'a::ordered_field)"
1288 proof
1289   fix x::'a
1290   have m1: "- (1::'a) < 0" by simp
1291   from add_strict_right_mono[OF m1, where c=x]
1292   have "(- 1) + x < x" by simp
1293   thus "\<exists>y. y < x" by blast
1294 qed
1296 lemma ordered_field_no_ub: "\<forall> x. \<exists>y. y > (x::'a::ordered_field)"
1297 proof
1298   fix x::'a
1299   have m1: " (1::'a) > 0" by simp
1300   from add_strict_right_mono[OF m1, where c=x]
1301   have "1 + x > x" by simp
1302   thus "\<exists>y. y > x" by blast
1303 qed
1305 subsection{*Anti-Monotonicity of @{term inverse}*}
1307 lemma less_imp_inverse_less:
1308 assumes less: "a < b" and apos:  "0 < a"
1309 shows "inverse b < inverse (a::'a::ordered_field)"
1310 proof (rule ccontr)
1311   assume "~ inverse b < inverse a"
1312   hence "inverse a \<le> inverse b"
1314   hence "~ (a < b)"
1315     by (simp add: linorder_not_less inverse_le_imp_le [OF _ apos])
1316   thus False
1317     by (rule notE [OF _ less])
1318 qed
1320 lemma inverse_less_imp_less:
1321   "[|inverse a < inverse b; 0 < a|] ==> b < (a::'a::ordered_field)"
1322 apply (simp add: order_less_le [of "inverse a"] order_less_le [of "b"])
1323 apply (force dest!: inverse_le_imp_le nonzero_inverse_eq_imp_eq)
1324 done
1326 text{*Both premises are essential. Consider -1 and 1.*}
1327 lemma inverse_less_iff_less [simp,noatp]:
1328   "[|0 < a; 0 < b|] ==> (inverse a < inverse b) = (b < (a::'a::ordered_field))"
1329 by (blast intro: less_imp_inverse_less dest: inverse_less_imp_less)
1331 lemma le_imp_inverse_le:
1332   "[|a \<le> b; 0 < a|] ==> inverse b \<le> inverse (a::'a::ordered_field)"
1333 by (force simp add: order_le_less less_imp_inverse_less)
1335 lemma inverse_le_iff_le [simp,noatp]:
1336  "[|0 < a; 0 < b|] ==> (inverse a \<le> inverse b) = (b \<le> (a::'a::ordered_field))"
1337 by (blast intro: le_imp_inverse_le dest: inverse_le_imp_le)
1340 text{*These results refer to both operands being negative.  The opposite-sign
1341 case is trivial, since inverse preserves signs.*}
1342 lemma inverse_le_imp_le_neg:
1343   "[|inverse a \<le> inverse b; b < 0|] ==> b \<le> (a::'a::ordered_field)"
1344 apply (rule classical)
1345 apply (subgoal_tac "a < 0")
1346  prefer 2 apply (force simp add: linorder_not_le intro: order_less_trans)
1347 apply (insert inverse_le_imp_le [of "-b" "-a"])
1348 apply (simp add: order_less_imp_not_eq nonzero_inverse_minus_eq)
1349 done
1351 lemma less_imp_inverse_less_neg:
1352    "[|a < b; b < 0|] ==> inverse b < inverse (a::'a::ordered_field)"
1353 apply (subgoal_tac "a < 0")
1354  prefer 2 apply (blast intro: order_less_trans)
1355 apply (insert less_imp_inverse_less [of "-b" "-a"])
1356 apply (simp add: order_less_imp_not_eq nonzero_inverse_minus_eq)
1357 done
1359 lemma inverse_less_imp_less_neg:
1360    "[|inverse a < inverse b; b < 0|] ==> b < (a::'a::ordered_field)"
1361 apply (rule classical)
1362 apply (subgoal_tac "a < 0")
1363  prefer 2
1364  apply (force simp add: linorder_not_less intro: order_le_less_trans)
1365 apply (insert inverse_less_imp_less [of "-b" "-a"])
1366 apply (simp add: order_less_imp_not_eq nonzero_inverse_minus_eq)
1367 done
1369 lemma inverse_less_iff_less_neg [simp,noatp]:
1370   "[|a < 0; b < 0|] ==> (inverse a < inverse b) = (b < (a::'a::ordered_field))"
1371 apply (insert inverse_less_iff_less [of "-b" "-a"])
1372 apply (simp del: inverse_less_iff_less
1374 done
1376 lemma le_imp_inverse_le_neg:
1377   "[|a \<le> b; b < 0|] ==> inverse b \<le> inverse (a::'a::ordered_field)"
1378 by (force simp add: order_le_less less_imp_inverse_less_neg)
1380 lemma inverse_le_iff_le_neg [simp,noatp]:
1381  "[|a < 0; b < 0|] ==> (inverse a \<le> inverse b) = (b \<le> (a::'a::ordered_field))"
1382 by (blast intro: le_imp_inverse_le_neg dest: inverse_le_imp_le_neg)
1385 subsection{*Inverses and the Number One*}
1387 lemma one_less_inverse_iff:
1388   "(1 < inverse x) = (0 < x & x < (1::'a::{ordered_field,division_by_zero}))"
1389 proof cases
1390   assume "0 < x"
1391     with inverse_less_iff_less [OF zero_less_one, of x]
1392     show ?thesis by simp
1393 next
1394   assume notless: "~ (0 < x)"
1395   have "~ (1 < inverse x)"
1396   proof
1397     assume "1 < inverse x"
1398     also with notless have "... \<le> 0" by (simp add: linorder_not_less)
1399     also have "... < 1" by (rule zero_less_one)
1400     finally show False by auto
1401   qed
1402   with notless show ?thesis by simp
1403 qed
1405 lemma inverse_eq_1_iff [simp]:
1406   "(inverse x = 1) = (x = (1::'a::{field,division_by_zero}))"
1407 by (insert inverse_eq_iff_eq [of x 1], simp)
1409 lemma one_le_inverse_iff:
1410   "(1 \<le> inverse x) = (0 < x & x \<le> (1::'a::{ordered_field,division_by_zero}))"
1411 by (force simp add: order_le_less one_less_inverse_iff zero_less_one
1412                     eq_commute [of 1])
1414 lemma inverse_less_1_iff:
1415   "(inverse x < 1) = (x \<le> 0 | 1 < (x::'a::{ordered_field,division_by_zero}))"
1416 by (simp add: linorder_not_le [symmetric] one_le_inverse_iff)
1418 lemma inverse_le_1_iff:
1419   "(inverse x \<le> 1) = (x \<le> 0 | 1 \<le> (x::'a::{ordered_field,division_by_zero}))"
1420 by (simp add: linorder_not_less [symmetric] one_less_inverse_iff)
1423 subsection{*Simplification of Inequalities Involving Literal Divisors*}
1425 lemma pos_le_divide_eq: "0 < (c::'a::ordered_field) ==> (a \<le> b/c) = (a*c \<le> b)"
1426 proof -
1427   assume less: "0<c"
1428   hence "(a \<le> b/c) = (a*c \<le> (b/c)*c)"
1429     by (simp add: mult_le_cancel_right order_less_not_sym [OF less])
1430   also have "... = (a*c \<le> b)"
1431     by (simp add: order_less_imp_not_eq2 [OF less] divide_inverse mult_assoc)
1432   finally show ?thesis .
1433 qed
1435 lemma neg_le_divide_eq: "c < (0::'a::ordered_field) ==> (a \<le> b/c) = (b \<le> a*c)"
1436 proof -
1437   assume less: "c<0"
1438   hence "(a \<le> b/c) = ((b/c)*c \<le> a*c)"
1439     by (simp add: mult_le_cancel_right order_less_not_sym [OF less])
1440   also have "... = (b \<le> a*c)"
1441     by (simp add: order_less_imp_not_eq [OF less] divide_inverse mult_assoc)
1442   finally show ?thesis .
1443 qed
1445 lemma le_divide_eq:
1446   "(a \<le> b/c) =
1447    (if 0 < c then a*c \<le> b
1448              else if c < 0 then b \<le> a*c
1449              else  a \<le> (0::'a::{ordered_field,division_by_zero}))"
1450 apply (cases "c=0", simp)
1451 apply (force simp add: pos_le_divide_eq neg_le_divide_eq linorder_neq_iff)
1452 done
1454 lemma pos_divide_le_eq: "0 < (c::'a::ordered_field) ==> (b/c \<le> a) = (b \<le> a*c)"
1455 proof -
1456   assume less: "0<c"
1457   hence "(b/c \<le> a) = ((b/c)*c \<le> a*c)"
1458     by (simp add: mult_le_cancel_right order_less_not_sym [OF less])
1459   also have "... = (b \<le> a*c)"
1460     by (simp add: order_less_imp_not_eq2 [OF less] divide_inverse mult_assoc)
1461   finally show ?thesis .
1462 qed
1464 lemma neg_divide_le_eq: "c < (0::'a::ordered_field) ==> (b/c \<le> a) = (a*c \<le> b)"
1465 proof -
1466   assume less: "c<0"
1467   hence "(b/c \<le> a) = (a*c \<le> (b/c)*c)"
1468     by (simp add: mult_le_cancel_right order_less_not_sym [OF less])
1469   also have "... = (a*c \<le> b)"
1470     by (simp add: order_less_imp_not_eq [OF less] divide_inverse mult_assoc)
1471   finally show ?thesis .
1472 qed
1474 lemma divide_le_eq:
1475   "(b/c \<le> a) =
1476    (if 0 < c then b \<le> a*c
1477              else if c < 0 then a*c \<le> b
1478              else 0 \<le> (a::'a::{ordered_field,division_by_zero}))"
1479 apply (cases "c=0", simp)
1480 apply (force simp add: pos_divide_le_eq neg_divide_le_eq linorder_neq_iff)
1481 done
1483 lemma pos_less_divide_eq:
1484      "0 < (c::'a::ordered_field) ==> (a < b/c) = (a*c < b)"
1485 proof -
1486   assume less: "0<c"
1487   hence "(a < b/c) = (a*c < (b/c)*c)"
1488     by (simp add: mult_less_cancel_right_disj order_less_not_sym [OF less])
1489   also have "... = (a*c < b)"
1490     by (simp add: order_less_imp_not_eq2 [OF less] divide_inverse mult_assoc)
1491   finally show ?thesis .
1492 qed
1494 lemma neg_less_divide_eq:
1495  "c < (0::'a::ordered_field) ==> (a < b/c) = (b < a*c)"
1496 proof -
1497   assume less: "c<0"
1498   hence "(a < b/c) = ((b/c)*c < a*c)"
1499     by (simp add: mult_less_cancel_right_disj order_less_not_sym [OF less])
1500   also have "... = (b < a*c)"
1501     by (simp add: order_less_imp_not_eq [OF less] divide_inverse mult_assoc)
1502   finally show ?thesis .
1503 qed
1505 lemma less_divide_eq:
1506   "(a < b/c) =
1507    (if 0 < c then a*c < b
1508              else if c < 0 then b < a*c
1509              else  a < (0::'a::{ordered_field,division_by_zero}))"
1510 apply (cases "c=0", simp)
1511 apply (force simp add: pos_less_divide_eq neg_less_divide_eq linorder_neq_iff)
1512 done
1514 lemma pos_divide_less_eq:
1515      "0 < (c::'a::ordered_field) ==> (b/c < a) = (b < a*c)"
1516 proof -
1517   assume less: "0<c"
1518   hence "(b/c < a) = ((b/c)*c < a*c)"
1519     by (simp add: mult_less_cancel_right_disj order_less_not_sym [OF less])
1520   also have "... = (b < a*c)"
1521     by (simp add: order_less_imp_not_eq2 [OF less] divide_inverse mult_assoc)
1522   finally show ?thesis .
1523 qed
1525 lemma neg_divide_less_eq:
1526  "c < (0::'a::ordered_field) ==> (b/c < a) = (a*c < b)"
1527 proof -
1528   assume less: "c<0"
1529   hence "(b/c < a) = (a*c < (b/c)*c)"
1530     by (simp add: mult_less_cancel_right_disj order_less_not_sym [OF less])
1531   also have "... = (a*c < b)"
1532     by (simp add: order_less_imp_not_eq [OF less] divide_inverse mult_assoc)
1533   finally show ?thesis .
1534 qed
1536 lemma divide_less_eq:
1537   "(b/c < a) =
1538    (if 0 < c then b < a*c
1539              else if c < 0 then a*c < b
1540              else 0 < (a::'a::{ordered_field,division_by_zero}))"
1541 apply (cases "c=0", simp)
1542 apply (force simp add: pos_divide_less_eq neg_divide_less_eq linorder_neq_iff)
1543 done
1546 subsection{*Field simplification*}
1548 text{* Lemmas @{text field_simps} multiply with denominators in
1549 in(equations) if they can be proved to be non-zero (for equations) or
1550 positive/negative (for inequations). *}
1552 lemmas field_simps = field_eq_simps
1553   (* multiply ineqn *)
1554   pos_divide_less_eq neg_divide_less_eq
1555   pos_less_divide_eq neg_less_divide_eq
1556   pos_divide_le_eq neg_divide_le_eq
1557   pos_le_divide_eq neg_le_divide_eq
1559 text{* Lemmas @{text sign_simps} is a first attempt to automate proofs
1560 of positivity/negativity needed for @{text field_simps}. Have not added @{text
1561 sign_simps} to @{text field_simps} because the former can lead to case
1562 explosions. *}
1564 lemmas sign_simps = group_simps
1565   zero_less_mult_iff  mult_less_0_iff
1567 (* Only works once linear arithmetic is installed:
1568 text{*An example:*}
1569 lemma fixes a b c d e f :: "'a::ordered_field"
1570 shows "\<lbrakk>a>b; c<d; e<f; 0 < u \<rbrakk> \<Longrightarrow>
1571  ((a-b)*(c-d)*(e-f))/((c-d)*(e-f)*(a-b)) <
1572  ((e-f)*(a-b)*(c-d))/((e-f)*(a-b)*(c-d)) + u"
1573 apply(subgoal_tac "(c-d)*(e-f)*(a-b) > 0")
1575 apply(subgoal_tac "(c-d)*(e-f)*(a-b)*u > 0")
1578 done
1579 *)
1582 subsection{*Division and Signs*}
1584 lemma zero_less_divide_iff:
1585      "((0::'a::{ordered_field,division_by_zero}) < a/b) = (0 < a & 0 < b | a < 0 & b < 0)"
1586 by (simp add: divide_inverse zero_less_mult_iff)
1588 lemma divide_less_0_iff:
1589      "(a/b < (0::'a::{ordered_field,division_by_zero})) =
1590       (0 < a & b < 0 | a < 0 & 0 < b)"
1591 by (simp add: divide_inverse mult_less_0_iff)
1593 lemma zero_le_divide_iff:
1594      "((0::'a::{ordered_field,division_by_zero}) \<le> a/b) =
1595       (0 \<le> a & 0 \<le> b | a \<le> 0 & b \<le> 0)"
1596 by (simp add: divide_inverse zero_le_mult_iff)
1598 lemma divide_le_0_iff:
1599      "(a/b \<le> (0::'a::{ordered_field,division_by_zero})) =
1600       (0 \<le> a & b \<le> 0 | a \<le> 0 & 0 \<le> b)"
1601 by (simp add: divide_inverse mult_le_0_iff)
1603 lemma divide_eq_0_iff [simp,noatp]:
1604      "(a/b = 0) = (a=0 | b=(0::'a::{field,division_by_zero}))"
1607 lemma divide_pos_pos:
1608   "0 < (x::'a::ordered_field) ==> 0 < y ==> 0 < x / y"
1612 lemma divide_nonneg_pos:
1613   "0 <= (x::'a::ordered_field) ==> 0 < y ==> 0 <= x / y"
1616 lemma divide_neg_pos:
1617   "(x::'a::ordered_field) < 0 ==> 0 < y ==> x / y < 0"
1620 lemma divide_nonpos_pos:
1621   "(x::'a::ordered_field) <= 0 ==> 0 < y ==> x / y <= 0"
1624 lemma divide_pos_neg:
1625   "0 < (x::'a::ordered_field) ==> y < 0 ==> x / y < 0"
1628 lemma divide_nonneg_neg:
1629   "0 <= (x::'a::ordered_field) ==> y < 0 ==> x / y <= 0"
1632 lemma divide_neg_neg:
1633   "(x::'a::ordered_field) < 0 ==> y < 0 ==> 0 < x / y"
1636 lemma divide_nonpos_neg:
1637   "(x::'a::ordered_field) <= 0 ==> y < 0 ==> 0 <= x / y"
1641 subsection{*Cancellation Laws for Division*}
1643 lemma divide_cancel_right [simp,noatp]:
1644      "(a/c = b/c) = (c = 0 | a = (b::'a::{field,division_by_zero}))"
1645 apply (cases "c=0", simp)
1647 done
1649 lemma divide_cancel_left [simp,noatp]:
1650      "(c/a = c/b) = (c = 0 | a = (b::'a::{field,division_by_zero}))"
1651 apply (cases "c=0", simp)
1653 done
1656 subsection {* Division and the Number One *}
1658 text{*Simplify expressions equated with 1*}
1659 lemma divide_eq_1_iff [simp,noatp]:
1660      "(a/b = 1) = (b \<noteq> 0 & a = (b::'a::{field,division_by_zero}))"
1661 apply (cases "b=0", simp)
1663 done
1665 lemma one_eq_divide_iff [simp,noatp]:
1666      "(1 = a/b) = (b \<noteq> 0 & a = (b::'a::{field,division_by_zero}))"
1667 by (simp add: eq_commute [of 1])
1669 lemma zero_eq_1_divide_iff [simp,noatp]:
1670      "((0::'a::{ordered_field,division_by_zero}) = 1/a) = (a = 0)"
1671 apply (cases "a=0", simp)
1672 apply (auto simp add: nonzero_eq_divide_eq)
1673 done
1675 lemma one_divide_eq_0_iff [simp,noatp]:
1676      "(1/a = (0::'a::{ordered_field,division_by_zero})) = (a = 0)"
1677 apply (cases "a=0", simp)
1678 apply (insert zero_neq_one [THEN not_sym])
1679 apply (auto simp add: nonzero_divide_eq_eq)
1680 done
1682 text{*Simplify expressions such as @{text "0 < 1/x"} to @{text "0 < x"}*}
1683 lemmas zero_less_divide_1_iff = zero_less_divide_iff [of 1, simplified]
1684 lemmas divide_less_0_1_iff = divide_less_0_iff [of 1, simplified]
1685 lemmas zero_le_divide_1_iff = zero_le_divide_iff [of 1, simplified]
1686 lemmas divide_le_0_1_iff = divide_le_0_iff [of 1, simplified]
1688 declare zero_less_divide_1_iff [simp]
1689 declare divide_less_0_1_iff [simp,noatp]
1690 declare zero_le_divide_1_iff [simp]
1691 declare divide_le_0_1_iff [simp,noatp]
1694 subsection {* Ordering Rules for Division *}
1696 lemma divide_strict_right_mono:
1697      "[|a < b; 0 < c|] ==> a / c < b / (c::'a::ordered_field)"
1698 by (simp add: order_less_imp_not_eq2 divide_inverse mult_strict_right_mono
1699               positive_imp_inverse_positive)
1701 lemma divide_right_mono:
1702      "[|a \<le> b; 0 \<le> c|] ==> a/c \<le> b/(c::'a::{ordered_field,division_by_zero})"
1703 by (force simp add: divide_strict_right_mono order_le_less)
1705 lemma divide_right_mono_neg: "(a::'a::{division_by_zero,ordered_field}) <= b
1706     ==> c <= 0 ==> b / c <= a / c"
1707 apply (drule divide_right_mono [of _ _ "- c"])
1708 apply auto
1709 done
1711 lemma divide_strict_right_mono_neg:
1712      "[|b < a; c < 0|] ==> a / c < b / (c::'a::ordered_field)"
1713 apply (drule divide_strict_right_mono [of _ _ "-c"], simp)
1714 apply (simp add: order_less_imp_not_eq nonzero_minus_divide_right [symmetric])
1715 done
1717 text{*The last premise ensures that @{term a} and @{term b}
1718       have the same sign*}
1719 lemma divide_strict_left_mono:
1720   "[|b < a; 0 < c; 0 < a*b|] ==> c / a < c / (b::'a::ordered_field)"
1721 by(auto simp: field_simps times_divide_eq zero_less_mult_iff mult_strict_right_mono)
1723 lemma divide_left_mono:
1724   "[|b \<le> a; 0 \<le> c; 0 < a*b|] ==> c / a \<le> c / (b::'a::ordered_field)"
1725 by(auto simp: field_simps times_divide_eq zero_less_mult_iff mult_right_mono)
1727 lemma divide_left_mono_neg: "(a::'a::{division_by_zero,ordered_field}) <= b
1728     ==> c <= 0 ==> 0 < a * b ==> c / a <= c / b"
1729   apply (drule divide_left_mono [of _ _ "- c"])
1730   apply (auto simp add: mult_commute)
1731 done
1733 lemma divide_strict_left_mono_neg:
1734   "[|a < b; c < 0; 0 < a*b|] ==> c / a < c / (b::'a::ordered_field)"
1735 by(auto simp: field_simps times_divide_eq zero_less_mult_iff mult_strict_right_mono_neg)
1738 text{*Simplify quotients that are compared with the value 1.*}
1740 lemma le_divide_eq_1 [noatp]:
1741   fixes a :: "'a :: {ordered_field,division_by_zero}"
1742   shows "(1 \<le> b / a) = ((0 < a & a \<le> b) | (a < 0 & b \<le> a))"
1743 by (auto simp add: le_divide_eq)
1745 lemma divide_le_eq_1 [noatp]:
1746   fixes a :: "'a :: {ordered_field,division_by_zero}"
1747   shows "(b / a \<le> 1) = ((0 < a & b \<le> a) | (a < 0 & a \<le> b) | a=0)"
1748 by (auto simp add: divide_le_eq)
1750 lemma less_divide_eq_1 [noatp]:
1751   fixes a :: "'a :: {ordered_field,division_by_zero}"
1752   shows "(1 < b / a) = ((0 < a & a < b) | (a < 0 & b < a))"
1753 by (auto simp add: less_divide_eq)
1755 lemma divide_less_eq_1 [noatp]:
1756   fixes a :: "'a :: {ordered_field,division_by_zero}"
1757   shows "(b / a < 1) = ((0 < a & b < a) | (a < 0 & a < b) | a=0)"
1758 by (auto simp add: divide_less_eq)
1761 subsection{*Conditional Simplification Rules: No Case Splits*}
1763 lemma le_divide_eq_1_pos [simp,noatp]:
1764   fixes a :: "'a :: {ordered_field,division_by_zero}"
1765   shows "0 < a \<Longrightarrow> (1 \<le> b/a) = (a \<le> b)"
1766 by (auto simp add: le_divide_eq)
1768 lemma le_divide_eq_1_neg [simp,noatp]:
1769   fixes a :: "'a :: {ordered_field,division_by_zero}"
1770   shows "a < 0 \<Longrightarrow> (1 \<le> b/a) = (b \<le> a)"
1771 by (auto simp add: le_divide_eq)
1773 lemma divide_le_eq_1_pos [simp,noatp]:
1774   fixes a :: "'a :: {ordered_field,division_by_zero}"
1775   shows "0 < a \<Longrightarrow> (b/a \<le> 1) = (b \<le> a)"
1776 by (auto simp add: divide_le_eq)
1778 lemma divide_le_eq_1_neg [simp,noatp]:
1779   fixes a :: "'a :: {ordered_field,division_by_zero}"
1780   shows "a < 0 \<Longrightarrow> (b/a \<le> 1) = (a \<le> b)"
1781 by (auto simp add: divide_le_eq)
1783 lemma less_divide_eq_1_pos [simp,noatp]:
1784   fixes a :: "'a :: {ordered_field,division_by_zero}"
1785   shows "0 < a \<Longrightarrow> (1 < b/a) = (a < b)"
1786 by (auto simp add: less_divide_eq)
1788 lemma less_divide_eq_1_neg [simp,noatp]:
1789   fixes a :: "'a :: {ordered_field,division_by_zero}"
1790   shows "a < 0 \<Longrightarrow> (1 < b/a) = (b < a)"
1791 by (auto simp add: less_divide_eq)
1793 lemma divide_less_eq_1_pos [simp,noatp]:
1794   fixes a :: "'a :: {ordered_field,division_by_zero}"
1795   shows "0 < a \<Longrightarrow> (b/a < 1) = (b < a)"
1796 by (auto simp add: divide_less_eq)
1798 lemma divide_less_eq_1_neg [simp,noatp]:
1799   fixes a :: "'a :: {ordered_field,division_by_zero}"
1800   shows "a < 0 \<Longrightarrow> b/a < 1 <-> a < b"
1801 by (auto simp add: divide_less_eq)
1803 lemma eq_divide_eq_1 [simp,noatp]:
1804   fixes a :: "'a :: {ordered_field,division_by_zero}"
1805   shows "(1 = b/a) = ((a \<noteq> 0 & a = b))"
1806 by (auto simp add: eq_divide_eq)
1808 lemma divide_eq_eq_1 [simp,noatp]:
1809   fixes a :: "'a :: {ordered_field,division_by_zero}"
1810   shows "(b/a = 1) = ((a \<noteq> 0 & a = b))"
1811 by (auto simp add: divide_eq_eq)
1814 subsection {* Reasoning about inequalities with division *}
1816 lemma mult_right_le_one_le: "0 <= (x::'a::ordered_idom) ==> 0 <= y ==> y <= 1
1817     ==> x * y <= x"
1818   by (auto simp add: mult_compare_simps);
1820 lemma mult_left_le_one_le: "0 <= (x::'a::ordered_idom) ==> 0 <= y ==> y <= 1
1821     ==> y * x <= x"
1822   by (auto simp add: mult_compare_simps);
1824 lemma mult_imp_div_pos_le: "0 < (y::'a::ordered_field) ==> x <= z * y ==>
1825     x / y <= z";
1826   by (subst pos_divide_le_eq, assumption+);
1828 lemma mult_imp_le_div_pos: "0 < (y::'a::ordered_field) ==> z * y <= x ==>
1829     z <= x / y"
1832 lemma mult_imp_div_pos_less: "0 < (y::'a::ordered_field) ==> x < z * y ==>
1833     x / y < z"
1836 lemma mult_imp_less_div_pos: "0 < (y::'a::ordered_field) ==> z * y < x ==>
1837     z < x / y"
1840 lemma frac_le: "(0::'a::ordered_field) <= x ==>
1841     x <= y ==> 0 < w ==> w <= z  ==> x / z <= y / w"
1842   apply (rule mult_imp_div_pos_le)
1843   apply simp;
1844   apply (subst times_divide_eq_left);
1845   apply (rule mult_imp_le_div_pos, assumption)
1846   apply (rule mult_mono)
1847   apply simp_all
1848 done
1850 lemma frac_less: "(0::'a::ordered_field) <= x ==>
1851     x < y ==> 0 < w ==> w <= z  ==> x / z < y / w"
1852   apply (rule mult_imp_div_pos_less)
1853   apply simp;
1854   apply (subst times_divide_eq_left);
1855   apply (rule mult_imp_less_div_pos, assumption)
1856   apply (erule mult_less_le_imp_less)
1857   apply simp_all
1858 done
1860 lemma frac_less2: "(0::'a::ordered_field) < x ==>
1861     x <= y ==> 0 < w ==> w < z  ==> x / z < y / w"
1862   apply (rule mult_imp_div_pos_less)
1863   apply simp_all
1864   apply (subst times_divide_eq_left);
1865   apply (rule mult_imp_less_div_pos, assumption)
1866   apply (erule mult_le_less_imp_less)
1867   apply simp_all
1868 done
1870 text{*It's not obvious whether these should be simprules or not.
1871   Their effect is to gather terms into one big fraction, like
1872   a*b*c / x*y*z. The rationale for that is unclear, but many proofs
1873   seem to need them.*}
1875 declare times_divide_eq [simp]
1878 subsection {* Ordered Fields are Dense *}
1880 lemma less_add_one: "a < (a+1::'a::ordered_semidom)"
1881 proof -
1882   have "a+0 < (a+1::'a::ordered_semidom)"
1883     by (blast intro: zero_less_one add_strict_left_mono)
1884   thus ?thesis by simp
1885 qed
1887 lemma zero_less_two: "0 < (1+1::'a::ordered_semidom)"
1888 by (blast intro: order_less_trans zero_less_one less_add_one)
1890 lemma less_half_sum: "a < b ==> a < (a+b) / (1+1::'a::ordered_field)"
1891 by (simp add: field_simps zero_less_two)
1893 lemma gt_half_sum: "a < b ==> (a+b)/(1+1::'a::ordered_field) < b"
1894 by (simp add: field_simps zero_less_two)
1896 instance ordered_field < dense_linear_order
1897 proof
1898   fix x y :: 'a
1899   have "x < x + 1" by simp
1900   then show "\<exists>y. x < y" ..
1901   have "x - 1 < x" by simp
1902   then show "\<exists>y. y < x" ..
1903   show "x < y \<Longrightarrow> \<exists>z>x. z < y" by (blast intro!: less_half_sum gt_half_sum)
1904 qed
1907 subsection {* Absolute Value *}
1909 lemma mult_sgn_abs: "sgn x * abs x = (x::'a::{ordered_idom,linorder})"
1910 using less_linear[of x 0]
1911 by(auto simp: sgn_if abs_if)
1913 lemma abs_one [simp]: "abs 1 = (1::'a::ordered_idom)"
1914 by (simp add: abs_if zero_less_one [THEN order_less_not_sym])
1916 lemma abs_le_mult: "abs (a * b) \<le> (abs a) * (abs (b::'a::lordered_ring))"
1917 proof -
1918   let ?x = "pprt a * pprt b - pprt a * nprt b - nprt a * pprt b + nprt a * nprt b"
1919   let ?y = "pprt a * pprt b + pprt a * nprt b + nprt a * pprt b + nprt a * nprt b"
1920   have a: "(abs a) * (abs b) = ?x"
1921     by (simp only: abs_prts[of a] abs_prts[of b] ring_simps)
1922   {
1923     fix u v :: 'a
1924     have bh: "\<lbrakk>u = a; v = b\<rbrakk> \<Longrightarrow>
1925               u * v = pprt a * pprt b + pprt a * nprt b +
1926                       nprt a * pprt b + nprt a * nprt b"
1927       apply (subst prts[of u], subst prts[of v])
1929       done
1930   }
1931   note b = this[OF refl[of a] refl[of b]]
1934   have xy: "- ?x <= ?y"
1935     apply (simp)
1936     apply (rule_tac y="0::'a" in order_trans)
1938     apply (simp_all add: mult_nonneg_nonneg mult_nonpos_nonpos)
1940     apply (simp_all add: mult_nonneg_nonneg mult_nonpos_nonpos)
1941     done
1942   have yx: "?y <= ?x"
1944     apply (rule_tac y=0 in order_trans)
1947     done
1948   have i1: "a*b <= abs a * abs b" by (simp only: a b yx)
1949   have i2: "- (abs a * abs b) <= a*b" by (simp only: a b xy)
1950   show ?thesis
1951     apply (rule abs_leI)
1953     apply (simp add: i2[simplified minus_le_iff])
1954     done
1955 qed
1957 lemma abs_eq_mult:
1958   assumes "(0 \<le> a \<or> a \<le> 0) \<and> (0 \<le> b \<or> b \<le> 0)"
1959   shows "abs (a*b) = abs a * abs (b::'a::lordered_ring)"
1960 proof -
1961   have s: "(0 <= a*b) | (a*b <= 0)"
1962     apply (auto)
1963     apply (rule_tac split_mult_pos_le)
1964     apply (rule_tac contrapos_np[of "a*b <= 0"])
1965     apply (simp)
1966     apply (rule_tac split_mult_neg_le)
1967     apply (insert prems)
1968     apply (blast)
1969     done
1970   have mulprts: "a * b = (pprt a + nprt a) * (pprt b + nprt b)"
1972   show ?thesis
1973   proof cases
1974     assume "0 <= a * b"
1975     then show ?thesis
1976       apply (simp_all add: mulprts abs_prts)
1977       apply (insert prems)
1979 	ring_simps
1980 	iffD1[OF zero_le_iff_zero_nprt] iffD1[OF le_zero_iff_zero_pprt]
1981 	iffD1[OF le_zero_iff_pprt_id] iffD1[OF zero_le_iff_nprt_id])
1982 	apply(drule (1) mult_nonneg_nonpos[of a b], simp)
1983 	apply(drule (1) mult_nonneg_nonpos2[of b a], simp)
1984       done
1985   next
1986     assume "~(0 <= a*b)"
1987     with s have "a*b <= 0" by simp
1988     then show ?thesis
1989       apply (simp_all add: mulprts abs_prts)
1990       apply (insert prems)
1991       apply (auto simp add: ring_simps)
1992       apply(drule (1) mult_nonneg_nonneg[of a b],simp)
1993       apply(drule (1) mult_nonpos_nonpos[of a b],simp)
1994       done
1995   qed
1996 qed
1998 lemma abs_mult: "abs (a * b) = abs a * abs (b::'a::ordered_idom)"
1999 by (simp add: abs_eq_mult linorder_linear)
2001 lemma abs_mult_self: "abs a * abs a = a * (a::'a::ordered_idom)"
2004 lemma nonzero_abs_inverse:
2005      "a \<noteq> 0 ==> abs (inverse (a::'a::ordered_field)) = inverse (abs a)"
2006 apply (auto simp add: linorder_neq_iff abs_if nonzero_inverse_minus_eq
2007                       negative_imp_inverse_negative)
2008 apply (blast intro: positive_imp_inverse_positive elim: order_less_asym)
2009 done
2011 lemma abs_inverse [simp]:
2012      "abs (inverse (a::'a::{ordered_field,division_by_zero})) =
2013       inverse (abs a)"
2014 apply (cases "a=0", simp)
2016 done
2018 lemma nonzero_abs_divide:
2019      "b \<noteq> 0 ==> abs (a / (b::'a::ordered_field)) = abs a / abs b"
2020 by (simp add: divide_inverse abs_mult nonzero_abs_inverse)
2022 lemma abs_divide [simp]:
2023      "abs (a / (b::'a::{ordered_field,division_by_zero})) = abs a / abs b"
2024 apply (cases "b=0", simp)
2026 done
2028 lemma abs_mult_less:
2029      "[| abs a < c; abs b < d |] ==> abs a * abs b < c*(d::'a::ordered_idom)"
2030 proof -
2031   assume ac: "abs a < c"
2032   hence cpos: "0<c" by (blast intro: order_le_less_trans abs_ge_zero)
2033   assume "abs b < d"
2034   thus ?thesis by (simp add: ac cpos mult_strict_mono)
2035 qed
2037 lemma eq_minus_self_iff: "(a = -a) = (a = (0::'a::ordered_idom))"
2038 by (force simp add: order_eq_iff le_minus_self_iff minus_le_self_iff)
2040 lemma less_minus_self_iff: "(a < -a) = (a < (0::'a::ordered_idom))"
2041 by (simp add: order_less_le le_minus_self_iff eq_minus_self_iff)
2043 lemma abs_less_iff: "(abs a < b) = (a < b & -a < (b::'a::ordered_idom))"
2044 apply (simp add: order_less_le abs_le_iff)
2045 apply (auto simp add: abs_if minus_le_self_iff eq_minus_self_iff)
2046 apply (simp add: le_minus_self_iff linorder_neq_iff)
2047 done
2049 lemma abs_mult_pos: "(0::'a::ordered_idom) <= x ==>
2050     (abs y) * x = abs (y * x)";
2051   apply (subst abs_mult);
2052   apply simp;
2053 done;
2055 lemma abs_div_pos: "(0::'a::{division_by_zero,ordered_field}) < y ==>
2056     abs x / y = abs (x / y)";
2057   apply (subst abs_divide);
2059 done;
2062 subsection {* Bounds of products via negative and positive Part *}
2064 lemma mult_le_prts:
2065   assumes
2066   "a1 <= (a::'a::lordered_ring)"
2067   "a <= a2"
2068   "b1 <= b"
2069   "b <= b2"
2070   shows
2071   "a * b <= pprt a2 * pprt b2 + pprt a1 * nprt b2 + nprt a2 * pprt b1 + nprt a1 * nprt b1"
2072 proof -
2073   have "a * b = (pprt a + nprt a) * (pprt b + nprt b)"
2074     apply (subst prts[symmetric])+
2075     apply simp
2076     done
2077   then have "a * b = pprt a * pprt b + pprt a * nprt b + nprt a * pprt b + nprt a * nprt b"
2079   moreover have "pprt a * pprt b <= pprt a2 * pprt b2"
2080     by (simp_all add: prems mult_mono)
2081   moreover have "pprt a * nprt b <= pprt a1 * nprt b2"
2082   proof -
2083     have "pprt a * nprt b <= pprt a * nprt b2"
2084       by (simp add: mult_left_mono prems)
2085     moreover have "pprt a * nprt b2 <= pprt a1 * nprt b2"
2086       by (simp add: mult_right_mono_neg prems)
2087     ultimately show ?thesis
2088       by simp
2089   qed
2090   moreover have "nprt a * pprt b <= nprt a2 * pprt b1"
2091   proof -
2092     have "nprt a * pprt b <= nprt a2 * pprt b"
2093       by (simp add: mult_right_mono prems)
2094     moreover have "nprt a2 * pprt b <= nprt a2 * pprt b1"
2095       by (simp add: mult_left_mono_neg prems)
2096     ultimately show ?thesis
2097       by simp
2098   qed
2099   moreover have "nprt a * nprt b <= nprt a1 * nprt b1"
2100   proof -
2101     have "nprt a * nprt b <= nprt a * nprt b1"
2102       by (simp add: mult_left_mono_neg prems)
2103     moreover have "nprt a * nprt b1 <= nprt a1 * nprt b1"
2104       by (simp add: mult_right_mono_neg prems)
2105     ultimately show ?thesis
2106       by simp
2107   qed
2108   ultimately show ?thesis
2109     by - (rule add_mono | simp)+
2110 qed
2112 lemma mult_ge_prts:
2113   assumes
2114   "a1 <= (a::'a::lordered_ring)"
2115   "a <= a2"
2116   "b1 <= b"
2117   "b <= b2"
2118   shows
2119   "a * b >= nprt a1 * pprt b2 + nprt a2 * nprt b2 + pprt a1 * pprt b1 + pprt a2 * nprt b1"
2120 proof -
2121   from prems have a1:"- a2 <= -a" by auto
2122   from prems have a2: "-a <= -a1" by auto
2123   from mult_le_prts[of "-a2" "-a" "-a1" "b1" b "b2", OF a1 a2 prems(3) prems(4), simplified nprt_neg pprt_neg]
2124   have le: "- (a * b) <= - nprt a1 * pprt b2 + - nprt a2 * nprt b2 + - pprt a1 * pprt b1 + - pprt a2 * nprt b1" by simp
2125   then have "-(- nprt a1 * pprt b2 + - nprt a2 * nprt b2 + - pprt a1 * pprt b1 + - pprt a2 * nprt b1) <= a * b"
2126     by (simp only: minus_le_iff)
2127   then show ?thesis by simp
2128 qed
2130 end