# HG changeset patch
# User haftmann
# Date 1476603064 -7200
# Node ID eabf80376aab5f687048e64e5b83fcd6a72e5474
# Parent  de5cd9217d4c929b09e393cdc9637baf5f250b66
more standardized names

diff -r de5cd9217d4c -r eabf80376aab NEWS
--- a/NEWS	Sun Oct 16 09:31:03 2016 +0200
+++ b/NEWS	Sun Oct 16 09:31:04 2016 +0200
@@ -249,6 +249,21 @@
 
 *** HOL ***
 
+* Sligthly more standardized theorem names:
+    sgn_times ~> sgn_mult
+    sgn_mult' ~> Real_Vector_Spaces.sgn_mult
+    divide_zero_left ~> div_0
+    zero_mod_left ~> mod_0
+    divide_zero ~> div_by_0
+    divide_1 ~> div_by_1
+    nonzero_mult_divide_cancel_left ~> nonzero_mult_div_cancel_left
+    div_mult_self1_is_id ~> nonzero_mult_div_cancel_left
+    nonzero_mult_divide_cancel_right ~> nonzero_mult_div_cancel_right
+    div_mult_self2_is_id ~> nonzero_mult_div_cancel_right
+    is_unit_divide_mult_cancel_left ~> is_unit_div_mult_cancel_left
+    is_unit_divide_mult_cancel_right ~> is_unit_div_mult_cancel_right
+INCOMPATIBILITY.
+
 * Dedicated syntax LENGTH('a) for length of types.
 
 * New proof method "argo" using the built-in Argo solver based on SMT
diff -r de5cd9217d4c -r eabf80376aab src/HOL/Analysis/Cauchy_Integral_Theorem.thy
--- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Sun Oct 16 09:31:03 2016 +0200
+++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Sun Oct 16 09:31:04 2016 +0200
@@ -5106,7 +5106,7 @@
                   and x: "x \<in> {0..1}" and y: "y \<in> {0..1}" for x y n
     proof -
       have "(linepath s t x) = (linepath s t y) + 2 * of_int n * complex_of_real pi"
-        by (metis add_divide_eq_iff complex_i_not_zero mult.commute nonzero_mult_divide_cancel_left eq)
+        by (metis add_divide_eq_iff complex_i_not_zero mult.commute nonzero_mult_div_cancel_left eq)
       then have "s*y + t*x = s*x + (t*y + of_int n * (pi * 2))"
         by (force simp: algebra_simps linepath_def dest: arg_cong [where f=Re])
       then have st: "x \<noteq> y \<Longrightarrow> (s-t) = (of_int n * (pi * 2) / (y-x))"
diff -r de5cd9217d4c -r eabf80376aab src/HOL/Analysis/Complex_Transcendental.thy
--- a/src/HOL/Analysis/Complex_Transcendental.thy	Sun Oct 16 09:31:03 2016 +0200
+++ b/src/HOL/Analysis/Complex_Transcendental.thy	Sun Oct 16 09:31:04 2016 +0200
@@ -1315,7 +1315,7 @@
   case False
   then have "z / of_real(norm z) = exp(\<i> * of_real(Arg z))"
     using Arg [of z]
-    by (metis abs_norm_cancel nonzero_mult_divide_cancel_left norm_of_real zero_less_norm_iff)
+    by (metis abs_norm_cancel nonzero_mult_div_cancel_left norm_of_real zero_less_norm_iff)
   then have "- z / of_real(norm z) = exp (\<i> * (of_real (Arg z) - pi))"
     using cis_conv_exp cis_pi
     by (auto simp: exp_diff algebra_simps)
@@ -1918,7 +1918,7 @@
     shows "csqrt z = exp(Ln(z) / 2)"
 proof -
   have "(exp (Ln z / 2))\<^sup>2 = (exp (Ln z))"
-    by (metis exp_double nonzero_mult_divide_cancel_left times_divide_eq_right zero_neq_numeral)
+    by (metis exp_double nonzero_mult_div_cancel_left times_divide_eq_right zero_neq_numeral)
   also have "... = z"
     using assms exp_Ln by blast
   finally have "csqrt z = csqrt ((exp (Ln z / 2))\<^sup>2)"
diff -r de5cd9217d4c -r eabf80376aab src/HOL/Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Analysis/Convex_Euclidean_Space.thy	Sun Oct 16 09:31:03 2016 +0200
+++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy	Sun Oct 16 09:31:04 2016 +0200
@@ -11985,7 +11985,7 @@
   have "UNIV \<subseteq> {x. a \<bullet> x = b} \<Longrightarrow> a = 0 \<and> b = 0"
     apply (drule_tac c = "((b+1) / (a \<bullet> a)) *\<^sub>R a" in subsetD)
     apply simp_all
-    by (metis add_cancel_right_right divide_1 zero_neq_one)
+    by (metis add_cancel_right_right div_by_1 zero_neq_one)
   then show ?thesis by force
 qed
 
diff -r de5cd9217d4c -r eabf80376aab src/HOL/Analysis/Derivative.thy
--- a/src/HOL/Analysis/Derivative.thy	Sun Oct 16 09:31:03 2016 +0200
+++ b/src/HOL/Analysis/Derivative.thy	Sun Oct 16 09:31:04 2016 +0200
@@ -698,7 +698,7 @@
     "(\<lambda>xa. f' x xa - (f b - f a) / (b - a) * xa) = (\<lambda>v. 0)" ..
   then show ?thesis
     by (metis (hide_lams) assms(1) diff_gt_0_iff_gt eq_iff_diff_eq_0
-      zero_less_mult_iff nonzero_mult_divide_cancel_right not_real_square_gt_zero
+      zero_less_mult_iff nonzero_mult_div_cancel_right not_real_square_gt_zero
       times_divide_eq_left)
 qed
 
diff -r de5cd9217d4c -r eabf80376aab src/HOL/Analysis/Polytope.thy
--- a/src/HOL/Analysis/Polytope.thy	Sun Oct 16 09:31:03 2016 +0200
+++ b/src/HOL/Analysis/Polytope.thy	Sun Oct 16 09:31:04 2016 +0200
@@ -2603,7 +2603,7 @@
       by (meson \<open>0 < a\<close> divide_less_eq floor_unique_iff)
     have "?n * a \<le> a + x"
       apply (simp add: algebra_simps)
-      by (metis \<open>0 < a\<close> floor_correct less_irrefl nonzero_mult_divide_cancel_left real_mult_le_cancel_iff2 times_divide_eq_right)
+      by (metis \<open>0 < a\<close> floor_correct less_irrefl nonzero_mult_div_cancel_left real_mult_le_cancel_iff2 times_divide_eq_right)
     also have "... < y"
       by (rule 1)
     finally have "?n * a < y" .
@@ -2616,7 +2616,7 @@
       by (meson \<open>0 < a\<close> divide_less_eq floor_unique_iff)
     have "?n * a \<le> a + y"
       apply (simp add: algebra_simps)
-      by (metis \<open>0 < a\<close> floor_correct less_irrefl nonzero_mult_divide_cancel_left real_mult_le_cancel_iff2 times_divide_eq_right)
+      by (metis \<open>0 < a\<close> floor_correct less_irrefl nonzero_mult_div_cancel_left real_mult_le_cancel_iff2 times_divide_eq_right)
     also have "... < x"
       by (rule 2)
     finally have "?n * a < x" .
diff -r de5cd9217d4c -r eabf80376aab src/HOL/Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Analysis/Topology_Euclidean_Space.thy	Sun Oct 16 09:31:03 2016 +0200
+++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy	Sun Oct 16 09:31:04 2016 +0200
@@ -3668,7 +3668,7 @@
   apply (cases "e < 0")
   apply (simp add: divide_simps)
   apply (rule subset_cball)
-  apply (metis divide_1 frac_le not_le order_refl zero_less_one)
+  apply (metis div_by_1 frac_le not_le order_refl zero_less_one)
   done
 
 lemma cball_divide_subset_numeral: "cball x (e / numeral w) \<subseteq> cball x e"
diff -r de5cd9217d4c -r eabf80376aab src/HOL/Binomial.thy
--- a/src/HOL/Binomial.thy	Sun Oct 16 09:31:03 2016 +0200
+++ b/src/HOL/Binomial.thy	Sun Oct 16 09:31:04 2016 +0200
@@ -407,7 +407,7 @@
   assumes "k \<le> n"
   shows "n choose k = fact n div (fact k * fact (n - k))"
   using binomial_fact_lemma [OF assms]
-  by (metis fact_nonzero mult_eq_0_iff nonzero_mult_divide_cancel_left)
+  by (metis fact_nonzero mult_eq_0_iff nonzero_mult_div_cancel_left)
 
 lemma binomial_fact:
   assumes kn: "k \<le> n"
diff -r de5cd9217d4c -r eabf80376aab src/HOL/Decision_Procs/Approximation.thy
--- a/src/HOL/Decision_Procs/Approximation.thy	Sun Oct 16 09:31:03 2016 +0200
+++ b/src/HOL/Decision_Procs/Approximation.thy	Sun Oct 16 09:31:04 2016 +0200
@@ -2224,7 +2224,7 @@
 proof -
   have "x \<noteq> 0" using assms by auto
   have "x + y = x * (1 + y / x)"
-    unfolding distrib_left times_divide_eq_right nonzero_mult_divide_cancel_left[OF \<open>x \<noteq> 0\<close>]
+    unfolding distrib_left times_divide_eq_right nonzero_mult_div_cancel_left[OF \<open>x \<noteq> 0\<close>]
     by auto
   moreover
   have "0 < y / x" using assms by auto
diff -r de5cd9217d4c -r eabf80376aab src/HOL/Decision_Procs/Ferrack.thy
--- a/src/HOL/Decision_Procs/Ferrack.thy	Sun Oct 16 09:31:03 2016 +0200
+++ b/src/HOL/Decision_Procs/Ferrack.thy	Sun Oct 16 09:31:04 2016 +0200
@@ -1596,7 +1596,7 @@
     using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp
   also have "\<dots> \<longleftrightarrow> ?n * (real_of_int c * (?t / ?n)) + ?n*(?N x e) < 0"
     by (simp only: pos_less_divide_eq[OF np, where a="real_of_int c *(?t/?n) + (?N x e)"
-      and b="0", simplified divide_zero_left]) (simp only: algebra_simps)
+      and b="0", simplified div_0]) (simp only: algebra_simps)
   also have "\<dots> \<longleftrightarrow> real_of_int c * ?t + ?n * (?N x e) < 0" using np by simp
   finally show ?case using nbt nb by (simp add: algebra_simps)
 next
