Theory Networks

theory Networks
  imports Timed_Automata.Timed_Automata Munta_Base.Normalized_Zone_Semantics_Impl
    Munta_Base.Reordering_Quantifiers Munta_Base.TA_Syntax_Bundles
begin

unbundle no_library_syntax

section ‹Networks of Timed Automata›

subsection ‹Syntax and Operational Semantics›

text ‹Input, output and internal transitions›

datatype 'a act = In 'a | Out 'a | Sil 'a

datatype 'b label = Del | Act 'b | Syn 'b 'b

type_synonym
  ('a, 'b, 'c, 't, 's) nta = "('a act * 'b, 'c, 't, 's) ta list"

inductive step_n ::
  "('a, 'b, 'c, 't, 's) nta ⇒ 's list ⇒ ('c, ('t::time)) cval ⇒ 'b label
  ⇒ 's list ⇒ ('c, 't) cval ⇒ bool"
("_ ⊢⇩N ⟨_, _⟩ →⇘_⇙ ⟨_,_⟩" [61,61,61,61,61,61] 61)
where
  step_n_t:
    "⟦∀ p ∈ {..<length N}. N!p ⊢ ⟨L!p, u⟩ →⇗d⇖ ⟨L!p, u ⊕ d⟩; d ≥ 0⟧
    ⟹ N ⊢⇩N ⟨L, u⟩ →⇘Del⇙ ⟨L, u ⊕ d⟩" |
  step_n_i:
    "⟦
      N!p ⊢ l ⟶⇗g,(Sil a, b),r⇖ l'; u ⊢ g; ∀ p ∈ {..<length N}. u' ⊢ inv_of (N!p) (L'!p);
      L!p = l; p < length L; L' = L[p := l']; u' = [r→0]u
     ⟧
    ⟹ N ⊢⇩N ⟨L, u⟩ →⇘Act b⇙ ⟨L', u'⟩" |
  step_n_s:
    "⟦N!p ⊢ l1 ⟶⇗g1,(In a, b1),r1⇖ l1'; N!q ⊢ l2 ⟶⇗g2,(Out a, b2),r2⇖ l2'; u ⊢ g1; u ⊢ g2;
      ∀ p ∈ {..<length N}. u' ⊢ inv_of (N!p) (L'!p);
      L!p = l1; L!q = l2; p < length L; q < length L; p ≠ q;
      L' = L[p := l1', q := l2']; u' = [(r1 @ r2)→0]u
     ⟧ ⟹ N ⊢⇩N ⟨L, u⟩ →⇘Syn b1 b2⇙ ⟨L', u'⟩"

inductive_cases[elim!]: "N ⊢⇩N ⟨L, u⟩ →⇘a⇙ ⟨L', u'⟩"

inductive steps_n ::
  "('a, 'b, 'c, 't, 's) nta ⇒ 's list ⇒ ('c, ('t::time)) cval
  ⇒ 's list ⇒ ('c, 't) cval ⇒ bool"
("_ ⊢⇩N ⟨_, _⟩ →* ⟨_,_⟩" [61,61,61] 61)
where
  refl: "N ⊢⇩N ⟨l, Z⟩ →* ⟨l, Z⟩" |
  step: "N ⊢⇩N ⟨l, Z⟩ →* ⟨l', Z'⟩ ⟹ N ⊢⇩N ⟨l', Z'⟩ →⇘_⇙ ⟨l'', Z''⟩
        ⟹ N ⊢⇩N ⟨l, Z⟩ →* ⟨l'', Z''⟩"

declare steps_n.intros[intro]

lemma stepI2:
  "N ⊢⇩N ⟨l, Z⟩ →* ⟨l'', Z''⟩" if "N ⊢⇩N ⟨l', Z'⟩ →* ⟨l'', Z''⟩" "N ⊢⇩N ⟨l, Z⟩ →⇘b⇙ ⟨l', Z'⟩"
  using that
  apply induction
   apply (rule steps_n.step)
    apply (rule refl)
   apply assumption
  apply simp
  by (rule steps_n.step; assumption)

lemma step_n_t_I:
  "⟦∀ p ∈ {..<length N}. u ⊢ inv_of (N!p) (L!p); ∀ p ∈ {..<length N}. u ⊕ d ⊢ inv_of (N!p) (L!p);
    d ≥ 0
   ⟧ ⟹ N ⊢⇩N ⟨L, u⟩ →⇘Del⇙ ⟨L, u ⊕ d⟩"
by (auto intro: step_n_t)

subsection ‹Product Automaton›

