Theory Tarjan
section ‹Tarjan's Algorithm›
theory Tarjan
imports
Tarjan_LowLink
begin
text ‹We use the DFS Framework to implement Tarjan's algorithm.
Note that, currently, we only provide an abstract version, and no refinement to
efficient code.
›
subsection ‹Preliminaries›
lemma tjs_union:
fixes tjs u
defines "dw ≡ dropWhile ((≠) u) tjs"
defines "tw ≡ takeWhile ((≠) u) tjs"
assumes "u ∈ set tjs"
shows "set tjs = set (tl dw) ∪ insert u (set tw)"
proof -
from takeWhile_dropWhile_id have "set tjs = set (tw@dw)" by (auto simp: dw_def tw_def)
hence "set tjs = set tw ∪ set dw" by (metis set_append)
moreover from ‹u ∈ set tjs› dropWhile_eq_Nil_conv have "dw ≠ []" by (auto simp: dw_def)
from hd_dropWhile[OF this[unfolded dw_def]] have "hd dw = u" by (simp add: dw_def)
with ‹dw ≠ []› have "set dw = insert u (set (tl dw))" by (cases "dw") auto
ultimately show ?thesis by blast
qed
subsection ‹Instantiation of the DFS-Framework›
record 'v tarjan_state = "'v state" +
sccs :: "'v set set"
lowlink :: "'v ⇀ nat"
tj_stack :: "'v list"
type_synonym 'v tarjan_param = "('v, ('v,unit) tarjan_state_ext) parameterization"
abbreviation "the_lowlink s v ≡ the (lowlink s v)"
context timing_syntax
begin
notation the_lowlink ("ζ")
end
locale Tarjan_def = graph_defs G
for G :: "('v, 'more) graph_rec_scheme"
begin
context begin interpretation timing_syntax .
definition tarjan_disc :: "'v ⇒ 'v tarjan_state ⇒ ('v,unit) tarjan_state_ext nres" where
"tarjan_disc v s = RETURN ⦇ sccs = sccs s,
lowlink = (lowlink s)(v ↦ δ s v),
tj_stack = v#tj_stack s⦈"
definition tj_stack_pop :: "'v list ⇒ 'v ⇒ ('v list × 'v set) nres" where
"tj_stack_pop tjs u = RETURN (tl (dropWhile ((≠) u) tjs), insert u (set (takeWhile ((≠) u) tjs)))"
lemma tj_stack_pop_set:
"tj_stack_pop tjs u ≤ SPEC (λ(tjs',scc). u ∈ set tjs ⟶ set tjs = set tjs' ∪ scc ∧ u ∈ scc)"
proof -
from tjs_union[of u tjs] show ?thesis
unfolding tj_stack_pop_def
by (refine_vcg) auto
qed
lemmas tj_stack_pop_set_leof_rule = weaken_SPEC[OF tj_stack_pop_set, THEN leof_lift]
definition tarjan_fin :: "'v ⇒ 'v tarjan_state ⇒ ('v,unit) tarjan_state_ext nres" where
"tarjan_fin v s = do {
let ll = (if stack s = [] then lowlink s
else let u = hd (stack s) in
(lowlink s)(u ↦ min (ζ s u) (ζ s v)));
let s' = s⦇ lowlink := ll ⦈;
ASSERT (v ∈ set (tj_stack s));
ASSERT (distinct (tj_stack s));
if ζ s v = δ s v then do {
ASSERT (scc_root' E s v (scc_of E v));
(tjs,scc) ← tj_stack_pop (tj_stack s) v;
RETURN (state.more (s'⦇ tj_stack := tjs, sccs := insert scc (sccs s)⦈))
} else do {
ASSERT (¬ scc_root' E s v (scc_of E v));
RETURN (state.more s')
}}"
definition tarjan_back :: "'v ⇒ 'v ⇒ 'v tarjan_state ⇒ ('v,unit) tarjan_state_ext nres" where
"tarjan_back u v s = (
if δ s v < δ s u ∧ v ∈ set (tj_stack s) then
let ul' = min (ζ s u) (δ s v)
in RETURN (state.more (s⦇ lowlink := (lowlink s)(u↦ul') ⦈))
else NOOP s)"
end
definition tarjan_params :: "'v tarjan_param" where
"tarjan_params = ⦇
on_init = RETURN ⦇ sccs = {}, lowlink = Map.empty, tj_stack = [] ⦈,
on_new_root = tarjan_disc,
on_discover = λu. tarjan_disc,
on_finish = tarjan_fin,
on_back_edge = tarjan_back,
on_cross_edge = tarjan_back,
is_break = λs. False ⦈"
schematic_goal tarjan_params_simps[simp]:
"on_init tarjan_params = ?OI"
"on_new_root tarjan_params = ?ONR"
"on_discover tarjan_params = ?OD"
"on_finish tarjan_params = ?OF"
"on_back_edge tarjan_params = ?OBE"
"on_cross_edge tarjan_params = ?OCE"
"is_break tarjan_params = ?IB"
unfolding tarjan_params_def gen_parameterization.simps
by (rule refl)+
sublocale param_DFS_defs G tarjan_params .
end
locale Tarjan = Tarjan_def G +
param_DFS G tarjan_params
for G :: "('v, 'more) graph_rec_scheme"
begin
lemma [simp]:
"sccs (empty_state ⦇sccs = s, lowlink = l, tj_stack = t⦈) = s"
"lowlink (empty_state ⦇sccs = s, lowlink = l, tj_stack = t⦈) = l"
"tj_stack (empty_state ⦇sccs = s, lowlink = l, tj_stack = t⦈) = t"
by (simp_all add: empty_state_def)
lemma sccs_more_cong[cong]:"state.more s = state.more s' ⟹ sccs s = sccs s'"
by (cases s, cases s') simp
lemma lowlink_more_cong[cong]:"state.more s = state.more s' ⟹ lowlink s = lowlink s'"
by (cases s, cases s') simp
lemma tj_stack_more_cong[cong]:"state.more s = state.more s' ⟹ tj_stack s = tj_stack s'"
by (cases s, cases s') simp
lemma [simp]:
"s⦇ state.more := ⦇sccs = sc, lowlink = l, tj_stack = t⦈⦈
= s⦇ sccs := sc, lowlink := l, tj_stack := t⦈"
by (cases s) simp
end
locale Tarjan_invar = Tarjan +
DFS_invar where param = tarjan_params
context Tarjan_def begin
lemma Tarjan_invar_eq[simp]:
"DFS_invar G tarjan_params s ⟷ Tarjan_invar G s" (is "?D ⟷ ?T")
proof
assume ?D then interpret DFS_invar where param=tarjan_params .
show ?T ..
next
assume ?T then interpret Tarjan_invar .
show ?D ..
qed
end
subsection ‹Correctness Proof›
context Tarjan begin
lemma i_tj_stack_discovered:
"is_invar (λs. set (tj_stack s) ⊆ dom (discovered s))"
proof (induct rule: establish_invarI)
case (finish s)
from finish show ?case
apply simp
unfolding tarjan_fin_def
apply (refine_vcg tj_stack_pop_set_leof_rule)
apply auto
done
qed (auto simp add: tarjan_disc_def tarjan_back_def)
lemmas (in Tarjan_invar) tj_stack_discovered =
i_tj_stack_discovered[THEN make_invar_thm]
lemma i_tj_stack_distinct:
"is_invar (λs. distinct (tj_stack s))"
proof (induct rule: establish_invarI_ND)
case (new_discover s s' v) then interpret Tarjan_invar where s=s by simp
from new_discover tj_stack_discovered have "v ∉ set (tj_stack s)" by auto
with new_discover show ?case by (simp add: tarjan_disc_def)
next
case (finish s) thus ?case
apply simp
unfolding tarjan_fin_def tj_stack_pop_def
apply (refine_vcg)
apply (auto intro: distinct_tl)
done
qed (simp_all add: tarjan_back_def)
lemmas (in Tarjan_invar) tj_stack_distinct =
i_tj_stack_distinct[THEN make_invar_thm]
context begin interpretation timing_syntax .
lemma i_tj_stack_incr_disc:
"is_invar (λs. ∀k<length (tj_stack s). ∀j<k. δ s (tj_stack s ! j) > δ s (tj_stack s ! k))"
proof (induct rule: establish_invarI_ND)
case (new_discover s s' v) then interpret Tarjan_invar where s=s by simp
from new_discover tj_stack_discovered have "v ∉ set (tj_stack s)" by auto
moreover {
fix k j
assume "k < Suc (length (tj_stack s))" "j < k"
hence "k - Suc 0 < length (tj_stack s)" by simp
hence "tj_stack s ! (k - Suc 0) ∈ set (tj_stack s)" using nth_mem by metis
with tj_stack_discovered timing_less_counter have "δ s (tj_stack s ! (k - Suc 0)) < counter s" by blast
}
moreover {
fix k j
define k' where "k' = k - Suc 0"
define j' where "j' = j - Suc 0"
assume A: "k < Suc (length (tj_stack s))" "j < k" "(v#tj_stack s) ! j ≠ v"
hence gt_0: "j > 0 ∧ k>0" by (cases "j=0") simp_all
moreover with ‹j < k› have "j' < k'" by (simp add: j'_def k'_def)
moreover from A have "k' < length (tj_stack s)" by (simp add: k'_def)
ultimately have "δ s (tj_stack s ! j') > δ s (tj_stack s ! k')"
using new_discover by blast
with gt_0 have "δ s ((v#tj_stack s) ! j) > δ s (tj_stack s ! k')"
unfolding j'_def
by (simp add: nth_Cons')
}
ultimately show ?case
using new_discover
by (auto simp add: tarjan_disc_def)
next
case (finish s s' u)
{
let ?dw = "dropWhile ((≠) u) (tj_stack s)"
let ?tw = "takeWhile ((≠) u) (tj_stack s)"
fix a k j
assume A: "a = tl ?dw" "k < length a" "j < k"
and "u ∈ set (tj_stack s)"
hence "?dw ≠ []" by auto
define j' k' where "j' = Suc j + length ?tw" and "k' = Suc k + length ?tw"
with ‹j < k› have "j' < k'" by simp
have "length (tj_stack s) = length ?tw + length ?dw"
by (simp add: length_append[symmetric])
moreover from A have *: "Suc k < length ?dw" and **: "Suc j < length ?dw" by auto
ultimately have "k' < length (tj_stack s)" by (simp add: k'_def)
with finish ‹j'<k'› have "δ s (tj_stack s ! k') < δ s (tj_stack s ! j')" by simp
also from dropWhile_nth[OF *] have "tj_stack s ! k' = ?dw ! Suc k"
by (simp add: k'_def)
also from dropWhile_nth[OF **] have "tj_stack s ! j' = ?dw ! Suc j"
by (simp add: j'_def)
also from nth_tl[OF ‹?dw ≠ []›] have "?dw ! Suc k = a ! k" by (simp add: A)
also from nth_tl[OF ‹?dw ≠ []›] have "?dw ! Suc j = a ! j" by (simp add: A)
finally have "δ s (a ! k) < δ s (a ! j)" .
} note aux = this
from finish show ?case
apply simp
unfolding tarjan_fin_def tj_stack_pop_def
apply refine_vcg
apply (auto intro!: aux)
done
qed (simp_all add: tarjan_back_def)
end end
context Tarjan_invar begin context begin interpretation timing_syntax .
lemma tj_stack_incr_disc:
assumes "k < length (tj_stack s)"
and "j < k"
shows "δ s (tj_stack s ! j) > δ s (tj_stack s ! k)"
using assms i_tj_stack_incr_disc[THEN make_invar_thm]
by blast
lemma tjs_disc_dw_tw:
fixes u
defines "dw ≡ dropWhile ((≠) u) (tj_stack s)"
defines "tw ≡ takeWhile ((≠) u) (tj_stack s)"
assumes "x ∈ set dw" "y ∈ set tw"
shows "δ s x < δ s y"
proof -
from assms obtain k where k: "dw ! k = x" "k < length dw" by (metis in_set_conv_nth)
from assms obtain j where j: "tw ! j = y" "j < length tw" by (metis in_set_conv_nth)
have "length (tj_stack s) = length tw + length dw"
by (simp add: length_append[symmetric] tw_def dw_def)
with k j have "δ s (tj_stack s ! (k + length tw)) < δ s (tj_stack s ! j)"
by (simp add: tj_stack_incr_disc)
also from j takeWhile_nth have "tj_stack s ! j = y" by (metis tw_def)
also from dropWhile_nth k have "tj_stack s ! (k + length tw) = x" by (metis tw_def dw_def)
finally show ?thesis .
qed
end end
context Tarjan begin context begin interpretation timing_syntax .
lemma i_sccs_finished_stack_ss_tj_stack:
"is_invar (λs. ⋃(sccs s) ⊆ dom (finished s) ∧ set (stack s) ⊆ set (tj_stack s))"
proof (induct rule: establish_invarI)
case (finish s s' u) then interpret Tarjan_invar where s=s by simp
let ?tw = "takeWhile ((≠) u) (tj_stack s)"
let ?dw = "dropWhile ((≠) u) (tj_stack s)"
{
fix x
assume A: "x ≠ u" "x ∈ set ?tw" "u ∈ set (tj_stack s)"
hence x_tj: "x ∈ set (tj_stack s)" by (auto dest: set_takeWhileD)
have "x ∈ dom (finished s)"
proof (rule ccontr)
assume "x ∉ dom (finished s)"
with x_tj tj_stack_discovered discovered_eq_finished_un_stack have "x ∈ set (stack s)" by blast
with ‹x≠u› finish have "x ∈ set (tl (stack s))" by (cases "stack s") auto
with tl_lt_stack_hd_discover finish have *: "δ s x < δ s u" by simp
from A have "?dw ≠ []" by simp
with hd_dropWhile[OF this] hd_in_set have "u ∈ set ?dw" by metis
with tjs_disc_dw_tw ‹x ∈ set ?tw› have "δ s u < δ s x" by simp
with * show False by force
qed
hence "∃y. finished s x = Some y" by blast
} note aux_scc = this
{
fix x
assume A: "x ∈ set (tl (stack s))" "u ∈ set (tj_stack s)"
with finish stack_distinct have "x ≠ u" by (cases "stack s") auto
moreover
from A have "x ∈ set (stack s)" by (metis in_set_tlD)
with stack_not_finished have "x ∉ dom (finished s)" by simp
with A aux_scc[OF ‹x ≠ u›] have "x ∉ set ?tw" by blast
moreover
from finish ‹x ∈ set (stack s)› have "x ∈ set (tj_stack s)" by auto
moreover note tjs_union[OF ‹u ∈ set (tj_stack s)›]
ultimately have "x ∈ set (tl ?dw)" by blast
} note aux_tj = this
from finish show ?case
apply simp
unfolding tarjan_fin_def tj_stack_pop_def
apply (refine_vcg)
using aux_scc aux_tj apply (auto dest: in_set_tlD)
done
qed (auto simp add: tarjan_disc_def tarjan_back_def)
lemma i_tj_stack_ss_stack_finished:
"is_invar (λs. set (tj_stack s) ⊆ set (stack s) ∪ dom (finished s))"
proof (induct rule: establish_invarI)
case (finish s) thus ?case
apply simp
unfolding tarjan_fin_def
apply (refine_vcg tj_stack_pop_set_leof_rule)
apply ((simp, cases "stack s", simp_all)[])+
done
qed (auto simp add: tarjan_disc_def tarjan_back_def)
lemma i_finished_ss_sccs_tj_stack:
"is_invar (λs. dom (finished s) ⊆ ⋃(sccs s) ∪ set (tj_stack s))"
proof (induction rule: establish_invarI_ND)
case (new_discover s s' v) then interpret Tarjan_invar where s=s by simp
from new_discover finished_discovered have "v ∉ dom (finished s)" by auto
with new_discover show ?case
by (auto simp add: tarjan_disc_def)
next
case (finish s s' u) then interpret Tarjan_invar where s=s by simp
from finish show ?case
apply simp
unfolding tarjan_fin_def
apply (refine_vcg tj_stack_pop_set_leof_rule)
apply auto
done
qed (simp_all add: tarjan_back_def)
end end
context Tarjan_invar begin
lemmas finished_ss_sccs_tj_stack =
i_finished_ss_sccs_tj_stack[THEN make_invar_thm]
lemmas tj_stack_ss_stack_finished =
i_tj_stack_ss_stack_finished[THEN make_invar_thm]
lemma sccs_finished:
"⋃(sccs s) ⊆ dom (finished s)"
using i_sccs_finished_stack_ss_tj_stack[THEN make_invar_thm]
by blast
lemma stack_ss_tj_stack:
"set (stack s) ⊆ set (tj_stack s)"
using i_sccs_finished_stack_ss_tj_stack[THEN make_invar_thm]
by blast
lemma hd_stack_in_tj_stack:
"stack s ≠ [] ⟹ hd (stack s) ∈ set (tj_stack s)"
using stack_ss_tj_stack hd_in_set
by auto
end
context Tarjan begin context begin interpretation timing_syntax .
lemma i_no_finished_root:
"is_invar (λs. scc_root s r scc ∧ r ∈ dom (finished s) ⟶ (∀x ∈ scc. x ∉ set (tj_stack s)))"
proof (induct rule: establish_invarI_ND_CB)
case (new_discover s s' v) then interpret Tarjan_invar where s=s by simp
{
fix x
let ?s = "s'⦇state.more := x⦈"
assume TRANS: "⋀Ψ. tarjan_disc v s' ≤⇩n SPEC Ψ ⟹ Ψ x"
and inv': "DFS_invar G tarjan_params (s'⦇state.more := x⦈)"
and r: "scc_root ?s r scc" "r ∈ dom (finished s')"
from inv' interpret s': Tarjan_invar where s="?s" by simp
have "tj_stack ?s = v#tj_stack s"
by (rule TRANS) (simp add: new_discover tarjan_disc_def)
moreover
from r s'.scc_root_finished_impl_scc_finished have "scc ⊆ dom (finished ?s)" by auto
with new_discover finished_discovered have "v ∉ scc" by force
moreover
from r finished_discovered new_discover have "r ∈ dom (discovered s)" by auto
with r inv' new_discover have "scc_root s r scc"
apply (intro scc_root_transfer[where s'="?s", THEN iffD2])
apply clarsimp_all
done
with new_discover r have "∀x ∈ scc. x ∉ set (tj_stack s')" by simp
ultimately have "∀x∈scc. x ∉ set (tj_stack ?s)" by (auto simp: new_discover)
}
with new_discover show ?case by (simp add: pw_leof_iff)
next
case (cross_back_edge s s' u v) then interpret Tarjan_invar where s=s by simp
{
fix x
let ?s = "s'⦇state.more := x⦈"
assume TRANS: "⋀Ψ. tarjan_back u v s' ≤⇩n SPEC Ψ ⟹ Ψ x"
and r: "scc_root ?s r scc" "r ∈ dom (finished s')"
with cross_back_edge have "scc_root s r scc"
by (simp add: scc_root_transfer'[where s'="?s"])
moreover
have "tj_stack ?s = tj_stack s" by (rule TRANS) (simp add: cross_back_edge tarjan_back_def)
ultimately have "∀x∈scc. x ∉ set (tj_stack ?s)"
using cross_back_edge r by simp
}
with cross_back_edge show ?case by (simp add: pw_leof_iff)
next
case (finish s s' u) then interpret Tarjan_invar where s=s by simp
{
fix x
let ?s = "s'⦇state.more := x⦈"
assume TRANS: "⋀Ψ. tarjan_fin u s' ≤⇩n SPEC Ψ ⟹ Ψ x"
and inv': "DFS_invar G tarjan_params (s'⦇state.more := x⦈)"
and r: "scc_root ?s r scc" "r ∈ dom (finished s')"
from inv' interpret s': Tarjan_invar where s="?s" by simp
have "∀x∈scc. x ∉ set (tj_stack ?s)"
proof (cases "r = u")
case False with finish r have "∀x∈scc. x ∉ set (tj_stack s)"
using scc_root_transfer'[where s'="?s"]
by simp
moreover have "set (tj_stack ?s) ⊆ set (tj_stack s)"
apply (rule TRANS)
unfolding tarjan_fin_def
apply (refine_vcg tj_stack_pop_set_leof_rule)
apply (simp_all add: finish)
done
ultimately show ?thesis by blast
next
case True with r s'.scc_root_unique_is_scc have "scc_root ?s u (scc_of E u)" by simp
with s'.scc_root_transfer'[where s'=s'] finish have "scc_root s' u (scc_of E u)" by simp
moreover
hence [simp]: "tj_stack ?s = tl (dropWhile ((≠) u) (tj_stack s))"
apply (rule_tac TRANS)
unfolding tarjan_fin_def tj_stack_pop_def
apply (refine_vcg)
apply (simp_all add: finish)
done
{
let ?dw = "dropWhile ((≠) u) (tj_stack s)"
let ?tw = "takeWhile ((≠) u) (tj_stack s)"
fix x
define j::nat where "j = 0"
assume x: "x ∈ set (tj_stack ?s)"
then obtain i where i: "i < length (tj_stack ?s)" "tj_stack ?s ! i = x"
by (metis in_set_conv_nth)
have "length (tj_stack s) = length ?tw + length ?dw"
by (simp add: length_append[symmetric])
with i have "δ s (tj_stack s ! (Suc i + length ?tw)) < δ s (tj_stack s ! length ?tw)"
by (simp add: tj_stack_incr_disc)
also from hd_stack_in_tj_stack finish have ne: "?dw ≠ []" and "length ?dw > 0" by simp_all
from hd_dropWhile[OF ne] hd_conv_nth[OF ne] have "?dw ! 0 = u" by simp
with dropWhile_nth[OF ‹length ?dw > 0›] have "tj_stack s ! length ?tw = u" by simp
also from i have "?dw ! Suc i = x" "Suc i < length ?dw" by (simp_all add: nth_tl[OF ne])
with dropWhile_nth[OF this(2)] have "tj_stack s ! (Suc i + length ?tw) = x" by simp
finally have "δ ?s x < δ ?s u" by (simp add: finish)
moreover from x s'.tj_stack_discovered have "x ∈ dom (discovered ?s)" by auto
ultimately have "x ∉ scc" using s'.scc_root_disc_le r True by force
} thus ?thesis by metis
qed
}
with finish show ?case by (simp add: pw_leof_iff)
qed simp_all
end end
context Tarjan_invar begin
lemma no_finished_root:
assumes "scc_root s r scc"
and "r ∈ dom (finished s)"
and "x ∈ scc"
shows "x ∉ set (tj_stack s)"
using assms
using i_no_finished_root[THEN make_invar_thm]
by blast
context begin interpretation timing_syntax .
lemma tj_stack_reach_stack:
assumes "u ∈ set (tj_stack s)"
shows "∃v ∈ set (stack s). (u,v) ∈ E⇧* ∧ δ s v ≤ δ s u"
proof -
have u_scc: "u ∈ scc_of E u" by simp
from assms tj_stack_discovered have u_disc: "u ∈ dom (discovered s)" by auto
with scc_root_of_node_exists obtain r where r: "scc_root s r (scc_of E u)" by blast
have "r ∈ set (stack s)"
proof (rule ccontr)
assume "r ∉ set (stack s)"
with r[unfolded scc_root_def] stack_set_def have "r ∈ dom (finished s)" by simp
with u_scc have "u ∉ set (tj_stack s)" using no_finished_root r by blast
with assms show False by contradiction
qed
moreover from r scc_reach_scc_root u_scc u_disc have "(u,r) ∈ E⇧*" by blast
moreover from r scc_root_disc_le u_scc u_disc have "δ s r ≤ δ s u" by blast
ultimately show ?thesis by metis
qed
lemma tj_stack_reach_hd_stack:
assumes "v ∈ set (tj_stack s)"
shows "(v, hd (stack s)) ∈ E⇧*"
proof -
from tj_stack_reach_stack assms obtain r where r: "r ∈ set (stack s)" "(v,r) ∈ E⇧*" by blast
hence "r = hd (stack s) ∨ r ∈ set (tl (stack s))" by (cases "stack s") auto
thus ?thesis
proof
assume "r = hd (stack s)" with r show ?thesis by simp
next
from r have ne :"stack s ≠ []" by auto
assume "r ∈ set (tl (stack s))"
with tl_stack_hd_tree_path ne have "(r,hd (stack s)) ∈ (tree_edges s)⇧+" by simp
with trancl_mono_mp tree_edges_ssE have "(r,hd (stack s))∈E⇧*" by (metis rtrancl_eq_or_trancl)
with ‹(v,r)∈E⇧*› show ?thesis by (metis rtrancl_trans)
qed
qed
lemma empty_stack_imp_empty_tj_stack:
assumes "stack s = []"
shows "tj_stack s = []"
proof (rule ccontr)
assume ne: "tj_stack s ≠ []"
then obtain x where x: "x ∈ set (tj_stack s)" by auto
with tj_stack_reach_stack obtain r where "r ∈ set (stack s)" by auto
with assms show False by simp
qed
lemma stacks_eq_iff: "stack s = [] ⟷ tj_stack s = []"
using empty_stack_imp_empty_tj_stack stack_ss_tj_stack
by auto
end end
context Tarjan begin context begin interpretation timing_syntax .
lemma i_sccs_are_sccs:
"is_invar (λs. ∀scc ∈ sccs s. is_scc E scc)"
proof (induction rule: establish_invarI)
case (finish s s' u) then interpret Tarjan_invar where s=s by simp
from finish have EQ[simp]:
"finished s' = (finished s)(u ↦ counter s)"
"discovered s' = discovered s"
"tree_edges s' = tree_edges s"
"sccs s' = sccs s"
"tj_stack s' = tj_stack s"
by simp_all
{
fix x
let ?s = "s'⦇state.more := x⦈"
assume TRANS: "⋀Ψ. tarjan_fin u s' ≤⇩n SPEC Ψ ⟹ Ψ x"
and inv': "DFS_invar G tarjan_params (s'⦇state.more := x⦈)"
then interpret s': Tarjan_invar where s="?s" by simp
from finish hd_in_set stack_set_def have
u_disc: "u ∈ dom (discovered s)"
and u_n_fin: "u ∉ dom (finished s)" by blast+
have "∀scc ∈ sccs ?s. is_scc E scc"
proof (cases "scc_root s' u (scc_of E u)")
case False
have "sccs ?s = sccs s"
apply (rule TRANS)
unfolding tarjan_fin_def tj_stack_pop_def
by (refine_vcg) (simp_all add: False)
thus ?thesis by (simp add: finish)
next
case True
let ?dw = "dropWhile ((≠) u) (tj_stack s)"
let ?tw = "takeWhile ((≠) u) (tj_stack s)"
let ?tw' = "insert u (set ?tw)"
have [simp]: "sccs ?s = insert ?tw' (sccs s)"
apply (rule TRANS)
unfolding tarjan_fin_def tj_stack_pop_def
by (refine_vcg) (simp_all add: True)
have [simp]: "tj_stack ?s = tl ?dw"
apply (rule TRANS)
unfolding tarjan_fin_def tj_stack_pop_def
by (refine_vcg) (simp_all add: True)
from True scc_root_transfer'[where s'=s'] have "scc_root s u (scc_of E u)" by simp
with inv' scc_root_transfer[where s'="?s"] u_disc have u_root: "scc_root ?s u (scc_of E u)" by simp
have "?tw' ⊆ scc_of E u"
proof
fix v assume v: "v ∈ ?tw'"
show "v ∈ scc_of E u"
proof cases
assume "v ≠ u" with v have v: "v ∈ set ?tw" by auto
hence v_tj: "v ∈ set (tj_stack s)" by (auto dest: set_takeWhileD)
with tj_stack_discovered have v_disc: "v ∈ dom (discovered s)" by auto
from hd_stack_in_tj_stack finish have "?dw ≠ []" by simp
with hd_dropWhile[OF this] hd_in_set have "u ∈ set ?dw" by metis
with v have "δ s v > δ s u" using tjs_disc_dw_tw by blast
moreover have "v ∈ dom (finished s)"
proof (rule ccontr)
assume "v ∉ dom (finished s)"
with v_disc stack_set_def have "v ∈ set (stack s)" by auto
with ‹v≠u› finish have "v ∈ set (tl (stack s))" by (cases "stack s") auto
with tl_lt_stack_hd_discover finish have "δ s v < δ s u" by simp
with ‹δ s v > δ s u› show False by force
qed
ultimately have "(u,v) ∈ (tree_edges s)⇧+"
using parenthesis_impl_tree_path_not_finished[OF u_disc] u_n_fin
by force
with trancl_mono_mp tree_edges_ssE have "(u,v)∈E⇧*" by (metis rtrancl_eq_or_trancl)
moreover
from tj_stack_reach_hd_stack v_tj finish have "(v,u)∈E⇧*" by simp
moreover have "is_scc E (scc_of E u)" "u ∈ scc_of E u" by simp_all
ultimately show ?thesis using is_scc_closed by metis
qed simp
qed
moreover have "scc_of E u ⊆ ?tw'"
proof
fix v assume v: "v ∈ scc_of E u"
moreover note u_root
moreover have "u ∈ dom (finished ?s)" by simp
ultimately have "v ∈ dom (finished ?s)" "v ∉ set (tj_stack ?s)"
using s'.scc_root_finished_impl_scc_finished s'.no_finished_root
by auto
with s'.finished_ss_sccs_tj_stack have "v ∈ ⋃(sccs ?s)" by blast
hence "v ∈ ⋃(sccs s) ∨ v ∈ ?tw'" by auto
thus "v ∈ ?tw'"
proof
assume "v ∈ ⋃(sccs s)"
then obtain scc where scc: "v ∈ scc" "scc ∈ sccs s" by auto
moreover with finish have "is_scc E scc" by simp
moreover have "is_scc E (scc_of E u)" by simp
moreover note v
ultimately have "scc = scc_of E u" using is_scc_unique by metis
hence "u ∈ scc" by simp
with scc sccs_finished have "u ∈ dom (finished s)" by auto
with u_n_fin show ?thesis by contradiction
qed simp
qed
ultimately have "?tw' = scc_of E u" by auto
hence "is_scc E ?tw'" by simp
with finish show ?thesis by auto
qed
}
thus ?case by (auto simp: pw_leof_iff finish)
qed (simp_all add: tarjan_back_def tarjan_disc_def)
end
lemmas (in Tarjan_invar) sccs_are_sccs =
i_sccs_are_sccs[THEN make_invar_thm]
context begin interpretation timing_syntax .
lemma i_lowlink_eq_LowLink:
"is_invar (λs. ∀x ∈ dom (discovered s). ζ s x = LowLink s x)"
proof -
{
fix s s' :: "'v tarjan_state"
fix v w
fix x
let ?s = "s'⦇state.more := x⦈"
assume pre_ll_sub_rev: "⋀w. ⟦Tarjan_invar G ?s; w ∈ dom (discovered ?s); w ≠ v⟧ ⟹ lowlink_set ?s w ⊆ lowlink_set s w ∪ {v}"
assume tree_sub : "tree_edges s' = tree_edges s ∨ (∃u. u ≠ v ∧ tree_edges s' = tree_edges s ∪ {(u,v)})"
assume "Tarjan_invar G s"
assume [simp]: "discovered s' = (discovered s)(v ↦ counter s)"
"finished s' = finished s"
"lowlink s' = lowlink s"
"cross_edges s' = cross_edges s" "back_edges s' = back_edges s"
assume v_n_disc: "v ∉ dom (discovered s)"
assume IH: "⋀w. w∈dom (discovered s) ⟹ ζ s w = LowLink s w"
assume TRANS: "⋀Ψ. tarjan_disc v s' ≤⇩n SPEC Ψ ⟹ Ψ x"
and INV: "DFS_invar G tarjan_params ?s"
and w_disc: "w ∈ dom (discovered ?s)"
interpret Tarjan_invar where s=s by fact
from INV interpret s':Tarjan_invar where s="?s" by simp
have [simp]: "lowlink ?s = (lowlink s)(v ↦ counter s)"
by (rule TRANS) (auto simp: tarjan_disc_def)
from v_n_disc edge_imp_discovered have "edges s `` {v} = {}" by auto
with tree_sub tree_edge_imp_discovered have "edges ?s `` {v} = {}" by auto
with s'.no_path_imp_no_lowlink_path have "⋀w. ¬(∃p. lowlink_path ?s v p w)" by metis
hence ll_v: "lowlink_set ?s v = {v}"
unfolding lowlink_set_def by auto
have "ζ ?s w = LowLink ?s w"
proof (cases "w=v")
case True with ll_v show ?thesis by simp
next
case False hence "ζ ?s w = ζ s w" by simp
also from IH have "ζ s w = LowLink s w" using w_disc False by simp
also have "LowLink s w = LowLink ?s w"
proof (rule LowLink_eqI[OF INV])
from v_n_disc show "discovered s ⊆⇩m discovered ?s" by (simp add: map_le_def)
from tree_sub show "lowlink_set s w ⊆ lowlink_set ?s w"
unfolding lowlink_set_def lowlink_path_def
by auto
show "lowlink_set ?s w ⊆ lowlink_set s w ∪ {v}"
proof (cases "w = v")
case True with ll_v show ?thesis by auto
next
case False thus ?thesis
using pre_ll_sub_rev w_disc INV
by simp
qed
show "w ∈ dom (discovered s)" using w_disc False by simp
fix ll assume "ll ∈ {v}" with timing_less_counter lowlink_set_discovered have
"⋀x. x∈δ s`lowlink_set s w ⟹ x < δ ?s ll" by simp force
moreover from Min_in lowlink_set_finite lowlink_set_not_empty w_disc False have
"LowLink s w ∈ δ s`lowlink_set s w " by auto
ultimately show "LowLink s w ≤ δ ?s ll" by force
qed
finally show ?thesis .
qed
} note tarjan_disc_aux = this
show ?thesis
proof (induct rule: establish_invarI_CB)
case (new_root s s' v0)
{
fix w x
let ?s = "new_root v0 s⦇state.more := x⦈"
have "lowlink_set ?s w ⊆ lowlink_set s w ∪ {v0}"
unfolding lowlink_set_def lowlink_path_def
by auto
} note * = this
from new_root show ?case
using tarjan_disc_aux[OF *]
by (auto simp add: pw_leof_iff)
next
case (discover s s' u v) then interpret Tarjan_invar where s=s by simp
let ?s' = "discover (hd (stack s)) v (s⦇pending := pending s - {(hd (stack s),v)}⦈)"
{
fix w x
let ?s = "?s'⦇state.more := x⦈"
assume INV: "Tarjan_invar G ?s"
and d: "w ∈ dom (discovered ?s')"
and "w≠v"
interpret s': Tarjan_invar where s="?s" by fact
have "lowlink_set ?s w ⊆ lowlink_set s w ∪ {v}"
proof
fix ll
assume ll: "ll ∈ lowlink_set ?s w"
hence "ll = w ∨ (∃p. lowlink_path ?s w p ll)" by (auto simp add: lowlink_set_def)
thus "ll ∈ lowlink_set s w ∪ {v}" (is "ll ∈ ?L")
proof
assume "ll = w" with d show ?thesis by (auto simp add: lowlink_set_def)
next
assume "∃p. lowlink_path ?s w p ll"
then obtain p where p: "lowlink_path ?s w p ll" ..
hence [simp]: "p≠[]" by (simp add: lowlink_path_def)
from p have "hd p = w" by (auto simp add: lowlink_path_def path_hd)
show ?thesis
proof (rule tri_caseE)
assume "v≠ll" "v ∉ set p" hence "lowlink_path s w p ll"
using p by (auto simp add: lowlink_path_def)
with ll show ?thesis by (auto simp add: lowlink_set_def)
next
assume "v = ll" thus ?thesis by simp
next
assume "v ∈ set p" "v ≠ ll"
then obtain i where i: "i < length p" "p!i = v"
by (metis in_set_conv_nth)
have "False"
proof (cases i)
case "0" with i have "hd p = v" by (simp add: hd_conv_nth)
with ‹hd p = w› ‹w ≠ v› show False by simp
next
case (Suc n) with i s'.lowlink_path_finished[OF p, where j=i] have
"v ∈ dom (finished ?s)" by simp
with finished_discovered discover show False by auto
qed
thus ?thesis ..
qed
qed
qed
} note * = this
from discover hd_in_set stack_set_def have "v ≠ u" by auto
with discover have **: "tree_edges ?s' = tree_edges s ∨ (∃u. u ≠ v ∧ tree_edges ?s' = tree_edges s ∪ {(u,v)})" by auto
from discover show ?case
using tarjan_disc_aux[OF * **]
by (auto simp: pw_leof_iff)
next
case (cross_back_edge s s' u v) then interpret Tarjan_invar where s=s by simp
from cross_back_edge have [simp]:
"discovered s' = discovered s"
"finished s' = finished s"
"tree_edges s' = tree_edges s"
"lowlink s' = lowlink s"
by simp_all
{
fix w :: "'v"
fix x
let ?s = "s'⦇state.more := x⦈"
let ?L = "δ s ` lowlink_set s w"
let ?L' = "δ ?s ` lowlink_set ?s w"
assume TRANS: "⋀Ψ. tarjan_back u v s' ≤⇩n SPEC Ψ ⟹ Ψ x"
and inv': "DFS_invar G tarjan_params ?s"
and w_disc': "w ∈ dom (discovered ?s)"
from inv' interpret s':Tarjan_invar where s="?s" by simp
have ll_sub: "lowlink_set s w ⊆ lowlink_set ?s w"
unfolding lowlink_set_def lowlink_path_def
by (auto simp: cross_back_edge)
have ll_sub_rev: "lowlink_set ?s w ⊆ lowlink_set s w ∪ {v}"
unfolding lowlink_set_def lowlink_path_def
by (auto simp: cross_back_edge)
from w_disc' have w_disc: "w ∈ dom (discovered s)" by simp
with LowLink_le_disc have LLw: "LowLink s w ≤ δ s w" by simp
from cross_back_edge hd_in_set have u_n_fin: "u ∉ dom (finished s)"
using stack_not_finished by auto
{
assume *: "v ∈ lowlink_set ?s w ⟹ LowLink s w ≤ δ ?s v"
have "LowLink s w = LowLink ?s w"
proof (rule LowLink_eqI[OF inv' _ ll_sub ll_sub_rev w_disc])
show "discovered s ⊆⇩m discovered ?s" by simp
fix ll assume "ll ∈ {v}" "ll ∈ lowlink_set ?s w"
with * show "LowLink s w ≤ δ ?s ll" by simp
qed
} note LL_eqI = this
have "ζ ?s w = LowLink ?s w"
proof (cases "w=u")
case True show ?thesis
proof (cases "(δ s v < δ s w ∧ v ∈ set (tj_stack s) ∧ δ s v < ζ s w)")
case False note all_False = this
with ‹w = u› have "ζ ?s w = ζ s w"
by (rule_tac TRANS) (auto simp add: tarjan_back_def cross_back_edge)
also from cross_back_edge w_disc have ζw: "... = LowLink s w" by simp
also have "LowLink s w = LowLink ?s w"
proof (rule LL_eqI)
assume v: "v ∈ lowlink_set ?s w"
show "LowLink s w ≤ δ ?s v"
proof (cases "δ s v < δ s w ∧ δ s v < ζ s w")
case False with ‹LowLink s w ≤ δ s w› ζw show ?thesis by auto
next
case True with all_False have v_n_tj: "v ∉ set (tj_stack s)" by simp
from v have e: "(v,u) ∈ E⇧*" "(u,v) ∈ E⇧*"
unfolding lowlink_set_def by (auto simp add: ‹w=u›)
from v_n_tj have "v ∉ set (stack s)" using stack_ss_tj_stack by auto
with cross_back_edge have "v ∈ dom (finished s)" by (auto simp add: stack_set_def)
with finished_ss_sccs_tj_stack v_n_tj sccs_are_sccs obtain scc
where scc: "v ∈ scc" "scc ∈ sccs s" "is_scc E scc" by blast
with is_scc_closed e have "u ∈ scc" by metis
with scc sccs_finished u_n_fin have False by blast
thus ?thesis ..
qed
qed
finally show ?thesis .
next
case True note all_True = this
with ‹w=u› have "ζ ?s w = δ s v"
by (rule_tac TRANS) (simp add: tarjan_back_def cross_back_edge)
also from True cross_back_edge w_disc have "δ s v < LowLink s w" by simp
with lowlink_set_finite lowlink_set_not_empty w_disc have "δ s v = Min (?L ∪ {δ s v})" by simp
also have "v ∈ lowlink_set ?s w"
proof -
have cb: "(u,v) ∈ cross_edges ?s ∪ back_edges ?s" by (simp add: cross_back_edge)
with s'.lowlink_path_single have "lowlink_path ?s u [u] v" by auto
moreover from cb s'.cross_edges_ssE s'.back_edges_ssE have "(u,v) ∈ E" by blast
hence "(u,v) ∈ E⇧*" ..
moreover from all_True tj_stack_reach_hd_stack have "(v,u) ∈ E⇧*" by (simp add: cross_back_edge)
moreover note ‹v ∈ dom (discovered s)›
ultimately show ?thesis by (auto intro: s'.lowlink_setI simp: ‹w=u›)
qed
with ll_sub ll_sub_rev have "lowlink_set ?s w = lowlink_set s w ∪ {v}" by auto
hence "Min (?L ∪ {δ s v}) = LowLink ?s w" by simp
finally show ?thesis .
qed
next
case False
hence "ζ ?s w = ζ s w"
by (rule_tac TRANS) (simp add: tarjan_back_def cross_back_edge)
also have "ζ s w = LowLink s w" using w_disc False by (simp add: cross_back_edge)
also have "LowLink s w = LowLink ?s w"
proof (rule LL_eqI)
assume v: "v ∈ lowlink_set ?s w"
thus "LowLink s w ≤ δ ?s v" using LLw
proof cases
assume "v ≠ w"
with v obtain p where p: "lowlink_path ?s w p v" "p≠[]"
by (auto simp add: lowlink_set_def lowlink_path_def)
hence "hd p = w" by (auto simp add: lowlink_path_def path_hd)
show ?thesis
proof (cases "u ∈ set p")
case False with last_in_set p cross_back_edge have "last p ≠ hd (stack s)" by force
with p have "lowlink_path s w p v"
by (auto simp: cross_back_edge lowlink_path_def)
with v have "v ∈ lowlink_set s w"
by (auto intro: lowlink_setI simp: lowlink_set_def cross_back_edge)
thus ?thesis by simp
next
case True then obtain i where i: "i < length p" "p!i = u"
by (metis in_set_conv_nth)
have "False"
proof (cases i)
case "0" with i have "hd p = u" by (simp add: hd_conv_nth)
with ‹hd p = w› ‹w ≠ u› show False by simp
next
case (Suc n) with i s'.lowlink_path_finished[OF p(1), where j=i] have
"u ∈ dom (finished ?s)" by simp
with u_n_fin show ?thesis by simp
qed
thus ?thesis ..
qed
qed simp
qed
finally show ?thesis .
qed
} note aux = this
with cross_back_edge show ?case by (auto simp: pw_leof_iff)
next
case (finish s s' u) then interpret Tarjan_invar where s=s by simp
from finish have [simp]:
"discovered s' = discovered s"
"finished s' = (finished s)(u↦counter s)"
"tree_edges s' = tree_edges s"
"back_edges s' = back_edges s"
"cross_edges s' = cross_edges s"
"lowlink s' = lowlink s" "tj_stack s' = tj_stack s"
by simp_all
from finish hd_in_set stack_discovered have u_disc: "u ∈ dom (discovered s)" by blast
{
fix w :: "'v"
fix x
let ?s = "s'⦇state.more := x⦈"
let ?L = "δ s ` lowlink_set s w"
let ?Lu = "δ s ` lowlink_set s u"
let ?L' = "δ s ` lowlink_set ?s w"
assume TRANS: "⋀Ψ. tarjan_fin u s' ≤⇩n SPEC Ψ ⟹ Ψ x"
and inv': "DFS_invar G tarjan_params ?s"
and w_disc: "w ∈ dom (discovered ?s)"
from inv' interpret s':Tarjan_invar where s="?s" by simp
have ll_sub: "lowlink_set s w ⊆ lowlink_set ?s w"
unfolding lowlink_set_def lowlink_path_def
by auto
have ll_sub_rev: "lowlink_set ?s w ⊆ lowlink_set s w ∪ lowlink_set s u"
proof
fix ll
assume ll: "ll ∈ lowlink_set ?s w"
hence "ll = w ∨ (∃p. lowlink_path ?s w p ll)" by (auto simp add: lowlink_set_def)
thus "ll ∈ lowlink_set s w ∪ lowlink_set s u"
proof (rule disjE1)
assume "ll = w" with w_disc show ?thesis by (auto simp add: lowlink_set_def)
next
assume "ll ≠ w"
assume "∃p. lowlink_path ?s w p ll"
then obtain p where p: "lowlink_path ?s w p ll" ..
hence [simp]: "p≠[]" by (simp add: lowlink_path_def)
from p have "hd p = w" by (auto simp add: lowlink_path_def path_hd)
show ?thesis
proof (cases "u ∈ set p")
case False hence "lowlink_path s w p ll"
using p by (auto simp add: lowlink_path_def)
with ll show ?thesis by (auto simp add: lowlink_set_def)
next
case True
then obtain i where i: "i < length p" "p!i = u"
by (metis in_set_conv_nth)
moreover
let ?dp = "drop i p"
from i have "?dp ≠ []" by simp
from i have "hd ?dp = u" by (simp add: hd_drop_conv_nth)
moreover from i have "last ?dp = last p" by simp
moreover {
fix k
assume "1 < length ?dp"
and "k < length ?dp - 1"
hence l: "1 < length p" "k+i < length p - 1" by (auto)
with p have "(p!(k+i), p!Suc (k+i)) ∈ tree_edges s" by (auto simp add: lowlink_path_def)
moreover from l have i: "i+k ≤ length p" "i+Suc k ≤ length p" by simp_all
ultimately have "(?dp!k,?dp!Suc k) ∈ tree_edges s" by (simp add: add.commute)
} note aux = this
moreover {
assume *: "1 < length ?dp"
hence l: "1 + i < length p" by simp
with s'.lowlink_path_finished[OF p] have "p ! (1+i) ∈ dom (finished ?s)" by auto
moreover from l have "i+1≤length p" by simp
ultimately have "?dp!1 ∈ dom (finished ?s)" by simp
moreover from aux[of 0] * have "(?dp!0,?dp!Suc 0) ∈ tree_edges s" by simp
with ‹hd ?dp = u› hd_conv_nth[of "?dp"] * have "(u,?dp!Suc 0) ∈ tree_edges s" by simp
with no_self_loop_in_tree have "?dp!1 ≠ u" by auto
ultimately have "?dp!1 ∈ dom (finished s)" by simp
}
moreover
from p have P: "path E w p ll" by (simp add: lowlink_path_def)
have "p = (take i p)@?dp" by simp
with P path_conc_conv obtain x where p': "path E x ?dp ll" "path E w (take i p) x" by metis
with ‹?dp ≠ []› path_hd have "hd ?dp = x" by metis
with ‹hd ?dp = u› p' have u_path: "path E u ?dp ll" and path_u: "path E w (take i p) u" by metis+
ultimately have "lowlink_path s u ?dp ll" using p by (simp add: lowlink_path_def)
moreover from u_path path_is_trancl ‹?dp ≠ []› have "(u,ll) ∈ E⇧+" by force
moreover { from ll ‹ll ≠ w› have "(ll,w) ∈ E⇧+" by (auto simp add: lowlink_set_def)
also from path_u path_is_rtrancl have "(w,u) ∈ E⇧*" by metis
finally have "(ll,u)∈E⇧+" .
}
moreover note ll u_disc
ultimately have "ll ∈ lowlink_set s u" unfolding lowlink_set_def by auto
thus ?thesis by auto
qed
qed
qed
hence ll_sub_rev': "?L' ⊆ ?L ∪ ?Lu" by auto
have ref_ne: "stack ?s ≠ [] ⟹
lowlink ?s = (lowlink s)(hd (stack ?s) ↦ min (ζ s (hd (stack ?s))) (ζ s u))"
apply (rule TRANS)
unfolding tarjan_fin_def tj_stack_pop_def
by refine_vcg simp_all
have ref_e: "stack ?s = [] ⟹ lowlink ?s = lowlink s"
apply (rule TRANS)
unfolding tarjan_fin_def tj_stack_pop_def
by refine_vcg simp_all
have ref_tj: "ζ s u ≠ δ s u ⟹ tj_stack ?s = tj_stack s"
apply (rule TRANS)
unfolding tarjan_fin_def tj_stack_pop_def
by refine_vcg simp_all
have "ζ ?s w = LowLink ?s w"
proof (cases "w = hd (stack ?s) ∧ stack ?s ≠ []")
case True note all_True = this
with ref_ne have *: "ζ ?s w = min (ζ s w) (ζ s u)" by simp
show ?thesis
proof (cases "ζ s u < ζ s w")
case False with * finish w_disc have "ζ ?s w = LowLink s w" by simp
also have "LowLink s w = LowLink ?s w"
proof (rule LowLink_eqI[OF inv' _ ll_sub ll_sub_rev])
from w_disc show "w ∈ dom (discovered s)" by simp
fix ll assume "ll ∈ lowlink_set s u"
hence "LowLink s u ≤ δ s ll" by simp
moreover from False finish w_disc u_disc have "LowLink s w ≤ LowLink s u" by simp
ultimately show "LowLink s w ≤ δ ?s ll" by simp
qed simp
finally show ?thesis .
next
case True note ζrel = this
have "LowLink s u ∈ ?L'"
proof -
from all_True finish have w_tl: "w∈set (tl (stack s))" by auto
obtain ll where ll: "ll ∈ lowlink_set s u" "δ s ll = LowLink s u"
using Min_in[of ?Lu] lowlink_set_finite lowlink_set_not_empty u_disc
by fastforce
have "ll ∈ lowlink_set ?s w"
proof (cases "δ s u = ζ s u")
case True
moreover from w_tl finish tl_lt_stack_hd_discover have "δ s w < δ s u" by simp
moreover from w_disc have "LowLink s w ≤ δ s w" by (simp add: LowLink_le_disc)
with w_disc finish have "ζ s w ≤ δ s w" by simp
moreover note ζrel
ultimately have False by force
thus ?thesis ..
next
case False with u_disc finish ll have "u ≠ ll" by auto
with ll have
e: "(ll,u) ∈ E⇧+" "(u,ll) ∈ E⇧+" and
p: "∃p. lowlink_path s u p ll" and
ll_disc: "ll ∈ dom (discovered s)"
by (auto simp: lowlink_set_def)
from p have p': "∃p. lowlink_path ?s u p ll"
unfolding lowlink_path_def
by auto
from w_tl tl_stack_hd_tree_path finish have T: "(w,u) ∈ (tree_edges ?s)⇧+" by simp
with s'.lowlink_path_tree_prepend all_True p' have "∃p. lowlink_path ?s w p ll" by blast
moreover from T trancl_mono_mp[OF s'.tree_edges_ssE] have "(w,u) ∈ E⇧+" by blast
with e have "(w,ll) ∈ E⇧+" by simp
moreover {
note e(1)
also from finish False ref_tj have "tj_stack ?s = tj_stack s" by simp
with hd_in_set finish stack_ss_tj_stack have "u ∈ set (tj_stack ?s)" by auto
with s'.tj_stack_reach_stack obtain x where x: "x ∈ set (stack ?s)" "(u,x) ∈ E⇧*" by blast
note this(2)
also have "(x,w) ∈ E⇧*"
proof (rule rtrancl_eq_or_trancl[THEN iffD2], safe)
assume "x ≠ w" with all_True x have "x ∈ set (tl (stack ?s))" by (cases "stack ?s") auto
with s'.tl_stack_hd_tree_path all_True have "(x,w) ∈ (tree_edges s)⇧+" by auto
with trancl_mono_mp[OF tree_edges_ssE] show "(x,w) ∈ E⇧+" by simp
qed
finally have "(ll,w) ∈ E⇧+" .
}
moreover note ll_disc
ultimately show ?thesis by (simp add: lowlink_set_def)
qed
hence "δ s ll ∈ ?L'" by auto
with ll show ?thesis by simp
qed
hence "LowLink ?s w ≤ LowLink s u"
using Min_le_iff[of ?L'] s'.lowlink_set_not_empty w_disc s'.lowlink_set_finite
by fastforce
also from True u_disc w_disc finish have "LowLink s u < LowLink s w" by simp
hence "Min (?L ∪ ?Lu) = LowLink s u"
using Min_Un[of ?L ?Lu] lowlink_set_finite lowlink_set_not_empty u_disc w_disc
by simp
hence "LowLink s u ≤ LowLink ?s w"
using Min_antimono[OF ll_sub_rev'] lowlink_set_finite s'.lowlink_set_not_empty w_disc
by auto
also from True u_disc finish * have "LowLink s u = ζ ?s w" by simp
finally show ?thesis ..
qed
next
case False note all_False = this
have "ζ ?s w = ζ s w"
proof (cases "stack ?s = []")
case True with ref_e show ?thesis by simp
next
case False with all_False have "w ≠ hd (stack ?s)" by simp
with False ref_ne show ?thesis by simp
qed
also from finish have "ζ s w = LowLink s w" using w_disc by simp
also {
fix v
assume "v ∈ lowlink_set s u"
and *: "v ∉ lowlink_set s w"
hence "v ≠ w" "w≠u" by (auto simp add: lowlink_set_def)
have "v ∉ lowlink_set ?s w"
proof (rule notI)
assume v: "v ∈ lowlink_set ?s w"
hence e: "(v,w) ∈ E⇧*" "(w,v) ∈ E⇧*"
and v_disc: "v ∈ dom (discovered s)" by (auto simp add: lowlink_set_def)
from v ‹v≠w› obtain p where p: "lowlink_path ?s w p v" by (auto simp add: lowlink_set_def)
hence [simp]: "p≠[]" by (simp add: lowlink_path_def)
from p have "hd p = w" by (auto simp add: lowlink_path_def path_hd)
show False
proof (cases "u ∈ set p")
case False hence "lowlink_path s w p v"
using p by (auto simp add: lowlink_path_def)
with e v_disc have "v ∈ lowlink_set s w" by (auto intro: lowlink_setI)
with * show False ..
next
case True
then obtain i where i: "i < length p" "p!i = u"
by (metis in_set_conv_nth)
show "False"
proof (cases i)
case "0" with i have "hd p = u" by (simp add: hd_conv_nth)
with ‹hd p = w› ‹w ≠ u› show False by simp
next
case (Suc n) with i p have *: "(p!n,u) ∈ tree_edges s" "n < length p"
unfolding lowlink_path_def
by auto
with tree_edge_imp_discovered have "p!n ∈ dom (discovered s)" by auto
moreover from finish hd_in_set stack_not_finished have "u ∉ dom (finished s)" by auto
with * have pn_n_fin: "p!n ∉ dom (finished s)" by (metis tree_edge_impl_parenthesis)
moreover from * no_self_loop_in_tree have "p!n ≠ u" by blast
ultimately have "p!n ∈ set (stack ?s)" using stack_set_def finish by (cases "stack s") auto
hence s_ne: "stack ?s ≠ []" by auto
with all_False have "w ≠ hd (stack ?s)" by simp
from stack_is_tree_path finish obtain v0 where
"path (tree_edges s) v0 (rev (stack ?s)) u"
by auto
with s_ne have "(hd (stack ?s), u) ∈ tree_edges s" by (auto simp: neq_Nil_conv path_simps)
with * tree_eq_rule have **: "hd (stack ?s) = p!n" by simp
show ?thesis
proof (cases n)
case "0" with * have "hd p = p!n" by (simp add: hd_conv_nth)
with ‹hd p = w› ** have "w = hd (stack ?s)" by simp
with ‹w≠hd (stack ?s)› show False ..
next
case (Suc m) with * ** s'.lowlink_path_finished[OF p, where j=n] have
"hd (stack ?s) ∈ dom (finished ?s)" by simp
with hd_in_set[OF s_ne] s'.stack_not_finished show ?thesis by blast
qed
qed
qed
qed
} with ll_sub ll_sub_rev have "lowlink_set ?s w = lowlink_set s w" by auto
hence "LowLink s w = LowLink ?s w" by simp
finally show ?thesis .
qed
}
with finish show ?case by (auto simp: pw_leof_iff)
qed simp_all
qed
end end
context Tarjan_invar begin context begin interpretation timing_syntax .
lemmas lowlink_eq_LowLink =
i_lowlink_eq_LowLink[THEN make_invar_thm, rule_format]
lemma lowlink_eq_disc_iff_scc_root:
assumes "v ∈ dom (finished s) ∨ (stack s ≠ [] ∧ v = hd (stack s) ∧ pending s `` {v} = {})"
shows "ζ s v = δ s v ⟷ scc_root s v (scc_of E v)"
proof -
from assms have "v ∈ dom (discovered s)" using finished_discovered hd_in_set stack_discovered by blast
hence "ζ s v = LowLink s v" using lowlink_eq_LowLink by simp
with LowLink_eq_disc_iff_scc_root[OF assms] show ?thesis by simp
qed
lemma nc_sccs_eq_reachable:
assumes NC: "¬ cond s"
shows "reachable = ⋃(sccs s)"
proof
from nc_finished_eq_reachable NC have [simp]: "reachable = dom (finished s)" by simp
with sccs_finished show "⋃(sccs s) ⊆ reachable" by simp
from NC have "stack s = []" by (simp add: cond_alt)
with stacks_eq_iff have "tj_stack s = []" by simp
with finished_ss_sccs_tj_stack show "reachable ⊆ ⋃(sccs s)" by simp
qed
end end
context Tarjan begin
lemma tarjan_fin_nofail:
assumes "pre_on_finish u s'"
shows "nofail (tarjan_fin u s')"
proof -
from assms obtain s where s: "DFS_invar G tarjan_params s" "stack s ≠ []" "u = hd (stack s)" "s' = finish u s" "cond s" "pending s `` {u} = {}"
by (auto simp: pre_on_finish_def)
then interpret Tarjan_invar where s=s by simp
from s hd_stack_in_tj_stack have "u ∈ set (tj_stack s')" by simp
moreover from s tj_stack_distinct have "distinct (tj_stack s')" by simp
moreover have "the (lowlink s' u) = the (discovered s' u) ⟷ scc_root s' u (scc_of E u)"
proof -
from s have "the (lowlink s' u) = the (discovered s' u) ⟷ the (lowlink s u) = the (discovered s u)" by simp
also from s lowlink_eq_disc_iff_scc_root have "... ⟷ scc_root s u (scc_of E u)" by blast
also from s scc_root_transfer'[where s'=s'] have "... ⟷ scc_root s' u (scc_of E u)" by simp
finally show ?thesis .
qed
ultimately show ?thesis
unfolding tarjan_fin_def tj_stack_pop_def
by simp
qed
sublocale DFS G tarjan_params
by unfold_locales (simp_all add: tarjan_disc_def tarjan_back_def tarjan_fin_nofail)
end