@@ -1606,7 +1606,7 @@
     using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp
   also have "\<dots> = (?n*(real_of_int c *(?t/?n)) + ?n*(?N x e) \<le> 0)"
     by (simp only: pos_le_divide_eq[OF np, where a="real_of_int c *(?t/?n) + (?N x e)"
-      and b="0", simplified divide_zero_left]) (simp only: algebra_simps)
+      and b="0", simplified div_0]) (simp only: algebra_simps)
   also have "\<dots> = (real_of_int c *?t + ?n* (?N x e) \<le> 0)" using np by simp
   finally show ?case using nbt nb by (simp add: algebra_simps)
 next
@@ -1616,7 +1616,7 @@
     using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp
   also have "\<dots> \<longleftrightarrow> ?n * (real_of_int c * (?t / ?n)) + ?n * ?N x e > 0"
     by (simp only: pos_divide_less_eq[OF np, where a="real_of_int c *(?t/?n) + (?N x e)"
-      and b="0", simplified divide_zero_left]) (simp only: algebra_simps)
+      and b="0", simplified div_0]) (simp only: algebra_simps)
   also have "\<dots> \<longleftrightarrow> real_of_int c * ?t + ?n * ?N x e > 0" using np by simp
   finally show ?case using nbt nb by (simp add: algebra_simps)
 next
@@ -1626,7 +1626,7 @@
     using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp
   also have "\<dots> \<longleftrightarrow> ?n * (real_of_int c * (?t / ?n)) + ?n * ?N x e \<ge> 0"
     by (simp only: pos_divide_le_eq[OF np, where a="real_of_int c *(?t/?n) + (?N x e)"
-      and b="0", simplified divide_zero_left]) (simp only: algebra_simps)
+      and b="0", simplified div_0]) (simp only: algebra_simps)
   also have "\<dots> \<longleftrightarrow> real_of_int c * ?t + ?n * ?N x e \<ge> 0" using np by simp
   finally show ?case using nbt nb by (simp add: algebra_simps)
 next
@@ -1637,7 +1637,7 @@
     using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp
   also have "\<dots> \<longleftrightarrow> ?n * (real_of_int c * (?t / ?n)) + ?n * ?N x e = 0"
     by (simp only: nonzero_eq_divide_eq[OF np, where a="real_of_int c *(?t/?n) + (?N x e)"
-      and b="0", simplified divide_zero_left]) (simp only: algebra_simps)
+      and b="0", simplified div_0]) (simp only: algebra_simps)
   also have "\<dots> \<longleftrightarrow> real_of_int c * ?t + ?n * ?N x e = 0" using np by simp
   finally show ?case using nbt nb by (simp add: algebra_simps)
 next
