Theory OAWN_SOS

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

section "Open semantics of the Algebra of Wireless Networks"

theory OAWN_SOS
imports TransitionSystems AWN
begin

text ‹
  These are variants of the SOS rules that work against a mixed global/local context, where
  the global context is represented by a function @{term σ} mapping ip addresses to states.
›

subsection "Open structural operational semantics for sequential process expressions "

inductive_set
  oseqp_sos
  :: "('s, 'm, 'p, 'l) seqp_env  ip
       ((ip  's) × ('s, 'm, 'p, 'l) seqp, 'm seq_action) transition set"
  for Γ :: "('s, 'm, 'p, 'l) seqp_env"
  and i :: ip
where
    obroadcastT: "σ' i = σ i 
                  ((σ, {l}broadcast(smsg).p),        broadcast (smsg (σ i)),              (σ', p))  oseqp_sos Γ i"
  | ogroupcastT: "σ' i = σ i 
                  ((σ, {l}groupcast(sips, smsg).p),  groupcast (sips (σ i)) (smsg (σ i)), (σ', p))  oseqp_sos Γ i"
  | ounicastT:   "σ' i = σ i 
                  ((σ, {l}unicast(sip, smsg).p  q), unicast (sip (σ i)) (smsg (σ i)),    (σ', p))  oseqp_sos Γ i"
  | onotunicastT:"σ' i = σ i 
                  ((σ, {l}unicast(sip, smsg).p  q), ¬unicast (sip (σ i)),               (σ', q))  oseqp_sos Γ i"
  | osendT:      "σ' i = σ i 
                  ((σ, {l}send(smsg).p),             send (smsg (σ i)),                  (σ', p))  oseqp_sos Γ i"
  | odeliverT:   "σ' i = σ i 
                  ((σ, {l}deliver(sdata).p),         deliver (sdata (σ i)),              (σ', p))  oseqp_sos Γ i"
  | oreceiveT:   "σ' i = umsg msg (σ i) 
                  ((σ, {l}receive(umsg).p),          receive msg,                       (σ', p))  oseqp_sos Γ i"
  | oassignT:    "σ' i = u (σ i) 
                  ((σ, {l}u p),                    τ,                                 (σ', p))  oseqp_sos Γ i"

  | ocallT:      "((σ, Γ pn), a, (σ', p'))  oseqp_sos Γ i 
                  ((σ, call(pn)), a, (σ', p'))  oseqp_sos Γ i" (* TPB: quite different to Table 1 *)

  | ochoiceT1:   "((σ, p), a, (σ', p'))  oseqp_sos Γ i 
                  ((σ, p  q), a, (σ', p'))  oseqp_sos Γ i"
  | ochoiceT2:   "((σ, q), a, (σ', q'))  oseqp_sos Γ i 
                  ((σ, p  q), a, (σ', q'))  oseqp_sos Γ i"

  | oguardT:     "σ' i  g (σ i)  ((σ, {l}g p), τ, (σ', p))  oseqp_sos Γ i"

inductive_cases
      oseq_callTE [elim]:      "((σ, call(pn)), a, (σ', q))  oseqp_sos Γ i"
  and oseq_choiceTE [elim]:    "((σ, p1  p2), a, (σ', q))  oseqp_sos Γ i"

lemma oseq_broadcastTE [elim]:
  "((σ, {l}broadcast(smsg). p), a, (σ', q))  oseqp_sos Γ i;
    a = broadcast (smsg (σ i)); σ' i = σ i; q = p  P  P"
  by (ind_cases "((σ, {l}broadcast(smsg). p), a, (σ', q))  oseqp_sos Γ i") simp

lemma oseq_groupcastTE [elim]:
  "((σ, {l}groupcast(sips, smsg). p), a, (σ', q))  oseqp_sos Γ i;
    a = groupcast (sips (σ i)) (smsg (σ i)); σ' i = σ i; q = p  P  P"
  by (ind_cases "((σ, {l}groupcast(sips, smsg). p), a, (σ', q))  oseqp_sos Γ i") simp

lemma oseq_unicastTE [elim]:
  "((σ, {l}unicast(sip, smsg). p  q), a, (σ', r))  oseqp_sos Γ i;
    a = unicast (sip (σ i)) (smsg (σ i)); σ' i = σ i; r = p  P;
    a = ¬unicast (sip (σ i)); σ' i = σ i; r = q  P  P"
  by (ind_cases "((σ, {l}unicast(sip, smsg). p  q), a, (σ', r))  oseqp_sos Γ i") simp_all

lemma oseq_sendTE [elim]:
  "((σ, {l}send(smsg). p), a, (σ', q))  oseqp_sos Γ i;
    a = send (smsg (σ i)); σ' i = σ i; q = p  P  P"
  by (ind_cases "((σ, {l}send(smsg). p), a, (σ', q))  oseqp_sos Γ i") simp

lemma oseq_deliverTE [elim]:
  "((σ, {l}deliver(sdata). p), a, (σ', q))  oseqp_sos Γ i;
    a = deliver (sdata (σ i)); σ' i = σ i; q = p  P  P"
  by (ind_cases "((σ, {l}deliver(sdata). p), a, (σ', q))  oseqp_sos Γ i") simp

lemma oseq_receiveTE [elim]:
  "((σ, {l}receive(umsg). p), a, (σ', q))  oseqp_sos Γ i;
    msg. a = receive msg; σ' i = umsg msg (σ i); q = p  P  P"
  by (ind_cases "((σ, {l}receive(umsg). p), a, (σ', q))  oseqp_sos Γ i") simp

lemma oseq_assignTE [elim]:
  "((σ, {l}u p), a, (σ', q))  oseqp_sos Γ i; a = τ; σ' i = u (σ i); q = p  P  P"
  by (ind_cases "((σ, {l}u p), a, (σ', q))  oseqp_sos Γ i") simp

lemma oseq_guardTE [elim]:
  "((σ, {l}g p), a, (σ', q))  oseqp_sos Γ i; a = τ; σ' i  g (σ i); q = p  P  P"
  by (ind_cases "((σ, {l}g p), a, (σ', q))  oseqp_sos Γ i") simp

lemmas oseqpTEs =
  oseq_broadcastTE
  oseq_groupcastTE
  oseq_unicastTE
  oseq_sendTE
  oseq_deliverTE
  oseq_receiveTE
  oseq_assignTE
  oseq_callTE
  oseq_choiceTE
  oseq_guardTE

declare oseqp_sos.intros [intro]

subsection "Open structural operational semantics for parallel process expressions "

inductive_set
  oparp_sos :: "ip
                ((ip  's) × 's1, 'm seq_action) transition set
                ('s2, 'm seq_action) transition set
                ((ip  's) × ('s1 × 's2), 'm seq_action) transition set"
  for i :: ip
  and S :: "((ip  's) × 's1, 'm seq_action) transition set"
  and T :: "('s2, 'm seq_action) transition set"
where
    oparleft:  " ((σ, s), a, (σ', s'))  S; m. a  receive m  
                ((σ, (s, t)), a, (σ', (s', t)))  oparp_sos i S T"
  | oparright: " (t, a, t')  T; m. a  send m; σ' i = σ i  
                ((σ, (s, t)), a, (σ', (s, t')))  oparp_sos i S T"
  | oparboth:  " ((σ, s), receive m, (σ', s'))  S; (t, send m, t')  T  
                ((σ, (s, t)), τ, (σ', (s', t')))  oparp_sos i S T"

lemma opar_broadcastTE [elim]:
  "((σ, (s, t)), broadcast m, (σ', (s', t')))  oparp_sos i S T;
    ((σ, s), broadcast m, (σ', s'))  S; t' = t  P;
    (t, broadcast m, t')  T; s' = s; σ' i = σ i  P  P"
  by (ind_cases "((σ, (s, t)), broadcast m, (σ', (s', t')))  oparp_sos i S T") simp_all

lemma opar_groupcastTE [elim]:
  "((σ, (s, t)), groupcast ips m, (σ', (s', t')))  oparp_sos i S T;
    ((σ, s), groupcast ips m, (σ', s'))  S; t' = t  P;
    (t, groupcast ips m, t')  T; s' = s; σ' i = σ i  P  P"
  by (ind_cases "((σ, (s, t)), groupcast ips m, (σ', (s', t')))  oparp_sos i S T") simp_all

lemma opar_unicastTE [elim]:
  "((σ, (s, t)), unicast i m, (σ', (s', t')))  oparp_sos i S T;
    ((σ, s), unicast i m, (σ', s'))  S; t' = t  P;
    (t, unicast i m, t')  T; s' = s; σ' i = σ i  P  P"
  by (ind_cases "((σ, (s, t)), unicast i m, (σ', (s', t')))  oparp_sos i S T") simp_all

lemma opar_notunicastTE [elim]:
  "((σ, (s, t)), notunicast i, (σ', (s', t')))  oparp_sos i S T;
    ((σ, s), notunicast i, (σ', s'))  S; t' = t  P;
    (t, notunicast i, t')  T; s' = s; σ' i = σ i  P  P"
  by (ind_cases "((σ, (s, t)), notunicast i, (σ', (s', t')))  oparp_sos i S T") simp_all

lemma opar_sendTE [elim]:
  "((σ, (s, t)), send m, (σ', (s', t')))  oparp_sos i S T;
    ((σ, s), send m, (σ', s'))  S; t' = t  P  P"
  by (ind_cases "((σ, (s, t)), send m, (σ', (s', t')))  oparp_sos i S T") auto

lemma opar_deliverTE [elim]:
  "((σ, (s, t)), deliver d, (σ', (s', t')))  oparp_sos i S T;
    ((σ, s), deliver d, (σ', s'))  S; t' = t  P;
    (t, deliver d, t')  T; s' = s; σ' i = σ i  P  P"
  by (ind_cases "((σ, (s, t)), deliver d, (σ', (s', t')))  oparp_sos i S T") simp_all

lemma opar_receiveTE [elim]:
  "((σ, (s, t)), receive m, (σ', (s', t')))  oparp_sos i S T;
    (t, receive m, t')  T; s' = s; σ' i = σ i  P  P"
  by (ind_cases "((σ, (s, t)), receive m, (σ', (s', t')))  oparp_sos i S T") auto

inductive_cases opar_tauTE: "((σ, (s, t)), τ, (σ', (s', t')))  oparp_sos i S T"

lemmas oparpTEs =
  opar_broadcastTE
  opar_groupcastTE
  opar_unicastTE
  opar_notunicastTE
  opar_sendTE
  opar_deliverTE
  opar_receiveTE

lemma oparp_sos_cases [elim]:
  assumes "((σ, (s, t)), a, (σ', (s', t')))  oparp_sos i 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; σ' i = σ i   P"
      and "m.  a = τ; ((σ, s), receive m, (σ', s'))  S; (t, send m, t')  T   P"
    shows "P"
  using assms by cases auto

definition extg :: "('a × 'b) × 'c  'a × 'b × 'c"
where "extg  λ((σ, l1), l2). (σ, (l1, l2))"

lemma extgsimp [simp]:
  "extg ((σ, l1), l2) = (σ, (l1, l2))"
  unfolding extg_def by simp

lemma extg_range_prod: "extg ` (i1 × i2) = {(σ, (s1, s2))|σ s1 s2. (σ, s1)  i1  s2  i2}"
  unfolding image_def extg_def
  by (rule Collect_cong) (auto split: prod.split)

definition
  opar_comp :: "((ip  's) × 's1, 'm seq_action) automaton
                ip
                ('s2, 'm seq_action) automaton
                ((ip  's) × 's1 × 's2, 'm seq_action) automaton"
  ("(_ ⟨⟨⇘_ _)" [102, 0, 103] 102)
where
  "s ⟨⟨⇘it   init = extg ` (init s × init t), trans = oparp_sos i (trans s) (trans t) "

lemma opar_comp_def':
  "s ⟨⟨⇘it =  init = {(σ, (sl, tl))|σ sl tl. (σ, sl)  init s  tl  init t},
                trans = oparp_sos i (trans s) (trans t) "
  unfolding opar_comp_def extg_def image_def by (auto split: prod.split)

lemma trans_opar_comp [simp]:
  "trans (s ⟨⟨⇘it) = oparp_sos i (trans s) (trans t)"
  unfolding opar_comp_def by simp

lemma init_opar_comp [simp]:
  "init (s ⟨⟨⇘it) = extg ` (init s × init t)"
  unfolding opar_comp_def by simp

subsection "Open structural operational semantics for node expressions "

inductive_set
  onode_sos :: "((ip  's) × 'l, 'm seq_action) transition set
                 ((ip  's) × 'l net_state, 'm node_action) transition set"
  for S :: "((ip  's) × 'l, 'm seq_action) transition set"
where
    onode_bcast:
    "((σ, s), broadcast m, (σ', s'))  S  ((σ, NodeS i s R), R:*cast(m), (σ', NodeS i s' R))  onode_sos S"

  | onode_gcast:
    "((σ, s), groupcast D m, (σ', s'))  S  ((σ, NodeS i s R), (RD):*cast(m), (σ', NodeS i s' R))  onode_sos S"

  | onode_ucast:
    " ((σ, s), unicast d m, (σ', s'))  S; dR   ((σ, NodeS i s R), {d}:*cast(m), (σ', NodeS i s' R))  onode_sos S"

    (* Such assumptions aid later proofs, but they must be justified when transferring results
       to closed systems. *)
  | onode_notucast: " ((σ, s), ¬unicast d, (σ', s'))  S; dR; j. ji  σ' j = σ j 
      ((σ, NodeS i s R), τ, (σ', NodeS i s' R))  onode_sos S"

  | onode_deliver: " ((σ, s), deliver d, (σ', s'))  S; j. ji  σ' j = σ j 
      ((σ, NodeS i s R), i:deliver(d), (σ', NodeS i s' R))  onode_sos S"

  | onode_tau: " ((σ, s), τ, (σ', s'))  S; j. ji  σ' j = σ j 
      ((σ, NodeS i s R),   τ, (σ', NodeS i s' R))  onode_sos S"

  | onode_receive:
    "((σ, s), receive m, (σ', s'))  S  ((σ, NodeS i s R), {i}¬{}:arrive(m), (σ', NodeS i s' R))  onode_sos S"

  | onode_arrive:
    "σ' i = σ i  ((σ, NodeS i s R), {}¬{i}:arrive(m),  (σ', NodeS i s R))  onode_sos S"

  | onode_connect1:
    "σ' i = σ i  ((σ, NodeS i s R), connect(i, i'),    (σ', NodeS i s (R  {i'})))  onode_sos S"

  | onode_connect2:
    "σ' i = σ i  ((σ, NodeS i s R), connect(i', i),    (σ', NodeS i s (R  {i'})))  onode_sos S"

  | onode_disconnect1:
    "σ' i = σ i  ((σ, NodeS i s R), disconnect(i, i'), (σ', NodeS i s (R - {i'})))  onode_sos S"

  | onode_disconnect2:
    "σ' i = σ i  ((σ, NodeS i s R), disconnect(i', i), (σ', NodeS i s (R - {i'})))  onode_sos S"

  | onode_connect_other:
    " i  i'; i  i''; σ' i = σ i   ((σ, NodeS i s R), connect(i', i''),    (σ', NodeS i s R))  onode_sos S"

  | onode_disconnect_other:
    " i  i'; i  i''; σ' i = σ i   ((σ, NodeS i s R), disconnect(i', i''), (σ', NodeS i s R))  onode_sos S"

inductive_cases
      onode_arriveTE [elim]:     "((σ, NodeS i s R), ii¬ni:arrive(m),   (σ', NodeS i' s' R'))  onode_sos S"
  and onode_castTE [elim]:       "((σ, NodeS i s R), RR:*cast(m),        (σ', NodeS i' s' R'))  onode_sos S"
  and onode_deliverTE [elim]:    "((σ, NodeS i s R), ii:deliver(d),      (σ', NodeS i' s' R'))  onode_sos S"
  and onode_connectTE [elim]:    "((σ, NodeS i s R), connect(ii, ii'),   (σ', NodeS i' s' R'))  onode_sos S"
  and onode_disconnectTE [elim]: "((σ, NodeS i s R), disconnect(ii, ii'),(σ', NodeS i' s' R'))  onode_sos S"
  and onode_newpktTE [elim]:     "((σ, NodeS i s R), ii:newpkt(d, di),   (σ', NodeS i' s' R'))  onode_sos S"
  and onode_tauTE [elim]:        "((σ, NodeS i s R), τ,                  (σ', NodeS i' s' R'))  onode_sos S"

lemma oarrives_or_not:
  assumes "((σ, NodeS i s R), ii¬ni:arrive(m), (σ', NodeS i' s' R'))  onode_sos S"
    shows "(ii = {i}  ni = {})  (ii = {}  ni = {i})"
  using assms by rule simp_all

definition
  onode_comp :: "ip
                  ((ip  's) × 'l, 'm seq_action) automaton
                  ip set
                  ((ip  's) × 'l net_state, 'm node_action) automaton"
    ("(_ : (_) : _o)" [0, 0, 0] 104)
where
  "i : onp : Rio   init = {(σ, NodeS i s Ri)|σ s. (σ, s)  init onp},
                      trans = onode_sos (trans onp) "

lemma trans_onode_comp:
  "trans (i : S : Ro) = onode_sos (trans S)"
  unfolding onode_comp_def by simp

lemma init_onode_comp:
  "init (i : S : Ro) = {(σ, NodeS i s R)|σ s. (σ, s)  init S}"
  unfolding onode_comp_def by simp

lemmas onode_comps = trans_onode_comp init_onode_comp

lemma fst_par_onode_comp [simp]:
  "trans (i : s ⟨⟨⇘It : Ro) = onode_sos (oparp_sos I (trans s) (trans t))"
  unfolding onode_comp_def by simp

lemma init_par_onode_comp [simp]:
  "init (i : s ⟨⟨⇘It : Ro) = {(σ, NodeS i (s1, s2) R)|σ s1 s2. ((σ, s1), s2)  init s × init t}"
  unfolding onode_comp_def by (simp add: extg_range_prod)

lemma onode_sos_dest_is_net_state:
  assumes "((σ, p), a, s')  onode_sos S"
    shows "σ' i' ζ' R'. s' = (σ', NodeS i' ζ' R')"
  using assms proof -
    assume "((σ, p), a, s')  onode_sos S"
    then obtain σ' i' ζ' R' where "s' = (σ', NodeS i' ζ' R')"
      by (cases s') (auto elim!: onode_sos.cases)
    thus ?thesis by simp
  qed

lemma onode_sos_dest_is_net_state':
  assumes "((σ, NodeS i p R), a, s')  onode_sos S"
    shows "σ' ζ' R'. s' = (σ', NodeS i ζ' R')"
  using assms proof -
    assume "((σ, NodeS i p R), a, s')  onode_sos S"
    then obtain σ' ζ' R' where "s' = (σ', NodeS i ζ' R')"
      by (cases s') (auto elim!: onode_sos.cases)
    thus ?thesis by simp
  qed

lemma onode_sos_dest_is_net_state'':
  assumes "((σ, NodeS i p R), a, (σ', s'))  onode_sos S"
    shows "ζ' R'. s' = NodeS i ζ' R'"
  proof -
    define ns' where "ns' = (σ', s')"
    with assms have "((σ, NodeS i p R), a, ns')  onode_sos S" by simp
    then obtain σ'' ζ' R' where "ns' = (σ'', NodeS i ζ' R')"
      by (metis onode_sos_dest_is_net_state')
    hence "s' = NodeS i ζ' R'" by (simp add: ns'_def)
    thus ?thesis by simp
  qed

lemma onode_sos_src_is_net_state:
  assumes "((σ, p), a, s')  onode_sos S"
    shows "i ζ R. p = NodeS i ζ R"
  using assms proof -
    assume "((σ, p), a, s')  onode_sos S"
    then obtain i ζ R where "p = NodeS i ζ R"
      by (cases s') (auto elim!: onode_sos.cases)
    thus ?thesis by simp
  qed

lemma onode_sos_net_states:
  assumes "((σ, s), a, (σ', s'))  onode_sos S"
    shows "i ζ R ζ' R'. s = NodeS i ζ R  s' = NodeS i ζ' R'"
  proof -
    from assms obtain i ζ R where "s = NodeS i ζ R"
      by (metis onode_sos_src_is_net_state)
    moreover with assms obtain ζ' R' where "s' = NodeS i ζ' R'"
      by (auto dest!: onode_sos_dest_is_net_state')
    ultimately show ?thesis by simp
  qed

lemma node_sos_cases [elim]:
  "((σ, NodeS i p R), a, (σ', NodeS i p' R'))  onode_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'; σ' i = σ i   P) 
  (i i'.      a = connect(i, i');      R' = R  {i'}; p = p'; σ' i = σ i   P) 
  (i i'.      a = connect(i', i);      R' = R  {i'}; p = p'; σ' i = σ i   P) 
  (i i'.      a = disconnect(i, i');   R' = R - {i'}; p = p'; σ' i = σ i   P) 
  (i i'.      a = disconnect(i', i);   R' = R - {i'}; p = p'; σ' i = σ i   P) 
  (i i' i''.  a = connect(i', i'');    R' = R; p = p'; i  i'; i  i''; σ' i = σ i   P) 
  (i i' i''.  a = disconnect(i', i''); R' = R; p = p'; i  i'; i  i''; σ' i = σ i   P) 
  P"
  by (erule onode_sos.cases) (simp | metis)+

subsection "Open structural operational semantics for partial network expressions "

inductive_set
  opnet_sos :: "((ip  's) × 'l net_state, 'm node_action) transition set
                        ((ip  's) × 'l net_state, 'm node_action) transition set
                        ((ip  's) × 'l net_state, 'm node_action) transition set"
  for S :: "((ip  's) × 'l net_state, 'm node_action) transition set"
  and T :: "((ip  's) × 'l net_state, 'm node_action) transition set"
where
    opnet_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'))  opnet_sos S T"

  | opnet_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'))  opnet_sos S T"

  | opnet_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'))  opnet_sos S T"

  | opnet_deliver1:
    "((σ, s), i:deliver(d), (σ', s'))  S
       ((σ, SubnetS s t), i:deliver(d), (σ', SubnetS s' t))  opnet_sos S T"

  | opnet_deliver2:
    " ((σ, t), i:deliver(d), (σ', t'))  T 
       ((σ, SubnetS s t), i:deliver(d), (σ', SubnetS s t'))  opnet_sos S T"

  | opnet_tau1:
    "((σ, s), τ, (σ', s'))  S  ((σ, SubnetS s t), τ, (σ', SubnetS s' t))  opnet_sos S T"

  | opnet_tau2:
    "((σ, t), τ, (σ', t'))  T  ((σ, SubnetS s t), τ, (σ', SubnetS s t'))  opnet_sos S T"

  | opnet_connect:
    " ((σ, s), connect(i, i'), (σ', s'))  S; ((σ, t), connect(i, i'), (σ', t'))  T 
       ((σ, SubnetS s t), connect(i, i'), (σ', SubnetS s' t'))  opnet_sos S T"

  | opnet_disconnect:
    " ((σ, s), disconnect(i, i'), (σ', s'))  S; ((σ, t), disconnect(i, i'), (σ', t'))  T 
       ((σ, SubnetS s t), disconnect(i, i'), (σ', SubnetS s' t'))  opnet_sos S T"

inductive_cases opartial_castTE [elim]:       "((σ, s), R:*cast(m), (σ', s'))  opnet_sos S T"
            and opartial_arriveTE [elim]:     "((σ, s), H¬K:arrive(m), (σ', s'))  opnet_sos S T"
            and opartial_deliverTE [elim]:    "((σ, s), i:deliver(d), (σ', s'))  opnet_sos S T"
            and opartial_tauTE [elim]:        "((σ, s), τ, (σ', s'))  opnet_sos S T"
            and opartial_connectTE [elim]:    "((σ, s), connect(i, i'), (σ', s'))  opnet_sos S T"
            and opartial_disconnectTE [elim]: "((σ, s), disconnect(i, i'), (σ', s'))  opnet_sos S T"
            and opartial_newpktTE [elim]:     "((σ, s), i:newpkt(d, di), (σ', s'))  opnet_sos S T"

fun opnet :: "(ip  ((ip  's) × 'l, 'm seq_action) automaton)
               net_tree  ((ip  's) × 'l net_state, 'm node_action) automaton"
where
    "opnet onp (i; Ri)  =  i : onp i : Rio"
  | "opnet onp (p1  p2) =  init = {(σ, SubnetS s1 s2) |σ s1 s2.
                                        (σ, s1)  init (opnet onp p1)
                                       (σ, s2)  init (opnet onp p2)
                                       net_ips s1  net_ips s2 = {}},
                             trans = opnet_sos (trans (opnet onp p1)) (trans (opnet onp p2)) "

lemma opnet_node_init [elim, simp]:
  assumes "(σ, s)  init (opnet onp i; R)"
    shows "(σ, s)  { (σ, NodeS i ns R) |σ ns. (σ, ns)  init (onp i)}"
  using assms by (simp add: onode_comp_def)

lemma opnet_node_init' [elim]:
 assumes "(σ, s)  init (opnet onp i; R)"
 obtains ns where "s = NodeS i ns R"
             and "(σ, ns)  init (onp i)"
   using assms by (auto simp add: onode_comp_def)

lemma opnet_node_trans [elim, simp]:
  assumes "(s, a, s')  trans (opnet onp i; R)"
    shows "(s, a, s')  onode_sos (trans (onp i))"
  using assms by (simp add: trans_onode_comp)

subsection "Open structural operational semantics for complete network expressions "

inductive_set
  ocnet_sos :: "((ip  's) × 'l net_state, 'm::msg node_action) transition set
                          ((ip  's) × 'l net_state, 'm node_action) transition set"
  for S :: "((ip  's) × 'l net_state, 'm node_action) transition set"
where
    ocnet_connect:
    " ((σ, s), connect(i, i'), (σ', s'))  S; j. j  net_ips s  (σ' j = σ j) 
      ((σ, s), connect(i, i'), (σ', s'))  ocnet_sos S"

  | ocnet_disconnect:
    " ((σ, s), disconnect(i, i'), (σ', s'))  S; j. j  net_ips s  (σ' j = σ j) 
      ((σ, s), disconnect(i, i'), (σ', s'))  ocnet_sos S"

  | ocnet_cast:
    " ((σ, s), R:*cast(m), (σ', s'))  S; j. j  net_ips s  (σ' j = σ j) 
      ((σ, s), τ, (σ', s'))  ocnet_sos S"

  | ocnet_tau:  
    " ((σ, s), τ, (σ', s'))  S; j. j  net_ips s  (σ' j = σ j) 
      ((σ, s), τ, (σ', s'))  ocnet_sos S"

  | ocnet_deliver:
    " ((σ, s), i:deliver(d), (σ', s'))  S; j. j  net_ips s  (σ' j = σ j) 
      ((σ, s), i:deliver(d), (σ', s'))  ocnet_sos S"

  | ocnet_newpkt:
    " ((σ, s), {i}¬K:arrive(newpkt(d, di)), (σ', s'))  S; j. j  net_ips s  (σ' j = σ j) 
      ((σ, s), i:newpkt(d, di), (σ', s'))  ocnet_sos S"

inductive_cases oconnect_completeTE: "((σ, s), connect(i, i'), (σ', s'))  ocnet_sos S"
            and odisconnect_completeTE: "((σ, s), disconnect(i, i'), (σ', s'))  ocnet_sos S"
            and otau_completeTE: "((σ, s), τ, (σ', s'))  ocnet_sos S"
            and odeliver_completeTE: "((σ, s), i:deliver(d), (σ', s'))  ocnet_sos S"
            and onewpkt_completeTE: "((σ, s), i:newpkt(d, di), (σ', s'))  ocnet_sos S"

lemmas ocompleteTEs = oconnect_completeTE
                      odisconnect_completeTE
                      otau_completeTE
                      odeliver_completeTE
                      onewpkt_completeTE

lemma ocomplete_no_cast [simp]:
  "((σ, s), R:*cast(m), (σ', s'))  ocnet_sos T"
  proof
    assume "((σ, s), R:*cast(m), (σ', s'))  ocnet_sos T"
    hence "R:*cast(m)  R:*cast(m)"
     by (rule ocnet_sos.cases) auto
    thus False by simp
  qed

lemma ocomplete_no_arrive [simp]:
  "((σ, s), ii¬ni:arrive(m), (σ', s'))  ocnet_sos T"
  proof
    assume "((σ, s), ii¬ni:arrive(m), (σ', s'))  ocnet_sos T"
    hence "ii¬ni:arrive(m)  ii¬ni:arrive(m)"
     by (rule ocnet_sos.cases) auto
    thus False by simp
  qed

lemma ocomplete_no_change [elim]:
  assumes "((σ, s), a, (σ', s'))  ocnet_sos T"
      and "j  net_ips s"
    shows "σ' j = σ j"
  using assms by cases simp_all

lemma ocomplete_transE [elim]:
  assumes "((σ, ζ), a, (σ', ζ'))  ocnet_sos (trans (opnet onp n))"
  obtains a' where "((σ, ζ), a', (σ', ζ'))  trans (opnet onp n)"
  using assms by (cases a) (auto elim!: ocompleteTEs [simplified])

abbreviation
  oclosed :: "((ip  's) × 'l net_state, ('m::msg) node_action) automaton
               ((ip  's) × 'l net_state, 'm node_action) automaton"
where
  "oclosed  (λA. A  trans := ocnet_sos (trans A) )"

end