--- a/NEWS Sun Oct 08 22:28:20 2017 +0200
+++ b/NEWS Sun Oct 08 22:28:20 2017 +0200
@@ -47,6 +47,10 @@
* Fact mod_mult_self4 (on nat) renamed to mod_mult_self3', to avoid clash
with fact mod_mult_self4 (on more generic semirings). INCOMPATIBILITY.
+* Facts sum.commute(_restrict) and prod.commute(_restrict) renamed to
+sum.swap(_restrict) and prod.swap(_restrict), to avoid name clashes
+on interpretation of abstract locales. INCOMPATIBILITY.
+
* Predicate pairwise_coprime abolished, use "pairwise coprime" instead.
INCOMPATIBILITY.
--- a/src/HOL/Analysis/Bochner_Integration.thy Sun Oct 08 22:28:20 2017 +0200
+++ b/src/HOL/Analysis/Bochner_Integration.thy Sun Oct 08 22:28:20 2017 +0200
@@ -368,7 +368,7 @@
if \<exists>x\<in>space M. y = f x \<and> z = g x then measure M {x\<in>space M. g x = z} *\<^sub>R y else 0))"
by (auto intro!: sum.cong simp: scaleR_sum_left)
also have "\<dots> = ?r"
- by (subst sum.commute)
+ by (subst sum.swap)
(auto intro!: sum.cong simp: sum.If_cases scaleR_sum_right[symmetric] eq)
finally show "simple_bochner_integral M f = ?r" .
qed
--- a/src/HOL/Analysis/Bounded_Linear_Function.thy Sun Oct 08 22:28:20 2017 +0200
+++ b/src/HOL/Analysis/Bounded_Linear_Function.thy Sun Oct 08 22:28:20 2017 +0200
@@ -387,7 +387,7 @@
have "(\<Sum>j\<in>Basis. \<Sum>i\<in>Basis. (x \<bullet> i * (f i \<bullet> j)) *\<^sub>R j) \<bullet> b
= (\<Sum>j\<in>Basis. if j = b then (\<Sum>i\<in>Basis. (x \<bullet> i * (f i \<bullet> j))) else 0)"
using b
- by (simp add: inner_sum_left inner_Basis if_distrib cong: if_cong) (simp add: sum.commute)
+ by (simp add: inner_sum_left inner_Basis if_distrib cong: if_cong) (simp add: sum.swap)
also have "\<dots> = (\<Sum>i\<in>Basis. (x \<bullet> i * (f i \<bullet> b)))"
using b by (simp add: sum.delta)
also have "\<dots> = f x \<bullet> b"
--- a/src/HOL/Analysis/Caratheodory.thy Sun Oct 08 22:28:20 2017 +0200
+++ b/src/HOL/Analysis/Caratheodory.thy Sun Oct 08 22:28:20 2017 +0200
@@ -44,7 +44,7 @@
qed
also have "\<dots> = (SUP p. \<Sum>i<p. \<Sum>n. f (i, n))"
unfolding suminf_sum[OF summableI, symmetric]
- by (simp add: suminf_eq_SUP SUP_pair sum.commute[of _ "{..< fst _}"])
+ by (simp add: suminf_eq_SUP SUP_pair sum.swap[of _ "{..< fst _}"])
finally show ?thesis unfolding g_def
by (simp add: suminf_eq_SUP)
qed
@@ -592,7 +592,7 @@
assume "\<Union>C = \<Union>D"
with split_sum[OF C D] split_sum[OF D C]
have "(\<Sum>d\<in>D. \<mu> d) = (\<Sum>c\<in>C. \<mu> c)"
- by (simp, subst sum.commute, simp add: ac_simps) }
+ by (simp, subst sum.swap, simp add: ac_simps) }
note sum_eq = this
{ fix C assume C: "C \<subseteq> M" "finite C" "disjoint C"
--- a/src/HOL/Analysis/Cartesian_Euclidean_Space.thy Sun Oct 08 22:28:20 2017 +0200
+++ b/src/HOL/Analysis/Cartesian_Euclidean_Space.thy Sun Oct 08 22:28:20 2017 +0200
@@ -518,14 +518,14 @@
lemma matrix_mul_assoc: "A ** (B ** C) = (A ** B) ** C"
apply (vector matrix_matrix_mult_def sum_distrib_left sum_distrib_right mult.assoc)
- apply (subst sum.commute)
+ apply (subst sum.swap)
apply simp
done
lemma matrix_vector_mul_assoc: "A *v (B *v x) = (A ** B) *v x"
apply (vector matrix_matrix_mult_def matrix_vector_mult_def
sum_distrib_left sum_distrib_right mult.assoc)
- apply (subst sum.commute)
+ apply (subst sum.swap)
apply simp
done
@@ -556,7 +556,7 @@
lemma dot_lmul_matrix: "((x::real ^_) v* A) \<bullet> y = x \<bullet> (A *v y)"
apply (simp add: inner_vec_def matrix_vector_mult_def vector_matrix_mult_def sum_distrib_right sum_distrib_left ac_simps)
- apply (subst sum.commute)
+ apply (subst sum.swap)
apply simp
done
@@ -659,7 +659,7 @@
apply (rule adjoint_unique)
apply (simp add: transpose_def inner_vec_def matrix_vector_mult_def
sum_distrib_right sum_distrib_left)
- apply (subst sum.commute)
+ apply (subst sum.swap)
apply (auto simp add: ac_simps)
done
--- a/src/HOL/Analysis/Determinants.thy Sun Oct 08 22:28:20 2017 +0200
+++ b/src/HOL/Analysis/Determinants.thy Sun Oct 08 22:28:20 2017 +0200
@@ -29,7 +29,7 @@
lemma trace_mul_sym: "trace ((A::'a::comm_semiring_1^'n^'m) ** B) = trace (B**A)"
apply (simp add: trace_def matrix_matrix_mult_def)
- apply (subst sum.commute)
+ apply (subst sum.swap)
apply (simp add: mult.commute)
done
--- a/src/HOL/Analysis/Linear_Algebra.thy Sun Oct 08 22:28:20 2017 +0200
+++ b/src/HOL/Analysis/Linear_Algebra.thy Sun Oct 08 22:28:20 2017 +0200
@@ -1886,7 +1886,7 @@
have "(\<Sum>x\<in>P. norm (f x)) \<le> (\<Sum>x\<in>P. \<Sum>b\<in>Basis. \<bar>f x \<bullet> b\<bar>)"
by (rule sum_mono) (rule norm_le_l1)
also have "(\<Sum>x\<in>P. \<Sum>b\<in>Basis. \<bar>f x \<bullet> b\<bar>) = (\<Sum>b\<in>Basis. \<Sum>x\<in>P. \<bar>f x \<bullet> b\<bar>)"
- by (rule sum.commute)
+ by (rule sum.swap)
also have "\<dots> \<le> of_nat (card (Basis :: 'n set)) * (2 * e)"
proof (rule sum_bounded_above)
fix i :: 'n
--- a/src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy Sun Oct 08 22:28:20 2017 +0200
+++ b/src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy Sun Oct 08 22:28:20 2017 +0200
@@ -648,7 +648,7 @@
if \<exists>x\<in>space M. y = f x \<and> z = g x then y * emeasure M {x\<in>space M. g x = z} else 0))"
by (auto intro!: sum.cong simp: sum_distrib_left)
also have "\<dots> = ?r"
- by (subst sum.commute)
+ by (subst sum.swap)
(auto intro!: sum.cong simp: sum.If_cases scaleR_sum_right[symmetric] eq)
finally show "integral\<^sup>S M f = ?r" .
qed
--- a/src/HOL/Computational_Algebra/Formal_Power_Series.thy Sun Oct 08 22:28:20 2017 +0200
+++ b/src/HOL/Computational_Algebra/Formal_Power_Series.thy Sun Oct 08 22:28:20 2017 +0200
@@ -3133,7 +3133,7 @@
done
also have "\<dots> = sum (\<lambda>i. of_nat (i + 1) * a$(i+1) * (sum (\<lambda>j. (b^ i)$j * of_nat (n - j + 1) * b$(n - j + 1)) {0..n})) {0.. n}"
unfolding sum_distrib_left
- apply (subst sum.commute)
+ apply (subst sum.swap)
apply (rule sum.cong, rule refl)+
apply simp
done
@@ -3314,7 +3314,7 @@
done
have "?r = sum (\<lambda>i. sum (\<lambda>(k,m). a$k * (c^k)$i * b$m * (d^m) $ (n - i)) {(k,m). k + m \<le> n}) {0..n}"
apply (simp add: fps_mult_nth sum_distrib_left)
- apply (subst sum.commute)
+ apply (subst sum.swap)
apply (rule sum.cong)
apply (auto simp add: field_simps)
done
--- a/src/HOL/Groups_Big.thy Sun Oct 08 22:28:20 2017 +0200
+++ b/src/HOL/Groups_Big.thy Sun Oct 08 22:28:20 2017 +0200
@@ -425,14 +425,14 @@
by (simp add: H)
qed
-lemma commute: "F (\<lambda>i. F (g i) B) A = F (\<lambda>j. F (\<lambda>i. g i j) A) B"
+lemma swap: "F (\<lambda>i. F (g i) B) A = F (\<lambda>j. F (\<lambda>i. g i j) A) B"
unfolding cartesian_product
by (rule reindex_bij_witness [where i = "\<lambda>(i, j). (j, i)" and j = "\<lambda>(i, j). (j, i)"]) auto
-lemma commute_restrict:
+lemma swap_restrict:
"finite A \<Longrightarrow> finite B \<Longrightarrow>
F (\<lambda>x. F (g x) {y. y \<in> B \<and> R x y}) A = F (\<lambda>y. F (\<lambda>x. g x y) {x. x \<in> A \<and> R x y}) B"
- by (simp add: inter_filter) (rule commute)
+ by (simp add: inter_filter) (rule swap)
lemma Plus:
fixes A :: "'b set" and B :: "'c set"
@@ -540,7 +540,7 @@
then have "sum g S = sum (\<lambda>x. sum (\<lambda>y. g x) {y. y\<in> f`S \<and> f x = y}) S"
by simp
also have "\<dots> = sum (\<lambda>y. sum g {x. x \<in> S \<and> f x = y}) (f ` S)"
- by (rule sum.commute_restrict [OF fin finite_imageI [OF fin]])
+ by (rule sum.swap_restrict [OF fin finite_imageI [OF fin]])
finally show ?thesis .
qed
@@ -843,7 +843,7 @@
lemma sum_product:
fixes f :: "'a \<Rightarrow> 'b::semiring_0"
shows "sum f A * sum g B = (\<Sum>i\<in>A. \<Sum>j\<in>B. f i * g j)"
- by (simp add: sum_distrib_left sum_distrib_right) (rule sum.commute)
+ by (simp add: sum_distrib_left sum_distrib_right) (rule sum.swap)
lemma sum_mult_sum_if_inj:
fixes f :: "'a \<Rightarrow> 'b::semiring_0"
@@ -1021,7 +1021,7 @@
have "?l = sum (\<lambda>i. sum (\<lambda>x.1) {j\<in>t. R i j}) s"
by auto
also have "\<dots> = ?r"
- unfolding sum.commute_restrict [OF assms(1-2)]
+ unfolding sum.swap_restrict [OF assms(1-2)]
using assms(3) by auto
finally show ?thesis .
qed
--- a/src/HOL/Inequalities.thy Sun Oct 08 22:28:20 2017 +0200
+++ b/src/HOL/Inequalities.thy Sun Oct 08 22:28:20 2017 +0200
@@ -59,7 +59,7 @@
let ?S = "(\<Sum>j=0..<n. (\<Sum>k=0..<n. (a j - a k) * (b j - b k)))"
have "2 * (of_nat n * (\<Sum>j=0..<n. (a j * b j)) - (\<Sum>j=0..<n. b j) * (\<Sum>k=0..<n. a k)) = ?S"
by (simp only: one_add_one[symmetric] algebra_simps)
- (simp add: algebra_simps sum_subtractf sum.distrib sum.commute[of "\<lambda>i j. a i * b j"] sum_distrib_left)
+ (simp add: algebra_simps sum_subtractf sum.distrib sum.swap[of "\<lambda>i j. a i * b j"] sum_distrib_left)
also
{ fix i j::nat assume "i<n" "j<n"
hence "a i - a j \<le> 0 \<and> b i - b j \<ge> 0 \<or> a i - a j \<ge> 0 \<and> b i - b j \<le> 0"
--- a/src/HOL/Library/Groups_Big_Fun.thy Sun Oct 08 22:28:20 2017 +0200
+++ b/src/HOL/Library/Groups_Big_Fun.thy Sun Oct 08 22:28:20 2017 +0200
@@ -106,7 +106,7 @@
by (simp add: expand_superset [of "{a. g a \<noteq> \<^bold>1} \<union> {a. h a \<noteq> \<^bold>1}"] F.distrib)
qed
-lemma commute:
+lemma swap:
assumes "finite C"
assumes subset: "{a. \<exists>b. g a b \<noteq> \<^bold>1} \<times> {b. \<exists>a. g a b \<noteq> \<^bold>1} \<subseteq> C" (is "?A \<times> ?B \<subseteq> C")
shows "G (\<lambda>a. G (g a)) = G (\<lambda>b. G (\<lambda>a. g a b))"
@@ -122,7 +122,7 @@
"{a. F.F (g a) {b. \<exists>a. g a b \<noteq> \<^bold>1} \<noteq> \<^bold>1} \<subseteq> {a. \<exists>b. g a b \<noteq> \<^bold>1}"
"{a. F.F (\<lambda>aa. g aa a) {a. \<exists>b. g a b \<noteq> \<^bold>1} \<noteq> \<^bold>1} \<subseteq> {b. \<exists>a. g a b \<noteq> \<^bold>1}"
by (auto elim: F.not_neutral_contains_not_neutral)
- from F.commute have
+ from F.swap have
"F.F (\<lambda>a. F.F (g a) {b. \<exists>a. g a b \<noteq> \<^bold>1}) {a. \<exists>b. g a b \<noteq> \<^bold>1} =
F.F (\<lambda>b. F.F (\<lambda>a. g a b) {a. \<exists>b. g a b \<noteq> \<^bold>1}) {b. \<exists>a. g a b \<noteq> \<^bold>1}" .
with subsets fins have "G (\<lambda>a. F.F (g a) {b. \<exists>a. g a b \<noteq> \<^bold>1}) =
--- a/src/HOL/Probability/Probability_Mass_Function.thy Sun Oct 08 22:28:20 2017 +0200
+++ b/src/HOL/Probability/Probability_Mass_Function.thy Sun Oct 08 22:28:20 2017 +0200
@@ -797,7 +797,7 @@
(insert assms, auto simp: scaleR_sum_left)
qed
also have "\<dots> = (\<Sum>j\<in>A. pmf p j *\<^sub>R (\<Sum>i\<in>(\<Union>x\<in>A. set_pmf (f x)). pmf (f j) i *\<^sub>R h i))"
- by (subst sum.commute) (simp add: scaleR_sum_right)
+ by (subst sum.swap) (simp add: scaleR_sum_right)
also have "\<dots> = (\<Sum>j\<in>A. pmf p j *\<^sub>R measure_pmf.expectation (f j) h)"
proof (intro sum.cong refl, goal_cases)
case (1 x)
@@ -2141,7 +2141,7 @@
by (intro sum.cong refl, subst sum_list_map_filter', subst sum_list_sum_nth) simp
also have "\<dots> = (\<Sum>xa = 0..<length xs. (\<Sum>x\<in>set (map fst xs).
if fst (xs ! xa) = x \<and> x \<in> A then snd (xs ! xa) else 0))"
- by (rule sum.commute)
+ by (rule sum.swap)
also have "\<dots> = (\<Sum>xa = 0..<length xs. if fst (xs ! xa) \<in> A then
(\<Sum>x\<in>set (map fst xs). if x = fst (xs ! xa) then snd (xs ! xa) else 0) else 0)"
by (auto intro!: sum.cong sum.neutral simp del: sum.delta)
--- a/src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy Sun Oct 08 22:28:20 2017 +0200
+++ b/src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy Sun Oct 08 22:28:20 2017 +0200
@@ -321,7 +321,7 @@
apply metis
done
also have "\<dots> = - (\<Sum>y\<in>Y`msgs. (\<Sum>x\<in>X`msgs. (\<P>(X ; Y) {(x, y)}) * log b ((\<P>(X ; Y) {(x, y)}) / (\<P>(Y) {y}))))"
- by (subst sum.commute) rule
+ by (subst sum.swap) rule
also have "\<dots> = -(\<Sum>y\<in>Y`msgs. (\<P>(Y) {y}) * (\<Sum>x\<in>X`msgs. (\<P>(X ; Y) {(x,y)}) / (\<P>(Y) {y}) * log b ((\<P>(X ; Y) {(x,y)}) / (\<P>(Y) {y}))))"
by (auto simp add: sum_distrib_left vimage_def intro!: sum.cong prob_conj_imp1)
finally show "- (\<Sum>(x, y)\<in>(\<lambda>x. (X x, Y x)) ` msgs. (\<P>(X ; Y) {(x, y)}) * log b ((\<P>(X ; Y) {(x, y)}) / (\<P>(Y) {y}))) =