# Theory A_Aodv_Data

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

section "Predicates and functions used in the AODV model"

theory A_Aodv_Data
imports A_Norreqid
begin

subsection "Sequence Numbers"

text ‹Sequence numbers approximate the relative freshness of routing information.›

definition inc :: "sqn ⇒ sqn"
where "inc sn ≡ if sn = 0 then sn else sn + 1"

lemma less_than_inc [simp]: "x ≤ inc x"
unfolding inc_def by simp

lemma inc_minus_suc_0 [simp]:
"inc x - Suc 0 = x"
unfolding inc_def by simp

lemma inc_never_one' [simp, intro]: "inc x ≠ Suc 0"
unfolding inc_def by simp

lemma inc_never_one [simp, intro]: "inc x ≠ 1"
by simp

subsection "Modelling Routes"

text ‹
A route is a 6-tuple, @{term "(dsn, dsk, flag, hops, nhip, pre)"} where
@{term dsn} is the destination sequence number', @{term dsk} is the
destination-sequence-number status', @{term flag} is the route status,
@{term hops} is the number of hops to the destination, @{term nhip} is the
next hop toward the destination, and @{term pre} is the set of precursor nodes'--those
interested in hearing about changes to the route.
›

type_synonym r = "sqn × k × f × nat × ip × ip set"

definition proj2 :: "r ⇒ sqn" ("π⇩2")
where "π⇩2 ≡ λ(dsn, _, _, _, _, _). dsn"

definition proj3 :: "r ⇒ k" ("π⇩3")
where "π⇩3 ≡ λ(_, dsk, _, _, _, _). dsk"

definition proj4 :: "r ⇒ f" ("π⇩4")
where "π⇩4 ≡ λ(_, _, flag, _, _, _). flag"

definition proj5 :: "r ⇒ nat" ("π⇩5")
where "π⇩5 ≡ λ(_, _, _, hops, _, _). hops"

definition proj6 :: "r ⇒ ip" ("π⇩6")
where "π⇩6 ≡ λ(_, _, _, _, nhip, _). nhip"

definition proj7 :: "r ⇒ ip set" ("π⇩7")
where "π⇩7 ≡ λ(_, _, _, _, _, pre). pre"

lemma projs [simp]:
"π⇩2(dsn, dsk, flag, hops, nhip, pre) = dsn"
"π⇩3(dsn, dsk, flag, hops, nhip, pre) = dsk"
"π⇩4(dsn, dsk, flag, hops, nhip, pre) = flag"
"π⇩5(dsn, dsk, flag, hops, nhip, pre) = hops"
"π⇩6(dsn, dsk, flag, hops, nhip, pre) = nhip"
"π⇩7(dsn, dsk, flag, hops, nhip, pre) = pre"
by (clarsimp simp: proj2_def proj3_def proj4_def
proj5_def proj6_def proj7_def)+

lemma proj3_pred [intro]: "⟦ P kno; P unk ⟧ ⟹ P (π⇩3 x)"
by (rule k.induct)

lemma proj4_pred [intro]: "⟦ P val; P inv ⟧ ⟹ P (π⇩4 x)"
by (rule f.induct)

lemma proj6_pair_snd [simp]:
fixes dsn' r
shows "π⇩6 (dsn', snd (r)) = π⇩6(r)"
by (cases r) simp

subsection "Routing Tables"

text ‹Routing tables map ip addresses to route entries.›

type_synonym rt = "ip ⇀ r"

syntax
"_Sigma_route" :: "rt ⇒ ip ⇀ r"  ("σ⇘route⇙'(_, _')")

translations
"σ⇘route⇙(rt, dip)" => "rt dip"

definition sqn :: "rt ⇒ ip ⇒ sqn"
where "sqn rt dip ≡ case σ⇘route⇙(rt, dip) of Some r ⇒ π⇩2(r) | None ⇒ 0"

definition sqnf :: "rt ⇒ ip ⇒ k"
where "sqnf rt dip ≡ case σ⇘route⇙(rt, dip) of Some r ⇒ π⇩3(r) | None ⇒ unk"

abbreviation flag :: "rt ⇒ ip ⇀ f"
where "flag rt dip ≡ map_option π⇩4 (σ⇘route⇙(rt, dip))"

abbreviation dhops :: "rt ⇒ ip ⇀ nat"
where "dhops rt dip ≡ map_option π⇩5 (σ⇘route⇙(rt, dip))"

abbreviation nhop :: "rt ⇒ ip ⇀ ip"
where "nhop rt dip ≡ map_option π⇩6 (σ⇘route⇙(rt, dip))"

abbreviation precs :: "rt ⇒ ip ⇀ ip set"
where "precs rt dip ≡ map_option π⇩7 (σ⇘route⇙(rt, dip))"

definition vD :: "rt ⇒ ip set"
where "vD rt ≡ {dip. flag rt dip = Some val}"

definition iD :: "rt ⇒ ip set"
where "iD rt ≡ {dip. flag rt dip = Some inv}"

definition kD :: "rt ⇒ ip set"
where "kD rt ≡ {dip. rt dip ≠ None}"

lemma kD_is_vD_and_iD: "kD rt = vD rt ∪ iD rt"
unfolding kD_def vD_def iD_def by auto

lemma vD_iD_gives_kD [simp]:
"⋀ip rt. ip ∈ vD rt ⟹ ip ∈ kD rt"
"⋀ip rt. ip ∈ iD rt ⟹ ip ∈ kD rt"
unfolding kD_is_vD_and_iD by simp_all

lemma kD_Some [dest]:
fixes dip rt
assumes "dip ∈ kD rt"
shows "∃dsn dsk flag hops nhip pre.
σ⇘route⇙(rt, dip) = Some (dsn, dsk, flag, hops, nhip, pre)"
using assms unfolding kD_def by simp

