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