diff --git a/thys/LTL_Master_Theorem/Code_Export.thy b/thys/LTL_Master_Theorem/Code_Export.thy
--- a/thys/LTL_Master_Theorem/Code_Export.thy
+++ b/thys/LTL_Master_Theorem/Code_Export.thy
@@ -1,63 +1,55 @@
 (*
     Author:   Benedikt Seidl
     License:  BSD
 *)
 
 section \<open>Code export to Standard ML\<close>
 
 theory Code_Export
 imports
   "LTL_to_DRA/DRA_Implementation"
   LTL.Code_Equations
   "HOL-Library.Code_Target_Numeral"
 begin
 
 subsection \<open>LTL to DRA\<close>
 
-lemma dgba_degen_code [code]:
-  "DGBA.degen A = dba (DGBA.alphabet A) (DGBA.initial A, 0) (DGBA.dexecute A) (DGBA.daccepting A)"
-  by (metis DGBA.degen_def DGBA.degen_simps(2) dba.sel(2))
-
-lemma dgca_degen_code [code]:
-  "DGCA.degen A = dca (DGCA.alphabet A) (DGCA.initial A, 0) (DGCA.dexecute A) (DGCA.drejecting A)"
-  by (metis DGCA.degen_def DGCA.degen_simps(2) dca.sel(2))
-
 export_code ltlc_to_draei checking
 
 
 declare ltl_to_dra.af_letter\<^sub>F_lifted_semantics [code]
 declare ltl_to_dra.af_letter\<^sub>G_lifted_semantics [code]
 declare ltl_to_dra.af_letter\<^sub>\<nu>_lifted_semantics [code]
 
 definition atoms_ltlc_list_literals :: "String.literal ltlc \<Rightarrow> String.literal list"
 where
   "atoms_ltlc_list_literals = atoms_ltlc_list"
 
 definition ltlc_to_draei_literals :: "String.literal ltlc \<Rightarrow> (String.literal set, nat) draei"
 where
   "ltlc_to_draei_literals = ltlc_to_draei"
 
 definition sort_transitions :: "(nat \<times> String.literal set \<times> nat) list \<Rightarrow> (nat \<times> String.literal set \<times> nat) list"
 where
   "sort_transitions = sort_key fst"
 
 export_code True_ltlc Iff_ltlc ltlc_to_draei_literals
   alphabetei initialei transei acceptingei
   integer_of_nat atoms_ltlc_list_literals sort_transitions set
   in SML module_name LTL file_prefix LTL_to_DRA
 
 
 
 subsection \<open>LTL to NBA\<close>
 
 (* TODO *)
 
 
 
 subsection \<open>LTL to LDBA\<close>
 
 (* TODO *)
 
 
 
 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>))"
     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>)))"
     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>)))"
     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 DGBA.degen_def)
+  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/DBA/DBA_Combine.thy b/thys/Transition_Systems_and_Automata/Automata/DBA/DBA_Combine.thy
--- a/thys/Transition_Systems_and_Automata/Automata/DBA/DBA_Combine.thy
+++ b/thys/Transition_Systems_and_Automata/Automata/DBA/DBA_Combine.thy
@@ -1,303 +1,303 @@
 section \<open>Deterministic Büchi Automata Combinations\<close>
 
 theory DBA_Combine
 imports "DBA" "DGBA"
 begin
 
   definition dbgail :: "('label, 'state) dba list \<Rightarrow> ('label, 'state list) dgba" where
     "dbgail AA \<equiv> dgba
       (INTER (set AA) dba.alphabet)
       (map dba.initial AA)
       (\<lambda> a pp. map2 (\<lambda> A p. dba.succ A a p) AA pp)
       (map (\<lambda> k pp. dba.accepting (AA ! k) (pp ! k)) [0 ..< length AA])"
 
   lemma dbgail_trace_smap:
     assumes "length pp = length AA" "k < length AA"
     shows "smap (\<lambda> pp. pp ! k) (dgba.trace (dbgail AA) w pp) = dba.trace (AA ! k) w (pp ! k)"
     using assms unfolding dbgail_def by (coinduction arbitrary: w pp) (force)
   lemma dbgail_nodes_length:
     assumes "pp \<in> DGBA.nodes (dbgail AA)"
     shows "length pp = length AA"
     using assms unfolding dbgail_def by induct auto
   lemma dbgail_nodes[intro]:
     assumes "pp \<in> DGBA.nodes (dbgail AA)" "k < length pp"
     shows "pp ! k \<in> DBA.nodes (AA ! k)"
     using assms unfolding dbgail_def by induct auto
 
   lemma dbgail_nodes_finite[intro]:
     assumes "list_all (finite \<circ> DBA.nodes) AA"
     shows "finite (DGBA.nodes (dbgail AA))"
   proof (rule finite_subset)
     show "DGBA.nodes (dbgail AA) \<subseteq> listset (map DBA.nodes AA)"
       by (force simp: listset_member list_all2_conv_all_nth dbgail_nodes_length)
     have "finite (listset (map DBA.nodes AA)) \<longleftrightarrow> list_all finite (map DBA.nodes AA)"
       by (rule listset_finite) (auto simp: list_all_iff)
     then show "finite (listset (map DBA.nodes AA))" using assms by (simp add: list.pred_map)
   qed
   lemma dbgail_nodes_card:
     assumes "list_all (finite \<circ> DBA.nodes) AA"
     shows "card (DGBA.nodes (dbgail AA)) \<le> prod_list (map (card \<circ> DBA.nodes) AA)"
   proof -
     have "card (DGBA.nodes (dbgail AA)) \<le> card (listset (map DBA.nodes AA))"
     proof (rule card_mono)
       have "finite (listset (map DBA.nodes AA)) \<longleftrightarrow> list_all finite (map DBA.nodes AA)"
         by (rule listset_finite) (auto simp: list_all_iff)
       then show "finite (listset (map DBA.nodes AA))" using assms by (simp add: list.pred_map)
       show "DGBA.nodes (dbgail AA) \<subseteq> listset (map DBA.nodes AA)"
         by (force simp: listset_member list_all2_conv_all_nth dbgail_nodes_length)
     qed
     also have "\<dots> = prod_list (map (card \<circ> DBA.nodes) AA)" by simp
     finally show ?thesis by this
   qed
 
   lemma dbgail_language[simp]: "DGBA.language (dbgail AA) = INTER (set AA) DBA.language"
   proof safe
     fix w A
     assume 1: "w \<in> DGBA.language (dbgail AA)" "A \<in> set AA"
     obtain 2:
       "dgba.run (dbgail AA) w (dgba.initial (dbgail AA))"
       "gen infs (dgba.accepting (dbgail AA)) (dgba.trace (dbgail AA) w (dgba.initial (dbgail 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: "(\<lambda> pp. dba.accepting A (pp ! k)) \<in> set (dgba.accepting (dbgail AA))"
       using 3 unfolding dbgail_def by auto
     show "w \<in> DBA.language A"
     proof
       show "dba.run A w (dba.initial A)"
         using 1(2) 2(1) unfolding DBA.run_alt_def DGBA.run_alt_def dbgail_def by auto
       have "True \<longleftrightarrow> infs (\<lambda> pp. dba.accepting A (pp ! k)) (dgba.trace (dbgail AA) w (map dba.initial AA))"
         using 2(2) 4 unfolding dbgail_def by auto
       also have "\<dots> \<longleftrightarrow> infs (dba.accepting A) (smap (\<lambda> pp. pp ! k)
         (dgba.trace (dbgail AA) w (map dba.initial AA)))" by (simp add: comp_def)
       also have "smap (\<lambda> pp. pp ! k) (dgba.trace (dbgail AA) w (map dba.initial AA)) =
         dba.trace (AA ! k) w (map dba.initial AA ! k)" using 3(2) by (fastforce intro: dbgail_trace_smap)
       also have "\<dots> = dba.trace A w (dba.initial A)" using 3 by auto
       finally show "infs (dba.accepting A) (dba.trace A w (dba.initial A))" by simp
     qed
   next
     fix w
     assume 1: "w \<in> INTER (set AA) DBA.language"
     have 2: "dba.run A w (dba.initial A)" "infs (dba.accepting A) (dba.trace A w (dba.initial A))"
       if "A \<in> set AA" for A using 1 that by auto
     show "w \<in> DGBA.language (dbgail AA)"
     proof (intro DGBA.language ballI gen)
       show "dgba.run (dbgail AA) w (dgba.initial (dbgail AA))"
         using 2(1) unfolding DBA.run_alt_def DGBA.run_alt_def dbgail_def by auto
     next
       fix P
       assume 3: "P \<in> set (dgba.accepting (dbgail AA))"
       obtain k where 4: "P = (\<lambda> pp. dba.accepting (AA ! k) (pp ! k))" "k < length AA"
         using 3 unfolding dbgail_def by auto
       have "True \<longleftrightarrow> infs (dba.accepting (AA ! k)) (dba.trace (AA ! k) w (map dba.initial AA ! k))"
         using 2(2) 4(2) by auto
       also have "dba.trace (AA ! k) w (map dba.initial AA ! k) =
         smap (\<lambda> pp. pp ! k) (dgba.trace (dbgail AA) w (map dba.initial AA))"
         using 4(2) by (fastforce intro: dbgail_trace_smap[symmetric])
       also have "infs (dba.accepting (AA ! k)) \<dots> \<longleftrightarrow> infs P (dgba.trace (dbgail AA) w (map dba.initial AA))"
         unfolding 4(1) by (simp add: comp_def)
       also have "map dba.initial AA = dgba.initial (dbgail AA)" unfolding dbgail_def by simp
       finally show "infs P (dgba.trace (dbgail AA) w (dgba.initial (dbgail AA)))" by simp
     qed
   qed
 
   definition dbail :: "('label, 'state) dba list \<Rightarrow> ('label, 'state list degen) dba" where
