src/HOL/Rings.thy
 author haftmann Thu Jan 30 16:09:03 2014 +0100 (2014-01-30) changeset 55187 6d0d93316daf parent 54703 499f92dc6e45 child 55912 e12a0ab9917c permissions -rw-r--r--
split rules for of_bool, similar to if
1 (*  Title:      HOL/Rings.thy
2     Author:     Gertrud Bauer
3     Author:     Steven Obua
4     Author:     Tobias Nipkow
5     Author:     Lawrence C Paulson
6     Author:     Markus Wenzel
8 *)
12 theory Rings
13 imports Groups
14 begin
16 class semiring = ab_semigroup_add + semigroup_mult +
17   assumes distrib_right[algebra_simps, field_simps]: "(a + b) * c = a * c + b * c"
18   assumes distrib_left[algebra_simps, field_simps]: "a * (b + c) = a * b + a * c"
19 begin
21 text{*For the @{text combine_numerals} simproc*}
22 lemma combine_common_factor:
23   "a * e + (b * e + c) = (a + b) * e + c"
26 end
28 class mult_zero = times + zero +
29   assumes mult_zero_left [simp]: "0 * a = 0"
30   assumes mult_zero_right [simp]: "a * 0 = 0"
32 class semiring_0 = semiring + comm_monoid_add + mult_zero
34 class semiring_0_cancel = semiring + cancel_comm_monoid_add
35 begin
37 subclass semiring_0
38 proof
39   fix a :: 'a
40   have "0 * a + 0 * a = 0 * a + 0" by (simp add: distrib_right [symmetric])
41   thus "0 * a = 0" by (simp only: add_left_cancel)
42 next
43   fix a :: 'a
44   have "a * 0 + a * 0 = a * 0 + 0" by (simp add: distrib_left [symmetric])
45   thus "a * 0 = 0" by (simp only: add_left_cancel)
46 qed
48 end
50 class comm_semiring = ab_semigroup_add + ab_semigroup_mult +
51   assumes distrib: "(a + b) * c = a * c + b * c"
52 begin
54 subclass semiring
55 proof
56   fix a b c :: 'a
57   show "(a + b) * c = a * c + b * c" by (simp add: distrib)
58   have "a * (b + c) = (b + c) * a" by (simp add: mult_ac)
59   also have "... = b * a + c * a" by (simp only: distrib)
60   also have "... = a * b + a * c" by (simp add: mult_ac)
61   finally show "a * (b + c) = a * b + a * c" by blast
62 qed
64 end
66 class comm_semiring_0 = comm_semiring + comm_monoid_add + mult_zero
67 begin
69 subclass semiring_0 ..
71 end
73 class comm_semiring_0_cancel = comm_semiring + cancel_comm_monoid_add
74 begin
76 subclass semiring_0_cancel ..
78 subclass comm_semiring_0 ..
80 end
82 class zero_neq_one = zero + one +
83   assumes zero_neq_one [simp]: "0 \<noteq> 1"
84 begin
86 lemma one_neq_zero [simp]: "1 \<noteq> 0"
87 by (rule not_sym) (rule zero_neq_one)
89 definition of_bool :: "bool \<Rightarrow> 'a"
90 where
91   "of_bool p = (if p then 1 else 0)"
93 lemma of_bool_eq [simp, code]:
94   "of_bool False = 0"
95   "of_bool True = 1"
98 lemma of_bool_eq_iff:
99   "of_bool p = of_bool q \<longleftrightarrow> p = q"
102 lemma split_of_bool [split]:
103   "P (of_bool p) \<longleftrightarrow> (p \<longrightarrow> P 1) \<and> (\<not> p \<longrightarrow> P 0)"
104   by (cases p) simp_all
106 lemma split_of_bool_asm:
107   "P (of_bool p) \<longleftrightarrow> \<not> (p \<and> \<not> P 1 \<or> \<not> p \<and> \<not> P 0)"
108   by (cases p) simp_all
110 end
112 class semiring_1 = zero_neq_one + semiring_0 + monoid_mult
114 text {* Abstract divisibility *}
116 class dvd = times
117 begin
119 definition dvd :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "dvd" 50) where
120   "b dvd a \<longleftrightarrow> (\<exists>k. a = b * k)"
122 lemma dvdI [intro?]: "a = b * k \<Longrightarrow> b dvd a"
123   unfolding dvd_def ..
125 lemma dvdE [elim?]: "b dvd a \<Longrightarrow> (\<And>k. a = b * k \<Longrightarrow> P) \<Longrightarrow> P"
126   unfolding dvd_def by blast
128 end
130 class comm_semiring_1 = zero_neq_one + comm_semiring_0 + comm_monoid_mult + dvd
131   (*previously almost_semiring*)
132 begin
134 subclass semiring_1 ..
136 lemma dvd_refl[simp]: "a dvd a"
137 proof
138   show "a = a * 1" by simp
139 qed
141 lemma dvd_trans:
142   assumes "a dvd b" and "b dvd c"
143   shows "a dvd c"
144 proof -
145   from assms obtain v where "b = a * v" by (auto elim!: dvdE)
146   moreover from assms obtain w where "c = b * w" by (auto elim!: dvdE)
147   ultimately have "c = a * (v * w)" by (simp add: mult_assoc)
148   then show ?thesis ..
149 qed
151 lemma dvd_0_left_iff [simp]: "0 dvd a \<longleftrightarrow> a = 0"
152 by (auto intro: dvd_refl elim!: dvdE)
154 lemma dvd_0_right [iff]: "a dvd 0"
155 proof
156   show "0 = a * 0" by simp
157 qed
159 lemma one_dvd [simp]: "1 dvd a"
160 by (auto intro!: dvdI)
162 lemma dvd_mult[simp]: "a dvd c \<Longrightarrow> a dvd (b * c)"
163 by (auto intro!: mult_left_commute dvdI elim!: dvdE)
165 lemma dvd_mult2[simp]: "a dvd b \<Longrightarrow> a dvd (b * c)"
166   apply (subst mult_commute)
167   apply (erule dvd_mult)
168   done
170 lemma dvd_triv_right [simp]: "a dvd b * a"
171 by (rule dvd_mult) (rule dvd_refl)
173 lemma dvd_triv_left [simp]: "a dvd a * b"
174 by (rule dvd_mult2) (rule dvd_refl)
176 lemma mult_dvd_mono:
177   assumes "a dvd b"
178     and "c dvd d"
179   shows "a * c dvd b * d"
180 proof -
181   from a dvd b obtain b' where "b = a * b'" ..
182   moreover from c dvd d obtain d' where "d = c * d'" ..
183   ultimately have "b * d = (a * c) * (b' * d')" by (simp add: mult_ac)
184   then show ?thesis ..
185 qed
187 lemma dvd_mult_left: "a * b dvd c \<Longrightarrow> a dvd c"
188 by (simp add: dvd_def mult_assoc, blast)
190 lemma dvd_mult_right: "a * b dvd c \<Longrightarrow> b dvd c"
191   unfolding mult_ac [of a] by (rule dvd_mult_left)
193 lemma dvd_0_left: "0 dvd a \<Longrightarrow> a = 0"
194 by simp
197   assumes "a dvd b" and "a dvd c" shows "a dvd (b + c)"
198 proof -
199   from a dvd b obtain b' where "b = a * b'" ..
200   moreover from a dvd c obtain c' where "c = a * c'" ..
201   ultimately have "b + c = a * (b' + c')" by (simp add: distrib_left)
202   then show ?thesis ..
203 qed
205 end
207 class no_zero_divisors = zero + times +
208   assumes no_zero_divisors: "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> a * b \<noteq> 0"
209 begin
211 lemma divisors_zero:
212   assumes "a * b = 0"
213   shows "a = 0 \<or> b = 0"
214 proof (rule classical)
215   assume "\<not> (a = 0 \<or> b = 0)"
216   then have "a \<noteq> 0" and "b \<noteq> 0" by auto
217   with no_zero_divisors have "a * b \<noteq> 0" by blast
218   with assms show ?thesis by simp
219 qed
221 end
223 class semiring_1_cancel = semiring + cancel_comm_monoid_add
224   + zero_neq_one + monoid_mult
225 begin
227 subclass semiring_0_cancel ..
229 subclass semiring_1 ..
231 end
233 class comm_semiring_1_cancel = comm_semiring + cancel_comm_monoid_add
234   + zero_neq_one + comm_monoid_mult
235 begin
237 subclass semiring_1_cancel ..
238 subclass comm_semiring_0_cancel ..
239 subclass comm_semiring_1 ..
241 end
243 class ring = semiring + ab_group_add
244 begin
246 subclass semiring_0_cancel ..
248 text {* Distribution rules *}
250 lemma minus_mult_left: "- (a * b) = - a * b"
251 by (rule minus_unique) (simp add: distrib_right [symmetric])
253 lemma minus_mult_right: "- (a * b) = a * - b"
254 by (rule minus_unique) (simp add: distrib_left [symmetric])
256 text{*Extract signs from products*}
257 lemmas mult_minus_left [simp] = minus_mult_left [symmetric]
258 lemmas mult_minus_right [simp] = minus_mult_right [symmetric]
260 lemma minus_mult_minus [simp]: "- a * - b = a * b"
261 by simp
263 lemma minus_mult_commute: "- a * b = a * - b"
264 by simp
266 lemma right_diff_distrib [algebra_simps, field_simps]:
267   "a * (b - c) = a * b - a * c"
268   using distrib_left [of a b "-c "] by simp
270 lemma left_diff_distrib [algebra_simps, field_simps]:
271   "(a - b) * c = a * c - b * c"
272   using distrib_right [of a "- b" c] by simp
274 lemmas ring_distribs =
275   distrib_left distrib_right left_diff_distrib right_diff_distrib
278   "a * e + c = b * e + d \<longleftrightarrow> (a - b) * e + c = d"
282   "a * e + c = b * e + d \<longleftrightarrow> c = (b - a) * e + d"
285 end
287 lemmas ring_distribs =
288   distrib_left distrib_right left_diff_distrib right_diff_distrib
290 class comm_ring = comm_semiring + ab_group_add
291 begin
293 subclass ring ..
294 subclass comm_semiring_0_cancel ..
296 lemma square_diff_square_factored:
297   "x * x - y * y = (x + y) * (x - y)"
300 end
302 class ring_1 = ring + zero_neq_one + monoid_mult
303 begin
305 subclass semiring_1_cancel ..
307 lemma square_diff_one_factored:
308   "x * x - 1 = (x + 1) * (x - 1)"
311 end
313 class comm_ring_1 = comm_ring + zero_neq_one + comm_monoid_mult
314   (*previously ring*)
315 begin
317 subclass ring_1 ..
318 subclass comm_semiring_1_cancel ..
320 lemma dvd_minus_iff [simp]: "x dvd - y \<longleftrightarrow> x dvd y"
321 proof
322   assume "x dvd - y"
323   then have "x dvd - 1 * - y" by (rule dvd_mult)
324   then show "x dvd y" by simp
325 next
326   assume "x dvd y"
327   then have "x dvd - 1 * y" by (rule dvd_mult)
328   then show "x dvd - y" by simp
329 qed
331 lemma minus_dvd_iff [simp]: "- x dvd y \<longleftrightarrow> x dvd y"
332 proof
333   assume "- x dvd y"
334   then obtain k where "y = - x * k" ..
335   then have "y = x * - k" by simp
336   then show "x dvd y" ..
337 next
338   assume "x dvd y"
339   then obtain k where "y = x * k" ..
340   then have "y = - x * - k" by simp
341   then show "- x dvd y" ..
342 qed
344 lemma dvd_diff [simp]:
345   "x dvd y \<Longrightarrow> x dvd z \<Longrightarrow> x dvd (y - z)"
346   using dvd_add [of x y "- z"] by simp
348 end
350 class ring_no_zero_divisors = ring + no_zero_divisors
351 begin
353 lemma mult_eq_0_iff [simp]:
354   shows "a * b = 0 \<longleftrightarrow> (a = 0 \<or> b = 0)"
355 proof (cases "a = 0 \<or> b = 0")
356   case False then have "a \<noteq> 0" and "b \<noteq> 0" by auto
357     then show ?thesis using no_zero_divisors by simp
358 next
359   case True then show ?thesis by auto
360 qed
362 text{*Cancellation of equalities with a common factor*}
363 lemma mult_cancel_right [simp]:
364   "a * c = b * c \<longleftrightarrow> c = 0 \<or> a = b"
365 proof -
366   have "(a * c = b * c) = ((a - b) * c = 0)"
368   thus ?thesis by (simp add: disj_commute)
369 qed
371 lemma mult_cancel_left [simp]:
372   "c * a = c * b \<longleftrightarrow> c = 0 \<or> a = b"
373 proof -
374   have "(c * a = c * b) = (c * (a - b) = 0)"
376   thus ?thesis by simp
377 qed
379 end
381 class ring_1_no_zero_divisors = ring_1 + ring_no_zero_divisors
382 begin
384 lemma square_eq_1_iff:
385   "x * x = 1 \<longleftrightarrow> x = 1 \<or> x = - 1"
386 proof -
387   have "(x - 1) * (x + 1) = x * x - 1"
389   hence "x * x = 1 \<longleftrightarrow> (x - 1) * (x + 1) = 0"
390     by simp
391   thus ?thesis
393 qed
395 lemma mult_cancel_right1 [simp]:
396   "c = b * c \<longleftrightarrow> c = 0 \<or> b = 1"
397 by (insert mult_cancel_right [of 1 c b], force)
399 lemma mult_cancel_right2 [simp]:
400   "a * c = c \<longleftrightarrow> c = 0 \<or> a = 1"
401 by (insert mult_cancel_right [of a c 1], simp)
403 lemma mult_cancel_left1 [simp]:
404   "c = c * b \<longleftrightarrow> c = 0 \<or> b = 1"
405 by (insert mult_cancel_left [of c 1 b], force)
407 lemma mult_cancel_left2 [simp]:
408   "c * a = c \<longleftrightarrow> c = 0 \<or> a = 1"
409 by (insert mult_cancel_left [of c a 1], simp)
411 end
413 class idom = comm_ring_1 + no_zero_divisors
414 begin
416 subclass ring_1_no_zero_divisors ..
418 lemma square_eq_iff: "a * a = b * b \<longleftrightarrow> (a = b \<or> a = - b)"
419 proof
420   assume "a * a = b * b"
421   then have "(a - b) * (a + b) = 0"
423   then show "a = b \<or> a = - b"
425 next
426   assume "a = b \<or> a = - b"
427   then show "a * a = b * b" by auto
428 qed
430 lemma dvd_mult_cancel_right [simp]:
431   "a * c dvd b * c \<longleftrightarrow> c = 0 \<or> a dvd b"
432 proof -
433   have "a * c dvd b * c \<longleftrightarrow> (\<exists>k. b * c = (a * k) * c)"
434     unfolding dvd_def by (simp add: mult_ac)
435   also have "(\<exists>k. b * c = (a * k) * c) \<longleftrightarrow> c = 0 \<or> a dvd b"
436     unfolding dvd_def by simp
437   finally show ?thesis .
438 qed
440 lemma dvd_mult_cancel_left [simp]:
441   "c * a dvd c * b \<longleftrightarrow> c = 0 \<or> a dvd b"
442 proof -
443   have "c * a dvd c * b \<longleftrightarrow> (\<exists>k. b * c = (a * k) * c)"
444     unfolding dvd_def by (simp add: mult_ac)
445   also have "(\<exists>k. b * c = (a * k) * c) \<longleftrightarrow> c = 0 \<or> a dvd b"
446     unfolding dvd_def by simp
447   finally show ?thesis .
448 qed
450 end
452 text {*
453   The theory of partially ordered rings is taken from the books:
454   \begin{itemize}
455   \item \emph{Lattice Theory} by Garret Birkhoff, American Mathematical Society 1979
456   \item \emph{Partially Ordered Algebraic Systems}, Pergamon Press 1963
457   \end{itemize}
458   Most of the used notions can also be looked up in
459   \begin{itemize}
460   \item @{url "http://www.mathworld.com"} by Eric Weisstein et. al.
461   \item \emph{Algebra I} by van der Waerden, Springer.
462   \end{itemize}
463 *}
466   assumes mult_left_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b"
467   assumes mult_right_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a * c \<le> b * c"
468 begin
470 lemma mult_mono:
471   "a \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a * c \<le> b * d"
472 apply (erule mult_right_mono [THEN order_trans], assumption)
473 apply (erule mult_left_mono, assumption)
474 done
476 lemma mult_mono':
477   "a \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> 0 \<le> a \<Longrightarrow> 0 \<le> c \<Longrightarrow> a * c \<le> b * d"
478 apply (rule mult_mono)
479 apply (fast intro: order_trans)+
480 done
482 end
484 class ordered_cancel_semiring = ordered_semiring + cancel_comm_monoid_add
485 begin
487 subclass semiring_0_cancel ..
489 lemma mult_nonneg_nonneg: "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> a * b"
490 using mult_left_mono [of 0 b a] by simp
492 lemma mult_nonneg_nonpos: "0 \<le> a \<Longrightarrow> b \<le> 0 \<Longrightarrow> a * b \<le> 0"
493 using mult_left_mono [of b 0 a] by simp
495 lemma mult_nonpos_nonneg: "a \<le> 0 \<Longrightarrow> 0 \<le> b \<Longrightarrow> a * b \<le> 0"
496 using mult_right_mono [of a 0 b] by simp
498 text {* Legacy - use @{text mult_nonpos_nonneg} *}
499 lemma mult_nonneg_nonpos2: "0 \<le> a \<Longrightarrow> b \<le> 0 \<Longrightarrow> b * a \<le> 0"
500 by (drule mult_right_mono [of b 0], auto)
502 lemma split_mult_neg_le: "(0 \<le> a & b \<le> 0) | (a \<le> 0 & 0 \<le> b) \<Longrightarrow> a * b \<le> 0"
503 by (auto simp add: mult_nonneg_nonpos mult_nonneg_nonpos2)
505 end
507 class linordered_semiring = ordered_semiring + linordered_cancel_ab_semigroup_add
508 begin
510 subclass ordered_cancel_semiring ..
514 lemma mult_left_less_imp_less:
515   "c * a < c * b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a < b"
516 by (force simp add: mult_left_mono not_le [symmetric])
518 lemma mult_right_less_imp_less:
519   "a * c < b * c \<Longrightarrow> 0 \<le> c \<Longrightarrow> a < b"
520 by (force simp add: mult_right_mono not_le [symmetric])
522 end
524 class linordered_semiring_1 = linordered_semiring + semiring_1
525 begin
527 lemma convex_bound_le:
528   assumes "x \<le> a" "y \<le> a" "0 \<le> u" "0 \<le> v" "u + v = 1"
529   shows "u * x + v * y \<le> a"
530 proof-
531   from assms have "u * x + v * y \<le> u * a + v * a"
533   thus ?thesis using assms unfolding distrib_right[symmetric] by simp
534 qed
536 end
539   assumes mult_strict_left_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b"
540   assumes mult_strict_right_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> a * c < b * c"
541 begin
543 subclass semiring_0_cancel ..
545 subclass linordered_semiring
546 proof
547   fix a b c :: 'a
548   assume A: "a \<le> b" "0 \<le> c"
549   from A show "c * a \<le> c * b"
550     unfolding le_less
551     using mult_strict_left_mono by (cases "c = 0") auto
552   from A show "a * c \<le> b * c"
553     unfolding le_less
554     using mult_strict_right_mono by (cases "c = 0") auto
555 qed
557 lemma mult_left_le_imp_le:
558   "c * a \<le> c * b \<Longrightarrow> 0 < c \<Longrightarrow> a \<le> b"
559 by (force simp add: mult_strict_left_mono _not_less [symmetric])
561 lemma mult_right_le_imp_le:
562   "a * c \<le> b * c \<Longrightarrow> 0 < c \<Longrightarrow> a \<le> b"
563 by (force simp add: mult_strict_right_mono not_less [symmetric])
565 lemma mult_pos_pos: "0 < a \<Longrightarrow> 0 < b \<Longrightarrow> 0 < a * b"
566 using mult_strict_left_mono [of 0 b a] by simp
568 lemma mult_pos_neg: "0 < a \<Longrightarrow> b < 0 \<Longrightarrow> a * b < 0"
569 using mult_strict_left_mono [of b 0 a] by simp
571 lemma mult_neg_pos: "a < 0 \<Longrightarrow> 0 < b \<Longrightarrow> a * b < 0"
572 using mult_strict_right_mono [of a 0 b] by simp
574 text {* Legacy - use @{text mult_neg_pos} *}
575 lemma mult_pos_neg2: "0 < a \<Longrightarrow> b < 0 \<Longrightarrow> b * a < 0"
576 by (drule mult_strict_right_mono [of b 0], auto)
578 lemma zero_less_mult_pos:
579   "0 < a * b \<Longrightarrow> 0 < a \<Longrightarrow> 0 < b"
580 apply (cases "b\<le>0")
581  apply (auto simp add: le_less not_less)
582 apply (drule_tac mult_pos_neg [of a b])
583  apply (auto dest: less_not_sym)
584 done
586 lemma zero_less_mult_pos2:
587   "0 < b * a \<Longrightarrow> 0 < a \<Longrightarrow> 0 < b"
588 apply (cases "b\<le>0")
589  apply (auto simp add: le_less not_less)
590 apply (drule_tac mult_pos_neg2 [of a b])
591  apply (auto dest: less_not_sym)
592 done
594 text{*Strict monotonicity in both arguments*}
595 lemma mult_strict_mono:
596   assumes "a < b" and "c < d" and "0 < b" and "0 \<le> c"
597   shows "a * c < b * d"
598   using assms apply (cases "c=0")
600   apply (erule mult_strict_right_mono [THEN less_trans])
601   apply (force simp add: le_less)
602   apply (erule mult_strict_left_mono, assumption)
603   done
605 text{*This weaker variant has more natural premises*}
606 lemma mult_strict_mono':
607   assumes "a < b" and "c < d" and "0 \<le> a" and "0 \<le> c"
608   shows "a * c < b * d"
609 by (rule mult_strict_mono) (insert assms, auto)
611 lemma mult_less_le_imp_less:
612   assumes "a < b" and "c \<le> d" and "0 \<le> a" and "0 < c"
613   shows "a * c < b * d"
614   using assms apply (subgoal_tac "a * c < b * c")
615   apply (erule less_le_trans)
616   apply (erule mult_left_mono)
617   apply simp
618   apply (erule mult_strict_right_mono)
619   apply assumption
620   done
622 lemma mult_le_less_imp_less:
623   assumes "a \<le> b" and "c < d" and "0 < a" and "0 \<le> c"
624   shows "a * c < b * d"
625   using assms apply (subgoal_tac "a * c \<le> b * c")
626   apply (erule le_less_trans)
627   apply (erule mult_strict_left_mono)
628   apply simp
629   apply (erule mult_right_mono)
630   apply simp
631   done
633 lemma mult_less_imp_less_left:
634   assumes less: "c * a < c * b" and nonneg: "0 \<le> c"
635   shows "a < b"
636 proof (rule ccontr)
637   assume "\<not>  a < b"
638   hence "b \<le> a" by (simp add: linorder_not_less)
639   hence "c * b \<le> c * a" using nonneg by (rule mult_left_mono)
640   with this and less show False by (simp add: not_less [symmetric])
641 qed
643 lemma mult_less_imp_less_right:
644   assumes less: "a * c < b * c" and nonneg: "0 \<le> c"
645   shows "a < b"
646 proof (rule ccontr)
647   assume "\<not> a < b"
648   hence "b \<le> a" by (simp add: linorder_not_less)
649   hence "b * c \<le> a * c" using nonneg by (rule mult_right_mono)
650   with this and less show False by (simp add: not_less [symmetric])
651 qed
653 end
655 class linordered_semiring_1_strict = linordered_semiring_strict + semiring_1
656 begin
658 subclass linordered_semiring_1 ..
660 lemma convex_bound_lt:
661   assumes "x < a" "y < a" "0 \<le> u" "0 \<le> v" "u + v = 1"
662   shows "u * x + v * y < a"
663 proof -
664   from assms have "u * x + v * y < u * a + v * a"
665     by (cases "u = 0")
666        (auto intro!: add_less_le_mono mult_strict_left_mono mult_left_mono)
667   thus ?thesis using assms unfolding distrib_right[symmetric] by simp
668 qed
670 end
672 class ordered_comm_semiring = comm_semiring_0 + ordered_ab_semigroup_add +
673   assumes comm_mult_left_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b"
674 begin
676 subclass ordered_semiring
677 proof
678   fix a b c :: 'a
679   assume "a \<le> b" "0 \<le> c"
680   thus "c * a \<le> c * b" by (rule comm_mult_left_mono)
681   thus "a * c \<le> b * c" by (simp only: mult_commute)
682 qed
684 end
686 class ordered_cancel_comm_semiring = ordered_comm_semiring + cancel_comm_monoid_add
687 begin
689 subclass comm_semiring_0_cancel ..
690 subclass ordered_comm_semiring ..
691 subclass ordered_cancel_semiring ..
693 end
695 class linordered_comm_semiring_strict = comm_semiring_0 + linordered_cancel_ab_semigroup_add +
696   assumes comm_mult_strict_left_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b"
697 begin
699 subclass linordered_semiring_strict
700 proof
701   fix a b c :: 'a
702   assume "a < b" "0 < c"
703   thus "c * a < c * b" by (rule comm_mult_strict_left_mono)
704   thus "a * c < b * c" by (simp only: mult_commute)
705 qed
707 subclass ordered_cancel_comm_semiring
708 proof
709   fix a b c :: 'a
710   assume "a \<le> b" "0 \<le> c"
711   thus "c * a \<le> c * b"
712     unfolding le_less
713     using mult_strict_left_mono by (cases "c = 0") auto
714 qed
716 end
718 class ordered_ring = ring + ordered_cancel_semiring
719 begin
724   "a * e + c < b * e + d \<longleftrightarrow> (a - b) * e + c < d"
728   "a * e + c < b * e + d \<longleftrightarrow> c < (b - a) * e + d"
732   "a * e + c \<le> b * e + d \<longleftrightarrow> (a - b) * e + c \<le> d"
736   "a * e + c \<le> b * e + d \<longleftrightarrow> c \<le> (b - a) * e + d"
739 lemma mult_left_mono_neg:
740   "b \<le> a \<Longrightarrow> c \<le> 0 \<Longrightarrow> c * a \<le> c * b"
741   apply (drule mult_left_mono [of _ _ "- c"])
742   apply simp_all
743   done
745 lemma mult_right_mono_neg:
746   "b \<le> a \<Longrightarrow> c \<le> 0 \<Longrightarrow> a * c \<le> b * c"
747   apply (drule mult_right_mono [of _ _ "- c"])
748   apply simp_all
749   done
751 lemma mult_nonpos_nonpos: "a \<le> 0 \<Longrightarrow> b \<le> 0 \<Longrightarrow> 0 \<le> a * b"
752 using mult_right_mono_neg [of a 0 b] by simp
754 lemma split_mult_pos_le:
755   "(0 \<le> a \<and> 0 \<le> b) \<or> (a \<le> 0 \<and> b \<le> 0) \<Longrightarrow> 0 \<le> a * b"
756 by (auto simp add: mult_nonneg_nonneg mult_nonpos_nonpos)
758 end
760 class linordered_ring = ring + linordered_semiring + linordered_ab_group_add + abs_if
761 begin
763 subclass ordered_ring ..
766 proof
767   fix a b
768   show "\<bar>a + b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>"
770 qed (auto simp add: abs_if)
772 lemma zero_le_square [simp]: "0 \<le> a * a"
773   using linear [of 0 a]
774   by (auto simp add: mult_nonneg_nonneg mult_nonpos_nonpos)
776 lemma not_square_less_zero [simp]: "\<not> (a * a < 0)"
779 end
781 (* The "strict" suffix can be seen as describing the combination of linordered_ring and no_zero_divisors.
782    Basically, linordered_ring + no_zero_divisors = linordered_ring_strict.
783  *)
784 class linordered_ring_strict = ring + linordered_semiring_strict
786 begin
788 subclass linordered_ring ..
790 lemma mult_strict_left_mono_neg: "b < a \<Longrightarrow> c < 0 \<Longrightarrow> c * a < c * b"
791 using mult_strict_left_mono [of b a "- c"] by simp
793 lemma mult_strict_right_mono_neg: "b < a \<Longrightarrow> c < 0 \<Longrightarrow> a * c < b * c"
794 using mult_strict_right_mono [of b a "- c"] by simp
796 lemma mult_neg_neg: "a < 0 \<Longrightarrow> b < 0 \<Longrightarrow> 0 < a * b"
797 using mult_strict_right_mono_neg [of a 0 b] by simp
799 subclass ring_no_zero_divisors
800 proof
801   fix a b
802   assume "a \<noteq> 0" then have A: "a < 0 \<or> 0 < a" by (simp add: neq_iff)
803   assume "b \<noteq> 0" then have B: "b < 0 \<or> 0 < b" by (simp add: neq_iff)
804   have "a * b < 0 \<or> 0 < a * b"
805   proof (cases "a < 0")
806     case True note A' = this
807     show ?thesis proof (cases "b < 0")
808       case True with A'
809       show ?thesis by (auto dest: mult_neg_neg)
810     next
811       case False with B have "0 < b" by auto
812       with A' show ?thesis by (auto dest: mult_strict_right_mono)
813     qed
814   next
815     case False with A have A': "0 < a" by auto
816     show ?thesis proof (cases "b < 0")
817       case True with A'
818       show ?thesis by (auto dest: mult_strict_right_mono_neg)
819     next
820       case False with B have "0 < b" by auto
821       with A' show ?thesis by (auto dest: mult_pos_pos)
822     qed
823   qed
824   then show "a * b \<noteq> 0" by (simp add: neq_iff)
825 qed
827 lemma zero_less_mult_iff:
828   "0 < a * b \<longleftrightarrow> 0 < a \<and> 0 < b \<or> a < 0 \<and> b < 0"
829   apply (auto simp add: mult_pos_pos mult_neg_neg)
830   apply (simp_all add: not_less le_less)
831   apply (erule disjE) apply assumption defer
832   apply (erule disjE) defer apply (drule sym) apply simp
833   apply (erule disjE) defer apply (drule sym) apply simp
834   apply (erule disjE) apply assumption apply (drule sym) apply simp
835   apply (drule sym) apply simp
836   apply (blast dest: zero_less_mult_pos)
837   apply (blast dest: zero_less_mult_pos2)
838   done
840 lemma zero_le_mult_iff:
841   "0 \<le> a * b \<longleftrightarrow> 0 \<le> a \<and> 0 \<le> b \<or> a \<le> 0 \<and> b \<le> 0"
842 by (auto simp add: eq_commute [of 0] le_less not_less zero_less_mult_iff)
844 lemma mult_less_0_iff:
845   "a * b < 0 \<longleftrightarrow> 0 < a \<and> b < 0 \<or> a < 0 \<and> 0 < b"
846   apply (insert zero_less_mult_iff [of "-a" b])
847   apply force
848   done
850 lemma mult_le_0_iff:
851   "a * b \<le> 0 \<longleftrightarrow> 0 \<le> a \<and> b \<le> 0 \<or> a \<le> 0 \<and> 0 \<le> b"
852   apply (insert zero_le_mult_iff [of "-a" b])
853   apply force
854   done
856 text{*Cancellation laws for @{term "c*a < c*b"} and @{term "a*c < b*c"},
857    also with the relations @{text "\<le>"} and equality.*}
859 text{*These disjunction'' versions produce two cases when the comparison is
860  an assumption, but effectively four when the comparison is a goal.*}
862 lemma mult_less_cancel_right_disj:
863   "a * c < b * c \<longleftrightarrow> 0 < c \<and> a < b \<or> c < 0 \<and>  b < a"
864   apply (cases "c = 0")
865   apply (auto simp add: neq_iff mult_strict_right_mono
866                       mult_strict_right_mono_neg)
867   apply (auto simp add: not_less
868                       not_le [symmetric, of "a*c"]
869                       not_le [symmetric, of a])
870   apply (erule_tac [!] notE)
871   apply (auto simp add: less_imp_le mult_right_mono
872                       mult_right_mono_neg)
873   done
875 lemma mult_less_cancel_left_disj:
876   "c * a < c * b \<longleftrightarrow> 0 < c \<and> a < b \<or> c < 0 \<and>  b < a"
877   apply (cases "c = 0")
878   apply (auto simp add: neq_iff mult_strict_left_mono
879                       mult_strict_left_mono_neg)
880   apply (auto simp add: not_less
881                       not_le [symmetric, of "c*a"]
882                       not_le [symmetric, of a])
883   apply (erule_tac [!] notE)
884   apply (auto simp add: less_imp_le mult_left_mono
885                       mult_left_mono_neg)
886   done
888 text{*The conjunction of implication'' lemmas produce two cases when the
889 comparison is a goal, but give four when the comparison is an assumption.*}
891 lemma mult_less_cancel_right:
892   "a * c < b * c \<longleftrightarrow> (0 \<le> c \<longrightarrow> a < b) \<and> (c \<le> 0 \<longrightarrow> b < a)"
893   using mult_less_cancel_right_disj [of a c b] by auto
895 lemma mult_less_cancel_left:
896   "c * a < c * b \<longleftrightarrow> (0 \<le> c \<longrightarrow> a < b) \<and> (c \<le> 0 \<longrightarrow> b < a)"
897   using mult_less_cancel_left_disj [of c a b] by auto
899 lemma mult_le_cancel_right:
900    "a * c \<le> b * c \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> a)"
901 by (simp add: not_less [symmetric] mult_less_cancel_right_disj)
903 lemma mult_le_cancel_left:
904   "c * a \<le> c * b \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> a)"
905 by (simp add: not_less [symmetric] mult_less_cancel_left_disj)
907 lemma mult_le_cancel_left_pos:
908   "0 < c \<Longrightarrow> c * a \<le> c * b \<longleftrightarrow> a \<le> b"
909 by (auto simp: mult_le_cancel_left)
911 lemma mult_le_cancel_left_neg:
912   "c < 0 \<Longrightarrow> c * a \<le> c * b \<longleftrightarrow> b \<le> a"
913 by (auto simp: mult_le_cancel_left)
915 lemma mult_less_cancel_left_pos:
916   "0 < c \<Longrightarrow> c * a < c * b \<longleftrightarrow> a < b"
917 by (auto simp: mult_less_cancel_left)
919 lemma mult_less_cancel_left_neg:
920   "c < 0 \<Longrightarrow> c * a < c * b \<longleftrightarrow> b < a"
921 by (auto simp: mult_less_cancel_left)
923 end
925 lemmas mult_sign_intros =
926   mult_nonneg_nonneg mult_nonneg_nonpos
927   mult_nonpos_nonneg mult_nonpos_nonpos
928   mult_pos_pos mult_pos_neg
929   mult_neg_pos mult_neg_neg
931 class ordered_comm_ring = comm_ring + ordered_comm_semiring
932 begin
934 subclass ordered_ring ..
935 subclass ordered_cancel_comm_semiring ..
937 end
939 class linordered_semidom = comm_semiring_1_cancel + linordered_comm_semiring_strict +
940   (*previously linordered_semiring*)
941   assumes zero_less_one [simp]: "0 < 1"
942 begin
945   shows "0 < a \<Longrightarrow> b < c \<Longrightarrow> b < a + c"
946   using add_strict_mono [of 0 a b c] by simp
948 lemma zero_le_one [simp]: "0 \<le> 1"
949 by (rule zero_less_one [THEN less_imp_le])
951 lemma not_one_le_zero [simp]: "\<not> 1 \<le> 0"
954 lemma not_one_less_zero [simp]: "\<not> 1 < 0"
957 lemma less_1_mult:
958   assumes "1 < m" and "1 < n"
959   shows "1 < m * n"
960   using assms mult_strict_mono [of 1 m 1 n]
961     by (simp add:  less_trans [OF zero_less_one])
963 end
965 class linordered_idom = comm_ring_1 +
967   abs_if + sgn_if
968   (*previously linordered_ring*)
969 begin
971 subclass linordered_semiring_1_strict ..
972 subclass linordered_ring_strict ..
973 subclass ordered_comm_ring ..
974 subclass idom ..
976 subclass linordered_semidom
977 proof
978   have "0 \<le> 1 * 1" by (rule zero_le_square)
979   thus "0 < 1" by (simp add: le_less)
980 qed
982 lemma linorder_neqE_linordered_idom:
983   assumes "x \<noteq> y" obtains "x < y" | "y < x"
984   using assms by (rule neqE)
986 text {* These cancellation simprules also produce two cases when the comparison is a goal. *}
988 lemma mult_le_cancel_right1:
989   "c \<le> b * c \<longleftrightarrow> (0 < c \<longrightarrow> 1 \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> 1)"
990 by (insert mult_le_cancel_right [of 1 c b], simp)
992 lemma mult_le_cancel_right2:
993   "a * c \<le> c \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> 1) \<and> (c < 0 \<longrightarrow> 1 \<le> a)"
994 by (insert mult_le_cancel_right [of a c 1], simp)
996 lemma mult_le_cancel_left1:
997   "c \<le> c * b \<longleftrightarrow> (0 < c \<longrightarrow> 1 \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> 1)"
998 by (insert mult_le_cancel_left [of c 1 b], simp)
1000 lemma mult_le_cancel_left2:
1001   "c * a \<le> c \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> 1) \<and> (c < 0 \<longrightarrow> 1 \<le> a)"
1002 by (insert mult_le_cancel_left [of c a 1], simp)
1004 lemma mult_less_cancel_right1:
1005   "c < b * c \<longleftrightarrow> (0 \<le> c \<longrightarrow> 1 < b) \<and> (c \<le> 0 \<longrightarrow> b < 1)"
1006 by (insert mult_less_cancel_right [of 1 c b], simp)
1008 lemma mult_less_cancel_right2:
1009   "a * c < c \<longleftrightarrow> (0 \<le> c \<longrightarrow> a < 1) \<and> (c \<le> 0 \<longrightarrow> 1 < a)"
1010 by (insert mult_less_cancel_right [of a c 1], simp)
1012 lemma mult_less_cancel_left1:
1013   "c < c * b \<longleftrightarrow> (0 \<le> c \<longrightarrow> 1 < b) \<and> (c \<le> 0 \<longrightarrow> b < 1)"
1014 by (insert mult_less_cancel_left [of c 1 b], simp)
1016 lemma mult_less_cancel_left2:
1017   "c * a < c \<longleftrightarrow> (0 \<le> c \<longrightarrow> a < 1) \<and> (c \<le> 0 \<longrightarrow> 1 < a)"
1018 by (insert mult_less_cancel_left [of c a 1], simp)
1020 lemma sgn_sgn [simp]:
1021   "sgn (sgn a) = sgn a"
1022 unfolding sgn_if by simp
1024 lemma sgn_0_0:
1025   "sgn a = 0 \<longleftrightarrow> a = 0"
1026 unfolding sgn_if by simp
1028 lemma sgn_1_pos:
1029   "sgn a = 1 \<longleftrightarrow> a > 0"
1030 unfolding sgn_if by simp
1032 lemma sgn_1_neg:
1033   "sgn a = - 1 \<longleftrightarrow> a < 0"
1034 unfolding sgn_if by auto
1036 lemma sgn_pos [simp]:
1037   "0 < a \<Longrightarrow> sgn a = 1"
1038 unfolding sgn_1_pos .
1040 lemma sgn_neg [simp]:
1041   "a < 0 \<Longrightarrow> sgn a = - 1"
1042 unfolding sgn_1_neg .
1044 lemma sgn_times:
1045   "sgn (a * b) = sgn a * sgn b"
1046 by (auto simp add: sgn_if zero_less_mult_iff)
1048 lemma abs_sgn: "\<bar>k\<bar> = k * sgn k"
1049 unfolding sgn_if abs_if by auto
1051 lemma sgn_greater [simp]:
1052   "0 < sgn a \<longleftrightarrow> 0 < a"
1053   unfolding sgn_if by auto
1055 lemma sgn_less [simp]:
1056   "sgn a < 0 \<longleftrightarrow> a < 0"
1057   unfolding sgn_if by auto
1059 lemma abs_dvd_iff [simp]: "\<bar>m\<bar> dvd k \<longleftrightarrow> m dvd k"
1062 lemma dvd_abs_iff [simp]: "m dvd \<bar>k\<bar> \<longleftrightarrow> m dvd k"
1065 lemma dvd_if_abs_eq:
1066   "\<bar>l\<bar> = \<bar>k\<bar> \<Longrightarrow> l dvd k"
1067 by(subst abs_dvd_iff[symmetric]) simp
1069 text {* The following lemmas can be proven in more generale structures, but
1070 are dangerous as simp rules in absence of @{thm neg_equal_zero},
1071 @{thm neg_less_pos}, @{thm neg_less_eq_nonneg}. *}
1073 lemma equation_minus_iff_1 [simp, no_atp]:
1074   "1 = - a \<longleftrightarrow> a = - 1"
1075   by (fact equation_minus_iff)
1077 lemma minus_equation_iff_1 [simp, no_atp]:
1078   "- a = 1 \<longleftrightarrow> a = - 1"
1079   by (subst minus_equation_iff, auto)
1081 lemma le_minus_iff_1 [simp, no_atp]:
1082   "1 \<le> - b \<longleftrightarrow> b \<le> - 1"
1083   by (fact le_minus_iff)
1085 lemma minus_le_iff_1 [simp, no_atp]:
1086   "- a \<le> 1 \<longleftrightarrow> - 1 \<le> a"
1087   by (fact minus_le_iff)
1089 lemma less_minus_iff_1 [simp, no_atp]:
1090   "1 < - b \<longleftrightarrow> b < - 1"
1091   by (fact less_minus_iff)
1093 lemma minus_less_iff_1 [simp, no_atp]:
1094   "- a < 1 \<longleftrightarrow> - 1 < a"
1095   by (fact minus_less_iff)
1097 end
1099 text {* Simprules for comparisons where common factors can be cancelled. *}
1101 lemmas mult_compare_simps =
1102     mult_le_cancel_right mult_le_cancel_left
1103     mult_le_cancel_right1 mult_le_cancel_right2
1104     mult_le_cancel_left1 mult_le_cancel_left2
1105     mult_less_cancel_right mult_less_cancel_left
1106     mult_less_cancel_right1 mult_less_cancel_right2
1107     mult_less_cancel_left1 mult_less_cancel_left2
1108     mult_cancel_right mult_cancel_left
1109     mult_cancel_right1 mult_cancel_right2
1110     mult_cancel_left1 mult_cancel_left2
1112 text {* Reasoning about inequalities with division *}
1114 context linordered_semidom
1115 begin
1117 lemma less_add_one: "a < a + 1"
1118 proof -
1119   have "a + 0 < a + 1"
1120     by (blast intro: zero_less_one add_strict_left_mono)
1121   thus ?thesis by simp
1122 qed
1124 lemma zero_less_two: "0 < 1 + 1"
1125 by (blast intro: less_trans zero_less_one less_add_one)
1127 end
1129 context linordered_idom
1130 begin
1132 lemma mult_right_le_one_le:
1133   "0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> y \<le> 1 \<Longrightarrow> x * y \<le> x"
1134   by (auto simp add: mult_le_cancel_left2)
1136 lemma mult_left_le_one_le:
1137   "0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> y \<le> 1 \<Longrightarrow> y * x \<le> x"
1138   by (auto simp add: mult_le_cancel_right2)
1140 end
1142 text {* Absolute Value *}
1144 context linordered_idom
1145 begin
1147 lemma mult_sgn_abs:
1148   "sgn x * \<bar>x\<bar> = x"
1149   unfolding abs_if sgn_if by auto
1151 lemma abs_one [simp]:
1152   "\<bar>1\<bar> = 1"
1155 end
1157 class ordered_ring_abs = ordered_ring + ordered_ab_group_add_abs +
1158   assumes abs_eq_mult:
1159     "(0 \<le> a \<or> a \<le> 0) \<and> (0 \<le> b \<or> b \<le> 0) \<Longrightarrow> \<bar>a * b\<bar> = \<bar>a\<bar> * \<bar>b\<bar>"
1161 context linordered_idom
1162 begin
1164 subclass ordered_ring_abs proof
1165 qed (auto simp add: abs_if not_less mult_less_0_iff)
1167 lemma abs_mult:
1168   "\<bar>a * b\<bar> = \<bar>a\<bar> * \<bar>b\<bar>"
1169   by (rule abs_eq_mult) auto
1171 lemma abs_mult_self:
1172   "\<bar>a\<bar> * \<bar>a\<bar> = a * a"
1175 lemma abs_mult_less:
1176   "\<bar>a\<bar> < c \<Longrightarrow> \<bar>b\<bar> < d \<Longrightarrow> \<bar>a\<bar> * \<bar>b\<bar> < c * d"
1177 proof -
1178   assume ac: "\<bar>a\<bar> < c"
1179   hence cpos: "0<c" by (blast intro: le_less_trans abs_ge_zero)
1180   assume "\<bar>b\<bar> < d"
1181   thus ?thesis by (simp add: ac cpos mult_strict_mono)
1182 qed
1184 lemma abs_less_iff:
1185   "\<bar>a\<bar> < b \<longleftrightarrow> a < b \<and> - a < b"