# Theory Rings

Up to index of Isabelle/HOL

theory Rings
imports Groups
(*  Title:      HOL/Rings.thy    Author:     Gertrud Bauer    Author:     Steven Obua    Author:     Tobias Nipkow    Author:     Lawrence C Paulson    Author:     Markus Wenzel    Author:     Jeremy Avigad*)header {* Rings *}theory Ringsimports Groupsbeginclass semiring = ab_semigroup_add + semigroup_mult +  assumes distrib_right[algebra_simps, field_simps]: "(a + b) * c = a * c + b * c"  assumes distrib_left[algebra_simps, field_simps]: "a * (b + c) = a * b + a * c"begintext{*For the @{text combine_numerals} simproc*}lemma combine_common_factor:  "a * e + (b * e + c) = (a + b) * e + c"by (simp add: distrib_right add_ac)endclass mult_zero = times + zero +  assumes mult_zero_left [simp]: "0 * a = 0"  assumes mult_zero_right [simp]: "a * 0 = 0"class semiring_0 = semiring + comm_monoid_add + mult_zeroclass semiring_0_cancel = semiring + cancel_comm_monoid_addbeginsubclass semiring_0proof  fix a :: 'a  have "0 * a + 0 * a = 0 * a + 0" by (simp add: distrib_right [symmetric])  thus "0 * a = 0" by (simp only: add_left_cancel)next  fix a :: 'a  have "a * 0 + a * 0 = a * 0 + 0" by (simp add: distrib_left [symmetric])  thus "a * 0 = 0" by (simp only: add_left_cancel)qedendclass comm_semiring = ab_semigroup_add + ab_semigroup_mult +  assumes distrib: "(a + b) * c = a * c + b * c"beginsubclass semiringproof  fix a b c :: 'a  show "(a + b) * c = a * c + b * c" by (simp add: distrib)  have "a * (b + c) = (b + c) * a" by (simp add: mult_ac)  also have "... = b * a + c * a" by (simp only: distrib)  also have "... = a * b + a * c" by (simp add: mult_ac)  finally show "a * (b + c) = a * b + a * c" by blastqedendclass comm_semiring_0 = comm_semiring + comm_monoid_add + mult_zerobeginsubclass semiring_0 ..endclass comm_semiring_0_cancel = comm_semiring + cancel_comm_monoid_addbeginsubclass semiring_0_cancel ..subclass comm_semiring_0 ..endclass zero_neq_one = zero + one +  assumes zero_neq_one [simp]: "0 ≠ 1"beginlemma one_neq_zero [simp]: "1 ≠ 0"by (rule not_sym) (rule zero_neq_one)endclass semiring_1 = zero_neq_one + semiring_0 + monoid_multtext {* Abstract divisibility *}class dvd = timesbegindefinition dvd :: "'a => 'a => bool" (infix "dvd" 50) where  "b dvd a <-> (∃k. a = b * k)"lemma dvdI [intro?]: "a = b * k ==> b dvd a"  unfolding dvd_def ..lemma dvdE [elim?]: "b dvd a ==> (!!k. a = b * k ==> P) ==> P"  unfolding dvd_def by blast endclass comm_semiring_1 = zero_neq_one + comm_semiring_0 + comm_monoid_mult + dvd  (*previously almost_semiring*)beginsubclass semiring_1 ..lemma dvd_refl[simp]: "a dvd a"proof  show "a = a * 1" by simpqedlemma dvd_trans:  assumes "a dvd b" and "b dvd c"  shows "a dvd c"proof -  from assms obtain v where "b = a * v" by (auto elim!: dvdE)  moreover from assms obtain w where "c = b * w" by (auto elim!: dvdE)  ultimately have "c = a * (v * w)" by (simp add: mult_assoc)  then show ?thesis ..qedlemma dvd_0_left_iff [no_atp, simp]: "0 dvd a <-> a = 0"by (auto intro: dvd_refl elim!: dvdE)lemma dvd_0_right [iff]: "a dvd 0"proof  show "0 = a * 0" by simpqedlemma one_dvd [simp]: "1 dvd a"by (auto intro!: dvdI)lemma dvd_mult[simp]: "a dvd c ==> a dvd (b * c)"by (auto intro!: mult_left_commute dvdI elim!: dvdE)lemma dvd_mult2[simp]: "a dvd b ==> a dvd (b * c)"  apply (subst mult_commute)  apply (erule dvd_mult)  donelemma dvd_triv_right [simp]: "a dvd b * a"by (rule dvd_mult) (rule dvd_refl)lemma dvd_triv_left [simp]: "a dvd a * b"by (rule dvd_mult2) (rule dvd_refl)lemma mult_dvd_mono:  assumes "a dvd b"    and "c dvd d"  shows "a * c dvd b * d"proof -  from a dvd b obtain b' where "b = a * b'" ..  moreover from c dvd d obtain d' where "d = c * d'" ..  ultimately have "b * d = (a * c) * (b' * d')" by (simp add: mult_ac)  then show ?thesis ..qedlemma dvd_mult_left: "a * b dvd c ==> a dvd c"by (simp add: dvd_def mult_assoc, blast)lemma dvd_mult_right: "a * b dvd c ==> b dvd c"  unfolding mult_ac [of a] by (rule dvd_mult_left)lemma dvd_0_left: "0 dvd a ==> a = 0"by simplemma dvd_add[simp]:  assumes "a dvd b" and "a dvd c" shows "a dvd (b + c)"proof -  from a dvd b obtain b' where "b = a * b'" ..  moreover from a dvd c obtain c' where "c = a * c'" ..  ultimately have "b + c = a * (b' + c')" by (simp add: distrib_left)  then show ?thesis ..qedendclass no_zero_divisors = zero + times +  assumes no_zero_divisors: "a ≠ 0 ==> b ≠ 0 ==> a * b ≠ 0"beginlemma divisors_zero:  assumes "a * b = 0"  shows "a = 0 ∨ b = 0"proof (rule classical)  assume "¬ (a = 0 ∨ b = 0)"  then have "a ≠ 0" and "b ≠ 0" by auto  with no_zero_divisors have "a * b ≠ 0" by blast  with assms show ?thesis by simpqedendclass semiring_1_cancel = semiring + cancel_comm_monoid_add  + zero_neq_one + monoid_multbeginsubclass semiring_0_cancel ..subclass semiring_1 ..endclass comm_semiring_1_cancel = comm_semiring + cancel_comm_monoid_add  + zero_neq_one + comm_monoid_multbeginsubclass semiring_1_cancel ..subclass comm_semiring_0_cancel ..subclass comm_semiring_1 ..endclass ring = semiring + ab_group_addbeginsubclass semiring_0_cancel ..text {* Distribution rules *}lemma minus_mult_left: "- (a * b) = - a * b"by (rule minus_unique) (simp add: distrib_right [symmetric]) lemma minus_mult_right: "- (a * b) = a * - b"by (rule minus_unique) (simp add: distrib_left [symmetric]) text{*Extract signs from products*}lemmas mult_minus_left [simp, no_atp] = minus_mult_left [symmetric]lemmas mult_minus_right [simp,no_atp] = minus_mult_right [symmetric]lemma minus_mult_minus [simp]: "- a * - b = a * b"by simplemma minus_mult_commute: "- a * b = a * - b"by simplemma right_diff_distrib[algebra_simps, field_simps]: "a * (b - c) = a * b - a * c"by (simp add: distrib_left diff_minus)lemma left_diff_distrib[algebra_simps, field_simps]: "(a - b) * c = a * c - b * c"by (simp add: distrib_right diff_minus)lemmas ring_distribs[no_atp] =  distrib_left distrib_right left_diff_distrib right_diff_distriblemma eq_add_iff1:  "a * e + c = b * e + d <-> (a - b) * e + c = d"by (simp add: algebra_simps)lemma eq_add_iff2:  "a * e + c = b * e + d <-> c = (b - a) * e + d"by (simp add: algebra_simps)endlemmas ring_distribs[no_atp] =  distrib_left distrib_right left_diff_distrib right_diff_distribclass comm_ring = comm_semiring + ab_group_addbeginsubclass ring ..subclass comm_semiring_0_cancel ..lemma square_diff_square_factored:  "x * x - y * y = (x + y) * (x - y)"  by (simp add: algebra_simps)endclass ring_1 = ring + zero_neq_one + monoid_multbeginsubclass semiring_1_cancel ..lemma square_diff_one_factored:  "x * x - 1 = (x + 1) * (x - 1)"  by (simp add: algebra_simps)endclass comm_ring_1 = comm_ring + zero_neq_one + comm_monoid_mult  (*previously ring*)beginsubclass ring_1 ..subclass comm_semiring_1_cancel ..lemma dvd_minus_iff [simp]: "x dvd - y <-> x dvd y"proof  assume "x dvd - y"  then have "x dvd - 1 * - y" by (rule dvd_mult)  then show "x dvd y" by simpnext  assume "x dvd y"  then have "x dvd - 1 * y" by (rule dvd_mult)  then show "x dvd - y" by simpqedlemma minus_dvd_iff [simp]: "- x dvd y <-> x dvd y"proof  assume "- x dvd y"  then obtain k where "y = - x * k" ..  then have "y = x * - k" by simp  then show "x dvd y" ..next  assume "x dvd y"  then obtain k where "y = x * k" ..  then have "y = - x * - k" by simp  then show "- x dvd y" ..qedlemma dvd_diff[simp]: "x dvd y ==> x dvd z ==> x dvd (y - z)"by (simp only: diff_minus dvd_add dvd_minus_iff)endclass ring_no_zero_divisors = ring + no_zero_divisorsbeginlemma mult_eq_0_iff [simp]:  shows "a * b = 0 <-> (a = 0 ∨ b = 0)"proof (cases "a = 0 ∨ b = 0")  case False then have "a ≠ 0" and "b ≠ 0" by auto    then show ?thesis using no_zero_divisors by simpnext  case True then show ?thesis by autoqedtext{*Cancellation of equalities with a common factor*}lemma mult_cancel_right [simp, no_atp]:  "a * c = b * c <-> c = 0 ∨ a = b"proof -  have "(a * c = b * c) = ((a - b) * c = 0)"    by (simp add: algebra_simps)  thus ?thesis by (simp add: disj_commute)qedlemma mult_cancel_left [simp, no_atp]:  "c * a = c * b <-> c = 0 ∨ a = b"proof -  have "(c * a = c * b) = (c * (a - b) = 0)"    by (simp add: algebra_simps)  thus ?thesis by simpqedendclass ring_1_no_zero_divisors = ring_1 + ring_no_zero_divisorsbeginlemma square_eq_1_iff:  "x * x = 1 <-> x = 1 ∨ x = - 1"proof -  have "(x - 1) * (x + 1) = x * x - 1"    by (simp add: algebra_simps)  hence "x * x = 1 <-> (x - 1) * (x + 1) = 0"    by simp  thus ?thesis    by (simp add: eq_neg_iff_add_eq_0)qedlemma mult_cancel_right1 [simp]:  "c = b * c <-> c = 0 ∨ b = 1"by (insert mult_cancel_right [of 1 c b], force)lemma mult_cancel_right2 [simp]:  "a * c = c <-> c = 0 ∨ a = 1"by (insert mult_cancel_right [of a c 1], simp) lemma mult_cancel_left1 [simp]:  "c = c * b <-> c = 0 ∨ b = 1"by (insert mult_cancel_left [of c 1 b], force)lemma mult_cancel_left2 [simp]:  "c * a = c <-> c = 0 ∨ a = 1"by (insert mult_cancel_left [of c a 1], simp)endclass idom = comm_ring_1 + no_zero_divisorsbeginsubclass ring_1_no_zero_divisors ..lemma square_eq_iff: "a * a = b * b <-> (a = b ∨ a = - b)"proof  assume "a * a = b * b"  then have "(a - b) * (a + b) = 0"    by (simp add: algebra_simps)  then show "a = b ∨ a = - b"    by (simp add: eq_neg_iff_add_eq_0)next  assume "a = b ∨ a = - b"  then show "a * a = b * b" by autoqedlemma dvd_mult_cancel_right [simp]:  "a * c dvd b * c <-> c = 0 ∨ a dvd b"proof -  have "a * c dvd b * c <-> (∃k. b * c = (a * k) * c)"    unfolding dvd_def by (simp add: mult_ac)  also have "(∃k. b * c = (a * k) * c) <-> c = 0 ∨ a dvd b"    unfolding dvd_def by simp  finally show ?thesis .qedlemma dvd_mult_cancel_left [simp]:  "c * a dvd c * b <-> c = 0 ∨ a dvd b"proof -  have "c * a dvd c * b <-> (∃k. b * c = (a * k) * c)"    unfolding dvd_def by (simp add: mult_ac)  also have "(∃k. b * c = (a * k) * c) <-> c = 0 ∨ a dvd b"    unfolding dvd_def by simp  finally show ?thesis .qedendtext {*  The theory of partially ordered rings is taken from the books:  \begin{itemize}  \item \emph{Lattice Theory} by Garret Birkhoff, American Mathematical Society 1979   \item \emph{Partially Ordered Algebraic Systems}, Pergamon Press 1963  \end{itemize}  Most of the used notions can also be looked up in   \begin{itemize}  \item \url{http://www.mathworld.com} by Eric Weisstein et. al.  \item \emph{Algebra I} by van der Waerden, Springer.  \end{itemize}*}class ordered_semiring = semiring + comm_monoid_add + ordered_ab_semigroup_add +  assumes mult_left_mono: "a ≤ b ==> 0 ≤ c ==> c * a ≤ c * b"  assumes mult_right_mono: "a ≤ b ==> 0 ≤ c ==> a * c ≤ b * c"beginlemma mult_mono:  "a ≤ b ==> c ≤ d ==> 0 ≤ b ==> 0 ≤ c ==> a * c ≤ b * d"apply (erule mult_right_mono [THEN order_trans], assumption)apply (erule mult_left_mono, assumption)donelemma mult_mono':  "a ≤ b ==> c ≤ d ==> 0 ≤ a ==> 0 ≤ c ==> a * c ≤ b * d"apply (rule mult_mono)apply (fast intro: order_trans)+doneendclass ordered_cancel_semiring = ordered_semiring + cancel_comm_monoid_addbeginsubclass semiring_0_cancel ..lemma mult_nonneg_nonneg: "0 ≤ a ==> 0 ≤ b ==> 0 ≤ a * b"using mult_left_mono [of 0 b a] by simplemma mult_nonneg_nonpos: "0 ≤ a ==> b ≤ 0 ==> a * b ≤ 0"using mult_left_mono [of b 0 a] by simplemma mult_nonpos_nonneg: "a ≤ 0 ==> 0 ≤ b ==> a * b ≤ 0"using mult_right_mono [of a 0 b] by simptext {* Legacy - use @{text mult_nonpos_nonneg} *}lemma mult_nonneg_nonpos2: "0 ≤ a ==> b ≤ 0 ==> b * a ≤ 0" by (drule mult_right_mono [of b 0], auto)lemma split_mult_neg_le: "(0 ≤ a & b ≤ 0) | (a ≤ 0 & 0 ≤ b) ==> a * b ≤ 0" by (auto simp add: mult_nonneg_nonpos mult_nonneg_nonpos2)endclass linordered_semiring = ordered_semiring + linordered_cancel_ab_semigroup_addbeginsubclass ordered_cancel_semiring ..subclass ordered_comm_monoid_add ..lemma mult_left_less_imp_less:  "c * a < c * b ==> 0 ≤ c ==> a < b"by (force simp add: mult_left_mono not_le [symmetric]) lemma mult_right_less_imp_less:  "a * c < b * c ==> 0 ≤ c ==> a < b"by (force simp add: mult_right_mono not_le [symmetric])endclass linordered_semiring_1 = linordered_semiring + semiring_1beginlemma convex_bound_le:  assumes "x ≤ a" "y ≤ a" "0 ≤ u" "0 ≤ v" "u + v = 1"  shows "u * x + v * y ≤ a"proof-  from assms have "u * x + v * y ≤ u * a + v * a"    by (simp add: add_mono mult_left_mono)  thus ?thesis using assms unfolding distrib_right[symmetric] by simpqedendclass linordered_semiring_strict = semiring + comm_monoid_add + linordered_cancel_ab_semigroup_add +  assumes mult_strict_left_mono: "a < b ==> 0 < c ==> c * a < c * b"  assumes mult_strict_right_mono: "a < b ==> 0 < c ==> a * c < b * c"beginsubclass semiring_0_cancel ..subclass linordered_semiringproof  fix a b c :: 'a  assume A: "a ≤ b" "0 ≤ c"  from A show "c * a ≤ c * b"    unfolding le_less    using mult_strict_left_mono by (cases "c = 0") auto  from A show "a * c ≤ b * c"    unfolding le_less    using mult_strict_right_mono by (cases "c = 0") autoqedlemma mult_left_le_imp_le:  "c * a ≤ c * b ==> 0 < c ==> a ≤ b"by (force simp add: mult_strict_left_mono _not_less [symmetric]) lemma mult_right_le_imp_le:  "a * c ≤ b * c ==> 0 < c ==> a ≤ b"by (force simp add: mult_strict_right_mono not_less [symmetric])lemma mult_pos_pos: "0 < a ==> 0 < b ==> 0 < a * b"using mult_strict_left_mono [of 0 b a] by simplemma mult_pos_neg: "0 < a ==> b < 0 ==> a * b < 0"using mult_strict_left_mono [of b 0 a] by simplemma mult_neg_pos: "a < 0 ==> 0 < b ==> a * b < 0"using mult_strict_right_mono [of a 0 b] by simptext {* Legacy - use @{text mult_neg_pos} *}lemma mult_pos_neg2: "0 < a ==> b < 0 ==> b * a < 0" by (drule mult_strict_right_mono [of b 0], auto)lemma zero_less_mult_pos:  "0 < a * b ==> 0 < a ==> 0 < b"apply (cases "b≤0") apply (auto simp add: le_less not_less)apply (drule_tac mult_pos_neg [of a b]) apply (auto dest: less_not_sym)donelemma zero_less_mult_pos2:  "0 < b * a ==> 0 < a ==> 0 < b"apply (cases "b≤0") apply (auto simp add: le_less not_less)apply (drule_tac mult_pos_neg2 [of a b]) apply (auto dest: less_not_sym)donetext{*Strict monotonicity in both arguments*}lemma mult_strict_mono:  assumes "a < b" and "c < d" and "0 < b" and "0 ≤ c"  shows "a * c < b * d"  using assms apply (cases "c=0")  apply (simp add: mult_pos_pos)  apply (erule mult_strict_right_mono [THEN less_trans])  apply (force simp add: le_less)  apply (erule mult_strict_left_mono, assumption)  donetext{*This weaker variant has more natural premises*}lemma mult_strict_mono':  assumes "a < b" and "c < d" and "0 ≤ a" and "0 ≤ c"  shows "a * c < b * d"by (rule mult_strict_mono) (insert assms, auto)lemma mult_less_le_imp_less:  assumes "a < b" and "c ≤ d" and "0 ≤ a" and "0 < c"  shows "a * c < b * d"  using assms apply (subgoal_tac "a * c < b * c")  apply (erule less_le_trans)  apply (erule mult_left_mono)  apply simp  apply (erule mult_strict_right_mono)  apply assumption  donelemma mult_le_less_imp_less:  assumes "a ≤ b" and "c < d" and "0 < a" and "0 ≤ c"  shows "a * c < b * d"  using assms apply (subgoal_tac "a * c ≤ b * c")  apply (erule le_less_trans)  apply (erule mult_strict_left_mono)  apply simp  apply (erule mult_right_mono)  apply simp  donelemma mult_less_imp_less_left:  assumes less: "c * a < c * b" and nonneg: "0 ≤ c"  shows "a < b"proof (rule ccontr)  assume "¬  a < b"  hence "b ≤ a" by (simp add: linorder_not_less)  hence "c * b ≤ c * a" using nonneg by (rule mult_left_mono)  with this and less show False by (simp add: not_less [symmetric])qedlemma mult_less_imp_less_right:  assumes less: "a * c < b * c" and nonneg: "0 ≤ c"  shows "a < b"proof (rule ccontr)  assume "¬ a < b"  hence "b ≤ a" by (simp add: linorder_not_less)  hence "b * c ≤ a * c" using nonneg by (rule mult_right_mono)  with this and less show False by (simp add: not_less [symmetric])qed  endclass linordered_semiring_1_strict = linordered_semiring_strict + semiring_1beginsubclass linordered_semiring_1 ..lemma convex_bound_lt:  assumes "x < a" "y < a" "0 ≤ u" "0 ≤ v" "u + v = 1"  shows "u * x + v * y < a"proof -  from assms have "u * x + v * y < u * a + v * a"    by (cases "u = 0")       (auto intro!: add_less_le_mono mult_strict_left_mono mult_left_mono)  thus ?thesis using assms unfolding distrib_right[symmetric] by simpqedendclass ordered_comm_semiring = comm_semiring_0 + ordered_ab_semigroup_add +   assumes comm_mult_left_mono: "a ≤ b ==> 0 ≤ c ==> c * a ≤ c * b"beginsubclass ordered_semiringproof  fix a b c :: 'a  assume "a ≤ b" "0 ≤ c"  thus "c * a ≤ c * b" by (rule comm_mult_left_mono)  thus "a * c ≤ b * c" by (simp only: mult_commute)qedendclass ordered_cancel_comm_semiring = ordered_comm_semiring + cancel_comm_monoid_addbeginsubclass comm_semiring_0_cancel ..subclass ordered_comm_semiring ..subclass ordered_cancel_semiring ..endclass linordered_comm_semiring_strict = comm_semiring_0 + linordered_cancel_ab_semigroup_add +  assumes comm_mult_strict_left_mono: "a < b ==> 0 < c ==> c * a < c * b"beginsubclass linordered_semiring_strictproof  fix a b c :: 'a  assume "a < b" "0 < c"  thus "c * a < c * b" by (rule comm_mult_strict_left_mono)  thus "a * c < b * c" by (simp only: mult_commute)qedsubclass ordered_cancel_comm_semiringproof  fix a b c :: 'a  assume "a ≤ b" "0 ≤ c"  thus "c * a ≤ c * b"    unfolding le_less    using mult_strict_left_mono by (cases "c = 0") autoqedendclass ordered_ring = ring + ordered_cancel_semiring beginsubclass ordered_ab_group_add ..lemma less_add_iff1:  "a * e + c < b * e + d <-> (a - b) * e + c < d"by (simp add: algebra_simps)lemma less_add_iff2:  "a * e + c < b * e + d <-> c < (b - a) * e + d"by (simp add: algebra_simps)lemma le_add_iff1:  "a * e + c ≤ b * e + d <-> (a - b) * e + c ≤ d"by (simp add: algebra_simps)lemma le_add_iff2:  "a * e + c ≤ b * e + d <-> c ≤ (b - a) * e + d"by (simp add: algebra_simps)lemma mult_left_mono_neg:  "b ≤ a ==> c ≤ 0 ==> c * a ≤ c * b"  apply (drule mult_left_mono [of _ _ "- c"])  apply simp_all  donelemma mult_right_mono_neg:  "b ≤ a ==> c ≤ 0 ==> a * c ≤ b * c"  apply (drule mult_right_mono [of _ _ "- c"])  apply simp_all  donelemma mult_nonpos_nonpos: "a ≤ 0 ==> b ≤ 0 ==> 0 ≤ a * b"using mult_right_mono_neg [of a 0 b] by simplemma split_mult_pos_le:  "(0 ≤ a ∧ 0 ≤ b) ∨ (a ≤ 0 ∧ b ≤ 0) ==> 0 ≤ a * b"by (auto simp add: mult_nonneg_nonneg mult_nonpos_nonpos)endclass linordered_ring = ring + linordered_semiring + linordered_ab_group_add + abs_ifbeginsubclass ordered_ring ..subclass ordered_ab_group_add_absproof  fix a b  show "¦a + b¦ ≤ ¦a¦ + ¦b¦"    by (auto simp add: abs_if not_less)    (auto simp del: minus_add_distrib simp add: minus_add_distrib [symmetric],     auto intro!: less_imp_le add_neg_neg)qed (auto simp add: abs_if)lemma zero_le_square [simp]: "0 ≤ a * a"  using linear [of 0 a]  by (auto simp add: mult_nonneg_nonneg mult_nonpos_nonpos)lemma not_square_less_zero [simp]: "¬ (a * a < 0)"  by (simp add: not_less)end(* The "strict" suffix can be seen as describing the combination of linordered_ring and no_zero_divisors.   Basically, linordered_ring + no_zero_divisors = linordered_ring_strict. *)class linordered_ring_strict = ring + linordered_semiring_strict  + ordered_ab_group_add + abs_ifbeginsubclass linordered_ring ..lemma mult_strict_left_mono_neg: "b < a ==> c < 0 ==> c * a < c * b"using mult_strict_left_mono [of b a "- c"] by simplemma mult_strict_right_mono_neg: "b < a ==> c < 0 ==> a * c < b * c"using mult_strict_right_mono [of b a "- c"] by simplemma mult_neg_neg: "a < 0 ==> b < 0 ==> 0 < a * b"using mult_strict_right_mono_neg [of a 0 b] by simpsubclass ring_no_zero_divisorsproof  fix a b  assume "a ≠ 0" then have A: "a < 0 ∨ 0 < a" by (simp add: neq_iff)  assume "b ≠ 0" then have B: "b < 0 ∨ 0 < b" by (simp add: neq_iff)  have "a * b < 0 ∨ 0 < a * b"  proof (cases "a < 0")    case True note A' = this    show ?thesis proof (cases "b < 0")      case True with A'      show ?thesis by (auto dest: mult_neg_neg)    next      case False with B have "0 < b" by auto      with A' show ?thesis by (auto dest: mult_strict_right_mono)    qed  next    case False with A have A': "0 < a" by auto    show ?thesis proof (cases "b < 0")      case True with A'      show ?thesis by (auto dest: mult_strict_right_mono_neg)    next      case False with B have "0 < b" by auto      with A' show ?thesis by (auto dest: mult_pos_pos)    qed  qed  then show "a * b ≠ 0" by (simp add: neq_iff)qedlemma zero_less_mult_iff:  "0 < a * b <-> 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0"  apply (auto simp add: mult_pos_pos mult_neg_neg)  apply (simp_all add: not_less le_less)  apply (erule disjE) apply assumption defer  apply (erule disjE) defer apply (drule sym) apply simp  apply (erule disjE) defer apply (drule sym) apply simp  apply (erule disjE) apply assumption apply (drule sym) apply simp  apply (drule sym) apply simp  apply (blast dest: zero_less_mult_pos)  apply (blast dest: zero_less_mult_pos2)  donelemma zero_le_mult_iff:  "0 ≤ a * b <-> 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0"by (auto simp add: eq_commute [of 0] le_less not_less zero_less_mult_iff)lemma mult_less_0_iff:  "a * b < 0 <-> 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b"  apply (insert zero_less_mult_iff [of "-a" b])  apply force  donelemma mult_le_0_iff:  "a * b ≤ 0 <-> 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b"  apply (insert zero_le_mult_iff [of "-a" b])   apply force  donetext{*Cancellation laws for @{term "c*a < c*b"} and @{term "a*c < b*c"},   also with the relations @{text "≤"} and equality.*}text{*These disjunction'' versions produce two cases when the comparison is an assumption, but effectively four when the comparison is a goal.*}lemma mult_less_cancel_right_disj:  "a * c < b * c <-> 0 < c ∧ a < b ∨ c < 0 ∧  b < a"  apply (cases "c = 0")  apply (auto simp add: neq_iff mult_strict_right_mono                       mult_strict_right_mono_neg)  apply (auto simp add: not_less                       not_le [symmetric, of "a*c"]                      not_le [symmetric, of a])  apply (erule_tac [!] notE)  apply (auto simp add: less_imp_le mult_right_mono                       mult_right_mono_neg)  donelemma mult_less_cancel_left_disj:  "c * a < c * b <-> 0 < c ∧ a < b ∨ c < 0 ∧  b < a"  apply (cases "c = 0")  apply (auto simp add: neq_iff mult_strict_left_mono                       mult_strict_left_mono_neg)  apply (auto simp add: not_less                       not_le [symmetric, of "c*a"]                      not_le [symmetric, of a])  apply (erule_tac [!] notE)  apply (auto simp add: less_imp_le mult_left_mono                       mult_left_mono_neg)  donetext{*The conjunction of implication'' lemmas produce two cases when thecomparison is a goal, but give four when the comparison is an assumption.*}lemma mult_less_cancel_right:  "a * c < b * c <-> (0 ≤ c --> a < b) ∧ (c ≤ 0 --> b < a)"  using mult_less_cancel_right_disj [of a c b] by autolemma mult_less_cancel_left:  "c * a < c * b <-> (0 ≤ c --> a < b) ∧ (c ≤ 0 --> b < a)"  using mult_less_cancel_left_disj [of c a b] by autolemma mult_le_cancel_right:   "a * c ≤ b * c <-> (0 < c --> a ≤ b) ∧ (c < 0 --> b ≤ a)"by (simp add: not_less [symmetric] mult_less_cancel_right_disj)lemma mult_le_cancel_left:  "c * a ≤ c * b <-> (0 < c --> a ≤ b) ∧ (c < 0 --> b ≤ a)"by (simp add: not_less [symmetric] mult_less_cancel_left_disj)lemma mult_le_cancel_left_pos:  "0 < c ==> c * a ≤ c * b <-> a ≤ b"by (auto simp: mult_le_cancel_left)lemma mult_le_cancel_left_neg:  "c < 0 ==> c * a ≤ c * b <-> b ≤ a"by (auto simp: mult_le_cancel_left)lemma mult_less_cancel_left_pos:  "0 < c ==> c * a < c * b <-> a < b"by (auto simp: mult_less_cancel_left)lemma mult_less_cancel_left_neg:  "c < 0 ==> c * a < c * b <-> b < a"by (auto simp: mult_less_cancel_left)endlemmas mult_sign_intros =  mult_nonneg_nonneg mult_nonneg_nonpos  mult_nonpos_nonneg mult_nonpos_nonpos  mult_pos_pos mult_pos_neg  mult_neg_pos mult_neg_negclass ordered_comm_ring = comm_ring + ordered_comm_semiringbeginsubclass ordered_ring ..subclass ordered_cancel_comm_semiring ..endclass linordered_semidom = comm_semiring_1_cancel + linordered_comm_semiring_strict +  (*previously linordered_semiring*)  assumes zero_less_one [simp]: "0 < 1"beginlemma pos_add_strict:  shows "0 < a ==> b < c ==> b < a + c"  using add_strict_mono [of 0 a b c] by simplemma zero_le_one [simp]: "0 ≤ 1"by (rule zero_less_one [THEN less_imp_le]) lemma not_one_le_zero [simp]: "¬ 1 ≤ 0"by (simp add: not_le) lemma not_one_less_zero [simp]: "¬ 1 < 0"by (simp add: not_less) lemma less_1_mult:  assumes "1 < m" and "1 < n"  shows "1 < m * n"  using assms mult_strict_mono [of 1 m 1 n]    by (simp add:  less_trans [OF zero_less_one]) endclass linordered_idom = comm_ring_1 +  linordered_comm_semiring_strict + ordered_ab_group_add +  abs_if + sgn_if  (*previously linordered_ring*)beginsubclass linordered_semiring_1_strict ..subclass linordered_ring_strict ..subclass ordered_comm_ring ..subclass idom ..subclass linordered_semidomproof  have "0 ≤ 1 * 1" by (rule zero_le_square)  thus "0 < 1" by (simp add: le_less)qed lemma linorder_neqE_linordered_idom:  assumes "x ≠ y" obtains "x < y" | "y < x"  using assms by (rule neqE)text {* These cancellation simprules also produce two cases when the comparison is a goal. *}lemma mult_le_cancel_right1:  "c ≤ b * c <-> (0 < c --> 1 ≤ b) ∧ (c < 0 --> b ≤ 1)"by (insert mult_le_cancel_right [of 1 c b], simp)lemma mult_le_cancel_right2:  "a * c ≤ c <-> (0 < c --> a ≤ 1) ∧ (c < 0 --> 1 ≤ a)"by (insert mult_le_cancel_right [of a c 1], simp)lemma mult_le_cancel_left1:  "c ≤ c * b <-> (0 < c --> 1 ≤ b) ∧ (c < 0 --> b ≤ 1)"by (insert mult_le_cancel_left [of c 1 b], simp)lemma mult_le_cancel_left2:  "c * a ≤ c <-> (0 < c --> a ≤ 1) ∧ (c < 0 --> 1 ≤ a)"by (insert mult_le_cancel_left [of c a 1], simp)lemma mult_less_cancel_right1:  "c < b * c <-> (0 ≤ c --> 1 < b) ∧ (c ≤ 0 --> b < 1)"by (insert mult_less_cancel_right [of 1 c b], simp)lemma mult_less_cancel_right2:  "a * c < c <-> (0 ≤ c --> a < 1) ∧ (c ≤ 0 --> 1 < a)"by (insert mult_less_cancel_right [of a c 1], simp)lemma mult_less_cancel_left1:  "c < c * b <-> (0 ≤ c --> 1 < b) ∧ (c ≤ 0 --> b < 1)"by (insert mult_less_cancel_left [of c 1 b], simp)lemma mult_less_cancel_left2:  "c * a < c <-> (0 ≤ c --> a < 1) ∧ (c ≤ 0 --> 1 < a)"by (insert mult_less_cancel_left [of c a 1], simp)lemma sgn_sgn [simp]:  "sgn (sgn a) = sgn a"unfolding sgn_if by simplemma sgn_0_0:  "sgn a = 0 <-> a = 0"unfolding sgn_if by simplemma sgn_1_pos:  "sgn a = 1 <-> a > 0"unfolding sgn_if by simplemma sgn_1_neg:  "sgn a = - 1 <-> a < 0"unfolding sgn_if by autolemma sgn_pos [simp]:  "0 < a ==> sgn a = 1"unfolding sgn_1_pos .lemma sgn_neg [simp]:  "a < 0 ==> sgn a = - 1"unfolding sgn_1_neg .lemma sgn_times:  "sgn (a * b) = sgn a * sgn b"by (auto simp add: sgn_if zero_less_mult_iff)lemma abs_sgn: "¦k¦ = k * sgn k"unfolding sgn_if abs_if by autolemma sgn_greater [simp]:  "0 < sgn a <-> 0 < a"  unfolding sgn_if by autolemma sgn_less [simp]:  "sgn a < 0 <-> a < 0"  unfolding sgn_if by autolemma abs_dvd_iff [simp]: "¦m¦ dvd k <-> m dvd k"  by (simp add: abs_if)lemma dvd_abs_iff [simp]: "m dvd ¦k¦ <-> m dvd k"  by (simp add: abs_if)lemma dvd_if_abs_eq:  "¦l¦ = ¦k¦ ==> l dvd k"by(subst abs_dvd_iff[symmetric]) simpendtext {* Simprules for comparisons where common factors can be cancelled. *}lemmas mult_compare_simps[no_atp] =    mult_le_cancel_right mult_le_cancel_left    mult_le_cancel_right1 mult_le_cancel_right2    mult_le_cancel_left1 mult_le_cancel_left2    mult_less_cancel_right mult_less_cancel_left    mult_less_cancel_right1 mult_less_cancel_right2    mult_less_cancel_left1 mult_less_cancel_left2    mult_cancel_right mult_cancel_left    mult_cancel_right1 mult_cancel_right2    mult_cancel_left1 mult_cancel_left2text {* Reasoning about inequalities with division *}context linordered_semidombeginlemma less_add_one: "a < a + 1"proof -  have "a + 0 < a + 1"    by (blast intro: zero_less_one add_strict_left_mono)  thus ?thesis by simpqedlemma zero_less_two: "0 < 1 + 1"by (blast intro: less_trans zero_less_one less_add_one)endcontext linordered_idombeginlemma mult_right_le_one_le:  "0 ≤ x ==> 0 ≤ y ==> y ≤ 1 ==> x * y ≤ x"  by (auto simp add: mult_le_cancel_left2)lemma mult_left_le_one_le:  "0 ≤ x ==> 0 ≤ y ==> y ≤ 1 ==> y * x ≤ x"  by (auto simp add: mult_le_cancel_right2)endtext {* Absolute Value *}context linordered_idombeginlemma mult_sgn_abs:  "sgn x * ¦x¦ = x"  unfolding abs_if sgn_if by autolemma abs_one [simp]:  "¦1¦ = 1"  by (simp add: abs_if)endclass ordered_ring_abs = ordered_ring + ordered_ab_group_add_abs +  assumes abs_eq_mult:    "(0 ≤ a ∨ a ≤ 0) ∧ (0 ≤ b ∨ b ≤ 0) ==> ¦a * b¦ = ¦a¦ * ¦b¦"context linordered_idombeginsubclass ordered_ring_abs proofqed (auto simp add: abs_if not_less mult_less_0_iff)lemma abs_mult:  "¦a * b¦ = ¦a¦ * ¦b¦"   by (rule abs_eq_mult) autolemma abs_mult_self:  "¦a¦ * ¦a¦ = a * a"  by (simp add: abs_if) lemma abs_mult_less:  "¦a¦ < c ==> ¦b¦ < d ==> ¦a¦ * ¦b¦ < c * d"proof -  assume ac: "¦a¦ < c"  hence cpos: "0<c" by (blast intro: le_less_trans abs_ge_zero)  assume "¦b¦ < d"  thus ?thesis by (simp add: ac cpos mult_strict_mono) qedlemma less_minus_self_iff:  "a < - a <-> a < 0"  by (simp only: less_le less_eq_neg_nonpos equal_neg_zero)lemma abs_less_iff:  "¦a¦ < b <-> a < b ∧ - a < b"   by (simp add: less_le abs_le_iff) (auto simp add: abs_if)lemma abs_mult_pos:  "0 ≤ x ==> ¦y¦ * x = ¦y * x¦"  by (simp add: abs_mult)endcode_modulename SML  Rings Arithcode_modulename OCaml  Rings Arithcode_modulename Haskell  Rings Arithend