Session Gabow_SCC

Theory Gabow_Skeleton

section ‹Skeleton for Gabow's SCC Algorithm \label{sec:skel}›
theory Gabow_Skeleton
imports CAVA_Automata.Digraph
begin

(* TODO: convenience locale, consider merging this with invariants *)
locale fr_graph =
  graph G
  for G :: "('v, 'more) graph_rec_scheme"
  +
  assumes finite_reachableE_V0[simp, intro!]: "finite (E* `` V0)"

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 ‹Statistics Setup›
text ‹
  We define some dummy-constants that are included into the generated code,
  and may be mapped to side-effecting ML-code that records statistics and debug information
  about the execution. In the skeleton algorithm, we count the number of visited nodes,
  and include a timing for the whole algorithm.
›

definition stat_newnode :: "unit => unit"   ― ‹Invoked if new node is visited›
  where [code]: "stat_newnode  λ_. ()"

definition stat_start :: "unit => unit"     ― ‹Invoked once if algorithm starts›
  where [code]: "stat_start  λ_. ()"

definition stat_stop :: "unit => unit"      ― ‹Invoked once if algorithm stops›
  where [code]: "stat_stop  λ_. ()"

lemma [autoref_rules]: 
  "(stat_newnode,stat_newnode)  unit_rel  unit_rel"
  "(stat_start,stat_start)  unit_rel  unit_rel"
  "(stat_stop,stat_stop)  unit_rel  unit_rel"
  by auto

abbreviation "stat_newnode_nres  RETURN (stat_newnode ())"
abbreviation "stat_start_nres  RETURN (stat_start ())"
abbreviation "stat_stop_nres  RETURN (stat_stop ())"

lemma discard_stat_refine[refine]:
  "m1m2  stat_newnode_nres  m1  m2"
  "m1m2  stat_start_nres  m1  m2"
  "m1m2  stat_stop_nres  m1  m2"
  by simp_all

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. ik  k<j}"

lemma path_seg_simps[simp]: 
  "ji  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  vp!i"

lemma idx_of_props:
  assumes 
    p_disjoint_sym: "i j v. i<length p  j<length p  vp!i  vp!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. vp ! 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  vp!i  vp!j  i=j"
  assumes A: "i<length p" "vp!i"
  shows "idx_of p v = i"
proof -
  from A p_disjoint_sym have "j<length p. vp ! 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, and the set
  pE› of pending edges.›
type_synonym 'v abs_state = "'v set list × 'v set × ('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)"

  definition vE :: "'v set list  'v set  ('v × 'v) set  ('v × 'v) set"
    ― ‹Visited edges: No longer pending edges from touched nodes›
    where "vE p D pE  (E  (touched p D × UNIV)) - pE"

  lemma vE_ss_E: "vE p D pE  E" ― ‹Visited edges are edges›
    unfolding vE_def by auto

end

locale outer_invar_loc ― ‹Invariant of the outer loop›
  = fr_graph G for G :: "('v,'more) graph_rec_scheme" +
  fixes it :: "'v set" ― ‹Remaining nodes to iterate over›
  fixes D :: "'v set" ― ‹Finished nodes›

  assumes it_initial: "itV0"  ― ‹Only start nodes to iterate over›

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

  lemma locale_this: "outer_invar_loc G it D" by unfold_locales

  definition (in fr_graph) "outer_invar  λit D. outer_invar_loc G 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 G
  for G :: "('v, 'more) graph_rec_scheme" +
  fixes v0 :: "'v"
  fixes D0 :: "'v set"
  fixes p :: "'v set list"
  fixes D :: "'v set"
  fixes pE :: "('v×'v) set"

  assumes v0_initial[simp, intro!]: "v0V0"
  assumes D_incr: "D0  D"

  assumes pE_E_from_p: "pE  E  ((set p)) × UNIV" 
    ― ‹Pending edges are edges from path›
  assumes E_from_p_touched: "E  ((set p) × UNIV)  pE  UNIV × touched p D" 
    ― ‹Edges from path are pending or touched›
  assumes D_reachable: "DE*``V0" ― ‹Done nodes are reachable›
  assumes p_connected: "Suc i<length p  p!i × p!Suc i  (E-pE)  {}"
    ― ‹CNodes on path are connected by non-pending edges›

  assumes p_disjoint: "i<j; j<length p  p!i  p!j = {}" 
    ― ‹CNodes on path are disjoint›
  assumes p_sc: "Uset p  U×U  (vE p D pE  U×U)*" 
    ― ‹Nodes in CNodes are mutually reachable by visited edges›

  assumes root_v0: "p[]  v0hd p" ― ‹Root CNode contains start node›
  assumes p_empty_v0: "p=[]  v0D" ― ‹Start node is done if path empty›
  
  assumes D_closed: "E``D  D" ― ‹Done is closed under transitions›
  (*assumes D_vis: "E∩D×D ⊆ vE" -- "All edges from done nodes are visited"*)

  assumes vE_no_back: "i<j; j<length p  vE p D pE  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›
begin
  abbreviation ltouched where "ltouched  touched p D"
  abbreviation lvE where "lvE  vE p D pE"

  lemma locale_this: "invar_loc G v0 D0 p D pE" by unfold_locales

  definition (in fr_graph) 
    "invar  λv0 D0 (p,D,pE). invar_loc G v0 D0 p D pE"

  lemma invar_this[simp, intro!]: "invar v0 D0 (p,D,pE)"
    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 D_vis: "ED×UNIV  lvE" ― ‹All edges from done nodes are visited›
    unfolding vE_def touched_def using pE_E_from_p p_not_D by blast 

  lemma vE_touched: "lvE  ltouched × ltouched" 
    ― ‹Visited edges only between touched nodes›
    using E_from_p_touched D_closed unfolding vE_def touched_def by blast

  lemma lvE_ss_E: "lvE  E" ― ‹Visited edges are edges›
    unfolding vE_def by auto


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

  lemma pE_by_vE: "pE = (E  (set p) × UNIV) - lvE"
    ― ‹Pending edges are edges from path not yet visited›
    unfolding vE_def touched_def
    using pE_E_from_p
    by auto

  lemma pick_pending: "p[]  pE  last p × UNIV = (E-lvE)  last p × UNIV"
    ― ‹Pending edges from end of path are non-visited edges from end of path›
    apply (subst pE_by_vE)
    by auto

  lemma p_connected': 
    assumes A: "Suc i<length p" 
    shows "p!i × p!Suc i  lvE  {}" 
  proof -
    from A p_not_D have "p!i  set p" "p!Suc i  set p" by auto
    with p_connected[OF A] show ?thesis unfolding vE_def touched_def
      by blast
  qed

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 "unproc_edges v0 p D pE  (E  (E*``{v0} - (D  (set p))) × UNIV)  pE"

  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 length)
    (λ(p,D,pE). (unproc_edges v0 p D 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 (in fr_graph) initial :: "'v  'v set  'v abs_state"
    where "initial v0 D  ([{v0}], D, (E  {v0}×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)=PDPE; 
      i=idx_of p v;
      p = collapse_aux p i
    in (p,D,pE)"

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

  definition (in fr_graph) push :: "'v  'v abs_state  'v abs_state" 
    where "push v PDPE  
    let
      (p,D,pE) = PDPE;
      p = p@[{v}];
      pE = pE  (E{v}×UNIV)
    in
      (p,D,pE)"

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

  text ‹The following lemmas match the definitions presented in the paper:›
  lemma "select_edge (p,D,pE)  do {
      e  SELECT (λe. e  pE  last p × UNIV);
      case e of
        None  RETURN (None,(p,D,pE))
      | Some (u,v)  RETURN (Some v, (p,D,pE - {(u,v)}))
    }"
    unfolding select_edge_def by simp

  lemma "collapse v (p,D,pE) 
     let i=idx_of p v in (take i p @ [(set (drop i p))],D,pE)"
    unfolding collapse_def collapse_aux_def by simp

  lemma "push v (p, D, pE)  (p @ [{v}], D, pE  E  {v} × UNIV)"
    unfolding push_def by simp

  lemma "pop (p, D, pE)  (butlast p, last p  D, pE)"
    unfolding pop_def by auto

  thm pop_def[unfolded Let_def, no_vars]

  thm select_edge_def[unfolded Let_def]


  definition skeleton :: "'v set nres" 
    ― ‹Abstract Skeleton Algorithm›
    where
    "skeleton  do {
      let D = {};
      r  FOREACHi outer_invar V0 (λv0 D0. do {
        if v0D0 then do {
          let s = initial v0 D0;

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

            ASSERT (p[]);
            case vo of 
              Some v  do { ― ‹Found outgoing edge to node v›
                if v  (set p) then do {
                  ― ‹Back edge: Collapse path›
                  RETURN (collapse v (p,D,pE))
                } else if vD then do {
                  ― ‹Edge to new node. Append to path›
                  RETURN (push v (p,D,pE))
                } else do {
                  ― ‹Edge to done node. Skip›
                  RETURN (p,D,pE)
                }
              }
            | None  do {
                ASSERT (pE  last p × UNIV = {});
                ― ‹No more outgoing edges from current node on path›
                RETURN (pop (p,D,pE))
              }
          }) 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 vE_collapse_aux[simp]: "vE (collapse_aux p i) D pE = vE p D pE"
    unfolding vE_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; up!i; vp!i  (u,v)(lvE  p!i×p!i)*"
    using p_sc[of "p!i"] by (auto simp: in_set_conv_nth)

  lemma cnode_connectedI': "i<length p; up!i; vp!i  (u,v)(lvE)*"
    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; vp!i; vp!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" "ulength p"
    shows "p!ipath_seg p l u  li  i<u"
  proof
    assume B: "p!ipath_seg p l u"
    from A obtain x where "xp!i" by (blast dest: p_no_empty_idx)
    with B obtain i' where C: "xp!i'" "li'" "i'<u" 
      by (auto simp: path_seg_def)
    from p_disjoint_sym[OF i<length p _ xp!i xp!i'] i'<u ulength p
    have "i=i'" by simp
    with C show "li  i<u" by auto
  qed (auto simp: path_seg_def)

  lemma path_seg_ss_eq[simp]:
    assumes A: "l1<u1" "u1length p" "l2<u2" "u2length p"
    shows "path_seg p l1 u1  path_seg p l2 u2  l2l1  u1u2"
  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: "l2l1" using A by simp
    have "p!(u1 - 1)  path_seg p l1 u1" using A by simp
    also note S finally have 2: "u1u2" using A by auto
    from 1 2 show "l2l1  u1u2" ..
  next
    assume "l2l1  u1u2" 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 "xp!i" "yp!j"
    assumes "ij" "j<length p"
    defines "seg  path_seg p i (Suc j)"
    shows "(x,y)(lvE  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)lvE" "up!j" "vp!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'] xp!i ‹Suc j < length p 
    have t: "(x,x')(lvE?seg×?seg)*" by auto
    have "(x,x')(lvE?seg'×?seg')*" using SSS 
      by (auto intro: rtrancl_mono_mp[OF _ t])
    also 
    from cnode_connectedI[OF _ x'p!j up!j] ‹Suc j < length p have
      t: "(x', u)  (lvE  p ! j × p ! j)*" by auto
    have "(x', u)  (lvE?seg'×?seg')*" using ISS
      by (auto intro: rtrancl_mono_mp[OF _ t])
    also have "(u,v)lvE?seg'×?seg'" using UV ISS by auto
    also from cnode_connectedI[OF ‹Suc j < length p vp!Suc j yp!Suc j] 
    have t: "(v, y)  (lvE  p ! Suc j × p ! Suc j)*" by auto
    have "(v, y)  (lvE?seg'×?seg')*" using ISS
      by (auto intro: rtrancl_mono_mp[OF _ t])
    finally show "(x,y)(lvE?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 "vp!i" 
      by (metis UnionE in_set_conv_nth)
    moreover from A root_v0 have "v0p!0" by (cases p) auto
    ultimately have 
      t: "(v0,v)(lvE  path_seg p 0 (Suc i) × path_seg p 0 (Suc i))*"
      by (auto intro: pathI)
    from lvE_ss_E have "(v0,v)E*" by (auto intro: rtrancl_mono_mp[OF _ t])
    thus "vE*``{v0}" by auto
  qed

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

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

  lemma pE_reachable: "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: "lvE*``D  D"
    by (metis D_closed Image_closed_trancl eq_iff reachable_mono lvE_ss_E)

  lemma D_closed_path: "path E u q w; uD  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 lvE u q w; uD  set q  D"
    by (metis D_closed_path path_mono lvE_ss_E)

  lemma path_in_lastnode:
    assumes P: "path lvE u q v"
    assumes [simp]: "p[]"
    assumes ND: "ulast p" "vlast p"
    shows "set q  last p"
    ― ‹A path from the last Cnode to the last Cnode remains in the last Cnode›
    (* TODO: This can be generalized in two directions: 
      either 1) The path end anywhere. Due to vE_touched we can infer 
        that it ends in last cnode  
      or 2) We may use any cnode, not only the last one
    *)
    using P ND
  proof (induction)
    case (path_prepend u v l w) 
    from (u,v)lvE› vE_touched have "vltouched" by auto
    hence "v(set p)"
      unfolding touched_def
    proof
      assume "vD"
      moreover from ‹path lvE v l w have "(v,w)lvE*" by (rule path_is_rtrancl)
      ultimately have "wD" using D_closed_vE_rtrancl by auto
      with wlast 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" "vp!i"
      by (metis UnionE in_set_conv_nth)
    have "i=length p - 1"
    proof (rule ccontr)
      assume "ilength 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 "lvE  last p × p!i = {}"
        by (simp add: last_conv_nth)
      with (u,v)lvE› ulast p vp!i show False by auto
    qed
    with vp!i have "vlast p" by (simp add: last_conv_nth)
    with path_prepend.IH wlast p ulast p show ?case by auto
  qed simp

  lemma loop_in_lastnode:
    assumes P: "path lvE u q u"
    assumes [simp]: "p[]"
    assumes ND: "set q  last p  {}"
    shows "ulast 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 "vset q" "vlast p" by auto
    then obtain q1 q2 where [simp]: "q=q1@v#q2" 
      by (auto simp: in_set_conv_decomp)
    from P have "path lvE v (v#q2@q1) v" 
      by (auto simp: path_conc_conv path_cons_conv)
    from path_in_lastnode[OF this p[] vlast p vlast p] 
    show "set q  last p" by simp
    from P show "ulast 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›

lemma (in fr_graph) vE_initial[simp]: "vE [{v0}] {} (E  {v0} × UNIV) = {}"
  unfolding vE_def touched_def by auto

context invar_loc
begin
  lemma vE_push: " (u,v)pE; ulast p; v(set p); vD  
     vE (p @ [{v}]) D ((pE - {(u,v)})  E{v}×UNIV) = insert (u,v) lvE"
    unfolding vE_def touched_def using pE_E_from_p
    by auto

  lemma vE_remove[simp]: 
    "p[]; (u,v)pE  vE p D (pE - {(u,v)}) = insert (u,v) lvE"
    unfolding vE_def touched_def using pE_E_from_p by blast

  lemma vE_pop[simp]: "p[]  vE (butlast p) (last p  D) pE = lvE"
    unfolding vE_def touched_def 
    by (cases p rule: rev_cases) auto


  lemma pE_fin: "p=[]  pE={}"
    using pE_by_vE by auto

  lemma (in invar_loc) lastp_un_D_closed:
    assumes NE: "p  []"
    assumes NO': "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)
    from NO' have NO: "(E - lvE)  (last p × UNIV) = {}"
      by (simp add: pick_pending[OF NE])

    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: "ulast p  D" hence "up!?i  D" by simp
    
    {
      assume "ulast p" "vlast p" 
      moreover from E NO ulast p have "(u,v)lvE" by auto
      ultimately have "vD  v(set p)" 
        using vE_touched unfolding touched_def by auto
      moreover {
        assume "v(set p)"
        then obtain j where V: "j<length p" "vp!j" 
          by (metis UnionE in_set_conv_nth)
        with vlast p have "j<?i" by (cases "j=?i") auto
        from vE_no_back[OF j<?i _] (u,v)lvE› V ulast p have False by auto
      } ultimately have "vD" by blast
    } with E UI D_closed show "vlast 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 "v0it - D"
    shows "invar v0 D (initial v0 D)"
    unfolding invar_def initial_def
    apply simp
    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 []
    done

  lemma invar_initial: 
    "outer_invar it D0; v0it; v0D0  invar v0 D0 (initial 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)"
    assumes NE[simp]: "p[]"
    assumes NO': "pE  (last p × UNIV) = {}"
    shows "invar v0 D0 (pop (p,D,pE))"
    unfolding invar_def pop_def
    apply simp
  proof -
    from INV interpret invar_loc G 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  (E - pE)  {}"
        by simp
    } note AUX_p_connected = this

    (*have [simp]: "(E ∩ (last p ∪ D ∪ ⋃set (butlast p)) × UNIV - pE) = vE"
      unfolding vE_def touched_def by auto*)

    show "invar_loc G v0 D0 (butlast p) (last p  D) pE"
      apply unfold_locales
  
      unfolding vE_pop[OF NE]

      apply simp

      using D_incr apply auto []

      using pE_E_from_p NO' apply auto []
  
      using E_from_p_touched apply (auto simp: touched_def) []
  
      using D_reachable p_reachable NE apply auto []

      apply (rule AUX_p_connected, assumption+) []

      using p_disjoint apply (simp add: nth_butlast)

      using p_sc apply simp

      using root_v0 apply (cases p rule: rev_cases) apply auto [2]

      using root_v0 p_empty_v0 apply (cases p rule: rev_cases) apply auto [2]

      apply (rule lastp_un_D_closed, insert NO', auto) []

      using vE_no_back apply (auto simp: nth_butlast) []

      using p_not_D lp_dj_blp apply auto []
      done
  qed

  thm invar_pop[of v_0 D_0, no_vars]

  lemma invar_collapse:
    assumes INV: "invar v0 D0 (p,D,pE)"
    assumes NE[simp]: "p[]"
    assumes E: "(u,v)pE" and "ulast 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)}))"
    unfolding invar_def collapse_def
    apply simp
    unfolding i_def[symmetric] p'_def[symmetric]
  proof -
    from INV interpret invar_loc G v0 D0 p D pE unfolding invar_def by simp

    let ?thesis="invar_loc G v0 D0 p' D (pE - {(u,v)})"

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

    have IL: "i < length p" and VMEM: "vp!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 ulast p have "up!(length p - 1)" by (auto simp: last_conv_nth)

    have defs_fold: 
      "vE p' D (pE - {(u,v)}) = insert (u,v) lvE" 
      "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
      from p_connected[OF this] have "p!j × p!Suc j  (E-pE)  {}" .
      moreover from P'_IDX_SS A have "p!jp'!j" and "p!Suc j  p'!Suc j"
        by auto
      ultimately have "p' ! j × p' ! Suc j  (E - (pE - {(u, v)}))  {}" 
        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 "vp'!j" and "vp'!k"
        with A have "vp!j" by simp
        show False proof (cases)
          assume "k=i"
          with vp'!k obtain k' where "vp!k'" "ik'" "k'<length p" 
            by (auto simp: path_seg_def)
          hence "p ! j  p ! k' = {}"
            using A by (auto intro!: p_disjoint)
          with vp!j vp!k' show False by auto
        next
          assume "ki" 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 vp'!j vp'!k by auto
        qed
      qed
    } note AUX_p_disjoint = this

    {
      fix U
      assume A: "Uset 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) lvE  U × U)*" 
      proof cases
        assume [simp]: "j=i"
        show ?thesis proof (clarsimp)
          fix x y
          assume "xpath_seg p i (length p)" "ypath_seg p i (length p)"
          then obtain ix iy where 
            IX: "xp!ix" "iix" "ix<length p" and
            IY: "yp!iy" "iiy" "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. (lvE  R×R)"
          let ?E = "(insert (u,v) lvE  ?last_cnode × ?last_cnode)"

          from pathI[OF xp!ix up!(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 up!(length p - 1)])
            apply (simp)
            apply (rule rev_subsetD[OF VMEM])
            apply (simp)
            done
          also 
          from pathI[OF vp!i yp!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 "ji"
        with j<Suc i have [simp]: "j<i" by simp
        with i<length p have "p!jset p"
          by (metis Suc_lessD in_set_conv_nth less_trans_Suc) 

        thus ?thesis using p_sc[of U] p!jset p
          apply (clarsimp)
          apply (subgoal_tac "(a,b)(lvE  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) lvE  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 "lvE  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)lvE" "xpath_seg p i (length p)" "yp!j"
            then obtain ix where "xp!ix" "iix" "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

    show ?thesis
      apply unfold_locales
      unfolding defs_fold

      apply simp

      using D_incr apply auto []

      using pE_E_from_p apply auto []

      using E_from_p_touched BACK apply (simp add: touched_def) apply blast

      apply (rule D_reachable)

      apply (rule AUX_p_connected, assumption+) []

      apply (rule AUX_p_disjoint, assumption+) []

      apply (rule AUX_p_sc, assumption+) []

      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) []

      apply (simp add: p'_def collapse_aux_def)

      apply (rule D_closed)

      apply (drule (1) AUX_vE_no_back, auto) []

      using p_not_D apply simp
      done
  qed
  
  lemma invar_push:
    assumes INV: "invar v0 D0 (p,D,pE)"
    assumes NE[simp]: "p[]"
    assumes E: "(u,v)pE" and UIL: "ulast p"
    assumes VNE: "v(set p)" "vD"
    shows "invar v0 D0 (push v (p,D,pE - {(u,v)}))"
    unfolding invar_def push_def
    apply simp
  proof -
    from INV interpret invar_loc G v0 D0 p D pE unfolding invar_def by simp

    let ?thesis 
      = "invar_loc G v0 D0 (p @ [{v}]) D (pE - {(u, v)}  E  {v} × UNIV)"

    note defs_fold = vE_push[OF E UIL VNE] touched_push

    {
      fix i
      assume SILL: "Suc i < length (p @ [{v}])"
      have "(p @ [{v}]) ! i × (p @ [{v}]) ! Suc i 
              (E - (pE - {(u, v)}  E  {v} × UNIV))  {}"
      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) fast
      next
        case False
        with SILL have SILL': "Suc i < length p" by simp
            
        with SILL' VNE have X1: "vp!i" "vp!Suc i" by auto
            
        from p_connected[OF SILL'] obtain a b where 
          "ap!i" "bp!Suc i" "(a,b)E" "(a,b)pE" 
          by auto
        with X1 have "av" "bv" by auto
        with (a,b)E› (a,b)pE have "(a,b)(E - (pE - {(u, v)}  E  {v} × UNIV))"
          by auto
        with ap!i bp!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) lvE  U × U)*"
      proof cases
        assume "Uset p"
        with p_sc have "U×U  (lvE  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 "Uset 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) lvE  (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
        
    show ?thesis
      apply unfold_locales
      unfolding defs_fold

      apply simp

      using D_incr apply auto []

      using pE_E_from_p apply auto []

      using E_from_p_touched VNE apply (auto simp: touched_def) []

      apply (rule D_reachable)

      apply (rule AUX_p_connected, assumption+) []

      using p_disjoint v(set p) apply (auto simp: nth_append) []

      apply (rule AUX_p_sc, assumption+) []

      using root_v0 apply simp

      apply simp

      apply (rule D_closed)

      apply (rule AUX_vE_no_back, assumption+) []

      using p_not_D VNE apply auto []
      done
  qed

  lemma invar_skip:
    assumes INV: "invar v0 D0 (p,D,pE)"
    assumes NE[simp]: "p[]"
    assumes E: "(u,v)pE" and UIL: "ulast p"
    assumes VNP: "v(set p)" and VD: "vD"
    shows "invar v0 D0 (p,D,pE - {(u, v)})"
    unfolding invar_def
    apply simp
  proof -
    from INV interpret invar_loc G v0 D0 p D pE unfolding invar_def by simp
    let ?thesis = "invar_loc G v0 D0 p D (pE - {(u, v)})"
    note defs_fold = vE_remove[OF NE E]

    show ?thesis
      apply unfold_locales
      unfolding defs_fold
      
      apply simp

      using D_incr apply auto []

      using pE_E_from_p apply auto []

      using E_from_p_touched VD apply (auto simp: touched_def) []

      apply (rule D_reachable)

      using p_connected apply auto []

      apply (rule p_disjoint, assumption+) []

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

      apply (rule root_v0, assumption+) []

      apply (rule p_empty_v0, assumption+) []

      apply (rule D_closed)

      using vE_no_back VD p_not_D 
      apply clarsimp
      apply (metis Suc_lessD UnionI VNP less_trans_Suc nth_mem)

      apply (rule p_not_D)
      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)"
    shows "D  E*``{v0}"
  proof -
    from INV interpret invar_loc G v0 D0 "[]" D pE 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)"
    assumes UR: "uE*``{v0}"
    shows "path (vE [] D pE) u q v  path E u q v"
  proof -
    from INV interpret invar_loc G v0 D0 "[]" D pE unfolding invar_def by auto
    
    show ?thesis
    proof
      assume "path lvE u q v"
      thus "path E u q v" using path_mono[OF lvE_ss_E] by blast
    next
      assume "path E u q v"
      thus "path lvE u q v" using UR
      proof induction
        case (path_prepend u v p w)
        with fin_D_is_reachable[OF INV] have "uD" by auto
        with D_closed (u,v)E› have "vD" by auto
        from path_prepend.prems path_prepend.hyps have "vE*``{v0}" by auto
        with path_prepend.IH fin_D_is_reachable[OF INV] have "path lvE v p w" 
          by simp
        moreover from uD vD (u,v)E› D_vis have "(u,v)lvE" by auto
        ultimately show ?case by (auto simp: path_cons_conv)
      qed simp
    qed
  qed

  lemma invar_outer_newnode: 
    assumes A: "v0D0" "v0it" 
    assumes OINV: "outer_invar it D0"
    assumes INV: "invar v0 D0 ([],D',pE)"
    shows "outer_invar (it-{v0}) D'"
  proof -
    from OINV interpret outer_invar_loc G it D0 unfolding outer_invar_def .
    from INV interpret inv: invar_loc G v0 D0 "[]" D' pE 
      unfolding invar_def by simp
    
    from fin_D_is_reachable[OF INV] have [simp]: "v0D'" 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: "v0D0" "v0it" 
    assumes OINV: "outer_invar it D0"
    shows "outer_invar (it-{v0}) D0"
  proof -
    from OINV interpret outer_invar_loc G 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)  pE={}"
    unfolding invar_def by (simp add: invar_loc.pE_fin)

