Theory Aodv_Data

(*  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" ("π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 "ipkD(rt)"
      and "the (flag rt ip) = val"
    shows "ipvD(rt)"
  using assms unfolding vD_def by auto

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

lemma iD_flag_is_inv [elim, simp]:
    fixes ip rt
  assumes "ipiD(rt)"
    shows "the (flag rt ip) = inv"
  proof -
    from ipiD(rt) have "ipkD(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 "ipkD(rt)"
      and "ipvD(rt)"
    shows "ipiD(rt)"
  proof -
    from ipkD(rt) obtain dsn dsk f hops nhop pre
      where rtip: "rt ip = Some (dsn, dsk, f, hops, nhop, pre)"
       by (metis kD_Some)
    from ipvD(rt) have "f  val"
    proof (rule contrapos_nn)
      assume "f = val"
      with rtip have "the (flag rt ip) = val" by simp
      with ipkD(rt) show "ipvD(rt)" ..
    qed
    with rtip have "the (flag rt ip)= inv" by simp  
    with ipkD(rt) show "ipiD(rt)" ..
  qed

lemma vD_or_iD [elim]:
    fixes ip rt
  assumes "ipkD(rt)"
      and "ipvD(rt)  P rt ip"
      and "ipiD(rt)  P rt ip"
    shows "P rt ip"
  proof -
    from ipkD(rt) have "ipvD(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. dipkD(rt)  π5(the (rt dip)) = the (dhops rt dip)"
  unfolding sqn_def by (drule kD_Some) clarsimp

lemma proj4_eq_flag: "dip rt. dipkD(rt)  π4(the (rt dip)) = the (flag rt dip)"
  unfolding sqn_def by (drule kD_Some) clarsimp

lemma proj2_eq_sqn: "dip rt. dipkD(rt)  π2(the (rt dip)) = sqn rt dip"
  unfolding sqn_def by (drule kD_Some) clarsimp

lemma kD_sqnf_is_proj3 [simp]:
  "ip rt. ipkD(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'  ipkD(rt)"
      and "ip = ip'  P rt ip ip'"
      and " ip  ip'; ipkD(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 "π2(addpre v pre) = π2(v)"
  unfolding addpre_def by (cases v) simp

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

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

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

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

lemma proj7_addpre:
  fixes dsn dsk flag hops nhip pre npre
  shows "π7(addpre v npre) = π7(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)) (σroute(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 "ipkD 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

lemma proj3_addpreRT [simp]:
    fixes ip rt ip' npre
  assumes "ipkD 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

lemma proj5_addpreRT [simp]:
  "rt dip ip npre. dipkD(rt)  π5(the (the (addpreRT rt dip npre) ip)) = π5(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. ipkD(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  π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 "ipkD(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 ipkD(rt)]
            c3 [OF ipkD(rt)]
            c4 [OF ipkD(rt)]
            c5 [OF ipkD(rt)]
            c6 [OF ipkD(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),
                                            π7(addpre r (π7(the σroute(rt, ip)))))))"
      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),
                        π7(addpre r (π7(the (rt ip)))))))"
      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: "ipkD rt. the (dhops rt ip)  1"
      and ip: "(ip = rip  Suc 0  hops)  (ip  rip  ipkD 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  ipkD rt" thus ?thesis
      using ex unfolding update_def
      by (cases "ripkD 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 "dipkD(rt)"
  proof -
    have "dipkD(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))  (dipvD(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)

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 "dipkD(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 "ipakD(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 "dipdom(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 "dipkD(rt)"
    shows "invalidate rt dests dip = None"
  using assms unfolding invalidate_def by clarsimp

lemma vD_invalidate_vD_not_dests:
  "dip rt dests. dipvD(invalidate rt dests)  dipvD(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 "dipdom(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. dipkD (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 "ipkD(rt)"
    shows "ipiD(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"    ("σ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]))"

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" ("σ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}
        and @{term addpreRT}.
  \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