41 theorem cyclic_rotation: |
41 theorem cyclic_rotation: |
42 assumes "cycle cs" shows "map ((cycle_of_list cs) ^^ n) cs = rotate n cs" |
42 assumes "cycle cs" shows "map ((cycle_of_list cs) ^^ n) cs = rotate n cs" |
43 proof - |
43 proof - |
44 { have "map (cycle_of_list cs) cs = rotate1 cs" using assms(1) |
44 { have "map (cycle_of_list cs) cs = rotate1 cs" using assms(1) |
45 proof (induction cs rule: cycle_of_list.induct) |
45 proof (induction cs rule: cycle_of_list.induct) |
46 case (1 i j cs) thus ?case |
46 case (1 i j cs) |
|
47 then have \<open>i \<notin> set cs\<close> \<open>j \<notin> set cs\<close> |
|
48 by auto |
|
49 then have \<open>map (Transposition.transpose i j) cs = cs\<close> |
|
50 by (auto intro: map_idI simp add: transpose_eq_iff) |
|
51 show ?case |
47 proof (cases) |
52 proof (cases) |
48 assume "cs = Nil" thus ?thesis by simp |
53 assume "cs = Nil" thus ?thesis by simp |
49 next |
54 next |
50 assume "cs \<noteq> Nil" hence ge_two: "length (j # cs) \<ge> 2" |
55 assume "cs \<noteq> Nil" hence ge_two: "length (j # cs) \<ge> 2" |
51 using not_less by auto |
56 using not_less by auto |
52 have "map (cycle_of_list (i # j # cs)) (i # j # cs) = |
57 have "map (cycle_of_list (i # j # cs)) (i # j # cs) = |
53 map (Fun.swap i j id) (map (cycle_of_list (j # cs)) (i # j # cs))" by simp |
58 map (transpose i j) (map (cycle_of_list (j # cs)) (i # j # cs))" by simp |
54 also have " ... = map (Fun.swap i j id) (i # (rotate1 (j # cs)))" |
59 also have " ... = map (transpose i j) (i # (rotate1 (j # cs)))" |
55 by (metis "1.IH" "1.prems" distinct.simps(2) id_outside_supp list.simps(9)) |
60 by (metis "1.IH" "1.prems" distinct.simps(2) id_outside_supp list.simps(9)) |
56 also have " ... = map (Fun.swap i j id) (i # (cs @ [j]))" by simp |
61 also have " ... = map (transpose i j) (i # (cs @ [j]))" by simp |
57 also have " ... = j # (map (Fun.swap i j id) cs) @ [i]" by simp |
62 also have " ... = j # (map (transpose i j) cs) @ [i]" by simp |
58 also have " ... = j # cs @ [i]" |
63 also have " ... = j # cs @ [i]" |
59 by (metis "1.prems" distinct.simps(2) list.set_intros(2) map_idI swap_id_eq) |
64 using \<open>map (Transposition.transpose i j) cs = cs\<close> by simp |
60 also have " ... = rotate1 (i # j # cs)" by simp |
65 also have " ... = rotate1 (i # j # cs)" by simp |
61 finally show ?thesis . |
66 finally show ?thesis . |
62 qed |
67 qed |
63 qed simp_all } |
68 qed simp_all } |
64 note cyclic_rotation' = this |
69 note cyclic_rotation' = this |
116 shows "p \<circ> (cycle_of_list cs) \<circ> (inv p) = cycle_of_list (map p cs)" |
121 shows "p \<circ> (cycle_of_list cs) \<circ> (inv p) = cycle_of_list (map p cs)" |
117 using assms |
122 using assms |
118 proof (induction cs rule: cycle_of_list.induct) |
123 proof (induction cs rule: cycle_of_list.induct) |
119 case (1 i j cs) |
124 case (1 i j cs) |
120 have "p \<circ> cycle_of_list (i # j # cs) \<circ> inv p = |
125 have "p \<circ> cycle_of_list (i # j # cs) \<circ> inv p = |
121 (p \<circ> (Fun.swap i j id) \<circ> inv p) \<circ> (p \<circ> cycle_of_list (j # cs) \<circ> inv p)" |
126 (p \<circ> (transpose i j) \<circ> inv p) \<circ> (p \<circ> cycle_of_list (j # cs) \<circ> inv p)" |
122 by (simp add: assms(2) bij_is_inj fun.map_comp) |
127 by (simp add: assms(2) bij_is_inj fun.map_comp) |
123 also have " ... = (transpose (p i) (p j)) \<circ> (p \<circ> cycle_of_list (j # cs) \<circ> inv p)" |
128 also have " ... = (transpose (p i) (p j)) \<circ> (p \<circ> cycle_of_list (j # cs) \<circ> inv p)" |
124 using "1.prems"(2) by (simp add: bij_inv_eq_iff transpose_apply_commute fun_eq_iff bij_betw_inv_into_left) |
129 using "1.prems"(2) by (simp add: bij_inv_eq_iff transpose_apply_commute fun_eq_iff bij_betw_inv_into_left) |
125 finally have "p \<circ> cycle_of_list (i # j # cs) \<circ> inv p = |
130 finally have "p \<circ> cycle_of_list (i # j # cs) \<circ> inv p = |
126 (transpose (p i) (p j)) \<circ> (cycle_of_list (map p (j # cs)))" |
131 (transpose (p i) (p j)) \<circ> (cycle_of_list (map p (j # cs)))" |