Theory E_Loop_Freedom
section "Routing graphs and loop freedom"
theory E_Loop_Freedom
imports E_Aodv_Predicates E_Fresher
begin
text ‹Define the central theorem that relates an invariant over network states to the absence
of loops in the associate routing graph.›
definition
rt_graph :: "(ip ⇒ state) ⇒ ip ⇒ ip rel"
where
"rt_graph σ = (λdip.
{(ip, ip') | ip ip' dsn dsk hops.
ip ≠ dip ∧ rt (σ ip) dip = Some (dsn, dsk, val, hops, ip')})"
text ‹Given the state of a network @{term σ}, a routing graph for a given destination
ip address @{term dip} abstracts the details of routing tables into nodes
(ip addresses) and vertices (valid routes between ip addresses).›
lemma rt_graphE [elim]:
fixes n dip ip ip'
assumes "(ip, ip') ∈ rt_graph σ dip"
shows "ip ≠ dip ∧ (∃r. rt (σ ip) = r
∧ (∃dsn dsk hops. r dip = Some (dsn, dsk, val, hops, ip')))"
using assms unfolding rt_graph_def by auto
lemma rt_graph_vD [dest]:
"⋀ip ip' σ dip. (ip, ip') ∈ rt_graph σ dip ⟹ dip ∈ vD(rt (σ ip))"
unfolding rt_graph_def vD_def by auto
lemma rt_graph_vD_trans [dest]:
"⋀ip ip' σ dip. (ip, ip') ∈ (rt_graph σ dip)⇧+ ⟹ dip ∈ vD(rt (σ ip))"
by (erule converse_tranclE) auto
lemma rt_graph_not_dip [dest]:
"⋀ip ip' σ dip. (ip, ip') ∈ rt_graph σ dip ⟹ ip ≠ dip"
unfolding rt_graph_def by auto
lemma rt_graph_not_dip_trans [dest]:
"⋀ip ip' σ dip. (ip, ip') ∈ (rt_graph σ dip)⇧+ ⟹ ip ≠ dip"
by (erule converse_tranclE) auto
text "NB: the property below cannot be lifted to the transitive closure"
lemma rt_graph_nhip_is_nhop [dest]:
"⋀ip ip' σ dip. (ip, ip') ∈ rt_graph σ dip ⟹ ip' = the (nhop (rt (σ ip)) dip)"
unfolding rt_graph_def by auto
theorem inv_to_loop_freedom:
assumes "∀i dip. let nhip = the (nhop (rt (σ i)) dip)
in dip ∈ vD (rt (σ i)) ∩ vD (rt (σ nhip)) ∧ nhip ≠ dip
⟶ (rt (σ i)) ⊏⇘dip⇙ (rt (σ nhip))"
shows "∀dip. irrefl ((rt_graph σ dip)⇧+)"
using assms proof (intro allI)
fix σ :: "ip ⇒ state" and dip
assume inv: "∀ip dip.
let nhip = the (nhop (rt (σ ip)) dip)
in dip ∈ vD(rt (σ ip)) ∩ vD(rt (σ nhip)) ∧
nhip ≠ dip ⟶ rt (σ ip) ⊏⇘dip⇙ rt (σ nhip)"
{ fix ip ip'
assume "(ip, ip') ∈ (rt_graph σ dip)⇧+"
and "dip ∈ vD(rt (σ ip'))"
and "ip' ≠ dip"
hence "rt (σ ip) ⊏⇘dip⇙ rt (σ ip')"
proof induction
fix nhip
assume "(ip, nhip) ∈ rt_graph σ dip"
and "dip ∈ vD(rt (σ nhip))"
and "nhip ≠ dip"
from ‹(ip, nhip) ∈ rt_graph σ dip› have "dip ∈ vD(rt (σ ip))"
and "nhip = the (nhop (rt (σ ip)) dip)"
by auto
from ‹dip ∈ vD(rt (σ ip))› and ‹dip ∈ vD(rt (σ nhip))›
have "dip ∈ vD(rt (σ ip)) ∩ vD(rt (σ nhip))" ..
with ‹nhip = the (nhop (rt (σ ip)) dip)›
and ‹nhip ≠ dip›
and inv
show "rt (σ ip) ⊏⇘dip⇙ rt (σ nhip)"
by (clarsimp simp: Let_def)
next
fix nhip nhip'
assume "(ip, nhip) ∈ (rt_graph σ dip)⇧+"
and "(nhip, nhip') ∈ rt_graph σ dip"
and IH: "⟦ dip ∈ vD(rt (σ nhip)); nhip ≠ dip ⟧ ⟹ rt (σ ip) ⊏⇘dip⇙ rt (σ nhip)"
and "dip ∈ vD(rt (σ nhip'))"
and "nhip' ≠ dip"
from ‹(nhip, nhip') ∈ rt_graph σ dip› have 1: "dip ∈ vD(rt (σ nhip))"
and 2: "nhip ≠ dip"
and "nhip' = the (nhop (rt (σ nhip)) dip)"
by auto
from 1 2 have "rt (σ ip) ⊏⇘dip⇙ rt (σ nhip)" by (rule IH)
also have "rt (σ nhip) ⊏⇘dip⇙ rt (σ nhip')"
proof -
from ‹dip ∈ vD(rt (σ nhip))› and ‹dip ∈ vD(rt (σ nhip'))›
have "dip ∈ vD(rt (σ nhip)) ∩ vD(rt (σ nhip'))" ..
with ‹nhip' ≠ dip›
and ‹nhip' = the (nhop (rt (σ nhip)) dip)›
and inv
show "rt (σ nhip) ⊏⇘dip⇙ rt (σ nhip')"
by (clarsimp simp: Let_def)
qed
finally show "rt (σ ip) ⊏⇘dip⇙ rt (σ nhip')" .
qed } note fresher = this
show "irrefl ((rt_graph σ dip)⇧+)"
unfolding irrefl_def proof (intro allI notI)
fix ip
assume "(ip, ip) ∈ (rt_graph σ dip)⇧+"
moreover then have "dip ∈ vD(rt (σ ip))"
and "ip ≠ dip"
by auto
ultimately have "rt (σ ip) ⊏⇘dip⇙ rt (σ ip)" by (rule fresher)
thus False by simp
qed
qed
end