src/HOL/Rings.thy
changeset 60867 86e7560e07d0
parent 60758 d8d85a8172b5
child 61649 268d88ec9087
     1.1 --- a/src/HOL/Rings.thy	Thu Aug 06 19:12:09 2015 +0200
     1.2 +++ b/src/HOL/Rings.thy	Thu Aug 06 23:56:48 2015 +0200
     1.3 @@ -633,6 +633,20 @@
     1.4    "a div 1 = a"
     1.5    using nonzero_mult_divide_cancel_left [of 1 a] by simp
     1.6  
     1.7 +end
     1.8 +
     1.9 +class idom_divide = idom + semidom_divide
    1.10 +
    1.11 +class algebraic_semidom = semidom_divide
    1.12 +begin
    1.13 +
    1.14 +text \<open>
    1.15 +  Class @{class algebraic_semidom} enriches a integral domain
    1.16 +  by notions from algebra, like units in a ring.
    1.17 +  It is a separate class to avoid spoiling fields with notions
    1.18 +  which are degenerated there.
    1.19 +\<close>
    1.20 +
    1.21  lemma dvd_times_left_cancel_iff [simp]:
    1.22    assumes "a \<noteq> 0"
    1.23    shows "a * b dvd a * c \<longleftrightarrow> b dvd c" (is "?P \<longleftrightarrow> ?Q")
    1.24 @@ -667,19 +681,60 @@
    1.25    with \<open>c \<noteq> 0\<close> show ?thesis by (simp add: mult.commute [of a])
    1.26  qed
    1.27  
    1.28 -end
    1.29 +lemma div_dvd_div [simp]:
    1.30 +  assumes "a dvd b" and "a dvd c"
    1.31 +  shows "b div a dvd c div a \<longleftrightarrow> b dvd c"
    1.32 +proof (cases "a = 0")
    1.33 +  case True with assms show ?thesis by simp
    1.34 +next
    1.35 +  case False
    1.36 +  moreover from assms obtain k l where "b = a * k" and "c = a * l"
    1.37 +    by (auto elim!: dvdE)
    1.38 +  ultimately show ?thesis by simp
    1.39 +qed
    1.40  
    1.41 -class idom_divide = idom + semidom_divide
    1.42 -
    1.43 -class algebraic_semidom = semidom_divide
    1.44 -begin
    1.45 +lemma div_add [simp]:
    1.46 +  assumes "c dvd a" and "c dvd b"
    1.47 +  shows "(a + b) div c = a div c + b div c"
    1.48 +proof (cases "c = 0")
    1.49 +  case True then show ?thesis by simp
    1.50 +next
    1.51 +  case False
    1.52 +  moreover from assms obtain k l where "a = c * k" and "b = c * l"
    1.53 +    by (auto elim!: dvdE)
    1.54 +  moreover have "c * k + c * l = c * (k + l)"
    1.55 +    by (simp add: algebra_simps)
    1.56 +  ultimately show ?thesis
    1.57 +    by simp
    1.58 +qed
    1.59  
    1.60 -text \<open>
    1.61 -  Class @{class algebraic_semidom} enriches a integral domain
    1.62 -  by notions from algebra, like units in a ring.
    1.63 -  It is a separate class to avoid spoiling fields with notions
    1.64 -  which are degenerated there.
    1.65 -\<close>
    1.66 +lemma div_mult_div_if_dvd:
    1.67 +  assumes "b dvd a" and "d dvd c"
    1.68 +  shows "(a div b) * (c div d) = (a * c) div (b * d)"
    1.69 +proof (cases "b = 0 \<or> c = 0")
    1.70 +  case True with assms show ?thesis by auto
    1.71 +next
    1.72 +  case False
    1.73 +  moreover from assms obtain k l where "a = b * k" and "c = d * l"
    1.74 +    by (auto elim!: dvdE)
    1.75 +  moreover have "b * k * (d * l) div (b * d) = (b * d) * (k * l) div (b * d)"
    1.76 +    by (simp add: ac_simps)
    1.77 +  ultimately show ?thesis by simp
    1.78 +qed
    1.79 +
    1.80 +lemma dvd_div_eq_mult:
    1.81 +  assumes "a \<noteq> 0" and "a dvd b"
    1.82 +  shows "b div a = c \<longleftrightarrow> b = c * a"
    1.83 +proof
    1.84 +  assume "b = c * a"
    1.85 +  then show "b div a = c" by (simp add: assms)
    1.86 +next
    1.87 +  assume "b div a = c"
    1.88 +  then have "b div a * a = c * a" by simp
    1.89 +  moreover from \<open>a \<noteq> 0\<close> \<open>a dvd b\<close> have "b div a * a = b"
    1.90 +    by (auto elim!: dvdE simp add: ac_simps)
    1.91 +  ultimately show "b = c * a" by simp
    1.92 +qed
    1.93  
    1.94  lemma dvd_div_mult_self [simp]:
    1.95    "a dvd b \<Longrightarrow> b div a * a = b"
    1.96 @@ -716,6 +771,22 @@
    1.97      by (cases "b = 0 \<or> c = 0") (auto, simp add: ac_simps)
    1.98  qed
    1.99  
   1.100 +lemma dvd_div_div_eq_mult:
   1.101 +  assumes "a \<noteq> 0" "c \<noteq> 0" and "a dvd b" "c dvd d"
   1.102 +  shows "b div a = d div c \<longleftrightarrow> b * c = a * d" (is "?P \<longleftrightarrow> ?Q")
   1.103 +proof -
   1.104 +  from assms have "a * c \<noteq> 0" by simp
   1.105 +  then have "?P \<longleftrightarrow> b div a * (a * c) = d div c * (a * c)"
   1.106 +    by simp
   1.107 +  also have "\<dots> \<longleftrightarrow> (a * (b div a)) * c = (c * (d div c)) * a"
   1.108 +    by (simp add: ac_simps)
   1.109 +  also have "\<dots> \<longleftrightarrow> (a * b div a) * c = (c * d div c) * a"
   1.110 +    using assms by (simp add: div_mult_swap)
   1.111 +  also have "\<dots> \<longleftrightarrow> ?Q"
   1.112 +    using assms by (simp add: ac_simps)
   1.113 +  finally show ?thesis .
   1.114 +qed
   1.115 +
   1.116  
   1.117  text \<open>Units: invertible elements in a ring\<close>
   1.118