src/HOL/Library/Permutations.thy
 author Andreas Lochbihler Fri Sep 20 10:09:16 2013 +0200 (2013-09-20) changeset 53745 788730ab7da4 parent 53374 a14d2a854c02 child 54681 8a8e6db7f391 permissions -rw-r--r--
prefer Code.abort over code_abort
```     1 (*  Title:      HOL/Library/Permutations.thy
```
```     2     Author:     Amine Chaieb, University of Cambridge
```
```     3 *)
```
```     4
```
```     5 header {* Permutations, both general and specifically on finite sets.*}
```
```     6
```
```     7 theory Permutations
```
```     8 imports Parity Fact
```
```     9 begin
```
```    10
```
```    11 definition permutes (infixr "permutes" 41) where
```
```    12   "(p permutes S) \<longleftrightarrow> (\<forall>x. x \<notin> S \<longrightarrow> p x = x) \<and> (\<forall>y. \<exists>!x. p x = y)"
```
```    13
```
```    14 (* ------------------------------------------------------------------------- *)
```
```    15 (* Transpositions.                                                           *)
```
```    16 (* ------------------------------------------------------------------------- *)
```
```    17
```
```    18 lemma swapid_sym: "Fun.swap a b id = Fun.swap b a id"
```
```    19   by (auto simp add: fun_eq_iff swap_def fun_upd_def)
```
```    20 lemma swap_id_refl: "Fun.swap a a id = id" by simp
```
```    21 lemma swap_id_sym: "Fun.swap a b id = Fun.swap b a id"
```
```    22   by (rule ext, simp add: swap_def)
```
```    23 lemma swap_id_idempotent[simp]: "Fun.swap a b id o Fun.swap a b id = id"
```
```    24   by (rule ext, auto simp add: swap_def)
```
```    25
```
```    26 lemma inv_unique_comp: assumes fg: "f o g = id" and gf: "g o f = id"
```
```    27   shows "inv f = g"
```
```    28   using fg gf inv_equality[of g f] by (auto simp add: fun_eq_iff)
```
```    29
```
```    30 lemma inverse_swap_id: "inv (Fun.swap a b id) = Fun.swap a b id"
```
```    31   by (rule inv_unique_comp, simp_all)
```
```    32
```
```    33 lemma swap_id_eq: "Fun.swap a b id x = (if x = a then b else if x = b then a else x)"
```
```    34   by (simp add: swap_def)
```
```    35
```
```    36 (* ------------------------------------------------------------------------- *)
```
```    37 (* Basic consequences of the definition.                                     *)
```
```    38 (* ------------------------------------------------------------------------- *)
```
```    39
```
```    40 lemma permutes_in_image: "p permutes S \<Longrightarrow> p x \<in> S \<longleftrightarrow> x \<in> S"
```
```    41   unfolding permutes_def by metis
```
```    42
```
```    43 lemma permutes_image: assumes pS: "p permutes S" shows "p ` S = S"
```
```    44   using pS
```
```    45   unfolding permutes_def
```
```    46   apply -
```
```    47   apply (rule set_eqI)
```
```    48   apply (simp add: image_iff)
```
```    49   apply metis
```
```    50   done
```
```    51
```
```    52 lemma permutes_inj: "p permutes S ==> inj p "
```
```    53   unfolding permutes_def inj_on_def by blast
```
```    54
```
```    55 lemma permutes_surj: "p permutes s ==> surj p"
```
```    56   unfolding permutes_def surj_def by metis
```
```    57
```
```    58 lemma permutes_inv_o: assumes pS: "p permutes S"
```
```    59   shows " p o inv p = id"
```
```    60   and "inv p o p = id"
```
```    61   using permutes_inj[OF pS] permutes_surj[OF pS]
```
```    62   unfolding inj_iff[symmetric] surj_iff[symmetric] by blast+
```
```    63
```
```    64
```
```    65 lemma permutes_inverses:
```
```    66   fixes p :: "'a \<Rightarrow> 'a"
```
```    67   assumes pS: "p permutes S"
```
```    68   shows "p (inv p x) = x"
```
```    69   and "inv p (p x) = x"
```
```    70   using permutes_inv_o[OF pS, unfolded fun_eq_iff o_def] by auto
```
```    71
```
```    72 lemma permutes_subset: "p permutes S \<Longrightarrow> S \<subseteq> T ==> p permutes T"
```
```    73   unfolding permutes_def by blast
```
```    74
```
```    75 lemma permutes_empty[simp]: "p permutes {} \<longleftrightarrow> p = id"
```
```    76   unfolding fun_eq_iff permutes_def apply simp by metis
```
```    77
```
```    78 lemma permutes_sing[simp]: "p permutes {a} \<longleftrightarrow> p = id"
```
```    79   unfolding fun_eq_iff permutes_def apply simp by metis
```
```    80
```
```    81 lemma permutes_univ: "p permutes UNIV \<longleftrightarrow> (\<forall>y. \<exists>!x. p x = y)"
```
```    82   unfolding permutes_def by simp
```
```    83
```
```    84 lemma permutes_inv_eq: "p permutes S ==> inv p y = x \<longleftrightarrow> p x = y"
```
```    85   unfolding permutes_def inv_def apply auto
```
```    86   apply (erule allE[where x=y])
```
```    87   apply (erule allE[where x=y])
```
```    88   apply (rule someI_ex) apply blast
```
```    89   apply (rule some1_equality)
```
```    90   apply blast
```
```    91   apply blast
```
```    92   done
```
```    93
```
```    94 lemma permutes_swap_id: "a \<in> S \<Longrightarrow> b \<in> S ==> Fun.swap a b id permutes S"
```
```    95   unfolding permutes_def swap_def fun_upd_def  by auto metis
```
```    96
```
```    97 lemma permutes_superset:
```
```    98   "p permutes S \<Longrightarrow> (\<forall>x \<in> S - T. p x = x) \<Longrightarrow> p permutes T"
```
```    99 by (simp add: Ball_def permutes_def) metis
```
```   100
```
```   101 (* ------------------------------------------------------------------------- *)
```
```   102 (* Group properties.                                                         *)
```
```   103 (* ------------------------------------------------------------------------- *)
```
```   104
```
```   105 lemma permutes_id: "id permutes S" unfolding permutes_def by simp
```
```   106
```
```   107 lemma permutes_compose: "p permutes S \<Longrightarrow> q permutes S ==> q o p permutes S"
```
```   108   unfolding permutes_def o_def by metis
```
```   109
```
```   110 lemma permutes_inv: assumes pS: "p permutes S" shows "inv p permutes S"
```
```   111   using pS unfolding permutes_def permutes_inv_eq[OF pS] by metis
```
```   112
```
```   113 lemma permutes_inv_inv: assumes pS: "p permutes S" shows "inv (inv p) = p"
```
```   114   unfolding fun_eq_iff permutes_inv_eq[OF pS] permutes_inv_eq[OF permutes_inv[OF pS]]
```
```   115   by blast
```
```   116
```
```   117 (* ------------------------------------------------------------------------- *)
```
```   118 (* The number of permutations on a finite set.                               *)
```
```   119 (* ------------------------------------------------------------------------- *)
```
```   120
```
```   121 lemma permutes_insert_lemma:
```
```   122   assumes pS: "p permutes (insert a S)"
```
```   123   shows "Fun.swap a (p a) id o p permutes S"
```
```   124   apply (rule permutes_superset[where S = "insert a S"])
```
```   125   apply (rule permutes_compose[OF pS])
```
```   126   apply (rule permutes_swap_id, simp)
```
```   127   using permutes_in_image[OF pS, of a] apply simp
```
```   128   apply (auto simp add: Ball_def swap_def)
```
```   129   done
```
```   130
```
```   131 lemma permutes_insert: "{p. p permutes (insert a S)} =
```
```   132         (\<lambda>(b,p). Fun.swap a b id o p) ` {(b,p). b \<in> insert a S \<and> p \<in> {p. p permutes S}}"
```
```   133 proof-
```
```   134
```
```   135   {fix p
```
```   136     {assume pS: "p permutes insert a S"
```
```   137       let ?b = "p a"
```
```   138       let ?q = "Fun.swap a (p a) id o p"
```
```   139       have th0: "p = Fun.swap a ?b id o ?q" unfolding fun_eq_iff o_assoc by simp
```
```   140       have th1: "?b \<in> insert a S " unfolding permutes_in_image[OF pS] by simp
```
```   141       from permutes_insert_lemma[OF pS] th0 th1
```
```   142       have "\<exists> b q. p = Fun.swap a b id o q \<and> b \<in> insert a S \<and> q permutes S" by blast}
```
```   143     moreover
```
```   144     {fix b q assume bq: "p = Fun.swap a b id o q" "b \<in> insert a S" "q permutes S"
```
```   145       from permutes_subset[OF bq(3), of "insert a S"]
```
```   146       have qS: "q permutes insert a S" by auto
```
```   147       have aS: "a \<in> insert a S" by simp
```
```   148       from bq(1) permutes_compose[OF qS permutes_swap_id[OF aS bq(2)]]
```
```   149       have "p permutes insert a S"  by simp }
```
```   150     ultimately have "p permutes insert a S \<longleftrightarrow> (\<exists> b q. p = Fun.swap a b id o q \<and> b \<in> insert a S \<and> q permutes S)" by blast}
```
```   151   thus ?thesis by auto
```
```   152 qed
```
```   153
```
```   154 lemma card_permutations: assumes Sn: "card S = n" and fS: "finite S"
```
```   155   shows "card {p. p permutes S} = fact n"
```
```   156 using fS Sn proof (induct arbitrary: n)
```
```   157   case empty thus ?case by simp
```
```   158 next
```
```   159   case (insert x F)
```
```   160   { fix n assume H0: "card (insert x F) = n"
```
```   161     let ?xF = "{p. p permutes insert x F}"
```
```   162     let ?pF = "{p. p permutes F}"
```
```   163     let ?pF' = "{(b, p). b \<in> insert x F \<and> p \<in> ?pF}"
```
```   164     let ?g = "(\<lambda>(b, p). Fun.swap x b id \<circ> p)"
```
```   165     from permutes_insert[of x F]
```
```   166     have xfgpF': "?xF = ?g ` ?pF'" .
```
```   167     have Fs: "card F = n - 1" using `x \<notin> F` H0 `finite F` by auto
```
```   168     from insert.hyps Fs have pFs: "card ?pF = fact (n - 1)" using `finite F` by auto
```
```   169     then have "finite ?pF" using fact_gt_zero_nat by (auto intro: card_ge_0_finite)
```
```   170     then have pF'f: "finite ?pF'" using H0 `finite F`
```
```   171       apply (simp only: Collect_split Collect_mem_eq)
```
```   172       apply (rule finite_cartesian_product)
```
```   173       apply simp_all
```
```   174       done
```
```   175
```
```   176     have ginj: "inj_on ?g ?pF'"
```
```   177     proof-
```
```   178       {
```
```   179         fix b p c q assume bp: "(b,p) \<in> ?pF'" and cq: "(c,q) \<in> ?pF'"
```
```   180           and eq: "?g (b,p) = ?g (c,q)"
```
```   181         from bp cq have ths: "b \<in> insert x F" "c \<in> insert x F" "x \<in> insert x F" "p permutes F" "q permutes F" by auto
```
```   182         from ths(4) `x \<notin> F` eq have "b = ?g (b,p) x" unfolding permutes_def
```
```   183           by (auto simp add: swap_def fun_upd_def fun_eq_iff)
```
```   184         also have "\<dots> = ?g (c,q) x" using ths(5) `x \<notin> F` eq
```
```   185           by (auto simp add: swap_def fun_upd_def fun_eq_iff)
```
```   186         also have "\<dots> = c"using ths(5) `x \<notin> F` unfolding permutes_def
```
```   187           by (auto simp add: swap_def fun_upd_def fun_eq_iff)
```
```   188         finally have bc: "b = c" .
```
```   189         hence "Fun.swap x b id = Fun.swap x c id" by simp
```
```   190         with eq have "Fun.swap x b id o p = Fun.swap x b id o q" by simp
```
```   191         hence "Fun.swap x b id o (Fun.swap x b id o p) = Fun.swap x b id o (Fun.swap x b id o q)" by simp
```
```   192         hence "p = q" by (simp add: o_assoc)
```
```   193         with bc have "(b,p) = (c,q)" by simp
```
```   194       }
```
```   195       thus ?thesis  unfolding inj_on_def by blast
```
```   196     qed
```
```   197     from `x \<notin> F` H0 have n0: "n \<noteq> 0 " using `finite F` by auto
```
```   198     hence "\<exists>m. n = Suc m" by presburger
```
```   199     then obtain m where n[simp]: "n = Suc m" by blast
```
```   200     from pFs H0 have xFc: "card ?xF = fact n"
```
```   201       unfolding xfgpF' card_image[OF ginj] using `finite F` `finite ?pF`
```
```   202       apply (simp only: Collect_split Collect_mem_eq card_cartesian_product)
```
```   203       by simp
```
```   204     from finite_imageI[OF pF'f, of ?g] have xFf: "finite ?xF" unfolding xfgpF' by simp
```
```   205     have "card ?xF = fact n"
```
```   206       using xFf xFc unfolding xFf by blast
```
```   207   }
```
```   208   thus ?case using insert by simp
```
```   209 qed
```
```   210
```
```   211 lemma finite_permutations: assumes fS: "finite S" shows "finite {p. p permutes S}"
```
```   212   using card_permutations[OF refl fS] fact_gt_zero_nat
```
```   213   by (auto intro: card_ge_0_finite)
```
```   214
```
```   215 (* ------------------------------------------------------------------------- *)
```
```   216 (* Permutations of index set for iterated operations.                        *)
```
```   217 (* ------------------------------------------------------------------------- *)
```
```   218
```
```   219 lemma (in comm_monoid_set) permute:
```
```   220   assumes "p permutes S"
```
```   221   shows "F g S = F (g o p) S"
```
```   222 proof -
```
```   223   from `p permutes S` have "inj p" by (rule permutes_inj)
```
```   224   then have "inj_on p S" by (auto intro: subset_inj_on)
```
```   225   then have "F g (p ` S) = F (g o p) S" by (rule reindex)
```
```   226   moreover from `p permutes S` have "p ` S = S" by (rule permutes_image)
```
```   227   ultimately show ?thesis by simp
```
```   228 qed
```
```   229
```
```   230 lemma setsum_permute:
```
```   231   assumes "p permutes S"
```
```   232   shows "setsum f S = setsum (f o p) S"
```
```   233   using assms by (fact setsum.permute)
```
```   234
```
```   235 lemma setsum_permute_natseg:
```
```   236   assumes pS: "p permutes {m .. n}"
```
```   237   shows "setsum f {m .. n} = setsum (f o p) {m .. n}"
```
```   238   using setsum_permute [OF pS, of f ] pS by blast
```
```   239
```
```   240 lemma setprod_permute:
```
```   241   assumes "p permutes S"
```
```   242   shows "setprod f S = setprod (f o p) S"
```
```   243   using assms by (fact setprod.permute)
```
```   244
```
```   245 lemma setprod_permute_natseg:
```
```   246   assumes pS: "p permutes {m .. n}"
```
```   247   shows "setprod f {m .. n} = setprod (f o p) {m .. n}"
```
```   248   using setprod_permute [OF pS, of f ] pS by blast
```
```   249
```
```   250 (* ------------------------------------------------------------------------- *)
```
```   251 (* Various combinations of transpositions with 2, 1 and 0 common elements.   *)
```
```   252 (* ------------------------------------------------------------------------- *)
```
```   253
```
```   254 lemma swap_id_common:" a \<noteq> c \<Longrightarrow> b \<noteq> c \<Longrightarrow>  Fun.swap a b id o Fun.swap a c id = Fun.swap b c id o Fun.swap a b id" by (simp add: fun_eq_iff swap_def)
```
```   255
```
```   256 lemma swap_id_common': "~(a = b) \<Longrightarrow> ~(a = c) \<Longrightarrow> Fun.swap a c id o Fun.swap b c id = Fun.swap b c id o Fun.swap a b id" by (simp add: fun_eq_iff swap_def)
```
```   257
```
```   258 lemma swap_id_independent: "~(a = c) \<Longrightarrow> ~(a = d) \<Longrightarrow> ~(b = c) \<Longrightarrow> ~(b = d) ==> Fun.swap a b id o Fun.swap c d id = Fun.swap c d id o Fun.swap a b id"
```
```   259   by (simp add: swap_def fun_eq_iff)
```
```   260
```
```   261 (* ------------------------------------------------------------------------- *)
```
```   262 (* Permutations as transposition sequences.                                  *)
```
```   263 (* ------------------------------------------------------------------------- *)
```
```   264
```
```   265
```
```   266 inductive swapidseq :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> bool" where
```
```   267   id[simp]: "swapidseq 0 id"
```
```   268 | comp_Suc: "swapidseq n p \<Longrightarrow> a \<noteq> b \<Longrightarrow> swapidseq (Suc n) (Fun.swap a b id o p)"
```
```   269
```
```   270 declare id[unfolded id_def, simp]
```
```   271 definition "permutation p \<longleftrightarrow> (\<exists>n. swapidseq n p)"
```
```   272
```
```   273 (* ------------------------------------------------------------------------- *)
```
```   274 (* Some closure properties of the set of permutations, with lengths.         *)
```
```   275 (* ------------------------------------------------------------------------- *)
```
```   276
```
```   277 lemma permutation_id[simp]: "permutation id"unfolding permutation_def
```
```   278   by (rule exI[where x=0], simp)
```
```   279 declare permutation_id[unfolded id_def, simp]
```
```   280
```
```   281 lemma swapidseq_swap: "swapidseq (if a = b then 0 else 1) (Fun.swap a b id)"
```
```   282   apply clarsimp
```
```   283   using comp_Suc[of 0 id a b] by simp
```
```   284
```
```   285 lemma permutation_swap_id: "permutation (Fun.swap a b id)"
```
```   286   apply (cases "a=b", simp_all)
```
```   287   unfolding permutation_def using swapidseq_swap[of a b] by blast
```
```   288
```
```   289 lemma swapidseq_comp_add: "swapidseq n p \<Longrightarrow> swapidseq m q ==> swapidseq (n + m) (p o q)"
```
```   290   proof (induct n p arbitrary: m q rule: swapidseq.induct)
```
```   291     case (id m q) thus ?case by simp
```
```   292   next
```
```   293     case (comp_Suc n p a b m q)
```
```   294     have th: "Suc n + m = Suc (n + m)" by arith
```
```   295     show ?case unfolding th comp_assoc
```
```   296       apply (rule swapidseq.comp_Suc) using comp_Suc.hyps(2)[OF comp_Suc.prems]  comp_Suc.hyps(3) by blast+
```
```   297 qed
```
```   298
```
```   299 lemma permutation_compose: "permutation p \<Longrightarrow> permutation q ==> permutation(p o q)"
```
```   300   unfolding permutation_def using swapidseq_comp_add[of _ p _ q] by metis
```
```   301
```
```   302 lemma swapidseq_endswap: "swapidseq n p \<Longrightarrow> a \<noteq> b ==> swapidseq (Suc n) (p o Fun.swap a b id)"
```
```   303   apply (induct n p rule: swapidseq.induct)
```
```   304   using swapidseq_swap[of a b]
```
```   305   by (auto simp add: comp_assoc intro: swapidseq.comp_Suc)
```
```   306
```
```   307 lemma swapidseq_inverse_exists: "swapidseq n p ==> \<exists>q. swapidseq n q \<and> p o q = id \<and> q o p = id"
```
```   308 proof(induct n p rule: swapidseq.induct)
```
```   309   case id  thus ?case by (rule exI[where x=id], simp)
```
```   310 next
```
```   311   case (comp_Suc n p a b)
```
```   312   from comp_Suc.hyps obtain q where q: "swapidseq n q" "p \<circ> q = id" "q \<circ> p = id" by blast
```
```   313   let ?q = "q o Fun.swap a b id"
```
```   314   note H = comp_Suc.hyps
```
```   315   from swapidseq_swap[of a b] H(3)  have th0: "swapidseq 1 (Fun.swap a b id)" by simp
```
```   316   from swapidseq_comp_add[OF q(1) th0] have th1:"swapidseq (Suc n) ?q" by simp
```
```   317   have "Fun.swap a b id o p o ?q = Fun.swap a b id o (p o q) o Fun.swap a b id" by (simp add: o_assoc)
```
```   318   also have "\<dots> = id" by (simp add: q(2))
```
```   319   finally have th2: "Fun.swap a b id o p o ?q = id" .
```
```   320   have "?q \<circ> (Fun.swap a b id \<circ> p) = q \<circ> (Fun.swap a b id o Fun.swap a b id) \<circ> p" by (simp only: o_assoc)
```
```   321   hence "?q \<circ> (Fun.swap a b id \<circ> p) = id" by (simp add: q(3))
```
```   322   with th1 th2 show ?case by blast
```
```   323 qed
```
```   324
```
```   325
```
```   326 lemma swapidseq_inverse: assumes H: "swapidseq n p" shows "swapidseq n (inv p)"
```
```   327   using swapidseq_inverse_exists[OF H] inv_unique_comp[of p] by auto
```
```   328
```
```   329 lemma permutation_inverse: "permutation p ==> permutation (inv p)"
```
```   330   using permutation_def swapidseq_inverse by blast
```
```   331
```
```   332 (* ------------------------------------------------------------------------- *)
```
```   333 (* The identity map only has even transposition sequences.                   *)
```
```   334 (* ------------------------------------------------------------------------- *)
```
```   335
```
```   336 lemma symmetry_lemma:"(\<And>a b c d. P a b c d ==> P a b d c) \<Longrightarrow>
```
```   337    (\<And>a b c d. a \<noteq> b \<Longrightarrow> c \<noteq> d \<Longrightarrow> (a = c \<and> b = d \<or>  a = c \<and> b \<noteq> d \<or> a \<noteq> c \<and> b = d \<or> a \<noteq> c \<and> a \<noteq> d \<and> b \<noteq> c \<and> b \<noteq> d) ==> P a b c d)
```
```   338    ==> (\<And>a b c d. a \<noteq> b --> c \<noteq> d \<longrightarrow>  P a b c d)" by metis
```
```   339
```
```   340 lemma swap_general: "a \<noteq> b \<Longrightarrow> c \<noteq> d \<Longrightarrow> Fun.swap a b id o Fun.swap c d id = id \<or>
```
```   341   (\<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 o Fun.swap c d id = Fun.swap x y id o Fun.swap a z id)"
```
```   342 proof-
```
```   343   assume H: "a\<noteq>b" "c\<noteq>d"
```
```   344 have "a \<noteq> b \<longrightarrow> c \<noteq> d \<longrightarrow>
```
```   345 (  Fun.swap a b id o Fun.swap c d id = id \<or>
```
```   346   (\<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 o Fun.swap c d id = Fun.swap x y id o Fun.swap a z id))"
```
```   347   apply (rule symmetry_lemma[where a=a and b=b and c=c and d=d])
```
```   348   apply (simp_all only: swapid_sym)
```
```   349   apply (case_tac "a = c \<and> b = d", clarsimp simp only: swapid_sym swap_id_idempotent)
```
```   350   apply (case_tac "a = c \<and> b \<noteq> d")
```
```   351   apply (rule disjI2)
```
```   352   apply (rule_tac x="b" in exI)
```
```   353   apply (rule_tac x="d" in exI)
```
```   354   apply (rule_tac x="b" in exI)
```
```   355   apply (clarsimp simp add: fun_eq_iff swap_def)
```
```   356   apply (case_tac "a \<noteq> c \<and> b = d")
```
```   357   apply (rule disjI2)
```
```   358   apply (rule_tac x="c" in exI)
```
```   359   apply (rule_tac x="d" in exI)
```
```   360   apply (rule_tac x="c" in exI)
```
```   361   apply (clarsimp simp add: fun_eq_iff swap_def)
```
```   362   apply (rule disjI2)
```
```   363   apply (rule_tac x="c" in exI)
```
```   364   apply (rule_tac x="d" in exI)
```
```   365   apply (rule_tac x="b" in exI)
```
```   366   apply (clarsimp simp add: fun_eq_iff swap_def)
```
```   367   done
```
```   368 with H show ?thesis by metis
```
```   369 qed
```
```   370
```
```   371 lemma swapidseq_id_iff[simp]: "swapidseq 0 p \<longleftrightarrow> p = id"
```
```   372   using swapidseq.cases[of 0 p "p = id"]
```
```   373   by auto
```
```   374
```
```   375 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 o q \<and> swapidseq m q \<and> a\<noteq> b))"
```
```   376   apply (rule iffI)
```
```   377   apply (erule swapidseq.cases[of n p])
```
```   378   apply simp
```
```   379   apply (rule disjI2)
```
```   380   apply (rule_tac x= "a" in exI)
```
```   381   apply (rule_tac x= "b" in exI)
```
```   382   apply (rule_tac x= "pa" in exI)
```
```   383   apply (rule_tac x= "na" in exI)
```
```   384   apply simp
```
```   385   apply auto
```
```   386   apply (rule comp_Suc, simp_all)
```
```   387   done
```
```   388 lemma fixing_swapidseq_decrease:
```
```   389   assumes spn: "swapidseq n p" and ab: "a\<noteq>b" and pa: "(Fun.swap a b id o p) a = a"
```
```   390   shows "n \<noteq> 0 \<and> swapidseq (n - 1) (Fun.swap a b id o p)"
```
```   391   using spn ab pa
```
```   392 proof(induct n arbitrary: p a b)
```
```   393   case 0 thus ?case by (auto simp add: swap_def fun_upd_def)
```
```   394 next
```
```   395   case (Suc n p a b)
```
```   396   from Suc.prems(1) swapidseq_cases[of "Suc n" p] obtain
```
```   397     c d q m where cdqm: "Suc n = Suc m" "p = Fun.swap c d id o q" "swapidseq m q" "c \<noteq> d" "n = m"
```
```   398     by auto
```
```   399   {assume H: "Fun.swap a b id o Fun.swap c d id = id"
```
```   400
```
```   401     have ?case apply (simp only: cdqm o_assoc H)
```
```   402       by (simp add: cdqm)}
```
```   403   moreover
```
```   404   { fix x y z
```
```   405     assume H: "x\<noteq>a" "y\<noteq>a" "z \<noteq>a" "x \<noteq>y"
```
```   406       "Fun.swap a b id o Fun.swap c d id = Fun.swap x y id o Fun.swap a z id"
```
```   407     from H have az: "a \<noteq> z" by simp
```
```   408
```
```   409     {fix h have "(Fun.swap x y id o h) a = a \<longleftrightarrow> h a = a"
```
```   410       using H by (simp add: swap_def)}
```
```   411     note th3 = this
```
```   412     from cdqm(2) have "Fun.swap a b id o p = Fun.swap a b id o (Fun.swap c d id o q)" by simp
```
```   413     hence "Fun.swap a b id o p = Fun.swap x y id o (Fun.swap a z id o q)" by (simp add: o_assoc H)
```
```   414     hence "(Fun.swap a b id o p) a = (Fun.swap x y id o (Fun.swap a z id o q)) a" by simp
```
```   415     hence "(Fun.swap x y id o (Fun.swap a z id o q)) a  = a" unfolding Suc by metis
```
```   416     hence th1: "(Fun.swap a z id o q) a = a" unfolding th3 .
```
```   417     from Suc.hyps[OF cdqm(3)[ unfolded cdqm(5)[symmetric]] az th1]
```
```   418     have th2: "swapidseq (n - 1) (Fun.swap a z id o q)" "n \<noteq> 0" by blast+
```
```   419     have th: "Suc n - 1 = Suc (n - 1)" using th2(2) by auto
```
```   420     have ?case unfolding cdqm(2) H o_assoc th
```
```   421       apply (simp only: Suc_not_Zero simp_thms comp_assoc)
```
```   422       apply (rule comp_Suc)
```
```   423       using th2 H apply blast+
```
```   424       done}
```
```   425   ultimately show ?case using swap_general[OF Suc.prems(2) cdqm(4)] by metis
```
```   426 qed
```
```   427
```
```   428 lemma swapidseq_identity_even:
```
```   429   assumes "swapidseq n (id :: 'a \<Rightarrow> 'a)" shows "even n"
```
```   430   using `swapidseq n id`
```
```   431 proof(induct n rule: nat_less_induct)
```
```   432   fix n
```
```   433   assume H: "\<forall>m<n. swapidseq m (id::'a \<Rightarrow> 'a) \<longrightarrow> even m" "swapidseq n (id :: 'a \<Rightarrow> 'a)"
```
```   434   {assume "n = 0" hence "even n" by arith}
```
```   435   moreover
```
```   436   {fix a b :: 'a and q m
```
```   437     assume h: "n = Suc m" "(id :: 'a \<Rightarrow> 'a) = Fun.swap a b id \<circ> q" "swapidseq m q" "a \<noteq> b"
```
```   438     from fixing_swapidseq_decrease[OF h(3,4), unfolded h(2)[symmetric]]
```
```   439     have m: "m \<noteq> 0" "swapidseq (m - 1) (id :: 'a \<Rightarrow> 'a)" by auto
```
```   440     from h m have mn: "m - 1 < n" by arith
```
```   441     from H(1)[rule_format, OF mn m(2)] h(1) m(1) have "even n" apply arith done}
```
```   442   ultimately show "even n" using H(2)[unfolded swapidseq_cases[of n id]] by auto
```
```   443 qed
```
```   444
```
```   445 (* ------------------------------------------------------------------------- *)
```
```   446 (* Therefore we have a welldefined notion of parity.                         *)
```
```   447 (* ------------------------------------------------------------------------- *)
```
```   448
```
```   449 definition "evenperm p = even (SOME n. swapidseq n p)"
```
```   450
```
```   451 lemma swapidseq_even_even: assumes
```
```   452   m: "swapidseq m p" and n: "swapidseq n p"
```
```   453   shows "even m \<longleftrightarrow> even n"
```
```   454 proof-
```
```   455   from swapidseq_inverse_exists[OF n]
```
```   456   obtain q where q: "swapidseq n q" "p \<circ> q = id" "q \<circ> p = id" by blast
```
```   457
```
```   458   from swapidseq_identity_even[OF swapidseq_comp_add[OF m q(1), unfolded q]]
```
```   459   show ?thesis by arith
```
```   460 qed
```
```   461
```
```   462 lemma evenperm_unique: assumes p: "swapidseq n p" and n:"even n = b"
```
```   463   shows "evenperm p = b"
```
```   464   unfolding n[symmetric] evenperm_def
```
```   465   apply (rule swapidseq_even_even[where p = p])
```
```   466   apply (rule someI[where x = n])
```
```   467   using p by blast+
```
```   468
```
```   469 (* ------------------------------------------------------------------------- *)
```
```   470 (* And it has the expected composition properties.                           *)
```
```   471 (* ------------------------------------------------------------------------- *)
```
```   472
```
```   473 lemma evenperm_id[simp]: "evenperm id = True"
```
```   474   apply (rule evenperm_unique[where n = 0]) by simp_all
```
```   475
```
```   476 lemma evenperm_swap: "evenperm (Fun.swap a b id) = (a = b)"
```
```   477 apply (rule evenperm_unique[where n="if a = b then 0 else 1"])
```
```   478 by (simp_all add: swapidseq_swap)
```
```   479
```
```   480 lemma evenperm_comp:
```
```   481   assumes p: "permutation p" and q:"permutation q"
```
```   482   shows "evenperm (p o q) = (evenperm p = evenperm q)"
```
```   483 proof-
```
```   484   from p q obtain
```
```   485     n m where n: "swapidseq n p" and m: "swapidseq m q"
```
```   486     unfolding permutation_def by blast
```
```   487   note nm =  swapidseq_comp_add[OF n m]
```
```   488   have th: "even (n + m) = (even n \<longleftrightarrow> even m)" by arith
```
```   489   from evenperm_unique[OF n refl] evenperm_unique[OF m refl]
```
```   490     evenperm_unique[OF nm th]
```
```   491   show ?thesis by blast
```
```   492 qed
```
```   493
```
```   494 lemma evenperm_inv: assumes p: "permutation p"
```
```   495   shows "evenperm (inv p) = evenperm p"
```
```   496 proof-
```
```   497   from p obtain n where n: "swapidseq n p" unfolding permutation_def by blast
```
```   498   from evenperm_unique[OF swapidseq_inverse[OF n] evenperm_unique[OF n refl, symmetric]]
```
```   499   show ?thesis .
```
```   500 qed
```
```   501
```
```   502 (* ------------------------------------------------------------------------- *)
```
```   503 (* A more abstract characterization of permutations.                         *)
```
```   504 (* ------------------------------------------------------------------------- *)
```
```   505
```
```   506
```
```   507 lemma bij_iff: "bij f \<longleftrightarrow> (\<forall>x. \<exists>!y. f y = x)"
```
```   508   unfolding bij_def inj_on_def surj_def
```
```   509   apply auto
```
```   510   apply metis
```
```   511   apply metis
```
```   512   done
```
```   513
```
```   514 lemma permutation_bijective:
```
```   515   assumes p: "permutation p"
```
```   516   shows "bij p"
```
```   517 proof-
```
```   518   from p obtain n where n: "swapidseq n p" unfolding permutation_def by blast
```
```   519   from swapidseq_inverse_exists[OF n] obtain q where
```
```   520     q: "swapidseq n q" "p \<circ> q = id" "q \<circ> p = id" by blast
```
```   521   thus ?thesis unfolding bij_iff  apply (auto simp add: fun_eq_iff) apply metis done
```
```   522 qed
```
```   523
```
```   524 lemma permutation_finite_support: assumes p: "permutation p"
```
```   525   shows "finite {x. p x \<noteq> x}"
```
```   526 proof-
```
```   527   from p obtain n where n: "swapidseq n p" unfolding permutation_def by blast
```
```   528   from n show ?thesis
```
```   529   proof(induct n p rule: swapidseq.induct)
```
```   530     case id thus ?case by simp
```
```   531   next
```
```   532     case (comp_Suc n p a b)
```
```   533     let ?S = "insert a (insert b {x. p x \<noteq> x})"
```
```   534     from comp_Suc.hyps(2) have fS: "finite ?S" by simp
```
```   535     from `a \<noteq> b` have th: "{x. (Fun.swap a b id o p) x \<noteq> x} \<subseteq> ?S"
```
```   536       by (auto simp add: swap_def)
```
```   537     from finite_subset[OF th fS] show ?case  .
```
```   538 qed
```
```   539 qed
```
```   540
```
```   541 lemma bij_inv_eq_iff: "bij p ==> x = inv p y \<longleftrightarrow> p x = y"
```
```   542   using surj_f_inv_f[of p] inv_f_f[of f] by (auto simp add: bij_def)
```
```   543
```
```   544 lemma bij_swap_comp:
```
```   545   assumes bp: "bij p" shows "Fun.swap a b id o p = Fun.swap (inv p a) (inv p b) p"
```
```   546   using surj_f_inv_f[OF bij_is_surj[OF bp]]
```
```   547   by (simp add: fun_eq_iff swap_def bij_inv_eq_iff[OF bp])
```
```   548
```
```   549 lemma bij_swap_ompose_bij: "bij p \<Longrightarrow> bij (Fun.swap a b id o p)"
```
```   550 proof-
```
```   551   assume H: "bij p"
```
```   552   show ?thesis
```
```   553     unfolding bij_swap_comp[OF H] bij_swap_iff
```
```   554     using H .
```
```   555 qed
```
```   556
```
```   557 lemma permutation_lemma:
```
```   558   assumes fS: "finite S" and p: "bij p" and pS: "\<forall>x. x\<notin> S \<longrightarrow> p x = x"
```
```   559   shows "permutation p"
```
```   560 using fS p pS
```
```   561 proof(induct S arbitrary: p rule: finite_induct)
```
```   562   case (empty p) thus ?case by simp
```
```   563 next
```
```   564   case (insert a F p)
```
```   565   let ?r = "Fun.swap a (p a) id o p"
```
```   566   let ?q = "Fun.swap a (p a) id o ?r "
```
```   567   have raa: "?r a = a" by (simp add: swap_def)
```
```   568   from bij_swap_ompose_bij[OF insert(4)]
```
```   569   have br: "bij ?r"  .
```
```   570
```
```   571   from insert raa have th: "\<forall>x. x \<notin> F \<longrightarrow> ?r x = x"
```
```   572     apply (clarsimp simp add: swap_def)
```
```   573     apply (erule_tac x="x" in allE)
```
```   574     apply auto
```
```   575     unfolding bij_iff apply metis
```
```   576     done
```
```   577   from insert(3)[OF br th]
```
```   578   have rp: "permutation ?r" .
```
```   579   have "permutation ?q" by (simp add: permutation_compose permutation_swap_id rp)
```
```   580   thus ?case by (simp add: o_assoc)
```
```   581 qed
```
```   582
```
```   583 lemma permutation: "permutation p \<longleftrightarrow> bij p \<and> finite {x. p x \<noteq> x}"
```
```   584   (is "?lhs \<longleftrightarrow> ?b \<and> ?f")
```
```   585 proof
```
```   586   assume p: ?lhs
```
```   587   from p permutation_bijective permutation_finite_support show "?b \<and> ?f" by auto
```
```   588 next
```
```   589   assume bf: "?b \<and> ?f"
```
```   590   hence bf: "?f" "?b" by blast+
```
```   591   from permutation_lemma[OF bf] show ?lhs by blast
```
```   592 qed
```
```   593
```
```   594 lemma permutation_inverse_works: assumes p: "permutation p"
```
```   595   shows "inv p o p = id" "p o inv p = id"
```
```   596   using permutation_bijective [OF p]
```
```   597   unfolding bij_def inj_iff surj_iff by auto
```
```   598
```
```   599 lemma permutation_inverse_compose:
```
```   600   assumes p: "permutation p" and q: "permutation q"
```
```   601   shows "inv (p o q) = inv q o inv p"
```
```   602 proof-
```
```   603   note ps = permutation_inverse_works[OF p]
```
```   604   note qs = permutation_inverse_works[OF q]
```
```   605   have "p o q o (inv q o inv p) = p o (q o inv q) o inv p" by (simp add: o_assoc)
```
```   606   also have "\<dots> = id" by (simp add: ps qs)
```
```   607   finally have th0: "p o q o (inv q o inv p) = id" .
```
```   608   have "inv q o inv p o (p o q) = inv q o (inv p o p) o q" by (simp add: o_assoc)
```
```   609   also have "\<dots> = id" by (simp add: ps qs)
```
```   610   finally have th1: "inv q o inv p o (p o q) = id" .
```
```   611   from inv_unique_comp[OF th0 th1] show ?thesis .
```
```   612 qed
```
```   613
```
```   614 (* ------------------------------------------------------------------------- *)
```
```   615 (* Relation to "permutes".                                                   *)
```
```   616 (* ------------------------------------------------------------------------- *)
```
```   617
```
```   618 lemma permutation_permutes: "permutation p \<longleftrightarrow> (\<exists>S. finite S \<and> p permutes S)"
```
```   619 unfolding permutation permutes_def bij_iff[symmetric]
```
```   620 apply (rule iffI, clarify)
```
```   621 apply (rule exI[where x="{x. p x \<noteq> x}"])
```
```   622 apply simp
```
```   623 apply clarsimp
```
```   624 apply (rule_tac B="S" in finite_subset)
```
```   625 apply auto
```
```   626 done
```
```   627
```
```   628 (* ------------------------------------------------------------------------- *)
```
```   629 (* Hence a sort of induction principle composing by swaps.                   *)
```
```   630 (* ------------------------------------------------------------------------- *)
```
```   631
```
```   632 lemma permutes_induct: "finite S \<Longrightarrow>  P id  \<Longrightarrow> (\<And> a b p. a \<in> S \<Longrightarrow> b \<in> S \<Longrightarrow> P p \<Longrightarrow> P p \<Longrightarrow> permutation p ==> P (Fun.swap a b id o p))
```
```   633          ==> (\<And>p. p permutes S ==> P p)"
```
```   634 proof(induct S rule: finite_induct)
```
```   635   case empty thus ?case by auto
```
```   636 next
```
```   637   case (insert x F p)
```
```   638   let ?r = "Fun.swap x (p x) id o p"
```
```   639   let ?q = "Fun.swap x (p x) id o ?r"
```
```   640   have qp: "?q = p" by (simp add: o_assoc)
```
```   641   from permutes_insert_lemma[OF insert.prems(3)] insert have Pr: "P ?r" by blast
```
```   642   from permutes_in_image[OF insert.prems(3), of x]
```
```   643   have pxF: "p x \<in> insert x F" by simp
```
```   644   have xF: "x \<in> insert x F" by simp
```
```   645   have rp: "permutation ?r"
```
```   646     unfolding permutation_permutes using insert.hyps(1)
```
```   647       permutes_insert_lemma[OF insert.prems(3)] by blast
```
```   648   from insert.prems(2)[OF xF pxF Pr Pr rp]
```
```   649   show ?case  unfolding qp .
```
```   650 qed
```
```   651
```
```   652 (* ------------------------------------------------------------------------- *)
```
```   653 (* Sign of a permutation as a real number.                                   *)
```
```   654 (* ------------------------------------------------------------------------- *)
```
```   655
```
```   656 definition "sign p = (if evenperm p then (1::int) else -1)"
```
```   657
```
```   658 lemma sign_nz: "sign p \<noteq> 0" by (simp add: sign_def)
```
```   659 lemma sign_id: "sign id = 1" by (simp add: sign_def)
```
```   660 lemma sign_inverse: "permutation p ==> sign (inv p) = sign p"
```
```   661   by (simp add: sign_def evenperm_inv)
```
```   662 lemma sign_compose: "permutation p \<Longrightarrow> permutation q ==> sign (p o q) = sign(p) * sign(q)" by (simp add: sign_def evenperm_comp)
```
```   663 lemma sign_swap_id: "sign (Fun.swap a b id) = (if a = b then 1 else -1)"
```
```   664   by (simp add: sign_def evenperm_swap)
```
```   665 lemma sign_idempotent: "sign p * sign p = 1" by (simp add: sign_def)
```
```   666
```
```   667 (* ------------------------------------------------------------------------- *)
```
```   668 (* More lemmas about permutations.                                           *)
```
```   669 (* ------------------------------------------------------------------------- *)
```
```   670
```
```   671 lemma permutes_natset_le:
```
```   672   assumes p: "p permutes (S::'a::wellorder set)" and le: "\<forall>i \<in> S.  p i <= i" shows "p = id"
```
```   673 proof-
```
```   674   {fix n
```
```   675     have "p n = n"
```
```   676       using p le
```
```   677     proof(induct n arbitrary: S rule: less_induct)
```
```   678       fix n S assume H: "\<And>m S. \<lbrakk>m < n; p permutes S; \<forall>i\<in>S. p i \<le> i\<rbrakk> \<Longrightarrow> p m = m"
```
```   679         "p permutes S" "\<forall>i \<in>S. p i \<le> i"
```
```   680       {assume "n \<notin> S"
```
```   681         with H(2) have "p n = n" unfolding permutes_def by metis}
```
```   682       moreover
```
```   683       {assume ns: "n \<in> S"
```
```   684         from H(3)  ns have "p n < n \<or> p n = n" by auto
```
```   685         moreover{assume h: "p n < n"
```
```   686           from H h have "p (p n) = p n" by metis
```
```   687           with permutes_inj[OF H(2)] have "p n = n" unfolding inj_on_def by blast
```
```   688           with h have False by simp}
```
```   689         ultimately have "p n = n" by blast }
```
```   690       ultimately show "p n = n"  by blast
```
```   691     qed}
```
```   692   thus ?thesis by (auto simp add: fun_eq_iff)
```
```   693 qed
```
```   694
```
```   695 lemma permutes_natset_ge:
```
```   696   assumes p: "p permutes (S::'a::wellorder set)" and le: "\<forall>i \<in> S.  p i \<ge> i" shows "p = id"
```
```   697 proof-
```
```   698   {fix i assume i: "i \<in> S"
```
```   699     from i permutes_in_image[OF permutes_inv[OF p]] have "inv p i \<in> S" by simp
```
```   700     with le have "p (inv p i) \<ge> inv p i" by blast
```
```   701     with permutes_inverses[OF p] have "i \<ge> inv p i" by simp}
```
```   702   then have th: "\<forall>i\<in>S. inv p i \<le> i"  by blast
```
```   703   from permutes_natset_le[OF permutes_inv[OF p] th]
```
```   704   have "inv p = inv id" by simp
```
```   705   then show ?thesis
```
```   706     apply (subst permutes_inv_inv[OF p, symmetric])
```
```   707     apply (rule inv_unique_comp)
```
```   708     apply simp_all
```
```   709     done
```
```   710 qed
```
```   711
```
```   712 lemma image_inverse_permutations: "{inv p |p. p permutes S} = {p. p permutes S}"
```
```   713 apply (rule set_eqI)
```
```   714 apply auto
```
```   715   using permutes_inv_inv permutes_inv apply auto
```
```   716   apply (rule_tac x="inv x" in exI)
```
```   717   apply auto
```
```   718   done
```
```   719
```
```   720 lemma image_compose_permutations_left:
```
```   721   assumes q: "q permutes S" shows "{q o p | p. p permutes S} = {p . p permutes S}"
```
```   722 apply (rule set_eqI)
```
```   723 apply auto
```
```   724 apply (rule permutes_compose)
```
```   725 using q apply auto
```
```   726 apply (rule_tac x = "inv q o x" in exI)
```
```   727 by (simp add: o_assoc permutes_inv permutes_compose permutes_inv_o)
```
```   728
```
```   729 lemma image_compose_permutations_right:
```
```   730   assumes q: "q permutes S"
```
```   731   shows "{p o q | p. p permutes S} = {p . p permutes S}"
```
```   732 apply (rule set_eqI)
```
```   733 apply auto
```
```   734 apply (rule permutes_compose)
```
```   735 using q apply auto
```
```   736 apply (rule_tac x = "x o inv q" in exI)
```
```   737 by (simp add: o_assoc permutes_inv permutes_compose permutes_inv_o comp_assoc)
```
```   738
```
```   739 lemma permutes_in_seg: "p permutes {1 ..n} \<Longrightarrow> i \<in> {1..n} ==> 1 <= p i \<and> p i <= n"
```
```   740
```
```   741 apply (simp add: permutes_def)
```
```   742 apply metis
```
```   743 done
```
```   744
```
```   745 lemma setsum_permutations_inverse: "setsum f {p. p permutes S} = setsum (\<lambda>p. f(inv p)) {p. p permutes S}" (is "?lhs = ?rhs")
```
```   746 proof-
```
```   747   let ?S = "{p . p permutes S}"
```
```   748 have th0: "inj_on inv ?S"
```
```   749 proof(auto simp add: inj_on_def)
```
```   750   fix q r
```
```   751   assume q: "q permutes S" and r: "r permutes S" and qr: "inv q = inv r"
```
```   752   hence "inv (inv q) = inv (inv r)" by simp
```
```   753   with permutes_inv_inv[OF q] permutes_inv_inv[OF r]
```
```   754   show "q = r" by metis
```
```   755 qed
```
```   756   have th1: "inv ` ?S = ?S" using image_inverse_permutations by blast
```
```   757   have th2: "?rhs = setsum (f o inv) ?S" by (simp add: o_def)
```
```   758   from setsum_reindex[OF th0, of f]  show ?thesis unfolding th1 th2 .
```
```   759 qed
```
```   760
```
```   761 lemma setum_permutations_compose_left:
```
```   762   assumes q: "q permutes S"
```
```   763   shows "setsum f {p. p permutes S} =
```
```   764             setsum (\<lambda>p. f(q o p)) {p. p permutes S}" (is "?lhs = ?rhs")
```
```   765 proof-
```
```   766   let ?S = "{p. p permutes S}"
```
```   767   have th0: "?rhs = setsum (f o (op o q)) ?S" by (simp add: o_def)
```
```   768   have th1: "inj_on (op o q) ?S"
```
```   769     apply (auto simp add: inj_on_def)
```
```   770   proof-
```
```   771     fix p r
```
```   772     assume "p permutes S" and r:"r permutes S" and rp: "q \<circ> p = q \<circ> r"
```
```   773     hence "inv q o q o p = inv q o q o r" by (simp add: comp_assoc)
```
```   774     with permutes_inj[OF q, unfolded inj_iff]
```
```   775
```
```   776     show "p = r" by simp
```
```   777   qed
```
```   778   have th3: "(op o q) ` ?S = ?S" using image_compose_permutations_left[OF q] by auto
```
```   779   from setsum_reindex[OF th1, of f]
```
```   780   show ?thesis unfolding th0 th1 th3 .
```
```   781 qed
```
```   782
```
```   783 lemma sum_permutations_compose_right:
```
```   784   assumes q: "q permutes S"
```
```   785   shows "setsum f {p. p permutes S} =
```
```   786             setsum (\<lambda>p. f(p o q)) {p. p permutes S}" (is "?lhs = ?rhs")
```
```   787 proof-
```
```   788   let ?S = "{p. p permutes S}"
```
```   789   have th0: "?rhs = setsum (f o (\<lambda>p. p o q)) ?S" by (simp add: o_def)
```
```   790   have th1: "inj_on (\<lambda>p. p o q) ?S"
```
```   791     apply (auto simp add: inj_on_def)
```
```   792   proof-
```
```   793     fix p r
```
```   794     assume "p permutes S" and r:"r permutes S" and rp: "p o q = r o q"
```
```   795     hence "p o (q o inv q)  = r o (q o inv q)" by (simp add: o_assoc)
```
```   796     with permutes_surj[OF q, unfolded surj_iff]
```
```   797
```
```   798     show "p = r" by simp
```
```   799   qed
```
```   800   have th3: "(\<lambda>p. p o q) ` ?S = ?S" using image_compose_permutations_right[OF q] by auto
```
```   801   from setsum_reindex[OF th1, of f]
```
```   802   show ?thesis unfolding th0 th1 th3 .
```
```   803 qed
```
```   804
```
```   805 (* ------------------------------------------------------------------------- *)
```
```   806 (* Sum over a set of permutations (could generalize to iteration).           *)
```
```   807 (* ------------------------------------------------------------------------- *)
```
```   808
```
```   809 lemma setsum_over_permutations_insert:
```
```   810   assumes fS: "finite S" and aS: "a \<notin> S"
```
```   811   shows "setsum f {p. p permutes (insert a S)} = setsum (\<lambda>b. setsum (\<lambda>q. f (Fun.swap a b id o q)) {p. p permutes S}) (insert a S)"
```
```   812 proof-
```
```   813   have th0: "\<And>f a b. (\<lambda>(b,p). f (Fun.swap a b id o p)) = f o (\<lambda>(b,p). Fun.swap a b id o p)"
```
```   814     by (simp add: fun_eq_iff)
```
```   815   have th1: "\<And>P Q. P \<times> Q = {(a,b). a \<in> P \<and> b \<in> Q}" by blast
```
```   816   have th2: "\<And>P Q. P \<Longrightarrow> (P \<Longrightarrow> Q) \<Longrightarrow> P \<and> Q" by blast
```
```   817   show ?thesis
```
```   818     unfolding permutes_insert
```
```   819     unfolding setsum_cartesian_product
```
```   820     unfolding  th1[symmetric]
```
```   821     unfolding th0
```
```   822   proof(rule setsum_reindex)
```
```   823     let ?f = "(\<lambda>(b, y). Fun.swap a b id \<circ> y)"
```
```   824     let ?P = "{p. p permutes S}"
```
```   825     {fix b c p q assume b: "b \<in> insert a S" and c: "c \<in> insert a S"
```
```   826       and p: "p permutes S" and q: "q permutes S"
```
```   827       and eq: "Fun.swap a b id o p = Fun.swap a c id o q"
```
```   828       from p q aS have pa: "p a = a" and qa: "q a = a"
```
```   829         unfolding permutes_def by metis+
```
```   830       from eq have "(Fun.swap a b id o p) a  = (Fun.swap a c id o q) a" by simp
```
```   831       hence bc: "b = c"
```
```   832         by (simp add: permutes_def pa qa o_def fun_upd_def swap_def id_def cong del: if_weak_cong split: split_if_asm)
```
```   833       from eq[unfolded bc] have "(\<lambda>p. Fun.swap a c id o p) (Fun.swap a c id o p) = (\<lambda>p. Fun.swap a c id o p) (Fun.swap a c id o q)" by simp
```
```   834       hence "p = q" unfolding o_assoc swap_id_idempotent
```
```   835         by (simp add: o_def)
```
```   836       with bc have "b = c \<and> p = q" by blast
```
```   837     }
```
```   838     then show "inj_on ?f (insert a S \<times> ?P)"
```
```   839       unfolding inj_on_def
```
```   840       apply clarify by metis
```
```   841   qed
```
```   842 qed
```
```   843
```
```   844 end
```
```   845
```