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,481 +1,481 @@
 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"
       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)"
       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
     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 "sset (smap f (gtrace (sdrop n r) (gtarget (stake n r) v))) \<subseteq> Collect 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 "sset (smap f (gtrace (sdrop n r) (gtarget (stake n r) v))) = sset (sconst k)"
       unfolding 1 by rule
     also have "\<dots> \<subseteq> Collect odd" using 4 by simp
     finally show ?thesis using that by simp
   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) (trace (w ||| r) p)"
       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: "sset (smap f (gtrace (sdrop n ?r) (gtarget (stake n ?r) ?v))) \<subseteq> {a. odd a}"
       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) unfolding trace_alt_def by simp
     have 18: "infs (gaccepting A) ?r" using 19 by (force simp: comp_def)
     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> \<not> infs (accepting A) (trace (w ||| r) v)"
+    have 3: "\<And> r v. v \<in> initial A \<Longrightarrow> run A (w ||| r) v \<Longrightarrow> fins (accepting A) (trace (w ||| r) v)"
       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: "\<not> infs (accepting A) (trace (w ||| s) q)" using 3 9 8 by this
-    have 11: "\<not> infs (accepting A) s" using 10 unfolding trace_alt_def by simp
+    have 10: "fins (accepting A) (trace (w ||| s) q)" using 3 9 8 by this
+    have 11: "fins (accepting A) s" using 10 unfolding trace_alt_def by simp
     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 11 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 "\<forall> k. v \<in> graph A w k \<longrightarrow> k \<le> 2 * card (nodes A)" using graph_le assms(1, 2) 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 "\<forall> k. v \<in> graph A w k \<longrightarrow> k \<le> 2 * card (nodes A)" using graph_le assms(1, 2) 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/LTL_Master_Theorem/LTL_to_DRA/DRA_Construction.thy b/thys/LTL_Master_Theorem/LTL_to_DRA/DRA_Construction.thy
