Theory Param_DFS

section ‹General DFS with Hooks›
theory Param_DFS
imports 
  CAVA_Base.CAVA_Base
  CAVA_Automata.Digraph
  "Misc/DFS_Framework_Refine_Aux"
begin

text ‹
  We define a general DFS algorithm, which is parameterized over
  hook functions at certain events during the DFS.
›

subsection ‹State and Parameterization›
(* A DFS with timing and a stack, phrased iteratively *)
text ‹The state of the general DFS. 
  Users may inherit from this state using the record package's 
  inheritance support.
›
record 'v state =
  counter :: nat               ― ‹Node counter (timer)›
  discovered :: "'v ⇀ nat"    ― ‹Discovered times of nodes›
  finished :: "'v ⇀ nat"      ― ‹Finished times of nodes›
  pending :: "('v × 'v) set"  ― ‹Edges to be processed next›
  stack :: "'v list"          ― ‹Current DFS stack›
  tree_edges :: "'v rel"      ― ‹Tree edges›
  back_edges :: "'v rel"      ― ‹Back edges›
  cross_edges :: "'v rel"     ― ‹Cross edges›

abbreviation "NOOP s ≡ RETURN (state.more s)"

text ‹Record holding the parameterization.›
record ('v,'s,'es) gen_parameterization =
  on_init :: "'es nres"
  on_new_root :: "'v ⇒ 's ⇒ 'es nres"
  on_discover :: "'v ⇒ 'v ⇒ 's ⇒ 'es nres"
  on_finish :: "'v ⇒ 's ⇒ 'es nres"
  on_back_edge :: "'v ⇒ 'v ⇒ 's ⇒ 'es nres"
  on_cross_edge :: "'v ⇒ 'v ⇒ 's ⇒ 'es nres"
  is_break :: "'s ⇒ bool"

text ‹Default type restriction for parameterizations.
  The event handler functions go from a complete state to
  the user-defined part of the state (i.e. the fields added by inheritance).
›
type_synonym ('v,'es) parameterization 
  = "('v,('v,'es) state_scheme,'es) gen_parameterization"

text ‹Default parameterization, the functions do nothing.
  This can be used as the basis for specialized parameterizations, which may 
  be derived by updating some fields.
›
definition "⋀more init. dflt_parametrization more init ≡ ⦇  
  on_init = init,
  on_new_root = λ_. RETURN o more,
  on_discover = λ_ _. RETURN o more,
  on_finish = λ_. RETURN o more,
  on_back_edge = λ_ _. RETURN o more,
  on_cross_edge = λ_ _. RETURN o more,
  is_break = λ_. False ⦈"
lemmas dflt_parametrization_simp[simp] =
  gen_parameterization.simps[mk_record_simp, OF dflt_parametrization_def]

text ‹This locale builds a DFS algorithm from a graph and a parameterization.›
locale param_DFS_defs =
  graph_defs G
  for G :: "('v, 'more) graph_rec_scheme"
  +
  fixes param :: "('v,'es) parameterization"
begin
  subsection ‹DFS operations›
  subsubsection ‹Node predicates›
  text ‹First, we define some predicates to check whether nodes are in certain sets›
  definition is_discovered :: "'v ⇒ ('v,'es) state_scheme ⇒ bool"
    where "is_discovered u s ≡ u ∈ dom (discovered s)"

  definition is_finished :: "'v ⇒ ('v,'es) state_scheme ⇒ bool"
    where "is_finished u s ≡ u ∈ dom (finished s)"

  definition is_empty_stack :: "('v,'es) state_scheme ⇒ bool"
    where "is_empty_stack s ≡ stack s = []"

  (*definition top_pending :: "('v,'es) state_scheme ⇒ 'v × 'v set" where
    "top_pending s ≡ (hd (stack s), pending s `` {hd (stack s)})"*)

  subsubsection ‹Effects on Basic State›
  text ‹We define the effect of the operations on the basic part of the state›
  definition discover 
    :: "'v ⇒ 'v ⇒ ('v,'es) state_scheme ⇒ ('v,'es) state_scheme"
  where
  "discover u v s ≡ let
    d = (discovered s)(v ↦ counter s); c = counter s + 1;
    st = v#stack s;
    p = pending s ∪ {v} × E``{v};
    t = insert (u,v) (tree_edges s)
  in s⦇ discovered := d, counter := c, stack := st, pending := p, tree_edges := t⦈"

  lemma discover_simps[simp]:
    "counter (discover u v s) = Suc (counter s)"
    "discovered (discover u v s) = (discovered s)(v ↦ counter s)" 
    "finished (discover u v s) = finished s"
    "stack (discover u v s) = v#stack s"
    "pending (discover u v s) = pending s ∪ {v} × E``{v}"
    "tree_edges (discover u v s) = insert (u,v) (tree_edges s)"
    "cross_edges (discover u v s) = cross_edges s"
    "back_edges (discover u v s) = back_edges s"
    "state.more (discover u v s) = state.more s"
    by (simp_all add: discover_def)

  definition finish 
    :: "'v ⇒ ('v,'es) state_scheme ⇒ ('v,'es) state_scheme" 
  where
  "finish u s ≡ let
    f = (finished s)(u ↦ counter s); c = counter s + 1;
    st = tl (stack s)
  in s⦇ finished := f, counter := c, stack := st⦈"

  lemma finish_simps[simp]:
    "counter (finish u s) = Suc (counter s)"
    "discovered (finish u s) = discovered s"
    "finished (finish u s) = (finished s)(u ↦ counter s)"
    "stack (finish u s) = tl (stack s)"
    "pending (finish u s) = pending s"
    "tree_edges (finish u s) = tree_edges s"
    "cross_edges (finish u s) = cross_edges s"
    "back_edges (finish u s) = back_edges s"
    "state.more (finish u s) = state.more s"
    by (simp_all add: finish_def)

  definition back_edge
    :: "'v ⇒ 'v ⇒ ('v,'es) state_scheme ⇒ ('v,'es) state_scheme"
  where
  "back_edge u v s ≡ let
    b = insert (u,v) (back_edges s)
   in s⦇ back_edges := b ⦈"

  lemma back_edge_simps[simp]:
    "counter (back_edge u v s) = counter s"
    "discovered (back_edge u v s) = discovered s"
    "finished (back_edge u v s) = finished s"
    "stack (back_edge u v s) = stack s"
    "pending (back_edge u v s) = pending s"
    "tree_edges (back_edge u v s) = tree_edges s"
    "cross_edges (back_edge u v s) = cross_edges s"
    "back_edges (back_edge u v s) = insert (u,v) (back_edges s)"
    "state.more (back_edge u v s) = state.more s"
    by (simp_all add: back_edge_def)

  definition cross_edge
    :: "'v ⇒ 'v ⇒ ('v,'es) state_scheme ⇒ ('v,'es) state_scheme"
  where
  "cross_edge u v s ≡ let
    c = insert (u,v) (cross_edges s)
   in s⦇ cross_edges := c ⦈"
  
  lemma cross_edge_simps[simp]:
    "counter (cross_edge u v s) = counter s"
    "discovered (cross_edge u v s) = discovered s"
    "finished (cross_edge u v s) = finished s"
    "stack (cross_edge u v s) = stack s"
    "pending (cross_edge u v s) = pending s"
    "tree_edges (cross_edge u v s) = tree_edges s"
    "cross_edges (cross_edge u v s) = insert (u,v) (cross_edges s)"
    "back_edges (cross_edge u v s) = back_edges s"
    "state.more (cross_edge u v s) = state.more s"
    by (simp_all add: cross_edge_def)


  definition new_root
    :: "'v ⇒ ('v,'es) state_scheme ⇒ ('v,'es) state_scheme"
  where
    "new_root v0 s ≡ let
       c = Suc (counter s);
       d = (discovered s)(v0 ↦ counter s);
       p = {v0}×E``{v0};
       st = [v0]
     in s⦇counter := c, discovered := d, pending := p, stack := st⦈"

  lemma new_root_simps[simp]:
    "counter (new_root v0 s) = Suc (counter s)"
    "discovered (new_root v0 s) = (discovered s)(v0 ↦ counter s)"
    "finished (new_root v0 s) = finished s"
    "stack (new_root v0 s) = [v0]"
    "pending (new_root v0 s) = ({v0}×E``{v0})"
    "tree_edges (new_root v0 s) = tree_edges s"
    "cross_edges (new_root v0 s) = cross_edges s"
    "back_edges (new_root v0 s) = back_edges s"
    "state.more (new_root v0 s) = state.more s"
    by (simp_all add: new_root_def)

  definition "empty_state e
    ≡ ⦇ counter = 0,
         discovered = Map.empty,
         finished = Map.empty,
         pending = {},
         stack = [],
         tree_edges = {},
         back_edges = {},
         cross_edges = {},
         … = e ⦈"

  lemma empty_state_simps[simp]:
    "counter (empty_state e) = 0"
    "discovered (empty_state e) = Map.empty"
    "finished (empty_state e) = Map.empty"
    "pending (empty_state e) = {}"
    "stack (empty_state e) = []"
    "tree_edges (empty_state e) = {}"
    "back_edges (empty_state e) = {}"
    "cross_edges (empty_state e) = {}"
    "state.more (empty_state e) = e"
    by (simp_all add: empty_state_def)




  subsubsection ‹Effects on Whole State›  
  text ‹The effects of the operations on the whole state are defined by 
    combining the effects of the basic state with the parameterization.›
  
  definition do_cross_edge
    :: "'v ⇒ 'v ⇒ ('v,'es) state_scheme ⇒ ('v,'es) state_scheme nres"
  where
  "do_cross_edge u v s ≡ do {
      let s = cross_edge u v s;
      e ← on_cross_edge param u v s;
      RETURN (s⦇state.more := e⦈)
    }"

  definition do_back_edge
    :: "'v ⇒ 'v ⇒ ('v,'es) state_scheme ⇒ ('v,'es) state_scheme nres"
  where
  "do_back_edge u v s ≡ do {
      let s = back_edge u v s;
      e ← on_back_edge param u v s;
      RETURN (s⦇state.more := e⦈)
    }"

  definition do_known_edge
    :: "'v ⇒ 'v ⇒ ('v,'es) state_scheme ⇒ ('v,'es) state_scheme nres"
  where
  "do_known_edge u v s ≡ 
    if is_finished v s then 
      do_cross_edge u v s 
    else 
      do_back_edge u v s"  

  definition do_discover
    :: "'v ⇒ 'v ⇒ ('v,'es) state_scheme ⇒ ('v,'es) state_scheme nres"
  where
  "do_discover u v s ≡ do {
    let s = discover u v s;
    e ← on_discover param u v s;
    RETURN (s⦇state.more := e⦈)
  }"

  definition do_finish
    :: "'v ⇒ ('v,'es) state_scheme ⇒ ('v,'es) state_scheme nres"
  where
  "do_finish u s ≡ do {
    let s = finish u s;
    e ← on_finish param u s;
    RETURN (s⦇state.more := e⦈)
  }"

  definition get_new_root where
    "get_new_root s ≡ SPEC (λv. v∈V0 ∧ ¬is_discovered v s)"  

  definition do_new_root where 
  "do_new_root v0 s ≡ do {
    let s = new_root v0 s;
    e ← on_new_root param v0 s;
    RETURN (s⦇state.more := e⦈)
  }"

  lemmas op_defs = discover_def finish_def back_edge_def cross_edge_def new_root_def
  lemmas do_defs = do_discover_def do_finish_def do_known_edge_def
    do_cross_edge_def do_back_edge_def do_new_root_def
  lemmas pred_defs = is_discovered_def is_finished_def is_empty_stack_def

  definition "init ≡ do {
    e ← on_init param;
    RETURN (empty_state e)
  }"

  subsection ‹DFS Algorithm›
  text ‹We phrase the DFS algorithm iteratively:
    While there are undiscovered root nodes or the stack is not empty,
      inspect the topmost node on the stack: 
        Follow any pending edge, or finish the node if there 
        are no pending edges left.

    ›

  definition cond :: "('v,'es) state_scheme ⇒ bool" where
    "cond s ⟷ (V0 ⊆ {v. is_discovered v s} ⟶ ¬is_empty_stack s) 
      ∧ ¬is_break param s"  

  lemma cond_alt:
    "cond = (λs. (V0 ⊆ dom (discovered s) ⟶ stack s ≠ []) ∧ ¬is_break param s)"
    apply (rule ext)
    unfolding cond_def is_discovered_def is_empty_stack_def
    by auto


  definition get_pending ::
    "('v, 'es) state_scheme ⇒ ('v × 'v option × ('v, 'es) state_scheme) nres" 
    ― ‹Get topmost stack node and a pending edge if any. The pending
          edge is removed.›
  where "get_pending s ≡ do {
    let u = hd (stack s);
    let Vs = pending s `` {u};

    if Vs = {} then
      RETURN (u,None,s)
    else do {
      v ← RES Vs;
      let s = s⦇ pending := pending s - {(u,v)}⦈;
      RETURN (u,Some v,s)
    }
  }"

  definition step :: "('v,'es) state_scheme ⇒ ('v,'es) state_scheme nres" 
  where
    "step s ≡ 
      if is_empty_stack s then do {
        v0 ← get_new_root s;
        do_new_root v0 s
      } else do {
        (u,Vs,s) ← get_pending s;
        case Vs of 
          None ⇒ do_finish u s 
        | Some v ⇒ do {
          if is_discovered v s then 
            do_known_edge u v s
          else 
            do_discover u v s
        }
      }"


  definition "it_dfs ≡ init ⤜ WHILE cond step"
  definition "it_dfsT ≡ init ⤜ WHILET cond step"