abbreviation state_set :: "('a, 'c, 'time, 's) transition set ⇒ 's set" where
  "state_set T ≡ fst ` T ∪ (snd o snd o snd o snd) ` T"

lemma guard_concat:
  assumes "∀ g ∈ set xs. u ⊢ g"
  shows "u ⊢ concat xs"
  using assms by (induction xs) (auto simp: clock_val_def)

lemma guard_append:
  assumes "u ⊢ g1" "u ⊢ g2"
  shows "u ⊢ g1 @ g2"
  using assms by (auto simp: clock_val_def)

lemma concat_guard:
  assumes "u ⊢ concat xs" "g ∈ set xs"
  shows "u ⊢ g"
using assms by (auto simp: list_all_iff clock_val_def)

lemma guard_consE:
  assumes "u ⊢ ac # cc"
  obtains "u ⊢⇩a ac" "u ⊢ cc"
  using assms unfolding clock_val_def by auto

lemma guard_consI:
  assumes "u ⊢⇩a ac" "u ⊢ cc"
  shows "u ⊢ ac # cc"
  using assms unfolding clock_val_def by auto

lemma collect_clock_pairs_append_cases:
  assumes "x ∈ collect_clock_pairs (g1 @ g2)"
  shows "x ∈ collect_clock_pairs g1 ∨ x ∈ collect_clock_pairs g2"
    using assms unfolding collect_clock_pairs_def by auto

lemma list_update_nth_split:
  assumes "j < length xs"
  shows "P (xs[i := x] ! j) = ((i = j ⟶ P x) ∧ (i ≠ j ⟶ P (xs ! j)))"
    using assms by (cases "i = j") auto

locale Product_TA_Defs =
  fixes N :: "('a, 'b, 'c, 't, 's) nta"