--- a/thys/LTL_Master_Theorem/LTL_to_DRA/DRA_Construction.thy
+++ b/thys/LTL_Master_Theorem/LTL_to_DRA/DRA_Construction.thy
@@ -1,440 +1,440 @@
 (*
     Author:   Benedikt Seidl
     License:  BSD
 *)
 
 section \<open>Constructing DRAs for LTL Formulas\<close>
 
 theory DRA_Construction
   imports
     Transition_Functions
 
     "../Quotient_Type"
     "../Omega_Words_Fun_Stream"
 
     "../Logical_Characterization/Master_Theorem"
 
     Transition_Systems_and_Automata.DBA_Combine
     Transition_Systems_and_Automata.DCA_Combine
     Transition_Systems_and_Automata.DRA_Combine
 begin
 
 \<comment> \<open>We use prefix and suffix on infinite words.\<close>
 hide_const Sublist.prefix Sublist.suffix
 
 locale dra_construction = transition_functions eq + quotient eq Rep Abs
   for
     eq :: "'a ltln \<Rightarrow> 'a ltln \<Rightarrow> bool" (infix "\<sim>" 75)
   and
     Rep :: "'ltlq \<Rightarrow> 'a ltln"
   and
     Abs :: "'a ltln \<Rightarrow> 'ltlq"
 begin
 
 subsection \<open>Lifting Setup\<close>
 
 abbreviation true\<^sub>n_lifted :: "'ltlq" ("\<up>true\<^sub>n") where
   "\<up>true\<^sub>n \<equiv> Abs true\<^sub>n"
 
 abbreviation false\<^sub>n_lifted :: "'ltlq" ("\<up>false\<^sub>n") where
   "\<up>false\<^sub>n \<equiv> Abs false\<^sub>n"
 
 abbreviation af_letter_lifted :: "'a set \<Rightarrow> 'ltlq \<Rightarrow> 'ltlq" ("\<up>afletter") where
   "\<up>afletter \<nu> \<phi> \<equiv> Abs (af_letter (Rep \<phi>) \<nu>)"
 
 abbreviation af_lifted :: "'ltlq \<Rightarrow> 'a set list \<Rightarrow> 'ltlq" ("\<up>af") where
   "\<up>af \<phi> w \<equiv> fold \<up>afletter w \<phi>"
 
 abbreviation GF_advice_lifted :: "'ltlq \<Rightarrow> 'a ltln set \<Rightarrow> 'ltlq" ("_\<up>[_]\<^sub>\<nu>" [90,60] 89) where
   "\<phi>\<up>[X]\<^sub>\<nu> \<equiv> Abs ((Rep \<phi>)[X]\<^sub>\<nu>)"
 
 
 lemma af_letter_lifted_semantics:
   "\<up>afletter \<nu> (Abs \<phi>) = Abs (af_letter \<phi> \<nu>)"
   by (metis Rep_Abs_eq af_letter_congruent Abs_eq)
 
 lemma af_lifted_semantics:
   "\<up>af (Abs \<phi>) w = Abs (af \<phi> w)"
   by (induction w rule: rev_induct) (auto simp: Abs_eq, insert Rep_Abs_eq af_letter_congruent eq_sym, blast)
 
 lemma af_lifted_range:
   "range (\<up>af (Abs \<phi>)) \<subseteq> {Abs \<psi> | \<psi>. nested_prop_atoms \<psi> \<subseteq> nested_prop_atoms \<phi>}"
   using af_lifted_semantics af_nested_prop_atoms by blast
 
 
 definition af_letter\<^sub>F_lifted :: "'a ltln \<Rightarrow> 'a set \<Rightarrow> 'ltlq \<Rightarrow> 'ltlq" ("\<up>afletter\<^sub>F")
 where
   "\<up>afletter\<^sub>F \<phi> \<nu> \<psi> \<equiv> Abs (af_letter\<^sub>F \<phi> (Rep \<psi>) \<nu>)"
 
 definition af_letter\<^sub>G_lifted :: "'a ltln \<Rightarrow> 'a set \<Rightarrow> 'ltlq \<Rightarrow> 'ltlq" ("\<up>afletter\<^sub>G")
 where
   "\<up>afletter\<^sub>G \<phi> \<nu> \<psi> \<equiv> Abs (af_letter\<^sub>G \<phi> (Rep \<psi>) \<nu>)"
 
 lemma af_letter\<^sub>F_lifted_semantics:
   "\<up>afletter\<^sub>F \<phi> \<nu> (Abs \<psi>) = Abs (af_letter\<^sub>F \<phi> \<psi> \<nu>)"
   by (metis af_letter\<^sub>F_lifted_def Rep_inverse af_letter\<^sub>F_def af_letter_congruent Abs_eq)
 
 lemma af_letter\<^sub>G_lifted_semantics:
   "\<up>afletter\<^sub>G \<phi> \<nu> (Abs \<psi>) = Abs (af_letter\<^sub>G \<phi> \<psi> \<nu>)"
   by (metis af_letter\<^sub>G_lifted_def Rep_inverse af_letter\<^sub>G_def af_letter_congruent Abs_eq)
 
 abbreviation af\<^sub>F_lifted :: "'a ltln \<Rightarrow> 'ltlq \<Rightarrow> 'a set list \<Rightarrow> 'ltlq" ("\<up>af\<^sub>F")
 where
   "\<up>af\<^sub>F \<phi> \<psi> w \<equiv> fold (\<up>afletter\<^sub>F \<phi>) w \<psi>"
 
 abbreviation af\<^sub>G_lifted :: "'a ltln \<Rightarrow> 'ltlq \<Rightarrow> 'a set list \<Rightarrow> 'ltlq" ("\<up>af\<^sub>G")
 where
   "\<up>af\<^sub>G \<phi> \<psi> w \<equiv> fold (\<up>afletter\<^sub>G \<phi>) w \<psi>"
 
 lemma af\<^sub>F_lifted_semantics:
   "\<up>af\<^sub>F \<phi> (Abs \<psi>) w = Abs (af\<^sub>F \<phi> \<psi> w)"
   by (induction w rule: rev_induct) (auto simp: af_letter\<^sub>F_lifted_semantics)
 
 lemma af\<^sub>G_lifted_semantics:
   "\<up>af\<^sub>G \<phi> (Abs \<psi>) w = Abs (af\<^sub>G \<phi> \<psi> w)"
   by (induction w rule: rev_induct) (auto simp: af_letter\<^sub>G_lifted_semantics)
 
 lemma af\<^sub>F_lifted_range:
   "nested_prop_atoms \<psi> \<subseteq> nested_prop_atoms (F\<^sub>n \<phi>) \<Longrightarrow> range (\<up>af\<^sub>F \<phi> (Abs \<psi>)) \<subseteq>  {Abs \<psi> | \<psi>. nested_prop_atoms \<psi> \<subseteq> nested_prop_atoms (F\<^sub>n \<phi>)}"
   using af\<^sub>F_lifted_semantics af\<^sub>F_nested_prop_atoms by blast
 
 lemma af\<^sub>G_lifted_range:
   "nested_prop_atoms \<psi> \<subseteq> nested_prop_atoms (G\<^sub>n \<phi>) \<Longrightarrow> range (\<up>af\<^sub>G \<phi> (Abs \<psi>)) \<subseteq>  {Abs \<psi> | \<psi>. nested_prop_atoms \<psi> \<subseteq> nested_prop_atoms (G\<^sub>n \<phi>)}"
   using af\<^sub>G_lifted_semantics af\<^sub>G_nested_prop_atoms by blast
 
 
 definition af_letter\<^sub>\<nu>_lifted :: "'a ltln set \<Rightarrow> 'a set \<Rightarrow> 'ltlq \<times> 'ltlq \<Rightarrow> 'ltlq \<times> 'ltlq" ("\<up>afletter\<^sub>\<nu>")
 where
   "\<up>afletter\<^sub>\<nu> X \<nu> p \<equiv>
     (Abs (fst (af_letter\<^sub>\<nu> X (Rep (fst p), Rep (snd p)) \<nu>)),
      Abs (snd (af_letter\<^sub>\<nu> X (Rep (fst p), Rep (snd p)) \<nu>)))"
 
 abbreviation af\<^sub>\<nu>_lifted :: "'a ltln set \<Rightarrow> 'ltlq \<times> 'ltlq \<Rightarrow> 'a set list \<Rightarrow> 'ltlq \<times> 'ltlq" ("\<up>af\<^sub>\<nu>")
 where
   "\<up>af\<^sub>\<nu> X p w \<equiv> fold (\<up>afletter\<^sub>\<nu> X) w p"
 
 lemma af_letter\<^sub>\<nu>_lifted_semantics:
   "\<up>afletter\<^sub>\<nu> X \<nu> (Abs x, Abs y) = (Abs (fst (af_letter\<^sub>\<nu> X (x, y) \<nu>)), Abs (snd (af_letter\<^sub>\<nu> X (x, y) \<nu>)))"
   by (simp add: af_letter\<^sub>\<nu>_def af_letter\<^sub>\<nu>_lifted_def) (insert GF_advice_congruent Rep_Abs_eq Rep_inverse af_letter_lifted_semantics eq_trans Abs_eq, blast)
 
 lemma af\<^sub>\<nu>_lifted_semantics:
   "\<up>af\<^sub>\<nu> X (Abs \<xi>, Abs \<zeta>) w = (Abs (fst (af\<^sub>\<nu> X (\<xi>, \<zeta>) w)), Abs (snd (af\<^sub>\<nu> X (\<xi>, \<zeta>) w)))"
   apply (induction w rule: rev_induct) 
    apply (auto simp: af_letter\<^sub>\<nu>_lifted_def af_letter\<^sub>\<nu>_lifted_semantics af_letter_lifted_semantics)
   by (metis (no_types, hide_lams) af_letter\<^sub>\<nu>_lifted_def af\<^sub>\<nu>_fst af_letter\<^sub>\<nu>_lifted_semantics eq_fst_iff prod.sel(2))
 
 
 
 subsection \<open>Büchi automata for basic languages\<close>
 
 definition \<AA>\<^sub>\<mu> :: "'a ltln \<Rightarrow> ('a set, 'ltlq) dba" where
   "\<AA>\<^sub>\<mu> \<phi> = dba UNIV (Abs \<phi>) \<up>afletter (\<lambda>\<psi>. \<psi> = \<up>true\<^sub>n)"
 
 definition \<AA>\<^sub>\<mu>_GF :: "'a ltln \<Rightarrow> ('a set, 'ltlq) dba" where
   "\<AA>\<^sub>\<mu>_GF \<phi> = dba UNIV (Abs (F\<^sub>n \<phi>)) (\<up>afletter\<^sub>F \<phi>) (\<lambda>\<psi>. \<psi> = \<up>true\<^sub>n)"
 
 definition \<AA>\<^sub>\<nu> :: "'a ltln \<Rightarrow> ('a set, 'ltlq) dca" where
   "\<AA>\<^sub>\<nu> \<phi> = dca UNIV (Abs \<phi>) \<up>afletter (\<lambda>\<psi>. \<psi> = \<up>false\<^sub>n)"
 
 definition \<AA>\<^sub>\<nu>_FG :: "'a ltln \<Rightarrow> ('a set, 'ltlq) dca" where
   "\<AA>\<^sub>\<nu>_FG \<phi> = dca UNIV (Abs (G\<^sub>n \<phi>)) (\<up>afletter\<^sub>G \<phi>) (\<lambda>\<psi>. \<psi> = \<up>false\<^sub>n)"
 
 
 lemma dba_run:
   "DBA.run (dba UNIV p \<delta> \<alpha>) (to_stream w) p"
   unfolding DBA.run_def by (rule transition_system.snth_run) fastforce
 
 lemma dca_run:
   "DCA.run (dca UNIV p \<delta> \<alpha>) (to_stream w) p"
   unfolding DCA.run_def by (rule transition_system.snth_run) fastforce
 
 
 lemma \<AA>\<^sub>\<mu>_language:
   "\<phi> \<in> \<mu>LTL \<Longrightarrow> to_stream w \<in> DBA.language (\<AA>\<^sub>\<mu> \<phi>) \<longleftrightarrow> w \<Turnstile>\<^sub>n \<phi>"
 proof -
   assume "\<phi> \<in> \<mu>LTL"
 
   then have "w \<Turnstile>\<^sub>n \<phi> \<longleftrightarrow> (\<forall>n. \<exists>k\<ge>n. af \<phi> (w[0 \<rightarrow> k]) \<sim> true\<^sub>n)"
     by (meson af_\<mu>LTL af_prefix_true le_cases)
 
   also have "\<dots> \<longleftrightarrow> (\<forall>n. \<exists>k\<ge>n. af \<phi> (w[0 \<rightarrow> Suc k]) \<sim> true\<^sub>n)"
     by (meson af_prefix_true le_SucI order_refl)
 
   also have "\<dots> \<longleftrightarrow> infs (\<lambda>\<psi>. \<psi> = \<up>true\<^sub>n) (DBA.trace (\<AA>\<^sub>\<mu> \<phi>) (to_stream w) (Abs \<phi>))"
     by (simp add: infs_snth \<AA>\<^sub>\<mu>_def DBA.succ_def af_lifted_semantics Abs_eq[symmetric] af_letter_lifted_semantics)
 
   also have "\<dots> \<longleftrightarrow> to_stream w \<in> DBA.language (\<AA>\<^sub>\<mu> \<phi>)"
     unfolding \<AA>\<^sub>\<mu>_def dba.initial_def dba.accepting_def
     by (metis dba_run DBA.language DBA.language_elim dba.sel(2) dba.sel(4))
 
   finally show ?thesis
     by simp
 qed
 
 lemma \<AA>\<^sub>\<mu>_GF_language:
   "\<phi> \<in> \<mu>LTL \<Longrightarrow> to_stream w \<in> DBA.language (\<AA>\<^sub>\<mu>_GF \<phi>) \<longleftrightarrow> w \<Turnstile>\<^sub>n G\<^sub>n (F\<^sub>n \<phi>)"
 proof -
   assume "\<phi> \<in> \<mu>LTL"
 
   then have "w \<Turnstile>\<^sub>n G\<^sub>n (F\<^sub>n \<phi>) \<longleftrightarrow> (\<forall>n. \<exists>k. af (F\<^sub>n \<phi>) (w[n \<rightarrow> k]) \<sim>\<^sub>L true\<^sub>n)"
     using ltl_lang_equivalence.af_\<mu>LTL_GF by blast
 
   also have "\<dots> \<longleftrightarrow> (\<forall>n. \<exists>k>n. af\<^sub>F \<phi> (F\<^sub>n \<phi>) (w[0 \<rightarrow> k]) \<sim> true\<^sub>n)"
     using af\<^sub>F_semantics_ltr af\<^sub>F_semantics_rtl
     using \<open>\<phi> \<in> \<mu>LTL\<close> af_\<mu>LTL_GF calculation by blast
 
   also have "\<dots> \<longleftrightarrow> (\<forall>n. \<exists>k\<ge>n. af\<^sub>F \<phi> (F\<^sub>n \<phi>) (w[0 \<rightarrow> Suc k]) \<sim> true\<^sub>n)"
     by (metis less_Suc_eq_le less_imp_Suc_add)
 
   also have "\<dots> \<longleftrightarrow> infs (\<lambda>\<psi>. \<psi> = \<up>true\<^sub>n) (DBA.trace (\<AA>\<^sub>\<mu>_GF \<phi>) (to_stream w) (Abs (F\<^sub>n \<phi>)))"
     by (simp add: infs_snth \<AA>\<^sub>\<mu>_GF_def DBA.succ_def af\<^sub>F_lifted_semantics Abs_eq[symmetric] af_letter\<^sub>F_lifted_semantics)
 
   also have "\<dots> \<longleftrightarrow> to_stream w \<in> DBA.language (\<AA>\<^sub>\<mu>_GF \<phi>)"
     unfolding \<AA>\<^sub>\<mu>_GF_def dba.initial_def dba.accepting_def
     by (metis dba_run DBA.language DBA.language_elim dba.sel(2) dba.sel(4))
 
   finally show ?thesis
     by simp
 qed
 
 lemma \<AA>\<^sub>\<nu>_language:
   "\<phi> \<in> \<nu>LTL \<Longrightarrow> to_stream w \<in> DCA.language (\<AA>\<^sub>\<nu> \<phi>) \<longleftrightarrow> w \<Turnstile>\<^sub>n \<phi>"
 proof -
   assume "\<phi> \<in> \<nu>LTL"
 
   then have "w \<Turnstile>\<^sub>n \<phi> \<longleftrightarrow> (\<exists>n. \<forall>k\<ge>n. \<not> af \<phi> (w[0 \<rightarrow> k]) \<sim> false\<^sub>n)"
     by (meson af_\<nu>LTL af_prefix_false le_cases order_refl)
 
   also have "\<dots> \<longleftrightarrow> (\<exists>n. \<forall>k\<ge>n. \<not> af \<phi> (w[0 \<rightarrow> Suc k]) \<sim> false\<^sub>n)"
     by (meson af_prefix_false le_SucI order_refl)
 
