generalized some rules
authorhaftmann
Sun Oct 08 22:28:22 2017 +0200 (19 months ago)
changeset 66814a24cde9588bb
parent 66813 351142796345
child 66815 93c6632ddf44
generalized some rules
src/HOL/Divides.thy
src/HOL/Euclidean_Division.thy
     1.1 --- a/src/HOL/Divides.thy	Sun Oct 08 22:28:22 2017 +0200
     1.2 +++ b/src/HOL/Divides.thy	Sun Oct 08 22:28:22 2017 +0200
     1.3 @@ -838,31 +838,13 @@
     1.4  
     1.5  subsubsection \<open>More Algebraic Laws for div and mod\<close>
     1.6  
     1.7 -text\<open>proving (a*b) div c = a * (b div c) + a * (b mod c)\<close>
     1.8 -
     1.9 -lemma zmult1_lemma:
    1.10 -     "[| eucl_rel_int b c (q, r) |]
    1.11 -      ==> eucl_rel_int (a * b) c (a*q + a*r div c, a*r mod c)"
    1.12 -by (auto simp add: split_ifs eucl_rel_int_iff linorder_neq_iff distrib_left ac_simps)
    1.13 -
    1.14  lemma zdiv_zmult1_eq: "(a*b) div c = a*(b div c) + a*(b mod c) div (c::int)"
    1.15 -apply (case_tac "c = 0", simp)
    1.16 -apply (blast intro: eucl_rel_int [THEN zmult1_lemma, THEN div_int_unique])
    1.17 -done
    1.18 -
    1.19 -text\<open>proving (a+b) div c = a div c + b div c + ((a mod c + b mod c) div c)\<close>
    1.20 -
    1.21 -lemma zadd1_lemma:
    1.22 -     "[| eucl_rel_int a c (aq, ar);  eucl_rel_int b c (bq, br) |]
    1.23 -      ==> eucl_rel_int (a+b) c (aq + bq + (ar+br) div c, (ar+br) mod c)"
    1.24 -by (force simp add: split_ifs eucl_rel_int_iff linorder_neq_iff distrib_left)
    1.25 +  by (fact div_mult1_eq)
    1.26  
    1.27  (*NOT suitable for rewriting: the RHS has an instance of the LHS*)
    1.28  lemma zdiv_zadd1_eq:
    1.29       "(a+b) div (c::int) = a div c + b div c + ((a mod c + b mod c) div c)"
    1.30 -apply (case_tac "c = 0", simp)
    1.31 -apply (blast intro: zadd1_lemma [OF eucl_rel_int eucl_rel_int] div_int_unique)
    1.32 -done
    1.33 +  by (fact div_add1_eq)
    1.34  
    1.35  lemma zmod_eq_0_iff: "(m mod d = 0) = (EX q::int. m = d*q)"
    1.36  by (simp add: dvd_eq_mod_eq_0 [symmetric] dvd_def)
     2.1 --- a/src/HOL/Euclidean_Division.thy	Sun Oct 08 22:28:22 2017 +0200
     2.2 +++ b/src/HOL/Euclidean_Division.thy	Sun Oct 08 22:28:22 2017 +0200
     2.3 @@ -531,9 +531,10 @@
     2.4        and "a div b = q"
     2.5        and "a mod b = 0"
     2.6        and "a = q * b"
     2.7 -  | (remainder) q r where "b \<noteq> 0" and "r \<noteq> 0"
     2.8 +  | (remainder) q r where "b \<noteq> 0"
     2.9        and "uniqueness_constraint r b"
    2.10        and "euclidean_size r < euclidean_size b"
    2.11 +      and "r \<noteq> 0"
    2.12        and "a div b = q"
    2.13        and "a mod b = r"
    2.14        and "a = q * b + r"
    2.15 @@ -630,6 +631,67 @@
    2.16    qed
    2.17  qed
    2.18  
    2.19 +lemma div_mult1_eq:
    2.20 +  "(a * b) div c = a * (b div c) + a * (b mod c) div c"
    2.21 +proof (cases "a * (b mod c)" c rule: divmod_cases)
    2.22 +  case (divides q)
    2.23 +  have "a * b = a * (b div c * c + b mod c)"
    2.24 +    by (simp add: div_mult_mod_eq)
    2.25 +  also have "\<dots> = (a * (b div c) + q) * c"
    2.26 +    using divides by (simp add: algebra_simps)
    2.27 +  finally have "(a * b) div c = \<dots> div c"
    2.28 +    by simp
    2.29 +  with divides show ?thesis
    2.30 +    by simp
    2.31 +next
    2.32 +  case (remainder q r)
    2.33 +  from remainder(1-3) show ?thesis
    2.34 +  proof (rule div_eqI)
    2.35 +    have "a * b = a * (b div c * c + b mod c)"
    2.36 +      by (simp add: div_mult_mod_eq)
    2.37 +    also have "\<dots> = a * c * (b div c) + q * c + r"
    2.38 +      using remainder by (simp add: algebra_simps)
    2.39 +    finally show "(a * (b div c) + a * (b mod c) div c) * c + r = a * b"
    2.40 +      using remainder(5-7) by (simp add: algebra_simps)
    2.41 +  qed
    2.42 +next
    2.43 +  case by0
    2.44 +  then show ?thesis
    2.45 +    by simp
    2.46 +qed
    2.47 +
    2.48 +lemma div_add1_eq:
    2.49 +  "(a + b) div c = a div c + b div c + (a mod c + b mod c) div c"
    2.50 +proof (cases "a mod c + b mod c" c rule: divmod_cases)
    2.51 +  case (divides q)
    2.52 +  have "a + b = (a div c * c + a mod c) + (b div c * c + b mod c)"
    2.53 +    using mod_mult_div_eq [of a c] mod_mult_div_eq [of b c] by (simp add: ac_simps)
    2.54 +  also have "\<dots> = (a div c + b div c) * c + (a mod c + b mod c)"
    2.55 +    by (simp add: algebra_simps)
    2.56 +  also have "\<dots> = (a div c + b div c + q) * c"
    2.57 +    using divides by (simp add: algebra_simps)
    2.58 +  finally have "(a + b) div c = (a div c + b div c + q) * c div c"
    2.59 +    by simp
    2.60 +  with divides show ?thesis
    2.61 +    by simp
    2.62 +next
    2.63 +  case (remainder q r)
    2.64 +  from remainder(1-3) show ?thesis
    2.65 +  proof (rule div_eqI)
    2.66 +    have "(a div c + b div c + q) * c + r + (a mod c + b mod c) =
    2.67 +        (a div c * c + a mod c) + (b div c * c + b mod c) + q * c + r"
    2.68 +      by (simp add: algebra_simps)
    2.69 +    also have "\<dots> = a + b + (a mod c + b mod c)"
    2.70 +      by (simp add: div_mult_mod_eq remainder) (simp add: ac_simps)
    2.71 +    finally show "(a div c + b div c + (a mod c + b mod c) div c) * c + r = a + b"
    2.72 +      using remainder by simp
    2.73 +  qed
    2.74 +next
    2.75 +  case by0
    2.76 +  then show ?thesis
    2.77 +    by simp
    2.78 +qed
    2.79 +
    2.80  end
    2.81  
    2.82  class unique_euclidean_ring = euclidean_ring + unique_euclidean_semiring
    2.83 @@ -947,23 +1009,6 @@
    2.84    and Suc_mod_mult_self4 [simp]: "Suc (n * k + m) mod n = Suc m mod n"
    2.85    by (subst mod_Suc_eq [symmetric], simp add: mod_simps)+
    2.86  
    2.87 -lemma div_mult1_eq: -- \<open>TODO: Generalization candidate\<close>
    2.88 -  "(a * b) div c = a * (b div c) + a * (b mod c) div c" for a b c :: nat
    2.89 -  apply (cases "c = 0")
    2.90 -   apply simp
    2.91 -  apply (rule div_eqI [of _ "(a * (b mod c)) mod c"])
    2.92 -     apply (auto simp add: algebra_simps distrib_left [symmetric])
    2.93 -  done
    2.94 -
    2.95 -lemma div_add1_eq: -- \<open>NOT suitable for rewriting: the RHS has an instance of the LHS\<close>
    2.96 -   -- \<open>TODO: Generalization candidate\<close>
    2.97 -  "(a + b) div c = a div c + b div c + ((a mod c + b mod c) div c)" for a b c :: nat
    2.98 -  apply (cases "c = 0")
    2.99 -   apply simp
   2.100 -  apply (rule div_eqI [of _ "(a mod c + b mod c) mod c"])
   2.101 -  apply (auto simp add: algebra_simps)
   2.102 -  done
   2.103 -
   2.104  context
   2.105    fixes m n q :: nat
   2.106  begin