(* Author: Florian Haftmann, TU Muenchen *) section ‹Fragments on permuations› theory Perm_Fragments imports "HOL-Library.Perm" "HOL-Library.Dlist" begin unbundle permutation_syntax text ‹On cycles› lemma cycle_prod_list: "⟨a # as⟩ = prod_list (map (λb. ⟨a↔b⟩) (rev as))" by (induct as) simp_all lemma cycle_append [simp]: "⟨a # as @ bs⟩ = ⟨a # bs⟩ * ⟨a # as⟩" proof (induct as rule: cycle.induct) case (3 b c as) then have "⟨a # (b # as) @ bs⟩ = ⟨a # bs⟩ * ⟨a # b # as⟩" by simp then have "⟨a # as @ bs⟩ * ⟨a↔b⟩ = ⟨a # bs⟩ * ⟨a # as⟩ * ⟨a↔b⟩" by (simp add: ac_simps) then have "⟨a # as @ bs⟩ * ⟨a↔b⟩ * ⟨a↔b⟩ = ⟨a # bs⟩ * ⟨a # as⟩ * ⟨a↔b⟩ * ⟨a↔b⟩" by simp then have "⟨a # as @ bs⟩ = ⟨a # bs⟩ * ⟨a # as⟩" by (simp add: ac_simps) then show "⟨a # (b # c # as) @ bs⟩ = ⟨a # bs⟩ * ⟨a # b # c # as⟩" by (simp add: ac_simps) qed simp_all lemma affected_cycle: "affected ⟨as⟩ ⊆ set as" proof (induct as rule: cycle.induct) case (3 a b as) from affected_times have "affected (⟨a # as⟩ * ⟨a↔b⟩) ⊆ affected ⟨a # as⟩ ∪ affected ⟨a↔b⟩" . moreover from 3 have "affected (⟨a # as⟩) ⊆ insert a (set as)" by simp moreover have "affected ⟨a↔b⟩ ⊆ {a, b}" by (cases "a = b") (simp_all add: affected_swap) ultimately have "affected (⟨a # as⟩ * ⟨a↔b⟩) ⊆ insert a (insert b (set as))" by blast then show ?case by auto qed simp_all lemma orbit_cycle_non_elem: assumes "a ∉ set as" shows "orbit ⟨as⟩ a = {a}" unfolding not_in_affected_iff_orbit_eq_singleton [symmetric] using assms affected_cycle [of as] by blast lemma inverse_cycle: assumes "distinct as" shows "inverse ⟨as⟩ = ⟨rev as⟩" using assms proof (induct as rule: cycle.induct) case (3 a b as) then have *: "inverse ⟨a # as⟩ = ⟨rev (a # as)⟩" and distinct: "distinct (a # b # as)" by simp_all show " inverse ⟨a # b # as⟩ = ⟨rev (a # b # as)⟩" proof (cases as rule: rev_cases) case Nil with * show ?thesis by (simp add: swap_sym) next case (snoc cs c) with distinct have "distinct (a # b # cs @ [c])" by simp then have **: "⟨a↔b⟩ * ⟨c↔a⟩ = ⟨c↔a⟩ * ⟨c↔b⟩" by transfer (auto simp add: comp_def Fun.swap_def) with snoc * show ?thesis by (simp add: mult.assoc [symmetric]) qed qed simp_all lemma order_cycle_non_elem: assumes "a ∉ set as" shows "order ⟨as⟩ a = 1" proof - from assms have "orbit ⟨as⟩ a = {a}" by (rule orbit_cycle_non_elem) then have "card (orbit ⟨as⟩ a) = card {a}" by simp then show ?thesis by simp qed lemma orbit_cycle_elem: assumes "distinct as" and "a ∈ set as" shows "orbit ⟨as⟩ a = set as" oops ― ‹(we need rotation here› lemma order_cycle_elem: assumes "distinct as" and "a ∈ set as" shows "order ⟨as⟩ a = length as" oops text ‹Adding fixpoints› definition fixate :: "'a ⇒ 'a perm ⇒ 'a perm" where "fixate a f = (if a ∈ affected f then f * ⟨apply (inverse f) a↔a⟩ else f)" lemma affected_fixate_trivial: assumes "a ∉ affected f" shows "affected (fixate a f) = affected f" using assms by (simp add: fixate_def) lemma affected_fixate_binary_circle: assumes "order f a = 2" shows "affected (fixate a f) = affected f - {a, apply f a}" (is "?A = ?B") proof (rule set_eqI) interpret bijection "apply f" by standard simp fix b from assms order_greater_eq_two_iff [of f a] have "a ∈ affected f" by simp moreover have "apply (f ^ 2) a = a" by (simp add: assms [symmetric]) ultimately show "b ∈ ?A ⟷ b ∈ ?B" by (cases "b ∈ {a, apply (inverse f) a}") (auto simp add: in_affected power2_eq_square apply_inverse apply_times fixate_def) qed lemma affected_fixate_no_binary_circle: assumes "order f a > 2" shows "affected (fixate a f) = affected f - {a}" (is "?A = ?B") proof (rule set_eqI) interpret bijection "apply f" by standard simp fix b from assms order_greater_eq_two_iff [of f a] have "a ∈ affected f" by simp moreover from assms have "apply f (apply f a) ≠ a" using apply_power_eq_iff [of f 2 a 0] by (simp add: power2_eq_square apply_times) ultimately show "b ∈ ?A ⟷ b ∈ ?B" by (cases "b ∈ {a, apply (inverse f) a}") (auto simp add: in_affected apply_inverse apply_times fixate_def) qed lemma affected_fixate: "affected (fixate a f) ⊆ affected f - {a}" proof - have "a ∉ affected f ∨ order f a = 2 ∨ order f a > 2" by (auto simp add: not_less dest: affected_order_greater_eq_two) then consider "a ∉ affected f" | "order f a = 2" | "order f a > 2" by blast then show ?thesis apply cases using affected_fixate_trivial [of a f] affected_fixate_binary_circle [of f a] affected_fixate_no_binary_circle [of f a] by auto qed lemma orbit_fixate_self [simp]: "orbit (fixate a f) a = {a}" proof - have "apply (f * inverse f) a = a" by simp then have "apply f (apply (inverse f) a) = a" by (simp only: apply_times comp_apply) then show ?thesis by (simp add: fixate_def not_in_affected_iff_orbit_eq_singleton [symmetric] in_affected apply_times) qed lemma order_fixate_self [simp]: "order (fixate a f) a = 1" proof - have "card (orbit (fixate a f) a) = card {a}" by simp then show ?thesis by (simp only: card_orbit_eq) simp qed lemma assumes "b ∉ orbit f a" shows "orbit (fixate b f) a = orbit f a" oops lemma assumes "b ∈ orbit f a" and "b ≠ a" shows "orbit (fixate b f) a = orbit f a - {b}" oops text ‹Distilling cycles from permutations› inductive_set orbits :: "'a perm ⇒ 'a set set" for f where in_orbitsI: "a ∈ affected f ⟹ orbit f a ∈ orbits f" lemma orbits_unfold: "orbits f = orbit f ` affected f" by (auto intro: in_orbitsI elim: orbits.cases) lemma in_orbit_affected: assumes "b ∈ orbit f a" assumes "a ∈ affected f" shows "b ∈ affected f" proof (cases "a = b") case True with assms show ?thesis by simp next case False with assms have "{a, b} ⊆ orbit f a" by auto also from assms have "orbit f a ⊆ affected f" by (blast intro!: orbit_subset_eq_affected) finally show ?thesis by simp qed lemma Union_orbits [simp]: "⋃orbits f = affected f" by (auto simp add: orbits.simps intro: in_orbitsI in_orbit_affected) lemma finite_orbits [simp]: "finite (orbits f)" by (simp add: orbits_unfold) lemma card_in_orbits: assumes "A ∈ orbits f" shows "card A ≥ 2" using assms by cases (auto dest: affected_order_greater_eq_two) lemma disjoint_orbits: assumes "A ∈ orbits f" and "B ∈ orbits f" and "A ≠ B" shows "A ∩ B = {}" using ‹A ∈ orbits f› apply cases using ‹B ∈ orbits f› apply cases using ‹A ≠ B› apply (simp_all add: orbit_disjoint) done definition trace :: "'a ⇒ 'a perm ⇒ 'a list" where "trace a f = map (λn. apply (f ^ n) a) [0..<order f a]" lemma set_trace_eq [simp]: "set (trace a f) = orbit f a" by (auto simp add: trace_def orbit_unfold_image) definition seeds :: "'a perm ⇒ 'a::linorder list" where "seeds f = sorted_list_of_set (Min ` orbits f)" definition cycles :: "'a perm ⇒ 'a::linorder list list" where "cycles f = map (λa. trace a f) (seeds f)" lemma (in comm_monoid_list_set) sorted_list_of_set: assumes "finite A" shows "list.F (map h (sorted_list_of_set A)) = set.F h A" proof - from distinct_sorted_list_of_set have "set.F h (set (sorted_list_of_set A)) = list.F (map h (sorted_list_of_set A))" by (rule distinct_set_conv_list) with ‹finite A› show ?thesis by (simp) qed text ‹Misc› primrec subtract :: "'a list ⇒ 'a list ⇒ 'a list" where "subtract [] ys = ys" | "subtract (x # xs) ys = subtract xs (removeAll x ys)" lemma length_subtract_less_eq [simp]: "length (subtract xs ys) ≤ length ys" proof (induct xs arbitrary: ys) case Nil then show ?case by simp next case (Cons x xs) then have "length (subtract xs (removeAll x ys)) ≤ length (removeAll x ys)" . also have "length (removeAll x ys) ≤ length ys" by simp finally show ?case by simp qed end