Theory Permutations_2

theory Permutations_2
imports
  "HOL-Combinatorics.Permutations"
  Graph_Theory.Auxiliary
  Executable_Permutations
begin

section ‹More›

abbreviation funswapid :: "'a ⇒ 'a ⇒ 'a ⇒ 'a" (infix "⇌⇩F" 90) where
  "x ⇌⇩F y ≡ transpose x y"

lemma in_funswapid_image_iff: "x ∈ (a ⇌⇩F b) ` S ⟷ (a ⇌⇩F b) x ∈ S"
  by (fact in_transpose_image_iff)

lemma bij_swap_compose: "bij (x ⇌⇩F y ∘ f) ⟷ bij f"
  by (metis UNIV_I bij_betw_comp_iff2 bij_betw_id bij_swap_iff subsetI)

lemma bij_eq_iff:
  assumes "bij f" shows "f x = f y ⟷ x = y"
  using assms by (auto simp add: bij_iff) 

lemma swap_swap_id[simp]: "(x ⇌⇩F y) ((x ⇌⇩F y) z) = z"
  by (fact transpose_involutory)


section ‹Modifying Permutations›

definition perm_swap :: "'a ⇒ 'a ⇒ ('a ⇒ 'a) ⇒ ('a ⇒ 'a)" where
  "perm_swap x y f ≡ x ⇌⇩F y o f o x ⇌⇩F y"

definition perm_rem :: "'a ⇒ ('a ⇒ 'a) ⇒ ('a ⇒ 'a)" where
  "perm_rem x f ≡ if f x ≠ x then x ⇌⇩F f x o f else f"

text ‹
  An example:

  @{lemma "perm_rem (2 :: nat) (list_succ [1,2,3,4]) x = list_succ [1,3,4] x"
      by (auto simp: perm_rem_def Fun.swap_def list_succ_def)}
›
lemma perm_swap_id[simp]: "perm_swap a b id = id"
  by (auto simp: perm_swap_def)
  
lemma perm_rem_permutes:
  assumes "f permutes S ∪ {x}"
  shows "perm_rem x f permutes S"
  using assms by (auto simp: permutes_def perm_rem_def) (metis transpose_def)+

lemma perm_rem_same:
  assumes "bij f" "f y = y" shows "perm_rem x f y = f y"
  using assms by (auto simp: perm_rem_def bij_iff transpose_def)

lemma perm_rem_simps:
  assumes "bij f"
  shows
  "x = y ⟹ perm_rem x f y = x"
  "f y = x ⟹ perm_rem x f y = f x"
  "y ≠ x ⟹ f y ≠ x ⟹ perm_rem x f y = f y"
  using assms by (auto simp: perm_rem_def transpose_def bij_iff)

lemma bij_perm_rem[simp]: "bij (perm_rem x f) ⟷ bij f"
  by (simp add: perm_rem_def bij_swap_compose)

lemma perm_rem_conv: "⋀f x y. bij f ⟹ perm_rem x f y = (
    if x = y then x
    else if f y = x then f (f y)
    else f y)"
  by (auto simp: perm_rem_simps)

lemma perm_rem_commutes:
  assumes "bij f" shows "perm_rem a (perm_rem b f) = perm_rem b (perm_rem a f)"
proof -
  have bij_simp: "⋀x y. f x = f y ⟷ x = y"
    using assms by (auto simp: bij_iff)
  show ?thesis using assms by (auto simp: perm_rem_conv bij_simp fun_eq_iff)
qed

lemma perm_rem_id[simp]: "perm_rem a id = id"
  by (simp add: perm_rem_def)

lemma perm_swap_comp: "perm_swap a b (f ∘ g) x = perm_swap a b f (perm_swap a b g x)"
  by (auto simp: perm_swap_def)

lemma bij_perm_swap_iff[simp]: "bij (perm_swap a b f) ⟷ bij f"
  by (simp add: bij_swap_compose bij_swap_iff perm_swap_def)
  
lemma funpow_perm_swap: "perm_swap a b f ^^ n = perm_swap a b (f ^^ n)"
  by (induct n) (auto simp: perm_swap_def fun_eq_iff)

lemma orbit_perm_swap: "orbit (perm_swap a b f) x = (a ⇌⇩F b) ` orbit f ((a ⇌⇩F b) x)"
  by (auto simp: orbit_altdef funpow_perm_swap) (auto simp: perm_swap_def)

lemma has_dom_perm_swap: "has_dom (perm_swap a b f) S = has_dom f ((a ⇌⇩F b) ` S)"
  by (auto simp: has_dom_def perm_swap_def inj_image_mem_iff) (metis image_iff swap_swap_id)

lemma perm_restrict_dom_subset:
  assumes "has_dom f A" shows "perm_restrict f A = f"
proof -
  from assms have "⋀x. x ∉ A ⟹ f x = x" by (auto simp: has_dom_def)
  then show ?thesis by (auto simp: perm_restrict_def fun_eq_iff)
qed

lemma perm_swap_permutes2:
  assumes "f permutes ((x ⇌⇩F y) ` S)"
  shows "perm_swap x y f permutes S"
  using assms
  by (auto simp: perm_swap_def permutes_conv_has_dom has_dom_perm_swap [unfolded perm_swap_def] intro!: bij_comp)


section ‹Cyclic Permutations›

lemma cyclic_on_perm_swap:
  assumes "cyclic_on f S" shows "cyclic_on (perm_swap x y f) ((x ⇌⇩F y) ` S)"
  using assms by (rule cyclic_on_image) (auto simp: perm_swap_def)

lemma orbit_perm_rem:
  assumes "bij f" "x ≠ y" shows "orbit (perm_rem y f) x = orbit f x - {y}" (is "?L = ?R")
proof (intro set_eqI iffI)
  fix z assume "z ∈ ?L"
  then show "z ∈ ?R"
    using assms by induct (auto simp: perm_rem_conv bij_iff intro: orbit.intros)
next
  fix z assume A: "z ∈ ?R"

  { assume "z ∈ orbit f x"
    then have "(z ≠ y ⟶ z ∈ ?L) ∧ (z = y ⟶ f z ∈ ?L)"
    proof induct
      case base with assms show ?case by (auto intro: orbit_eqI(1) simp: perm_rem_conv)
    next
      case (step z) then show ?case
        using assms by (cases "y = z") (auto intro: orbit_eqI simp: perm_rem_conv)
    qed
  } with A show "z ∈ ?L" by auto
qed

lemma orbit_perm_rem_eq:
  assumes "bij f" shows "orbit (perm_rem y f) x = (if x = y then {y} else orbit f x - {y})"
  using assms by (simp add: orbit_eq_singleton_iff orbit_perm_rem perm_rem_simps)

lemma cyclic_on_perm_rem:
  assumes "cyclic_on f S" "bij f" "S ≠ {x}" shows "cyclic_on (perm_rem x f) (S - {x})"
  using assms[unfolded cyclic_on_alldef] by (simp add: cyclic_on_def orbit_perm_rem_eq) auto

end