end

subsubsection ‹Termination›

context invar_loc 
begin
  lemma unproc_finite[simp, intro!]: "finite (unproc_edges v0 p D pE)"
    ― ‹The set of unprocessed edges is finite›
  proof -
    have "unproc_edges v0 p D pE  E*``{v0} × E*``{v0}"
      unfolding unproc_edges_def 
      using pE_reachable
      by auto
    thus ?thesis
      by (rule finite_subset) simp
  qed

  lemma unproc_decreasing: 
    ― ‹As effect of selecting a pending edge, the set of unprocessed edges
      decreases›
    assumes [simp]: "p[]" and A: "(u,v)pE" "ulast p"
    shows "unproc_edges v0 p D (pE-{(u,v)})  unproc_edges v0 p D pE"
    using A unfolding unproc_edges_def
    by fastforce
end

context fr_graph 
begin

  lemma abs_wf_pop:
    assumes INV: "invar v0 D0 (p,D,pE)"
    assumes NE[simp]: "p[]"
    assumes NO: "pE  last aba × UNIV = {}"
    shows "(pop (p,D,pE), (p, D, pE))  abs_wf_rel v0"
    unfolding pop_def
    apply simp
  proof -
    from INV interpret invar_loc G v0 D0 p D pE unfolding invar_def by simp 
    let ?thesis = "((butlast p, last p  D, pE), p, D, pE)  abs_wf_rel v0"
    have "unproc_edges v0 (butlast p) (last p  D) pE = unproc_edges v0 p D pE"
      unfolding unproc_edges_def
      apply (cases p rule: rev_cases, simp)
      apply auto
      done
    thus ?thesis
      by (auto simp: abs_wf_rel_def)
  qed

  lemma abs_wf_collapse:
    assumes INV: "invar v0 D0 (p,D,pE)"
    assumes NE[simp]: "p[]"
    assumes E: "(u,v)pE" "ulast p"
    shows "(collapse v (p,D,pE-{(u,v)}), (p, D, pE)) abs_wf_rel v0"
    unfolding collapse_def
    apply simp
  proof -
    from INV interpret invar_loc G v0 D0 p D pE unfolding invar_def by simp 
    define i where "i = idx_of p v"
    let ?thesis 
      = "((collapse_aux p i, D, pE-{(u,v)}), (p, D, pE))  abs_wf_rel v0"

    have "unproc_edges v0 (collapse_aux p i) D (pE-{(u,v)}) 
      = unproc_edges v0 p D (pE-{(u,v)})"
      unfolding unproc_edges_def by (auto)
    also note unproc_decreasing[OF NE E]
    finally show ?thesis
      by (auto simp: abs_wf_rel_def)
  qed
    
  lemma abs_wf_push:
    assumes INV: "invar v0 D0 (p,D,pE)"
    assumes NE[simp]: "p[]"
    assumes E: "(u,v)pE" "ulast p" and A: "vD" "v(set p)"
    shows "(push v (p,D,pE-{(u,v)}), (p, D, pE))  abs_wf_rel v0"
    unfolding push_def
    apply simp
  proof -
    from INV interpret invar_loc G v0 D0 p D pE unfolding invar_def by simp 
    let ?thesis 
      = "((p@[{v}], D, pE-{(u,v)}  E{v}×UNIV), (p, D, pE))  abs_wf_rel v0"

    have "unproc_edges v0 (p@[{v}]) D (pE-{(u,v)}  E{v}×UNIV) 
      = unproc_edges v0 p D (pE-{(u,v)})"
      unfolding unproc_edges_def
      using E A pE_reachable
      by auto
    also note unproc_decreasing[OF NE E]
    finally show ?thesis
      by (auto simp: abs_wf_rel_def)
  qed

  lemma abs_wf_skip:
    assumes INV: "invar v0 D0 (p,D,pE)"
    assumes NE[simp]: "p[]"
    assumes E: "(u,v)pE" "ulast p"
    shows "((p, D, pE-{(u,v)}), (p, D, pE))  abs_wf_rel v0"
  proof -
    from INV interpret invar_loc G v0 D0 p D pE unfolding invar_def by simp 
    from unproc_decreasing[OF NE E] show ?thesis
      by (auto simp: abs_wf_rel_def)
  qed
end

subsubsection ‹Main Correctness Theorem›

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

  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 = 4]]

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

  text ‹Short proof, as presented in the paper›
  context 
    notes [refine] = refine_vcg 
  begin
    theorem "skeleton  SPEC (λD. outer_invar {} D)"
      unfolding skeleton_def select_edge_def select_def
      by (refine_vcg WHILEIT_rule[OF abs_wf_rel_wf])
         (auto intro: invar_preserve simp: pE_fin' finite_V0)
  end

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 G "{}" 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_raw‹\label{sec:algo-ds}›

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.

  As we use a tail-recursive formulation, we use another stack 
  P :: (nat × 'v set) list› to represent the pending edges. The
  entries in P› are sorted by ascending first component,
  and P› only contains entries with non-empty second component. 
  An entry (i,l)› means that the edges from the node at 
  S[i]› to the nodes stored in l› are pending.
›

subsection ‹Preliminaries›
primrec find_max_nat :: "nat  (natbool)  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_relbool_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 nat | DONE

type_synonym 'v oGS = "'v  node_state"

definition oGS_α :: "'v oGS  'v set" where "oGS_α I  {v. I v = Some DONE}"

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


type_synonym 'a GS 
  = "'a list × nat list × ('a  node_state) × (nat × 'a set) list"
locale GS =  
  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 v = Some DONE}" ― ‹Done nodes›
  
  definition "pE_α  { (u,v) . j I. (j,I)set P  u = S!j  vI }" 
    ― ‹Pending edges›

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

end

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

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

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

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

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

  definition S_idx_of ― ‹Stack index for node›
    where "S_idx_of v  case I v of Some (STACK i)  i"

end

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 fst P)"
  assumes P_distinct: "distinct (map fst P)"
  assumes P_bound: "set P  {0..<length S}×Collect ((≠) {})"
