Theory Fresher

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

section "Quality relations between routes"

theory Fresher
imports Aodv_Data
begin

subsection "Net sequence numbers"

subsubsection "On individual routes"

definition
  nsqn⇩r :: "r ⇒ sqn"
where
  "nsqn⇩r r ≡ if π⇩4(r) = val ∨ π⇩2(r) = 0 then π⇩2(r) else (π⇩2(r) - 1)"

lemma nsqnr_def':
  "nsqn⇩r r = (if π⇩4(r) = inv then π⇩2(r) - 1 else π⇩2(r))"
  unfolding nsqn⇩r_def by simp

lemma nsqn⇩r_zero [simp]:
  "⋀dsn dsk flag hops nhip pre. nsqn⇩r (0, dsk, flag, hops, nhip, pre) = 0"
  unfolding nsqn⇩r_def by clarsimp

lemma nsqn⇩r_val [simp]:
  "⋀dsn dsk hops nhip pre. nsqn⇩r (dsn, dsk, val, hops, nhip, pre) = dsn"
  unfolding nsqn⇩r_def by clarsimp

lemma nsqn⇩r_inv [simp]:
  "⋀dsn dsk hops nhip pre. nsqn⇩r (dsn, dsk, inv, hops, nhip, pre) = dsn - 1"
  unfolding nsqn⇩r_def by clarsimp

lemma nsqn⇩r_lte_dsn [simp]:
  "⋀dsn dsk flag hops nhip pre. nsqn⇩r (dsn, dsk, flag, hops, nhip, pre) ≤ dsn"
  unfolding nsqn⇩r_def by clarsimp

subsubsection "On routes in routing tables"

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

lemma nsqn_sqn_def:
  "⋀rt dip. nsqn rt dip = (if flag rt dip = Some val ∨ sqn rt dip = 0
                            then sqn rt dip else sqn rt dip - 1)"
  unfolding nsqn_def sqn_def by (clarsimp split: option.split)

lemma not_in_kD_nsqn [simp]:
  assumes "dip ∉ kD(rt)"
  shows "nsqn rt dip = 0"
  using assms unfolding nsqn_def by simp

lemma kD_nsqn:
  assumes "dip ∈ kD(rt)"
    shows "nsqn rt dip = nsqn⇩r(the (σ⇘route⇙(rt, dip)))"
  using assms [THEN kD_Some] unfolding nsqn_def by clarsimp

lemma nsqnr_r_flag_pred [simp, intro]:
    fixes dsn dsk flag hops nhip pre
  assumes "P (nsqn⇩r (dsn, dsk, val, hops, nhip, pre))"
      and "P (nsqn⇩r (dsn, dsk, inv, hops, nhip, pre))"
    shows "P (nsqn⇩r (dsn, dsk, flag, hops, nhip, pre))"
  using assms by (cases flag) auto

lemma nsqn⇩r_addpreRT_inv [simp]:
  "⋀rt dip npre dip'. dip ∈ kD(rt) ⟹
   nsqn⇩r (the (the (addpreRT rt dip npre) dip')) = nsqn⇩r (the (rt dip'))"
  unfolding addpreRT_def nsqn⇩r_def
  by (frule kD_Some) (clarsimp split: option.split)

lemma sqn_nsqn:
  "⋀rt dip. sqn rt dip - 1 ≤ nsqn rt dip"
  unfolding sqn_def nsqn_def by (clarsimp split: option.split)

lemma nsqn_sqn: "nsqn rt dip ≤ sqn rt dip"
  unfolding sqn_def nsqn_def by (cases "rt dip") auto

lemma val_nsqn_sqn [elim, simp]:
  assumes "ip∈kD(rt)"
      and "the (flag rt ip) = val"
    shows "nsqn rt ip = sqn rt ip"
  using assms unfolding nsqn_sqn_def by auto

lemma vD_nsqn_sqn [elim, simp]:
  assumes "ip∈vD(rt)"
    shows "nsqn rt ip = sqn rt ip"
  proof -
    from ‹ip∈vD(rt)› have "ip∈kD(rt)"
                      and "the (flag rt ip) = val" by auto
    thus ?thesis ..
  qed

lemma inv_nsqn_sqn [elim, simp]:
  assumes "ip∈kD(rt)"
      and "the (flag rt ip) = inv"
    shows "nsqn rt ip = sqn rt ip - 1"
  using assms unfolding nsqn_sqn_def by auto

lemma iD_nsqn_sqn [elim, simp]:
  assumes "ip∈iD(rt)"
    shows "nsqn rt ip = sqn rt ip - 1"
  proof -
    from ‹ip∈iD(rt)› have "ip∈kD(rt)"
                      and "the (flag rt ip) = inv" by auto
    thus ?thesis ..
  qed

lemma nsqn_update_changed_kno_val [simp]: "⋀rt ip dsn dsk hops nhip.
  rt ≠ update rt ip (dsn, kno, val, hops, nhip, {})
   ⟹ nsqn (update rt ip (dsn, kno, val, hops, nhip, {})) ip = dsn"
  unfolding nsqn⇩r_def update_def
  by (clarsimp simp: kD_nsqn split: option.split_asm option.split if_split_asm)
     (metis fun_upd_triv)

lemma nsqn_addpreRT_inv [simp]:
  "⋀rt dip npre dip'. dip ∈ kD(rt) ⟹
   nsqn (the (addpreRT rt dip npre)) dip' = nsqn rt dip'"
  unfolding addpreRT_def nsqn_def nsqn⇩r_def
  by (frule kD_Some) (clarsimp split: option.split)

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

