src/HOL/Rings.thy
 author blanchet Tue Nov 07 15:16:42 2017 +0100 (19 months ago) changeset 67022 49309fe530fd parent 66937 a1a4a5e2933a child 67051 e7e54a0b9197 permissions -rw-r--r--
more robust parsing for THF proofs (esp. polymorphic Leo-III proofs)
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 *)
10 section \<open>Rings\<close>
12 theory Rings
13   imports Groups Set
14 begin
16 class semiring = ab_semigroup_add + semigroup_mult +
17   assumes distrib_right[algebra_simps]: "(a + b) * c = a * c + b * c"
18   assumes distrib_left[algebra_simps]: "a * (b + c) = a * b + a * c"
19 begin
21 text \<open>For the \<open>combine_numerals\<close> simproc\<close>
22 lemma combine_common_factor: "a * e + (b * e + c) = (a + b) * e + c"
23   by (simp add: distrib_right ac_simps)
25 end
27 class mult_zero = times + zero +
28   assumes mult_zero_left [simp]: "0 * a = 0"
29   assumes mult_zero_right [simp]: "a * 0 = 0"
30 begin
32 lemma mult_not_zero: "a * b \<noteq> 0 \<Longrightarrow> a \<noteq> 0 \<and> b \<noteq> 0"
33   by auto
35 end
37 class semiring_0 = semiring + comm_monoid_add + mult_zero
39 class semiring_0_cancel = semiring + cancel_comm_monoid_add
40 begin
42 subclass semiring_0
43 proof
44   fix a :: 'a
45   have "0 * a + 0 * a = 0 * a + 0"
46     by (simp add: distrib_right [symmetric])
47   then show "0 * a = 0"
49   have "a * 0 + a * 0 = a * 0 + 0"
50     by (simp add: distrib_left [symmetric])
51   then show "a * 0 = 0"
53 qed
55 end
57 class comm_semiring = ab_semigroup_add + ab_semigroup_mult +
58   assumes distrib: "(a + b) * c = a * c + b * c"
59 begin
61 subclass semiring
62 proof
63   fix a b c :: 'a
64   show "(a + b) * c = a * c + b * c"
66   have "a * (b + c) = (b + c) * a"
68   also have "\<dots> = b * a + c * a"
69     by (simp only: distrib)
70   also have "\<dots> = a * b + a * c"
72   finally show "a * (b + c) = a * b + a * c"
73     by blast
74 qed
76 end
78 class comm_semiring_0 = comm_semiring + comm_monoid_add + mult_zero
79 begin
81 subclass semiring_0 ..
83 end
85 class comm_semiring_0_cancel = comm_semiring + cancel_comm_monoid_add
86 begin
88 subclass semiring_0_cancel ..
90 subclass comm_semiring_0 ..
92 end
94 class zero_neq_one = zero + one +
95   assumes zero_neq_one [simp]: "0 \<noteq> 1"
96 begin
98 lemma one_neq_zero [simp]: "1 \<noteq> 0"
99   by (rule not_sym) (rule zero_neq_one)
101 definition of_bool :: "bool \<Rightarrow> 'a"
102   where "of_bool p = (if p then 1 else 0)"
104 lemma of_bool_eq [simp, code]:
105   "of_bool False = 0"
106   "of_bool True = 1"
109 lemma of_bool_eq_iff: "of_bool p = of_bool q \<longleftrightarrow> p = q"
112 lemma split_of_bool [split]: "P (of_bool p) \<longleftrightarrow> (p \<longrightarrow> P 1) \<and> (\<not> p \<longrightarrow> P 0)"
113   by (cases p) simp_all
115 lemma split_of_bool_asm: "P (of_bool p) \<longleftrightarrow> \<not> (p \<and> \<not> P 1 \<or> \<not> p \<and> \<not> P 0)"
116   by (cases p) simp_all
118 end
120 class semiring_1 = zero_neq_one + semiring_0 + monoid_mult
121 begin
123 lemma (in semiring_1) of_bool_conj:
124   "of_bool (P \<and> Q) = of_bool P * of_bool Q"
125   by auto
127 end
129 text \<open>Abstract divisibility\<close>
131 class dvd = times
132 begin
134 definition dvd :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "dvd" 50)
135   where "b dvd a \<longleftrightarrow> (\<exists>k. a = b * k)"
137 lemma dvdI [intro?]: "a = b * k \<Longrightarrow> b dvd a"
138   unfolding dvd_def ..
140 lemma dvdE [elim?]: "b dvd a \<Longrightarrow> (\<And>k. a = b * k \<Longrightarrow> P) \<Longrightarrow> P"
141   unfolding dvd_def by blast
143 end
145 context comm_monoid_mult
146 begin
148 subclass dvd .
150 lemma dvd_refl [simp]: "a dvd a"
151 proof
152   show "a = a * 1" by simp
153 qed
155 lemma dvd_trans [trans]:
156   assumes "a dvd b" and "b dvd c"
157   shows "a dvd c"
158 proof -
159   from assms obtain v where "b = a * v"
160     by (auto elim!: dvdE)
161   moreover from assms obtain w where "c = b * w"
162     by (auto elim!: dvdE)
163   ultimately have "c = a * (v * w)"
165   then show ?thesis ..
166 qed
168 lemma subset_divisors_dvd: "{c. c dvd a} \<subseteq> {c. c dvd b} \<longleftrightarrow> a dvd b"
169   by (auto simp add: subset_iff intro: dvd_trans)
171 lemma strict_subset_divisors_dvd: "{c. c dvd a} \<subset> {c. c dvd b} \<longleftrightarrow> a dvd b \<and> \<not> b dvd a"
172   by (auto simp add: subset_iff intro: dvd_trans)
174 lemma one_dvd [simp]: "1 dvd a"
175   by (auto intro!: dvdI)
177 lemma dvd_mult [simp]: "a dvd c \<Longrightarrow> a dvd (b * c)"
178   by (auto intro!: mult.left_commute dvdI elim!: dvdE)
180 lemma dvd_mult2 [simp]: "a dvd b \<Longrightarrow> a dvd (b * c)"
181   using dvd_mult [of a b c] by (simp add: ac_simps)
183 lemma dvd_triv_right [simp]: "a dvd b * a"
184   by (rule dvd_mult) (rule dvd_refl)
186 lemma dvd_triv_left [simp]: "a dvd a * b"
187   by (rule dvd_mult2) (rule dvd_refl)
189 lemma mult_dvd_mono:
190   assumes "a dvd b"
191     and "c dvd d"
192   shows "a * c dvd b * d"
193 proof -
194   from \<open>a dvd b\<close> obtain b' where "b = a * b'" ..
195   moreover from \<open>c dvd d\<close> obtain d' where "d = c * d'" ..
196   ultimately have "b * d = (a * c) * (b' * d')"
198   then show ?thesis ..
199 qed
201 lemma dvd_mult_left: "a * b dvd c \<Longrightarrow> a dvd c"
202   by (simp add: dvd_def mult.assoc) blast
204 lemma dvd_mult_right: "a * b dvd c \<Longrightarrow> b dvd c"
205   using dvd_mult_left [of b a c] by (simp add: ac_simps)
207 end
209 class comm_semiring_1 = zero_neq_one + comm_semiring_0 + comm_monoid_mult
210 begin
212 subclass semiring_1 ..
214 lemma dvd_0_left_iff [simp]: "0 dvd a \<longleftrightarrow> a = 0"
215   by (auto intro: dvd_refl elim!: dvdE)
217 lemma dvd_0_right [iff]: "a dvd 0"
218 proof
219   show "0 = a * 0" by simp
220 qed
222 lemma dvd_0_left: "0 dvd a \<Longrightarrow> a = 0"
223   by simp
226   assumes "a dvd b" and "a dvd c"
227   shows "a dvd (b + c)"
228 proof -
229   from \<open>a dvd b\<close> obtain b' where "b = a * b'" ..
230   moreover from \<open>a dvd c\<close> obtain c' where "c = a * c'" ..
231   ultimately have "b + c = a * (b' + c')"
233   then show ?thesis ..
234 qed
236 end
238 class semiring_1_cancel = semiring + cancel_comm_monoid_add
239   + zero_neq_one + monoid_mult
240 begin
242 subclass semiring_0_cancel ..
244 subclass semiring_1 ..
246 end
248 class comm_semiring_1_cancel =
249   comm_semiring + cancel_comm_monoid_add + zero_neq_one + comm_monoid_mult +
250   assumes right_diff_distrib' [algebra_simps]: "a * (b - c) = a * b - a * c"
251 begin
253 subclass semiring_1_cancel ..
254 subclass comm_semiring_0_cancel ..
255 subclass comm_semiring_1 ..
257 lemma left_diff_distrib' [algebra_simps]: "(b - c) * a = b * a - c * a"
260 lemma dvd_add_times_triv_left_iff [simp]: "a dvd c * a + b \<longleftrightarrow> a dvd b"
261 proof -
262   have "a dvd a * c + b \<longleftrightarrow> a dvd b" (is "?P \<longleftrightarrow> ?Q")
263   proof
264     assume ?Q
265     then show ?P by simp
266   next
267     assume ?P
268     then obtain d where "a * c + b = a * d" ..
269     then have "a * c + b - a * c = a * d - a * c" by simp
270     then have "b = a * d - a * c" by simp
271     then have "b = a * (d - c)" by (simp add: algebra_simps)
272     then show ?Q ..
273   qed
274   then show "a dvd c * a + b \<longleftrightarrow> a dvd b" by (simp add: ac_simps)
275 qed
277 lemma dvd_add_times_triv_right_iff [simp]: "a dvd b + c * a \<longleftrightarrow> a dvd b"
280 lemma dvd_add_triv_left_iff [simp]: "a dvd a + b \<longleftrightarrow> a dvd b"
281   using dvd_add_times_triv_left_iff [of a 1 b] by simp
283 lemma dvd_add_triv_right_iff [simp]: "a dvd b + a \<longleftrightarrow> a dvd b"
284   using dvd_add_times_triv_right_iff [of a b 1] by simp
287   assumes "a dvd b"
288   shows "a dvd b + c \<longleftrightarrow> a dvd c" (is "?P \<longleftrightarrow> ?Q")
289 proof
290   assume ?P
291   then obtain d where "b + c = a * d" ..
292   moreover from \<open>a dvd b\<close> obtain e where "b = a * e" ..
293   ultimately have "a * e + c = a * d" by simp
294   then have "a * e + c - a * e = a * d - a * e" by simp
295   then have "c = a * d - a * e" by simp
296   then have "c = a * (d - e)" by (simp add: algebra_simps)
297   then show ?Q ..
298 next
299   assume ?Q
300   with assms show ?P by simp
301 qed
303 lemma dvd_add_left_iff: "a dvd c \<Longrightarrow> a dvd b + c \<longleftrightarrow> a dvd b"
306 end
308 class ring = semiring + ab_group_add
309 begin
311 subclass semiring_0_cancel ..
313 text \<open>Distribution rules\<close>
315 lemma minus_mult_left: "- (a * b) = - a * b"
316   by (rule minus_unique) (simp add: distrib_right [symmetric])
318 lemma minus_mult_right: "- (a * b) = a * - b"
319   by (rule minus_unique) (simp add: distrib_left [symmetric])
321 text \<open>Extract signs from products\<close>
322 lemmas mult_minus_left [simp] = minus_mult_left [symmetric]
323 lemmas mult_minus_right [simp] = minus_mult_right [symmetric]
325 lemma minus_mult_minus [simp]: "- a * - b = a * b"
326   by simp
328 lemma minus_mult_commute: "- a * b = a * - b"
329   by simp
331 lemma right_diff_distrib [algebra_simps]: "a * (b - c) = a * b - a * c"
332   using distrib_left [of a b "-c "] by simp
334 lemma left_diff_distrib [algebra_simps]: "(a - b) * c = a * c - b * c"
335   using distrib_right [of a "- b" c] by simp
337 lemmas ring_distribs = distrib_left distrib_right left_diff_distrib right_diff_distrib
339 lemma eq_add_iff1: "a * e + c = b * e + d \<longleftrightarrow> (a - b) * e + c = d"
342 lemma eq_add_iff2: "a * e + c = b * e + d \<longleftrightarrow> c = (b - a) * e + d"
345 end
347 lemmas ring_distribs = distrib_left distrib_right left_diff_distrib right_diff_distrib
349 class comm_ring = comm_semiring + ab_group_add
350 begin
352 subclass ring ..
353 subclass comm_semiring_0_cancel ..
355 lemma square_diff_square_factored: "x * x - y * y = (x + y) * (x - y)"
358 end
360 class ring_1 = ring + zero_neq_one + monoid_mult
361 begin
363 subclass semiring_1_cancel ..
365 lemma square_diff_one_factored: "x * x - 1 = (x + 1) * (x - 1)"
368 end
370 class comm_ring_1 = comm_ring + zero_neq_one + comm_monoid_mult
371 begin
373 subclass ring_1 ..
374 subclass comm_semiring_1_cancel
375   by unfold_locales (simp add: algebra_simps)
377 lemma dvd_minus_iff [simp]: "x dvd - y \<longleftrightarrow> x dvd y"
378 proof
379   assume "x dvd - y"
380   then have "x dvd - 1 * - y" by (rule dvd_mult)
381   then show "x dvd y" by simp
382 next
383   assume "x dvd y"
384   then have "x dvd - 1 * y" by (rule dvd_mult)
385   then show "x dvd - y" by simp
386 qed
388 lemma minus_dvd_iff [simp]: "- x dvd y \<longleftrightarrow> x dvd y"
389 proof
390   assume "- x dvd y"
391   then obtain k where "y = - x * k" ..
392   then have "y = x * - k" by simp
393   then show "x dvd y" ..
394 next
395   assume "x dvd y"
396   then obtain k where "y = x * k" ..
397   then have "y = - x * - k" by simp
398   then show "- x dvd y" ..
399 qed
401 lemma dvd_diff [simp]: "x dvd y \<Longrightarrow> x dvd z \<Longrightarrow> x dvd (y - z)"
402   using dvd_add [of x y "- z"] by simp
404 end
406 class semiring_no_zero_divisors = semiring_0 +
407   assumes no_zero_divisors: "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> a * b \<noteq> 0"
408 begin
410 lemma divisors_zero:
411   assumes "a * b = 0"
412   shows "a = 0 \<or> b = 0"
413 proof (rule classical)
414   assume "\<not> ?thesis"
415   then have "a \<noteq> 0" and "b \<noteq> 0" by auto
416   with no_zero_divisors have "a * b \<noteq> 0" by blast
417   with assms show ?thesis by simp
418 qed
420 lemma mult_eq_0_iff [simp]: "a * b = 0 \<longleftrightarrow> a = 0 \<or> b = 0"
421 proof (cases "a = 0 \<or> b = 0")
422   case False
423   then have "a \<noteq> 0" and "b \<noteq> 0" by auto
424     then show ?thesis using no_zero_divisors by simp
425 next
426   case True
427   then show ?thesis by auto
428 qed
430 end
432 class semiring_1_no_zero_divisors = semiring_1 + semiring_no_zero_divisors
434 class semiring_no_zero_divisors_cancel = semiring_no_zero_divisors +
435   assumes mult_cancel_right [simp]: "a * c = b * c \<longleftrightarrow> c = 0 \<or> a = b"
436     and mult_cancel_left [simp]: "c * a = c * b \<longleftrightarrow> c = 0 \<or> a = b"
437 begin
439 lemma mult_left_cancel: "c \<noteq> 0 \<Longrightarrow> c * a = c * b \<longleftrightarrow> a = b"
440   by simp
442 lemma mult_right_cancel: "c \<noteq> 0 \<Longrightarrow> a * c = b * c \<longleftrightarrow> a = b"
443   by simp
445 end
447 class ring_no_zero_divisors = ring + semiring_no_zero_divisors
448 begin
450 subclass semiring_no_zero_divisors_cancel
451 proof
452   fix a b c
453   have "a * c = b * c \<longleftrightarrow> (a - b) * c = 0"
455   also have "\<dots> \<longleftrightarrow> c = 0 \<or> a = b"
456     by auto
457   finally show "a * c = b * c \<longleftrightarrow> c = 0 \<or> a = b" .
458   have "c * a = c * b \<longleftrightarrow> c * (a - b) = 0"
460   also have "\<dots> \<longleftrightarrow> c = 0 \<or> a = b"
461     by auto
462   finally show "c * a = c * b \<longleftrightarrow> c = 0 \<or> a = b" .
463 qed
465 end
467 class ring_1_no_zero_divisors = ring_1 + ring_no_zero_divisors
468 begin
470 subclass semiring_1_no_zero_divisors ..
472 lemma square_eq_1_iff: "x * x = 1 \<longleftrightarrow> x = 1 \<or> x = - 1"
473 proof -
474   have "(x - 1) * (x + 1) = x * x - 1"
476   then have "x * x = 1 \<longleftrightarrow> (x - 1) * (x + 1) = 0"
477     by simp
478   then show ?thesis
480 qed
482 lemma mult_cancel_right1 [simp]: "c = b * c \<longleftrightarrow> c = 0 \<or> b = 1"
483   using mult_cancel_right [of 1 c b] by auto
485 lemma mult_cancel_right2 [simp]: "a * c = c \<longleftrightarrow> c = 0 \<or> a = 1"
486   using mult_cancel_right [of a c 1] by simp
488 lemma mult_cancel_left1 [simp]: "c = c * b \<longleftrightarrow> c = 0 \<or> b = 1"
489   using mult_cancel_left [of c 1 b] by force
491 lemma mult_cancel_left2 [simp]: "c * a = c \<longleftrightarrow> c = 0 \<or> a = 1"
492   using mult_cancel_left [of c a 1] by simp
494 end
496 class semidom = comm_semiring_1_cancel + semiring_no_zero_divisors
497 begin
499 subclass semiring_1_no_zero_divisors ..
501 end
503 class idom = comm_ring_1 + semiring_no_zero_divisors
504 begin
506 subclass semidom ..
508 subclass ring_1_no_zero_divisors ..
510 lemma dvd_mult_cancel_right [simp]: "a * c dvd b * c \<longleftrightarrow> c = 0 \<or> a dvd b"
511 proof -
512   have "a * c dvd b * c \<longleftrightarrow> (\<exists>k. b * c = (a * k) * c)"
513     unfolding dvd_def by (simp add: ac_simps)
514   also have "(\<exists>k. b * c = (a * k) * c) \<longleftrightarrow> c = 0 \<or> a dvd b"
515     unfolding dvd_def by simp
516   finally show ?thesis .
517 qed
519 lemma dvd_mult_cancel_left [simp]: "c * a dvd c * b \<longleftrightarrow> c = 0 \<or> a dvd b"
520 proof -
521   have "c * a dvd c * b \<longleftrightarrow> (\<exists>k. b * c = (a * k) * c)"
522     unfolding dvd_def by (simp add: ac_simps)
523   also have "(\<exists>k. b * c = (a * k) * c) \<longleftrightarrow> c = 0 \<or> a dvd b"
524     unfolding dvd_def by simp
525   finally show ?thesis .
526 qed
528 lemma square_eq_iff: "a * a = b * b \<longleftrightarrow> a = b \<or> a = - b"
529 proof
530   assume "a * a = b * b"
531   then have "(a - b) * (a + b) = 0"
533   then show "a = b \<or> a = - b"
535 next
536   assume "a = b \<or> a = - b"
537   then show "a * a = b * b" by auto
538 qed
540 end
542 class idom_abs_sgn = idom + abs + sgn +
543   assumes sgn_mult_abs: "sgn a * \<bar>a\<bar> = a"
544     and sgn_sgn [simp]: "sgn (sgn a) = sgn a"
545     and abs_abs [simp]: "\<bar>\<bar>a\<bar>\<bar> = \<bar>a\<bar>"
546     and abs_0 [simp]: "\<bar>0\<bar> = 0"
547     and sgn_0 [simp]: "sgn 0 = 0"
548     and sgn_1 [simp]: "sgn 1 = 1"
549     and sgn_minus_1: "sgn (- 1) = - 1"
550     and sgn_mult: "sgn (a * b) = sgn a * sgn b"
551 begin
553 lemma sgn_eq_0_iff:
554   "sgn a = 0 \<longleftrightarrow> a = 0"
555 proof -
556   { assume "sgn a = 0"
557     then have "sgn a * \<bar>a\<bar> = 0"
558       by simp
559     then have "a = 0"
561   } then show ?thesis
562     by auto
563 qed
565 lemma abs_eq_0_iff:
566   "\<bar>a\<bar> = 0 \<longleftrightarrow> a = 0"
567 proof -
568   { assume "\<bar>a\<bar> = 0"
569     then have "sgn a * \<bar>a\<bar> = 0"
570       by simp
571     then have "a = 0"
573   } then show ?thesis
574     by auto
575 qed
577 lemma abs_mult_sgn:
578   "\<bar>a\<bar> * sgn a = a"
579   using sgn_mult_abs [of a] by (simp add: ac_simps)
581 lemma abs_1 [simp]:
582   "\<bar>1\<bar> = 1"
583   using sgn_mult_abs [of 1] by simp
585 lemma sgn_abs [simp]:
586   "\<bar>sgn a\<bar> = of_bool (a \<noteq> 0)"
587   using sgn_mult_abs [of "sgn a"] mult_cancel_left [of "sgn a" "\<bar>sgn a\<bar>" 1]
588   by (auto simp add: sgn_eq_0_iff)
590 lemma abs_sgn [simp]:
591   "sgn \<bar>a\<bar> = of_bool (a \<noteq> 0)"
592   using sgn_mult_abs [of "\<bar>a\<bar>"] mult_cancel_right [of "sgn \<bar>a\<bar>" "\<bar>a\<bar>" 1]
593   by (auto simp add: abs_eq_0_iff)
595 lemma abs_mult:
596   "\<bar>a * b\<bar> = \<bar>a\<bar> * \<bar>b\<bar>"
597 proof (cases "a = 0 \<or> b = 0")
598   case True
599   then show ?thesis
600     by auto
601 next
602   case False
603   then have *: "sgn (a * b) \<noteq> 0"
605   from abs_mult_sgn [of "a * b"] abs_mult_sgn [of a] abs_mult_sgn [of b]
606   have "\<bar>a * b\<bar> * sgn (a * b) = \<bar>a\<bar> * sgn a * \<bar>b\<bar> * sgn b"
608   then have "\<bar>a * b\<bar> * sgn (a * b) = \<bar>a\<bar> * \<bar>b\<bar> * sgn (a * b)"
609     by (simp add: sgn_mult ac_simps)
610   with * show ?thesis
611     by simp
612 qed
614 lemma sgn_minus [simp]:
615   "sgn (- a) = - sgn a"
616 proof -
617   from sgn_minus_1 have "sgn (- 1 * a) = - 1 * sgn a"
618     by (simp only: sgn_mult)
619   then show ?thesis
620     by simp
621 qed
623 lemma abs_minus [simp]:
624   "\<bar>- a\<bar> = \<bar>a\<bar>"
625 proof -
626   have [simp]: "\<bar>- 1\<bar> = 1"
627     using sgn_mult_abs [of "- 1"] by simp
628   then have "\<bar>- 1 * a\<bar> = 1 * \<bar>a\<bar>"
629     by (simp only: abs_mult)
630   then show ?thesis
631     by simp
632 qed
634 end
636 text \<open>
637   The theory of partially ordered rings is taken from the books:
638     \<^item> \<^emph>\<open>Lattice Theory\<close> by Garret Birkhoff, American Mathematical Society, 1979
639     \<^item> \<^emph>\<open>Partially Ordered Algebraic Systems\<close>, Pergamon Press, 1963
641   Most of the used notions can also be looked up in
642     \<^item> \<^url>\<open>http://www.mathworld.com\<close> by Eric Weisstein et. al.
643     \<^item> \<^emph>\<open>Algebra I\<close> by van der Waerden, Springer
644 \<close>
646 text \<open>Syntactic division operator\<close>
648 class divide =
649   fixes divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "div" 70)
651 setup \<open>Sign.add_const_constraint (@{const_name "divide"}, SOME @{typ "'a \<Rightarrow> 'a \<Rightarrow> 'a"})\<close>
653 context semiring
654 begin
656 lemma [field_simps]:
657   shows distrib_left_NO_MATCH: "NO_MATCH (x div y) a \<Longrightarrow> a * (b + c) = a * b + a * c"
658     and distrib_right_NO_MATCH: "NO_MATCH (x div y) c \<Longrightarrow> (a + b) * c = a * c + b * c"
659   by (rule distrib_left distrib_right)+
661 end
663 context ring
664 begin
666 lemma [field_simps]:
667   shows left_diff_distrib_NO_MATCH: "NO_MATCH (x div y) c \<Longrightarrow> (a - b) * c = a * c - b * c"
668     and right_diff_distrib_NO_MATCH: "NO_MATCH (x div y) a \<Longrightarrow> a * (b - c) = a * b - a * c"
669   by (rule left_diff_distrib right_diff_distrib)+
671 end
673 setup \<open>Sign.add_const_constraint (@{const_name "divide"}, SOME @{typ "'a::divide \<Rightarrow> 'a \<Rightarrow> 'a"})\<close>
675 text \<open>Algebraic classes with division\<close>
677 class semidom_divide = semidom + divide +
678   assumes nonzero_mult_div_cancel_right [simp]: "b \<noteq> 0 \<Longrightarrow> (a * b) div b = a"
679   assumes div_by_0 [simp]: "a div 0 = 0"
680 begin
682 lemma nonzero_mult_div_cancel_left [simp]: "a \<noteq> 0 \<Longrightarrow> (a * b) div a = b"
683   using nonzero_mult_div_cancel_right [of a b] by (simp add: ac_simps)
685 subclass semiring_no_zero_divisors_cancel
686 proof
687   show *: "a * c = b * c \<longleftrightarrow> c = 0 \<or> a = b" for a b c
688   proof (cases "c = 0")
689     case True
690     then show ?thesis by simp
691   next
692     case False
693     have "a = b" if "a * c = b * c"
694     proof -
695       from that have "a * c div c = b * c div c"
696         by simp
697       with False show ?thesis
698         by simp
699     qed
700     then show ?thesis by auto
701   qed
702   show "c * a = c * b \<longleftrightarrow> c = 0 \<or> a = b" for a b c
703     using * [of a c b] by (simp add: ac_simps)
704 qed
706 lemma div_self [simp]: "a \<noteq> 0 \<Longrightarrow> a div a = 1"
707   using nonzero_mult_div_cancel_left [of a 1] by simp
709 lemma div_0 [simp]: "0 div a = 0"
710 proof (cases "a = 0")
711   case True
712   then show ?thesis by simp
713 next
714   case False
715   then have "a * 0 div a = 0"
716     by (rule nonzero_mult_div_cancel_left)
717   then show ?thesis by simp
718 qed
720 lemma div_by_1 [simp]: "a div 1 = a"
721   using nonzero_mult_div_cancel_left [of 1 a] by simp
723 lemma dvd_div_eq_0_iff:
724   assumes "b dvd a"
725   shows "a div b = 0 \<longleftrightarrow> a = 0"
726   using assms by (elim dvdE, cases "b = 0") simp_all
728 lemma dvd_div_eq_cancel:
729   "a div c = b div c \<Longrightarrow> c dvd a \<Longrightarrow> c dvd b \<Longrightarrow> a = b"
730   by (elim dvdE, cases "c = 0") simp_all
732 lemma dvd_div_eq_iff:
733   "c dvd a \<Longrightarrow> c dvd b \<Longrightarrow> a div c = b div c \<longleftrightarrow> a = b"
734   by (elim dvdE, cases "c = 0") simp_all
736 end
738 class idom_divide = idom + semidom_divide
739 begin
741 lemma dvd_neg_div:
742   assumes "b dvd a"
743   shows "- a div b = - (a div b)"
744 proof (cases "b = 0")
745   case True
746   then show ?thesis by simp
747 next
748   case False
749   from assms obtain c where "a = b * c" ..
750   then have "- a div b = (b * - c) div b"
751     by simp
752   from False also have "\<dots> = - c"
753     by (rule nonzero_mult_div_cancel_left)
754   with False \<open>a = b * c\<close> show ?thesis
755     by simp
756 qed
758 lemma dvd_div_neg:
759   assumes "b dvd a"
760   shows "a div - b = - (a div b)"
761 proof (cases "b = 0")
762   case True
763   then show ?thesis by simp
764 next
765   case False
766   then have "- b \<noteq> 0"
767     by simp
768   from assms obtain c where "a = b * c" ..
769   then have "a div - b = (- b * - c) div - b"
770     by simp
771   from \<open>- b \<noteq> 0\<close> also have "\<dots> = - c"
772     by (rule nonzero_mult_div_cancel_left)
773   with False \<open>a = b * c\<close> show ?thesis
774     by simp
775 qed
777 end
779 class algebraic_semidom = semidom_divide
780 begin
782 text \<open>
783   Class @{class algebraic_semidom} enriches a integral domain
784   by notions from algebra, like units in a ring.
785   It is a separate class to avoid spoiling fields with notions
786   which are degenerated there.
787 \<close>
789 lemma dvd_times_left_cancel_iff [simp]:
790   assumes "a \<noteq> 0"
791   shows "a * b dvd a * c \<longleftrightarrow> b dvd c"
792     (is "?lhs \<longleftrightarrow> ?rhs")
793 proof
794   assume ?lhs
795   then obtain d where "a * c = a * b * d" ..
796   with assms have "c = b * d" by (simp add: ac_simps)
797   then show ?rhs ..
798 next
799   assume ?rhs
800   then obtain d where "c = b * d" ..
801   then have "a * c = a * b * d" by (simp add: ac_simps)
802   then show ?lhs ..
803 qed
805 lemma dvd_times_right_cancel_iff [simp]:
806   assumes "a \<noteq> 0"
807   shows "b * a dvd c * a \<longleftrightarrow> b dvd c"
808   using dvd_times_left_cancel_iff [of a b c] assms by (simp add: ac_simps)
810 lemma div_dvd_iff_mult:
811   assumes "b \<noteq> 0" and "b dvd a"
812   shows "a div b dvd c \<longleftrightarrow> a dvd c * b"
813 proof -
814   from \<open>b dvd a\<close> obtain d where "a = b * d" ..
815   with \<open>b \<noteq> 0\<close> show ?thesis by (simp add: ac_simps)
816 qed
818 lemma dvd_div_iff_mult:
819   assumes "c \<noteq> 0" and "c dvd b"
820   shows "a dvd b div c \<longleftrightarrow> a * c dvd b"
821 proof -
822   from \<open>c dvd b\<close> obtain d where "b = c * d" ..
823   with \<open>c \<noteq> 0\<close> show ?thesis by (simp add: mult.commute [of a])
824 qed
826 lemma div_dvd_div [simp]:
827   assumes "a dvd b" and "a dvd c"
828   shows "b div a dvd c div a \<longleftrightarrow> b dvd c"
829 proof (cases "a = 0")
830   case True
831   with assms show ?thesis by simp
832 next
833   case False
834   moreover from assms obtain k l where "b = a * k" and "c = a * l"
835     by (auto elim!: dvdE)
836   ultimately show ?thesis by simp
837 qed
840   assumes "c dvd a" and "c dvd b"
841   shows "(a + b) div c = a div c + b div c"
842 proof (cases "c = 0")
843   case True
844   then show ?thesis by simp
845 next
846   case False
847   moreover from assms obtain k l where "a = c * k" and "b = c * l"
848     by (auto elim!: dvdE)
849   moreover have "c * k + c * l = c * (k + l)"
851   ultimately show ?thesis
852     by simp
853 qed
855 lemma div_mult_div_if_dvd:
856   assumes "b dvd a" and "d dvd c"
857   shows "(a div b) * (c div d) = (a * c) div (b * d)"
858 proof (cases "b = 0 \<or> c = 0")
859   case True
860   with assms show ?thesis by auto
861 next
862   case False
863   moreover from assms obtain k l where "a = b * k" and "c = d * l"
864     by (auto elim!: dvdE)
865   moreover have "b * k * (d * l) div (b * d) = (b * d) * (k * l) div (b * d)"
867   ultimately show ?thesis by simp
868 qed
870 lemma dvd_div_eq_mult:
871   assumes "a \<noteq> 0" and "a dvd b"
872   shows "b div a = c \<longleftrightarrow> b = c * a"
873     (is "?lhs \<longleftrightarrow> ?rhs")
874 proof
875   assume ?rhs
876   then show ?lhs by (simp add: assms)
877 next
878   assume ?lhs
879   then have "b div a * a = c * a" by simp
880   moreover from assms have "b div a * a = b"
881     by (auto elim!: dvdE simp add: ac_simps)
882   ultimately show ?rhs by simp
883 qed
885 lemma dvd_div_mult_self [simp]: "a dvd b \<Longrightarrow> b div a * a = b"
886   by (cases "a = 0") (auto elim: dvdE simp add: ac_simps)
888 lemma dvd_mult_div_cancel [simp]: "a dvd b \<Longrightarrow> a * (b div a) = b"
889   using dvd_div_mult_self [of a b] by (simp add: ac_simps)
891 lemma div_mult_swap:
892   assumes "c dvd b"
893   shows "a * (b div c) = (a * b) div c"
894 proof (cases "c = 0")
895   case True
896   then show ?thesis by simp
897 next
898   case False
899   from assms obtain d where "b = c * d" ..
900   moreover from False have "a * divide (d * c) c = ((a * d) * c) div c"
901     by simp
902   ultimately show ?thesis by (simp add: ac_simps)
903 qed
905 lemma dvd_div_mult: "c dvd b \<Longrightarrow> b div c * a = (b * a) div c"
906   using div_mult_swap [of c b a] by (simp add: ac_simps)
908 lemma dvd_div_mult2_eq:
909   assumes "b * c dvd a"
910   shows "a div (b * c) = a div b div c"
911 proof -
912   from assms obtain k where "a = b * c * k" ..
913   then show ?thesis
914     by (cases "b = 0 \<or> c = 0") (auto, simp add: ac_simps)
915 qed
917 lemma dvd_div_div_eq_mult:
918   assumes "a \<noteq> 0" "c \<noteq> 0" and "a dvd b" "c dvd d"
919   shows "b div a = d div c \<longleftrightarrow> b * c = a * d"
920     (is "?lhs \<longleftrightarrow> ?rhs")
921 proof -
922   from assms have "a * c \<noteq> 0" by simp
923   then have "?lhs \<longleftrightarrow> b div a * (a * c) = d div c * (a * c)"
924     by simp
925   also have "\<dots> \<longleftrightarrow> (a * (b div a)) * c = (c * (d div c)) * a"
927   also have "\<dots> \<longleftrightarrow> (a * b div a) * c = (c * d div c) * a"
928     using assms by (simp add: div_mult_swap)
929   also have "\<dots> \<longleftrightarrow> ?rhs"
930     using assms by (simp add: ac_simps)
931   finally show ?thesis .
932 qed
934 lemma dvd_mult_imp_div:
935   assumes "a * c dvd b"
936   shows "a dvd b div c"
937 proof (cases "c = 0")
938   case True then show ?thesis by simp
939 next
940   case False
941   from \<open>a * c dvd b\<close> obtain d where "b = a * c * d" ..
942   with False show ?thesis
943     by (simp add: mult.commute [of a] mult.assoc)
944 qed
946 lemma div_div_eq_right:
947   assumes "c dvd b" "b dvd a"
948   shows   "a div (b div c) = a div b * c"
949 proof (cases "c = 0 \<or> b = 0")
950   case True
951   then show ?thesis
952     by auto
953 next
954   case False
955   from assms obtain r s where "b = c * r" and "a = c * r * s"
956     by (blast elim: dvdE)
957   moreover with False have "r \<noteq> 0"
958     by auto
959   ultimately show ?thesis using False
960     by simp (simp add: mult.commute [of _ r] mult.assoc mult.commute [of c])
961 qed
963 lemma div_div_div_same:
964   assumes "d dvd b" "b dvd a"
965   shows   "(a div d) div (b div d) = a div b"
966 proof (cases "b = 0 \<or> d = 0")
967   case True
968   with assms show ?thesis
969     by auto
970 next
971   case False
972   from assms obtain r s
973     where "a = d * r * s" and "b = d * r"
974     by (blast elim: dvdE)
975   with False show ?thesis
976     by simp (simp add: ac_simps)
977 qed
980 text \<open>Units: invertible elements in a ring\<close>
982 abbreviation is_unit :: "'a \<Rightarrow> bool"
983   where "is_unit a \<equiv> a dvd 1"
985 lemma not_is_unit_0 [simp]: "\<not> is_unit 0"
986   by simp
988 lemma unit_imp_dvd [dest]: "is_unit b \<Longrightarrow> b dvd a"
989   by (rule dvd_trans [of _ 1]) simp_all
991 lemma unit_dvdE:
992   assumes "is_unit a"
993   obtains c where "a \<noteq> 0" and "b = a * c"
994 proof -
995   from assms have "a dvd b" by auto
996   then obtain c where "b = a * c" ..
997   moreover from assms have "a \<noteq> 0" by auto
998   ultimately show thesis using that by blast
999 qed
1001 lemma dvd_unit_imp_unit: "a dvd b \<Longrightarrow> is_unit b \<Longrightarrow> is_unit a"
1002   by (rule dvd_trans)
1004 lemma unit_div_1_unit [simp, intro]:
1005   assumes "is_unit a"
1006   shows "is_unit (1 div a)"
1007 proof -
1008   from assms have "1 = 1 div a * a" by simp
1009   then show "is_unit (1 div a)" by (rule dvdI)
1010 qed
1012 lemma is_unitE [elim?]:
1013   assumes "is_unit a"
1014   obtains b where "a \<noteq> 0" and "b \<noteq> 0"
1015     and "is_unit b" and "1 div a = b" and "1 div b = a"
1016     and "a * b = 1" and "c div a = c * b"
1017 proof (rule that)
1018   define b where "b = 1 div a"
1019   then show "1 div a = b" by simp
1020   from assms b_def show "is_unit b" by simp
1021   with assms show "a \<noteq> 0" and "b \<noteq> 0" by auto
1022   from assms b_def show "a * b = 1" by simp
1023   then have "1 = a * b" ..
1024   with b_def \<open>b \<noteq> 0\<close> show "1 div b = a" by simp
1025   from assms have "a dvd c" ..
1026   then obtain d where "c = a * d" ..
1027   with \<open>a \<noteq> 0\<close> \<open>a * b = 1\<close> show "c div a = c * b"
1028     by (simp add: mult.assoc mult.left_commute [of a])
1029 qed
1031 lemma unit_prod [intro]: "is_unit a \<Longrightarrow> is_unit b \<Longrightarrow> is_unit (a * b)"
1032   by (subst mult_1_left [of 1, symmetric]) (rule mult_dvd_mono)
1034 lemma is_unit_mult_iff: "is_unit (a * b) \<longleftrightarrow> is_unit a \<and> is_unit b"
1035   by (auto dest: dvd_mult_left dvd_mult_right)
1037 lemma unit_div [intro]: "is_unit a \<Longrightarrow> is_unit b \<Longrightarrow> is_unit (a div b)"
1038   by (erule is_unitE [of b a]) (simp add: ac_simps unit_prod)
1040 lemma mult_unit_dvd_iff:
1041   assumes "is_unit b"
1042   shows "a * b dvd c \<longleftrightarrow> a dvd c"
1043 proof
1044   assume "a * b dvd c"
1045   with assms show "a dvd c"
1047 next
1048   assume "a dvd c"
1049   then obtain k where "c = a * k" ..
1050   with assms have "c = (a * b) * (1 div b * k)"
1052   then show "a * b dvd c" by (rule dvdI)
1053 qed
1055 lemma mult_unit_dvd_iff': "is_unit a \<Longrightarrow> (a * b) dvd c \<longleftrightarrow> b dvd c"
1056   using mult_unit_dvd_iff [of a b c] by (simp add: ac_simps)
1058 lemma dvd_mult_unit_iff:
1059   assumes "is_unit b"
1060   shows "a dvd c * b \<longleftrightarrow> a dvd c"
1061 proof
1062   assume "a dvd c * b"
1063   with assms have "c * b dvd c * (b * (1 div b))"
1064     by (subst mult_assoc [symmetric]) simp
1065   also from assms have "b * (1 div b) = 1"
1066     by (rule is_unitE) simp
1067   finally have "c * b dvd c" by simp
1068   with \<open>a dvd c * b\<close> show "a dvd c" by (rule dvd_trans)
1069 next
1070   assume "a dvd c"
1071   then show "a dvd c * b" by simp
1072 qed
1074 lemma dvd_mult_unit_iff': "is_unit b \<Longrightarrow> a dvd b * c \<longleftrightarrow> a dvd c"
1075   using dvd_mult_unit_iff [of b a c] by (simp add: ac_simps)
1077 lemma div_unit_dvd_iff: "is_unit b \<Longrightarrow> a div b dvd c \<longleftrightarrow> a dvd c"
1078   by (erule is_unitE [of _ a]) (auto simp add: mult_unit_dvd_iff)
1080 lemma dvd_div_unit_iff: "is_unit b \<Longrightarrow> a dvd c div b \<longleftrightarrow> a dvd c"
1081   by (erule is_unitE [of _ c]) (simp add: dvd_mult_unit_iff)
1083 lemmas unit_dvd_iff = mult_unit_dvd_iff mult_unit_dvd_iff'
1084   dvd_mult_unit_iff dvd_mult_unit_iff'
1085   div_unit_dvd_iff dvd_div_unit_iff (* FIXME consider named_theorems *)
1087 lemma unit_mult_div_div [simp]: "is_unit a \<Longrightarrow> b * (1 div a) = b div a"
1088   by (erule is_unitE [of _ b]) simp
1090 lemma unit_div_mult_self [simp]: "is_unit a \<Longrightarrow> b div a * a = b"
1091   by (rule dvd_div_mult_self) auto
1093 lemma unit_div_1_div_1 [simp]: "is_unit a \<Longrightarrow> 1 div (1 div a) = a"
1094   by (erule is_unitE) simp
1096 lemma unit_div_mult_swap: "is_unit c \<Longrightarrow> a * (b div c) = (a * b) div c"
1097   by (erule unit_dvdE [of _ b]) (simp add: mult.left_commute [of _ c])
1099 lemma unit_div_commute: "is_unit b \<Longrightarrow> (a div b) * c = (a * c) div b"
1100   using unit_div_mult_swap [of b c a] by (simp add: ac_simps)
1102 lemma unit_eq_div1: "is_unit b \<Longrightarrow> a div b = c \<longleftrightarrow> a = c * b"
1103   by (auto elim: is_unitE)
1105 lemma unit_eq_div2: "is_unit b \<Longrightarrow> a = c div b \<longleftrightarrow> a * b = c"
1106   using unit_eq_div1 [of b c a] by auto
1108 lemma unit_mult_left_cancel: "is_unit a \<Longrightarrow> a * b = a * c \<longleftrightarrow> b = c"
1109   using mult_cancel_left [of a b c] by auto
1111 lemma unit_mult_right_cancel: "is_unit a \<Longrightarrow> b * a = c * a \<longleftrightarrow> b = c"
1112   using unit_mult_left_cancel [of a b c] by (auto simp add: ac_simps)
1114 lemma unit_div_cancel:
1115   assumes "is_unit a"
1116   shows "b div a = c div a \<longleftrightarrow> b = c"
1117 proof -
1118   from assms have "is_unit (1 div a)" by simp
1119   then have "b * (1 div a) = c * (1 div a) \<longleftrightarrow> b = c"
1120     by (rule unit_mult_right_cancel)
1121   with assms show ?thesis by simp
1122 qed
1124 lemma is_unit_div_mult2_eq:
1125   assumes "is_unit b" and "is_unit c"
1126   shows "a div (b * c) = a div b div c"
1127 proof -
1128   from assms have "is_unit (b * c)"
1130   then have "b * c dvd a"
1131     by (rule unit_imp_dvd)
1132   then show ?thesis
1133     by (rule dvd_div_mult2_eq)
1134 qed
1136 lemmas unit_simps = mult_unit_dvd_iff div_unit_dvd_iff dvd_mult_unit_iff
1137   dvd_div_unit_iff unit_div_mult_swap unit_div_commute
1138   unit_mult_left_cancel unit_mult_right_cancel unit_div_cancel
1139   unit_eq_div1 unit_eq_div2
1141 lemma is_unit_div_mult_cancel_left:
1142   assumes "a \<noteq> 0" and "is_unit b"
1143   shows "a div (a * b) = 1 div b"
1144 proof -
1145   from assms have "a div (a * b) = a div a div b"
1146     by (simp add: mult_unit_dvd_iff dvd_div_mult2_eq)
1147   with assms show ?thesis by simp
1148 qed
1150 lemma is_unit_div_mult_cancel_right:
1151   assumes "a \<noteq> 0" and "is_unit b"
1152   shows "a div (b * a) = 1 div b"
1153   using assms is_unit_div_mult_cancel_left [of a b] by (simp add: ac_simps)
1155 lemma unit_div_eq_0_iff:
1156   assumes "is_unit b"
1157   shows "a div b = 0 \<longleftrightarrow> a = 0"
1158   by (rule dvd_div_eq_0_iff) (insert assms, auto)
1160 lemma div_mult_unit2:
1161   "is_unit c \<Longrightarrow> b dvd a \<Longrightarrow> a div (b * c) = a div b div c"
1162   by (rule dvd_div_mult2_eq) (simp_all add: mult_unit_dvd_iff)
1164 end
1166 class unit_factor =
1167   fixes unit_factor :: "'a \<Rightarrow> 'a"
1169 class semidom_divide_unit_factor = semidom_divide + unit_factor +
1170   assumes unit_factor_0 [simp]: "unit_factor 0 = 0"
1171     and is_unit_unit_factor: "a dvd 1 \<Longrightarrow> unit_factor a = a"
1172     and unit_factor_is_unit: "a \<noteq> 0 \<Longrightarrow> unit_factor a dvd 1"
1173     and unit_factor_mult: "unit_factor (a * b) = unit_factor a * unit_factor b"
1174   -- \<open>This fine-grained hierarchy will later on allow lean normalization of polynomials\<close>
1176 class normalization_semidom = algebraic_semidom + semidom_divide_unit_factor +
1177   fixes normalize :: "'a \<Rightarrow> 'a"
1178   assumes unit_factor_mult_normalize [simp]: "unit_factor a * normalize a = a"
1179     and normalize_0 [simp]: "normalize 0 = 0"
1180 begin
1182 text \<open>
1183   Class @{class normalization_semidom} cultivates the idea that each integral
1184   domain can be split into equivalence classes whose representants are
1185   associated, i.e. divide each other. @{const normalize} specifies a canonical
1186   representant for each equivalence class. The rationale behind this is that
1187   it is easier to reason about equality than equivalences, hence we prefer to
1188   think about equality of normalized values rather than associated elements.
1189 \<close>
1191 declare unit_factor_is_unit [iff]
1193 lemma unit_factor_dvd [simp]: "a \<noteq> 0 \<Longrightarrow> unit_factor a dvd b"
1194   by (rule unit_imp_dvd) simp
1196 lemma unit_factor_self [simp]: "unit_factor a dvd a"
1197   by (cases "a = 0") simp_all
1199 lemma normalize_mult_unit_factor [simp]: "normalize a * unit_factor a = a"
1200   using unit_factor_mult_normalize [of a] by (simp add: ac_simps)
1202 lemma normalize_eq_0_iff [simp]: "normalize a = 0 \<longleftrightarrow> a = 0"
1203   (is "?lhs \<longleftrightarrow> ?rhs")
1204 proof
1205   assume ?lhs
1206   moreover have "unit_factor a * normalize a = a" by simp
1207   ultimately show ?rhs by simp
1208 next
1209   assume ?rhs
1210   then show ?lhs by simp
1211 qed
1213 lemma unit_factor_eq_0_iff [simp]: "unit_factor a = 0 \<longleftrightarrow> a = 0"
1214   (is "?lhs \<longleftrightarrow> ?rhs")
1215 proof
1216   assume ?lhs
1217   moreover have "unit_factor a * normalize a = a" by simp
1218   ultimately show ?rhs by simp
1219 next
1220   assume ?rhs
1221   then show ?lhs by simp
1222 qed
1224 lemma div_unit_factor [simp]: "a div unit_factor a = normalize a"
1225 proof (cases "a = 0")
1226   case True
1227   then show ?thesis by simp
1228 next
1229   case False
1230   then have "unit_factor a \<noteq> 0"
1231     by simp
1232   with nonzero_mult_div_cancel_left
1233   have "unit_factor a * normalize a div unit_factor a = normalize a"
1234     by blast
1235   then show ?thesis by simp
1236 qed
1238 lemma normalize_div [simp]: "normalize a div a = 1 div unit_factor a"
1239 proof (cases "a = 0")
1240   case True
1241   then show ?thesis by simp
1242 next
1243   case False
1244   have "normalize a div a = normalize a div (unit_factor a * normalize a)"
1245     by simp
1246   also have "\<dots> = 1 div unit_factor a"
1247     using False by (subst is_unit_div_mult_cancel_right) simp_all
1248   finally show ?thesis .
1249 qed
1251 lemma is_unit_normalize:
1252   assumes "is_unit a"
1253   shows "normalize a = 1"
1254 proof -
1255   from assms have "unit_factor a = a"
1256     by (rule is_unit_unit_factor)
1257   moreover from assms have "a \<noteq> 0"
1258     by auto
1259   moreover have "normalize a = a div unit_factor a"
1260     by simp
1261   ultimately show ?thesis
1262     by simp
1263 qed
1265 lemma unit_factor_1 [simp]: "unit_factor 1 = 1"
1266   by (rule is_unit_unit_factor) simp
1268 lemma normalize_1 [simp]: "normalize 1 = 1"
1269   by (rule is_unit_normalize) simp
1271 lemma normalize_1_iff: "normalize a = 1 \<longleftrightarrow> is_unit a"
1272   (is "?lhs \<longleftrightarrow> ?rhs")
1273 proof
1274   assume ?rhs
1275   then show ?lhs by (rule is_unit_normalize)
1276 next
1277   assume ?lhs
1278   then have "unit_factor a * normalize a = unit_factor a * 1"
1279     by simp
1280   then have "unit_factor a = a"
1281     by simp
1282   moreover
1283   from \<open>?lhs\<close> have "a \<noteq> 0" by auto
1284   then have "is_unit (unit_factor a)" by simp
1285   ultimately show ?rhs by simp
1286 qed
1288 lemma div_normalize [simp]: "a div normalize a = unit_factor a"
1289 proof (cases "a = 0")
1290   case True
1291   then show ?thesis by simp
1292 next
1293   case False
1294   then have "normalize a \<noteq> 0" by simp
1295   with nonzero_mult_div_cancel_right
1296   have "unit_factor a * normalize a div normalize a = unit_factor a" by blast
1297   then show ?thesis by simp
1298 qed
1300 lemma mult_one_div_unit_factor [simp]: "a * (1 div unit_factor b) = a div unit_factor b"
1301   by (cases "b = 0") simp_all
1303 lemma inv_unit_factor_eq_0_iff [simp]:
1304   "1 div unit_factor a = 0 \<longleftrightarrow> a = 0"
1305   (is "?lhs \<longleftrightarrow> ?rhs")
1306 proof
1307   assume ?lhs
1308   then have "a * (1 div unit_factor a) = a * 0"
1309     by simp
1310   then show ?rhs
1311     by simp
1312 next
1313   assume ?rhs
1314   then show ?lhs by simp
1315 qed
1317 lemma normalize_mult: "normalize (a * b) = normalize a * normalize b"
1318 proof (cases "a = 0 \<or> b = 0")
1319   case True
1320   then show ?thesis by auto
1321 next
1322   case False
1323   have "unit_factor (a * b) * normalize (a * b) = a * b"
1324     by (rule unit_factor_mult_normalize)
1325   then have "normalize (a * b) = a * b div unit_factor (a * b)"
1326     by simp
1327   also have "\<dots> = a * b div unit_factor (b * a)"
1329   also have "\<dots> = a * b div unit_factor b div unit_factor a"
1330     using False by (simp add: unit_factor_mult is_unit_div_mult2_eq [symmetric])
1331   also have "\<dots> = a * (b div unit_factor b) div unit_factor a"
1332     using False by (subst unit_div_mult_swap) simp_all
1333   also have "\<dots> = normalize a * normalize b"
1334     using False
1335     by (simp add: mult.commute [of a] mult.commute [of "normalize a"] unit_div_mult_swap [symmetric])
1336   finally show ?thesis .
1337 qed
1339 lemma unit_factor_idem [simp]: "unit_factor (unit_factor a) = unit_factor a"
1340   by (cases "a = 0") (auto intro: is_unit_unit_factor)
1342 lemma normalize_unit_factor [simp]: "a \<noteq> 0 \<Longrightarrow> normalize (unit_factor a) = 1"
1343   by (rule is_unit_normalize) simp
1345 lemma normalize_idem [simp]: "normalize (normalize a) = normalize a"
1346 proof (cases "a = 0")
1347   case True
1348   then show ?thesis by simp
1349 next
1350   case False
1351   have "normalize a = normalize (unit_factor a * normalize a)"
1352     by simp
1353   also have "\<dots> = normalize (unit_factor a) * normalize (normalize a)"
1354     by (simp only: normalize_mult)
1355   finally show ?thesis
1356     using False by simp_all
1357 qed
1359 lemma unit_factor_normalize [simp]:
1360   assumes "a \<noteq> 0"
1361   shows "unit_factor (normalize a) = 1"
1362 proof -
1363   from assms have *: "normalize a \<noteq> 0"
1364     by simp
1365   have "unit_factor (normalize a) * normalize (normalize a) = normalize a"
1366     by (simp only: unit_factor_mult_normalize)
1367   then have "unit_factor (normalize a) * normalize a = normalize a"
1368     by simp
1369   with * have "unit_factor (normalize a) * normalize a div normalize a = normalize a div normalize a"
1370     by simp
1371   with * show ?thesis
1372     by simp
1373 qed
1375 lemma dvd_unit_factor_div:
1376   assumes "b dvd a"
1377   shows "unit_factor (a div b) = unit_factor a div unit_factor b"
1378 proof -
1379   from assms have "a = a div b * b"
1380     by simp
1381   then have "unit_factor a = unit_factor (a div b * b)"
1382     by simp
1383   then show ?thesis
1384     by (cases "b = 0") (simp_all add: unit_factor_mult)
1385 qed
1387 lemma dvd_normalize_div:
1388   assumes "b dvd a"
1389   shows "normalize (a div b) = normalize a div normalize b"
1390 proof -
1391   from assms have "a = a div b * b"
1392     by simp
1393   then have "normalize a = normalize (a div b * b)"
1394     by simp
1395   then show ?thesis
1396     by (cases "b = 0") (simp_all add: normalize_mult)
1397 qed
1399 lemma normalize_dvd_iff [simp]: "normalize a dvd b \<longleftrightarrow> a dvd b"
1400 proof -
1401   have "normalize a dvd b \<longleftrightarrow> unit_factor a * normalize a dvd b"
1402     using mult_unit_dvd_iff [of "unit_factor a" "normalize a" b]
1403       by (cases "a = 0") simp_all
1404   then show ?thesis by simp
1405 qed
1407 lemma dvd_normalize_iff [simp]: "a dvd normalize b \<longleftrightarrow> a dvd b"
1408 proof -
1409   have "a dvd normalize  b \<longleftrightarrow> a dvd normalize b * unit_factor b"
1410     using dvd_mult_unit_iff [of "unit_factor b" a "normalize b"]
1411       by (cases "b = 0") simp_all
1412   then show ?thesis by simp
1413 qed
1415 lemma normalize_idem_imp_unit_factor_eq:
1416   assumes "normalize a = a"
1417   shows "unit_factor a = of_bool (a \<noteq> 0)"
1418 proof (cases "a = 0")
1419   case True
1420   then show ?thesis
1421     by simp
1422 next
1423   case False
1424   then show ?thesis
1425     using assms unit_factor_normalize [of a] by simp
1426 qed
1428 lemma normalize_idem_imp_is_unit_iff:
1429   assumes "normalize a = a"
1430   shows "is_unit a \<longleftrightarrow> a = 1"
1431   using assms by (cases "a = 0") (auto dest: is_unit_normalize)
1433 text \<open>
1434   We avoid an explicit definition of associated elements but prefer explicit
1435   normalisation instead. In theory we could define an abbreviation like @{prop
1436   "associated a b \<longleftrightarrow> normalize a = normalize b"} but this is counterproductive
1437   without suggestive infix syntax, which we do not want to sacrifice for this
1438   purpose here.
1439 \<close>
1441 lemma associatedI:
1442   assumes "a dvd b" and "b dvd a"
1443   shows "normalize a = normalize b"
1444 proof (cases "a = 0 \<or> b = 0")
1445   case True
1446   with assms show ?thesis by auto
1447 next
1448   case False
1449   from \<open>a dvd b\<close> obtain c where b: "b = a * c" ..
1450   moreover from \<open>b dvd a\<close> obtain d where a: "a = b * d" ..
1451   ultimately have "b * 1 = b * (c * d)"
1453   with False have "1 = c * d"
1454     unfolding mult_cancel_left by simp
1455   then have "is_unit c" and "is_unit d"
1456     by auto
1457   with a b show ?thesis
1458     by (simp add: normalize_mult is_unit_normalize)
1459 qed
1461 lemma associatedD1: "normalize a = normalize b \<Longrightarrow> a dvd b"
1462   using dvd_normalize_iff [of _ b, symmetric] normalize_dvd_iff [of a _, symmetric]
1463   by simp
1465 lemma associatedD2: "normalize a = normalize b \<Longrightarrow> b dvd a"
1466   using dvd_normalize_iff [of _ a, symmetric] normalize_dvd_iff [of b _, symmetric]
1467   by simp
1469 lemma associated_unit: "normalize a = normalize b \<Longrightarrow> is_unit a \<Longrightarrow> is_unit b"
1470   using dvd_unit_imp_unit by (auto dest!: associatedD1 associatedD2)
1472 lemma associated_iff_dvd: "normalize a = normalize b \<longleftrightarrow> a dvd b \<and> b dvd a"
1473   (is "?lhs \<longleftrightarrow> ?rhs")
1474 proof
1475   assume ?rhs
1476   then show ?lhs by (auto intro!: associatedI)
1477 next
1478   assume ?lhs
1479   then have "unit_factor a * normalize a = unit_factor a * normalize b"
1480     by simp
1481   then have *: "normalize b * unit_factor a = a"
1483   show ?rhs
1484   proof (cases "a = 0 \<or> b = 0")
1485     case True
1486     with \<open>?lhs\<close> show ?thesis by auto
1487   next
1488     case False
1489     then have "b dvd normalize b * unit_factor a" and "normalize b * unit_factor a dvd b"
1490       by (simp_all add: mult_unit_dvd_iff dvd_mult_unit_iff)
1491     with * show ?thesis by simp
1492   qed
1493 qed
1495 lemma associated_eqI:
1496   assumes "a dvd b" and "b dvd a"
1497   assumes "normalize a = a" and "normalize b = b"
1498   shows "a = b"
1499 proof -
1500   from assms have "normalize a = normalize b"
1501     unfolding associated_iff_dvd by simp
1502   with \<open>normalize a = a\<close> have "a = normalize b"
1503     by simp
1504   with \<open>normalize b = b\<close> show "a = b"
1505     by simp
1506 qed
1508 lemma normalize_unit_factor_eqI:
1509   assumes "normalize a = normalize b"
1510     and "unit_factor a = unit_factor b"
1511   shows "a = b"
1512 proof -
1513   from assms have "unit_factor a * normalize a = unit_factor b * normalize b"
1514     by simp
1515   then show ?thesis
1516     by simp
1517 qed
1519 end
1522 text \<open>Syntactic division remainder operator\<close>
1524 class modulo = dvd + divide +
1525   fixes modulo :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "mod" 70)
1527 text \<open>Arbitrary quotient and remainder partitions\<close>
1529 class semiring_modulo = comm_semiring_1_cancel + divide + modulo +
1530   assumes div_mult_mod_eq: "a div b * b + a mod b = a"
1531 begin
1533 lemma mod_div_decomp:
1534   fixes a b
1535   obtains q r where "q = a div b" and "r = a mod b"
1536     and "a = q * b + r"
1537 proof -
1538   from div_mult_mod_eq have "a = a div b * b + a mod b" by simp
1539   moreover have "a div b = a div b" ..
1540   moreover have "a mod b = a mod b" ..
1541   note that ultimately show thesis by blast
1542 qed
1544 lemma mult_div_mod_eq: "b * (a div b) + a mod b = a"
1545   using div_mult_mod_eq [of a b] by (simp add: ac_simps)
1547 lemma mod_div_mult_eq: "a mod b + a div b * b = a"
1548   using div_mult_mod_eq [of a b] by (simp add: ac_simps)
1550 lemma mod_mult_div_eq: "a mod b + b * (a div b) = a"
1551   using div_mult_mod_eq [of a b] by (simp add: ac_simps)
1553 lemma minus_div_mult_eq_mod: "a - a div b * b = a mod b"
1554   by (rule add_implies_diff [symmetric]) (fact mod_div_mult_eq)
1556 lemma minus_mult_div_eq_mod: "a - b * (a div b) = a mod b"
1557   by (rule add_implies_diff [symmetric]) (fact mod_mult_div_eq)
1559 lemma minus_mod_eq_div_mult: "a - a mod b = a div b * b"
1560   by (rule add_implies_diff [symmetric]) (fact div_mult_mod_eq)
1562 lemma minus_mod_eq_mult_div: "a - a mod b = b * (a div b)"
1563   by (rule add_implies_diff [symmetric]) (fact mult_div_mod_eq)
1565 end
1568 text \<open>Quotient and remainder in integral domains\<close>
1570 class semidom_modulo = algebraic_semidom + semiring_modulo
1571 begin
1573 lemma mod_0 [simp]: "0 mod a = 0"
1574   using div_mult_mod_eq [of 0 a] by simp
1576 lemma mod_by_0 [simp]: "a mod 0 = a"
1577   using div_mult_mod_eq [of a 0] by simp
1579 lemma mod_by_1 [simp]:
1580   "a mod 1 = 0"
1581 proof -
1582   from div_mult_mod_eq [of a one] div_by_1 have "a + a mod 1 = a" by simp
1583   then have "a + a mod 1 = a + 0" by simp
1584   then show ?thesis by (rule add_left_imp_eq)
1585 qed
1587 lemma mod_self [simp]:
1588   "a mod a = 0"
1589   using div_mult_mod_eq [of a a] by simp
1591 lemma dvd_imp_mod_0 [simp]:
1592   assumes "a dvd b"
1593   shows "b mod a = 0"
1594   using assms minus_div_mult_eq_mod [of b a] by simp
1596 lemma mod_0_imp_dvd:
1597   assumes "a mod b = 0"
1598   shows   "b dvd a"
1599 proof -
1600   have "b dvd ((a div b) * b)" by simp
1601   also have "(a div b) * b = a"
1602     using div_mult_mod_eq [of a b] by (simp add: assms)
1603   finally show ?thesis .
1604 qed
1606 lemma mod_eq_0_iff_dvd:
1607   "a mod b = 0 \<longleftrightarrow> b dvd a"
1608   by (auto intro: mod_0_imp_dvd)
1610 lemma dvd_eq_mod_eq_0 [nitpick_unfold, code]:
1611   "a dvd b \<longleftrightarrow> b mod a = 0"
1614 lemma dvd_mod_iff:
1615   assumes "c dvd b"
1616   shows "c dvd a mod b \<longleftrightarrow> c dvd a"
1617 proof -
1618   from assms have "(c dvd a mod b) \<longleftrightarrow> (c dvd ((a div b) * b + a mod b))"
1620   also have "(a div b) * b + a mod b = a"
1621     using div_mult_mod_eq [of a b] by simp
1622   finally show ?thesis .
1623 qed
1625 lemma dvd_mod_imp_dvd:
1626   assumes "c dvd a mod b" and "c dvd b"
1627   shows "c dvd a"
1628   using assms dvd_mod_iff [of c b a] by simp
1630 lemma dvd_minus_mod [simp]:
1631   "b dvd a - a mod b"
1634 lemma cancel_div_mod_rules:
1635   "((a div b) * b + a mod b) + c = a + c"
1636   "(b * (a div b) + a mod b) + c = a + c"
1637   by (simp_all add: div_mult_mod_eq mult_div_mod_eq)
1639 end
1641 text \<open>Interlude: basic tool support for algebraic and arithmetic calculations\<close>
1643 named_theorems arith "arith facts -- only ground formulas"
1644 ML_file "Tools/arith_data.ML"
1646 ML_file "~~/src/Provers/Arith/cancel_div_mod.ML"
1648 ML \<open>
1649 structure Cancel_Div_Mod_Ring = Cancel_Div_Mod
1650 (
1651   val div_name = @{const_name divide};
1652   val mod_name = @{const_name modulo};
1653   val mk_binop = HOLogic.mk_binop;
1654   val mk_sum = Arith_Data.mk_sum;
1655   val dest_sum = Arith_Data.dest_sum;
1657   val div_mod_eqs = map mk_meta_eq @{thms cancel_div_mod_rules};
1659   val prove_eq_sums = Arith_Data.prove_conv2 all_tac (Arith_Data.simp_all_tac
1661 )
1662 \<close>
1664 simproc_setup cancel_div_mod_int ("(a::'a::semidom_modulo) + b") =
1665   \<open>K Cancel_Div_Mod_Ring.proc\<close>
1667 class idom_modulo = idom + semidom_modulo
1668 begin
1670 subclass idom_divide ..
1672 lemma div_diff [simp]:
1673   "c dvd a \<Longrightarrow> c dvd b \<Longrightarrow> (a - b) div c = a div c - b div c"
1674   using div_add [of _  _ "- b"] by (simp add: dvd_neg_div)
1676 end
1679 class ordered_semiring = semiring + ordered_comm_monoid_add +
1680   assumes mult_left_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b"
1681   assumes mult_right_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a * c \<le> b * c"
1682 begin
1684 lemma mult_mono: "a \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a * c \<le> b * d"
1685   apply (erule (1) mult_right_mono [THEN order_trans])
1686   apply (erule (1) mult_left_mono)
1687   done
1689 lemma mult_mono': "a \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> 0 \<le> a \<Longrightarrow> 0 \<le> c \<Longrightarrow> a * c \<le> b * d"
1690   by (rule mult_mono) (fast intro: order_trans)+
1692 end
1694 class ordered_semiring_0 = semiring_0 + ordered_semiring
1695 begin
1697 lemma mult_nonneg_nonneg [simp]: "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> a * b"
1698   using mult_left_mono [of 0 b a] by simp
1700 lemma mult_nonneg_nonpos: "0 \<le> a \<Longrightarrow> b \<le> 0 \<Longrightarrow> a * b \<le> 0"
1701   using mult_left_mono [of b 0 a] by simp
1703 lemma mult_nonpos_nonneg: "a \<le> 0 \<Longrightarrow> 0 \<le> b \<Longrightarrow> a * b \<le> 0"
1704   using mult_right_mono [of a 0 b] by simp
1706 text \<open>Legacy -- use @{thm [source] mult_nonpos_nonneg}.\<close>
1707 lemma mult_nonneg_nonpos2: "0 \<le> a \<Longrightarrow> b \<le> 0 \<Longrightarrow> b * a \<le> 0"
1708   by (drule mult_right_mono [of b 0]) auto
1710 lemma split_mult_neg_le: "(0 \<le> a \<and> b \<le> 0) \<or> (a \<le> 0 \<and> 0 \<le> b) \<Longrightarrow> a * b \<le> 0"
1711   by (auto simp add: mult_nonneg_nonpos mult_nonneg_nonpos2)
1713 end
1715 class ordered_cancel_semiring = ordered_semiring + cancel_comm_monoid_add
1716 begin
1718 subclass semiring_0_cancel ..
1720 subclass ordered_semiring_0 ..
1722 end
1724 class linordered_semiring = ordered_semiring + linordered_cancel_ab_semigroup_add
1725 begin
1727 subclass ordered_cancel_semiring ..
1733 lemma mult_left_less_imp_less: "c * a < c * b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a < b"
1734   by (force simp add: mult_left_mono not_le [symmetric])
1736 lemma mult_right_less_imp_less: "a * c < b * c \<Longrightarrow> 0 \<le> c \<Longrightarrow> a < b"
1737   by (force simp add: mult_right_mono not_le [symmetric])
1739 end
1741 class zero_less_one = order + zero + one +
1742   assumes zero_less_one [simp]: "0 < 1"
1744 class linordered_semiring_1 = linordered_semiring + semiring_1 + zero_less_one
1745 begin
1747 lemma convex_bound_le:
1748   assumes "x \<le> a" "y \<le> a" "0 \<le> u" "0 \<le> v" "u + v = 1"
1749   shows "u * x + v * y \<le> a"
1750 proof-
1751   from assms have "u * x + v * y \<le> u * a + v * a"
1753   with assms show ?thesis
1754     unfolding distrib_right[symmetric] by simp
1755 qed
1757 end
1760   assumes mult_strict_left_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b"
1761   assumes mult_strict_right_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> a * c < b * c"
1762 begin
1764 subclass semiring_0_cancel ..
1766 subclass linordered_semiring
1767 proof
1768   fix a b c :: 'a
1769   assume *: "a \<le> b" "0 \<le> c"
1770   then show "c * a \<le> c * b"
1771     unfolding le_less
1772     using mult_strict_left_mono by (cases "c = 0") auto
1773   from * show "a * c \<le> b * c"
1774     unfolding le_less
1775     using mult_strict_right_mono by (cases "c = 0") auto
1776 qed
1778 lemma mult_left_le_imp_le: "c * a \<le> c * b \<Longrightarrow> 0 < c \<Longrightarrow> a \<le> b"
1779   by (auto simp add: mult_strict_left_mono _not_less [symmetric])
1781 lemma mult_right_le_imp_le: "a * c \<le> b * c \<Longrightarrow> 0 < c \<Longrightarrow> a \<le> b"
1782   by (auto simp add: mult_strict_right_mono not_less [symmetric])
1784 lemma mult_pos_pos[simp]: "0 < a \<Longrightarrow> 0 < b \<Longrightarrow> 0 < a * b"
1785   using mult_strict_left_mono [of 0 b a] by simp
1787 lemma mult_pos_neg: "0 < a \<Longrightarrow> b < 0 \<Longrightarrow> a * b < 0"
1788   using mult_strict_left_mono [of b 0 a] by simp
1790 lemma mult_neg_pos: "a < 0 \<Longrightarrow> 0 < b \<Longrightarrow> a * b < 0"
1791   using mult_strict_right_mono [of a 0 b] by simp
1793 text \<open>Legacy -- use @{thm [source] mult_neg_pos}.\<close>
1794 lemma mult_pos_neg2: "0 < a \<Longrightarrow> b < 0 \<Longrightarrow> b * a < 0"
1795   by (drule mult_strict_right_mono [of b 0]) auto
1797 lemma zero_less_mult_pos: "0 < a * b \<Longrightarrow> 0 < a \<Longrightarrow> 0 < b"
1798   apply (cases "b \<le> 0")
1799    apply (auto simp add: le_less not_less)
1800   apply (drule_tac mult_pos_neg [of a b])
1801    apply (auto dest: less_not_sym)
1802   done
1804 lemma zero_less_mult_pos2: "0 < b * a \<Longrightarrow> 0 < a \<Longrightarrow> 0 < b"
1805   apply (cases "b \<le> 0")
1806    apply (auto simp add: le_less not_less)
1807   apply (drule_tac mult_pos_neg2 [of a b])
1808    apply (auto dest: less_not_sym)
1809   done
1811 text \<open>Strict monotonicity in both arguments\<close>
1812 lemma mult_strict_mono:
1813   assumes "a < b" and "c < d" and "0 < b" and "0 \<le> c"
1814   shows "a * c < b * d"
1815   using assms
1816   apply (cases "c = 0")
1817    apply simp
1818   apply (erule mult_strict_right_mono [THEN less_trans])
1819    apply (auto simp add: le_less)
1820   apply (erule (1) mult_strict_left_mono)
1821   done
1823 text \<open>This weaker variant has more natural premises\<close>
1824 lemma mult_strict_mono':
1825   assumes "a < b" and "c < d" and "0 \<le> a" and "0 \<le> c"
1826   shows "a * c < b * d"
1827   by (rule mult_strict_mono) (insert assms, auto)
1829 lemma mult_less_le_imp_less:
1830   assumes "a < b" and "c \<le> d" and "0 \<le> a" and "0 < c"
1831   shows "a * c < b * d"
1832   using assms
1833   apply (subgoal_tac "a * c < b * c")
1834    apply (erule less_le_trans)
1835    apply (erule mult_left_mono)
1836    apply simp
1837   apply (erule (1) mult_strict_right_mono)
1838   done
1840 lemma mult_le_less_imp_less:
1841   assumes "a \<le> b" and "c < d" and "0 < a" and "0 \<le> c"
1842   shows "a * c < b * d"
1843   using assms
1844   apply (subgoal_tac "a * c \<le> b * c")
1845    apply (erule le_less_trans)
1846    apply (erule mult_strict_left_mono)
1847    apply simp
1848   apply (erule (1) mult_right_mono)
1849   done
1851 end
1853 class linordered_semiring_1_strict = linordered_semiring_strict + semiring_1 + zero_less_one
1854 begin
1856 subclass linordered_semiring_1 ..
1858 lemma convex_bound_lt:
1859   assumes "x < a" "y < a" "0 \<le> u" "0 \<le> v" "u + v = 1"
1860   shows "u * x + v * y < a"
1861 proof -
1862   from assms have "u * x + v * y < u * a + v * a"
1863     by (cases "u = 0") (auto intro!: add_less_le_mono mult_strict_left_mono mult_left_mono)
1864   with assms show ?thesis
1865     unfolding distrib_right[symmetric] by simp
1866 qed
1868 end
1870 class ordered_comm_semiring = comm_semiring_0 + ordered_ab_semigroup_add +
1871   assumes comm_mult_left_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b"
1872 begin
1874 subclass ordered_semiring
1875 proof
1876   fix a b c :: 'a
1877   assume "a \<le> b" "0 \<le> c"
1878   then show "c * a \<le> c * b" by (rule comm_mult_left_mono)
1879   then show "a * c \<le> b * c" by (simp only: mult.commute)
1880 qed
1882 end
1884 class ordered_cancel_comm_semiring = ordered_comm_semiring + cancel_comm_monoid_add
1885 begin
1887 subclass comm_semiring_0_cancel ..
1888 subclass ordered_comm_semiring ..
1889 subclass ordered_cancel_semiring ..
1891 end
1893 class linordered_comm_semiring_strict = comm_semiring_0 + linordered_cancel_ab_semigroup_add +
1894   assumes comm_mult_strict_left_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b"
1895 begin
1897 subclass linordered_semiring_strict
1898 proof
1899   fix a b c :: 'a
1900   assume "a < b" "0 < c"
1901   then show "c * a < c * b"
1902     by (rule comm_mult_strict_left_mono)
1903   then show "a * c < b * c"
1904     by (simp only: mult.commute)
1905 qed
1907 subclass ordered_cancel_comm_semiring
1908 proof
1909   fix a b c :: 'a
1910   assume "a \<le> b" "0 \<le> c"
1911   then show "c * a \<le> c * b"
1912     unfolding le_less
1913     using mult_strict_left_mono by (cases "c = 0") auto
1914 qed
1916 end
1918 class ordered_ring = ring + ordered_cancel_semiring
1919 begin
1923 lemma less_add_iff1: "a * e + c < b * e + d \<longleftrightarrow> (a - b) * e + c < d"
1926 lemma less_add_iff2: "a * e + c < b * e + d \<longleftrightarrow> c < (b - a) * e + d"
1929 lemma le_add_iff1: "a * e + c \<le> b * e + d \<longleftrightarrow> (a - b) * e + c \<le> d"
1932 lemma le_add_iff2: "a * e + c \<le> b * e + d \<longleftrightarrow> c \<le> (b - a) * e + d"
1935 lemma mult_left_mono_neg: "b \<le> a \<Longrightarrow> c \<le> 0 \<Longrightarrow> c * a \<le> c * b"
1936   apply (drule mult_left_mono [of _ _ "- c"])
1937   apply simp_all
1938   done
1940 lemma mult_right_mono_neg: "b \<le> a \<Longrightarrow> c \<le> 0 \<Longrightarrow> a * c \<le> b * c"
1941   apply (drule mult_right_mono [of _ _ "- c"])
1942   apply simp_all
1943   done
1945 lemma mult_nonpos_nonpos: "a \<le> 0 \<Longrightarrow> b \<le> 0 \<Longrightarrow> 0 \<le> a * b"
1946   using mult_right_mono_neg [of a 0 b] by simp
1948 lemma split_mult_pos_le: "(0 \<le> a \<and> 0 \<le> b) \<or> (a \<le> 0 \<and> b \<le> 0) \<Longrightarrow> 0 \<le> a * b"
1949   by (auto simp add: mult_nonpos_nonpos)
1951 end
1953 class abs_if = minus + uminus + ord + zero + abs +
1954   assumes abs_if: "\<bar>a\<bar> = (if a < 0 then - a else a)"
1956 class linordered_ring = ring + linordered_semiring + linordered_ab_group_add + abs_if
1957 begin
1959 subclass ordered_ring ..
1962 proof
1963   fix a b
1964   show "\<bar>a + b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>"
1965     by (auto simp add: abs_if not_le not_less algebra_simps
1967 qed (auto simp: abs_if)
1969 lemma zero_le_square [simp]: "0 \<le> a * a"
1970   using linear [of 0 a] by (auto simp add: mult_nonpos_nonpos)
1972 lemma not_square_less_zero [simp]: "\<not> (a * a < 0)"
1975 proposition abs_eq_iff: "\<bar>x\<bar> = \<bar>y\<bar> \<longleftrightarrow> x = y \<or> x = -y"
1976   by (auto simp add: abs_if split: if_split_asm)
1978 lemma abs_eq_iff':
1979   "\<bar>a\<bar> = b \<longleftrightarrow> b \<ge> 0 \<and> (a = b \<or> a = - b)"
1980   by (cases "a \<ge> 0") auto
1982 lemma eq_abs_iff':
1983   "a = \<bar>b\<bar> \<longleftrightarrow> a \<ge> 0 \<and> (b = a \<or> b = - a)"
1984   using abs_eq_iff' [of b a] by auto
1986 lemma sum_squares_ge_zero: "0 \<le> x * x + y * y"
1989 lemma not_sum_squares_lt_zero: "\<not> x * x + y * y < 0"
1990   by (simp add: not_less sum_squares_ge_zero)
1992 end
1994 class linordered_ring_strict = ring + linordered_semiring_strict
1996 begin
1998 subclass linordered_ring ..
2000 lemma mult_strict_left_mono_neg: "b < a \<Longrightarrow> c < 0 \<Longrightarrow> c * a < c * b"
2001   using mult_strict_left_mono [of b a "- c"] by simp
2003 lemma mult_strict_right_mono_neg: "b < a \<Longrightarrow> c < 0 \<Longrightarrow> a * c < b * c"
2004   using mult_strict_right_mono [of b a "- c"] by simp
2006 lemma mult_neg_neg: "a < 0 \<Longrightarrow> b < 0 \<Longrightarrow> 0 < a * b"
2007   using mult_strict_right_mono_neg [of a 0 b] by simp
2009 subclass ring_no_zero_divisors
2010 proof
2011   fix a b
2012   assume "a \<noteq> 0"
2013   then have a: "a < 0 \<or> 0 < a" by (simp add: neq_iff)
2014   assume "b \<noteq> 0"
2015   then have b: "b < 0 \<or> 0 < b" by (simp add: neq_iff)
2016   have "a * b < 0 \<or> 0 < a * b"
2017   proof (cases "a < 0")
2018     case True
2019     show ?thesis
2020     proof (cases "b < 0")
2021       case True
2022       with \<open>a < 0\<close> show ?thesis by (auto dest: mult_neg_neg)
2023     next
2024       case False
2025       with b have "0 < b" by auto
2026       with \<open>a < 0\<close> show ?thesis by (auto dest: mult_strict_right_mono)
2027     qed
2028   next
2029     case False
2030     with a have "0 < a" by auto
2031     show ?thesis
2032     proof (cases "b < 0")
2033       case True
2034       with \<open>0 < a\<close> show ?thesis
2035         by (auto dest: mult_strict_right_mono_neg)
2036     next
2037       case False
2038       with b have "0 < b" by auto
2039       with \<open>0 < a\<close> show ?thesis by auto
2040     qed
2041   qed
2042   then show "a * b \<noteq> 0"
2044 qed
2046 lemma zero_less_mult_iff: "0 < a * b \<longleftrightarrow> 0 < a \<and> 0 < b \<or> a < 0 \<and> b < 0"
2047   by (cases a 0 b 0 rule: linorder_cases[case_product linorder_cases])
2048      (auto simp add: mult_neg_neg not_less le_less dest: zero_less_mult_pos zero_less_mult_pos2)
2050 lemma zero_le_mult_iff: "0 \<le> a * b \<longleftrightarrow> 0 \<le> a \<and> 0 \<le> b \<or> a \<le> 0 \<and> b \<le> 0"
2051   by (auto simp add: eq_commute [of 0] le_less not_less zero_less_mult_iff)
2053 lemma mult_less_0_iff: "a * b < 0 \<longleftrightarrow> 0 < a \<and> b < 0 \<or> a < 0 \<and> 0 < b"
2054   using zero_less_mult_iff [of "- a" b] by auto
2056 lemma mult_le_0_iff: "a * b \<le> 0 \<longleftrightarrow> 0 \<le> a \<and> b \<le> 0 \<or> a \<le> 0 \<and> 0 \<le> b"
2057   using zero_le_mult_iff [of "- a" b] by auto
2059 text \<open>
2060   Cancellation laws for @{term "c * a < c * b"} and @{term "a * c < b * c"},
2061   also with the relations \<open>\<le>\<close> and equality.
2062 \<close>
2064 text \<open>
2065   These ``disjunction'' versions produce two cases when the comparison is
2066   an assumption, but effectively four when the comparison is a goal.
2067 \<close>
2069 lemma mult_less_cancel_right_disj: "a * c < b * c \<longleftrightarrow> 0 < c \<and> a < b \<or> c < 0 \<and>  b < a"
2070   apply (cases "c = 0")
2071    apply (auto simp add: neq_iff mult_strict_right_mono mult_strict_right_mono_neg)
2072      apply (auto simp add: not_less not_le [symmetric, of "a*c"] not_le [symmetric, of a])
2073      apply (erule_tac [!] notE)
2074      apply (auto simp add: less_imp_le mult_right_mono mult_right_mono_neg)
2075   done
2077 lemma mult_less_cancel_left_disj: "c * a < c * b \<longleftrightarrow> 0 < c \<and> a < b \<or> c < 0 \<and>  b < a"
2078   apply (cases "c = 0")
2079    apply (auto simp add: neq_iff mult_strict_left_mono mult_strict_left_mono_neg)
2080      apply (auto simp add: not_less not_le [symmetric, of "c * a"] not_le [symmetric, of a])
2081      apply (erule_tac [!] notE)
2082      apply (auto simp add: less_imp_le mult_left_mono mult_left_mono_neg)
2083   done
2085 text \<open>
2086   The ``conjunction of implication'' lemmas produce two cases when the
2087   comparison is a goal, but give four when the comparison is an assumption.
2088 \<close>
2090 lemma mult_less_cancel_right: "a * c < b * c \<longleftrightarrow> (0 \<le> c \<longrightarrow> a < b) \<and> (c \<le> 0 \<longrightarrow> b < a)"
2091   using mult_less_cancel_right_disj [of a c b] by auto
2093 lemma mult_less_cancel_left: "c * a < c * b \<longleftrightarrow> (0 \<le> c \<longrightarrow> a < b) \<and> (c \<le> 0 \<longrightarrow> b < a)"
2094   using mult_less_cancel_left_disj [of c a b] by auto
2096 lemma mult_le_cancel_right: "a * c \<le> b * c \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> a)"
2097   by (simp add: not_less [symmetric] mult_less_cancel_right_disj)
2099 lemma mult_le_cancel_left: "c * a \<le> c * b \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> a)"
2100   by (simp add: not_less [symmetric] mult_less_cancel_left_disj)
2102 lemma mult_le_cancel_left_pos: "0 < c \<Longrightarrow> c * a \<le> c * b \<longleftrightarrow> a \<le> b"
2103   by (auto simp: mult_le_cancel_left)
2105 lemma mult_le_cancel_left_neg: "c < 0 \<Longrightarrow> c * a \<le> c * b \<longleftrightarrow> b \<le> a"
2106   by (auto simp: mult_le_cancel_left)
2108 lemma mult_less_cancel_left_pos: "0 < c \<Longrightarrow> c * a < c * b \<longleftrightarrow> a < b"
2109   by (auto simp: mult_less_cancel_left)
2111 lemma mult_less_cancel_left_neg: "c < 0 \<Longrightarrow> c * a < c * b \<longleftrightarrow> b < a"
2112   by (auto simp: mult_less_cancel_left)
2114 end
2116 lemmas mult_sign_intros =
2117   mult_nonneg_nonneg mult_nonneg_nonpos
2118   mult_nonpos_nonneg mult_nonpos_nonpos
2119   mult_pos_pos mult_pos_neg
2120   mult_neg_pos mult_neg_neg
2122 class ordered_comm_ring = comm_ring + ordered_comm_semiring
2123 begin
2125 subclass ordered_ring ..
2126 subclass ordered_cancel_comm_semiring ..
2128 end
2130 class linordered_nonzero_semiring = ordered_comm_semiring + monoid_mult + linorder + zero_less_one
2131 begin
2133 subclass zero_neq_one
2134   by standard (insert zero_less_one, blast)
2136 subclass comm_semiring_1
2137   by standard (rule mult_1_left)
2139 lemma zero_le_one [simp]: "0 \<le> 1"
2140   by (rule zero_less_one [THEN less_imp_le])
2142 lemma not_one_le_zero [simp]: "\<not> 1 \<le> 0"
2145 lemma not_one_less_zero [simp]: "\<not> 1 < 0"
2148 lemma mult_left_le: "c \<le> 1 \<Longrightarrow> 0 \<le> a \<Longrightarrow> a * c \<le> a"
2149   using mult_left_mono[of c 1 a] by simp
2151 lemma mult_le_one: "a \<le> 1 \<Longrightarrow> 0 \<le> b \<Longrightarrow> b \<le> 1 \<Longrightarrow> a * b \<le> 1"
2152   using mult_mono[of a 1 b 1] by simp
2154 lemma zero_less_two: "0 < 1 + 1"
2155   using add_pos_pos[OF zero_less_one zero_less_one] .
2157 end
2159 class linordered_semidom = semidom + linordered_comm_semiring_strict + zero_less_one +
2160   assumes le_add_diff_inverse2 [simp]: "b \<le> a \<Longrightarrow> a - b + b = a"
2161 begin
2163 subclass linordered_nonzero_semiring ..
2165 text \<open>Addition is the inverse of subtraction.\<close>
2167 lemma le_add_diff_inverse [simp]: "b \<le> a \<Longrightarrow> b + (a - b) = a"
2170 lemma add_diff_inverse: "\<not> a < b \<Longrightarrow> b + (a - b) = a"
2171   by simp
2173 lemma add_le_imp_le_diff: "i + k \<le> n \<Longrightarrow> i \<le> n - k"
2174   apply (subst add_le_cancel_right [where c=k, symmetric])
2176   apply (simp only: add.assoc [symmetric])
2178   apply fastforce
2179   done
2182   assumes 1: "i + k \<le> n"
2183     and 2: "n \<le> j + k"
2184   shows "i + k \<le> n \<Longrightarrow> n \<le> j + k \<Longrightarrow> n - k \<le> j"
2185 proof -
2186   have "n - (i + k) + (i + k) = n"
2187     using 1 by simp
2188   moreover have "n - k = n - k - i + i"
2190   ultimately show ?thesis
2191     using 2
2193     apply (rule add_le_imp_le_diff [of _ k "j + k", simplified add_diff_cancel_right'])
2195     done
2196 qed
2198 lemma less_1_mult: "1 < m \<Longrightarrow> 1 < n \<Longrightarrow> 1 < m * n"
2199   using mult_strict_mono [of 1 m 1 n] by (simp add: less_trans [OF zero_less_one])
2201 end
2203 class linordered_idom = comm_ring_1 + linordered_comm_semiring_strict +
2204   ordered_ab_group_add + abs_if + sgn +
2205   assumes sgn_if: "sgn x = (if x = 0 then 0 else if 0 < x then 1 else - 1)"
2206 begin
2208 subclass linordered_ring_strict ..
2210 subclass linordered_semiring_1_strict
2211 proof
2212   have "0 \<le> 1 * 1"
2213     by (fact zero_le_square)
2214   then show "0 < 1"
2216 qed
2218 subclass ordered_comm_ring ..
2219 subclass idom ..
2221 subclass linordered_semidom
2222   by standard simp
2224 subclass idom_abs_sgn
2225   by standard
2226     (auto simp add: sgn_if abs_if zero_less_mult_iff)
2228 lemma linorder_neqE_linordered_idom:
2229   assumes "x \<noteq> y"
2230   obtains "x < y" | "y < x"
2231   using assms by (rule neqE)
2233 text \<open>These cancellation simp rules also produce two cases when the comparison is a goal.\<close>
2235 lemma mult_le_cancel_right1: "c \<le> b * c \<longleftrightarrow> (0 < c \<longrightarrow> 1 \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> 1)"
2236   using mult_le_cancel_right [of 1 c b] by simp
2238 lemma mult_le_cancel_right2: "a * c \<le> c \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> 1) \<and> (c < 0 \<longrightarrow> 1 \<le> a)"
2239   using mult_le_cancel_right [of a c 1] by simp
2241 lemma mult_le_cancel_left1: "c \<le> c * b \<longleftrightarrow> (0 < c \<longrightarrow> 1 \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> 1)"
2242   using mult_le_cancel_left [of c 1 b] by simp
2244 lemma mult_le_cancel_left2: "c * a \<le> c \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> 1) \<and> (c < 0 \<longrightarrow> 1 \<le> a)"
2245   using mult_le_cancel_left [of c a 1] by simp
2247 lemma mult_less_cancel_right1: "c < b * c \<longleftrightarrow> (0 \<le> c \<longrightarrow> 1 < b) \<and> (c \<le> 0 \<longrightarrow> b < 1)"
2248   using mult_less_cancel_right [of 1 c b] by simp
2250 lemma mult_less_cancel_right2: "a * c < c \<longleftrightarrow> (0 \<le> c \<longrightarrow> a < 1) \<and> (c \<le> 0 \<longrightarrow> 1 < a)"
2251   using mult_less_cancel_right [of a c 1] by simp
2253 lemma mult_less_cancel_left1: "c < c * b \<longleftrightarrow> (0 \<le> c \<longrightarrow> 1 < b) \<and> (c \<le> 0 \<longrightarrow> b < 1)"
2254   using mult_less_cancel_left [of c 1 b] by simp
2256 lemma mult_less_cancel_left2: "c * a < c \<longleftrightarrow> (0 \<le> c \<longrightarrow> a < 1) \<and> (c \<le> 0 \<longrightarrow> 1 < a)"
2257   using mult_less_cancel_left [of c a 1] by simp
2259 lemma sgn_0_0: "sgn a = 0 \<longleftrightarrow> a = 0"
2260   by (fact sgn_eq_0_iff)
2262 lemma sgn_1_pos: "sgn a = 1 \<longleftrightarrow> a > 0"
2263   unfolding sgn_if by simp
2265 lemma sgn_1_neg: "sgn a = - 1 \<longleftrightarrow> a < 0"
2266   unfolding sgn_if by auto
2268 lemma sgn_pos [simp]: "0 < a \<Longrightarrow> sgn a = 1"
2269   by (simp only: sgn_1_pos)
2271 lemma sgn_neg [simp]: "a < 0 \<Longrightarrow> sgn a = - 1"
2272   by (simp only: sgn_1_neg)
2274 lemma abs_sgn: "\<bar>k\<bar> = k * sgn k"
2275   unfolding sgn_if abs_if by auto
2277 lemma sgn_greater [simp]: "0 < sgn a \<longleftrightarrow> 0 < a"
2278   unfolding sgn_if by auto
2280 lemma sgn_less [simp]: "sgn a < 0 \<longleftrightarrow> a < 0"
2281   unfolding sgn_if by auto
2283 lemma abs_sgn_eq_1 [simp]:
2284   "a \<noteq> 0 \<Longrightarrow> \<bar>sgn a\<bar> = 1"
2285   by simp
2287 lemma abs_sgn_eq: "\<bar>sgn a\<bar> = (if a = 0 then 0 else 1)"
2290 lemma sgn_mult_self_eq [simp]:
2291   "sgn a * sgn a = of_bool (a \<noteq> 0)"
2292   by (cases "a > 0") simp_all
2294 lemma abs_mult_self_eq [simp]:
2295   "\<bar>a\<bar> * \<bar>a\<bar> = a * a"
2296   by (cases "a > 0") simp_all
2299   "sgn (a + b) = sgn a" if "sgn b = sgn a"
2300 proof (cases a 0 rule: linorder_cases)
2301   case equal
2302   with that show ?thesis
2303     by simp
2304 next
2305   case less
2306   with that have "b < 0"
2308   with \<open>a < 0\<close> have "a + b < 0"
2310   with \<open>a < 0\<close> show ?thesis
2311     by simp
2312 next
2313   case greater
2314   with that have "b > 0"
2316   with \<open>a > 0\<close> have "a + b > 0"
2318   with \<open>a > 0\<close> show ?thesis
2319     by simp
2320 qed
2323   "\<bar>a + b\<bar> = \<bar>a\<bar> + \<bar>b\<bar>" if "sgn b = sgn a"
2324 proof -
2325   have "a + b = sgn a * \<bar>a\<bar> + sgn b * \<bar>b\<bar>"
2327   also have "\<dots> = sgn a * (\<bar>a\<bar> + \<bar>b\<bar>)"
2328     using that by (simp add: algebra_simps)
2329   finally show ?thesis
2330     by (auto simp add: abs_mult)
2331 qed
2333 lemma sgn_not_eq_imp:
2334   "sgn a = - sgn b" if "sgn b \<noteq> sgn a" and "sgn a \<noteq> 0" and "sgn b \<noteq> 0"
2335   using that by (cases "a < 0") (auto simp add: sgn_0_0 sgn_1_pos sgn_1_neg)
2337 lemma abs_dvd_iff [simp]: "\<bar>m\<bar> dvd k \<longleftrightarrow> m dvd k"
2340 lemma dvd_abs_iff [simp]: "m dvd \<bar>k\<bar> \<longleftrightarrow> m dvd k"
2343 lemma dvd_if_abs_eq: "\<bar>l\<bar> = \<bar>k\<bar> \<Longrightarrow> l dvd k"
2344   by (subst abs_dvd_iff [symmetric]) simp
2346 text \<open>
2347   The following lemmas can be proven in more general structures, but
2348   are dangerous as simp rules in absence of @{thm neg_equal_zero},
2349   @{thm neg_less_pos}, @{thm neg_less_eq_nonneg}.
2350 \<close>
2352 lemma equation_minus_iff_1 [simp, no_atp]: "1 = - a \<longleftrightarrow> a = - 1"
2353   by (fact equation_minus_iff)
2355 lemma minus_equation_iff_1 [simp, no_atp]: "- a = 1 \<longleftrightarrow> a = - 1"
2356   by (subst minus_equation_iff, auto)
2358 lemma le_minus_iff_1 [simp, no_atp]: "1 \<le> - b \<longleftrightarrow> b \<le> - 1"
2359   by (fact le_minus_iff)
2361 lemma minus_le_iff_1 [simp, no_atp]: "- a \<le> 1 \<longleftrightarrow> - 1 \<le> a"
2362   by (fact minus_le_iff)
2364 lemma less_minus_iff_1 [simp, no_atp]: "1 < - b \<longleftrightarrow> b < - 1"
2365   by (fact less_minus_iff)
2367 lemma minus_less_iff_1 [simp, no_atp]: "- a < 1 \<longleftrightarrow> - 1 < a"
2368   by (fact minus_less_iff)
2371   shows "x+y < 0 \<Longrightarrow> x<0 \<or> y<0"
2372   by (auto simp: not_less intro: le_less_trans [of _ "x+y"])
2374 end
2376 text \<open>Simprules for comparisons where common factors can be cancelled.\<close>
2378 lemmas mult_compare_simps =
2379   mult_le_cancel_right mult_le_cancel_left
2380   mult_le_cancel_right1 mult_le_cancel_right2
2381   mult_le_cancel_left1 mult_le_cancel_left2
2382   mult_less_cancel_right mult_less_cancel_left
2383   mult_less_cancel_right1 mult_less_cancel_right2
2384   mult_less_cancel_left1 mult_less_cancel_left2
2385   mult_cancel_right mult_cancel_left
2386   mult_cancel_right1 mult_cancel_right2
2387   mult_cancel_left1 mult_cancel_left2
2390 text \<open>Reasoning about inequalities with division\<close>
2392 context linordered_semidom
2393 begin
2395 lemma less_add_one: "a < a + 1"
2396 proof -
2397   have "a + 0 < a + 1"
2398     by (blast intro: zero_less_one add_strict_left_mono)
2399   then show ?thesis by simp
2400 qed
2402 end
2404 context linordered_idom
2405 begin
2407 lemma mult_right_le_one_le: "0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> y \<le> 1 \<Longrightarrow> x * y \<le> x"
2408   by (rule mult_left_le)
2410 lemma mult_left_le_one_le: "0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> y \<le> 1 \<Longrightarrow> y * x \<le> x"
2411   by (auto simp add: mult_le_cancel_right2)
2413 end
2415 text \<open>Absolute Value\<close>
2417 context linordered_idom
2418 begin
2420 lemma mult_sgn_abs: "sgn x * \<bar>x\<bar> = x"
2421   by (fact sgn_mult_abs)
2423 lemma abs_one: "\<bar>1\<bar> = 1"
2424   by (fact abs_1)
2426 end
2428 class ordered_ring_abs = ordered_ring + ordered_ab_group_add_abs +
2429   assumes abs_eq_mult:
2430     "(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>"
2432 context linordered_idom
2433 begin
2435 subclass ordered_ring_abs
2436   by standard (auto simp: abs_if not_less mult_less_0_iff)
2438 lemma abs_mult_self [simp]: "\<bar>a\<bar> * \<bar>a\<bar> = a * a"
2441 lemma abs_mult_less:
2442   assumes ac: "\<bar>a\<bar> < c"
2443     and bd: "\<bar>b\<bar> < d"
2444   shows "\<bar>a\<bar> * \<bar>b\<bar> < c * d"
2445 proof -
2446   from ac have "0 < c"
2447     by (blast intro: le_less_trans abs_ge_zero)
2448   with bd show ?thesis by (simp add: ac mult_strict_mono)
2449 qed
2451 lemma abs_less_iff: "\<bar>a\<bar> < b \<longleftrightarrow> a < b \<and> - a < b"
2454 lemma abs_mult_pos: "0 \<le> x \<Longrightarrow> \<bar>y\<bar> * x = \<bar>y * x\<bar>"
2457 lemma abs_diff_less_iff: "\<bar>x - a\<bar> < r \<longleftrightarrow> a - r < x \<and> x < a + r"
2458   by (auto simp add: diff_less_eq ac_simps abs_less_iff)
2460 lemma abs_diff_le_iff: "\<bar>x - a\<bar> \<le> r \<longleftrightarrow> a - r \<le> x \<and> x \<le> a + r"
2461   by (auto simp add: diff_le_eq ac_simps abs_le_iff)
2463 lemma abs_add_one_gt_zero: "0 < 1 + \<bar>x\<bar>"
2464   by (auto simp: abs_if not_less intro: zero_less_one add_strict_increasing less_trans)
2466 end
2468 subsection \<open>Dioids\<close>
2470 text \<open>
2471   Dioids are the alternative extensions of semirings, a semiring can
2472   either be a ring or a dioid but never both.
2473 \<close>
2475 class dioid = semiring_1 + canonically_ordered_monoid_add
2476 begin
2478 subclass ordered_semiring
2479   by standard (auto simp: le_iff_add distrib_left distrib_right)
2481 end
2484 hide_fact (open) comm_mult_left_mono comm_mult_strict_left_mono distrib
2486 code_identifier
2487   code_module Rings \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
2489 end