src/HOL/Divides.thy

 qed (simp add: div_by_0)
 
 text \<open>@{const divide} and @{const modulo}\<close>
 
 lemma div_mod_equality: "((a div b) * b + a mod b) + c = a + c"
-  by (simp add: mod_div_equality)
+  by (simp add: div_mult_mod_eq)
 
 lemma div_mod_equality2: "(b * (a div b) + a mod b) + c = a + c"
-  by (simp add: mod_div_equality2)
+  by (simp add: mult_div_mod_eq)
 
 lemma mod_by_0 [simp]: "a mod 0 = a"
-  using mod_div_equality [of a zero] by simp
+  using div_mult_mod_eq [of a zero] by simp
 
 lemma mod_0 [simp]: "0 mod a = 0"
-  using mod_div_equality [of zero a] div_0 by simp
+  using div_mult_mod_eq [of zero a] div_0 by simp
 
 lemma div_mult_self2 [simp]:
   assumes "b \<noteq> 0"
   shows "(a + b * c) div b = c + a div b"
   using assms div_mult_self1 [of b a c] by (simp add: mult.commute)

 proof (cases "b = 0")
   case True then show ?thesis by simp
 next
   case False
   have "a + c * b = (a + c * b) div b * b + (a + c * b) mod b"
-    by (simp add: mod_div_equality)
+    by (simp add: div_mult_mod_eq)
   also from False div_mult_self1 [of b a c] have
     "\<dots> = (c + a div b) * b + (a + c * b) mod b"
       by (simp add: algebra_simps)
   finally have "a = a div b * b + (a + c * b) mod b"
     by (simp add: add.commute [of a] add.assoc distrib_right)
   then have "a div b * b + (a + c * b) mod b = a div b * b + a mod b"
-    by (simp add: mod_div_equality)
+    by (simp add: div_mult_mod_eq)
   then show ?thesis by simp
 qed
 
 lemma mod_mult_self2 [simp]:
   "(a + b * c) mod b = a mod b"

   using mod_mult_self1 [of 0 a b] by simp
 
 lemma mod_by_1 [simp]:
   "a mod 1 = 0"
 proof -
-  from mod_div_equality [of a one] div_by_1 have "a + a mod 1 = a" by simp
+  from div_mult_mod_eq [of a one] div_by_1 have "a + a mod 1 = a" by simp
   then have "a + a mod 1 = a + 0" by simp
   then show ?thesis by (rule add_left_imp_eq)
 qed
 
 lemma mod_self [simp]:

 proof
   assume "b dvd a"
   then show "a mod b = 0" by simp
 next
   assume "a mod b = 0"
-  with mod_div_equality [of a b] have "a div b * b = a" by simp
+  with div_mult_mod_eq [of a b] have "a div b * b = a" by simp
   then have "a = b * (a div b)" by (simp add: ac_simps)
   then show "b dvd a" ..
 qed
 
 lemma dvd_eq_mod_eq_0 [nitpick_unfold, code]:

 next
   assume "b \<noteq> 0"
   hence "a div b + a mod b div b = (a mod b + a div b * b) div b"
     by (rule div_mult_self1 [symmetric])
   also have "\<dots> = a div b"
-    by (simp only: mod_div_equality3)
+    by (simp only: mod_div_mult_eq)
   also have "\<dots> = a div b + 0"
     by simp
   finally show ?thesis
     by (rule add_left_imp_eq)
 qed

   "a mod b mod b = a mod b"
 proof -
   have "a mod b mod b = (a mod b + a div b * b) mod b"
     by (simp only: mod_mult_self1)
   also have "\<dots> = a mod b"
-    by (simp only: mod_div_equality3)
+    by (simp only: mod_div_mult_eq)
   finally show ?thesis .
 qed
 
 lemma dvd_mod_imp_dvd:
   assumes "k dvd m mod n" and "k dvd n"
   shows "k dvd m"
 proof -
   from assms have "k dvd (m div n) * n + m mod n"
     by (simp only: dvd_add dvd_mult)
-  then show ?thesis by (simp add: mod_div_equality)
+  then show ?thesis by (simp add: div_mult_mod_eq)
 qed
 
 text \<open>Addition respects modular equivalence.\<close>
 
 lemma mod_add_left_eq: \<comment> \<open>FIXME reorient\<close>
   "(a + b) mod c = (a mod c + b) mod c"
 proof -
   have "(a + b) mod c = (a div c * c + a mod c + b) mod c"
-    by (simp only: mod_div_equality)
+    by (simp only: div_mult_mod_eq)
   also have "\<dots> = (a mod c + b + a div c * c) mod c"
     by (simp only: ac_simps)
   also have "\<dots> = (a mod c + b) mod c"
     by (rule mod_mult_self1)
   finally show ?thesis .

 
 lemma mod_add_right_eq: \<comment> \<open>FIXME reorient\<close>
   "(a + b) mod c = (a + b mod c) mod c"
 proof -
   have "(a + b) mod c = (a + (b div c * c + b mod c)) mod c"