lemma kD_None [dest]:
fixes dip rt
assumes "dip ∉ kD rt"
shows "σ⇘route⇙(rt, dip) = None"
using assms unfolding kD_def
by (metis (mono_tags) mem_Collect_eq)

lemma vD_Some [dest]:
fixes dip rt
assumes "dip ∈ vD rt"
shows "∃dsn dsk hops nhip pre.
σ⇘route⇙(rt, dip) = Some (dsn, dsk, val, hops, nhip, pre)"
using assms unfolding vD_def by simp

lemma vD_empty [simp]: "vD Map.empty = {}"
unfolding vD_def by simp

lemma iD_Some [dest]:
fixes dip rt
assumes "dip ∈ iD rt"
shows "∃dsn dsk hops nhip pre.
σ⇘route⇙(rt, dip) = Some (dsn, dsk, inv, hops, nhip, pre)"
using assms unfolding iD_def by simp

lemma val_is_vD [elim]:
fixes ip rt
assumes "ip∈kD(rt)"
and "the (flag rt ip) = val"
shows "ip∈vD(rt)"
using assms unfolding vD_def by auto

lemma inv_is_iD [elim]:
fixes ip rt
assumes "ip∈kD(rt)"
and "the (flag rt ip) = inv"
shows "ip∈iD(rt)"
using assms unfolding iD_def by auto

lemma iD_flag_is_inv [elim, simp]:
fixes ip rt
assumes "ip∈iD(rt)"
shows "the (flag rt ip) = inv"
proof -
from ‹ip∈iD(rt)› have "ip∈kD(rt)" by auto
with assms show ?thesis unfolding iD_def by auto
qed

lemma kD_but_not_vD_is_iD [elim]:
fixes ip rt
assumes "ip∈kD(rt)"
and "ip∉vD(rt)"
shows "ip∈iD(rt)"
proof -
from ‹ip∈kD(rt)› obtain dsn dsk f hops nhop pre
where rtip: "rt ip = Some (dsn, dsk, f, hops, nhop, pre)"
by (metis kD_Some)
from ‹ip∉vD(rt)› have "f ≠ val"
proof (rule contrapos_nn)
assume "f = val"
with rtip have "the (flag rt ip) = val" by simp
with ‹ip∈kD(rt)› show "ip∈vD(rt)" ..
qed
with rtip have "the (flag rt ip)= inv" by simp
with ‹ip∈kD(rt)› show "ip∈iD(rt)" ..
qed

lemma vD_or_iD [elim]:
fixes ip rt
assumes "ip∈kD(rt)"
and "ip∈vD(rt) ⟹ P rt ip"
and "ip∈iD(rt) ⟹ P rt ip"
shows "P rt ip"
proof -
from ‹ip∈kD(rt)› have "ip∈vD(rt) ∪ iD(rt)"
thus ?thesis by (auto elim: assms(2-3))
qed

lemma proj5_eq_dhops: "⋀dip rt. dip∈kD(rt) ⟹ π⇩5(the (rt dip)) = the (dhops rt dip)"
unfolding sqn_def by (drule kD_Some) clarsimp

lemma proj4_eq_flag: "⋀dip rt. dip∈kD(rt) ⟹ π⇩4(the (rt dip)) = the (flag rt dip)"
unfolding sqn_def by (drule kD_Some) clarsimp

lemma proj2_eq_sqn: "⋀dip rt. dip∈kD(rt) ⟹ π⇩2(the (rt dip)) = sqn rt dip"
unfolding sqn_def by (drule kD_Some) clarsimp

lemma kD_sqnf_is_proj3 [simp]:
"⋀ip rt. ip∈kD(rt) ⟹ sqnf rt ip = π⇩3(the (rt ip))"
unfolding sqnf_def by auto

lemma vD_flag_val [simp]:
"⋀dip rt. dip ∈ vD (rt) ⟹ the (flag rt dip) = val"
unfolding vD_def by clarsimp

lemma kD_update [simp]:
"⋀rt nip v. kD (rt(nip ↦ v)) = insert nip (kD rt)"
unfolding kD_def by auto

lemma kD_empty [simp]: "kD Map.empty = {}"
unfolding kD_def by simp

lemma ip_equal_or_known [elim]:
fixes rt ip ip'
assumes "ip = ip' ∨ ip∈kD(rt)"
and "ip = ip' ⟹ P rt ip ip'"
and "⟦ ip ≠ ip'; ip∈kD(rt)⟧ ⟹ P rt ip ip'"
shows "P rt ip ip'"
using assms by auto

subsection "Updating Routing Tables"

text ‹Routing table entries are modified through explicit functions.
The properties of these functions are important in invariant proofs.›

subsubsection "Updating Precursor Lists"

definition addpre :: "r ⇒ ip set ⇒ r"
where "addpre r npre ≡ let (dsn, dsk, flag, hops, nhip, pre) = r in
(dsn, dsk, flag, hops, nhip, pre ∪ npre)"

fixes v pre
shows "π⇩2(addpre v pre) = π⇩2(v)"
unfolding addpre_def by (cases v) simp

fixes v pre
shows "π⇩3(addpre v pre) = π⇩3(v)"
unfolding addpre_def by (cases v) simp

fixes v pre
shows "π⇩4(addpre v pre) = π⇩4(v)"
unfolding addpre_def by (cases v) simp

fixes v pre
shows "π⇩5(addpre v pre) = π⇩5(v)"
unfolding addpre_def by (cases v) simp

fixes dsn dsk flag hops nhip pre npre
shows "π⇩6(addpre v npre) = π⇩6(v)"
unfolding addpre_def by (cases v) simp

fixes dsn dsk flag hops nhip pre npre
shows "π⇩7(addpre v npre) = π⇩7(v) ∪ npre"
unfolding addpre_def by (cases v) simp

