diff --git a/thys/Transition_Systems_and_Automata/Automata/NBA/NGBA_Algorithms.thy b/thys/Transition_Systems_and_Automata/Automata/NBA/NGBA_Algorithms.thy
new file mode 100644
--- /dev/null
+++ b/thys/Transition_Systems_and_Automata/Automata/NBA/NGBA_Algorithms.thy
@@ -0,0 +1,67 @@
+section \<open>Algorithms on Nondeterministic Generalized Büchi Automata\<close>
+
+theory NGBA_Algorithms
+imports
+  NBA_Algorithms
+  NGBA_Implement
+  NBA_Combine
+begin
+
+  subsection \<open>Implementations\<close>
+
+  context
+  begin
+
+    interpretation autoref_syn by this
+
+    (* TODO: move *)
+    lemma degen_param[param, autoref_rules]: "(degen, degen) \<in> \<langle>S \<rightarrow> bool_rel\<rangle> list_rel \<rightarrow> S \<times>\<^sub>r nat_rel \<rightarrow> bool_rel"
+    proof (intro fun_relI)
+      fix cs ds ak bl
+      assume "(cs, ds) \<in> \<langle>S \<rightarrow> bool_rel\<rangle> list_rel" "(ak, bl) \<in>  S \<times>\<^sub>r nat_rel"
+      then show "(degen cs ak, degen ds bl) \<in> bool_rel"
+        unfolding degen_def list_rel_def fun_rel_def list_all2_conv_all_nth
+        by (cases "snd ak < length cs") (auto 0 3)
+    qed
+
+    lemma count_alt_def: "Degeneralization.count cs a k =
+      (if k < length cs
+      then if (cs ! k) a then Suc k mod length cs else k
+      else if List.null cs then k else 0)"
+      unfolding count_def null_def by rule
+
+    (* TODO: move *)
+    lemmas [param] = null_transfer[unfolded pred_bool_Id, to_set]
+
+    (* TODO: move *)
+    lemma count_param[param, autoref_rules]: "(Degeneralization.count, Degeneralization.count) \<in>
+      \<langle>A \<rightarrow> bool_rel\<rangle> list_rel \<rightarrow> A \<rightarrow> nat_rel \<rightarrow> nat_rel"
+      unfolding count_alt_def by parametricity
+
+    (* TODO: why do we need this? *)
+    lemma degeneralize_annotated: "degeneralize A = nba
+      (ngba.alphabet A)
+      (ngba.initial A \<times> ({0} ::: \<langle>nat_rel\<rangle> list_set_rel))
+      (\<lambda> a (p, k). ngba.transition A a p \<times> ({Degeneralization.count (ngba.accepting A) p k} ::: \<langle>nat_rel\<rangle> list_set_rel))
+      (degen (ngba.accepting A))"
+      unfolding degeneralization.degeneralize_def by simp
+
+    schematic_goal ngba_degeneralize: "(?f :: ?'a, degeneralize) \<in> ?R"
+      unfolding degeneralize_annotated by autoref
+    concrete_definition ngba_degeneralize uses ngba_degeneralize
+    lemmas ngba_degeneralize_refine[autoref_rules] = ngba_degeneralize.refine
+
+    schematic_goal nba_intersect':
+      assumes [autoref_rules]: "(seq, HOL.eq) \<in> L \<rightarrow> L \<rightarrow> bool_rel"
+      shows "(?f, intersect') \<in> \<langle>L, S\<rangle> nbai_nba_rel \<rightarrow> \<langle>L, T\<rangle> nbai_nba_rel \<rightarrow> \<langle>L, S \<times>\<^sub>r T\<rangle> ngbai_ngba_rel"
+      unfolding intersection.intersect_def by autoref
+    concrete_definition nba_intersect' uses nba_intersect'
+    lemma nba_intersect'_refine[autoref_rules]:
+      assumes "GEN_OP seq HOL.eq (L \<rightarrow> L \<rightarrow> bool_rel)"
+      shows "(nba_intersect' seq, intersect') \<in>
+        \<langle>L, S\<rangle> nbai_nba_rel \<rightarrow> \<langle>L, T\<rangle> nbai_nba_rel \<rightarrow> \<langle>L, S \<times>\<^sub>r T\<rangle> ngbai_ngba_rel"
+      using nba_intersect'.refine assms unfolding autoref_tag_defs by this
+
+  end
+
+end
\ No newline at end of file
diff --git a/thys/Transition_Systems_and_Automata/Automata/NBA/NGBA_Implement.thy b/thys/Transition_Systems_and_Automata/Automata/NBA/NGBA_Implement.thy
new file mode 100644
--- /dev/null
+++ b/thys/Transition_Systems_and_Automata/Automata/NBA/NGBA_Implement.thy
@@ -0,0 +1,102 @@
+section \<open>Implementation of Nondeterministic Generalized Büchi Automata\<close>
+
+theory NGBA_Implement
+imports
+  "NGBA_Refine"
+  "../../Basic/Implement"
+begin
+
+  consts i_ngba_scheme :: "interface \<Rightarrow> interface \<Rightarrow> interface"
+
+  context
+  begin
+
+    interpretation autoref_syn by this
+
+    lemma ngba_scheme_itype[autoref_itype]:
+      "ngba ::\<^sub>i \<langle>L\<rangle>\<^sub>i i_set \<rightarrow>\<^sub>i \<langle>S\<rangle>\<^sub>i i_set \<rightarrow>\<^sub>i (L \<rightarrow>\<^sub>i S \<rightarrow>\<^sub>i \<langle>S\<rangle>\<^sub>i i_set) \<rightarrow>\<^sub>i \<langle>\<langle>S\<rangle>\<^sub>i i_set\<rangle>\<^sub>i i_list \<rightarrow>\<^sub>i
+        \<langle>L, S\<rangle>\<^sub>i i_ngba_scheme"
+      "alphabet ::\<^sub>i \<langle>L, S\<rangle>\<^sub>i i_ngba_scheme \<rightarrow>\<^sub>i \<langle>L\<rangle>\<^sub>i i_set"
+      "initial ::\<^sub>i \<langle>L, S\<rangle>\<^sub>i i_ngba_scheme \<rightarrow>\<^sub>i \<langle>S\<rangle>\<^sub>i i_set"
+      "transition ::\<^sub>i \<langle>L, S\<rangle>\<^sub>i i_ngba_scheme \<rightarrow>\<^sub>i L \<rightarrow>\<^sub>i S \<rightarrow>\<^sub>i \<langle>S\<rangle>\<^sub>i i_set"
+      "accepting ::\<^sub>i \<langle>L, S\<rangle>\<^sub>i i_ngba_scheme \<rightarrow>\<^sub>i \<langle>\<langle>S\<rangle>\<^sub>i i_set\<rangle>\<^sub>i i_list"
+      by auto
+
+  end
+
+  datatype ('label, 'state) ngbai = ngbai
+    (alphabeti: "'label list")
+    (initiali: "'state list")
+    (transitioni: "'label \<Rightarrow> 'state \<Rightarrow> 'state list")
+    (acceptingi: "('state \<Rightarrow> bool) list")
+
+  definition ngbai_rel :: "('label\<^sub>1 \<times> 'label\<^sub>2) set \<Rightarrow> ('state\<^sub>1 \<times> 'state\<^sub>2) set \<Rightarrow>
+    (('label\<^sub>1, 'state\<^sub>1) ngbai \<times> ('label\<^sub>2, 'state\<^sub>2) ngbai) set" where
+    [to_relAPP]: "ngbai_rel L S \<equiv> {(A\<^sub>1, A\<^sub>2).
+      (alphabeti A\<^sub>1, alphabeti A\<^sub>2) \<in> \<langle>L\<rangle> list_rel \<and>
+      (initiali A\<^sub>1, initiali A\<^sub>2) \<in> \<langle>S\<rangle> list_rel \<and>
+      (transitioni A\<^sub>1, transitioni A\<^sub>2) \<in> L \<rightarrow> S \<rightarrow> \<langle>S\<rangle> list_rel \<and>
+      (acceptingi A\<^sub>1, acceptingi A\<^sub>2) \<in> \<langle>S \<rightarrow> bool_rel\<rangle> list_rel}"
+
+  lemma ngbai_param[param]:
+    "(ngbai, ngbai) \<in> \<langle>L\<rangle> list_rel \<rightarrow> \<langle>S\<rangle> list_rel \<rightarrow> (L \<rightarrow> S \<rightarrow> \<langle>S\<rangle> list_rel) \<rightarrow>
+      \<langle>S \<rightarrow> bool_rel\<rangle> list_rel \<rightarrow> \<langle>L, S\<rangle> ngbai_rel"
+    "(alphabeti, alphabeti) \<in> \<langle>L, S\<rangle> ngbai_rel \<rightarrow> \<langle>L\<rangle> list_rel"
+    "(initiali, initiali) \<in> \<langle>L, S\<rangle> ngbai_rel \<rightarrow> \<langle>S\<rangle> list_rel"
+    "(transitioni, transitioni) \<in> \<langle>L, S\<rangle> ngbai_rel \<rightarrow> L \<rightarrow> S \<rightarrow> \<langle>S\<rangle> list_rel"
+    "(acceptingi, acceptingi) \<in> \<langle>L, S\<rangle> ngbai_rel \<rightarrow> \<langle>S \<rightarrow> bool_rel\<rangle> list_rel"
+    unfolding ngbai_rel_def fun_rel_def by auto
+
+  definition ngbai_ngba_rel :: "('label\<^sub>1 \<times> 'label\<^sub>2) set \<Rightarrow> ('state\<^sub>1 \<times> 'state\<^sub>2) set \<Rightarrow>
+    (('label\<^sub>1, 'state\<^sub>1) ngbai \<times> ('label\<^sub>2, 'state\<^sub>2) ngba) set" where
+    [to_relAPP]: "ngbai_ngba_rel L S \<equiv> {(A\<^sub>1, A\<^sub>2).
+      (alphabeti A\<^sub>1, alphabet A\<^sub>2) \<in> \<langle>L\<rangle> list_set_rel \<and>
+      (initiali A\<^sub>1, initial A\<^sub>2) \<in> \<langle>S\<rangle> list_set_rel \<and>
+      (transitioni A\<^sub>1, transition A\<^sub>2) \<in> L \<rightarrow> S \<rightarrow> \<langle>S\<rangle> list_set_rel \<and>
+      (acceptingi A\<^sub>1, accepting A\<^sub>2) \<in> \<langle>S \<rightarrow> bool_rel\<rangle> list_rel}"
+
+  lemmas [autoref_rel_intf] = REL_INTFI[of ngbai_ngba_rel i_ngba_scheme]
+
+  lemma ngbai_ngba_param[param, autoref_rules]:
+    "(ngbai, ngba) \<in> \<langle>L\<rangle> list_set_rel \<rightarrow> \<langle>S\<rangle> list_set_rel \<rightarrow> (L \<rightarrow> S \<rightarrow> \<langle>S\<rangle> list_set_rel) \<rightarrow>
+      \<langle>S \<rightarrow> bool_rel\<rangle> list_rel \<rightarrow> \<langle>L, S\<rangle> ngbai_ngba_rel"
+    "(alphabeti, alphabet) \<in> \<langle>L, S\<rangle> ngbai_ngba_rel \<rightarrow> \<langle>L\<rangle> list_set_rel"
+    "(initiali, initial) \<in> \<langle>L, S\<rangle> ngbai_ngba_rel \<rightarrow> \<langle>S\<rangle> list_set_rel"
+    "(transitioni, transition) \<in> \<langle>L, S\<rangle> ngbai_ngba_rel \<rightarrow> L \<rightarrow> S \<rightarrow> \<langle>S\<rangle> list_set_rel"
+    "(acceptingi, accepting) \<in> \<langle>L, S\<rangle> ngbai_ngba_rel \<rightarrow> \<langle>S \<rightarrow> bool_rel\<rangle> list_rel"
+    unfolding ngbai_ngba_rel_def fun_rel_def by auto
+
+  definition ngbai_ngba :: "('label, 'state) ngbai \<Rightarrow> ('label, 'state) ngba" where
+    "ngbai_ngba A \<equiv> ngba (set (alphabeti A)) (set (initiali A)) (\<lambda> a p. set (transitioni A a p)) (acceptingi A)"
+  definition ngbai_invar :: "('label, 'state) ngbai \<Rightarrow> bool" where
+    "ngbai_invar A \<equiv> distinct (alphabeti A) \<and> distinct (initiali A) \<and> (\<forall> a p. distinct (transitioni A a p))"
+
+  lemma ngbai_ngba_id_param[param]: "(ngbai_ngba, id) \<in> \<langle>L, S\<rangle> ngbai_ngba_rel \<rightarrow> \<langle>L, S\<rangle> ngba_rel"
+  proof
+    fix Ai A
+    assume 1: "(Ai, A) \<in> \<langle>L, S\<rangle> ngbai_ngba_rel"
+    have 2: "ngbai_ngba Ai = ngba (set (alphabeti Ai)) (set (initiali Ai))
+      (\<lambda> a p. set (transitioni Ai a p)) (acceptingi Ai)" unfolding ngbai_ngba_def by rule
+    have 3: "id A = ngba (id (alphabet A)) (id (initial A))
+      (\<lambda> a p. id (transition A a p)) (accepting A)" by simp
+    show "(ngbai_ngba Ai, id A) \<in> \<langle>L, S\<rangle> ngba_rel" unfolding 2 3 using 1 by parametricity
+  qed
+
+  lemma ngbai_ngba_br: "\<langle>Id, Id\<rangle> ngbai_ngba_rel = br ngbai_ngba ngbai_invar"
+  proof safe
+    show "(A, B) \<in> \<langle>Id, Id\<rangle> ngbai_ngba_rel" if "(A, B) \<in> br ngbai_ngba ngbai_invar"
+      for A and B :: "('a, 'b) ngba"
+      using that unfolding ngbai_ngba_rel_def ngbai_ngba_def ngbai_invar_def
+      by (auto simp: in_br_conv list_set_rel_def)
+    show "(A, B) \<in> br ngbai_ngba ngbai_invar" if "(A, B) \<in> \<langle>Id, Id\<rangle> ngbai_ngba_rel"
+      for A and B :: "('a, 'b) ngba"
+    proof -
+      have 1: "(ngbai_ngba A, id B) \<in> \<langle>Id, Id\<rangle> ngba_rel" using that by parametricity
+      have 2: "ngbai_invar A"
+        using ngbai_ngba_param(2 - 5)[param_fo, OF that]
+        by (auto simp: in_br_conv list_set_rel_def ngbai_invar_def)
+      show ?thesis using 1 2 unfolding in_br_conv by auto
+    qed
+  qed
+
+end
\ No newline at end of file
diff --git a/thys/Transition_Systems_and_Automata/Automata/NBA/NGBA_Refine.thy b/thys/Transition_Systems_and_Automata/Automata/NBA/NGBA_Refine.thy
new file mode 100644
--- /dev/null
+++ b/thys/Transition_Systems_and_Automata/Automata/NBA/NGBA_Refine.thy
@@ -0,0 +1,57 @@
+section \<open>Relations on Nondeterministic Generalized Büchi Automata\<close>
+
+theory NGBA_Refine
+imports
+  "NGBA"
+  "../../Transition_Systems/Transition_System_Refine"
+begin
+
+  definition ngba_rel :: "('label\<^sub>1 \<times> 'label\<^sub>2) set \<Rightarrow> ('state\<^sub>1 \<times> 'state\<^sub>2) set \<Rightarrow>
+    (('label\<^sub>1, 'state\<^sub>1) ngba \<times> ('label\<^sub>2, 'state\<^sub>2) ngba) set" where
+    [to_relAPP]: "ngba_rel L S \<equiv> {(A\<^sub>1, A\<^sub>2).
+      (alphabet A\<^sub>1, alphabet A\<^sub>2) \<in> \<langle>L\<rangle> set_rel \<and>
+      (initial A\<^sub>1, initial A\<^sub>2) \<in> \<langle>S\<rangle> set_rel \<and>
+      (transition A\<^sub>1, transition A\<^sub>2) \<in> L \<rightarrow> S \<rightarrow> \<langle>S\<rangle> set_rel \<and>
+      (accepting A\<^sub>1, accepting A\<^sub>2) \<in> \<langle>S \<rightarrow> bool_rel\<rangle> list_rel}"
+
+  lemma ngba_param[param]:
+    "(ngba, ngba) \<in> \<langle>L\<rangle> set_rel \<rightarrow> \<langle>S\<rangle> set_rel \<rightarrow> (L \<rightarrow> S \<rightarrow> \<langle>S\<rangle> set_rel) \<rightarrow> \<langle>S \<rightarrow> bool_rel\<rangle> list_rel \<rightarrow>
+      \<langle>L, S\<rangle> ngba_rel"
+    "(alphabet, alphabet) \<in> \<langle>L, S\<rangle> ngba_rel \<rightarrow> \<langle>L\<rangle> set_rel"
+    "(initial, initial) \<in> \<langle>L, S\<rangle> ngba_rel \<rightarrow> \<langle>S\<rangle> set_rel"
+    "(transition, transition) \<in> \<langle>L, S\<rangle> ngba_rel \<rightarrow> L \<rightarrow> S \<rightarrow> \<langle>S\<rangle> set_rel"
+    "(accepting, accepting) \<in> \<langle>L, S\<rangle> ngba_rel \<rightarrow> \<langle>S \<rightarrow> bool_rel\<rangle> list_rel"
+    unfolding ngba_rel_def fun_rel_def by auto
+
+  lemma ngba_rel_id[simp]: "\<langle>Id, Id\<rangle> ngba_rel = Id" unfolding ngba_rel_def using ngba.expand by auto
+
+  lemma enableds_param[param]: "(ngba.enableds, ngba.enableds) \<in> \<langle>L, S\<rangle> ngba_rel \<rightarrow> S \<rightarrow> \<langle>L \<times>\<^sub>r S\<rangle> set_rel"
+    using ngba_param(2, 4) unfolding ngba.enableds_def fun_rel_def set_rel_def by fastforce
+  lemma paths_param[param]: "(ngba.paths, ngba.paths) \<in> \<langle>L, S\<rangle> ngba_rel \<rightarrow> S \<rightarrow> \<langle>\<langle>L \<times>\<^sub>r S\<rangle> list_rel\<rangle> set_rel"
+    using enableds_param[param_fo] by parametricity
+  lemma runs_param[param]: "(ngba.runs, ngba.runs) \<in> \<langle>L, S\<rangle> ngba_rel \<rightarrow> S \<rightarrow> \<langle>\<langle>L \<times>\<^sub>r S\<rangle> stream_rel\<rangle> set_rel"
+    using enableds_param[param_fo] by parametricity
+
+  lemma reachable_param[param]: "(reachable, reachable) \<in> \<langle>L, S\<rangle> ngba_rel \<rightarrow> S \<rightarrow> \<langle>S\<rangle> set_rel"
+  proof -
+    have 1: "reachable A p = (\<lambda> wr. target wr p) ` ngba.paths A p" for A :: "('label, 'state) ngba" and p
+      unfolding ngba.reachable_alt_def ngba.paths_def by auto
+    show ?thesis unfolding 1 using enableds_param[param_fo] by parametricity
+  qed
+  lemma nodes_param[param]: "(nodes, nodes) \<in> \<langle>L, S\<rangle> ngba_rel \<rightarrow> \<langle>S\<rangle> set_rel"
+    unfolding ngba.nodes_alt_def Collect_mem_eq by parametricity
+
+  (* TODO: move *)
+  lemma gen_param[param]: "(gen, gen) \<in> (A \<rightarrow> B \<rightarrow> bool_rel) \<rightarrow> \<langle>A\<rangle> list_rel \<rightarrow> B \<rightarrow> bool_rel"
+    unfolding gen_def by parametricity
+
+  lemma language_param[param]: "(language, language) \<in> \<langle>L, S\<rangle> ngba_rel \<rightarrow> \<langle>\<langle>L\<rangle> stream_rel\<rangle> set_rel"
+  proof -
+    have 1: "language A = (\<Union> p \<in> initial A. \<Union> wr \<in> ngba.runs A p.
+      if gen infs (accepting A) (trace wr p) then {smap fst wr} else {})"
+      for A :: "('label, 'state) ngba"
+      unfolding ngba.language_def ngba.runs_def image_def by (auto iff: split_szip_ex)
+    show ?thesis unfolding 1 using enableds_param[param_fo] by parametricity
+  qed
+
+end
\ No newline at end of file
diff --git a/thys/Transition_Systems_and_Automata/ROOT b/thys/Transition_Systems_and_Automata/ROOT
--- a/thys/Transition_Systems_and_Automata/ROOT
+++ b/thys/Transition_Systems_and_Automata/ROOT
@@ -1,36 +1,38 @@
 chapter AFP
 
 session Transition_Systems_and_Automata (AFP) = "Collections" +
   options [timeout = 2400]
   sessions
     "DFS_Framework"
     "Gabow_SCC"
   directories
+    "Basic"
+    "Transition_Systems"
     "Automata"
     "Automata/DBA"
     "Automata/DCA"
     "Automata/DFA"
     "Automata/DRA"
     "Automata/NBA"
     "Automata/NFA"
-    "Basic"
-    "Transition_Systems"
   theories
     "Basic/Basic"
     "Basic/Sequence"
     "Basic/Sequence_Zip"
     "Basic/Sequence_LTL"
     "Basic/Maps"
     "Basic/Acceptance"
     "Transition_Systems/Transition_System"
     "Transition_Systems/Transition_System_Extra"
     "Transition_Systems/Transition_System_Construction"
     "Automata/DFA/DFA"
     "Automata/NFA/NFA"
+    "Automata/NBA/NBA_Combine"
     "Automata/NBA/NBA_Translate"
+    "Automata/NBA/NGBA_Algorithms"
     "Automata/DBA/DBA_Combine"
     "Automata/DCA/DCA_Combine"
     "Automata/DRA/DRA_Combine"
     "Automata/DRA/DRA_Translate"
   document_files
     "root.tex"