lemma nsqn_invalidate_eq:
  assumes "dip ∈ kD(rt)"
      and "dests dip = Some rsn"
    shows "nsqn (invalidate rt dests) dip = rsn - 1"
  using assms
  proof -
    from assms obtain dsk hops nhip pre
      where "invalidate rt dests dip = Some (rsn, dsk, inv, hops, nhip, pre)"
      unfolding invalidate_def by auto
    moreover from ‹dip ∈ kD(rt)› have "dip ∈ kD(invalidate rt dests)" by simp
    ultimately show ?thesis
      using ‹dests dip = Some rsn› by simp
  qed

lemma nsqn_invalidate_other [simp]:
  assumes "dip∈kD(rt)"
      and "dip∉dom dests"
    shows "nsqn (invalidate rt dests) dip = nsqn rt dip"
  using assms by (clarsimp simp add: kD_nsqn)

subsection "Comparing routes "

definition
  fresher :: "r ⇒ r ⇒ bool" (‹(_/ ⊑ _)›  [51, 51] 50)
where
  "fresher r r' ≡ ((nsqn⇩r r < nsqn⇩r r') ∨ (nsqn⇩r r  = nsqn⇩r r' ∧ π⇩5(r) ≥ π⇩5(r')))"

lemma fresherI1 [intro]:
  assumes "nsqn⇩r r < nsqn⇩r r'"
    shows "r ⊑ r'"
  unfolding fresher_def using assms by simp

lemma fresherI2 [intro]:
  assumes "nsqn⇩r r = nsqn⇩r r'"
      and "π⇩5(r) ≥ π⇩5(r')"
    shows "r ⊑ r'"
  unfolding fresher_def using assms by simp

lemma fresherI [intro]:
  assumes "(nsqn⇩r r < nsqn⇩r r') ∨ (nsqn⇩r r  = nsqn⇩r r' ∧ π⇩5(r) ≥ π⇩5(r'))"
    shows "r ⊑ r'"
  unfolding fresher_def using assms .

lemma fresherE [elim]:
  assumes "r ⊑ r'"
      and "nsqn⇩r r < nsqn⇩r r' ⟹ P r r'"
      and "nsqn⇩r r  = nsqn⇩r r' ∧ π⇩5(r) ≥ π⇩5(r') ⟹ P r r'"
    shows "P r r'"
  using assms unfolding fresher_def by auto

lemma fresher_refl [simp]: "r ⊑ r"
  unfolding fresher_def by simp

lemma fresher_trans [elim, trans]:
  "⟦ x ⊑ y; y ⊑ z ⟧ ⟹ x ⊑ z"
  unfolding fresher_def by auto

lemma not_fresher_trans [elim, trans]:
  "⟦ ¬(x ⊑ y); ¬(z ⊑ x) ⟧ ⟹ ¬(z ⊑ y)"
  unfolding fresher_def by auto

lemma fresher_dsn_flag_hops_const [simp]:
  fixes dsn dsk dsk' flag hops nhip nhip' pre pre'
  shows "(dsn, dsk, flag, hops, nhip, pre) ⊑ (dsn, dsk', flag, hops, nhip', pre')"
  unfolding fresher_def by (cases flag) simp_all

lemma addpre_fresher [simp]: "⋀r npre. r ⊑ (addpre r npre)"
  by clarsimp

subsection "Comparing routing tables "

definition
  rt_fresher :: "ip ⇒ rt ⇒ rt ⇒ bool"
where
  "rt_fresher ≡ λdip rt rt'. (the (σ⇘route⇙(rt, dip))) ⊑ (the (σ⇘route⇙(rt', dip)))"

abbreviation
   rt_fresher_syn :: "rt ⇒ ip ⇒ rt ⇒ bool" (‹(_/ ⊑⇘_⇙ _)›  [51, 999, 51] 50)
where
  "rt1 ⊑⇘i⇙ rt2 ≡ rt_fresher i rt1 rt2"

lemma rt_fresher_def':
  "(rt⇩1 ⊑⇘i⇙ rt⇩2) = (nsqn⇩r (the (rt⇩1 i)) < nsqn⇩r (the (rt⇩2 i)) ∨
                     nsqn⇩r (the (rt⇩1 i)) = nsqn⇩r (the (rt⇩2 i)) ∧ π⇩5 (the (rt⇩2 i)) ≤ π⇩5 (the (rt⇩1 i)))"
  unfolding rt_fresher_def fresher_def by (rule refl)

lemma single_rt_fresher [intro]:
  assumes "the (rt1 ip) ⊑ the (rt2 ip)"
    shows "rt1 ⊑⇘ip⇙ rt2"
  using assms unfolding rt_fresher_def .

lemma rt_fresher_single [intro]:
  assumes "rt1 ⊑⇘ip⇙ rt2"
    shows "the (rt1 ip) ⊑ the (rt2 ip)"
  using assms unfolding rt_fresher_def .

lemma rt_fresher_def2:
  assumes "dip ∈ kD(rt1)"
      and "dip ∈ kD(rt2)"
    shows "(rt1 ⊑⇘dip⇙ rt2) = (nsqn rt1 dip < nsqn rt2 dip
                               ∨ (nsqn rt1 dip = nsqn rt2 dip
                                   ∧ the (dhops rt1 dip) ≥ the (dhops rt2 dip)))"
  using assms unfolding rt_fresher_def fresher_def by (simp add: kD_nsqn proj5_eq_dhops)