-    by (simp only: mod_div_equality)
+    by (simp only: div_mult_mod_eq)
   also have "\<dots> = (a + b mod c + b div c * c) mod c"
     by (simp only: ac_simps)
   also have "\<dots> = (a + b mod c) mod c"
     by (rule mod_mult_self1)
   finally show ?thesis .

 
 lemma mod_mult_left_eq: \<comment> \<open>FIXME reorient\<close>
   "(a * b) mod c = ((a mod c) * b) mod c"
 proof -
   have "(a * b) mod c = ((a div c * c + a mod c) * b) mod c"
-    by (simp only: mod_div_equality)
+    by (simp only: div_mult_mod_eq)
   also have "\<dots> = (a mod c * b + a div c * b * c) mod c"
     by (simp only: algebra_simps)
   also have "\<dots> = (a mod c * b) mod c"
     by (rule mod_mult_self1)
   finally show ?thesis .

 
 lemma mod_mult_right_eq: \<comment> \<open>FIXME reorient\<close>
   "(a * b) mod c = (a * (b mod c)) mod c"
 proof -
   have "(a * b) mod c = (a * (b div c * c + b mod c)) mod c"
-    by (simp only: mod_div_equality)
+    by (simp only: div_mult_mod_eq)
   also have "\<dots> = (a * (b mod c) + a * (b div c) * c) mod c"
     by (simp only: algebra_simps)
   also have "\<dots> = (a * (b mod c)) mod c"
     by (rule mod_mult_self1)
   finally show ?thesis .

   also have "\<dots> = (a mod (c * k) + a div (c * k) * k * c) mod c"
     by (simp only: mod_mult_self1)
   also have "\<dots> = (a div (c * k) * (c * k) + a mod (c * k)) mod c"
     by (simp only: ac_simps)
   also have "\<dots> = a mod c"
-    by (simp only: mod_div_equality)
+    by (simp only: div_mult_mod_eq)
   finally show ?thesis .
 qed
 
 lemma div_mult_mult2 [simp]:
   "c \<noteq> 0 \<Longrightarrow> (a * c) div (b * c) = a div b"

   "(c * a) mod (c * b) = c * (a mod b)"
 proof (cases "c = 0")
   case True then show ?thesis by simp
 next
   case False
-  from mod_div_equality
+  from div_mult_mod_eq
   have "((c * a) div (c * b)) * (c * b) + (c * a) mod (c * b) = c * a" .
   with False have "c * ((a div b) * b + a mod b) + (c * a) mod (c * b)
     = c * a + c * (a mod b)" by (simp add: algebra_simps)
-  with mod_div_equality show ?thesis by simp
+  with div_mult_mod_eq show ?thesis by simp
 qed
 
 lemma mod_mult_mult2:
   "(a * c) mod (b * c) = (a mod b) * c"
   using mod_mult_mult1 [of c a b] by (simp add: mult.commute)

 text \<open>Negation respects modular equivalence.\<close>
 
 lemma mod_minus_eq: "(- a) mod b = (- (a mod b)) mod b"
 proof -
   have "(- a) mod b = (- (a div b * b + a mod b)) mod b"
-    by (simp only: mod_div_equality)
+    by (simp only: div_mult_mod_eq)
   also have "\<dots> = (- (a mod b) + - (a div b) * b) mod b"
     by (simp add: ac_simps)
   also have "\<dots> = (- (a mod b)) mod b"
     by (rule mod_mult_self1)
   finally show ?thesis .

   "1 div 2 = 0"
 proof (cases "2 = 0")
   case True then show ?thesis by simp
 next
   case False
-  from mod_div_equality have "1 div 2 * 2 + 1 mod 2 = 1" .
+  from div_mult_mod_eq have "1 div 2 * 2 + 1 mod 2 = 1" .
   with one_mod_two_eq_one have "1 div 2 * 2 + 1 = 1" by simp
   then have "1 div 2 * 2 = 0" by (simp add: ac_simps add_left_imp_eq del: mult_eq_0_iff)
   then have "1 div 2 = 0 \<or> 2 = 0" by simp
   with False show ?thesis by auto
 qed

   then show "a mod 2 = 0 \<or> b mod 2 = 0"
     by (rule divisors_zero)
 next
   fix a
   assume "a mod 2 = 1"
-  then have "a = a div 2 * 2 + 1" using mod_div_equality [of a 2] by simp
+  then have "a = a div 2 * 2 + 1" using div_mult_mod_eq [of a 2] by simp
   then show "\<exists>b. a = b + 1" ..
 qed
 
 lemma even_iff_mod_2_eq_zero:
   "even a \<longleftrightarrow> a mod 2 = 0"

   "even a \<Longrightarrow> 2 * (a div 2) = a"
   by (fact dvd_mult_div_cancel)
 
 lemma odd_two_times_div_two_succ [simp]:
   "odd a \<Longrightarrow> 2 * (a div 2) + 1 = a"
