# HG changeset patch
# User haftmann
# Date 1424343216 -3600
# Node ID ebd8ecacfba66c9174170058838a4dd8c7f874b8
# Parent  aa2deef7cf47a762a8764a0c47a11629f06aa91b
establish unique preferred fact names

diff -r aa2deef7cf47 -r ebd8ecacfba6 NEWS
--- a/NEWS	Wed Feb 18 22:46:48 2015 +0100
+++ b/NEWS	Thu Feb 19 11:53:36 2015 +0100
@@ -68,6 +68,14 @@
 
 *** HOL ***
 
+* Qualified some duplicated fact names required for boostrapping
+the type class hierarchy:
+  ab_add_uminus_conv_diff ~> diff_conv_add_uminus
+  field_inverse_zero ~> inverse_zero
+  field_divide_inverse ~> divide_inverse
+  field_inverse ~> left_inverse
+Minor INCOMPATIBILITY.
+
 * Eliminated fact duplicates:
   mult_less_imp_less_right ~> mult_right_less_imp_less
   mult_less_imp_less_left ~> mult_left_less_imp_less
diff -r aa2deef7cf47 -r ebd8ecacfba6 src/HOL/Fields.thy
--- a/src/HOL/Fields.thy	Wed Feb 18 22:46:48 2015 +0100
+++ b/src/HOL/Fields.thy	Thu Feb 19 11:53:36 2015 +0100
@@ -1204,7 +1204,9 @@
 
 end
 
+hide_fact (open) field_inverse field_divide_inverse field_inverse_zero
+
 code_identifier
   code_module Fields \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
-
+ 
 end
diff -r aa2deef7cf47 -r ebd8ecacfba6 src/HOL/Groups.thy
--- a/src/HOL/Groups.thy	Wed Feb 18 22:46:48 2015 +0100
+++ b/src/HOL/Groups.thy	Thu Feb 19 11:53:36 2015 +0100
@@ -518,11 +518,11 @@
 
 class ab_group_add = minus + uminus + comm_monoid_add +
   assumes ab_left_minus: "- a + a = 0"
-  assumes ab_add_uminus_conv_diff: "a - b = a + (- b)"
+  assumes ab_diff_conv_add_uminus: "a - b = a + (- b)"
 begin
 
 subclass group_add
-  proof qed (simp_all add: ab_left_minus ab_add_uminus_conv_diff)
+  proof qed (simp_all add: ab_left_minus ab_diff_conv_add_uminus)
 
 subclass cancel_comm_monoid_add
 proof
@@ -1375,6 +1375,7 @@
 
 end
 
+hide_fact (open) ab_diff_conv_add_uminus add_imp_eq
 
 subsection {* Tools setup *}
 
diff -r aa2deef7cf47 -r ebd8ecacfba6 src/HOL/Library/Convex.thy
--- a/src/HOL/Library/Convex.thy	Wed Feb 18 22:46:48 2015 +0100
+++ b/src/HOL/Library/Convex.thy	Thu Feb 19 11:53:36 2015 +0100
@@ -329,7 +329,7 @@
   have "u * f x + v * f y \<le> u * max (f x) (f y) + v * max (f x) (f y)"
     using assms(4,5) by (auto simp add: mult_left_mono add_mono)
   also have "\<dots> = max (f x) (f y)"
-    using assms(6) unfolding distrib[symmetric] by auto
+    using assms(6) by (simp add: distrib_right [symmetric]) 
   finally show ?thesis
     using assms unfolding convex_on_def by fastforce
 qed
diff -r aa2deef7cf47 -r ebd8ecacfba6 src/HOL/Library/Fundamental_Theorem_Algebra.thy
--- a/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Wed Feb 18 22:46:48 2015 +0100
+++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Thu Feb 19 11:53:36 2015 +0100
@@ -810,7 +810,7 @@
       from t inv0 have "t * (cmod w ^ (k + 1) * m) < 1"
         by (simp add: field_simps)
       with zero_less_power[OF t(1), of k] have th30: "t^k * (t* (cmod w ^ (k + 1) * m)) < t^k * 1"
-        by (metis comm_mult_strict_left_mono)
+        by simp
       have "cmod (?w^k * ?w * poly s ?w) = t^k * (t* (cmod w ^ (k + 1) * cmod (poly s ?w)))"
         using w0 t(1)
         by (simp add: algebra_simps power_mult_distrib norm_power norm_mult)