"addpre (dsn, dsk, fl, hops, nhip, pre) npre = (dsn, dsk, fl, hops, nhip, pre ∪ npre)"

definition addpreRT :: "rt ⇒ ip ⇒ ip set ⇀ rt"
where "addpreRT rt dip npre ≡
map_option (λs. rt (dip ↦ addpre s npre)) (σ⇘route⇙(rt, dip))"

"⋀dsn dsn' v pre. (dsn, snd(addpre (dsn', v) pre)) = addpre (dsn, v) pre"

fixes ip rt ip' npre
assumes "ip∈kD rt"
and "ip'∈kD rt"
shows "π⇩2(the (the (addpreRT rt ip' npre) ip)) = π⇩2(the (rt ip))"
using assms [THEN kD_Some] unfolding addpreRT_def by clarsimp

fixes ip rt ip' npre
assumes "ip∈kD rt"
and "ip'∈kD rt"
shows "π⇩3(the (the (addpreRT rt ip' npre) ip)) = π⇩3(the (rt ip))"
using assms [THEN kD_Some] unfolding addpreRT_def by clarsimp

"⋀rt dip ip npre. dip∈kD(rt) ⟹ π⇩5(the (the (addpreRT rt dip npre) ip)) = π⇩5(the (rt ip))"

fixes rt pre ip dip
assumes "dip ∈ kD rt"
shows "flag (the (addpreRT rt dip pre)) ip = flag rt ip"
using assms [THEN kD_Some] by (clarsimp)

fixes rt dip npre
assumes "dip ∈ kD rt"
shows "kD (the (addpreRT rt dip npre)) = kD rt"
using assms [THEN kD_Some]
by clarsimp blast

fixes rt dip npre
assumes "dip ∈ kD rt"
shows "vD (the (addpreRT rt dip npre)) = vD rt"
using assms [THEN kD_Some] by clarsimp auto

fixes rt dip npre
assumes "dip ∈ kD rt"
shows "iD (the (addpreRT rt dip npre)) = iD rt"
using assms [THEN kD_Some] by clarsimp auto

fixes rt pre ip dip
assumes "dip ∈ kD rt"
shows "nhop (the (addpreRT rt dip pre)) ip = nhop rt ip"
using assms [THEN kD_Some] by (clarsimp)

fixes rt pre ip dip
assumes "dip ∈ kD rt"
shows "sqn (the (addpreRT rt dip pre)) ip = sqn rt ip"
using assms [THEN kD_Some] by (clarsimp)

fixes rt pre ip dip
assumes "dip ∈ kD rt"
shows "dhops (the (addpreRT rt dip pre)) ip = dhops rt ip"
using assms [THEN kD_Some] by (clarsimp)

"⋀ip dip. ip∈kD(rt ξ) ⟹ sqnf (the (addpreRT (rt ξ) ip npre)) dip = sqnf (rt ξ) dip"

subsubsection "Updating route entries"

lemma in_kD_case [simp]:
fixes dip rt
assumes "dip ∈ kD(rt)"
shows "(case rt dip of None ⇒ en | Some r ⇒ es r) = es (the (rt dip))"
using assms [THEN kD_Some] by auto

lemma not_in_kD_case [simp]:
fixes dip rt
assumes "dip ∉ kD(rt)"
shows "(case rt dip of None ⇒ en | Some r ⇒ es r) = en"
using assms [THEN kD_None] by auto

lemma rt_Some_sqn [dest]:
fixes rt and ip dsn dsk flag hops nhip pre
assumes "rt ip = Some (dsn, dsk, flag, hops, nhip, pre)"
shows "sqn rt ip = dsn"
unfolding sqn_def using assms by simp

lemma not_kD_sqn [simp]:
fixes dip rt
assumes "dip ∉ kD(rt)"
shows "sqn rt dip = 0"
using assms unfolding sqn_def
by simp

definition update_arg_wf :: "r ⇒ bool"
where "update_arg_wf r ≡ π⇩4(r) = val ∧
(π⇩2(r) = 0) = (π⇩3(r) = unk) ∧
(π⇩3(r) = unk ⟶ π⇩5(r) = 1)"

lemma update_arg_wf_gives_cases:
"⋀r. update_arg_wf r ⟹ (π⇩2(r) = 0) = (π⇩3(r) = unk)"
unfolding update_arg_wf_def by simp

lemma update_arg_wf_tuples [simp]:
"⋀nhip pre. update_arg_wf (0, unk, val, Suc 0, nhip, pre)"
"⋀n hops nhip pre. update_arg_wf (Suc n, kno, val, hops,  nhip, pre)"
unfolding update_arg_wf_def by auto

lemma update_arg_wf_tuples' [elim]:
"⋀n hops nhip pre. Suc 0 ≤ n ⟹ update_arg_wf (n, kno, val, hops,  nhip, pre)"
unfolding update_arg_wf_def by auto

lemma wf_r_cases [intro]:
fixes P r
assumes "update_arg_wf r"
and c1: "⋀nhip pre. P (0, unk, val, Suc 0, nhip, pre)"
and c2: "⋀dsn hops nhip pre. dsn > 0 ⟹ P (dsn, kno, val, hops, nhip, pre)"
shows "P r"
proof -
obtain dsn dsk flag hops nhip pre
where *: "r = (dsn, dsk, flag, hops, nhip, pre)" by (cases r)
with ‹update_arg_wf r› have wf1: "flag = val"
and wf2: "(dsn = 0) = (dsk = unk)"
and wf3: "dsk = unk ⟶ (hops = 1)"
unfolding update_arg_wf_def by auto
have "P (dsn, dsk, flag, hops, nhip, pre)"
proof (cases dsk)
assume "dsk = unk"
moreover with wf2 wf3 have "dsn = 0" and "hops = Suc 0" by auto
ultimately show ?thesis using ‹flag = val› by simp (rule c1)
next
assume "dsk = kno"
moreover with wf2 have "dsn > 0" by simp
ultimately show ?thesis using ‹flag = val› by simp (rule c2)
qed
with * show "P r" by simp
qed

