(* Title: HOL/Algebra/Cycles.thy
Author: Paulo EmÃlio de Vilhena
*)
theory Cycles
imports "HOL-Library.Permutations" "HOL-Library.FuncSet"
begin
section \<open>Cycles\<close>
abbreviation cycle :: "'a list \<Rightarrow> bool" where
"cycle cs \<equiv> distinct cs"
fun cycle_of_list :: "'a list \<Rightarrow> 'a \<Rightarrow> 'a"
where
"cycle_of_list (i # j # cs) = (Fun.swap i j id) \<circ> (cycle_of_list (j # cs))"
| "cycle_of_list cs = id"
subsection\<open>Cycles as Rotations\<close>
text\<open>We start proving that the function derived from a cycle rotates its support list.\<close>
lemma id_outside_supp:
assumes "cycle cs" and "x \<notin> set cs"
shows "(cycle_of_list cs) x = x" using assms
proof (induction cs rule: cycle_of_list.induct)
case (1 i j cs)
have "cycle_of_list (i # j # cs) x = (Fun.swap i j id) (cycle_of_list (j # cs) x)" by simp
also have " ... = (Fun.swap i j id) x"
using "1.IH" "1.prems"(1) "1.prems"(2) by auto
also have " ... = x" using 1(3) by simp
finally show ?case .
next
case "2_1" thus ?case by simp
next
case "2_2" thus ?case by simp
qed
lemma cycle_permutes:
assumes "cycle cs"
shows "permutation (cycle_of_list cs)"
proof (induction rule: cycle_of_list.induct)
case (1 i j cs) thus ?case
by (metis cycle_of_list.simps(1) permutation_compose permutation_swap_id)
next
case "2_1" thus ?case by simp
next
case "2_2" thus ?case by simp
qed
theorem cyclic_rotation:
assumes "cycle cs"
shows "map ((cycle_of_list cs) ^^ n) cs = rotate n cs"
proof -
{ have "map (cycle_of_list cs) cs = rotate1 cs" using assms(1)
proof (induction cs rule: cycle_of_list.induct)
case (1 i j cs) thus ?case
proof (cases)
assume "cs = Nil" thus ?thesis by simp
next
assume "cs \<noteq> Nil" hence ge_two: "length (j # cs) \<ge> 2"
using not_less by auto
have "map (cycle_of_list (i # j # cs)) (i # j # cs) =
map (Fun.swap i j id) (map (cycle_of_list (j # cs)) (i # j # cs))" by simp
also have " ... = map (Fun.swap i j id) (i # (rotate1 (j # cs)))"
by (metis "1.IH" "1.prems" distinct.simps(2) id_outside_supp list.simps(9))
also have " ... = map (Fun.swap i j id) (i # (cs @ [j]))" by simp
also have " ... = j # (map (Fun.swap i j id) cs) @ [i]" by simp
also have " ... = j # cs @ [i]"
by (metis "1.prems" distinct.simps(2) list.set_intros(2) map_idI swap_id_eq)
also have " ... = rotate1 (i # j # cs)" by simp
finally show ?thesis .
qed
next
case "2_1" thus ?case by simp
next
case "2_2" thus ?case by simp
qed }
note cyclic_rotation' = this
from assms show ?thesis
proof (induction n)
case 0 thus ?case by simp
next
case (Suc n)
have "map ((cycle_of_list cs) ^^ (Suc n)) cs =
map (cycle_of_list cs) (map ((cycle_of_list cs) ^^ n) cs)" by simp
also have " ... = map (cycle_of_list cs) (rotate n cs)"
by (simp add: Suc.IH assms)
also have " ... = rotate (Suc n) cs"
using cyclic_rotation'
by (metis rotate1_rotate_swap rotate_Suc rotate_map)
finally show ?case .
qed
qed
corollary cycle_is_surj:
assumes "cycle cs"
shows "(cycle_of_list cs) ` (set cs) = (set cs)"
using cyclic_rotation[OF assms, of 1] by (simp add: image_set)
corollary cycle_is_id_root:
assumes "cycle cs"
shows "(cycle_of_list cs) ^^ (length cs) = id"
proof -
have "map ((cycle_of_list cs) ^^ (length cs)) cs = cs"
by (simp add: assms cyclic_rotation)
hence "\<And>x. x \<in> (set cs) \<Longrightarrow> ((cycle_of_list cs) ^^ (length cs)) x = x"
using map_eq_conv by fastforce
moreover have "\<And>n x. x \<notin> (set cs) \<Longrightarrow> ((cycle_of_list cs) ^^ n) x = x"
proof -
fix n show "\<And>x. x \<notin> (set cs) \<Longrightarrow> ((cycle_of_list cs) ^^ n) x = x"
proof (induction n)
case 0 thus ?case by simp
next
case (Suc n) thus ?case using id_outside_supp[OF assms] by simp
qed
qed
hence "\<And>x. x \<notin> (set cs) \<Longrightarrow> ((cycle_of_list cs) ^^ (length cs)) x = x" by simp
ultimately show ?thesis
by (meson eq_id_iff)
qed
corollary
assumes "cycle cs"
shows "(cycle_of_list cs) = (cycle_of_list (rotate n cs))"
proof -
{ fix cs :: "'a list" assume A: "cycle cs"
have "(cycle_of_list cs) = (cycle_of_list (rotate1 cs))"
proof
have "\<And>x. x \<in> set cs \<Longrightarrow> (cycle_of_list cs) x = (cycle_of_list (rotate1 cs)) x"
proof -
have "cycle (rotate1 cs)" using A by simp
hence "map (cycle_of_list (rotate1 cs)) (rotate1 cs) = (rotate 2 cs)"
using cyclic_rotation by (metis Suc_eq_plus1 add.left_neutral
funpow.simps(2) funpow_simps_right(1) o_id one_add_one rotate_Suc rotate_def)
also have " ... = map (cycle_of_list cs) (rotate1 cs)"
using cyclic_rotation[OF A]
by (metis One_nat_def Suc_1 funpow.simps(2) id_apply map_map rotate0 rotate_Suc)
finally have "map (cycle_of_list (rotate1 cs)) (rotate1 cs) =
map (cycle_of_list cs) (rotate1 cs)" .
moreover fix x assume "x \<in> set cs"
ultimately show "(cycle_of_list cs) x = (cycle_of_list (rotate1 cs)) x" by auto
qed
moreover have "\<And>x. x \<notin> set cs \<Longrightarrow> (cycle_of_list cs) x = (cycle_of_list (rotate1 cs)) x"
using A by (simp add: id_outside_supp)
ultimately show "\<And>x. (cycle_of_list cs) x = (cycle_of_list (rotate1 cs)) x" by blast
qed }
note rotate1_lemma = this
show "cycle_of_list cs = cycle_of_list (rotate n cs)"
proof (induction n)
case 0 thus ?case by simp
next
case (Suc n)
have "cycle (rotate n cs)" by (simp add: assms)
thus ?case using rotate1_lemma[of "rotate n cs"]
by (simp add: Suc.IH)
qed
qed
subsection\<open>Conjugation of cycles\<close>
lemma conjugation_of_cycle:
assumes "cycle cs" and "bij p"
shows "p \<circ> (cycle_of_list cs) \<circ> (inv p) = cycle_of_list (map p cs)"
using assms
proof (induction cs rule: cycle_of_list.induct)
case (1 i j cs)
have "p \<circ> cycle_of_list (i # j # cs) \<circ> inv p =
(p \<circ> (Fun.swap i j id) \<circ> inv p) \<circ> (p \<circ> cycle_of_list (j # cs) \<circ> inv p)"
by (simp add: assms(2) bij_is_inj fun.map_comp)
also have " ... = (Fun.swap (p i) (p j) id) \<circ> (p \<circ> cycle_of_list (j # cs) \<circ> inv p)"
by (simp add: "1.prems"(2) bij_is_inj bij_swap_comp comp_swap o_assoc)
finally have "p \<circ> cycle_of_list (i # j # cs) \<circ> inv p =
(Fun.swap (p i) (p j) id) \<circ> (cycle_of_list (map p (j # cs)))"
using "1.IH" "1.prems"(1) assms(2) by fastforce
thus ?case by (metis cycle_of_list.simps(1) list.simps(9))
next
case "2_1" thus ?case
by (metis bij_is_surj comp_id cycle_of_list.simps(2) list.simps(8) surj_iff)
next
case "2_2" thus ?case
by (metis bij_is_surj comp_id cycle_of_list.simps(3) list.simps(8) list.simps(9) surj_iff)
qed
subsection\<open>When Cycles Commute\<close>
lemma cycles_commute:
assumes "cycle \<sigma>1" "cycle \<sigma>2" and "set \<sigma>1 \<inter> set \<sigma>2 = {}"
shows "(cycle_of_list \<sigma>1) \<circ> (cycle_of_list \<sigma>2) = (cycle_of_list \<sigma>2) \<circ> (cycle_of_list \<sigma>1)"
proof -
{ fix \<pi>1 :: "'a list" and \<pi>2 :: "'a list" and x :: "'a"
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"
have "((cycle_of_list \<pi>1) \<circ> (cycle_of_list \<pi>2)) x =
((cycle_of_list \<pi>2) \<circ> (cycle_of_list \<pi>1)) x"
proof -
have "((cycle_of_list \<pi>1) \<circ> (cycle_of_list \<pi>2)) x = (cycle_of_list \<pi>1) x"
using id_outside_supp[OF A(2) A(5)] by simp
also have " ... = ((cycle_of_list \<pi>2) \<circ> (cycle_of_list \<pi>1)) x"
using id_outside_supp[OF A(2), of "(cycle_of_list \<pi>1) x"]
cycle_is_surj[OF A(1)] A(3) A(4) by fastforce
finally show ?thesis .
qed }
note aux_lemma = this
let ?\<sigma>12 = "\<lambda>x. ((cycle_of_list \<sigma>1) \<circ> (cycle_of_list \<sigma>2)) x"
let ?\<sigma>21 = "\<lambda>x. ((cycle_of_list \<sigma>2) \<circ> (cycle_of_list \<sigma>1)) x"
show ?thesis
proof
fix x have "x \<in> set \<sigma>1 \<union> set \<sigma>2 \<or> x \<notin> set \<sigma>1 \<union> set \<sigma>2" by blast
from this show "?\<sigma>12 x = ?\<sigma>21 x"
proof
assume "x \<in> set \<sigma>1 \<union> set \<sigma>2"
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
from this show "?\<sigma>12 x = ?\<sigma>21 x"
proof
assume "x \<in> set \<sigma>1 \<and> x \<notin> set \<sigma>2" thus ?thesis
using aux_lemma[OF assms(1-3)] by simp
next
assume "x \<notin> set \<sigma>1 \<and> x \<in> set \<sigma>2" thus ?thesis
using assms aux_lemma inf_commute by metis
qed
next
assume "x \<notin> set \<sigma>1 \<union> set \<sigma>2" thus ?thesis using id_outside_supp assms(1-2)
by (metis UnCI comp_apply)
qed
qed
qed
subsection\<open>Cycles from Permutations\<close>
subsubsection\<open>Exponentiation of permutations\<close>
text\<open>Some important properties of permutations before defining how to extract its cycles\<close>
lemma exp_of_permutation1:
assumes "p permutes S"
shows "(p ^^ n) permutes S" using assms
proof (induction n)
case 0 thus ?case by (simp add: permutes_def)
next
case (Suc n) thus ?case by (metis funpow_Suc_right permutes_compose)
qed
lemma exp_of_permutation2:
assumes "p permutes S"
and "i < j" "(p ^^ j) = (p ^^ i)"
shows "(p ^^ (j - i)) = id" using assms
proof -
have "(p ^^ i) \<circ> (p ^^ (j - i)) = (p ^^ j)"
by (metis add_diff_inverse_nat assms(2) funpow_add le_eq_less_or_eq not_le)
also have " ... = (p ^^ i)" using assms(3) by simp
finally have "(p ^^ i) \<circ> (p ^^ (j - i)) = (p ^^ i)" .
moreover have "bij (p ^^ i)" using exp_of_permutation1[OF assms(1)]
using permutes_bij by auto
ultimately show ?thesis
by (metis (no_types, lifting) bij_is_inj comp_assoc fun.map_id inv_o_cancel)
qed
lemma exp_of_permutation3:
assumes "p permutes S" "finite S"
shows "\<exists>n. (p ^^ n) = id \<and> n > 0"
proof (rule ccontr)
assume "\<nexists>n. (p ^^ n) = id \<and> 0 < n"
hence S: "\<And>n. n > 0 \<Longrightarrow> (p ^^ n) \<noteq> id" by auto
hence "\<And>i j. \<lbrakk> i \<ge> 0; j \<ge> 0 \<rbrakk> \<Longrightarrow> i \<noteq> j \<Longrightarrow> (p ^^ i) \<noteq> (p ^^ j)"
proof -
fix i :: "nat" and j :: "nat" assume "i \<ge> 0" "j \<ge> 0" and Ineq: "i \<noteq> j"
show "(p ^^ i) \<noteq> (p ^^ j)"
proof (rule ccontr)
assume "\<not> (p ^^ i) \<noteq> (p ^^ j)" hence Eq: "(p ^^ i) = (p ^^ j)" by simp
have "(p ^^ (j - i)) = id" if "j > i"
using Eq exp_of_permutation2[OF assms(1) that] by simp
moreover have "(p ^^ (i - j)) = id" if "i > j"
using Eq exp_of_permutation2[OF assms(1) that] by simp
ultimately show False using Ineq S
by (meson le_eq_less_or_eq not_le zero_less_diff)
qed
qed
hence "bij_betw (\<lambda>i. (p ^^ i)) {i :: nat . i \<ge> 0} {(p ^^ i) | i :: nat . i \<ge> 0}"
unfolding bij_betw_def inj_on_def by blast
hence "infinite {(p ^^ i) | i :: nat . i \<ge> 0}"
using bij_betw_finite by auto
moreover have "{(p ^^ i) | i :: nat . i \<ge> 0} \<subseteq> {\<pi>. \<pi> permutes S}"
using exp_of_permutation1[OF assms(1)] by blast
hence "finite {(p ^^ i) | i :: nat . i \<ge> 0}"
by (simp add: assms(2) finite_permutations finite_subset)
ultimately show False ..
qed
lemma power_prop:
assumes "(p ^^ k) x = x"
shows "(p ^^ (k * l)) x = x"
proof (induction l)
case 0 thus ?case by simp
next
case (Suc l)
hence "(p ^^ (k * (Suc l))) x = ((p ^^ (k * l)) \<circ> (p ^^ k)) x"
by (metis funpow_Suc_right funpow_mult)
also have " ... = (p ^^ (k * l)) x"
by (simp add: assms)
also have " ... = x"
using Suc.IH Suc.prems assms by blast
finally show ?case .
qed
lemma exp_of_permutation4:
assumes "p permutes S" "finite S"
shows "\<exists>n. (p ^^ n) = id \<and> n > m"
proof -
obtain k where "k > 0" "(p ^^ k) = id"
using exp_of_permutation3[OF assms] by blast
moreover obtain n where "n * k > m"
by (metis calculation(1) dividend_less_times_div mult.commute mult_Suc_right)
ultimately show ?thesis
by (metis (full_types) funpow_mult id_funpow mult.commute)
qed
subsubsection\<open>Extraction of cycles from permutations\<close>
definition
least_power :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> nat"
where "least_power f x = (LEAST n. (f ^^ n) x = x \<and> n > 0)"
abbreviation
support :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a list"
where "support p x \<equiv> map (\<lambda>i. (p ^^ i) x) [0..< (least_power p x)]"
lemma least_power_wellfounded:
assumes "permutation p"
shows "(p ^^ (least_power p x)) x = x"
proof -
obtain S where "p permutes S" "finite S"
using assms permutation_permutes by blast
hence "\<exists>n. (p ^^ n) x = x \<and> n > 0"
using eq_id_iff exp_of_permutation3 by metis
thus ?thesis unfolding least_power_def
by (metis (mono_tags, lifting) LeastI_ex)
qed
lemma least_power_gt_zero:
assumes "permutation p"
shows "least_power p x > 0"
proof (rule ccontr)
obtain S where "p permutes S" "finite S"
using assms permutation_permutes by blast
hence Ex: "\<exists>n. (p ^^ n) x = x \<and> n > 0"
using eq_id_iff exp_of_permutation3 by metis
assume "\<not> 0 < least_power p x" hence "least_power p x = 0"
using Ex unfolding least_power_def by (metis (mono_tags, lifting) LeastI)
thus False unfolding least_power_def
by (metis (mono_tags, lifting) Ex LeastI_ex less_irrefl)
qed
lemma least_power_gt_one:
assumes "permutation p" "p x \<noteq> x"
shows "least_power p x > Suc 0"
proof (rule ccontr)
obtain S where "p permutes S" "finite S"
using assms permutation_permutes by blast
hence Ex: "\<exists>n. (p ^^ n) x = x \<and> n > 0"
using eq_id_iff exp_of_permutation3 by metis
assume "\<not> Suc 0 < least_power p x" hence "least_power p x = (Suc 0)"
using Ex unfolding least_power_def by (metis (mono_tags, lifting) LeastI Suc_lessI)
hence "p x = x" using least_power_wellfounded[OF assms(1), of x] by simp
from \<open>p x = x\<close> and \<open>p x \<noteq> x\<close> show False by simp
qed
lemma least_power_bound:
assumes "permutation p" shows "\<exists>m > 0. (least_power p x) \<le> m"
proof -
obtain S where "p permutes S" "finite S"
using assms permutation_permutes by blast
hence "\<exists>n. (p ^^ n) x = x \<and> n > 0"
using eq_id_iff exp_of_permutation3 by metis
then obtain m :: "nat" where "m > 0" "m = (least_power p x)"
unfolding least_power_def by (metis (mono_tags, lifting) LeastI_ex)
thus ?thesis by blast
qed
lemma lt_least_power:
assumes "Suc n = least_power p x"
and "0 < i" "i \<le> n"
shows "(p ^^ i) x \<noteq> x"
proof (rule ccontr)
assume "\<not> (p ^^ i) x \<noteq> x" hence "(p ^^ i) x = x" by simp
hence "i \<in> {n. (p ^^ n) x = x \<and> n > 0}"
using assms(2-3) by blast
moreover have "i < least_power p x"
using assms(3) assms(1) by linarith
ultimately show False unfolding least_power_def
using not_less_Least by auto
qed
lemma least_power_welldefined:
assumes "permutation p" and "y \<in> {(p ^^ k) x | k. k \<ge> 0}"
shows "least_power p x = least_power p y"
proof -
have aux_lemma: "\<And>z. least_power p z = least_power p (p z)"
proof -
fix z
have "(p ^^ (least_power p z)) z = z"
by (metis assms(1) least_power_wellfounded)
hence "(p ^^ (least_power p z)) (p z) = (p z)"
by (metis funpow_swap1)
hence "least_power p z \<ge> least_power p (p z)"
by (metis assms(1) inc_induct le_SucE least_power_gt_zero lt_least_power nat_le_linear)
moreover have "(p ^^ (least_power p (p z))) (p z) = (p z)"
by (simp add: assms(1) least_power_wellfounded)
hence "(p ^^ (least_power p (p z))) z = z"
by (metis assms(1) funpow_swap1 permutation_permutes permutes_def)
hence "least_power p z \<le> least_power p (p z)"
by (metis assms(1) least_power_gt_zero less_imp_Suc_add lt_least_power not_less_eq_eq)
ultimately show "least_power p z = least_power p (p z)" by simp
qed
obtain k where "k \<ge> 0" "y = (p ^^ k) x"
using assms(2) by blast
thus ?thesis
proof (induction k arbitrary: x y)
case 0 thus ?case by simp
next
case (Suc k)
have "least_power p ((p ^^ k) x) = least_power p x"
using Suc.IH by fastforce
thus ?case using aux_lemma
using Suc.prems(2) by auto
qed
qed
theorem cycle_of_permutation:
assumes "permutation p"
shows "cycle (support p x)"
proof (rule ccontr)
assume "\<not> cycle (support p x)"
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"
using atLeast_upt by (simp add: distinct_conv_nth)
then obtain i j where ij: "0 \<le> i" "i < j" "j < least_power p x"
and "(p ^^ i) x = (p ^^ j) x"
by (metis atLeast_upt le0 le_eq_less_or_eq lessThan_iff not_less set_upt)
hence "(p ^^ i) x = (p ^^ i) ((p ^^ (j - i)) x)"
by (metis add_diff_inverse_nat funpow_add not_less_iff_gr_or_eq o_apply)
hence "(p ^^ (j - i)) x = x"
using exp_of_permutation1 assms by (metis bij_pointE permutation_permutes permutes_bij)
moreover have "0 \<le> j - i \<and> j - i < least_power p x"
by (simp add: ij(3) less_imp_diff_less)
hence "(p ^^ (j - i)) x \<noteq> x" using lt_least_power ij
by (metis diff_le_self lessE less_imp_diff_less less_imp_le zero_less_diff)
ultimately show False by simp
qed
subsection\<open>Decomposition on Cycles\<close>
text\<open>We show that a permutation can be decomposed on cycles\<close>
subsubsection\<open>Preliminaries\<close>
lemma support_set:
assumes "permutation p"
shows "set (support p x) = {(p ^^ k) x | k. k \<ge> 0}"
proof -
have "{(p ^^ k) x | k. k \<ge> 0} = {(p ^^ k) x | k. 0 \<le> k \<and> k < (least_power p x)}" (is "?A = ?B")
proof
show "?B \<subseteq> ?A" by blast
next
show "?A \<subseteq> ?B"
proof
fix y assume "y \<in> ?A"
then obtain k :: "nat" where k: "k \<ge> 0" "(p ^^ k) x = y" by blast
hence "k = (least_power p x) * (k div (least_power p x)) + (k mod (least_power p x))" by simp
hence "y = (p ^^ ((least_power p x) * (k div (least_power p x)) + (k mod (least_power p x)))) x"
using k by auto
hence " y = (p ^^ (k mod (least_power p x))) x"
using power_prop[OF least_power_wellfounded[OF assms, of x], of "k div (least_power p x)"]
by (metis add.commute funpow_add o_apply)
moreover have "k mod (least_power p x) < least_power p x"
using k mod_less_divisor[of "least_power p x" k, OF least_power_gt_zero[OF assms]] by simp
ultimately show "y \<in> ?B"
by blast
qed
qed
moreover have "{(p ^^ k) x | k. 0 \<le> k \<and> k < (least_power p x)} = set (support p x)" (is "?B = ?C")
proof
show "?B \<subseteq> ?C"
proof
fix y assume "y \<in> {(p ^^ k) x | k. 0 \<le> k \<and> k < (least_power p x)}"
then obtain k where "k \<ge> 0" "k < (least_power p x)" "y = (p ^^ k) x" by blast
thus "y \<in> ?C" by auto
qed
next
show "?C \<subseteq> ?B"
proof
fix y assume "y \<in> ?C"
then obtain k where "k \<ge> 0" "k < (least_power p x)" "(support p x) ! k = y" by auto
thus "y \<in> ?B" by auto
qed
qed
ultimately show ?thesis by simp
qed
lemma disjoint_support:
assumes "p permutes S" "finite S"
shows "disjoint {{(p ^^ k) x | k. k \<ge> 0} | x. x \<in> S}" (is "disjoint ?A")
proof (rule disjointI)
{ fix a b assume "a \<in> ?A" "b \<in> ?A" "a \<inter> b \<noteq> {}"
then obtain x y where x: "x \<in> S" "a = {(p ^^ k) x | k. k \<ge> 0}"
and y: "y \<in> S" "b = {(p ^^ k) y | k. k \<ge> 0}" by blast
assume "a \<inter> b \<noteq> {}"
then obtain z kx ky where z: "kx \<ge> 0" "ky \<ge> 0" "z = (p ^^ kx) x" "z = (p ^^ ky) y"
using x(2) y(2) by blast
have "a \<subseteq> b"
proof
fix w assume "w \<in> a"
then obtain k where k: "k \<ge> 0" "w = (p ^^ k) x" using x by blast
define l where "l = (kx div (least_power p w)) + 1"
hence l: "l * (least_power p w) > kx"
using least_power_gt_zero assms One_nat_def add.right_neutral add_Suc_right
mult.commute permutation_permutes
by (metis dividend_less_times_div mult_Suc_right)
have "w = (p ^^ (l * (least_power p w))) w"
by (metis assms least_power_wellfounded mult.commute permutation_permutes power_prop)
also have "... = (p ^^ (l * (least_power p w) + k)) x"
using k by (simp add: funpow_add)
also have " ... = (p ^^ (l * (least_power p w) + k - kx + kx)) x"
using l by auto
also have " ... = (p ^^ (l * (least_power p w) + k - kx)) ((p ^^ kx) x)"
by (simp add: funpow_add)
also have " ... = (p ^^ (l * (least_power p w) + k - kx)) ((p ^^ ky) y)" using z
by simp
finally have "w = (p ^^ (l * (least_power p w) + k - kx + ky)) y"
by (simp add: funpow_add)
thus "w \<in> b" using y by blast
qed } note aux_lemma = this
fix a b assume ab: "a \<in> ?A" "b \<in> ?A" "a \<noteq> b"
show "a \<inter> b = {}"
proof (rule ccontr)
assume "a \<inter> b \<noteq> {}" thus False using aux_lemma ab
by (metis (no_types, lifting) inf.absorb2 inf.orderE)
qed
qed
lemma support_coverture:
assumes "p permutes S" "finite S"
shows "\<Union>{{(p ^^ k) x | k. k \<ge> 0} | x. x \<in> S} = S"
proof
show "\<Union>{{(p ^^ k) x |k. 0 \<le> k} |x. x \<in> S} \<subseteq> S"
proof
fix y assume "y \<in> \<Union>{{(p ^^ k) x |k. 0 \<le> k} |x. x \<in> S}"
then obtain x k where x: "x \<in> S" and k: "k \<ge> 0" and y: "y = (p ^^ k) x" by blast
have "(p ^^ k) x \<in> S"
proof (induction k)
case 0 thus ?case using x by simp
next
case (Suc k) thus ?case using assms
by (simp add: permutes_in_image)
qed
thus "y \<in> S" using y by simp
qed
next
show "S \<subseteq> \<Union>{{(p ^^ k) x |k. 0 \<le> k} |x. x \<in> S}"
proof
fix x assume x: "x \<in> S"
hence "x \<in> {(p ^^ k) x |k. 0 \<le> k}"
by (metis (mono_tags, lifting) CollectI funpow_0 le_numeral_extra(3))
thus "x \<in> \<Union>{{(p ^^ k) x |k. 0 \<le> k} |x. x \<in> S}" using x by blast
qed
qed
theorem cycle_restrict:
assumes "permutation p" "y \<in> set (support p x)"
shows "p y = (cycle_of_list (support p x)) y"
proof -
have "\<And> i. \<lbrakk> 0 \<le> i; i < length (support p x) - 1 \<rbrakk> \<Longrightarrow>
p ((support p x) ! i) = (support p x) ! (i + 1)"
proof -
fix i assume i: "0 \<le> i" "i < length (support p x) - 1"
hence "p ((support p x) ! i) = p ((p ^^ i) x)" by simp
also have " ... = (p ^^ (i + 1)) x" by simp
also have " ... = (support p x) ! (i + 1)"
using i by simp
finally show "p ((support p x) ! i) = (support p x) ! (i + 1)" .
qed
hence 1: "map p (butlast (support p x)) = tl (support p x)"
using nth_butlast [where 'a='a] nth_tl [where 'a='a]
nth_equalityI[of "map p (butlast (support p x))" "tl (support p x)"] by force
have "p ((support p x) ! (length (support p x) - 1)) = p ((p ^^ (length (support p x) - 1)) x)"
using assms(2) by auto
also have " ... = (p ^^ (length (support p x))) x"
by (metis (mono_tags, lifting) Suc_pred' assms(2) funpow_Suc_right
funpow_swap1 length_pos_if_in_set o_apply)
also have " ... = x"
by (simp add: assms(1) least_power_wellfounded)
also have " ... = (support p x) ! 0"
by (simp add: assms(1) least_power_gt_zero)
finally have "p ((support p x) ! (length (support p x) - 1)) = (support p x) ! 0" .
hence 2: "p (last (support p x)) = hd (support p x)"
by (metis assms(2) hd_conv_nth last_conv_nth length_greater_0_conv length_pos_if_in_set)
have "map p (support p x) = (tl (support p x)) @ [hd (support p x)]" using 1 2
by (metis (no_types, lifting) assms(2) last_map length_greater_0_conv
length_pos_if_in_set list.map_disc_iff map_butlast snoc_eq_iff_butlast)
hence "map p (support p x) = rotate1 (support p x)"
by (metis assms(2) length_greater_0_conv length_pos_if_in_set rotate1_hd_tl)
moreover have "map (cycle_of_list (support p x)) (support p x) = rotate1 (support p x)"
using cyclic_rotation[OF cycle_of_permutation[OF assms(1)], of 1 x] by simp
ultimately show ?thesis using assms(2)
using map_eq_conv by fastforce
qed
subsubsection\<open>Decomposition\<close>
inductive cycle_decomp :: "'a set \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> bool" where
empty: "cycle_decomp {} id" |
comp: "\<lbrakk> cycle_decomp I p; cycle cs; set cs \<inter> I = {} \<rbrakk> \<Longrightarrow>
cycle_decomp (set cs \<union> I) ((cycle_of_list cs) \<circ> p)"
lemma semidecomposition:
assumes "p permutes S" "finite S"
shows "(\<lambda>y. if y \<in> (S - set (support p x)) then p y else y) permutes (S - set (support p x))"
(is "?q permutes ?S'")
proof -
have "\<And>y. y \<notin> S \<Longrightarrow> p y = y"
by (meson assms permutes_not_in)
moreover have cycle_surj: "(cycle_of_list (support p x)) ` set (support p x) = set (support p x)"
using cycle_is_surj cycle_of_permutation assms permutation_permutes by metis
hence "\<And>y. y \<in> set (support p x) \<Longrightarrow> p y \<in> set (support p x)"
using cycle_restrict assms permutation_permutes by (metis imageI)
ultimately
have 1: "\<And>y. y \<notin> ?S' \<Longrightarrow> p y \<notin> ?S'" by auto
have 2: "\<And>y. y \<in> ?S' \<Longrightarrow> p y \<in> ?S'"
proof -
fix y assume y: "y \<in> ?S'" show "p y \<in> ?S'"
proof (rule ccontr)
assume "p y \<notin> ?S'" hence "p y \<in> set (support p x)"
using assms(1) permutes_in_image y by fastforce
then obtain y' where y': "y' \<in> set (support p x)" "(cycle_of_list (support p x)) y' = p y"
using cycle_surj by (metis (mono_tags, lifting) imageE)
hence "p y' = p y"
using cycle_restrict assms permutation_permutes by metis
hence "y = y'" by (metis assms(1) permutes_def)
thus False using y y' by blast
qed
qed
have "p ` ?S' = ?S'"
proof -
have "\<And> y. y \<in> ?S' \<Longrightarrow> \<exists>!x. p x = y"
by (metis assms(1) permutes_def)
hence "\<And> y. y \<in> ?S' \<Longrightarrow> \<exists>x \<in> ?S'. p x = y" using 1 by metis
thus ?thesis using 2 by blast
qed
hence "bij_betw p ?S' ?S'"
by (metis DiffD1 assms(1) bij_betw_subset permutes_imp_bij subsetI)
hence "bij_betw ?q ?S' ?S'"
by (rule rev_iffD1 [OF _ bij_betw_cong]) auto
moreover have "\<And>y. y \<notin> ?S' \<Longrightarrow> ?q y = y" by auto
ultimately show ?thesis
using bij_imp_permutes by blast
qed
lemma cycle_decomposition_aux:
assumes "p permutes S" "finite S" "card S = k"
shows "cycle_decomp S p" using assms
proof(induct arbitrary: S p rule: less_induct)
case (less x) thus ?case
proof (cases "S = {}")
case True thus ?thesis
by (metis empty less.prems(1) permutes_empty)
next
case False
then obtain x where x: "x \<in> S" by blast
define S' :: "'a set" where S': "S' = S - set (support p x)"
define q :: "'a \<Rightarrow> 'a" where q: "q = (\<lambda>x. if x \<in> S' then p x else x)"
hence q_permutes: "q permutes S'"
using semidecomposition[OF less.prems(1-2), of x] S' q by blast
moreover have "x \<in> set (support p x)"
by (metis (no_types, lifting) add.left_neutral diff_zero funpow_0 in_set_conv_nth least_power_gt_zero
length_map length_upt less.prems(1) less.prems(2) nth_map_upt permutation_permutes)
hence "card S' < card S"
by (metis Diff_iff S' \<open>x \<in> S\<close> card_seteq leI less.prems(2) subsetI)
ultimately have "cycle_decomp S' q"
using S' less.hyps less.prems(2) less.prems(3) by blast
moreover have "p = (cycle_of_list (support p x)) \<circ> q"
proof
fix y show "p y = ((cycle_of_list (support p x)) \<circ> q) y"
proof (cases)
assume y: "y \<in> set (support p x)" hence "y \<notin> S'" using S' by simp
hence "q y = y" using q by simp
thus ?thesis
using comp_apply cycle_restrict less.prems permutation_permutes y by fastforce
next
assume y: "y \<notin> set (support p x)" thus ?thesis
proof (cases)
assume "y \<in> S'"
hence "q y \<in> S'" using q_permutes
by (simp add: permutes_in_image)
hence "q y \<notin> set (support p x)"
using S' by blast
hence "(cycle_of_list (support p x)) (q y) = (q y)"
by (metis cycle_of_permutation id_outside_supp less.prems(1-2) permutation_permutes)
thus ?thesis by (simp add: \<open>y \<in> S'\<close> q)
next
assume "y \<notin> S'" hence "y \<notin> S" using y S' by blast
hence "(cycle_of_list (support p x) \<circ> q) y = (cycle_of_list (support p x)) y"
by (simp add: \<open>y \<notin> S'\<close> q)
also have " ... = y"
by (metis cycle_of_permutation id_outside_supp less.prems(1-2) permutation_permutes y)
also have " ... = p y"
by (metis \<open>y \<notin> S\<close> less.prems(1) permutes_def)
finally show ?thesis by simp
qed
qed
qed
moreover have "cycle (support p x)"
using cycle_of_permutation less.prems permutation_permutes by fastforce
moreover have "set (support p x) \<inter> S' = {}" using S' by simp
moreover have "set (support p x) \<subseteq> S"
using support_coverture[OF less.prems(1-2)] support_set[of p x] x
permutation_permutes[of p] less.prems(1-2) by blast
hence "S = set (support p x) \<union> S'" using S' by blast
ultimately show ?thesis using comp[of S' q "support p x"] by auto
qed
qed
theorem cycle_decomposition:
assumes "p permutes S" "finite S"
shows "cycle_decomp S p"
using assms cycle_decomposition_aux by blast
end