-  also have "\<dots> \<longleftrightarrow> \<not> infs (\<lambda>\<psi>. \<psi> = \<up>false\<^sub>n) (DCA.trace (\<AA>\<^sub>\<nu> \<phi>) (to_stream w) (Abs \<phi>))"
+  also have "\<dots> \<longleftrightarrow> fins (\<lambda>\<psi>. \<psi> = \<up>false\<^sub>n) (DCA.trace (\<AA>\<^sub>\<nu> \<phi>) (to_stream w) (Abs \<phi>))"
     by (simp add: infs_snth \<AA>\<^sub>\<nu>_def DBA.succ_def af_lifted_semantics Abs_eq[symmetric] af_letter_lifted_semantics)
 
   also have "\<dots> \<longleftrightarrow> to_stream w \<in> DCA.language (\<AA>\<^sub>\<nu> \<phi>)"
     unfolding \<AA>\<^sub>\<nu>_def dca.initial_def dca.rejecting_def
     by (metis dca_run DCA.language DCA.language_elim dca.sel(2) dca.sel(4))
 
   finally show ?thesis
     by simp
 qed
 
 lemma \<AA>\<^sub>\<nu>_FG_language:
   "\<phi> \<in> \<nu>LTL \<Longrightarrow> to_stream w \<in> DCA.language (\<AA>\<^sub>\<nu>_FG \<phi>) \<longleftrightarrow> w \<Turnstile>\<^sub>n F\<^sub>n (G\<^sub>n \<phi>)"
 proof -
   assume "\<phi> \<in> \<nu>LTL"
 
   then have "w \<Turnstile>\<^sub>n F\<^sub>n (G\<^sub>n \<phi>) \<longleftrightarrow> (\<exists>k. \<forall>j. \<not> af (G\<^sub>n \<phi>) (w[k \<rightarrow> j]) \<sim>\<^sub>L false\<^sub>n)"
     using ltl_lang_equivalence.af_\<nu>LTL_FG by blast
 
   also have "\<dots> \<longleftrightarrow> (\<exists>n. \<forall>k>n. \<not> af\<^sub>G \<phi> (G\<^sub>n \<phi>) (w[0 \<rightarrow> k]) \<sim> false\<^sub>n)"
     using af\<^sub>G_semantics_ltr af\<^sub>G_semantics_rtl
     using \<open>\<phi> \<in> \<nu>LTL\<close> af_\<nu>LTL_FG calculation by blast
 
   also have "\<dots> \<longleftrightarrow> (\<exists>n. \<forall>k\<ge>n. \<not> af\<^sub>G \<phi> (G\<^sub>n \<phi>) (w[0 \<rightarrow> Suc k]) \<sim> false\<^sub>n)"
     by (metis less_Suc_eq_le less_imp_Suc_add)
 
-  also have "\<dots> \<longleftrightarrow> \<not> infs (\<lambda>\<psi>. \<psi> = \<up>false\<^sub>n) (DCA.trace (\<AA>\<^sub>\<nu>_FG \<phi>) (to_stream w) (Abs (G\<^sub>n \<phi>)))"
+  also have "\<dots> \<longleftrightarrow> fins (\<lambda>\<psi>. \<psi> = \<up>false\<^sub>n) (DCA.trace (\<AA>\<^sub>\<nu>_FG \<phi>) (to_stream w) (Abs (G\<^sub>n \<phi>)))"
     by (simp add: infs_snth \<AA>\<^sub>\<nu>_FG_def DBA.succ_def af\<^sub>G_lifted_semantics Abs_eq[symmetric] af_letter\<^sub>G_lifted_semantics)
 
   also have "\<dots> \<longleftrightarrow> to_stream w \<in> DCA.language (\<AA>\<^sub>\<nu>_FG \<phi>)"
     unfolding \<AA>\<^sub>\<nu>_FG_def dca.initial_def dca.rejecting_def
     by (metis dca_run DCA.language DCA.language_elim dca.sel(2) dca.sel(4))
 
   finally show ?thesis
     by simp
 qed
 
 
 lemma \<AA>\<^sub>\<mu>_nodes:
   "DBA.nodes (\<AA>\<^sub>\<mu> \<phi>) \<subseteq> {Abs \<psi> | \<psi>. nested_prop_atoms \<psi> \<subseteq> nested_prop_atoms \<phi>}"
   unfolding \<AA>\<^sub>\<mu>_def transition_system_initial.nodes_alt_def
   using af_lifted_semantics af_nested_prop_atoms by fastforce
 
 lemma \<AA>\<^sub>\<mu>_GF_nodes:
   "DBA.nodes (\<AA>\<^sub>\<mu>_GF \<phi>) \<subseteq> {Abs \<psi> | \<psi>. nested_prop_atoms \<psi> \<subseteq> nested_prop_atoms (F\<^sub>n \<phi>)}"
   unfolding \<AA>\<^sub>\<mu>_GF_def DBA.nodes_def transition_system_initial.nodes_alt_def transition_system.reachable_alt_def
   using af\<^sub>F_nested_prop_atoms[of "F\<^sub>n \<phi>"] by (auto simp: af\<^sub>F_lifted_semantics)
 
 lemma \<AA>\<^sub>\<nu>_nodes:
   "DCA.nodes (\<AA>\<^sub>\<nu> \<phi>) \<subseteq> {Abs \<psi> | \<psi>. nested_prop_atoms \<psi> \<subseteq> nested_prop_atoms \<phi>}"
   unfolding \<AA>\<^sub>\<nu>_def transition_system_initial.nodes_alt_def
   using af_lifted_semantics af_nested_prop_atoms by fastforce
 
 lemma \<AA>\<^sub>\<nu>_FG_nodes:
   "DCA.nodes (\<AA>\<^sub>\<nu>_FG \<phi>) \<subseteq> {Abs \<psi> | \<psi>. nested_prop_atoms \<psi> \<subseteq> nested_prop_atoms (G\<^sub>n \<phi>)}"
   unfolding \<AA>\<^sub>\<nu>_FG_def DCA.nodes_def transition_system_initial.nodes_alt_def transition_system.reachable_alt_def
   using af\<^sub>G_nested_prop_atoms[of "G\<^sub>n \<phi>"] by (auto simp: af\<^sub>G_lifted_semantics)
 
 
 
 subsection \<open>A DCA checking the GF-advice Function\<close>
 
 definition \<CC> :: "'a ltln \<Rightarrow> 'a ltln set \<Rightarrow> ('a set, 'ltlq \<times> 'ltlq) dca" where
   "\<CC> \<phi> X = dca UNIV (Abs \<phi>, Abs (\<phi>[X]\<^sub>\<nu>)) (\<up>afletter\<^sub>\<nu> X) (\<lambda>p. snd p = \<up>false\<^sub>n)"
 
 lemma \<CC>_language:
   "to_stream w \<in> DCA.language (\<CC> \<phi> X) \<longleftrightarrow> (\<exists>i. suffix i w \<Turnstile>\<^sub>n af \<phi> (prefix i w)[X]\<^sub>\<nu>)"
 proof -
 
   have "(\<exists>i. suffix i w \<Turnstile>\<^sub>n af \<phi> (prefix i w)[X]\<^sub>\<nu>)
         \<longleftrightarrow> (\<exists>m. \<forall>k\<ge>m. \<not> snd (af\<^sub>\<nu> X (\<phi>, \<phi>[X]\<^sub>\<nu>) (prefix (Suc k) w)) \<sim> false\<^sub>n)"
     using af\<^sub>\<nu>_semantics_ltr af\<^sub>\<nu>_semantics_rtl by blast
 
