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.48 +lemma div_add1_eq:
    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