-  using mod_div_equality2 [of 2 a] by (simp add: even_iff_mod_2_eq_zero)
+  using mult_div_mod_eq [of 2 a] by (simp add: even_iff_mod_2_eq_zero)
  
 end
 
 
 subsection \<open>Generic numeral division with a pragmatic type class\<close>

 
 lemma mult_div_cancel:
   "b * (a div b) = a - a mod b"
 proof -
   have "b * (a div b) + a mod b = a"
-    using mod_div_equality [of a b] by (simp add: ac_simps)
+    using div_mult_mod_eq [of a b] by (simp add: ac_simps)
   then have "b * (a div b) + a mod b - a mod b = a - a mod b"
     by simp
   then show ?thesis
     by simp
 qed

 
 lemma mod_less_eq_dividend [simp]:
   fixes m n :: nat
   shows "m mod n \<le> m"
 proof (rule add_leD2)
-  from mod_div_equality have "m div n * n + m mod n = m" .
+  from div_mult_mod_eq have "m div n * n + m mod n = m" .
   then show "m div n * n + m mod n \<le> m" by auto
 qed
 
 lemma mod_geq: "\<not> m < (n::nat) \<Longrightarrow> m mod n = (m - n) mod n"
 by (simp add: le_mod_geq linorder_not_less)

 by (simp add: le_mod_geq)
 
 lemma mod_1 [simp]: "m mod Suc 0 = 0"
 by (induct m) (simp_all add: mod_geq)
 
-(* a simple rearrangement of mod_div_equality: *)
+(* a simple rearrangement of div_mult_mod_eq: *)
 lemma mult_div_cancel: "(n::nat) * (m div n) = m - (m mod n)"
-  using mod_div_equality2 [of n m] by arith
+  using mult_div_mod_eq [of n m] by arith
 
 lemma mod_le_divisor[simp]: "0 < n \<Longrightarrow> m mod n \<le> (n::nat)"
   apply (drule mod_less_divisor [where m = m])
   apply simp
   done

 lemma mod_eqD:
   fixes m d r q :: nat
   assumes "m mod d = r"
   shows "\<exists>q. m = r + q * d"
 proof -
-  from mod_div_equality obtain q where "q * d + m mod d = m" by blast
+  from div_mult_mod_eq obtain q where "q * d + m mod d = m" by blast
   with assms have "m = r + q * d" by simp
   then show ?thesis ..
 qed
 
 lemma split_div:

     from not0 R[THEN spec,of "n div k",THEN spec, of "n mod k"]
     show ?P by simp
   qed
 qed
 
-theorem mod_div_equality' [nitpick_unfold]: "(m::nat) mod n = m - (m div n) * n"
-  using mod_div_equality [of m n] by arith
+theorem div_mult_mod_eq' [nitpick_unfold]: "(m::nat) mod n = m - (m div n) * n"
+  using div_mult_mod_eq [of m n] by arith
 
 lemma div_mod_equality': "(m::nat) div n * n = m - m mod n"
-  using mod_div_equality [of m n] by arith
+  using div_mult_mod_eq [of m n] by arith
 (* FIXME: very similar to mult_div_cancel *)
 
 lemma div_eq_dividend_iff: "a \<noteq> 0 \<Longrightarrow> (a :: nat) div b = a \<longleftrightarrow> b = 1"
   apply rule
   apply (cases "b = 0")

 end
   
 text\<open>Basic laws about division and remainder\<close>
 
 lemma zmod_zdiv_equality: "(a::int) = b * (a div b) + (a mod b)"
-  by (fact mod_div_equality2 [symmetric])
+  by (fact mult_div_mod_eq [symmetric])
 
 lemma zdiv_int: "int (a div b) = int a div int b"
   by (simp add: divide_int_def)
 
 lemma zmod_int: "int (a mod b) = int a mod int b"

 (* REVISIT: should this be generalized to all semiring_div types? *)
 lemmas zmod_eq_0D [dest!] = zmod_eq_0_iff [THEN iffD1]
 
 lemma zmod_zdiv_equality' [nitpick_unfold]:
   "(m::int) mod n = m - (m div n) * n"
-  using mod_div_equality [of m n] by arith
+  using div_mult_mod_eq [of m n] by arith
 
 
 subsubsection \<open>Proving  @{term "a div (b * c) = (a div b) div c"}\<close>
 
 (*The condition c>0 seems necessary.  Consider that 7 div ~6 = ~2 but

 lemma zmod_trival_iff:
   fixes i k :: int
   shows "i mod k = i \<longleftrightarrow> k = 0 \<or> 0 \<le> i \<and> i < k \<or> i \<le> 0 \<and> k < i"
 proof -
   have "i mod k = i \<longleftrightarrow> i div k = 0"
-    by safe (insert mod_div_equality [of i k], auto)
+    by safe (insert div_mult_mod_eq [of i k], auto)
   with zdiv_eq_0_iff
   show ?thesis
     by simp
 qed