src/HOL/Divides.thy
changeset 66814 a24cde9588bb
parent 66810 cc2b490f9dc4
child 66815 93c6632ddf44
     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)