(* $Id: DFS.thy,v 1.8 2009/03/04 14:02:51 berghofe Exp $ *)
header {* Depth First Search *}
theory DFS
imports Main
begin
definition
"succsr succs \ {(x, y). y \ set (succs x)}"
function (tailrec)
gen_dfs
where
base: "gen_dfs succs ins memb S [] = S"
| step: "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 pat_completeness auto
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 is_node"
context DFS
begin
definition rel where
"rel = inv_image finite_psubset (\S. {n \ is_node. \ 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 induct_scheme
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 mem_def cong: conj_cong)
apply (rule finite_Int [unfolded Int_def [unfolded mem_def]])
apply (rule disjI1)
apply (rule graph_finite)
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)}\<^sup>* `` 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 (step S y xs)
then show ?case
by (auto simp add: visit_subset_dfs ins_eq ins_invariant succs_is_node)
qed simp
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\<^sup>* `` X = X"
proof
show "r\<^sup>* `` X \ X"
proof(unfold Image_def, auto)
fix x y
assume "y \ X"
assume "(y,x) \ r\<^sup>*"
thus "x \ X"
by (induct, auto! simp add: Image_def)
qed
qed auto
lemma reachable_closed_dfs:
assumes xs: "list_all is_node xs"
shows "reachable (set xs) \ set_of (dfs empt xs)"
proof -
from xs 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 xs 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 (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 (simp add: reachable_def)
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)\<^sup>*)"
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 (step S x xs)
show ?case
proof (cases "memb x S")
case False
then show ?thesis
apply simp
apply (rule step)
apply assumption
apply (rule I)
apply assumption
apply (rule step)+
done
qed (simp add: step)
qed simp
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 xy: "(x, y) \ (succsr succs)\<^sup>*"
shows "is_node x \ is_node y" using xy
proof induct
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