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 (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);
      usUn_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: "v0goD 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)  lj
    | _  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 "vseg (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) ≤ j`)*)
      proof -
        have f1: "x1 x. ¬ (x1::nat) < x1 - x"
          using less_imp_diff_less by blast
        have "j  last B"
          by (metis j < last B less_le)
        hence f2: "x1. ¬ last B < x1  ¬ x1  j"
          using f1 by (metis diff_diff_cancel le_trans)
        have "x1. seg_end x1  j  ¬ x1 < 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 "vseg 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 "jlast 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 "vseg (length B - 1)" using jlast B
        by (auto simp: seg_def last_conv_nth seg_start_def seg_end_def)
      thus "vlast p_α" by (auto simp: p_α_def last_map)
    }

    {
      fix v
      assume "v?R"
      hence "vseg (length B - 1)"
        by (auto simp: p_α_def last_map)
      then obtain j where "v=S!j" "jlast 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 jlast 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. ilast 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. ilast 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;
      osFOREACHci (λ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 {
                  sgcollapse_impl v s;
                  blast_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›
                sgpop_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 (EVr×UNIV) V0 (λv. vVl);
      ASSERT (res  None);
      RETURN (the res)
    }"

  lemma reconstruct_reach_correct:
    assumes CEC: "ce_correct Vr Vl"
    shows "reconstruct_reach Vr Vl 
       SPEC (λ(pr,va). v0V0. path E v0 pr va  vaVl)"
  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 "v0V0" "set pr  Vr" "vaVl" 
      "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 vaVl 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*``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" "icS" 
      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 "vset 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 "vset 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 "aVl" "bVl"
    from NONTRIV obtain u v where E: "(u,v)(E  Vl×Vl)" by auto
    from CONN aVl E have "(a,u)(EVl×Vl)*" by auto
    also note E
    also (rtrancl_into_trancl1) from CONN bVl E have "(v,b)(EVl×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: "v0V0" "path E v0 pr va"

    from INV have "i<num_acc. qinsert 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. qset 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