# Theory D_Aodv

```(*  Title:       variants/d_fwdrreqs/Aodv.thy
Author:      Timothy Bourke, Inria
Author:      Peter Höfner, NICTA
*)

section "The AODV protocol"

theory D_Aodv
imports D_Aodv_Data D_Aodv_Message
AWN.AWN_SOS_Labels AWN.AWN_Invariants
begin

subsection "Data state"

record state =
ip    :: "ip"
sn    :: "sqn"
rt    :: "rt"
rreqs :: "(ip × rreqid) set"
store :: "store"
(* all locals *)
msg    :: "msg"
data   :: "data"
dests  :: "ip ⇀ sqn"
pre    :: "ip set"
rreqid :: "rreqid"
dip    :: "ip"
oip    :: "ip"
hops   :: "nat"
dsn    :: "sqn"
dsk    :: "k"
osn    :: "sqn"
sip    :: "ip"
handled:: "bool"

abbreviation aodv_init :: "ip ⇒ state"
where "aodv_init i ≡ ⦇
ip = i,
sn = 1,
rt = Map.empty,
rreqs = {},
store = Map.empty,

msg    = (SOME x. True),
data   = (SOME x. True),
dests  = (SOME x. True),
pre    = (SOME x. True),
rreqid = (SOME x. True),
dip    = (SOME x. True),
oip    = (SOME x. True),
hops   = (SOME x. True),
dsn    = (SOME x. True),
dsk    = (SOME x. True),
osn    = (SOME x. True),
sip    = (SOME x. x ≠ i),
handled= (SOME x. True)
⦈"

lemma some_neq_not_eq [simp]: "¬((SOME x :: nat. x ≠ i) = i)"
by (subst some_eq_ex) (metis zero_neq_numeral)

definition clear_locals :: "state ⇒ state"
where "clear_locals ξ = ξ ⦇
msg    := (SOME x. True),
data   := (SOME x. True),
dests  := (SOME x. True),
pre    := (SOME x. True),
rreqid := (SOME x. True),
dip    := (SOME x. True),
oip    := (SOME x. True),
hops   := (SOME x. True),
dsn    := (SOME x. True),
dsk    := (SOME x. True),
osn    := (SOME x. True),
sip    := (SOME x. x ≠ ip ξ),
handled:= (SOME x. True)
⦈"

lemma clear_locals_sip_not_ip [simp]: "¬(sip (clear_locals ξ) = ip ξ)"
unfolding clear_locals_def by simp

lemma clear_locals_but_not_globals [simp]:
"ip (clear_locals ξ) = ip ξ"
"sn (clear_locals ξ) = sn ξ"
"rt (clear_locals ξ) = rt ξ"
"rreqs (clear_locals ξ) = rreqs ξ"
"store (clear_locals ξ) = store ξ"
unfolding clear_locals_def by auto

subsection "Auxilliary message handling definitions"

definition is_newpkt
where "is_newpkt ξ ≡ case msg ξ of
Newpkt data' dip' ⇒ { ξ⦇data := data', dip := dip'⦈ }
| _ ⇒ {}"

definition is_pkt
where "is_pkt ξ ≡ case msg ξ of
Pkt data' dip' oip' ⇒ { ξ⦇ data := data', dip := dip', oip := oip' ⦈ }
| _ ⇒ {}"

definition is_rreq
where "is_rreq ξ ≡ case msg ξ of
Rreq hops' rreqid' dip' dsn' dsk' oip' osn' sip' handled' ⇒
{ ξ⦇ hops := hops', rreqid := rreqid', dip := dip', dsn := dsn',
dsk := dsk', oip := oip', osn := osn', sip := sip',
handled := handled' ⦈ }
| _ ⇒ {}"

lemma is_rreq_asm [dest!]:
assumes "ξ' ∈ is_rreq ξ"
shows "(∃hops' rreqid' dip' dsn' dsk' oip' osn' sip' handled'.
msg ξ = Rreq hops' rreqid' dip' dsn' dsk' oip' osn' sip' handled' ∧
ξ' = ξ⦇ hops := hops', rreqid := rreqid', dip := dip', dsn := dsn',
dsk := dsk', oip := oip', osn := osn', sip := sip',
handled := handled' ⦈)"
using assms unfolding is_rreq_def
by (cases "msg ξ") simp_all

definition is_rrep
where "is_rrep ξ ≡ case msg ξ of
Rrep hops' dip' dsn' oip' sip' ⇒
{ ξ⦇ hops := hops', dip := dip', dsn := dsn', oip := oip', sip := sip' ⦈ }
| _ ⇒ {}"

lemma is_rrep_asm [dest!]:
assumes "ξ' ∈ is_rrep ξ"
shows "(∃hops' dip' dsn' oip' sip'.
msg ξ = Rrep hops' dip' dsn' oip' sip' ∧
ξ' = ξ⦇ hops := hops', dip := dip', dsn := dsn', oip := oip', sip := sip' ⦈)"
using assms unfolding is_rrep_def
by (cases "msg ξ") simp_all

definition is_rerr
where "is_rerr ξ ≡ case msg ξ of
Rerr dests' sip' ⇒ { ξ⦇ dests := dests', sip := sip' ⦈ }
| _ ⇒ {}"

lemma is_rerr_asm [dest!]:
assumes "ξ' ∈ is_rerr ξ"
shows "(∃dests' sip'.
msg ξ = Rerr dests' sip' ∧
ξ' = ξ⦇ dests := dests', sip := sip' ⦈)"
using assms unfolding is_rerr_def
by (cases "msg ξ") simp_all

lemmas is_msg_defs =
is_rerr_def is_rrep_def is_rreq_def is_pkt_def is_newpkt_def

lemma is_msg_inv_ip [simp]:
"ξ' ∈ is_rerr ξ   ⟹ ip ξ' = ip ξ"
"ξ' ∈ is_rrep ξ   ⟹ ip ξ' = ip ξ"
"ξ' ∈ is_rreq ξ   ⟹ ip ξ' = ip ξ"
"ξ' ∈ is_pkt ξ    ⟹ ip ξ' = ip ξ"
"ξ' ∈ is_newpkt ξ ⟹ ip ξ' = ip ξ"
unfolding is_msg_defs
by (cases "msg ξ", clarsimp+)+

lemma is_msg_inv_sn [simp]:
"ξ' ∈ is_rerr ξ   ⟹ sn ξ' = sn ξ"
"ξ' ∈ is_rrep ξ   ⟹ sn ξ' = sn ξ"
"ξ' ∈ is_rreq ξ   ⟹ sn ξ' = sn ξ"
"ξ' ∈ is_pkt ξ    ⟹ sn ξ' = sn ξ"
"ξ' ∈ is_newpkt ξ ⟹ sn ξ' = sn ξ"
unfolding is_msg_defs
by (cases "msg ξ", clarsimp+)+

lemma is_msg_inv_rt [simp]:
"ξ' ∈ is_rerr ξ   ⟹ rt ξ' = rt ξ"
"ξ' ∈ is_rrep ξ   ⟹ rt ξ' = rt ξ"
"ξ' ∈ is_rreq ξ   ⟹ rt ξ' = rt ξ"
"ξ' ∈ is_pkt ξ    ⟹ rt ξ' = rt ξ"
"ξ' ∈ is_newpkt ξ ⟹ rt ξ' = rt ξ"
unfolding is_msg_defs
by (cases "msg ξ", clarsimp+)+

lemma is_msg_inv_rreqs [simp]:
"ξ' ∈ is_rerr ξ   ⟹ rreqs ξ' = rreqs ξ"
"ξ' ∈ is_rrep ξ   ⟹ rreqs ξ' = rreqs ξ"
"ξ' ∈ is_rreq ξ   ⟹ rreqs ξ' = rreqs ξ"
"ξ' ∈ is_pkt ξ    ⟹ rreqs ξ' = rreqs ξ"
"ξ' ∈ is_newpkt ξ ⟹ rreqs ξ' = rreqs ξ"
unfolding is_msg_defs
by (cases "msg ξ", clarsimp+)+

lemma is_msg_inv_store [simp]:
"ξ' ∈ is_rerr ξ   ⟹ store ξ' = store ξ"
"ξ' ∈ is_rrep ξ   ⟹ store ξ' = store ξ"
"ξ' ∈ is_rreq ξ   ⟹ store ξ' = store ξ"
"ξ' ∈ is_pkt ξ    ⟹ store ξ' = store ξ"
"ξ' ∈ is_newpkt ξ ⟹ store ξ' = store ξ"
unfolding is_msg_defs
by (cases "msg ξ", clarsimp+)+

lemma is_msg_inv_sip [simp]:
"ξ' ∈ is_pkt ξ    ⟹ sip ξ' = sip ξ"
"ξ' ∈ is_newpkt ξ ⟹ sip ξ' = sip ξ"
unfolding is_msg_defs
by (cases "msg ξ", clarsimp+)+

subsection "The protocol process"

datatype pseqp =
PAodv
| PNewPkt
| PPkt
| PRreq
| PRrep
| PRerr

fun nat_of_seqp :: "pseqp ⇒ nat"
where
"nat_of_seqp PAodv  = 1"
| "nat_of_seqp PPkt   = 2"
| "nat_of_seqp PNewPkt   = 3"
| "nat_of_seqp PRreq  = 4"
| "nat_of_seqp PRrep  = 5"
| "nat_of_seqp PRerr  = 6"

instantiation "pseqp" :: ord
begin
definition less_eq_seqp [iff]: "l1 ≤ l2 = (nat_of_seqp l1 ≤ nat_of_seqp l2)"
definition less_seqp [iff]:    "l1 < l2 = (nat_of_seqp l1 < nat_of_seqp l2)"
instance ..
end

abbreviation AODV
where
"AODV ≡ λ_. ⟦clear_locals⟧ call(PAodv)"

abbreviation PKT
where
"PKT args ≡

⟦ξ. let (data, dip, oip) = args ξ in
(clear_locals ξ) ⦇ data := data, dip := dip, oip := oip ⦈⟧
call(PPkt)"
abbreviation NEWPKT
where
"NEWPKT args ≡
⟦ξ. let (data, dip) = args ξ in
(clear_locals ξ) ⦇ data := data, dip := dip ⦈⟧
call(PNewPkt)"

abbreviation RREQ
where
"RREQ args ≡
⟦ξ. let (hops, rreqid, dip, dsn, dsk, oip, osn, sip, handled) = args ξ in
(clear_locals ξ) ⦇ hops := hops, rreqid := rreqid, dip := dip,
dsn := dsn, dsk := dsk, oip := oip,
osn := osn, sip := sip, handled := handled ⦈⟧
call(PRreq)"

abbreviation RREP
where
"RREP args ≡
⟦ξ. let (hops, dip, dsn, oip, sip) = args ξ in
(clear_locals ξ) ⦇ hops := hops, dip := dip, dsn := dsn,
oip := oip, sip := sip ⦈⟧
call(PRrep)"

abbreviation RERR
where
"RERR args ≡
⟦ξ. let (dests, sip) = args ξ in
(clear_locals ξ) ⦇ dests := dests, sip := sip ⦈⟧
call(PRerr)"

fun Γ⇩A⇩O⇩D⇩V :: "(state, msg, pseqp, pseqp label) seqp_env"
where
"Γ⇩A⇩O⇩D⇩V PAodv = labelled PAodv (
receive(λmsg' ξ. ξ ⦇ msg := msg' ⦈).
(    ⟨is_newpkt⟩ NEWPKT(λξ. (data ξ, ip ξ))
⊕ ⟨is_pkt⟩ PKT(λξ. (data ξ, dip ξ, oip ξ))
⊕ ⟨is_rreq⟩
⟦ξ. ξ ⦇rt := update (rt ξ) (sip ξ) (0, unk, val, 1, sip ξ, {}) ⦈⟧
RREQ(λξ. (hops ξ, rreqid ξ, dip ξ, dsn ξ, dsk ξ, oip ξ, osn ξ, sip ξ, handled ξ))
⊕ ⟨is_rrep⟩
⟦ξ. ξ ⦇rt := update (rt ξ) (sip ξ) (0, unk, val, 1, sip ξ, {}) ⦈⟧
RREP(λξ. (hops ξ, dip ξ, dsn ξ, oip ξ, sip ξ))
⊕ ⟨is_rerr⟩
⟦ξ. ξ ⦇rt := update (rt ξ) (sip ξ) (0, unk, val, 1, sip ξ, {}) ⦈⟧
RERR(λξ. (dests ξ, sip ξ))
)
⊕ ⟨λξ. { ξ⦇ dip := dip ⦈ | dip. dip ∈ qD(store ξ) ∩ vD(rt ξ) }⟩
⟦ξ. ξ ⦇ data := hd(σ⇘queue⇙(store ξ, dip ξ)) ⦈⟧
unicast(λξ. the (nhop (rt ξ) (dip ξ)), λξ. pkt(data ξ, dip ξ, ip ξ)).
⟦ξ. ξ ⦇ store := the (drop (dip ξ) (store ξ)) ⦈⟧
AODV()
▹ ⟦ξ. ξ ⦇ dests := (λrip. if (rip ∈ vD (rt ξ) ∧ nhop (rt ξ) rip = nhop (rt ξ) (dip ξ))
then Some (inc (sqn (rt ξ) rip)) else None) ⦈⟧
⟦ξ. ξ ⦇ rt := invalidate (rt ξ) (dests ξ) ⦈⟧
⟦ξ. ξ ⦇ store := setRRF (store ξ) (dests ξ)⦈⟧
⟦ξ. ξ ⦇ pre := ⋃{ the (precs (rt ξ) rip) | rip. rip ∈ dom (dests ξ) } ⦈⟧
⟦ξ. ξ ⦇ dests := (λrip. if ((dests ξ) rip ≠ None ∧ the (precs (rt ξ) rip) ≠ {})
then (dests ξ) rip else None) ⦈⟧
groupcast(λξ. pre ξ, λξ. rerr(dests ξ, ip ξ)). AODV()
⊕ ⟨λξ. { ξ⦇ dip := dip ⦈
| dip. dip ∈ qD(store ξ) - vD(rt ξ) ∧ the (σ⇘p-flag⇙(store ξ, dip)) = req }⟩
⟦ξ. ξ ⦇ store := unsetRRF (store ξ) (dip ξ) ⦈⟧
⟦ξ. ξ ⦇ sn := inc (sn ξ) ⦈⟧
⟦ξ. ξ ⦇ rreqid := nrreqid (rreqs ξ) (ip ξ) ⦈⟧
⟦ξ. ξ ⦇ rreqs := rreqs ξ ∪ {(ip ξ, rreqid ξ)} ⦈⟧
broadcast(λξ. rreq(0, rreqid ξ, dip ξ, sqn (rt ξ) (dip ξ), sqnf (rt ξ) (dip ξ), ip ξ, sn ξ,
ip ξ, False)). AODV())"

|  "Γ⇩A⇩O⇩D⇩V PNewPkt = labelled PNewPkt (
⟨ξ. dip ξ = ip ξ⟩
deliver(λξ. data ξ).AODV()
⊕ ⟨ξ. dip ξ ≠ ip ξ⟩
⟦ξ. ξ ⦇ store := add (data ξ) (dip ξ) (store ξ) ⦈⟧
AODV())"

| "Γ⇩A⇩O⇩D⇩V PPkt = labelled PPkt (
⟨ξ. dip ξ = ip ξ⟩
deliver(λξ. data ξ).AODV()
⊕ ⟨ξ. dip ξ ≠ ip ξ⟩
(
⟨ξ. dip ξ ∈ vD (rt ξ)⟩
unicast(λξ. the (nhop (rt ξ) (dip ξ)), λξ. pkt(data ξ, dip ξ, oip ξ)).AODV()
▹
⟦ξ. ξ ⦇ dests := (λrip. if (rip ∈ vD (rt ξ) ∧ nhop (rt ξ) rip = nhop (rt ξ) (dip ξ))
then Some (inc (sqn (rt ξ) rip)) else None) ⦈⟧
⟦ξ. ξ ⦇ rt := invalidate (rt ξ) (dests ξ) ⦈⟧
⟦ξ. ξ ⦇ store := setRRF (store ξ) (dests ξ)⦈⟧
⟦ξ. ξ ⦇ pre := ⋃{ the (precs (rt ξ) rip) | rip. rip ∈ dom (dests ξ) } ⦈⟧
⟦ξ. ξ ⦇ dests := (λrip. if ((dests ξ) rip ≠ None ∧ the (precs (rt ξ) rip) ≠ {})
then (dests ξ) rip else None) ⦈⟧
groupcast(λξ. pre ξ, λξ. rerr(dests ξ, ip ξ)).AODV()
⊕ ⟨ξ. dip ξ ∉ vD (rt ξ)⟩
(
⟨ξ. dip ξ ∈ iD (rt ξ)⟩
groupcast(λξ. the (precs (rt ξ) (dip ξ)), λξ. rerr([dip ξ ↦ sqn (rt ξ) (dip ξ)],
ip ξ)).AODV()
⊕ ⟨ξ. dip ξ ∉ iD (rt ξ)⟩
AODV()
)
))"

| "Γ⇩A⇩O⇩D⇩V PRreq = labelled PRreq (
⟨ξ. (oip ξ, rreqid ξ) ∈ rreqs ξ⟩
AODV()
⊕ ⟨ξ. (oip ξ, rreqid ξ) ∉ rreqs ξ⟩
⟦ξ. ξ ⦇ rt := update (rt ξ) (oip ξ) (osn ξ, kno, val, hops ξ + 1, sip ξ, {}) ⦈⟧
⟦ξ. ξ ⦇ rreqs := rreqs ξ ∪ {(oip ξ, rreqid ξ)} ⦈⟧
(
⟨ξ. handled ξ = False⟩
(
⟨ξ. dip ξ = ip ξ⟩
⟦ξ. ξ ⦇ sn := max (sn ξ) (dsn ξ) ⦈⟧
unicast(λξ. the (nhop (rt ξ) (oip ξ)), λξ. rrep(0, dip ξ, sn ξ, oip ξ, ip ξ)).
broadcast(λξ. rreq(hops ξ + 1, rreqid ξ, dip ξ, dsn ξ, dsk ξ, oip ξ, osn ξ, ip ξ, True)).
AODV()
▹
⟦ξ. ξ ⦇ dests := (λrip. if (rip ∈ vD (rt ξ) ∧ nhop (rt ξ) rip = nhop (rt ξ) (oip ξ))
then Some (inc (sqn (rt ξ) rip)) else None) ⦈⟧
⟦ξ. ξ ⦇ rt := invalidate (rt ξ) (dests ξ) ⦈⟧
⟦ξ. ξ ⦇ store := setRRF (store ξ) (dests ξ)⦈⟧
⟦ξ. ξ ⦇ pre := ⋃{ the (precs (rt ξ) rip) | rip. rip ∈ dom (dests ξ) } ⦈⟧
⟦ξ. ξ ⦇ dests := (λrip. if ((dests ξ) rip ≠ None ∧ the (precs (rt ξ) rip) ≠ {})
then (dests ξ) rip else None) ⦈⟧
groupcast(λξ. pre ξ, λξ. rerr(dests ξ, ip ξ)).AODV()
⊕ ⟨ξ. dip ξ ≠ ip ξ⟩
(
⟨ξ. dip ξ ∈ vD (rt ξ) ∧ dsn ξ ≤ sqn (rt ξ) (dip ξ) ∧ sqnf (rt ξ) (dip ξ) = kno⟩
⟦ξ. ξ ⦇ rt := the (addpreRT (rt ξ) (dip ξ) {sip ξ}) ⦈⟧
⟦ξ. ξ ⦇ rt := the (addpreRT (rt ξ) (oip ξ) {the (nhop (rt ξ) (dip ξ))}) ⦈⟧
unicast(λξ. the (nhop (rt ξ) (oip ξ)), λξ. rrep(the (dhops (rt ξ) (dip ξ)), dip ξ,
sqn (rt ξ) (dip ξ), oip ξ, ip ξ)).
broadcast(λξ. rreq(hops ξ + 1, rreqid ξ, dip ξ, dsn ξ,
dsk ξ, oip ξ, osn ξ, ip ξ, True)).
AODV()
▹
⟦ξ. ξ ⦇ dests := (λrip. if (rip ∈ vD (rt ξ) ∧ nhop (rt ξ) rip = nhop (rt ξ) (oip ξ))
then Some (inc (sqn (rt ξ) rip)) else None) ⦈⟧
⟦ξ. ξ ⦇ rt := invalidate (rt ξ) (dests ξ) ⦈⟧
⟦ξ. ξ ⦇ store := setRRF (store ξ) (dests ξ)⦈⟧
⟦ξ. ξ ⦇ pre := ⋃{ the (precs (rt ξ) rip) | rip. rip ∈ dom (dests ξ) } ⦈⟧
⟦ξ. ξ ⦇ dests := (λrip. if ((dests ξ) rip ≠ None ∧ the (precs (rt ξ) rip) ≠ {})
then (dests ξ) rip else None) ⦈⟧
groupcast(λξ. pre ξ, λξ. rerr(dests ξ, ip ξ)).AODV()
⊕ ⟨ξ. dip ξ ∉ vD (rt ξ) ∨ sqn (rt ξ) (dip ξ) < dsn ξ ∨ sqnf (rt ξ) (dip ξ) = unk⟩
broadcast(λξ. rreq(hops ξ + 1, rreqid ξ, dip ξ, max (sqn (rt ξ) (dip ξ)) (dsn ξ),
dsk ξ, oip ξ, osn ξ, ip ξ, False)).
AODV()
)
)
⊕ ⟨ξ. handled ξ = True⟩
broadcast(λξ. rreq(hops ξ + 1, rreqid ξ, dip ξ, dsn ξ, dsk ξ, oip ξ, osn ξ, ip ξ, True)).
AODV()
))"

| "Γ⇩A⇩O⇩D⇩V PRrep = labelled PRrep (
⟨ξ. rt ξ ≠ update (rt ξ) (dip ξ) (dsn ξ, kno, val, hops ξ + 1, sip ξ, {}) ⟩
(
⟦ξ. ξ ⦇ rt := update (rt ξ) (dip ξ) (dsn ξ, kno, val, hops ξ + 1, sip ξ, {}) ⦈ ⟧
(
⟨ξ. oip ξ = ip ξ ⟩
AODV()
⊕ ⟨ξ. oip ξ ≠ ip ξ ⟩
(
⟨ξ. oip ξ ∈ vD (rt ξ)⟩
⟦ξ. ξ ⦇ rt := the (addpreRT (rt ξ) (dip ξ) {the (nhop (rt ξ) (oip ξ))}) ⦈⟧
⟦ξ. ξ ⦇ rt := the (addpreRT (rt ξ) (the (nhop (rt ξ) (dip ξ)))
{the (nhop (rt ξ) (oip ξ))}) ⦈⟧
unicast(λξ. the (nhop (rt ξ) (oip ξ)), λξ. rrep(hops ξ + 1, dip ξ, dsn ξ, oip ξ, ip ξ)).
AODV()
▹
⟦ξ. ξ ⦇ dests := (λrip. if (rip ∈ vD (rt ξ) ∧ nhop (rt ξ) rip = nhop (rt ξ) (oip ξ))
then Some (inc (sqn (rt ξ) rip)) else None) ⦈⟧
⟦ξ. ξ ⦇ rt := invalidate (rt ξ) (dests ξ) ⦈⟧
⟦ξ. ξ ⦇ store := setRRF (store ξ) (dests ξ)⦈⟧
⟦ξ. ξ ⦇ pre := ⋃{ the (precs (rt ξ) rip) | rip. rip ∈ dom (dests ξ) } ⦈⟧
⟦ξ. ξ ⦇ dests := (λrip. if ((dests ξ) rip ≠ None ∧ the (precs (rt ξ) rip) ≠ {})
then (dests ξ) rip else None) ⦈⟧
groupcast(λξ. pre ξ, λξ. rerr(dests ξ, ip ξ)).AODV()
⊕ ⟨ξ. oip ξ ∉ vD (rt ξ)⟩
AODV()
)
)
)
⊕ ⟨ξ. rt ξ = update (rt ξ) (dip ξ) (dsn ξ, kno, val, hops ξ + 1, sip ξ, {}) ⟩
AODV()
)"

| "Γ⇩A⇩O⇩D⇩V PRerr = labelled PRerr (
⟦ξ. ξ ⦇ dests := (λrip. case (dests ξ) rip of None ⇒ None
| Some rsn ⇒ if rip ∈ vD (rt ξ) ∧ the (nhop (rt ξ) rip) = sip ξ
∧ sqn (rt ξ) rip < rsn then Some rsn else None) ⦈⟧
⟦ξ. ξ ⦇ rt := invalidate (rt ξ) (dests ξ) ⦈⟧
⟦ξ. ξ ⦇ store := setRRF (store ξ) (dests ξ)⦈⟧
⟦ξ. ξ ⦇ pre := ⋃{ the (precs (rt ξ) rip) | rip. rip ∈ dom (dests ξ) } ⦈⟧
⟦ξ. ξ ⦇ dests := (λrip. if ((dests ξ) rip ≠ None ∧ the (precs (rt ξ) rip) ≠ {})
then (dests ξ) rip else None) ⦈⟧
groupcast(λξ. pre ξ, λξ. rerr(dests ξ, ip ξ)). AODV())"

declare Γ⇩A⇩O⇩D⇩V.simps [simp del, code del]
lemmas Γ⇩A⇩O⇩D⇩V_simps [simp, code] = Γ⇩A⇩O⇩D⇩V.simps [simplified]

fun Γ⇩A⇩O⇩D⇩V_skeleton
where
"Γ⇩A⇩O⇩D⇩V_skeleton PAodv   = seqp_skeleton (Γ⇩A⇩O⇩D⇩V PAodv)"
| "Γ⇩A⇩O⇩D⇩V_skeleton PNewPkt = seqp_skeleton (Γ⇩A⇩O⇩D⇩V PNewPkt)"
| "Γ⇩A⇩O⇩D⇩V_skeleton PPkt    = seqp_skeleton (Γ⇩A⇩O⇩D⇩V PPkt)"
| "Γ⇩A⇩O⇩D⇩V_skeleton PRreq   = seqp_skeleton (Γ⇩A⇩O⇩D⇩V PRreq)"
| "Γ⇩A⇩O⇩D⇩V_skeleton PRrep   = seqp_skeleton (Γ⇩A⇩O⇩D⇩V PRrep)"
| "Γ⇩A⇩O⇩D⇩V_skeleton PRerr   = seqp_skeleton (Γ⇩A⇩O⇩D⇩V PRerr)"

lemma Γ⇩A⇩O⇩D⇩V_skeleton_wf [simp]:
"wellformed Γ⇩A⇩O⇩D⇩V_skeleton"
proof (rule, intro allI)
fix pn pn'
show "call(pn') ∉ stermsl (Γ⇩A⇩O⇩D⇩V_skeleton pn)"
by (cases pn) simp_all
qed

declare Γ⇩A⇩O⇩D⇩V_skeleton.simps [simp del, code del]
lemmas Γ⇩A⇩O⇩D⇩V_skeleton_simps [simp, code]
= Γ⇩A⇩O⇩D⇩V_skeleton.simps [simplified Γ⇩A⇩O⇩D⇩V_simps seqp_skeleton.simps]

lemma aodv_proc_cases [dest]:
fixes p pn
shows "p ∈ ctermsl (Γ⇩A⇩O⇩D⇩V pn) ⟹
(p ∈ ctermsl (Γ⇩A⇩O⇩D⇩V PAodv) ∨
p ∈ ctermsl (Γ⇩A⇩O⇩D⇩V PNewPkt)  ∨
p ∈ ctermsl (Γ⇩A⇩O⇩D⇩V PPkt)  ∨
p ∈ ctermsl (Γ⇩A⇩O⇩D⇩V PRreq) ∨
p ∈ ctermsl (Γ⇩A⇩O⇩D⇩V PRrep) ∨
p ∈ ctermsl (Γ⇩A⇩O⇩D⇩V PRerr))"
by (cases pn) simp_all

definition σ⇩A⇩O⇩D⇩V :: "ip ⇒ (state × (state, msg, pseqp, pseqp label) seqp) set"
where "σ⇩A⇩O⇩D⇩V i ≡ {(aodv_init i, Γ⇩A⇩O⇩D⇩V PAodv)}"

abbreviation paodv
:: "ip ⇒ (state × (state, msg, pseqp, pseqp label) seqp, msg seq_action) automaton"
where
"paodv i ≡ ⦇ init = σ⇩A⇩O⇩D⇩V i, trans = seqp_sos Γ⇩A⇩O⇩D⇩V ⦈"

lemma aodv_trans: "trans (paodv i) = seqp_sos Γ⇩A⇩O⇩D⇩V"
by simp

lemma aodv_control_within [simp]: "control_within Γ⇩A⇩O⇩D⇩V (init (paodv i))"
unfolding σ⇩A⇩O⇩D⇩V_def by (rule control_withinI) (auto simp del: Γ⇩A⇩O⇩D⇩V_simps)

lemma aodv_wf [simp]:
"wellformed Γ⇩A⇩O⇩D⇩V"
proof (rule, intro allI)
fix pn pn'
show "call(pn') ∉ stermsl (Γ⇩A⇩O⇩D⇩V pn)"
by (cases pn) simp_all
qed

lemmas aodv_labels_not_empty [simp] = labels_not_empty [OF aodv_wf]

lemma aodv_ex_label [intro]: "∃l. l∈labels Γ⇩A⇩O⇩D⇩V p"
by (metis aodv_labels_not_empty all_not_in_conv)

lemma aodv_ex_labelE [elim]:
assumes "∀l∈labels Γ⇩A⇩O⇩D⇩V p. P l p"
and "∃p l. P l p ⟹ Q"
shows "Q"
using assms by (metis aodv_ex_label)

lemma aodv_simple_labels [simp]: "simple_labels Γ⇩A⇩O⇩D⇩V"
proof
fix pn p
assume "p∈subterms(Γ⇩A⇩O⇩D⇩V pn)"
thus "∃!l. labels Γ⇩A⇩O⇩D⇩V p = {l}"
by (cases pn) (simp_all cong: seqp_congs | elim disjE)+
qed

lemma σ⇩A⇩O⇩D⇩V_labels [simp]: "(ξ, p) ∈ σ⇩A⇩O⇩D⇩V i ⟹  labels Γ⇩A⇩O⇩D⇩V p = {PAodv-:0}"
unfolding σ⇩A⇩O⇩D⇩V_def by simp

lemma aodv_init_kD_empty [simp]:
"(ξ, p) ∈ σ⇩A⇩O⇩D⇩V i ⟹ kD (rt ξ) = {}"
unfolding σ⇩A⇩O⇩D⇩V_def kD_def by simp

lemma aodv_init_sip_not_ip [simp]: "¬(sip (aodv_init i) = i)" by simp

lemma aodv_init_sip_not_ip' [simp]:
assumes "(ξ, p) ∈ σ⇩A⇩O⇩D⇩V i"
shows "sip ξ ≠ ip ξ"
using assms unfolding σ⇩A⇩O⇩D⇩V_def by simp

lemma aodv_init_sip_not_i [simp]:
assumes "(ξ, p) ∈ σ⇩A⇩O⇩D⇩V i"
shows "sip ξ ≠ i"
using assms unfolding σ⇩A⇩O⇩D⇩V_def by simp

lemma clear_locals_sip_not_ip':
assumes "ip ξ = i"
shows "¬(sip (clear_locals ξ) = i)"
using assms by auto

text ‹Stop the simplifier from descending into process terms.›
declare seqp_congs [cong]

text ‹Configure the main invariant tactic for AODV.›

declare
Γ⇩A⇩O⇩D⇩V_simps [cterms_env]
aodv_proc_cases [ctermsl_cases]
seq_invariant_ctermsI [OF aodv_wf aodv_control_within aodv_simple_labels aodv_trans,
cterms_intros]
seq_step_invariant_ctermsI [OF aodv_wf aodv_control_within aodv_simple_labels aodv_trans,
cterms_intros]

end
```