|
1 (* ************************************************************************** *) |
|
2 (* Title: Cycles.thy *) |
|
3 (* Author: Paulo EmÃlio de Vilhena *) |
|
4 (* ************************************************************************** *) |
|
5 |
|
6 theory Cycles |
|
7 imports "HOL-Library.Permutations" "HOL-Library.FuncSet" |
|
8 |
|
9 begin |
|
10 |
|
11 section \<open>Cycles\<close> |
|
12 |
|
13 abbreviation cycle :: "'a list \<Rightarrow> bool" where |
|
14 "cycle cs \<equiv> distinct cs" |
|
15 |
|
16 fun cycle_of_list :: "'a list \<Rightarrow> 'a \<Rightarrow> 'a" |
|
17 where |
|
18 "cycle_of_list (i # j # cs) = (Fun.swap i j id) \<circ> (cycle_of_list (j # cs))" |
|
19 | "cycle_of_list cs = id" |
|
20 |
|
21 |
|
22 subsection\<open>Cycles as Rotations\<close> |
|
23 |
|
24 text\<open>We start proving that the function derived from a cycle rotates its support list.\<close> |
|
25 |
|
26 lemma id_outside_supp: |
|
27 assumes "cycle cs" and "x \<notin> set cs" |
|
28 shows "(cycle_of_list cs) x = x" using assms |
|
29 proof (induction cs rule: cycle_of_list.induct) |
|
30 case (1 i j cs) |
|
31 have "cycle_of_list (i # j # cs) x = (Fun.swap i j id) (cycle_of_list (j # cs) x)" by simp |
|
32 also have " ... = (Fun.swap i j id) x" |
|
33 using "1.IH" "1.prems"(1) "1.prems"(2) by auto |
|
34 also have " ... = x" using 1(3) by simp |
|
35 finally show ?case . |
|
36 next |
|
37 case "2_1" thus ?case by simp |
|
38 next |
|
39 case "2_2" thus ?case by simp |
|
40 qed |
|
41 |
|
42 lemma cycle_permutes: |
|
43 assumes "cycle cs" |
|
44 shows "permutation (cycle_of_list cs)" |
|
45 proof (induction rule: cycle_of_list.induct) |
|
46 case (1 i j cs) thus ?case |
|
47 by (metis cycle_of_list.simps(1) permutation_compose permutation_swap_id) |
|
48 next |
|
49 case "2_1" thus ?case by simp |
|
50 next |
|
51 case "2_2" thus ?case by simp |
|
52 qed |
|
53 |
|
54 theorem cyclic_rotation: |
|
55 assumes "cycle cs" |
|
56 shows "map ((cycle_of_list cs) ^^ n) cs = rotate n cs" |
|
57 proof - |
|
58 { have "map (cycle_of_list cs) cs = rotate1 cs" using assms(1) |
|
59 proof (induction cs rule: cycle_of_list.induct) |
|
60 case (1 i j cs) thus ?case |
|
61 proof (cases) |
|
62 assume "cs = Nil" thus ?thesis by simp |
|
63 next |
|
64 assume "cs \<noteq> Nil" hence ge_two: "length (j # cs) \<ge> 2" |
|
65 using not_less by auto |
|
66 have "map (cycle_of_list (i # j # cs)) (i # j # cs) = |
|
67 map (Fun.swap i j id) (map (cycle_of_list (j # cs)) (i # j # cs))" by simp |
|
68 also have " ... = map (Fun.swap i j id) (i # (rotate1 (j # cs)))" |
|
69 by (metis "1.IH" "1.prems" distinct.simps(2) id_outside_supp list.simps(9)) |
|
70 also have " ... = map (Fun.swap i j id) (i # (cs @ [j]))" by simp |
|
71 also have " ... = j # (map (Fun.swap i j id) cs) @ [i]" by simp |
|
72 also have " ... = j # cs @ [i]" |
|
73 by (metis "1.prems" distinct.simps(2) list.set_intros(2) map_idI swap_id_eq) |
|
74 also have " ... = rotate1 (i # j # cs)" by simp |
|
75 finally show ?thesis . |
|
76 qed |
|
77 next |
|
78 case "2_1" thus ?case by simp |
|
79 next |
|
80 case "2_2" thus ?case by simp |
|
81 qed } |
|
82 note cyclic_rotation' = this |
|
83 |
|
84 from assms show ?thesis |
|
85 proof (induction n) |
|
86 case 0 thus ?case by simp |
|
87 next |
|
88 case (Suc n) |
|
89 have "map ((cycle_of_list cs) ^^ (Suc n)) cs = |
|
90 map (cycle_of_list cs) (map ((cycle_of_list cs) ^^ n) cs)" by simp |
|
91 also have " ... = map (cycle_of_list cs) (rotate n cs)" |
|
92 by (simp add: Suc.IH assms) |
|
93 also have " ... = rotate (Suc n) cs" |
|
94 using cyclic_rotation' |
|
95 by (metis rotate1_rotate_swap rotate_Suc rotate_map) |
|
96 finally show ?case . |
|
97 qed |
|
98 qed |
|
99 |
|
100 corollary cycle_is_surj: |
|
101 assumes "cycle cs" |
|
102 shows "(cycle_of_list cs) ` (set cs) = (set cs)" |
|
103 using cyclic_rotation[OF assms, of 1] by (simp add: image_set) |
|
104 |
|
105 corollary cycle_is_id_root: |
|
106 assumes "cycle cs" |
|
107 shows "(cycle_of_list cs) ^^ (length cs) = id" |
|
108 proof - |
|
109 have "map ((cycle_of_list cs) ^^ (length cs)) cs = cs" |
|
110 by (simp add: assms cyclic_rotation) |
|
111 hence "\<And>x. x \<in> (set cs) \<Longrightarrow> ((cycle_of_list cs) ^^ (length cs)) x = x" |
|
112 using map_eq_conv by fastforce |
|
113 moreover have "\<And>n x. x \<notin> (set cs) \<Longrightarrow> ((cycle_of_list cs) ^^ n) x = x" |
|
114 proof - |
|
115 fix n show "\<And>x. x \<notin> (set cs) \<Longrightarrow> ((cycle_of_list cs) ^^ n) x = x" |
|
116 proof (induction n) |
|
117 case 0 thus ?case by simp |
|
118 next |
|
119 case (Suc n) thus ?case using id_outside_supp[OF assms] by simp |
|
120 qed |
|
121 qed |
|
122 hence "\<And>x. x \<notin> (set cs) \<Longrightarrow> ((cycle_of_list cs) ^^ (length cs)) x = x" by simp |
|
123 ultimately show ?thesis |
|
124 by (meson eq_id_iff) |
|
125 qed |
|
126 |
|
127 corollary |
|
128 assumes "cycle cs" |
|
129 shows "(cycle_of_list cs) = (cycle_of_list (rotate n cs))" |
|
130 proof - |
|
131 { fix cs :: "'a list" assume A: "cycle cs" |
|
132 have "(cycle_of_list cs) = (cycle_of_list (rotate1 cs))" |
|
133 proof |
|
134 have "\<And>x. x \<in> set cs \<Longrightarrow> (cycle_of_list cs) x = (cycle_of_list (rotate1 cs)) x" |
|
135 proof - |
|
136 have "cycle (rotate1 cs)" using A by simp |
|
137 hence "map (cycle_of_list (rotate1 cs)) (rotate1 cs) = (rotate 2 cs)" |
|
138 using cyclic_rotation by (metis Suc_eq_plus1 add.left_neutral |
|
139 funpow.simps(2) funpow_simps_right(1) o_id one_add_one rotate_Suc rotate_def) |
|
140 also have " ... = map (cycle_of_list cs) (rotate1 cs)" |
|
141 using cyclic_rotation[OF A] |
|
142 by (metis One_nat_def Suc_1 funpow.simps(2) id_apply map_map rotate0 rotate_Suc) |
|
143 finally have "map (cycle_of_list (rotate1 cs)) (rotate1 cs) = |
|
144 map (cycle_of_list cs) (rotate1 cs)" . |
|
145 moreover fix x assume "x \<in> set cs" |
|
146 ultimately show "(cycle_of_list cs) x = (cycle_of_list (rotate1 cs)) x" by auto |
|
147 qed |
|
148 moreover have "\<And>x. x \<notin> set cs \<Longrightarrow> (cycle_of_list cs) x = (cycle_of_list (rotate1 cs)) x" |
|
149 using A by (simp add: id_outside_supp) |
|
150 ultimately show "\<And>x. (cycle_of_list cs) x = (cycle_of_list (rotate1 cs)) x" by blast |
|
151 qed } |
|
152 note rotate1_lemma = this |
|
153 |
|
154 show "cycle_of_list cs = cycle_of_list (rotate n cs)" |
|
155 proof (induction n) |
|
156 case 0 thus ?case by simp |
|
157 next |
|
158 case (Suc n) |
|
159 have "cycle (rotate n cs)" by (simp add: assms) |
|
160 thus ?case using rotate1_lemma[of "rotate n cs"] |
|
161 by (simp add: Suc.IH) |
|
162 qed |
|
163 qed |
|
164 |
|
165 |
|
166 subsection\<open>Conjugation of cycles\<close> |
|
167 |
|
168 lemma conjugation_of_cycle: |
|
169 assumes "cycle cs" and "bij p" |
|
170 shows "p \<circ> (cycle_of_list cs) \<circ> (inv p) = cycle_of_list (map p cs)" |
|
171 using assms |
|
172 proof (induction cs rule: cycle_of_list.induct) |
|
173 case (1 i j cs) |
|
174 have "p \<circ> cycle_of_list (i # j # cs) \<circ> inv p = |
|
175 (p \<circ> (Fun.swap i j id) \<circ> inv p) \<circ> (p \<circ> cycle_of_list (j # cs) \<circ> inv p)" |
|
176 by (simp add: assms(2) bij_is_inj fun.map_comp) |
|
177 also have " ... = (Fun.swap (p i) (p j) id) \<circ> (p \<circ> cycle_of_list (j # cs) \<circ> inv p)" |
|
178 by (simp add: "1.prems"(2) bij_is_inj bij_swap_comp comp_swap o_assoc) |
|
179 finally have "p \<circ> cycle_of_list (i # j # cs) \<circ> inv p = |
|
180 (Fun.swap (p i) (p j) id) \<circ> (cycle_of_list (map p (j # cs)))" |
|
181 using "1.IH" "1.prems"(1) assms(2) by fastforce |
|
182 thus ?case by (metis cycle_of_list.simps(1) list.simps(9)) |
|
183 next |
|
184 case "2_1" thus ?case |
|
185 by (metis bij_is_surj comp_id cycle_of_list.simps(2) list.simps(8) surj_iff) |
|
186 next |
|
187 case "2_2" thus ?case |
|
188 by (metis bij_is_surj comp_id cycle_of_list.simps(3) list.simps(8) list.simps(9) surj_iff) |
|
189 qed |
|
190 |
|
191 |
|
192 subsection\<open>When Cycles Commute\<close> |
|
193 |
|
194 lemma cycles_commute: |
|
195 assumes "cycle \<sigma>1" "cycle \<sigma>2" and "set \<sigma>1 \<inter> set \<sigma>2 = {}" |
|
196 shows "(cycle_of_list \<sigma>1) \<circ> (cycle_of_list \<sigma>2) = (cycle_of_list \<sigma>2) \<circ> (cycle_of_list \<sigma>1)" |
|
197 proof - |
|
198 { fix \<pi>1 :: "'a list" and \<pi>2 :: "'a list" and x :: "'a" |
|
199 assume A: "cycle \<pi>1" "cycle \<pi>2" "set \<pi>1 \<inter> set \<pi>2 = {}" "x \<in> set \<pi>1" "x \<notin> set \<pi>2" |
|
200 have "((cycle_of_list \<pi>1) \<circ> (cycle_of_list \<pi>2)) x = |
|
201 ((cycle_of_list \<pi>2) \<circ> (cycle_of_list \<pi>1)) x" |
|
202 proof - |
|
203 have "((cycle_of_list \<pi>1) \<circ> (cycle_of_list \<pi>2)) x = (cycle_of_list \<pi>1) x" |
|
204 using id_outside_supp[OF A(2) A(5)] by simp |
|
205 also have " ... = ((cycle_of_list \<pi>2) \<circ> (cycle_of_list \<pi>1)) x" |
|
206 using id_outside_supp[OF A(2), of "(cycle_of_list \<pi>1) x"] |
|
207 cycle_is_surj[OF A(1)] A(3) A(4) by fastforce |
|
208 finally show ?thesis . |
|
209 qed } |
|
210 note aux_lemma = this |
|
211 |
|
212 let ?\<sigma>12 = "\<lambda>x. ((cycle_of_list \<sigma>1) \<circ> (cycle_of_list \<sigma>2)) x" |
|
213 let ?\<sigma>21 = "\<lambda>x. ((cycle_of_list \<sigma>2) \<circ> (cycle_of_list \<sigma>1)) x" |
|
214 |
|
215 show ?thesis |
|
216 proof |
|
217 fix x have "x \<in> set \<sigma>1 \<union> set \<sigma>2 \<or> x \<notin> set \<sigma>1 \<union> set \<sigma>2" by blast |
|
218 from this show "?\<sigma>12 x = ?\<sigma>21 x" |
|
219 proof |
|
220 assume "x \<in> set \<sigma>1 \<union> set \<sigma>2" |
|
221 hence "(x \<in> set \<sigma>1 \<and> x \<notin> set \<sigma>2) \<or> (x \<notin> set \<sigma>1 \<and> x \<in> set \<sigma>2)" using assms(3) by blast |
|
222 from this show "?\<sigma>12 x = ?\<sigma>21 x" |
|
223 proof |
|
224 assume "x \<in> set \<sigma>1 \<and> x \<notin> set \<sigma>2" thus ?thesis |
|
225 using aux_lemma[OF assms(1-3)] by simp |
|
226 next |
|
227 assume "x \<notin> set \<sigma>1 \<and> x \<in> set \<sigma>2" thus ?thesis |
|
228 using assms aux_lemma inf_commute by metis |
|
229 qed |
|
230 next |
|
231 assume "x \<notin> set \<sigma>1 \<union> set \<sigma>2" thus ?thesis using id_outside_supp assms(1-2) |
|
232 by (metis UnCI comp_apply) |
|
233 qed |
|
234 qed |
|
235 qed |
|
236 |
|
237 |
|
238 subsection\<open>Cycles from Permutations\<close> |
|
239 |
|
240 subsubsection\<open>Exponentiation of permutations\<close> |
|
241 |
|
242 text\<open>Some important properties of permutations before defining how to extract its cycles\<close> |
|
243 |
|
244 lemma exp_of_permutation1: |
|
245 assumes "p permutes S" |
|
246 shows "(p ^^ n) permutes S" using assms |
|
247 proof (induction n) |
|
248 case 0 thus ?case by (simp add: permutes_def) |
|
249 next |
|
250 case (Suc n) thus ?case by (metis funpow_Suc_right permutes_compose) |
|
251 qed |
|
252 |
|
253 lemma exp_of_permutation2: |
|
254 assumes "p permutes S" |
|
255 and "i < j" "(p ^^ j) = (p ^^ i)" |
|
256 shows "(p ^^ (j - i)) = id" using assms |
|
257 proof - |
|
258 have "(p ^^ i) \<circ> (p ^^ (j - i)) = (p ^^ j)" |
|
259 by (metis add_diff_inverse_nat assms(2) funpow_add le_eq_less_or_eq not_le) |
|
260 also have " ... = (p ^^ i)" using assms(3) by simp |
|
261 finally have "(p ^^ i) \<circ> (p ^^ (j - i)) = (p ^^ i)" . |
|
262 moreover have "bij (p ^^ i)" using exp_of_permutation1[OF assms(1)] |
|
263 using permutes_bij by auto |
|
264 ultimately show ?thesis |
|
265 by (metis (no_types, lifting) bij_is_inj comp_assoc fun.map_id inv_o_cancel) |
|
266 qed |
|
267 |
|
268 lemma exp_of_permutation3: |
|
269 assumes "p permutes S" "finite S" |
|
270 shows "\<exists>n. (p ^^ n) = id \<and> n > 0" |
|
271 proof (rule ccontr) |
|
272 assume "\<nexists>n. (p ^^ n) = id \<and> 0 < n" |
|
273 hence S: "\<And>n. n > 0 \<Longrightarrow> (p ^^ n) \<noteq> id" by auto |
|
274 hence "\<And>i j. \<lbrakk> i \<ge> 0; j \<ge> 0 \<rbrakk> \<Longrightarrow> i \<noteq> j \<Longrightarrow> (p ^^ i) \<noteq> (p ^^ j)" |
|
275 proof - |
|
276 fix i :: "nat" and j :: "nat" assume "i \<ge> 0" "j \<ge> 0" and Ineq: "i \<noteq> j" |
|
277 show "(p ^^ i) \<noteq> (p ^^ j)" |
|
278 proof (rule ccontr) |
|
279 assume "\<not> (p ^^ i) \<noteq> (p ^^ j)" hence Eq: "(p ^^ i) = (p ^^ j)" by simp |
|
280 have "(p ^^ (j - i)) = id" if "j > i" |
|
281 using Eq exp_of_permutation2[OF assms(1) that] by simp |
|
282 moreover have "(p ^^ (i - j)) = id" if "i > j" |
|
283 using Eq exp_of_permutation2[OF assms(1) that] by simp |
|
284 ultimately show False using Ineq S |
|
285 by (meson le_eq_less_or_eq not_le zero_less_diff) |
|
286 qed |
|
287 qed |
|
288 hence "bij_betw (\<lambda>i. (p ^^ i)) {i :: nat . i \<ge> 0} {(p ^^ i) | i :: nat . i \<ge> 0}" |
|
289 unfolding bij_betw_def inj_on_def by blast |
|
290 hence "infinite {(p ^^ i) | i :: nat . i \<ge> 0}" |
|
291 using bij_betw_finite by auto |
|
292 moreover have "{(p ^^ i) | i :: nat . i \<ge> 0} \<subseteq> {\<pi>. \<pi> permutes S}" |
|
293 using exp_of_permutation1[OF assms(1)] by blast |
|
294 hence "finite {(p ^^ i) | i :: nat . i \<ge> 0}" |
|
295 by (simp add: assms(2) finite_permutations finite_subset) |
|
296 ultimately show False .. |
|
297 qed |
|
298 |
|
299 lemma power_prop: |
|
300 assumes "(p ^^ k) x = x" |
|
301 shows "(p ^^ (k * l)) x = x" |
|
302 proof (induction l) |
|
303 case 0 thus ?case by simp |
|
304 next |
|
305 case (Suc l) |
|
306 hence "(p ^^ (k * (Suc l))) x = ((p ^^ (k * l)) \<circ> (p ^^ k)) x" |
|
307 by (metis funpow_Suc_right funpow_mult) |
|
308 also have " ... = (p ^^ (k * l)) x" |
|
309 by (simp add: assms) |
|
310 also have " ... = x" |
|
311 using Suc.IH Suc.prems assms by blast |
|
312 finally show ?case . |
|
313 qed |
|
314 |
|
315 lemma exp_of_permutation4: |
|
316 assumes "p permutes S" "finite S" |
|
317 shows "\<exists>n. (p ^^ n) = id \<and> n > m" |
|
318 proof - |
|
319 obtain k where "k > 0" "(p ^^ k) = id" |
|
320 using exp_of_permutation3[OF assms] by blast |
|
321 moreover obtain n where "n * k > m" |
|
322 by (metis calculation(1) dividend_less_times_div mult.commute mult_Suc_right) |
|
323 ultimately show ?thesis |
|
324 using funpow_mult[of n k p] id_funpow[of n] mult.commute[of k n] by smt |
|
325 qed |
|
326 |
|
327 |
|
328 subsubsection\<open>Extraction of cycles from permutations\<close> |
|
329 |
|
330 definition |
|
331 least_power :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> nat" |
|
332 where "least_power f x = (LEAST n. (f ^^ n) x = x \<and> n > 0)" |
|
333 |
|
334 abbreviation |
|
335 support :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a list" |
|
336 where "support p x \<equiv> map (\<lambda>i. (p ^^ i) x) [0..< (least_power p x)]" |
|
337 |
|
338 lemma least_power_wellfounded: |
|
339 assumes "permutation p" |
|
340 shows "(p ^^ (least_power p x)) x = x" |
|
341 proof - |
|
342 obtain S where "p permutes S" "finite S" |
|
343 using assms permutation_permutes by blast |
|
344 hence "\<exists>n. (p ^^ n) x = x \<and> n > 0" |
|
345 using eq_id_iff exp_of_permutation3 by metis |
|
346 thus ?thesis unfolding least_power_def |
|
347 by (metis (mono_tags, lifting) LeastI_ex) |
|
348 qed |
|
349 |
|
350 lemma least_power_gt_zero: |
|
351 assumes "permutation p" |
|
352 shows "least_power p x > 0" |
|
353 proof (rule ccontr) |
|
354 obtain S where "p permutes S" "finite S" |
|
355 using assms permutation_permutes by blast |
|
356 hence Ex: "\<exists>n. (p ^^ n) x = x \<and> n > 0" |
|
357 using eq_id_iff exp_of_permutation3 by metis |
|
358 assume "\<not> 0 < least_power p x" hence "least_power p x = 0" |
|
359 using Ex unfolding least_power_def by (metis (mono_tags, lifting) LeastI) |
|
360 thus False unfolding least_power_def |
|
361 by (metis (mono_tags, lifting) Ex LeastI_ex less_irrefl) |
|
362 qed |
|
363 |
|
364 lemma least_power_gt_one: |
|
365 assumes "permutation p" "p x \<noteq> x" |
|
366 shows "least_power p x > Suc 0" |
|
367 proof (rule ccontr) |
|
368 obtain S where "p permutes S" "finite S" |
|
369 using assms permutation_permutes by blast |
|
370 hence Ex: "\<exists>n. (p ^^ n) x = x \<and> n > 0" |
|
371 using eq_id_iff exp_of_permutation3 by metis |
|
372 assume "\<not> Suc 0 < least_power p x" hence "least_power p x = (Suc 0)" |
|
373 using Ex unfolding least_power_def by (metis (mono_tags, lifting) LeastI Suc_lessI) |
|
374 hence "p x = x" using least_power_wellfounded[OF assms(1), of x] by simp |
|
375 from \<open>p x = x\<close> and \<open>p x \<noteq> x\<close> show False by simp |
|
376 qed |
|
377 |
|
378 lemma least_power_bound: |
|
379 assumes "permutation p" shows "\<exists>m > 0. (least_power p x) \<le> m" |
|
380 proof - |
|
381 obtain S where "p permutes S" "finite S" |
|
382 using assms permutation_permutes by blast |
|
383 hence "\<exists>n. (p ^^ n) x = x \<and> n > 0" |
|
384 using eq_id_iff exp_of_permutation3 by metis |
|
385 then obtain m :: "nat" where "m > 0" "m = (least_power p x)" |
|
386 unfolding least_power_def by (metis (mono_tags, lifting) LeastI_ex) |
|
387 thus ?thesis by blast |
|
388 qed |
|
389 |
|
390 lemma lt_least_power: |
|
391 assumes "Suc n = least_power p x" |
|
392 and "0 < i" "i \<le> n" |
|
393 shows "(p ^^ i) x \<noteq> x" |
|
394 proof (rule ccontr) |
|
395 assume "\<not> (p ^^ i) x \<noteq> x" hence "(p ^^ i) x = x" by simp |
|
396 hence "i \<in> {n. (p ^^ n) x = x \<and> n > 0}" |
|
397 using assms(2-3) by blast |
|
398 moreover have "i < least_power p x" |
|
399 using assms(3) assms(1) by linarith |
|
400 ultimately show False unfolding least_power_def |
|
401 using not_less_Least by auto |
|
402 qed |
|
403 |
|
404 lemma least_power_welldefined: |
|
405 assumes "permutation p" and "y \<in> {(p ^^ k) x | k. k \<ge> 0}" |
|
406 shows "least_power p x = least_power p y" |
|
407 proof - |
|
408 have aux_lemma: "\<And>z. least_power p z = least_power p (p z)" |
|
409 proof - |
|
410 fix z |
|
411 have "(p ^^ (least_power p z)) z = z" |
|
412 by (metis assms(1) least_power_wellfounded) |
|
413 hence "(p ^^ (least_power p z)) (p z) = (p z)" |
|
414 by (metis funpow_swap1) |
|
415 hence "least_power p z \<ge> least_power p (p z)" |
|
416 by (metis assms(1) inc_induct le_SucE least_power_gt_zero lt_least_power nat_le_linear) |
|
417 |
|
418 moreover have "(p ^^ (least_power p (p z))) (p z) = (p z)" |
|
419 by (simp add: assms(1) least_power_wellfounded) |
|
420 hence "(p ^^ (least_power p (p z))) z = z" |
|
421 by (metis assms(1) funpow_swap1 permutation_permutes permutes_def) |
|
422 hence "least_power p z \<le> least_power p (p z)" |
|
423 by (metis assms(1) least_power_gt_zero less_imp_Suc_add lt_least_power not_less_eq_eq) |
|
424 |
|
425 ultimately show "least_power p z = least_power p (p z)" by simp |
|
426 qed |
|
427 |
|
428 obtain k where "k \<ge> 0" "y = (p ^^ k) x" |
|
429 using assms(2) by blast |
|
430 thus ?thesis |
|
431 proof (induction k arbitrary: x y) |
|
432 case 0 thus ?case by simp |
|
433 next |
|
434 case (Suc k) |
|
435 have "least_power p ((p ^^ k) x) = least_power p x" |
|
436 using Suc.IH by fastforce |
|
437 thus ?case using aux_lemma |
|
438 using Suc.prems(2) by auto |
|
439 qed |
|
440 qed |
|
441 |
|
442 theorem cycle_of_permutation: |
|
443 assumes "permutation p" |
|
444 shows "cycle (support p x)" |
|
445 proof (rule ccontr) |
|
446 assume "\<not> cycle (support p x)" |
|
447 hence "\<exists> i j. i \<in> {0..<least_power p x} \<and> j \<in> {0..<least_power p x} \<and> i \<noteq> j \<and> (p ^^ i) x = (p ^^ j) x" |
|
448 using atLeast_upt by (simp add: distinct_conv_nth) |
|
449 then obtain i j where ij: "0 \<le> i" "i < j" "j < least_power p x" |
|
450 and "(p ^^ i) x = (p ^^ j) x" |
|
451 by (metis atLeast_upt le0 le_eq_less_or_eq lessThan_iff not_less set_upt) |
|
452 hence "(p ^^ i) x = (p ^^ i) ((p ^^ (j - i)) x)" |
|
453 by (metis add_diff_inverse_nat funpow_add not_less_iff_gr_or_eq o_apply) |
|
454 hence "(p ^^ (j - i)) x = x" |
|
455 using exp_of_permutation1 assms by (metis bij_pointE permutation_permutes permutes_bij) |
|
456 moreover have "0 \<le> j - i \<and> j - i < least_power p x" |
|
457 by (simp add: ij(3) less_imp_diff_less) |
|
458 hence "(p ^^ (j - i)) x \<noteq> x" using lt_least_power ij |
|
459 by (metis diff_le_self lessE less_imp_diff_less less_imp_le zero_less_diff) |
|
460 ultimately show False by simp |
|
461 qed |
|
462 |
|
463 |
|
464 subsection\<open>Decomposition on Cycles\<close> |
|
465 |
|
466 text\<open>We show that a permutation can be decomposed on cycles\<close> |
|
467 |
|
468 subsubsection\<open>Preliminaries\<close> |
|
469 |
|
470 lemma support_set: |
|
471 assumes "permutation p" |
|
472 shows "set (support p x) = {(p ^^ k) x | k. k \<ge> 0}" |
|
473 proof - |
|
474 have "{(p ^^ k) x | k. k \<ge> 0} = {(p ^^ k) x | k. 0 \<le> k \<and> k < (least_power p x)}" (is "?A = ?B") |
|
475 proof |
|
476 show "?B \<subseteq> ?A" by blast |
|
477 next |
|
478 show "?A \<subseteq> ?B" |
|
479 proof |
|
480 fix y assume "y \<in> ?A" |
|
481 then obtain k :: "nat" where k: "k \<ge> 0" "(p ^^ k) x = y" by blast |
|
482 hence "k = (least_power p x) * (k div (least_power p x)) + (k mod (least_power p x))" by simp |
|
483 hence "y = (p ^^ ((least_power p x) * (k div (least_power p x)) + (k mod (least_power p x)))) x" |
|
484 using k by auto |
|
485 hence " y = (p ^^ (k mod (least_power p x))) x" |
|
486 using power_prop[OF least_power_wellfounded[OF assms, of x], of "k div (least_power p x)"] |
|
487 by (metis add.commute funpow_add o_apply) |
|
488 moreover have "k mod (least_power p x) < least_power p x" |
|
489 using k mod_less_divisor[of "least_power p x" k, OF least_power_gt_zero[OF assms]] by simp |
|
490 ultimately show "y \<in> ?B" |
|
491 by blast |
|
492 qed |
|
493 qed |
|
494 |
|
495 moreover have "{(p ^^ k) x | k. 0 \<le> k \<and> k < (least_power p x)} = set (support p x)" (is "?B = ?C") |
|
496 proof |
|
497 show "?B \<subseteq> ?C" |
|
498 proof |
|
499 fix y assume "y \<in> {(p ^^ k) x | k. 0 \<le> k \<and> k < (least_power p x)}" |
|
500 then obtain k where "k \<ge> 0" "k < (least_power p x)" "y = (p ^^ k) x" by blast |
|
501 thus "y \<in> ?C" by auto |
|
502 qed |
|
503 next |
|
504 show "?C \<subseteq> ?B" |
|
505 proof |
|
506 fix y assume "y \<in> ?C" |
|
507 then obtain k where "k \<ge> 0" "k < (least_power p x)" "(support p x) ! k = y" by auto |
|
508 thus "y \<in> ?B" by auto |
|
509 qed |
|
510 qed |
|
511 |
|
512 ultimately show ?thesis by simp |
|
513 qed |
|
514 |
|
515 lemma disjoint_support: |
|
516 assumes "p permutes S" "finite S" |
|
517 shows "disjoint {{(p ^^ k) x | k. k \<ge> 0} | x. x \<in> S}" (is "disjoint ?A") |
|
518 proof (rule disjointI) |
|
519 { fix a b assume "a \<in> ?A" "b \<in> ?A" "a \<inter> b \<noteq> {}" |
|
520 then obtain x y where x: "x \<in> S" "a = {(p ^^ k) x | k. k \<ge> 0}" |
|
521 and y: "y \<in> S" "b = {(p ^^ k) y | k. k \<ge> 0}" by blast |
|
522 assume "a \<inter> b \<noteq> {}" |
|
523 then obtain z kx ky where z: "kx \<ge> 0" "ky \<ge> 0" "z = (p ^^ kx) x" "z = (p ^^ ky) y" |
|
524 using x(2) y(2) by blast |
|
525 have "a \<subseteq> b" |
|
526 proof |
|
527 fix w assume "w \<in> a" |
|
528 then obtain k where k: "k \<ge> 0" "w = (p ^^ k) x" using x by blast |
|
529 define l where "l = (kx div (least_power p w)) + 1" |
|
530 hence l: "l * (least_power p w) > kx" |
|
531 using least_power_gt_zero assms One_nat_def add.right_neutral add_Suc_right |
|
532 mult.commute permutation_permutes |
|
533 by (metis dividend_less_times_div mult_Suc_right) |
|
534 |
|
535 have "w = (p ^^ (l * (least_power p w))) w" |
|
536 by (metis assms least_power_wellfounded mult.commute permutation_permutes power_prop) |
|
537 also have "... = (p ^^ (l * (least_power p w) + k)) x" |
|
538 using k by (simp add: funpow_add) |
|
539 also have " ... = (p ^^ (l * (least_power p w) + k - kx + kx)) x" |
|
540 using l by auto |
|
541 also have " ... = (p ^^ (l * (least_power p w) + k - kx)) ((p ^^ kx) x)" |
|
542 by (simp add: funpow_add) |
|
543 also have " ... = (p ^^ (l * (least_power p w) + k - kx)) ((p ^^ ky) y)" using z |
|
544 by simp |
|
545 finally have "w = (p ^^ (l * (least_power p w) + k - kx + ky)) y" |
|
546 by (simp add: funpow_add) |
|
547 thus "w \<in> b" using y by blast |
|
548 qed } note aux_lemma = this |
|
549 |
|
550 fix a b assume ab: "a \<in> ?A" "b \<in> ?A" "a \<noteq> b" |
|
551 show "a \<inter> b = {}" |
|
552 proof (rule ccontr) |
|
553 assume "a \<inter> b \<noteq> {}" thus False using aux_lemma ab |
|
554 by (metis (no_types, lifting) inf.absorb2 inf.orderE) |
|
555 qed |
|
556 qed |
|
557 |
|
558 lemma support_coverture: |
|
559 assumes "p permutes S" "finite S" |
|
560 shows "\<Union>{{(p ^^ k) x | k. k \<ge> 0} | x. x \<in> S} = S" |
|
561 proof |
|
562 show "\<Union>{{(p ^^ k) x |k. 0 \<le> k} |x. x \<in> S} \<subseteq> S" |
|
563 proof |
|
564 fix y assume "y \<in> \<Union>{{(p ^^ k) x |k. 0 \<le> k} |x. x \<in> S}" |
|
565 then obtain x k where x: "x \<in> S" and k: "k \<ge> 0" and y: "y = (p ^^ k) x" by blast |
|
566 have "(p ^^ k) x \<in> S" |
|
567 proof (induction k) |
|
568 case 0 thus ?case using x by simp |
|
569 next |
|
570 case (Suc k) thus ?case using assms |
|
571 by (simp add: permutes_in_image) |
|
572 qed |
|
573 thus "y \<in> S" using y by simp |
|
574 qed |
|
575 next |
|
576 show "S \<subseteq> \<Union>{{(p ^^ k) x |k. 0 \<le> k} |x. x \<in> S}" |
|
577 proof |
|
578 fix x assume x: "x \<in> S" |
|
579 hence "x \<in> {(p ^^ k) x |k. 0 \<le> k}" |
|
580 by (metis (mono_tags, lifting) CollectI funpow_0 le_numeral_extra(3)) |
|
581 thus "x \<in> \<Union>{{(p ^^ k) x |k. 0 \<le> k} |x. x \<in> S}" using x by blast |
|
582 qed |
|
583 qed |
|
584 |
|
585 theorem cycle_restrict: |
|
586 assumes "permutation p" "y \<in> set (support p x)" |
|
587 shows "p y = (cycle_of_list (support p x)) y" |
|
588 proof - |
|
589 have "\<And> i. \<lbrakk> 0 \<le> i; i < length (support p x) - 1 \<rbrakk> \<Longrightarrow> |
|
590 p ((support p x) ! i) = (support p x) ! (i + 1)" |
|
591 proof - |
|
592 fix i assume i: "0 \<le> i" "i < length (support p x) - 1" |
|
593 hence "p ((support p x) ! i) = p ((p ^^ i) x)" by simp |
|
594 also have " ... = (p ^^ (i + 1)) x" by simp |
|
595 also have " ... = (support p x) ! (i + 1)" |
|
596 using i by simp |
|
597 finally show "p ((support p x) ! i) = (support p x) ! (i + 1)" . |
|
598 qed |
|
599 hence 1: "map p (butlast (support p x)) = tl (support p x)" |
|
600 using nth_equalityI[of "map p (butlast (support p x))" "tl (support p x)"] |
|
601 by (smt Suc_eq_plus1 le0 length_butlast length_map length_tl nth_butlast nth_map nth_tl) |
|
602 |
|
603 have "p ((support p x) ! (length (support p x) - 1)) = p ((p ^^ (length (support p x) - 1)) x)" |
|
604 using assms(2) by auto |
|
605 also have " ... = (p ^^ (length (support p x))) x" |
|
606 by (metis (mono_tags, lifting) Suc_pred' assms(2) funpow_Suc_right |
|
607 funpow_swap1 length_pos_if_in_set o_apply) |
|
608 also have " ... = x" |
|
609 by (simp add: assms(1) least_power_wellfounded) |
|
610 also have " ... = (support p x) ! 0" |
|
611 by (simp add: assms(1) least_power_gt_zero) |
|
612 finally have "p ((support p x) ! (length (support p x) - 1)) = (support p x) ! 0" . |
|
613 hence 2: "p (last (support p x)) = hd (support p x)" |
|
614 by (metis assms(2) hd_conv_nth last_conv_nth length_greater_0_conv length_pos_if_in_set) |
|
615 |
|
616 have "map p (support p x) = (tl (support p x)) @ [hd (support p x)]" using 1 2 |
|
617 by (metis (no_types, lifting) assms(2) last_map length_greater_0_conv |
|
618 length_pos_if_in_set list.map_disc_iff map_butlast snoc_eq_iff_butlast) |
|
619 hence "map p (support p x) = rotate1 (support p x)" |
|
620 by (metis assms(2) length_greater_0_conv length_pos_if_in_set rotate1_hd_tl) |
|
621 |
|
622 moreover have "map (cycle_of_list (support p x)) (support p x) = rotate1 (support p x)" |
|
623 using cyclic_rotation[OF cycle_of_permutation[OF assms(1)], of 1 x] by simp |
|
624 |
|
625 ultimately show ?thesis using assms(2) |
|
626 using map_eq_conv by fastforce |
|
627 qed |
|
628 |
|
629 |
|
630 subsubsection\<open>Decomposition\<close> |
|
631 |
|
632 inductive cycle_decomp :: "'a set \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> bool" where |
|
633 empty: "cycle_decomp {} id" | |
|
634 comp: "\<lbrakk> cycle_decomp I p; cycle cs; set cs \<inter> I = {} \<rbrakk> \<Longrightarrow> |
|
635 cycle_decomp (set cs \<union> I) ((cycle_of_list cs) \<circ> p)" |
|
636 |
|
637 |
|
638 lemma semidecomposition: |
|
639 assumes "p permutes S" "finite S" |
|
640 shows "(\<lambda>y. if y \<in> (S - set (support p x)) then p y else y) permutes (S - set (support p x))" |
|
641 (is "?q permutes ?S'") |
|
642 proof - |
|
643 have "\<And>y. y \<notin> S \<Longrightarrow> p y = y" |
|
644 by (meson assms permutes_not_in) |
|
645 |
|
646 moreover have cycle_surj: "(cycle_of_list (support p x)) ` set (support p x) = set (support p x)" |
|
647 using cycle_is_surj cycle_of_permutation assms permutation_permutes by metis |
|
648 hence "\<And>y. y \<in> set (support p x) \<Longrightarrow> p y \<in> set (support p x)" |
|
649 using cycle_restrict assms permutation_permutes by (metis imageI) |
|
650 |
|
651 ultimately |
|
652 have 1: "\<And>y. y \<notin> ?S' \<Longrightarrow> p y \<notin> ?S'" by auto |
|
653 have 2: "\<And>y. y \<in> ?S' \<Longrightarrow> p y \<in> ?S'" |
|
654 proof - |
|
655 fix y assume y: "y \<in> ?S'" show "p y \<in> ?S'" |
|
656 proof (rule ccontr) |
|
657 assume "p y \<notin> ?S'" hence "p y \<in> set (support p x)" |
|
658 using assms(1) permutes_in_image y by fastforce |
|
659 then obtain y' where y': "y' \<in> set (support p x)" "(cycle_of_list (support p x)) y' = p y" |
|
660 using cycle_surj by (metis (mono_tags, lifting) imageE) |
|
661 hence "p y' = p y" |
|
662 using cycle_restrict assms permutation_permutes by metis |
|
663 hence "y = y'" by (metis assms(1) permutes_def) |
|
664 thus False using y y' by blast |
|
665 qed |
|
666 qed |
|
667 |
|
668 have "p ` ?S' = ?S'" |
|
669 proof - |
|
670 have "\<And> y. y \<in> ?S' \<Longrightarrow> \<exists>!x. p x = y" |
|
671 by (metis assms(1) permutes_def) |
|
672 hence "\<And> y. y \<in> ?S' \<Longrightarrow> \<exists>x \<in> ?S'. p x = y" using 1 by metis |
|
673 thus ?thesis using 2 by blast |
|
674 qed |
|
675 hence "bij_betw p ?S' ?S'" |
|
676 by (metis DiffD1 assms(1) bij_betw_subset permutes_imp_bij subsetI) |
|
677 hence "bij_betw ?q ?S' ?S'" by (smt bij_betw_cong) |
|
678 moreover have "\<And>y. y \<notin> ?S' \<Longrightarrow> ?q y = y" by auto |
|
679 ultimately show ?thesis |
|
680 using bij_imp_permutes by blast |
|
681 qed |
|
682 |
|
683 |
|
684 lemma cycle_decomposition_aux: |
|
685 assumes "p permutes S" "finite S" "card S = k" |
|
686 shows "cycle_decomp S p" using assms |
|
687 proof(induct arbitrary: S p rule: less_induct) |
|
688 case (less x) thus ?case |
|
689 proof (cases "S = {}") |
|
690 case True thus ?thesis |
|
691 (* using less empty by auto *) |
|
692 by (metis empty less.prems(1) permutes_empty) |
|
693 next |
|
694 case False |
|
695 then obtain x where x: "x \<in> S" by blast |
|
696 define S' :: "'a set" where S': "S' = S - set (support p x)" |
|
697 define q :: "'a \<Rightarrow> 'a" where q: "q = (\<lambda>x. if x \<in> S' then p x else x)" |
|
698 hence q_permutes: "q permutes S'" |
|
699 using semidecomposition[OF less.prems(1-2), of x] S' q by blast |
|
700 moreover have "x \<in> set (support p x)" |
|
701 by (smt add.left_neutral diff_zero funpow_0 in_set_conv_nth least_power_gt_zero |
|
702 length_map length_upt less.prems(1) less.prems(2) nth_map_upt permutation_permutes) |
|
703 hence "card S' < card S" |
|
704 by (metis Diff_iff S' \<open>x \<in> S\<close> card_seteq leI less.prems(2) subsetI) |
|
705 ultimately have "cycle_decomp S' q" |
|
706 using S' less.hyps less.prems(2) less.prems(3) by blast |
|
707 |
|
708 moreover have "p = (cycle_of_list (support p x)) \<circ> q" |
|
709 proof |
|
710 fix y show "p y = ((cycle_of_list (support p x)) \<circ> q) y" |
|
711 proof (cases) |
|
712 assume y: "y \<in> set (support p x)" hence "y \<notin> S'" using S' by simp |
|
713 hence "q y = y" using q by simp |
|
714 thus ?thesis |
|
715 (* using cycle_restrict less.prems(1) less.prems(2) permutation_permutes y by fastforce *) |
|
716 using comp_apply cycle_restrict less.prems permutation_permutes y by fastforce |
|
717 next |
|
718 assume y: "y \<notin> set (support p x)" thus ?thesis |
|
719 proof (cases) |
|
720 assume "y \<in> S'" |
|
721 hence "q y \<in> S'" using q_permutes |
|
722 by (simp add: permutes_in_image) |
|
723 hence "q y \<notin> set (support p x)" |
|
724 using S' by blast |
|
725 hence "(cycle_of_list (support p x)) (q y) = (q y)" |
|
726 by (metis cycle_of_permutation id_outside_supp less.prems(1-2) permutation_permutes) |
|
727 thus ?thesis by (simp add: \<open>y \<in> S'\<close> q) |
|
728 next |
|
729 assume "y \<notin> S'" hence "y \<notin> S" using y S' by blast |
|
730 hence "(cycle_of_list (support p x) \<circ> q) y = (cycle_of_list (support p x)) y" |
|
731 by (simp add: \<open>y \<notin> S'\<close> q) |
|
732 also have " ... = y" |
|
733 by (metis cycle_of_permutation id_outside_supp less.prems(1-2) permutation_permutes y) |
|
734 also have " ... = p y" |
|
735 by (metis \<open>y \<notin> S\<close> less.prems(1) permutes_def) |
|
736 finally show ?thesis by simp |
|
737 qed |
|
738 qed |
|
739 qed |
|
740 moreover have "cycle (support p x)" |
|
741 using cycle_of_permutation less.prems permutation_permutes by fastforce |
|
742 moreover have "set (support p x) \<inter> S' = {}" using S' by simp |
|
743 moreover have "set (support p x) \<subseteq> S" |
|
744 using support_coverture[OF less.prems(1-2)] support_set[of p x] x |
|
745 permutation_permutes[of p] less.prems(1-2) by blast |
|
746 hence "S = set (support p x) \<union> S'" using S' by blast |
|
747 ultimately show ?thesis using comp[of S' q "support p x"] by auto |
|
748 qed |
|
749 qed |
|
750 |
|
751 theorem cycle_decomposition: |
|
752 assumes "p permutes S" "finite S" |
|
753 shows "cycle_decomp S p" |
|
754 using assms cycle_decomposition_aux by blast |
|
755 |
|
756 end |