|
1 (* Author: Paulo EmÃlio de Vilhena |
|
2 *) |
|
3 |
|
4 theory Cycles |
|
5 imports "HOL-Library.FuncSet" Permutations |
|
6 begin |
|
7 |
|
8 section \<open>Cycles\<close> |
|
9 |
|
10 subsection \<open>Definitions\<close> |
|
11 |
|
12 abbreviation cycle :: "'a list \<Rightarrow> bool" |
|
13 where "cycle cs \<equiv> distinct cs" |
|
14 |
|
15 fun cycle_of_list :: "'a list \<Rightarrow> 'a \<Rightarrow> 'a" |
|
16 where |
|
17 "cycle_of_list (i # j # cs) = (Fun.swap i j id) \<circ> (cycle_of_list (j # cs))" |
|
18 | "cycle_of_list cs = id" |
|
19 |
|
20 |
|
21 subsection \<open>Basic Properties\<close> |
|
22 |
|
23 text \<open>We start proving that the function derived from a cycle rotates its support list.\<close> |
|
24 |
|
25 lemma id_outside_supp: |
|
26 assumes "x \<notin> set cs" shows "(cycle_of_list cs) x = x" |
|
27 using assms by (induct cs rule: cycle_of_list.induct) (simp_all) |
|
28 |
|
29 lemma permutation_of_cycle: "permutation (cycle_of_list cs)" |
|
30 proof (induct cs rule: cycle_of_list.induct) |
|
31 case 1 thus ?case |
|
32 using permutation_compose[OF permutation_swap_id] unfolding comp_apply by simp |
|
33 qed simp_all |
|
34 |
|
35 lemma cycle_permutes: "(cycle_of_list cs) permutes (set cs)" |
|
36 using permutation_bijective[OF permutation_of_cycle] id_outside_supp[of _ cs] |
|
37 by (simp add: bij_iff permutes_def) |
|
38 |
|
39 theorem cyclic_rotation: |
|
40 assumes "cycle cs" shows "map ((cycle_of_list cs) ^^ n) cs = rotate n cs" |
|
41 proof - |
|
42 { have "map (cycle_of_list cs) cs = rotate1 cs" using assms(1) |
|
43 proof (induction cs rule: cycle_of_list.induct) |
|
44 case (1 i j cs) thus ?case |
|
45 proof (cases) |
|
46 assume "cs = Nil" thus ?thesis by simp |
|
47 next |
|
48 assume "cs \<noteq> Nil" hence ge_two: "length (j # cs) \<ge> 2" |
|
49 using not_less by auto |
|
50 have "map (cycle_of_list (i # j # cs)) (i # j # cs) = |
|
51 map (Fun.swap i j id) (map (cycle_of_list (j # cs)) (i # j # cs))" by simp |
|
52 also have " ... = map (Fun.swap i j id) (i # (rotate1 (j # cs)))" |
|
53 by (metis "1.IH" "1.prems" distinct.simps(2) id_outside_supp list.simps(9)) |
|
54 also have " ... = map (Fun.swap i j id) (i # (cs @ [j]))" by simp |
|
55 also have " ... = j # (map (Fun.swap i j id) cs) @ [i]" by simp |
|
56 also have " ... = j # cs @ [i]" |
|
57 by (metis "1.prems" distinct.simps(2) list.set_intros(2) map_idI swap_id_eq) |
|
58 also have " ... = rotate1 (i # j # cs)" by simp |
|
59 finally show ?thesis . |
|
60 qed |
|
61 qed simp_all } |
|
62 note cyclic_rotation' = this |
|
63 |
|
64 show ?thesis |
|
65 using cyclic_rotation' by (induct n) (auto, metis map_map rotate1_rotate_swap rotate_map) |
|
66 qed |
|
67 |
|
68 corollary cycle_is_surj: |
|
69 assumes "cycle cs" shows "(cycle_of_list cs) ` (set cs) = (set cs)" |
|
70 using cyclic_rotation[OF assms, of "Suc 0"] by (simp add: image_set) |
|
71 |
|
72 corollary cycle_is_id_root: |
|
73 assumes "cycle cs" shows "(cycle_of_list cs) ^^ (length cs) = id" |
|
74 proof - |
|
75 have "map ((cycle_of_list cs) ^^ (length cs)) cs = cs" |
|
76 unfolding cyclic_rotation[OF assms] by simp |
|
77 hence "((cycle_of_list cs) ^^ (length cs)) i = i" if "i \<in> set cs" for i |
|
78 using that map_eq_conv by fastforce |
|
79 moreover have "((cycle_of_list cs) ^^ n) i = i" if "i \<notin> set cs" for i n |
|
80 using id_outside_supp[OF that] by (induct n) (simp_all) |
|
81 ultimately show ?thesis |
|
82 by fastforce |
|
83 qed |
|
84 |
|
85 corollary cycle_of_list_rotate_independent: |
|
86 assumes "cycle cs" shows "(cycle_of_list cs) = (cycle_of_list (rotate n cs))" |
|
87 proof - |
|
88 { fix cs :: "'a list" assume cs: "cycle cs" |
|
89 have "(cycle_of_list cs) = (cycle_of_list (rotate1 cs))" |
|
90 proof - |
|
91 from cs have rotate1_cs: "cycle (rotate1 cs)" by simp |
|
92 hence "map (cycle_of_list (rotate1 cs)) (rotate1 cs) = (rotate 2 cs)" |
|
93 using cyclic_rotation[OF rotate1_cs, of 1] by (simp add: numeral_2_eq_2) |
|
94 moreover have "map (cycle_of_list cs) (rotate1 cs) = (rotate 2 cs)" |
|
95 using cyclic_rotation[OF cs] |
|
96 by (metis One_nat_def Suc_1 funpow.simps(2) id_apply map_map rotate0 rotate_Suc) |
|
97 ultimately have "(cycle_of_list cs) i = (cycle_of_list (rotate1 cs)) i" if "i \<in> set cs" for i |
|
98 using that map_eq_conv unfolding sym[OF set_rotate1[of cs]] by fastforce |
|
99 moreover have "(cycle_of_list cs) i = (cycle_of_list (rotate1 cs)) i" if "i \<notin> set cs" for i |
|
100 using that by (simp add: id_outside_supp) |
|
101 ultimately show "(cycle_of_list cs) = (cycle_of_list (rotate1 cs))" |
|
102 by blast |
|
103 qed } note rotate1_lemma = this |
|
104 |
|
105 show ?thesis |
|
106 using rotate1_lemma[of "rotate n cs"] by (induct n) (auto, metis assms distinct_rotate rotate1_lemma) |
|
107 qed |
|
108 |
|
109 |
|
110 subsection\<open>Conjugation of cycles\<close> |
|
111 |
|
112 lemma conjugation_of_cycle: |
|
113 assumes "cycle cs" and "bij p" |
|
114 shows "p \<circ> (cycle_of_list cs) \<circ> (inv p) = cycle_of_list (map p cs)" |
|
115 using assms |
|
116 proof (induction cs rule: cycle_of_list.induct) |
|
117 case (1 i j cs) |
|
118 have "p \<circ> cycle_of_list (i # j # cs) \<circ> inv p = |
|
119 (p \<circ> (Fun.swap i j id) \<circ> inv p) \<circ> (p \<circ> cycle_of_list (j # cs) \<circ> inv p)" |
|
120 by (simp add: assms(2) bij_is_inj fun.map_comp) |
|
121 also have " ... = (Fun.swap (p i) (p j) id) \<circ> (p \<circ> cycle_of_list (j # cs) \<circ> inv p)" |
|
122 by (simp add: "1.prems"(2) bij_is_inj bij_swap_comp comp_swap o_assoc) |
|
123 finally have "p \<circ> cycle_of_list (i # j # cs) \<circ> inv p = |
|
124 (Fun.swap (p i) (p j) id) \<circ> (cycle_of_list (map p (j # cs)))" |
|
125 using "1.IH" "1.prems"(1) assms(2) by fastforce |
|
126 thus ?case by (metis cycle_of_list.simps(1) list.simps(9)) |
|
127 next |
|
128 case "2_1" thus ?case |
|
129 by (metis bij_is_surj comp_id cycle_of_list.simps(2) list.simps(8) surj_iff) |
|
130 next |
|
131 case "2_2" thus ?case |
|
132 by (metis bij_is_surj comp_id cycle_of_list.simps(3) list.simps(8) list.simps(9) surj_iff) |
|
133 qed |
|
134 |
|
135 |
|
136 subsection\<open>When Cycles Commute\<close> |
|
137 |
|
138 lemma cycles_commute: |
|
139 assumes "cycle p" "cycle q" and "set p \<inter> set q = {}" |
|
140 shows "(cycle_of_list p) \<circ> (cycle_of_list q) = (cycle_of_list q) \<circ> (cycle_of_list p)" |
|
141 proof |
|
142 { fix p :: "'a list" and q :: "'a list" and i :: "'a" |
|
143 assume A: "cycle p" "cycle q" "set p \<inter> set q = {}" "i \<in> set p" "i \<notin> set q" |
|
144 have "((cycle_of_list p) \<circ> (cycle_of_list q)) i = |
|
145 ((cycle_of_list q) \<circ> (cycle_of_list p)) i" |
|
146 proof - |
|
147 have "((cycle_of_list p) \<circ> (cycle_of_list q)) i = (cycle_of_list p) i" |
|
148 using id_outside_supp[OF A(5)] by simp |
|
149 also have " ... = ((cycle_of_list q) \<circ> (cycle_of_list p)) i" |
|
150 using id_outside_supp[of "(cycle_of_list p) i"] cycle_is_surj[OF A(1)] A(3,4) by fastforce |
|
151 finally show ?thesis . |
|
152 qed } note aui_lemma = this |
|
153 |
|
154 fix i consider "i \<in> set p" "i \<notin> set q" | "i \<notin> set p" "i \<in> set q" | "i \<notin> set p" "i \<notin> set q" |
|
155 using \<open>set p \<inter> set q = {}\<close> by blast |
|
156 thus "((cycle_of_list p) \<circ> (cycle_of_list q)) i = ((cycle_of_list q) \<circ> (cycle_of_list p)) i" |
|
157 proof cases |
|
158 case 1 thus ?thesis |
|
159 using aui_lemma[OF assms] by simp |
|
160 next |
|
161 case 2 thus ?thesis |
|
162 using aui_lemma[OF assms(2,1)] assms(3) by (simp add: ac_simps) |
|
163 next |
|
164 case 3 thus ?thesis |
|
165 by (simp add: id_outside_supp) |
|
166 qed |
|
167 qed |
|
168 |
|
169 |
|
170 subsection \<open>Cycles from Permutations\<close> |
|
171 |
|
172 subsubsection \<open>Exponentiation of permutations\<close> |
|
173 |
|
174 text \<open>Some important properties of permutations before defining how to extract its cycles.\<close> |
|
175 |
|
176 lemma permutation_funpow: |
|
177 assumes "permutation p" shows "permutation (p ^^ n)" |
|
178 using assms by (induct n) (simp_all add: permutation_compose) |
|
179 |
|
180 lemma permutes_funpow: |
|
181 assumes "p permutes S" shows "(p ^^ n) permutes S" |
|
182 using assms by (induct n) (simp add: permutes_def, metis funpow_Suc_right permutes_compose) |
|
183 |
|
184 lemma funpow_diff: |
|
185 assumes "inj p" and "i \<le> j" "(p ^^ i) a = (p ^^ j) a" shows "(p ^^ (j - i)) a = a" |
|
186 proof - |
|
187 have "(p ^^ i) ((p ^^ (j - i)) a) = (p ^^ i) a" |
|
188 using assms(2-3) by (metis (no_types) add_diff_inverse_nat funpow_add not_le o_def) |
|
189 thus ?thesis |
|
190 unfolding inj_eq[OF inj_fn[OF assms(1)], of i] . |
|
191 qed |
|
192 |
|
193 lemma permutation_is_nilpotent: |
|
194 assumes "permutation p" obtains n where "(p ^^ n) = id" and "n > 0" |
|
195 proof - |
|
196 obtain S where "finite S" and "p permutes S" |
|
197 using assms unfolding permutation_permutes by blast |
|
198 hence "\<exists>n. (p ^^ n) = id \<and> n > 0" |
|
199 proof (induct S arbitrary: p) |
|
200 case empty thus ?case |
|
201 using id_funpow[of 1] unfolding permutes_empty by blast |
|
202 next |
|
203 case (insert s S) |
|
204 have "(\<lambda>n. (p ^^ n) s) ` UNIV \<subseteq> (insert s S)" |
|
205 using permutes_in_image[OF permutes_funpow[OF insert(4)], of _ s] by auto |
|
206 hence "\<not> inj_on (\<lambda>n. (p ^^ n) s) UNIV" |
|
207 using insert(1) infinite_iff_countable_subset unfolding sym[OF finite_insert, of S s] by metis |
|
208 then obtain i j where ij: "i < j" "(p ^^ i) s = (p ^^ j) s" |
|
209 unfolding inj_on_def by (metis nat_neq_iff) |
|
210 hence "(p ^^ (j - i)) s = s" |
|
211 using funpow_diff[OF permutes_inj[OF insert(4)]] le_eq_less_or_eq by blast |
|
212 hence "p ^^ (j - i) permutes S" |
|
213 using permutes_superset[OF permutes_funpow[OF insert(4), of "j - i"], of S] by auto |
|
214 then obtain n where n: "((p ^^ (j - i)) ^^ n) = id" "n > 0" |
|
215 using insert(3) by blast |
|
216 thus ?case |
|
217 using ij(1) nat_0_less_mult_iff zero_less_diff unfolding funpow_mult by metis |
|
218 qed |
|
219 thus thesis |
|
220 using that by blast |
|
221 qed |
|
222 |
|
223 lemma permutation_is_nilpotent': |
|
224 assumes "permutation p" obtains n where "(p ^^ n) = id" and "n > m" |
|
225 proof - |
|
226 obtain n where "(p ^^ n) = id" and "n > 0" |
|
227 using permutation_is_nilpotent[OF assms] by blast |
|
228 then obtain k where "n * k > m" |
|
229 by (metis dividend_less_times_div mult_Suc_right) |
|
230 from \<open>(p ^^ n) = id\<close> have "p ^^ (n * k) = id" |
|
231 by (induct k) (simp, metis funpow_mult id_funpow) |
|
232 with \<open>n * k > m\<close> show thesis |
|
233 using that by blast |
|
234 qed |
|
235 |
|
236 |
|
237 subsubsection \<open>Extraction of cycles from permutations\<close> |
|
238 |
|
239 definition least_power :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> nat" |
|
240 where "least_power f x = (LEAST n. (f ^^ n) x = x \<and> n > 0)" |
|
241 |
|
242 abbreviation support :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a list" |
|
243 where "support p x \<equiv> map (\<lambda>i. (p ^^ i) x) [0..< (least_power p x)]" |
|
244 |
|
245 |
|
246 lemma least_powerI: |
|
247 assumes "(f ^^ n) x = x" and "n > 0" |
|
248 shows "(f ^^ (least_power f x)) x = x" and "least_power f x > 0" |
|
249 using assms unfolding least_power_def by (metis (mono_tags, lifting) LeastI)+ |
|
250 |
|
251 lemma least_power_le: |
|
252 assumes "(f ^^ n) x = x" and "n > 0" shows "least_power f x \<le> n" |
|
253 using assms unfolding least_power_def by (simp add: Least_le) |
|
254 |
|
255 lemma least_power_of_permutation: |
|
256 assumes "permutation p" shows "(p ^^ (least_power p a)) a = a" and "least_power p a > 0" |
|
257 using permutation_is_nilpotent[OF assms] least_powerI by (metis id_apply)+ |
|
258 |
|
259 lemma least_power_gt_one: |
|
260 assumes "permutation p" and "p a \<noteq> a" shows "least_power p a > Suc 0" |
|
261 using least_power_of_permutation[OF assms(1)] assms(2) |
|
262 by (metis Suc_lessI funpow.simps(2) funpow_simps_right(1) o_id) |
|
263 |
|
264 lemma least_power_minimal: |
|
265 assumes "(p ^^ n) a = a" shows "(least_power p a) dvd n" |
|
266 proof (cases "n = 0", simp) |
|
267 let ?lpow = "least_power p" |
|
268 |
|
269 assume "n \<noteq> 0" then have "n > 0" by simp |
|
270 hence "(p ^^ (?lpow a)) a = a" and "least_power p a > 0" |
|
271 using assms unfolding least_power_def by (metis (mono_tags, lifting) LeastI)+ |
|
272 hence aux_lemma: "(p ^^ ((?lpow a) * k)) a = a" for k :: nat |
|
273 by (induct k) (simp_all add: funpow_add) |
|
274 |
|
275 have "(p ^^ (n mod ?lpow a)) ((p ^^ (n - (n mod ?lpow a))) a) = (p ^^ n) a" |
|
276 by (metis add_diff_inverse_nat funpow_add mod_less_eq_dividend not_less o_apply) |
|
277 with \<open>(p ^^ n) a = a\<close> have "(p ^^ (n mod ?lpow a)) a = a" |
|
278 using aux_lemma by (simp add: minus_mod_eq_mult_div) |
|
279 hence "?lpow a \<le> n mod ?lpow a" if "n mod ?lpow a > 0" |
|
280 using least_power_le[OF _ that, of p a] by simp |
|
281 with \<open>least_power p a > 0\<close> show "(least_power p a) dvd n" |
|
282 using mod_less_divisor not_le by blast |
|
283 qed |
|
284 |
|
285 lemma least_power_dvd: |
|
286 assumes "permutation p" shows "(least_power p a) dvd n \<longleftrightarrow> (p ^^ n) a = a" |
|
287 proof |
|
288 show "(p ^^ n) a = a \<Longrightarrow> (least_power p a) dvd n" |
|
289 using least_power_minimal[of _ p] by simp |
|
290 next |
|
291 have "(p ^^ ((least_power p a) * k)) a = a" for k :: nat |
|
292 using least_power_of_permutation(1)[OF assms(1)] by (induct k) (simp_all add: funpow_add) |
|
293 thus "(least_power p a) dvd n \<Longrightarrow> (p ^^ n) a = a" by blast |
|
294 qed |
|
295 |
|
296 theorem cycle_of_permutation: |
|
297 assumes "permutation p" shows "cycle (support p a)" |
|
298 proof - |
|
299 have "(least_power p a) dvd (j - i)" if "i \<le> j" "j < least_power p a" and "(p ^^ i) a = (p ^^ j) a" for i j |
|
300 using funpow_diff[OF bij_is_inj that(1,3)] assms by (simp add: permutation least_power_dvd) |
|
301 moreover have "i = j" if "i \<le> j" "j < least_power p a" and "(least_power p a) dvd (j - i)" for i j |
|
302 using that le_eq_less_or_eq nat_dvd_not_less by auto |
|
303 ultimately have "inj_on (\<lambda>i. (p ^^ i) a) {..< (least_power p a)}" |
|
304 unfolding inj_on_def by (metis le_cases lessThan_iff) |
|
305 thus ?thesis |
|
306 by (simp add: atLeast_upt distinct_map) |
|
307 qed |
|
308 |
|
309 |
|
310 subsection \<open>Decomposition on Cycles\<close> |
|
311 |
|
312 text \<open>We show that a permutation can be decomposed on cycles\<close> |
|
313 |
|
314 subsubsection \<open>Preliminaries\<close> |
|
315 |
|
316 lemma support_set: |
|
317 assumes "permutation p" shows "set (support p a) = range (\<lambda>i. (p ^^ i) a)" |
|
318 proof |
|
319 show "set (support p a) \<subseteq> range (\<lambda>i. (p ^^ i) a)" |
|
320 by auto |
|
321 next |
|
322 show "range (\<lambda>i. (p ^^ i) a) \<subseteq> set (support p a)" |
|
323 proof (auto) |
|
324 fix i |
|
325 have "(p ^^ i) a = (p ^^ (i mod (least_power p a))) ((p ^^ (i - (i mod (least_power p a)))) a)" |
|
326 by (metis add_diff_inverse_nat funpow_add mod_less_eq_dividend not_le o_apply) |
|
327 also have " ... = (p ^^ (i mod (least_power p a))) a" |
|
328 using least_power_dvd[OF assms] by (metis dvd_minus_mod) |
|
329 also have " ... \<in> (\<lambda>i. (p ^^ i) a) ` {0..< (least_power p a)}" |
|
330 using least_power_of_permutation(2)[OF assms] by fastforce |
|
331 finally show "(p ^^ i) a \<in> (\<lambda>i. (p ^^ i) a) ` {0..< (least_power p a)}" . |
|
332 qed |
|
333 qed |
|
334 |
|
335 lemma disjoint_support: |
|
336 assumes "permutation p" shows "disjoint (range (\<lambda>a. set (support p a)))" (is "disjoint ?A") |
|
337 proof (rule disjointI) |
|
338 { fix i j a b |
|
339 assume "set (support p a) \<inter> set (support p b) \<noteq> {}" have "set (support p a) \<subseteq> set (support p b)" |
|
340 unfolding support_set[OF assms] |
|
341 proof (auto) |
|
342 from \<open>set (support p a) \<inter> set (support p b) \<noteq> {}\<close> |
|
343 obtain i j where ij: "(p ^^ i) a = (p ^^ j) b" |
|
344 by auto |
|
345 |
|
346 fix k |
|
347 have "(p ^^ k) a = (p ^^ (k + (least_power p a) * l)) a" for l |
|
348 using least_power_dvd[OF assms] by (induct l) (simp, metis dvd_triv_left funpow_add o_def) |
|
349 then obtain m where "m \<ge> i" and "(p ^^ m) a = (p ^^ k) a" |
|
350 using least_power_of_permutation(2)[OF assms] |
|
351 by (metis dividend_less_times_div le_eq_less_or_eq mult_Suc_right trans_less_add2) |
|
352 hence "(p ^^ m) a = (p ^^ (m - i)) ((p ^^ i) a)" |
|
353 by (metis Nat.le_imp_diff_is_add funpow_add o_apply) |
|
354 with \<open>(p ^^ m) a = (p ^^ k) a\<close> have "(p ^^ k) a = (p ^^ ((m - i) + j)) b" |
|
355 unfolding ij by (simp add: funpow_add) |
|
356 thus "(p ^^ k) a \<in> range (\<lambda>i. (p ^^ i) b)" |
|
357 by blast |
|
358 qed } note aux_lemma = this |
|
359 |
|
360 fix supp_a supp_b |
|
361 assume "supp_a \<in> ?A" and "supp_b \<in> ?A" |
|
362 then obtain a b where a: "supp_a = set (support p a)" and b: "supp_b = set (support p b)" |
|
363 by auto |
|
364 assume "supp_a \<noteq> supp_b" thus "supp_a \<inter> supp_b = {}" |
|
365 using aux_lemma unfolding a b by blast |
|
366 qed |
|
367 |
|
368 lemma disjoint_support': |
|
369 assumes "permutation p" |
|
370 shows "set (support p a) \<inter> set (support p b) = {} \<longleftrightarrow> a \<notin> set (support p b)" |
|
371 proof - |
|
372 have "a \<in> set (support p a)" |
|
373 using least_power_of_permutation(2)[OF assms] by force |
|
374 show ?thesis |
|
375 proof |
|
376 assume "set (support p a) \<inter> set (support p b) = {}" |
|
377 with \<open>a \<in> set (support p a)\<close> show "a \<notin> set (support p b)" |
|
378 by blast |
|
379 next |
|
380 assume "a \<notin> set (support p b)" show "set (support p a) \<inter> set (support p b) = {}" |
|
381 proof (rule ccontr) |
|
382 assume "set (support p a) \<inter> set (support p b) \<noteq> {}" |
|
383 hence "set (support p a) = set (support p b)" |
|
384 using disjoint_support[OF assms] by (meson UNIV_I disjoint_def image_iff) |
|
385 with \<open>a \<in> set (support p a)\<close> and \<open>a \<notin> set (support p b)\<close> show False |
|
386 by simp |
|
387 qed |
|
388 qed |
|
389 qed |
|
390 |
|
391 lemma support_coverture: |
|
392 assumes "permutation p" shows "\<Union> { set (support p a) | a. p a \<noteq> a } = { a. p a \<noteq> a }" |
|
393 proof |
|
394 show "{ a. p a \<noteq> a } \<subseteq> \<Union> { set (support p a) | a. p a \<noteq> a }" |
|
395 proof |
|
396 fix a assume "a \<in> { a. p a \<noteq> a }" |
|
397 have "a \<in> set (support p a)" |
|
398 using least_power_of_permutation(2)[OF assms, of a] by force |
|
399 with \<open>a \<in> { a. p a \<noteq> a }\<close> show "a \<in> \<Union> { set (support p a) | a. p a \<noteq> a }" |
|
400 by blast |
|
401 qed |
|
402 next |
|
403 show "\<Union> { set (support p a) | a. p a \<noteq> a } \<subseteq> { a. p a \<noteq> a }" |
|
404 proof |
|
405 fix b assume "b \<in> \<Union> { set (support p a) | a. p a \<noteq> a }" |
|
406 then obtain a i where "p a \<noteq> a" and "(p ^^ i) a = b" |
|
407 by auto |
|
408 have "p a = a" if "(p ^^ i) a = (p ^^ Suc i) a" |
|
409 using funpow_diff[OF bij_is_inj _ that] assms unfolding permutation by simp |
|
410 with \<open>p a \<noteq> a\<close> and \<open>(p ^^ i) a = b\<close> show "b \<in> { a. p a \<noteq> a }" |
|
411 by auto |
|
412 qed |
|
413 qed |
|
414 |
|
415 theorem cycle_restrict: |
|
416 assumes "permutation p" and "b \<in> set (support p a)" shows "p b = (cycle_of_list (support p a)) b" |
|
417 proof - |
|
418 note least_power_props [simp] = least_power_of_permutation[OF assms(1)] |
|
419 |
|
420 have "map (cycle_of_list (support p a)) (support p a) = rotate1 (support p a)" |
|
421 using cyclic_rotation[OF cycle_of_permutation[OF assms(1)], of 1 a] by simp |
|
422 hence "map (cycle_of_list (support p a)) (support p a) = tl (support p a) @ [ a ]" |
|
423 by (simp add: hd_map rotate1_hd_tl) |
|
424 also have " ... = map p (support p a)" |
|
425 proof (rule nth_equalityI, auto) |
|
426 fix i assume "i < least_power p a" show "(tl (support p a) @ [a]) ! i = p ((p ^^ i) a)" |
|
427 proof (cases) |
|
428 assume i: "i = least_power p a - 1" |
|
429 hence "(tl (support p a) @ [ a ]) ! i = a" |
|
430 by (metis (no_types, lifting) diff_zero length_map length_tl length_upt nth_append_length) |
|
431 also have " ... = p ((p ^^ i) a)" |
|
432 by (metis (mono_tags, hide_lams) least_power_props i Suc_diff_1 funpow_simps_right(2) funpow_swap1 o_apply) |
|
433 finally show ?thesis . |
|
434 next |
|
435 assume "i \<noteq> least_power p a - 1" |
|
436 with \<open>i < least_power p a\<close> have "i < least_power p a - 1" |
|
437 by simp |
|
438 hence "(tl (support p a) @ [ a ]) ! i = (p ^^ (Suc i)) a" |
|
439 by (metis One_nat_def Suc_eq_plus1 add.commute length_map length_upt map_tl nth_append nth_map_upt tl_upt) |
|
440 thus ?thesis |
|
441 by simp |
|
442 qed |
|
443 qed |
|
444 finally have "map (cycle_of_list (support p a)) (support p a) = map p (support p a)" . |
|
445 thus ?thesis |
|
446 using assms(2) by auto |
|
447 qed |
|
448 |
|
449 |
|
450 subsubsection\<open>Decomposition\<close> |
|
451 |
|
452 inductive cycle_decomp :: "'a set \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> bool" |
|
453 where |
|
454 empty: "cycle_decomp {} id" |
|
455 | comp: "\<lbrakk> cycle_decomp I p; cycle cs; set cs \<inter> I = {} \<rbrakk> \<Longrightarrow> |
|
456 cycle_decomp (set cs \<union> I) ((cycle_of_list cs) \<circ> p)" |
|
457 |
|
458 |
|
459 lemma semidecomposition: |
|
460 assumes "p permutes S" and "finite S" |
|
461 shows "(\<lambda>y. if y \<in> (S - set (support p a)) then p y else y) permutes (S - set (support p a))" |
|
462 proof (rule bij_imp_permutes) |
|
463 show "(if b \<in> (S - set (support p a)) then p b else b) = b" if "b \<notin> S - set (support p a)" for b |
|
464 using that by auto |
|
465 next |
|
466 have is_permutation: "permutation p" |
|
467 using assms unfolding permutation_permutes by blast |
|
468 |
|
469 let ?q = "\<lambda>y. if y \<in> (S - set (support p a)) then p y else y" |
|
470 show "bij_betw ?q (S - set (support p a)) (S - set (support p a))" |
|
471 proof (rule bij_betw_imageI) |
|
472 show "inj_on ?q (S - set (support p a))" |
|
473 using permutes_inj[OF assms(1)] unfolding inj_on_def by auto |
|
474 next |
|
475 have aux_lemma: "set (support p s) \<subseteq> (S - set (support p a))" if "s \<in> S - set (support p a)" for s |
|
476 proof - |
|
477 have "(p ^^ i) s \<in> S" for i |
|
478 using that unfolding permutes_in_image[OF permutes_funpow[OF assms(1)]] by simp |
|
479 thus ?thesis |
|
480 using that disjoint_support'[OF is_permutation, of s a] by auto |
|
481 qed |
|
482 have "(p ^^ 1) s \<in> set (support p s)" for s |
|
483 unfolding support_set[OF is_permutation] by blast |
|
484 hence "p s \<in> set (support p s)" for s |
|
485 by simp |
|
486 hence "p ` (S - set (support p a)) \<subseteq> S - set (support p a)" |
|
487 using aux_lemma by blast |
|
488 moreover have "(p ^^ ((least_power p s) - 1)) s \<in> set (support p s)" for s |
|
489 unfolding support_set[OF is_permutation] by blast |
|
490 hence "\<exists>s' \<in> set (support p s). p s' = s" for s |
|
491 using least_power_of_permutation[OF is_permutation] by (metis Suc_diff_1 funpow.simps(2) o_apply) |
|
492 hence "S - set (support p a) \<subseteq> p ` (S - set (support p a))" |
|
493 using aux_lemma |
|
494 by (clarsimp simp add: image_iff) (metis image_subset_iff) |
|
495 ultimately show "?q ` (S - set (support p a)) = (S - set (support p a))" |
|
496 by auto |
|
497 qed |
|
498 qed |
|
499 |
|
500 theorem cycle_decomposition: |
|
501 assumes "p permutes S" and "finite S" shows "cycle_decomp S p" |
|
502 using assms |
|
503 proof(induct "card S" arbitrary: S p rule: less_induct) |
|
504 case less show ?case |
|
505 proof (cases) |
|
506 assume "S = {}" thus ?thesis |
|
507 using empty less(2) by auto |
|
508 next |
|
509 have is_permutation: "permutation p" |
|
510 using less(2-3) unfolding permutation_permutes by blast |
|
511 |
|
512 assume "S \<noteq> {}" then obtain s where "s \<in> S" |
|
513 by blast |
|
514 define q where "q = (\<lambda>y. if y \<in> (S - set (support p s)) then p y else y)" |
|
515 have "(cycle_of_list (support p s) \<circ> q) = p" |
|
516 proof |
|
517 fix a |
|
518 consider "a \<in> S - set (support p s)" | "a \<in> set (support p s)" | "a \<notin> S" "a \<notin> set (support p s)" |
|
519 by blast |
|
520 thus "((cycle_of_list (support p s) \<circ> q)) a = p a" |
|
521 proof cases |
|
522 case 1 |
|
523 have "(p ^^ 1) a \<in> set (support p a)" |
|
524 unfolding support_set[OF is_permutation] by blast |
|
525 with \<open>a \<in> S - set (support p s)\<close> have "p a \<notin> set (support p s)" |
|
526 using disjoint_support'[OF is_permutation, of a s] by auto |
|
527 with \<open>a \<in> S - set (support p s)\<close> show ?thesis |
|
528 using id_outside_supp[of _ "support p s"] unfolding q_def by simp |
|
529 next |
|
530 case 2 thus ?thesis |
|
531 using cycle_restrict[OF is_permutation] unfolding q_def by simp |
|
532 next |
|
533 case 3 thus ?thesis |
|
534 using id_outside_supp[OF 3(2)] less(2) permutes_not_in unfolding q_def by fastforce |
|
535 qed |
|
536 qed |
|
537 |
|
538 moreover from \<open>s \<in> S\<close> have "(p ^^ i) s \<in> S" for i |
|
539 unfolding permutes_in_image[OF permutes_funpow[OF less(2)]] . |
|
540 hence "set (support p s) \<union> (S - set (support p s)) = S" |
|
541 by auto |
|
542 |
|
543 moreover have "s \<in> set (support p s)" |
|
544 using least_power_of_permutation[OF is_permutation] by force |
|
545 with \<open>s \<in> S\<close> have "card (S - set (support p s)) < card S" |
|
546 using less(3) by (metis DiffE card_seteq linorder_not_le subsetI) |
|
547 hence "cycle_decomp (S - set (support p s)) q" |
|
548 using less(1)[OF _ semidecomposition[OF less(2-3)], of s] less(3) unfolding q_def by blast |
|
549 |
|
550 moreover show ?thesis |
|
551 using comp[OF calculation(3) cycle_of_permutation[OF is_permutation], of s] |
|
552 unfolding calculation(1-2) by blast |
|
553 qed |
|
554 qed |
|
555 |
|
556 end |