avoid name clashes on interpretation of abstract locales
authorhaftmann
Sun Oct 08 22:28:20 2017 +0200 (19 months ago)
changeset 668043f9bb52082c4
parent 66803 dd8922885a68
child 66805 274b4edca859
avoid name clashes on interpretation of abstract locales
NEWS
src/HOL/Analysis/Bochner_Integration.thy
src/HOL/Analysis/Bounded_Linear_Function.thy
src/HOL/Analysis/Caratheodory.thy
src/HOL/Analysis/Cartesian_Euclidean_Space.thy
src/HOL/Analysis/Determinants.thy
src/HOL/Analysis/Linear_Algebra.thy
src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy
src/HOL/Computational_Algebra/Formal_Power_Series.thy
src/HOL/Groups_Big.thy
src/HOL/Inequalities.thy
src/HOL/Library/Groups_Big_Fun.thy
src/HOL/Probability/Probability_Mass_Function.thy
src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy
     1.1 --- a/NEWS	Sun Oct 08 22:28:20 2017 +0200
     1.2 +++ b/NEWS	Sun Oct 08 22:28:20 2017 +0200
     1.3 @@ -47,6 +47,10 @@
     1.4  * Fact mod_mult_self4 (on nat) renamed to mod_mult_self3', to avoid clash
     1.5  with fact mod_mult_self4 (on more generic semirings). INCOMPATIBILITY.
     1.6  
     1.7 +* Facts sum.commute(_restrict) and prod.commute(_restrict) renamed to
     1.8 +sum.swap(_restrict) and prod.swap(_restrict), to avoid name clashes
     1.9 +on interpretation of abstract locales. INCOMPATIBILITY.
    1.10 +
    1.11  * Predicate pairwise_coprime abolished, use "pairwise coprime" instead.
    1.12  INCOMPATIBILITY.
    1.13  
     2.1 --- a/src/HOL/Analysis/Bochner_Integration.thy	Sun Oct 08 22:28:20 2017 +0200
     2.2 +++ b/src/HOL/Analysis/Bochner_Integration.thy	Sun Oct 08 22:28:20 2017 +0200
     2.3 @@ -368,7 +368,7 @@
     2.4        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))"
     2.5      by (auto intro!: sum.cong simp: scaleR_sum_left)
     2.6    also have "\<dots> = ?r"
     2.7 -    by (subst sum.commute)
     2.8 +    by (subst sum.swap)
     2.9         (auto intro!: sum.cong simp: sum.If_cases scaleR_sum_right[symmetric] eq)
    2.10    finally show "simple_bochner_integral M f = ?r" .
    2.11  qed
     3.1 --- a/src/HOL/Analysis/Bounded_Linear_Function.thy	Sun Oct 08 22:28:20 2017 +0200
     3.2 +++ b/src/HOL/Analysis/Bounded_Linear_Function.thy	Sun Oct 08 22:28:20 2017 +0200
     3.3 @@ -387,7 +387,7 @@
     3.4    have "(\<Sum>j\<in>Basis. \<Sum>i\<in>Basis. (x \<bullet> i * (f i \<bullet> j)) *\<^sub>R j) \<bullet> b
     3.5      = (\<Sum>j\<in>Basis. if j = b then (\<Sum>i\<in>Basis. (x \<bullet> i * (f i \<bullet> j))) else 0)"
     3.6      using b
     3.7 -    by (simp add: inner_sum_left inner_Basis if_distrib cong: if_cong) (simp add: sum.commute)
     3.8 +    by (simp add: inner_sum_left inner_Basis if_distrib cong: if_cong) (simp add: sum.swap)
     3.9    also have "\<dots> = (\<Sum>i\<in>Basis. (x \<bullet> i * (f i \<bullet> b)))"
    3.10      using b by (simp add: sum.delta)
    3.11    also have "\<dots> = f x \<bullet> b"
     4.1 --- a/src/HOL/Analysis/Caratheodory.thy	Sun Oct 08 22:28:20 2017 +0200
     4.2 +++ b/src/HOL/Analysis/Caratheodory.thy	Sun Oct 08 22:28:20 2017 +0200
     4.3 @@ -44,7 +44,7 @@
     4.4    qed
     4.5    also have "\<dots> = (SUP p. \<Sum>i<p. \<Sum>n. f (i, n))"
     4.6      unfolding suminf_sum[OF summableI, symmetric]
     4.7 -    by (simp add: suminf_eq_SUP SUP_pair sum.commute[of _ "{..< fst _}"])
     4.8 +    by (simp add: suminf_eq_SUP SUP_pair sum.swap[of _ "{..< fst _}"])
     4.9    finally show ?thesis unfolding g_def
    4.10      by (simp add: suminf_eq_SUP)
    4.11  qed
    4.12 @@ -592,7 +592,7 @@
    4.13      assume "\<Union>C = \<Union>D"
    4.14      with split_sum[OF C D] split_sum[OF D C]
    4.15      have "(\<Sum>d\<in>D. \<mu> d) = (\<Sum>c\<in>C. \<mu> c)"
    4.16 -      by (simp, subst sum.commute, simp add: ac_simps) }
    4.17 +      by (simp, subst sum.swap, simp add: ac_simps) }
    4.18    note sum_eq = this
    4.19  
    4.20    { fix C assume C: "C \<subseteq> M" "finite C" "disjoint C"
     5.1 --- a/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Sun Oct 08 22:28:20 2017 +0200
     5.2 +++ b/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Sun Oct 08 22:28:20 2017 +0200
     5.3 @@ -518,14 +518,14 @@
     5.4  
     5.5  lemma matrix_mul_assoc: "A ** (B ** C) = (A ** B) ** C"
     5.6    apply (vector matrix_matrix_mult_def sum_distrib_left sum_distrib_right mult.assoc)
     5.7 -  apply (subst sum.commute)
     5.8 +  apply (subst sum.swap)
     5.9    apply simp
    5.10    done
    5.11  
    5.12  lemma matrix_vector_mul_assoc: "A *v (B *v x) = (A ** B) *v x"
    5.13    apply (vector matrix_matrix_mult_def matrix_vector_mult_def
    5.14      sum_distrib_left sum_distrib_right mult.assoc)
    5.15 -  apply (subst sum.commute)
    5.16 +  apply (subst sum.swap)
    5.17    apply simp
    5.18    done
    5.19  
    5.20 @@ -556,7 +556,7 @@
    5.21  
    5.22  lemma dot_lmul_matrix: "((x::real ^_) v* A) \<bullet> y = x \<bullet> (A *v y)"
    5.23    apply (simp add: inner_vec_def matrix_vector_mult_def vector_matrix_mult_def sum_distrib_right sum_distrib_left ac_simps)
    5.24 -  apply (subst sum.commute)
    5.25 +  apply (subst sum.swap)
    5.26    apply simp
    5.27    done
    5.28  
    5.29 @@ -659,7 +659,7 @@
    5.30    apply (rule adjoint_unique)
    5.31    apply (simp add: transpose_def inner_vec_def matrix_vector_mult_def
    5.32      sum_distrib_right sum_distrib_left)
    5.33 -  apply (subst sum.commute)
    5.34 +  apply (subst sum.swap)
    5.35    apply (auto simp add: ac_simps)
    5.36    done
    5.37  
     6.1 --- a/src/HOL/Analysis/Determinants.thy	Sun Oct 08 22:28:20 2017 +0200
     6.2 +++ b/src/HOL/Analysis/Determinants.thy	Sun Oct 08 22:28:20 2017 +0200
     6.3 @@ -29,7 +29,7 @@
     6.4  
     6.5  lemma trace_mul_sym: "trace ((A::'a::comm_semiring_1^'n^'m) ** B) = trace (B**A)"
     6.6    apply (simp add: trace_def matrix_matrix_mult_def)
     6.7 -  apply (subst sum.commute)
     6.8 +  apply (subst sum.swap)
     6.9    apply (simp add: mult.commute)
    6.10    done
    6.11  
     7.1 --- a/src/HOL/Analysis/Linear_Algebra.thy	Sun Oct 08 22:28:20 2017 +0200
     7.2 +++ b/src/HOL/Analysis/Linear_Algebra.thy	Sun Oct 08 22:28:20 2017 +0200
     7.3 @@ -1886,7 +1886,7 @@
     7.4    have "(\<Sum>x\<in>P. norm (f x)) \<le> (\<Sum>x\<in>P. \<Sum>b\<in>Basis. \<bar>f x \<bullet> b\<bar>)"
     7.5      by (rule sum_mono) (rule norm_le_l1)
     7.6    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>)"
     7.7 -    by (rule sum.commute)
     7.8 +    by (rule sum.swap)
     7.9    also have "\<dots> \<le> of_nat (card (Basis :: 'n set)) * (2 * e)"
    7.10    proof (rule sum_bounded_above)
    7.11      fix i :: 'n
     8.1 --- a/src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy	Sun Oct 08 22:28:20 2017 +0200
     8.2 +++ b/src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy	Sun Oct 08 22:28:20 2017 +0200
     8.3 @@ -648,7 +648,7 @@
     8.4        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))"
     8.5      by (auto intro!: sum.cong simp: sum_distrib_left)
     8.6    also have "\<dots> = ?r"
     8.7 -    by (subst sum.commute)
     8.8 +    by (subst sum.swap)
     8.9         (auto intro!: sum.cong simp: sum.If_cases scaleR_sum_right[symmetric] eq)
    8.10    finally show "integral\<^sup>S M f = ?r" .
    8.11  qed
     9.1 --- a/src/HOL/Computational_Algebra/Formal_Power_Series.thy	Sun Oct 08 22:28:20 2017 +0200
     9.2 +++ b/src/HOL/Computational_Algebra/Formal_Power_Series.thy	Sun Oct 08 22:28:20 2017 +0200
     9.3 @@ -3133,7 +3133,7 @@
     9.4        done
     9.5      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}"
     9.6        unfolding sum_distrib_left
     9.7 -      apply (subst sum.commute)
     9.8 +      apply (subst sum.swap)
     9.9        apply (rule sum.cong, rule refl)+
    9.10        apply simp
    9.11        done
    9.12 @@ -3314,7 +3314,7 @@
    9.13      done
    9.14    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}"
    9.15      apply (simp add: fps_mult_nth sum_distrib_left)
    9.16 -    apply (subst sum.commute)
    9.17 +    apply (subst sum.swap)
    9.18      apply (rule sum.cong)
    9.19      apply (auto simp add: field_simps)
    9.20      done
    10.1 --- a/src/HOL/Groups_Big.thy	Sun Oct 08 22:28:20 2017 +0200
    10.2 +++ b/src/HOL/Groups_Big.thy	Sun Oct 08 22:28:20 2017 +0200
    10.3 @@ -425,14 +425,14 @@
    10.4      by (simp add: H)
    10.5  qed
    10.6  
    10.7 -lemma commute: "F (\<lambda>i. F (g i) B) A = F (\<lambda>j. F (\<lambda>i. g i j) A) B"
    10.8 +lemma swap: "F (\<lambda>i. F (g i) B) A = F (\<lambda>j. F (\<lambda>i. g i j) A) B"
    10.9    unfolding cartesian_product
   10.10    by (rule reindex_bij_witness [where i = "\<lambda>(i, j). (j, i)" and j = "\<lambda>(i, j). (j, i)"]) auto
   10.11  
   10.12 -lemma commute_restrict:
   10.13 +lemma swap_restrict:
   10.14    "finite A \<Longrightarrow> finite B \<Longrightarrow>
   10.15      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"
   10.16 -  by (simp add: inter_filter) (rule commute)
   10.17 +  by (simp add: inter_filter) (rule swap)
   10.18  
   10.19  lemma Plus:
   10.20    fixes A :: "'b set" and B :: "'c set"
   10.21 @@ -540,7 +540,7 @@
   10.22    then have "sum g S = sum (\<lambda>x. sum (\<lambda>y. g x) {y. y\<in> f`S \<and> f x = y}) S"
   10.23      by simp
   10.24    also have "\<dots> = sum (\<lambda>y. sum g {x. x \<in> S \<and> f x = y}) (f ` S)"
   10.25 -    by (rule sum.commute_restrict [OF fin finite_imageI [OF fin]])
   10.26 +    by (rule sum.swap_restrict [OF fin finite_imageI [OF fin]])
   10.27    finally show ?thesis .
   10.28  qed
   10.29  
   10.30 @@ -843,7 +843,7 @@
   10.31  lemma sum_product:
   10.32    fixes f :: "'a \<Rightarrow> 'b::semiring_0"
   10.33    shows "sum f A * sum g B = (\<Sum>i\<in>A. \<Sum>j\<in>B. f i * g j)"
   10.34 -  by (simp add: sum_distrib_left sum_distrib_right) (rule sum.commute)
   10.35 +  by (simp add: sum_distrib_left sum_distrib_right) (rule sum.swap)
   10.36  
   10.37  lemma sum_mult_sum_if_inj:
   10.38    fixes f :: "'a \<Rightarrow> 'b::semiring_0"
   10.39 @@ -1021,7 +1021,7 @@
   10.40    have "?l = sum (\<lambda>i. sum (\<lambda>x.1) {j\<in>t. R i j}) s"
   10.41      by auto
   10.42    also have "\<dots> = ?r"
   10.43 -    unfolding sum.commute_restrict [OF assms(1-2)]
   10.44 +    unfolding sum.swap_restrict [OF assms(1-2)]
   10.45      using assms(3) by auto
   10.46    finally show ?thesis .
   10.47  qed
    11.1 --- a/src/HOL/Inequalities.thy	Sun Oct 08 22:28:20 2017 +0200
    11.2 +++ b/src/HOL/Inequalities.thy	Sun Oct 08 22:28:20 2017 +0200
    11.3 @@ -59,7 +59,7 @@
    11.4    let ?S = "(\<Sum>j=0..<n. (\<Sum>k=0..<n. (a j - a k) * (b j - b k)))"
    11.5    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"
    11.6      by (simp only: one_add_one[symmetric] algebra_simps)
    11.7 -      (simp add: algebra_simps sum_subtractf sum.distrib sum.commute[of "\<lambda>i j. a i * b j"] sum_distrib_left)
    11.8 +      (simp add: algebra_simps sum_subtractf sum.distrib sum.swap[of "\<lambda>i j. a i * b j"] sum_distrib_left)
    11.9    also
   11.10    { fix i j::nat assume "i<n" "j<n"
   11.11      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"
    12.1 --- a/src/HOL/Library/Groups_Big_Fun.thy	Sun Oct 08 22:28:20 2017 +0200
    12.2 +++ b/src/HOL/Library/Groups_Big_Fun.thy	Sun Oct 08 22:28:20 2017 +0200
    12.3 @@ -106,7 +106,7 @@
    12.4      by (simp add: expand_superset [of "{a. g a \<noteq> \<^bold>1} \<union> {a. h a \<noteq> \<^bold>1}"] F.distrib)
    12.5  qed
    12.6  
    12.7 -lemma commute:
    12.8 +lemma swap:
    12.9    assumes "finite C"
   12.10    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")
   12.11    shows "G (\<lambda>a. G (g a)) = G (\<lambda>b. G (\<lambda>a. g a b))"
   12.12 @@ -122,7 +122,7 @@
   12.13      "{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}"
   12.14      "{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}"
   12.15      by (auto elim: F.not_neutral_contains_not_neutral)
   12.16 -  from F.commute have
   12.17 +  from F.swap have
   12.18      "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} =
   12.19        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}" .
   12.20    with subsets fins have "G (\<lambda>a. F.F (g a) {b. \<exists>a. g a b \<noteq> \<^bold>1}) =
    13.1 --- a/src/HOL/Probability/Probability_Mass_Function.thy	Sun Oct 08 22:28:20 2017 +0200
    13.2 +++ b/src/HOL/Probability/Probability_Mass_Function.thy	Sun Oct 08 22:28:20 2017 +0200
    13.3 @@ -797,7 +797,7 @@
    13.4           (insert assms, auto simp: scaleR_sum_left)
    13.5    qed
    13.6    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))"
    13.7 -    by (subst sum.commute) (simp add: scaleR_sum_right)
    13.8 +    by (subst sum.swap) (simp add: scaleR_sum_right)
    13.9    also have "\<dots> = (\<Sum>j\<in>A. pmf p j *\<^sub>R measure_pmf.expectation (f j) h)"
   13.10    proof (intro sum.cong refl, goal_cases)
   13.11      case (1 x)
   13.12 @@ -2141,7 +2141,7 @@
   13.13      by (intro sum.cong refl, subst sum_list_map_filter', subst sum_list_sum_nth) simp
   13.14    also have "\<dots> = (\<Sum>xa = 0..<length xs. (\<Sum>x\<in>set (map fst xs).
   13.15                       if fst (xs ! xa) = x \<and> x \<in> A then snd (xs ! xa) else 0))"
   13.16 -    by (rule sum.commute)
   13.17 +    by (rule sum.swap)
   13.18    also have "\<dots> = (\<Sum>xa = 0..<length xs. if fst (xs ! xa) \<in> A then
   13.19                       (\<Sum>x\<in>set (map fst xs). if x = fst (xs ! xa) then snd (xs ! xa) else 0) else 0)"
   13.20      by (auto intro!: sum.cong sum.neutral simp del: sum.delta)
    14.1 --- a/src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy	Sun Oct 08 22:28:20 2017 +0200
    14.2 +++ b/src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy	Sun Oct 08 22:28:20 2017 +0200
    14.3 @@ -321,7 +321,7 @@
    14.4      apply metis
    14.5      done
    14.6    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}))))"
    14.7 -    by (subst sum.commute) rule
    14.8 +    by (subst sum.swap) rule
    14.9    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}))))"
   14.10      by (auto simp add: sum_distrib_left vimage_def intro!: sum.cong prob_conj_imp1)
   14.11    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}))) =