Theory A_Fresher

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

section "Quality relations between routes"

theory A_Fresher
imports A_Aodv_Data
begin

subsection "Net sequence numbers"

subsubsection "On individual routes"

definition
  nsqnr :: "r  sqn"
where
  "nsqnr r  if π4(r) = val  π2(r) = 0 then π2(r) else (π2(r) - 1)"

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

lemma nsqnr_zero [simp]:
  "dsn dsk flag hops nhip pre. nsqnr (0, dsk, flag, hops, nhip, pre) = 0"
  unfolding nsqnr_def by clarsimp

lemma nsqnr_val [simp]:
  "dsn dsk hops nhip pre. nsqnr (dsn, dsk, val, hops, nhip, pre) = dsn"
  unfolding nsqnr_def by clarsimp

lemma nsqnr_inv [simp]:
  "dsn dsk hops nhip pre. nsqnr (dsn, dsk, inv, hops, nhip, pre) = dsn - 1"
  unfolding nsqnr_def by clarsimp

lemma nsqnr_lte_dsn [simp]:
  "dsn dsk flag hops nhip pre. nsqnr (dsn, dsk, flag, hops, nhip, pre)  dsn"
  unfolding nsqnr_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  nsqnr(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 = nsqnr(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 (nsqnr (dsn, dsk, val, hops, nhip, pre))"
      and "P (nsqnr (dsn, dsk, inv, hops, nhip, pre))"
    shows "P (nsqnr (dsn, dsk, flag, hops, nhip, pre))"
  using assms by (cases flag) auto

lemma nsqnr_addpreRT_inv [simp]:
  "rt dip npre dip'. dip  kD(rt) 
   nsqnr (the (the (addpreRT rt dip npre) dip')) = nsqnr (the (rt dip'))"
  unfolding addpreRT_def nsqnr_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 "ipkD(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 "ipvD(rt)"
    shows "nsqn rt ip = sqn rt ip"
  proof -
    from ipvD(rt) have "ipkD(rt)"
                      and "the (flag rt ip) = val" by auto
    thus ?thesis ..
  qed

lemma inv_nsqn_sqn [elim, simp]:
  assumes "ipkD(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 "ipiD(rt)"
    shows "nsqn rt ip = sqn rt ip - 1"
  proof -
    from ipiD(rt) have "ipkD(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 nsqnr_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 nsqnr_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 "dipkD(rt)"
      and "dipdom 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'  ((nsqnr r < nsqnr r')  (nsqnr r  = nsqnr r'  π5(r)  π5(r')))"

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

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

lemma fresherI [intro]:
  assumes "(nsqnr r < nsqnr r')  (nsqnr r  = nsqnr r'  π5(r)  π5(r'))"
    shows "r  r'"
  unfolding fresher_def using assms .

lemma fresherE [elim]:
  assumes "r  r'"
      and "nsqnr r < nsqnr r'  P r r'"
      and "nsqnr r  = nsqnr 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 ⊑⇘irt2  rt_fresher i rt1 rt2"

lemma rt_fresher_def':
  "(rt1 ⊑⇘irt2) = (nsqnr (the (rt1 i)) < nsqnr (the (rt2 i)) 
                     nsqnr (the (rt1 i)) = nsqnr (the (rt2 i))  π5 (the (rt2 i))  π5 (the (rt1 i)))"
  unfolding rt_fresher_def fresher_def by (rule refl)

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

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

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

lemma rt_fresher_trans [elim, trans]:
  assumes "rt1 ⊑⇘diprt2"
      and "rt2 ⊑⇘diprt3"
    shows "rt1 ⊑⇘diprt3"
  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 ⊑⇘diprt2)  (rt2 ⊑⇘diprt1)"

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

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

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

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

lemma rt_fresh_as_fresherI [intro]:
  assumes "dipkD(rt1)"
      and "dipkD(rt2)"
      and "the (rt1 dip)  the (rt2 dip)"
      and "the (rt2 dip)  the (rt1 dip)"
    shows "rt1 ≈⇘diprt2"
  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 ≈⇘diprt'"
  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 ⊑⇘diprt'"
      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' ⊑⇘diprt"
      by (rule rt_fresherI2)
  qed

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

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

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

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

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

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

lemma rt_fresh_as_nsqnr:
  assumes "dip  kD(rt1)"
      and "dip  kD(rt2)"
      and "rt1 ≈⇘diprt2"
    shows "nsqnr (the (rt2 dip)) = nsqnr (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 "dipkD(rt)"
      and "the (rt dip)  r"
    shows "rt ⊑⇘diprt(dip  r)"
  using assms unfolding rt_fresher_def by simp

lemma rt_fresher_map_update_other [intro!]:
  assumes "dipkD(rt)"
      and "dip  ip"
    shows "rt ⊑⇘diprt(ip  r)"
  using assms unfolding rt_fresher_def by simp

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

