Quelle  Aodv_Data.thy

(*  Title:       Aodv_Data.thy
    License:     BSD 2-Clause. See LICENSE.
    Author:      Timothy Bourke, Inria
*)

section "Predicates and functions used in the AODV model"

theory Aodv_Data
imports Aodv_Basic
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" (‹π₂›)
  where "π₂ ≡ λ(dsn, _, _, _, _, _). dsn"

definition proj3 :: "r ==> k" (‹π₃›)
  where "π₃ ≡ λ(_, dsk, _, _, _, _). dsk"

definition proj4 :: "r ==> f" (‹π₄›)
  where "π₄ ≡ λ(_, _, flag, _, _, _). flag"

definition proj5 :: "r ==> nat" (‹π₅›)
  where "π₅ ≡ λ(_, _, _, hops, _, _). hops"

definition proj6 :: "r ==> ip" (‹π₆›)
  where "π₆ ≡ λ(_, _, _, _, nhip, _). nhip"

definition proj7 :: "r ==> ip set" (‹π₇›)
  where "π₇ ≡ λ(_, _, _, _, _, pre). pre"

lemma projs [simp]:
  "π₂(dsn, dsk, flag, hops, nhip, pre) = dsn"
  "π₃(dsn, dsk, flag, hops, nhip, pre) = dsk"
  "π₄(dsn, dsk, flag, hops, nhip, pre) = flag"
  "π₅(dsn, dsk, flag, hops, nhip, pre) = hops"
  "π₆(dsn, dsk, flag, hops, nhip, pre) = nhip"
  "π₇(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 (π₃ x)"
  by (rule k.induct)

lemma proj4_pred [intro]: "[ P val; P inv ] ==> P (π₄ x)"
  by (rule f.induct)

lemma proj6_pair_snd [simp]:
  fixes dsn' r
  shows "π₆ (dsn', snd (r)) = π₆(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"  (‹σ'(_, _')›)

translations
 "σ(rt, dip)" => "rt dip" 

definition sqn :: "rt ==> ip ==> sqn"
  where "sqn rt dip ≡ case σ(rt, dip) of Some r ==> π₂(r) | None ==> 0"

definition sqnf :: "rt ==> ip ==> k"
  where "sqnf rt dip ≡ case σ(rt, dip) of Some r ==> π₃(r) | None ==> unk"

abbreviation flag :: "rt ==> ip ⇀ f"
  where "flag rt dip ≡ map_option π₄ (σ(rt, dip))"

abbreviation dhops :: "rt ==> ip ⇀ nat"
   where "dhops rt dip ≡ map_option π₅ (σ(rt, dip))"

abbreviation nhop :: "rt ==> ip ⇀ ip"
   where "nhop rt dip ≡ map_option π₆ (σ(rt, dip))"

