# Theory Tarjan

```section ‹Tarjan's Algorithm›
theory Tarjan
imports
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›
(* Though this is a general lemma about dropWhile/takeWhile, it is probably only of use for this algorithm. *)
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
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 (* end timing syntax *)

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 .

"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"
"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"
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}"
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"
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"
by (auto simp: cross_back_edge)

have ll_sub_rev: "lowlink_set ?s w ⊆ lowlink_set s w ∪ {v}"
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 ― ‹‹w ≠ u››
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≠[]"
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"
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"
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"
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"
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"
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"
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 .

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

interpretation tarjan: Tarjan_def for G .

subsection ‹Interface›
definition "tarjan G ≡ do {
ASSERT (fb_graph G);
s ← tarjan.it_dfs TYPE('a) G;
RETURN (sccs s) }"

definition "tarjan_spec G ≡ do {
ASSERT (fb_graph G);
SPEC (λsccs.  (∀scc ∈ sccs. is_scc (g_E G) scc)
∧ ⋃sccs = tarjan.reachable TYPE('a) G)}"

lemma tarjan_correct:
"tarjan G ≤ tarjan_spec G"
unfolding tarjan_def tarjan_spec_def
proof (refine_vcg le_ASSERTI order_trans[OF DFS.it_dfs_correct])
assume "fb_graph G"
then interpret fb_graph G .
interpret Tarjan ..
show "DFS G (tarjan.tarjan_params TYPE('b) G)" ..
next
fix s
assume C: "DFS_invar G (tarjan.tarjan_params TYPE('b) G) s ∧ ¬ tarjan.cond TYPE('b) G s"
then interpret Tarjan_invar G s by simp

from sccs_are_sccs show "∀scc∈sccs s. is_scc (g_E G) scc" .

from nc_sccs_eq_reachable C show "⋃(sccs s) = tarjan.reachable TYPE('b) G" by simp
qed

end
```