begin
  lemma locale_this: "GS_invar SBIP" by unfold_locales

end

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

definition "GS_rel  br GS.α GS_invar"
lemma GS_rel_sv[intro!,simp,relator_props]: "single_valued GS_rel"
  unfolding GS_rel_def by auto

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!ij}"
    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 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 "vset 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_α  vp_α!i  vp_α!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 set  'a GS" where
  "GS_initial_impl I v0 succs  (
    [v0],
    [0],
    I(v0(STACK 0)),
    if succs={} then [] else [(0,succs)])"

context GS
begin
  definition "push_impl v succs  
    let
      _ = stat_newnode ();
      j = length S;
      S = S@[v];
      B = B@[j];
      I = I(v  STACK j);
      P = if succs={} then P else P@[(j,succs)]
    in
      (S,B,I,P)"

  
  definition mark_as_done 
    where "l u I. mark_as_done l u I  do {
    (_,I)WHILET 
      (λ(l,I). l<u) 
      (λ(l,I). do { ASSERT (l<length S); RETURN (Suc l,I(S!l  DONE))}) 
      (l,I);
    RETURN I
  }"

  definition mark_as_done_abs where
    "l u I. mark_as_done_abs l u I 
     (λv. if v{S!j | j. lj  j<u} then Some DONE else I v)"

  lemma mark_as_done_aux:
    fixes l u I
    shows "l<u; ulength S  mark_as_done l u I 
     SPEC (λr. r = mark_as_done_abs l u 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. lj  j<l'} then Some DONE else I v)
           ll'  l'u"
        and R="measure (λ(l',_). u-l')" 
      ]
      refine_vcg)
    
    apply (auto intro!: ext simp: less_Suc_eq)
    done    

  definition "pop_impl  
    do {
      let lsi = length B - 1;
      ASSERT (lsi<length B);
      I  mark_as_done (seg_start lsi) (seg_end lsi) I;
      ASSERT (B[]);
      let S = 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 (j,succs) = last P;
      ASSERT (length B - 1 < length B);
      if j  seg_start (length B - 1) then do {
        ASSERT (succs{});
        v  SPEC (λx. xsuccs);
        let succs = succs - {v};
        ASSERT (P[]  length P - 1 < length P);
        let P = (if succs={} then butlast P else P[length P - 1 := (j,succs)]);
        RETURN (Some v,(S,B,I,P))
      } else RETURN (None,(S,B,I,P))
    }" 


  definition "find_seg_impl j  find_max_nat (length B) (λi. B!ij)"

  lemma (in GS_invar) find_seg_impl:
    "j<length S  find_seg_impl j = find_seg j"
    unfolding find_seg_impl_def
    thm find_max_nat_correct
    apply (subst find_max_nat_correct)
    apply (simp add: B0)
    apply (simp add: B0)
    apply (simp add: find_seg_def)
    done


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

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

end

lemma (in -) GS_initial_correct: 
  assumes REL: "(I,D)oGS_rel"
  assumes A: "v0D"
  shows "GS.α (GS_initial_impl I v0 succs) = ([{v0}],D,{v0}×succs)" (is ?G1)
  and "GS_invar (GS_initial_impl I v0 succs)" (is ?G2)
proof -
  from REL have [simp]: "D = oGS_α I" and I: "oGS_invar 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)

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

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

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

    unfolding GS.pE_α_def apply auto []
    done

  show ?G2
    unfolding GS_initial_impl_def
    apply unfold_locales
    apply auto
    done
qed

context GS_invar
begin
  lemma push_correct:
    assumes A: "v(set p_α)" and B: "vD_α"
    shows "GS.α (push_impl v succs) = (p_α@[{v}],D_α,pE_α  {v}×succs)" 
      (is ?G1)
    and "GS_invar (push_impl v succs)" (is ?G2)
  proof -

    note [simp] = Let_def

    have A1: "GS.D_α (push_impl v succs) = D_α"
      using B
      by (auto simp: push_impl_def GS.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.p_α (push_impl v succs) = p_α @ [{v}]"
      unfolding push_impl_def GS.p_α_def GS.seg_def[abs_def] 
        GS.seg_start_def GS.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.pE_α (push_impl v succs) = pE_α  {v} × succs"
      unfolding push_impl_def GS.pE_α_def
      using P_bound
      apply (force simp: nth_append elim!: iexI2)
      done

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

    show ?G2
      apply unfold_locales
      unfolding push_impl_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) []
      
      using P_sorted P_distinct P_bound apply (auto simp: sorted_append) [3]
      done
  qed

  lemma no_last_out_P_aux:
    assumes NE: "p_α[]" and NS: "pE_α  last p_α × UNIV = {}"
    shows "set P  {0..<last B} × UNIV"
  proof -
    {
      fix j I
      assume jII: "(j,I)set P"
        and JL: "last Bj"
      with P_bound have JU: "j<length S" and INE: "I{}" by auto
      with JL JU have "S!j  last p_α"
        using NE
        unfolding p_α_def 
        apply (auto 
          simp: last_map seg_def seg_start_def seg_end_def last_conv_nth) 
        done
      moreover from jII have "{S!j} × I  pE_α" unfolding pE_α_def
        by auto
      moreover note INE NS
      ultimately have False by blast
    } thus ?thesis by fastforce
  qed

  lemma pop_correct:
    assumes NE: "p_α[]" and NS: "pE_α  last p_α × UNIV = {}"
    shows "pop_impl 
       GS_rel (SPEC (λr. r=(butlast p_α, D_α  last p_α, pE_α)))"
  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  n0" 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 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,
      P)"

    have ABS: "GS.α ci = (butlast p_α, D_α  last p_α, pE_α)"
      apply (simp add: GS.α_def ci_def)
      apply (intro conjI)
      apply (auto  
        simp del: map_butlast
        simp add: map_butlast[symmetric] butlast_upt
        simp add: GS.p_α_def GS.seg_def[abs_def] GS.seg_start_def GS.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.D_α_def p_α_def last_map BNE seg_def mark_as_done_abs_def) []

      using AUX1 no_last_out_P_aux[OF NE NS]
      apply (auto simp: GS.pE_α_def mark_as_done_abs_def elim!: bex2I) []
      done

    have INV: "GS_invar 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 P_sorted P_distinct 
      apply (auto) [2]

      using P_bound no_last_out_P_aux[OF NE NS]
      apply (auto simp: in_set_conv_decomp)
      done
      

    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 (rule brI)
      apply (simp_all add: ABS INV)
      done
  qed


  lemma sel_rem_last_correct:
    assumes NE: "p_α[]"
    shows
    "sel_rem_last  (Id ×r GS_rel) (select_edge (p_α,D_α,pE_α))"
  proof -
    {
      fix l i a b b'
      have "i<length l; l!i=(a,b)  map fst (l[i:=(a,b')]) = map fst l"
        by (induct l arbitrary: i) (auto split: nat.split)
    } note map_fst_upd_snd_eq = this

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

    have INVAR: "sel_rem_last  SPEC (GS_invar 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 apply (cases P rule: rev_cases, auto) []

      apply simp

      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 P_distinct 
      apply (auto simp: map_butlast sorted_butlast distinct_butlast) [2]

      using P_bound apply (auto dest: in_set_butlastD) []

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

      using P_sorted P_distinct 
      apply (auto simp: last_conv_nth map_fst_upd_snd_eq) [2]

      using P_bound 
      apply (cases P rule: rev_cases, simp)
      apply (auto) []

      using locale_this apply (cases SBIP) apply simp
      done


    {
      assume NS: "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

        apply simp
        using P_bound apply (cases P rule: rev_cases, auto) []
        apply simp

        using no_last_out_P_aux[OF NE NS]
        apply (auto simp: seg_start_def last_conv_nth) []

        apply (cases SBIP)
        apply simp
        done
    } note SPEC_E = this

    {
      assume NON_EMPTY: "pE_αlast p_α×UNIV  {}"

      then obtain j succs P' where 
        EFMT: "P = P'@[(j,succs)]"
        unfolding pE_α_def
        by (cases P rule: rev_cases) auto
        
      with P_bound have J_UPPER: "j<length S" and SNE: "succs{}" 
        by auto

      have J_LOWER: "seg_start (length B - Suc 0)  j"
      proof (rule ccontr)
        assume "¬(seg_start (length B - Suc 0)  j)"
        hence "j < seg_start (length B - 1)" by simp
        with P_sorted EFMT 
        have P_bound': "set P  {0..<seg_start (length B - 1)} × UNIV"
          by (auto simp: sorted_append)
        hence "pE_α  last p_α×UNIV = {}"
          by (auto 
            simp: p_α_def last_conv_nth seg_def pE_α_def S_idx_uniq seg_end_def)
        thus False using NON_EMPTY by simp
      qed

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

      from EFMT have SSS: "{S!j}×succspE_α"
        unfolding pE_α_def
        by auto


      {
        fix v
        assume "vsuccs"
        with SJL SSS have G: "(S!j,v)pE_α  last p_α×UNIV" by auto
        
        {
          fix j' succs'
          assume "S ! j' = S ! j" "(j', succs')  set P'"
          with J_UPPER P_bound S_idx_uniq EFMT have "j'=j" by auto
          with P_distinct (j', succs')  set P' EFMT have False by auto
        } note AUX3=this

        have G1: "GS.pE_α (S,B,I,P' @ [(j, succs - {v})]) = pE_α - {(S!j, v)}"
          unfolding GS.pE_α_def using AUX3
          by (auto simp: EFMT)
        
        {
          assume "succs{v}"
          hence "GS.pE_α (S,B,I,P' @ [(j, succs - {v})]) = GS.pE_α (S,B,I,P')"
            unfolding GS.pE_α_def by auto

          with G1 have "GS.pE_α (S,B,I,P') = pE_α - {(S!j, v)}" by simp
        } 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)(pE_αlast p_α×UNIV) 
           GS.α 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 (frule AUX3(1))

        apply safe

        apply (drule (1) AUX3(3)) apply (auto simp: EFMT GS.α_def) []
        apply (drule AUX3(2)) apply (auto simp: GS.α_def) []
        done
    } note SPEC_NE=this

    have SPEC: "sel_rem_last  SPEC (λr. case r of 
        (None, SBIP')  SBIP' = SBIP  pE_α  last p_α × UNIV = {}  GS_invar SBIP
      | (Some v, SBIP')  u. (u, v)  pE_α  last p_α × UNIV 
                         GS.α SBIP' = (p_α, D_α, pE_α - {(u, v)})
                         GS_invar SBIP'
    )"  
      using INVAR
      apply (cases "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 (fastforce simp: br_def GS_rel_def GS.α_def)
      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 refine_vcg)
    apply (metis I_consistent in_set_conv_nth set_p_α_is_set_S)
    apply (erule S_idx_of_correct)
    apply (simp add: find_seg_impl find_seg_idx_of_correct)
    by (metis find_seg_correct(2) find_seg_impl)

  lemma collapse_correct:
    assumes A: "v(set p_α)"
    shows "collapse_impl v GS_rel (SPEC (λr. r=collapse v α))"
  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.seg_start ?SBIP' i = seg_start i"
          by (simp add: GS.seg_start_def)

        have [simp]: "GS.seg_end ?SBIP' i = seg_end (length B - 1)"
          using ILEN by (simp add: GS.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 "ifind_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.seg ?SBIP' i =  (seg ` {i..<length B})"
          unfolding GS.seg_def[abs_def]
          apply simp
          apply (rule)
          apply (auto dest!: AUX1) []

          (* The following three lines complete the proof. AUX_ex_conj_SeqSI
            and all stuff 
            below would be unnecessary, if smt would be allowed for AFP.
          apply (auto simp: seg_start_def seg_end_def split: if_split_asm)
          apply (smt distinct_sorted_mono[OF B_sorted B_distinct])
          apply (smt distinct_sorted_mono[OF B_sorted B_distinct] B_in_bound')
          *)

          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 (hide_lams, no_types) Suc_lessD Suc_lessI less_trans_Suc
           B_in_bound')
         done
      } note AUX2 = this
      
      from ILEN have "GS.p_α (S, take (Suc i) B, I, P) = collapse_aux p_α i"
        unfolding GS.p_α_def collapse_aux_def
        apply (simp add: min_absorb2 drop_map)
        apply (rule conjI)
        apply (auto 
          simp: GS.seg_def[abs_def] GS.seg_start_def GS.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.α (S, take (Suc (idx_of p_α v)) B, I, P)"
      unfolding GS.α_def
      using idx_of_props[OF p_α_disjoint_sym A]
      by (simp add: AUX1)
    } note ABS=this

    {
      have "GS_invar (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]
        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 find_seg_impl)
      unfolding GS_rel_def
      apply (rule brI)
        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: "fg  f x  g x" by auto

context fr_graph begin
  definition "push_impl v s  GS.push_impl s v (E``{v})" 
  lemmas push_impl_def_opt = 
    push_impl_def[abs_def, 
    THEN ext_def, THEN opt_GSdef, unfolded GS.push_impl_def GS_sel_simps]

  text ‹Definition for presentation›
  lemma "push_impl v (S,B,I,P)  (S@[v], B@[length S], I(vSTACK (length S)),
    if E``{v}={} then P else P@[(length S,E``{v})])"
    unfolding push_impl_def GS.push_impl_def GS.P_def GS.S_def
    by (auto simp: Let_def)

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

  lemma push_refine:
    assumes A: "(s,(p,D,pE))GS_rel" "(v,v')Id"
    assumes B: "v(set p)" "vD"
    shows "(push_impl v s, push v' (p,D,pE))GS_rel"
  proof -
    from A have [simp]: "p=GS.p_α s  D=GS.D_α s  pE=GS.pE_α s" "v'=v" 
      and INV: "GS_invar s"
      by (auto simp add: GS_rel_def br_def GS_α_split)

    from INV B show ?thesis
      by (auto 
        simp: GS_rel_def br_def GS_invar.push_correct push_impl_def push_def)
  qed

  definition "pop_impl s  GS.pop_impl s"
  lemmas pop_impl_def_opt = 
    pop_impl_def[abs_def, THEN opt_GSdef, unfolded GS.pop_impl_def
    GS.mark_as_done_def GS.seg_start_def GS.seg_end_def 
    GS_sel_simps]

  lemma pop_refine:
    assumes A: "(s,(p,D,pE))GS_rel"
    assumes B: "p  []" "pE  last p × UNIV = {}"
    shows "pop_impl s  GS_rel (RETURN (pop (p,D,pE)))"
  proof -
    from A have [simp]: "p=GS.p_α s  D=GS.D_α s  pE=GS.pE_α s" 
      and INV: "GS_invar s"
      by (auto simp add: GS_rel_def br_def GS_α_split)

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

  thm pop_refine[no_vars]

  definition "collapse_impl v s  GS.collapse_impl s v"
  lemmas collapse_impl_def_opt = 
    collapse_impl_def[abs_def, 
    THEN ext_def, THEN opt_GSdef, unfolded GS.collapse_impl_def GS_sel_simps]

  lemma collapse_refine:
    assumes A: "(s,(p,D,pE))GS_rel" "(v,v')Id"
    assumes B: "v'(set p)"
    shows "collapse_impl v s GS_rel (RETURN (collapse v' (p,D,pE)))"
  proof -
    from A have [simp]: "p=GS.p_α s  D=GS.D_α s  pE=GS.pE_α s" "v'=v" 
      and INV: "GS_invar s"
      by (auto simp add: GS_rel_def br_def GS_α_split)

    show ?thesis
      unfolding collapse_impl_def[abs_def]
      apply (rule order_trans[OF GS_invar.collapse_correct])
      using INV B by (simp_all add: GS.α_def RETURN_def)
  qed

  definition "select_edge_impl s  GS.sel_rem_last s"
  lemmas select_edge_impl_def_opt = 
    select_edge_impl_def[abs_def, 
      THEN opt_GSdef, 
      unfolded GS.sel_rem_last_def GS.seg_start_def GS_sel_simps]

  lemma select_edge_refine: 
    assumes A: "(s,(p,D,pE))GS_rel"
    assumes NE: "p  []"
    shows "select_edge_impl s  (Id ×r GS_rel) (select_edge (p,D,pE))"
  proof -
    from A have [simp]: "p=GS.p_α s  D=GS.D_α s  pE=GS.pE_α s" 
      and INV: "GS_invar 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  GS_initial_impl I v0 (E``{v0})"

  lemma initial_refine:
    "v0D0; (I,D0)oGS_rel; (v0i,v0)Id 
     (initial_impl v0i I,initial v0 D0)GS_rel"
    unfolding initial_impl_def GS_rel_def br_def
    apply (simp_all add: GS_initial_correct)
    apply (auto simp: initial_def)
    done


  definition "path_is_empty_impl s  GS.S s = []"
  lemma path_is_empty_refine: 
    "GS_invar s  path_is_empty_impl s  GS.p_α s=[]"
    unfolding path_is_empty_impl_def GS.p_α_def GS_invar.empty_eq
    by auto

  definition (in GS) "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.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.is_on_stack_impl_def GS_sel_simps]

  lemma is_on_stack_refine:
    " GS_invar s   is_on_stack_impl v s  v(set (GS.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) "is_done_impl v 
     case I v of Some DONE  True | _  False"

  lemma (in GS_invar) is_done_impl_correct:
    shows "is_done_impl v  vD_α"
    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  True | _  False"

  definition "is_done_impl v s  GS.is_done_impl s v"

  lemma is_done_orefine:
    " oGS_invar s   is_done_oimpl v s  voGS_α 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 s   is_done_impl v s  vGS.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)

end

subsection ‹Refined Skeleton Algorithm›

context fr_graph begin

  lemma I_to_outer:
    assumes "((S, B, I, P), ([], D, {}))  GS_rel"
    shows "(I,D)oGS_rel"
    using assms
    unfolding GS_rel_def oGS_rel_def br_def oGS_α_def GS.α_def GS.D_α_def GS_invar_def oGS_invar_def
    apply (auto simp: GS.p_α_def)
    done
  
  
  definition skeleton_impl :: "'v oGS nres" where
    "skeleton_impl  do {
      stat_start_nres;
      let I=Map.empty;
      r  FOREACHi (λit I. outer_invar it (oGS_α I)) V0 (λv0 I0. do {
        if ¬is_done_oimpl v0 I0 then do {
          let s = initial_impl v0 I0;

          (S,B,I,P)WHILEIT (invar v0 (oGS_α I0) o GS.α)
            (λs. ¬path_is_empty_impl s) (λs.
          do {
            ― ‹Select edge from end of path›
            (vo,s)  select_edge_impl s;

            case vo of 
              Some v  do {
                if is_on_stack_impl v s then do {
                  collapse_impl v s
                } else if ¬is_done_impl v s then do {
                  ― ‹Edge to new node. Append to path›
                  RETURN (push_impl v s)
                } else do {
                  ― ‹Edge to done node. Skip›
                  RETURN s
                }
              }
            | None  do {
                ― ‹No more outgoing edges from current node on path›
                pop_impl s
              }
          }) s;
          RETURN I
        } else
          RETURN I0
      }) I;
      stat_stop_nres;
      RETURN r
    }"

  subsubsection ‹Correctness Theorem›

  lemma "skeleton_impl  oGS_rel skeleton"
    using [[goals_limit = 1]]
    unfolding skeleton_impl_def skeleton_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.α_def oGS_rel_def oGS_α_def 
      is_on_stack_refine path_is_empty_refine is_done_refine is_done_orefine
    )

    done

  lemmas skeleton_refines 
    = select_edge_refine push_refine pop_refine collapse_refine 
      initial_refine oinitial_refine
  lemmas skeleton_refine_simps 
    = GS_rel_def br_def GS.α_def oGS_rel_def oGS_α_def 
      is_on_stack_refine path_is_empty_refine is_done_refine is_done_orefine

  text ‹Short proof, for presentation›
  context
    notes [[goals_limit = 1]]
    notes [refine] = inj_on_id bind_refine'
  begin
  lemma "skeleton_impl  oGS_rel skeleton"
    unfolding skeleton_impl_def skeleton_def
    by (refine_rcg skeleton_refines, refine_dref_type)
       (vc_solve (nopre) solve: asm_rl I_to_outer simp: skeleton_refine_simps)  

  end

