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
```