Theory B_Fresher
section "Quality relations between routes"
theory B_Fresher
imports B_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