--- a/src/HOL/Rings.thy Sat Dec 17 15:22:13 2016 +0100
+++ b/src/HOL/Rings.thy Sat Dec 17 15:22:13 2016 +0100
@@ -713,9 +713,41 @@
lemma div_by_1 [simp]: "a div 1 = a"
using nonzero_mult_div_cancel_left [of 1 a] by simp
+lemma dvd_div_eq_0_iff:
+ assumes "b dvd a"
+ shows "a div b = 0 \<longleftrightarrow> a = 0"
+ using assms by (elim dvdE, cases "b = 0") simp_all
+
+lemma dvd_div_eq_cancel:
+ "a div c = b div c \<Longrightarrow> c dvd a \<Longrightarrow> c dvd b \<Longrightarrow> a = b"
+ by (elim dvdE, cases "c = 0") simp_all
+
+lemma dvd_div_eq_iff:
+ "c dvd a \<Longrightarrow> c dvd b \<Longrightarrow> a div c = b div c \<longleftrightarrow> a = b"
+ by (elim dvdE, cases "c = 0") simp_all
+
end
class idom_divide = idom + semidom_divide
+begin
+
+lemma dvd_neg_div':
+ assumes "b dvd a"
+ shows "- a div b = - (a div b)"
+proof (cases "b = 0")
+ case True
+ then show ?thesis by simp
+next
+ case False
+ from assms obtain c where "a = b * c" ..
+ moreover from False have "b * - c div b = - (b * c div b)"
+ using nonzero_mult_div_cancel_left [of b "- c"]
+ by simp
+ ultimately show ?thesis
+ by simp
+qed
+
+end
class algebraic_semidom = semidom_divide
begin
@@ -1060,6 +1092,15 @@
shows "a div (b * a) = 1 div b"
using assms is_unit_div_mult_cancel_left [of a b] by (simp add: ac_simps)
+lemma unit_div_eq_0_iff:
+ assumes "is_unit b"
+ shows "a div b = 0 \<longleftrightarrow> a = 0"
+ by (rule dvd_div_eq_0_iff) (insert assms, auto)
+
+lemma div_mult_unit2:
+ "is_unit c \<Longrightarrow> b dvd a \<Longrightarrow> a div (b * c) = a div b div c"
+ by (rule dvd_div_mult2_eq) (simp_all add: mult_unit_dvd_iff)
+
end
class normalization_semidom = algebraic_semidom +
@@ -1373,6 +1414,17 @@
by simp
qed
+lemma normalize_unit_factor_eqI:
+ assumes "normalize a = normalize b"
+ and "unit_factor a = unit_factor b"
+ shows "a = b"
+proof -
+ from assms have "unit_factor a * normalize a = unit_factor b * normalize b"
+ by simp
+ then show ?thesis
+ by simp
+qed
+
end