Quelle  Fresher.thy

(*  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 π₄(r) = val ∨ π₂(r) = 0 then π₂(r) else (π₂(r) - 1)"

lemma nsqnr_def':
  "nsqn_r r = (if π₄(r) = inv then π₂(r) - 1 else π₂(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 σ(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 (σ(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' ∧ π₅(r) ≥ π₅(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 "π₅(r) ≥ π₅(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' ∧ π₅(r) ≥ π₅(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' ∧ π₅(r) ≥ π₅(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 (σ(rt, dip))) ⊑ (the (σ(rt', dip)))"

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

lemma rt_fresher_def':
  "(rt₁ ⊑ rt₂) = (nsqn_r (the (rt₁ i)) < nsqn_r (the (rt₂ i)) ∨
                     nsqn_r (the (rt₁ i)) = nsqn_r (the (rt₂ i)) ∧ π₅ (the (rt₂ i)) ≤ π₅ (the (rt₁ i)))"
  unfolding rt_fresher_def fresher_def by (rule refl)

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

lemma rt_fresher_single [intro]:
  assumes "rt1 ⊑ 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 ⊑ 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 ⊑ 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 ⊑ rt2"
  unfolding rt_fresher_def2 [OF assms(1-2)] using assms(3-4) by simp

lemma rt_fresherE [elim]:
  assumes "rt1 ⊑ 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 ⊑ rt"
  unfolding rt_fresher_def by simp

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

lemma rt_fresher_if_Some [intro!]:
  assumes "the (rt dip) ⊑ r"
    shows "rt ⊑ (λ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 ⊑ rt2) ∧ (rt2 ⊑ rt1)"

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

lemma rt_fresh_as_refl [simp]: "∧rt dip. rt ≈ rt"
  unfolding rt_fresh_as_def by simp

lemma rt_fresh_as_trans [simp, intro, trans]:
  "∧rt1 rt2 rt3 dip. [ rt1 ≈ rt2; rt2 ≈ rt3 ] ==> rt1 ≈ rt3"
  unfolding rt_fresh_as_def rt_fresher_def
  by (metis (mono_tags) fresher_trans)

lemma rt_fresh_asI [intro!]:
  assumes "rt1 ⊑ rt2"
      and "rt2 ⊑ rt1"
    shows "rt1 ≈ 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 ≈ 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 "π₅(the (rt dip)) = π₅(the (rt' dip))"
    shows "rt ≈ 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 ⊑ 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' ⊑ rt"
      by (rule rt_fresherI2)
  qed

lemma rt_fresh_asE [elim]:
  assumes "rt1 ≈ rt2"
      and "[ rt1 ⊑ rt2; rt2 ⊑ 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 ≈ rt2"
    shows "rt1 ⊑ rt2"
  using assms unfolding rt_fresh_as_def by simp

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

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

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

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

lemma not_single_rt_fresher [elim]:
  assumes "¬(the (rt1 ip) ⊑ the (rt2 ip))"
    shows "¬(rt1 ⊑ rt2)"
  proof
    assume "rt1 ⊑ 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 ⊑ rt2)"
    shows "¬(the (rt1 ip) ⊑ the (rt2 ip))"
  proof
    assume "the (rt1 ip) ⊑ the (rt2 ip)"
    hence "rt1 ⊑ rt2" ..
    with ‹¬(rt1 ⊑ rt2)› show False ..
  qed

lemma rt_fresh_as_nsqnr:
  assumes "dip ∈ kD(rt1)"
      and "dip ∈ kD(rt2)"
      and "rt1 ≈ 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 ⊑ 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 ⊑ 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 ⊑ 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 ⊑ 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 ⊑ 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 ⊑ 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 ≈ 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 ≈ 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 ⊑ rt2) ∧ ¬(rt1 ≈ rt2)"

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

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

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

lemma rt_strictly_fresherE' [elim]:
  assumes "rt1 ⊏ rt2"
      and "[ rt1 ⊑ rt2; ¬(rt2 ⊑ 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 ⊑ rt2"
      and "¬(rt1 ≈ rt2)"
    shows "rt1 ⊏ 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 ⊏ rt2"
      and "[ rt1 ⊑ rt2; ¬(rt1 ≈ 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 ⊏ rt2 =
     (nsqn_r (the (rt1 i)) < nsqn_r (the (rt2 i))
       ∨ (nsqn_r (the (rt1 i)) = nsqn_r (the (rt2 i)) ∧ π₅(the (rt1 i)) > π₅(the (rt2 i))))"
  unfolding rt_strictly_fresher_def'' rt_fresher_def fresher_def by auto

lemma rt_strictly_fresher_fresherD [dest]:
  assumes "rt1 ⊏ 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 ⊏ rt2"
    shows "¬ rt1 ≈ rt2"
  using assms unfolding rt_strictly_fresher_def by auto

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

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

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

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

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

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

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

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

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

lemma rt_fresher_imp_nsqn_le:
  assumes "rt1 ⊑ 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 ⊏ rt2"
  proof
    from assms show "rt1 ⊑ rt2" ..
  next
    show "¬(rt1 ≈ rt2)"
    proof
      assume "rt1 ≈ rt2"
      hence "rt2 ⊑ 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 "π₅(the (rt2 i)) < π₅(the (rt1 i))"
    shows "rt1 ⊏ 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 ⊏ rt') = (rt ⊏ 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 ⊏ rt2) = (rt1 ⊏ 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 ⊏ rt' ] ==> update rt ip r ⊏ rt'"
  unfolding rt_strictly_fresher_def' by clarsimp

lemma addpreRT_strictly_fresher [simp]:
  assumes "dip ∈ kD(rt)"
    shows "(the (addpreRT rt dip npre) ⊏ rt2) = (rt ⊏ 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, {}) ⊏ 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, {}) ⊏ 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 "π₅ (the (rt2 nhip dip)) < π₅ (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 ≈ 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