Theory DFS
section ‹Depth First Search›
theory DFS
imports Main
begin
definition "succsr succs = {(x, y). y ∈ set (succs x)}"
partial_function (tailrec) gen_dfs
where
"gen_dfs succs ins memb S wl =
(case wl of
[] ⇒ S
| x # xs ⇒
if memb x S then gen_dfs succs ins memb S xs
else gen_dfs succs ins memb (ins x S) (succs x @ xs))"
lemma gen_dfs_simps[simp]:
"gen_dfs succs ins memb S [] = S"
"gen_dfs succs ins memb S (x # xs) =
(if memb x S then gen_dfs succs ins memb S xs
else gen_dfs succs ins memb (ins x S) (succs x @ xs))"
by (simp_all add: gen_dfs.simps)
locale DFS =
fixes succs :: "'a ⇒ 'a list"
and is_node :: "'a ⇒ bool"
and invariant :: "'b ⇒ bool"
and ins :: "'a ⇒ 'b ⇒ 'b"
and memb :: "'a ⇒ 'b ⇒ bool"
and empt :: 'b
assumes ins_eq: "⋀x y S. is_node x ⟹ is_node y ⟹ invariant S ⟹ ¬ memb y S ⟹
memb x (ins y S) = ((x = y) ∨ memb x S)"
and empt: "⋀x. is_node x ⟹ ¬ memb x empt"
and succs_is_node: "⋀x. is_node x ⟹ list_all is_node (succs x)"
and empt_invariant: "invariant empt"
and ins_invariant: "⋀x S. is_node x ⟹ invariant S ⟹ ¬ memb x S ⟹ invariant (ins x S)"
and graph_finite: "finite {x. is_node x}"
begin
definition rel where
"rel = inv_image finite_psubset (λS. {n. is_node n ∧ ¬ memb n S})"
abbreviation "dfs ≡ gen_dfs succs ins memb"
lemma dfs_induct [consumes 2, case_names base step]:
assumes S: "invariant S"
and xs: "list_all is_node xs"
and I1: "⋀S. invariant S ⟹ P S []"
and I2: "⋀S x xs. invariant S ⟹ is_node x ⟹ list_all is_node xs ⟹
(memb x S ⟹ P S xs) ⟹ (¬ memb x S ⟹ P (ins x S) (succs x @ xs)) ⟹ P S (x # xs)"
shows "P S xs" using I1 I2 S xs
apply induction_schema
apply atomize_elim
apply (case_tac xs, simp+)
apply atomize_elim
apply (rule conjI)
apply (rule ins_invariant, assumption+)
apply (rule succs_is_node, assumption)
apply (relation "rel <*lex*> measure length")
apply (simp add: wf_lex_prod rel_def)
apply simp
apply simp
apply (rule disjI1)
apply (simp add: rel_def finite_psubset_def)
apply (rule conjI)
apply (auto simp add: ins_eq graph_finite cong: conj_cong)
done
definition "succss xs = (⋃x∈xs. set (succs x))"
definition "set_of S = {x. is_node x ∧ memb x S}"
definition "reachable xs = {(x, y). y ∈ set (succs x)}⇧* `` xs"
lemma visit_subset_dfs: "invariant S ⟹ list_all is_node xs ⟹
is_node y ⟹ memb y S ⟹ memb y (dfs S xs)"
by (induct S xs rule: dfs_induct) (simp_all add: ins_eq)
lemma next_subset_dfs: "invariant S ⟹ list_all is_node xs ⟹
x ∈ set xs ⟹ memb x (dfs S xs)"
proof (induct S xs rule: dfs_induct)
case base
then show ?case by simp
next
case (step S y xs)
then show ?case
by (auto simp add: visit_subset_dfs ins_eq ins_invariant succs_is_node)
qed
lemma succss_closed_dfs':
"invariant ys ⟹ list_all is_node xs ⟹
succss (set_of ys) ⊆ set xs ∪ set_of ys ⟹
succss (set_of (dfs ys xs)) ⊆ set_of (dfs ys xs)"
by (induct ys xs rule: dfs_induct)
(auto simp add: ins_eq succss_def set_of_def cong: conj_cong)
lemma succss_closed_dfs: "list_all is_node xs ⟹
succss (set_of (dfs empt xs)) ⊆ set_of (dfs empt xs)"
apply (rule succss_closed_dfs')
apply (rule empt_invariant)
apply assumption
apply (simp add: succss_def)
apply (rule subsetI)
apply (erule UN_E)
apply (simp add: set_of_def empt cong: conj_cong)
done
lemma Image_closed_trancl: assumes "r `` X ⊆ X" shows "r⇧* `` X = X"
proof
show "X ⊆ r⇧* `` X" by auto
show "r⇧* `` X ⊆ X"
proof -
{ fix x y
assume y: "y ∈ X"
assume "(y,x) ∈ r⇧*"
then have "x ∈ X" using assms y
by induct (auto simp add: Image_def)
} then show ?thesis by auto
qed
qed
lemma reachable_closed_dfs:
assumes "list_all is_node xs"
shows "reachable (set xs) ⊆ set_of (dfs empt xs)"
proof -
from assms have "reachable (set xs) ⊆ reachable (set_of (dfs empt xs))"
apply (unfold reachable_def)
apply (rule Image_mono)
apply (auto simp add: set_of_def next_subset_dfs empt_invariant list_all_iff)
done
also from succss_closed_dfs assms have "… = set_of (dfs empt xs)"
apply (unfold reachable_def)
apply (rule Image_closed_trancl)
apply (auto simp add: succss_def set_of_def)
done
finally show ?thesis .
qed
lemma reachable_succs: "reachable (set (succs x)) ⊆ reachable {x}"
by (auto simp add: reachable_def intro: converse_rtrancl_into_rtrancl)
lemma dfs_subset_reachable_visit_nodes:
"invariant ys ⟹ list_all is_node xs ⟹
set_of (dfs ys xs) ⊆ reachable (set xs) ∪ set_of ys"
proof (induct ys xs rule: dfs_induct)
case base
then show ?case by (simp add: reachable_def)
next
case (step S x xs)
show ?case
proof (cases "memb x S")
case True
with step show ?thesis
by (auto simp add: reachable_def)
next
case False
have "reachable (set (succs x)) ⊆ reachable {x}"
by (rule reachable_succs)
then have "reachable (set (succs x @ xs)) ⊆ reachable (set (x # xs))"
by (auto simp add: reachable_def)
then show ?thesis using step
by (auto simp add: reachable_def ins_eq set_of_def cong: conj_cong)
qed
qed
theorem dfs_eq_reachable:
assumes y: "is_node y"
and xs: "list_all is_node xs"
shows "memb y (dfs empt xs) = (y ∈ reachable (set xs))"
proof
assume "memb y (dfs empt xs)"
with dfs_subset_reachable_visit_nodes [OF empt_invariant xs] y
show "y ∈ reachable (set xs)"
by (auto simp add: empt set_of_def)
next
assume "y ∈ reachable (set xs)"
with reachable_closed_dfs [OF xs] show "memb y (dfs empt xs)"
by (auto simp add: set_of_def)
qed
theorem dfs_eq_rtrancl:
assumes y: "is_node y"
and x: "is_node x"
shows "memb y (dfs empt [x]) = ((x,y) ∈ (succsr succs)⇧*)"
proof -
from x have x': "list_all is_node [x]" by simp
show ?thesis
by (simp only: dfs_eq_reachable [OF y x'] reachable_def succsr_def) (auto simp add: empt)
qed
theorem dfs_invariant [consumes 2, case_names base step]:
assumes S: "invariant S"
and xs: "list_all is_node xs"
and H: "I S"
and I: "⋀S x. ¬ memb x S ⟹ is_node x ⟹ invariant S ⟹ I S ⟹ I (ins x S)"
shows "I (dfs S xs)"
proof -
from S xs H
have "I (dfs S xs) ∧ invariant (dfs S xs)"
proof (induct S xs rule: dfs_induct)
case base
then show ?case by simp
next
case (step S x xs)
show ?case
proof (cases "memb x S")
case True
then show ?thesis by (simp add: step)
next
case False
then show ?thesis
apply simp
apply (rule step)
apply assumption
apply (rule I)
apply assumption
apply (rule step)+
done
qed
qed
then show ?thesis ..
qed
theorem dfs_invariant': "invariant S ⟹ list_all is_node xs ⟹ invariant (dfs S xs)"
by (induct S xs rule: dfs_induct) auto
theorem succsr_is_node:
assumes "(x, y) ∈ (succsr succs)⇧*"
shows "is_node x ⟹ is_node y" using assms
proof induct
case base
then show ?case .
next
case (step y z)
then have "is_node y" by simp
then have "list_all is_node (succs y)"
by (rule succs_is_node)
with step show ?case
by (simp add: succsr_def list_all_iff)
qed
end
declare gen_dfs_simps [simp del]
end