Theory DFS_Invars_Basic

section ‹Basic Invariant Library›
theory DFS_Invars_Basic
imports "../Param_DFS"
begin

text ‹We provide more basic invariants of the DFS algorithm›



subsection ‹Basic Timing Invariants›

(* Timing *)
abbreviation "the_discovered s v  the (discovered s v)"
abbreviation "the_finished s v  the (finished s v)"

locale timing_syntax
begin
  (* Timing related syntax shortcuts *) 
  notation the_discovered ("δ")
  notation the_finished ("φ")
end

context param_DFS begin context begin interpretation timing_syntax .

  definition "timing_common_inv s  
  ― ‹δ s v < φ s v›
   (v  dom (finished s). δ s v < φ s v)

  ― ‹v ≠ w ⟶ δ s v ≠ δ s w ∧ φ s v ≠ φ s w›
  ― ‹Can't use card dom = card ran› as the maps may be infinite ...›
   (v  dom (discovered s). w  dom (discovered s). v  w  δ s v  δ s w)
   (v  dom (finished s). w  dom (finished s). v  w  φ s v  φ s w)

  ― ‹δ s v < counter ∧ φ s v < counter›
   (v  dom (discovered s). δ s v < counter s)
   (v  dom (finished s). φ s v < counter s)

   (v  dom (finished s). w  succ v. δ s w < φ s v)"

  lemma timing_common_inv: 
    "is_invar timing_common_inv"
  proof (induction rule: is_invarI)
    case (finish s s') then interpret DFS_invar where s=s by simp

    from finish have NE: "stack s  []" by (simp add: cond_alt)
    
    have *: "hd (stack s)  dom (finished s)" "hd (stack s)  dom (discovered s)"
      using stack_not_finished stack_discovered hd_in_set[OF NE]
      by blast+

    from discovered_closed have 
      "(E - pending s) `` {hd (stack s)}  dom (discovered s)"
      using hd_in_set[OF NE]
      by (auto simp add: discovered_closed_def)
    hence succ_hd: "pending s `` {hd (stack s)} = {} 
       succ (hd (stack s))  dom (discovered s)"
      by blast
    
    from finish show ?case 
        apply (simp add: timing_common_inv_def)
        apply (intro conjI)
        using * apply simp
        using * apply simp
        apply (metis less_irrefl)
        apply (metis less_irrefl)
        apply (metis less_SucI)
        apply (metis less_SucI)
        apply (blast dest!: succ_hd)
        using * apply simp
        done
  next
    case (discover s) then interpret DFS_invar where s=s by simp
    from discover show ?case
      apply (simp add: timing_common_inv_def)
      apply (intro conjI)
      using finished_discovered apply fastforce
      apply (metis less_irrefl)
      apply (metis less_irrefl)
      apply (metis less_SucI)
      apply (metis less_SucI)
      using finished_imp_succ_discovered apply fastforce
      done
  next
    case (new_root s s' v0) then interpret DFS_invar where s=s by simp
    from new_root show ?case
      apply (simp add: timing_common_inv_def)
      apply (intro conjI)
      using finished_discovered apply fastforce
      apply (metis less_irrefl)
      apply (metis less_irrefl)
      apply (metis less_SucI)
      apply (metis less_SucI)
      using finished_imp_succ_discovered apply fastforce
      done
  qed (simp_all add: timing_common_inv_def)
end end

context DFS_invar begin context begin interpretation timing_syntax .

  lemmas s_timing_common_inv = 
    timing_common_inv[THEN make_invar_thm]

  lemma timing_less_counter:
    "v  dom (discovered s)  δ s v < counter s"
    "v  dom (finished s)  φ s v < counter s"
    using s_timing_common_inv
    by (auto simp add: timing_common_inv_def)

  lemma disc_lt_fin:
    "v  dom (finished s)  δ s v < φ s v"
    using s_timing_common_inv
    by (auto simp add: timing_common_inv_def)

  lemma disc_unequal:
    assumes "v  dom (discovered s)" "w  dom (discovered s)"
    and "v  w"
    shows "δ s v  δ s w"
    using s_timing_common_inv assms
    by (auto simp add: timing_common_inv_def)

  lemma fin_unequal:
    assumes "v  dom (finished s)" "w  dom (finished s)"
    and "v  w"
    shows "φ s v  φ s w"
    using s_timing_common_inv assms
    by (auto simp add: timing_common_inv_def)

  lemma finished_succ_fin:
    assumes "v  dom (finished s)"
    and "w  succ v"
    shows "δ s w < φ s v"
    using assms s_timing_common_inv
    by (simp add: timing_common_inv_def)
end end

context param_DFS begin context begin interpretation timing_syntax .

  lemma i_prev_stack_discover_all:
    "is_invar (λs.  n < length (stack s).  v  set (drop (Suc n) (stack s)). 
                   δ s (stack s ! n) > δ s v)"
  proof (induct rule: is_invarI)
    case (finish s) thus ?case 
      by (cases "stack s") auto
  next
    case (discover s s' u v) 
    hence EQ[simp]: "discovered s' = (discovered s)(v  counter s)"
                    "stack s' = v#stack s"
      by simp_all
    
    from discover interpret DFS_invar where s=s by simp
    from discover stack_discovered have v_ni: "v  set (stack s)" by auto

    from stack_discovered timing_less_counter have 
      "w. w  set (stack s)  δ s w < counter s" 
      by blast
    with v_ni have "w. w  set (stack s)  δ s' w < δ s' v" by auto
    hence "w. w  set (drop (Suc 0) (stack s'))  δ s' w < δ s' (stack s' ! 0)" 
      by auto
      
    moreover
    from v_ni have 
      "n. n < (length (stack s')); n > 0
       δ s' (stack s' ! n) = δ s (stack s' ! n)" 
      by auto
    with discover(1) v_ni 
    have  "n. n < (length (stack s')) - 1; n > 0 
        w  set (drop (Suc n) (stack s')). δ s' (stack s' ! n) > δ s' w"
      by (auto dest: in_set_dropD)
    ultimately show ?case 
      by (metis drop_Suc_Cons length_drop length_pos_if_in_set length_tl 
        list.sel(3) neq0_conv nth_Cons_0 EQ(2) zero_less_diff)
  qed simp_all
end end

context DFS_invar begin context begin interpretation timing_syntax .

  lemmas prev_stack_discover_all 
    = i_prev_stack_discover_all[THEN make_invar_thm]

  lemma prev_stack_discover:
    "n < length (stack s); v  set (drop (Suc n) (stack s)) 
      δ s (stack s ! n) > δ s v"
    by (metis prev_stack_discover_all)

  lemma Suc_stack_discover:
    assumes n: "n < (length (stack s)) - 1"
    shows "δ s (stack s ! n) > δ s (stack s ! Suc n)"
  proof -
    from prev_stack_discover assms have 
      " v. v  set (drop (Suc n) (stack s))  δ s (stack s ! n) > δ s v" 
      by fastforce
    moreover from n have "stack s ! Suc n  set (drop (Suc n) (stack s))" 
      using in_set_conv_nth by fastforce
    ultimately show ?thesis .
  qed

  lemma tl_lt_stack_hd_discover:
    assumes notempty: "stack s  []"
    and "x  set (tl (stack s))"
    shows "δ s x < δ s (hd (stack s))"
  proof -
    from notempty obtain y ys where "stack s = y#ys" by (metis list.exhaust)
    with assms show ?thesis
      using prev_stack_discover
      by (cases ys) force+
  qed

  lemma stack_nth_order:
    assumes l: "i < length (stack s)" "j < length (stack s)"
    shows "δ s (stack s ! i) < δ s (stack s ! j)  i > j" (is "δ s ?i < δ s ?j  _")
  proof
    assume δ: "δ s ?i < δ s ?j"
    
    from l stack_set_def have 
      disc: "?i  dom (discovered s)" "?j  dom (discovered s)"
      by auto
    with disc_unequal[OF disc] δ have "i  j" by auto

    moreover
    {
      assume "i < j"

      with l have "stack s ! j  set (drop (Suc i) (stack s))" 
        using in_set_drop_conv_nth[of "stack s ! j" "Suc i" "stack s"]
        by fastforce
      with prev_stack_discover l have "δ s (stack s ! j) < δ s (stack s ! i)" 
        by simp
      with δ have "False" by simp
    }
    ultimately show "i > j" by force
  next
    assume "i > j"
    with l have "stack s ! i  set (drop (Suc j) (stack s))" 
      using in_set_drop_conv_nth[of "stack s ! i" "Suc j" "stack s"]
      by fastforce
    with prev_stack_discover l show "δ s ?i < δ s ?j" by simp
  qed
end end

subsection ‹Paranthesis Theorem›
(* Parenthesis Thm *)
context param_DFS begin context begin interpretation timing_syntax .

  definition "parenthesis s 
    v  dom (discovered s). w  dom (discovered s).
     δ s v < δ s w  v  dom (finished s)  (
             φ s v < δ s w ― ‹disjoint›
            (φ s v > δ s w  w  dom (finished s)  φ s w < φ s v))"

  lemma i_parenthesis: "is_invar parenthesis"
  proof (induct rule: is_invarI)
    case (finish s s')
    hence EQ[simp]: "discovered s' = discovered s" 
                    "counter s' = Suc (counter s)"
                    "finished s' = (finished s)(hd (stack s)  counter s)"
      by simp_all

    from finish interpret DFS_invar where s=s by simp
    from finish have NE[simp]: "stack s  []" by (simp add: cond_alt)

    {
      fix x y
      assume  dom: "x  dom (discovered s')" "y  dom (discovered s')"
        and δ: "δ s' x < δ s' y"
        and f: "x  dom (finished s')"
      hence neq: "x  y" by force

      note assms = dom δ f EQ

      let ?DISJ = "φ s' x < δ s' y"
      let ?IN = "δ s' y < φ s' x  y  dom (finished s')  φ s' y < φ s' x"

      have "?DISJ  ?IN"
      proof (cases "x = hd (stack s)")
        case True note x_is_hd = this
        hence φx: "φ s' x = counter s" by simp
        from x_is_hd neq have y_not_hd: "y  hd (stack s)" by simp
        
        have "δ s y < φ s' x  y  dom (finished s)  φ s y < φ s' x"
        proof (cases "y  set (stack s)")
          ― ‹y on stack is not possible: According to @{thm [display] δ} it is discovered after @{text "x (= hd (stack s))"}
          case True with y_not_hd have "y  set (tl (stack s))" 
            by (cases "stack s") simp_all
          with tl_lt_stack_hd_discover[OF NE] δ x_is_hd have "δ s y < δ s x" 
            by simp
          with δ have False by simp
          thus ?thesis ..
        next
          case False ― ‹y must be a successor of @{text "x (= (hd (stack s)))"}
          from dom have "y  dom (discovered s)" by simp
          with False discovered_not_stack_imp_finished  have *: 
            "y  dom (finished s)" 
            by simp
          moreover with timing_less_counter φx have "φ s y < φ s' x" by simp
          moreover with * disc_lt_fin φx have "δ s y < φ s' x" 
            by (metis less_trans)
          ultimately show ?thesis by simp
        qed
        with y_not_hd show ?thesis by simp
      next
        case False note [simp] = this
        show ?thesis
        proof (cases "y = hd (stack s)")
          case False with finish assms show ?thesis 
            by (simp add: parenthesis_def)
        next
          case True with stack_not_finished have "y  dom (finished s)" 
            using hd_in_set[OF NE] 
            by auto
          with finish assms have "φ s x < δ s y" 
            unfolding parenthesis_def
            by auto
          hence ?DISJ by simp
          thus ?thesis ..
        qed
      qed
    }
    thus ?case by (simp add: parenthesis_def)
  next
    case (discover s s' u v)
    hence EQ[simp]: "discovered s' = (discovered s)(v  counter s)" 
                    "finished s' = finished s"
                    "counter s' = Suc (counter s)"
      by simp_all
    
    from discover interpret DFS_invar where s=s by simp
    from discover finished_discovered have 
      V': "v  dom (discovered s)" "v  dom (finished s)" 
      by auto

    {
      fix x y
      assume  dom: "x  dom (discovered s')" "y  dom (discovered s')"
        and δ: "δ s' x < δ s' y"
        and f: "x  dom (finished s')"

      let ?DISJ = "φ s' x < δ s' y"
      let ?IN = "δ s' y < φ s' x  y  dom (finished s')  φ s' y < φ s' x"
      
      from dom V' f have x: "x  dom (discovered s)""x  v" by auto
      
      have "?DISJ  ?IN"
      proof (cases "y = v")
        case True hence "δ s' y = counter s" by simp
        moreover from timing_less_counter x f have "φ s' x < counter s" by auto
        ultimately have "?DISJ" by simp
        thus ?thesis ..
      next
        case False with dom have "y  dom (discovered s)" by simp
        with discover False δ f x show ?thesis by (simp add: parenthesis_def)
      qed
    }
    thus ?case by (simp add: parenthesis_def)
  next
    case (new_root s s' v0) 
    then interpret DFS_invar where s=s by simp
    
    from finished_discovered new_root have "v0  dom (finished s')" by auto
    with new_root timing_less_counter show ?case by (simp add: parenthesis_def)
  qed (simp_all add: parenthesis_def)
end end

context DFS_invar begin context begin interpretation timing_syntax .

  lemma parenthesis:
    assumes "v  dom (finished s)" "w  dom (discovered s)"
    and "δ s v < δ s w"
    shows "φ s v < δ s w ― ‹disjoint›
            (φ s v > δ s w  w  dom (finished s)  φ s w < φ s v)"
    using assms
    using i_parenthesis[THEN make_invar_thm]
    using finished_discovered
    unfolding parenthesis_def
    by blast

  lemma parenthesis_contained:
    assumes "v  dom (finished s)" "w  dom (discovered s)"
    and "δ s v < δ s w" "φ s v > δ s w"
    shows "w  dom (finished s)  φ s w < φ s v"
    using parenthesis assms
    by force
  
  lemma parenthesis_disjoint:
    assumes "v  dom (finished s)" "w  dom (discovered s)"
    and "δ s v < δ s w" "φ s w > φ s v"
    shows "φ s v < δ s w"
    using parenthesis assms
    by force

  lemma finished_succ_contained:
    assumes "v  dom (finished s)"
    and "w  succ v"
    and "δ s v < δ s w"
    shows "w  dom (finished s)  φ s w < φ s v"
    using finished_succ_fin finished_imp_succ_discovered parenthesis_contained
    using assms
    by metis

end end


subsection ‹Edge Types›
context param_DFS 
begin
  abbreviation "edges s  tree_edges s  cross_edges s  back_edges s"

  (* Demo for simple invariant proof *)
  lemma "is_invar (λs. finite (edges s))"
    by (induction rule: establish_invarI) auto

  text ‹Sometimes it's useful to just chose between tree-edges and non-tree.›
  lemma edgesE_CB:
    assumes "x  edges s"
    and "x  tree_edges s  P"
    and "x  cross_edges s  back_edges s  P"
    shows "P"
    using assms by auto

  definition "edges_basic s  
     Field (back_edges s)  dom (discovered s)  back_edges s  E - pending s
    Field (cross_edges s)  dom (discovered s)  cross_edges s  E - pending s
    Field (tree_edges s)  dom (discovered s)  tree_edges s  E - pending s
    back_edges s  cross_edges s = {}
    back_edges s  tree_edges s = {}
    cross_edges s  tree_edges s = {}
   "

  lemma i_edges_basic:
    "is_invar edges_basic"
    unfolding edges_basic_def[abs_def]
  proof (induct rule: is_invarI_full)
    case (back_edge s)
    then interpret DFS_invar where s=s by simp
    from back_edge show ?case by (auto dest: pendingD)
  next
    case (cross_edge s)
    then interpret DFS_invar where s=s by simp
    from cross_edge show ?case by (auto dest: pendingD)
  next
    case (discover s)
    then interpret DFS_invar where s=s by simp
    from discover show ?case 
      (* Speed optimized proof, using only auto takes too long *)
      apply (simp add: Field_def Range_def Domain_def)
      apply (drule pendingD) apply simp
      by (blast)
  next
    case (new_root s) 
    thus ?case by (simp add: Field_def) blast
  qed auto

  lemmas (in DFS_invar) edges_basic = i_edges_basic[THEN make_invar_thm]
    
  lemma i_edges_covered: 
    "is_invar (λs. (E  dom (discovered s) × UNIV) - pending s = edges s)"
  proof (induction rule: is_invarI_full)
    case (new_root s s' v0) 
    interpret DFS_invar G param s by fact  

    from new_root empty_stack_imp_empty_pending 
    have [simp]: "pending s = {}" by simp

    from v0  dom (discovered s) 
    have [simp]: "E  insert v0 (dom (discovered s)) × UNIV - {v0} × succ v0 
      = E  dom (discovered s) × UNIV" by auto

    from new_root show ?case by simp
  next
    case (cross_edge s s' u v) 
    interpret DFS_invar G param s by fact  

    from cross_edge stack_discovered have "u  dom (discovered s)" 
      by (cases "stack s") auto

    with cross_edge(2-) pending_ssE have 
      "E  dom (discovered s) × UNIV - (pending s - {(hd (stack s), v)})
      = insert (hd (stack s), v) (E  dom (discovered s) × UNIV - pending s)"
      by auto

    thus ?case using cross_edge by simp
  next
    case (back_edge s s' u v)
    interpret DFS_invar G param s by fact  

    from back_edge stack_discovered have "u  dom (discovered s)" 
      by (cases "stack s") auto

    with back_edge(2-) pending_ssE have 
      "E  dom (discovered s) × UNIV - (pending s - {(hd (stack s), v)})
      = insert (hd (stack s), v) (E  dom (discovered s) × UNIV - pending s)"
      by auto

    thus ?case using back_edge by simp
  next
    case (discover s s' u v)
    interpret DFS_invar G param s by fact  

    from discover stack_discovered have "u  dom (discovered s)" 
      by (cases "stack s") auto

    with discover(2-) pending_ssE have 
      "E  insert v (dom (discovered s)) × UNIV 
        - (pending s - {(hd (stack s), v)}  {v} × succ v)
      = insert (hd (stack s), v) (E  dom (discovered s) × UNIV - pending s)"
      by auto

    thus ?case using discover by simp
  qed simp_all
end

context DFS_invar begin

  lemmas edges_covered = 
    i_edges_covered[THEN make_invar_thm]

  lemma edges_ss_reachable_edges:
    "edges s  E  reachable × UNIV"
    using edges_covered discovered_reachable
    by (fast intro: rtrancl_image_advance_rtrancl)

  lemma nc_edges_covered:
    assumes "¬cond s" "¬is_break param s"
    shows "E  reachable × UNIV = edges s"
  proof -
    from assms have [simp]: "stack s = []" 
      unfolding cond_def by (auto simp: pred_defs)
    hence [simp]: "pending s = {}" by (rule empty_stack_imp_empty_pending)
    
    
    from edges_covered nc_discovered_eq_reachable[OF assms] 
    show ?thesis by simp
  qed

  lemma 
    tree_edges_ssE: "tree_edges s  E" and
    tree_edges_not_pending: "tree_edges s  - pending s" and
    tree_edge_is_succ: "(v,w)  tree_edges s  w  succ v" and
    tree_edges_discovered: "Field (tree_edges s)  dom (discovered s)" and

    cross_edges_ssE: "cross_edges s  E" and
    cross_edges_not_pending: "cross_edges s  - pending s" and
    cross_edge_is_succ: "(v,w)  cross_edges s  w  succ v" and
    cross_edges_discovered: "Field (cross_edges s)  dom (discovered s)" and

    back_edges_ssE: "back_edges s  E" and
    back_edges_not_pending: "back_edges s  - pending s" and
    back_edge_is_succ: "(v,w)  back_edges s  w  succ v" and
    back_edges_discovered: "Field (back_edges s)  dom (discovered s)"
    using edges_basic
    unfolding edges_basic_def 
    by auto

  lemma edges_disjoint: 
   "back_edges s  cross_edges s = {}"
   "back_edges s  tree_edges s = {}"
   "cross_edges s  tree_edges s = {}"
    using edges_basic
    unfolding edges_basic_def 
    by auto

  lemma tree_edge_imp_discovered:
    "(v,w)  tree_edges s  v  dom (discovered s)"
    "(v,w)  tree_edges s  w  dom (discovered s)"
    using tree_edges_discovered
    by (auto simp add: Field_def)

  lemma back_edge_imp_discovered:
    "(v,w)  back_edges s  v  dom (discovered s)"
    "(v,w)  back_edges s  w  dom (discovered s)"
    using back_edges_discovered
    by (auto simp add: Field_def)

  lemma cross_edge_imp_discovered:
    "(v,w)  cross_edges s  v  dom (discovered s)"
    "(v,w)  cross_edges s  w  dom (discovered s)"
    using cross_edges_discovered
    by (auto simp add: Field_def)

  lemma edge_imp_discovered:
    "(v,w)  edges s  v  dom (discovered s)"
    "(v,w)  edges s  w  dom (discovered s)"
    using tree_edge_imp_discovered cross_edge_imp_discovered back_edge_imp_discovered
    by blast+

  lemma tree_edges_finite[simp, intro!]: "finite (tree_edges s)"
    using finite_subset[OF tree_edges_discovered discovered_finite] by simp

  lemma cross_edges_finite[simp, intro!]: "finite (cross_edges s)"
    using finite_subset[OF cross_edges_discovered discovered_finite] by simp

  lemma back_edges_finite[simp, intro!]: "finite (back_edges s)"
    using finite_subset[OF back_edges_discovered discovered_finite] by simp

  lemma edges_finite: "finite (edges s)"
    by auto

  
end

subsubsection ‹Properties of the DFS Tree›
(* Tree *)

context DFS_invar begin context begin interpretation timing_syntax .
  lemma tree_edge_disc_lt_fin:
    "(v,w)  tree_edges s  v  dom (finished s)  δ s w < φ s v"
    by (metis finished_succ_fin tree_edge_is_succ)

  lemma back_edge_disc_lt_fin:
    "(v,w)  back_edges s  v  dom (finished s)  δ s w < φ s v"
    by (metis finished_succ_fin back_edge_is_succ)

  lemma cross_edge_disc_lt_fin:
    "(v,w)  cross_edges s  v  dom (finished s)  δ s w < φ s v"
    by (metis finished_succ_fin cross_edge_is_succ)
end end

(* Stack & Tree *)
context param_DFS begin

  lemma i_stack_is_tree_path:
    "is_invar (λs. stack s  []  (v0  V0. 
        path (tree_edges s) v0 (rev (tl (stack s))) (hd (stack s))))"
  proof (induct rule: is_invarI)
    case (discover s s' u v)
    hence EQ[simp]: "stack s' = v # stack s"
                    "tree_edges s' = insert (hd (stack s), v) (tree_edges s)"
      by simp_all
    from discover have NE[simp]: "stack s  []" by simp

    from discover obtain v0 where 
      "v0  V0"
      "path (tree_edges s) v0 (rev (tl (stack s))) (hd (stack s))"
      by blast
    with path_mono[OF _ this(2)] EQ have 
      "path (tree_edges s') v0 (rev (tl (stack s))) (hd (stack s))" 
      by blast
    with v0  V0 show ?case
      by (cases "stack s") (auto simp: path_simps)

  next
    case (finish s s')
    hence EQ[simp]: "stack s' = tl (stack s)"
                    "tree_edges s' = tree_edges s"
      by simp_all

    from finish obtain v0 where
      "v0  V0"
      "path (tree_edges s) v0 (rev (tl (stack s))) (hd (stack s))"
      by blast
    hence P: "path (tree_edges s') v0 (rev (stack s')) (hd (stack s))" by simp
      
    show ?case
    proof
      assume A: "stack s'  []"
      with P have "(hd (stack s'), hd (stack s))  tree_edges s'"
        by (auto simp: neq_Nil_conv path_simps)
      moreover from P A have 
        "path (tree_edges s') v0 (rev (tl (stack s')) @ [hd (stack s')]) (hd (stack s))"
        by (simp)
      moreover note v0  V0
      ultimately show "v0V0. path (tree_edges s') v0 (rev (tl (stack s'))) (hd (stack s'))"
        by (auto simp add: path_append_conv)
    qed
  qed simp_all
end

context DFS_invar begin

  lemmas stack_is_tree_path = 
    i_stack_is_tree_path[THEN make_invar_thm, rule_format]

  lemma stack_is_path:
    "stack s  []  v0V0. path E v0 (rev (tl (stack s))) (hd (stack s))"
    using stack_is_tree_path path_mono[OF tree_edges_ssE]
    by blast

  lemma hd_succ_stack_is_path:
    assumes ne: "stack s  []"
    and succ: "v  succ (hd (stack s))"
    shows "v0V0. path E v0 (rev (stack s)) v"
  proof -
    from stack_is_path[OF ne] succ obtain v0 where
      "v0  V0"
      "path E v0 (rev (tl (stack s)) @ [hd (stack s)]) v"
      by (auto simp add: path_append_conv)
    thus ?thesis using ne
      by (cases "stack s") auto
  qed

  lemma tl_stack_hd_tree_path:
    assumes "stack s  []"
    and "v  set (tl (stack s))"
    shows "(v, hd (stack s))  (tree_edges s)+"
  proof -
    from stack_is_tree_path assms obtain v0 where 
      "path (tree_edges s) v0 (rev (tl (stack s))) (hd (stack s))" 
      by auto
    from assms path_member_reach_end[OF this] show ?thesis by simp
  qed
end

context param_DFS begin
  definition "tree_discovered_inv s 
                       (tree_edges s = {}  dom (discovered s)  V0  (stack s = []  (v0V0. stack s = [v0])))
                      (tree_edges s  {}  (tree_edges s)+ `` V0  V0 = dom (discovered s)  V0)"


  lemma i_tree_discovered_inv: 
    "is_invar tree_discovered_inv"
  proof (induct rule: is_invarI)
    case (discover s s' u v) 
    hence EQ[simp]: "stack s' = v # stack s"
                    "tree_edges s' = insert (hd (stack s), v) (tree_edges s)"
                    "discovered s' = (discovered s)(v  counter s)"
      by simp_all
    
    from discover interpret DFS_invar where s=s by simp

    from discover have NE[simp]: "stack s  []" by simp
    note TDI = tree_discovered_inv s[unfolded tree_discovered_inv_def]

    have "tree_edges s' = {}  dom (discovered s')  V0  (stack s' = []  (v0V0. stack s' = [v0]))"
      by simp ― ‹@{text "tree_edges s' ≠ {}"}

    moreover {
      fix x
      assume A: "x  (tree_edges s')+ `` V0  V0" "x  V0"
      then obtain y where y: "(y,x)  (tree_edges s')+" "y  V0" by auto
     

      have "x  dom (discovered s')  V0"
      proof (cases "tree_edges s = {}")
        case True with discover A have "(tree_edges s')+ = {(hd (stack s), v)}"
          by (simp add: trancl_single)
        with A show ?thesis by auto
      next
        case False note t_ne = this

        show ?thesis
        proof (cases "x = v")
          case True thus ?thesis by simp
        next
          case False with y have "(y,x)  (tree_edges s)+"
          proof (induct rule: trancl_induct)
            case (step a b) hence "(a,b)  tree_edges s" by simp
            with tree_edge_imp_discovered have "a  dom (discovered s)" by simp
            with discover have "a  v" by blast
            with step show ?case by auto
          qed simp
          with y  V0 have "x  (tree_edges s)+ `` V0" by auto
          with t_ne TDI show ?thesis by auto
        qed
      qed
    } note t_d = this

    {
      fix x
      assume "x  dom (discovered s')  V0" "x  V0"
      hence A: "x  dom (discovered s')" by simp

      have "x  (tree_edges s')+ `` V0  V0"
      proof (cases "tree_edges s = {}")
        case True with trancl_single have "(tree_edges s')+ = {(hd (stack s), v)}" by simp
        moreover from True TDI have "hd (stack s)  V0" "dom (discovered s)  V0" by auto
        ultimately show ?thesis using A xV0 by auto
      next
        case False note t_ne = this

        show ?thesis
        proof (cases "x=v")
          case False with A have "x  dom (discovered s)" by simp
          with TDI t_ne x  V0 have "x  (tree_edges s)+ `` V0" by auto
          with trancl_sub_insert_trancl show ?thesis by simp blast
        next
          case True
          from t_ne TDI have "dom (discovered s)  V0 = (tree_edges s)+ `` V0  V0"
            by simp

          moreover from stack_is_tree_path[OF NE] obtain v0 where "v0  V0" and 
            "(v0, hd (stack s))  (tree_edges s)*"
            by (blast intro!: path_is_rtrancl)
          with EQ have "(v0, hd (stack s))  (tree_edges s')*" by (auto intro: rtrancl_mono_mp)
          ultimately show ?thesis using v0  V0 True by (auto elim: rtrancl_into_trancl1)
        qed
      qed
    } with t_d have "(tree_edges s')+ `` V0  V0 = dom (discovered s')  V0" by blast

    ultimately show ?case by (simp add: tree_discovered_inv_def)
  qed (auto simp add: tree_discovered_inv_def)
      
  lemmas (in DFS_invar) tree_discovered_inv = 
    i_tree_discovered_inv[THEN make_invar_thm]

  lemma (in DFS_invar) discovered_iff_tree_path:
    "v  V0  v  dom (discovered s)  (v0V0. (v0,v)  (tree_edges s)+)"
    using tree_discovered_inv
    by (auto simp add: tree_discovered_inv_def)

  lemma i_tree_one_predecessor:
    "is_invar (λs. (v,v')  tree_edges s. y. y  v  (y,v')  tree_edges s)"
  proof (induct rule: is_invarI)
    case (discover s s' u v) 
    hence EQ[simp]: "tree_edges s' = insert (hd (stack s),v) (tree_edges s)" by simp

    from discover interpret DFS_invar where s=s by simp
    from discover have NE[simp]: "stack s  []" by (simp add: cond_alt)

    {
      fix w w' y
      assume *: "(w,w')  tree_edges s'"
        and  "y  w"

      from discover stack_discovered have v_hd: "hd (stack s)  v" 
        using hd_in_set[OF NE] by blast
      from discover tree_edges_discovered have 
        v_notin_tree: "(x,x')  tree_edges s. x  v  x'  v" 
        by (blast intro!: Field_not_elem)

      have "(y,w')  tree_edges s'"
      proof (cases "w = hd (stack s)")
        case True
        have "(y,v)  tree_edges s'"
        proof (rule notI)
          assume "(y,v)  tree_edges s'" 
          with True yw have "(y,v)  tree_edges s" by simp
          with v_notin_tree show False by auto
        qed
        with True * yw v_hd show ?thesis 
          apply (cases "w = v")
          apply simp 
          using discover apply simp apply blast
          done
      next
        case False with v_notin_tree * yw v_hd 
        show ?thesis
          apply (cases "w' = v")
          apply simp apply blast
          using discover apply simp apply blast
          done
      qed
    }
    thus ?case by blast
  qed simp_all
 
  lemma (in DFS_invar) tree_one_predecessor:
    assumes "(v,w)  tree_edges s"
    and "a  v"
    shows "(a,w)  tree_edges s"
    using assms make_invar_thm[OF i_tree_one_predecessor]
    by blast

  lemma (in DFS_invar) tree_eq_rule:
    "(v,w)  tree_edges s; (u,w)  tree_edges s  v=u"
    using tree_one_predecessor
    by blast

context begin interpretation timing_syntax .

  lemma i_tree_edge_disc:
    "is_invar (λs. (v,v')  tree_edges s. δ s v < δ s v')"
  proof (induct rule: is_invarI)
    case (discover s s' u v) 
    hence EQ[simp]: "tree_edges s' = insert (hd (stack s), v) (tree_edges s)"
                    "discovered s' = (discovered s)(v  counter s)"
      by simp_all

    from discover interpret DFS_invar where s=s by simp
    from discover have NE[simp]: "stack s  []" by (simp add: cond_alt)
    
    from discover tree_edges_discovered have 
      v_notin_tree: "(x,x')  tree_edges s. x  v  x'  v" 
      by (blast intro!: Field_not_elem)
    from discover stack_discovered have 
      v_hd: "hd (stack s)  v" 
      using hd_in_set[OF NE] 
      by blast
    
    {
      fix a b
      assume T: "(a,b)  tree_edges s'"
      have "δ s' a < δ s' b"
      proof (cases "b = v")
        case True with T v_notin_tree have [simp]: "a = hd (stack s)" by auto
        with stack_discovered have "a  dom (discovered s)" 
          by (metis hd_in_set NE subsetD)
        with v_hd True timing_less_counter show ?thesis by simp
      next
        case False with v_notin_tree T have "(a,b)  tree_edges s" "a  v" by auto
        with discover have "δ s a < δ s b" by auto
        with False av show ?thesis by simp
      qed
    } thus ?case by blast
  next
    case (new_root s s' v0) then interpret DFS_invar where s=s by simp
    from new_root have "tree_edges s' = tree_edges s" by simp
    moreover from tree_edge_imp_discovered new_root have "(v,v')  tree_edges s. v  v0  v'  v0" by blast
    ultimately show ?case using new_root by auto
  qed simp_all
end end

context DFS_invar begin context begin interpretation timing_syntax .

  lemma tree_edge_disc:
    "(v,w)  tree_edges s  δ s v < δ s w"
    using i_tree_edge_disc[THEN make_invar_thm]
    by blast
  
  lemma tree_path_disc:
    "(v,w)  (tree_edges s)+  δ s v < δ s w"
    by (auto elim!: trancl_induct dest: tree_edge_disc)

  lemma no_loop_in_tree:
    "(v,v)  (tree_edges s)+"
    using tree_path_disc by auto

  lemma tree_acyclic:
    "acyclic (tree_edges s)"
    by (metis acyclicI no_loop_in_tree)

  lemma no_self_loop_in_tree:
    "(v,v)  tree_edges s"
    using tree_edge_disc by auto

  lemma tree_edge_unequal:
    "(v,w)  tree_edges s  v  w"
    by (metis no_self_loop_in_tree)

  lemma tree_path_unequal:
    "(v,w)  (tree_edges s)+  v  w"
    by (metis no_loop_in_tree)

  lemma tree_subpath':
    assumes x: "(x,v)  (tree_edges s)+"
    and y: "(y,v)  (tree_edges s)+"
    and "x  y"
    shows "(x,y)  (tree_edges s)+  (y,x)  (tree_edges s)+"
  proof -
    from x obtain px where px: "path (tree_edges s) x px v" and "px  []"
      using trancl_is_path by metis
    from y obtain py where py: "path (tree_edges s) y py v" and "py  []"
      using trancl_is_path by metis

    from px  [] py  [] px py
    show ?thesis
    proof (induction arbitrary: v rule: rev_nonempty_induct2')
      case (single) hence "(x,v)  tree_edges s" "(y,v)  tree_edges s" 
        by (simp_all add: path_simps)
      with tree_eq_rule have "x=y" by simp
      with xy show ?case by contradiction
    next
      case (snocl a as) hence "(y,v)  tree_edges s" by (simp add: path_simps)
      moreover from snocl have "path (tree_edges s) x as a" "(a,v)  tree_edges s" 
        by (simp_all add: path_simps)
      ultimately have "path (tree_edges s) x as y"
        using tree_eq_rule
        by auto
      with path_is_trancl as  [] show ?case by metis
    next
      case (snocr _ a as) hence "(x,v)  tree_edges s" by (simp add: path_simps)
      moreover from snocr have "path (tree_edges s) y as a" "(a,v)  tree_edges s" 
        by (simp_all add: path_simps)
      ultimately have "path (tree_edges s) y as x"
        using tree_eq_rule
        by auto
      with path_is_trancl as  [] show ?case by metis
    next
      case (snoclr a as b bs) hence 
        "path (tree_edges s) x as a" "(a,v)  tree_edges s"
        "path (tree_edges s) y bs b" "(b,v)  tree_edges s"
        by (simp_all add: path_simps)
      moreover hence "a=b"  using tree_eq_rule by simp
      ultimately show ?thesis using snoclr.IH by metis
    qed
  qed

  lemma tree_subpath:
    assumes "(x,v)  (tree_edges s)+"
    and "(y,v)  (tree_edges s)+"
    and δ: "δ s x < δ s y"
    shows "(x,y)  (tree_edges s)+"
  proof -
    from δ have "x  y" by auto
    with assms tree_subpath' have "(x,y)  (tree_edges s)+  (y,x)  (tree_edges s)+" 
      by simp
    moreover from δ tree_path_disc have "(y,x)  (tree_edges s)+" by force
    ultimately show ?thesis by simp
  qed

  lemma on_stack_is_tree_path:
    assumes x: "x  set (stack s)"
    and y: "y  set (stack s)"
    and δ: "δ s x < δ s y"
    shows "(x,y)  (tree_edges s)+"
  proof -
    from x obtain i where i: "stack s ! i = x" "i < length (stack s)"
      by (metis in_set_conv_nth)

    from y obtain j where j: "stack s ! j = y" "j < length (stack s)"
      by (metis in_set_conv_nth)
    
    with i δ stack_nth_order have "j < i" by force
    
    from x have ne[simp]: "stack s  []" by auto

    from j<i have "x  set (tl (stack s))"
      using nth_mem nth_tl[OF ne, of "i - 1"] i
      by auto
    with tl_stack_hd_tree_path have 
      x_path: "(x, hd (stack s))  (tree_edges s)+" 
      by simp

    then show ?thesis
    proof (cases "j=0")
      case True with j have "hd (stack s) = y" by (metis hd_conv_nth ne)
      with x_path show ?thesis by simp
    next
      case False hence "y  set (tl (stack s))"
        using nth_mem nth_tl[OF ne, of "j - 1"] j
        by auto
      with tl_stack_hd_tree_path have "(y, hd (stack s))  (tree_edges s)+" 
        by simp
      with x_path δ show ?thesis
        using tree_subpath
        by metis
    qed
  qed

  lemma hd_stack_tree_path_finished:
    assumes "stack s  []"
    assumes "(hd (stack s), v)  (tree_edges s)+"
    shows "v  dom (finished s)"
  proof (cases "v  set (stack s)")
    case True
    from assms no_loop_in_tree have "hd (stack s)  v" by auto
    with True have "v  set (tl (stack s))" by (cases "stack s") auto
    with tl_stack_hd_tree_path assms have "(hd (stack s), hd (stack s))  (tree_edges s)+" by (metis trancl_trans)
    with no_loop_in_tree show ?thesis by contradiction
  next
    case False
    from assms obtain x where "(x,v)  tree_edges s" by (metis tranclE)
    with tree_edge_imp_discovered have "v  dom (discovered s)" by blast
    with False show ?thesis by (simp add: stack_set_def)
  qed

  lemma tree_edge_impl_parenthesis:
    assumes t: "(v,w)  tree_edges s"
    and f: "v  dom (finished s)"
    shows "w  dom (finished s) 
       δ s v < δ s w
       φ s w < φ s v "
  proof -
    from tree_edge_disc_lt_fin assms have "δ s w < φ s v" by simp
    with f tree_edge_imp_discovered[OF t] tree_edge_disc[OF t]
    show ?thesis
      using parenthesis_contained
      by metis
  qed

  lemma tree_path_impl_parenthesis:
    assumes "(v,w)  (tree_edges s)+"
    and "v  dom (finished s)"
    shows "w  dom (finished s) 
       δ s v < δ s w
       φ s w < φ s v "
    using assms
    by (auto elim!: trancl_induct dest: tree_edge_impl_parenthesis)

  lemma nc_reachable_v0_parenthesis:
    assumes C: "¬ cond s" "¬ is_break param s"
    and v: "v  reachable" "v  V0"
    obtains v0 where "v0  V0"
                 and "δ s v0 < δ s v  φ s v < φ s v0 "
  proof -
    from nc_discovered_eq_reachable[OF C] discovered_iff_tree_path v
    obtain v0 where "v0  V0" and
      "(v0,v)  (tree_edges s)+" 
      by auto
    moreover with nc_V0_finished[OF C] have "v0  dom (finished s)" 
      by auto
    ultimately show ?thesis
      using tree_path_impl_parenthesis that[OF v0  V0]
      by simp
  qed

end end

context param_DFS begin context begin interpretation timing_syntax .

  definition paren_imp_tree_reach where
    "paren_imp_tree_reach s  v  dom (discovered s). w  dom (finished s). 
        δ s v < δ s w  (v  dom (finished s)  φ s v > φ s w) 
                (v,w)  (tree_edges s)+"

  lemma paren_imp_tree_reach:
    "is_invar paren_imp_tree_reach"
    unfolding paren_imp_tree_reach_def[abs_def]
  proof (induct rule: is_invarI)
    case (discover s s' u v) 
    hence EQ[simp]: "tree_edges s' = insert (hd (stack s), v) (tree_edges s)"
                    "finished s' = finished s"
                    "discovered s' = (discovered s)(v  counter s)"
      by simp_all

    from discover interpret DFS_invar where s=s by simp
    from discover have NE[simp]: "stack s  []" by (simp add: cond_alt)
    
    show ?case
    proof (intro ballI impI)
      fix a b
      assume F:"a  dom (discovered s')" "b  dom (finished s')"
        and D: "δ s' a < δ s' b  (a  dom (finished s')  φ s' a > φ s' b)"
        
      from F finished_discovered discover have "b  v" by auto
      show "(a,b)  (tree_edges s')+"
      proof (cases "a = v")
        case True with D bv have "counter s < δ s b" by simp
        also from F have "b  dom (discovered s)" 
          using finished_discovered by auto
        with timing_less_counter have "δ s b < counter s" by simp
        finally have False .
        thus ?thesis ..
      next
        case False with bv F D discover have "(a,b)  (tree_edges s)+" by simp
        thus ?thesis by (auto intro: trancl_mono_mp)
      qed
    qed
  next
    case (finish s s' u) 
    hence EQ[simp]: "tree_edges s' = tree_edges s"
                    "finished s' = (finished s)(hd (stack s)  counter s)"
                    "discovered s' = discovered s"
                    "stack s' = tl (stack s)"
      by simp_all

    from finish interpret DFS_invar where s=s by simp
    from finish have NE[simp]: "stack s  []" by (simp add: cond_alt)

    show ?case
    proof (intro ballI impI)
      fix a b
      assume F: "a  dom (discovered s')" "b  dom (finished s')"
        and paren: "δ s' a < δ s' b  (a  dom (finished s')  φ s' a > φ s' b)"
      hence "a  b" by auto
      
      show "(a,b)  (tree_edges s')+"
      proof (cases "b = hd (stack s)")
        case True hence φb: "φ s' b = counter s" by simp
        have "a  set (stack s)"
          unfolding stack_set_def
        proof
          from F show "a  dom (discovered s)" by simp
          from True ab φb paren have "a  dom (finished s)  φ s a > counter s" by simp
          with timing_less_counter show "a  dom (finished s)" by force
        qed 
        with paren True on_stack_is_tree_path have "(a,b)  (tree_edges s)+" by auto
        thus ?thesis by (auto intro: trancl_mono_mp)
      next
        case False note b_not_hd = this
        show ?thesis
        proof (cases "a = hd (stack s)")
          case False with b_not_hd F paren finish show ?thesis by simp
        next
          case True with paren b_not_hd F have 
            "a  dom (discovered s)" "b  dom (finished s)"  "δ s a < δ s b"  
            by simp_all
          moreover from True stack_not_finished have "a  dom (finished s)" 
            by simp
          ultimately show ?thesis by (simp add: finish)
        qed
      qed
    qed  
  next
    case (new_root s s' v0) then interpret DFS_invar where s=s by simp
    from new_root finished_discovered have "v0  dom (finished s)" by auto
    moreover note timing_less_counter finished_discovered
    ultimately show ?case using new_root by clarsimp force
  qed simp_all
end end

context DFS_invar begin context begin interpretation timing_syntax .

  lemmas s_paren_imp_tree_reach =
    paren_imp_tree_reach[THEN make_invar_thm]
  
  lemma parenthesis_impl_tree_path_not_finished:
    assumes "v  dom (discovered s)"
    and "w  dom (finished s)"
    and "δ s v < δ s w"
    and "v  dom (finished s)"
    shows "(v,w)  (tree_edges s)+"
    using s_paren_imp_tree_reach assms
    by (auto simp add: paren_imp_tree_reach_def)

  lemma parenthesis_impl_tree_path:
    assumes "v  dom (finished s)" "w  dom (finished s)"
    and "δ s v < δ s w" "φ s v > φ s w"
    shows "(v,w)  (tree_edges s)+"
  proof -
    from assms(1) have "v  dom (discovered s)"
      using finished_discovered by blast
    with assms show ?thesis
      using s_paren_imp_tree_reach assms
      by (auto simp add: paren_imp_tree_reach_def)
  qed

  lemma tree_path_iff_parenthesis:
    assumes "v  dom (finished s)" "w  dom (finished s)"
    shows "(v,w)  (tree_edges s)+  δ s v < δ s w  φ s v > φ s w"
    using assms
    by (metis parenthesis_impl_tree_path tree_path_impl_parenthesis) 

  lemma no_pending_succ_impl_path_in_tree:
    assumes v: "v  dom (discovered s)" "pending s `` {v} = {}"
    and w: "w  succ v"
    and δ: "δ s v < δ s w"
    shows "(v,w)  (tree_edges s)+"
  proof (cases "v  dom (finished s)")
    case True 
    with assms assms have "δ s w < φ s v" "w  dom (discovered s)"
      using finished_succ_fin finished_imp_succ_discovered 
      by simp_all
    with True δ show ?thesis
      using parenthesis_contained parenthesis_impl_tree_path
      by blast
  next
    case False
    show ?thesis
    proof (cases "w  dom (finished s)")
      case True with False v δ show ?thesis by (simp add: parenthesis_impl_tree_path_not_finished)
    next
      case False with v  dom (finished s) no_pending_imp_succ_discovered v w have 
        "v  set (stack s)" "w  set (stack s)" 
        by (simp_all add: stack_set_def)
      with on_stack_is_tree_path δ show ?thesis by simp
    qed
  qed

  lemma finished_succ_impl_path_in_tree:
    assumes f:  "v  dom (finished s)"
    and s: "w  succ v"
    and δ: "δ s v < δ s w"
    shows "(v,w)  (tree_edges s)+"
    using no_pending_succ_impl_path_in_tree finished_no_pending finished_discovered
    using assms
    by blast
end end

subsubsection ‹Properties of Cross Edges›
(* Cross Edges *)
context param_DFS begin context begin interpretation timing_syntax .

  lemma i_cross_edges_finished: "is_invar (λs. (u,v)cross_edges s. 
    v  dom (finished s)  (u  dom (finished s)  φ s v < φ s u))"
  proof (induction rule: is_invarI_full)
    case (finish s s' u e)
    interpret DFS_invar G param s by fact
    from finish stack_not_finished have "u  dom (finished s)" by auto
    with finish show ?case by (auto intro: timing_less_counter)
  next
    case (cross_edge s s' u v e)
    interpret DFS_invar G param s by fact
    from cross_edge stack_not_finished have "u  dom (finished s)" by auto
    with cross_edge show ?case by (auto intro: timing_less_counter)
  qed simp_all

end end

context DFS_invar begin context begin interpretation timing_syntax .
  lemmas cross_edges_finished 
    = i_cross_edges_finished[THEN make_invar_thm]

  lemma cross_edges_target_finished: 
    "(u,v)cross_edges s  v  dom (finished s)" 
    using cross_edges_finished by auto

  lemma cross_edges_finished_decr: 
    "(u,v)cross_edges s; udom (finished s)  φ s v < φ s u" 
    using cross_edges_finished by auto

  lemma cross_edge_unequal:
    assumes cross: "(v,w)  cross_edges s"
    shows "v  w"
  proof -
    from cross_edges_target_finished[OF cross] have 
      w_fin: "w  dom (finished s)" .

    show ?thesis
    proof (cases "v  dom (finished s)")
      case True with cross_edges_finished_decr[OF cross] 
      show ?thesis by force
    next
      case False with w_fin show ?thesis by force
    qed
  qed 
end end


subsubsection ‹Properties of Back Edges›
(* Back Edges *)
context param_DFS begin context begin interpretation timing_syntax .
  
  lemma i_back_edge_impl_tree_path:
    "is_invar (λs. (v,w)  back_edges s. (w,v)  (tree_edges s)+  w = v)"
  proof (induct rule: is_invarI_full)
    case (back_edge s s' u v) then interpret DFS_invar where s=s by simp

    from back_edge have st: "v  set (stack s)" "u  set (stack s)"
      using stack_set_def
      by auto
   
    have "(v,u)  (tree_edges s)+  u = v"
    proof (rule disjCI)
      assume "u  v"
      with st back_edge have "v  set (tl (stack s))" by (metis not_hd_in_tl)
      with tl_lt_stack_hd_discover st back_edge have "δ s v < δ s u" by simp
      with on_stack_is_tree_path st show "(v,u)  (tree_edges s)+" by simp
    qed
    with back_edge show ?case by auto
  next
    case discover thus ?case using trancl_sub_insert_trancl by force
  qed simp_all

end end

context DFS_invar begin context begin interpretation timing_syntax .

  lemma back_edge_impl_tree_path:
    "(v,w)  back_edges s; v  w  (w,v)  (tree_edges s)+"
    using i_back_edge_impl_tree_path[THEN make_invar_thm]
    by blast

  lemma back_edge_disc:
    assumes "(v,w)  back_edges s"
    shows "δ s w  δ s v"
  proof cases
    assume "vw" 
    with assms back_edge_impl_tree_path have "(w,v)  (tree_edges s)+" by simp
    with tree_path_disc show ?thesis by force
  qed simp

  lemma back_edges_tree_disjoint:
    "back_edges s  tree_edges s = {}"
    using back_edge_disc tree_edge_disc
    by force

  lemma back_edges_tree_pathes_disjoint:
    "back_edges s  (tree_edges s)+ = {}"
    using back_edge_disc tree_path_disc
    by force

  lemma back_edge_finished:
    assumes "(v,w)  back_edges s"
    and "w  dom (finished s)"
    shows "v  dom (finished s)  φ s v  φ s w"
  proof (cases "v=w")
    case True with assms show ?thesis by simp
  next
    case False with back_edge_impl_tree_path assms have "(w,v)  (tree_edges s)+" by simp
    with tree_path_impl_parenthesis assms show ?thesis by fastforce
  qed

end end

context param_DFS begin context begin interpretation timing_syntax .
  (* The lemma should probably replaced by:
     is_invar (λs. ∀(v,w) ∈ (tree_edges s)+. v ∈ succ w ⟶ (w,v) ∈ back_edges s ∨ (w,v) ∈ pending s)
  *)
  lemma i_disc_imp_back_edge_or_pending:
    "is_invar (λs. (v,w)  E. 
        v  dom (discovered s)  w  dom (discovered s)
       δ s v  δ s w
       (w  dom (finished s)  v  dom (finished s)  φ s w  φ s v)
       (v,w)  back_edges s  (v,w)  pending s)"
  proof (induct rule: is_invarI_full)
    case (cross_edge s s' u v) then interpret DFS_invar where s=s by simp
    from cross_edge stack_not_finished[of u] have "u  dom (finished s)"
      using hd_in_set
      by (auto simp add: cond_alt)
    with cross_edge show ?case by auto
  next
    case (finish s s' u v) then interpret DFS_invar where s=s by simp

    from finish have 
      IH: "v w. w  succ v; v  dom (discovered s); w  dom (discovered s); 
                  δ s w  δ s v;
                  (w  dom (finished s)  v  dom (finished s)  φ s v  φ s w)
                  (v, w)  back_edges s  (v, w)  pending s" 
      by blast

    from finish have ne[simp]: "stack s  []"
                 and p[simp]: "pending s `` {hd (stack s)} = {}"
      by (simp_all)

    from hd_in_set[OF ne] have disc: "hd (stack s)  dom (discovered s)" 
                            and not_fin: "hd (stack s)  dom (finished s)"
      using stack_discovered stack_not_finished
      by blast+

    {
      fix w
      assume w: "w  succ (hd (stack s))" "w  hd (stack s)" "w  dom (discovered s)"
        and f: "w  dom (finished s)  counter s  φ s w"
        and δ: "δ s w  δ s (hd (stack s))"

      with timing_less_counter have "w  dom (finished s)" by force
      with finish w δ disc have "(hd (stack s), w)  back_edges s" by blast
    }

    moreover
    {
      fix w
      assume "hd (stack s)  succ w" "w  hd (stack s)"
      and "w  dom (finished s)" "δ s (hd (stack s))  δ s w"
      with IH[of "hd (stack s)" w] disc not_fin have
        "(w, hd (stack s))  back_edges s"
        using finished_discovered finished_no_pending[of w]
        by blast
    }

    ultimately show ?case
      using finish
      by clarsimp auto
  next
    case (discover s s' u v) then interpret DFS_invar where s=s by simp

    from discover show ?case 
      using timing_less_counter
      by clarsimp fastforce
  next
    case (new_root s s' v0) then interpret DFS_invar where s=s by simp

    from new_root empty_stack_imp_empty_pending have "pending s = {}" by simp
    with new_root show ?case 
      using timing_less_counter
      by clarsimp fastforce
  qed auto
end end

context DFS_invar begin context begin interpretation timing_syntax .

  lemma disc_imp_back_edge_or_pending:
    "w  succ v; v  dom (discovered s); w  dom (discovered s); δ s w  δ s v;
      (w  dom (finished s)  v  dom (finished s)  φ s v  φ s w)
      (v, w)  back_edges s  (v, w)  pending s"
    using i_disc_imp_back_edge_or_pending[THEN make_invar_thm]
    by blast

  lemma finished_imp_back_edge:
    "w  succ v; v  dom (finished s); w  dom (finished s); 
      δ s w  δ s v; φ s v  φ s w
      (v, w)  back_edges s"
    using disc_imp_back_edge_or_pending finished_discovered finished_no_pending
    by fast

  lemma finished_not_finished_imp_back_edge:
    "w  succ v; v  dom (finished s); w  dom (discovered s);
      w  dom (finished s);
      δ s w  δ s v
      (v, w)  back_edges s"
    using disc_imp_back_edge_or_pending finished_discovered finished_no_pending
    by fast

  lemma finished_self_loop_in_back_edges:
    assumes "v  dom (finished s)"
    and "(v,v)  E"
    shows "(v,v)  back_edges s"
    using assms
    using finished_imp_back_edge
    by blast
end end

(* Back edges and Cycles *)

context DFS_invar begin 

  context begin interpretation timing_syntax .
    (* Cross and tree_edges edges are always acyclic *)
    lemma tree_cross_acyclic:
      "acyclic (tree_edges s  cross_edges s)" (is "acyclic ?E")
    proof (rule ccontr)
      {
        fix u v
        assume *: "u  dom (finished s)" and "(u,v)  ?E+"
        from this(2) have "φ s v < φ s u  v  dom (finished s)"
        proof induct
          case base thus ?case 
            by (metis Un_iff * cross_edges_finished_decr cross_edges_target_finished tree_edge_impl_parenthesis)
        next
          case (step v w)
          hence "φ s w < φ s v  w  dom (finished s)"
            by (metis Un_iff cross_edges_finished_decr cross_edges_target_finished tree_edge_impl_parenthesis)
          with step show ?case by auto
        qed
      } note aux = this

      assume "¬ acyclic ?E"
      then obtain u where path: "(u,u)  ?E+" by (auto simp add: acyclic_def)
      show False
      proof cases
        assume "u  dom (finished s)" 
        with aux path show False by blast
      next
        assume *: "u  dom (finished s)"
        moreover 
        from no_loop_in_tree have "(u,u)  (tree_edges s)+" .
        with trancl_union_outside[OF path] obtain x y where "(u,x)  ?E*" "(x,y)  cross_edges s" "(y,u)  ?E*" by auto
        with cross_edges_target_finished have "y  dom (finished s)" by simp
        moreover with * (y,u)  ?E* have "(y,u)  ?E+" by (auto simp add: rtrancl_eq_or_trancl)
        ultimately show False by (metis aux)
      qed
    qed
  end

  lemma cycle_contains_back_edge:
    assumes cycle: "(u,u)  (edges s)+"
    shows "v w. (u,v)  (edges s)*  (v,w)  back_edges s  (w,u)  (edges s)*"
  proof -
    from tree_cross_acyclic have "(u,u)  (tree_edges s  cross_edges s)+" by (simp add: acyclic_def)
    with trancl_union_outside[OF cycle] show ?thesis .
  qed

  lemma cycle_needs_back_edge:
    assumes "back_edges s = {}"
    shows "acyclic (edges s)"
  proof (rule ccontr)
    assume "¬ acyclic (edges s)"
    then obtain u where "(u,u)  (edges s)+" by (auto simp: acyclic_def)
    with assms have "(u,u)  (tree_edges s  cross_edges s)+" by auto
    with tree_cross_acyclic show False by (simp add: acyclic_def)
  qed

  lemma back_edge_closes_cycle:
    assumes "back_edges s  {}"
    shows "¬ acyclic (edges s)"
  proof -
    from assms obtain v w where be: "(v,w)  back_edges s" by auto
    hence "(w,w)  (edges s)+"
    proof (cases "v=w")
      case False 
      with be back_edge_impl_tree_path have "(w,v)  (tree_edges s)+" by simp
      hence "(w,v)  (edges s)+" by (blast intro: trancl_mono_mp)
      also from be have "(v,w)  edges s" by simp
      finally show ?thesis .
    qed auto
    thus ?thesis by (auto simp add: acyclic_def)
  qed

  lemma back_edge_closes_reachable_cycle:
    "back_edges s  {}  ¬ acyclic (E  reachable × UNIV)"
    by (metis back_edge_closes_cycle edges_ss_reachable_edges cyclic_subset)

  lemma cycle_iff_back_edges:
    "acyclic (edges s)  back_edges s = {}"
  by (metis back_edge_closes_cycle cycle_needs_back_edge)
end 


subsection ‹White Path Theorem›

context DFS begin
context begin interpretation timing_syntax .

  definition white_path where
    "white_path s x y  xy 
        (p. path E x p y  
               (δ s x < δ s y  ( v  set (tl p). δ s x < δ s v)))"

  lemma white_path:
    "it_dfs  SPEC(λs. x  reachable. y  reachable. ¬ is_break param s  
            white_path s x y  (x,y)  (tree_edges s)*)"
  proof (rule it_dfs_SPEC, intro ballI impI)
    fix s x y
    assume DI: "DFS_invar G param s"
      and C: "¬ cond s" "¬ is_break param s"
      and reach: "x  reachable" "y  reachable"

    from DI interpret DFS_invar where s=s .

    note fin_eq_reach = nc_finished_eq_reachable[OF C]

    show "white_path s x y  (x,y)  (tree_edges s)*"
    proof (cases "x=y")
      case True thus ?thesis by (simp add: white_path_def)
    next
      case False
      
      show ?thesis
      proof
        assume "(x,y)  (tree_edges s)*"
        with xy have T: "(x,y)  (tree_edges s)+" by (metis rtranclD)
        then obtain p where P: "path (tree_edges s) x p y" by (metis trancl_is_path)
        with tree_edges_ssE have "path E x p y" using path_mono[where E="tree_edges s"] 
          by simp
        moreover 
        from P have "δ s x < δ s y  ( v  set (tl p). δ s x < δ s v)"
          using xy
        proof (induct rule: path_tl_induct)
          case (single u) thus ?case by (fact tree_edge_disc)
        next
          case (step u v) note δ s x < δ s u
          also from step have "δ s u < δ s v" by (metis tree_edge_disc)
          finally show ?case .
        qed
        ultimately show "white_path s x y"
          by (auto simp add: xy white_path_def)
      next
        assume "white_path s x y"
        with xy obtain p where 
            P:"path E x p y" and
            white: "δ s x < δ s y  ( v  set (tl p). δ s x < δ s v)"
          unfolding white_path_def
          by blast
        hence "p  []" by auto
        thus "(x,y)  (tree_edges s)*" using P white reach(2)
        proof (induction p arbitrary: y rule: rev_nonempty_induct)
          case single hence "y  succ x" by (simp add: path_cons_conv)
          with reach single show ?case 
            using fin_eq_reach finished_succ_impl_path_in_tree[of x y] 
            by simp
        next
          case (snoc u us) hence "path E x us u" by (simp add: path_append_conv)
          moreover hence "(x,u)  E*" by (simp add: path_is_rtrancl)
          with reach have ureach: "u  reachable" 
            by (metis rtrancl_image_advance_rtrancl) 
          moreover from snoc have "δ s x < δ s u" "(vset (tl us). δ s x < δ s v)" 
            by simp_all
          ultimately have x_u: "(x,u)  (tree_edges s)*" by (metis snoc.IH)
            
          from snoc have "y  succ u" by (simp add: path_append_conv)
          from snoc(5) fin_eq_reach finished_discovered have 
            y_f_d: "y  dom (finished s)" "y  dom (discovered s)"
            by auto
            
          from y  succ u ureach fin_eq_reach have "δ s y < φ s u" 
            using finished_succ_fin by simp
          also from δ s x < δ s u have "x  u" by auto
          with x_u have "(x,u)  (tree_edges s)+" by (metis rtrancl_eq_or_trancl)
          with fin_eq_reach reach have "φ s u < φ s x" 
            using tree_path_impl_parenthesis
            by simp
          finally have "φ s y < φ s x" 
            using reach fin_eq_reach y_f_d snoc
            using parenthesis_contained
            by blast
          hence "(x,y)  (tree_edges s)+"
            using reach fin_eq_reach y_f_d snoc
            using parenthesis_impl_tree_path
            by blast
          thus ?case by auto
        qed
      qed
    qed
  qed
end end


end