src/HOL/Integ/IntDiv.thy

 
 lemma zdiv_zmod_equality: "(b * (a div b) + (a mod b)) + k = (a::int)+k"
 by(simp add: zmod_zdiv_equality[symmetric])
 
 lemma zdiv_zmod_equality2: "((a div b) * b + (a mod b)) + k = (a::int)+k"
-by(simp add: zmult_commute zmod_zdiv_equality[symmetric])
+by(simp add: mult_commute zmod_zdiv_equality[symmetric])
 
 use "IntDiv_setup.ML"
 
 lemma pos_mod_conj : "(0::int) < b ==> 0 \<le> a mod b & a mod b < b"
 apply (cut_tac a = a and b = b in divAlg_correct)

 
 lemma zmod_zmult1_eq': "(a*b) mod (c::int) = ((a mod c) * b) mod c"
 apply (rule trans)
 apply (rule_tac s = "b*a mod c" in trans)
 apply (rule_tac [2] zmod_zmult1_eq)
-apply (simp_all add: zmult_commute)
+apply (simp_all add: mult_commute)
 done
 
 lemma zmod_zmult_distrib: "(a*b) mod (c::int) = ((a mod c) * (b mod c)) mod c"
 apply (rule zmod_zmult1_eq' [THEN trans])
 apply (rule zmod_zmult1_eq)

 
 lemma zdiv_zmult_self1 [simp]: "b \<noteq> (0::int) ==> (a*b) div b = a"
 by (simp add: zdiv_zmult1_eq)
 
 lemma zdiv_zmult_self2 [simp]: "b \<noteq> (0::int) ==> (b*a) div b = a"
-by (subst zmult_commute, erule zdiv_zmult_self1)
+by (subst mult_commute, erule zdiv_zmult_self1)
 
 lemma zmod_zmult_self1 [simp]: "(a*b) mod b = (0::int)"
 by (simp add: zmod_zmult1_eq)
 
 lemma zmod_zmult_self2 [simp]: "(b*a) mod b = (0::int)"
-by (simp add: zmult_commute zmod_zmult1_eq)
+by (simp add: mult_commute zmod_zmult1_eq)
 
 lemma zmod_eq_0_iff: "(m mod d = 0) = (EX q::int. m = d*q)"
 proof
   assume "m mod d = 0"
   with zmod_zdiv_equality[of m d] show "EX q::int. m = d*q" by auto

 apply (auto simp add: linorder_neq_iff zdiv_zmult_zmult1_aux1 zdiv_zmult_zmult1_aux2)
 done
 
 lemma zdiv_zmult_zmult2: "c \<noteq> (0::int) ==> (a*c) div (b*c) = a div b"
 apply (drule zdiv_zmult_zmult1)
-apply (auto simp add: zmult_commute)
+apply (auto simp add: mult_commute)
 done
 
 
 
 subsection{*Distribution of Factors over mod*}

 apply (auto simp add: linorder_neq_iff zmod_zmult_zmult1_aux1 zmod_zmult_zmult1_aux2)
 done
 
 lemma zmod_zmult_zmult2: "(a*c) mod (b*c) = (a mod b) * (c::int)"
 apply (cut_tac c = c in zmod_zmult_zmult1)
-apply (auto simp add: zmult_commute)
+apply (auto simp add: mult_commute)
 done
 
 
 subsection {*Splitting Rules for div and mod*}
 

 apply (case_tac "a = 0", simp)
 apply (subgoal_tac "1 < a * 2")
  prefer 2 apply arith
 apply (subgoal_tac "2* (1 + b mod a) \<le> 2*a")
  apply (rule_tac [2] mult_left_mono)
-apply (auto simp add: add_commute [of 1] zmult_commute add1_zle_eq 
+apply (auto simp add: add_commute [of 1] mult_commute add1_zle_eq 
                       pos_mod_bound)
 apply (subst zmod_zadd1_eq)
 apply (simp add: zmod_zmult_zmult2 mod_pos_pos_trivial)
 apply (rule mod_pos_pos_trivial)
 apply (auto simp add: mod_pos_pos_trivial left_distrib)

 
 lemma zdvd_refl [simp]: "m dvd (m::int)"
 by (auto simp add: dvd_def intro: zmult_1_right [symmetric])
 
 lemma zdvd_trans: "m dvd n ==> n dvd k ==> m dvd (k::int)"
-by (auto simp add: dvd_def intro: zmult_assoc)
+by (auto simp add: dvd_def intro: mult_assoc)
 
 lemma zdvd_zminus_iff: "(m dvd -n) = (m dvd (n::int))"
   apply (simp add: dvd_def, auto)
    apply (rule_tac [!] x = "-k" in exI, auto)
   done

   done
 
 lemma zdvd_anti_sym:
     "0 < m ==> 0 < n ==> m dvd n ==> n dvd m ==> m = (n::int)"
   apply (simp add: dvd_def, auto)
-  apply (simp add: zmult_assoc zmult_eq_self_iff zero_less_mult_iff zmult_eq_1_iff)
+  apply (simp add: mult_assoc zero_less_mult_iff zmult_eq_1_iff)
   done
 
 lemma zdvd_zadd: "k dvd m ==> k dvd n ==> k dvd (m + n :: int)"
   apply (simp add: dvd_def)
   apply (blast intro: right_distrib [symmetric])

   apply (simp add: dvd_def)
   apply (blast intro: mult_left_commute)
   done
 
 lemma zdvd_zmult2: "k dvd (m::int) ==> k dvd m * n"
-  apply (subst zmult_commute)
+  apply (subst mult_commute)
   apply (erule zdvd_zmult)
   done
 
 lemma [iff]: "(k::int) dvd m * k"
   apply (rule zdvd_zmult)

   apply (rule zdvd_refl)
   done
 
 lemma zdvd_zmultD2: "j * k dvd n ==> j dvd (n::int)"
   apply (simp add: dvd_def)
-  apply (simp add: zmult_assoc, blast)
+  apply (simp add: mult_assoc, blast)
   done
 
 lemma zdvd_zmultD: "j * k dvd n ==> k dvd (n::int)"
   apply (rule zdvd_zmultD2)
-  apply (subst zmult_commute, assumption)
+  apply (subst mult_commute, assumption)
   done
 
 lemma zdvd_zmult_mono: "i dvd m ==> j dvd (n::int) ==> i * j dvd m * n"
   apply (simp add: dvd_def, clarify)
   apply (rule_tac x = "k * ka" in exI)