-    "dbail = degen \<circ> dbgail"
+    "dbail = dgbad \<circ> dbgail"
 
   lemma dbail_nodes_finite[intro]:
     assumes "list_all (finite \<circ> DBA.nodes) AA"
     shows "finite (DBA.nodes (dbail AA))"
     using dbgail_nodes_finite assms unfolding dbail_def by auto
   lemma dbail_nodes_card:
     assumes"list_all (finite \<circ> DBA.nodes) AA"
     shows "card (DBA.nodes (dbail AA)) \<le> max 1 (length AA) * prod_list (map (card \<circ> DBA.nodes) AA)"
   proof -
     have "card (DBA.nodes (dbail AA)) \<le>
       max 1 (length (dgba.accepting (dbgail AA))) * card (DGBA.nodes (dbgail AA))"
-      unfolding dbail_def using degen_nodes_card by simp
+      unfolding dbail_def using dgbad_nodes_card by simp
     also have "length (dgba.accepting (dbgail AA)) = length AA" unfolding dbgail_def by simp
     also have "card (DGBA.nodes (dbgail AA)) \<le> prod_list (map (card \<circ> DBA.nodes) AA)"
       using dbgail_nodes_card assms by this
     finally show ?thesis by simp
   qed
 
   lemma dbail_language[simp]: "DBA.language (dbail AA) = INTER (set AA) DBA.language"
