Theory Gabow_Skeleton

section ‹Skeleton for Gabow's SCC Algorithm›
theory Gabow_Skeleton
imports "../lib/Base_MEC" "../ds/Graph" "../ds/Stack_Set"
begin

text ‹
  In this theory, we formalize a skeleton of Gabow's SCC algorithm. 
  The skeleton serves as a starting point to develop concrete algorithms,
  like enumerating the SCCs or checking emptiness of a generalized Büchi automaton.
›

section ‹Abstract Algorithm›
text ‹
  In this section, we formalize an abstract version of a path-based SCC algorithm.
  Later, this algorithm will be refined to use Gabow's data structure.
›

subsection ‹Preliminaries›
definition path_seg :: "'a set list ⇒ nat ⇒ nat ⇒ 'a set"
  ― ‹Set of nodes in a segment of the path›
  where "path_seg p i j ≡ ⋃{p!k|k. i≤k ∧ k<j}"

lemma path_seg_simps[simp]: 
  "j≤i ⟹ path_seg p i j = {}"
  "path_seg p i (Suc i) = p!i"
  unfolding path_seg_def
  apply auto []
  apply (auto simp: le_less_Suc_eq) []
  done

lemma path_seg_drop:
  "⋃(set (drop i p)) = path_seg p i (length p)"
  unfolding path_seg_def
  by (fastforce simp: in_set_drop_conv_nth Bex_def)

lemma path_seg_butlast: 
  "p≠[] ⟹ path_seg p 0 (length p - Suc 0) = ⋃(set (butlast p))"
  apply (cases p rule: rev_cases, simp)
  apply (fastforce simp: path_seg_def nth_append in_set_conv_nth)
  done

definition idx_of :: "'a set list ⇒ 'a ⇒ nat"
  ― ‹Index of path segment that contains a node›
  where "idx_of p v ≡ THE i. i<length p ∧ v∈p!i"

lemma idx_of_props:
  assumes 
    p_disjoint_sym: "∀i j v. i<length p ∧ j<length p ∧ v∈p!i ∧ v∈p!j ⟶ i=j"
  assumes ON_STACK: "v∈⋃(set p)"
  shows 
    "idx_of p v < length p" and
    "v ∈ p ! idx_of p v"