diff -r aa2deef7cf47 -r ebd8ecacfba6 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Wed Feb 18 22:46:48 2015 +0100
+++ b/src/HOL/Library/Multiset.thy	Thu Feb 19 11:53:36 2015 +0100
@@ -1963,7 +1963,7 @@
   by (fact add_left_cancel)
 
 lemma multi_union_self_other_eq: "(A::'a multiset) + X = A + Y \<Longrightarrow> X = Y"
-  by (fact add_imp_eq)
+  by (fact add_left_imp_eq)
 
 lemma mset_less_trans: "(M::'a multiset) < K \<Longrightarrow> K < N \<Longrightarrow> M < N"
   by (fact order_less_trans)
diff -r aa2deef7cf47 -r ebd8ecacfba6 src/HOL/Library/Polynomial.thy
--- a/src/HOL/Library/Polynomial.thy	Wed Feb 18 22:46:48 2015 +0100
+++ b/src/HOL/Library/Polynomial.thy	Thu Feb 19 11:53:36 2015 +0100
@@ -710,7 +710,7 @@
 lemma [code]:
   fixes p q :: "'a::ab_group_add poly"
   shows "p - q = p + - q"
-  by (fact ab_add_uminus_conv_diff)
+  by (fact diff_conv_add_uminus)
 
 lemma poly_add [simp]: "poly (p + q) x = poly p x + poly q x"
   apply (induct p arbitrary: q, simp)
@@ -1518,7 +1518,7 @@
   assumes "pdivmod_rel x' y q' r'"
   shows "pdivmod_rel (x + x') y (q + q') (r + r')"
   using assms unfolding pdivmod_rel_def
-  by (auto simp add: distrib degree_add_less)
+  by (auto simp add: algebra_simps degree_add_less)
 
 lemma poly_div_add_left:
   fixes x y z :: "'a::field poly"
diff -r aa2deef7cf47 -r ebd8ecacfba6 src/HOL/Metis_Examples/Big_O.thy
--- a/src/HOL/Metis_Examples/Big_O.thy	Wed Feb 18 22:46:48 2015 +0100
+++ b/src/HOL/Metis_Examples/Big_O.thy	Thu Feb 19 11:53:36 2015 +0100
@@ -457,9 +457,9 @@
   hence F4: "\<exists>(u\<Colon>'a) SKF\<^sub>7\<Colon>'a \<Rightarrow> 'b. \<bar>g (SKF\<^sub>7 (\<bar>inverse c\<bar> * u))\<bar> \<le> u * \<bar>f (SKF\<^sub>7 (\<bar>inverse c\<bar> * u))\<bar> \<and> (0\<Colon>'a) \<le> \<bar>inverse c\<bar>"
     using F3 by metis
   hence "\<exists>(v\<Colon>'a) (u\<Colon>'a) SKF\<^sub>7\<Colon>'a \<Rightarrow> 'b. \<bar>inverse c\<bar> * \<bar>g (SKF\<^sub>7 (u * v))\<bar> \<le> u * (v * \<bar>f (SKF\<^sub>7 (u * v))\<bar>)"
-    by (metis comm_mult_left_mono)
+    by (metis mult_left_mono)
   thus "\<exists>ca\<Colon>'a. \<forall>x\<Colon>'b. \<bar>inverse c\<bar> * \<bar>g x\<bar> \<le> ca * \<bar>f x\<bar>"
-    using A2 F4 by (metis mult.assoc comm_mult_left_mono)
+    using A2 F4 by (metis mult.assoc mult_left_mono)
 qed
 
 lemma bigo_const_mult6 [intro]: "(\<lambda>x. c) *o O(f) <= O(f)"
diff -r aa2deef7cf47 -r ebd8ecacfba6 src/HOL/Multivariate_Analysis/Linear_Algebra.thy
--- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Wed Feb 18 22:46:48 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Thu Feb 19 11:53:36 2015 +0100
@@ -340,7 +340,7 @@
   by (drule bilinear_rmul [of _ _ "- 1"]) simp
 
 lemma (in ab_group_add) eq_add_iff: "x = x + y \<longleftrightarrow> y = 0"
-  using add_imp_eq[of x y 0] by auto
+  using add_left_imp_eq[of x y 0] by auto
 
 lemma bilinear_lzero:
   assumes "bilinear h"
