Theory AWN_SOS

(*  Title:       AWN_SOS.thy
    License:     BSD 2-Clause. See LICENSE.
    Author:      Timothy Bourke
*)

section "Semantics of the Algebra of Wireless Networks"

theory AWN_SOS
imports TransitionSystems AWN
begin

subsection "Table 1: Structural operational semantics for sequential process expressions "

inductive_set
  seqp_sos
  :: "('s, 'm, 'p, 'l) seqp_env ⇒ ('s × ('s, 'm, 'p, 'l) seqp, 'm seq_action) transition set"
  for Γ :: "('s, 'm, 'p, 'l) seqp_env"
where
    broadcastT: "((ξ, {l}broadcast(s⇩m⇩s⇩g).p),          broadcast (s⇩m⇩s⇩g ξ),         (ξ, p)) ∈ seqp_sos Γ"
  | groupcastT: "((ξ, {l}groupcast(s⇩i⇩p⇩s, s⇩m⇩s⇩g).p),    groupcast (s⇩i⇩p⇩s ξ) (s⇩m⇩s⇩g ξ), (ξ, p)) ∈ seqp_sos Γ"
  | unicastT:   "((ξ, {l}unicast(s⇩i⇩p, s⇩m⇩s⇩g).p ▹ q),   unicast (s⇩i⇩p ξ) (s⇩m⇩s⇩g ξ),    (ξ, p)) ∈ seqp_sos Γ"
  | notunicastT:"((ξ, {l}unicast(s⇩i⇩p, s⇩m⇩s⇩g).p ▹ q),    ¬unicast (s⇩i⇩p ξ),          (ξ, q)) ∈ seqp_sos Γ"
  | sendT:      "((ξ, {l}send(s⇩m⇩s⇩g).p),               send (s⇩m⇩s⇩g ξ),              (ξ, p)) ∈ seqp_sos Γ"
  | deliverT:   "((ξ, {l}deliver(s⇩d⇩a⇩t⇩a).p),           deliver (s⇩d⇩a⇩t⇩a ξ),          (ξ, p)) ∈ seqp_sos Γ"
  | receiveT:   "((ξ, {l}receive(u⇩m⇩s⇩g).p),            receive msg,       (u⇩m⇩s⇩g msg ξ, p)) ∈ seqp_sos Γ"
  | assignT:    "((ξ, {l}⟦u⟧ p),                      τ,                        (u ξ, p)) ∈ seqp_sos Γ"

  | callT:      "⟦ ((ξ, Γ pn), a, (ξ', p')) ∈ seqp_sos Γ ⟧ ⟹
                 ((ξ, call(pn)), a, (ξ', p')) ∈ seqp_sos Γ" (* TPB: quite different to Table 1 *)

  | choiceT1:   "((ξ, p), a, (ξ', p')) ∈ seqp_sos Γ  ⟹ ((ξ, p ⊕ q), a, (ξ', p')) ∈ seqp_sos Γ"
  | choiceT2:   "((ξ, q), a, (ξ', q')) ∈ seqp_sos Γ  ⟹ ((ξ, p ⊕ q), a, (ξ', q')) ∈ seqp_sos Γ"

  | guardT:     "ξ' ∈ g ξ ⟹ ((ξ, {l}⟨g⟩ p), τ, (ξ', p)) ∈ seqp_sos Γ"

inductive_cases
      seqp_callTE [elim]:      "((ξ, call(pn)), a, (ξ', q)) ∈ seqp_sos Γ"
  and seqp_choiceTE [elim]:    "((ξ, p1 ⊕ p2), a, (ξ', q)) ∈ seqp_sos Γ"

lemma seqp_broadcastTE [elim]:
  "⟦((ξ, {l}broadcast(s⇩m⇩s⇩g). p), a, (ξ', q)) ∈ seqp_sos Γ;
    ⟦a = broadcast (s⇩m⇩s⇩g ξ); ξ' = ξ; q = p⟧ ⟹ P⟧ ⟹ P"
  by (ind_cases "((ξ, {l}broadcast(s⇩m⇩s⇩g). p), a, (ξ', q)) ∈ seqp_sos Γ") simp

