# HG changeset patch
# User haftmann
# Date 1620539330 0
# Node ID 1bd3463e30b8361b92ddd9811080f05737f49a72
# Parent  a037f01aedabbaaf54002213a93b2e785fdb495f
more elementary swap

diff -r a037f01aedab -r 1bd3463e30b8 NEWS
--- a/NEWS	Fri May 07 16:49:08 2021 +0200
+++ b/NEWS	Sun May 09 05:48:50 2021 +0000
@@ -94,8 +94,12 @@
 * Lemma "permutes_induct" has been given stronger
 hypotheses and named premises.  INCOMPATIBILITY.
 
-* Combinator "Fun.swap" moved into separate theory "Transposition" in
-HOL-Combinatorics.  INCOMPATIBILITY.
+* Theory "Transposition" in HOL-Combinatorics provides elementary
+swap operation "transpose".
+
+* Combinator "Fun.swap" resolved into a mere input abbreviation
+in separate theory "Transposition" in HOL-Combinatorics.
+INCOMPATIBILITY.
 
 
 *** ML ***
diff -r a037f01aedab -r 1bd3463e30b8 src/HOL/Algebra/Sym_Groups.thy
--- a/src/HOL/Algebra/Sym_Groups.thy	Fri May 07 16:49:08 2021 +0200
+++ b/src/HOL/Algebra/Sym_Groups.thy	Sun May 09 05:48:50 2021 +0000
@@ -158,7 +158,7 @@
     empty:  "swapidseq_ext {} 0 id"
   | single: "\<lbrakk> swapidseq_ext S n p; a \<notin> S \<rbrakk> \<Longrightarrow> swapidseq_ext (insert a S) n p"
   | comp:   "\<lbrakk> swapidseq_ext S n p; a \<noteq> b \<rbrakk> \<Longrightarrow>
-               swapidseq_ext (insert a (insert b S)) (Suc n) ((Fun.swap a b id) \<circ> p)"
+               swapidseq_ext (insert a (insert b S)) (Suc n) ((transpose a b) \<circ> p)"
 
 
 lemma swapidseq_ext_finite:
@@ -180,7 +180,7 @@
   then show ?case by simp
 next
   case (comp S n p a b)
-  then have \<open>swapidseq (Suc n) (Fun.swap a b id \<circ> p)\<close>
+  then have \<open>swapidseq (Suc n) (transpose a b \<circ> p)\<close>
     by (simp add: comp_Suc)
   then show ?case by (simp add: comp_def)
 qed
@@ -205,12 +205,12 @@
 lemma swapidseq_ext_backwards:
   assumes "swapidseq_ext A (Suc n) p"
   shows "\<exists>a b A' p'. a \<noteq> b \<and> A = (insert a (insert b A')) \<and>
-                     swapidseq_ext A' n p' \<and> p = (Fun.swap a b id) \<circ> p'"
+                     swapidseq_ext A' n p' \<and> p = (transpose a b) \<circ> p'"
 proof -
   { fix A n k and p :: "'a \<Rightarrow> 'a"
     assume "swapidseq_ext A n p" "n = Suc k"
     hence "\<exists>a b A' p'. a \<noteq> b \<and> A = (insert a (insert b A')) \<and>
-                       swapidseq_ext A' k p' \<and> p = (Fun.swap a b id) \<circ> p'"
+                       swapidseq_ext A' k p' \<and> p = (transpose a b) \<circ> p'"
     proof (induction, simp)
       case single thus ?case
         by (metis Un_insert_right insert_iff insert_is_Un swapidseq_ext.single)
@@ -224,13 +224,13 @@
 
 lemma swapidseq_ext_backwards':
   assumes "swapidseq_ext A (Suc n) p"
-  shows "\<exists>a b A' p'. a \<in> A \<and> b \<in> A \<and> a \<noteq> b \<and> swapidseq_ext A n p' \<and> p = (Fun.swap a b id) \<circ> p'"
+  shows "\<exists>a b A' p'. a \<in> A \<and> b \<in> A \<and> a \<noteq> b \<and> swapidseq_ext A n p' \<and> p = (transpose a b) \<circ> p'"
   using swapidseq_ext_backwards[OF assms] swapidseq_ext_finite_expansion
   by (metis Un_insert_left assms insertI1 sup.idem sup_commute swapidseq_ext_finite)
 
 lemma swapidseq_ext_endswap:
   assumes "swapidseq_ext S n p" "a \<noteq> b"
-  shows "swapidseq_ext (insert a (insert b S)) (Suc n) (p \<circ> (Fun.swap a b id))"
+  shows "swapidseq_ext (insert a (insert b S)) (Suc n) (p \<circ> (transpose a b))"
   using assms
 proof (induction n arbitrary: S p a b)
   case 0 hence "p = id"
@@ -241,12 +241,12 @@
   case (Suc n)
   then obtain c d S' and p' :: "'a \<Rightarrow> 'a"
     where cd: "c \<noteq> d" and S: "S = (insert c (insert d S'))" "swapidseq_ext S' n p'"
-      and p: "p = (Fun.swap c d id) \<circ> p'"
+      and p: "p = transpose c d \<circ> p'"
     using swapidseq_ext_backwards[OF Suc(2)] by blast
-  hence "swapidseq_ext (insert a (insert b S')) (Suc n) (p' \<circ> (Fun.swap a b id))"
+  hence "swapidseq_ext (insert a (insert b S')) (Suc n) (p' \<circ> (transpose a b))"
     by (simp add: Suc.IH Suc.prems(2))
   hence "swapidseq_ext (insert c (insert d (insert a (insert b S')))) (Suc (Suc n))
-                 ((Fun.swap c d id) \<circ> p' \<circ> (Fun.swap a b id))"
+                 (transpose c d \<circ> p' \<circ> (transpose a b))"
     by (metis cd fun.map_comp swapidseq_ext.comp)
   thus ?case
     by (metis S(1) p insert_commute) 
@@ -315,11 +315,11 @@
         and p: "p = q \<circ> r" and S: "U \<union> V = S"
       by blast
     obtain a b r' V' 
-      where "a \<noteq> b" and r': "V = (insert a (insert b V'))" "swapidseq_ext V' m r'" "r = (Fun.swap a b id) \<circ> r'"
+      where "a \<noteq> b" and r': "V = (insert a (insert b V'))" "swapidseq_ext V' m r'" "r = (transpose a b) \<circ> r'"
       using swapidseq_ext_backwards[OF r] by blast
-    have "swapidseq_ext (insert a (insert b U)) (n - m) (q \<circ> (Fun.swap a b id))"
+    have "swapidseq_ext (insert a (insert b U)) (n - m) (q \<circ> (transpose a b))"
       using swapidseq_ext_endswap[OF q \<open>a \<noteq> b\<close>] step(2) by (metis Suc_diff_Suc)
-    hence "?split m (q \<circ> (Fun.swap a b id)) r' (insert a (insert b U)) V'"
+    hence "?split m (q \<circ> (transpose a b)) r' (insert a (insert b U)) V'"
       using r' S unfolding p by fastforce 
     thus ?case by blast
   qed
@@ -350,7 +350,7 @@
     by auto
   obtain a b c where cs_def: "cs = [ a, b, c ]"
     using stupid_lemma[OF cs(3)] by auto
-  have "swapidseq (Suc (Suc 0)) ((Fun.swap a b id) \<circ> (Fun.swap b c id))"
+  have "swapidseq (Suc (Suc 0)) ((transpose a b) \<circ> (Fun.swap b c id))"
     using comp_Suc[OF comp_Suc[OF id], of b c a b] cs(2) unfolding cs_def by simp
   hence "evenperm p"
     using cs(1) unfolding cs_def by (simp add: evenperm_unique)
@@ -395,10 +395,10 @@
         have "q \<in> generate (alt_group n) (three_cycles n)"
         proof -
           obtain a b q' where ab: "a \<noteq> b" "a \<in> S" "b \<in> S"
-            and q': "swapidseq_ext S (Suc 0) q'" "q = (Fun.swap a b id) \<circ> q'"
+            and q': "swapidseq_ext S (Suc 0) q'" "q = (transpose a b) \<circ> q'"
             using swapidseq_ext_backwards'[OF seq] by auto 
           obtain c d where cd: "c \<noteq> d" "c \<in> S" "d \<in> S"
-            and q: "q = (Fun.swap a b id) \<circ> (Fun.swap c d id)"
+            and q: "q = (transpose a b) \<circ> (Fun.swap c d id)"
             using swapidseq_ext_backwards'[OF q'(1)]
                   swapidseq_ext_zero_imp_id
             unfolding q'(2)
@@ -416,7 +416,7 @@
           next
             case ineq
             hence "q = cycle_of_list [ a, b, c ] \<circ> cycle_of_list [ b, c, d ]"
-              unfolding q by (simp add: comp_swap)
+              unfolding q by (simp add: swap_nilpotent o_assoc)
             moreover have "{ a, b, c } \<subseteq> {1..n}" and "{ b, c, d } \<subseteq> {1..n}"
               using ab cd S by blast+
             ultimately show ?thesis
