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>