end

end

Theory Gabow_SCC

section ‹Enumerating the SCCs of a Graph \label{sec:scc}›
theory Gabow_SCC
imports Gabow_Skeleton
begin

text ‹
  As a first variant, we implement an algorithm that computes a list of SCCs 
  of a graph, in topological order. This is the standard variant described by
  Gabow~\cite{Gabow2000}.
›

section ‹Specification›
context fr_graph
begin
  text ‹We specify a distinct list that covers all reachable nodes and
    contains SCCs in topological order›

  definition "compute_SCC_spec  SPEC (λl. 
    distinct l  (set l) = E*``V0  (Uset l. is_scc E U) 
     (i j. i<j  j<length l  l!j × l!i  E* = {}) )"
end

section ‹Extended Invariant›

locale cscc_invar_ext = fr_graph G
  for G :: "('v,'more) graph_rec_scheme" + 
  fixes l :: "'v set list" and D :: "'v set"
  assumes l_is_D: "(set l) = D" ― ‹The output contains all done CNodes›
  assumes l_scc: "set l  Collect (is_scc E)" ― ‹The output contains only SCCs›
  assumes l_no_fwd: "i j. i<j; j<length l  l!j × l!i  E* = {}" 
    ― ‹The output contains no forward edges›
begin
  lemma l_no_empty: "{}set l" using l_scc by (auto simp: in_set_conv_decomp)
end
  
locale cscc_outer_invar_loc = outer_invar_loc G it D + cscc_invar_ext G l D
  for G :: "('v,'more) graph_rec_scheme" and it l D 
begin
  lemma locale_this: "cscc_outer_invar_loc G it l D" by unfold_locales
  lemma abs_outer_this: "outer_invar_loc G it D" by unfold_locales
end

locale cscc_invar_loc = invar_loc G v0 D0 p D pE + cscc_invar_ext G l D
  for G :: "('v,'more) graph_rec_scheme" and v0 D0 and l :: "'v set list" 
  and p D pE
begin
  lemma locale_this: "cscc_invar_loc G v0 D0 l p D pE" by unfold_locales
  lemma invar_this: "invar_loc G v0 D0 p D pE" by unfold_locales
end

context fr_graph
begin
  definition "cscc_outer_invar  λit (l,D). cscc_outer_invar_loc G it l D"
  definition "cscc_invar  λv0 D0 (l,p,D,pE). cscc_invar_loc G v0 D0 l p D pE"
end

section ‹Definition of the SCC-Algorithm›

context fr_graph
begin
  definition compute_SCC :: "'v set list nres" where
    "compute_SCC  do {
      let so = ([],{});
      (l,D)  FOREACHi cscc_outer_invar V0 (λv0 (l,D0). do {
        if v0D0 then do {
          let s = (l,initial v0 D0);

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

            ASSERT (p[]);
            case vo of 
              Some v  do {
                if v  (set p) then do {
                  ― ‹Collapse›
                  RETURN (l,collapse v (p,D,pE))
                } else if vD then do {
                  ― ‹Edge to new node. Append to path›
                  RETURN (l,push v (p,D,pE))
                } else RETURN (l,p,D,pE)
              }
            | None  do {
                ― ‹No more outgoing edges from current node on path›
                ASSERT (pE  last p × UNIV = {});
                let V = last p;
                let (p,D,pE) = pop (p,D,pE);
                let l = V#l;
                RETURN (l,p,D,pE)
              }
          }) s;
          ASSERT (p=[]  pE={});
          RETURN (l,D)
        } else
          RETURN (l,D0)
      }) so;
      RETURN l
    }"
end

section ‹Preservation of Invariant Extension›
context cscc_invar_ext
begin
  lemma l_disjoint: 
    assumes A: "i<j" "j<length l"
    shows "l!i  l!j = {}"
  proof (rule disjointI)
    fix u
    assume "ul!i" "ul!j"
    with l_no_fwd A show False by auto
  qed

  corollary l_distinct: "distinct l"
    using l_disjoint l_no_empty
    by (metis distinct_conv_nth inf_idem linorder_cases nth_mem)
end

