src/HOL/Euclidean_Division.thy
 changeset 66814 a24cde9588bb parent 66813 351142796345 child 66816 212a3334e7da
```     1.1 --- a/src/HOL/Euclidean_Division.thy	Sun Oct 08 22:28:22 2017 +0200
1.2 +++ b/src/HOL/Euclidean_Division.thy	Sun Oct 08 22:28:22 2017 +0200
1.3 @@ -531,9 +531,10 @@
1.4        and "a div b = q"
1.5        and "a mod b = 0"
1.6        and "a = q * b"
1.7 -  | (remainder) q r where "b \<noteq> 0" and "r \<noteq> 0"
1.8 +  | (remainder) q r where "b \<noteq> 0"
1.9        and "uniqueness_constraint r b"
1.10        and "euclidean_size r < euclidean_size b"
1.11 +      and "r \<noteq> 0"
1.12        and "a div b = q"
1.13        and "a mod b = r"
1.14        and "a = q * b + r"
1.15 @@ -630,6 +631,67 @@
1.16    qed
1.17  qed
1.18
1.19 +lemma div_mult1_eq:
1.20 +  "(a * b) div c = a * (b div c) + a * (b mod c) div c"
1.21 +proof (cases "a * (b mod c)" c rule: divmod_cases)
1.22 +  case (divides q)
1.23 +  have "a * b = a * (b div c * c + b mod c)"
1.24 +    by (simp add: div_mult_mod_eq)
1.25 +  also have "\<dots> = (a * (b div c) + q) * c"
1.26 +    using divides by (simp add: algebra_simps)
1.27 +  finally have "(a * b) div c = \<dots> div c"
1.28 +    by simp
1.29 +  with divides show ?thesis
1.30 +    by simp
1.31 +next
1.32 +  case (remainder q r)
1.33 +  from remainder(1-3) show ?thesis
1.34 +  proof (rule div_eqI)
1.35 +    have "a * b = a * (b div c * c + b mod c)"
1.36 +      by (simp add: div_mult_mod_eq)
1.37 +    also have "\<dots> = a * c * (b div c) + q * c + r"
1.38 +      using remainder by (simp add: algebra_simps)
1.39 +    finally show "(a * (b div c) + a * (b mod c) div c) * c + r = a * b"
1.40 +      using remainder(5-7) by (simp add: algebra_simps)
1.41 +  qed
1.42 +next
1.43 +  case by0
1.44 +  then show ?thesis
1.45 +    by simp
1.46 +qed
1.47 +
1.49 +  "(a + b) div c = a div c + b div c + (a mod c + b mod c) div c"
1.50 +proof (cases "a mod c + b mod c" c rule: divmod_cases)
1.51 +  case (divides q)
1.52 +  have "a + b = (a div c * c + a mod c) + (b div c * c + b mod c)"
1.53 +    using mod_mult_div_eq [of a c] mod_mult_div_eq [of b c] by (simp add: ac_simps)
1.54 +  also have "\<dots> = (a div c + b div c) * c + (a mod c + b mod c)"
1.55 +    by (simp add: algebra_simps)
1.56 +  also have "\<dots> = (a div c + b div c + q) * c"
1.57 +    using divides by (simp add: algebra_simps)
1.58 +  finally have "(a + b) div c = (a div c + b div c + q) * c div c"
1.59 +    by simp
1.60 +  with divides show ?thesis
1.61 +    by simp
1.62 +next
1.63 +  case (remainder q r)
1.64 +  from remainder(1-3) show ?thesis
1.65 +  proof (rule div_eqI)
1.66 +    have "(a div c + b div c + q) * c + r + (a mod c + b mod c) =
1.67 +        (a div c * c + a mod c) + (b div c * c + b mod c) + q * c + r"
1.68 +      by (simp add: algebra_simps)
1.69 +    also have "\<dots> = a + b + (a mod c + b mod c)"
1.70 +      by (simp add: div_mult_mod_eq remainder) (simp add: ac_simps)
1.71 +    finally show "(a div c + b div c + (a mod c + b mod c) div c) * c + r = a + b"
1.72 +      using remainder by simp
1.73 +  qed
1.74 +next
1.75 +  case by0
1.76 +  then show ?thesis
1.77 +    by simp
1.78 +qed
1.79 +
1.80  end
1.81
1.82  class unique_euclidean_ring = euclidean_ring + unique_euclidean_semiring
1.83 @@ -947,23 +1009,6 @@
1.84    and Suc_mod_mult_self4 [simp]: "Suc (n * k + m) mod n = Suc m mod n"
1.85    by (subst mod_Suc_eq [symmetric], simp add: mod_simps)+
1.86
1.87 -lemma div_mult1_eq: -- \<open>TODO: Generalization candidate\<close>
1.88 -  "(a * b) div c = a * (b div c) + a * (b mod c) div c" for a b c :: nat
1.89 -  apply (cases "c = 0")
1.90 -   apply simp
1.91 -  apply (rule div_eqI [of _ "(a * (b mod c)) mod c"])
1.92 -     apply (auto simp add: algebra_simps distrib_left [symmetric])
1.93 -  done
1.94 -
1.95 -lemma div_add1_eq: -- \<open>NOT suitable for rewriting: the RHS has an instance of the LHS\<close>
1.96 -   -- \<open>TODO: Generalization candidate\<close>
1.97 -  "(a + b) div c = a div c + b div c + ((a mod c + b mod c) div c)" for a b c :: nat
1.98 -  apply (cases "c = 0")
1.99 -   apply simp
1.100 -  apply (rule div_eqI [of _ "(a mod c + b mod c) mod c"])
1.101 -  apply (auto simp add: algebra_simps)
1.102 -  done
1.103 -
1.104  context
1.105    fixes m n q :: nat
1.106  begin
```