@@ -499,7 +499,7 @@
         unfolding sym[OF cs(1)] unfolding cs_def by simp
       also have " ... = p \<circ> p"
         using cs(2) unfolding cs(1) cs_def
-        by (auto, metis comp_id comp_swap swap_commute swap_triple)
+        by (simp add: comp_swap swap_commute transpose_comp_triple) 
       finally have "q \<circ> p \<circ> (inv' q) = p \<circ> p" .
       moreover have "bij p"
         unfolding cs(1) cs_def by (simp add: bij_comp)
diff -r a037f01aedab -r 1bd3463e30b8 src/HOL/Analysis/Brouwer_Fixpoint.thy
--- a/src/HOL/Analysis/Brouwer_Fixpoint.thy	Fri May 07 16:49:08 2021 +0200
+++ b/src/HOL/Analysis/Brouwer_Fixpoint.thy	Sun May 09 05:48:50 2021 +0000
@@ -1114,9 +1114,14 @@
       moreover have "j < i \<or> i = j \<or> i < j" by arith
       moreover note i
       ultimately have "enum j = b.enum j \<longleftrightarrow> j \<noteq> i"
-        unfolding enum_def[abs_def] b.enum_def[abs_def]
-        by (auto simp: fun_eq_iff swap_image i'_def
-                           in_upd_image inj_on_image_set_diff[OF inj_upd]) }
+        apply (simp only: fun_eq_iff enum_def b.enum_def flip: image_comp)
+        apply (cases \<open>i = j\<close>)
+         apply simp
+         apply (metis Suc_i' \<open>i \<le> n\<close> imageI in_upd_image lessI lessThan_iff lessThan_subset_iff less_irrefl_nat transpose_apply_second transpose_commute)
+        apply (subst transpose_image_eq)
+         apply (auto simp add: i'_def)
+        done
+      }
     note enum_eq_benum = this
     then have "enum ` ({.. n} - {i}) = b.enum ` ({.. n} - {i})"
       by (intro image_cong) auto
diff -r a037f01aedab -r 1bd3463e30b8 src/HOL/Analysis/Cartesian_Space.thy
--- a/src/HOL/Analysis/Cartesian_Space.thy	Fri May 07 16:49:08 2021 +0200
+++ b/src/HOL/Analysis/Cartesian_Space.thy	Sun May 09 05:48:50 2021 +0000
@@ -10,7 +10,9 @@
 
 theory Cartesian_Space
   imports
-    Finite_Cartesian_Product Linear_Algebra "HOL-Combinatorics.Transposition"
+    "HOL-Combinatorics.Transposition"
+    Finite_Cartesian_Product
+    Linear_Algebra
 begin
 
 subsection\<^marker>\<open>tag unimportant\<close> \<open>Type @{typ \<open>'a ^ 'n\<close>} and fields as vector spaces\<close> (*much of the following
@@ -1061,7 +1063,7 @@
   then obtain f0 where "bij_betw f0 (UNIV::'n set) S"
     by (metis finite_class.finite_UNIV finite_same_card_bij finiteI_independent)
   then obtain f where f: "bij_betw f (UNIV::'n set) S" and a: "a = f k"
-    using bij_swap_iff [of k "inv f0 a" f0]
+    using bij_swap_iff [of f0 k "inv f0 a"]
     by (metis UNIV_I \<open>a \<in> S\<close> bij_betw_inv_into_right bij_betw_swap_iff swap_apply(1))
   show thesis
   proof
@@ -1206,7 +1208,7 @@
   fixes P :: "real^'n^'n \<Rightarrow> bool"
   assumes zero_row: "\<And>A i. row i A = 0 \<Longrightarrow> P A"
     and diagonal: "\<And>A. (\<And>i j. i \<noteq> j \<Longrightarrow> A$i$j = 0) \<Longrightarrow> P A"
-    and swap_cols: "\<And>A m n. \<lbrakk>P A; m \<noteq> n\<rbrakk> \<Longrightarrow> P(\<chi> i j. A $ i $ Fun.swap m n id j)"
+    and swap_cols: "\<And>A m n. \<lbrakk>P A; m \<noteq> n\<rbrakk> \<Longrightarrow> P(\<chi> i j. A $ i $ Transposition.transpose m n j)"
     and row_op: "\<And>A m n c. \<lbrakk>P A; m \<noteq> n\<rbrakk>
                    \<Longrightarrow> P(\<chi> i. if i = m then row m A + c *\<^sub>R row n A else row i A)"
   shows "P A"
@@ -1293,14 +1295,14 @@
             by blast
         next
           case False
-          have *: "A $ i $ Fun.swap k l id j = 0" if "j \<noteq> k" "j \<notin> K" "i \<noteq> j" for i j
+          have *: "A $ i $ Transposition.transpose k l j = 0" if "j \<noteq> k" "j \<notin> K" "i \<noteq> j" for i j
             using False l insert.prems that
-            by (auto simp: swap_id_eq insert split: if_split_asm)
-          have "P (\<chi> i j. (\<chi> i j. A $ i $ Fun.swap k l id j) $ i $ Fun.swap k l id j)"
+            by (auto simp add: Transposition.transpose_def)
+          have "P (\<chi> i j. (\<chi> i j. A $ i $ Transposition.transpose k l j) $ i $ Transposition.transpose k l j)"
             by (rule swap_cols [OF nonzero_hyp False]) (auto simp: l *)
           moreover
-          have "(\<chi> i j. (\<chi> i j. A $ i $ Fun.swap k l id j) $ i $ Fun.swap k l id j) = A"
-            by (vector Fun.swap_def)
+          have "(\<chi> i j. (\<chi> i j. A $ i $ Transposition.transpose k l j) $ i $ Transposition.transpose k l j) = A"
+            by simp
           ultimately show ?thesis
             by simp
         qed
@@ -1316,14 +1318,14 @@
   assumes mult: "\<And>A B. \<lbrakk>P A; P B\<rbrakk> \<Longrightarrow> P(A ** B)"
     and zero_row: "\<And>A i. row i A = 0 \<Longrightarrow> P A"
     and diagonal: "\<And>A. (\<And>i j. i \<noteq> j \<Longrightarrow> A$i$j = 0) \<Longrightarrow> P A"
-    and swap1: "\<And>m n. m \<noteq> n \<Longrightarrow> P(\<chi> i j. mat 1 $ i $ Fun.swap m n id j)"
+    and swap1: "\<And>m n. m \<noteq> n \<Longrightarrow> P(\<chi> i j. mat 1 $ i $ Transposition.transpose m n j)"
     and idplus: "\<And>m n c. m \<noteq> n \<Longrightarrow> P(\<chi> i j. if i = m \<and> j = n then c else of_bool (i = j))"
   shows "P A"
 proof -
-  have swap: "P (\<chi> i j. A $ i $ Fun.swap m n id j)"  (is "P ?C")
+  have swap: "P (\<chi> i j. A $ i $ Transposition.transpose m n j)"  (is "P ?C")
     if "P A" "m \<noteq> n" for A m n
   proof -
-    have "A ** (\<chi> i j. mat 1 $ i $ Fun.swap m n id j) = ?C"
+    have "A ** (\<chi> i j. mat 1 $ i $ Transposition.transpose m n j) = ?C"
       by (simp add: matrix_matrix_mult_def mat_def vec_eq_iff if_distrib sum.delta_remove)
     then show ?thesis
       using mult swap1 that by metis
@@ -1347,7 +1349,7 @@
   assumes mult: "\<And>A B. \<lbrakk>P A; P B\<rbrakk> \<Longrightarrow> P(A ** B)"
     and zero_row: "\<And>A i. row i A = 0 \<Longrightarrow> P A"
     and diagonal: "\<And>A. (\<And>i j. i \<noteq> j \<Longrightarrow> A$i$j = 0) \<Longrightarrow> P A"
-    and swap1: "\<And>m n. m \<noteq> n \<Longrightarrow> P(\<chi> i j. mat 1 $ i $ Fun.swap m n id j)"
+    and swap1: "\<And>m n. m \<noteq> n \<Longrightarrow> P(\<chi> i j. mat 1 $ i $ Transposition.transpose m n j)"
     and idplus: "\<And>m n. m \<noteq> n \<Longrightarrow> P(\<chi> i j. of_bool (i = m \<and> j = n \<or> i = j))"
   shows "P A"
 proof -
@@ -1386,7 +1388,7 @@
     and comp: "\<And>f g. \<lbrakk>linear f; linear g; P f; P g\<rbrakk> \<Longrightarrow> P(f \<circ> g)"
     and zeroes: "\<And>f i. \<lbrakk>linear f; \<And>x. (f x) $ i = 0\<rbrakk> \<Longrightarrow> P f"
     and const: "\<And>c. P(\<lambda>x. \<chi> i. c i * x$i)"
-    and swap: "\<And>m n::'n. m \<noteq> n \<Longrightarrow> P(\<lambda>x. \<chi> i. x $ Fun.swap m n id i)"
+    and swap: "\<And>m n::'n. m \<noteq> n \<Longrightarrow> P(\<lambda>x. \<chi> i. x $ Transposition.transpose m n i)"
     and idplus: "\<And>m n::'n. m \<noteq> n \<Longrightarrow> P(\<lambda>x. \<chi> i. if i = m then x$m + x$n else x$i)"
   shows "P f"
 proof -
@@ -1415,13 +1417,13 @@
   next
     fix m n :: "'n"
     assume "m \<noteq> n"
-    have eq: "(\<Sum>j\<in>UNIV. if i = Fun.swap m n id j then x $ j else 0) =
-              (\<Sum>j\<in>UNIV. if j = Fun.swap m n id i then x $ j else 0)"
+    have eq: "(\<Sum>j\<in>UNIV. if i = Transposition.transpose m n j then x $ j else 0) =
+              (\<Sum>j\<in>UNIV. if j = Transposition.transpose m n i then x $ j else 0)"
       for i and x :: "real^'n"
       by (rule sum.cong) (auto simp add: swap_id_eq)
-    have "(\<lambda>x::real^'n. \<chi> i. x $ Fun.swap m n id i) = ((*v) (\<chi> i j. if i = Fun.swap m n id j then 1 else 0))"
+    have "(\<lambda>x::real^'n. \<chi> i. x $ Transposition.transpose m n i) = ((*v) (\<chi> i j. if i = Transposition.transpose m n j then 1 else 0))"
       by (auto simp: mat_def matrix_vector_mult_def eq if_distrib [of "\<lambda>x. x * y" for y] cong: if_cong)
-    with swap [OF \<open>m \<noteq> n\<close>] show "P ((*v) (\<chi> i j. mat 1 $ i $ Fun.swap m n id j))"
+    with swap [OF \<open>m \<noteq> n\<close>] show "P ((*v) (\<chi> i j. mat 1 $ i $ Transposition.transpose m n j))"
       by (simp add: mat_def matrix_vector_mult_def)
   next
     fix m n :: "'n"
diff -r a037f01aedab -r 1bd3463e30b8 src/HOL/Analysis/Change_Of_Vars.thy
--- a/src/HOL/Analysis/Change_Of_Vars.thy	Fri May 07 16:49:08 2021 +0200
+++ b/src/HOL/Analysis/Change_Of_Vars.thy	Sun May 09 05:48:50 2021 +0000
@@ -272,10 +272,10 @@
   next
     fix m :: "'n" and n :: "'n" and S :: "(real, 'n) vec set"
     assume "m \<noteq> n" and "S \<in> lmeasurable"
-    let ?h = "\<lambda>v::(real, 'n) vec. \<chi> i. v $ Fun.swap m n id i"
+    let ?h = "\<lambda>v::(real, 'n) vec. \<chi> i. v $ Transposition.transpose m n i"
     have lin: "linear ?h"
       by (rule linearI) (simp_all add: plus_vec_def scaleR_vec_def)
-    have meq: "measure lebesgue ((\<lambda>v::(real, 'n) vec. \<chi> i. v $ Fun.swap m n id i) ` cbox a b)
+    have meq: "measure lebesgue ((\<lambda>v::(real, 'n) vec. \<chi> i. v $ Transposition.transpose m n i) ` cbox a b)
              = measure lebesgue (cbox a b)" for a b
     proof (cases "cbox a b = {}")
       case True then show ?thesis
@@ -285,14 +285,14 @@
       then have him: "?h ` (cbox a b) \<noteq> {}"
         by blast
       have eq: "?h ` (cbox a b) = cbox (?h a) (?h b)"
-        by (auto simp: image_iff lambda_swap_Galois mem_box_cart) (metis swap_id_eq)+
+        by (auto simp: image_iff lambda_swap_Galois mem_box_cart) (metis transpose_involutory)+
       show ?thesis
         using him prod.permute [OF permutes_swap_id, where S=UNIV and g="\<lambda>i. (b - a)$i", symmetric]
         by (simp add: eq content_cbox_cart False)
     qed
-    have "(\<chi> i j. if Fun.swap m n id i = j then 1 else 0) = (\<chi> i j. if j = Fun.swap m n id i then 1 else (0::real))"
+    have "(\<chi> i j. if Transposition.transpose m n i = j then 1 else 0) = (\<chi> i j. if j = Transposition.transpose m n i then 1 else (0::real))"
       by (auto intro!: Cart_lambda_cong)
-    then have "matrix ?h = transpose(\<chi> i j. mat 1 $ i $ Fun.swap m n id j)"
+    then have "matrix ?h = transpose(\<chi> i j. mat 1 $ i $ Transposition.transpose m n j)"
       by (auto simp: matrix_eq transpose_def axis_def mat_def matrix_def)
     then have 1: "\<bar>det (matrix ?h)\<bar> = 1"
       by (simp add: det_permute_columns permutes_swap_id sign_swap_id abs_mult)
diff -r a037f01aedab -r 1bd3463e30b8 src/HOL/Analysis/Determinants.thy
--- a/src/HOL/Analysis/Determinants.thy	Fri May 07 16:49:08 2021 +0200
+++ b/src/HOL/Analysis/Determinants.thy	Sun May 09 05:48:50 2021 +0000
@@ -227,7 +227,7 @@
   shows "det A = 0"
 proof -
   let ?U="UNIV::'n set"
-  let ?t_jk="Fun.swap j k id"
+  let ?t_jk="Transposition.transpose j k"
   let ?PU="{p. p permutes ?U}"
   let ?S1="{p. p\<in>?PU \<and> evenperm p}"
   let ?S2="{(?t_jk \<circ> p) |p. p \<in>?S1}"
@@ -240,10 +240,11 @@
       and y: "y permutes ?U" and even_y: "evenperm y" and eq: "?t_jk \<circ> x = ?t_jk \<circ> y"
     show "x = y" by (metis (hide_lams, no_types) comp_assoc eq id_comp swap_id_idempotent)
   qed
-  have tjk_permutes: "?t_jk permutes ?U" unfolding permutes_def swap_id_eq by (auto,metis)
+  have tjk_permutes: "?t_jk permutes ?U"
+    by (auto simp add: permutes_def dest: transpose_eq_imp_eq) (meson transpose_involutory)
   have tjk_eq: "\<forall>i l. A $ i $ ?t_jk l  =  A $ i $ l"
     using r jk
-    unfolding column_def vec_eq_iff swap_id_eq by fastforce
+    unfolding column_def vec_eq_iff by (simp add: Transposition.transpose_def) 
   have sign_tjk: "sign ?t_jk = -1" using sign_swap_id[of j k] jk by auto
   {fix x
     assume x: "x\<in> ?S1"
@@ -260,8 +261,8 @@
   have PU_decomposition: "?PU = ?S1 \<union> ?S2"
   proof (auto)
     fix x
-    assume x: "x permutes ?U" and "\<forall>p. p permutes ?U \<longrightarrow> x = Fun.swap j k id \<circ> p \<longrightarrow> \<not> evenperm p"
-    then obtain p where p: "p permutes UNIV" and x_eq: "x = Fun.swap j k id \<circ> p"
+    assume x: "x permutes ?U" and "\<forall>p. p permutes ?U \<longrightarrow> x = Transposition.transpose j k \<circ> p \<longrightarrow> \<not> evenperm p"
+    then obtain p where p: "p permutes UNIV" and x_eq: "x = Transposition.transpose j k \<circ> p"
       and odd_p: "\<not> evenperm p"
       by (metis (mono_tags) id_o o_assoc permutes_compose swap_id_idempotent tjk_permutes)
     thus "evenperm x"
@@ -269,10 +270,10 @@
           jk permutation_permutes permutation_swap_id)
   next
     fix p assume p: "p permutes ?U"
-    show "Fun.swap j k id \<circ> p permutes UNIV" by (metis p permutes_compose tjk_permutes)
+    show "Transposition.transpose j k \<circ> p permutes UNIV" by (metis p permutes_compose tjk_permutes)
   qed
   have "sum ?f ?S2 = sum ((\<lambda>p. of_int (sign p) * (\<Prod>i\<in>UNIV. A $ i $ p i))
-  \<circ> (\<circ>) (Fun.swap j k id)) {p \<in> {p. p permutes UNIV}. evenperm p}"
+  \<circ> (\<circ>) (Transposition.transpose j k)) {p \<in> {p. p permutes UNIV}. evenperm p}"
     unfolding g_S1 by (rule sum.reindex[OF inj_g])
   also have "\<dots> = sum (\<lambda>p. of_int (sign (?t_jk \<circ> p)) * (\<Prod>i\<in>UNIV. A $ i $ p i)) ?S1"
     unfolding o_def by (rule sum.cong, auto simp: tjk_eq)
