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