(*  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_msg).p), broadcast (s_msg ξ), (ξ, p)) ∈ seqp_sos Γ"
  | groupcastT: "((ξ, {l}groupcast(s_ips, s_msg).p), groupcast (s_ips ξ) (s_msg ξ), (ξ, p)) ∈ seqp_sos Γ"
  | unicastT:   "((ξ, {l}unicast(s_ip, s_msg).p ▹ q), unicast (s_ip ξ) (s_msg ξ), (ξ, p)) ∈ seqp_sos Γ"
  | notunicastT:"((ξ, {l}unicast(s_ip, s_msg).p ▹ q), ¬unicast (s_ip ξ), (ξ, q)) ∈ seqp_sos Γ"
  | sendT:      "((ξ, {l}send(s_msg).p), send (s_msg ξ), (ξ, p)) ∈ seqp_sos Γ"
  | deliverT:   "((ξ, {l}deliver(s_data).p), deliver (s_data ξ), (ξ, p)) ∈ seqp_sos Γ"
  | receiveT:   "((ξ, {l}receive(u_msg).p), receive msg, (u_msg 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_msg). p), a, (ξ', q)) ∈ seqp_sos Γ;
    [a = broadcast (s_msg ξ); ξ' = ξ; q = p] ==> P] ==> P"
  by (ind_cases "((ξ, {l}broadcast(s_msg). p), a, (ξ', q)) ∈ seqp_sos Γ") simp

lemma seqp_groupcastTE [elim]:
  "[((ξ, {l}groupcast(s_ips, s_msg). p), a, (ξ', q)) ∈ seqp_sos Γ;
    [a = groupcast (s_ips ξ) (s_msg ξ); ξ' = ξ; q = p] ==> P] ==> P"
  by (ind_cases "((ξ, {l}groupcast(s_ips, s_msg). p), a, (ξ', q)) ∈ seqp_sos Γ") simp

lemma seqp_unicastTE [elim]:
  "[((ξ, {l}unicast(s_ip, s_msg). p ▹ q), a, (ξ', r)) ∈ seqp_sos Γ;
    [a = unicast (s_ip ξ) (s_msg ξ); ξ' = ξ; r = p] ==> P;
    [a = ¬unicast (s_ip ξ); ξ' = ξ; r = q] ==> P] ==> P"
  by (ind_cases "((ξ, {l}unicast(s_ip, s_msg). p ▹ q), a, (ξ', r)) ∈ seqp_sos Γ") simp_all

lemma seqp_sendTE [elim]:
  "[((ξ, {l}send(s_msg). p), a, (ξ', q)) ∈ seqp_sos Γ;
    [a = send (s_msg ξ); ξ' = ξ; q = p] ==> P] ==> P"
  by (ind_cases "((ξ, {l}send(s_msg). p), a, (ξ', q)) ∈ seqp_sos Γ") simp

lemma seqp_deliverTE [elim]:
  "[((ξ, {l}deliver(s_data). p), a, (ξ', q)) ∈ seqp_sos Γ;
    [a = deliver (s_data ξ); ξ' = ξ; q = p] ==> P] ==> P"
  by (ind_cases "((ξ, {l}deliver(s_data). p), a, (ξ', q)) ∈ seqp_sos Γ") simp

lemma seqp_receiveTE [elim]:
  "[((ξ, {l}receive(u_msg). p), a, (ξ', q)) ∈ seqp_sos Γ;
    ∧msg. [a = receive msg; ξ' = u_msg msg ξ; q = p] ==> P] ==> P"
  by (ind_cases "((ξ, {l}receive(u_msg). 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₁ ∥ p₂) = ( init = {SubnetS s₁ s₂ |s₁ s₂. s₁ ∈ init (pnet np p₁)
                                                      ∧ s₂ ∈ init (pnet np p₂)},
                           trans = pnet_sos (trans (pnet np p₁)) (trans (pnet np p₂)) )"

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