Quelle  OAWN_SOS.thy

(*  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(s_msg).p), broadcast (s_msg (σ i)), (σ', p)) ∈ oseqp_sos Γ i"
  | ogroupcastT: "σ' i = σ i ==>
                  ((σ, {l}groupcast(s_ips, s_msg).p), groupcast (s_ips (σ i)) (s_msg (σ i)), (σ', p)) ∈ oseqp_sos Γ i"
  | ounicastT:   "σ' i = σ i ==>
                  ((σ, {l}unicast(s_ip, s_msg).p ▹ q), unicast (s_ip (σ i)) (s_msg (σ i)), (σ', p)) ∈ oseqp_sos Γ i"
  | onotunicastT:"σ' i = σ i ==>
                  ((σ, {l}unicast(s_ip, s_msg).p ▹ q), ¬unicast (s_ip (σ i)), (σ', q)) ∈ oseqp_sos Γ i"
  | osendT:      "σ' i = σ i ==>
                  ((σ, {l}send(s_msg).p), send (s_msg (σ i)), (σ', p)) ∈ oseqp_sos Γ i"
  | odeliverT:   "σ' i = σ i ==>
                  ((σ, {l}deliver(s_data).p), deliver (s_data (σ i)), (σ', p)) ∈ oseqp_sos Γ i"
  | oreceiveT:   "σ' i = u_msg msg (σ i) ==>
                  ((σ, {l}receive(u_msg).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(s_msg). p), a, (σ', q)) ∈ oseqp_sos Γ i;
    [a = broadcast (s_msg (σ i)); σ' i = σ i; q = p] ==> P] ==> P"
  by (ind_cases "((σ, {l}broadcast(s_msg). p), a, (σ', q)) ∈ oseqp_sos Γ i") simp

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

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

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

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

lemma oseq_receiveTE [elim]:
  "[((σ, {l}receive(u_msg). p), a, (σ', q)) ∈ oseqp_sos Γ i;
    ∧msg. [a = receive msg; σ' i = u_msg msg (σ i); q = p] ==> P] ==> P"
  by (ind_cases "((σ, {l}receive(u_msg). 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 ⟨⟨ t ≡ ( init = extg ` (init s × init t), trans = oparp_sos i (trans s) (trans t) )"

lemma opar_comp_def':
  "s ⟨⟨ t = ( init = {(σ, (s_l, t_l))|σ s_l t_l. (σ, s_l) ∈ init s ∧ t_l ∈ 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 ⟨⟨ t) = oparp_sos i (trans s) (trans t)"
  unfolding opar_comp_def by simp

lemma init_opar_comp [simp]:
  "init (s ⟨⟨ t) = 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), (R∩D):*cast(m), (σ', NodeS i s' R)) ∈ onode_sos S"

  | onode_ucast:
    "[ ((σ, s), unicast d m, (σ', s')) ∈ S; d∈R ] ==> ((σ, 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; d∉R; ∀j. j≠i ⟶ σ' j = σ j ]
     ==> ((σ, NodeS i s R), τ, (σ', NodeS i s' R)) ∈ onode_sos S"

  | onode_deliver: "[ ((σ, s), deliver d, (σ', s')) ∈ S; ∀j. j≠i ⟶ σ' j = σ j ]
     ==> ((σ, NodeS i s R), i:deliver(d), (σ', NodeS i s' R)) ∈ onode_sos S"

  | onode_tau: "[ ((σ, s), τ, (σ', s')) ∈ S; ∀j. j≠i ⟶ σ' 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 : R_i⟩_o ≡ ( init = {(σ, NodeS i s R_i)|σ s. (σ, s) ∈ init onp},
                      trans = onode_sos (trans onp) )"

lemma trans_onode_comp:
  "trans (⟨i : S : R⟩_o) = onode_sos (trans S)"
  unfolding onode_comp_def by simp

lemma init_onode_comp:
  "init (⟨i : S : R⟩_o) = {(σ, 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 ⟨⟨ t : R⟩_o) = onode_sos (oparp_sos I (trans s) (trans t))"
  unfolding onode_comp_def by simp

lemma init_par_onode_comp [simp]:
  "init (⟨i : s ⟨⟨ t : R⟩_o) = {(σ, 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; R_i⟩) = ⟨i : onp i : R_i⟩_o"
  | "opnet onp (p₁ ∥ p₂) = ( init = {(σ, SubnetS s₁ s₂) |σ s₁ s₂.
                                        (σ, s₁) ∈ init (opnet onp p₁)
                                      ∧ (σ, s₂) ∈ init (opnet onp p₂)
                                      ∧ net_ips s₁ ∩ net_ips s₂ = {}},
                             trans = opnet_sos (trans (opnet onp p₁)) (trans (opnet onp p₂)) )"

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