Theory OClosed_Transfer
section "Transfer open results onto closed models"
theory OClosed_Transfer
imports Closed OClosed_Lifting
begin
locale openproc =
fixes np :: "ip ⇒ ('s, ('m::msg) seq_action) automaton"
and onp :: "ip ⇒ ((ip ⇒ 'g) × 'l, 'm seq_action) automaton"
and sr :: "'s ⇒ ('g × 'l)"
assumes init: "{ (σ, ζ) |σ ζ s. s ∈ init (np i)
∧ (σ i, ζ) = sr s
∧ (∀j. j≠i ⟶ σ j ∈ (fst o sr) ` init (np j)) } ⊆ init (onp i)"
and init_notempty: "∀j. init (np j) ≠ {}"
and trans: "⋀s a s' σ σ'. ⟦ σ i = fst (sr s);
σ' i = fst (sr s');
(s, a, s') ∈ trans (np i) ⟧
⟹ ((σ, snd (sr s)), a, (σ', snd (sr s'))) ∈ trans (onp i)"
begin
lemma init_pnet_p_NodeS:
assumes "NodeS i s R ∈ init (pnet np p)"
shows "p = ⟨i; R⟩"
using assms by (cases p) (auto simp add: node_comps)
lemma init_pnet_p_SubnetS:
assumes "SubnetS s1 s2 ∈ init (pnet np p)"
obtains p1 p2 where "p = (p1 ∥ p2)"
and "s1 ∈ init (pnet np p1)"
and "s2 ∈ init (pnet np p2)"
using assms by (cases p) (auto simp add: node_comps)
lemma init_pnet_fst_sr_netgmap:
assumes "s ∈ init (pnet np p)"
and "i ∈ net_ips s"
and "wf_net_tree p"
shows "the (fst (netgmap sr s) i) ∈ (fst ∘ sr) ` init (np i)"
using assms proof (induction s arbitrary: p)
fix ii s R⇩i p
assume "NodeS ii s R⇩i ∈ init (pnet np p)"
and "i ∈ net_ips (NodeS ii s R⇩i)"
and "wf_net_tree p"
note this(1)
moreover then have "p = ⟨ii; R⇩i⟩"
by (rule init_pnet_p_NodeS)
ultimately have "s ∈ init (np ii)"
by (clarsimp simp: node_comps)
with ‹i ∈ net_ips (NodeS ii s R⇩i)›
show "the (fst (netgmap sr (NodeS ii s R⇩i)) i) ∈ (fst ∘ sr) ` init (np i)"
by clarsimp
next
fix s1 s2 p
assume IH1: "⋀p. s1 ∈ init (pnet np p)
⟹ i ∈ net_ips s1
⟹ wf_net_tree p
⟹ the (fst (netgmap sr s1) i) ∈ (fst ∘ sr) ` init (np i)"
and IH2: "⋀p. s2 ∈ init (pnet np p)
⟹ i ∈ net_ips s2
⟹ wf_net_tree p
⟹ the (fst (netgmap sr s2) i) ∈ (fst ∘ sr) ` init (np i)"
and "SubnetS s1 s2 ∈ init (pnet np p)"
and "i ∈ net_ips (SubnetS s1 s2)"
and "wf_net_tree p"
from this(3) obtain p1 p2 where "p = (p1 ∥ p2)"
and "s1 ∈ init (pnet np p1)"
and "s2 ∈ init (pnet np p2)"
by (rule init_pnet_p_SubnetS)
from this(1) and ‹wf_net_tree p› have "wf_net_tree p1"
and "wf_net_tree p2"
and "net_tree_ips p1 ∩ net_tree_ips p2 = {}"
by auto
from ‹i ∈ net_ips (SubnetS s1 s2)› have "i ∈ net_ips s1 ∨ i ∈ net_ips s2"
by simp
thus "the (fst (netgmap sr (SubnetS s1 s2)) i) ∈ (fst ∘ sr) ` init (np i)"
proof
assume "i ∈ net_ips s1"
hence "i ∉ net_ips s2"
proof -
from ‹s1 ∈ init (pnet np p1)› and ‹i ∈ net_ips s1› have "i∈net_tree_ips p1" ..
with ‹net_tree_ips p1 ∩ net_tree_ips p2 = {}› have "i∉net_tree_ips p2" by auto
with ‹s2 ∈ init (pnet np p2)› show ?thesis ..
qed
moreover from ‹s1 ∈ init (pnet np p1)› ‹i ∈ net_ips s1› and ‹wf_net_tree p1›
have "the (fst (netgmap sr s1) i) ∈ (fst ∘ sr) ` init (np i)"
by (rule IH1)
ultimately show ?thesis by simp
next
assume "i ∈ net_ips s2"
moreover with ‹s2 ∈ init (pnet np p2)› have "the (fst (netgmap sr s2) i) ∈ (fst ∘ sr) ` init (np i)"
using ‹wf_net_tree p2› by (rule IH2)
moreover from ‹s2 ∈ init (pnet np p2)› and ‹i ∈ net_ips s2› have "i∈net_tree_ips p2" ..
ultimately show ?thesis by simp
qed
qed
lemma init_lifted:
assumes "wf_net_tree p"
shows "{ (σ, snd (netgmap sr s)) |σ s. s ∈ init (pnet np p)
∧ (∀i. if i∈net_tree_ips p then σ i = the (fst (netgmap sr s) i)
else σ i ∈ (fst o sr) ` init (np i)) } ⊆ init (opnet onp p)"
using assms proof (induction p)
fix i R
assume "wf_net_tree ⟨i; R⟩"
show "{(σ, snd (netgmap sr s)) |σ s. s ∈ init (pnet np ⟨i; R⟩)
∧ (∀j. if j ∈ net_tree_ips ⟨i; R⟩ then σ j = the (fst (netgmap sr s) j)
else σ j ∈ (fst ∘ sr) ` init (np j))} ⊆ init (opnet onp ⟨i; R⟩)"
by (clarsimp simp add: node_comps onode_comps)
(rule subsetD [OF init], auto)
next
fix p1 p2
assume IH1: "wf_net_tree p1
⟹ {(σ, snd (netgmap sr s)) |σ s. s ∈ init (pnet np p1)
∧ (∀i. if i ∈ net_tree_ips p1 then σ i = the (fst (netgmap sr s) i)
else σ i ∈ (fst ∘ sr) ` init (np i))} ⊆ init (opnet onp p1)"
(is "_ ⟹ ?S1 ⊆ _")
and IH2: "wf_net_tree p2
⟹ {(σ, snd (netgmap sr s)) |σ s. s ∈ init (pnet np p2)
∧ (∀i. if i ∈ net_tree_ips p2 then σ i = the (fst (netgmap sr s) i)
else σ i ∈ (fst ∘ sr) ` init (np i))} ⊆ init (opnet onp p2)"
(is "_ ⟹ ?S2 ⊆ _")
and "wf_net_tree (p1 ∥ p2)"
from this(3) have "wf_net_tree p1"
and "wf_net_tree p2"
and "net_tree_ips p1 ∩ net_tree_ips p2 = {}" by auto
show "{(σ, snd (netgmap sr s)) |σ s. s ∈ init (pnet np (p1 ∥ p2))
∧ (∀i. if i ∈ net_tree_ips (p1 ∥ p2) then σ i = the (fst (netgmap sr s) i)
else σ i ∈ (fst ∘ sr) ` init (np i))} ⊆ init (opnet onp (p1 ∥ p2))"
proof (rule, clarsimp simp only: split_paired_all pnet.simps automaton.simps)
fix σ s1 s2
assume σ_desc: "∀i. if i ∈ net_tree_ips (p1 ∥ p2)
then σ i = the (fst (netgmap sr (SubnetS s1 s2)) i)
else σ i ∈ (fst ∘ sr) ` init (np i)"
and "s1 ∈ init (pnet np p1)"
and "s2 ∈ init (pnet np p2)"
from this(2-3) have "net_ips s1 = net_tree_ips p1"
and "net_ips s2 = net_tree_ips p2" by auto
have "(σ, snd (netgmap sr s1)) ∈ ?S1"
proof -
{ fix i
assume "i ∈ net_tree_ips p1"
with ‹net_tree_ips p1 ∩ net_tree_ips p2 = {}› have "i ∉ net_tree_ips p2" by auto
with ‹s2 ∈ init (pnet np p2)› have "i ∉ net_ips s2" ..
hence "the ((fst (netgmap sr s1) ++ fst (netgmap sr s2)) i) = the (fst (netgmap sr s1) i)"
by simp
}
moreover
{ fix i
assume "i ∉ net_tree_ips p1"
have "σ i ∈ (fst ∘ sr) ` init (np i)"
proof (cases "i ∈ net_tree_ips p2")
assume "i ∉ net_tree_ips p2"
with ‹i ∉ net_tree_ips p1› and σ_desc show ?thesis
by (auto dest: spec [of _ i])
next
assume "i ∈ net_tree_ips p2"
with ‹s2 ∈ init (pnet np p2)› have "i ∈ net_ips s2" ..
with ‹s2 ∈ init (pnet np p2)› have "the (fst (netgmap sr s2) i) ∈ (fst ∘ sr) ` init (np i)"
using ‹wf_net_tree p2› by (rule init_pnet_fst_sr_netgmap)
with ‹i∈net_tree_ips p2› and ‹i∈net_ips s2› show ?thesis
using σ_desc by simp
qed
}
ultimately show ?thesis
using ‹s1 ∈ init (pnet np p1)› and σ_desc by auto
qed
hence "(σ, snd (netgmap sr s1)) ∈ init (opnet onp p1)"
by (rule subsetD [OF IH1 [OF ‹wf_net_tree p1›]])
have "(σ, snd (netgmap sr s2)) ∈ ?S2"
proof -
{ fix i
assume "i ∈ net_tree_ips p2"
with ‹s2 ∈ init (pnet np p2)› have "i ∈ net_ips s2" ..
hence "the ((fst (netgmap sr s1) ++ fst (netgmap sr s2)) i) = the (fst (netgmap sr s2) i)"
by simp
}
moreover
{ fix i
assume "i ∉ net_tree_ips p2"
have "σ i ∈ (fst ∘ sr) ` init (np i)"
proof (cases "i ∈ net_tree_ips p1")
assume "i ∉ net_tree_ips p1"
with ‹i ∉ net_tree_ips p2› and σ_desc show ?thesis
by (auto dest: spec [of _ i])
next
assume "i ∈ net_tree_ips p1"
with ‹s1 ∈ init (pnet np p1)› have "i ∈ net_ips s1" ..
with ‹s1 ∈ init (pnet np p1)› have "the (fst (netgmap sr s1) i) ∈ (fst ∘ sr) ` init (np i)"
using ‹wf_net_tree p1› by (rule init_pnet_fst_sr_netgmap)
moreover from ‹s2 ∈ init (pnet np p2)› and ‹i ∉ net_tree_ips p2› have "i∉net_ips s2" ..
ultimately show ?thesis
using ‹i∈net_tree_ips p1› ‹i∈net_ips s1› and ‹i∉net_tree_ips p2› σ_desc by simp
qed
}
ultimately show ?thesis
using ‹s2 ∈ init (pnet np p2)› and σ_desc by auto
qed
hence "(σ, snd (netgmap sr s2)) ∈ init (opnet onp p2)"
by (rule subsetD [OF IH2 [OF ‹wf_net_tree p2›]])
with ‹(σ, snd (netgmap sr s1)) ∈ init (opnet onp p1)›
show "(σ, snd (netgmap sr (SubnetS s1 s2))) ∈ init (opnet onp (p1 ∥ p2))"
using ‹net_tree_ips p1 ∩ net_tree_ips p2 = {}›
‹net_ips s1 = net_tree_ips p1›
‹net_ips s2 = net_tree_ips p2› by simp
qed
qed
lemma init_pnet_opnet [elim]:
assumes "wf_net_tree p"
and "s ∈ init (pnet np p)"
shows "netgmap sr s ∈ netmask (net_tree_ips p) ` init (opnet onp p)"
proof -
from ‹wf_net_tree p›
have "{ (σ, snd (netgmap sr s)) |σ s. s ∈ init (pnet np p)
∧ (∀i. if i∈net_tree_ips p then σ i = the (fst (netgmap sr s) i)
else σ i ∈ (fst o sr) ` init (np i)) } ⊆ init (opnet onp p)"
(is "?S ⊆ _")
by (rule init_lifted)
hence "netmask (net_tree_ips p) ` ?S ⊆ netmask (net_tree_ips p) ` init (opnet onp p)"
by (rule image_mono)
moreover have "netgmap sr s ∈ netmask (net_tree_ips p) ` ?S"
proof -
{ fix i
from init_notempty have "∃s. s ∈ (fst ∘ sr) ` init (np i)" by auto
hence "(SOME x. x ∈ (fst ∘ sr) ` init (np i)) ∈ (fst ∘ sr) ` init (np i)" ..
}
with ‹s ∈ init (pnet np p)› and init_notempty
have "(λi. if i ∈ net_tree_ips p
then the (fst (netgmap sr s) i)
else SOME x. x ∈ (fst ∘ sr) ` init (np i), snd (netgmap sr s)) ∈ ?S"
(is "?s ∈ ?S") by auto
moreover have "netgmap sr s = netmask (net_tree_ips p) ?s"
proof (intro prod_eqI ext)
fix i
show "fst (netgmap sr s) i = fst (netmask (net_tree_ips p) ?s) i"
proof (cases "i ∈ net_tree_ips p")
assume "i ∈ net_tree_ips p"
with ‹s∈init (pnet np p)› have "i∈net_ips s" ..
hence "Some (the (fst (netgmap sr s) i)) = fst (netgmap sr s) i"
by (rule some_the_fst_netgmap)
with ‹i∈net_tree_ips p› show ?thesis
by simp
next
assume "i ∉ net_tree_ips p"
moreover with ‹s∈init (pnet np p)› have "i∉net_ips s" ..
ultimately show ?thesis
by simp
qed
qed simp
ultimately show ?thesis
by (rule rev_image_eqI)
qed
ultimately show ?thesis
by (rule rev_subsetD [rotated])
qed
lemma transfer_connect:
assumes "(s, connect(i, i'), s') ∈ trans (pnet np n)"
and "s ∈ reachable (pnet np n) TT"
and "netgmap sr s = netmask (net_tree_ips n) (σ, ζ)"
and "wf_net_tree n"
obtains σ' ζ' where "((σ, ζ), connect(i, i'), (σ', ζ')) ∈ trans (opnet onp n)"
and "∀j. j∉net_ips ζ ⟶ σ' j = σ j"
and "netgmap sr s' = netmask (net_tree_ips n) (σ', ζ')"
proof atomize_elim
from assms have "((σ, snd (netgmap sr s)), connect(i, i'), (σ, snd (netgmap sr s'))) ∈ trans (opnet onp n)
∧ netgmap sr s' = netmask (net_tree_ips n) (σ, snd (netgmap sr s'))"
proof (induction n arbitrary: s s' ζ)
fix ii R⇩i ns ns' ζ
assume "(ns, connect(i, i'), ns') ∈ trans (pnet np ⟨ii; R⇩i⟩)"
and "netgmap sr ns = netmask (net_tree_ips ⟨ii; R⇩i⟩) (σ, ζ)"
from this(1) have "(ns, connect(i, i'), ns') ∈ node_sos (trans (np ii))"
by (simp add: node_comps)
moreover then obtain ni s s' R R' where "ns = NodeS ni s R"
and "ns' = NodeS ni s' R'" ..
ultimately have "(NodeS ni s R, connect(i, i'), NodeS ni s' R') ∈ node_sos (trans (np ii))"
by simp
moreover then have "s' = s" by auto
ultimately have "((σ, NodeS ni (snd (sr s)) R), connect(i, i'), (σ, NodeS ni (snd (sr s)) R'))
∈ onode_sos (trans (onp ii))"
by - (rule node_connectTE', auto intro!: onode_sos.intros [simplified])
with ‹ns = NodeS ni s R› ‹ns' = NodeS ni s' R'› ‹s' = s›
and ‹netgmap sr ns = netmask (net_tree_ips ⟨ii; R⇩i⟩) (σ, ζ)›
show "((σ, snd (netgmap sr ns)), connect(i, i'), (σ, snd (netgmap sr ns'))) ∈ trans (opnet onp ⟨ii; R⇩i⟩)
∧ netgmap sr ns' = netmask (net_tree_ips ⟨ii; R⇩i⟩) (σ, snd (netgmap sr ns'))"
by (simp add: onode_comps)
next
fix n1 n2 s s' ζ
assume IH1: "⋀s s' ζ. (s, connect(i, i'), s') ∈ trans (pnet np n1)
⟹ s ∈ reachable (pnet np n1) TT
⟹ netgmap sr s = netmask (net_tree_ips n1) (σ, ζ)
⟹ wf_net_tree n1
⟹ ((σ, snd (netgmap sr s)), connect(i, i'), (σ, snd (netgmap sr s'))) ∈ trans (opnet onp n1)
∧ netgmap sr s' = netmask (net_tree_ips n1) (σ, snd (netgmap sr s'))"
and IH2: "⋀s s' ζ. (s, connect(i, i'), s') ∈ trans (pnet np n2)
⟹ s ∈ reachable (pnet np n2) TT
⟹ netgmap sr s = netmask (net_tree_ips n2) (σ, ζ)
⟹ wf_net_tree n2
⟹ ((σ, snd (netgmap sr s)), connect(i, i'), (σ, snd (netgmap sr s'))) ∈ trans (opnet onp n2)
∧ netgmap sr s' = netmask (net_tree_ips n2) (σ, snd (netgmap sr s'))"
and tr: "(s, connect(i, i'), s') ∈ trans (pnet np (n1 ∥ n2))"
and sr: "s ∈ reachable (pnet np (n1 ∥ n2)) TT"
and nm: "netgmap sr s = netmask (net_tree_ips (n1 ∥ n2)) (σ, ζ)"
and "wf_net_tree (n1 ∥ n2)"
from this(3) have "(s, connect(i, i'), s') ∈ pnet_sos (trans (pnet np n1))
(trans (pnet np n2))"
by simp
then obtain s1 s1' s2 s2' where "s = SubnetS s1 s2"
and "s' = SubnetS s1' s2'"
and "(s1, connect(i, i'), s1') ∈ trans (pnet np n1)"
and "(s2, connect(i, i'), s2') ∈ trans (pnet np n2)"
by (rule partial_connectTE) auto
from this(1) and nm have "netgmap sr (SubnetS s1 s2) = netmask (net_tree_ips (n1 ∥ n2)) (σ, ζ)"
by simp
from ‹wf_net_tree (n1 ∥ n2)› have "wf_net_tree n1" and "wf_net_tree n2"
and "net_tree_ips n1 ∩ net_tree_ips n2 = {}" by auto
from sr ‹s = SubnetS s1 s2› have "s1 ∈ reachable (pnet np n1) TT" by (metis subnet_reachable(1))
hence "net_ips s1 = net_tree_ips n1" by (rule pnet_net_ips_net_tree_ips)
from sr ‹s = SubnetS s1 s2› have "s2 ∈ reachable (pnet np n2) TT" by (metis subnet_reachable(2))
hence "net_ips s2 = net_tree_ips n2" by (rule pnet_net_ips_net_tree_ips)
from nm ‹s = SubnetS s1 s2›
have "netgmap sr (SubnetS s1 s2) = netmask (net_tree_ips (n1 ∥ n2)) (σ, ζ)" by simp
hence "netgmap sr s1 = netmask (net_tree_ips n1) (σ, snd (netgmap sr s1))"
using ‹net_tree_ips n1 ∩ net_tree_ips n2 = {}› ‹net_ips s1 = net_tree_ips n1›
and ‹net_ips s2 = net_tree_ips n2› by (rule netgmap_subnet_split1)
with ‹(s1, connect(i, i'), s1') ∈ trans (pnet np n1)›
and ‹s1 ∈ reachable (pnet np n1) TT›
have "((σ, snd (netgmap sr s1)), connect(i, i'), (σ, snd (netgmap sr s1'))) ∈ trans (opnet onp n1)"
and "netgmap sr s1' = netmask (net_tree_ips n1) (σ, snd (netgmap sr s1'))"
using ‹wf_net_tree n1› unfolding atomize_conj by (rule IH1)
from ‹netgmap sr (SubnetS s1 s2) = netmask (net_tree_ips (n1 ∥ n2)) (σ, ζ)›
‹net_ips s1 = net_tree_ips n1› and ‹net_ips s2 = net_tree_ips n2›
have "netgmap sr s2 = netmask (net_tree_ips n2) (σ, snd (netgmap sr s2))"
by (rule netgmap_subnet_split2)
with ‹(s2, connect(i, i'), s2') ∈ trans (pnet np n2)›
and ‹s2 ∈ reachable (pnet np n2) TT›
have "((σ, snd (netgmap sr s2)), connect(i, i'), (σ, snd (netgmap sr s2'))) ∈ trans (opnet onp n2)"
and "netgmap sr s2' = netmask (net_tree_ips n2) (σ, snd (netgmap sr s2'))"
using ‹wf_net_tree n2› unfolding atomize_conj by (rule IH2)
have "((σ, snd (netgmap sr s)), connect(i, i'), (σ, snd (netgmap sr s')))
∈ trans (opnet onp (n1 ∥ n2))"
proof -
from ‹((σ, snd (netgmap sr s1)), connect(i, i'), (σ, snd (netgmap sr s1'))) ∈ trans (opnet onp n1)›
and ‹((σ, snd (netgmap sr s2)), connect(i, i'), (σ, snd (netgmap sr s2'))) ∈ trans (opnet onp n2)›
have "((σ, SubnetS (snd (netgmap sr s1)) (snd (netgmap sr s2))), connect(i, i'),
(σ, SubnetS (snd (netgmap sr s1')) (snd (netgmap sr s2'))))
∈ opnet_sos (trans (opnet onp n1)) (trans (opnet onp n2))"
by (rule opnet_connect)
with ‹s = SubnetS s1 s2› ‹s' = SubnetS s1' s2'› show ?thesis by simp
qed
moreover from ‹netgmap sr s1' = netmask (net_tree_ips n1) (σ, snd (netgmap sr s1'))›
‹netgmap sr s2' = netmask (net_tree_ips n2) (σ, snd (netgmap sr s2'))›
‹s' = SubnetS s1' s2'›
have "netgmap sr s' = netmask (net_tree_ips (n1 ∥ n2)) (σ, snd (netgmap sr s'))" ..
ultimately show "((σ, snd (netgmap sr s)), connect(i, i'), (σ, snd (netgmap sr s')))
∈ trans (opnet onp (n1 ∥ n2))
∧ netgmap sr s' = netmask (net_tree_ips (n1 ∥ n2)) (σ, snd (netgmap sr s'))" ..
qed
moreover from ‹netgmap sr s = netmask (net_tree_ips n) (σ, ζ)› have "ζ = snd (netgmap sr s)" by simp
ultimately show " ∃σ' ζ'. ((σ, ζ), connect(i, i'), (σ', ζ')) ∈ trans (opnet onp n)
∧ (∀j. j ∉ net_ips ζ ⟶ σ' j = σ j)
∧ netgmap sr s' = netmask (net_tree_ips n) (σ', ζ')" by auto
qed
lemma transfer_disconnect:
assumes "(s, disconnect(i, i'), s') ∈ trans (pnet np n)"
and "s ∈ reachable (pnet np n) TT"
and "netgmap sr s = netmask (net_tree_ips n) (σ, ζ)"
and "wf_net_tree n"
obtains σ' ζ' where "((σ, ζ), disconnect(i, i'), (σ', ζ')) ∈ trans (opnet onp n)"
and "∀j. j∉net_ips ζ ⟶ σ' j = σ j"
and "netgmap sr s' = netmask (net_tree_ips n) (σ', ζ')"
proof atomize_elim
from assms have "((σ, snd (netgmap sr s)), disconnect(i, i'), (σ, snd (netgmap sr s'))) ∈ trans (opnet onp n)
∧ netgmap sr s' = netmask (net_tree_ips n) (σ, snd (netgmap sr s'))"
proof (induction n arbitrary: s s' ζ)
fix ii R⇩i ns ns' ζ
assume "(ns, disconnect(i, i'), ns') ∈ trans (pnet np ⟨ii; R⇩i⟩)"
and "netgmap sr ns = netmask (net_tree_ips ⟨ii; R⇩i⟩) (σ, ζ)"
from this(1) have "(ns, disconnect(i, i'), ns') ∈ node_sos (trans (np ii))"
by (simp add: node_comps)
moreover then obtain ni s s' R R' where "ns = NodeS ni s R"
and "ns' = NodeS ni s' R'" ..
ultimately have "(NodeS ni s R, disconnect(i, i'), NodeS ni s' R') ∈ node_sos (trans (np ii))"
by simp
moreover then have "s' = s" by auto
ultimately have "((σ, NodeS ni (snd (sr s)) R), disconnect(i, i'), (σ, NodeS ni (snd (sr s)) R'))
∈ onode_sos (trans (onp ii))"
by - (rule node_disconnectTE', auto intro!: onode_sos.intros [simplified])
with ‹ns = NodeS ni s R› ‹ns' = NodeS ni s' R'› ‹s' = s›
and ‹netgmap sr ns = netmask (net_tree_ips ⟨ii; R⇩i⟩) (σ, ζ)›
show "((σ, snd (netgmap sr ns)), disconnect(i, i'), (σ, snd (netgmap sr ns'))) ∈ trans (opnet onp ⟨ii; R⇩i⟩)
∧ netgmap sr ns' = netmask (net_tree_ips ⟨ii; R⇩i⟩) (σ, snd (netgmap sr ns'))"
by (simp add: onode_comps)
next
fix n1 n2 s s' ζ
assume IH1: "⋀s s' ζ. (s, disconnect(i, i'), s') ∈ trans (pnet np n1)
⟹ s ∈ reachable (pnet np n1) TT
⟹ netgmap sr s = netmask (net_tree_ips n1) (σ, ζ)
⟹ wf_net_tree n1
⟹ ((σ, snd (netgmap sr s)), disconnect(i, i'), (σ, snd (netgmap sr s'))) ∈ trans (opnet onp n1)
∧ netgmap sr s' = netmask (net_tree_ips n1) (σ, snd (netgmap sr s'))"
and IH2: "⋀s s' ζ. (s, disconnect(i, i'), s') ∈ trans (pnet np n2)
⟹ s ∈ reachable (pnet np n2) TT
⟹ netgmap sr s = netmask (net_tree_ips n2) (σ, ζ)
⟹ wf_net_tree n2
⟹ ((σ, snd (netgmap sr s)), disconnect(i, i'), (σ, snd (netgmap sr s'))) ∈ trans (opnet onp n2)
∧ netgmap sr s' = netmask (net_tree_ips n2) (σ, snd (netgmap sr s'))"
and tr: "(s, disconnect(i, i'), s') ∈ trans (pnet np (n1 ∥ n2))"
and sr: "s ∈ reachable (pnet np (n1 ∥ n2)) TT"
and nm: "netgmap sr s = netmask (net_tree_ips (n1 ∥ n2)) (σ, ζ)"
and "wf_net_tree (n1 ∥ n2)"
from this(3) have "(s, disconnect(i, i'), s') ∈ pnet_sos (trans (pnet np n1))
(trans (pnet np n2))"
by simp
then obtain s1 s1' s2 s2' where "s = SubnetS s1 s2"
and "s' = SubnetS s1' s2'"
and "(s1, disconnect(i, i'), s1') ∈ trans (pnet np n1)"
and "(s2, disconnect(i, i'), s2') ∈ trans (pnet np n2)"
by (rule partial_disconnectTE) auto
from this(1) and nm have "netgmap sr (SubnetS s1 s2) = netmask (net_tree_ips (n1 ∥ n2)) (σ, ζ)"
by simp
from ‹wf_net_tree (n1 ∥ n2)› have "wf_net_tree n1" and "wf_net_tree n2"
and "net_tree_ips n1 ∩ net_tree_ips n2 = {}" by auto
from sr ‹s = SubnetS s1 s2› have "s1 ∈ reachable (pnet np n1) TT" by (metis subnet_reachable(1))
hence "net_ips s1 = net_tree_ips n1" by (rule pnet_net_ips_net_tree_ips)
from sr ‹s = SubnetS s1 s2› have "s2 ∈ reachable (pnet np n2) TT" by (metis subnet_reachable(2))
hence "net_ips s2 = net_tree_ips n2" by (rule pnet_net_ips_net_tree_ips)
from nm ‹s = SubnetS s1 s2›
have "netgmap sr (SubnetS s1 s2) = netmask (net_tree_ips (n1 ∥ n2)) (σ, ζ)" by simp
hence "netgmap sr s1 = netmask (net_tree_ips n1) (σ, snd (netgmap sr s1))"
using ‹net_tree_ips n1 ∩ net_tree_ips n2 = {}› ‹net_ips s1 = net_tree_ips n1›
and ‹net_ips s2 = net_tree_ips n2› by (rule netgmap_subnet_split1)
with ‹(s1, disconnect(i, i'), s1') ∈ trans (pnet np n1)›
and ‹s1 ∈ reachable (pnet np n1) TT›
have "((σ, snd (netgmap sr s1)), disconnect(i, i'), (σ, snd (netgmap sr s1'))) ∈ trans (opnet onp n1)"
and "netgmap sr s1' = netmask (net_tree_ips n1) (σ, snd (netgmap sr s1'))"
using ‹wf_net_tree n1› unfolding atomize_conj by (rule IH1)
from ‹netgmap sr (SubnetS s1 s2) = netmask (net_tree_ips (n1 ∥ n2)) (σ, ζ)›
‹net_ips s1 = net_tree_ips n1› and ‹net_ips s2 = net_tree_ips n2›
have "netgmap sr s2 = netmask (net_tree_ips n2) (σ, snd (netgmap sr s2))"
by (rule netgmap_subnet_split2)
with ‹(s2, disconnect(i, i'), s2') ∈ trans (pnet np n2)›
and ‹s2 ∈ reachable (pnet np n2) TT›
have "((σ, snd (netgmap sr s2)), disconnect(i, i'), (σ, snd (netgmap sr s2'))) ∈ trans (opnet onp n2)"
and "netgmap sr s2' = netmask (net_tree_ips n2) (σ, snd (netgmap sr s2'))"
using ‹wf_net_tree n2› unfolding atomize_conj by (rule IH2)
have "((σ, snd (netgmap sr s)), disconnect(i, i'), (σ, snd (netgmap sr s')))
∈ trans (opnet onp (n1 ∥ n2))"
proof -
from ‹((σ, snd (netgmap sr s1)), disconnect(i, i'), (σ, snd (netgmap sr s1'))) ∈ trans (opnet onp n1)›
and ‹((σ, snd (netgmap sr s2)), disconnect(i, i'), (σ, snd (netgmap sr s2'))) ∈ trans (opnet onp n2)›
have "((σ, SubnetS (snd (netgmap sr s1)) (snd (netgmap sr s2))), disconnect(i, i'),
(σ, SubnetS (snd (netgmap sr s1')) (snd (netgmap sr s2'))))
∈ opnet_sos (trans (opnet onp n1)) (trans (opnet onp n2))"
by (rule opnet_disconnect)
with ‹s = SubnetS s1 s2› ‹s' = SubnetS s1' s2'› show ?thesis by simp
qed
moreover from ‹netgmap sr s1' = netmask (net_tree_ips n1) (σ, snd (netgmap sr s1'))›
‹netgmap sr s2' = netmask (net_tree_ips n2) (σ, snd (netgmap sr s2'))›
‹s' = SubnetS s1' s2'›
have "netgmap sr s' = netmask (net_tree_ips (n1 ∥ n2)) (σ, snd (netgmap sr s'))" ..
ultimately show "((σ, snd (netgmap sr s)), disconnect(i, i'), (σ, snd (netgmap sr s')))
∈ trans (opnet onp (n1 ∥ n2))
∧ netgmap sr s' = netmask (net_tree_ips (n1 ∥ n2)) (σ, snd (netgmap sr s'))" ..
qed
moreover from ‹netgmap sr s = netmask (net_tree_ips n) (σ, ζ)› have "ζ = snd (netgmap sr s)" by simp
ultimately show "∃σ' ζ'. ((σ, ζ), disconnect(i, i'), (σ', ζ')) ∈ trans (opnet onp n)
∧ (∀j. j ∉ net_ips ζ ⟶ σ' j = σ j)
∧ netgmap sr s' = netmask (net_tree_ips n) (σ', ζ')" by auto
qed
lemma transfer_tau:
assumes "(s, τ, s') ∈ trans (pnet np n)"
and "s ∈ reachable (pnet np n) TT"
and "netgmap sr s = netmask (net_tree_ips n) (σ, ζ)"
and "wf_net_tree n"
obtains σ' ζ' where "((σ, ζ), τ, (σ', ζ')) ∈ trans (opnet onp n)"
and "∀j. j∉net_ips ζ ⟶ σ' j = σ j"
and "netgmap sr s' = netmask (net_tree_ips n) (σ', ζ')"
proof atomize_elim
from assms(4,2,1) obtain i where "i∈net_ips s"
and "∀j. j≠i ⟶ netmap s' j = netmap s j"
and "net_ip_action np τ i n s s'"
by (metis pnet_tau_single_node)
from this(2) have "∀j. j≠i ⟶ fst (netgmap sr s') j = fst (netgmap sr s) j"
by (clarsimp intro!: netmap_is_fst_netgmap')
from ‹(s, τ, s') ∈ trans (pnet np n)› have "net_ips s' = net_ips s"
by (rule pnet_maintains_dom [THEN sym])
define σ' where "σ' j = (if j = i then the (fst (netgmap sr s') i) else σ j)" for j
from ‹∀j. j≠i ⟶ fst (netgmap sr s') j = fst (netgmap sr s) j›
and ‹netgmap sr s = netmask (net_tree_ips n) (σ, ζ)›
have "∀j. j≠i ⟶ σ' j = σ j"
unfolding σ'_def by clarsimp
from assms(2) have "net_ips s = net_tree_ips n"
by (rule pnet_net_ips_net_tree_ips)
from ‹netgmap sr s = netmask (net_tree_ips n) (σ, ζ)›
have "ζ = snd (netgmap sr s)" by simp
from ‹∀j. j≠i ⟶ fst (netgmap sr s') j = fst (netgmap sr s) j› ‹i ∈ net_ips s›
‹net_ips s = net_tree_ips n› ‹net_ips s' = net_ips s›
‹netgmap sr s = netmask (net_tree_ips n) (σ, ζ)›
have "fst (netgmap sr s') = fst (netmask (net_tree_ips n) (σ', snd (netgmap sr s')))"
unfolding σ'_def [abs_def] by - (rule ext, clarsimp)
hence "netgmap sr s' = netmask (net_tree_ips n) (σ', snd (netgmap sr s'))"
by (rule prod_eqI, simp)
with assms(1, 3)
have "((σ, snd (netgmap sr s)), τ, (σ', snd (netgmap sr s'))) ∈ trans (opnet onp n)"
using assms(2,4) ‹i∈net_ips s› and ‹net_ip_action np τ i n s s'›
proof (induction n arbitrary: s s' ζ)
fix ii R⇩i ns ns' ζ
assume "(ns, τ, ns') ∈ trans (pnet np ⟨ii; R⇩i⟩)"
and nsr: "ns ∈ reachable (pnet np ⟨ii; R⇩i⟩) TT"
and "netgmap sr ns = netmask (net_tree_ips ⟨ii; R⇩i⟩) (σ, ζ)"
and "netgmap sr ns' = netmask (net_tree_ips ⟨ii; R⇩i⟩) (σ', snd (netgmap sr ns'))"
and "i∈net_ips ns"
from this(1) have "(ns, τ, ns') ∈ node_sos (trans (np ii))"
by (simp add: node_comps)
moreover with nsr obtain s s' R R' where "ns = NodeS ii s R"
and "ns' = NodeS ii s' R'"
by (metis net_node_reachable_is_node node_tauTE')
moreover from ‹i ∈ net_ips ns› and ‹ns = NodeS ii s R› have "ii = i" by simp
ultimately have ntr: "(NodeS i s R, τ, NodeS i s' R') ∈ node_sos (trans (np i))"
by simp
hence "R' = R" by (metis net_state.inject(1) node_tauTE')
from ntr obtain a where "(s, a, s') ∈ trans (np i)"
and "(∃d. a = ¬unicast d ∧ d∉R) ∨ (a = τ)"
by (rule node_tauTE') auto
from ‹netgmap sr ns = netmask (net_tree_ips ⟨ii; R⇩i⟩) (σ, ζ)› ‹ns = NodeS ii s R› and ‹ii = i›
have "σ i = fst (sr s)" by simp (metis map_upd_Some_unfold)
moreover from ‹netgmap sr ns' = netmask (net_tree_ips ⟨ii; R⇩i⟩) (σ', snd (netgmap sr ns'))›
‹ns' = NodeS ii s' R'› and ‹ii = i›
have "σ' i = fst (sr s')"
unfolding σ'_def [abs_def] by clarsimp (hypsubst_thin,
metis (full_types, lifting) fun_upd_same option.sel)
ultimately have "((σ, snd (sr s)), a, (σ', snd (sr s'))) ∈ trans (onp i)"
using ‹(s, a, s') ∈ trans (np i)› by (rule trans)
from ‹(∃d. a = ¬unicast d ∧ d∉R) ∨ (a = τ)› ‹∀j. j≠i ⟶ σ' j = σ j› ‹R'=R›
and ‹((σ, snd (sr s)), a, (σ', snd (sr s'))) ∈ trans (onp i)›
have "((σ, NodeS i (snd (sr s)) R), τ, (σ', NodeS i (snd (sr s')) R')) ∈ onode_sos (trans (onp i))"
by (metis onode_sos.onode_notucast onode_sos.onode_tau)
with ‹ns = NodeS ii s R› ‹ns' = NodeS ii s' R'› ‹ii = i›
show "((σ, snd (netgmap sr ns)), τ, (σ', snd (netgmap sr ns'))) ∈ trans (opnet onp ⟨ii; R⇩i⟩)"
by (simp add: onode_comps)
next
fix n1 n2 s s' ζ
assume IH1: "⋀s s' ζ. (s, τ, s') ∈ trans (pnet np n1)
⟹ netgmap sr s = netmask (net_tree_ips n1) (σ, ζ)
⟹ netgmap sr s' = netmask (net_tree_ips n1) (σ', snd (netgmap sr s'))
⟹ s ∈ reachable (pnet np n1) TT
⟹ wf_net_tree n1
⟹ i∈net_ips s
⟹ net_ip_action np τ i n1 s s'
⟹ ((σ, snd (netgmap sr s)), τ, (σ', snd (netgmap sr s'))) ∈ trans (opnet onp n1)"
and IH2: "⋀s s' ζ. (s, τ, s') ∈ trans (pnet np n2)
⟹ netgmap sr s = netmask (net_tree_ips n2) (σ, ζ)
⟹ netgmap sr s' = netmask (net_tree_ips n2) (σ', snd (netgmap sr s'))
⟹ s ∈ reachable (pnet np n2) TT
⟹ wf_net_tree n2
⟹ i∈net_ips s
⟹ net_ip_action np τ i n2 s s'
⟹ ((σ, snd (netgmap sr s)), τ, (σ', snd (netgmap sr s'))) ∈ trans (opnet onp n2)"
and tr: "(s, τ, s') ∈ trans (pnet np (n1 ∥ n2))"
and sr: "s ∈ reachable (pnet np (n1 ∥ n2)) TT"
and nm: "netgmap sr s = netmask (net_tree_ips (n1 ∥ n2)) (σ, ζ)"
and nm': "netgmap sr s' = netmask (net_tree_ips (n1 ∥ n2)) (σ', snd (netgmap sr s'))"
and "wf_net_tree (n1 ∥ n2)"
and "i∈net_ips s"
and "net_ip_action np τ i (n1 ∥ n2) s s'"
from tr have "(s, τ, s') ∈ pnet_sos (trans (pnet np n1)) (trans (pnet np n2))" by simp
then obtain s1 s1' s2 s2' where "s = SubnetS s1 s2"
and "s' = SubnetS s1' s2'"
by (rule partial_tauTE) auto
from this(1) and nm have "netgmap sr (SubnetS s1 s2) = netmask (net_tree_ips (n1 ∥ n2)) (σ, ζ)"
by simp
from ‹s' = SubnetS s1' s2'› and nm'
have "netgmap sr (SubnetS s1' s2') = netmask (net_tree_ips (n1 ∥ n2)) (σ', snd (netgmap sr s'))"
by simp
from ‹wf_net_tree (n1 ∥ n2)› have "wf_net_tree n1"
and "wf_net_tree n2"
and "net_tree_ips n1 ∩ net_tree_ips n2 = {}" by auto
from sr [simplified ‹s = SubnetS s1 s2›] have "s1 ∈ reachable (pnet np n1) TT"
by (rule subnet_reachable(1))
hence "net_ips s1 = net_tree_ips n1" by (rule pnet_net_ips_net_tree_ips)
from sr [simplified ‹s = SubnetS s1 s2›] have "s2 ∈ reachable (pnet np n2) TT"
by (rule subnet_reachable(2))
hence "net_ips s2 = net_tree_ips n2" by (rule pnet_net_ips_net_tree_ips)
from nm [simplified ‹s = SubnetS s1 s2›]
‹net_tree_ips n1 ∩ net_tree_ips n2 = {}›
‹net_ips s1 = net_tree_ips n1›
‹net_ips s2 = net_tree_ips n2›
have "netgmap sr s1 = netmask (net_tree_ips n1) (σ, snd (netgmap sr s1))"
by (rule netgmap_subnet_split1)
from nm [simplified ‹s = SubnetS s1 s2›]
‹net_ips s1 = net_tree_ips n1›
‹net_ips s2 = net_tree_ips n2›
have "netgmap sr s2 = netmask (net_tree_ips n2) (σ, snd (netgmap sr s2))"
by (rule netgmap_subnet_split2)
from ‹i∈net_ips s› and ‹s = SubnetS s1 s2› have "i∈net_ips s1 ∨ i∈net_ips s2" by auto
thus "((σ, snd (netgmap sr s)), τ, (σ', snd (netgmap sr s'))) ∈ trans (opnet onp (n1 ∥ n2))"
proof
assume "i∈net_ips s1"
with ‹s = SubnetS s1 s2› ‹s' = SubnetS s1' s2'› ‹net_ip_action np τ i (n1 ∥ n2) s s'›
have "(s1, τ, s1') ∈ trans (pnet np n1)"
and "net_ip_action np τ i n1 s1 s1'"
and "s2' = s2" by simp_all
from ‹net_ips s1 = net_tree_ips n1› and ‹(s1, τ, s1') ∈ trans (pnet np n1)›
have "net_ips s1' = net_tree_ips n1" by (metis pnet_maintains_dom)
from nm' [simplified ‹s' = SubnetS s1' s2'› ‹s2' = s2›]
‹net_tree_ips n1 ∩ net_tree_ips n2 = {}›
‹net_ips s1' = net_tree_ips n1›
‹net_ips s2 = net_tree_ips n2›
have "netgmap sr s1' = netmask (net_tree_ips n1) (σ', snd (netgmap sr s1'))"
by (rule netgmap_subnet_split1)
from ‹(s1, τ, s1') ∈ trans (pnet np n1)›
‹netgmap sr s1 = netmask (net_tree_ips n1) (σ, snd (netgmap sr s1))›
‹netgmap sr s1' = netmask (net_tree_ips n1) (σ', snd (netgmap sr s1'))›
‹s1 ∈ reachable (pnet np n1) TT›
‹wf_net_tree n1›
‹i∈net_ips s1›
‹net_ip_action np τ i n1 s1 s1'›
have "((σ, snd (netgmap sr s1)), τ, (σ', snd (netgmap sr s1'))) ∈ trans (opnet onp n1)"
by (rule IH1)
with ‹s = SubnetS s1 s2› ‹s' = SubnetS s1' s2'› ‹s2' = s2› show ?thesis
by (simp del: step_node_tau) (erule opnet_tau1)
next
assume "i∈net_ips s2"
with ‹s = SubnetS s1 s2› ‹s' = SubnetS s1' s2'› ‹net_ip_action np τ i (n1 ∥ n2) s s'›
have "(s2, τ, s2') ∈ trans (pnet np n2)"
and "net_ip_action np τ i n2 s2 s2'"
and "s1' = s1" by simp_all
from ‹net_ips s2 = net_tree_ips n2› and ‹(s2, τ, s2') ∈ trans (pnet np n2)›
have "net_ips s2' = net_tree_ips n2" by (metis pnet_maintains_dom)
from nm' [simplified ‹s' = SubnetS s1' s2'› ‹s1' = s1›]
‹net_ips s1 = net_tree_ips n1›
‹net_ips s2' = net_tree_ips n2›
have "netgmap sr s2' = netmask (net_tree_ips n2) (σ', snd (netgmap sr s2'))"
by (rule netgmap_subnet_split2)
from ‹(s2, τ, s2') ∈ trans (pnet np n2)›
‹netgmap sr s2 = netmask (net_tree_ips n2) (σ, snd (netgmap sr s2))›
‹netgmap sr s2' = netmask (net_tree_ips n2) (σ', snd (netgmap sr s2'))›
‹s2 ∈ reachable (pnet np n2) TT›
‹wf_net_tree n2›
‹i∈net_ips s2›
‹net_ip_action np τ i n2 s2 s2'›
have "((σ, snd (netgmap sr s2)), τ, (σ', snd (netgmap sr s2'))) ∈ trans (opnet onp n2)"
by (rule IH2)
with ‹s = SubnetS s1 s2› ‹s' = SubnetS s1' s2'› ‹s1' = s1› show ?thesis
by (simp del: step_node_tau) (erule opnet_tau2)
qed
qed
with ‹ζ = snd (netgmap sr s)› have "((σ, ζ), τ, (σ', snd (netgmap sr s'))) ∈ trans (opnet onp n)"
by simp
moreover from ‹∀j. j≠i ⟶ σ' j = σ j› ‹i ∈ net_ips s› ‹ζ = snd (netgmap sr s)›
have "∀j. j∉net_ips ζ ⟶ σ' j = σ j" by (metis net_ips_netgmap)
ultimately have "((σ, ζ), τ, (σ', snd (netgmap sr s'))) ∈ trans (opnet onp n)
∧ (∀j. j∉net_ips ζ ⟶ σ' j = σ j)
∧ netgmap sr s' = netmask (net_tree_ips n) (σ', snd (netgmap sr s'))"
using ‹netgmap sr s' = netmask (net_tree_ips n) (σ', snd (netgmap sr s'))› by simp
thus "∃σ' ζ'. ((σ, ζ), τ, (σ', ζ')) ∈ trans (opnet onp n)
∧ (∀j. j∉net_ips ζ ⟶ σ' j = σ j)
∧ netgmap sr s' = netmask (net_tree_ips n) (σ', ζ')" by auto
qed
lemma transfer_deliver:
assumes "(s, i:deliver(d), s') ∈ trans (pnet np n)"
and "s ∈ reachable (pnet np n) TT"
and "netgmap sr s = netmask (net_tree_ips n) (σ, ζ)"
and "wf_net_tree n"
obtains σ' ζ' where "((σ, ζ), i:deliver(d), (σ', ζ')) ∈ trans (opnet onp n)"
and "∀j. j∉net_ips ζ ⟶ σ' j = σ j"
and "netgmap sr s' = netmask (net_tree_ips n) (σ', ζ')"
proof atomize_elim
from assms(4,2,1) obtain "i∈net_ips s"
and "∀j. j≠i ⟶ netmap s' j = netmap s j"
and "net_ip_action np (i:deliver(d)) i n s s'"
by (metis delivered_to_net_ips pnet_deliver_single_node)
from this(2) have "∀j. j≠i ⟶ fst (netgmap sr s') j = fst (netgmap sr s) j"
by (clarsimp intro!: netmap_is_fst_netgmap')
from ‹(s, i:deliver(d), s') ∈ trans (pnet np n)› have "net_ips s' = net_ips s"
by (rule pnet_maintains_dom [THEN sym])
define σ' where "σ' j = (if j = i then the (fst (netgmap sr s') i) else σ j)" for j
from ‹∀j. j≠i ⟶ fst (netgmap sr s') j = fst (netgmap sr s) j›
and ‹netgmap sr s = netmask (net_tree_ips n) (σ, ζ)›
have "∀j. j≠i ⟶ σ' j = σ j"
unfolding σ'_def by clarsimp
from assms(2) have "net_ips s = net_tree_ips n"
by (rule pnet_net_ips_net_tree_ips)
from ‹netgmap sr s = netmask (net_tree_ips n) (σ, ζ)›
have "ζ = snd (netgmap sr s)" by simp
from ‹∀j. j≠i ⟶ fst (netgmap sr s') j = fst (netgmap sr s) j› ‹i ∈ net_ips s›
‹net_ips s = net_tree_ips n› ‹net_ips s' = net_ips s›
‹netgmap sr s = netmask (net_tree_ips n) (σ, ζ)›
have "fst (netgmap sr s') = fst (netmask (net_tree_ips n) (σ', snd (netgmap sr s')))"
unfolding σ'_def [abs_def] by - (rule ext, clarsimp)
hence "netgmap sr s' = netmask (net_tree_ips n) (σ', snd (netgmap sr s'))"
by (rule prod_eqI, simp)
with assms(1, 3)
have "((σ, snd (netgmap sr s)), i:deliver(d), (σ', snd (netgmap sr s'))) ∈ trans (opnet onp n)"
using assms(2,4) ‹i∈net_ips s› and ‹net_ip_action np (i:deliver(d)) i n s s'›
proof (induction n arbitrary: s s' ζ)
fix ii R⇩i ns ns' ζ
assume "(ns, i:deliver(d), ns') ∈ trans (pnet np ⟨ii; R⇩i⟩)"
and nsr: "ns ∈ reachable (pnet np ⟨ii; R⇩i⟩) TT"
and "netgmap sr ns = netmask (net_tree_ips ⟨ii; R⇩i⟩) (σ, ζ)"
and "netgmap sr ns' = netmask (net_tree_ips ⟨ii; R⇩i⟩) (σ', snd (netgmap sr ns'))"
and "i∈net_ips ns"
from this(1) have "(ns, i:deliver(d), ns') ∈ node_sos (trans (np ii))"
by (simp add: node_comps)
moreover with nsr obtain s s' R R' where "ns = NodeS ii s R"
and "ns' = NodeS ii s' R'"
by (metis net_node_reachable_is_node node_sos_dest)
moreover from ‹i ∈ net_ips ns› and ‹ns = NodeS ii s R› have "ii = i" by simp
ultimately have ntr: "(NodeS i s R, i:deliver(d), NodeS i s' R') ∈ node_sos (trans (np i))"
by simp
hence "R' = R" by (metis net_state.inject(1) node_deliverTE')
from ntr have "(s, deliver d, s') ∈ trans (np i)"
by (rule node_deliverTE') simp
from ‹netgmap sr ns = netmask (net_tree_ips ⟨ii; R⇩i⟩) (σ, ζ)› ‹ns = NodeS ii s R› and ‹ii = i›
have "σ i = fst (sr s)" by simp (metis map_upd_Some_unfold)
moreover from ‹netgmap sr ns' = netmask (net_tree_ips ⟨ii; R⇩i⟩) (σ', snd (netgmap sr ns'))›
‹ns' = NodeS ii s' R'› and ‹ii = i›
have "σ' i = fst (sr s')"
unfolding σ'_def [abs_def] by clarsimp (hypsubst_thin,
metis (lifting, full_types) fun_upd_same option.sel)
ultimately have "((σ, snd (sr s)), deliver d, (σ', snd (sr s'))) ∈ trans (onp i)"
using ‹(s, deliver d, s') ∈ trans (np i)› by (rule trans)
with ‹∀j. j≠i ⟶ σ' j = σ j› ‹R'=R›
have "((σ, NodeS i (snd (sr s)) R), i:deliver(d), (σ', NodeS i (snd (sr s')) R'))
∈ onode_sos (trans (onp i))"
by (metis onode_sos.onode_deliver)
with ‹ns = NodeS ii s R› ‹ns' = NodeS ii s' R'› ‹ii = i›
show "((σ, snd (netgmap sr ns)), i:deliver(d), (σ', snd (netgmap sr ns'))) ∈ trans (opnet onp ⟨ii; R⇩i⟩)"
by (simp add: onode_comps)
next
fix n1 n2 s s' ζ
assume IH1: "⋀s s' ζ. (s, i:deliver(d), s') ∈ trans (pnet np n1)
⟹ netgmap sr s = netmask (net_tree_ips n1) (σ, ζ)
⟹ netgmap sr s' = netmask (net_tree_ips n1) (σ', snd (netgmap sr s'))
⟹ s ∈ reachable (pnet np n1) TT
⟹ wf_net_tree n1
⟹ i∈net_ips s
⟹ net_ip_action np (i:deliver(d)) i n1 s s'
⟹ ((σ, snd (netgmap sr s)), i:deliver(d), (σ', snd (netgmap sr s'))) ∈ trans (opnet onp n1)"
and IH2: "⋀s s' ζ. (s, i:deliver(d), s') ∈ trans (pnet np n2)
⟹ netgmap sr s = netmask (net_tree_ips n2) (σ, ζ)
⟹ netgmap sr s' = netmask (net_tree_ips n2) (σ', snd (netgmap sr s'))
⟹ s ∈ reachable (pnet np n2) TT
⟹ wf_net_tree n2
⟹ i∈net_ips s
⟹ net_ip_action np (i:deliver(d)) i n2 s s'
⟹ ((σ, snd (netgmap sr s)), i:deliver(d), (σ', snd (netgmap sr s'))) ∈ trans (opnet onp n2)"
and tr: "(s, i:deliver(d), s') ∈ trans (pnet np (n1 ∥ n2))"
and sr: "s ∈ reachable (pnet np (n1 ∥ n2)) TT"
and nm: "netgmap sr s = netmask (net_tree_ips (n1 ∥ n2)) (σ, ζ)"
and nm': "netgmap sr s' = netmask (net_tree_ips (n1 ∥ n2)) (σ', snd (netgmap sr s'))"
and "wf_net_tree (n1 ∥ n2)"
and "i∈net_ips s"
and "net_ip_action np (i:deliver(d)) i (n1 ∥ n2) s s'"
from tr have "(s, i:deliver(d), s') ∈ pnet_sos (trans (pnet np n1)) (trans (pnet np n2))" by simp
then obtain s1 s1' s2 s2' where "s = SubnetS s1 s2"
and "s' = SubnetS s1' s2'"
by (rule partial_deliverTE) auto
from this(1) and nm have "netgmap sr (SubnetS s1 s2) = netmask (net_tree_ips (n1 ∥ n2)) (σ, ζ)"
by simp
from ‹s' = SubnetS s1' s2'› and nm'
have "netgmap sr (SubnetS s1' s2') = netmask (net_tree_ips (n1 ∥ n2)) (σ', snd (netgmap sr s'))"
by simp
from ‹wf_net_tree (n1 ∥ n2)› have "wf_net_tree n1"
and "wf_net_tree n2"
and "net_tree_ips n1 ∩ net_tree_ips n2 = {}" by auto
from sr [simplified ‹s = SubnetS s1 s2›] have "s1 ∈ reachable (pnet np n1) TT"
by (rule subnet_reachable(1))
hence "net_ips s1 = net_tree_ips n1" by (rule pnet_net_ips_net_tree_ips)
from sr [simplified ‹s = SubnetS s1 s2›] have "s2 ∈ reachable (pnet np n2) TT"
by (rule subnet_reachable(2))
hence "net_ips s2 = net_tree_ips n2" by (rule pnet_net_ips_net_tree_ips)
from nm [simplified ‹s = SubnetS s1 s2›]
‹net_tree_ips n1 ∩ net_tree_ips n2 = {}›
‹net_ips s1 = net_tree_ips n1›
‹net_ips s2 = net_tree_ips n2›
have "netgmap sr s1 = netmask (net_tree_ips n1) (σ, snd (netgmap sr s1))"
by (rule netgmap_subnet_split1)
from nm [simplified ‹s = SubnetS s1 s2›]
‹net_ips s1 = net_tree_ips n1›
‹net_ips s2 = net_tree_ips n2›
have "netgmap sr s2 = netmask (net_tree_ips n2) (σ, snd (netgmap sr s2))"
by (rule netgmap_subnet_split2)
from ‹i∈net_ips s› and ‹s = SubnetS s1 s2› have "i∈net_ips s1 ∨ i∈net_ips s2" by auto
thus "((σ, snd (netgmap sr s)), i:deliver(d), (σ', snd (netgmap sr s'))) ∈ trans (opnet onp (n1 ∥ n2))"
proof
assume "i∈net_ips s1"
with ‹s = SubnetS s1 s2› ‹s' = SubnetS s1' s2'› ‹net_ip_action np (i:deliver(d)) i (n1 ∥ n2) s s'›
have "(s1, i:deliver(d), s1') ∈ trans (pnet np n1)"
and "net_ip_action np (i:deliver(d)) i n1 s1 s1'"
and "s2' = s2" by simp_all
from ‹net_ips s1 = net_tree_ips n1› and ‹(s1, i:deliver(d), s1') ∈ trans (pnet np n1)›
have "net_ips s1' = net_tree_ips n1" by (metis pnet_maintains_dom)
from nm' [simplified ‹s' = SubnetS s1' s2'› ‹s2' = s2›]
‹net_tree_ips n1 ∩ net_tree_ips n2 = {}›
‹net_ips s1' = net_tree_ips n1›
‹net_ips s2 = net_tree_ips n2›
have "netgmap sr s1' = netmask (net_tree_ips n1) (σ', snd (netgmap sr s1'))"
by (rule netgmap_subnet_split1)
from ‹(s1, i:deliver(d), s1') ∈ trans (pnet np n1)›
‹netgmap sr s1 = netmask (net_tree_ips n1) (σ, snd (netgmap sr s1))›
‹netgmap sr s1' = netmask (net_tree_ips n1) (σ', snd (netgmap sr s1'))›
‹s1 ∈ reachable (pnet np n1) TT›
‹wf_net_tree n1›
‹i∈net_ips s1›
‹net_ip_action np (i:deliver(d)) i n1 s1 s1'›
have "((σ, snd (netgmap sr s1)), i:deliver(d), (σ', snd (netgmap sr s1'))) ∈ trans (opnet onp n1)"
by (rule IH1)
with ‹s = SubnetS s1 s2› ‹s' = SubnetS s1' s2'› ‹s2' = s2› show ?thesis
by simp (erule opnet_deliver1)
next
assume "i∈net_ips s2"
with ‹s = SubnetS s1 s2› ‹s' = SubnetS s1' s2'› ‹net_ip_action np (i:deliver(d)) i (n1 ∥ n2) s s'›
have "(s2, i:deliver(d), s2') ∈ trans (pnet np n2)"
and "net_ip_action np (i:deliver(d)) i n2 s2 s2'"
and "s1' = s1" by simp_all
from ‹net_ips s2 = net_tree_ips n2› and ‹(s2, i:deliver(d), s2') ∈ trans (pnet np n2)›
have "net_ips s2' = net_tree_ips n2" by (metis pnet_maintains_dom)
from nm' [simplified ‹s' = SubnetS s1' s2'› ‹s1' = s1›]
‹net_ips s1 = net_tree_ips n1›
‹net_ips s2' = net_tree_ips n2›
have "netgmap sr s2' = netmask (net_tree_ips n2) (σ', snd (netgmap sr s2'))"
by (rule netgmap_subnet_split2)
from ‹(s2, i:deliver(d), s2') ∈ trans (pnet np n2)›
‹netgmap sr s2 = netmask (net_tree_ips n2) (σ, snd (netgmap sr s2))›
‹netgmap sr s2' = netmask (net_tree_ips n2) (σ', snd (netgmap sr s2'))›
‹s2 ∈ reachable (pnet np n2) TT›
‹wf_net_tree n2›
‹i∈net_ips s2›
‹net_ip_action np (i:deliver(d)) i n2 s2 s2'›
have "((σ, snd (netgmap sr s2)), i:deliver(d), (σ', snd (netgmap sr s2'))) ∈ trans (opnet onp n2)"
by (rule IH2)
with ‹s = SubnetS s1 s2› ‹s' = SubnetS s1' s2'› ‹s1' = s1› show ?thesis
by simp (erule opnet_deliver2)
qed
qed
with ‹ζ = snd (netgmap sr s)› have "((σ, ζ), i:deliver(d), (σ', snd (netgmap sr s'))) ∈ trans (opnet onp n)"
by simp
moreover from ‹∀j. j≠i ⟶ σ' j = σ j› ‹i ∈ net_ips s› ‹ζ = snd (netgmap sr s)›
have "∀j. j∉net_ips ζ ⟶ σ' j = σ j" by (metis net_ips_netgmap)
ultimately have "((σ, ζ), i:deliver(d), (σ', snd (netgmap sr s'))) ∈ trans (opnet onp n)
∧ (∀j. j∉net_ips ζ ⟶ σ' j = σ j)
∧ netgmap sr s' = netmask (net_tree_ips n) (σ', snd (netgmap sr s'))"
using ‹netgmap sr s' = netmask (net_tree_ips n) (σ', snd (netgmap sr s'))› by simp
thus "∃σ' ζ'. ((σ, ζ), i:deliver(d), (σ', ζ')) ∈ trans (opnet onp n)
∧ (∀j. j∉net_ips ζ ⟶ σ' j = σ j)
∧ netgmap sr s' = netmask (net_tree_ips n) (σ', ζ')" by auto
qed
lemma transfer_arrive':
assumes "(s, H¬K:arrive(m), s') ∈ trans (pnet np n)"
and "s ∈ reachable (pnet np n) TT"
and "netgmap sr s = netmask (net_tree_ips n) (σ, ζ)"
and "netgmap sr s' = netmask (net_tree_ips n) (σ', ζ')"
and "wf_net_tree n"
shows "((σ, ζ), H¬K:arrive(m), (σ', ζ')) ∈ trans (opnet onp n)"
proof -
from assms(2) have "net_ips s = net_tree_ips n" ..
with assms(1) have "net_ips s' = net_tree_ips n"
by (metis pnet_maintains_dom)
from ‹netgmap sr s = netmask (net_tree_ips n) (σ, ζ)›
have "ζ = snd (netgmap sr s)" by simp
from ‹netgmap sr s' = netmask (net_tree_ips n) (σ', ζ')›
have "ζ' = snd (netgmap sr s')"
and "netgmap sr s' = netmask (net_tree_ips n) (σ', snd (netgmap sr s'))"
by simp_all
from assms(1-3) ‹netgmap sr s' = netmask (net_tree_ips n) (σ', snd (netgmap sr s'))› assms(5)
have "((σ, snd (netgmap sr s)), H¬K:arrive(m), (σ', snd (netgmap sr s'))) ∈ trans (opnet onp n)"
proof (induction n arbitrary: s s' ζ H K)
fix ii R⇩i ns ns' ζ H K
assume "(ns, H¬K:arrive(m), ns') ∈ trans (pnet np ⟨ii; R⇩i⟩)"
and nsr: "ns ∈ reachable (pnet np ⟨ii; R⇩i⟩) TT"
and "netgmap sr ns = netmask (net_tree_ips ⟨ii; R⇩i⟩) (σ, ζ)"
and "netgmap sr ns' = netmask (net_tree_ips ⟨ii; R⇩i⟩) (σ', snd (netgmap sr ns'))"
from this(1) have "(ns, H¬K:arrive(m), ns') ∈ node_sos (trans (np ii))"
by (simp add: node_comps)
moreover with nsr obtain s s' R where "ns = NodeS ii s R"
and "ns' = NodeS ii s' R"
by (metis net_node_reachable_is_node node_arriveTE')
ultimately have "(NodeS ii s R, H¬K:arrive(m), NodeS ii s' R) ∈ node_sos (trans (np ii))"
by simp
from this(1) have "((σ, NodeS ii (snd (sr s)) R), H¬K:arrive(m), (σ', NodeS ii (snd (sr s')) R))
∈ onode_sos (trans (onp ii))"
proof (rule node_arriveTE)
assume "(s, receive m, s') ∈ trans (np ii)"
and "H = {ii}"
and "K = {}"
from ‹netgmap sr ns = netmask (net_tree_ips ⟨ii; R⇩i⟩) (σ, ζ)› and ‹ns = NodeS ii s R›
have "σ ii = fst (sr s)"
by simp (metis map_upd_Some_unfold)
moreover from ‹netgmap sr ns' = netmask (net_tree_ips ⟨ii; R⇩i⟩) (σ', snd (netgmap sr ns'))›
and ‹ns' = NodeS ii s' R›
have "σ' ii = fst (sr s')" by simp (metis map_upd_Some_unfold)
ultimately have "((σ, snd (sr s)), receive m, (σ', snd (sr s'))) ∈ trans (onp ii)"
using ‹(s, receive m, s') ∈ trans (np ii)› by (rule trans)
hence "((σ, NodeS ii (snd (sr s)) R), {ii}¬{}:arrive(m), (σ', NodeS ii (snd (sr s')) R))
∈ onode_sos (trans (onp ii))"
by (rule onode_receive)
with ‹H={ii}› and ‹K={}›
show "((σ, NodeS ii (snd (sr s)) R), H¬K:arrive(m), (σ', NodeS ii (snd (sr s')) R))
∈ onode_sos (trans (onp ii))"
by simp
next
assume "H = {}"
and "s' = s"
and "K = {ii}"
from ‹s' = s› ‹netgmap sr ns' = netmask (net_tree_ips ⟨ii; R⇩i⟩) (σ', snd (netgmap sr ns'))›
‹netgmap sr ns = netmask (net_tree_ips ⟨ii; R⇩i⟩) (σ, ζ)›
‹ns = NodeS ii s R› and ‹ns' = NodeS ii s' R›
have "σ' ii = σ ii" by simp (metis option.sel)
hence "((σ, NodeS ii (snd (sr s)) R), {}¬{ii}:arrive(m), (σ', NodeS ii (snd (sr s)) R))
∈ onode_sos (trans (onp ii))"
by (rule onode_arrive)
with ‹H={}› ‹K={ii}› and ‹s' = s›
show "((σ, NodeS ii (snd (sr s)) R), H¬K:arrive(m), (σ', NodeS ii (snd (sr s')) R))
∈ onode_sos (trans (onp ii))"
by simp
qed
with ‹ns = NodeS ii s R› ‹ns' = NodeS ii s' R›
show "((σ, snd (netgmap sr ns)), H¬K:arrive(m), (σ', snd (netgmap sr ns')))
∈ trans (opnet onp ⟨ii; R⇩i⟩)"
by (simp add: onode_comps)
next
fix n1 n2 s s' ζ H K
assume IH1: "⋀s s' ζ H K. (s, H¬K:arrive(m), s') ∈ trans (pnet np n1)
⟹ s ∈ reachable (pnet np n1) TT
⟹ netgmap sr s = netmask (net_tree_ips n1) (σ, ζ)
⟹ netgmap sr s' = netmask (net_tree_ips n1) (σ', snd (netgmap sr s'))
⟹ wf_net_tree n1
⟹ ((σ, snd (netgmap sr s)), H¬K:arrive(m), σ', snd (netgmap sr s'))
∈ trans (opnet onp n1)"
and IH2: "⋀s s' ζ H K. (s, H¬K:arrive(m), s') ∈ trans (pnet np n2)
⟹ s ∈ reachable (pnet np n2) TT
⟹ netgmap sr s = netmask (net_tree_ips n2) (σ, ζ)
⟹ netgmap sr s' = netmask (net_tree_ips n2) (σ', snd (netgmap sr s'))
⟹ wf_net_tree n2
⟹ ((σ, snd (netgmap sr s)), H¬K:arrive(m), σ', snd (netgmap sr s'))
∈ trans (opnet onp n2)"
and "(s, H¬K:arrive(m), s') ∈ trans (pnet np (n1 ∥ n2))"
and sr: "s ∈ reachable (pnet np (n1 ∥ n2)) TT"
and nm: "netgmap sr s = netmask (net_tree_ips (n1 ∥ n2)) (σ, ζ)"
and nm': "netgmap sr s' = netmask (net_tree_ips (n1 ∥ n2)) (σ', snd (netgmap sr s'))"
and "wf_net_tree (n1 ∥ n2)"
from this(3) have "(s, H¬K:arrive(m), s') ∈ pnet_sos (trans (pnet np n1))
(trans (pnet np n2))"
by simp
thus "((σ, snd (netgmap sr s)), H¬K:arrive(m), (σ', snd (netgmap sr s')))
∈ trans (opnet onp (n1 ∥ n2))"
proof (rule partial_arriveTE)
fix s1 s1' s2 s2' H1 H2 K1 K2
assume "s = SubnetS s1 s2"
and "s' = SubnetS s1' s2'"
and tr1: "(s1, H1¬K1:arrive(m), s1') ∈ trans (pnet np n1)"
and tr2: "(s2, H2¬K2:arrive(m), s2') ∈ trans (pnet np n2)"
and "H = H1 ∪ H2"
and "K = K1 ∪ K2"
from ‹wf_net_tree (n1 ∥ n2)› have "wf_net_tree n1"
and "wf_net_tree n2"
and "net_tree_ips n1 ∩ net_tree_ips n2 = {}" by auto
from sr [simplified ‹s = SubnetS s1 s2›] have "s1 ∈ reachable (pnet np n1) TT"
by (rule subnet_reachable(1))
hence "net_ips s1 = net_tree_ips n1" by (rule pnet_net_ips_net_tree_ips)
with tr1 have "net_ips s1' = net_tree_ips n1" by (metis pnet_maintains_dom)
from sr [simplified ‹s = SubnetS s1 s2›] have "s2 ∈ reachable (pnet np n2) TT"
by (rule subnet_reachable(2))
hence "net_ips s2 = net_tree_ips n2" by (rule pnet_net_ips_net_tree_ips)
with tr2 have "net_ips s2' = net_tree_ips n2" by (metis pnet_maintains_dom)
from ‹(s1, H1¬K1:arrive(m), s1') ∈ trans (pnet np n1)›
‹s1 ∈ reachable (pnet np n1) TT›
have "((σ, snd (netgmap sr s1)), H1¬K1:arrive(m), (σ', snd (netgmap sr s1')))
∈ trans (opnet onp n1)"
proof (rule IH1 [OF _ _ _ _ ‹wf_net_tree n1›])
from nm [simplified ‹s = SubnetS s1 s2›]
‹net_tree_ips n1 ∩ net_tree_ips n2 = {}›
‹net_ips s1 = net_tree_ips n1›
‹net_ips s2 = net_tree_ips n2›
show "netgmap sr s1 = netmask (net_tree_ips n1) (σ, snd (netgmap sr s1))"
by (rule netgmap_subnet_split1)
next
from nm' [simplified ‹s' = SubnetS s1' s2'›]
‹net_tree_ips n1 ∩ net_tree_ips n2 = {}›
‹net_ips s1' = net_tree_ips n1›
‹net_ips s2' = net_tree_ips n2›
show "netgmap sr s1' = netmask (net_tree_ips n1) (σ', snd (netgmap sr s1'))"
by (rule netgmap_subnet_split1)
qed
moreover from ‹(s2, H2¬K2:arrive(m), s2') ∈ trans (pnet np n2)›
‹s2 ∈ reachable (pnet np n2) TT›
have "((σ, snd (netgmap sr s2)), H2¬K2:arrive(m), (σ', snd (netgmap sr s2')))
∈ trans (opnet onp n2)"
proof (rule IH2 [OF _ _ _ _ ‹wf_net_tree n2›])
from nm [simplified ‹s = SubnetS s1 s2›]
‹net_ips s1 = net_tree_ips n1›
‹net_ips