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.4      by (simp add: H)
     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