# HG changeset patch
# User haftmann
# Date 1507494500 -7200
# Node ID 3f9bb52082c414903e547f10922d33533dc9d8e0
# Parent  dd8922885a6831ce96bab8c9a9f04802b13b74fd
avoid name clashes on interpretation of abstract locales

diff -r dd8922885a68 -r 3f9bb52082c4 NEWS
--- 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.
 
diff -r dd8922885a68 -r 3f9bb52082c4 src/HOL/Analysis/Bochner_Integration.thy
--- 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
diff -r dd8922885a68 -r 3f9bb52082c4 src/HOL/Analysis/Bounded_Linear_Function.thy
--- 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"
diff -r dd8922885a68 -r 3f9bb52082c4 src/HOL/Analysis/Caratheodory.thy
--- 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"
diff -r dd8922885a68 -r 3f9bb52082c4 src/HOL/Analysis/Cartesian_Euclidean_Space.thy
--- 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
 
diff -r dd8922885a68 -r 3f9bb52082c4 src/HOL/Analysis/Determinants.thy
--- 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
 
diff -r dd8922885a68 -r 3f9bb52082c4 src/HOL/Analysis/Linear_Algebra.thy
--- 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
diff -r dd8922885a68 -r 3f9bb52082c4 src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy
--- 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
diff -r dd8922885a68 -r 3f9bb52082c4 src/HOL/Computational_Algebra/Formal_Power_Series.thy
--- 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
diff -r dd8922885a68 -r 3f9bb52082c4 src/HOL/Groups_Big.thy
--- 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
diff -r dd8922885a68 -r 3f9bb52082c4 src/HOL/Inequalities.thy
--- 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"
diff -r dd8922885a68 -r 3f9bb52082c4 src/HOL/Library/Groups_Big_Fun.thy
--- 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}) =
diff -r dd8922885a68 -r 3f9bb52082c4 src/HOL/Probability/Probability_Mass_Function.thy
--- 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)
diff -r dd8922885a68 -r 3f9bb52082c4 src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy
--- 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}))) =