definition update :: "rt ⇒ ip ⇒ r ⇒ rt"
where
"update rt ip r ≡
case σ⇘route⇙(rt, ip) of
None ⇒ rt (ip ↦ r)
| Some s ⇒
if π⇩2(s) < π⇩2(r) then rt (ip ↦ addpre r (π⇩7(s)))
else if π⇩2(s) = π⇩2(r) ∧ (π⇩5(s) > π⇩5(r) ∨ π⇩4(s) = inv)
then rt (ip ↦ addpre r (π⇩7(s)))
else if π⇩3(r) = unk
then rt (ip ↦ (π⇩2(s), snd (addpre r (π⇩7(s)))))
else rt (ip ↦ addpre s (π⇩7(r)))"

lemma update_simps [simp]:
fixes r s nrt nr nr' ns rt ip
defines "s ≡ the σ⇘route⇙(rt, ip)"
and "nr ≡ addpre r (π⇩7(s))"
and "nr' ≡ (π⇩2(s), π⇩3(nr), π⇩4(nr), π⇩5(nr), π⇩6(nr), π⇩7(nr))"
and "ns ≡ addpre s (π⇩7(r))"
shows
"⟦ip ∉ kD(rt)⟧                            ⟹ update rt ip r = rt (ip ↦ r)"
"⟦ip ∈ kD(rt); sqn rt ip < π⇩2(r)⟧         ⟹ update rt ip r = rt (ip ↦ nr)"
"⟦ip ∈ kD(rt); sqn rt ip = π⇩2(r);
the (dhops rt ip) > π⇩5(r)⟧ ⟹ update rt ip r = rt (ip ↦ nr)"
"⟦ip ∈ kD(rt); sqn rt ip = π⇩2(r);
flag rt ip = Some inv⟧     ⟹ update rt ip r = rt (ip ↦ nr)"
"⟦ip ∈ kD(rt); π⇩3(r) = unk; (π⇩2(r) = 0) = (π⇩3(r) = unk)⟧  ⟹ update rt ip r = rt (ip ↦ nr')"
"⟦ip ∈ kD(rt); sqn rt ip ≥ π⇩2(r); π⇩3(r) = kno;
sqn rt ip = π⇩2(r) ⟹ the (dhops rt ip) ≤ π⇩5(r) ∧ the (flag rt ip) = val ⟧
⟹ update rt ip r = rt (ip ↦ ns)"
proof -
assume "ip∉kD(rt)"
hence "σ⇘route⇙(rt, ip) = None" ..
thus "update rt ip r = rt (ip ↦ r)"
unfolding update_def by simp
next
assume "ip ∈ kD(rt)"
and "sqn rt ip < π⇩2(r)"
from this(1) obtain dsn dsk fl hops nhip pre
where "rt ip = Some (dsn, dsk, fl, hops, nhip, pre)"
by (metis kD_Some)
with ‹sqn rt ip < π⇩2(r)› show "update rt ip r = rt (ip ↦ nr)"
unfolding update_def nr_def s_def by auto
next
assume "ip ∈ kD(rt)"
and "sqn rt ip = π⇩2(r)"
and "the (dhops rt ip) > π⇩5(r)"
from this(1) obtain dsn dsk fl hops nhip pre
where "rt ip = Some (dsn, dsk, fl, hops, nhip, pre)"
by (metis kD_Some)
with ‹sqn rt ip = π⇩2(r)› and ‹the (dhops rt ip) > π⇩5(r)›
show "update rt ip r = rt (ip ↦ nr)"
unfolding update_def nr_def s_def by auto
next
assume "ip ∈ kD(rt)"
and "sqn rt ip = π⇩2(r)"
and "flag rt ip = Some inv"
from this(1) obtain dsn dsk fl hops nhip pre
where "rt ip = Some (dsn, dsk, fl, hops, nhip, pre)"
by (metis kD_Some)
with ‹sqn rt ip = π⇩2(r)› and ‹flag rt ip = Some inv›
show "update rt ip r = rt (ip ↦ nr)"
unfolding update_def nr_def s_def by auto
next
assume "ip ∈ kD(rt)"
and "π⇩3(r) = unk"
and "(π⇩2(r) = 0) = (π⇩3(r) = unk)"
from this(1) obtain dsn dsk fl hops nhip pre
where "rt ip = Some (dsn, dsk, fl, hops, nhip, pre)"
by (metis kD_Some)
with ‹(π⇩2(r) = 0) = (π⇩3(r) = unk)› and ‹π⇩3(r) = unk›
show "update rt ip r = rt (ip ↦ nr')"
unfolding update_def nr'_def nr_def s_def
by (cases r) simp
next
assume "ip ∈ kD(rt)"
and otherassms: "sqn rt ip ≥ π⇩2(r)"
"π⇩3(r) = kno"
"sqn rt ip = π⇩2(r) ⟹ the (dhops rt ip) ≤ π⇩5(r) ∧ the (flag rt ip) = val"
from this(1) obtain dsn dsk fl hops nhip pre
where "rt ip = Some (dsn, dsk, fl, hops, nhip, pre)"
by (metis kD_Some)
with otherassms show "update rt ip r = rt (ip ↦ ns)"
unfolding update_def ns_def s_def by auto
qed

lemma update_cases [elim]:
assumes "(π⇩2(r) = 0) = (π⇩3(r) = unk)"
and c1: "⟦ip ∉ kD(rt)⟧ ⟹ P (rt (ip ↦ r))"

