src/HOL/Rings.thy
 changeset 60570 7ed2cde6806d parent 60562 24af00b010cf child 60615 e5fa1d5d3952
```--- a/src/HOL/Rings.thy	Thu Jun 25 15:01:41 2015 +0200
+++ b/src/HOL/Rings.thy	Thu Jun 25 15:01:42 2015 +0200
@@ -619,6 +619,16 @@
shows "a div a = 1"
using assms nonzero_mult_divide_cancel_left [of a 1] by simp

+lemma divide_zero_left [simp]:
+  "0 div a = 0"
+proof (cases "a = 0")
+  case True then show ?thesis by simp
+next
+  case False then have "a * 0 div a = 0"
+    by (rule nonzero_mult_divide_cancel_left)
+  then show ?thesis by simp
+qed
+
end

class idom_divide = idom + semidom_divide
@@ -651,6 +661,16 @@
shows "b div c * a = (b * a) div c"
using assms div_mult_swap [of c b a] by (simp add: ac_simps)

+lemma dvd_div_mult2_eq:
+  assumes "b * c dvd a"
+  shows "a div (b * c) = a div b div c"
+using assms proof
+  fix k
+  assume "a = b * c * k"
+  then show ?thesis
+    by (cases "b = 0 \<or> c = 0") (auto, simp add: ac_simps)
+qed
+

text \<open>Units: invertible elements in a ring\<close>

@@ -803,6 +823,17 @@
with assms show ?thesis by simp
qed

+lemma is_unit_div_mult2_eq:
+  assumes "is_unit b" and "is_unit c"
+  shows "a div (b * c) = a div b div c"
+proof -
+  from assms have "is_unit (b * c)" by (simp add: unit_prod)
+  then have "b * c dvd a"
+    by (rule unit_imp_dvd)
+  then show ?thesis
+    by (rule dvd_div_mult2_eq)
+qed
+

text \<open>Associated elements in a ring --- an equivalence relation induced
by the quasi-order divisibility.\<close>```