diff --git a/thys/Transition_Systems_and_Automata/Automata/DFA/DFA.thy b/thys/Transition_Systems_and_Automata/Automata/DFA/DFA.thy
--- a/thys/Transition_Systems_and_Automata/Automata/DFA/DFA.thy
+++ b/thys/Transition_Systems_and_Automata/Automata/DFA/DFA.thy
@@ -1,73 +1,48 @@
 section \<open>Deterministic Finite Automata\<close>
 
 theory DFA
-imports
-  "../../Transition_Systems/Transition_System"
-  "../../Transition_Systems/Transition_System_Extra"
-  "../../Transition_Systems/Transition_System_Construction"
+imports "../Deterministic"
 begin
 
-  record ('label, 'state) dfa =
-    succ :: "'label \<Rightarrow> 'state \<Rightarrow> 'state"
-    initial :: "'state"
-    accepting :: "'state set"
-
-  global_interpretation dfa: transition_system_initial "succ A" "top" "\<lambda> p. p = initial A"
-    for A
-    defines path = dfa.path and run = dfa.run and reachable = dfa.reachable and nodes = dfa.nodes
-    by this
-
-  abbreviation target :: "('label, 'state, 'more) dfa_scheme \<Rightarrow> 'label list \<Rightarrow> 'state \<Rightarrow> 'state" where
-    "target \<equiv> dfa.target TYPE('more)"
-  abbreviation states :: "('label, 'state, 'more) dfa_scheme \<Rightarrow> 'label list \<Rightarrow> 'state \<Rightarrow> 'state list" where
-    "states \<equiv> dfa.states TYPE('more)"
-  abbreviation trace :: "('label, 'state, 'more) dfa_scheme \<Rightarrow> 'label stream \<Rightarrow> 'state \<Rightarrow> 'state stream" where
-    "trace \<equiv> dfa.trace TYPE('more)"
-
-  abbreviation successors :: "('label, 'state, 'more) dfa_scheme \<Rightarrow> 'state \<Rightarrow> 'state set" where
-    "successors \<equiv> dfa.successors TYPE('label) TYPE('more)"
-
-  definition language :: "('label, 'state) dfa \<Rightarrow> 'label list set" where
-    "language A \<equiv> {w. target A w (initial A) \<in> accepting A}"
-
-  lemma language[intro]:
-    assumes "target A w (initial A) \<in> accepting A"
-    shows "w \<in> language A"
-    using assms unfolding language_def by auto
-  lemma language_elim[elim]:
-    assumes "w \<in> language A"
-    obtains "target A w (initial A) \<in> accepting A"
-    using assms unfolding language_def by auto
+  datatype ('label, 'state) dfa = dfa
+    (alphabet: "'label set")
+    (initial: "'state")
+    (transition: "'label \<Rightarrow> 'state \<Rightarrow> 'state")
+    (accepting: "'state pred")
 
-  definition complement :: "('label, 'state) dfa \<Rightarrow> ('label, 'state) dfa" where
-    "complement A \<equiv> \<lparr> succ = succ A, initial = initial A, accepting = - accepting A \<rparr>"
-
-  lemma complement_simps[simp]:
-    "succ (complement A) = succ A"
-    "initial (complement A) = initial A"
-    "accepting (complement A) = - accepting A"
-    unfolding complement_def by simp+
-
-  lemma complement_language[simp]: "language (complement A) = - language A" by force
+  global_interpretation dfa: automaton dfa alphabet initial transition accepting
+    defines path = dfa.path and run = dfa.run and reachable = dfa.reachable and nodes = dfa.nodes
+    by unfold_locales auto
+  global_interpretation dfa: automaton_path dfa alphabet initial transition accepting "\<lambda> P w r p. P (last (p # r))"
+    defines language = dfa.language
+    by standard
 
