src/HOL/Divides.thy
 changeset 64164 38c407446400 parent 64014 ca1239a3277b child 64238 b60a9752b6d0
```     1.1 --- a/src/HOL/Divides.thy	Tue Oct 11 16:44:13 2016 +0200
1.2 +++ b/src/HOL/Divides.thy	Wed Oct 12 20:38:47 2016 +0200
1.3 @@ -11,9 +11,8 @@
1.4
1.5  subsection \<open>Abstract division in commutative semirings.\<close>
1.6
1.7 -class semiring_div = semidom + modulo +
1.8 -  assumes mod_div_equality: "a div b * b + a mod b = a"
1.9 -    and div_by_0: "a div 0 = 0"
1.10 +class semiring_div = semidom + semiring_modulo +
1.11 +  assumes div_by_0: "a div 0 = 0"
1.12      and div_0: "0 div a = 0"
1.13      and div_mult_self1 [simp]: "b \<noteq> 0 \<Longrightarrow> (a + c * b) div b = c + a div b"
1.14      and div_mult_mult1 [simp]: "c \<noteq> 0 \<Longrightarrow> (c * a) div (c * b) = a div b"
1.15 @@ -41,14 +40,6 @@
1.16
1.17  text \<open>@{const divide} and @{const modulo}\<close>
1.18
1.19 -lemma mod_div_equality2: "b * (a div b) + a mod b = a"
1.20 -  unfolding mult.commute [of b]
1.21 -  by (rule mod_div_equality)
1.22 -
1.23 -lemma mod_div_equality': "a mod b + a div b * b = a"
1.24 -  using mod_div_equality [of a b]
1.25 -  by (simp only: ac_simps)
1.26 -
1.27  lemma div_mod_equality: "((a div b) * b + a mod b) + c = a + c"
1.28    by (simp add: mod_div_equality)
1.29
1.30 @@ -143,17 +134,6 @@
1.31    "(a + b) mod b = a mod b"
1.32    using mod_mult_self1 [of a 1 b] by simp
1.33
1.34 -lemma mod_div_decomp:
1.35 -  fixes a b
1.36 -  obtains q r where "q = a div b" and "r = a mod b"
1.37 -    and "a = q * b + r"
1.38 -proof -
1.39 -  from mod_div_equality have "a = a div b * b + a mod b" by simp
1.40 -  moreover have "a div b = a div b" ..
1.41 -  moreover have "a mod b = a mod b" ..
1.42 -  note that ultimately show thesis by blast
1.43 -qed
1.44 -
1.45  lemma dvd_imp_mod_0 [simp]:
1.46    assumes "a dvd b"
1.47    shows "b mod a = 0"
1.48 @@ -189,7 +169,7 @@
1.49    hence "a div b + a mod b div b = (a mod b + a div b * b) div b"
1.50      by (rule div_mult_self1 [symmetric])
1.51    also have "\<dots> = a div b"
1.52 -    by (simp only: mod_div_equality')
1.53 +    by (simp only: mod_div_equality3)
1.54    also have "\<dots> = a div b + 0"
1.55      by simp
1.56    finally show ?thesis
1.57 @@ -202,7 +182,7 @@
1.58    have "a mod b mod b = (a mod b + a div b * b) mod b"
1.59      by (simp only: mod_mult_self1)
1.60    also have "\<dots> = a mod b"
1.61 -    by (simp only: mod_div_equality')
1.62 +    by (simp only: mod_div_equality3)
1.63    finally show ?thesis .
1.64  qed
1.65
```