diff --git a/thys/Gabow_SCC/Gabow_GBG.thy b/thys/Gabow_SCC/Gabow_GBG.thy
--- a/thys/Gabow_SCC/Gabow_GBG.thy
+++ b/thys/Gabow_SCC/Gabow_GBG.thy
@@ -1,2102 +1,2102 @@
 section \<open>Lasso Finding Algorithm for Generalized B\"uchi Graphs \label{sec:gbg}\<close>
 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)\<^sup>* `` 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 \<open>
   We implement an algorithm that computes witnesses for the 
   non-emptiness of Generalized B\"uchi Graphs (GBG).
 \<close>
 
 section \<open>Specification\<close>
 context igb_graph
 begin
   definition ce_correct 
     \<comment> \<open>Specifies a correct counter-example\<close>
     where
     "ce_correct Vr Vl \<equiv> (\<exists>pr pl. 
         Vr \<subseteq> E\<^sup>*``V0 \<and> Vl \<subseteq> E\<^sup>*``V0 \<comment> \<open>Only reachable nodes are covered\<close>
       \<and> set pr\<subseteq>Vr \<and> set pl\<subseteq>Vl     \<comment> \<open>The paths are inside the specified sets\<close>
       \<and> Vl\<times>Vl \<subseteq> (E \<inter> Vl\<times>Vl)\<^sup>*      \<comment> \<open>\<open>Vl\<close> is mutually connected\<close>
       \<and> Vl\<times>Vl \<inter> E \<noteq> {}            \<comment> \<open>\<open>Vl\<close> is non-trivial\<close>
       \<and> is_lasso_prpl (pr,pl))    \<comment> \<open>Paths form a lasso\<close>
     "     
 
   definition find_ce_spec :: "('Q set \<times> 'Q set) option nres" where
     "find_ce_spec \<equiv> SPEC (\<lambda>r. case r of
       None \<Rightarrow> (\<forall>prpl. \<not>is_lasso_prpl prpl)
     | Some (Vr,Vl) \<Rightarrow> ce_correct Vr Vl
     )"
 
   definition find_lasso_spec :: "('Q list \<times> 'Q list) option nres" where
     "find_lasso_spec \<equiv> SPEC (\<lambda>r. case r of
       None \<Rightarrow> (\<forall>prpl. \<not>is_lasso_prpl prpl)
     | Some prpl \<Rightarrow> is_lasso_prpl prpl
     )"
 
 end
 
 section \<open>Invariant Extension\<close>
 
 text \<open>Extension of the outer invariant:\<close>
 context igb_fr_graph
 begin
   definition no_acc_over
     \<comment> \<open>Specifies that there is no accepting cycle touching a set of nodes\<close>
     where
     "no_acc_over D \<equiv> \<not>(\<exists>v\<in>D. \<exists>pl. pl\<noteq>[] \<and> path E v pl v \<and> 
     (\<forall>i<num_acc. \<exists>q\<in>set pl. i\<in>acc q))"
 
   definition "fgl_outer_invar_ext \<equiv> \<lambda>it (brk,D). 
     case brk of None \<Rightarrow> no_acc_over D | Some (Vr,Vl) \<Rightarrow> ce_correct Vr Vl"
 
   definition "fgl_outer_invar \<equiv> \<lambda>it (brk,D). case brk of 
     None \<Rightarrow> outer_invar it D \<and> no_acc_over D
   | Some (Vr,Vl) \<Rightarrow> ce_correct Vr Vl"
   
 end
 
 text \<open>Extension of the inner invariant:\<close>
 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 \<times> 'Q set) option" and p D pE +
   assumes no_acc: "brk=None \<Longrightarrow> \<not>(\<exists>v pl. pl\<noteq>[] \<and> path lvE v pl v \<and> 
     (\<forall>i<num_acc. \<exists>q\<in>set pl. i\<in>acc q))" \<comment> \<open>No accepting cycle over 
       visited edges\<close>
   assumes acc: "brk=Some (Vr,Vl) \<Longrightarrow> 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 \<equiv> 
   \<lambda>(brk, p, D, pE). fgl_invar_loc G v0 D0 brk p D pE"
 
 section \<open>Definition of the Lasso-Finding Algorithm\<close>
 
 context igb_fr_graph
 begin
   definition find_ce :: "('Q set \<times> 'Q set) option nres" where
     "find_ce \<equiv> do {
       let D = {};
       (brk,_)\<leftarrow>FOREACHci fgl_outer_invar V0 
         (\<lambda>(brk,_). brk=None) 
         (\<lambda>v0 (brk,D0). do {
           if v0\<notin>D0 then do {
             let s = (None,initial v0 D0);
 
             (brk,p,D,pE) \<leftarrow> WHILEIT (fgl_invar v0 D0)
               (\<lambda>(brk,p,D,pE). brk=None \<and> p \<noteq> []) (\<lambda>(_,p,D,pE). 
             do {
               \<comment> \<open>Select edge from end of path\<close>
               (vo,(p,D,pE)) \<leftarrow> select_edge (p,D,pE);
 
               ASSERT (p\<noteq>[]);
               case vo of 
                 Some v \<Rightarrow> do {
                   if v \<in> \<Union>(set p) then do {
                     \<comment> \<open>Collapse\<close>
                     let (p,D,pE) = collapse v (p,D,pE);
 
                     ASSERT (p\<noteq>[]);
 
                     if \<forall>i<num_acc. \<exists>q\<in>last p. i\<in>acc q then
                       RETURN (Some (\<Union>(set (butlast p)),last p),p,D,pE)
                     else
                       RETURN (None,p,D,pE)
                   } else if v\<notin>D then do {
                     \<comment> \<open>Edge to new node. Append to path\<close>
                     RETURN (None,push v (p,D,pE))
                   } else RETURN (None,p,D,pE)
                 }
               | None \<Rightarrow> do {
                   \<comment> \<open>No more outgoing edges from current node on path\<close>
                   ASSERT (pE \<inter> last p \<times> UNIV = {});
                   RETURN (None,pop (p,D,pE))
                 }
             }) s;
             ASSERT (brk=None \<longrightarrow> (p=[] \<and> pE={}));
             RETURN (brk,D)
           } else 
             RETURN (brk,D0)
       }) (None,D);
       RETURN brk
     }"
 end
 
 section \<open>Invariant Preservation\<close>
 
 
 context igb_fr_graph
 begin
 
   definition "fgl_invar_part \<equiv> \<lambda>(brk, p, D, pE). 
     fgl_invar_loc_axioms G brk p D pE"
 
   lemma fgl_outer_invarI[intro?]:
     "\<lbrakk>
       brk=None \<Longrightarrow> outer_invar it D; 
       \<lbrakk>brk=None \<Longrightarrow> outer_invar it D\<rbrakk> \<Longrightarrow> fgl_outer_invar_ext it (brk,D)\<rbrakk> 
       \<Longrightarrow> 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?]:
     "\<lbrakk> invar v0 D0 PDPE; 
        invar v0 D0 PDPE \<Longrightarrow> fgl_invar_part (B,PDPE)\<rbrakk> 
      \<Longrightarrow> 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\<in>it" "v0\<notin>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 \<noteq> []" and P: "path (vE [{v0}] D0 (E \<inter> {v0} \<times> UNIV)) v pl v"
       hence 1: "v\<in>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 \<open>v0\<notin>D0\<close>
       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\<noteq>[]"
     assumes NO': "pE \<inter> last p \<times> 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\<noteq>[]"
     assumes NONTRIV: "vE p D pE \<inter> (last p \<times> last p) \<noteq> {}"
     assumes ACC: "\<forall>i<num_acc. \<exists>q\<in>last p. i\<in>acc q"
     shows "fgl_invar_part (Some (\<Union>(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 \<open>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.\<close>
 
     let ?Er = "E \<inter> (\<Union>(set (butlast p)) \<times> UNIV)"
 
     txt \<open>We choose a node in the last Cnode, that is reachable only using
       former Cnodes.\<close>
 
     obtain w where "(v0,w)\<in>?Er\<^sup>*" "w\<in>last p"
     proof cases
       assume "length p = 1"
       hence "v0\<in>last p"
         using root_v0 
         by (cases p) auto
       thus thesis by (auto intro: that)
     next
       assume "length p\<noteq>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\<in>p!(length p - 2)" and VIP: "v\<in>p!(length p - 1)" and "(u,v)\<in>lvE"
         using \<open>length p > 1\<close> by auto
       from root_v0 have V0IP: "v0\<in>p!0" by (cases p) auto
       
       from VIP have "v\<in>last p" by (cases p rule: rev_cases) auto
 
       from pathI[OF V0IP UIP] \<open>length p > 1\<close> have 
         "(v0,u)\<in>(lvE \<inter> \<Union>(set (butlast p)) \<times> \<Union>(set (butlast p)))\<^sup>*"
         (is "_ \<in> \<dots>\<^sup>*")  
         by (simp add: path_seg_butlast)
       also have "\<dots> \<subseteq> ?Er" using lvE_ss_E by auto
       finally (rtrancl_mono_mp[rotated]) have "(v0,u)\<in>?Er\<^sup>*" .
       also note \<open>(u,v)\<in>lvE\<close> UIP hence "(u,v)\<in>?Er" using lvE_ss_E \<open>length p > 1\<close> 
         apply (auto simp: Bex_def in_set_conv_nth)
         by (metis One_nat_def Suc_lessE \<open>Suc (length p - 2) < length p\<close> 
           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 \<subseteq> \<Union>(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 \<open>From that node, we construct a lasso by inductively appending a path
       for each accepting set\<close>
     {
       fix na
       assume na_def: "na = num_acc"
 
       have "\<exists>pl. pl\<noteq>[] 
         \<and> path (lvE \<inter> last p\<times>last p) w pl w 
         \<and> (\<forall>i<num_acc. \<exists>q\<in>set pl. i\<in>acc q)"
         using ACC
         unfolding na_def[symmetric]
       proof (induction na)
         case 0 
 
         from NONTRIV obtain u v 
           where "(u,v)\<in>lvE \<inter> last p \<times> last p" "u\<in>last p" "v\<in>last p"
           by auto
         from cnode_connectedI \<open>w\<in>last p\<close> \<open>u\<in>last p\<close> 
         have "(w,u)\<in>(lvE \<inter> last p \<times> last p)\<^sup>*"
           by auto
         also note \<open>(u,v)\<in>lvE \<inter> last p \<times> last p\<close>
         also (rtrancl_into_trancl1) from cnode_connectedI \<open>v\<in>last p\<close> \<open>w\<in>last p\<close> 
         have "(v,w)\<in>(lvE \<inter> last p \<times> last p)\<^sup>*"
           by auto
         finally obtain pl where "pl\<noteq>[]" "path (lvE \<inter> last p \<times> last p) w pl w"
           by (rule trancl_is_path)
         thus ?case by auto
       next
         case (Suc n)
         from Suc.prems have "\<forall>i<n. \<exists>q\<in>last p. i\<in>acc q" by auto
         with Suc.IH obtain pl where IH: 
           "pl\<noteq>[]" 
           "path (lvE \<inter> last p \<times> last p) w pl w" 
           "\<forall>i<n. \<exists>q\<in>set pl. i\<in>acc q" 
           by blast
   
         from Suc.prems obtain v where "v\<in>last p" and "n\<in>acc v" by auto
         from cnode_connectedI \<open>w\<in>last p\<close> \<open>v\<in>last p\<close> 
         have "(w,v)\<in>(lvE \<inter> last p \<times> last p)\<^sup>*" by auto
         then obtain pl1 where P1: "path (lvE \<inter> last p \<times> last p) w pl1 v" 
           by (rule rtrancl_is_path)
         also from cnode_connectedI \<open>w\<in>last p\<close> \<open>v\<in>last p\<close> 
         have "(v,w)\<in>(lvE \<inter> last p \<times> last p)\<^sup>*" by auto
         then obtain pl2 where P2: "path (lvE \<inter> last p \<times> last p) v pl2 w"
           by (rule rtrancl_is_path)
         also (path_conc) note IH(2)
         finally (path_conc) have 
           P: "path (lvE \<inter> last p \<times> last p) w (pl1@pl2@pl) w"
           by simp
         moreover from IH(1) have "pl1@pl2@pl \<noteq> []" by simp
         moreover have "\<forall>i'<n. \<exists>q\<in>set (pl1@pl2@pl). i'\<in>acc q" using IH(3) by auto
         moreover have "v\<in>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 \<open>n\<in>acc v\<close> have "\<exists>q\<in>set (pl1@pl2@pl). n\<in>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\<noteq>[]" "path (lvE \<inter> last p\<times>last p) w pl w" 
       "\<forall>i<num_acc. \<exists>q\<in>set pl. i\<in>acc q" by blast
     hence "path E w pl w" and L_SS: "set pl \<subseteq> 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 \<open>path E w pl w\<close> P_REACH pl by auto
     
     from p_sc have "last p \<times> last p \<subseteq> (lvE \<inter> last p \<times> last p)\<^sup>*" by auto
     with lvE_ss_E have VL_CLOSED: "last p \<times> last p \<subseteq> (E \<inter> last p \<times> last p)\<^sup>*"
       apply (erule_tac order_trans)
       apply (rule rtrancl_mono)
       by blast
 
     have NONTRIV': "last p \<times> last p \<inter> E \<noteq> {}"
       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 \<subseteq> E\<^sup>*``V0" 
       and BLP_REACH: "\<Union>(set (butlast p)) \<subseteq> E\<^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' \<equiv> 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\<noteq>[]"
     assumes E: "(u,v)\<in>pE" and "u\<in>last p"
     assumes BACK: "v\<in>\<Union>(set p)"
     assumes ACC: "\<forall>i<num_acc. \<exists>q\<in>last p'. i\<in>acc q"
     defines i_def: "i \<equiv> idx_of p v"
     shows "fgl_invar_part (
       Some (\<Union>(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\<in>p!i" 
       by (simp_all add: i_def)
 
     have "u\<in>last p'" 
       using \<open>u\<in>last p\<close> \<open>i<length p\<close> 
       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\<in>last p'" 
       using \<open>v\<in>p!i\<close> \<open>i<length p\<close> 
       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' \<inter> last p' \<times> last p' \<noteq> {}" 
       unfolding p'_def pE'_def by (auto simp: E)
     
     have "p'\<noteq>[]" 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' \<equiv> 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\<noteq>[]"
     assumes E: "(u,v)\<in>pE" and "u\<in>last p"
     assumes BACK: "v\<in>\<Union>(set p)"
     assumes NACC: "j<num_acc" "\<forall>q\<in>last p'. j\<notin>acc q"
     defines "i \<equiv> 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\<in>p!i" 
       by (simp_all add: i_def)
 
     have "u\<in>last p'" 
       using \<open>u\<in>last p\<close> \<open>i<length p\<close>
       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\<in>last p'" 
       using \<open>v\<in>p!i\<close> \<open>i<length p\<close> 
       unfolding p'_def collapse_aux_def
       by (metis UnionI append_Nil Cons_nth_drop_Suc in_set_conv_decomp last_snoc)
     ultimately have "vE' \<inter> last p' \<times> last p' \<noteq> {}" 
       unfolding vE'_alt by (auto)
     
     have "p'\<noteq>[]" by (simp add: p'_def collapse_aux_def)
 
     {
       txt \<open>
         We show that no visited strongly connected component contains states
         from all acceptance sets.\<close>
       fix w pl
       txt \<open>For this, we chose a non-trivial loop inside the visited edges\<close>
       assume P: "path vE' w pl w" and NT: "pl\<noteq>[]"
       txt \<open>And show that there is one acceptance set disjoint with the nodes
         of the loop\<close>
       have "\<exists>i<num_acc. \<forall>q\<in>set pl. i\<notin>acc q"
       proof cases
         assume "set pl \<inter> last p' = {}" 
           \<comment> \<open>Case: The loop is outside the last Cnode\<close>
         with path_restrict[OF P] \<open>u\<in>last p'\<close> \<open>v\<in>last p'\<close> 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 \<inter> last p' \<noteq> {}" 
           \<comment> \<open>Case: The loop touches the last Cnode\<close>
         txt \<open>Then, the loop must be completely inside the last CNode\<close>
         from inv'.loop_in_lastnode[folded vE'_def, OF P \<open>p'\<noteq>[]\<close> this] 
         have "w\<in>last p'" "set pl \<subseteq> 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') \<noteq> 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\<noteq>[]"
     assumes E: "(u,v)\<in>pE" and UIL: "u\<in>last p"
     assumes VNE: "v\<notin>\<Union>(set p)" "v\<notin>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)} \<union> E\<inter>{v}\<times>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 \<open>We show that there still is no loop that contains all accepting
         nodes. For this, we choose some loop.\<close>
       fix w pl
       assume P: "path (insert (u,v) lvE) w pl w" and [simp]: "pl\<noteq>[]"
       have "\<exists>i<num_acc. \<forall>q\<in>set pl. i\<notin>acc q" 
       proof cases
         assume "v\<in>set pl" \<comment> \<open>Case: The newly pushed last cnode is on the loop\<close>
         txt \<open>Then the loop is entirely on the last cnode\<close>
         with inv'.loop_in_lastnode[unfolded defs_fold, OF P]
         have [simp]: "w=v" and SPL: "set pl = {v}" by auto
         txt \<open>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.\<close>
         from P SPL have "u=v \<or> (v,v)\<in>lvE" 
           apply (cases pl) apply (auto simp: path_cons_conv)
           apply (case_tac list)
           apply (auto simp: path_cons_conv)
           done
         txt \<open>Both leads to a contradiction\<close>
         hence False proof
           assume "u=v" \<comment> \<open>This is impossible, as @{text "u"} was on the 
             original path, but @{text "v"} was not\<close>
           with UIL VNE show False by auto
         next
           assume "(v,v)\<in>lvE" \<comment> \<open>This is impossible, as all visited edges are
             from touched nodes, but @{text "v"} was untouched\<close>
           with vE_touched VNE show False unfolding touched_def by auto
         qed
         thus ?thesis ..
       next
         assume A: "v\<notin>set pl" 
           \<comment> \<open>Case: The newly pushed last cnode is not on the loop\<close>
         txt \<open>Then, the path lays inside the old visited edges\<close>
         have "path lvE w pl w" 
         proof -
           have "w\<in>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 \<open>And thus, the proposition follows from the invariant on the old
           state\<close>
         with no_acc show ?thesis 
           apply simp
           using \<open>pl\<noteq>[]\<close> 
           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\<noteq>[]"
     assumes E: "(u,v)\<in>pE" and UIL: "u\<in>last p"
     assumes VID: "v\<in>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 \<open>We show that there still is no loop that contains all accepting
         nodes. For this, we choose some loop.\<close>
       fix w pl
       assume P: "path (insert (u,v) lvE) w pl w" and [simp]: "pl\<noteq>[]"
       from P have "\<exists>i<num_acc. \<forall>q\<in>set pl. i\<notin>acc q" 
       proof (cases rule: path_edge_rev_cases)
         case no_use \<comment> \<open>Case: The loop does not use the new edge\<close>
         txt \<open>The proposition follows from the invariant for the old state\<close>
         with no_acc show ?thesis 
           apply simp
           using \<open>pl\<noteq>[]\<close> 
           by blast
       next
         case (split p1 p2) \<comment> \<open>Case: The loop uses the new edge\<close>
         txt \<open>As done is closed under transitions, the nodes of the edge have
           already been visited\<close>
         from split(2) D_closed_vE_rtrancl 
         have WID: "w\<in>D" 
           using VID by (auto dest!: path_is_rtrancl)
         from split(1) WID D_closed_vE_rtrancl have "u\<in>D"
           apply (cases rule: path_edge_cases)
           apply (auto dest!: path_is_rtrancl)
           done
         txt \<open>Which is a contradition to the assumptions\<close>
         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 {} \<Longrightarrow> 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\<notin>D0" "v0\<in>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\<in>D'" "path E v pl v"
       have "path (E \<inter> D' \<times> 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\<notin>D0" "v0\<in>it" 
     assumes OINV: "fgl_outer_invar it (None,D0)"
     assumes INV: "fgl_invar v0 D0 (brk,p,D',pE)"
     assumes CASES: "(\<exists>Vr Vl. brk = Some (Vr, Vl)) \<or> 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\<in>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\<^sup>*``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 \<open>Main Correctness Proof\<close>
 
 context igb_fr_graph
 begin
   lemma outer_invar_from_fgl_invarI: 
     "fgl_outer_invar it (None,D) \<Longrightarrow> 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) \<Longrightarrow> 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 \<le> 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 "_ \<inter> _ = {}"]
         solve: fgl_invar_preserve)
       done
   qed
 end
 
 section "Emptiness Check"
 text \<open>Using the lasso-finding algorithm, we can define an emptiness check\<close>
 
 context igb_fr_graph
 begin
   definition "abs_is_empty \<equiv> do {
     ce \<leftarrow> find_ce;
     RETURN (ce = None)
     }"
 
   theorem abs_is_empty_correct: 
     "abs_is_empty \<le> SPEC (\<lambda>res. res \<longleftrightarrow> (\<forall>r. \<not>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 \<equiv> do {
     ce \<leftarrow> find_ce;
     case ce of
       None \<Rightarrow> RETURN None
     | Some (Vr,Vl) \<Rightarrow> do {
         ASSERT (\<exists>pr pl. set pr \<subseteq> Vr \<and> set pl \<subseteq> Vl \<and> Vl \<times> Vl \<subseteq> (E \<inter> Vl\<times>Vl)\<^sup>* 
           \<and> is_lasso_prpl (pr,pl));
         (pr,pl) \<leftarrow> SPEC (\<lambda>(pr,pl). 
            set pr \<subseteq> Vr 
           \<and> set pl \<subseteq> Vl 
           \<and> Vl \<times> Vl \<subseteq> (E \<inter> Vl\<times>Vl)\<^sup>*
           \<and> is_lasso_prpl (pr,pl));
         RETURN (Some (pr,pl))
       }
     }"
 
   theorem abs_is_empty_ce_correct: "abs_is_empty_ce \<le> SPEC (\<lambda>res. case res of
       None \<Rightarrow> (\<forall>r. \<not>is_acc_run r)
     | Some (pr,pl) \<Rightarrow> is_acc_run (pr\<frown>pl\<^sup>\<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 \<open>Refinement\<close>
 text \<open>
   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.
 \<close>
 
 subsection \<open>Addition of Explicit Accepting Sets\<close>
 text \<open>In a first step, we explicitely keep track of the current set of
   acceptance classes for every c-node on the path.\<close>
 
 type_synonym 'a abs_gstate = "nat set list \<times> 'a abs_state"
 type_synonym 'a ce = "('a set \<times> 'a set) option"
 type_synonym 'a abs_gostate = "'a ce \<times> 'a set"
 
 context igb_fr_graph
 begin
 
   definition gstate_invar :: "'Q abs_gstate \<Rightarrow> bool" where 
     "gstate_invar \<equiv> \<lambda>(a,p,D,pE). a = map (\<lambda>V. \<Union>(acc`V)) p"
 
   definition "gstate_rel \<equiv> 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 \<Rightarrow> 'a set list \<Rightarrow> nat \<Rightarrow> nat set list \<times> 'a set list"
     where "gcollapse_aux a p i \<equiv> 
       (take i a @ [\<Union>(set (drop i a))],take i p @ [\<Union>(set (drop i p))])"
 
   definition (in -) gcollapse :: "'a \<Rightarrow> 'a abs_gstate \<Rightarrow> 'a abs_gstate" 
     where "gcollapse v APDPE \<equiv> 
     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 \<equiv> 
     let
       (a,s) = s
     in
       (a@[acc v],push v s)"
 
   definition "gpop s \<equiv>
     let (a,s) = s in (butlast a,pop s)"
 
   definition ginitial :: "'Q \<Rightarrow> 'Q abs_gostate \<Rightarrow> 'Q abs_gstate" 
     where "ginitial v0 s0 \<equiv> ([acc v0], initial v0 (snd s0))"
 
   definition goinitial :: "'Q abs_gostate" where "goinitial \<equiv> (None,{})"
   definition go_is_no_brk :: "'Q abs_gostate \<Rightarrow> bool" 
     where "go_is_no_brk s \<equiv> fst s = None"
   definition goD :: "'Q abs_gostate \<Rightarrow> 'Q set" where "goD s \<equiv> snd s"
   definition goBrk :: "'Q abs_gostate \<Rightarrow> 'Q ce" where "goBrk s \<equiv> fst s"
   definition gto_outer :: "'Q ce \<Rightarrow> 'Q abs_gstate \<Rightarrow> 'Q abs_gostate" 
     where "gto_outer brk s \<equiv> let (A,p,D,pE)=s in (brk,D)"
 
   definition "gselect_edge s \<equiv> do {
     let (a,s)=s; 
     (r,s)\<leftarrow>select_edge s;
     RETURN (r,a,s) 
   }"
 
   definition gfind_ce :: "('Q set \<times> 'Q set) option nres" where
     "gfind_ce \<equiv> do {
       let os = goinitial;
       os\<leftarrow>FOREACHci fgl_outer_invar V0 (go_is_no_brk) (\<lambda>v0 s0. do {
         if v0\<notin>goD s0 then do {
           let s = (None,ginitial v0 s0);
 
           (brk,a,p,D,pE) \<leftarrow> WHILEIT (\<lambda>(brk,a,s). fgl_invar v0 (goD s0) (brk,s))
             (\<lambda>(brk,a,p,D,pE). brk=None \<and> p \<noteq> []) (\<lambda>(_,a,p,D,pE). 
           do {
             \<comment> \<open>Select edge from end of path\<close>
             (vo,(a,p,D,pE)) \<leftarrow> gselect_edge (a,p,D,pE);
 
             ASSERT (p\<noteq>[]);
             case vo of 
               Some v \<Rightarrow> do {
                 if v \<in> \<Union>(set p) then do {
                   \<comment> \<open>Collapse\<close>
                   let (a,p,D,pE) = gcollapse v (a,p,D,pE);
 
                   ASSERT (p\<noteq>[]);
                   ASSERT (a\<noteq>[]);
 
                   if last a = {0..<num_acc} then
                     RETURN (Some (\<Union>(set (butlast p)),last p),a,p,D,pE)
                   else
                     RETURN (None,a,p,D,pE)
                 } else if v\<notin>D then do {
                   \<comment> \<open>Edge to new node. Append to path\<close>
                   RETURN (None,gpush v (a,p,D,pE))
                 } else RETURN (None,a,p,D,pE)
               }
             | None \<Rightarrow> do {
                 \<comment> \<open>No more outgoing edges from current node on path\<close>
                 ASSERT (pE \<inter> last p \<times> UNIV = {});
                 RETURN (None,gpop (a,p,D,pE))
               }
           }) s;
           ASSERT (brk=None \<longrightarrow> (p=[] \<and> pE={}));
           RETURN (gto_outer brk (a,p,D,pE))
         } else RETURN s0
     }) os;
     RETURN (goBrk os)
   }"
 
   lemma gcollapse_refine:
     "\<lbrakk>(v',v)\<in>Id; (s',s)\<in>gstate_rel\<rbrakk> 
       \<Longrightarrow> (gcollapse v' s',collapse v s)\<in>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:
     "\<lbrakk>(v',v)\<in>Id; (s',s)\<in>gstate_rel\<rbrakk> \<Longrightarrow> (gpush v' s',push v s)\<in>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:
     "\<lbrakk>(s',s)\<in>gstate_rel\<rbrakk> \<Longrightarrow> (gpop s',pop s)\<in>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) \<in> gstate_rel"
     unfolding ginitial_def gstate_rel_def br_def gstate_invar_def initial_def
     by auto
 
   lemma oinitial_b_refine: "((None,{}),(None,{}))\<in>Id\<times>\<^sub>rId" by simp
 
   lemma gselect_edge_refine: "\<lbrakk>(s',s)\<in>gstate_rel\<rbrakk> \<Longrightarrow> gselect_edge s' 
     \<le>\<Down>(\<langle>Id\<rangle>option_rel \<times>\<^sub>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\<noteq>[]"
     assumes "((a',p',D',pE'),(p,D,pE))\<in>gstate_rel"
     shows "(last a' = {0..<num_acc}) = (\<forall>i<num_acc. \<exists>q\<in>last p. i\<in>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)\<in>Id" and S: "(s',s)\<in>gstate_rel" 
       and P: "\<And>a' p' D' pE' p D pE. ((a',p',D',pE'),(p,D,pE))\<in>gstate_rel 
       \<Longrightarrow> f' a' p' D' pE' \<le>\<Down>R (f p D pE)"
     shows "(let (a',p',D',pE') = gcollapse v' s' in f' a' p' D' pE') 
       \<le> \<Down>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) \<Longrightarrow> a=[]"
     "gstate_invar ([],p,D,pE) \<Longrightarrow> p=[]"
     by (auto simp add: gstate_invar_def)
 
   lemma find_ce_refine: "gfind_ce \<le>\<Down>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 \<open>Refinement to Gabow's Data Structure\<close>
 
 subsubsection \<open>Preliminaries\<close>
 definition Un_set_drop_impl :: "nat \<Rightarrow> 'a set list \<Rightarrow> 'a set nres"
   \<comment> \<open>Executable version of @{text "\<Union>set (drop i A)"}, using indexing to
   access @{text "A"}\<close>
   where "Un_set_drop_impl i A \<equiv> 
   do {
     (_,res) \<leftarrow> WHILET (\<lambda>(i,res). i < length A) (\<lambda>(i,res). do {
       ASSERT (i<length A);
       let res = A!i \<union> res;
       let i = i + 1;
       RETURN (i,res)
     }) (i,{});
     RETURN res
   }"
 
 lemma Un_set_drop_impl_correct: 
   "Un_set_drop_impl i A \<le> SPEC (\<lambda>r. r=\<Union>(set (drop i A)))"
   unfolding Un_set_drop_impl_def
   apply (refine_rcg 
     WHILET_rule[where I="\<lambda>(i',res). res=\<Union>(set ((drop i (take i' A)))) \<and> i\<le>i'" 
     and R="measure (\<lambda>(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,{})\<in>\<langle>R\<rangle>Rs"
   assumes [autoref_rules]: "(un_impl,(\<union>))\<in>\<langle>R\<rangle>Rs\<rightarrow>\<langle>R\<rangle>Rs\<rightarrow>\<langle>R\<rangle>Rs"
   shows "(?c,Un_set_drop_impl)\<in>nat_rel \<rightarrow> \<langle>\<langle>R\<rangle>Rs\<rangle>as_rel \<rightarrow> \<langle>\<langle>R\<rangle>Rs\<rangle>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 \<le> 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 {} (\<langle>R\<rangle>Rs)"
   assumes "GEN_OP un_impl (\<union>) (\<langle>R\<rangle>Rs\<rightarrow>\<langle>R\<rangle>Rs\<rightarrow>\<langle>R\<rangle>Rs)"
   shows "(\<lambda>i A. RETURN (Un_set_drop_tr es_impl un_impl i A),Un_set_drop_impl)
     \<in>nat_rel \<rightarrow> \<langle>\<langle>R\<rangle>Rs\<rangle>as_rel \<rightarrow> \<langle>\<langle>R\<rangle>Rs\<rangle>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 \<open>Actual Refinement\<close>
 
 type_synonym 'Q gGS = "nat set list \<times> 'Q GS"
 
 type_synonym 'Q goGS = "'Q ce \<times> 'Q oGS"
 
 context igb_graph
 begin
 
 definition gGS_invar :: "'Q gGS \<Rightarrow> bool"
   where "gGS_invar s \<equiv> 
   let (a,S,B,I,P) = s in 
     GS_invar (S,B,I,P)
     \<and> length a = length B
     \<and> \<Union>(set a) \<subseteq> {0..<num_acc}
   "
 
 definition gGS_\<alpha> :: "'Q gGS \<Rightarrow> 'Q abs_gstate"
   where "gGS_\<alpha> s \<equiv> let (a,s)=s in (a,GS.\<alpha> s)"
 
 definition "gGS_rel \<equiv> br gGS_\<alpha> 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 \<Rightarrow> bool" where
   "goGS_invar s \<equiv> let (brk,ogs)=s in brk=None \<longrightarrow> oGS_invar ogs"
 
 definition "goGS_\<alpha> s \<equiv> let (brk,ogs)=s in (brk,oGS_\<alpha> ogs)"
 
 definition "goGS_rel \<equiv> br goGS_\<alpha> 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))\<in>gGS_rel"
     obtains S' B' I' P' where "s'=(a,S',B',I',P')" 
       and "((S',B',I',P'),(p,D,pE))\<in>GS_rel" 
       and "length a = length B'"
       and "\<Union>(set a) \<subseteq> {0..<num_acc}"
     using assms
     apply (cases s')
     apply (simp add: gGS_rel_def br_def gGS_\<alpha>_def GS.\<alpha>_def)
     apply (rule that)
     apply (simp only:)
     apply (auto simp: GS_rel_def br_def gGS_invar_def GS.\<alpha>_def)
     done
 
 
   definition goinitial_impl :: "'Q goGS" 
     where "goinitial_impl \<equiv> (None,Map.empty)"
   lemma goinitial_impl_refine: "(goinitial_impl,goinitial)\<in>goGS_rel"
     by (auto 
       simp: goinitial_impl_def goinitial_def goGS_rel_def br_def 
       simp: goGS_\<alpha>_def goGS_invar_def oGS_\<alpha>_def oGS_invar_def)
 
   definition gto_outer_impl :: "'Q ce \<Rightarrow> 'Q gGS \<Rightarrow> 'Q goGS"
     where "gto_outer_impl brk s \<equiv> let (A,S,B,I,P)=s in (brk,I)"
 
   lemma gto_outer_refine:
     assumes A: "brk = None \<longrightarrow> (p=[] \<and> pE={})"
     assumes B: "(s, (A,p, D, pE)) \<in> gGS_rel"
     assumes C: "(brk',brk)\<in>Id"
     shows "(gto_outer_impl brk' s,gto_outer brk (A,p,D,pE))\<in>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_\<alpha>_def gto_outer_def 
               gto_outer_impl_def goGS_invar_def 
         simp: gGS_rel_def oGS_rel_def GS_rel_def gGS_\<alpha>_def gGS_invar_def 
               GS.\<alpha>_def) []
 
       using B apply (auto 
         simp: gto_outer_def gto_outer_impl_def
         simp: br_def goGS_rel_def goGS_invar_def goGS_\<alpha>_def oGS_\<alpha>_def
         simp: gGS_rel_def gGS_\<alpha>_def GS.\<alpha>_def GS.D_\<alpha>_def
       )
 
       done
   qed
 
   definition "gpush_impl v s \<equiv> let (a,s)=s in (a@[acc v], push_impl v s)"
 
 
   lemma gpush_impl_refine:
     assumes B: "(s',(a,p,D,pE))\<in>gGS_rel"
     assumes A: "(v',v)\<in>Id" 
     assumes PRE: "v' \<notin> \<Union>(set p)" "v' \<notin> D"
     shows "(gpush_impl v' s', gpush v (a,p,D,pE))\<in>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))\<in>GS_rel" and L: "length a = length B'" 
       and R: "\<Union>(set a) \<subseteq> {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_\<alpha>_def GS_rel_def br_def
       apply (auto dest: AUX1)
       done
   qed
   
   definition gpop_impl :: "'Q gGS \<Rightarrow> 'Q gGS nres" 
     where "gpop_impl s \<equiv> do {
     let (a,s)=s;
     s\<leftarrow>pop_impl s;
     ASSERT (a\<noteq>[]);
     let a = butlast a;
     RETURN (a,s)
   }"
 
   lemma gpop_impl_refine:
     assumes A: "(s',(a,p,D,pE))\<in>gGS_rel"
     assumes PRE: "p \<noteq> []" "pE \<inter> last p \<times> UNIV = {}"
     shows "gpop_impl s' \<le> \<Down>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))\<in>GS_rel" and L: "length a = length B'"
       and R: "\<Union>(set a) \<subseteq> {0..<num_acc}"
       by (rule gGS_relE)
 
     from PRE OSR have [simp]: "a\<noteq>[]" using L
       by (auto simp add: GS_rel_def br_def GS.\<alpha>_def GS.p_\<alpha>_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_\<alpha>_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_\<alpha>_def GS_rel_def GS.\<alpha>_def br_def
       apply (auto dest!: AUX1 in_set_butlastD iff: Sup_le_iff)
       done
   qed
   
   definition gselect_edge_impl :: "'Q gGS \<Rightarrow> ('Q option \<times> 'Q gGS) nres" 
     where "gselect_edge_impl s \<equiv> 
     do { 
       let (a,s)=s; 
       (vo,s)\<leftarrow>select_edge_impl s; 
       RETURN (vo,a,s)
     }"
 
   thm select_edge_refine
   lemma gselect_edge_impl_refine:
     assumes A: "(s', a, p, D, pE) \<in> gGS_rel" 
     assumes PRE: "p \<noteq> []"
     shows "gselect_edge_impl s' \<le> \<Down>(Id \<times>\<^sub>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))\<in>GS_rel" and L: "length a = length B'"
       and R: "\<Union>(set a) \<subseteq> {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_\<alpha>_def gGS_invar_def GS_rel_def GS.\<alpha>_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 \<Rightarrow> 'Q gGS \<Rightarrow> 'Q gGS nres" where 
     "gcollapse_impl_aux v s \<equiv> 
     do { 
       let (A,s)=s;
       \<^cancel>\<open>ASSERT (v\<in>\<Union>set (GS.p_\<alpha> s));\<close>
       i \<leftarrow> GS.idx_of_impl s v;
       s \<leftarrow> collapse_impl v s;
       ASSERT (i < length A);
       us \<leftarrow> 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=\<Union>(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) \<in> gGS_rel" 
     assumes B: "(v',v)\<in>Id"
     assumes PRE: "v\<in>\<Union>(set p)"
     shows "gcollapse_impl_aux v' s' 
       \<le> \<Down> 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))\<in>GS_rel" and L: "length a = length B'"
       and R: "\<Union>(set a) \<subseteq> {0..<num_acc}"
       by (rule gGS_relE)
 
     from B have [simp]: "v'=v" by simp
 
     from OSR have [simp]: "GS.p_\<alpha> (S',B',I',P') = p"
       by (simp add: GS_rel_def br_def GS.\<alpha>_def)
 
     from OSR PRE have PRE': "v \<in> \<Union>(set (GS.p_\<alpha> (S',B',I',P')))"
       by (simp add: GS_rel_def br_def GS.\<alpha>_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_\<alpha> s, GS.D_\<alpha> s, GS.pE_\<alpha> 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_\<alpha>_def)
         apply (drule arg_cong[where f=length])
         using GS_invar.p_\<alpha>_disjoint_sym[OF GS_invar]
           and PRE \<open>GS.p_\<alpha> (S', B', I', P') = p\<close> 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.\<alpha>_def br_def gGS_\<alpha>_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 \<Rightarrow> 'Q gGS \<Rightarrow> 'Q gGS nres" 
     where "gcollapse_impl v s \<equiv>     
     do { 
       let (A,S,B,I,P)=s;
       i \<leftarrow> GS.idx_of_impl (S,B,I,P) v;
       ASSERT (i+1 \<le> length B);
       let B = take (i+1) B;
       ASSERT (i < length A);
       us\<leftarrow>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 \<le> 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) \<in> gGS_rel" 
     assumes B: "(v',v)\<in>Id"
     assumes PRE: "v\<in>\<Union>(set p)"
     shows "gcollapse_impl v' s' 
     \<le> \<Down> 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 \<Rightarrow> 'Q goGS \<Rightarrow> 'Q gGS" 
     where "ginitial_impl v0 s0 \<equiv> ([acc v0],initial_impl v0 (snd s0))"
   lemma ginitial_impl_refine: 
     assumes A: "v0\<notin>goD s0" "go_is_no_brk s0"
     assumes REL: "(s0i,s0)\<in>goGS_rel" "(v0i,v0)\<in>Id" 
     shows "(ginitial_impl v0i s0i,ginitial v0 s0)\<in>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_\<alpha>_def gGS_invar_def goGS_rel_def goGS_\<alpha>_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 \<Rightarrow> bool"
     where "gpath_is_empty_impl s = path_is_empty_impl (snd s)"
 
   lemma gpath_is_empty_refine: 
     "(s,(a,p,D,pE))\<in>gGS_rel \<Longrightarrow> gpath_is_empty_impl s \<longleftrightarrow> p=[]"
     unfolding gpath_is_empty_impl_def 
     using path_is_empty_refine
     by (fastforce simp: gGS_rel_def br_def gGS_invar_def gGS_\<alpha>_def GS.\<alpha>_def)
 
   definition gis_on_stack_impl :: "'Q \<Rightarrow> 'Q gGS \<Rightarrow> bool" 
     where "gis_on_stack_impl v s = is_on_stack_impl v (snd s)"
 
   lemma gis_on_stack_refine: 
     "\<lbrakk>(s,(a,p,D,pE))\<in>gGS_rel\<rbrakk> \<Longrightarrow> gis_on_stack_impl v s \<longleftrightarrow> v\<in>\<Union>(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_\<alpha>_def GS.\<alpha>_def)
 
   definition gis_done_impl :: "'Q \<Rightarrow> 'Q gGS \<Rightarrow> bool"
     where "gis_done_impl v s \<equiv> is_done_impl v (snd s)"
   thm is_done_refine
   lemma gis_done_refine: "(s,(a,p,D,pE))\<in>gGS_rel 
     \<Longrightarrow> gis_done_impl v s \<longleftrightarrow> (v \<in> D)"
     using is_done_refine[of "(snd s)" v]
     by (auto 
       simp: gGS_rel_def br_def gGS_\<alpha>_def gGS_invar_def GS.\<alpha>_def 
             gis_done_impl_def)
 
 
   definition (in -) "on_stack_less I u v \<equiv> 
     case I v of 
       Some (STACK j) \<Rightarrow> j<u
     | _ \<Rightarrow> False"
 
   definition (in -) "on_stack_ge I l v \<equiv> 
     case I v of 
       Some (STACK j) \<Rightarrow> l\<le>j
     | _ \<Rightarrow> False"
 
 
   lemma (in GS_invar) set_butlast_p_refine:
     assumes PRE: "p_\<alpha>\<noteq>[]"
     shows "Collect (on_stack_less I (last B)) = \<Union>(set (butlast p_\<alpha>))" (is "?L=?R")
   proof (intro equalityI subsetI)
     from PRE have [simp]: "B\<noteq>[]" by (auto simp: p_\<alpha>_def)
 
     have [simp]: "S\<noteq>[]"
       by (simp add: empty_eq)
 
     {
       fix v
       assume "v\<in>?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 \<open>j<last B\<close> have "j<B!(length B - 1)" by (simp add: last_conv_nth)
       from find_seg_bounds[OF \<open>j<length S\<close>] find_seg_correct[OF \<open>j<length S\<close>]
       have "v\<in>seg (find_seg j)" "find_seg j < length B" by auto
       moreover with \<open>j<B!(length B - 1)\<close> 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: "\<And>x\<^sub>1 x. \<not> (x\<^sub>1::nat) < x\<^sub>1 - x"
           using less_imp_diff_less by blast
         have "j \<le> last B"
           by (metis \<open>j < last B\<close> less_le)
         hence f2: "\<And>x\<^sub>1. \<not> last B < x\<^sub>1 \<or> \<not> x\<^sub>1 \<le> j"
           using f1 by (metis diff_diff_cancel le_trans)
         have "\<And>x\<^sub>1. seg_end x\<^sub>1 \<le> j \<or> \<not> x\<^sub>1 < find_seg j"
           by (metis \<open>seg_start (find_seg j) \<le> j\<close> calculation(2) 
             le_trans seg_end_less_start)
         thus "find_seg j < length B - 1"
           using f1 f2 
           by (metis GS.seg_start_def \<open>B \<noteq> []\<close> \<open>j < B ! (length B - 1)\<close>
             \<open>seg_start (find_seg j) \<le> j\<close> calculation(2) diff_diff_cancel 
             last_conv_nth nat_neq_iff seg_start_less_end)
       qed
       ultimately show "v\<in>?R" 
         by (auto simp: p_\<alpha>_def map_butlast[symmetric] butlast_upt)
     }
 
     {
       fix v
       assume "v\<in>?R"
       then obtain i where "i<length B - 1" and "v\<in>seg i"
         by (auto simp: p_\<alpha>_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 \<le> length B - 1" using \<open>i<length B - 1\<close>
         by (auto simp: seg_end_def last_conv_nth split: if_split_asm)
       with sorted_nth_mono[OF B_sorted \<open>i+1 \<le> length B - 1\<close>] have "j<last B"
         by (auto simp: last_conv_nth)
       moreover from \<open>j < seg_end i\<close> have "j<length S"
         by (metis GS.seg_end_def add_diff_inverse_nat \<open>i + 1 \<le> length B - 1\<close>
           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 \<open>v=S!j\<close> have "I v = Some (STACK j)" by auto
       ultimately show "v\<in>?L"
         by (auto simp: on_stack_less_def)
     }
   qed
 
   lemma (in GS_invar) set_last_p_refine:
     assumes PRE: "p_\<alpha>\<noteq>[]"
     shows "Collect (on_stack_ge I (last B)) = last p_\<alpha>" (is "?L=?R")
   proof (intro equalityI subsetI)
     from PRE have [simp]: "B\<noteq>[]" by (auto simp: p_\<alpha>_def)
 
     have [simp]: "S\<noteq>[]" by (simp add: empty_eq)
 
     {
       fix v
       assume "v\<in>?L"
       then obtain j where [simp]: "I v = Some (STACK j)" and "j\<ge>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\<in>seg (length B - 1)" using \<open>j\<ge>last B\<close>
         by (auto simp: seg_def last_conv_nth seg_start_def seg_end_def)
       thus "v\<in>last p_\<alpha>" by (auto simp: p_\<alpha>_def last_map)
     }
 
     {
       fix v
       assume "v\<in>?R"
       hence "v\<in>seg (length B - 1)"
         by (auto simp: p_\<alpha>_def last_map)
       then obtain j where "v=S!j" "j\<ge>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 \<open>j\<ge>last B\<close> show "v\<in>?L" by (auto simp: on_stack_ge_def)
     }
   qed
 
   definition ce_impl :: "'Q gGS \<Rightarrow> (('Q set \<times> 'Q set) option \<times> 'Q gGS) nres"
     where "ce_impl s \<equiv> 
     do {
       let (a,S,B,I,P) = s;
       ASSERT (B\<noteq>[]);
       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))\<in>gGS_rel"
     assumes PRE: "p\<noteq>[]"
     shows "ce_impl s \<le> \<Down>(Id\<times>\<^sub>rgGS_rel) 
       (RETURN (Some (\<Union>(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))\<in>GS_rel" and L: "length a = length B'"
       by (rule gGS_relE)
 
     from OSR have [simp]: "GS.p_\<alpha> (S',B',I',P') = p"
       by (simp add: GS_rel_def br_def GS.\<alpha>_def)
 
     from PRE have NE': "GS.p_\<alpha> (S', B', I', P') \<noteq> []" by simp
     hence BNE[simp]: "B'\<noteq>[]" by (simp add: GS.p_\<alpha>_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 \<equiv> 
     do {
       let (a,_)=s;
       ASSERT (a\<noteq>[]);
       RETURN (\<forall>i<num_acc. i\<in>last a)
     }"
 
   lemma last_is_acc_impl_refine:
     assumes A: "(s,(a,p,D,pE))\<in>gGS_rel"
     assumes PRE: "a\<noteq>[]"
     shows "last_is_acc_impl s \<le> RETURN (last a = {0..<num_acc})"
   proof -
     from A PRE have "last a \<subseteq> {0..<num_acc}"
       unfolding gGS_rel_def gGS_invar_def br_def gGS_\<alpha>_def by auto
     hence C: "(\<forall>i<num_acc. i\<in>last a) \<longleftrightarrow> (last a = {0..<num_acc})"
       by auto
 
     from A obtain gs where [simp]: "s=(a,gs)"
       by (auto simp: gGS_rel_def gGS_\<alpha>_def br_def split: prod.splits)
 
     show ?thesis
       unfolding last_is_acc_impl_def 
       by (auto simp: gGS_rel_def br_def gGS_\<alpha>_def C PRE split: prod.splits)
   qed
 
   definition go_is_no_brk_impl :: "'Q goGS \<Rightarrow> bool" 
     where "go_is_no_brk_impl s \<equiv> fst s = None"
   lemma go_is_no_brk_refine: 
     "(s,s')\<in>goGS_rel \<Longrightarrow> go_is_no_brk_impl s \<longleftrightarrow> 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_\<alpha>_def split: prod.splits)
 
   definition goD_impl :: "'Q goGS \<Rightarrow> 'Q oGS" where "goD_impl s \<equiv> snd s"
   lemma goD_refine: 
     "go_is_no_brk s' \<Longrightarrow> (s,s')\<in>goGS_rel \<Longrightarrow> (goD_impl s, goD s')\<in>oGS_rel"
     unfolding goD_impl_def goD_def
     by (auto 
       simp: goGS_rel_def br_def goGS_\<alpha>_def goGS_invar_def oGS_rel_def 
             go_is_no_brk_def) 
 
   definition go_is_done_impl :: "'Q \<Rightarrow> 'Q goGS \<Rightarrow> bool" 
     where "go_is_done_impl v s \<equiv> is_done_oimpl v (snd s)"
   thm is_done_orefine
   lemma go_is_done_impl_refine: "\<lbrakk>go_is_no_brk s'; (s,s')\<in>goGS_rel; (v,v')\<in>Id\<rbrakk> 
     \<Longrightarrow> go_is_done_impl v s \<longleftrightarrow> (v'\<in>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_\<alpha>_def)
     done
 
 
   definition goBrk_impl :: "'Q goGS \<Rightarrow> 'Q ce" where "goBrk_impl \<equiv> fst"
 
   lemma goBrk_refine: "(s,s')\<in>goGS_rel \<Longrightarrow> (goBrk_impl s, goBrk s')\<in>Id"
     unfolding goBrk_impl_def goBrk_def
     by (auto simp: goGS_rel_def br_def goGS_\<alpha>_def split: prod.splits)
 
   definition find_ce_impl :: "('Q set \<times> 'Q set) option nres" where
     "find_ce_impl \<equiv> do {
       stat_start_nres;
       let os=goinitial_impl;
       os\<leftarrow>FOREACHci (\<lambda>it os. fgl_outer_invar it (goGS_\<alpha> os)) V0 
         (go_is_no_brk_impl) (\<lambda>v0 s0. 
       do {
         if \<not>go_is_done_impl v0 s0 then do {
 
           let s = (None,ginitial_impl v0 s0);
 
           (brk,s)\<leftarrow>WHILEIT 
             (\<lambda>(brk,s). fgl_invar v0 (oGS_\<alpha> (goD_impl s0)) (brk,snd (gGS_\<alpha> s)))
             (\<lambda>(brk,s). brk=None \<and> \<not>gpath_is_empty_impl s) (\<lambda>(l,s).
           do {
             \<comment> \<open>Select edge from end of path\<close>
             (vo,s) \<leftarrow> gselect_edge_impl s;
 
             case vo of 
               Some v \<Rightarrow> do {
                 if gis_on_stack_impl v s then do {
                   s\<leftarrow>gcollapse_impl v s;
                   b\<leftarrow>last_is_acc_impl s;
                   if b then
                     ce_impl s
                   else 
                     RETURN (None,s)
                 } else if \<not>gis_done_impl v s then do {
                   \<comment> \<open>Edge to new node. Append to path\<close>
                   RETURN (None,gpush_impl v s)
                 } else do {
                   \<comment> \<open>Edge to done node. Skip\<close>
                   RETURN (None,s)
                 }
               }
             | None \<Rightarrow> do {
                 \<comment> \<open>No more outgoing edges from current node on path\<close>
                 s\<leftarrow>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 \<le> \<Down>Id gfind_ce"
   proof -
     note [refine2] = prod_relI[OF IdI[of None] ginitial_impl_refine]
 
     have [refine]: "\<And>s a p D pE. \<lbrakk>
       (s,(a,p,D,pE))\<in>gGS_rel;
       p \<noteq> []; pE \<inter> last p \<times> UNIV = {}
       \<rbrakk> \<Longrightarrow>
       gpop_impl s \<bind> (\<lambda>s. RETURN (None, s))
         \<le> SPEC (\<lambda>c. (c, None, gpop (a,p,D,pE)) \<in> Id \<times>\<^sub>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_\<alpha>_def gGS_\<alpha>_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 \<open>Constructing a Lasso from Counterexample\<close>
 
 subsection \<open>Lassos in GBAs\<close>
 
 context igb_fr_graph begin
 
   definition reconstruct_reach :: "'Q set \<Rightarrow> 'Q set \<Rightarrow> ('Q list \<times> 'Q) nres"
     \<comment> \<open>Reconstruct the reaching path of a lasso\<close>
     where "reconstruct_reach Vr Vl \<equiv> do {
       res \<leftarrow> find_path (E\<inter>Vr\<times>UNIV) V0 (\<lambda>v. v\<in>Vl);
       ASSERT (res \<noteq> None);
       RETURN (the res)
     }"
 
   lemma reconstruct_reach_correct:
     assumes CEC: "ce_correct Vr Vl"
     shows "reconstruct_reach Vr Vl 
       \<le> SPEC (\<lambda>(pr,va). \<exists>v0\<in>V0. path E v0 pr va \<and> va\<in>Vl)"
   proof -
     have FIN_aux: "finite ((E \<inter> Vr \<times> UNIV)\<^sup>* `` 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 \<subseteq> Vr"
       have "path (E \<inter> Vr\<times>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\<in>V0" "set pr \<subseteq> Vr" "va\<in>Vl" 
       "path (E \<inter> Vr\<times>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 \<in> (E \<inter> Vr \<times> UNIV)\<^sup>* `` 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 \<open>va\<in>Vl\<close> 1 apply auto []
 
       apply (auto dest: path_mono[of "E \<inter> Vr \<times> UNIV" E, simplified]) []
       done
   qed
 
   definition "rec_loop_invar Vl va s \<equiv> let (v,p,cS) = s in 
     va \<in> E\<^sup>*``V0 \<and>
     path E va p v \<and>
     cS = acc v \<union> (\<Union>(acc`set p)) \<and>
     va \<in> Vl \<and> v \<in> Vl \<and> set p \<subseteq> Vl"
 
   definition reconstruct_lasso :: "'Q set \<Rightarrow> 'Q set \<Rightarrow> ('Q list \<times> 'Q list) nres"
     \<comment> \<open>Reconstruct lasso\<close>
     where "reconstruct_lasso Vr Vl \<equiv> do {
     (pr,va) \<leftarrow> reconstruct_reach Vr Vl;
     
     let cS_full = {0..<num_acc};
     let E = E \<inter> UNIV\<times>Vl;
     
     (vd,p,_) \<leftarrow> WHILEIT (rec_loop_invar Vl va) 
       (\<lambda>(_,_,cS). cS \<noteq> cS_full) 
       (\<lambda>(v,p,cS). do {
         ASSERT (\<exists>v'. (v,v')\<in>E\<^sup>* \<and> \<not> (acc v' \<subseteq> cS));
         sr \<leftarrow> find_path E {v} (\<lambda>v. \<not> (acc v \<subseteq> cS));
         ASSERT (sr \<noteq> None);
         let (p_seg,v) = the sr;
         RETURN (v,p@p_seg,cS \<union> acc v)
       }) (va,[],acc va);
 
     p_close_r \<leftarrow> (if p=[] then 
         find_path1 E vd ((=) va)
       else
         find_path E {vd} ((=) va));
 
     ASSERT (p_close_r \<noteq> 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 \<le> SPEC (is_lasso_prpl)"
 proof -
 
   let ?E = "E \<inter> UNIV \<times> Vl"
 
   have E_SS: "E \<inter> Vl \<times> Vl \<subseteq> ?E" by auto
 
   from CEC have
     REACH: "Vl \<subseteq> E\<^sup>*``V0"
     and CONN: "Vl\<times>Vl \<subseteq> (E \<inter> Vl\<times>Vl)\<^sup>*"
     and NONTRIV: "Vl\<times>Vl \<inter> E \<noteq> {}"
     and NES[simp]: "Vl\<noteq>{}"
     and ALL: "\<Union>(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}) (\<lambda>(_::'Q,_::'Q list,cS). cS))"
   hence WF: "wf term_rel" by simp
 
   { fix va
     assume "va \<in> 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)\<^sup>* `` {v})"
       apply -
       apply (rule finite_subset[where B="E\<^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 \<noteq> {0..<num_acc}"
 
     from NC INV obtain i where "i<num_acc" "i\<notin>cS" 
       unfolding rec_loop_invar_def by auto blast
 
-    with ALL obtain v' where "v'\<in>Vl" "\<not> acc v' \<subseteq> cS"
-      by simp (smt UN_iff atLeastLessThan_iff le0 subsetCE)
+    with ALL obtain v' where v': "v'\<in>Vl" "\<not> acc v' \<subseteq> cS"
+      by (metis NES atLeastLessThan_iff cSUP_least in_mono zero_le)
      
-    moreover with CONN INV have "(v,v')\<in>(E \<inter> Vl \<times> Vl)\<^sup>*"
+    with CONN INV have "(v,v')\<in>(E \<inter> Vl \<times> Vl)\<^sup>*"
       unfolding rec_loop_invar_def by auto
     hence "(v,v')\<in>?E\<^sup>*" using rtrancl_mono_mp[OF E_SS] by blast
-    ultimately have "\<exists>v'. (v,v')\<in>(?E)\<^sup>* \<and> \<not> acc v' \<subseteq> cS" by auto
+    with v' have "\<exists>v'. (v,v')\<in>(?E)\<^sup>* \<and> \<not> acc v' \<subseteq> 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 "\<not> (acc v' \<subseteq> cS)"
     and "\<forall>v\<in>set p'. acc v \<subseteq> cS"
     hence "rec_loop_invar Vl va (v', p@p', cS \<union> 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 "\<not> (acc v' \<subseteq> cS)"
       and "\<forall>v\<in>set p'. acc v \<subseteq> cS"
     hence "((v', p@p', cS \<union> acc v'), (v,p,cS)) \<in> term_rel"
       unfolding term_rel_def rec_loop_invar_def
       by (auto simp: finite_psupset_def)
   } note VAR = this
 
   have CONN1: "Vl \<times> Vl \<subseteq> (?E)\<^sup>+"
   proof clarify
     fix a b
     assume "a\<in>Vl" "b\<in>Vl"
     from NONTRIV obtain u v where E: "(u,v)\<in>(E \<inter> Vl\<times>Vl)" by auto
     from CONN \<open>a\<in>Vl\<close> E have "(a,u)\<in>(E\<inter>Vl\<times>Vl)\<^sup>*" by auto
     also note E
     also (rtrancl_into_trancl1) from CONN \<open>b\<in>Vl\<close> E have "(v,b)\<in>(E\<inter>Vl\<times>Vl)\<^sup>*"
       by auto
     finally show "(a,b)\<in>(?E)\<^sup>+" 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) \<in> (?E)\<^sup>+"
       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) \<in> (?E)\<^sup>*"
       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 \<in> Vl" "v0 \<in> V0"
       "path E v0 pr va" "pl \<noteq> []" "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\<noteq>[]" "path ?E v p' va"
       and PR: "v0\<in>V0" "path E v0 pr va"
 
     from INV have "\<forall>i<num_acc. \<exists>q\<in>insert v (set p). i \<in> acc q"
       unfolding rec_loop_invar_def
       by auto
     moreover from INV 1 have "insert v (set p) \<subseteq> set p \<union> set p'"
       unfolding rec_loop_invar_def
       apply (cases p)
       apply blast
       apply (cases p')
       apply (auto simp: path_simps)
       done
     ultimately have ACC: "\<forall>i<num_acc. \<exists>q\<in>set p \<union> set p'. i \<in> 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 \<open>p\<noteq>[]\<close> 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 \<equiv> do {
   ce \<leftarrow> find_ce_spec;
   case ce of 
     None \<Rightarrow> RETURN None
   | Some (Vr,Vl) \<Rightarrow> do {
       l \<leftarrow> reconstruct_lasso Vr Vl;
       RETURN (Some l)
     }
 }"
 
 lemma (in igb_fr_graph) find_lasso_correct: "find_lasso \<le> 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
diff --git a/thys/No_FTL_observers/Axioms.thy b/thys/No_FTL_observers/Axioms.thy
--- a/thys/No_FTL_observers/Axioms.thy
+++ b/thys/No_FTL_observers/Axioms.thy
@@ -1,266 +1,266 @@
 (*
    Author: Mike Stannett
    Date: 22 October 2012
    m.stannett@sheffield.ac.uk
 *)
 theory Axioms
 imports SpaceTime SomeFunc
 begin
 
 record Body =
   Ph :: "bool"
   IOb :: "bool"
 
 
 class WorldView = SpaceTime +
 fixes
   (* Worldview relation *)
   W :: "Body \<Rightarrow> Body \<Rightarrow> 'a Point \<Rightarrow> bool" ("_ sees _ at _")
 and
   (* Worldview transformation *)
   wvt :: "Body \<Rightarrow> Body \<Rightarrow> 'a Point \<Rightarrow> 'a Point"
 assumes
   AxWVT: "\<lbrakk> IOb m; IOb k \<rbrakk> \<Longrightarrow> (W k b x \<longleftrightarrow> W m b (wvt m k x))"
 and
   AxWVTSym: "\<lbrakk> IOb m; IOb k \<rbrakk> \<Longrightarrow> (y = wvt k m x  \<longleftrightarrow>  x = wvt m k y)"
 begin
 end
 
 
 (* THE BASIC AXIOMS *)
 (* ================ *)
 
 
 class AxiomPreds = WorldView 
 begin
   fun sqrtTest :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where
      "sqrtTest x r = ((r \<ge> 0) \<and> (r*r = x))"
 
   fun cTest :: "Body \<Rightarrow> 'a \<Rightarrow> bool" where
     "cTest m v = ( (v > 0) \<and> ( \<forall>x y . ( 
                (\<exists>p. (Ph p \<and> W m p x \<and> W m p y)) \<longleftrightarrow> (space2 x y = (v * v)*(time2 x y)) 
              )))"
 end
 
 (*
   AxEuclidean
   Quantities form a Euclidean field, ie positive quantities have
   square roots. We introduce a function, sqrt, that determines them.
 *)
 class AxEuclidean = AxiomPreds + Quantities +
 assumes
   AxEuclidean: "(x \<ge> Groups.zero_class.zero) \<Longrightarrow> (\<exists>r. sqrtTest x r)"
 begin
 
   abbreviation sqrt :: "'a \<Rightarrow> 'a" where
      "sqrt \<equiv> someFunc sqrtTest"
 
   lemma lemSqrt: 
     assumes "x \<ge> 0"
       and   "r = sqrt x"
     shows   "r \<ge> 0  \<and>  r*r = x"
   proof -
     have rootExists: "(\<exists>r. sqrtTest x r)" by (metis AxEuclidean assms(1))
     hence "sqrtTest x (sqrt x)" by (metis lemSomeFunc)
     thus ?thesis using assms(2) by simp
   qed
 
 end
 
 
 (* 
    AxLight
    There is an inertial observer, according to whom, any light
    signal moves with the same velocity in any direction 
 *)
 class AxLight = WorldView +
 assumes
   AxLight: "\<exists>m v.( IOb m \<and> (v > (0::'a)) \<and> ( \<forall>x y.( 
               (\<exists>p.(Ph p \<and> W m p x \<and> W m p y)) \<longleftrightarrow> (space2 x y = (v * v)*time2 x y) 
             )))"
 begin
 end
 
 
 
 (*
   AxPh
   For any inertial observer, the speed of light is the same in every
   direction everywhere, and it is finite. Furthermore, it is possible
   to send out a light signal in any direction.
 *)
 class AxPh = WorldView + AxiomPreds +
 assumes
   AxPh: "IOb m \<Longrightarrow> (\<exists>v. cTest m v)"
 begin
 
   abbreviation c :: "Body \<Rightarrow> 'a" where
     "c \<equiv> someFunc cTest"
 
   fun lightcone :: "Body \<Rightarrow> 'a Point \<Rightarrow> 'a Cone" where
     "lightcone m v = mkCone v (c m)"
 
 
 lemma lemCProps:
   assumes "IOb m"
      and  "v = c m"
   shows "(v > 0) \<and> (\<forall>x y.((\<exists>p. (Ph p \<and> W m p x \<and> W m p y)) 
                       \<longleftrightarrow> ( space2 x y = (c m * c m)*time2 x y )))"
 proof -
   have vExists: "(\<exists>v. cTest m v)" by (metis AxPh assms(1))
   hence "cTest m (c m)" by (metis lemSomeFunc)
   thus ?thesis using assms(2) by simp
 qed
 
 
 lemma lemCCone: 
   assumes "IOb m"
     and   "onCone y (lightcone m x)"
   shows   "\<exists>p. (Ph p \<and> W m p x \<and> W m p y)"
 proof -
   have "(\<exists>p.(Ph p \<and> W m p x \<and> W m p y)) 
                       \<longleftrightarrow> ( space2 x y = (c m * c m)*time2 x y )"
-    by (smt assms(1) lemCProps)
+    by (simp add: assms(1) lemCProps)
   hence ph_exists: "(space2 x y = (c m * c m)*time2 x y) \<longrightarrow> (\<exists>p.(Ph p \<and> W m p x \<and> W m p y))"
     by metis
   define lcmx where "lcmx = lightcone m x"
   have lcmx_vertex: "vertex lcmx = x" by (simp add: lcmx_def)
   have lcmx_slope: "slope lcmx = c m" by (simp add: lcmx_def)
   have "onCone y lcmx \<longrightarrow> (space2 x y = (c m * c m)*time2 x y)" 
     by (metis lcmx_vertex lcmx_slope onCone.simps)
   hence "space2 x y = (c m * c m)*time2 x y" by (metis lcmx_def assms(2))
   thus ?thesis by (metis ph_exists)
 qed
 
 
 lemma lemCPos: 
   assumes "IOb m"
   shows   "c m > 0"
   by (metis assms(1) lemCProps)
 
 
 lemma lemCPhoton:
   assumes "IOb m"
   shows "\<forall>x y. (\<exists>p. (Ph p \<and> W m p x \<and> W m p y)) \<longleftrightarrow> (space2 x y = (c m * c m)*(time2 x y))"
   by (metis assms(1) lemCProps)
 
 end
 
 
 
 (*
   AxEv
   Inertial observers see the same events (meetings of bodies).
   This also enables us to discuss the worldview transformation.
 *)
 class AxEv = WorldView +
 assumes
   AxEv: "\<lbrakk> IOb m; IOb k\<rbrakk> \<Longrightarrow>  (\<exists>y. (\<forall>b. (W m b x  \<longleftrightarrow> W k b y)))"
 begin
 end
 
 
 
 (*
   Inertial observers can move with any speed slower than that of light
 *)
 class AxThExp = WorldView + AxPh +
 assumes
     AxThExp: "IOb m \<Longrightarrow> (\<forall>x y .( 
        (\<exists>k.(IOb k \<and> W m k x \<and> W m k y)) \<longleftrightarrow> (space2 x y < (c m * c m) * time2 x y) 
        ))"
 
 begin
 end
 
 
 
 (*
   Every inertial observer is stationary according to himself
 *)
 class AxSelf = WorldView +
 assumes
   AxSelf: "IOb m  \<Longrightarrow>  (W m m x) \<longrightarrow> (onAxisT x)"
 begin
 end
 
 
 
 (* 
   All inertial observers agree that the speed of light is 1
 *)
 class AxC = WorldView + AxPh +
 assumes
   AxC: "IOb m \<Longrightarrow> c m = 1"
 begin
 end
 
 
 (*
   Inertial observers agree as to the spatial distance between two
   events if these two events are simultaneous for both of them.
 *)
 class AxSym = WorldView +
 assumes
   AxSym: "\<lbrakk> IOb m; IOb k \<rbrakk> \<Longrightarrow>
             (W m e x \<and> W m f y \<and> W k e x'\<and> W k f y' \<and>
             tval x = tval y \<and> tval x' = tval y' )
           \<longrightarrow> (space2 x y = space2 x' y')"
 begin
 end
 
 
 
 (*
   AxLines
   All observers agree about lines
 *)
 class AxLines = WorldView + 
 assumes
   AxLines: "\<lbrakk> IOb m; IOb k; collinear x p q \<rbrakk> \<Longrightarrow> 
      collinear (wvt k m x) (wvt k m p) (wvt k m q)"
 begin
 end
 
 
 
 (*
   AxPlanes
   All observers agree about planes
 *)
 class AxPlanes = WorldView +
 assumes
   AxPlanes: "\<lbrakk> IOb m; IOb k \<rbrakk> \<Longrightarrow> 
      (coplanar e x y z  \<longrightarrow> coplanar (wvt k m e) (wvt k m x) (wvt k m y) (wvt k m z))"
 begin
 end
 
 
 
 (*
   AxCones
   All observers agree about lightcones
 *)
 class AxCones = WorldView + AxPh +
 assumes
   AxCones: "\<lbrakk> IOb m; IOb k \<rbrakk> \<Longrightarrow> 
      ( onCone x (lightCone m v) \<longrightarrow> onCone (wvt k m x) (lightcone k (wvt k m v)))"
 begin
 end
 
 
 
 (*
   All inertial observers see time travelling in the same direction. That
   is, if m thinks that k reached y after he reached x, then
   k should also think that he reached y after he reached x.
 *)
 class AxTime = WorldView +
 assumes 
   AxTime: "\<lbrakk> IOb m; IOb k \<rbrakk> 
               \<Longrightarrow>( x \<lesssim> y \<longrightarrow> wvt k m x \<lesssim> wvt k m y )"
 begin
 end
 
 
 end
diff --git a/thys/X86_Semantics/Memory.thy b/thys/X86_Semantics/Memory.thy
--- a/thys/X86_Semantics/Memory.thy
+++ b/thys/X86_Semantics/Memory.thy
@@ -1,358 +1,361 @@
 (*  Title:       X86 instruction semantics and basic block symbolic execution
     Authors:     Freek Verbeek, Abhijith Bharadwaj, Joshua Bockenek, Ian Roessle, Timmy Weerwag, Binoy Ravindran
     Year:        2020
     Maintainer:  Freek Verbeek (freek@vt.edu)
 *)
 
 section "Memory-related theorems"
 
 theory Memory
   imports BitByte
 begin
 
 context
   fixes dummy_type :: "'a::len"
 begin
 
 primrec read_bytes :: "('a word \<Rightarrow> 8 word) \<Rightarrow> 'a word \<Rightarrow> nat \<Rightarrow> 8word list"
   where "read_bytes m a 0   = []"
   | "read_bytes m a (Suc n) = m (a + of_nat n) # read_bytes m a n"
 
 text \<open>Read bytes from memory. Memory is represented by a term of @{typ "64 word \<Rightarrow> 8 word"}.
       Given an address @{term [show_types] "a::64 word"} and a size @{term n}, retrieve the bytes in
       the order they are stored in memory.\<close>
 
 definition region_addresses :: "'a word \<Rightarrow> nat \<Rightarrow> 'a word set"
   where "region_addresses a si \<equiv> {a' . \<exists> i < si . a' = a + of_nat (si - i - 1)}"
 
 text \<open>The set of addresses belonging to a region starting at address @{term "a::64 word"} of @{term si} bytes.\<close>
 
 definition region_overflow :: "'a word \<Rightarrow> nat \<Rightarrow> bool"
   where "region_overflow a si \<equiv> unat a + si \<ge> 2^LENGTH('a)"
 
 text \<open>An overflow occurs if the address plus the size is greater equal @{term "2^64"}\<close>
 
 definition enclosed :: "'a word \<Rightarrow> nat \<Rightarrow> 'a word \<Rightarrow> nat \<Rightarrow> bool"
   where "enclosed a' si' a si \<equiv> unat a + si < 2^LENGTH('a) \<and> unat a \<le> unat a' \<and> unat a' + si' \<le> unat a + si"
 
 text \<open>A region is enclosed in another if its @{const region_addresses} is a subset of the other.\<close>
 
 definition separate :: "'a word \<Rightarrow> nat \<Rightarrow> 'a word \<Rightarrow> nat \<Rightarrow> bool"
   where "separate a si a' si' \<equiv> si \<noteq>0 \<and> si' \<noteq> 0 \<and> region_addresses a si \<inter> region_addresses a' si' = {}"
 
 text \<open>A region is separate from another if they do not overlap.\<close>
 
 
 
 lemma region_addresses_iff: "a' \<in> region_addresses a si \<longleftrightarrow> unat (a' - a) < si"
   apply (auto simp add: region_addresses_def unsigned_of_nat)
    apply (metis diff_Suc_less le_less_trans less_imp_Suc_add take_bit_nat_less_eq_self zero_less_Suc)
-  by (smt (z3) add.commute add_Suc_right add_diff_cancel_left' diff_add_cancel less_add_Suc2 less_imp_Suc_add word_unat.Rep_inverse)
+  by (metis Suc_diff_Suc add.commute diff_add_cancel diff_diff_cancel diff_less less_imp_Suc_add order_less_imp_le word_unat.Rep_inverse zero_less_Suc)
 
 lemma notin_region_addresses:
   assumes "x \<notin> region_addresses a si"
   shows "unat x < unat a \<or> unat a + si \<le> unat x"
   by (metis assms add.commute less_diff_conv2 not_le_imp_less region_addresses_iff unat_sub_if')
 
 lemma notin_region_addresses_sub:
   assumes "x \<notin> region_addresses a si"
   shows "unat (x - a') < unat (a - a') \<or> unat (a - a') + si \<le> unat (x - a')"
   using assms notin_region_addresses region_addresses_iff by auto
 
 lemma region_addresses_eq_empty_iff: "region_addresses a si = {} \<longleftrightarrow> si = 0"
   by (metis region_addresses_iff add_diff_cancel_left' ex_in_conv neq0_conv not_less0 unsigned_0)
 
 lemma length_read_bytes:
   shows "length (read_bytes m a si) = si"
   by (induct si,auto)
 
 lemma nth_read_bytes:
 assumes "n < si"
 shows "read_bytes m a si ! n = m (a + of_nat (si - 1 - n))"
   using assms
   apply (induct si arbitrary: n,auto)
   subgoal for si n
     by(cases n,auto)
   done
 
 text \<open>Writing to memory occurs via function @{const override_on}.
       In case of enclosure, reading bytes from memory overridden on a set of region addresses can
       be simplified to reading bytes from the overwritten memory only.
       In case of separation, reading bytes from overridden memory can be simplified to reading
       from the original memory.\<close>
 
 lemma read_bytes_override_on_enclosed:
 assumes "offset' \<le> offset"
     and "si' \<le> si"
     and "unat offset + si' \<le> si + unat offset'"
   shows "read_bytes (override_on m m' (region_addresses (a - offset) si)) (a - offset') si' = read_bytes m' (a - offset') si'"
 proof-
   {
     fix i
     assume 1: "i < si'"
     let ?i = "(si + i + unat offset') - unat offset - si'"
 
     have "i + unat offset' < si' + unat offset"
       using 1 assms(1)
       by unat_arith
     hence 2: "si + i + unat offset' - (unat offset + si') < si"
       using diff_less[of "(si' + unat offset - i) - unat offset'" si] assms(3)
       by auto
     moreover
     have "of_nat (si' - Suc i) - offset' = of_nat (si - Suc ?i) - offset"
       using assms 1 2 by (auto simp add: of_nat_diff)
     ultimately
     have "\<exists> i' < si. of_nat (si' - Suc i) - offset' = of_nat (si - Suc i') - offset"
       by auto
   }
   note 1 = this
   show ?thesis
     apply (rule nth_equalityI)
     using 1
     by (auto simp add: length_read_bytes nth_read_bytes override_on_def region_addresses_def)
 qed
 
 lemmas read_bytes_override_on = read_bytes_override_on_enclosed[where offset=0 and offset'=0,simplified]
 
 lemma read_bytes_override_on_enclosed_plus:
   assumes "unat offset + si' \<le> si"
       and "si \<le> 2^LENGTH('a)"
   shows "read_bytes (override_on m m' (region_addresses a si)) (offset+a) si' = read_bytes m' (offset+a) si'"
 proof-
   {
     fix i
     have "i < si' \<Longrightarrow> \<exists> i' < si. offset + (of_nat (si' - Suc i)::'a word) = of_nat (si - Suc i')"
       apply (rule exI[of _"si - si' + i - unat offset"])
       using assms by (auto simp add: of_nat_diff)
   }
   note 1 = this
   show ?thesis
     apply (rule nth_equalityI)
     using assms 1
     by (auto simp add: override_on_def length_read_bytes nth_read_bytes region_addresses_def)
 qed
 
 
 lemma read_bytes_override_on_separate:
 assumes "separate a si a' si'"
   shows "read_bytes (override_on m m' (region_addresses a si)) a' si' = read_bytes m a' si'"
   apply (rule nth_equalityI)
   using assms
   by (auto simp add: length_read_bytes nth_read_bytes override_on_def separate_def region_addresses_def)
 
 
 text\<open>Bytes are are written to memory one-by-one, then read by @{const read_bytes} producing a list of bytes.
     That list is concatenated again using @{const word_rcat}. Writing @{term si} bytes of word @{term w} into
     memory, reading the byte-list and concatenating again produces @{term si} bytes of the original word.\<close>
 
 
 lemma word_rcat_read_bytes_enclosed:
   fixes w :: "'b::len word"
   assumes "LENGTH('b) \<le> 2^LENGTH('a)"
     and "unat offset + si \<le> 2^LENGTH('a)"
   shows "word_rcat (read_bytes (\<lambda>a'. take_byte (unat (a' - a)) w) (a + offset) si) = \<langle>unat offset * 8,(unat offset + si) * 8\<rangle>w"
   apply (rule word_eqI)
   using assms
   apply (auto simp add: test_bit_rcat word_size length_read_bytes rev_nth nth_read_bytes unat_of_nat nth_takebyte unat_word_ariths )
     apply (auto simp add: take_byte_def nth_ucast nth_takebits take_bit_eq_mod split: if_split_asm)[1]
    apply (auto simp add: nth_takebits split: if_split_asm)[1]
   apply (auto simp add: take_byte_def nth_ucast nth_takebits split: if_split_asm)[1]
   by (auto simp add: rev_nth length_read_bytes take_byte_def nth_ucast nth_takebits nth_read_bytes unat_word_ariths unat_of_nat take_bit_eq_mod split: if_split_asm)
 
 lemmas word_rcat_read_bytes = word_rcat_read_bytes_enclosed[where offset=0,simplified]
 
 
 
 text \<open>The following theorems allow reasoning over enclosure and separation, for example as linear arithmetic.\<close>
 
 lemma enclosed_spec:
   assumes enclosed: "enclosed a' si' a si"
       and x_in: "x \<in> region_addresses a' si'"
     shows "x \<in> region_addresses a si"
 proof -
   from x_in have "unat (x - a') < si'"
     using region_addresses_iff by blast
   with enclosed have "unat (x - a) < si"
     unfolding enclosed_def by (auto simp add: unat_sub_if' split: if_split_asm)
   then show ?thesis
     using region_addresses_iff by blast
 qed
 
 lemma address_in_enclosed_region_as_linarith:
   assumes "enclosed a' si' a si"
       and "x \<in> region_addresses a' si'"
     shows "a \<le> x \<and> a' \<le> x \<and> x < a' + of_nat si' \<and> x < a + of_nat si"
   using assms
   by (auto simp add: enclosed_def region_addresses_def word_le_nat_alt word_less_nat_alt unat_of_nat unat_word_ariths unat_sub_if' take_bit_eq_mod)
 
 
 lemma address_of_enclosed_region_ge:
   assumes "enclosed a' si' a si"
     shows "a' \<ge> a"
   using assms word_le_nat_alt
   by (auto simp add: enclosed_def)
 
 lemma address_in_enclosed_region:
   assumes "enclosed a' si' a si"
       and "x \<in> region_addresses a' si'"
     shows "unat (x - a) \<ge> unat (a' - a) \<and> unat (a' - a) + si' > unat (x - a) \<and> unat (x - a) < si"
-  by (smt (z3) address_in_enclosed_region_as_linarith add_diff_cancel_left' address_of_enclosed_region_ge assms(1) assms(2) diff_diff_add enclosed_spec le_iff_add nat_add_left_cancel_less region_addresses_iff unat_sub_if' word_le_minus_mono_left word_unat.Rep_inverse word_unat_less_le)
+  by (smt (verit, ccfv_threshold) Memory.enclosed_def Memory.region_addresses_iff
+      address_in_enclosed_region_as_linarith assms(1) assms(2) diff_diff_add
+      le_add_diff_inverse mcs(4) nat_add_left_cancel_less no_ulen_sub of_nat_add
+      un_ui_le unat_mono unat_of_nat_eq unat_sub unsigned_less word_sub_le_iff)
 
 lemma enclosed_minus_minus:
   fixes a :: "'a word"
   assumes "offset \<ge> offset'"
       and "unat offset - si \<le> unat offset' - si'"
       and "unat offset' \<ge> si'"
       and "unat offset \<ge> si"
       and "a \<ge> offset"
     shows "enclosed (a - offset') si' (a - offset) si"
 proof-
   have "unat offset' \<le> unat a"
     using assms(1,5)
     by unat_arith
   thus ?thesis
     using assms
     apply (auto simp add: enclosed_def unat_sub_if_size word_size)
     apply unat_arith
     using diff_le_mono2[of "unat offset - si" "unat offset' - si'" "unat a"]
     apply (auto simp add: enclosed_def unat_sub_if_size word_size)
      by unat_arith+
 qed
 
 lemma enclosed_plus:
   fixes a :: "'a word"
   assumes "si' < si"
       and "unat a + si < 2^LENGTH('a)"
     shows "enclosed a si' a si"
   using assms
   by (auto simp add: enclosed_def)
 
 lemma separate_symm: "separate a si a' si' = separate a' si' a si"
   by (metis inf.commute separate_def)
 
 lemma separate_iff: "separate a si a' si' \<longleftrightarrow> si > 0 \<and> si' > 0 \<and> unat (a' - a) \<ge> si \<and> unat (a - a') \<ge> si'"
 proof
   assume assm: "separate a si a' si'"
   have "unat (a' - a) \<ge> si" if "separate a si a' si'" for a si a' si'
   proof (rule ccontr)
     assume "\<not> unat (a' - a) \<ge> si"
     then have "a' \<in> region_addresses a si"
       by (simp add: region_addresses_iff)
     moreover from that have "a' \<in> region_addresses a' si'"
       using region_addresses_iff separate_def by auto
     ultimately have "\<not>separate a si a' si'"
       by (meson disjoint_iff separate_def)
     with that show False
       by blast
   qed
   with assm have "unat (a' - a) \<ge> si" and "unat (a - a') \<ge> si'"
     using separate_symm by auto
   with assm show "si > 0 \<and> si' > 0 \<and> unat (a' - a) \<ge> si \<and> unat (a - a') \<ge> si'"
     using separate_def by auto
 next
   assume assm: "si > 0 \<and> si' > 0 \<and> unat (a' - a) \<ge> si \<and> unat (a - a') \<ge> si'"
   then have "unat (x - a') \<ge> si'" if "unat (x - a) < si" for x
     using that apply (auto simp add: unat_sub_if' split: if_split_asm)
      apply (meson Nat.le_diff_conv2 add_increasing le_less_trans less_imp_le_nat unsigned_greater_eq unsigned_less)
-    by (smt (z3) Nat.le_diff_conv2 add_leD2 le_less_trans linorder_not_less nat_le_linear unat_lt2p)
+    by (smt (verit) Nat.le_diff_conv2 add_leD2 le_less_trans linorder_not_less nat_le_linear unat_lt2p)
   then have "region_addresses a si \<inter> region_addresses a' si' = {}"
     by (simp add: region_addresses_iff disjoint_iff leD)
   with assm show "separate a si a' si'"
     by (simp add: separate_def)
 qed
 
 lemma separate_as_linarith:
 assumes "\<not>region_overflow a si"
     and "\<not>region_overflow a' si'"
   shows "separate a si a' si' \<longleftrightarrow> 0 < si \<and> 0 < si' \<and> (a + of_nat si \<le> a' \<or> a' + of_nat si' \<le> a)"
     (is "?lhs \<longleftrightarrow> ?rhs")
 proof
   assume ?lhs then show ?rhs
    by (meson separate_iff le_less le_plus not_le_imp_less word_of_nat_le)
 next
   have *: "separate a si a' si'"
     if "si > 0" and "si' > 0" and "a + of_nat si \<le> a'"
       and "\<not>region_overflow a si" and "\<not>region_overflow a' si'"
     for a si a' si'
   proof -
     from that have "unat a + si < 2^LENGTH('a)" and "unat a' + si' < 2^LENGTH('a)"
       by (meson not_le region_overflow_def)+
     have "x < a + of_nat si" if "x \<in> region_addresses a si" for x
-      by (smt (z3) Abs_fnat_hom_add \<open>unat a + si < 2 ^ LENGTH('a)\<close> add.commute dual_order.trans le_add1 less_diff_conv2 not_less region_addresses_iff that unat_of_nat_len unat_sub_if' word_less_iff_unsigned word_unat.Rep_inverse)
+      by (smt (verit) Abs_fnat_hom_add \<open>unat a + si < 2 ^ LENGTH('a)\<close> add.commute dual_order.trans le_add1 less_diff_conv2 not_less region_addresses_iff that unat_of_nat_len unat_sub_if' word_less_iff_unsigned word_unat.Rep_inverse)
     moreover have "x \<ge> a'" if "x \<in> region_addresses a' si'" for x
       using address_in_enclosed_region_as_linarith enclosed_def \<open>unat a' + si' < 2 ^ LENGTH('a)\<close> that by blast
     ultimately show ?thesis
       using separate_def that by fastforce
   qed
   assume ?rhs then show ?lhs
     by (meson "*" assms separate_symm)
 qed
 
 text \<open>Compute separation in case the addresses and sizes are immediate values.\<close>
 lemmas separate_as_linarith_numeral [simp] =
   separate_as_linarith [of "numeral a::'a word" "numeral si" "numeral a'::'a word" "numeral si'"] for a si a' si'
 lemmas separate_as_linarith_numeral_1 [simp] =
   separate_as_linarith [of "numeral a::'a word" "numeral si" "numeral a'::'a word" "Suc 0"] for a si a'
 lemmas separate_as_linarith_numeral1_ [simp] =
   separate_as_linarith [of "numeral a::'a word" "Suc 0" "numeral a'::'a word" "numeral si'"] for a a' si'
 lemmas separate_as_linarith_numeral11 [simp] =
   separate_as_linarith [of "numeral a::'a word" "Suc 0" "numeral a'::'a word" "Suc 0"] for a a'
 lemmas region_overflow_numeral[simp] =
   region_overflow_def [of "numeral a::'a word" "numeral si"] for a si
 lemmas region_overflow_numeral1[simp] =
   region_overflow_def [of "numeral a::'a word" "Suc 0"] for a
 
 
 lemma separate_plus_none:
   assumes "si' \<le> unat offset"
       and "0 < si"
       and "0 < si'"
       and "unat offset + si \<le> 2^LENGTH('a)"
     shows "separate (offset + a) si a si'"
   using assms apply (auto simp add: separate_iff)
-  by (smt (z3) Nat.diff_diff_right add.commute add_leD1 diff_0 diff_is_0_eq diff_zero not_gr_zero unat_sub_if' unsigned_0)
+  by (smt (verit) Nat.diff_diff_right add.commute add_leD1 diff_0 diff_is_0_eq diff_zero not_gr_zero unat_sub_if' unsigned_0)
 
 lemmas unat_minus = unat_sub_if'[of 0,simplified]
 
 lemma separate_minus_minus':
   assumes "si \<noteq> 0"
       and "si' \<noteq> 0"
       and "unat offset \<ge> si"
       and "unat offset' \<ge> si'"
       and "unat offset - si \<ge> unat offset'"
     shows "separate (a - offset) si (a - offset') si'"
   using assms apply (auto simp add: separate_iff)
    apply (metis Nat.le_diff_conv2 add.commute add_leD2 unat_sub_if')
-  by (smt (z3) add.commute add_diff_cancel_right' diff_add_cancel diff_le_self diff_less less_le_trans nat_le_linear not_le unat_sub_if')
+  by (smt (verit) add.commute add_diff_cancel_right' diff_add_cancel diff_le_self diff_less less_le_trans nat_le_linear not_le unat_sub_if')
 
 lemma separate_minus_minus:
   assumes "si \<noteq> 0"
       and "si' \<noteq> 0"
       and "unat offset \<ge> si"
       and "unat offset' \<ge> si'"
       and "unat offset - si \<ge> unat offset' \<or> unat offset' - si' \<ge> unat offset"
     shows "separate (a - offset) si (a - offset') si'"
   by (meson assms separate_minus_minus' separate_symm)
 
 lemma separate_minus_none:
   assumes "si \<noteq> 0"
       and "si' \<noteq> 0"
       and "unat offset \<ge> si"
       and "si' \<le> 2^LENGTH('a) - unat offset"
     shows "separate (a - offset) si a si'"
 proof -
   have "0 < si" and "0 < si'"
     using assms(1,2) by blast+
   moreover have "\<not> offset \<le> 0"
     using assms(1) assms(3) by fastforce
   ultimately show ?thesis
-    by (smt (z3) add_diff_cancel_left' assms(3,4) diff_diff_eq2 diff_zero le_add_diff_inverse less_or_eq_imp_le separate_iff unat_sub_if' unsigned_0 unsigned_less word_less_eq_iff_unsigned)
+    by (simp add: assms(3) assms(4) local.unat_minus separate_iff unsigned_eq_0_iff)
 qed
 
 
 text \<open>The following theorems are used during symbolic execution to determine whether two regions are separate.\<close>
 
 lemmas separate_simps = separate_plus_none separate_minus_none separate_minus_minus
 
 end
 end
\ No newline at end of file
diff --git a/thys/X86_Semantics/ROOT b/thys/X86_Semantics/ROOT
--- a/thys/X86_Semantics/ROOT
+++ b/thys/X86_Semantics/ROOT
@@ -1,17 +1,13 @@
 chapter AFP
 
 session "X86_Semantics" = HOL +
-
   options [timeout = 1800]
   sessions
-      "HOL-Eisbach"
-      Word_Lib
-
+    "HOL-Eisbach"
+    Word_Lib
   theories
     Examples
     Example_WC
-
   document_files
     "root.bib"
     "root.tex"
-