lemma seqp_groupcastTE [elim]:
  "⟦((ξ, {l}groupcast(s⇩i⇩p⇩s, s⇩m⇩s⇩g). p), a, (ξ', q)) ∈ seqp_sos Γ;
    ⟦a = groupcast (s⇩i⇩p⇩s ξ) (s⇩m⇩s⇩g ξ); ξ' = ξ; q = p⟧ ⟹ P⟧ ⟹ P"
  by (ind_cases "((ξ, {l}groupcast(s⇩i⇩p⇩s, s⇩m⇩s⇩g). p), a, (ξ', q)) ∈ seqp_sos Γ") simp

lemma seqp_unicastTE [elim]:
  "⟦((ξ, {l}unicast(s⇩i⇩p, s⇩m⇩s⇩g). p ▹ q), a, (ξ', r)) ∈ seqp_sos Γ;
    ⟦a = unicast (s⇩i⇩p ξ) (s⇩m⇩s⇩g ξ); ξ' = ξ; r = p⟧ ⟹ P;
    ⟦a = ¬unicast (s⇩i⇩p ξ); ξ' = ξ; r = q⟧ ⟹ P⟧ ⟹ P"
  by (ind_cases "((ξ, {l}unicast(s⇩i⇩p, s⇩m⇩s⇩g). p ▹ q), a, (ξ', r)) ∈ seqp_sos Γ") simp_all

lemma seqp_sendTE [elim]:
  "⟦((ξ, {l}send(s⇩m⇩s⇩g). p), a, (ξ', q)) ∈ seqp_sos Γ;
    ⟦a = send (s⇩m⇩s⇩g ξ); ξ' = ξ; q = p⟧ ⟹ P⟧ ⟹ P"
  by (ind_cases "((ξ, {l}send(s⇩m⇩s⇩g). p), a, (ξ', q)) ∈ seqp_sos Γ") simp

lemma seqp_deliverTE [elim]:
  "⟦((ξ, {l}deliver(s⇩d⇩a⇩t⇩a). p), a, (ξ', q)) ∈ seqp_sos Γ;
    ⟦a = deliver (s⇩d⇩a⇩t⇩a ξ); ξ' = ξ; q = p⟧ ⟹ P⟧ ⟹ P"
  by (ind_cases "((ξ, {l}deliver(s⇩d⇩a⇩t⇩a). p), a, (ξ', q)) ∈ seqp_sos Γ") simp

lemma seqp_receiveTE [elim]:
  "⟦((ξ, {l}receive(u⇩m⇩s⇩g). p), a, (ξ', q)) ∈ seqp_sos Γ;
    ⋀msg. ⟦a = receive msg; ξ' = u⇩m⇩s⇩g msg ξ; q = p⟧ ⟹ P⟧ ⟹ P"
  by (ind_cases "((ξ, {l}receive(u⇩m⇩s⇩g). p), a, (ξ', q)) ∈ seqp_sos Γ") simp

lemma seqp_assignTE [elim]:
  "⟦((ξ, {l}⟦u⟧ p), a, (ξ', q)) ∈ seqp_sos Γ; ⟦a = τ; ξ' = u ξ; q = p⟧ ⟹ P⟧ ⟹ P"
  by (ind_cases "((ξ, {l}⟦u⟧ p), a, (ξ', q)) ∈ seqp_sos Γ") simp

lemma seqp_guardTE [elim]:
  "⟦((ξ, {l}⟨g⟩ p), a, (ξ', q)) ∈ seqp_sos Γ; ⟦a = τ; ξ' ∈ g ξ; q = p⟧ ⟹ P⟧ ⟹ P"
  by (ind_cases "((ξ, {l}⟨g⟩ p), a, (ξ', q)) ∈ seqp_sos Γ") simp

lemmas seqpTEs =
  seqp_broadcastTE
  seqp_groupcastTE
  seqp_unicastTE
  seqp_sendTE
  seqp_deliverTE
  seqp_receiveTE
  seqp_assignTE
  seqp_callTE
  seqp_choiceTE
  seqp_guardTE

