Theory State_Networks

theory State_Networks
  imports Networks Munta_Base.Normalized_Zone_Semantics_Impl
    Munta_Base.More_Methods
begin

unbundle no_library_syntax

section ‹Networks of Timed Automata With Discrete State›

subsection ‹Syntax and Operational Semantics›

text ‹
  We extend Networks of Timed Automata with arbitrary shared (global) state.
  Syntactically, this extension is very simple.
  We can just use the free action label slot to annotate edges with a guard
  and an update function on discrete states.
  The slightly more clumsy part is adding invariants for discrete states
  by directly specifying an invariant annotating function.
›

type_synonym
  ('a, 'c, 'time, 's, 'st) transition =
  "'s * ('st ⇒ ('c, 'time) cconstraint) * 'a * ('st ⇒ 'c list) * 's"

type_synonym
  ('a, 'c, 'time, 's, 'st) sta = "('a, 'c, 'time, 's, 'st) transition set * ('c, 'time, 's) invassn"

type_synonym
  ('a, 'c, 't, 's, 'st) snta =
  "('a act × ('st ⇒ bool) × ('st ⇒ 'st option), 'c, 't, 's, 'st) sta list × ('s ⇒ 'st ⇒ bool) list"

(*
type_synonym
  ('a, 'c, 'time, 's) unta = "programc × ('a act, 'c, 'time, 's) uta list"

type_synonym
  ('a, 'c, 't, 's, 'st) snta =
  "('a, ('st ⇒ bool) × ('st ⇒ 'st), 'c, 't, 's) nta × ('s ⇒ 'st ⇒ bool) list"
*)

text ‹
  Semantic states now consist of three things:
  a list of process locations, the shared state, and a clock valuation.
  The semantic extension then is also obvious: we can take the same transitions
  as in the network without shared state, however we have to add state updates
  and checks for guards on the shared state.
  The updates on discrete state for synchronizing transitions are in the same order as in UPPAAL
  (output before input).
›

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

inductive step_sn ::
  "('a, 'c, 't, 's, 'st) snta ⇒ 's list ⇒ 'st ⇒ ('c, ('t::time)) cval ⇒ 'a label
  ⇒ 's list ⇒ 'st ⇒ ('c, 't) cval ⇒ bool"
  ("_ ⊢ ⟨_, _, _⟩ →⇘_⇙ ⟨_, _, _⟩" [61,61,61,61,61] 61)
where
  step_sn_t:
    "(N, I) ⊢ ⟨L, s, u⟩ →⇘Del⇙ ⟨L, s, u ⊕ d⟩"
    if "∀ p ∈ {..<length N}. u ⊕ d ⊢ snd (N ! p) (L ! p)"
       "d ≥ 0" "length N = length I" |
  step_sn_i:
    "(N, I) ⊢ ⟨L, s, u⟩ →⇘Act a⇙ ⟨L', s', u'⟩"
    if "(l, g, (Sil a, c, m), f, l') ∈ fst (N!p)"
       "u ⊢ g s" "∀ p ∈ {..<length N}. u' ⊢ snd (N!p) (L'!p)"
       "r = f s"
       "L!p = l" "p < length L" "L' = L[p := l']" "u' = [r→0]u"
       "c s" "∀ p < length I. (I ! p) (L' ! p) s'" "Some s' = m s"
       "length N = length I" |
  step_sn_s:
    "(N, I) ⊢ ⟨L, s, u⟩ →⇘Syn a⇙ ⟨L', s', u'⟩"
    if "(l1, g1, (In a, ci, mi), f1, l1') ∈ fst (N!p)"
       "(l2, g2, (Out a, co, mo), f2, l2') ∈ fst (N!q)" "u ⊢ g1 s" "u ⊢ g2 s"
       "∀ p ∈ {..<length N}. u' ⊢ snd (N!p) (L'!p)"
       "r1 = f1 s" "r2 = f2 s"
       "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"
       "ci s" "co s" "∀ p < length I. (I ! p) (L' ! p) s'"
       "Some so = mo s" "Some s' = mi so" "length N = length I"

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

inductive steps_sn ::
  "('a, 'c, 't, 's, 'st) snta ⇒ 's list ⇒ 'st ⇒ ('c, ('t::time)) cval
  ⇒ 's list ⇒ 'st ⇒ ('c, 't) cval ⇒ bool"
("_ ⊢ ⟨_, _, _⟩ →* ⟨_, _, _⟩" [61, 61, 61,61,61] 61)
where
  refl: "N ⊢ ⟨L, s, u⟩ →* ⟨L, s, u⟩" |
  step: "N ⊢ ⟨L, s, u⟩ →* ⟨L', s', u'⟩ ⟹ N ⊢ ⟨L', s', u'⟩ →⇘l⇙ ⟨L'', s'', u''⟩
        ⟹ N ⊢ ⟨L, s, u⟩ →* ⟨L'', s'', u''⟩"

declare steps_sn.intros[intro]

lemma stepI2:
  "N ⊢ ⟨l, s, u⟩ →* ⟨l'', s'', u''⟩" if
  "N ⊢ ⟨l', s', u'⟩ →* ⟨l'', s'', u''⟩" "N ⊢ ⟨l, s, u⟩ →⇘a⇙ ⟨l', s', u'⟩"
  using that
  apply induction
   apply rule
    apply (rule refl)
   apply assumption
  apply simp
  by (rule; assumption)

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

subsection ‹Product Automaton›

locale Prod_TA_Defs =
  fixes A :: "('a, 'c, 't, 's, 'st) snta"
begin

definition
  "T_s p s = {(l, g s, a, f s, l') | l g a f l'. (l, g, a, f, l') ∈ fst (fst A ! p)}"

definition
  "N_s s = map (λ p. (T_s p s, snd (fst A ! p))) [0..<length (fst A)]"

abbreviation "P ≡ snd A"

definition "p ≡ length (fst A)"

abbreviation "product s ≡ Product_TA_Defs.product_ta (N_s s)"

abbreviation "T' s ≡ trans_of (product s)"
abbreviation "I' s ≡ inv_of (product s)"

definition
  "prod_trans_i =
    {((L, s), g, a, r, (L', s')) | L s g c a r m L' s'.
     (∀ q < p. (P ! q) (L ! q) s) ∧ (∀ q < p. (P ! q) (L' ! q) s')
     ∧ (L, g, (a, Networks.label.Act (c, m)), r, L') ∈ T' s ∧ c s ∧ Some s' = m s}"

definition
  "prod_trans_s =
    {((L, s), g, a, r, (L', s')) | L s g ci co a r mi mo L' s' so.
      ci s ∧ co s
      ∧ (∀ q < p. (P ! q) (L ! q) s) ∧ (∀ q < p. (P ! q) (L' ! q) s')
      ∧ (L, g, (a, Networks.label.Syn (ci, mi) (co, mo)), r, L') ∈ T' s
      ∧ Some so = mo s
      ∧ Some s' = mi so
    }"

  definition
    "prod_trans ≡ prod_trans_i ∪ prod_trans_s"

  definition
    "prod_invariant ≡ λ (L, s). I' s L"

  definition prod_ta :: "('a, 'c, 't, 's list × 'st) ta" where
    "prod_ta ≡ (prod_trans, prod_invariant)"

  lemma prod_ta_cases:
    assumes "prod_ta ⊢ L ⟶⇗g,a,r⇖ L'"
    shows "(L, g, a, r, L') ∈ prod_trans_i ∨ (L, g, a, r, L') ∈ prod_trans_s"
    using assms unfolding prod_ta_def trans_of_def prod_trans_def by auto

  lemma inv_of_simp:
    "inv_of prod_ta (L, s) = I' s L"
    unfolding inv_of_def prod_ta_def prod_invariant_def by simp

  lemma I'_simp:
    "I' s L = I' s' L"
    unfolding Product_TA_Defs.product_ta_def inv_of_def Product_TA_Defs.product_invariant_def N_s_def
    apply simp
    apply (rule arg_cong[where f = concat])
    by simp

  lemma collect_clki_prod_invariant:
    "Timed_Automata.collect_clki prod_invariant = Timed_Automata.collect_clki (I' s)"
    unfolding prod_invariant_def Timed_Automata.collect_clki_def
    apply (simp split: prod.split)
    apply safe
     apply (subst (asm) I'_simp[where s' = s])
    by auto

  lemma collect_clki_prod_invariant':
    "Timed_Automata.collect_clki prod_invariant
    ⊆ ⋃ {Timed_Automata.collect_clki (snd (fst A ! p)) | p. p < length (fst A)}"
    unfolding collect_clki_prod_invariant[of s]
    unfolding inv_of_def Product_TA_Defs.product_ta_def
    unfolding Product_TA_Defs.product_invariant_def
    unfolding inv_of_def N_s_def
    unfolding Timed_Automata.collect_clki_def
    unfolding collect_clock_pairs_def
    by auto

  lemma collect_clkt_prod_trans_subs:
    "Timed_Automata.collect_clkt prod_trans ⊆ Timed_Automata.collect_clkt (⋃ (T' ` UNIV))"
    unfolding Timed_Automata.collect_clkt_def prod_trans_def prod_trans_i_def prod_trans_s_def
    by fastforce

  lemma collect_clkvt_prod_trans_subs:
    "collect_clkvt prod_trans ⊆ collect_clkvt (⋃ (T' ` UNIV))"
    unfolding collect_clkvt_def prod_trans_def prod_trans_i_def prod_trans_s_def by fastforce

lemma T_simp:
  "T ! q = trans_of (N ! q)" if "q < length N"
  using that oops

  (*
lemma prod_state_set_subs:
  assumes "l ∈ state_set T'" "q < p"
  shows "l ! q ∈ state_set (trans_of (N ! q))"
  using assms
  apply (simp only: T_simp[symmetric] p_def)
  by (rule product_state_set_subs; simp add: product_ta_def trans_of_def)
*)

abbreviation "N ≡ fst A"

context
  fixes Q
  assumes finite_state:
    "∀ l. ∀ q < p. (P ! q) l s ⟶ Q s"
    "finite {s. Q s}"
      and finite_trans: "∀ A ∈ set N. finite (fst A)"
      and p_gt_0: "p > 0"
begin

  lemma finite_state':
    "finite {s. ∀q<p. (P ! q) (L ! q) s}" (is "finite ?S")
  proof -
    from p_gt_0 obtain q where "q < p" by blast
    then have "?S ⊆ {s. Q s}" using finite_state(1) by auto
    moreover have "finite …" by (rule finite_state(2))
    ultimately show ?thesis by (rule finite_subset)
  qed

  lemma finite_trans':
    "∀A∈set (N_s s). finite (trans_of A)"
  unfolding N_s_def apply clarsimp
    unfolding trans_of_def T_s_def
    apply simp
    apply (drule nth_mem)
    using finite_trans
    using [[simproc add: finite_Collect]]
    apply simp
    apply (rule finite_imageI)
    apply (rule finite_vimageI)
     apply simp
    unfolding inj_on_def by auto

  lemma finite_states:
    "finite (Product_TA_Defs.states (N_s s))"
    using finite_trans' by (rule Product_TA_Defs.finite_states)

  lemma
    "finite (T' s)"
    using finite_trans' by (rule Product_TA_Defs.finite_trans_of_product)

  (* Duplicated proof, what is the better way? *)
  lemma finite_product_1:
    "finite (T' s)"
    unfolding product_def
    unfolding trans_of_def Product_TA_Defs.product_ta_def
    apply simp
    unfolding Product_TA_Defs.product_trans_def
  proof safe
    have "Product_TA_Defs.product_trans_i (N_s s)
        ⊆ {(L, g, (a, Networks.label.Act (aa, b)), r, L[p := l']) |L p g a aa b r l'.
            L ∈ Product_TA_Defs.states (N_s s) ∧ p < length (N_s s) ∧
            (L ! p, g, (Sil a, aa, b), r, l') ∈ ⋃ (trans_of ` set (N_s s))}"
      unfolding Product_TA_Defs.product_trans_i_def
      by (fastforce simp: Product_TA_Defs.states_length)
    moreover have "finite …"
      apply defer_ex
      using finite_states[of s] apply clarsimp
      apply (subst finite_Collect_bounded_ex_6)
      subgoal premises prems for y y'
      proof -
        have "
              {(a, b, c, d, e, f). ∃x∈set (N_s s). x ⊢ y ! y' ⟶⇗a,(Sil b, c, d),e⇖ f}
            = {xx. ∃ x a b c d e f. x∈set (N_s s) ∧ x ⊢ y ! y' ⟶⇗a,(Sil b, c, d),e⇖ f
                   ∧ xx = (a, b, c, d, e, f)}"
          by force
        moreover have "finite …" (* finite_Collect_bounded_ex is not crucial here *)
          using finite_trans'[of s]
          using [[simproc add: finite_Collect]]
          by (auto simp: inj_on_def intro: finite_vimageI simp del: finite_Collect_bounded_ex)
        ultimately show ?thesis by simp
      qed
      by auto
    ultimately show "finite (Product_TA_Defs.product_trans_i (N_s s))" by (rule finite_subset)
  next
    have "Product_TA_Defs.product_trans_s (N_s s)
        ⊆ {(L, g1 @ g2, (a, Networks.label.Syn b1 b2), r1 @ r2, L[p := l1', q := l2']) |
              L p q g1 g2 a b1 b2 r1 r2 l1' l2'.
              L ∈ Product_TA_Defs.states (N_s s) ∧
              p < length (N_s s) ∧ q < length (N_s s) ∧
              (L ! p, g1, (In a, b1), r1, l1') ∈ map trans_of (N_s s) ! p ∧
              (L ! q, g2, (Out a, b2), r2, l2') ∈ map trans_of (N_s s) ! q ∧ p ≠ q}"
      unfolding Product_TA_Defs.product_trans_s_def
      by (fastforce simp: Product_TA_Defs.states_length)
    moreover have "finite …"
      apply defer_ex
      using finite_states[of s]
      apply clarsimp
      subgoal
        apply (mini_existential, simp)
        apply (mini_existential, simp)
        apply (mini_existential, simp)
        apply (mini_existential, simp)
        apply (subst finite_Collect_bounded_ex_6)
        subgoal
          using [[simproc add: finite_Collect]] finite_trans'[of s]
          by (auto simp: inj_on_def intro: finite_vimageI)
        apply safe
        apply (subst finite_Collect_bounded_ex_5)
        subgoal
          using [[simproc add: finite_Collect]] finite_trans'[of s]
          by (auto 4 3 simp: simp: inj_on_def intro: finite_vimageI)
        by auto
      done
    ultimately show "finite (Product_TA_Defs.product_trans_s (N_s s))" by (rule finite_subset)
  qed

  lemma prod_trans_i_alt_def:
    "prod_trans_i =
      {((L, s), g, a, r, (L', s')) | L s g c a r m L' s'.
       (L, g, (a, Networks.label.Act (c, m)), r, L') ∈ T' s ∧
       (∀ q < p. (P ! q) (L ! q) s) ∧ (∀ q < p. (P ! q) (L' ! q) s')
       ∧ c s ∧ Some s' = m s}"
    unfolding prod_trans_i_def by (safe; metis)

  lemma Some_finite:
    "finite {x. Some x = y}"
    using not_finite_existsD by fastforce

  lemma finite_prod_trans:
    "finite prod_trans" if "p > 0"
    unfolding prod_trans_def
  proof safe
    have "prod_trans_i ⊆
        {((L, s), g, a, r, (L', s')) | L s g c a r m L' s'.
         Q s ∧
         (L, g, (a, Networks.label.Act (c, m)), r, L') ∈ T' s ∧
         (∀ q < p. (P ! q) (L ! q) s) ∧ (∀ q < p. (P ! q) (L' ! q) s')
         ∧ c s ∧ Some s' = m s}
      "
      unfolding prod_trans_i_alt_def
      using finite_state(1) p_gt_0 by force
    moreover have
      "finite …"
      apply defer_ex
      apply (mini_existential, simp only: ex_simps)
      using finite_state(2) apply clarsimp
      apply (subst finite_Collect_bounded_ex_7)
      using [[simproc add: finite_Collect]] finite_state' finite_product_1
      by (auto 4 3 simp: inj_on_def intro: finite_vimageI)
    ultimately show "finite prod_trans_i" by (rule finite_subset)
  next
    have "prod_trans_s ⊆
        {((L, s), g, a, r, (L', s')) | L s g ci co a r mi mo L' s' so.
          Q s ∧
          product s ⊢ L ⟶⇗g,(a, Networks.label.Syn (ci, mi) (co, mo)),r⇖ L' ∧
          (∀q<p. (P ! q) (L ! q) s) ∧ (∀q<p. (P ! q) (L' ! q) s') ∧
          ci s ∧ co s ∧ Some so = mo s ∧ Some s' = mi so}
      "
      unfolding prod_trans_s_def
      using finite_state(1) p_gt_0 by fastforce
    moreover have
      "finite …"
      apply defer_ex
      apply (mini_existential, simp only: ex_simps)
      using finite_state(2) apply clarsimp
      apply (subst finite_Collect_bounded_ex_9)

      subgoal
        using [[simproc add: finite_Collect]] finite_state' finite_product_1
        by (auto 4 3 simp: inj_on_def intro: finite_vimageI)[]

      apply safe
      subgoal for s a b c d e f g h i
        apply (rule finite_subset[where B =
              "(λ s'. ((a, s), b, e, f, i, s')) ` { s'. ∃ so. Some so = h s ∧ Some s' = g so}"
              ])
         apply force
        apply (rule finite_imageI)
        apply (subst finite_Collect_bounded_ex)
        by (force intro: Some_finite)+
      done
    ultimately show "finite prod_trans_s" by (rule finite_subset)
  qed

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

  abbreviation "states' s ≡ Product_TA_Defs.states (N_s s)"

  lemma N_s_length:
    "length (N_s s) = p"
    unfolding N_s_def p_def by simp

end (* End locale for product TA definition *)

locale Prod_TA_Defs' =
  Prod_TA_Defs A for A :: "('a, 'c, 't :: time, 's, 'st) snta"
begin

lemma A_unfold:
  "A ≡ (N, P)"
  by auto

lemma network_step_delay:
  assumes step: "(N, P) ⊢ ⟨L, s, u⟩ →⇘Del⇙ ⟨L', s', u'⟩" and len: "length L = p"
  shows "N_s s ⊢⇩N ⟨L, u⟩ →⇘Networks.label.Del⇙ ⟨L', u'⟩"
  subgoal
    using step
    apply cases
    subgoal
      apply simp
      apply (rule step_n_t)
      subgoal
        unfolding N_s_def by (auto simp: inv_of_def)
      apply assumption
      done
    done
  done

lemma network_step_silent:
  assumes step: "(N, P) ⊢ ⟨L, s, u⟩ →⇘Act a⇙ ⟨L', s', u'⟩" and len: "length L = p"
  obtains a where "N_s s ⊢⇩N ⟨L, u⟩ →⇘Networks.label.Act a⇙ ⟨L', u'⟩"
  subgoal premises prems
    using step
    apply cases
    subgoal
      apply (rule prems)
      apply (rule step_n_i)
      unfolding N_s_def T_s_def by (auto 4 0 simp: trans_of_def inv_of_def len p_def)
    done
  done

lemma network_step_sync:
  assumes step: "(N, P) ⊢ ⟨L, s, u⟩ →⇘Syn a⇙ ⟨L', s', u'⟩" and len: "length L = p"
  obtains a b where "N_s s ⊢⇩N ⟨L, u⟩ →⇘Networks.label.Syn a b⇙ ⟨L', u'⟩"
  subgoal premises prems
    using step
    apply cases
    subgoal
      subgoal premises A
        apply (rule prems)
        apply (rule step_n_s)
                   defer
                   defer
                   apply (rule A; fail)
                  apply (rule A(4); fail)
        subgoal
          using A unfolding N_s_def by (auto simp: inv_of_def len)
                defer
                defer
                apply (rule A; fail)
               apply (rule A(11); fail)
        using A unfolding N_s_def T_s_def by (auto 4 0 simp: trans_of_def len p_def)
      done
    done
  done

lemma network_step:
  assumes step: "(N, P) ⊢ ⟨L, s, u⟩ →⇘a⇙ ⟨L', s', u'⟩" and len: "length L = p"
  obtains a where "N_s s ⊢⇩N ⟨L, u⟩ →⇘a⇙ ⟨L', u'⟩"
  subgoal
    using step
    apply (cases a; simp)
      apply (rule that, erule network_step_delay[OF _ len, simplified])
     apply (erule network_step_silent[OF _ len, simplified], erule that)
    apply (erule network_step_sync[OF _ len, simplified], erule that)
    done
  done

lemma trans_of_N_s_1:
  "(fst ` trans_of (N_s s ! q)) = fst ` fst (N ! q)" if "q < p"
  using that unfolding trans_of_def N_s_def p_def T_s_def by (auto 0 7 simp: image_iff)

lemma trans_of_N_s_2:
  "((snd o snd o snd o snd) ` trans_of (N_s s ! q)) = (snd o snd o snd o snd) ` fst (N ! q)" if "q < p"
  using that unfolding trans_of_def N_s_def p_def T_s_def by force

lemma
  "fst ` trans_of (N_s s ! q) = fst ` trans_of (N_s s' ! q)" if "q < p"
  using that by (simp add: trans_of_N_s_1)

lemma states'_simp:
  "states' s = states' s'"
  unfolding Product_TA_Defs.states_def using trans_of_N_s_1 trans_of_N_s_2 by (simp add: N_s_length)

  lemma states_step:
    "L' ∈ states' s" if "A ⊢ ⟨L, s, u⟩ →⇘a⇙ ⟨L', s', u'⟩" "L ∈ states' s"
  proof -
    interpret Product_TA_Defs' "N_s s" .
    from ‹L ∈ _› have "L ∈ states" .
    from ‹L ∈ _› have "length L = p" by (simp add: N_s_length states_length)
    with network_step[folded A_unfold, OF that(1)] obtain a where
      "N_s s ⊢⇩N ⟨L, u⟩ →⇘a⇙ ⟨L',u'⟩"
      by auto
    then show ?thesis using that(2) by (rule states_step)
  qed

  lemma states_steps:
    "L' ∈ states' s'" if "A ⊢ ⟨L, s, u⟩ →* ⟨L', s', u'⟩" "L ∈ states' s"
    using that proof (induction A ≡ A _ _ _ _ _ _ rule: steps_sn.induct)
    case (refl L s u)
    then show ?case by assumption
  next
    case (step L s u L' s' u' L'' s'' u'')
    with states_step[of L' s' u' L'' s'' u''] states'_simp show ?case by blast
  qed

  lemma inv_step:
    "∀p<length P. (P ! p) (L' ! p) s'" if
    "A ⊢ ⟨L, s, u⟩ →⇘a⇙ ⟨L', s', u'⟩" "∀p<length P. (P ! p) (L ! p) s"
    using that by (cases) auto

  lemma inv_steps:
    "∀p<length P. (P ! p) (L' ! p) s'" if
    "A ⊢ ⟨L, s, u⟩ →* ⟨L', s', u'⟩" "∀p<length P. (P ! p) (L ! p) s"
    using that by (induction A ≡ A _ _ _ _ _ _ rule: steps_sn.induct) (auto dest: inv_step)

end

(* Network + valid start state *)
locale Prod_TA =
  Prod_TA_Defs' A for A :: "('a, 'c, 't :: time, 's, 'st) snta" +
  fixes L :: "'s list" and s :: 'st
  assumes states[intro]: "L ∈ states' s"
  assumes Len: "length N = length P"
      and inv: "∀p<length P. (P ! p) (L ! p) s"
begin

  sublocale Product_TA "N_s s" L by standard rule

  lemma inv_prod_simp:
    "inv_of prod_ta (l, s') = Product_TA_Defs.product_invariant (N_s s') l" if "length l = p"
    unfolding prod_ta_def prod_invariant_def Product_TA_Defs.product_ta_def N_s_def inv_of_def
    using that by (simp add: p_def)

  lemma inv_of_N_simp:
    "map inv_of (N_s s') ! q = I ! q" if "q < p"
    using that unfolding inv_of_def N_s_def p_def by simp

  lemma product_inv_prod_simp:
    "inv_of prod_ta (l, s') = I' s l" if "length l = p"
    using that
    apply (simp add: inv_prod_simp)
    apply (simp add: N_s_length inv_of_def Product_TA_Defs.product_invariant_def)
    apply (rule arg_cong[where f = concat])
    apply (clarsimp cong: map_cong)
    by (subst inv_of_N_simp; simp)

  lemma product_inv_prod[intro]:
    "u ⊢ inv_of prod_ta (l, s')" if "u ⊢ inv_of product_ta l" "length l = p"
    using that by (simp add: product_inv_prod_simp)

  lemma A_simp[simp]:
    "N' = N" "P' = P" if "A = (N', P')"
    using that by auto

  lemma length_L[intro]:
    "length L = p"
    by (simp add: N_s_length)

  lemma prod_complete_delay:
    assumes step: "A ⊢ ⟨L, s, u⟩ →⇘Del⇙ ⟨L', s', u'⟩"
    obtains d where "prod_ta ⊢ ⟨(L, s), u⟩ →⇗d⇖ ⟨(L', s'), u'⟩"
  using step proof cases
    case prems: (step_sn_t N d P)
    note [simp] = A_simp[OF prems(1)]
    from prems have "N_s s ⊢⇩N ⟨L, u⟩ →⇘Networks.Del⇙ ⟨L', u'⟩"
      unfolding N_s_def by (auto 4 3 simp: inv_of_def intro: step_n_t)
    with prems show ?thesis
      by (auto 4 4
          intro: that
          simp: product_inv_prod_simp[OF length_L]
          elim!: product_delay_complete step_t.cases)
  qed

  lemma prod_complete_silent:
    assumes step: "A ⊢ ⟨L, s, u⟩ →⇘Act a⇙ ⟨L', s', u'⟩"
    obtains a where "prod_ta ⊢ ⟨(L, s), u⟩ →⇘a⇙ ⟨(L', s'), u'⟩"
  using step proof cases
    case prems: (step_sn_i l g c m f l' N q r I)
    note [simp] = A_simp[OF prems(1)]
    from prems(13) have [simp]: "length P = p" by (simp add: p_def)
    have "N_s s ⊢⇩N ⟨L, u⟩ →⇘Networks.label.Act (c, m)⇙ ⟨L', u'⟩"
      apply (rule step_n_i)
      using prems unfolding N_s_def T_s_def by (auto 3 0 simp: trans_of_def inv_of_def N_s_length)
    with ‹length P = p› obtain b where
      "product_ta ⊢ ⟨L, u⟩ →⇘(b, Networks.label.Act (c, m))⇙ ⟨L', u'⟩"
      by (clarsimp elim!: product_int_complete)
    with prems inv obtain g r where step:
      "((L, s), g, b, r, (L', s')) ∈ prod_trans_i"
      "u ⊢ g" "[r→0]u = u'" "u' ⊢ inv_of product_ta L'"
        apply atomize_elim
      unfolding prod_trans_i_def by - (erule step_a.cases; auto)
    then have "((L, s), g, b, r, (L', s')) ∈ trans_of prod_ta"
      by (simp add: prod_trans_def trans_of_def prod_ta_def)
    moreover have "length L' = p"
      using length_L prems(8) by auto
    ultimately show ?thesis
      apply -
      apply (rule that)
      apply rule
      using step(2-) by force+
  qed

  lemma prod_complete_sync:
    assumes step: "A ⊢ ⟨L, s, u⟩ →⇘Syn a⇙ ⟨L', s', u'⟩"
    obtains a where "prod_ta ⊢ ⟨(L, s), u⟩ →⇘a⇙ ⟨(L', s'), u'⟩"
  using step proof cases
    case prems: (step_sn_s l1 g1 ci mi f1 l1' N q1 l2 g2 co mo f2 l2' q2 r1 r2 I so)
    note [simp] = A_simp[OF prems(1)]
    from prems(21) have [simp]: "length P = p" by (simp add: p_def)
    (* Clean *)
    have "N_s s ⊢⇩N ⟨L, u⟩ →⇘Networks.label.Syn (ci, mi) (co, mo)⇙ ⟨L', u'⟩"
        apply (rule step_n_s)
                   defer
                   defer
                   apply (rule prems; fail)
                  apply (rule prems(5); fail)
        subgoal
          using prems unfolding N_s_def by (auto simp: inv_of_def)
                defer
                defer
                apply (rule prems; fail)
               apply (rule prems(12); fail)
        using prems unfolding N_s_def T_s_def by (auto 3 0 simp: trans_of_def p_def N_s_length)
    with ‹length P = p› obtain a where
      "product_ta ⊢ ⟨L, u⟩ →⇘(a, Networks.label.Syn (ci, mi) (co, mo))⇙ ⟨L', u'⟩"
      by (auto elim!: product_sync_complete)
    with prems inv obtain g r where step:
        "((L, s), g, a, r, (L', s')) ∈ prod_trans_s"
        "u ⊢ g" "[r→0]u = u'" "u' ⊢ inv_of product_ta L'"
        apply atomize_elim
      unfolding prod_trans_s_def by - (erule step_a.cases; auto; blast) (* Slow *)
    then have "((L, s), g, a, r, (L', s')) ∈ trans_of prod_ta"
      by (simp add: prod_trans_def trans_of_def prod_ta_def)
    moreover have "length L' = p"
      using length_L ‹L' = _› by auto
    ultimately show ?thesis
      apply -
      apply (rule that)
      apply rule
      using step(2-) by force+
  qed
    
  lemma prod_complete:
    assumes step: "A ⊢ ⟨L, s, u⟩ →⇘a⇙ ⟨L', s', u'⟩"
    shows "prod_ta ⊢ ⟨(L, s), u⟩ → ⟨(L', s'), u'⟩"
    using step
    by (cases a; simp; blast elim!: prod_complete_delay prod_complete_silent prod_complete_sync)

  lemma A_unfold:
    "A = (N, P)"
    by simp

  lemma prod_sound'_delay:
    assumes step: "prod_ta ⊢ ⟨(L, s), u⟩ →⇗d⇖ ⟨(L', s'), u'⟩"
    shows "A ⊢ ⟨L, s, u⟩ →⇘Del⇙ ⟨L', s', u'⟩ ∧ product_ta ⊢ ⟨L, u⟩ → ⟨L', u'⟩
           ∧ (∀p<length P. (P ! p) (L' ! p) s')"
    using assms proof cases
    case prems: 1
    then have "product_ta ⊢ ⟨L, u⟩ →⇗d⇖ ⟨L', u'⟩" unfolding inv_of_simp by fast
    moreover from product_delay_sound[OF this] prems(1-3) have "A ⊢ ⟨L, s, u⟩ →⇘Del⇙ ⟨L', s', u'⟩"
      apply simp
      apply (subst A_unfold)
      apply (rule step_sn_t)
      by (auto simp: N_s_def inv_of_def step_t.simps N_s_length p_def Len intro: ‹0 ≤ d›)
    ultimately show ?thesis using prems inv by fast
  qed

  lemma prod_sound'_action:
    assumes step: "prod_ta ⊢ ⟨(L, s), u⟩ →⇘a⇙ ⟨(L', s'), u'⟩"
    obtains a where "(A ⊢ ⟨L, s, u⟩ →⇘a⇙ ⟨L', s', u'⟩ ∧ a ≠ Del) ∧ product_ta ⊢ ⟨L, u⟩ → ⟨L', u'⟩
             ∧ (∀p<length P. (P ! p) (L' ! p) s')"
    using assms
  proof cases
    case prems: (1 g r)
    from Len have [simp]: "length P = p" by (simp add: p_def)
    from prems(1)[THEN prod_ta_cases] show ?thesis
    proof (rule disjE, goal_cases)
      case 1
      then obtain c m where *:
        "Some s' = m s" "∀q<p. (P ! q) (L ! q) s" "∀q<p. (P ! q) (L' ! q) s'"
        "product_ta ⊢ L ⟶⇗g,(a, Networks.label.Act (c, m)),r⇖ L'" "c s"
        unfolding prod_trans_i_def by auto
      with prems have "product_ta ⊢ ⟨L, u⟩ →⇘(a, Networks.label.Act (c, m))⇙ ⟨L', u'⟩"
        unfolding inv_of_simp by (metis I'_simp step_a.intros)
      moreover from product_action_sound[OF this] prems(3-4) obtain a where
        "A ⊢ ⟨L, s, u⟩ →⇘Act a⇙ ⟨L', s', u'⟩"
        apply safe
        apply (simp add: N_s_def trans_of_def N_s_length T_s_def)
        apply (simp only: ex_simps[symmetric])
        apply (erule exE, erule exE)
        apply (rule that)
        apply (subst A_unfold)
        apply (rule step_sn_i)
                   apply fast
        using *(3) by (auto simp: N_s_def inv_of_def p_def ‹Some s' = m s› intro: ‹c s›)
      ultimately show ?thesis using * by (auto intro: that)
    next
      case 2
      then obtain ci co mi mo si where *:
        "Some s' = mi si" "Some si = mo s" "∀q<p. (P ! q) (L ! q) s" "∀q<p. (P ! q) (L' ! q) s'"
        "product_ta ⊢ L ⟶⇗g,(a, Networks.label.Syn (ci, mi) (co, mo)),r⇖ L'"
        "ci s" "co s"
        unfolding prod_trans_s_def by auto
      with prems have "product_ta ⊢ ⟨L, u⟩ →⇘(a, Networks.label.Syn (ci, mi) (co, mo))⇙ ⟨L', u'⟩"
        unfolding inv_of_simp by (metis I'_simp step_a.intros)
      moreover from product_action_sound[OF this] prems(3-4) obtain a where
        "A ⊢ ⟨L, s, u⟩ →⇘Syn a⇙ ⟨L', s', u'⟩"
        apply safe
        apply (simp add: N_s_def trans_of_def N_s_length T_s_def)
        apply (simp only: ex_simps[symmetric])
        apply (erule exE, erule exE, erule exE, erule exE)
        apply (rule that)
        apply (subst A_unfold)
        apply (rule step_sn_s)
                           apply fast
                          apply blast
        using *(4) by (auto simp: N_s_def inv_of_def p_def ‹Some s' = _› ‹Some si = _› intro: *(6-)) (* Slow *)
      ultimately show ?thesis using * by (intro that conjI) auto
    qed
  qed

  lemma prod_sound':
    assumes step: "prod_ta ⊢ ⟨(L, s), u⟩ → ⟨(L', s'), u'⟩"
    obtains a where "A ⊢ ⟨L, s, u⟩ →⇘a⇙ ⟨L', s', u'⟩ ∧ product_ta ⊢ ⟨L, u⟩ → ⟨L', u'⟩
             ∧ (∀p<length P. (P ! p) (L' ! p) s')"
    using assms apply cases
     apply (erule prod_sound'_action; blast intro: that)
    apply (rule that, erule prod_sound'_delay)
    done

  lemmas prod_sound = prod_sound'[THEN conjunct1]
  lemmas prod_inv_1 = prod_sound'[THEN conjunct2, THEN conjunct1]
  lemmas prod_inv_2 = prod_sound'[THEN conjunct2, THEN conjunct2]

  lemma states_prod_step[intro]:
    "L' ∈ states" if "prod_ta ⊢ ⟨(L, s), u⟩ → ⟨(L', s'), u'⟩"
    by (blast intro: prod_inv_1[OF that])

  lemma inv_prod_step[intro]:
    "∀p<length P. (P ! p) (L' ! p) s'" if "prod_ta ⊢ ⟨(L, s), u⟩ → ⟨(L', s'), u'⟩"
    using that by (blast intro: prod_inv_2)

  lemma prod_steps_sound:
    assumes step: "prod_ta ⊢ ⟨(L, s), u⟩ →* ⟨(L', s'), u'⟩"
    shows "A ⊢ ⟨L, s, u⟩ →* ⟨L', s', u'⟩"
    using step states inv
  proof (induction A ≡ prod_ta l ≡ "(L, s)" _ l' ≡ "(L', s')" _ arbitrary: L s rule: steps.induct)
    case (refl u)
    then show ?case by blast
  next
    case prems: (step u l' u' u'' L s)
    obtain L'' s'' where "l' = (L'', s'')" by force
    interpret interp: Prod_TA A L s by (standard; rule prems Len)
    from prems(3)[OF ‹l' = _›] prems(1,2,4-) have *: "A ⊢ ⟨L'', s'', u'⟩ →* ⟨L', s', u''⟩"
      unfolding ‹l' = _›
      by (metis Prod_TA_Defs'.states'_simp interp.states_prod_step interp.inv_prod_step)
    show ?case
      using * prems by (auto simp: ‹l' = _› intro: interp.prod_sound stepI2)
  qed

  lemma prod_steps_complete:
    "prod_ta ⊢ ⟨(L, s), u⟩ →* ⟨(L', s'), u'⟩" if "A ⊢ ⟨L, s, u⟩ →* ⟨L', s', u'⟩"
    using that states inv proof (induction A ≡ A L _ _ _ _ _ rule: steps_sn.induct)
    case (refl L s u)
    then show ?case by blast
  next
    case prems: (step L s u L' s' u' L'' s'' u'')
    interpret interp: Prod_TA A L' s' apply standard
      using prems by - (assumption | rule Prod_TA_Defs'.states_steps Len Prod_TA_Defs'.inv_steps)+
    from prems show ?case by - (rule steps_altI, auto intro!: interp.prod_complete)
  qed

  lemma prod_correct:
    "prod_ta ⊢ ⟨(L, s), u⟩ →* ⟨(L', s'), u'⟩ ⟷ A ⊢ ⟨L, s, u⟩ →* ⟨L', s', u'⟩"
    by (metis prod_steps_complete prod_steps_sound)

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

end (* End of theory *)