diff --git a/thys/Buchi_Complementation/Ranking.thy b/thys/Buchi_Complementation/Ranking.thy
--- a/thys/Buchi_Complementation/Ranking.thy
+++ b/thys/Buchi_Complementation/Ranking.thy
@@ -1,479 +1,478 @@
 section \<open>Rankings\<close>
 
 theory Ranking
 imports
   "Alternate"
   "Graph"
 begin
 
   subsection \<open>Rankings\<close>
 
   type_synonym 'state ranking = "'state node \<Rightarrow> nat"
 
   definition ranking :: "('label, 'state) nba \<Rightarrow> 'label stream \<Rightarrow> 'state ranking \<Rightarrow> bool" where
     "ranking A w f \<equiv>
       (\<forall> v \<in> gunodes A w. f v \<le> 2 * card (nodes A)) \<and>
       (\<forall> v \<in> gunodes A w. \<forall> u \<in> gusuccessors A w v. f u \<le> f v) \<and>
       (\<forall> v \<in> gunodes A w. gaccepting A v \<longrightarrow> even (f v)) \<and>
       (\<forall> v \<in> gunodes A w. \<forall> r k. gurun A w r v \<longrightarrow> smap f (gtrace r v) = sconst k \<longrightarrow> odd k)"
 
   subsection \<open>Ranking Implies Word not in Language\<close>
 
   lemma ranking_stuck:
     assumes "ranking A w f"
     assumes "v \<in> gunodes A w" "gurun A w r v"
     obtains n k
     where "smap f (gtrace (sdrop n r) (gtarget (stake n r) v)) = sconst k"
   proof -
     have 0: "f u \<le> f v" if "v \<in> gunodes A w" "u \<in> gusuccessors A w v" for v u
       using assms(1) that unfolding ranking_def by auto
     have 1: "shd (v ## gtrace r v) \<in> gunodes A w" using assms(2) by auto
     have 2: "sdescending (smap f (v ## gtrace r v))"
     using 1 assms(3)
     proof (coinduction arbitrary: r v rule: sdescending.coinduct)
       case sdescending
       obtain u s where 1: "r = u ## s" using stream.exhaust by blast
       have 2: "v \<in> gunodes A w" using sdescending(1) by simp
       have 3: "gurun A w (u ## s) v" using sdescending(2) 1 by auto
       have 4: "u \<in> gusuccessors A w v" using 3 by auto
       have 5: "u \<in> gureachable A w v" using graph.reachable_successors 4 by blast
       show ?case
       unfolding 1
       proof (intro exI conjI disjI1)
         show "f u \<le> f v" using 0 2 4 by this
         show "shd (u ## gtrace s u) \<in> gunodes A w" using 2 5 by auto
         show "gurun A w s u" using 3 by auto
       qed auto
     qed
-    obtain n k where 3: "sdrop n (smap f (v ## gtrace r v)) = sconst k"
+    obtain s k where 3: "smap f (v ## gtrace r v) = s @- sconst k"
       using sdescending_stuck[OF 2] by metis
-    have "gtrace (sdrop (Suc n) r) (gtarget (stake (Suc n) r) v) = sdrop (Suc n) (gtrace r v)"
+    have "gtrace (sdrop (Suc (length s)) r) (gtarget (stake (Suc (length s)) r) v) = sdrop (Suc (length s)) (gtrace r v)"
       using sscan_sdrop by rule