-    unfolding dbail_def using degen_language dbgail_language by auto
+    unfolding dbail_def using dgbad_language dbgail_language by auto
 
   definition dbau :: "('label, 'state\<^sub>1) dba \<Rightarrow> ('label, 'state\<^sub>2) dba \<Rightarrow>
     ('label, 'state\<^sub>1 \<times> 'state\<^sub>2) dba" where
     "dbau A B \<equiv> dba
       (dba.alphabet A \<union> dba.alphabet B)
       (dba.initial A, dba.initial B)
       (\<lambda> a (p, q). (dba.succ A a p, dba.succ B a q))
       (\<lambda> (p, q). dba.accepting A p \<or> dba.accepting B q)"
 
   (* TODO: can these be extracted as more general theorems about sscan? *)
   lemma dbau_fst[iff]: "infs (P \<circ> fst) (dba.trace (dbau A B) w (p, q)) \<longleftrightarrow> infs P (dba.trace A w p)"
   proof -
     let ?t = "dba.trace (dbau 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 = dba.trace A w p" unfolding dbau_def by (coinduction arbitrary: w p q) (auto)
     finally show ?thesis by this
   qed
   lemma dbau_snd[iff]: "infs (P \<circ> snd) (dba.trace (dbau A B) w (p, q)) \<longleftrightarrow> infs P (dba.trace B w q)"
   proof -
     let ?t = "dba.trace (dbau 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 = dba.trace B w q" unfolding dbau_def by (coinduction arbitrary: w p q) (auto)
     finally show ?thesis by this
   qed
   lemma dbau_nodes_fst[intro]:
     assumes "dba.alphabet A = dba.alphabet B"
     shows "fst ` DBA.nodes (dbau A B) \<subseteq> DBA.nodes A"
   proof (rule subsetI, erule imageE)
     fix pq p
     assume "pq \<in> DBA.nodes (dbau A B)" "p = fst pq"
     then show "p \<in> DBA.nodes A" using assms unfolding dbau_def by (induct arbitrary: p) (auto)
   qed
   lemma dbau_nodes_snd[intro]:
     assumes "dba.alphabet A = dba.alphabet B"
     shows "snd ` DBA.nodes (dbau A B) \<subseteq> DBA.nodes B"
   proof (rule subsetI, erule imageE)
     fix pq q
     assume "pq \<in> DBA.nodes (dbau A B)" "q = snd pq"
     then show "q \<in> DBA.nodes B" using assms unfolding dbau_def by (induct arbitrary: q) (auto)
   qed
 
   lemma dbau_nodes_finite[intro]:
     assumes "dba.alphabet A = dba.alphabet B"
     assumes "finite (DBA.nodes A)" "finite (DBA.nodes B)"
     shows "finite (DBA.nodes (dbau A B))"
   proof (rule finite_subset)
     show "DBA.nodes (dbau A B) \<subseteq> DBA.nodes A \<times> DBA.nodes B"
       using dbau_nodes_fst[OF assms(1)] dbau_nodes_snd[OF assms(1)] unfolding image_subset_iff by force
     show "finite (DBA.nodes A \<times> DBA.nodes B)" using assms(2, 3) by simp
   qed
   lemma dbau_nodes_card[intro]:
     assumes "dba.alphabet A = dba.alphabet B"
     assumes "finite (DBA.nodes A)" "finite (DBA.nodes B)"
     shows "card (DBA.nodes (dbau A B)) \<le> card (DBA.nodes A) * card (DBA.nodes B)"
   proof -
     have "card (DBA.nodes (dbau A B)) \<le> card (DBA.nodes A \<times> DBA.nodes B)"
     proof (rule card_mono)
       show "finite (DBA.nodes A \<times> DBA.nodes B)" using assms(2, 3) by simp
       show "DBA.nodes (dbau A B) \<subseteq> DBA.nodes A \<times> DBA.nodes B"
         using dbau_nodes_fst[OF assms(1)] dbau_nodes_snd[OF assms(1)] unfolding image_subset_iff by force
     qed
     also have "\<dots> = card (DBA.nodes A) * card (DBA.nodes B)" using card_cartesian_product by this
     finally show ?thesis by this
   qed
 
   lemma dbau_language[simp]:
     assumes "dba.alphabet A = dba.alphabet B"
     shows "DBA.language (dbau A B) = DBA.language A \<union> DBA.language B"
   proof -
     have 1: "dba.alphabet (dbau A B) = dba.alphabet A \<union> dba.alphabet B" unfolding dbau_def by simp
     have 2: "dba.initial (dbau A B) = (dba.initial A, dba.initial B)" unfolding dbau_def by simp
     have 3: "dba.accepting (dbau A B) = (\<lambda> pq. (dba.accepting A \<circ> fst) pq \<or> (dba.accepting B \<circ> snd) pq)"
       unfolding dbau_def by auto
     have 4: "infs (dba.accepting (dbau A B)) (DBA.trace (dbau A B) w (p, q)) \<longleftrightarrow>
       infs (dba.accepting A) (DBA.trace A w p) \<or> infs (dba.accepting B) (DBA.trace B w q)" for w p q
       unfolding 3 by blast
     show ?thesis using assms unfolding DBA.language_def DBA.run_alt_def 1 2 4 by auto
   qed
 
   definition dbaul :: "('label, 'state) dba list \<Rightarrow> ('label, 'state list) dba" where
     "dbaul AA \<equiv> dba
       (UNION (set AA) dba.alphabet)
       (map dba.initial AA)
       (\<lambda> a pp. map2 (\<lambda> A p. dba.succ A a p) AA pp)
       (\<lambda> pp. \<exists> k < length AA. dba.accepting (AA ! k) (pp ! k))"
 
   lemma dbaul_trace_smap:
     assumes "length pp = length AA" "k < length AA"
     shows "smap (\<lambda> pp. pp ! k) (dba.trace (dbaul AA) w pp) = dba.trace (AA ! k) w (pp ! k)"
     using assms unfolding dbaul_def by (coinduction arbitrary: w pp) (force)
   lemma dbaul_nodes_length:
     assumes "pp \<in> DBA.nodes (dbaul AA)"
     shows "length pp = length AA"
     using assms unfolding dbaul_def by induct auto
   lemma dbaul_nodes[intro]:
     assumes "INTER (set AA) dba.alphabet = UNION (set AA) dba.alphabet"
     assumes "pp \<in> DBA.nodes (dbaul AA)" "k < length pp"
     shows "pp ! k \<in> DBA.nodes (AA ! k)"
     using assms(2, 3, 1) unfolding dbaul_def by induct force+
 
   lemma dbaul_nodes_finite[intro]:
     assumes "INTER (set AA) dba.alphabet = UNION (set AA) dba.alphabet"
     assumes "list_all (finite \<circ> DBA.nodes) AA"
     shows "finite (DBA.nodes (dbaul AA))"
   proof (rule finite_subset)
     show "DBA.nodes (dbaul AA) \<subseteq> listset (map DBA.nodes AA)"
       using assms(1) by (force simp: listset_member list_all2_conv_all_nth dbaul_nodes_length)
     have "finite (listset (map DBA.nodes AA)) \<longleftrightarrow> list_all finite (map DBA.nodes AA)"
       by (rule listset_finite) (auto simp: list_all_iff)
     then show "finite (listset (map DBA.nodes AA))" using assms(2) by (simp add: list.pred_map)
   qed
   lemma dbaul_nodes_card:
     assumes "INTER (set AA) dba.alphabet = UNION (set AA) dba.alphabet"
     assumes "list_all (finite \<circ> DBA.nodes) AA"
     shows "card (DBA.nodes (dbaul AA)) \<le> prod_list (map (card \<circ> DBA.nodes) AA)"
   proof -
     have "card (DBA.nodes (dbaul AA)) \<le> card (listset (map DBA.nodes AA))"
     proof (rule card_mono)
       have "finite (listset (map DBA.nodes AA)) \<longleftrightarrow> list_all finite (map DBA.nodes AA)"
         by (rule listset_finite) (auto simp: list_all_iff)
       then show "finite (listset (map DBA.nodes AA))" using assms(2) by (simp add: list.pred_map)
       show "DBA.nodes (dbaul AA) \<subseteq> listset (map DBA.nodes AA)"
         using assms(1) by (force simp: listset_member list_all2_conv_all_nth dbaul_nodes_length)
     qed
     also have "\<dots> = prod_list (map (card \<circ> DBA.nodes) AA)" by simp
     finally show ?thesis by this
   qed
 
   lemma dbaul_language[simp]:
     assumes "INTER (set AA) dba.alphabet = UNION (set AA) dba.alphabet"
     shows "DBA.language (dbaul AA) = UNION (set AA) DBA.language"
   proof safe
     fix w
     assume 1: "w \<in> DBA.language (dbaul AA)"
     obtain 2:
       "dba.run (dbaul AA) w (dba.initial (dbaul AA))"
       "infs (dba.accepting (dbaul AA)) (dba.trace (dbaul AA) w (dba.initial (dbaul AA)))"
       using 1 by rule
     obtain k where 3:
       "k < length AA"
       "infs (\<lambda> pp. dba.accepting (AA ! k) (pp ! k)) (dba.trace (dbaul AA) w (map dba.initial AA))"
       using 2(2) unfolding dbaul_def by auto
     show "w \<in> UNION (set AA) DBA.language"
     proof (intro UN_I DBA.language)
       show "AA ! k \<in> set AA" using 3(1) by simp
       show "dba.run (AA ! k) w (dba.initial (AA ! k))"
         using assms 2(1) 3(1) unfolding DBA.run_alt_def DGBA.run_alt_def dbaul_def by force
       have "True \<longleftrightarrow> infs (\<lambda> pp. dba.accepting (AA ! k) (pp ! k))
         (dba.trace (dbaul AA) w (map dba.initial AA))" using 3(2) by auto
       also have "\<dots> \<longleftrightarrow> infs (dba.accepting (AA ! k))
         (smap (\<lambda> pp. pp ! k) (dba.trace (dbaul AA) w (map dba.initial AA)))" by (simp add: comp_def)
       also have "smap (\<lambda> pp. pp ! k) (dba.trace (dbaul AA) w (map dba.initial AA)) =
         dba.trace (AA ! k) w (map dba.initial AA ! k)" using 3(1) by (fastforce intro: dbaul_trace_smap)
       also have "\<dots> = dba.trace (AA ! k) w (dba.initial (AA ! k))" using 3 by auto
       finally show "infs (dba.accepting (AA ! k)) (dba.trace (AA ! k) w (dba.initial (AA ! k)))" by simp
     qed
   next
     fix A w
     assume 1: "A \<in> set AA" "w \<in> DBA.language A"
     obtain 2: "dba.run A w (dba.initial A)" "infs (dba.accepting A) (dba.trace A w (dba.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> DBA.language (dbaul AA)"
     proof
       show "dba.run (dbaul AA) w (dba.initial (dbaul AA))"
         using 1(1) 2(1) unfolding DBA.run_alt_def DGBA.run_alt_def dbaul_def by auto
       have "True \<longleftrightarrow> infs (dba.accepting (AA ! k)) (dba.trace (AA ! k) w (map dba.initial AA ! k))"
         using 2(2) 3 by auto
       also have "dba.trace (AA ! k) w (map dba.initial AA ! k) =
         smap (\<lambda> pp. pp ! k) (dba.trace (dbaul AA) w (map dba.initial AA))"
         using 3(2) by (fastforce intro: dbaul_trace_smap[symmetric])
       also have "infs (dba.accepting (AA ! k)) \<dots> \<longleftrightarrow> infs (\<lambda> pp. dba.accepting (AA ! k) (pp ! k))
         (dba.trace (dbaul AA) w (map dba.initial AA))" by (simp add: comp_def)
       finally show "infs (dba.accepting (dbaul AA)) (dba.trace (dbaul AA) w (dba.initial (dbaul AA)))"
         using 3(2) unfolding dbaul_def by auto
     qed
   qed
 
 end
\ No newline at end of file
diff --git a/thys/Transition_Systems_and_Automata/Automata/DBA/DGBA.thy b/thys/Transition_Systems_and_Automata/Automata/DBA/DGBA.thy
--- a/thys/Transition_Systems_and_Automata/Automata/DBA/DGBA.thy
+++ b/thys/Transition_Systems_and_Automata/Automata/DBA/DGBA.thy
@@ -1,90 +1,146 @@
 section \<open>Deterministic Generalized Büchi Automata\<close>
 
 theory DGBA
 imports
   "DBA"
-  "../../Transition_Systems/Transition_System_Degeneralization"
+  "../../Basic/Degeneralization"
 begin
 
   datatype ('label, 'state) dgba = dgba
     (alphabet: "'label set")
     (initial: "'state")
     (succ: "'label \<Rightarrow> 'state \<Rightarrow> 'state")
     (accepting: "'state pred gen")
 
-  global_interpretation dgba: transition_system_initial_generalized
-    "succ A" "\<lambda> a p. a \<in> alphabet A" "\<lambda> p. p = initial A" "accepting A"
+  global_interpretation dgba: transition_system_initial
+    "succ A" "\<lambda> a p. a \<in> alphabet A" "\<lambda> p. p = initial A"
     for A
     defines path = dgba.path and run = dgba.run and reachable = dgba.reachable and nodes = dgba.nodes and
-      enableds = dgba.enableds and paths = dgba.paths and runs = dgba.runs and
-      dexecute = dgba.dexecute and denabled = dgba.denabled and dinitial = dgba.dinitial and
-      daccepting = dgba.dcondition
+      enableds = dgba.enableds and paths = dgba.paths and runs = dgba.runs
     by this
 
   abbreviation target where "target \<equiv> dgba.target"
   abbreviation states where "states \<equiv> dgba.states"
   abbreviation trace where "trace \<equiv> dgba.trace"
 
   abbreviation successors :: "('label, 'state) dgba \<Rightarrow> 'state \<Rightarrow> 'state set" where
     "successors \<equiv> dgba.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: dgba.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) dgba \<Rightarrow> 'label stream set" where
     "language A \<equiv> {w. run A w (initial A) \<and> gen infs (accepting A) (trace A w (initial A))}"
 
   lemma language[intro]:
     assumes "run A w (initial A)" "gen infs (accepting 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)" "gen infs (accepting 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
 
-  definition degen :: "('label, 'state) dgba \<Rightarrow> ('label, 'state degen) dba" where
-    "degen A \<equiv> dba (alphabet A) (The (dinitial A)) (dexecute A) (daccepting A)"
-
-  lemma degen_simps[simp]:
-    "dba.alphabet (degen A) = alphabet A"
-    "dba.initial (degen A) = (initial A, 0)"
-    "dba.succ (degen A) = dexecute A"
-    "dba.accepting (degen A) = daccepting A"
-    unfolding degen_def dgba.dinitial_def by auto
+  definition dgbad :: "('label, 'state) dgba \<Rightarrow> ('label, 'state degen) dba" where
+    "dgbad A \<equiv> dba
+      (alphabet A)
+      (initial A, 0)
+      (\<lambda> a (p, k). (succ A a p, count (accepting A) p k))
+      (degen (accepting A))"
 
-  lemma degen_trace[simp]: "dba.trace (degen A) = dgba.degen.trace A" unfolding degen_simps by rule
-  lemma degen_run[simp]: "dba.run (degen A) = dgba.degen.run A"
-    unfolding DBA.run_def degen_simps dgba.denabled_def case_prod_beta' by rule
-  lemma degen_nodes[simp]: "DBA.nodes (degen A) = dgba.degen.nodes TYPE('label) A"
-    unfolding DBA.nodes_def degen_simps
-    unfolding dgba.denabled_def dgba.dinitial_def
-    unfolding prod_eq_iff case_prod_beta' prod.sel
-    by rule
+  lemma dgbad_simps[simp]:
+    "dba.alphabet (dgbad A) = alphabet A"
+    "dba.initial (dgbad A) = (initial A, 0)"
+    "dba.succ (dgbad A) a (p, k) = (succ A a p, count (accepting A) p k)"
+    "dba.accepting (dgbad A) = degen (accepting A)"
+    unfolding dgbad_def by auto
 
-  lemma degen_nodes_finite[iff]: "finite (DBA.nodes (degen A)) \<longleftrightarrow> finite (DGBA.nodes A)" by simp
-  lemma degen_nodes_card: "card (DBA.nodes (degen A)) \<le> max 1 (length (accepting A)) * card (DGBA.nodes A)"
-    using dgba.degen_nodes_card by simp
+  lemma dgbad_target[simp]: "dba.target (dgbad A) w (p, k) =
+    (dgba.target A w p, fold (count (accepting A)) (butlast (p # dgba.states A w p)) k)"
+    by (induct w arbitrary: p k) (auto)
+  lemma dgbad_states[simp]: "dba.states (dgbad A) w (p, k) =
+    dgba.states A w p || scan (count (accepting A)) (p # dgba.states A w p) k"
+    by (induct w arbitrary: p k) (auto)
+  lemma dgbad_trace[simp]: "dba.trace (dgbad A) w (p, k) =
+    dgba.trace A w p ||| sscan (count (accepting A)) (p ## dgba.trace A w p) k"
+    by (coinduction arbitrary: w p k) (auto)
+  lemma dgbad_path[iff]: "dba.path (dgbad A) w (p, k) \<longleftrightarrow> dgba.path A w p"
+    unfolding DBA.path_alt_def DGBA.path_alt_def by simp
+  lemma dgbad_run[iff]: "dba.run (dgbad A) w (p, k) \<longleftrightarrow> dgba.run A w p"
+    unfolding DBA.run_alt_def DGBA.run_alt_def by simp
 
-  lemma degen_language[simp]: "DBA.language (degen A) = DGBA.language A"
-    unfolding DBA.language_def DGBA.language_def degen_simps
-    unfolding degen_trace degen_run
-    unfolding dgba.degen_run dgba.degen_infs gen_def
-    by rule
+  (* TODO: revise *)
+  lemma dgbad_nodes_fst[simp]: "fst ` DBA.nodes (dgbad A) = DGBA.nodes A"
+    unfolding dba.nodes_alt_def dba.reachable_alt_def
+    unfolding dgba.nodes_alt_def dgba.reachable_alt_def
+    unfolding image_def by simp
+  lemma dgbad_nodes_snd_empty:
+    assumes "accepting A = []"
+    shows "snd ` DBA.nodes (dgbad A) \<subseteq> {0}"
+  proof -
+    have 2: "snd (dba.succ (dgbad A) a (p, k)) = 0" for a p k using assms by auto
+    show ?thesis using 2 by (auto elim: dba.nodes.cases)
+  qed
+  lemma dgbad_nodes_snd_nonempty:
+    assumes "accepting A \<noteq> []"
+    shows "snd ` DBA.nodes (dgbad A) \<subseteq> {0 ..< length (accepting A)}"
+  proof -
+    have 1: "snd (dba.initial (dgbad A)) < length (accepting A)"
+      using assms by simp
+    have 2: "snd (dba.succ (dgbad A) a (p, k)) < length (accepting A)" for a p k
+      using assms by auto
+    show ?thesis using 1 2 by (auto elim: dba.nodes.cases)
+  qed
+  lemma dgbad_nodes_empty:
+    assumes "accepting A = []"
+    shows "DBA.nodes (dgbad A) = DGBA.nodes A \<times> {0}"
+  proof -
+    have "(p, k) \<in> DBA.nodes (dgbad A) \<longleftrightarrow> p \<in> fst ` DBA.nodes (dgbad A) \<and> k = 0" for p k
+      using dgbad_nodes_snd_empty[OF assms] by (force simp del: dgbad_nodes_fst)
+    then show ?thesis by auto
+  qed
+  lemma dgbad_nodes_nonempty:
+    assumes "accepting A \<noteq> []"
+    shows "DBA.nodes (dgbad A) \<subseteq> DGBA.nodes A \<times> {0 ..< length (accepting A)}"
+    using subset_fst_snd dgbad_nodes_fst[of A] dgbad_nodes_snd_nonempty[OF assms] by blast
+  lemma dgbad_nodes: "DBA.nodes (dgbad A) \<subseteq> DGBA.nodes A \<times> {0 ..< max 1 (length (accepting A))}"
+    using dgbad_nodes_empty dgbad_nodes_nonempty by force
+
+  lemma dgbad_language[simp]: "DBA.language (dgbad A) = DGBA.language A" by force
+
+  lemma dgbad_nodes_finite[iff]: "finite (DBA.nodes (dgbad A)) \<longleftrightarrow> finite (DGBA.nodes A)"
+  proof
+    show "finite (DGBA.nodes A)" if "finite (DBA.nodes (dgbad A))"
+      using that by (auto simp flip: dgbad_nodes_fst)
+    show "finite (DBA.nodes (dgbad A))" if "finite (DGBA.nodes A)"
+      using dgbad_nodes that finite_subset by fastforce
+  qed
+  lemma dgbad_nodes_card: "card (DBA.nodes (dgbad A)) \<le> max 1 (length (accepting A)) * card (DGBA.nodes A)"
+  proof (cases "finite (DGBA.nodes A)")
+    case True
+    have "card (DBA.nodes (dgbad A)) \<le> card (DGBA.nodes A \<times> {0 ..< max 1 (length (accepting A))})"
+      using dgbad_nodes True by (blast intro: card_mono)
+    also have "\<dots> = max 1 (length (accepting A)) * card (DGBA.nodes A)" unfolding card_cartesian_product by simp
+    finally show ?thesis by this
+  next
+    case False
+    then have "card (DGBA.nodes A) = 0" "card (DBA.nodes (dgbad A)) = 0" by auto
+    then show ?thesis by simp
+  qed
 
 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)))"
       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))"
       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))"
         using 4 by simp
       also have "\<dots> \<longleftrightarrow> \<not> infs (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
     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))"
       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))"
       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))"
         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)))"
         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)))"
       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))
         (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))
         (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
     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))"
       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))"
         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))
         (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)))"
         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 = degen \<circ> dcgaul"
