(* Author: Paulo Emílio de Vilhena *) theory Cycles imports "HOL-Library.FuncSet" Permutations begin section ‹Cycles› subsection ‹Definitions› abbreviation cycle :: "'a list ⇒ bool" where "cycle cs ≡ distinct cs" fun cycle_of_list :: "'a list ⇒ 'a ⇒ 'a" where "cycle_of_list (i # j # cs) = transpose i j ∘ cycle_of_list (j # cs)" | "cycle_of_list cs = id" subsection ‹Basic Properties› text ‹We start proving that the function derived from a cycle rotates its support list.› lemma id_outside_supp: assumes "x ∉ set cs" shows "(cycle_of_list cs) x = x" using assms by (induct cs rule: cycle_of_list.induct) (simp_all) lemma permutation_of_cycle: "permutation (cycle_of_list cs)" proof (induct cs rule: cycle_of_list.induct) case 1 thus ?case using permutation_compose[OF permutation_swap_id] unfolding comp_apply by simp qed simp_all lemma cycle_permutes: "(cycle_of_list cs) permutes (set cs)" using permutation_bijective[OF permutation_of_cycle] id_outside_supp[of _ cs] by (simp add: bij_iff permutes_def) 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) then have ‹i ∉ set cs› ‹j ∉ set cs› by auto then have ‹map (Transposition.transpose i j) cs = cs› by (auto intro: map_idI simp add: transpose_eq_iff) show ?case proof (cases) assume "cs = Nil" thus ?thesis by simp next assume "cs ≠ Nil" hence ge_two: "length (j # cs) ≥ 2" using not_less by auto have "map (cycle_of_list (i # j # cs)) (i # j # cs) = map (transpose i j) (map (cycle_of_list (j # cs)) (i # j # cs))" by simp also have " ... = map (transpose i j) (i # (rotate1 (j # cs)))" by (metis "1.IH" "1.prems" distinct.simps(2) id_outside_supp list.simps(9)) also have " ... = map (transpose i j) (i # (cs @ [j]))" by simp also have " ... = j # (map (transpose i j) cs) @ [i]" by simp also have " ... = j # cs @ [i]" using ‹map (Transposition.transpose i j) cs = cs› by simp also have " ... = rotate1 (i # j # cs)" by simp finally show ?thesis . qed qed simp_all } note cyclic_rotation' = this show ?thesis using cyclic_rotation' by (induct n) (auto, metis map_map rotate1_rotate_swap rotate_map) qed corollary cycle_is_surj: assumes "cycle cs" shows "(cycle_of_list cs) ` (set cs) = (set cs)" using cyclic_rotation[OF assms, of "Suc 0"] 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" unfolding cyclic_rotation[OF assms] by simp hence "((cycle_of_list cs) ^^ (length cs)) i = i" if "i ∈ set cs" for i using that map_eq_conv by fastforce moreover have "((cycle_of_list cs) ^^ n) i = i" if "i ∉ set cs" for i n using id_outside_supp[OF that] by (induct n) (simp_all) ultimately show ?thesis by fastforce qed corollary cycle_of_list_rotate_independent: assumes "cycle cs" shows "(cycle_of_list cs) = (cycle_of_list (rotate n cs))" proof - { fix cs :: "'a list" assume cs: "cycle cs" have "(cycle_of_list cs) = (cycle_of_list (rotate1 cs))" proof - from cs have rotate1_cs: "cycle (rotate1 cs)" by simp hence "map (cycle_of_list (rotate1 cs)) (rotate1 cs) = (rotate 2 cs)" using cyclic_rotation[OF rotate1_cs, of 1] by (simp add: numeral_2_eq_2) moreover have "map (cycle_of_list cs) (rotate1 cs) = (rotate 2 cs)" using cyclic_rotation[OF cs] by (metis One_nat_def Suc_1 funpow.simps(2) id_apply map_map rotate0 rotate_Suc) ultimately have "(cycle_of_list cs) i = (cycle_of_list (rotate1 cs)) i" if "i ∈ set cs" for i using that map_eq_conv unfolding sym[OF set_rotate1[of cs]] by fastforce moreover have "(cycle_of_list cs) i = (cycle_of_list (rotate1 cs)) i" if "i ∉ set cs" for i using that by (simp add: id_outside_supp) ultimately show "(cycle_of_list cs) = (cycle_of_list (rotate1 cs))" by blast qed } note rotate1_lemma = this show ?thesis using rotate1_lemma[of "rotate n cs"] by (induct n) (auto, metis assms distinct_rotate rotate1_lemma) qed subsection‹Conjugation of cycles› lemma conjugation_of_cycle: assumes "cycle cs" and "bij p" shows "p ∘ (cycle_of_list cs) ∘ (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 ∘ cycle_of_list (i # j # cs) ∘ inv p = (p ∘ (transpose i j) ∘ inv p) ∘ (p ∘ cycle_of_list (j # cs) ∘ inv p)" by (simp add: assms(2) bij_is_inj fun.map_comp) also have " ... = (transpose (p i) (p j)) ∘ (p ∘ cycle_of_list (j # cs) ∘ inv p)" using "1.prems"(2) by (simp add: bij_inv_eq_iff transpose_apply_commute fun_eq_iff bij_betw_inv_into_left) finally have "p ∘ cycle_of_list (i # j # cs) ∘ inv p = (transpose (p i) (p j)) ∘ (cycle_of_list (map p (j # cs)))" using "1.IH" "1.prems"(1) assms(2) by fastforce thus ?case by (simp add: fun_eq_iff) 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‹When Cycles Commute› lemma cycles_commute: assumes "cycle p" "cycle q" and "set p ∩ set q = {}" shows "(cycle_of_list p) ∘ (cycle_of_list q) = (cycle_of_list q) ∘ (cycle_of_list p)" proof { fix p :: "'a list" and q :: "'a list" and i :: "'a" assume A: "cycle p" "cycle q" "set p ∩ set q = {}" "i ∈ set p" "i ∉ set q" have "((cycle_of_list p) ∘ (cycle_of_list q)) i = ((cycle_of_list q) ∘ (cycle_of_list p)) i" proof - have "((cycle_of_list p) ∘ (cycle_of_list q)) i = (cycle_of_list p) i" using id_outside_supp[OF A(5)] by simp also have " ... = ((cycle_of_list q) ∘ (cycle_of_list p)) i" using id_outside_supp[of "(cycle_of_list p) i"] cycle_is_surj[OF A(1)] A(3,4) by fastforce finally show ?thesis . qed } note aui_lemma = this fix i consider "i ∈ set p" "i ∉ set q" | "i ∉ set p" "i ∈ set q" | "i ∉ set p" "i ∉ set q" using ‹set p ∩ set q = {}› by blast thus "((cycle_of_list p) ∘ (cycle_of_list q)) i = ((cycle_of_list q) ∘ (cycle_of_list p)) i" proof cases case 1 thus ?thesis using aui_lemma[OF assms] by simp next case 2 thus ?thesis using aui_lemma[OF assms(2,1)] assms(3) by (simp add: ac_simps) next case 3 thus ?thesis by (simp add: id_outside_supp) qed qed subsection ‹Cycles from Permutations› subsubsection ‹Exponentiation of permutations› text ‹Some important properties of permutations before defining how to extract its cycles.› lemma permutation_funpow: assumes "permutation p" shows "permutation (p ^^ n)" using assms by (induct n) (simp_all add: permutation_compose) lemma permutes_funpow: assumes "p permutes S" shows "(p ^^ n) permutes S" using assms by (induct n) (simp add: permutes_def, metis funpow_Suc_right permutes_compose) lemma funpow_diff: assumes "inj p" and "i ≤ j" "(p ^^ i) a = (p ^^ j) a" shows "(p ^^ (j - i)) a = a" proof - have "(p ^^ i) ((p ^^ (j - i)) a) = (p ^^ i) a" using assms(2-3) by (metis (no_types) add_diff_inverse_nat funpow_add not_le o_def) thus ?thesis unfolding inj_eq[OF inj_fn[OF assms(1)], of i] . qed lemma permutation_is_nilpotent: assumes "permutation p" obtains n where "(p ^^ n) = id" and "n > 0" proof - obtain S where "finite S" and "p permutes S" using assms unfolding permutation_permutes by blast hence "∃n. (p ^^ n) = id ∧ n > 0" proof (induct S arbitrary: p) case empty thus ?case using id_funpow[of 1] unfolding permutes_empty by blast next case (insert s S) have "(λn. (p ^^ n) s) ` UNIV ⊆ (insert s S)" using permutes_in_image[OF permutes_funpow[OF insert(4)], of _ s] by auto hence "¬ inj_on (λn. (p ^^ n) s) UNIV" using insert(1) infinite_iff_countable_subset unfolding sym[OF finite_insert, of S s] by metis then obtain i j where ij: "i < j" "(p ^^ i) s = (p ^^ j) s" unfolding inj_on_def by (metis nat_neq_iff) hence "(p ^^ (j - i)) s = s" using funpow_diff[OF permutes_inj[OF insert(4)]] le_eq_less_or_eq by blast hence "p ^^ (j - i) permutes S" using permutes_superset[OF permutes_funpow[OF insert(4), of "j - i"], of S] by auto then obtain n where n: "((p ^^ (j - i)) ^^ n) = id" "n > 0" using insert(3) by blast thus ?case using ij(1) nat_0_less_mult_iff zero_less_diff unfolding funpow_mult by metis qed thus thesis using that by blast qed lemma permutation_is_nilpotent': assumes "permutation p" obtains n where "(p ^^ n) = id" and "n > m" proof - obtain n where "(p ^^ n) = id" and "n > 0" using permutation_is_nilpotent[OF assms] by blast then obtain k where "n * k > m" by (metis dividend_less_times_div mult_Suc_right) from ‹(p ^^ n) = id› have "p ^^ (n * k) = id" by (induct k) (simp, metis funpow_mult id_funpow) with ‹n * k > m› show thesis using that by blast qed subsubsection ‹Extraction of cycles from permutations› definition least_power :: "('a ⇒ 'a) ⇒ 'a ⇒ nat" where "least_power f x = (LEAST n. (f ^^ n) x = x ∧ n > 0)" abbreviation support :: "('a ⇒ 'a) ⇒ 'a ⇒ 'a list" where "support p x ≡ map (λi. (p ^^ i) x) [0..< (least_power p x)]" lemma least_powerI: assumes "(f ^^ n) x = x" and "n > 0" shows "(f ^^ (least_power f x)) x = x" and "least_power f x > 0" using assms unfolding least_power_def by (metis (mono_tags, lifting) LeastI)+ lemma least_power_le: assumes "(f ^^ n) x = x" and "n > 0" shows "least_power f x ≤ n" using assms unfolding least_power_def by (simp add: Least_le) lemma least_power_of_permutation: assumes "permutation p" shows "(p ^^ (least_power p a)) a = a" and "least_power p a > 0" using permutation_is_nilpotent[OF assms] least_powerI by (metis id_apply)+ lemma least_power_gt_one: assumes "permutation p" and "p a ≠ a" shows "least_power p a > Suc 0" using least_power_of_permutation[OF assms(1)] assms(2) by (metis Suc_lessI funpow.simps(2) funpow_simps_right(1) o_id) lemma least_power_minimal: assumes "(p ^^ n) a = a" shows "(least_power p a) dvd n" proof (cases "n = 0", simp) let ?lpow = "least_power p" assume "n ≠ 0" then have "n > 0" by simp hence "(p ^^ (?lpow a)) a = a" and "least_power p a > 0" using assms unfolding least_power_def by (metis (mono_tags, lifting) LeastI)+ hence aux_lemma: "(p ^^ ((?lpow a) * k)) a = a" for k :: nat by (induct k) (simp_all add: funpow_add) have "(p ^^ (n mod ?lpow a)) ((p ^^ (n - (n mod ?lpow a))) a) = (p ^^ n) a" by (metis add_diff_inverse_nat funpow_add mod_less_eq_dividend not_less o_apply) with ‹(p ^^ n) a = a› have "(p ^^ (n mod ?lpow a)) a = a" using aux_lemma by (simp add: minus_mod_eq_mult_div) hence "?lpow a ≤ n mod ?lpow a" if "n mod ?lpow a > 0" using least_power_le[OF _ that, of p a] by simp with ‹least_power p a > 0› show "(least_power p a) dvd n" using mod_less_divisor not_le by blast qed lemma least_power_dvd: assumes "permutation p" shows "(least_power p a) dvd n ⟷ (p ^^ n) a = a" proof show "(p ^^ n) a = a ⟹ (least_power p a) dvd n" using least_power_minimal[of _ p] by simp next have "(p ^^ ((least_power p a) * k)) a = a" for k :: nat using least_power_of_permutation(1)[OF assms(1)] by (induct k) (simp_all add: funpow_add) thus "(least_power p a) dvd n ⟹ (p ^^ n) a = a" by blast qed theorem cycle_of_permutation: assumes "permutation p" shows "cycle (support p a)" proof - have "(least_power p a) dvd (j - i)" if "i ≤ j" "j < least_power p a" and "(p ^^ i) a = (p ^^ j) a" for i j using funpow_diff[OF bij_is_inj that(1,3)] assms by (simp add: permutation least_power_dvd) moreover have "i = j" if "i ≤ j" "j < least_power p a" and "(least_power p a) dvd (j - i)" for i j using that le_eq_less_or_eq nat_dvd_not_less by auto ultimately have "inj_on (λi. (p ^^ i) a) {..< (least_power p a)}" unfolding inj_on_def by (metis le_cases lessThan_iff) thus ?thesis by (simp add: atLeast_upt distinct_map) qed subsection ‹Decomposition on Cycles› text ‹We show that a permutation can be decomposed on cycles› subsubsection ‹Preliminaries› lemma support_set: assumes "permutation p" shows "set (support p a) = range (λi. (p ^^ i) a)" proof show "set (support p a) ⊆ range (λi. (p ^^ i) a)" by auto next show "range (λi. (p ^^ i) a) ⊆ set (support p a)" proof (auto) fix i have "(p ^^ i) a = (p ^^ (i mod (least_power p a))) ((p ^^ (i - (i mod (least_power p a)))) a)" by (metis add_diff_inverse_nat funpow_add mod_less_eq_dividend not_le o_apply) also have " ... = (p ^^ (i mod (least_power p a))) a" using least_power_dvd[OF assms] by (metis dvd_minus_mod) also have " ... ∈ (λi. (p ^^ i) a) ` {0..< (least_power p a)}" using least_power_of_permutation(2)[OF assms] by fastforce finally show "(p ^^ i) a ∈ (λi. (p ^^ i) a) ` {0..< (least_power p a)}" . qed qed lemma disjoint_support: assumes "permutation p" shows "disjoint (range (λa. set (support p a)))" (is "disjoint ?A") proof (rule disjointI) { fix i j a b assume "set (support p a) ∩ set (support p b) ≠ {}" have "set (support p a) ⊆ set (support p b)" unfolding support_set[OF assms] proof (auto) from ‹set (support p a) ∩ set (support p b) ≠ {}› obtain i j where ij: "(p ^^ i) a = (p ^^ j) b" by auto fix k have "(p ^^ k) a = (p ^^ (k + (least_power p a) * l)) a" for l using least_power_dvd[OF assms] by (induct l) (simp, metis dvd_triv_left funpow_add o_def) then obtain m where "m ≥ i" and "(p ^^ m) a = (p ^^ k) a" using least_power_of_permutation(2)[OF assms] by (metis dividend_less_times_div le_eq_less_or_eq mult_Suc_right trans_less_add2) hence "(p ^^ m) a = (p ^^ (m - i)) ((p ^^ i) a)" by (metis Nat.le_imp_diff_is_add funpow_add o_apply) with ‹(p ^^ m) a = (p ^^ k) a› have "(p ^^ k) a = (p ^^ ((m - i) + j)) b" unfolding ij by (simp add: funpow_add) thus "(p ^^ k) a ∈ range (λi. (p ^^ i) b)" by blast qed } note aux_lemma = this fix supp_a supp_b assume "supp_a ∈ ?A" and "supp_b ∈ ?A" then obtain a b where a: "supp_a = set (support p a)" and b: "supp_b = set (support p b)" by auto assume "supp_a ≠ supp_b" thus "supp_a ∩ supp_b = {}" using aux_lemma unfolding a b by blast qed lemma disjoint_support': assumes "permutation p" shows "set (support p a) ∩ set (support p b) = {} ⟷ a ∉ set (support p b)" proof - have "a ∈ set (support p a)" using least_power_of_permutation(2)[OF assms] by force show ?thesis proof assume "set (support p a) ∩ set (support p b) = {}" with ‹a ∈ set (support p a)› show "a ∉ set (support p b)" by blast next assume "a ∉ set (support p b)" show "set (support p a) ∩ set (support p b) = {}" proof (rule ccontr) assume "set (support p a) ∩ set (support p b) ≠ {}" hence "set (support p a) = set (support p b)" using disjoint_support[OF assms] by (meson UNIV_I disjoint_def image_iff) with ‹a ∈ set (support p a)› and ‹a ∉ set (support p b)› show False by simp qed qed qed lemma support_coverture: assumes "permutation p" shows "⋃ { set (support p a) | a. p a ≠ a } = { a. p a ≠ a }" proof show "{ a. p a ≠ a } ⊆ ⋃ { set (support p a) | a. p a ≠ a }" proof fix a assume "a ∈ { a. p a ≠ a }" have "a ∈ set (support p a)" using least_power_of_permutation(2)[OF assms, of a] by force with ‹a ∈ { a. p a ≠ a }› show "a ∈ ⋃ { set (support p a) | a. p a ≠ a }" by blast qed next show "⋃ { set (support p a) | a. p a ≠ a } ⊆ { a. p a ≠ a }" proof fix b assume "b ∈ ⋃ { set (support p a) | a. p a ≠ a }" then obtain a i where "p a ≠ a" and "(p ^^ i) a = b" by auto have "p a = a" if "(p ^^ i) a = (p ^^ Suc i) a" using funpow_diff[OF bij_is_inj _ that] assms unfolding permutation by simp with ‹p a ≠ a› and ‹(p ^^ i) a = b› show "b ∈ { a. p a ≠ a }" by auto qed qed theorem cycle_restrict: assumes "permutation p" and "b ∈ set (support p a)" shows "p b = (cycle_of_list (support p a)) b" proof - note least_power_props [simp] = least_power_of_permutation[OF assms(1)] have "map (cycle_of_list (support p a)) (support p a) = rotate1 (support p a)" using cyclic_rotation[OF cycle_of_permutation[OF assms(1)], of 1 a] by simp hence "map (cycle_of_list (support p a)) (support p a) = tl (support p a) @ [ a ]" by (simp add: hd_map rotate1_hd_tl) also have " ... = map p (support p a)" proof (rule nth_equalityI, auto) fix i assume "i < least_power p a" show "(tl (support p a) @ [a]) ! i = p ((p ^^ i) a)" proof (cases) assume i: "i = least_power p a - 1" hence "(tl (support p a) @ [ a ]) ! i = a" by (metis (no_types, lifting) diff_zero length_map length_tl length_upt nth_append_length) also have " ... = p ((p ^^ i) a)" by (metis (mono_tags, opaque_lifting) least_power_props i Suc_diff_1 funpow_simps_right(2) funpow_swap1 o_apply) finally show ?thesis . next assume "i ≠ least_power p a - 1" with ‹i < least_power p a› have "i < least_power p a - 1" by simp hence "(tl (support p a) @ [ a ]) ! i = (p ^^ (Suc i)) a" by (metis One_nat_def Suc_eq_plus1 add.commute length_map length_upt map_tl nth_append nth_map_upt tl_upt) thus ?thesis by simp qed qed finally have "map (cycle_of_list (support p a)) (support p a) = map p (support p a)" . thus ?thesis using assms(2) by auto qed subsubsection‹Decomposition› inductive cycle_decomp :: "'a set ⇒ ('a ⇒ 'a) ⇒ bool" where empty: "cycle_decomp {} id" | comp: "⟦ cycle_decomp I p; cycle cs; set cs ∩ I = {} ⟧ ⟹ cycle_decomp (set cs ∪ I) ((cycle_of_list cs) ∘ p)" lemma semidecomposition: assumes "p permutes S" and "finite S" shows "(λy. if y ∈ (S - set (support p a)) then p y else y) permutes (S - set (support p a))" proof (rule bij_imp_permutes) show "(if b ∈ (S - set (support p a)) then p b else b) = b" if "b ∉ S - set (support p a)" for b using that by auto next have is_permutation: "permutation p" using assms unfolding permutation_permutes by blast let ?q = "λy. if y ∈ (S - set (support p a)) then p y else y" show "bij_betw ?q (S - set (support p a)) (S - set (support p a))" proof (rule bij_betw_imageI) show "inj_on ?q (S - set (support p a))" using permutes_inj[OF assms(1)] unfolding inj_on_def by auto next have aux_lemma: "set (support p s) ⊆ (S - set (support p a))" if "s ∈ S - set (support p a)" for s proof - have "(p ^^ i) s ∈ S" for i using that unfolding permutes_in_image[OF permutes_funpow[OF assms(1)]] by simp thus ?thesis using that disjoint_support'[OF is_permutation, of s a] by auto qed have "(p ^^ 1) s ∈ set (support p s)" for s unfolding support_set[OF is_permutation] by blast hence "p s ∈ set (support p s)" for s by simp hence "p ` (S - set (support p a)) ⊆ S - set (support p a)" using aux_lemma by blast moreover have "(p ^^ ((least_power p s) - 1)) s ∈ set (support p s)" for s unfolding support_set[OF is_permutation] by blast hence "∃s' ∈ set (support p s). p s' = s" for s using least_power_of_permutation[OF is_permutation] by (metis Suc_diff_1 funpow.simps(2) o_apply) hence "S - set (support p a) ⊆ p ` (S - set (support p a))" using aux_lemma by (clarsimp simp add: image_iff) (metis image_subset_iff) ultimately show "?q ` (S - set (support p a)) = (S - set (support p a))" by auto qed qed theorem cycle_decomposition: assumes "p permutes S" and "finite S" shows "cycle_decomp S p" using assms proof(induct "card S" arbitrary: S p rule: less_induct) case less show ?case proof (cases) assume "S = {}" thus ?thesis using empty less(2) by auto next have is_permutation: "permutation p" using less(2-3) unfolding permutation_permutes by blast assume "S ≠ {}" then obtain s where "s ∈ S" by blast define q where "q = (λy. if y ∈ (S - set (support p s)) then p y else y)" have "(cycle_of_list (support p s) ∘ q) = p" proof fix a consider "a ∈ S - set (support p s)" | "a ∈ set (support p s)" | "a ∉ S" "a ∉ set (support p s)" by blast thus "((cycle_of_list (support p s) ∘ q)) a = p a" proof cases case 1 have "(p ^^ 1) a ∈ set (support p a)" unfolding support_set[OF is_permutation] by blast with ‹a ∈ S - set (support p s)› have "p a ∉ set (support p s)" using disjoint_support'[OF is_permutation, of a s] by auto with ‹a ∈ S - set (support p s)› show ?thesis using id_outside_supp[of _ "support p s"] unfolding q_def by simp next case 2 thus ?thesis using cycle_restrict[OF is_permutation] unfolding q_def by simp next case 3 thus ?thesis using id_outside_supp[OF 3(2)] less(2) permutes_not_in unfolding q_def by fastforce qed qed moreover from ‹s ∈ S› have "(p ^^ i) s ∈ S" for i unfolding permutes_in_image[OF permutes_funpow[OF less(2)]] . hence "set (support p s) ∪ (S - set (support p s)) = S" by auto moreover have "s ∈ set (support p s)" using least_power_of_permutation[OF is_permutation] by force with ‹s ∈ S› have "card (S - set (support p s)) < card S" using less(3) by (metis DiffE card_seteq linorder_not_le subsetI) hence "cycle_decomp (S - set (support p s)) q" using less(1)[OF _ semidecomposition[OF less(2-3)], of s] less(3) unfolding q_def by blast moreover show ?thesis using comp[OF calculation(3) cycle_of_permutation[OF is_permutation], of s] unfolding calculation(1-2) by blast qed qed end