Theory Perm_Fragments

(* Author: Florian Haftmann, TU Muenchen *)

section ‹Fragments on permuations›

theory Perm_Fragments
imports "HOL-Library.Dlist" "HOL-Combinatorics.Perm"
begin

text ‹On cycles›

context
  includes permutation_syntax
begin

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: fun_eq_iff transpose_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 * ⟨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)"

end


text ‹Misc›

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

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