+    "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 degen_nodes_card by simp
+      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 degen_language dcgaul_language[OF assms] by auto
+    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/Automata/DCA/DGCA.thy b/thys/Transition_Systems_and_Automata/Automata/DCA/DGCA.thy
--- a/thys/Transition_Systems_and_Automata/Automata/DCA/DGCA.thy
+++ b/thys/Transition_Systems_and_Automata/Automata/DCA/DGCA.thy
@@ -1,91 +1,146 @@
 section \<open>Deterministic Co-Generalized Co-Büchi Automata\<close>
 
 theory DGCA
 imports
   "DCA"
-  "../../Transition_Systems/Transition_System_Degeneralization"
+  "../../Basic/Degeneralization"
 begin
 
   datatype ('label, 'state) dgca = dgca
     (alphabet: "'label set")
     (initial: "'state")
     (succ: "'label \<Rightarrow> 'state \<Rightarrow> 'state")
     (rejecting: "'state pred gen")
 
-  global_interpretation dgca: transition_system_initial_generalized
-    "succ A" "\<lambda> a p. a \<in> alphabet A" "\<lambda> p. p = initial A" "rejecting A"
+  global_interpretation dgca: transition_system_initial
+    "succ A" "\<lambda> a p. a \<in> alphabet A" "\<lambda> p. p = initial A"
     for A
     defines path = dgca.path and run = dgca.run and reachable = dgca.reachable and nodes = dgca.nodes and