and c2: "⟦ip ∈ kD(rt); sqn rt ip < π⇩2(r)⟧
⟹ P (rt (ip ↦ addpre r (π⇩7(the σ⇘route⇙(rt, ip)))))"
and c3: "⟦ip ∈ kD(rt); sqn rt ip = π⇩2(r); the (dhops rt ip) > π⇩5(r)⟧
⟹ P (rt (ip ↦ addpre r (π⇩7(the σ⇘route⇙(rt, ip)))))"
and c4: "⟦ip ∈ kD(rt); sqn rt ip = π⇩2(r); the (flag rt ip) = inv⟧
⟹ P (rt (ip ↦ addpre r (π⇩7(the σ⇘route⇙(rt, ip)))))"
and c5: "⟦ip ∈ kD(rt); π⇩3(r) = unk⟧
⟹ P (rt (ip ↦ (π⇩2(the σ⇘route⇙(rt, ip)), π⇩3(r),
π⇩4(r), π⇩5(r), π⇩6(r), π⇩7(addpre r (π⇩7(the σ⇘route⇙(rt, ip)))))))"
and c6: "⟦ip ∈ kD(rt); sqn rt ip ≥ π⇩2(r); π⇩3(r) = kno;
sqn rt ip = π⇩2(r) ⟹ the (dhops rt ip) ≤ π⇩5(r) ∧ the (flag rt ip) = val⟧
⟹ P (rt (ip ↦ addpre (the σ⇘route⇙(rt, ip)) (π⇩7(r))))"
shows "(P (update rt ip r))"
proof (cases "ip ∈ kD(rt)")
assume "ip ∉ kD(rt)"
with c1 show ?thesis
by simp
next
assume "ip ∈ kD(rt)"
moreover then obtain dsn dsk fl hops nhip pre
where rteq: "rt ip = Some (dsn, dsk, fl, hops, nhip, pre)"
by (metis kD_Some)
moreover obtain dsn' dsk' fl' hops' nhip' pre'
where req: "r = (dsn', dsk', fl', hops', nhip', pre')"
by (cases r) metis
ultimately show ?thesis
using ‹(π⇩2(r) = 0) = (π⇩3(r) = unk)›
c2 [OF ‹ip∈kD(rt)›]
c3 [OF ‹ip∈kD(rt)›]
c4 [OF ‹ip∈kD(rt)›]
c5 [OF ‹ip∈kD(rt)›]
c6 [OF ‹ip∈kD(rt)›]
unfolding update_def sqn_def by auto
qed

lemma update_cases_kD:
assumes "(π⇩2(r) = 0) = (π⇩3(r) = unk)"
and "ip ∈ kD(rt)"
and c2: "sqn rt ip < π⇩2(r) ⟹ P (rt (ip ↦ addpre r (π⇩7(the σ⇘route⇙(rt, ip)))))"
and c3: "⟦sqn rt ip = π⇩2(r); the (dhops rt ip) > π⇩5(r)⟧
⟹ P (rt (ip ↦ addpre r (π⇩7(the σ⇘route⇙(rt, ip)))))"
and c4: "⟦sqn rt ip = π⇩2(r); the (flag rt ip) = inv⟧
⟹ P (rt (ip ↦ addpre r (π⇩7(the σ⇘route⇙(rt, ip)))))"
and c5: "π⇩3(r) = unk ⟹ P (rt (ip ↦ (π⇩2(the σ⇘route⇙(rt, ip)), π⇩3(r),
π⇩4(r), π⇩5(r), π⇩6(r),
and c6: "⟦sqn rt ip ≥ π⇩2(r); π⇩3(r) = kno;
sqn rt ip = π⇩2(r) ⟹ the (dhops rt ip) ≤ π⇩5(r) ∧ the (flag rt ip) = val⟧
⟹ P (rt (ip ↦ addpre (the σ⇘route⇙(rt, ip)) (π⇩7(r))))"
shows "(P (update rt ip r))"
using assms(1) proof (rule update_cases)
assume "sqn rt ip < π⇩2(r)"
thus "P (rt(ip ↦ addpre r (π⇩7(the (rt ip)))))" by (rule c2)
next
assume "sqn rt ip = π⇩2(r)"
and "the (dhops rt ip) > π⇩5(r)"
thus "P (rt(ip ↦ addpre r (π⇩7 (the (rt ip)))))"
by (rule c3)
next
assume "sqn rt ip = π⇩2(r)"
and "the (flag rt ip) = inv"
thus "P (rt(ip ↦ addpre r (π⇩7 (the (rt ip)))))"
by (rule c4)
next
assume "π⇩3(r) = unk"
thus "P (rt (ip ↦ (π⇩2(the σ⇘route⇙(rt, ip)), π⇩3(r), π⇩4(r), π⇩5(r), π⇩6(r),
by (rule c5)
next
assume "sqn rt ip ≥ π⇩2(r)"
and "π⇩3(r) = kno"
and "sqn rt ip = π⇩2(r) ⟹ the (dhops rt ip) ≤ π⇩5(r) ∧ the (flag rt ip) = val"
thus "P (rt (ip ↦ addpre (the (rt ip)) (π⇩7(r))))"
by (rule c6)
qed (simp add: ‹ip ∈ kD(rt)›)

lemma in_kD_after_update [simp]:
fixes rt nip dsn dsk flag hops nhip pre
shows "kD (update rt nip (dsn, dsk, flag, hops, nhip, pre)) = insert nip (kD rt)"
unfolding update_def
by (cases "rt nip") auto

