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_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