declare seqp_sos.intros [intro]

subsection "Table 2: Structural operational semantics for parallel process expressions "

inductive_set
  parp_sos :: "('s1, 'm seq_action) transition set
                    ⇒ ('s2, 'm seq_action) transition set
                    ⇒ ('s1 × 's2, 'm seq_action) transition set"
  for S :: "('s1, 'm seq_action) transition set"
  and T :: "('s2, 'm seq_action) transition set"
where
    parleft:  "⟦ (s, a, s') ∈ S; ⋀m. a ≠ receive m ⟧ ⟹ ((s, t), a, (s', t)) ∈ parp_sos S T"
  | parright: "⟦ (t, a, t') ∈ T; ⋀m. a ≠ send m ⟧ ⟹ ((s, t), a, (s, t')) ∈ parp_sos S T"
  | parboth:  "⟦ (s, receive m, s') ∈ S; (t, send m, t') ∈ T ⟧
               ⟹((s, t), τ, (s', t')) ∈ parp_sos S T"

lemma par_broadcastTE [elim]:
  "⟦((s, t), broadcast m, (s', t')) ∈ parp_sos S T;
    ⟦(s, broadcast m, s') ∈ S; t' = t⟧ ⟹ P;
    ⟦(t, broadcast m, t') ∈ T; s' = s⟧ ⟹ P⟧ ⟹ P"
  by (ind_cases "((s, t), broadcast m, (s', t')) ∈ parp_sos S T") simp_all

lemma par_groupcastTE [elim]:
  "⟦((s, t), groupcast ips m, (s', t')) ∈ parp_sos S T;
    ⟦(s, groupcast ips m, s') ∈ S; t' = t⟧ ⟹ P;
    ⟦(t, groupcast ips m, t') ∈ T; s' = s⟧ ⟹ P⟧ ⟹ P"
  by (ind_cases "((s, t), groupcast ips m, (s', t')) ∈ parp_sos S T") simp_all

lemma par_unicastTE [elim]:
  "⟦((s, t), unicast i m, (s', t')) ∈ parp_sos S T;
    ⟦(s, unicast i m, s') ∈ S; t' = t⟧ ⟹ P;
    ⟦(t, unicast i m, t') ∈ T; s' = s⟧ ⟹ P⟧ ⟹ P"
  by (ind_cases "((s, t), unicast i m, (s', t')) ∈ parp_sos S T") simp_all

lemma par_notunicastTE [elim]:
  "⟦((s, t), notunicast i, (s', t')) ∈ parp_sos S T;
    ⟦(s, notunicast i, s') ∈ S; t' = t⟧ ⟹ P;
    ⟦(t, notunicast i, t') ∈ T; s' = s⟧ ⟹ P⟧ ⟹ P"
  by (ind_cases "((s, t), notunicast i, (s', t')) ∈ parp_sos S T") simp_all

lemma par_sendTE [elim]:
  "⟦((s, t), send m, (s', t')) ∈ parp_sos S T;
    ⟦(s, send m, s') ∈ S; t' = t⟧ ⟹ P⟧ ⟹ P"
  by (ind_cases "((s, t), send m, (s', t')) ∈ parp_sos S T") auto

lemma par_deliverTE [elim]:
  "⟦((s, t), deliver d, (s', t')) ∈ parp_sos S T;
    ⟦(s, deliver d, s') ∈ S; t' = t⟧ ⟹ P;
    ⟦(t, deliver d, t') ∈ T; s' = s⟧ ⟹ P⟧ ⟹ P"
  by (ind_cases "((s, t), deliver d, (s', t')) ∈ parp_sos S T") simp_all

lemma par_receiveTE [elim]:
  "⟦((s, t), receive m, (s', t')) ∈ parp_sos S T;
    ⟦(t, receive m, t') ∈ T; s' = s⟧ ⟹ P⟧ ⟹ P"
  by (ind_cases "((s, t), receive m, (s', t')) ∈ parp_sos S T") auto

inductive_cases par_tauTE: "((s, t), τ, (s', t')) ∈ parp_sos S T"

lemmas parpTEs =
  par_broadcastTE
  par_groupcastTE
  par_unicastTE
  par_notunicastTE
  par_sendTE
  par_deliverTE
  par_receiveTE

lemma parp_sos_cases [elim]:
  assumes "((s, t), a, (s', t')) ∈ parp_sos S T"
      and "⟦ (s, a, s') ∈ S; ⋀m. a ≠ receive m; t' = t ⟧ ⟹ P"
      and "⟦ (t, a, t') ∈ T; ⋀m. a ≠ send m; s' = s ⟧ ⟹ P"
      and "⋀m. ⟦ (s, receive m, s') ∈ S; (t, send m, t') ∈ T ⟧ ⟹ P"
    shows "P"
  using assms by cases auto

definition
  par_comp :: "('s1, 'm seq_action) automaton
              ⇒ ('s2, 'm seq_action) automaton
              ⇒ ('s1 × 's2, 'm seq_action) automaton"
  (‹(_ ⟨⟨ _)› [102, 103] 102)
where
  "s ⟨⟨ t ≡ ⦇ init = init s × init t, trans = parp_sos (trans s) (trans t) ⦈"

lemma trans_par_comp [simp]:
  "trans (s ⟨⟨ t) = parp_sos (trans s) (trans t)"
  unfolding par_comp_def by simp

lemma init_par_comp [simp]:
  "init (s ⟨⟨ t) = init s × init t"
  unfolding par_comp_def by simp

subsection "Table 3: Structural operational semantics for node expressions "

inductive_set
  node_sos :: "('s, 'm seq_action) transition set ⇒ ('s net_state, 'm node_action) transition set"
  for S :: "('s, 'm seq_action) transition set"
where
    node_bcast:
    "(s, broadcast m, s') ∈ S ⟹ (NodeS i s R, R:*cast(m), NodeS i s' R) ∈ node_sos S"
  | node_gcast:
    "(s, groupcast D m, s') ∈ S ⟹ (NodeS i s R, (R∩D):*cast(m), NodeS i s' R) ∈ node_sos S"
  | node_ucast:
    "⟦ (s, unicast d m, s') ∈ S; d∈R ⟧ ⟹ (NodeS i s R, {d}:*cast(m), NodeS i s' R) ∈ node_sos S"
  | node_notucast:
    "⟦ (s, ¬unicast d, s') ∈ S; d∉R ⟧ ⟹ (NodeS i s R, τ, NodeS i s' R) ∈ node_sos S"
  | node_deliver:
    "(s, deliver d, s') ∈ S ⟹ (NodeS i s R, i:deliver(d), NodeS i s' R) ∈ node_sos S"
  | node_receive:
    "(s, receive m, s') ∈ S ⟹ (NodeS i s R, {i}¬{}:arrive(m), NodeS i s' R) ∈ node_sos S"
  | node_tau:
    "(s, τ, s') ∈ S         ⟹ (NodeS i s R, τ, NodeS i s' R) ∈ node_sos S"
  | node_arrive:
    "(NodeS i s R, {}¬{i}:arrive(m),  NodeS i s R) ∈ node_sos S"
  | node_connect1:
    "(NodeS i s R, connect(i, i'),    NodeS i s (R ∪ {i'})) ∈ node_sos S"
  | node_connect2:
    "(NodeS i s R, connect(i', i),    NodeS i s (R ∪ {i'})) ∈ node_sos S"
  | node_disconnect1:
    "(NodeS i s R, disconnect(i, i'), NodeS i s (R - {i'})) ∈ node_sos S"
  | node_disconnect2:
    "(NodeS i s R, disconnect(i', i), NodeS i s (R - {i'})) ∈ node_sos S"
  | node_connect_other:
    "⟦ i ≠ i'; i ≠ i'' ⟧ ⟹ (NodeS i s R, connect(i', i''), NodeS i s R) ∈ node_sos S"
  | node_disconnect_other:
    "⟦ i ≠ i'; i ≠ i'' ⟧ ⟹ (NodeS i s R, disconnect(i', i''), NodeS i s R) ∈ node_sos S"

inductive_cases node_arriveTE:  "(NodeS i s R, ii¬ni:arrive(m), NodeS i s' R) ∈ node_sos S"
            and node_arriveTE': "(NodeS i s R, H¬K:arrive(m), s') ∈ node_sos S"
            and node_castTE:    "(NodeS i s R, RM:*cast(m), NodeS i s' R') ∈ node_sos S"
            and node_castTE':   "(NodeS i s R, RM:*cast(m), s') ∈ node_sos S"
            and node_deliverTE: "(NodeS i s R, i:deliver(d), NodeS i s' R) ∈ node_sos S"
            and node_deliverTE': "(s, i:deliver(d), s') ∈ node_sos S"
            and node_deliverTE'': "(NodeS ii s R, i:deliver(d), s') ∈ node_sos S"
            and node_tauTE:     "(NodeS i s R, τ, NodeS i s' R) ∈ node_sos S"
            and node_tauTE':    "(NodeS i s R, τ, s') ∈ node_sos S"
            and node_connectTE: "(NodeS ii s R, connect(i, i'), NodeS ii s' R') ∈ node_sos S"
            and node_connectTE': "(NodeS ii s R, connect(i, i'), s') ∈ node_sos S"
            and node_disconnectTE: "(NodeS ii s R, disconnect(i, i'), NodeS ii s' R') ∈ node_sos S"
            and node_disconnectTE': "(NodeS ii s R, disconnect(i, i'), s') ∈ node_sos S"

lemma node_sos_never_newpkt [simp]:
  assumes "(s, a, s') ∈ node_sos S"
    shows "a ≠ i:newpkt(d, di)"
  using assms by cases auto

lemma arrives_or_not:
  assumes "(NodeS i s R, ii¬ni:arrive(m), NodeS i' s' R') ∈ node_sos S"
    shows "(ii = {i} ∧ ni = {}) ∨ (ii = {} ∧ ni = {i})"
  using assms by rule simp_all

definition
  node_comp :: "ip ⇒ ('s, 'm seq_action) automaton ⇒ ip set
                   ⇒ ('s net_state, 'm node_action) automaton"
    (‹(⟨_ : (_) : _⟩)› [0, 0, 0] 104)
where
  "⟨i : np : R⇩i⟩ ≡ ⦇ init = {NodeS i s R⇩i|s. s ∈ init np}, trans = node_sos (trans np) ⦈"

lemma trans_node_comp:
  "trans (⟨i : np : R⇩i⟩) = node_sos (trans np)"
  unfolding node_comp_def by simp

lemma init_node_comp:
  "init (⟨i : np : R⇩i⟩) = {NodeS i s R⇩i|s. s ∈ init np}"
  unfolding node_comp_def by simp

lemmas node_comps = trans_node_comp init_node_comp

lemma trans_par_node_comp [simp]:
  "trans (⟨i : s ⟨⟨ t : R⟩) = node_sos (parp_sos (trans s) (trans t))"
  unfolding node_comp_def by simp

lemma snd_par_node_comp [simp]:
  "init (⟨i : s ⟨⟨ t : R⟩) = {NodeS i st R|st. st ∈ init s × init t}"
  unfolding node_comp_def by simp

lemma node_sos_dest_is_net_state:
  assumes "(s, a, s') ∈ node_sos S"
    shows "∃i' P' R'. s' = NodeS i' P' R'"
  using assms by induct auto

lemma node_sos_dest:
  assumes "(NodeS i p R, a, s') ∈ node_sos S"
    shows "∃P' R'. s' = NodeS i P' R'"
  using assms assms [THEN node_sos_dest_is_net_state]
  by - (erule node_sos.cases, auto)

lemma node_sos_states [elim]:
  assumes "(ns, a, ns') ∈ node_sos S"
  obtains i s R s' R' where "ns  = NodeS i s  R"
                        and "ns' = NodeS i s' R'"
  proof -
    assume [intro!]: "⋀i s R s' R'. ns = NodeS i s R ⟹ ns' = NodeS i s' R' ⟹ thesis"
    from assms(1) obtain i s R where "ns = NodeS i s R"
      by (cases ns) auto
    moreover with assms(1) obtain s' R' where "ns' = NodeS i s' R'"
      by (metis node_sos_dest)
    ultimately show thesis ..
  qed

lemma node_sos_cases [elim]:
  "(NodeS i p R, a, NodeS i p' R') ∈ node_sos S ⟹
  (⋀m .       ⟦ a = R:*cast(m);          R' = R; (p, broadcast m, p') ∈ S ⟧ ⟹ P) ⟹
  (⋀m D.      ⟦ a = (R ∩ D):*cast(m);    R' = R; (p, groupcast D m, p') ∈ S ⟧ ⟹ P) ⟹
  (⋀d m.      ⟦ a = {d}:*cast(m);        R' = R; (p, unicast d m, p') ∈ S; d ∈ R ⟧ ⟹ P) ⟹
  (⋀d.        ⟦ a = τ;                   R' = R; (p, ¬unicast d, p') ∈ S; d ∉ R ⟧ ⟹ P) ⟹
  (⋀d.        ⟦ a = i:deliver(d);        R' = R; (p, deliver d, p') ∈ S ⟧ ⟹ P) ⟹
  (⋀m.        ⟦ a = {i}¬{}:arrive(m);    R' = R; (p, receive m, p') ∈ S ⟧ ⟹ P) ⟹
  (            ⟦ a = τ;                   R' = R; (p, τ, p') ∈ S ⟧ ⟹ P) ⟹
  (⋀m.        ⟦ a = {}¬{i}:arrive(m);    R' = R; p = p' ⟧ ⟹ P) ⟹
  (⋀i i'.     ⟦ a = connect(i, i');      R' = R ∪ {i'}; p = p' ⟧ ⟹ P) ⟹
  (⋀i i'.     ⟦ a = connect(i', i);      R' = R ∪ {i'}; p = p' ⟧ ⟹ P) ⟹
  (⋀i i'.     ⟦ a = disconnect(i, i');   R' = R - {i'}; p = p' ⟧ ⟹ P) ⟹
  (⋀i i'.     ⟦ a = disconnect(i', i);   R' = R - {i'}; p = p' ⟧ ⟹ P) ⟹
  (⋀i i' i''. ⟦ a = connect(i', i'');    R' = R; p = p'; i ≠ i'; i ≠ i'' ⟧ ⟹ P) ⟹
  (⋀i i' i''. ⟦ a = disconnect(i', i''); R' = R; p = p'; i ≠ i'; i ≠ i'' ⟧ ⟹ P) ⟹
  P"
  by (erule node_sos.cases) simp_all

