# HG changeset patch
# User haftmann
# Date 1507494502 -7200
# Node ID a24cde9588bbb59481c391f291192194fa92a730
# Parent  3511427963453aa7d3ef72c8eda9d47a04bf8103
generalized some rules

diff -r 351142796345 -r a24cde9588bb src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Sun Oct 08 22:28:22 2017 +0200
+++ b/src/HOL/Divides.thy	Sun Oct 08 22:28:22 2017 +0200
@@ -838,31 +838,13 @@
 
 subsubsection \<open>More Algebraic Laws for div and mod\<close>
 
-text\<open>proving (a*b) div c = a * (b div c) + a * (b mod c)\<close>
-
-lemma zmult1_lemma:
-     "[| eucl_rel_int b c (q, r) |]
-      ==> eucl_rel_int (a * b) c (a*q + a*r div c, a*r mod c)"
-by (auto simp add: split_ifs eucl_rel_int_iff linorder_neq_iff distrib_left ac_simps)
-
 lemma zdiv_zmult1_eq: "(a*b) div c = a*(b div c) + a*(b mod c) div (c::int)"
-apply (case_tac "c = 0", simp)
-apply (blast intro: eucl_rel_int [THEN zmult1_lemma, THEN div_int_unique])
-done
-
-text\<open>proving (a+b) div c = a div c + b div c + ((a mod c + b mod c) div c)\<close>
-
-lemma zadd1_lemma:
-     "[| eucl_rel_int a c (aq, ar);  eucl_rel_int b c (bq, br) |]
-      ==> eucl_rel_int (a+b) c (aq + bq + (ar+br) div c, (ar+br) mod c)"
-by (force simp add: split_ifs eucl_rel_int_iff linorder_neq_iff distrib_left)
+  by (fact div_mult1_eq)
 
 (*NOT suitable for rewriting: the RHS has an instance of the LHS*)
 lemma zdiv_zadd1_eq:
      "(a+b) div (c::int) = a div c + b div c + ((a mod c + b mod c) div c)"
-apply (case_tac "c = 0", simp)
-apply (blast intro: zadd1_lemma [OF eucl_rel_int eucl_rel_int] div_int_unique)
-done
+  by (fact div_add1_eq)
 
 lemma zmod_eq_0_iff: "(m mod d = 0) = (EX q::int. m = d*q)"
 by (simp add: dvd_eq_mod_eq_0 [symmetric] dvd_def)
diff -r 351142796345 -r a24cde9588bb src/HOL/Euclidean_Division.thy
--- a/src/HOL/Euclidean_Division.thy	Sun Oct 08 22:28:22 2017 +0200
+++ b/src/HOL/Euclidean_Division.thy	Sun Oct 08 22:28:22 2017 +0200
@@ -531,9 +531,10 @@
       and "a div b = q"
       and "a mod b = 0"
       and "a = q * b"
-  | (remainder) q r where "b \<noteq> 0" and "r \<noteq> 0"
+  | (remainder) q r where "b \<noteq> 0"
       and "uniqueness_constraint r b"
       and "euclidean_size r < euclidean_size b"
+      and "r \<noteq> 0"
       and "a div b = q"
       and "a mod b = r"
       and "a = q * b + r"
@@ -630,6 +631,67 @@
   qed
 qed
 
+lemma div_mult1_eq:
+  "(a * b) div c = a * (b div c) + a * (b mod c) div c"
+proof (cases "a * (b mod c)" c rule: divmod_cases)
+  case (divides q)
+  have "a * b = a * (b div c * c + b mod c)"
+    by (simp add: div_mult_mod_eq)
+  also have "\<dots> = (a * (b div c) + q) * c"
+    using divides by (simp add: algebra_simps)
+  finally have "(a * b) div c = \<dots> div c"
+    by simp
+  with divides show ?thesis
+    by simp
+next
+  case (remainder q r)
+  from remainder(1-3) show ?thesis
+  proof (rule div_eqI)
+    have "a * b = a * (b div c * c + b mod c)"
+      by (simp add: div_mult_mod_eq)
+    also have "\<dots> = a * c * (b div c) + q * c + r"
+      using remainder by (simp add: algebra_simps)
+    finally show "(a * (b div c) + a * (b mod c) div c) * c + r = a * b"
+      using remainder(5-7) by (simp add: algebra_simps)
+  qed
+next
+  case by0
+  then show ?thesis
+    by simp
+qed
+
+lemma div_add1_eq:
+  "(a + b) div c = a div c + b div c + (a mod c + b mod c) div c"
+proof (cases "a mod c + b mod c" c rule: divmod_cases)
+  case (divides q)
+  have "a + b = (a div c * c + a mod c) + (b div c * c + b mod c)"
+    using mod_mult_div_eq [of a c] mod_mult_div_eq [of b c] by (simp add: ac_simps)
+  also have "\<dots> = (a div c + b div c) * c + (a mod c + b mod c)"
+    by (simp add: algebra_simps)
+  also have "\<dots> = (a div c + b div c + q) * c"
+    using divides by (simp add: algebra_simps)
+  finally have "(a + b) div c = (a div c + b div c + q) * c div c"
+    by simp
+  with divides show ?thesis
+    by simp
+next
+  case (remainder q r)
+  from remainder(1-3) show ?thesis
+  proof (rule div_eqI)
+    have "(a div c + b div c + q) * c + r + (a mod c + b mod c) =
+        (a div c * c + a mod c) + (b div c * c + b mod c) + q * c + r"
+      by (simp add: algebra_simps)
+    also have "\<dots> = a + b + (a mod c + b mod c)"
+      by (simp add: div_mult_mod_eq remainder) (simp add: ac_simps)
+    finally show "(a div c + b div c + (a mod c + b mod c) div c) * c + r = a + b"
+      using remainder by simp
+  qed
+next
+  case by0
+  then show ?thesis
+    by simp
+qed
+
 end
 
 class unique_euclidean_ring = euclidean_ring + unique_euclidean_semiring
@@ -947,23 +1009,6 @@
   and Suc_mod_mult_self4 [simp]: "Suc (n * k + m) mod n = Suc m mod n"
   by (subst mod_Suc_eq [symmetric], simp add: mod_simps)+
 
-lemma div_mult1_eq: -- \<open>TODO: Generalization candidate\<close>
-  "(a * b) div c = a * (b div c) + a * (b mod c) div c" for a b c :: nat
-  apply (cases "c = 0")
-   apply simp
-  apply (rule div_eqI [of _ "(a * (b mod c)) mod c"])
-     apply (auto simp add: algebra_simps distrib_left [symmetric])
-  done
-
-lemma div_add1_eq: -- \<open>NOT suitable for rewriting: the RHS has an instance of the LHS\<close>
-   -- \<open>TODO: Generalization candidate\<close>
-  "(a + b) div c = a div c + b div c + ((a mod c + b mod c) div c)" for a b c :: nat
-  apply (cases "c = 0")
-   apply simp
-  apply (rule div_eqI [of _ "(a mod c + b mod c) mod c"])
-  apply (auto simp add: algebra_simps)
-  done
-
 context
   fixes m n q :: nat
 begin