src/HOL/Library/Groups_Big_Fun.thy
changeset 66804 3f9bb52082c4
parent 64272 f76b6dda2e56
child 67764 0f8cb5568b63
     1.1 --- a/src/HOL/Library/Groups_Big_Fun.thy	Sun Oct 08 22:28:20 2017 +0200
     1.2 +++ b/src/HOL/Library/Groups_Big_Fun.thy	Sun Oct 08 22:28:20 2017 +0200
     1.3 @@ -106,7 +106,7 @@
     1.4      by (simp add: expand_superset [of "{a. g a \<noteq> \<^bold>1} \<union> {a. h a \<noteq> \<^bold>1}"] F.distrib)
     1.5  qed
     1.6  
     1.7 -lemma commute:
     1.8 +lemma swap:
     1.9    assumes "finite C"
    1.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")
    1.11    shows "G (\<lambda>a. G (g a)) = G (\<lambda>b. G (\<lambda>a. g a b))"
    1.12 @@ -122,7 +122,7 @@
    1.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}"
    1.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}"
    1.15      by (auto elim: F.not_neutral_contains_not_neutral)
    1.16 -  from F.commute have
    1.17 +  from F.swap have
    1.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} =
    1.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}" .
    1.20    with subsets fins have "G (\<lambda>a. F.F (g a) {b. \<exists>a. g a b \<noteq> \<^bold>1}) =