1 (* Title: Library/Permutations
2 Author: Amine Chaieb, University of Cambridge
5 header {* Permutations, both general and specifically on finite sets.*}
8 imports Finite_Cartesian_Product Parity Fact
11 definition permutes (infixr "permutes" 41) where
12 "(p permutes S) \<longleftrightarrow> (\<forall>x. x \<notin> S \<longrightarrow> p x = x) \<and> (\<forall>y. \<exists>!x. p x = y)"
14 (* ------------------------------------------------------------------------- *)
16 (* ------------------------------------------------------------------------- *)
18 declare swap_self[simp]
19 lemma swapid_sym: "Fun.swap a b id = Fun.swap b a id"
20 by (auto simp add: expand_fun_eq swap_def fun_upd_def)
21 lemma swap_id_refl: "Fun.swap a a id = id" by simp
22 lemma swap_id_sym: "Fun.swap a b id = Fun.swap b a id"
23 by (rule ext, simp add: swap_def)
24 lemma swap_id_idempotent[simp]: "Fun.swap a b id o Fun.swap a b id = id"
25 by (rule ext, auto simp add: swap_def)
27 lemma inv_unique_comp: assumes fg: "f o g = id" and gf: "g o f = id"
29 using fg gf inv_equality[of g f] by (auto simp add: expand_fun_eq)
31 lemma inverse_swap_id: "inv (Fun.swap a b id) = Fun.swap a b id"
32 by (rule inv_unique_comp, simp_all)
34 lemma swap_id_eq: "Fun.swap a b id x = (if x = a then b else if x = b then a else x)"
35 by (simp add: swap_def)
37 (* ------------------------------------------------------------------------- *)
38 (* Basic consequences of the definition. *)
39 (* ------------------------------------------------------------------------- *)
41 lemma permutes_in_image: "p permutes S \<Longrightarrow> p x \<in> S \<longleftrightarrow> x \<in> S"
42 unfolding permutes_def by metis
44 lemma permutes_image: assumes pS: "p permutes S" shows "p ` S = S"
46 unfolding permutes_def
49 apply (simp add: image_iff)
53 lemma permutes_inj: "p permutes S ==> inj p "
54 unfolding permutes_def inj_on_def by blast
56 lemma permutes_surj: "p permutes s ==> surj p"
57 unfolding permutes_def surj_def by metis
59 lemma permutes_inv_o: assumes pS: "p permutes S"
60 shows " p o inv p = id"
62 using permutes_inj[OF pS] permutes_surj[OF pS]
63 unfolding inj_iff[symmetric] surj_iff[symmetric] by blast+
66 lemma permutes_inverses:
67 fixes p :: "'a \<Rightarrow> 'a"
68 assumes pS: "p permutes S"
69 shows "p (inv p x) = x"
71 using permutes_inv_o[OF pS, unfolded expand_fun_eq o_def] by auto
73 lemma permutes_subset: "p permutes S \<Longrightarrow> S \<subseteq> T ==> p permutes T"
74 unfolding permutes_def by blast
76 lemma permutes_empty[simp]: "p permutes {} \<longleftrightarrow> p = id"
77 unfolding expand_fun_eq permutes_def apply simp by metis
79 lemma permutes_sing[simp]: "p permutes {a} \<longleftrightarrow> p = id"
80 unfolding expand_fun_eq permutes_def apply simp by metis
82 lemma permutes_univ: "p permutes UNIV \<longleftrightarrow> (\<forall>y. \<exists>!x. p x = y)"
83 unfolding permutes_def by simp
85 lemma permutes_inv_eq: "p permutes S ==> inv p y = x \<longleftrightarrow> p x = y"
86 unfolding permutes_def inv_onto_def apply auto
87 apply (erule allE[where x=y])
88 apply (erule allE[where x=y])
89 apply (rule someI_ex) apply blast
90 apply (rule some1_equality)
95 lemma permutes_swap_id: "a \<in> S \<Longrightarrow> b \<in> S ==> Fun.swap a b id permutes S"
96 unfolding permutes_def swap_def fun_upd_def by auto metis
98 lemma permutes_superset:
99 "p permutes S \<Longrightarrow> (\<forall>x \<in> S - T. p x = x) \<Longrightarrow> p permutes T"
100 by (simp add: Ball_def permutes_def Diff_iff) metis
102 (* ------------------------------------------------------------------------- *)
103 (* Group properties. *)
104 (* ------------------------------------------------------------------------- *)
106 lemma permutes_id: "id permutes S" unfolding permutes_def by simp
108 lemma permutes_compose: "p permutes S \<Longrightarrow> q permutes S ==> q o p permutes S"
109 unfolding permutes_def o_def by metis
111 lemma permutes_inv: assumes pS: "p permutes S" shows "inv p permutes S"
112 using pS unfolding permutes_def permutes_inv_eq[OF pS] by metis
114 lemma permutes_inv_inv: assumes pS: "p permutes S" shows "inv (inv p) = p"
115 unfolding expand_fun_eq permutes_inv_eq[OF pS] permutes_inv_eq[OF permutes_inv[OF pS]]
118 (* ------------------------------------------------------------------------- *)
119 (* The number of permutations on a finite set. *)
120 (* ------------------------------------------------------------------------- *)
122 lemma permutes_insert_lemma:
123 assumes pS: "p permutes (insert a S)"
124 shows "Fun.swap a (p a) id o p permutes S"
125 apply (rule permutes_superset[where S = "insert a S"])
126 apply (rule permutes_compose[OF pS])
127 apply (rule permutes_swap_id, simp)
128 using permutes_in_image[OF pS, of a] apply simp
129 apply (auto simp add: Ball_def Diff_iff swap_def)
132 lemma permutes_insert: "{p. p permutes (insert a S)} =
133 (\<lambda>(b,p). Fun.swap a b id o p) ` {(b,p). b \<in> insert a S \<and> p \<in> {p. p permutes S}}"
137 {assume pS: "p permutes insert a S"
139 let ?q = "Fun.swap a (p a) id o p"
140 have th0: "p = Fun.swap a ?b id o ?q" unfolding expand_fun_eq o_assoc by simp
141 have th1: "?b \<in> insert a S " unfolding permutes_in_image[OF pS] by simp
142 from permutes_insert_lemma[OF pS] th0 th1
143 have "\<exists> b q. p = Fun.swap a b id o q \<and> b \<in> insert a S \<and> q permutes S" by blast}
145 {fix b q assume bq: "p = Fun.swap a b id o q" "b \<in> insert a S" "q permutes S"
146 from permutes_subset[OF bq(3), of "insert a S"]
147 have qS: "q permutes insert a S" by auto
148 have aS: "a \<in> insert a S" by simp
149 from bq(1) permutes_compose[OF qS permutes_swap_id[OF aS bq(2)]]
150 have "p permutes insert a S" by simp }
151 ultimately have "p permutes insert a S \<longleftrightarrow> (\<exists> b q. p = Fun.swap a b id o q \<and> b \<in> insert a S \<and> q permutes S)" by blast}
155 lemma hassize_insert: "a \<notin> F \<Longrightarrow> insert a F hassize n \<Longrightarrow> F hassize (n - 1)"
156 by (auto simp add: hassize_def)
158 lemma hassize_permutations: assumes Sn: "S hassize n"
159 shows "{p. p permutes S} hassize (fact n)"
161 from Sn have fS:"finite S" by (simp add: hassize_def)
163 have "\<forall>n. (S hassize n) \<longrightarrow> ({p. p permutes S} hassize (fact n))"
164 proof(rule finite_induct[where F = S])
165 from fS show "finite S" .
167 show "\<forall>n. ({} hassize n) \<longrightarrow> ({p. p permutes {}} hassize fact n)"
168 by (simp add: hassize_def permutes_empty)
171 assume fF: "finite F" and xF: "x \<notin> F"
172 and H: "\<forall>n. (F hassize n) \<longrightarrow> ({p. p permutes F} hassize fact n)"
173 {fix n assume H0: "insert x F hassize n"
174 let ?xF = "{p. p permutes insert x F}"
175 let ?pF = "{p. p permutes F}"
176 let ?pF' = "{(b, p). b \<in> insert x F \<and> p \<in> ?pF}"
177 let ?g = "(\<lambda>(b, p). Fun.swap x b id \<circ> p)"
178 from permutes_insert[of x F]
179 have xfgpF': "?xF = ?g ` ?pF'" .
180 from hassize_insert[OF xF H0] have Fs: "F hassize (n - 1)" .
181 from H Fs have pFs: "?pF hassize fact (n - 1)" by blast
182 hence pF'f: "finite ?pF'" using H0 unfolding hassize_def
183 apply (simp only: Collect_split Collect_mem_eq)
184 apply (rule finite_cartesian_product)
188 have ginj: "inj_on ?g ?pF'"
191 fix b p c q assume bp: "(b,p) \<in> ?pF'" and cq: "(c,q) \<in> ?pF'"
192 and eq: "?g (b,p) = ?g (c,q)"
193 from bp cq have ths: "b \<in> insert x F" "c \<in> insert x F" "x \<in> insert x F" "p permutes F" "q permutes F" by auto
194 from ths(4) xF eq have "b = ?g (b,p) x" unfolding permutes_def
195 by (auto simp add: swap_def fun_upd_def expand_fun_eq)
196 also have "\<dots> = ?g (c,q) x" using ths(5) xF eq
197 by (auto simp add: swap_def fun_upd_def expand_fun_eq)
198 also have "\<dots> = c"using ths(5) xF unfolding permutes_def
199 by (auto simp add: swap_def fun_upd_def expand_fun_eq)
200 finally have bc: "b = c" .
201 hence "Fun.swap x b id = Fun.swap x c id" by simp
202 with eq have "Fun.swap x b id o p = Fun.swap x b id o q" by simp
203 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
204 hence "p = q" by (simp add: o_assoc)
205 with bc have "(b,p) = (c,q)" by simp }
206 thus ?thesis unfolding inj_on_def by blast
208 from xF H0 have n0: "n \<noteq> 0 " by (auto simp add: hassize_def)
209 hence "\<exists>m. n = Suc m" by arith
210 then obtain m where n[simp]: "n = Suc m" by blast
211 from pFs H0 have xFc: "card ?xF = fact n"
212 unfolding xfgpF' card_image[OF ginj] hassize_def
213 apply (simp only: Collect_split Collect_mem_eq card_cartesian_product)
215 from finite_imageI[OF pF'f, of ?g] have xFf: "finite ?xF" unfolding xfgpF' by simp
216 have "?xF hassize fact n"
218 unfolding hassize_def xFf by blast }
219 thus "\<forall>n. (insert x F hassize n) \<longrightarrow> ({p. p permutes insert x F} hassize fact n)"
222 with Sn show ?thesis by blast
225 lemma finite_permutations: "finite S ==> finite {p. p permutes S}"
226 using hassize_permutations[of S] unfolding hassize_def by blast
228 (* ------------------------------------------------------------------------- *)
229 (* Permutations of index set for iterated operations. *)
230 (* ------------------------------------------------------------------------- *)
232 lemma (in ab_semigroup_mult) fold_image_permute: assumes fS: "finite S" and pS: "p permutes S"
233 shows "fold_image times f z S = fold_image times (f o p) z S"
234 using fold_image_reindex[OF fS subset_inj_on[OF permutes_inj[OF pS], of S, simplified], of f z]
235 unfolding permutes_image[OF pS] .
236 lemma (in ab_semigroup_add) fold_image_permute: assumes fS: "finite S" and pS: "p permutes S"
237 shows "fold_image plus f z S = fold_image plus (f o p) z S"
239 interpret ab_semigroup_mult plus apply unfold_locales apply (simp add: add_assoc)
240 apply (simp add: add_commute) done
241 from fold_image_reindex[OF fS subset_inj_on[OF permutes_inj[OF pS], of S, simplified], of f z]
243 unfolding permutes_image[OF pS] .
246 lemma setsum_permute: assumes pS: "p permutes S"
247 shows "setsum f S = setsum (f o p) S"
248 unfolding setsum_def using fold_image_permute[of S p f 0] pS by clarsimp
250 lemma setsum_permute_natseg:assumes pS: "p permutes {m .. n}"
251 shows "setsum f {m .. n} = setsum (f o p) {m .. n}"
252 using setsum_permute[OF pS, of f ] pS by blast
254 lemma setprod_permute: assumes pS: "p permutes S"
255 shows "setprod f S = setprod (f o p) S"
256 unfolding setprod_def
257 using ab_semigroup_mult_class.fold_image_permute[of S p f 1] pS by clarsimp
259 lemma setprod_permute_natseg:assumes pS: "p permutes {m .. n}"
260 shows "setprod f {m .. n} = setprod (f o p) {m .. n}"
261 using setprod_permute[OF pS, of f ] pS by blast
263 (* ------------------------------------------------------------------------- *)
264 (* Various combinations of transpositions with 2, 1 and 0 common elements. *)
265 (* ------------------------------------------------------------------------- *)
267 lemma swap_id_common:" a \<noteq> c \<Longrightarrow> b \<noteq> c \<Longrightarrow> Fun.swap a b id o Fun.swap a c id = Fun.swap b c id o Fun.swap a b id" by (simp add: expand_fun_eq swap_def)
269 lemma swap_id_common': "~(a = b) \<Longrightarrow> ~(a = c) \<Longrightarrow> Fun.swap a c id o Fun.swap b c id = Fun.swap b c id o Fun.swap a b id" by (simp add: expand_fun_eq swap_def)
271 lemma swap_id_independent: "~(a = c) \<Longrightarrow> ~(a = d) \<Longrightarrow> ~(b = c) \<Longrightarrow> ~(b = d) ==> Fun.swap a b id o Fun.swap c d id = Fun.swap c d id o Fun.swap a b id"
272 by (simp add: swap_def expand_fun_eq)
274 (* ------------------------------------------------------------------------- *)
275 (* Permutations as transposition sequences. *)
276 (* ------------------------------------------------------------------------- *)
279 inductive swapidseq :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> bool" where
280 id[simp]: "swapidseq 0 id"
281 | comp_Suc: "swapidseq n p \<Longrightarrow> a \<noteq> b \<Longrightarrow> swapidseq (Suc n) (Fun.swap a b id o p)"
283 declare id[unfolded id_def, simp]
284 definition "permutation p \<longleftrightarrow> (\<exists>n. swapidseq n p)"
286 (* ------------------------------------------------------------------------- *)
287 (* Some closure properties of the set of permutations, with lengths. *)
288 (* ------------------------------------------------------------------------- *)
290 lemma permutation_id[simp]: "permutation id"unfolding permutation_def
291 by (rule exI[where x=0], simp)
292 declare permutation_id[unfolded id_def, simp]
294 lemma swapidseq_swap: "swapidseq (if a = b then 0 else 1) (Fun.swap a b id)"
296 using comp_Suc[of 0 id a b] by simp
298 lemma permutation_swap_id: "permutation (Fun.swap a b id)"
299 apply (cases "a=b", simp_all)
300 unfolding permutation_def using swapidseq_swap[of a b] by blast
302 lemma swapidseq_comp_add: "swapidseq n p \<Longrightarrow> swapidseq m q ==> swapidseq (n + m) (p o q)"
303 proof (induct n p arbitrary: m q rule: swapidseq.induct)
304 case (id m q) thus ?case by simp
306 case (comp_Suc n p a b m q)
307 have th: "Suc n + m = Suc (n + m)" by arith
308 show ?case unfolding th o_assoc[symmetric]
309 apply (rule swapidseq.comp_Suc) using comp_Suc.hyps(2)[OF comp_Suc.prems] comp_Suc.hyps(3) by blast+
312 lemma permutation_compose: "permutation p \<Longrightarrow> permutation q ==> permutation(p o q)"
313 unfolding permutation_def using swapidseq_comp_add[of _ p _ q] by metis
315 lemma swapidseq_endswap: "swapidseq n p \<Longrightarrow> a \<noteq> b ==> swapidseq (Suc n) (p o Fun.swap a b id)"
316 apply (induct n p rule: swapidseq.induct)
317 using swapidseq_swap[of a b]
318 by (auto simp add: o_assoc[symmetric] intro: swapidseq.comp_Suc)
320 lemma swapidseq_inverse_exists: "swapidseq n p ==> \<exists>q. swapidseq n q \<and> p o q = id \<and> q o p = id"
321 proof(induct n p rule: swapidseq.induct)
322 case id thus ?case by (rule exI[where x=id], simp)
324 case (comp_Suc n p a b)
325 from comp_Suc.hyps obtain q where q: "swapidseq n q" "p \<circ> q = id" "q \<circ> p = id" by blast
326 let ?q = "q o Fun.swap a b id"
327 note H = comp_Suc.hyps
328 from swapidseq_swap[of a b] H(3) have th0: "swapidseq 1 (Fun.swap a b id)" by simp
329 from swapidseq_comp_add[OF q(1) th0] have th1:"swapidseq (Suc n) ?q" by simp
330 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)
331 also have "\<dots> = id" by (simp add: q(2))
332 finally have th2: "Fun.swap a b id o p o ?q = id" .
333 have "?q \<circ> (Fun.swap a b id \<circ> p) = q \<circ> (Fun.swap a b id o Fun.swap a b id) \<circ> p" by (simp only: o_assoc)
334 hence "?q \<circ> (Fun.swap a b id \<circ> p) = id" by (simp add: q(3))
335 with th1 th2 show ?case by blast
339 lemma swapidseq_inverse: assumes H: "swapidseq n p" shows "swapidseq n (inv p)"
340 using swapidseq_inverse_exists[OF H] inv_unique_comp[of p] by auto
342 lemma permutation_inverse: "permutation p ==> permutation (inv p)"
343 using permutation_def swapidseq_inverse by blast
345 (* ------------------------------------------------------------------------- *)
346 (* The identity map only has even transposition sequences. *)
347 (* ------------------------------------------------------------------------- *)
349 lemma symmetry_lemma:"(\<And>a b c d. P a b c d ==> P a b d c) \<Longrightarrow>
350 (\<And>a b c d. a \<noteq> b \<Longrightarrow> c \<noteq> d \<Longrightarrow> (a = c \<and> b = d \<or> a = c \<and> b \<noteq> d \<or> a \<noteq> c \<and> b = d \<or> a \<noteq> c \<and> a \<noteq> d \<and> b \<noteq> c \<and> b \<noteq> d) ==> P a b c d)
351 ==> (\<And>a b c d. a \<noteq> b --> c \<noteq> d \<longrightarrow> P a b c d)" by metis
353 lemma swap_general: "a \<noteq> b \<Longrightarrow> c \<noteq> d \<Longrightarrow> Fun.swap a b id o Fun.swap c d id = id \<or>
354 (\<exists>x y z. x \<noteq> a \<and> y \<noteq> a \<and> z \<noteq> a \<and> x \<noteq> y \<and> Fun.swap a b id o Fun.swap c d id = Fun.swap x y id o Fun.swap a z id)"
356 assume H: "a\<noteq>b" "c\<noteq>d"
357 have "a \<noteq> b \<longrightarrow> c \<noteq> d \<longrightarrow>
358 ( Fun.swap a b id o Fun.swap c d id = id \<or>
359 (\<exists>x y z. x \<noteq> a \<and> y \<noteq> a \<and> z \<noteq> a \<and> x \<noteq> y \<and> Fun.swap a b id o Fun.swap c d id = Fun.swap x y id o Fun.swap a z id))"
360 apply (rule symmetry_lemma[where a=a and b=b and c=c and d=d])
361 apply (simp_all only: swapid_sym)
362 apply (case_tac "a = c \<and> b = d", clarsimp simp only: swapid_sym swap_id_idempotent)
363 apply (case_tac "a = c \<and> b \<noteq> d")
365 apply (rule_tac x="b" in exI)
366 apply (rule_tac x="d" in exI)
367 apply (rule_tac x="b" in exI)
368 apply (clarsimp simp add: expand_fun_eq swap_def)
369 apply (case_tac "a \<noteq> c \<and> b = d")
371 apply (rule_tac x="c" in exI)
372 apply (rule_tac x="d" in exI)
373 apply (rule_tac x="c" in exI)
374 apply (clarsimp simp add: expand_fun_eq swap_def)
376 apply (rule_tac x="c" in exI)
377 apply (rule_tac x="d" in exI)
378 apply (rule_tac x="b" in exI)
379 apply (clarsimp simp add: expand_fun_eq swap_def)
381 with H show ?thesis by metis
384 lemma swapidseq_id_iff[simp]: "swapidseq 0 p \<longleftrightarrow> p = id"
385 using swapidseq.cases[of 0 p "p = id"]
388 lemma swapidseq_cases: "swapidseq n p \<longleftrightarrow> (n=0 \<and> p = id \<or> (\<exists>a b q m. n = Suc m \<and> p = Fun.swap a b id o q \<and> swapidseq m q \<and> a\<noteq> b))"
390 apply (erule swapidseq.cases[of n p])
393 apply (rule_tac x= "a" in exI)
394 apply (rule_tac x= "b" in exI)
395 apply (rule_tac x= "pa" in exI)
396 apply (rule_tac x= "na" in exI)
399 apply (rule comp_Suc, simp_all)
401 lemma fixing_swapidseq_decrease:
402 assumes spn: "swapidseq n p" and ab: "a\<noteq>b" and pa: "(Fun.swap a b id o p) a = a"
403 shows "n \<noteq> 0 \<and> swapidseq (n - 1) (Fun.swap a b id o p)"
405 proof(induct n arbitrary: p a b)
406 case 0 thus ?case by (auto simp add: swap_def fun_upd_def)
409 from Suc.prems(1) swapidseq_cases[of "Suc n" p] obtain
410 c d q m where cdqm: "Suc n = Suc m" "p = Fun.swap c d id o q" "swapidseq m q" "c \<noteq> d" "n = m"
412 {assume H: "Fun.swap a b id o Fun.swap c d id = id"
414 have ?case apply (simp only: cdqm o_assoc H)
418 assume H: "x\<noteq>a" "y\<noteq>a" "z \<noteq>a" "x \<noteq>y"
419 "Fun.swap a b id o Fun.swap c d id = Fun.swap x y id o Fun.swap a z id"
420 from H have az: "a \<noteq> z" by simp
422 {fix h have "(Fun.swap x y id o h) a = a \<longleftrightarrow> h a = a"
423 using H by (simp add: swap_def)}
425 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
426 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)
427 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
428 hence "(Fun.swap x y id o (Fun.swap a z id o q)) a = a" unfolding Suc by metis
429 hence th1: "(Fun.swap a z id o q) a = a" unfolding th3 .
430 from Suc.hyps[OF cdqm(3)[ unfolded cdqm(5)[symmetric]] az th1]
431 have th2: "swapidseq (n - 1) (Fun.swap a z id o q)" "n \<noteq> 0" by blast+
432 have th: "Suc n - 1 = Suc (n - 1)" using th2(2) by auto
433 have ?case unfolding cdqm(2) H o_assoc th
434 apply (simp only: Suc_not_Zero simp_thms o_assoc[symmetric])
435 apply (rule comp_Suc)
436 using th2 H apply blast+
438 ultimately show ?case using swap_general[OF Suc.prems(2) cdqm(4)] by metis
441 lemma swapidseq_identity_even:
442 assumes "swapidseq n (id :: 'a \<Rightarrow> 'a)" shows "even n"
443 using `swapidseq n id`
444 proof(induct n rule: nat_less_induct)
446 assume H: "\<forall>m<n. swapidseq m (id::'a \<Rightarrow> 'a) \<longrightarrow> even m" "swapidseq n (id :: 'a \<Rightarrow> 'a)"
447 {assume "n = 0" hence "even n" by arith}
449 {fix a b :: 'a and q m
450 assume h: "n = Suc m" "(id :: 'a \<Rightarrow> 'a) = Fun.swap a b id \<circ> q" "swapidseq m q" "a \<noteq> b"
451 from fixing_swapidseq_decrease[OF h(3,4), unfolded h(2)[symmetric]]
452 have m: "m \<noteq> 0" "swapidseq (m - 1) (id :: 'a \<Rightarrow> 'a)" by auto
453 from h m have mn: "m - 1 < n" by arith
454 from H(1)[rule_format, OF mn m(2)] h(1) m(1) have "even n" apply arith done}
455 ultimately show "even n" using H(2)[unfolded swapidseq_cases[of n id]] by auto
458 (* ------------------------------------------------------------------------- *)
459 (* Therefore we have a welldefined notion of parity. *)
460 (* ------------------------------------------------------------------------- *)
462 definition "evenperm p = even (SOME n. swapidseq n p)"
464 lemma swapidseq_even_even: assumes
465 m: "swapidseq m p" and n: "swapidseq n p"
466 shows "even m \<longleftrightarrow> even n"
468 from swapidseq_inverse_exists[OF n]
469 obtain q where q: "swapidseq n q" "p \<circ> q = id" "q \<circ> p = id" by blast
471 from swapidseq_identity_even[OF swapidseq_comp_add[OF m q(1), unfolded q]]
472 show ?thesis by arith
475 lemma evenperm_unique: assumes p: "swapidseq n p" and n:"even n = b"
476 shows "evenperm p = b"
477 unfolding n[symmetric] evenperm_def
478 apply (rule swapidseq_even_even[where p = p])
479 apply (rule someI[where x = n])
482 (* ------------------------------------------------------------------------- *)
483 (* And it has the expected composition properties. *)
484 (* ------------------------------------------------------------------------- *)
486 lemma evenperm_id[simp]: "evenperm id = True"
487 apply (rule evenperm_unique[where n = 0]) by simp_all
489 lemma evenperm_swap: "evenperm (Fun.swap a b id) = (a = b)"
490 apply (rule evenperm_unique[where n="if a = b then 0 else 1"])
491 by (simp_all add: swapidseq_swap)
494 assumes p: "permutation p" and q:"permutation q"
495 shows "evenperm (p o q) = (evenperm p = evenperm q)"
498 n m where n: "swapidseq n p" and m: "swapidseq m q"
499 unfolding permutation_def by blast
500 note nm = swapidseq_comp_add[OF n m]
501 have th: "even (n + m) = (even n \<longleftrightarrow> even m)" by arith
502 from evenperm_unique[OF n refl] evenperm_unique[OF m refl]
503 evenperm_unique[OF nm th]
504 show ?thesis by blast
507 lemma evenperm_inv: assumes p: "permutation p"
508 shows "evenperm (inv p) = evenperm p"
510 from p obtain n where n: "swapidseq n p" unfolding permutation_def by blast
511 from evenperm_unique[OF swapidseq_inverse[OF n] evenperm_unique[OF n refl, symmetric]]
515 (* ------------------------------------------------------------------------- *)
516 (* A more abstract characterization of permutations. *)
517 (* ------------------------------------------------------------------------- *)
520 lemma bij_iff: "bij f \<longleftrightarrow> (\<forall>x. \<exists>!y. f y = x)"
521 unfolding bij_def inj_on_def surj_def
527 lemma permutation_bijective:
528 assumes p: "permutation p"
531 from p obtain n where n: "swapidseq n p" unfolding permutation_def by blast
532 from swapidseq_inverse_exists[OF n] obtain q where
533 q: "swapidseq n q" "p \<circ> q = id" "q \<circ> p = id" by blast
534 thus ?thesis unfolding bij_iff apply (auto simp add: expand_fun_eq) apply metis done
537 lemma permutation_finite_support: assumes p: "permutation p"
538 shows "finite {x. p x \<noteq> x}"
540 from p obtain n where n: "swapidseq n p" unfolding permutation_def by blast
542 proof(induct n p rule: swapidseq.induct)
543 case id thus ?case by simp
545 case (comp_Suc n p a b)
546 let ?S = "insert a (insert b {x. p x \<noteq> x})"
547 from comp_Suc.hyps(2) have fS: "finite ?S" by simp
548 from `a \<noteq> b` have th: "{x. (Fun.swap a b id o p) x \<noteq> x} \<subseteq> ?S"
549 by (auto simp add: swap_def)
550 from finite_subset[OF th fS] show ?case .
554 lemma bij_inv_eq_iff: "bij p ==> x = inv p y \<longleftrightarrow> p x = y"
555 using surj_f_inv_f[of p] inv_f_f[of f] by (auto simp add: bij_def)
558 assumes bp: "bij p" shows "Fun.swap a b id o p = Fun.swap (inv p a) (inv p b) p"
559 using surj_f_inv_f[OF bij_is_surj[OF bp]]
560 by (simp add: expand_fun_eq swap_def bij_inv_eq_iff[OF bp])
562 lemma bij_swap_ompose_bij: "bij p \<Longrightarrow> bij (Fun.swap a b id o p)"
566 unfolding bij_swap_comp[OF H] bij_swap_iff
570 lemma permutation_lemma:
571 assumes fS: "finite S" and p: "bij p" and pS: "\<forall>x. x\<notin> S \<longrightarrow> p x = x"
572 shows "permutation p"
574 proof(induct S arbitrary: p rule: finite_induct)
575 case (empty p) thus ?case by simp
578 let ?r = "Fun.swap a (p a) id o p"
579 let ?q = "Fun.swap a (p a) id o ?r "
580 have raa: "?r a = a" by (simp add: swap_def)
581 from bij_swap_ompose_bij[OF insert(4)]
584 from insert raa have th: "\<forall>x. x \<notin> F \<longrightarrow> ?r x = x"
585 apply (clarsimp simp add: swap_def)
586 apply (erule_tac x="x" in allE)
588 unfolding bij_iff apply metis
590 from insert(3)[OF br th]
591 have rp: "permutation ?r" .
592 have "permutation ?q" by (simp add: permutation_compose permutation_swap_id rp)
593 thus ?case by (simp add: o_assoc)
596 lemma permutation: "permutation p \<longleftrightarrow> bij p \<and> finite {x. p x \<noteq> x}"
597 (is "?lhs \<longleftrightarrow> ?b \<and> ?f")
600 from p permutation_bijective permutation_finite_support show "?b \<and> ?f" by auto
602 assume bf: "?b \<and> ?f"
603 hence bf: "?f" "?b" by blast+
604 from permutation_lemma[OF bf] show ?lhs by blast
607 lemma permutation_inverse_works: assumes p: "permutation p"
608 shows "inv p o p = id" "p o inv p = id"
609 using permutation_bijective[OF p] surj_iff bij_def inj_iff by auto
611 lemma permutation_inverse_compose:
612 assumes p: "permutation p" and q: "permutation q"
613 shows "inv (p o q) = inv q o inv p"
615 note ps = permutation_inverse_works[OF p]
616 note qs = permutation_inverse_works[OF q]
617 have "p o q o (inv q o inv p) = p o (q o inv q) o inv p" by (simp add: o_assoc)
618 also have "\<dots> = id" by (simp add: ps qs)
619 finally have th0: "p o q o (inv q o inv p) = id" .
620 have "inv q o inv p o (p o q) = inv q o (inv p o p) o q" by (simp add: o_assoc)
621 also have "\<dots> = id" by (simp add: ps qs)
622 finally have th1: "inv q o inv p o (p o q) = id" .
623 from inv_unique_comp[OF th0 th1] show ?thesis .
626 (* ------------------------------------------------------------------------- *)
627 (* Relation to "permutes". *)
628 (* ------------------------------------------------------------------------- *)
630 lemma permutation_permutes: "permutation p \<longleftrightarrow> (\<exists>S. finite S \<and> p permutes S)"
631 unfolding permutation permutes_def bij_iff[symmetric]
632 apply (rule iffI, clarify)
633 apply (rule exI[where x="{x. p x \<noteq> x}"])
636 apply (rule_tac B="S" in finite_subset)
640 (* ------------------------------------------------------------------------- *)
641 (* Hence a sort of induction principle composing by swaps. *)
642 (* ------------------------------------------------------------------------- *)
644 lemma permutes_induct: "finite S \<Longrightarrow> P id \<Longrightarrow> (\<And> a b p. a \<in> S \<Longrightarrow> b \<in> S \<Longrightarrow> P p \<Longrightarrow> P p \<Longrightarrow> permutation p ==> P (Fun.swap a b id o p))
645 ==> (\<And>p. p permutes S ==> P p)"
646 proof(induct S rule: finite_induct)
647 case empty thus ?case by auto
650 let ?r = "Fun.swap x (p x) id o p"
651 let ?q = "Fun.swap x (p x) id o ?r"
652 have qp: "?q = p" by (simp add: o_assoc)
653 from permutes_insert_lemma[OF insert.prems(3)] insert have Pr: "P ?r" by blast
654 from permutes_in_image[OF insert.prems(3), of x]
655 have pxF: "p x \<in> insert x F" by simp
656 have xF: "x \<in> insert x F" by simp
657 have rp: "permutation ?r"
658 unfolding permutation_permutes using insert.hyps(1)
659 permutes_insert_lemma[OF insert.prems(3)] by blast
660 from insert.prems(2)[OF xF pxF Pr Pr rp]
661 show ?case unfolding qp .
664 (* ------------------------------------------------------------------------- *)
665 (* Sign of a permutation as a real number. *)
666 (* ------------------------------------------------------------------------- *)
668 definition "sign p = (if evenperm p then (1::int) else -1)"
670 lemma sign_nz: "sign p \<noteq> 0" by (simp add: sign_def)
671 lemma sign_id: "sign id = 1" by (simp add: sign_def)
672 lemma sign_inverse: "permutation p ==> sign (inv p) = sign p"
673 by (simp add: sign_def evenperm_inv)
674 lemma sign_compose: "permutation p \<Longrightarrow> permutation q ==> sign (p o q) = sign(p) * sign(q)" by (simp add: sign_def evenperm_comp)
675 lemma sign_swap_id: "sign (Fun.swap a b id) = (if a = b then 1 else -1)"
676 by (simp add: sign_def evenperm_swap)
677 lemma sign_idempotent: "sign p * sign p = 1" by (simp add: sign_def)
679 (* ------------------------------------------------------------------------- *)
680 (* More lemmas about permutations. *)
681 (* ------------------------------------------------------------------------- *)
683 lemma permutes_natset_le:
684 assumes p: "p permutes (S::'a::wellorder set)" and le: "\<forall>i \<in> S. p i <= i" shows "p = id"
689 proof(induct n arbitrary: S rule: less_induct)
690 fix n S assume H: "\<And>m S. \<lbrakk>m < n; p permutes S; \<forall>i\<in>S. p i \<le> i\<rbrakk> \<Longrightarrow> p m = m"
691 "p permutes S" "\<forall>i \<in>S. p i \<le> i"
692 {assume "n \<notin> S"
693 with H(2) have "p n = n" unfolding permutes_def by metis}
695 {assume ns: "n \<in> S"
696 from H(3) ns have "p n < n \<or> p n = n" by auto
697 moreover{assume h: "p n < n"
698 from H h have "p (p n) = p n" by metis
699 with permutes_inj[OF H(2)] have "p n = n" unfolding inj_on_def by blast
700 with h have False by simp}
701 ultimately have "p n = n" by blast }
702 ultimately show "p n = n" by blast
704 thus ?thesis by (auto simp add: expand_fun_eq)
707 lemma permutes_natset_ge:
708 assumes p: "p permutes (S::'a::wellorder set)" and le: "\<forall>i \<in> S. p i \<ge> i" shows "p = id"
710 {fix i assume i: "i \<in> S"
711 from i permutes_in_image[OF permutes_inv[OF p]] have "inv p i \<in> S" by simp
712 with le have "p (inv p i) \<ge> inv p i" by blast
713 with permutes_inverses[OF p] have "i \<ge> inv p i" by simp}
714 then have th: "\<forall>i\<in>S. inv p i \<le> i" by blast
715 from permutes_natset_le[OF permutes_inv[OF p] th]
716 have "inv p = inv id" by simp
718 apply (subst permutes_inv_inv[OF p, symmetric])
719 apply (rule inv_unique_comp)
724 lemma image_inverse_permutations: "{inv p |p. p permutes S} = {p. p permutes S}"
727 using permutes_inv_inv permutes_inv apply auto
728 apply (rule_tac x="inv x" in exI)
732 lemma image_compose_permutations_left:
733 assumes q: "q permutes S" shows "{q o p | p. p permutes S} = {p . p permutes S}"
736 apply (rule permutes_compose)
738 apply (rule_tac x = "inv q o x" in exI)
739 by (simp add: o_assoc permutes_inv permutes_compose permutes_inv_o)
741 lemma image_compose_permutations_right:
742 assumes q: "q permutes S"
743 shows "{p o q | p. p permutes S} = {p . p permutes S}"
746 apply (rule permutes_compose)
748 apply (rule_tac x = "x o inv q" in exI)
749 by (simp add: o_assoc permutes_inv permutes_compose permutes_inv_o o_assoc[symmetric])
751 lemma permutes_in_seg: "p permutes {1 ..n} \<Longrightarrow> i \<in> {1..n} ==> 1 <= p i \<and> p i <= n"
753 apply (simp add: permutes_def)
758 lemma setsum_permutations_inverse: "setsum f {p. p permutes S} = setsum (\<lambda>p. f(inv p)) {p. p permutes S}" (is "?lhs = ?rhs")
760 let ?S = "{p . p permutes S}"
761 have th0: "inj_on inv ?S"
762 proof(auto simp add: inj_on_def)
764 assume q: "q permutes S" and r: "r permutes S" and qr: "inv q = inv r"
765 hence "inv (inv q) = inv (inv r)" by simp
766 with permutes_inv_inv[OF q] permutes_inv_inv[OF r]
767 show "q = r" by metis
769 have th1: "inv ` ?S = ?S" using image_inverse_permutations by blast
770 have th2: "?rhs = setsum (f o inv) ?S" by (simp add: o_def)
771 from setsum_reindex[OF th0, of f] show ?thesis unfolding th1 th2 .
774 lemma setum_permutations_compose_left:
775 assumes q: "q permutes S"
776 shows "setsum f {p. p permutes S} =
777 setsum (\<lambda>p. f(q o p)) {p. p permutes S}" (is "?lhs = ?rhs")
779 let ?S = "{p. p permutes S}"
780 have th0: "?rhs = setsum (f o (op o q)) ?S" by (simp add: o_def)
781 have th1: "inj_on (op o q) ?S"
782 apply (auto simp add: inj_on_def)
785 assume "p permutes S" and r:"r permutes S" and rp: "q \<circ> p = q \<circ> r"
786 hence "inv q o q o p = inv q o q o r" by (simp add: o_assoc[symmetric])
787 with permutes_inj[OF q, unfolded inj_iff]
791 have th3: "(op o q) ` ?S = ?S" using image_compose_permutations_left[OF q] by auto
792 from setsum_reindex[OF th1, of f]
793 show ?thesis unfolding th0 th1 th3 .
796 lemma sum_permutations_compose_right:
797 assumes q: "q permutes S"
798 shows "setsum f {p. p permutes S} =
799 setsum (\<lambda>p. f(p o q)) {p. p permutes S}" (is "?lhs = ?rhs")
801 let ?S = "{p. p permutes S}"
802 have th0: "?rhs = setsum (f o (\<lambda>p. p o q)) ?S" by (simp add: o_def)
803 have th1: "inj_on (\<lambda>p. p o q) ?S"
804 apply (auto simp add: inj_on_def)
807 assume "p permutes S" and r:"r permutes S" and rp: "p o q = r o q"
808 hence "p o (q o inv q) = r o (q o inv q)" by (simp add: o_assoc)
809 with permutes_surj[OF q, unfolded surj_iff]
813 have th3: "(\<lambda>p. p o q) ` ?S = ?S" using image_compose_permutations_right[OF q] by auto
814 from setsum_reindex[OF th1, of f]
815 show ?thesis unfolding th0 th1 th3 .
818 (* ------------------------------------------------------------------------- *)
819 (* Sum over a set of permutations (could generalize to iteration). *)
820 (* ------------------------------------------------------------------------- *)
822 lemma setsum_over_permutations_insert:
823 assumes fS: "finite S" and aS: "a \<notin> S"
824 shows "setsum f {p. p permutes (insert a S)} = setsum (\<lambda>b. setsum (\<lambda>q. f (Fun.swap a b id o q)) {p. p permutes S}) (insert a S)"
826 have th0: "\<And>f a b. (\<lambda>(b,p). f (Fun.swap a b id o p)) = f o (\<lambda>(b,p). Fun.swap a b id o p)"
827 by (simp add: expand_fun_eq)
828 have th1: "\<And>P Q. P \<times> Q = {(a,b). a \<in> P \<and> b \<in> Q}" by blast
829 have th2: "\<And>P Q. P \<Longrightarrow> (P \<Longrightarrow> Q) \<Longrightarrow> P \<and> Q" by blast
831 unfolding permutes_insert
832 unfolding setsum_cartesian_product
833 unfolding th1[symmetric]
835 proof(rule setsum_reindex)
836 let ?f = "(\<lambda>(b, y). Fun.swap a b id \<circ> y)"
837 let ?P = "{p. p permutes S}"
838 {fix b c p q assume b: "b \<in> insert a S" and c: "c \<in> insert a S"
839 and p: "p permutes S" and q: "q permutes S"
840 and eq: "Fun.swap a b id o p = Fun.swap a c id o q"
841 from p q aS have pa: "p a = a" and qa: "q a = a"
842 unfolding permutes_def by metis+
843 from eq have "(Fun.swap a b id o p) a = (Fun.swap a c id o q) a" by simp
845 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)
846 from eq[unfolded bc] have "(\<lambda>p. Fun.swap a c id o p) (Fun.swap a c id o p) = (\<lambda>p. Fun.swap a c id o p) (Fun.swap a c id o q)" by simp
847 hence "p = q" unfolding o_assoc swap_id_idempotent
849 with bc have "b = c \<and> p = q" by blast
852 then show "inj_on ?f (insert a S \<times> ?P)"
854 apply clarify by metis