lemma rt_fresherI1 [intro]:
  assumes "dip ∈ kD(rt1)"
      and "dip ∈ kD(rt2)"
      and "nsqn rt1 dip < nsqn rt2 dip"
    shows "rt1 ⊑⇘dip⇙ rt2"
  unfolding rt_fresher_def2 [OF assms(1-2)] using assms(3) by simp

lemma rt_fresherI2 [intro]:
  assumes "dip ∈ kD(rt1)"
      and "dip ∈ kD(rt2)"
      and "nsqn rt1 dip = nsqn rt2 dip"
      and "the (dhops rt1 dip) ≥ the (dhops rt2 dip)"
    shows "rt1 ⊑⇘dip⇙ rt2"
  unfolding rt_fresher_def2 [OF assms(1-2)] using assms(3-4) by simp

lemma rt_fresherE [elim]:
  assumes "rt1 ⊑⇘dip⇙ rt2"
      and "dip ∈ kD(rt1)"
      and "dip ∈ kD(rt2)"
      and "⟦ nsqn rt1 dip < nsqn rt2 dip ⟧ ⟹ P rt1 rt2 dip"
      and "⟦ nsqn rt1 dip = nsqn rt2 dip;
             the (dhops rt1 dip) ≥ the (dhops rt2 dip) ⟧ ⟹ P rt1 rt2 dip"
    shows "P rt1 rt2 dip"
  using assms(1) unfolding rt_fresher_def2 [OF assms(2-3)]
  using assms(4-5) by auto

lemma rt_fresher_refl [simp]: "rt ⊑⇘dip⇙ rt"
  unfolding rt_fresher_def by simp

lemma rt_fresher_trans [elim, trans]:
  assumes "rt1 ⊑⇘dip⇙ rt2"
      and "rt2 ⊑⇘dip⇙ rt3"
    shows "rt1 ⊑⇘dip⇙ rt3"
  using assms unfolding rt_fresher_def by auto

lemma rt_fresher_if_Some [intro!]:
  assumes "the (rt dip) ⊑ r"
    shows "rt ⊑⇘dip⇙ (λip. if ip = dip then Some r else rt ip)"
  using assms unfolding rt_fresher_def by simp

definition rt_fresh_as :: "ip ⇒ rt ⇒ rt ⇒ bool"
where
  "rt_fresh_as ≡ λdip rt1 rt2. (rt1 ⊑⇘dip⇙ rt2) ∧ (rt2 ⊑⇘dip⇙ rt1)"

abbreviation
   rt_fresh_as_syn :: "rt ⇒ ip ⇒ rt ⇒ bool" (‹(_/ ≈⇘_⇙ _)›  [51, 999, 51] 50)
where
  "rt1 ≈⇘i⇙ rt2 ≡ rt_fresh_as i rt1 rt2"

lemma rt_fresh_as_refl [simp]: "⋀rt dip. rt ≈⇘dip⇙ rt"
  unfolding rt_fresh_as_def by simp

lemma rt_fresh_as_trans [simp, intro, trans]:
  "⋀rt1 rt2 rt3 dip. ⟦ rt1 ≈⇘dip⇙ rt2; rt2 ≈⇘dip⇙ rt3 ⟧ ⟹ rt1 ≈⇘dip⇙ rt3"
  unfolding rt_fresh_as_def rt_fresher_def
  by (metis (mono_tags) fresher_trans)

lemma rt_fresh_asI [intro!]:
  assumes "rt1 ⊑⇘dip⇙ rt2"
      and "rt2 ⊑⇘dip⇙ rt1"
    shows "rt1 ≈⇘dip⇙ rt2"
  using assms unfolding rt_fresh_as_def by simp

lemma rt_fresh_as_fresherI [intro]:
  assumes "dip∈kD(rt1)"
      and "dip∈kD(rt2)"
      and "the (rt1 dip) ⊑ the (rt2 dip)"
      and "the (rt2 dip) ⊑ the (rt1 dip)"
    shows "rt1 ≈⇘dip⇙ rt2"
  using assms unfolding rt_fresh_as_def
  by (clarsimp dest!: single_rt_fresher)

lemma nsqn_rt_fresh_asI:
  assumes "dip ∈ kD(rt)"
      and "dip ∈ kD(rt')"
      and "nsqn rt dip = nsqn rt' dip"
      and "π⇩5(the (rt dip)) = π⇩5(the (rt' dip))"
    shows "rt ≈⇘dip⇙ rt'"
  proof
    from assms(1-2,4) have dhops': "the (dhops rt' dip) ≤ the (dhops rt dip)"
      by (simp add: proj5_eq_dhops)
    with assms(1-3) show "rt ⊑⇘dip⇙ rt'"
      by (rule rt_fresherI2)
  next
    from assms(1-2,4) have dhops: "the (dhops rt dip) ≤ the (dhops rt' dip)"
      by (simp add: proj5_eq_dhops)
    with assms(2,1) assms(3) [symmetric] show "rt' ⊑⇘dip⇙ rt"
      by (rule rt_fresherI2)
  qed

lemma rt_fresh_asE [elim]:
  assumes "rt1 ≈⇘dip⇙ rt2"
      and "⟦ rt1 ⊑⇘dip⇙ rt2; rt2 ⊑⇘dip⇙ rt1 ⟧ ⟹ P rt1 rt2 dip"
    shows "P rt1 rt2 dip"
  using assms unfolding rt_fresh_as_def by simp

