Theory A_Global_Invariants
section "Global invariant proofs over sequential processes"
theory A_Global_Invariants
imports A_Seq_Invariants
A_Aodv_Predicates
A_Fresher
A_Quality_Increases
AWN.OAWN_Convert
A_OAodv
begin
lemma other_quality_increases [elim]:
assumes "other quality_increases I σ σ'"
shows "∀j. quality_increases (σ j) (σ' j)"
using assms by (rule, clarsimp) (metis quality_increases_refl)
lemma weaken_otherwith [elim]:
fixes m
assumes *: "otherwith P I (orecvmsg Q) σ σ' a"
and weakenP: "⋀σ m. P σ m ⟹ P' σ m"
and weakenQ: "⋀σ m. Q σ m ⟹ Q' σ m"
shows "otherwith P' I (orecvmsg Q') σ σ' a"
proof
fix j
assume "j∉I"
with * have "P (σ j) (σ' j)" by auto
thus "P' (σ j) (σ' j)" by (rule weakenP)
next
from * have "orecvmsg Q σ a" by auto
thus "orecvmsg Q' σ a"
by rule (erule weakenQ)
qed
lemma oreceived_msg_inv:
assumes other: "⋀σ σ' m. ⟦ P σ m; other Q {i} σ σ' ⟧ ⟹ P σ' m"
and local: "⋀σ m. P σ m ⟹ P (σ(i := σ i⦇msg := m⦈)) m"
shows "opaodv i ⊨ (otherwith Q {i} (orecvmsg P), other Q {i} →)
onl Γ⇩A⇩O⇩D⇩V (λ(σ, l). l ∈ {PAodv-:1} ⟶ P σ (msg (σ i)))"
proof (inv_cterms, intro impI)
fix σ σ' l
assume "l = PAodv-:1 ⟶ P σ (msg (σ i))"
and "l = PAodv-:1"
and "other Q {i} σ σ'"
from this(1-2) have "P σ (msg (σ i))" ..
hence "P σ' (msg (σ i))" using ‹other Q {i} σ σ'›
by (rule other)
moreover from ‹other Q {i} σ σ'› have "σ' i = σ i" ..
ultimately show "P σ' (msg (σ' i))" by simp
next
fix σ σ' msg
assume "otherwith Q {i} (orecvmsg P) σ σ' (receive msg)"
and "σ' i = σ i⦇msg := msg⦈"
from this(1) have "P σ msg"
and "∀j. j≠i ⟶ Q (σ j) (σ' j)" by auto
from this(1) have "P (σ(i := σ i⦇msg := msg⦈)) msg" by (rule local)
thus "P σ' msg"
proof (rule other)
from ‹σ' i = σ i⦇msg := msg⦈› and ‹∀j. j≠i ⟶ Q (σ j) (σ' j)›
show "other Q {i} (σ(i := σ i⦇msg := msg⦈)) σ'"
by - (rule otherI, auto)
qed
qed
text ‹(Equivalent to) Proposition 7.27›
lemma local_quality_increases:
"paodv i ⊫⇩A (recvmsg rreq_rrep_sn →) onll Γ⇩A⇩O⇩D⇩V (λ((ξ, _), _, (ξ', _)). quality_increases ξ ξ')"
proof (rule step_invariantI)
fix s a s'
assume sr: "s ∈ reachable (paodv i) (recvmsg rreq_rrep_sn)"
and tr: "(s, a, s') ∈ trans (paodv i)"
and rm: "recvmsg rreq_rrep_sn a"
from sr have srTT: "s ∈ reachable (paodv i) TT" ..
from route_tables_fresher sr tr rm
have "onll Γ⇩A⇩O⇩D⇩V (λ((ξ, _), _, (ξ', _)). ∀dip∈kD (rt ξ). rt ξ ⊑⇘dip⇙ rt ξ') (s, a, s')"
by (rule step_invariantD)
moreover from known_destinations_increase srTT tr TT_True
have "onll Γ⇩A⇩O⇩D⇩V (λ((ξ, _), _, (ξ', _)). kD (rt ξ) ⊆ kD (rt ξ')) (s, a, s')"
by (rule step_invariantD)
moreover from sqns_increase srTT tr TT_True
have "onll Γ⇩A⇩O⇩D⇩V (λ((ξ, _), _, (ξ', _)). ∀ip. sqn (rt ξ) ip ≤ sqn (rt ξ') ip) (s, a, s')"
by (rule step_invariantD)
ultimately show "onll Γ⇩A⇩O⇩D⇩V (λ((ξ, _), _, (ξ', _)). quality_increases ξ ξ') (s, a, s')"
unfolding onll_def by auto
qed
lemmas olocal_quality_increases =
open_seq_step_invariant [OF local_quality_increases initiali_aodv oaodv_trans aodv_trans,
simplified seqll_onll_swap]
lemma oquality_increases:
"opaodv i ⊨⇩A (otherwith quality_increases {i} (orecvmsg (λ_. rreq_rrep_sn)),
other quality_increases {i} →)
onll Γ⇩A⇩O⇩D⇩V (λ((σ, _), _, (σ', _)). ∀j. quality_increases (σ j) (σ' j))"
(is "_ ⊨⇩A (?S, _ →) _")
proof (rule onll_ostep_invariantI, simp)
fix σ p l a σ' p' l'
assume or: "(σ, p) ∈ oreachable (opaodv i) ?S (other quality_increases {i})"
and ll: "l ∈ labels Γ⇩A⇩O⇩D⇩V p"
and "?S σ σ' a"
and tr: "((σ, p), a, (σ', p')) ∈ oseqp_sos Γ⇩A⇩O⇩D⇩V i"
and ll': "l' ∈ labels Γ⇩A⇩O⇩D⇩V p'"
from this(1-3) have "orecvmsg (λ_. rreq_rrep_sn) σ a"
by (auto dest!: oreachable_weakenE [where QS="act (recvmsg rreq_rrep_sn)"
and QU="other quality_increases {i}"]
otherwith_actionD)
with or have orw: "(σ, p) ∈ oreachable (opaodv i) (act (recvmsg rreq_rrep_sn))
(other quality_increases {i})"
by - (erule oreachable_weakenE, auto)
with tr ll ll' and ‹orecvmsg (λ_. rreq_rrep_sn) σ a› have "quality_increases (σ i) (σ' i)"
by - (drule onll_ostep_invariantD [OF olocal_quality_increases], auto simp: seqll_def)
with ‹?S σ σ' a› show "∀j. quality_increases (σ j) (σ' j)"
by (auto dest!: otherwith_syncD)
qed
lemma rreq_rrep_nsqn_fresh_any_step_invariant:
"opaodv i ⊨⇩A (act (recvmsg rreq_rrep_sn), other A {i} →)
onll Γ⇩A⇩O⇩D⇩V (λ((σ, _), a, _). anycast (msg_fresh σ) a)"
proof (rule ostep_invariantI, simp del: act_simp)
fix σ p a σ' p'
assume or: "(σ, p) ∈ oreachable (opaodv i) (act (recvmsg rreq_rrep_sn)) (other A {i})"
and "((σ, p), a, (σ', p')) ∈ oseqp_sos Γ⇩A⇩O⇩D⇩V i"
and recv: "act (recvmsg rreq_rrep_sn) σ σ' a"
obtain l l' where "l∈labels Γ⇩A⇩O⇩D⇩V p" and "l'∈labels Γ⇩A⇩O⇩D⇩V p'"
by (metis aodv_ex_label)
from ‹((σ, p), a, (σ', p')) ∈ oseqp_sos Γ⇩A⇩O⇩D⇩V i›
have tr: "((σ, p), a, (σ', p')) ∈ trans (opaodv i)" by simp
have "anycast (rreq_rrep_fresh (rt (σ i))) a"
proof -
have "opaodv i ⊨⇩A (act (recvmsg rreq_rrep_sn), other A {i} →)
onll Γ⇩A⇩O⇩D⇩V (seqll i (λ((ξ, _), a, _). anycast (rreq_rrep_fresh (rt ξ)) a))"
by (rule ostep_invariant_weakenE [OF
open_seq_step_invariant [OF rreq_rrep_fresh_any_step_invariant initiali_aodv,
simplified seqll_onll_swap]]) auto
hence "onll Γ⇩A⇩O⇩D⇩V (seqll i (λ((ξ, _), a, _). anycast (rreq_rrep_fresh (rt ξ)) a))
((σ, p), a, (σ', p'))"
using or tr recv by - (erule(4) ostep_invariantE)
thus ?thesis
using ‹l∈labels Γ⇩A⇩O⇩D⇩V p› and ‹l'∈labels Γ⇩A⇩O⇩D⇩V p'› by auto
qed
moreover have "anycast (rerr_invalid (rt (σ i))) a"
proof -
have "opaodv i ⊨⇩A (act (recvmsg rreq_rrep_sn), other A {i} →)
onll Γ⇩A⇩O⇩D⇩V (seqll i (λ((ξ, _), a, _). anycast (rerr_invalid (rt ξ)) a))"
by (rule ostep_invariant_weakenE [OF
open_seq_step_invariant [OF rerr_invalid_any_step_invariant initiali_aodv,
simplified seqll_onll_swap]]) auto
hence "onll Γ⇩A⇩O⇩D⇩V (seqll i (λ((ξ, _), a, _). anycast (rerr_invalid (rt ξ)) a))
((σ, p), a, (σ', p'))"
using or tr recv by - (erule(4) ostep_invariantE)
thus ?thesis
using ‹l∈labels Γ⇩A⇩O⇩D⇩V p› and ‹l'∈labels Γ⇩A⇩O⇩D⇩V p'› by auto
qed
moreover have "anycast rreq_rrep_sn a"
proof -
from or tr recv
have "onll Γ⇩A⇩O⇩D⇩V (seqll i (λ(_, a, _). anycast rreq_rrep_sn a)) ((σ, p), a, (σ', p'))"
by (rule ostep_invariantE [OF
open_seq_step_invariant [OF rreq_rrep_sn_any_step_invariant initiali_aodv
oaodv_trans aodv_trans,
simplified seqll_onll_swap]])
thus ?thesis
using ‹l∈labels Γ⇩A⇩O⇩D⇩V p› and ‹l'∈labels Γ⇩A⇩O⇩D⇩V p'› by auto
qed
moreover have "anycast (λm. not_Pkt m ⟶ msg_sender m = i) a"
proof -
have "opaodv i ⊨⇩A (act (recvmsg rreq_rrep_sn), other A {i} →)
onll Γ⇩A⇩O⇩D⇩V (seqll i (λ((ξ, _), a, _). anycast (λm. not_Pkt m ⟶ msg_sender m = i) a))"
by (rule ostep_invariant_weakenE [OF
open_seq_step_invariant [OF sender_ip_valid initiali_aodv,
simplified seqll_onll_swap]]) auto
thus ?thesis using or tr recv ‹l∈labels Γ⇩A⇩O⇩D⇩V p› and ‹l'∈labels Γ⇩A⇩O⇩D⇩V p'›
by - (drule(3) onll_ostep_invariantD, auto)
qed
ultimately have "anycast (msg_fresh σ) a"
by (simp_all add: anycast_def
del: msg_fresh
split: seq_action.split_asm msg.split_asm) simp_all
thus "onll Γ⇩A⇩O⇩D⇩V (λ((σ, _), a, _). anycast (msg_fresh σ) a) ((σ, p), a, (σ', p'))"
by auto
qed
lemma oreceived_rreq_rrep_nsqn_fresh_inv:
"opaodv i ⊨ (otherwith quality_increases {i} (orecvmsg msg_fresh),
other quality_increases {i} →)
onl Γ⇩A⇩O⇩D⇩V (λ(σ, l). l ∈ {PAodv-:1} ⟶ msg_fresh σ (msg (σ i)))"
proof (rule oreceived_msg_inv)
fix σ σ' m
assume *: "msg_fresh σ m"
and "other quality_increases {i} σ σ'"
from this(2) have "∀j. quality_increases (σ j) (σ' j)" ..
thus "msg_fresh σ' m" using * ..
next
fix σ m
assume "msg_fresh σ m"
thus "msg_fresh (σ(i := σ i⦇msg := m⦈)) m"
proof (cases m)
fix dests sip
assume "m = Rerr dests sip"
with ‹msg_fresh σ m› show ?thesis by auto
qed auto
qed
lemma oquality_increases_nsqn_fresh:
"opaodv i ⊨⇩A (otherwith quality_increases {i} (orecvmsg msg_fresh),
other quality_increases {i} →)
onll Γ⇩A⇩O⇩D⇩V (λ((σ, _), _, (σ', _)). ∀j. quality_increases (σ j) (σ' j))"
by (rule ostep_invariant_weakenE [OF oquality_increases]) auto
lemma oosn_rreq:
"opaodv i ⊨ (otherwith quality_increases {i} (orecvmsg msg_fresh),
other quality_increases {i} →)
onl Γ⇩A⇩O⇩D⇩V (seql i (λ(ξ, l). l ∈ {PAodv-:4, PAodv-:5} ∪ {PRreq-:n |n. True} ⟶ 1 ≤ osn ξ))"
by (rule oinvariant_weakenE [OF open_seq_invariant [OF osn_rreq initiali_aodv]])
(auto simp: seql_onl_swap)
lemma rreq_sip:
"opaodv i ⊨ (otherwith quality_increases {i} (orecvmsg msg_fresh),
other quality_increases {i} →)
onl Γ⇩A⇩O⇩D⇩V (λ(σ, l).
(l ∈ {PAodv-:4, PAodv-:5, PRreq-:0, PRreq-:2} ∧ sip (σ i) ≠ oip (σ i))
⟶ oip (σ i) ∈ kD(rt (σ (sip (σ i))))
∧ nsqn (rt (σ (sip (σ i)))) (oip (σ i)) ≥ osn (σ i)
∧ (nsqn (rt (σ (sip (σ i)))) (oip (σ i)) = osn (σ i)
⟶ (hops (σ i) ≥ the (dhops (rt (σ (sip (σ i)))) (oip (σ i)))
∨ the (flag (rt (σ (sip (σ i)))) (oip (σ i))) = inv)))"
(is "_ ⊨ (?S, ?U →) _")
proof (inv_cterms inv add: oseq_step_invariant_sterms [OF oquality_increases_nsqn_fresh
aodv_wf oaodv_trans]
onl_oinvariant_sterms [OF aodv_wf oreceived_rreq_rrep_nsqn_fresh_inv]
onl_oinvariant_sterms [OF aodv_wf oosn_rreq]
simp add: seqlsimp
simp del: One_nat_def, rule impI)
fix σ σ' p l
assume "(σ, p) ∈ oreachable (opaodv i) ?S ?U"
and "l ∈ labels Γ⇩A⇩O⇩D⇩V p"
and pre:
"(l = PAodv-:4 ∨ l = PAodv-:5 ∨ l = PRreq-:0 ∨ l = PRreq-:2) ∧ sip (σ i) ≠ oip (σ i)
⟶ oip (σ i) ∈ kD (rt (σ (sip (σ i))))
∧ osn (σ i) ≤ nsqn (rt (σ (sip (σ i)))) (oip (σ i))
∧ (nsqn (rt (σ (sip (σ i)))) (oip (σ i)) = osn (σ i)
⟶ the (dhops (rt (σ (sip (σ i)))) (oip (σ i))) ≤ hops (σ i)
∨ the (flag (rt (σ (sip (σ i)))) (oip (σ i))) = inv)"
and "other quality_increases {i} σ σ'"
and hyp: "(l=PAodv-:4 ∨ l=PAodv-:5 ∨ l=PRreq-:0 ∨ l=PRreq-:2) ∧ sip (σ' i) ≠ oip (σ' i)"
(is "?labels ∧ sip (σ' i) ≠ oip (σ' i)")
from this(4) have "σ' i = σ i" ..
with hyp have hyp': "?labels ∧ sip (σ i) ≠ oip (σ i)" by simp
show "oip (σ' i) ∈ kD (rt (σ' (sip (σ' i))))
∧ osn (σ' i) ≤ nsqn (rt (σ' (sip (σ' i)))) (oip (σ' i))
∧ (nsqn (rt (σ' (sip (σ' i)))) (oip (σ' i)) = osn (σ' i)
⟶ the (dhops (rt (σ' (sip (σ' i)))) (oip (σ' i))) ≤ hops (σ' i)
∨ the (flag (rt (σ' (sip (σ' i)))) (oip (σ' i))) = inv)"
proof (cases "sip (σ i) = i")
assume "sip (σ i) ≠ i"
from ‹other quality_increases {i} σ σ'›
have "quality_increases (σ (sip (σ i))) (σ' (sip (σ' i)))"
by (rule otherE) (clarsimp simp: ‹sip (σ i) ≠ i›)
moreover from ‹(σ, p) ∈ oreachable (opaodv i) ?S ?U› ‹l ∈ labels Γ⇩A⇩O⇩D⇩V p› and hyp
have "1 ≤ osn (σ' i)"
by (auto dest!: onl_oinvariant_weakenD [OF oosn_rreq]
simp add: seqlsimp ‹σ' i = σ i›)
moreover from ‹sip (σ i) ≠ i› hyp' and pre
have "oip (σ' i) ∈ kD (rt (σ (sip (σ i))))
∧ osn (σ' i) ≤ nsqn (rt (σ (sip (σ i)))) (oip (σ' i))
∧ (nsqn (rt (σ (sip (σ i)))) (oip (σ' i)) = osn (σ' i)
⟶ the (dhops (rt (σ (sip (σ i)))) (oip (σ' i))) ≤ hops (σ' i)
∨ the (flag (rt (σ (sip (σ i)))) (oip (σ' i))) = inv)"
by (auto simp: ‹σ' i = σ i›)
ultimately show ?thesis
by (rule quality_increases_rreq_rrep_props)
next
assume "sip (σ i) = i" thus ?thesis
using ‹σ' i = σ i› hyp and pre by auto
qed
qed (auto elim!: quality_increases_rreq_rrep_props')
lemma odsn_rrep:
"opaodv i ⊨ (otherwith quality_increases {i} (orecvmsg msg_fresh),
other quality_increases {i} →)
onl Γ⇩A⇩O⇩D⇩V (seql i (λ(ξ, l). l ∈ {PAodv-:6, PAodv-:7} ∪ {PRrep-:n|n. True} ⟶ 1 ≤ dsn ξ))"
by (rule oinvariant_weakenE [OF open_seq_invariant [OF dsn_rrep initiali_aodv]])
(auto simp: seql_onl_swap)
lemma rrep_sip:
"opaodv i ⊨ (otherwith quality_increases {i} (orecvmsg msg_fresh),
other quality_increases {i} →)
onl Γ⇩A⇩O⇩D⇩V (λ(σ, l).
(l ∈ {PAodv-:6, PAodv-:7, PRrep-:0, PRrep-:1} ∧ sip (σ i) ≠ dip (σ i))
⟶ dip (σ i) ∈ kD(rt (σ (sip (σ i))))
∧ nsqn (rt (σ (sip (σ i)))) (dip (σ i)) ≥ dsn (σ i)
∧ (nsqn (rt (σ (sip (σ i)))) (dip (σ i)) = dsn (σ i)
⟶ (hops (σ i) ≥ the (dhops (rt (σ (sip (σ i)))) (dip (σ i)))
∨ the (flag (rt (σ (sip (σ i)))) (dip (σ i))) = inv)))"
(is "_ ⊨ (?S, ?U →) _")
proof (inv_cterms inv add: oseq_step_invariant_sterms [OF oquality_increases_nsqn_fresh aodv_wf
oaodv_trans]
onl_oinvariant_sterms [OF aodv_wf oreceived_rreq_rrep_nsqn_fresh_inv]
onl_oinvariant_sterms [OF aodv_wf odsn_rrep]
simp del: One_nat_def, rule impI)
fix σ σ' p l
assume "(σ, p) ∈ oreachable (opaodv i) ?S ?U"
and "l ∈ labels Γ⇩A⇩O⇩D⇩V p"
and pre:
"(l = PAodv-:6 ∨ l = PAodv-:7 ∨ l = PRrep-:0 ∨ l = PRrep-:1) ∧ sip (σ i) ≠ dip (σ i)
⟶ dip (σ i) ∈ kD (rt (σ (sip (σ i))))
∧ dsn (σ i) ≤ nsqn (rt (σ (sip (σ i)))) (dip (σ i))
∧ (nsqn (rt (σ (sip (σ i)))) (dip (σ i)) = dsn (σ i)
⟶ the (dhops (rt (σ (sip (σ i)))) (dip (σ i))) ≤ hops (σ i)
∨ the (flag (rt (σ (sip (σ i)))) (dip (σ i))) = inv)"
and "other quality_increases {i} σ σ'"
and hyp: "(l=PAodv-:6 ∨ l=PAodv-:7 ∨ l=PRrep-:0 ∨ l=PRrep-:1) ∧ sip (σ' i) ≠ dip (σ' i)"
(is "?labels ∧ sip (σ' i) ≠ dip (σ' i)")
from this(4) have "σ' i = σ i" ..
with hyp have hyp': "?labels ∧ sip (σ i) ≠ dip (σ i)" by simp
show "dip (σ' i) ∈ kD (rt (σ' (sip (σ' i))))
∧ dsn (σ' i) ≤ nsqn (rt (σ' (sip (σ' i)))) (dip (σ' i))
∧ (nsqn (rt (σ' (sip (σ' i)))) (dip (σ' i)) = dsn (σ' i)
⟶ the (dhops (rt (σ' (sip (σ' i)))) (dip (σ' i))) ≤ hops (σ' i)
∨ the (flag (rt (σ' (sip (σ' i)))) (dip (σ' i))) = inv)"
proof (cases "sip (σ i) = i")
assume "sip (σ i) ≠ i"
from ‹other quality_increases {i} σ σ'›
have "quality_increases (σ (sip (σ i))) (σ' (sip (σ' i)))"
by (rule otherE) (clarsimp simp: ‹sip (σ i) ≠ i›)
moreover from ‹(σ, p) ∈ oreachable (opaodv i) ?S ?U› ‹l ∈ labels Γ⇩A⇩O⇩D⇩V p› and hyp
have "1 ≤ dsn (σ' i)"
by (auto dest!: onl_oinvariant_weakenD [OF odsn_rrep]
simp add: seqlsimp ‹σ' i = σ i›)
moreover from ‹sip (σ i) ≠ i› hyp' and pre
have "dip (σ' i) ∈ kD (rt (σ (sip (σ i))))
∧ dsn (σ' i) ≤ nsqn (rt (σ (sip (σ i)))) (dip (σ' i))
∧ (nsqn (rt (σ (sip (σ i)))) (dip (σ' i)) = dsn (σ' i)
⟶ the (dhops (rt (σ (sip (σ i)))) (dip (σ' i))) ≤ hops (σ' i)
∨ the (flag (rt (σ (sip (σ i)))) (dip (σ' i))) = inv)"
by (auto simp: ‹σ' i = σ i›)
ultimately show ?thesis
by (rule quality_increases_rreq_rrep_props)
next
assume "sip (σ i) = i" thus ?thesis
using ‹σ' i = σ i› hyp and pre by auto
qed
qed (auto simp add: seqlsimp elim!: quality_increases_rreq_rrep_props')
lemma rerr_sip:
"opaodv i ⊨ (otherwith quality_increases {i} (orecvmsg msg_fresh),
other quality_increases {i} →)
onl Γ⇩A⇩O⇩D⇩V (λ(σ, l).
l ∈ {PAodv-:8, PAodv-:9, PRerr-:0, PRerr-:1}
⟶ (∀ripc∈dom(dests (σ i)). ripc∈kD(rt (σ (sip (σ i)))) ∧
the (dests (σ i) ripc) - 1 ≤ nsqn (rt (σ (sip (σ i)))) ripc))"
(is "_ ⊨ (?S, ?U →) _")
proof -
{ fix dests rip sip rsn and σ σ' :: "ip ⇒ state"
assume qinc: "∀j. quality_increases (σ j) (σ' j)"
and *: "∀rip∈dom dests. rip ∈ kD (rt (σ sip))
∧ the (dests rip) - 1 ≤ nsqn (rt (σ sip)) rip"
and "dests rip = Some rsn"
from this(3) have "rip∈dom dests" by auto
with * and ‹dests rip = Some rsn› have "rip∈kD(rt (σ sip))"
and "rsn - 1 ≤ nsqn (rt (σ sip)) rip"
by (auto dest!: bspec)
from qinc have "quality_increases (σ sip) (σ' sip)" ..
have "rip ∈ kD(rt (σ' sip)) ∧ rsn - 1 ≤ nsqn (rt (σ' sip)) rip"
proof
from ‹rip∈kD(rt (σ sip))› and ‹quality_increases (σ sip) (σ' sip)›
show "rip ∈ kD(rt (σ' sip))" ..
next
from ‹rip∈kD(rt (σ sip))› and ‹quality_increases (σ sip) (σ' sip)›
have "nsqn (rt (σ sip)) rip ≤ nsqn (rt (σ' sip)) rip" ..
with ‹rsn - 1 ≤ nsqn (rt (σ sip)) rip› show "rsn - 1 ≤ nsqn (rt (σ' sip)) rip"
by (rule le_trans)
qed
} note partial = this
show ?thesis
by (inv_cterms inv add: oseq_step_invariant_sterms [OF oquality_increases_nsqn_fresh aodv_wf
oaodv_trans]
onl_oinvariant_sterms [OF aodv_wf oreceived_rreq_rrep_nsqn_fresh_inv]
other_quality_increases other_localD
simp del: One_nat_def, intro conjI)
(clarsimp simp del: One_nat_def split: if_split_asm option.split_asm, erule(2) partial)+
qed
lemma prerr_guard: "paodv i ⊫
onl Γ⇩A⇩O⇩D⇩V (λ(ξ, l). (l = PRerr-:1
⟶ (∀ip∈dom(dests ξ). ip∈vD(rt ξ)
∧ the (nhop (rt ξ) ip) = sip ξ
∧ sqn (rt ξ) ip < the (dests ξ ip))))"
by (inv_cterms) (clarsimp split: option.split_asm if_split_asm)
lemmas oaddpreRT_welldefined =
open_seq_invariant [OF addpreRT_welldefined initiali_aodv oaodv_trans aodv_trans,
simplified seql_onl_swap,
THEN oinvariant_anyact]
lemmas odests_vD_inc_sqn =
open_seq_invariant [OF dests_vD_inc_sqn initiali_aodv oaodv_trans aodv_trans,
simplified seql_onl_swap,
THEN oinvariant_anyact]
lemmas oprerr_guard =
open_seq_invariant [OF prerr_guard initiali_aodv oaodv_trans aodv_trans,
simplified seql_onl_swap,
THEN oinvariant_anyact]
text ‹Proposition 7.28›
lemma seq_compare_next_hop':
"opaodv i ⊨ (otherwith quality_increases {i} (orecvmsg msg_fresh),
other quality_increases {i} →) onl Γ⇩A⇩O⇩D⇩V (λ(σ, _).
∀dip. let nhip = the (nhop (rt (σ i)) dip)
in dip ∈ kD(rt (σ i)) ∧ nhip ≠ dip ⟶
dip ∈ kD(rt (σ nhip)) ∧ nsqn (rt (σ i)) dip ≤ nsqn (rt (σ nhip)) dip)"
(is "_ ⊨ (?S, ?U →) _")
proof -
{ fix nhop and σ σ' :: "ip ⇒ state"
assume pre: "∀dip∈kD(rt (σ i)). nhop dip ≠ dip ⟶
dip∈kD(rt (σ (nhop dip))) ∧ nsqn (rt (σ i)) dip ≤ nsqn (rt (σ (nhop dip))) dip"
and qinc: "∀j. quality_increases (σ j) (σ' j)"
have "∀dip∈kD(rt (σ i)). nhop dip ≠ dip ⟶
dip∈kD(rt (σ' (nhop dip))) ∧ nsqn (rt (σ i)) dip ≤ nsqn (rt (σ' (nhop dip))) dip"
proof (intro ballI impI)
fix dip
assume "dip∈kD(rt (σ i))"
and "nhop dip ≠ dip"
with pre have "dip∈kD(rt (σ (nhop dip)))"
and "nsqn (rt (σ i)) dip ≤ nsqn (rt (σ (nhop dip))) dip"
by auto
from qinc have qinc_nhop: "quality_increases (σ (nhop dip)) (σ' (nhop dip))" ..
with ‹dip∈kD(rt (σ (nhop dip)))› have "dip∈kD (rt (σ' (nhop dip)))" ..
moreover have "nsqn (rt (σ i)) dip ≤ nsqn (rt (σ' (nhop dip))) dip"
proof -
from ‹dip∈kD(rt (σ (nhop dip)))› qinc_nhop
have "nsqn (rt (σ (nhop dip))) dip ≤ nsqn (rt (σ' (nhop dip))) dip" ..
with ‹nsqn (rt (σ i)) dip ≤ nsqn (rt (σ (nhop dip))) dip› show ?thesis
by simp
qed
ultimately show "dip∈kD(rt (σ' (nhop dip)))
∧ nsqn (rt (σ i)) dip ≤ nsqn (rt (σ' (nhop dip))) dip" ..
qed
} note basic = this
{ fix nhop and σ σ' :: "ip ⇒ state"
assume pre: "∀dip∈kD(rt (σ i)). nhop dip ≠ dip ⟶ dip∈kD(rt (σ (nhop dip)))
∧ nsqn (rt (σ i)) dip ≤ nsqn (rt (σ (nhop dip))) dip"
and ndest: "∀ripc∈dom (dests (σ i)). ripc ∈ kD (rt (σ (sip (σ i))))
∧ the (dests (σ i) ripc) - 1 ≤ nsqn (rt (σ (sip (σ i)))) ripc"
and issip: "∀ip∈dom (dests (σ i)). nhop ip = sip (σ i)"
and qinc: "∀j. quality_increases (σ j) (σ' j)"
have "∀dip∈kD(rt (σ i)). nhop dip ≠ dip ⟶ dip ∈ kD (rt (σ' (nhop dip)))
∧ nsqn (invalidate (rt (σ i)) (dests (σ i))) dip ≤ nsqn (rt (σ' (nhop dip))) dip"
proof (intro ballI impI)
fix dip
assume "dip∈kD(rt (σ i))"
and "nhop dip ≠ dip"
with pre and qinc have "dip∈kD(rt (σ' (nhop dip)))"
and "nsqn (rt (σ i)) dip ≤ nsqn (rt (σ' (nhop dip))) dip"
by (auto dest!: basic)
have "nsqn (invalidate (rt (σ i)) (dests (σ i))) dip ≤ nsqn (rt (σ' (nhop dip))) dip"
proof (cases "dip∈dom (dests (σ i))")
assume "dip∈dom (dests (σ i))"
with ‹dip∈kD(rt (σ i))› obtain dsn where "dests (σ i) dip = Some dsn"
by auto
with ‹dip∈kD(rt (σ i))› have "nsqn (invalidate (rt (σ i)) (dests (σ i))) dip = dsn - 1"
by (rule nsqn_invalidate_eq)
moreover have "dsn - 1 ≤ nsqn (rt (σ' (nhop dip))) dip"
proof -
from ‹dests (σ i) dip = Some dsn› have "the (dests (σ i) dip) = dsn" by simp
with ndest and ‹dip∈dom (dests (σ i))› have "dip ∈ kD (rt (σ (sip (σ i))))"
"dsn - 1 ≤ nsqn (rt (σ (sip (σ i)))) dip"
by auto
moreover from issip and ‹dip∈dom (dests (σ i))› have "nhop dip = sip (σ i)" ..
ultimately have "dip ∈ kD (rt (σ (nhop dip)))"
and "dsn - 1 ≤ nsqn (rt (σ (nhop dip))) dip" by auto
with qinc show "dsn - 1 ≤ nsqn (rt (σ' (nhop dip))) dip"
by simp (metis kD_nsqn_quality_increases_trans)
qed
ultimately show ?thesis by simp
next
assume "dip ∉ dom (dests (σ i))"
with ‹dip∈kD(rt (σ i))›
have "nsqn (invalidate (rt (σ i)) (dests (σ i))) dip = nsqn (rt (σ i)) dip"
by (rule nsqn_invalidate_other)
with ‹nsqn (rt (σ i)) dip ≤ nsqn (rt (σ' (nhop dip))) dip› show ?thesis by simp
qed
with ‹dip∈kD(rt (σ' (nhop dip)))›
show "dip ∈ kD (rt (σ' (nhop dip)))
∧ nsqn (invalidate (rt (σ i)) (dests (σ i))) dip ≤ nsqn (rt (σ' (nhop dip))) dip" ..
qed
} note basic_prerr = this
{ fix σ σ' :: "ip ⇒ state"
assume a1: "∀dip∈kD(rt (σ i)). the (nhop (rt (σ i)) dip) ≠ dip
⟶ dip∈kD(rt (σ (the (nhop (rt (σ i)) dip))))
∧ nsqn (rt (σ i)) dip ≤ nsqn (rt (σ (the (nhop (rt (σ i)) dip)))) dip"
and a2: "∀j. quality_increases (σ j) (σ' j)"
have "∀dip∈kD(rt (σ i)).
the (nhop (update (rt (σ i)) (sip (σ i)) (0, unk, val, Suc 0, sip (σ i), {})) dip) ≠ dip ⟶
dip∈kD(rt (σ' (the (nhop (update (rt (σ i)) (sip (σ i))
(0, unk, val, Suc 0, sip (σ i), {}))
dip)))) ∧
nsqn (update (rt (σ i)) (sip (σ i)) (0, unk, val, Suc 0, sip (σ i), {})) dip
≤ nsqn (rt (σ' (the (nhop (update (rt (σ i)) (sip (σ i))
(0, unk, val, Suc 0, sip (σ i), {}))
dip))))
dip" (is "∀dip∈kD(rt (σ i)). ?P dip")
proof
fix dip
assume "dip∈kD(rt (σ i))"
with a1 and a2
have "the (nhop (rt (σ i)) dip) ≠ dip ⟶ dip∈kD(rt (σ' (the (nhop (rt (σ i)) dip))))
∧ nsqn (rt (σ i)) dip ≤ nsqn (rt (σ' (the (nhop (rt (σ i)) dip)))) dip"
by - (drule(1) basic, auto)
thus "?P dip" by (cases "dip = sip (σ i)") auto
qed
} note nhop_update_sip = this
{ fix σ σ' oip sip osn hops
assume pre: "∀dip∈kD (rt (σ i)). the (nhop (rt (σ i)) dip) ≠ dip
⟶ dip∈kD(rt (σ (the (nhop (rt (σ i)) dip))))
∧ nsqn (rt (σ i)) dip ≤ nsqn (rt (σ (the (nhop (rt (σ i)) dip)))) dip"
and qinc: "∀j. quality_increases (σ j) (σ' j)"
and *: "sip ≠ oip ⟶ oip∈kD(rt (σ sip))
∧ osn ≤ nsqn (rt (σ sip)) oip
∧ (nsqn (rt (σ sip)) oip = osn
⟶ the (dhops (rt (σ sip)) oip) ≤ hops
∨ the (flag (rt (σ sip)) oip) = inv)"
from pre and qinc
have pre': "∀dip∈kD (rt (σ i)). the (nhop (rt (σ i)) dip) ≠ dip
⟶ dip∈kD(rt (σ' (the (nhop (rt (σ i)) dip))))
∧ nsqn (rt (σ i)) dip ≤ nsqn (rt (σ' (the (nhop (rt (σ i)) dip)))) dip"
by (rule basic)
have "(the (nhop (update (rt (σ i)) oip (osn, kno, val, Suc hops, sip, {})) oip) ≠ oip
⟶ oip∈kD(rt (σ' (the (nhop (update (rt (σ i)) oip
(osn, kno, val, Suc hops, sip, {})) oip))))
∧ nsqn (update (rt (σ i)) oip (osn, kno, val, Suc hops, sip, {})) oip
≤ nsqn (rt (σ' (the (nhop (update (rt (σ i)) oip
(osn, kno, val, Suc hops, sip, {})) oip)))) oip)"
(is "?nhop_not_oip ⟶ ?oip_in_kD ∧ ?nsqn_le_nsqn")
proof (rule, split update_rt_split_asm)
assume "rt (σ i) = update (rt (σ i)) oip (osn, kno, val, Suc hops, sip, {})"
and "the (nhop (rt (σ i)) oip) ≠ oip"
with pre' show "?oip_in_kD ∧ ?nsqn_le_nsqn" by auto
next
assume rtnot: "rt (σ i) ≠ update (rt (σ i)) oip (osn, kno, val, Suc hops, sip, {})"
and notoip: ?nhop_not_oip
with * qinc have ?oip_in_kD
by (clarsimp elim!: kD_quality_increases)
moreover with * pre qinc rtnot notoip have ?nsqn_le_nsqn
by simp (metis kD_nsqn_quality_increases_trans)
ultimately show "?oip_in_kD ∧ ?nsqn_le_nsqn" ..
qed
} note update1 = this
{ fix σ σ' oip sip osn hops
assume pre: "∀dip∈kD (rt (σ i)). the (nhop (rt (σ i)) dip) ≠ dip
⟶ dip∈kD(rt (σ (the (nhop (rt (σ i)) dip))))
∧ nsqn (rt (σ i)) dip ≤ nsqn (rt (σ (the (nhop (rt (σ i)) dip)))) dip"
and qinc: "∀j. quality_increases (σ j) (σ' j)"
and *: "sip ≠ oip ⟶ oip∈kD(rt (σ sip))
∧ osn ≤ nsqn (rt (σ sip)) oip
∧ (nsqn (rt (σ sip)) oip = osn
⟶ the (dhops (rt (σ sip)) oip) ≤ hops
∨ the (flag (rt (σ sip)) oip) = inv)"
from pre and qinc
have pre': "∀dip∈kD (rt (σ i)). the (nhop (rt (σ i)) dip) ≠ dip
⟶ dip∈kD(rt (σ' (the (nhop (rt (σ i)) dip))))
∧ nsqn (rt (σ i)) dip ≤ nsqn (rt (σ' (the (nhop (rt (σ i)) dip)))) dip"
by (rule basic)
have "∀dip∈kD(rt (σ i)).
the (nhop (update (rt (σ i)) oip (osn, kno, val, Suc hops, sip, {})) dip) ≠ dip
⟶ dip∈kD(rt (σ' (the (nhop (update (rt (σ i)) oip
(osn, kno, val, Suc hops, sip, {})) dip))))
∧ nsqn (update (rt (σ i)) oip (osn, kno, val, Suc hops, sip, {})) dip
≤ nsqn (rt (σ' (the (nhop (update (rt (σ i)) oip
(osn, kno, val, Suc hops, sip, {})) dip)))) dip"
(is "∀dip∈kD(rt (σ i)). _ ⟶ ?dip_in_kD dip ∧ ?nsqn_le_nsqn dip")
proof (intro ballI impI, split update_rt_split_asm)
fix dip
assume "dip∈kD(rt (σ i))"
and "the (nhop (rt (σ i)) dip) ≠ dip"
and "rt (σ i) = update (rt (σ i)) oip (osn, kno, val, Suc hops, sip, {})"
with pre' show "?dip_in_kD dip ∧ ?nsqn_le_nsqn dip" by simp
next
fix dip
assume "dip∈kD(rt (σ i))"
and notdip: "the (nhop (update (rt (σ i)) oip
(osn, kno, val, Suc hops, sip, {})) dip) ≠ dip"
and rtnot: "rt (σ i) ≠ update (rt (σ i)) oip (osn, kno, val, Suc hops, sip, {})"
show "?dip_in_kD dip ∧ ?nsqn_le_nsqn dip"
proof (cases "dip = oip")
assume "dip ≠ oip"
with pre' ‹dip∈kD(rt (σ i))› notdip
show ?thesis by clarsimp
next
assume "dip = oip"
with rtnot qinc ‹dip∈kD(rt (σ i))› notdip *
have "?dip_in_kD dip"
by simp (metis kD_quality_increases)
moreover from ‹dip = oip› rtnot qinc ‹dip∈kD(rt (σ i))› notdip *
have "?nsqn_le_nsqn dip" by simp (metis kD_nsqn_quality_increases_trans)
ultimately show ?thesis ..
qed
qed
} note update2 = this
have "opaodv i ⊨ (?S, ?U →) onl Γ⇩A⇩O⇩D⇩V (λ(σ, _).
∀dip ∈ kD(rt (σ i)). the (nhop (rt (σ i)) dip) ≠ dip
⟶ dip ∈ kD(rt (σ (the (nhop (rt (σ i)) dip))))
∧ nsqn (rt (σ i)) dip ≤ nsqn (rt (σ (the (nhop (rt (σ i)) dip)))) dip)"
by (inv_cterms inv add: oseq_step_invariant_sterms [OF oquality_increases_nsqn_fresh aodv_wf
oaodv_trans]
onl_oinvariant_sterms [OF aodv_wf oaddpreRT_welldefined]
onl_oinvariant_sterms [OF aodv_wf odests_vD_inc_sqn]
onl_oinvariant_sterms [OF aodv_wf oprerr_guard]
onl_oinvariant_sterms [OF aodv_wf rreq_sip]
onl_oinvariant_sterms [OF aodv_wf rrep_sip]
onl_oinvariant_sterms [OF aodv_wf rerr_sip]
other_quality_increases
other_localD
solve: basic basic_prerr
simp add: seqlsimp nsqn_invalidate nhop_update_sip
simp del: One_nat_def)
(rule conjI, erule(2) update1, erule(2) update2)+
thus ?thesis unfolding Let_def by auto
qed
text ‹Proposition 7.30›
lemmas okD_unk_or_atleast_one =
open_seq_invariant [OF kD_unk_or_atleast_one initiali_aodv,
simplified seql_onl_swap]
lemmas ozero_seq_unk_hops_one =
open_seq_invariant [OF zero_seq_unk_hops_one initiali_aodv,
simplified seql_onl_swap]
lemma oreachable_fresh_okD_unk_or_atleast_one:
fixes dip
assumes "(σ, p) ∈ oreachable (opaodv i)
(otherwith ((=)) {i} (orecvmsg (λσ m. msg_fresh σ m
∧ msg_zhops m)))
(other quality_increases {i})"
and "dip∈kD(rt (σ i))"
shows "π⇩3(the (rt (σ i) dip)) = unk ∨ 1 ≤ π⇩2(the (rt (σ i) dip))"
(is "?P dip")
proof -
have "∃l. l∈labels Γ⇩A⇩O⇩D⇩V p" by (metis aodv_ex_label)
with assms(1) have "∀dip∈kD (rt (σ i)). ?P dip"
by - (drule oinvariant_weakenD [OF okD_unk_or_atleast_one [OF oaodv_trans aodv_trans]],
auto dest!: otherwith_actionD onlD simp: seqlsimp)
with ‹dip∈kD(rt (σ i))› show ?thesis by simp
qed
lemma oreachable_fresh_ozero_seq_unk_hops_one:
fixes dip
assumes "(σ, p) ∈ oreachable (opaodv i)
(otherwith ((=)) {i} (orecvmsg (λσ m. msg_fresh σ m
∧ msg_zhops m)))
(other quality_increases {i})"
and "dip∈kD(rt (σ i))"
shows "sqn (rt (σ i)) dip = 0 ⟶
sqnf (rt (σ i)) dip = unk
∧ the (dhops (rt (σ i)) dip) = 1
∧ the (nhop (rt (σ i)) dip) = dip"
(is "?P dip")
proof -
have "∃l. l∈labels Γ⇩A⇩O⇩D⇩V p" by (metis aodv_ex_label)
with assms(1) have "∀dip∈kD (rt (σ i)). ?P dip"
by - (drule oinvariant_weakenD [OF ozero_seq_unk_hops_one [OF oaodv_trans aodv_trans]],
auto dest!: onlD otherwith_actionD simp: seqlsimp)
with ‹dip∈kD(rt (σ i))› show ?thesis by simp
qed
lemma seq_nhop_quality_increases':
shows "opaodv i ⊨ (otherwith ((=)) {i}
(orecvmsg (λσ m. msg_fresh σ m ∧ msg_zhops m)),
other quality_increases {i} →)
onl Γ⇩A⇩O⇩D⇩V (λ(σ, _). ∀dip. let nhip = the (nhop (rt (σ i)) dip)
in dip ∈ vD (rt (σ i)) ∩ vD (rt (σ nhip))
∧ nhip ≠ dip
⟶ (rt (σ i)) ⊏⇘dip⇙ (rt (σ nhip)))"
(is "_ ⊨ (?S i, _ →) _")
proof -
have weaken:
"⋀p I Q R P. p ⊨ (otherwith quality_increases I (orecvmsg Q), other quality_increases I →) P
⟹ p ⊨ (otherwith ((=)) I (orecvmsg (λσ m. Q σ m ∧ R σ m)), other quality_increases I →) P"
by auto
{
fix i a and σ σ' :: "ip ⇒ state"
assume a1: "∀dip. dip∈vD(rt (σ i))
∧ dip∈vD(rt (σ (the (nhop (rt (σ i)) dip))))
∧ (the (nhop (rt (σ i)) dip)) ≠ dip
⟶ rt (σ i) ⊏⇘dip⇙ rt (σ (the (nhop (rt (σ i)) dip)))"
and ow: "?S i σ σ' a"
have "∀dip. dip∈vD(rt (σ i))
∧ dip∈vD (rt (σ' (the (nhop (rt (σ i)) dip))))
∧ (the (nhop (rt (σ i)) dip)) ≠ dip
⟶ rt (σ i) ⊏⇘dip⇙ rt (σ' (the (nhop (rt (σ i)) dip)))"
proof clarify
fix dip
assume a2: "dip∈vD(rt (σ i))"
and a3: "dip∈vD (rt (σ' (the (nhop (rt (σ i)) dip))))"
and a4: "(the (nhop (rt (σ i)) dip)) ≠ dip"
from ow have "∀j. j ≠ i ⟶ σ j = σ' j" by auto
show "rt (σ i) ⊏⇘dip⇙ rt (σ' (the (nhop (rt (σ i)) dip)))"
proof (cases "(the (nhop (rt (σ i)) dip)) = i")
assume "(the (nhop (rt (σ i)) dip)) = i"
with ‹dip ∈ vD(rt (σ i))› have "dip ∈ vD(rt (σ (the (nhop (rt (σ i)) dip))))" by simp
with a1 a2 a4 have "rt (σ i) ⊏⇘dip⇙ rt (σ (the (nhop (rt (σ i)) dip)))" by simp
with ‹(the (nhop (rt (σ i)) dip)) = i› have "rt (σ i) ⊏⇘dip⇙ rt (σ i)" by simp
hence False by simp
thus ?thesis ..
next
assume "(the (nhop (rt (σ i)) dip)) ≠ i"
with ‹∀j. j ≠ i ⟶ σ j = σ' j›
have *: "σ (the (nhop (rt (σ i)) dip)) = σ' (the (nhop (rt (σ i)) dip))" by simp
with ‹dip∈vD (rt (σ' (the (nhop (rt (σ i)) dip))))›
have "dip∈vD (rt (σ (the (nhop (rt (σ i)) dip))))" by simp
with a1 a2 a4 have "rt (σ i) ⊏⇘dip⇙ rt (σ (the (nhop (rt (σ i)) dip)))" by simp
with * show ?thesis by simp
qed
qed
} note basic = this
{ fix σ σ' a dip sip i
assume a1: "∀dip. dip∈vD(rt (σ i))
∧ dip∈vD(rt (σ (the (nhop (rt (σ i)) dip))))
∧ the (nhop (rt (σ i)) dip) ≠ dip
⟶ rt (σ i) ⊏⇘dip⇙ rt (σ (the (nhop (rt (σ i)) dip)))"
and ow: "?S i σ σ' a"
have "∀dip. dip∈vD(update (rt (σ i)) sip (0, unk, val, Suc 0, sip, {}))
∧ dip∈vD(rt (σ' (the (nhop (update (rt (σ i)) sip (0, unk, val, Suc 0, sip, {})) dip))))
∧ the (nhop (update (rt (σ i)) sip (0, unk, val, Suc 0, sip, {})) dip) ≠ dip
⟶ update (rt (σ i)) sip (0, unk, val, Suc 0, sip, {})
⊏⇘dip⇙ rt (σ' (the (nhop (update (rt (σ i)) sip (0, unk, val, Suc 0, sip, {})) dip)))"
proof clarify
fix dip
assume a2: "dip∈vD (update (rt (σ i)) sip (0, unk, val, Suc 0, sip, {}))"
and a3: "dip∈vD(rt (σ' (the (nhop
(update (rt (σ i)) sip (0, unk, val, Suc 0, sip, {})) dip))))"
and a4: "the (nhop (update (rt (σ i)) sip (0, unk, val, Suc 0, sip, {})) dip) ≠ dip"
show "update (rt (σ i)) sip (0, unk, val, Suc 0, sip, {})
⊏⇘dip⇙ rt (σ' (the (nhop (update (rt (σ i)) sip (0, unk, val, Suc 0, sip, {})) dip)))"
proof (cases "dip = sip")
assume "dip = sip"
with ‹the (nhop (update (rt (σ i)) sip (0, unk, val, Suc 0, sip, {})) dip) ≠ dip›
have False by simp
thus ?thesis ..
next
assume [simp]: "dip ≠ sip"
from a2 have "dip∈vD(rt (σ i)) ∨ dip = sip"
by (rule vD_update_val)
with ‹dip ≠ sip› have "dip∈vD(rt (σ i))" by simp
moreover from a3 have "dip∈vD(rt (σ' (the (nhop (rt (σ i)) dip))))" by simp
moreover from a4 have "the (nhop (rt (σ i)) dip) ≠ dip" by simp
ultimately have "rt (σ i) ⊏⇘dip⇙ rt (σ' (the (nhop (rt (σ i)) dip)))"
using a1 ow by - (drule(1) basic, simp)
with ‹dip ≠ sip› show ?thesis
by - (erule rt_strictly_fresher_update_other, simp)
qed
qed
} note update_0_unk = this
{ fix σ a σ' nhop
assume pre: "∀dip. dip∈vD(rt (σ i)) ∧ dip∈vD(rt (σ (nhop dip))) ∧ nhop dip ≠ dip
⟶ rt (σ i) ⊏⇘dip⇙ rt (σ (nhop dip))"
and ow: "?S i σ σ' a"
have "∀dip. dip ∈ vD (invalidate (rt (σ i)) (dests (σ i)))
∧ dip ∈ vD (rt (σ' (nhop dip))) ∧ nhop dip ≠ dip
⟶ rt (σ i) ⊏⇘dip⇙ rt (σ' (nhop dip))"
proof clarify
fix dip
assume "dip∈vD(invalidate (rt (σ i)) (dests (σ i)))"
and "dip∈vD(rt (σ' (nhop dip)))"
and "nhop dip ≠ dip"
from this(1) have "dip∈vD (rt (σ i))"
by (clarsimp dest!: vD_invalidate_vD_not_dests)
moreover from ow have "∀j. j ≠ i ⟶ σ j = σ' j" by auto
ultimately have "rt (σ i) ⊏⇘dip⇙ rt (σ (nhop dip))"
using pre ‹dip ∈ vD (rt (σ' (nhop dip)))› ‹nhop dip ≠ dip›
by metis
with ‹∀j. j ≠ i ⟶ σ j = σ' j› show "rt (σ i) ⊏⇘dip⇙ rt (σ' (nhop dip))"
by (metis rt_strictly_fresher_irefl)
qed
} note invalidate = this
{ fix σ a σ' dip oip osn sip hops i
assume pre: "∀dip. dip ∈ vD (rt (σ i))
∧ dip ∈ vD (rt (σ (the (nhop (rt (σ i)) dip))))
∧ the (nhop (rt (σ i)) dip) ≠ dip
⟶ rt (σ i) ⊏⇘dip⇙ rt (σ (the (nhop (rt (σ i)) dip)))"
and ow: "?S i σ σ' a"
and "Suc 0 ≤ osn"
and a6: "sip ≠ oip ⟶ oip ∈ kD (rt (σ sip))
∧ osn ≤ nsqn (rt (σ sip)) oip
∧ (nsqn (rt (σ sip)) oip = osn
⟶ the (dhops (rt (σ sip)) oip) ≤ hops
∨ the (flag (rt (σ sip)) oip) = inv)"
and after: "σ' i = σ i⦇rt := update (rt (σ i)) oip (osn, kno, val, Suc hops, sip, {})⦈"
have "∀dip. dip ∈ vD (update (rt (σ i)) oip (osn, kno, val, Suc hops, sip, {}))
∧ dip ∈ vD (rt (σ' (the (nhop (update (rt (σ i)) oip
(osn, kno, val, Suc hops, sip, {})) dip))))
∧ the (nhop (update (rt (σ i)) oip (osn, kno, val, Suc hops, sip, {})) dip) ≠ dip
⟶ update (rt (σ i)) oip (osn, kno, val, Suc hops, sip, {})
⊏⇘dip⇙
rt (σ' (the (nhop (update (rt (σ i)) oip (osn, kno, val, Suc hops, sip, {})) dip)))"
proof clarify
fix dip
assume a2: "dip∈vD(update (rt (σ i)) oip (osn, kno, val, Suc (hops), sip, {}))"
and a3: "dip∈vD(rt (σ' (the (nhop (update (rt (σ i)) oip
(osn, kno, val, Suc hops, sip, {})) dip))))"
and a4: "the (nhop (update (rt (σ i)) oip (osn, kno, val, Suc hops, sip, {})) dip) ≠ dip"
from ow have a5: "∀j. j ≠ i ⟶ σ j = σ' j" by auto
show "update (rt (σ i)) oip (osn, kno, val, Suc hops, sip, {})
⊏⇘dip⇙
rt (σ' (the (nhop (update (rt (σ i)) oip (osn, kno, val, Suc hops, sip, {})) dip)))"
(is "?rt1 ⊏⇘dip⇙ ?rt2 dip")
proof (cases "?rt1 = rt (σ i)")
assume nochange [simp]:
"update (rt (σ i)) oip (osn, kno, val, Suc hops, sip, {}) = rt (σ i)"
from after have "σ' i = σ i" by simp
with a5 have "∀j. σ j = σ' j" by metis
from a2 have "dip∈vD (rt (σ i))" by simp
moreover from a3 have "dip∈vD(rt (σ (the (nhop (rt (σ i)) dip))))"
using nochange and ‹∀j. σ j = σ' j› by clarsimp
moreover from a4 have "the (nhop (rt (σ i)) dip) ≠ dip" by simp
ultimately have "rt (σ i) ⊏⇘dip⇙ rt (σ (the (nhop (rt (σ i)) dip)))"
using pre by simp
hence "rt (σ i) ⊏⇘dip⇙ rt (σ' (the (nhop (rt (σ i)) dip)))"
using ‹∀j. σ j = σ' j› by simp
thus "?thesis" by simp
next
assume change: "?rt1 ≠ rt (σ i)"
from after a2 have "dip∈kD(rt (σ' i))" by auto
show ?thesis
proof (cases "dip = oip")
assume "dip ≠ oip"
with a2 have "dip∈vD (rt (σ i))" by auto
moreover with a3 a5 after and ‹dip ≠ oip›
have "dip∈vD(rt (σ (the (nhop (rt (σ i)) dip))))"
by simp metis
moreover from a4 and ‹dip ≠ oip› have "the (nhop (rt (σ i)) dip) ≠ dip" by simp
ultimately have "rt (σ i) ⊏⇘dip⇙ rt (σ (the (nhop (rt (σ i)) dip)))"
using pre by simp
with after and a5 and ‹dip ≠ oip› show ?thesis
by simp (metis rt_strictly_fresher_update_other
rt_strictly_fresher_irefl)
next
assume "dip = oip"
with a4 and change have "sip ≠ oip" by simp
with a6 have "oip∈kD(rt (σ sip))"
and "osn ≤ nsqn (rt (σ sip)) oip" by auto
from a3 change ‹dip = oip› have "oip∈vD(rt (σ' sip))" by simp
hence "the (flag (rt (σ' sip)) oip) = val" by simp
from ‹oip∈kD(rt (σ sip))›
have "osn < nsqn (rt (σ' sip)) oip ∨ (osn = nsqn (rt (σ' sip)) oip
∧ the (dhops (rt (σ' sip)) oip) ≤ hops)"
proof
assume "oip∈vD(rt (σ sip))"
hence "the (flag (rt (σ sip)) oip) = val" by simp
with a6 ‹sip ≠ oip› have "nsqn (rt (σ sip)) oip = osn ⟶
the (dhops (rt (σ sip)) oip) ≤ hops"
by simp
show ?thesis
proof (cases "sip = i")
assume "sip ≠ i"
with a5 have "σ sip = σ' sip" by simp
with ‹osn ≤ nsqn (rt (σ sip)) oip›
and ‹nsqn (rt (σ sip)) oip = osn ⟶ the (dhops (rt (σ sip)) oip) ≤ hops›
show ?thesis by auto
next
assume [simp]: "sip = i"
have "?rt1 = rt (σ i)"
proof (rule update_cases_kD, simp_all)
from ‹Suc 0 ≤ osn› show "0 < osn" by simp
next
from ‹oip∈kD(rt (σ sip))› and ‹sip = i› show "oip∈kD(rt (σ i))"
by simp
next
assume "sqn (rt (σ i)) oip < osn"
also from ‹osn ≤ nsqn (rt (σ sip)) oip›
have "... ≤ nsqn (rt (σ i)) oip" by simp
also have "... ≤ sqn (rt (σ i)) oip"
by (rule nsqn_sqn)
finally have "sqn (rt (σ i)) oip < sqn (rt (σ i)) oip" .
hence False by simp
thus "(λa. if a = oip
then Some (osn, kno, val, Suc hops, i, π⇩7 (the (rt (σ i) oip)))
else rt (σ i) a) = rt (σ i)" ..
next
assume "sqn (rt (σ i)) oip = osn"
and "Suc hops < the (dhops (rt (σ i)) oip)"
from this(1) and ‹oip ∈ vD (rt (σ sip))› have "nsqn (rt (σ i)) oip = osn"
by simp
with ‹nsqn (rt (σ sip)) oip = osn ⟶ the (dhops (rt (σ sip)) oip) ≤ hops›
have "the (dhops (rt (σ i)) oip) ≤ hops" by simp
with ‹Suc hops < the (dhops (rt (σ i)) oip)› have False by simp
thus "(λa. if a = oip
then Some (osn, kno, val, Suc hops, i, π⇩7 (the (rt (σ i) oip)))
else rt (σ i) a) = rt (σ i)" ..
next
assume "the (flag (rt (σ i)) oip) = inv"
with ‹the (flag (rt (σ sip)) oip) = val› have False by simp
thus "(λa. if a = oip
then Some (osn, kno, val, Suc hops, i, π⇩7 (the (rt (σ i) oip)))
else rt (σ i) a) = rt (σ i)" ..
next
from ‹oip∈kD(rt (σ sip))›
show "(λa. if a = oip then Some (the (rt (σ i) oip)) else rt (σ i) a) = rt (σ i)"
by (auto dest!: kD_Some)
qed
with change have False ..
thus ?thesis ..
qed
next
assume "oip∈iD(rt (σ sip))"
with ‹the (flag (rt (σ' sip)) oip) = val› and a5 have "sip = i"
by (metis f.distinct(1) iD_flag_is_inv)
from ‹oip∈iD(rt (σ sip))› have "the (flag (rt (σ sip)) oip) = inv" by auto
with ‹sip = i› ‹Suc 0 ≤ osn› change after ‹oip∈kD(rt (σ sip))›
have "nsqn (rt (σ sip)) oip < nsqn (rt (σ' sip)) oip"
unfolding update_def
by (clarsimp split: option.split_asm if_split_asm)
(auto simp: sqn_def)
with ‹osn ≤ nsqn (rt (σ sip)) oip› have "osn < nsqn (rt (σ' sip)) oip"
by simp
thus ?thesis ..
qed
thus ?thesis
proof
assume osnlt: "osn < nsqn (rt (σ' sip)) oip"
from ‹dip∈kD(rt (σ' i))› and ‹dip = oip› have "dip ∈ kD (?rt1)" by simp
moreover from a3 have "dip ∈ kD(?rt2 dip)" by simp
moreover have "nsqn ?rt1 dip < nsqn (?rt2 dip) dip"
proof -
have "nsqn ?rt1 oip = osn"
by (simp add: ‹dip = oip› nsqn_update_changed_kno_val [OF change [THEN not_sym]])
also have "... < nsqn (rt (σ' sip)) oip" using osnlt .
also have "... = nsqn (?rt2 oip) oip" by (simp add: change)
finally show ?thesis
using ‹dip = oip› by simp
qed
ultimately show ?thesis
by (rule rt_strictly_fresher_ltI)
next
assume osneq: "osn = nsqn (rt (σ' sip)) oip ∧ the (dhops (rt (σ' sip)) oip) ≤ hops"
have "oip∈kD(?rt1)" by simp
moreover from a3 ‹dip = oip› have "oip∈kD(?rt2 oip)" by simp
moreover have "nsqn ?rt1 oip = nsqn (?rt2 oip) oip"
proof -
from osneq have "osn = nsqn (rt (σ' sip)) oip" ..
also have "osn = nsqn ?rt1 oip"
by (simp add: ‹dip = oip› nsqn_update_changed_kno_val [OF change [THEN not_sym]])
also have "nsqn (rt (σ' sip)) oip = nsqn (?rt2 oip) oip"
by (simp add: change)
finally show ?thesis .
qed
moreover have "π⇩5(the (?rt2 oip oip)) < π⇩5(the (?rt1 oip))"
proof -
from osneq have "the (dhops (rt (σ' sip)) oip) ≤ hops" ..
moreover from ‹oip ∈ vD (rt (σ' sip))› have "oip∈kD(rt (σ' sip))" by auto
ultimately have "π⇩5(the (rt (σ' sip) oip)) ≤ hops"
by (auto simp add: proj5_eq_dhops)
also from change after have "hops < π⇩5(the (rt (σ' i) oip))"
by (simp add: proj5_eq_dhops) (metis dhops_update_changed lessI)
finally have "π⇩5(the (rt (σ' sip) oip)) < π⇩5(the (rt (σ' i) oip))" .
with change after show ?thesis by simp
qed
ultimately have "?rt1 ⊏⇘oip⇙ ?rt2 oip"
by (rule rt_strictly_fresher_eqI)
with ‹dip = oip› show ?thesis by simp
qed
qed
qed
qed
} note rreq_rrep_update = this
have "opaodv i ⊨ (otherwith ((=)) {i} (orecvmsg (λσ m. msg_fresh σ m
∧ msg_zhops m)),
other quality_increases {i} →)
onl Γ⇩A⇩O⇩D⇩V
(λ(σ, _). ∀dip. dip ∈ vD (rt (σ i)) ∩ vD (rt (σ (the (nhop (rt (σ i)) dip))))
∧ the (nhop (rt (σ i)) dip) ≠ dip
⟶ rt (σ i) ⊏⇘dip⇙ rt (σ (the (nhop (rt (σ i)) dip))))"
proof (inv_cterms inv add: onl_oinvariant_sterms [OF aodv_wf rreq_sip [THEN weaken]]
onl_oinvariant_sterms [OF aodv_wf rrep_sip [THEN weaken]]
onl_oinvariant_sterms [OF aodv_wf rerr_sip [THEN weaken]]
onl_oinvariant_sterms [OF aodv_wf oosn_rreq [THEN weaken]]
onl_oinvariant_sterms [OF aodv_wf odsn_rrep [THEN weaken]]
onl_oinvariant_sterms [OF aodv_wf oaddpreRT_welldefined]
solve: basic update_0_unk invalidate rreq_rrep_update
simp add: seqlsimp)
fix σ σ' p l
assume or: "(σ, p) ∈ oreachable (opaodv i) (?S i) (other quality_increases {i})"
and "other quality_increases {i} σ σ'"
and ll: "l ∈ labels Γ⇩A⇩O⇩D⇩V p"
and pre: "∀dip. dip∈vD (rt (σ i))
∧ dip∈vD(rt (σ (the (nhop (rt (σ i)) dip))))
∧ the (nhop (rt (σ i)) dip) ≠ dip
⟶ rt (σ i) ⊏⇘dip⇙ rt (σ (the (nhop (rt (σ i)) dip)))"
from this(1-2)
have or': "(σ', p) ∈ oreachable (opaodv i) (?S i) (other quality_increases {i})"
by - (rule oreachable_other')
from or and ll have next_hop: "∀dip. let nhip = the (nhop (rt (σ i)) dip)
in dip ∈ kD(rt (σ i)) ∧ nhip ≠ dip
⟶ dip ∈ kD(rt (σ nhip))
∧ nsqn (rt (σ i)) dip ≤ nsqn (rt (σ nhip)) dip"
by (auto dest!: onl_oinvariant_weakenD [OF seq_compare_next_hop'])
from or and ll have unk_hops_one: "∀dip∈kD (rt (σ i)). sqn (rt (σ i)) dip = 0
⟶ sqnf (rt (σ i)) dip = unk
∧ the (dhops (rt (σ i)) dip) = 1
∧ the (nhop (rt (σ i)) dip) = dip"
by (auto dest!: onl_oinvariant_weakenD [OF ozero_seq_unk_hops_one
[OF oaodv_trans aodv_trans]]
otherwith_actionD
simp: seqlsimp)
from ‹other quality_increases {i} σ σ'› have "σ' i = σ i" by auto
hence "quality_increases (σ i) (σ' i)" by auto
with ‹other quality_increases {i} σ σ'› have "∀j. quality_increases (σ j) (σ' j)"
by - (erule otherE, metis singleton_iff)
show "∀dip. dip ∈ vD (rt (σ' i))
∧ dip ∈ vD (rt (σ' (the (nhop (rt (σ' i)) dip))))
∧ the (nhop (rt (σ' i)) dip) ≠ dip
⟶ rt (σ' i) ⊏⇘dip⇙ rt (σ' (the (nhop (rt (σ' i)) dip)))"
proof clarify
fix dip
assume "dip∈vD(rt (σ' i))"
and "dip∈vD(rt (σ' (the (nhop (rt (σ' i)) dip))))"
and "the (nhop (rt (σ' i)) dip) ≠ dip"
from this(1) and ‹σ' i = σ i› have "dip∈vD(rt (σ i))"
and "dip∈kD(rt (σ i))"
by auto
from ‹the (nhop (rt (σ' i)) dip) ≠ dip› and ‹σ' i = σ i›
have "the (nhop (rt (σ i)) dip) ≠ dip" (is "?nhip ≠ _") by simp
with ‹dip∈kD(rt (σ i))› and next_hop
have "dip∈kD(rt (σ (?nhip)))"
and nsqns: "nsqn (rt (σ i)) dip ≤ nsqn (rt (σ ?nhip)) dip"
by (auto simp: Let_def)
have "0 < sqn (rt (σ i)) dip"
proof (rule neq0_conv [THEN iffD1, OF notI])
assume "sqn (rt (σ i)) dip = 0"
with ‹dip∈kD(rt (σ i))› and unk_hops_one
have "?nhip = dip" by simp
with ‹?nhip ≠ dip› show False ..
qed
also have "... = nsqn (rt (σ i)) dip"
by (rule vD_nsqn_sqn [OF ‹dip∈vD(rt (σ i))›, THEN sym])
also have "... ≤ nsqn (rt (σ ?nhip)) dip"
by (rule nsqns)
also have "... ≤ sqn (rt (σ ?nhip)) dip"
by (rule nsqn_sqn)
finally have "0 < sqn (rt (σ ?nhip)) dip" .
have "rt (σ i) ⊏⇘dip⇙ rt (σ' ?nhip)"
proof (cases "dip∈vD(rt (σ ?nhip))")
assume "dip∈vD(rt (σ ?nhip))"
with pre ‹dip∈vD(rt (σ i))› and ‹?nhip ≠ dip›
have "rt (σ i) ⊏⇘dip⇙ rt (σ ?nhip)" by auto
moreover from ‹∀j. quality_increases (σ j) (σ' j)›
have "quality_increases (σ ?nhip) (σ' ?nhip)" ..
ultimately show ?thesis
using ‹dip∈kD(rt (σ ?nhip))›
by (rule strictly_fresher_quality_increases_right)
next
assume "dip∉vD(rt (σ ?nhip))"
with ‹dip∈kD(rt (σ ?nhip))› have "dip∈iD(rt (σ ?nhip))" ..
hence "the (flag (rt (σ ?nhip)) dip) = inv"
by auto
have "nsqn (rt (σ i)) dip ≤ nsqn (rt (σ ?nhip)) dip"
by (rule nsqns)
also from ‹dip∈iD(rt (σ ?nhip))›
have "... = sqn (rt (σ ?nhip)) dip - 1" ..
also have "... < sqn (rt (σ' ?nhip)) dip"
proof -
from ‹∀j. quality_increases (σ j) (σ' j)›
have "quality_increases (σ ?nhip) (σ' ?nhip)" ..
hence "∀ip. sqn (rt (σ ?nhip)) ip ≤ sqn (rt (σ' ?nhip)) ip" by auto
hence "sqn (rt (σ ?nhip)) dip ≤ sqn (rt (σ' ?nhip)) dip" ..
with ‹0 < sqn (rt (σ ?nhip)) dip› show ?thesis by auto
qed
also have "... = nsqn (rt (σ' ?nhip)) dip"
proof (rule vD_nsqn_sqn [THEN sym])
from ‹dip∈vD(rt (σ' (the (nhop (rt (σ' i)) dip))))› and ‹σ' i = σ i›
show "dip∈vD(rt (σ' ?nhip))" by simp
qed
finally have "nsqn (rt (σ i)) dip < nsqn (rt (σ' ?nhip)) dip" .
moreover from ‹dip∈vD(rt (σ' (the (nhop (rt (σ' i)) dip))))› and ‹σ' i = σ i›
have "dip∈kD(rt (σ' ?nhip))" by auto
ultimately show "rt (σ i) ⊏⇘dip⇙ rt (σ' ?nhip)"
using ‹dip∈kD(rt (σ i))› by - (rule rt_strictly_fresher_ltI)
qed
with ‹σ' i = σ i› show "rt (σ' i) ⊏⇘dip⇙ rt (σ' (the (nhop (rt (σ' i)) dip)))"
by simp
qed
qed
thus ?thesis unfolding Let_def .
qed
lemma seq_compare_next_hop:
fixes w
shows "opaodv i ⊨ (otherwith ((=)) {i} (orecvmsg msg_fresh),
other quality_increases {i} →)
global (λσ. ∀dip. let nhip = the (nhop (rt (σ i)) dip)
in dip ∈ kD(rt (σ i)) ∧ nhip ≠ dip ⟶
dip ∈ kD(rt (σ nhip))
∧ nsqn (rt (σ i)) dip ≤ nsqn (rt (σ nhip)) dip)"
by (rule oinvariant_weakenE [OF seq_compare_next_hop']) (auto dest!: onlD)
lemma seq_nhop_quality_increases:
shows "opaodv i ⊨ (otherwith ((=)) {i}
(orecvmsg (λσ m. msg_fresh σ m ∧ msg_zhops m)),
other quality_increases {i} →)
global (λσ. ∀dip. let nhip = the (nhop (rt (σ i)) dip)
in dip ∈ vD (rt (σ i)) ∩ vD (rt (σ nhip)) ∧ nhip ≠ dip
⟶ (rt (σ i)) ⊏⇘dip⇙ (rt (σ nhip)))"
by (rule oinvariant_weakenE [OF seq_nhop_quality_increases']) (auto dest!: onlD)
end