# Theory Deterministic

```section ‹Deterministic Automata›

theory Deterministic
imports
"../Transition_Systems/Transition_System"
"../Transition_Systems/Transition_System_Extra"
"../Transition_Systems/Transition_System_Construction"
"../Basic/Degeneralization"
begin

locale automaton =
fixes automaton :: "'label set ⇒ 'state ⇒ ('label ⇒ 'state ⇒ 'state) ⇒ 'condition ⇒ 'automaton"
fixes alphabet initial transition condition
assumes automaton[simp]: "automaton (alphabet A) (initial A) (transition A) (condition A) = A"
assumes alphabet[simp]: "alphabet (automaton a i t c) = a"
assumes initial[simp]: "initial (automaton a i t c) = i"
assumes transition[simp]: "transition (automaton a i t c) = t"
assumes condition[simp]: "condition (automaton a i t c) = c"
begin

(* TODO: is there a way to use defines without renaming the constants? *)
sublocale transition_system_initial
"transition A" "λ a p. a ∈ alphabet A" "λ p. p = initial A"
for A
defines path' = path and run' = run and reachable' = reachable and nodes' = nodes
by this

lemma path_alt_def: "path A w p ⟷ w ∈ lists (alphabet A)"
proof
show "w ∈ lists (alphabet A)" if "path A w p" using that by (induct arbitrary: p) (auto)
show "path A w p" if "w ∈ lists (alphabet A)" using that by (induct arbitrary: p) (auto)
qed
lemma run_alt_def: "run A w p ⟷ w ∈ streams (alphabet A)"
proof
show "w ∈ streams (alphabet A)" if "run A w p"
using that by (coinduction arbitrary: w p) (force elim: run.cases)
show "run A w p" if "w ∈ streams (alphabet A)"
using that by (coinduction arbitrary: w p) (force elim: streams.cases)
qed

end

locale automaton_path =
automaton automaton alphabet initial transition condition
for automaton :: "'label set ⇒ 'state ⇒ ('label ⇒ 'state ⇒ 'state) ⇒ 'condition ⇒ 'automaton"
and alphabet initial transition condition
+
fixes test :: "'condition ⇒ 'label list ⇒ 'state list ⇒ 'state ⇒ bool"
begin

definition language :: "'automaton ⇒ 'label list set" where
"language A ≡ {w. path A w (initial A) ∧ test (condition A) w (states A w (initial A)) (initial A)}"

lemma language[intro]:
assumes "path A w (initial A)" "test (condition A) w (states A w (initial A)) (initial A)"
shows "w ∈ language A"
using assms unfolding language_def by auto
lemma language_elim[elim]:
assumes "w ∈ language A"
obtains "path A w (initial A)" "test (condition A) w (states A w (initial A)) (initial A)"
using assms unfolding language_def by auto

lemma language_alphabet: "language A ⊆ lists (alphabet A)" using path_alt_def by auto

end

locale automaton_run =
automaton automaton alphabet initial transition condition
for automaton :: "'label set ⇒ 'state ⇒ ('label ⇒ 'state ⇒ 'state) ⇒ 'condition ⇒ 'automaton"
and alphabet initial transition condition
+
fixes test :: "'condition ⇒ 'label stream ⇒ 'state stream ⇒ 'state ⇒ bool"
begin

definition language :: "'automaton ⇒ 'label stream set" where
"language A ≡ {w. run A w (initial A) ∧ test (condition A) w (trace A w (initial A)) (initial A)}"

lemma language[intro]:
assumes "run A w (initial A)" "test (condition A) w (trace A w (initial A)) (initial A)"
shows "w ∈ language A"
using assms unfolding language_def by auto
lemma language_elim[elim]:
assumes "w ∈ language A"
obtains "run A w (initial A)" "test (condition A) w (trace A w (initial A)) (initial A)"
using assms unfolding language_def by auto

lemma language_alphabet: "language A ⊆ streams (alphabet A)" using run_alt_def by auto

end

locale automaton_degeneralization =
a: automaton automaton⇩1 alphabet⇩1 initial⇩1 transition⇩1 condition⇩1 +
b: automaton automaton⇩2 alphabet⇩2 initial⇩2 transition⇩2 condition⇩2
for automaton⇩1 :: "'label set ⇒ 'state ⇒ ('label ⇒ 'state ⇒ 'state) ⇒ 'item pred gen ⇒ 'automaton⇩1"
and alphabet⇩1 initial⇩1 transition⇩1 condition⇩1
and automaton⇩2 :: "'label set ⇒ 'state degen ⇒ ('label ⇒ 'state degen ⇒ 'state degen) ⇒ 'item_degen pred ⇒ 'automaton⇩2"
and alphabet⇩2 initial⇩2 transition⇩2 condition⇩2
+
fixes item :: "'state × 'label × 'state ⇒ 'item"
fixes translate :: "'item_degen ⇒ 'item degen"
begin

definition degeneralize :: "'automaton⇩1 ⇒ 'automaton⇩2" where
"degeneralize A ≡ automaton⇩2
(alphabet⇩1 A)
(initial⇩1 A, 0)
(λ a (p, k). (transition⇩1 A a p, count (condition⇩1 A) (item (p, a, transition⇩1 A a p)) k))
(degen (condition⇩1 A) ∘ translate)"

lemma degeneralize_simps[simp]:
"alphabet⇩2 (degeneralize A) = alphabet⇩1 A"
"initial⇩2 (degeneralize A) = (initial⇩1 A, 0)"
"transition⇩2 (degeneralize A) a (p, k) =
(transition⇩1 A a p, count (condition⇩1 A) (item (p, a, transition⇩1 A a p)) k)"
"condition⇩2 (degeneralize A) = degen (condition⇩1 A) ∘ translate"
unfolding degeneralize_def by auto

lemma degeneralize_target[simp]: "b.target (degeneralize A) w (p, k) =
(a.target A w p, fold (count (condition⇩1 A) ∘ item) (p # a.states A w p || w || a.states A w p) k)"
by (induct w arbitrary: p k) (auto)
lemma degeneralize_states[simp]: "b.states (degeneralize A) w (p, k) =
a.states A w p || scan (count (condition⇩1 A) ∘ item) (p # a.states A w p || w || a.states A w p) k"
by (induct w arbitrary: p k) (auto)
lemma degeneralize_trace[simp]: "b.trace (degeneralize A) w (p, k) =
a.trace A w p ||| sscan (count (condition⇩1 A) ∘ item) (p ## a.trace A w p ||| w ||| a.trace A w p) k"
by (coinduction arbitrary: w p k) (auto, metis sscan.code)

lemma degeneralize_path[iff]: "b.path (degeneralize A) w (p, k) ⟷ a.path A w p"
unfolding a.path_alt_def b.path_alt_def by simp
lemma degeneralize_run[iff]: "b.run (degeneralize A) w (p, k) ⟷ a.run A w p"
unfolding a.run_alt_def b.run_alt_def by simp

lemma degeneralize_reachable_fst[simp]: "fst ` b.reachable (degeneralize A) (p, k) = a.reachable A p"
unfolding a.reachable_alt_def b.reachable_alt_def image_def by simp
lemma degeneralize_reachable_snd_empty[simp]:
assumes "condition⇩1 A = []"
shows "snd ` b.reachable (degeneralize A) (p, k) = {k}"
proof -
have "snd ql = k" if "ql ∈ b.reachable (degeneralize A) (p, k)" for ql
using that assms by induct auto
then show ?thesis by auto
qed
lemma degeneralize_reachable_empty[simp]:
assumes "condition⇩1 A = []"
shows "b.reachable (degeneralize A) (p, k) = a.reachable A p × {k}"
using degeneralize_reachable_fst degeneralize_reachable_snd_empty assms
by (metis prod_singleton(2))
lemma degeneralize_reachable_snd:
"snd ` b.reachable (degeneralize A) (p, k) ⊆ insert k {0 ..< length (condition⇩1 A)}"
by (cases "condition⇩1 A = []") (auto)
lemma degeneralize_reachable:
"b.reachable (degeneralize A) (p, k) ⊆ a.reachable A p × insert k {0 ..< length (condition⇩1 A)}"
by (cases "condition⇩1 A = []") (auto 0 3)