end

subsection ‹Invariants›
text ‹We now build the infrastructure for establishing invariants 
  of DFS algorithms. The infrastructure is modular and extensible, i.e., 
  we can define re-usable libraries of invariants.
›


text ‹For technical reasons, invariants are established in a two-step process:
  ▸ First, we prove the invariant wrt. the parameterization in the ‹param_DFS› locale.
  ▸ Next, we transfer the invariant to the ‹DFS_invar›-locale.
›
(* This locale is required to establish new invariants.
  We would like to directly establish new invariants in the 
  DFS_invar-locale, unfortunately this causes technical problems:
  When interpreting the DFS_invar locale in a proof inside the 
  DFS_invar-locale itself, we get "duplicate constant" warnings,
  unless we prefix the interpreted locale, which may be quite confusing
  in a proof, as the user has to choose the prefixed lemmas, while the
  unprefixed ones are also available, but for the wrong state.
 *)
locale param_DFS =
  fb_graph G + param_DFS_defs G param
  for G :: "('v, 'more) graph_rec_scheme"
  and param :: "('v,'es) parameterization"
begin

  definition is_invar :: "(('v, 'es) state_scheme ⇒ bool) ⇒ bool"
    ― ‹Predicate that states that @{term I} is an invariant.›
    where "is_invar I ≡ is_rwof_invar init cond step I"

