# HG changeset patch
# User haftmann
# Date 1620675954 0
# Node ID 7734c442802fed38c98fa3f81ac633587d9bad22
# Parent  fecfb96474ca014a6b83b94c289523b9aaf09fcf
avoid Fun.swap

diff -r fecfb96474ca -r 7734c442802f src/HOL/Combinatorics/Cycles.thy
--- a/src/HOL/Combinatorics/Cycles.thy	Mon May 10 19:45:51 2021 +0000
+++ b/src/HOL/Combinatorics/Cycles.thy	Mon May 10 19:45:54 2021 +0000
@@ -43,20 +43,25 @@
 proof -
   { have "map (cycle_of_list cs) cs = rotate1 cs" using assms(1)
     proof (induction cs rule: cycle_of_list.induct)
-      case (1 i j cs) thus ?case
+      case (1 i j cs)
+      then have \<open>i \<notin> set cs\<close> \<open>j \<notin> set cs\<close>
+        by auto
+      then have \<open>map (Transposition.transpose i j) cs = cs\<close>
+        by (auto intro: map_idI simp add: transpose_eq_iff)
+      show ?case
       proof (cases)
         assume "cs = Nil" thus ?thesis by simp
       next
         assume "cs \<noteq> Nil" hence ge_two: "length (j # cs) \<ge> 2"
           using not_less by auto
         have "map (cycle_of_list (i # j # cs)) (i # j # cs) =
-              map (Fun.swap i j id) (map (cycle_of_list (j # cs)) (i # j # cs))" by simp
-        also have " ... = map (Fun.swap i j id) (i # (rotate1 (j # cs)))"
+              map (transpose i j) (map (cycle_of_list (j # cs)) (i # j # cs))" by simp
+        also have " ... = map (transpose i j) (i # (rotate1 (j # cs)))"
           by (metis "1.IH" "1.prems" distinct.simps(2) id_outside_supp list.simps(9))
-        also have " ... = map (Fun.swap i j id) (i # (cs @ [j]))" by simp
-        also have " ... = j # (map (Fun.swap i j id) cs) @ [i]" by simp
+        also have " ... = map (transpose i j) (i # (cs @ [j]))" by simp
+        also have " ... = j # (map (transpose i j) cs) @ [i]" by simp
         also have " ... = j # cs @ [i]"
-          by (metis "1.prems" distinct.simps(2) list.set_intros(2) map_idI swap_id_eq)
+          using \<open>map (Transposition.transpose i j) cs = cs\<close> by simp
         also have " ... = rotate1 (i # j # cs)" by simp
         finally show ?thesis .
       qed
@@ -118,7 +123,7 @@
 proof (induction cs rule: cycle_of_list.induct)
   case (1 i j cs)
   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)"
+       (p \<circ> (transpose i j) \<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 " ... = (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)
diff -r fecfb96474ca -r 7734c442802f src/HOL/Combinatorics/Permutations.thy
--- a/src/HOL/Combinatorics/Permutations.thy	Mon May 10 19:45:51 2021 +0000
+++ b/src/HOL/Combinatorics/Permutations.thy	Mon May 10 19:45:54 2021 +0000
@@ -382,7 +382,7 @@
   apply (rule permutes_swap_id, simp)
   using permutes_in_image[OF assms, of a]
   apply simp
-  apply (auto simp add: Ball_def Fun.swap_def)
+  apply (auto simp add: Ball_def)
   done
 
 lemma permutes_insert: "{p. p permutes (insert a S)} =
@@ -459,17 +459,17 @@
         from bp cq have pF: "p permutes F" and qF: "q permutes F"
           by auto
         from pF \<open>x \<notin> F\<close> eq have "b = ?g (b, p) x"
-          by (auto simp: permutes_def Fun.swap_def fun_upd_def fun_eq_iff)
+          by (auto simp: permutes_def fun_upd_def fun_eq_iff)
         also from qF \<open>x \<notin> F\<close> eq have "\<dots> = ?g (c, q) x"
           by (auto simp: fun_upd_def fun_eq_iff)
         also from qF \<open>x \<notin> F\<close> have "\<dots> = c"
-          by (auto simp: permutes_def Fun.swap_def fun_upd_def fun_eq_iff)
+          by (auto simp: permutes_def fun_upd_def fun_eq_iff)
         finally have "b = c" .
-        then have "Fun.swap x b id = Fun.swap x c id"
+        then have "transpose x b = transpose x c"
           by simp
-        with eq have "Fun.swap x b id \<circ> p = Fun.swap x b id \<circ> q"
+        with eq have "transpose x b \<circ> p = transpose x b \<circ> q"
           by simp
-        then have "Fun.swap x b id \<circ> (Fun.swap x b id \<circ> p) = Fun.swap x b id \<circ> (Fun.swap x b id \<circ> q)"
+        then have "transpose x b \<circ> (transpose x b \<circ> p) = transpose x b \<circ> (transpose x b \<circ> q)"
           by simp
         then have "p = q"
           by (simp add: o_assoc)
@@ -545,10 +545,10 @@
 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>
+    using permutes_bij by blast
+  have \<open>P (p \<circ> transpose (inv p a) (inv p b))\<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 = transpose a b \<circ> p\<close>
+  also have \<open>p \<circ> transpose (inv p a) (inv p b) = transpose a b \<circ> p\<close>
     using \<open>bij p\<close> by (rule transpose_comp_eq [symmetric])
   finally show ?case .
 qed
@@ -674,16 +674,16 @@
 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>
-  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)
+  transpose a b \<circ> transpose a c = transpose b c \<circ> transpose a b"
+  by (simp add: fun_eq_iff transpose_def)
 
 lemma swap_id_common': "a \<noteq> b \<Longrightarrow> a \<noteq> c \<Longrightarrow>
-  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)
+  transpose a c \<circ> transpose b c = transpose b c \<circ> transpose a b"
+  by (simp add: fun_eq_iff transpose_def)
 
 lemma swap_id_independent: "a \<noteq> c \<Longrightarrow> a \<noteq> d \<Longrightarrow> b \<noteq> c \<Longrightarrow> b \<noteq> d \<Longrightarrow>
   transpose a b \<circ> transpose c d = transpose c d \<circ> transpose a b"
-  by (simp add: fun_eq_iff Fun.swap_def)
+  by (simp add: fun_eq_iff transpose_def)
 
 
 subsection \<open>The identity map only has even transposition sequences\<close>
@@ -740,7 +740,7 @@
 proof (induct n arbitrary: p a b)
   case 0
   then show ?case
-    by (auto simp add: Fun.swap_def fun_upd_def)
+    by (auto simp add: fun_upd_def)
 next
   case (Suc n p a b)
   from Suc.prems(1) swapidseq_cases[of "Suc n" p]
@@ -909,7 +909,7 @@
     from comp_Suc.hyps(2) have *: "finite ?S"
       by simp
     from \<open>a \<noteq> b\<close> have **: "{x. (transpose a b \<circ> p) x \<noteq> x} \<subseteq> ?S"
-      by (auto simp: Fun.swap_def)
+      by auto
     show ?case
       by (rule finite_subset[OF ** *])
   qed
@@ -927,14 +927,14 @@
     by simp
 next
   case (insert a F p)
-  let ?r = "Fun.swap a (p a) id \<circ> p"
-  let ?q = "Fun.swap a (p a) id \<circ> ?r"
+  let ?r = "transpose a (p a) \<circ> p"
+  let ?q = "transpose a (p a) \<circ> ?r"
   have *: "?r a = a"
-    by (simp add: Fun.swap_def)
+    by simp
   from insert * have **: "\<forall>x. x \<notin> F \<longrightarrow> ?r x = x"
     by (metis bij_pointE comp_apply id_apply insert_iff swap_apply(3))
   have "bij ?r"
-    by (rule bij_swap_compose_bij[OF insert(4)])
+    using insert by (simp add: bij_comp)
   have "permutation ?r"
     by (rule insert(3)[OF \<open>bij ?r\<close> **])
   then have "permutation ?q"
@@ -1596,7 +1596,7 @@
       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
+        by (simp add: permutes_def pa qa o_def fun_upd_def id_def
             cong del: if_weak_cong split: if_split_asm)
       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