Theory Closed
section "Lemmas for closed networks"
theory Closed
imports Pnet
begin
lemma complete_net_preserves_subnets:
assumes "(SubnetS s t, a, st') ∈ cnet_sos (pnet_sos (trans (pnet np p1)) (trans (pnet np p2)))"
shows "∃s' t'. st' = SubnetS s' t'"
using assms by cases (auto dest: partial_net_preserves_subnets)
lemma complete_net_reachable_is_subnet:
assumes "st ∈ reachable (closed (pnet np (p1 ∥ p2))) I"
shows "∃s t. st = SubnetS s t"
using assms by induction (auto dest!: complete_net_preserves_subnets)
lemma closed_reachable_par_subnet_induct [consumes, case_names init step]:
assumes "SubnetS s t ∈ reachable (closed (pnet np (p1 ∥ p2))) I"
and init: "⋀s t. SubnetS s t ∈ init (closed (pnet np (p1 ∥ p2))) ⟹ P s t"
and step: "⋀s t s' t' a. ⟦
SubnetS s t ∈ reachable (closed (pnet np (p1 ∥ p2))) I;
P s t; (SubnetS s t, a, SubnetS s' t') ∈ trans (closed (pnet np (p1 ∥ p2))); I a ⟧
⟹ P s' t'"
shows "P s t"
using assms(1) proof (induction "SubnetS s t" arbitrary: s t)
fix s t
assume "SubnetS s t ∈ init (closed (pnet np (p1 ∥ p2)))"
with init show "P s t" .
next
fix st a s' t'
assume "st ∈ reachable (closed (pnet np (p1 ∥ p2))) I"
and tr: "(st, a, SubnetS s' t') ∈ trans (closed (pnet np (p1 ∥ p2)))"
and "I a"
and IH: "⋀s t. st = SubnetS s t ⟹ P s t"
from this(1) obtain s t where "st = SubnetS s t"
and "SubnetS s t ∈ reachable (closed (pnet np (p1 ∥ p2))) I"
by (metis complete_net_reachable_is_subnet)
note this(2)
moreover from IH and ‹st = SubnetS s t› have "P s t" .
moreover from tr and ‹st = SubnetS s t›
have "(SubnetS s t, a, SubnetS s' t') ∈ trans (closed (pnet np (p1 ∥ p2)))" by simp
ultimately show "P s' t'"
using ‹I a› by (rule assms(3))
qed
lemma reachable_closed_reachable_pnet [elim]:
assumes "s ∈ reachable (closed (pnet np n)) TT"
shows "s ∈ reachable (pnet np n) TT"
using assms proof (induction rule: reachable.induct)
fix s s' a
assume sr: "s ∈ reachable (pnet np n) TT"
and "(s, a, s') ∈ trans (closed (pnet np n))"
from this(2) have "(s, a, s') ∈ cnet_sos (trans (pnet np n))" by simp
thus "s' ∈ reachable (pnet np n) TT"
by cases (insert sr, auto elim!: reachable_step)
qed (auto elim: reachable_init)
lemma closed_node_net_state [elim]:
assumes "st ∈ reachable (closed (pnet np ⟨ii; R⇩i⟩)) TT"
obtains ξ p q R where "st = NodeS ii ((ξ, p), q) R"
using assms by (metis net_node_reachable_is_node reachable_closed_reachable_pnet surj_pair)
lemma closed_subnet_net_state [elim]:
assumes "st ∈ reachable (closed (pnet np (p1 ∥ p2))) TT"
obtains s t where "st = SubnetS s t"
using assms by (metis reachable_closed_reachable_pnet net_par_reachable_is_subnet)
lemma closed_imp_pnet_trans [elim, dest]:
assumes "(s, a, s') ∈ trans (closed (pnet np n))"
shows "∃a'. (s, a', s') ∈ trans (pnet np n)"
using assms by (auto elim!: cnet_sos.cases)
lemma reachable_not_in_net_tree_ips [elim]:
assumes "s ∈ reachable (closed (pnet np n)) TT"
and "i∉net_tree_ips n"
shows "netmap s i = None"
using assms proof induction
fix s
assume "s ∈ init (closed (pnet np n))"
and "i ∉ net_tree_ips n"
thus "netmap s i = None"
proof (induction n arbitrary: s)
fix ii R s
assume "s ∈ init (closed (pnet np ⟨ii; R⟩))"
and "i ∉ net_tree_ips ⟨ii; R⟩"
from this(2) have "i ≠ ii" by simp
moreover from ‹s ∈ init (closed (pnet np ⟨ii; R⟩))› obtain p where "s = NodeS ii p R"
by simp (metis pnet.simps(1) pnet_node_init')
ultimately show "netmap s i = None" by simp
next
fix p1 p2 s
assume IH1: "⋀s. s ∈ init (closed (pnet np p1)) ⟹ i ∉ net_tree_ips p1
⟹ netmap s i = None"
and IH2: "⋀s. s ∈ init (closed (pnet np p2)) ⟹ i ∉ net_tree_ips p2
⟹ netmap s i = None"
and "s ∈ init (closed (pnet np (p1 ∥ p2)))"
and "i ∉ net_tree_ips (p1 ∥ p2)"
from this(3) obtain s1 s2 where "s = SubnetS s1 s2"
and "s1 ∈ init (closed (pnet np p1))"
and "s2 ∈ init (closed (pnet np p2))" by simp metis
moreover from ‹i ∉ net_tree_ips (p1 ∥ p2)› have "i ∉ net_tree_ips p1"
and "i ∉ net_tree_ips p2" by auto
ultimately have "netmap s1 i = None"
and "netmap s2 i = None"
using IH1 IH2 by auto
with ‹s = SubnetS s1 s2› show "netmap s i = None" by simp
qed
next
fix s a s'
assume sr: "s ∈ reachable (closed (pnet np n)) TT"
and tr: "(s, a, s') ∈ trans (closed (pnet np n))"
and IH: "i ∉ net_tree_ips n ⟹ netmap s i = None"
and "i ∉ net_tree_ips n"
from this(3-4) have "i∉net_ips s" by auto
with tr have "i∉net_ips s'"
by simp (erule cnet_sos.cases, (metis net_ips_is_dom_netmap pnet_maintains_dom)+)
thus "netmap s' i = None" by simp
qed
lemma closed_pnet_aodv_init [elim]:
assumes "s ∈ init (closed (pnet np n))"
and "i∈net_tree_ips n"
shows "the (netmap s i) ∈ init (np i)"
using assms proof (induction n arbitrary: s)
fix ii R s
assume "s ∈ init (closed (pnet np ⟨ii; R⟩))"
and "i∈net_tree_ips ⟨ii; R⟩"
hence "s ∈ init (pnet np ⟨i; R⟩)" by simp
then obtain p where "s = NodeS i p R"
and "p ∈ init (np i)" ..
with ‹s = NodeS i p R› have "netmap s = [i ↦ p]" by simp
with ‹p ∈ init (np i)› show "the (netmap s i) ∈ init (np i)" by simp
next
fix p1 p2 s
assume IH1: "⋀s. s ∈ init (closed (pnet np p1)) ⟹
i∈net_tree_ips p1 ⟹ the (netmap s i) ∈ init (np i)"
and IH2: "⋀s. s ∈ init (closed (pnet np p2)) ⟹
i∈net_tree_ips p2 ⟹ the (netmap s i) ∈ init (np i)"
and "s ∈ init (closed (pnet np (p1 ∥ p2)))"
and "i∈net_tree_ips (p1 ∥ p2)"
from this(3) obtain s1 s2 where "s = SubnetS s1 s2"
and "s1 ∈ init (closed (pnet np p1))"
and "s2 ∈ init (closed (pnet np p2))"
by auto
from this(2) have "net_tree_ips p1 = net_ips s1"
by (clarsimp dest!: pnet_init_net_ips_net_tree_ips)
from ‹s2 ∈ init (closed (pnet np p2))› have "net_tree_ips p2 = net_ips s2"
by (clarsimp dest!: pnet_init_net_ips_net_tree_ips)
show "the (netmap s i) ∈ init (np i)"
proof (cases "i∈net_tree_ips p2")
assume "i∈net_tree_ips p2"
with ‹s2 ∈ init (closed (pnet np p2))› have "the (netmap s2 i) ∈ init (np i)"
by (rule IH2)
moreover from ‹i∈net_tree_ips p2› and ‹net_tree_ips p2 = net_ips s2›
have "i∈net_ips s2" by simp
ultimately show ?thesis
using ‹s = SubnetS s1 s2› by (auto simp add: net_ips_is_dom_netmap)
next
assume "i∉net_tree_ips p2"
with ‹i∈net_tree_ips (p1 ∥ p2)› have "i∈net_tree_ips p1" by simp
with ‹s1 ∈ init (closed (pnet np p1))› have "the (netmap s1 i) ∈ init (np i)"
by (rule IH1)
moreover from ‹i∈net_tree_ips p1› and ‹net_tree_ips p1 = net_ips s1›
have "i∈net_ips s1" by simp
moreover from ‹i∉net_tree_ips p2› and ‹net_tree_ips p2 = net_ips s2›
have "i∉net_ips s2" by simp
ultimately show ?thesis
using ‹s = SubnetS s1 s2›
by (simp add: map_add_dom_app_simps net_ips_is_dom_netmap)
qed
qed
end