context fr_graph
begin
  definition "cscc_invar_part  λ(l,p,D,pE). cscc_invar_ext G l D"

  lemma cscc_invarI[intro?]:
    assumes "invar v0 D0 PDPE"
    assumes "invar v0 D0 PDPE  cscc_invar_part (l,PDPE)"
    shows "cscc_invar v0 D0 (l,PDPE)"
    using assms
    unfolding initial_def cscc_invar_def invar_def
    apply (simp split: prod.split_asm)
    apply intro_locales
    apply (simp add: invar_loc_def)
    apply (simp add: cscc_invar_part_def cscc_invar_ext_def)
    done

  thm cscc_invarI[of v_0 D_0 s l]

  lemma cscc_outer_invarI[intro?]:
    assumes "outer_invar it D"
    assumes "outer_invar it D  cscc_invar_ext G l D"
    shows "cscc_outer_invar it (l,D)"
    using assms
    unfolding initial_def cscc_outer_invar_def outer_invar_def
    apply (simp split: prod.split_asm)
    apply intro_locales
    apply (simp add: outer_invar_loc_def)
    apply (simp add: cscc_invar_ext_def)
    done

  lemma cscc_invar_initial[simp, intro!]:
    assumes A: "v0it" "v0D0"
    assumes INV: "cscc_outer_invar it (l,D0)"
    shows "cscc_invar_part (l,initial v0 D0)"
  proof -
    from INV interpret cscc_outer_invar_loc G it l D0 
      unfolding cscc_outer_invar_def by simp
    
    show ?thesis
      unfolding cscc_invar_part_def initial_def
      apply simp
      by unfold_locales
  qed

  lemma cscc_invar_pop:
    assumes INV: "cscc_invar v0 D0 (l,p,D,pE)"
    assumes "invar v0 D0 (pop (p,D,pE))"
    assumes NE[simp]: "p[]"
    assumes NO': "pE  (last p × UNIV) = {}"
    shows "cscc_invar_part (last p # l, pop (p,D,pE))"
  proof -
    from INV interpret cscc_invar_loc G v0 D0 l p D pE 
      unfolding cscc_invar_def by simp

    have AUX_l_scc: "is_scc E (last p)"
      unfolding is_scc_pointwise
    proof safe
      {
        assume "last p = {}" thus False 
          using p_no_empty by (cases p rule: rev_cases) auto 
      }

      fix u v
      assume "ulast p" "vlast p"
      with p_sc[of "last p"] have "(u,v)  (lvE  last p × last p)*" by auto
      with lvE_ss_E show "(u,v)(E  last p × last p)*"
        by (metis Int_mono equalityE rtrancl_mono_mp)
      
      fix u'
      assume "u'last p" "(u,u')E*" "(u',v)E*"

      from u'last p ulast p (u,u')E*
        and rtrancl_reachable_induct[OF order_refl lastp_un_D_closed[OF NE NO']]
      have "u'D" by auto
      with (u',v)E* and rtrancl_reachable_induct[OF order_refl D_closed] 
      have "vD" by auto
      with vlast p p_not_D show False by (cases p rule: rev_cases) auto
    qed

    {
      fix i j
      assume A: "i<j" "j<Suc (length l)"
      have "l ! (j - Suc 0) × (last p # l) ! i  E* = {}"
      proof (rule disjointI, safe)
        fix u v
        assume "(u, v)  E*" "u  l ! (j - Suc 0)" "v  (last p # l) ! i"
        from u  l ! (j - Suc 0) A have "u(set l)"
          by (metis Ex_list_of_length Suc_pred UnionI length_greater_0_conv 
            less_nat_zero_code not_less_eq nth_mem) 
        with l_is_D have "uD" by simp
        with rtrancl_reachable_induct[OF order_refl D_closed] (u,v)E* 
        have "vD" by auto

        show False proof cases
          assume "i=0" hence "vlast p" using v  (last p # l) ! i by simp
          with p_not_D vD show False by (cases p rule: rev_cases) auto
        next
          assume "i0" with v  (last p # l) ! i have "vl!(i - 1)" by auto
          with l_no_fwd[of "i - 1" "j - 1"] 
            and u  l ! (j - Suc 0) (u, v)  E* i0 A
          show False by fastforce 
        qed
      qed
    } note AUX_l_no_fwd = this

    show ?thesis
      unfolding cscc_invar_part_def pop_def apply simp
      apply unfold_locales
      apply clarsimp_all
      using l_is_D apply auto []

      using l_scc AUX_l_scc apply auto []

      apply (rule AUX_l_no_fwd, assumption+) []
      done
  qed

  thm cscc_invar_pop[of v_0 D_0 l p D pE]

  lemma cscc_invar_unchanged: 
    assumes INV: "cscc_invar v0 D0 (l,p,D,pE)"
    shows "cscc_invar_part (l,p',D,pE')"
    using INV unfolding cscc_invar_def cscc_invar_part_def cscc_invar_loc_def
    by simp

  corollary cscc_invar_collapse:
    assumes INV: "cscc_invar v0 D0 (l,p,D,pE)"
    shows "cscc_invar_part (l,collapse v (p',D,pE'))"
    unfolding collapse_def
    by (simp add: cscc_invar_unchanged[OF INV])

  corollary cscc_invar_push:
    assumes INV: "cscc_invar v0 D0 (l,p,D,pE)"
    shows "cscc_invar_part (l,push v (p',D,pE'))"
    unfolding push_def
    by (simp add: cscc_invar_unchanged[OF INV])


  lemma cscc_outer_invar_initial: "cscc_invar_ext G [] {}"
    by unfold_locales auto


  lemma cscc_invar_outer_newnode:
    assumes A: "v0D0" "v0it" 
    assumes OINV: "cscc_outer_invar it (l,D0)"
    assumes INV: "cscc_invar v0 D0 (l',[],D',pE)"
    shows "cscc_invar_ext G l' D'"
  proof -
    from OINV interpret cscc_outer_invar_loc G it l D0 
      unfolding cscc_outer_invar_def by simp
    from INV interpret inv: cscc_invar_loc G v0 D0 l' "[]" D' pE 
      unfolding cscc_invar_def by simp
    
    show ?thesis 
      by unfold_locales

  qed

  lemma cscc_invar_outer_Dnode:
    assumes "cscc_outer_invar it (l, D)"
    shows "cscc_invar_ext G l D"
    using assms
    by (simp add: cscc_outer_invar_def cscc_outer_invar_loc_def)
    
  lemmas cscc_invar_preserve = invar_preserve
    cscc_invar_initial
    cscc_invar_pop cscc_invar_collapse cscc_invar_push cscc_invar_unchanged 
    cscc_outer_invar_initial cscc_invar_outer_newnode cscc_invar_outer_Dnode

  text ‹On termination, the invariant implies the specification›
  lemma cscc_finI:
    assumes INV: "cscc_outer_invar {} (l,D)"
    shows fin_l_is_scc: "Uset l  is_scc E U"
    and fin_l_distinct: "distinct l"
    and fin_l_is_reachable: "(set l) = E* `` V0"
    and fin_l_no_fwd: "i<j; j<length l  l!j ×l!i  E* = {}"
  proof -
    from INV interpret cscc_outer_invar_loc G "{}" l D
      unfolding cscc_outer_invar_def by simp

    show "Uset l  is_scc E U" using l_scc by auto

    show "distinct l" by (rule l_distinct)

    show "(set l) = E* `` V0"
      using fin_outer_D_is_reachable[OF outer_invar_this] l_is_D
      by auto

    show "i<j; j<length l  l!j ×l!i  E* = {}"
      by (rule l_no_fwd)

  qed

end

section ‹Main Correctness Proof›

context fr_graph 
begin
  lemma invar_from_cscc_invarI: "cscc_invar v0 D0 (L,PDPE)  invar v0 D0 PDPE"
    unfolding cscc_invar_def invar_def
    apply (simp split: prod.splits)
    unfolding cscc_invar_loc_def by simp

  lemma outer_invar_from_cscc_invarI: 
    "cscc_outer_invar it (L,D) outer_invar it D"
    unfolding cscc_outer_invar_def outer_invar_def
    apply (simp split: prod.splits)
    unfolding cscc_outer_invar_loc_def by simp

  text ‹With the extended invariant and the auxiliary lemmas, the actual 
    correctness proof is straightforward:›
  theorem compute_SCC_correct: "compute_SCC  compute_SCC_spec"
  proof -
    note [[goals_limit = 2]]
    note [simp del] = Union_iff

    show ?thesis
      unfolding compute_SCC_def compute_SCC_spec_def select_edge_def select_def
      apply (refine_rcg
        WHILEIT_rule[where R="inv_image (abs_wf_rel v0) snd" for v0]
        refine_vcg 
      )

      apply (vc_solve
        rec: cscc_invarI cscc_outer_invarI
        solve: cscc_invar_preserve cscc_finI
        intro: invar_from_cscc_invarI outer_invar_from_cscc_invarI
        dest!: sym[of "pop A" for A]
        simp: pE_fin'[OF invar_from_cscc_invarI] finite_V0
      )
      apply auto
      done
  qed


  text ‹Simple proof, for presentation›
  context 
    notes [refine]=refine_vcg
    notes [[goals_limit = 1]]
  begin
    theorem "compute_SCC  compute_SCC_spec"
      unfolding compute_SCC_def compute_SCC_spec_def select_edge_def select_def
      by (refine_rcg 
        WHILEIT_rule[where R="inv_image (abs_wf_rel v0) snd" for v0])
      (vc_solve 
        rec: cscc_invarI cscc_outer_invarI solve: cscc_invar_preserve cscc_finI
        intro: invar_from_cscc_invarI outer_invar_from_cscc_invarI
        dest!: sym[of "pop A" for A]
        simp: pE_fin'[OF invar_from_cscc_invarI] finite_V0, auto)
  end

end


section ‹Refinement to Gabow's Data Structure›

context GS begin
  definition "seg_set_impl l u  do {
    (_,res)  WHILET
      (λ(l,_). l<u) 
      (λ(l,res). do { 
        ASSERT (l<length S); 
        let x = S!l;
        ASSERT (xres); 
        RETURN (Suc l,insert x res)
      }) 
      (l,{});
      
    RETURN res
  }"

  lemma seg_set_impl_aux:
    fixes l u
    shows "l<u; ulength S; distinct S  seg_set_impl l u 
     SPEC (λr. r = {S!j | j. lj  j<u})"
    unfolding seg_set_impl_def
    apply (refine_rcg 
      WHILET_rule[where 
        I="λ(l',res). res = {S!j | j. lj  j<l'}  ll'  l'u"
        and R="measure (λ(l',_). u-l')" 
      ]
      refine_vcg)

    apply (auto simp: less_Suc_eq nth_eq_iff_index_eq)
    done

  lemma (in GS_invar) seg_set_impl_correct:
    assumes "i<length B"
    shows "seg_set_impl (seg_start i) (seg_end i)  SPEC (λr. r=p_α!i)"
    apply (refine_rcg order_trans[OF seg_set_impl_aux] refine_vcg)

    using assms 
    apply (simp_all add: seg_start_less_end seg_end_bound S_distinct) [3]

    apply (auto simp: p_α_def assms seg_def) []
    done

  definition "last_seg_impl 
     do {
      ASSERT (length B - 1 < length B);
      seg_set_impl (seg_start (length B - 1)) (seg_end (length B - 1))
    }"

  lemma (in GS_invar) last_seg_impl_correct:
    assumes "p_α  []"
    shows "last_seg_impl  SPEC (λr. r=last p_α)"
    unfolding last_seg_impl_def
    apply (refine_rcg order_trans[OF seg_set_impl_correct] refine_vcg)
    using assms apply (auto simp add: p_α_def last_conv_nth)
    done

end

context fr_graph
begin

  definition "last_seg_impl s  GS.last_seg_impl s"
  lemmas last_seg_impl_def_opt = 
    last_seg_impl_def[abs_def, THEN opt_GSdef, 
      unfolded GS.last_seg_impl_def GS.seg_set_impl_def 
    GS.seg_start_def GS.seg_end_def GS_sel_simps] 
    (* TODO: Some potential for optimization here: the assertion 
      guarantees that length B - 1 + 1 = length B !*)

  lemma last_seg_impl_refine: 
    assumes A: "(s,(p,D,pE))GS_rel"
    assumes NE: "p[]"
    shows "last_seg_impl s  Id (RETURN (last p))"
  proof -
    from A have 
      [simp]: "p=GS.p_α s  D=GS.D_α s  pE=GS.pE_α s" 
        and INV: "GS_invar s"
      by (auto simp add: GS_rel_def br_def GS_α_split)

    show ?thesis
      unfolding last_seg_impl_def[abs_def]
      apply (rule order_trans[OF GS_invar.last_seg_impl_correct])
      using INV NE
      apply (simp_all) 
      done
  qed

  definition compute_SCC_impl :: "'v set list nres" where
    "compute_SCC_impl  do {
      stat_start_nres;
      let so = ([],Map.empty);
      (l,D)  FOREACHi (λit (l,s). cscc_outer_invar it (l,oGS_α s)) 
        V0 (λv0 (l,I0). do {
          if ¬is_done_oimpl v0 I0 then do {
            let ls = (l,initial_impl v0 I0);

            (l,(S,B,I,P))WHILEIT (λ(l,s). cscc_invar v0 (oGS_α I0) (l,GS.α s))
              (λ(l,s). ¬path_is_empty_impl s) (λ(l,s).
            do {
              ― ‹Select edge from end of path›
              (vo,s)  select_edge_impl s;

              case vo of 
                Some v  do {
                  if is_on_stack_impl v s then do {
                    scollapse_impl v s;
                    RETURN (l,s)
                  } else if ¬is_done_impl v s then do {
                    ― ‹Edge to new node. Append to path›
                    RETURN (l,push_impl v s)
                  } else do {
                    ― ‹Edge to done node. Skip›
                    RETURN (l,s)
                  }
                }
              | None  do {
                  ― ‹No more outgoing edges from current node on path›
                  scc  last_seg_impl s;
                  spop_impl s;
                  let l = scc#l;
                  RETURN (l,s)
                }
            }) (ls);
            RETURN (l,I)
          } else RETURN (l,I0)
      }) so;
      stat_stop_nres;
      RETURN l
    }"

  lemma compute_SCC_impl_refine: "compute_SCC_impl  Id compute_SCC"
  proof -
    note [refine2] = bind_Let_refine2[OF last_seg_impl_refine]

    have [refine2]: "s' p D pE l' l v' v. 
      (s',(p,D,pE))GS_rel;
      (l',l)Id;
      (v',v)Id;
      v(set p)
      do { s'collapse_impl v' s'; RETURN (l',s') } 
       (Id ×r GS_rel) (RETURN (l,collapse v (p,D,pE)))"
      apply (refine_rcg order_trans[OF collapse_refine] refine_vcg)
      apply assumption+
      apply (auto simp add: pw_le_iff refine_pw_simps)
      done

    note [[goals_limit = 1]]
    show ?thesis
      unfolding compute_SCC_impl_def compute_SCC_def
      apply (refine_rcg
        bind_refine'
        select_edge_refine push_refine 
        pop_refine
        (*collapse_refine*) 
        initial_refine
        oinitial_refine
        (*last_seg_impl_refine*)
        prod_relI IdI
        inj_on_id
      )

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

      done
  qed

end

end

Theory Find_Path

section ‹Safety-Property Model-Checker\label{sec:find_path}›
theory Find_Path
imports
  CAVA_Automata.Digraph
  CAVA_Base.CAVA_Code_Target
begin
  section ‹Finding Path to Error›
  text ‹
    This function searches a graph and a set of start nodes for a reachable
    node that satisfies some property, and returns a path to such a node iff it
    exists.
›
  definition "find_path E U0 P  do {
    ASSERT (finite U0);
    ASSERT (finite (E*``U0));
    SPEC (λp. case p of 
      Some (p,v)  u0U0. path E u0 p v  P v  (vset p. ¬ P v)
    | None  u0U0. vE*``{u0}. ¬P v)
    }"

  lemma find_path_ex_rule:
    assumes "finite U0"
    assumes "finite (E*``U0)"
    assumes "vE*``U0. P v"
    shows "find_path E U0 P  SPEC (λr. 
      p v. r = Some (p,v)  P v  (vset p. ¬P v)  (u0U0. path E u0 p v))"
    unfolding find_path_def
    using assms
    by (fastforce split: option.splits) 

  subsection ‹Nontrivial Paths›

  definition "find_path1 E u0 P  do { 
    ASSERT (finite (E*``{u0}));
    SPEC (λp. case p of 
      Some (p,v)  path E u0 p v  P v  p[]
    | None  vE+``{u0}. ¬P v)}"

  lemma (in -) find_path1_ex_rule:
    assumes "finite (E*``{u0})"
    assumes "vE+``{u0}. P v"
    shows "find_path1 E u0 P  SPEC (λr. 
      p v. r = Some (p,v)  p[]  P v  path E u0 p v)"
    unfolding find_path1_def
    using assms
    by (fastforce split: option.splits) 

end

Theory Gabow_GBG

section ‹Lasso Finding Algorithm for Generalized B\"uchi Graphs \label{sec:gbg}›
theory Gabow_GBG
imports 
  Gabow_Skeleton 
  CAVA_Automata.Lasso
  Find_Path
begin

(* TODO: convenience locale, consider merging this with invariants *)
locale igb_fr_graph = 
  igb_graph G + fr_graph G
  for G :: "('Q,'more) igb_graph_rec_scheme"

lemma igb_fr_graphI:
  assumes "igb_graph G"
  assumes "finite ((g_E G)* `` g_V0 G)"
  shows "igb_fr_graph G"
proof -
  interpret igb_graph G by fact
  show ?thesis using assms(2) by unfold_locales
qed

text ‹
  We implement an algorithm that computes witnesses for the 
  non-emptiness of Generalized B\"uchi Graphs (GBG).
›

section ‹Specification›
context igb_graph
begin
  definition ce_correct 
    ― ‹Specifies a correct counter-example›
    where
    "ce_correct Vr Vl  (pr pl. 
        Vr  E*``V0  Vl  E*``V0 ― ‹Only reachable nodes are covered›
       set prVr  set plVl     ― ‹The paths are inside the specified sets›
       Vl×Vl  (E  Vl×Vl)*      ― ‹Vl› is mutually connected›
       Vl×Vl  E  {}            ― ‹Vl› is non-trivial›
       is_lasso_prpl (pr,pl))    ― ‹Paths form a lasso›
    "     

  definition find_ce_spec :: "('Q set × 'Q set) option nres" where
    "find_ce_spec  SPEC (λr. case r of
      None  (prpl. ¬is_lasso_prpl prpl)
    | Some (Vr,Vl)  ce_correct Vr Vl
    )"

  definition find_lasso_spec :: "('Q list × 'Q list) option nres" where
    "find_lasso_spec  SPEC (λr. case r of
      None  (prpl. ¬is_lasso_prpl prpl)
    | Some prpl  is_lasso_prpl prpl
    )"

end

section ‹Invariant Extension›

text ‹Extension of the outer invariant:›
context igb_fr_graph
begin
  definition no_acc_over
    ― ‹Specifies that there is no accepting cycle touching a set of nodes›
    where
    "no_acc_over D  ¬(vD. pl. pl[]  path E v pl v  
    (i<num_acc. qset pl. iacc q))"

  definition "fgl_outer_invar_ext  λit (brk,D). 
    case brk of None  no_acc_over D | Some (Vr,Vl)  ce_correct Vr Vl"

  definition "fgl_outer_invar  λit (brk,D). case brk of 
    None  outer_invar it D  no_acc_over D
  | Some (Vr,Vl)  ce_correct Vr Vl"
  
end

text ‹Extension of the inner invariant:›
locale fgl_invar_loc = 
  invar_loc G v0 D0 p D pE 
  + igb_graph G
  for G :: "('Q, 'more) igb_graph_rec_scheme"
  and v0 D0 and brk :: "('Q set × 'Q set) option" and p D pE +
  assumes no_acc: "brk=None  ¬(v pl. pl[]  path lvE v pl v  
    (i<num_acc. qset pl. iacc q))" ― ‹No accepting cycle over 
      visited edges›
  assumes acc: "brk=Some (Vr,Vl)  ce_correct Vr Vl"
begin
  lemma locale_this: "fgl_invar_loc G v0 D0 brk p D pE"
    by unfold_locales
  lemma invar_loc_this: "invar_loc G v0 D0 p D pE" by unfold_locales
  lemma eas_gba_graph_this: "igb_graph G" by unfold_locales
end

definition (in igb_graph) "fgl_invar v0 D0  
  λ(brk, p, D, pE). fgl_invar_loc G v0 D0 brk p D pE"

section ‹Definition of the Lasso-Finding Algorithm›

context igb_fr_graph
begin
  definition find_ce :: "('Q set × 'Q set) option nres" where
    "find_ce  do {
      let D = {};
      (brk,_)FOREACHci fgl_outer_invar V0 
        (λ(brk,_). brk=None) 
        (λv0 (brk,D0). do {
          if v0D0 then do {
            let s = (None,initial v0 D0);

            (brk,p,D,pE)  WHILEIT (fgl_invar v0 D0)
              (λ(brk,p,D,pE). brk=None  p  []) (λ(_,p,D,pE). 
            do {
              ― ‹Select edge from end of path›
              (vo,(p,D,pE))  select_edge (p,D,pE);

              ASSERT (p[]);
              case vo of 
                Some v  do {
                  if v  (set p) then do {
                    ― ‹Collapse›
                    let (p,D,pE) = collapse v (p,D,pE);

                    ASSERT (p[]);

                    if i<num_acc. qlast p. iacc q then
                      RETURN (Some ((set (butlast p)),last p),p,D,pE)
                    else
                      RETURN (None,p,D,pE)
                  } else if vD then do {
                    ― ‹Edge to new node. Append to path›
                    RETURN (None,push v (p,D,pE))
                  } else RETURN (None,p,D,pE)
                }
              | None  do {
                  ― ‹No more outgoing edges from current node on path›
                  ASSERT (pE  last p × UNIV = {});
                  RETURN (None,pop (p,D,pE))
                }
            }) s;
            ASSERT (brk=None  (p=[]  pE={}));
            RETURN (brk,D)
          } else 
            RETURN (brk,D0)
      }) (None,D);
      RETURN brk
    }"
end

section ‹Invariant Preservation›


