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›
(* 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

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