subsection "Table 4: Structural operational semantics for partial network expressions "

inductive_set
  pnet_sos :: "('s net_state, 'm node_action) transition set
                    ⇒ ('s net_state, 'm node_action) transition set
                    ⇒ ('s net_state, 'm node_action) transition set"
  for S :: "('s net_state, 'm node_action) transition set"
  and T :: "('s net_state, 'm node_action) transition set"
where
    pnet_cast1: "⟦ (s, R:*cast(m), s') ∈ S; (t, H¬K:arrive(m), t') ∈ T; H ⊆ R; K ∩ R = {} ⟧
      ⟹ (SubnetS s t, R:*cast(m), SubnetS s' t') ∈ pnet_sos S T"

  | pnet_cast2: "⟦ (s, H¬K:arrive(m), s') ∈ S; (t, R:*cast(m), t') ∈ T;  H ⊆ R; K ∩ R = {} ⟧
      ⟹ (SubnetS s t, R:*cast(m), SubnetS s' t') ∈ pnet_sos S T"

  | pnet_arrive: "⟦ (s, H¬K:arrive(m), s') ∈ S; (t, H'¬K':arrive(m), t') ∈ T ⟧
      ⟹ (SubnetS s t,  (H ∪ H')¬(K ∪ K'):arrive(m), SubnetS s' t') ∈ pnet_sos S T"

  | pnet_deliver1: "(s, i:deliver(d), s') ∈ S
      ⟹ (SubnetS s t, i:deliver(d), SubnetS s' t) ∈ pnet_sos S T"
  | pnet_deliver2: "⟦ (t, i:deliver(d), t') ∈ T ⟧
      ⟹ (SubnetS s t, i:deliver(d), SubnetS s t') ∈ pnet_sos S T"

  | pnet_tau1: "(s, τ, s') ∈ S ⟹ (SubnetS s t, τ, SubnetS s' t) ∈ pnet_sos S T"
  | pnet_tau2: "(t, τ, t') ∈ T ⟹ (SubnetS s t, τ, SubnetS s t') ∈ pnet_sos S T"

  | pnet_connect: "⟦ (s, connect(i, i'), s') ∈ S; (t, connect(i, i'), t') ∈ T ⟧
      ⟹ (SubnetS s t, connect(i, i'), SubnetS s' t') ∈ pnet_sos S T"

  | pnet_disconnect: "⟦ (s, disconnect(i, i'), s') ∈ S; (t, disconnect(i, i'), t') ∈ T ⟧
      ⟹ (SubnetS s t, disconnect(i, i'), SubnetS s' t') ∈ pnet_sos S T"

inductive_cases partial_castTE [elim]:       "(s, R:*cast(m), s') ∈ pnet_sos S T"
            and partial_arriveTE [elim]:     "(s, H¬K:arrive(m), s') ∈ pnet_sos S T"
            and partial_deliverTE [elim]:    "(s, i:deliver(d), s') ∈ pnet_sos S T"
            and partial_tauTE [elim]:        "(s, τ, s') ∈ pnet_sos S T"
            and partial_connectTE [elim]:    "(s, connect(i, i'), s') ∈ pnet_sos S T"
            and partial_disconnectTE [elim]: "(s, disconnect(i, i'), s') ∈ pnet_sos S T"

lemma pnet_sos_never_newpkt:
  assumes "(st, a, st') ∈ pnet_sos S T"
      and "⋀i d di a s s'. (s, a, s') ∈ S ⟹ a ≠ i:newpkt(d, di)"
      and "⋀i d di a t t'. (t, a, t') ∈ T ⟹ a ≠ i:newpkt(d, di)"
    shows "a ≠ i:newpkt(d, di)"
  using assms(1) by cases (auto dest!: assms(2-3))

fun pnet :: "(ip ⇒ ('s, 'm seq_action) automaton)
              ⇒ net_tree ⇒ ('s net_state, 'm node_action) automaton"
where
    "pnet np (⟨i; R⇩i⟩)  =  ⟨i : np i : R⇩i⟩"
  | "pnet np (p⇩1 ∥ p⇩2) = ⦇ init = {SubnetS s⇩1 s⇩2 |s⇩1 s⇩2. s⇩1 ∈ init (pnet np p⇩1)
                                                      ∧ s⇩2 ∈ init (pnet np p⇩2)},
                           trans = pnet_sos (trans (pnet np p⇩1)) (trans (pnet np p⇩2)) ⦈"

lemma pnet_node_init [elim, simp]:
  assumes "s ∈ init (pnet np ⟨i; R⟩)"
    shows "s ∈ { NodeS i s R |s. s ∈ init (np i)}"
  using assms by (simp add: node_comp_def)

lemma pnet_node_init' [elim]:
 assumes "s ∈ init (pnet np ⟨i; R⟩)"
 obtains ns where "s = NodeS i ns R"
             and "ns ∈ init (np i)"
   using assms by (auto simp add: node_comp_def)

lemma pnet_node_trans [elim, simp]:
  assumes "(s, a, s') ∈ trans (pnet np ⟨i; R⟩)"
    shows "(s, a, s') ∈ node_sos (trans (np i))"
  using assms by (simp add: trans_node_comp)

lemma pnet_never_newpkt':
  assumes "(s, a, s') ∈ trans (pnet np n)"
    shows "∀i d di. a ≠ i:newpkt(d, di)"
  using assms proof (induction n arbitrary: s a s')
    fix n1 n2 s a s'
    assume IH1: "⋀s a s'. (s, a, s') ∈ trans (pnet np n1) ⟹ ∀i d di. a ≠ i:newpkt(d, di)"
       and IH2: "⋀s a s'. (s, a, s') ∈ trans (pnet np n2) ⟹ ∀i d di. a ≠ i:newpkt(d, di)"
       and "(s, a, s') ∈ trans (pnet np (n1 ∥ n2))"
    show "∀i d di. a ≠ i:newpkt(d, di)"
    proof (intro allI)
      fix i d di
      from ‹(s, a, s') ∈ trans (pnet np (n1 ∥ n2))›
        have "(s, a, s') ∈ pnet_sos (trans (pnet np n1)) (trans (pnet np n2))"
          by simp
      thus "a ≠ i:newpkt(d, di)"
        by (rule pnet_sos_never_newpkt) (auto dest!: IH1 IH2)
    qed
  qed (simp add: node_comps)

lemma pnet_never_newpkt:
  assumes "(s, a, s') ∈ trans (pnet np n)"
    shows "a ≠ i:newpkt(d, di)"
  proof -
    from assms have "∀i d di. a ≠ i:newpkt(d, di)"
      by (rule pnet_never_newpkt')
    thus ?thesis by clarsimp
  qed

subsection "Table 5: Structural operational semantics for complete network expressions "

inductive_set
  cnet_sos :: "('s, ('m::msg) node_action) transition set
                    ⇒ ('s, 'm node_action) transition set"
  for S :: "('s, 'm node_action) transition set"
where
    cnet_connect: "(s, connect(i, i'), s') ∈ S  ⟹ (s, connect(i, i'), s') ∈ cnet_sos S"
  | cnet_disconnect: "(s, disconnect(i, i'), s') ∈ S  ⟹ (s, disconnect(i, i'), s') ∈ cnet_sos S"
  | cnet_cast: "(s, R:*cast(m), s') ∈ S  ⟹ (s, τ, s') ∈ cnet_sos S"
  | cnet_tau: "(s, τ, s') ∈ S  ⟹ (s, τ, s') ∈ cnet_sos S"
  | cnet_deliver: "(s, i:deliver(d), s') ∈ S  ⟹ (s, i:deliver(d), s') ∈ cnet_sos S"
  | cnet_newpkt: "(s, {i}¬K:arrive(newpkt(d, di)), s') ∈ S  ⟹ (s, i:newpkt(d, di), s') ∈ cnet_sos S"

inductive_cases connect_completeTE: "(s, connect(i, i'), s') ∈ cnet_sos S"
            and disconnect_completeTE: "(s, disconnect(i, i'), s') ∈ cnet_sos S"
            and tau_completeTE: "(s, τ, s') ∈ cnet_sos S"
            and deliver_completeTE: "(s, i:deliver(d), s') ∈ cnet_sos S"
            and newpkt_completeTE: "(s, i:newpkt(d, di), s') ∈ cnet_sos S"

lemmas completeTEs = connect_completeTE
                     disconnect_completeTE
                     tau_completeTE
                     deliver_completeTE
                     newpkt_completeTE

lemma complete_no_cast [simp]:
  "(s, R:*cast(m), s') ∉ cnet_sos T"
  proof
    assume "(s, R:*cast(m), s') ∈ cnet_sos T"
    hence "R:*cast(m) ≠ R:*cast(m)"
     by (rule cnet_sos.cases) auto
    thus False by simp
  qed

lemma complete_no_arrive [simp]:
  "(s, ii¬ni:arrive(m), s') ∉ cnet_sos T"
  proof
    assume "(s, ii¬ni:arrive(m), s') ∈ cnet_sos T"
    hence "ii¬ni:arrive(m) ≠ ii¬ni:arrive(m)"
     by (rule cnet_sos.cases) auto
    thus False by simp
  qed

abbreviation
  closed :: "('s net_state, ('m::msg) node_action) automaton ⇒ ('s net_state, 'm node_action) automaton"
where
  "closed ≡ (λA. A ⦇ trans := cnet_sos (trans A) ⦈)"

end