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