src/HOL/Euclidean_Division.thy
 changeset 66807 c3631f32dfeb parent 66806 a4e82b58d833 child 66808 1907167b6038
```     1.1 --- a/src/HOL/Euclidean_Division.thy	Sun Oct 08 22:28:21 2017 +0200
1.2 +++ b/src/HOL/Euclidean_Division.thy	Sun Oct 08 22:28:21 2017 +0200
1.3 @@ -9,82 +9,6 @@
1.4    imports Nat_Transfer
1.5  begin
1.6
1.7 -subsection \<open>Quotient and remainder in integral domains\<close>
1.8 -
1.9 -class semidom_modulo = algebraic_semidom + semiring_modulo
1.10 -begin
1.11 -
1.12 -lemma mod_0 [simp]: "0 mod a = 0"
1.13 -  using div_mult_mod_eq [of 0 a] by simp
1.14 -
1.15 -lemma mod_by_0 [simp]: "a mod 0 = a"
1.16 -  using div_mult_mod_eq [of a 0] by simp
1.17 -
1.18 -lemma mod_by_1 [simp]:
1.19 -  "a mod 1 = 0"
1.20 -proof -
1.21 -  from div_mult_mod_eq [of a one] div_by_1 have "a + a mod 1 = a" by simp
1.22 -  then have "a + a mod 1 = a + 0" by simp
1.23 -  then show ?thesis by (rule add_left_imp_eq)
1.24 -qed
1.25 -
1.26 -lemma mod_self [simp]:
1.27 -  "a mod a = 0"
1.28 -  using div_mult_mod_eq [of a a] by simp
1.29 -
1.30 -lemma dvd_imp_mod_0 [simp]:
1.31 -  assumes "a dvd b"
1.32 -  shows "b mod a = 0"
1.33 -  using assms minus_div_mult_eq_mod [of b a] by simp
1.34 -
1.35 -lemma mod_0_imp_dvd:
1.36 -  assumes "a mod b = 0"
1.37 -  shows   "b dvd a"
1.38 -proof -
1.39 -  have "b dvd ((a div b) * b)" by simp
1.40 -  also have "(a div b) * b = a"
1.41 -    using div_mult_mod_eq [of a b] by (simp add: assms)
1.42 -  finally show ?thesis .
1.43 -qed
1.44 -
1.45 -lemma mod_eq_0_iff_dvd:
1.46 -  "a mod b = 0 \<longleftrightarrow> b dvd a"
1.47 -  by (auto intro: mod_0_imp_dvd)
1.48 -
1.49 -lemma dvd_eq_mod_eq_0 [nitpick_unfold, code]:
1.50 -  "a dvd b \<longleftrightarrow> b mod a = 0"
1.51 -  by (simp add: mod_eq_0_iff_dvd)
1.52 -
1.53 -lemma dvd_mod_iff:
1.54 -  assumes "c dvd b"
1.55 -  shows "c dvd a mod b \<longleftrightarrow> c dvd a"
1.56 -proof -
1.57 -  from assms have "(c dvd a mod b) \<longleftrightarrow> (c dvd ((a div b) * b + a mod b))"
1.59 -  also have "(a div b) * b + a mod b = a"
1.60 -    using div_mult_mod_eq [of a b] by simp
1.61 -  finally show ?thesis .
1.62 -qed
1.63 -
1.64 -lemma dvd_mod_imp_dvd:
1.65 -  assumes "c dvd a mod b" and "c dvd b"
1.66 -  shows "c dvd a"
1.67 -  using assms dvd_mod_iff [of c b a] by simp
1.68 -
1.69 -end
1.70 -
1.71 -class idom_modulo = idom + semidom_modulo
1.72 -begin
1.73 -
1.74 -subclass idom_divide ..
1.75 -
1.76 -lemma div_diff [simp]:
1.77 -  "c dvd a \<Longrightarrow> c dvd b \<Longrightarrow> (a - b) div c = a div c - b div c"
1.78 -  using div_add [of _  _ "- b"] by (simp add: dvd_neg_div)
1.79 -
1.80 -end
1.81 -
1.82 -
1.83  subsection \<open>Euclidean (semi)rings with explicit division and remainder\<close>
1.84
1.85  class euclidean_semiring = semidom_modulo + normalization_semidom +
```