Theory Executable_Permutations

section ‹Permutations as Products of Disjoint Cycles›

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

subsection ‹Cyclic Permutations›

definition list_succ :: "'a list ⇒ 'a ⇒ 'a" where
  "list_succ xs x = (if x ∈ set xs then xs ! ((index xs x + 1) mod length xs) else x)"

text ‹
  We demonstrate the functions on the following simple lemmas

  @{lemma "list_succ [1 :: int, 2, 3] 1 = 2" by code_simp}
  @{lemma "list_succ [1 :: int, 2, 3] 2 = 3" by code_simp}
  @{lemma "list_succ [1 :: int, 2, 3] 3 = 1" by code_simp}
›

lemma list_succ_altdef:
  "list_succ xs x = (let n = index xs x in if n + 1 = length xs then xs ! 0 else if n + 1 < length xs then xs ! (n + 1) else x)"
  using index_le_size[of xs x] unfolding list_succ_def index_less_size_conv[symmetric] by (auto simp: Let_def)

lemma list_succ_Nil:
  "list_succ [] = id"
  by (simp add: list_succ_def fun_eq_iff)

lemma list_succ_singleton:
  "list_succ [x] = list_succ []"
  by (simp add: fun_eq_iff list_succ_def)

lemma list_succ_short:
  assumes "length xs < 2" shows "list_succ xs = id"
  using assms
  by (cases xs) (rename_tac [2] y ys, case_tac [2] ys, auto simp: list_succ_Nil list_succ_singleton)

lemma list_succ_simps:
  "index xs x + 1 = length xs ⟹ list_succ xs x = xs ! 0"
  "index xs x + 1 < length xs ⟹ list_succ xs x = xs ! (index xs x + 1)"
  "length xs ≤ index xs x ⟹ list_succ xs x = x"
  by (auto simp: list_succ_altdef)

lemma list_succ_not_in:
  assumes "x ∉ set xs" shows "list_succ xs x = x"
  using assms by (auto simp: list_succ_def)

lemma list_succ_list_succ_rev:
  assumes "distinct xs" shows "list_succ (rev xs) (list_succ xs x) = x"
proof -
  { assume "index xs x + 1 < length xs"
    moreover then have "length xs - Suc (Suc (length xs - Suc (Suc (index xs x)))) = index xs x"
      by linarith
    ultimately have ?thesis using assms
      by (simp add: list_succ_def index_rev index_nth_id rev_nth)
  }
  moreover
  { assume A: "index xs x + 1 = length xs"
    moreover
    from A have "xs ≠ []" by auto
    moreover
    with A have "last xs = xs ! index xs x" by (cases "length xs") (auto simp: last_conv_nth)
    ultimately
    have ?thesis
      using assms
      by (auto simp add: list_succ_def rev_nth index_rev index_nth_id last_conv_nth)
  }
  moreover
  { assume A: "index xs x ≥ length xs"
    then have "x ∉ set xs" by (metis index_less less_irrefl)
    then have ?thesis by (auto simp: list_succ_def) }
  ultimately show ?thesis by (metis discrete le_less not_less) 
qed

lemma inj_list_succ: "distinct xs ⟹ inj (list_succ xs)"
  by (metis injI list_succ_list_succ_rev)

lemma inv_list_succ_eq: "distinct xs ⟹ inv (list_succ xs) = list_succ (rev xs)"
  by (metis distinct_rev inj_imp_inv_eq inj_list_succ list_succ_list_succ_rev)

lemma bij_list_succ: "distinct xs ⟹ bij (list_succ xs)"
  by (metis bij_def inj_list_succ distinct_rev list_succ_list_succ_rev surj_def)

lemma list_succ_permutes:
  assumes "distinct xs" shows "list_succ xs permutes set xs"
  using assms by (auto simp: permutes_conv_has_dom bij_list_succ has_dom_def list_succ_def)

lemma permutation_list_succ:
  assumes "distinct xs" shows "permutation (list_succ xs)"
  using list_succ_permutes[OF assms] by (auto simp: permutation_permutes)

lemma list_succ_nth:
  assumes "distinct xs" "n < length xs" shows "list_succ xs (xs ! n) = xs ! (Suc n mod length xs)"
  using assms by (auto simp: list_succ_def index_nth_id)

lemma list_succ_last[simp]:
  assumes "distinct xs" "xs ≠ []" shows "list_succ xs (last xs) = hd xs"
  using assms by (auto simp: list_succ_def hd_conv_nth)

lemma list_succ_rotate1[simp]:
  assumes "distinct xs" shows "list_succ (rotate1 xs) = list_succ xs"
