(*  Title:       Loop_Freedom.thy
    License:     BSD 2-Clause. See LICENSE.
    Author:      Timothy Bourke, Inria
*)

section "Routing graphs and loop freedom"

theory Loop_Freedom
imports Aodv_Predicates 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 pre.
        ip ≠ dip ∧ rt (σ ip) dip = Some (dsn, dsk, val, hops, ip', pre)})"

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 pre. r dip = Some (dsn, dsk, val, hops, ip', pre)))"
  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)) ⊏ (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) ⊏ rt (σ nhip)"
    { fix ip ip'
      assume "(ip, ip') ∈ (rt_graph σ dip)⁺"
         and "dip ∈ vD(rt (σ ip'))"
         and "ip' ≠ dip"
       hence "rt (σ ip) ⊏ 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) ⊏ 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) ⊏ 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) ⊏ rt (σ nhip)" by (rule IH)
           also have "rt (σ nhip) ⊏ 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) ⊏ rt (σ nhip')"
                   by (clarsimp simp: Let_def)
             qed
           finally show "rt (σ ip) ⊏ 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) ⊏ rt (σ ip)" by (rule fresher)
      thus False by simp
    qed
  qed

end