# Theory DRA_Combine

```section ‹Deterministic Rabin Automata Combinations›

theory DRA_Combine
imports "DRA" "../DBA/DBA" "../DCA/DCA"
begin

global_interpretation intersection_bc: automaton_intersection_run
dba.dba dba.alphabet dba.initial dba.transition dba.accepting "λ P w r p. infs P (p ## r)"
dca.dca dca.alphabet dca.initial dca.transition dca.rejecting "λ P w r p. fins P (p ## r)"
dra.dra dra.alphabet dra.initial dra.transition dra.condition "λ P w r p. cogen rabin P (p ## r)"
"λ c⇩1 c⇩2. [(c⇩1 ∘ fst, c⇩2 ∘ snd)]"
defines intersect_bc = intersection_bc.product
by (unfold_locales) (simp add: cogen_def rabin_def)

(* TODO: why are only the constants of the first interpretation folded back correctly? *)
lemmas intersect_bc_language[simp] = intersection_bc.product_language[folded DCA.language_def DRA.language_def]
lemmas intersect_bc_nodes_finite = intersection_bc.product_nodes_finite[folded DCA.nodes_def DRA.nodes_def]
lemmas intersect_bc_nodes_card = intersection_bc.product_nodes_card[folded DCA.nodes_def DRA.nodes_def]

(* TODO: are there some statements about the rabin constant hidden in here?
same for gen/cogen, also in other combinations, shouldn't have to unfold those *)
global_interpretation union_list: automaton_union_list_run
dra.dra dra.alphabet dra.initial dra.transition dra.condition "λ P w r p. cogen rabin P (p ## r)"
dra.dra dra.alphabet dra.initial dra.transition dra.condition "λ P w r p. cogen rabin P (p ## r)"
"λ cs. do { k ← [0 ..< length cs]; (f, g) ← cs ! k; [(λ pp. f (pp ! k), λ pp. g (pp ! k))] }"
defines union_list = union_list.product
by (unfold_locales) (auto simp: cogen_def rabin_def comp_def split_beta)

lemmas union_list_language = union_list.product_language
lemmas union_list_nodes_finite = union_list.product_nodes_finite
lemmas union_list_nodes_card = union_list.product_nodes_card

end```