lemma degeneralize_nodes_fst[simp]: "fst ` b.nodes (degeneralize A) = a.nodes A"
unfolding a.nodes_alt_def b.nodes_alt_def by simp
lemma degeneralize_nodes_snd_empty:
assumes "condition⇩1 A = []"
shows "snd ` b.nodes (degeneralize A) = {0}"
using assms unfolding b.nodes_alt_def by auto
lemma degeneralize_nodes_empty:
assumes "condition⇩1 A = []"
shows "b.nodes (degeneralize A) = a.nodes A × {0}"
using assms unfolding b.nodes_alt_def by auto
lemma degeneralize_nodes_snd:
"snd ` b.nodes (degeneralize A) ⊆ insert 0 {0 ..< length (condition⇩1 A)}"
using degeneralize_reachable_snd unfolding b.nodes_alt_def by auto
lemma degeneralize_nodes:
"b.nodes (degeneralize A) ⊆ a.nodes A × insert 0 {0 ..< length (condition⇩1 A)}"
using degeneralize_reachable unfolding a.nodes_alt_def b.nodes_alt_def by simp

lemma degeneralize_nodes_finite[iff]: "finite (b.nodes (degeneralize A)) ⟷ finite (a.nodes A)"
proof
show "finite (a.nodes A)" if "finite (b.nodes (degeneralize A))"
using that by (auto simp flip: degeneralize_nodes_fst)
show "finite (b.nodes (degeneralize A))" if "finite (a.nodes A)"
using finite_subset degeneralize_nodes that by blast
qed
lemma degeneralize_nodes_card: "card (b.nodes (degeneralize A)) ≤
max 1 (length (condition⇩1 A)) * card (a.nodes A)"
proof (cases "finite (a.nodes A)")
case True
have "card (b.nodes (degeneralize A)) ≤ card (a.nodes A × insert 0 {0 ..< length (condition⇩1 A)})"
using degeneralize_nodes True by (blast intro: card_mono)
also have "… = card (insert 0 {0 ..< length (condition⇩1 A)}) * card (a.nodes A)"
unfolding card_cartesian_product by simp
also have "card (insert 0 {0 ..< length (condition⇩1 A)}) = max 1 (length (condition⇩1 A))"
by (simp add: card_insert_if Suc_leI max_absorb2)
finally show ?thesis by this
next
case False
then have "card (a.nodes A) = 0" "card (b.nodes (degeneralize A)) = 0" by auto
then show ?thesis by simp
qed