diff -r a037f01aedab -r 1bd3463e30b8 src/HOL/Analysis/Linear_Algebra.thy
--- a/src/HOL/Analysis/Linear_Algebra.thy	Fri May 07 16:49:08 2021 +0200
+++ b/src/HOL/Analysis/Linear_Algebra.thy	Sun May 09 05:48:50 2021 +0000
@@ -1875,5 +1875,4 @@
   shows "continuous_on S (\<lambda>x. h (f x) (g x))"
   using assms by (simp add: continuous_on_eq_continuous_within bilinear_continuous_compose)
 
-
 end
diff -r a037f01aedab -r 1bd3463e30b8 src/HOL/Analysis/Vitali_Covering_Theorem.thy
--- a/src/HOL/Analysis/Vitali_Covering_Theorem.thy	Fri May 07 16:49:08 2021 +0200
+++ b/src/HOL/Analysis/Vitali_Covering_Theorem.thy	Sun May 09 05:48:50 2021 +0000
@@ -16,7 +16,7 @@
   by auto
 
 lemma lambda_swap_Galois:
-   "(x = (\<chi> i. y $ Fun.swap m n id i) \<longleftrightarrow> (\<chi> i. x $ Fun.swap m n id i) = y)"
+   "(x = (\<chi> i. y $ Transposition.transpose m n i) \<longleftrightarrow> (\<chi> i. x $ Transposition.transpose m n i) = y)"
   by (auto; simp add: pointfree_idE vec_eq_iff)
 
 lemma lambda_add_Galois:
