Theory DFS
section "Depth-First Search"
theory DFS
imports Main
begin
subsection "Definition of Graphs"
typedecl node
type_synonym graph = "(node * node) list"
primrec nexts :: "[graph, node] ⇒ node list"
where
"nexts [] n = []"
| "nexts (e#es) n = (if fst e = n then snd e # nexts es n else nexts es n)"
definition nextss :: "[graph, node list] ⇒ node set"
where "nextss g xs = set g `` set xs"
lemma nexts_set: "y ∈ set (nexts g x) = ((x,y) ∈ set g)"
by (induct g) auto
lemma nextss_Cons: "nextss g (x#xs) = set (nexts g x) ∪ nextss g xs"
unfolding nextss_def by (auto simp add:Image_def nexts_set)
definition reachable :: "[graph, node list] ⇒ node set"
where "reachable g xs = (set g)⇧* `` set xs"
subsection "Depth-First Search with Stack"
definition nodes_of :: "graph ⇒ node set"
where "nodes_of g = set (map fst g @ map snd g)"
lemma [simp]: "x ∉ nodes_of g ⟹ nexts g x = []"
by (induct g) (auto simp add: nodes_of_def)
lemma [simp]: "finite (nodes_of g - set ys)"
proof(rule finite_subset)
show "finite (nodes_of g)"
by (auto simp add: nodes_of_def)
qed (auto)
function
dfs :: "graph ⇒ node list ⇒ node list ⇒ node list"
where
dfs_base: "dfs g [] ys = ys"
| dfs_inductive: "dfs g (x#xs) ys = (if List.member ys x then dfs g xs ys
else dfs g (nexts g x@xs) (x#ys))"
by pat_completeness auto
termination
apply (relation "inv_image (finite_psubset <*lex*> less_than)
(λ(g,xs,ys). (nodes_of g - set ys, size xs))")
apply auto[1]
apply (simp_all add: finite_psubset_def)
by (case_tac "x ∈ nodes_of g") (auto simp add: List.member_def)
text ‹
\begin{itemize}
\item The second argument of \isatext{\isastyle{dfs}} is a stack of nodes that will be
visited.
\item The third argument of \isatext{\isastyle{dfs}} is a list of nodes that have
been visited already.
\end{itemize}
›
subsection "Depth-First Search with Nested-Recursion"
function
dfs2 :: "graph ⇒ node list ⇒ node list ⇒ node list"
where
"dfs2 g [] ys = ys"
| dfs2_inductive:
"dfs2 g (x#xs) ys = (if List.member ys x then dfs2 g xs ys
else dfs2 g xs (dfs2 g (nexts g x) (x#ys)))"
by pat_completeness auto
lemma dfs2_invariant: "dfs2_dom (g, xs, ys) ⟹ set ys ⊆ set (dfs2 g xs ys)"
by (induct g xs ys rule: dfs2.pinduct) (force simp add: dfs2.psimps)+
termination dfs2
apply (relation "inv_image (finite_psubset <*lex*> less_than)
(λ(g,xs,ys). (nodes_of g - set ys, size xs))")
apply auto[1]
apply (simp_all add: finite_psubset_def)
apply (case_tac "x ∈ nodes_of g")
apply (auto simp add: List.member_def)[2]
by (insert dfs2_invariant) force
lemma dfs_app: "dfs g (xs@ys) zs = dfs g ys (dfs g xs zs)"
by (induct g xs zs rule: dfs.induct) auto
lemma "dfs2 g xs ys = dfs g xs ys"
by (induct g xs ys rule: dfs2.induct) (auto simp add: dfs_app)
subsection "Basic Properties"
lemma visit_subset_dfs: "set ys ⊆ set (dfs g xs ys)"
by (induct g xs ys rule: dfs.induct) auto
lemma next_subset_dfs: "set xs ⊆ set (dfs g xs ys)"
proof(induct g xs ys rule:dfs.induct)
case(2 g x xs ys)
show ?case
proof(cases "x ∈ set ys")
case True
have "set ys ⊆ set (dfs g xs ys)"
by (rule visit_subset_dfs)
with 2 and True show ?thesis
by (auto simp add: List.member_def)
next
case False
have "set (x#ys) ⊆ set (dfs g (nexts g x @ xs) (x#ys))"
by(rule visit_subset_dfs)
with 2 and False show ?thesis
by (auto simp add: List.member_def)
qed
qed(simp)
lemma nextss_closed_dfs'[rule_format]:
"nextss g ys ⊆ set xs ∪ set ys ⟶ nextss g (dfs g xs ys) ⊆ set (dfs g xs ys)"
by (induct g xs ys rule:dfs.induct, auto simp add:nextss_Cons List.member_def)
lemma nextss_closed_dfs: "nextss g (dfs g xs []) ⊆ set (dfs g xs [])"
by (rule nextss_closed_dfs', simp add: nextss_def)
lemma Image_closed_trancl: assumes "r `` X ⊆ X" shows "r⇧* `` X = X"
proof
show "r⇧* `` X ⊆ X"
proof -
{
fix x y
assume y: "y ∈ X"
assume "(y,x) ∈ r⇧*"
then have "x ∈ X"
by (induct) (insert assms y, auto simp add: Image_def)
}
then show ?thesis unfolding Image_def by auto
qed
qed auto
lemma reachable_closed_dfs: "reachable g xs ⊆ set(dfs g xs [])"
proof -
have "reachable g xs ⊆ reachable g (dfs g xs [])"
unfolding reachable_def by (rule Image_mono) (auto simp add: next_subset_dfs)
also have "… = set(dfs g xs [])"
unfolding reachable_def
proof (rule Image_closed_trancl)
from nextss_closed_dfs
show "set g `` set (dfs g xs []) ⊆ set (dfs g xs [])"
by (simp add: nextss_def)
qed
finally show ?thesis .
qed
lemma reachable_nexts: "reachable g (nexts g x) ⊆ reachable g [x]"
unfolding reachable_def
by (auto intro: converse_rtrancl_into_rtrancl simp: nexts_set)
lemma reachable_append: "reachable g (xs @ ys) = reachable g xs ∪ reachable g ys"
unfolding reachable_def by auto
lemma dfs_subset_reachable_visit_nodes: "set (dfs g xs ys) ⊆ reachable g xs ∪ set ys"
proof(induct g xs ys rule: dfs.induct)
case 1
then show ?case by simp
next
case (2 g x xs ys)
show ?case
proof (cases "x ∈ set ys")
case True
with 2 show "set (dfs g (x#xs) ys) ⊆ reachable g (x#xs) ∪ set ys"
by (auto simp add: reachable_def List.member_def)
next
case False
have "reachable g (nexts g x) ⊆ reachable g [x]"
by (rule reachable_nexts)
hence a: "reachable g (nexts g x @ xs) ⊆ reachable g (x#xs)"
by(simp add: reachable_append, auto simp add: reachable_def)
with False 2
show "set (dfs g (x#xs) ys) ⊆ reachable g (x#xs) ∪ set ys"
by (auto simp add: reachable_def List.member_def)
qed
qed
subsection "Correctness"
theorem dfs_eq_reachable: "set (dfs g xs []) = reachable g xs"
proof
have "set (dfs g xs []) ⊆ reachable g xs ∪ set []"
by (rule dfs_subset_reachable_visit_nodes[of g xs "[]"])
thus "set (dfs g xs []) ⊆ reachable g xs"
by simp
qed(rule reachable_closed_dfs)
theorem "y ∈ set (dfs g [x] []) = ((x,y) ∈ (set g)⇧*)"
by(simp only:dfs_eq_reachable reachable_def, auto)
subsection "Executable Code"
consts Node :: "int ⇒ node"
code_datatype Node
instantiation node :: equal
begin
definition equal_node :: "node ⇒ node ⇒ bool"
where
[code del]: "equal_node = HOL.eq"
instance proof
qed (simp add: equal_node_def)
end
declare [[code abort: "HOL.equal :: node ⇒ node ⇒ bool"]]
export_code dfs dfs2 in SML file ‹dfs.ML›
end