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