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 s2 = net_tree_ips n2›
show "netgmap sr s2 = netmask (net_tree_ips n2) (σ, snd (netgmap sr s2))"
by (rule netgmap_subnet_split2)
next
from nm' [simplified ‹s' = SubnetS s1' s2'›]
‹net_ips s1' = net_tree_ips n1›
‹net_ips s2' = net_tree_ips n2›
show "netgmap sr s2' = netmask (net_tree_ips n2) (σ', snd (netgmap sr s2'))"
by (rule netgmap_subnet_split2)
qed
ultimately show "((σ, snd (netgmap sr s)), H¬K:arrive(m), (σ', snd (netgmap sr s')))
∈ trans (opnet onp (n1 ∥ n2))"
using ‹s = SubnetS s1 s2› ‹s' = SubnetS s1' s2'› ‹H = H1 ∪ H2› ‹K = K1 ∪ K2›
by simp (rule opnet_sos.opnet_arrive)
qed
qed
with ‹ζ = snd (netgmap sr s)› and ‹ζ' = snd (netgmap sr s')›
show "((σ, ζ), H¬K:arrive(m), (σ', ζ')) ∈ trans (opnet onp n)"
by simp
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 "wf_net_tree n"
obtains σ' ζ' where "((σ, ζ), H¬K:arrive(m), (σ', ζ')) ∈ trans (opnet onp n)"
and "∀j. j∉net_ips ζ ⟶ σ' j = σ j"
and "netgmap sr s' = netmask (net_tree_ips n) (σ', ζ')"
proof atomize_elim
define σ' where "σ' i = (if i∈net_tree_ips n then the (fst (netgmap sr s') i) else σ i)" for i
from assms(2) have "net_ips s = net_tree_ips n"
by (rule pnet_net_ips_net_tree_ips)
with assms(1) have "net_ips s' = net_tree_ips n"
by (metis pnet_maintains_dom)
have "netgmap sr s' = netmask (net_tree_ips n) (σ', snd (netgmap sr s'))"
proof (rule prod_eqI)
from ‹net_ips s' = net_tree_ips n›
show "fst (netgmap sr s') = fst (netmask (net_tree_ips n) (σ', snd (netgmap sr s')))"
unfolding σ'_def [abs_def] by - (rule ext, clarsimp)
qed simp
moreover with assms(1-3)
have "((σ, ζ), H¬K:arrive(m), (σ', snd (netgmap sr s'))) ∈ trans (opnet onp n)"
using ‹wf_net_tree n› by (rule transfer_arrive')
moreover have "∀j. j∉net_ips ζ ⟶ σ' j = σ j"
proof -
have "∀j. j∉net_tree_ips n ⟶ σ' j = σ j" unfolding σ'_def by simp
with assms(3) and ‹net_ips s = net_tree_ips n›
show ?thesis
by clarsimp (metis (mono_tags) net_ips_netgmap snd_conv)
qed
ultimately show "∃σ' ζ'. ((σ, ζ), H¬K:arrive(m), (σ', ζ')) ∈ trans (opnet onp n)
∧ (∀j. j∉net_ips ζ ⟶ σ' j = σ j)
∧ netgmap sr s' = netmask (net_tree_ips n) (σ', ζ')" by auto
qed
lemma transfer_cast:
assumes "(s, mR:*cast(m), 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 "((σ, ζ), mR:*cast(m), (σ', ζ')) ∈ trans (opnet onp n)"
and "∀j. j∉net_ips ζ ⟶ σ' j = σ j"
and "netgmap sr s' = netmask (net_tree_ips n) (σ', ζ')"
proof atomize_elim
define σ' where "σ' i = (if i∈net_tree_ips n then the (fst (netgmap sr s') i) else σ i)" for i
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)
have "netgmap sr s' = netmask (net_tree_ips n) (σ', snd (netgmap sr s'))"
proof (rule prod_eqI)
from ‹net_ips s' = net_tree_ips n›
show "fst (netgmap sr s') = fst (netmask (net_tree_ips n) (σ', snd (netgmap sr s')))"
unfolding σ'_def [abs_def] by - (rule ext, clarsimp simp add: some_the_fst_netgmap)
qed simp
from ‹net_ips s' = net_tree_ips n› and ‹net_ips s = net_tree_ips n›
have "∀j. j∉net_ips (snd (netgmap sr s)) ⟶ σ' j = σ j"
unfolding σ'_def by simp
from ‹netgmap sr s = netmask (net_tree_ips n) (σ, ζ)›
have "ζ = snd (netgmap sr s)" by simp
from assms(1-3) ‹netgmap sr s' = netmask (net_tree_ips n) (σ', snd (netgmap sr s'))› assms(4)
have "((σ, snd (netgmap sr s)), mR:*cast(m), (σ', snd (netgmap sr s'))) ∈ trans (opnet onp n)"
proof (induction n arbitrary: s s' ζ mR)
fix ii R⇩i ns ns' ζ mR
assume "(ns, mR:*cast(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, mR:*cast(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_castTE')
ultimately have "(NodeS ii s R, mR:*cast(m), NodeS ii s' R) ∈ node_sos (trans (np ii))"
by simp
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)
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)
from ‹(NodeS ii s R, mR:*cast(m), NodeS ii s' R) ∈ node_sos (trans (np ii))›
have "((σ, NodeS ii (snd (sr s)) R), mR:*cast(m), (σ', NodeS ii (snd (sr s')) R))
∈ onode_sos (trans (onp ii))"
proof (rule node_castTE)
assume "(s, broadcast m, s') ∈ trans (np ii)"
and "mR = R"
from ‹σ ii = fst (sr s)› ‹σ' ii = fst (sr s')› and this(1)
have "((σ, snd (sr s)), broadcast m, (σ', snd (sr s'))) ∈ trans (onp ii)"
by (rule trans)
hence "((σ, NodeS ii (snd (sr s)) R), R:*cast(m), (σ', NodeS ii (snd (sr s')) R))
∈ onode_sos (trans (onp ii))"
by (rule onode_bcast)
with ‹mR = R› show "((σ, NodeS ii (snd (sr s)) R), mR:*cast(m), (σ', NodeS ii (snd (sr s')) R))
∈ onode_sos (trans (onp ii))"
by simp
next
fix D
assume "(s, groupcast D m, s') ∈ trans (np ii)"
and "mR = R ∩ D"
from ‹σ ii = fst (sr s)› ‹σ' ii = fst (sr s')› and this(1)
have "((σ, snd (sr s)), groupcast D m, (σ', snd (sr s'))) ∈ trans (onp ii)"
by (rule trans)
hence "((σ, NodeS ii (snd (sr s)) R), (R ∩ D):*cast(m), (σ', NodeS ii (snd (sr s')) R))
∈ onode_sos (trans (onp ii))"
by (rule onode_gcast)
with ‹mR = R ∩ D› show "((σ, NodeS ii (snd (sr s)) R), mR:*cast(m), (σ', NodeS ii (snd (sr s')) R))
∈ onode_sos (trans (onp ii))"
by simp
next
fix d
assume "(s, unicast d m, s') ∈ trans (np ii)"
and "d ∈ R"
and "mR = {d}"
from ‹σ ii = fst (sr s)› ‹σ' ii = fst (sr s')› and this(1)
have "((σ, snd (sr s)), unicast d m, (σ', snd (sr s'))) ∈ trans (onp ii)"
by (rule trans)
hence "((σ, NodeS ii (snd (sr s)) R), {d}:*cast(m), (σ', NodeS ii (snd (sr s')) R))
∈ onode_sos (trans (onp ii))"
using ‹d∈R› by (rule onode_ucast)
with ‹mR={d}› show "((σ, NodeS ii (snd (sr s)) R), mR:*cast(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)), mR:*cast(m), (σ', snd (netgmap sr ns')))
∈ trans (opnet onp ⟨ii; R⇩i⟩)"
by (simp add: onode_comps)
next
fix n1 n2 s s' ζ mR
assume IH1: "⋀s s' ζ mR. (s, mR:*cast(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)), mR:*cast(m), σ', snd (netgmap sr s'))
∈ trans (opnet onp n1)"
and IH2: "⋀s s' ζ mR. (s, mR:*cast(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)), mR:*cast(m), σ', snd (netgmap sr s'))
∈ trans (opnet onp n2)"
and "(s, mR:*cast(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, mR:*cast(m), s') ∈ pnet_sos (trans (pnet np n1)) (trans (pnet np n2))"
by simp
then obtain s1 s1' s2 s2' H K
where "s = SubnetS s1 s2"
and "s' = SubnetS s1' s2'"
and "H ⊆ mR"
and "K ∩ mR = {}"
and trtr: "((s1, mR:*cast(m), s1') ∈ trans (pnet np n1)
∧ (s2, H¬K:arrive(m), s2') ∈ trans (pnet np n2))
∨ ((s1, H¬K:arrive(m), s1') ∈ trans (pnet np n1)
∧ (s2, mR:*cast(m), s2') ∈ trans (pnet np n2))"
by (rule partial_castTE) metis+
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 trtr 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 trtr have "net_ips s2' = net_tree_ips n2" by (metis pnet_maintains_dom)
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_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 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 trtr show "((σ, snd (netgmap sr s)), mR:*cast(m), (σ', snd (netgmap sr s')))
∈ trans (opnet onp (n1 ∥ n2))"
proof (elim disjE conjE)
assume "(s1, mR:*cast(m), s1') ∈ trans (pnet np n1)"
and "(s2, H¬K:arrive(m), s2') ∈ trans (pnet np n2)"
from ‹(s1, mR:*cast(m), s1') ∈ trans (pnet np n1)›
‹s1 ∈ reachable (pnet np n1) TT›
‹netgmap sr s1 = netmask (net_tree_ips n1) (σ, snd (netgmap sr s1))›
‹netgmap sr s1' = netmask (net_tree_ips n1) (σ', snd (netgmap sr s1'))›
‹wf_net_tree n1›
have "((σ, snd (netgmap sr s1)), mR:*cast(m), (σ', snd (netgmap sr s1'))) ∈ trans (opnet onp n1)"
by (rule IH1)
moreover from ‹(s2, H¬K:arrive(m), s2') ∈ trans (pnet np n2)›
‹s2 ∈ reachable (pnet np n2) TT›
‹netgmap sr s2 = netmask (net_tree_ips n2) (σ, snd (netgmap sr s2))›
‹netgmap sr s2' = netmask (net_tree_ips n2) (σ', snd (netgmap sr s2'))›
‹wf_net_tree n2›
have "((σ, snd (netgmap sr s2)), H¬K:arrive(m), (σ', snd (netgmap sr s2'))) ∈ trans (opnet onp n2)"
by (rule transfer_arrive')
ultimately have "((σ, SubnetS (snd (netgmap sr s1)) (snd (netgmap sr s2))), mR:*cast(m),
(σ', SubnetS (snd (netgmap sr s1')) (snd (netgmap sr s2'))))
∈ opnet_sos (trans (opnet onp n1)) (trans (opnet onp n2))"
using ‹H ⊆ mR› and ‹K ∩ mR = {}› by (rule opnet_sos.intros(1))
with ‹s = SubnetS s1 s2› ‹s' = SubnetS s1' s2'› show ?thesis by simp
next
assume "(s1, H¬K:arrive(m), s1') ∈ trans (pnet np n1)"
and "(s2, mR:*cast(m), s2') ∈ trans (pnet np n2)"
from ‹(s1, H¬K:arrive(m), s1') ∈ trans (pnet np n1)›
‹s1 ∈ reachable (pnet np n1) TT›
‹netgmap sr s1 = netmask (net_tree_ips n1) (σ, snd (netgmap sr s1))›
‹netgmap sr s1' = netmask (net_tree_ips n1) (σ', snd (netgmap sr s1'))›
‹wf_net_tree n1›
have "((σ, snd (netgmap sr s1)), H¬K:arrive(m), (σ', snd (netgmap sr s1'))) ∈ trans (opnet onp n1)"
by (rule transfer_arrive')
moreover from ‹(s2, mR:*cast(m), s2') ∈ trans (pnet np n2)›
‹s2 ∈ reachable (pnet np n2) TT›
‹netgmap sr s2 = netmask (net_tree_ips n2) (σ, snd (netgmap sr s2))›
‹netgmap sr s2' = netmask (net_tree_ips n2) (σ', snd (netgmap sr s2'))›
‹wf_net_tree n2›
have "((σ, snd (netgmap sr s2)), mR:*cast(m), (σ', snd (netgmap sr s2'))) ∈ trans (opnet onp n2)"
by (rule IH2)
ultimately have "((σ, SubnetS (snd (netgmap sr s1)) (snd (netgmap sr s2))), mR:*cast(m),
(σ', SubnetS (snd (netgmap sr s1')) (snd (netgmap sr s2'))))
∈ opnet_sos (trans (opnet onp n1)) (trans (opnet onp n2))"
using ‹H ⊆ mR› and ‹K ∩ mR = {}› by (rule opnet_sos.intros(2))
with ‹s = SubnetS s1 s2› ‹s' = SubnetS s1' s2'› show ?thesis by simp
qed
qed
with ‹ζ = snd (netgmap sr s)› have "((σ, ζ), mR:*cast(m), (σ', snd (netgmap sr s'))) ∈ trans (opnet onp n)"
by simp
moreover from ‹∀j. j∉net_ips (snd (netgmap sr s)) ⟶ σ' j = σ j› ‹ζ = snd (netgmap sr s)›
have "∀j. j∉net_ips ζ ⟶ σ' j = σ j" by simp
moreover note ‹netgmap sr s' = netmask (net_tree_ips n) (σ', snd (netgmap sr s'))›
ultimately show "∃σ' ζ'. ((σ, ζ), mR:*cast(m), (σ', ζ')) ∈ trans (opnet onp n)
∧ (∀j. j∉net_ips ζ ⟶ σ' j = σ j)
∧ netgmap sr s' = netmask (net_tree_ips n) (σ', ζ')"
by auto
qed
lemma transfer_pnet_action:
assumes "s ∈ reachable (pnet np n) TT"
and "netgmap sr s = netmask (net_tree_ips n) (σ, ζ)"
and "wf_net_tree n"
and "(s, a, s') ∈ trans (pnet np n)"
obtains σ' ζ' where "((σ, ζ), a, (σ', ζ')) ∈ trans (opnet onp n)"
and "∀j. j∉net_ips ζ ⟶ σ' j = σ j"
and "netgmap sr s' = netmask (net_tree_ips n) (σ', ζ')"
proof atomize_elim
show "∃σ' ζ'. ((σ, ζ), a, (σ', ζ')) ∈ trans (opnet onp n)
∧ (∀j. j∉net_ips ζ ⟶ σ' j = σ j)
∧ netgmap sr s' = netmask (net_tree_ips n) (σ', ζ')"
proof (cases a)
case node_cast
with assms(4) show ?thesis
by (auto elim!: transfer_cast [OF _ assms(1-3)])
next
case node_deliver
with assms(4) show ?thesis
by (auto elim!: transfer_deliver [OF _ assms(1-3)])
next
case node_arrive
with assms(4) show ?thesis
by (auto elim!: transfer_arrive [OF _ assms(1-3)])
next
case node_connect
with assms(4) show ?thesis
by (auto elim!: transfer_connect [OF _ assms(1-3)])
next
case node_disconnect
with assms(4) show ?thesis
by (auto elim!: transfer_disconnect [OF _ assms(1-3)])
next
case node_newpkt
with assms(4) have False by (metis pnet_never_newpkt)
thus ?thesis ..
next
case node_tau
with assms(4) show ?thesis
by (auto elim!: transfer_tau [OF _ assms(1-3), simplified])
qed
qed
lemma transfer_action_pnet_closed:
assumes "(s, a, s') ∈ trans (closed (pnet np n))"
obtains a' where "(s, a', s') ∈ trans (pnet np n)"
and "⋀σ ζ σ' ζ'. ⟦ ((σ, ζ), a', (σ', ζ')) ∈ trans (opnet onp n);
(∀j. j∉net_ips ζ ⟶ σ' j = σ j) ⟧
⟹ ((σ, ζ), a, (σ', ζ')) ∈ trans (oclosed (opnet onp n))"
proof (atomize_elim)
from assms have "(s, a, s') ∈ cnet_sos (trans (pnet np n))" by simp
thus "∃a'. (s, a', s') ∈ trans (pnet np n)
∧ (∀σ ζ σ' ζ'. ((σ, ζ), a', (σ', ζ')) ∈ trans (opnet onp n)
⟶ (∀j. j ∉ net_ips ζ ⟶ σ' j = σ j)
⟶ ((σ, ζ), a, (σ', ζ')) ∈ trans (oclosed (opnet onp n)))"
proof cases
case (cnet_cast R m) thus ?thesis
by (auto intro!: exI [where x="R:*cast(m)"] dest!: ocnet_cast)
qed (auto intro!: ocnet_sos.intros [simplified])
qed
lemma transfer_action:
assumes "s ∈ reachable (closed (pnet np n)) TT"
and "netgmap sr s = netmask (net_tree_ips n) (σ, ζ)"
and "wf_net_tree n"
and "(s, a, s') ∈ trans (closed (pnet np n))"
obtains σ' ζ' where "((σ, ζ), a, (σ', ζ')) ∈ trans (oclosed (opnet onp n))"
and "netgmap sr s' = netmask (net_tree_ips n) (σ', ζ')"
proof atomize_elim
from assms(1) have "s ∈ reachable (pnet np n) TT" ..
from assms(4)
show "∃σ' ζ'. ((σ, ζ), a, (σ', ζ')) ∈ trans (oclosed (opnet onp n))
∧ netgmap sr s' = netmask (net_tree_ips n) (σ', ζ')"
by (cases a)
((elim transfer_action_pnet_closed
transfer_pnet_action [OF ‹s ∈ reachable (pnet np n) TT› assms(2-3)])?,
(auto intro!: exI)[1])+
qed
lemma pnet_reachable_transfer':
assumes "wf_net_tree n"
and "s ∈ reachable (closed (pnet np n)) TT"
shows "netgmap sr s ∈ netmask (net_tree_ips n) ` oreachable (oclosed (opnet onp n)) (λ_ _ _. True) U"
(is " _ ∈ ?f ` ?oreachable n")
using assms(2) proof induction
fix s
assume "s ∈ init (closed (pnet np n))"
hence "s ∈ init (pnet np n)" by simp
with ‹wf_net_tree n› have "netgmap sr s ∈ netmask (net_tree_ips n) ` init (opnet onp n)"
by (rule init_pnet_opnet)
hence "netgmap sr s ∈ netmask (net_tree_ips n) ` init (oclosed (opnet onp n))"
by simp
moreover have "netmask (net_tree_ips n) ` init (oclosed (opnet onp n))
⊆ netmask (net_tree_ips n) ` ?oreachable n"
by (intro image_mono subsetI) (rule oreachable_init)
ultimately show "netgmap sr s ∈ netmask (net_tree_ips n) ` ?oreachable n"
by (rule rev_subsetD)
next
fix s a s'
assume "s ∈ reachable (closed (pnet np n)) TT"
and "netgmap sr s ∈ netmask (net_tree_ips n) ` ?oreachable n"
and "(s, a, s') ∈ trans (closed (pnet np n))"
from this(2) obtain σ ζ where "netgmap sr s = netmask (net_tree_ips n) (σ, ζ)"
and "(σ, ζ) ∈ ?oreachable n"
by clarsimp
from ‹s ∈ reachable (closed (pnet np n)) TT› this(1) ‹wf_net_tree n›
and ‹(s, a, s') ∈ trans (closed (pnet np n))›
obtain σ' ζ' where "((σ, ζ), a, (σ', ζ')) ∈ trans (oclosed (opnet onp n))"
and "netgmap sr s' = netmask (net_tree_ips n) (σ', ζ')"
by (rule transfer_action)
from ‹(σ, ζ) ∈ ?oreachable n› and this(1) have "(σ', ζ') ∈ ?oreachable n"
by (rule oreachable_local) simp
with ‹netgmap sr s' = netmask (net_tree_ips n) (σ', ζ')›
show "netgmap sr s' ∈ netmask (net_tree_ips n) ` ?oreachable n" by (rule image_eqI)
qed
definition
someinit :: "nat ⇒ 'g"
where
"someinit i ≡ SOME x. x ∈ (fst o sr) ` init (np i)"
definition
initmissing :: "((nat ⇒ 'g option) × 'a) ⇒ (nat ⇒ 'g) × 'a"
where
"initmissing σ = (λi. case (fst σ) i of None ⇒ someinit i | Some s ⇒ s, snd σ)"
lemma initmissing_def':
"initmissing = apfst (default someinit)"
by (auto simp add: initmissing_def default_def)
lemma netmask_initmissing_netgmap:
"netmask (net_ips s) (initmissing (netgmap sr s)) = netgmap sr s"
proof (intro prod_eqI ext)
fix i
show "fst (netmask (net_ips s) (initmissing (netgmap sr s))) i = fst (netgmap sr s) i"
unfolding initmissing_def by (clarsimp split: option.split)
qed (simp add: initmissing_def)
lemma snd_initmissing [simp]:
"snd (initmissing x)= snd x"
unfolding initmissing_def by simp
lemma initmnissing_snd_netgmap [simp]:
assumes "initmissing (netgmap sr s) = (σ, ζ)"
shows "snd (netgmap sr s) = ζ"
using assms unfolding initmissing_def by simp
lemma in_net_ips_fst_init_missing [simp]:
assumes "i ∈ net_ips s"
shows "fst (initmissing (netgmap sr s)) i = the (fst (netgmap sr s) i)"
using assms unfolding initmissing_def by (clarsimp split: option.split)
lemma not_in_net_ips_fst_init_missing [simp]:
assumes "i ∉ net_ips s"
shows "fst (initmissing (netgmap sr s)) i = someinit i"
using assms unfolding initmissing_def by (clarsimp split: option.split)
lemma initmissing_oreachable_netmask [elim]:
assumes "initmissing (netgmap sr s) ∈ oreachable (oclosed (opnet onp n)) (λ_ _ _. True) U"
(is "_ ∈ ?oreachable n")
and "net_ips s = net_tree_ips n"
shows "netgmap sr s ∈ netmask (net_tree_ips n) ` ?oreachable n"
proof -
obtain σ ζ where "initmissing (netgmap sr s) = (σ, ζ)" by (metis surj_pair)
with assms(1) have "(σ, ζ) ∈ ?oreachable n" by simp
have "netgmap sr s = netmask (net_ips s) (σ, ζ)"
proof (intro prod_eqI ext)
fix i
show "fst (netgmap sr s) i = fst (netmask (net_ips s) (σ, ζ)) i"
proof (cases "i∈net_ips s")
assume "i∈net_ips s"
hence "fst (initmissing (netgmap sr s)) i = the (fst (netgmap sr s) i)"
by (rule in_net_ips_fst_init_missing)
moreover from ‹i∈net_ips s› have "Some (the (fst (netgmap sr s) i)) = fst (netgmap sr s) i"
by (rule some_the_fst_netgmap)
ultimately show ?thesis
using ‹initmissing (netgmap sr s) = (σ, ζ)› by simp
qed simp
next
from ‹initmissing (netgmap sr s) = (σ, ζ)›
show "snd (netgmap sr s) = snd (netmask (net_ips s) (σ, ζ))"
by simp
qed
with assms(2) have "netgmap sr s = netmask (net_tree_ips n) (σ, ζ)" by simp
moreover from ‹(σ, ζ) ∈ ?oreachable n›
have "netmask (net_ips s) (σ, ζ) ∈ netmask (net_ips s) ` ?oreachable n"
by (rule imageI)
ultimately show ?thesis
by (simp only: assms(2))
qed
lemma pnet_reachable_transfer:
assumes "wf_net_tree n"
and "s ∈ reachable (closed (pnet np n)) TT"
shows "initmissing (netgmap sr s) ∈ oreachable (oclosed (opnet onp n)) (λ_ _ _. True) U"
(is " _ ∈ ?oreachable n")
using assms(2) proof induction
fix s
assume "s ∈ init (closed (pnet np n))"
hence "s ∈ init (pnet np n)" by simp
from ‹wf_net_tree n› have "initmissing (netgmap sr s) ∈ init (opnet onp n)"
proof (rule init_lifted [THEN subsetD], intro CollectI exI conjI allI)
show "initmissing (netgmap sr s) = (fst (initmissing (netgmap sr s)), snd (netgmap sr s))"
by (metis snd_initmissing surjective_pairing)
next
from ‹s ∈ init (pnet np n)› show "s ∈ init (pnet np n)" ..
next
fix i
show "if i ∈ net_tree_ips n
then (fst (initmissing (netgmap sr s))) i = the (fst (netgmap sr s) i)
else (fst (initmissing (netgmap sr s))) i ∈ (fst ∘ sr) ` init (np i)"
proof (cases "i ∈ net_tree_ips n", simp_all only: if_True if_False)
assume "i ∈ net_tree_ips n"
with ‹s ∈ init (pnet np n)› have "i ∈ net_ips s" ..
thus "fst (initmissing (netgmap sr s)) i = the (fst (netgmap sr s) i)" by simp
next
assume "i ∉ net_tree_ips n"
with ‹s ∈ init (pnet np n)› have "i ∉ net_ips s" ..
hence "fst (initmissing (netgmap sr s)) i = someinit i" by simp
moreover have "someinit i ∈ (fst ∘ sr) ` init (np i)"
unfolding someinit_def proof (rule someI_ex)
from init_notempty show "∃x. x ∈ (fst o sr) ` init (np i)" by auto
qed
ultimately show "fst (initmissing (netgmap sr s)) i ∈ (fst ∘ sr) ` init (np i)"
by simp
qed
qed
hence "initmissing (netgmap sr s) ∈ init (oclosed (opnet onp n))" by simp
thus "initmissing (netgmap sr s) ∈ ?oreachable n" ..
next
fix s a s'
assume "s ∈ reachable (closed (pnet np n)) TT"
and "(s, a, s') ∈ trans (closed (pnet np n))"
and "initmissing (netgmap sr s) ∈ ?oreachable n"
from this(1) have "s ∈ reachable (pnet np n) TT" ..
hence "net_ips s = net_tree_ips n" by (rule pnet_net_ips_net_tree_ips)
with ‹initmissing (netgmap sr s) ∈ ?oreachable n›
have "netgmap sr s ∈ netmask (net_tree_ips n) ` ?oreachable n"
by (rule initmissing_oreachable_netmask)
obtain σ ζ where "(σ, ζ) = initmissing (netgmap sr s)" by (metis surj_pair)
with ‹initmissing (netgmap sr s) ∈ ?oreachable n›
have "(σ, ζ) ∈ ?oreachable n" by simp
from ‹(σ, ζ) = initmissing (netgmap sr s)› and ‹net_ips s = net_tree_ips n› [symmetric]
have "netgmap sr s = netmask (net_tree_ips n) (σ, ζ)"
by (clarsimp simp add: netmask_initmissing_netgmap)
with ‹s ∈ reachable (closed (pnet np n)) TT›
obtain σ' ζ' where "((σ, ζ), a, (σ', ζ')) ∈ trans (oclosed (opnet onp n))"
and "netgmap sr s' = netmask (net_tree_ips n) (σ', ζ')"
using ‹wf_net_tree n› and ‹(s, a, s') ∈ trans (closed (pnet np n))›
by (rule transfer_action)
from ‹(σ, ζ) ∈ ?oreachable n› have "net_ips ζ = net_tree_ips n"
by (rule opnet_net_ips_net_tree_ips [OF oclosed_oreachable_oreachable])
with ‹((σ, ζ), a, (σ', ζ')) ∈ trans (oclosed (opnet onp n))›
have "∀j. j∉net_tree_ips n ⟶ σ' j = σ j"
by (clarsimp elim!: ocomplete_no_change)
have "initmissing (netgmap sr s') = (σ', ζ')"
proof (intro prod_eqI ext)
fix i
from ‹netgmap sr s' = netmask (net_tree_ips n) (σ', ζ')›
‹∀j. j∉net_tree_ips n ⟶ σ' j = σ j›
‹(σ, ζ) = initmissing (netgmap sr s)›
‹net_ips s = net_tree_ips n›
show "fst (initmissing (netgmap sr s')) i = fst (σ', ζ') i"
unfolding initmissing_def by simp
next
from ‹netgmap sr s' = netmask (net_tree_ips n) (σ', ζ')›
show "snd (initmissing (netgmap sr s')) = snd (σ', ζ')" by simp
qed
moreover from ‹(σ, ζ) ∈ ?oreachable n› ‹((σ, ζ), a, (σ', ζ')) ∈ trans (oclosed (opnet onp n))›
have "(σ', ζ') ∈ ?oreachable n"
by (rule oreachable_local) (rule TrueI)
ultimately show "initmissing (netgmap sr s') ∈ ?oreachable n"
by simp
qed
definition
netglobal :: "((nat ⇒ 'g) ⇒ bool) ⇒ 's net_state ⇒ bool"
where
"netglobal P ≡ (λs. P (fst (initmissing (netgmap sr s))))"
lemma netglobalsimp [simp]:
"netglobal P s = P (fst (initmissing (netgmap sr s)))"
unfolding netglobal_def by simp
lemma netglobalE [elim]:
assumes "netglobal P s"
and "⋀σ. ⟦ P σ; fst (initmissing (netgmap sr s)) = σ ⟧ ⟹ Q σ"
shows "netglobal Q s"
using assms by simp
lemma netglobal_weakenE [elim]:
assumes "p ⊫ netglobal P"
and "⋀σ. P σ ⟹ Q σ"
shows "p ⊫ netglobal Q"
using assms(1) proof (rule invariant_weakenE)
fix s
assume "netglobal P s"
thus "netglobal Q s"
by (rule netglobalE) (erule assms(2))
qed
lemma close_opnet:
assumes "wf_net_tree n"
and "oclosed (opnet onp n) ⊨ (λ_ _ _. True, U →) global P"
shows "closed (pnet np n) ⊫ netglobal P"
unfolding invariant_def proof
fix s
assume "s ∈ reachable (closed (pnet np n)) TT"
with assms(1)
have "initmissing (netgmap sr s) ∈ oreachable (oclosed (opnet onp n)) (λ_ _ _. True) U"
by (rule pnet_reachable_transfer)
with assms(2) have "global P (initmissing (netgmap sr s))" ..
thus "netglobal P s" by simp
qed
end
locale openproc_parq =
op?: openproc np onp sr for np :: "ip ⇒ ('s, ('m::msg) seq_action) automaton" and onp sr
+ fixes qp :: "('t, 'm seq_action) automaton"
assumes init_qp_notempty: "init qp ≠ {}"
sublocale openproc_parq ⊆ openproc "λi. np i ⟨⟨ qp"
"λi. onp i ⟨⟨⇘i⇙ qp"
"λ(p, q). (fst (sr p), (snd (sr p), q))"
proof unfold_locales
fix i
show "{ (σ, ζ) |σ ζ s. s ∈ init (np i ⟨⟨ qp)
∧ (σ i, ζ) = ((λ(p, q). (fst (sr p), (snd (sr p), q))) s)
∧ (∀j. j≠i ⟶ σ j ∈ (fst o (λ(p, q). (fst (sr p), (snd (sr p), q))))
` init (np j ⟨⟨ qp)) } ⊆ init (onp i ⟨⟨⇘i⇙ qp)"
(is "?S ⊆ _")
proof
fix s
assume "s ∈ ?S"
then obtain σ p lq
where "s = (σ, (snd (sr p), lq))"
and "lq ∈ init qp"
and "p ∈ init (np i)"
and "σ i = fst (sr p)"
and "∀j. j ≠ i ⟶ σ j ∈ (fst ∘ (λ(p, q). (fst (sr p), snd (sr p), q)))
` (init (np j) × init qp)"
by auto
from this(5) have "∀j. j ≠ i ⟶ σ j ∈ (fst ∘ sr) ` init (np j)"
by auto
with ‹p ∈ init (np i)› and ‹σ i = fst (sr p)› have "(σ, snd (sr p)) ∈ init (onp i)"
by - (rule init [THEN subsetD], auto)
with ‹lq∈ init qp› have "((σ, snd (sr p)), lq) ∈ init (onp i) × init qp"
by simp
hence "(σ, (snd (sr p), lq)) ∈ extg ` (init (onp i) × init qp)"
by (rule rev_image_eqI) simp
with ‹s = (σ, (snd (sr p), lq))› show "s ∈ init (onp i ⟨⟨⇘i⇙ qp)"
by simp
qed
next
fix i s a s' σ σ'
assume "σ i = fst ((λ(p, q). (fst (sr p), (snd (sr p), q))) s)"
and "σ' i = fst ((λ(p, q). (fst (sr p), (snd (sr p), q))) s')"
and "(s, a, s') ∈ trans (np i ⟨⟨ qp)"
then obtain p q p' q' where "s = (p, q)"
and "s' = (p', q')"
and "σ i = fst (sr p)"
and "σ' i = fst (sr p')"
by (clarsimp split: prod.split_asm)
from this(1-2) and ‹(s, a, s') ∈ trans (np i ⟨⟨ qp)›
have "((p, q), a, (p', q')) ∈ parp_sos (trans (np i)) (trans qp)" by simp
hence "((σ, (snd (sr p), q)), a, (σ', (snd (sr p'), q'))) ∈ trans (onp i ⟨⟨⇘i⇙ qp)"
proof cases
assume "q' = q"
and "(p, a, p') ∈ trans (np i)"
and "⋀m. a ≠ receive m"
from ‹σ i = fst (sr p)› and ‹σ' i = fst (sr p')› this(2)
have "((σ, snd (sr p)), a, (σ', snd (sr p'))) ∈ trans (onp i)" by (rule trans)
with ‹q' = q› and ‹⋀m. a ≠ receive m›
show "((σ, snd (sr p), q), a, (σ', (snd (sr p'), q'))) ∈ trans (onp i ⟨⟨⇘i⇙ qp)"
by (auto elim!: oparleft)
next
assume "p' = p"
and "(q, a, q') ∈ trans qp"
and "⋀m. a ≠ send m"
with ‹σ i = fst (sr p)› and ‹σ' i = fst (sr p')›
show "((σ, snd (sr p), q), a, (σ', (snd (sr p'), q'))) ∈ trans (onp i ⟨⟨⇘i⇙ qp)"
by (auto elim!: oparright)
next
fix m
assume "a = τ"
and "(p, receive m, p') ∈ trans (np i)"
and "(q, send m, q') ∈ trans qp"
from ‹σ i = fst (sr p)› and ‹σ' i = fst (sr p')› this(2)
have "((σ, snd (sr p)), receive m, (σ', snd (sr p'))) ∈ trans (onp i)"
by (rule trans)
with ‹(q, send m, q') ∈ trans qp› and ‹a = τ›
show "((σ, snd (sr p), q), a, (σ', (snd (sr p'), q'))) ∈ trans (onp i ⟨⟨⇘i⇙ qp)"
by (simp del: step_seq_tau) (rule oparboth)
qed
with ‹s = (p, q)› ‹s' = (p', q')›
show "((σ, snd ((λ(p, q). (fst (sr p), (snd (sr p), q))) s)), a,
(σ', snd ((λ(p, q). (fst (sr p), (snd (sr p), q))) s'))) ∈ trans (onp i ⟨⟨⇘i⇙ qp)"
by simp
next
show "∀j. init (np j ⟨⟨ qp) ≠ {}"
by (clarsimp simp add: init_notempty init_qp_notempty)
qed
end