Quelle  Gabow_GBG.thy

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<sup>*</sup>``V0 ― ‹Only reachable nodes are covered›
      ∧ set pr⊆Vr ∧ set pl⊆Vl ― ‹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 ≡ ¬(∃v∈D. ∃pl. pl≠[] ∧ path E v pl v ∧
    (∀i<num_acc. ∃q∈set pl. i∈acc 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. ∃q∈set pl. i∈acc 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 v0∉D0 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. ∃q∈last p. i∈acc q then
                      RETURN (Some (∪(set (butlast p)),last p),p,D,pE)
                    else
                      RETURN (None,p,D,pE)
                  } else if v∉D 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: "v0∈it" "v0∉D0"
    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: "v∈D0"
        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 ‹v0∉D0›
      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. ∃q∈last p. i∈acc 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^*" "w∈last p"
    proof cases
      assume "length p = 1"
      hence "v0∈last p"
        using root_v0 
        by (cases p) auto
      thus thesis by (auto intro: that)
    next
      assume "length p≠1"
      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: "u∈p!(length p - 2)" and VIP: "v∈p!(length p - 1)" and "(u,v)∈lvE"
        using ‹length p > 1› by auto
      from root_v0 have V0IP: "v0∈p!0" by (cases p) auto
      
      from VIP have "v∈last 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. ∃q∈set pl. i∈acc 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" "u∈last p" "v∈last p"
          by auto
        from cnode_connectedI ‹w∈last p› ‹u∈last 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 ‹v∈last p› ‹w∈last 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. ∃q∈last p. i∈acc q" by auto
        with Suc.IH obtain pl where IH: 
          "pl≠[]" 
          "path (lvE ∩ last p × last p) w pl w" 
          "∀i<n. ∃q∈set pl. i∈acc q" 
          by blast
  
        from Suc.prems obtain v where "v∈last p" and "n∈acc v" by auto
        from cnode_connectedI ‹w∈last p› ‹v∈last 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 ‹w∈last p› ‹v∈last 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. ∃q∈set (pl1@pl2@pl). i'∈acc q" using IH(3) by auto
        moreover have "v∈set (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 ‹n∈acc v› have "∃q∈set (pl1@pl2@pl). n∈acc 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. ∃q∈set pl. i∈acc 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<sup>*</sup>``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 "u∈last p"
    assumes BACK: "v∈∪(set p)"
    assumes ACC: "∀i<num_acc. ∃q∈last p'. i∈acc 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 "v∈p!i" 
      by (simp_all add: i_def)

    have "u∈last p'" 
      using ‹u∈last 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 "v∈last p'" 
      using ‹v∈p!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 "u∈last p"
    assumes BACK: "v∈∪(set p)"
    assumes NACC: "j<num_acc" "∀q∈last p'. j∉acc 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 "v∈p!i" 
      by (simp_all add: i_def)

    have "u∈last p'" 
      using ‹u∈last 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 "v∈last p'" 
      using ‹v∈p!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. ∀q∈set pl. i∉acc q"
      proof cases
        assume "set pl ∩ last p' = {}" 
          ― ‹Case: The loop is outside the last Cnode›
        with path_restrict[OF P] ‹u∈last p'› ‹v∈last 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 "w∈last 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: "u∈last p"
    assumes VNE: "v∉∪(set p)" "v∉D"
    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. ∀q∈set pl. i∉acc q" 
      proof cases
        assume "v∈set 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: "v∉set 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 "w∈set 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: "u∈last p"
    assumes VID: "v∈D"
    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. ∀q∈set pl. i∉acc 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: "w∈D" 
          using VID by (auto dest!: path_is_rtrancl)
        from split(1) WID D_closed_vE_rtrancl have "u∈D"
          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: "v0∉D0" "v0∈it" 
    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: "v∈D'" "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: "v0∉D0" "v0∈it" 
    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)" "v∈D"
    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 (pr⌢pl^\<omega>)
    )"
    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;
      os←FOREACHci fgl_outer_invar V0 (go_is_no_brk) (λv0 s0. do {
        if v0∉goD 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 v∉D 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'
    ≤⇓(⟨Id⟩option_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. ∃q∈last p. i∈acc 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)))) ∧ i≤i'" 
    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,{})∈⟨R⟩Rs"
  assumes [autoref_rules]: "(un_impl,(∪))∈⟨R⟩Rs→⟨R⟩Rs→⟨R⟩Rs"
  shows "(?c,Un_set_drop_impl)∈nat_rel → ⟨⟨R⟩Rs⟩as_rel → ⟨⟨R⟩Rs⟩nres_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 {} (⟨R⟩Rs)"
  assumes "GEN_OP un_impl (∪) (⟨R⟩Rs→⟨R⟩Rs→⟨R⟩Rs)"
  shows "(λi A. RETURN (Un_set_drop_tr es_impl un_impl i A),Un_set_drop_impl)
    ∈nat_rel → ⟨⟨R⟩Rs⟩as_rel → ⟨⟨R⟩Rs⟩nres_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;
    s←pop_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 (simp add: refine_pw_simps pw_le_iff)
      unfolding gGS_rel_def GS_rel_def GS.α_def br_def gGS_α_def gGS_invar_def
      apply (clarsimp simp: L dest!: AUX1)
      apply (auto dest!: AUX1 simp: L)
      apply (force dest!: in_set_dropD) []
      apply (force dest!: in_set_takeD) []
      done
  qed

  definition gcollapse_impl :: "'Q ==> 'Q gGS ==> 'Q gGS nres" 
    where "gcollapse_impl v s ≡
    do {
      let (A,S,B,I,P)=s;
      i ← GS.idx_of_impl (S,B,I,P) v;
      ASSERT (i+1 ≤ length B);
      let B = take (i+1) B;
      ASSERT (i < length A);
      us←Un_set_drop_impl i A;
      let A = take i A @ [us];
      RETURN (A,S,B,I,P)
    }"

  lemma gcollapse_impl_aux_opt_refine: 
    "gcollapse_impl v s ≤ gcollapse_impl_aux v s"
    unfolding gcollapse_impl_def gcollapse_impl_aux_def collapse_impl_def 
      GS.collapse_impl_def
    apply (simp add: refine_pw_simps pw_le_iff split: prod.splits) 
    apply blast
    done
  
  lemma gcollapse_impl_refine:
    assumes A: "(s', a, p, D, pE) ∈ gGS_rel" 
    assumes B: "(v',v)∈Id"
    assumes PRE: "v∈∪(set p)"
    shows "gcollapse_impl v' s'
    ≤ ⇓ gGS_rel (RETURN (gcollapse v (a, p, D, pE)))"
    using order_trans[OF 
      gcollapse_impl_aux_opt_refine 
      gcollapse_impl_aux_refine[OF assms]]
    .

  definition ginitial_impl :: "'Q ==> 'Q goGS ==> 'Q gGS" 
    where "ginitial_impl v0 s0 ≡ ([acc v0],initial_impl v0 (snd s0))"
  lemma ginitial_impl_refine: 
    assumes A: "v0∉goD s0" "go_is_no_brk s0"
    assumes REL: "(s0i,s0)∈goGS_rel" "(v0i,v0)∈Id" 
    shows "(ginitial_impl v0i s0i,ginitial v0 s0)∈gGS_rel"
    unfolding ginitial_impl_def ginitial_def 
    using REL initial_refine[OF A(1) _ REL(2), of "snd s0i"] A(2)
    apply (auto 
      simp: gGS_rel_def br_def gGS_α_def gGS_invar_def goGS_rel_def goGS_α_def
      simp: go_is_no_brk_def goD_def oGS_rel_def GS_rel_def goGS_invar_def
      split: prod.splits

    )
    using acc_bound
    apply (fastforce simp: initial_impl_def GS_initial_impl_def)+
    done

  definition gpath_is_empty_impl :: "'Q gGS ==> bool"
    where "gpath_is_empty_impl s = path_is_empty_impl (snd s)"

  lemma gpath_is_empty_refine: 
    "(s,(a,p,D,pE))∈gGS_rel ==> gpath_is_empty_impl s ⟷ p=[]"
    unfolding gpath_is_empty_impl_def 
    using path_is_empty_refine
    by (fastforce simp: gGS_rel_def br_def gGS_invar_def gGS_α_def GS.α_def)

  definition gis_on_stack_impl :: "'Q ==> 'Q gGS ==> bool" 
    where "gis_on_stack_impl v s = is_on_stack_impl v (snd s)"

  lemma gis_on_stack_refine: 
    "[(s,(a,p,D,pE))∈gGS_rel] ==> gis_on_stack_impl v s ⟷ v∈∪(set p)"
    unfolding gis_on_stack_impl_def 
    using is_on_stack_refine
    by (fastforce simp: gGS_rel_def br_def gGS_invar_def gGS_α_def GS.α_def)

  definition gis_done_impl :: "'Q ==> 'Q gGS ==> bool"
    where "gis_done_impl v s ≡ is_done_impl v (snd s)"
  thm is_done_refine
  lemma gis_done_refine: "(s,(a,p,D,pE))∈gGS_rel
    ==> gis_done_impl v s ⟷ (v ∈ D)"
    using is_done_refine[of "(snd s)" v]
    by (auto 
      simp: gGS_rel_def br_def gGS_α_def gGS_invar_def GS.α_def 
            gis_done_impl_def)


  definition (in -) "on_stack_less I u v ≡
    case I v of
      Some (STACK j) ==> j<u
    | _ ==> False"

  definition (in -) "on_stack_ge I l v ≡
    case I v of
      Some (STACK j) ==> l≤j
    | _ ==> False"


  lemma (in GS_invar) set_butlast_p_refine:
    assumes PRE: "p_α≠[]"
    shows "Collect (on_stack_less I (last B)) = ∪(set (butlast p_α))" (is "?L=?R")
  proof (intro equalityI subsetI)
    from PRE have [simp]: "B≠[]" by (auto simp: p_α_def)

    have [simp]: "S≠[]"
      by (simp add: empty_eq)

    {
      fix v
      assume "v∈?L"
      then obtain j where [simp]: "I v = Some (STACK j)" and "j<last B"
        by (auto simp: on_stack_less_def split: option.splits node_state.splits)

      from I_consistent[of v j] have [simp]: "j<length S" "v=S!j" by auto
      
      from B0 have "B!0=0" by simp
      from ‹j<last B› have "j<B!(length B - 1)" by (simp add: last_conv_nth)
      from find_seg_bounds[OF ‹j<length S›] find_seg_correct[OF ‹j<length S›]
      have "v∈seg (find_seg j)" "find_seg j < length B" by auto
      moreover with ‹j<B!(length B - 1)› have "find_seg j < length B - 1"
        (* What follows is an unreadable, auto-generated structured proof
          that replaces the following smt-call:
        by (smt GS.seg_start_def `seg_start (find_seg j) \<le> j`)*)
      proof -
        have f1: "∧x₁ x. ¬ (x₁::nat) < x₁ - x"
          using less_imp_diff_less by blast
        have "j ≤ last B"
          by (metis ‹j < last B› less_le)
        hence f2: "∧x₁. ¬ last B < x₁ ∨ ¬ x₁ ≤ j"
          using f1 by (metis diff_diff_cancel le_trans)
        have "∧x₁. seg_end x₁ ≤ j ∨ ¬ x₁ < find_seg j"
          by (metis ‹seg_start (find_seg j) ≤ j› calculation(2) 
            le_trans seg_end_less_start)
        thus "find_seg j < length B - 1"
          using f1 f2 
          by (metis GS.seg_start_def ‹B ≠ []› ‹j < B ! (length B - 1)›
            ‹seg_start (find_seg j) ≤ j› calculation(2) diff_diff_cancel 
            last_conv_nth nat_neq_iff seg_start_less_end)
      qed
      ultimately show "v∈?R" 
        by (auto simp: p_α_def map_butlast[symmetric] butlast_upt)
    }

    {
      fix v
      assume "v∈?R"
      then obtain i where "i<length B - 1" and "v∈seg i"
        by (auto simp: p_α_def map_butlast[symmetric] butlast_upt)
      then obtain j where "j < seg_end i" and "v=S!j"
        by (auto simp: seg_def)
      hence "j<B!(i+1)" and "i+1 ≤ length B - 1" using ‹i<length B - 1›
        by (auto simp: seg_end_def last_conv_nth split: if_split_asm)
      with sorted_nth_mono[OF B_sorted ‹i+1 ≤ length B - 1›] have "j<last B"
        by (auto simp: last_conv_nth)
      moreover from ‹j < seg_end i› have "j<length S"
        by (metis GS.seg_end_def add_diff_inverse_nat ‹i + 1 ≤ length B - 1›
          add_lessD1 less_imp_diff_less less_le_not_le nat_neq_iff 
          seg_end_bound)
        (*by (smt `i < length B - 1` seg_end_bound)*)
      with I_consistent ‹v=S!j› have "I v = Some (STACK j)" by auto
      ultimately show "v∈?L"
        by (auto simp: on_stack_less_def)
    }
  qed

  lemma (in GS_invar) set_last_p_refine:
    assumes PRE: "p_α≠[]"
    shows "Collect (on_stack_ge I (last B)) = last p_α" (is "?L=?R")
  proof (intro equalityI subsetI)
    from PRE have [simp]: "B≠[]" by (auto simp: p_α_def)

    have [simp]: "S≠[]" by (simp add: empty_eq)

    {
      fix v
      assume "v∈?L"
      then obtain j where [simp]: "I v = Some (STACK j)" and "j≥last B"
        by (auto simp: on_stack_ge_def split: option.splits node_state.splits)

      from I_consistent[of v j] have [simp]: "j<length S" "v=S!j" by auto
      hence "v∈seg (length B - 1)" using ‹j≥last B›
        by (auto simp: seg_def last_conv_nth seg_start_def seg_end_def)
      thus "v∈last p_α" by (auto simp: p_α_def last_map)
    }

    {
      fix v
      assume "v∈?R"
      hence "v∈seg (length B - 1)"
        by (auto simp: p_α_def last_map)
      then obtain j where "v=S!j" "j≥last B" "j<length S"
        by (auto simp: seg_def last_conv_nth seg_start_def seg_end_def)
      with I_consistent have "I v = Some (STACK j)" by simp
      with ‹j≥last B› show "v∈?L" by (auto simp: on_stack_ge_def)
    }
  qed

  definition ce_impl :: "'Q gGS ==> (('Q set × 'Q set) option × 'Q gGS) nres"
    where "ce_impl s ≡
    do {
      let (a,S,B,I,P) = s;
      ASSERT (B≠[]);
      let bls = Collect (on_stack_less I (last B));
      let ls = Collect (on_stack_ge I (last B));
      RETURN (Some (bls, ls),a,S,B,I,P)
    }"

  lemma ce_impl_refine:
    assumes A: "(s,(a,p,D,pE))∈gGS_rel"
    assumes PRE: "p≠[]"
    shows "ce_impl s ≤ ⇓(Id×_{rgGS_rel})
      (RETURN (Some (∪(set (butlast p)),last p),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'"
      by (rule gGS_relE)

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

    from PRE have NE': "GS.p_α (S', B', I', P') ≠ []" by simp
    hence BNE[simp]: "B'≠[]" by (simp add: GS.p_α_def)

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

    show ?thesis
      using GS_invar.set_butlast_p_refine[OF GS_invar NE']
      using GS_invar.set_last_p_refine[OF GS_invar NE']
      unfolding ce_impl_def
      using A
      by auto
  qed

  definition "last_is_acc_impl s ≡
    do {
      let (a,_)=s;
      ASSERT (a≠[]);
      RETURN (∀i<num_acc. i∈last a)
    }"

  lemma last_is_acc_impl_refine:
    assumes A: "(s,(a,p,D,pE))∈gGS_rel"
    assumes PRE: "a≠[]"
    shows "last_is_acc_impl s ≤ RETURN (last a = {0..<num_acc})"
  proof -
    from A PRE have "last a ⊆ {0..<num_acc}"
      unfolding gGS_rel_def gGS_invar_def br_def gGS_α_def by auto
    hence C: "(∀i<num_acc. i∈last a) ⟷ (last a = {0..<num_acc})"
      by auto

    from A obtain gs where [simp]: "s=(a,gs)"
      by (auto simp: gGS_rel_def gGS_α_def br_def split: prod.splits)

    show ?thesis
      unfolding last_is_acc_impl_def 
      by (auto simp: gGS_rel_def br_def gGS_α_def C PRE split: prod.splits)
  qed

  definition go_is_no_brk_impl :: "'Q goGS ==> bool" 
    where "go_is_no_brk_impl s ≡ fst s = None"
  lemma go_is_no_brk_refine: 
    "(s,s')∈goGS_rel ==> go_is_no_brk_impl s ⟷ go_is_no_brk s'"
    unfolding go_is_no_brk_def go_is_no_brk_impl_def
    by (auto simp: goGS_rel_def br_def goGS_α_def split: prod.splits)

  definition goD_impl :: "'Q goGS ==> 'Q oGS" where "goD_impl s ≡ snd s"
  lemma goD_refine: 
    "go_is_no_brk s' ==> (s,s')∈goGS_rel ==> (goD_impl s, goD s')∈oGS_rel"
    unfolding goD_impl_def goD_def
    by (auto 
      simp: goGS_rel_def br_def goGS_α_def goGS_invar_def oGS_rel_def 
            go_is_no_brk_def) 

  definition go_is_done_impl :: "'Q ==> 'Q goGS ==> bool" 
    where "go_is_done_impl v s ≡ is_done_oimpl v (snd s)"
  thm is_done_orefine
  lemma go_is_done_impl_refine: "[go_is_no_brk s'; (s,s')∈goGS_rel; (v,v')∈Id]
    ==> go_is_done_impl v s ⟷ (v'∈goD s')"
    using is_done_orefine
    unfolding go_is_done_impl_def goD_def go_is_no_brk_def
    apply (fastforce simp: goGS_rel_def br_def goGS_invar_def goGS_α_def)
    done


  definition goBrk_impl :: "'Q goGS ==> 'Q ce" where "goBrk_impl ≡ fst"

  lemma goBrk_refine: "(s,s')∈goGS_rel ==> (goBrk_impl s, goBrk s')∈Id"
    unfolding goBrk_impl_def goBrk_def
    by (auto simp: goGS_rel_def br_def goGS_α_def split: prod.splits)

  definition find_ce_impl :: "('Q set × 'Q set) option nres" where
    "find_ce_impl ≡ do {
      stat_start_nres;
      let os=goinitial_impl;
      os←FOREACHci (λit os. fgl_outer_invar it (goGS_α os)) V0
        (go_is_no_brk_impl) (λv0 s0.
      do {
        if ¬go_is_done_impl v0 s0 then do {

          let s = (None,ginitial_impl v0 s0);

          (brk,s)←WHILEIT
            (λ(brk,s). fgl_invar v0 (oGS_α (goD_impl s0)) (brk,snd (gGS_α s)))
            (λ(brk,s). brk=None ∧ ¬gpath_is_empty_impl s) (λ(l,s).
          do {
            ― ‹Select edge from end of path›
            (vo,s) ← gselect_edge_impl s;

            case vo of
              Some v ==> do {
                if gis_on_stack_impl v s then do {
                  s←gcollapse_impl v s;
                  b←last_is_acc_impl s;
                  if b then
                    ce_impl s
                  else
                    RETURN (None,s)
                } else if ¬gis_done_impl v s then do {
                  ― ‹Edge to new node. Append to path›
                  RETURN (None,gpush_impl v s)
                } else do {
                  ― ‹Edge to done node. Skip›
                  RETURN (None,s)
                }
              }
            | None ==> do {
                ― ‹No more outgoing edges from current node on path›
                s←gpop_impl s;
                RETURN (None,s)
              }
          }) (s);
          RETURN (gto_outer_impl brk s)
        } else RETURN s0
      }) os;
      stat_stop_nres;
      RETURN (goBrk_impl os)
    }"

  lemma find_ce_impl_refine: "find_ce_impl ≤ ⇓Id gfind_ce"
  proof -
    note [refine2] = prod_relI[OF IdI[of None] ginitial_impl_refine]

    have [refine]: "∧s a p D pE. [
      (s,(a,p,D,pE))∈gGS_rel;
      p ≠ []; pE ∩ last p × UNIV = {}
      ] ==>
      gpop_impl s 🍋 (λs. RETURN (None, s))
        ≤ SPEC (λc. (c, None, gpop (a,p,D,pE)) ∈ Id ×_r gGS_rel)"
      apply (drule (2) gpop_impl_refine)
      apply (fastforce simp add: pw_le_iff refine_pw_simps)
      done

    note [[goals_limit = 1]]

    note FOREACHci_refine_rcg'[refine del]

    show ?thesis
      unfolding find_ce_impl_def gfind_ce_def
      apply (refine_rcg
        bind_refine'
        prod_relI IdI
        inj_on_id

        gselect_edge_impl_refine gpush_impl_refine 
        oinitial_refine ginitial_impl_refine 
        bind_Let_refine2[OF gcollapse_impl_refine]
        if_bind_cond_refine[OF last_is_acc_impl_refine]
        ce_impl_refine
        goinitial_impl_refine
        gto_outer_refine
        goBrk_refine
        FOREACHci_refine_rcg'[where R=goGS_rel, OF inj_on_id]
      )

      apply refine_dref_type
    
      apply (simp_all add: go_is_no_brk_refine go_is_done_impl_refine)
      apply (auto simp: goGS_rel_def br_def) []
      apply (auto simp: goGS_rel_def br_def goGS_α_def gGS_α_def gGS_rel_def 
                        goD_def goD_impl_def) []

      apply (auto dest: gpath_is_empty_refine ) []
      apply (auto dest: gis_on_stack_refine) []
      apply (auto dest: gis_done_refine) []
      done
  qed

end

section ‹Constructing a Lasso from Counterexample›

subsection ‹Lassos in GBAs›

context igb_fr_graph begin

  definition reconstruct_reach :: "'Q set ==> 'Q set ==> ('Q list × 'Q) nres"
    ― ‹Reconstruct the reaching path of a lasso›
    where "reconstruct_reach Vr Vl ≡ do {
      res ← find_path (E∩Vr×UNIV) V0 (λv. v∈Vl);
      ASSERT (res ≠ None);
      RETURN (the res)
    }"

  lemma reconstruct_reach_correct:
    assumes CEC: "ce_correct Vr Vl"
    shows "reconstruct_reach Vr Vl
      ≤ SPEC (λ(pr,va). ∃v0∈V0. path E v0 pr va ∧ va∈Vl)"
  proof -
    have FIN_aux: "finite ((E ∩ Vr × UNIV)^* `` V0)"
      by (metis finite_reachableE_V0 finite_subset inf_sup_ord(1) inf_sup_ord(2)
        inf_top.left_neutral reachable_mono)
    
    {
      fix u p v
      assume P: "path E u p v" and SS: "set p ⊆ Vr"
      have "path (E ∩ Vr×UNIV) u p v"
        apply (rule path_mono[OF _ path_restrict[OF P]])
        using SS by auto
    } note P_CONV=this

    from CEC obtain v0 "pr" va where "v0∈V0" "set pr ⊆ Vr" "va∈Vl" 
      "path (E ∩ Vr×UNIV) v0 pr va"
      unfolding ce_correct_def is_lasso_prpl_def is_lasso_prpl_pre_def
      by (force simp: neq_Nil_conv path_simps dest: P_CONV)
    hence 1: "va ∈ (E ∩ Vr × UNIV)^* `` V0" 
      by (auto dest: path_is_rtrancl)
      
    show ?thesis
      using assms unfolding reconstruct_reach_def
      apply (refine_rcg refine_vcg order_trans[OF find_path_ex_rule])
      apply (clarsimp_all simp: FIN_aux finite_V0)

      using ‹va∈Vl› 1 apply auto []

      apply (auto dest: path_mono[of "E ∩ Vr × UNIV" E, simplified]) []
      done
  qed

  definition "rec_loop_invar Vl va s ≡ let (v,p,cS) = s in
    va ∈ E^*``V0 ∧
    path E va p v ∧
    cS = acc v ∪ (∪(acc`set p)) ∧
    va ∈ Vl ∧ v ∈ Vl ∧ set p ⊆ Vl"

  definition reconstruct_lasso :: "'Q set ==> 'Q set ==> ('Q list × 'Q list) nres"
    ― ‹Reconstruct lasso›
    where "reconstruct_lasso Vr Vl ≡ do {
    (pr,va) ← reconstruct_reach Vr Vl;
    
    let cS_full = {0..<num_acc};
    let E = E ∩ UNIV×Vl;
    
    (vd,p,_) ← WHILEIT (rec_loop_invar Vl va)
      (λ(_,_,cS). cS ≠ cS_full)
      (λ(v,p,cS). do {
        ASSERT (∃v'. (v,v')∈E^* ∧ ¬ (acc v' ⊆ cS));
        sr ← find_path E {v} (λv. ¬ (acc v ⊆ cS));
        ASSERT (sr ≠ None);
        let (p_seg,v) = the sr;
        RETURN (v,p@p_seg,cS ∪ acc v)
      }) (va,[],acc va);

    p_close_r ← (if p=[] then
        find_path1 E vd ((=) va)
      else
        find_path E {vd} ((=) va));

    ASSERT (p_close_r ≠ None);
    let (p_close,_) = the p_close_r;

    RETURN (pr, p@p_close)
  }"


lemma (in igb_fr_graph) reconstruct_lasso_correct:
  assumes CEC: "ce_correct Vr Vl"
  shows "reconstruct_lasso Vr Vl ≤ SPEC (is_lasso_prpl)"
proof -

  let ?E = "E ∩ UNIV × Vl"

  have E_SS: "E ∩ Vl × Vl ⊆ ?E" by auto

  from CEC have
    REACH: "Vl ⊆ E^*``V0"
    and CONN: "Vl×Vl ⊆ (E ∩ Vl×Vl)^*"
    and NONTRIV: "Vl×Vl ∩ E ≠ {}"
    and NES[simp]: "Vl≠{}"
    and ALL: "∪(acc`Vl) = {0..<num_acc}"
    unfolding ce_correct_def is_lasso_prpl_def
    apply clarsimp_all
    apply auto []
    apply force
    done

  define term_rel
    where "term_rel = (inv_image (finite_psupset {0..<num_acc}) (λ(_::'Q,_::'Q list,cS). cS))"
  hence WF: "wf term_rel" by simp

  { fix va
    assume "va ∈ Vl"
    hence "rec_loop_invar Vl va (va, [], acc va)"
      unfolding rec_loop_invar_def using REACH by auto
  } note INVAR_INITIAL = this

  {
    fix v p cS va
    assume "rec_loop_invar Vl va (v, p, cS)"
    hence "finite ((?E)^* `` {v})"
      apply -
      apply (rule finite_subset[where B="E<sup>*</sup>``V0"])
      unfolding rec_loop_invar_def
      using REACH
      apply (clarsimp_all dest!: path_is_rtrancl)
      apply (drule rtrancl_mono_mp[where U="?E" and V=E, rotated], (auto) [])
      by (metis rev_ImageI rtrancl_trans)
  } note FIN1 = this

  {
    fix va v :: 'Q and p cS
    assume INV: "rec_loop_invar Vl va (v,p,cS)"
      and NC: "cS ≠ {0..<num_acc}"

    from NC INV obtain i where "i<num_acc" "i∉cS" 
      unfolding rec_loop_invar_def by auto blast

    with ALL obtain v' where v': "v'∈Vl" "¬ acc v' ⊆ cS"
      by (metis NES atLeastLessThan_iff cSUP_least in_mono zero_le)
     
    with CONN INV have "(v,v')∈(E ∩ Vl × Vl)^*"
      unfolding rec_loop_invar_def by auto
    hence "(v,v')∈?E^*" using rtrancl_mono_mp[OF E_SS] by blast
    with v' have "∃v'. (v,v')∈(?E)^* ∧ ¬ acc v' ⊆ cS" by auto
  } note ASSERT1 = this

  {
    fix va v p cS v' p'
    assume "rec_loop_invar Vl va (v, p, cS)"
    and "path (?E) v p' v'"
    and "¬ (acc v' ⊆ cS)"
    and "∀v∈set p'. acc v ⊆ cS"
    hence "rec_loop_invar Vl va (v', p@p', cS ∪ acc v')"
      unfolding rec_loop_invar_def
      apply simp
      apply (intro conjI)
      apply (auto simp: path_simps dest: path_mono[of "?E" E, simplified]) []

      apply (cases p')
      apply (auto simp: path_simps) [2]

      apply (cases p' rule: rev_cases)
      apply (auto simp: path_simps) [2]

      apply (erule path_set_induct)
      apply auto [2]
      done
  } note INV_PRES = this

  {
    fix va v p cS v' p'
    assume "rec_loop_invar Vl va (v, p, cS)"
      and "path ?E v p' v'"
      and "¬ (acc v' ⊆ cS)"
      and "∀v∈set p'. acc v ⊆ cS"
    hence "((v', p@p', cS ∪ acc v'), (v,p,cS)) ∈ term_rel"
      unfolding term_rel_def rec_loop_invar_def
      by (auto simp: finite_psupset_def)
  } note VAR = this

  have CONN1: "Vl × Vl ⊆ (?E)⁺"
  proof clarify
    fix a b
    assume "a∈Vl" "b∈Vl"
    from NONTRIV obtain u v where E: "(u,v)∈(E ∩ Vl×Vl)" by auto
    from CONN ‹a∈Vl› E have "(a,u)∈(E∩Vl×Vl)^*" by auto
    also note E
    also (rtrancl_into_trancl1) from CONN ‹b∈Vl› E have "(v,b)∈(E∩Vl×Vl)^*"
      by auto
    finally show "(a,b)∈(?E)⁺" using trancl_mono[OF _ E_SS] by auto
  qed
    
  {
    fix va v p cS
    assume "rec_loop_invar Vl va (v, p, cS)"
    hence "(v,va) ∈ (?E)⁺"
      unfolding rec_loop_invar_def
      using CONN1
      by auto
  } note CLOSE1 = this

  {
    fix va v p cS
    assume "rec_loop_invar Vl va (v, p, cS)"
    hence "(v,va) ∈ (?E)^*"
      unfolding rec_loop_invar_def
      using CONN rtrancl_mono[OF E_SS]
      by auto
  } note CLOSE2 = this

  {
    fix "pr" vd pl va v0
    assume "rec_loop_invar Vl va (vd, [], {0..<num_acc})" "va ∈ Vl" "v0 ∈ V0"
      "path E v0 pr va" "pl ≠ []" "path ?E vd pl va"
    hence "is_lasso_prpl (pr, pl)"
      unfolding is_lasso_prpl_def is_lasso_prpl_pre_def rec_loop_invar_def
      by (auto simp: neq_Nil_conv path_simps
        dest!: path_mono[of "?E" E, simplified]) []
  } note INV_POST1 = this

  {
    fix va v p p' "pr" v0
    assume INV: "rec_loop_invar Vl va (v,p,{0..<num_acc})" 
      and 1: "p≠[]" "path ?E v p' va"
      and PR: "v0∈V0" "path E v0 pr va"

    from INV have "∀i<num_acc. ∃q∈insert v (set p). i ∈ acc q"
      unfolding rec_loop_invar_def
      by auto
    moreover from INV 1 have "insert v (set p) ⊆ set p ∪ set p'"
      unfolding rec_loop_invar_def
      apply (cases p)
      apply blast
      apply (cases p')
      apply (auto simp: path_simps)
      done
    ultimately have ACC: "∀i<num_acc. ∃q∈set p ∪ set p'. i ∈ acc q" by blast
    
    from INV 1 have PL: "path E va (p @ p') va"
      by (auto simp: rec_loop_invar_def path_simps 
        dest!: path_mono[of "?E" E, simplified]) []

    have "is_lasso_prpl (pr,p@p')"
      unfolding is_lasso_prpl_def is_lasso_prpl_pre_def
      apply (clarsimp simp: ACC)
      using PR PL ‹p≠[]› by auto
  } note INV_POST2 = this

  show ?thesis
    unfolding reconstruct_lasso_def
    apply (refine_rcg 
      WF
      order_trans[OF reconstruct_reach_correct]
      order_trans[OF find_path_ex_rule]
      order_trans[OF find_path1_ex_rule]
      refine_vcg 
    )

    apply (vc_solve 
      del: subsetI
      solve: ASSERT1 INV_PRES asm_rl VAR CLOSE1 CLOSE2 INV_POST1 INV_POST2
      simp: INVAR_INITIAL FIN1 CEC)
    done
qed

definition find_lasso where "find_lasso ≡ do {
  ce ← find_ce_spec;
  case ce of
    None ==> RETURN None
  | Some (Vr,Vl) ==> do {
      l ← reconstruct_lasso Vr Vl;
      RETURN (Some l)
    }
}"

lemma (in igb_fr_graph) find_lasso_correct: "find_lasso ≤ find_lasso_spec"
  unfolding find_lasso_spec_def find_lasso_def find_ce_spec_def
  apply (refine_rcg refine_vcg order_trans[OF reconstruct_lasso_correct])
  apply auto
  done

end

end