Theory Nested_DFS

section ‹\isaheader{Nested DFS (HPY improvement)}›
theory Nested_DFS
imports 
  Collections.Refine_Dflt
  Succ_Graph
  Collections.Code_Target_ICF
  CAVA_Automata.Digraph_Basic
begin

text ‹
  Implementation of a nested DFS algorithm for accepting cycle detection
  using the refinement framework. The algorithm uses the improvement of 
  [HPY96], i.e., it reports a cycle if the inner DFS finds a path back to 
  the stack of the outer DFS.

  The algorithm returns a witness in case that an accepting cycle is detected.
›

subsection "Tools for DFS Algorithms"

subsubsection "Invariants"
definition "gen_dfs_pre E U S V u0 
  E``U  U   ― ‹Upper bound is closed under transitions›
   finite U ― ‹Upper bound is finite›
   V  U    ― ‹Visited set below upper bound›
   u0  U   ― ‹Start node in upper bound›
   E``(V-S)  V ― ‹Visited nodes closed under reachability, or on stack›
   u0V     ― ‹Start node not yet visited›
   S  V    ― ‹Stack is visited›
   (vS. (v,u0)(ES×UNIV)*) ― ‹u0› reachable from stack, only over stack›
  "

definition "gen_dfs_var U  finite_psupset U"

definition "gen_dfs_fe_inv E U S V0 u0 it V brk  
  (¬brk  E``(V-S)  V)  ― ‹Visited set closed under reachability›
   E``{u0} - it  V     ― ‹Successors of u0› visited›
   V0  V               ― ‹Visited set increasing›
   V  V0  (E - UNIV×S)* `` (E``{u0} - it - S) ― ‹All visited nodes reachable›
"

definition "gen_dfs_post E U S V0 u0 V brk  
  (¬brk  E``(V-S)  V) ― ‹Visited set closed under reachability›
   u0  V               ― ‹u0› visited›
   V0  V               ― ‹Visited set increasing›
   V  V0  (E - UNIV×S)* `` {u0} ― ‹All visited nodes reachable›
"

subsubsection "Invariant Preservation"
lemma gen_dfs_pre_initial: 
  assumes "finite (E*``{v0})"
  assumes "v0U"
  shows "gen_dfs_pre E (E*``{v0}) {} {} v0"
  using assms unfolding gen_dfs_pre_def 
  apply auto
  done

lemma gen_dfs_pre_imp_wf:
  assumes "gen_dfs_pre E U S V u0"
  shows "wf (gen_dfs_var U)"
  using assms unfolding gen_dfs_pre_def gen_dfs_var_def by auto

lemma gen_dfs_pre_imp_fin:
  assumes "gen_dfs_pre E U S V u0"
  shows "finite (E `` {u0})"
  apply (rule finite_subset[where B="U"])
  using assms unfolding gen_dfs_pre_def
  by auto

text ‹Inserted u0› on stack and to visited set›
lemma gen_dfs_pre_imp_fe:
  assumes "gen_dfs_pre E U S V u0"
  shows "gen_dfs_fe_inv E U (insert u0 S) (insert u0 V) u0 
    (E``{u0}) (insert u0 V) False"
  using assms unfolding gen_dfs_pre_def gen_dfs_fe_inv_def
  apply auto
  done

lemma gen_dfs_fe_inv_pres_visited:
  assumes "gen_dfs_pre E U S V u0"
  assumes "gen_dfs_fe_inv E U (insert u0 S) (insert u0 V) u0 it V' False"
  assumes "tit" "itE``{u0}" "tV'"
  shows "gen_dfs_fe_inv E U (insert u0 S) (insert u0 V) u0 (it-{t}) V' False"
  using assms unfolding gen_dfs_fe_inv_def
  apply auto
  done

lemma gen_dfs_upper_aux:
  assumes "(x,y)E'*"
  assumes "(u0,x)E"
  assumes "u0U"
  assumes "E'E"
  assumes "E``U  U"
  shows "yU"
  using assms
  by induct auto


lemma gen_dfs_fe_inv_imp_var:
  assumes "gen_dfs_pre E U S V u0"
  assumes "gen_dfs_fe_inv E U (insert u0 S) (insert u0 V) u0 it V' False"
  assumes "tit" "itE``{u0}" "tV'"
  shows "(V',V)  gen_dfs_var U"
  using assms unfolding gen_dfs_fe_inv_def gen_dfs_pre_def gen_dfs_var_def
  apply (clarsimp simp add: finite_psupset_def)
  apply (blast dest: gen_dfs_upper_aux)
  done

lemma gen_dfs_fe_inv_imp_pre:
  assumes "gen_dfs_pre E U S V u0"
  assumes "gen_dfs_fe_inv E U (insert u0 S) (insert u0 V) u0 it V' False"
  assumes "tit" "itE``{u0}" "tV'"
  shows "gen_dfs_pre E U (insert u0 S) V' t"
  using assms unfolding gen_dfs_fe_inv_def gen_dfs_pre_def
  apply clarsimp
  apply (intro conjI)
  apply (blast dest: gen_dfs_upper_aux)
  apply blast
  apply blast
  apply blast
  apply clarsimp
  apply (rule rtrancl_into_rtrancl[where b=u0])
  apply (auto intro: rev_subsetD[OF _ rtrancl_mono[where r="E  S × UNIV"]]) []
  apply blast
  done