proof -
  from ON_STACK obtain i where "i<length p" "v ∈ p ! i"
    by (auto simp add: in_set_conv_nth)
  moreover hence "∀j<length p. v∈p ! j ⟶ i=j"
    using p_disjoint_sym by auto
  ultimately show "idx_of p v < length p" 
    and "v ∈ p ! idx_of p v" unfolding idx_of_def
    by (metis (lifting) theI')+
qed

lemma idx_of_uniq:
  assumes 
    p_disjoint_sym: "∀i j v. i<length p ∧ j<length p ∧ v∈p!i ∧ v∈p!j ⟶ i=j"
  assumes A: "i<length p" "v∈p!i"
  shows "idx_of p v = i"
proof -
  from A p_disjoint_sym have "∀j<length p. v∈p ! j ⟶ i=j" by auto
  with A show ?thesis
    unfolding idx_of_def
    by (metis (lifting) the_equality)
qed


subsection ‹Invariants›
text ‹The state of the inner loop consists of the path ‹p› of
  collapsed nodes, the set ‹D› of finished (done) nodes, the multiset
  ‹pE› of pending edges, and the set ‹vE› of visited edges.›
type_synonym 'v abs_state = "'v set list × 'v set × ('v × 'v) multiset × ('v × 'v) set"

context fr_graph
begin
  definition touched :: "'v set list ⇒ 'v set ⇒ 'v set" 
    ― ‹Touched: Nodes that are done or on path›
    where "touched p D ≡ D ∪ ⋃(set p)"

end

locale outer_invar_loc ― ‹Invariant of the outer loop›
  = fr_graph E V0 for E :: "'v digraph" and V0 +
  fixes it :: "'v set" ― ‹Remaining nodes to iterate over›
  fixes D :: "'v set" ― ‹Finished nodes›

  assumes it_initial: "it⊆V0"  ― ‹Only start nodes to iterate over›

  assumes it_done: "V0 - it ⊆ D"  ― ‹Nodes already iterated over are visited›
  assumes D_reachable: "D⊆E⇧*``V0" ― ‹Done nodes are reachable›
  assumes D_closed: "E``D ⊆ D" ― ‹Done is closed under transitions›
begin

  lemma locale_this: "outer_invar_loc E V0 it D" by unfold_locales

  definition (in fr_graph) "outer_invar ≡ λit D. outer_invar_loc E V0 it D"

  lemma outer_invar_this[simp, intro!]: "outer_invar it D"
    unfolding outer_invar_def apply simp by unfold_locales 
end

locale invar_loc ― ‹Invariant of the inner loop›
  = 
fr_graph E V0
  for E :: "'v digraph" and V0 +
  fixes v0 :: "'v"
  fixes D0 :: "'v set"
  fixes p :: "'v set list"
  fixes D :: "'v set"
  fixes pE :: "('v × 'v) multiset"
  fixes vE :: "('v × 'v) set"

  assumes v0_initial[simp, intro!]: "v0∈V0"
  assumes D_incr: "D0 ⊆ D"

  assumes vE_ss_E: "vE ⊆ E" ― ‹Visited edges are edges›

  assumes pE_E_from_p: "(set_mset pE) ⊆ E ∩ (⋃(set p)) × UNIV" 
    ― ‹Pending edges are edges from path›
  assumes E_from_p_touched: "E ∩ (⋃(set p) × UNIV) ⊆ (set_mset pE) ∪ UNIV × touched p D" 
    ― ‹Edges from path are pending or touched›
  assumes D_reachable: "D⊆E⇧*``V0" ― ‹Done nodes are reachable›
  assumes p_connected: "Suc i<length p ⟹ p!i × p!Suc i ∩ vE ≠ {}"
    ― ‹CNodes on path are connected by visited edges›

  assumes p_disjoint: "⟦i<j; j<length p⟧ ⟹ p!i ∩ p!j = {}" 
    ― ‹CNodes on path are disjoint›
  assumes p_sc: "U∈set p ⟹ U×U ⊆ (vE ∩ U×U)⇧*" 
    ― ‹Nodes in CNodes are mutually reachable by visited edges›

  assumes root_v0: "p≠[] ⟹ v0∈hd p" ― ‹Root CNode contains start node›
  assumes p_empty_v0: "p=[] ⟹ v0∈D" ― ‹Start node is done if path empty›
  
  assumes D_closed: "E``D ⊆ D" ― ‹Done is closed under transitions›

  assumes vE_no_back: "⟦i<j; j<length p⟧ ⟹ vE ∩ p!j × p!i = {}" 
  ― ‹Visited edges do not go back on path›

  assumes p_not_D: "⋃(set p) ∩ D = {}" ― ‹Path does not contain done nodes›

  assumes D_vis: "E∩D×UNIV ⊆ vE" ― ‹All edges from done nodes are visited›

  assumes vE_touched: "vE ⊆ touched p D × touched p D" ― ‹Visited edges only between touched nodes›
  assumes pE_if_not_visited: "(E ∩ ⋃(set p) × UNIV) - vE ⊆ set_mset pE" 
    ― ‹Edges from path not yet visited must be pending›

begin
  abbreviation ltouched where "ltouched ≡ touched p D"

  lemma locale_this: "invar_loc E V0 v0 D0 p D pE vE" by unfold_locales

  definition (in fr_graph) 
    "invar ≡ λv0 D0 (p,D,pE,vE). invar_loc E V0 v0 D0 p D pE vE"

  lemma invar_this[simp, intro!]: "invar v0 D0 (p,D,pE,vE)"
    unfolding invar_def apply simp by unfold_locales 

  lemma finite_reachableE_v0[simp, intro!]: "finite (E⇧*``{v0})"
    apply (rule finite_subset[OF _ finite_reachableE_V0])
    using v0_initial by auto


  lemma path_touched: "⋃(set p) ⊆ ltouched" by (auto simp: touched_def)
  lemma D_touched: "D ⊆ ltouched" by (auto simp: touched_def)

  lemma D_succs_in_D: "E ∩ (D × UNIV) = E ∩ (D × D)"
    using D_closed by blast

  lemma D_image_closed: "E⇧*``D = D"
    using D_closed
    by (simp add: Image_closed_trancl)

end

subsubsection ‹Termination›


context fr_graph 
begin
  text ‹The termination argument is based on unprocessed edges: 
    Reachable edges from untouched nodes and pending edges.›
  definition "reachable_edges v0 ≡ E ∩ (E⇧*``{v0}) × (E⇧*``{v0})"
  lemma reachable_edges_alt: "reachable_edges v0 = E ∩ (E⇧*``{v0}) × UNIV" 
    unfolding reachable_edges_def
    by auto

  definition "unproc_edges v0 vE ≡ reachable_edges v0 - vE"

  text ‹
    In each iteration of the loop, either the number of unprocessed edges
    decreases, or the path length decreases.›
  definition "abs_wf_rel v0 ≡ inv_image (finite_psubset <*lex*> measure size <*lex*> measure length)
    (λ(p,D,pE,vE). (unproc_edges v0 vE, pE, p))"

  lemma abs_wf_rel_wf[simp, intro!]: "wf (abs_wf_rel v0)"
    unfolding abs_wf_rel_def
    by auto
end

subsection ‹Abstract Skeleton Algorithm›

context fr_graph
begin

  definition out_edges :: "'v ⇒ (('v × 'v) multiset) nres" where
    "out_edges v = SPEC (λ r. set_mset r = (E ∩ {v}×UNIV))"

  definition initial :: "'v ⇒ 'v set ⇒ ('v abs_state) nres"
    where "initial v0 D ≡ do { pE ← out_edges v0; RETURN([{v0}], D, pE, E∩D×UNIV)}"

  definition (in -) collapse_aux :: "'a set list ⇒ nat ⇒ 'a set list"
    where "collapse_aux p i ≡ take i p @ [⋃(set (drop i p))]"

  definition (in -) collapse :: "'a ⇒ 'a abs_state ⇒ 'a abs_state" 
    where "collapse v PDPE ≡ 
    let 
      (p,D,pE,vE)=PDPE; 
      i=idx_of p v;
      p = collapse_aux p i
    in (p,D,pE,vE)"

  definition (in -) 
    select_edge :: "'a abs_state ⇒ ('a option × 'a abs_state) nres"
    where
    "select_edge PDPE ≡ do {
      let (p,D,pE,vE) = PDPE;
      e ← SELECT (λe. e ∈ (set_mset pE) ∩ last p × UNIV);
      case e of
        None ⇒ RETURN (None,(p,D,pE,vE))
      | Some (u,v) ⇒ RETURN (Some v, (p,D,pE - {#(u,v)#},insert (u,v) vE))
    }"

  definition push :: "'v ⇒ 'v abs_state ⇒ ('v abs_state) nres" 
    where "push v PDPE ≡ 
    do {
      let (p,D,pE,vE) = PDPE;
      let p = p@[{v}];
      pE' ← out_edges v;
      let pE = pE + pE';
      RETURN (p,D,pE,vE)
    }"

  definition (in -) pop :: "'v abs_state ⇒ 'v abs_state"
    where "pop PDPE ≡ let
      (p,D,pE,vE) = PDPE;
      (p,V) = (butlast p, last p);
      D = V ∪ D
    in
      (p,D,pE,vE)"

  definition skeleton :: "'v set nres" 
    ― ‹Abstract Skeleton Algorithm›
    where
    "skeleton ≡ do {
      let D = {};
      r ← FOREACHi outer_invar V0 (λv0 D0. do {
        if v0∉D0 then do {
          ASSERT(v0 ∈ E⇧*``V0);
          s ← initial v0 D0;

          (p,D,pE,vE) ← WHILEIT (invar v0 D0)
            (λ(p,D,pE,vE). p ≠ []) (λ(p,D,pE,vE). 
          do {
            ― ‹Select edge from end of path›
            (vo,(p,D,pE,vE)) ← select_edge (p,D,pE,vE);

            ASSERT (p≠[]);
            case vo of 
              Some v ⇒ do { ― ‹Found outgoing edge to node ‹v››
                ASSERT (v ∈ E⇧* `` V0);
                if v ∈ ⋃(set p) then do {
                  ― ‹Back edge: Collapse path›
                  RETURN (collapse v (p,D,pE,vE))
                } else if v∉D then do {
                  ― ‹Edge to new node. Append to path›
                  push v (p,D,pE,vE)
                } else do {
                  ― ‹Edge to done node. Skip›
                  RETURN (p,D,pE,vE)
                }
              }
            | None ⇒ do {
                ASSERT ((set_mset pE) ∩ last p × UNIV = {});
                ― ‹No more outgoing edges from current node on path›
                RETURN (pop (p,D,pE,vE))
              }
          }) s;
          ASSERT (p=[] ∧ pE={#});
          RETURN D
        } else
          RETURN D0
      }) D;
      RETURN r
    }"

end

subsection ‹Invariant Preservation›

context fr_graph begin

  lemma set_collapse_aux[simp]: "⋃(set (collapse_aux p i)) = ⋃(set p)"
    apply (subst (2) append_take_drop_id[of _ p,symmetric])
    apply (simp del: append_take_drop_id)
    unfolding collapse_aux_def by auto

  lemma touched_collapse[simp]: "touched (collapse_aux p i) D = touched p D"
    unfolding touched_def by simp

  lemma touched_push[simp]: "touched (p @ [V]) D = touched p D ∪ V"
    unfolding touched_def by auto

end

subsubsection ‹Corollaries of the invariant›
text ‹In this section, we prove some more corollaries of the invariant,
  which are helpful to show invariant preservation›

context invar_loc
begin
  lemma cnode_connectedI: 
    "⟦i<length p; u∈p!i; v∈p!i⟧ ⟹ (u,v)∈(vE ∩ p!i×p!i)⇧*"
    using p_sc[of "p!i"] by (auto simp: in_set_conv_nth)

  lemma cnode_connectedI': "⟦i<length p; u∈p!i; v∈p!i⟧ ⟹ (u,v)∈(vE)⇧*"
    by (metis inf.cobounded1 rtrancl_mono_mp cnode_connectedI)

  lemma p_no_empty: "{} ∉ set p"
  proof 
    assume "{}∈set p"
    then obtain i where IDX: "i<length p" "p!i={}" 
      by (auto simp add: in_set_conv_nth)
    show False proof (cases i)
      case 0 with root_v0 IDX show False by (cases p) auto
    next
      case [simp]: (Suc j)
      from p_connected[of j] IDX show False by simp
    qed
  qed

  corollary p_no_empty_idx: "i<length p ⟹ p!i≠{}"
    using p_no_empty by (metis nth_mem)
  
  lemma p_disjoint_sym: "⟦i<length p; j<length p; v∈p!i; v∈p!j⟧ ⟹ i=j"
    by (metis disjoint_iff_not_equal linorder_neqE_nat p_disjoint)

  lemma pi_ss_path_seg_eq[simp]:
    assumes A: "i<length p" "u≤length p"
    shows "p!i⊆path_seg p l u ⟷ l≤i ∧ i<u"
  proof
    assume B: "p!i⊆path_seg p l u"
    from A obtain x where "x∈p!i" by (blast dest: p_no_empty_idx)
    with B obtain i' where C: "x∈p!i'" "l≤i'" "i'<u" 
      by (auto simp: path_seg_def)
    from p_disjoint_sym[OF ‹i<length p› _ ‹x∈p!i› ‹x∈p!i'›] ‹i'<u› ‹u≤length p›
    have "i=i'" by simp
    with C show "l≤i ∧ i<u" by auto
  qed (auto simp: path_seg_def)

  lemma path_seg_ss_eq[simp]:
    assumes A: "l1<u1" "u1≤length p" "l2<u2" "u2≤length p"
    shows "path_seg p l1 u1 ⊆ path_seg p l2 u2 ⟷ l2≤l1 ∧ u1≤u2"
  proof
    assume S: "path_seg p l1 u1 ⊆ path_seg p l2 u2"
    have "p!l1 ⊆ path_seg p l1 u1" using A by simp
    also note S finally have 1: "l2≤l1" using A by simp
    have "p!(u1 - 1) ⊆ path_seg p l1 u1" using A by simp
    also note S finally have 2: "u1≤u2" using A by auto
    from 1 2 show "l2≤l1 ∧ u1≤u2" ..
  next
    assume "l2≤l1 ∧ u1≤u2" thus "path_seg p l1 u1 ⊆ path_seg p l2 u2"
      using A
      apply (clarsimp simp: path_seg_def) []
      apply (metis dual_order.strict_trans1 dual_order.trans)
      done
  qed

  lemma pathI: 
    assumes "x∈p!i" "y∈p!j"
    assumes "i≤j" "j<length p"
    defines "seg ≡ path_seg p i (Suc j)"
    shows "(x,y)∈(vE ∩ seg×seg)⇧*"
    ― ‹We can obtain a path between cnodes on path›
    using assms(3,1,2,4) unfolding seg_def
  proof (induction arbitrary: y rule: dec_induct)
    case base thus ?case by (auto intro!: cnode_connectedI)
  next
    case (step j)

    let ?seg = "path_seg p i (Suc j)"
    let ?seg' = "path_seg p i (Suc (Suc j))"

    have SSS: "?seg ⊆ ?seg'" 
      apply (subst path_seg_ss_eq)
      using step.hyps step.prems by auto

    from p_connected[OF ‹Suc j < length p›] obtain u v where 
      UV: "(u,v)∈vE" "u∈p!j" "v∈p!Suc j" by auto

    have ISS: "p!j ⊆ ?seg'" "p!Suc j ⊆ ?seg'" 
      using step.hyps step.prems by simp_all

    from p_no_empty_idx[of j] ‹Suc j < length p› obtain x' where "x'∈p!j" 
      by auto
    with step.IH[of x'] ‹x∈p!i› ‹Suc j < length p› 
    have t: "(x,x')∈(vE∩?seg×?seg)⇧*" by auto
    have "(x,x')∈(vE∩?seg'×?seg')⇧*" using SSS 
      by (auto intro: rtrancl_mono_mp[OF _ t])
    also 
    from cnode_connectedI[OF _ ‹x'∈p!j› ‹u∈p!j›] ‹Suc j < length p› have
      t: "(x', u) ∈ (vE ∩ p ! j × p ! j)⇧*" by auto
    have "(x', u) ∈ (vE∩?seg'×?seg')⇧*" using ISS
      by (auto intro: rtrancl_mono_mp[OF _ t])
    also have "(u,v)∈vE∩?seg'×?seg'" using UV ISS by auto
    also from cnode_connectedI[OF ‹Suc j < length p› ‹v∈p!Suc j› ‹y∈p!Suc j›] 
    have t: "(v, y) ∈ (vE ∩ p ! Suc j × p ! Suc j)⇧*" by auto
    have "(v, y) ∈ (vE∩?seg'×?seg')⇧*" using ISS
      by (auto intro: rtrancl_mono_mp[OF _ t])
    finally show "(x,y)∈(vE∩?seg'×?seg')⇧*" .
  qed

  lemma p_reachable: "⋃(set p) ⊆ E⇧*``{v0}" ― ‹Nodes on path are reachable›
  proof 
    fix v
    assume A: "v∈⋃(set p)"
    then obtain i where "i<length p" and "v∈p!i" 
      by (metis UnionE in_set_conv_nth)
    moreover from A root_v0 have "v0∈p!0" by (cases p) auto
    ultimately have 
      t: "(v0,v)∈(vE ∩ path_seg p 0 (Suc i) × path_seg p 0 (Suc i))⇧*"
      by (auto intro: pathI)
    from vE_ss_E have "(v0,v)∈E⇧*" by (auto intro: rtrancl_mono_mp[OF _ t])
    thus "v∈E⇧*``{v0}" by auto
  qed

  lemma p_elem_reachable: "X ∈ set p ⟹ X ⊆ E⇧* `` {v0}"
    using p_reachable
    by blast

  lemma touched_reachable: "ltouched ⊆ E⇧*``V0" ― ‹Touched nodes are reachable›
    unfolding touched_def using p_reachable D_reachable by blast

  lemma vE_reachable: "vE ⊆ E⇧*``V0 × E⇧*``V0"
    apply (rule order_trans[OF vE_touched])
    using touched_reachable by blast

  lemma pE_reachable: "(set_mset pE) ⊆ E⇧*``{v0} × E⇧*``{v0}"
  proof safe
    fix u v
    assume E: "(u,v)∈#pE"
    with pE_E_from_p p_reachable have "(v0,u)∈E⇧*" "(u,v)∈E" by blast+
    thus "(v0,u)∈E⇧*" "(v0,v)∈E⇧*" by auto
  qed

  lemma D_closed_vE_rtrancl: "vE⇧*``D ⊆ D"
    by (metis D_closed Image_closed_trancl eq_iff reachable_mono vE_ss_E)

  lemma D_closed_path: "⟦path E u q w; u∈D⟧ ⟹ set q ⊆ D"
  proof -
    assume a1: "path E u q w"
    assume "u ∈ D"
    hence f1: "{u} ⊆ D"
      using bot.extremum by force
    have "set q ⊆ E⇧* `` {u}"
      using a1 by (metis insert_subset path_nodes_reachable)
    thus "set q ⊆ D"
      using f1 by (metis D_closed rtrancl_reachable_induct subset_trans)
  qed

  lemma D_closed_path_vE: "⟦path vE u q w; u∈D⟧ ⟹ set q ⊆ D"
    by (metis D_closed_path path_mono vE_ss_E)

  lemma path_in_lastnode:
    assumes P: "path vE u q v"
    assumes [simp]: "p≠[]"
    assumes ND: "u∈last p" "v∈last p"
    shows "set q ⊆ last p"
    ― ‹A path from the last Cnode to the last Cnode remains in the last Cnode›
    using P ND
  proof (induction)
    case (path_prepend u v l w) 
    from ‹(u,v)∈vE› vE_touched have "v∈ltouched" by auto
    hence "v∈⋃(set p)"
      unfolding touched_def
    proof
      assume "v∈D"
      moreover from ‹path vE v l w› have "(v,w)∈vE⇧*" by (rule path_is_rtrancl)
      ultimately have "w∈D" using D_closed_vE_rtrancl by auto
      with ‹w∈last p› p_not_D have False
        by (metis IntI Misc.last_in_set Sup_inf_eq_bot_iff assms(2) 
          bex_empty path_prepend.hyps(2))
      thus ?thesis ..
    qed
    then obtain i where "i<length p" "v∈p!i"
      by (metis UnionE in_set_conv_nth)
    have "i=length p - 1"
    proof (rule ccontr)
      assume "i≠length p - 1"
      with ‹i<length p› have "i < length p - 1" by simp
      with vE_no_back[of i "length p - 1"] ‹i<length p› 
      have "vE ∩ last p × p!i = {}"
        by (simp add: last_conv_nth)
      with ‹(u,v)∈vE› ‹u∈last p› ‹v∈p!i› show False by auto
    qed
    with ‹v∈p!i› have "v∈last p" by (simp add: last_conv_nth)
    with path_prepend.IH ‹w∈last p› ‹u∈last p› show ?case by auto
  qed simp

  lemma loop_in_lastnode:
    assumes P: "path vE u q u"
    assumes [simp]: "p≠[]"
    assumes ND: "set q ∩ last p ≠ {}"
    shows "u∈last p" and "set q ⊆ last p"
    ― ‹A loop that touches the last node is completely inside the last node›
  proof -
    from ND obtain v where "v∈set q" "v∈last p" by auto
    then obtain q1 q2 where [simp]: "q=q1@v#q2" 
      by (auto simp: in_set_conv_decomp)
    from P have "path vE v (v#q2@q1) v" 
      by (auto simp: path_conc_conv path_cons_conv)
    from path_in_lastnode[OF this ‹p≠[]› ‹v∈last p› ‹v∈last p›] 
    show "set q ⊆ last p" by simp
    from P show "u∈last p" 
      apply (cases q, simp)
      
      apply simp
      using ‹set q ⊆ last p›
      apply (auto simp: path_cons_conv)
      done
  qed


  lemma no_D_p_edges: "E ∩ D × ⋃(set p) = {}"
    using D_closed p_not_D by auto

  lemma idx_of_props:
    assumes ON_STACK: "v∈⋃(set p)"
    shows 
      "idx_of p v < length p" and
      "v ∈ p ! idx_of p v"
    using idx_of_props[OF _ assms] p_disjoint_sym by blast+

end

subsubsection ‹Auxiliary Lemmas Regarding the Operations›

context invar_loc
begin
  lemma pE_fin: "p=[] ⟹ pE={#}"
    using pE_E_from_p by auto

  lemma lastp_un_D_closed:
    assumes NE: "p ≠ []"
    assumes NO': "(set_mset pE) ∩ (last p × UNIV) = {}"
    shows "E``(last p ∪ D) ⊆ (last p ∪ D)"
    ― ‹On pop, the popped CNode and D are closed under transitions›
  proof (intro subsetI, elim ImageE)

    have "(E - vE) ∩ (last p × UNIV) = (E ∩ ⋃ (set p) × UNIV - vE) ∩ (last p × UNIV)" 
      using NE by blast
    also from pE_if_not_visited have "... ⊆ (set_mset pE) ∩ (last p × UNIV)"
      by fast
    finally have NO: "(E - vE) ∩ (last p × UNIV) = {}" using NO' by blast

    let ?i = "length p - 1"
    from NE have [simp]: "last p = p!?i" by (metis last_conv_nth) 
    
    fix u v
    assume E: "(u,v)∈E"
    assume UI: "u∈last p ∪ D" hence "u∈p!?i ∪ D" by simp
    
    {
      assume "u∈last p" "v∉last p" 
      moreover from E NO ‹u∈last p› have "(u,v)∈vE" by auto
      ultimately have "v∈D ∨ v∈⋃(set p)" 
        using vE_touched unfolding touched_def by auto
      moreover {
        assume "v∈⋃(set p)"
        then obtain j where V: "j<length p" "v∈p!j" 
          by (metis UnionE in_set_conv_nth)
        with ‹v∉last p› have "j<?i" by (cases "j=?i") auto
        from vE_no_back[OF ‹j<?i› _] ‹(u,v)∈vE› V ‹u∈last p› have False by auto
      } ultimately have "v∈D" by blast
    } with E UI D_closed show "v∈last p ∪ D" by auto
  qed



end


subsubsection ‹Preservation of Invariant by Operations›

context fr_graph
begin
  lemma (in outer_invar_loc) invar_initial_aux: 
    assumes "v0∈it - D"
    shows "initial v0 D ≤ SPEC (invar v0 D)"
    unfolding invar_def initial_def out_edges_def
    apply refine_vcg
    apply clarsimp
    apply unfold_locales
    apply simp_all
    using assms it_initial apply auto []
    using D_reachable it_initial assms apply auto []
    using D_closed apply auto []
    using assms apply auto []
    unfolding touched_def 
    apply(subgoal_tac "E ∩ D × UNIV ⊆ E ∩ D × D")
      apply blast
      using D_closed apply blast
    apply blast
    done

  lemma invar_initial: 
    "⟦outer_invar it D0; v0∈it; v0∉D0⟧ ⟹ initial v0 D0 ≤ SPEC (invar v0 D0)"
    unfolding outer_invar_def
    apply (drule outer_invar_loc.invar_initial_aux) 
    by auto

  lemma outer_invar_initial[simp, intro!]: "outer_invar V0 {}"
    unfolding outer_invar_def
    apply unfold_locales
    by auto

  lemma invar_pop:
    assumes INV: "invar v0 D0 (p,D,pE,vE)"
    assumes NE[simp]: "p≠[]"
    assumes NO': "(set_mset pE) ∩ (last p × UNIV) = {}"
    shows "invar v0 D0 (pop (p,D,pE,vE))"
    unfolding invar_def pop_def
    apply simp
  proof -
    from INV interpret invar_loc E V0 v0 D0 p D pE unfolding invar_def by simp

    have [simp]: "set p = insert (last p) (set (butlast p))" 
      using NE by (cases p rule: rev_cases) auto

    from p_disjoint have lp_dj_blp: "last p ∩ ⋃(set (butlast p)) = {}"
      apply (cases p rule: rev_cases)
      apply simp
      apply (fastforce simp: in_set_conv_nth nth_append)
      done

    {
      fix i
      assume A: "Suc i < length (butlast p)"
      hence A': "Suc i < length p" by auto

      from nth_butlast[of i p] A have [simp]: "butlast p ! i = p ! i" by auto
      from nth_butlast[of "Suc i" p] A 
      have [simp]: "butlast p ! Suc i = p ! Suc i" by auto

      from p_connected[OF A'] 
      have "butlast p ! i × butlast p ! Suc i ∩ vE ≠ {}"
        by simp
    } note AUX_p_connected = this

    have AUX_last_p_visited: "E ∩ last p × UNIV ⊆ vE"
    proof safe
      fix u v
      assume UVE: "(u,v) ∈ E"
      and ULP: "u ∈ last p"
      hence "(u,v) ∉# pE" using NO' by blast
      moreover have "(u,v) ∈ E ∩ (⋃(set p)) × UNIV" using ULP UVE by auto
      ultimately show "(u,v) ∈ vE" using pE_if_not_visited by blast
    qed
      

    show "invar_loc E V0 v0 D0 (butlast p) (last p ∪ D) pE vE"
      apply unfold_locales
      subgoal by simp
      subgoal using D_incr by auto
      subgoal using vE_ss_E by simp
      subgoal using pE_E_from_p NO' by auto []
      subgoal using E_from_p_touched by (auto simp: touched_def) []
      subgoal using D_reachable p_reachable NE by auto []
      subgoal by (rule AUX_p_connected, assumption+) []
      subgoal using p_disjoint by (simp add: nth_butlast)
      subgoal using p_sc by simp
      subgoal using root_v0 by (cases p rule: rev_cases; auto)
      subgoal using root_v0 p_empty_v0 by (cases p rule: rev_cases; auto)
      subgoal apply (rule lastp_un_D_closed) using insert NO' by auto
      subgoal using vE_no_back by (auto simp: nth_butlast)
      subgoal using p_not_D lp_dj_blp by auto
      subgoal using D_vis AUX_last_p_visited by blast
      subgoal using vE_touched unfolding touched_def by auto
      subgoal using pE_if_not_visited by auto
      done
  qed

  lemma set_mset_subtract_cases: obtains "set_mset (m-{#x#}) = set_mset m" | "set_mset (m-{#x#}) = set_mset m - {x}"
    by (meson at_most_one_mset_mset_diff more_than_one_mset_mset_diff)

  lemma invar_collapse:
    assumes INV: "invar v0 D0 (p,D,pE,vE)"
    assumes NE[simp]: "p≠[]"
    assumes E: "(u,v)∈#pE" and "u∈last p"
    assumes BACK: "v∈⋃(set p)"
    defines "i ≡ idx_of p v"
    defines "p' ≡ collapse_aux p i"
    shows "invar v0 D0 (collapse v (p,D,pE - {#(u,v)#},insert (u,v) vE))"
    unfolding invar_def collapse_def
    apply simp
    unfolding i_def[symmetric] p'_def[symmetric]
  proof -
    from INV interpret invar_loc E V0 v0 D0 p D pE unfolding invar_def by simp

    let ?thesis="invar_loc E V0 v0 D0 p' D (pE - {#(u,v)#}) (insert (u,v) vE)"

    have SETP'[simp]: "⋃(set p') = ⋃(set p)" unfolding p'_def by simp

    have IL: "i < length p" and VMEM: "v∈p!i" 
      using idx_of_props[OF BACK] unfolding i_def by auto

    have [simp]: "length p' = Suc i" 
      unfolding p'_def collapse_aux_def using IL by auto

    have P'_IDX_SS: "∀j<Suc i. p!j ⊆ p'!j"
      unfolding p'_def collapse_aux_def using IL 
      by (auto simp add: nth_append path_seg_drop)

    from ‹u∈last p› have "u∈p!(length p - 1)" by (auto simp: last_conv_nth)

    have defs_fold: 
      "touched p' D = ltouched"
      by (simp_all add: p'_def E)

    {
      fix j
      assume A: "Suc j < length p'" 
      hence "Suc j < length p" using IL by simp
      note p_connected[OF this]
      moreover from P'_IDX_SS A have "p!j⊆p'!j" and "p!Suc j ⊆ p'!Suc j"
        by auto
      ultimately have "p' ! j × p' ! Suc j ∩ insert (u,v) vE ≠ {}" 
        by blast
    } note AUX_p_connected = this

    have P_IDX_EQ[simp]: "∀j. j < i ⟶ p'!j = p!j"
      unfolding p'_def collapse_aux_def using IL  
      by (auto simp: nth_append)

    have P'_LAST[simp]: "p'!i = path_seg p i (length p)" (is "_ = ?last_cnode")
      unfolding p'_def collapse_aux_def using IL 
      by (auto simp: nth_append path_seg_drop)

    {
      fix j k
      assume A: "j < k" "k < length p'" 
      have "p' ! j ∩ p' ! k = {}"
      proof (safe, simp)
        fix v
        assume "v∈p'!j" and "v∈p'!k"
        with A have "v∈p!j" by simp
        show False proof (cases)
          assume "k=i"
          with ‹v∈p'!k› obtain k' where "v∈p!k'" "i≤k'" "k'<length p" 
            by (auto simp: path_seg_def)
          hence "p ! j ∩ p ! k' = {}"
            using A by (auto intro!: p_disjoint)
          with ‹v∈p!j› ‹v∈p!k'› show False by auto
        next
          assume "k≠i" with A have "k<i" by simp
          hence "k<length p" using IL by simp
          note p_disjoint[OF ‹j<k› this] 
          also have "p!j = p'!j" using ‹j<k› ‹k<i› by simp
          also have "p!k = p'!k" using ‹k<i› by simp
          finally show False using ‹v∈p'!j› ‹v∈p'!k› by auto
        qed
      qed
    } note AUX_p_disjoint = this

    {
      fix U
      assume A: "U∈set p'"
      then obtain j where "j<Suc i" and [simp]: "U=p'!j"
        by (auto simp: in_set_conv_nth)
      hence "U × U ⊆ (insert (u, v) vE ∩ U × U)⇧*" 
      proof cases
        assume [simp]: "j=i"
        show ?thesis proof (clarsimp)
          fix x y
          assume "x∈path_seg p i (length p)" "y∈path_seg p i (length p)"
          then obtain ix iy where 
            IX: "x∈p!ix" "i≤ix" "ix<length p" and
            IY: "y∈p!iy" "i≤iy" "iy<length p"
            by (auto simp: path_seg_def)
            

          from IX have SS1: "path_seg p ix (length p) ⊆ ?last_cnode"
            by (subst path_seg_ss_eq) auto

          from IY have SS2: "path_seg p i (Suc iy) ⊆ ?last_cnode"
            by (subst path_seg_ss_eq) auto

          let ?rE = "λR. (vE ∩ R×R)"
          let ?E = "(insert (u,v) vE ∩ ?last_cnode × ?last_cnode)"

          from pathI[OF ‹x∈p!ix› ‹u∈p!(length p - 1)›] have
            "(x,u)∈(?rE (path_seg p ix (Suc (length p - 1))))⇧*" using IX by auto
          hence "(x,u)∈?E⇧*" 
            apply (rule rtrancl_mono_mp[rotated]) 
            using SS1
            by auto

          also have "(u,v)∈?E" using ‹i<length p›
            apply (clarsimp)
            apply (intro conjI)
            apply (rule rev_subsetD[OF ‹u∈p!(length p - 1)›])
            apply (simp)
            apply (rule rev_subsetD[OF VMEM])
            apply (simp)
            done
          also 
          from pathI[OF ‹v∈p!i› ‹y∈p!iy›] have
            "(v,y)∈(?rE (path_seg p i (Suc iy)))⇧*" using IY by auto
          hence "(v,y)∈?E⇧*"
            apply (rule rtrancl_mono_mp[rotated]) 
            using SS2
            by auto
          finally show "(x,y)∈?E⇧*" .
        qed
      next
        assume "j≠i"
        with ‹j<Suc i› have [simp]: "j<i" by simp
        with ‹i<length p› have "p!j∈set p"
          by (metis Suc_lessD in_set_conv_nth less_trans_Suc) 

        thus ?thesis using p_sc[of U] ‹p!j∈set p›
          apply (clarsimp)
          apply (subgoal_tac "(a,b)∈(vE ∩ p ! j × p ! j)⇧*")
          apply (erule rtrancl_mono_mp[rotated])
          apply auto
          done
      qed
    } note AUX_p_sc = this

    { fix j k
      assume A: "j<k" "k<length p'"
      hence "j<i" by simp
      have "insert (u, v) vE ∩ p' ! k × p' ! j = {}"
      proof -
        have "{(u,v)} ∩ p' ! k × p' ! j = {}" 
          apply auto
          by (metis IL P_IDX_EQ Suc_lessD VMEM ‹j < i› 
            less_irrefl_nat less_trans_Suc p_disjoint_sym)
        moreover have "vE ∩ p' ! k × p' ! j = {}" 
        proof (cases "k<i")
          case True thus ?thesis
            using vE_no_back[of j k] A ‹i<length p› by auto
        next
          case False with A have [simp]: "k=i" by simp
          show ?thesis proof (rule disjointI, clarsimp simp: ‹j<i›)
            fix x y
            assume B: "(x,y)∈vE" "x∈path_seg p i (length p)" "y∈p!j"
            then obtain ix where "x∈p!ix" "i≤ix" "ix<length p" 
              by (auto simp: path_seg_def)
            moreover with A have "j<ix" by simp
            ultimately show False using vE_no_back[of j ix] B by auto
          qed
        qed
        ultimately show ?thesis by blast
      qed
    } note AUX_vE_no_back = this

    have V_TOUCHED: "v∈ltouched" using BACK path_touched by auto

    note pE_removed_cases = set_mset_subtract_cases[of pE "(u,v)"]

    

    show ?thesis
      apply unfold_locales
      unfolding defs_fold

      subgoal by simp

      subgoal using D_incr by auto []

      subgoal using vE_ss_E E pE_E_from_p by blast

      subgoal using pE_E_from_p in_diffD SETP' subset_eq by metis
      
      subgoal
        apply (simp) using E_from_p_touched V_TOUCHED 
        apply (cases rule: pE_removed_cases)
        by (auto)

      subgoal by (rule D_reachable)    

      subgoal by (rule AUX_p_connected)

      subgoal by (rule AUX_p_disjoint)

      subgoal for U by (rule AUX_p_sc)

      subgoal
        using root_v0 
        apply (cases i) 
        apply (simp add: p'_def collapse_aux_def)
        apply (metis NE hd_in_set)
        apply (cases p, simp_all add: p'_def collapse_aux_def) []
        done

      subgoal by (simp add: p'_def collapse_aux_def)

      subgoal by (rule D_closed)

      subgoal by (drule (1) AUX_vE_no_back, auto)

      subgoal using p_not_D by simp

      subgoal using D_vis by auto
      subgoal 
        using V_TOUCHED vE_touched 
        apply clarsimp
        using ‹u∈last p› path_touched 
        by fastforce
      subgoal by (smt (verit) Diff_eq_empty_iff Diff_insert Diff_insert2 E SETP' insert_Diff pE_if_not_visited pE_removed_cases subset_insertI)
      done

  qed
  
  lemma invar_push:
    assumes INV: "invar v0 D0 (p,D,pE,vE)"
    assumes NE[simp]: "p≠[]"
    assumes E: "(u,v)∈#pE" and UIL: "u∈last p"
    assumes VNE: "v∉⋃(set p)" "v∉D"
    shows "push v (p,D,pE - {#(u,v)#}, insert (u,v) vE) ≤ SPEC (invar v0 D0)"
    unfolding invar_def push_def out_edges_def
    apply refine_vcg
    apply clarsimp
  proof -
    fix succE
    assume succE_v: "set_mset succE = E ∩ {v} × UNIV"

    from INV interpret invar_loc E V0 v0 D0 p D pE unfolding invar_def by simp

    let ?thesis 
      = "invar_loc E V0 v0 D0 (p @ [{v}]) D (pE - {#(u, v)#} + succE) (insert (u, v) vE)"

    note defs_fold = touched_push

    note pE_removed_cases = set_mset_subtract_cases[of pE "(u,v)"]

    {
      fix i
      assume SILL: "Suc i < length (p @ [{v}])"
      have "(p @ [{v}]) ! i × (p @ [{v}]) ! Suc i 
             ∩ insert (u, v) vE ≠ {}"
      proof (cases "i = length p - 1")
        case True thus ?thesis using SILL E pE_E_from_p UIL VNE
          by (simp add: nth_append last_conv_nth)
      next
        case False
        with SILL have SILL': "Suc i < length p" by simp
            
        with SILL' VNE have X1: "v∉p!i" "v∉p!Suc i" by auto

        from p_connected[OF SILL'] obtain a b where 
          "a∈p!i" "b∈p!Suc i" "(a,b)∈vE" by auto 

        with ‹a∈p!i› ‹b∈p!Suc i›
        show ?thesis using SILL'
          by (simp add: nth_append; blast) 
      qed
    } note AUX_p_connected = this



    {
      fix U
      assume A: "U ∈ set (p @ [{v}])"
      have "U × U ⊆ (insert (u, v) vE ∩ U × U)⇧*"
      proof cases
        assume "U∈set p"
        with p_sc have "U×U ⊆ (vE ∩ U×U)⇧*" .
        thus ?thesis
          by (metis (lifting, no_types) Int_insert_left_if0 Int_insert_left_if1 
            in_mono insert_subset rtrancl_mono_mp subsetI)
      next
        assume "U∉set p" with A have "U={v}" by simp
        thus ?thesis by auto
      qed
    } note AUX_p_sc = this

    {
      fix i j
      assume A: "i < j" "j < length (p @ [{v}])"
      have "insert (u, v) vE ∩ (p @ [{v}]) ! j × (p @ [{v}]) ! i = {}"
      proof (cases "j=length p")
        case False with A have "j<length p" by simp
        from vE_no_back ‹i<j› this VNE show ?thesis 
          by (auto simp add: nth_append)
      next
        from p_not_D A have PDDJ: "p!i ∩ D = {}" 
          by (auto simp: Sup_inf_eq_bot_iff)
        case True thus ?thesis
          using A apply (simp add: nth_append)
          apply (rule conjI)
          using UIL A p_disjoint_sym
          apply (metis Misc.last_in_set NE UnionI VNE(1))

          using vE_touched VNE PDDJ apply (auto simp: touched_def) []
          done
      qed
    } note AUX_vE_no_back = this

    have U_TOUCHED: "u∈ltouched"
      using ‹u∈last p› path_touched by fastforce
        
    show ?thesis
      apply unfold_locales
      unfolding defs_fold

      subgoal by simp

      subgoal using D_incr by auto []

      subgoal using vE_ss_E E pE_E_from_p by blast 

      subgoal using pE_E_from_p succE_v by (auto dest: in_diffD)

      subgoal      
        apply (cases rule: pE_removed_cases)
        using E_from_p_touched VNE succE_v
        by auto
        
      subgoal by (rule D_reachable)

      subgoal for i by (rule AUX_p_connected)
        

      subgoal using p_disjoint ‹v∉⋃(set p)› by (auto simp: nth_append)

      subgoal for U by (rule AUX_p_sc)

      subgoal using root_v0 by simp

      subgoal by simp

      subgoal by (rule D_closed)

      subgoal for i j by (rule AUX_vE_no_back)

      subgoal using p_not_D VNE by auto

      subgoal using D_vis by auto
      subgoal using vE_touched U_TOUCHED by auto
      subgoal
        apply (cases rule: pE_removed_cases)
        using succE_v pE_if_not_visited
        by auto
      done
  qed

  lemma invar_pE_is_node:
    assumes INV: "invar v0 D0 (p,D,pE,vE)"
    assumes E: "(u,v)∈#pE"
    shows "v∈E⇧*``V0"
  proof -
    from INV interpret invar_loc E V0 v0 D0 p D pE unfolding invar_def by simp
    from E pE_reachable show ?thesis by blast
  qed

  lemma invar_skip:
    assumes INV: "invar v0 D0 (p,D,pE,vE)"
    assumes NE[simp]: "p≠[]"
    assumes E: "(u,v)∈#pE" and UIL: "u∈last p"
    assumes VNP: "v∉⋃(set p)" and VD: "v∈D"
    shows "invar v0 D0 (p,D,pE - {#(u, v)#}, insert (u,v) vE)"
    unfolding invar_def
    apply simp
  proof -
    from INV interpret invar_loc E V0 v0 D0 p D pE unfolding invar_def by simp
    let ?thesis = "invar_loc E V0 v0 D0 p D (pE - {#(u, v)#}) (insert (u,v) vE)"

    note pE_removed_cases = set_mset_subtract_cases[of pE "(u,v)"]

    have U_TOUCHED: "u∈ltouched"
      using ‹u∈last p› path_touched by fastforce

    have V_TOUCHED: "v ∈ ltouched"
      using ‹v∈D› D_touched by blast

    show ?thesis
      apply unfold_locales
      
      subgoal by simp

      subgoal using D_incr by auto

      subgoal using vE_ss_E E pE_E_from_p by blast 

      subgoal using pE_E_from_p apply (cases rule:pE_removed_cases) by auto

      subgoal using E_from_p_touched VD apply (cases rule:pE_removed_cases) by (auto simp: touched_def)

      subgoal by (rule D_reachable)

      subgoal using p_connected by auto []

      subgoal by (rule p_disjoint)

      subgoal 
        apply (drule p_sc)
        apply (erule order_trans)
        apply (rule rtrancl_mono)
        by blast []

      subgoal by (rule root_v0)

      subgoal by (rule p_empty_v0)

      subgoal by (rule D_closed)

      subgoal for i j
        using vE_no_back VD p_not_D 
        apply clarsimp
        by (metis Suc_lessD UnionI VNP less_trans_Suc nth_mem)

      subgoal by (rule p_not_D)

      subgoal using D_vis by auto
      subgoal using vE_touched U_TOUCHED V_TOUCHED by auto
      subgoal
        apply (cases rule: pE_removed_cases)
        using  pE_if_not_visited
        by auto
      done
  qed


  lemma fin_D_is_reachable: 
    ― ‹When inner loop terminates, all nodes reachable from start node are
      finished›
    assumes INV: "invar v0 D0 ([], D, pE, vE)"
    shows "D ⊇ E⇧*``{v0}"
  proof -
    from INV interpret invar_loc E V0 v0 D0 "[]" D pE vE unfolding invar_def by auto

    from p_empty_v0 rtrancl_reachable_induct[OF order_refl D_closed] D_reachable
    show ?thesis by auto
  qed

  lemma fin_reachable_path: 
    ― ‹When inner loop terminates, nodes reachable from start node are
      reachable over visited edges›
    assumes INV: "invar v0 D0 ([], D, pE, vE)"
    assumes UR: "u∈E⇧*``{v0}"
    shows "path vE u q v ⟷ path E u q v"
  proof -
    from INV interpret invar_loc E V0 v0 D0 "[]" D pE vE unfolding invar_def by auto
    
    show ?thesis
    proof
      assume "path vE u q v"
      thus "path E u q v" using path_mono[OF vE_ss_E] by blast
    next
      assume "path E u q v"
      thus "path vE u q v" using UR
      proof induction
        case (path_prepend u v p w)
        with fin_D_is_reachable[OF INV] have "u∈D" by auto
        with D_closed ‹(u,v)∈E› have "v∈D" by auto
        from path_prepend.prems path_prepend.hyps have "v∈E⇧*``{v0}" by auto
        with path_prepend.IH fin_D_is_reachable[OF INV] have "path vE v p w" 
          by simp
        moreover from ‹u∈D› ‹v∈D› ‹(u,v)∈E› D_vis have "(u,v)∈vE" by auto
        ultimately show ?case by (auto simp: path_cons_conv)
      qed simp
    qed
  qed

  lemma invar_outer_newnode: 
    assumes A: "v0∉D0" "v0∈it" 
    assumes OINV: "outer_invar it D0"
    assumes INV: "invar v0 D0 ([],D',pE,vE)"
    shows "outer_invar (it-{v0}) D'"
  proof -
    from OINV interpret outer_invar_loc E V0 it D0 unfolding outer_invar_def .
    from INV interpret inv: invar_loc E V0 v0 D0 "[]" D' pE vE
      unfolding invar_def by simp
    
    from fin_D_is_reachable[OF INV] have [simp]: "v0∈D'" by auto

    show ?thesis
      unfolding outer_invar_def
      apply unfold_locales
      using it_initial apply auto []
      using it_done inv.D_incr apply auto []
      using inv.D_reachable apply assumption
      using inv.D_closed apply assumption
      done
  qed

  lemma invar_outer_Dnode:
    assumes A: "v0∈D0" "v0∈it" 
    assumes OINV: "outer_invar it D0"
    shows "outer_invar (it-{v0}) D0"
  proof -
    from OINV interpret outer_invar_loc E V0 it D0 unfolding outer_invar_def .
    
    show ?thesis
      unfolding outer_invar_def
      apply unfold_locales
      using it_initial apply auto []
      using it_done A apply auto []
      using D_reachable apply assumption
      using D_closed apply assumption
      done
  qed

  lemma pE_fin': "invar x σ ([], D, pE, vE) ⟹ pE={#}"
    unfolding invar_def by (simp add: invar_loc.pE_fin)

end

subsubsection ‹Termination›


context invar_loc 
begin
  lemma reachable_finite[simp, intro!]: "finite (reachable_edges v0)"
    ― ‹The set of unprocessed edges is finite›
  proof -
    have "reachable_edges v0 ⊆ E⇧*``{v0} × E⇧*``{v0}"
      unfolding reachable_edges_def
      by auto
    thus ?thesis
      by (rule finite_subset) simp
  qed


  lemma unproc_finite[simp, intro!]: "finite (unproc_edges v0 vE)"
    ― ‹The set of unprocessed edges is finite›
    unfolding unproc_edges_def
    by auto

  lemma pE_reachable_edges: "set_mset pE ⊆ reachable_edges v0"
    using pE_reachable pE_E_from_p unfolding reachable_edges_def
    by blast
    
end


context fr_graph 
begin


  lemma abs_wf_pop:
    assumes NE[simp]: "p≠[]"
    shows "(pop (p,D,pE,vE), (p, D, pE,vE)) ∈ abs_wf_rel v0"
    unfolding pop_def
    by (auto simp: abs_wf_rel_def)

  lemma abs_wf_take_edge:
    assumes INV: "invar v0 D0 (p,D,pE,vE)"
    assumes E: "(u,v) ∈# pE" 
    shows "((p',D',pE-{#(u,v)#}, insert(u,v) vE), (p, D, pE, vE))∈ abs_wf_rel v0"
  proof -
    from INV interpret invar_loc E V0 v0 D0 p D pE unfolding invar_def by simp 

    have "size (pE - {#(u,v)#}) < size pE" using E 
      by (simp add: size_Diff1_less)
    then show ?thesis
      using assms
      by (clarsimp simp: abs_wf_rel_def unproc_edges_def)

  qed    

  lemma abs_wf_collapse:
    assumes INV: "invar v0 D0 (p,D,pE,vE)"
    assumes E: "(u,v)∈#pE"
    shows "(collapse v (p,D,pE-{#(u,v)#}, insert(u,v) vE), (p, D, pE, vE))∈ abs_wf_rel v0"
    using INV E
    unfolding collapse_def
    by (simp add: abs_wf_take_edge)
    
  lemma abs_wf_push:
    assumes INV: "invar v0 D0 (p,D,pE,vE)"
    assumes NE[simp]: "p≠[]"
    assumes E: "(u,v)∈#pE" "u∈last p" and A: "v∉D" "v∉⋃(set p)"
    shows "push v (p,D,pE-{#(u,v)#},insert (u,v) vE) ≤ SPEC (λr. (r, (p, D, pE, vE)) ∈ abs_wf_rel v0)"
    unfolding push_def out_edges_def
    apply refine_vcg
    apply clarsimp
  proof -
    fix succE
    assume succE_v: "set_mset succE = E ∩ {v} × UNIV"

    from INV interpret invar_loc E V0 v0 D0 p D pE vE unfolding invar_def by simp 
    let ?thesis 
      = "((p@[{v}], D, pE - {#(u, v)#} + succE, insert (u, v) vE), (p, D, pE, vE)) ∈ abs_wf_rel v0"

    have "(u,v)∉vE" using vE_touched A unfolding touched_def by blast
    hence "unproc_edges v0 (insert (u,v) vE) ⊂ unproc_edges v0 vE"
      unfolding unproc_edges_def using pE_reachable_edges E by blast
    thus ?thesis
    unfolding abs_wf_rel_def by simp
  qed

  lemma abs_wf_skip:
    assumes INV: "invar v0 D0 (p,D,pE,vE)"
    assumes E: "(u,v)∈#pE"
    shows "((p, D, pE-{#(u,v)#}, insert (u,v) vE), (p, D, pE, vE)) ∈ abs_wf_rel v0"
    using assms abs_wf_take_edge by simp
end

subsubsection ‹Main Correctness Theorem›

context fr_graph 
begin
  lemmas invar_preserve = 
    invar_pop invar_skip invar_collapse 
    abs_wf_pop abs_wf_collapse  abs_wf_skip 
    outer_invar_initial invar_outer_newnode invar_outer_Dnode

    invar_pE_is_node


  lemma invar_rel_push:
    assumes INV: "invar v0 D0 (p,D,pE,vE)"
    assumes NE[simp]: "p≠[]"
    assumes E: "(u,v)∈#pE" and UIL: "u∈last p"
    assumes VNE: "v∉⋃(set p)" "v∉D"
    shows "push v (p,D,pE - {#(u,v)#}, insert (u,v) vE) ≤ SPEC (λr. invar v0 D0 r ∧ (r,(p,D,pE,vE)) ∈ abs_wf_rel v0)"
    apply (rule SPEC_rule_conjI[OF invar_push abs_wf_push])
    by fact+

  lemmas [refine_vcg] = invar_initial

  text ‹The main correctness theorem for the dummy-algorithm just states that
    it satisfies the invariant when finished, and the path is empty.
  ›
  theorem skeleton_spec: "skeleton ≤ SPEC (λD. outer_invar {} D)"
  proof -
    note [simp del] = Union_iff
    note [[goals_limit = 7]]

    note [refine_vcg del] = WHILEIT_rule

    note [simp] = invar_pE_is_node

    show ?thesis
      unfolding skeleton_def select_edge_def select_def
      apply (refine_vcg)
      apply (vc_solve solve: invar_preserve simp: pE_fin')
      apply auto
      apply (refine_vcg WHILEIT_rule[OF abs_wf_rel_wf])
      apply (vc_solve solve: invar_preserve simp: pE_fin')
      apply auto
      apply (refine_vcg invar_rel_push)
      done
  qed

end

subsection "Consequences of Invariant when Finished"
context fr_graph
begin
  lemma fin_outer_D_is_reachable:
    ― ‹When outer loop terminates, exactly the reachable nodes are finished›
    assumes INV: "outer_invar {} D"
    shows "D = E⇧*``V0"
  proof -
    from INV interpret outer_invar_loc E V0 "{}" D unfolding outer_invar_def by auto

    from it_done rtrancl_reachable_induct[OF order_refl D_closed] D_reachable
    show ?thesis by auto
  qed

end

section ‹Refinement to Gabow's Data Structure›

text ‹
  The implementation due to Gabow \cite{Gabow2000} represents a path as
  a stack ‹S› of single nodes, and a stack ‹B› that contains the
  boundaries of the collapsed segments. Moreover, a map ‹I› maps nodes
  to their stack indices, or SCC index once they are done.

  As we use a tail-recursive formulation, we use another stack 
  ‹P :: ('v × 'v list) list› to represent the pending edges.
›

subsection ‹Preliminaries›
primrec find_max_nat :: "nat ⇒ (nat⇒bool) ⇒ nat" 
  ― ‹Find the maximum number below an upper bound for which a predicate holds›
  where
  "find_max_nat 0 _ = 0"
| "find_max_nat (Suc n) P = (if (P n) then n else find_max_nat n P)"

lemma find_max_nat_correct: 
  "⟦P 0; 0<u⟧ ⟹ find_max_nat u P = Max {i. i<u ∧ P i}"
  apply (induction u)
  apply auto

  apply (rule Max_eqI[THEN sym])
  apply auto [3]
  
  apply (case_tac u)
  apply simp
  apply clarsimp
  by (metis less_SucI less_antisym)

lemma find_max_nat_param[param]:
  assumes "(n,n')∈nat_rel"
  assumes "⋀j j'. ⟦(j,j')∈nat_rel; j'<n'⟧ ⟹ (P j,P' j')∈bool_rel"
  shows "(find_max_nat n P,find_max_nat n' P') ∈ nat_rel"
  using assms
  by (induction n arbitrary: n') auto

context begin interpretation autoref_syn .
  lemma find_max_nat_autoref[autoref_rules]:
    assumes "(n,n')∈nat_rel"
    assumes "⋀j j'. ⟦(j,j')∈nat_rel; j'<n'⟧ ⟹ (P j,P'$j')∈bool_rel"
    shows "(find_max_nat n P,
        (OP find_max_nat ::: nat_rel → (nat_rel→bool_rel) → nat_rel) $n'$P'
      ) ∈ nat_rel"
    using find_max_nat_param[OF assms]
    by simp

end

subsection ‹Gabow's Datastructure›

subsubsection ‹Definition and Invariant›
datatype node_state = STACK (val: nat) | DONE (scc: nat)

definition "DONE0 = DONE 0"

type_synonym 'v oGS = "'v ⇀ node_state"

definition oGS_α :: "'v oGS ⇒ 'v set" where "oGS_α I ≡ {v. ∃ i. I v = Some (DONE i)}"

locale oGS_invar = fr_graph +
  fixes I :: "'v oGS"
  assumes I_no_stack: "I v ≠ Some (STACK j)"

definition "edges_of_succs v0 succs = (map (Pair v0) succs)"

lemma edges_of_succs_append: "edges_of_succs v0 (succs1 @ succs2) = edges_of_succs v0 succs1 @ edges_of_succs v0 succs2"
  apply(auto simp: edges_of_succs_def)
  done


type_synonym 'a GS 
  = "'a list × nat list × ('a ⇀ node_state) × ('a × 'a list) list"
locale GS_defs = fr_graph_defs E V0 for E and V0 :: "'a set" +
  fixes SBIP :: "'a GS"
begin
  definition "S ≡ (λ(S,B,I,P). S) SBIP"
  definition "B ≡ (λ(S,B,I,P). B) SBIP"
  definition "I ≡ (λ(S,B,I,P). I) SBIP"
  definition "P ≡ (λ(S,B,I,P). P) SBIP"

  definition seg_start :: "nat ⇒ nat" ― ‹Start index of segment, inclusive›
    where "seg_start i ≡ B!i" 

  definition seg_end :: "nat ⇒ nat"  ― ‹End index of segment, exclusive›
    where "seg_end i ≡ if i+1 = length B then length S else B!(i+1)"

  definition seg :: "nat ⇒ 'a set" ― ‹Collapsed set at index›
    where "seg i ≡ {S!j | j. seg_start i ≤ j ∧ j < seg_end i }"

  definition "p_α ≡ map seg [0..<length B]" ― ‹Collapsed path›

  definition "D_α ≡ {v. ∃ i. I v = Some (DONE i)}" ― ‹Done nodes›

  definition "pE_α = mset (concat (map (λ(u,I). edges_of_succs u I) P))" ― ‹Pending edges›

  lemma set_mset_pE_α: "set_mset (pE_α) = { (u,v) . ∃I. (u,I)∈set P ∧ v∈set I }"
    unfolding pE_α_def edges_of_succs_def
    by auto

  definition "α ≡ (p_α,D_α,pE_α)" ― ‹Abstract state›

  lemma D_α_alt_def:  "D_α = oGS_α I" unfolding D_α_def oGS_α_def by simp

end

lemma GS_sel_simps[simp]:
  "GS_defs.S (S,B,I,P) = S"
  "GS_defs.B (S,B,I,P) = B"
  "GS_defs.I (S,B,I,P) = I"
  "GS_defs.P (S,B,I,P) = P"
  unfolding GS_defs.S_def GS_defs.B_def GS_defs.I_def GS_defs.P_def
  by auto


lemma GS_sel_id: "s = (GS_defs.S s, GS_defs.B s, GS_defs.I s, GS_defs.P s)"
  unfolding GS_defs.S_def GS_defs.B_def GS_defs.I_def GS_defs.P_def
  by(auto split: prod.split)

lemma GS_selI:
  "x = (S,B,I,P) ⟹ GS_defs.S x = S"
  "x = (S,B,I,P) ⟹ GS_defs.B x = B"
  "x = (S,B,I,P) ⟹ GS_defs.I x = I"
  "x = (S,B,I,P) ⟹ GS_defs.P x = P"
  unfolding GS_defs.S_def GS_defs.B_def GS_defs.I_def GS_defs.P_def
  by auto
  

context GS_defs begin
  lemma seg_start_indep[simp]: "GS_defs.seg_start (S',B,I',P') = seg_start"  
    unfolding GS_defs.seg_start_def[abs_def] by (auto)
  lemma seg_end_indep[simp]: "GS_defs.seg_end (S,B,I',P') = seg_end"  
    unfolding GS_defs.seg_end_def[abs_def] by auto
  lemma seg_indep[simp]: "GS_defs.seg (S,B,I',P') = seg"  
    unfolding GS_defs.seg_def[abs_def] by auto
  lemma p_α_indep[simp]: "GS_defs.p_α (S,B,I',P') = p_α"
    unfolding GS_defs.p_α_def by auto

  lemma D_α_indep[simp]: "GS_defs.D_α (S',B',I,P') = D_α"
    unfolding GS_defs.D_α_def by auto

  lemma pE_α_indep[simp]: "GS_defs.pE_α (S',B',I',P) = pE_α" 
    unfolding GS_defs.pE_α_def by auto

  definition find_seg ― ‹Abs-path index for stack index›
    where "find_seg j ≡ Max {i. i<length B ∧ B!i≤j}"

  definition S_idx_of ― ‹Stack index for node›
    where "S_idx_of v ≡ val (the (I v))"

  lemma S_idx_of_indep[simp]: "GS_defs.S_idx_of (S', B', I, P') = S_idx_of"
    unfolding GS_defs.S_idx_of_def by simp

  lemma p_α_B_empty: "p_α ≠ [] ⟷ B ≠ []"
    unfolding p_α_def
    by simp

  lemma seg_start_last: "B ≠ [] ⟹ seg_start (length B - 1) = last B"
    unfolding seg_start_def
    apply(auto simp: last_conv_nth)
    done

  lemma seg_end_last: "B ≠ [] ⟹ seg_end (length B - 1) = length S"
    unfolding seg_end_def
    by simp

  lemma S_idx_of_upd[simp]: "GS_defs.S_idx_of (S', B', I(v ↦ STACK n), P') = (S_idx_of(v := n))"
    unfolding GS_defs.S_idx_of_def by auto

end

locale GS = GS_defs + fr_graph 

locale GS_invar = GS +
  
  assumes B_in_bound: "set B ⊆ {0..<length S}"
  assumes B_sorted: "sorted B"
  assumes B_distinct: "distinct B"
  assumes B0: "S≠[] ⟹ B≠[] ∧ B!0=0"
  assumes S_distinct: "distinct S"

  assumes I_consistent: "(I v = Some (STACK j)) ⟷ (j<length S ∧ v = S!j)"
  
  assumes P_sorted: "sorted (map (S_idx_of o fst) P)"
  assumes P_bound: "set P ⊆ set S×Collect ((≠) [])"
  assumes P_distinct: "distinct (map fst P)"

  assumes S_subset_nodes: "set S ⊆ (E⇧* `` V0)"
begin
  lemma locale_this: "GS_invar E V0 SBIP" by unfold_locales
  

  lemma S_length_nodes: "length S ≤ card (E⇧* `` V0)"
    by (metis S_distinct S_subset_nodes card_mono distinct_card finite_reachableE_V0)

  lemma B_length_nodes: "length B ≤ card (E⇧* `` V0)"
    using distinct_card[OF B_distinct, symmetric] card_mono[OF _  B_in_bound] S_length_nodes
    by auto

  lemma P_length_nodes: "length P ≤ card (E⇧* `` V0)"
  proof -
    have "length P = length (map fst P)" by simp
    also have "length (map fst P) = card (fst ` set P)" using distinct_card[OF P_distinct, symmetric] by simp
    also have "… ≤ card (set S)" using P_bound
      by (fastforce intro: card_mono)
    also have "... = length S" using distinct_card[OF S_distinct] .
    also have "... ≤ card (E⇧* `` V0)" using S_length_nodes .
    finally show ?thesis .
  qed



end





context fr_graph begin

definition "oGS_rel ≡ br oGS_α (oGS_invar E V0)"
lemma oGS_rel_sv[intro!,simp,relator_props]: "single_valued oGS_rel"
  unfolding oGS_rel_def by auto

definition GS_rel :: "('v GS × 'v abs_state) set"
  where "GS_rel ≡ { (c,(p,D,pE,vE)) . (c,(p,D,pE)) ∈ br GS_defs.α (GS_invar E V0) }"
  
end

context GS_invar
begin
  lemma empty_eq: "S=[] ⟷ B=[]"
    using B_in_bound B0 by auto

  lemma B_in_bound': "i<length B ⟹ B!i < length S"
    using B_in_bound nth_mem by fastforce

  lemma seg_start_bound:
    assumes A: "i<length B" shows "seg_start i < length S"
    using B_in_bound nth_mem[OF A] unfolding seg_start_def by auto

  lemma seg_end_bound:
    assumes A: "i<length B" shows "seg_end i ≤ length S"
  proof (cases "i+1=length B")
    case True thus ?thesis by (simp add: seg_end_def)
  next
    case False with A have "i+1<length B" by simp
    from nth_mem[OF this] B_in_bound have " B ! (i + 1) < length S" by auto
    thus ?thesis using False by (simp add: seg_end_def)
  qed

  lemma seg_start_less_end: "i<length B ⟹ seg_start i < seg_end i"
    unfolding seg_start_def seg_end_def
    using B_in_bound' distinct_sorted_mono[OF B_sorted B_distinct]
    by auto

  lemma seg_end_less_start: "⟦i<j; j<length B⟧ ⟹ seg_end i ≤ seg_start j"
    unfolding seg_start_def seg_end_def
    by (auto simp: distinct_sorted_mono_iff[OF B_distinct B_sorted])

  lemma find_seg_bounds:
    assumes A: "j<length S"
    shows "seg_start (find_seg j) ≤ j" 
    and "j < seg_end (find_seg j)" 
    and "find_seg j < length B"
  proof -
    let ?M = "{i. i<length B ∧ B!i≤j}"
    from A have [simp]: "B≠[]" using empty_eq by (cases S) auto
    have NE: "?M≠{}" using A B0 by (cases B) auto

    have F: "finite ?M" by auto
    
    from Max_in[OF F NE]
    have LEN: "find_seg j < length B" and LB: "B!find_seg j ≤ j"
      unfolding find_seg_def
      by auto

    thus "find_seg j < length B" by -
    
    from LB show LB': "seg_start (find_seg j) ≤ j"
      unfolding seg_start_def by simp

    moreover show UB': "j < seg_end (find_seg j)"
      unfolding seg_end_def 
    proof (split if_split, intro impI conjI)
      show "j<length S" using A .
      
      assume "find_seg j + 1 ≠ length B" 
      with LEN have P1: "find_seg j + 1 < length B" by simp

      show "j < B ! (find_seg j + 1)"
      proof (rule ccontr, simp only: linorder_not_less)
        assume P2: "B ! (find_seg j + 1) ≤ j"
        with P1 Max_ge[OF F, of "find_seg j + 1", folded find_seg_def]
        show False by simp
      qed
    qed
  qed
    
  lemma find_seg_correct:
    assumes A: "j<length S"
    shows "S!j ∈ seg (find_seg j)" and "find_seg j < length B"
    using find_seg_bounds[OF A]
      unfolding seg_def by auto

  lemma set_p_α_is_set_S:
    "⋃(set p_α) = set S"
    apply rule
    unfolding p_α_def seg_def[abs_def]
    using seg_end_bound apply fastforce []

    apply (auto simp: in_set_conv_nth)

    using find_seg_bounds
    apply (fastforce simp: in_set_conv_nth)
    done

  lemma last_p_α_alt_def: "p_α ≠ [] ⟹ last p_α = {S ! j |j. last B ≤ j ∧ j < length S}"
    unfolding p_α_def seg_def seg_start_def seg_end_def
    apply(simp add: last_map last_conv_nth)
    done

  lemma last_p_α_drop_B: "p_α ≠ [] ⟹ last p_α = set (drop (last B) S)" 
    using set_drop_conv last_p_α_alt_def 
    by fast

  lemma S_idx_uniq: 
    "⟦i<length S; j<length S⟧ ⟹ S!i=S!j ⟷ i=j"
    using S_distinct
    by (simp add: nth_eq_iff_index_eq)

  lemma S_idx_of_correct: 
    assumes A: "v∈⋃(set p_α)"
    shows "S_idx_of v < length S" and "S!S_idx_of v = v"
  proof -
    from A have "v∈set S" by (simp add: set_p_α_is_set_S)
    then obtain j where G1: "j<length S" "v=S!j" by (auto simp: in_set_conv_nth)
    with I_consistent have "I v = Some (STACK j)" by simp
    hence "S_idx_of v = j" by (simp add: S_idx_of_def)
    with G1 show "S_idx_of v < length S" and "S!S_idx_of v = v" by simp_all
  qed

  lemma p_α_disjoint_sym: 
    shows "∀i j v. i<length p_α ∧ j<length p_α ∧ v∈p_α!i ∧ v∈p_α!j ⟶ i=j"
  proof (intro allI impI, elim conjE)
    fix i j v
    assume A: "i < length p_α" "j < length p_α" "v ∈ p_α ! i" "v ∈ p_α ! j"
    from A have LI: "i<length B" and LJ: "j<length B" by (simp_all add: p_α_def)

    from A have B1: "seg_start j < seg_end i" and B2: "seg_start i < seg_end j"
      unfolding p_α_def seg_def[abs_def]
      apply clarsimp_all
      apply (subst (asm) S_idx_uniq)
      apply (metis dual_order.strict_trans1 seg_end_bound)
      apply (metis dual_order.strict_trans1 seg_end_bound)
      apply simp
      apply (subst (asm) S_idx_uniq)
      apply (metis dual_order.strict_trans1 seg_end_bound)
      apply (metis dual_order.strict_trans1 seg_end_bound)
      apply simp
      done

    from B1 have B1: "(B!j < B!Suc i ∧ Suc i < length B) ∨ i=length B - 1"
      using LI unfolding seg_start_def seg_end_def by (auto split: if_split_asm)

    from B2 have B2: "(B!i < B!Suc j ∧ Suc j < length B) ∨ j=length B - 1"
      using LJ unfolding seg_start_def seg_end_def by (auto split: if_split_asm)

    from B1 have B1: "j<Suc i ∨ i=length B - 1"
      using LI LJ distinct_sorted_strict_mono_iff[OF B_distinct B_sorted]
      by auto

    from B2 have B2: "i<Suc j ∨ j=length B - 1"
      using LI LJ distinct_sorted_strict_mono_iff[OF B_distinct B_sorted]
      by auto

    from B1 B2 show "i=j"
      using LI LJ
      by auto
  qed

end


subsection ‹Refinement of the Operations›

  definition GS_initial_impl :: "'a oGS ⇒ 'a ⇒ 'a list ⇒ 'a GS" where
  "GS_initial_impl I v0 succs ≡ (
    [v0],
    [0],
    I(v0↦(STACK 0)),
    if succs=[] then [] else [(v0,succs)])"

  definition mark_as_done 
    where "mark_as_done S I l u i ≡ do {
    (_,I)←WHILET 
      (λ(l,I). l<u) 
      (λ(l,I). do { ASSERT (l<length S); RETURN (Suc l,I(S!l ↦ DONE i))}) 
      (l,I);
    RETURN I
  }"
  sepref_register mark_as_done :: "'a list ⇒ (('a, node_state) i_map) ⇒ nat ⇒ nat ⇒ nat ⇒ (('a, node_state) i_map) nres"

  definition open_GS :: "'a GS ⇒ 'a GS" where "open_GS s = (case s of (S,B,I,P) ⇒ (S,B,I,P))"
  sepref_register open_GS :: "'a list × nat list × ('a ⇒ node_state option) × ('a × 'a list) list
     ⇒ 'a list × nat list × (('a, node_state) i_map) × ('a × 'a list) list"

  definition close_GS :: "'a list ⇒ nat list ⇒ ('a ⇀ node_state) ⇒ ('a × 'a list) list ⇒ 'a GS" 
    where "close_GS S B I P = (S,B,I,P)"
  sepref_register close_GS :: "'a list ⇒ nat list ⇒ (('a, node_state) i_map) ⇒ ('a × 'a list) list
     ⇒ 'a list × nat list × ('a ⇒ node_state option) × ('a × 'a list) list"

context GS_defs
begin
  definition "push_impl_core v succs ≡ let 
    j = length S;
    S = S@[v];
    B = B@[j];
    I = I(v ↦ STACK j);
    P = (if succs=[] then P else P@[(v,succs)])
  in
    (S,B,I,P)
  "

  definition "push_impl v succs ≡ 
    do {
      ASSERT(length S < card(E⇧*``V0));
      ASSERT(length B < card(E⇧*``V0));
      ASSERT(length P < card(E⇧*``V0));
      RETURN (push_impl_core v succs)
    }"

  definition mark_as_done_abs where
    "⋀l u I i. mark_as_done_abs l u I i
    ≡ (λv. if v∈{S!j | j. l≤j ∧ j<u} then Some (DONE i) else I v)"

  lemma mark_as_done_aux:
    fixes I l u i
    shows "⟦l<u; u≤length S⟧ ⟹ mark_as_done S I l u i
    ≤ SPEC (λr. r = mark_as_done_abs l u I i)"
    unfolding mark_as_done_def mark_as_done_abs_def
    apply (refine_rcg 
      WHILET_rule[where 
        I="λ(l',I'). 
          (I' = (λv. if v∈{S!j | j. l≤j ∧ j<l'} then Some (DONE i) else I v))
          ∧ l≤l' ∧ l'≤u"
        and R="measure (λ(l',_). u-l')" 
      ]
      refine_vcg)
    
    apply (auto del: ext intro!: ext simp: less_Suc_eq)
    done    

  definition "pop_impl i ≡ 
    do {
      ASSERT (length B ≥ 1);
      let lsi = length B - 1;
      ASSERT (lsi<length B);
      let l = (seg_start lsi);
      let u = (seg_end lsi);
      I ← mark_as_done S I l u i;
      ASSERT (B≠[]);
      S ← mop_list_take (last B) S;
      ASSERT (B≠[]);
      let B = butlast B;
      RETURN (S,B,I,P)
    }"
    
    

  definition "sel_rem_last ≡ 
    if P=[] then 
      RETURN (None,(S,B,I,P))
    else do {
      let ((v,succs), P') = op_list_pop_last P;
      ASSERT (∃j. I v = Some (STACK j));
      ASSERT (length B ≥ 1);
      if S_idx_of v ≥ seg_start (length B - 1) then do {
        ASSERT (succs≠[]);
        (w, succs) ← mop_list_pop_last succs;
        let P = (if succs=[] then P' else op_list_append P' (v,succs));
        RETURN (Some w,(S,B,I,P))
      } else RETURN (None,(S,B,I,P))
    }"


  definition "find_seg_impl' j ≡ find_max_nat (length B) (λi. B!i≤j)"

  definition "find_seg_impl j = do {
    ASSERT(length B ≥ 1);
    (i)←WHILEIT
      (λi. i < length B ∧ (∀k . i < k & k < length B ⟶ B!k > j)) 
      (λi. B!i > j) 
      (λi. do { ASSERT (i ≥ 1); RETURN (i - 1)}) 
      (length B - 1);
    RETURN i
  }"


  lemma(in GS_invar) "S ≠ [] ⟹ {i. i < length B ∧ B ! i ≤ j} ≠ {}"
    using B0 by force

  lemma s_max_j_in_X:
    assumes SIN: "X ≠ []"
        and SORT: "sorted X"
        and JBOUND: "j ≥ X ! s"
        and SLEN: "s < length X" 
        and SSMALL: "∀k. s < k ∧ k < length X ⟶ j < X ! k"
      shows "s = Max {i. i < length X ∧ X ! i ≤ j}"
  proof -
    define s2 where "s2 ≡ Max {i. i < length X ∧ X ! i ≤ j}"
    have FIN:  "finite {i. i < length X ∧ X ! i ≤ j}" by fast
    hence NEMP: "{i. i < length X ∧ X ! i ≤ j} ≠ {}" using SIN SLEN JBOUND by fast
    have S2LEN: "s2 < length X" using s2_def FIN NEMP by force
    have L: "s2 ≤ s"
    proof(rule ccontr)
      assume "¬ s2 ≤ s"
      hence "s2 > s" by force
      moreover have "s2 < length X" using s2_def FIN NEMP by force
      ultimately have "j < X ! s2" using SSMALL by blast
      thus False using s2_def eq_Max_iff[OF FIN NEMP, of s2] by force
    qed

    moreover have "s ≤ s2" using Max_ge[OF FIN] s2_def by (simp add: JBOUND SLEN)
    ultimately show ?thesis using s2_def by fastforce
  qed


  lemma (in GS_invar) find_seg_impl_aux:
    fixes j
    shows "j<length S ⟹ find_seg_impl j 
    ≤ SPEC (λr. r = find_seg j)"
    unfolding find_seg_impl_def find_seg_def
    apply (refine_rcg 
      WHILEIT_rule[where R="measure (λi. i)" 
      ]
      refine_vcg)
    
    apply (auto simp: B0) 
    subgoal for s 
      apply(cases "s = 0")
      apply (auto simp: B0) 
      done
    subgoal for s k apply(cases "s = k")
      apply fast
      apply simp
      done          
    apply(rule s_max_j_in_X)
    apply(auto simp: B_sorted)
    done
    

  definition "idx_of_impl v ≡ do {
      ASSERT (∃ j. I v = Some (STACK j));
      let j = S_idx_of v;
      ASSERT (j<length S);
      i ← find_seg_impl j;
      RETURN i
    }"


  definition "collapse_impl v ≡ 
    do { 
      i←idx_of_impl v;
      ASSERT (i+1 ≤ length B);
      let B = take (i+1) B;
      RETURN (S,B,I,P)
    }"

end

lemma (in fr_graph) GS_initial_correct: 
  assumes REL: "(I,D)∈oGS_rel"
  assumes A: "v0∉D"
  assumes REACH: "v0 ∈ V0"
  shows "GS_defs.α (GS_initial_impl I v0 succs) = ([{v0}],D,mset (edges_of_succs v0 succs))" (is ?G1)
  and "GS_invar E V0 (GS_initial_impl I v0 succs)" (is ?G2)
proof -
  from REL have [simp]: "D = oGS_α I" and I: "oGS_invar E V0 I"
    by (simp_all add: oGS_rel_def br_def)

  from I have [simp]: "⋀j v. I v ≠ Some (STACK j)"
    by (simp add: oGS_invar_def fr_graph_axioms oGS_invar_axioms_def)

  show ?G1
    unfolding GS_defs.α_def GS_initial_impl_def edges_of_succs_def
    apply (simp split del: if_split) apply (intro conjI)

    unfolding GS_defs.p_α_def GS_defs.seg_def[abs_def] GS_defs.seg_start_def GS_defs.seg_end_def
    apply (auto) []

    using A unfolding GS_defs.D_α_def apply (auto simp: oGS_α_def) []

    unfolding GS_defs.pE_α_def edges_of_succs_def apply auto []
    done

  show ?G2
    unfolding GS_initial_impl_def
    apply unfold_locales
    apply (auto simp: REACH)
    done
qed

context GS_invar
begin


  lemma push_impl_core_correct:
    assumes A: "v∉⋃(set p_α)" and B: "v∉D_α" and REACH: "v ∈ E⇧* `` V0"
    shows "GS_defs.α (push_impl_core v succs) = (p_α@[{v}],D_α,pE_α + mset (edges_of_succs v succs))" 
      (is ?G1)
    and "GS_invar E V0 (push_impl_core v succs)" (is ?G2)
  proof -

    note [simp] = Let_def

    have A1: "GS_defs.D_α (push_impl_core v succs) = D_α"
      using B
      by (auto simp: push_impl_core_def GS_defs.D_α_def)

    have iexI: "⋀a b j P. ⟦a!j = b!j; P j⟧ ⟹ ∃j'. a!j = b!j' ∧ P j'"
      by blast

    have A2: "GS_defs.p_α (push_impl_core v succs) = p_α @ [{v}]"
      unfolding push_impl_core_def GS_defs.p_α_def GS_defs.seg_def[abs_def] 
        GS_defs.seg_start_def GS_defs.seg_end_def
      apply (clarsimp split del: if_split)

      apply clarsimp
      apply safe
      apply (((rule iexI)?, 
        (auto  
          simp: nth_append nat_in_between_eq 
          dest: order.strict_trans[OF _ B_in_bound']
        )) []
      ) +
      done

    have iexI2: "⋀j I Q. ⟦(j,I)∈set P; (j,I)∈set P ⟹ Q j⟧ ⟹ ∃j. Q j"
      by blast

    have A3: "GS_defs.pE_α (push_impl_core v succs) = pE_α + mset (edges_of_succs v succs)"
      unfolding push_impl_core_def GS_defs.pE_α_def edges_of_succs_def
      apply (force simp: nth_append elim!: iexI2)
      done

    show ?G1
      unfolding GS_defs.α_def
      by (simp add: A1 A2 A3)

    show ?G2
      apply unfold_locales
      unfolding push_impl_core_def
      apply simp_all

      using B_in_bound B_sorted B_distinct apply (auto simp: sorted_append) [3]
      using B_in_bound B0 apply (cases S) apply (auto simp: nth_append) [2]

      using S_distinct A apply (simp add: set_p_α_is_set_S)

      using A I_consistent 
      apply (auto simp: nth_append set_p_α_is_set_S  split: if_split_asm) []

      apply(simp flip: map_map)
      apply(subgoal_tac "v ∉ set (map fst P)")
      using map_fun_upd[of v "(map fst P)" S_idx_of "length S"] apply(simp add: map_fun_upd[of v "(map fst P)" S_idx_of "length S"] del: map_map)
      apply rule
      apply rule
      using P_sorted apply force
      
      apply rule
      apply simp
      apply(subgoal_tac "∀x∈set (map (S_idx_of o fst) P). x ≤ length S")
      using sorted_append_bigger[OF P_sorted] apply blast
      apply simp
      using S_idx_of_correct(1)[of "fst _"] P_bound set_p_α_is_set_S 
      apply auto[]
      apply force

      using A set_p_α_is_set_S P_bound apply auto[2]
      apply rule
      using P_distinct apply simp
      using A set_p_α_is_set_S P_bound P_distinct apply auto[]
      using REACH S_subset_nodes apply auto

      done
  qed

  lemma no_last_out_P_aux':
    assumes NE: "p_α≠[]" and NS: "set_mset pE_α ∩ last p_α × UNIV = {}"
    shows "set P ⊆ set (take (last B) S) × (Collect ((≠) []))"
  proof
    fix x
    assume XP: "x ∈ set P"
    moreover then obtain v I where X_DEF: "x = (v,I)" by fastforce
    ultimately have VS: "v ∈ set S" and IC: "I ∈ (Collect ((≠) []))" using P_bound by blast+
    moreover then obtain w where "w ∈ set I" by blast
    ultimately have "(v,w) ∈# pE_α" unfolding pE_α_def edges_of_succs_def using XP X_DEF 
      by auto
    hence "v ∉ last p_α" using NE NS by blast
    hence "v ∉ set (drop (last B) S)" using last_p_α_drop_B[OF NE] by blast
    moreover have "v ∈ set (take (last B) S) ∪ set (drop (last B) S)" using VS append_take_drop_id
      by (simp add: set_union_code)
    ultimately have "v ∈ set (take (last B) S)" by blast
    thus "x ∈ set (take (last B) S) × {y. [] ≠ y}" using IC X_DEF by blast
  qed


  lemma map_update_snd_keeps_fst: "P ! n = (a,b) ⟹ map fst (P[n := (a, b')]) = map fst P"
    by (metis fst_conv list_update_id map_update)


  lemma no_last_out_P_aux:
    assumes NE: "p_α≠[]" and NS: "set_mset pE_α ∩ last p_α × UNIV = {}"
    shows "set (map (S_idx_of o fst) P) ⊆ {0..<last B}"
  proof -
    {
      fix v I
      assume jII: "(v,I)∈set P"
        and JL: "last B ≤ S_idx_of v"
      with P_bound have VPA: "v ∈ ⋃ (set p_α)" and INE: "I≠[]" by(auto simp: set_p_α_is_set_S)
      hence JU: "S_idx_of v < length S" 
        using S_idx_of_correct(1) by blast
      with JL JU have "S!(S_idx_of v) ∈ last p_α"
        using NE
        unfolding p_α_def 
        apply (auto 
          simp: last_map seg_def seg_start_def seg_end_def last_conv_nth) 
        done
      hence "v ∈ last p_α" using S_idx_of_correct(2)[OF VPA] by auto
      moreover from jII have "set (edges_of_succs v I) ⊆ set_mset pE_α" unfolding pE_α_def
        by auto
      moreover note INE NS
      ultimately have False unfolding edges_of_succs_def by auto
    } thus ?thesis by fastforce
  qed


  lemma sorted_after_pop:
  fixes i
  assumes BNE: "B ≠ []"
  assumes PS: "set P ⊆ set (take (last B) S) × {y. [] ≠ y}"
  defines "S'≡ take (last B) S"
  defines "B'≡ butlast B"
  defines "I' ≡ mark_as_done_abs (seg_start (length B - Suc 0)) (seg_end (length B - Suc 0)) I i"
    shows "sorted (map (GS_defs.S_idx_of (S', B', I', P) ∘ fst) P)"
  proof (cases P)
    case Nil
    then show ?thesis by simp
  next
    case (Cons a x)

    {
      fix p 
      assume P_MEM: "p ∈ set (map fst P)"
      hence P_MEM2: "p ∈ set (take (last B) S)" using PS by auto
      then obtain j where "j = index (take (last B) S) p" and "j < last B" using nth_index by simp
      hence "p ∉ {S ! j |j. last B ≤ j ∧ j < length S}" using P_distinct
        by (smt (verit) S_distinct P_MEM2 index_nth_id index_take mem_Collect_eq)
      hence EQ: "I' p = I p" unfolding I'_def mark_as_done_abs_def seg_start_last[OF BNE, simplified] seg_end_last[OF BNE, simplified] by argo
    } note I'_to_I = this
    hence "∀p2 ∈ set (map fst P). I' p2 = I p2" by blast
    hence "map (GS_defs.S_idx_of (S', B', I', P) ∘ fst) P = map (GS_defs.S_idx_of (S', B', I, P) ∘ fst) P" unfolding GS_defs.S_idx_of_def GS_defs.I_def by force
    also have "... = map (S_idx_of ∘ fst) P" unfolding S_idx_of_indep by simp
    finally show ?thesis using P_sorted by presburger
  qed

  lemma pop_correct:
    assumes NE: "p_α≠[]" and NS: "set_mset pE_α ∩ last p_α × UNIV = {}"
    shows "pop_impl i
      ≤ ⇓GS_rel (SPEC (λr. r=(butlast p_α, D_α ∪ last p_α, pE_α, vE)))"
  proof -
    have iexI: "⋀a b j P. ⟦a!j = b!j; P j⟧ ⟹ ∃j'. a!j = b!j' ∧ P j'"
      by blast
    
    have [simp]: "⋀n. n - Suc 0 ≠ n ⟷ n≠0" by auto

    from NE have BNE: "B≠[]"
      unfolding p_α_def by auto

    {
      fix i j
      assume B: "j<B!i" and A: "i<length B"
      note B
      also from sorted_nth_mono[OF B_sorted, of i "length B - 1"] A 
      have "B!i ≤ last B"
        by (simp add: last_conv_nth)
      finally have "j < last B" .
      hence "take (last B) S ! j = S ! j" 
        and "take (B!(length B - Suc 0)) S !j = S!j"
        by (simp_all add: last_conv_nth BNE)
    } note AUX1=this

    {
      fix v j
      have "(mark_as_done_abs 
              (seg_start (length B - Suc 0))
              (seg_end (length B - Suc 0)) I i v = Some (STACK j)) 
        ⟷ (j < length S ∧ j < last B ∧ v = take (last B) S ! j)"
        apply (simp add: mark_as_done_abs_def)
        apply safe []
        using I_consistent
        apply (clarsimp_all
          simp: seg_start_def seg_end_def last_conv_nth BNE
          simp: S_idx_uniq)

        apply (force)
        apply (subst nth_take)
        apply force
        apply force
        done
    } note AUX2 = this

    define ci where "ci = ( 
      take (last B) S, 
      butlast B,
      mark_as_done_abs 
        (seg_start (length B - Suc 0)) (seg_end (length B - Suc 0)) I i,
      P)"

    have ABS: "GS_defs.α ci = (butlast p_α, D_α ∪ last p_α, pE_α)"
      apply (simp add: GS_defs.α_def ci_def)
      apply (intro conjI)
      apply (auto  
        simp del: map_butlast
        simp add: map_butlast[symmetric] butlast_upt
        simp add: GS_defs.p_α_def GS_defs.seg_def[abs_def] GS_defs.seg_start_def GS_defs.seg_end_def
        simp: nth_butlast last_conv_nth nth_take AUX1
        cong: if_cong
        intro!: iexI
        dest: order.strict_trans[OF _ B_in_bound']
      ) []

      apply (auto 
        simp: GS_defs.D_α_def p_α_def last_map BNE seg_def mark_as_done_abs_def) []

      done

    have SUBP: "set P ⊆ set (take (last B) S) × {y. [] ≠ y}"
      using no_last_out_P_aux'[OF NE NS] .

    have INV: "GS_invar E V0 ci"
      apply unfold_locales
      apply (simp_all add: ci_def)

      using B_in_bound B_sorted B_distinct 
      apply (cases B rule: rev_cases, simp) 
      apply (auto simp: sorted_append order.strict_iff_order) [] 

      using B_sorted BNE apply (auto simp: sorted_butlast) []

      using B_distinct BNE apply (auto simp: distinct_butlast) []

      using B0 apply (cases B rule: rev_cases, simp add: BNE) 
      apply (auto simp: nth_append split: if_split_asm) []
   
      using S_distinct apply (auto) []

      apply (rule AUX2)
      
      using sorted_after_pop[OF BNE SUBP] apply blast
      
      using no_last_out_P_aux'[OF NE NS] apply blast
      using P_distinct apply simp

      using S_subset_nodes
        by (meson set_take_subset subset_trans)
      

    show ?thesis
      unfolding pop_impl_def
      apply (refine_rcg 
        SPEC_refine refine_vcg order_trans[OF mark_as_done_aux])
      apply (simp_all add: BNE seg_start_less_end seg_end_bound)
      apply (fold ci_def)
      unfolding GS_rel_def
      apply (metis BNE B_in_bound' GS_defs.seg_start_def GS_defs.seg_start_last diff_less length_greater_0_conv linorder_not_less nat_le_linear zero_less_one)
      apply (simp_all add: ABS INV in_br_conv)
      done
  qed

  lemma node_state_rule[refine_vcg]: 
    "⟦ ⋀j. v=STACK j ⟹ f1 j ≤ SPEC Φ; ⋀i. v=DONE i ⟹ f2 i ≤ SPEC Φ⟧ 
    ⟹ (case v of STACK j ⇒ f1 j | DONE i ⇒ f2 i) ≤ SPEC Φ"
    by (auto split: node_state.split)

  lemma f_comp_fst: "f a = (f o fst) (a,b)" 
    by simp

  lemma "map f (x # xs) = f x # map f xs" 
    by simp

  lemma sel_rem_last_correct:
    assumes NE: "p_α≠[]"
    shows
    "sel_rem_last ≤ ⇓(Id ×⇩r GS_rel) (select_edge (p_α,D_α,pE_α,vE))"
  proof -
    from NE have BNE[simp]: "B≠[]" unfolding p_α_def by simp

    have INVAR: "sel_rem_last ≤ SPEC (GS_invar E V0 o snd)"
      unfolding sel_rem_last_def
      apply (refine_rcg refine_vcg)
      using locale_this apply (cases SBIP) 
      apply simp 
      apply simp

      using P_bound I_consistent
      apply (metis Misc.last_in_set in_set_conv_nth mem_Sigma_iff subset_iff)

      apply auto[1]
      using P_bound apply fastforce

      apply simp apply (intro impI conjI)

      apply (unfold_locales, simp_all) []
      using B_in_bound B_sorted B_distinct B0 S_distinct I_consistent 
      apply auto [6]

      using P_sorted apply (auto simp: map_butlast sorted_butlast)[]
      using P_bound apply (auto simp: butlast_subset) []
      using P_distinct apply (auto simp: map_butlast distinct_butlast)[]

      using S_subset_nodes apply blast

      apply (unfold_locales, simp_all) []
      using B_in_bound B_sorted B_distinct B0 S_distinct I_consistent 
      apply auto [6]

      apply(subgoal_tac "sorted (map (S_idx_of ∘ fst) (butlast P @ [last P]))") 
      apply fastforce
      apply (metis append_butlast_last_id P_sorted)
      
      using P_bound apply (auto simp: butlast_subset) []
      subgoal for a x1 x2 aa apply (subgoal_tac "distinct (map fst (butlast P @ [(x1,x2)]))") 
        apply simp
        by (metis append_butlast_last_id P_distinct)
      using S_subset_nodes apply blast


      using locale_this apply (cases SBIP) apply simp
      done
    

    {
      assume NS: "set_mset pE_α∩last p_α×UNIV = {}"
      hence "sel_rem_last 
        ≤ SPEC (λr. case r of (None,SBIP') ⇒ SBIP'=SBIP | _ ⇒ False)"
        unfolding sel_rem_last_def
        apply (refine_rcg refine_vcg)
        apply (cases SBIP)
        apply simp

        subgoal for a b v succs  
        apply(subgoal_tac "v ∈ set S")
        using I_consistent apply (metis in_set_conv_nth)
        using P_bound I_consistent unfolding op_list_pop_last_def by auto


        apply simp
        using P_bound apply (cases P rule: rev_cases, auto) []
        apply simp
        
        using no_last_out_P_aux[OF NE NS] 
        apply(subgoal_tac "S_idx_of (fst (last P)) < last B") 
        unfolding seg_start_def
        apply (auto simp: last_conv_nth) []
        apply force

        apply (cases SBIP)
        apply simp
        done
    } note SPEC_E = this
    
    {
      assume NON_EMPTY: "set_mset pE_α∩last p_α×UNIV ≠ {}"

      then obtain v succs P' where 
        EFMT: "P = P'@[(v,succs)]"
        unfolding pE_α_def
        by (cases P rule: rev_cases) auto
        
      with P_bound have VPA: "v ∈ ⋃ (set p_α)" and SNE: "succs≠[]" 
        by(auto simp: set_p_α_is_set_S)

      with P_bound have J_UPPER: "S_idx_of v<length S" 
        using S_idx_of_correct(1) by blast
      have J_LOWER: "seg_start (length B - Suc 0) ≤ S_idx_of v"
      proof (rule ccontr)
        assume "¬(seg_start (length B - Suc 0) ≤ S_idx_of v)"
        hence "S_idx_of v < seg_start (length B - 1)" by simp
        with EFMT P_sorted
        have P_bound': "set (map (S_idx_of ∘ fst) P) ⊆ {0..<seg_start (length B - 1)}"
          by (auto simp: sorted_append)
        have "set_mset pE_α ∩ last p_α×UNIV = {}"
        proof (rule ccontr)
          assume ASM: "set_mset pE_α ∩ last p_α × UNIV ≠ {}"
          then obtain v1 v2 where INB: "(v1,v2) ∈ set_mset pE_α ∩ last p_α × UNIV" by blast
          hence VPA1: "v1 ∈ fst ` (set P)" 
            unfolding pE_α_def edges_of_succs_def by auto
          hence "S_idx_of v1 < seg_start (length B - 1)" 
            unfolding edges_of_succs_def pE_α_def using P_bound' INB 
            by fastforce
          moreover have "last B ≤ S_idx_of v1"
          proof -
            from INB have "v1 ∈ {S ! j |j. last B ≤ j ∧ j < length S}" 
              using last_p_α_alt_def[OF NE] by blast
            then obtain j where JID: "v1 = S ! j" and LBJ: "last B ≤ j" and "j < length S" by blast
            hence "I v1 = Some (STACK j)" using I_consistent[of v1 j] by blast
            hence "S_idx_of v1 = j" unfolding S_idx_of_def by simp
            thus ?thesis using LBJ by blast
          qed
          ultimately show False unfolding seg_start_def by(simp add: last_conv_nth) 
        qed
        thus False using NON_EMPTY by simp
      qed

      from J_UPPER J_LOWER have SJL: "S!(S_idx_of v)∈last p_α" 
        unfolding p_α_def seg_def[abs_def] seg_end_def
        by (auto simp: last_map)

      from EFMT have SSS: "{S!(S_idx_of v)}×set succs⊆set_mset pE_α"
        unfolding pE_α_def edges_of_succs_def
        by (auto simp: S_idx_of_correct[OF VPA])


      {
        with SJL SSS SNE have G: "(v,last succs)∈set_mset pE_α ∩ last p_α×UNIV" by (auto simp: S_idx_of_correct[OF VPA])

        from SNE have SUCCS_ALT: "succs = butlast succs @ [last succs]"
          by simp
        
        {
          fix v' succs'
          assume "v' = v" "(v', succs') ∈ set P'"
          with P_distinct ‹(v', succs') ∈ set P'› EFMT have False by auto
        } note AUX3=this

        have G1: "GS_defs.pE_α (S,B,I,P' @ [(v, butlast succs)]) = pE_α - {#(v, last succs)#}"
        proof -
          from EFMT have "pE_α = GS_defs.pE_α (S,B,I,P' @ [(v, succs)])" 
            using pE_α_indep by auto
          show ?thesis apply (auto simp: GS_defs.pE_α_def)

          unfolding GS_defs.pE_α_def edges_of_succs_def using AUX3 EFMT
          apply(subst(asm) SUCCS_ALT)
          by simp
        qed

        {
          assume "butlast succs = []"
          hence "pE_α = GS_defs.pE_α (S,B,I,P' @ [(v, [last succs])])" 
            using pE_α_indep[unfolded EFMT] SUCCS_ALT by simp
          hence "GS_defs.pE_α (S,B,I,P') = pE_α - {#(v, last succs)#}"
            unfolding GS_defs.pE_α_def edges_of_succs_def by auto
        } note G2 = this
        
        note G G1 G2
      } note AUX3 = this

      have "sel_rem_last ≤ SPEC (λr. case r of 
        (Some v,SBIP') ⇒ ∃u. 
            (u,v)∈((set_mset pE_α)∩last p_α×UNIV) 
          ∧ GS_defs.α SBIP' = (p_α,D_α,pE_α-{#(u,v)#})
      | _ ⇒ False)"
        unfolding sel_rem_last_def
        apply (refine_rcg refine_vcg)

        using SNE apply (vc_solve simp: J_LOWER EFMT)
    
        apply(subgoal_tac "v ∈ set S")
        using I_consistent J_UPPER S_idx_of_correct(2) set_p_α_is_set_S apply auto[1]
        using EFMT P_bound apply fastforce 

        apply(rule conjI)

        subgoal for j
          apply(rule impI)
          apply(rule exI[where ?x=v])
          using AUX3(1) apply clarsimp
          apply(frule AUX3(3))
          apply (auto simp: GS_defs.α_def)
          done

        subgoal for j
          apply(rule impI)
          apply(rule exI[where ?x=v])
          using AUX3(1) apply clarsimp
          apply(auto simp: AUX3(2) GS_defs.α_def)
          done
        
        done

    } note SPEC_NE=this

    have SPEC: "sel_rem_last ≤ SPEC (λr. case r of 
        (None, SBIP') ⇒ SBIP' = SBIP ∧ (set_mset pE_α) ∩ last p_α × UNIV = {} ∧ GS_invar E V0 SBIP
      | (Some v, SBIP') ⇒ ∃u. (u, v) ∈ (set_mset pE_α) ∩ last p_α × UNIV 
                        ∧ GS_defs.α SBIP' = (p_α, D_α, pE_α - {#(u, v)#})
                        ∧ GS_invar E V0 SBIP'
    )"  
      using INVAR
      apply (cases "(set_mset pE_α) ∩ last p_α × UNIV = {}") 
      apply (frule SPEC_E)
      apply (auto split: option.splits simp: pw_le_iff; blast; fail)
      apply (frule SPEC_NE)
      apply (auto split: option.splits simp: pw_le_iff; blast; fail)
      done    
      
      
    have X1: "(∃y. (y=None ⟶ Φ y) ∧ (∀a b. y=Some (a,b) ⟶ Ψ y a b)) ⟷
      (Φ None ∨ (∃a b. Ψ (Some (a,b)) a b))" for Φ Ψ
      by auto
      

    show ?thesis
      apply (rule order_trans[OF SPEC])
      unfolding select_edge_def select_def 
      apply (simp 
        add: pw_le_iff refine_pw_simps prod_rel_sv 
        del: SELECT_pw
        split: option.splits prod.splits)
      apply (auto simp: in_br_conv GS_rel_def GS_defs.α_def)
      apply (metis option.inject prod.inject)
      done
  qed


  lemma find_seg_idx_of_correct:
    assumes A: "v∈⋃(set p_α)"
    shows "(find_seg (S_idx_of v)) = idx_of p_α v"
  proof -
    note S_idx_of_correct[OF A] idx_of_props[OF p_α_disjoint_sym A]
    from find_seg_correct[OF ‹S_idx_of v < length S›] have 
      "find_seg (S_idx_of v) < length p_α" 
      and "S!S_idx_of v ∈ p_α!find_seg (S_idx_of v)"
      unfolding p_α_def by auto
    from idx_of_uniq[OF p_α_disjoint_sym this] ‹S ! S_idx_of v = v› 
    show ?thesis by auto
  qed


  lemma idx_of_correct:
    assumes A: "v∈⋃(set p_α)"
    shows "idx_of_impl v ≤ SPEC (λx. x=idx_of p_α v ∧ x<length B)"
    using assms
    unfolding idx_of_impl_def
    apply (refine_rcg SPEC_refine refine_vcg order_trans[OF find_seg_impl_aux])
    apply (metis I_consistent S_idx_of_correct(1) S_idx_of_correct(2))
    apply (erule S_idx_of_correct)
    using find_seg_idx_of_correct apply blast
    using find_seg_correct(2) by blast

  lemma collapse_correct:
    assumes A: "v∈⋃(set p_α)"
    shows "collapse_impl v ≤⇓GS_rel (SPEC (λr. r=collapse v (p_α, D_α, pE_α, vE)))"
  proof -
    {
      fix i
      assume "i<length p_α"
      hence ILEN: "i<length B" by (simp add: p_α_def)

      let ?SBIP' = "(S, take (Suc i) B, I, P)"

      {
        have [simp]: "GS_defs.seg_start ?SBIP' i = seg_start i"
          by (simp add: GS_defs.seg_start_def)

        have [simp]: "GS_defs.seg_end ?SBIP' i = seg_end (length B - 1)"
          using ILEN by (simp add: GS_defs.seg_end_def min_absorb2)

        {
          fix j
          assume B: "seg_start i ≤ j" "j < seg_end (length B - Suc 0)"
          hence "j<length S" using ILEN seg_end_bound 
          proof -
            note B(2)
            also from ‹i<length B› have "(length B - Suc 0) < length B" by auto
            from seg_end_bound[OF this] 
            have "seg_end (length B - Suc 0) ≤ length S" .
            finally show ?thesis .
          qed

          have "i ≤ find_seg j ∧ find_seg j < length B 
            ∧ seg_start (find_seg j) ≤ j ∧ j < seg_end (find_seg j)" 
          proof (intro conjI)
            show "i≤find_seg j"
              by (metis le_trans not_less B(1) find_seg_bounds(2) 
                seg_end_less_start ILEN ‹j < length S›)
          qed (simp_all add: find_seg_bounds[OF ‹j<length S›])
        } note AUX1 = this

        {
          fix Q and j::nat
          assume "Q j"
          hence "∃i. S!j = S!i ∧ Q i"
            by blast
        } note AUX_ex_conj_SeqSI = this

        have "GS_defs.seg ?SBIP' i = ⋃ (seg ` {i..<length B})"
          unfolding GS_defs.seg_def[abs_def]
          apply simp
          apply (rule)
          apply (auto dest!: AUX1) []

          apply (auto 
            simp: seg_start_def seg_end_def 
            split: if_split_asm
            intro!: AUX_ex_conj_SeqSI
          )

         apply (metis diff_diff_cancel le_diff_conv le_eq_less_or_eq 
           lessI trans_le_add1 
           distinct_sorted_mono[OF B_sorted B_distinct, of i])

         apply (metis diff_diff_cancel le_diff_conv le_eq_less_or_eq 
           trans_le_add1 distinct_sorted_mono[OF B_sorted B_distinct, of i])
         
         apply (metis (opaque_lifting, no_types) Suc_lessD Suc_lessI less_trans_Suc
           B_in_bound')
         done
      } note AUX2 = this
      
      from ILEN have "GS_defs.p_α (S, take (Suc i) B, I, P) = collapse_aux p_α i"
        unfolding GS_defs.p_α_def collapse_aux_def
        apply (simp add: min_absorb2 drop_map)
        apply (rule conjI)
        apply (auto 
          simp: GS_defs.seg_def[abs_def] GS_defs.seg_start_def GS_defs.seg_end_def take_map) []

        apply (simp add: AUX2)
        done
    } note AUX1 = this

    from A obtain i where [simp]: "I v = Some (STACK i)"
      using I_consistent set_p_α_is_set_S
      by (auto simp: in_set_conv_nth)

    {
      have "(collapse_aux p_α (idx_of p_α v), D_α, pE_α) =
        GS_defs.α (S, take (Suc (idx_of p_α v)) B, I, P)"
      unfolding GS_defs.α_def
      using idx_of_props[OF p_α_disjoint_sym A]
      by (simp add: AUX1)
    } note ABS=this

    {
      have "GS_invar E V0 (S, take (Suc (idx_of p_α v)) B, I, P)"
        apply unfold_locales
        apply simp_all

        using B_in_bound B_sorted B_distinct
        apply (auto simp: sorted_take dest: in_set_takeD) [3]

        using B0 S_distinct apply auto [2]

        using I_consistent apply simp

        using P_sorted P_distinct P_bound apply auto[3]

        using S_subset_nodes apply auto

        done
    } note INV=this

    show ?thesis
      unfolding collapse_impl_def
      apply (refine_rcg SPEC_refine refine_vcg order_trans[OF idx_of_correct])
      apply fact
      apply (metis discrete)

      apply (simp add: collapse_def α_def)
      unfolding GS_rel_def
      apply (clarsimp simp: in_br_conv)
        apply (rule conjI)
        apply (rule ABS)
        apply (rule INV)
      done
  qed

end

text ‹Technical adjustment for avoiding case-splits for definitions
  extracted from GS-locale›
lemma opt_GSdef: "f ≡ g ⟹ f s ≡ case s of (S,B,I,P) ⇒ g (S,B,I,P)" by auto

lemma ext_def: "f≡g ⟹ f x ≡ g x" by auto

context fr_graph begin

  interpretation GSX: GS E V0 SBIP for SBIP by unfold_locales

  definition "push_impl_fr v s ≡ do{ succs ← successors {v}; GSX.push_impl s v succs}" 
  lemmas push_impl_def_opt = 
    push_impl_fr_def[abs_def, 
    THEN ext_def, THEN opt_GSdef, unfolded GSX.push_impl_def GS_sel_simps]

  lemma GS_α_split: 
    "GS_defs.α s = (p,D,pE) ⟷ (p=GS_defs.p_α s ∧ D=GS_defs.D_α s ∧ pE=GS_defs.pE_α s)"
    "(p,D,pE) = GS_defs.α s ⟷ (p=GS_defs.p_α s ∧ D=GS_defs.D_α s ∧ pE=GS_defs.pE_α s)"
    by (auto simp add: GS_defs.α_def)

  lemma ex_tuple3_eq_conv_aux: "(∃a b c. (a,b,c) = x ∧ P a b c) ⟷ (case x of (a,b,c) ⇒ P a b c)"
    apply (cases x)
    by auto

  lemma push_refine:
    assumes A: "(s,(p,D,pE,vE))∈GS_rel" "(v,v')∈Id"
    assumes B: "v∉⋃(set p)" "v∉D"
    assumes REACH: "v ∈ E⇧* `` V0"
    shows "push_impl_fr v s ≤ ⇓GS_rel (push v' (p,D,pE,vE))"
  proof -
    from A have XF[simp]: "p=GS_defs.p_α s" "D=GS_defs.D_α s" "pE=GS_defs.pE_α s" "v'=v" 
      and INV: "GS_invar E V0 s"
      by (auto simp add: GS_rel_def br_def GS_α_split)

    interpret GS_invar E V0 s by fact

    note CC = push_impl_core_correct[OF B[unfolded XF] REACH]

    have VNS: "v∉set (GSX.S s)" 
      using XF(1) assms(3) set_p_α_is_set_S by blast
    hence LS: "length (GSX.S s) < card (E⇧* `` V0)"
      by (metis REACH S_distinct S_length_nodes S_subset_nodes card_subset_eq distinct_card finite_reachableE_V0 le_neq_implies_less)
    hence LB: "length (GSX.B s) < card (E⇧* `` V0)"
      by (metis B_distinct B_in_bound' B_length_nodes B_sorted order_le_imp_less_or_eq order_le_less_trans order_less_imp_not_eq2 sorted_wrt_less_idx strict_sorted_iff)

    have LP: "length (GSX.P s) < card (E⇧* `` V0)"
    proof -
      have "v∉set (map fst (GSX.P s))" 
        using P_bound VNS by auto
      hence "set (map fst (GSX.P s)) ⊆ E⇧* `` V0 - {v}" using P_bound S_subset_nodes by fastforce
      hence "card (set (map fst (GSX.P s))) ≤ card (E⇧* `` V0 - {v})"
        by (auto intro: card_mono)
      moreover have "card (set (map fst (GSX.P s))) = length (GSX.P s)"
        by (metis P_distinct distinct_card length_map)
      moreover have "card (E⇧* `` V0 - {v}) = card (E⇧* `` V0) - 1"
        by (simp add: REACH)
      moreover have "card (E⇧* `` V0) ≠ 0"
        using REACH by auto
      ultimately show ?thesis by linarith
    qed

    show ?thesis
      unfolding push_impl_fr_def GSX.push_impl_def successors_def push_def  out_edges_def
      apply (clarsimp simp: pw_le_iff refine_pw_simps LS LB LP)
      subgoal for p D pE vE succs
        apply (clarsimp simp: GS_rel_def in_br_conv ex_tuple3_eq_conv_aux split: prod.splits)
        using CC[of succs]
        apply clarsimp
        unfolding edges_of_succs_def by auto
      done
  qed


  definition "pop_impl_fr s ≡ GSX.pop_impl s"
  lemmas pop_impl_def_opt = 
    pop_impl_fr_def[abs_def, THEN opt_GSdef, unfolded GSX.pop_impl_def
    mark_as_done_def GS_defs.seg_start_def GS_defs.seg_end_def 
    GS_sel_simps]

  lemma pop_refine:
    assumes A: "(s,(p,D,pE,vE))∈GS_rel"
    assumes B: "p ≠ []" "set_mset pE ∩ last p × UNIV = {}"
    shows "pop_impl_fr s i ≤ ⇓GS_rel (RETURN (pop (p,D,pE,vE)))"
  proof -
    from A have [simp]: "p=GS_defs.p_α s ∧ D=GS_defs.D_α s ∧ pE=GS_defs.pE_α s" 
      and INV: "GS_invar E V0 s"
      by (auto simp add: GS_rel_def br_def GS_α_split)

    show ?thesis
      unfolding pop_impl_fr_def[abs_def] pop_def
      apply (rule order_trans[OF GS_invar.pop_correct])
      using INV B
      apply (auto simp add: Un_commute RETURN_def)
      done
  qed


  definition "collapse_impl_fr v s ≡ GSX.collapse_impl s v"
  lemmas collapse_impl_fr_def_opt = 
    collapse_impl_fr_def[abs_def, 
    THEN ext_def, THEN opt_GSdef, unfolded GSX.collapse_impl_def GS_sel_simps]

  lemma collapse_refine:
    assumes A: "(s,(p,D,pE,vE))∈GS_rel" "(v,v')∈Id"
    assumes B: "v'∈⋃(set p)"
    shows "collapse_impl_fr v s ≤⇓GS_rel (RETURN (collapse v' (p,D,pE,vE)))"
  proof -
    from A have [simp]: "p=GS_defs.p_α s ∧ D=GS_defs.D_α s ∧ pE=GS_defs.pE_α s" "v'=v" 
      and INV: "GS_invar E V0 s"
      by (auto simp add: GS_rel_def br_def GS_α_split)

    show ?thesis
      unfolding collapse_impl_fr_def[abs_def]
      apply (rule order_trans[OF GS_invar.collapse_correct])
      using INV B by (auto simp add: GS_defs.α_def RETURN_def)
  qed

  definition "select_edge_impl s ≡ GSX.sel_rem_last s"
  sepref_register select_edge_impl :: "'v list × nat list × ('v ⇒ node_state option) × ('v × 'v list) list
     ⇒ ('v option × 'v list × nat list × ('v ⇒ node_state option) × ('v × 'v list) list) nres"


  lemmas select_edge_impl_def_opt = 
    select_edge_impl_def[abs_def, 
      THEN opt_GSdef, 
      unfolded GSX.sel_rem_last_def GS_defs.seg_start_def GS_sel_simps]

  lemma select_edge_refine: 
    assumes A: "(s,(p,D,pE,vE))∈GS_rel"
    assumes NE: "p ≠ []"
    shows "select_edge_impl s ≤ ⇓(Id ×⇩r GS_rel) (select_edge (p,D,pE,vE))"
  proof -
    from A have [simp]: "p=GS_defs.p_α s ∧ D=GS_defs.D_α s ∧ pE=GS_defs.pE_α s" 
      and INV: "GS_invar E V0 s"
      by (auto simp add: GS_rel_def br_def GS_α_split)

    from INV NE show ?thesis
      unfolding select_edge_impl_def
      using GS_invar.sel_rem_last_correct[OF INV] NE
      by (simp)
  qed

  definition "initial_impl v0 I ≡ do{ succs ← successors {v0}; RETURN (GS_initial_impl I v0 succs)}"
  sepref_register initial_impl :: "'v ⇒ ('v ⇒ node_state option) ⇒ ('v list × nat list × ('v ⇒ node_state option) × ('v × 'v list) list) nres"


  lemma initial_refine:
    "⟦v0∈V0;v0∉D0; (I,D0)∈oGS_rel; (v0i,v0)∈Id⟧ 
    ⟹ initial_impl v0i I ≤ ⇓GS_rel (initial v0 D0)"
    unfolding initial_impl_def GS_rel_def br_def successors_def initial_def out_edges_def
    apply (clarsimp simp: pw_le_iff refine_pw_simps)
    subgoal for p D pE vE succs
      using GS_initial_correct[of I D0 v0 succs]
      apply clarsimp
      unfolding edges_of_succs_def
      by auto
    done


  definition "path_is_empty_impl s ≡ GS_defs.S s = []"
  lemma path_is_empty_refine: 
    "GS_invar E V0 s ⟹ path_is_empty_impl s ⟷ GS_defs.p_α s=[]"
    unfolding path_is_empty_impl_def GS_defs.p_α_def GS_invar.empty_eq
    by auto

  definition (in GS_defs) "is_on_stack_impl v 
    ≡ case I v of Some (STACK _) ⇒ True | _ ⇒ False"

  lemma (in GS_invar) is_on_stack_impl_correct:
    shows "is_on_stack_impl v ⟷ v∈⋃(set p_α)"
    unfolding is_on_stack_impl_def
    using I_consistent[of v]
    apply (force 
      simp: set_p_α_is_set_S in_set_conv_nth 
      split: option.split node_state.split)
    done

  definition "is_on_stack_impl v s ≡ GS_defs.is_on_stack_impl s v"
  lemmas is_on_stack_impl_def_opt = 
    is_on_stack_impl_def[abs_def, THEN ext_def, THEN opt_GSdef, 
      unfolded GS_defs.is_on_stack_impl_def GS_sel_simps]

  lemma is_on_stack_refine:
    "⟦ GS_invar E V0 s ⟧ ⟹ is_on_stack_impl v s ⟷ v∈⋃(set (GS_defs.p_α s))"
    unfolding is_on_stack_impl_def GS_rel_def br_def
    by (simp add: GS_invar.is_on_stack_impl_correct)


  definition (in GS_defs) "is_done_impl v 
    ≡ case I v of Some (DONE i) ⇒ True | _ ⇒ False"

  lemma (in GS_invar) is_done_impl_correct:
    shows "is_done_impl v ⟷ v∈D_α"
    unfolding is_done_impl_def D_α_def
    apply (auto split: option.split node_state.split)
    done

  definition "is_done_oimpl v I ≡ case I v of Some (DONE i) ⇒ True | _ ⇒ False"
  sepref_register is_done_oimpl :: "'a ⇒ ('a, node_state) i_map ⇒ bool" 

  definition "is_done_impl v s ≡ GS_defs.is_done_impl s v"

  lemma is_done_orefine:
    "⟦ oGS_invar E V0 s ⟧ ⟹ is_done_oimpl v s ⟷ v∈oGS_α s"
    unfolding is_done_oimpl_def oGS_rel_def br_def
    by (auto 
      simp: oGS_invar_def oGS_α_def 
      split: option.splits node_state.split)

  lemma is_done_refine:
    "⟦ GS_invar E V0 s ⟧ ⟹ is_done_impl v s ⟷ v∈GS_defs.D_α s"
    unfolding is_done_impl_def GS_rel_def br_def
    by (simp add: GS_invar.is_done_impl_correct)

  lemma oinitial_refine: "(Map.empty, {}) ∈ oGS_rel"
    by (auto simp: oGS_rel_def br_def oGS_α_def oGS_invar_def fr_graph_axioms oGS_invar_axioms_def)

end

subsection ‹Refined Skeleton Algorithm›

context fr_graph begin

  lemma I_to_outer:
    assumes "((S, B, I, P), ([], D, {#}, vE)) ∈ GS_rel"
    shows "(I,D)∈oGS_rel"
    using assms
    unfolding GS_rel_def oGS_rel_def br_def oGS_α_def GS_defs.α_def GS_defs.D_α_def GS_invar_def GS_invar_axioms_def oGS_invar_def
    apply (auto simp: GS_defs.p_α_def fr_graph_axioms oGS_invar_axioms_def)
    done
  
  
  definition "skeleton_inner_while_body s = 
          do {
            ― ‹Select edge from end of path›
            (vo,s) ← select_edge_impl s;

            case vo of 
              Some v ⇒ do {
                ASSERT (v ∈ E⇧*``V0);
                if is_on_stack_impl v s then do {
                  collapse_impl_fr v s
                } else if ¬is_done_impl v s then do {
                  ― ‹Edge to new node. Append to path›
                  push_impl_fr v s
                } else do {
                  ― ‹Edge to done node. Skip›
                  RETURN s
                }
              }
            | None ⇒ do {
                ― ‹No more outgoing edges from current node on path›
                pop_impl_fr s 0
              }
          }"


  definition skeleton_impl :: "'v oGS nres" where
    "skeleton_impl ≡ do {
      let I=Map.empty;
      r ← FOREACHi (λit I. outer_invar it (oGS_α I)) V0 (λv0 I0. do {
        ASSERT (v0 ∈ E⇧*``V0);
        if ¬is_done_oimpl v0 I0 then do {
          s ← initial_impl v0 I0;

          (S,B,I,P)← WHILEIT ((λ(p,D,pE). ∃vE. invar v0 (oGS_α I0) (p,D,pE,vE)) o GS_defs.α)
            (λs. ¬path_is_empty_impl s) 
            skeleton_inner_while_body s;
          RETURN I
        } else
          RETURN I0
      }) I;
      RETURN r
    }"

  subsubsection ‹Correctness Theorem›

  theorem skeleton_impl_refine: "skeleton_impl ≤ ⇓oGS_rel skeleton"
    using [[goals_limit = 23]]
    unfolding skeleton_impl_def skeleton_def skeleton_inner_while_body_def
    apply (refine_rcg
      bind_refine'
      select_edge_refine push_refine 
      pop_refine
      collapse_refine 
      initial_refine
      oinitial_refine
      inj_on_id
    )
    using [[goals_limit = 5]]
    apply refine_dref_type  

    apply (vc_solve (nopre) solve: asm_rl I_to_outer
      simp: GS_rel_def br_def GS_defs.α_def oGS_rel_def oGS_α_def 
      is_on_stack_refine path_is_empty_refine is_done_refine is_done_orefine
    )

    done

  end

end