-    also have "smap f \<dots> = sdrop n (smap f (v ## gtrace r v))"
-      by (auto, metis 3 id_apply sdrop_smap sdrop_stl siterate.simps(2)
-        sscan_const stream.map stream.map_sel(2) stream.sel(2))
-    also have "\<dots> = sconst k" using 3 by this
+    also have "smap f \<dots> = sdrop (length s) (smap f (v ## gtrace r v))"
+      by (metis "3" id_apply sdrop_simps(2) sdrop_smap sdrop_stl shift_eq siterate.simps(2) stream.sel(2))
+    also have "\<dots> = sconst k" unfolding 3 using shift_eq by metis
     finally show ?thesis using that by blast
   qed
 
   lemma ranking_stuck_odd:
     assumes "ranking A w f"
     assumes "v \<in> gunodes A w" "gurun A w r v"
     obtains n
     where "Ball (sset (smap f (gtrace (sdrop n r) (gtarget (stake n r) v)))) odd"
   proof -
     obtain n k where 1: "smap f (gtrace (sdrop n r) (gtarget (stake n r) v)) = sconst k"
       using ranking_stuck assms by this
     have 2: "gtarget (stake n r) v \<in> gunodes A w"
       using assms(2, 3) by (simp add: graph.nodes_target graph.run_stake)
     have 3: "gurun A w (sdrop n r) (gtarget (stake n r) v)"
       using assms(2, 3) by (simp add: graph.run_sdrop)
     have 4: "odd k" using 1 2 3 assms(1) unfolding ranking_def by meson
     have 5: "Ball (sset (smap f (gtrace (sdrop n r) (gtarget (stake n r) v)))) odd"
       unfolding 1 using 4 by simp
     show ?thesis using that 5 by this
   qed
 
   lemma ranking_language:
     assumes "ranking A w f"
     shows "w \<notin> language A"
   proof
     assume 1: "w \<in> language A"
     obtain r p where 2: "run A (w ||| r) p" "p \<in> initial A" "infs (accepting A) (p ## r)" using 1 by rule
     let ?r = "fromN 1 ||| r"
     let ?v = "(0, p)"
     have 3: "?v \<in> gunodes A w" "gurun A w ?r ?v" using 2(1, 2) by (auto intro: run_grun)
 
     obtain n where 4: "Ball (sset (smap f (gtrace (sdrop n ?r) (gtarget (stake n ?r) ?v)))) odd"
       using ranking_stuck_odd assms 3 by this
     let ?s = "stake n ?r"
     let ?t = "sdrop n ?r"
     let ?u = "gtarget ?s ?v"
 
     have "sset (gtrace ?t ?u) \<subseteq> gureachable A w ?v"
     proof (intro graph.reachable_trace graph.reachable_target graph.reachable.reflexive)
       show "gupath A w ?s ?v" using graph.run_stake 3(2) by this
       show "gurun A w ?t ?u" using graph.run_sdrop 3(2) by this
     qed
     also have "\<dots> \<subseteq> gunodes A w" using 3(1) by blast
     finally have 7: "sset (gtrace ?t ?u) \<subseteq> gunodes A w" by this
     have 8: "\<And> p. p \<in> gunodes A w \<Longrightarrow> gaccepting A p \<Longrightarrow> even (f p)"
       using assms unfolding ranking_def by auto
     have 9: "\<And> p. p \<in> sset (gtrace ?t ?u) \<Longrightarrow> gaccepting A p \<Longrightarrow> even (f p)" using 7 8 by auto
 
     have 19: "infs (accepting A) (smap snd ?r)" using 2(3) by simp
     have 18: "infs (gaccepting A) ?r" using 19 by simp
     have 17: "infs (gaccepting A) (gtrace ?r ?v)" using 18 unfolding gtrace_alt_def by this
     have 16: "infs (gaccepting A) (gtrace (?s @- ?t) ?v)" using 17 unfolding stake_sdrop by this
     have 15: "infs (gaccepting A) (gtrace ?t ?u)" using 16 by simp
     have 13: "infs (even \<circ> f) (gtrace ?t ?u)" using infs_mono[OF _ 15] 9 by simp
     have 12: "infs even (smap f (gtrace ?t ?u))" using 13 by (simp add: comp_def)
     have 11: "Bex (sset (smap f (gtrace ?t ?u))) even" using 12 infs_any by metis
 
     show False using 4 11 by auto
   qed
 
   subsection \<open>Word not in Language Implies Ranking\<close>
 
   subsubsection \<open>Removal of Endangered Nodes\<close>
 
   definition clean :: "('label, 'state) nba \<Rightarrow> 'label stream \<Rightarrow> 'state node set \<Rightarrow> 'state node set" where
     "clean A w V \<equiv> {v \<in> V. infinite (greachable A w V v)}"
 
   lemma clean_decreasing: "clean A w V \<subseteq> V" unfolding clean_def by auto
   lemma clean_successors:
     assumes "v \<in> V" "u \<in> gusuccessors A w v"
     shows "u \<in> clean A w V \<Longrightarrow> v \<in> clean A w V"
   proof -
     assume 1: "u \<in> clean A w V"
     have 2: "u \<in> V" "infinite (greachable A w V u)" using 1 unfolding clean_def by auto
     have 3: "u \<in> greachable A w V v" using graph.reachable.execute assms(2) 2(1) by blast
     have 4: "greachable A w V u \<subseteq> greachable A w V v" using 3 by blast
     have 5: "infinite (greachable A w V v)" using 2(2) 4 by (simp add: infinite_super)
     show "v \<in> clean A w V" unfolding clean_def using assms(1) 5 by simp
   qed
 
   subsubsection \<open>Removal of Safe Nodes\<close>
 
   definition prune :: "('label, 'state) nba \<Rightarrow> 'label stream \<Rightarrow> 'state node set \<Rightarrow> 'state node set" where
     "prune A w V \<equiv> {v \<in> V. \<exists> u \<in> greachable A w V v. gaccepting A u}"
 
   lemma prune_decreasing: "prune A w V \<subseteq> V" unfolding prune_def by auto
   lemma prune_successors:
     assumes "v \<in> V" "u \<in> gusuccessors A w v"
     shows "u \<in> prune A w V \<Longrightarrow> v \<in> prune A w V"
   proof -
     assume 1: "u \<in> prune A w V"
     have 2: "u \<in> V" "\<exists> x \<in> greachable A w V u. gaccepting A x" using 1 unfolding prune_def by auto
     have 3: "u \<in> greachable A w V v" using graph.reachable.execute assms(2) 2(1) by blast
     have 4: "greachable A w V u \<subseteq> greachable A w V v" using 3 by blast
     show "v \<in> prune A w V" unfolding prune_def using assms(1) 2(2) 4 by auto
   qed
 
   subsubsection \<open>Run Graph Interation\<close>
 
   definition graph :: "('label, 'state) nba \<Rightarrow> 'label stream \<Rightarrow> nat \<Rightarrow> 'state node set" where
     "graph A w k \<equiv> alternate (clean A w) (prune A w) k (gunodes A w)"
 
   abbreviation "level A w k l \<equiv> {v \<in> graph A w k. fst v = l}"
 
   lemma graph_0[simp]: "graph A w 0 = gunodes A w" unfolding graph_def by simp
   lemma graph_Suc[simp]: "graph A w (Suc k) = (if even k then clean A w else prune A w) (graph A w k)"
     unfolding graph_def by simp
 
   lemma graph_antimono: "antimono (graph A w)"
     using alternate_antimono clean_decreasing prune_decreasing
     unfolding antimono_def le_fun_def graph_def
     by metis
   lemma graph_nodes: "graph A w k \<subseteq> gunodes A w" using graph_0 graph_antimono le0 antimonoD by metis
   lemma graph_successors:
     assumes "v \<in> gunodes A w" "u \<in> gusuccessors A w v"
     shows "u \<in> graph A w k \<Longrightarrow> v \<in> graph A w k"
   using assms
   proof (induct k arbitrary: u v)
     case 0
     show ?case using 0(2) by simp
   next
     case (Suc k)
     have 1: "v \<in> graph A w k" using Suc using antimono_iff_le_Suc graph_antimono rev_subsetD by blast
     show ?case using Suc(2) clean_successors[OF 1 Suc(4)] prune_successors[OF 1 Suc(4)] by auto
   qed
 
   lemma graph_level_finite:
     assumes "finite (nodes A)"
     shows "finite (level A w k l)"
   proof -
     have "level A w k l \<subseteq> {v \<in> gunodes A w. fst v = l}" by (simp add: graph_nodes subset_CollectI)
     also have "{v \<in> gunodes A w. fst v = l} \<subseteq> {l} \<times> nodes A" using gnodes_nodes by force
     also have "finite ({l} \<times> nodes A)" using assms(1) by simp
     finally show ?thesis by this
   qed
 
   lemma find_safe:
     assumes "w \<notin> language A"
     assumes "V \<noteq> {}" "V \<subseteq> gunodes A w"
     assumes "\<And> v. v \<in> V \<Longrightarrow> gsuccessors A w V v \<noteq> {}"
     obtains v
     where "v \<in> V" "\<forall> u \<in> greachable A w V v. \<not> gaccepting A u"
   proof (rule ccontr)
     assume 1: "\<not> thesis"
     have 2: "\<And> v. v \<in> V \<Longrightarrow> \<exists> u \<in> greachable A w V v. gaccepting A u" using that 1 by auto
     have 3: "\<And> r v. v \<in> initial A \<Longrightarrow> run A (w ||| r) v \<Longrightarrow> fins (accepting A) r" using assms(1) by auto
     obtain v where 4: "v \<in> V" using assms(2) by force
     obtain x where 5: "x \<in> greachable A w V v" "gaccepting A x" using 2 4 by blast
     obtain y where 50: "gpath A w V y v" "x = gtarget y v" using 5(1) by rule
     obtain r where 6: "grun A w V r x" "infs (\<lambda> x. x \<in> V \<and> gaccepting A x) r"
     proof (rule graph.recurring_condition)
       show "x \<in> V \<and> gaccepting A x" using greachable_subset 4 5 by blast
     next
       fix v
       assume 1: "v \<in> V \<and> gaccepting A v"
       obtain v' where 20: "v' \<in> gsuccessors A w V v" using assms(4) 1 by (meson IntE equals0I)
       have 21: "v' \<in> V" using 20 by auto
       have 22: "\<exists> u \<in> greachable A w V v'. u \<in> V \<and> gaccepting A u"
         using greachable_subset 2 21 by blast
       obtain r where 30: "gpath A w V r v'" "gtarget r v' \<in> V \<and> gaccepting A (gtarget r v')"
         using 22 by blast
       show "\<exists> r. r \<noteq> [] \<and> gpath A w V r v \<and> gtarget r v \<in> V \<and> gaccepting A (gtarget r v)"
       proof (intro exI conjI)
         show "v' # r \<noteq> []" by simp
         show "gpath A w V (v' # r) v" using 20 30 by auto
         show "gtarget (v' # r) v \<in> V" using 30 by simp
         show "gaccepting A (gtarget (v' # r) v)" using 30 by simp
       qed
     qed auto
     obtain u where 100: "u \<in> ginitial A" "v \<in> gureachable A w u" using 4 assms(3) by blast
     have 101: "gupath A w y v" using gpath_subset 50(1) subset_UNIV by this
     have 102: "gurun A w r x" using grun_subset 6(1) subset_UNIV by this
     obtain t where 103: "gupath A w t u" "v = gtarget t u" using 100(2) by rule
     have 104: "gurun A w (t @- y @- r) u" using 101 102 103 50(2) by auto
     obtain s q where 7: "t @- y @- r = fromN (Suc 0) ||| s" "u = (0, q)"
       using grun_elim[OF 104] 100(1) by blast
     have 8: "run A (w ||| s) q" using grun_run[OF 104[unfolded 7]] by simp
     have 9: "q \<in> initial A" using 100(1) 7(2) by auto
     have 91: "sset (trace (w ||| s) q) \<subseteq> reachable A q"
       using nba.reachable_trace nba.reachable.reflexive 8 by this
     have 10: "fins (accepting A) s" using 3 9 8 by this
     have 12: "infs (gaccepting A) r" using infs_mono[OF _ 6(2)] by simp
     have "s = smap snd (t @- y @- r)" unfolding 7(1) by simp
     also have "infs (accepting A) \<dots>" using 12 by (simp add: comp_def)
     finally have 13: "infs (accepting A) s" by this
     show False using 10 13 by simp
   qed
 
   lemma remove_run:
     assumes "finite (nodes A)" "w \<notin> language A"
     assumes "V \<subseteq> gunodes A w" "clean A w V \<noteq> {}"
     obtains v r
     where
       "grun A w V r v"
       "sset (gtrace r v) \<subseteq> clean A w V"
       "sset (gtrace r v) \<subseteq> - prune A w (clean A w V)"
   proof -
     obtain u where 1: "u \<in> clean A w V" "\<forall> x \<in> greachable A w (clean A w V) u. \<not> gaccepting A x"
     proof (rule find_safe)
       show "w \<notin> language A" using assms(2) by this
       show "clean A w V \<noteq> {}" using assms(4) by this
       show "clean A w V \<subseteq> gunodes A w" using assms(3) by (meson clean_decreasing subset_iff)
     next
       fix v
       assume 1: "v \<in> clean A w V"
       have 2: "v \<in> V" using 1 clean_decreasing by blast
       have 3: "infinite (greachable A w V v)" using 1 clean_def by auto
       have "gsuccessors A w V v \<subseteq> gusuccessors A w v" by auto
       also have "finite \<dots>" using 2 assms(1, 3) finite_nodes_gsuccessors by blast
       finally have 4: "finite (gsuccessors A w V v)" by this
       have 5: "infinite (insert v (\<Union>((greachable A w V) ` (gsuccessors A w V v))))"
         using graph.reachable_step 3 by metis
       obtain u where 6: "u \<in> gsuccessors A w V v" "infinite (greachable A w V u)" using 4 5 by auto
       have 7: "u \<in> clean A w V" using 6 unfolding clean_def by auto
       show "gsuccessors A w (clean A w V) v \<noteq> {}" using 6(1) 7 by auto
     qed auto
     have 2: "u \<in> V" using 1(1) unfolding clean_def by auto
     have 3: "infinite (greachable A w V u)" using 1(1) unfolding clean_def by simp
     have 4: "finite (gsuccessors A w V v)" if "v \<in> greachable A w V u" for v
     proof -
       have 1: "v \<in> V" using that greachable_subset 2 by blast
       have "gsuccessors A w V v \<subseteq> gusuccessors A w v" by auto
       also have "finite \<dots>" using 1 assms(1, 3) finite_nodes_gsuccessors by blast
       finally show ?thesis by this
     qed
     obtain r where 5: "grun A w V r u" using graph.koenig[OF 3 4] by this
     have 6: "greachable A w V u \<subseteq> V" using 2 greachable_subset by blast
     have 7: "sset (gtrace r u) \<subseteq> V"
       using graph.reachable_trace[OF graph.reachable.reflexive 5(1)] 6 by blast
     have 8: "sset (gtrace r u) \<subseteq> clean A w V"
       unfolding clean_def using 7 infinite_greachable_gtrace[OF 5(1)] by auto
     have 9: "sset (gtrace r u) \<subseteq> greachable A w (clean A w V) u"
       using 5 8 by (metis graph.reachable.reflexive graph.reachable_trace grun_subset)
     show ?thesis
     proof
       show "grun A w V r u" using 5(1) by this
       show "sset (gtrace r u) \<subseteq> clean A w V" using 8 by this
       show "sset (gtrace r u) \<subseteq> - prune A w (clean A w V)"
       proof (intro subsetI ComplI)
         fix p
         assume 10: "p \<in> sset (gtrace r u)" "p \<in> prune A w (clean A w V)"
         have 20: "\<exists> x \<in> greachable A w (clean A w V) p. gaccepting A x"
           using 10(2) unfolding prune_def by auto
         have 30: "greachable A w (clean A w V) p \<subseteq> greachable A w (clean A w V) u"
           using 10(1) 9 by blast
         show "False" using 1(2) 20 30 by force
       qed
     qed
   qed
 
   lemma level_bounded:
     assumes "finite (nodes A)" "w \<notin> language A"
     obtains n
     where "\<And> l. l \<ge> n \<Longrightarrow> card (level A w (2 * k) l) \<le> card (nodes A) - k"
   proof (induct k arbitrary: thesis)
     case (0)
     show ?case
     proof (rule 0)
       fix l :: nat
       have "finite ({l} \<times> nodes A)" using assms(1) by simp
       also have "level A w 0 l \<subseteq> {l} \<times> nodes A" using gnodes_nodes by force
       also (card_mono) have "card \<dots> = card (nodes A)" using assms(1) by simp
       finally show "card (level A w (2 * 0) l) \<le> card (nodes A) - 0" by simp
     qed
   next
     case (Suc k)
     show ?case
     proof (cases "graph A w (Suc (2 * k)) = {}")
       case True
       have 3: "graph A w (2 * Suc k) = {}" using True prune_decreasing by simp blast
       show ?thesis using Suc(2) 3 by simp
     next
       case False
       obtain v r where 1:
         "grun A w (graph A w (2 * k)) r v"
         "sset (gtrace r v) \<subseteq> graph A w (Suc (2 * k))"
         "sset (gtrace r v) \<subseteq> - graph A w (Suc (Suc (2 * k)))"
       proof (rule remove_run)
         show "finite (nodes A)" "w \<notin> language A" using assms by this
         show "clean A w (graph A w (2 * k)) \<noteq> {}" using False by simp
         show "graph A w (2 * k) \<subseteq> gunodes A w" using graph_nodes by this
       qed auto
       obtain l q where 2: "v = (l, q)" by force
       obtain n where 90: "\<And> l. n \<le> l \<Longrightarrow> card (level A w (2 * k) l) \<le> card (nodes A) - k"
         using Suc(1) by blast
       show ?thesis
       proof (rule Suc(2))
         fix j
         assume 100: "n + Suc l \<le> j"
         have 6: "graph A w (Suc (Suc (2 * k))) \<subseteq> graph A w (Suc (2 * k))"
           using graph_antimono antimono_iff_le_Suc by blast
         have 101: "gtrace r v !! (j - Suc l) \<in> graph A w (Suc (2 * k))" using 1(2) snth_sset by auto
         have 102: "gtrace r v !! (j - Suc l) \<notin> graph A w (Suc (Suc (2 * k)))" using 1(3) snth_sset by blast
         have 103: "gtrace r v !! (j - Suc l) \<in> level A w (Suc (2 * k)) j"
           using 1(1) 100 101 2 by (auto elim: grun_elim)
         have 104: "gtrace r v !! (j - Suc l) \<notin> level A w (Suc (Suc (2 * k))) j" using 100 102 by simp
         have "level A w (2 * Suc k) j = level A w (Suc (Suc (2 * k))) j" by simp
         also have "\<dots> \<subset> level A w (Suc (2 * k)) j" using 103 104 6 by blast
         also have "\<dots> \<subseteq> level A w (2 * k) j" by (simp add: Collect_mono clean_def)
         finally have 105: "level A w (2 * Suc k) j \<subset> level A w (2 * k) j" by this
         have "card (level A w (2 * Suc k) j) < card (level A w (2 * k) j)"
           using assms(1) 105 by (simp add: graph_level_finite psubset_card_mono)
         also have "\<dots> \<le> card (nodes A) - k" using 90 100 by simp
         finally show "card (level A w (2 * Suc k) j) \<le> card (nodes A) - Suc k" by simp
       qed
     qed
   qed
   lemma graph_empty:
     assumes "finite (nodes A)" "w \<notin> language A"
     shows "graph A w (Suc (2 * card (nodes A))) = {}"
   proof -
     obtain n where 1: "\<And> l. l \<ge> n \<Longrightarrow> card (level A w (2 * card (nodes A)) l) = 0"
       using level_bounded[OF assms(1, 2), of "card (nodes A)"] by auto
     have "graph A w (2 * card (nodes A)) =
       (\<Union> l \<in> {..< n}. level A w (2 * card (nodes A)) l) \<union>
       (\<Union> l \<in> {n ..}. level A w (2 * card (nodes A)) l)"
       by auto
     also have "(\<Union> l \<in> {n ..}. level A w (2 * card (nodes A)) l) = {}"
       using graph_level_finite assms(1) 1 by fastforce
     also have "finite ((\<Union> l \<in> {..< n}. level A w (2 * card (nodes A)) l) \<union> {})"
       using graph_level_finite assms(1) by auto
     finally have 100: "finite (graph A w (2 * card (nodes A)))" by this
     have 101: "finite (greachable A w (graph A w (2 * card (nodes A))) v)" for v
       using 100 greachable_subset[of A w "graph A w (2 * card (nodes A))" v]
       using finite_insert infinite_super by auto
     show ?thesis using 101 by (simp add: clean_def)
   qed
   lemma graph_le:
     assumes "finite (nodes A)" "w \<notin> language A"
     assumes "v \<in> graph A w k"
     shows "k \<le> 2 * card (nodes A)"
     using graph_empty graph_antimono assms
     by (metis (no_types, lifting) Suc_leI antimono_def basic_trans_rules(30) empty_iff not_le_imp_less)
 
   subsection \<open>Node Ranks\<close>
 
   definition rank :: "('label, 'state) nba \<Rightarrow> 'label stream \<Rightarrow> 'state node \<Rightarrow> nat" where
     "rank A w v \<equiv> GREATEST k. v \<in> graph A w k"
 
   lemma rank_member:
     assumes "finite (nodes A)" "w \<notin> language A" "v \<in> gunodes A w"
     shows "v \<in> graph A w (rank A w v)"
   unfolding rank_def
   proof (rule GreatestI_nat)
     show "v \<in> graph A w 0" using assms(3) by simp
     show "k \<le> 2 * card (nodes A)" if "v \<in> graph A w k" for k
       using graph_le assms(1, 2) that by blast
   qed
   lemma rank_removed:
     assumes "finite (nodes A)" "w \<notin> language A"
     shows "v \<notin> graph A w (Suc (rank A w v))"
   proof
     assume "v \<in> graph A w (Suc (rank A w v))"
     then have 2: "Suc (rank A w v) \<le> rank A w v"
       unfolding rank_def using Greatest_le_nat graph_le assms by metis
     then show "False" by auto
   qed
   lemma rank_le:
     assumes "finite (nodes A)" "w \<notin> language A"
     assumes "v \<in> gunodes A w" "u \<in> gusuccessors A w v"
     shows "rank A w u \<le> rank A w v"
   unfolding rank_def
   proof (rule Greatest_le_nat)
     have 1: "u \<in> gureachable A w v" using graph.reachable_successors assms(4) by blast
     have 2: "u \<in> gunodes A w" using assms(3) 1 by auto
     show "v \<in> graph A w (GREATEST k. u \<in> graph A w k)"
     unfolding rank_def[symmetric]
     proof (rule graph_successors)
       show "v \<in> gunodes A w" using assms(3) by this
       show "u \<in> gusuccessors A w v" using assms(4) by this
       show "u \<in> graph A w (rank A w u)" using rank_member assms(1, 2) 2 by this
     qed
     show "k \<le> 2 * card (nodes A)" if "v \<in> graph A w k" for k
       using graph_le assms(1, 2) that by blast
   qed
 
   lemma language_ranking:
     assumes "finite (nodes A)" "w \<notin> language A"
     shows "ranking A w (rank A w)"
   unfolding ranking_def
   proof (intro conjI ballI allI impI)
     fix v
     assume 1: "v \<in> gunodes A w"
     have 2: "v \<in> graph A w (rank A w v)" using rank_member assms 1 by this
     show "rank A w v \<le> 2 * card (nodes A)" using graph_le assms 2 by this
   next
     fix v u
     assume 1: "v \<in> gunodes A w" "u \<in> gusuccessors A w v"
     show "rank A w u \<le> rank A w v" using rank_le assms 1 by this
   next
     fix v
     assume 1: "v \<in> gunodes A w" "gaccepting A v"
     have 2: "v \<in> graph A w (rank A w v)" using rank_member assms 1(1) by this
     have 3: "v \<notin> graph A w (Suc (rank A w v))" using rank_removed assms by this
     have 4: "v \<in> prune A w (graph A w (rank A w v))" using 2 1(2) unfolding prune_def by auto
     have 5: "graph A w (Suc (rank A w v)) \<noteq> prune A w (graph A w (rank A w v))" using 3 4 by blast
     show "even (rank A w v)" using 5 by auto
   next
     fix v r k
     assume 1: "v \<in> gunodes A w" "gurun A w r v" "smap (rank A w) (gtrace r v) = sconst k"
     have "sset (gtrace r v) \<subseteq> gureachable A w v"
       using 1(2) by (metis graph.reachable.reflexive graph.reachable_trace)
     then have 6: "sset (gtrace r v) \<subseteq> gunodes A w" using 1(1) by blast
     have 60: "rank A w ` sset (gtrace r v) \<subseteq> {k}"
       using 1(3) by (metis equalityD1 sset_sconst stream.set_map)
     have 50: "sset (gtrace r v) \<subseteq> graph A w k"
       using rank_member[OF assms] subsetD[OF 6] 60 unfolding image_subset_iff by auto
     have 70: "grun A w (graph A w k) r v" using grun_subset 1(2) 50 by this
     have 7: "sset (gtrace r v) \<subseteq> clean A w (graph A w k)"
       unfolding clean_def using 50 infinite_greachable_gtrace[OF 70] by auto
     have 8: "sset (gtrace r v) \<inter> graph A w (Suc k) = {}" using rank_removed[OF assms] 60 by blast
     have 9: "sset (gtrace r v) \<noteq> {}" using stream.set_sel(1) by auto
     have 10: "graph A w (Suc k) \<noteq> clean A w (graph A w k)" using 7 8 9 by blast
     show "odd k" using 10 unfolding graph_Suc by auto
   qed
 
   subsection \<open>Correctness Theorem\<close>
 
   theorem language_ranking_iff:
     assumes "finite (nodes A)"
     shows "w \<notin> language A \<longleftrightarrow> (\<exists> f. ranking A w f)"
     using ranking_language language_ranking assms by blast
 
 end