-      enableds = dgca.enableds and paths = dgca.paths and runs = dgca.runs and
-      dexecute = dgca.dexecute and denabled = dgca.denabled and dinitial = dgca.dinitial and
-      drejecting = dgca.dcondition
+      enableds = dgca.enableds and paths = dgca.paths and runs = dgca.runs
     by this
 
   abbreviation target where "target \<equiv> dgca.target"
   abbreviation states where "states \<equiv> dgca.states"
   abbreviation trace where "trace \<equiv> dgca.trace"
 
   abbreviation successors :: "('label, 'state) dgca \<Rightarrow> 'state \<Rightarrow> 'state set" where
     "successors \<equiv> dgca.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: dgca.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) dgca \<Rightarrow> 'label stream set" where
     "language A \<equiv> {w. run A w (initial A) \<and> cogen fins (rejecting A) (trace A w (initial A))}"
 
   lemma language[intro]:
     assumes "run A w (initial A)" "cogen 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)" "cogen 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
 
-  definition degen :: "('label, 'state) dgca \<Rightarrow> ('label, 'state degen) dca" where
-    "degen A \<equiv> dca (alphabet A) (The (dinitial A)) (dexecute A) (drejecting A)"
-
-  lemma degen_simps[simp]:
-    "dca.alphabet (degen A) = alphabet A"
-    "dca.initial (degen A) = (initial A, 0)"
-    "dca.succ (degen A) = dexecute A"
-    "dca.rejecting (degen A) = drejecting A"
-    unfolding degen_def dgca.dinitial_def by auto
+  definition dgcad :: "('label, 'state) dgca \<Rightarrow> ('label, 'state degen) dca" where
+    "dgcad A \<equiv> dca
+      (alphabet A)
+      (initial A, 0)
+      (\<lambda> a (p, k). (succ A a p, count (rejecting A) p k))
+      (degen (rejecting A))"
 
-  lemma degen_trace[simp]: "dca.trace (degen A) = dgca.degen.trace A" unfolding degen_simps by rule
-  lemma degen_run[simp]: "dca.run (degen A) = dgca.degen.run A"
-    unfolding DCA.run_def degen_simps dgca.denabled_def case_prod_beta' by rule
-  lemma degen_nodes[simp]: "DCA.nodes (degen A) = dgca.degen.nodes TYPE('label) A"
-    unfolding DCA.nodes_def degen_simps
-    unfolding dgca.denabled_def dgca.dinitial_def
-    unfolding prod_eq_iff case_prod_beta' prod.sel
-    by rule
+  lemma dgcad_simps[simp]:
+    "dca.alphabet (dgcad A) = alphabet A"
+    "dca.initial (dgcad A) = (initial A, 0)"
+    "dca.succ (dgcad A) a (p, k) = (succ A a p, count (rejecting A) p k)"
+    "dca.rejecting (dgcad A) = degen (rejecting A)"
+    unfolding dgcad_def by auto
 
