wenzelm@41959: (* Title: HOL/Library/Permutations.thy wenzelm@41959: 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 huffman@36335: imports Parity Fact chaieb@29840: begin 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: huffman@30488: lemma swapid_sym: "Fun.swap a b id = Fun.swap b a id" nipkow@39302: by (auto simp add: fun_eq_iff 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" nipkow@39302: using fg gf inv_equality[of g f] by (auto simp add: fun_eq_iff) 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 huffman@30488: unfolding permutes_def huffman@30488: apply - nipkow@39302: apply (rule set_eqI) chaieb@29840: apply (simp add: image_iff) chaieb@29840: apply metis chaieb@29840: done chaieb@29840: huffman@30488: lemma permutes_inj: "p permutes S ==> inj p " huffman@30488: unfolding permutes_def inj_on_def by blast chaieb@29840: huffman@30488: lemma permutes_surj: "p permutes s ==> surj p" huffman@30488: 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: huffman@30488: 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" nipkow@39302: using permutes_inv_o[OF pS, unfolded fun_eq_iff 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" nipkow@39302: unfolding fun_eq_iff permutes_def apply simp by metis chaieb@29840: chaieb@29840: lemma permutes_sing[simp]: "p permutes {a} \ p = id" nipkow@39302: unfolding fun_eq_iff permutes_def apply simp by metis huffman@30488: 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" nipkow@33057: 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" nipkow@32988: unfolding permutes_def swap_def fun_upd_def by auto metis chaieb@29840: nipkow@32988: lemma permutes_superset: nipkow@32988: "p permutes S \ (\x \ S - T. p x = x) \ p permutes T" huffman@36361: by (simp add: Ball_def permutes_def) metis chaieb@29840: chaieb@29840: (* ------------------------------------------------------------------------- *) chaieb@29840: (* Group properties. *) chaieb@29840: (* ------------------------------------------------------------------------- *) chaieb@29840: huffman@30488: 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" huffman@30488: 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" nipkow@39302: unfolding fun_eq_iff 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: huffman@30488: 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 huffman@36361: apply (auto simp add: Ball_def 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: huffman@30488: {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" nipkow@39302: have th0: "p = Fun.swap a ?b id o ?q" unfolding fun_eq_iff o_assoc by simp huffman@30488: 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" huffman@30488: 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: hoelzl@33715: lemma card_permutations: assumes Sn: "card S = n" and fS: "finite S" hoelzl@33715: shows "card {p. p permutes S} = fact n" hoelzl@33715: using fS Sn proof (induct arbitrary: n) huffman@36361: case empty thus ?case by simp hoelzl@33715: next hoelzl@33715: case (insert x F) hoelzl@33715: { fix n assume H0: "card (insert x F) = n" hoelzl@33715: let ?xF = "{p. p permutes insert x F}" hoelzl@33715: let ?pF = "{p. p permutes F}" hoelzl@33715: let ?pF' = "{(b, p). b \ insert x F \ p \ ?pF}" hoelzl@33715: let ?g = "(\(b, p). Fun.swap x b id \ p)" hoelzl@33715: from permutes_insert[of x F] hoelzl@33715: have xfgpF': "?xF = ?g ` ?pF'" . hoelzl@33715: have Fs: "card F = n - 1" using `x \ F` H0 `finite F` by auto hoelzl@33715: from insert.hyps Fs have pFs: "card ?pF = fact (n - 1)" using `finite F` by auto hoelzl@33715: moreover hence "finite ?pF" using fact_gt_zero_nat by (auto intro: card_ge_0_finite) hoelzl@33715: ultimately have pF'f: "finite ?pF'" using H0 `finite F` hoelzl@33715: apply (simp only: Collect_split Collect_mem_eq) hoelzl@33715: apply (rule finite_cartesian_product) hoelzl@33715: apply simp_all hoelzl@33715: done chaieb@29840: hoelzl@33715: have ginj: "inj_on ?g ?pF'" hoelzl@33715: proof- hoelzl@33715: { hoelzl@33715: fix b p c q assume bp: "(b,p) \ ?pF'" and cq: "(c,q) \ ?pF'" hoelzl@33715: and eq: "?g (b,p) = ?g (c,q)" hoelzl@33715: 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 hoelzl@33715: from ths(4) `x \ F` eq have "b = ?g (b,p) x" unfolding permutes_def nipkow@39302: by (auto simp add: swap_def fun_upd_def fun_eq_iff) hoelzl@33715: also have "\ = ?g (c,q) x" using ths(5) `x \ F` eq nipkow@39302: by (auto simp add: swap_def fun_upd_def fun_eq_iff) hoelzl@33715: also have "\ = c"using ths(5) `x \ F` unfolding permutes_def nipkow@39302: by (auto simp add: swap_def fun_upd_def fun_eq_iff) hoelzl@33715: finally have bc: "b = c" . hoelzl@33715: hence "Fun.swap x b id = Fun.swap x c id" by simp hoelzl@33715: with eq have "Fun.swap x b id o p = Fun.swap x b id o q" by simp hoelzl@33715: 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 hoelzl@33715: hence "p = q" by (simp add: o_assoc) hoelzl@33715: with bc have "(b,p) = (c,q)" by simp hoelzl@33715: } hoelzl@33715: thus ?thesis unfolding inj_on_def by blast hoelzl@33715: qed hoelzl@33715: from `x \ F` H0 have n0: "n \ 0 " using `finite F` by auto hoelzl@33715: hence "\m. n = Suc m" by arith hoelzl@33715: then obtain m where n[simp]: "n = Suc m" by blast hoelzl@33715: from pFs H0 have xFc: "card ?xF = fact n" hoelzl@33715: unfolding xfgpF' card_image[OF ginj] using `finite F` `finite ?pF` hoelzl@33715: apply (simp only: Collect_split Collect_mem_eq card_cartesian_product) hoelzl@33715: by simp hoelzl@33715: from finite_imageI[OF pF'f, of ?g] have xFf: "finite ?xF" unfolding xfgpF' by simp hoelzl@33715: have "card ?xF = fact n" hoelzl@33715: using xFf xFc unfolding xFf by blast hoelzl@33715: } hoelzl@33715: thus ?case using insert by simp chaieb@29840: qed chaieb@29840: hoelzl@33715: lemma finite_permutations: assumes fS: "finite S" shows "finite {p. p permutes S}" hoelzl@33715: using card_permutations[OF refl fS] fact_gt_zero_nat hoelzl@33715: by (auto intro: card_ge_0_finite) chaieb@29840: chaieb@29840: (* ------------------------------------------------------------------------- *) chaieb@29840: (* Permutations of index set for iterated operations. *) chaieb@29840: (* ------------------------------------------------------------------------- *) chaieb@29840: huffman@30488: 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] . huffman@30488: 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: huffman@30488: 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: huffman@30488: lemma setsum_permute_natseg:assumes pS: "p permutes {m .. n}" chaieb@29840: shows "setsum f {m .. n} = setsum (f o p) {m .. n}" huffman@30488: using setsum_permute[OF pS, of f ] pS by blast chaieb@29840: huffman@30488: lemma setprod_permute: assumes pS: "p permutes S" chaieb@29840: shows "setprod f S = setprod (f o p) S" huffman@30488: unfolding setprod_def chaieb@29840: using ab_semigroup_mult_class.fold_image_permute[of S p f 1] pS by clarsimp chaieb@29840: huffman@30488: lemma setprod_permute_natseg:assumes pS: "p permutes {m .. n}" chaieb@29840: shows "setprod f {m .. n} = setprod (f o p) {m .. n}" huffman@30488: 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: nipkow@39302: 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: fun_eq_iff swap_def) chaieb@29840: nipkow@39302: 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: fun_eq_iff 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" nipkow@39302: by (simp add: swap_def fun_eq_iff) 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) huffman@30488: 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 huffman@30488: case (comp_Suc n p a b m q) chaieb@29840: have th: "Suc n + m = Suc (n + m)" by arith huffman@30488: show ?case unfolding th o_assoc[symmetric] huffman@30488: 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) huffman@30488: 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 huffman@30488: 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" . huffman@30488: 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: huffman@30488: lemma swap_general: "a \ b \ c \ d \ Fun.swap a b id o Fun.swap c d id = id \ huffman@30488: (\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" huffman@30488: have "a \ b \ c \ d \ huffman@30488: ( Fun.swap a b id o Fun.swap c d id = id \ huffman@30488: (\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]) huffman@30488: 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) nipkow@39302: apply (clarsimp simp add: fun_eq_iff 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) nipkow@39302: apply (clarsimp simp add: fun_eq_iff 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) nipkow@39302: apply (clarsimp simp add: fun_eq_iff swap_def) chaieb@29840: done huffman@30488: 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" huffman@30488: huffman@30488: have ?case apply (simp only: cdqm o_assoc H) chaieb@29840: by (simp add: cdqm)} chaieb@29840: moreover chaieb@29840: { fix x y z huffman@30488: 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+ huffman@30488: 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} huffman@30488: ultimately show ?case using swap_general[OF Suc.prems(2) cdqm(4)] by metis chaieb@29840: qed chaieb@29840: huffman@30488: 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)" huffman@30488: {assume "n = 0" hence "even n" by arith} huffman@30488: 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: huffman@30488: 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 huffman@30488: 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: huffman@30488: 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- huffman@30488: from p q obtain huffman@30488: 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: huffman@30488: lemma permutation_bijective: huffman@30488: 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 huffman@30488: from swapidseq_inverse_exists[OF n] obtain q where chaieb@29840: q: "swapidseq n q" "p \ q = id" "q \ p = id" by blast nipkow@39302: thus ?thesis unfolding bij_iff apply (auto simp add: fun_eq_iff) apply metis done huffman@30488: 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: huffman@30488: 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]] nipkow@39302: by (simp add: fun_eq_iff 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" huffman@30488: show ?thesis chaieb@29840: unfolding bij_swap_comp[OF H] bij_swap_iff chaieb@29840: using H . chaieb@29840: qed chaieb@29840: huffman@30488: 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)] huffman@30488: have br: "bij ?r" . huffman@30488: huffman@30488: 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: huffman@30488: 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" huffman@44227: using permutation_bijective [OF p] huffman@44227: unfolding bij_def inj_iff surj_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) huffman@30488: 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 huffman@30488: 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 huffman@30488: 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" huffman@30488: unfolding permutation_permutes using insert.hyps(1) chaieb@29840: permutes_insert_lemma[OF insert.prems(3)] by blast huffman@30488: from insert.prems(2)[OF xF pxF Pr Pr rp] huffman@30488: 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: huffman@30488: 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: huffman@30037: 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 huffman@30488: have "p n = n" chaieb@29840: using p le huffman@30037: proof(induct n arbitrary: S rule: less_induct) huffman@30488: fix n S assume H: "\m S. \m < n; p permutes S; \i\S. p i \ i\ \ p m = m" wenzelm@32960: "p permutes S" "\i \S. p i \ i" chaieb@29840: {assume "n \ S" wenzelm@32960: with H(2) have "p n = n" unfolding permutes_def by metis} chaieb@29840: moreover chaieb@29840: {assume ns: "n \ S" wenzelm@32960: from H(3) ns have "p n < n \ p n = n" by auto wenzelm@32960: moreover{assume h: "p n < n" wenzelm@32960: from H h have "p (p n) = p n" by metis wenzelm@32960: with permutes_inj[OF H(2)] have "p n = n" unfolding inj_on_def by blast wenzelm@32960: with h have False by simp} wenzelm@32960: ultimately have "p n = n" by blast } chaieb@29840: ultimately show "p n = n" by blast chaieb@29840: qed} nipkow@39302: thus ?thesis by (auto simp add: fun_eq_iff) chaieb@29840: qed chaieb@29840: chaieb@29840: lemma permutes_natset_ge: huffman@30037: 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 huffman@30488: from permutes_natset_le[OF permutes_inv[OF p] th] chaieb@29840: have "inv p = inv id" by simp huffman@30488: 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}" nipkow@39302: apply (rule set_eqI) 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: huffman@30488: lemma image_compose_permutations_left: chaieb@29840: assumes q: "q permutes S" shows "{q o p | p. p permutes S} = {p . p permutes S}" nipkow@39302: apply (rule set_eqI) 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}" nipkow@39302: apply (rule set_eqI) 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: huffman@30036: 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- huffman@30036: let ?S = "{p . p permutes S}" huffman@30488: have th0: "inj_on inv ?S" chaieb@29840: proof(auto simp add: inj_on_def) chaieb@29840: fix q r huffman@30036: 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: huffman@30036: assumes q: "q permutes S" huffman@30036: shows "setsum f {p. p permutes S} = huffman@30036: setsum (\p. f(q o p)) {p. p permutes S}" (is "?lhs = ?rhs") chaieb@29840: proof- huffman@30036: 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 huffman@30036: 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: huffman@30036: assumes q: "q permutes S" huffman@30036: shows "setsum f {p. p permutes S} = huffman@30036: setsum (\p. f(p o q)) {p. p permutes S}" (is "?lhs = ?rhs") chaieb@29840: proof- huffman@30036: 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 huffman@30036: 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)" nipkow@39302: by (simp add: fun_eq_iff) 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 huffman@30488: show ?thesis huffman@30488: 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}" huffman@30488: {fix b c p q assume b: "b \ insert a S" and c: "c \ insert a S" huffman@30488: 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" wenzelm@32960: 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" wenzelm@32960: 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) 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 wenzelm@32960: by (simp add: o_def) chaieb@29840: with bc have "b = c \ p = q" by blast chaieb@29840: } huffman@30488: huffman@30488: 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