lemma nhop_of_update [simp]:
fixes rt dip dsn dsk flag hops nhip
assumes "rt ≠ update rt dip (dsn, dsk, flag, hops, nhip, {})"
shows "the (nhop (update rt dip (dsn, dsk, flag, hops, nhip, {})) dip) = nhip"
proof -
from assms
have update_neq: "⋀v. rt dip = Some v ⟹
update rt dip (dsn, dsk, flag, hops, nhip, {})
≠ rt(dip ↦ addpre (the (rt dip)) (π⇩7 (dsn, dsk, flag, hops, nhip, {})))"
by auto
show ?thesis
proof (cases "rt dip = None")
assume "rt dip = None"
thus "?thesis" unfolding update_def by clarsimp
next
assume "rt dip ≠ None"
then obtain v where "rt dip = Some v" by (metis not_None_eq)
with update_neq [OF this] show ?thesis
unfolding update_def by auto
qed
qed

lemma sqn_if_updated:
fixes rip v rt ip
shows "sqn (λx. if x = rip then Some v else rt x) ip
= (if ip = rip then π⇩2(v) else sqn rt ip)"
unfolding sqn_def by simp

lemma update_sqn [simp]:
fixes rt dip rip dsn dsk hops nhip pre
assumes "(dsn = 0) = (dsk = unk)"
shows "sqn rt dip ≤ sqn (update rt rip (dsn, dsk, val, hops, nhip, pre)) dip"
proof (rule update_cases)
show "(π⇩2 (dsn, dsk, val, hops, nhip, pre) = 0) = (π⇩3 (dsn, dsk, val, hops, nhip, pre) = unk)"
by simp (rule assms)
qed (clarsimp simp: sqn_if_updated sqn_def)+

lemma sqn_update_bigger [simp]:
fixes rt ip ip' dsn dsk flag hops nhip pre
assumes "1 ≤ hops"
shows "sqn rt ip ≤ sqn (update rt ip' (dsn, dsk, flag, hops, nhip, pre)) ip"
using assms unfolding update_def sqn_def
by (clarsimp split: option.split) auto

lemma dhops_update [intro]:
fixes rt dsn dsk flag hops ip rip nhip pre
assumes ex: "∀ip∈kD rt. the (dhops rt ip) ≥ 1"
and ip: "(ip = rip ∧ Suc 0 ≤ hops) ∨ (ip ≠ rip ∧ ip∈kD rt)"
shows "Suc 0 ≤ the (dhops (update rt rip (dsn, dsk, flag, hops, nhip, pre)) ip)"
using ip proof
assume "ip = rip ∧ Suc 0 ≤ hops" thus ?thesis
unfolding update_def using ex
by (cases "rip ∈ kD rt") (drule(1) bspec, auto)
next
assume "ip ≠ rip ∧ ip∈kD rt" thus ?thesis
using ex unfolding update_def
by (cases "rip∈kD rt") auto
qed

lemma update_another [simp]:
fixes dip ip rt dsn dsk flag hops nhip pre
assumes "ip ≠ dip"
shows "(update rt dip (dsn, dsk, flag, hops, nhip, pre)) ip = rt ip"
using assms unfolding update_def
by (clarsimp split: option.split)

lemma nhop_update_another [simp]:
fixes dip ip rt dsn dsk flag hops nhip pre
assumes "ip ≠ dip"
shows "nhop (update rt dip (dsn, dsk, flag, hops, nhip, pre)) ip = nhop rt ip"
using assms unfolding update_def
by (clarsimp split: option.split)

lemma dhops_update_another [simp]:
fixes dip ip rt dsn dsk flag hops nhip pre
assumes "ip ≠ dip"
shows "dhops (update rt dip (dsn, dsk, flag, hops, nhip, pre)) ip = dhops rt ip"
using assms unfolding update_def
by (clarsimp split: option.split)

lemma sqn_update_same [simp]:
"⋀rt ip dsn dsk flag hops nhip pre. sqn (rt(ip ↦ v)) ip = π⇩2(v)"
unfolding sqn_def by simp

lemma dhops_update_changed [simp]:
fixes rt dip osn hops nhip
assumes "rt ≠ update rt dip (osn, kno, val, hops, nhip, {})"
shows "the (dhops (update rt dip (osn, kno, val, hops, nhip, {})) dip) = hops"
using assms unfolding update_def
by (clarsimp split: option.split_asm option.split if_split_asm) auto

lemma nhop_update_unk_val [simp]:
"⋀rt dip ip dsn hops npre.
the (nhop (update rt dip (dsn, unk, val, hops, ip, npre)) dip) = ip"
unfolding update_def by (clarsimp split: option.split)

lemma nhop_update_changed [simp]:
fixes rt dip dsn dsk flg hops sip
assumes "update rt dip (dsn, dsk, flg, hops, sip, {}) ≠ rt"
shows "the (nhop (update rt dip (dsn, dsk, flg, hops, sip, {})) dip) = sip"
using assms unfolding update_def
by (clarsimp split: option.splits if_split_asm) auto

lemma update_rt_split_asm:
"⋀rt ip dsn dsk flag hops sip.
P (update rt ip (dsn, dsk, flag, hops, sip, {}))
=
(¬(rt = update rt ip (dsn, dsk, flag, hops, sip, {}) ∧ ¬P rt
∨ rt ≠ update rt ip (dsn, dsk, flag, hops, sip, {})
∧ ¬P (update rt ip (dsn, dsk, flag, hops, sip, {}))))"
by auto

lemma sqn_update [simp]: "⋀rt dip dsn flg hops sip.
rt ≠ update rt dip (dsn, kno, flg, hops, sip, {})
⟹ sqn (update rt dip (dsn, kno, flg, hops, sip, {})) dip = dsn"
unfolding update_def by (clarsimp split: option.split if_split_asm) auto

lemma sqnf_update [simp]: "⋀rt dip dsn dsk flg hops sip.
rt ≠ update rt dip (dsn, dsk, flg, hops, sip, {})
⟹ sqnf (update rt dip (dsn, dsk, flg, hops, sip, {})) dip = dsk"
unfolding update_def sqnf_def
by (clarsimp split: option.splits if_split_asm) auto