diff -r a037f01aedab -r 1bd3463e30b8 src/HOL/Combinatorics/Combinatorics.thy
--- a/src/HOL/Combinatorics/Combinatorics.thy	Fri May 07 16:49:08 2021 +0200
+++ b/src/HOL/Combinatorics/Combinatorics.thy	Sun May 09 05:48:50 2021 +0000
@@ -10,6 +10,7 @@
   Multiset_Permutations
   Cycles
   Perm
+  Orbits
 begin
 
 end
diff -r a037f01aedab -r 1bd3463e30b8 src/HOL/Combinatorics/Cycles.thy
--- a/src/HOL/Combinatorics/Cycles.thy	Fri May 07 16:49:08 2021 +0200
+++ b/src/HOL/Combinatorics/Cycles.thy	Sun May 09 05:48:50 2021 +0000
@@ -2,7 +2,9 @@
 *)
 
 theory Cycles
-  imports "HOL-Library.FuncSet" Permutations
+  imports
+    "HOL-Library.FuncSet"
+Permutations
 begin
 
 section \<open>Cycles\<close>
@@ -14,7 +16,7 @@
 
 fun cycle_of_list :: "'a list \<Rightarrow> 'a \<Rightarrow> 'a"
   where
-    "cycle_of_list (i # j # cs) = (Fun.swap i j id) \<circ> (cycle_of_list (j # cs))"
+    "cycle_of_list (i # j # cs) = transpose i j \<circ> cycle_of_list (j # cs)"
   | "cycle_of_list cs = id"
 
 
