diff --git a/thys/Graph_Saturation/GraphRewriting.thy b/thys/Graph_Saturation/GraphRewriting.thy
--- a/thys/Graph_Saturation/GraphRewriting.thy
+++ b/thys/Graph_Saturation/GraphRewriting.thy
@@ -1,552 +1,552 @@
 section \<open>Graph rewriting and saturation\<close>
 text \<open>Here we describe graph rewriting, again without connecting it to semantics.\<close>
 theory GraphRewriting
   imports RulesAndChains 
     "HOL-Library.Infinite_Set"
 begin
 
 (* Algorithm 1 on page 16 *)
 text \<open>To describe Algorithm 1, we give a single step instead of the recursive call.
 This allows us to reason about its effect without dealing with non-termination.
 We define a worklist, saying what work can be done.
 A valid selection needs to be made in order to ensure fairness.
 To do a step, we define the function extend, and use it in @{term make_step}.
 A function that always makes a valid selection is used in this step. \<close>
 
 abbreviation graph_of where
   "graph_of \<equiv> \<lambda> X. LG (snd X) {0..<fst X}"
 
 definition nextMax :: "nat set \<Rightarrow> nat"
   where
   "nextMax x \<equiv> if x = {} then 0 else Suc (Max x)"
 
 lemma nextMax_max[intro]:
   assumes "finite x" "v \<in> x"
   shows "v < nextMax x" "v \<le> nextMax x"
   using Max.coboundedI[OF assms] assms(2) unfolding nextMax_def by auto
 
 definition worklist :: "nat \<times> ('a \<times> nat \<times> nat) set
            \<Rightarrow> (('a, 'b) labeled_graph \<times> ('a, 'b) labeled_graph) set
               \<Rightarrow> (nat \<times> ('a, 'b) Graph_PreRule \<times> ('b \<times> nat) set) set" where
 "worklist G Rs \<equiv> let G = graph_of G
   in {(N,R,f). R\<in> Rs \<and> graph_homomorphism (fst R) G f \<and> N = nextMax (Range f)
                  \<and> \<not> extensible R G f }"
 
 definition valid_selection where
 "valid_selection Rs G R f \<equiv>
   let wl = worklist G Rs in
     (nextMax (Range f), R,f) \<in> wl \<and>
     (\<forall> (N,_) \<in> wl. N \<ge> nextMax (Range f)) \<and>
     graph_rule R"
 
 lemma valid_selection_exists:
   assumes "worklist G Rs \<noteq> {}"
           "set_of_graph_rules Rs"
   shows "\<exists>L R f. valid_selection Rs G R f"
 proof -
   define wl where "wl = worklist G Rs" hence wl_ne:"wl \<noteq> {}" using assms(1) by auto
   let ?N = "LEAST N. N \<in> Domain wl"
   from wl_ne have "\<exists> N. N \<in> Domain wl" by auto
   with LeastI2 have "?N \<in> Domain wl" by metis
   then obtain L R f where NLRf:"(?N,(L,R),f)\<in>wl" by auto
   hence N_def:"?N = nextMax (Range f)"
     and in_Rs: "(L,R) \<in> Rs" unfolding wl_def worklist_def Let_def by auto
   from Least_le wl_ne Domain.intros case_prodI2 
   have min:"(\<forall> (N',_) \<in> wl. N' \<ge> ?N)" by (metis (no_types, lifting))
   from in_Rs have "finite_graph R" "subgraph L R"
     using assms(2)[unfolded set_of_graph_rules_def] by auto
   with min NLRf N_def show ?thesis unfolding wl_def[symmetric] valid_selection_def by auto
 qed
 
 definition valid_selector where
 "valid_selector Rs selector \<equiv> \<forall> G.
    (worklist G Rs \<noteq> {} \<longrightarrow> (\<exists> (R,f)\<in>UNIV. selector G = Some (R,f)
                                \<and> valid_selection Rs G R f)) \<and>
    (worklist G Rs = {} \<longrightarrow> selector G = None)"
 
 lemma valid_selectorD[dest]:
   assumes "valid_selector Rs selector"
   shows "worklist G Rs = {} \<longleftrightarrow> selector G = None"
         "selector G = Some (R,f) \<Longrightarrow> valid_selection Rs G R f"
   using assms[unfolded valid_selector_def,rule_format,of G]
   by (cases "worklist G Rs = {}",auto)
 
 text \<open>The following gives a valid selector.
       This selector is not useful as concrete implementation, because it used the choice operation.\<close>
 definition non_constructive_selector where
 "non_constructive_selector Rs G \<equiv> let wl = worklist G Rs in
    if wl = {} then None else Some (SOME (R,f). valid_selection Rs G R f) "
 
 lemma non_constructive_selector:
   assumes "set_of_graph_rules Rs"
   shows "valid_selector Rs (non_constructive_selector Rs)"
   unfolding valid_selector_def proof((clarify,standard;clarify),goal_cases)
   case (1 n E)
   let ?x = "(SOME (R, f). valid_selection Rs (n, E) R f)"
   from valid_selection_exists[OF 1 assms]
   have "\<exists> R f. valid_selection Rs (n, E) R f" by auto
   hence "\<exists> x. valid_selection Rs (n, E) (fst x) (snd x)"
     by auto
   from this prod.case_eq_if tfl_some
   have "\<not> valid_selection Rs (n, E) (fst ?x) (snd ?x) \<Longrightarrow> False"
     by (metis (mono_tags, lifting))
   thus ?case unfolding non_constructive_selector_def Let_def using 1 by (auto simp:prod_eq_iff)
 qed (auto simp:non_constructive_selector_def)
 
 
 text \<open>The following is used to make a weak pushout step.
       In the paper, we aren't too specific on how this should be done. Here we are.
       We work on natural numbers in order to be able to pick fresh elements easily. \<close>
 definition extend ::
     "nat \<Rightarrow> ('b, 'a::linorder) Graph_PreRule  \<Rightarrow> ('a \<times> nat) set \<Rightarrow> ('a \<times> nat) set" where
 "extend n R f \<equiv> f \<union> 
    (let V_new = sorted_list_of_set (vertices (snd R) - vertices (fst R))
     in set (zip V_new [n..<(n+length V_new)]))"
 
 lemma nextMax_set[simp]:
   assumes "sorted xs"
   shows "nextMax (set xs) = (if xs = Nil then 0 else Suc (last xs))"
   using assms
 proof(induct xs)
   case Nil show ?case unfolding nextMax_def by auto
 next
   case (Cons a list)
   hence "list \<noteq> [] \<Longrightarrow> fold max list a = last list"
     using list_sorted_max by (metis last.simps)
   thus ?case unfolding nextMax_def Max.set_eq_fold by auto
 qed
 
 lemma nextMax_Un_eq[simp]:
 "finite x \<Longrightarrow> finite y \<Longrightarrow> nextMax (x \<union> y) = max (nextMax x) (nextMax y)"
   unfolding nextMax_def using Max_Un by auto
 
 lemma extend: (* extensible into the new graph *)
   assumes "graph_homomorphism (fst R) (LG E {0..<n}) f" "graph_rule R"
   defines "g \<equiv> extend n R f"
   defines "G' \<equiv> LG ((on_triple g `` (edges (snd R))) \<union> E) {0..<max n (nextMax (Range g))}"
   shows "graph_homomorphism (snd R) G' g" "agree_on (fst R) f g" "f \<subseteq> g"
         "subgraph (LG E {0..<n}) G'"
         "weak_universal (t:: 'x itself) R (LG E {0..<n}) G' f g"
 proof -
   have ln:"length x = length [n..<n + length x]" for x::"'b list" by auto
   let ?R_L = "vertices (snd R) - vertices (fst R)"
   from assms
   have "graph_rule (fst R,snd R)" and fin_R:"finite (vertices (snd R))"
     and subsLR:"vertices (fst R) \<subseteq> vertices (snd R)" and gr_R:"graph (snd R)"
     unfolding subgraph_def graph_union_iff
     by auto
   hence fin_R_L[simp]:"finite ?R_L"
      and fin_L:"finite (vertices (fst R))"
      using finite_subset by auto
   from assms have f_dom:"Domain f = vertices (fst R)"
     and f_uni:"univalent f" unfolding graph_homomorphism_def by auto
   from assms[unfolded graph_homomorphism_def]
   have "f `` vertices (fst R) \<subseteq> vertices (LG E {0..<n})" by blast
   hence f_ran:"Range f \<subseteq> {0..<n}" using f_dom by auto
   let ?g = "(let V_new = sorted_list_of_set ?R_L
               in set (zip V_new [n..<n + length V_new]))" (* new part of g *)
   have fin_g':"finite ?g" "finite (Range ?g)" unfolding Let_def by auto
   have "finite (Domain f)" "univalent f" using assms(1) fin_L
     unfolding graph_homomorphism_def by auto
   hence fin_f:"finite (Range f)" unfolding Range_snd by auto
   hence fin_g:"finite (Range g)" unfolding extend_def g_def Let_def Range_Un_eq by auto
   have nextMax_f:"nextMax (Range f) \<le> n"
     using f_ran Max_in[OF fin_f] by (simp add:nextMax_def Suc_leI subset_eq)
   
   have "x \<in> Domain ?g \<Longrightarrow> x \<notin> Domain f" for x unfolding f_dom Let_def by auto
-  hence g_not_f:"(x,y) \<in> ?g \<Longrightarrow> (x,z) \<notin> f" for x y z by auto
+  hence g_not_f:"(x,y) \<in> ?g \<Longrightarrow> (x,z) \<notin> f" for x y z by blast
   have uni_g':"univalent ?g" "univalent (converse ?g)" unfolding Let_def by auto
   with f_uni have uni_g:"univalent g" by (auto simp:g_def extend_def g_not_f)
   from fin_g have "(a,b) \<in> g \<Longrightarrow> b < Suc (Max (Range g))" for a b
     unfolding less_Suc_eq_le by (rule Max.coboundedI) force
   hence "(a,b) \<in> g \<Longrightarrow> b < nextMax (Range g)" for a b
     unfolding nextMax_def by (cases "Range g = {}",auto)
   hence in_g:"(a,b) \<in> g \<Longrightarrow> b < max n (nextMax (Range g))" for a b by fastforce
   let ?G = "LG E {0..<n}"
   have gr_G:"graph ?G" using assms(1) unfolding graph_homomorphism_def by blast
   hence "(a, aa, b) \<in> E \<Longrightarrow> b < max n c" "(a, aa, b) \<in> E \<Longrightarrow> aa < max n c"
     for a aa b c by fastforce+
   hence gr_G':"graph G'" unfolding G'_def restrict_def using in_g by auto
   show "subgraph (LG E {0..<n}) G'"
     unfolding subgraph_def2[OF gr_G gr_G'] unfolding G'_def by auto
   have g_dom:"vertices (snd R) = Domain g" using subsLR
     unfolding g_def extend_def Domain_Un_eq f_dom by (auto simp:Let_def)
   show "graph_homomorphism (snd R) G' g"
     by (intro graph_homomorphismI[OF g_dom _ uni_g _ gr_R gr_G'])
        (auto simp:G'_def intro:in_g)
   show "f \<subseteq> g" by (auto simp:g_def extend_def)
   thus "agree_on (fst R) f g" using f_dom uni_g agree_on_subset equalityE by metis
   show "weak_universal t R ?G G' f g" proof fix a:: "('b \<times> 'x) set" fix b G
     assume a:"graph_homomorphism (snd R) G a"
              "graph_homomorphism ?G G b" "f O b \<subseteq> a"
     hence univ_b:"univalent b" and univ_a:"univalent a"
       and rng_b:"Range b \<subseteq> vertices G" and rng_a:"Range a \<subseteq> vertices G"
       and ep_b:"edge_preserving b (edges (LG E {0..<n})) (edges G)"
       and ep_a:"edge_preserving a (edges (snd R)) (edges G)"
       unfolding graph_homomorphism_def prod.sel labeled_graph.sel by blast+
     from a have dom_b:"Domain b = {0..<n}"
       and dom_a:"Domain a = vertices (snd R)" and v6: "graph G"
       unfolding graph_homomorphism_def prod.sel labeled_graph.sel by auto
 
     have help_dom_b:"(y, z) \<in> b \<Longrightarrow> n \<le> y \<Longrightarrow> False" for y z using dom_b
       by (metis Domain.DomainI atLeastLessThan_iff not_less)
     have disj_doms:"Domain b \<inter> Domain (?g\<inverse> O a) = {}" using help_dom_b
       unfolding Let_def by (auto dest!:set_zip_leftD)
 
     have "max n (nextMax (Range ?g)) = n + length (sorted_list_of_set ?R_L)" (is "_ = ?len")
       unfolding Let_def Range_snd set_map[symmetric] map_snd_zip[OF ln] nextMax_set[OF sorted_upt]
-      by fastforce
+      by (fastforce simp del: length_sorted_list_of_set)
     hence n_eq:"?len = max n (nextMax (Range g))"
       unfolding Range_snd[symmetric] g_def extend_def Range_Un_eq
                 nextMax_Un_eq[OF fin_f fin_g'(2)] max.assoc[symmetric] max_absorb1[OF nextMax_f]
       by auto
 
     let ?h = "b \<union> ?g\<inverse> O a"
 
     have dg:"Domain (?g\<inverse>) = {n..<max n (nextMax (Range g))}"
       unfolding Let_def Domain_converse Range_set_zip[OF ln] atLeastLessThan_upt
       unfolding Range_snd n_eq ..
     have "?g `` Domain a = ?g `` (?R_L \<union> vertices (fst R))"
       using dom_a subsLR by auto
-    also have "\<dots> = ?g `` ?R_L \<union> ?g `` vertices (fst R)" by auto
+    also have "\<dots> = ?g `` ?R_L \<union> ?g `` vertices (fst R)" by blast
     also have "?g `` vertices (fst R) = {}" apply(rule Image_outside_Domain)
       unfolding Let_def Domain_set_zip[OF ln] by auto
     also have "?g `` ?R_L = Range ?g" apply(rule Image_Domain)
       unfolding Let_def Domain_set_zip[OF ln] by auto
     finally have dg2:"?g `` Domain a = {n..<max n (nextMax (Range g))}"
       unfolding Let_def Range_set_zip[OF ln] set_sorted_list_of_set[OF fin_R_L] 
       unfolding n_eq set_upt by auto
     have "Domain (?g\<inverse> O a) = {n..<max n (nextMax (Range g))}"
       unfolding Domain_id_on converse_converse dg dg2 by auto
     hence v1: "vertices G' = Domain ?h" unfolding G'_def Domain_Un_eq dom_b by auto
     have "b `` vertices G' \<subseteq> vertices G" "(?g\<inverse> O a) `` vertices G' \<subseteq> vertices G"
       using rng_a rng_b by auto
     hence v2: "?h `` vertices G' \<subseteq> vertices G" by blast
     have v3: "univalent ?h"
       using disj_doms univalent_union[OF univ_b univalent_composes[OF uni_g'(2) univ_a]] by blast
     (* showing edge preservation *)
     { fix l x y x' y' assume a2:"(l,x,y) \<in> edges G'" "(x,x') \<in> ?h" "(y,y') \<in> ?h"
       have "(l,x',y') \<in> edges G" proof(cases "(l,x,y) \<in> edges ?G")
         case True
         with gr_G[THEN restrictD]
         have "x \<in> Domain b" "y \<in> Domain b" unfolding dom_b by auto
         hence "x \<notin> Domain (converse ?g O a)" "y \<notin> Domain (converse ?g O a)"
           using disj_doms by blast+
         hence "(x,x') \<in> b" "(y,y') \<in> b" using a2 by auto
         with ep_b True show ?thesis unfolding edge_preserving by auto
       next
         have "g O ?h = f O b \<union> ?g O b \<union> ((f O ?g\<inverse>) O a \<union> (?g O ?g\<inverse>) O a)"
           unfolding g_def extend_def by blast
         also have "(?g O ?g\<inverse>) = Id_on ?R_L"
           unfolding univalent_O_converse[OF uni_g'(2)] unfolding Let_def by auto
         also have "(f O ?g\<inverse>) = {}" using f_ran unfolding Let_def by (auto dest!:set_zip_leftD)
         also have "?g O b = {}" using help_dom_b unfolding Let_def by (auto dest!:set_zip_rightD)
         finally have gOh:"g O ?h \<subseteq> a" using a(3) by blast
         case False
         hence "(l,x,y) \<in> on_triple g `` edges (snd R)" using a2(1) unfolding G'_def by auto
         then obtain r_x r_y
           where r:"(l,r_x,r_y) \<in> edges (snd R)" "(r_x,x) \<in> g" "(r_y,y) \<in> g" by auto
         hence "(r_x,x') \<in> a" "(r_y,y') \<in> a" using gOh a2(2,3) by auto
         hence "(l,x',y') \<in> on_triple a `` edges (snd R)" using r(1) unfolding on_triple_def by auto
         thus ?thesis using ep_a unfolding edge_preserving by auto
       qed
     }
     hence v4: "edge_preserving ?h (edges G') (edges G)" by auto
     have "graph_homomorphism G' G ?h" by(fact graph_homomorphismI[OF v1 v2 v3 v4 gr_G' v6])
     thus "\<exists>h. graph_homomorphism G' G h \<and> b \<subseteq> h" by auto
   qed
 qed
 
 text \<open>Showing that the extend function indeed creates a valid pushout.\<close>
 lemma selector_pushout:
   assumes "valid_selector Rs selector" "selector G'' = Some (R,f)"
   defines "G \<equiv> graph_of G''"
   assumes "graph G"
   defines "g \<equiv> extend (fst G'') R f"
   defines "G' \<equiv> LG (on_triple g `` edges (snd R) \<union> (snd G'')) {0..<max (fst G'') (nextMax (Range g))}"
   shows "pushout_step (t:: 'x itself) R G G'"
 proof -
   have "valid_selection Rs G'' R f" using assms by(cases "selector G''",auto)
   hence igh:"graph_homomorphism (fst R) G f" "graph_rule R"
     unfolding valid_selection_def worklist_def G_def Let_def by auto
   have "subgraph G G'"
        "graph_homomorphism (fst R) G f"
        "graph_homomorphism (snd R) G' g"
        "f \<subseteq> g"
        "weak_universal t R G G' f g"
     using extend[OF igh[unfolded G_def],folded g_def,folded G'_def,folded G_def] igh(1)
     by auto
   thus ?thesis unfolding pushout_step_def by auto
 qed
 
 text \<open>Making a single step in Algorithm 1.
   A prerequisite is that its first argument is a @{term valid_selector}.\<close>
 
 definition make_step where
 "make_step selector S \<equiv>
    case selector S of
      None \<Rightarrow> S |
      Some (R,f) \<Rightarrow> (let g = extend (fst S) R f in
          (max (fst S) (nextMax (Range g)), (on_triple g `` (edges (snd R))) \<union> (snd S)))"
 
 lemma WPC_through_make_step:
   assumes "set_of_graph_rules Rs" "graph (graph_of (X 0))"
      and makestep: "\<forall> i. X (Suc i) = make_step selector (X i)"
      and selector: "valid_selector Rs selector"
   shows "Simple_WPC t Rs (\<lambda> i. graph_of (X i))" "chain (\<lambda> i. graph_of (X i))"
 proof
   note ms = makestep[unfolded make_step_def,rule_format]
   have gr:"graph (graph_of (X i))" for i proof(induct i)
     case (Suc i)
     then show ?case proof(cases "selector (X i)")
       case None
       then show ?thesis using ms Suc by auto
     next
       case (Some a)
       then obtain R f where Some:"selector (X i) = Some (R,f)" by fastforce
       then show ?thesis using ms[of i,unfolded Some Let_def]
         selector_pushout[OF selector Some Suc,of t
                         ,unfolded pushout_step_def subgraph_def]
         by auto
     qed
   qed (fact assms)
   show "chain (\<lambda> i. graph_of (X i))" unfolding chain_def
   proof(clarify) fix i
     show "subgraph (graph_of (X i)) (graph_of (X (i + 1)))"
     proof(cases "selector (X i)")
       case None
       then show ?thesis using ms gr by (auto intro!:graph_homomorphismI)
     next
       case Some
       then obtain R f where Some:"selector (X i) = Some (R,f)" by fastforce
       then show ?thesis using ms selector_pushout[OF selector Some gr,of t]
       unfolding pushout_step_def Let_def by simp
     qed
   qed
   show "graph_of (X i) = graph_of (X (Suc i)) \<or>
          (\<exists>R\<in>Rs. pushout_step t R (graph_of (X i)) (graph_of (X (Suc i))))" for i
   proof(cases "selector (X i)")
     case None thus ?thesis using ms by auto
   next
     case Some
     then obtain R f where Some:"selector (X i) = Some (R,f)" by fastforce
     hence "R \<in> Rs" 
       using valid_selectorD(2)[OF selector,unfolded valid_selection_def worklist_def Let_def]
       by(cases R,blast)
     then show ?thesis using ms[of i,unfolded Some Let_def] selector_pushout[OF selector Some gr]
       unfolding make_step_def by auto
   qed
 qed (fact assms)+
 
 lemma N_occurs_finitely_often:
   assumes "finite Rs" "set_of_graph_rules Rs" "graph (graph_of (X 0))"
       and makestep: "\<And> i. X (Suc i) = make_step selector (X i)"
       and selector: "valid_selector Rs selector"
     shows "finite {(R,f). \<exists> i. R\<in> Rs \<and> graph_homomorphism (fst R) (graph_of (X i)) f
                         \<and> nextMax (Range f) \<le> N}" (is "finite {(R,f).?P R f}")
 proof -
   have prod_eq : "(\<forall> x \<in> {(x, y). A x y}. B x) \<longleftrightarrow> (\<forall> x. A (fst x) (snd x) \<longrightarrow> B x)"
      "(x \<in> {(x, y). A x y}) \<longleftrightarrow> (A (fst x) (snd x))"
     for A B x by auto
   let ?S = "{(R,f).?P R f}"
   let "?Q R f" = "Domain f = vertices (fst (R::('a, 'b) Graph_PreRule)) \<and> univalent f \<and> nextMax (Range f) \<le> N"
   have seteq:"(\<Union>R\<in>Rs. {(R', f). R' = R \<and> ?Q R f}) = {(R,f). R \<in> Rs \<and> ?Q R f}" by auto
   have "\<forall> R \<in> Rs. finite {(R',f). R' = R \<and> ?Q R f}"
   proof fix R assume "R \<in> Rs"
     hence fin:"finite (vertices (fst R))" using assms by auto
     hence fin2:"finite (Pow (vertices (fst R) \<times> {0..N}))" by auto
     have fin:"Domain x = vertices (fst R) \<Longrightarrow> univalent x \<Longrightarrow> finite (snd ` x)"
       for x:: "('b \<times> nat) set" using fin univalent_finite[of x] by simp
     hence "Domain f = vertices (fst R) \<Longrightarrow>
       univalent f \<Longrightarrow> (a,b) \<in> f \<Longrightarrow> nextMax (Range f) \<le> N \<Longrightarrow> b \<le> N" for f a b
       unfolding Range_snd using image_eqI nextMax_max(2) snd_conv order.trans by metis
     hence sub:"{f. ?Q R f} \<subseteq> Pow (vertices (fst R) \<times> {0..N})"
       using nextMax_max[OF fin] by (auto simp:Range_snd image_def)
     from finite_subset[OF sub fin2] show "finite {(R',f). R' = R \<and> ?Q R f}" by auto
   qed
   from this[folded finite_UN[OF assms(1)],unfolded seteq]
   have fin:"finite {(R,f). R \<in> Rs \<and> ?Q R f}".
   have "?P R f \<Longrightarrow> R \<in> Rs \<and> ?Q R f" for R f
     unfolding graph_homomorphism_def by auto
   hence "?S \<subseteq> {(R,f). R \<in> Rs \<and> ?Q R f}" unfolding subset_eq prod_eq by blast
   from finite_subset[OF this fin] show ?thesis by auto
 qed
 
 lemma inj_on_infinite:
   assumes "infinite A" "inj_on f A" "range f \<subseteq> B"
   shows "infinite B"
 proof -
   from assms[unfolded infinite_iff_countable_subset] obtain g::"nat \<Rightarrow> 'a" where
     g:"inj g \<and> range g \<subseteq> A" by blast
   hence i:"inj (f o g)" using assms(2) using comp_inj_on inj_on_subset by blast
   have "range (f o g) \<subseteq> B" using assms(3) by auto
   with i show ?thesis
     unfolding infinite_iff_countable_subset by blast
 qed
 
 lemma makestep_makes_selector_inj:
   assumes "selector (X y) = Some (R,f)"
           "selector (X x) = Some (R,f)"
           "valid_selector Rs selector"
     and step: "\<forall> i. X (Suc i) = make_step selector (X i)"
     and chain:"chain (\<lambda> i. graph_of (X i))"
   shows "x = y"
 proof(rule ccontr)
   assume a:"x \<noteq> y"
   define x' y' where "x' \<equiv> min x y" "y' \<equiv> max x y"
   hence xy:"selector (X x') = Some (R, f)" "selector (X y') = Some (R, f)" "x' < y'"
     using assms(1,2) a unfolding min_def max_def by auto
   with valid_selectorD assms
   have "valid_selection Rs (X x') R f" "valid_selection Rs (X y') R f" by auto
   hence not_ex:"\<not> extensible R (graph_of (X y')) f"
     and hom:"graph_homomorphism (fst R) (graph_of (X x')) f" "graph_rule R"
     unfolding valid_selection_def Let_def worklist_def by auto
   have X:"X (Suc x') = (max (fst (X x')) (nextMax (Range (extend (fst (X x')) R f))),
           on_triple (extend (fst (X x')) R f) `` edges (snd R) \<union> snd (X x'))"
     unfolding step[unfolded make_step_def Let_def,rule_format] xy by auto
   let ?ex = "extend (fst (X x')) R f"
   have hom:"graph_homomorphism (snd R) (graph_of (X (Suc x'))) ?ex"
        and agr:"agree_on (fst R) f ?ex" using extend(1,2)[OF hom] unfolding X by auto
   from xy have "Suc x' \<le> y'" by auto
   with chain[unfolded chain_def2] have "subgraph (graph_of (X (Suc x'))) (graph_of (X y'))" by auto
   from subgraph_preserves_hom[OF this hom]
   have hom:"graph_homomorphism (snd R) (graph_of (X y')) ?ex".
   with agr have "extensible R (graph_of (X y')) f" unfolding extensible_def by auto
   thus False using not_ex by auto
 qed
 
 lemma fair_through_make_step:
   assumes "finite Rs" "set_of_graph_rules Rs" "graph (graph_of (X 0))"
      (* It should suffice to take infinitely many make_steps, 
         rather than having every step be a make_step,
         but we focus on the algorithm as in the paper here *)
      and makestep: "\<forall> i. X (Suc i) = make_step selector (X i)"
      and selector: "valid_selector Rs selector"
   shows "fair_chain Rs (\<lambda> i. graph_of (X i))"
 proof
   show chn:"chain (\<lambda>i. graph_of (X i))" using WPC_through_make_step assms by blast
   fix R f i
   assume Rs:"R \<in> Rs" and h:"graph_homomorphism (fst R) (graph_of (X i)) f"
   hence R:"finite (vertices (snd R))" "subgraph (fst R) (snd R)"  "finite (vertices (fst R))"
     using assms by auto
   hence f:"finite f" "finite (Range f)" "finite (Domain f)" "univalent f" 
     using h unfolding graph_homomorphism_def Range_snd by auto
   define N where "N \<equiv> nextMax (Range f)"
   fix S
   let "?Q X' j" = " fst X' \<in> Rs
                   \<and> graph_homomorphism (fst (fst X')) (graph_of (X (j+i))) (snd X')
                   \<and> nextMax (Range (snd X')) \<le> N"
   let ?S = "{(R,f). \<exists>j. ?Q (R,f) j}"
   from assms(4) have "\<And>ia. X (Suc ia + i) = make_step selector (X (ia + i))" by auto
   note r = assms(1,2) chain_then_restrict[OF chn] this assms(5)
   from N_occurs_finitely_often[of Rs "\<lambda> j. X (j + i)",OF r]
   have fin_S:"finite ?S" by auto
   { assume a:"\<forall>j. \<not> extensible R (graph_of (X j)) f"
     let "?P X' j" = "?Q X' j \<and> Some X' = selector (X (j+i))"
     { fix j let ?j = "j+i" have "?j \<ge> i" by auto
       from subgraph_preserves_hom[OF chain[OF chn this] h]
       have h:"graph_homomorphism (fst R) (graph_of (X ?j)) f".
       have "\<not> extensible R (graph_of (X ?j)) f" using a by blast 
       with h Rs have wl:"(nextMax (Range f),R,f) \<in> worklist (X ?j) Rs" 
         unfolding worklist_def Let_def set_eq_iff by auto
       hence "worklist (X ?j) Rs \<noteq> {}" by auto
       with valid_selectorD[OF selector]
       obtain R' f'
         where sel:"Some (R',f') = selector (X ?j)"
                   "valid_selection Rs (X ?j) R' f'" by auto
       hence max:"(nextMax (Range f'), R', f') \<in> worklist (X ?j) Rs"
                 "(\<forall>(N, _)\<in>worklist (X ?j) Rs. nextMax (Range f') \<le> N)"
         unfolding valid_selection_def Let_def by auto
       with wl have "nextMax (Range f') \<le> N" unfolding N_def by auto
       with max(1)[unfolded worklist_def Let_def mem_Collect_eq prod.case] sel(1)
       have "\<exists> X'. ?P X' j" by (metis fst_conv snd_conv)
     }
     then obtain ch where ch:"\<And> j. ?P (ch j) j" by metis (* uses 'choice' internally *)
     have inj:"inj ch" proof fix x y assume "ch x = ch y"
       with ch[of x] ch[of y]
       have "selector (X (x + i)) = Some (ch x)" "selector (X (y + i)) = Some (ch x)" by auto
       with makestep_makes_selector_inj[OF _ _ selector makestep chn] have "x + i = y + i"
         by (cases "ch x",metis (full_types))
       thus "x = y" by auto
     qed
     have "ch x \<in> ?S" for x using ch[of x] unfolding mem_Collect_eq by(intro case_prodI2) metis
     hence "range ch \<subseteq> ?S" unfolding UNIV_def by(rule image_Collect_subsetI)
     with infinite_iff_countable_subset inj have "infinite ?S" by blast
     with fin_S have "False" by auto
   }
   thus "\<exists>j. extensible R (graph_of (X j)) f" by auto
 qed
 
 fun mk_chain where
   "mk_chain sel Rs init 0 = init" |
   "mk_chain sel Rs init (Suc n) = mk_chain sel Rs (make_step sel init) n"
 
 lemma mk_chain:
   "\<forall> i. mk_chain sel Rs init (Suc i) = make_step sel (mk_chain sel Rs init i)"
 proof
   fix i
   show "mk_chain sel Rs init (Suc i) = make_step sel (mk_chain sel Rs init i)"
     by (induct i arbitrary:init,auto)
 qed
 
 text \<open>Algorithm 1, abstractly.\<close>
 abbreviation the_lcg where
 "the_lcg sel Rs init \<equiv> chain_sup (\<lambda>i. graph_of (mk_chain sel Rs init i))"
 
 lemma mk_chain_edges:
   assumes "valid_selector Rules sel"
           "\<Union> ((edges o snd) ` Rules) \<subseteq> L \<times> UNIV"
           "edges (graph_of G) \<subseteq> L \<times> UNIV"
   shows "edges (graph_of (mk_chain sel Rules G i)) \<subseteq> L \<times> UNIV"
 using assms(3) proof(induct i arbitrary:G)
   case 0
   then show ?case using assms(2) by auto
 next
   case (Suc i G)
   hence "edges (graph_of (make_step sel G)) \<subseteq> L \<times> UNIV"
   proof(cases "sel G")
     case None show ?thesis unfolding None make_step_def using Suc by auto
   next
     case (Some a)
     then obtain R f where Some:"sel G = Some (R, f)" by fastforce
     hence "(a, x, y) \<in> edges (snd R) \<Longrightarrow> a \<in> L" for a x y
       using assms(2) valid_selectorD(2)[OF assms(1) Some]
       unfolding valid_selection_def Let_def worklist_def by auto
     then show ?thesis unfolding Some make_step_def Let_def using Suc by auto
   qed
   thus ?case unfolding mk_chain.simps by(rule Suc)
 qed
 
 lemma the_lcg_edges:
   assumes "valid_selector Rules sel"
           "fst ` (\<Union> ((edges o snd) ` Rules)) \<subseteq> L" (is "fst `?fR \<subseteq> _")
           "fst ` snd G \<subseteq> L"
   shows "fst ` edges (the_lcg sel Rules G) \<subseteq> L"
 proof -
   from assms have "fst `?fR \<times> UNIV \<subseteq> L \<times> UNIV" "fst `(edges (graph_of G)) \<times> UNIV \<subseteq> L \<times> UNIV"
     by auto
   hence "(\<Union> ((edges o snd) ` Rules)) \<subseteq> L \<times> UNIV" "edges (graph_of G) \<subseteq> L \<times> UNIV"
     using fst_UNIV[of ?fR] fst_UNIV[of "(edges (graph_of G))"] by blast+
   note assms = assms(1) this
   have "edges (graph_of (mk_chain sel Rules G i)) \<subseteq> L \<times> UNIV" for i
     using mk_chain_edges[OF assms,unfolded Times_subset_cancel2[OF UNIV_I]].
   hence "edges (the_lcg sel Rules G) \<subseteq> L \<times> UNIV" unfolding chain_sup_def by auto
   thus ?thesis by auto
 qed
 
 text \<open>Lemma 9.\<close>
 lemma lcg_through_make_step:
 assumes "finite Rs" "set_of_graph_rules Rs" "graph (graph_of init)"
         "valid_selector Rs sel"
   shows "least_consequence_graph t Rs (graph_of init) (the_lcg sel Rs init)"
 proof -
   from assms have gr:"graph (graph_of (mk_chain sel Rs init 0))" by auto
   note assms = assms(1,2) this mk_chain assms(4)
   from set_of_graph_rulesD[OF assms(2)]
   have "(\<And>R. R \<in> Rs \<Longrightarrow> subgraph (fst R) (snd R) \<and> finite_graph (fst R))" by auto
   from fair_chain_impl_consequence_graph[OF fair_through_make_step[OF assms] this]
        wpc_simpl[OF WPC_through_make_step(1)[OF assms(2-)],THEN wpc_least] 
   show ?thesis unfolding least_consequence_graph_def by auto
 qed
 
 end
diff --git a/thys/UTP/toolkit/List_Extra.thy b/thys/UTP/toolkit/List_Extra.thy
--- a/thys/UTP/toolkit/List_Extra.thy
+++ b/thys/UTP/toolkit/List_Extra.thy
@@ -1,892 +1,890 @@
 (******************************************************************************)
 (* Project: Isabelle/UTP Toolkit                                              *)
 (* File: List_Extra.thy                                                       *)
 (* Authors: Simon Foster and Frank Zeyda                                      *)
 (* Emails: simon.foster@york.ac.uk and frank.zeyda@york.ac.uk                 *)
 (******************************************************************************)
 
 section \<open> Lists: extra functions and properties \<close>
 
 theory List_Extra
   imports
   "HOL-Library.Sublist"
   "HOL-Library.Monad_Syntax"
   "HOL-Library.Prefix_Order"
   "Optics.Lens_Instances"
 begin
 
 subsection \<open> Useful Abbreviations \<close>
 
 abbreviation "list_sum xs \<equiv> foldr (+) xs 0"
 
 subsection \<open> Folds \<close>
 
 context abel_semigroup
 begin
 
   lemma foldr_snoc: "foldr (\<^bold>*) (xs @ [x]) k = (foldr (\<^bold>*) xs k) \<^bold>* x"
     by (induct xs, simp_all add: commute left_commute)
   
 end
 
 subsection \<open> List Lookup \<close>
 
 text \<open>
   The following variant of the standard \<open>nth\<close> function returns \<open>\<bottom>\<close> if the index is 
   out of range.
 \<close>
 
 primrec
   nth_el :: "'a list \<Rightarrow> nat \<Rightarrow> 'a option" ("_\<langle>_\<rangle>\<^sub>l" [90, 0] 91)
 where
   "[]\<langle>i\<rangle>\<^sub>l = None"
 | "(x # xs)\<langle>i\<rangle>\<^sub>l = (case i of 0 \<Rightarrow> Some x | Suc j \<Rightarrow> xs \<langle>j\<rangle>\<^sub>l)"
 
 lemma nth_el_appendl[simp]: "i < length xs \<Longrightarrow> (xs @ ys)\<langle>i\<rangle>\<^sub>l = xs\<langle>i\<rangle>\<^sub>l"
   apply (induct xs arbitrary: i)
    apply simp
   apply (case_tac i)
    apply simp_all
   done
 
 lemma nth_el_appendr[simp]: "length xs \<le> i \<Longrightarrow> (xs @ ys)\<langle>i\<rangle>\<^sub>l = ys\<langle>i - length xs\<rangle>\<^sub>l"
   apply (induct xs arbitrary: i)
    apply simp
   apply (case_tac i)
    apply simp_all
   done
 
 subsection \<open> Extra List Theorems \<close>
 
 subsubsection \<open> Map \<close>
 
 lemma map_nth_Cons_atLeastLessThan:
   "map (nth (x # xs)) [Suc m..<n] = map (nth xs) [m..<n - 1]"
 proof -
   have "nth xs = nth (x # xs) \<circ> Suc"
     by auto
   hence "map (nth xs) [m..<n - 1] = map (nth (x # xs) \<circ> Suc) [m..<n - 1]"
     by simp
   also have "... = map (nth (x # xs)) (map Suc [m..<n - 1])"
     by simp
   also have "... = map (nth (x # xs)) [Suc m..<n]"
     by (metis Suc_diff_1 le_0_eq length_upt list.simps(8) list.size(3) map_Suc_upt not_less upt_0)
   finally show ?thesis ..
 qed
 
 subsubsection \<open> Sorted Lists \<close>
 
 lemma sorted_last [simp]: "\<lbrakk> x \<in> set xs; sorted xs \<rbrakk> \<Longrightarrow> x \<le> last xs"
   by (induct xs, auto)
 
 lemma sorted_prefix:
   assumes "xs \<le> ys" "sorted ys"
   shows "sorted xs"
 proof -
   obtain zs where "ys = xs @ zs"
     using Prefix_Order.prefixE assms(1) by auto
   thus ?thesis
     using assms(2) sorted_append by blast
 qed
 
 lemma sorted_map: "\<lbrakk> sorted xs; mono f \<rbrakk> \<Longrightarrow> sorted (map f xs)"
   by (simp add: monoD sorted_iff_nth_mono)
 
 lemma sorted_distinct [intro]: "\<lbrakk> sorted (xs); distinct(xs) \<rbrakk> \<Longrightarrow> (\<forall> i<length xs - 1. xs!i < xs!(i + 1))"
   apply (induct xs)
    apply (auto)
   apply (metis (no_types, hide_lams) Suc_leI Suc_less_eq Suc_pred gr0_conv_Suc not_le not_less_iff_gr_or_eq nth_Cons_Suc nth_mem nth_non_equal_first_eq)
   done
 
 text \<open> Is the given list a permutation of the given set? \<close>
 
 definition is_sorted_list_of_set :: "('a::ord) set \<Rightarrow> 'a list \<Rightarrow> bool" where
 "is_sorted_list_of_set A xs = ((\<forall> i<length(xs) - 1. xs!i < xs!(i + 1)) \<and> set(xs) = A)"
 
 lemma sorted_is_sorted_list_of_set:
   assumes "is_sorted_list_of_set A xs"
   shows "sorted(xs)" and "distinct(xs)"
 using assms proof (induct xs arbitrary: A)
   show "sorted []"
     by auto
 next
   show "distinct []"
     by auto
 next
   fix A :: "'a set"
   case (Cons x xs) note hyps = this
   assume isl: "is_sorted_list_of_set A (x # xs)"
   hence srt: "(\<forall>i<length xs - Suc 0. xs ! i < xs ! Suc i)"
     using less_diff_conv by (auto simp add: is_sorted_list_of_set_def)
   with hyps(1) have srtd: "sorted xs"
     by (simp add: is_sorted_list_of_set_def)
   with isl show "sorted (x # xs)"
     apply (auto simp add: is_sorted_list_of_set_def)
     apply (metis (mono_tags, lifting) all_nth_imp_all_set less_le_trans linorder_not_less not_less_iff_gr_or_eq nth_Cons_0 sorted_iff_nth_mono zero_order(3))
     done
   from srt hyps(2) have "distinct xs"
     by (simp add: is_sorted_list_of_set_def)
   with isl show "distinct (x # xs)"
   proof -
     have "(\<forall>n. \<not> n < length (x # xs) - 1 \<or> (x # xs) ! n < (x # xs) ! (n + 1)) \<and> set (x # xs) = A"
       by (meson \<open>is_sorted_list_of_set A (x # xs)\<close> is_sorted_list_of_set_def)
   then show ?thesis
     by (metis \<open>distinct xs\<close> add.commute add_diff_cancel_left' distinct.simps(2) leD length_Cons length_greater_0_conv length_pos_if_in_set less_le nth_Cons_0 nth_Cons_Suc plus_1_eq_Suc set_ConsD sorted.elims(2) srtd)    
   qed
 qed
 
 lemma is_sorted_list_of_set_alt_def:
   "is_sorted_list_of_set A xs \<longleftrightarrow> sorted (xs) \<and> distinct (xs) \<and> set(xs) = A"
   apply (auto intro: sorted_is_sorted_list_of_set)
     apply (auto simp add: is_sorted_list_of_set_def)
   apply (metis Nat.add_0_right One_nat_def add_Suc_right sorted_distinct)
   done
 
 definition sorted_list_of_set_alt :: "('a::ord) set \<Rightarrow> 'a list" where
 "sorted_list_of_set_alt A =
   (if (A = {}) then [] else (THE xs. is_sorted_list_of_set A xs))"
 
 lemma is_sorted_list_of_set:
   "finite A \<Longrightarrow> is_sorted_list_of_set A (sorted_list_of_set A)"
-  apply (simp add: is_sorted_list_of_set_def)
-  apply (metis One_nat_def add.right_neutral add_Suc_right sorted_distinct sorted_list_of_set)
-  done
+  by (simp add: is_sorted_list_of_set_alt_def)
 
 lemma sorted_list_of_set_other_def:
   "finite A \<Longrightarrow> sorted_list_of_set(A) = (THE xs. sorted(xs) \<and> distinct(xs) \<and> set xs = A)"
   apply (rule sym)
   apply (rule the_equality)
    apply (auto)
   apply (simp add: sorted_distinct_set_unique)
   done
 
 lemma sorted_list_of_set_alt [simp]:
   "finite A \<Longrightarrow> sorted_list_of_set_alt(A) = sorted_list_of_set(A)"
   apply (rule sym)
   apply (auto simp add: sorted_list_of_set_alt_def is_sorted_list_of_set_alt_def sorted_list_of_set_other_def)
   done
 
 text \<open> Sorting lists according to a relation \<close>
 
 definition is_sorted_list_of_set_by :: "'a rel \<Rightarrow> 'a set \<Rightarrow> 'a list \<Rightarrow> bool" where
 "is_sorted_list_of_set_by R A xs = ((\<forall> i<length(xs) - 1. (xs!i, xs!(i + 1)) \<in> R) \<and> set(xs) = A)"
 
 definition sorted_list_of_set_by :: "'a rel \<Rightarrow> 'a set \<Rightarrow> 'a list" where
 "sorted_list_of_set_by R A = (THE xs. is_sorted_list_of_set_by R A xs)"
 
 definition fin_set_lexord :: "'a rel \<Rightarrow> 'a set rel" where
 "fin_set_lexord R = {(A, B). finite A \<and> finite B \<and>
                              (\<exists> xs ys. is_sorted_list_of_set_by R A xs \<and> is_sorted_list_of_set_by R B ys
                               \<and> (xs, ys) \<in> lexord R)}"
 
 lemma is_sorted_list_of_set_by_mono:
   "\<lbrakk> R \<subseteq> S; is_sorted_list_of_set_by R A xs \<rbrakk> \<Longrightarrow> is_sorted_list_of_set_by S A xs"
   by (auto simp add: is_sorted_list_of_set_by_def)
 
 lemma lexord_mono':
   "\<lbrakk> (\<And> x y. f x y \<longrightarrow> g x y); (xs, ys) \<in> lexord {(x, y). f x y} \<rbrakk> \<Longrightarrow> (xs, ys) \<in> lexord {(x, y). g x y}"
   by (metis case_prodD case_prodI lexord_take_index_conv mem_Collect_eq)
 
 lemma fin_set_lexord_mono [mono]:
   "(\<And> x y. f x y \<longrightarrow> g x y) \<Longrightarrow> (xs, ys) \<in> fin_set_lexord {(x, y). f x y} \<longrightarrow> (xs, ys) \<in> fin_set_lexord {(x, y). g x y}"
 proof
   assume
     fin: "(xs, ys) \<in> fin_set_lexord {(x, y). f x y}" and
     hyp: "(\<And> x y. f x y \<longrightarrow> g x y)"
 
   from fin have "finite xs" "finite ys"
     using fin_set_lexord_def by fastforce+
 
   with fin hyp show "(xs, ys) \<in> fin_set_lexord {(x, y). g x y}"
     apply (auto simp add: fin_set_lexord_def)
     apply (rename_tac xs' ys')
     apply (rule_tac x="xs'" in exI)
     apply (auto)
      apply (metis case_prodD case_prodI is_sorted_list_of_set_by_def mem_Collect_eq)
     apply (metis case_prodD case_prodI is_sorted_list_of_set_by_def lexord_mono' mem_Collect_eq)
     done
 qed
 
 definition distincts :: "'a set \<Rightarrow> 'a list set" where
 "distincts A = {xs \<in> lists A. distinct(xs)}"
 
 lemma tl_element:
   "\<lbrakk> x \<in> set xs; x \<noteq> hd(xs) \<rbrakk> \<Longrightarrow> x \<in> set(tl(xs))"
   by (metis in_set_insert insert_Nil list.collapse list.distinct(2) set_ConsD)
 
 subsubsection \<open> List Update \<close>
 
 lemma listsum_update:
   fixes xs :: "'a::ring list"
   assumes "i < length xs"
   shows "list_sum (xs[i := v]) = list_sum xs - xs ! i + v"
 using assms proof (induct xs arbitrary: i)
   case Nil
   then show ?case by (simp)
 next
   case (Cons a xs)
   then show ?case
   proof (cases i)
     case 0
     thus ?thesis
       by (simp add: add.commute) 
   next
     case (Suc i')
     with Cons show ?thesis
       by (auto)
   qed
 qed
 
 subsubsection \<open> Drop While and Take While \<close>
 
 
 lemma dropWhile_sorted_le_above:
   "\<lbrakk> sorted xs; x \<in> set (dropWhile (\<lambda> x. x \<le> n) xs) \<rbrakk> \<Longrightarrow> x > n"
   apply (induct xs)
    apply (auto)
   apply (rename_tac a xs)
   apply (case_tac "a \<le> n")
    apply (auto)
 done
 
 lemma set_dropWhile_le:
   "sorted xs \<Longrightarrow> set (dropWhile (\<lambda> x. x \<le> n) xs) = {x\<in>set xs. x > n}"
   apply (induct xs)
    apply (simp)
   apply (rename_tac x xs)
   apply (subgoal_tac "sorted xs")
    apply (simp)
    apply (safe)
      apply (auto)
 done
 
 lemma set_takeWhile_less_sorted:
   "\<lbrakk> sorted I; x \<in> set I; x < n \<rbrakk> \<Longrightarrow> x \<in> set (takeWhile (\<lambda>x. x < n) I)"
 proof (induct I arbitrary: x)
   case Nil thus ?case
     by (simp)
 next
   case (Cons a I) thus ?case
     by auto
 qed
 
 lemma nth_le_takeWhile_ord: "\<lbrakk> sorted xs; i \<ge> length (takeWhile (\<lambda> x. x \<le> n) xs); i < length xs \<rbrakk> \<Longrightarrow> n \<le> xs ! i"
   apply (induct xs arbitrary: i, auto)
   apply (rename_tac x xs i)
   apply (case_tac "x \<le> n")
    apply (auto)
   apply (metis One_nat_def Suc_eq_plus1 le_less_linear le_less_trans less_imp_le list.size(4) nth_mem set_ConsD)
   done
 
 lemma length_takeWhile_less:
   "\<lbrakk> a \<in> set xs; \<not> P a \<rbrakk> \<Longrightarrow> length (takeWhile P xs) < length xs"
   by (metis in_set_conv_nth length_takeWhile_le nat_neq_iff not_less set_takeWhileD takeWhile_nth)
 
 lemma nth_length_takeWhile_less:
   "\<lbrakk> sorted xs; distinct xs; (\<exists> a \<in> set xs. a \<ge> n) \<rbrakk> \<Longrightarrow> xs ! length (takeWhile (\<lambda>x. x < n) xs) \<ge> n"
   by (induct xs, auto)
 
 subsubsection \<open> Last and But Last \<close>
 
 lemma length_gt_zero_butlast_concat:
   assumes "length ys > 0"
   shows "butlast (xs @ ys) = xs @ (butlast ys)"
   using assms by (metis butlast_append length_greater_0_conv)
 
 lemma length_eq_zero_butlast_concat:
   assumes "length ys = 0"
   shows "butlast (xs @ ys) = butlast xs"
   using assms by (metis append_Nil2 length_0_conv)
 
 lemma butlast_single_element:
   shows "butlast [e] = []"
   by (metis butlast.simps(2))
 
 lemma last_single_element:
   shows "last [e] = e"
   by (metis last.simps)
 
 lemma length_zero_last_concat:
   assumes "length t = 0"
   shows "last (s @ t) = last s"
   by (metis append_Nil2 assms length_0_conv)
 
 lemma length_gt_zero_last_concat:
   assumes "length t > 0"
   shows "last (s @ t) = last t"
   by (metis assms last_append length_greater_0_conv)
 
 subsubsection \<open> Prefixes and Strict Prefixes \<close>
 
 lemma prefix_length_eq:
   "\<lbrakk> length xs = length ys; prefix xs ys \<rbrakk> \<Longrightarrow> xs = ys"
   by (metis not_equal_is_parallel parallel_def)
 
 lemma prefix_Cons_elim [elim]:
   assumes "prefix (x # xs) ys"
   obtains ys' where "ys = x # ys'" "prefix xs ys'"
   using assms
   by (metis append_Cons prefix_def)
 
 lemma prefix_map_inj:
   "\<lbrakk> inj_on f (set xs \<union> set ys); prefix (map f xs) (map f ys) \<rbrakk> \<Longrightarrow>
    prefix xs ys"
   apply (induct xs arbitrary:ys)
    apply (simp_all)
   apply (erule prefix_Cons_elim)
   apply (auto)
   apply (metis image_insert insertI1 insert_Diff_if singletonE)
   done
 
 lemma prefix_map_inj_eq [simp]:
   "inj_on f (set xs \<union> set ys) \<Longrightarrow>
    prefix (map f xs) (map f ys) \<longleftrightarrow> prefix xs ys"
   using map_mono_prefix prefix_map_inj by blast
 
 lemma strict_prefix_Cons_elim [elim]:
   assumes "strict_prefix (x # xs) ys"
   obtains ys' where "ys = x # ys'" "strict_prefix xs ys'"
   using assms
   by (metis Sublist.strict_prefixE' Sublist.strict_prefixI' append_Cons)
 
 lemma strict_prefix_map_inj:
   "\<lbrakk> inj_on f (set xs \<union> set ys); strict_prefix (map f xs) (map f ys) \<rbrakk> \<Longrightarrow>
    strict_prefix xs ys"
   apply (induct xs arbitrary:ys)
    apply (auto)
   using prefix_bot.bot.not_eq_extremum apply fastforce
   apply (erule strict_prefix_Cons_elim)
   apply (auto)
   apply (metis (hide_lams, full_types) image_insert insertI1 insert_Diff_if singletonE)
   done
 
 lemma strict_prefix_map_inj_eq [simp]:
   "inj_on f (set xs \<union> set ys) \<Longrightarrow>
    strict_prefix (map f xs) (map f ys) \<longleftrightarrow> strict_prefix xs ys"
   by (simp add: inj_on_map_eq_map strict_prefix_def)
 
 lemma prefix_drop:
   "\<lbrakk> drop (length xs) ys = zs; prefix xs ys \<rbrakk>
    \<Longrightarrow> ys = xs @ zs"
   by (metis append_eq_conv_conj prefix_def)
 
 lemma list_append_prefixD [dest]: "x @ y \<le> z \<Longrightarrow> x \<le> z"
   using append_prefixD less_eq_list_def by blast
 
 lemma prefix_not_empty:
   assumes "strict_prefix xs ys" and "xs \<noteq> []"
   shows "ys \<noteq> []"
   using Sublist.strict_prefix_simps(1) assms(1) by blast
 
 lemma prefix_not_empty_length_gt_zero:
   assumes "strict_prefix xs ys" and "xs \<noteq> []"
   shows "length ys > 0"
   using assms prefix_not_empty by auto
 
 lemma butlast_prefix_suffix_not_empty:
   assumes "strict_prefix (butlast xs) ys"
   shows "ys \<noteq> []"
   using assms prefix_not_empty_length_gt_zero by fastforce
 
 lemma prefix_and_concat_prefix_is_concat_prefix:
   assumes "prefix s t" "prefix (e @ t) u"
   shows "prefix (e @ s) u"
   using Sublist.same_prefix_prefix assms(1) assms(2) prefix_order.dual_order.trans by blast
 
 lemma prefix_eq_exists:
   "prefix s t \<longleftrightarrow> (\<exists>xs . s @ xs = t)"
   using prefix_def by auto
 
 lemma strict_prefix_eq_exists:
   "strict_prefix s t \<longleftrightarrow> (\<exists>xs . s @ xs = t \<and> (length xs) > 0)"
   using prefix_def strict_prefix_def by auto
 
 lemma butlast_strict_prefix_eq_butlast:
   assumes "length s = length t" and "strict_prefix (butlast s) t"
   shows "strict_prefix (butlast s) t \<longleftrightarrow> (butlast s) = (butlast t)"
   by (metis append_butlast_last_id append_eq_append_conv assms(1) assms(2) length_0_conv length_butlast strict_prefix_eq_exists)
 
 lemma butlast_eq_if_eq_length_and_prefix:
   assumes "length s > 0" "length z > 0"
           "length s = length z" "strict_prefix (butlast s) t" "strict_prefix (butlast z) t"
   shows   "(butlast s) = (butlast z)"
   using assms by (auto simp add:strict_prefix_eq_exists)
 
 lemma prefix_imp_length_lteq:
   assumes "prefix s t"
   shows "length s \<le> length t"
   using assms by (simp add: Sublist.prefix_length_le)
 
 lemma prefix_imp_length_not_gt:
   assumes "prefix s t"
   shows "\<not> length t < length s"
   using assms by (simp add: Sublist.prefix_length_le leD)
 
 lemma prefix_and_eq_length_imp_eq_list:
   assumes "prefix s t" and "length t = length s"
   shows "s=t"
   using assms by (simp add: prefix_length_eq)
 
 lemma butlast_prefix_imp_length_not_gt:
   assumes "length s > 0" "strict_prefix (butlast s) t"
   shows "\<not> (length t < length s)"
   using assms prefix_length_less by fastforce
 
 lemma length_not_gt_iff_eq_length:
   assumes "length s > 0" and "strict_prefix (butlast s) t"
   shows "(\<not> (length s < length t)) = (length s = length t)"
 proof -
   have "(\<not> (length s < length t)) = ((length t < length s) \<or> (length s = length t))"
       by (metis not_less_iff_gr_or_eq)
   also have "... = (length s = length t)"
       using assms
       by (simp add:butlast_prefix_imp_length_not_gt)
 
   finally show ?thesis .
 qed
 
 text \<open> Greatest common prefix \<close>
 
 fun gcp :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where
 "gcp [] ys = []" |
 "gcp (x # xs) (y # ys) = (if (x = y) then x # gcp xs ys else [])" |
 "gcp _ _ = []"
 
 lemma gcp_right [simp]: "gcp xs [] = []"
   by (induct xs, auto)
 
 lemma gcp_append [simp]: "gcp (xs @ ys) (xs @ zs) = xs @ gcp ys zs"
   by (induct xs, auto)
 
 lemma gcp_lb1: "prefix (gcp xs ys) xs"
   apply (induct xs arbitrary: ys, auto)
   apply (case_tac ys, auto)
   done
 
 lemma gcp_lb2: "prefix (gcp xs ys) ys"
   apply (induct ys arbitrary: xs, auto)
   apply (case_tac xs, auto)
   done
 
 interpretation prefix_semilattice: semilattice_inf gcp prefix strict_prefix
 proof
   fix xs ys :: "'a list"
   show "prefix (gcp xs ys) xs"
     by (induct xs arbitrary: ys, auto, case_tac ys, auto)
   show "prefix (gcp xs ys) ys"
     by (induct ys arbitrary: xs, auto, case_tac xs, auto)
 next
   fix xs ys zs :: "'a list"
   assume "prefix xs ys" "prefix xs zs"
   thus "prefix xs (gcp ys zs)"
     by (simp add: prefix_def, auto)
 qed
 
 subsubsection \<open> Lexicographic Order \<close>
 
 lemma lexord_append:
   assumes "(xs\<^sub>1 @ ys\<^sub>1, xs\<^sub>2 @ ys\<^sub>2) \<in> lexord R" "length(xs\<^sub>1) = length(xs\<^sub>2)"
   shows "(xs\<^sub>1, xs\<^sub>2) \<in> lexord R \<or> (xs\<^sub>1 = xs\<^sub>2 \<and> (ys\<^sub>1, ys\<^sub>2) \<in> lexord R)"
 using assms
 proof (induct xs\<^sub>2 arbitrary: xs\<^sub>1)
   case (Cons x\<^sub>2 xs\<^sub>2') note hyps = this
   from hyps(3) obtain x\<^sub>1 xs\<^sub>1' where xs\<^sub>1: "xs\<^sub>1 = x\<^sub>1 # xs\<^sub>1'" "length(xs\<^sub>1') = length(xs\<^sub>2')"
     by (auto, metis Suc_length_conv)
   with hyps(2) have xcases: "(x\<^sub>1, x\<^sub>2) \<in> R \<or> (xs\<^sub>1' @ ys\<^sub>1, xs\<^sub>2' @ ys\<^sub>2) \<in> lexord R"
     by (auto)
   show ?case
   proof (cases "(x\<^sub>1, x\<^sub>2) \<in> R")
     case True with xs\<^sub>1 show ?thesis
       by (auto)
   next
     case False
     with xcases have "(xs\<^sub>1' @ ys\<^sub>1, xs\<^sub>2' @ ys\<^sub>2) \<in> lexord R"
       by (auto)
     with hyps(1) xs\<^sub>1 have dichot: "(xs\<^sub>1', xs\<^sub>2') \<in> lexord R \<or> (xs\<^sub>1' = xs\<^sub>2' \<and> (ys\<^sub>1, ys\<^sub>2) \<in> lexord R)"
       by (auto)
     have "x\<^sub>1 = x\<^sub>2"
       using False hyps(2) xs\<^sub>1(1) by auto
     with dichot xs\<^sub>1 show ?thesis
       by (simp)
   qed
 next
   case Nil thus ?case
     by auto
 qed
 
 lemma strict_prefix_lexord_rel:
   "strict_prefix xs ys \<Longrightarrow> (xs, ys) \<in> lexord R"
   by (metis Sublist.strict_prefixE' lexord_append_rightI)
 
 lemma strict_prefix_lexord_left:
   assumes "trans R" "(xs, ys) \<in> lexord R" "strict_prefix xs' xs"
   shows "(xs', ys) \<in> lexord R"
   by (metis assms lexord_trans strict_prefix_lexord_rel)
 
 lemma prefix_lexord_right:
   assumes "trans R" "(xs, ys) \<in> lexord R" "strict_prefix ys ys'"
   shows "(xs, ys') \<in> lexord R"
   by (metis assms lexord_trans strict_prefix_lexord_rel)
 
 lemma lexord_eq_length:
   assumes "(xs, ys) \<in> lexord R" "length xs = length ys"
   shows "\<exists> i. (xs!i, ys!i) \<in> R \<and> i < length xs \<and> (\<forall> j<i. xs!j = ys!j)"
 using assms proof (induct xs arbitrary: ys)
   case (Cons x xs) note hyps = this
   then obtain y ys' where ys: "ys = y # ys'" "length ys' = length xs"
     by (metis Suc_length_conv)
   show ?case
   proof (cases "(x, y) \<in> R")
     case True with ys show ?thesis
       by (rule_tac x="0" in exI, simp)
   next
     case False
     with ys hyps(2) have xy: "x = y" "(xs, ys') \<in> lexord R"
       by auto
     with hyps(1,3) ys obtain i where "(xs!i, ys'!i) \<in> R" "i < length xs" "(\<forall> j<i. xs!j = ys'!j)"
       by force
     with xy ys show ?thesis
       apply (rule_tac x="Suc i" in exI)
       apply (auto simp add: less_Suc_eq_0_disj)
     done
   qed
 next
   case Nil thus ?case by (auto)
 qed
 
 lemma lexord_intro_elems:
   assumes "length xs > i" "length ys > i" "(xs!i, ys!i) \<in> R" "\<forall> j<i. xs!j = ys!j"
   shows "(xs, ys) \<in> lexord R"
 using assms proof (induct i arbitrary: xs ys)
   case 0 thus ?case
     by (auto, metis lexord_cons_cons list.exhaust nth_Cons_0)
 next
   case (Suc i) note hyps = this
   then obtain x' y' xs' ys' where "xs = x' # xs'" "ys = y' # ys'"
     by (metis Suc_length_conv Suc_lessE)
   moreover with hyps(5) have "\<forall>j<i. xs' ! j = ys' ! j"
     by (auto)
   ultimately show ?case using hyps
     by (auto)
 qed
 
 subsection \<open> Distributed Concatenation \<close>
 
 definition uncurry :: "('a \<Rightarrow> 'b \<Rightarrow>  'c) \<Rightarrow> ('a \<times> 'b \<Rightarrow> 'c)" where
 [simp]: "uncurry f = (\<lambda>(x, y). f x y)"
 
 definition dist_concat ::
   "'a list set \<Rightarrow> 'a list set \<Rightarrow> 'a list set" (infixr "\<^sup>\<frown>" 100) where
 "dist_concat ls1 ls2 = (uncurry (@) ` (ls1 \<times> ls2))"
 
 lemma dist_concat_left_empty [simp]:
   "{} \<^sup>\<frown> ys = {}"
   by (simp add: dist_concat_def)
 
 lemma dist_concat_right_empty [simp]:
   "xs \<^sup>\<frown> {} = {}"
   by (simp add: dist_concat_def)
 
 lemma dist_concat_insert [simp]:
 "insert l ls1 \<^sup>\<frown> ls2 = ((@) l ` ( ls2)) \<union> (ls1 \<^sup>\<frown> ls2)"
   by (auto simp add: dist_concat_def)
 
 subsection \<open> List Domain and Range \<close>
 
 abbreviation seq_dom :: "'a list \<Rightarrow> nat set" ("dom\<^sub>l") where
 "seq_dom xs \<equiv> {0..<length xs}"
 
 abbreviation seq_ran :: "'a list \<Rightarrow> 'a set" ("ran\<^sub>l") where
 "seq_ran xs \<equiv> set xs"
 
 subsection \<open> Extracting List Elements \<close>
 
 definition seq_extract :: "nat set \<Rightarrow> 'a list \<Rightarrow> 'a list" (infix "\<upharpoonleft>\<^sub>l" 80) where
 "seq_extract A xs = nths xs A"
 
 lemma seq_extract_Nil [simp]: "A \<upharpoonleft>\<^sub>l [] = []"
   by (simp add: seq_extract_def)
 
 lemma seq_extract_Cons:
   "A \<upharpoonleft>\<^sub>l (x # xs) = (if 0 \<in> A then [x] else []) @ {j. Suc j \<in> A} \<upharpoonleft>\<^sub>l xs"
   by (simp add: seq_extract_def nths_Cons)
 
 lemma seq_extract_empty [simp]: "{} \<upharpoonleft>\<^sub>l xs = []"
   by (simp add: seq_extract_def)
 
 lemma seq_extract_ident [simp]: "{0..<length xs} \<upharpoonleft>\<^sub>l xs = xs"
   unfolding list_eq_iff_nth_eq
   by (auto simp add: seq_extract_def length_nths atLeast0LessThan)
 
 lemma seq_extract_split:
   assumes "i \<le> length xs"
   shows "{0..<i} \<upharpoonleft>\<^sub>l xs @ {i..<length xs} \<upharpoonleft>\<^sub>l xs = xs"
 using assms
 proof (induct xs arbitrary: i)
   case Nil thus ?case by (simp add: seq_extract_def)
 next
   case (Cons x xs) note hyp = this
   have "{j. Suc j < i} = {0..<i - 1}"
     by (auto)
   moreover have "{j. i \<le> Suc j \<and> j < length xs} = {i - 1..<length xs}"
     by (auto)
   ultimately show ?case
     using hyp by (force simp add: seq_extract_def nths_Cons)
 qed
 
 lemma seq_extract_append:
   "A \<upharpoonleft>\<^sub>l (xs @ ys) = (A \<upharpoonleft>\<^sub>l xs) @ ({j. j + length xs \<in> A} \<upharpoonleft>\<^sub>l ys)"
   by (simp add: seq_extract_def nths_append)
 
 lemma seq_extract_range: "A \<upharpoonleft>\<^sub>l xs = (A \<inter> dom\<^sub>l(xs)) \<upharpoonleft>\<^sub>l xs"
   apply (auto simp add: seq_extract_def nths_def)
   apply (metis (no_types, lifting) atLeastLessThan_iff filter_cong in_set_zip nth_mem set_upt)
 done
 
 lemma seq_extract_out_of_range:
   "A \<inter> dom\<^sub>l(xs) = {} \<Longrightarrow> A \<upharpoonleft>\<^sub>l xs = []"
   by (metis seq_extract_def seq_extract_range nths_empty)
 
 lemma seq_extract_length [simp]:
   "length (A \<upharpoonleft>\<^sub>l xs) = card (A \<inter> dom\<^sub>l(xs))"
 proof -
   have "{i. i < length(xs) \<and> i \<in> A} = (A \<inter> {0..<length(xs)})"
     by (auto)
   thus ?thesis
     by (simp add: seq_extract_def length_nths)
 qed
 
 lemma seq_extract_Cons_atLeastLessThan:
   assumes "m < n"
   shows "{m..<n} \<upharpoonleft>\<^sub>l (x # xs) = (if (m = 0) then x # ({0..<n-1} \<upharpoonleft>\<^sub>l xs) else {m-1..<n-1} \<upharpoonleft>\<^sub>l xs)"
 proof -
   have "{j. Suc j < n} = {0..<n - Suc 0}"
     by (auto)
   moreover have "{j. m \<le> Suc j \<and> Suc j < n} = {m - Suc 0..<n - Suc 0}"
     by (auto)
 
   ultimately show ?thesis using assms
     by (auto simp add: seq_extract_Cons)
 qed
 
 lemma seq_extract_singleton:
   assumes "i < length xs"
   shows "{i} \<upharpoonleft>\<^sub>l xs = [xs ! i]"
   using assms
   apply (induct xs arbitrary: i)
   apply (auto simp add: seq_extract_Cons)
   apply (rename_tac xs i)
   apply (subgoal_tac "{j. Suc j = i} = {i - 1}")
   apply (auto)
 done
 
 lemma seq_extract_as_map:
   assumes "m < n" "n \<le> length xs"
   shows "{m..<n} \<upharpoonleft>\<^sub>l xs = map (nth xs) [m..<n]"
 using assms proof (induct xs arbitrary: m n)
   case Nil thus ?case by simp
 next
   case (Cons x xs)
   have "[m..<n] = m # [m+1..<n]"
     using Cons.prems(1) upt_eq_Cons_conv by blast
   moreover have "map (nth (x # xs)) [Suc m..<n] = map (nth xs) [m..<n-1]"
     by (simp add: map_nth_Cons_atLeastLessThan)
   ultimately show ?case
     using Cons upt_rec
     by (auto simp add: seq_extract_Cons_atLeastLessThan)
 qed
 
 lemma seq_append_as_extract:
   "xs = ys @ zs \<longleftrightarrow> (\<exists> i\<le>length(xs). ys = {0..<i} \<upharpoonleft>\<^sub>l xs \<and> zs = {i..<length(xs)} \<upharpoonleft>\<^sub>l xs)"
 proof
   assume xs: "xs = ys @ zs"
   moreover have "ys = {0..<length ys} \<upharpoonleft>\<^sub>l (ys @ zs)"
     by (simp add: seq_extract_append)
   moreover have "zs = {length ys..<length ys + length zs} \<upharpoonleft>\<^sub>l (ys @ zs)"
   proof -
     have "{length ys..<length ys + length zs} \<inter> {0..<length ys} = {}"
       by auto
     moreover have s1: "{j. j < length zs} = {0..<length zs}"
       by auto
     ultimately show ?thesis
       by (simp add: seq_extract_append seq_extract_out_of_range)
   qed
   ultimately show "(\<exists> i\<le>length(xs). ys = {0..<i} \<upharpoonleft>\<^sub>l xs \<and> zs = {i..<length(xs)} \<upharpoonleft>\<^sub>l xs)"
     by (rule_tac x="length ys" in exI, auto)
 next
   assume "\<exists>i\<le>length xs. ys = {0..<i} \<upharpoonleft>\<^sub>l xs \<and> zs = {i..<length xs} \<upharpoonleft>\<^sub>l xs"
   thus "xs = ys @ zs"
     by (auto simp add: seq_extract_split)
 qed
 
 subsection \<open> Filtering a list according to a set \<close>
 
 definition seq_filter :: "'a list \<Rightarrow> 'a set \<Rightarrow> 'a list" (infix "\<restriction>\<^sub>l" 80) where
 "seq_filter xs A = filter (\<lambda> x. x \<in> A) xs"
 
 lemma seq_filter_Cons_in [simp]: 
   "x \<in> cs \<Longrightarrow> (x # xs) \<restriction>\<^sub>l cs = x # (xs \<restriction>\<^sub>l cs)"
   by (simp add: seq_filter_def)
 
 lemma seq_filter_Cons_out [simp]: 
   "x \<notin> cs \<Longrightarrow> (x # xs) \<restriction>\<^sub>l cs = (xs \<restriction>\<^sub>l cs)"
   by (simp add: seq_filter_def)
 
 lemma seq_filter_Nil [simp]: "[] \<restriction>\<^sub>l A = []"
   by (simp add: seq_filter_def)
 
 lemma seq_filter_empty [simp]: "xs \<restriction>\<^sub>l {} = []"
   by (simp add: seq_filter_def)
 
 lemma seq_filter_append: "(xs @ ys) \<restriction>\<^sub>l A = (xs \<restriction>\<^sub>l A) @ (ys \<restriction>\<^sub>l A)"
   by (simp add: seq_filter_def)
 
 lemma seq_filter_UNIV [simp]: "xs \<restriction>\<^sub>l UNIV = xs"
   by (simp add: seq_filter_def)
 
 lemma seq_filter_twice [simp]: "(xs \<restriction>\<^sub>l A) \<restriction>\<^sub>l B = xs \<restriction>\<^sub>l (A \<inter> B)"
   by (simp add: seq_filter_def)
 
 subsection \<open> Minus on lists \<close>
 
 instantiation list :: (type) minus
 begin
 
 text \<open> We define list minus so that if the second list is not a prefix of the first, then an arbitrary
         list longer than the combined length is produced. Thus we can always determined from the output
         whether the minus is defined or not. \<close>
 
 definition "xs - ys = (if (prefix ys xs) then drop (length ys) xs else [])"
 
 instance ..
 end
 
 lemma minus_cancel [simp]: "xs - xs = []"
   by (simp add: minus_list_def)
 
 lemma append_minus [simp]: "(xs @ ys) - xs = ys"
   by (simp add: minus_list_def)
 
 lemma minus_right_nil [simp]: "xs - [] = xs"
   by (simp add: minus_list_def)
 
 lemma list_concat_minus_list_concat: "(s @ t) - (s @ z) = t - z"
   by (simp add: minus_list_def)
 
 lemma length_minus_list: "y \<le> x \<Longrightarrow> length(x - y) = length(x) - length(y)"
   by (simp add: less_eq_list_def minus_list_def)
 
 lemma map_list_minus:
   "xs \<le> ys \<Longrightarrow> map f (ys - xs) = map f ys - map f xs"
   by (simp add: drop_map less_eq_list_def map_mono_prefix minus_list_def)
 
 lemma list_minus_first_tl [simp]: 
   "[x] \<le> xs \<Longrightarrow> (xs - [x]) = tl xs"
   by (metis Prefix_Order.prefixE append.left_neutral append_minus list.sel(3) not_Cons_self2 tl_append2)
 
 text \<open> Extra lemmas about @{term prefix} and @{term strict_prefix} \<close>
 
 lemma prefix_concat_minus:
   assumes "prefix xs ys"
   shows "xs @ (ys - xs) = ys"
   using assms by (metis minus_list_def prefix_drop)
 
 lemma prefix_minus_concat:
   assumes "prefix s t"
   shows "(t - s) @ z = (t @ z) - s"
   using assms by (simp add: Sublist.prefix_length_le minus_list_def)
 
 lemma strict_prefix_minus_not_empty:
   assumes "strict_prefix xs ys"
   shows "ys - xs \<noteq> []"
   using assms by (metis append_Nil2 prefix_concat_minus strict_prefix_def)
 
 lemma strict_prefix_diff_minus:
   assumes "prefix xs ys" and "xs \<noteq> ys"
   shows "(ys - xs) \<noteq> []"
   using assms by (simp add: strict_prefix_minus_not_empty)
 
 lemma length_tl_list_minus_butlast_gt_zero:
   assumes "length s < length t" and "strict_prefix (butlast s) t" and "length s > 0"
   shows "length (tl (t - (butlast s))) > 0"
   using assms
   by (metis Nitpick.size_list_simp(2) butlast_snoc hd_Cons_tl length_butlast length_greater_0_conv length_tl less_trans nat_neq_iff strict_prefix_minus_not_empty prefix_order.dual_order.strict_implies_order prefix_concat_minus)
 
 lemma list_minus_butlast_eq_butlast_list:
   assumes "length t = length s" and "strict_prefix (butlast s) t"
   shows "t - (butlast s) = [last t]"
   using assms
   by (metis append_butlast_last_id append_eq_append_conv butlast.simps(1) length_butlast less_numeral_extra(3) list.size(3) prefix_order.dual_order.strict_implies_order prefix_concat_minus prefix_length_less)
 
 lemma butlast_strict_prefix_length_lt_imp_last_tl_minus_butlast_eq_last:
   assumes "length s > 0" "strict_prefix (butlast s) t" "length s < length t"
   shows "last (tl (t - (butlast s))) = (last t)"
   using assms by (metis last_append last_tl length_tl_list_minus_butlast_gt_zero less_numeral_extra(3) list.size(3) append_minus strict_prefix_eq_exists)
 
 lemma tl_list_minus_butlast_not_empty:
   assumes "strict_prefix (butlast s) t" and "length s > 0" and "length t > length s"
   shows "tl (t - (butlast s)) \<noteq> []"
   using assms length_tl_list_minus_butlast_gt_zero by fastforce
 
 lemma tl_list_minus_butlast_empty:
   assumes "strict_prefix (butlast s) t" and "length s > 0" and "length t = length s"
   shows "tl (t - (butlast s)) = []"
   using assms by (simp add: list_minus_butlast_eq_butlast_list)
 
 lemma concat_minus_list_concat_butlast_eq_list_minus_butlast:
   assumes "prefix (butlast u) s"
   shows "(t @ s) - (t @ (butlast u)) = s - (butlast u)"
   using assms by (metis append_assoc prefix_concat_minus append_minus)
 
 lemma tl_list_minus_butlast_eq_empty:
   assumes "strict_prefix (butlast s) t" and "length s = length t"
   shows "tl (t - (butlast s)) = []"
   using assms by (metis list.sel(3) list_minus_butlast_eq_butlast_list)
 
 (* this can be shown using length_tl, but care is needed when list is empty? *)
 lemma prefix_length_tl_minus:
   assumes "strict_prefix s t"
   shows "length (tl (t-s)) = (length (t-s)) - 1"
   by (auto)
 
 lemma length_list_minus:
   assumes "strict_prefix s t"
   shows "length(t - s) = length(t) - length(s)"
   using assms by (simp add: minus_list_def prefix_order.dual_order.strict_implies_order)
 
 subsection \<open> Laws on @{term take}, @{term drop}, and @{term nths} \<close>
 
 lemma take_prefix: "m \<le> n \<Longrightarrow> take m xs \<le> take n xs"
   by (metis Prefix_Order.prefixI append_take_drop_id min_absorb2 take_append take_take)
 
 lemma nths_atLeastAtMost_0_take: "nths xs {0..m} = take (Suc m) xs"
   by (metis atLeast0AtMost lessThan_Suc_atMost nths_upt_eq_take)
 
 lemma nths_atLeastLessThan_0_take: "nths xs {0..<m} = take m xs"
   by (simp add: atLeast0LessThan)
 
 lemma nths_atLeastAtMost_prefix: "m \<le> n \<Longrightarrow> nths xs {0..m} \<le> nths xs {0..n}"
   by (simp add: nths_atLeastAtMost_0_take take_prefix)
 
 lemma sorted_nths_atLeastAtMost_0: "\<lbrakk> m \<le> n; sorted (nths xs {0..n}) \<rbrakk> \<Longrightarrow> sorted (nths xs {0..m})"
   using nths_atLeastAtMost_prefix sorted_prefix by blast
 
 lemma sorted_nths_atLeastLessThan_0: "\<lbrakk> m \<le> n; sorted (nths xs {0..<n}) \<rbrakk> \<Longrightarrow> sorted (nths xs {0..<m})"
   by (metis atLeast0LessThan nths_upt_eq_take sorted_prefix take_prefix)
 
 lemma list_augment_as_update: 
   "k < length xs \<Longrightarrow> list_augment xs k x = list_update xs k x"
   by (metis list_augment_def list_augment_idem list_update_overwrite)
 
 lemma nths_list_update_out: "k \<notin> A \<Longrightarrow> nths (list_update xs k x) A = nths xs A"
   apply (induct xs arbitrary: k x A)
    apply (auto)
   apply (rename_tac a xs k x A)
   apply (case_tac k)
    apply (auto simp add: nths_Cons)
   done
 
 lemma nths_list_augment_out: "\<lbrakk> k < length xs; k \<notin> A \<rbrakk> \<Longrightarrow> nths (list_augment xs k x) A = nths xs A"
   by (simp add: list_augment_as_update nths_list_update_out)
 
 end
\ No newline at end of file