Theory ONode_Lifting
section "Lifting rules for (open) nodes"
theory ONode_Lifting
imports AWN OAWN_SOS OInvariants
begin
lemma node_net_state':
assumes "s ∈ oreachable (⟨i : T : R⇩i⟩⇩o) S U"
shows "∃σ ζ R. s = (σ, NodeS i ζ R)"
using assms proof induction
fix s
assume "s ∈ init (⟨i : T : R⇩i⟩⇩o)"
then obtain σ ζ where "s = (σ, NodeS i ζ R⇩i)"
by (auto simp: onode_comps)
thus "∃σ ζ R. s = (σ, NodeS i ζ R)" by auto
next
fix s a σ'
assume rt: "s ∈ oreachable (⟨i : T : R⇩i⟩⇩o) S U"
and ih: "∃σ ζ R. s = (σ, NodeS i ζ R)"
and "U (fst s) σ'"
then obtain σ ζ R
where "(σ, NodeS i ζ R) ∈ oreachable (⟨i : T : R⇩i⟩⇩o) S U"
and "U σ σ'" and "snd s = NodeS i ζ R" by auto
from this(1-2)
have "(σ', NodeS i ζ R) ∈ oreachable (⟨i : T : R⇩i⟩⇩o) S U"
by - (erule(1) oreachable_other')
with ‹snd s = NodeS i ζ R› show "∃σ ζ R. (σ', snd s) = (σ, NodeS i ζ R)" by simp
next
fix s a s'
assume rt: "s ∈ oreachable (⟨i : T : R⇩i⟩⇩o) S U"
and ih: "∃σ ζ R. s = (σ, NodeS i ζ R)"
and tr: "(s, a, s') ∈ trans (⟨i : T : R⇩i⟩⇩o)"
and "S (fst s) (fst s') a"
from ih obtain σ ζ R where "s = (σ, NodeS i ζ R)" by auto
with tr have "((σ, NodeS i ζ R), a, s') ∈ onode_sos (trans T)"
by (simp add: onode_comps)
then obtain σ' ζ' R' where "s' = (σ', NodeS i ζ' R')"
using onode_sos_dest_is_net_state' by metis
with tr ‹s = (σ, NodeS i ζ R)› show "∃σ ζ R. s' = (σ, NodeS i ζ R)"
by simp
qed
lemma node_net_state:
assumes "(σ, s) ∈ oreachable (⟨i : T : R⇩i⟩⇩o) S U"
shows "∃ζ R. s = NodeS i ζ R"
using assms
by (metis Pair_inject node_net_state')
lemma node_net_state_trans [elim]:
assumes sor: "(σ, s) ∈ oreachable (⟨i : ζ⇩i : R⇩i⟩⇩o) S U"
and str: "((σ, s), a, (σ', s')) ∈ trans (⟨i : ζ⇩i : R⇩i⟩⇩o)"
obtains ζ R ζ' R'
where "s = NodeS i ζ R"
and "s' = NodeS i ζ' R'"
proof -
assume *: "⋀ζ R ζ' R'. s = NodeS i ζ R ⟹ s' = NodeS i ζ' R' ⟹ thesis"
from sor obtain ζ R where "s = NodeS i ζ R"
by (metis node_net_state)
moreover with str obtain ζ' R' where "s' = NodeS i ζ' R'"
by (simp only: onode_comps)
(metis onode_sos_dest_is_net_state'')
ultimately show thesis by (rule *)
qed
lemma nodemap_induct' [consumes, case_names init other local]:
assumes "(σ, NodeS ii ζ R) ∈ oreachable (⟨ii : T : R⇩i⟩⇩o) S U"
and init: "⋀σ ζ. (σ, NodeS ii ζ R⇩i) ∈ init (⟨ii : T : R⇩i⟩⇩o) ⟹ P (σ, NodeS ii ζ R⇩i)"
and other: "⋀σ ζ R σ' a.
⟦ (σ, NodeS ii ζ R) ∈ oreachable (⟨ii : T : R⇩i⟩⇩o) S U;
U σ σ'; P (σ, NodeS ii ζ R) ⟧ ⟹ P (σ', NodeS ii ζ R)"
and local: "⋀σ ζ R σ' ζ' R' a.
⟦ (σ, NodeS ii ζ R) ∈ oreachable (⟨ii : T : R⇩i⟩⇩o) S U;
((σ, NodeS ii ζ R), a, (σ', NodeS ii ζ' R')) ∈ trans (⟨ii : T : R⇩i⟩⇩o);
S σ σ' a; P (σ, NodeS ii ζ R) ⟧ ⟹ P (σ', NodeS ii ζ' R')"
shows "P (σ, NodeS ii ζ R)"
using assms(1) proof induction
fix s
assume "s ∈ init (⟨ii : T : R⇩i⟩⇩o)"
hence "s ∈ oreachable (⟨ii : T : R⇩i⟩⇩o) S U"
by (rule oreachable_init)
with ‹s ∈ init (⟨ii : T : R⇩i⟩⇩o)› obtain σ ζ where "s = (σ, NodeS ii ζ R⇩i)"
by (simp add: onode_comps) metis
with ‹s ∈ init (⟨ii : T : R⇩i⟩⇩o)› and init show "P s" by simp
next
fix s a σ'
assume sr: "s ∈ oreachable (⟨ii : T : R⇩i⟩⇩o) S U"
and "U (fst s) σ'"
and "P s"
from sr obtain σ ζ R where "s = (σ, NodeS ii ζ R)"
using node_net_state' by metis
with sr ‹U (fst s) σ'› ‹P s› show "P (σ', snd s)"
by simp (metis other)
next
fix s a s'
assume sr: "s ∈ oreachable (⟨ii : T : R⇩i⟩⇩o) S U"
and tr: "(s, a, s') ∈ trans (⟨ii : T : R⇩i⟩⇩o)"
and "S (fst s) (fst s') a"
and "P s"
from this(1-3) have "s' ∈ oreachable (⟨ii : T : R⇩i⟩⇩o) S U"
by - (erule(2) oreachable_local)
then obtain σ' ζ' R' where [simp]: "s' = (σ', NodeS ii ζ' R')"
using node_net_state' by metis
from sr and ‹P s› obtain σ ζ R
where [simp]: "s = (σ, NodeS ii ζ R)"
and A1: "(σ, NodeS ii ζ R) ∈ oreachable (⟨ii : T : R⇩i⟩⇩o) S U"
and A4: "P (σ, NodeS ii ζ R)"
using node_net_state' by metis
with tr and ‹S (fst s) (fst s') a›
have A2: "((σ, NodeS ii ζ R), a, (σ', NodeS ii ζ' R')) ∈ trans (⟨ii : T : R⇩i⟩⇩o)"
and A3: "S σ σ' a" by simp_all
from A1 A2 A3 A4 have "P (σ', NodeS ii ζ' R')" by (rule local)
thus "P s'" by simp
qed
lemma nodemap_induct [consumes, case_names init step]:
assumes "(σ, NodeS ii ζ R) ∈ oreachable (⟨ii : T : R⇩i⟩⇩o) S U"
and init: "⋀σ ζ. (σ, NodeS ii ζ R⇩i) ∈ init (⟨ii : T : R⇩i⟩⇩o) ⟹ P σ ζ R⇩i"
and other: "⋀σ ζ R σ' a.
⟦ (σ, NodeS ii ζ R) ∈ oreachable (⟨ii : T : R⇩i⟩⇩o) S U;
U σ σ'; P σ ζ R ⟧ ⟹ P σ' ζ R"
and local: "⋀σ ζ R σ' ζ' R' a.
⟦ (σ, NodeS ii ζ R) ∈ oreachable (⟨ii : T : R⇩i⟩⇩o) S U;
((σ, NodeS ii ζ R), a, (σ', NodeS ii ζ' R')) ∈ trans (⟨ii : T : R⇩i⟩⇩o);
S σ σ' a; P σ ζ R ⟧ ⟹ P σ' ζ' R'"
shows "P σ ζ R"
using assms(1) proof (induction "(σ, NodeS ii ζ R)" arbitrary: σ ζ R)
fix σ ζ R
assume a1: "(σ, NodeS ii ζ R) ∈ init (⟨ii : T : R⇩i⟩⇩o)"
hence "R = R⇩i" by (simp add: init_onode_comp)
with a1 have "(σ, NodeS ii ζ R⇩i) ∈ init (⟨ii : T : R⇩i⟩⇩o)" by simp
with init and ‹R = R⇩i› show "P σ ζ R" by simp
next
fix st a σ' ζ' R'
assume "st ∈ oreachable (⟨ii : T : R⇩i⟩⇩o) S U"
and tr: "(st, a, (σ', NodeS ii ζ' R')) ∈ trans (⟨ii : T : R⇩i⟩⇩o)"
and "S (fst st) (fst (σ', NodeS ii ζ' R')) a"
and IH: "⋀σ ζ R. st = (σ, NodeS ii ζ R) ⟹ P σ ζ R"
from this(1) obtain σ ζ R where "st = (σ, NodeS ii ζ R)"
and "(σ, NodeS ii ζ R) ∈ oreachable (⟨ii : T : R⇩i⟩⇩o) S U"
by (metis node_net_state')
note this(2)
moreover from tr and ‹st = (σ, NodeS ii ζ R)›
have "((σ, NodeS ii ζ R), a, (σ', NodeS ii ζ' R')) ∈ trans (⟨ii : T : R⇩i⟩⇩o)" by simp
moreover from ‹S (fst st) (fst (σ', NodeS ii ζ' R')) a› and ‹st = (σ, NodeS ii ζ R)›
have "S σ σ' a" by simp
moreover from IH and ‹st = (σ, NodeS ii ζ R)› have "P σ ζ R" .
ultimately show "P σ' ζ' R'" by (rule local)
next
fix st σ' ζ R
assume "st ∈ oreachable (⟨ii : T : R⇩i⟩⇩o) S U"
and "U (fst st) σ'"
and "snd st = NodeS ii ζ R"
and IH: "⋀σ ζ R. st = (σ, NodeS ii ζ R) ⟹ P σ ζ R"
from this(1,3) obtain σ where "st = (σ, NodeS ii ζ R)"
and "(σ, NodeS ii ζ R) ∈ oreachable (⟨ii : T : R⇩i⟩⇩o) S U"
by (metis surjective_pairing)
note this(2)
moreover from ‹U (fst st) σ'› and ‹st = (σ, NodeS ii ζ R)› have "U σ σ'" by simp
moreover from IH and ‹st = (σ, NodeS ii ζ R)› have "P σ ζ R" .
ultimately show "P σ' ζ R" by (rule other)
qed
lemma node_addressD [dest, simp]:
assumes "(σ, NodeS i ζ R) ∈ oreachable (⟨ii : T : R⇩i⟩⇩o) S U"
shows "i = ii"
using assms by (clarsimp dest!: node_net_state')
lemma node_proc_reachable [dest]:
assumes "(σ, NodeS i ζ R) ∈ oreachable (⟨ii : T : R⇩i⟩⇩o)
(otherwith S {ii} (oarrivemsg I)) (other U {ii})"
and sgivesu: "⋀ξ ξ'. S ξ ξ' ⟹ U ξ ξ'"
shows "(σ, ζ) ∈ oreachable T (otherwith S {ii} (orecvmsg I)) (other U {ii})"
proof -
from assms(1) have "(σ, NodeS ii ζ R) ∈ oreachable (⟨ii : T : R⇩i⟩⇩o)
(otherwith S {ii} (oarrivemsg I)) (other U {ii})"
by - (frule node_addressD, simp)
thus ?thesis
proof (induction rule: nodemap_induct)
fix σ ζ
assume "(σ, NodeS ii ζ R⇩i) ∈ init (⟨ii : T : R⇩i⟩⇩o)"
hence "(σ, ζ) ∈ init T" by (auto simp: onode_comps)
thus "(σ, ζ) ∈ oreachable T (otherwith S {ii} (orecvmsg I)) (other U {ii})"
by (rule oreachable_init)
next
fix σ ζ R σ' ζ' R' a
assume "other U {ii} σ σ'"
and "(σ, ζ) ∈ oreachable T (otherwith S {ii} (orecvmsg I)) (other U {ii})"
thus "(σ', ζ) ∈ oreachable T (otherwith S {ii} (orecvmsg I)) (other U {ii})"
by - (rule oreachable_other')
next
fix σ ζ R σ' ζ' R' a
assume rs: "(σ, NodeS ii ζ R) ∈ oreachable (⟨ii : T : R⇩i⟩⇩o)
(otherwith S {ii} (oarrivemsg I)) (other U {ii})"
and tr: "((σ, NodeS ii ζ R), a, (σ', NodeS ii ζ' R')) ∈ trans (⟨ii : T : R⇩i⟩⇩o)"
and ow: "otherwith S {ii} (oarrivemsg I) σ σ' a"
and ih: "(σ, ζ) ∈ oreachable T (otherwith S {ii} (orecvmsg I)) (other U {ii})"
from ow have *: "σ' ii = σ ii ⟹ other U {ii} σ σ'"
by (clarsimp elim!: otherwithE) (rule otherI, simp_all, metis sgivesu)
from tr have "((σ, NodeS ii ζ R), a, (σ', NodeS ii ζ' R')) ∈ onode_sos (trans T)"
by (simp add: onode_comps)
thus "(σ', ζ') ∈ oreachable T (otherwith S {ii} (orecvmsg I)) (other U {ii})"
proof cases
case onode_bcast
with ih and ow show ?thesis
by (auto elim!: oreachable_local' otherwithE)
next
case onode_gcast
with ih and ow show ?thesis
by (auto elim!: oreachable_local' otherwithE)
next
case onode_ucast
with ih and ow show ?thesis
by (auto elim!: oreachable_local' otherwithE)
next
case onode_notucast
with ih and ow show ?thesis
by (auto elim!: oreachable_local' otherwithE)
next
case onode_deliver
with ih and ow show ?thesis
by (auto elim!: oreachable_local' otherwithE)
next
case onode_tau
with ih and ow show ?thesis
by (auto elim!: oreachable_local' otherwithE)
next
case onode_receive
with ih and ow show ?thesis
by (auto elim!: oreachable_local' otherwithE)
next
case (onode_arrive m)
hence "ζ' = ζ" and "σ' ii = σ ii" by auto
from this(2) have "other U {ii} σ σ'" by (rule *)
with ih and ‹ζ' = ζ› show ?thesis by auto
next
case onode_connect1
hence "ζ' = ζ" and "σ' ii = σ ii" by auto
from this(2) have "other U {ii} σ σ'" by (rule *)
with ih and ‹ζ' = ζ› show ?thesis by auto
next
case onode_connect2
hence "ζ' = ζ" and "σ' ii = σ ii" by auto
from this(2) have "other U {ii} σ σ'" by (rule *)
with ih and ‹ζ' = ζ› show ?thesis by auto
next
case onode_connect_other
hence "ζ' = ζ" and "σ' ii = σ ii" by auto
from this(2) have "other U {ii} σ σ'" by (rule *)
with ih and ‹ζ' = ζ› show ?thesis by auto
next
case onode_disconnect1
hence "ζ' = ζ" and "σ' ii = σ ii" by auto
from this(2) have "other U {ii} σ σ'" by (rule *)
with ih and ‹ζ' = ζ› show ?thesis by auto
next
case onode_disconnect2
hence "ζ' = ζ" and "σ' ii = σ ii" by auto
from this(2) have "other U {ii} σ σ'" by (rule *)
with ih and ‹ζ' = ζ› show ?thesis by auto
next
case onode_disconnect_other
hence "ζ' = ζ" and "σ' ii = σ ii" by auto
from this(2) have "other U {ii} σ σ'" by (rule *)
with ih and ‹ζ' = ζ› show ?thesis by auto
qed
qed
qed
lemma node_proc_reachable_statelessassm [dest]:
assumes "(σ, NodeS i ζ R) ∈ oreachable (⟨ii : T : R⇩i⟩⇩o)
(otherwith (λ_ _. True) {ii} (oarrivemsg I))
(other (λ_ _. True) {ii})"
shows "(σ, ζ) ∈ oreachable T
(otherwith (λ_ _. True) {ii} (orecvmsg I)) (other (λ_ _. True) {ii})"
using assms
by (rule node_proc_reachable) simp_all
lemma node_lift:
assumes "T ⊨ (otherwith S {ii} (orecvmsg I), other U {ii} →) global P"
and "⋀ξ ξ'. S ξ ξ' ⟹ U ξ ξ'"
shows "⟨ii : T : R⇩i⟩⇩o ⊨ (otherwith S {ii} (oarrivemsg I), other U {ii} →) global P"
proof (rule oinvariant_oreachableI)
fix σ ζ
assume "(σ, ζ) ∈ oreachable (⟨ii : T : R⇩i⟩⇩o) (otherwith S {ii} (oarrivemsg I)) (other U {ii})"
moreover then obtain i s R where "ζ = NodeS i s R"
by (metis node_net_state)
ultimately have "(σ, NodeS i s R) ∈ oreachable (⟨ii : T : R⇩i⟩⇩o)
(otherwith S {ii} (oarrivemsg I)) (other U {ii})"
by simp
hence "(σ, s) ∈ oreachable T (otherwith S {ii} (orecvmsg I)) (other U {ii})"
by - (erule node_proc_reachable, erule assms(2))
with assms(1) show "global P (σ, ζ)"
by (metis fst_conv globalsimp oinvariantD)
qed
lemma node_lift_step [intro]:
assumes pinv: "T ⊨⇩A (otherwith S {i} (orecvmsg I), other U {i} →) globala (λ(σ, _, σ'). Q σ σ')"
and other: "⋀σ σ'. other U {i} σ σ' ⟹ Q σ σ'"
and sgivesu: "⋀ξ ξ'. S ξ ξ' ⟹ U ξ ξ'"
shows "⟨i : T : R⇩i⟩⇩o ⊨⇩A (otherwith S {i} (oarrivemsg I), other U {i} →)
globala (λ(σ, _, σ'). Q σ σ')"
(is "_ ⊨⇩A (?S, ?U →) _")
proof (rule ostep_invariantI, simp)
fix σ s a σ' s'
assume rs: "(σ, s) ∈ oreachable (⟨i : T : R⇩i⟩⇩o) ?S ?U"
and tr: "((σ, s), a, (σ', s')) ∈ trans (⟨i : T : R⇩i⟩⇩o)"
and ow: "?S σ σ' a"
from ow have *: "σ' i = σ i ⟹ other U {i} σ σ'"
by (clarsimp elim!: otherwithE) (rule otherI, simp_all, metis sgivesu)
from rs tr obtain ζ R
where [simp]: "s = NodeS i ζ R"
and "(σ, NodeS i ζ R) ∈ oreachable (⟨i : T : R⇩i⟩⇩o) ?S ?U"
by (metis node_net_state)
from this(2) have or: "(σ, ζ) ∈ oreachable T (otherwith S {i} (orecvmsg I)) ?U"
by (rule node_proc_reachable [OF _ assms(3)])
from tr have "((σ, NodeS i ζ R), a, (σ', s')) ∈ onode_sos (trans T)"
by (simp add: onode_comps)
thus "Q σ σ'"
proof cases
fix m ζ'
assume "a = R:*cast(m)"
and tr': "((σ, ζ), broadcast m, (σ', ζ')) ∈ trans T"
from this(1) and ‹?S σ σ' a› have "otherwith S {i} (orecvmsg I) σ σ' (broadcast m)"
by (auto elim!: otherwithE)
with or tr' show ?thesis by (rule ostep_invariantD [OF pinv, simplified])
next
fix D m ζ'
assume "a = (R ∩ D):*cast(m)"
and tr': "((σ, ζ), groupcast D m, (σ', ζ')) ∈ trans T"
from this(1) and ‹?S σ σ' a› have "otherwith S {i} (orecvmsg I) σ σ' (groupcast D m)"
by (auto elim!: otherwithE)
with or tr' show ?thesis by (rule ostep_invariantD [OF pinv, simplified])
next
fix d m ζ'
assume "a = {d}:*cast(m)"
and tr': "((σ, ζ), unicast d m, (σ', ζ')) ∈ trans T"
from this(1) and ‹?S σ σ' a› have "otherwith S {i} (orecvmsg I) σ σ' (unicast d m)"
by (auto elim!: otherwithE)
with or tr' show ?thesis by (rule ostep_invariantD [OF pinv, simplified])
next
fix d ζ'
assume "a = τ"
and tr': "((σ, ζ), ¬unicast d, (σ', ζ')) ∈ trans T"
from this(1) and ‹?S σ σ' a› have "otherwith S {i} (orecvmsg I) σ σ' (¬unicast d)"
by (auto elim!: otherwithE)
with or tr' show ?thesis by (rule ostep_invariantD [OF pinv, simplified])
next
fix d ζ'
assume "a = i:deliver(d)"
and tr': "((σ, ζ), deliver d, (σ', ζ')) ∈ trans T"
from this(1) and ‹?S σ σ' a› have "otherwith S {i} (orecvmsg I) σ σ' (deliver d)"
by (auto elim!: otherwithE)
with or tr' show ?thesis by (rule ostep_invariantD [OF pinv, simplified])
next
fix ζ'
assume "a = τ"
and tr': "((σ, ζ), τ, (σ', ζ')) ∈ trans T"
from this(1) and ‹?S σ σ' a› have "otherwith S {i} (orecvmsg I) σ σ' τ"
by (auto elim!: otherwithE)
with or tr' show ?thesis by (rule ostep_invariantD [OF pinv, simplified])
next
fix m ζ'
assume "a = {i}¬{}:arrive(m)"
and tr': "((σ, ζ), receive m, (σ', ζ')) ∈ trans T"
from this(1) and ‹?S σ σ' a› have "otherwith S {i} (orecvmsg I) σ σ' (receive m)"
by (auto elim!: otherwithE)
with or tr' show ?thesis by (rule ostep_invariantD [OF pinv, simplified])
next
fix m
assume "a = {}¬{i}:arrive(m)"
and "σ' i = σ i"
from this(2) have "other U {i} σ σ'" by (rule *)
thus ?thesis by (rule other)
next
fix i'
assume "a = connect(i, i')"
and "σ' i = σ i"
from this(2) have "other U {i} σ σ'" by (rule *)
thus ?thesis by (rule other)
next
fix i'
assume "a = connect(i', i)"
and "σ' i = σ i"
from this(2) have "other U {i} σ σ'" by (rule *)
thus ?thesis by (rule other)
next
fix i' i''
assume "a = connect(i', i'')"
and "σ' i = σ i"
from this(2) have "other U {i} σ σ'" by (rule *)
thus ?thesis by (rule other)
next
fix i'
assume "a = disconnect(i, i')"
and "σ' i = σ i"
from this(2) have "other U {i} σ σ'" by (rule *)
thus ?thesis by (rule other)
next
fix i'
assume "a = disconnect(i', i)"
and "σ' i = σ i"
from this(2) have "other U {i} σ σ'" by (rule *)
thus ?thesis by (rule other)
next
fix i' i''
assume "a = disconnect(i', i'')"
and "σ' i = σ i"
from this(2) have "other U {i} σ σ'" by (rule *)
thus ?thesis by (rule other)
qed
qed
lemma node_lift_step_statelessassm [intro]:
assumes "T ⊨⇩A (λσ _. orecvmsg I σ, other (λ_ _. True) {i} →)
globala (λ(σ, _, σ'). Q (σ i) (σ' i))"
and "⋀ξ. Q ξ ξ"
shows "⟨i : T : R⇩i⟩⇩o ⊨⇩A (λσ _. oarrivemsg I σ, other (λ_ _. True) {i} →)
globala (λ(σ, _, σ'). Q (σ i) (σ' i))"
proof -
from assms(1)
have "T ⊨⇩A (otherwith (λ_ _. True) {i} (orecvmsg I), other (λ_ _. True) {i} →)
globala (λ(σ, _, σ'). Q (σ i) (σ' i))"
by rule auto
with assms(2) have "⟨i : T : R⇩i⟩⇩o ⊨⇩A (otherwith (λ_ _. True) {i} (oarrivemsg I),
other (λ_ _. True) {i} →)
globala (λ(σ, _, σ'). Q (σ i) (σ' i))"
by - (rule node_lift_step, auto)
thus ?thesis by rule auto
qed
lemma node_lift_anycast [intro]:
assumes pinv: "T ⊨⇩A (otherwith S {i} (orecvmsg I), other U {i} →)
globala (λ(σ, a, σ'). anycast (Q σ σ') a)"
and "⋀ξ ξ'. S ξ ξ' ⟹ U ξ ξ'"
shows "⟨i : T : R⇩i⟩⇩o ⊨⇩A (otherwith S {i} (oarrivemsg I), other U {i} →)
globala (λ(σ, a, σ'). castmsg (Q σ σ') a)"
(is "_ ⊨⇩A (?S, ?U →) _")
proof (rule ostep_invariantI, simp)
fix σ s a σ' s'
assume rs: "(σ, s) ∈ oreachable (⟨i : T : R⇩i⟩⇩o) ?S ?U"
and tr: "((σ, s), a, (σ', s')) ∈ trans (⟨i : T : R⇩i⟩⇩o)"
and "?S σ σ' a"
from this(1-2) obtain ζ R
where [simp]: "s = NodeS i ζ R"
and "(σ, NodeS i ζ R) ∈ oreachable (⟨i : T : R⇩i⟩⇩o) ?S ?U"
by (metis node_net_state)
from this(2) have "(σ, ζ) ∈ oreachable T (otherwith S {i} (orecvmsg I)) ?U"
by (rule node_proc_reachable [OF _ assms(2)])
moreover from tr have "((σ, NodeS i ζ R), a, (σ', s')) ∈ onode_sos (trans T)"
by (simp add: onode_comps)
ultimately show "castmsg (Q σ σ') a" using ‹?S σ σ' a›
by - (erule onode_sos.cases, auto elim!: otherwithE dest!: ostep_invariantD [OF pinv])
qed
lemma node_lift_anycast_statelessassm [intro]:
assumes pinv: "T ⊨⇩A (λσ _. orecvmsg I σ, other (λ_ _. True) {i} →)
globala (λ(σ, a, σ'). anycast (Q σ σ') a)"
shows "⟨i : T : R⇩i⟩⇩o ⊨⇩A (λσ _. oarrivemsg I σ, other (λ_ _. True) {i} →)
globala (λ(σ, a, σ'). castmsg (Q σ σ') a)"
(is "_ ⊨⇩A (?S, _ →) _")
proof -
from assms(1)
have "T ⊨⇩A (otherwith (λ_ _. True) {i} (orecvmsg I), other (λ_ _. True) {i} →)
globala (λ(σ, a, σ'). anycast (Q σ σ') a)"
by rule auto
hence "⟨i : T : R⇩i⟩⇩o ⊨⇩A (otherwith (λ_ _. True) {i} (oarrivemsg I), other (λ_ _. True) {i} →)
globala (λ(σ, a, σ'). castmsg (Q σ σ') a)"
by (rule node_lift_anycast) simp_all
thus ?thesis
by rule auto
qed
lemma node_local_deliver:
"⟨i : ζ⇩i : R⇩i⟩⇩o ⊨⇩A (S, U →) globala (λ(_, a, _). ∀j. j≠i ⟶ (∀d. a ≠ j:deliver(d)))"
proof (rule ostep_invariantI, simp)
fix σ s a σ' s'
assume 1: "(σ, s) ∈ oreachable (⟨i : ζ⇩i : R⇩i⟩⇩o) S U"
and 2: "((σ, s), a, (σ', s')) ∈ trans (⟨i : ζ⇩i : R⇩i⟩⇩o)"
and "S σ σ' a"
moreover from 1 2 obtain ζ R ζ' R' where "s = NodeS i ζ R" and "s' = NodeS i ζ' R'" ..
ultimately show "∀j. j≠i ⟶ (∀d. a ≠ j:deliver(d))"
by (cases a) (auto simp add: onode_comps)
qed
lemma node_tau_deliver_unchanged:
"⟨i : ζ⇩i : R⇩i⟩⇩o ⊨⇩A (S, U →) globala (λ(σ, a, σ'). a = τ ∨ (∃i d. a = i:deliver(d))
⟶ (∀j. j≠i ⟶ σ' j = σ j))"
proof (rule ostep_invariantI, clarsimp simp only: globalasimp snd_conv fst_conv)
fix σ s a σ' s' j
assume 1: "(σ, s) ∈ oreachable (⟨i : ζ⇩i : R⇩i⟩⇩o) S U"
and 2: "((σ, s), a, (σ', s')) ∈ trans (⟨i : ζ⇩i : R⇩i⟩⇩o)"
and "S σ σ' a"
and "a = τ ∨ (∃i d. a = i:deliver(d))"
and "j ≠ i"
moreover from 1 2 obtain ζ R ζ' R' where "s = NodeS i ζ R" and "s' = NodeS i ζ' R'" ..
ultimately show "σ' j = σ j"
by (cases a) (auto simp del: step_node_tau simp add: onode_comps)
qed
end