@@ -118,12 +120,12 @@
   have "p \<circ> cycle_of_list (i # j # cs) \<circ> inv p =
        (p \<circ> (Fun.swap i j id) \<circ> inv p) \<circ> (p \<circ> cycle_of_list (j # cs) \<circ> inv p)"
     by (simp add: assms(2) bij_is_inj fun.map_comp)
-  also have " ... = (Fun.swap (p i) (p j) id) \<circ> (p \<circ> cycle_of_list (j # cs) \<circ> inv p)"
-    by (simp add: "1.prems"(2) bij_is_inj bij_swap_comp comp_swap o_assoc)
+  also have " ... = (transpose (p i) (p j)) \<circ> (p \<circ> cycle_of_list (j # cs) \<circ> inv p)"
+    using "1.prems"(2) by (simp add: bij_inv_eq_iff transpose_apply_commute fun_eq_iff bij_betw_inv_into_left)
   finally have "p \<circ> cycle_of_list (i # j # cs) \<circ> inv p =
-               (Fun.swap (p i) (p j) id) \<circ> (cycle_of_list (map p (j # cs)))"
+               (transpose (p i) (p j)) \<circ> (cycle_of_list (map p (j # cs)))"
     using "1.IH" "1.prems"(1) assms(2) by fastforce
-  thus ?case by (metis cycle_of_list.simps(1) list.simps(9))
+  thus ?case by (simp add: fun_eq_iff)
 next
   case "2_1" thus ?case
     by (metis bij_is_surj comp_id cycle_of_list.simps(2) list.simps(8) surj_iff) 
diff -r a037f01aedab -r 1bd3463e30b8 src/HOL/Combinatorics/Perm.thy
--- a/src/HOL/Combinatorics/Perm.thy	Fri May 07 16:49:08 2021 +0200
+++ b/src/HOL/Combinatorics/Perm.thy	Sun May 09 05:48:50 2021 +0000
@@ -732,12 +732,12 @@
 subsection \<open>Swaps\<close>
 
 lift_definition swap :: "'a \<Rightarrow> 'a \<Rightarrow> 'a perm"  ("\<langle>_ \<leftrightarrow> _\<rangle>")
-  is "\<lambda>a b. Fun.swap a b id"
+  is "\<lambda>a b. transpose a b"
 proof
   fix a b :: 'a
-  have "{c. Fun.swap a b id c \<noteq> c} \<subseteq> {a, b}"
-    by (auto simp add: Fun.swap_def)
-  then show "finite {c. Fun.swap a b id c \<noteq> c}"
+  have "{c. transpose a b c \<noteq> c} \<subseteq> {a, b}"
+    by (auto simp add: transpose_def)
+  then show "finite {c. transpose a b c \<noteq> c}"
     by (rule finite_subset) simp
 qed simp
 
@@ -753,7 +753,7 @@
 lemma apply_swap_eq_iff [simp]:
   "\<langle>a \<leftrightarrow> b\<rangle> \<langle>$\<rangle> c = a \<longleftrightarrow> c = b"
   "\<langle>a \<leftrightarrow> b\<rangle> \<langle>$\<rangle> c = b \<longleftrightarrow> c = a"
-  by (transfer; auto simp add: Fun.swap_def)+
+  by (transfer; auto simp add: transpose_def)+
 
 lemma swap_1 [simp]:
   "\<langle>a \<leftrightarrow> a\<rangle> = 1"
@@ -761,19 +761,19 @@
 
 lemma swap_sym:
   "\<langle>b \<leftrightarrow> a\<rangle> = \<langle>a \<leftrightarrow> b\<rangle>"
-  by (transfer; auto simp add: Fun.swap_def)+
+  by (transfer; auto simp add: transpose_def)+
 
 lemma swap_self [simp]:
   "\<langle>a \<leftrightarrow> b\<rangle> * \<langle>a \<leftrightarrow> b\<rangle> = 1"
-  by transfer (simp add: Fun.swap_def fun_eq_iff)
+  by transfer simp
 
 lemma affected_swap:
   "a \<noteq> b \<Longrightarrow> affected \<langle>a \<leftrightarrow> b\<rangle> = {a, b}"
-  by transfer (auto simp add: Fun.swap_def)
+  by transfer (auto simp add: transpose_def)
 
 lemma inverse_swap [simp]:
   "inverse \<langle>a \<leftrightarrow> b\<rangle> = \<langle>a \<leftrightarrow> b\<rangle>"
-  by transfer (auto intro: inv_equality simp: Fun.swap_def)
+  by transfer (auto intro: inv_equality)
 
 
 subsection \<open>Permutations specified by cycles\<close>
diff -r a037f01aedab -r 1bd3463e30b8 src/HOL/Combinatorics/Permutations.thy
--- a/src/HOL/Combinatorics/Permutations.thy	Fri May 07 16:49:08 2021 +0200
+++ b/src/HOL/Combinatorics/Permutations.thy	Sun May 09 05:48:50 2021 +0000
@@ -181,8 +181,8 @@
 lemma permutes_univ: "p permutes UNIV \<longleftrightarrow> (\<forall>y. \<exists>!x. p x = y)"
   by (simp add: permutes_def)
 
-lemma permutes_swap_id: "a \<in> S \<Longrightarrow> b \<in> S \<Longrightarrow> Fun.swap a b id permutes S"
-  by (rule bij_imp_permutes) (auto simp add: swap_id_eq)
+lemma permutes_swap_id: "a \<in> S \<Longrightarrow> b \<in> S \<Longrightarrow> transpose a b permutes S"
+  by (rule bij_imp_permutes) (auto intro: transpose_apply_other)
 
 lemma permutes_superset:
   \<open>p permutes T\<close> if \<open>p permutes S\<close> \<open>\<And>x. x \<in> S - T \<Longrightarrow> p x = x\<close>
@@ -376,7 +376,7 @@
 
 lemma permutes_insert_lemma:
   assumes "p permutes (insert a S)"
-  shows "Fun.swap a (p a) id \<circ> p permutes S"
+  shows "transpose a (p a) \<circ> p permutes S"
   apply (rule permutes_superset[where S = "insert a S"])
   apply (rule permutes_compose[OF assms])
   apply (rule permutes_swap_id, simp)
@@ -386,25 +386,25 @@
   done
 
 lemma permutes_insert: "{p. p permutes (insert a S)} =
-  (\<lambda>(b, p). Fun.swap a b id \<circ> p) ` {(b, p). b \<in> insert a S \<and> p \<in> {p. p permutes S}}"
+  (\<lambda>(b, p). transpose a b \<circ> p) ` {(b, p). b \<in> insert a S \<and> p \<in> {p. p permutes S}}"
 proof -
   have "p permutes insert a S \<longleftrightarrow>
-    (\<exists>b q. p = Fun.swap a b id \<circ> q \<and> b \<in> insert a S \<and> q permutes S)" for p
+    (\<exists>b q. p = transpose a b \<circ> q \<and> b \<in> insert a S \<and> q permutes S)" for p
   proof -
-    have "\<exists>b q. p = Fun.swap a b id \<circ> q \<and> b \<in> insert a S \<and> q permutes S"
+    have "\<exists>b q. p = transpose a b \<circ> q \<and> b \<in> insert a S \<and> q permutes S"
       if p: "p permutes insert a S"
     proof -
       let ?b = "p a"
-      let ?q = "Fun.swap a (p a) id \<circ> p"
-      have *: "p = Fun.swap a ?b id \<circ> ?q"
+      let ?q = "transpose a (p a) \<circ> p"
+      have *: "p = transpose a ?b \<circ> ?q"
         by (simp add: fun_eq_iff o_assoc)
       have **: "?b \<in> insert a S"
         unfolding permutes_in_image[OF p] by simp
       from permutes_insert_lemma[OF p] * ** show ?thesis
-       by blast
+        by blast
     qed
     moreover have "p permutes insert a S"
-      if bq: "p = Fun.swap a b id \<circ> q" "b \<in> insert a S" "q permutes S" for b q
+      if bq: "p = transpose a b \<circ> q" "b \<in> insert a S" "q permutes S" for b q
     proof -
       from permutes_subset[OF bq(3), of "insert a S"] have q: "q permutes insert a S"
         by auto
@@ -434,7 +434,7 @@
     let ?xF = "{p. p permutes insert x F}"
     let ?pF = "{p. p permutes F}"
     let ?pF' = "{(b, p). b \<in> insert x F \<and> p \<in> ?pF}"
-    let ?g = "(\<lambda>(b, p). Fun.swap x b id \<circ> p)"
+    let ?g = "(\<lambda>(b, p). transpose x b \<circ> p)"
     have xfgpF': "?xF = ?g ` ?pF'"
       by (rule permutes_insert[of x F])
     from \<open>x \<notin> F\<close> \<open>finite F\<close> card_insert have Fs: "card F = n - 1"
@@ -508,15 +508,15 @@
 lemma permutes_induct [consumes 2, case_names id swap]:
   \<open>P p\<close> if \<open>p permutes S\<close> \<open>finite S\<close>
   and id: \<open>P id\<close>
-  and swap: \<open>\<And>a b p. a \<in> S \<Longrightarrow> b \<in> S \<Longrightarrow> p permutes S \<Longrightarrow> P p \<Longrightarrow> P (Fun.swap a b id \<circ> p)\<close>
+  and swap: \<open>\<And>a b p. a \<in> S \<Longrightarrow> b \<in> S \<Longrightarrow> p permutes S \<Longrightarrow> P p \<Longrightarrow> P (transpose a b \<circ> p)\<close>
 using \<open>finite S\<close> \<open>p permutes S\<close> swap proof (induction S arbitrary: p)
   case empty
   with id show ?case
     by (simp only: permutes_empty)
 next
   case (insert x S p)
-  define q where \<open>q = Fun.swap x (p x) id \<circ> p\<close>
-  then have swap_q: \<open>Fun.swap x (p x) id \<circ> q = p\<close>
+  define q where \<open>q = transpose x (p x) \<circ> p\<close>
+  then have swap_q: \<open>transpose x (p x) \<circ> q = p\<close>
     by (simp add: o_assoc)
   from \<open>p permutes insert x S\<close> have \<open>q permutes S\<close>
     by (simp add: q_def permutes_insert_lemma)
@@ -528,7 +528,7 @@
     by simp
   moreover from \<open>p permutes insert x S\<close> have \<open>p x \<in> insert x S\<close>
     using permutes_in_image [of p \<open>insert x S\<close> x] by simp
-  ultimately have \<open>P (Fun.swap x (p x) id \<circ> q)\<close>
+  ultimately have \<open>P (transpose x (p x) \<circ> q)\<close>
     using \<open>q permutes insert x S\<close> \<open>P q\<close>
     by (rule insert.prems(2))
   then show ?case
@@ -538,16 +538,18 @@
 lemma permutes_rev_induct [consumes 2, case_names id swap]:
   \<open>P p\<close> if \<open>p permutes S\<close> \<open>finite S\<close>
   and id': \<open>P id\<close>
-  and swap': \<open>\<And>a b p. a \<in> S \<Longrightarrow> b \<in> S \<Longrightarrow> p permutes S \<Longrightarrow> P p \<Longrightarrow> P (Fun.swap a b p)\<close>
+  and swap': \<open>\<And>a b p. a \<in> S \<Longrightarrow> b \<in> S \<Longrightarrow> p permutes S \<Longrightarrow> P p \<Longrightarrow> P (p \<circ> transpose a b)\<close>
 using \<open>p permutes S\<close> \<open>finite S\<close> proof (induction rule: permutes_induct)
   case id
   from id' show ?case .
 next
   case (swap a b p)
+  then have \<open>bij p\<close>
+    using permutes_bij by blast 
   have \<open>P (Fun.swap (inv p a) (inv p b) p)\<close>
     by (rule swap') (auto simp add: swap permutes_in_image permutes_inv)
-  also have \<open>Fun.swap (inv p a) (inv p b) p = Fun.swap a b id \<circ> p\<close>
-    by (rule bij_swap_comp [symmetric]) (rule permutes_bij, rule swap)
+  also have \<open>Fun.swap (inv p a) (inv p b) p = transpose a b \<circ> p\<close>
+    using \<open>bij p\<close> by (rule transpose_comp_eq [symmetric])
   finally show ?case .
 qed
 
@@ -576,7 +578,7 @@
 inductive swapidseq :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> bool"
   where
     id[simp]: "swapidseq 0 id"
-  | comp_Suc: "swapidseq n p \<Longrightarrow> a \<noteq> b \<Longrightarrow> swapidseq (Suc n) (Fun.swap a b id \<circ> p)"
+  | comp_Suc: "swapidseq n p \<Longrightarrow> a \<noteq> b \<Longrightarrow> swapidseq (Suc n) (transpose a b \<circ> p)"
 
 declare id[unfolded id_def, simp]
 
@@ -590,13 +592,13 @@
 
 declare permutation_id[unfolded id_def, simp]
 
-lemma swapidseq_swap: "swapidseq (if a = b then 0 else 1) (Fun.swap a b id)"
+lemma swapidseq_swap: "swapidseq (if a = b then 0 else 1) (transpose a b)"
   apply clarsimp
   using comp_Suc[of 0 id a b]
   apply simp
   done
 
-lemma permutation_swap_id: "permutation (Fun.swap a b id)"
+lemma permutation_swap_id: "permutation (transpose a b)"
 proof (cases "a = b")
   case True
   then show ?thesis by simp
@@ -627,7 +629,7 @@
 lemma permutation_compose: "permutation p \<Longrightarrow> permutation q \<Longrightarrow> permutation (p \<circ> q)"
   unfolding permutation_def using swapidseq_comp_add[of _ p _ q] by metis
 
-lemma swapidseq_endswap: "swapidseq n p \<Longrightarrow> a \<noteq> b \<Longrightarrow> swapidseq (Suc n) (p \<circ> Fun.swap a b id)"
+lemma swapidseq_endswap: "swapidseq n p \<Longrightarrow> a \<noteq> b \<Longrightarrow> swapidseq (Suc n) (p \<circ> transpose a b)"
   by (induct n p rule: swapidseq.induct)
     (use swapidseq_swap[of a b] in \<open>auto simp add: comp_assoc intro: swapidseq.comp_Suc\<close>)
 
@@ -640,20 +642,20 @@
   case (comp_Suc n p a b)
   from comp_Suc.hyps obtain q where q: "swapidseq n q" "p \<circ> q = id" "q \<circ> p = id"
     by blast
-  let ?q = "q \<circ> Fun.swap a b id"
+  let ?q = "q \<circ> transpose a b"
   note H = comp_Suc.hyps
-  from swapidseq_swap[of a b] H(3) have *: "swapidseq 1 (Fun.swap a b id)"
+  from swapidseq_swap[of a b] H(3) have *: "swapidseq 1 (transpose a b)"
     by simp
   from swapidseq_comp_add[OF q(1) *] have **: "swapidseq (Suc n) ?q"
     by simp
-  have "Fun.swap a b id \<circ> p \<circ> ?q = Fun.swap a b id \<circ> (p \<circ> q) \<circ> Fun.swap a b id"
+  have "transpose a b \<circ> p \<circ> ?q = transpose a b \<circ> (p \<circ> q) \<circ> transpose a b"
     by (simp add: o_assoc)
   also have "\<dots> = id"
     by (simp add: q(2))
-  finally have ***: "Fun.swap a b id \<circ> p \<circ> ?q = id" .
-  have "?q \<circ> (Fun.swap a b id \<circ> p) = q \<circ> (Fun.swap a b id \<circ> Fun.swap a b id) \<circ> p"
+  finally have ***: "transpose a b \<circ> p \<circ> ?q = id" .
+  have "?q \<circ> (transpose a b \<circ> p) = q \<circ> (transpose a b \<circ> transpose a b) \<circ> p"
     by (simp only: o_assoc)
-  then have "?q \<circ> (Fun.swap a b id \<circ> p) = id"
+  then have "?q \<circ> (transpose a b \<circ> p) = id"
     by (simp add: q(3))
   with ** *** show ?case
     by blast
@@ -672,15 +674,15 @@
 subsection \<open>Various combinations of transpositions with 2, 1 and 0 common elements\<close>
 
 lemma swap_id_common:" a \<noteq> c \<Longrightarrow> b \<noteq> c \<Longrightarrow>
-  Fun.swap a b id \<circ> Fun.swap a c id = Fun.swap b c id \<circ> Fun.swap a b id"
+  transpose a b \<circ> transpose a c = Fun.swap b c id \<circ> transpose a b"
   by (simp add: fun_eq_iff Fun.swap_def)
 
 lemma swap_id_common': "a \<noteq> b \<Longrightarrow> a \<noteq> c \<Longrightarrow>
-  Fun.swap a c id \<circ> Fun.swap b c id = Fun.swap b c id \<circ> Fun.swap a b id"
+  transpose a c \<circ> Fun.swap b c id = Fun.swap b c id \<circ> transpose a b"
   by (simp add: fun_eq_iff Fun.swap_def)
 
 lemma swap_id_independent: "a \<noteq> c \<Longrightarrow> a \<noteq> d \<Longrightarrow> b \<noteq> c \<Longrightarrow> b \<noteq> d \<Longrightarrow>
-  Fun.swap a b id \<circ> Fun.swap c d id = Fun.swap c d id \<circ> Fun.swap a b id"
+  transpose a b \<circ> transpose c d = transpose c d \<circ> transpose a b"
   by (simp add: fun_eq_iff Fun.swap_def)
 
 
@@ -695,36 +697,18 @@
   using assms by metis
 
 lemma swap_general: "a \<noteq> b \<Longrightarrow> c \<noteq> d \<Longrightarrow>
-  Fun.swap a b id \<circ> Fun.swap c d id = id \<or>
+  transpose a b \<circ> transpose c d = id \<or>
   (\<exists>x y z. x \<noteq> a \<and> y \<noteq> a \<and> z \<noteq> a \<and> x \<noteq> y \<and>
-    Fun.swap a b id \<circ> Fun.swap c d id = Fun.swap x y id \<circ> Fun.swap a z id)"
+    transpose a b \<circ> transpose c d = transpose x y \<circ> transpose a z)"
 proof -
   assume neq: "a \<noteq> b" "c \<noteq> d"
   have "a \<noteq> b \<longrightarrow> c \<noteq> d \<longrightarrow>
-    (Fun.swap a b id \<circ> Fun.swap c d id = id \<or>
+    (transpose a b \<circ> transpose c d = id \<or>
       (\<exists>x y z. x \<noteq> a \<and> y \<noteq> a \<and> z \<noteq> a \<and> x \<noteq> y \<and>
-        Fun.swap a b id \<circ> Fun.swap c d id = Fun.swap x y id \<circ> Fun.swap a z id))"
+        transpose a b \<circ> transpose c d = transpose x y \<circ> transpose a z))"
     apply (rule symmetry_lemma[where a=a and b=b and c=c and d=d])
-     apply (simp_all only: swap_commute)
-    apply (case_tac "a = c \<and> b = d")
-     apply (clarsimp simp only: swap_commute swap_id_idempotent)
-    apply (case_tac "a = c \<and> b \<noteq> d")
-     apply (rule disjI2)
-     apply (rule_tac x="b" in exI)
-     apply (rule_tac x="d" in exI)
-     apply (rule_tac x="b" in exI)
-     apply (clarsimp simp add: fun_eq_iff Fun.swap_def)
-    apply (case_tac "a \<noteq> c \<and> b = d")
-     apply (rule disjI2)
-     apply (rule_tac x="c" in exI)
-     apply (rule_tac x="d" in exI)
-     apply (rule_tac x="c" in exI)
-     apply (clarsimp simp add: fun_eq_iff Fun.swap_def)
-    apply (rule disjI2)
-    apply (rule_tac x="c" in exI)
-    apply (rule_tac x="d" in exI)
-    apply (rule_tac x="b" in exI)
-    apply (clarsimp simp add: fun_eq_iff Fun.swap_def)
+     apply (simp_all only: ac_simps)
+    apply (metis id_comp swap_id_common swap_id_common' swap_id_independent transpose_comp_involutory)
     done
   with neq show ?thesis by metis
 qed
@@ -733,7 +717,7 @@
   using swapidseq.cases[of 0 p "p = id"] by auto
 
 lemma swapidseq_cases: "swapidseq n p \<longleftrightarrow>
-    n = 0 \<and> p = id \<or> (\<exists>a b q m. n = Suc m \<and> p = Fun.swap a b id \<circ> q \<and> swapidseq m q \<and> a \<noteq> b)"
+    n = 0 \<and> p = id \<or> (\<exists>a b q m. n = Suc m \<and> p = transpose a b \<circ> q \<and> swapidseq m q \<and> a \<noteq> b)"
   apply (rule iffI)
    apply (erule swapidseq.cases[of n p])
     apply simp
@@ -750,8 +734,8 @@
 lemma fixing_swapidseq_decrease:
   assumes "swapidseq n p"
     and "a \<noteq> b"
-    and "(Fun.swap a b id \<circ> p) a = a"
-  shows "n \<noteq> 0 \<and> swapidseq (n - 1) (Fun.swap a b id \<circ> p)"
+    and "(transpose a b \<circ> p) a = a"
+  shows "n \<noteq> 0 \<and> swapidseq (n - 1) (transpose a b \<circ> p)"
   using assms
 proof (induct n arbitrary: p a b)
   case 0
@@ -761,11 +745,11 @@
   case (Suc n p a b)
   from Suc.prems(1) swapidseq_cases[of "Suc n" p]
   obtain c d q m where
-    cdqm: "Suc n = Suc m" "p = Fun.swap c d id \<circ> q" "swapidseq m q" "c \<noteq> d" "n = m"
+    cdqm: "Suc n = Suc m" "p = transpose c d \<circ> q" "swapidseq m q" "c \<noteq> d" "n = m"
     by auto
-  consider "Fun.swap a b id \<circ> Fun.swap c d id = id"
+  consider "transpose a b \<circ> transpose c d = id"
     | x y z where "x \<noteq> a" "y \<noteq> a" "z \<noteq> a" "x \<noteq> y"
-      "Fun.swap a b id \<circ> Fun.swap c d id = Fun.swap x y id \<circ> Fun.swap a z id"
+      "transpose a b \<circ> transpose c d = transpose x y \<circ> transpose a z"
     using swap_general[OF Suc.prems(2) cdqm(4)] by metis
   then show ?case
   proof cases
@@ -776,20 +760,20 @@
     case prems: 2
     then have az: "a \<noteq> z"
       by simp
-    from prems have *: "(Fun.swap x y id \<circ> h) a = a \<longleftrightarrow> h a = a" for h
-      by (simp add: Fun.swap_def)
-    from cdqm(2) have "Fun.swap a b id \<circ> p = Fun.swap a b id \<circ> (Fun.swap c d id \<circ> q)"
+    from prems have *: "(transpose x y \<circ> h) a = a \<longleftrightarrow> h a = a" for h
+      by (simp add: transpose_def)
+    from cdqm(2) have "transpose a b \<circ> p = transpose a b \<circ> (transpose c d \<circ> q)"
       by simp
-    then have "Fun.swap a b id \<circ> p = Fun.swap x y id \<circ> (Fun.swap a z id \<circ> q)"
+    then have "transpose a b \<circ> p = transpose x y \<circ> (transpose a z \<circ> q)"
       by (simp add: o_assoc prems)
-    then have "(Fun.swap a b id \<circ> p) a = (Fun.swap x y id \<circ> (Fun.swap a z id \<circ> q)) a"
+    then have "(transpose a b \<circ> p) a = (transpose x y \<circ> (transpose a z \<circ> q)) a"
       by simp
-    then have "(Fun.swap x y id \<circ> (Fun.swap a z id \<circ> q)) a = a"
+    then have "(transpose x y \<circ> (transpose a z \<circ> q)) a = a"
       unfolding Suc by metis
-    then have "(Fun.swap a z id \<circ> q) a = a"
+    then have "(transpose a z \<circ> q) a = a"
       by (simp only: *)
     from Suc.hyps[OF cdqm(3)[ unfolded cdqm(5)[symmetric]] az this]
-    have **: "swapidseq (n - 1) (Fun.swap a z id \<circ> q)" "n \<noteq> 0"
+    have **: "swapidseq (n - 1) (transpose a z \<circ> q)" "n \<noteq> 0"
       by blast+
     from \<open>n \<noteq> 0\<close> have ***: "Suc n - 1 = Suc (n - 1)"
       by auto
@@ -810,7 +794,7 @@
 proof (induct n rule: nat_less_induct)
   case H: (1 n)
   consider "n = 0"
-    | a b :: 'a and q m where "n = Suc m" "id = Fun.swap a b id \<circ> q" "swapidseq m q" "a \<noteq> b"
+    | a b :: 'a and q m where "n = Suc m" "id = transpose a b \<circ> q" "swapidseq m q" "a \<noteq> b"
     using H(2)[unfolded swapidseq_cases[of n id]] by auto
   then show ?case
   proof cases
@@ -865,7 +849,7 @@
   \<open>evenperm (\<lambda>x. x)\<close>
   using evenperm_id by (simp add: id_def [abs_def])
 
-lemma evenperm_swap: "evenperm (Fun.swap a b id) = (a = b)"
+lemma evenperm_swap: "evenperm (transpose a b) = (a = b)"
   by (rule evenperm_unique[where n="if a = b then 0 else 1"]) (simp_all add: swapidseq_swap)
 
 lemma evenperm_comp:
@@ -924,7 +908,7 @@
     let ?S = "insert a (insert b {x. p x \<noteq> x})"
     from comp_Suc.hyps(2) have *: "finite ?S"
       by simp
-    from \<open>a \<noteq> b\<close> have **: "{x. (Fun.swap a b id \<circ> p) x \<noteq> x} \<subseteq> ?S"
+    from \<open>a \<noteq> b\<close> have **: "{x. (transpose a b \<circ> p) x \<noteq> x} \<subseteq> ?S"
       by (auto simp: Fun.swap_def)
     show ?case
       by (rule finite_subset[OF ** *])
@@ -1061,7 +1045,7 @@
 lemma sign_compose: "permutation p \<Longrightarrow> permutation q \<Longrightarrow> sign (p \<circ> q) = sign p * sign q"
   by (simp add: sign_def evenperm_comp)
 
-lemma sign_swap_id: "sign (Fun.swap a b id) = (if a = b then 1 else - 1)"
+lemma sign_swap_id: "sign (transpose a b) = (if a = b then 1 else - 1)"
   by (simp add: sign_def evenperm_swap)
 
 lemma sign_idempotent [simp]: "sign p * sign p = 1"
@@ -1589,16 +1573,16 @@
   assumes fS: "finite S"
     and aS: "a \<notin> S"
   shows "sum f {p. p permutes (insert a S)} =
-    sum (\<lambda>b. sum (\<lambda>q. f (Fun.swap a b id \<circ> q)) {p. p permutes S}) (insert a S)"
+    sum (\<lambda>b. sum (\<lambda>q. f (transpose a b \<circ> q)) {p. p permutes S}) (insert a S)"
 proof -
-  have *: "\<And>f a b. (\<lambda>(b, p). f (Fun.swap a b id \<circ> p)) = f \<circ> (\<lambda>(b,p). Fun.swap a b id \<circ> p)"
+  have *: "\<And>f a b. (\<lambda>(b, p). f (transpose a b \<circ> p)) = f \<circ> (\<lambda>(b,p). transpose a b \<circ> p)"
     by (simp add: fun_eq_iff)
   have **: "\<And>P Q. {(a, b). a \<in> P \<and> b \<in> Q} = P \<times> Q"
     by blast
   show ?thesis
     unfolding * ** sum.cartesian_product permutes_insert
   proof (rule sum.reindex)
-    let ?f = "(\<lambda>(b, y). Fun.swap a b id \<circ> y)"
+    let ?f = "(\<lambda>(b, y). transpose a b \<circ> y)"
     let ?P = "{p. p permutes S}"
     {
       fix b c p q
@@ -1606,16 +1590,16 @@
       assume c: "c \<in> insert a S"
       assume p: "p permutes S"
       assume q: "q permutes S"
-      assume eq: "Fun.swap a b id \<circ> p = Fun.swap a c id \<circ> q"
+      assume eq: "transpose a b \<circ> p = transpose a c \<circ> q"
       from p q aS have pa: "p a = a" and qa: "q a = a"
         unfolding permutes_def by metis+
-      from eq have "(Fun.swap a b id \<circ> p) a  = (Fun.swap a c id \<circ> q) a"
+      from eq have "(transpose a b \<circ> p) a  = (transpose a c \<circ> q) a"
         by simp
       then have bc: "b = c"
         by (simp add: permutes_def pa qa o_def fun_upd_def Fun.swap_def id_def
             cong del: if_weak_cong split: if_split_asm)
-      from eq[unfolded bc] have "(\<lambda>p. Fun.swap a c id \<circ> p) (Fun.swap a c id \<circ> p) =
-        (\<lambda>p. Fun.swap a c id \<circ> p) (Fun.swap a c id \<circ> q)" by simp
+      from eq[unfolded bc] have "(\<lambda>p. transpose a c \<circ> p) (transpose a c \<circ> p) =
+        (\<lambda>p. transpose a c \<circ> p) (transpose a c \<circ> q)" by simp
       then have "p = q"
         unfolding o_assoc swap_id_idempotent by simp
       with bc have "b = c \<and> p = q"
diff -r a037f01aedab -r 1bd3463e30b8 src/HOL/Combinatorics/Transposition.thy
--- a/src/HOL/Combinatorics/Transposition.thy	Fri May 07 16:49:08 2021 +0200
+++ b/src/HOL/Combinatorics/Transposition.thy	Sun May 09 05:48:50 2021 +0000
@@ -4,77 +4,167 @@
   imports Main
 begin
 
+definition transpose :: \<open>'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a\<close>
+  where \<open>transpose a b c = (if c = a then b else if c = b then a else c)\<close>
+
+lemma transpose_apply_first [simp]:
+  \<open>transpose a b a = b\<close>
+  by (simp add: transpose_def)
+
+lemma transpose_apply_second [simp]:
+  \<open>transpose a b b = a\<close>
+  by (simp add: transpose_def)
+
+lemma transpose_apply_other [simp]:
+  \<open>transpose a b c = c\<close> if \<open>c \<noteq> a\<close> \<open>c \<noteq> b\<close>
+  using that by (simp add: transpose_def)
+
+lemma transpose_same [simp]:
+  \<open>transpose a a = id\<close>
+  by (simp add: fun_eq_iff transpose_def)
+
+lemma transpose_eq_iff:
+  \<open>transpose a b c = d \<longleftrightarrow> (c \<noteq> a \<and> c \<noteq> b \<and> d = c) \<or> (c = a \<and> d = b) \<or> (c = b \<and> d = a)\<close>
+  by (auto simp add: transpose_def)
+
+lemma transpose_eq_imp_eq:
+  \<open>c = d\<close> if \<open>transpose a b c = transpose a b d\<close>
+  using that by (auto simp add: transpose_eq_iff)
+
+lemma transpose_commute [ac_simps]:
+  \<open>transpose b a = transpose a b\<close>
+  by (auto simp add: fun_eq_iff transpose_eq_iff)
+
+lemma transpose_involutory [simp]:
+  \<open>transpose a b (transpose a b c) = c\<close>
+  by (auto simp add: transpose_eq_iff)
+
+lemma transpose_comp_involutory [simp]:
+  \<open>transpose a b \<circ> transpose a b = id\<close>
+  by (rule ext) simp
+
+lemma transpose_triple:
+  \<open>transpose a b (transpose b c (transpose a b d)) = transpose a c d\<close>
+  if \<open>a \<noteq> c\<close> and \<open>b \<noteq> c\<close>
+  using that by (simp add: transpose_def)
+
+lemma transpose_comp_triple:
+  \<open>transpose a b \<circ> transpose b c \<circ> transpose a b = transpose a c\<close>
+  if \<open>a \<noteq> c\<close> and \<open>b \<noteq> c\<close>
+  using that by (simp add: fun_eq_iff transpose_triple)
+
+lemma transpose_image_eq [simp]:
+  \<open>transpose a b ` A = A\<close> if \<open>a \<in> A \<longleftrightarrow> b \<in> A\<close>
+  using that by (auto simp add: transpose_def [abs_def])
+
+lemma inj_on_transpose [simp]:
+  \<open>inj_on (transpose a b) A\<close>
+  by rule (drule transpose_eq_imp_eq)
+
+lemma inj_transpose:
+  \<open>inj (transpose a b)\<close>
+  by (fact inj_on_transpose)
+
+lemma surj_transpose:
+  \<open>surj (transpose a b)\<close>
+  by simp
+
+lemma bij_betw_transpose_iff [simp]:
+  \<open>bij_betw (transpose a b) A A\<close> if \<open>a \<in> A \<longleftrightarrow> b \<in> A\<close>
+  using that by (auto simp: bij_betw_def)
+
+lemma bij_transpose [simp]:
+  \<open>bij (transpose a b)\<close>
+  by (rule bij_betw_transpose_iff) simp
+
+lemma bijection_transpose:
+  \<open>bijection (transpose a b)\<close>
+  by standard (fact bij_transpose)
+
+lemma inv_transpose_eq [simp]:
+  \<open>inv (transpose a b) = transpose a b\<close>
+  by (rule inv_unique_comp) simp_all
+
+lemma transpose_apply_commute:
+  \<open>transpose a b (f c) = f (transpose (inv f a) (inv f b) c)\<close>
+  if \<open>bij f\<close>
+proof -
+  from that have \<open>surj f\<close>
+    by (rule bij_is_surj)
+  with that show ?thesis
+    by (simp add: transpose_def bij_inv_eq_iff surj_f_inv_f)
+qed
+
+lemma transpose_comp_eq:
+  \<open>transpose a b \<circ> f = f \<circ> transpose (inv f a) (inv f b)\<close>
+  if \<open>bij f\<close>
+  using that by (simp add: fun_eq_iff transpose_apply_commute)
+
+
+text \<open>Legacy input alias\<close>
+
 setup \<open>Context.theory_map (Name_Space.map_naming (Name_Space.qualified_path true \<^binding>\<open>Fun\<close>))\<close>
 
-definition swap :: \<open>'a \<Rightarrow> 'a \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b)\<close>
-  where \<open>swap a b f = f (a := f b, b:= f a)\<close>
+abbreviation (input) swap :: \<open>'a \<Rightarrow> 'a \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b\<close>
+  where \<open>swap a b f \<equiv> f \<circ> transpose a b\<close>
+
+lemma swap_def:
+  \<open>Fun.swap a b f = f (a := f b, b:= f a)\<close>
+  by (simp add: fun_eq_iff)
 
 setup \<open>Context.theory_map (Name_Space.map_naming (Name_Space.parent_path))\<close>
 
-lemma swap_apply [simp]:
+lemma swap_apply:
   "Fun.swap a b f a = f b"
   "Fun.swap a b f b = f a"
   "c \<noteq> a \<Longrightarrow> c \<noteq> b \<Longrightarrow> Fun.swap a b f c = f c"
-  by (simp_all add: Fun.swap_def)
+  by simp_all
 
-lemma swap_self [simp]: "Fun.swap a a f = f"
-  by (simp add: Fun.swap_def)
+lemma swap_self: "Fun.swap a a f = f"
+  by simp
 
 lemma swap_commute: "Fun.swap a b f = Fun.swap b a f"
-  by (simp add: fun_upd_def Fun.swap_def fun_eq_iff)
+  by (simp add: ac_simps)
 
-lemma swap_nilpotent [simp]: "Fun.swap a b (Fun.swap a b f) = f"
-  by (rule ext) (simp add: fun_upd_def Fun.swap_def)
+lemma swap_nilpotent: "Fun.swap a b (Fun.swap a b f) = f"
+  by (simp add: comp_assoc)
 
-lemma swap_comp_involutory [simp]: "Fun.swap a b \<circ> Fun.swap a b = id"
-  by (rule ext) simp
+lemma swap_comp_involutory: "Fun.swap a b \<circ> Fun.swap a b = id"
+  by (simp add: fun_eq_iff)
 
 lemma swap_triple:
   assumes "a \<noteq> c" and "b \<noteq> c"
   shows "Fun.swap a b (Fun.swap b c (Fun.swap a b f)) = Fun.swap a c f"
-  using assms by (simp add: fun_eq_iff Fun.swap_def)
+  using assms transpose_comp_triple [of a c b]
+  by (simp add: comp_assoc)
 
 lemma comp_swap: "f \<circ> Fun.swap a b g = Fun.swap a b (f \<circ> g)"
-  by (rule ext) (simp add: fun_upd_def Fun.swap_def)
+  by (simp add: comp_assoc)
 
-lemma swap_image_eq [simp]:
+lemma swap_image_eq:
   assumes "a \<in> A" "b \<in> A"
   shows "Fun.swap a b f ` A = f ` A"
-proof -
-  have subset: "\<And>f. Fun.swap a b f ` A \<subseteq> f ` A"
-    using assms by (auto simp: image_iff Fun.swap_def)
-  then have "Fun.swap a b (Fun.swap a b f) ` A \<subseteq> (Fun.swap a b f) ` A" .
-  with subset[of f] show ?thesis by auto
-qed
+  using assms by (metis image_comp transpose_image_eq)
 
 lemma inj_on_imp_inj_on_swap: "inj_on f A \<Longrightarrow> a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> inj_on (Fun.swap a b f) A"
-  by (auto simp add: inj_on_def Fun.swap_def)
-
-lemma inj_on_swap_iff [simp]:
+  by (simp add: comp_inj_on)
+  
+lemma inj_on_swap_iff:
   assumes A: "a \<in> A" "b \<in> A"
   shows "inj_on (Fun.swap a b f) A \<longleftrightarrow> inj_on f A"
-proof
-  assume "inj_on (Fun.swap a b f) A"
-  with A have "inj_on (Fun.swap a b (Fun.swap a b f)) A"
-    by (iprover intro: inj_on_imp_inj_on_swap)
-  then show "inj_on f A" by simp
-next
-  assume "inj_on f A"
-  with A show "inj_on (Fun.swap a b f) A"
-    by (iprover intro: inj_on_imp_inj_on_swap)
-qed
+  using assms by (metis inj_on_imageI inj_on_imp_inj_on_swap transpose_image_eq)
 
 lemma surj_imp_surj_swap: "surj f \<Longrightarrow> surj (Fun.swap a b f)"
-  by simp
+  by (meson comp_surj surj_transpose)
 
-lemma surj_swap_iff [simp]: "surj (Fun.swap a b f) \<longleftrightarrow> surj f"
-  by simp
+lemma surj_swap_iff: "surj (Fun.swap a b f) \<longleftrightarrow> surj f"
+  by (metis fun.set_map surj_transpose)
 
-lemma bij_betw_swap_iff [simp]: "x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> bij_betw (Fun.swap x y f) A B \<longleftrightarrow> bij_betw f A B"
-  by (auto simp: bij_betw_def)
+lemma bij_betw_swap_iff: "x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> bij_betw (Fun.swap x y f) A B \<longleftrightarrow> bij_betw f A B"
+  by (meson bij_betw_comp_iff bij_betw_transpose_iff)
 
-lemma bij_swap_iff [simp]: "bij (Fun.swap a b f) \<longleftrightarrow> bij f"
-  by simp
+lemma bij_swap_iff: "bij (Fun.swap a b f) \<longleftrightarrow> bij f"
+  by (simp add: bij_betw_swap_iff)
 
 lemma swap_image:
   \<open>Fun.swap i j f ` A = f ` (A - {i, j}
@@ -82,26 +172,22 @@
   by (auto simp add: Fun.swap_def)
 
 lemma inv_swap_id: "inv (Fun.swap a b id) = Fun.swap a b id"
-  by (rule inv_unique_comp) (simp_all add: fun_eq_iff Fun.swap_def)
+  by simp
 
 lemma bij_swap_comp:
   assumes "bij p"
   shows "Fun.swap a b id \<circ> p = Fun.swap (inv p a) (inv p b) p"
-  using surj_f_inv_f[OF bij_is_surj[OF \<open>bij p\<close>]]
-  by (simp add: fun_eq_iff Fun.swap_def bij_inv_eq_iff[OF \<open>bij p\<close>])
-
-
-subsection \<open>Transpositions\<close>
+  using assms by (simp add: transpose_comp_eq) 
 
 lemma swap_id_eq: "Fun.swap a b id x = (if x = a then b else if x = b then a else x)"
   by (simp add: Fun.swap_def)
 
 lemma swap_unfold:
   \<open>Fun.swap a b p = p \<circ> Fun.swap a b id\<close>
-  by (simp add: fun_eq_iff Fun.swap_def)
+  by simp
 
-lemma swap_id_idempotent [simp]: "Fun.swap a b id \<circ> Fun.swap a b id = id"
-  by (simp flip: swap_unfold)
+lemma swap_id_idempotent: "Fun.swap a b id \<circ> Fun.swap a b id = id"
+  by simp
 
 lemma bij_swap_compose_bij:
   \<open>bij (Fun.swap a b id \<circ> p)\<close> if \<open>bij p\<close>
diff -r a037f01aedab -r 1bd3463e30b8 src/HOL/ex/Dedekind_Real.thy
--- a/src/HOL/ex/Dedekind_Real.thy	Fri May 07 16:49:08 2021 +0200
+++ b/src/HOL/ex/Dedekind_Real.thy	Sun May 09 05:48:50 2021 +0000
@@ -372,7 +372,8 @@
 
 lemma preal_mult_assoc: "((x::preal) * y) * z = x * (y * z)"
   apply (simp add: preal_mult_def mem_mult_set Rep_preal)
-  apply (force simp: mult_set_def ac_simps)
+  apply (simp add: mult_set_def)
+  apply (metis (no_types, hide_lams) ab_semigroup_mult_class.mult_ac(1))
   done
 
 instance preal :: ab_semigroup_mult
diff -r a037f01aedab -r 1bd3463e30b8 src/HOL/ex/Perm_Fragments.thy
--- a/src/HOL/ex/Perm_Fragments.thy	Fri May 07 16:49:08 2021 +0200
+++ b/src/HOL/ex/Perm_Fragments.thy	Sun May 09 05:48:50 2021 +0000
@@ -77,7 +77,7 @@
     with distinct have "distinct (a # b # cs @ [c])"
       by simp
     then have **: "\<langle>a \<leftrightarrow> b\<rangle> * \<langle>c \<leftrightarrow> a\<rangle> = \<langle>c \<leftrightarrow> a\<rangle> * \<langle>c \<leftrightarrow> b\<rangle>"
-      by transfer (auto simp add: comp_def Fun.swap_def)
+      by transfer (auto simp add: fun_eq_iff transpose_def)
     with snoc * show ?thesis
       by (simp add: mult.assoc [symmetric])
   qed