lemma rt_fresh_asD1 [dest]:
  assumes "rt1 ≈⇘dip⇙ rt2"
    shows "rt1 ⊑⇘dip⇙ rt2"
  using assms unfolding rt_fresh_as_def by simp

lemma rt_fresh_asD2 [dest]:
  assumes "rt1 ≈⇘dip⇙ rt2"
    shows "rt2 ⊑⇘dip⇙ rt1"
  using assms unfolding rt_fresh_as_def by simp

lemma rt_fresh_as_sym:
  assumes "rt1 ≈⇘dip⇙ rt2"
    shows "rt2 ≈⇘dip⇙ rt1"
  using assms unfolding rt_fresh_as_def by simp

lemma not_rt_fresh_asI1 [intro]:
  assumes "¬ (rt1 ⊑⇘dip⇙ rt2)"
    shows "¬ (rt1 ≈⇘dip⇙ rt2)"
  proof
    assume "rt1 ≈⇘dip⇙ rt2"
    hence "rt1 ⊑⇘dip⇙ rt2" ..
    with ‹¬ (rt1 ⊑⇘dip⇙ rt2)› show False ..
  qed

lemma not_rt_fresh_asI2 [intro]:
  assumes "¬ (rt2 ⊑⇘dip⇙ rt1)"
    shows "¬ (rt1 ≈⇘dip⇙ rt2)"
  proof
    assume "rt1 ≈⇘dip⇙ rt2"
    hence "rt2 ⊑⇘dip⇙ rt1" ..
    with ‹¬ (rt2 ⊑⇘dip⇙ rt1)› show False ..
  qed

lemma not_single_rt_fresher [elim]:
  assumes "¬(the (rt1 ip) ⊑ the (rt2 ip))"
    shows "¬(rt1 ⊑⇘ip⇙ rt2)"
  proof
    assume "rt1 ⊑⇘ip⇙ rt2"
    hence "the (rt1 ip) ⊑ the (rt2 ip)" ..
    with ‹¬(the (rt1 ip) ⊑ the (rt2 ip))› show False ..
  qed

lemmas not_single_rt_fresh_asI1 [intro] =  not_rt_fresh_asI1 [OF not_single_rt_fresher]
lemmas not_single_rt_fresh_asI2 [intro] =  not_rt_fresh_asI2 [OF not_single_rt_fresher]

lemma not_rt_fresher_single [elim]:
  assumes "¬(rt1 ⊑⇘ip⇙ rt2)"
    shows "¬(the (rt1 ip) ⊑ the (rt2 ip))"
  proof
    assume "the (rt1 ip) ⊑ the (rt2 ip)"
    hence "rt1 ⊑⇘ip⇙ rt2" ..
    with ‹¬(rt1 ⊑⇘ip⇙ rt2)› show False ..
  qed

lemma rt_fresh_as_nsqnr:
  assumes "dip ∈ kD(rt1)"
      and "dip ∈ kD(rt2)"
      and "rt1 ≈⇘dip⇙ rt2"
    shows "nsqn⇩r (the (rt2 dip)) = nsqn⇩r (the (rt1 dip))"
  using assms(3) unfolding rt_fresh_as_def
  by (auto simp: rt_fresher_def2 [OF ‹dip ∈ kD(rt1)› ‹dip ∈ kD(rt2)›]
                 rt_fresher_def2 [OF ‹dip ∈ kD(rt2)› ‹dip ∈ kD(rt1)›]
                 kD_nsqn [OF ‹dip ∈ kD(rt1)›]
                 kD_nsqn [OF ‹dip ∈ kD(rt2)›])

lemma rt_fresher_mapupd [intro!]:
  assumes "dip∈kD(rt)"
      and "the (rt dip) ⊑ r"
    shows "rt ⊑⇘dip⇙ rt(dip ↦ r)"
  using assms unfolding rt_fresher_def by simp

lemma rt_fresher_map_update_other [intro!]:
  assumes "dip∈kD(rt)"
      and "dip ≠ ip"
    shows "rt ⊑⇘dip⇙ rt(ip ↦ r)"
  using assms unfolding rt_fresher_def by simp

lemma rt_fresher_update_other [simp]:
  assumes inkD: "dip∈kD(rt)"
     and "dip ≠ ip"
   shows "rt ⊑⇘dip⇙ update rt ip r"
   using assms unfolding update_def
   by (clarsimp split: option.split) (fastforce)