-  lemma degen_nodes_finite[iff]: "finite (DCA.nodes (degen A)) \<longleftrightarrow> finite (DGCA.nodes A)" by simp
-  lemma degen_nodes_card: "card (DCA.nodes (degen A)) \<le> max 1 (length (rejecting A)) * card (DGCA.nodes A)"
-    using dgca.degen_nodes_card by simp
+  lemma dgcad_target[simp]: "dca.target (dgcad A) w (p, k) =
+    (dgca.target A w p, fold (count (rejecting A)) (butlast (p # dgca.states A w p)) k)"
+    by (induct w arbitrary: p k) (auto)
+  lemma dgcad_states[simp]: "dca.states (dgcad A) w (p, k) =
+    dgca.states A w p || scan (count (rejecting A)) (p # dgca.states A w p) k"
+    by (induct w arbitrary: p k) (auto)
+  lemma dgcad_trace[simp]: "dca.trace (dgcad A) w (p, k) =
+    dgca.trace A w p ||| sscan (count (rejecting A)) (p ## dgca.trace A w p) k"
+    by (coinduction arbitrary: w p k) (auto)
+  lemma dgcad_path[iff]: "dca.path (dgcad A) w (p, k) \<longleftrightarrow> dgca.path A w p"
+    unfolding DCA.path_alt_def DGCA.path_alt_def by simp
+  lemma dgcad_run[iff]: "dca.run (dgcad A) w (p, k) \<longleftrightarrow> dgca.run A w p"
+    unfolding DCA.run_alt_def DGCA.run_alt_def by simp
 
-  lemma degen_language[simp]: "DCA.language (degen A) = DGCA.language A"
-    unfolding DCA.language_def DGCA.language_def degen_simps
-    unfolding degen_trace degen_run
-    unfolding dgca.degen_run dgca.degen_infs cogen_def
-    unfolding ball_simps(10)
-    by rule
+  (* TODO: revise *)
+  lemma dgcad_nodes_fst[simp]: "fst ` DCA.nodes (dgcad A) = DGCA.nodes A"
+    unfolding dca.nodes_alt_def dca.reachable_alt_def
+    unfolding dgca.nodes_alt_def dgca.reachable_alt_def
+    unfolding image_def by simp
+  lemma dgcad_nodes_snd_empty:
+    assumes "rejecting A = []"
+    shows "snd ` DCA.nodes (dgcad A) \<subseteq> {0}"
+  proof -
+    have 2: "snd (dca.succ (dgcad A) a (p, k)) = 0" for a p k using assms by auto
+    show ?thesis using 2 by (auto elim: dca.nodes.cases)
+  qed
+  lemma dgcad_nodes_snd_nonempty:
+    assumes "rejecting A \<noteq> []"
+    shows "snd ` DCA.nodes (dgcad A) \<subseteq> {0 ..< length (rejecting A)}"
+  proof -
+    have 1: "snd (dca.initial (dgcad A)) < length (rejecting A)"
+      using assms by simp
+    have 2: "snd (dca.succ (dgcad A) a (p, k)) < length (rejecting A)" for a p k
+      using assms by auto
+    show ?thesis using 1 2 by (auto elim: dca.nodes.cases)
+  qed
+  lemma dgcad_nodes_empty:
+    assumes "rejecting A = []"
+    shows "DCA.nodes (dgcad A) = DGCA.nodes A \<times> {0}"
+  proof -
+    have "(p, k) \<in> DCA.nodes (dgcad A) \<longleftrightarrow> p \<in> fst ` DCA.nodes (dgcad A) \<and> k = 0" for p k
+      using dgcad_nodes_snd_empty[OF assms] by (force simp del: dgcad_nodes_fst)
+    then show ?thesis by auto
+  qed
+  lemma dgcad_nodes_nonempty:
+    assumes "rejecting A \<noteq> []"
+    shows "DCA.nodes (dgcad A) \<subseteq> DGCA.nodes A \<times> {0 ..< length (rejecting A)}"
+    using subset_fst_snd dgcad_nodes_fst[of A] dgcad_nodes_snd_nonempty[OF assms] by blast
+  lemma dgcad_nodes: "DCA.nodes (dgcad A) \<subseteq> DGCA.nodes A \<times> {0 ..< max 1 (length (rejecting A))}"
+    using dgcad_nodes_empty dgcad_nodes_nonempty by force
+
+  lemma dgcad_language[simp]: "DCA.language (dgcad A) = DGCA.language A" by force
+
+  lemma dgcad_nodes_finite[iff]: "finite (DCA.nodes (dgcad A)) \<longleftrightarrow> finite (DGCA.nodes A)"
+  proof
+    show "finite (DGCA.nodes A)" if "finite (DCA.nodes (dgcad A))"
+      using that by (auto simp flip: dgcad_nodes_fst)
+    show "finite (DCA.nodes (dgcad A))" if "finite (DGCA.nodes A)"
+      using dgcad_nodes that finite_subset by fastforce
+  qed
+  lemma dgcad_nodes_card: "card (DCA.nodes (dgcad A)) \<le> max 1 (length (rejecting A)) * card (DGCA.nodes A)"
+  proof (cases "finite (DGCA.nodes A)")
+    case True
+    have "card (DCA.nodes (dgcad A)) \<le> card (DGCA.nodes A \<times> {0 ..< max 1 (length (rejecting A))})"
+      using dgcad_nodes True by (blast intro: card_mono)
+    also have "\<dots> = max 1 (length (rejecting A)) * card (DGCA.nodes A)" unfolding card_cartesian_product by simp
+    finally show ?thesis by this
+  next
+    case False
+    then have "card (DGCA.nodes A) = 0" "card (DCA.nodes (dgcad A)) = 0" by auto
+    then show ?thesis by simp
+  qed
 
 end
\ No newline at end of file
diff --git a/thys/Transition_Systems_and_Automata/Basic/Acceptance.thy b/thys/Transition_Systems_and_Automata/Basic/Acceptance.thy
--- a/thys/Transition_Systems_and_Automata/Basic/Acceptance.thy
+++ b/thys/Transition_Systems_and_Automata/Basic/Acceptance.thy
@@ -1,51 +1,49 @@
 theory Acceptance
 imports Sequence_LTL
 begin
 
   type_synonym 'a pred = "'a \<Rightarrow> bool"
   type_synonym 'a rabin = "'a pred \<times> 'a pred"
   type_synonym 'a gen = "'a list"
-  (* TODO: move to degeneralization theory *)
-  type_synonym 'a degen = "'a \<times> nat"
 
   definition rabin :: "'a rabin \<Rightarrow> 'a stream pred" where
     "rabin \<equiv> \<lambda> (I, F) w. infs I w \<and> fins F w"
 
   lemma rabin[intro]:
     assumes "IF = (I, F)" "infs I w" "fins F w"
     shows "rabin IF w"
     using assms unfolding rabin_def by auto
   lemma rabin_elim[elim]:
     assumes "rabin IF w"
     obtains I F
     where "IF = (I, F)" "infs I w" "fins F w"
     using assms unfolding rabin_def by auto
 
   definition gen :: "('a \<Rightarrow> 'b pred) \<Rightarrow> ('a gen \<Rightarrow> 'b pred)" where
     "gen P cs w \<equiv> \<forall> c \<in> set cs. P c w"
 
   lemma gen[intro]:
     assumes "\<And> c. c \<in> set cs \<Longrightarrow> P c w"
     shows "gen P cs w"
     using assms unfolding gen_def by auto
   lemma gen_elim[elim]:
     assumes "gen P cs w"
     obtains "\<And> c. c \<in> set cs \<Longrightarrow> P c w"
     using assms unfolding gen_def by auto
 
   definition cogen :: "('a \<Rightarrow> 'b pred) \<Rightarrow> ('a gen \<Rightarrow> 'b pred)" where
     "cogen P cs w \<equiv> \<exists> c \<in> set cs. P c w"
 
   lemma cogen[intro]:
     assumes "c \<in> set cs" "P c w"
     shows "cogen P cs w"
     using assms unfolding cogen_def by auto
   lemma cogen_elim[elim]:
     assumes "cogen P cs w"
     obtains c
     where "c \<in> set cs" "P c w"
     using assms unfolding cogen_def by auto
 
   lemma cogen_alt_def: "cogen P cs w \<longleftrightarrow> \<not> gen (\<lambda> c w. Not (P c w)) cs w" by auto
 
 end
\ No newline at end of file
diff --git a/thys/Transition_Systems_and_Automata/Basic/Degeneralization.thy b/thys/Transition_Systems_and_Automata/Basic/Degeneralization.thy
new file mode 100644
--- /dev/null
+++ b/thys/Transition_Systems_and_Automata/Basic/Degeneralization.thy
@@ -0,0 +1,224 @@
+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 0"
+
+  lemma count_empty[simp]: "count [] a k = 0" unfolding count_def by simp
+  lemma count_nonempty[simp]:
+    assumes "cs \<noteq> []"
+    shows "count cs a k < length cs"
+    using assms 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 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 unfolding count_def 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 1: "count cs (shd w) k < length cs" using mod_Suc assms(1) unfolding count_def by auto
+    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)
+        obtain u a v where 3: "w = u @- a ## v" "(cs ! l) a"
+          using degen_skip_arbitrary_condition 2(2) infs_set 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
+        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)
+      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
+      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
+      qed
+    qed
+  qed
+
+end
\ No newline at end of file
diff --git a/thys/Transition_Systems_and_Automata/Transition_Systems/Transition_System_Degeneralization.thy b/thys/Transition_Systems_and_Automata/Transition_Systems/Transition_System_Degeneralization.thy
deleted file mode 100644
--- a/thys/Transition_Systems_and_Automata/Transition_Systems/Transition_System_Degeneralization.thy
+++ /dev/null
@@ -1,350 +0,0 @@
-theory Transition_System_Degeneralization
-imports
-  "../Basic/Acceptance"
-  "Transition_System_Extra"
-begin
-
-  locale transition_system_initial_generalized =
-    transition_system_initial execute enabled initial
-    for execute :: "'transition \<Rightarrow> 'state \<Rightarrow> 'state"
-    and enabled :: "'transition \<Rightarrow> 'state \<Rightarrow> bool"
-    and initial :: "'state \<Rightarrow> bool"
-    +
-    (* TODO: why is this a list and not a set? *)
-    fixes condition :: "'state pred gen"
-  begin
-
-    (* TODO: make this a definition, prove useful (automation) things about, use opaquely *)
-    abbreviation "count p k \<equiv>
-      if k < length condition
-      then if (condition ! k) p then Suc k mod length condition else k
-      else 0"
-
-    definition dexecute :: "'transition \<Rightarrow> 'state degen \<Rightarrow> 'state degen" where
-      "dexecute a \<equiv> \<lambda> (p, k). (execute a p, count p k)"
-    definition denabled :: "'transition \<Rightarrow> 'state degen \<Rightarrow> bool" where
-      "denabled a \<equiv> \<lambda> (p, k). enabled a p"
-    definition dinitial :: "'state degen \<Rightarrow> bool" where
-      "dinitial \<equiv> \<lambda> (p, k). initial p \<and> k = 0"
-
-    sublocale degen: transition_system_initial dexecute denabled dinitial by this
-
-    lemma degen_run[iff]: "degen.run r (p, k) \<longleftrightarrow> run r p"
-    proof
-      show "run r p" if "degen.run r (p, k)"
-        using that by (coinduction arbitrary: r p k) (auto simp: dexecute_def denabled_def)
-      show "degen.run r (p, k)" if "run r p"
-        using that by (coinduction arbitrary: r p k) (auto simp: dexecute_def denabled_def)
-    qed
-
-    lemma degen_target_fst: "fst (degen.target w (p, k)) = target w p"
-      by (induct w arbitrary: p k) (auto simp: dexecute_def)
-    lemma degen_target_snd:
-      assumes "k < length condition"
-      assumes "\<And> q. q \<in> set (butlast (p # states w p)) \<Longrightarrow> \<not> (condition ! k) q"
-      shows "snd (degen.target w (p, k)) = k"
-      using assms by (induct w arbitrary: p) (auto simp: dexecute_def)
-    lemma degen_target_snd':
-      assumes "k < length condition"
-      assumes "\<And> q l. (q, l) \<in> set (butlast ((p, k) # degen.states w (p, k))) \<Longrightarrow> \<not> (condition ! l) q"
-      shows "snd (degen.target w (p, k)) = k"
-    using assms
-    proof (induct w arbitrary: p k)
-      case (Nil)
-      show ?case by simp
-    next
-      case (Cons a w)
-      have "snd (degen.target (a # w) (p, k)) = snd (degen.target w (dexecute a (p, k)))" by simp
-      also obtain q where 1: "dexecute a (p, k) = (q, k)" unfolding dexecute_def using Cons(2, 3) by auto
-      also have "snd (degen.target w \<dots>) = k" using Cons 1 by auto
-      finally show ?case by this
-    qed
-    lemma degen_nodes_fst[simp]: "fst ` degen.nodes = nodes"
-    proof (intro equalityI subsetI)
-      show "p \<in> fst ` degen.nodes" if "p \<in> nodes" for p
-      using that
-      proof induct
-        case (initial p)
-        have 1: "dinitial (p, 0)" using initial unfolding dinitial_def by simp
-        show ?case using 1 by (auto intro: rev_image_eqI)
-      next
-        case (execute p a)
-        obtain k where 1: "(p, k) \<in> degen.nodes" using execute(2) by auto
-        have 2: "denabled a (p, k)" unfolding denabled_def using execute(3) by simp
-        have 3: "execute a p = fst (dexecute a (p, k))" unfolding dexecute_def by simp
-        show ?case using 1 2 3 by auto
-      qed
-      show "p \<in> nodes" if "p \<in> fst ` degen.nodes" for p
-      using that
-      proof
-        fix pk
-        assume "pk \<in> degen.nodes" "p = fst pk"
-        then show "p \<in> nodes"
-          by (induct arbitrary: p) (auto simp: dexecute_def denabled_def dinitial_def)
-      qed
-    qed
-    lemma degen_nodes_snd_empty:
-      assumes "condition = []"
-      shows "snd ` degen.nodes \<subseteq> {0}"
-    proof -
-      have 1: "dinitial (p, k) \<Longrightarrow> k = 0" for p k unfolding dinitial_def by simp
-      have 2: "snd (dexecute a (p, k)) = 0" for a p k using assms unfolding dexecute_def by simp
-      show ?thesis using 1 2 by (auto elim: degen.nodes.cases)
-    qed
-    lemma degen_nodes_snd_nonempty:
-      assumes "condition \<noteq> []"
-      shows "snd ` degen.nodes \<subseteq> {0 ..< length condition}"
-    proof -
-      have 1: "dinitial (p, k) \<Longrightarrow> k < length condition" for p k using assms unfolding dinitial_def by simp
-      have 2: "snd (dexecute a (p, k)) < length condition" for a p k using assms unfolding dexecute_def by simp
-      show ?thesis using 1 2 by (auto elim: degen.nodes.cases)
-    qed
-    lemma degen_nodes_empty:
-      assumes "condition = []"
-      shows "degen.nodes = nodes \<times> {0}"
-    proof -
-      have "(p, k) \<in> degen.nodes \<longleftrightarrow> p \<in> fst ` degen.nodes \<and> k = 0" for p k
-        using degen_nodes_snd_empty assms by (force simp del: degen_nodes_fst)
-      then show ?thesis by auto
-    qed
-    lemma degen_nodes_nonempty:
-      assumes "condition \<noteq> []"
-      shows "degen.nodes \<subseteq> nodes \<times> {0 ..< length condition}"
-      using subset_fst_snd degen_nodes_fst degen_nodes_snd_nonempty[OF assms] by blast
-    lemma degen_nodes: "degen.nodes \<subseteq> nodes \<times> {0 ..< max 1 (length condition)}"
-      using degen_nodes_empty degen_nodes_nonempty by force
-
-    lemma degen_nodes_finite[iff]: "finite degen.nodes \<longleftrightarrow> finite nodes"
-    proof
-      show "finite nodes" if "finite degen.nodes" using that by (auto simp flip: degen_nodes_fst)
-      show "finite degen.nodes" if "finite nodes" using degen_nodes that by (auto intro: finite_subset)
-    qed
-    lemma degen_nodes_card: "card degen.nodes \<le> max 1 (length condition) * card nodes"
-    proof (cases "finite nodes")
-      case True
-      have "card degen.nodes \<le> card (nodes \<times> {0 ..< max 1 (length condition)})"
-        using degen_nodes True by (blast intro: card_mono)
-      also have "\<dots> = max 1 (length condition) * card nodes" unfolding card_cartesian_product by simp
-      finally show ?thesis by this
-    next
-      case False
-      then have "card nodes = 0" "card degen.nodes = 0" by auto
-      then show ?thesis by simp
-    qed
-
-    definition dcondition :: "'state degen pred" where
-      "dcondition \<equiv> \<lambda> (p, k). k \<ge> length condition \<or> (condition ! k) p"
-
-    lemma degen_skip_condition:
-      assumes "k < length condition"
-      assumes "infs dcondition (degen.trace r (p, k))"
-      obtains s t q
-      where "r = s @- t" "degen.target s (p, k) = (q, k)" "dcondition (q, k)"
-    proof -
-      have 1: "Collect dcondition \<inter> sset ((p, k) ## degen.trace r (p, k)) \<noteq> {}"
-        using infs_any assms(2) by auto
-      obtain u q l v where 2:
-        "(p, k) ## degen.trace r (p, k) = u @- (q, l) ## v"
-        "Collect dcondition \<inter> set u = {}"
-        "(q, l) \<in> Collect dcondition"
-        using 1 by (force elim!: split_stream_first)
-      let ?w = "(p, k) # degen.states (stake (length u) r) (p, k)"
-      have "?w = stake (Suc (length u)) ((p, k) ## degen.trace r (p, k))" by simp
-      also have "\<dots> = stake (Suc (length u)) (u @- (q, l) ## v)" unfolding 2(1) by rule
-      also have "\<dots> = u @ [(q, l)]" unfolding stake_Suc using eq_shift by auto
-      finally have 3: "(p, k) # degen.states (stake (length u) r) (p, k) = u @ [(q, l)]" by this
-      have 4: "degen.target (stake (length u) r) (p, k) = (q, l)" unfolding degen.target_alt_def 3 by simp
-      have 5: "Collect dcondition \<inter> set (butlast ?w) = {}" using 2(2) 3 by simp
-      have "l = snd (q, l)" by simp
-      also have "\<dots> = snd (degen.target (stake (length u) r) (p, k))" using 4 by simp
-      also have "\<dots> = k" using degen_target_snd' assms(1) 5 unfolding dcondition_def by blast
-      finally have 6: "k = l" by rule
-      show ?thesis
-      proof
-        show "r = stake (length u) r @- sdrop (length u) r" by simp
-        show "degen.target (stake (length u) r) (p, k) = (q, k)" using 4 6 by simp
-        show "dcondition (q, k)" using 2(3) 6 by auto
-      qed
-    qed
-    lemma degen_skip_increment:
-      assumes "k < length condition"
-      assumes "infs dcondition (degen.trace w (p, k))"
-      obtains u v q
-      where "w = u @- v" "u \<noteq> []" "degen.target u (p, k) = (q, Suc k mod length condition)"
-    proof -
-      obtain u v q where 1: "w = u @- v" "degen.target u (p, k) = (q, k)" "dcondition (q, k)"
-        using degen_skip_condition assms by this
-      show ?thesis
-      proof
-        show "w = (u @ [shd v]) @- stl v" using 1(1) by simp
-        show "u @ [shd v] \<noteq> []" by simp
-        show "degen.target (u @ [shd v]) (p, k) = (execute (shd v) q, Suc k mod length condition)"
-          using assms(1) 1(2, 3) by (simp add: dexecute_def dcondition_def)
-      qed
-    qed
-    lemma degen_skip_arbitrary:
-      assumes "k < length condition" "l < length condition"
-      assumes "infs dcondition (degen.trace w (p, k))"
-      obtains u v q
-      where "w = u @- v" "degen.target u (p, k) = (q, l)"
-    using assms
-    proof (induct "nat ((int l - int k) mod length condition)" arbitrary: thesis l)
-      case (0)
-      have 1: "length condition > 0" using assms(1) by auto
-      have 2: "(int l - int k) mod length condition = 0" using 0(1) 1 by (auto intro: antisym)
-      have 3: "int l mod length condition = int k mod length condition" 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 "degen.target [] (p, k) = (p, l)" using 4 by simp
-      qed
-    next
-      case (Suc n)
-      have 1: "length condition > 0" using assms(1) by auto
-      define l' where "l' = nat ((int l - 1) mod length condition)"
-      obtain u v q where 2: "w = u @- v" "degen.target u (p, k) = (q, l')"
-      proof (rule Suc(1))
-        have 2: "Suc n < length condition" 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 condition" using 2 by simp
-        also have "\<dots> = (int l - int k - 1) mod length condition" using Suc(2) by (simp add: mod_simps)
-        also have "\<dots> = (int l - 1 - int k) mod length condition" by (simp add: algebra_simps)
-        also have "\<dots> = (int l' - int k) mod length condition" using l'_def 1 by (simp add: mod_simps)
-        finally show "n = nat ((int l' - int k) mod length condition)" by this
-        show "k < length condition" using Suc(4) by this
-        show "l' < length condition" using nat_less_iff l'_def 1 by simp
-        show "infs dcondition (degen.trace w (p, k))" using Suc(6) by this
-      qed
-      obtain vu vv t where 3: "v = vu @- vv" "degen.target vu (q, l') = (t, Suc l' mod length condition)"
-      proof (rule degen_skip_increment)
-        show "l' < length condition" using nat_less_iff l'_def 1 by simp
-        show "infs dcondition (degen.trace v (q, l'))" using Suc(6) 2 by simp
-      qed
-      show ?case
-      proof (rule Suc(3))
-        have "l = nat (int l)" by simp
-        also have "int l = int l mod length condition" using Suc(5) by simp
-        also have "\<dots> = int (Suc l') mod length condition" using l'_def 1 by (simp add: mod_simps)
-        finally have 4: "l = Suc l' mod length condition" using nat_mod_as_int by metis
-        show "w = (u @ vu) @- vv" unfolding 2(1) 3(1) by simp
-        show "degen.target (u @ vu) (p, k) = (t, l)" using 2(2) 3(2) 4 by simp
-      qed
-    qed
-    lemma degen_skip_arbitrary_condition:
-      assumes "l < length condition"
-      assumes "infs dcondition (degen.trace w (p, k))"
-      obtains u v q
-      where "w = u @- v" "degen.target u (p, k) = (q, l)" "dcondition (q, l)"
-    proof -
-      obtain x y where 10: "dexecute (shd w) (p, k) = (x, y)" by force
-      have 11: "y < length condition" using mod_Suc assms(1) 10 unfolding dexecute_def by auto
-      have 12: "infs dcondition (degen.trace (stl w) (x, y))"
-        using 10 by (metis alw_ev_stl assms(2) sscan.simps(2))
-      obtain u v q where 1: "stl w = u @- v" "degen.target u (x, y) = (q, l)"
-        using degen_skip_arbitrary 11 assms(1) 12 by this
-      have 2: "infs dcondition (degen.trace v (q, l))" using 12 1(2) unfolding 1(1) by simp
-      obtain vu vv t where 3: "v = vu @- vv" "degen.target vu (q, l) = (t, l)" "dcondition (t, l)"
-        using degen_skip_condition assms(1) 2 by this
-      show ?thesis
-      proof
-        show "w = (shd w # u @ vu) @- vv" using 1(1) 3(1)
-          by (simp add: "1"(1) "3"(1) stream.expand)
-        show "degen.target (shd w # u @ vu) (p, k) = (t, l)" using 1(2) 3(2) 10 by simp
-        show "dcondition (t, l)" using 3(3) by this
-      qed
-    qed
-
-    lemma degen_infs_1:
-      assumes "infs dcondition (degen.trace w (p, k))"
-      assumes "P \<in> set condition"
-      shows "infs P (trace w p)"
-    using assms
-    proof (coinduction arbitrary: w p k rule: infs_trace_coinduct)
-      case (infs_trace w p k)
-      obtain l where 1: "P = condition ! l" "l < length condition"
-        using infs_trace(2) in_set_conv_nth by metis
-      obtain u v q where 2: "w = u @- v" "degen.target  u (p, k) = (q, l)" "dcondition (q, l)"
-        using degen_skip_arbitrary_condition 1(2) infs_trace(1) by this
-      have 3: "q = target u p" using 2(2) degen_target_fst by (metis fst_conv)
-      obtain p' k' where 4: "dexecute (shd w) (p, k) = (p', k')" by force
-      have 5: "infs dcondition (degen.trace (shd w ## stl w) (p, k))" using infs_trace(1) by simp
-      show ?case
-      proof (intro exI conjI)
-        show "w = u @- v" using 2(1) by this
-        show "P (target u p)" using 1(2) 2(3) unfolding dcondition_def 1(1) 3 by simp
-        show "w = [shd w] @- stl w" "[shd w] \<noteq> []" "stl w = stl w" by auto
-        show "target [shd w] p = p'" using 4 by (simp add: dexecute_def)
-        show "infs dcondition (degen.trace (stl w) (p', k'))" using 4 5 unfolding sscan_scons by simp
-        show "P \<in> set condition" using infs_trace(2) by this
-      qed
-    qed
-    lemma degen_infs_2:
-      assumes "\<And> P. P \<in> set condition \<Longrightarrow> infs P (trace w p)"
-      shows "infs dcondition (degen.trace w (p, k))"
-    using assms
-    proof (coinduction arbitrary: w p k rule: degen.infs_trace_coinduct)
-      case (infs_trace w p k)
-      show ?case
-      proof (cases "k < length condition")
-        case True
-        have 1: "infs (condition ! k) (trace w p)" using infs_trace True by simp
-        have 2: "{q. (condition ! k) q} \<inter> sset (p ## trace w p) \<noteq> {}" using infs_any 1 by auto
-        obtain ys x zs where 3:
-          "p ## trace w p = ys @- x ## zs"
-          "{q. (condition ! k) q} \<inter> set ys = {}"
-          "x \<in> {q. (condition ! k) q}"
-          using split_stream_first 2 by this
-        define u where "u = stake (length ys) w"
-        define v where "v = sdrop (length ys) w"
-        obtain q l where 4: "degen.target u (p, k) = (q, l)" by force
-        have "p # states u p = stake (length (ys @ [x])) (p ## trace w p)" unfolding u_def by simp
-        also have "p ## trace w p = (ys @ [x]) @- zs" using 3(1) by simp
-        also have "stake (length (ys @ [x])) \<dots> = ys @ [x]" unfolding stake_shift by simp
-        finally have 5: "p # states u p = ys @ [x]" by this
-        have 6: "butlast (p # states u p) = ys" using 5 by auto
-        have "l = snd (degen.target u (p, k))" unfolding 4 by simp
-        also have "\<dots> = k" using degen_target_snd 3(2) 6 True by fast
-        finally have 7: "k = l" by rule
-        have "q = fst (degen.target u (p, k))" unfolding 4 by simp
-        also have "\<dots> = target u p" using degen_target_fst by this
-        also have "\<dots> = last (p # states u p)" unfolding scan_last by rule
-        also have "\<dots> = x" unfolding 5 by simp
-        finally have 8: "q = x" by this
-        have 9: "(condition ! l) q" using 3(3) unfolding 7 8 by simp
-        obtain x y where 10: "dexecute (shd w) (p, k) = (x, y)" by force
-        have 11: "\<forall> P \<in> set condition. infs P (trace (shd w ## stl w) p)" using infs_trace by simp
-        have 12: "execute (shd w) p = x" using infs_trace(1) 10 unfolding dexecute_def by auto
-        show ?thesis
-        proof (intro exI conjI)
-          show "w = u @- v" unfolding u_def v_def by simp
-          show "dcondition (degen.target u (p, k))" using 4 9 by (auto simp: dcondition_def)
-          show "w = [shd w] @- stl w" "[shd w] \<noteq> []" "stl w = stl w" by auto
-          show "degen.target [shd w] (p, k) = (x, y)" using 10 by simp
-          show "\<forall> P. P \<in> set condition \<longrightarrow> infs P (trace (stl w) x)"
-            using 11 12 unfolding sscan_scons by simp
-        qed
-      next
-        case False
-        obtain x y where 10: "dexecute (shd w) (p, k) = (x, y)" by force
-        have 11: "\<forall> P \<in> set condition. infs P (trace (shd w ## stl w) p)" using infs_trace by simp
-        have 12: "execute (shd w) p = x" using infs_trace(1) 10 unfolding dexecute_def by auto
-        show ?thesis
-        proof (intro exI conjI)
-          show "w = [] @- w" by simp
-          show "dcondition (degen.target [] (p, k))" unfolding dcondition_def using False by simp
-          show "w = [shd w] @- stl w" "[shd w] \<noteq> []" "stl w = stl w" by auto
-          show "degen.target [shd w] (p, k) = (x, y)" using 10 by simp
-          show "\<forall> P. P \<in> set condition \<longrightarrow> infs P (trace (stl w) x)"
-            using 11 12 unfolding sscan_scons by simp
-        qed
-      qed
-    qed
-
-    lemma degen_infs: "infs dcondition (degen.trace w (p, k)) \<longleftrightarrow>
-      (\<forall> P \<in> set condition. infs P (trace w p))"
-      using degen_infs_1 degen_infs_2 by auto
-
-  end
-
-end
\ No newline at end of file