Theory DBA_Combine

```section ‹Deterministic Büchi Automata Combinations›

theory DBA_Combine
imports DBA DGBA
begin

global_interpretation degeneralization: automaton_degeneralization_run
dgba dgba.alphabet dgba.initial dgba.transition dgba.accepting "λ P w r p. gen infs P (p ## r)"
dba dba.alphabet dba.initial dba.transition dba.accepting "λ P w r p. infs P (p ## r)"
fst id
defines degeneralize = degeneralization.degeneralize
by (unfold_locales) (auto simp flip: sscan_smap)

lemmas degeneralize_language[simp] = degeneralization.degeneralize_language[folded DBA.language_def]
lemmas degeneralize_nodes_finite[iff] = degeneralization.degeneralize_nodes_finite[folded DBA.nodes_def]
lemmas degeneralize_nodes_card = degeneralization.degeneralize_nodes_card[folded DBA.nodes_def]

global_interpretation intersection: automaton_intersection_run
dba.dba dba.alphabet dba.initial dba.transition dba.accepting "λ P w r p. infs P (p ## r)"
dba.dba dba.alphabet dba.initial dba.transition dba.accepting "λ P w r p. infs P (p ## r)"
dgba.dgba dgba.alphabet dgba.initial dgba.transition dgba.accepting "λ P w r p. gen infs P (p ## r)"
"λ c⇩1 c⇩2. [c⇩1 ∘ fst, c⇩2 ∘ snd]"
defines intersect' = intersection.product
by unfold_locales auto

lemmas intersect'_language[simp] = intersection.product_language[folded DGBA.language_def]
lemmas intersect'_nodes_finite = intersection.product_nodes_finite[folded DGBA.nodes_def]
lemmas intersect'_nodes_card = intersection.product_nodes_card[folded DGBA.nodes_def]

global_interpretation union: automaton_union_run
dba.dba dba.alphabet dba.initial dba.transition dba.accepting "λ P w r p. infs P (p ## r)"
dba.dba dba.alphabet dba.initial dba.transition dba.accepting "λ P w r p. infs P (p ## r)"
dba.dba dba.alphabet dba.initial dba.transition dba.accepting "λ P w r p. infs P (p ## r)"
"λ c⇩1 c⇩2 pq. (c⇩1 ∘ fst) pq ∨ (c⇩2 ∘ snd) pq"
defines union = union.product
by (unfold_locales) (simp del: comp_apply)

lemmas union_language = union.product_language
lemmas union_nodes_finite = union.product_nodes_finite
lemmas union_nodes_card = union.product_nodes_card

global_interpretation intersection_list: automaton_intersection_list_run
dba.dba dba.alphabet dba.initial dba.transition dba.accepting "λ P w r p. infs P (p ## r)"
dgba.dgba dgba.alphabet dgba.initial dgba.transition dgba.accepting "λ P w r p. gen infs P (p ## r)"
"λ cs. map (λ k pp. (cs ! k) (pp ! k)) [0 ..< length cs]"
defines intersect_list' = intersection_list.product
by (unfold_locales) (auto simp: gen_def comp_def)

lemmas intersect_list'_language[simp] = intersection_list.product_language[folded DGBA.language_def]
lemmas intersect_list'_nodes_finite = intersection_list.product_nodes_finite[folded DGBA.nodes_def]
lemmas intersect_list'_nodes_card = intersection_list.product_nodes_card[folded DGBA.nodes_def]

global_interpretation union_list: automaton_union_list_run
dba.dba dba.alphabet dba.initial dba.transition dba.accepting "λ P w r p. infs P (p ## r)"
dba.dba dba.alphabet dba.initial dba.transition dba.accepting "λ P w r p. infs P (p ## r)"
"λ cs pp. ∃ k < length cs. (cs ! k) (pp ! k)"
defines union_list = union_list.product

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

(* TODO: these compound definitions are annoying, can we move those into Deterministic theory *)

abbreviation intersect where "intersect A B ≡ degeneralize (intersect' A B)"

lemma intersect_language[simp]: "DBA.language (intersect A B) = DBA.language A ∩ DBA.language B"
by simp
lemma intersect_nodes_finite:
assumes "finite (DBA.nodes A)" "finite (DBA.nodes B)"
shows "finite (DBA.nodes (intersect A B))"
using intersect'_nodes_finite assms by simp
lemma intersect_nodes_card:
assumes "finite (DBA.nodes A)" "finite (DBA.nodes B)"
shows "card (DBA.nodes (intersect A B)) ≤ 2 * card (DBA.nodes A) * card (DBA.nodes B)"
proof -
have "card (DBA.nodes (intersect A B)) ≤
max 1 (length (dgba.accepting (intersect' A B))) * card (DGBA.nodes (intersect' A B))"
using degeneralize_nodes_card by this
also have "length (dgba.accepting (intersect' A B)) = 2" by simp
also have "card (DGBA.nodes (intersect' A B)) ≤ card (DBA.nodes A) * card (DBA.nodes B)"
using intersect'_nodes_card assms by this
finally show ?thesis by simp
qed

abbreviation intersect_list where "intersect_list AA ≡ degeneralize (intersect_list' AA)"

lemma intersect_list_language[simp]: "DBA.language (intersect_list AA) = ⋂ (DBA.language ` set AA)"
by simp
lemma intersect_list_nodes_finite:
assumes "list_all (finite ∘ DBA.nodes) AA"
shows "finite (DBA.nodes (intersect_list AA))"
using intersect_list'_nodes_finite assms by simp
lemma intersect_list_nodes_card:
assumes "list_all (finite ∘ DBA.nodes) AA"
shows "card (DBA.nodes (intersect_list AA)) ≤ max 1 (length AA) * prod_list (map (card ∘ DBA.nodes) AA)"
proof -
have "card (DBA.nodes (intersect_list AA)) ≤
max 1 (length (dgba.accepting (intersect_list' AA))) * card (DGBA.nodes (intersect_list' AA))"
using degeneralize_nodes_card by this
also have "length (dgba.accepting (intersect_list' AA)) = length AA" by simp
also have "card (DGBA.nodes (intersect_list' AA)) ≤ prod_list (map (card ∘ DBA.nodes) AA)"
using intersect_list'_nodes_card assms by this
finally show ?thesis by simp
qed

end```