theorem rt_fresher_update [simp]:
  assumes "dip∈kD(rt)"
      and "the (dhops rt dip) ≥ 1"
      and "update_arg_wf r"
   shows "rt ⊑⇘dip⇙ update rt ip r"
  proof (cases "dip = ip")
    assume "dip ≠ ip" with ‹dip∈kD(rt)› show ?thesis
      by (rule rt_fresher_update_other)
  next
    assume "dip = ip"

    from ‹dip∈kD(rt)› obtain dsn⇩n dsk⇩n f⇩n hops⇩n nhip⇩n pre⇩n
      where rtn [simp]: "the (rt dip) = (dsn⇩n, dsk⇩n, f⇩n, hops⇩n, nhip⇩n, pre⇩n)"
      by (metis prod_cases6)
    with ‹the (dhops rt dip) ≥ 1› and ‹dip∈kD(rt)› have "hops⇩n ≥ 1"
      by (metis proj5_eq_dhops projs(4))
    from ‹dip∈kD(rt)› rtn have [simp]: "sqn rt dip = dsn⇩n"
                           and [simp]: "the (dhops rt dip) = hops⇩n"
                           and [simp]: "the (flag rt dip) = f⇩n"
      by (simp add: sqn_def proj5_eq_dhops [symmetric]
                            proj4_eq_flag [symmetric])+

    from ‹update_arg_wf r› have "(dsn⇩n, dsk⇩n, f⇩n, hops⇩n, nhip⇩n, pre⇩n)
                                  ⊑ the ((update rt dip r) dip)"
      proof (rule wf_r_cases)
        fix nhip pre
        from ‹hops⇩n ≥ 1› have "⋀pre'. (dsn⇩n, dsk⇩n, f⇩n, hops⇩n, nhip⇩n, pre⇩n)
                                        ⊑ (dsn⇩n, unk, val, Suc 0, nhip, pre')"
          unfolding fresher_def sqn_def by (cases f⇩n) auto
        thus "(dsn⇩n, dsk⇩n, f⇩n, hops⇩n, nhip⇩n, pre⇩n)
               ⊑ the (update rt dip (0, unk, val, Suc 0, nhip, pre) dip)"
          using ‹dip∈kD(rt)› by - (rule update_cases_kD, simp_all)
      next
        fix dsn :: sqn and hops nhip pre
        assume "0 < dsn"
        show "(dsn⇩n, dsk⇩n, f⇩n, hops⇩n, nhip⇩n, pre⇩n)
               ⊑ the (update rt dip (dsn, kno, val, hops, nhip, pre) dip)"
        proof (rule update_cases_kD [OF _ ‹dip∈kD(rt)›], simp_all add: ‹0 < dsn›)
          assume "dsn⇩n < dsn"
            thus "(dsn⇩n, dsk⇩n, f⇩n, hops⇩n, nhip⇩n, pre⇩n)
                   ⊑ (dsn, kno, val, hops, nhip, pre ∪ pre⇩n)"
              unfolding fresher_def by auto
        next
          assume "dsn⇩n = dsn"
             and "hops < hops⇩n"
            thus "(dsn, dsk⇩n, f⇩n, hops⇩n, nhip⇩n, pre⇩n)
                   ⊑ (dsn, kno, val, hops, nhip, pre ∪ pre⇩n)"
              unfolding fresher_def nsqn⇩r_def by simp
        next
          assume "dsn⇩n = dsn"
            with ‹0 < dsn›
            show "(dsn, dsk⇩n, inv, hops⇩n, nhip⇩n, pre⇩n)
                   ⊑ (dsn, kno, val, hops, nhip, pre ∪ pre⇩n)"
              unfolding fresher_def by simp
        qed
      qed
    hence "rt ⊑⇘dip⇙ update rt dip r"
      by - (rule single_rt_fresher, simp)
    with ‹dip = ip› show ?thesis by simp
  qed

theorem rt_fresher_invalidate [simp]:
  assumes "dip∈kD(rt)"
      and indests: "∀rip∈dom(dests). rip∈vD(rt) ∧ sqn rt rip < the (dests rip)"
    shows "rt ⊑⇘dip⇙ invalidate rt dests"
  proof (cases "dip∈dom(dests)")
    assume "dip∉dom(dests)"
      thus ?thesis using ‹dip∈kD(rt)›
      by - (rule single_rt_fresher, simp)
  next
    assume "dip∈dom(dests)"
    moreover with indests have "dip∈vD(rt)"
                           and "sqn rt dip < the (dests dip)"
      by auto
    ultimately show ?thesis
      unfolding invalidate_def sqn_def
      by - (rule single_rt_fresher, auto simp: fresher_def)
  qed

lemma nsqn⇩r_invalidate [simp]:
  assumes "dip∈kD(rt)"
      and "dip∈dom(dests)"
    shows "nsqn⇩r (the (invalidate rt dests dip)) = the (dests dip) - 1"
  using assms unfolding invalidate_def by auto

lemma rt_fresh_as_inc_invalidate [simp]:
  assumes "dip∈kD(rt)"
      and "∀rip∈dom(dests). rip∈vD(rt) ∧ the (dests rip) = inc (sqn rt rip)"
    shows "rt ≈⇘dip⇙ invalidate rt dests"
  proof (cases "dip∈dom(dests)")
    assume "dip∉dom(dests)"
    with ‹dip∈kD(rt)› have "dip∈kD(invalidate rt dests)"
      by simp
    with ‹dip∈kD(rt)› show ?thesis
      by rule (simp_all add: ‹dip∉dom(dests)›)
  next
    assume "dip∈dom(dests)"
    with assms(2) have "dip∈vD(rt)"
                  and "the (dests dip) = inc (sqn rt dip)" by auto
    from ‹dip∈vD(rt)› have "dip∈kD(rt)" by simp
    moreover then have "dip∈kD(invalidate rt dests)" by simp
    ultimately show ?thesis
    proof (rule nsqn_rt_fresh_asI)
      from ‹dip∈vD(rt)› have "nsqn rt dip = sqn rt dip" by simp
      also have "sqn rt dip = nsqn⇩r (the (invalidate rt dests dip))"
      proof -
        from ‹dip∈kD(rt)› have "nsqn⇩r (the (invalidate rt dests dip)) = the (dests dip) - 1"
          using ‹dip∈dom(dests)› by (rule nsqn⇩r_invalidate)
        with ‹the (dests dip) = inc (sqn rt dip)›
          show "sqn rt dip = nsqn⇩r (the (invalidate rt dests dip))" by simp
      qed
      also from ‹dip∈kD(invalidate rt dests)›
        have "nsqn⇩r (the (invalidate rt dests dip)) = nsqn (invalidate rt dests) dip"
          by (simp add: kD_nsqn)
      finally show "nsqn rt dip = nsqn (invalidate rt dests) dip" .
    qed simp
  qed

lemmas rt_fresher_inc_invalidate [simp] = rt_fresh_as_inc_invalidate [THEN rt_fresh_asD1]

lemma rt_fresh_as_addpreRT [simp]:
  assumes "ip∈kD(rt)"
    shows "rt ≈⇘dip⇙ the (addpreRT rt ip npre)"
  using assms [THEN kD_Some] by (auto simp: addpreRT_def)

lemmas rt_fresher_addpreRT [simp] = rt_fresh_as_addpreRT [THEN rt_fresh_asD1]

subsection "Strictly comparing routing tables "

definition rt_strictly_fresher :: "ip ⇒ rt ⇒ rt ⇒ bool"
where
  "rt_strictly_fresher ≡ λdip rt1 rt2. (rt1 ⊑⇘dip⇙ rt2) ∧ ¬(rt1 ≈⇘dip⇙ rt2)"

abbreviation
   rt_strictly_fresher_syn :: "rt ⇒ ip ⇒ rt ⇒ bool" (‹(_/ ⊏⇘_⇙ _)›  [51, 999, 51] 50)
where
  "rt1 ⊏⇘i⇙ rt2 ≡ rt_strictly_fresher i rt1 rt2"

lemma rt_strictly_fresher_def'':
  "rt1 ⊏⇘i⇙ rt2 = ((rt1 ⊑⇘i⇙ rt2) ∧ ¬(rt2 ⊑⇘i⇙ rt1))"
  unfolding rt_strictly_fresher_def rt_fresh_as_def by auto

lemma rt_strictly_fresherI' [intro]:
  assumes "rt1 ⊑⇘i⇙ rt2"
      and "¬(rt2 ⊑⇘i⇙ rt1)"
    shows "rt1 ⊏⇘i⇙ rt2"
  using assms unfolding rt_strictly_fresher_def'' by simp

lemma rt_strictly_fresherE' [elim]:
  assumes "rt1 ⊏⇘i⇙ rt2"
      and "⟦ rt1 ⊑⇘i⇙ rt2; ¬(rt2 ⊑⇘i⇙ rt1) ⟧ ⟹ P rt1 rt2 i"
    shows "P rt1 rt2 i"
  using assms unfolding rt_strictly_fresher_def'' by simp

lemma rt_strictly_fresherI [intro]:
  assumes "rt1 ⊑⇘i⇙ rt2"
      and "¬(rt1 ≈⇘i⇙ rt2)"
    shows "rt1 ⊏⇘i⇙ rt2"
  unfolding rt_strictly_fresher_def using assms ..

lemmas rt_strictly_fresher_singleI [elim] = rt_strictly_fresherI [OF single_rt_fresher]

lemma rt_strictly_fresherE [elim]:
  assumes "rt1 ⊏⇘i⇙ rt2"
      and "⟦ rt1 ⊑⇘i⇙ rt2; ¬(rt1 ≈⇘i⇙ rt2) ⟧ ⟹ P rt1 rt2 i"
    shows "P rt1 rt2 i"
  using assms(1) unfolding rt_strictly_fresher_def
  by rule (erule(1) assms(2))

lemma rt_strictly_fresher_def':
  "rt1 ⊏⇘i⇙ rt2 =
     (nsqn⇩r (the (rt1 i)) < nsqn⇩r (the (rt2 i))
       ∨ (nsqn⇩r (the (rt1 i)) = nsqn⇩r (the (rt2 i)) ∧ π⇩5(the (rt1 i)) > π⇩5(the (rt2 i))))"
  unfolding rt_strictly_fresher_def'' rt_fresher_def fresher_def by auto

lemma rt_strictly_fresher_fresherD [dest]:
  assumes "rt1 ⊏⇘dip⇙ rt2"
    shows "the (rt1 dip) ⊑ the (rt2 dip)"
  using assms unfolding rt_strictly_fresher_def rt_fresher_def by auto

lemma rt_strictly_fresher_not_fresh_asD [dest]:
  assumes "rt1 ⊏⇘dip⇙ rt2"
    shows "¬ rt1 ≈⇘dip⇙ rt2"
  using assms unfolding rt_strictly_fresher_def by auto

lemma rt_strictly_fresher_trans [elim, trans]:
  assumes "rt1 ⊏⇘dip⇙ rt2"
      and "rt2 ⊏⇘dip⇙ rt3"
    shows "rt1 ⊏⇘dip⇙ rt3"
  using assms proof -
    from ‹rt1 ⊏⇘dip⇙ rt2› obtain "the (rt1 dip) ⊑ the (rt2 dip)" by auto
    also from ‹rt2 ⊏⇘dip⇙ rt3› obtain "the (rt2 dip) ⊑ the (rt3 dip)" by auto
    finally have "the (rt1 dip) ⊑ the (rt3 dip)" .

    moreover have "¬ (rt1 ≈⇘dip⇙ rt3)"
    proof -    
      from ‹rt1 ⊏⇘dip⇙ rt2› obtain "¬(the (rt2 dip) ⊑ the (rt1 dip))" by auto
      also from ‹rt2 ⊏⇘dip⇙ rt3› obtain "¬(the (rt3 dip) ⊑ the (rt2 dip))" by auto
      finally have "¬(the (rt3 dip) ⊑ the (rt1 dip))" .
      thus ?thesis ..
    qed
    ultimately show "rt1 ⊏⇘dip⇙ rt3" ..
 qed

lemma rt_strictly_fresher_irefl [simp]: "¬ (rt ⊏⇘dip⇙ rt)"
  unfolding rt_strictly_fresher_def
  by clarsimp

lemma rt_fresher_trans_rt_strictly_fresher [elim, trans]:
  assumes "rt1 ⊏⇘dip⇙ rt2"
      and "rt2 ⊑⇘dip⇙ rt3"
    shows "rt1 ⊏⇘dip⇙ rt3"
  proof -
    from ‹rt1 ⊏⇘dip⇙ rt2› have "rt1 ⊑⇘dip⇙ rt2"
                           and "¬(rt2 ⊑⇘dip⇙ rt1)"
      unfolding rt_strictly_fresher_def'' by auto
    from this(1) and ‹rt2 ⊑⇘dip⇙ rt3› have "rt1 ⊑⇘dip⇙ rt3" ..

    moreover from ‹¬(rt2 ⊑⇘dip⇙ rt1)› have "¬(rt3 ⊑⇘dip⇙ rt1)"
      proof (rule contrapos_nn)
        assume "rt3 ⊑⇘dip⇙ rt1"
        with ‹rt2 ⊑⇘dip⇙ rt3› show "rt2 ⊑⇘dip⇙ rt1" ..
      qed

    ultimately show "rt1 ⊏⇘dip⇙ rt3"
      unfolding rt_strictly_fresher_def'' by auto
  qed

lemma rt_fresher_trans_rt_strictly_fresher' [elim, trans]:
  assumes "rt1 ⊑⇘dip⇙ rt2"
      and "rt2 ⊏⇘dip⇙ rt3"
    shows "rt1 ⊏⇘dip⇙ rt3"
  proof -
    from ‹rt2 ⊏⇘dip⇙ rt3› have "rt2 ⊑⇘dip⇙ rt3"
                           and "¬(rt3 ⊑⇘dip⇙ rt2)"
      unfolding rt_strictly_fresher_def'' by auto
    from ‹rt1 ⊑⇘dip⇙ rt2› and this(1) have "rt1 ⊑⇘dip⇙ rt3" ..

    moreover from ‹¬(rt3 ⊑⇘dip⇙ rt2)› have "¬(rt3 ⊑⇘dip⇙ rt1)"
      proof (rule contrapos_nn)
        assume "rt3 ⊑⇘dip⇙ rt1"
        thus "rt3 ⊑⇘dip⇙ rt2" using ‹rt1 ⊑⇘dip⇙ rt2› ..
      qed

    ultimately show "rt1 ⊏⇘dip⇙ rt3"
      unfolding rt_strictly_fresher_def'' by auto
  qed

lemma rt_fresher_imp_nsqn_le:
  assumes "rt1 ⊑⇘ip⇙ rt2"
      and "ip ∈ kD rt1"
      and "ip ∈ kD rt2"
    shows "nsqn rt1 ip ≤ nsqn rt2 ip"
  using assms(1)
  by (auto simp add: rt_fresher_def2 [OF assms(2-3)])

lemma rt_strictly_fresher_ltI [intro]:
  assumes "dip ∈ kD(rt1)"
      and "dip ∈ kD(rt2)"
      and "nsqn rt1 dip < nsqn rt2 dip"
    shows "rt1 ⊏⇘dip⇙ rt2"
  proof
    from assms show "rt1 ⊑⇘dip⇙ rt2" ..
  next
    show "¬(rt1 ≈⇘dip⇙ rt2)"
    proof
      assume "rt1 ≈⇘dip⇙ rt2"
      hence "rt2 ⊑⇘dip⇙ rt1" ..
      hence "nsqn rt2 dip ≤ nsqn rt1 dip"
        using ‹dip ∈ kD(rt2)› ‹dip ∈ kD(rt1)›
        by (rule rt_fresher_imp_nsqn_le)
      with ‹nsqn rt1 dip < nsqn rt2 dip› show "False"
        by simp
    qed
  qed

lemma rt_strictly_fresher_eqI [intro]:
  assumes "i∈kD(rt1)"
      and "i∈kD(rt2)"
      and "nsqn rt1 i = nsqn rt2 i"
      and "π⇩5(the (rt2 i)) < π⇩5(the (rt1 i))"
    shows "rt1 ⊏⇘i⇙ rt2"
  using assms unfolding rt_strictly_fresher_def' by (auto simp add: kD_nsqn)

lemma invalidate_rtsf_left [simp]:
  "⋀dests dip rt rt'. dests dip = None ⟹ (invalidate rt dests ⊏⇘dip⇙ rt') = (rt ⊏⇘dip⇙ rt')"
  unfolding invalidate_def rt_strictly_fresher_def'
  by (rule iffI) (auto split: option.split_asm)

lemma vD_invalidate_rt_strictly_fresher [simp]:
  assumes "dip ∈ vD(invalidate rt1 dests)"
    shows "(invalidate rt1 dests ⊏⇘dip⇙ rt2) = (rt1 ⊏⇘dip⇙ rt2)"
  proof (cases "dip ∈ dom(dests)")
    assume "dip ∈ dom(dests)"
    hence "dip ∉ vD(invalidate rt1 dests)"
      unfolding invalidate_def vD_def
      by clarsimp (metis assms option.simps(3) vD_invalidate_vD_not_dests)
    with ‹dip ∈ vD(invalidate rt1 dests)› show ?thesis by simp
  next
    assume "dip ∉ dom(dests)"
    hence "dests dip = None" by auto
    moreover with ‹dip ∈ vD(invalidate rt1 dests)› have "dip ∈ vD(rt1)"
      unfolding invalidate_def vD_def
      by clarsimp (metis (opaque_lifting, no_types) assms vD_Some vD_invalidate_vD_not_dests)
    ultimately show ?thesis
      unfolding invalidate_def rt_strictly_fresher_def' by auto
  qed

lemma rt_strictly_fresher_update_other [elim!]:
  "⋀dip ip rt r rt'. ⟦ dip ≠ ip; rt ⊏⇘dip⇙ rt' ⟧ ⟹ update rt ip r ⊏⇘dip⇙ rt'"
  unfolding rt_strictly_fresher_def' by clarsimp

lemma addpreRT_strictly_fresher [simp]:
  assumes "dip ∈ kD(rt)"
    shows "(the (addpreRT rt dip npre) ⊏⇘ip⇙ rt2) = (rt ⊏⇘ip⇙ rt2)"
  using assms unfolding rt_strictly_fresher_def' by clarsimp

lemma lt_sqn_imp_update_strictly_fresher:
  assumes "dip ∈ vD (rt2 nhip)"
      and  *: "osn < sqn (rt2 nhip) dip"
      and **: "rt ≠ update rt dip (osn, kno, val, hops, nhip, {})"
    shows "update rt dip (osn, kno, val, hops, nhip, {}) ⊏⇘dip⇙ rt2 nhip"
  unfolding rt_strictly_fresher_def'
  proof (rule disjI1)
    from ** have "nsqn (update rt dip (osn, kno, val, hops, nhip, {})) dip = osn"
      by (rule nsqn_update_changed_kno_val)
    with ‹dip∈vD(rt2 nhip)›
      have "nsqn⇩r (the (update rt dip (osn, kno, val, hops, nhip, {}) dip)) = osn"
        by (simp add: kD_nsqn)
    also have "osn < sqn (rt2 nhip) dip" by (rule *)
    also have "sqn (rt2 nhip) dip = nsqn⇩r (the (rt2 nhip dip))"
      unfolding nsqn⇩r_def using ‹dip ∈ vD (rt2 nhip)›
      by - (metis vD_flag_val proj2_eq_sqn proj4_eq_flag vD_iD_gives_kD(1))
    finally show "nsqn⇩r (the (update rt dip (osn, kno, val, hops, nhip, {}) dip))
                                                              < nsqn⇩r (the (rt2 nhip dip))" .
  qed

lemma dhops_le_hops_imp_update_strictly_fresher:
  assumes "dip ∈ vD(rt2 nhip)"
      and sqn: "sqn (rt2 nhip) dip = osn"
      and hop: "the (dhops (rt2 nhip) dip) ≤ hops"
      and **: "rt ≠ update rt dip (osn, kno, val, Suc hops, nhip, {})"
    shows "update rt dip (osn, kno, val, Suc hops, nhip, {}) ⊏⇘dip⇙ rt2 nhip"
  unfolding rt_strictly_fresher_def'
  proof (rule disjI2, rule conjI)
    from ** have "nsqn (update rt dip (osn, kno, val, Suc hops, nhip, {})) dip = osn"
      by (rule nsqn_update_changed_kno_val)
    with ‹dip∈vD(rt2 nhip)›
      have "nsqn⇩r (the (update rt dip (osn, kno, val, Suc hops, nhip, {}) dip)) = osn"
        by (simp add: kD_nsqn)
    also have "osn = sqn (rt2 nhip) dip" by (rule sqn [symmetric])
    also have "sqn (rt2 nhip) dip = nsqn⇩r (the (rt2 nhip dip))"
      unfolding nsqn⇩r_def using ‹dip ∈ vD(rt2 nhip)›
      by - (metis vD_flag_val proj2_eq_sqn proj4_eq_flag vD_iD_gives_kD(1))
    finally show "nsqn⇩r (the (update rt dip (osn, kno, val, Suc hops, nhip, {}) dip))
                                                              = nsqn⇩r (the (rt2 nhip dip))" .
  next
    have "the (dhops (rt2 nhip) dip) ≤ hops" by (rule hop)
    also have "hops < hops + 1" by simp
    also have "hops + 1 = the (dhops (update rt dip (osn, kno, val, Suc hops, nhip, {})) dip)"
      using ** by simp
    finally have "the (dhops (rt2 nhip) dip)
                        < the (dhops (update rt dip (osn, kno, val, Suc hops, nhip, {})) dip)" .
    thus "π⇩5 (the (rt2 nhip dip)) < π⇩5 (the (update rt dip (osn, kno, val, Suc hops, nhip, {}) dip))"
      using ‹dip ∈ vD(rt2 nhip)› by (simp add: proj5_eq_dhops)
  qed

lemma nsqn_invalidate:
  assumes "dip ∈ kD(rt)"
      and "∀ip∈dom(dests). ip ∈ vD(rt) ∧ the (dests ip) = inc (sqn rt ip)"
    shows "nsqn (invalidate rt dests) dip = nsqn rt dip"
  proof -
    from ‹dip ∈ kD(rt)› have "dip ∈ kD(invalidate rt dests)" by simp

    from assms have "rt ≈⇘dip⇙ invalidate rt dests"
      by (rule rt_fresh_as_inc_invalidate)
    with ‹dip ∈ kD(rt)› ‹dip ∈ kD(invalidate rt dests)› show ?thesis
      by (simp add: kD_nsqn del: invalidate_kD_inv)
         (erule(2) rt_fresh_as_nsqnr)
  qed

end