chaieb@29840: (* Title: Library/Permutations chaieb@29840: ID: \$Id: chaieb@29840: Author: Amine Chaieb, University of Cambridge chaieb@29840: *) chaieb@29840: chaieb@29840: header {* Permutations, both general and specifically on finite sets.*} chaieb@29840: chaieb@29840: theory Permutations blanchet@30240: imports Main Finite_Cartesian_Product Parity Fact chaieb@29840: begin chaieb@29840: chaieb@29840: (* Why should I import Main just to solve the Typerep problem! *) chaieb@29840: chaieb@29840: definition permutes (infixr "permutes" 41) where chaieb@29840: "(p permutes S) \ (\x. x \ S \ p x = x) \ (\y. \!x. p x = y)" chaieb@29840: chaieb@29840: (* ------------------------------------------------------------------------- *) chaieb@29840: (* Transpositions. *) chaieb@29840: (* ------------------------------------------------------------------------- *) chaieb@29840: chaieb@29840: declare swap_self[simp] chaieb@29840: lemma swapid_sym: "Fun.swap a b id = Fun.swap b a id" chaieb@29840: by (auto simp add: expand_fun_eq swap_def fun_upd_def) chaieb@29840: lemma swap_id_refl: "Fun.swap a a id = id" by simp chaieb@29840: lemma swap_id_sym: "Fun.swap a b id = Fun.swap b a id" chaieb@29840: by (rule ext, simp add: swap_def) chaieb@29840: lemma swap_id_idempotent[simp]: "Fun.swap a b id o Fun.swap a b id = id" chaieb@29840: by (rule ext, auto simp add: swap_def) chaieb@29840: chaieb@29840: lemma inv_unique_comp: assumes fg: "f o g = id" and gf: "g o f = id" chaieb@29840: shows "inv f = g" chaieb@29840: using fg gf inv_equality[of g f] by (auto simp add: expand_fun_eq) chaieb@29840: chaieb@29840: lemma inverse_swap_id: "inv (Fun.swap a b id) = Fun.swap a b id" chaieb@29840: by (rule inv_unique_comp, simp_all) chaieb@29840: chaieb@29840: lemma swap_id_eq: "Fun.swap a b id x = (if x = a then b else if x = b then a else x)" chaieb@29840: by (simp add: swap_def) chaieb@29840: chaieb@29840: (* ------------------------------------------------------------------------- *) chaieb@29840: (* Basic consequences of the definition. *) chaieb@29840: (* ------------------------------------------------------------------------- *) chaieb@29840: chaieb@29840: lemma permutes_in_image: "p permutes S \ p x \ S \ x \ S" chaieb@29840: unfolding permutes_def by metis chaieb@29840: chaieb@29840: lemma permutes_image: assumes pS: "p permutes S" shows "p ` S = S" chaieb@29840: using pS chaieb@29840: unfolding permutes_def chaieb@29840: apply - chaieb@29840: apply (rule set_ext) chaieb@29840: apply (simp add: image_iff) chaieb@29840: apply metis chaieb@29840: done chaieb@29840: chaieb@29840: lemma permutes_inj: "p permutes S ==> inj p " chaieb@29840: unfolding permutes_def inj_on_def by blast chaieb@29840: chaieb@29840: lemma permutes_surj: "p permutes s ==> surj p" chaieb@29840: unfolding permutes_def surj_def by metis chaieb@29840: chaieb@29840: lemma permutes_inv_o: assumes pS: "p permutes S" chaieb@29840: shows " p o inv p = id" chaieb@29840: and "inv p o p = id" chaieb@29840: using permutes_inj[OF pS] permutes_surj[OF pS] chaieb@29840: unfolding inj_iff[symmetric] surj_iff[symmetric] by blast+ chaieb@29840: chaieb@29840: chaieb@29840: lemma permutes_inverses: chaieb@29840: fixes p :: "'a \ 'a" chaieb@29840: assumes pS: "p permutes S" chaieb@29840: shows "p (inv p x) = x" chaieb@29840: and "inv p (p x) = x" chaieb@29840: using permutes_inv_o[OF pS, unfolded expand_fun_eq o_def] by auto chaieb@29840: chaieb@29840: lemma permutes_subset: "p permutes S \ S \ T ==> p permutes T" chaieb@29840: unfolding permutes_def by blast chaieb@29840: chaieb@29840: lemma permutes_empty[simp]: "p permutes {} \ p = id" chaieb@29840: unfolding expand_fun_eq permutes_def apply simp by metis chaieb@29840: chaieb@29840: lemma permutes_sing[simp]: "p permutes {a} \ p = id" chaieb@29840: unfolding expand_fun_eq permutes_def apply simp by metis chaieb@29840: chaieb@29840: lemma permutes_univ: "p permutes UNIV \ (\y. \!x. p x = y)" chaieb@29840: unfolding permutes_def by simp chaieb@29840: chaieb@29840: lemma permutes_inv_eq: "p permutes S ==> inv p y = x \ p x = y" chaieb@29840: unfolding permutes_def inv_def apply auto chaieb@29840: apply (erule allE[where x=y]) chaieb@29840: apply (erule allE[where x=y]) chaieb@29840: apply (rule someI_ex) apply blast chaieb@29840: apply (rule some1_equality) chaieb@29840: apply blast chaieb@29840: apply blast chaieb@29840: done chaieb@29840: chaieb@29840: lemma permutes_swap_id: "a \ S \ b \ S ==> Fun.swap a b id permutes S" chaieb@29840: unfolding permutes_def swap_def fun_upd_def apply auto apply metis done chaieb@29840: chaieb@29840: lemma permutes_superset: "p permutes S \ (\x \ S - T. p x = x) \ p permutes T" chaieb@29840: apply (simp add: Ball_def permutes_def Diff_iff) by metis chaieb@29840: chaieb@29840: (* ------------------------------------------------------------------------- *) chaieb@29840: (* Group properties. *) chaieb@29840: (* ------------------------------------------------------------------------- *) chaieb@29840: chaieb@29840: lemma permutes_id: "id permutes S" unfolding permutes_def by simp chaieb@29840: chaieb@29840: lemma permutes_compose: "p permutes S \ q permutes S ==> q o p permutes S" chaieb@29840: unfolding permutes_def o_def by metis chaieb@29840: chaieb@29840: lemma permutes_inv: assumes pS: "p permutes S" shows "inv p permutes S" chaieb@29840: using pS unfolding permutes_def permutes_inv_eq[OF pS] by metis chaieb@29840: chaieb@29840: lemma permutes_inv_inv: assumes pS: "p permutes S" shows "inv (inv p) = p" chaieb@29840: unfolding expand_fun_eq permutes_inv_eq[OF pS] permutes_inv_eq[OF permutes_inv[OF pS]] chaieb@29840: by blast chaieb@29840: chaieb@29840: (* ------------------------------------------------------------------------- *) chaieb@29840: (* The number of permutations on a finite set. *) chaieb@29840: (* ------------------------------------------------------------------------- *) chaieb@29840: chaieb@29840: lemma permutes_insert_lemma: chaieb@29840: assumes pS: "p permutes (insert a S)" chaieb@29840: shows "Fun.swap a (p a) id o p permutes S" chaieb@29840: apply (rule permutes_superset[where S = "insert a S"]) chaieb@29840: apply (rule permutes_compose[OF pS]) chaieb@29840: apply (rule permutes_swap_id, simp) chaieb@29840: using permutes_in_image[OF pS, of a] apply simp chaieb@29840: apply (auto simp add: Ball_def Diff_iff swap_def) chaieb@29840: done chaieb@29840: chaieb@29840: lemma permutes_insert: "{p. p permutes (insert a S)} = chaieb@29840: (\(b,p). Fun.swap a b id o p) ` {(b,p). b \ insert a S \ p \ {p. p permutes S}}" chaieb@29840: proof- chaieb@29840: chaieb@29840: {fix p chaieb@29840: {assume pS: "p permutes insert a S" chaieb@29840: let ?b = "p a" chaieb@29840: let ?q = "Fun.swap a (p a) id o p" chaieb@29840: have th0: "p = Fun.swap a ?b id o ?q" unfolding expand_fun_eq o_assoc by simp chaieb@29840: have th1: "?b \ insert a S " unfolding permutes_in_image[OF pS] by simp chaieb@29840: from permutes_insert_lemma[OF pS] th0 th1 chaieb@29840: have "\ b q. p = Fun.swap a b id o q \ b \ insert a S \ q permutes S" by blast} chaieb@29840: moreover chaieb@29840: {fix b q assume bq: "p = Fun.swap a b id o q" "b \ insert a S" "q permutes S" chaieb@29840: from permutes_subset[OF bq(3), of "insert a S"] chaieb@29840: have qS: "q permutes insert a S" by auto chaieb@29840: have aS: "a \ insert a S" by simp chaieb@29840: from bq(1) permutes_compose[OF qS permutes_swap_id[OF aS bq(2)]] chaieb@29840: have "p permutes insert a S" by simp } chaieb@29840: ultimately have "p permutes insert a S \ (\ b q. p = Fun.swap a b id o q \ b \ insert a S \ q permutes S)" by blast} chaieb@29840: thus ?thesis by auto chaieb@29840: qed chaieb@29840: chaieb@29840: lemma hassize_insert: "a \ F \ insert a F hassize n \ F hassize (n - 1)" chaieb@29840: by (auto simp add: hassize_def) chaieb@29840: chaieb@29840: lemma hassize_permutations: assumes Sn: "S hassize n" chaieb@29840: shows "{p. p permutes S} hassize (fact n)" chaieb@29840: proof- chaieb@29840: from Sn have fS:"finite S" by (simp add: hassize_def) chaieb@29840: chaieb@29840: have "\n. (S hassize n) \ ({p. p permutes S} hassize (fact n))" chaieb@29840: proof(rule finite_induct[where F = S]) chaieb@29840: from fS show "finite S" . chaieb@29840: next chaieb@29840: show "\n. ({} hassize n) \ ({p. p permutes {}} hassize fact n)" chaieb@29840: by (simp add: hassize_def permutes_empty) chaieb@29840: next chaieb@29840: fix x F chaieb@29840: assume fF: "finite F" and xF: "x \ F" chaieb@29840: and H: "\n. (F hassize n) \ ({p. p permutes F} hassize fact n)" chaieb@29840: {fix n assume H0: "insert x F hassize n" chaieb@29840: let ?xF = "{p. p permutes insert x F}" chaieb@29840: let ?pF = "{p. p permutes F}" chaieb@29840: let ?pF' = "{(b, p). b \ insert x F \ p \ ?pF}" chaieb@29840: let ?g = "(\(b, p). Fun.swap x b id \ p)" chaieb@29840: from permutes_insert[of x F] chaieb@29840: have xfgpF': "?xF = ?g ` ?pF'" . chaieb@29840: from hassize_insert[OF xF H0] have Fs: "F hassize (n - 1)" . chaieb@29840: from H Fs have pFs: "?pF hassize fact (n - 1)" by blast chaieb@29840: hence pF'f: "finite ?pF'" using H0 unfolding hassize_def chaieb@29840: apply (simp only: Collect_split Collect_mem_eq) chaieb@29840: apply (rule finite_cartesian_product) chaieb@29840: apply simp_all chaieb@29840: done chaieb@29840: chaieb@29840: have ginj: "inj_on ?g ?pF'" chaieb@29840: proof- chaieb@29840: { chaieb@29840: fix b p c q assume bp: "(b,p) \ ?pF'" and cq: "(c,q) \ ?pF'" chaieb@29840: and eq: "?g (b,p) = ?g (c,q)" chaieb@29840: from bp cq have ths: "b \ insert x F" "c \ insert x F" "x \ insert x F" "p permutes F" "q permutes F" by auto chaieb@29840: from ths(4) xF eq have "b = ?g (b,p) x" unfolding permutes_def chaieb@29840: by (auto simp add: swap_def fun_upd_def expand_fun_eq) chaieb@29840: also have "\ = ?g (c,q) x" using ths(5) xF eq chaieb@29840: by (auto simp add: swap_def fun_upd_def expand_fun_eq) chaieb@29840: also have "\ = c"using ths(5) xF unfolding permutes_def chaieb@29840: by (auto simp add: swap_def fun_upd_def expand_fun_eq) chaieb@29840: finally have bc: "b = c" . chaieb@29840: hence "Fun.swap x b id = Fun.swap x c id" by simp chaieb@29840: with eq have "Fun.swap x b id o p = Fun.swap x b id o q" by simp chaieb@29840: 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 chaieb@29840: hence "p = q" by (simp add: o_assoc) chaieb@29840: with bc have "(b,p) = (c,q)" by simp } chaieb@29840: thus ?thesis unfolding inj_on_def by blast chaieb@29840: qed chaieb@29840: from xF H0 have n0: "n \ 0 " by (auto simp add: hassize_def) chaieb@29840: hence "\m. n = Suc m" by arith chaieb@29840: then obtain m where n[simp]: "n = Suc m" by blast chaieb@29840: from pFs H0 have xFc: "card ?xF = fact n" chaieb@29840: unfolding xfgpF' card_image[OF ginj] hassize_def chaieb@29840: apply (simp only: Collect_split Collect_mem_eq card_cartesian_product) chaieb@29840: by simp chaieb@29840: from finite_imageI[OF pF'f, of ?g] have xFf: "finite ?xF" unfolding xfgpF' by simp chaieb@29840: have "?xF hassize fact n" chaieb@29840: using xFf xFc chaieb@29840: unfolding hassize_def xFf by blast } chaieb@29840: thus "\n. (insert x F hassize n) \ ({p. p permutes insert x F} hassize fact n)" chaieb@29840: by blast chaieb@29840: qed chaieb@29840: with Sn show ?thesis by blast chaieb@29840: qed chaieb@29840: chaieb@29840: lemma finite_permutations: "finite S ==> finite {p. p permutes S}" chaieb@29840: using hassize_permutations[of S] unfolding hassize_def by blast chaieb@29840: chaieb@29840: (* ------------------------------------------------------------------------- *) chaieb@29840: (* Permutations of index set for iterated operations. *) chaieb@29840: (* ------------------------------------------------------------------------- *) chaieb@29840: chaieb@29840: lemma (in ab_semigroup_mult) fold_image_permute: assumes fS: "finite S" and pS: "p permutes S" chaieb@29840: shows "fold_image times f z S = fold_image times (f o p) z S" chaieb@29840: using fold_image_reindex[OF fS subset_inj_on[OF permutes_inj[OF pS], of S, simplified], of f z] chaieb@29840: unfolding permutes_image[OF pS] . chaieb@29840: lemma (in ab_semigroup_add) fold_image_permute: assumes fS: "finite S" and pS: "p permutes S" chaieb@29840: shows "fold_image plus f z S = fold_image plus (f o p) z S" chaieb@29840: proof- chaieb@29840: interpret ab_semigroup_mult plus apply unfold_locales apply (simp add: add_assoc) chaieb@29840: apply (simp add: add_commute) done chaieb@29840: from fold_image_reindex[OF fS subset_inj_on[OF permutes_inj[OF pS], of S, simplified], of f z] chaieb@29840: show ?thesis chaieb@29840: unfolding permutes_image[OF pS] . chaieb@29840: qed chaieb@29840: chaieb@29840: lemma setsum_permute: assumes pS: "p permutes S" chaieb@29840: shows "setsum f S = setsum (f o p) S" chaieb@29840: unfolding setsum_def using fold_image_permute[of S p f 0] pS by clarsimp chaieb@29840: chaieb@29840: lemma setsum_permute_natseg:assumes pS: "p permutes {m .. n}" chaieb@29840: shows "setsum f {m .. n} = setsum (f o p) {m .. n}" chaieb@29840: using setsum_permute[OF pS, of f ] pS by blast chaieb@29840: chaieb@29840: lemma setprod_permute: assumes pS: "p permutes S" chaieb@29840: shows "setprod f S = setprod (f o p) S" chaieb@29840: unfolding setprod_def chaieb@29840: using ab_semigroup_mult_class.fold_image_permute[of S p f 1] pS by clarsimp chaieb@29840: chaieb@29840: lemma setprod_permute_natseg:assumes pS: "p permutes {m .. n}" chaieb@29840: shows "setprod f {m .. n} = setprod (f o p) {m .. n}" chaieb@29840: using setprod_permute[OF pS, of f ] pS by blast chaieb@29840: chaieb@29840: (* ------------------------------------------------------------------------- *) chaieb@29840: (* Various combinations of transpositions with 2, 1 and 0 common elements. *) chaieb@29840: (* ------------------------------------------------------------------------- *) chaieb@29840: chaieb@29840: lemma swap_id_common:" a \ c \ b \ c \ 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) chaieb@29840: chaieb@29840: lemma swap_id_common': "~(a = b) \ ~(a = c) \ 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) chaieb@29840: chaieb@29840: lemma swap_id_independent: "~(a = c) \ ~(a = d) \ ~(b = c) \ ~(b = d) ==> Fun.swap a b id o Fun.swap c d id = Fun.swap c d id o Fun.swap a b id" chaieb@29840: by (simp add: swap_def expand_fun_eq) chaieb@29840: chaieb@29840: (* ------------------------------------------------------------------------- *) chaieb@29840: (* Permutations as transposition sequences. *) chaieb@29840: (* ------------------------------------------------------------------------- *) chaieb@29840: chaieb@29840: chaieb@29840: inductive swapidseq :: "nat \ ('a \ 'a) \ bool" where chaieb@29840: id[simp]: "swapidseq 0 id" chaieb@29840: | comp_Suc: "swapidseq n p \ a \ b \ swapidseq (Suc n) (Fun.swap a b id o p)" chaieb@29840: chaieb@29840: declare id[unfolded id_def, simp] chaieb@29840: definition "permutation p \ (\n. swapidseq n p)" chaieb@29840: chaieb@29840: (* ------------------------------------------------------------------------- *) chaieb@29840: (* Some closure properties of the set of permutations, with lengths. *) chaieb@29840: (* ------------------------------------------------------------------------- *) chaieb@29840: chaieb@29840: lemma permutation_id[simp]: "permutation id"unfolding permutation_def chaieb@29840: by (rule exI[where x=0], simp) chaieb@29840: declare permutation_id[unfolded id_def, simp] chaieb@29840: chaieb@29840: lemma swapidseq_swap: "swapidseq (if a = b then 0 else 1) (Fun.swap a b id)" chaieb@29840: apply clarsimp chaieb@29840: using comp_Suc[of 0 id a b] by simp chaieb@29840: chaieb@29840: lemma permutation_swap_id: "permutation (Fun.swap a b id)" chaieb@29840: apply (cases "a=b", simp_all) chaieb@29840: unfolding permutation_def using swapidseq_swap[of a b] by blast chaieb@29840: chaieb@29840: lemma swapidseq_comp_add: "swapidseq n p \ swapidseq m q ==> swapidseq (n + m) (p o q)" chaieb@29840: proof (induct n p arbitrary: m q rule: swapidseq.induct) chaieb@29840: case (id m q) thus ?case by simp chaieb@29840: next chaieb@29840: case (comp_Suc n p a b m q) chaieb@29840: have th: "Suc n + m = Suc (n + m)" by arith chaieb@29840: show ?case unfolding th o_assoc[symmetric] chaieb@29840: apply (rule swapidseq.comp_Suc) using comp_Suc.hyps(2)[OF comp_Suc.prems] comp_Suc.hyps(3) by blast+ chaieb@29840: qed chaieb@29840: chaieb@29840: lemma permutation_compose: "permutation p \ permutation q ==> permutation(p o q)" chaieb@29840: unfolding permutation_def using swapidseq_comp_add[of _ p _ q] by metis chaieb@29840: chaieb@29840: lemma swapidseq_endswap: "swapidseq n p \ a \ b ==> swapidseq (Suc n) (p o Fun.swap a b id)" chaieb@29840: apply (induct n p rule: swapidseq.induct) chaieb@29840: using swapidseq_swap[of a b] chaieb@29840: by (auto simp add: o_assoc[symmetric] intro: swapidseq.comp_Suc) chaieb@29840: chaieb@29840: lemma swapidseq_inverse_exists: "swapidseq n p ==> \q. swapidseq n q \ p o q = id \ q o p = id" chaieb@29840: proof(induct n p rule: swapidseq.induct) chaieb@29840: case id thus ?case by (rule exI[where x=id], simp) chaieb@29840: next chaieb@29840: case (comp_Suc n p a b) chaieb@29840: from comp_Suc.hyps obtain q where q: "swapidseq n q" "p \ q = id" "q \ p = id" by blast chaieb@29840: let ?q = "q o Fun.swap a b id" chaieb@29840: note H = comp_Suc.hyps chaieb@29840: from swapidseq_swap[of a b] H(3) have th0: "swapidseq 1 (Fun.swap a b id)" by simp chaieb@29840: from swapidseq_comp_add[OF q(1) th0] have th1:"swapidseq (Suc n) ?q" by simp chaieb@29840: 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) chaieb@29840: also have "\ = id" by (simp add: q(2)) chaieb@29840: finally have th2: "Fun.swap a b id o p o ?q = id" . chaieb@29840: have "?q \ (Fun.swap a b id \ p) = q \ (Fun.swap a b id o Fun.swap a b id) \ p" by (simp only: o_assoc) chaieb@29840: hence "?q \ (Fun.swap a b id \ p) = id" by (simp add: q(3)) chaieb@29840: with th1 th2 show ?case by blast chaieb@29840: qed chaieb@29840: chaieb@29840: chaieb@29840: lemma swapidseq_inverse: assumes H: "swapidseq n p" shows "swapidseq n (inv p)" chaieb@29840: using swapidseq_inverse_exists[OF H] inv_unique_comp[of p] by auto chaieb@29840: chaieb@29840: lemma permutation_inverse: "permutation p ==> permutation (inv p)" chaieb@29840: using permutation_def swapidseq_inverse by blast chaieb@29840: chaieb@29840: (* ------------------------------------------------------------------------- *) chaieb@29840: (* The identity map only has even transposition sequences. *) chaieb@29840: (* ------------------------------------------------------------------------- *) chaieb@29840: chaieb@29840: lemma symmetry_lemma:"(\a b c d. P a b c d ==> P a b d c) \ chaieb@29840: (\a b c d. a \ b \ c \ d \ (a = c \ b = d \ a = c \ b \ d \ a \ c \ b = d \ a \ c \ a \ d \ b \ c \ b \ d) ==> P a b c d) chaieb@29840: ==> (\a b c d. a \ b --> c \ d \ P a b c d)" by metis chaieb@29840: chaieb@29840: lemma swap_general: "a \ b \ c \ d \ Fun.swap a b id o Fun.swap c d id = id \ chaieb@29840: (\x y z. x \ a \ y \ a \ z \ a \ x \ y \ Fun.swap a b id o Fun.swap c d id = Fun.swap x y id o Fun.swap a z id)" chaieb@29840: proof- chaieb@29840: assume H: "a\b" "c\d" chaieb@29840: have "a \ b \ c \ d \ chaieb@29840: ( Fun.swap a b id o Fun.swap c d id = id \ chaieb@29840: (\x y z. x \ a \ y \ a \ z \ a \ x \ y \ Fun.swap a b id o Fun.swap c d id = Fun.swap x y id o Fun.swap a z id))" chaieb@29840: apply (rule symmetry_lemma[where a=a and b=b and c=c and d=d]) chaieb@29840: apply (simp_all only: swapid_sym) chaieb@29840: apply (case_tac "a = c \ b = d", clarsimp simp only: swapid_sym swap_id_idempotent) chaieb@29840: apply (case_tac "a = c \ b \ d") chaieb@29840: apply (rule disjI2) chaieb@29840: apply (rule_tac x="b" in exI) chaieb@29840: apply (rule_tac x="d" in exI) chaieb@29840: apply (rule_tac x="b" in exI) chaieb@29840: apply (clarsimp simp add: expand_fun_eq swap_def) chaieb@29840: apply (case_tac "a \ c \ b = d") chaieb@29840: apply (rule disjI2) chaieb@29840: apply (rule_tac x="c" in exI) chaieb@29840: apply (rule_tac x="d" in exI) chaieb@29840: apply (rule_tac x="c" in exI) chaieb@29840: apply (clarsimp simp add: expand_fun_eq swap_def) chaieb@29840: apply (rule disjI2) chaieb@29840: apply (rule_tac x="c" in exI) chaieb@29840: apply (rule_tac x="d" in exI) chaieb@29840: apply (rule_tac x="b" in exI) chaieb@29840: apply (clarsimp simp add: expand_fun_eq swap_def) chaieb@29840: done chaieb@29840: with H show ?thesis by metis chaieb@29840: qed chaieb@29840: chaieb@29840: lemma swapidseq_id_iff[simp]: "swapidseq 0 p \ p = id" chaieb@29840: using swapidseq.cases[of 0 p "p = id"] chaieb@29840: by auto chaieb@29840: chaieb@29840: lemma swapidseq_cases: "swapidseq n p \ (n=0 \ p = id \ (\a b q m. n = Suc m \ p = Fun.swap a b id o q \ swapidseq m q \ a\ b))" chaieb@29840: apply (rule iffI) chaieb@29840: apply (erule swapidseq.cases[of n p]) chaieb@29840: apply simp chaieb@29840: apply (rule disjI2) chaieb@29840: apply (rule_tac x= "a" in exI) chaieb@29840: apply (rule_tac x= "b" in exI) chaieb@29840: apply (rule_tac x= "pa" in exI) chaieb@29840: apply (rule_tac x= "na" in exI) chaieb@29840: apply simp chaieb@29840: apply auto chaieb@29840: apply (rule comp_Suc, simp_all) chaieb@29840: done chaieb@29840: lemma fixing_swapidseq_decrease: chaieb@29840: assumes spn: "swapidseq n p" and ab: "a\b" and pa: "(Fun.swap a b id o p) a = a" chaieb@29840: shows "n \ 0 \ swapidseq (n - 1) (Fun.swap a b id o p)" chaieb@29840: using spn ab pa chaieb@29840: proof(induct n arbitrary: p a b) chaieb@29840: case 0 thus ?case by (auto simp add: swap_def fun_upd_def) chaieb@29840: next chaieb@29840: case (Suc n p a b) chaieb@29840: from Suc.prems(1) swapidseq_cases[of "Suc n" p] obtain chaieb@29840: c d q m where cdqm: "Suc n = Suc m" "p = Fun.swap c d id o q" "swapidseq m q" "c \ d" "n = m" chaieb@29840: by auto chaieb@29840: {assume H: "Fun.swap a b id o Fun.swap c d id = id" chaieb@29840: chaieb@29840: have ?case apply (simp only: cdqm o_assoc H) chaieb@29840: by (simp add: cdqm)} chaieb@29840: moreover chaieb@29840: { fix x y z chaieb@29840: assume H: "x\a" "y\a" "z \a" "x \y" chaieb@29840: "Fun.swap a b id o Fun.swap c d id = Fun.swap x y id o Fun.swap a z id" chaieb@29840: from H have az: "a \ z" by simp chaieb@29840: chaieb@29840: {fix h have "(Fun.swap x y id o h) a = a \ h a = a" chaieb@29840: using H by (simp add: swap_def)} chaieb@29840: note th3 = this chaieb@29840: 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 chaieb@29840: 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) chaieb@29840: 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 chaieb@29840: hence "(Fun.swap x y id o (Fun.swap a z id o q)) a = a" unfolding Suc by metis chaieb@29840: hence th1: "(Fun.swap a z id o q) a = a" unfolding th3 . chaieb@29840: from Suc.hyps[OF cdqm(3)[ unfolded cdqm(5)[symmetric]] az th1] chaieb@29840: have th2: "swapidseq (n - 1) (Fun.swap a z id o q)" "n \ 0" by blast+ chaieb@29840: have th: "Suc n - 1 = Suc (n - 1)" using th2(2) by auto chaieb@29840: have ?case unfolding cdqm(2) H o_assoc th chaieb@29840: apply (simp only: Suc_not_Zero simp_thms o_assoc[symmetric]) chaieb@29840: apply (rule comp_Suc) chaieb@29840: using th2 H apply blast+ chaieb@29840: done} chaieb@29840: ultimately show ?case using swap_general[OF Suc.prems(2) cdqm(4)] by metis chaieb@29840: qed chaieb@29840: chaieb@29840: lemma swapidseq_identity_even: chaieb@29840: assumes "swapidseq n (id :: 'a \ 'a)" shows "even n" chaieb@29840: using `swapidseq n id` chaieb@29840: proof(induct n rule: nat_less_induct) chaieb@29840: fix n chaieb@29840: assume H: "\m 'a) \ even m" "swapidseq n (id :: 'a \ 'a)" chaieb@29840: {assume "n = 0" hence "even n" by arith} chaieb@29840: moreover chaieb@29840: {fix a b :: 'a and q m chaieb@29840: assume h: "n = Suc m" "(id :: 'a \ 'a) = Fun.swap a b id \ q" "swapidseq m q" "a \ b" chaieb@29840: from fixing_swapidseq_decrease[OF h(3,4), unfolded h(2)[symmetric]] chaieb@29840: have m: "m \ 0" "swapidseq (m - 1) (id :: 'a \ 'a)" by auto chaieb@29840: from h m have mn: "m - 1 < n" by arith chaieb@29840: from H(1)[rule_format, OF mn m(2)] h(1) m(1) have "even n" apply arith done} chaieb@29840: ultimately show "even n" using H(2)[unfolded swapidseq_cases[of n id]] by auto chaieb@29840: qed chaieb@29840: chaieb@29840: (* ------------------------------------------------------------------------- *) chaieb@29840: (* Therefore we have a welldefined notion of parity. *) chaieb@29840: (* ------------------------------------------------------------------------- *) chaieb@29840: chaieb@29840: definition "evenperm p = even (SOME n. swapidseq n p)" chaieb@29840: chaieb@29840: lemma swapidseq_even_even: assumes chaieb@29840: m: "swapidseq m p" and n: "swapidseq n p" chaieb@29840: shows "even m \ even n" chaieb@29840: proof- chaieb@29840: from swapidseq_inverse_exists[OF n] chaieb@29840: obtain q where q: "swapidseq n q" "p \ q = id" "q \ p = id" by blast chaieb@29840: chaieb@29840: from swapidseq_identity_even[OF swapidseq_comp_add[OF m q(1), unfolded q]] chaieb@29840: show ?thesis by arith chaieb@29840: qed chaieb@29840: chaieb@29840: lemma evenperm_unique: assumes p: "swapidseq n p" and n:"even n = b" chaieb@29840: shows "evenperm p = b" chaieb@29840: unfolding n[symmetric] evenperm_def chaieb@29840: apply (rule swapidseq_even_even[where p = p]) chaieb@29840: apply (rule someI[where x = n]) chaieb@29840: using p by blast+ chaieb@29840: chaieb@29840: (* ------------------------------------------------------------------------- *) chaieb@29840: (* And it has the expected composition properties. *) chaieb@29840: (* ------------------------------------------------------------------------- *) chaieb@29840: chaieb@29840: lemma evenperm_id[simp]: "evenperm id = True" chaieb@29840: apply (rule evenperm_unique[where n = 0]) by simp_all chaieb@29840: chaieb@29840: lemma evenperm_swap: "evenperm (Fun.swap a b id) = (a = b)" chaieb@29840: apply (rule evenperm_unique[where n="if a = b then 0 else 1"]) chaieb@29840: by (simp_all add: swapidseq_swap) chaieb@29840: chaieb@29840: lemma evenperm_comp: chaieb@29840: assumes p: "permutation p" and q:"permutation q" chaieb@29840: shows "evenperm (p o q) = (evenperm p = evenperm q)" chaieb@29840: proof- chaieb@29840: from p q obtain chaieb@29840: n m where n: "swapidseq n p" and m: "swapidseq m q" chaieb@29840: unfolding permutation_def by blast chaieb@29840: note nm = swapidseq_comp_add[OF n m] chaieb@29840: have th: "even (n + m) = (even n \ even m)" by arith chaieb@29840: from evenperm_unique[OF n refl] evenperm_unique[OF m refl] chaieb@29840: evenperm_unique[OF nm th] chaieb@29840: show ?thesis by blast chaieb@29840: qed chaieb@29840: chaieb@29840: lemma evenperm_inv: assumes p: "permutation p" chaieb@29840: shows "evenperm (inv p) = evenperm p" chaieb@29840: proof- chaieb@29840: from p obtain n where n: "swapidseq n p" unfolding permutation_def by blast chaieb@29840: from evenperm_unique[OF swapidseq_inverse[OF n] evenperm_unique[OF n refl, symmetric]] chaieb@29840: show ?thesis . chaieb@29840: qed chaieb@29840: chaieb@29840: (* ------------------------------------------------------------------------- *) chaieb@29840: (* A more abstract characterization of permutations. *) chaieb@29840: (* ------------------------------------------------------------------------- *) chaieb@29840: chaieb@29840: chaieb@29840: lemma bij_iff: "bij f \ (\x. \!y. f y = x)" chaieb@29840: unfolding bij_def inj_on_def surj_def chaieb@29840: apply auto chaieb@29840: apply metis chaieb@29840: apply metis chaieb@29840: done chaieb@29840: chaieb@29840: lemma permutation_bijective: chaieb@29840: assumes p: "permutation p" chaieb@29840: shows "bij p" chaieb@29840: proof- chaieb@29840: from p obtain n where n: "swapidseq n p" unfolding permutation_def by blast chaieb@29840: from swapidseq_inverse_exists[OF n] obtain q where chaieb@29840: q: "swapidseq n q" "p \ q = id" "q \ p = id" by blast chaieb@29840: thus ?thesis unfolding bij_iff apply (auto simp add: expand_fun_eq) apply metis done chaieb@29840: qed chaieb@29840: chaieb@29840: lemma permutation_finite_support: assumes p: "permutation p" chaieb@29840: shows "finite {x. p x \ x}" chaieb@29840: proof- chaieb@29840: from p obtain n where n: "swapidseq n p" unfolding permutation_def by blast chaieb@29840: from n show ?thesis chaieb@29840: proof(induct n p rule: swapidseq.induct) chaieb@29840: case id thus ?case by simp chaieb@29840: next chaieb@29840: case (comp_Suc n p a b) chaieb@29840: let ?S = "insert a (insert b {x. p x \ x})" chaieb@29840: from comp_Suc.hyps(2) have fS: "finite ?S" by simp chaieb@29840: from `a \ b` have th: "{x. (Fun.swap a b id o p) x \ x} \ ?S" chaieb@29840: by (auto simp add: swap_def) chaieb@29840: from finite_subset[OF th fS] show ?case . chaieb@29840: qed chaieb@29840: qed chaieb@29840: chaieb@29840: lemma bij_inv_eq_iff: "bij p ==> x = inv p y \ p x = y" chaieb@29840: using surj_f_inv_f[of p] inv_f_f[of f] by (auto simp add: bij_def) chaieb@29840: chaieb@29840: lemma bij_swap_comp: chaieb@29840: assumes bp: "bij p" shows "Fun.swap a b id o p = Fun.swap (inv p a) (inv p b) p" chaieb@29840: using surj_f_inv_f[OF bij_is_surj[OF bp]] chaieb@29840: by (simp add: expand_fun_eq swap_def bij_inv_eq_iff[OF bp]) chaieb@29840: chaieb@29840: lemma bij_swap_ompose_bij: "bij p \ bij (Fun.swap a b id o p)" chaieb@29840: proof- chaieb@29840: assume H: "bij p" chaieb@29840: show ?thesis chaieb@29840: unfolding bij_swap_comp[OF H] bij_swap_iff chaieb@29840: using H . chaieb@29840: qed chaieb@29840: chaieb@29840: lemma permutation_lemma: chaieb@29840: assumes fS: "finite S" and p: "bij p" and pS: "\x. x\ S \ p x = x" chaieb@29840: shows "permutation p" chaieb@29840: using fS p pS chaieb@29840: proof(induct S arbitrary: p rule: finite_induct) chaieb@29840: case (empty p) thus ?case by simp chaieb@29840: next chaieb@29840: case (insert a F p) chaieb@29840: let ?r = "Fun.swap a (p a) id o p" chaieb@29840: let ?q = "Fun.swap a (p a) id o ?r " chaieb@29840: have raa: "?r a = a" by (simp add: swap_def) chaieb@29840: from bij_swap_ompose_bij[OF insert(4)] chaieb@29840: have br: "bij ?r" . chaieb@29840: chaieb@29840: from insert raa have th: "\x. x \ F \ ?r x = x" chaieb@29840: apply (clarsimp simp add: swap_def) chaieb@29840: apply (erule_tac x="x" in allE) chaieb@29840: apply auto chaieb@29840: unfolding bij_iff apply metis chaieb@29840: done chaieb@29840: from insert(3)[OF br th] chaieb@29840: have rp: "permutation ?r" . chaieb@29840: have "permutation ?q" by (simp add: permutation_compose permutation_swap_id rp) chaieb@29840: thus ?case by (simp add: o_assoc) chaieb@29840: qed chaieb@29840: chaieb@29840: lemma permutation: "permutation p \ bij p \ finite {x. p x \ x}" chaieb@29840: (is "?lhs \ ?b \ ?f") chaieb@29840: proof chaieb@29840: assume p: ?lhs chaieb@29840: from p permutation_bijective permutation_finite_support show "?b \ ?f" by auto chaieb@29840: next chaieb@29840: assume bf: "?b \ ?f" chaieb@29840: hence bf: "?f" "?b" by blast+ chaieb@29840: from permutation_lemma[OF bf] show ?lhs by blast chaieb@29840: qed chaieb@29840: chaieb@29840: lemma permutation_inverse_works: assumes p: "permutation p" chaieb@29840: shows "inv p o p = id" "p o inv p = id" chaieb@29840: using permutation_bijective[OF p] surj_iff bij_def inj_iff by auto chaieb@29840: chaieb@29840: lemma permutation_inverse_compose: chaieb@29840: assumes p: "permutation p" and q: "permutation q" chaieb@29840: shows "inv (p o q) = inv q o inv p" chaieb@29840: proof- chaieb@29840: note ps = permutation_inverse_works[OF p] chaieb@29840: note qs = permutation_inverse_works[OF q] chaieb@29840: have "p o q o (inv q o inv p) = p o (q o inv q) o inv p" by (simp add: o_assoc) chaieb@29840: also have "\ = id" by (simp add: ps qs) chaieb@29840: finally have th0: "p o q o (inv q o inv p) = id" . chaieb@29840: have "inv q o inv p o (p o q) = inv q o (inv p o p) o q" by (simp add: o_assoc) chaieb@29840: also have "\ = id" by (simp add: ps qs) chaieb@29840: finally have th1: "inv q o inv p o (p o q) = id" . chaieb@29840: from inv_unique_comp[OF th0 th1] show ?thesis . chaieb@29840: qed chaieb@29840: chaieb@29840: (* ------------------------------------------------------------------------- *) chaieb@29840: (* Relation to "permutes". *) chaieb@29840: (* ------------------------------------------------------------------------- *) chaieb@29840: chaieb@29840: lemma permutation_permutes: "permutation p \ (\S. finite S \ p permutes S)" chaieb@29840: unfolding permutation permutes_def bij_iff[symmetric] chaieb@29840: apply (rule iffI, clarify) chaieb@29840: apply (rule exI[where x="{x. p x \ x}"]) chaieb@29840: apply simp chaieb@29840: apply clarsimp chaieb@29840: apply (rule_tac B="S" in finite_subset) chaieb@29840: apply auto chaieb@29840: done chaieb@29840: chaieb@29840: (* ------------------------------------------------------------------------- *) chaieb@29840: (* Hence a sort of induction principle composing by swaps. *) chaieb@29840: (* ------------------------------------------------------------------------- *) chaieb@29840: chaieb@29840: lemma permutes_induct: "finite S \ P id \ (\ a b p. a \ S \ b \ S \ P p \ P p \ permutation p ==> P (Fun.swap a b id o p)) chaieb@29840: ==> (\p. p permutes S ==> P p)" chaieb@29840: proof(induct S rule: finite_induct) chaieb@29840: case empty thus ?case by auto chaieb@29840: next chaieb@29840: case (insert x F p) chaieb@29840: let ?r = "Fun.swap x (p x) id o p" chaieb@29840: let ?q = "Fun.swap x (p x) id o ?r" chaieb@29840: have qp: "?q = p" by (simp add: o_assoc) chaieb@29840: from permutes_insert_lemma[OF insert.prems(3)] insert have Pr: "P ?r" by blast chaieb@29840: from permutes_in_image[OF insert.prems(3), of x] chaieb@29840: have pxF: "p x \ insert x F" by simp chaieb@29840: have xF: "x \ insert x F" by simp chaieb@29840: have rp: "permutation ?r" chaieb@29840: unfolding permutation_permutes using insert.hyps(1) chaieb@29840: permutes_insert_lemma[OF insert.prems(3)] by blast chaieb@29840: from insert.prems(2)[OF xF pxF Pr Pr rp] chaieb@29840: show ?case unfolding qp . chaieb@29840: qed chaieb@29840: chaieb@29840: (* ------------------------------------------------------------------------- *) chaieb@29840: (* Sign of a permutation as a real number. *) chaieb@29840: (* ------------------------------------------------------------------------- *) chaieb@29840: chaieb@29840: definition "sign p = (if evenperm p then (1::int) else -1)" chaieb@29840: chaieb@29840: lemma sign_nz: "sign p \ 0" by (simp add: sign_def) chaieb@29840: lemma sign_id: "sign id = 1" by (simp add: sign_def) chaieb@29840: lemma sign_inverse: "permutation p ==> sign (inv p) = sign p" chaieb@29840: by (simp add: sign_def evenperm_inv) chaieb@29840: lemma sign_compose: "permutation p \ permutation q ==> sign (p o q) = sign(p) * sign(q)" by (simp add: sign_def evenperm_comp) chaieb@29840: lemma sign_swap_id: "sign (Fun.swap a b id) = (if a = b then 1 else -1)" chaieb@29840: by (simp add: sign_def evenperm_swap) chaieb@29840: lemma sign_idempotent: "sign p * sign p = 1" by (simp add: sign_def) chaieb@29840: chaieb@29840: (* ------------------------------------------------------------------------- *) chaieb@29840: (* More lemmas about permutations. *) chaieb@29840: (* ------------------------------------------------------------------------- *) chaieb@29840: chaieb@29840: lemma permutes_natset_le: blanchet@30240: assumes p: "p permutes (S::'a::wellorder set)" and le: "\i \ S. p i <= i" shows "p = id" chaieb@29840: proof- chaieb@29840: {fix n chaieb@29840: have "p n = n" chaieb@29840: using p le blanchet@30240: proof(induct n arbitrary: S rule: less_induct) blanchet@30240: fix n S assume H: "\m S. \m < n; p permutes S; \i\S. p i \ i\ \ p m = m" chaieb@29840: "p permutes S" "\i \S. p i \ i" chaieb@29840: {assume "n \ S" chaieb@29840: with H(2) have "p n = n" unfolding permutes_def by metis} chaieb@29840: moreover chaieb@29840: {assume ns: "n \ S" chaieb@29840: from H(3) ns have "p n < n \ p n = n" by auto chaieb@29840: moreover{assume h: "p n < n" chaieb@29840: from H h have "p (p n) = p n" by metis chaieb@29840: with permutes_inj[OF H(2)] have "p n = n" unfolding inj_on_def by blast blanchet@30240: with h have False by simp} chaieb@29840: ultimately have "p n = n" by blast } chaieb@29840: ultimately show "p n = n" by blast chaieb@29840: qed} chaieb@29840: thus ?thesis by (auto simp add: expand_fun_eq) chaieb@29840: qed chaieb@29840: chaieb@29840: lemma permutes_natset_ge: blanchet@30240: assumes p: "p permutes (S::'a::wellorder set)" and le: "\i \ S. p i \ i" shows "p = id" chaieb@29840: proof- chaieb@29840: {fix i assume i: "i \ S" chaieb@29840: from i permutes_in_image[OF permutes_inv[OF p]] have "inv p i \ S" by simp chaieb@29840: with le have "p (inv p i) \ inv p i" by blast chaieb@29840: with permutes_inverses[OF p] have "i \ inv p i" by simp} chaieb@29840: then have th: "\i\S. inv p i \ i" by blast chaieb@29840: from permutes_natset_le[OF permutes_inv[OF p] th] chaieb@29840: have "inv p = inv id" by simp chaieb@29840: then show ?thesis chaieb@29840: apply (subst permutes_inv_inv[OF p, symmetric]) chaieb@29840: apply (rule inv_unique_comp) chaieb@29840: apply simp_all chaieb@29840: done chaieb@29840: qed chaieb@29840: chaieb@29840: lemma image_inverse_permutations: "{inv p |p. p permutes S} = {p. p permutes S}" chaieb@29840: apply (rule set_ext) chaieb@29840: apply auto chaieb@29840: using permutes_inv_inv permutes_inv apply auto chaieb@29840: apply (rule_tac x="inv x" in exI) chaieb@29840: apply auto chaieb@29840: done chaieb@29840: chaieb@29840: lemma image_compose_permutations_left: chaieb@29840: assumes q: "q permutes S" shows "{q o p | p. p permutes S} = {p . p permutes S}" chaieb@29840: apply (rule set_ext) chaieb@29840: apply auto chaieb@29840: apply (rule permutes_compose) chaieb@29840: using q apply auto chaieb@29840: apply (rule_tac x = "inv q o x" in exI) chaieb@29840: by (simp add: o_assoc permutes_inv permutes_compose permutes_inv_o) chaieb@29840: chaieb@29840: lemma image_compose_permutations_right: chaieb@29840: assumes q: "q permutes S" chaieb@29840: shows "{p o q | p. p permutes S} = {p . p permutes S}" chaieb@29840: apply (rule set_ext) chaieb@29840: apply auto chaieb@29840: apply (rule permutes_compose) chaieb@29840: using q apply auto chaieb@29840: apply (rule_tac x = "x o inv q" in exI) chaieb@29840: by (simp add: o_assoc permutes_inv permutes_compose permutes_inv_o o_assoc[symmetric]) chaieb@29840: chaieb@29840: lemma permutes_in_seg: "p permutes {1 ..n} \ i \ {1..n} ==> 1 <= p i \ p i <= n" chaieb@29840: chaieb@29840: apply (simp add: permutes_def) chaieb@29840: apply metis chaieb@29840: done chaieb@29840: chaieb@29840: term setsum blanchet@30240: lemma setsum_permutations_inverse: "setsum f {p. p permutes S} = setsum (\p. f(inv p)) {p. p permutes S}" (is "?lhs = ?rhs") chaieb@29840: proof- blanchet@30240: let ?S = "{p . p permutes S}" chaieb@29840: have th0: "inj_on inv ?S" chaieb@29840: proof(auto simp add: inj_on_def) chaieb@29840: fix q r blanchet@30240: assume q: "q permutes S" and r: "r permutes S" and qr: "inv q = inv r" chaieb@29840: hence "inv (inv q) = inv (inv r)" by simp chaieb@29840: with permutes_inv_inv[OF q] permutes_inv_inv[OF r] chaieb@29840: show "q = r" by metis chaieb@29840: qed chaieb@29840: have th1: "inv ` ?S = ?S" using image_inverse_permutations by blast chaieb@29840: have th2: "?rhs = setsum (f o inv) ?S" by (simp add: o_def) chaieb@29840: from setsum_reindex[OF th0, of f] show ?thesis unfolding th1 th2 . chaieb@29840: qed chaieb@29840: chaieb@29840: lemma setum_permutations_compose_left: blanchet@30240: assumes q: "q permutes S" blanchet@30240: shows "setsum f {p. p permutes S} = blanchet@30240: setsum (\p. f(q o p)) {p. p permutes S}" (is "?lhs = ?rhs") chaieb@29840: proof- blanchet@30240: let ?S = "{p. p permutes S}" chaieb@29840: have th0: "?rhs = setsum (f o (op o q)) ?S" by (simp add: o_def) chaieb@29840: have th1: "inj_on (op o q) ?S" chaieb@29840: apply (auto simp add: inj_on_def) chaieb@29840: proof- chaieb@29840: fix p r blanchet@30240: assume "p permutes S" and r:"r permutes S" and rp: "q \ p = q \ r" chaieb@29840: hence "inv q o q o p = inv q o q o r" by (simp add: o_assoc[symmetric]) chaieb@29840: with permutes_inj[OF q, unfolded inj_iff] chaieb@29840: chaieb@29840: show "p = r" by simp chaieb@29840: qed chaieb@29840: have th3: "(op o q) ` ?S = ?S" using image_compose_permutations_left[OF q] by auto chaieb@29840: from setsum_reindex[OF th1, of f] chaieb@29840: show ?thesis unfolding th0 th1 th3 . chaieb@29840: qed chaieb@29840: chaieb@29840: lemma sum_permutations_compose_right: blanchet@30240: assumes q: "q permutes S" blanchet@30240: shows "setsum f {p. p permutes S} = blanchet@30240: setsum (\p. f(p o q)) {p. p permutes S}" (is "?lhs = ?rhs") chaieb@29840: proof- blanchet@30240: let ?S = "{p. p permutes S}" chaieb@29840: have th0: "?rhs = setsum (f o (\p. p o q)) ?S" by (simp add: o_def) chaieb@29840: have th1: "inj_on (\p. p o q) ?S" chaieb@29840: apply (auto simp add: inj_on_def) chaieb@29840: proof- chaieb@29840: fix p r blanchet@30240: assume "p permutes S" and r:"r permutes S" and rp: "p o q = r o q" chaieb@29840: hence "p o (q o inv q) = r o (q o inv q)" by (simp add: o_assoc) chaieb@29840: with permutes_surj[OF q, unfolded surj_iff] chaieb@29840: chaieb@29840: show "p = r" by simp chaieb@29840: qed chaieb@29840: have th3: "(\p. p o q) ` ?S = ?S" using image_compose_permutations_right[OF q] by auto chaieb@29840: from setsum_reindex[OF th1, of f] chaieb@29840: show ?thesis unfolding th0 th1 th3 . chaieb@29840: qed chaieb@29840: chaieb@29840: (* ------------------------------------------------------------------------- *) chaieb@29840: (* Sum over a set of permutations (could generalize to iteration). *) chaieb@29840: (* ------------------------------------------------------------------------- *) chaieb@29840: chaieb@29840: lemma setsum_over_permutations_insert: chaieb@29840: assumes fS: "finite S" and aS: "a \ S" chaieb@29840: shows "setsum f {p. p permutes (insert a S)} = setsum (\b. setsum (\q. f (Fun.swap a b id o q)) {p. p permutes S}) (insert a S)" chaieb@29840: proof- chaieb@29840: have th0: "\f a b. (\(b,p). f (Fun.swap a b id o p)) = f o (\(b,p). Fun.swap a b id o p)" chaieb@29840: by (simp add: expand_fun_eq) chaieb@29840: have th1: "\P Q. P \ Q = {(a,b). a \ P \ b \ Q}" by blast chaieb@29840: have th2: "\P Q. P \ (P \ Q) \ P \ Q" by blast chaieb@29840: show ?thesis chaieb@29840: unfolding permutes_insert chaieb@29840: unfolding setsum_cartesian_product chaieb@29840: unfolding th1[symmetric] chaieb@29840: unfolding th0 chaieb@29840: proof(rule setsum_reindex) chaieb@29840: let ?f = "(\(b, y). Fun.swap a b id \ y)" chaieb@29840: let ?P = "{p. p permutes S}" chaieb@29840: {fix b c p q assume b: "b \ insert a S" and c: "c \ insert a S" chaieb@29840: and p: "p permutes S" and q: "q permutes S" chaieb@29840: and eq: "Fun.swap a b id o p = Fun.swap a c id o q" chaieb@29840: from p q aS have pa: "p a = a" and qa: "q a = a" chaieb@29840: unfolding permutes_def by metis+ chaieb@29840: from eq have "(Fun.swap a b id o p) a = (Fun.swap a c id o q) a" by simp chaieb@29840: hence bc: "b = c" chaieb@29840: apply (simp add: permutes_def pa qa o_def fun_upd_def swap_def id_def cong del: if_weak_cong) chaieb@29840: apply (cases "a = b", auto) chaieb@29840: by (cases "b = c", auto) chaieb@29840: from eq[unfolded bc] have "(\p. Fun.swap a c id o p) (Fun.swap a c id o p) = (\p. Fun.swap a c id o p) (Fun.swap a c id o q)" by simp chaieb@29840: hence "p = q" unfolding o_assoc swap_id_idempotent chaieb@29840: by (simp add: o_def) chaieb@29840: with bc have "b = c \ p = q" by blast chaieb@29840: } chaieb@29840: chaieb@29840: then show "inj_on ?f (insert a S \ ?P)" chaieb@29840: unfolding inj_on_def chaieb@29840: apply clarify by metis chaieb@29840: qed chaieb@29840: qed chaieb@29840: chaieb@29840: end