end

locale automaton_degeneralization_run =
automaton_degeneralization
automaton⇩1 alphabet⇩1 initial⇩1 transition⇩1 condition⇩1
automaton⇩2 alphabet⇩2 initial⇩2 transition⇩2 condition⇩2
item translate +
a: automaton_run automaton⇩1 alphabet⇩1 initial⇩1 transition⇩1 condition⇩1 test⇩1 +
b: automaton_run automaton⇩2 alphabet⇩2 initial⇩2 transition⇩2 condition⇩2 test⇩2
for automaton⇩1 alphabet⇩1 initial⇩1 transition⇩1 condition⇩1 test⇩1
and automaton⇩2 alphabet⇩2 initial⇩2 transition⇩2 condition⇩2 test⇩2
and item translate
+
assumes test[iff]: "test⇩2 (degen cs ∘ translate) w
(r ||| sscan (count cs ∘ item) (p ## r ||| w ||| r) k) (p, k) ⟷ test⇩1 cs w r p"
begin

lemma degeneralize_language[simp]: "b.language (degeneralize A) = a.language A" by force

end

locale automaton_product =
a: automaton automaton⇩1 alphabet⇩1 initial⇩1 transition⇩1 condition⇩1 +
b: automaton automaton⇩2 alphabet⇩2 initial⇩2 transition⇩2 condition⇩2 +
c: automaton automaton⇩3 alphabet⇩3 initial⇩3 transition⇩3 condition⇩3
for automaton⇩1 :: "'label set ⇒ 'state⇩1 ⇒ ('label ⇒ 'state⇩1 ⇒ 'state⇩1) ⇒ 'condition⇩1 ⇒ 'automaton⇩1"
and alphabet⇩1 initial⇩1 transition⇩1 condition⇩1
and automaton⇩2 :: "'label set ⇒ 'state⇩2 ⇒ ('label ⇒ 'state⇩2 ⇒ 'state⇩2) ⇒ 'condition⇩2 ⇒ 'automaton⇩2"
and alphabet⇩2 initial⇩2 transition⇩2 condition⇩2
and automaton⇩3 :: "'label set ⇒ 'state⇩1 × 'state⇩2 ⇒ ('label ⇒ 'state⇩1 × 'state⇩2 ⇒ 'state⇩1 × 'state⇩2) ⇒ 'condition⇩3 ⇒ 'automaton⇩3"
and alphabet⇩3 initial⇩3 transition⇩3 condition⇩3
+
fixes condition :: "'condition⇩1 ⇒ 'condition⇩2 ⇒ 'condition⇩3"
begin

definition product :: "'automaton⇩1 ⇒ 'automaton⇩2 ⇒ 'automaton⇩3" where
"product A B ≡ automaton⇩3
(alphabet⇩1 A ∩ alphabet⇩2 B)
(initial⇩1 A, initial⇩2 B)
(λ a (p, q). (transition⇩1 A a p, transition⇩2 B a q))
(condition (condition⇩1 A) (condition⇩2 B))"

lemma product_simps[simp]:
"alphabet⇩3 (product A B) = alphabet⇩1 A ∩ alphabet⇩2 B"
"initial⇩3 (product A B) = (initial⇩1 A, initial⇩2 B)"
"transition⇩3 (product A B) a (p, q) = (transition⇩1 A a p, transition⇩2 B a q)"
"condition⇩3 (product A B) = condition (condition⇩1 A) (condition⇩2 B)"
unfolding product_def by auto

lemma product_target[simp]: "c.target (product A B) w (p, q) = (a.target A w p, b.target B w q)"
by (induct w arbitrary: p q) (auto)
lemma product_states[simp]: "c.states (product A B) w (p, q) = a.states A w p || b.states B w q"
by (induct w arbitrary: p q) (auto)
lemma product_trace[simp]: "c.trace (product A B) w (p, q) = a.trace A w p ||| b.trace B w q"
by (coinduction arbitrary: w p q) (auto)

lemma product_path[iff]: "c.path (product A B) w (p, q) ⟷ a.path A w p ∧ b.path B w q"
unfolding a.path_alt_def b.path_alt_def c.path_alt_def by simp
lemma product_run[iff]: "c.run (product A B) w (p, q) ⟷ a.run A w p ∧ b.run B w q"
unfolding a.run_alt_def b.run_alt_def c.run_alt_def by simp

lemma product_reachable[simp]: "c.reachable (product A B) (p, q) ⊆ a.reachable A p × b.reachable B q"
unfolding c.reachable_alt_def by auto
lemma product_nodes[simp]: "c.nodes (product A B) ⊆ a.nodes A × b.nodes B"
unfolding a.nodes_alt_def b.nodes_alt_def c.nodes_alt_def by auto
lemma product_reachable_fst[simp]:
assumes "alphabet⇩1 A ⊆ alphabet⇩2 B"
shows "fst ` c.reachable (product A B) (p, q) = a.reachable A p"
using assms
unfolding a.reachable_alt_def a.path_alt_def
unfolding b.reachable_alt_def b.path_alt_def
unfolding c.reachable_alt_def c.path_alt_def
by auto force
lemma product_reachable_snd[simp]:
assumes "alphabet⇩1 A ⊇ alphabet⇩2 B"
shows "snd ` c.reachable (product A B) (p, q) = b.reachable B q"
using assms
unfolding a.reachable_alt_def a.path_alt_def
unfolding b.reachable_alt_def b.path_alt_def
unfolding c.reachable_alt_def c.path_alt_def
by auto force
lemma product_nodes_fst[simp]:
assumes "alphabet⇩1 A ⊆ alphabet⇩2 B"
shows "fst ` c.nodes (product A B) = a.nodes A"
using assms product_reachable_fst
unfolding a.nodes_alt_def b.nodes_alt_def c.nodes_alt_def
by fastforce
lemma product_nodes_snd[simp]:
assumes "alphabet⇩1 A ⊇ alphabet⇩2 B"
shows "snd ` c.nodes (product A B) = b.nodes B"
using assms product_reachable_snd
unfolding a.nodes_alt_def b.nodes_alt_def c.nodes_alt_def
by fastforce

lemma product_nodes_finite[intro]:
assumes "finite (a.nodes A)" "finite (b.nodes B)"
shows "finite (c.nodes (product A B))"
proof (rule finite_subset)
show "c.nodes (product A B) ⊆ a.nodes A × b.nodes B" using product_nodes by this
show "finite (a.nodes A × b.nodes B)" using assms by simp
qed
lemma product_nodes_finite_strong[iff]:
assumes "alphabet⇩1 A = alphabet⇩2 B"
shows "finite (c.nodes (product A B)) ⟷ finite (a.nodes A) ∧ finite (b.nodes B)"
proof safe
show "finite (a.nodes A)" if "finite (c.nodes (product A B))"
using product_nodes_fst assms that by (metis finite_imageI equalityD1)
show "finite (b.nodes B)" if "finite (c.nodes (product A B))"
using product_nodes_snd assms that by (metis finite_imageI equalityD2)
show "finite (c.nodes (product A B))" if "finite (a.nodes A)" "finite (b.nodes B)"
using that by rule
qed
lemma product_nodes_card[intro]:
assumes "finite (a.nodes A)" "finite (b.nodes B)"
shows "card (c.nodes (product A B)) ≤ card (a.nodes A) * card (b.nodes B)"
proof -
have "card (c.nodes (product A B)) ≤ card (a.nodes A × b.nodes B)"
proof (rule card_mono)
show "finite (a.nodes A × b.nodes B)" using assms by simp
show "c.nodes (product A B) ⊆ a.nodes A × b.nodes B" using product_nodes by this
qed
also have "… = card (a.nodes A) * card (b.nodes B)" using card_cartesian_product by this
finally show ?thesis by this
qed
lemma product_nodes_card_strong[intro]:
assumes "alphabet⇩1 A = alphabet⇩2 B"
shows "card (c.nodes (product A B)) ≤ card (a.nodes A) * card (b.nodes B)"
proof (cases "finite (a.nodes A) ∧ finite (b.nodes B)")
case True
show ?thesis using True by auto
next
case False
have 1: "card (c.nodes (product A B)) = 0" using False assms by simp
have 2: "card (a.nodes A) * card (b.nodes B) = 0" using False by auto
show ?thesis using 1 2 by simp
qed

end

locale automaton_intersection_path =
automaton_product
automaton⇩1 alphabet⇩1 initial⇩1 transition⇩1 condition⇩1
automaton⇩2 alphabet⇩2 initial⇩2 transition⇩2 condition⇩2
automaton⇩3 alphabet⇩3 initial⇩3 transition⇩3 condition⇩3
condition +
a: automaton_path automaton⇩1 alphabet⇩1 initial⇩1 transition⇩1 condition⇩1 test⇩1 +
b: automaton_path automaton⇩2 alphabet⇩2 initial⇩2 transition⇩2 condition⇩2 test⇩2 +
c: automaton_path automaton⇩3 alphabet⇩3 initial⇩3 transition⇩3 condition⇩3 test⇩3
for automaton⇩1 alphabet⇩1 initial⇩1 transition⇩1 condition⇩1 test⇩1
and automaton⇩2 alphabet⇩2 initial⇩2 transition⇩2 condition⇩2 test⇩2
and automaton⇩3 alphabet⇩3 initial⇩3 transition⇩3 condition⇩3 test⇩3
and condition
+
assumes test[iff]: "length r = length s ⟹
test⇩3 (condition c⇩1 c⇩2) w (r || s) (p, q) ⟷ test⇩1 c⇩1 w r p ∧ test⇩2 c⇩2 w s q"
begin

lemma product_language[simp]: "c.language (product A B) = a.language A ∩ b.language B" by force

end

locale automaton_union_path =
automaton_product
automaton⇩1 alphabet⇩1 initial⇩1 transition⇩1 condition⇩1
automaton⇩2 alphabet⇩2 initial⇩2 transition⇩2 condition⇩2
automaton⇩3 alphabet⇩3 initial⇩3 transition⇩3 condition⇩3
condition +
a: automaton_path automaton⇩1 alphabet⇩1 initial⇩1 transition⇩1 condition⇩1 test⇩1 +
b: automaton_path automaton⇩2 alphabet⇩2 initial⇩2 transition⇩2 condition⇩2 test⇩2 +
c: automaton_path automaton⇩3 alphabet⇩3 initial⇩3 transition⇩3 condition⇩3 test⇩3
for automaton⇩1 alphabet⇩1 initial⇩1 transition⇩1 condition⇩1 test⇩1
and automaton⇩2 alphabet⇩2 initial⇩2 transition⇩2 condition⇩2 test⇩2
and automaton⇩3 alphabet⇩3 initial⇩3 transition⇩3 condition⇩3 test⇩3
and condition
+
assumes test[iff]: "length r = length s ⟹
test⇩3 (condition c⇩1 c⇩2) w (r || s) (p, q) ⟷ test⇩1 c⇩1 w r p ∨ test⇩2 c⇩2 w s q"
begin

lemma product_language[simp]:
assumes "alphabet⇩1 A = alphabet⇩2 B"
shows "c.language (product A B) = a.language A ∪ b.language B"
using assms by (force simp: a.path_alt_def b.path_alt_def)

end

locale automaton_intersection_run =
automaton_product
automaton⇩1 alphabet⇩1 initial⇩1 transition⇩1 condition⇩1
automaton⇩2 alphabet⇩2 initial⇩2 transition⇩2 condition⇩2
automaton⇩3 alphabet⇩3 initial⇩3 transition⇩3 condition⇩3
condition +
a: automaton_run automaton⇩1 alphabet⇩1 initial⇩1 transition⇩1 condition⇩1 test⇩1 +
b: automaton_run automaton⇩2 alphabet⇩2 initial⇩2 transition⇩2 condition⇩2 test⇩2 +
c: automaton_run automaton⇩3 alphabet⇩3 initial⇩3 transition⇩3 condition⇩3 test⇩3
for automaton⇩1 alphabet⇩1 initial⇩1 transition⇩1 condition⇩1 test⇩1
and automaton⇩2 alphabet⇩2 initial⇩2 transition⇩2 condition⇩2 test⇩2
and automaton⇩3 alphabet⇩3 initial⇩3 transition⇩3 condition⇩3 test⇩3
and condition
+
assumes test[iff]: "test⇩3 (condition c⇩1 c⇩2) w (r ||| s) (p, q) ⟷ test⇩1 c⇩1 w r p ∧ test⇩2 c⇩2 w s q"
begin

lemma product_language[simp]: "c.language (product A B) = a.language A ∩ b.language B" by force

end

locale automaton_union_run =
automaton_product
automaton⇩1 alphabet⇩1 initial⇩1 transition⇩1 condition⇩1
automaton⇩2 alphabet⇩2 initial⇩2 transition⇩2 condition⇩2
automaton⇩3 alphabet⇩3 initial⇩3 transition⇩3 condition⇩3
condition +
a: automaton_run automaton⇩1 alphabet⇩1 initial⇩1 transition⇩1 condition⇩1 test⇩1 +
b: automaton_run automaton⇩2 alphabet⇩2 initial⇩2 transition⇩2 condition⇩2 test⇩2 +
c: automaton_run automaton⇩3 alphabet⇩3 initial⇩3 transition⇩3 condition⇩3 test⇩3
for automaton⇩1 alphabet⇩1 initial⇩1 transition⇩1 condition⇩1 test⇩1
and automaton⇩2 alphabet⇩2 initial⇩2 transition⇩2 condition⇩2 test⇩2
and automaton⇩3 alphabet⇩3 initial⇩3 transition⇩3 condition⇩3 test⇩3
and condition
+
assumes test[iff]: "test⇩3 (condition c⇩1 c⇩2) w (r ||| s) (p, q) ⟷ test⇩1 c⇩1 w r p ∨ test⇩2 c⇩2 w s q"
begin

lemma product_language[simp]:
assumes "alphabet⇩1 A = alphabet⇩2 B"
shows "c.language (product A B) = a.language A ∪ b.language B"
using assms by (force simp: a.run_alt_def b.run_alt_def)

end

(* TODO: complete this in analogy to the pair case *)
locale automaton_product_list =
a: automaton automaton⇩1 alphabet⇩1 initial⇩1 transition⇩1 condition⇩1 +
b: automaton automaton⇩2 alphabet⇩2 initial⇩2 transition⇩2 condition⇩2
for automaton⇩1 :: "'label set ⇒ 'state ⇒ ('label ⇒ 'state ⇒ 'state) ⇒ 'condition⇩1 ⇒ 'automaton⇩1"
and alphabet⇩1 initial⇩1 transition⇩1 condition⇩1
and automaton⇩2 :: "'label set ⇒ 'state list ⇒ ('label ⇒ 'state list ⇒ 'state list) ⇒ 'condition⇩2 ⇒ 'automaton⇩2"
and alphabet⇩2 initial⇩2 transition⇩2 condition⇩2
+
fixes condition :: "'condition⇩1 list ⇒ 'condition⇩2"
begin

definition product :: "'automaton⇩1 list ⇒ 'automaton⇩2" where
"product AA ≡ automaton⇩2
(⋂ (alphabet⇩1 ` set AA))
(map initial⇩1 AA)
(λ a ps. map2 (λ A p. transition⇩1 A a p) AA ps)
(condition (map condition⇩1 AA))"

lemma product_simps[simp]:
"alphabet⇩2 (product AA) = ⋂ (alphabet⇩1 ` set AA)"
"initial⇩2 (product AA) = map initial⇩1 AA"
"transition⇩2 (product AA) a ps = map2 (λ A p. transition⇩1 A a p) AA ps"
"condition⇩2 (product AA) = condition (map condition⇩1 AA)"
unfolding product_def by auto

(* TODO: get rid of indices, express this using stranspose and listset *)
lemma product_trace_smap:
assumes "length ps = length AA" "k < length AA"
shows "smap (λ ps. ps ! k) (b.trace (product AA) w ps) = a.trace (AA ! k) w (ps ! k)"
using assms by (coinduction arbitrary: w ps) (force)

lemma product_nodes: "b.nodes (product AA) ⊆ listset (map a.nodes AA)"
proof
show "ps ∈ listset (map a.nodes AA)" if "ps ∈ b.nodes (product AA)" for ps
using that by (induct) (auto simp: listset_member list_all2_conv_all_nth)
qed

lemma product_nodes_finite[intro]:
assumes "list_all (finite ∘ a.nodes) AA"
shows "finite (b.nodes (product AA))"
using list.pred_map product_nodes assms by (blast dest: finite_subset)
lemma product_nodes_card:
assumes "list_all (finite ∘ a.nodes) AA"
shows "card (b.nodes (product AA)) ≤ prod_list (map (card ∘ a.nodes) AA)"
proof -
have "card (b.nodes (product AA)) ≤ card (listset (map a.nodes AA))"
using list.pred_map product_nodes assms by (blast intro: card_mono)
also have "… = prod_list (map (card ∘ a.nodes) AA)" by simp
finally show ?thesis by this
qed

end

locale automaton_intersection_list_run =
automaton_product_list
automaton⇩1 alphabet⇩1 initial⇩1 transition⇩1 condition⇩1
automaton⇩2 alphabet⇩2 initial⇩2 transition⇩2 condition⇩2
condition +
a: automaton_run automaton⇩1 alphabet⇩1 initial⇩1 transition⇩1 condition⇩1 test⇩1 +
b: automaton_run automaton⇩2 alphabet⇩2 initial⇩2 transition⇩2 condition⇩2 test⇩2
for automaton⇩1 alphabet⇩1 initial⇩1 transition⇩1 condition⇩1 test⇩1
and automaton⇩2 alphabet⇩2 initial⇩2 transition⇩2 condition⇩2 test⇩2
and condition
+
assumes test[iff]: "test⇩2 (condition cs) w rs ps ⟷
(∀ k < length cs. test⇩1 (cs ! k) w (smap (λ ps. ps ! k) rs) (ps ! k))"
begin

lemma product_language[simp]: "b.language (product AA) = ⋂ (a.language ` set AA)"
unfolding a.language_def b.language_def
unfolding a.run_alt_def b.run_alt_def streams_iff_sset
by (fastforce simp: set_conv_nth product_trace_smap)

end

locale automaton_union_list_run =
automaton_product_list
automaton⇩1 alphabet⇩1 initial⇩1 transition⇩1 condition⇩1
automaton⇩2 alphabet⇩2 initial⇩2 transition⇩2 condition⇩2
condition +
a: automaton_run automaton⇩1 alphabet⇩1 initial⇩1 transition⇩1 condition⇩1 test⇩1 +
b: automaton_run automaton⇩2 alphabet⇩2 initial⇩2 transition⇩2 condition⇩2 test⇩2
for automaton⇩1 alphabet⇩1 initial⇩1 transition⇩1 condition⇩1 test⇩1
and automaton⇩2 alphabet⇩2 initial⇩2 transition⇩2 condition⇩2 test⇩2
and condition
+
assumes test[iff]: "test⇩2 (condition cs) w rs ps ⟷
(∃ k < length cs. test⇩1 (cs ! k) w (smap (λ ps. ps ! k) rs) (ps ! k))"
begin

lemma product_language[simp]:
assumes "⋂ (alphabet⇩1 ` set AA) = ⋃ (alphabet⇩1 ` set AA)"
shows "b.language (product AA) = ⋃ (a.language ` set AA)"
using assms
unfolding a.language_def b.language_def
unfolding a.run_alt_def b.run_alt_def streams_iff_sset
by (fastforce simp: set_conv_nth product_trace_smap)

end

locale automaton_complement =
a: automaton automaton⇩1 alphabet⇩1 initial⇩1 transition⇩1 condition⇩1 +
b: automaton automaton⇩2 alphabet⇩2 initial⇩2 transition⇩2 condition⇩2
for automaton⇩1 :: "'label set ⇒ 'state ⇒ ('label ⇒ 'state ⇒ 'state) ⇒ 'condition⇩1 ⇒ 'automaton⇩1"
and alphabet⇩1 initial⇩1 transition⇩1 condition⇩1
and automaton⇩2 :: "'label set ⇒ 'state ⇒ ('label ⇒ 'state ⇒ 'state) ⇒ 'condition⇩2 ⇒ 'automaton⇩2"
and alphabet⇩2 initial⇩2 transition⇩2 condition⇩2
+
fixes condition :: "'condition⇩1 ⇒ 'condition⇩2"
begin

definition complement :: "'automaton⇩1 ⇒ 'automaton⇩2" where
"complement A ≡ automaton⇩2 (alphabet⇩1 A) (initial⇩1 A) (transition⇩1 A) (condition (condition⇩1 A))"

lemma combine_simps[simp]:
"alphabet⇩2 (complement A) = alphabet⇩1 A"
"initial⇩2 (complement A) = initial⇩1 A"
"transition⇩2 (complement A) = transition⇩1 A"
"condition⇩2 (complement A) = condition (condition⇩1 A)"
unfolding complement_def by auto

end

locale automaton_complement_path =
automaton_complement
automaton⇩1 alphabet⇩1 initial⇩1 transition⇩1 condition⇩1
automaton⇩2 alphabet⇩2 initial⇩2 transition⇩2 condition⇩2
condition +
a: automaton_path automaton⇩1 alphabet⇩1 initial⇩1 transition⇩1 condition⇩1 test⇩1 +
b: automaton_path automaton⇩2 alphabet⇩2 initial⇩2 transition⇩2 condition⇩2 test⇩2
for automaton⇩1 alphabet⇩1 initial⇩1 transition⇩1 condition⇩1 test⇩1
and automaton⇩2 alphabet⇩2 initial⇩2 transition⇩2 condition⇩2 test⇩2
and condition
+
assumes test[iff]: "test⇩2 (condition c) w r p ⟷ ¬ test⇩1 c w r p"
begin

lemma complement_language[simp]: "b.language (complement A) = lists (alphabet⇩1 A) - a.language A"
unfolding a.language_def b.language_def a.path_alt_def b.path_alt_def by auto

end

locale automaton_complement_run =
automaton_complement
automaton⇩1 alphabet⇩1 initial⇩1 transition⇩1 condition⇩1
automaton⇩2 alphabet⇩2 initial⇩2 transition⇩2 condition⇩2
condition +
a: automaton_run automaton⇩1 alphabet⇩1 initial⇩1 transition⇩1 condition⇩1 test⇩1 +
b: automaton_run automaton⇩2 alphabet⇩2 initial⇩2 transition⇩2 condition⇩2 test⇩2
for automaton⇩1 alphabet⇩1 initial⇩1 transition⇩1 condition⇩1 test⇩1
and automaton⇩2 alphabet⇩2 initial⇩2 transition⇩2 condition⇩2 test⇩2
and condition
+
assumes test[iff]: "test⇩2 (condition c) w r p ⟷ ¬ test⇩1 c w r p"
begin

lemma complement_language[simp]: "b.language (complement A) = streams (alphabet⇩1 A) - a.language A"
unfolding a.language_def b.language_def a.run_alt_def b.run_alt_def by auto

end

end```