Theory D_Fresher

(*  Title:       variants/d_fwdrreqs/Fresher.thy
Author:      Timothy Bourke, Inria
Author:      Peter Höfner, NICTA
*)

section "Quality relations between routes"

theory D_Fresher
imports D_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

"rt dip npre dip'. dip  kD(rt)
nsqnr (the (the (addpreRT rt dip npre) dip')) = nsqnr (the (rt dip'))"
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)

"rt dip npre dip'. dip  kD(rt)
nsqn (the (addpreRT rt dip npre)) dip' = nsqn rt dip'"
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

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)"
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)"
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
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  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
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"
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]

assumes "ipkD(rt)"
shows "rt ≈⇘dipthe (addpreRT rt ip npre)"
using assms [THEN kD_Some] by (auto simp: addpreRT_def)

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

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"
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"
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