-  also have "\<dots> \<longleftrightarrow> \<not> infs (\<lambda>p. snd p = \<up>false\<^sub>n) (DCA.trace (\<CC> \<phi> X) (to_stream w) (Abs \<phi>, Abs (\<phi>[X]\<^sub>\<nu>)))"
+  also have "\<dots> \<longleftrightarrow> fins (\<lambda>p. snd p = \<up>false\<^sub>n) (DCA.trace (\<CC> \<phi> X) (to_stream w) (Abs \<phi>, Abs (\<phi>[X]\<^sub>\<nu>)))"
     by(simp add: infs_snth \<CC>_def DCA.succ_def af\<^sub>\<nu>_lifted_semantics af_letter\<^sub>\<nu>_lifted_semantics Abs_eq)
 
   also have "\<dots> \<longleftrightarrow> to_stream w \<in> DCA.language (\<CC> \<phi> X)"
     by (simp add: \<CC>_def dca.initial_def dca.rejecting_def DCA.language_def dca_run)
 
   finally show ?thesis
     by blast
 qed
 
 
 lemma \<CC>_nodes:
   "DCA.nodes (\<CC> \<phi> X) \<subseteq> {Abs \<psi> | \<psi>. nested_prop_atoms \<psi> \<subseteq> nested_prop_atoms \<phi>} \<times> {Abs \<psi> | \<psi>. nested_prop_atoms \<psi> \<subseteq> nested_prop_atoms\<^sub>\<nu> \<phi> X}"
   unfolding \<CC>_def DCA.nodes_def transition_system_initial.nodes_alt_def transition_system.reachable_alt_def
   apply (auto simp add: af\<^sub>\<nu>_lifted_semantics af_letter\<^sub>\<nu>_lifted_semantics)
   using af\<^sub>\<nu>_fst_nested_prop_atoms apply force
   using GF_advice_nested_prop_atoms\<^sub>\<nu> af\<^sub>\<nu>_snd_nested_prop_atoms dra_construction_axioms by fastforce
 
 
 
 subsection \<open>A DRA for each combination of sets X and Y\<close>
 
 lemma dba_language:
   "(\<And>w. to_stream w \<in> DBA.language \<AA> \<longleftrightarrow> w \<Turnstile>\<^sub>n \<phi>) \<Longrightarrow> DBA.language \<AA> = {w. to_omega w \<Turnstile>\<^sub>n \<phi>}"
   by (metis (mono_tags, lifting) Collect_cong DBA.language_def mem_Collect_eq to_stream_to_omega)
 
 lemma dca_language:
   "(\<And>w. to_stream w \<in> DCA.language \<AA> \<longleftrightarrow> w \<Turnstile>\<^sub>n \<phi>) \<Longrightarrow> DCA.language \<AA> = {w. to_omega w \<Turnstile>\<^sub>n \<phi>}"
   by (metis (mono_tags, lifting) Collect_cong DCA.language_def mem_Collect_eq to_stream_to_omega)
 
 
 definition \<AA>\<^sub>1 :: "'a ltln \<Rightarrow> 'a ltln list \<Rightarrow> ('a set, 'ltlq \<times> 'ltlq) dca" where
   "\<AA>\<^sub>1 \<phi> xs = \<CC> \<phi> (set xs)"
 
 lemma \<AA>\<^sub>1_language:
   "to_omega ` DCA.language (\<AA>\<^sub>1 \<phi> xs) = L\<^sub>1 \<phi> (set xs)"
   by (simp add: \<AA>\<^sub>1_def L\<^sub>1_def set_eq_iff \<CC>_language)
 
 lemma \<AA>\<^sub>1_alphabet:
   "DCA.alphabet (\<AA>\<^sub>1 \<phi> xs) = UNIV"
   unfolding \<AA>\<^sub>1_def \<CC>_def by simp
 
 
 definition \<AA>\<^sub>2 :: "'a ltln list \<Rightarrow> 'a ltln list \<Rightarrow> ('a set, 'ltlq list degen) dba" where
   "\<AA>\<^sub>2 xs ys = dbail (map (\<lambda>\<psi>. \<AA>\<^sub>\<mu>_GF (\<psi>[set ys]\<^sub>\<mu>)) xs)"
 
 lemma \<AA>\<^sub>2_language:
   "to_omega ` DBA.language (\<AA>\<^sub>2 xs ys) = L\<^sub>2 (set xs) (set ys)"
   by (simp add: \<AA>\<^sub>2_def L\<^sub>2_def set_eq_iff dba_language[OF \<AA>\<^sub>\<mu>_GF_language[OF FG_advice_\<mu>LTL(1)]])
 
 lemma \<AA>\<^sub>2_alphabet:
   "DBA.alphabet (\<AA>\<^sub>2 xs ys) = UNIV"
   by (simp add: \<AA>\<^sub>2_def \<AA>\<^sub>\<mu>_GF_def dbail_def dbgail_def)
 
 
 definition \<AA>\<^sub>3 :: "'a ltln list \<Rightarrow> 'a ltln list \<Rightarrow> ('a set, 'ltlq list) dca" where
   "\<AA>\<^sub>3 xs ys = dcail (map (\<lambda>\<psi>. \<AA>\<^sub>\<nu>_FG (\<psi>[set xs]\<^sub>\<nu>)) ys)"
 
 lemma \<AA>\<^sub>3_language:
   "to_omega ` DCA.language (\<AA>\<^sub>3 xs ys) = L\<^sub>3 (set xs) (set ys)"
   by (simp add: \<AA>\<^sub>3_def L\<^sub>3_def set_eq_iff dca_language[OF \<AA>\<^sub>\<nu>_FG_language[OF GF_advice_\<nu>LTL(1)]])
 
 lemma \<AA>\<^sub>3_alphabet:
   "DCA.alphabet (\<AA>\<^sub>3 xs ys) = UNIV"
   by (simp add: \<AA>\<^sub>3_def \<AA>\<^sub>\<nu>_FG_def dcail_def)
 
 
 definition "\<AA>' \<phi> xs ys = dbcrai (\<AA>\<^sub>2 xs ys) (dcai (\<AA>\<^sub>1 \<phi> xs) (\<AA>\<^sub>3 xs ys))"
 
 lemma \<AA>'_language:
   "to_omega ` DRA.language (\<AA>' \<phi> xs ys) = (L\<^sub>1 \<phi> (set xs) \<inter> L\<^sub>2 (set xs) (set ys) \<inter> L\<^sub>3 (set xs) (set ys))"
   by (simp add: \<AA>'_def \<AA>\<^sub>1_language \<AA>\<^sub>2_language \<AA>\<^sub>3_language) fastforce
 
 lemma \<AA>'_alphabet:
   "DRA.alphabet (\<AA>' \<phi> xs ys) = UNIV"
   by (simp add: \<AA>'_def dbcrai_def dcai_def \<AA>\<^sub>1_alphabet \<AA>\<^sub>2_alphabet \<AA>\<^sub>3_alphabet)
 
 
 
 subsection \<open>A DRA for @{term "L(\<phi>)"}\<close>
 
 definition "ltl_to_dra \<phi> = draul (map (\<lambda>(xs, ys). \<AA>' \<phi> xs ys) (advice_sets \<phi>))"
 
 lemma ltl_to_dra_language:
   "to_omega ` DRA.language (ltl_to_dra \<phi>) = language_ltln \<phi>"
 proof -
   have 1: "INTER (set (map (\<lambda>(x, y). \<AA>' \<phi> x y) (advice_sets \<phi>))) dra.alphabet = UNION (set (map (\<lambda>(x, y). \<AA>' \<phi> x y) (advice_sets \<phi>))) dra.alphabet"
     by (induction "advice_sets \<phi>") (metis advice_sets_not_empty, simp add: \<AA>'_alphabet split_def advice_sets_not_empty)
 
   have "language_ltln \<phi> = \<Union> {(L\<^sub>1 \<phi> X \<inter> L\<^sub>2 X Y \<inter> L\<^sub>3 X Y) | X Y. X \<subseteq> subformulas\<^sub>\<mu> \<phi> \<and> Y \<subseteq> subformulas\<^sub>\<nu> \<phi>}"
     unfolding master_theorem_language by auto
   also have "\<dots> = \<Union> {L\<^sub>1 \<phi> (set xs) \<inter> L\<^sub>2 (set xs) (set ys) \<inter> L\<^sub>3 (set xs) (set ys) | xs ys. (xs, ys) \<in> set (advice_sets \<phi>)}"
     unfolding advice_sets_subformulas by (metis (no_types, lifting))
   also have "\<dots> = \<Union> {to_omega ` DRA.language (\<AA>' \<phi> xs ys) | xs ys. (xs, ys) \<in> set (advice_sets \<phi>)}"
     by (simp add: \<AA>'_language)
   finally show ?thesis
     unfolding ltl_to_dra_def draul_language[OF 1] by auto
 qed
 
 lemma ltl_to_dra_alphabet:
   "alphabet (ltl_to_dra \<phi>) = UNIV"
   by (auto simp: ltl_to_dra_def draul_def \<AA>'_alphabet split: prod.split)
      (insert advice_sets_subformulas, blast)
 
 
 
 subsection \<open>Setting the Alphabet of a DRA\<close>
 
 definition dra_set_alphabet :: "('a set, 'b) dra \<Rightarrow> 'a set set \<Rightarrow> ('a set, 'b) dra"
 where
   "dra_set_alphabet \<AA> \<Sigma> = dra \<Sigma> (initial \<AA>) (succ \<AA>) (accepting \<AA>)"
 
 lemma dra_set_alphabet_language:
   "\<Sigma> \<subseteq> alphabet \<AA> \<Longrightarrow> language (dra_set_alphabet \<AA> \<Sigma>) = language \<AA> \<inter> {s. sset s \<subseteq> \<Sigma>}"
   by (auto simp add: dra_set_alphabet_def language_def set_eq_iff DRA.run_alt_def)
 
 lemma dra_set_alphabet_alphabet[simp]:
   "alphabet (dra_set_alphabet \<AA> \<Sigma>) = \<Sigma>"
   unfolding dra_set_alphabet_def by simp
 
 lemma dra_set_alphabet_nodes:
   "\<Sigma> \<subseteq> alphabet \<AA> \<Longrightarrow> DRA.nodes (dra_set_alphabet \<AA> \<Sigma>) \<subseteq> DRA.nodes \<AA>"
   unfolding dra_set_alphabet_def DRA.nodes_def transition_system_initial.nodes_alt_def transition_system.reachable_alt_def
   by auto (metis DRA.path_alt_def DRA.path_def dra.sel(1) dra.sel(3) subset_trans)
 
 
 
 subsection \<open>A DRA for @{term "L(\<phi>)"} with a finite alphabet\<close>
 
 definition "ltl_to_dra_alphabet \<phi> Ap = dra_set_alphabet (ltl_to_dra \<phi>) (Pow Ap)"
 
 lemma ltl_to_dra_alphabet_language:
   assumes
     "atoms_ltln \<phi> \<subseteq> Ap"
   shows
     "to_omega ` language (ltl_to_dra_alphabet \<phi> Ap) = language_ltln \<phi> \<inter> {w. range w \<subseteq> Pow Ap}"
 proof -
   have 1: "Pow Ap \<subseteq> alphabet (ltl_to_dra \<phi>)"
     unfolding ltl_to_dra_alphabet by simp
 
   show ?thesis
     unfolding ltl_to_dra_alphabet_def dra_set_alphabet_language[OF 1]
     by (simp add: ltl_to_dra_language sset_range) force
 qed
 
 lemma ltl_to_dra_alphabet_alphabet[simp]:
   "alphabet (ltl_to_dra_alphabet \<phi> Ap) = Pow Ap"
   unfolding ltl_to_dra_alphabet_def by simp
 
 lemma ltl_to_dra_alphabet_nodes:
   "DRA.nodes (ltl_to_dra_alphabet \<phi> Ap) \<subseteq> DRA.nodes (ltl_to_dra \<phi>)"
   unfolding ltl_to_dra_alphabet_def
   by (rule dra_set_alphabet_nodes) (simp add: ltl_to_dra_alphabet)
 
 end
 
 end
diff --git a/thys/Transition_Systems_and_Automata/Automata/DCA/DCA.thy b/thys/Transition_Systems_and_Automata/Automata/DCA/DCA.thy
--- a/thys/Transition_Systems_and_Automata/Automata/DCA/DCA.thy
+++ b/thys/Transition_Systems_and_Automata/Automata/DCA/DCA.thy
@@ -1,62 +1,62 @@
 section \<open>Deterministic Co-Büchi Automata\<close>
 
 theory DCA
 imports
   "../../Basic/Sequence_Zip"
   "../../Basic/Acceptance"
   "../../Transition_Systems/Transition_System"
   "../../Transition_Systems/Transition_System_Extra"
   "../../Transition_Systems/Transition_System_Construction"
 begin
 
   datatype ('label, 'state) dca = dca
     (alphabet: "'label set")
     (initial: "'state")
     (succ: "'label \<Rightarrow> 'state \<Rightarrow> 'state")
     (rejecting: "'state \<Rightarrow> bool")
 
   global_interpretation dca: transition_system_initial
     "succ A" "\<lambda> a p. a \<in> alphabet A" "\<lambda> p. p = initial A"
     for A
     defines path = dca.path and run = dca.run and reachable = dca.reachable and nodes = dca.nodes and
       enableds = dca.enableds and paths = dca.paths and runs = dca.runs
     by this
 
   abbreviation target where "target \<equiv> dca.target"
   abbreviation states where "states \<equiv> dca.states"
   abbreviation trace where "trace \<equiv> dca.trace"
 
   abbreviation successors :: "('label, 'state) dca \<Rightarrow> 'state \<Rightarrow> 'state set" where
     "successors \<equiv> dca.successors TYPE('label)"
 
   lemma path_alt_def: "path A w p \<longleftrightarrow> set w \<subseteq> alphabet A"
   unfolding lists_iff_set[symmetric]
   proof
     show "w \<in> lists (alphabet A)" if "path A w p" using that by (induct arbitrary: p) (auto)
     show "path A w p" if "w \<in> lists (alphabet A)" using that by (induct arbitrary: p) (auto)
   qed
   lemma run_alt_def: "run A w p \<longleftrightarrow> sset w \<subseteq> alphabet A"
   unfolding streams_iff_sset[symmetric]
   proof
     show "w \<in> streams (alphabet A)" if "run A w p"
       using that by (coinduction arbitrary: w p) (force elim: dca.run.cases)
     show "run A w p" if "w \<in> streams (alphabet A)"
       using that by (coinduction arbitrary: w p) (force elim: streams.cases)
   qed
 
   definition language :: "('label, 'state) dca \<Rightarrow> 'label stream set" where
-    "language A \<equiv> {w. run A w (initial A) \<and> \<not> infs (rejecting A) (trace A w (initial A))}"
+    "language A \<equiv> {w. run A w (initial A) \<and> fins (rejecting A) (trace A w (initial A))}"
 
   lemma language[intro]:
-    assumes "run A w (initial A)" "\<not> infs (rejecting A) (trace A w (initial A))"
+    assumes "run A w (initial A)" "fins (rejecting A) (trace A w (initial A))"
     shows "w \<in> language A"
     using assms unfolding language_def by auto
   lemma language_elim[elim]:
     assumes "w \<in> language A"
-    obtains "run A w (initial A)" "\<not> infs (rejecting A) (trace A w (initial A))"
+    obtains "run A w (initial A)" "fins (rejecting A) (trace A w (initial A))"
     using assms unfolding language_def by auto
 
   lemma language_alphabet: "language A \<subseteq> streams (alphabet A)"
     unfolding language_def run_alt_def using sset_streams by auto
 
 end
\ No newline at end of file
diff --git a/thys/Transition_Systems_and_Automata/Automata/DCA/DCA_Combine.thy b/thys/Transition_Systems_and_Automata/Automata/DCA/DCA_Combine.thy
--- a/thys/Transition_Systems_and_Automata/Automata/DCA/DCA_Combine.thy
+++ b/thys/Transition_Systems_and_Automata/Automata/DCA/DCA_Combine.thy
@@ -1,298 +1,298 @@
 section \<open>Deterministic Co-Büchi Automata Combinations\<close>
 
 theory DCA_Combine
 imports "DCA" "DGCA"
 begin
 
   definition dcai :: "('label, 'state\<^sub>1) dca \<Rightarrow> ('label, 'state\<^sub>2) dca \<Rightarrow>
     ('label, 'state\<^sub>1 \<times> 'state\<^sub>2) dca" where
     "dcai A B \<equiv> dca
       (dca.alphabet A \<inter> dca.alphabet B)
       (dca.initial A, dca.initial B)
       (\<lambda> a (p, q). (dca.succ A a p, dca.succ B a q))
       (\<lambda> (p, q). dca.rejecting A p \<or> dca.rejecting B q)"
 
   lemma dcai_fst[iff]: "infs (P \<circ> fst) (dca.trace (dcai A B) w (p, q)) \<longleftrightarrow> infs P (dca.trace A w p)"
   proof -
     let ?t = "dca.trace (dcai A B) w (p, q)"
     have "infs (P \<circ> fst) ?t \<longleftrightarrow> infs P (smap fst ?t)" by (simp add: comp_def)
     also have "smap fst ?t = dca.trace A w p" unfolding dcai_def by (coinduction arbitrary: w p q) (auto)
     finally show ?thesis by this
   qed
   lemma dcai_snd[iff]: "infs (P \<circ> snd) (dca.trace (dcai A B) w (p, q)) \<longleftrightarrow> infs P (dca.trace B w q)"
   proof -
     let ?t = "dca.trace (dcai A B) w (p, q)"
     have "infs (P \<circ> snd) ?t \<longleftrightarrow> infs P (smap snd ?t)" by (simp add: comp_def)
     also have "smap snd ?t = dca.trace B w q" unfolding dcai_def by (coinduction arbitrary: w p q) (auto)
     finally show ?thesis by this
   qed
   lemma dcai_nodes_fst[intro]: "fst ` DCA.nodes (dcai A B) \<subseteq> DCA.nodes A"
   proof (rule subsetI, erule imageE)
     fix pq p
     assume "pq \<in> DCA.nodes (dcai A B)" "p = fst pq"
     then show "p \<in> DCA.nodes A" unfolding dcai_def by (induct arbitrary: p) (auto)
   qed
   lemma dcai_nodes_snd[intro]: "snd ` DCA.nodes (dcai A B) \<subseteq> DCA.nodes B"
   proof (rule subsetI, erule imageE)
     fix pq q
     assume "pq \<in> DCA.nodes (dcai A B)" "q = snd pq"
     then show "q \<in> DCA.nodes B" unfolding dcai_def by (induct arbitrary: q) (auto)
   qed
 
   lemma dcai_nodes_finite[intro]:
     assumes "finite (DCA.nodes A)" "finite (DCA.nodes B)"
     shows "finite (DCA.nodes (dcai A B))"
   proof (rule finite_subset)
     show "DCA.nodes (dcai A B) \<subseteq> DCA.nodes A \<times> DCA.nodes B"
       using dcai_nodes_fst dcai_nodes_snd unfolding image_subset_iff by force
     show "finite (DCA.nodes A \<times> DCA.nodes B)" using assms by simp
   qed
   lemma dcai_nodes_card[intro]:
     assumes "finite (DCA.nodes A)" "finite (DCA.nodes B)"
     shows "card (DCA.nodes (dcai A B)) \<le> card (DCA.nodes A) * card (DCA.nodes B)"
   proof -
     have "card (DCA.nodes (dcai A B)) \<le> card (DCA.nodes A \<times> DCA.nodes B)"
     proof (rule card_mono)
       show "finite (DCA.nodes A \<times> DCA.nodes B)" using assms by simp
       show "DCA.nodes (dcai A B) \<subseteq> DCA.nodes A \<times> DCA.nodes B"
         using dcai_nodes_fst dcai_nodes_snd unfolding image_subset_iff by force
     qed
     also have "\<dots> = card (DCA.nodes A) * card (DCA.nodes B)" using card_cartesian_product by this
     finally show ?thesis by this
   qed
 
   lemma dcai_language[simp]: "DCA.language (dcai A B) = DCA.language A \<inter> DCA.language B"
   proof -
     have 1: "dca.alphabet (dcai A B) = dca.alphabet A \<inter> dca.alphabet B" unfolding dcai_def by simp
     have 2: "dca.initial (dcai A B) = (dca.initial A, dca.initial B)" unfolding dcai_def by simp
     have 3: "dca.rejecting (dcai A B) = (\<lambda> pq. (dca.rejecting A \<circ> fst) pq \<or> (dca.rejecting B \<circ> snd) pq)"
       unfolding dcai_def by auto
     have 4: "infs (dca.rejecting (dcai A B)) (DCA.trace (dcai A B) w (p, q)) \<longleftrightarrow>
       infs (dca.rejecting A) (DCA.trace A w p) \<or> infs (dca.rejecting B) (DCA.trace B w q)" for w p q
       unfolding 3 by blast
     show ?thesis unfolding DCA.language_def DCA.run_alt_def 1 2 4 by auto
   qed
 
   definition dcail :: "('label, 'state) dca list \<Rightarrow> ('label, 'state list) dca" where
     "dcail AA \<equiv> dca
       (INTER (set AA) dca.alphabet)
       (map dca.initial AA)
       (\<lambda> a pp. map2 (\<lambda> A p. dca.succ A a p) AA pp)
       (\<lambda> pp. \<exists> k < length AA. dca.rejecting (AA ! k) (pp ! k))"
 
   lemma dcail_trace_smap:
     assumes "length pp = length AA" "k < length AA"
     shows "smap (\<lambda> pp. pp ! k) (dca.trace (dcail AA) w pp) = dca.trace (AA ! k) w (pp ! k)"
     using assms unfolding dcail_def by (coinduction arbitrary: w pp) (force)
   lemma dcail_nodes_length:
     assumes "pp \<in> DCA.nodes (dcail AA)"
     shows "length pp = length AA"
     using assms unfolding dcail_def by induct auto
   lemma dcail_nodes[intro]:
     assumes "pp \<in> DCA.nodes (dcail AA)" "k < length pp"
     shows "pp ! k \<in> DCA.nodes (AA ! k)"
     using assms unfolding dcail_def by induct auto
 
   lemma dcail_finite[intro]:
     assumes "list_all (finite \<circ> DCA.nodes) AA"
     shows "finite (DCA.nodes (dcail AA))"
   proof (rule finite_subset)
     show "DCA.nodes (dcail AA) \<subseteq> listset (map DCA.nodes AA)"
       by (force simp: listset_member list_all2_conv_all_nth dcail_nodes_length)
     have "finite (listset (map DCA.nodes AA)) \<longleftrightarrow> list_all finite (map DCA.nodes AA)"
       by (rule listset_finite) (auto simp: list_all_iff)
     then show "finite (listset (map DCA.nodes AA))" using assms by (simp add: list.pred_map)
   qed
   lemma dcail_nodes_card:
     assumes "list_all (finite \<circ> DCA.nodes) AA"
     shows "card (DCA.nodes (dcail AA)) \<le> prod_list (map (card \<circ> DCA.nodes) AA)"
   proof -
     have "card (DCA.nodes (dcail AA)) \<le> card (listset (map DCA.nodes AA))"
     proof (rule card_mono)
       have "finite (listset (map DCA.nodes AA)) \<longleftrightarrow> list_all finite (map DCA.nodes AA)"
         by (rule listset_finite) (auto simp: list_all_iff)
       then show "finite (listset (map DCA.nodes AA))" using assms by (simp add: list.pred_map)
       show "DCA.nodes (dcail AA) \<subseteq> listset (map DCA.nodes AA)"
         by (force simp: listset_member list_all2_conv_all_nth dcail_nodes_length)
     qed
     also have "\<dots> = prod_list (map (card \<circ> DCA.nodes) AA)" by simp
     finally show ?thesis by this
   qed
 
   lemma dcail_language[simp]: "DCA.language (dcail AA) = INTER (set AA) DCA.language"
   proof safe
     fix A w
     assume 1: "w \<in> DCA.language (dcail AA)" "A \<in> set AA"
     obtain 2:
       "dca.run (dcail AA) w (dca.initial (dcail AA))"
-      "\<not> infs (dca.rejecting (dcail AA)) (dca.trace (dcail AA) w (dca.initial (dcail AA)))"
+      "fins (dca.rejecting (dcail AA)) (dca.trace (dcail AA) w (dca.initial (dcail AA)))"
       using 1(1) by rule
     obtain k where 3: "A = AA ! k" "k < length AA" using 1(2) unfolding in_set_conv_nth by auto
-    have 4: "\<not> infs (\<lambda> pp. dca.rejecting A (pp ! k)) (dca.trace (dcail AA) w (map dca.initial AA))"
+    have 4: "fins (\<lambda> pp. dca.rejecting A (pp ! k)) (dca.trace (dcail AA) w (map dca.initial AA))"
       using 2(2) 3 unfolding dcail_def by auto
     show "w \<in> DCA.language A"
     proof
       show "dca.run A w (dca.initial A)"
         using 1(2) 2(1) unfolding DCA.run_alt_def dcail_def by auto
-      have "True \<longleftrightarrow> \<not> infs (\<lambda> pp. dca.rejecting A (pp ! k)) (dca.trace (dcail AA) w (map dca.initial AA))"
+      have "True \<longleftrightarrow> fins (\<lambda> pp. dca.rejecting A (pp ! k)) (dca.trace (dcail AA) w (map dca.initial AA))"
         using 4 by simp
-      also have "\<dots> \<longleftrightarrow> \<not> infs (dca.rejecting A) (smap (\<lambda> pp. pp ! k)
+      also have "\<dots> \<longleftrightarrow> fins (dca.rejecting A) (smap (\<lambda> pp. pp ! k)
         (dca.trace (dcail AA) w (map dca.initial AA)))" by (simp add: comp_def)
       also have "smap (\<lambda> pp. pp ! k) (dca.trace (dcail AA) w (map dca.initial AA)) =
         dca.trace (AA ! k) w (map dca.initial AA ! k)" using 3(2) by (fastforce intro: dcail_trace_smap)
       also have "\<dots> = dca.trace A w (dca.initial A)" using 3 by auto
-      finally show "\<not> infs (dca.rejecting A) (DCA.trace A w (dca.initial A))" by simp
+      finally show "fins (dca.rejecting A) (DCA.trace A w (dca.initial A))" by simp
     qed
   next
     fix w
     assume 1: "w \<in> INTER (set AA) DCA.language"
-    have 2: "dca.run A w (dca.initial A)" "\<not> infs (dca.rejecting A) (dca.trace A w (dca.initial A))"
+    have 2: "dca.run A w (dca.initial A)" "fins (dca.rejecting A) (dca.trace A w (dca.initial A))"
       if "A \<in> set AA" for A using 1 that by auto
-    have 3: "\<not> infs (\<lambda> pp. dca.rejecting (AA ! k) (pp ! k)) (dca.trace (dcail AA) w (map dca.initial AA))"
+    have 3: "fins (\<lambda> pp. dca.rejecting (AA ! k) (pp ! k)) (dca.trace (dcail AA) w (map dca.initial AA))"
       if "k < length AA" for k
     proof -
-      have "True \<longleftrightarrow> \<not> infs (dca.rejecting (AA ! k)) (dca.trace (AA ! k) w (map dca.initial AA ! k))"
+      have "True \<longleftrightarrow> fins (dca.rejecting (AA ! k)) (dca.trace (AA ! k) w (map dca.initial AA ! k))"
         using 2(2) that by auto
       also have "dca.trace (AA ! k) w (map dca.initial AA ! k) =
         smap (\<lambda> pp. pp ! k) (dca.trace (dcail AA) w (map dca.initial AA))"
         using that by (fastforce intro: dcail_trace_smap[symmetric])
       also have "infs (dca.rejecting (AA ! k)) \<dots> \<longleftrightarrow> infs (\<lambda> pp. dca.rejecting (AA ! k) (pp ! k))
         (dca.trace (dcail AA) w (map dca.initial AA))" by (simp add: comp_def)
       finally show ?thesis by simp
     qed
     show "w \<in> DCA.language (dcail AA)"
     proof
       show "dca.run (dcail AA) w (dca.initial (dcail AA))"
         using 2(1) unfolding DCA.run_alt_def dcail_def by auto
-      show "\<not> infs (dca.rejecting (dcail AA)) (dca.trace (dcail AA) w (dca.initial (dcail AA)))"
+      show "fins (dca.rejecting (dcail AA)) (dca.trace (dcail AA) w (dca.initial (dcail AA)))"
         using 3 unfolding dcail_def by auto
     qed
   qed
 
   definition dcgaul :: "('label, 'state) dca list \<Rightarrow> ('label, 'state list) dgca" where
     "dcgaul AA \<equiv> dgca
       (UNION (set AA) dca.alphabet)
       (map dca.initial AA)
       (\<lambda> a pp. map2 (\<lambda> A p. dca.succ A a p) AA pp)
       (map (\<lambda> k pp. dca.rejecting (AA ! k) (pp ! k)) [0 ..< length AA])"
 
   lemma dcgaul_trace_smap:
     assumes "length pp = length AA" "k < length AA"
     shows "smap (\<lambda> pp. pp ! k) (dgca.trace (dcgaul AA) w pp) = dca.trace (AA ! k) w (pp ! k)"
     using assms unfolding dcgaul_def by (coinduction arbitrary: w pp) (force)
   lemma dcgaul_nodes_length:
     assumes "pp \<in> DGCA.nodes (dcgaul AA)"
     shows "length pp = length AA"
     using assms unfolding dcgaul_def by induct auto
   lemma dcgaul_nodes[intro]:
     assumes "INTER (set AA) dca.alphabet = UNION (set AA) dca.alphabet"
     assumes "pp \<in> DGCA.nodes (dcgaul AA)" "k < length pp"
     shows "pp ! k \<in> DCA.nodes (AA ! k)"
     using assms(2, 3, 1) unfolding dcgaul_def by induct force+
 
   lemma dcgaul_nodes_finite[intro]:
     assumes "INTER (set AA) dca.alphabet = UNION (set AA) dca.alphabet"
     assumes "list_all (finite \<circ> DCA.nodes) AA"
     shows "finite (DGCA.nodes (dcgaul AA))"
   proof (rule finite_subset)
     show "DGCA.nodes (dcgaul AA) \<subseteq> listset (map DCA.nodes AA)"
       using assms(1) by (force simp: listset_member list_all2_conv_all_nth dcgaul_nodes_length)
     have "finite (listset (map DCA.nodes AA)) \<longleftrightarrow> list_all finite (map DCA.nodes AA)"
       by (rule listset_finite) (auto simp: list_all_iff)
     then show "finite (listset (map DCA.nodes AA))" using assms(2) by (simp add: list.pred_map)
   qed
   lemma dcgaul_nodes_card:
     assumes "INTER (set AA) dca.alphabet = UNION (set AA) dca.alphabet"
     assumes "list_all (finite \<circ> DCA.nodes) AA"
     shows "card (DGCA.nodes (dcgaul AA)) \<le> prod_list (map (card \<circ> DCA.nodes) AA)"
   proof -
     have "card (DGCA.nodes (dcgaul AA)) \<le> card (listset (map DCA.nodes AA))"
     proof (rule card_mono)
       have "finite (listset (map DCA.nodes AA)) \<longleftrightarrow> list_all finite (map DCA.nodes AA)"
         by (rule listset_finite) (auto simp: list_all_iff)
       then show "finite (listset (map DCA.nodes AA))" using assms(2) by (simp add: list.pred_map)
       show "DGCA.nodes (dcgaul AA) \<subseteq> listset (map DCA.nodes AA)"
         using assms(1) by (force simp: listset_member list_all2_conv_all_nth dcgaul_nodes_length)
     qed
     also have "\<dots> = prod_list (map (card \<circ> DCA.nodes) AA)" by simp
     finally show ?thesis by this
   qed
 
   lemma dcgaul_language[simp]:
     assumes "INTER (set AA) dca.alphabet = UNION (set AA) dca.alphabet"
     shows "DGCA.language (dcgaul AA) = UNION (set AA) DCA.language"
   proof safe
     fix w
     assume 1: "w \<in> DGCA.language (dcgaul AA)"
     obtain k where 2:
       "dgca.run (dcgaul AA) w (dgca.initial (dcgaul AA))"
       "k < length AA"
-      "\<not> infs (\<lambda> pp. dca.rejecting (AA ! k) (pp ! k)) (dgca.trace (dcgaul AA) w (dgca.initial (dcgaul AA)))"
+      "fins (\<lambda> pp. dca.rejecting (AA ! k) (pp ! k)) (dgca.trace (dcgaul AA) w (dgca.initial (dcgaul AA)))"
       using 1 unfolding dcgaul_def by force
     show "w \<in> UNION (set AA) DCA.language"
     proof (intro UN_I DCA.language)
       show "AA ! k \<in> set AA" using 2(2) by simp
       show "dca.run (AA ! k) w (dca.initial (AA ! k))"
         using assms 2(1, 2) unfolding DCA.run_alt_def DGCA.run_alt_def dcgaul_def by force
-      have "True \<longleftrightarrow> \<not> infs (\<lambda> pp. dca.rejecting (AA ! k) (pp ! k))
+      have "True \<longleftrightarrow> fins (\<lambda> pp. dca.rejecting (AA ! k) (pp ! k))
         (dgca.trace (dcgaul AA) w (map dca.initial AA))" using 2(3) unfolding dcgaul_def by auto
-      also have "\<dots> \<longleftrightarrow> \<not> infs (dca.rejecting (AA ! k))
+      also have "\<dots> \<longleftrightarrow> fins (dca.rejecting (AA ! k))
         (smap (\<lambda> pp. pp ! k) (dgca.trace (dcgaul AA) w (map dca.initial AA)))" by (simp add: comp_def)
       also have "smap (\<lambda> pp. pp ! k) (dgca.trace (dcgaul AA) w (map dca.initial AA)) =
         dca.trace (AA ! k) w (map dca.initial AA ! k)" using 2(2) by (fastforce intro: dcgaul_trace_smap)
       also have "\<dots> = dca.trace (AA ! k) w (dca.initial (AA ! k))" using 2(2) by auto
-      finally show "\<not> infs (dca.rejecting (AA ! k)) (dca.trace (AA ! k) w (dca.initial (AA ! k)))" by simp
+      finally show "fins (dca.rejecting (AA ! k)) (dca.trace (AA ! k) w (dca.initial (AA ! k)))" by simp
     qed
   next
     fix A w
     assume 1: "A \<in> set AA" "w \<in> DCA.language A"
-    obtain 2: "dca.run A w (dca.initial A)" "\<not> infs (dca.rejecting A) (dca.trace A w (dca.initial A))"
+    obtain 2: "dca.run A w (dca.initial A)" "fins (dca.rejecting A) (dca.trace A w (dca.initial A))"
       using 1(2) by rule
     obtain k where 3: "A = AA ! k" "k < length AA" using 1(1) unfolding in_set_conv_nth by auto
     show "w \<in> DGCA.language (dcgaul AA)"
     proof (intro DGCA.language bexI cogen)
       show "dgca.run (dcgaul AA) w (dgca.initial (dcgaul AA))"
         using 1(1) 2(1) unfolding DCA.run_alt_def DGCA.run_alt_def dcgaul_def by auto
-      have "True \<longleftrightarrow> \<not> infs (dca.rejecting (AA ! k)) (dca.trace (AA ! k) w (map dca.initial AA ! k))"
+      have "True \<longleftrightarrow> fins (dca.rejecting (AA ! k)) (dca.trace (AA ! k) w (map dca.initial AA ! k))"
         using 2(2) 3 by auto
       also have "dca.trace (AA ! k) w (map dca.initial AA ! k) =
         smap (\<lambda> pp. pp ! k) (dgca.trace (dcgaul AA) w (map dca.initial AA))"
         using 3(2) by (fastforce intro: dcgaul_trace_smap[symmetric])
-      also have "\<not> infs (dca.rejecting (AA ! k)) \<dots> \<longleftrightarrow> \<not> infs (\<lambda> pp. dca.rejecting (AA ! k) (pp ! k))
+      also have "fins (dca.rejecting (AA ! k)) \<dots> \<longleftrightarrow> fins (\<lambda> pp. dca.rejecting (AA ! k) (pp ! k))
         (dgca.trace (dcgaul AA) w (map dca.initial AA))" by (simp add: comp_def)
       also have "map dca.initial AA = dgca.initial (dcgaul AA)" unfolding dcgaul_def by simp
-      finally show "\<not> infs (\<lambda> pp. dca.rejecting (AA ! k) (pp ! k)) (dgca.trace (dcgaul AA) w (dgca.initial (dcgaul AA)))"
+      finally show "fins (\<lambda> pp. dca.rejecting (AA ! k) (pp ! k)) (dgca.trace (dcgaul AA) w (dgca.initial (dcgaul AA)))"
         by simp
       show "(\<lambda> pp. dca.rejecting (AA ! k) (pp ! k)) \<in> set (dgca.rejecting (dcgaul AA))"
         unfolding dcgaul_def using 3(2) by simp
     qed
   qed
 
   definition dcaul :: "('label, 'state) dca list \<Rightarrow> ('label, 'state list degen) dca" where
     "dcaul = dgcad \<circ> dcgaul"
 
   lemma dcaul_nodes_finite[intro]:
     assumes "INTER (set AA) dca.alphabet = UNION (set AA) dca.alphabet"
     assumes "list_all (finite \<circ> DCA.nodes) AA"
     shows "finite (DCA.nodes (dcaul AA))"
     using dcgaul_nodes_finite assms unfolding dcaul_def by auto
   lemma dcaul_nodes_card:
     assumes "INTER (set AA) dca.alphabet = UNION (set AA) dca.alphabet"
     assumes "list_all (finite \<circ> DCA.nodes) AA"
     shows "card (DCA.nodes (dcaul AA)) \<le> max 1 (length AA) * prod_list (map (card \<circ> DCA.nodes) AA)"
   proof -
     have "card (DCA.nodes (dcaul AA)) \<le>
       max 1 (length (dgca.rejecting (dcgaul AA))) * card (DGCA.nodes (dcgaul AA))"
       unfolding dcaul_def using dgcad_nodes_card by simp
     also have "length (dgca.rejecting (dcgaul AA)) = length AA" unfolding dcgaul_def by simp
     also have "card (DGCA.nodes (dcgaul AA)) \<le> prod_list (map (card \<circ> DCA.nodes) AA)"
       using dcgaul_nodes_card assms by this
     finally show ?thesis by simp
   qed
 
   lemma dcaul_language[simp]:
     assumes "INTER (set AA) dca.alphabet = UNION (set AA) dca.alphabet"
     shows "DCA.language (dcaul AA) = UNION (set AA) DCA.language"
     unfolding dcaul_def using dgcad_language dcgaul_language[OF assms] by auto
 
 end
\ No newline at end of file
diff --git a/thys/Transition_Systems_and_Automata/Transition_Systems/Transition_System_Extra.thy b/thys/Transition_Systems_and_Automata/Transition_Systems/Transition_System_Extra.thy
--- a/thys/Transition_Systems_and_Automata/Transition_Systems/Transition_System_Extra.thy
+++ b/thys/Transition_Systems_and_Automata/Transition_Systems/Transition_System_Extra.thy
@@ -1,97 +1,67 @@
 section \<open>Additional Theorems for Transition Systems\<close>
 
 theory Transition_System_Extra
 imports
   "../Basic/Sequence_LTL"
   "Transition_System"
 begin
 
   context transition_system
   begin
 
     definition "enableds p \<equiv> {a. enabled a p}"
     definition "paths p \<equiv> {r. path r p}"
     definition "runs p \<equiv> {r. run r p}"
 
     lemma stake_run:
       assumes "\<And> k. path (stake k r) p"
       shows "run r p"
       using assms by (coinduction arbitrary: r p) (force elim: path.cases)
     lemma snth_run:
       assumes "\<And> k. enabled (r !! k) (target (stake k r) p)"
       shows "run r p"
       using assms by (coinduction arbitrary: r p) (metis stream.sel fold_simps snth.simps stake.simps)
 
     lemma run_stake:
       assumes "run r p"
       shows "path (stake k r) p"
       using assms by (metis run_shift_elim stake_sdrop)
     lemma run_sdrop:
       assumes "run r p"
       shows "run (sdrop k r) (target (stake k r) p)"
       using assms by (metis run_shift_elim stake_sdrop)
     lemma run_snth:
       assumes "run r p"
       shows "enabled (r !! k) (target (stake k r) p)"
       using assms by (metis stream.collapse sdrop_simps(1) run_scons_elim run_sdrop)
 
+    lemma run_alt_def_snth: "run r p \<longleftrightarrow> (\<forall> k. enabled (r !! k) (target (stake k r) p))"
+      using snth_run run_snth by blast
+
     lemma reachable_states:
       assumes "q \<in> reachable p" "path r q"
       shows "set (states r q) \<subseteq> reachable p"
       using assms by (induct r arbitrary: q) (auto)
     lemma reachable_trace:
       assumes "q \<in> reachable p" "run r q"
       shows "sset (trace r q) \<subseteq> reachable p"
       using assms unfolding sset_subset_stream_pred
       by (coinduction arbitrary: r q) (force elim: run.cases)
 
-    lemma infs_trace_coinduct[case_names infs_trace, consumes 1]:
-      assumes "R r p"
-      assumes "\<And> r p. R r p \<Longrightarrow>
-        (\<exists> u s. r = u @- s \<and> P (target u p)) \<and>
-        (\<exists> u s. r = u @- s \<and> u \<noteq> [] \<and> R s (target u p))"
-      shows "infs P (trace r p)"
-    proof -
-      have "infs P (p ## trace r p)"
-      using assms(1)
-      proof (coinduction arbitrary: r p)
-        case infs
-        obtain u r\<^sub>1 v r\<^sub>2 where 1:
-          "r = u @- r\<^sub>1" "P (target u p)"
-          "r = v @- r\<^sub>2" "v \<noteq> []" "R r\<^sub>2 (target v p)"
-          using assms(2) infs by blast
-        show ?case
-        unfolding ev_stl_alt_def
-        proof (intro exI conjI bexI)
-          show "P (target u p)" using 1(2) by this
-          show "target u p \<in> sset (p ## trace r p)" unfolding target_alt_def 1(1) by simp
-          show "R r\<^sub>2 (target v p)" using 1(5) by this
-          have "trace r p = states v p @- trace r\<^sub>2 (target v p)" unfolding 1(3) by simp
-          also have "states v p = butlast (states v p) @ [target v p]"
-            unfolding target_alt_def using 1(4) by simp
-          finally show "p ## trace r p =
-            (p # butlast (states v p)) @- target v p ## trace r\<^sub>2 (target v p)" by simp
-          show "p # butlast (states v p) \<noteq> []" by simp
-          show "target v p ## trace r\<^sub>2 (target v p) = target v p ## trace r\<^sub>2 (target v p)" by simp
-        qed
-      qed
-      then show ?thesis by simp
-    qed
-
   end
 
   context transition_system_initial
   begin
 
     lemma nodes_states:
       assumes "p \<in> nodes" "path r p"
       shows "set (states r p) \<subseteq> nodes"
       using reachable_states assms by blast
     lemma nodes_trace:
       assumes "p \<in> nodes" "run r p"
       shows "sset (trace r p) \<subseteq> nodes"
       using reachable_trace assms by blast
 
   end
 
 end
\ No newline at end of file