Theory DFS_Framework.DFS_Invars_Basic
section ‹Basic Invariant Library›
theory DFS_Invars_Basic
imports "../Param_DFS"
begin
text ‹We provide more basic invariants of the DFS algorithm›
subsection ‹Basic Timing Invariants›
abbreviation "the_discovered s v ≡ the (discovered s v)"
abbreviation "the_finished s v ≡ the (finished s v)"
locale timing_syntax
begin
notation the_discovered (‹δ›)
notation the_finished (‹φ›)
end
context param_DFS begin context begin interpretation timing_syntax .
definition "timing_common_inv s ≡
(∀v ∈ dom (finished s). δ s v < φ s v)
∧ (∀v ∈ dom (discovered s). ∀w ∈ dom (discovered s). v ≠ w ⟶ δ s v ≠ δ s w)
∧ (∀v ∈ dom (finished s). ∀w ∈ dom (finished s). v ≠ w ⟶ φ s v ≠ φ s w)
∧ (∀v ∈ dom (discovered s). δ s v < counter s)
∧ (∀v ∈ dom (finished s). φ s v < counter s)
∧ (∀v ∈ dom (finished s). ∀w ∈ succ v. δ s w < φ s v)"
lemma timing_common_inv:
"is_invar timing_common_inv"
proof (induction rule: is_invarI)
case (finish s s') then interpret DFS_invar where s=s by simp
from finish have NE: "stack s ≠ []" by (simp add: cond_alt)
have *: "hd (stack s) ∉ dom (finished s)" "hd (stack s) ∈ dom (discovered s)"
using stack_not_finished stack_discovered hd_in_set[OF NE]
by blast+
from discovered_closed have
"(E - pending s) `` {hd (stack s)} ⊆ dom (discovered s)"
using hd_in_set[OF NE]
by (auto simp add: discovered_closed_def)
hence succ_hd: "pending s `` {hd (stack s)} = {}
⟹ succ (hd (stack s)) ⊆ dom (discovered s)"
by blast
from finish show ?case
apply (simp add: timing_common_inv_def)
apply (intro conjI)
using * apply simp
using * apply simp
apply (metis less_irrefl)
apply (metis less_irrefl)
apply (metis less_SucI)
apply (metis less_SucI)
apply (blast dest!: succ_hd)
using * apply simp
done
next
case (discover s) then interpret DFS_invar where s=s by simp
from discover show ?case
apply (simp add: timing_common_inv_def)
apply (intro conjI)
using finished_discovered apply fastforce
apply (metis less_irrefl)
apply (metis less_irrefl)
apply (metis less_SucI)
apply (metis less_SucI)
using finished_imp_succ_discovered apply fastforce
done
next
case (new_root s s' v0) then interpret DFS_invar where s=s by simp
from new_root show ?case
apply (simp add: timing_common_inv_def)
apply (intro conjI)
using finished_discovered apply fastforce
apply (metis less_irrefl)
apply (metis less_irrefl)
apply (metis less_SucI)
apply (metis less_SucI)
using finished_imp_succ_discovered apply fastforce
done
qed (simp_all add: timing_common_inv_def)
end end
context DFS_invar begin context begin interpretation timing_syntax .
lemmas s_timing_common_inv =
timing_common_inv[THEN make_invar_thm]
lemma timing_less_counter:
"v ∈ dom (discovered s) ⟹ δ s v < counter s"
"v ∈ dom (finished s) ⟹ φ s v < counter s"
using s_timing_common_inv
by (auto simp add: timing_common_inv_def)
lemma disc_lt_fin:
"v ∈ dom (finished s) ⟹ δ s v < φ s v"
using s_timing_common_inv
by (auto simp add: timing_common_inv_def)
lemma disc_unequal:
assumes "v ∈ dom (discovered s)" "w ∈ dom (discovered s)"
and "v ≠ w"
shows "δ s v ≠ δ s w"
using s_timing_common_inv assms
by (auto simp add: timing_common_inv_def)
lemma fin_unequal:
assumes "v ∈ dom (finished s)" "w ∈ dom (finished s)"
and "v ≠ w"
shows "φ s v ≠ φ s w"
using s_timing_common_inv assms
by (auto simp add: timing_common_inv_def)
lemma finished_succ_fin:
assumes "v ∈ dom (finished s)"
and "w ∈ succ v"
shows "δ s w < φ s v"
using assms s_timing_common_inv
by (simp add: timing_common_inv_def)
end end
context param_DFS begin context begin interpretation timing_syntax .
lemma i_prev_stack_discover_all:
"is_invar (λs. ∀ n < length (stack s). ∀ v ∈ set (drop (Suc n) (stack s)).
δ s (stack s ! n) > δ s v)"
proof (induct rule: is_invarI)
case (finish s) thus ?case
by (cases "stack s") auto
next
case (discover s s' u v)
hence EQ[simp]: "discovered s' = (discovered s)(v ↦ counter s)"
"stack s' = v#stack s"
by simp_all
from discover interpret DFS_invar where s=s by simp
from discover stack_discovered have v_ni: "v ∉ set (stack s)" by auto
from stack_discovered timing_less_counter have
"⋀w. w ∈ set (stack s) ⟹ δ s w < counter s"
by blast
with v_ni have "⋀w. w ∈ set (stack s) ⟹ δ s' w < δ s' v" by auto
hence "⋀w. w ∈ set (drop (Suc 0) (stack s')) ⟹ δ s' w < δ s' (stack s' ! 0)"
by auto
moreover
from v_ni have
"⋀n. ⟦n < (length (stack s')); n > 0⟧
⟹ δ s' (stack s' ! n) = δ s (stack s' ! n)"
by auto
with discover(1) v_ni
have "⋀n. ⟦n < (length (stack s')) - 1; n > 0⟧
⟹ ∀ w ∈ set (drop (Suc n) (stack s')). δ s' (stack s' ! n) > δ s' w"
by (auto dest: in_set_dropD)
ultimately show ?case
by (metis drop_Suc_Cons length_drop length_pos_if_in_set length_tl
list.sel(3) neq0_conv nth_Cons_0 EQ(2) zero_less_diff)
qed simp_all
end end
context DFS_invar begin context begin interpretation timing_syntax .
lemmas prev_stack_discover_all
= i_prev_stack_discover_all[THEN make_invar_thm]
lemma prev_stack_discover:
"⟦n < length (stack s); v ∈ set (drop (Suc n) (stack s)) ⟧
⟹ δ s (stack s ! n) > δ s v"
by (metis prev_stack_discover_all)
lemma Suc_stack_discover:
assumes n: "n < (length (stack s)) - 1"
shows "δ s (stack s ! n) > δ s (stack s ! Suc n)"
proof -
from prev_stack_discover assms have
"⋀ v. v ∈ set (drop (Suc n) (stack s)) ⟹ δ s (stack s ! n) > δ s v"
by fastforce
moreover from n have "stack s ! Suc n ∈ set (drop (Suc n) (stack s))"
using in_set_conv_nth by fastforce
ultimately show ?thesis .
qed
lemma tl_lt_stack_hd_discover:
assumes notempty: "stack s ≠ []"
and "x ∈ set (tl (stack s))"
shows "δ s x < δ s (hd (stack s))"
proof -
from notempty obtain y ys where "stack s = y#ys" by (metis list.exhaust)
with assms show ?thesis
using prev_stack_discover
by (cases ys) force+
qed
lemma stack_nth_order:
assumes l: "i < length (stack s)" "j < length (stack s)"
shows "δ s (stack s ! i) < δ s (stack s ! j) ⟷ i > j" (is "δ s ?i < δ s ?j ⟷ _")
proof
assume δ: "δ s ?i < δ s ?j"
from l stack_set_def have
disc: "?i ∈ dom (discovered s)" "?j ∈ dom (discovered s)"
by auto
with disc_unequal[OF disc] δ have "i ≠ j" by auto
moreover
{
assume "i < j"
with l have "stack s ! j ∈ set (drop (Suc i) (stack s))"
using in_set_drop_conv_nth[of "stack s ! j" "Suc i" "stack s"]
by fastforce
with prev_stack_discover l have "δ s (stack s ! j) < δ s (stack s ! i)"
by simp
with δ have "False" by simp
}
ultimately show "i > j" by force
next
assume "i > j"
with l have "stack s ! i ∈ set (drop (Suc j) (stack s))"
using in_set_drop_conv_nth[of "stack s ! i" "Suc j" "stack s"]
by fastforce
with prev_stack_discover l show "δ s ?i < δ s ?j" by simp
qed
end end
subsection ‹Paranthesis Theorem›
context param_DFS begin context begin interpretation timing_syntax .
definition "parenthesis s ≡
∀v ∈ dom (discovered s). ∀w ∈ dom (discovered s).
δ s v < δ s w ∧ v ∈ dom (finished s) ⟶ (
φ s v < δ s w
∨ (φ s v > δ s w ∧ w ∈ dom (finished s) ∧ φ s w < φ s v))"
lemma i_parenthesis: "is_invar parenthesis"
proof (induct rule: is_invarI)
case (finish s s')
hence EQ[simp]: "discovered s' = discovered s"
"counter s' = Suc (counter s)"
"finished s' = (finished s)(hd (stack s) ↦ counter s)"
by simp_all
from finish interpret DFS_invar where s=s by simp
from finish have NE[simp]: "stack s ≠ []" by (simp add: cond_alt)
{
fix x y
assume dom: "x ∈ dom (discovered s')" "y ∈ dom (discovered s')"
and δ: "δ s' x < δ s' y"
and f: "x ∈ dom (finished s')"
hence neq: "x ≠ y" by force
note assms = dom δ f EQ
let ?DISJ = "φ s' x < δ s' y"
let ?IN = "δ s' y < φ s' x ∧ y ∈ dom (finished s') ∧ φ s' y < φ s' x"
have "?DISJ ∨ ?IN"
proof (cases "x = hd (stack s)")
case True note x_is_hd = this
hence φx: "φ s' x = counter s" by simp
from x_is_hd neq have y_not_hd: "y ≠ hd (stack s)" by simp
have "δ s y < φ s' x ∧ y ∈ dom (finished s) ∧ φ s y < φ s' x"
proof (cases "y ∈ set (stack s)")
case True with y_not_hd have "y ∈ set (tl (stack s))"
by (cases "stack s") simp_all
with tl_lt_stack_hd_discover[OF NE] δ x_is_hd have "δ s y < δ s x"
by simp
with δ have False by simp
thus ?thesis ..
next
case False
from dom have "y ∈ dom (discovered s)" by simp
with False discovered_not_stack_imp_finished have *:
"y ∈ dom (finished s)"
by simp
moreover with timing_less_counter φx have "φ s y < φ s' x" by simp
moreover with * disc_lt_fin φx have "δ s y < φ s' x"
by (metis less_trans)
ultimately show ?thesis by simp
qed
with y_not_hd show ?thesis by simp
next
case False note [simp] = this
show ?thesis
proof (cases "y = hd (stack s)")
case False with finish assms show ?thesis
by (simp add: parenthesis_def)
next
case True with stack_not_finished have "y ∉ dom (finished s)"
using hd_in_set[OF NE]
by auto
with finish assms have "φ s x < δ s y"
unfolding parenthesis_def
by auto
hence ?DISJ by simp
thus ?thesis ..
qed
qed
}
thus ?case by (simp add: parenthesis_def)
next
case (discover s s' u v)
hence EQ[simp]: "discovered s' = (discovered s)(v ↦ counter s)"
"finished s' = finished s"
"counter s' = Suc (counter s)"
by simp_all
from discover interpret DFS_invar where s=s by simp
from discover finished_discovered have
V': "v ∉ dom (discovered s)" "v ∉ dom (finished s)"
by auto
{
fix x y
assume dom: "x ∈ dom (discovered s')" "y ∈ dom (discovered s')"
and δ: "δ s' x < δ s' y"
and f: "x ∈ dom (finished s')"
let ?DISJ = "φ s' x < δ s' y"
let ?IN = "δ s' y < φ s' x ∧ y ∈ dom (finished s') ∧ φ s' y < φ s' x"
from dom V' f have x: "x ∈ dom (discovered s)""x ≠ v" by auto
have "?DISJ ∨ ?IN"
proof (cases "y = v")
case True hence "δ s' y = counter s" by simp
moreover from timing_less_counter x f have "φ s' x < counter s" by auto
ultimately have "?DISJ" by simp
thus ?thesis ..
next
case False with dom have "y ∈ dom (discovered s)" by simp
with discover False δ f x show ?thesis by (simp add: parenthesis_def)
qed
}
thus ?case by (simp add: parenthesis_def)
next
case (new_root s s' v0)
then interpret DFS_invar where s=s by simp
from finished_discovered new_root have "v0 ∉ dom (finished s')" by auto
with new_root timing_less_counter show ?case by (simp add: parenthesis_def)
qed (simp_all add: parenthesis_def)
end end
context DFS_invar begin context begin interpretation timing_syntax .
lemma parenthesis:
assumes "v ∈ dom (finished s)" "w ∈ dom (discovered s)"
and "δ s v < δ s w"
shows "φ s v < δ s w
∨ (φ s v > δ s w ∧ w ∈ dom (finished s) ∧ φ s w < φ s v)"
using assms
using i_parenthesis[THEN make_invar_thm]
using finished_discovered
unfolding parenthesis_def
by blast
lemma parenthesis_contained:
assumes "v ∈ dom (finished s)" "w ∈ dom (discovered s)"
and "δ s v < δ s w" "φ s v > δ s w"
shows "w ∈ dom (finished s) ∧ φ s w < φ s v"
using parenthesis assms
by force
lemma parenthesis_disjoint:
assumes "v ∈ dom (finished s)" "w ∈ dom (discovered s)"
and "δ s v < δ s w" "φ s w > φ s v"
shows "φ s v < δ s w"
using parenthesis assms
by force
lemma finished_succ_contained:
assumes "v ∈ dom (finished s)"
and "w ∈ succ v"
and "δ s v < δ s w"
shows "w ∈ dom (finished s) ∧ φ s w < φ s v"
using finished_succ_fin finished_imp_succ_discovered parenthesis_contained
using assms
by metis
end end
subsection ‹Edge Types›
context param_DFS
begin
abbreviation "edges s ≡ tree_edges s ∪ cross_edges s ∪ back_edges s"
lemma "is_invar (λs. finite (edges s))"
by (induction rule: establish_invarI) auto
text ‹Sometimes it's useful to just chose between tree-edges and non-tree.›
lemma edgesE_CB:
assumes "x ∈ edges s"
and "x ∈ tree_edges s ⟹ P"
and "x ∈ cross_edges s ∪ back_edges s ⟹ P"
shows "P"
using assms by auto
definition "edges_basic s ≡
Field (back_edges s) ⊆ dom (discovered s) ∧ back_edges s ⊆ E - pending s
∧ Field (cross_edges s) ⊆ dom (discovered s) ∧ cross_edges s ⊆ E - pending s
∧ Field (tree_edges s) ⊆ dom (discovered s) ∧ tree_edges s ⊆ E - pending s
∧ back_edges s ∩ cross_edges s = {}
∧ back_edges s ∩ tree_edges s = {}
∧ cross_edges s ∩ tree_edges s = {}
"
lemma i_edges_basic:
"is_invar edges_basic"
unfolding edges_basic_def[abs_def]
proof (induct rule: is_invarI_full)
case (back_edge s)
then interpret DFS_invar where s=s by simp
from back_edge show ?case by (auto dest: pendingD)
next
case (cross_edge s)
then interpret DFS_invar where s=s by simp
from cross_edge show ?case by (auto dest: pendingD)
next
case (discover s)
then interpret DFS_invar where s=s by simp
from discover show ?case
apply (simp add: Field_def Range_def Domain_def)
apply (drule pendingD) apply simp
by (blast)
next
case (new_root s)
thus ?case by (simp add: Field_def) blast
qed auto
lemmas (in DFS_invar) edges_basic = i_edges_basic[THEN make_invar_thm]
lemma i_edges_covered:
"is_invar (λs. (E ∩ dom (discovered s) × UNIV) - pending s = edges s)"
proof (induction rule: is_invarI_full)
case (new_root s s' v0)
interpret DFS_invar G param s by fact
from new_root empty_stack_imp_empty_pending
have [simp]: "pending s = {}" by simp
from ‹v0 ∉ dom (discovered s)›
have [simp]: "E ∩ insert v0 (dom (discovered s)) × UNIV - {v0} × succ v0
= E ∩ dom (discovered s) × UNIV" by auto
from new_root show ?case by simp
next
case (cross_edge s s' u v)
interpret DFS_invar G param s by fact
from cross_edge stack_discovered have "u ∈ dom (discovered s)"
by (cases "stack s") auto
with cross_edge(2-) pending_ssE have
"E ∩ dom (discovered s) × UNIV - (pending s - {(hd (stack s), v)})
= insert (hd (stack s), v) (E ∩ dom (discovered s) × UNIV - pending s)"
by auto
thus ?case using cross_edge by simp
next
case (back_edge s s' u v)
interpret DFS_invar G param s by fact
from back_edge stack_discovered have "u ∈ dom (discovered s)"
by (cases "stack s") auto
with back_edge(2-) pending_ssE have
"E ∩ dom (discovered s) × UNIV - (pending s - {(hd (stack s), v)})
= insert (hd (stack s), v) (E ∩ dom (discovered s) × UNIV - pending s)"
by auto
thus ?case using back_edge by simp
next
case (discover s s' u v)
interpret DFS_invar G param s by fact
from discover stack_discovered have "u ∈ dom (discovered s)"
by (cases "stack s") auto
with discover(2-) pending_ssE have
"E ∩ insert v (dom (discovered s)) × UNIV
- (pending s - {(hd (stack s), v)} ∪ {v} × succ v)
= insert (hd (stack s), v) (E ∩ dom (discovered s) × UNIV - pending s)"
by auto
thus ?case using discover by simp
qed simp_all
end
context DFS_invar begin
lemmas edges_covered =
i_edges_covered[THEN make_invar_thm]
lemma edges_ss_reachable_edges:
"edges s ⊆ E ∩ reachable × UNIV"
using edges_covered discovered_reachable
by (fast intro: rtrancl_image_advance_rtrancl)
lemma nc_edges_covered:
assumes "¬cond s" "¬is_break param s"
shows "E ∩ reachable × UNIV = edges s"
proof -
from assms have [simp]: "stack s = []"
unfolding cond_def by (auto simp: pred_defs)
hence [simp]: "pending s = {}" by (rule empty_stack_imp_empty_pending)
from edges_covered nc_discovered_eq_reachable[OF assms]
show ?thesis by simp
qed
lemma
tree_edges_ssE: "tree_edges s ⊆ E" and
tree_edges_not_pending: "tree_edges s ⊆ - pending s" and
tree_edge_is_succ: "(v,w) ∈ tree_edges s ⟹ w ∈ succ v" and
tree_edges_discovered: "Field (tree_edges s) ⊆ dom (discovered s)" and
cross_edges_ssE: "cross_edges s ⊆ E" and
cross_edges_not_pending: "cross_edges s ⊆ - pending s" and
cross_edge_is_succ: "(v,w) ∈ cross_edges s ⟹ w ∈ succ v" and
cross_edges_discovered: "Field (cross_edges s) ⊆ dom (discovered s)" and
back_edges_ssE: "back_edges s ⊆ E" and
back_edges_not_pending: "back_edges s ⊆ - pending s" and
back_edge_is_succ: "(v,w) ∈ back_edges s ⟹ w ∈ succ v" and
back_edges_discovered: "Field (back_edges s) ⊆ dom (discovered s)"
using edges_basic
unfolding edges_basic_def
by auto
lemma edges_disjoint:
"back_edges s ∩ cross_edges s = {}"
"back_edges s ∩ tree_edges s = {}"
"cross_edges s ∩ tree_edges s = {}"
using edges_basic
unfolding edges_basic_def
by auto
lemma tree_edge_imp_discovered:
"(v,w) ∈ tree_edges s ⟹ v ∈ dom (discovered s)"
"(v,w) ∈ tree_edges s ⟹ w ∈ dom (discovered s)"
using tree_edges_discovered
by (auto simp add: Field_def)
lemma back_edge_imp_discovered:
"(v,w) ∈ back_edges s ⟹ v ∈ dom (discovered s)"
"(v,w) ∈ back_edges s ⟹ w ∈ dom (discovered s)"
using back_edges_discovered
by (auto simp add: Field_def)
lemma cross_edge_imp_discovered:
"(v,w) ∈ cross_edges s ⟹ v ∈ dom (discovered s)"
"(v,w) ∈ cross_edges s ⟹ w ∈ dom (discovered s)"
using cross_edges_discovered
by (auto simp add: Field_def)
lemma edge_imp_discovered:
"(v,w) ∈ edges s ⟹ v ∈ dom (discovered s)"
"(v,w) ∈ edges s ⟹ w ∈ dom (discovered s)"
using tree_edge_imp_discovered cross_edge_imp_discovered back_edge_imp_discovered
by blast+
lemma tree_edges_finite[simp, intro!]: "finite (tree_edges s)"
using finite_subset[OF tree_edges_discovered discovered_finite] by simp
lemma cross_edges_finite[simp, intro!]: "finite (cross_edges s)"
using finite_subset[OF cross_edges_discovered discovered_finite] by simp
lemma back_edges_finite[simp, intro!]: "finite (back_edges s)"
using finite_subset[OF back_edges_discovered discovered_finite] by simp
lemma edges_finite: "finite (edges s)"
by auto
end
subsubsection ‹Properties of the DFS Tree›
context DFS_invar begin context begin interpretation timing_syntax .
lemma tree_edge_disc_lt_fin:
"(v,w) ∈ tree_edges s ⟹ v ∈ dom (finished s) ⟹ δ s w < φ s v"
by (metis finished_succ_fin tree_edge_is_succ)
lemma back_edge_disc_lt_fin:
"(v,w) ∈ back_edges s ⟹ v ∈ dom (finished s) ⟹ δ s w < φ s v"
by (metis finished_succ_fin back_edge_is_succ)
lemma cross_edge_disc_lt_fin:
"(v,w) ∈ cross_edges s ⟹ v ∈ dom (finished s) ⟹ δ s w < φ s v"
by (metis finished_succ_fin cross_edge_is_succ)
end end
context param_DFS begin
lemma i_stack_is_tree_path:
"is_invar (λs. stack s ≠ [] ⟶ (∃v0 ∈ V0.
path (tree_edges s) v0 (rev (tl (stack s))) (hd (stack s))))"
proof (induct rule: is_invarI)
case (discover s s' u v)
hence EQ[simp]: "stack s' = v # stack s"
"tree_edges s' = insert (hd (stack s), v) (tree_edges s)"
by simp_all
from discover have NE[simp]: "stack s ≠ []" by simp
from discover obtain v0 where
"v0 ∈ V0"
"path (tree_edges s) v0 (rev (tl (stack s))) (hd (stack s))"
by blast
with path_mono[OF _ this(2)] EQ have
"path (tree_edges s') v0 (rev (tl (stack s))) (hd (stack s))"
by blast
with ‹v0 ∈ V0› show ?case
by (cases "stack s") (auto simp: path_simps)
next
case (finish s s')
hence EQ[simp]: "stack s' = tl (stack s)"
"tree_edges s' = tree_edges s"
by simp_all
from finish obtain v0 where
"v0 ∈ V0"
"path (tree_edges s) v0 (rev (tl (stack s))) (hd (stack s))"
by blast
hence P: "path (tree_edges s') v0 (rev (stack s')) (hd (stack s))" by simp
show ?case
proof
assume A: "stack s' ≠ []"
with P have "(hd (stack s'), hd (stack s)) ∈ tree_edges s'"
by (auto simp: neq_Nil_conv path_simps)
moreover from P A have
"path (tree_edges s') v0 (rev (tl (stack s')) @ [hd (stack s')]) (hd (stack s))"
by (simp)
moreover note ‹v0 ∈ V0›
ultimately show "∃v0∈V0. path (tree_edges s') v0 (rev (tl (stack s'))) (hd (stack s'))"
by (auto simp add: path_append_conv)
qed
qed simp_all
end
context DFS_invar begin
lemmas stack_is_tree_path =
i_stack_is_tree_path[THEN make_invar_thm, rule_format]
lemma stack_is_path:
"stack s ≠ [] ⟹ ∃v0∈V0. path E v0 (rev (tl (stack s))) (hd (stack s))"
using stack_is_tree_path path_mono[OF tree_edges_ssE]
by blast
lemma hd_succ_stack_is_path:
assumes ne: "stack s ≠ []"
and succ: "v ∈ succ (hd (stack s))"
shows "∃v0∈V0. path E v0 (rev (stack s)) v"
proof -
from stack_is_path[OF ne] succ obtain v0 where
"v0 ∈ V0"
"path E v0 (rev (tl (stack s)) @ [hd (stack s)]) v"
by (auto simp add: path_append_conv)
thus ?thesis using ne
by (cases "stack s") auto
qed
lemma tl_stack_hd_tree_path:
assumes "stack s ≠ []"
and "v ∈ set (tl (stack s))"
shows "(v, hd (stack s)) ∈ (tree_edges s)⇧+"
proof -
from stack_is_tree_path assms obtain v0 where
"path (tree_edges s) v0 (rev (tl (stack s))) (hd (stack s))"
by auto
from assms path_member_reach_end[OF this] show ?thesis by simp
qed
end
context param_DFS begin
definition "tree_discovered_inv s ≡
(tree_edges s = {} ⟶ dom (discovered s) ⊆ V0 ∧ (stack s = [] ∨ (∃v0∈V0. stack s = [v0])))
∧ (tree_edges s ≠ {} ⟶ (tree_edges s)⇧+ `` V0 ∪ V0 = dom (discovered s) ∪ V0)"
lemma i_tree_discovered_inv:
"is_invar tree_discovered_inv"
proof (induct rule: is_invarI)
case (discover s s' u v)
hence EQ[simp]: "stack s' = v # stack s"
"tree_edges s' = insert (hd (stack s), v) (tree_edges s)"
"discovered s' = (discovered s)(v ↦ counter s)"
by simp_all
from discover interpret DFS_invar where s=s by simp
from discover have NE[simp]: "stack s ≠ []" by simp
note TDI = ‹tree_discovered_inv s›[unfolded tree_discovered_inv_def]
have "tree_edges s' = {} ⟶ dom (discovered s') ⊆ V0 ∧ (stack s' = [] ∨ (∃v0∈V0. stack s' = [v0]))"
by simp
moreover {
fix x
assume A: "x ∈ (tree_edges s')⇧+ `` V0 ∪ V0" "x ∉ V0"
then obtain y where y: "(y,x) ∈ (tree_edges s')⇧+" "y ∈ V0" by auto
have "x ∈ dom (discovered s') ∪ V0"
proof (cases "tree_edges s = {}")
case True with discover A have "(tree_edges s')⇧+ = {(hd (stack s), v)}"
by (simp add: trancl_single)
with A show ?thesis by auto
next
case False note t_ne = this
show ?thesis
proof (cases "x = v")
case True thus ?thesis by simp
next
case False with y have "(y,x) ∈ (tree_edges s)⇧+"
proof (induct rule: trancl_induct)
case (step a b) hence "(a,b) ∈ tree_edges s" by simp
with tree_edge_imp_discovered have "a ∈ dom (discovered s)" by simp
with discover have "a ≠ v" by blast
with step show ?case by auto
qed simp
with ‹y ∈ V0› have "x ∈ (tree_edges s)⇧+ `` V0" by auto
with t_ne TDI show ?thesis by auto
qed
qed
} note t_d = this
{
fix x
assume "x ∈ dom (discovered s') ∪ V0" "x ∉ V0"
hence A: "x ∈ dom (discovered s')" by simp
have "x ∈ (tree_edges s')⇧+ `` V0 ∪ V0"
proof (cases "tree_edges s = {}")
case True with trancl_single have "(tree_edges s')⇧+ = {(hd (stack s), v)}" by simp
moreover from True TDI have "hd (stack s) ∈ V0" "dom (discovered s) ⊆ V0" by auto
ultimately show ?thesis using A ‹x∉V0› by auto
next
case False note t_ne = this
show ?thesis
proof (cases "x=v")
case False with A have "x ∈ dom (discovered s)" by simp
with TDI t_ne ‹x ∉ V0› have "x ∈ (tree_edges s)⇧+ `` V0" by auto
with trancl_sub_insert_trancl show ?thesis by simp blast
next
case True
from t_ne TDI have "dom (discovered s) ∪ V0 = (tree_edges s)⇧+ `` V0 ∪ V0"
by simp
moreover from stack_is_tree_path[OF NE] obtain v0 where "v0 ∈ V0" and
"(v0, hd (stack s)) ∈ (tree_edges s)⇧*"
by (blast intro!: path_is_rtrancl)
with EQ have "(v0, hd (stack s)) ∈ (tree_edges s')⇧*" by (auto intro: rtrancl_mono_mp)
ultimately show ?thesis using ‹v0 ∈ V0› True by (auto elim: rtrancl_into_trancl1)
qed
qed
} with t_d have "(tree_edges s')⇧+ `` V0 ∪ V0 = dom (discovered s') ∪ V0" by blast
ultimately show ?case by (simp add: tree_discovered_inv_def)
qed (auto simp add: tree_discovered_inv_def)
lemmas (in DFS_invar) tree_discovered_inv =
i_tree_discovered_inv[THEN make_invar_thm]
lemma (in DFS_invar) discovered_iff_tree_path:
"v ∉ V0 ⟹ v ∈ dom (discovered s) ⟷ (∃v0∈V0. (v0,v) ∈ (tree_edges s)⇧+)"
using tree_discovered_inv
by (auto simp add: tree_discovered_inv_def)
lemma i_tree_one_predecessor:
"is_invar (λs. ∀(v,v') ∈ tree_edges s. ∀y. y ≠ v ⟶ (y,v') ∉ tree_edges s)"
proof (induct rule: is_invarI)
case (discover s s' u v)
hence EQ[simp]: "tree_edges s' = insert (hd (stack s),v) (tree_edges s)" by simp
from discover interpret DFS_invar where s=s by simp
from discover have NE[simp]: "stack s ≠ []" by (simp add: cond_alt)
{
fix w w' y
assume *: "(w,w') ∈ tree_edges s'"
and "y ≠ w"
from discover stack_discovered have v_hd: "hd (stack s) ≠ v"
using hd_in_set[OF NE] by blast
from discover tree_edges_discovered have
v_notin_tree: "∀(x,x') ∈ tree_edges s. x ≠ v ∧ x' ≠ v"
by (blast intro!: Field_not_elem)
have "(y,w') ∉ tree_edges s'"
proof (cases "w = hd (stack s)")
case True
have "(y,v) ∉ tree_edges s'"
proof (rule notI)
assume "(y,v) ∈ tree_edges s'"
with True ‹y≠w› have "(y,v) ∈ tree_edges s" by simp
with v_notin_tree show False by auto
qed
with True * ‹y≠w› v_hd show ?thesis
apply (cases "w = v")
apply simp
using discover apply simp apply blast
done
next
case False with v_notin_tree * ‹y≠w› v_hd
show ?thesis
apply (cases "w' = v")
apply simp apply blast
using discover apply simp apply blast
done
qed
}
thus ?case by blast
qed simp_all
lemma (in DFS_invar) tree_one_predecessor:
assumes "(v,w) ∈ tree_edges s"
and "a ≠ v"
shows "(a,w) ∉ tree_edges s"
using assms make_invar_thm[OF i_tree_one_predecessor]
by blast
lemma (in DFS_invar) tree_eq_rule:
"⟦(v,w) ∈ tree_edges s; (u,w) ∈ tree_edges s⟧ ⟹ v=u"
using tree_one_predecessor
by blast
context begin interpretation timing_syntax .
lemma i_tree_edge_disc:
"is_invar (λs. ∀(v,v') ∈ tree_edges s. δ s v < δ s v')"
proof (induct rule: is_invarI)
case (discover s s' u v)
hence EQ[simp]: "tree_edges s' = insert (hd (stack s), v) (tree_edges s)"
"discovered s' = (discovered s)(v ↦ counter s)"
by simp_all
from discover interpret DFS_invar where s=s by simp
from discover have NE[simp]: "stack s ≠ []" by (simp add: cond_alt)
from discover tree_edges_discovered have
v_notin_tree: "∀(x,x') ∈ tree_edges s. x ≠ v ∧ x' ≠ v"
by (blast intro!: Field_not_elem)
from discover stack_discovered have
v_hd: "hd (stack s) ≠ v"
using hd_in_set[OF NE]
by blast
{
fix a b
assume T: "(a,b) ∈ tree_edges s'"
have "δ s' a < δ s' b"
proof (cases "b = v")
case True with T v_notin_tree have [simp]: "a = hd (stack s)" by auto
with stack_discovered have "a ∈ dom (discovered s)"
by (metis hd_in_set NE subsetD)
with v_hd True timing_less_counter show ?thesis by simp
next
case False with v_notin_tree T have "(a,b) ∈ tree_edges s" "a ≠ v" by auto
with discover have "δ s a < δ s b" by auto
with False ‹a≠v› show ?thesis by simp
qed
} thus ?case by blast
next
case (new_root s s' v0) then interpret DFS_invar where s=s by simp
from new_root have "tree_edges s' = tree_edges s" by simp
moreover from tree_edge_imp_discovered new_root have "∀(v,v') ∈ tree_edges s. v ≠ v0 ∧ v' ≠ v0" by blast
ultimately show ?case using new_root by auto
qed simp_all
end end
context DFS_invar begin context begin interpretation timing_syntax .
lemma tree_edge_disc:
"(v,w) ∈ tree_edges s ⟹ δ s v < δ s w"
using i_tree_edge_disc[THEN make_invar_thm]
by blast
lemma tree_path_disc:
"(v,w) ∈ (tree_edges s)⇧+ ⟹ δ s v < δ s w"
by (auto elim!: trancl_induct dest: tree_edge_disc)
lemma no_loop_in_tree:
"(v,v) ∉ (tree_edges s)⇧+"
using tree_path_disc by auto
lemma tree_acyclic:
"acyclic (tree_edges s)"
by (metis acyclicI no_loop_in_tree)
lemma no_self_loop_in_tree:
"(v,v) ∉ tree_edges s"
using tree_edge_disc by auto
lemma tree_edge_unequal:
"(v,w) ∈ tree_edges s ⟹ v ≠ w"
by (metis no_self_loop_in_tree)
lemma tree_path_unequal:
"(v,w) ∈ (tree_edges s)⇧+ ⟹ v ≠ w"
by (metis no_loop_in_tree)
lemma tree_subpath':
assumes x: "(x,v) ∈ (tree_edges s)⇧+"
and y: "(y,v) ∈ (tree_edges s)⇧+"
and "x ≠ y"
shows "(x,y) ∈ (tree_edges s)⇧+ ∨ (y,x) ∈ (tree_edges s)⇧+"
proof -
from x obtain px where px: "path (tree_edges s) x px v" and "px ≠ []"
using trancl_is_path by metis
from y obtain py where py: "path (tree_edges s) y py v" and "py ≠ []"
using trancl_is_path by metis
from ‹px ≠ []› ‹py ≠ []› px py
show ?thesis
proof (induction arbitrary: v rule: rev_nonempty_induct2')
case (single) hence "(x,v) ∈ tree_edges s" "(y,v) ∈ tree_edges s"
by (simp_all add: path_simps)
with tree_eq_rule have "x=y" by simp
with ‹x≠y› show ?case by contradiction
next
case (snocl a as) hence "(y,v) ∈ tree_edges s" by (simp add: path_simps)
moreover from snocl have "path (tree_edges s) x as a" "(a,v) ∈ tree_edges s"
by (simp_all add: path_simps)
ultimately have "path (tree_edges s) x as y"
using tree_eq_rule
by auto
with path_is_trancl ‹as ≠ []› show ?case by metis
next
case (snocr _ a as) hence "(x,v) ∈ tree_edges s" by (simp add: path_simps)
moreover from snocr have "path (tree_edges s) y as a" "(a,v) ∈ tree_edges s"
by (simp_all add: path_simps)
ultimately have "path (tree_edges s) y as x"
using tree_eq_rule
by auto
with path_is_trancl ‹as ≠ []› show ?case by metis
next
case (snoclr a as b bs) hence
"path (tree_edges s) x as a" "(a,v) ∈ tree_edges s"
"path (tree_edges s) y bs b" "(b,v) ∈ tree_edges s"
by (simp_all add: path_simps)
moreover hence "a=b" using tree_eq_rule by simp
ultimately show ?thesis using snoclr.IH by metis
qed
qed
lemma tree_subpath:
assumes "(x,v) ∈ (tree_edges s)⇧+"
and "(y,v) ∈ (tree_edges s)⇧+"
and δ: "δ s x < δ s y"
shows "(x,y) ∈ (tree_edges s)⇧+"
proof -
from δ have "x ≠ y" by auto
with assms tree_subpath' have "(x,y) ∈ (tree_edges s)⇧+ ∨ (y,x) ∈ (tree_edges s)⇧+"
by simp
moreover from δ tree_path_disc have "(y,x) ∉ (tree_edges s)⇧+" by force
ultimately show ?thesis by simp
qed
lemma on_stack_is_tree_path:
assumes x: "x ∈ set (stack s)"
and y: "y ∈ set (stack s)"
and δ: "δ s x < δ s y"
shows "(x,y) ∈ (tree_edges s)⇧+"
proof -
from x obtain i where i: "stack s ! i = x" "i < length (stack s)"
by (metis in_set_conv_nth)
from y obtain j where j: "stack s ! j = y" "j < length (stack s)"
by (metis in_set_conv_nth)
with i δ stack_nth_order have "j < i" by force
from x have ne[simp]: "stack s ≠ []" by auto
from ‹j<i› have "x ∈ set (tl (stack s))"
using nth_mem nth_tl[OF ne, of "i - 1"] i
by auto
with tl_stack_hd_tree_path have
x_path: "(x, hd (stack s)) ∈ (tree_edges s)⇧+"
by simp
then show ?thesis
proof (cases "j=0")
case True with j have "hd (stack s) = y" by (metis hd_conv_nth ne)
with x_path show ?thesis by simp
next
case False hence "y ∈ set (tl (stack s))"
using nth_mem nth_tl[OF ne, of "j - 1"] j
by auto
with tl_stack_hd_tree_path have "(y, hd (stack s)) ∈ (tree_edges s)⇧+"
by simp
with x_path δ show ?thesis
using tree_subpath
by metis
qed
qed
lemma hd_stack_tree_path_finished:
assumes "stack s ≠ []"
assumes "(hd (stack s), v) ∈ (tree_edges s)⇧+"
shows "v ∈ dom (finished s)"
proof (cases "v ∈ set (stack s)")
case True
from assms no_loop_in_tree have "hd (stack s) ≠ v" by auto
with True have "v ∈ set (tl (stack s))" by (cases "stack s") auto
with tl_stack_hd_tree_path assms have "(hd (stack s), hd (stack s)) ∈ (tree_edges s)⇧+" by (metis trancl_trans)
with no_loop_in_tree show ?thesis by contradiction
next
case False
from assms obtain x where "(x,v) ∈ tree_edges s" by (metis tranclE)
with tree_edge_imp_discovered have "v ∈ dom (discovered s)" by blast
with False show ?thesis by (simp add: stack_set_def)
qed
lemma tree_edge_impl_parenthesis:
assumes t: "(v,w) ∈ tree_edges s"
and f: "v ∈ dom (finished s)"
shows "w ∈ dom (finished s)
∧ δ s v < δ s w
∧ φ s w < φ s v "
proof -
from tree_edge_disc_lt_fin assms have "δ s w < φ s v" by simp
with f tree_edge_imp_discovered[OF t] tree_edge_disc[OF t]
show ?thesis
using parenthesis_contained
by metis
qed
lemma tree_path_impl_parenthesis:
assumes "(v,w) ∈ (tree_edges s)⇧+"
and "v ∈ dom (finished s)"
shows "w ∈ dom (finished s)
∧ δ s v < δ s w
∧ φ s w < φ s v "
using assms
by (auto elim!: trancl_induct dest: tree_edge_impl_parenthesis)
lemma nc_reachable_v0_parenthesis:
assumes C: "¬ cond s" "¬ is_break param s"
and v: "v ∈ reachable" "v ∉ V0"
obtains v0 where "v0 ∈ V0"
and "δ s v0 < δ s v ∧ φ s v < φ s v0 "
proof -
from nc_discovered_eq_reachable[OF C] discovered_iff_tree_path v
obtain v0 where "v0 ∈ V0" and
"(v0,v) ∈ (tree_edges s)⇧+"
by auto
moreover with nc_V0_finished[OF C] have "v0 ∈ dom (finished s)"
by auto
ultimately show ?thesis
using tree_path_impl_parenthesis that[OF ‹v0 ∈ V0›]
by simp
qed
end end
context param_DFS begin context begin interpretation timing_syntax .
definition paren_imp_tree_reach where
"paren_imp_tree_reach s ≡ ∀v ∈ dom (discovered s). ∀w ∈ dom (finished s).
δ s v < δ s w ∧ (v ∉ dom (finished s) ∨ φ s v > φ s w)
⟶ (v,w) ∈ (tree_edges s)⇧+"
lemma paren_imp_tree_reach:
"is_invar paren_imp_tree_reach"
unfolding paren_imp_tree_reach_def[abs_def]
proof (induct rule: is_invarI)
case (discover s s' u v)
hence EQ[simp]: "tree_edges s' = insert (hd (stack s), v) (tree_edges s)"
"finished s' = finished s"
"discovered s' = (discovered s)(v ↦ counter s)"
by simp_all
from discover interpret DFS_invar where s=s by simp
from discover have NE[simp]: "stack s ≠ []" by (simp add: cond_alt)
show ?case
proof (intro ballI impI)
fix a b
assume F:"a ∈ dom (discovered s')" "b ∈ dom (finished s')"
and D: "δ s' a < δ s' b ∧ (a ∉ dom (finished s') ∨ φ s' a > φ s' b)"
from F finished_discovered discover have "b ≠ v" by auto
show "(a,b) ∈ (tree_edges s')⇧+"
proof (cases "a = v")
case True with D ‹b≠v› have "counter s < δ s b" by simp
also from F have "b ∈ dom (discovered s)"
using finished_discovered by auto
with timing_less_counter have "δ s b < counter s" by simp
finally have False .
thus ?thesis ..
next
case False with ‹b≠v› F D discover have "(a,b) ∈ (tree_edges s)⇧+" by simp
thus ?thesis by (auto intro: trancl_mono_mp)
qed
qed
next
case (finish s s' u)
hence EQ[simp]: "tree_edges s' = tree_edges s"
"finished s' = (finished s)(hd (stack s) ↦ counter s)"
"discovered s' = discovered s"
"stack s' = tl (stack s)"
by simp_all
from finish interpret DFS_invar where s=s by simp
from finish have NE[simp]: "stack s ≠ []" by (simp add: cond_alt)
show ?case
proof (intro ballI impI)
fix a b
assume F: "a ∈ dom (discovered s')" "b ∈ dom (finished s')"
and paren: "δ s' a < δ s' b ∧ (a ∉ dom (finished s') ∨ φ s' a > φ s' b)"
hence "a ≠ b" by auto
show "(a,b) ∈ (tree_edges s')⇧+"
proof (cases "b = hd (stack s)")
case True hence φb: "φ s' b = counter s" by simp
have "a ∈ set (stack s)"
unfolding stack_set_def
proof
from F show "a ∈ dom (discovered s)" by simp
from True ‹a≠b› φb paren have "a ∈ dom (finished s) ⟶ φ s a > counter s" by simp
with timing_less_counter show "a ∉ dom (finished s)" by force
qed
with paren True on_stack_is_tree_path have "(a,b) ∈ (tree_edges s)⇧+" by auto
thus ?thesis by (auto intro: trancl_mono_mp)
next
case False note b_not_hd = this
show ?thesis
proof (cases "a = hd (stack s)")
case False with b_not_hd F paren finish show ?thesis by simp
next
case True with paren b_not_hd F have
"a ∈ dom (discovered s)" "b ∈ dom (finished s)" "δ s a < δ s b"
by simp_all
moreover from True stack_not_finished have "a ∉ dom (finished s)"
by simp
ultimately show ?thesis by (simp add: finish)
qed
qed
qed
next
case (new_root s s' v0) then interpret DFS_invar where s=s by simp
from new_root finished_discovered have "v0 ∉ dom (finished s)" by auto
moreover note timing_less_counter finished_discovered
ultimately show ?case using new_root by clarsimp force
qed simp_all
end end
context DFS_invar begin context begin interpretation timing_syntax .
lemmas s_paren_imp_tree_reach =
paren_imp_tree_reach[THEN make_invar_thm]
lemma parenthesis_impl_tree_path_not_finished:
assumes "v ∈ dom (discovered s)"
and "w ∈ dom (finished s)"
and "δ s v < δ s w"
and "v ∉ dom (finished s)"
shows "(v,w) ∈ (tree_edges s)⇧+"
using s_paren_imp_tree_reach assms
by (auto simp add: paren_imp_tree_reach_def)
lemma parenthesis_impl_tree_path:
assumes "v ∈ dom (finished s)" "w ∈ dom (finished s)"
and "δ s v < δ s w" "φ s v > φ s w"
shows "(v,w) ∈ (tree_edges s)⇧+"
proof -
from assms(1) have "v ∈ dom (discovered s)"
using finished_discovered by blast
with assms show ?thesis
using s_paren_imp_tree_reach assms
by (auto simp add: paren_imp_tree_reach_def)
qed
lemma tree_path_iff_parenthesis:
assumes "v ∈ dom (finished s)" "w ∈ dom (finished s)"
shows "(v,w) ∈ (tree_edges s)⇧+ ⟷ δ s v < δ s w ∧ φ s v > φ s w"
using assms
by (metis parenthesis_impl_tree_path tree_path_impl_parenthesis)
lemma no_pending_succ_impl_path_in_tree:
assumes v: "v ∈ dom (discovered s)" "pending s `` {v} = {}"
and w: "w ∈ succ v"
and δ: "δ s v < δ s w"
shows "(v,w) ∈ (tree_edges s)⇧+"
proof (cases "v ∈ dom (finished s)")
case True
with assms assms have "δ s w < φ s v" "w ∈ dom (discovered s)"
using finished_succ_fin finished_imp_succ_discovered
by simp_all
with True δ show ?thesis
using parenthesis_contained parenthesis_impl_tree_path
by blast
next
case False
show ?thesis
proof (cases "w ∈ dom (finished s)")
case True with False v δ show ?thesis by (simp add: parenthesis_impl_tree_path_not_finished)
next
case False with ‹v ∉ dom (finished s)› no_pending_imp_succ_discovered v w have
"v ∈ set (stack s)" "w ∈ set (stack s)"
by (simp_all add: stack_set_def)
with on_stack_is_tree_path δ show ?thesis by simp
qed
qed
lemma finished_succ_impl_path_in_tree:
assumes f: "v ∈ dom (finished s)"
and s: "w ∈ succ v"
and δ: "δ s v < δ s w"
shows "(v,w) ∈ (tree_edges s)⇧+"
using no_pending_succ_impl_path_in_tree finished_no_pending finished_discovered
using assms
by blast
end end
subsubsection ‹Properties of Cross Edges›
context param_DFS begin context begin interpretation timing_syntax .
lemma i_cross_edges_finished: "is_invar (λs. ∀(u,v)∈cross_edges s.
v ∈ dom (finished s) ∧ (u ∈ dom (finished s) ⟶ φ s v < φ s u))"
proof (induction rule: is_invarI_full)
case (finish s s' u e)
interpret DFS_invar G param s by fact
from finish stack_not_finished have "u ∉ dom (finished s)" by auto
with finish show ?case by (auto intro: timing_less_counter)
next
case (cross_edge s s' u v e)
interpret DFS_invar G param s by fact
from cross_edge stack_not_finished have "u ∉ dom (finished s)" by auto
with cross_edge show ?case by (auto intro: timing_less_counter)
qed simp_all
end end
context DFS_invar begin context begin interpretation timing_syntax .
lemmas cross_edges_finished
= i_cross_edges_finished[THEN make_invar_thm]
lemma cross_edges_target_finished:
"(u,v)∈cross_edges s ⟹ v ∈ dom (finished s)"
using cross_edges_finished by auto
lemma cross_edges_finished_decr:
"⟦(u,v)∈cross_edges s; u∈dom (finished s)⟧ ⟹ φ s v < φ s u"
using cross_edges_finished by auto
lemma cross_edge_unequal:
assumes cross: "(v,w) ∈ cross_edges s"
shows "v ≠ w"
proof -
from cross_edges_target_finished[OF cross] have
w_fin: "w ∈ dom (finished s)" .
show ?thesis
proof (cases "v ∈ dom (finished s)")
case True with cross_edges_finished_decr[OF cross]
show ?thesis by force
next
case False with w_fin show ?thesis by force
qed
qed
end end
subsubsection ‹Properties of Back Edges›
context param_DFS begin context begin interpretation timing_syntax .
lemma i_back_edge_impl_tree_path:
"is_invar (λs. ∀(v,w) ∈ back_edges s. (w,v) ∈ (tree_edges s)⇧+ ∨ w = v)"
proof (induct rule: is_invarI_full)
case (back_edge s s' u v) then interpret DFS_invar where s=s by simp
from back_edge have st: "v ∈ set (stack s)" "u ∈ set (stack s)"
using stack_set_def
by auto
have "(v,u) ∈ (tree_edges s)⇧+ ∨ u = v"
proof (rule disjCI)
assume "u ≠ v"
with st back_edge have "v ∈ set (tl (stack s))" by (metis not_hd_in_tl)
with tl_lt_stack_hd_discover st back_edge have "δ s v < δ s u" by simp
with on_stack_is_tree_path st show "(v,u) ∈ (tree_edges s)⇧+" by simp
qed
with back_edge show ?case by auto
next
case discover thus ?case using trancl_sub_insert_trancl by force
qed simp_all
end end
context DFS_invar begin context begin interpretation timing_syntax .
lemma back_edge_impl_tree_path:
"⟦(v,w) ∈ back_edges s; v ≠ w⟧ ⟹ (w,v) ∈ (tree_edges s)⇧+"
using i_back_edge_impl_tree_path[THEN make_invar_thm]
by blast
lemma back_edge_disc:
assumes "(v,w) ∈ back_edges s"
shows "δ s w ≤ δ s v"
proof cases
assume "v≠w"
with assms back_edge_impl_tree_path have "(w,v) ∈ (tree_edges s)⇧+" by simp
with tree_path_disc show ?thesis by force
qed simp
lemma back_edges_tree_disjoint:
"back_edges s ∩ tree_edges s = {}"
using back_edge_disc tree_edge_disc
by force
lemma back_edges_tree_pathes_disjoint:
"back_edges s ∩ (tree_edges s)⇧+ = {}"
using back_edge_disc tree_path_disc
by force
lemma back_edge_finished:
assumes "(v,w) ∈ back_edges s"
and "w ∈ dom (finished s)"
shows "v ∈ dom (finished s) ∧ φ s v ≤ φ s w"
proof (cases "v=w")
case True with assms show ?thesis by simp
next
case False with back_edge_impl_tree_path assms have "(w,v) ∈ (tree_edges s)⇧+" by simp
with tree_path_impl_parenthesis assms show ?thesis by fastforce
qed
end end
context param_DFS begin context begin interpretation timing_syntax .
lemma i_disc_imp_back_edge_or_pending:
"is_invar (λs. ∀(v,w) ∈ E.
v ∈ dom (discovered s) ∧ w ∈ dom (discovered s)
∧ δ s v ≥ δ s w
∧ (w ∈ dom (finished s) ⟶ v ∈ dom (finished s) ∧ φ s w ≥ φ s v)
⟶ (v,w) ∈ back_edges s ∨ (v,w) ∈ pending s)"
proof (induct rule: is_invarI_full)
case (cross_edge s s' u v) then interpret DFS_invar where s=s by simp
from cross_edge stack_not_finished[of u] have "u ∉ dom (finished s)"
using hd_in_set
by (auto simp add: cond_alt)
with cross_edge show ?case by auto
next
case (finish s s' u v) then interpret DFS_invar where s=s by simp
from finish have
IH: "⋀v w. ⟦w ∈ succ v; v ∈ dom (discovered s); w ∈ dom (discovered s);
δ s w ≤ δ s v;
(w ∈ dom (finished s) ⟹ v ∈ dom (finished s) ∧ φ s v ≤ φ s w)⟧
⟹ (v, w) ∈ back_edges s ∨ (v, w) ∈ pending s"
by blast
from finish have ne[simp]: "stack s ≠ []"
and p[simp]: "pending s `` {hd (stack s)} = {}"
by (simp_all)
from hd_in_set[OF ne] have disc: "hd (stack s) ∈ dom (discovered s)"
and not_fin: "hd (stack s) ∉ dom (finished s)"
using stack_discovered stack_not_finished
by blast+
{
fix w
assume w: "w ∈ succ (hd (stack s))" "w ≠ hd (stack s)" "w ∈ dom (discovered s)"
and f: "w ∈ dom (finished s) ⟶ counter s ≤ φ s w"
and δ: "δ s w ≤ δ s (hd (stack s))"
with timing_less_counter have "w ∉ dom (finished s)" by force
with finish w δ disc have "(hd (stack s), w) ∈ back_edges s" by blast
}
moreover
{
fix w
assume "hd (stack s) ∈ succ w" "w ≠ hd (stack s)"
and "w ∈ dom (finished s)" "δ s (hd (stack s)) ≤ δ s w"
with IH[of "hd (stack s)" w] disc not_fin have
"(w, hd (stack s)) ∈ back_edges s"
using finished_discovered finished_no_pending[of w]
by blast
}
ultimately show ?case
using finish
by clarsimp auto
next
case (discover s s' u v) then interpret DFS_invar where s=s by simp
from discover show ?case
using timing_less_counter
by clarsimp fastforce
next
case (new_root s s' v0) then interpret DFS_invar where s=s by simp
from new_root empty_stack_imp_empty_pending have "pending s = {}" by simp
with new_root show ?case
using timing_less_counter
by clarsimp fastforce
qed auto
end end
context DFS_invar begin context begin interpretation timing_syntax .
lemma disc_imp_back_edge_or_pending:
"⟦w ∈ succ v; v ∈ dom (discovered s); w ∈ dom (discovered s); δ s w ≤ δ s v;
(w ∈ dom (finished s) ⟹ v ∈ dom (finished s) ∧ φ s v ≤ φ s w)⟧
⟹ (v, w) ∈ back_edges s ∨ (v, w) ∈ pending s"
using i_disc_imp_back_edge_or_pending[THEN make_invar_thm]
by blast
lemma finished_imp_back_edge:
"⟦w ∈ succ v; v ∈ dom (finished s); w ∈ dom (finished s);
δ s w ≤ δ s v; φ s v ≤ φ s w⟧
⟹ (v, w) ∈ back_edges s"
using disc_imp_back_edge_or_pending finished_discovered finished_no_pending
by fast
lemma finished_not_finished_imp_back_edge:
"⟦w ∈ succ v; v ∈ dom (finished s); w ∈ dom (discovered s);
w ∉ dom (finished s);
δ s w ≤ δ s v⟧
⟹ (v, w) ∈ back_edges s"
using disc_imp_back_edge_or_pending finished_discovered finished_no_pending
by fast
lemma finished_self_loop_in_back_edges:
assumes "v ∈ dom (finished s)"
and "(v,v) ∈ E"
shows "(v,v) ∈ back_edges s"
using assms
using finished_imp_back_edge
by blast
end end
context DFS_invar begin
context begin interpretation timing_syntax .
lemma tree_cross_acyclic:
"acyclic (tree_edges s ∪ cross_edges s)" (is "acyclic ?E")
proof (rule ccontr)
{
fix u v
assume *: "u ∈ dom (finished s)" and "(u,v) ∈ ?E⇧+"
from this(2) have "φ s v < φ s u ∧ v ∈ dom (finished s)"
proof induct
case base thus ?case
by (metis Un_iff * cross_edges_finished_decr cross_edges_target_finished tree_edge_impl_parenthesis)
next
case (step v w)
hence "φ s w < φ s v ∧ w ∈ dom (finished s)"
by (metis Un_iff cross_edges_finished_decr cross_edges_target_finished tree_edge_impl_parenthesis)
with step show ?case by auto
qed
} note aux = this
assume "¬ acyclic ?E"
then obtain u where path: "(u,u) ∈ ?E⇧+" by (auto simp add: acyclic_def)
show False
proof cases
assume "u ∈ dom (finished s)"
with aux path show False by blast
next
assume *: "u ∉ dom (finished s)"
moreover
from no_loop_in_tree have "(u,u) ∉ (tree_edges s)⇧+" .
with trancl_union_outside[OF path] obtain x y where "(u,x) ∈ ?E⇧*" "(x,y) ∈ cross_edges s" "(y,u) ∈ ?E⇧*" by auto
with cross_edges_target_finished have "y ∈ dom (finished s)" by simp
moreover with * ‹(y,u) ∈ ?E⇧*› have "(y,u) ∈ ?E⇧+" by (auto simp add: rtrancl_eq_or_trancl)
ultimately show False by (metis aux)
qed
qed
end
lemma cycle_contains_back_edge:
assumes cycle: "(u,u) ∈ (edges s)⇧+"
shows "∃v w. (u,v) ∈ (edges s)⇧* ∧ (v,w) ∈ back_edges s ∧ (w,u) ∈ (edges s)⇧*"
proof -
from tree_cross_acyclic have "(u,u) ∉ (tree_edges s ∪ cross_edges s)⇧+" by (simp add: acyclic_def)
with trancl_union_outside[OF cycle] show ?thesis .
qed
lemma cycle_needs_back_edge:
assumes "back_edges s = {}"
shows "acyclic (edges s)"
proof (rule ccontr)
assume "¬ acyclic (edges s)"
then obtain u where "(u,u) ∈ (edges s)⇧+" by (auto simp: acyclic_def)
with assms have "(u,u) ∈ (tree_edges s ∪ cross_edges s)⇧+" by auto
with tree_cross_acyclic show False by (simp add: acyclic_def)
qed
lemma back_edge_closes_cycle:
assumes "back_edges s ≠ {}"
shows "¬ acyclic (edges s)"
proof -
from assms obtain v w where be: "(v,w) ∈ back_edges s" by auto
hence "(w,w) ∈ (edges s)⇧+"
proof (cases "v=w")
case False
with be back_edge_impl_tree_path have "(w,v) ∈ (tree_edges s)⇧+" by simp
hence "(w,v) ∈ (edges s)⇧+" by (blast intro: trancl_mono_mp)
also from be have "(v,w) ∈ edges s" by simp
finally show ?thesis .
qed auto
thus ?thesis by (auto simp add: acyclic_def)
qed
lemma back_edge_closes_reachable_cycle:
"back_edges s ≠ {} ⟹ ¬ acyclic (E ∩ reachable × UNIV)"
by (metis back_edge_closes_cycle edges_ss_reachable_edges cyclic_subset)
lemma cycle_iff_back_edges:
"acyclic (edges s) ⟷ back_edges s = {}"
by (metis back_edge_closes_cycle cycle_needs_back_edge)
end
subsection ‹White Path Theorem›
context DFS begin
context begin interpretation timing_syntax .
definition white_path where
"white_path s x y ≡ x≠y
⟶ (∃p. path E x p y ∧
(δ s x < δ s y ∧ (∀ v ∈ set (tl p). δ s x < δ s v)))"
lemma white_path:
"it_dfs ≤ SPEC(λs. ∀x ∈ reachable. ∀y ∈ reachable. ¬ is_break param s ⟶
white_path s x y ⟷ (x,y) ∈ (tree_edges s)⇧*)"
proof (rule it_dfs_SPEC, intro ballI impI)
fix s x y
assume DI: "DFS_invar G param s"
and C: "¬ cond s" "¬ is_break param s"
and reach: "x ∈ reachable" "y ∈ reachable"
from DI interpret DFS_invar where s=s .
note fin_eq_reach = nc_finished_eq_reachable[OF C]
show "white_path s x y ⟷ (x,y) ∈ (tree_edges s)⇧*"
proof (cases "x=y")
case True thus ?thesis by (simp add: white_path_def)
next
case False
show ?thesis
proof
assume "(x,y) ∈ (tree_edges s)⇧*"
with ‹x≠y› have T: "(x,y) ∈ (tree_edges s)⇧+" by (metis rtranclD)
then obtain p where P: "path (tree_edges s) x p y" by (metis trancl_is_path)
with tree_edges_ssE have "path E x p y" using path_mono[where E="tree_edges s"]
by simp
moreover
from P have "δ s x < δ s y ∧ (∀ v ∈ set (tl p). δ s x < δ s v)"
using ‹x≠y›
proof (induct rule: path_tl_induct)
case (single u) thus ?case by (fact tree_edge_disc)
next
case (step u v) note ‹δ s x < δ s u›
also from step have "δ s u < δ s v" by (metis tree_edge_disc)
finally show ?case .
qed
ultimately show "white_path s x y"
by (auto simp add: ‹x≠y› white_path_def)
next
assume "white_path s x y"
with ‹x≠y› obtain p where
P:"path E x p y" and
white: "δ s x < δ s y ∧ (∀ v ∈ set (tl p). δ s x < δ s v)"
unfolding white_path_def
by blast
hence "p ≠ []" by auto
thus "(x,y) ∈ (tree_edges s)⇧*" using P white reach(2)
proof (induction p arbitrary: y rule: rev_nonempty_induct)
case single hence "y ∈ succ x" by (simp add: path_cons_conv)
with reach single show ?case
using fin_eq_reach finished_succ_impl_path_in_tree[of x y]
by simp
next
case (snoc u us) hence "path E x us u" by (simp add: path_append_conv)
moreover hence "(x,u) ∈ E⇧*" by (simp add: path_is_rtrancl)
with reach have ureach: "u ∈ reachable"
by (metis rtrancl_image_advance_rtrancl)
moreover from snoc have "δ s x < δ s u" "(∀v∈set (tl us). δ s x < δ s v)"
by simp_all
ultimately have x_u: "(x,u) ∈ (tree_edges s)⇧*" by (metis snoc.IH)
from snoc have "y ∈ succ u" by (simp add: path_append_conv)
from snoc(5) fin_eq_reach finished_discovered have
y_f_d: "y ∈ dom (finished s)" "y ∈ dom (discovered s)"
by auto
from ‹y ∈ succ u› ureach fin_eq_reach have "δ s y < φ s u"
using finished_succ_fin by simp
also from ‹δ s x < δ s u› have "x ≠ u" by auto
with x_u have "(x,u) ∈ (tree_edges s)⇧+" by (metis rtrancl_eq_or_trancl)
with fin_eq_reach reach have "φ s u < φ s x"
using tree_path_impl_parenthesis
by simp
finally have "φ s y < φ s x"
using reach fin_eq_reach y_f_d snoc
using parenthesis_contained
by blast
hence "(x,y) ∈ (tree_edges s)⇧+"
using reach fin_eq_reach y_f_d snoc
using parenthesis_impl_tree_path
by blast
thus ?case by auto
qed
qed
qed
qed
end end
end