end

text ‹Invariants are transferred to this locale, which is parameterized
  with a state. ›
locale DFS_invar =
  param_DFS G param
  for G :: "('v, 'more) graph_rec_scheme"
  and param :: "('v,'es) parameterization"
  +
  fixes s :: "('v,'es) state_scheme"
  assumes rwof: "rwof init cond step s"
begin

  lemma make_invar_thm: "is_invar I ⟹ I s"
    ― ‹Lemma to transfer an invariant into this locale›
    using rwof_cons[OF _ rwof, folded is_invar_def] .

end

subsubsection ‹Establishing Invariants›
context param_DFS
begin
  text ‹ Include this into refine-rules to discard any information about 
    parameterization ›
  lemmas indep_invar_rules = 
    leof_True_rule[where m="on_init param"]
    leof_True_rule[where m="on_new_root param v0 s'" for v0 s']
    leof_True_rule[where m="on_discover param u v s'" for u v s']
    leof_True_rule[where m="on_finish param v s'" for v s']
    leof_True_rule[where m="on_cross_edge param u v s'" for u v s']
    leof_True_rule[where m="on_back_edge param u v s'" for u v s']

  
  lemma rwof_eq_DFS_invar[simp]: 
    "rwof init cond step = DFS_invar G param"
    ― ‹The DFS-invar locale is equivalent to the strongest invariant of the loop.›
    apply (auto intro: DFS_invar.rwof intro!: ext)
    by unfold_locales

  lemma DFS_invar_step: "⟦nofail it_dfs; DFS_invar G param s; cond s⟧ 
    ⟹ step s ≤ SPEC (DFS_invar G param)"
    ― ‹A step preserves the (best) invariant.›
    unfolding it_dfs_def rwof_eq_DFS_invar[symmetric]
    by (rule rwof_step)

  lemma DFS_invar_step': "⟦nofail (step s); DFS_invar G param s; cond s⟧ 
    ⟹ step s ≤ SPEC (DFS_invar G param)"
    unfolding it_dfs_def rwof_eq_DFS_invar[symmetric]
    by (rule rwof_step')

  text ‹We define symbolic names for the preconditions of certain operations›
  definition "pre_is_break s ≡ DFS_invar G param s"

  definition "pre_on_new_root v0 s' ≡ ∃s.
    DFS_invar G param s ∧ cond s ∧ 
    stack s = [] ∧ v0 ∈ V0 ∧ v0 ∉ dom (discovered s) ∧
    s' = new_root v0 s"

  definition "pre_on_finish u s' ≡ ∃s.
    DFS_invar G param s ∧ cond s ∧ 
    stack s ≠ [] ∧ u = hd (stack s) ∧ pending s `` {u} = {} ∧ s' = finish u s"

  definition "pre_edge_selected u v s ≡ 
    DFS_invar G param s ∧ cond s ∧ 
    stack s ≠ [] ∧ u = hd (stack s) ∧ (u, v) ∈ pending s"

  definition "pre_on_cross_edge u v s' ≡ ∃s. pre_edge_selected u v s ∧
        v ∈ dom (discovered s) ∧ v∈dom (finished s) 
        ∧ s' = cross_edge u v (s⦇pending := pending s - {(u,v)}⦈)"

  definition "pre_on_back_edge u v s' ≡ ∃s. pre_edge_selected u v s ∧
        v ∈ dom (discovered s) ∧ v∉dom (finished s) 
        ∧ s' = back_edge u v (s⦇pending := pending s - {(u,v)}⦈)"

  definition "pre_on_discover u v s' ≡ ∃s. pre_edge_selected u v s ∧
        v ∉ dom (discovered s) 
        ∧ s' = discover u v (s⦇pending := pending s - {(u,v)}⦈)"

  lemmas pre_on_defs = pre_on_new_root_def pre_on_finish_def 
    pre_edge_selected_def pre_on_cross_edge_def pre_on_back_edge_def
    pre_on_discover_def pre_is_break_def

  text ‹Next, we define a set of rules to establish an invariant.›  

  lemma establish_invarI[case_names init new_root finish cross_edge back_edge discover]:
    ― ‹Establish a DFS invariant (explicit preconditions).›
    assumes init: "on_init param ≤⇩n SPEC (λx. I (empty_state x))"
    assumes new_root: "⋀s s' v0. 
      ⟦DFS_invar G param s; I s; cond s; ¬ is_break param s;
       stack s = []; v0 ∈ V0; v0 ∉ dom (discovered s);
        s' = new_root v0 s⟧
         ⟹ on_new_root param v0 s' ≤⇩n 
             SPEC (λx. DFS_invar G param (s'⦇state.more := x⦈)
                         ⟶ I (s'⦇state.more := x⦈))"
    assumes finish: "⋀s s' u. 
      ⟦DFS_invar G param s; I s; cond s; ¬ is_break param s;
       stack s ≠ []; u = hd (stack s); 
       pending s `` {u} = {};
       s' = finish u s⟧
         ⟹ on_finish param u s' ≤⇩n 
              SPEC (λx. DFS_invar G param (s'⦇state.more := x⦈)
                        ⟶ I (s'⦇state.more := x⦈))"
    assumes cross_edge: "⋀s s' u v.
       ⟦DFS_invar G param s; I s; cond s; ¬ is_break param s;
        stack s ≠ []; (u, v) ∈ pending s; u = hd (stack s); 
        v ∈ dom (discovered s); v∈dom (finished s);
        s' = cross_edge u v (s⦇pending := pending s - {(u,v)}⦈)⟧
       ⟹ on_cross_edge param u v s' ≤⇩n
           SPEC (λx. DFS_invar G param (s'⦇state.more := x⦈)
                      ⟶ I (s'⦇state.more := x⦈))"
    assumes back_edge: "⋀s s' u v.
       ⟦DFS_invar G param s; I s; cond s; ¬ is_break param s;
        stack s ≠ []; (u, v) ∈ pending s; u = hd (stack s); 
        v ∈ dom (discovered s); v∉dom (finished s);
        s' = back_edge u v (s⦇pending := pending s - {(u,v)}⦈)⟧
       ⟹ on_back_edge param u v s' ≤⇩n
           SPEC (λx. DFS_invar G param (s'⦇state.more := x⦈) 
                      ⟶ I (s'⦇state.more := x⦈))"
    assumes discover: "⋀s s' u v.
       ⟦DFS_invar G param s; I s; cond s; ¬ is_break param s;
        stack s ≠ [];  (u, v) ∈ pending s; u = hd (stack s); 
        v ∉ dom (discovered s);
        s' = discover u v (s⦇pending := pending s - {(u,v)}⦈)⟧
       ⟹ on_discover param u v s' ≤⇩n
           SPEC (λx. DFS_invar G param (s'⦇state.more := x⦈)
                      ⟶ I (s'⦇state.more := x⦈))"
    shows "is_invar I"
    unfolding is_invar_def
  proof
    show "init ≤⇩n SPEC I"
      unfolding init_def
      by (refine_rcg refine_vcg) (simp add: init)
  next
    fix s
    assume "rwof init cond step s" and IC: "I s" "cond s"
    hence DI: "DFS_invar G param s" by unfold_locales
    then interpret DFS_invar G param s .

    from ‹cond s› have IB: "¬ is_break param s" by (simp add: cond_def)

    have B: "step s ≤⇩n SPEC (DFS_invar G param)"
      by rule (metis DFS_invar_step' DI ‹cond s›)

    note rule_assms = DI IC IB

    show "step s ≤⇩n SPEC I"
      apply (rule leof_use_spec_rule[OF B])
      unfolding step_def do_defs pred_defs get_pending_def get_new_root_def
      apply (refine_rcg refine_vcg)
      apply (simp_all)

      apply (blast intro: new_root[OF rule_assms])
      apply (blast intro: finish[OF rule_assms])
      apply (rule cross_edge[OF rule_assms], auto) []
      apply (rule back_edge[OF rule_assms], auto) []
      apply (rule discover[OF rule_assms], auto) []
      done
  qed

  lemma establish_invarI'[case_names init new_root finish cross_edge back_edge discover]:
    ― ‹Establish a DFS invariant (symbolic preconditions).›
    assumes init: "on_init param ≤⇩n SPEC (λx. I (empty_state x))"
    assumes new_root: "⋀s' v0. pre_on_new_root v0 s'
         ⟹ on_new_root param v0 s' ≤⇩n 
             SPEC (λx. DFS_invar G param (s'⦇state.more := x⦈)
                         ⟶ I (s'⦇state.more := x⦈))"
    assumes finish: "⋀s' u. pre_on_finish u s' 
         ⟹ on_finish param u s' ≤⇩n 
              SPEC (λx. DFS_invar G param (s'⦇state.more := x⦈)
                        ⟶ I (s'⦇state.more := x⦈))"
    assumes cross_edge: "⋀s' u v. pre_on_cross_edge u v s'
       ⟹ on_cross_edge param u v s' ≤⇩n
           SPEC (λx. DFS_invar G param (s'⦇state.more := x⦈)
                      ⟶ I (s'⦇state.more := x⦈))"
    assumes back_edge: "⋀s' u v. pre_on_back_edge u v s'
       ⟹ on_back_edge param u v s' ≤⇩n
           SPEC (λx. DFS_invar G param (s'⦇state.more := x⦈) 
                      ⟶ I (s'⦇state.more := x⦈))"
    assumes discover: "⋀s' u v. pre_on_discover u v s'
       ⟹ on_discover param u v s' ≤⇩n
           SPEC (λx. DFS_invar G param (s'⦇state.more := x⦈)
                      ⟶ I (s'⦇state.more := x⦈))"
    shows "is_invar I"
    apply (rule establish_invarI)
    using assms
    unfolding pre_on_defs
    apply -
    apply blast
    apply (rprems,blast)+
    done
  
  lemma establish_invarI_ND [case_names prereq init new_discover finish cross_edge back_edge]:
    ― ‹Establish a DFS invariant (new-root and discover cases are combined).›
    assumes prereq: "⋀u v s. on_discover param u v s = on_new_root param v s"
    assumes init: "on_init param ≤⇩n SPEC (λx. I (empty_state x))"
    assumes new_discover: "⋀s s' v. 
      ⟦DFS_invar G param s; I s; cond s; ¬ is_break param s;
       v ∉ dom (discovered s); 
       discovered s' = (discovered s)(v↦counter s); finished s' = finished s;
       counter s' = Suc (counter s); stack s' = v#stack s;
       back_edges s' = back_edges s; cross_edges s' = cross_edges s;
       tree_edges s' ⊇ tree_edges s;
       state.more s' = state.more s⟧
         ⟹ on_new_root param v s' ≤⇩n 
             SPEC (λx. DFS_invar G param (s'⦇state.more := x⦈)
                         ⟶ I (s'⦇state.more := x⦈))"
    assumes finish: "⋀s s' u. 
      ⟦DFS_invar G param s; I s; cond s; ¬ is_break param s;
       stack s ≠ []; u = hd (stack s); 
       pending s `` {u} = {};
       s' = finish u s⟧
         ⟹ on_finish param u s' ≤⇩n 
              SPEC (λx. DFS_invar G param (s'⦇state.more := x⦈)
                        ⟶ I (s'⦇state.more := x⦈))"
    assumes cross_edge: "⋀s s' u v.
       ⟦DFS_invar G param s; I s; cond s; ¬ is_break param s;
        stack s ≠ []; (u, v) ∈ pending s; u = hd (stack s); 
        v ∈ dom (discovered s); v∈dom (finished s);
        s' = cross_edge u v (s⦇pending := pending s - {(u,v)}⦈)⟧
       ⟹ on_cross_edge param u v s' ≤⇩n
           SPEC (λx. DFS_invar G param (s'⦇state.more := x⦈)
                      ⟶ I (s'⦇state.more := x⦈))"
    assumes back_edge: "⋀s s' u v.
       ⟦DFS_invar G param s; I s; cond s; ¬ is_break param s;
        stack s ≠ []; (u, v) ∈ pending s; u = hd (stack s); 
        v ∈ dom (discovered s); v∉dom (finished s);
        s' = back_edge u v (s⦇pending := pending s - {(u,v)}⦈)⟧
       ⟹ on_back_edge param u v s' ≤⇩n
           SPEC (λx. DFS_invar G param (s'⦇state.more := x⦈) 
                        ⟶ I (s'⦇state.more := x⦈))"
    shows "is_invar I"
  proof (induct rule: establish_invarI)
    case (new_root s) thus ?case by (auto intro!: new_discover)
  next
    case (discover s s' u v) hence
      "on_new_root param v s' ≤⇩n 
        SPEC (λx. DFS_invar G param (s'⦇state.more := x⦈)
                   ⟶ I (s'⦇state.more := x⦈))"
      by (auto intro!: new_discover)
    with prereq show ?case by simp
  qed fact+

  (* Variant of establish_invarI, where cross_edge and back_edge are combined *)
  lemma establish_invarI_CB [case_names prereq init new_root finish cross_back_edge discover]:
    ― ‹Establish a DFS invariant (cross and back edge cases are combined).›
    assumes prereq: "⋀u v s. on_back_edge param u v s = on_cross_edge param u v s"
    assumes init: "on_init param ≤⇩n SPEC (λx. I (empty_state x))"
    assumes new_root: "⋀s s' v0. 
      ⟦DFS_invar G param s; I s; cond s; ¬ is_break param s;
       stack s = []; v0 ∈ V0; v0 ∉ dom (discovered s);
        s' = new_root v0 s⟧
         ⟹ on_new_root param v0 s' ≤⇩n 
             SPEC (λx. DFS_invar G param (s'⦇state.more := x⦈)
                         ⟶ I (s'⦇state.more := x⦈))"
    assumes finish: "⋀s s' u. 
      ⟦DFS_invar G param s; I s; cond s; ¬ is_break param s;
       stack s ≠ []; u = hd (stack s); 
       pending s `` {u} = {};
       s' = finish u s⟧
         ⟹ on_finish param u s' ≤⇩n 
              SPEC (λx. DFS_invar G param (s'⦇state.more := x⦈)
                        ⟶ I (s'⦇state.more := x⦈))"
    assumes cross_back_edge: "⋀s s' u v.
       ⟦DFS_invar G param s; I s; cond s; ¬ is_break param s;
        stack s ≠ []; (u, v) ∈ pending s; u = hd (stack s); 
        v ∈ dom (discovered s);
        discovered s' = discovered s; finished s' = finished s;
        stack s' = stack s; tree_edges s' = tree_edges s; counter s' = counter s;
        pending s' = pending s - {(u,v)};
        cross_edges s' ∪ back_edges s' = cross_edges s ∪ back_edges s ∪ {(u,v)};
        state.more s' = state.more s ⟧
       ⟹ on_cross_edge param u v s' ≤⇩n
           SPEC (λx. DFS_invar G param (s'⦇state.more := x⦈)
                      ⟶ I (s'⦇state.more := x⦈))"
    assumes discover: "⋀s s' u v.
       ⟦DFS_invar G param s; I s; cond s; ¬ is_break param s;
        stack s ≠ [];  (u, v) ∈ pending s; u = hd (stack s); 
        v ∉ dom (discovered s);
        s' = discover u v (s⦇pending := pending s - {(u,v)}⦈)⟧
       ⟹ on_discover param u v s' ≤⇩n
           SPEC (λx. DFS_invar G param (s'⦇state.more := x⦈)
                      ⟶ I (s'⦇state.more := x⦈))"
    shows "is_invar I"
  proof (induct rule: establish_invarI)
    case cross_edge thus ?case by (auto intro!: cross_back_edge)
  next
    case (back_edge s s' u v) hence
      "on_cross_edge param u v s' ≤⇩n 
             SPEC (λx. DFS_invar G param (s'⦇state.more := x⦈)
                         ⟶ I (s'⦇state.more := x⦈))"
      by (auto intro!: cross_back_edge)
    with prereq show ?case by simp
  qed fact+

  (* Variant of establish_invarI, where cross_edge and back_edge, and discover and new_root are combined *)
  lemma establish_invarI_ND_CB [case_names prereq_ND prereq_CB init new_discover finish cross_back_edge]:
    ― ‹Establish a DFS invariant (new-root/discover and cross/back-edge cases are combined).›
    assumes prereq: 
        "⋀u v s. on_discover param u v s = on_new_root param v s"
        "⋀u v s. on_back_edge param u v s = on_cross_edge param u v s"
    assumes init: "on_init param ≤⇩n SPEC (λx. I (empty_state x))"
    assumes new_discover: "⋀s s' v. 
     ⟦DFS_invar G param s; I s; cond s; ¬ is_break param s;
      v ∉ dom (discovered s); 
      discovered s' = (discovered s)(v↦counter s); finished s' = finished s;
      counter s' = Suc (counter s); stack s' = v#stack s;
      back_edges s' = back_edges s; cross_edges s' = cross_edges s;
      tree_edges s' ⊇ tree_edges s;
      state.more s' = state.more s⟧
        ⟹ on_new_root param v s' ≤⇩n 
            SPEC (λx. DFS_invar G param (s'⦇state.more := x⦈)
                        ⟶ I (s'⦇state.more := x⦈))"
    assumes finish: "⋀s s' u. 
      ⟦DFS_invar G param s; I s; cond s; ¬ is_break param s;
       stack s ≠ []; u = hd (stack s); 
       pending s `` {u} = {};
       s' = finish u s⟧
         ⟹ on_finish param u s' ≤⇩n 
              SPEC (λx. DFS_invar G param (s'⦇state.more := x⦈)
                        ⟶ I (s'⦇state.more := x⦈))"
    assumes cross_back_edge: "⋀s s' u v.
       ⟦DFS_invar G param s; I s; cond s; ¬ is_break param s;
        stack s ≠ []; (u, v) ∈ pending s; u = hd (stack s); 
        v ∈ dom (discovered s);
        discovered s' = discovered s; finished s' = finished s;
        stack s' = stack s; tree_edges s' = tree_edges s; counter s' = counter s;
        pending s' = pending s - {(u,v)};
        cross_edges s' ∪ back_edges s' = cross_edges s ∪ back_edges s ∪ {(u,v)};
        state.more s' = state.more s ⟧
       ⟹ on_cross_edge param u v s' ≤⇩n
           SPEC (λx. DFS_invar G param (s'⦇state.more := x⦈)
                      ⟶ I (s'⦇state.more := x⦈))"
    shows "is_invar I"
  proof (induct rule: establish_invarI_ND)
    case cross_edge thus ?case by (auto intro!: cross_back_edge)
  next
    case (back_edge s s' u v) hence
      "on_cross_edge param u v s' ≤⇩n 
             SPEC (λx. DFS_invar G param (s'⦇state.more := x⦈)
                         ⟶ I (s'⦇state.more := x⦈))"
      by (auto intro!: cross_back_edge)
    with prereq show ?case by simp
  qed fact+


  lemma is_invarI_full [case_names init new_root finish cross_edge back_edge discover]:
    ― ‹Establish a DFS invariant not taking into account the parameterization.›
    assumes init: "⋀e. I (empty_state e)"
    assumes new_root: "⋀s s' v0 e. 
       ⟦I s; cond s; DFS_invar G param s; DFS_invar G param s';
        stack s = []; v0 ∉ dom (discovered s); v0 ∈ V0;
        s' = new_root v0 s⦇state.more := e⦈⟧ 
      ⟹ I s'"
    and finish: "⋀s s' u e. 
       ⟦I s; cond s; DFS_invar G param s; DFS_invar G param s';
        stack s ≠ []; pending s `` {u} = {};
        u = hd (stack s); s' = finish u s⦇state.more := e⦈⟧ 
       ⟹ I s'"
    and cross_edge: "⋀s s' u v e.
       ⟦I s; cond s; DFS_invar G param s; DFS_invar G param s';
        stack s ≠ []; v ∈ pending s `` {u}; v ∈ dom (discovered s); 
        v ∈ dom (finished s);
        u = hd (stack s); 
        s' = (cross_edge u v (s⦇pending := pending s - {(u,v)}⦈))⦇state.more := e⦈⟧
       ⟹ I s'"
    and back_edge: "⋀s s' u v e.
       ⟦I s; cond s; DFS_invar G param s; DFS_invar G param s';
        stack s ≠ []; v ∈ pending s `` {u}; v ∈ dom (discovered s); v ∉ dom (finished s); 
        u = hd (stack s); 
        s' = (back_edge u v (s⦇pending := pending s - {(u,v)}⦈))⦇state.more := e⦈⟧
       ⟹ I s'"
    and discover: "⋀s s' u v e.
       ⟦I s; cond s; DFS_invar G param s; DFS_invar G param s';
        stack s ≠ []; v ∈ pending s `` {u}; v ∉ dom (discovered s); 
        u = hd (stack s); 
        s' = (discover u v (s⦇pending := pending s - {(u,v)}⦈))⦇state.more := e⦈⟧
       ⟹ I s'"
  shows "is_invar I"
  apply (rule establish_invarI) 
  apply (blast intro: indep_invar_rules assms)+
  done

  lemma is_invarI [case_names init new_root finish visited discover]:
    ― ‹Establish a DFS invariant not taking into account the parameterization, cross/back-edges combined.›
    assumes init': "⋀e. I (empty_state e)"
    and new_root': "⋀s s' v0 e. 
       ⟦I s; cond s; DFS_invar G param s; DFS_invar G param s';
        stack s = []; v0 ∉ dom (discovered s); v0 ∈ V0;
        s' = new_root v0 s⦇state.more := e⦈⟧ 
      ⟹ I s'"
    and finish': "⋀s s' u e. 
       ⟦I s; cond s; DFS_invar G param s; DFS_invar G param s';
        stack s ≠ []; pending s `` {u} = {};
        u = hd (stack s); s' = finish u s⦇state.more := e⦈⟧ 
       ⟹ I s'"
    and visited': "⋀s s' u v e c b.
       ⟦I s; cond s; DFS_invar G param s; DFS_invar G param s';
        stack s ≠ []; v ∈ pending s `` {u}; v ∈ dom (discovered s);
        u = hd (stack s);
        cross_edges s ⊆ c; back_edges s ⊆ b;
        s' = s⦇ 
          pending := pending s - {(u,v)},
          state.more := e, 
          cross_edges := c, 
          back_edges := b⦈⟧
       ⟹ I s'"
    and discover': "⋀s s' u v e.
       ⟦I s; cond s;  DFS_invar G param s; DFS_invar G param s';
        stack s ≠ []; v ∈ pending s `` {u}; v ∉ dom (discovered s); 
        u = hd (stack s); 
        s' = (discover u v (s⦇pending := pending s - {(u,v)}⦈))⦇state.more := e⦈⟧
       ⟹ I s'"
    shows "is_invar I"
  proof (induct rule: is_invarI_full)
    case (cross_edge s s' u v e) thus ?case
      apply -
      apply (rule visited'[of s s' v u "insert (u,v) (cross_edges s)" "back_edges s" e])
      apply clarsimp_all
      done
  next
    case (back_edge s s' u v e) thus ?case
      apply -
      apply (rule visited'[of s s' v u "cross_edges s" "insert (u,v) (back_edges s)" e])
      apply clarsimp_all
      done
  qed fact+

end

subsection ‹Basic Invariants›
text ‹We establish some basic invariants›

context param_DFS begin
  (* Establish some invariants *)
  definition "basic_invar s ≡
    set (stack s) = dom (discovered s) - dom (finished s) ∧
    distinct (stack s) ∧
    (stack s ≠ [] ⟶ last (stack s) ∈ V0) ∧
    dom (finished s) ⊆ dom (discovered s) ∧
    Domain (pending s) ⊆ dom (discovered s) - dom (finished s) ∧
    pending s ⊆ E"

  lemma i_basic_invar: "is_invar basic_invar" 
    unfolding basic_invar_def[abs_def]
    apply (induction rule: is_invarI)
    apply (clarsimp_all simp: neq_Nil_conv last_tl)
    apply blast+
    done
end

context DFS_invar begin
  lemmas basic_invar = make_invar_thm[OF i_basic_invar]

  lemma pending_ssE: "pending s ⊆ E" 
    using basic_invar 
    by (auto simp: basic_invar_def)

  lemma pendingD:
    "(u,v)∈pending s ⟹ (u,v)∈E ∧ u∈dom (discovered s)"
    using basic_invar 
    by (auto simp: basic_invar_def)

  lemma stack_set_def:
    "set (stack s) = dom (discovered s) - dom (finished s)"
    using basic_invar
    by (simp add: basic_invar_def)

  lemma stack_discovered:
    "set (stack s) ⊆ dom (discovered s)"
    using stack_set_def
    by auto

  lemma stack_distinct:
    "distinct (stack s)"
    using basic_invar
    by (simp add: basic_invar_def)

  lemma last_stack_in_V0:
    "stack s ≠ [] ⟹ last (stack s) ∈ V0"
    using basic_invar
    by (simp add: basic_invar_def)

  lemma stack_not_finished:
    "x ∈ set (stack s) ⟹ x ∉ dom (finished s)"
    using stack_set_def
    by auto

  lemma discovered_not_stack_imp_finished:
    "x ∈ dom (discovered s) ⟹ x ∉ set (stack s) ⟹ x ∈ dom (finished s)"
    using stack_set_def
    by auto

  lemma finished_discovered:
    "dom (finished s) ⊆ dom (discovered s)"
    using basic_invar
    by (auto simp add: basic_invar_def)

  lemma finished_no_pending:
    "v ∈ dom (finished s) ⟹ pending s `` {v} = {}"
    using basic_invar
    by (auto simp add: basic_invar_def)

  lemma discovered_eq_finished_un_stack:
    "dom (discovered s) = dom (finished s) ∪ set (stack s)"
    using stack_set_def finished_discovered by auto


  lemma pending_on_stack:
    "(v,w) ∈ pending s ⟹ v ∈ set (stack s)"
    using basic_invar
    by (auto simp add: basic_invar_def)

  lemma empty_stack_imp_empty_pending:
    "stack s = [] ⟹ pending s = {}"
    using pending_on_stack
    by auto
end


context param_DFS begin

(* Establish some more invariants *)
  lemma i_discovered_reachable: 
    "is_invar (λs. dom (discovered s) ⊆ reachable)"
  proof (induct rule: is_invarI)
    case (discover s) then interpret i: DFS_invar where s=s by simp
    from discover show ?case 
      apply (clarsimp dest!: i.pendingD)
      by (metis contra_subsetD list.set_sel(1) rtrancl_image_advance i.stack_discovered)
  qed auto

  definition "discovered_closed s ≡
      E``dom (finished s) ⊆ dom (discovered s)
    ∧ (E - pending s) `` set (stack s) ⊆ dom (discovered s)"

  lemma i_discovered_closed: "is_invar discovered_closed"
  proof (induct rule: is_invarI)
    case (finish s s') 
    hence "(E - pending s) `` set (stack s) ⊆ dom (discovered s)" 
      by (simp add: discovered_closed_def)
    moreover from finish have "set (stack s') ⊆ set (stack s)" 
      by (auto simp add: neq_Nil_conv cond_def)
    ultimately have "(E - pending s') `` set (stack s') ⊆ dom (discovered s')"
      using finish
      by simp blast

    moreover
    from ‹stack s ≠ []› finish have "E``dom (finished s') ⊆ dom (discovered s')" 
      apply (cases "stack s") apply simp
      apply (simp add: discovered_closed_def) 
      apply (blast)
      done
    ultimately show ?case by (simp add: discovered_closed_def)
  qed (auto simp add: discovered_closed_def cond_def)

  lemma i_discovered_finite: "is_invar (λs. finite (dom (discovered s)))"
    by (induction rule: is_invarI) auto

end

context DFS_invar
begin

  lemmas discovered_reachable = 
    i_discovered_reachable [THEN make_invar_thm]

  lemma stack_reachable: "set (stack s) ⊆ reachable" 
    using stack_discovered discovered_reachable by blast

  lemmas discovered_closed = i_discovered_closed[THEN make_invar_thm]

  lemmas discovered_finite[simp, intro!] = i_discovered_finite[THEN make_invar_thm]
  lemma finished_finite[simp, intro!]: "finite (dom (finished s))"
    using finished_discovered discovered_finite by (rule finite_subset)

  lemma finished_closed:
    "E `` dom (finished s) ⊆ dom (discovered s)"
    using discovered_closed[unfolded discovered_closed_def]
    by auto

  lemma finished_imp_succ_discovered:
    "v ∈ dom (finished s) ⟹ w ∈ succ v ⟹ w ∈ dom (discovered s)"
    using discovered_closed[unfolded discovered_closed_def]
    by auto

  lemma pending_reachable: "pending s ⊆ reachable × reachable" 
    using pendingD discovered_reachable
    by (fast intro: rtrancl_image_advance_rtrancl)

  lemma pending_finite[simp, intro!]: "finite (pending s)"
  proof -
    have "pending s ⊆ (SIGMA u:dom (discovered s). E``{u})"
      by (auto dest: pendingD)
    also have "finite …"
      apply rule
      apply (rule discovered_finite)
      using discovered_reachable
      by (blast intro: finitely_branching)
    finally (finite_subset) show ?thesis .
  qed

  lemma no_pending_imp_succ_discovered:
    assumes "u ∈ dom (discovered s)"
    and "pending s `` {u} = {}"
    and "v ∈ succ u"
    shows "v ∈ dom (discovered s)"
  proof (cases "u ∈ dom (finished s)")
    case True with finished_imp_succ_discovered assms show ?thesis by simp
  next
    case False with stack_set_def assms have "u ∈ set (stack s)" by auto
    with assms discovered_closed[unfolded discovered_closed_def] show ?thesis by blast
  qed

  lemma nc_finished_eq_reachable:
    assumes NC: "¬cond s" "¬is_break param s" 
    shows "dom (finished s) = reachable"
  proof -
    from NC basic_invar 
    have [simp]: "stack s = []" "dom (discovered s) = dom (finished s)" and SS: "V0 ⊆ dom (discovered s)"
      unfolding basic_invar_def cond_alt by auto

    show "dom (finished s) = reachable"
    proof 
      from discovered_reachable show "dom (finished s) ⊆ reachable"
        by simp
    next
      from discovered_closed have "E``(dom (finished s)) ⊆ dom (finished s)"
        unfolding discovered_closed_def by auto
      with SS show "reachable ⊆ dom (finished s)"
        by (simp, metis rtrancl_reachable_induct)
    qed
  qed

  lemma nc_V0_finished:
    assumes NC: "¬ cond s" "¬ is_break param s"
    shows "V0 ⊆ dom (finished s)"
    using nc_finished_eq_reachable[OF NC]
    by blast 

  lemma nc_discovered_eq_finished:
    assumes NC: "¬ cond s" "¬ is_break param s"
    shows "dom (discovered s) = dom (finished s)"
    using finished_discovered
    using nc_finished_eq_reachable[OF NC] discovered_reachable
    by blast

  lemma nc_discovered_eq_reachable:
    assumes NC: "¬ cond s" "¬ is_break param s"
    shows "dom (discovered s) = reachable"
    using NC
    using nc_discovered_eq_finished nc_finished_eq_reachable
    by blast

  lemma nc_fin_closed: 
    assumes NC: "¬cond s"
    assumes NB: "¬is_break param s"
    shows "E``dom (finished s) ⊆ dom (finished s)"
    using finished_imp_succ_discovered
    by (auto simp: nc_discovered_eq_finished[OF NC NB])

end

subsection ‹Total Correctness›
text ‹We can show termination of the DFS algorithm, independently of the parameterization›

context param_DFS begin
  definition "param_dfs_variant ≡ inv_image 
    (finite_psupset reachable <*lex*> finite_psubset <*lex*> less_than)
    (λs. (dom (discovered s), pending s, length (stack s)))"

  lemma param_dfs_variant_wf[simp, intro!]:
    assumes [simp, intro!]: "finite reachable"
    shows "wf param_dfs_variant"  
    unfolding param_dfs_variant_def
    by auto

  lemma param_dfs_variant_step:   
    assumes A: "DFS_invar G param s" "cond s" "nofail it_dfs"
    shows "step s ≤ SPEC (λs'. (s',s)∈param_dfs_variant)"
  proof -
    interpret DFS_invar G param s by fact

    from A show ?thesis
      unfolding rwof_eq_DFS_invar[symmetric] it_dfs_def
      apply -
      apply (drule (2) WHILE_nofail_imp_rwof_nofail)
      unfolding step_def get_new_root_def do_defs get_pending_def
      unfolding param_dfs_variant_def
      apply refine_vcg
      using discovered_reachable (* TODO: Clean, up. *) 
        (* FIXME: auto-steps take loooong *)
      apply (auto 
        split: option.splits 
        simp: refine_pw_simps pw_le_iff is_discovered_def finite_psupset_def
      ) [1]
      apply (auto simp: refine_pw_simps pw_le_iff is_empty_stack_def) []
      apply simp_all

      apply (auto 
        simp: refine_pw_simps pw_le_iff is_discovered_def
        split: if_split_asm
        ) [2]

      apply (clarsimp simp: refine_pw_simps pw_le_iff is_discovered_def)
      using discovered_reachable pending_reachable
      apply (auto
        simp: is_discovered_def
        simp: refine_pw_simps pw_le_iff finite_psupset_def
        split: if_split_asm)
      done
  qed

  
end


context param_DFS begin
  lemma it_dfsT_eq_it_dfs:
    assumes [simp, intro!]: "finite reachable"
    shows "it_dfsT = it_dfs"
  proof -
    have "it_dfs ≤ it_dfsT" 
      unfolding it_dfs_def it_dfsT_def WHILE_def WHILET_def
      apply (rule bind_mono)
      apply simp
      apply (rule WHILEI_le_WHILEIT)
      done
    also have "it_dfsT ≤ it_dfs"
    proof (cases "nofail it_dfs")
      case False thus ?thesis by (simp add: not_nofail_iff)
    next
      case True

      show ?thesis
        unfolding it_dfsT_def it_dfs_def
        apply (rule bind_mono)
        apply simp
        apply (subst WHILET_eq_WHILE_tproof[
          where I="DFS_invar G param"
          and V="param_dfs_variant"
          ])
        apply auto []

        apply (subst rwof_eq_DFS_invar[symmetric])
        using rwof_init[OF True[unfolded it_dfs_def]]
        apply (fastforce dest: order_trans) []
        
        apply (rule SPEC_rule_conjI)
          apply (rule DFS_invar_step[OF True], assumption+) []
          apply (rule param_dfs_variant_step, (assumption|rule True)+) []
        
        apply simp
        done
    qed
    finally show ?thesis by simp
  qed
end

subsection ‹Non-Failing Parameterization›
text ‹
  The proofs so far have been done modulo failure of the parameterization.
  In this locale, we assume that the parameterization does not fail,
  and derive the correctness proof of the DFS algorithm wrt. its invariant.
›
(* Locale that assumes that parameterization does not fail *)
locale DFS =
  param_DFS G param
  for G :: "('v, 'more) graph_rec_scheme"
  and param :: "('v,'es) parameterization"
  +
  assumes nofail_on_init: 
    "nofail (on_init param)"

  assumes nofail_on_new_root:
    "pre_on_new_root v0 s ⟹ nofail (on_new_root param v0 s)"

  assumes nofail_on_finish: 
    "pre_on_finish u s ⟹ nofail (on_finish param u s)"

  assumes nofail_on_cross_edge: 
    "pre_on_cross_edge u v s ⟹ nofail (on_cross_edge param u v s)"

  assumes nofail_on_back_edge: 
    "pre_on_back_edge u v s ⟹ nofail (on_back_edge param u v s)"

  assumes nofail_on_discover: 
    "pre_on_discover u v s ⟹ nofail (on_discover param u v s)"

begin
  lemmas nofails = nofail_on_init nofail_on_new_root nofail_on_finish 
    nofail_on_cross_edge nofail_on_back_edge nofail_on_discover


  lemma init_leof_invar: "init ≤⇩n SPEC (DFS_invar G param)"
    unfolding rwof_eq_DFS_invar[symmetric]
    by (rule rwof_leof_init)

  lemma it_dfs_eq_spec: "it_dfs = SPEC (λs. DFS_invar G param s ∧ ¬cond s)"
    unfolding rwof_eq_DFS_invar[symmetric] it_dfs_def
    apply (rule nofail_WHILE_eq_rwof)
    apply (subst WHILE_eq_I_rwof)
    unfolding rwof_eq_DFS_invar
    apply (rule SPEC_nofail[where Φ="λ_. True"])
    apply (refine_vcg leofD[OF _ init_leof_invar, THEN weaken_SPEC])
    apply (simp add: init_def refine_pw_simps nofail_on_init)
    apply (rule DFS_invar_step')
    apply (simp add: step_def refine_pw_simps nofail_on_init do_defs 
      get_pending_def get_new_root_def pred_defs
      split: option.split)
    apply (intro allI conjI impI nofails)
    apply (auto simp add: pre_on_defs)
    done

  lemma it_dfs_correct: "it_dfs ≤ SPEC (λs. DFS_invar G param s ∧ ¬cond s)"
    by (simp add: it_dfs_eq_spec)

  lemma it_dfs_SPEC:
    assumes "⋀s. ⟦DFS_invar G param s; ¬cond s⟧ ⟹ P s"
    shows "it_dfs ≤ SPEC P"
    using weaken_SPEC[OF it_dfs_correct]
    using assms
    by blast

  lemma it_dfsT_correct: 
    assumes "finite reachable"
    shows "it_dfsT ≤ SPEC (λs. DFS_invar G param s ∧ ¬cond s)"
    apply (subst it_dfsT_eq_it_dfs[OF assms])
    by (rule it_dfs_correct)

  lemma it_dfsT_SPEC:
    assumes "finite reachable"
    assumes "⋀s. ⟦DFS_invar G param s; ¬cond s⟧ ⟹ P s"
    shows "it_dfsT ≤ SPEC P"
    apply (subst it_dfsT_eq_it_dfs[OF assms(1)])
    using assms(2)
    by (rule it_dfs_SPEC)

end

end