(* Title: variants/b_fwdrreps/Fresher.thy License: BSD 2-Clause. See LICENSE. Author: Timothy Bourke, Inria *) 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