lemma update_kno_dsn_greater_zero:
"⋀rt dip ip dsn hops npre. 1 ≤ dsn ⟹ 1 ≤ (sqn (update rt dip (dsn, kno, val, hops, ip, npre)) dip)"
unfolding update_def
by (clarsimp split: option.splits)

lemma proj3_update [simp]: "⋀rt dip dsn dsk flg hops sip.
rt ≠ update rt dip (dsn, dsk, flg, hops, sip, {})
⟹ π⇩3(the (update rt dip (dsn, dsk, flg, hops, sip, {}) dip)) = dsk"
unfolding update_def sqnf_def
by (clarsimp split: option.splits if_split_asm) auto

lemma nhop_update_changed_kno_val [simp]: "⋀rt ip dsn dsk hops nhip.
rt ≠ update rt ip (dsn, kno, val, hops, nhip, {})
⟹ the (nhop (update rt ip (dsn, kno, val, hops, nhip, {})) ip) = nhip"
unfolding update_def
by (clarsimp split: option.split_asm option.split if_split_asm) auto

lemma flag_update [simp]: "⋀rt dip dsn flg hops sip.
rt ≠ update rt dip (dsn, kno, flg, hops, sip, {})
⟹ the (flag (update rt dip (dsn, kno, flg, hops, sip, {})) dip) = flg"
unfolding update_def
by (clarsimp split: option.split if_split_asm) auto

lemma the_flag_Some [dest!]:
fixes ip rt
assumes "the (flag rt ip) = x"
and "ip ∈ kD rt"
shows "flag rt ip = Some x"
using assms by auto

lemma kD_update_unchanged [dest]:
fixes rt dip dsn dsk flag hops nhip pre
assumes "rt = update rt dip (dsn, dsk, flag, hops, nhip, pre)"
shows "dip∈kD(rt)"
proof -
have "dip∈kD(update rt dip (dsn, dsk, flag, hops, nhip, pre))" by simp
with assms show ?thesis by simp
qed

lemma nhop_update [simp]: "⋀rt dip dsn dsk flg hops sip.
rt ≠ update rt dip (dsn, dsk, flg, hops, sip, {})
⟹ the (nhop (update rt dip (dsn, dsk, flg, hops, sip, {})) dip) = sip"
unfolding update_def sqnf_def
by (clarsimp split: option.splits if_split_asm) auto

lemma sqn_update_another [simp]:
fixes dip ip rt dsn dsk flag hops nhip pre
assumes "ip ≠ dip"
shows "sqn (update rt dip (dsn, dsk, flag, hops, nhip, pre)) ip = sqn rt ip"
using assms unfolding update_def sqn_def
by (clarsimp split: option.splits) auto

lemma sqnf_update_another [simp]:
fixes dip ip rt dsn dsk flag hops nhip pre
assumes "ip ≠ dip"
shows "sqnf (update rt dip (dsn, dsk, flag, hops, nhip, pre)) ip = sqnf rt ip"
using assms unfolding update_def sqnf_def
by (clarsimp split: option.splits) auto

lemma vD_update_val [dest]:
"⋀dip rt dip' dsn dsk hops nhip pre.
dip ∈ vD(update rt dip' (dsn, dsk, val, hops, nhip, pre)) ⟹ (dip∈vD(rt) ∨ dip=dip')"
unfolding update_def vD_def by (clarsimp split: option.split_asm if_split_asm)

subsubsection "Invalidating route entries"

definition invalidate :: "rt ⇒ (ip ⇀ sqn) ⇒ rt"
where "invalidate rt dests ≡
λip. case (rt ip, dests ip) of
(None, _) ⇒ None
| (Some s, None) ⇒ Some s
| (Some (_, dsk, _, hops, nhip, pre), Some rsn) ⇒
Some (rsn, dsk, inv, hops, nhip, pre)"

lemma proj3_invalidate [simp]:
"⋀dip. π⇩3(the ((invalidate rt dests) dip)) = π⇩3(the (rt dip))"
unfolding invalidate_def by (clarsimp split: option.split)

lemma proj5_invalidate [simp]:
"⋀dip. π⇩5(the ((invalidate rt dests) dip)) = π⇩5(the (rt dip))"
unfolding invalidate_def by (clarsimp split: option.split)

lemma proj6_invalidate [simp]:
"⋀dip. π⇩6(the ((invalidate rt dests) dip)) = π⇩6(the (rt dip))"
unfolding invalidate_def by (clarsimp split: option.split)

lemma proj7_invalidate [simp]:
"⋀dip. π⇩7(the ((invalidate rt dests) dip)) = π⇩7(the (rt dip))"
unfolding invalidate_def by (clarsimp split: option.split)

subsection "Route Requests"

lemma invalidate_kD_inv [simp]:
"⋀rt dests. kD (invalidate rt dests) = kD rt"
unfolding invalidate_def kD_def
by (simp split: option.split)

lemma invalidate_sqn:
fixes rt dip dests
assumes "∀rsn. dests dip = Some rsn ⟶ sqn rt dip ≤ rsn"
shows "sqn rt dip ≤ sqn (invalidate rt dests) dip"
proof (cases "dip ∉ kD(rt)")
assume "¬ dip ∉ kD(rt)"
hence "dip∈kD(rt)" by simp
then obtain dsn dsk flag hops nhip pre where "rt dip = Some (dsn, dsk, flag, hops, nhip, pre)"
by (metis kD_Some)
with assms show "sqn rt dip ≤ sqn (invalidate rt dests) dip"
by (cases "dests dip") (auto simp add: invalidate_def sqn_def)
qed simp

