# Theory Containers_DFS_Ex

theory Containers_DFS_Ex
imports Containers Transitive_Closure_Table
```(* 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"

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 𝒱)"

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"
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 {})"

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
```