Theory Containers_DFS_Ex

(* Title:      Containers/Examples/Containers_DFS_Ex.thy
   Author:     Andreas Lochbihler, ETH Zurich *)

section ‹Formalisation of depth-first search using Containers›

theory Containers_DFS_Ex imports
  "../Containers"
  "HOL-Library.Transitive_Closure_Table"
begin

subsection ‹Auxiliary stuff›

definition restrict :: "('a × 'a) set ⇒ 'a set ⇒ ('a × 'a) set" (infixl "↿" 60)
where "R ↿ A = {(a, b) ∈ R. b ∈ A}"

lemma in_restrict [iff]: "(a, b) ∈ R ↿ A ⟷ (a, b) ∈ R ∧ b ∈ A"
by(simp add: restrict_def)

lemma restrict_UNIV [simp]: "R ↿ UNIV = R"
by auto

lemma restrict_restrict [simp]: "R ↿ A ↿ B = R ↿ (A ∩ B)"
by auto

lemma rtrancl_restrict_reachable:
  assumes x: "(x, y) ∈ R⇧*"
  and z: "(z, y) ∉ R⇧*"
  shows "(x, y) ∈ (R ↿ - R⇧* `` {z})⇧*"
using x
proof(induction rule: converse_rtrancl_induct)
  case (step x x')
  from ‹(x, x') ∈ R› z ‹(x', y) ∈ R⇧*›
  have "(x, x') ∈ R ↿ - R⇧* `` {z}" by(auto intro: rtrancl_trans converse_rtrancl_into_rtrancl)
  thus ?case using step.IH by(rule converse_rtrancl_into_rtrancl)
qed simp

lemma rtrancl_restrict_start:
  assumes "(x, y) ∈ R⇧*"
  shows "(x, y) ∈ (R ↿ - {x})⇧*"
proof -
  let ?R = "λx y. (x, y) ∈ R"
  define z where "z ≡ x"
  with assms obtain xs where "rtrancl_path ?R x xs y" "z ∉ set xs"
    by(auto simp add: rtrancl_def rtranclp_eq_rtrancl_path elim: rtrancl_path_distinct)
  thus "(x, y) ∈ (R ↿ - {z})⇧*"
    by induction(auto intro: converse_rtrancl_into_rtrancl)
qed

lemma (in comp_fun_commute) fold_set_union_disj: (* Move to distribution *)
  assumes "finite A" "finite B" "A ∩ B = {}"
  shows "Finite_Set.fold f z (A ∪ B) = Finite_Set.fold f (Finite_Set.fold f z A) B"
using assms(2,1,3) by induction simp_all

lemma Image_insert [simp]:
  fixes A :: "'a set"
  assumes "NO_MATCH ({} :: 'a set) A"
  shows "R `` insert x A = R `` {x} ∪ (R `` A)"
by(auto)

subsection ‹Declarative definition›

datatype 'a dfs_result = is_Reachable: Reachable | Visited "'a set"

context fixes E :: "('a × 'a) set" begin

definition reachable :: "'a => 'a => bool"
where "reachable src tgt ⟷ (src, tgt) ∈ E⇧*"

text ‹
  We avoid the non-determinism of visited nodes in depth-first search by only returning
  the set of visited nodes when the search fails, because in that case it contains all reachable
  nodes and therefore is deterministic again.
›

definition dfs :: "'a ⇒ 'a ⇒ 'a set ⇒ 'a dfs_result"
where 
  "dfs src tgt visited =
  (if tgt ∈ (E ↿ - visited)⇧* `` {src} then Reachable else Visited (visited ∪ (E ↿ - visited)⇧* `` {src}))"

subsection ‹Derivation of the recursion equation›

context
  fixes tgt :: 'a and loop
  defines "loop ≡ λx r. case r of Reachable ⇒ Reachable | Visited 𝒱 ⇒ 
    if x ∈ 𝒱 then Visited 𝒱 else dfs x tgt 𝒱"
begin

private lemma loop_simps:
  "loop x Reachable = Reachable"
  "loop x (Visited 𝒱) = (if x ∈ 𝒱 then Visited 𝒱 else dfs x tgt 𝒱)"
by(simp_all add: loop_def)

context notes [simp] = loop_simps begin

lemma comp_fun_commute_dfs_body: "comp_fun_commute loop"
by(unfold_locales)(auto simp add: loop_def dfs_def fun_eq_iff intro: rtrancl_mono[THEN subsetD, rotated] rtrancl_trans dest: rtrancl_restrict_reachable split: dfs_result.split)

interpretation f: comp_fun_commute loop
by(rule comp_fun_commute_dfs_body)

lemma fold_dfs_Reachable [simp]:
  "Finite_Set.fold loop Reachable A = Reachable"
proof(cases "finite A")
  case True thus ?thesis by(induction) auto
qed simp

lemma dfs_blocked:
  assumes "finite A"
  and "E `` A ⊆ visited" "tgt ∉ A"
  shows "Finite_Set.fold loop (Visited visited) A = Visited (A ∪ visited)"
using assms by induction(auto elim: converse_rtranclE simp add: dfs_def)

lemma dfs_visited:
  assumes "finite A"
  and "A ⊆ visited"
  shows "Finite_Set.fold loop (Visited visited) A = Visited visited"
using assms by induction(auto)

lemma dfs_rec:
  "dfs src tgt visited =
  (if src = tgt then Reachable
   else let succs = E `` {src} in if finite succs then Finite_Set.fold loop (Visited (insert src visited)) succs
   else Code.abort (STR ''infinite successor relation'') (λ_. dfs src tgt visited))"
proof(cases "src ≠ tgt ∧ finite (E `` {src})")
  case False
  thus ?thesis by(auto simp add: dfs_def)
next
  case True
  hence [simp]: "src ≠ tgt" "tgt ≠ src"
    and fin: "finite (E `` {src})" by auto

  show ?thesis
  proof(cases "(src, tgt) ∈ (E ↿ - visited)⇧*")
    case True
    let ?g = "λx y. (x, y) ∈ E ↿ - visited"
    have "Finite_Set.fold loop (Visited (insert src visited)) (E `` {src}) = 
      Finite_Set.fold loop (Finite_Set.fold loop (Visited (insert src visited)) (E `` {src} - insert src visited)) (E `` {src} ∩ insert src visited)"
      using fin by(subst f.fold_set_union_disj[symmetric])(auto intro: arg_cong2[where f="Finite_Set.fold loop"])
    also from True obtain xs where "rtrancl_path ?g src xs tgt" "distinct (src # xs)"
      by(auto simp add: rtrancl_def rtranclp_eq_rtrancl_path elim: rtrancl_path_distinct)
    hence "Finite_Set.fold loop (Visited (insert src visited)) (E `` {src} - insert src visited) = Reachable"
      using ‹src ≠ tgt› fin
    proof(induction src xs z≡tgt)
      case (step x y xs)
      let ?succs = "E `` {x} - visited - {y,x}"
    
      have "Finite_Set.fold loop (Visited (insert x visited)) (insert y ?succs) =
            Finite_Set.fold loop (loop y (Visited (insert x visited))) ?succs"
        by(rule f.fold_insert2)(simp_all add: ‹finite (E `` {x})›)
      also
      from ‹distinct (x # y # xs)› have "x ∉ set (y # xs)" by simp
      with ‹rtrancl_path ?g y xs tgt›
      have "(y, tgt) ∈ (E ↿ - insert x visited)⇧*"
        by induction(auto intro: converse_rtrancl_into_rtrancl)
      with ‹(x, y) ∈ E ↿ - visited› have "loop y (Visited (insert x visited)) = Reachable" 
        using ‹x ∉ set (y # xs)› by(auto simp add: dfs_def)
      also from ‹(x, y) ∈ E ↿ - visited›
      have "insert y ?succs = E `` {x} - insert x visited"
        using ‹distinct (x # y # xs)› by auto
      finally show ?case by simp
    qed simp
    finally show ?thesis using True by(simp add: dfs_def Let_def)
  next
    case False
    have "Finite_Set.fold loop (Visited (insert src visited)) (E `` {src}) = 
      Finite_Set.fold loop (Finite_Set.fold loop (Visited (insert src visited)) (E `` {src} - insert src visited)) (E `` {src} ∩ insert src visited)"
      using fin by(subst f.fold_set_union_disj[symmetric])(auto intro: arg_cong2[where f="Finite_Set.fold loop"])
    also from fin have "finite (E `` {src} - visited)" by simp
    then have "Finite_Set.fold loop (Visited (insert src visited)) (E `` {src} - insert src visited) = Visited (visited ∪ (E ↿ - visited)⇧* `` {src})"
      using False
    proof(induct A≡"E `` {src} - visited" arbitrary: visited rule: finite_psubset_induct)
      case psubset
      note fin = ‹finite (E `` {src})›
      note src_tgt = ‹(src, tgt) ∉ (E ↿ - visited)⇧*›
      show ?case
      proof (cases "E `` {src} - insert src visited = {}")
        case True
        { let ?g = "λx y. (x, y) ∈ E ↿ - visited"
          fix x
          assume "(src, x) ∈ (E ↿ - visited)⇧*"
          then obtain xs where "rtrancl_path ?g src xs x" "distinct (src # xs)"
            by(auto simp add: rtrancl_def rtranclp_eq_rtrancl_path elim: rtrancl_path_distinct)
          hence "src = x" using True by induction auto }
        then show ?thesis unfolding True using True
          by(auto elim: converse_rtranclE)
      next
        case False
        then obtain y where y: "y ∈ E `` {src}" "y ∉ visited" "y ≠ src" by auto
        let ?succs = "E `` {src} - insert src visited - {y}"
        let ?visited = "insert src visited"
        let ?visited' = "?visited ∪ (E ↿ - insert src visited)⇧* `` {y}"
        have "Finite_Set.fold loop (Visited ?visited) (insert y ?succs) =
              Finite_Set.fold loop (loop y (Visited ?visited)) ?succs"
          by(rule f.fold_insert2)(simp_all add: fin)
        also have y_tgt: "(y, tgt) ∉ (E ↿ - ?visited)⇧*" using y src_tgt
          by(auto intro: converse_rtrancl_into_rtrancl rtrancl_mono[THEN subsetD, rotated])
        hence "loop y (Visited (insert src visited)) = Visited ?visited'"
          using y by(auto simp add: dfs_def)
        also define A where "A ≡ ?succs ∩ (E ↿ - insert src visited)⇧* `` {y}"
        have "?succs = A ∪ (E `` {src} - insert src ?visited')" unfolding A_def using y by auto
        hence "Finite_Set.fold loop (Visited ?visited') ?succs =
               Finite_Set.fold loop (Visited ?visited') …" by simp
        also have "… = Finite_Set.fold loop (Finite_Set.fold loop (Visited ?visited') A) (E `` {src} - insert src ?visited')"
          by(rule f.fold_set_union_disj)(auto simp add: A_def intro: finite_subset[OF _ fin])
        also {
          from fin have "finite A" unfolding A_def
            by(rule finite_subset[rotated]) auto
          moreover have "E `` A ⊆ ?visited'" using y unfolding A_def
            by(auto intro: rtrancl_into_rtrancl)
          moreover have "tgt ∉ A" unfolding A_def using y_tgt by auto
          ultimately have "Finite_Set.fold loop (Visited ?visited') A = (Visited (A ∪ ?visited'))"
            by(rule dfs_blocked) }
        also have "A ∪ ?visited' = insert src ?visited'" unfolding A_def by auto
        also { 
          have "E `` {src} - ?visited' ⊂ E `` {src} - visited" using y by fastforce
          moreover have "(src, tgt) ∉ (E ↿ - ?visited')⇧*" using ‹(src, tgt) ∉ (E ↿ - visited)⇧*›
            by(auto intro: rtrancl_mono[THEN subsetD, rotated])
          ultimately
          have "Finite_Set.fold loop (Visited (insert src ?visited')) (E `` {src} - insert src ?visited') =
                Visited (?visited' ∪ (E ↿ - ?visited')⇧* `` {src})"
            by(rule psubset.hyps) }
        also {
          fix x
          assume src_x: "(src, x) ∈ (E ↿ - visited)⇧*"
            and y_x: "(y, x) ∉ (E ↿ - insert src visited)⇧*"
          from src_x have "(src, x) ∈ (E ↿ - ?visited)⇧*"
            by (metis rtrancl_restrict_start Compl_insert Containers_DFS_Ex.restrict_restrict Diff_Compl double_complement)
          from rtrancl_restrict_reachable[OF this y_x]
          have "(src, x) ∈ (E ↿ - ?visited')⇧*" by simp (metis Un_insert_left compl_sup) }
        then have "?visited' ∪ (E ↿ - ?visited')⇧* `` {src} = visited ∪ (E ↿ - visited)⇧* `` {src}"
          using y by(auto intro: converse_rtrancl_into_rtrancl rtrancl_mono[THEN subsetD, rotated])
        also have "insert y ?succs = E `` {src} - insert src visited" using y by auto
        finally show ?thesis .
      qed
    qed
    finally
    show ?thesis using False fin
      by(simp add: dfs_def Let_def)(subst dfs_visited; auto)
  qed
qed

end

end

lift_definition dfs_body :: "'a ⇒ ('a, 'a dfs_result) comp_fun_commute"
is "λtgt x r. case r of Reachable ⇒ Reachable | Visited 𝒱 ⇒ if x ∈ 𝒱 then Visited 𝒱 else dfs x tgt 𝒱"
 by(rule comp_fun_commute_dfs_body)

lemma dfs_code [code]:
  "dfs src tgt visited =
  (if src = tgt then Reachable
   else let S = E `` {src} in 
   if finite S then set_fold_cfc (dfs_body tgt) (Visited (insert src visited)) S
   else Code.abort (STR ''infinite successor relation'') (λ_. dfs src tgt visited))"
by transfer(subst dfs_rec, simp add: Let_def)

lemma reachable_dfs [code]:
  "reachable src tgt = is_Reachable (dfs src tgt {})"
by(simp add: dfs_def reachable_def)

end

subsection ‹Refinement to executable code›

typedef 'a graph = "UNIV :: ('a × 'a) set set" morphisms edges Graph ..
setup_lifting type_definition_graph

text ‹Implement graphs with successor function›

definition graph_of_succs :: "('a ⇒ 'a set) ⇒ ('a × 'a) set"
where "graph_of_succs succs = {(v, w). w ∈ succs v}"
declare graph_of_succs_def[containers_post, symmetric, containers_pre]

lift_definition Succ :: "('a ⇒ 'a set) ⇒ 'a graph" is "graph_of_succs" .
code_datatype Succ

text ‹Identify operations on graph›

definition successors :: "('a × 'a) set ⇒ 'a ⇒ 'a set" where "successors E x = E `` {x}"
declare successors_def[containers_post, symmetric, containers_pre]

lift_definition succs :: "'a graph ⇒ 'a ⇒ 'a set" is successors .
lemma succs_code [code]: "succs (Succ s) = s" by transfer(simp add: successors_def fun_eq_iff graph_of_succs_def)

text ‹Transfer algorithms to abstract graph type›

lift_definition reachable_impl :: "'a graph ⇒ 'a ⇒ 'a ⇒ bool" is reachable .
lift_definition dfs_impl :: "'a graph ⇒ 'a ⇒ 'a ⇒ 'a set ⇒ 'a dfs_result" is dfs .
lift_definition dfs_body_impl :: "'a graph ⇒ 'a ⇒ ('a, 'a dfs_result) comp_fun_commute" is dfs_body .

lemmas [containers_identify, code] = reachable_dfs dfs_code dfs_body.rep_eq

subsection ‹Tests›

definition test_graph :: "nat graph"
where "test_graph = Succ ((λ_. {})(0 := {1,3}, 1 := {2,4}, 2 := {1}, 3 := {1, 5}, 4 := {5}))"

definition test_dfs where "test_dfs = map (reachable_impl test_graph 0) [0..<7]"

ML_val ‹
  val [true, true, true, true, true, true, false] = @{code test_dfs};
›

end