lemma sqn_invalidate_in_dests [simp]:
fixes dests ipa rsn rt
assumes "dests ipa = Some rsn"
and "ipa∈kD(rt)"
shows "sqn (invalidate rt dests) ipa = rsn"
unfolding invalidate_def sqn_def
using assms(1) assms(2) [THEN kD_Some]
by clarsimp

lemma dhops_invalidate [simp]:
"⋀dip. the (dhops (invalidate rt dests) dip) = the (dhops rt dip)"
unfolding invalidate_def by (clarsimp split: option.split)

lemma sqnf_invalidate [simp]:
"⋀dip. sqnf (invalidate (rt ξ) (dests ξ)) dip = sqnf (rt ξ) dip"
unfolding sqnf_def invalidate_def by (clarsimp split: option.split)

lemma nhop_invalidate [simp]:
"⋀dip. the (nhop (invalidate (rt ξ) (dests ξ)) dip) = the (nhop (rt ξ) dip)"
unfolding invalidate_def by (clarsimp split: option.split)

lemma invalidate_other [simp]:
fixes rt dests dip
assumes "dip∉dom(dests)"
shows "invalidate rt dests dip = rt dip"
using assms unfolding invalidate_def
by (clarsimp split: option.split_asm)

lemma invalidate_none [simp]:
fixes rt dests dip
assumes "dip∉kD(rt)"
shows "invalidate rt dests dip = None"
using assms unfolding invalidate_def by clarsimp

lemma vD_invalidate_vD_not_dests:
"⋀dip rt dests. dip∈vD(invalidate rt dests) ⟹ dip∈vD(rt) ∧ dests dip = None"
unfolding invalidate_def vD_def
by (clarsimp split: option.split_asm)

lemma sqn_invalidate_not_in_dests [simp]:
fixes dests dip rt
assumes "dip∉dom(dests)"
shows "sqn (invalidate rt dests) dip = sqn rt dip"
using assms unfolding sqn_def by simp

lemma invalidate_changes:
fixes rt dests dip dsn dsk flag hops nhip pre
assumes "invalidate rt dests dip = Some (dsn, dsk, flag, hops, nhip, pre)"
shows "  dsn = (case dests dip of None ⇒ π⇩2(the (rt dip)) | Some rsn ⇒ rsn)
∧ dsk = π⇩3(the (rt dip))
∧ flag = (if dests dip = None then π⇩4(the (rt dip)) else inv)
∧ hops = π⇩5(the (rt dip))
∧ nhip = π⇩6(the (rt dip))
∧ pre = π⇩7(the (rt dip))"
using assms unfolding invalidate_def
by (cases "rt dip", clarsimp, cases "dests dip") auto

lemma proj3_inv: "⋀dip rt dests. dip∈kD (rt)
⟹ π⇩3(the (invalidate rt dests dip)) = π⇩3(the (rt dip))"
by (clarsimp simp: invalidate_def kD_def split: option.split)

lemma dests_iD_invalidate [simp]:
assumes "dests ip = Some rsn"
and "ip∈kD(rt)"
shows "ip∈iD(invalidate rt dests)"
using assms(1) assms(2) [THEN kD_Some] unfolding invalidate_def iD_def
by (clarsimp split: option.split)

subsection "Queued Packets"

text ‹Functions for sending data packets.›

type_synonym store = "ip ⇀ (p × data list)"

definition sigma_queue :: "store ⇒ ip ⇒ data list"    ("σ⇘queue⇙'(_, _')")
where "σ⇘queue⇙(store, dip) ≡ case store dip of None ⇒ [] | Some (p, q) ⇒ q"

definition qD :: "store ⇒ ip set"
where "qD ≡ dom"

definition add :: "data ⇒ ip ⇒ store ⇒ store"
where "add d dip store ≡ case store dip of
None ⇒ store (dip ↦ (req, [d]))
| Some (p, q) ⇒ store (dip ↦ (p, q @ [d]))"

fixes d dip store
shows "qD(add d dip store) = insert dip (qD store)"
by (clarsimp split: option.split)

definition drop :: "ip ⇒ store ⇀ store"
where "drop dip store ≡
map_option (λ(p, q). if tl q = [] then store (dip := None)
else store (dip ↦ (p, tl q))) (store dip)"

definition sigma_p_flag :: "store ⇒ ip ⇀ p" ("σ⇘p-flag⇙'(_, _')")
where "σ⇘p-flag⇙(store, dip) ≡ map_option fst (store dip)"

definition unsetRRF :: "store ⇒ ip ⇒ store"
where "unsetRRF store dip ≡ case store dip of
None ⇒ store
| Some (p, q) ⇒ store (dip ↦ (noreq, q))"

definition setRRF :: "store ⇒ (ip ⇀ sqn) ⇒ store"
where "setRRF store dests ≡ λdip. if dests dip = None then store dip
else map_option (λ(_, q). (req, q)) (store dip)"

subsection "Comparison with the original technical report"

text ‹
The major differences with the AODV technical report of Fehnker et al are:
\begin{enumerate}
\item @{term nhop} is partial, thus a @{term the}' is needed, similarly for @{term dhops}
\item @{term precs} is partial.
\item @{term "σ⇘p-flag⇙(store, dip)"} is partial.
\item The routing table (@{typ rt}) is modelled as a map (@{typ "ip ⇒ r option"})
rather than a set of 7-tuples, likewise, the @{typ r} is a 6-tuple rather than
a 7-tuple, i.e., the destination ip-address (@{term "dip"}) is taken from the
argument to the function, rather than a part of the result. Well-definedness then
follows from the structure of the type and more related facts are available
automatically, rather than having to be acquired through tedious proofs.
\item Similar remarks hold for the dests mapping passed to @{term "invalidate"},
and @{term "store"}.
\end{enumerate}
›

end