@@ -1647,7 +1647,7 @@
     using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp
   also have "\<dots> \<longleftrightarrow> ?n * (real_of_int c * (?t / ?n)) + ?n * ?N x e \<noteq> 0"
     by (simp only: nonzero_eq_divide_eq[OF np, where a="real_of_int c *(?t/?n) + (?N x e)"
-      and b="0", simplified divide_zero_left]) (simp only: algebra_simps)
+      and b="0", simplified div_0]) (simp only: algebra_simps)
   also have "\<dots> \<longleftrightarrow> real_of_int c * ?t + ?n * ?N x e \<noteq> 0" using np by simp
   finally show ?case using nbt nb by (simp add: algebra_simps)
 qed(simp_all add: nbt numbound0_I[where bs ="bs" and b="(Inum (x#bs) t)/ real_of_int n" and b'="x"])
diff -r de5cd9217d4c -r eabf80376aab src/HOL/Decision_Procs/MIR.thy
--- a/src/HOL/Decision_Procs/MIR.thy	Sun Oct 16 09:31:03 2016 +0200
+++ b/src/HOL/Decision_Procs/MIR.thy	Sun Oct 16 09:31:04 2016 +0200
@@ -4412,7 +4412,7 @@
     using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp
   also have "\<dots> = (?n*(real_of_int c *(?t/?n)) + ?n*(?N x e) < 0)"
     by (simp only: pos_less_divide_eq[OF np, where a="real_of_int c *(?t/?n) + (?N x e)"
-      and b="0", simplified divide_zero_left]) (simp only: algebra_simps)
+      and b="0", simplified div_0]) (simp only: algebra_simps)
   also have "\<dots> = (real_of_int c *?t + ?n* (?N x e) < 0)"
     using np by simp
   finally show ?case using nbt nb by (simp add: algebra_simps)
@@ -4423,7 +4423,7 @@
     using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp
   also have "\<dots> = (?n*(real_of_int c *(?t/?n)) + ?n*(?N x e) \<le> 0)"
     by (simp only: pos_le_divide_eq[OF np, where a="real_of_int c *(?t/?n) + (?N x e)"
-      and b="0", simplified divide_zero_left]) (simp only: algebra_simps)
+      and b="0", simplified div_0]) (simp only: algebra_simps)
   also have "\<dots> = (real_of_int c *?t + ?n* (?N x e) \<le> 0)"
     using np by simp
   finally show ?case using nbt nb by (simp add: algebra_simps)
@@ -4434,7 +4434,7 @@
     using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp
   also have "\<dots> = (?n*(real_of_int c *(?t/?n)) + ?n*(?N x e) > 0)"
     by (simp only: pos_divide_less_eq[OF np, where a="real_of_int c *(?t/?n) + (?N x e)"
-      and b="0", simplified divide_zero_left]) (simp only: algebra_simps)
+      and b="0", simplified div_0]) (simp only: algebra_simps)
   also have "\<dots> = (real_of_int c *?t + ?n* (?N x e) > 0)"
     using np by simp
   finally show ?case using nbt nb by (simp add: algebra_simps)
@@ -4445,7 +4445,7 @@
     using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp
   also have "\<dots> = (?n*(real_of_int c *(?t/?n)) + ?n*(?N x e) \<ge> 0)"
     by (simp only: pos_divide_le_eq[OF np, where a="real_of_int c *(?t/?n) + (?N x e)"
-      and b="0", simplified divide_zero_left]) (simp only: algebra_simps)
+      and b="0", simplified div_0]) (simp only: algebra_simps)
   also have "\<dots> = (real_of_int c *?t + ?n* (?N x e) \<ge> 0)"
     using np by simp
   finally show ?case using nbt nb by (simp add: algebra_simps)
@@ -4457,7 +4457,7 @@
     using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp
   also have "\<dots> = (?n*(real_of_int c *(?t/?n)) + ?n*(?N x e) = 0)"
     by (simp only: nonzero_eq_divide_eq[OF np, where a="real_of_int c *(?t/?n) + (?N x e)"
-      and b="0", simplified divide_zero_left]) (simp only: algebra_simps)
+      and b="0", simplified div_0]) (simp only: algebra_simps)
   also have "\<dots> = (real_of_int c *?t + ?n* (?N x e) = 0)"
     using np by simp
   finally show ?case using nbt nb by (simp add: algebra_simps)
@@ -4469,7 +4469,7 @@
     using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp
   also have "\<dots> = (?n*(real_of_int c *(?t/?n)) + ?n*(?N x e) \<noteq> 0)"
     by (simp only: nonzero_eq_divide_eq[OF np, where a="real_of_int c *(?t/?n) + (?N x e)"
-      and b="0", simplified divide_zero_left]) (simp only: algebra_simps)
+      and b="0", simplified div_0]) (simp only: algebra_simps)
   also have "\<dots> = (real_of_int c *?t + ?n* (?N x e) \<noteq> 0)"
     using np by simp
   finally show ?case using nbt nb by (simp add: algebra_simps)
diff -r de5cd9217d4c -r eabf80376aab src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
--- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Sun Oct 16 09:31:03 2016 +0200
+++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Sun Oct 16 09:31:04 2016 +0200
@@ -2704,7 +2704,7 @@
       using cd mult_cancel_left[of "2 * ?c * ?d" "?a * (- (?d * ?t + ?c* ?s)/ (2 * ?c * ?d)) + ?r" 0]
       by simp
     also have "\<dots> \<longleftrightarrow> ?a * (- (?d * ?t + ?c* ?s )) + 2 * ?c * ?d * ?r = 0"
-      using nonzero_mult_divide_cancel_left [OF cd2] cd
+      using nonzero_mult_div_cancel_left [OF cd2] cd
       by (simp add: algebra_simps diff_divide_distrib del: distrib_right)
     finally show ?thesis
       using cd
@@ -2811,7 +2811,7 @@
       using cd mult_cancel_left[of "2 * ?c * ?d" "?a * (- (?d * ?t + ?c* ?s)/ (2*?c*?d)) + ?r" 0]
       by simp
     also have "\<dots> \<longleftrightarrow> ?a * (- (?d * ?t + ?c* ?s )) + 2*?c*?d*?r \<noteq> 0"
-      using nonzero_mult_divide_cancel_left[OF cd2] cd
+      using nonzero_mult_div_cancel_left[OF cd2] cd
       by (simp add: algebra_simps diff_divide_distrib del: distrib_right)
     finally show ?thesis
       using cd
@@ -2899,7 +2899,7 @@
         mult_less_cancel_left_disj[of "2 * ?c * ?d" "?a * (- (?d * ?t + ?c* ?s)/ (2*?c*?d)) + ?r" 0]
       by simp
     also have "\<dots> \<longleftrightarrow> ?a * (- (?d * ?t + ?c* ?s )) + 2*?c*?d*?r < 0"
-      using nonzero_mult_divide_cancel_left[of "2*?c*?d"] c d
+      using nonzero_mult_div_cancel_left[of "2*?c*?d"] c d
       by (simp add: algebra_simps diff_divide_distrib del: distrib_right)
     finally show ?thesis
       using cd c d nc nd cd2'
@@ -2923,7 +2923,7 @@
         mult_less_cancel_left_disj[of "2 * ?c * ?d" 0 "?a * (- (?d * ?t + ?c* ?s)/ (2*?c*?d)) + ?r"]
       by simp
     also have "\<dots> \<longleftrightarrow> ?a * ((?d * ?t + ?c* ?s )) - 2 * ?c * ?d * ?r < 0"
