Theory Pnet
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