# Theory E_Global_Invariants

(*  Title:       variants/e_all_abcd/Global_Invariants.thy
Author:      Timothy Bourke, Inria
Author:      Peter Höfner, NICTA
*)

section "Global invariant proofs over sequential processes"

theory E_Global_Invariants
imports E_Seq_Invariants
E_Aodv_Predicates
E_Fresher
E_Quality_Increases
AWN.OAWN_Convert
E_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 "jI"
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

assumes other: "σ σ' m.  P σ m; other Q {i} σ σ'   P σ' m"
and local: "σ m. P σ m  P (σ(i := σ imsg := m)) m"
shows "opaodv i  (otherwith Q {i} (orecvmsg P), other Q {i} →)
onl ΓAODV (λ(σ, 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 = σ imsg := msg"
from this(1) have "P σ msg"
and "j. ji  Q (σ j) (σ' j)" by auto
from this(1) have "P (σ(i := σ imsg := msg)) msg" by (rule local)
thus "P σ' msg"
proof (rule other)
from σ' i = σ imsg := msg and j. ji  Q (σ j) (σ' j)
show "other Q {i} (σ(i := σ imsg := 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 ΓAODV (λ((ξ, _), _, (ξ', _)). quality_increases ξ ξ')"
proof (rule step_invariantI)
fix s a s'
assume sr:
and tr: "(s, a, s')  trans (paodv i)"
and rm:
from sr have srTT: "s  reachable (paodv i) TT" ..

from route_tables_fresher sr tr rm
have "onll ΓAODV (λ((ξ, _), _, (ξ', _)). dipkD (rt ξ). rt ξ ⊑⇘diprt ξ') (s, a, s')"
by (rule step_invariantD)

moreover from known_destinations_increase srTT tr TT_True
have "onll ΓAODV (λ((ξ, _), _, (ξ', _)). kD (rt ξ)  kD (rt ξ')) (s, a, s')"
by (rule step_invariantD)

moreover from sqns_increase srTT tr TT_True
have "onll ΓAODV (λ((ξ, _), _, (ξ', _)). ip. sqn (rt ξ) ip  sqn (rt ξ') ip) (s, a, s')"
by (rule step_invariantD)

ultimately show "onll ΓAODV (λ((ξ, _), _, (ξ', _)). 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 ΓAODV (λ((σ, _), _, (σ', _)). 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 ΓAODV p"
and "?S σ σ' a"
and tr: "((σ, p), a, (σ', p'))  oseqp_sos ΓAODV i"
and ll': "l'  labels ΓAODV p'"
from this(1-3) have "orecvmsg (λ_. rreq_rrep_sn) σ a"
by (auto dest!: oreachable_weakenE [where QS=
and QU=]
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 ΓAODV (λ((σ, _), 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 ΓAODV i"
and recv: "act (recvmsg rreq_rrep_sn) σ σ' a"
obtain l l' where "llabels ΓAODV p" and "l'labels ΓAODV p'"
by (metis aodv_ex_label)
from ((σ, p), a, (σ', p'))  oseqp_sos ΓAODV 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 ΓAODV (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 ΓAODV (seqll i (λ((ξ, _), a, _). anycast (rreq_rrep_fresh (rt ξ)) a))
((σ, p), a, (σ', p'))"
using or tr recv by - (erule(4) ostep_invariantE)
thus ?thesis
using llabels ΓAODV p and l'labels ΓAODV 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 ΓAODV (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 ΓAODV (seqll i (λ((ξ, _), a, _). anycast (rerr_invalid (rt ξ)) a))
((σ, p), a, (σ', p'))"
using or tr recv by - (erule(4) ostep_invariantE)
thus ?thesis
using llabels ΓAODV p and l'labels ΓAODV p' by auto
qed

moreover have
proof -
from or tr recv
have "onll ΓAODV (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 llabels ΓAODV p and l'labels ΓAODV 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 ΓAODV (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 llabels ΓAODV p and l'labels ΓAODV p'
by - (drule(3) onll_ostep_invariantD, auto)
qed

ultimately have "anycast (msg_fresh σ) a"
del: msg_fresh
split: seq_action.split_asm msg.split_asm) simp_all
thus "onll ΓAODV (λ((σ, _), a, _). anycast (msg_fresh σ) a) ((σ, p), a, (σ', p'))"
by auto
qed

"opaodv i  (otherwith quality_increases {i} (orecvmsg msg_fresh),
other quality_increases {i} →)
onl ΓAODV (λ(σ, l). l  {PAodv-:1}  msg_fresh σ (msg (σ i)))"
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 := σ imsg := 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 ΓAODV (λ((σ, _), _, (σ', _)). 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 ΓAODV (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 ΓAODV (λ(σ, 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 oosn_rreq]
simp del: One_nat_def, rule impI)
fix σ σ' p l
assume "(σ, p)  oreachable (opaodv i) ?S ?U"
and "l  labels ΓAODV 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 ΓAODV 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 ΓAODV (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 ΓAODV (λ(σ, 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 odsn_rrep]
simp del: One_nat_def, rule impI)
fix σ σ' p l
assume "(σ, p)  oreachable (opaodv i) ?S ?U"
and "l  labels ΓAODV 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 ΓAODV 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 ΓAODV (λ(σ, l).
l  {PAodv-:8, PAodv-:9, PRerr-:0, PRerr-:1}
(ripcdom(dests (σ i)). ripckD(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 *: "ripdom dests. rip  kD (rt (σ sip))
the (dests rip) - 1  nsqn (rt (σ sip)) rip"
and "dests rip = Some rsn"
from this(3) have "ripdom dests" by auto
with * and dests rip = Some rsn have "ripkD(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 ripkD(rt (σ sip)) and quality_increases (σ sip) (σ' sip)
show "rip  kD(rt (σ' sip))" ..
next
from ripkD(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]
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 ΓAODV (λ(ξ, l). (l = PRerr-:1
(ipdom(dests ξ). ipvD(rt ξ)
the (nhop (rt ξ) ip) = sip ξ
sqn (rt ξ) ip < the (dests ξ ip))))"
by (inv_cterms) (clarsimp split: option.split_asm if_split_asm)

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 ΓAODV (λ(σ, _).
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: "dipkD(rt (σ i)). nhop dip  dip
dipkD(rt (σ (nhop dip)))  nsqn (rt (σ i)) dip  nsqn (rt (σ (nhop dip))) dip"
and qinc: "j. quality_increases (σ j) (σ' j)"
have "dipkD(rt (σ i)). nhop dip  dip
dipkD(rt (σ' (nhop dip)))  nsqn (rt (σ i)) dip  nsqn (rt (σ' (nhop dip))) dip"
proof (intro ballI impI)
fix dip
assume "dipkD(rt (σ i))"
and "nhop dip  dip"
with pre have "dipkD(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 dipkD(rt (σ (nhop dip))) have "dipkD (rt (σ' (nhop dip)))" ..

moreover have "nsqn (rt (σ i)) dip  nsqn (rt (σ' (nhop dip))) dip"
proof -
from dipkD(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 "dipkD(rt (σ' (nhop dip)))
nsqn (rt (σ i)) dip  nsqn (rt (σ' (nhop dip))) dip" ..
qed
} note basic = this

{ fix nhop and σ σ' :: "ip  state"
assume pre: "dipkD(rt (σ i)). nhop dip  dip  dipkD(rt (σ (nhop dip)))
nsqn (rt (σ i)) dip  nsqn (rt (σ (nhop dip))) dip"
and ndest: "ripcdom (dests (σ i)). ripc  kD (rt (σ (sip (σ i))))
the (dests (σ i) ripc) - 1  nsqn (rt (σ (sip (σ i)))) ripc"
and issip: "ipdom (dests (σ i)). nhop ip = sip (σ i)"
and qinc: "j. quality_increases (σ j) (σ' j)"
have "dipkD(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 "dipkD(rt (σ i))"
and "nhop dip  dip"
with pre and qinc have "dipkD(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 "dipdom (dests (σ i))")
assume "dipdom (dests (σ i))"
with dipkD(rt (σ i)) obtain dsn where "dests (σ i) dip = Some dsn"
by auto
with dipkD(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 dipdom (dests (σ i)) have "dip  kD (rt (σ (sip (σ i))))"
"dsn - 1  nsqn (rt (σ (sip (σ i)))) dip"
by auto
moreover from issip and dipdom (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 dipkD(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 dipkD(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: "dipkD(rt (σ i)). the (nhop (rt (σ i)) dip)  dip
dipkD(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 "dipkD(rt (σ i)).
the (nhop (update (rt (σ i)) (sip (σ i)) (0, unk, val, Suc 0, sip (σ i))) dip)  dip
dipkD(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 "dipkD(rt (σ i)). ?P dip")
proof
fix dip
assume "dipkD(rt (σ i))"
with a1 and a2
have "the (nhop (rt (σ i)) dip)  dip  dipkD(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: "dipkD (rt (σ i)). the (nhop (rt (σ i)) dip)  dip
dipkD(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  oipkD(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': "dipkD (rt (σ i)). the (nhop (rt (σ i)) dip)  dip
dipkD(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
oipkD(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: "dipkD (rt (σ i)). the (nhop (rt (σ i)) dip)  dip
dipkD(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  oipkD(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': "dipkD (rt (σ i)). the (nhop (rt (σ i)) dip)  dip
dipkD(rt (σ' (the (nhop (rt (σ i)) dip))))
nsqn (rt (σ i)) dip  nsqn (rt (σ' (the (nhop (rt (σ i)) dip)))) dip"
by (rule basic)
have "dipkD(rt (σ i)).
the (nhop (update (rt (σ i)) oip (osn, kno, val, Suc hops, sip)) dip)  dip
dipkD(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 "dipkD(rt (σ i)). _  ?dip_in_kD dip  ?nsqn_le_nsqn dip")
proof (intro ballI impI, split update_rt_split_asm)
fix dip
assume "dipkD(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 "dipkD(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' dipkD(rt (σ i)) notdip
show ?thesis by clarsimp
next
assume "dip = oip"
with rtnot qinc dipkD(rt (σ i)) notdip *
have "?dip_in_kD dip"
by simp (metis kD_quality_increases)
moreover from dip = oip rtnot qinc dipkD(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 ΓAODV (λ(σ, _).
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 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 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 "dipkD(rt (σ i))"
shows "π3(the (rt (σ i) dip)) = unk  1  π2(the (rt (σ i) dip))"
(is "?P dip")
proof -
have "l. llabels ΓAODV p" by (metis aodv_ex_label)
with assms(1) have "dipkD (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 dipkD(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 "dipkD(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. llabels ΓAODV p" by (metis aodv_ex_label)
with assms(1) have "dipkD (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 dipkD(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 ΓAODV (λ(σ, _). 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. dipvD(rt (σ i))
dipvD(rt (σ (the (nhop (rt (σ i)) dip))))
(the (nhop (rt (σ i)) dip))  dip
rt (σ i) ⊏⇘diprt (σ (the (nhop (rt (σ i)) dip)))"
and ow: "?S i σ σ' a"
have "dip. dipvD(rt (σ i))
dipvD (rt (σ' (the (nhop (rt (σ i)) dip))))
(the (nhop (rt (σ i)) dip))  dip
rt (σ i) ⊏⇘diprt (σ' (the (nhop (rt (σ i)) dip)))"
proof clarify
fix dip
assume a2: "dipvD(rt (σ i))"
and a3: "dipvD (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) ⊏⇘diprt (σ' (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) ⊏⇘diprt (σ (the (nhop (rt (σ i)) dip)))" by simp
with (the (nhop (rt (σ i)) dip)) = i have "rt (σ i) ⊏⇘diprt (σ 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 dipvD (rt (σ' (the (nhop (rt (σ i)) dip))))
have "dipvD (rt (σ (the (nhop (rt (σ i)) dip))))" by simp
with a1 a2 a4 have "rt (σ i) ⊏⇘diprt (σ (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. dipvD(rt (σ i))
dipvD(rt (σ (the (nhop (rt (σ i)) dip))))
the (nhop (rt (σ i)) dip)  dip
rt (σ i) ⊏⇘diprt (σ (the (nhop (rt (σ i)) dip)))"
and ow: "?S i σ σ' a"
have "dip. dipvD(update (rt (σ i)) sip (0, unk, val, Suc 0, sip))
dipvD(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)
⊏⇘diprt (σ' (the (nhop (update (rt (σ i)) sip (0, unk, val, Suc 0, sip)) dip)))"
proof clarify
fix dip
assume a2: "dipvD (update (rt (σ i)) sip (0, unk, val, Suc 0, sip))"
and a3: "dipvD(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)
⊏⇘diprt (σ' (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 "dipvD(rt (σ i))  dip = sip"
by (rule vD_update_val)
with dip  sip have "dipvD(rt (σ i))" by simp
moreover from a3 have "dipvD(rt (σ' (the (nhop (rt (σ i)) dip))))" by simp
moreover from a4 have "the (nhop (rt (σ i)) dip)  dip" by simp
ultimately have "rt (σ i) ⊏⇘diprt (σ' (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. dipvD(rt (σ i))  dipvD(rt (σ (nhop dip)))  nhop dip  dip
rt (σ i) ⊏⇘diprt (σ (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) ⊏⇘diprt (σ' (nhop dip))"
proof clarify
fix dip
assume "dipvD(invalidate (rt (σ i)) (dests (σ i)))"
and "dipvD(rt (σ' (nhop dip)))"
and "nhop dip  dip"
from this(1) have "dipvD (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) ⊏⇘diprt (σ (nhop dip))"
using pre dip  vD (rt (σ' (nhop dip))) nhop dip  dip
by metis
with j. j  i  σ j = σ' j show  "rt (σ i) ⊏⇘diprt (σ' (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) ⊏⇘diprt (σ (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 = σ irt := 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)
⊏⇘diprt (σ' (the (nhop (update (rt (σ i)) oip (osn, kno, val, Suc hops, sip)) dip)))"
proof clarify
fix dip
assume a2: "dipvD(update (rt (σ i)) oip (osn, kno, val, Suc (hops), sip))"
and a3: "dipvD(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)
⊏⇘diprt (σ' (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 "dipvD (rt (σ i))" by simp
moreover from a3 have "dipvD(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) ⊏⇘diprt (σ (the (nhop (rt (σ i)) dip)))"
using pre by simp

hence "rt (σ i) ⊏⇘diprt (σ' (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 "dipkD(rt (σ' i))" by auto
show ?thesis
proof (cases "dip = oip")
assume "dip  oip"

with a2 have "dipvD (rt (σ i))" by auto
moreover with a3 a5 after and dip  oip
have "dipvD(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) ⊏⇘diprt (σ (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 "oipkD(rt (σ sip))"
and "osn  nsqn (rt (σ sip)) oip" by auto

from a3 change dip = oip have "oipvD(rt (σ' sip))" by simp
hence "the (flag (rt (σ' sip)) oip) = val" by simp

from oipkD(rt (σ sip))
have "osn < nsqn (rt (σ' sip)) oip  (osn = nsqn (rt (σ' sip)) oip
the (dhops (rt (σ' sip)) oip)  hops)"
proof
assume "oipvD(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
― ‹alternative to using @{text sip_not_ip}
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 oipkD(rt (σ sip)) and sip = i show "oipkD(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)
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)
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)
else rt (σ i) a) = rt (σ i)" ..
next
from oipkD(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 "oipiD(rt (σ sip))"
with the (flag (rt (σ' sip)) oip) = val and a5 have "sip = i"
by (metis f.distinct(1) iD_flag_is_inv)
from oipiD(rt (σ sip)) have "the (flag (rt (σ sip)) oip) = inv" by auto
with sip = i Suc 0  osn change after oipkD(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 dipkD(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 "oipkD(?rt1)" by simp
moreover from a3 dip = oip have "oipkD(?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"
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 "oipkD(rt (σ' sip))" by auto
ultimately have "π5(the (rt (σ' sip) oip))  hops"
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 ΓAODV
(λ(σ, _). dip. dip  vD (rt (σ i))  vD (rt (σ (the (nhop (rt (σ i)) dip))))
the (nhop (rt (σ i)) dip)  dip
rt (σ i) ⊏⇘diprt (σ (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]]
solve: basic update_0_unk invalidate rreq_rrep_update
fix σ σ' p l
assume or: "(σ, p)  oreachable (opaodv i) (?S i)  (other quality_increases {i})"
and "other quality_increases {i} σ σ'"
and ll: "l  labels ΓAODV p"
and pre: "dip. dipvD (rt (σ i))
dipvD(rt (σ (the (nhop (rt (σ i)) dip))))
the (nhop (rt (σ i)) dip)  dip
rt (σ i) ⊏⇘diprt (σ (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: "dipkD (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) ⊏⇘diprt (σ' (the (nhop (rt (σ' i)) dip)))"
proof clarify
fix dip
assume "dipvD(rt (σ' i))"
and "dipvD(rt (σ' (the (nhop (rt (σ' i)) dip))))"
and "the (nhop (rt (σ' i)) dip)  dip"
from this(1) and σ' i = σ i have "dipvD(rt (σ i))"
and "dipkD(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 dipkD(rt (σ i)) and next_hop
have "dipkD(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 dipkD(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 dipvD(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) ⊏⇘diprt (σ' ?nhip)"
proof (cases "dipvD(rt (σ ?nhip))")
assume "dipvD(rt (σ ?nhip))"
with pre dipvD(rt (σ i)) and ?nhip  dip
have "rt (σ i) ⊏⇘diprt (σ ?nhip)" by auto
moreover from j. quality_increases (σ j) (σ' j)
have "quality_increases (σ ?nhip) (σ' ?nhip)" ..
ultimately show ?thesis
using dipkD(rt (σ ?nhip))
by (rule strictly_fresher_quality_increases_right)
next
assume "dipvD(rt (σ ?nhip))"
with dipkD(rt (σ ?nhip)) have "dipiD(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 dipiD(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 dipvD(rt (σ' (the (nhop (rt (σ' i)) dip)))) and σ' i = σ i
show "dipvD(rt (σ' ?nhip))" by simp
qed
finally have "nsqn (rt (σ i)) dip < nsqn (rt (σ' ?nhip)) dip" .

moreover from dipvD(rt (σ' (the (nhop (rt (σ' i)) dip)))) and σ' i = σ i
have "dipkD(rt (σ' ?nhip))" by auto
ultimately show "rt (σ i) ⊏⇘diprt (σ' ?nhip)"
using dipkD(rt (σ i)) by - (rule rt_strictly_fresher_ltI)
qed
with σ' i = σ i show "rt (σ' i) ⊏⇘diprt (σ' (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 =