diff --git a/thys/Transition_Systems_and_Automata/Basic/Degeneralization.thy b/thys/Transition_Systems_and_Automata/Basic/Degeneralization.thy
--- a/thys/Transition_Systems_and_Automata/Basic/Degeneralization.thy
+++ b/thys/Transition_Systems_and_Automata/Basic/Degeneralization.thy
@@ -1,230 +1,230 @@
 theory Degeneralization
 imports
   Acceptance
   Sequence_Zip
 begin
 
   type_synonym 'a degen = "'a \<times> nat"
 
   definition degen :: "'a pred gen \<Rightarrow> 'a degen pred" where
     "degen cs \<equiv> \<lambda> (a, k). k \<ge> length cs \<or> (cs ! k) a"
 
   lemma degen_simps[iff]: "degen cs (a, k) \<longleftrightarrow> k \<ge> length cs \<or> (cs ! k) a" unfolding degen_def by simp
 
   definition count :: "'a pred gen \<Rightarrow> 'a \<Rightarrow> nat \<Rightarrow> nat" where
     "count cs a k \<equiv>
       if k < length cs
       then if (cs ! k) a then Suc k mod length cs else k
       else if cs = [] then k else 0"
 
   lemma count_empty[simp]: "count [] a k = k" unfolding count_def by simp
   lemma count_nonempty[simp]: "cs \<noteq> [] \<Longrightarrow> count cs a k < length cs" unfolding count_def by simp
   lemma count_constant_1:
     assumes "k < length cs"
     assumes "\<And> a. a \<in> set w \<Longrightarrow> \<not> (cs ! k) a"
     shows "fold (count cs) w k = k"
     using assms unfolding count_def by (induct w) (auto)
   lemma count_constant_2:
     assumes "k < length cs"
     assumes "\<And> a. a \<in> set (w || k # scan (count cs) w k) \<Longrightarrow> \<not> degen cs a"
     shows "fold (count cs) w k = k"
     using assms unfolding count_def by (induct w) (auto)
   lemma count_step:
     assumes "k < length cs"
     assumes "(cs ! k) a"
     shows "count cs a k = Suc k mod length cs"
     using assms unfolding count_def by simp
 
   lemma degen_skip_condition:
     assumes "k < length cs"
     assumes "infs (degen cs) (w ||| k ## sscan (count cs) w k)"
     obtains u a v
     where "w = u @- a ## v" "fold (count cs) u k = k" "(cs ! k) a"
   proof -
     have 1: "Collect (degen cs) \<inter> sset (w ||| k ## sscan (count cs) w k) \<noteq> {}"
       using infs_any assms(2) by auto
     obtain ys x zs where 2:
       "w ||| k ## sscan (count cs) w k = ys @- x ## zs"
       "Collect (degen cs) \<inter> set ys = {}"
       "x \<in> Collect (degen cs)"
       using split_stream_first 1 by this
     define u where "u \<equiv> stake (length ys) w"
     define a where "a \<equiv> w !! length ys"
     define v where "v \<equiv> sdrop (Suc (length ys)) w"
     have "ys = stake (length ys) (w ||| k ## sscan (count cs) w k)" using shift_eq 2(1) by auto
     also have "\<dots> = stake (length ys) w || stake (length ys) (k ## sscan (count cs) w k)" by simp
     also have "\<dots> = take (length ys) u || take (length ys) (k # scan (count cs) u k)"
       unfolding u_def
       using append_eq_conv_conj length_stake length_zip stream.sel
       using sscan_stake stake.simps(2) stake_Suc stake_szip take_stake
       by metis
     also have "\<dots> = take (length ys) (u || k # scan (count cs) u k)" using take_zip by rule
     also have "\<dots> = u || k # scan (count cs) u k" unfolding u_def by simp
     finally have 3: "ys = u || k # scan (count cs) u k" by this
     have "x = (w ||| k ## sscan (count cs) w k) !! length ys" unfolding 2(1) by simp
     also have "\<dots> = (w !! length ys, (k ## sscan (count cs) w k) !! length ys)" by simp
     also have "\<dots> = (a, fold (count cs) u k)" unfolding u_def a_def by simp
     finally have 4: "x = (a, fold (count cs) u k)" by this
     have 5: "fold (count cs) u k = k" using count_constant_2 assms(1) 2(2) unfolding 3 by blast
     show ?thesis
     proof
       show "w = u @- a ## v" unfolding u_def a_def v_def using id_stake_snth_sdrop by this
       show "fold (count cs) u k = k" using 5 by this
       show "(cs ! k) a" using assms(1) 2(3) unfolding 4 5 by simp
     qed
   qed
   lemma degen_skip_arbitrary:
     assumes "k < length cs" "l < length cs"
     assumes "infs (degen cs) (w ||| k ## sscan (count cs) w k)"
     obtains u v
     where "w = u @- v" "fold (count cs) u k = l"
   using assms
   proof (induct "nat ((int l - int k) mod length cs)" arbitrary: l thesis)
     case (0)
     have 1: "length cs > 0" using assms(1) by auto
     have 2: "(int l - int k) mod length cs = 0" using 0(1) 1 by (auto intro: antisym)
     have 3: "int l mod length cs = int k mod length cs" using mod_eq_dvd_iff 2 by force
     have 4: "k = l" using 0(3, 4) 3 by simp
     show ?case
     proof (rule 0(2))
       show "w = [] @- w" by simp
       show "fold (count cs) [] k = l" using 4 by simp
     qed
   next
     case (Suc n)
     have 1: "length cs > 0" using assms(1) by auto
     define l' where "l' = nat ((int l - 1) mod length cs)"
     obtain u v where 2: "w = u @- v" "fold (count cs) u k = l'"
     proof (rule Suc(1))
       have 2: "Suc n < length cs" using nat_less_iff Suc(2) 1 by simp
       have "n = nat (int n)" by simp
       also have "int n = (int (Suc n) - 1) mod length cs" using 2 by simp
       also have "\<dots> = (int l - int k - 1) mod length cs" using Suc(2) by (simp add: mod_simps)
       also have "\<dots> = (int l - 1 - int k) mod length cs" by (simp add: algebra_simps)
       also have "\<dots> = (int l' - int k) mod length cs" using l'_def 1 by (simp add: mod_simps)
       finally show "n = nat ((int l' - int k) mod length cs)" by this
       show "k < length cs" using Suc(4) by this
       show "l' < length cs" using nat_less_iff l'_def 1 by simp
       show "infs (degen cs) (w ||| k ## sscan (count cs) w k)" using Suc(6) by this
     qed
     have 3: "l' < length cs" using nat_less_iff l'_def 1 by simp
     have 4: "v ||| l' ## sscan (count cs) v l' = sdrop (length u) (w ||| k ## sscan (count cs) w k)"
       using 2 eq_scons eq_shift
       by (metis sdrop.simps(2) sdrop_simps sdrop_szip sscan_scons_snth sscan_sdrop stream.sel(2))
     have 5: "infs (degen cs) (v ||| l' ## sscan (count cs) v l')" using Suc(6) unfolding 4 by blast
     obtain vu a vv where 6: "v = vu @- a ## vv" "fold (count cs) vu l' = l'" "(cs ! l') a"
       using degen_skip_condition 3 5 by this
     have "l = nat (int l)" by simp
     also have "int l = int l mod length cs" using Suc(5) by simp
     also have "\<dots> = int (Suc l') mod length cs" using l'_def 1 by (simp add: mod_simps)
     finally have 7: "l = Suc l' mod length cs" using nat_mod_as_int by metis
     show ?case
     proof (rule Suc(3))
       show "w = (u @ vu @ [a]) @- vv" unfolding 2(1) 6(1) by simp
       show "fold (count cs) (u @ vu @ [a]) k = l" using 2(2) 3 6(2, 3) 7 count_step by simp
     qed
   qed
   lemma degen_skip_arbitrary_condition:
     assumes "l < length cs"
     assumes "infs (degen cs) (w ||| k ## sscan (count cs) w k)"
     obtains u a v
     where "w = u @- a ## v" "fold (count cs) u k = l" "(cs ! l) a"
   proof -
     have 0: "cs \<noteq> []" using assms(1) by auto
     have 1: "count cs (shd w) k < length cs" using 0 by simp
     have 2: "infs (degen cs) (stl w ||| count cs (shd w) k ## sscan (count cs) (stl w) (count cs (shd w) k))"
       using assms(2) by (metis alw.cases sscan.code stream.sel(2) szip.simps(2))
     obtain u v where 3: "stl w = u @- v" "fold (count cs) u (count cs (shd w) k) = l"
       using degen_skip_arbitrary 1 assms(1) 2 by this
     have 4: "v ||| l ## sscan (count cs) v l =
       sdrop (length u) (stl w ||| count cs (shd w) k ## sscan (count cs) (stl w) (count cs (shd w) k))"
       using 3 eq_scons eq_shift
       by (metis sdrop.simps(2) sdrop_simps sdrop_szip sscan_scons_snth sscan_sdrop stream.sel(2))
     have 5: "infs (degen cs) (v ||| l ## sscan (count cs) v l)" using 2 unfolding 4 by blast
     obtain vu a vv where 6: "v = vu @- a ## vv" "fold (count cs) vu l = l" "(cs ! l) a"
       using degen_skip_condition assms(1) 5 by this
     show ?thesis
     proof
       show "w = (shd w # u @ vu) @- a ## vv" using 3(1) 6(1) by (simp add: eq_scons)
       show "fold (count cs) (shd w # u @ vu) k = l" using 3(2) 6(2) by simp
       show "(cs ! l) a" using 6(3) by this
     qed
   qed
   lemma gen_degen_step:
     assumes "gen infs cs w"
     obtains u a v
     where "w = u @- a ## v" "degen cs (a, fold (count cs) u k)"
   proof (cases "k < length cs")
     case True
     have 1: "infs (cs ! k) w" using assms True by auto
     have 2: "{a. (cs ! k) a} \<inter> sset w \<noteq> {}" using infs_any 1 by auto
     obtain u a v where 3: "w = u @- a ## v" "{a. (cs ! k) a} \<inter> set u = {}" "a \<in> {a. (cs ! k) a}"
       using split_stream_first 2 by this
     have 4: "fold (count cs) u k = k" using count_constant_1 True 3(2) by auto
     show ?thesis using 3(1, 3) 4 that by simp
   next
     case False
     show ?thesis
     proof
       show "w = [] @- shd w ## stl w" by simp
       show "degen cs (shd w, fold (count cs) [] k)" using False by simp
     qed
   qed
 
   lemma degen_infs[iff]: "infs (degen cs) (w ||| k ## sscan (count cs) w k) \<longleftrightarrow> gen infs cs w"
   proof
     show "gen infs cs w" if "infs (degen cs) (w ||| k ## sscan (count cs) w k)"
     proof
       fix c
       assume 1: "c \<in> set cs"
       obtain l where 2: "c = cs ! l" "l < length cs" using in_set_conv_nth 1 by metis
       show "infs c w"
       using that unfolding 2(1)
-      proof (coinduction arbitrary: w k rule: infs_set_coinduct)
-        case (infs_set w k)
+      proof (coinduction arbitrary: w k rule: infs_coinduct_shift)
+        case (infs w k)
         obtain u a v where 3: "w = u @- a ## v" "(cs ! l) a"
-          using degen_skip_arbitrary_condition 2(2) infs_set by this
+          using degen_skip_arbitrary_condition 2(2) infs by this
         let ?k = "fold (count cs) u k"
         let ?l = "fold (count cs) (u @ [a]) k"
         have 4: "a ## v ||| ?k ## sscan (count cs) (a ## v) ?k =
           sdrop (length u) (w ||| k ## sscan (count cs) w k)"
           using 3(1) eq_shift scons_eq
           by (metis sdrop_simps(1) sdrop_stl sdrop_szip sscan_scons_snth sscan_sdrop stream.sel(2))
         have 5: "infs (degen cs) (a ## v ||| ?k ## sscan (count cs) (a ## v) ?k)"
-          using infs_set unfolding 4 by blast
+          using infs unfolding 4 by blast
         show ?case
         proof (intro exI conjI bexI)
           show "w = (u @ [a]) @- v" "(cs ! l) a" "a \<in> set (u @ [a])" "v = v" using 3 by auto
           show "infs (degen cs) (v ||| ?l ## sscan (count cs) v ?l)" using 5 by simp
         qed
       qed
     qed
     show "infs (degen cs) (w ||| k ## sscan (count cs) w k)" if "gen infs cs w"
     using that
-    proof (coinduction arbitrary: w k rule: infs_set_coinduct)
-      case (infs_set w k)
+    proof (coinduction arbitrary: w k rule: infs_coinduct_shift)
+      case (infs w k)
       obtain u a v where 1: "w = u @- a ## v" "degen cs (a, fold (count cs) u k)"
-        using gen_degen_step infs_set by this
+        using gen_degen_step infs by this
       let ?u = "u @ [a] || k # scan (count cs) u k"
       let ?l = "fold (count cs) (u @ [a]) k"
       show ?case
       proof (intro exI conjI bexI)
         have "w ||| k ## sscan (count cs) w k =
           (u @ [a]) @- v ||| k ## scan (count cs) u k @- ?l ## sscan (count cs) v ?l"
           unfolding 1(1) by simp
         also have "\<dots> = ?u @- (v ||| ?l ## sscan (count cs) v ?l)"
           by (metis length_Cons length_append_singleton scan_length shift.simps(2) szip_shift)
         finally show "w ||| k ## sscan (count cs) w k = ?u @- (v ||| ?l ## sscan (count cs) v ?l)" by this
         show "degen cs (a, fold (count cs) u k)" using 1(2) by this
         have "(a, fold (count cs) u k) = (last (u @ [a]), last (k # scan (count cs) u k))"
           unfolding scan_last by simp
         also have "\<dots> = last ?u" by (simp add: zip_eq_Nil_iff)
         also have "\<dots> \<in> set ?u" by (fastforce intro: last_in_set simp: zip_eq_Nil_iff)
         finally show "(a, fold (count cs) u k) \<in> set ?u" by this
         show "v ||| ?l ## sscan (count cs) v ?l = v ||| ?l ## sscan (count cs) v ?l" by rule
-        show "gen infs cs v" using infs_set unfolding 1(1) by auto
+        show "gen infs cs v" using infs unfolding 1(1) by auto
       qed
     qed
   qed
 
 end
diff --git a/thys/Transition_Systems_and_Automata/Basic/Sequence.thy b/thys/Transition_Systems_and_Automata/Basic/Sequence.thy
--- a/thys/Transition_Systems_and_Automata/Basic/Sequence.thy
+++ b/thys/Transition_Systems_and_Automata/Basic/Sequence.thy
@@ -1,470 +1,491 @@
 section \<open>Finite and Infinite Sequences\<close>
 
 theory Sequence
 imports
   "Basic"
   "HOL-Library.Stream"
   "HOL-Library.Monad_Syntax"
 begin
 
   subsection \<open>List Basics\<close>
 
   declare upt_Suc[simp del]
   declare last.simps[simp del]
   declare butlast.simps[simp del]
   declare Cons_nth_drop_Suc[simp]
   declare list.pred_True[simp]
 
   lemma list_pred_cases:
     assumes "list_all P xs"
     obtains (nil) "xs = []" | (cons) y ys where "xs = y # ys" "P y" "list_all P ys"
     using assms by (cases xs) (auto)
 
   lemma lists_iff_set: "w \<in> lists A \<longleftrightarrow> set w \<subseteq> A" by auto
 
   lemma fold_const: "fold const xs a = last (a # xs)"
     by (induct xs arbitrary: a) (auto simp: last.simps)
 
   lemma take_Suc: "take (Suc n) xs = (if xs = [] then [] else hd xs # take n (tl xs))"
     by (simp add: take_Suc)
 
   lemma bind_map[simp]: "map f xs \<bind> g = xs \<bind> g \<circ> f" unfolding List.bind_def by simp
 
   lemma ball_bind[iff]: "Ball (set (xs \<bind> f)) P \<longleftrightarrow> (\<forall> x \<in> set xs. \<forall> y \<in> set (f x). P y)"
     unfolding set_list_bind by simp
   lemma bex_bind[iff]: "Bex (set (xs \<bind> f)) P \<longleftrightarrow> (\<exists> x \<in> set xs. \<exists> y \<in> set (f x). P y)"
     unfolding set_list_bind by simp
 
   lemma list_choice: "list_all (\<lambda> x. \<exists> y. P x y) xs \<longleftrightarrow> (\<exists> ys. list_all2 P xs ys)"
     by (induct xs) (auto simp: list_all2_Cons1)
 
   lemma listset_member: "ys \<in> listset XS \<longleftrightarrow> list_all2 (\<in>) ys XS"
     by (induct XS arbitrary: ys) (auto simp: set_Cons_def list_all2_Cons2)
   lemma listset_empty[iff]: "listset XS = {} \<longleftrightarrow> \<not> list_all (\<lambda> A. A \<noteq> {}) XS"
     by (induct XS) (auto simp: set_Cons_def)
   lemma listset_finite[iff]:
     assumes "list_all (\<lambda> A. A \<noteq> {}) XS"
     shows "finite (listset XS) \<longleftrightarrow> list_all finite XS"
   using assms
   proof (induct XS)
     case Nil
     show ?case by simp
   next
     case (Cons A XS)
     note [simp] = finite_image_iff finite_cartesian_product_iff
     have "listset (A # XS) = case_prod Cons ` (A \<times> listset XS)" by (auto simp: set_Cons_def)
     also have "finite \<dots> \<longleftrightarrow> finite (A \<times> listset XS)" by (simp add: inj_on_def)
     also have "\<dots> \<longleftrightarrow> finite A \<and> finite (listset XS)" using Cons(2) by simp
     also have "finite (listset XS) \<longleftrightarrow> list_all finite XS" using Cons by simp
     also have "finite A \<and> \<dots> \<longleftrightarrow> list_all finite (A # XS)" by simp
     finally show ?case by this
   qed
   lemma listset_finite'[intro]:
     assumes "list_all finite XS"
     shows "finite (listset XS)"
     using infinite_imp_nonempty assms by blast
   lemma listset_card[simp]: "card (listset XS) = prod_list (map card XS)"
   proof (induct XS)
     case Nil
     show ?case by simp
   next
     case (Cons A XS)
     have 1: "inj (case_prod Cons)" unfolding inj_def by simp
     have "listset (A # XS) = case_prod Cons ` (A \<times> listset XS)" by (auto simp: set_Cons_def)
     also have "card \<dots> = card (A \<times> listset XS)" using card_image 1 by auto
     also have "\<dots> = card A * card (listset XS)" using card_cartesian_product by this
     also have "card (listset XS) = prod_list (map card XS)" using Cons by this
     also have "card A * \<dots> = prod_list (map card (A # XS))" by simp
     finally show ?case by this
   qed
 
   subsection \<open>Stream Basics\<close>
 
   declare stream.map_id[simp]
   declare stream.set_map[simp]
   declare stream.set_sel(1)[intro!, simp]
   declare stream.pred_True[simp]
   declare stream.pred_map[iff]
   declare stream.rel_map[iff]
   declare shift_simps[simp del]
   declare stake_sdrop[simp]
   declare stake_siterate[simp del]
   declare sdrop_snth[simp]
 
   lemma stream_pred_cases:
     assumes "pred_stream P xs"
     obtains (scons) y ys where "xs = y ## ys" "P y" "pred_stream P ys"
     using assms by (cases xs) (auto)
 
   lemma stream_rel_coinduct[case_names stream_rel, coinduct pred: stream_all2]:
     assumes "R u v"
     assumes "\<And> a u b v. R (a ## u) (b ## v) \<Longrightarrow> P a b \<and> R u v"
     shows "stream_all2 P u v"
     using assms by (coinduct) (metis stream.collapse)
   lemma stream_rel_coinduct_shift[case_names stream_rel, consumes 1]:
     assumes "R u v"
     assumes "\<And> u v. R u v \<Longrightarrow>
       \<exists> u\<^sub>1 u\<^sub>2 v\<^sub>1 v\<^sub>2. u = u\<^sub>1 @- u\<^sub>2 \<and> v = v\<^sub>1 @- v\<^sub>2 \<and> u\<^sub>1 \<noteq> [] \<and> v\<^sub>1 \<noteq> [] \<and> list_all2 P u\<^sub>1 v\<^sub>1 \<and> R u\<^sub>2 v\<^sub>2"
     shows "stream_all2 P u v"
   proof -
     have "\<exists> u\<^sub>1 u\<^sub>2 v\<^sub>1 v\<^sub>2. u = u\<^sub>1 @- u\<^sub>2 \<and> v = v\<^sub>1 @- v\<^sub>2 \<and> list_all2 P u\<^sub>1 v\<^sub>1 \<and> R u\<^sub>2 v\<^sub>2"
       using assms(1) by force
     then show ?thesis using assms(2) by (coinduct) (force elim: list.rel_cases)
   qed
 
   lemma stream_pred_coinduct[case_names stream_pred, coinduct pred: pred_stream]:
     assumes "R w"
     assumes "\<And> a w. R (a ## w) \<Longrightarrow> P a \<and> R w"
     shows "pred_stream P w"
     using assms unfolding stream.pred_rel eq_onp_def by (coinduction arbitrary: w) (auto)
   lemma stream_pred_coinduct_shift[case_names stream_pred, consumes 1]:
     assumes "R w"
     assumes "\<And> w. R w \<Longrightarrow> \<exists> u v. w = u @- v \<and> u \<noteq> [] \<and> list_all P u \<and> R v"
     shows "pred_stream P w"
   proof -
     have "\<exists> u v. w = u @- v \<and> list_all P u \<and> R v"
       using assms(1) by (metis list_all_simps(2) shift.simps(1))
     then show ?thesis using assms(2) by (coinduct) (force elim: list_pred_cases)
   qed
   lemma stream_pred_flat_coinduct[case_names stream_pred, consumes 1]:
     assumes "R ws"
     assumes "\<And> w ws. R (w ## ws) \<Longrightarrow> w \<noteq> [] \<and> list_all P w \<and> R ws"
     shows "pred_stream P (flat ws)"
     using assms
     by (coinduction arbitrary: ws rule: stream_pred_coinduct_shift) (metis stream.exhaust flat_Stream)
 
   lemmas stream_eq_coinduct[case_names stream_eq, coinduct pred: HOL.eq] =
     stream_rel_coinduct[where ?P = HOL.eq, unfolded stream.rel_eq]
   lemmas stream_eq_coinduct_shift[case_names stream_eq, consumes 1] =
     stream_rel_coinduct_shift[where ?P = HOL.eq, unfolded stream.rel_eq list.rel_eq]
 
   lemma stream_pred_shift[iff]: "pred_stream P (u @- v) \<longleftrightarrow> list_all P u \<and> pred_stream P v"
     by (induct u) (auto)
   lemma stream_rel_shift[iff]:
     assumes "length u\<^sub>1 = length v\<^sub>1"
     shows "stream_all2 P (u\<^sub>1 @- u\<^sub>2) (v\<^sub>1 @- v\<^sub>2) \<longleftrightarrow> list_all2 P u\<^sub>1 v\<^sub>1 \<and> stream_all2 P u\<^sub>2 v\<^sub>2"
     using assms by (induct rule: list_induct2) (auto)
 
   lemma sset_subset_stream_pred: "sset w \<subseteq> A \<longleftrightarrow> pred_stream (\<lambda> a. a \<in> A) w"
     unfolding stream.pred_set by auto
 
   lemma eq_scons: "w = a ## v \<longleftrightarrow> a = shd w \<and> v = stl w" by auto
   lemma scons_eq: "a ## v = w \<longleftrightarrow> shd w = a \<and> stl w = v" by auto
   lemma eq_shift: "w = u @- v \<longleftrightarrow> stake (length u) w = u \<and> sdrop (length u) w = v"
     by (induct u arbitrary: w) (force+)
   lemma shift_eq: "u @- v = w \<longleftrightarrow> u = stake (length u) w \<and> v = sdrop (length u) w"
     by (induct u arbitrary: w) (force+)
   lemma scons_eq_shift: "a ## w = u @- v \<longleftrightarrow> ([] = u \<and> a ## w = v) \<or> (\<exists> u'. a # u' = u \<and> w = u' @- v)"
     by (cases u) (auto)
   lemma shift_eq_scons: "u @- v = a ## w \<longleftrightarrow> (u = [] \<and> v = a ## w) \<or> (\<exists> u'. u = a # u' \<and> u' @- v = w)"
     by (cases u) (auto)
 
   lemma stream_all2_sset1:
     assumes "stream_all2 P xs ys"
     shows "\<forall> x \<in> sset xs. \<exists> y \<in> sset ys. P x y"
   proof -
     have "pred_stream (\<lambda> x. \<exists> y \<in> S. P x y) xs" if "sset ys \<subseteq> S" for S
       using assms that by (coinduction arbitrary: xs ys) (force elim: stream.rel_cases)
     then show ?thesis unfolding stream.pred_set by auto
   qed
   lemma stream_all2_sset2:
     assumes "stream_all2 P xs ys"
     shows "\<forall> y \<in> sset ys. \<exists> x \<in> sset xs. P x y"
   proof -
     have "pred_stream (\<lambda> y. \<exists> x \<in> S. P x y) ys" if "sset xs \<subseteq> S" for S
       using assms that by (coinduction arbitrary: xs ys) (force elim: stream.rel_cases)
     then show ?thesis unfolding stream.pred_set by auto
   qed
 
   lemma smap_eq_scons[iff]: "smap f xs = y ## ys \<longleftrightarrow> f (shd xs) = y \<and> smap f (stl xs) = ys"
     using smap_ctr by metis
   lemma scons_eq_smap[iff]: "y ## ys = smap f xs \<longleftrightarrow> y = f (shd xs) \<and> ys = smap f (stl xs)"
     using smap_ctr by metis
   lemma smap_eq_shift[iff]:
     "smap f w = u @- v \<longleftrightarrow> (\<exists> w\<^sub>1 w\<^sub>2. w = w\<^sub>1 @- w\<^sub>2 \<and> map f w\<^sub>1 = u \<and> smap f w\<^sub>2 = v)"
     using sdrop_smap eq_shift stake_sdrop stake_smap by metis
   lemma shift_eq_smap[iff]:
     "u @- v = smap f w \<longleftrightarrow> (\<exists> w\<^sub>1 w\<^sub>2. w = w\<^sub>1 @- w\<^sub>2 \<and> u = map f w\<^sub>1 \<and> v = smap f w\<^sub>2)"
     using sdrop_smap eq_shift stake_sdrop stake_smap by metis
 
   lemma szip_eq_scons[iff]: "szip xs ys = z ## zs \<longleftrightarrow> (shd xs, shd ys) = z \<and> szip (stl xs) (stl ys) = zs"
     using szip.ctr stream.inject by metis
   lemma scons_eq_szip[iff]: "z ## zs = szip xs ys \<longleftrightarrow> z = (shd xs, shd ys) \<and> zs = szip (stl xs) (stl ys)"
     using szip.ctr stream.inject by metis
 
   lemma siterate_eq_scons[iff]: "siterate f s = a ## w \<longleftrightarrow> s = a \<and> siterate f (f s) = w"
     using siterate.ctr stream.inject by metis
   lemma scons_eq_siterate[iff]: "a ## w = siterate f s \<longleftrightarrow> a = s \<and> w = siterate f (f s)"
     using siterate.ctr stream.inject by metis
 
   lemma snth_0: "(a ## w) !! 0 = a" by simp
   lemma eqI_snth:
     assumes "\<And> i. u !! i = v !! i"
     shows "u = v"
     using assms by (coinduction arbitrary: u v) (metis stream.sel snth.simps)
 
   lemma stream_pred_snth: "pred_stream P w \<longleftrightarrow> (\<forall> i. P (w !! i))"
     unfolding stream.pred_set sset_range by simp
   lemma stream_rel_snth: "stream_all2 P u v \<longleftrightarrow> (\<forall> i. P (u !! i) (v !! i))"
   proof safe
     show "P (u !! i) (v !! i)" if "stream_all2 P u v" for i
       using that by (induct i arbitrary: u v) (auto elim: stream.rel_cases)
     show "stream_all2 P u v" if "\<forall> i. P (u !! i) (v !! i)"
       using that by (coinduct) (metis snth_0 snth_Stream)
   qed
 
   lemma stream_rel_pred_szip: "stream_all2 P u v \<longleftrightarrow> pred_stream (case_prod P) (szip u v)"
     unfolding stream_pred_snth stream_rel_snth by simp
 
   lemma sconst_eq[iff]: "sconst x = sconst y \<longleftrightarrow> x = y" by (auto) (metis siterate.simps(1))
   lemma stream_pred__sconst[iff]: "pred_stream P (sconst x) \<longleftrightarrow> P x"
     unfolding stream_pred_snth by simp
   lemma stream_rel_sconst[iff]: "stream_all2 P (sconst x) (sconst y) \<longleftrightarrow> P x y"
     unfolding stream_rel_snth by simp
 
   lemma set_sset_stake[intro!, simp]: "set (stake n xs) \<subseteq> sset xs"
     by (metis sset_shift stake_sdrop sup_ge1)
   lemma sset_sdrop[intro!, simp]: "sset (sdrop n xs) \<subseteq> sset xs"
     by (metis sset_shift stake_sdrop sup_ge2)
 
   lemma set_stake_snth: "x \<in> set (stake n xs) \<longleftrightarrow> (\<exists> i < n. xs !! i = x)"
     unfolding in_set_conv_nth by auto
 
   (* TODO: these should be generated by the transfer option on the primcorec definitions *)
   (* TODO: transfer_prover cannot handle corecursive definitions due to the \<lambda>(s1, s2). undefined
     abortion term that is never used *)
   lemma szip_transfer[transfer_rule]:
     includes lifting_syntax
     shows "(stream_all2 A ===> stream_all2 B ===> stream_all2 (rel_prod A B)) szip szip"
     by (intro rel_funI, coinduction) (force elim: stream.rel_cases)
   lemma siterate_transfer[transfer_rule]:
     includes lifting_syntax
     shows "((A ===> A) ===> A ===> stream_all2 A) siterate siterate"
     by (intro rel_funI, coinduction) (force dest: rel_funD)
 
   lemma split_stream_first:
     assumes "A \<inter> sset xs \<noteq> {}"
     obtains ys a zs
     where "xs = ys @- a ## zs" "A \<inter> set ys = {}" "a \<in> A"
   proof
     let ?n = "LEAST n. xs !! n \<in> A"
     have 1: "xs !! n \<notin> A" if "n < ?n" for n using that by (metis (full_types) not_less_Least)
     show "xs = stake ?n xs @- (xs !! ?n) ## sdrop (Suc ?n) xs" using id_stake_snth_sdrop by blast
     show "A \<inter> set (stake ?n xs) = {}" using 1 by (metis (no_types, lifting) disjoint_iff_not_equal set_stake_snth)
     show "xs !! ?n \<in> A" using assms unfolding sset_range by (auto intro: LeastI)
   qed
   lemma split_stream_first':
     assumes "x \<in> sset xs"
     obtains ys zs
     where "xs = ys @- x ## zs" "x \<notin> set ys"
   proof
     let ?n = "LEAST n. xs !! n = x"
     have 1: "xs !! ?n = x" using assms unfolding sset_range by (auto intro: LeastI)
     have 2: "xs !! n \<noteq> x" if "n < ?n" for n using that by (metis (full_types) not_less_Least)
     show "xs = stake ?n xs @- x ## sdrop (Suc ?n) xs" using 1 by (metis id_stake_snth_sdrop)
     show "x \<notin> set (stake ?n xs)" using 2 by (meson set_stake_snth)
   qed
 
   lemma streams_UNIV[iff]: "streams A = UNIV \<longleftrightarrow> A = UNIV"
   proof
     show "A = UNIV \<Longrightarrow> streams A = UNIV" by simp
   next
     assume "streams A = UNIV"
     then have "w \<in> streams A" for w by simp
     then have "sset w \<subseteq> A" for w unfolding streams_iff_sset by this
     then have "sset (sconst a) \<subseteq> A" for a by blast
     then have "a \<in> A" for a by simp
     then show "A = UNIV" by auto
   qed
   lemma streams_int[simp]: "streams (A \<inter> B) = streams A \<inter> streams B" by (auto iff: streams_iff_sset)
   lemma streams_Int[simp]: "streams (\<Inter> S) = \<Inter> (streams ` S)" by (auto iff: streams_iff_sset)
 
   lemma pred_list_listsp[pred_set_conv]: "list_all = listsp"
     unfolding list.pred_set by auto
   lemma pred_stream_streamsp[pred_set_conv]: "pred_stream = streamsp"
     unfolding stream.pred_set streams_iff_sset[to_pred] by auto
 
   subsection \<open>The scan Function\<close>
 
   primrec (transfer) scan :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'b list" where
     "scan f [] a = []" | "scan f (x # xs) a = f x a # scan f xs (f x a)"
 
   lemma scan_append[simp]: "scan f (xs @ ys) a = scan f xs a @ scan f ys (fold f xs a)"
     by (induct xs arbitrary: a) (auto)
 
   lemma scan_eq_nil[iff]: "scan f xs a = [] \<longleftrightarrow> xs = []" by (cases xs) (auto)
   lemma scan_eq_cons[iff]:
     "scan f xs a = b # w \<longleftrightarrow> (\<exists> y ys. xs = y # ys \<and> f y a = b \<and> scan f ys (f y a) = w)"
     by (cases xs) (auto)
   lemma scan_eq_append[iff]:
     "scan f xs a = u @ v \<longleftrightarrow> (\<exists> ys zs. xs = ys @ zs \<and> scan f ys a = u \<and> scan f zs (fold f ys a) = v)"
     by (induct u arbitrary: xs a) (auto, metis append_Cons fold_simps(2), blast)
 
   lemma scan_length[simp]: "length (scan f xs a) = length xs"
     by (induct xs arbitrary: a) (auto)
   (* TODO: figure out how this is used, should it be a simp rule? or flipped? also target_alt_def *)
   lemma scan_last: "last (a # scan f xs a) = fold f xs a"
     by (induct xs arbitrary: a) (auto simp: last.simps)
   lemma scan_butlast[simp]: "scan f (butlast xs) a = butlast (scan f xs a)"
     by (induct xs arbitrary: a) (auto simp: butlast.simps)
 
   lemma scan_const[simp]: "scan const xs a = xs"
     by (induct xs arbitrary: a) (auto)
   lemma scan_nth[simp]:
     assumes "i < length (scan f xs a)"
     shows "scan f xs a ! i = fold f (take (Suc i) xs) a"
     using assms by (cases xs, simp, induct i arbitrary: xs a, auto simp: take_Suc neq_Nil_conv)
   lemma scan_map[simp]: "scan f (map g xs) a = scan (f \<circ> g) xs a"
     by (induct xs arbitrary: a) (auto)
   lemma scan_take[simp]: "take k (scan f xs a) = scan f (take k xs) a"
     by (induct k arbitrary: xs a) (auto simp: take_Suc neq_Nil_conv)
   lemma scan_drop[simp]: "drop k (scan f xs a) = scan f (drop k xs) (fold f (take k xs) a)"
     by (induct k arbitrary: xs a) (auto simp: take_Suc neq_Nil_conv)
 
   primcorec (transfer) sscan :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a stream \<Rightarrow> 'b \<Rightarrow> 'b stream" where
     "sscan f xs a = f (shd xs) a ## sscan f (stl xs) (f (shd xs) a)"
 
   lemma sscan_scons[simp]: "sscan f (x ## xs) a = f x a ## sscan f xs (f x a)"
     by (simp add: stream.expand)
   lemma sscan_shift[simp]: "sscan f (xs @- ys) a = scan f xs a @- sscan f ys (fold f xs a)"
     by (induct xs arbitrary: a) (auto)
 
   lemma sscan_eq_scons[iff]:
     "sscan f xs a = b ## w \<longleftrightarrow> f (shd xs) a = b \<and> sscan f (stl xs) (f (shd xs) a) = w"
     using sscan.ctr stream.inject by metis
   lemma scons_eq_sscan[iff]:
     "b ## w = sscan f xs a \<longleftrightarrow> b = f (shd xs) a \<and> w = sscan f (stl xs) (f (shd xs) a)"
     using sscan.ctr stream.inject by metis
 
   lemma sscan_const[simp]: "sscan const xs a = xs"
     by (coinduction arbitrary: xs a) (auto)
   lemma sscan_snth[simp]: "sscan f xs a !! i = fold f (stake (Suc i) xs) a"
     by (induct i arbitrary: xs a) (auto)
   lemma sscan_scons_snth[simp]: "(a ## sscan f xs a) !! i = fold f (stake i xs) a"
     by (induct i arbitrary: xs a) (auto)
   lemma sscan_smap[simp]: "sscan f (smap g xs) a = sscan (f \<circ> g) xs a"
     by (coinduction arbitrary: xs a) (auto)
   lemma sscan_stake[simp]: "stake k (sscan f xs a) = scan f (stake k xs) a"
     by (induct k arbitrary: a xs) (auto)
   lemma sscan_sdrop[simp]: "sdrop k (sscan f xs a) = sscan f (sdrop k xs) (fold f (stake k xs) a)"
     by (induct k arbitrary: a xs) (auto)
 
   subsection \<open>Transposing Streams\<close>
 
   primcorec (transfer) stranspose :: "'a stream list \<Rightarrow> 'a list stream" where
     "stranspose ws = map shd ws ## stranspose (map stl ws)"
 
   lemma stranspose_eq_scons[iff]: "stranspose ws = a ## w \<longleftrightarrow> map shd ws = a \<and> stranspose (map stl ws) = w"
     using stranspose.ctr stream.inject by metis
   lemma scons_eq_stranspose[iff]: "a ## w = stranspose ws \<longleftrightarrow> a = map shd ws \<and> w = stranspose (map stl ws)"
     using stranspose.ctr stream.inject by metis
 
   lemma stranspose_nil[simp]: "stranspose [] = sconst []" by coinduction auto
   lemma stranspose_cons[simp]: "stranspose (w # ws) = smap2 Cons w (stranspose ws)"
     by (coinduction arbitrary: w ws) (metis list.simps(9) smap2.simps stranspose.simps stream.sel)
 
   lemma snth_stranspose[simp]: "stranspose ws !! k = map (\<lambda> w. w !! k) ws" by (induct k arbitrary: ws) (auto)
   lemma stranspose_nth[simp]:
     assumes "k < length ws"
     shows "smap (\<lambda> xs. xs ! k) (stranspose ws) = ws ! k"
     using assms by (auto intro: eqI_snth)
 
   subsection \<open>Distinct Streams\<close>
 
   coinductive sdistinct :: "'a stream \<Rightarrow> bool" where
     scons[intro!]: "x \<notin> sset xs \<Longrightarrow> sdistinct xs \<Longrightarrow> sdistinct (x ## xs)"
 
   lemma sdistinct_scons_elim[elim!]:
     assumes "sdistinct (x ## xs)"
     obtains "x \<notin> sset xs" "sdistinct xs"
     using assms by (auto elim: sdistinct.cases)
 
   lemma sdistinct_coinduct[case_names sdistinct, coinduct pred: sdistinct]:
     assumes "P xs"
     assumes "\<And> x xs. P (x ## xs) \<Longrightarrow> x \<notin> sset xs \<and> P xs"
     shows "sdistinct xs"
     using stream.collapse sdistinct.coinduct assms by metis
 
   lemma sdistinct_shift[intro!]:
     assumes "distinct xs" "sdistinct ys" "set xs \<inter> sset ys = {}"
     shows "sdistinct (xs @- ys)"
     using assms by (induct xs) (auto)
   lemma sdistinct_shift_elim[elim!]:
     assumes "sdistinct (xs @- ys)"
     obtains "distinct xs" "sdistinct ys" "set xs \<inter> sset ys = {}"
     using assms by (induct xs) (auto)
 
   lemma sdistinct_infinite_sset:
     assumes "sdistinct w"
     shows "infinite (sset w)"
     using assms by (coinduction arbitrary: w) (force elim: sdistinct.cases)
 
   lemma not_sdistinct_decomp:
     assumes "\<not> sdistinct w"
     obtains u v a w'
     where "w = u @- a ## v @- a ## w'"
   proof (rule ccontr)
     assume 1: "\<not> thesis"
     assume 2: "w = u @- a ## v @- a ## w' \<Longrightarrow> thesis" for u a v w'
     have 3: "\<forall> u v a w'. w \<noteq> u @- a ## v @- a ## w'" using 1 2 by auto
     have 4: "sdistinct w" using 3 by (coinduct) (metis id_stake_snth_sdrop imageE shift.simps sset_range)
     show False using assms 4 by auto
   qed
 
   subsection \<open>Sorted Streams\<close>
 
   coinductive (in order) sascending :: "'a stream \<Rightarrow> bool" where
     "a \<le> b \<Longrightarrow> sascending (b ## w) \<Longrightarrow> sascending (a ## b ## w)"
 
   coinductive (in order) sdescending :: "'a stream \<Rightarrow> bool" where
     "a \<ge> b \<Longrightarrow> sdescending (b ## w) \<Longrightarrow> sdescending (a ## b ## w)"
 
   lemma sdescending_coinduct[case_names sdescending, coinduct pred: sdescending]:
     assumes "P w"
     assumes "\<And> a b w. P (a ## b ## w) \<Longrightarrow> a \<ge> b \<and> P (b ## w)"
     shows "sdescending w"
     using stream.collapse sdescending.coinduct assms by (metis (no_types))
 
+  lemma sdescending_scons:
+    assumes "sdescending (a ## w)"
+    shows "sdescending w"
+    using assms by (auto elim: sdescending.cases)
+  lemma sdescending_sappend:
+    assumes "sdescending (u @- v)"
+    obtains "sdescending v"
+    using assms by (induct u) (auto elim: sdescending.cases)
   lemma sdescending_sdrop:
     assumes "sdescending w"
     shows "sdescending (sdrop k w)"
-    using assms by (induct k) (auto, metis sdescending.cases sdrop_stl stream.sel(2))
+    using assms by (metis sdescending_sappend stake_sdrop)
+
+  lemma sdescending_sset_scons:
+    assumes "sdescending (a ## w)"
+    assumes "b \<in> sset w"
+    shows "a \<ge> b"
+  proof -
+    have "pred_stream (\<lambda> b. a \<ge> b) w" if "sdescending w" "a \<ge> shd w" for w
+      using that by (coinduction arbitrary: w) (auto elim: sdescending.cases)
+    then show ?thesis using assms unfolding stream.pred_set by force
+  qed
+  lemma sdescending_sset_sappend:
+    assumes "sdescending (u @- v)"
+    assumes "a \<in> set u" "b \<in> sset v"
+    shows "a \<ge> b"
+    using assms by (induct u) (auto elim: sdescending.cases dest: sdescending_sset_scons)
 
   lemma sdescending_snth_antimono:
     assumes "sdescending w"
     shows "antimono (snth w)"
   unfolding antimono_iff_le_Suc
   proof
     fix k
     have "sdescending (sdrop k w)" using sdescending_sdrop assms by this
     then obtain a b v where 2: "sdrop k w = a ## b ## v" "a \<ge> b" by rule
     then show "w !! k \<ge> w !! Suc k" by (metis sdrop_simps stream.sel)
   qed
 
   lemma sdescending_stuck:
     fixes w :: "'a :: wellorder stream"
     assumes "sdescending w"
-    obtains k
-    where "sdrop k w = sconst (w !! k)"
+    obtains u a
+    where "w = u @- sconst a"
   using assms
-  proof (induct "w !! 0" arbitrary: w thesis rule: less_induct)
+  proof (induct "shd w" arbitrary: w thesis rule: less_induct)
     case less
     show ?case
-    proof (cases "w = sconst (w !! 0)")
+    proof (cases "w = sconst (shd w)")
       case True
-      show ?thesis using less(2)[of 0] True by simp
+      show ?thesis using shift_replicate_sconst less(2) True by metis
     next
       case False
-      obtain k where 1: "w !! k \<noteq> w !! 0"
-        using False by (metis empty_iff eqI_snth insert_iff snth_sset sset_sconst)
-      have 2: "antimono (snth w)" using sdescending_snth_antimono less(3) by this
-      have 3: "w !! k \<le> w !! 0" using 1 2 by (blast dest: antimonoD)
-      have 4: "sdrop k w !! 0 < w !! 0" using 1 3 by auto
-      have 5: "sdescending (sdrop k w)" using sdescending_sdrop less(3) by this
-      obtain l where 5: "sdrop l (sdrop k w) = sconst (sdrop k w !! l)"
-        using less(1)[OF 4 _ 5] by this
-      show ?thesis using less(2) 5 by simp
+      then obtain u v where 1: "w = u @- v" "u \<noteq> []" "shd w \<noteq> shd v"
+        by (metis empty_iff eqI_snth insert_iff sdrop_simps(1) shift.simps(1) snth_sset sset_sconst stake_sdrop)
+      have 2: "shd w \<ge> shd v" using sdescending_sset_sappend less(3) 1 by (metis hd_in_set shd_sset shift_simps(1))
+      have 3: "shd w > shd v" using 1(3) 2 by simp
+      obtain s a where 4: "v = s @- sconst a" using sdescending_sappend less(1, 3) 1(1) 3 by metis
+      have 5: "w = (u @ s) @- sconst a" unfolding 1(1) 4 by simp
+      show ?thesis using less(2) 5 by this
     qed
   qed
 
 end
diff --git a/thys/Transition_Systems_and_Automata/Basic/Sequence_LTL.thy b/thys/Transition_Systems_and_Automata/Basic/Sequence_LTL.thy
--- a/thys/Transition_Systems_and_Automata/Basic/Sequence_LTL.thy
+++ b/thys/Transition_Systems_and_Automata/Basic/Sequence_LTL.thy
@@ -1,116 +1,137 @@
 section \<open>Linear Temporal Logic on Streams\<close>
 
 theory Sequence_LTL
 imports
   "Sequence"
   "HOL-Library.Linear_Temporal_Logic_on_Streams"
 begin
 
   subsection \<open>Basics\<close>
 
   text \<open>Avoid destroying the constant @{const holds} prematurely.\<close>
   lemmas [simp del] = holds.simps holds_eq1 holds_eq2 not_holds_eq
 
   (* TODO: these cannot be applied successively to simplify infs due to introduction of \<circ>
     avoid or add extra simplification rules for infs *)
   lemma ev_smap[iff]: "ev P (smap f w) \<longleftrightarrow> ev (P \<circ> smap f) w" using ev_smap unfolding comp_apply by this
   lemma alw_smap[iff]: "alw P (smap f w) \<longleftrightarrow> alw (P \<circ> smap f) w" using alw_smap unfolding comp_apply by this
   lemma holds_smap[iff]: "holds P (smap f w) \<longleftrightarrow> holds (P \<circ> f) w" unfolding holds.simps by simp
 
   lemmas [iff] = ev_sconst alw_sconst hld_smap'
 
   lemmas [iff] = alw_ev_stl
   lemma alw_ev_sdrop[iff]: "alw (ev P) (sdrop n w) \<longleftrightarrow> alw (ev P) w"
     using alw_ev_sdrop alw_sdrop by blast
   lemma alw_ev_scons[iff]: "alw (ev P) (a ## w) \<longleftrightarrow> alw (ev P) w" by (metis alw_ev_stl stream.sel(2))
   lemma alw_ev_shift[iff]: "alw (ev P) (u @- v) \<longleftrightarrow> alw (ev P) v" by (induct u) (auto)
 
   lemmas [simp del, iff] = ev_alw_stl
   lemma ev_alw_sdrop[iff]: "ev (alw P) (sdrop n w) \<longleftrightarrow> ev (alw P) w"
     using alwD alw_alw alw_sdrop ev_alw_imp_alw_ev not_ev_iff by metis
   lemma ev_alw_scons[iff]: "ev (alw P) (a ## w) \<longleftrightarrow> ev (alw P) w" by (metis ev_alw_stl stream.sel(2))
   lemma ev_alw_shift[iff]: "ev (alw P) (u @- v) \<longleftrightarrow> ev (alw P) v" by (induct u) (auto)
 
   lemma holds_sconst[iff]: "holds P (sconst a) \<longleftrightarrow> P a" unfolding holds.simps by simp
   lemma HLD_sconst[iff]: "HLD A (sconst a) \<longleftrightarrow> a \<in> A" unfolding HLD_def holds.simps by simp
 
   lemma ev_alt_def: "ev \<phi> w \<longleftrightarrow> (\<exists> u v. w = u @- v \<and> \<phi> v)"
     using ev.base ev_shift ev_imp_shift by metis
   lemma ev_stl_alt_def: "ev \<phi> (stl w) \<longleftrightarrow> (\<exists> u v. w = u @- v \<and> u \<noteq> [] \<and> \<phi> v)"
     unfolding ev_alt_def by (cases w) (force simp: scons_eq)
 
   lemma ev_HLD_sset: "ev (HLD A) w \<longleftrightarrow> sset w \<inter> A \<noteq> {}" unfolding HLD_def ev_holds_sset by auto
 
   lemma alw_ev_coinduct[case_names alw_ev, consumes 1]:
     assumes "R w"
     assumes "\<And> w. R w \<Longrightarrow> ev \<phi> w \<and> ev R (stl w)"
     shows "alw (ev \<phi>) w"
   proof -
     have "ev R w" using assms(1) by rule
     then show ?thesis using assms(2) by (coinduct) (metis alw_sdrop not_ev_iff sdrop_stl sdrop_wait)
   qed
 
   subsection \<open>Infinite Occurrence\<close>
 
   abbreviation "infs P w \<equiv> alw (ev (holds P)) w"
   abbreviation "fins P w \<equiv> \<not> infs P w"
 
   lemma infs_suffix: "infs P w \<longleftrightarrow> (\<forall> u v. w = u @- v \<longrightarrow> Bex (sset v) P)"
     using alwD alw_iff_sdrop alw_shift ev_holds_sset stake_sdrop by (metis (mono_tags, hide_lams))
   lemma infs_snth: "infs P w \<longleftrightarrow> (\<forall> n. \<exists> k \<ge> n. P (w !! k))"
     by (auto simp: alw_iff_sdrop ev_iff_sdrop holds.simps intro: le_add1 dest: le_Suc_ex)
   lemma infs_infm: "infs P w \<longleftrightarrow> (\<exists>\<^sub>\<infinity> i. P (w !! i))"
     unfolding infs_snth INFM_nat_le by rule
 
   lemma infs_coinduct[case_names infs, coinduct pred: infs]:
     assumes "R w"
     assumes "\<And> w. R w \<Longrightarrow> Bex (sset w) P \<and> ev R (stl w)"
     shows "infs P w"
     using assms by (coinduct rule: alw_ev_coinduct) (auto simp: ev_holds_sset)
-  lemma infs_set_coinduct[case_names infs_set, consumes 1]:
+  lemma infs_coinduct_shift[case_names infs, consumes 1]:
     assumes "R w"
     assumes "\<And> w. R w \<Longrightarrow> \<exists> u v. w = u @- v \<and> Bex (set u) P \<and> R v"
     shows "infs P w"
     using assms by (coinduct) (force simp: ev_stl_alt_def)
   lemma infs_flat_coinduct[case_names infs_flat, consumes 1]:
     assumes "R w"
     assumes "\<And> u v. R (u ## v) \<Longrightarrow> Bex (set u) P \<and> R v"
     shows "infs P (flat w)"
-    using assms by (coinduction arbitrary: w rule: infs_set_coinduct)
+    using assms by (coinduction arbitrary: w rule: infs_coinduct_shift)
       (metis empty_iff flat_Stream list.set(1) stream.exhaust)
+  lemma infs_sscan_coinduct[case_names infs_sscan, consumes 1]:
+    assumes "R w a"
+    assumes "\<And> w a. R w a \<Longrightarrow> P a \<and> (\<exists> u v. w = u @- v \<and> u \<noteq> [] \<and> R v (fold f u a))"
+    shows "infs P (a ## sscan f w a)"
+  using assms(1)
+  proof (coinduction arbitrary: w a rule: infs_coinduct_shift)
+    case (infs w a)
+    obtain u v where 1: "P a" "w = u @- v" "u \<noteq> []" "R v (fold f u a)" using infs assms(2) by blast
+    show ?case
+    proof (intro exI conjI bexI)
+      have "sscan f w a = scan f u a @- sscan f v (fold f u a)" unfolding 1(2) by simp
+      also have "scan f u a = butlast (scan f u a) @ [fold f u a]"
+        using 1(3) by (metis last_ConsR scan_eq_nil scan_last snoc_eq_iff_butlast)
+      also have "a ## \<dots> @- sscan f v (fold f u a) =
+        (a # butlast (scan f u a)) @- fold f u a ## sscan f v (fold f u a)" by simp
+      finally show "a ## sscan f w a = (a # butlast (scan f u a)) @- fold f u a ## sscan f v (fold f u a)" by this
+      show "P a" using 1(1) by this
+      show "a \<in> set (a # butlast (scan f u a))" by simp
+      show "R v (fold f u a)" using 1(4) by this
+    qed rule
+  qed
 
   lemma infs_mono: "(\<And> a. a \<in> sset w \<Longrightarrow> P a \<Longrightarrow> Q a) \<Longrightarrow> infs P w \<Longrightarrow> infs Q w"
     unfolding infs_snth by force
   lemma infs_mono_strong: "stream_all2 (\<lambda> a b. P a \<longrightarrow> Q b) u v \<Longrightarrow> infs P u \<Longrightarrow> infs Q v"
     unfolding stream_rel_snth infs_snth by blast
 
   lemma infs_all: "Ball (sset w) P \<Longrightarrow> infs P w" unfolding infs_snth by auto
   lemma infs_any: "infs P w \<Longrightarrow> Bex (sset w) P" unfolding ev_holds_sset by auto
 
   lemma infs_bot[iff]: "infs bot w \<longleftrightarrow> False" using infs_any by auto
   lemma infs_top[iff]: "infs top w \<longleftrightarrow> True" by (simp add: infs_all)
   lemma infs_disj[iff]: "infs (\<lambda> a. P a \<or> Q a) w \<longleftrightarrow> infs P w \<or> infs Q w"
     unfolding infs_snth using le_trans le_cases by metis
   lemma infs_bex[iff]:
     assumes "finite S"
     shows "infs (\<lambda> a. \<exists> x \<in> S. P x a) w \<longleftrightarrow> (\<exists> x \<in> S. infs (P x) w)"
     using assms infs_any by induct auto
   lemma infs_bex_le_nat[iff]: "infs (\<lambda> a. \<exists> k < n :: nat. P k a) w \<longleftrightarrow> (\<exists> k < n. infs (P k) w)"
   proof -
     have "infs (\<lambda> a. \<exists> k < n. P k a) w \<longleftrightarrow> infs (\<lambda> a. \<exists> k \<in> {k. k < n}. P k a) w" by simp
     also have "\<dots> \<longleftrightarrow> (\<exists> k \<in> {k. k < n}. infs (P k) w)" by blast
     also have "\<dots> \<longleftrightarrow> (\<exists> k < n. infs (P k) w)" by simp
     finally show ?thesis by this
   qed
 
   lemma infs_cycle[iff]:
     assumes "w \<noteq> []"
     shows "infs P (cycle w) \<longleftrightarrow> Bex (set w) P"
   proof
     show "infs P (cycle w) \<Longrightarrow> Bex (set w) P"
       using assms by (auto simp: ev_holds_sset dest: alwD)
     show "Bex (set w) P \<Longrightarrow> infs P (cycle w)"
-      using assms by (coinduction rule: infs_set_coinduct) (blast dest: cycle_decomp)
+      using assms by (coinduction rule: infs_coinduct_shift) (blast dest: cycle_decomp)
   qed
 
 end
\ No newline at end of file
diff --git a/thys/Transition_Systems_and_Automata/Transition_Systems/Transition_System_Construction.thy b/thys/Transition_Systems_and_Automata/Transition_Systems/Transition_System_Construction.thy
--- a/thys/Transition_Systems_and_Automata/Transition_Systems/Transition_System_Construction.thy
+++ b/thys/Transition_Systems_and_Automata/Transition_Systems/Transition_System_Construction.thy
@@ -1,110 +1,99 @@
 section \<open>Constructing Paths and Runs in Transition Systems\<close>
 
 theory Transition_System_Construction
 imports
   "../Basic/Sequence_LTL"
   "Transition_System"
 begin
 
   context transition_system
   begin
 
     lemma invariant_run:
       assumes "P p" "\<And> p. P p \<Longrightarrow> \<exists> a. enabled a p \<and> P (execute a p) \<and> Q p a"
       obtains r
       where "run r p" "pred_stream P (p ## trace r p)" "stream_all2 Q (p ## trace r p) r"
     proof -
-      obtain f where 1: "P p" "\<And> p. P p \<Longrightarrow> enabled (f p) p \<and> P (execute (f p) p) \<and> Q p (f p)"
+      obtain f where 1:
+        "P p"
+        "\<And> p. P p \<Longrightarrow> enabled (f p) p"
+        "\<And> p. P p \<Longrightarrow> P (execute (f p) p)"
+        "\<And> p. P p \<Longrightarrow> Q p (f p)"
         using assms by metis
-      note 2 = that[of "smap f (siterate (\<lambda> p. execute (f p) p) p)"]
-      show ?thesis using 1 by (intro 2; coinduction arbitrary: p) (auto)
+      let ?r = "\<lambda> p. smap f (siterate (\<lambda> p. execute (f p) p) p)"
+      show ?thesis
+      proof
+        show "run (?r p) p" using 1 by (coinduction arbitrary: p) (auto)
+        show "pred_stream P (p ## trace (?r p) p)" using 1 by (coinduction arbitrary: p) (auto)
+        show "stream_all2 Q (p ## trace (?r p) p) (?r p)" using 1 by (coinduction arbitrary: p) (auto)
+      qed
+    qed
+    lemma recurring_condition:
+      assumes "P p" "\<And> p. P p \<Longrightarrow> \<exists> r. r \<noteq> [] \<and> path r p \<and> P (target r p)"
+      obtains r
+      where "run r p" "infs P (p ## trace r p)"
+    proof -
+      obtain f where 1:
+        "P p"
+        "\<And> p. P p \<Longrightarrow> f p \<noteq> []"
+        "\<And> p. P p \<Longrightarrow> path (f p) p"
+        "\<And> p. P p \<Longrightarrow> P (target (f p) p)"
+        using assms by metis
+      let ?r = "\<lambda> p. flat (smap f (siterate (\<lambda> p. target (f p) p) p))"
+      have 2: "?r p = f p @- ?r (target (f p) p)" if "P p" for p using that 1(2) by (simp add: flat_unfold)
+      show ?thesis
+      proof
+        show "run (?r p) p" using 1 2 by (coinduction arbitrary: p rule: run_coinduct_shift) (blast)
+        show "infs P (p ## trace (?r p) p)" using 1 2 by (coinduction arbitrary: p rule: infs_sscan_coinduct) (blast)
+      qed
     qed
 
     lemma invariant_run_index:
       assumes "P n p" "\<And> n p. P n p \<Longrightarrow> \<exists> a. enabled a p \<and> P (Suc n) (execute a p) \<and> Q n p a"
       obtains r
       where
         "run r p"
         "\<And> i. P (n + i) (target (stake i r) p)"
         "\<And> i. Q (n + i) (target (stake i r) p) (r !! i)"
     proof -
       define s where "s \<equiv> (n, p)"
       have 1: "case_prod P s" using assms(1) unfolding s_def by auto
       obtain f where 2:
         "\<And> n p. P n p \<Longrightarrow> enabled (f n p) p"
         "\<And> n p. P n p \<Longrightarrow> P (Suc n) (execute (f n p) p)"
         "\<And> n p. P n p \<Longrightarrow> Q n p (f n p)"
         using assms(2) by metis
       define g where "g \<equiv> \<lambda> (n, p). (Suc n, execute (f n p) p)"
 
       let ?r = "smap (case_prod f) (siterate g s)"
 
       have 3: "run ?r (snd s)" using 1 2(1, 2) unfolding g_def by (coinduction arbitrary: s) (auto)
       have 4: "case_prod P (compow k g s)" for k using 1 2(2) unfolding g_def by (induct k) (auto)
       have 5: "case_prod Q (compow k g s) (?r !! k)" for k using 2(3) 4 by (simp add: case_prod_beta)
 
       have 6: "compow k g (n, p) = (n + k, target (stake k ?r) p)" for k
         unfolding s_def g_def by (induct k) (auto simp add: stake_Suc simp del: stake.simps(2))
 
       show ?thesis using that 3 4 5 unfolding s_def 6 by simp
     qed
 
-    lemma recurring_condition:
-      assumes "P p" "\<And> p. P p \<Longrightarrow> \<exists> r. r \<noteq> [] \<and> path r p \<and> P (target r p)"
-      obtains r
-      where "run r p" "infs P (p ## trace r p)"
-    proof -
-      obtain f where 1:
-        "P p"
-        "\<And> p. P p \<Longrightarrow> f p \<noteq> []"
-        "\<And> p. P p \<Longrightarrow> path (f p) p"
-        "\<And> p. P p \<Longrightarrow> P (target (f p) p)"
-        using assms by metis
-      define g where "g p \<equiv> target (f p) p" for p
-      define h where "h p \<equiv> states (f p) p" for p
-
-      have 2: "P (g p)" if "P p" for p using 1(4) that unfolding g_def by simp
-      have 3: "h p \<noteq> []" if "P p" for p using 1(2) that unfolding h_def by simp
-
-      let ?r = "\<lambda> p. flat (smap f (siterate g p))"
-      let ?t = "\<lambda> p. flat (smap h (siterate g p))"
-
-      have 4: "?t p = h p @- ?t (g p)" if "P p" for p
-        using 1(2) that by (simp add: flat_unfold g_def h_def)
-      have 5: "trace (?r p) p = h p @- trace (?r (g p)) (g p)" if "P p" for p
-        using 1(2) that by (simp add: flat_unfold g_def h_def)
-      have 6: "?t p = trace (?r p) p"
-        using 1(1) 2 3 4 5 by (coinduction arbitrary: p rule: stream_eq_coinduct_shift) (blast)
-
-      have 7: "run (?r p) p"
-        using 1 unfolding g_def by (coinduction arbitrary: p rule: run_flat_coinduct) (auto)
-
-      have 8: "g p = last (h p)" if "P p" for p by (metis 3 that g_def h_def last.simps scan_last)
-      have 9: "Bex (set (h p)) P" if "P p" for p using 2 3 8 that by force
-      have 10: "infs P (?t p)"
-        using 1 9 unfolding g_def by (coinduction arbitrary: p rule: infs_flat_coinduct) (auto)
-      have 11: "infs P (p ## ?t p)" using 10 by simp
-
-      show ?thesis using that 7 11 unfolding 6 by this
-    qed
-
     lemma koenig:
       assumes "infinite (reachable p)"
       assumes "\<And> q. q \<in> reachable p \<Longrightarrow> finite (successors q)"
       obtains r
       where "run r p"
     proof (rule invariant_run[where ?P = "\<lambda> q. q \<in> reachable p \<and> infinite (reachable q)"])
       show "p \<in> reachable p \<and> infinite (reachable p)" using assms(1) by auto
     next
       fix q
       assume 1: "q \<in> reachable p \<and> infinite (reachable q)"
       have 2: "finite (successors q)" using assms(2) 1 by auto
       have 3: "infinite (insert q (\<Union>(reachable ` (successors q))))" using reachable_step 1 by metis
       obtain s where 4: "s \<in> successors q" "infinite (reachable s)" using 2 3 by auto
       show "\<exists> a. enabled a q \<and> (execute a q \<in> reachable p \<and> infinite (reachable (execute a q))) \<and> True"
         using 1 4 by auto
     qed
 
   end
 
 end