diff -r aa2deef7cf47 -r ebd8ecacfba6 src/HOL/Multivariate_Analysis/Path_Connected.thy
--- a/src/HOL/Multivariate_Analysis/Path_Connected.thy	Wed Feb 18 22:46:48 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Path_Connected.thy	Thu Feb 19 11:53:36 2015 +0100
@@ -976,8 +976,7 @@
     apply (auto split: split_if_asm)
     done
   have "continuous_on (UNIV - {0}) (\<lambda>x::'a. 1 / norm x)"
-    unfolding field_divide_inverse
-    by (simp add: continuous_intros)
+    by (auto intro!: continuous_intros)
   then show ?thesis
     unfolding * **
     using path_connected_punctured_universe[OF assms]
diff -r aa2deef7cf47 -r ebd8ecacfba6 src/HOL/NSA/StarDef.thy
--- a/src/HOL/NSA/StarDef.thy	Wed Feb 18 22:46:48 2015 +0100
+++ b/src/HOL/NSA/StarDef.thy	Thu Feb 19 11:53:36 2015 +0100
@@ -795,7 +795,7 @@
 done
 
 instance star :: (cancel_ab_semigroup_add) cancel_ab_semigroup_add
-by (intro_classes, transfer, rule add_imp_eq)
+by (intro_classes, transfer, rule add_left_imp_eq)
 
 instance star :: (cancel_comm_monoid_add) cancel_comm_monoid_add ..
 
diff -r aa2deef7cf47 -r ebd8ecacfba6 src/HOL/Number_Theory/Binomial.thy
--- a/src/HOL/Number_Theory/Binomial.thy	Wed Feb 18 22:46:48 2015 +0100
+++ b/src/HOL/Number_Theory/Binomial.thy	Thu Feb 19 11:53:36 2015 +0100
@@ -161,7 +161,7 @@
     using Suc.hyps by simp
   also have "\<dots> = a*(\<Sum>k=0..n. of_nat (n choose k) * a^k * b^(n-k)) +
                    b*(\<Sum>k=0..n. of_nat (n choose k) * a^k * b^(n-k))"
-    by (rule distrib)
+    by (rule distrib_right)
   also have "\<dots> = (\<Sum>k=0..n. of_nat (n choose k) * a^(k+1) * b^(n-k)) +
                   (\<Sum>k=0..n. of_nat (n choose k) * a^k * b^(n-k+1))"
     by (auto simp add: setsum_right_distrib ac_simps)
diff -r aa2deef7cf47 -r ebd8ecacfba6 src/HOL/Probability/Probability_Mass_Function.thy
--- a/src/HOL/Probability/Probability_Mass_Function.thy	Wed Feb 18 22:46:48 2015 +0100
+++ b/src/HOL/Probability/Probability_Mass_Function.thy	Thu Feb 19 11:53:36 2015 +0100
@@ -582,14 +582,14 @@
   (* Proof by Manuel Eberl *)
 
   have summable: "summable (\<lambda>x::nat. rate ^ x / fact x)" using summable_exp
-    by (simp add: field_simps field_divide_inverse[symmetric])
+    by (simp add: field_simps divide_inverse [symmetric])
   have "(\<integral>\<^sup>+(x::nat). rate ^ x / fact x * exp (-rate) \<partial>count_space UNIV) =
           exp (-rate) * (\<integral>\<^sup>+(x::nat). rate ^ x / fact x \<partial>count_space UNIV)"
     by (simp add: field_simps nn_integral_cmult[symmetric])
   also from rate_pos have "(\<integral>\<^sup>+(x::nat). rate ^ x / fact x \<partial>count_space UNIV) = (\<Sum>x. rate ^ x / fact x)"
     by (simp_all add: nn_integral_count_space_nat suminf_ereal summable suminf_ereal_finite)
   also have "... = exp rate" unfolding exp_def
-    by (simp add: field_simps field_divide_inverse[symmetric] transfer_int_nat_factorial)
+    by (simp add: field_simps divide_inverse [symmetric] transfer_int_nat_factorial)
   also have "ereal (exp (-rate)) * ereal (exp rate) = 1"
     by (simp add: mult_exp_exp)
   finally show "(\<integral>\<^sup>+ x. ereal (rate ^ x / real (fact x) * exp (- rate)) \<partial>count_space UNIV) = 1" .
