src/HOL/Rings.thy
 changeset 60570 7ed2cde6806d parent 60562 24af00b010cf child 60615 e5fa1d5d3952
```     1.1 --- a/src/HOL/Rings.thy	Thu Jun 25 15:01:41 2015 +0200
1.2 +++ b/src/HOL/Rings.thy	Thu Jun 25 15:01:42 2015 +0200
1.3 @@ -619,6 +619,16 @@
1.4    shows "a div a = 1"
1.5    using assms nonzero_mult_divide_cancel_left [of a 1] by simp
1.6
1.7 +lemma divide_zero_left [simp]:
1.8 +  "0 div a = 0"
1.9 +proof (cases "a = 0")
1.10 +  case True then show ?thesis by simp
1.11 +next
1.12 +  case False then have "a * 0 div a = 0"
1.13 +    by (rule nonzero_mult_divide_cancel_left)
1.14 +  then show ?thesis by simp
1.15 +qed
1.16 +
1.17  end
1.18
1.19  class idom_divide = idom + semidom_divide
1.20 @@ -651,6 +661,16 @@
1.21    shows "b div c * a = (b * a) div c"
1.22    using assms div_mult_swap [of c b a] by (simp add: ac_simps)
1.23
1.24 +lemma dvd_div_mult2_eq:
1.25 +  assumes "b * c dvd a"
1.26 +  shows "a div (b * c) = a div b div c"
1.27 +using assms proof
1.28 +  fix k
1.29 +  assume "a = b * c * k"
1.30 +  then show ?thesis
1.31 +    by (cases "b = 0 \<or> c = 0") (auto, simp add: ac_simps)
1.32 +qed
1.33 +
1.34
1.35  text \<open>Units: invertible elements in a ring\<close>
1.36
1.37 @@ -803,6 +823,17 @@
1.38    with assms show ?thesis by simp
1.39  qed
1.40
1.41 +lemma is_unit_div_mult2_eq:
1.42 +  assumes "is_unit b" and "is_unit c"
1.43 +  shows "a div (b * c) = a div b div c"
1.44 +proof -
1.45 +  from assms have "is_unit (b * c)" by (simp add: unit_prod)
1.46 +  then have "b * c dvd a"
1.47 +    by (rule unit_imp_dvd)
1.48 +  then show ?thesis
1.49 +    by (rule dvd_div_mult2_eq)
1.50 +qed
1.51 +
1.52
1.53  text \<open>Associated elements in a ring --- an equivalence relation induced
1.54    by the quasi-order divisibility.\<close>
```