# Theory Perm_Fragments

theory Perm_Fragments
imports Perm Dlist
(* 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⟩"
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⟩"
then show "⟨a # (b # c # as) @ bs⟩ =
⟨a # bs⟩ * ⟨a # b # c # as⟩"
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
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
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

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"
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]
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)"

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
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