Theory Simple_Network_Language

theory Simple_Network_Language
  imports Main
    Munta_Model_Checker.State_Networks
    Munta_Model_Checker.UPPAAL_State_Networks_Impl
    FinFun.FinFun
    Simple_Expressions
    Munta_Tagging
begin

section ‹Simple Networks of Automata With Broadcast Channels and Committed Locations›

no_notation top_assn ("true")

abbreviation concat_map where
  "concat_map f xs ≡ concat (map f xs)"


type_synonym
  ('c, 't, 's) invassn = "'s ⇒ ('c, 't) cconstraint"

type_synonym
  ('a, 's, 'c, 't, 'x, 'v) transition =
  "'s × ('x, 'v) bexp × ('c, 't) cconstraint × 'a × ('x, 'v) upd × 'c list × 's"

type_synonym
  ('a, 's, 'c, 't, 'x, 'v) sta =
  "'s set × 's set × ('a, 's, 'c, 't, 'x, 'v) transition set × ('c, 't, 's) invassn"

type_synonym
  ('a, 's, 'c, 't, 'x, 'v) nta = "'a set × ('a act, 's, 'c, 't, 'x, 'v) sta list × ('x ⇀ 'v * 'v)"

context begin

qualified definition conv_t where "conv_t ≡ λ (l,b,g,a,f,r,l'). (l,b,conv_cc g,a,f,r,l')"

qualified definition conv_A where "conv_A ≡ λ (C, U, T, I). (C, U, conv_t ` T, conv_cc o I)"

definition conv where
  "conv ≡ λ(broadcast, automata, bounds). (broadcast, map conv_A automata, bounds)"

end

datatype 'b label = Del | Internal 'b | Bin 'b | Broad 'b

definition bounded where
  "bounded bounds s ≡ dom s = dom bounds ∧
    (∀x ∈ dom s. fst (the (bounds x)) ≤ the (s x) ∧ the (s x) ≤ snd (the (bounds x)))"

definition committed :: "('a, 's, 'c, 't, 'x, 'v) sta ⇒ 's set" where
  "committed A ≡ fst A"

definition urgent :: "('a, 's, 'c, 't, 'x, 'v) sta ⇒ 's set" where
  "urgent A ≡ fst (snd A)"

definition trans :: "('a, 's, 'c, 't, 'x, 'v) sta ⇒ ('a, 's, 'c, 't, 'x, 'v) transition set"
  where
  "trans A ≡ fst (snd (snd A))"

definition inv :: "('a, 's, 'c, 't, 'x, 'v) sta ⇒ ('c, 't, 's) invassn" where
  "inv A ≡ snd (snd (snd A))"

no_notation step_sn ("_ ⊢ ⟨_, _, _⟩ →⇘_⇙ ⟨_, _, _⟩" [61,61,61,61,61] 61)
no_notation steps_sn ("_ ⊢ ⟨_, _, _⟩ →* ⟨_, _, _⟩" [61, 61, 61,61,61] 61)

datatype 'a tag = ANY 'a | TRANS 'a | SEL 'a | SEND 'a | RECV 'a

inductive step_u ::
  "('a, 's, 'c, 't :: time, 'x, 'v :: linorder) nta ⇒ 's list ⇒ ('x ⇀ 'v) ⇒ ('c, 't) cval
  ⇒ 'a label ⇒ 's list ⇒ ('x ⇀ 'v) ⇒ ('c, 't) cval ⇒ bool"
("_ ⊢ ⟨_, _, _⟩ →⇘_⇙ ⟨_, _, _⟩" [61,61,61,61,61] 61)
where
  step_t:
    "⟦
      ''target invariant'' ¦ ∀p < length N. u ⊕ d ⊢ inv (N ! p) (L ! p);
      ''nonnegative''      ¦ d ≥ 0;
      ''urgent''           ¦ (∃p < length N. L ! p ∈ urgent (N ! p)) ⟶ d = 0;
      ''bounded''          ¦ bounded B s
     ⟧
    ⟹ (broadcast, N, B) ⊢ ⟨L, s, u⟩ →⇘Del⇙ ⟨L, s, u ⊕ d⟩" |
  step_int:
    "⟦
      TRANS ''silent'' ¦ (l, b, g, Sil a, f, r, l') ∈ trans (N ! p);
      ''committed'' ¦ l ∈ committed (N ! p) ∨ (∀p < length N. L ! p ∉ committed (N ! p));
      ''bexp''      ¦ check_bexp s b True;
      ''guard''     ¦ u ⊢ g;
      ''target invariant'' ¦ ∀p < length N. u' ⊢ inv (N ! p) (L' ! p);
      ''loc''           ¦ L!p = l;
      ''range''         ¦ p < length L;
      ''new loc''       ¦ L' = L[p := l'];
      ''new valuation'' ¦ u' = [r→0]u;
      ''is_upd''        ¦ is_upds s f s';
      ''bounded''       ¦ bounded B s'
    ⟧
    ⟹ (broadcast, N, B) ⊢ ⟨L, s, u⟩ →⇘Internal a⇙ ⟨L', s', u'⟩" |
  step_bin:
    "⟦
      ''not broadcast'' ¦ (a ∉ broadcast);
      TRANS ''in''  ¦ (l1, b1, g1, In a,  f1, r1, l1') ∈ trans (N ! p);
      TRANS ''out'' ¦ (l2, b2, g2, Out a, f2, r2, l2') ∈ trans (N ! q);
      ''committed'' ¦
        l1 ∈ committed (N ! p) ∨ l2 ∈ committed (N ! q) ∨ (∀p < length N. L ! p ∉ committed (N ! p));
      ''bexp'' ¦ check_bexp s b1 True; ''bexp'' ¦ check_bexp s b2 True;
      ''guard'' ¦ u ⊢ g1; ''guard'' ¦ u ⊢ g2;
      ''target invariant'' ¦ ∀p < length N. u' ⊢ inv (N ! p) (L' ! p);
      RECV ''loc'' ¦ L!p = l1; SEND ''loc'' ¦ L!q = l2;
      RECV ''range'' ¦ p < length L; SEND ''range'' ¦ q < length L;
      ''different'' ¦ p ≠ q;
      ''new loc''       ¦ L' = L[p := l1', q := l2'];
      ''new valuation'' ¦ u' = [r1@r2→0]u;
      ''upd'' ¦ is_upds s f1 s'; ''upd'' ¦ is_upds s' f2 s'';
      ''bounded'' ¦ bounded B s''
    ⟧
    ⟹ (broadcast, N, B) ⊢ ⟨L, s, u⟩ →⇘Bin a⇙ ⟨L', s'', u'⟩" |
  step_broad:
    "⟦
      ''broadcast'' ¦ a ∈ broadcast;
      TRANS ''out'' ¦ (l, b, g, Out a, f, r, l') ∈ trans (N ! p);
      TRANS ''in''  ¦ (∀p ∈ set ps. (L ! p, bs p, gs p, In a, fs p, rs p, ls' p) ∈ trans (N ! p));
      ''committed'' ¦ (l ∈ committed (N ! p) ∨ (∃p ∈ set ps. L ! p ∈ committed (N ! p))
      ∨ (∀p < length N. L ! p ∉ committed (N ! p)));
      ''bexp''    ¦ check_bexp s b True;
      ''bexp''    ¦ ∀p ∈ set ps. check_bexp s (bs p) True;
      ''guard''   ¦ u ⊢ g;
      ''guard''   ¦ ∀p ∈ set ps. u ⊢ gs p;
      ''maximal'' ¦ ∀q < length N. q ∉ set ps ∧ p ≠ q
        ⟶ (∀b g f r l'. (L!q, b, g, In a, f, r, l') ∈ trans (N ! q)
        ⟶ ¬ check_bexp s b True ∨ ¬ u ⊢ g);
      ''target invariant'' ¦ ∀p < length N. u' ⊢ inv (N ! p) (L' ! p);
      SEND ''loc''       ¦ L!p = l;
      SEND ''range''     ¦ p < length L;
      SEL ''range''      ¦ set ps ⊆ {0..<length N};
      SEL ''not sender'' ¦ p ∉ set ps;
      SEL ''distinct''   ¦ distinct ps;
      SEL ''sorted''     ¦ sorted ps;
      ''new loc'' ¦ L' = (fold (λp L . L[p := ls' p]) ps L)[p := l'];
      ''new valuation'' ¦ u' = [r@concat (map rs ps)→0]u;
      ''upd''     ¦ is_upds s f s';
      ''upds''    ¦ is_upds s' (concat_map fs ps) s'';
      ''bounded'' ¦ bounded B s''
    ⟧
    ⟹ (broadcast, N, B) ⊢ ⟨L, s, u⟩ →⇘Broad a⇙ ⟨L', s'', u'⟩"
lemmas [intro?] = step_u.intros[unfolded TAG_def]

text ‹Comments:
▪ Should there be an error transition + state if states run of bounds or updates are undefined?
Then one could run a reachability check for the error state.
▪ Should the state be total?
▪ Note that intermediate states are allowed to run out of bounds
›

definition steps_u ::
  "('a, 's, 'c, 't :: time, 'x, 'v :: linorder) nta ⇒ 's list ⇒ ('x ⇀ 'v) ⇒ ('c, 't) cval
  ⇒ 's list ⇒ ('x ⇀ 'v) ⇒ ('c, 't) cval ⇒ bool"
("_ ⊢ ⟨_, _, _⟩ →* ⟨_, _, _⟩" [61,61,61,61,61] 61)
where
  "A ⊢ ⟨L, s, u⟩ →* ⟨L', s', u'⟩ ≡
    (λ (L, s, u) (L', s', u'). ∃a. A ⊢ ⟨L, s, u⟩ →⇘a⇙ ⟨L', s', u'⟩)⇧*⇧* (L, s, u) (L', s', u')"

paragraph ‹Misc›

lemma clock_val_concat_iff:
  ‹u ⊢ concat gs ⟷ (∀g ∈ set gs. u ⊢ g)›
  by (auto intro: guard_concat concat_guard)

lemma clock_val_append_iff:
  ‹u ⊢ g1 @ g2 ⟷ u ⊢ g1 ∧ u ⊢ g2›
proof -
  have "u ⊢ g1 @ g2 ⟷ u ⊢ concat [g1, g2]"
    by simp
  also have "... ⟷ u ⊢ g1 ∧ u ⊢ g2"
    unfolding clock_val_concat_iff by simp
  finally show ?thesis .
qed


subsection ‹Product Construction›

locale Prod_TA_Defs =
  fixes A :: "('a, 's, 'c, 't, 'x, 'v :: linorder) nta"
begin

definition
  "broadcast = fst A"

definition
  "N i = fst (snd A) ! i"

definition
  "bounds = snd (snd A)"

definition ―‹Number of processes›
  "n_ps = length (fst (snd A))"

definition states  :: "'s list set" where
  "states ≡ {L. length L = n_ps ∧
    (∀ i. i < n_ps ⟶ L ! i ∈ (⋃ (l, e, g, a, r, u, l') ∈ (trans (N i)). {l, l'}))}"

definition
  "prod_inv ≡ λ(L, s). if L ∈ states then concat (map (λi. inv (N i) (L ! i)) [0..<n_ps]) else []"

definition
  "trans_int =
    {((L, s), g, Internal a, r, (L', s')) | L s l b g f p a r l' L' s'.
      (l, b, g, Sil a, f, r, l') ∈ trans (N p) ∧
      (l ∈ committed (N p) ∨ (∀p < n_ps. L ! p ∉ committed (N p))) ∧
      L!p = l ∧ p < length L ∧ L' = L[p := l'] ∧ is_upds s f s' ∧ check_bexp s b True ∧
      L ∈ states ∧ bounded bounds s ∧ bounded bounds s'
    }"

definition
  "trans_bin =
    {((L, s), g1 @ g2, Bin a, r1 @ r2, (L', s'')) |
      L s L' s' s'' a p q l1 b1 g1 f1 r1 l1' l2 b2 g2 f2 r2 l2'.
      a ∉ broadcast ∧
      (l1, b1, g1, In a,  f1, r1, l1') ∈ trans (N p) ∧
      (l2, b2, g2, Out a, f2, r2, l2') ∈ trans (N q) ∧
      (l1 ∈ committed (N p) ∨ l2 ∈ committed (N q) ∨ (∀p < n_ps. L ! p ∉ committed (N p))) ∧
      L!p = l1 ∧ L!q = l2 ∧ p < length L ∧ q < length L ∧ p ≠ q ∧
      check_bexp s b1 True ∧ check_bexp s b2 True ∧
      L' = L[p := l1', q := l2'] ∧ is_upds s f1 s' ∧ is_upds s' f2 s'' ∧
      L ∈ states ∧ bounded bounds s ∧ bounded bounds s''
    }"

definition
  "trans_broad =
    {((L, s), g @ concat (map gs ps), Broad a, r @ concat (map rs ps), (L', s'')) |
    L s L' s' s'' a p l b g f r l' bs gs fs rs ls' ps.
      a ∈ broadcast  ∧
      (l, b, g, Out a, f, r, l') ∈ trans (N p) ∧
      (∀p ∈ set ps. (L ! p, bs p, gs p, In a, fs p, rs p, ls' p) ∈ trans (N p)) ∧
      (l ∈ committed (N p) ∨ (∃p ∈ set ps. L ! p ∈ committed (N p))
      ∨ (∀p < n_ps. L ! p ∉ committed (N p))) ∧
      (∀q < n_ps. q ∉ set ps ∧ p ≠ q ⟶
        ¬ (∃b g f r l'. (L!q, b, g, In a, f, r, l') ∈ trans (N q) ∧ check_bexp s b True)) ∧
      L!p = l ∧
      p < length L ∧ set ps ⊆ {0..<n_ps} ∧ p ∉ set ps ∧ distinct ps ∧ sorted ps ∧
      check_bexp s b True ∧ (∀p ∈ set ps. check_bexp s (bs p) True) ∧
      L' = (fold (λp L . L[p := ls' p]) ps L)[p := l'] ∧
      is_upds s f s' ∧ is_upds s' (concat_map fs ps) s'' ∧
      L ∈ states ∧ bounded bounds s ∧ bounded bounds s''
    }"

definition
  "trans_prod = trans_int ∪ trans_bin ∪ trans_broad"

definition
  "prod_ta = (trans_prod, prod_inv :: ('s list × ('x ⇒ 'v option) ⇒ _))"

lemma inv_of_prod[simp]:
  "inv_of prod_ta = prod_inv"
  unfolding prod_ta_def inv_of_def by simp

lemma trans_of_prod[simp]:
  "trans_of prod_ta = trans_prod"
  unfolding prod_ta_def trans_of_def by simp

lemma A_split:
  ‹A = (broadcast, map N [0..<n_ps], bounds)›
  unfolding broadcast_def N_def bounds_def n_ps_def by (cases A) (simp add: List.map_nth)

lemma map_N_n_ps_simp:
  "map N [0..<n_ps] ! p = N p"
  unfolding N_def n_ps_def List.map_nth ..

lemma N_split_simp[simp]:
  assumes "A = (broadcast', N', B)"
  shows "N' ! i = N i"
  unfolding N_def unfolding assms by simp

lemma state_preservation_updI:
  assumes "l' ∈ (⋃ (l, b, g, a, r, u, l') ∈ trans (N p). {l, l'})" "L ∈ states"
  shows "L[p := l'] ∈ states"
  using assms unfolding states_def by (fastforce simp: nth_list_update')

lemma state_preservation_fold_updI:
  assumes "∀p ∈ set ps. ls' p ∈ (⋃ (l, b, g, a, r, u, l') ∈ trans (N p). {l, l'})" "L ∈ states"
  shows "fold (λp L. L[p := ls' p]) ps L ∈ states"
  using assms by (induction ps arbitrary: L) (auto intro: state_preservation_updI)

lemma state_set_states:
  "Simulation_Graphs_TA.state_set prod_ta ⊆ {(l, s). l ∈ states}"
  unfolding prod_ta_def state_set_def
  unfolding trans_of_def trans_prod_def
  unfolding trans_int_def trans_bin_def trans_broad_def
  by auto (auto intro: state_preservation_updI state_preservation_fold_updI)

lemma trans_prod_bounded_inv:
  ‹bounded bounds s'› if ‹((L, s), g, a, r, (L', s')) ∈ trans_prod›
  using that unfolding bounds_def trans_prod_def trans_int_def trans_bin_def trans_broad_def
  by (auto simp: bounds_def)

lemma trans_prod_states_inv:
  ‹L' ∈ states› if ‹((L, s), g, a, r, (L', s')) ∈ trans_prod› ‹L ∈ states›
  using that
  unfolding bounds_def trans_prod_def trans_int_def trans_bin_def trans_broad_def
  apply clarsimp
  apply safe
         apply (force intro!: state_preservation_updI)
        apply (force intro!: state_preservation_updI)
       apply (force intro!: state_preservation_updI)
      apply (force intro!: state_preservation_updI)
     apply (force intro!: state_preservation_updI)
    apply (fastforce intro!: state_preservation_updI state_preservation_fold_updI)
  subgoal
    apply (rule state_preservation_updI)
    apply force
    apply (force intro!: state_preservation_fold_updI)
    done
  apply (fastforce intro!: state_preservation_updI state_preservation_fold_updI)
  done

end (* Prod TA Defs *)


locale Prod_TA_sem =
  Prod_TA_Defs A for A :: "('a, 's, 'c, 't :: time, 'x, 'v :: linorder) nta"
begin

lemma prod_invI[intro]:
  ‹u ⊢ prod_inv (L, s)› if ‹∀p<n_ps. u ⊢ Simple_Network_Language.inv (N p) (L ! p)›
  using that unfolding prod_inv_def by (auto intro!: guard_concat)

lemma prod_invD[dest]:
  ‹∀p<n_ps. u ⊢ Simple_Network_Language.inv (N p) (L ! p)› if ‹u ⊢ prod_inv (L, s)› ‹L ∈ states›
  using that unfolding prod_inv_def by (auto elim: concat_guard)

lemma delay_sound:
  assumes "prod_ta ⊢ ⟨(L, s), u⟩ →⇗d⇖ ⟨(L', s'), u'⟩" "L ∈ states" "bounded bounds s"
          "∀N ∈ set (fst (snd A)). urgent N = {}"
        shows "A ⊢ ⟨L, s, u⟩ →⇘Del⇙ ⟨L', s', u'⟩"
proof -
  from assms(4) have "l ∉ urgent (N p)" if "p < n_ps" for p l
    using that unfolding N_def n_ps_def by auto
  then show ?thesis
    by (subst A_split) (use assms in ‹cases, auto intro!: step_t simp: TAG_def›)
qed

lemma action_sound:
  "A ⊢ ⟨L, s, u⟩ →⇘a⇙ ⟨L', s', u'⟩" if "prod_ta ⊢ ⟨(L, s), u⟩ →⇘a⇙ ⟨(L', s'), u'⟩"
  using that
proof cases
  case prems: (1 g r)
  note [simp add] = map_N_n_ps_simp clock_val_append_iff clock_val_concat_iff
  from ‹prod_ta ⊢ (L, s) ⟶⇗g,a,r⇖ (L', s')›[THEN state_setI2] have "L' ∈ states"
    using state_set_states that by fast
  from ‹prod_ta ⊢ (L, s) ⟶⇗g,a,r⇖ (L', s')› show ?thesis
    unfolding trans_of_prod trans_prod_def
  proof safe
    assume "((L, s), g, a, r, L', s') ∈ trans_int"
    then show "A ⊢ ⟨L, s, u⟩ →⇘a⇙ ⟨L', s', u'⟩"
      unfolding trans_int_def
      apply clarsimp
      using prems ‹L' ∈ _›
      by (subst A_split) (intro step_int; simp add: TAG_def; elim prod_invD; assumption)
  next
    assume "((L, s), g, a, r, L', s') ∈ trans_bin"
    then show "A ⊢ ⟨L, s, u⟩ →⇘a⇙ ⟨L', s', u'⟩"
      unfolding trans_bin_def
      using prems ‹L' ∈ _›
      apply clarsimp
      apply (subst A_split, standard)
                     apply (assumption | simp; elim prod_invD; assumption)+
      done
  next
    assume "((L, s), g, a, r, L', s') ∈ trans_broad"
    then show "A ⊢ ⟨L, s, u⟩ →⇘a⇙ ⟨L', s', u'⟩"
      using prems ‹L' ∈ _›
      unfolding trans_broad_def inv_of_prod
      apply clarsimp
      apply (subst A_split)
      apply standard
      apply (simp; elim prod_invD; assumption)+
      apply fastforce+
      done
  qed
qed

lemma bounded_inv:
  ‹bounded bounds s'› if ‹A ⊢ ⟨L, s, u⟩ →⇘a⇙ ⟨L', s', u'⟩›
  using that unfolding bounds_def by cases (simp add: TAG_def)+

lemma states_inv:
  ‹L' ∈ states› if ‹A ⊢ ⟨L, s, u⟩ →⇘a⇙ ⟨L', s', u'⟩› ‹L ∈ states›
  using that unfolding bounds_def
proof cases
  case (step_t N d B broadcast)
  with ‹L ∈ states› show ?thesis
    by simp
next
  case prems[unfolded TAG_def]: (step_int l b g a f r l' N' p B broadcast)
  from ‹A = _› prems(3) have "l' ∈ (⋃ (l, b, g, a, r, u, l') ∈ trans (N p). {l, l'})"
    by force
  with ‹L ∈ states› show ?thesis
    unfolding ‹L' = _› by (intro state_preservation_updI)
next
  case prems[unfolded TAG_def]:
    (step_bin broadcast a l1 b1 g1 f1 r1 l1' N' p l2 b2 g2 f2 r2 l2' q s' B)
  from ‹A = _› prems(4, 5) have
    "l1' ∈ (⋃ (l, b, g, a, r, u, l') ∈ trans (N p). {l, l'})"
    "l2' ∈ (⋃ (l, b, g, a, r, u, l') ∈ trans (N q). {l, l'})"
    by force+
  with ‹L ∈ states› show ?thesis
    unfolding ‹L' = _› by (intro state_preservation_updI)
next
  case prems[unfolded TAG_def]: (step_broad a broadcast l b g f r l' N' p ps bs gs fs rs ls' s' B)
  from ‹A = _› prems(4, 5) have
    "l' ∈ (⋃ (l, b, g, a, r, u, l') ∈ trans (N p). {l, l'})"
    "∀ q ∈ set ps. ls' q ∈ (⋃ (l, b, g, a, r, u, l') ∈ trans (N q). {l, l'})"
    by force+
  with ‹L ∈ states› show ?thesis
    unfolding ‹L' = _› by (intro state_preservation_updI state_preservation_fold_updI)
qed

end (* Prod TA Defs on a time domain *)


locale Prod_TA =
  Prod_TA_sem A for A :: "('a, 's, 'c, 't :: time, 'x, 'v :: linorder) nta" +
  assumes broadcast_receivers_unguarded:
    "∀p < n_ps. ∀l b g a f r l'. (l, b, g, In a, f, r, l') ∈ trans (N p) ∧ a ∈ broadcast ⟶ g = []"
begin

lemma action_complete:
  "prod_ta ⊢ ⟨(L, s), u⟩ →⇘a⇙ ⟨(L', s'), u'⟩"
  if "A ⊢ ⟨L, s, u⟩ →⇘a⇙ ⟨L', s', u'⟩" "a ≠ Del" "L ∈ states" "bounded bounds s"
using that(1) proof cases
  case (step_t N d B broadcast)
  then show ?thesis
    using that(2) by auto
next
  case prems[unfolded TAG_def]: (step_int l b g a' f r l' N' p B broadcast')
  have [simp]:
    "B = bounds" "broadcast' = broadcast" "length N' = n_ps"
    unfolding bounds_def broadcast_def n_ps_def unfolding prems(1) by simp+
  have [simp]:
    "N' ! i = N i" for i
    unfolding N_def unfolding prems(1) by simp
  have "prod_ta ⊢ (L, s) ⟶⇗g,Internal a',r⇖ (L', s')"
  proof -
    from prems ‹L ∈ states› ‹bounded _ s› have "((L, s),g,Internal a',r,(L', s')) ∈ trans_int"
      unfolding trans_int_def
      by simp (rule exI conjI HOL.refl | assumption | (simp; fail))+
    then show ?thesis
      unfolding prod_ta_def trans_of_def trans_prod_def by simp
  qed
  moreover have "u ⊢ g"
    by (rule prems)
  moreover have "u' ⊢ inv_of prod_ta (L', s')"
    using prems(7) by auto
  moreover have "u' = [r→0]u"
    by (rule prems)
  ultimately show ?thesis
    unfolding ‹a = _› ..
next
  case prems[unfolded TAG_def]:
    (step_bin a' broadcast' l1 b1 g1 f1 r1 l1' N' p l2 b2 g2 f2 r2 l2' q s'' B)
  have [simp]:
    "B = bounds" "broadcast' = broadcast" "length N' = n_ps"
    unfolding bounds_def broadcast_def n_ps_def unfolding prems(1) by simp+
  have [simp]:
    "N' ! i = N i" for i
    unfolding N_def unfolding prems(1) by simp
  have "prod_ta ⊢ (L, s) ⟶⇗g1 @ g2,Bin a',r1 @ r2⇖ (L', s')"
  proof -
    from prems ‹L ∈ states› ‹bounded bounds s› have
      "((L, s),g1 @ g2,Bin a',r1 @ r2,(L', s')) ∈ trans_bin"
      unfolding trans_bin_def
      using [[simproc add: ex_reorder4]]
      by simp (rule exI conjI HOL.refl | assumption | fast)+
    then show ?thesis
      unfolding prod_ta_def trans_of_def trans_prod_def by simp
  qed
  moreover have "u ⊢ g1 @ g2"
    using ‹u ⊢ g1› ‹u ⊢ g2› by (rule guard_append)
  moreover have "u' ⊢ inv_of prod_ta (L', s')"
    using prems by auto
  moreover have "u' = [r1@r2→0]u"
    by (rule prems)
  ultimately show ?thesis
    unfolding ‹a = _› ..
next
  case prems[unfolded TAG_def]: (step_broad a' broadcast' l b g f r l' N' p ps bs gs fs rs ls' s'' B)
  have [simp]:
    "B = bounds" "broadcast' = broadcast" "length N' = n_ps"
    unfolding bounds_def broadcast_def n_ps_def unfolding prems(1) by simp+
  have [simp]:
    "N' ! i = N i" for i
    unfolding N_def unfolding prems(1) by simp
  let ?r = "r @ concat (map rs ps)" and ?g = "g @ concat (map gs ps)"
  have "prod_ta ⊢ (L, s) ⟶⇗?g,Broad a',?r⇖ (L', s')"
  proof -
    have *: "¬ u ⊢ g ⟷ False" if
      "p < n_ps" "(l, b, g, In a', f, r, l') ∈ Simple_Network_Language.trans (N p)"
      "a' ∈ broadcast"
      for l b g a' f r l' p
    proof -
      from that broadcast_receivers_unguarded have ‹g = []›
        by blast
      then show ?thesis
        by auto
    qed
    from prems ‹L ∈ states› ‹bounded bounds s› have "((L, s),?g,Broad a',?r,(L', s')) ∈ trans_broad"
      unfolding trans_broad_def
      by clarsimp
         (intro exI conjI HOL.refl; (rule HOL.refl | assumption | fastforce simp: *))
   then show ?thesis
      unfolding prod_ta_def trans_of_def trans_prod_def by simp
  qed
  moreover have "u ⊢ ?g"
    using prems by (auto intro!: guard_append guard_concat)
  moreover have "u' ⊢ inv_of prod_ta (L', s')"
    using prems by auto
  moreover have "u' = [?r→0]u"
    by (rule prems)
  ultimately show ?thesis
    unfolding ‹a = _› ..
qed

lemma delay_complete:
  assumes "A ⊢ ⟨L, s, u⟩ →⇘Del⇙ ⟨L', s', u'⟩"
  obtains d where "prod_ta ⊢ ⟨(L, s), u⟩ →⇗d⇖ ⟨(L', s'), u'⟩"
  using assms
proof cases
  case prems: (step_t N' d B broadcast)
  have [simp]:
    "length N' = n_ps"
    unfolding n_ps_def unfolding prems(1) by simp+
  have [simp]:
    "N' ! i = N i" for i
    unfolding N_def unfolding prems(1) by simp
  from prems show ?thesis
  by (intro that[of d]; unfold ‹u' = _› ‹L' = L› ‹s' = s› TAG_def)
     (rule step_t.intros; (unfold inv_of_prod; rule prod_invI)?; simp)
qed

lemma step_iff:
  "(∃ a. A ⊢ ⟨L, s, u⟩ →⇘a⇙ ⟨L', s', u'⟩) ⟷ prod_ta ⊢ ⟨(L, s), u⟩ → ⟨(L', s'), u'⟩"
  if "bounded bounds s" "L ∈ states" "∀N ∈ set (fst (snd A)). urgent N = {}"
  using that(1,2)
  apply safe
  subgoal for a
    by (cases a; blast dest: action_complete elim: delay_complete)
  by (auto intro: action_sound delay_sound[OF _ _ _ that(3)])

end (* Prod TA *)

end (* Theory *)