Theory Topological_Sortings_Rankings

subsection ‹Topological sorting›
theory Topological_Sortings_Rankings
  imports Rankings
begin

text ‹
  The following returns the set of all rankings of the given set ‹A› that are extensions of the
  given relation ‹R›, i.e.\ all topological sortings of ‹R›.

  Note that there are no requirements about ‹R›; in particular it does not have to be reflexive,
  antisymmetric, or transitive. If it is not antisymmetric or not transitive, the result set will
  simply be empty.
›

function topo_sorts :: "'a set ⇒ 'a relation ⇒ 'a list set" where
  "topo_sorts A R =
     (if infinite A then {} else if A = {} then {[]} else
      ⋃x∈{x∈A. ∀z∈A. R x z ⟶ z = x}. (λxs. x # xs) ` topo_sorts (A - {x}) (λy z. R y z ∧ y ≠ x ∧ z ≠ x))"
  by auto
termination
proof (relation "Wellfounded.measure (card ∘ fst)", goal_cases)
  case (2 A R x)
  show ?case
  proof (cases "infinite A ∨ A = {}")
    case False
    have "A - {x} ⊂ A"
      using 2 by auto
    with False have "card (A - {x}) < card A"
      by (intro psubset_card_mono) auto
    thus ?thesis
      using False 2 by simp
  qed (use 2 in auto)
qed auto

lemmas [simp del] = topo_sorts.simps

lemma topo_sorts_empty [simp]: "topo_sorts {} R = {[]}"
  by (subst topo_sorts.simps) auto

lemma topo_sorts_infinite: "infinite A ⟹ topo_sorts A R = {}"
  by (subst topo_sorts.simps) auto

lemma topo_sorts_rec:
  "finite A ⟹ A ≠ {} ⟹ 
     topo_sorts A R = (⋃x∈{x∈A. ∀z∈A. R x z ⟶ z = x}. 
       (λxs. x # xs) ` topo_sorts (A - {x}) (λy z. R y z ∧ y ≠ x ∧ z ≠ x))"
  by (subst topo_sorts.simps) simp_all

lemma topo_sorts_cong [cong]:
  assumes "A = B" "⋀x y. x ∈ A ⟹ y ∈ B ⟹ x ≠ y ⟹ R x y = R' x y"
  shows   "topo_sorts A R = topo_sorts B R'"
proof (cases "finite A")
  case True
  from this and assms(2) show ?thesis
    unfolding assms(1)[symmetric]
  proof (induction arbitrary: R R' rule: finite_psubset_induct)
    case (psubset A R R')
    show ?case
    proof (cases "A = {}")
      case False
      have "(⋃x∈{x ∈ A. ∀z∈A. R x z ⟶ z = x}. (#) x ` topo_sorts (A - {x}) (λy z. R y z ∧ y ≠ x ∧ z ≠ x)) =
            (⋃x∈{x ∈ A. ∀z∈A. R' x z ⟶ z = x}. (#) x ` topo_sorts (A - {x}) (λy z. R' y z ∧ y ≠ x ∧ z ≠ x))"
        using psubset.prems psubset.hyps
        by (intro arg_cong[of _ _ "⋃"] image_cong refl psubset.IH) auto
      thus ?thesis
        by (subst (1 2) topo_sorts_rec) (use False psubset.hyps in simp_all)
    qed auto
  qed
qed (simp_all add: assms(1) topo_sorts_infinite)

lemma topo_sorts_correct:
  assumes "⋀x y. R x y ⟹ x ∈ A ∧ y ∈ A"
  shows   "topo_sorts A R = {xs∈permutations_of_set A. R ≤ of_ranking xs}"
  using assms
proof (induction A R rule: topo_sorts.induct)
  case (1 A R)
  note R = "1.prems"

  show ?case
  proof (cases "A = {} ∨ infinite A")
    case True
    thus ?thesis using R
      by (auto simp: topo_sorts_infinite permutations_of_set_infinite)
  next
    case False
    define M where "M = {x∈A. ∀z∈A. R x z ⟶ z = x}"
    define R' where "R' = (λx y z. R y z ∧ y ≠ x ∧ z ≠ x)"

    have IH: "topo_sorts (A - {x}) (R' x) = {xs ∈ permutations_of_set (A - {x}). (R' x) ≤ of_ranking xs}"
      if x: "x ∈ M" for x
      unfolding R'_def by (rule "1.IH") (use False x R in ‹auto simp: M_def›)

    have "{xs∈permutations_of_set A. R ≤ of_ranking xs} =
            (⋃x∈A. ((#) x) ` {xs ∈ permutations_of_set (A - {x}). R ≤ of_ranking (x # xs)})"
      by (subst permutations_of_set_nonempty) (use False in auto)
    also have "… = (⋃x∈A. ((#) x) ` {xs ∈ permutations_of_set (A - {x}). x ∈ M ∧ R' x ≤ of_ranking xs})"
    proof (intro arg_cong[of _ _ "⋃"] image_cong Collect_cong conj_cong refl)
      fix x xs
      assume x: "x ∈ A" and xs: "xs ∈ permutations_of_set (A - {x})"
      from xs have xs': "set xs = A - {x}" "distinct xs"
        by (auto simp: permutations_of_set_def)

      have "R ≤ of_ranking (x # xs) ⟷ (∀y z. R y z ⟶ z = x ∧ y ∈ set (x # xs) ∨ of_ranking xs y z)"
        unfolding le_fun_def of_ranking_Cons by auto
      also have "(λy z. R y z ⟶ z = x ∧ y ∈ set (x # xs) ∨ of_ranking xs y z) =
                 (λy z. R y z ⟶ ((y = x ⟶ z = x) ∧ (y ≠ x ∧ z ≠ x ⟶ of_ranking xs y z)))"
        unfolding fun_eq_iff using R of_ranking_altdef' xs'(1,2) by fastforce
      also have "(∀y z. … y z) ⟷ (∀z. R x z ⟶ z = x) ∧ R' x ≤ of_ranking xs"
        unfolding le_fun_def of_ranking_Cons R'_def by auto
      also have "(∀z. R x z ⟶ z = x) ⟷ x ∈ M"
        unfolding M_def using x R by auto
      finally show "(R ≤ of_ranking (x # xs)) = (x ∈ M ∧ R' x ≤ of_ranking xs)" .
    qed
    also have "… = (⋃x∈M. ((#) x) ` {xs∈permutations_of_set (A - {x}). R' x ≤ of_ranking xs})"
      unfolding M_def by blast
    also have "… = (⋃x∈M. ((#) x) ` topo_sorts (A - {x}) (R' x))"
      using IH by blast
    also have "… = topo_sorts A R"
      unfolding R'_def M_def using False by (subst (2) topo_sorts_rec) simp_all
    finally show ?thesis ..
  qed
qed

lemma topo_sorts_nonempty:
  assumes "finite A" "⋀x y. R x y ⟹ x ∈ A ∧ y ∈ A" "⋀x y. R x y ⟹ ¬R y x" "transp R"
  shows   "topo_sorts A R ≠ {}"
  using assms
proof (induction A R rule: topo_sorts.induct)
  case (1 A R)
  define R' where "R' = (λx y. x ∈ A ∧ y ∈ A ∧ x = y ∨ R x y)"
  interpret R': order_on A R' 
    by standard (use "1.prems"(2,3) in ‹auto simp: R'_def intro: transpD[OF ‹transp R›]›)

  show ?case
  proof (cases "A = {}")
    case False
    define M where "M = Max_wrt_among R' A"
    have "M ≠ {}"
      unfolding M_def by (rule R'.Max_wrt_among_nonempty) (use False ‹finite A› in simp_all)
    obtain x where x: "x ∈ M"
      using ‹M ≠ {}› by blast
    have M_altdef: "M = {x∈A. ∀z∈A. R x z ⟶ z = x}"
      unfolding M_def Max_wrt_among_def R'_def using "1.prems" by blast

    define L where "L = topo_sorts (A - {x}) (λy z. R y z ∧ y ≠ x ∧ z ≠ x)"
    have "L ≠ {}"
      unfolding L_def
    proof (rule "1.IH")
      show "transp (λa b. R a b ∧ a ≠ x ∧ b ≠ x)"
        using ‹transp R› unfolding transp_def by blast
    qed (use "1.prems"(2,3) False x ‹finite A› in ‹auto simp: M_altdef›)

    have "topo_sorts A R = 
            (⋃x∈{x∈A. ∀z∈A. R x z ⟶ z = x}. 
              (λxs. x # xs) ` topo_sorts (A - {x}) (λy z. R y z ∧ y ≠ x ∧ z ≠ x))"
      by (subst topo_sorts.simps) (use False ‹finite A› in simp_all)
    also have "{x∈A. ∀z∈A. R x z ⟶ z = x} = M"
      unfolding M_altdef ..
    finally show "topo_sorts A R ≠ {}"
      using ‹L ≠ {}› ‹x ∈ M› unfolding L_def by blast
  qed auto
qed

lemma bij_betw_topo_sorts_linorders_on:
  assumes "⋀x y. R x y ⟹ x ∈ A ∧ y ∈ A"
  shows   "bij_betw of_ranking (topo_sorts A R) {R'. finite_linorder_on A R' ∧ R ≤ R'}"
proof -
  have "bij_betw of_ranking {xs∈permutations_of_set A. R ≤ of_ranking xs}
          {R'∈{R'. finite_linorder_on A R'}. R ≤ R'}"
    using bij_betw_permutations_of_set_finite_linorders_on
    by (rule bij_betw_Collect) auto
  also have "{xs∈permutations_of_set A. R ≤ of_ranking xs} = topo_sorts A R"
    by (subst topo_sorts_correct) (use assms in auto)
  finally show ?thesis
    by simp
qed


text ‹
  In the following, we give a more convenient formulation of this for computation. 

  The input is a relation represented as a list of pairs $(x, \textit{ys})$ where $\textit{ys}$ 
  is the set of all elements such that $(x,y)$ is in the relation.
›

function topo_sorts_aux :: "('a × 'a set) list ⇒ 'a list list" where
  "topo_sorts_aux xs =
     (if xs = [] then [[]] else
      List.bind (map fst (filter (λ(_,ys). ys = {}) xs))
        (λx. map ((#) x) (topo_sorts_aux 
          (map (map_prod id (Set.filter (λy. y ≠ x))) (filter (λ(y,_). y ≠ x) xs)))))"
  by auto
termination
  by (relation "Wellfounded.measure length")
     (auto simp: length_filter_less)

lemmas [simp del] = topo_sorts_aux.simps

lemma topo_sorts_aux_Nil [simp]: "topo_sorts_aux [] = [[]]"
  by (subst topo_sorts_aux.simps) auto

lemma topo_sorts_aux_rec:
  "xs ≠ [] ⟹ topo_sorts_aux xs =
     List.bind (map fst (filter (λ(_,ys). ys = {}) xs))
        (λx. map ((#) x) (topo_sorts_aux 
          (map (map_prod id (Set.filter (λy. y ≠ x))) (filter (λ(y,_). y ≠ x) xs))))"
  by (subst topo_sorts_aux.simps) auto

lemma topo_sorts_aux_Cons:
  "topo_sorts_aux (y#xs) =
     List.bind (map fst (filter (λ(_,ys). ys = {}) (y#xs)))
        (λx. map ((#) x) (topo_sorts_aux 
          (map (map_prod id (Set.filter (λy. y ≠ x))) (filter (λ(y,_). y ≠ x) (y#xs)))))"
  by (rule topo_sorts_aux_rec) auto

lemma set_topo_sorts_aux:
  assumes "distinct (map fst xs)"
  assumes "⋀x ys. (x, ys) ∈ set xs ⟹ ys ⊆ set (map fst xs) - {x}"
  shows   "set (topo_sorts_aux xs) = 
             topo_sorts (set (map fst xs)) (λx y. ∃ys. (x, ys) ∈ set xs ∧ y ∈ ys)"
  using assms
proof (induction xs rule: topo_sorts_aux.induct)
  case (1 xs)
  show ?case
  proof (cases "xs = []")
    case True
    thus ?thesis
      by (simp add: topo_sorts.simps[of "{}"] topo_sorts_aux.simps[of "[]"])
  next
    case False
    define M where "M = set (map fst (filter (λ(_,ys). ys = {}) xs))"
    define xs' where "xs' = (λx. map (map_prod id (Set.filter (λy. y ≠ x))) (filter (λ(y,_). y ≠ x) xs))"
    define R' where "R' = (λx a b. ∃ys. (a, ys) ∈ set (xs' x) ∧ b ∈ ys)"

    have IH: "set (topo_sorts_aux (xs' x)) = topo_sorts (set (map fst (xs' x))) (R' x)"
      if "x ∈ M" for x
      unfolding xs'_def R'_def
    proof (rule "1.IH", goal_cases)
      case 2
      show ?case using that by (auto simp: M_def)
    next
      case 3
      thus ?case using "1.prems"
        by (auto intro!: distinct_filter simp: distinct_map intro: inj_on_subset)
    next
      case 4
      thus ?case using "1.prems" by fastforce
    qed fact+

    have "topo_sorts (set (map fst xs)) (λx y. ∃ys. (x, ys) ∈ set xs ∧ y ∈ ys) =
            (⋃x∈{x ∈ set (map fst xs). ∀z∈set (map fst xs). (∃ys. (x, ys) ∈ set xs ∧ z ∈ ys) ⟶ z = x}.
               (#) x ` topo_sorts (set (map fst xs) - {x}) (λy z. (∃ys. (y, ys) ∈ set xs ∧ z ∈ ys) ∧ y ≠ x ∧ z ≠ x))"
      by (subst topo_sorts_rec) (use False in simp_all)
    also have "{x ∈ set (map fst xs). ∀z∈set (map fst xs). (∃ys. (x, ys) ∈ set xs ∧ z ∈ ys) ⟶ z = x} = M"
      (is "?lhs = ?rhs")
    proof (intro equalityI subsetI)
      fix x assume "x ∈ ?rhs"
      thus "x ∈ ?lhs"
        using "1.prems" by (fastforce simp: M_def distinct_map inj_on_def)
    next
      fix x assume "x ∈ ?lhs"
      hence x: "x ∈ set (map fst xs)" "⋀z ys. z ∈ set (map fst xs) ⟹ (x, ys) ∈ set xs ∧ z ∈ ys ⟹ z = x"
        by blast+
      from x(1) obtain ys where ys: "(x, ys) ∈ set xs"
        by force
      have "ys ⊆ {}"
      proof
        fix y assume "y ∈ ys"
        with ys show "y ∈ {}"
          using x(2)[of y ys] "1.prems" by auto
      qed
      thus "x ∈ ?rhs"
        unfolding M_def using x(1) ys by (auto simp: image_iff)
    qed
    also have "(λx. set (map fst xs) - {x}) = (λx. set (map fst (xs' x)))"
      by (force simp: xs'_def fun_eq_iff)
    also have "(λx y z. (∃ys. (y, ys) ∈ set xs ∧ z ∈ ys) ∧ y ≠ x ∧ z ≠ x) = R'"
      unfolding R'_def using "1.prems"
      by (auto simp: fun_eq_iff distinct_map inj_on_def xs'_def map_prod_def
                           case_prod_unfold image_iff)
    also have "(⋃x∈M. (#) x ` topo_sorts (set (map fst (xs' x))) (R' x)) =
               (⋃x∈M. (#) x ` set (topo_sorts_aux (xs' x)))"
      using IH by blast
    also have "… = set (topo_sorts_aux xs)"
      by (subst (2) topo_sorts_aux_rec) (use False in ‹auto simp: M_def xs'_def List.bind_def›)
    finally show ?thesis ..
  qed
qed

lemma topo_sorts_code [code]:
  "topo_sorts (set xs) R = (let xs' = remdups xs in
     set (topo_sorts_aux (map (λx. (x, set (filter (λy. y ≠ x ∧ R x y) xs'))) xs')))"
proof -
  define xs' where "xs' = remdups xs"
  have "set (topo_sorts_aux (map (λx. (x, set (filter (λy. y ≠ x ∧ R x y) xs'))) xs')) = 
        topo_sorts (set xs) (λx y. ∃ys. (x, ys) ∈ (λx. (x, set (filter (λy. y ≠ x ∧ R x y) xs'))) ` set xs' ∧ y ∈ ys)"
    by (subst set_topo_sorts_aux) (auto simp: o_def xs'_def)
  also have "(λx y. ∃ys. (x, ys) ∈ (λx. (x, set (filter (λy. y ≠ x ∧ R x y) xs'))) ` set xs' ∧ y ∈ ys) =
             (λx y. x ∈ set xs ∧ y ∈ set xs ∧ x ≠ y ∧ R x y)"
    by (auto simp: xs'_def image_iff)
  also have "topo_sorts (set xs) … = topo_sorts (set xs) R"
    by (rule topo_sorts_cong) auto
  finally show ?thesis
    by (simp add: Let_def xs'_def)
qed

end