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.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*)