Theory Roy_Floyd_Warshall

theory Roy_Floyd_Warshall
imports Main
begin

section ‹Transitive closure algorithm›

text ‹
  The Roy-Floyd-Warshall algorithm takes a finite relation as input and
  produces its transitive closure as output. It iterates over all elements of
  the field of the relation and maintains a cumulative approximation of the
  result: step ‹0› starts with the original relation, and step ‹Suc n›
  connects all paths over the intermediate element ‹n›. The final
  approximation coincides with the full transitive closure.

  This algorithm is often named after ``Floyd'', ``Warshall'', or
  ``Floyd-Warshall'', but the earliest known description is due to B. Roy
  \<^cite>‹"Roy:1959"›.

  ┉
  Subsequently we use a direct mathematical model of the relation, bypassing
  matrices and arrays that are usually seen in the literature. This is more
  efficient for sparse relations: only the adjacency for immediate
  predecessors and successors needs to be maintained, not the square of all
  possible combinations. Moreover we do not have to worry about mutable data
  structures in a multi-threaded environment. See also the graph
  implementation in the Isabelle sources @{file
  ‹$ISABELLE_HOME/src/Pure/General/graph.ML›} and @{file
  ‹$ISABELLE_HOME/src/Pure/General/graph.scala›}.
›

type_synonym relation = "(nat × nat) set"

fun steps :: "relation ⇒ nat ⇒ relation"
where
  "steps rel 0 = rel"
| "steps rel (Suc n) =
    steps rel n ∪ {(x, y). (x, n) ∈ steps rel n ∧ (n, y) ∈ steps rel n}"


text ‹Implementation view on the relation:›

definition preds :: "relation ⇒ nat ⇒ nat set"
  where "preds rel y = {x. (x, y) ∈ rel}"

definition succs :: "relation ⇒ nat ⇒ nat set"
  where "succs rel x = {y. (x, y) ∈ rel}"

lemma
  "steps rel (Suc n) =
    steps rel n ∪ {(x, y). x ∈ preds (steps rel n) n ∧ y ∈ succs (steps rel n) n}"
  by (simp add: preds_def succs_def)

