--- 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
--- 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
--- 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 *}
--- 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
--- 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)
--- 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)
--- 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"
--- 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)"
--- 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"
--- 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]
--- 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 ..
--- 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)
--- 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" .
--- 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"
--- 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
--- 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
--- 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