diff --git a/thys/Transition_Systems_and_Automata/Automata/DBTA/DBTA.thy b/thys/Transition_Systems_and_Automata/Automata/DBTA/DBTA.thy
new file mode 100644
--- /dev/null
+++ b/thys/Transition_Systems_and_Automata/Automata/DBTA/DBTA.thy
@@ -0,0 +1,26 @@
+section \<open>Deterministic Büchi Transition Automata\<close>
+
+theory DBTA
+imports "../Deterministic"
+begin
+
+  datatype ('label, 'state) dbta = dbta
+    (alphabet: "'label set")
+    (initial: "'state")
+    (transition: "'label \<Rightarrow> 'state \<Rightarrow> 'state")
+    (accepting: "('state \<times> 'label \<times> 'state) pred")
+
+  global_interpretation dbta: automaton dbta alphabet initial transition accepting
+    defines path = dbta.path and run = dbta.run and reachable = dbta.reachable and nodes = dbta.nodes
+    by unfold_locales auto
+  global_interpretation dbta: automaton_run dbta alphabet initial transition accepting
+    "\<lambda> P w r p. infs P (p ## r ||| w ||| r)"
+    defines language = dbta.language
+    by standard
+
+  abbreviation target where "target \<equiv> dbta.target"
+  abbreviation states where "states \<equiv> dbta.states"
+  abbreviation trace where "trace \<equiv> dbta.trace"
+  abbreviation successors where "successors \<equiv> dbta.successors TYPE('label)"
+
+end
\ No newline at end of file
diff --git a/thys/Transition_Systems_and_Automata/Automata/DBTA/DBTA_Combine.thy b/thys/Transition_Systems_and_Automata/Automata/DBTA/DBTA_Combine.thy
new file mode 100644
--- /dev/null
+++ b/thys/Transition_Systems_and_Automata/Automata/DBTA/DBTA_Combine.thy
@@ -0,0 +1,115 @@
+section \<open>Deterministic Büchi Transition Automata Combinations\<close>
+
+theory DBTA_Combine
+imports DBTA DGBTA
+begin
+
+  (* TODO: exact copy-paste from NBTA, abstract *)
+  global_interpretation degeneralization: automaton_degeneralization_run
+    dgbta dgbta.alphabet dgbta.initial dgbta.transition dgbta.accepting "\<lambda> P w r p. gen infs P (p ## r ||| w ||| r)"
+    dbta dbta.alphabet dbta.initial dbta.transition dbta.accepting "\<lambda> P w r p. infs P (p ## r ||| w ||| r)"
+    id "\<lambda> ((p, k), a, (q, l)). ((p, a, q), k)"
+    defines degeneralize = degeneralization.degeneralize
+  proof
+    fix w :: "'a stream"
+    fix r :: "'b stream"
+    fix cs p k
+    let ?f = "\<lambda> ((p, k), a, (q, l)). ((p, a, q), k)"
+    let ?s = "sscan (count cs \<circ> id) (p ## r ||| w ||| r) k"
+    have "infs (degen cs \<circ> ?f) ((p, k) ## (r ||| ?s) ||| w ||| (r ||| ?s)) \<longleftrightarrow>
+      infs (degen cs) (smap ?f ((p, k) ## (r ||| ?s) ||| w ||| (r ||| ?s)))"
+      by (simp add: comp_def)
+    also have "smap ?f ((p, k) ## (r ||| ?s) ||| w ||| (r ||| ?s)) = (p ## r ||| w ||| r) ||| k ## ?s"
+      by (coinduction arbitrary: p k r w) (auto simp: eq_scons simp flip: szip_unfold sscan_scons)
+    also have "\<dots> = (p ## r ||| w ||| r) ||| k ## sscan (count cs) (p ## r ||| w ||| r) k" by simp
+    also have "infs (degen cs) \<dots> = gen infs cs (p ## r ||| w ||| r)" using degen_infs by this
+    finally show "infs (degen cs \<circ> ?f) ((p, k) ## (r ||| ?s) ||| w ||| (r ||| ?s)) \<longleftrightarrow>
+      gen infs cs (p ## r ||| w ||| r)" by this
+  qed
+
+  lemmas degeneralize_language[simp] = degeneralization.degeneralize_language[folded DBTA.language_def]
+  lemmas degeneralize_nodes_finite[iff] = degeneralization.degeneralize_nodes_finite[folded DBTA.nodes_def]
+  lemmas degeneralize_nodes_card = degeneralization.degeneralize_nodes_card[folded DBTA.nodes_def]
+
+  global_interpretation intersection: automaton_intersection_run
+    dbta.dbta dbta.alphabet dbta.initial dbta.transition dbta.accepting "\<lambda> P w r p. infs P (p ## r ||| w ||| r)"
+    dbta.dbta dbta.alphabet dbta.initial dbta.transition dbta.accepting "\<lambda> P w r p. infs P (p ## r ||| w ||| r)"
+    dgbta.dgbta dgbta.alphabet dgbta.initial dgbta.transition dgbta.accepting "\<lambda> P w r p. gen infs P (p ## r ||| w ||| r)"
+    "\<lambda> c\<^sub>1 c\<^sub>2. [c\<^sub>1 \<circ> (\<lambda> ((p\<^sub>1, p\<^sub>2), a, (q\<^sub>1, q\<^sub>2)). (p\<^sub>1, a, q\<^sub>1)), c\<^sub>2 \<circ> (\<lambda> ((p\<^sub>1, p\<^sub>2), a, (q\<^sub>1, q\<^sub>2)). (p\<^sub>2, a, q\<^sub>2))]"
+    defines intersect' = intersection.combine
+  proof
+    fix w :: "'a stream"
+    fix u :: "'b stream"
+    fix v :: "'c stream"
+    fix c\<^sub>1 c\<^sub>2 p q
+    let ?tfst = "\<lambda> ((p\<^sub>1, p\<^sub>2), a, (q\<^sub>1, q\<^sub>2)). (p\<^sub>1, a, q\<^sub>1)"
+    let ?tsnd = "\<lambda> ((p\<^sub>1, p\<^sub>2), a, (q\<^sub>1, q\<^sub>2)). (p\<^sub>2, a, q\<^sub>2)"
+    have "gen infs [c\<^sub>1 \<circ> ?tfst, c\<^sub>2 \<circ> ?tsnd] ((p, q) ## (u ||| v) ||| w ||| u ||| v) \<longleftrightarrow>
+      infs c\<^sub>1 (smap ?tfst ((p, q) ## (u ||| v) ||| w ||| u ||| v)) \<and>
+      infs c\<^sub>2 (smap ?tsnd ((p, q) ## (u ||| v) ||| w ||| u ||| v))"
+      unfolding gen_def by (simp add: comp_def)
+    also have "smap ?tfst ((p, q) ## (u ||| v) ||| w ||| u ||| v) = p ## u ||| w ||| u"
+      by (coinduction arbitrary: p q u v w) (auto simp flip: szip_unfold, metis stream.collapse)
+    also have "smap ?tsnd ((p, q) ## (u ||| v) ||| w ||| u ||| v) = q ## v ||| w ||| v"
+      by (coinduction arbitrary: p q u v w) (auto simp flip: szip_unfold, metis stream.collapse)
+    finally show "gen infs [c\<^sub>1 \<circ> ?tfst, c\<^sub>2 \<circ> ?tsnd] ((p, q) ## (u ||| v) ||| w ||| u ||| v) \<longleftrightarrow>
+      infs c\<^sub>1 (p ## u ||| w ||| u) \<and> infs c\<^sub>2 (q ## v ||| w ||| v)" by this
+  qed
+
+  lemmas intersect'_language[simp] = intersection.combine_language[folded DGBTA.language_def]
+  lemmas intersect'_nodes_finite = intersection.combine_nodes_finite[folded DGBTA.nodes_def]
+  lemmas intersect'_nodes_card = intersection.combine_nodes_card[folded DGBTA.nodes_def]
+
+  global_interpretation union: automaton_union_run
+    dbta.dbta dbta.alphabet dbta.initial dbta.transition dbta.accepting "\<lambda> P w r p. infs P (p ## r ||| w ||| r)"
+    dbta.dbta dbta.alphabet dbta.initial dbta.transition dbta.accepting "\<lambda> P w r p. infs P (p ## r ||| w ||| r)"
+    dbta.dbta dbta.alphabet dbta.initial dbta.transition dbta.accepting "\<lambda> P w r p. infs P (p ## r ||| w ||| r)"
+    "\<lambda> c\<^sub>1 c\<^sub>2 pq. (c\<^sub>1 \<circ> (\<lambda> ((p\<^sub>1, p\<^sub>2), a, (q\<^sub>1, q\<^sub>2)). (p\<^sub>1, a, q\<^sub>1))) pq \<or> (c\<^sub>2 \<circ> (\<lambda> ((p\<^sub>1, p\<^sub>2), a, (q\<^sub>1, q\<^sub>2)). (p\<^sub>2, a, q\<^sub>2))) pq"
+    defines union = union.combine
+  proof
+    fix w :: "'a stream"
+    fix u :: "'b stream"
+    fix v :: "'c stream"
+    fix c\<^sub>1 c\<^sub>2 p q
+    let ?tfst = "\<lambda> ((p\<^sub>1, p\<^sub>2), a, (q\<^sub>1, q\<^sub>2)). (p\<^sub>1, a, q\<^sub>1)"
+    let ?tsnd = "\<lambda> ((p\<^sub>1, p\<^sub>2), a, (q\<^sub>1, q\<^sub>2)). (p\<^sub>2, a, q\<^sub>2)"
+    have "infs (\<lambda> pq. (c\<^sub>1 \<circ> (\<lambda> ((p\<^sub>1, p\<^sub>2), a, q\<^sub>1, q\<^sub>2). (p\<^sub>1, a, q\<^sub>1))) pq \<or>
+       (c\<^sub>2 \<circ> (\<lambda> ((p\<^sub>1, p\<^sub>2), a, q\<^sub>1, q\<^sub>2). (p\<^sub>2, a, q\<^sub>2))) pq) ((p, q) ## (u ||| v) ||| w ||| (u ||| v))  \<longleftrightarrow>
+      infs c\<^sub>1 (smap ?tfst ((p, q) ## (u ||| v) ||| w ||| u ||| v)) \<or>
+      infs c\<^sub>2 (smap ?tsnd ((p, q) ## (u ||| v) ||| w ||| u ||| v))"
+      by (simp add: comp_def)
+    also have "smap ?tfst ((p, q) ## (u ||| v) ||| w ||| u ||| v) = p ## u ||| w ||| u"
+      by (coinduction arbitrary: p q u v w) (auto simp flip: szip_unfold, metis stream.collapse)
+    also have "smap ?tsnd ((p, q) ## (u ||| v) ||| w ||| u ||| v) = q ## v ||| w ||| v"
+      by (coinduction arbitrary: p q u v w) (auto simp flip: szip_unfold, metis stream.collapse)
+    finally show "infs (\<lambda> pq. (c\<^sub>1 \<circ> (\<lambda> ((p\<^sub>1, p\<^sub>2), a, q\<^sub>1, q\<^sub>2). (p\<^sub>1, a, q\<^sub>1))) pq \<or>
+       (c\<^sub>2 \<circ> (\<lambda> ((p\<^sub>1, p\<^sub>2), a, q\<^sub>1, q\<^sub>2). (p\<^sub>2, a, q\<^sub>2))) pq) ((p, q) ## (u ||| v) ||| w ||| (u ||| v)) \<longleftrightarrow>
+      infs c\<^sub>1 (p ## u ||| w ||| u) \<or> infs c\<^sub>2 (q ## v ||| w ||| v)" by this
+  qed
+
+  lemmas union_language = union.combine_language
+  lemmas union_nodes_finite = union.combine_nodes_finite
+  lemmas union_nodes_card = union.combine_nodes_card
+
+  abbreviation intersect where "intersect A B \<equiv> degeneralize (intersect' A B)"
+
+  lemma intersect_language[simp]: "DBTA.language (intersect A B) = DBTA.language A \<inter> DBTA.language B"
+    by simp
+  lemma intersect_nodes_finite:
+    assumes "finite (DBTA.nodes A)" "finite (DBTA.nodes B)"
+    shows "finite (DBTA.nodes (intersect A B))"
+    using intersect'_nodes_finite assms by simp
+  lemma intersect_nodes_card:
+    assumes "finite (DBTA.nodes A)" "finite (DBTA.nodes B)"
+    shows "card (DBTA.nodes (intersect A B)) \<le> 2 * card (DBTA.nodes A) * card (DBTA.nodes B)"
+  proof -
+    have "card (DBTA.nodes (intersect A B)) \<le>
+      max 1 (length (dgbta.accepting (intersect' A B))) * card (DGBTA.nodes (intersect' A B))"
+      using degeneralize_nodes_card by this
+    also have "length (dgbta.accepting (intersect' A B)) = 2" by simp
+    also have "card (DGBTA.nodes (intersect' A B)) \<le> card (DBTA.nodes A) * card (DBTA.nodes B)"
+      using intersect'_nodes_card assms by this
+    finally show ?thesis by simp
+  qed
+
+end
\ No newline at end of file
diff --git a/thys/Transition_Systems_and_Automata/Automata/DBTA/DGBTA.thy b/thys/Transition_Systems_and_Automata/Automata/DBTA/DGBTA.thy
new file mode 100644
--- /dev/null
+++ b/thys/Transition_Systems_and_Automata/Automata/DBTA/DGBTA.thy
@@ -0,0 +1,26 @@
+section \<open>Deterministic Generalized Büchi Transition Automata\<close>
+
+theory DGBTA
+imports "../Deterministic"
+begin
+
+  datatype ('label, 'state) dgbta = dgbta
+    (alphabet: "'label set")
+    (initial: "'state")
+    (transition: "'label \<Rightarrow> 'state \<Rightarrow> 'state")
+    (accepting: "('state \<times> 'label \<times> 'state) pred gen")
+
+  global_interpretation dgbta: automaton dgbta alphabet initial transition accepting
+    defines path = dgbta.path and run = dgbta.run and reachable = dgbta.reachable and nodes = dgbta.nodes
+    by unfold_locales auto
+  global_interpretation dgbta: automaton_run dgbta alphabet initial transition accepting
+    "\<lambda> P w r p. gen infs P (p ## r ||| w ||| r)"
+    defines language = dgbta.language
+    by standard
+
+  abbreviation target where "target \<equiv> dgbta.target"
+  abbreviation states where "states \<equiv> dgbta.states"
+  abbreviation trace where "trace \<equiv> dgbta.trace"
+  abbreviation successors where "successors \<equiv> dgbta.successors TYPE('label)"
+
+end
\ No newline at end of file
diff --git a/thys/Transition_Systems_and_Automata/Automata/NBTA/NBTA.thy b/thys/Transition_Systems_and_Automata/Automata/NBTA/NBTA.thy
new file mode 100644
--- /dev/null
+++ b/thys/Transition_Systems_and_Automata/Automata/NBTA/NBTA.thy
@@ -0,0 +1,26 @@
+section \<open>Nondeterministic Büchi Transition Automata\<close>
+
+theory NBTA
+imports "../Nondeterministic"
+begin
+
+  datatype ('label, 'state) nbta = nbta
+    (alphabet: "'label set")
+    (initial: "'state set")
+    (transition: "'label \<Rightarrow> 'state \<Rightarrow> 'state set")
+    (accepting: "('state \<times> 'label \<times> 'state) pred")
+
+  global_interpretation nbta: automaton nbta alphabet initial transition accepting
+    defines path = nbta.path and run = nbta.run and reachable = nbta.reachable and nodes = nbta.nodes
+    by unfold_locales auto
+  global_interpretation nbta: automaton_run nbta alphabet initial transition accepting
+    "\<lambda> P w r p. infs P (p ## r ||| w ||| r)"
+    defines language = nbta.language
+    by standard
+
+  abbreviation target where "target \<equiv> nbta.target"
+  abbreviation states where "states \<equiv> nbta.states"
+  abbreviation trace where "trace \<equiv> nbta.trace"
+  abbreviation successors where "successors \<equiv> nbta.successors TYPE('label)"
+
+end
\ No newline at end of file
diff --git a/thys/Transition_Systems_and_Automata/Automata/NBTA/NBTA_Combine.thy b/thys/Transition_Systems_and_Automata/Automata/NBTA/NBTA_Combine.thy
new file mode 100644
--- /dev/null
+++ b/thys/Transition_Systems_and_Automata/Automata/NBTA/NBTA_Combine.thy
@@ -0,0 +1,80 @@
+section \<open>Nondeterministic Büchi Transition Automata Combinations\<close>
+
+theory NBTA_Combine
+imports NBTA NGBTA
+begin
+
+  global_interpretation degeneralization: automaton_degeneralization_run
+    ngbta ngbta.alphabet ngbta.initial ngbta.transition ngbta.accepting "\<lambda> P w r p. gen infs P (p ## r ||| w ||| r)"
+    nbta nbta.alphabet nbta.initial nbta.transition nbta.accepting "\<lambda> P w r p. infs P (p ## r ||| w ||| r)"
+    id "\<lambda> ((p, k), a, (q, l)). ((p, a, q), k)"
+    defines degeneralize = degeneralization.degeneralize
+  proof
+    fix w :: "'a stream"
+    fix r :: "'b stream"
+    fix cs p k
+    let ?f = "\<lambda> ((p, k), a, (q, l)). ((p, a, q), k)"
+    let ?s = "sscan (count cs \<circ> id) (p ## r ||| w ||| r) k"
+    have "infs (degen cs \<circ> ?f) ((p, k) ## (r ||| ?s) ||| w ||| (r ||| ?s)) \<longleftrightarrow>
+      infs (degen cs) (smap ?f ((p, k) ## (r ||| ?s) ||| w ||| (r ||| ?s)))"
+      by (simp add: comp_def)
+    also have "smap ?f ((p, k) ## (r ||| ?s) ||| w ||| (r ||| ?s)) = (p ## r ||| w ||| r) ||| k ## ?s"
+      by (coinduction arbitrary: p k r w) (auto simp: eq_scons simp flip: szip_unfold sscan_scons)
+    also have "\<dots> = (p ## r ||| w ||| r) ||| k ## sscan (count cs) (p ## r ||| w ||| r) k" by simp
+    also have "infs (degen cs) \<dots> = gen infs cs (p ## r ||| w ||| r)" using degen_infs by this
+    finally show "infs (degen cs \<circ> ?f) ((p, k) ## (r ||| ?s) ||| w ||| (r ||| ?s)) \<longleftrightarrow>
+      gen infs cs (p ## r ||| w ||| r)" by this
+  qed
+
+  lemmas degeneralize_language[simp] = degeneralization.degeneralize_language[folded NBTA.language_def]
+  lemmas degeneralize_nodes_finite[iff] = degeneralization.degeneralize_nodes_finite[folded NBTA.nodes_def]
+
+  global_interpretation intersection: automaton_intersection_run
+    nbta nbta.alphabet nbta.initial nbta.transition nbta.accepting "\<lambda> P w r p. infs P (p ## r ||| w ||| r)"
+    nbta nbta.alphabet nbta.initial nbta.transition nbta.accepting "\<lambda> P w r p. infs P (p ## r ||| w ||| r)"
+    ngbta ngbta.alphabet ngbta.initial ngbta.transition ngbta.accepting "\<lambda> P w r p. gen infs P (p ## r ||| w ||| r)"
+    "\<lambda> c\<^sub>1 c\<^sub>2. [c\<^sub>1 \<circ> (\<lambda> ((p\<^sub>1, p\<^sub>2), a, (q\<^sub>1, q\<^sub>2)). (p\<^sub>1, a, q\<^sub>1)), c\<^sub>2 \<circ> (\<lambda> ((p\<^sub>1, p\<^sub>2), a, (q\<^sub>1, q\<^sub>2)). (p\<^sub>2, a, q\<^sub>2))]"
+    defines intersect' = intersection.intersect
+  proof
+    fix w :: "'a stream"
+    fix u :: "'b stream"
+    fix v :: "'c stream"
+    fix c\<^sub>1 c\<^sub>2 p q
+    let ?tfst = "\<lambda> ((p\<^sub>1, p\<^sub>2), a, (q\<^sub>1, q\<^sub>2)). (p\<^sub>1, a, q\<^sub>1)"
+    let ?tsnd = "\<lambda> ((p\<^sub>1, p\<^sub>2), a, (q\<^sub>1, q\<^sub>2)). (p\<^sub>2, a, q\<^sub>2)"
+    have "gen infs [c\<^sub>1 \<circ> ?tfst, c\<^sub>2 \<circ> ?tsnd] ((p, q) ## (u ||| v) ||| w ||| u ||| v) \<longleftrightarrow>
+      infs c\<^sub>1 (smap ?tfst ((p, q) ## (u ||| v) ||| w ||| u ||| v)) \<and>
+      infs c\<^sub>2 (smap ?tsnd ((p, q) ## (u ||| v) ||| w ||| u ||| v))"
+      unfolding gen_def by (simp add: comp_def)
+    also have "smap ?tfst ((p, q) ## (u ||| v) ||| w ||| u ||| v) = p ## u ||| w ||| u"
+      by (coinduction arbitrary: p q u v w) (auto simp flip: szip_unfold, metis stream.collapse)
+    also have "smap ?tsnd ((p, q) ## (u ||| v) ||| w ||| u ||| v) = q ## v ||| w ||| v"
+      by (coinduction arbitrary: p q u v w) (auto simp flip: szip_unfold, metis stream.collapse)
+    finally show "gen infs [c\<^sub>1 \<circ> ?tfst, c\<^sub>2 \<circ> ?tsnd] ((p, q) ## (u ||| v) ||| w ||| u ||| v) \<longleftrightarrow>
+      infs c\<^sub>1 (p ## u ||| w ||| u) \<and> infs c\<^sub>2 (q ## v ||| w ||| v)" by this
+  qed
+
+  lemmas intersect'_language[simp] = intersection.intersect_language[folded NGBTA.language_def]
+  lemmas intersect'_nodes_finite[intro] = intersection.intersect_nodes_finite[folded NGBTA.nodes_def]
+
+  global_interpretation union: automaton_union_run
+    nbta nbta.alphabet nbta.initial nbta.transition nbta.accepting "\<lambda> P w r p. infs P (p ## r ||| w ||| r)"
+    nbta nbta.alphabet nbta.initial nbta.transition nbta.accepting "\<lambda> P w r p. infs P (p ## r ||| w ||| r)"
+    nbta nbta.alphabet nbta.initial nbta.transition nbta.accepting "\<lambda> P w r p. infs P (p ## r ||| w ||| r)"
+    "\<lambda> c\<^sub>1 c\<^sub>2 m. case m of (Inl p, a, Inl q) \<Rightarrow> c\<^sub>1 (p, a, q) | (Inr p, a, Inr q) \<Rightarrow> c\<^sub>2 (p, a, q)"
+    defines union = union.union
+    by (unfold_locales) (auto simp add: szip_smap_fold comp_def case_prod_unfold simp flip: stream.map)
+
+  lemmas union_language = union.union_language
+  lemmas union_nodes_finite = union.union_nodes_finite
+
+  abbreviation intersect where "intersect A B \<equiv> degeneralize (intersect' A B)"
+
+  lemma intersect_language[simp]: "NBTA.language (intersect A B) = NBTA.language A \<inter> NBTA.language B"
+    by simp
+  lemma intersect_nodes_finite[intro]:
+    assumes "finite (NBTA.nodes A)" "finite (NBTA.nodes B)"
+    shows "finite (NBTA.nodes (intersect A B))"
+    using intersect'_nodes_finite assms by simp
+
+end
\ No newline at end of file
diff --git a/thys/Transition_Systems_and_Automata/Automata/NBTA/NGBTA.thy b/thys/Transition_Systems_and_Automata/Automata/NBTA/NGBTA.thy
new file mode 100644
--- /dev/null
+++ b/thys/Transition_Systems_and_Automata/Automata/NBTA/NGBTA.thy
@@ -0,0 +1,26 @@
+section \<open>Nondeterministic Generalized Büchi Transition Automata\<close>
+
+theory NGBTA
+imports "../Nondeterministic"
+begin
+
+  datatype ('label, 'state) ngbta = ngbta
+    (alphabet: "'label set")
+    (initial: "'state set")
+    (transition: "'label \<Rightarrow> 'state \<Rightarrow> 'state set")
+    (accepting: "('state \<times> 'label \<times> 'state) pred gen")
+
+  global_interpretation ngbta: automaton ngbta alphabet initial transition accepting
+    defines path = ngbta.path and run = ngbta.run and reachable = ngbta.reachable and nodes = ngbta.nodes
+    by unfold_locales auto
+  global_interpretation ngbta: automaton_run ngbta alphabet initial transition accepting
+    "\<lambda> P w r p. gen infs P (p ## r ||| w ||| r)"
+    defines language = ngbta.language
+    by standard
+
+  abbreviation target where "target \<equiv> ngbta.target"
+  abbreviation states where "states \<equiv> ngbta.states"
+  abbreviation trace where "trace \<equiv> ngbta.trace"
+  abbreviation successors where "successors \<equiv> ngbta.successors TYPE('label)"
+
+end
\ No newline at end of file
diff --git a/thys/Transition_Systems_and_Automata/Basic/Sequence_Zip.thy b/thys/Transition_Systems_and_Automata/Basic/Sequence_Zip.thy
--- a/thys/Transition_Systems_and_Automata/Basic/Sequence_Zip.thy
+++ b/thys/Transition_Systems_and_Automata/Basic/Sequence_Zip.thy
@@ -1,164 +1,171 @@
 section \<open>Zipping Sequences\<close>
 
 theory Sequence_Zip
 imports "Sequence_LTL"
 begin
 
   subsection \<open>Zipping Lists\<close>
 
   notation zip (infixr "||" 51)
 
   lemmas [simp] = zip_map_fst_snd
 
   lemma split_zip[no_atp]: "(\<And> x. PROP P x) \<equiv> (\<And> y z. length y = length z \<Longrightarrow> PROP P (y || z))"
   proof
     fix y z
     assume 1: "\<And> x. PROP P x"
     show "PROP P (y || z)" using 1 by this
   next
     fix x :: "('a \<times> 'b) list"
     assume 1: "\<And> y z. length y = length z \<Longrightarrow> PROP P (y || z)"
     have 2: "length (map fst x) = length (map snd x)" by simp
     have 3: "PROP P (map fst x || map snd x)" using 1 2 by this
     show "PROP P x" using 3 by simp
   qed
   lemma split_zip_all[no_atp]: "(\<forall> x. P x) \<longleftrightarrow> (\<forall> y z. length y = length z \<longrightarrow> P (y || z))"
     by (fastforce iff: split_zip)
   lemma split_zip_ex[no_atp]: "(\<exists> x. P x) \<longleftrightarrow> (\<exists> y z. length y = length z \<and> P (y || z))"
     by (fastforce iff: split_zip)
 
   lemma zip_eq[iff]:
     assumes "length u = length v" "length r = length s"
     shows "u || v = r || s \<longleftrightarrow> u = r \<and> v = s"
     using assms zip_eq_conv by metis
 
   lemma list_rel_pred_zip: "list_all2 P xs ys \<longleftrightarrow> length xs = length ys \<and> list_all (case_prod P) (xs || ys)"
     unfolding list_all2_conv_all_nth list_all_length by auto
 
   lemma list_choice_zip: "list_all (\<lambda> x. \<exists> y. P x y) xs \<longleftrightarrow>
     (\<exists> ys. length ys = length xs \<and> list_all (case_prod P) (xs || ys))"
     unfolding list_choice list_rel_pred_zip by metis
   lemma list_choice_pair: "list_all (\<lambda> xy. case_prod (\<lambda> x y. \<exists> z. P x y z) xy) (xs || ys) \<longleftrightarrow>
     (\<exists> zs. length zs = min (length xs) (length ys) \<and> list_all (\<lambda> (x, y, z). P x y z) (xs || ys || zs))"
   proof -
     have 1: "list_all (\<lambda> (xy, z). case xy of (x, y) \<Rightarrow> P x y z) ((xs || ys) || zs) \<longleftrightarrow>
       list_all (\<lambda> (x, y, z). P x y z) (xs || ys || zs)" for zs
       unfolding zip_assoc list.pred_map by (auto intro!: list.pred_cong)
     have 2: "(\<lambda> (x, y). \<exists> z. P x y z) = (\<lambda> xy. \<exists> z. case xy of (x, y) \<Rightarrow> P x y z)" by auto
     show ?thesis unfolding list_choice_zip 1 2 by force
   qed
 
   lemma list_rel_zip[iff]:
     assumes "length u = length v" "length r = length s"
     shows "list_all2 (rel_prod A B) (u || v) (r || s) \<longleftrightarrow> list_all2 A u r \<and> list_all2 B v s"
   proof safe
     assume [transfer_rule]: "list_all2 (rel_prod A B) (u || v) (r || s)"
     have "list_all2 A (map fst (u || v)) (map fst (r || s))" by transfer_prover
     then show "list_all2 A u r" using assms by simp
     have "list_all2 B (map snd (u || v)) (map snd (r || s))" by transfer_prover
     then show "list_all2 B v s" using assms by simp
   next
     assume [transfer_rule]: "list_all2 A u r" "list_all2 B v s"
     show "list_all2 (rel_prod A B) (u || v) (r || s)" by transfer_prover
   qed
 
   lemma zip_last[simp]:
     assumes "xs || ys \<noteq> []" "length xs = length ys"
     shows "last (xs || ys) = (last xs, last ys)"
   proof -
     have 1: "xs \<noteq> []" "ys \<noteq> []" using assms(1) by auto
     have "last (xs || ys) = (xs || ys) ! (length (xs || ys) - 1)" using last_conv_nth assms by blast
     also have "\<dots> = (xs ! (length (xs || ys) - 1), ys ! (length (xs || ys) - 1))" using assms 1 by simp
     also have "\<dots> = (xs ! (length xs - 1), ys ! (length ys - 1))" using assms(2) by simp
     also have "\<dots> = (last xs, last ys)" using last_conv_nth 1 by metis
     finally show ?thesis by this
   qed
 
   subsection \<open>Zipping Streams\<close>
 
   notation szip (infixr "|||" 51)
 
   lemmas [simp] = szip_unfold
 
+  lemma smap_szip_same: "smap f (xs ||| xs) = smap (\<lambda> x. f (x, x)) xs" by (coinduction arbitrary: xs) (auto)
+
   lemma szip_smap[simp]: "smap fst zs ||| smap snd zs = zs" by (coinduction arbitrary: zs) (auto)
   lemma szip_smap_fst[simp]: "smap fst (xs ||| ys) = xs" by (coinduction arbitrary: xs ys) (auto)
   lemma szip_smap_snd[simp]: "smap snd (xs ||| ys) = ys" by (coinduction arbitrary: xs ys) (auto)
 
+  lemma szip_smap_both: "smap f xs ||| smap g ys = smap (map_prod f g) (xs ||| ys)" by (coinduction arbitrary: xs ys) (auto)
+  lemma szip_smap_left: "smap f xs ||| ys = smap (apfst f) (xs ||| ys)" by (coinduction arbitrary: xs ys) (auto)
+  lemma szip_smap_right: "xs ||| smap f ys = smap (apsnd f) (xs ||| ys)" by (coinduction arbitrary: xs ys) (auto)
+  lemmas szip_smap_fold = szip_smap_both szip_smap_left szip_smap_right
+
   lemma szip_sconst_smap_fst: "sconst a ||| xs = smap (Pair a) xs"
     by (coinduction arbitrary: xs) (auto)
   lemma szip_sconst_smap_snd: "xs ||| sconst a = smap (prod.swap \<circ> Pair a) xs"
     by (coinduction arbitrary: xs) (auto)
 
   lemma split_szip[no_atp]: "(\<And> x. PROP P x) \<equiv> (\<And> y z. PROP P (y ||| z))"
   proof
     fix y z
     assume 1: "\<And> x. PROP P x"
     show "PROP P (y ||| z)" using 1 by this
   next
     fix x
     assume 1: "\<And> y z. PROP P (y ||| z)"
     have 2: "PROP P (smap fst x ||| smap snd x)" using 1 by this
     show "PROP P x" using 2 by simp
   qed
   lemma split_szip_all[no_atp]: "(\<forall> x. P x) \<longleftrightarrow> (\<forall> y z. P (y ||| z))" by (fastforce iff: split_szip)
   lemma split_szip_ex[no_atp]: "(\<exists> x. P x) \<longleftrightarrow> (\<exists> y z. P (y ||| z))" by (fastforce iff: split_szip)
 
   lemma szip_eq[iff]: "u ||| v = r ||| s \<longleftrightarrow> u = r \<and> v = s"
     using szip_smap_fst szip_smap_snd by metis
 
   lemma stream_rel_szip[iff]:
     "stream_all2 (rel_prod A B) (u ||| v) (r ||| s) \<longleftrightarrow> stream_all2 A u r \<and> stream_all2 B v s"
   proof safe
     assume [transfer_rule]: "stream_all2 (rel_prod A B) (u ||| v) (r ||| s)"
     have "stream_all2 A (smap fst (u ||| v)) (smap fst (r ||| s))" by transfer_prover
     then show "stream_all2 A u r" by simp
     have "stream_all2 B (smap snd (u ||| v)) (smap snd (r ||| s))" by transfer_prover
     then show "stream_all2 B v s" by simp
   next
     assume [transfer_rule]: "stream_all2 A u r" "stream_all2 B v s"
     show "stream_all2 (rel_prod A B) (u ||| v) (r ||| s)" by transfer_prover
   qed
 
   lemma szip_shift[simp]:
     assumes "length u = length s"
     shows "u @- v ||| s @- t = (u || s) @- (v ||| t)"
     using assms by (simp add: eq_shift stake_shift sdrop_shift)
 
   lemma szip_sset_fst[simp]: "fst ` sset (u ||| v) = sset u" by (metis stream.set_map szip_smap_fst)
   lemma szip_sset_snd[simp]: "snd ` sset (u ||| v) = sset v" by (metis stream.set_map szip_smap_snd)
   lemma szip_sset_elim[elim]:
     assumes "(a, b) \<in> sset (u ||| v)"
     obtains "a \<in> sset u" "b \<in> sset v"
     using assms by (metis image_eqI fst_conv snd_conv szip_sset_fst szip_sset_snd)
   lemma szip_sset[simp]: "sset (u ||| v) \<subseteq> sset u \<times> sset v" by auto
 
   lemma sset_szip_finite[iff]: "finite (sset (u ||| v)) \<longleftrightarrow> finite (sset u) \<and> finite (sset v)"
   proof safe
     assume 1: "finite (sset (u ||| v))"
     have 2: "finite (fst ` sset (u ||| v))" using 1 by blast
     have 3: "finite (snd ` sset (u ||| v))" using 1 by blast
     show "finite (sset u)" using 2 by simp
     show "finite (sset v)" using 3 by simp
   next
     assume 1: "finite (sset u)" "finite (sset v)"
     have "sset (u ||| v) \<subseteq> sset u \<times> sset v" by simp
     also have "finite \<dots>" using 1 by simp
     finally show "finite (sset (u ||| v))" by this
   qed
 
   lemma infs_szip_fst[iff]: "infs (P \<circ> fst) (u ||| v) \<longleftrightarrow> infs P u"
   proof -
     have "infs (P \<circ> fst) (u ||| v) \<longleftrightarrow> infs P (smap fst (u ||| v))"
       by (simp add: comp_def del: szip_smap_fst)
     also have "\<dots> \<longleftrightarrow> infs P u" by simp
     finally show ?thesis by this
   qed
   lemma infs_szip_snd[iff]: "infs (P \<circ> snd) (u ||| v) \<longleftrightarrow> infs P v"
   proof -
     have "infs (P \<circ> snd) (u ||| v) \<longleftrightarrow> infs P (smap snd (u ||| v))"
       by (simp add: comp_def del: szip_smap_snd)
     also have "\<dots> \<longleftrightarrow> infs P v" by simp
     finally show ?thesis by this
   qed
 
 end
\ No newline at end of file