Quelle  Pnet.thy

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

section "Lemmas for partial networks"

theory Pnet
imports AWN_SOS Invariants
begin

text ‹
 These lemmas mostly concern the preservation of node structure by @{term pnet_sos} transitions.
 ›

lemma pnet_maintains_dom:
  assumes "(s, a, s') ∈ trans (pnet np p)"
    shows "net_ips s = net_ips s'"
  using assms proof (induction p arbitrary: s a s')
    fix i R σ s a s'
    assume "(s, a, s') ∈ trans (pnet np ⟨i; R⟩)"
    hence "(s, a, s') ∈ node_sos (trans (np i))" ..
    thus "net_ips s = net_ips s'"
      by (rule node_sos.cases) simp_all
  next
    fix p1 p2 s a s'
    assume "∧s a s'. (s, a, s') ∈ trans (pnet np p1) ==> net_ips s = net_ips s'"
       and "∧s a s'. (s, a, s') ∈ trans (pnet np p2) ==> net_ips s = net_ips s'"
       and "(s, a, s') ∈ trans (pnet np (p1 ∥ p2))"
    thus "net_ips s = net_ips s'"
      by simp (erule pnet_sos.cases, simp_all)
  qed

lemma pnet_net_ips_net_tree_ips [elim]:
  assumes "s ∈ reachable (pnet np p) I"
    shows "net_ips s = net_tree_ips p"
  using assms proof induction
    fix s
    assume "s ∈ init (pnet np p)"
    thus "net_ips s = net_tree_ips p"
    proof (induction p arbitrary: s)
      fix i R s
      assume "s ∈ init (pnet np ⟨i; R⟩)"
      then obtain ns where "s = NodeS i ns R" ..
      thus "net_ips s = net_tree_ips ⟨i; R⟩"
        by simp
    next
      fix p1 p2 s
      assume IH1: "∧s. s ∈ init (pnet np p1) ==> net_ips s = net_tree_ips p1"
         and IH2: "∧s. s ∈ init (pnet np p2) ==> net_ips s = net_tree_ips p2"
         and "s ∈ init (pnet np (p1 ∥ p2))"
      from this(3) obtain s1 s2 where "s1 ∈ init (pnet np p1)"
                                  and "s2 ∈ init (pnet np p2)"
                                  and "s = SubnetS s1 s2" by auto
      from this(1-2) have "net_ips s1 = net_tree_ips p1"
                      and "net_ips s2 = net_tree_ips p2"
        using IH1 IH2 by auto
      with ‹s = SubnetS s1 s2› show "net_ips s = net_tree_ips (p1 ∥ p2)" by auto
    qed
  next
    fix s a s'
    assume "(s, a, s') ∈ trans (pnet np p)"
       and "net_ips s = net_tree_ips p"
    from this(1) have "net_ips s = net_ips s'"
      by (rule pnet_maintains_dom)
    with ‹net_ips s = net_tree_ips p› show "net_ips s' = net_tree_ips p"
      by simp
  qed

lemma pnet_init_net_ips_net_tree_ips:
  assumes "s ∈ init (pnet np p)"
    shows "net_ips s = net_tree_ips p"
  using assms(1) by (rule reachable_init [THEN pnet_net_ips_net_tree_ips])

lemma pnet_init_in_net_ips_in_net_tree_ips [elim]:
  assumes "s ∈ init (pnet np p)"
      and "i ∈ net_ips s"
    shows "i ∈ net_tree_ips p"
  using assms by (clarsimp dest!: pnet_init_net_ips_net_tree_ips)

lemma pnet_init_in_net_tree_ips_in_net_ips [elim]:
  assumes "s ∈ init (pnet np p)"
      and "i ∈ net_tree_ips p"
    shows "i ∈ net_ips s"
  using assms by (clarsimp dest!: pnet_init_net_ips_net_tree_ips)

lemma pnet_init_not_in_net_tree_ips_not_in_net_ips [elim]:
  assumes "s ∈ init (pnet np p)"
      and "i ∉ net_tree_ips p"
    shows "i ∉ net_ips s"
  proof
    assume "i ∈ net_ips s"
    with assms(1) have "i ∈ net_tree_ips p" ..
    with assms(2) show False ..
  qed

lemma net_node_reachable_is_node:
  assumes "st ∈ reachable (pnet np ⟨ii; R_i⟩) I"
    shows "∃ns R. st = NodeS ii ns R"
  using assms proof induct
    fix s
    assume "s ∈ init (pnet np ⟨ii; R_i⟩)"
    thus "∃ns R. s = NodeS ii ns R"
      by (rule pnet_node_init') simp
  next
    fix s a s'
    assume "s ∈ reachable (pnet np ⟨ii; R_i⟩) I"
       and "∃ns R. s = NodeS ii ns R"
       and "(s, a, s') ∈ trans (pnet np ⟨ii; R_i⟩)"
       and "I a"
    thus "∃ns R. s' = NodeS ii ns R"
      by (auto simp add: trans_node_comp dest!: node_sos_dest)
  qed

lemma partial_net_preserves_subnets:
  assumes "(SubnetS s t, a, st') ∈ pnet_sos (trans (pnet np p1)) (trans (pnet np p2))"
    shows "∃s' t'. st' = SubnetS s' t'"
  using assms by cases simp_all

lemma net_par_reachable_is_subnet:
  assumes "st ∈ reachable (pnet np (p1 ∥ p2)) I"
    shows "∃s t. st = SubnetS s t"
  using assms by induct (auto dest!: partial_net_preserves_subnets)

lemma reachable_par_subnet_induct [consumes, case_names init step]:
  assumes "SubnetS s t ∈ reachable (pnet np (p1 ∥ p2)) I"
      and init: "∧s t. SubnetS s t ∈ init (pnet np (p1 ∥ p2)) ==> P s t"
      and step: "∧s t s' t' a. [
                    SubnetS s t ∈ reachable (pnet np (p1 ∥ p2)) I;
                    P s t; (SubnetS s t, a, SubnetS s' t') ∈ (trans (pnet np (p1 ∥ p2))); I a ]
                    ==> P s' t'"
    shows "P s t"
  using assms(1) proof (induction "SubnetS s t" arbitrary: s t)
    fix s t
    assume "SubnetS s t ∈ init (pnet np (p1 ∥ p2))"
    with init show "P s t" .
  next
    fix st a s' t'
    assume "st ∈ reachable (pnet np (p1 ∥ p2)) I"
       and tr: "(st, a, SubnetS s' t') ∈ trans (pnet np (p1 ∥ p2))"
       and "I a"
       and IH: "∧s t. st = SubnetS s t ==> P s t"
    from this(1) obtain s t where "st = SubnetS s t"
                              and str: "SubnetS s t ∈ reachable (pnet np (p1 ∥ p2)) I"
      by (metis net_par_reachable_is_subnet)
    note this(2)
    moreover from IH and ‹st = SubnetS s t› have "P s t" .
    moreover from ‹st = SubnetS s t› and tr
      have "(SubnetS s t, a, SubnetS s' t') ∈ trans (pnet np (p1 ∥ p2))" by simp
    ultimately show "P s' t'"
      using ‹I a› by (rule step)
  qed

lemma subnet_reachable:
  assumes "SubnetS s1 s2 ∈ reachable (pnet np (p1 ∥ p2)) TT"
    shows "s1 ∈ reachable (pnet np p1) TT"
          "s2 ∈ reachable (pnet np p2) TT"
  proof -
    from assms have "s1 ∈ reachable (pnet np p1) TT
                  ∧ s2 ∈ reachable (pnet np p2) TT"
    proof (induction rule: reachable_par_subnet_induct)
      fix s1 s2
      assume "SubnetS s1 s2 ∈ init (pnet np (p1 ∥ p2))"
      thus "s1 ∈ reachable (pnet np p1) TT
          ∧ s2 ∈ reachable (pnet np p2) TT"
        by (auto dest: reachable_init)
    next
      case (step s1 s2 s1' s2' a)
      hence "SubnetS s1 s2 ∈ reachable (pnet np (p1 ∥ p2)) TT"
        and sr1: "s1 ∈ reachable (pnet np p1) TT"
        and sr2: "s2 ∈ reachable (pnet np p2) TT"
        and "(SubnetS s1 s2, a, SubnetS s1' s2') ∈ trans (pnet np (p1 ∥ p2))" by auto
      from this(4)
        have "(SubnetS s1 s2, a, SubnetS s1' s2') ∈ pnet_sos (trans (pnet np p1)) (trans (pnet np p2))"
          by simp
      thus "s1' ∈ reachable (pnet np p1) TT
         ∧ s2' ∈ reachable (pnet np p2) TT"
        by cases (insert sr1 sr2, auto elim: reachable_step)
    qed
    thus "s1 ∈ reachable (pnet np p1) TT"
         "s2 ∈ reachable (pnet np p2) TT" by auto
  qed

lemma delivered_to_node [elim]:
  assumes "s ∈ reachable (pnet np ⟨ii; R_i⟩) TT"
      and "(s, i:deliver(d), s') ∈ trans (pnet np ⟨ii; R_i⟩)"
    shows "i = ii"
  proof -
    from assms(1) obtain P R where "s = NodeS ii P R"
      by (metis net_node_reachable_is_node)
    with assms(2) show "i = ii"
       by (clarsimp simp add: trans_node_comp elim!: node_deliverTE')
  qed

lemma delivered_to_net_ips:
  assumes "s ∈ reachable (pnet np p) TT"
      and "(s, i:deliver(d), s') ∈ trans (pnet np p)"
    shows "i ∈ net_ips s"
  using assms proof (induction p arbitrary: s s')
    fix ii R_i s s'
    assume sr: "s ∈ reachable (pnet np ⟨ii; R_i⟩) TT"
       and "(s, i:deliver(d), s') ∈ trans (pnet np ⟨ii; R_i⟩)"
    from this(2) have tr: "(s, i:deliver(d), s') ∈ node_sos (trans (np ii))" by simp
    from sr obtain P R where [simp]: "s = NodeS ii P R"
      by (metis net_node_reachable_is_node)
    moreover from tr obtain P' R' where [simp]: "s' = NodeS ii P' R'"
      by simp (metis node_sos_dest)
    ultimately have "i = ii" using tr by auto
    thus "i ∈ net_ips s" by simp
  next
    fix p1 p2 s s'
    assume IH1: "∧s s'. [ s ∈ reachable (pnet np p1) TT;
                          (s, i:deliver(d), s') ∈ trans (pnet np p1) ] ==> i ∈ net_ips s"
       and IH2: "∧s s'. [ s ∈ reachable (pnet np p2) TT;
                          (s, i:deliver(d), s') ∈ trans (pnet np p2) ] ==> i ∈ net_ips s"
       and sr: "s ∈ reachable (pnet np (p1 ∥ p2)) TT"
       and tr: "(s, i:deliver(d), s') ∈ trans (pnet np (p1 ∥ p2))"
    from tr have "(s, i:deliver(d), s') ∈ pnet_sos (trans (pnet np p1)) (trans (pnet np p2))"
      by simp
    thus "i ∈ net_ips s"
    proof (rule partial_deliverTE)
      fix s1 s1' s2
      assume "s = SubnetS s1 s2"
         and "s' = SubnetS s1' s2"
         and tr: "(s1, i:deliver(d), s1') ∈ trans (pnet np p1)"
      from sr have "s1 ∈ reachable (pnet np p1) TT"
        by (auto simp only: ‹s = SubnetS s1 s2› elim: subnet_reachable)
      hence "i ∈ net_ips s1" using tr by (rule IH1)
      thus "i ∈ net_ips s" by (simp add: ‹s = SubnetS s1 s2›)
    next
      fix s2 s2' s1
      assume "s = SubnetS s1 s2"
         and "s' = SubnetS s1 s2'"
         and tr: "(s2, i:deliver(d), s2') ∈ trans (pnet np p2)"
      from sr have "s2 ∈ reachable (pnet np p2) TT"
        by (auto simp only: ‹s = SubnetS s1 s2› elim: subnet_reachable)
      hence "i ∈ net_ips s2" using tr by (rule IH2)
      thus "i ∈ net_ips s" by (simp add: ‹s = SubnetS s1 s2›)
    qed
  qed

lemma wf_net_tree_net_ips_disjoint [elim]:
  assumes "wf_net_tree (p1 ∥ p2)"
      and "s1 ∈ reachable (pnet np p1) S"
      and "s2 ∈ reachable (pnet np p2) S"
    shows "net_ips s1 ∩ net_ips s2 = {}"
  proof -
    from ‹wf_net_tree (p1 ∥ p2)› have "net_tree_ips p1 ∩ net_tree_ips p2 = {}" by auto
    moreover from assms(2) have "net_ips s1 = net_tree_ips p1" ..
    moreover from assms(3) have "net_ips s2 = net_tree_ips p2" ..
    ultimately show ?thesis by simp
  qed

lemma init_mapstate_Some_aodv_init [elim]:
  assumes "s ∈ init (pnet np p)"
      and "netmap s i = Some v"
    shows "v ∈ init (np i)"
  using assms proof (induction p arbitrary: s)
    fix ii R s
    assume "s ∈ init (pnet np ⟨ii; R⟩)"
       and "netmap s i = Some v"
    from this(1) obtain ns where s: "s = NodeS ii ns R"
      and ns: "ns ∈ init (np ii)" ..
    from s and ‹netmap s i = Some v› have "i = ii"
      by simp (metis domI domIff)
    with s ns show "v ∈ init (np i)"
      using ‹netmap s i = Some v› by simp
  next
    fix p1 p2 s
    assume IH1: "∧s. s ∈ init (pnet np p1) ==> netmap s i = Some v ==> v ∈ init (np i)"
       and IH2: "∧s. s ∈ init (pnet np p2) ==> netmap s i = Some v ==> v ∈ init (np i)"
       and "s ∈ init (pnet np (p1 ∥ p2))"
       and "netmap s i = Some v"
    from this(3) obtain s1 s2 where "s = SubnetS s1 s2"
                                and "s1 ∈ init (pnet np p1)"
                                and "s2 ∈ init (pnet np p2)" by auto
    from this(1) and ‹netmap s i = Some v›
      have "netmap s1 i = Some v ∨ netmap s2 i = Some v" by auto
    thus "v ∈ init (np i)"
    proof
      assume "netmap s1 i = Some v"
      with ‹s1 ∈ init (pnet np p1)› show ?thesis by (rule IH1)
    next
      assume "netmap s2 i = Some v"
      with ‹s2 ∈ init (pnet np p2)› show ?thesis by (rule IH2)
    qed
  qed

lemma reachable_connect_netmap [elim]:
  assumes "s ∈ reachable (pnet np n) TT"
      and "(s, connect(i, i'), s') ∈ trans (pnet np n)"
    shows "netmap s' = netmap s"
  using assms proof (induction n arbitrary: s s')
    fix ii R_i s s'
    assume sr: "s ∈ reachable (pnet np ⟨ii; R_i⟩) TT"
       and "(s, connect(i, i'), s') ∈ trans (pnet np ⟨ii; R_i⟩)"
    from this(2) have tr: "(s, connect(i, i'), s') ∈ node_sos (trans (np ii))" ..
    from sr obtain p R where "s = NodeS ii p R"
      by (metis net_node_reachable_is_node)
    with tr show "netmap s' = netmap s"
      by (auto elim!: node_sos.cases)
  next
    fix p1 p2 s s'
    assume IH1: "∧s s'. [ s ∈ reachable (pnet np p1) TT;
                          (s, connect(i, i'), s') ∈ trans (pnet np p1) ] ==> netmap s' = netmap s"
       and IH2: "∧s s'. [ s ∈ reachable (pnet np p2) TT;
                          (s, connect(i, i'), s') ∈ trans (pnet np p2) ] ==> netmap s' = netmap s"
       and sr: "s ∈ reachable (pnet np (p1 ∥ p2)) TT"
       and tr: "(s, connect(i, i'), s') ∈ trans (pnet np (p1 ∥ p2))"
    from tr have "(s, connect(i, i'), s') ∈ pnet_sos (trans (pnet np p1)) (trans (pnet np p2))"
      by simp
    thus "netmap s' = netmap s"
    proof cases
      fix s1 s1' s2 s2'
      assume "s = SubnetS s1 s2"
         and "s' = SubnetS s1' s2'"
         and tr1: "(s1, connect(i, i'), s1') ∈ trans (pnet np p1)"
         and tr2: "(s2, connect(i, i'), s2') ∈ trans (pnet np p2)"
    from this(1) and sr
      have "SubnetS s1 s2 ∈ reachable (pnet np (p1 ∥ p2)) TT" by simp
    hence sr1: "s1 ∈ reachable (pnet np p1) TT"
      and sr2: "s2 ∈ reachable (pnet np p2) TT"
      by (auto intro: subnet_reachable)
    from sr1 tr1 have "netmap s1' = netmap s1" by (rule IH1)
    moreover from sr2 tr2 have "netmap s2' = netmap s2" by (rule IH2)
    ultimately show "netmap s' = netmap s"
      using ‹s = SubnetS s1 s2› and ‹s' = SubnetS s1' s2'› by simp
    qed simp_all
  qed

lemma reachable_disconnect_netmap [elim]:
  assumes "s ∈ reachable (pnet np n) TT"
      and "(s, disconnect(i, i'), s') ∈ trans (pnet np n)"
    shows "netmap s' = netmap s"
  using assms proof (induction n arbitrary: s s')
    fix ii R_i s s'
    assume sr: "s ∈ reachable (pnet np ⟨ii; R_i⟩) TT"
       and "(s, disconnect(i, i'), s') ∈ trans (pnet np ⟨ii; R_i⟩)"
    from this(2) have tr: "(s, disconnect(i, i'), s') ∈ node_sos (trans (np ii))" ..
    from sr obtain p R where "s = NodeS ii p R"
      by (metis net_node_reachable_is_node)
    with tr show "netmap s' = netmap s"
      by (auto elim!: node_sos.cases)
  next
    fix p1 p2 s s'
    assume IH1: "∧s s'. [ s ∈ reachable (pnet np p1) TT;
                          (s, disconnect(i, i'), s') ∈ trans (pnet np p1) ] ==> netmap s' = netmap s"
       and IH2: "∧s s'. [ s ∈ reachable (pnet np p2) TT;
                          (s, disconnect(i, i'), s') ∈ trans (pnet np p2) ] ==> netmap s' = netmap s"
       and sr: "s ∈ reachable (pnet np (p1 ∥ p2)) TT"
       and tr: "(s, disconnect(i, i'), s') ∈ trans (pnet np (p1 ∥ p2))"
    from tr have "(s, disconnect(i, i'), s') ∈ pnet_sos (trans (pnet np p1)) (trans (pnet np p2))"
      by simp
    thus "netmap s' = netmap s"
    proof cases
      fix s1 s1' s2 s2'
      assume "s = SubnetS s1 s2"
         and "s' = SubnetS s1' s2'"
         and tr1: "(s1, disconnect(i, i'), s1') ∈ trans (pnet np p1)"
         and tr2: "(s2, disconnect(i, i'), s2') ∈ trans (pnet np p2)"
    from this(1) and sr
      have "SubnetS s1 s2 ∈ reachable (pnet np (p1 ∥ p2)) TT" by simp
    hence sr1: "s1 ∈ reachable (pnet np p1) TT"
      and sr2: "s2 ∈ reachable (pnet np p2) TT"
      by (auto intro: subnet_reachable)
    from sr1 tr1 have "netmap s1' = netmap s1" by (rule IH1)
    moreover from sr2 tr2 have "netmap s2' = netmap s2" by (rule IH2)
    ultimately show "netmap s' = netmap s"
      using ‹s = SubnetS s1 s2› and ‹s' = SubnetS s1' s2'› by simp
    qed simp_all
  qed

fun net_ip_action :: "(ip ==> ('s, 'm seq_action) automaton)
                       ==> 'm node_action ==> ip ==> net_tree ==> 's net_state ==> 's net_state ==> bool"
where
    "net_ip_action np a i (p1 ∥ p2) (SubnetS s1 s2) (SubnetS s1' s2') =
         ((i ∈ net_ips s1 ⟶ ((s1, a, s1') ∈ trans (pnet np p1)
                                ∧ s2' = s2 ∧ net_ip_action np a i p1 s1 s1'))
          ∧ (i ∈ net_ips s2 ⟶ ((s2, a, s2') ∈ trans (pnet np p2))
                                   ∧ s1' = s1 ∧ net_ip_action np a i p2 s2 s2'))"
  | "net_ip_action np a i p s s' = True"

lemma pnet_tau_single_node [elim]:
  assumes "wf_net_tree p"
      and "s ∈ reachable (pnet np p) TT"
      and "(s, τ, s') ∈ trans (pnet np p)"
  shows "∃i∈net_ips s. ((∀j. j≠i ⟶ netmap s' j = netmap s j)
                         ∧ net_ip_action np τ i p s s')"
  using assms proof (induction p arbitrary: s s')
    fix ii R_i s s'
    assume "s ∈ reachable (pnet np ⟨ii; R_i⟩) TT"
       and "(s, τ, s') ∈ trans (pnet np ⟨ii; R_i⟩)"
    from this obtain p R p' R' where "s = NodeS ii p R" and "s' = NodeS ii p' R'"
      by (metis (opaque_lifting, no_types) TT_True net_node_reachable_is_node
                                      reachable_step)
    hence "net_ips s = {ii}"
      and "net_ips s' = {ii}" by simp_all
    hence "∃i∈dom (netmap s). ∀j. j ≠ i ⟶ netmap s' j = netmap s j"
      by (simp add: net_ips_is_dom_netmap)
    thus "∃i∈net_ips s. (∀j. j ≠ i ⟶ netmap s' j = netmap s j)
                         ∧ net_ip_action np τ i (⟨ii; R_i⟩) s s'"
      by (simp add: net_ips_is_dom_netmap)
  next
    fix p1 p2 s s'
    assume IH1: "∧s s'. [ wf_net_tree p1;
                          s ∈ reachable (pnet np p1) TT;
                          (s, τ, s') ∈ trans (pnet np p1) ]
                         ==> ∃i∈net_ips s. (∀j. j ≠ i ⟶ netmap s' j = netmap s j)
                                            ∧ net_ip_action np τ i p1 s s'"
       and IH2: "∧s s'. [ wf_net_tree p2;
                          s ∈ reachable (pnet np p2) TT;
                          (s, τ, s') ∈ trans (pnet np p2) ]
                         ==> ∃i∈net_ips s. (∀j. j ≠ i ⟶ netmap s' j = netmap s j)
                                            ∧ net_ip_action np τ i p2 s s'"
       and sr: "s ∈ reachable (pnet np (p1 ∥ p2)) TT"
       and "wf_net_tree (p1 ∥ p2)"
       and tr: "(s, τ, s') ∈ trans (pnet np (p1 ∥ p2))"
    from ‹wf_net_tree (p1 ∥ p2)› have "net_tree_ips p1 ∩ net_tree_ips p2 = {}"
                                  and "wf_net_tree p1" 
                                  and "wf_net_tree p2" by auto
    from tr have "(s, τ, s') ∈ pnet_sos (trans (pnet np p1)) (trans (pnet np p2))" by simp
    thus "∃i∈net_ips s. (∀j. j ≠ i ⟶ netmap s' j = netmap s j)
                        ∧ net_ip_action np τ i (p1 ∥ p2) s s'"
    proof cases
      fix s1 s1' s2
      assume subs:  "s = SubnetS s1 s2"
         and subs': "s' = SubnetS s1' s2"
         and tr1: "(s1, τ, s1') ∈ trans (pnet np p1)"
      from sr have sr1: "s1 ∈ reachable (pnet np p1) TT"
               and "s2 ∈ reachable (pnet np p2) TT"
        by (simp_all only: subs) (erule subnet_reachable)+
      with ‹net_tree_ips p1 ∩ net_tree_ips p2 = {}› have "dom(netmap s1) ∩ dom(netmap s2) = {}"
        by (metis net_ips_is_dom_netmap pnet_net_ips_net_tree_ips)
      from ‹wf_net_tree p1› sr1 tr1 obtain i where "i∈dom(netmap s1)"
                                               and *: "∀j. j ≠ i ⟶ netmap s1' j = netmap s1 j"
                                               and "net_ip_action np τ i p1 s1 s1'"
          by (auto simp add: net_ips_is_dom_netmap dest!: IH1)
      from this(1) and ‹dom(netmap s1) ∩ dom(netmap s2) = {}› have "i∉dom(netmap s2)"
        by auto
      with subs subs' tr1 ‹net_ip_action np τ i p1 s1 s1'› have "net_ip_action np τ i (p1 ∥ p2) s s'"
        by (simp add: net_ips_is_dom_netmap)
      moreover have "∀j. j ≠ i ⟶ (netmap s1' ++ netmap s2) j = (netmap s1 ++ netmap s2) j"
      proof (intro allI impI)
        fix j
        assume "j ≠ i"
        with * have "netmap s1' j = netmap s1 j" by simp
        thus "(netmap s1' ++ netmap s2) j = (netmap s1 ++ netmap s2) j"
          by (metis (opaque_lifting, mono_tags) map_add_dom_app_simps(1) map_add_dom_app_simps(3))
      qed
      ultimately show ?thesis using ‹i∈dom(netmap s1)› subs subs'
        by (auto simp add: net_ips_is_dom_netmap)
    next
      fix s2 s2' s1
      assume subs: "s = SubnetS s1 s2"
         and subs': "s' = SubnetS s1 s2'"
         and tr2: "(s2, τ, s2') ∈ trans (pnet np p2)"
      from sr have "s1 ∈ reachable (pnet np p1) TT"
               and sr2: "s2 ∈ reachable (pnet np p2) TT"
        by (simp_all only: subs) (erule subnet_reachable)+
      with ‹net_tree_ips p1 ∩ net_tree_ips p2 = {}› have "dom(netmap s1) ∩ dom(netmap s2) = {}"
        by (metis net_ips_is_dom_netmap pnet_net_ips_net_tree_ips)
      from ‹wf_net_tree p2› sr2 tr2 obtain i where "i∈dom(netmap s2)"
                                               and *: "∀j. j ≠ i ⟶ netmap s2' j = netmap s2 j"
                                               and "net_ip_action np τ i p2 s2 s2'"
          by (auto simp add: net_ips_is_dom_netmap dest!: IH2)
      from this(1) and ‹dom(netmap s1) ∩ dom(netmap s2) = {}› have "i∉dom(netmap s1)"
        by auto
      with subs subs' tr2 ‹net_ip_action np τ i p2 s2 s2'› have "net_ip_action np τ i (p1 ∥ p2) s s'"
        by (simp add: net_ips_is_dom_netmap)
      moreover have "∀j. j ≠ i ⟶ (netmap s1 ++ netmap s2') j = (netmap s1 ++ netmap s2) j"
      proof (intro allI impI)
        fix j
        assume "j ≠ i"
        with * have "netmap s2' j = netmap s2 j" by simp
        thus "(netmap s1 ++ netmap s2') j = (netmap s1 ++ netmap s2) j"
          by (metis (opaque_lifting, mono_tags) domD map_add_Some_iff map_add_dom_app_simps(3))
      qed
      ultimately show ?thesis using ‹i∈dom(netmap s2)› subs subs'
        by (clarsimp simp add: net_ips_is_dom_netmap)
           (metis domI dom_map_add map_add_find_right)
    qed simp_all
  qed

lemma pnet_deliver_single_node [elim]:
  assumes "wf_net_tree p"
      and "s ∈ reachable (pnet np p) TT"
      and "(s, i:deliver(d), s') ∈ trans (pnet np p)"
  shows "(∀j. j≠i ⟶ netmap s' j = netmap s j) ∧ net_ip_action np (i:deliver(d)) i p s s'"
    (is "?P p s s'")
  using assms proof (induction p arbitrary: s s')
    fix ii R_i s s'
    assume sr: "s ∈ reachable (pnet np ⟨ii; R_i⟩) TT"
       and tr: "(s, i:deliver(d), s') ∈ trans (pnet np ⟨ii; R_i⟩)"
    from this obtain p R p' R' where "s = NodeS ii p R" and "s' = NodeS ii p' R'"
      by (metis (opaque_lifting, no_types) TT_True net_node_reachable_is_node
                                      reachable_step)
    hence "net_ips s = {ii}"
      and "net_ips s' = {ii}" by simp_all
    hence "∀j. j ≠ ii ⟶ netmap s' j = netmap s j"
      by simp
    moreover from sr tr have "i = ii" by (rule delivered_to_node)
    ultimately show "(∀j. j ≠ i ⟶ netmap s' j = netmap s j)
                     ∧ net_ip_action np (i:deliver(d)) i (⟨ii; R_i⟩) s s'"
      by simp
  next
    fix p1 p2 s s'
    assume IH1: "∧s s'. [ wf_net_tree p1;
                          s ∈ reachable (pnet np p1) TT;
                          (s, i:deliver(d), s') ∈ trans (pnet np p1) ]
                         ==> (∀j. j ≠ i ⟶ netmap s' j = netmap s j)
                             ∧ net_ip_action np (i:deliver(d)) i p1 s s'"
       and IH2: "∧s s'. [ wf_net_tree p2;
                          s ∈ reachable (pnet np p2) TT;
                          (s, i:deliver(d), s') ∈ trans (pnet np p2) ]
                         ==> (∀j. j ≠ i ⟶ netmap s' j = netmap s j)
                             ∧ net_ip_action np (i:deliver(d)) i p2 s s'"
       and sr: "s ∈ reachable (pnet np (p1 ∥ p2)) TT"
       and "wf_net_tree (p1 ∥ p2)"
       and tr: "(s, i:deliver(d), s') ∈ trans (pnet np (p1 ∥ p2))"
    from ‹wf_net_tree (p1 ∥ p2)› have "net_tree_ips p1 ∩ net_tree_ips p2 = {}"
                                  and "wf_net_tree p1" 
                                  and "wf_net_tree p2" by auto
    from tr have "(s, i:deliver(d), s') ∈ pnet_sos (trans (pnet np p1)) (trans (pnet np p2))" by simp
    thus "(∀j. j ≠ i ⟶ netmap s' j = netmap s j)
          ∧ net_ip_action np (i:deliver(d)) i (p1 ∥ p2) s s'"
    proof cases
      fix s1 s1' s2
      assume subs:  "s = SubnetS s1 s2"
         and subs': "s' = SubnetS s1' s2"
         and tr1: "(s1, i:deliver(d), s1') ∈ trans (pnet np p1)"
      from sr have sr1: "s1 ∈ reachable (pnet np p1) TT"
               and "s2 ∈ reachable (pnet np p2) TT"
        by (simp_all only: subs) (erule subnet_reachable)+
      with ‹net_tree_ips p1 ∩ net_tree_ips p2 = {}› have "dom(netmap s1) ∩ dom(netmap s2) = {}"
        by (metis net_ips_is_dom_netmap pnet_net_ips_net_tree_ips)
      moreover from sr1 tr1 have "i ∈ net_ips s1" by (rule delivered_to_net_ips)
      ultimately have "i∉dom(netmap s2)" by (auto simp add: net_ips_is_dom_netmap)

      from ‹wf_net_tree p1› sr1 tr1 have *: "∀j. j ≠ i ⟶ netmap s1' j = netmap s1 j"
                                     and "net_ip_action np (i:deliver(d)) i p1 s1 s1'"
          by (auto dest!: IH1)
      from subs subs' tr1 this(2) ‹i∉dom(netmap s2)›
        have "net_ip_action np (i:deliver(d)) i (p1 ∥ p2) s s'"
          by (simp add: net_ips_is_dom_netmap)
      moreover have "∀j. j ≠ i ⟶ (netmap s1' ++ netmap s2) j = (netmap s1 ++ netmap s2) j"
      proof (intro allI impI)
        fix j
        assume "j ≠ i"
        with * have "netmap s1' j = netmap s1 j" by simp
        thus "(netmap s1' ++ netmap s2) j = (netmap s1 ++ netmap s2) j"
          by (metis (opaque_lifting, mono_tags) map_add_dom_app_simps(1) map_add_dom_app_simps(3))
      qed
      ultimately show ?thesis using ‹i∈net_ips s1› subs subs' by auto
    next
      fix s2 s2' s1
      assume subs: "s = SubnetS s1 s2"
         and subs': "s' = SubnetS s1 s2'"
         and tr2: "(s2, i:deliver(d), s2') ∈ trans (pnet np p2)"
      from sr have "s1 ∈ reachable (pnet np p1) TT"
               and sr2: "s2 ∈ reachable (pnet np p2) TT"
        by (simp_all only: subs) (erule subnet_reachable)+
      with ‹net_tree_ips p1 ∩ net_tree_ips p2 = {}› have "dom(netmap s1) ∩ dom(netmap s2) = {}"
        by (metis net_ips_is_dom_netmap pnet_net_ips_net_tree_ips)
      moreover from sr2 tr2 have "i ∈ net_ips s2" by (rule delivered_to_net_ips)
      ultimately have "i∉dom(netmap s1)" by (auto simp add: net_ips_is_dom_netmap)

      from ‹wf_net_tree p2› sr2 tr2 have *: "∀j. j ≠ i ⟶ netmap s2' j = netmap s2 j"
                                     and "net_ip_action np (i:deliver(d)) i p2 s2 s2'"
          by (auto dest!: IH2)
      from subs subs' tr2 this(2) ‹i∉dom(netmap s1)›
        have "net_ip_action np (i:deliver(d)) i (p1 ∥ p2) s s'"
          by (simp add: net_ips_is_dom_netmap)
      moreover have "∀j. j ≠ i ⟶ (netmap s1 ++ netmap s2') j = (netmap s1 ++ netmap s2) j"
      proof (intro allI impI)
        fix j
        assume "j ≠ i"
        with * have "netmap s2' j = netmap s2 j" by simp
        thus "(netmap s1 ++ netmap s2') j = (netmap s1 ++ netmap s2) j"
          by (metis (opaque_lifting, mono_tags) domD map_add_Some_iff map_add_dom_app_simps(3))
      qed
      ultimately show ?thesis using ‹i∈net_ips s2› subs subs' by auto
    qed simp_all
  qed

end