text ‹
  The main function requires an upper bound for the iteration, which is left
  unspecified here (via Hilbert's choice).
›

definition is_bound :: "relation ⇒ nat ⇒ bool"
  where "is_bound rel n ⟷ (∀m ∈ Field rel. m < n)"

definition "transitive_closure rel = steps rel (SOME n. is_bound rel n)"


section ‹Correctness proof›

subsection ‹Miscellaneous lemmas›

lemma finite_bound:
  assumes "finite rel"
  shows "∃n. is_bound rel n"
  using assms
proof induct
  case empty
  then show ?case by (simp add: is_bound_def)
next
  case (insert p rel)
  then obtain n where n: "∀m ∈ Field rel. m < n"
    unfolding is_bound_def by blast
  obtain x y where "p = (x, y)" by (cases p)
  then have "∀m ∈ Field (insert p rel). m < max (Suc x) (max (Suc y) n)"
    using n by auto
  then show ?case
    unfolding is_bound_def by blast
qed

lemma steps_Suc: "(x, y) ∈ steps rel (Suc n) ⟷
  (x, y) ∈ steps rel n ∨ (x, n) ∈ steps rel n ∧ (n, y) ∈ steps rel n"
  by auto

lemma steps_cases:
  assumes "(x, y) ∈ steps rel (Suc n)"
  obtains (copy) "(x, y) ∈ steps rel n"
    | (step) "(x, n) ∈ steps rel n" and "(n, y) ∈ steps rel n"
  using assms by auto

lemma steps_rel: "(x, y) ∈ rel ⟹ (x, y) ∈ steps rel n"
  by (induct n) auto


subsection ‹Bounded closure›

text ‹
  The bounded closure connects all transitive paths over elements below a
  given bound. For an upper bound of the relation, this coincides with the
  full transitive closure.
›

inductive_set Clos :: "relation ⇒ nat ⇒ relation"
  for rel :: relation and n :: nat
where
  base: "(x, y) ∈ Clos rel n" if "(x, y) ∈ rel"
| step: "(x, y) ∈ Clos rel n" if "(x, z) ∈ Clos rel n" and "(z, y) ∈ Clos rel n" and "z < n"

theorem Clos_closure:
  assumes "is_bound rel n"
  shows "(x, y) ∈ Clos rel n ⟷ (x, y) ∈ rel⇧+"
proof
  show "(x, y) ∈ rel⇧+" if "(x, y) ∈ Clos rel n"
    using that by induct simp_all
  show "(x, y) ∈ Clos rel n" if "(x, y) ∈ rel⇧+"
    using that
  proof (induct rule: trancl_induct)
    case (base y)
    then show ?case by (rule Clos.base)
  next
    case (step y z)
    from ‹(y, z) ∈ rel› have 1: "(y, z) ∈ Clos rel n" by (rule base)
    from ‹(y, z) ∈ rel› and ‹is_bound rel n› have 2: "y < n"
      unfolding is_bound_def Field_def by blast
    from step(3) 1 2 show ?case by (rule Clos.step)
  qed
qed

lemma Clos_Suc:
  assumes "(x, y) ∈ Clos rel n"
  shows "(x, y) ∈ Clos rel (Suc n)"
  using assms by induct (auto intro: Clos.intros)

text ‹
  In each step of the algorithm the approximated relation is exactly the
  bounded closure.
›

theorem steps_Clos_equiv: "(x, y) ∈ steps rel n ⟷ (x, y) ∈ Clos rel n"
proof (induct n arbitrary: x y)
  case 0
  show ?case
  proof
    show "(x, y) ∈ Clos rel 0" if "(x, y) ∈ steps rel 0"
    proof -
      from that have "(x, y) ∈ rel" by simp
      then show ?thesis by (rule Clos.base)
    qed
    show "(x, y) ∈ steps rel 0" if "(x, y) ∈ Clos rel 0"
      using that by cases simp_all
  qed
next
  case (Suc n)
  show ?case
  proof
    show "(x, y) ∈ Clos rel (Suc n)" if "(x, y) ∈ steps rel (Suc n)"
      using that
    proof (cases rule: steps_cases)
      case copy
      with Suc(1) have "(x, y) ∈ Clos rel n" ..
      then show ?thesis by (rule Clos_Suc)
    next
      case step
      with Suc have "(x, n) ∈ Clos rel n" and "(n, y) ∈ Clos rel n"
        by simp_all
      then have "(x, n) ∈ Clos rel (Suc n)" and "(n, y) ∈ Clos rel (Suc n)"
        by (simp_all add: Clos_Suc)
      then show ?thesis by (rule Clos.step) simp
    qed
    show "(x, y) ∈ steps rel (Suc n)" if "(x, y) ∈ Clos rel (Suc n)"
      using that
    proof induct
      case (base x y)
      then show ?case by (simp add: steps_rel)
    next
      case (step x z y)
      with Suc show ?case
        by (auto simp add: steps_Suc less_Suc_eq intro: Clos.step)
    qed
  qed
qed


subsection ‹Main theorem›

text ‹
  The main theorem follows immediately from the key observations above. Note
  that the assumption of finiteness gives a bound for the iteration, although
  the details are left unspecified. A concrete implementation could choose the
  the maximum element + 1, or iterate directly over the data structures for
  the @{term preds} and @{term succs} implementation.
›

theorem transitive_closure_correctness:
  assumes "finite rel"
  shows "transitive_closure rel = rel⇧+"
proof -
  let ?N = "SOME n. is_bound rel n"
  have is_bound: "is_bound rel ?N"
    by (rule someI_ex) (rule finite_bound [OF ‹finite rel›])
  have "(x, y) ∈ steps rel ?N ⟷ (x, y) ∈ rel⇧+" for x y
  proof -
    have "(x, y) ∈ steps rel ?N ⟷ (x, y) ∈ Clos rel ?N"
      by (rule steps_Clos_equiv)
    also have "… ⟷ (x, y) ∈ rel⇧+"
      using is_bound by (rule Clos_closure)
    finally show ?thesis .
  qed
  then show ?thesis unfolding transitive_closure_def by auto
qed


section ‹Alternative formulation›

text ‹
  The core of the algorithm may be expressed more declaratively as follows,
  using an inductive definition to imitate a logic-program. This is equivalent
  to the function specification @{term steps} from above.
›

inductive Steps :: "relation ⇒ nat ⇒ nat × nat ⇒ bool"
  for rel :: relation
where
  base: "Steps rel 0 (x, y)" if "(x, y) ∈ rel"
| copy: "Steps rel (Suc n) (x, y)" if "Steps rel n (x, y)"
| step: "Steps rel (Suc n) (x, y)" if "Steps rel n (x, n)" and "Steps rel n (n, y)"

lemma steps_equiv: "(x, y) ∈ steps rel n ⟷ Steps rel n (x, y)"
proof
  show "Steps rel n (x, y)" if "(x, y) ∈ steps rel n"
    using that
  proof (induct n arbitrary: x y)
    case 0
    then have "(x, y) ∈ rel" by simp
    then show ?case by (rule base)
  next
    case (Suc n)
    from Suc(2) show ?case
    proof (cases rule: steps_cases)
      case copy
      with Suc(1) have "Steps rel n (x, y)" .
      then show ?thesis by (rule Steps.copy)
    next
      case step
      with Suc(1) have "Steps rel n (x, n)" and "Steps rel n (n, y)"
        by simp_all
      then show ?thesis by (rule Steps.step)
    qed
  qed
  show "(x, y) ∈ steps rel n" if "Steps rel n (x, y)"
    using that by induct simp_all
qed

end