Theory E_Loop_Freedom

(*  Title:       variants/e_all_abcd/Loop_Freedom.thy
    License:     BSD 2-Clause. See LICENSE.
    Author:      Timothy Bourke, Inria
    Author:      Peter Höfner, NICTA
*)

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) ⊏⇘diprt (σ nhip)"
    { fix ip ip'
      assume "(ip, ip')  (rt_graph σ dip)+"
         and "dip  vD(rt (σ ip'))"
         and "ip'  dip"
       hence "rt (σ ip) ⊏⇘diprt (σ 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) ⊏⇘diprt (σ 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) ⊏⇘diprt (σ 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) ⊏⇘diprt (σ nhip)" by (rule IH)
           also have "rt (σ nhip) ⊏⇘diprt (σ 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) ⊏⇘diprt (σ nhip')"
                   by (clarsimp simp: Let_def)
             qed
           finally show "rt (σ ip) ⊏⇘diprt (σ 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) ⊏⇘diprt (σ ip)" by (rule fresher)
      thus False by simp
    qed
  qed

end