establish unique preferred fact names
authorhaftmann
Thu Feb 19 11:53:36 2015 +0100 (2015-02-19)
changeset 59557ebd8ecacfba6
parent 59556 aa2deef7cf47
child 59558 5d9f0ace9af0
establish unique preferred fact names
NEWS
src/HOL/Fields.thy
src/HOL/Groups.thy
src/HOL/Library/Convex.thy
src/HOL/Library/Fundamental_Theorem_Algebra.thy
src/HOL/Library/Multiset.thy
src/HOL/Library/Polynomial.thy
src/HOL/Metis_Examples/Big_O.thy
src/HOL/Multivariate_Analysis/Linear_Algebra.thy
src/HOL/Multivariate_Analysis/Path_Connected.thy
src/HOL/NSA/StarDef.thy
src/HOL/Number_Theory/Binomial.thy
src/HOL/Probability/Probability_Mass_Function.thy
src/HOL/Quotient_Examples/Quotient_Rat.thy
src/HOL/Rings.thy
src/HOL/Semiring_Normalization.thy
src/HOL/Tools/numeral_simprocs.ML
     1.1 --- a/NEWS	Wed Feb 18 22:46:48 2015 +0100
     1.2 +++ b/NEWS	Thu Feb 19 11:53:36 2015 +0100
     1.3 @@ -68,6 +68,14 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* Qualified some duplicated fact names required for boostrapping
     1.8 +the type class hierarchy:
     1.9 +  ab_add_uminus_conv_diff ~> diff_conv_add_uminus
    1.10 +  field_inverse_zero ~> inverse_zero
    1.11 +  field_divide_inverse ~> divide_inverse
    1.12 +  field_inverse ~> left_inverse
    1.13 +Minor INCOMPATIBILITY.
    1.14 +
    1.15  * Eliminated fact duplicates:
    1.16    mult_less_imp_less_right ~> mult_right_less_imp_less
    1.17    mult_less_imp_less_left ~> mult_left_less_imp_less
     2.1 --- a/src/HOL/Fields.thy	Wed Feb 18 22:46:48 2015 +0100
     2.2 +++ b/src/HOL/Fields.thy	Thu Feb 19 11:53:36 2015 +0100
     2.3 @@ -1204,7 +1204,9 @@
     2.4  
     2.5  end
     2.6  
     2.7 +hide_fact (open) field_inverse field_divide_inverse field_inverse_zero
     2.8 +
     2.9  code_identifier
    2.10    code_module Fields \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
    2.11 -
    2.12 + 
    2.13  end
     3.1 --- a/src/HOL/Groups.thy	Wed Feb 18 22:46:48 2015 +0100
     3.2 +++ b/src/HOL/Groups.thy	Thu Feb 19 11:53:36 2015 +0100
     3.3 @@ -518,11 +518,11 @@
     3.4  
     3.5  class ab_group_add = minus + uminus + comm_monoid_add +
     3.6    assumes ab_left_minus: "- a + a = 0"
     3.7 -  assumes ab_add_uminus_conv_diff: "a - b = a + (- b)"
     3.8 +  assumes ab_diff_conv_add_uminus: "a - b = a + (- b)"
     3.9  begin
    3.10  
    3.11  subclass group_add
    3.12 -  proof qed (simp_all add: ab_left_minus ab_add_uminus_conv_diff)
    3.13 +  proof qed (simp_all add: ab_left_minus ab_diff_conv_add_uminus)
    3.14  
    3.15  subclass cancel_comm_monoid_add
    3.16  proof
    3.17 @@ -1375,6 +1375,7 @@
    3.18  
    3.19  end
    3.20  
    3.21 +hide_fact (open) ab_diff_conv_add_uminus add_imp_eq
    3.22  
    3.23  subsection {* Tools setup *}
    3.24  
     4.1 --- a/src/HOL/Library/Convex.thy	Wed Feb 18 22:46:48 2015 +0100
     4.2 +++ b/src/HOL/Library/Convex.thy	Thu Feb 19 11:53:36 2015 +0100
     4.3 @@ -329,7 +329,7 @@
     4.4    have "u * f x + v * f y \<le> u * max (f x) (f y) + v * max (f x) (f y)"
     4.5      using assms(4,5) by (auto simp add: mult_left_mono add_mono)
     4.6    also have "\<dots> = max (f x) (f y)"
     4.7 -    using assms(6) unfolding distrib[symmetric] by auto
     4.8 +    using assms(6) by (simp add: distrib_right [symmetric]) 
     4.9    finally show ?thesis
    4.10      using assms unfolding convex_on_def by fastforce
    4.11  qed
     5.1 --- a/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Wed Feb 18 22:46:48 2015 +0100
     5.2 +++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Thu Feb 19 11:53:36 2015 +0100
     5.3 @@ -810,7 +810,7 @@
     5.4        from t inv0 have "t * (cmod w ^ (k + 1) * m) < 1"
     5.5          by (simp add: field_simps)
     5.6        with zero_less_power[OF t(1), of k] have th30: "t^k * (t* (cmod w ^ (k + 1) * m)) < t^k * 1"
     5.7 -        by (metis comm_mult_strict_left_mono)
     5.8 +        by simp
     5.9        have "cmod (?w^k * ?w * poly s ?w) = t^k * (t* (cmod w ^ (k + 1) * cmod (poly s ?w)))"
    5.10          using w0 t(1)
    5.11          by (simp add: algebra_simps power_mult_distrib norm_power norm_mult)
     6.1 --- a/src/HOL/Library/Multiset.thy	Wed Feb 18 22:46:48 2015 +0100
     6.2 +++ b/src/HOL/Library/Multiset.thy	Thu Feb 19 11:53:36 2015 +0100
     6.3 @@ -1963,7 +1963,7 @@
     6.4    by (fact add_left_cancel)
     6.5  
     6.6  lemma multi_union_self_other_eq: "(A::'a multiset) + X = A + Y \<Longrightarrow> X = Y"
     6.7 -  by (fact add_imp_eq)
     6.8 +  by (fact add_left_imp_eq)
     6.9  
    6.10  lemma mset_less_trans: "(M::'a multiset) < K \<Longrightarrow> K < N \<Longrightarrow> M < N"
    6.11    by (fact order_less_trans)
     7.1 --- a/src/HOL/Library/Polynomial.thy	Wed Feb 18 22:46:48 2015 +0100
     7.2 +++ b/src/HOL/Library/Polynomial.thy	Thu Feb 19 11:53:36 2015 +0100
     7.3 @@ -710,7 +710,7 @@
     7.4  lemma [code]:
     7.5    fixes p q :: "'a::ab_group_add poly"
     7.6    shows "p - q = p + - q"
     7.7 -  by (fact ab_add_uminus_conv_diff)
     7.8 +  by (fact diff_conv_add_uminus)
     7.9  
    7.10  lemma poly_add [simp]: "poly (p + q) x = poly p x + poly q x"
    7.11    apply (induct p arbitrary: q, simp)
    7.12 @@ -1518,7 +1518,7 @@
    7.13    assumes "pdivmod_rel x' y q' r'"
    7.14    shows "pdivmod_rel (x + x') y (q + q') (r + r')"
    7.15    using assms unfolding pdivmod_rel_def
    7.16 -  by (auto simp add: distrib degree_add_less)
    7.17 +  by (auto simp add: algebra_simps degree_add_less)
    7.18  
    7.19  lemma poly_div_add_left:
    7.20    fixes x y z :: "'a::field poly"
     8.1 --- a/src/HOL/Metis_Examples/Big_O.thy	Wed Feb 18 22:46:48 2015 +0100
     8.2 +++ b/src/HOL/Metis_Examples/Big_O.thy	Thu Feb 19 11:53:36 2015 +0100
     8.3 @@ -457,9 +457,9 @@
     8.4    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>"
     8.5      using F3 by metis
     8.6    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>)"
     8.7 -    by (metis comm_mult_left_mono)
     8.8 +    by (metis mult_left_mono)
     8.9    thus "\<exists>ca\<Colon>'a. \<forall>x\<Colon>'b. \<bar>inverse c\<bar> * \<bar>g x\<bar> \<le> ca * \<bar>f x\<bar>"
    8.10 -    using A2 F4 by (metis mult.assoc comm_mult_left_mono)
    8.11 +    using A2 F4 by (metis mult.assoc mult_left_mono)
    8.12  qed
    8.13  
    8.14  lemma bigo_const_mult6 [intro]: "(\<lambda>x. c) *o O(f) <= O(f)"
     9.1 --- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Wed Feb 18 22:46:48 2015 +0100
     9.2 +++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Thu Feb 19 11:53:36 2015 +0100
     9.3 @@ -340,7 +340,7 @@
     9.4    by (drule bilinear_rmul [of _ _ "- 1"]) simp
     9.5  
     9.6  lemma (in ab_group_add) eq_add_iff: "x = x + y \<longleftrightarrow> y = 0"
     9.7 -  using add_imp_eq[of x y 0] by auto
     9.8 +  using add_left_imp_eq[of x y 0] by auto
     9.9  
    9.10  lemma bilinear_lzero:
    9.11    assumes "bilinear h"
    10.1 --- a/src/HOL/Multivariate_Analysis/Path_Connected.thy	Wed Feb 18 22:46:48 2015 +0100
    10.2 +++ b/src/HOL/Multivariate_Analysis/Path_Connected.thy	Thu Feb 19 11:53:36 2015 +0100
    10.3 @@ -976,8 +976,7 @@
    10.4      apply (auto split: split_if_asm)
    10.5      done
    10.6    have "continuous_on (UNIV - {0}) (\<lambda>x::'a. 1 / norm x)"
    10.7 -    unfolding field_divide_inverse
    10.8 -    by (simp add: continuous_intros)
    10.9 +    by (auto intro!: continuous_intros)
   10.10    then show ?thesis
   10.11      unfolding * **
   10.12      using path_connected_punctured_universe[OF assms]
    11.1 --- a/src/HOL/NSA/StarDef.thy	Wed Feb 18 22:46:48 2015 +0100
    11.2 +++ b/src/HOL/NSA/StarDef.thy	Thu Feb 19 11:53:36 2015 +0100
    11.3 @@ -795,7 +795,7 @@
    11.4  done
    11.5  
    11.6  instance star :: (cancel_ab_semigroup_add) cancel_ab_semigroup_add
    11.7 -by (intro_classes, transfer, rule add_imp_eq)
    11.8 +by (intro_classes, transfer, rule add_left_imp_eq)
    11.9  
   11.10  instance star :: (cancel_comm_monoid_add) cancel_comm_monoid_add ..
   11.11  
    12.1 --- a/src/HOL/Number_Theory/Binomial.thy	Wed Feb 18 22:46:48 2015 +0100
    12.2 +++ b/src/HOL/Number_Theory/Binomial.thy	Thu Feb 19 11:53:36 2015 +0100
    12.3 @@ -161,7 +161,7 @@
    12.4      using Suc.hyps by simp
    12.5    also have "\<dots> = a*(\<Sum>k=0..n. of_nat (n choose k) * a^k * b^(n-k)) +
    12.6                     b*(\<Sum>k=0..n. of_nat (n choose k) * a^k * b^(n-k))"
    12.7 -    by (rule distrib)
    12.8 +    by (rule distrib_right)
    12.9    also have "\<dots> = (\<Sum>k=0..n. of_nat (n choose k) * a^(k+1) * b^(n-k)) +
   12.10                    (\<Sum>k=0..n. of_nat (n choose k) * a^k * b^(n-k+1))"
   12.11      by (auto simp add: setsum_right_distrib ac_simps)
    13.1 --- a/src/HOL/Probability/Probability_Mass_Function.thy	Wed Feb 18 22:46:48 2015 +0100
    13.2 +++ b/src/HOL/Probability/Probability_Mass_Function.thy	Thu Feb 19 11:53:36 2015 +0100
    13.3 @@ -582,14 +582,14 @@
    13.4    (* Proof by Manuel Eberl *)
    13.5  
    13.6    have summable: "summable (\<lambda>x::nat. rate ^ x / fact x)" using summable_exp
    13.7 -    by (simp add: field_simps field_divide_inverse[symmetric])
    13.8 +    by (simp add: field_simps divide_inverse [symmetric])
    13.9    have "(\<integral>\<^sup>+(x::nat). rate ^ x / fact x * exp (-rate) \<partial>count_space UNIV) =
   13.10            exp (-rate) * (\<integral>\<^sup>+(x::nat). rate ^ x / fact x \<partial>count_space UNIV)"
   13.11      by (simp add: field_simps nn_integral_cmult[symmetric])
   13.12    also from rate_pos have "(\<integral>\<^sup>+(x::nat). rate ^ x / fact x \<partial>count_space UNIV) = (\<Sum>x. rate ^ x / fact x)"
   13.13      by (simp_all add: nn_integral_count_space_nat suminf_ereal summable suminf_ereal_finite)
   13.14    also have "... = exp rate" unfolding exp_def
   13.15 -    by (simp add: field_simps field_divide_inverse[symmetric] transfer_int_nat_factorial)
   13.16 +    by (simp add: field_simps divide_inverse [symmetric] transfer_int_nat_factorial)
   13.17    also have "ereal (exp (-rate)) * ereal (exp rate) = 1"
   13.18      by (simp add: mult_exp_exp)
   13.19    finally show "(\<integral>\<^sup>+ x. ereal (rate ^ x / real (fact x) * exp (- rate)) \<partial>count_space UNIV) = 1" .
    14.1 --- a/src/HOL/Quotient_Examples/Quotient_Rat.thy	Wed Feb 18 22:46:48 2015 +0100
    14.2 +++ b/src/HOL/Quotient_Examples/Quotient_Rat.thy	Thu Feb 19 11:53:36 2015 +0100
    14.3 @@ -239,7 +239,7 @@
    14.4        by (metis linorder_neqE_linordered_idom mult_eq_0_iff not_square_less_zero)
    14.5        assume "a * b * d * d \<le> b * b * c * d"
    14.6        then show "a * b * d * d * e * e * e * e \<le> b * b * c * d * e * e * e * e"
    14.7 -        using e2 by (metis comm_mult_left_mono mult.commute linorder_le_cases
    14.8 +        using e2 by (metis mult_left_mono mult.commute linorder_le_cases
    14.9            mult_left_mono_neg)
   14.10      qed
   14.11    show "q < r ==> 0 < s ==> s * q < s * r" unfolding less_rat_def
   14.12 @@ -249,7 +249,7 @@
   14.13      have "a * b * d * d * (e * f) \<le> b * b * c * d * (e * f)" using a
   14.14        by (simp add: mult_right_mono)
   14.15      then show "a * b * d * d * e * f * f * f \<le> b * b * c * d * e * f * f * f"
   14.16 -      by (simp add: mult.assoc[symmetric]) (metis a(3) comm_mult_left_mono
   14.17 +      by (simp add: mult.assoc[symmetric]) (metis a(3) mult_left_mono
   14.18          mult.commute mult_left_mono_neg zero_le_mult_iff)
   14.19    qed
   14.20    show "\<exists>z. r \<le> of_int z"
    15.1 --- a/src/HOL/Rings.thy	Wed Feb 18 22:46:48 2015 +0100
    15.2 +++ b/src/HOL/Rings.thy	Thu Feb 19 11:53:36 2015 +0100
    15.3 @@ -1259,6 +1259,8 @@
    15.4  
    15.5  end
    15.6  
    15.7 +hide_fact (open) comm_mult_left_mono comm_mult_strict_left_mono distrib
    15.8 +
    15.9  code_identifier
   15.10    code_module Rings \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
   15.11  
    16.1 --- a/src/HOL/Semiring_Normalization.thy	Wed Feb 18 22:46:48 2015 +0100
    16.2 +++ b/src/HOL/Semiring_Normalization.thy	Thu Feb 19 11:53:36 2015 +0100
    16.3 @@ -24,13 +24,13 @@
    16.4    assume nz: "r\<noteq> 0" and cnd: "a = b \<and> c\<noteq>d"
    16.5      and eq: "a + (r * c) = b + (r * d)"
    16.6    have "(0 * d) + (r * c) = (0 * c) + (r * d)"
    16.7 -    using add_imp_eq eq mult_zero_left by (simp add: cnd)
    16.8 +    using add_left_imp_eq eq mult_zero_left by (simp add: cnd)
    16.9    then show False using crossproduct_eq [of 0 d] nz cnd by simp
   16.10  qed
   16.11  
   16.12  lemma add_0_iff:
   16.13    "b = b + a \<longleftrightarrow> a = 0"
   16.14 -  using add_imp_eq [of b a 0] by auto
   16.15 +  using add_left_imp_eq [of b a 0] by auto
   16.16  
   16.17  end
   16.18  
    17.1 --- a/src/HOL/Tools/numeral_simprocs.ML	Wed Feb 18 22:46:48 2015 +0100
    17.2 +++ b/src/HOL/Tools/numeral_simprocs.ML	Thu Feb 19 11:53:36 2015 +0100
    17.3 @@ -718,9 +718,9 @@
    17.4             @{thm "divide_divide_eq_right"},
    17.5             @{thm diff_conv_add_uminus}, @{thm "minus_divide_left"},
    17.6             @{thm "add_divide_distrib"} RS sym,
    17.7 -           @{thm field_divide_inverse} RS sym, @{thm inverse_divide}, 
    17.8 +           @{thm Fields.field_divide_inverse} RS sym, @{thm inverse_divide}, 
    17.9             Conv.fconv_rule (Conv.arg_conv (Conv.arg1_conv (Conv.rewr_conv (mk_meta_eq @{thm mult.commute}))))   
   17.10 -           (@{thm field_divide_inverse} RS sym)]
   17.11 +           (@{thm Fields.field_divide_inverse} RS sym)]
   17.12  
   17.13  val field_comp_ss =
   17.14    simpset_of