theorem rt_fresher_update [simp]:
  assumes "dipkD(rt)"
      and "the (dhops rt dip)  1"
      and "update_arg_wf r"
   shows "rt ⊑⇘dipupdate rt ip r"
  proof (cases "dip = ip")
    assume "dip  ip" with dipkD(rt) show ?thesis
      by (rule rt_fresher_update_other)
  next
    assume "dip = ip"

    from dipkD(rt) obtain dsnn dskn fn hopsn nhipn pren
      where rtn [simp]: "the (rt dip) = (dsnn, dskn, fn, hopsn, nhipn, pren)"
      by (metis prod_cases6)
    with the (dhops rt dip)  1 and dipkD(rt) have "hopsn  1"
      by (metis proj5_eq_dhops projs(4))
    from dipkD(rt) rtn have [simp]: "sqn rt dip = dsnn"
                           and [simp]: "the (dhops rt dip) = hopsn"
                           and [simp]: "the (flag rt dip) = fn"
      by (simp add: sqn_def proj5_eq_dhops [symmetric]
                            proj4_eq_flag [symmetric])+

    from update_arg_wf r have "(dsnn, dskn, fn, hopsn, nhipn, pren)
                                   the ((update rt dip r) dip)"
      proof (rule wf_r_cases)
        fix nhip pre
        from hopsn  1 have "pre'. (dsnn, dskn, fn, hopsn, nhipn, pren)
                                         (dsnn, unk, val, Suc 0, nhip, pre')"
          unfolding fresher_def sqn_def by (cases fn) auto
        thus "(dsnn, dskn, fn, hopsn, nhipn, pren)
                the (update rt dip (0, unk, val, Suc 0, nhip, pre) dip)"
          using dipkD(rt) by - (rule update_cases_kD, simp_all)
      next
        fix dsn :: sqn and hops nhip pre
        assume "0 < dsn"
        show "(dsnn, dskn, fn, hopsn, nhipn, pren)
                the (update rt dip (dsn, kno, val, hops, nhip, pre) dip)"
        proof (rule update_cases_kD [OF _ dipkD(rt)], simp_all add: 0 < dsn)
          assume "dsnn < dsn"
            thus "(dsnn, dskn, fn, hopsn, nhipn, pren)
                    (dsn, kno, val, hops, nhip, pre  pren)"
              unfolding fresher_def by auto
        next
          assume "dsnn = dsn"
             and "hops < hopsn"
            thus "(dsn, dskn, fn, hopsn, nhipn, pren)
                    (dsn, kno, val, hops, nhip, pre  pren)"
              unfolding fresher_def nsqnr_def by simp
        next
          assume "dsnn = dsn"
            with 0 < dsn
            show "(dsn, dskn, inv, hopsn, nhipn, pren)
                    (dsn, kno, val, hops, nhip, pre  pren)"
              unfolding fresher_def by simp
        qed
      qed
    hence "rt ⊑⇘dipupdate rt dip r"
      by - (rule single_rt_fresher, simp)
    with dip = ip show ?thesis by simp
  qed

theorem rt_fresher_invalidate [simp]:
  assumes "dipkD(rt)"
      and indests: "ripdom(dests). ripvD(rt)  sqn rt rip < the (dests rip)"
    shows "rt ⊑⇘dipinvalidate rt dests"
  proof (cases "dipdom(dests)")
    assume "dipdom(dests)"
      thus ?thesis using dipkD(rt)
      by - (rule single_rt_fresher, simp)
  next
    assume "dipdom(dests)"
    moreover with indests have "dipvD(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 nsqnr_invalidate [simp]:
  assumes "dipkD(rt)"
      and "dipdom(dests)"
    shows "nsqnr (the (invalidate rt dests dip)) = the (dests dip) - 1"
  using assms unfolding invalidate_def by auto

lemma rt_fresh_as_inc_invalidate [simp]:
  assumes "dipkD(rt)"
      and "ripdom(dests). ripvD(rt)  the (dests rip) = inc (sqn rt rip)"
    shows "rt ≈⇘dipinvalidate rt dests"
  proof (cases "dipdom(dests)")
    assume "dipdom(dests)"
    with dipkD(rt) have "dipkD(invalidate rt dests)"
      by simp
    with dipkD(rt) show ?thesis
      by rule (simp_all add: dipdom(dests))
  next
    assume "dipdom(dests)"
    with assms(2) have "dipvD(rt)"
                  and "the (dests dip) = inc (sqn rt dip)" by auto
    from dipvD(rt) have "dipkD(rt)" by simp
    moreover then have "dipkD(invalidate rt dests)" by simp
    ultimately show ?thesis
    proof (rule nsqn_rt_fresh_asI)
      from dipvD(rt) have "nsqn rt dip = sqn rt dip" by simp
      also have "sqn rt dip = nsqnr (the (invalidate rt dests dip))"
      proof -
        from dipkD(rt) have "nsqnr (the (invalidate rt dests dip)) = the (dests dip) - 1"
          using dipdom(dests) by (rule nsqnr_invalidate)
        with the (dests dip) = inc (sqn rt dip)
          show "sqn rt dip = nsqnr (the (invalidate rt dests dip))" by simp
      qed
      also from dipkD(invalidate rt dests)
        have "nsqnr (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 "ipkD(rt)"
    shows "rt ≈⇘dipthe (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 ⊑⇘diprt2)  ¬(rt1 ≈⇘diprt2)"

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

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

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

lemma rt_strictly_fresherE' [elim]:
  assumes "rt1 ⊏⇘irt2"
      and " rt1 ⊑⇘irt2; ¬(rt2 ⊑⇘irt1)   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 ⊑⇘irt2"
      and "¬(rt1 ≈⇘irt2)"
    shows "rt1 ⊏⇘irt2"
  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 ⊏⇘irt2"
      and " rt1 ⊑⇘irt2; ¬(rt1 ≈⇘irt2)   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 ⊏⇘irt2 =
     (nsqnr (the (rt1 i)) < nsqnr (the (rt2 i))
        (nsqnr (the (rt1 i)) = nsqnr (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 ⊏⇘diprt2"
    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 ⊏⇘diprt2"
    shows "¬ rt1 ≈⇘diprt2"
  using assms unfolding rt_strictly_fresher_def by auto

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

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

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

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

    moreover from ¬(rt2 ⊑⇘diprt1) have "¬(rt3 ⊑⇘diprt1)"
      proof (rule contrapos_nn)
        assume "rt3 ⊑⇘diprt1"
        with rt2 ⊑⇘diprt3 show "rt2 ⊑⇘diprt1" ..
      qed

    ultimately show "rt1 ⊏⇘diprt3"
      unfolding rt_strictly_fresher_def'' by auto
  qed

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

    moreover from ¬(rt3 ⊑⇘diprt2) have "¬(rt3 ⊑⇘diprt1)"
      proof (rule contrapos_nn)
        assume "rt3 ⊑⇘diprt1"
        thus "rt3 ⊑⇘diprt2" using rt1 ⊑⇘diprt2 ..
      qed

    ultimately show "rt1 ⊏⇘diprt3"
      unfolding rt_strictly_fresher_def'' by auto
  qed

lemma rt_fresher_imp_nsqn_le:
  assumes "rt1 ⊑⇘iprt2"
      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 ⊏⇘diprt2"
  proof
    from assms show "rt1 ⊑⇘diprt2" ..
  next
    show "¬(rt1 ≈⇘diprt2)"
    proof
      assume "rt1 ≈⇘diprt2"
      hence "rt2 ⊑⇘diprt1" ..
      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 "ikD(rt1)"
      and "ikD(rt2)"
      and "nsqn rt1 i = nsqn rt2 i"
      and "π5(the (rt2 i)) < π5(the (rt1 i))"
    shows "rt1 ⊏⇘irt2"
  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 ⊏⇘diprt') = (rt ⊏⇘diprt')"
  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 ⊏⇘diprt2) = (rt1 ⊏⇘diprt2)"
  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 ⊏⇘diprt'   update rt ip r ⊏⇘diprt'"
  unfolding rt_strictly_fresher_def' by clarsimp

lemma addpreRT_strictly_fresher [simp]:
  assumes "dip  kD(rt)"
    shows "(the (addpreRT rt dip npre) ⊏⇘iprt2) = (rt ⊏⇘iprt2)"
  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, {}) ⊏⇘diprt2 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 dipvD(rt2 nhip)
      have "nsqnr (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 = nsqnr (the (rt2 nhip dip))"
      unfolding nsqnr_def using dip  vD (rt2 nhip)
      by - (metis vD_flag_val proj2_eq_sqn proj4_eq_flag vD_iD_gives_kD(1))
    finally show "nsqnr (the (update rt dip (osn, kno, val, hops, nhip, {}) dip))
                                                              < nsqnr (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, {}) ⊏⇘diprt2 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 dipvD(rt2 nhip)
      have "nsqnr (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 = nsqnr (the (rt2 nhip dip))"
      unfolding nsqnr_def using dip  vD(rt2 nhip)
      by - (metis vD_flag_val proj2_eq_sqn proj4_eq_flag vD_iD_gives_kD(1))
    finally show "nsqnr (the (update rt dip (osn, kno, val, Suc hops, nhip, {}) dip))
                                                              = nsqnr (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 "ipdom(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 ≈⇘dipinvalidate 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