context igb_fr_graph
begin

  definition "fgl_invar_part  λ(brk, p, D, pE). 
    fgl_invar_loc_axioms G brk p D pE"

  lemma fgl_outer_invarI[intro?]:
    "
      brk=None  outer_invar it D; 
      brk=None  outer_invar it D  fgl_outer_invar_ext it (brk,D) 
       fgl_outer_invar it (brk,D)"
    unfolding outer_invar_def fgl_outer_invar_ext_def fgl_outer_invar_def
    apply (auto split: prod.splits option.splits)
    done

  lemma fgl_invarI[intro?]:
    " invar v0 D0 PDPE; 
       invar v0 D0 PDPE  fgl_invar_part (B,PDPE) 
      fgl_invar v0 D0 (B,PDPE)"
    unfolding invar_def fgl_invar_part_def fgl_invar_def
    apply (simp split: prod.split_asm)
    apply intro_locales
    apply (simp add: invar_loc_def)
    apply assumption
    done


  lemma fgl_invar_initial: 
    assumes OINV: "fgl_outer_invar it (None,D0)"
    assumes A: "v0it" "v0D0"
    shows "fgl_invar_part (None, initial v0 D0)"
  proof -
    from OINV interpret outer_invar_loc G it D0 
      by (simp add: fgl_outer_invar_def outer_invar_def)

    from OINV have no_acc: "no_acc_over D0"
      by (simp add: fgl_outer_invar_def fgl_outer_invar_ext_def)

    {
      fix v pl

      assume "pl  []" and P: "path (vE [{v0}] D0 (E  {v0} × UNIV)) v pl v"
      hence 1: "vD0"
        by (cases pl) (auto simp: path_cons_conv vE_def touched_def)
      have 2: "path E v pl v" using path_mono[OF vE_ss_E P] .
      note 1 2
    } note AUX1=this


    show ?thesis
      unfolding fgl_invar_part_def
      apply (simp split: prod.splits add: initial_def)
      apply unfold_locales
      using v0D0
      using AUX1 no_acc unfolding no_acc_over_def apply blast
      by simp
  qed

  lemma fgl_invar_pop:
    assumes INV: "fgl_invar v0 D0 (None,p,D,pE)"
    assumes INV': "invar v0 D0 (pop (p,D,pE))"
    assumes NE[simp]: "p[]"
    assumes NO': "pE  last p × UNIV = {}"
    shows "fgl_invar_part (None, pop (p,D,pE))"
  proof -
    from INV interpret fgl_invar_loc G v0 D0 None p D pE 
      by (simp add: fgl_invar_def)

    show ?thesis
      apply (unfold fgl_invar_part_def pop_def)
      apply (simp split: prod.splits)
      apply unfold_locales
      unfolding vE_pop[OF NE]

      using no_acc apply auto []
      apply simp
      done
  qed

  lemma fgl_invar_collapse_ce_aux:
    assumes INV: "invar v0 D0 (p, D, pE)"
    assumes NE[simp]: "p[]"
    assumes NONTRIV: "vE p D pE  (last p × last p)  {}"
    assumes ACC: "i<num_acc. qlast p. iacc q"
    shows "fgl_invar_part (Some ((set (butlast p)), last p), p, D, pE)"
  proof -
    from INV interpret invar_loc G v0 D0 p D pE by (simp add: invar_def)
    txt ‹The last collapsed node on the path contains states from all 
      accepting sets.
      As it is strongly connected and reachable, we get a counter-example. 
      Here, we explicitely construct the lasso.›

    let ?Er = "E  ((set (butlast p)) × UNIV)"

    txt ‹We choose a node in the last Cnode, that is reachable only using
      former Cnodes.›

    obtain w where "(v0,w)?Er*" "wlast p"
    proof cases
      assume "length p = 1"
      hence "v0last p"
        using root_v0 
        by (cases p) auto
      thus thesis by (auto intro: that)
    next
      assume "length p1"
      hence "length p > 1" by (cases p) auto
      hence "Suc (length p - 2) < length p" by auto
      from p_connected'[OF this] obtain u v where
        UIP: "up!(length p - 2)" and VIP: "vp!(length p - 1)" and "(u,v)lvE"
        using ‹length p > 1 by auto
      from root_v0 have V0IP: "v0p!0" by (cases p) auto
      
      from VIP have "vlast p" by (cases p rule: rev_cases) auto

      from pathI[OF V0IP UIP] ‹length p > 1 have 
        "(v0,u)(lvE  (set (butlast p)) × (set (butlast p)))*"
        (is "_  *")  
        by (simp add: path_seg_butlast)
      also have "  ?Er" using lvE_ss_E by auto
      finally (rtrancl_mono_mp[rotated]) have "(v0,u)?Er*" .
      also note (u,v)lvE› UIP hence "(u,v)?Er" using lvE_ss_E ‹length p > 1 
        apply (auto simp: Bex_def in_set_conv_nth)
        by (metis One_nat_def Suc_lessE ‹Suc (length p - 2) < length p 
          diff_Suc_1 length_butlast nth_butlast)
      finally show ?thesis by (rule that) fact 
    qed
    then obtain "pr" where 
      P_REACH: "path E v0 pr w" and 
      R_SS: "set pr  (set (butlast p))"
      apply -
      apply (erule rtrancl_is_path)
      apply (frule path_nodes_edges)
      apply (auto 
        dest!: order_trans[OF _ image_Int_subset] 
        dest: path_mono[of _ E, rotated])
      done

    have [simp]: "last p = p!(length p - 1)" by (cases p rule: rev_cases) auto

    txt ‹From that node, we construct a lasso by inductively appending a path
      for each accepting set›
    {
      fix na
      assume na_def: "na = num_acc"

      have "pl. pl[] 
         path (lvE  last p×last p) w pl w 
         (i<num_acc. qset pl. iacc q)"
        using ACC
        unfolding na_def[symmetric]
      proof (induction na)
        case 0 

        from NONTRIV obtain u v 
          where "(u,v)lvE  last p × last p" "ulast p" "vlast p"
          by auto
        from cnode_connectedI wlast p ulast p 
        have "(w,u)(lvE  last p × last p)*"
          by auto
        also note (u,v)lvE  last p × last p
        also (rtrancl_into_trancl1) from cnode_connectedI vlast p wlast p 
        have "(v,w)(lvE  last p × last p)*"
          by auto
        finally obtain pl where "pl[]" "path (lvE  last p × last p) w pl w"
          by (rule trancl_is_path)
        thus ?case by auto
      next
        case (Suc n)
        from Suc.prems have "i<n. qlast p. iacc q" by auto
        with Suc.IH obtain pl where IH: 
          "pl[]" 
          "path (lvE  last p × last p) w pl w" 
          "i<n. qset pl. iacc q" 
          by blast
  
        from Suc.prems obtain v where "vlast p" and "nacc v" by auto
        from cnode_connectedI wlast p vlast p 
        have "(w,v)(lvE  last p × last p)*" by auto
        then obtain pl1 where P1: "path (lvE  last p × last p) w pl1 v" 
          by (rule rtrancl_is_path)
        also from cnode_connectedI wlast p vlast p 
        have "(v,w)(lvE  last p × last p)*" by auto
        then obtain pl2 where P2: "path (lvE  last p × last p) v pl2 w"
          by (rule rtrancl_is_path)
        also (path_conc) note IH(2)
        finally (path_conc) have 
          P: "path (lvE  last p × last p) w (pl1@pl2@pl) w"
          by simp
        moreover from IH(1) have "pl1@pl2@pl  []" by simp
        moreover have "i'<n. qset (pl1@pl2@pl). i'acc q" using IH(3) by auto
        moreover have "vset (pl1@pl2@pl)" using P1 P2 P IH(1)
          apply (cases pl2, simp_all add: path_cons_conv path_conc_conv)
          apply (cases pl, simp_all add: path_cons_conv)
          apply (cases pl1, simp_all add: path_cons_conv)
          done
        with nacc v have "qset (pl1@pl2@pl). nacc q" by auto
        ultimately show ?case
          apply (intro exI conjI)
          apply assumption+
          apply (auto elim: less_SucE)
          done
      qed
    }
    then obtain pl where pl: "pl[]" "path (lvE  last p×last p) w pl w" 
      "i<num_acc. qset pl. iacc q" by blast
    hence "path E w pl w" and L_SS: "set pl  last p"
      apply -
      apply (frule path_mono[of _ E, rotated])
      using lvE_ss_E
      apply auto [2]

      apply (drule path_nodes_edges)
      apply (drule order_trans[OF _ image_Int_subset])
      apply auto []
      done

    have LASSO: "is_lasso_prpl (pr,pl)"
      unfolding is_lasso_prpl_def is_lasso_prpl_pre_def
      using ‹path E w pl w P_REACH pl by auto
    
    from p_sc have "last p × last p  (lvE  last p × last p)*" by auto
    with lvE_ss_E have VL_CLOSED: "last p × last p  (E  last p × last p)*"
      apply (erule_tac order_trans)
      apply (rule rtrancl_mono)
      by blast

    have NONTRIV': "last p × last p  E  {}"
      by (metis Int_commute NONTRIV disjoint_mono lvE_ss_E subset_refl)

    from order_trans[OF path_touched touched_reachable]
    have LP_REACH: "last p  E*``V0" 
      and BLP_REACH: "(set (butlast p))  E*``V0"
      apply -
      apply (cases p rule: rev_cases)
      apply simp
      apply auto []

      apply (cases p rule: rev_cases)
      apply simp
      apply auto []
      done
      
    show ?thesis
      apply (simp add: fgl_invar_part_def)
      apply unfold_locales
      apply simp

      using LASSO R_SS L_SS VL_CLOSED NONTRIV' LP_REACH BLP_REACH
      unfolding ce_correct_def 
      apply simp 
      apply blast
      done

  qed

  lemma fgl_invar_collapse_ce:
    fixes u v
    assumes INV: "fgl_invar v0 D0 (None,p,D,pE)"
    defines "pE'  pE - {(u,v)}"
    assumes CFMT: "(p',D',pE'') = collapse v (p,D,pE')"
    assumes INV': "invar v0 D0 (p',D',pE'')"
    assumes NE[simp]: "p[]"
    assumes E: "(u,v)pE" and "ulast p"
    assumes BACK: "v(set p)"
    assumes ACC: "i<num_acc. qlast p'. iacc q"
    defines i_def: "i  idx_of p v"
    shows "fgl_invar_part (
      Some ((set (butlast p')), last p'), 
      collapse v (p,D,pE'))"
  proof -

    from CFMT have p'_def: "p' = collapse_aux p i" and [simp]: "D'=D" "pE''=pE'"
      by (simp_all add: collapse_def i_def)

    from INV interpret fgl_invar_loc G v0 D0 None p D pE 
      by (simp add: fgl_invar_def)

    from idx_of_props[OF BACK] have "i<length p" and "vp!i" 
      by (simp_all add: i_def)

    have "ulast p'" 
      using ulast p i<length p 
      unfolding p'_def collapse_aux_def
      apply (simp add: last_drop last_snoc)
      by (metis Misc.last_in_set drop_eq_Nil last_drop not_le)
    moreover have "vlast p'" 
      using vp!i i<length p 
      unfolding p'_def collapse_aux_def
      by (metis UnionI append_Nil Cons_nth_drop_Suc in_set_conv_decomp last_snoc)
    ultimately have "vE p' D pE'  last p' × last p'  {}" 
      unfolding p'_def pE'_def by (auto simp: E)
    
    have "p'[]" by (simp add: p'_def collapse_aux_def)

    have [simp]: "collapse v (p,D,pE') = (p',D,pE')" 
      unfolding collapse_def p'_def i_def
      by simp

    show ?thesis
      apply simp
      apply (rule fgl_invar_collapse_ce_aux) 
      using INV' apply simp
      apply fact+
      done
  qed

  lemma fgl_invar_collapse_nce:
    fixes u v
    assumes INV: "fgl_invar v0 D0 (None,p,D,pE)"
    defines "pE'  pE - {(u,v)}"
    assumes CFMT: "(p',D',pE'') = collapse v (p,D,pE')"
    assumes INV': "invar v0 D0 (p',D',pE'')"
    assumes NE[simp]: "p[]"
    assumes E: "(u,v)pE" and "ulast p"
    assumes BACK: "v(set p)"
    assumes NACC: "j<num_acc" "qlast p'. jacc q"
    defines "i  idx_of p v"
    shows "fgl_invar_part (None, collapse v (p,D,pE'))"
  proof -
    from CFMT have p'_def: "p' = collapse_aux p i" and [simp]: "D'=D" "pE''=pE'"
      by (simp_all add: collapse_def i_def)

    have [simp]: "collapse v (p,D,pE') = (p',D,pE')" 
      by (simp add: collapse_def p'_def i_def)

    from INV interpret fgl_invar_loc G v0 D0 None p D pE 
      by (simp add: fgl_invar_def)

    from INV' interpret inv': invar_loc G v0 D0 p' D pE' by (simp add: invar_def)

    define vE' where "vE' = vE p' D pE'"

    have vE'_alt: "vE' = insert (u,v) lvE"
      by (simp add: vE'_def p'_def pE'_def E)

    from idx_of_props[OF BACK] have "i<length p" and "vp!i" 
      by (simp_all add: i_def)

    have "ulast p'" 
      using ulast p i<length p
      unfolding p'_def collapse_aux_def
      apply (simp add: last_drop last_snoc)
      by (metis Misc.last_in_set drop_eq_Nil last_drop leD)
    moreover have "vlast p'" 
      using vp!i i<length p 
      unfolding p'_def collapse_aux_def
      by (metis UnionI append_Nil Cons_nth_drop_Suc in_set_conv_decomp last_snoc)
    ultimately have "vE'  last p' × last p'  {}" 
      unfolding vE'_alt by (auto)
    
    have "p'[]" by (simp add: p'_def collapse_aux_def)

    {
      txt ‹
        We show that no visited strongly connected component contains states
        from all acceptance sets.›
      fix w pl
      txt ‹For this, we chose a non-trivial loop inside the visited edges›
      assume P: "path vE' w pl w" and NT: "pl[]"
      txt ‹And show that there is one acceptance set disjoint with the nodes
        of the loop›
      have "i<num_acc. qset pl. iacc q"
      proof cases
        assume "set pl  last p' = {}" 
          ― ‹Case: The loop is outside the last Cnode›
        with path_restrict[OF P] ulast p' vlast p' have "path lvE w pl w"
          apply -
          apply (drule path_mono[of _ lvE, rotated])
          unfolding vE'_alt
          by auto
        with no_acc NT show ?thesis by auto
      next
        assume "set pl  last p'  {}" 
          ― ‹Case: The loop touches the last Cnode›
        txt ‹Then, the loop must be completely inside the last CNode›
        from inv'.loop_in_lastnode[folded vE'_def, OF P p'[] this] 
        have "wlast p'" "set pl  last p'" .
        with NACC show ?thesis by blast
      qed
    } note AUX_no_acc = this

    show ?thesis
      apply (simp add: fgl_invar_part_def)
      apply unfold_locales
      using AUX_no_acc[unfolded vE'_def] apply auto []
      
      apply simp
      done
  qed

  lemma collapse_ne: "([],D',pE')  collapse v (p,D,pE)"
    by (simp add: collapse_def collapse_aux_def Let_def)

  lemma fgl_invar_push:
    assumes INV: "fgl_invar v0 D0 (None,p,D,pE)"
    assumes BRK[simp]: "brk=None" 
    assumes NE[simp]: "p[]"
    assumes E: "(u,v)pE" and UIL: "ulast p"
    assumes VNE: "v(set p)" "vD"
    assumes INV': "invar v0 D0 (push v (p,D,pE - {(u,v)}))"
    shows "fgl_invar_part (None, push v (p,D,pE - {(u,v)}))"
  proof -
    from INV interpret fgl_invar_loc G v0 D0 None p D pE 
      by (simp add: fgl_invar_def)

    define pE' where "pE' = (pE - {(u,v)}  E{v}×UNIV)"

    have [simp]: "push v (p,D,pE - {(u,v)}) = (p@[{v}],D,pE')"
      by (simp add: push_def pE'_def)

    from INV' interpret inv': invar_loc G v0 D0 "(p@[{v}])" D "pE'"
      by (simp add: invar_def)

    note defs_fold = vE_push[OF E UIL VNE, folded pE'_def]

    {
      txt ‹We show that there still is no loop that contains all accepting
        nodes. For this, we choose some loop.›
      fix w pl
      assume P: "path (insert (u,v) lvE) w pl w" and [simp]: "pl[]"
      have "i<num_acc. qset pl. iacc q" 
      proof cases
        assume "vset pl" ― ‹Case: The newly pushed last cnode is on the loop›
        txt ‹Then the loop is entirely on the last cnode›
        with inv'.loop_in_lastnode[unfolded defs_fold, OF P]
        have [simp]: "w=v" and SPL: "set pl = {v}" by auto
        txt ‹However, we then either have that the last cnode is contained in
          the last but one cnode, or that there is a visited edge inside the
          last cnode.›
        from P SPL have "u=v  (v,v)lvE" 
          apply (cases pl) apply (auto simp: path_cons_conv)
          apply (case_tac list)
          apply (auto simp: path_cons_conv)
          done
        txt ‹Both leads to a contradiction›
        hence False proof
          assume "u=v" ― ‹This is impossible, as @{text "u"} was on the 
            original path, but @{text "v"} was not›
          with UIL VNE show False by auto
        next
          assume "(v,v)lvE" ― ‹This is impossible, as all visited edges are
            from touched nodes, but @{text "v"} was untouched›
          with vE_touched VNE show False unfolding touched_def by auto
        qed
        thus ?thesis ..
      next
        assume A: "vset pl" 
          ― ‹Case: The newly pushed last cnode is not on the loop›
        txt ‹Then, the path lays inside the old visited edges›
        have "path lvE w pl w" 
        proof -
          have "wset pl" using P by (cases pl) (auto simp: path_cons_conv)
          with A show ?thesis using path_restrict[OF P]
            apply -
            apply (drule path_mono[of _ lvE, rotated])
            apply (cases pl, auto) []
            
            apply assumption
            done
        qed
        txt ‹And thus, the proposition follows from the invariant on the old
          state›
        with no_acc show ?thesis 
          apply simp
          using pl[] 
          by blast
      qed
    } note AUX_no_acc = this

    show ?thesis
      unfolding fgl_invar_part_def
      apply simp
      apply unfold_locales
      unfolding defs_fold

      using AUX_no_acc apply auto []
      
      apply simp
      done
  qed


  lemma fgl_invar_skip:
    assumes INV: "fgl_invar v0 D0 (None,p,D,pE)"
    assumes BRK[simp]: "brk=None" 
    assumes NE[simp]: "p[]"
    assumes E: "(u,v)pE" and UIL: "ulast p"
    assumes VID: "vD"
    assumes INV': "invar v0 D0 (p, D, (pE - {(u,v)}))"
    shows "fgl_invar_part (None, p, D, (pE - {(u,v)}))"
  proof -
    from INV interpret fgl_invar_loc G v0 D0 None p D pE 
      by (simp add: fgl_invar_def)
    from INV' interpret inv': invar_loc G v0 D0 p D "(pE - {(u,v)})" 
      by (simp add: invar_def)

    {
      txt ‹We show that there still is no loop that contains all accepting
        nodes. For this, we choose some loop.›
      fix w pl
      assume P: "path (insert (u,v) lvE) w pl w" and [simp]: "pl[]"
      from P have "i<num_acc. qset pl. iacc q" 
      proof (cases rule: path_edge_rev_cases)
        case no_use ― ‹Case: The loop does not use the new edge›
        txt ‹The proposition follows from the invariant for the old state›
        with no_acc show ?thesis 
          apply simp
          using pl[] 
          by blast
      next
        case (split p1 p2) ― ‹Case: The loop uses the new edge›
        txt ‹As done is closed under transitions, the nodes of the edge have
          already been visited›
        from split(2) D_closed_vE_rtrancl 
        have WID: "wD" 
          using VID by (auto dest!: path_is_rtrancl)
        from split(1) WID D_closed_vE_rtrancl have "uD"
          apply (cases rule: path_edge_cases)
          apply (auto dest!: path_is_rtrancl)
          done
        txt ‹Which is a contradition to the assumptions›
        with UIL p_not_D have False by (cases p rule: rev_cases) auto
        thus ?thesis ..
      qed
    } note AUX_no_acc = this


    show ?thesis 
      apply (simp add: fgl_invar_part_def)
      apply unfold_locales
      unfolding vE_remove[OF NE E]

      using AUX_no_acc apply auto []

      apply simp
      done

  qed

  lemma fgl_outer_invar_initial: 
    "outer_invar V0 {}  fgl_outer_invar_ext V0 (None, {})"
    unfolding fgl_outer_invar_ext_def
    apply (simp add: no_acc_over_def)
    done

  lemma fgl_outer_invar_brk:
    assumes INV: "fgl_invar v0 D0 (Some (Vr,Vl),p,D,pE)"
    shows "fgl_outer_invar_ext anyIt (Some (Vr,Vl), anyD)"
  proof -
    from INV interpret fgl_invar_loc G v0 D0 "Some (Vr,Vl)" p D pE
      by (simp add: fgl_invar_def)

    from acc show ?thesis by (simp add: fgl_outer_invar_ext_def)
  qed

  lemma fgl_outer_invar_newnode_nobrk:
    assumes A: "v0D0" "v0it" 
    assumes OINV: "fgl_outer_invar it (None,D0)"
    assumes INV: "fgl_invar v0 D0 (None,[],D',pE)"
    shows "fgl_outer_invar_ext (it-{v0}) (None,D')"
  proof -
    from OINV interpret outer_invar_loc G it D0 
      unfolding fgl_outer_invar_def outer_invar_def by simp

    from INV interpret inv: fgl_invar_loc G v0 D0 None "[]" D' pE 
      unfolding fgl_invar_def by simp

    from inv.pE_fin have [simp]: "pE = {}" by simp

    { fix v pl
      assume A: "vD'" "path E v pl v"
      have "path (E  D' × UNIV) v pl v"
        apply (rule path_mono[OF _ path_restrict_closed[OF inv.D_closed A]])
        by auto
    } note AUX1=this

    show ?thesis
      unfolding fgl_outer_invar_ext_def
      apply simp
      using inv.no_acc AUX1 
      apply (auto simp add: vE_def touched_def no_acc_over_def) []
      done
  qed

  lemma fgl_outer_invar_newnode:
    assumes A: "v0D0" "v0it" 
    assumes OINV: "fgl_outer_invar it (None,D0)"
    assumes INV: "fgl_invar v0 D0 (brk,p,D',pE)"
    assumes CASES: "(Vr Vl. brk = Some (Vr, Vl))  p = []"
    shows "fgl_outer_invar_ext (it-{v0}) (brk,D')"
    using CASES
    apply (elim disjE1)
    using fgl_outer_invar_brk[of v0 D0 _ _ p D' pE] INV 
    apply - 
    apply (auto, assumption) []
    using fgl_outer_invar_newnode_nobrk[OF A] OINV INV apply auto []
    done

  lemma fgl_outer_invar_Dnode:
    assumes "fgl_outer_invar it (None, D)" "vD"
    shows "fgl_outer_invar_ext (it - {v}) (None, D)"
    using assms
    by (auto simp: fgl_outer_invar_def fgl_outer_invar_ext_def)

  
  lemma fgl_fin_no_lasso:
    assumes A: "fgl_outer_invar {} (None, D)"
    assumes B: "is_lasso_prpl prpl"
    shows "False"
  proof -
    obtain "pr" pl where [simp]: "prpl = (pr,pl)" by (cases prpl)
    from A have NA: "no_acc_over D" 
      by (simp add: fgl_outer_invar_def fgl_outer_invar_ext_def)

    from A have "outer_invar {} D" by (simp add: fgl_outer_invar_def)
    with fin_outer_D_is_reachable have [simp]: "D=E*``V0" by simp

    from NA B show False
      apply (simp add: no_acc_over_def is_lasso_prpl_def is_lasso_prpl_pre_def)
      apply clarsimp
      apply (blast dest: path_is_rtrancl)
      done
  qed

  lemma fgl_fin_lasso:
    assumes A: "fgl_outer_invar it (Some (Vr,Vl), D)"
    shows "ce_correct Vr Vl"
    using A by (simp add: fgl_outer_invar_def fgl_outer_invar_ext_def)


  lemmas fgl_invar_preserve = 
    fgl_invar_initial fgl_invar_push fgl_invar_pop 
    fgl_invar_collapse_ce fgl_invar_collapse_nce fgl_invar_skip
    fgl_outer_invar_newnode fgl_outer_invar_Dnode
    invar_initial outer_invar_initial fgl_invar_initial fgl_outer_invar_initial
    fgl_fin_no_lasso fgl_fin_lasso

end

section ‹Main Correctness Proof›

context igb_fr_graph
begin
  lemma outer_invar_from_fgl_invarI: 
    "fgl_outer_invar it (None,D)  outer_invar it D"
    unfolding fgl_outer_invar_def outer_invar_def
    by (simp split: prod.splits)

  lemma invar_from_fgl_invarI: "fgl_invar v0 D0 (B,PDPE)  invar v0 D0 PDPE"
    unfolding fgl_invar_def invar_def
    apply (simp split: prod.splits)
    unfolding fgl_invar_loc_def by simp
   
  theorem find_ce_correct: "find_ce  find_ce_spec"
  proof -
    note [simp del] = Union_iff

    show ?thesis
      unfolding find_ce_def find_ce_spec_def select_edge_def select_def
      apply (refine_rcg
        WHILEIT_rule[where R="inv_image (abs_wf_rel v0) snd" for v0]
        refine_vcg 
      )
      
      using [[goals_limit = 5]]

      apply (vc_solve
        rec: fgl_invarI fgl_outer_invarI
        intro: invar_from_fgl_invarI outer_invar_from_fgl_invarI
        dest!: sym[of "collapse a b" for a b]
        simp: collapse_ne
        simp: pE_fin'[OF invar_from_fgl_invarI] finite_V0
        solve: invar_preserve 
        solve: asm_rl[of "_  _ = {}"]
        solve: fgl_invar_preserve)
      done
  qed
end

section "Emptiness Check"
text ‹Using the lasso-finding algorithm, we can define an emptiness check›

context igb_fr_graph
begin
  definition "abs_is_empty  do {
    ce  find_ce;
    RETURN (ce = None)
    }"

  theorem abs_is_empty_correct: 
    "abs_is_empty  SPEC (λres. res  (r. ¬is_acc_run r))"
    unfolding abs_is_empty_def
    apply (refine_rcg refine_vcg 
      order_trans[OF find_ce_correct, unfolded find_ce_spec_def])
    unfolding ce_correct_def
    using lasso_accepted accepted_lasso
    apply (clarsimp split: option.splits)
    apply (metis is_lasso_prpl_of_lasso surj_pair)
    by (metis is_lasso_prpl_conv)

  definition "abs_is_empty_ce  do {
    ce  find_ce;
    case ce of
      None  RETURN None
    | Some (Vr,Vl)  do {
        ASSERT (pr pl. set pr  Vr  set pl  Vl  Vl × Vl  (E  Vl×Vl)* 
           is_lasso_prpl (pr,pl));
        (pr,pl)  SPEC (λ(pr,pl). 
           set pr  Vr 
           set pl  Vl 
           Vl × Vl  (E  Vl×Vl)*
           is_lasso_prpl (pr,pl));
        RETURN (Some (pr,pl))
      }
    }"

  theorem abs_is_empty_ce_correct: "abs_is_empty_ce  SPEC (λres. case res of
      None  (r. ¬is_acc_run r)
    | Some (pr,pl)  is_acc_run (prplω)
    )"
    unfolding abs_is_empty_ce_def
    apply (refine_rcg refine_vcg 
      order_trans[OF find_ce_correct, unfolded find_ce_spec_def])

    apply (clarsimp_all simp: ce_correct_def)

    using accepted_lasso finite_reachableE_V0 apply (metis is_lasso_prpl_of_lasso surj_pair)
    apply blast
    apply (simp add: lasso_prpl_acc_run)
    done

end

section ‹Refinement›
text ‹
  In this section, we refine the lasso finding algorithm to use efficient
  data structures. First, we explicitely keep track of the set of acceptance
  classes for every c-node on the path. Second, we use Gabow's data structure
  to represent the path.
›

subsection ‹Addition of Explicit Accepting Sets›
text ‹In a first step, we explicitely keep track of the current set of
  acceptance classes for every c-node on the path.›

type_synonym 'a abs_gstate = "nat set list × 'a abs_state"
type_synonym 'a ce = "('a set × 'a set) option"
type_synonym 'a abs_gostate = "'a ce × 'a set"

context igb_fr_graph
begin

  definition gstate_invar :: "'Q abs_gstate  bool" where 
    "gstate_invar  λ(a,p,D,pE). a = map (λV. (acc`V)) p"

  definition "gstate_rel  br snd gstate_invar"

  lemma gstate_rel_sv[relator_props,simp,intro!]: "single_valued gstate_rel"
    by (simp add: gstate_rel_def)

  definition (in -) gcollapse_aux 
    :: "nat set list  'a set list  nat  nat set list × 'a set list"
    where "gcollapse_aux a p i  
      (take i a @ [(set (drop i a))],take i p @ [(set (drop i p))])"

  definition (in -) gcollapse :: "'a  'a abs_gstate  'a abs_gstate" 
    where "gcollapse v APDPE  
    let 
      (a,p,D,pE)=APDPE; 
      i=idx_of p v;
      (a,p) = gcollapse_aux a p i
    in (a,p,D,pE)"

  definition "gpush v s  
    let
      (a,s) = s
    in
      (a@[acc v],push v s)"

  definition "gpop s 
    let (a,s) = s in (butlast a,pop s)"

  definition ginitial :: "'Q  'Q abs_gostate  'Q abs_gstate" 
    where "ginitial v0 s0  ([acc v0], initial v0 (snd s0))"

  definition goinitial :: "'Q abs_gostate" where "goinitial  (None,{})"
  definition go_is_no_brk :: "'Q abs_gostate  bool" 
    where "go_is_no_brk s  fst s = None"
  definition goD :: "'Q abs_gostate  'Q set" where "goD s  snd s"
  definition goBrk :: "'Q abs_gostate  'Q ce" where "goBrk s  fst s"
  definition gto_outer :: "'Q ce  'Q abs_gstate  'Q abs_gostate" 
    where "gto_outer brk s  let (A,p,D,pE)=s in (brk,D)"

  definition "gselect_edge s  do {
    let (a,s)=s; 
    (r,s)select_edge s;
    RETURN (r,a,s) 
  }"

  definition gfind_ce :: "('Q set × 'Q set) option nres" where
    "gfind_ce  do {
      let os = goinitial;
      osFOREACHci fgl_outer_invar V0 (go_is_no_brk) (λv0 s0. do {
        if v0goD s0 then do {
          let s = (None,ginitial v0 s0);

          (brk,a,p,D,pE)  WHILEIT (λ(brk,a,s). fgl_invar v0 (goD s0) (brk,s))
            (λ(brk,a,p,D,pE). brk=None  p  []) (λ(_,a,p,D,pE). 
          do {
            ― ‹Select edge from end of path›
            (vo,(a,p,D,pE))  gselect_edge (a,p,D,pE);

            ASSERT (p[]);
            case vo of 
              Some v  do {
                if v  (set p) then do {
                  ― ‹Collapse›
                  let (a,p,D,pE) = gcollapse v (a,p,D,pE);

                  ASSERT (p[]);
                  ASSERT (a[]);

                  if last a = {0..<num_acc} then
                    RETURN (Some ((set (butlast p)),last p),a,p,D,pE)
                  else
                    RETURN (None,a,p,D,pE)
                } else if vD then do {
                  ― ‹Edge to new node. Append to path›
                  RETURN (None,gpush v (a,p,D,pE))
                } else RETURN (None,a,p,D,pE)
              }
            | None  do {
                ― ‹No more outgoing edges from current node on path›
                ASSERT (pE  last p × UNIV = {});
                RETURN (None,gpop (a,p,D,pE))
              }
          }) s;
          ASSERT (brk=None  (p=[]  pE={}));
          RETURN (gto_outer brk (a,p,D,pE))
        } else RETURN s0
    }) os;
    RETURN (goBrk os)
  }"

  lemma gcollapse_refine:
    "(v',v)Id; (s',s)gstate_rel 
       (gcollapse v' s',collapse v s)gstate_rel"
    unfolding gcollapse_def collapse_def collapse_aux_def gcollapse_aux_def 
    apply (simp add: gstate_rel_def br_def Let_def)
    unfolding gstate_invar_def[abs_def]
    apply (auto split: prod.splits simp: take_map drop_map)
    done

  lemma gpush_refine:
    "(v',v)Id; (s',s)gstate_rel  (gpush v' s',push v s)gstate_rel"
    unfolding gpush_def push_def 
    apply (simp add: gstate_rel_def br_def)
    unfolding gstate_invar_def[abs_def]
    apply (auto split: prod.splits)
    done

  lemma gpop_refine:
    "(s',s)gstate_rel  (gpop s',pop s)gstate_rel"
    unfolding gpop_def pop_def 
    apply (simp add: gstate_rel_def br_def)
    unfolding gstate_invar_def[abs_def]
    apply (auto split: prod.splits simp: map_butlast)
    done

  lemma ginitial_refine:
    "(ginitial x (None, b), initial x b)  gstate_rel"
    unfolding ginitial_def gstate_rel_def br_def gstate_invar_def initial_def
    by auto

  lemma oinitial_b_refine: "((None,{}),(None,{}))Id×rId" by simp

  lemma gselect_edge_refine: "(s',s)gstate_rel  gselect_edge s' 
    (Idoption_rel ×r gstate_rel) (select_edge s)"
    unfolding gselect_edge_def select_edge_def
    apply (simp add: pw_le_iff refine_pw_simps prod_rel_sv
      split: prod.splits option.splits)

    apply (auto simp: gstate_rel_def br_def gstate_invar_def)
    done

  lemma last_acc_impl:
    assumes "p[]"
    assumes "((a',p',D',pE'),(p,D,pE))gstate_rel"
    shows "(last a' = {0..<num_acc}) = (i<num_acc. qlast p. iacc q)"
    using assms acc_bound unfolding gstate_rel_def br_def gstate_invar_def
    by (auto simp: last_map)

  lemma fglr_aux1:
    assumes V: "(v',v)Id" and S: "(s',s)gstate_rel" 
      and P: "a' p' D' pE' p D pE. ((a',p',D',pE'),(p,D,pE))gstate_rel 
       f' a' p' D' pE' R (f p D pE)"
    shows "(let (a',p',D',pE') = gcollapse v' s' in f' a' p' D' pE') 
       R (let (p,D,pE) = collapse v s in f p D pE)"
    apply (auto split: prod.splits)
    apply (rule P)
    using gcollapse_refine[OF V S]
    apply simp
    done

  lemma gstate_invar_empty: 
    "gstate_invar (a,[],D,pE)  a=[]"
    "gstate_invar ([],p,D,pE)  p=[]"
    by (auto simp add: gstate_invar_def)

  lemma find_ce_refine: "gfind_ce Id find_ce"
    unfolding gfind_ce_def find_ce_def
    unfolding goinitial_def go_is_no_brk_def[abs_def] goD_def goBrk_def 
      gto_outer_def
    using [[goals_limit = 1]]
    apply (refine_rcg 
      gselect_edge_refine prod_relI[OF IdI gpop_refine]
      prod_relI[OF IdI gpush_refine]
      fglr_aux1 last_acc_impl oinitial_b_refine
      inj_on_id
    )
    apply refine_dref_type
    apply (simp_all add: ginitial_refine)
    apply (vc_solve (nopre) 
      solve: asm_rl 
      simp: gstate_rel_def br_def gstate_invar_empty)
    done
end

subsection ‹Refinement to Gabow's Data Structure›

subsubsection ‹Preliminaries›
definition Un_set_drop_impl :: "nat  'a set list  'a set nres"
  ― ‹Executable version of @{text "⋃set (drop i A)"}, using indexing to
  access @{text "A"}
  where "Un_set_drop_impl i A  
  do {
    (_,res)  WHILET (λ(i,res). i < length A) (λ(i,res). do {
      ASSERT (i<length A);
      let res = A!i  res;
      let i = i + 1;
      RETURN (i,res)
    }) (i,{});
    RETURN res
  }"

lemma Un_set_drop_impl_correct: 
  "Un_set_drop_impl i A  SPEC (λr. r=(set (drop i A)))"
  unfolding Un_set_drop_impl_def
  apply (refine_rcg 
    WHILET_rule[where I="λ(i',res). res=(set ((drop i (take i' A))))  ii'" 
    and R="measure (λ(i',_). length A - i')"] 
    refine_vcg)
  apply (auto simp: take_Suc_conv_app_nth)
  done

schematic_goal Un_set_drop_code_aux: 
  assumes [autoref_rules]: "(es_impl,{})RRs"
  assumes [autoref_rules]: "(un_impl,(∪))RRsRRsRRs"
  shows "(?c,Un_set_drop_impl)nat_rel  RRsas_rel  RRsnres_rel"
  unfolding Un_set_drop_impl_def[abs_def]
  apply (autoref (trace, keep_goal))
  done
concrete_definition Un_set_drop_code uses Un_set_drop_code_aux

schematic_goal Un_set_drop_tr_aux: 
  "RETURN ?c  Un_set_drop_code es_impl un_impl i A"
  unfolding Un_set_drop_code_def
  by refine_transfer
concrete_definition Un_set_drop_tr for es_impl un_impl i A 
  uses Un_set_drop_tr_aux 

lemma Un_set_drop_autoref[autoref_rules]: 
  assumes "GEN_OP es_impl {} (RRs)"
  assumes "GEN_OP un_impl (∪) (RRsRRsRRs)"
  shows "(λi A. RETURN (Un_set_drop_tr es_impl un_impl i A),Un_set_drop_impl)
    nat_rel  RRsas_rel  RRsnres_rel"
  apply (intro fun_relI nres_relI)
  apply (rule order_trans[OF Un_set_drop_tr.refine])
  using Un_set_drop_code.refine[of es_impl Rs R un_impl, 
    param_fo, THEN nres_relD]
  using assms
  by simp


subsubsection ‹Actual Refinement›

type_synonym 'Q gGS = "nat set list × 'Q GS"

type_synonym 'Q goGS = "'Q ce × 'Q oGS"

context igb_graph
begin

definition gGS_invar :: "'Q gGS  bool"
  where "gGS_invar s  
  let (a,S,B,I,P) = s in 
    GS_invar (S,B,I,P)
     length a = length B
     (set a)  {0..<num_acc}
  "

definition gGS_α :: "'Q gGS  'Q abs_gstate"
  where "gGS_α s  let (a,s)=s in (a,GS.α s)"

definition "gGS_rel  br gGS_α gGS_invar"

lemma gGS_rel_sv[relator_props,intro!,simp]: "single_valued gGS_rel"
  unfolding gGS_rel_def by auto


definition goGS_invar :: "'Q goGS  bool" where
  "goGS_invar s  let (brk,ogs)=s in brk=None  oGS_invar ogs"

definition "goGS_α s  let (brk,ogs)=s in (brk,oGS_α ogs)"

definition "goGS_rel  br goGS_α goGS_invar"

lemma goGS_rel_sv[relator_props,intro!,simp]: "single_valued goGS_rel"
  unfolding goGS_rel_def by auto

end


context igb_fr_graph
begin
  lemma gGS_relE:
    assumes "(s',(a,p,D,pE))gGS_rel"
    obtains S' B' I' P' where "s'=(a,S',B',I',P')" 
      and "((S',B',I',P'),(p,D,pE))GS_rel" 
      and "length a = length B'"
      and "(set a)  {0..<num_acc}"
    using assms
    apply (cases s')
    apply (simp add: gGS_rel_def br_def gGS_α_def GS.α_def)
    apply (rule that)
    apply (simp only:)
    apply (auto simp: GS_rel_def br_def gGS_invar_def GS.α_def)
    done


  definition goinitial_impl :: "'Q goGS" 
    where "goinitial_impl  (None,Map.empty)"
  lemma goinitial_impl_refine: "(goinitial_impl,goinitial)goGS_rel"
    by (auto 
      simp: goinitial_impl_def goinitial_def goGS_rel_def br_def 
      simp: goGS_α_def goGS_invar_def oGS_α_def oGS_invar_def)

  definition gto_outer_impl :: "'Q ce  'Q gGS  'Q goGS"
    where "gto_outer_impl brk s  let (A,S,B,I,P)=s in (brk,I)"

  lemma gto_outer_refine:
    assumes A: "brk = None  (p=[]  pE={})"
    assumes B: "(s, (A,p, D, pE))  gGS_rel"
    assumes C: "(brk',brk)Id"
    shows "(gto_outer_impl brk' s,gto_outer brk (A,p,D,pE))goGS_rel"
  proof (cases s)
    fix A S B I P
    assume [simp]: "s=(A,S,B,I,P)"
    show ?thesis
      using C
      apply (cases brk)
      using assms I_to_outer[of S B I P D]
      apply (auto 
        simp: goGS_rel_def br_def goGS_α_def gto_outer_def 
              gto_outer_impl_def goGS_invar_def 
        simp: gGS_rel_def oGS_rel_def GS_rel_def gGS_α_def gGS_invar_def 
              GS.α_def) []

      using B apply (auto 
        simp: gto_outer_def gto_outer_impl_def
        simp: br_def goGS_rel_def goGS_invar_def goGS_α_def oGS_α_def
        simp: gGS_rel_def gGS_α_def GS.α_def GS.D_α_def
      )

      done
  qed

  definition "gpush_impl v s  let (a,s)=s in (a@[acc v], push_impl v s)"


  lemma gpush_impl_refine:
    assumes B: "(s',(a,p,D,pE))gGS_rel"
    assumes A: "(v',v)Id" 
    assumes PRE: "v'  (set p)" "v'  D"
    shows "(gpush_impl v' s', gpush v (a,p,D,pE))gGS_rel"
  proof -
    from B obtain S' B' I' P' where [simp]: "s'=(a,S',B',I',P')" 
      and OSR: "((S',B',I',P'),(p,D,pE))GS_rel" and L: "length a = length B'" 
      and R: "(set a)  {0..<num_acc}"
      by (rule gGS_relE)
    {
      fix S B I P S' B' I' P'
      assume "push_impl v (S, B, I, P) = (S', B', I', P')"
      hence "length B' = Suc (length B)" 
        by (auto simp add: push_impl_def GS.push_impl_def Let_def)  
    } note AUX1=this

    from push_refine[OF OSR A PRE] A L acc_bound R show ?thesis
      unfolding gpush_impl_def gpush_def
        gGS_rel_def gGS_invar_def gGS_α_def GS_rel_def br_def
      apply (auto dest: AUX1)
      done
  qed
  
  definition gpop_impl :: "'Q gGS  'Q gGS nres" 
    where "gpop_impl s  do {
    let (a,s)=s;
    spop_impl s;
    ASSERT (a[]);
    let a = butlast a;
    RETURN (a,s)
  }"

  lemma gpop_impl_refine:
    assumes A: "(s',(a,p,D,pE))gGS_rel"
    assumes PRE: "p  []" "pE  last p × UNIV = {}"
    shows "gpop_impl s'  gGS_rel (RETURN (gpop (a,p,D,pE)))"
  proof -
    from A obtain S' B' I' P' where [simp]: "s'=(a,S',B',I',P')" 
      and OSR: "((S',B',I',P'),(p,D,pE))GS_rel" and L: "length a = length B'"
      and R: "(set a)  {0..<num_acc}"
      by (rule gGS_relE)

    from PRE OSR have [simp]: "a[]" using L
      by (auto simp add: GS_rel_def br_def GS.α_def GS.p_α_def)

    {
      fix S B I P S' B' I' P'
      assume "nofail (pop_impl ((S, B, I, P)::'a GS))"
        "inres (pop_impl ((S, B, I, P)::'a GS)) (S', B', I', P')"
      hence "length B' = length B - Suc 0"
        apply (simp add: pop_impl_def GS.pop_impl_def Let_def
          refine_pw_simps)
        apply auto
        done
    } note AUX1=this

    from A L show ?thesis
      unfolding gpop_impl_def gpop_def gGS_rel_def gGS_α_def br_def
      apply (simp add: Let_def)
      using pop_refine[OF OSR PRE]
      apply (simp add: pw_le_iff refine_pw_simps split: prod.splits)
      unfolding gGS_rel_def gGS_invar_def gGS_α_def GS_rel_def GS.α_def br_def
      apply (auto dest!: AUX1 in_set_butlastD iff: Sup_le_iff)
      done
  qed
  
  definition gselect_edge_impl :: "'Q gGS  ('Q option × 'Q gGS) nres" 
    where "gselect_edge_impl s  
    do { 
      let (a,s)=s; 
      (vo,s)select_edge_impl s; 
      RETURN (vo,a,s)
    }"

  thm select_edge_refine
  lemma gselect_edge_impl_refine:
    assumes A: "(s', a, p, D, pE)  gGS_rel" 
    assumes PRE: "p  []"
    shows "gselect_edge_impl s'  (Id ×r gGS_rel) (gselect_edge (a, p, D, pE))"
  proof -
    from A obtain S' B' I' P' where [simp]: "s'=(a,S',B',I',P')" 
      and OSR: "((S',B',I',P'),(p,D,pE))GS_rel" and L: "length a = length B'"
      and R: "(set a)  {0..<num_acc}"
      by (rule gGS_relE)

    {
      fix S B I P S' B' I' P' vo
      assume "nofail (select_edge_impl ((S, B, I, P)::'a GS))"
        "inres (select_edge_impl ((S, B, I, P)::'a GS)) (vo, (S', B', I', P'))"
      hence "length B' = length B"
        apply (simp add: select_edge_impl_def GS.sel_rem_last_def refine_pw_simps
          split: if_split_asm prod.splits)
        apply auto
        done
    } note AUX1=this

    show ?thesis
      using select_edge_refine[OF OSR PRE]
      unfolding gselect_edge_impl_def gselect_edge_def
      apply (simp add: refine_pw_simps pw_le_iff prod_rel_sv)

      unfolding gGS_rel_def br_def gGS_α_def gGS_invar_def GS_rel_def GS.α_def
      apply (simp split: prod.splits)
      apply clarsimp
      using R
      apply (auto simp: L dest: AUX1)
      done
  qed


  term GS.idx_of_impl

  thm GS_invar.idx_of_correct


  definition gcollapse_impl_aux :: "'Q  'Q gGS  'Q gGS nres" where 
    "gcollapse_impl_aux v s  
    do { 
      let (A,s)=s;
      ⌦‹ASSERT (v∈⋃set (GS.p_α s));›
      i  GS.idx_of_impl s v;
      s  collapse_impl v s;
      ASSERT (i < length A);
      us  Un_set_drop_impl i A;
      let A = take i A @ [us];
      RETURN (A,s)
    }"

  term collapse
  lemma gcollapse_alt:
    "gcollapse v APDPE = ( 
      let 
        (a,p,D,pE)=APDPE; 
        i=idx_of p v;
        s=collapse v (p,D,pE);
        us=(set (drop i a));
        a = take i a @ [us]
      in (a,s))"
    unfolding gcollapse_def gcollapse_aux_def collapse_def collapse_aux_def
    by auto

  thm collapse_refine
  lemma gcollapse_impl_aux_refine:
    assumes A: "(s', a, p, D, pE)  gGS_rel" 
    assumes B: "(v',v)Id"
    assumes PRE: "v(set p)"
    shows "gcollapse_impl_aux v' s' 
        gGS_rel (RETURN (gcollapse v (a, p, D, pE)))"
  proof -
    note [simp] = Let_def

    from A obtain S' B' I' P' where [simp]: "s'=(a,S',B',I',P')" 
      and OSR: "((S',B',I',P'),(p,D,pE))GS_rel" and L: "length a = length B'"
      and R: "(set a)  {0..<num_acc}"
      by (rule gGS_relE)

    from B have [simp]: "v'=v" by simp

    from OSR have [simp]: "GS.p_α (S',B',I',P') = p"
      by (simp add: GS_rel_def br_def GS.α_def)

    from OSR PRE have PRE': "v  (set (GS.p_α (S',B',I',P')))"
      by (simp add: GS_rel_def br_def GS.α_def)

    from OSR have GS_invar: "GS_invar (S',B',I',P')" 
      by (simp add: GS_rel_def br_def)

    term GS.B
    {
      fix s
      assume "collapse v (p, D, pE) = (GS.p_α s, GS.D_α s, GS.pE_α s)"
      hence "length (GS.B s) = Suc (idx_of p v)"
        unfolding collapse_def collapse_aux_def Let_def
        apply (cases s)
        apply (auto simp: GS.p_α_def)
        apply (drule arg_cong[where f=length])
        using GS_invar.p_α_disjoint_sym[OF GS_invar]
          and PRE ‹GS.p_α (S', B', I', P') = p idx_of_props(1)[of p v]
        by simp
    } note AUX1 = this

    show ?thesis
      unfolding gcollapse_alt gcollapse_impl_aux_def
      apply simp
      apply (rule RETURN_as_SPEC_refine)
      apply (refine_rcg
        order_trans[OF GS_invar.idx_of_correct[OF GS_invar PRE']] 
        order_trans[OF collapse_refine[OF OSR B PRE, simplified]]
        refine_vcg
      )
      using PRE' apply simp
      
      apply (simp add: L)

      using Un_set_drop_impl_correct acc_bound R
      apply (