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› (* 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 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 (* 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 . 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 ― ‹‹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≠[]" 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