proof (rule ext)
  fix y show "list_succ (rotate1 xs) y = list_succ xs y"
    using assms
  proof (induct xs)
    case Nil then show ?case by simp
  next
    case (Cons x xs)
    show ?case
    proof (cases "x = y")
      case True
      then have "index (xs @ [y]) y = length xs"
        using ‹distinct (x # xs)› by (simp add: index_append)
      with True show ?thesis by (cases "xs=[]") (auto simp: list_succ_def nth_append)
    next
      case False
      then show ?thesis
        apply (cases "index xs y + 1 < length xs")
        apply (auto simp:list_succ_def index_append nth_append)
        by (metis Suc_lessI index_less_size_conv mod_self nth_Cons_0 nth_append nth_append_length)
    qed
  qed
qed
  
lemma list_succ_rotate[simp]:
  assumes "distinct xs" shows "list_succ (rotate n xs) = list_succ xs"
  using assms by (induct n) auto

lemma list_succ_in_conv:
  "list_succ xs x ∈ set xs ⟷ x ∈ set xs"
  by (auto simp: list_succ_def not_nil_if_in_set )

lemma list_succ_in_conv1:
  assumes "A ∩ set xs = {}"
  shows "list_succ xs x ∈ A ⟷ x ∈ A"
  by (metis assms disjoint_iff_not_equal list_succ_in_conv list_succ_not_in)

lemma list_succ_commute:
  assumes "set xs ∩ set ys = {}"
  shows "list_succ xs (list_succ ys x) = list_succ ys (list_succ xs x)"
proof -
  have "⋀x. x ∈ set xs ⟹ list_succ ys x = x"
     "⋀x. x ∈ set ys ⟹ list_succ xs x = x"
    using assms by (blast intro: list_succ_not_in)+
  then show ?thesis
    by (cases "x ∈ set xs ∪ set ys") (auto simp: list_succ_in_conv list_succ_not_in)
qed


subsection ‹Arbitrary Permutations›

fun lists_succ :: "'a list list ⇒ 'a ⇒ 'a" where
  "lists_succ [] x = x"
| "lists_succ (xs # xss) x = list_succ xs (lists_succ xss x)"

definition distincts ::  "'a list list ⇒ bool" where
  "distincts xss ≡ distinct xss ∧ (∀xs ∈ set xss. distinct xs ∧ xs ≠ []) ∧ (∀xs ∈ set xss. ∀ys ∈ set xss. xs ≠ ys ⟶ set xs ∩ set ys = {})"

lemma distincts_distinct: "distincts xss ⟹ distinct xss"
  by (auto simp: distincts_def)

lemma distincts_Nil[simp]: "distincts []"
  by (simp add: distincts_def)

lemma distincts_single: "distincts [xs] ⟷ distinct xs ∧ xs ≠ []"
  by (auto simp add: distincts_def)

lemma distincts_Cons: "distincts (xs # xss)
   ⟷ xs ≠ [] ∧ distinct xs ∧ distincts xss ∧ (set xs ∩ (⋃ys ∈ set xss. set ys)) = {}" (is "?L ⟷ ?R")
proof 
  assume ?L then show ?R by (auto simp: distincts_def)
next
  assume ?R
  then have "distinct (xs # xss)"
    apply (auto simp: disjoint_iff_not_equal distincts_distinct)
    apply (metis length_greater_0_conv nth_mem)
    done
  moreover
  from ‹?R› have "∀xs ∈ set (xs # xss). distinct xs ∧ xs ≠ []"
    by (auto simp: distincts_def)
  moreover
  from ‹?R› have "∀xs' ∈ set (xs # xss). ∀ys ∈ set (xs # xss). xs' ≠ ys ⟶ set xs' ∩ set ys = {}"
    by (simp add: distincts_def) blast
  ultimately show ?L unfolding distincts_def by (intro conjI)
qed

lemma distincts_Cons': "distincts (xs # xss)
   ⟷ xs ≠ [] ∧ distinct xs ∧ distincts xss ∧ (∀ys ∈ set xss. set xs ∩ set ys = {})" (is "?L ⟷ ?R")
 unfolding distincts_Cons by blast

lemma distincts_rev:
  "distincts (map rev xss) ⟷ distincts xss"
  by (simp add: distincts_def distinct_map)

lemma length_distincts:
  assumes "distincts xss"
  shows "length xss = card (set ` set xss)"
  using assms
proof (induct xss)
  case Nil then show ?case by simp
next
  case (Cons xs xss)
  then have "set xs ∉ set ` set xss"
    using equals0I[of "set xs"] by (auto simp: distincts_Cons disjoint_iff_not_equal )
  with Cons show ?case by (auto simp add: distincts_Cons)
qed

lemma distincts_remove1: "distincts xss ⟹ distincts (remove1 xs xss)"
  by (auto simp: distincts_def)

lemma distinct_Cons_remove1:
  "x ∈ set xs ⟹ distinct (x # remove1 x xs) = distinct xs"
  by (induct xs) auto

lemma set_Cons_remove1:
  "x ∈ set xs ⟹ set (x # remove1 x xs) = set xs"
  by (induct xs) auto

lemma distincts_Cons_remove1:
  "xs ∈ set xss ⟹ distincts (xs # remove1 xs xss) = distincts xss"
  by (simp only: distinct_Cons_remove1 set_Cons_remove1 distincts_def)

lemma distincts_inj_on_set:
  assumes "distincts xss" shows "inj_on set (set xss)"
  by (rule inj_onI) (metis assms distincts_def inf.idem set_empty)

lemma distincts_distinct_set:
  assumes "distincts xss" shows "distinct (map set xss)"
  using assms by (auto simp: distinct_map distincts_distinct distincts_inj_on_set)

lemma distincts_distinct_nth:
  assumes "distincts xss" "n < length xss" shows "distinct (xss ! n)"
  using assms by (auto simp: distincts_def)

lemma lists_succ_not_in:
  assumes "x ∉ (⋃xs∈set xss. set xs)" shows "lists_succ xss x = x"
  using assms by (induct xss) (auto simp: list_succ_not_in)

lemma lists_succ_in_conv:
  "lists_succ xss x ∈ (⋃xs∈set xss. set xs) ⟷ x ∈ (⋃xs∈set xss. set xs)"
  by (induct xss) (auto simp: list_succ_in_conv lists_succ_not_in list_succ_not_in)

lemma lists_succ_in_conv1:
  assumes "A ∩ (⋃xs∈set xss. set xs) = {}"
  shows "lists_succ xss x ∈ A ⟷ x ∈ A"
  by (metis Int_iff assms emptyE lists_succ_in_conv lists_succ_not_in)

lemma lists_succ_Cons_pf: "lists_succ (xs # xss) = list_succ xs o lists_succ xss"
  by auto

lemma lists_succ_Nil_pf: "lists_succ [] = id"
  by (simp add: fun_eq_iff)

lemmas lists_succ_simps_pf = lists_succ_Cons_pf lists_succ_Nil_pf

lemma lists_succ_permutes:
  assumes "distincts xss"
  shows "lists_succ xss permutes (⋃xs ∈ set xss. set xs)"
  using assms
proof (induction xss)
  case Nil then show ?case by auto
next
  case (Cons xs xss)
  have "list_succ xs permutes (set xs)"
    using Cons by (intro list_succ_permutes) (simp add: distincts_def in_set_member)
  moreover
  have "lists_succ xss permutes (⋃ys ∈ set xss. set ys)"
    using Cons by (auto simp: Cons distincts_def)
  ultimately show "lists_succ (xs # xss) permutes (⋃ys ∈ set (xs # xss). set ys)"
    using Cons by (auto simp: lists_succ_Cons_pf intro: permutes_compose permutes_subset)
qed

lemma bij_lists_succ: "distincts xss ⟹ bij (lists_succ xss)"
  by (induct xss) (auto simp: lists_succ_simps_pf bij_comp bij_list_succ distincts_Cons)

lemma lists_succ_snoc: "lists_succ (xss @ [xs]) = lists_succ xss o list_succ xs"
  by (induct xss) auto

lemma inv_lists_succ_eq:
  assumes "distincts xss"
  shows "inv (lists_succ xss) = lists_succ (rev (map rev xss))"
proof -
  have *: "⋀f g. inv (λb. f (g b)) = inv (f o g)" by (simp add: o_def)
  have **: "lists_succ [] = id" by auto
  show ?thesis
    using assms by (induct xss) (auto simp: * ** lists_succ_snoc lists_succ_Cons_pf o_inv_distrib
      inv_list_succ_eq distincts_Cons bij_list_succ bij_lists_succ)
qed

lemma lists_succ_remove1:
  assumes "distincts xss" "xs ∈ set xss"
  shows "lists_succ (xs # remove1 xs xss) = lists_succ xss"
  using assms
proof (induct xss)
  case Nil then show ?case by simp
next
  case (Cons ys xss)
  show ?case
  proof cases
    assume "xs = ys" then show ?case by simp
  next
    assume "xs ≠ ys"
    with Cons.prems have inter: "set xs ∩ set ys = {}" and "xs ∈ set xss"
      by (auto simp: distincts_Cons)
    have dists:
        "distincts (xs # remove1 xs xss)"
        "distincts (xs # ys # remove1 xs xss)"
      using ‹distincts (ys # xss)› ‹xs ∈ set xss› by (auto simp: distincts_def)

    have "list_succ xs ∘ (list_succ ys ∘ lists_succ (remove1 xs xss))
        = list_succ ys ∘ (list_succ xs ∘ lists_succ (remove1 xs xss))"
      using inter unfolding fun_eq_iff comp_def
      by (subst list_succ_commute) auto
    also have "… = list_succ ys o (lists_succ (xs # remove1 xs xss))"
      using dists by (simp add: lists_succ_Cons_pf distincts_Cons)
    also have "… = list_succ ys o lists_succ xss"
      using ‹xs ∈ set xss› ‹distincts (ys # xss)›
      by (simp add: distincts_Cons Cons.hyps)
    finally
    show "lists_succ (xs # remove1 xs (ys # xss)) = lists_succ (ys # xss)"
      using Cons dists by (auto simp: lists_succ_Cons_pf distincts_Cons)
  qed
qed

lemma lists_succ_no_order:
  assumes "distincts xss" "distincts yss" "set xss = set yss"
  shows "lists_succ xss = lists_succ yss"
  using assms
proof (induct xss arbitrary: yss)
  case Nil then show ?case by simp
next
  case (Cons xs xss)
  have "xs ∉ set xss" "xs ∈ set yss" using Cons.prems
    by (auto dest: distincts_distinct)
  have "lists_succ xss = lists_succ (remove1 xs yss)"
    using Cons.prems ‹xs ∉ _›
    by (intro Cons.hyps) (auto simp add: distincts_Cons distincts_remove1 distincts_distinct)
  then have "lists_succ (xs # xss) = lists_succ (xs # remove1 xs yss)"
    using Cons.prems ‹xs ∈ _›
    by (simp add: lists_succ_Cons_pf distincts_Cons_remove1)
  then show ?case
    using Cons.prems ‹xs ∈ _› by (simp add: lists_succ_remove1)
qed



section ‹List Orbits›

text ‹Computes the orbit of @{term x} under @{term f}›
definition orbit_list :: "('a ⇒ 'a) ⇒ 'a ⇒ 'a list" where
  "orbit_list f x ≡ iterate 0 (funpow_dist1 f x x) f x"

partial_function (tailrec)
  orbit_list_impl :: "('a ⇒ 'a) ⇒ 'a ⇒ 'a list ⇒ 'a ⇒ 'a list"
where
  "orbit_list_impl f s acc x = (let x' = f x in if x' = s then rev (x # acc) else orbit_list_impl f s (x # acc) x')"

context notes [simp] = length_fold_remove1_le begin
text ‹Computes the list of orbits›
fun orbits_list :: "('a ⇒ 'a) ⇒ 'a list ⇒ 'a list list" where
  "orbits_list f [] = []"
| "orbits_list f (x # xs) =
     orbit_list f x # orbits_list f (fold remove1 (orbit_list f x) xs)"

fun orbits_list_impl :: "('a ⇒ 'a) ⇒ 'a list ⇒ 'a list list" where
  "orbits_list_impl f [] = []"
| "orbits_list_impl f (x # xs) =
     (let fc = orbit_list_impl f x [] x in fc # orbits_list_impl f (fold remove1 fc xs))"

declare orbit_list_impl.simps[code]
end

abbreviation sset :: "'a list list ⇒ 'a set set" where
  "sset xss ≡ set ` set xss"

lemma iterate_funpow_step:
  assumes "f x ≠ y" "y ∈ orbit f x"
  shows "iterate 0 (funpow_dist1 f x y) f x = x # iterate 0 (funpow_dist1 f (f x) y) f (f x)"
proof -
  from assms have A: "y ∈ orbit f (f x)" by (simp add: orbit_step)
  have "iterate 0 (funpow_dist1 f x y) f x = x # iterate 1 (funpow_dist1 f x y) f x" (is "_ = _ # ?it")
    unfolding iterate_def by (simp add: upt_rec) 
  also have "?it = map (λn. (f ^^ n) x) (map Suc [0..<funpow_dist f (f x) y])"
    unfolding iterate_def map_Suc_upt by simp
  also have "… = map (λn. (f ^^ n) (f x)) [0..<funpow_dist f (f x) y]"
    by (simp add: funpow_swap1)
  also have "… = iterate 0 (funpow_dist1 f (f x) y) f (f x)"
    unfolding iterate_def
    unfolding iterate_def by (simp add: funpow_dist_step[OF assms(1) A])
  finally show ?thesis .
qed

lemma orbit_list_impl_conv:
  assumes "y ∈ orbit f x"
  shows "orbit_list_impl f y acc x = rev acc @ iterate 0 (funpow_dist1 f x y) f x"
  using assms
proof (induct n≡"funpow_dist1 f x y" arbitrary: x acc)
  case (Suc x)

  show ?case
  proof cases
    assume "f x = y"
    then show ?thesis by (subst orbit_list_impl.simps) (simp add: Let_def iterate_def funpow_dist_0)
  next
    assume not_y :"f x ≠ y"

    have y_in_succ: "y ∈ orbit f (f x)"
      by (intro orbit_step Suc.prems not_y)

    have "orbit_list_impl f y acc x = orbit_list_impl f y (x # acc) (f x)"
      using not_y by (subst orbit_list_impl.simps) simp
    also have "… = rev (x # acc) @ iterate 0 (funpow_dist1 f (f x) y) f (f x)" (is "_ = ?rev @ ?it")
      by (intro Suc funpow_dist_step not_y y_in_succ)
    also have "… = rev acc @ iterate 0 (funpow_dist1 f x y) f x"
      using not_y Suc.prems by (simp add: iterate_funpow_step)
    finally show ?thesis .
  qed
qed

lemma orbit_list_conv_impl:
  assumes "x ∈ orbit f x"
  shows "orbit_list f x = orbit_list_impl f x [] x"
  unfolding orbit_list_impl_conv[OF assms] orbit_list_def by simp


lemma set_orbit_list:
  assumes "x ∈ orbit f x"
  shows "set (orbit_list f x) = orbit f x"
  by (simp add: orbit_list_def orbit_conv_funpow_dist1[OF assms] set_iterate)

lemma set_orbit_list':
  assumes "permutation f" shows "set (orbit_list f x) = orbit f x"
  using assms by (simp add: permutation_self_in_orbit set_orbit_list)

lemma distinct_orbit_list:
  assumes "x ∈ orbit f x"
  shows "distinct (orbit_list f x)"
  by (simp del: upt_Suc add: orbit_list_def iterate_def distinct_map inj_on_funpow_dist1[OF assms])

lemma distinct_orbit_list':
  assumes "permutation f" shows "distinct (orbit_list f x)"
  using assms by (simp add: permutation_self_in_orbit distinct_orbit_list)

lemma orbits_list_conv_impl:
  assumes "permutation f"
  shows "orbits_list f xs = orbits_list_impl f xs"
proof (induct "length xs" arbitrary: xs rule: less_induct)
  case less show ?case
    using assms by (cases xs) (auto simp: assms less less_Suc_eq_le length_fold_remove1_le
      orbit_list_conv_impl permutation_self_in_orbit Let_def)
qed

lemma orbit_list_not_nil[simp]: "orbit_list f x ≠ []"
  by (simp add: orbit_list_def)

lemma sset_orbits_list:
  assumes "permutation f" shows "sset (orbits_list f xs) = (orbit f) ` set xs"
proof (induct "length xs" arbitrary: xs rule: less_induct)
  case less
  show ?case
  proof (cases xs)
    case Nil then show ?thesis by simp
  next
    case (Cons x' xs')
    let ?xs'' = "fold remove1 (orbit_list f x') xs'"
    have A: "sset (orbits_list f ?xs'') = orbit f ` set ?xs''"
      using Cons by (simp add: less_Suc_eq_le length_fold_remove1_le less.hyps)
    have B: "set (orbit_list f x') = orbit f x'"
      by (rule set_orbit_list) (simp add: permutation_self_in_orbit assms)

    have "orbit f ` set (fold remove1 (orbit_list f x') xs') ⊆ orbit f ` set xs'"
      using set_fold_remove1[of _ xs'] by auto
    moreover
    have "orbit f ` set xs' - {orbit f x'} ⊆ (orbit f ` set (fold remove1 (orbit_list f x') xs'))" (is "?L ⊆ ?R")
    proof
      fix A assume "A ∈ ?L"
      then obtain y where "A = orbit f y" "y ∈ set xs'" by auto
      have "A ≠ orbit f x'" using ‹A ∈ ?L› by auto
      from ‹A = _› ‹A ≠ _› have "y ∉ orbit f x'"
        by (meson assms cyclic_on_orbit orbit_cyclic_eq3 permutation_permutes)
      with ‹y ∈ _› have "y ∈ set (fold remove1 (orbit_list f x') xs')"
        by (auto simp: set_fold_remove1' set_orbit_list permutation_self_in_orbit assms)
      then show "A ∈ ?R" using ‹A = _› by auto
    qed
    ultimately
    show ?thesis by (auto simp: A B Cons)
  qed
qed



subsection ‹Relation to @{term cyclic_on}›

lemma list_succ_orbit_list:
  assumes "s ∈ orbit f s" "⋀x. x ∉ orbit f s ⟹ f x = x"
  shows "list_succ (orbit_list f s) = f"
proof -
  have "distinct (orbit_list f s)" "⋀x. x ∉ set (orbit_list f s) ⟹ x = f x"
    using assms by (simp_all add: distinct_orbit_list set_orbit_list)
  moreover
  have "⋀i. i < length (orbit_list f s) ⟹ orbit_list f s ! (Suc i mod length (orbit_list f s)) = f (orbit_list f s ! i)"
    using funpow_dist1_prop[OF ‹s ∈ orbit f s›] by (auto simp: orbit_list_def funpow_mod_eq)
  ultimately show ?thesis
    by (auto simp: list_succ_def fun_eq_iff)
qed

lemma list_succ_funpow_conv:
  assumes A: "distinct xs" "x ∈ set xs"
  shows "(list_succ xs ^^ n) x = xs ! ((index xs x + n) mod length xs)"
proof -
  have "xs ≠ []" using assms by auto
  then show ?thesis
    by (induct n) (auto simp: hd_conv_nth A index_nth_id list_succ_def mod_simps)
qed

lemma orbit_list_succ:
  assumes "distinct xs" "x ∈ set xs"
  shows "orbit (list_succ xs) x = set xs"
proof (intro set_eqI iffI)
  fix y assume "y ∈ orbit (list_succ xs) x"
  then show "y ∈ set xs"
    by induct (auto simp: list_succ_in_conv ‹x ∈ set xs›)
next
  fix y assume "y ∈ set xs"
  moreover
  { fix i j have "i < length xs ⟹ j < length xs ⟹ ∃n. xs ! j = xs ! ((i + n) mod length xs)"
      using assms by (auto simp: exI[where x="j + (length xs - i)"])
  }
  ultimately
  show "y ∈ orbit (list_succ xs) x"
    using assms by (auto simp: orbit_altdef_permutation permutation_list_succ list_succ_funpow_conv index_nth_id in_set_conv_nth)
qed

lemma cyclic_on_list_succ:
  assumes "distinct xs" "xs ≠ []" shows "cyclic_on (list_succ xs) (set xs)"
  using assms last_in_set by (auto simp: cyclic_on_def orbit_list_succ)

lemma obtain_orbit_list_func:
  assumes "s ∈ orbit f s" "⋀x. x ∉ orbit f s ⟹ f x = x"
  obtains xs where "f = list_succ xs" "set xs = orbit f s" "distinct xs" "hd xs = s"
proof -
  { from assms have "f = list_succ (orbit_list f s)" by (simp add: list_succ_orbit_list)
    moreover
    have "set (orbit_list f s) = orbit f s" "distinct (orbit_list f s)"
      by (auto simp: set_orbit_list distinct_orbit_list assms)
    moreover have "hd (orbit_list f s) = s"
      by (simp add: orbit_list_def iterate_def hd_map del: upt_Suc)
    ultimately have "∃xs. f = list_succ xs ∧ set xs = orbit f s ∧ distinct xs ∧ hd xs = s" by blast
  } then show ?thesis by (metis that)
qed

lemma cyclic_on_obtain_list_succ:
  assumes "cyclic_on f S" "⋀x. x ∉ S ⟹ f x = x"
  obtains xs where "f = list_succ xs" "set xs = S" "distinct xs"
proof -
  from assms obtain s where s: "s ∈ orbit f s" "⋀x. x ∉ orbit f s ⟹ f x = x"  "S = orbit f s"
    by (auto simp: cyclic_on_def)
  then show ?thesis by (metis that obtain_orbit_list_func)
qed

lemma cyclic_on_obtain_list_succ':
  assumes "cyclic_on f S" "f permutes S"
  obtains xs where "f = list_succ xs" "set xs = S" "distinct xs"
  using assms unfolding permutes_def by (metis cyclic_on_obtain_list_succ)

lemma list_succ_unique:
  assumes "s ∈ orbit f s" "⋀x. x ∉ orbit f s ⟹ f x = x"
  shows "∃!xs. f = list_succ xs ∧ distinct xs ∧ hd xs = s ∧ set xs = orbit f s"
proof -
  from assms obtain xs where xs: "f = list_succ xs" "distinct xs" "hd xs = s" "set xs = orbit f s" 
    by (rule obtain_orbit_list_func)
  moreover
  { fix zs
    assume A: "f = list_succ zs" "distinct zs" "hd zs = s" "set zs = orbit f s"
    then have "zs ≠ []" using ‹s ∈ orbit f s› by auto
    from ‹distinct xs› ‹distinct zs› ‹set xs = orbit f s› ‹set zs = orbit f s›
    have len: "length xs = length zs" by (metis distinct_card)

    { fix n assume "n < length xs"
      then have "zs ! n = xs ! n"
      proof (induct n)
        case 0 with A xs ‹zs ≠ []› show ?case by (simp add: hd_conv_nth nth_rotate_conv_nth)
      next
        case (Suc n)
        then have "list_succ zs (zs ! n) = list_succ xs (xs! n)"
          using ‹f = list_succ xs› ‹f = list_succ zs› by simp
        with ‹Suc n < _› show ?case
          by (simp add:list_succ_nth len ‹distinct xs› ‹distinct zs›)
      qed }
    then have "zs = xs" by (metis len nth_equalityI) }
  ultimately show ?thesis by metis
qed

lemma distincts_orbits_list:
  assumes "distinct as" "permutation f"
  shows "distincts (orbits_list f as)"
  using assms(1)
proof (induct "length as" arbitrary: as rule: less_induct)
  case less
  show ?case
  proof (cases as)
    case Nil then show ?thesis by simp
  next
    case (Cons a as')
    let ?as' = "fold remove1 (orbit_list f a) as'"
    from Cons less.prems have A: "distincts (orbits_list f (fold remove1 (orbit_list f a) as'))"
      by (intro less) (auto simp: distinct_fold_remove1 length_fold_remove1_le less_Suc_eq_le)

    have B: "set (orbit_list f a) ∩ ⋃(sset (orbits_list f (fold remove1 (orbit_list f a) as'))) = {}"
    proof -
      have "orbit f a ∩ set (fold remove1 (orbit_list f a) as') = {}"
        using assms less.prems Cons by (simp add: set_fold_remove1_distinct set_orbit_list')
      then have "orbit f a ∩ ⋃ (orbit f ` set (fold remove1 (orbit_list f a) as')) = {}"
        by auto (metis assms(2) cyclic_on_orbit disjoint_iff_not_equal permutation_self_in_orbit[OF assms(2)] orbit_cyclic_eq3 permutation_permutes)
      then show ?thesis using assms
      by (auto simp: set_orbit_list' sset_orbits_list disjoint_iff_not_equal)
    qed
    show ?thesis
      using A B assms by (auto simp: distincts_Cons Cons distinct_orbit_list')
  qed
qed

lemma cyclic_on_lists_succ':
  assumes "distincts xss"
  shows "A ∈ sset xss ⟹ cyclic_on (lists_succ xss) A"
  using assms
proof (induction xss arbitrary: A)
  case Nil then show ?case by auto
next
  case (Cons xs xss A)
  then have inter: "set xs ∩ (⋃ys∈set xss. set ys) = {}" by (auto simp: distincts_Cons)

  note pcp[OF _ _ inter] = permutes_comp_preserves_cyclic1 permutes_comp_preserves_cyclic2
  from Cons show "cyclic_on (lists_succ (xs # xss)) A"
    by (cases "A = set xs")
      (auto intro: pcp simp: cyclic_on_list_succ list_succ_permutes
        lists_succ_permutes lists_succ_Cons_pf distincts_Cons)
qed

lemma cyclic_on_lists_succ:
  assumes "distincts xss"
  shows "⋀xs. xs ∈ set xss ⟹ cyclic_on (lists_succ xss) (set xs)"
  using assms by (auto intro: cyclic_on_lists_succ')

lemma permutes_as_lists_succ:
  assumes "distincts xss"
  assumes ls_eq: "⋀xs. xs ∈ set xss ⟹ list_succ xs = perm_restrict f (set xs)"
  assumes "f permutes (⋃(sset xss))"
  shows "f = lists_succ xss"
  using assms
proof (induct xss arbitrary: f)
  case Nil then show ?case by simp
next
  case (Cons xs xss)
  let ?sets = "λxss. ⋃ys ∈ set xss. set ys"

  have xs: "distinct xs" "xs ≠ []" using Cons by (auto simp: distincts_Cons)

  have f_xs: "perm_restrict f (set xs) = list_succ xs"
    using Cons by simp

  have co_xs: "cyclic_on (perm_restrict f (set xs)) (set xs)"
    unfolding f_xs using xs by (rule cyclic_on_list_succ)

  have perm_xs: "perm_restrict f (set xs) permutes set xs"
    unfolding f_xs using ‹distinct xs› by (rule list_succ_permutes)

  have perm_xss: "perm_restrict f (?sets xss) permutes (?sets xss)"
  proof -
    have "perm_restrict f (?sets (xs # xss) - set xs) permutes (?sets (xs # xss) - set xs)"
      using Cons co_xs by (intro perm_restrict_diff_cyclic) (auto simp: cyclic_on_perm_restrict)
    also have "?sets (xs # xss) - set xs = ?sets xss"
      using Cons by (auto simp: distincts_Cons)
    finally show ?thesis .
  qed

  have f_xss: "perm_restrict f (?sets xss) = lists_succ xss"
  proof -
    have *: "⋀xs. xs ∈ set xss ⟹ ((⋃x∈set xss. set x) ∩ set xs) = set xs"
      by blast
    with perm_xss Cons.prems show ?thesis
      by (intro Cons.hyps) (auto simp: distincts_Cons perm_restrict_perm_restrict *)
  qed

  from Cons.prems show "f = lists_succ (xs # xss)"
    by (simp add: lists_succ_Cons_pf distincts_Cons f_xss[symmetric]
      perm_restrict_union perm_xs perm_xss)
qed

lemma cyclic_on_obtain_lists_succ:
  assumes
    permutes: "f permutes S" and
    S: "S = ⋃(sset css)" and
    dists: "distincts css" and
    cyclic: "⋀cs. cs ∈ set css ⟹ cyclic_on f (set cs)"
  obtains xss where "f = lists_succ xss" "distincts xss" "map set xss = map set css" "map hd xss = map hd css"
proof -
  let ?fc = "λcs. perm_restrict f (set cs)"
  define some_list where "some_list cs = (SOME xs. ?fc cs = list_succ xs ∧ set xs = set cs ∧ distinct xs ∧ hd xs = hd cs)" for cs
  { fix cs assume "cs ∈ set css"
    then have "cyclic_on (?fc cs) (set cs)" "⋀x. x ∉ set cs ⟹ ?fc cs x = x" "hd cs ∈ set cs"
      using cyclic dists by (auto simp add: cyclic_on_perm_restrict perm_restrict_def distincts_def)
    then have "hd cs ∈ orbit (?fc cs) (hd cs)"  "⋀x. x ∉ orbit (?fc cs) (hd cs) ⟹ ?fc cs x = x" "hd cs ∈ set cs" "set cs = orbit (?fc cs) (hd cs)"
      by (auto simp: cyclic_on_alldef)
    then have "∃xs. ?fc cs = list_succ xs ∧ set xs = set cs ∧ distinct xs ∧ hd xs = hd cs"
      by (metis obtain_orbit_list_func)
    then have "?fc cs = list_succ (some_list cs) ∧ set (some_list cs) = set cs ∧ distinct (some_list cs) ∧ hd (some_list cs) = hd cs"
      unfolding some_list_def by (rule someI_ex)
    then have "?fc cs = list_succ (some_list cs)" "set (some_list cs) = set cs" "distinct (some_list cs)" "hd (some_list cs) = hd cs"
      by auto
  } note sl_cs  = this

  have "⋀cs. cs ∈ set css ⟹ cs ≠ []" using dists by (auto simp: distincts_def)
  then have some_list_ne: "⋀cs. cs ∈ set css ⟹ some_list cs ≠ []"
    by (metis set_empty sl_cs(2))

  have set: "map set (map some_list css) = map set css" "map hd (map some_list css) = map hd css"
    using sl_cs(2,4) by (auto simp add: map_idI)

  have distincts: "distincts (map some_list css)"
  proof -
    have c_dist: "⋀xs ys. ⟦xs∈set css; ys∈set css; xs ≠ ys⟧ ⟹ set xs ∩ set ys = {}"
      using dists by (auto simp: distincts_def)

    have "distinct (map some_list css)"
    proof -
      have "inj_on some_list (set css)"
        using sl_cs(2) c_dist by (intro inj_onI) (metis inf.idem set_empty) 
      with ‹distincts css› show ?thesis
        by (auto simp: distincts_distinct distinct_map)
    qed
    moreover
    have "∀xs∈set (map some_list css). distinct xs ∧ xs ≠ []"
      using sl_cs(3) some_list_ne by auto
    moreover
    from c_dist have "(∀xs∈set (map some_list css). ∀ys∈set (map some_list css). xs ≠ ys ⟶ set xs ∩ set ys = {})"
      using sl_cs(2) by auto
    ultimately
    show ?thesis by (simp add: distincts_def)
  qed

  have f: "f = lists_succ (map some_list css)"
    using distincts
  proof (rule permutes_as_lists_succ)
    fix xs assume "xs ∈ set (map some_list css)"
    then show "list_succ xs = perm_restrict f (set xs)"
      using sl_cs(1) sl_cs(2) by auto
  next
    have "S = (⋃xs∈set (map some_list css). set xs)"
      using S sl_cs(2) by auto
    with permutes show "f permutes ⋃(sset (map some_list css))"
      by simp
  qed

  from f distincts set  show ?thesis ..
qed


subsection ‹Permutations of a List›

lemma length_remove1_less:
  assumes "x ∈ set xs" shows "length (remove1 x xs) < length xs"
proof -
  from assms have "0 < length xs" by auto
  with assms show ?thesis by (auto simp: length_remove1)
qed
context notes [simp] = length_remove1_less begin
fun permutations :: "'a list ⇒ 'a list list" where
  permutations_Nil: "permutations [] = [[]]"
| permutations_Cons:
    "permutations xs = [y # ys. y <- xs, ys <- permutations (remove1 y xs)]"
end

declare permutations_Cons[simp del]

text ‹
  The function above returns all permutations of a list. The function below computes
  only those which yield distinct cyclic permutation functions (cf. @{term list_succ}).
›

fun cyc_permutations :: "'a list ⇒ 'a list list" where
  "cyc_permutations [] = [[]]"
| "cyc_permutations (x # xs) = map (Cons x) (permutations xs)"



lemma nil_in_permutations[simp]: "[] ∈ set (permutations xs) ⟷ xs = []"
  by (induct xs) (auto simp: permutations_Cons)

lemma permutations_not_nil:
  assumes "xs ≠ []"
  shows "permutations xs = concat (map (λx. map ((#) x) (permutations (remove1 x xs))) xs)"
  using assms by (cases xs) (auto simp: permutations_Cons)

lemma set_permutations_step:
  assumes "xs ≠ []"
  shows "set (permutations xs) = (⋃x ∈ set xs. Cons x ` set (permutations (remove1 x xs)))"
  using assms by (cases xs) (auto simp: permutations_Cons)

lemma in_set_permutations:
  assumes "distinct xs"
  shows "ys ∈ set (permutations xs) ⟷ distinct ys ∧ set xs = set ys" (is "?L xs ys ⟷ ?R xs ys")
  using assms
proof (induct "length xs" arbitrary: xs ys)
  case 0 then show ?case by auto
next
  case (Suc n)
  then have "xs ≠ []" by auto

  show ?case
  proof
    assume "?L xs ys"
    then obtain y ys' where "ys = y # ys'" "y ∈ set xs" "ys' ∈ set (permutations (remove1 (hd ys) xs))"
      using ‹xs ≠ []› by (auto simp: permutations_not_nil)
    moreover
    then have "?R (remove1 y xs) ys'"
      using Suc.prems Suc.hyps(2) by (intro Suc.hyps(1)[THEN iffD1]) (auto simp: length_remove1)
    ultimately show "?R xs ys"
      using Suc by auto
  next
    assume "?R xs ys"
    with ‹xs ≠ []› obtain y ys' where "ys = y # ys'" "y ∈ set xs" by (cases ys) auto
    moreover
    then have "ys' ∈ set (permutations (remove1 y xs))"
      using Suc ‹?R xs ys› by (intro Suc.hyps(1)[THEN iffD2]) (auto simp: length_remove1)
    ultimately
    show "?L xs ys"
      using ‹xs ≠ []› by (auto simp: permutations_not_nil)
  qed
qed

lemma in_set_cyc_permutations:
  assumes "distinct xs"
  shows "ys ∈ set (cyc_permutations xs) ⟷ distinct ys ∧ set xs = set ys ∧ hd ys = hd xs" (is "?L xs ys ⟷ ?R xs ys")
proof (cases xs)
  case (Cons x xs) with assms show ?thesis
    by (cases ys) (auto simp: in_set_permutations intro!: imageI)
qed auto

lemma in_set_cyc_permutations_obtain:
  assumes "distinct xs" "distinct ys" "set xs = set ys"
  obtains n where "rotate n ys ∈ set (cyc_permutations xs)"
proof (cases xs)
  case Nil with assms have "rotate 0 ys ∈ set (cyc_permutations xs)" by auto
  then show ?thesis ..
next
  case (Cons x xs')
  let ?ys' = "rotate (index ys x) ys"
  have "ys ≠ []" "x ∈ set ys"
    using Cons assms by auto
  then have "distinct ?ys' ∧ set xs = set ?ys' ∧ hd ?ys' = hd xs"
    using assms Cons by (auto simp add: hd_rotate_conv_nth)
  with ‹distinct xs› have "?ys' ∈ set (cyc_permutations xs)"
    by (rule in_set_cyc_permutations[THEN iffD2])
  then show ?thesis ..
qed

lemma list_succ_set_cyc_permutations:
  assumes "distinct xs" "xs ≠ []"
  shows "list_succ ` set (cyc_permutations xs) = {f. f permutes set xs ∧ cyclic_on f (set xs)}" (is "?L = ?R")
proof (intro set_eqI iffI)
  fix f assume "f ∈ ?L"
  moreover have "⋀ys. set xs = set ys ⟹ xs ≠ [] ⟹ ys ≠ []" by auto
  ultimately show "f ∈ ?R"
    using assms by (auto simp: in_set_cyc_permutations list_succ_permutes cyclic_on_list_succ)
next
  fix f assume "f ∈ ?R"
  then obtain ys where ys: "list_succ ys = f" "distinct ys" "set ys = set xs"
    by (auto elim: cyclic_on_obtain_list_succ')
  moreover
  with ‹distinct xs› obtain n where "rotate n ys ∈ set (cyc_permutations xs)"
    by (auto elim: in_set_cyc_permutations_obtain)
  then have "list_succ (rotate n ys) ∈ ?L" by simp
  ultimately
  show "f ∈ ?L" by simp
qed


subsection ‹Enumerating Permutations from List Orbits›

definition cyc_permutationss :: "'a list list ⇒ 'a list list list" where
  "cyc_permutationss = product_lists o map cyc_permutations"

lemma cyc_permutationss_Nil[simp]: "cyc_permutationss [] = [[]]"
  by (auto simp: cyc_permutationss_def)

lemma in_set_cyc_permutationss:
  assumes "distincts xss"
  shows "yss ∈ set (cyc_permutationss xss) ⟷ distincts yss ∧ map set xss = map set yss ∧ map hd xss = map hd yss"
proof -
  { assume A: "list_all2 (λx ys. x ∈ set ys) yss (map cyc_permutations xss)"
    then have "length yss = length xss" by (auto simp: list_all2_lengthD)
    then have "⋃(sset xss) = ⋃(sset yss)" "distincts yss" "map set xss = map set yss" "map hd xss = map hd yss"
      using A assms
      by (induct yss xss rule: list_induct2) (auto simp: distincts_Cons in_set_cyc_permutations)
  } note X = this
  { assume A: "distincts yss" "map set xss = map set yss" "map hd xss = map hd yss"
    then have "length yss = length xss" by (auto dest: map_eq_imp_length_eq)
    then have "list_all2 (λx ys. x ∈ set ys) yss (map cyc_permutations xss)"
      using A assms
      by (induct yss xss rule: list_induct2) (auto simp: distincts_Cons in_set_cyc_permutations)
  } note Y = this
  show "?thesis"
    unfolding cyc_permutationss_def
    by (auto simp: product_lists_set intro: X Y)
qed

lemma lists_succ_set_cyc_permutationss:
  assumes "distincts xss"
  shows "lists_succ ` set (cyc_permutationss xss) = {f. f permutes ⋃(sset xss) ∧ (∀c ∈ sset xss. cyclic_on f c)}" (is "?L = ?R")
  using assms
proof (intro set_eqI iffI)
  fix f assume "f ∈ ?L"
  then obtain yss where "yss ∈ set (cyc_permutationss xss)" "f = lists_succ yss" by (rule imageE)
  moreover
  from ‹yss ∈ _› assms have "set (map set xss) = set (map set yss)"
    by (auto simp: in_set_cyc_permutationss)
  then have "sset xss = sset yss" by simp
  ultimately
  show "f ∈ ?R"
    using assms
  by (auto simp: in_set_cyc_permutationss cyclic_on_lists_succ') (metis lists_succ_permutes)
next
  fix f assume "f ∈ ?R"
  then have "f permutes ⋃(sset xss)" "⋀cs. cs ∈ set xss ⟹ cyclic_on f (set cs)"
    by auto
  from this(1) refl assms this(2)
  obtain yss where "f = lists_succ yss" "distincts yss" "map set yss = map set xss" "map hd yss = map hd xss"
    by (rule cyclic_on_obtain_lists_succ)
  with assms show "f ∈ ?L" by (auto intro!: imageI simp: in_set_cyc_permutationss)
qed


subsection ‹Lists of Permutations›

definition permutationss :: "'a list list ⇒ 'a list list list" where
  "permutationss = product_lists o map permutations"

lemma permutationss_Nil[simp]: "permutationss [] = [[]]"
  by (auto simp: permutationss_def)

lemma permutationss_Cons:
  "permutationss (xs # xss) = concat (map (λys. map (Cons ys) (permutationss xss)) (permutations xs))"
  by (auto simp: permutationss_def)

lemma in_set_permutationss:
  assumes "distincts xss"
  shows "yss ∈ set (permutationss xss) ⟷ distincts yss ∧ map set xss = map set yss"
proof -
  { assume A: "list_all2 (λx ys. x ∈ set ys) yss (map permutations xss)"
    then have "length yss = length xss" by (auto simp: list_all2_lengthD)
    then have "⋃(sset xss) = ⋃(sset yss)" "distincts yss" "map set xss = map set yss"
      using A assms
      by (induct yss xss rule: list_induct2) (auto simp: distincts_Cons in_set_permutations)
  } note X = this
  { assume A: "distincts yss" "map set xss = map set yss"
    then have "length yss = length xss" by (auto dest: map_eq_imp_length_eq)
    then have "list_all2 (λx ys. x ∈ set ys) yss (map permutations xss)"
      using A assms
      by (induct yss xss rule: list_induct2) (auto simp: in_set_permutations distincts_Cons)
  } note Y = this
  show "?thesis"
    unfolding permutationss_def
    by (auto simp: product_lists_set intro: X Y)
qed

lemma set_permutationss:
  assumes "distincts xss"
  shows "set (permutationss xss) = {yss. distincts yss ∧ map set xss = map set yss}"
  using in_set_permutationss[OF assms] by blast

lemma permutationss_complete:
  assumes "distincts xss" "distincts yss" "xss ≠ []"
    and "set ` set xss = set ` set yss"
  shows "set yss ∈ set ` set (permutationss xss)"
proof -
  have "length xss = length yss"
    using assms by (simp add: length_distincts)
  from ‹sset xss = _›
  have "∃yss'. set yss' = set yss ∧ map set yss' = map set xss"
    using assms(1-2)
  proof (induct xss arbitrary: yss)
    case Nil then show ?case by simp
  next
    case (Cons xs xss)
    from ‹sset (xs # xss) = sset yss›
    obtain ys where ys: "ys ∈ set yss" "set ys = set xs"
      by auto (metis imageE insertI1)
    with ‹distincts yss› have "set ys ∉ sset (remove1 ys yss)"
      by (fastforce simp: distincts_def)
    moreover
    from ‹distincts (xs # xss)› have "set xs ∉ sset xss"
      by (fastforce simp: distincts_def)
    ultimately have "sset xss = sset (remove1 ys yss)"
      using ‹distincts yss› ‹sset (xs # xss) = sset yss›
      apply (auto simp: distincts_distinct ‹set ys = set xs›[symmetric])
      apply (smt Diff_insert_absorb ‹ys ∈ set yss› image_insert insert_Diff rev_image_eqI)
      by (metis ‹ys ∈ set yss› image_eqI insert_Diff insert_iff)
    then obtain yss' where "set yss' = set (remove1 ys yss) ∧ map set yss' = map set xss"
      using Cons by atomize_elim (auto simp: distincts_Cons distincts_remove1)
    then have "set (ys # yss') = set yss ∧ map set (ys # yss') = map set (xs # xss)"
      using ys set_remove1_eq ‹distincts yss› by (auto simp: distincts_distinct)
    then show ?case ..
  qed
  then obtain yss' where "set yss' = set yss" "map set yss' = map set xss" by blast
  then have "distincts yss'" using ‹distincts xss› ‹distincts yss›
    unfolding distincts_def
    by simp_all (metis ‹length xss = length yss› card_distinct distinct_card length_map)
  then have "set yss' ∈ set ` set (permutationss xss)"
    using ‹distincts xss› ‹map set yss' = _›
    by (auto simp: set_permutationss)
  then show ?thesis using ‹set yss' = _› by auto
qed

lemma permutations_complete: (* could generalize with multi-sets *)
  assumes "distinct xs" "distinct ys" "set xs = set ys"
  shows "ys ∈ set (permutations xs)"
  using assms
proof (induct "length xs" arbitrary: xs ys)
  case 0 then show ?case by simp
next
  case (Suc n)
  from Suc.hyps have "xs ≠ []" by auto
  then obtain y ys' where [simp]: "ys = y # ys'" "y ∈ set xs" using Suc.prems by (cases ys) auto
  have "ys' ∈ set (permutations (remove1 y xs))"
    using Suc.prems ‹Suc n = _› by (intro Suc.hyps) (simp_all add: length_remove1 )
  then show ?case using ‹xs ≠ []› by (auto simp: set_permutations_step)
qed


end