begin

  abbreviation "T ≡ map trans_of N"
  abbreviation "I ≡ map inv_of N"

  definition "states = {L. length L = length T ∧ (∀ p ∈ {..<length T}. L!p ∈ state_set (T!p))}"

  definition
    "product_trans_i =
      {(L,g,(a,Act b),r,L[p:=l']) | L p g a b r l'.
      L ∈ states ∧ (L!p, g, (Sil a, b), r, l') ∈ T!p ∧ p < length L}"

  definition
    "product_trans_s =
      {(L,g1 @ g2,(a,Syn b1 b2),r1 @ r2,L[p:=l1',q:=l2']) | L p q g1 g2 a b1 b2 r1 r2 l1' l2'.
        L ∈ states ∧ (L!p, g1, (In a, b1), r1, l1') ∈ T!p ∧ (L!q, g2, (Out a, b2), r2, l2') ∈ T!q
        ∧ p < length L ∧ q < length L ∧ p ≠ q
      }"

  definition
    "product_trans ≡ product_trans_i ∪ product_trans_s"

lemma product_state_set_subs:
  assumes "q < length N" "l ∈ state_set product_trans"
  shows "l ! q ∈ state_set (T ! q)"
  using assms
  unfolding product_trans_def product_trans_i_def product_trans_s_def states_def
  apply safe
     apply (solves auto)
    apply (solves auto)
  apply simp
   apply (subst list_update_nth_split; force)
  apply simp
  apply (subst list_update_nth_split)
   apply simp
  apply safe
   apply (subst (asm) (2) list_update_nth_split; force)
  apply (subst list_update_nth_split)
   apply simp
  by (subst (asm) (2) list_update_nth_split; force) ― ‹slow: 13s›

  definition
    "product_invariant L ≡
    concat (map (λ p. if p < length I then (I!p) (L!p) else []) [0..<length L])"

  definition product_ta :: "('a × 'b label, 'c, 't, 's list) ta" where
    "product_ta ≡ (product_trans, product_invariant)"

  lemma collect_clki_product_invariant:
    "Timed_Automata.collect_clki product_invariant = ⋃ (Timed_Automata.collect_clki ` set I)"
    unfolding Timed_Automata.collect_clki_def product_invariant_def
    apply (simp add: image_Union)
    apply safe
    subgoal
      unfolding collect_clock_pairs_def by fastforce
    apply clarsimp
    subgoal premises prems for a b aa ba x
    proof -
      let ?L = "map (λ _. x) [0..<length N]"
      let ?x = "collect_clock_pairs
        (concat
        (map (λp. if p < length N then (I ! p) (?L ! p) else [])
        [0..<length ?L]))"
      show ?thesis
        apply (intro exI[where x = ?x] conjI)
         apply (rule exI; rule HOL.refl)
        apply simp
        using prems unfolding collect_clock_pairs_def by (fastforce dest: mem_nth)
    qed
    done

  lemma states_length:
    assumes "L ∈ states"
    shows "length L = length N"
    using assms unfolding states_def by auto

  lemma collect_clkt_product_trans_subs:
    "Timed_Automata.collect_clkt product_trans ⊆ ⋃ (Timed_Automata.collect_clkt ` set T)"
    unfolding
      Timed_Automata.collect_clkt_def product_trans_def product_trans_i_def product_trans_s_def
    by (fastforce dest: collect_clock_pairs_append_cases states_length)

  lemma collect_clkvt_product_trans_subs:
    "collect_clkvt product_trans ⊆ ⋃ (collect_clkvt ` set T)"
    unfolding collect_clkvt_def product_trans_def product_trans_i_def product_trans_s_def
    by (fastforce dest: states_length)

  lemma statesI_aux:
    fixes L
    assumes L: "L ∈ states"
    assumes
      "p < length T"
      "(l, g, a, r, l') ∈ T ! p"
    shows "(L[p := l]) ∈ states"
    unfolding states_def apply clarsimp
    using L apply (simp add: states_def)
    apply safe
    apply (subst list_update_nth_split)
    using assms by (fastforce simp: states_def)+

  lemma product_trans_s_alt_def:
    "product_trans_s =
      {(L, g, (a, Syn b1 b2), r, L') | L g a b1 b2 r L'. ∃ p q g1 g2 r1 r2 l1' l2'.
      L ∈ states ∧ p < length L ∧ q < length L ∧ p ≠ q ∧
      g = g1 @ g2 ∧ r = r1 @ r2 ∧ L' = L[p:=l1', q:=l2']
        ∧ (L!p, g1, (In a, b1), r1, l1') ∈ T!p ∧ (L!q, g2, (Out a, b2), r2, l2') ∈ T!q
      }"
    unfolding product_trans_s_def by (safe; metis)

  context
    assumes states_not_empty: "states ≠ {}"
    assumes trans_complete:
      "∀ p < length T. ∀ t1 ∈ T ! p. case t1 of (l1, g1, (In a, b1), r1, l1')
      ⇒ ∃ q < length T. p ≠ q ∧ (∃ l2 g2 b2 r2 l2'. (l2, g2, (Out a, b2), r2, l2') ∈ T ! q) |
      (l1, g1, (Out a, b1), r1, l1')
      ⇒ ∃ q < length T. p ≠ q ∧ (∃ l2 g2 b2 r2 l2'. (l2, g2, (In a, b2), r2, l2') ∈ T ! q) | _ ⇒ True"
  begin

  lemma collect_clkt_product_trans_sups:
    "Timed_Automata.collect_clkt product_trans ⊇ ⋃ (Timed_Automata.collect_clkt ` set T)"
  proof
    fix x assume "x ∈ ⋃ (Timed_Automata.collect_clkt ` set T)"
    then obtain trans l1 g1 a' b1 r1 l1' where x:
      "trans ∈ set T" "(l1, g1, (a', b1), r1, l1') ∈ trans" "x ∈ collect_clock_pairs g1"
      unfolding Timed_Automata.collect_clkt_def by force
    then obtain p where p:
        "p < length T" "T ! p = trans"
      by (auto dest!: mem_nth)
    from states_not_empty obtain L where L: "L ∈ states" by auto
    have "length T = length L" by (auto simp: states_length[OF ‹L ∈ states›])
    show "x ∈ Timed_Automata.collect_clkt product_trans"
    proof (cases a')
      case a': (In a)
      with x p trans_complete obtain q l2 g2 b2 r2 l2' where trans2:
        "q < length T" "(l2, g2, (Out a, b2), r2, l2') ∈ T ! q" "p ≠ q"
        by atomize_elim fastforce
      have "L[p := l1, q := l2] ∈ states" (is "?L ∈ _")
        using L p(1) x(1,2) trans2 unfolding p(2)[symmetric] by (auto intro!: statesI_aux)
      moreover have "?L ! p = l1" "?L ! q = l2"
        using ‹p ≠ q› ‹p < length T› ‹q < length T› ‹L ∈ states› by (auto dest: states_length)
      moreover note t = calculation
      have "(?L, g1 @ g2, (a, Syn b1 b2), r1 @ r2, ?L[p := l1', q := l2']) ∈ product_trans_s"
        unfolding product_trans_s_alt_def
        apply clarsimp
        using t p(1) x(1,2) trans2 unfolding p(2)[symmetric] a' ‹length T = length L›
        by metis
      moreover have "x ∈ collect_clock_pairs (g1 @ g2)"
        using x(3) by (auto simp: collect_clock_pairs_def)
      ultimately show ?thesis unfolding Timed_Automata.collect_clkt_def product_trans_def by force
    next
      case a': (Out a)
      with x p trans_complete obtain q l2 g2 b2 r2 l2' where trans2:
        "q < length T" "(l2, g2, (In a, b2), r2, l2') ∈ T ! q" "p ≠ q"
        by atomize_elim fastforce
      have "L[q := l2, p := l1] ∈ states" (is "?L ∈ _")
        using L p(1) x(1,2) trans2 unfolding p(2)[symmetric] by (auto intro!: statesI_aux)
      moreover have "?L ! p = l1" "?L ! q = l2"
        using ‹p ≠ q› ‹p < length T› ‹q < length T› ‹L ∈ states› by (auto dest: states_length)
      moreover note t = calculation
      have "(?L, g2 @ g1, (a, Syn b2 b1), r2 @ r1, ?L[q := l2', p := l1']) ∈ product_trans_s"
        unfolding product_trans_s_alt_def
        apply clarsimp
        using t p(1) x(1,2) trans2 unfolding p(2)[symmetric] a' ‹length T = length L›
        by metis
      moreover have "x ∈ collect_clock_pairs (g2 @ g1)"
        using x(3) by (auto simp: collect_clock_pairs_def)
      ultimately show ?thesis unfolding Timed_Automata.collect_clkt_def product_trans_def by force
    next
      case a': (Sil a)
      have "L[p := l1] ∈ states" (is "?L ∈ _")
        using L p(1) x(1,2) unfolding p(2)[symmetric] by (auto intro!: statesI_aux)
      moreover have "?L ! p = l1"
        using ‹p < length T› ‹L ∈ states› by (auto dest: states_length)
      ultimately have "(?L, g1, (a, Act b1), r1, ?L[p := l1']) ∈ product_trans_i"
        using x p unfolding product_trans_i_def a' by (force simp: states_length[OF ‹L ∈ states›])
      with x(3) show ?thesis unfolding Timed_Automata.collect_clkt_def product_trans_def by force
    qed
  qed

  lemma collect_clkvt_product_trans_sups:
    "collect_clkvt product_trans ⊇ ⋃ (collect_clkvt ` set T)"
  proof
    fix x assume "x ∈ ⋃ (collect_clkvt ` set T)"
    then obtain trans l1 g1 a' b1 r1 l1' where x:
      "trans ∈ set T" "(l1, g1, (a', b1), r1, l1') ∈ trans" "x ∈ set r1"
      unfolding collect_clkvt_def by force
    then obtain p where p:
        "p < length T" "T ! p = trans"
      by (auto dest!: mem_nth)
    from states_not_empty obtain L where L: "L ∈ states" by auto
    show "x ∈ collect_clkvt product_trans"
    proof (cases a')
      case a': (In a)
      with x p trans_complete obtain q l2 g2 b2 r2 l2' where trans2:
        "q < length T" "(l2, g2, (Out a, b2), r2, l2') ∈ T ! q" "p ≠ q"
        by atomize_elim fastforce
      moreover have "L[p := l1, q := l2] ∈ states" (is "?L ∈ _")
        using L p(1) x(1,2) trans2 unfolding p(2)[symmetric] by (auto intro!: statesI_aux)
      moreover have "?L ! p = l1" "?L ! q = l2"
        using ‹p ≠ q› ‹p < length T› ‹q < length T› ‹L ∈ states› by (auto dest: states_length)
      ultimately have
        "(?L, g1 @ g2, (a, Syn b1 b2), r1 @ r2, ?L[p := l1', q := l2']) ∈ product_trans_s"
        using p(1) x trans2 unfolding p(2)[symmetric] a' product_trans_s_def
        by (fastforce simp: states_length[OF ‹L ∈ states›])
      with x(3) show ?thesis unfolding collect_clkvt_def product_trans_def by force
    next
      case a': (Out a)
      with x p trans_complete obtain q l2 g2 b2 r2 l2' where trans2:
        "q < length T" "(l2, g2, (In a, b2), r2, l2') ∈ T ! q" "p ≠ q"
        by atomize_elim fastforce
      moreover have "L[q := l2, p := l1] ∈ states" (is "?L ∈ _")
        using L p(1) x(1,2) trans2 unfolding p(2)[symmetric] by (auto intro!: statesI_aux)
      moreover have "?L ! p = l1" "?L ! q = l2"
        using ‹p ≠ q› ‹p < length T› ‹q < length T› ‹L ∈ states› by (auto dest: states_length)
      ultimately have "(?L, g2 @ g1, (a, Syn b2 b1), r2 @ r1, ?L[q := l2', p := l1']) ∈ product_trans_s"
        using p(1) x trans2 unfolding p(2)[symmetric] a' product_trans_s_def
        apply (simp add: states_length[OF ‹L ∈ states›] del: ex_simps)
        apply (tactic ‹rearrange_ex_tac @{context} 1›)
        apply simp
        apply (rule exI, rule conjI, assumption)
        apply (simp only: ex_simps[symmetric])
        apply (tactic ‹rearrange_ex_tac @{context} 1›)
        apply simp
        by (fastforce simp: states_length[OF ‹L ∈ states›])
          (* fastforce can solve this on its own but not very quickly *)
      with x(3) show ?thesis unfolding collect_clkvt_def product_trans_def by force
    next
      case a': (Sil a)
      have "L[p := l1] ∈ states" (is "?L ∈ _")
        using L p(1) x(1,2) unfolding p(2)[symmetric] by (auto intro!: statesI_aux)
      moreover have "?L ! p = l1"
        using ‹p < length T› ‹L ∈ states› by (auto dest: states_length)
      ultimately have "(?L, g1, (a, Act b1), r1, ?L[p := l1']) ∈ product_trans_i"
        using x p unfolding product_trans_i_def a' by (force simp: states_length[OF ‹L ∈ states›])
      with x(3) show ?thesis unfolding collect_clkvt_def product_trans_def by force
    qed
  qed

  lemma collect_clkt_product_trans:
    "Timed_Automata.collect_clkt product_trans = ⋃ (Timed_Automata.collect_clkt ` set T)"
    using collect_clkt_product_trans_sups collect_clkt_product_trans_subs by simp

  lemma collect_clkvt_product_trans:
    "collect_clkvt product_trans = ⋃ (collect_clkvt ` set T)"
  using collect_clkvt_product_trans_sups collect_clkvt_product_trans_subs by simp

  end (* End of context for syntactic 1-to-1 correspondence for transitions *)

  context
    assumes finite_trans: "∀ A ∈ set N. finite (trans_of A)"
  begin

  lemma finite_states:
    "finite states"
  proof -
    have "states ⊆ {L. set L ⊆
          (⋃ {fst ` trans_of (N ! p) | p. p < length N} ∪
            ⋃ {(snd ∘ snd ∘ snd ∘ snd) ` trans_of (N ! p) | p. p < length N})
          ∧ length L = length N}"
      unfolding states_def
      apply clarsimp
      apply (drule mem_nth)
      apply safe
      subgoal for _ _ i
        by (erule ballE[where x = i]) auto
      done
    moreover have "finite …" using finite_trans by - (rule finite_lists_length_eq; auto)
    ultimately show ?thesis by (rule finite_subset)
  qed

  lemma finite_product_trans_i:
    "finite product_trans_i"
  proof -
    let ?N = "⋃ (trans_of ` set N)"
    let ?S = "{(L, p, g, (a, Act b), r, l')|L p g a b r l'.
      L ∈ states ∧ (L ! p, g, (Sil a, b), r, l') ∈ map trans_of N ! p ∧ p < length L}"
    let ?R = "{(L, p, g, (a, Act b), r, l')|L p g a b r l'.
      L ∈ states ∧ p < length L ∧ (g, (Sil a, b), r, l') ∈ snd ` ?N}"
    have "?S ⊆ ?R" by (fastforce simp: states_length dest: nth_mem)
    moreover have "finite ?R" using finite_states [[simproc add: finite_Collect]]
      apply simp
      apply (rule finite_imageI)
      apply (rule finite_SigmaI)
       apply (rule finite_subset[where B = "{(p, L). p < length L ∧ L ∈ states}"])
        apply force
      using states_length
       apply -
       apply (rule finite_subset[where B = "{(p, L). p < length N ∧ L ∈ states}"]; fastforce)
      using finite_trans
      apply (intro finite_vimageI)
      unfolding inj_on_def by auto
    ultimately have "finite ?S" by (rule finite_subset)
    moreover have "product_trans_i = (λ (L, p, g, a, r, l'). (L, g, a, r, L[p := l'])) ` ?S"
      unfolding product_trans_i_def by (auto 4 3 simp: image_Collect)
    ultimately show ?thesis by auto
  qed

  lemma finite_Collect_bounded_ex_5' [simp]:
  assumes "finite {(a,b,c,d,e) . P a b c d e}"
  shows
    "finite {x. ∃a b c d e. P a b c d e ∧ Q x a b c d e}
    ⟷ (∀ a b c d e. P a b c d e ⟶ finite {x. Q x a b c d e})"
  using assms finite_Collect_bounded_ex[OF assms, where Q = "λ x. λ (a, b, c, d, e). Q x a b c d e"]
  by clarsimp (* force, simp *)

  lemma finite_product_trans_s:
    "finite product_trans_s"
  proof -
    let ?N = "⋃ (trans_of ` set N)"
    have "(g1, (In a, b), r1, l1') ∈ snd ` ?N" if
      "(L ! p, g1, (In a, b), r1, l1') ∈ map trans_of N ! p" "p < length L" "L ∈ states"
      for L p g1 a b r1 l1'
      using that by (auto simp: states_length dest: nth_mem)
    let ?S = "{(L, p, q, g1, g2, (a, Syn b1 b2), r1, r2, l1', l2')|L p q g1 g2 a b1 b2 r1 r2 l1' l2'.
      L ∈ states ∧ (L ! p, g1, (In a, b1), r1, l1') ∈ map trans_of N ! p ∧
        (L ! q, g2, (Out a, b2), r2, l2') ∈ map trans_of N ! q ∧ p < length L ∧ q < length L}"
    define F1 where "F1 ≡ {(g1, a, b, r1, l1') | g1 a b r1 l1'. (g1, (In a, b), r1, l1') ∈ snd ` ?N}"
    have fin1: "finite F1" unfolding F1_def using finite_trans
      using [[simproc add: finite_Collect]] by (force simp: inj_on_def intro: finite_vimageI)
    define F2 where "F2 ≡ {(g1, a, b, r1, l1') | g1 a b r1 l1'. (g1, (Out a, b), r1, l1') ∈ snd ` ?N}"
    have fin2: "finite F2" unfolding F2_def using finite_trans
      using [[simproc add: finite_Collect]] by (force simp: inj_on_def intro: finite_vimageI)
    define R where "R ≡ {(L, p, q, g1, g2, (a, Syn b1 b2), r1, r2, l1', l2')|L p q g1 g2 a b1 b2 r1 r2 l1' l2'.
      L ∈ states ∧ p < length L ∧ q < length L ∧ (g1, a, b1, r1, l1') ∈ F1 ∧ (g2, a, b2, r2, l2') ∈ F2}"

    have R_alt_def: "R = {t. ∃ L p q g1 a b1 r1 l1' g2 b2 r2 l2'.
      L ∈ states ∧ p < length L ∧ q < length L
      ∧ (g1, a, b1, r1, l1') ∈ F1 ∧ (g2, a, b2, r2, l2') ∈ F2
      ∧ t = (L, p, q, g1, g2, (a, Syn b1 b2), r1, r2, l1', l2')
      }"
      unfolding R_def by auto
    have "?S ⊆ R" by (fastforce simp: R_alt_def F1_def F2_def states_length dest: nth_mem)
    moreover have "finite R"
      unfolding R_alt_def
      using fin1 fin2 finite_states
      using [[simproc add: finite_Collect]]
      by (auto simp: inj_on_def intro: finite_vimageI intro!: finite_imageI)
    ultimately have "finite ?S" by (rule finite_subset)
    moreover have
      "product_trans_s
      ⊆ (λ (L, p, q, g1, g2, a, r1, r2, l1', l2').
          (L, g1 @ g2, a, r1 @ r2, L[p := l1', q := l2'])) ` ?S"
      unfolding product_trans_s_def by (simp add: image_Collect) blast
    ultimately show ?thesis by (auto intro: finite_subset)
  qed

  lemma finite_trans_of_product:
    shows "finite (trans_of product_ta)"
    using finite_product_trans_s finite_product_trans_i
    unfolding product_ta_def trans_of_def product_trans_def
    by auto

  end (* End of context for finiteness of trans *)

  lemma inv_of_product[simp]:
      "inv_of product_ta = product_invariant"
    unfolding product_ta_def inv_of_def by simp

  lemma concat_map_if_aux:
    assumes "(m :: nat) ≥ n"
    shows "concat (map (λ i. if i < n then f i else []) [0..<m])
         = concat (map (λ i. if i < n then f i else []) [0..<n])"
    using assms by (induction rule: dec_induct) auto

  lemma finite_invariant_of_product[folded inv_of_product]:
    assumes "∀ A ∈ set N. finite (range (inv_of A))"
    shows "finite (range product_invariant)"
  proof -
    let ?N = "⋃ (range ` inv_of ` set N)"
    let ?X = "{I. set I ⊆ ?N ∧ length I ≤ length N}"
    have "[] ∈ ?X" by auto
    have "finite ?N"
      using assms
      by auto
    then have "finite ?X" by (rule finite_lists_length_le)
    moreover have "range product_invariant ⊆ concat ` ?X"
    proof
      fix x assume "x ∈ range product_invariant"
      then obtain L where L:
            "x = concat
                       (map (λp. if p < length (map inv_of N)
                                  then (map inv_of N ! p) (L ! p) else [])
                         [0..<length L])"
        unfolding product_invariant_def by auto
      show "x ∈ concat ` ?X"
      proof (cases "length L ≤ length N")
        case True
        then show ?thesis using L by (fastforce dest: nth_mem)
      next
        case False
        then have "x = concat
                       (map (λp. if p < length (map inv_of N)
                                  then (map inv_of N ! p) (L ! p) else [])
                         [0..<length N])"
          using L by (auto intro: concat_map_if_aux)
        then show ?thesis by (fastforce dest: nth_mem)
      qed
    qed
    ultimately show ?thesis by - (drule finite_subset; auto)
  qed

end (* End locale for product TA definition *)

locale Product_TA_Defs' =
  Product_TA_Defs N for N :: "('a, 'b, 'c, 't :: time, 's) nta"
begin

  lemma product_invariantD:
    assumes "u ⊢ product_invariant L" "p < length N" "length L = length N"
    shows "u ⊢ inv_of (N ! p) (L!p)"
  using assms unfolding product_invariant_def by (force intro: concat_guard)

  lemma states_step:
    "L' ∈ states" if "N ⊢⇩N ⟨L, u⟩ →⇘a⇙ ⟨L', u'⟩" "L ∈ states"
    using that unfolding states_def apply safe
        apply simp
       apply simp
      apply force
     apply (subst list_update_nth_split)
      apply simp
     apply (rule conjI)
      apply clarsimp
    subgoal premises prems for p g a r l'
      using prems(3-6) by force
     apply clarsimp
     apply (solves auto)
    apply (subst list_update_nth_split)
     apply (simp; fail)
    apply safe
     apply simp
    subgoal premises prems
      using prems(3-7) by force
    apply (subst list_update_nth_split)
     apply simp
    apply safe
     apply simp
    subgoal premises prems
      using prems(3-6) by force
    by auto

  lemma states_steps:
    "L' ∈ states" if "N ⊢⇩N ⟨L, u⟩ →* ⟨L', u'⟩" "L ∈ states"
    using that apply (induction N ≡ N _ _ _ _ rule: steps_n.induct)
     apply assumption
    apply simp
    by (rule states_step; assumption)

end

lemma steps_altI:
  "A ⊢ ⟨l, Z⟩ →* ⟨l'', Z''⟩" if
  "A ⊢ ⟨l, Z⟩ →* ⟨l', Z'⟩" "A ⊢ ⟨l', Z'⟩ → ⟨l'', Z''⟩"
  using that by (induction; blast)

(* Network + valid start state *)
locale Product_TA =
  Product_TA_Defs' N for N :: "('a, 'b, 'c, 't :: time, 's) nta" +
  fixes L :: "'s list"
  assumes states[intro]: "L ∈ states"
begin

  lemma
    len[simp]: "length L = length N"
  using states unfolding states_def by auto

  lemma product_delay_complete:
    assumes step: "N ⊢⇩N ⟨L, u⟩ →⇘Del⇙ ⟨L', u'⟩"
    obtains d where "product_ta ⊢ ⟨L, u⟩ →⇗d⇖ ⟨L', u'⟩"
  using step proof cases
    case prems: (step_n_t d)
    from prems have *:
      "∀p∈{..<length N}. u ⊕ d ⊢ inv_of (N ! p) (L ! p)"
    by (auto elim!: step_t.cases)
    from prems * show ?thesis
    by (fastforce simp add: product_ta_def inv_of_def product_invariant_def[abs_def]
                  intro!: guard_concat that
       )
  qed

  lemma product_int_complete:
    assumes step: "N ⊢⇩N ⟨L, u⟩ →⇘Act b⇙ ⟨L', u'⟩"
    obtains a where "product_ta ⊢ ⟨L, u⟩ →⇘(a, Act b)⇙ ⟨L', u'⟩"
    using step proof cases
    case prems: (step_n_i p l g a r l')
    from prems show ?thesis
      apply -
      apply (rule that)
      apply (rule step_a.intros[where g = g and r = r])
      by (fastforce
          simp: product_trans_def product_trans_i_def product_invariant_def product_ta_def
          trans_of_def inv_of_def
          intro: guard_concat
          )+
  qed

  lemma product_sync_complete:
    assumes step: "N ⊢⇩N ⟨L, u⟩ →⇘Syn b1 b2⇙ ⟨L', u'⟩"
    obtains a where "product_ta ⊢ ⟨L, u⟩ →⇘(a, Syn b1 b2)⇙ ⟨L', u'⟩"
    using step proof cases
    case prems: (step_n_s p l1 g1 a r1 l1' q l2 g2 r2 l2')
    from prems show ?thesis
      apply -
      apply (rule that)
      apply (rule step_a.intros[where g = "g1 @ g2" and a = "(a, Syn b1 b2)" and r = "r1 @ r2"])
      subgoal premises prems
        apply
          (clarsimp simp add:
            product_trans_def product_trans_s_def product_invariant_def product_ta_def
            trans_of_def inv_of_def
            )
        apply (erule allE[where x = p])
        using ‹p < _› apply simp
        apply (erule allE[where x = q])
        using prems by (fastforce simp: trans_of_def)
      by (fastforce
            simp: product_invariant_def product_ta_def inv_of_def
            intro: guard_concat guard_append
         )+
  qed

  lemma product_complete:
    assumes step: "N ⊢⇩N ⟨L, u⟩ →⇘b⇙ ⟨L', u'⟩"
    shows "product_ta ⊢ ⟨L, u⟩ → ⟨L', u'⟩"
    using step
    by (cases b) (rule product_delay_complete product_int_complete product_sync_complete, simp, blast)+

  lemma product_ta_cases:
    assumes "product_ta ⊢ L ⟶⇗g,a,r⇖ L'"
    shows "(L, g, a, r, L') ∈ product_trans_i ∨ (L, g, a, r, L') ∈ product_trans_s"
  using assms unfolding product_ta_def trans_of_def product_trans_def by auto

  lemma product_delay_sound:
    assumes step: "product_ta ⊢ ⟨L, u⟩ →⇗d⇖ ⟨L', u'⟩"
    shows "N ⊢⇩N ⟨L, u⟩ →⇘Del⇙ ⟨L', u'⟩"
  using assms by cases (force intro!: step_n_t product_invariantD len)

  lemma product_action_sound:
    assumes step: "product_ta ⊢ ⟨L, u⟩ →⇘(a, b)⇙ ⟨L', u'⟩"
    shows "N ⊢⇩N ⟨L, u⟩ →⇘b⇙ ⟨L', u'⟩"
    using assms
    apply cases
    apply simp
    apply (drule product_ta_cases)
    apply (erule disjE)
    unfolding product_trans_i_def product_trans_s_def
     apply (solves ‹auto intro!: product_invariantD step_n_i›)
    by (auto intro!: product_invariantD step_n_s simp: clock_val_def)

  lemma product_sound:
    assumes step: "product_ta ⊢ ⟨L, u⟩ → ⟨L', u'⟩"
    obtains a where "N ⊢⇩N ⟨L, u⟩ →⇘a⇙ ⟨L', u'⟩"
    using step by cases (force dest!: product_action_sound product_delay_sound)+

  lemma states_product_step[intro]:
    "L' ∈ states" if "product_ta ⊢ ⟨L, u⟩ → ⟨L', u'⟩"
    by (auto intro: product_sound that elim!: states_step)

  lemma product_steps_sound:
    "N ⊢⇩N ⟨L, u⟩ →* ⟨L', u'⟩" if "product_ta ⊢ ⟨L, u⟩ →* ⟨L', u'⟩"
    using that states proof (induction A ≡ product_ta _ _ _ _ rule: steps.induct)
    case (refl l u)
    then show ?case by blast
  next
    case prems: (step l u l' u' l'' u'')
    interpret interp: Product_TA N l by standard (rule prems)
    from prems have *: "N ⊢⇩N ⟨l', u'⟩ →* ⟨l'',u''⟩" by auto
    from prems show ?case by - (erule interp.product_sound, rule stepI2, rule *)
  qed

  lemma product_steps_complete:
    "product_ta ⊢ ⟨L, u⟩ →* ⟨L', u'⟩" if "N ⊢⇩N ⟨L, u⟩ →* ⟨L', u'⟩"
    using that states proof (induction N ≡ N _ _ _ _ rule: steps_n.induct)
    case (refl l Z)
    then show ?case by blast
  next
    case prems: (step l Z l' Z' _ l'' Z'')
    interpret interp: Product_TA N l' by standard (blast intro: prems states_steps)
    from prems show ?case by - (assumption | rule steps_altI interp.product_complete)+
  qed

  lemma product_correct:
    "product_ta ⊢ ⟨L, u⟩ →* ⟨L', u'⟩ ⟷ N ⊢⇩N ⟨L, u⟩ →* ⟨L', u'⟩"
    by (metis product_steps_complete product_steps_sound)

  end (* End context: network + valid start state *)

end (* End of theory *)