src/HOL/Library/Permutations.thy
changeset 29840 cfab6a76aa13
child 30036 3a074e3a9a18
child 30240 5b25fee0362c
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Library/Permutations.thy	Mon Feb 09 16:42:15 2009 +0000
     1.3 @@ -0,0 +1,862 @@
     1.4 +(* Title:      Library/Permutations
     1.5 +   ID:         $Id: 
     1.6 +   Author:     Amine Chaieb, University of Cambridge
     1.7 +*)
     1.8 +
     1.9 +header {* Permutations, both general and specifically on finite sets.*}
    1.10 +
    1.11 +theory Permutations
    1.12 +imports Main Finite_Cartesian_Product Parity 
    1.13 +begin
    1.14 +
    1.15 +  (* Why should I import Main just to solve the Typerep problem! *)
    1.16 +
    1.17 +definition permutes (infixr "permutes" 41) where
    1.18 +  "(p permutes S) \<longleftrightarrow> (\<forall>x. x \<notin> S \<longrightarrow> p x = x) \<and> (\<forall>y. \<exists>!x. p x = y)"
    1.19 +
    1.20 +(* ------------------------------------------------------------------------- *)
    1.21 +(* Transpositions.                                                           *)
    1.22 +(* ------------------------------------------------------------------------- *)
    1.23 +
    1.24 +declare swap_self[simp]
    1.25 +lemma swapid_sym: "Fun.swap a b id = Fun.swap b a id" 
    1.26 +  by (auto simp add: expand_fun_eq swap_def fun_upd_def)
    1.27 +lemma swap_id_refl: "Fun.swap a a id = id" by simp
    1.28 +lemma swap_id_sym: "Fun.swap a b id = Fun.swap b a id"
    1.29 +  by (rule ext, simp add: swap_def)
    1.30 +lemma swap_id_idempotent[simp]: "Fun.swap a b id o Fun.swap a b id = id"
    1.31 +  by (rule ext, auto simp add: swap_def)
    1.32 +
    1.33 +lemma inv_unique_comp: assumes fg: "f o g = id" and gf: "g o f = id"
    1.34 +  shows "inv f = g"
    1.35 +  using fg gf inv_equality[of g f] by (auto simp add: expand_fun_eq)
    1.36 +
    1.37 +lemma inverse_swap_id: "inv (Fun.swap a b id) = Fun.swap a b id"
    1.38 +  by (rule inv_unique_comp, simp_all)
    1.39 +
    1.40 +lemma swap_id_eq: "Fun.swap a b id x = (if x = a then b else if x = b then a else x)"
    1.41 +  by (simp add: swap_def)
    1.42 +
    1.43 +(* ------------------------------------------------------------------------- *)
    1.44 +(* Basic consequences of the definition.                                     *)
    1.45 +(* ------------------------------------------------------------------------- *)
    1.46 +
    1.47 +lemma permutes_in_image: "p permutes S \<Longrightarrow> p x \<in> S \<longleftrightarrow> x \<in> S"
    1.48 +  unfolding permutes_def by metis
    1.49 +
    1.50 +lemma permutes_image: assumes pS: "p permutes S" shows "p ` S = S"
    1.51 +  using pS
    1.52 +  unfolding permutes_def 
    1.53 +  apply - 
    1.54 +  apply (rule set_ext) 
    1.55 +  apply (simp add: image_iff)
    1.56 +  apply metis
    1.57 +  done
    1.58 +
    1.59 +lemma permutes_inj: "p permutes S ==> inj p " 
    1.60 +  unfolding permutes_def inj_on_def by blast 
    1.61 +
    1.62 +lemma permutes_surj: "p permutes s ==> surj p" 
    1.63 +  unfolding permutes_def surj_def by metis 
    1.64 +
    1.65 +lemma permutes_inv_o: assumes pS: "p permutes S"
    1.66 +  shows " p o inv p = id"
    1.67 +  and "inv p o p = id"
    1.68 +  using permutes_inj[OF pS] permutes_surj[OF pS]
    1.69 +  unfolding inj_iff[symmetric] surj_iff[symmetric] by blast+
    1.70 +
    1.71 +
    1.72 +lemma permutes_inverses: 
    1.73 +  fixes p :: "'a \<Rightarrow> 'a"
    1.74 +  assumes pS: "p permutes S"
    1.75 +  shows "p (inv p x) = x"
    1.76 +  and "inv p (p x) = x"
    1.77 +  using permutes_inv_o[OF pS, unfolded expand_fun_eq o_def] by auto
    1.78 +
    1.79 +lemma permutes_subset: "p permutes S \<Longrightarrow> S \<subseteq> T ==> p permutes T"
    1.80 +  unfolding permutes_def by blast
    1.81 +
    1.82 +lemma permutes_empty[simp]: "p permutes {} \<longleftrightarrow> p = id"
    1.83 +  unfolding expand_fun_eq permutes_def apply simp by metis 
    1.84 +
    1.85 +lemma permutes_sing[simp]: "p permutes {a} \<longleftrightarrow> p = id"
    1.86 +  unfolding expand_fun_eq permutes_def apply simp by metis
    1.87 + 
    1.88 +lemma permutes_univ: "p permutes UNIV \<longleftrightarrow> (\<forall>y. \<exists>!x. p x = y)"
    1.89 +  unfolding permutes_def by simp
    1.90 +
    1.91 +lemma permutes_inv_eq: "p permutes S ==> inv p y = x \<longleftrightarrow> p x = y"
    1.92 +  unfolding permutes_def inv_def apply auto
    1.93 +  apply (erule allE[where x=y])
    1.94 +  apply (erule allE[where x=y])
    1.95 +  apply (rule someI_ex) apply blast
    1.96 +  apply (rule some1_equality)
    1.97 +  apply blast
    1.98 +  apply blast
    1.99 +  done
   1.100 +
   1.101 +lemma permutes_swap_id: "a \<in> S \<Longrightarrow> b \<in> S ==> Fun.swap a b id permutes S"
   1.102 +  unfolding permutes_def swap_def fun_upd_def  apply auto apply metis done
   1.103 +
   1.104 +lemma permutes_superset: "p permutes S \<Longrightarrow> (\<forall>x \<in> S - T. p x = x) \<Longrightarrow> p permutes T"
   1.105 +apply (simp add: Ball_def permutes_def Diff_iff) by metis
   1.106 +
   1.107 +(* ------------------------------------------------------------------------- *)
   1.108 +(* Group properties.                                                         *)
   1.109 +(* ------------------------------------------------------------------------- *)
   1.110 +
   1.111 +lemma permutes_id: "id permutes S" unfolding permutes_def by simp 
   1.112 +
   1.113 +lemma permutes_compose: "p permutes S \<Longrightarrow> q permutes S ==> q o p permutes S"
   1.114 +  unfolding permutes_def o_def by metis
   1.115 +
   1.116 +lemma permutes_inv: assumes pS: "p permutes S" shows "inv p permutes S"
   1.117 +  using pS unfolding permutes_def permutes_inv_eq[OF pS] by metis  
   1.118 +
   1.119 +lemma permutes_inv_inv: assumes pS: "p permutes S" shows "inv (inv p) = p"
   1.120 +  unfolding expand_fun_eq permutes_inv_eq[OF pS] permutes_inv_eq[OF permutes_inv[OF pS]]
   1.121 +  by blast
   1.122 +
   1.123 +(* ------------------------------------------------------------------------- *)
   1.124 +(* The number of permutations on a finite set.                               *)
   1.125 +(* ------------------------------------------------------------------------- *)
   1.126 +
   1.127 +lemma permutes_insert_lemma: 
   1.128 +  assumes pS: "p permutes (insert a S)"
   1.129 +  shows "Fun.swap a (p a) id o p permutes S"
   1.130 +  apply (rule permutes_superset[where S = "insert a S"])
   1.131 +  apply (rule permutes_compose[OF pS])
   1.132 +  apply (rule permutes_swap_id, simp)
   1.133 +  using permutes_in_image[OF pS, of a] apply simp
   1.134 +  apply (auto simp add: Ball_def Diff_iff swap_def)
   1.135 +  done
   1.136 +
   1.137 +lemma permutes_insert: "{p. p permutes (insert a S)} =
   1.138 +        (\<lambda>(b,p). Fun.swap a b id o p) ` {(b,p). b \<in> insert a S \<and> p \<in> {p. p permutes S}}"
   1.139 +proof-
   1.140 +
   1.141 +  {fix p 
   1.142 +    {assume pS: "p permutes insert a S"
   1.143 +      let ?b = "p a"
   1.144 +      let ?q = "Fun.swap a (p a) id o p"
   1.145 +      have th0: "p = Fun.swap a ?b id o ?q" unfolding expand_fun_eq o_assoc by simp 
   1.146 +      have th1: "?b \<in> insert a S " unfolding permutes_in_image[OF pS] by simp 
   1.147 +      from permutes_insert_lemma[OF pS] th0 th1
   1.148 +      have "\<exists> b q. p = Fun.swap a b id o q \<and> b \<in> insert a S \<and> q permutes S" by blast}
   1.149 +    moreover
   1.150 +    {fix b q assume bq: "p = Fun.swap a b id o q" "b \<in> insert a S" "q permutes S"
   1.151 +      from permutes_subset[OF bq(3), of "insert a S"] 
   1.152 +      have qS: "q permutes insert a S" by auto
   1.153 +      have aS: "a \<in> insert a S" by simp
   1.154 +      from bq(1) permutes_compose[OF qS permutes_swap_id[OF aS bq(2)]]
   1.155 +      have "p permutes insert a S"  by simp }
   1.156 +    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}
   1.157 +  thus ?thesis by auto
   1.158 +qed
   1.159 +
   1.160 +lemma hassize_insert: "a \<notin> F \<Longrightarrow> insert a F hassize n \<Longrightarrow> F hassize (n - 1)"
   1.161 +  by (auto simp add: hassize_def)
   1.162 +
   1.163 +lemma hassize_permutations: assumes Sn: "S hassize n"
   1.164 +  shows "{p. p permutes S} hassize (fact n)"
   1.165 +proof-
   1.166 +  from Sn have fS:"finite S" by (simp add: hassize_def)
   1.167 +
   1.168 +  have "\<forall>n. (S hassize n) \<longrightarrow> ({p. p permutes S} hassize (fact n))"
   1.169 +  proof(rule finite_induct[where F = S])
   1.170 +    from fS show "finite S" .
   1.171 +  next
   1.172 +    show "\<forall>n. ({} hassize n) \<longrightarrow> ({p. p permutes {}} hassize fact n)"
   1.173 +      by (simp add: hassize_def permutes_empty)
   1.174 +  next
   1.175 +    fix x F 
   1.176 +    assume fF: "finite F" and xF: "x \<notin> F" 
   1.177 +      and H: "\<forall>n. (F hassize n) \<longrightarrow> ({p. p permutes F} hassize fact n)"
   1.178 +    {fix n assume H0: "insert x F hassize n"
   1.179 +      let ?xF = "{p. p permutes insert x F}"
   1.180 +      let ?pF = "{p. p permutes F}"
   1.181 +      let ?pF' = "{(b, p). b \<in> insert x F \<and> p \<in> ?pF}"
   1.182 +      let ?g = "(\<lambda>(b, p). Fun.swap x b id \<circ> p)"
   1.183 +      from permutes_insert[of x F]
   1.184 +      have xfgpF': "?xF = ?g ` ?pF'" .
   1.185 +      from hassize_insert[OF xF H0] have Fs: "F hassize (n - 1)" .
   1.186 +      from H Fs have pFs: "?pF hassize fact (n - 1)" by blast
   1.187 +      hence pF'f: "finite ?pF'" using H0 unfolding hassize_def 
   1.188 +	apply (simp only: Collect_split Collect_mem_eq)
   1.189 +	apply (rule finite_cartesian_product)
   1.190 +	apply simp_all
   1.191 +	done
   1.192 +
   1.193 +      have ginj: "inj_on ?g ?pF'"
   1.194 +      proof-
   1.195 +	{
   1.196 +	  fix b p c q assume bp: "(b,p) \<in> ?pF'" and cq: "(c,q) \<in> ?pF'" 
   1.197 +	    and eq: "?g (b,p) = ?g (c,q)"
   1.198 +	  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
   1.199 +	  from ths(4) xF eq have "b = ?g (b,p) x" unfolding permutes_def 
   1.200 +	    by (auto simp add: swap_def fun_upd_def expand_fun_eq)
   1.201 +	  also have "\<dots> = ?g (c,q) x" using ths(5) xF eq  
   1.202 +	    by (auto simp add: swap_def fun_upd_def expand_fun_eq)
   1.203 +	  also have "\<dots> = c"using ths(5) xF unfolding permutes_def
   1.204 +	    by (auto simp add: swap_def fun_upd_def expand_fun_eq)
   1.205 +	  finally have bc: "b = c" .
   1.206 +	  hence "Fun.swap x b id = Fun.swap x c id" by simp
   1.207 +	  with eq have "Fun.swap x b id o p = Fun.swap x b id o q" by simp
   1.208 +	  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
   1.209 +	  hence "p = q" by (simp add: o_assoc)
   1.210 +	  with bc have "(b,p) = (c,q)" by simp }
   1.211 +	thus ?thesis  unfolding inj_on_def by blast
   1.212 +      qed
   1.213 +      from xF H0 have n0: "n \<noteq> 0 " by (auto simp add: hassize_def)
   1.214 +      hence "\<exists>m. n = Suc m" by arith
   1.215 +      then obtain m where n[simp]: "n = Suc m" by blast 
   1.216 +      from pFs H0 have xFc: "card ?xF = fact n" 
   1.217 +	unfolding xfgpF' card_image[OF ginj] hassize_def
   1.218 +	apply (simp only: Collect_split Collect_mem_eq card_cartesian_product)
   1.219 +	by simp
   1.220 +      from finite_imageI[OF pF'f, of ?g] have xFf: "finite ?xF" unfolding xfgpF' by simp 
   1.221 +      have "?xF hassize fact n"
   1.222 +	using xFf xFc 
   1.223 +	unfolding hassize_def  xFf by blast }
   1.224 +    thus "\<forall>n. (insert x F hassize n) \<longrightarrow> ({p. p permutes insert x F} hassize fact n)" 
   1.225 +      by blast
   1.226 +  qed
   1.227 +  with Sn show ?thesis by blast
   1.228 +qed
   1.229 +
   1.230 +lemma finite_permutations: "finite S ==> finite {p. p permutes S}"
   1.231 +  using hassize_permutations[of S] unfolding hassize_def by blast
   1.232 +
   1.233 +(* ------------------------------------------------------------------------- *)
   1.234 +(* Permutations of index set for iterated operations.                        *)
   1.235 +(* ------------------------------------------------------------------------- *)
   1.236 +
   1.237 +lemma (in ab_semigroup_mult) fold_image_permute: assumes fS: "finite S" and pS: "p permutes S" 
   1.238 +  shows "fold_image times f z S = fold_image times (f o p) z S"
   1.239 +  using fold_image_reindex[OF fS subset_inj_on[OF permutes_inj[OF pS], of S, simplified], of f z]
   1.240 +  unfolding permutes_image[OF pS] .
   1.241 +lemma (in ab_semigroup_add) fold_image_permute: assumes fS: "finite S" and pS: "p permutes S" 
   1.242 +  shows "fold_image plus f z S = fold_image plus (f o p) z S"
   1.243 +proof-
   1.244 +  interpret ab_semigroup_mult plus apply unfold_locales apply (simp add: add_assoc)
   1.245 +    apply (simp add: add_commute) done
   1.246 +  from fold_image_reindex[OF fS subset_inj_on[OF permutes_inj[OF pS], of S, simplified], of f z]
   1.247 +  show ?thesis
   1.248 +  unfolding permutes_image[OF pS] .
   1.249 +qed
   1.250 +
   1.251 +lemma setsum_permute: assumes pS: "p permutes S" 
   1.252 +  shows "setsum f S = setsum (f o p) S"
   1.253 +  unfolding setsum_def using fold_image_permute[of S p f 0] pS by clarsimp
   1.254 +
   1.255 +lemma setsum_permute_natseg:assumes pS: "p permutes {m .. n}" 
   1.256 +  shows "setsum f {m .. n} = setsum (f o p) {m .. n}"
   1.257 +  using setsum_permute[OF pS, of f ] pS by blast 
   1.258 +
   1.259 +lemma setprod_permute: assumes pS: "p permutes S" 
   1.260 +  shows "setprod f S = setprod (f o p) S"
   1.261 +  unfolding setprod_def 
   1.262 +  using ab_semigroup_mult_class.fold_image_permute[of S p f 1] pS by clarsimp
   1.263 +
   1.264 +lemma setprod_permute_natseg:assumes pS: "p permutes {m .. n}" 
   1.265 +  shows "setprod f {m .. n} = setprod (f o p) {m .. n}"
   1.266 +  using setprod_permute[OF pS, of f ] pS by blast 
   1.267 +
   1.268 +(* ------------------------------------------------------------------------- *)
   1.269 +(* Various combinations of transpositions with 2, 1 and 0 common elements.   *)
   1.270 +(* ------------------------------------------------------------------------- *)
   1.271 +
   1.272 +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: expand_fun_eq swap_def)
   1.273 +
   1.274 +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: expand_fun_eq swap_def)
   1.275 +
   1.276 +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"
   1.277 +  by (simp add: swap_def expand_fun_eq)
   1.278 +
   1.279 +(* ------------------------------------------------------------------------- *)
   1.280 +(* Permutations as transposition sequences.                                  *)
   1.281 +(* ------------------------------------------------------------------------- *)
   1.282 +
   1.283 +
   1.284 +inductive swapidseq :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> bool" where
   1.285 +  id[simp]: "swapidseq 0 id"
   1.286 +| comp_Suc: "swapidseq n p \<Longrightarrow> a \<noteq> b \<Longrightarrow> swapidseq (Suc n) (Fun.swap a b id o p)"
   1.287 +
   1.288 +declare id[unfolded id_def, simp]
   1.289 +definition "permutation p \<longleftrightarrow> (\<exists>n. swapidseq n p)"
   1.290 +
   1.291 +(* ------------------------------------------------------------------------- *)
   1.292 +(* Some closure properties of the set of permutations, with lengths.         *)
   1.293 +(* ------------------------------------------------------------------------- *)
   1.294 +
   1.295 +lemma permutation_id[simp]: "permutation id"unfolding permutation_def
   1.296 +  by (rule exI[where x=0], simp)
   1.297 +declare permutation_id[unfolded id_def, simp]
   1.298 +
   1.299 +lemma swapidseq_swap: "swapidseq (if a = b then 0 else 1) (Fun.swap a b id)"
   1.300 +  apply clarsimp
   1.301 +  using comp_Suc[of 0 id a b] by simp
   1.302 +
   1.303 +lemma permutation_swap_id: "permutation (Fun.swap a b id)"
   1.304 +  apply (cases "a=b", simp_all)
   1.305 +  unfolding permutation_def using swapidseq_swap[of a b] by blast 
   1.306 +
   1.307 +lemma swapidseq_comp_add: "swapidseq n p \<Longrightarrow> swapidseq m q ==> swapidseq (n + m) (p o q)"
   1.308 +  proof (induct n p arbitrary: m q rule: swapidseq.induct)
   1.309 +    case (id m q) thus ?case by simp
   1.310 +  next
   1.311 +    case (comp_Suc n p a b m q) 
   1.312 +    have th: "Suc n + m = Suc (n + m)" by arith
   1.313 +    show ?case unfolding th o_assoc[symmetric] 
   1.314 +      apply (rule swapidseq.comp_Suc) using comp_Suc.hyps(2)[OF comp_Suc.prems]  comp_Suc.hyps(3) by blast+ 
   1.315 +qed
   1.316 +
   1.317 +lemma permutation_compose: "permutation p \<Longrightarrow> permutation q ==> permutation(p o q)"
   1.318 +  unfolding permutation_def using swapidseq_comp_add[of _ p _ q] by metis
   1.319 +
   1.320 +lemma swapidseq_endswap: "swapidseq n p \<Longrightarrow> a \<noteq> b ==> swapidseq (Suc n) (p o Fun.swap a b id)"
   1.321 +  apply (induct n p rule: swapidseq.induct)
   1.322 +  using swapidseq_swap[of a b]
   1.323 +  by (auto simp add: o_assoc[symmetric] intro: swapidseq.comp_Suc)
   1.324 +
   1.325 +lemma swapidseq_inverse_exists: "swapidseq n p ==> \<exists>q. swapidseq n q \<and> p o q = id \<and> q o p = id"
   1.326 +proof(induct n p rule: swapidseq.induct)
   1.327 +  case id  thus ?case by (rule exI[where x=id], simp)
   1.328 +next 
   1.329 +  case (comp_Suc n p a b)
   1.330 +  from comp_Suc.hyps obtain q where q: "swapidseq n q" "p \<circ> q = id" "q \<circ> p = id" by blast
   1.331 +  let ?q = "q o Fun.swap a b id"
   1.332 +  note H = comp_Suc.hyps
   1.333 +  from swapidseq_swap[of a b] H(3)  have th0: "swapidseq 1 (Fun.swap a b id)" by simp
   1.334 +  from swapidseq_comp_add[OF q(1) th0] have th1:"swapidseq (Suc n) ?q" by simp 
   1.335 +  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)
   1.336 +  also have "\<dots> = id" by (simp add: q(2))
   1.337 +  finally have th2: "Fun.swap a b id o p o ?q = id" .
   1.338 +  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) 
   1.339 +  hence "?q \<circ> (Fun.swap a b id \<circ> p) = id" by (simp add: q(3))
   1.340 +  with th1 th2 show ?case by blast
   1.341 +qed
   1.342 +
   1.343 +
   1.344 +lemma swapidseq_inverse: assumes H: "swapidseq n p" shows "swapidseq n (inv p)"
   1.345 +  using swapidseq_inverse_exists[OF H] inv_unique_comp[of p] by auto
   1.346 +
   1.347 +lemma permutation_inverse: "permutation p ==> permutation (inv p)"
   1.348 +  using permutation_def swapidseq_inverse by blast
   1.349 +
   1.350 +(* ------------------------------------------------------------------------- *)
   1.351 +(* The identity map only has even transposition sequences.                   *)
   1.352 +(* ------------------------------------------------------------------------- *)
   1.353 +
   1.354 +lemma symmetry_lemma:"(\<And>a b c d. P a b c d ==> P a b d c) \<Longrightarrow>
   1.355 +   (\<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)
   1.356 +   ==> (\<And>a b c d. a \<noteq> b --> c \<noteq> d \<longrightarrow>  P a b c d)" by metis
   1.357 +
   1.358 +lemma swap_general: "a \<noteq> b \<Longrightarrow> c \<noteq> d \<Longrightarrow> Fun.swap a b id o Fun.swap c d id = id \<or> 
   1.359 +  (\<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)" 
   1.360 +proof-
   1.361 +  assume H: "a\<noteq>b" "c\<noteq>d"
   1.362 +have "a \<noteq> b \<longrightarrow> c \<noteq> d \<longrightarrow> 
   1.363 +(  Fun.swap a b id o Fun.swap c d id = id \<or> 
   1.364 +  (\<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))" 
   1.365 +  apply (rule symmetry_lemma[where a=a and b=b and c=c and d=d])
   1.366 +  apply (simp_all only: swapid_sym) 
   1.367 +  apply (case_tac "a = c \<and> b = d", clarsimp simp only: swapid_sym swap_id_idempotent)
   1.368 +  apply (case_tac "a = c \<and> b \<noteq> d")
   1.369 +  apply (rule disjI2)
   1.370 +  apply (rule_tac x="b" in exI)
   1.371 +  apply (rule_tac x="d" in exI)
   1.372 +  apply (rule_tac x="b" in exI)
   1.373 +  apply (clarsimp simp add: expand_fun_eq swap_def)
   1.374 +  apply (case_tac "a \<noteq> c \<and> b = d")
   1.375 +  apply (rule disjI2)
   1.376 +  apply (rule_tac x="c" in exI)
   1.377 +  apply (rule_tac x="d" in exI)
   1.378 +  apply (rule_tac x="c" in exI)
   1.379 +  apply (clarsimp simp add: expand_fun_eq swap_def)
   1.380 +  apply (rule disjI2)
   1.381 +  apply (rule_tac x="c" in exI)
   1.382 +  apply (rule_tac x="d" in exI)
   1.383 +  apply (rule_tac x="b" in exI)
   1.384 +  apply (clarsimp simp add: expand_fun_eq swap_def)
   1.385 +  done
   1.386 +with H show ?thesis by metis 
   1.387 +qed
   1.388 +
   1.389 +lemma swapidseq_id_iff[simp]: "swapidseq 0 p \<longleftrightarrow> p = id"
   1.390 +  using swapidseq.cases[of 0 p "p = id"]
   1.391 +  by auto
   1.392 +
   1.393 +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))"
   1.394 +  apply (rule iffI)
   1.395 +  apply (erule swapidseq.cases[of n p])
   1.396 +  apply simp
   1.397 +  apply (rule disjI2)
   1.398 +  apply (rule_tac x= "a" in exI)
   1.399 +  apply (rule_tac x= "b" in exI)
   1.400 +  apply (rule_tac x= "pa" in exI)
   1.401 +  apply (rule_tac x= "na" in exI)
   1.402 +  apply simp
   1.403 +  apply auto
   1.404 +  apply (rule comp_Suc, simp_all)
   1.405 +  done
   1.406 +lemma fixing_swapidseq_decrease:
   1.407 +  assumes spn: "swapidseq n p" and ab: "a\<noteq>b" and pa: "(Fun.swap a b id o p) a = a"
   1.408 +  shows "n \<noteq> 0 \<and> swapidseq (n - 1) (Fun.swap a b id o p)"
   1.409 +  using spn ab pa
   1.410 +proof(induct n arbitrary: p a b)
   1.411 +  case 0 thus ?case by (auto simp add: swap_def fun_upd_def)
   1.412 +next
   1.413 +  case (Suc n p a b)
   1.414 +  from Suc.prems(1) swapidseq_cases[of "Suc n" p] obtain
   1.415 +    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"
   1.416 +    by auto
   1.417 +  {assume H: "Fun.swap a b id o Fun.swap c d id = id"
   1.418 +    
   1.419 +    have ?case apply (simp only: cdqm o_assoc H) 
   1.420 +      by (simp add: cdqm)}
   1.421 +  moreover
   1.422 +  { fix x y z
   1.423 +    assume H: "x\<noteq>a" "y\<noteq>a" "z \<noteq>a" "x \<noteq>y" 
   1.424 +      "Fun.swap a b id o Fun.swap c d id = Fun.swap x y id o Fun.swap a z id"
   1.425 +    from H have az: "a \<noteq> z" by simp
   1.426 +
   1.427 +    {fix h have "(Fun.swap x y id o h) a = a \<longleftrightarrow> h a = a"
   1.428 +      using H by (simp add: swap_def)}
   1.429 +    note th3 = this
   1.430 +    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
   1.431 +    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)
   1.432 +    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
   1.433 +    hence "(Fun.swap x y id o (Fun.swap a z id o q)) a  = a" unfolding Suc by metis
   1.434 +    hence th1: "(Fun.swap a z id o q) a = a" unfolding th3 .
   1.435 +    from Suc.hyps[OF cdqm(3)[ unfolded cdqm(5)[symmetric]] az th1]
   1.436 +    have th2: "swapidseq (n - 1) (Fun.swap a z id o q)" "n \<noteq> 0" by blast+
   1.437 +    have th: "Suc n - 1 = Suc (n - 1)" using th2(2) by auto 
   1.438 +    have ?case unfolding cdqm(2) H o_assoc th
   1.439 +      apply (simp only: Suc_not_Zero simp_thms o_assoc[symmetric])
   1.440 +      apply (rule comp_Suc)
   1.441 +      using th2 H apply blast+
   1.442 +      done}
   1.443 +  ultimately show ?case using swap_general[OF Suc.prems(2) cdqm(4)] by metis 
   1.444 +qed
   1.445 +
   1.446 +lemma swapidseq_identity_even: 
   1.447 +  assumes "swapidseq n (id :: 'a \<Rightarrow> 'a)" shows "even n"
   1.448 +  using `swapidseq n id`
   1.449 +proof(induct n rule: nat_less_induct)
   1.450 +  fix n
   1.451 +  assume H: "\<forall>m<n. swapidseq m (id::'a \<Rightarrow> 'a) \<longrightarrow> even m" "swapidseq n (id :: 'a \<Rightarrow> 'a)"
   1.452 +  {assume "n = 0" hence "even n" by arith} 
   1.453 +  moreover 
   1.454 +  {fix a b :: 'a and q m
   1.455 +    assume h: "n = Suc m" "(id :: 'a \<Rightarrow> 'a) = Fun.swap a b id \<circ> q" "swapidseq m q" "a \<noteq> b"
   1.456 +    from fixing_swapidseq_decrease[OF h(3,4), unfolded h(2)[symmetric]]
   1.457 +    have m: "m \<noteq> 0" "swapidseq (m - 1) (id :: 'a \<Rightarrow> 'a)" by auto
   1.458 +    from h m have mn: "m - 1 < n" by arith
   1.459 +    from H(1)[rule_format, OF mn m(2)] h(1) m(1) have "even n" apply arith done}
   1.460 +  ultimately show "even n" using H(2)[unfolded swapidseq_cases[of n id]] by auto
   1.461 +qed
   1.462 +
   1.463 +(* ------------------------------------------------------------------------- *)
   1.464 +(* Therefore we have a welldefined notion of parity.                         *)
   1.465 +(* ------------------------------------------------------------------------- *)
   1.466 +
   1.467 +definition "evenperm p = even (SOME n. swapidseq n p)"
   1.468 +
   1.469 +lemma swapidseq_even_even: assumes 
   1.470 +  m: "swapidseq m p" and n: "swapidseq n p"
   1.471 +  shows "even m \<longleftrightarrow> even n"
   1.472 +proof-
   1.473 +  from swapidseq_inverse_exists[OF n]
   1.474 +  obtain q where q: "swapidseq n q" "p \<circ> q = id" "q \<circ> p = id" by blast
   1.475 +  
   1.476 +  from swapidseq_identity_even[OF swapidseq_comp_add[OF m q(1), unfolded q]]
   1.477 +  show ?thesis by arith
   1.478 +qed
   1.479 +
   1.480 +lemma evenperm_unique: assumes p: "swapidseq n p" and n:"even n = b"
   1.481 +  shows "evenperm p = b"
   1.482 +  unfolding n[symmetric] evenperm_def
   1.483 +  apply (rule swapidseq_even_even[where p = p])
   1.484 +  apply (rule someI[where x = n])
   1.485 +  using p by blast+
   1.486 +
   1.487 +(* ------------------------------------------------------------------------- *)
   1.488 +(* And it has the expected composition properties.                           *)
   1.489 +(* ------------------------------------------------------------------------- *)
   1.490 +
   1.491 +lemma evenperm_id[simp]: "evenperm id = True"
   1.492 +  apply (rule evenperm_unique[where n = 0]) by simp_all
   1.493 +
   1.494 +lemma evenperm_swap: "evenperm (Fun.swap a b id) = (a = b)"
   1.495 +apply (rule evenperm_unique[where n="if a = b then 0 else 1"])
   1.496 +by (simp_all add: swapidseq_swap)
   1.497 +
   1.498 +lemma evenperm_comp: 
   1.499 +  assumes p: "permutation p" and q:"permutation q"
   1.500 +  shows "evenperm (p o q) = (evenperm p = evenperm q)"
   1.501 +proof-
   1.502 +  from p q obtain 
   1.503 +    n m where n: "swapidseq n p" and m: "swapidseq m q" 
   1.504 +    unfolding permutation_def by blast
   1.505 +  note nm =  swapidseq_comp_add[OF n m]
   1.506 +  have th: "even (n + m) = (even n \<longleftrightarrow> even m)" by arith
   1.507 +  from evenperm_unique[OF n refl] evenperm_unique[OF m refl]
   1.508 +    evenperm_unique[OF nm th]
   1.509 +  show ?thesis by blast
   1.510 +qed
   1.511 +
   1.512 +lemma evenperm_inv: assumes p: "permutation p"
   1.513 +  shows "evenperm (inv p) = evenperm p"
   1.514 +proof-
   1.515 +  from p obtain n where n: "swapidseq n p" unfolding permutation_def by blast
   1.516 +  from evenperm_unique[OF swapidseq_inverse[OF n] evenperm_unique[OF n refl, symmetric]]
   1.517 +  show ?thesis .
   1.518 +qed
   1.519 +
   1.520 +(* ------------------------------------------------------------------------- *)
   1.521 +(* A more abstract characterization of permutations.                         *)
   1.522 +(* ------------------------------------------------------------------------- *)
   1.523 +
   1.524 +
   1.525 +lemma bij_iff: "bij f \<longleftrightarrow> (\<forall>x. \<exists>!y. f y = x)"
   1.526 +  unfolding bij_def inj_on_def surj_def
   1.527 +  apply auto
   1.528 +  apply metis
   1.529 +  apply metis
   1.530 +  done
   1.531 +
   1.532 +lemma permutation_bijective: 
   1.533 +  assumes p: "permutation p" 
   1.534 +  shows "bij p"
   1.535 +proof-
   1.536 +  from p obtain n where n: "swapidseq n p" unfolding permutation_def by blast
   1.537 +  from swapidseq_inverse_exists[OF n] obtain q where 
   1.538 +    q: "swapidseq n q" "p \<circ> q = id" "q \<circ> p = id" by blast
   1.539 +  thus ?thesis unfolding bij_iff  apply (auto simp add: expand_fun_eq) apply metis done
   1.540 +qed  
   1.541 +
   1.542 +lemma permutation_finite_support: assumes p: "permutation p"
   1.543 +  shows "finite {x. p x \<noteq> x}"
   1.544 +proof-
   1.545 +  from p obtain n where n: "swapidseq n p" unfolding permutation_def by blast
   1.546 +  from n show ?thesis
   1.547 +  proof(induct n p rule: swapidseq.induct)
   1.548 +    case id thus ?case by simp
   1.549 +  next
   1.550 +    case (comp_Suc n p a b)
   1.551 +    let ?S = "insert a (insert b {x. p x \<noteq> x})"
   1.552 +    from comp_Suc.hyps(2) have fS: "finite ?S" by simp
   1.553 +    from `a \<noteq> b` have th: "{x. (Fun.swap a b id o p) x \<noteq> x} \<subseteq> ?S"
   1.554 +      by (auto simp add: swap_def)
   1.555 +    from finite_subset[OF th fS] show ?case  .
   1.556 +qed
   1.557 +qed
   1.558 +
   1.559 +lemma bij_inv_eq_iff: "bij p ==> x = inv p y \<longleftrightarrow> p x = y"
   1.560 +  using surj_f_inv_f[of p] inv_f_f[of f] by (auto simp add: bij_def)
   1.561 +
   1.562 +lemma bij_swap_comp: 
   1.563 +  assumes bp: "bij p" shows "Fun.swap a b id o p = Fun.swap (inv p a) (inv p b) p"
   1.564 +  using surj_f_inv_f[OF bij_is_surj[OF bp]]
   1.565 +  by (simp add: expand_fun_eq swap_def bij_inv_eq_iff[OF bp])
   1.566 +
   1.567 +lemma bij_swap_ompose_bij: "bij p \<Longrightarrow> bij (Fun.swap a b id o p)"
   1.568 +proof-
   1.569 +  assume H: "bij p"
   1.570 +  show ?thesis 
   1.571 +    unfolding bij_swap_comp[OF H] bij_swap_iff
   1.572 +    using H .
   1.573 +qed
   1.574 +
   1.575 +lemma permutation_lemma: 
   1.576 +  assumes fS: "finite S" and p: "bij p" and pS: "\<forall>x. x\<notin> S \<longrightarrow> p x = x"
   1.577 +  shows "permutation p"
   1.578 +using fS p pS
   1.579 +proof(induct S arbitrary: p rule: finite_induct)
   1.580 +  case (empty p) thus ?case by simp
   1.581 +next
   1.582 +  case (insert a F p)
   1.583 +  let ?r = "Fun.swap a (p a) id o p"
   1.584 +  let ?q = "Fun.swap a (p a) id o ?r "
   1.585 +  have raa: "?r a = a" by (simp add: swap_def)
   1.586 +  from bij_swap_ompose_bij[OF insert(4)]
   1.587 +  have br: "bij ?r"  . 
   1.588 +  
   1.589 +  from insert raa have th: "\<forall>x. x \<notin> F \<longrightarrow> ?r x = x"    
   1.590 +    apply (clarsimp simp add: swap_def)
   1.591 +    apply (erule_tac x="x" in allE)
   1.592 +    apply auto
   1.593 +    unfolding bij_iff apply metis
   1.594 +    done
   1.595 +  from insert(3)[OF br th]
   1.596 +  have rp: "permutation ?r" .
   1.597 +  have "permutation ?q" by (simp add: permutation_compose permutation_swap_id rp)
   1.598 +  thus ?case by (simp add: o_assoc)
   1.599 +qed
   1.600 +
   1.601 +lemma permutation: "permutation p \<longleftrightarrow> bij p \<and> finite {x. p x \<noteq> x}" 
   1.602 +  (is "?lhs \<longleftrightarrow> ?b \<and> ?f")
   1.603 +proof
   1.604 +  assume p: ?lhs
   1.605 +  from p permutation_bijective permutation_finite_support show "?b \<and> ?f" by auto
   1.606 +next
   1.607 +  assume bf: "?b \<and> ?f"
   1.608 +  hence bf: "?f" "?b" by blast+
   1.609 +  from permutation_lemma[OF bf] show ?lhs by blast
   1.610 +qed
   1.611 +
   1.612 +lemma permutation_inverse_works: assumes p: "permutation p"
   1.613 +  shows "inv p o p = id" "p o inv p = id"
   1.614 +using permutation_bijective[OF p] surj_iff bij_def inj_iff by auto
   1.615 +
   1.616 +lemma permutation_inverse_compose:
   1.617 +  assumes p: "permutation p" and q: "permutation q"
   1.618 +  shows "inv (p o q) = inv q o inv p"
   1.619 +proof-
   1.620 +  note ps = permutation_inverse_works[OF p]
   1.621 +  note qs = permutation_inverse_works[OF q]
   1.622 +  have "p o q o (inv q o inv p) = p o (q o inv q) o inv p" by (simp add: o_assoc)
   1.623 +  also have "\<dots> = id" by (simp add: ps qs)
   1.624 +  finally have th0: "p o q o (inv q o inv p) = id" .
   1.625 +  have "inv q o inv p o (p o q) = inv q o (inv p o p) o q" by (simp add: o_assoc)
   1.626 +  also have "\<dots> = id" by (simp add: ps qs)
   1.627 +  finally have th1: "inv q o inv p o (p o q) = id" . 
   1.628 +  from inv_unique_comp[OF th0 th1] show ?thesis .
   1.629 +qed
   1.630 +
   1.631 +(* ------------------------------------------------------------------------- *)
   1.632 +(* Relation to "permutes".                                                   *)
   1.633 +(* ------------------------------------------------------------------------- *)
   1.634 +
   1.635 +lemma permutation_permutes: "permutation p \<longleftrightarrow> (\<exists>S. finite S \<and> p permutes S)"
   1.636 +unfolding permutation permutes_def bij_iff[symmetric]
   1.637 +apply (rule iffI, clarify)
   1.638 +apply (rule exI[where x="{x. p x \<noteq> x}"])
   1.639 +apply simp
   1.640 +apply clarsimp
   1.641 +apply (rule_tac B="S" in finite_subset)
   1.642 +apply auto
   1.643 +done
   1.644 +
   1.645 +(* ------------------------------------------------------------------------- *)
   1.646 +(* Hence a sort of induction principle composing by swaps.                   *)
   1.647 +(* ------------------------------------------------------------------------- *)
   1.648 +
   1.649 +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))
   1.650 +         ==> (\<And>p. p permutes S ==> P p)"
   1.651 +proof(induct S rule: finite_induct)
   1.652 +  case empty thus ?case by auto
   1.653 +next 
   1.654 +  case (insert x F p)
   1.655 +  let ?r = "Fun.swap x (p x) id o p"
   1.656 +  let ?q = "Fun.swap x (p x) id o ?r"
   1.657 +  have qp: "?q = p" by (simp add: o_assoc)
   1.658 +  from permutes_insert_lemma[OF insert.prems(3)] insert have Pr: "P ?r" by blast
   1.659 +  from permutes_in_image[OF insert.prems(3), of x] 
   1.660 +  have pxF: "p x \<in> insert x F" by simp
   1.661 +  have xF: "x \<in> insert x F" by simp
   1.662 +  have rp: "permutation ?r"
   1.663 +    unfolding permutation_permutes using insert.hyps(1) 
   1.664 +      permutes_insert_lemma[OF insert.prems(3)] by blast
   1.665 +  from insert.prems(2)[OF xF pxF Pr Pr rp] 
   1.666 +  show ?case  unfolding qp . 
   1.667 +qed
   1.668 +
   1.669 +(* ------------------------------------------------------------------------- *)
   1.670 +(* Sign of a permutation as a real number.                                   *)
   1.671 +(* ------------------------------------------------------------------------- *)
   1.672 +
   1.673 +definition "sign p = (if evenperm p then (1::int) else -1)"
   1.674 +
   1.675 +lemma sign_nz: "sign p \<noteq> 0" by (simp add: sign_def) 
   1.676 +lemma sign_id: "sign id = 1" by (simp add: sign_def)
   1.677 +lemma sign_inverse: "permutation p ==> sign (inv p) = sign p"
   1.678 +  by (simp add: sign_def evenperm_inv)
   1.679 +lemma sign_compose: "permutation p \<Longrightarrow> permutation q ==> sign (p o q) = sign(p) * sign(q)" by (simp add: sign_def evenperm_comp)
   1.680 +lemma sign_swap_id: "sign (Fun.swap a b id) = (if a = b then 1 else -1)"
   1.681 +  by (simp add: sign_def evenperm_swap)
   1.682 +lemma sign_idempotent: "sign p * sign p = 1" by (simp add: sign_def)
   1.683 +
   1.684 +(* ------------------------------------------------------------------------- *)
   1.685 +(* More lemmas about permutations.                                           *)
   1.686 +(* ------------------------------------------------------------------------- *)
   1.687 +
   1.688 +lemma permutes_natset_le:
   1.689 +  assumes p: "p permutes (S:: nat set)" and le: "\<forall>i \<in> S.  p i <= i" shows "p = id"
   1.690 +proof-
   1.691 +  {fix n
   1.692 +    have "p n = n" 
   1.693 +      using p le
   1.694 +    proof(induct n arbitrary: S rule: nat_less_induct)
   1.695 +      fix n S assume H: "\<forall> m< n. \<forall>S. p permutes S \<longrightarrow> (\<forall>i\<in>S. p i \<le> i) \<longrightarrow> p m = m" 
   1.696 +	"p permutes S" "\<forall>i \<in>S. p i \<le> i"
   1.697 +      {assume "n \<notin> S"
   1.698 +	with H(2) have "p n = n" unfolding permutes_def by metis}
   1.699 +      moreover
   1.700 +      {assume ns: "n \<in> S"
   1.701 +	from H(3)  ns have "p n < n \<or> p n = n" by auto 
   1.702 +	moreover{assume h: "p n < n"
   1.703 +	  from H h have "p (p n) = p n" by metis
   1.704 +	  with permutes_inj[OF H(2)] have "p n = n" unfolding inj_on_def by blast
   1.705 +	  with h have False by arith}
   1.706 +	ultimately have "p n = n" by blast }
   1.707 +      ultimately show "p n = n"  by blast
   1.708 +    qed}
   1.709 +  thus ?thesis by (auto simp add: expand_fun_eq)
   1.710 +qed
   1.711 +
   1.712 +lemma permutes_natset_ge:
   1.713 +  assumes p: "p permutes (S:: nat set)" and le: "\<forall>i \<in> S.  p i \<ge> i" shows "p = id"
   1.714 +proof-
   1.715 +  {fix i assume i: "i \<in> S"
   1.716 +    from i permutes_in_image[OF permutes_inv[OF p]] have "inv p i \<in> S" by simp
   1.717 +    with le have "p (inv p i) \<ge> inv p i" by blast
   1.718 +    with permutes_inverses[OF p] have "i \<ge> inv p i" by simp}
   1.719 +  then have th: "\<forall>i\<in>S. inv p i \<le> i"  by blast
   1.720 +  from permutes_natset_le[OF permutes_inv[OF p] th] 
   1.721 +  have "inv p = inv id" by simp
   1.722 +  then show ?thesis 
   1.723 +    apply (subst permutes_inv_inv[OF p, symmetric])
   1.724 +    apply (rule inv_unique_comp)
   1.725 +    apply simp_all
   1.726 +    done
   1.727 +qed
   1.728 +
   1.729 +lemma image_inverse_permutations: "{inv p |p. p permutes S} = {p. p permutes S}"
   1.730 +apply (rule set_ext)
   1.731 +apply auto
   1.732 +  using permutes_inv_inv permutes_inv apply auto
   1.733 +  apply (rule_tac x="inv x" in exI)
   1.734 +  apply auto
   1.735 +  done
   1.736 +
   1.737 +lemma image_compose_permutations_left: 
   1.738 +  assumes q: "q permutes S" shows "{q o p | p. p permutes S} = {p . p permutes S}"
   1.739 +apply (rule set_ext)
   1.740 +apply auto
   1.741 +apply (rule permutes_compose)
   1.742 +using q apply auto
   1.743 +apply (rule_tac x = "inv q o x" in exI)
   1.744 +by (simp add: o_assoc permutes_inv permutes_compose permutes_inv_o)
   1.745 +
   1.746 +lemma image_compose_permutations_right:
   1.747 +  assumes q: "q permutes S"
   1.748 +  shows "{p o q | p. p permutes S} = {p . p permutes S}"
   1.749 +apply (rule set_ext)
   1.750 +apply auto
   1.751 +apply (rule permutes_compose)
   1.752 +using q apply auto
   1.753 +apply (rule_tac x = "x o inv q" in exI)
   1.754 +by (simp add: o_assoc permutes_inv permutes_compose permutes_inv_o o_assoc[symmetric])
   1.755 +
   1.756 +lemma permutes_in_seg: "p permutes {1 ..n} \<Longrightarrow> i \<in> {1..n} ==> 1 <= p i \<and> p i <= n"
   1.757 +
   1.758 +apply (simp add: permutes_def)
   1.759 +apply metis
   1.760 +done
   1.761 +
   1.762 +term setsum
   1.763 +lemma setsum_permutations_inverse: "setsum f {p. p permutes {m..n}} = setsum (\<lambda>p. f(inv p)) {p. p permutes {m..n}}" (is "?lhs = ?rhs")
   1.764 +proof-
   1.765 +  let ?S = "{p . p permutes {m .. n}}"
   1.766 +have th0: "inj_on inv ?S" 
   1.767 +proof(auto simp add: inj_on_def)
   1.768 +  fix q r
   1.769 +  assume q: "q permutes {m .. n}" and r: "r permutes {m .. n}" and qr: "inv q = inv r"
   1.770 +  hence "inv (inv q) = inv (inv r)" by simp
   1.771 +  with permutes_inv_inv[OF q] permutes_inv_inv[OF r]
   1.772 +  show "q = r" by metis
   1.773 +qed
   1.774 +  have th1: "inv ` ?S = ?S" using image_inverse_permutations by blast
   1.775 +  have th2: "?rhs = setsum (f o inv) ?S" by (simp add: o_def)
   1.776 +  from setsum_reindex[OF th0, of f]  show ?thesis unfolding th1 th2 .
   1.777 +qed
   1.778 +
   1.779 +lemma setum_permutations_compose_left:
   1.780 +  assumes q: "q permutes {m..n}"
   1.781 +  shows "setsum f {p. p permutes {m..n}} =
   1.782 +            setsum (\<lambda>p. f(q o p)) {p. p permutes {m..n}}" (is "?lhs = ?rhs")
   1.783 +proof-
   1.784 +  let ?S = "{p. p permutes {m..n}}"
   1.785 +  have th0: "?rhs = setsum (f o (op o q)) ?S" by (simp add: o_def)
   1.786 +  have th1: "inj_on (op o q) ?S"
   1.787 +    apply (auto simp add: inj_on_def)
   1.788 +  proof-
   1.789 +    fix p r
   1.790 +    assume "p permutes {m..n}" and r:"r permutes {m..n}" and rp: "q \<circ> p = q \<circ> r"
   1.791 +    hence "inv q o q o p = inv q o q o r" by (simp add: o_assoc[symmetric])
   1.792 +    with permutes_inj[OF q, unfolded inj_iff]
   1.793 +
   1.794 +    show "p = r" by simp
   1.795 +  qed
   1.796 +  have th3: "(op o q) ` ?S = ?S" using image_compose_permutations_left[OF q] by auto
   1.797 +  from setsum_reindex[OF th1, of f]
   1.798 +  show ?thesis unfolding th0 th1 th3 .
   1.799 +qed
   1.800 +
   1.801 +lemma sum_permutations_compose_right:
   1.802 +  assumes q: "q permutes {m..n}"
   1.803 +  shows "setsum f {p. p permutes {m..n}} =
   1.804 +            setsum (\<lambda>p. f(p o q)) {p. p permutes {m..n}}" (is "?lhs = ?rhs")
   1.805 +proof-
   1.806 +  let ?S = "{p. p permutes {m..n}}"
   1.807 +  have th0: "?rhs = setsum (f o (\<lambda>p. p o q)) ?S" by (simp add: o_def)
   1.808 +  have th1: "inj_on (\<lambda>p. p o q) ?S"
   1.809 +    apply (auto simp add: inj_on_def)
   1.810 +  proof-
   1.811 +    fix p r
   1.812 +    assume "p permutes {m..n}" and r:"r permutes {m..n}" and rp: "p o q = r o q"
   1.813 +    hence "p o (q o inv q)  = r o (q o inv q)" by (simp add: o_assoc)
   1.814 +    with permutes_surj[OF q, unfolded surj_iff]
   1.815 +
   1.816 +    show "p = r" by simp
   1.817 +  qed
   1.818 +  have th3: "(\<lambda>p. p o q) ` ?S = ?S" using image_compose_permutations_right[OF q] by auto
   1.819 +  from setsum_reindex[OF th1, of f]
   1.820 +  show ?thesis unfolding th0 th1 th3 .
   1.821 +qed
   1.822 +
   1.823 +(* ------------------------------------------------------------------------- *)
   1.824 +(* Sum over a set of permutations (could generalize to iteration).           *)
   1.825 +(* ------------------------------------------------------------------------- *)
   1.826 +
   1.827 +lemma setsum_over_permutations_insert:
   1.828 +  assumes fS: "finite S" and aS: "a \<notin> S"
   1.829 +  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)"
   1.830 +proof-
   1.831 +  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)"
   1.832 +    by (simp add: expand_fun_eq)
   1.833 +  have th1: "\<And>P Q. P \<times> Q = {(a,b). a \<in> P \<and> b \<in> Q}" by blast
   1.834 +  have th2: "\<And>P Q. P \<Longrightarrow> (P \<Longrightarrow> Q) \<Longrightarrow> P \<and> Q" by blast
   1.835 +  show ?thesis 
   1.836 +    unfolding permutes_insert    
   1.837 +    unfolding setsum_cartesian_product
   1.838 +    unfolding  th1[symmetric]
   1.839 +    unfolding th0
   1.840 +  proof(rule setsum_reindex)
   1.841 +    let ?f = "(\<lambda>(b, y). Fun.swap a b id \<circ> y)"
   1.842 +    let ?P = "{p. p permutes S}"
   1.843 +    {fix b c p q assume b: "b \<in> insert a S" and c: "c \<in> insert a S" 
   1.844 +      and p: "p permutes S" and q: "q permutes S" 
   1.845 +      and eq: "Fun.swap a b id o p = Fun.swap a c id o q"
   1.846 +      from p q aS have pa: "p a = a" and qa: "q a = a"
   1.847 +	unfolding permutes_def by metis+
   1.848 +      from eq have "(Fun.swap a b id o p) a  = (Fun.swap a c id o q) a" by simp
   1.849 +      hence bc: "b = c"
   1.850 +	apply (simp add: permutes_def pa qa o_def fun_upd_def swap_def id_def cong del: if_weak_cong)
   1.851 +	apply (cases "a = b", auto)
   1.852 +	by (cases "b = c", auto)
   1.853 +      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
   1.854 +      hence "p = q" unfolding o_assoc swap_id_idempotent
   1.855 +	by (simp add: o_def)
   1.856 +      with bc have "b = c \<and> p = q" by blast
   1.857 +    }
   1.858 +    
   1.859 +    then show "inj_on ?f (insert a S \<times> ?P)" 
   1.860 +      unfolding inj_on_def
   1.861 +      apply clarify by metis
   1.862 +  qed
   1.863 +qed
   1.864 +
   1.865 +end