diff -r aa2deef7cf47 -r ebd8ecacfba6 src/HOL/Quotient_Examples/Quotient_Rat.thy
--- a/src/HOL/Quotient_Examples/Quotient_Rat.thy	Wed Feb 18 22:46:48 2015 +0100
+++ b/src/HOL/Quotient_Examples/Quotient_Rat.thy	Thu Feb 19 11:53:36 2015 +0100
@@ -239,7 +239,7 @@
       by (metis linorder_neqE_linordered_idom mult_eq_0_iff not_square_less_zero)
       assume "a * b * d * d \<le> b * b * c * d"
       then show "a * b * d * d * e * e * e * e \<le> b * b * c * d * e * e * e * e"
-        using e2 by (metis comm_mult_left_mono mult.commute linorder_le_cases
+        using e2 by (metis mult_left_mono mult.commute linorder_le_cases
           mult_left_mono_neg)
     qed
   show "q < r ==> 0 < s ==> s * q < s * r" unfolding less_rat_def
@@ -249,7 +249,7 @@
     have "a * b * d * d * (e * f) \<le> b * b * c * d * (e * f)" using a
       by (simp add: mult_right_mono)
     then show "a * b * d * d * e * f * f * f \<le> b * b * c * d * e * f * f * f"
-      by (simp add: mult.assoc[symmetric]) (metis a(3) comm_mult_left_mono
+      by (simp add: mult.assoc[symmetric]) (metis a(3) mult_left_mono
         mult.commute mult_left_mono_neg zero_le_mult_iff)
   qed
   show "\<exists>z. r \<le> of_int z"
diff -r aa2deef7cf47 -r ebd8ecacfba6 src/HOL/Rings.thy
--- a/src/HOL/Rings.thy	Wed Feb 18 22:46:48 2015 +0100
+++ b/src/HOL/Rings.thy	Thu Feb 19 11:53:36 2015 +0100
@@ -1259,6 +1259,8 @@
 
 end
 
+hide_fact (open) comm_mult_left_mono comm_mult_strict_left_mono distrib
+
 code_identifier
   code_module Rings \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
 
diff -r aa2deef7cf47 -r ebd8ecacfba6 src/HOL/Semiring_Normalization.thy
--- a/src/HOL/Semiring_Normalization.thy	Wed Feb 18 22:46:48 2015 +0100
+++ b/src/HOL/Semiring_Normalization.thy	Thu Feb 19 11:53:36 2015 +0100
@@ -24,13 +24,13 @@
   assume nz: "r\<noteq> 0" and cnd: "a = b \<and> c\<noteq>d"
     and eq: "a + (r * c) = b + (r * d)"
   have "(0 * d) + (r * c) = (0 * c) + (r * d)"
-    using add_imp_eq eq mult_zero_left by (simp add: cnd)
+    using add_left_imp_eq eq mult_zero_left by (simp add: cnd)
   then show False using crossproduct_eq [of 0 d] nz cnd by simp
 qed
 
 lemma add_0_iff:
   "b = b + a \<longleftrightarrow> a = 0"
-  using add_imp_eq [of b a 0] by auto
+  using add_left_imp_eq [of b a 0] by auto
 
 end
 
diff -r aa2deef7cf47 -r ebd8ecacfba6 src/HOL/Tools/numeral_simprocs.ML
--- a/src/HOL/Tools/numeral_simprocs.ML	Wed Feb 18 22:46:48 2015 +0100
+++ b/src/HOL/Tools/numeral_simprocs.ML	Thu Feb 19 11:53:36 2015 +0100
@@ -718,9 +718,9 @@
            @{thm "divide_divide_eq_right"},
            @{thm diff_conv_add_uminus}, @{thm "minus_divide_left"},
            @{thm "add_divide_distrib"} RS sym,
-           @{thm field_divide_inverse} RS sym, @{thm inverse_divide}, 
+           @{thm Fields.field_divide_inverse} RS sym, @{thm inverse_divide}, 
            Conv.fconv_rule (Conv.arg_conv (Conv.arg1_conv (Conv.rewr_conv (mk_meta_eq @{thm mult.commute}))))   
-           (@{thm field_divide_inverse} RS sym)]
+           (@{thm Fields.field_divide_inverse} RS sym)]
 
 val field_comp_ss =
   simpset_of