more standardized names
authorhaftmann
Sun Oct 16 09:31:04 2016 +0200 (2016-10-16)
changeset 64240eabf80376aab
parent 64239 de5cd9217d4c
child 64241 430d74089d4d
more standardized names
NEWS
src/HOL/Analysis/Cauchy_Integral_Theorem.thy
src/HOL/Analysis/Complex_Transcendental.thy
src/HOL/Analysis/Convex_Euclidean_Space.thy
src/HOL/Analysis/Derivative.thy
src/HOL/Analysis/Polytope.thy
src/HOL/Analysis/Topology_Euclidean_Space.thy
src/HOL/Binomial.thy
src/HOL/Decision_Procs/Approximation.thy
src/HOL/Decision_Procs/Ferrack.thy
src/HOL/Decision_Procs/MIR.thy
src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
src/HOL/Decision_Procs/mir_tac.ML
src/HOL/Divides.thy
src/HOL/GCD.thy
src/HOL/Library/Float.thy
src/HOL/Library/Formal_Power_Series.thy
src/HOL/Library/Normalized_Fraction.thy
src/HOL/Library/Polynomial_FPS.thy
src/HOL/Library/Polynomial_Factorial.thy
src/HOL/Library/Stirling.thy
src/HOL/Nonstandard_Analysis/HDeriv.thy
src/HOL/Number_Theory/Euclidean_Algorithm.thy
src/HOL/Number_Theory/Gauss.thy
src/HOL/Old_Number_Theory/EvenOdd.thy
src/HOL/Old_Number_Theory/Gauss.thy
src/HOL/Old_Number_Theory/IntPrimes.thy
src/HOL/Old_Number_Theory/Quadratic_Reciprocity.thy
src/HOL/Probability/SPMF.thy
src/HOL/Quotient_Examples/Quotient_Rat.thy
src/HOL/Rat.thy
src/HOL/Real_Vector_Spaces.thy
src/HOL/Rings.thy
src/HOL/Tools/numeral_simprocs.ML
src/HOL/ex/Simproc_Tests.thy
     1.1 --- a/NEWS	Sun Oct 16 09:31:03 2016 +0200
     1.2 +++ b/NEWS	Sun Oct 16 09:31:04 2016 +0200
     1.3 @@ -249,6 +249,21 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* Sligthly more standardized theorem names:
     1.8 +    sgn_times ~> sgn_mult
     1.9 +    sgn_mult' ~> Real_Vector_Spaces.sgn_mult
    1.10 +    divide_zero_left ~> div_0
    1.11 +    zero_mod_left ~> mod_0
    1.12 +    divide_zero ~> div_by_0
    1.13 +    divide_1 ~> div_by_1
    1.14 +    nonzero_mult_divide_cancel_left ~> nonzero_mult_div_cancel_left
    1.15 +    div_mult_self1_is_id ~> nonzero_mult_div_cancel_left
    1.16 +    nonzero_mult_divide_cancel_right ~> nonzero_mult_div_cancel_right
    1.17 +    div_mult_self2_is_id ~> nonzero_mult_div_cancel_right
    1.18 +    is_unit_divide_mult_cancel_left ~> is_unit_div_mult_cancel_left
    1.19 +    is_unit_divide_mult_cancel_right ~> is_unit_div_mult_cancel_right
    1.20 +INCOMPATIBILITY.
    1.21 +
    1.22  * Dedicated syntax LENGTH('a) for length of types.
    1.23  
    1.24  * New proof method "argo" using the built-in Argo solver based on SMT
     2.1 --- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Sun Oct 16 09:31:03 2016 +0200
     2.2 +++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Sun Oct 16 09:31:04 2016 +0200
     2.3 @@ -5106,7 +5106,7 @@
     2.4                    and x: "x \<in> {0..1}" and y: "y \<in> {0..1}" for x y n
     2.5      proof -
     2.6        have "(linepath s t x) = (linepath s t y) + 2 * of_int n * complex_of_real pi"
     2.7 -        by (metis add_divide_eq_iff complex_i_not_zero mult.commute nonzero_mult_divide_cancel_left eq)
     2.8 +        by (metis add_divide_eq_iff complex_i_not_zero mult.commute nonzero_mult_div_cancel_left eq)
     2.9        then have "s*y + t*x = s*x + (t*y + of_int n * (pi * 2))"
    2.10          by (force simp: algebra_simps linepath_def dest: arg_cong [where f=Re])
    2.11        then have st: "x \<noteq> y \<Longrightarrow> (s-t) = (of_int n * (pi * 2) / (y-x))"
     3.1 --- a/src/HOL/Analysis/Complex_Transcendental.thy	Sun Oct 16 09:31:03 2016 +0200
     3.2 +++ b/src/HOL/Analysis/Complex_Transcendental.thy	Sun Oct 16 09:31:04 2016 +0200
     3.3 @@ -1315,7 +1315,7 @@
     3.4    case False
     3.5    then have "z / of_real(norm z) = exp(\<i> * of_real(Arg z))"
     3.6      using Arg [of z]
     3.7 -    by (metis abs_norm_cancel nonzero_mult_divide_cancel_left norm_of_real zero_less_norm_iff)
     3.8 +    by (metis abs_norm_cancel nonzero_mult_div_cancel_left norm_of_real zero_less_norm_iff)
     3.9    then have "- z / of_real(norm z) = exp (\<i> * (of_real (Arg z) - pi))"
    3.10      using cis_conv_exp cis_pi
    3.11      by (auto simp: exp_diff algebra_simps)
    3.12 @@ -1918,7 +1918,7 @@
    3.13      shows "csqrt z = exp(Ln(z) / 2)"
    3.14  proof -
    3.15    have "(exp (Ln z / 2))\<^sup>2 = (exp (Ln z))"
    3.16 -    by (metis exp_double nonzero_mult_divide_cancel_left times_divide_eq_right zero_neq_numeral)
    3.17 +    by (metis exp_double nonzero_mult_div_cancel_left times_divide_eq_right zero_neq_numeral)
    3.18    also have "... = z"
    3.19      using assms exp_Ln by blast
    3.20    finally have "csqrt z = csqrt ((exp (Ln z / 2))\<^sup>2)"
     4.1 --- a/src/HOL/Analysis/Convex_Euclidean_Space.thy	Sun Oct 16 09:31:03 2016 +0200
     4.2 +++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy	Sun Oct 16 09:31:04 2016 +0200
     4.3 @@ -11985,7 +11985,7 @@
     4.4    have "UNIV \<subseteq> {x. a \<bullet> x = b} \<Longrightarrow> a = 0 \<and> b = 0"
     4.5      apply (drule_tac c = "((b+1) / (a \<bullet> a)) *\<^sub>R a" in subsetD)
     4.6      apply simp_all
     4.7 -    by (metis add_cancel_right_right divide_1 zero_neq_one)
     4.8 +    by (metis add_cancel_right_right div_by_1 zero_neq_one)
     4.9    then show ?thesis by force
    4.10  qed
    4.11  
     5.1 --- a/src/HOL/Analysis/Derivative.thy	Sun Oct 16 09:31:03 2016 +0200
     5.2 +++ b/src/HOL/Analysis/Derivative.thy	Sun Oct 16 09:31:04 2016 +0200
     5.3 @@ -698,7 +698,7 @@
     5.4      "(\<lambda>xa. f' x xa - (f b - f a) / (b - a) * xa) = (\<lambda>v. 0)" ..
     5.5    then show ?thesis
     5.6      by (metis (hide_lams) assms(1) diff_gt_0_iff_gt eq_iff_diff_eq_0
     5.7 -      zero_less_mult_iff nonzero_mult_divide_cancel_right not_real_square_gt_zero
     5.8 +      zero_less_mult_iff nonzero_mult_div_cancel_right not_real_square_gt_zero
     5.9        times_divide_eq_left)
    5.10  qed
    5.11  
     6.1 --- a/src/HOL/Analysis/Polytope.thy	Sun Oct 16 09:31:03 2016 +0200
     6.2 +++ b/src/HOL/Analysis/Polytope.thy	Sun Oct 16 09:31:04 2016 +0200
     6.3 @@ -2603,7 +2603,7 @@
     6.4        by (meson \<open>0 < a\<close> divide_less_eq floor_unique_iff)
     6.5      have "?n * a \<le> a + x"
     6.6        apply (simp add: algebra_simps)
     6.7 -      by (metis \<open>0 < a\<close> floor_correct less_irrefl nonzero_mult_divide_cancel_left real_mult_le_cancel_iff2 times_divide_eq_right)
     6.8 +      by (metis \<open>0 < a\<close> floor_correct less_irrefl nonzero_mult_div_cancel_left real_mult_le_cancel_iff2 times_divide_eq_right)
     6.9      also have "... < y"
    6.10        by (rule 1)
    6.11      finally have "?n * a < y" .
    6.12 @@ -2616,7 +2616,7 @@
    6.13        by (meson \<open>0 < a\<close> divide_less_eq floor_unique_iff)
    6.14      have "?n * a \<le> a + y"
    6.15        apply (simp add: algebra_simps)
    6.16 -      by (metis \<open>0 < a\<close> floor_correct less_irrefl nonzero_mult_divide_cancel_left real_mult_le_cancel_iff2 times_divide_eq_right)
    6.17 +      by (metis \<open>0 < a\<close> floor_correct less_irrefl nonzero_mult_div_cancel_left real_mult_le_cancel_iff2 times_divide_eq_right)
    6.18      also have "... < x"
    6.19        by (rule 2)
    6.20      finally have "?n * a < x" .
     7.1 --- a/src/HOL/Analysis/Topology_Euclidean_Space.thy	Sun Oct 16 09:31:03 2016 +0200
     7.2 +++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy	Sun Oct 16 09:31:04 2016 +0200
     7.3 @@ -3668,7 +3668,7 @@
     7.4    apply (cases "e < 0")
     7.5    apply (simp add: divide_simps)
     7.6    apply (rule subset_cball)
     7.7 -  apply (metis divide_1 frac_le not_le order_refl zero_less_one)
     7.8 +  apply (metis div_by_1 frac_le not_le order_refl zero_less_one)
     7.9    done
    7.10  
    7.11  lemma cball_divide_subset_numeral: "cball x (e / numeral w) \<subseteq> cball x e"
     8.1 --- a/src/HOL/Binomial.thy	Sun Oct 16 09:31:03 2016 +0200
     8.2 +++ b/src/HOL/Binomial.thy	Sun Oct 16 09:31:04 2016 +0200
     8.3 @@ -407,7 +407,7 @@
     8.4    assumes "k \<le> n"
     8.5    shows "n choose k = fact n div (fact k * fact (n - k))"
     8.6    using binomial_fact_lemma [OF assms]
     8.7 -  by (metis fact_nonzero mult_eq_0_iff nonzero_mult_divide_cancel_left)
     8.8 +  by (metis fact_nonzero mult_eq_0_iff nonzero_mult_div_cancel_left)
     8.9  
    8.10  lemma binomial_fact:
    8.11    assumes kn: "k \<le> n"
     9.1 --- a/src/HOL/Decision_Procs/Approximation.thy	Sun Oct 16 09:31:03 2016 +0200
     9.2 +++ b/src/HOL/Decision_Procs/Approximation.thy	Sun Oct 16 09:31:04 2016 +0200
     9.3 @@ -2224,7 +2224,7 @@
     9.4  proof -
     9.5    have "x \<noteq> 0" using assms by auto
     9.6    have "x + y = x * (1 + y / x)"
     9.7 -    unfolding distrib_left times_divide_eq_right nonzero_mult_divide_cancel_left[OF \<open>x \<noteq> 0\<close>]
     9.8 +    unfolding distrib_left times_divide_eq_right nonzero_mult_div_cancel_left[OF \<open>x \<noteq> 0\<close>]
     9.9      by auto
    9.10    moreover
    9.11    have "0 < y / x" using assms by auto
    10.1 --- a/src/HOL/Decision_Procs/Ferrack.thy	Sun Oct 16 09:31:03 2016 +0200
    10.2 +++ b/src/HOL/Decision_Procs/Ferrack.thy	Sun Oct 16 09:31:04 2016 +0200
    10.3 @@ -1596,7 +1596,7 @@
    10.4      using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp
    10.5    also have "\<dots> \<longleftrightarrow> ?n * (real_of_int c * (?t / ?n)) + ?n*(?N x e) < 0"
    10.6      by (simp only: pos_less_divide_eq[OF np, where a="real_of_int c *(?t/?n) + (?N x e)"
    10.7 -      and b="0", simplified divide_zero_left]) (simp only: algebra_simps)
    10.8 +      and b="0", simplified div_0]) (simp only: algebra_simps)
    10.9    also have "\<dots> \<longleftrightarrow> real_of_int c * ?t + ?n * (?N x e) < 0" using np by simp
   10.10    finally show ?case using nbt nb by (simp add: algebra_simps)
   10.11  next
   10.12 @@ -1606,7 +1606,7 @@
   10.13      using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp
   10.14    also have "\<dots> = (?n*(real_of_int c *(?t/?n)) + ?n*(?N x e) \<le> 0)"
   10.15      by (simp only: pos_le_divide_eq[OF np, where a="real_of_int c *(?t/?n) + (?N x e)"
   10.16 -      and b="0", simplified divide_zero_left]) (simp only: algebra_simps)
   10.17 +      and b="0", simplified div_0]) (simp only: algebra_simps)
   10.18    also have "\<dots> = (real_of_int c *?t + ?n* (?N x e) \<le> 0)" using np by simp
   10.19    finally show ?case using nbt nb by (simp add: algebra_simps)
   10.20  next
   10.21 @@ -1616,7 +1616,7 @@
   10.22      using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp
   10.23    also have "\<dots> \<longleftrightarrow> ?n * (real_of_int c * (?t / ?n)) + ?n * ?N x e > 0"
   10.24      by (simp only: pos_divide_less_eq[OF np, where a="real_of_int c *(?t/?n) + (?N x e)"
   10.25 -      and b="0", simplified divide_zero_left]) (simp only: algebra_simps)
   10.26 +      and b="0", simplified div_0]) (simp only: algebra_simps)
   10.27    also have "\<dots> \<longleftrightarrow> real_of_int c * ?t + ?n * ?N x e > 0" using np by simp
   10.28    finally show ?case using nbt nb by (simp add: algebra_simps)
   10.29  next
   10.30 @@ -1626,7 +1626,7 @@
   10.31      using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp
   10.32    also have "\<dots> \<longleftrightarrow> ?n * (real_of_int c * (?t / ?n)) + ?n * ?N x e \<ge> 0"
   10.33      by (simp only: pos_divide_le_eq[OF np, where a="real_of_int c *(?t/?n) + (?N x e)"
   10.34 -      and b="0", simplified divide_zero_left]) (simp only: algebra_simps)
   10.35 +      and b="0", simplified div_0]) (simp only: algebra_simps)
   10.36    also have "\<dots> \<longleftrightarrow> real_of_int c * ?t + ?n * ?N x e \<ge> 0" using np by simp
   10.37    finally show ?case using nbt nb by (simp add: algebra_simps)
   10.38  next
   10.39 @@ -1637,7 +1637,7 @@
   10.40      using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp
   10.41    also have "\<dots> \<longleftrightarrow> ?n * (real_of_int c * (?t / ?n)) + ?n * ?N x e = 0"
   10.42      by (simp only: nonzero_eq_divide_eq[OF np, where a="real_of_int c *(?t/?n) + (?N x e)"
   10.43 -      and b="0", simplified divide_zero_left]) (simp only: algebra_simps)
   10.44 +      and b="0", simplified div_0]) (simp only: algebra_simps)
   10.45    also have "\<dots> \<longleftrightarrow> real_of_int c * ?t + ?n * ?N x e = 0" using np by simp
   10.46    finally show ?case using nbt nb by (simp add: algebra_simps)
   10.47  next
   10.48 @@ -1647,7 +1647,7 @@
   10.49      using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp
   10.50    also have "\<dots> \<longleftrightarrow> ?n * (real_of_int c * (?t / ?n)) + ?n * ?N x e \<noteq> 0"
   10.51      by (simp only: nonzero_eq_divide_eq[OF np, where a="real_of_int c *(?t/?n) + (?N x e)"
   10.52 -      and b="0", simplified divide_zero_left]) (simp only: algebra_simps)
   10.53 +      and b="0", simplified div_0]) (simp only: algebra_simps)
   10.54    also have "\<dots> \<longleftrightarrow> real_of_int c * ?t + ?n * ?N x e \<noteq> 0" using np by simp
   10.55    finally show ?case using nbt nb by (simp add: algebra_simps)
   10.56  qed(simp_all add: nbt numbound0_I[where bs ="bs" and b="(Inum (x#bs) t)/ real_of_int n" and b'="x"])
    11.1 --- a/src/HOL/Decision_Procs/MIR.thy	Sun Oct 16 09:31:03 2016 +0200
    11.2 +++ b/src/HOL/Decision_Procs/MIR.thy	Sun Oct 16 09:31:04 2016 +0200
    11.3 @@ -4412,7 +4412,7 @@
    11.4      using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp
    11.5    also have "\<dots> = (?n*(real_of_int c *(?t/?n)) + ?n*(?N x e) < 0)"
    11.6      by (simp only: pos_less_divide_eq[OF np, where a="real_of_int c *(?t/?n) + (?N x e)"
    11.7 -      and b="0", simplified divide_zero_left]) (simp only: algebra_simps)
    11.8 +      and b="0", simplified div_0]) (simp only: algebra_simps)
    11.9    also have "\<dots> = (real_of_int c *?t + ?n* (?N x e) < 0)"
   11.10      using np by simp
   11.11    finally show ?case using nbt nb by (simp add: algebra_simps)
   11.12 @@ -4423,7 +4423,7 @@
   11.13      using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp
   11.14    also have "\<dots> = (?n*(real_of_int c *(?t/?n)) + ?n*(?N x e) \<le> 0)"
   11.15      by (simp only: pos_le_divide_eq[OF np, where a="real_of_int c *(?t/?n) + (?N x e)"
   11.16 -      and b="0", simplified divide_zero_left]) (simp only: algebra_simps)
   11.17 +      and b="0", simplified div_0]) (simp only: algebra_simps)
   11.18    also have "\<dots> = (real_of_int c *?t + ?n* (?N x e) \<le> 0)"
   11.19      using np by simp
   11.20    finally show ?case using nbt nb by (simp add: algebra_simps)
   11.21 @@ -4434,7 +4434,7 @@
   11.22      using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp
   11.23    also have "\<dots> = (?n*(real_of_int c *(?t/?n)) + ?n*(?N x e) > 0)"
   11.24      by (simp only: pos_divide_less_eq[OF np, where a="real_of_int c *(?t/?n) + (?N x e)"
   11.25 -      and b="0", simplified divide_zero_left]) (simp only: algebra_simps)
   11.26 +      and b="0", simplified div_0]) (simp only: algebra_simps)
   11.27    also have "\<dots> = (real_of_int c *?t + ?n* (?N x e) > 0)"
   11.28      using np by simp
   11.29    finally show ?case using nbt nb by (simp add: algebra_simps)
   11.30 @@ -4445,7 +4445,7 @@
   11.31      using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp
   11.32    also have "\<dots> = (?n*(real_of_int c *(?t/?n)) + ?n*(?N x e) \<ge> 0)"
   11.33      by (simp only: pos_divide_le_eq[OF np, where a="real_of_int c *(?t/?n) + (?N x e)"
   11.34 -      and b="0", simplified divide_zero_left]) (simp only: algebra_simps)
   11.35 +      and b="0", simplified div_0]) (simp only: algebra_simps)
   11.36    also have "\<dots> = (real_of_int c *?t + ?n* (?N x e) \<ge> 0)"
   11.37      using np by simp
   11.38    finally show ?case using nbt nb by (simp add: algebra_simps)
   11.39 @@ -4457,7 +4457,7 @@
   11.40      using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp
   11.41    also have "\<dots> = (?n*(real_of_int c *(?t/?n)) + ?n*(?N x e) = 0)"
   11.42      by (simp only: nonzero_eq_divide_eq[OF np, where a="real_of_int c *(?t/?n) + (?N x e)"
   11.43 -      and b="0", simplified divide_zero_left]) (simp only: algebra_simps)
   11.44 +      and b="0", simplified div_0]) (simp only: algebra_simps)
   11.45    also have "\<dots> = (real_of_int c *?t + ?n* (?N x e) = 0)"
   11.46      using np by simp
   11.47    finally show ?case using nbt nb by (simp add: algebra_simps)
   11.48 @@ -4469,7 +4469,7 @@
   11.49      using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp
   11.50    also have "\<dots> = (?n*(real_of_int c *(?t/?n)) + ?n*(?N x e) \<noteq> 0)"
   11.51      by (simp only: nonzero_eq_divide_eq[OF np, where a="real_of_int c *(?t/?n) + (?N x e)"
   11.52 -      and b="0", simplified divide_zero_left]) (simp only: algebra_simps)
   11.53 +      and b="0", simplified div_0]) (simp only: algebra_simps)
   11.54    also have "\<dots> = (real_of_int c *?t + ?n* (?N x e) \<noteq> 0)"
   11.55      using np by simp
   11.56    finally show ?case using nbt nb by (simp add: algebra_simps)
    12.1 --- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Sun Oct 16 09:31:03 2016 +0200
    12.2 +++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Sun Oct 16 09:31:04 2016 +0200
    12.3 @@ -2704,7 +2704,7 @@
    12.4        using cd mult_cancel_left[of "2 * ?c * ?d" "?a * (- (?d * ?t + ?c* ?s)/ (2 * ?c * ?d)) + ?r" 0]
    12.5        by simp
    12.6      also have "\<dots> \<longleftrightarrow> ?a * (- (?d * ?t + ?c* ?s )) + 2 * ?c * ?d * ?r = 0"
    12.7 -      using nonzero_mult_divide_cancel_left [OF cd2] cd
    12.8 +      using nonzero_mult_div_cancel_left [OF cd2] cd
    12.9        by (simp add: algebra_simps diff_divide_distrib del: distrib_right)
   12.10      finally show ?thesis
   12.11        using cd
   12.12 @@ -2811,7 +2811,7 @@
   12.13        using cd mult_cancel_left[of "2 * ?c * ?d" "?a * (- (?d * ?t + ?c* ?s)/ (2*?c*?d)) + ?r" 0]
   12.14        by simp
   12.15      also have "\<dots> \<longleftrightarrow> ?a * (- (?d * ?t + ?c* ?s )) + 2*?c*?d*?r \<noteq> 0"
   12.16 -      using nonzero_mult_divide_cancel_left[OF cd2] cd
   12.17 +      using nonzero_mult_div_cancel_left[OF cd2] cd
   12.18        by (simp add: algebra_simps diff_divide_distrib del: distrib_right)
   12.19      finally show ?thesis
   12.20        using cd
   12.21 @@ -2899,7 +2899,7 @@
   12.22          mult_less_cancel_left_disj[of "2 * ?c * ?d" "?a * (- (?d * ?t + ?c* ?s)/ (2*?c*?d)) + ?r" 0]
   12.23        by simp
   12.24      also have "\<dots> \<longleftrightarrow> ?a * (- (?d * ?t + ?c* ?s )) + 2*?c*?d*?r < 0"
   12.25 -      using nonzero_mult_divide_cancel_left[of "2*?c*?d"] c d
   12.26 +      using nonzero_mult_div_cancel_left[of "2*?c*?d"] c d
   12.27        by (simp add: algebra_simps diff_divide_distrib del: distrib_right)
   12.28      finally show ?thesis
   12.29        using cd c d nc nd cd2'
   12.30 @@ -2923,7 +2923,7 @@
   12.31          mult_less_cancel_left_disj[of "2 * ?c * ?d" 0 "?a * (- (?d * ?t + ?c* ?s)/ (2*?c*?d)) + ?r"]
   12.32        by simp
   12.33      also have "\<dots> \<longleftrightarrow> ?a * ((?d * ?t + ?c* ?s )) - 2 * ?c * ?d * ?r < 0"
   12.34 -      using nonzero_mult_divide_cancel_left[of "2 * ?c * ?d"] c d
   12.35 +      using nonzero_mult_div_cancel_left[of "2 * ?c * ?d"] c d
   12.36        by (simp add: algebra_simps diff_divide_distrib del: distrib_right)
   12.37      finally show ?thesis
   12.38        using cd c d nc nd
   12.39 @@ -2946,7 +2946,7 @@
   12.40          order_less_not_sym[OF c'']
   12.41        by simp
   12.42      also have "\<dots> \<longleftrightarrow> - ?a * ?t + 2 * ?c * ?r < 0"
   12.43 -      using nonzero_mult_divide_cancel_left[OF c'] \<open>?c > 0\<close>
   12.44 +      using nonzero_mult_div_cancel_left[OF c'] \<open>?c > 0\<close>
   12.45        by (simp add: algebra_simps diff_divide_distrib less_le del: distrib_right)
   12.46      finally show ?thesis
   12.47        using cd nc nd
   12.48 @@ -2969,7 +2969,7 @@
   12.49          mult_less_cancel_left_disj[of "2 * ?c" 0 "?a* (- ?t / (2*?c))+ ?r"]
   12.50        by simp
   12.51      also have "\<dots> \<longleftrightarrow> ?a*?t -  2*?c *?r < 0"
   12.52 -      using nonzero_mult_divide_cancel_left[OF c'] cd(1) order_less_not_sym[OF c'']
   12.53 +      using nonzero_mult_div_cancel_left[OF c'] cd(1) order_less_not_sym[OF c'']
   12.54            less_imp_neq[OF c''] c''
   12.55          by (simp add: algebra_simps diff_divide_distrib del: distrib_right)
   12.56      finally show ?thesis
   12.57 @@ -2993,7 +2993,7 @@
   12.58          order_less_not_sym[OF d'']
   12.59        by simp
   12.60      also have "\<dots> \<longleftrightarrow> - ?a * ?s+  2 * ?d * ?r < 0"
   12.61 -      using nonzero_mult_divide_cancel_left[OF d'] cd(2)
   12.62 +      using nonzero_mult_div_cancel_left[OF d'] cd(2)
   12.63        by (simp add: algebra_simps diff_divide_distrib less_le del: distrib_right)
   12.64      finally show ?thesis
   12.65        using cd nc nd
   12.66 @@ -3016,7 +3016,7 @@
   12.67          mult_less_cancel_left_disj[of "2 * ?d" 0 "?a* (- ?s / (2*?d))+ ?r"]
   12.68        by simp
   12.69      also have "\<dots> \<longleftrightarrow> ?a * ?s -  2 * ?d * ?r < 0"
   12.70 -      using nonzero_mult_divide_cancel_left[OF d'] cd(2) order_less_not_sym[OF d'']
   12.71 +      using nonzero_mult_div_cancel_left[OF d'] cd(2) order_less_not_sym[OF d'']
   12.72            less_imp_neq[OF d''] d''
   12.73          by (simp add: algebra_simps diff_divide_distrib del: distrib_right)
   12.74      finally show ?thesis
   12.75 @@ -3108,7 +3108,7 @@
   12.76          mult_le_cancel_left[of "2 * ?c * ?d" "?a * (- (?d * ?t + ?c* ?s)/ (2*?c*?d)) + ?r" 0]
   12.77        by simp
   12.78      also have "\<dots> \<longleftrightarrow> ?a * (- (?d * ?t + ?c* ?s )) + 2*?c*?d*?r \<le> 0"
   12.79 -      using nonzero_mult_divide_cancel_left[of "2*?c*?d"] c d
   12.80 +      using nonzero_mult_div_cancel_left[of "2*?c*?d"] c d
   12.81        by (simp add: algebra_simps diff_divide_distrib del: distrib_right)
   12.82      finally  have ?thesis using dc c d  nc nd dc'
   12.83        by (simp add: r[of "(- (?d * ?t) + - (?c *?s)) / (2 * ?c * ?d)"] msubstle_def
   12.84 @@ -3133,7 +3133,7 @@
   12.85          mult_le_cancel_left[of "2 * ?c * ?d" 0 "?a * (- (?d * ?t + ?c* ?s)/ (2*?c*?d)) + ?r"]
   12.86        by simp
   12.87      also have "\<dots> \<longleftrightarrow> ?a * ((?d * ?t + ?c* ?s )) - 2 * ?c * ?d * ?r \<le> 0"
   12.88 -      using nonzero_mult_divide_cancel_left[of "2 * ?c * ?d"] c d
   12.89 +      using nonzero_mult_div_cancel_left[of "2 * ?c * ?d"] c d
   12.90        by (simp add: algebra_simps diff_divide_distrib del: distrib_right)
   12.91      finally  have ?thesis using dc c d  nc nd
   12.92        by (simp add: r[of "(- (?d * ?t) + - (?c *?s)) / (2 * ?c * ?d)"] msubstle_def
   12.93 @@ -3157,7 +3157,7 @@
   12.94          order_less_not_sym[OF c'']
   12.95        by simp
   12.96      also have "\<dots> \<longleftrightarrow> - ?a*?t+  2*?c *?r \<le> 0"
   12.97 -      using nonzero_mult_divide_cancel_left[OF c'] c
   12.98 +      using nonzero_mult_div_cancel_left[OF c'] c
   12.99        by (simp add: algebra_simps diff_divide_distrib less_le del: distrib_right)
  12.100      finally have ?thesis using c d nc nd
  12.101        by (simp add: r[of "- (?t / (2*?c))"] msubstle_def Let_def
  12.102 @@ -3181,7 +3181,7 @@
  12.103          mult_le_cancel_left[of "2 * ?c" 0 "?a* (- ?t / (2*?c))+ ?r"]
  12.104        by simp
  12.105      also have "\<dots> \<longleftrightarrow> ?a * ?t - 2 * ?c * ?r \<le> 0"
  12.106 -      using nonzero_mult_divide_cancel_left[OF c'] c order_less_not_sym[OF c'']
  12.107 +      using nonzero_mult_div_cancel_left[OF c'] c order_less_not_sym[OF c'']
  12.108            less_imp_neq[OF c''] c''
  12.109          by (simp add: algebra_simps diff_divide_distrib del: distrib_right)
  12.110      finally have ?thesis using c d nc nd
  12.111 @@ -3206,7 +3206,7 @@
  12.112          order_less_not_sym[OF d'']
  12.113        by simp
  12.114      also have "\<dots> \<longleftrightarrow> - ?a * ?s + 2 * ?d * ?r \<le> 0"
  12.115 -      using nonzero_mult_divide_cancel_left[OF d'] d
  12.116 +      using nonzero_mult_div_cancel_left[OF d'] d
  12.117        by (simp add: algebra_simps diff_divide_distrib less_le del: distrib_right)
  12.118      finally have ?thesis using c d nc nd
  12.119        by (simp add: r[of "- (?s / (2*?d))"] msubstle_def Let_def
  12.120 @@ -3230,7 +3230,7 @@
  12.121          mult_le_cancel_left[of "2 * ?d" 0 "?a* (- ?s / (2*?d))+ ?r"]
  12.122        by simp
  12.123      also have "\<dots> \<longleftrightarrow> ?a * ?s -  2 * ?d * ?r \<le> 0"
  12.124 -      using nonzero_mult_divide_cancel_left[OF d'] d order_less_not_sym[OF d'']
  12.125 +      using nonzero_mult_div_cancel_left[OF d'] d order_less_not_sym[OF d'']
  12.126            less_imp_neq[OF d''] d''
  12.127          by (simp add: algebra_simps diff_divide_distrib del: distrib_right)
  12.128      finally have ?thesis using c d nc nd
    13.1 --- a/src/HOL/Decision_Procs/mir_tac.ML	Sun Oct 16 09:31:03 2016 +0200
    13.2 +++ b/src/HOL/Decision_Procs/mir_tac.ML	Sun Oct 16 09:31:04 2016 +0200
    13.3 @@ -25,7 +25,7 @@
    13.4               @{thm of_nat_numeral},
    13.5               @{thm "of_nat_Suc"}, @{thm "of_nat_1"},
    13.6               @{thm "of_int_0"}, @{thm "of_nat_0"},
    13.7 -             @{thm "divide_zero"}, 
    13.8 +             @{thm "div_by_0"}, 
    13.9               @{thm "divide_divide_eq_left"}, @{thm "times_divide_eq_right"}, 
   13.10               @{thm "times_divide_eq_left"}, @{thm "divide_divide_eq_right"},
   13.11               @{thm uminus_add_conv_diff [symmetric]}, @{thm "minus_divide_left"}]
    14.1 --- a/src/HOL/Divides.thy	Sun Oct 16 09:31:03 2016 +0200
    14.2 +++ b/src/HOL/Divides.thy	Sun Oct 16 09:31:04 2016 +0200
    14.3 @@ -26,18 +26,6 @@
    14.4      using div_mult_self1 [of b 0 a] by (simp add: ac_simps div_0)
    14.5  qed (simp add: div_by_0)
    14.6  
    14.7 -lemma div_by_1:
    14.8 -  "a div 1 = a"
    14.9 -  by (fact divide_1)
   14.10 -
   14.11 -lemma div_mult_self1_is_id:
   14.12 -  "b \<noteq> 0 \<Longrightarrow> b * a div b = a"
   14.13 -  by (fact nonzero_mult_divide_cancel_left)
   14.14 -
   14.15 -lemma div_mult_self2_is_id:
   14.16 -  "b \<noteq> 0 \<Longrightarrow> a * b div b = a"
   14.17 -  by (fact nonzero_mult_divide_cancel_right)
   14.18 -
   14.19  text \<open>@{const divide} and @{const modulo}\<close>
   14.20  
   14.21  lemma div_mod_equality: "((a div b) * b + a mod b) + c = a + c"
   14.22 @@ -412,7 +400,7 @@
   14.23  apply (auto simp add: dvd_def)
   14.24  apply (subgoal_tac "-(y * k) = y * - k")
   14.25   apply (simp only:)
   14.26 - apply (erule div_mult_self1_is_id)
   14.27 + apply (erule nonzero_mult_div_cancel_left)
   14.28  apply simp
   14.29  done
   14.30  
   14.31 @@ -420,7 +408,7 @@
   14.32  apply (case_tac "y = 0") apply simp
   14.33  apply (auto simp add: dvd_def)
   14.34  apply (subgoal_tac "y * k = -y * -k")
   14.35 - apply (erule ssubst, rule div_mult_self1_is_id)
   14.36 + apply (erule ssubst, rule nonzero_mult_div_cancel_left)
   14.37   apply simp
   14.38  apply simp
   14.39  done
   14.40 @@ -1817,7 +1805,7 @@
   14.41      by (cases "0::int" k rule: linorder_cases) simp_all
   14.42    then show "is_unit (unit_factor k)"
   14.43      by simp
   14.44 -qed (simp_all add: sgn_times mult_sgn_abs)
   14.45 +qed (simp_all add: sgn_mult mult_sgn_abs)
   14.46    
   14.47  end
   14.48    
   14.49 @@ -2707,4 +2695,6 @@
   14.50    "numeral x dvd (numeral y :: 'a) \<longleftrightarrow> numeral y mod numeral x = (0 :: 'a::semiring_div)"
   14.51    by (fact dvd_eq_mod_eq_0)
   14.52  
   14.53 +hide_fact (open) div_0 div_by_0
   14.54 +
   14.55  end
    15.1 --- a/src/HOL/GCD.thy	Sun Oct 16 09:31:03 2016 +0200
    15.2 +++ b/src/HOL/GCD.thy	Sun Oct 16 09:31:04 2016 +0200
    15.3 @@ -356,7 +356,7 @@
    15.4    then have "gcd a b * lcm a b div lcm a b = normalize (a * b) div lcm a b"
    15.5      by (simp_all add: normalize_mult)
    15.6    with \<open>lcm a b \<noteq> 0\<close> show ?thesis
    15.7 -    using nonzero_mult_divide_cancel_right [of "lcm a b" "gcd a b"] by simp
    15.8 +    using nonzero_mult_div_cancel_right [of "lcm a b" "gcd a b"] by simp
    15.9  qed
   15.10  
   15.11  lemma lcm_1_left [simp]: "lcm 1 a = normalize a"
    16.1 --- a/src/HOL/Library/Float.thy	Sun Oct 16 09:31:03 2016 +0200
    16.2 +++ b/src/HOL/Library/Float.thy	Sun Oct 16 09:31:04 2016 +0200
    16.3 @@ -590,7 +590,7 @@
    16.4  
    16.5  qualified lemma compute_float_sgn[code]:
    16.6    "sgn (Float m1 e1) = (if 0 < m1 then 1 else if m1 < 0 then -1 else 0)"
    16.7 -  by transfer (simp add: sgn_times)
    16.8 +  by transfer (simp add: sgn_mult)
    16.9  
   16.10  lift_definition is_float_pos :: "float \<Rightarrow> bool" is "op < 0 :: real \<Rightarrow> bool" .
   16.11  
    17.1 --- a/src/HOL/Library/Formal_Power_Series.thy	Sun Oct 16 09:31:03 2016 +0200
    17.2 +++ b/src/HOL/Library/Formal_Power_Series.thy	Sun Oct 16 09:31:04 2016 +0200
    17.3 @@ -3013,7 +3013,7 @@
    17.4  *)
    17.5  
    17.6  lemma fps_divide_1 [simp]: "(a :: 'a::field fps) / 1 = a"
    17.7 -  by (fact divide_1)
    17.8 +  by (fact div_by_1)
    17.9  
   17.10  lemma radical_divide:
   17.11    fixes a :: "'a::field_char_0 fps"
    18.1 --- a/src/HOL/Library/Normalized_Fraction.thy	Sun Oct 16 09:31:03 2016 +0200
    18.2 +++ b/src/HOL/Library/Normalized_Fraction.thy	Sun Oct 16 09:31:04 2016 +0200
    18.3 @@ -10,7 +10,7 @@
    18.4  apply (auto simp add: dvd_def)
    18.5  apply (subgoal_tac "-(y * k) = y * - k")
    18.6  apply (simp only:)
    18.7 -apply (erule nonzero_mult_divide_cancel_left)
    18.8 +apply (erule nonzero_mult_div_cancel_left)
    18.9  apply simp
   18.10  done
   18.11  
    19.1 --- a/src/HOL/Library/Polynomial_FPS.thy	Sun Oct 16 09:31:03 2016 +0200
    19.2 +++ b/src/HOL/Library/Polynomial_FPS.thy	Sun Oct 16 09:31:04 2016 +0200
    19.3 @@ -100,7 +100,7 @@
    19.4    also have "fps_of_poly \<dots> = fps_of_poly (p div q) * fps_of_poly q" 
    19.5      by (simp add: fps_of_poly_mult)
    19.6    also from nz have "\<dots> / fps_of_poly q = fps_of_poly (p div q)"
    19.7 -    by (intro div_mult_self2_is_id) (auto simp: fps_of_poly_0)
    19.8 +    by (intro nonzero_mult_div_cancel_right) (auto simp: fps_of_poly_0)
    19.9    finally show ?thesis ..
   19.10  qed simp
   19.11  
    20.1 --- a/src/HOL/Library/Polynomial_Factorial.thy	Sun Oct 16 09:31:03 2016 +0200
    20.2 +++ b/src/HOL/Library/Polynomial_Factorial.thy	Sun Oct 16 09:31:04 2016 +0200
    20.3 @@ -331,7 +331,7 @@
    20.4    from assms obtain q where p: "p = [:c:] * q" by (erule dvdE)
    20.5    moreover {
    20.6      have "smult c q = [:c:] * q" by simp
    20.7 -    also have "\<dots> div [:c:] = q" by (rule nonzero_mult_divide_cancel_left) (insert False, auto)
    20.8 +    also have "\<dots> div [:c:] = q" by (rule nonzero_mult_div_cancel_left) (insert False, auto)
    20.9      finally have "smult c q div [:c:] = q" .
   20.10    }
   20.11    ultimately show ?thesis by (intro poly_eqI) (auto simp: coeff_map_poly False)
    21.1 --- a/src/HOL/Library/Stirling.thy	Sun Oct 16 09:31:03 2016 +0200
    21.2 +++ b/src/HOL/Library/Stirling.thy	Sun Oct 16 09:31:04 2016 +0200
    21.3 @@ -108,7 +108,7 @@
    21.4        using Suc.hyps[OF geq1]
    21.5        by (simp only: stirling_Suc_n_1 of_nat_fact of_nat_add of_nat_mult)
    21.6      also have "\<dots> = Suc n * (\<Sum>k=1..n. fact n div k) + Suc n * fact n div Suc n"
    21.7 -      by (metis nat.distinct(1) nonzero_mult_divide_cancel_left)
    21.8 +      by (metis nat.distinct(1) nonzero_mult_div_cancel_left)
    21.9      also have "\<dots> = (\<Sum>k=1..n. fact (Suc n) div k) + fact (Suc n) div Suc n"
   21.10        by (simp add: setsum_distrib_left div_mult_swap dvd_fact)
   21.11      also have "\<dots> = (\<Sum>k=1..Suc n. fact (Suc n) div k)"
    22.1 --- a/src/HOL/Nonstandard_Analysis/HDeriv.thy	Sun Oct 16 09:31:03 2016 +0200
    22.2 +++ b/src/HOL/Nonstandard_Analysis/HDeriv.thy	Sun Oct 16 09:31:04 2016 +0200
    22.3 @@ -147,7 +147,7 @@
    22.4  apply (auto simp add: mem_infmal_iff [symmetric] add.commute)
    22.5  apply (drule_tac c = "xa - star_of x" in approx_mult1)
    22.6  apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD]
    22.7 -            simp add: mult.assoc nonzero_mult_divide_cancel_right)
    22.8 +            simp add: mult.assoc nonzero_mult_div_cancel_right)
    22.9  apply (drule_tac x3=D in
   22.10             HFinite_star_of [THEN [2] Infinitesimal_HFinite_mult,
   22.11               THEN mem_infmal_iff [THEN iffD1]])
   22.12 @@ -417,7 +417,7 @@
   22.13    have "\<forall>w. w \<noteq> star_of x \<and> w \<approx> star_of x \<longrightarrow>
   22.14           ( *f* g) w * (w - star_of x) / (w - star_of x) \<approx>
   22.15           star_of (g x)"
   22.16 -    by (simp add: isNSCont_def nonzero_mult_divide_cancel_right)
   22.17 +    by (simp add: isNSCont_def nonzero_mult_div_cancel_right)
   22.18    thus ?thesis using all
   22.19      by (simp add: NSDERIV_iff2 starfun_if_eq cong: if_cong)
   22.20  qed
    23.1 --- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Sun Oct 16 09:31:03 2016 +0200
    23.2 +++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Sun Oct 16 09:31:04 2016 +0200
    23.3 @@ -26,7 +26,7 @@
    23.4      "b \<noteq> 0 \<Longrightarrow> euclidean_size a \<le> euclidean_size (a * b)"
    23.5  begin
    23.6  
    23.7 -lemma zero_mod_left [simp]: "0 mod a = 0"
    23.8 +lemma mod_0 [simp]: "0 mod a = 0"
    23.9    using mod_div_equality [of 0 a] by simp
   23.10  
   23.11  lemma dvd_mod_iff: 
    24.1 --- a/src/HOL/Number_Theory/Gauss.thy	Sun Oct 16 09:31:03 2016 +0200
    24.2 +++ b/src/HOL/Number_Theory/Gauss.thy	Sun Oct 16 09:31:04 2016 +0200
    24.3 @@ -52,7 +52,7 @@
    24.4  qed
    24.5  
    24.6  lemma p_eq2: "int p = (2 * ((int p - 1) div 2)) + 1"
    24.7 -  using odd_p p_ge_2 div_mult_self1_is_id [of 2 "p - 1"]   
    24.8 +  using odd_p p_ge_2 nonzero_mult_div_cancel_left [of 2 "p - 1"]   
    24.9    by simp
   24.10  
   24.11  lemma p_odd_int: obtains z::int where "int p = 2*z+1" "0<z"
    25.1 --- a/src/HOL/Old_Number_Theory/EvenOdd.thy	Sun Oct 16 09:31:03 2016 +0200
    25.2 +++ b/src/HOL/Old_Number_Theory/EvenOdd.thy	Sun Oct 16 09:31:04 2016 +0200
    25.3 @@ -14,6 +14,13 @@
    25.4  definition zEven :: "int set"
    25.5    where "zEven = {x. \<exists>k. x = 2 * k}"
    25.6  
    25.7 +lemma in_zEven_zOdd_iff:
    25.8 +  fixes k :: int
    25.9 +  shows "k \<in> zEven \<longleftrightarrow> even k"
   25.10 +    and "k \<in> zOdd \<longleftrightarrow> odd k"
   25.11 +  by (auto simp add: zEven_def zOdd_def elim: evenE oddE)
   25.12 +
   25.13 +
   25.14  subsection \<open>Some useful properties about even and odd\<close>
   25.15  
   25.16  lemma zOddI [intro?]: "x = 2 * k + 1 \<Longrightarrow> x \<in> zOdd"
    26.1 --- a/src/HOL/Old_Number_Theory/Gauss.thy	Sun Oct 16 09:31:03 2016 +0200
    26.2 +++ b/src/HOL/Old_Number_Theory/Gauss.thy	Sun Oct 16 09:31:04 2016 +0200
    26.3 @@ -46,16 +46,11 @@
    26.4  qed
    26.5  
    26.6  lemma p_eq: "p = (2 * (p - 1) div 2) + 1"
    26.7 -  using div_mult_self1_is_id [of 2 "p - 1"] by auto
    26.8 +  using nonzero_mult_div_cancel_left [of 2 "p - 1"] by auto
    26.9  
   26.10  
   26.11  lemma (in -) zodd_imp_zdiv_eq: "x \<in> zOdd ==> 2 * (x - 1) div 2 = 2 * ((x - 1) div 2)"
   26.12 -  apply (frule odd_minus_one_even)
   26.13 -  apply (simp add: zEven_def)
   26.14 -  apply (subgoal_tac "2 \<noteq> 0")
   26.15 -  apply (frule_tac b = "2 :: int" and a = "x - 1" in div_mult_self1_is_id)
   26.16 -  apply (auto simp add: even_div_2_prop2)
   26.17 -  done
   26.18 +  by (simp add: in_zEven_zOdd_iff)
   26.19  
   26.20  
   26.21  lemma p_eq2: "p = (2 * ((p - 1) div 2)) + 1"
    27.1 --- a/src/HOL/Old_Number_Theory/IntPrimes.thy	Sun Oct 16 09:31:03 2016 +0200
    27.2 +++ b/src/HOL/Old_Number_Theory/IntPrimes.thy	Sun Oct 16 09:31:04 2016 +0200
    27.3 @@ -227,7 +227,7 @@
    27.4  lemma zcong_zless_0:
    27.5      "0 \<le> a ==> a < m ==> [a = 0] (mod m) ==> a = 0"
    27.6    apply (unfold zcong_def dvd_def, auto)
    27.7 -  apply (metis div_pos_pos_trivial linorder_not_less div_mult_self1_is_id)
    27.8 +  apply (metis div_pos_pos_trivial linorder_not_less nonzero_mult_div_cancel_left)
    27.9    done
   27.10  
   27.11  lemma zcong_zless_unique:
    28.1 --- a/src/HOL/Old_Number_Theory/Quadratic_Reciprocity.thy	Sun Oct 16 09:31:03 2016 +0200
    28.2 +++ b/src/HOL/Old_Number_Theory/Quadratic_Reciprocity.thy	Sun Oct 16 09:31:04 2016 +0200
    28.3 @@ -315,7 +315,7 @@
    28.4        by (rule zdiv_mono1) (insert p_g_2, auto)
    28.5      then show "b \<le> (q * a) div p"
    28.6        apply (subgoal_tac "p \<noteq> 0")
    28.7 -      apply (frule div_mult_self1_is_id, force)
    28.8 +      apply (frule nonzero_mult_div_cancel_left, force)
    28.9        apply (insert p_g_2, auto)
   28.10        done
   28.11    qed
   28.12 @@ -349,7 +349,7 @@
   28.13        by (rule zdiv_mono1) (insert q_g_2, auto)
   28.14      then show "a \<le> (p * b) div q"
   28.15        apply (subgoal_tac "q \<noteq> 0")
   28.16 -      apply (frule div_mult_self1_is_id, force)
   28.17 +      apply (frule nonzero_mult_div_cancel_left, force)
   28.18        apply (insert q_g_2, auto)
   28.19        done
   28.20    qed
    29.1 --- a/src/HOL/Probability/SPMF.thy	Sun Oct 16 09:31:03 2016 +0200
    29.2 +++ b/src/HOL/Probability/SPMF.thy	Sun Oct 16 09:31:04 2016 +0200
    29.3 @@ -2363,7 +2363,7 @@
    29.4  apply(cases "weight_spmf p > 0")
    29.5  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)
    29.6  apply(subgoal_tac "1 = r'")
    29.7 - apply (metis (no_types) divide_1 eq_iff measure_spmf.subprob_measure_le_1 mult.commute mult_cancel_right1)
    29.8 + apply (metis (no_types) div_by_1 eq_iff measure_spmf.subprob_measure_le_1 mult.commute mult_cancel_right1)
    29.9  apply(meson eq_iff le_divide_eq_1_pos measure_spmf.subprob_measure_le_1 mult_imp_div_pos_le order.trans)
   29.10  done
   29.11  
    30.1 --- a/src/HOL/Quotient_Examples/Quotient_Rat.thy	Sun Oct 16 09:31:03 2016 +0200
    30.2 +++ b/src/HOL/Quotient_Examples/Quotient_Rat.thy	Sun Oct 16 09:31:04 2016 +0200
    30.3 @@ -258,7 +258,7 @@
    30.4      fix a b :: int
    30.5      assume "b \<noteq> 0"
    30.6      then have "a * b \<le> (a div b + 1) * b * b"
    30.7 -      by (metis mult.commute div_mult_self1_is_id less_int_def linorder_le_cases zdiv_mono1 zdiv_mono1_neg zle_add1_eq_le)
    30.8 +      by (metis mult.commute nonzero_mult_div_cancel_left less_int_def linorder_le_cases zdiv_mono1 zdiv_mono1_neg zle_add1_eq_le)
    30.9      then show "\<exists>z::int. a * b \<le> z * b * b" by auto
   30.10    qed
   30.11  qed
    31.1 --- a/src/HOL/Rat.thy	Sun Oct 16 09:31:03 2016 +0200
    31.2 +++ b/src/HOL/Rat.thy	Sun Oct 16 09:31:04 2016 +0200
    31.3 @@ -295,10 +295,10 @@
    31.4          (q * gcd r s) * (sgn (q * s) * r * gcd p q)"
    31.5        by simp
    31.6      with assms show ?thesis
    31.7 -      by (auto simp add: ac_simps sgn_times sgn_0_0)
    31.8 +      by (auto simp add: ac_simps sgn_mult sgn_0_0)
    31.9    qed
   31.10    from assms show ?thesis
   31.11 -    by (auto simp: normalize_def Let_def dvd_div_div_eq_mult mult.commute sgn_times
   31.12 +    by (auto simp: normalize_def Let_def dvd_div_div_eq_mult mult.commute sgn_mult
   31.13          split: if_splits intro: *)
   31.14  qed
   31.15  
   31.16 @@ -651,7 +651,7 @@
   31.17        @{thm True_implies_equals},
   31.18        @{thm distrib_left [where a = "numeral v" for v]},
   31.19        @{thm distrib_left [where a = "- numeral v" for v]},
   31.20 -      @{thm divide_1}, @{thm divide_zero_left},
   31.21 +      @{thm div_by_1}, @{thm div_0},
   31.22        @{thm times_divide_eq_right}, @{thm times_divide_eq_left},
   31.23        @{thm minus_divide_left} RS sym, @{thm minus_divide_right} RS sym,
   31.24        @{thm add_divide_distrib}, @{thm diff_divide_distrib},
    32.1 --- a/src/HOL/Real_Vector_Spaces.thy	Sun Oct 16 09:31:03 2016 +0200
    32.2 +++ b/src/HOL/Real_Vector_Spaces.thy	Sun Oct 16 09:31:04 2016 +0200
    32.3 @@ -1325,6 +1325,8 @@
    32.4    for x y :: "'a::real_normed_div_algebra"
    32.5    by (simp add: sgn_div_norm norm_mult mult.commute)
    32.6  
    32.7 +hide_fact (open) sgn_mult
    32.8 +
    32.9  lemma real_sgn_eq: "sgn x = x / \<bar>x\<bar>"
   32.10    for x :: real
   32.11    by (simp add: sgn_div_norm divide_inverse)
    33.1 --- a/src/HOL/Rings.thy	Sun Oct 16 09:31:03 2016 +0200
    33.2 +++ b/src/HOL/Rings.thy	Sun Oct 16 09:31:04 2016 +0200
    33.3 @@ -574,12 +574,12 @@
    33.4  text \<open>Algebraic classes with division\<close>
    33.5    
    33.6  class semidom_divide = semidom + divide +
    33.7 -  assumes nonzero_mult_divide_cancel_right [simp]: "b \<noteq> 0 \<Longrightarrow> (a * b) div b = a"
    33.8 -  assumes divide_zero [simp]: "a div 0 = 0"
    33.9 +  assumes nonzero_mult_div_cancel_right [simp]: "b \<noteq> 0 \<Longrightarrow> (a * b) div b = a"
   33.10 +  assumes div_by_0 [simp]: "a div 0 = 0"
   33.11  begin
   33.12  
   33.13 -lemma nonzero_mult_divide_cancel_left [simp]: "a \<noteq> 0 \<Longrightarrow> (a * b) div a = b"
   33.14 -  using nonzero_mult_divide_cancel_right [of a b] by (simp add: ac_simps)
   33.15 +lemma nonzero_mult_div_cancel_left [simp]: "a \<noteq> 0 \<Longrightarrow> (a * b) div a = b"
   33.16 +  using nonzero_mult_div_cancel_right [of a b] by (simp add: ac_simps)
   33.17  
   33.18  subclass semiring_no_zero_divisors_cancel
   33.19  proof
   33.20 @@ -603,21 +603,21 @@
   33.21  qed
   33.22  
   33.23  lemma div_self [simp]: "a \<noteq> 0 \<Longrightarrow> a div a = 1"
   33.24 -  using nonzero_mult_divide_cancel_left [of a 1] by simp
   33.25 +  using nonzero_mult_div_cancel_left [of a 1] by simp
   33.26  
   33.27 -lemma divide_zero_left [simp]: "0 div a = 0"
   33.28 +lemma div_0 [simp]: "0 div a = 0"
   33.29  proof (cases "a = 0")
   33.30    case True
   33.31    then show ?thesis by simp
   33.32  next
   33.33    case False
   33.34    then have "a * 0 div a = 0"
   33.35 -    by (rule nonzero_mult_divide_cancel_left)
   33.36 +    by (rule nonzero_mult_div_cancel_left)
   33.37    then show ?thesis by simp
   33.38  qed
   33.39  
   33.40 -lemma divide_1 [simp]: "a div 1 = a"
   33.41 -  using nonzero_mult_divide_cancel_left [of 1 a] by simp
   33.42 +lemma div_by_1 [simp]: "a div 1 = a"
   33.43 +  using nonzero_mult_div_cancel_left [of 1 a] by simp
   33.44  
   33.45  end
   33.46  
   33.47 @@ -952,7 +952,7 @@
   33.48    unit_mult_left_cancel unit_mult_right_cancel unit_div_cancel
   33.49    unit_eq_div1 unit_eq_div2
   33.50  
   33.51 -lemma is_unit_divide_mult_cancel_left:
   33.52 +lemma is_unit_div_mult_cancel_left:
   33.53    assumes "a \<noteq> 0" and "is_unit b"
   33.54    shows "a div (a * b) = 1 div b"
   33.55  proof -
   33.56 @@ -961,10 +961,10 @@
   33.57    with assms show ?thesis by simp
   33.58  qed
   33.59  
   33.60 -lemma is_unit_divide_mult_cancel_right:
   33.61 +lemma is_unit_div_mult_cancel_right:
   33.62    assumes "a \<noteq> 0" and "is_unit b"
   33.63    shows "a div (b * a) = 1 div b"
   33.64 -  using assms is_unit_divide_mult_cancel_left [of a b] by (simp add: ac_simps)
   33.65 +  using assms is_unit_div_mult_cancel_left [of a b] by (simp add: ac_simps)
   33.66  
   33.67  end
   33.68  
   33.69 @@ -1058,7 +1058,7 @@
   33.70  next
   33.71    case False
   33.72    then have "normalize a \<noteq> 0" by simp
   33.73 -  with nonzero_mult_divide_cancel_right
   33.74 +  with nonzero_mult_div_cancel_right
   33.75    have "unit_factor a * normalize a div normalize a = unit_factor a" by blast
   33.76    then show ?thesis by simp
   33.77  qed
   33.78 @@ -1070,7 +1070,7 @@
   33.79  next
   33.80    case False
   33.81    then have "unit_factor a \<noteq> 0" by simp
   33.82 -  with nonzero_mult_divide_cancel_left
   33.83 +  with nonzero_mult_div_cancel_left
   33.84    have "unit_factor a * normalize a div unit_factor a = normalize a"
   33.85      by blast
   33.86    then show ?thesis by simp
   33.87 @@ -1085,7 +1085,7 @@
   33.88    have "normalize a div a = normalize a div (unit_factor a * normalize a)"
   33.89      by simp
   33.90    also have "\<dots> = 1 div unit_factor a"
   33.91 -    using False by (subst is_unit_divide_mult_cancel_right) simp_all
   33.92 +    using False by (subst is_unit_div_mult_cancel_right) simp_all
   33.93    finally show ?thesis .
   33.94  qed
   33.95  
   33.96 @@ -1906,7 +1906,7 @@
   33.97  lemma sgn_neg [simp]: "a < 0 \<Longrightarrow> sgn a = - 1"
   33.98    by (simp only: sgn_1_neg)
   33.99  
  33.100 -lemma sgn_times: "sgn (a * b) = sgn a * sgn b"
  33.101 +lemma sgn_mult: "sgn (a * b) = sgn a * sgn b"
  33.102    by (auto simp add: sgn_if zero_less_mult_iff)
  33.103  
  33.104  lemma abs_sgn: "\<bar>k\<bar> = k * sgn k"
    34.1 --- a/src/HOL/Tools/numeral_simprocs.ML	Sun Oct 16 09:31:03 2016 +0200
    34.2 +++ b/src/HOL/Tools/numeral_simprocs.ML	Sun Oct 16 09:31:04 2016 +0200
    34.3 @@ -173,7 +173,7 @@
    34.4  
    34.5  (*Simplify 0+n, n+0, Numeral1*n, n*Numeral1, 1*x, x*1, x/1 *)
    34.6  val add_0s =  @{thms add_0_left add_0_right};
    34.7 -val mult_1s = @{thms mult_1s divide_numeral_1 mult_1_left mult_1_right mult_minus1 mult_minus1_right divide_1};
    34.8 +val mult_1s = @{thms mult_1s divide_numeral_1 mult_1_left mult_1_right mult_minus1 mult_minus1_right div_by_1};
    34.9  
   34.10  (* For post-simplification of the rhs of simproc-generated rules *)
   34.11  val post_simps =
   34.12 @@ -184,7 +184,7 @@
   34.13       @{thm mult_minus1}, @{thm mult_minus1_right}]
   34.14  
   34.15  val field_post_simps =
   34.16 -    post_simps @ [@{thm divide_zero_left}, @{thm divide_1}]
   34.17 +    post_simps @ [@{thm div_0}, @{thm div_by_1}]
   34.18  
   34.19  (*Simplify inverse Numeral1*)
   34.20  val inverse_1s = [@{thm inverse_numeral_1}];
   34.21 @@ -712,7 +712,7 @@
   34.22  val ths =
   34.23   [@{thm "mult_numeral_1"}, @{thm "mult_numeral_1_right"},
   34.24    @{thm "divide_numeral_1"},
   34.25 -  @{thm "divide_zero"}, @{thm divide_zero_left},
   34.26 +  @{thm "div_by_0"}, @{thm div_0},
   34.27    @{thm "divide_divide_eq_left"},
   34.28    @{thm "times_divide_eq_left"}, @{thm "times_divide_eq_right"},
   34.29    @{thm "times_divide_times_eq"},
    35.1 --- a/src/HOL/ex/Simproc_Tests.thy	Sun Oct 16 09:31:03 2016 +0200
    35.2 +++ b/src/HOL/ex/Simproc_Tests.thy	Sun Oct 16 09:31:04 2016 +0200
    35.3 @@ -361,7 +361,7 @@
    35.4      have "(k) / (k*y) = uu"
    35.5        by (tactic \<open>test @{context} [@{simproc divide_cancel_factor}]\<close>) fact
    35.6    next
    35.7 -    assume "(if b = 0 then 0 else a * c / 1) = uu"
    35.8 +    assume "(if b = 0 then 0 else a * c) = uu"
    35.9      have "(a*(b*c)) / b = uu"
   35.10        by (tactic \<open>test @{context} [@{simproc divide_cancel_factor}]\<close>) fact
   35.11    next