lemma gen_dfs_post_imp_fe_inv:
  assumes "gen_dfs_pre E U S V u0"
  assumes "gen_dfs_fe_inv E U (insert u0 S) (insert u0 V) u0 it V' False"
  assumes "tit" "itE``{u0}" "tV'"
  assumes "gen_dfs_post E U (insert u0 S) V' t V'' cyc"
  shows "gen_dfs_fe_inv E U (insert u0 S) (insert u0 V) u0 (it-{t}) V'' cyc"
  using assms unfolding gen_dfs_fe_inv_def gen_dfs_post_def gen_dfs_pre_def
  apply clarsimp
  apply (intro conjI)
  apply blast
  apply blast
  apply blast
  apply (erule order_trans)
  apply simp
  apply (rule conjI)
    apply (erule order_trans[
      where y="insert u0 (V  (E - UNIV × insert u0 S)* 
        `` (E `` {u0} - it - insert u0 S))"])
    apply blast

    apply (cases cyc)
      apply simp
      apply blast

      apply simp
      apply blast
  done

lemma gen_dfs_post_aux:
  assumes 1: "(u0,x)E"
  assumes 2: "(x,y)(E - UNIV × insert u0 S)*"
  assumes 3: "SV" "xV"
  shows "(u0, y)  (E - UNIV × S)*"
proof -
  from 1 3 have "(u0,x)(E - UNIV × S)" by blast
  also have "(x,y)(E - UNIV × S)*"
    apply (rule_tac rev_subsetD[OF 2 rtrancl_mono])
    by auto
  finally show ?thesis .
qed

lemma gen_dfs_fe_imp_post_brk:
  assumes "gen_dfs_pre E U S V u0"
  assumes "gen_dfs_fe_inv E U (insert u0 S) (insert u0 V) u0 it V' True"
  assumes "itE``{u0}"
  shows "gen_dfs_post E U S V u0 V' True"
  using assms unfolding gen_dfs_pre_def gen_dfs_fe_inv_def gen_dfs_post_def
  apply clarify
  apply (intro conjI)
  apply simp
  apply simp
  apply simp
  apply clarsimp
  apply (blast intro: gen_dfs_post_aux)
  done


lemma gen_dfs_fe_inv_imp_post:
  assumes "gen_dfs_pre E U S V u0"
  assumes "gen_dfs_fe_inv E U (insert u0 S) (insert u0 V) u0 {} V' cyc"
  assumes "cyccyc'"
  shows "gen_dfs_post E U S V u0 V' cyc'"
  using assms unfolding gen_dfs_pre_def gen_dfs_fe_inv_def gen_dfs_post_def
  apply clarsimp
  apply (intro conjI)
  apply blast
  apply (auto intro: gen_dfs_post_aux) []
  done

lemma gen_dfs_pre_imp_post_brk:
  assumes "gen_dfs_pre E U S V u0"
  shows "gen_dfs_post E U S V u0 (insert u0 V) True"
  using assms unfolding gen_dfs_pre_def gen_dfs_post_def
  apply auto
  done

subsubsection "Consequences of Postcondition"
lemma gen_dfs_post_imp_reachable: 
  assumes "gen_dfs_pre E U S V0 u0"
  assumes "gen_dfs_post E U S V0 u0 V brk"
  shows "V  V0  E*``{u0}"
  using assms unfolding gen_dfs_post_def gen_dfs_pre_def
  apply clarsimp
  apply (blast intro: rev_subsetD[OF _ rtrancl_mono])
  done

lemma gen_dfs_post_imp_complete:
  assumes "gen_dfs_pre E U {} V0 u0"
  assumes "gen_dfs_post E U {} V0 u0 V False"
  shows "V0  E*``{u0}  V"
  using assms unfolding gen_dfs_post_def gen_dfs_pre_def
  apply clarsimp
  apply (blast dest: Image_closed_trancl)
  done

lemma gen_dfs_post_imp_eq:
  assumes "gen_dfs_pre E U {} V0 u0"
  assumes "gen_dfs_post E U {} V0 u0 V False"
  shows "V = V0  E*``{u0}"
  using gen_dfs_post_imp_reachable[OF assms] gen_dfs_post_imp_complete[OF assms]
  by blast

lemma gen_dfs_post_imp_below_U:
  assumes "gen_dfs_pre E U S V0 u0"
  assumes "gen_dfs_post E U S V0 u0 V False"
  shows "V  U"
  using assms unfolding gen_dfs_pre_def gen_dfs_post_def
  apply clarsimp
  apply (blast intro: rev_subsetD[OF _ rtrancl_mono] dest: Image_closed_trancl)
  done

subsection "Abstract Algorithm"

subsubsection ‹Inner (red) DFS›

text ‹A witness of the red algorithm is a node on the stack and a path
  to this node›
type_synonym 'v red_witness = "('v list × 'v) option"
text ‹Prepend node to red witness›
fun prep_wit_red :: "'v  'v red_witness  'v red_witness" where
  "prep_wit_red v None = None"
| "prep_wit_red v (Some (p,u)) = Some (v#p,u)"

text ‹
  Initial witness for node u› with onstack successor v›
definition red_init_witness :: "'v  'v  'v red_witness" where
  "red_init_witness u v = Some ([u],v)"

definition red_dfs where
  "red_dfs E onstack V u  
    RECT (λD (V,u). do {
      let V=insert u V;

      ― ‹Check whether we have a successor on stack›
      brk  FOREACHC (E``{u}) (λbrk. brk=None) 
        (λt _. if tonstack then RETURN (red_init_witness u t) else RETURN None)
        None;

      ― ‹Recurse for successors›
      case brk of
        None 
          FOREACHC (E``{u}) (λ(V,brk). brk=None)
            (λt (V,_). 
              if tV then do {
                (V,brk)  D (V,t);
                RETURN (V,prep_wit_red u brk)
              } else RETURN (V,None))
            (V,None)
      | _  RETURN (V,brk)
    }) (V,u)
  "

text ‹
  A witness of the blue DFS may be in two different phases, the REACH›
  phase is before the node on the stack has actually been popped, and the
  CIRC› phase is after the node on the stack has been popped.

  REACH v p u p'›: \begin{description}
  \item[v›] accepting node 
  \item[p›] path from v› to u›
  \item[u›] node on stack
  \item[p'›] path from current node to v›
  \end{description}

  CIRC v pc pr›: \begin{description}
  \item[v›] accepting node 
  \item[pc›] path from v› to v›
  \item[pr›] path from current node to v›
  \end{description}
›
datatype 'v blue_witness = 
  NO_CYC
| REACH "'v" "'v list" "'v" "'v list"
| CIRC "'v" "'v list" "'v list"

text ‹Prepend node to witness›
primrec prep_wit_blue :: "'v  'v blue_witness  'v blue_witness" where
  "prep_wit_blue u0 NO_CYC = NO_CYC"
| "prep_wit_blue u0 (REACH v p u p') = (
  if u0=u then
    CIRC v (p@u#p') (u0#p')
  else
    REACH v p u (u0#p')
  )"
| "prep_wit_blue u0 (CIRC v pc pr) = CIRC v pc (u0#pr)"

text ‹Initialize blue witness›
fun init_wit_blue :: "'v  'v red_witness  'v blue_witness" where
  "init_wit_blue u0 None = NO_CYC"
| "init_wit_blue u0 (Some (p,u)) = (
  if u=u0 then
    CIRC u0 p []
  else REACH u0 p u [])"

text ‹Extract result from witness›
definition "extract_res cyc 
   (case cyc of CIRC v pc pr  Some (v,pc,pr) | _  None)"

subsubsection ‹Outer (Blue) DFS›
definition blue_dfs 
  :: "('a×'a) set  'a set  'a  ('a×'a list×'a list) option nres" 
  where
  "blue_dfs E A s  do {
    (_,_,_,cyc)  RECT (λD (blues,reds,onstack,s). do {
      let blues=insert s blues;
      let onstack=insert s onstack;
      (blues,reds,onstack,cyc)  
      FOREACHC (E``{s}) (λ(_,_,_,cyc). cyc=NO_CYC) 
        (λt (blues,reds,onstack,cyc). 
          if tblues then do {
            (blues,reds,onstack,cyc)  D (blues,reds,onstack,t);
            RETURN (blues,reds,onstack,(prep_wit_blue s cyc))
          } else RETURN (blues,reds,onstack,cyc))
        (blues,reds,onstack,NO_CYC);

      (reds,cyc)  
      if cyc=NO_CYC  sA then do {
        (reds,rcyc)  red_dfs E onstack reds s;
        RETURN (reds, init_wit_blue s rcyc)
      } else RETURN (reds,cyc);

      let onstack=onstack - {s};
      RETURN (blues,reds,onstack,cyc)
    }) ({},{},{},s);
    RETURN (extract_res cyc)
  }
  "


subsection "Correctness"

subsubsection "Specification"

text ‹Specification of a reachable accepting cycle:›
definition "has_acc_cycle E A v0  vA. (v0,v)E*  (v,v)E+"

text ‹Specification of witness for accepting cycle›
definition "is_acc_cycle E A v0 v r c 
   vA  path E v0 r v  path E v c v  c[]"

text ‹Specification is compatible with existence of accepting cycle›
lemma is_acc_cycle_eq:
  "has_acc_cycle E A v0  (v r c. is_acc_cycle E A v0 v r c)"
  unfolding has_acc_cycle_def is_acc_cycle_def
  by (auto elim!: rtrancl_is_path trancl_is_path
    intro: path_is_rtrancl path_is_trancl) 

subsubsection "Correctness Proofs"

text ‹Additional invariant to be maintained between calls of red dfs›
definition "red_dfs_inv E U reds onstack  
  E``U  U           ― ‹Upper bound is closed under transitions›
   finite U         ― ‹Upper bound is finite›
   reds  U         ― ‹Red set below upper bound›
   E``reds  reds   ― ‹Red nodes closed under reachability›
   E``reds  onstack = {} ― ‹No red node with edge to stack›
"

lemma red_dfs_inv_initial:
  assumes "finite (E*``{v0})"
  shows "red_dfs_inv E (E*``{v0}) {} {}"
  using assms unfolding red_dfs_inv_def
  apply auto
  done

text ‹Correctness of the red DFS.›
theorem red_dfs_correct:
  fixes v0 u0 :: 'v
  assumes PRE: 
    "red_dfs_inv E U reds onstack"
    "u0U"
    "u0reds"
  shows "red_dfs E onstack reds u0 
     SPEC (λ(reds',cyc). case cyc of
      Some (p,v)  vonstack  p[]  path E u0 p v
    | None  
        red_dfs_inv E U reds' onstack 
         u0reds' 
         reds'  reds  E* `` {u0}
  )"
proof -
  let ?dfs_red = "
    RECT (λD (V,u). do {
      let V=insert u V;

      ― ‹Check whether we have a successor on stack›
      brk  FOREACHC (E``{u}) (λbrk. brk=None) 
        (λt _. if tonstack then 
            RETURN (red_init_witness u t) 
          else RETURN None) 
        None;

      ― ‹Recurse for successors›
      case brk of
        None 
          FOREACHC (E``{u}) (λ(V,brk). brk=None)
            (λt (V,_). 
              if tV then do {
                (V,brk)  D (V,t);
                RETURN (V,prep_wit_red u brk)
              } else RETURN (V,None))
            (V,None)
      | _  RETURN (V,brk)
    }) (V,u)
"
  let "RECT ?body ?init" = "?dfs_red"

  define pre where "pre = (λS (V,u0). gen_dfs_pre E U S V u0  E``V  onstack = {})"
  define post where "post = (λS (V0,u0) (V,cyc). gen_dfs_post E U S V0 u0 V (cycNone)
     (case cyc of None  E``V  onstack = {}
      | Some (p,v)  vonstack  p[]  path E u0 p v))
    "

  define fe_inv where "fe_inv = (λS V0 u0 it (V,cyc). 
    gen_dfs_fe_inv E U S V0 u0 it V (cycNone)
     (case cyc of None  E``V  onstack = {}
      | Some (p,v)  vonstack  p[]  path E u0 p v))
    "


  from PRE have GENPRE: "gen_dfs_pre E U {} reds u0"
    unfolding red_dfs_inv_def gen_dfs_pre_def
    by auto
  with PRE have PRE': "pre {} (reds,u0)"
    unfolding pre_def red_dfs_inv_def
    by auto

  have IMP_POST: "SPEC (post {} (reds,u0)) 
     SPEC (λ(reds',cyc). case cyc of
      Some (p,v)  vonstack  p[]  path E u0 p v
    | None  
        red_dfs_inv E U reds' onstack 
         u0reds' 
         reds'  reds  E* `` {u0})"
    apply (clarsimp split: option.split)
    apply (intro impI conjI allI)
    apply simp_all
  proof -
    fix reds' p v
    assume "post {} (reds,u0) (reds',Some (p,v))"
    thus "vonstack" and "p[]" and "path E u0 p v"
      unfolding post_def by auto
  next
    fix reds'
    assume "post {} (reds, u0) (reds', None)"
    hence GPOST: "gen_dfs_post E U {} reds u0 reds' False"
      and NS: "E``reds'  onstack = {}"
      unfolding post_def by auto

    from GPOST show "u0reds'" unfolding gen_dfs_post_def by auto

    show "red_dfs_inv E U reds' onstack"
      unfolding red_dfs_inv_def
      apply (intro conjI)
      using GENPRE[unfolded gen_dfs_pre_def]
      apply (simp_all) [2]
      apply (rule gen_dfs_post_imp_below_U[OF GENPRE GPOST])
      using GPOST[unfolded gen_dfs_post_def] apply simp
      apply fact
      done

    from GPOST show "reds'  reds  E* `` {u0}" 
      unfolding gen_dfs_post_def by auto
  qed

  {
    fix σ S
    assume INV0: "pre S σ"
    have "RECT ?body σ
       SPEC (post S σ)"

      apply (rule RECT_rule_arb[where 
        pre="pre" and
        V="gen_dfs_var U <*lex*> {}" and
        arb="S"
        ])

      apply refine_mono

      using INV0[unfolded pre_def] apply (auto intro: gen_dfs_pre_imp_wf) []
      
      apply fact

      apply (rename_tac D S u)
      apply (intro refine_vcg)

      ― ‹First foreach loop, checking for onstack-successor›
      apply (rule_tac I="λit cyc. 
        (case cyc of None  (E``{b} - it)  onstack = {}
          | Some (p,v)  (vonstack  p[]  path E b p v))" 
        in FOREACHc_rule)
      apply (auto simp add: pre_def gen_dfs_pre_imp_fin) []
      apply auto []
      apply (auto 
        split: option.split 
        simp: red_init_witness_def intro: path1) []

      apply (intro refine_vcg)

      ― ‹Second foreach loop, iterating over sucessors›
      apply (rule_tac I="fe_inv (insert b S) (insert b a) b" in
        FOREACHc_rule
      )
      apply (auto simp add: pre_def gen_dfs_pre_imp_fin) []

      apply (auto simp add: pre_def fe_inv_def gen_dfs_pre_imp_fe) []

      apply (intro refine_vcg)

      ― ‹Recursive call›
      apply (rule order_trans)
      apply (rprems)
      apply (clarsimp simp add: pre_def fe_inv_def)
      apply (rule gen_dfs_fe_inv_imp_pre, assumption+) []
      apply (auto simp add: pre_def fe_inv_def intro: gen_dfs_fe_inv_imp_var) []

      apply (clarsimp simp add: pre_def post_def fe_inv_def
        split: option.split_asm prod.split_asm
        ) []
        apply (blast intro: gen_dfs_post_imp_fe_inv)
        apply (blast intro: gen_dfs_post_imp_fe_inv path_prepend)

      apply (auto simp add: pre_def post_def fe_inv_def 
        intro: gen_dfs_fe_inv_pres_visited) []

      apply (auto simp add: pre_def post_def fe_inv_def
        intro: gen_dfs_fe_inv_imp_post) []

      apply (auto simp add: pre_def post_def fe_inv_def
        intro: gen_dfs_fe_imp_post_brk) []

      apply (auto simp add: pre_def post_def fe_inv_def
        intro: gen_dfs_pre_imp_post_brk) []

      apply (auto simp add: pre_def post_def fe_inv_def
        intro: gen_dfs_pre_imp_post_brk) []

      done
  } note GEN=this

  note GEN[OF PRE']
  also note IMP_POST
  finally show ?thesis
    unfolding red_dfs_def .
qed

text ‹Main theorem: Correctness of the blue DFS›
theorem blue_dfs_correct:
  fixes v0 :: 'v
  assumes FIN[simp,intro!]: "finite (E*``{v0})"
  shows "blue_dfs E A v0  SPEC (λr. 
    case r of None  ¬has_acc_cycle E A v0
  | Some (v,pc,pv)  is_acc_cycle E A v0 v pv pc)"
proof -
  let ?ndfs = "
  do {
    (_,_,_,cyc)  RECT (λD (blues,reds,onstack,s). do {
      let blues=insert s blues;
      let onstack=insert s onstack;
      (blues,reds,onstack,cyc)  
      FOREACHC (E``{s}) (λ(_,_,_,cyc). cyc=NO_CYC) 
        (λt (blues,reds,onstack,cyc). 
          if tblues then do {
            (blues,reds,onstack,cyc)  D (blues,reds,onstack,t);
            RETURN (blues,reds,onstack,(prep_wit_blue s cyc))
          } else RETURN (blues,reds,onstack,cyc))
        (blues,reds,onstack,NO_CYC);

      (reds,cyc)  
      if cyc=NO_CYC  sA then do {
        (reds,rcyc)  red_dfs E onstack reds s;
        RETURN (reds, init_wit_blue s rcyc)
      } else RETURN (reds,cyc);

      let onstack=onstack - {s};
      RETURN (blues,reds,onstack,cyc)
    }) ({},{},{},s);
    RETURN (case cyc of NO_CYC  None | CIRC v pc pr  Some (v,pc,pr))
  }" 
  let "do {_  RECT ?body ?init; _}" = "?ndfs"

  let ?U = "E*``{v0}"

  define add_inv where "add_inv = (λblues reds onstack. 
    ¬(v(blues-onstack)A. (v,v)E+)  ― ‹No cycles over finished, accepting states›
     reds  blues                     ― ‹Red nodes are also blue›
     reds  onstack = {}              ― ‹No red nodes on stack›
     red_dfs_inv E ?U reds onstack)"

  define cyc_post where "cyc_post = (λblues reds onstack u0 cyc. (case cyc of 
      NO_CYC  add_inv blues reds onstack
    | REACH v p u p'  vA  uonstack-{u0}  p[] 
       path E v p u  path E u0 p' v
    | CIRC v pc pr  vA  pc[]  path E v pc v  path E u0 pr v
    ))"

  define pre where "pre = (λ(blues,reds,onstack,u).  
    gen_dfs_pre E ?U onstack blues u  add_inv blues reds onstack)"

  define post where "post = (λ(blues0,reds0::'v set,onstack0,u0) (blues,reds,onstack,cyc). 
    onstack = onstack0
     gen_dfs_post E ?U onstack0 blues0 u0 blues (cycNO_CYC)
     cyc_post blues reds onstack u0 cyc)"

  define fe_inv where "fe_inv = (λblues0 u0 onstack0 it (blues,reds,onstack,cyc). 
    onstack=onstack0 
     gen_dfs_fe_inv E ?U onstack0 blues0 u0 it blues (cycNO_CYC)
     cyc_post blues reds onstack u0 cyc)"

  have GENPRE: "gen_dfs_pre E ?U {} {} v0"
    apply (auto intro: gen_dfs_pre_initial)
    done
  hence PRE': "pre ({},{},{},v0)"
    unfolding pre_def add_inv_def
    apply (auto intro: red_dfs_inv_initial)
    done

  {
    fix blues reds onstack cyc
    assume "post ({},{},{},v0) (blues,reds,onstack,cyc)"
    hence "case cyc of NO_CYC  ¬has_acc_cycle E A v0
      | REACH _ _ _ _  False
      | CIRC v pc pr  is_acc_cycle E A v0 v pr pc"
      unfolding post_def cyc_post_def
      apply (cases cyc)
      using gen_dfs_post_imp_eq[OF GENPRE, of blues] 
      apply (auto simp: add_inv_def has_acc_cycle_def) []
      apply auto []
      apply (auto simp: is_acc_cycle_def) []
      done
  } note IMP_POST = this

  {
    fix onstack blues u0 reds
    assume "pre (blues,reds,onstack,u0)"
    hence "fe_inv (insert u0 blues) u0 (insert u0 onstack) (E``{u0}) 
      (insert u0 blues,reds,insert u0 onstack,NO_CYC)"
      unfolding fe_inv_def add_inv_def cyc_post_def
      apply clarsimp
      apply (intro conjI)
      apply (simp add: pre_def gen_dfs_pre_imp_fe)
      apply (auto simp: pre_def add_inv_def) []
      apply (auto simp: pre_def add_inv_def) []
      defer
      apply (auto simp: pre_def add_inv_def) []
      apply (unfold pre_def add_inv_def red_dfs_inv_def gen_dfs_pre_def) []
      apply clarsimp
      apply blast

      apply (auto simp: pre_def add_inv_def gen_dfs_pre_def) []
      done
  } note PRE_IMP_FE = this

  have [simp]: "u cyc. prep_wit_blue u cyc = NO_CYC  cyc=NO_CYC"
    by (case_tac cyc) auto

  {
    fix blues0 reds0 onstack0 u0 
      blues reds onstack blues' reds' onstack' 
      cyc it t
    assume PRE: "pre (blues0,reds0,onstack0,u0)"
    assume FEI: "fe_inv (insert u0 blues0) u0 (insert u0 onstack0) 
        it (blues,reds,onstack,NO_CYC)"
    assume IT: "tit" "itE``{u0}" "tblues"
    assume POST: "post (blues,reds,onstack, t) (blues',reds',onstack',cyc)"
    note [simp del] = path_simps
    have "fe_inv (insert u0 blues0) u0 (insert u0 onstack0) (it-{t}) 
      (blues',reds',onstack',prep_wit_blue u0 cyc)"
      unfolding fe_inv_def
      using PRE FEI IT POST
      unfolding fe_inv_def post_def pre_def
      apply (clarsimp)
      apply (intro allI impI conjI)
      apply (blast intro: gen_dfs_post_imp_fe_inv)
      unfolding cyc_post_def
      apply (auto split: blue_witness.split_asm intro: path_conc path_prepend)
      done
  } note FE_INV_PRES=this

  {
    fix blues reds onstack u0
    assume "pre (blues,reds,onstack,u0)"
    hence "(v0,u0)E*"
      unfolding pre_def gen_dfs_pre_def by auto
  } note PRE_IMP_REACH = this

  {
    fix blues0 reds0 onstack0 u0 blues reds onstack 
    assume A: "pre (blues0,reds0,onstack0,u0)"
       "fe_inv (insert u0 blues0) u0 (insert u0 onstack0) 
        {} (blues,reds,onstack,NO_CYC)"
       "u0A"
    have "u0reds" using A
      unfolding fe_inv_def add_inv_def pre_def cyc_post_def
      apply auto
      done
  } note FE_IMP_RED_PRE = this

  {
    fix blues0 reds0 onstack0 u0 blues reds onstack rcyc reds'
    assume PRE: "pre (blues0,reds0,onstack0,u0)"
    assume FEI: "fe_inv (insert u0 blues0) u0 (insert u0 onstack0) 
        {} (blues,reds,onstack,NO_CYC)"
    assume ACC: "u0A" 
    assume SPECR: "case rcyc of
      Some (p,v)  vonstack  p[]  path E u0 p v
    | None  
        red_dfs_inv E ?U reds' onstack 
         u0reds' 
         reds'  reds  E* `` {u0}"
    have "post (blues0,reds0,onstack0,u0) 
      (blues,reds',onstack - {u0},init_wit_blue u0 rcyc)"
      unfolding post_def add_inv_def cyc_post_def
      apply (clarsimp)
      apply (intro conjI)
    proof goal_cases
      from PRE FEI show OS0[symmetric]: "onstack - {u0} = onstack0"
        by (auto simp: pre_def fe_inv_def add_inv_def gen_dfs_pre_def) []

      from PRE FEI have "u0onstack"
        unfolding pre_def gen_dfs_pre_def fe_inv_def gen_dfs_fe_inv_def
        by auto

      from PRE FEI 
      show POST: "gen_dfs_post E (E* `` {v0}) onstack0 blues0 u0 blues 
        (init_wit_blue u0 rcyc  NO_CYC)" 
        by (auto simp: pre_def fe_inv_def intro: gen_dfs_fe_inv_imp_post)

      case 3

      from FEI have [simp]: "onstack=insert u0 onstack0" 
        unfolding fe_inv_def by auto
      from FEI have "u0blues" unfolding fe_inv_def gen_dfs_fe_inv_def by auto

      show ?case
        apply (cases rcyc)
        apply (simp_all add: split_paired_all)
      proof -
        assume [simp]: "rcyc=None"
        show "(v(blues - (onstack0 - {u0}))  A. (v, v)  E+) 
          reds'  blues 
          reds'  (onstack0 - {u0}) = {} 
          red_dfs_inv E (E* `` {v0}) reds' (onstack0 - {u0})"
        proof (intro conjI)
          from SPECR have RINV: "red_dfs_inv E ?U reds' onstack" 
            and "u0reds'" 
            and REDS'R: "reds'  reds  E*``{u0}"
            by auto

          from RINV show 
            RINV': "red_dfs_inv E (E* `` {v0}) reds' (onstack0 - {u0})"
            unfolding red_dfs_inv_def by auto

          from RINV'[unfolded red_dfs_inv_def] have 
            REDS'CL: "E``reds'  reds'" 
            and DJ': "E `` reds'  (onstack0 - {u0}) = {}" by auto

          from RINV[unfolded red_dfs_inv_def] have 
            DJ: "E `` reds'  (onstack) = {}" by auto

          show "reds'  blues" 
          proof 
            fix v assume "vreds'"
            with REDS'R have "vreds  (u0,v)E*" by blast
            thus "vblues" proof
              assume "vreds" 
              moreover with FEI have "redsblues" 
                unfolding fe_inv_def add_inv_def cyc_post_def by auto
              ultimately show ?thesis ..
            next
              from POST[unfolded gen_dfs_post_def OS0] have 
                CL: "E `` (blues - (onstack0 - {u0}))  blues" and "u0blues" 
                by auto
              from PRE FEI have "onstack0  blues"
                unfolding pre_def fe_inv_def gen_dfs_pre_def gen_dfs_fe_inv_def
                by auto

              assume "(u0,v)E*"
              thus "vblues"
              proof (cases rule: rtrancl_last_visit[where S="onstack - {u0}"])
                case no_visit
                thus "vblues" using u0blues CL 
                  by induct (auto elim: rtranclE)
              next
                case (last_visit_point u)
                then obtain uh where "(u0,uh)E*" and "(uh,u)E"
                  by (metis tranclD2) 
                with REDS'CL DJ' u0reds' have "uhreds'" 
                  by (auto dest: Image_closed_trancl)
                with DJ' (uh,u)E u  onstack - {u0} have False 
                  by simp blast
                thus ?thesis ..
              qed
            qed
          qed

          show "v(blues - (onstack0 - {u0}))  A. (v, v)  E+"
          proof 
            fix v
            assume A: "v  (blues - (onstack0 - {u0}))  A"
            show "(v,v)E+" proof (cases "v=u0")
              assume "vu0" 
              with A have "v(blues - (insert u0 onstack))  A" by auto
              with FEI show ?thesis 
                unfolding fe_inv_def add_inv_def cyc_post_def by auto
            next
              assume [simp]: "v=u0"
              show ?thesis proof
                assume "(v,v)E+"
                then obtain uh where "(u0,uh)E*" and "(uh,u0)E" 
                  by (auto dest: tranclD2)
                with REDS'CL DJ u0reds' have "uhreds'" 
                  by (auto dest: Image_closed_trancl)
                with DJ (uh,u0)E u0  onstack show False by blast
              qed
            qed
          qed

          show "reds'  (onstack0 - {u0}) = {}" 
          proof (rule ccontr)
            assume "reds'  (onstack0 - {u0})  {}"
            then obtain v where "vreds'" and "vonstack0" and "vu0" by auto
          
            from vreds' REDS'R have "vreds  (u0,v)E*"
              by auto
            thus False proof
              assume "vreds" 
              with FEI[unfolded fe_inv_def add_inv_def cyc_post_def] 
                vonstack0
              show False by auto
            next
              assume "(u0,v)E*"
              with vu0 obtain uh where "(u0,uh)E*" and "(uh,v)E"
                by (auto elim: rtranclE)
              with REDS'CL DJ u0reds' have "uhreds'" 
                by (auto dest: Image_closed_trancl)
              with DJ (uh,v)E v  onstack0 show False by simp blast
            qed
          qed
        qed
      next
        fix u p
        assume [simp]: "rcyc = Some (p,u)"
        show "(u = u0  u0  A  p  []  path E u0 p u0) 
          (u  u0  u0  A  u  onstack0  p  []  path E u0 p u)"
        proof (intro conjI impI)
          show "u0A" by fact
          show "u0A" by fact
          from SPECR show 
            "uu0  uonstack0" 
            "p[]" 
            "p[]" 
            "path E u0 p u" 
            "u=u0  path E u0 p u0"
            by auto
        qed
      qed
    qed
  } note RED_IMP_POST = this

  {
    fix blues0 reds0 onstack0 u0 blues reds onstack and cyc :: "'v blue_witness"
    assume PRE: "pre (blues0,reds0,onstack0,u0)"
    and FEI: "fe_inv (insert u0 blues0) u0 (insert u0 onstack0) 
        {} (blues,reds,onstack,NO_CYC)"
    and FC[simp]: "cyc=NO_CYC"
    and NCOND: "u0A"

    from PRE FEI have OS0: "onstack0 = onstack - {u0}" 
      by (auto simp: pre_def fe_inv_def add_inv_def gen_dfs_pre_def) []

    from PRE FEI have "u0onstack"
      unfolding pre_def gen_dfs_pre_def fe_inv_def gen_dfs_fe_inv_def
      by auto
    with OS0 have OS1: "onstack = insert u0 onstack0" by auto
    
    have "post (blues0,reds0,onstack0,u0) (blues,reds,onstack - {u0},NO_CYC)"
      apply (clarsimp simp: post_def cyc_post_def) []
      apply (intro conjI impI)
      apply (simp add: OS0)
      using PRE FEI apply (auto 
        simp: pre_def fe_inv_def intro: gen_dfs_fe_inv_imp_post) []
      
      using FEI[unfolded fe_inv_def cyc_post_def] unfolding add_inv_def
      apply clarsimp
      apply (intro conjI)
      using NCOND apply auto []
      apply auto []
      apply (clarsimp simp: red_dfs_inv_def, blast) []
      done
  } note NCOND_IMP_POST=this

  {
    fix blues0 reds0 onstack0 u0 blues reds onstack it 
      and cyc :: "'v blue_witness"
    assume PRE: "pre (blues0,reds0,onstack0,u0)"
    and FEI: "fe_inv (insert u0 blues0) u0 (insert u0 onstack0) 
        it (blues,reds,onstack,cyc)"
    and NC: "cycNO_CYC"
    and IT: "itE``{u0}"
    from PRE FEI have OS0: "onstack0 = onstack - {u0}"
      by (auto simp: pre_def fe_inv_def add_inv_def gen_dfs_pre_def) []

    from PRE FEI have "u0onstack"
      unfolding pre_def gen_dfs_pre_def fe_inv_def gen_dfs_fe_inv_def
      by auto
    with OS0 have OS1: "onstack = insert u0 onstack0" by auto

    have "post (blues0,reds0,onstack0,u0) (blues,reds,onstack - {u0},cyc)"
      apply (clarsimp simp: post_def) []
      apply (intro conjI impI)
      apply (simp add: OS0)
      using PRE FEI IT NC apply (auto 
        simp: pre_def fe_inv_def intro: gen_dfs_fe_imp_post_brk) []
      using FEI[unfolded fe_inv_def] NC 
      unfolding cyc_post_def 
      apply (auto split: blue_witness.split simp: OS1) []
      done
  } note BREAK_IMP_POST = this

  {
    fix σ
    assume INV0: "pre σ"
    have "RECT ?body σ 
       SPEC (post σ)"

      apply (intro refine_vcg
        RECT_rule[where pre="pre"
        and V="gen_dfs_var ?U <*lex*> {}"]
      )
      apply refine_mono
      apply (blast intro!: gen_dfs_pre_imp_wf[OF GENPRE])
      apply (rule INV0)

      ― ‹Foreach loop›
      apply (rule_tac 
        I="fe_inv (insert bb a) bb (insert bb ab)" 
        in FOREACHc_rule')

      apply (auto simp add: pre_def gen_dfs_pre_imp_fin) []

      apply (blast intro: PRE_IMP_FE)

      apply (intro refine_vcg)

      ― ‹Recursive call›
      apply (rule order_trans)
      apply (rprems)
      apply (clarsimp simp add: pre_def fe_inv_def cyc_post_def)
      apply (rule gen_dfs_fe_inv_imp_pre, assumption+) []
      apply (auto simp add: pre_def fe_inv_def intro: gen_dfs_fe_inv_imp_var) []

      apply (auto intro: FE_INV_PRES) []

      apply (auto simp add: pre_def post_def fe_inv_def 
        intro: gen_dfs_fe_inv_pres_visited) []

      apply (intro refine_vcg)

      ― ‹Nested DFS call›
      apply (rule order_trans)
      apply (rule red_dfs_correct[where U="E* `` {v0}"])
      apply (auto simp add: fe_inv_def add_inv_def cyc_post_def) []
      apply (auto intro: PRE_IMP_REACH) []
      apply (auto dest: FE_IMP_RED_PRE) []

      apply (intro refine_vcg)
      apply clarsimp
      apply (rule RED_IMP_POST, assumption+) []

      apply (clarsimp, blast intro: NCOND_IMP_POST) []

      apply (intro refine_vcg)
      apply simp

      apply (clarsimp, blast intro: BREAK_IMP_POST) []
      done
  } note GEN=this

  show ?thesis
    unfolding blue_dfs_def extract_res_def
    apply (intro refine_vcg)
    apply (rule order_trans)
    apply (rule GEN)
    apply fact
    apply (intro refine_vcg)
    apply clarsimp
    apply (drule IMP_POST)
    apply (simp split: blue_witness.split_asm)
    done
qed

subsection "Refinement"

subsubsection ‹Setup for Custom Datatypes›
text ‹This effort can be automated, but currently, such an automation is
  not yet implemented›
abbreviation "red_wit_rel  nat_rellist_rel,nat_relprod_reloption_rel"
abbreviation "wit_res_rel  
  nat_rel,nat_rellist_rel,nat_rellist_relprod_relprod_reloption_rel"
abbreviation "i_red_wit  i_natii_list,i_natii_prodii_option"
abbreviation "i_res  
  i_nat,i_natii_list,i_natii_listii_prodii_prodii_option"

abbreviation "blue_wit_rel  (Id::(nat blue_witness × _) set)"
consts i_blue_wit :: interface

term extract_res

lemma [autoref_itype]:
  "NO_CYC ::i i_blue_wit"
  "(=) ::i i_blue_wit i i_blue_wit i i_bool"
  "init_wit_blue ::i i_nat i i_red_wit i i_blue_wit"
  "prep_wit_blue ::i i_nat i i_blue_wit i i_blue_wit"
  "red_init_witness ::i i_nat i i_nat i i_red_wit"
  "prep_wit_red ::i i_nat i i_red_wit i i_red_wit"
  "extract_res ::i i_blue_wit i i_res"
  by auto

context begin interpretation autoref_syn .  
lemma [autoref_op_pat]: "NO_CYC  OP NO_CYC :::i i_blue_wit" by simp
end

lemma autoref_wit[autoref_rules_raw]:
  "(NO_CYC,NO_CYC)blue_wit_rel"
  "((=), (=))  blue_wit_rel  blue_wit_rel  bool_rel"
  "(init_wit_blue, init_wit_blue)  nat_rel  red_wit_rel  blue_wit_rel"
  "(prep_wit_blue,prep_wit_blue)nat_rel  blue_wit_rel  blue_wit_rel"
  "(red_init_witness, red_init_witness)  nat_relnat_relred_wit_rel"
  "(prep_wit_red,prep_wit_red)  nat_rel  red_wit_rel  red_wit_rel"
  "(extract_res,extract_res)  blue_wit_rel  wit_res_rel"
  by simp_all

subsubsection ‹Actual Refinement›



schematic_goal red_dfs_impl_refine_aux:
  (*notes [[goals_limit = 1]]*)
  fixes u'::"nat" and V'::"nat set"
  notes [autoref_tyrel] = 
    ty_REL[where 'a="nat set" and R="nat_reliam_set_rel"]
  assumes [autoref_rules]:
    "(u,u')nat_rel" 
    "(V,V')nat_reliam_set_rel" 
    "(onstack,onstack')nat_reliam_set_rel" 
    "(E,E')nat_relslg_rel"
  shows "(RETURN (?f::?'c), red_dfs E' onstack' V' u')  ?R"
  apply -
  unfolding red_dfs_def
  apply (autoref_monadic)
  done

concrete_definition red_dfs_impl uses red_dfs_impl_refine_aux
prepare_code_thms red_dfs_impl_def
declare red_dfs_impl.refine[autoref_higher_order_rule, autoref_rules]

schematic_goal ndfs_impl_refine_aux:
  fixes s::"nat"
  notes [autoref_tyrel] = 
    ty_REL[where 'a="nat set" and R="nat_reliam_set_rel"]
  assumes [autoref_rules]: 
    "(succi,E)nat_relslg_rel"
    "(Ai,A)nat_reliam_set_rel"
  notes [autoref_rules] = IdI[of s]
  shows "(RETURN (?f::?'c), blue_dfs E A s)  ?Rnres_rel"
  unfolding blue_dfs_def
  apply (autoref_monadic (trace))
  done

concrete_definition ndfs_impl for succi Ai s uses ndfs_impl_refine_aux 
prepare_code_thms ndfs_impl_def
export_code ndfs_impl checking SML

term "λE A v0. ndfs_impl (succ_of_list_impl E) (acc_of_list_impl A) v0"

term nat_of_integer

definition "succ_of_list_impl_int  
  succ_of_list_impl o map (λ(u,v). (nat_of_integer u, nat_of_integer v))"

definition "acc_of_list_impl_int  
  acc_of_list_impl o map nat_of_integer"

export_code 
  ndfs_impl 
  succ_of_list_impl_int
  acc_of_list_impl_int
  nat_of_integer
  integer_of_nat
  in SML module_name HPY_new

ML_val @{code ndfs_impl} (@{code succ_of_list_impl_int} [(1,2),(2,3),(2,7),(7,1)])
    (@{code acc_of_list_impl_int} [7]) (@{code nat_of_integer} 1)


schematic_goal ndfs_impl_refine_aux_old:
  fixes s::"nat"
  assumes [autoref_rules]: 
    "(succi,E)nat_relslg_rel"
    "(Ai,A)nat_reldflt_rs_rel"
  notes [autoref_rules] = IdI[of s]
  shows "(RETURN (?f::?'c), blue_dfs E A s)  ?Rnres_rel"
  unfolding blue_dfs_def red_dfs_def 
  using [[autoref_trace]]
  apply (autoref_monadic)
  done

end