-      using nonzero_mult_divide_cancel_left[of "2 * ?c * ?d"] c d
+      using nonzero_mult_div_cancel_left[of "2 * ?c * ?d"] c d
       by (simp add: algebra_simps diff_divide_distrib del: distrib_right)
     finally show ?thesis
       using cd c d nc nd
@@ -2946,7 +2946,7 @@
         order_less_not_sym[OF c'']
       by simp
     also have "\<dots> \<longleftrightarrow> - ?a * ?t + 2 * ?c * ?r < 0"
-      using nonzero_mult_divide_cancel_left[OF c'] \<open>?c > 0\<close>
+      using nonzero_mult_div_cancel_left[OF c'] \<open>?c > 0\<close>
       by (simp add: algebra_simps diff_divide_distrib less_le del: distrib_right)
     finally show ?thesis
       using cd nc nd
@@ -2969,7 +2969,7 @@
         mult_less_cancel_left_disj[of "2 * ?c" 0 "?a* (- ?t / (2*?c))+ ?r"]
       by simp
     also have "\<dots> \<longleftrightarrow> ?a*?t -  2*?c *?r < 0"
-      using nonzero_mult_divide_cancel_left[OF c'] cd(1) order_less_not_sym[OF c'']
+      using nonzero_mult_div_cancel_left[OF c'] cd(1) order_less_not_sym[OF c'']
           less_imp_neq[OF c''] c''
         by (simp add: algebra_simps diff_divide_distrib del: distrib_right)
     finally show ?thesis
@@ -2993,7 +2993,7 @@
         order_less_not_sym[OF d'']
       by simp
     also have "\<dots> \<longleftrightarrow> - ?a * ?s+  2 * ?d * ?r < 0"
-      using nonzero_mult_divide_cancel_left[OF d'] cd(2)
+      using nonzero_mult_div_cancel_left[OF d'] cd(2)
       by (simp add: algebra_simps diff_divide_distrib less_le del: distrib_right)
     finally show ?thesis
       using cd nc nd
@@ -3016,7 +3016,7 @@
         mult_less_cancel_left_disj[of "2 * ?d" 0 "?a* (- ?s / (2*?d))+ ?r"]
       by simp
     also have "\<dots> \<longleftrightarrow> ?a * ?s -  2 * ?d * ?r < 0"
-      using nonzero_mult_divide_cancel_left[OF d'] cd(2) order_less_not_sym[OF d'']
+      using nonzero_mult_div_cancel_left[OF d'] cd(2) order_less_not_sym[OF d'']
           less_imp_neq[OF d''] d''
         by (simp add: algebra_simps diff_divide_distrib del: distrib_right)
     finally show ?thesis
@@ -3108,7 +3108,7 @@
         mult_le_cancel_left[of "2 * ?c * ?d" "?a * (- (?d * ?t + ?c* ?s)/ (2*?c*?d)) + ?r" 0]
       by simp
     also have "\<dots> \<longleftrightarrow> ?a * (- (?d * ?t + ?c* ?s )) + 2*?c*?d*?r \<le> 0"
-      using nonzero_mult_divide_cancel_left[of "2*?c*?d"] c d
+      using nonzero_mult_div_cancel_left[of "2*?c*?d"] c d
       by (simp add: algebra_simps diff_divide_distrib del: distrib_right)
     finally  have ?thesis using dc c d  nc nd dc'
       by (simp add: r[of "(- (?d * ?t) + - (?c *?s)) / (2 * ?c * ?d)"] msubstle_def
@@ -3133,7 +3133,7 @@
         mult_le_cancel_left[of "2 * ?c * ?d" 0 "?a * (- (?d * ?t + ?c* ?s)/ (2*?c*?d)) + ?r"]
       by simp
     also have "\<dots> \<longleftrightarrow> ?a * ((?d * ?t + ?c* ?s )) - 2 * ?c * ?d * ?r \<le> 0"
-      using nonzero_mult_divide_cancel_left[of "2 * ?c * ?d"] c d
+      using nonzero_mult_div_cancel_left[of "2 * ?c * ?d"] c d
       by (simp add: algebra_simps diff_divide_distrib del: distrib_right)
     finally  have ?thesis using dc c d  nc nd
       by (simp add: r[of "(- (?d * ?t) + - (?c *?s)) / (2 * ?c * ?d)"] msubstle_def
@@ -3157,7 +3157,7 @@
         order_less_not_sym[OF c'']
       by simp
     also have "\<dots> \<longleftrightarrow> - ?a*?t+  2*?c *?r \<le> 0"
-      using nonzero_mult_divide_cancel_left[OF c'] c
+      using nonzero_mult_div_cancel_left[OF c'] c
       by (simp add: algebra_simps diff_divide_distrib less_le del: distrib_right)
     finally have ?thesis using c d nc nd
       by (simp add: r[of "- (?t / (2*?c))"] msubstle_def Let_def
@@ -3181,7 +3181,7 @@
         mult_le_cancel_left[of "2 * ?c" 0 "?a* (- ?t / (2*?c))+ ?r"]
       by simp
     also have "\<dots> \<longleftrightarrow> ?a * ?t - 2 * ?c * ?r \<le> 0"
-      using nonzero_mult_divide_cancel_left[OF c'] c order_less_not_sym[OF c'']
+      using nonzero_mult_div_cancel_left[OF c'] c order_less_not_sym[OF c'']
           less_imp_neq[OF c''] c''
         by (simp add: algebra_simps diff_divide_distrib del: distrib_right)
     finally have ?thesis using c d nc nd
@@ -3206,7 +3206,7 @@
         order_less_not_sym[OF d'']
       by simp
     also have "\<dots> \<longleftrightarrow> - ?a * ?s + 2 * ?d * ?r \<le> 0"
-      using nonzero_mult_divide_cancel_left[OF d'] d
+      using nonzero_mult_div_cancel_left[OF d'] d
       by (simp add: algebra_simps diff_divide_distrib less_le del: distrib_right)
     finally have ?thesis using c d nc nd
       by (simp add: r[of "- (?s / (2*?d))"] msubstle_def Let_def
@@ -3230,7 +3230,7 @@
         mult_le_cancel_left[of "2 * ?d" 0 "?a* (- ?s / (2*?d))+ ?r"]
       by simp
     also have "\<dots> \<longleftrightarrow> ?a * ?s -  2 * ?d * ?r \<le> 0"
-      using nonzero_mult_divide_cancel_left[OF d'] d order_less_not_sym[OF d'']
+      using nonzero_mult_div_cancel_left[OF d'] d order_less_not_sym[OF d'']
           less_imp_neq[OF d''] d''
         by (simp add: algebra_simps diff_divide_distrib del: distrib_right)
     finally have ?thesis using c d nc nd
diff -r de5cd9217d4c -r eabf80376aab src/HOL/Decision_Procs/mir_tac.ML
--- a/src/HOL/Decision_Procs/mir_tac.ML	Sun Oct 16 09:31:03 2016 +0200
+++ b/src/HOL/Decision_Procs/mir_tac.ML	Sun Oct 16 09:31:04 2016 +0200
@@ -25,7 +25,7 @@
              @{thm of_nat_numeral},
              @{thm "of_nat_Suc"}, @{thm "of_nat_1"},
              @{thm "of_int_0"}, @{thm "of_nat_0"},
-             @{thm "divide_zero"}, 
+             @{thm "div_by_0"}, 
              @{thm "divide_divide_eq_left"}, @{thm "times_divide_eq_right"}, 
              @{thm "times_divide_eq_left"}, @{thm "divide_divide_eq_right"},
              @{thm uminus_add_conv_diff [symmetric]}, @{thm "minus_divide_left"}]
diff -r de5cd9217d4c -r eabf80376aab src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Sun Oct 16 09:31:03 2016 +0200
+++ b/src/HOL/Divides.thy	Sun Oct 16 09:31:04 2016 +0200
@@ -26,18 +26,6 @@
     using div_mult_self1 [of b 0 a] by (simp add: ac_simps div_0)
 qed (simp add: div_by_0)
 
-lemma div_by_1:
-  "a div 1 = a"
-  by (fact divide_1)
-
-lemma div_mult_self1_is_id:
-  "b \<noteq> 0 \<Longrightarrow> b * a div b = a"
-  by (fact nonzero_mult_divide_cancel_left)
-
-lemma div_mult_self2_is_id:
-  "b \<noteq> 0 \<Longrightarrow> a * b div b = a"
-  by (fact nonzero_mult_divide_cancel_right)
-
 text \<open>@{const divide} and @{const modulo}\<close>
 
 lemma div_mod_equality: "((a div b) * b + a mod b) + c = a + c"
@@ -412,7 +400,7 @@
 apply (auto simp add: dvd_def)
 apply (subgoal_tac "-(y * k) = y * - k")
  apply (simp only:)
- apply (erule div_mult_self1_is_id)
+ apply (erule nonzero_mult_div_cancel_left)
 apply simp
 done
 
@@ -420,7 +408,7 @@
 apply (case_tac "y = 0") apply simp
 apply (auto simp add: dvd_def)
 apply (subgoal_tac "y * k = -y * -k")
- apply (erule ssubst, rule div_mult_self1_is_id)
+ apply (erule ssubst, rule nonzero_mult_div_cancel_left)
  apply simp
 apply simp
 done
@@ -1817,7 +1805,7 @@
     by (cases "0::int" k rule: linorder_cases) simp_all
   then show "is_unit (unit_factor k)"
     by simp
-qed (simp_all add: sgn_times mult_sgn_abs)
+qed (simp_all add: sgn_mult mult_sgn_abs)
   
 end
   
@@ -2707,4 +2695,6 @@
   "numeral x dvd (numeral y :: 'a) \<longleftrightarrow> numeral y mod numeral x = (0 :: 'a::semiring_div)"
   by (fact dvd_eq_mod_eq_0)
 
+hide_fact (open) div_0 div_by_0
+
 end
diff -r de5cd9217d4c -r eabf80376aab src/HOL/GCD.thy
--- a/src/HOL/GCD.thy	Sun Oct 16 09:31:03 2016 +0200
+++ b/src/HOL/GCD.thy	Sun Oct 16 09:31:04 2016 +0200
@@ -356,7 +356,7 @@
   then have "gcd a b * lcm a b div lcm a b = normalize (a * b) div lcm a b"
     by (simp_all add: normalize_mult)
   with \<open>lcm a b \<noteq> 0\<close> show ?thesis
-    using nonzero_mult_divide_cancel_right [of "lcm a b" "gcd a b"] by simp
+    using nonzero_mult_div_cancel_right [of "lcm a b" "gcd a b"] by simp
 qed
 
 lemma lcm_1_left [simp]: "lcm 1 a = normalize a"
diff -r de5cd9217d4c -r eabf80376aab src/HOL/Library/Float.thy
--- a/src/HOL/Library/Float.thy	Sun Oct 16 09:31:03 2016 +0200
+++ b/src/HOL/Library/Float.thy	Sun Oct 16 09:31:04 2016 +0200
@@ -590,7 +590,7 @@
 
 qualified lemma compute_float_sgn[code]:
   "sgn (Float m1 e1) = (if 0 < m1 then 1 else if m1 < 0 then -1 else 0)"
-  by transfer (simp add: sgn_times)
+  by transfer (simp add: sgn_mult)
 
 lift_definition is_float_pos :: "float \<Rightarrow> bool" is "op < 0 :: real \<Rightarrow> bool" .
 
diff -r de5cd9217d4c -r eabf80376aab src/HOL/Library/Formal_Power_Series.thy
--- a/src/HOL/Library/Formal_Power_Series.thy	Sun Oct 16 09:31:03 2016 +0200
+++ b/src/HOL/Library/Formal_Power_Series.thy	Sun Oct 16 09:31:04 2016 +0200
@@ -3013,7 +3013,7 @@
 *)
 
 lemma fps_divide_1 [simp]: "(a :: 'a::field fps) / 1 = a"
-  by (fact divide_1)
+  by (fact div_by_1)
 
 lemma radical_divide:
   fixes a :: "'a::field_char_0 fps"
diff -r de5cd9217d4c -r eabf80376aab src/HOL/Library/Normalized_Fraction.thy
--- a/src/HOL/Library/Normalized_Fraction.thy	Sun Oct 16 09:31:03 2016 +0200
+++ b/src/HOL/Library/Normalized_Fraction.thy	Sun Oct 16 09:31:04 2016 +0200
@@ -10,7 +10,7 @@
 apply (auto simp add: dvd_def)
 apply (subgoal_tac "-(y * k) = y * - k")
 apply (simp only:)
-apply (erule nonzero_mult_divide_cancel_left)
+apply (erule nonzero_mult_div_cancel_left)
 apply simp
 done
 
diff -r de5cd9217d4c -r eabf80376aab src/HOL/Library/Polynomial_FPS.thy
--- a/src/HOL/Library/Polynomial_FPS.thy	Sun Oct 16 09:31:03 2016 +0200
+++ b/src/HOL/Library/Polynomial_FPS.thy	Sun Oct 16 09:31:04 2016 +0200
@@ -100,7 +100,7 @@
   also have "fps_of_poly \<dots> = fps_of_poly (p div q) * fps_of_poly q" 
     by (simp add: fps_of_poly_mult)
   also from nz have "\<dots> / fps_of_poly q = fps_of_poly (p div q)"
-    by (intro div_mult_self2_is_id) (auto simp: fps_of_poly_0)
+    by (intro nonzero_mult_div_cancel_right) (auto simp: fps_of_poly_0)
   finally show ?thesis ..
 qed simp
 
diff -r de5cd9217d4c -r eabf80376aab src/HOL/Library/Polynomial_Factorial.thy
--- a/src/HOL/Library/Polynomial_Factorial.thy	Sun Oct 16 09:31:03 2016 +0200
+++ b/src/HOL/Library/Polynomial_Factorial.thy	Sun Oct 16 09:31:04 2016 +0200
@@ -331,7 +331,7 @@
   from assms obtain q where p: "p = [:c:] * q" by (erule dvdE)
   moreover {
     have "smult c q = [:c:] * q" by simp
-    also have "\<dots> div [:c:] = q" by (rule nonzero_mult_divide_cancel_left) (insert False, auto)
+    also have "\<dots> div [:c:] = q" by (rule nonzero_mult_div_cancel_left) (insert False, auto)
     finally have "smult c q div [:c:] = q" .
   }
   ultimately show ?thesis by (intro poly_eqI) (auto simp: coeff_map_poly False)
diff -r de5cd9217d4c -r eabf80376aab src/HOL/Library/Stirling.thy
--- a/src/HOL/Library/Stirling.thy	Sun Oct 16 09:31:03 2016 +0200
+++ b/src/HOL/Library/Stirling.thy	Sun Oct 16 09:31:04 2016 +0200
@@ -108,7 +108,7 @@
       using Suc.hyps[OF geq1]
       by (simp only: stirling_Suc_n_1 of_nat_fact of_nat_add of_nat_mult)
     also have "\<dots> = Suc n * (\<Sum>k=1..n. fact n div k) + Suc n * fact n div Suc n"
-      by (metis nat.distinct(1) nonzero_mult_divide_cancel_left)
+      by (metis nat.distinct(1) nonzero_mult_div_cancel_left)
     also have "\<dots> = (\<Sum>k=1..n. fact (Suc n) div k) + fact (Suc n) div Suc n"
       by (simp add: setsum_distrib_left div_mult_swap dvd_fact)
     also have "\<dots> = (\<Sum>k=1..Suc n. fact (Suc n) div k)"
diff -r de5cd9217d4c -r eabf80376aab src/HOL/Nonstandard_Analysis/HDeriv.thy
--- a/src/HOL/Nonstandard_Analysis/HDeriv.thy	Sun Oct 16 09:31:03 2016 +0200
+++ b/src/HOL/Nonstandard_Analysis/HDeriv.thy	Sun Oct 16 09:31:04 2016 +0200
@@ -147,7 +147,7 @@
 apply (auto simp add: mem_infmal_iff [symmetric] add.commute)
 apply (drule_tac c = "xa - star_of x" in approx_mult1)
 apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD]
-            simp add: mult.assoc nonzero_mult_divide_cancel_right)
+            simp add: mult.assoc nonzero_mult_div_cancel_right)
 apply (drule_tac x3=D in
            HFinite_star_of [THEN [2] Infinitesimal_HFinite_mult,
              THEN mem_infmal_iff [THEN iffD1]])
@@ -417,7 +417,7 @@
   have "\<forall>w. w \<noteq> star_of x \<and> w \<approx> star_of x \<longrightarrow>
          ( *f* g) w * (w - star_of x) / (w - star_of x) \<approx>
          star_of (g x)"
-    by (simp add: isNSCont_def nonzero_mult_divide_cancel_right)
+    by (simp add: isNSCont_def nonzero_mult_div_cancel_right)
   thus ?thesis using all
     by (simp add: NSDERIV_iff2 starfun_if_eq cong: if_cong)
 qed
diff -r de5cd9217d4c -r eabf80376aab src/HOL/Number_Theory/Euclidean_Algorithm.thy
--- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Sun Oct 16 09:31:03 2016 +0200
+++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Sun Oct 16 09:31:04 2016 +0200
@@ -26,7 +26,7 @@
     "b \<noteq> 0 \<Longrightarrow> euclidean_size a \<le> euclidean_size (a * b)"
 begin
 
-lemma zero_mod_left [simp]: "0 mod a = 0"
+lemma mod_0 [simp]: "0 mod a = 0"
   using mod_div_equality [of 0 a] by simp
 
 lemma dvd_mod_iff: 
diff -r de5cd9217d4c -r eabf80376aab src/HOL/Number_Theory/Gauss.thy
--- a/src/HOL/Number_Theory/Gauss.thy	Sun Oct 16 09:31:03 2016 +0200
+++ b/src/HOL/Number_Theory/Gauss.thy	Sun Oct 16 09:31:04 2016 +0200
@@ -52,7 +52,7 @@
 qed
 
 lemma p_eq2: "int p = (2 * ((int p - 1) div 2)) + 1"
-  using odd_p p_ge_2 div_mult_self1_is_id [of 2 "p - 1"]   
+  using odd_p p_ge_2 nonzero_mult_div_cancel_left [of 2 "p - 1"]   
   by simp
 
 lemma p_odd_int: obtains z::int where "int p = 2*z+1" "0<z"
diff -r de5cd9217d4c -r eabf80376aab src/HOL/Old_Number_Theory/EvenOdd.thy
--- a/src/HOL/Old_Number_Theory/EvenOdd.thy	Sun Oct 16 09:31:03 2016 +0200
+++ b/src/HOL/Old_Number_Theory/EvenOdd.thy	Sun Oct 16 09:31:04 2016 +0200
@@ -14,6 +14,13 @@
 definition zEven :: "int set"
   where "zEven = {x. \<exists>k. x = 2 * k}"
 
+lemma in_zEven_zOdd_iff:
+  fixes k :: int
+  shows "k \<in> zEven \<longleftrightarrow> even k"
+    and "k \<in> zOdd \<longleftrightarrow> odd k"
+  by (auto simp add: zEven_def zOdd_def elim: evenE oddE)
+
+
 subsection \<open>Some useful properties about even and odd\<close>
 
 lemma zOddI [intro?]: "x = 2 * k + 1 \<Longrightarrow> x \<in> zOdd"
diff -r de5cd9217d4c -r eabf80376aab src/HOL/Old_Number_Theory/Gauss.thy
--- a/src/HOL/Old_Number_Theory/Gauss.thy	Sun Oct 16 09:31:03 2016 +0200
+++ b/src/HOL/Old_Number_Theory/Gauss.thy	Sun Oct 16 09:31:04 2016 +0200
@@ -46,16 +46,11 @@
 qed
 
 lemma p_eq: "p = (2 * (p - 1) div 2) + 1"
-  using div_mult_self1_is_id [of 2 "p - 1"] by auto
+  using nonzero_mult_div_cancel_left [of 2 "p - 1"] by auto
 
 
 lemma (in -) zodd_imp_zdiv_eq: "x \<in> zOdd ==> 2 * (x - 1) div 2 = 2 * ((x - 1) div 2)"
-  apply (frule odd_minus_one_even)
-  apply (simp add: zEven_def)
-  apply (subgoal_tac "2 \<noteq> 0")
-  apply (frule_tac b = "2 :: int" and a = "x - 1" in div_mult_self1_is_id)
-  apply (auto simp add: even_div_2_prop2)
-  done
+  by (simp add: in_zEven_zOdd_iff)
 
 
 lemma p_eq2: "p = (2 * ((p - 1) div 2)) + 1"
diff -r de5cd9217d4c -r eabf80376aab src/HOL/Old_Number_Theory/IntPrimes.thy
--- a/src/HOL/Old_Number_Theory/IntPrimes.thy	Sun Oct 16 09:31:03 2016 +0200
+++ b/src/HOL/Old_Number_Theory/IntPrimes.thy	Sun Oct 16 09:31:04 2016 +0200
@@ -227,7 +227,7 @@
 lemma zcong_zless_0:
     "0 \<le> a ==> a < m ==> [a = 0] (mod m) ==> a = 0"
   apply (unfold zcong_def dvd_def, auto)
-  apply (metis div_pos_pos_trivial linorder_not_less div_mult_self1_is_id)
+  apply (metis div_pos_pos_trivial linorder_not_less nonzero_mult_div_cancel_left)
   done
 
 lemma zcong_zless_unique:
diff -r de5cd9217d4c -r eabf80376aab src/HOL/Old_Number_Theory/Quadratic_Reciprocity.thy
--- a/src/HOL/Old_Number_Theory/Quadratic_Reciprocity.thy	Sun Oct 16 09:31:03 2016 +0200
+++ b/src/HOL/Old_Number_Theory/Quadratic_Reciprocity.thy	Sun Oct 16 09:31:04 2016 +0200
@@ -315,7 +315,7 @@
       by (rule zdiv_mono1) (insert p_g_2, auto)
     then show "b \<le> (q * a) div p"
       apply (subgoal_tac "p \<noteq> 0")
-      apply (frule div_mult_self1_is_id, force)
+      apply (frule nonzero_mult_div_cancel_left, force)
       apply (insert p_g_2, auto)
       done
   qed
@@ -349,7 +349,7 @@
       by (rule zdiv_mono1) (insert q_g_2, auto)
     then show "a \<le> (p * b) div q"
       apply (subgoal_tac "q \<noteq> 0")
-      apply (frule div_mult_self1_is_id, force)
+      apply (frule nonzero_mult_div_cancel_left, force)
       apply (insert q_g_2, auto)
       done
   qed
diff -r de5cd9217d4c -r eabf80376aab src/HOL/Probability/SPMF.thy
--- a/src/HOL/Probability/SPMF.thy	Sun Oct 16 09:31:03 2016 +0200
+++ b/src/HOL/Probability/SPMF.thy	Sun Oct 16 09:31:04 2016 +0200
@@ -2363,7 +2363,7 @@
 apply(cases "weight_spmf p > 0")
 apply(auto simp add: scale_scale_spmf min_def max_def field_simps not_le weight_spmf_lt_0 weight_spmf_eq_0 not_less weight_spmf_le_0)
 apply(subgoal_tac "1 = r'")
- apply (metis (no_types) divide_1 eq_iff measure_spmf.subprob_measure_le_1 mult.commute mult_cancel_right1)
+ apply (metis (no_types) div_by_1 eq_iff measure_spmf.subprob_measure_le_1 mult.commute mult_cancel_right1)
 apply(meson eq_iff le_divide_eq_1_pos measure_spmf.subprob_measure_le_1 mult_imp_div_pos_le order.trans)
 done
 
diff -r de5cd9217d4c -r eabf80376aab src/HOL/Quotient_Examples/Quotient_Rat.thy
--- a/src/HOL/Quotient_Examples/Quotient_Rat.thy	Sun Oct 16 09:31:03 2016 +0200
+++ b/src/HOL/Quotient_Examples/Quotient_Rat.thy	Sun Oct 16 09:31:04 2016 +0200
@@ -258,7 +258,7 @@
     fix a b :: int
     assume "b \<noteq> 0"
     then have "a * b \<le> (a div b + 1) * b * b"
-      by (metis mult.commute div_mult_self1_is_id less_int_def linorder_le_cases zdiv_mono1 zdiv_mono1_neg zle_add1_eq_le)
+      by (metis mult.commute nonzero_mult_div_cancel_left less_int_def linorder_le_cases zdiv_mono1 zdiv_mono1_neg zle_add1_eq_le)
     then show "\<exists>z::int. a * b \<le> z * b * b" by auto
   qed
 qed
diff -r de5cd9217d4c -r eabf80376aab src/HOL/Rat.thy
--- a/src/HOL/Rat.thy	Sun Oct 16 09:31:03 2016 +0200
+++ b/src/HOL/Rat.thy	Sun Oct 16 09:31:04 2016 +0200
@@ -295,10 +295,10 @@
         (q * gcd r s) * (sgn (q * s) * r * gcd p q)"
       by simp
     with assms show ?thesis
-      by (auto simp add: ac_simps sgn_times sgn_0_0)
+      by (auto simp add: ac_simps sgn_mult sgn_0_0)
   qed
   from assms show ?thesis
-    by (auto simp: normalize_def Let_def dvd_div_div_eq_mult mult.commute sgn_times
+    by (auto simp: normalize_def Let_def dvd_div_div_eq_mult mult.commute sgn_mult
         split: if_splits intro: *)
 qed
 
@@ -651,7 +651,7 @@
       @{thm True_implies_equals},
       @{thm distrib_left [where a = "numeral v" for v]},
       @{thm distrib_left [where a = "- numeral v" for v]},
-      @{thm divide_1}, @{thm divide_zero_left},
+      @{thm div_by_1}, @{thm div_0},
       @{thm times_divide_eq_right}, @{thm times_divide_eq_left},
       @{thm minus_divide_left} RS sym, @{thm minus_divide_right} RS sym,
       @{thm add_divide_distrib}, @{thm diff_divide_distrib},
diff -r de5cd9217d4c -r eabf80376aab src/HOL/Real_Vector_Spaces.thy
--- a/src/HOL/Real_Vector_Spaces.thy	Sun Oct 16 09:31:03 2016 +0200
+++ b/src/HOL/Real_Vector_Spaces.thy	Sun Oct 16 09:31:04 2016 +0200
@@ -1325,6 +1325,8 @@
   for x y :: "'a::real_normed_div_algebra"
   by (simp add: sgn_div_norm norm_mult mult.commute)
 
+hide_fact (open) sgn_mult
+
 lemma real_sgn_eq: "sgn x = x / \<bar>x\<bar>"
   for x :: real
   by (simp add: sgn_div_norm divide_inverse)
diff -r de5cd9217d4c -r eabf80376aab src/HOL/Rings.thy
--- a/src/HOL/Rings.thy	Sun Oct 16 09:31:03 2016 +0200
+++ b/src/HOL/Rings.thy	Sun Oct 16 09:31:04 2016 +0200
@@ -574,12 +574,12 @@
 text \<open>Algebraic classes with division\<close>
   
 class semidom_divide = semidom + divide +
-  assumes nonzero_mult_divide_cancel_right [simp]: "b \<noteq> 0 \<Longrightarrow> (a * b) div b = a"
-  assumes divide_zero [simp]: "a div 0 = 0"
+  assumes nonzero_mult_div_cancel_right [simp]: "b \<noteq> 0 \<Longrightarrow> (a * b) div b = a"
+  assumes div_by_0 [simp]: "a div 0 = 0"
 begin
 
-lemma nonzero_mult_divide_cancel_left [simp]: "a \<noteq> 0 \<Longrightarrow> (a * b) div a = b"
-  using nonzero_mult_divide_cancel_right [of a b] by (simp add: ac_simps)
+lemma nonzero_mult_div_cancel_left [simp]: "a \<noteq> 0 \<Longrightarrow> (a * b) div a = b"
+  using nonzero_mult_div_cancel_right [of a b] by (simp add: ac_simps)
 
 subclass semiring_no_zero_divisors_cancel
 proof
@@ -603,21 +603,21 @@
 qed
 
 lemma div_self [simp]: "a \<noteq> 0 \<Longrightarrow> a div a = 1"
-  using nonzero_mult_divide_cancel_left [of a 1] by simp
+  using nonzero_mult_div_cancel_left [of a 1] by simp
 
-lemma divide_zero_left [simp]: "0 div a = 0"
+lemma div_0 [simp]: "0 div a = 0"
 proof (cases "a = 0")
   case True
   then show ?thesis by simp
 next
   case False
   then have "a * 0 div a = 0"
-    by (rule nonzero_mult_divide_cancel_left)
+    by (rule nonzero_mult_div_cancel_left)
   then show ?thesis by simp
 qed
 
-lemma divide_1 [simp]: "a div 1 = a"
-  using nonzero_mult_divide_cancel_left [of 1 a] by simp
+lemma div_by_1 [simp]: "a div 1 = a"
+  using nonzero_mult_div_cancel_left [of 1 a] by simp
 
 end
 
@@ -952,7 +952,7 @@
   unit_mult_left_cancel unit_mult_right_cancel unit_div_cancel
   unit_eq_div1 unit_eq_div2
 
-lemma is_unit_divide_mult_cancel_left:
+lemma is_unit_div_mult_cancel_left:
   assumes "a \<noteq> 0" and "is_unit b"
   shows "a div (a * b) = 1 div b"
 proof -
@@ -961,10 +961,10 @@
   with assms show ?thesis by simp
 qed
 
-lemma is_unit_divide_mult_cancel_right:
+lemma is_unit_div_mult_cancel_right:
   assumes "a \<noteq> 0" and "is_unit b"
   shows "a div (b * a) = 1 div b"
-  using assms is_unit_divide_mult_cancel_left [of a b] by (simp add: ac_simps)
+  using assms is_unit_div_mult_cancel_left [of a b] by (simp add: ac_simps)
 
 end
 
@@ -1058,7 +1058,7 @@
 next
   case False
   then have "normalize a \<noteq> 0" by simp
-  with nonzero_mult_divide_cancel_right
+  with nonzero_mult_div_cancel_right
   have "unit_factor a * normalize a div normalize a = unit_factor a" by blast
   then show ?thesis by simp
 qed
@@ -1070,7 +1070,7 @@
 next
   case False
   then have "unit_factor a \<noteq> 0" by simp
-  with nonzero_mult_divide_cancel_left
+  with nonzero_mult_div_cancel_left
   have "unit_factor a * normalize a div unit_factor a = normalize a"
     by blast
   then show ?thesis by simp
@@ -1085,7 +1085,7 @@
   have "normalize a div a = normalize a div (unit_factor a * normalize a)"
     by simp
   also have "\<dots> = 1 div unit_factor a"
-    using False by (subst is_unit_divide_mult_cancel_right) simp_all
+    using False by (subst is_unit_div_mult_cancel_right) simp_all
   finally show ?thesis .
 qed
 
@@ -1906,7 +1906,7 @@
 lemma sgn_neg [simp]: "a < 0 \<Longrightarrow> sgn a = - 1"
   by (simp only: sgn_1_neg)
 
-lemma sgn_times: "sgn (a * b) = sgn a * sgn b"
+lemma sgn_mult: "sgn (a * b) = sgn a * sgn b"
   by (auto simp add: sgn_if zero_less_mult_iff)
 
 lemma abs_sgn: "\<bar>k\<bar> = k * sgn k"
diff -r de5cd9217d4c -r eabf80376aab src/HOL/Tools/numeral_simprocs.ML
--- a/src/HOL/Tools/numeral_simprocs.ML	Sun Oct 16 09:31:03 2016 +0200
+++ b/src/HOL/Tools/numeral_simprocs.ML	Sun Oct 16 09:31:04 2016 +0200
@@ -173,7 +173,7 @@
 
 (*Simplify 0+n, n+0, Numeral1*n, n*Numeral1, 1*x, x*1, x/1 *)
 val add_0s =  @{thms add_0_left add_0_right};
-val mult_1s = @{thms mult_1s divide_numeral_1 mult_1_left mult_1_right mult_minus1 mult_minus1_right divide_1};
+val mult_1s = @{thms mult_1s divide_numeral_1 mult_1_left mult_1_right mult_minus1 mult_minus1_right div_by_1};
 
 (* For post-simplification of the rhs of simproc-generated rules *)
 val post_simps =
@@ -184,7 +184,7 @@
      @{thm mult_minus1}, @{thm mult_minus1_right}]
 
 val field_post_simps =
-    post_simps @ [@{thm divide_zero_left}, @{thm divide_1}]
+    post_simps @ [@{thm div_0}, @{thm div_by_1}]
 
 (*Simplify inverse Numeral1*)
 val inverse_1s = [@{thm inverse_numeral_1}];
@@ -712,7 +712,7 @@
 val ths =
  [@{thm "mult_numeral_1"}, @{thm "mult_numeral_1_right"},
   @{thm "divide_numeral_1"},
-  @{thm "divide_zero"}, @{thm divide_zero_left},
+  @{thm "div_by_0"}, @{thm div_0},
   @{thm "divide_divide_eq_left"},
   @{thm "times_divide_eq_left"}, @{thm "times_divide_eq_right"},
   @{thm "times_divide_times_eq"},
diff -r de5cd9217d4c -r eabf80376aab src/HOL/ex/Simproc_Tests.thy
--- a/src/HOL/ex/Simproc_Tests.thy	Sun Oct 16 09:31:03 2016 +0200
+++ b/src/HOL/ex/Simproc_Tests.thy	Sun Oct 16 09:31:04 2016 +0200
@@ -361,7 +361,7 @@
     have "(k) / (k*y) = uu"
       by (tactic \<open>test @{context} [@{simproc divide_cancel_factor}]\<close>) fact
   next
-    assume "(if b = 0 then 0 else a * c / 1) = uu"
+    assume "(if b = 0 then 0 else a * c) = uu"
     have "(a*(b*c)) / b = uu"
       by (tactic \<open>test @{context} [@{simproc divide_cancel_factor}]\<close>) fact
   next