-  definition product :: "('label, 'state\<^sub>1) dfa \<Rightarrow> ('label, 'state\<^sub>2) dfa \<Rightarrow>
-    ('label, 'state\<^sub>1 \<times> 'state\<^sub>2) dfa" where
-    "product A B \<equiv>
-    \<lparr>
-      succ = \<lambda> a (p\<^sub>1, p\<^sub>2). (succ A a p\<^sub>1, succ B a p\<^sub>2),
-      initial = (initial A, initial B),
-      accepting = accepting A \<times> accepting B
-    \<rparr>"
+  abbreviation target where "target \<equiv> dfa.target"
+  abbreviation states where "states \<equiv> dfa.states"
+  abbreviation trace where "trace \<equiv> dfa.trace"
+  abbreviation successors where "successors \<equiv> dfa.successors TYPE('label)"
 
-  lemma product_simps[simp]:
-    "succ (product A B) a (p\<^sub>1, p\<^sub>2) = (succ A a p\<^sub>1, succ B a p\<^sub>2)"
-    "initial (product A B) = (initial A, initial B)"
-    "accepting (product A B) = accepting A \<times> accepting B"
-    unfolding product_def by simp+
+  global_interpretation intersection: automaton_intersection_path
+    dfa alphabet initial transition accepting "\<lambda> P w r p. P (last (p # r))"
+    dfa alphabet initial transition accepting "\<lambda> P w r p. P (last (p # r))"
+    dfa alphabet initial transition accepting "\<lambda> P w r p. P (last (p # r))"
+    "\<lambda> c\<^sub>1 c\<^sub>2 (p, q). c\<^sub>1 p \<and> c\<^sub>2 q"
+    defines intersect = intersection.combine
+    by (unfold_locales) (auto simp: zip_eq_Nil_iff)
 
-  lemma product_target[simp]: "target (product A B) r (p\<^sub>1, p\<^sub>2) = (target A r p\<^sub>1, target B r p\<^sub>2)"
-    by (induct r arbitrary: p\<^sub>1 p\<^sub>2) (auto)
+  global_interpretation union: automaton_union_path
+    dfa alphabet initial transition accepting "\<lambda> P w r p. P (last (p # r))"
+    dfa alphabet initial transition accepting "\<lambda> P w r p. P (last (p # r))"
+    dfa alphabet initial transition accepting "\<lambda> P w r p. P (last (p # r))"
+    "\<lambda> c\<^sub>1 c\<^sub>2 (p, q). c\<^sub>1 p \<or> c\<^sub>2 q"
+    defines union = union.combine
+    by (unfold_locales) (auto simp: zip_eq_Nil_iff)
 
-  lemma product_language[simp]: "language (product A B) = language A \<inter> language B" by force
+  global_interpretation complement: automaton_complement_path
+    dfa alphabet initial transition accepting "\<lambda> P w r p. P (last (p # r))"
+    dfa alphabet initial transition accepting "\<lambda> P w r p. P (last (p # r))"
+    "\<lambda> c p. \<not> c p"
+    defines complement = complement.complement
+    by unfold_locales auto
 
-end
+end
\ No newline at end of file
diff --git a/thys/Transition_Systems_and_Automata/Automata/NFA/NFA.thy b/thys/Transition_Systems_and_Automata/Automata/NFA/NFA.thy
--- a/thys/Transition_Systems_and_Automata/Automata/NFA/NFA.thy
+++ b/thys/Transition_Systems_and_Automata/Automata/NFA/NFA.thy
@@ -1,72 +1,42 @@
 section \<open>Nondeterministic Finite Automata\<close>
 
 theory NFA
-imports
-  "../../Basic/Sequence_Zip"
-  "../../Transition_Systems/Transition_System"
-  "../../Transition_Systems/Transition_System_Extra"
-  "../../Transition_Systems/Transition_System_Construction"
+imports "../Nondeterministic"
 begin
 
-  record ('label, 'state) nfa =
-    succ :: "'label \<Rightarrow> 'state \<Rightarrow> 'state set"
-    initial :: "'state set"
-    accepting :: "'state set"
-
-  global_interpretation nfa: transition_system_initial
-    "\<lambda> a p. snd a" "\<lambda> a p. snd a \<in> succ A (fst a) p" "\<lambda> p. p \<in> initial A"
-    for A
-    defines path = nfa.path and run = nfa.run and reachable = nfa.reachable and nodes = nfa.nodes
-    by this
-
-  abbreviation "target \<equiv> nfa.target"
-  abbreviation "states \<equiv> nfa.states"
-  abbreviation "trace \<equiv> nfa.trace"
-
-  abbreviation successors :: "('label, 'state, 'more) nfa_scheme \<Rightarrow> 'state \<Rightarrow> 'state set" where
-    "successors \<equiv> nfa.successors TYPE('label) TYPE('more)"
-
-  lemma states_alt_def: "states r p = map snd r" by (induct r arbitrary: p) (auto)
-  lemma trace_alt_def: "trace r p = smap snd r" by (coinduction arbitrary: r p) (auto)
-
-  definition language :: "('label, 'state) nfa \<Rightarrow> 'label list set" where
-    "language A \<equiv> {map fst r |r p. path A r p \<and> p \<in> initial A \<and> target r p \<in> accepting A}"
+  datatype ('label, 'state) nfa = nfa
+    (alphabet: "'label set")
+    (initial: "'state set")
+    (transition: "'label \<Rightarrow> 'state \<Rightarrow> 'state set")
+    (accepting: "'state pred")
 
-  lemma language[intro]:
-    assumes "path A (w || r) p" "p \<in> initial A" "target (w || r) p \<in> accepting A" "length w = length r"
-    shows "w \<in> language A"
-    using assms unfolding language_def by (force iff: split_zip_ex)
-  lemma language_elim[elim]:
-    assumes "w \<in> language A"
-    obtains r p
-    where "path A (w || r) p" "p \<in> initial A" "target (w || r) p \<in> accepting A" "length w = length r"
-    using assms unfolding language_def by (force iff: split_zip_ex)
-
-  definition product :: "('label, 'state\<^sub>1) nfa \<Rightarrow> ('label, 'state\<^sub>2) nfa \<Rightarrow>
-    ('label, 'state\<^sub>1 \<times> 'state\<^sub>2) nfa" where
-    "product A B \<equiv>
-    \<lparr>
-      succ = \<lambda> a (p\<^sub>1, p\<^sub>2). succ A a p\<^sub>1 \<times> succ B a p\<^sub>2,
-      initial = initial A \<times> initial B,
-      accepting = accepting A \<times> accepting B
-    \<rparr>"
+  global_interpretation nfa: automaton nfa alphabet initial transition accepting
+    defines path = nfa.path and run = nfa.run and reachable = nfa.reachable and nodes = nfa.nodes
+    by unfold_locales auto
+  global_interpretation nfa: automaton_path nfa alphabet initial transition accepting "\<lambda> P w r p. P (last (p # r))"
+    defines language = nfa.language
+    by standard
 
-  lemma product_simps[simp]:
-    "succ (product A B) a (p\<^sub>1, p\<^sub>2) = succ A a p\<^sub>1 \<times> succ B a p\<^sub>2"
-    "initial (product A B) = initial A \<times> initial B"
-    "accepting (product A B) = accepting A \<times> accepting B"
-    unfolding product_def by simp+
+  abbreviation target where "target \<equiv> nfa.target"
+  abbreviation states where "states \<equiv> nfa.states"
+  abbreviation trace where "trace \<equiv> nfa.trace"
+  abbreviation successors where "successors \<equiv> nfa.successors TYPE('label)"
 
-  lemma product_target[simp]:
-    assumes "length w = length r\<^sub>1" "length r\<^sub>1 = length r\<^sub>2"
-    shows "target (w || r\<^sub>1 || r\<^sub>2) (p\<^sub>1, p\<^sub>2) = (target (w || r\<^sub>1) p\<^sub>1, target (w || r\<^sub>2) p\<^sub>2)"
-    using assms by (induct arbitrary: p\<^sub>1 p\<^sub>2 rule: list_induct3) (auto)
-  lemma product_path[iff]:
-    assumes "length w = length r\<^sub>1" "length r\<^sub>1 = length r\<^sub>2"
-    shows "path (product A B) (w || r\<^sub>1 || r\<^sub>2) (p\<^sub>1, p\<^sub>2) \<longleftrightarrow> path A (w || r\<^sub>1) p\<^sub>1 \<and> path B (w || r\<^sub>2) p\<^sub>2"
-    using assms by (induct arbitrary: p\<^sub>1 p\<^sub>2 rule: list_induct3) (auto)
+  (* TODO: going from target to last requires states as intermediate step, used in other places too *)
+  global_interpretation nfa: automaton_intersection_path
+    nfa alphabet initial transition accepting "\<lambda> P w r p. P (last (p # r))"
+    nfa alphabet initial transition accepting "\<lambda> P w r p. P (last (p # r))"
+    nfa alphabet initial transition accepting "\<lambda> P w r p. P (last (p # r))"
+    "\<lambda> c\<^sub>1 c\<^sub>2 (p, q). c\<^sub>1 p \<and> c\<^sub>2 q"
+    defines intersect = nfa.intersect
+    by (unfold_locales) (auto simp: zip_eq_Nil_iff)
 
-  lemma product_language[simp]: "language (product A B) = language A \<inter> language B"
-    by (fastforce iff: split_zip)
+  global_interpretation nfa: automaton_union_path
+    nfa alphabet initial transition accepting "\<lambda> P w r p. P (last (p # r))"
+    nfa alphabet initial transition accepting "\<lambda> P w r p. P (last (p # r))"
+    nfa alphabet initial transition accepting "\<lambda> P w r p. P (last (p # r))"
+    case_sum
+    defines union = nfa.union
+    by (unfold_locales) (auto simp: last_map)
 
-end
+end
\ No newline at end of file