abbreviation precs :: "rt ==> ip ⇀ ip set"
   where "precs rt dip ≡ map_option π₇ (σ(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.
           σ(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 "σ(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.
           σ(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.
           σ(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)"
      by (simp add: kD_is_vD_and_iD)
    thus ?thesis by (auto elim: assms(2-3))
  qed

lemma proj5_eq_dhops: "∧dip rt. dip∈kD(rt) ==> π₅(the (rt dip)) = the (dhops rt dip)"
  unfolding sqn_def by (drule kD_Some) clarsimp

lemma proj4_eq_flag: "∧dip rt. dip∈kD(rt) ==> π₄(the (rt dip)) = the (flag rt dip)"
  unfolding sqn_def by (drule kD_Some) clarsimp

lemma proj2_eq_sqn: "∧dip rt. dip∈kD(rt) ==> π₂(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 = π₃(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)"

lemma proj2_addpre:
  fixes v pre
  shows "π₂(addpre v pre) = π₂(v)"
  unfolding addpre_def by (cases v) simp

lemma proj3_addpre:
  fixes v pre
  shows "π₃(addpre v pre) = π₃(v)"
  unfolding addpre_def by (cases v) simp

lemma proj4_addpre:
  fixes v pre
  shows "π₄(addpre v pre) = π₄(v)"
  unfolding addpre_def by (cases v) simp

lemma proj5_addpre:
  fixes v pre
  shows "π₅(addpre v pre) = π₅(v)"
  unfolding addpre_def by (cases v) simp

lemma proj6_addpre:
  fixes dsn dsk flag hops nhip pre npre
  shows "π₆(addpre v npre) = π₆(v)"
  unfolding addpre_def by (cases v) simp

lemma proj7_addpre:
  fixes dsn dsk flag hops nhip pre npre
  shows "π₇(addpre v npre) = π₇(v) ∪ npre"
  unfolding addpre_def by (cases v) simp

lemma addpre_empty: "addpre r {} = r"
  unfolding addpre_def by simp

lemma addpre_r:
  "addpre (dsn, dsk, fl, hops, nhip, pre) npre = (dsn, dsk, fl, hops, nhip, pre ∪ npre)"
  unfolding addpre_def by simp

lemmas addpre_simps [simp] = proj2_addpre proj3_addpre proj4_addpre proj5_addpre
                             proj6_addpre proj7_addpre addpre_empty addpre_r

definition addpreRT :: "rt ==> ip ==> ip set ⇀ rt"
  where "addpreRT rt dip npre ≡
           map_option (λs. rt (dip ↦ addpre s npre)) (σ(rt, dip))"

lemma snd_addpre [simp]:
  "∧dsn dsn' v pre. (dsn, snd(addpre (dsn', v) pre)) = addpre (dsn, v) pre"
  unfolding addpre_def by clarsimp

lemma proj2_addpreRT [simp]:
    fixes ip rt ip' npre
  assumes "ip∈kD rt"
      and "ip'∈kD rt"
    shows "π₂(the (the (addpreRT rt ip' npre) ip)) = π₂(the (rt ip))"
  using assms [THEN kD_Some] unfolding addpreRT_def by clarsimp

lemma proj3_addpreRT [simp]:
    fixes ip rt ip' npre
  assumes "ip∈kD rt"
      and "ip'∈kD rt"
    shows "π₃(the (the (addpreRT rt ip' npre) ip)) = π₃(the (rt ip))"
  using assms [THEN kD_Some] unfolding addpreRT_def by clarsimp

lemma proj5_addpreRT [simp]:
  "∧rt dip ip npre. dip∈kD(rt) ==> π₅(the (the (addpreRT rt dip npre) ip)) = π₅(the (rt ip))"
  unfolding addpreRT_def by auto

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

  lemma kD_addpreRT [simp]:
  fixes rt dip npre
  assumes "dip ∈ kD rt"
  shows "kD (the (addpreRT rt dip npre)) = kD rt"
  unfolding kD_def addpreRT_def
  using assms [THEN kD_Some]
  by clarsimp blast

lemma vD_addpreRT [simp]:
  fixes rt dip npre
  assumes "dip ∈ kD rt"
  shows "vD (the (addpreRT rt dip npre)) = vD rt"
  unfolding vD_def addpreRT_def
  using assms [THEN kD_Some] by clarsimp auto

lemma iD_addpreRT [simp]:
  fixes rt dip npre
  assumes "dip ∈ kD rt"
  shows "iD (the (addpreRT rt dip npre)) = iD rt"
  unfolding iD_def addpreRT_def
  using assms [THEN kD_Some] by clarsimp auto

lemma nhop_addpreRT [simp]:
    fixes rt pre ip dip
  assumes "dip ∈ kD rt"
    shows "nhop (the (addpreRT rt dip pre)) ip = nhop rt ip"
  unfolding sqn_def addpreRT_def
  using assms [THEN kD_Some] by (clarsimp)

lemma sqn_addpreRT [simp]:
    fixes rt pre ip dip
  assumes "dip ∈ kD rt"
    shows "sqn (the (addpreRT rt dip pre)) ip = sqn rt ip"
  unfolding sqn_def addpreRT_def
  using assms [THEN kD_Some] by (clarsimp)

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

lemma sqnf_addpreRT [simp]:
  "∧ip dip. ip∈kD(rt ξ) ==> sqnf (the (addpreRT (rt ξ) ip npre)) dip = sqnf (rt ξ) dip"
  unfolding sqnf_def addpreRT_def by auto

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 ≡ π₄(r) = val ∧
                         (π₂(r) = 0) = (π₃(r) = unk) ∧
                         (π₃(r) = unk ⟶ π₅(r) = 1)"

lemma update_arg_wf_gives_cases:
  "∧r. update_arg_wf r ==> (π₂(r) = 0) = (π₃(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 σ(rt, ip) of
       None ==> rt (ip ↦ r)
     | Some s ==>
          if π₂(s) < π₂(r) then rt (ip ↦ addpre r (π₇(s)))
          else if π₂(s) = π₂(r) ∧ (π₅(s) > π₅(r) ∨ π₄(s) = inv)
               then rt (ip ↦ addpre r (π₇(s)))
               else if π₃(r) = unk
                    then rt (ip ↦ (π₂(s), snd (addpre r (π₇(s)))))
                    else rt (ip ↦ addpre s (π₇(r)))"

lemma update_simps [simp]:
  fixes r s nrt nr nr' ns rt ip
  defines "s ≡ the σ(rt, ip)"
      and "nr ≡ addpre r (π₇(s))"
      and "nr' ≡ (π₂(s), π₃(nr), π₄(nr), π₅(nr), π₆(nr), π₇(nr))"
      and "ns ≡ addpre s (π₇(r))"
  shows
  "[ip ∉ kD(rt)] ==> update rt ip r = rt (ip ↦ r)"
  "[ip ∈ kD(rt); sqn rt ip < π₂(r)] ==> update rt ip r = rt (ip ↦ nr)"
  "[ip ∈ kD(rt); sqn rt ip = π₂(r);
                 the (dhops rt ip) > π₅(r)] ==> update rt ip r = rt (ip ↦ nr)"
  "[ip ∈ kD(rt); sqn rt ip = π₂(r);
                 flag rt ip = Some inv] ==> update rt ip r = rt (ip ↦ nr)"
  "[ip ∈ kD(rt); π₃(r) = unk; (π₂(r) = 0) = (π₃(r) = unk)] ==> update rt ip r = rt (ip ↦ nr')"
  "[ip ∈ kD(rt); sqn rt ip ≥ π₂(r); π₃(r) = kno;
    sqn rt ip = π₂(r) ==> the (dhops rt ip) ≤ π₅(r) ∧ the (flag rt ip) = val ]
                                            ==> update rt ip r = rt (ip ↦ ns)"
  proof -
    assume "ip∉kD(rt)"
    hence "σ(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 < π₂(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 < \π₂(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 = π₂(r)"
       and "the (dhops rt ip) > π₅(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 = π₂(r)› and ‹the (dhops rt ip) > π₅(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 = π₂(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 = π₂(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 "π₃(r) = unk"
       and "(π₂(r) = 0) = (π₃(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 ‹(π₂(r) = 0) = (π₃(r) = unk)› and ‹π₃(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 ≥ π₂(r)"
           "π₃(r) = kno"
           "sqn rt ip = π₂(r) ==> the (dhops rt ip) ≤ π₅(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 "(π₂(r) = 0) = (π₃(r) = unk)"
      and c1: "[ip ∉ kD(rt)] ==> P (rt (ip ↦ r))"

      and c2: "[ip ∈ kD(rt); sqn rt ip < π₂(r)]
                ==> P (rt (ip ↦ addpre r (π₇(the σ(rt, ip)))))"
      and c3: "[ip ∈ kD(rt); sqn rt ip = π₂(r); the (dhops rt ip) > π₅(r)]
                ==> P (rt (ip ↦ addpre r (π₇(the σ(rt, ip)))))"
      and c4: "[ip ∈ kD(rt); sqn rt ip = π₂(r); the (flag rt ip) = inv]
                ==> P (rt (ip ↦ addpre r (π₇(the σ(rt, ip)))))"
      and c5: "[ip ∈ kD(rt); π₃(r) = unk]
                ==> P (rt (ip ↦ (π₂(the σ(rt, ip)), π₃(r),
                                  π₄(r), π₅(r), π₆(r), π₇(addpre r (π₇(the σ(rt, ip)))))))"
      and c6: "[ip ∈ kD(rt); sqn rt ip ≥ π₂(r); π₃(r) = kno;
                sqn rt ip = π₂(r) ==> the (dhops rt ip) ≤ π₅(r) ∧ the (flag rt ip) = val]
                ==> P (rt (ip ↦ addpre (the σ(rt, ip)) (π₇(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 ‹(π₂(r) = 0) = (π₃(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 "(π₂(r) = 0) = (π₃(r) = unk)"
      and "ip ∈ kD(rt)"
      and c2: "sqn rt ip < π₂(r) ==> P (rt (ip ↦ addpre r (π₇(the σ(rt, ip)))))"
      and c3: "[sqn rt ip = π₂(r); the (dhops rt ip) > π₅(r)]
                ==> P (rt (ip ↦ addpre r (π₇(the σ(rt, ip)))))"
      and c4: "[sqn rt ip = π₂(r); the (flag rt ip) = inv]
                ==> P (rt (ip ↦ addpre r (π₇(the σ(rt, ip)))))"
      and c5: "π₃(r) = unk ==> P (rt (ip ↦ (π₂(the σ(rt, ip)), π₃(r),
                                            π₄(r), π₅(r), π₆(r),
                                            π₇(addpre r (π₇(the σ(rt, ip)))))))"
      and c6: "[sqn rt ip ≥ π₂(r); π₃(r) = kno;
                sqn rt ip = π₂(r) ==> the (dhops rt ip) ≤ π₅(r) ∧ the (flag rt ip) = val]
                ==> P (rt (ip ↦ addpre (the σ(rt, ip)) (π₇(r))))"
  shows "(P (update rt ip r))"
  using assms(1) proof (rule update_cases)
    assume "sqn rt ip < π₂(r)"
    thus "P (rt(ip ↦ addpre r (π₇(the (rt ip)))))" by (rule c2)
  next
    assume "sqn rt ip = π₂(r)"
       and "the (dhops rt ip) > π₅(r)"
    thus "P (rt(ip ↦ addpre r (π₇ (the (rt ip)))))"
      by (rule c3)
  next
    assume "sqn rt ip = π₂(r)"
       and "the (flag rt ip) = inv"
    thus "P (rt(ip ↦ addpre r (π₇ (the (rt ip)))))"
      by (rule c4)
  next
    assume "π₃(r) = unk"
    thus "P (rt (ip ↦ (π₂(the σ(rt, ip)), π₃(r), π₄(r), π₅(r), π₆(r),
                        π₇(addpre r (π₇(the (rt ip)))))))"
      by (rule c5)
  next
    assume "sqn rt ip ≥ π₂(r)"
       and "π₃(r) = kno"
       and "sqn rt ip = π₂(r) ==> the (dhops rt ip) ≤ π₅(r) ∧ the (flag rt ip) = val"
    thus "P (rt (ip ↦ addpre (the (rt ip)) (π₇(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)) (π₇ (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 π₂(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 "(π₂ (dsn, dsk, val, hops, nhip, pre) = 0) = (π₃ (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 = π₂(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, {})
  ==> π₃(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. π₃(the ((invalidate rt dests) dip)) = π₃(the (rt dip))"
  unfolding invalidate_def by (clarsimp split: option.split)

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

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

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

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 ==> π₂(the (rt dip)) | Some rsn ==> rsn)
           ∧ dsk = π₃(the (rt dip))
           ∧ flag = (if dests dip = None then π₄(the (rt dip)) else inv)
           ∧ hops = π₅(the (rt dip))
           ∧ nhip = π₆(the (rt dip))
           ∧ pre = π₇(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)
                      ==> π₃(the (invalidate rt dests dip)) = π₃(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 "Route Requests"

text ‹Generate a fresh route request identifier.›

definition nrreqid :: "(ip × rreqid) set ==> ip ==> rreqid"
  where "nrreqid rreqs ip ≡ Max ({n. (ip, n) ∈ rreqs} ∪ {0}) + 1"

subsection "Queued Packets"

text ‹Functions for sending data packets.›

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

definition sigma_queue :: "store ==> ip ==> data list"    (‹σ'(_, _')›)
  where "σ(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]))"

lemma qD_add [simp]:
  fixes d dip store
  shows "qD(add d dip store) = insert dip (qD store)"
  unfolding add_def Let_def qD_def
  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" (‹σ_-flag'(_, _')›)
  where "σ_-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}
 and @{term addpreRT}.
 \item @{term precs} is partial.
 \item @{term "σ_-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