src/HOL/Groups_Big.thy
 changeset 66804 3f9bb52082c4 parent 66364 fa3247e6ee4b child 66936 cf8d8fc23891
```     1.1 --- a/src/HOL/Groups_Big.thy	Sun Oct 08 22:28:20 2017 +0200
1.2 +++ b/src/HOL/Groups_Big.thy	Sun Oct 08 22:28:20 2017 +0200
1.3 @@ -425,14 +425,14 @@
1.5  qed
1.6
1.7 -lemma commute: "F (\<lambda>i. F (g i) B) A = F (\<lambda>j. F (\<lambda>i. g i j) A) B"
1.8 +lemma swap: "F (\<lambda>i. F (g i) B) A = F (\<lambda>j. F (\<lambda>i. g i j) A) B"
1.9    unfolding cartesian_product
1.10    by (rule reindex_bij_witness [where i = "\<lambda>(i, j). (j, i)" and j = "\<lambda>(i, j). (j, i)"]) auto
1.11
1.12 -lemma commute_restrict:
1.13 +lemma swap_restrict:
1.14    "finite A \<Longrightarrow> finite B \<Longrightarrow>
1.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"
1.16 -  by (simp add: inter_filter) (rule commute)
1.17 +  by (simp add: inter_filter) (rule swap)
1.18
1.19  lemma Plus:
1.20    fixes A :: "'b set" and B :: "'c set"
1.21 @@ -540,7 +540,7 @@
1.22    then have "sum g S = sum (\<lambda>x. sum (\<lambda>y. g x) {y. y\<in> f`S \<and> f x = y}) S"
1.23      by simp
1.24    also have "\<dots> = sum (\<lambda>y. sum g {x. x \<in> S \<and> f x = y}) (f ` S)"
1.25 -    by (rule sum.commute_restrict [OF fin finite_imageI [OF fin]])
1.26 +    by (rule sum.swap_restrict [OF fin finite_imageI [OF fin]])
1.27    finally show ?thesis .
1.28  qed
1.29
1.30 @@ -843,7 +843,7 @@
1.31  lemma sum_product:
1.32    fixes f :: "'a \<Rightarrow> 'b::semiring_0"
1.33    shows "sum f A * sum g B = (\<Sum>i\<in>A. \<Sum>j\<in>B. f i * g j)"
1.34 -  by (simp add: sum_distrib_left sum_distrib_right) (rule sum.commute)
1.35 +  by (simp add: sum_distrib_left sum_distrib_right) (rule sum.swap)
1.36
1.37  lemma sum_mult_sum_if_inj:
1.38    fixes f :: "'a \<Rightarrow> 'b::semiring_0"
1.39 @@ -1021,7 +1021,7 @@
1.40    have "?l = sum (\<lambda>i. sum (\<lambda>x.1) {j\<in>t. R i j}) s"
1.41      by auto
1.42    also have "\<dots> = ?r"
1.43 -    unfolding sum.commute_restrict [OF assms(1-2)]
1.44 +    unfolding sum.swap_restrict [OF assms(1-2)]
1.45      using assms(3) by auto
1.46    finally show ?thesis .
1.47  qed
```