Quelle  Aodv.thy

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

section "The AODV protocol"

theory Aodv
imports Aodv_Data Aodv_Message
        AWN.AWN_SOS_Labels AWN.AWN_Invariants
begin

subsection "Data state"

record state =
  ip    :: "ip"
  sn    :: "sqn"
  rt    :: "rt" 
  rreqs :: "(ip × rreqid) set"
  store :: "store"
  (* all locals *)
  msg    :: "msg"
  data   :: "data"
  dests  :: "ip ⇀ sqn"
  pre    :: "ip set"
  rreqid :: "rreqid"
  dip    :: "ip"
  oip    :: "ip"
  hops   :: "nat"
  dsn    :: "sqn"
  dsk    :: "k"
  osn    :: "sqn"
  sip    :: "ip"

abbreviation aodv_init :: "ip ==> state"
where "aodv_init i ≡ (
         ip = i,
         sn = 1,
         rt = Map.empty,
         rreqs = {},
         store = Map.empty,

         msg = (SOME x. True),
         data = (SOME x. True),
         dests = (SOME x. True),
         pre = (SOME x. True),
         rreqid = (SOME x. True),
         dip = (SOME x. True),
         oip = (SOME x. True),
         hops = (SOME x. True),
         dsn = (SOME x. True),
         dsk = (SOME x. True),
         osn = (SOME x. True),
         sip = (SOME x. x ≠ i)
       )"

lemma some_neq_not_eq [simp]: "¬((SOME x :: nat. x ≠ i) = i)"
  by (subst some_eq_ex) (metis zero_neq_numeral)

definition clear_locals :: "state ==> state"
where "clear_locals ξ = ξ (
    msg := (SOME x. True),
    data := (SOME x. True),
    dests := (SOME x. True),
    pre := (SOME x. True),
    rreqid := (SOME x. True),
    dip := (SOME x. True),
    oip := (SOME x. True),
    hops := (SOME x. True),
    dsn := (SOME x. True),
    dsk := (SOME x. True),
    osn := (SOME x. True),
    sip := (SOME x. x ≠ ip ξ)
  )"

lemma clear_locals_sip_not_ip [simp]: "¬(sip (clear_locals ξ) = ip ξ)"
  unfolding clear_locals_def by simp

lemma clear_locals_but_not_globals [simp]:
  "ip (clear_locals ξ) = ip ξ"
  "sn (clear_locals ξ) = sn ξ"
  "rt (clear_locals ξ) = rt ξ"
  "rreqs (clear_locals ξ) = rreqs ξ"
  "store (clear_locals ξ) = store ξ"
  unfolding clear_locals_def by auto

subsection "Auxilliary message handling definitions"

definition is_newpkt
where "is_newpkt ξ ≡ case msg ξ of
                       Newpkt data' dip' ==> { ξ(data := data', dip := dip') }
                     | _ ==> {}"

definition is_pkt
where "is_pkt ξ ≡ case msg ξ of
                    Pkt data' dip' oip' ==> { ξ( data := data', dip := dip', oip := oip' ) }
                  | _ ==> {}"

definition is_rreq
where "is_rreq ξ ≡ case msg ξ of
                     Rreq hops' rreqid' dip' dsn' dsk' oip' osn' sip' ==>
                       { ξ( hops := hops', rreqid := rreqid', dip := dip', dsn := dsn',
                            dsk := dsk', oip := oip', osn := osn', sip := sip' ) }
                   | _ ==> {}"

lemma is_rreq_asm [dest!]:
  assumes "ξ' ∈ is_rreq ξ"
    shows "(∃hops' rreqid' dip' dsn' dsk' oip' osn' sip'.
               msg ξ = Rreq hops' rreqid' dip' dsn' dsk' oip' osn' sip' ∧
               ξ' = ξ( hops := hops', rreqid := rreqid', dip := dip', dsn := dsn',
                       dsk := dsk', oip := oip', osn := osn', sip := sip' ))"
  using assms unfolding is_rreq_def
  by (cases "msg ξ") simp_all

definition is_rrep
where "is_rrep ξ ≡ case msg ξ of
                     Rrep hops' dip' dsn' oip' sip' ==>
                       { ξ( hops := hops', dip := dip', dsn := dsn', oip := oip', sip := sip' ) }
                   | _ ==> {}"

lemma is_rrep_asm [dest!]:
  assumes "ξ' ∈ is_rrep ξ"
    shows "(∃hops' dip' dsn' oip' sip'.
               msg ξ = Rrep hops' dip' dsn' oip' sip' ∧
               ξ' = ξ( hops := hops', dip := dip', dsn := dsn', oip := oip', sip := sip' ))"
  using assms unfolding is_rrep_def
  by (cases "msg ξ") simp_all

definition is_rerr
where "is_rerr ξ ≡ case msg ξ of
                     Rerr dests' sip' ==> { ξ( dests := dests', sip := sip' ) }
                   | _ ==> {}"

lemma is_rerr_asm [dest!]:
  assumes "ξ' ∈ is_rerr ξ"
    shows "(∃dests' sip'.
               msg ξ = Rerr dests' sip' ∧
               ξ' = ξ( dests := dests', sip := sip' ))"
  using assms unfolding is_rerr_def
  by (cases "msg ξ") simp_all

lemmas is_msg_defs =
  is_rerr_def is_rrep_def is_rreq_def is_pkt_def is_newpkt_def

lemma is_msg_inv_ip [simp]:
  "ξ' ∈ is_rerr ξ ==> ip ξ' = ip ξ"
  "ξ' ∈ is_rrep ξ ==> ip ξ' = ip ξ"
  "ξ' ∈ is_rreq ξ ==> ip ξ' = ip ξ"
  "ξ' ∈ is_pkt ξ ==> ip ξ' = ip ξ"
  "ξ' ∈ is_newpkt ξ ==> ip ξ' = ip ξ"
  unfolding is_msg_defs
  by (cases "msg ξ", clarsimp+)+

lemma is_msg_inv_sn [simp]:
  "ξ' ∈ is_rerr ξ ==> sn ξ' = sn ξ"
  "ξ' ∈ is_rrep ξ ==> sn ξ' = sn ξ"
  "ξ' ∈ is_rreq ξ ==> sn ξ' = sn ξ"
  "ξ' ∈ is_pkt ξ ==> sn ξ' = sn ξ"
  "ξ' ∈ is_newpkt ξ ==> sn ξ' = sn ξ"
  unfolding is_msg_defs
  by (cases "msg ξ", clarsimp+)+

lemma is_msg_inv_rt [simp]:
  "ξ' ∈ is_rerr ξ ==> rt ξ' = rt ξ"
  "ξ' ∈ is_rrep ξ ==> rt ξ' = rt ξ"
  "ξ' ∈ is_rreq ξ ==> rt ξ' = rt ξ"
  "ξ' ∈ is_pkt ξ ==> rt ξ' = rt ξ"
  "ξ' ∈ is_newpkt ξ ==> rt ξ' = rt ξ"
  unfolding is_msg_defs
  by (cases "msg ξ", clarsimp+)+

lemma is_msg_inv_rreqs [simp]:
  "ξ' ∈ is_rerr ξ ==> rreqs ξ' = rreqs ξ"
  "ξ' ∈ is_rrep ξ ==> rreqs ξ' = rreqs ξ"
  "ξ' ∈ is_rreq ξ ==> rreqs ξ' = rreqs ξ"
  "ξ' ∈ is_pkt ξ ==> rreqs ξ' = rreqs ξ"
  "ξ' ∈ is_newpkt ξ ==> rreqs ξ' = rreqs ξ"
  unfolding is_msg_defs
  by (cases "msg ξ", clarsimp+)+

lemma is_msg_inv_store [simp]:
  "ξ' ∈ is_rerr ξ ==> store ξ' = store ξ"
  "ξ' ∈ is_rrep ξ ==> store ξ' = store ξ"
  "ξ' ∈ is_rreq ξ ==> store ξ' = store ξ"
  "ξ' ∈ is_pkt ξ ==> store ξ' = store ξ"
  "ξ' ∈ is_newpkt ξ ==> store ξ' = store ξ"
  unfolding is_msg_defs
  by (cases "msg ξ", clarsimp+)+

lemma is_msg_inv_sip [simp]:
  "ξ' ∈ is_pkt ξ ==> sip ξ' = sip ξ"
  "ξ' ∈ is_newpkt ξ ==> sip ξ' = sip ξ"
  unfolding is_msg_defs
  by (cases "msg ξ", clarsimp+)+

subsection "The protocol process"

datatype pseqp =
    PAodv
  | PNewPkt
  | PPkt
  | PRreq
  | PRrep
  | PRerr

fun nat_of_seqp :: "pseqp ==> nat"
where
  "nat_of_seqp PAodv = 1"
| "nat_of_seqp PPkt = 2"
| "nat_of_seqp PNewPkt = 3"
| "nat_of_seqp PRreq = 4"
| "nat_of_seqp PRrep = 5"
| "nat_of_seqp PRerr = 6"

instantiation "pseqp" :: ord
begin
definition less_eq_seqp [iff]: "l1 ≤ l2 = (nat_of_seqp l1 ≤ nat_of_seqp l2)"
definition less_seqp [iff]:    "l1 < l2 = (nat_of_seqp l1 < nat_of_seqp l2)"
instance ..
end

abbreviation AODV
where
  "AODV ≡ λ_. [clear_locals] call(PAodv)"

abbreviation PKT
where
  "PKT args ≡

     [ξ. let (data, dip, oip) = args ξ in
         (clear_locals ξ) ( data := data, dip := dip, oip := oip )]
     call(PPkt)"
abbreviation NEWPKT
where
  "NEWPKT args ≡
     [ξ. let (data, dip) = args ξ in
         (clear_locals ξ) ( data := data, dip := dip )]
     call(PNewPkt)"

abbreviation RREQ
where
  "RREQ args ≡
     [ξ. let (hops, rreqid, dip, dsn, dsk, oip, osn, sip) = args ξ in
         (clear_locals ξ) ( hops := hops, rreqid := rreqid, dip := dip,
                            dsn := dsn, dsk := dsk, oip := oip,
                            osn := osn, sip := sip )]
     call(PRreq)"

abbreviation RREP
where
  "RREP args ≡
     [ξ. let (hops, dip, dsn, oip, sip) = args ξ in
         (clear_locals ξ) ( hops := hops, dip := dip, dsn := dsn,
                            oip := oip, sip := sip )]
     call(PRrep)"

abbreviation RERR
where
  "RERR args ≡
     [ξ. let (dests, sip) = args ξ in
         (clear_locals ξ) ( dests := dests, sip := sip )]
     call(PRerr)"

fun Γ_AODV :: "(state, msg, pseqp, pseqp label) seqp_env"
where
  "Γ_AODV PAodv = labelled PAodv (
     receive(λmsg' ξ. ξ ( msg := msg' )).
     ( ⟨is_newpkt⟩ NEWPKT(λξ. (data ξ, ip ξ))
       ⊕ ⟨is_pkt⟩ PKT(λξ. (data ξ, dip ξ, oip ξ))
       ⊕ ⟨is_rreq⟩
            [ξ. ξ (rt := update (rt ξ) (sip ξ) (0, unk, val, 1, sip ξ, {}) )]
            RREQ(λξ. (hops ξ, rreqid ξ, dip ξ, dsn ξ, dsk ξ, oip ξ, osn ξ, sip ξ))
       ⊕ ⟨is_rrep⟩
            [ξ. ξ (rt := update (rt ξ) (sip ξ) (0, unk, val, 1, sip ξ, {}) )]
            RREP(λξ. (hops ξ, dip ξ, dsn ξ, oip ξ, sip ξ))
       ⊕ ⟨is_rerr⟩
            [ξ. ξ (rt := update (rt ξ) (sip ξ) (0, unk, val, 1, sip ξ, {}) )]
            RERR(λξ. (dests ξ, sip ξ))
     )
     ⊕ ⟨λξ. { ξ( dip := dip ) | dip. dip ∈ qD(store ξ) ∩ vD(rt ξ) }⟩
          [ξ. ξ ( data := hd(σ(store ξ, dip ξ)) )]
          unicast(λξ. the (nhop (rt ξ) (dip ξ)), λξ. pkt(data ξ, dip ξ, ip ξ)).
            [ξ. ξ ( store := the (drop (dip ξ) (store ξ)) )]
            AODV()
          ▹ [ξ. ξ ( dests := (λrip. if (rip ∈ vD (rt ξ) ∧ nhop (rt ξ) rip = nhop (rt ξ) (dip ξ))
                                     then Some (inc (sqn (rt ξ) rip)) else None) )]
             [ξ. ξ ( rt := invalidate (rt ξ) (dests ξ) )]
             [ξ. ξ ( store := setRRF (store ξ) (dests ξ))]
             [ξ. ξ ( pre := ∪{ the (precs (rt ξ) rip) | rip. rip ∈ dom (dests ξ) } )]
             [ξ. ξ ( dests := (λrip. if ((dests ξ) rip ≠ None ∧ the (precs (rt ξ) rip) ≠ {})
                                     then (dests ξ) rip else None) )]
             groupcast(λξ. pre ξ, λξ. rerr(dests ξ, ip ξ)). AODV()
     ⊕ ⟨λξ. { ξ( dip := dip )
             | dip. dip ∈ qD(store ξ) - vD(rt ξ) ∧ the (σ_-flag(store ξ, dip)) = req }⟩
         [ξ. ξ ( store := unsetRRF (store ξ) (dip ξ) )]
         [ξ. ξ ( sn := inc (sn ξ) )]
         [ξ. ξ ( rreqid := nrreqid (rreqs ξ) (ip ξ) )]
         [ξ. ξ ( rreqs := rreqs ξ ∪ {(ip ξ, rreqid ξ)} )]
         broadcast(λξ. rreq(0, rreqid ξ, dip ξ, sqn (rt ξ) (dip ξ), sqnf (rt ξ) (dip ξ),
                            ip ξ, sn ξ, ip ξ)). AODV())"

|  "Γ_AODV PNewPkt = labelled PNewPkt (
     ⟨ξ. dip ξ = ip ξ⟩
        deliver(λξ. data ξ).AODV()
     ⊕ ⟨ξ. dip ξ ≠ ip ξ⟩
        [ξ. ξ ( store := add (data ξ) (dip ξ) (store ξ) )]
        AODV())"

| "Γ_AODV PPkt = labelled PPkt (
     ⟨ξ. dip ξ = ip ξ⟩
        deliver(λξ. data ξ).AODV()
     ⊕ ⟨ξ. dip ξ ≠ ip ξ⟩
     (
       ⟨ξ. dip ξ ∈ vD (rt ξ)⟩
         unicast(λξ. the (nhop (rt ξ) (dip ξ)), λξ. pkt(data ξ, dip ξ, oip ξ)).AODV()
         ▹
           [ξ. ξ ( dests := (λrip. if (rip ∈ vD (rt ξ) ∧ nhop (rt ξ) rip = nhop (rt ξ) (dip ξ))
                                   then Some (inc (sqn (rt ξ) rip)) else None) )]
           [ξ. ξ ( rt := invalidate (rt ξ) (dests ξ) )]
           [ξ. ξ ( store := setRRF (store ξ) (dests ξ))]
           [ξ. ξ ( pre := ∪{ the (precs (rt ξ) rip) | rip. rip ∈ dom (dests ξ) } )]
           [ξ. ξ ( dests := (λrip. if ((dests ξ) rip ≠ None ∧ the (precs (rt ξ) rip) ≠ {})
                                   then (dests ξ) rip else None) )]
           groupcast(λξ. pre ξ, λξ. rerr(dests ξ, ip ξ)).AODV()
       ⊕ ⟨ξ. dip ξ ∉ vD (rt ξ)⟩
       (
           ⟨ξ. dip ξ ∈ iD (rt ξ)⟩
             groupcast(λξ. the (precs (rt ξ) (dip ξ)),
                       λξ. rerr([dip ξ ↦ sqn (rt ξ) (dip ξ)], ip ξ)). AODV()
           ⊕ ⟨ξ. dip ξ ∉ iD (rt ξ)⟩
              AODV()
       )
     ))"

| "Γ_AODV PRreq = labelled PRreq (
     ⟨ξ. (oip ξ, rreqid ξ) ∈ rreqs ξ⟩
       AODV()
     ⊕ ⟨ξ. (oip ξ, rreqid ξ) ∉ rreqs ξ⟩
       [ξ. ξ ( rt := update (rt ξ) (oip ξ) (osn ξ, kno, val, hops ξ + 1, sip ξ, {}) )]
       [ξ. ξ ( rreqs := rreqs ξ ∪ {(oip ξ, rreqid ξ)} )]
       (
         ⟨ξ. dip ξ = ip ξ⟩
           [ξ. ξ ( sn := max (sn ξ) (dsn ξ) )]
           unicast(λξ. the (nhop (rt ξ) (oip ξ)), λξ. rrep(0, dip ξ, sn ξ, oip ξ, ip ξ)).AODV()
           ▹
             [ξ. ξ ( dests := (λrip. if (rip ∈ vD (rt ξ) ∧ nhop (rt ξ) rip = nhop (rt ξ) (oip ξ))
                                     then Some (inc (sqn (rt ξ) rip)) else None) )]
             [ξ. ξ ( rt := invalidate (rt ξ) (dests ξ) )]
             [ξ. ξ ( store := setRRF (store ξ) (dests ξ))]
             [ξ. ξ ( pre := ∪{ the (precs (rt ξ) rip) | rip. rip ∈ dom (dests ξ) } )]
             [ξ. ξ ( dests := (λrip. if ((dests ξ) rip ≠ None ∧ the (precs (rt ξ) rip) ≠ {})
                                     then (dests ξ) rip else None) )]
             groupcast(λξ. pre ξ, λξ. rerr(dests ξ, ip ξ)).AODV()
         ⊕ ⟨ξ. dip ξ ≠ ip ξ⟩
         (
           ⟨ξ. dip ξ ∈ vD (rt ξ) ∧ dsn ξ ≤ sqn (rt ξ) (dip ξ) ∧ sqnf (rt ξ) (dip ξ) = kno⟩
             [ξ. ξ ( rt := the (addpreRT (rt ξ) (dip ξ) {sip ξ}) )]
             [ξ. ξ ( rt := the (addpreRT (rt ξ) (oip ξ) {the (nhop (rt ξ) (dip ξ))}) )]
             unicast(λξ. the (nhop (rt ξ) (oip ξ)), λξ. rrep(the (dhops (rt ξ) (dip ξ)), dip ξ,
                         sqn (rt ξ) (dip ξ), oip ξ, ip ξ)).
             AODV()
           ▹
             [ξ. ξ ( dests := (λrip. if (rip ∈ vD (rt ξ) ∧ nhop (rt ξ) rip = nhop (rt ξ) (oip ξ))
                                     then Some (inc (sqn (rt ξ) rip)) else None) )]
             [ξ. ξ ( rt := invalidate (rt ξ) (dests ξ) )]
             [ξ. ξ ( store := setRRF (store ξ) (dests ξ))]
             [ξ. ξ ( pre := ∪{ the (precs (rt ξ) rip) | rip. rip ∈ dom (dests ξ) } )]
             [ξ. ξ ( dests := (λrip. if ((dests ξ) rip ≠ None ∧ the (precs (rt ξ) rip) ≠ {})
                                     then (dests ξ) rip else None) )]
             groupcast(λξ. pre ξ, λξ. rerr(dests ξ, ip ξ)).AODV()
           ⊕ ⟨ξ. dip ξ ∉ vD (rt ξ) ∨ sqn (rt ξ) (dip ξ) < dsn ξ ∨ sqnf (rt ξ) (dip ξ) = unk⟩
             broadcast(λξ. rreq(hops ξ + 1, rreqid ξ, dip ξ, max (sqn (rt ξ) (dip ξ)) (dsn ξ),
                                dsk ξ, oip ξ, osn ξ, ip ξ)).
             AODV()
         )
       ))"

| "Γ_AODV PRrep = labelled PRrep (
     ⟨ξ. rt ξ ≠ update (rt ξ) (dip ξ) (dsn ξ, kno, val, hops ξ + 1, sip ξ, {}) ⟩
     (
       [ξ. ξ ( rt := update (rt ξ) (dip ξ) (dsn ξ, kno, val, hops ξ + 1, sip ξ, {}) ) ]
       (
         ⟨ξ. oip ξ = ip ξ ⟩
            AODV()
         ⊕ ⟨ξ. oip ξ ≠ ip ξ ⟩
         (
           ⟨ξ. oip ξ ∈ vD (rt ξ)⟩
             [ξ. ξ ( rt := the (addpreRT (rt ξ) (dip ξ) {the (nhop (rt ξ) (oip ξ))}) )]
             [ξ. ξ ( rt := the (addpreRT (rt ξ) (the (nhop (rt ξ) (dip ξ)))
                                               {the (nhop (rt ξ) (oip ξ))}) )]
             unicast(λξ. the (nhop (rt ξ) (oip ξ)), λξ. rrep(hops ξ + 1, dip ξ, dsn ξ, oip ξ, ip ξ)).
             AODV()
           ▹
             [ξ. ξ ( dests := (λrip. if (rip ∈ vD (rt ξ) ∧ nhop (rt ξ) rip = nhop (rt ξ) (oip ξ))
                                     then Some (inc (sqn (rt ξ) rip)) else None) )]
             [ξ. ξ ( rt := invalidate (rt ξ) (dests ξ) )]
             [ξ. ξ ( store := setRRF (store ξ) (dests ξ))]
             [ξ. ξ ( pre := ∪{ the (precs (rt ξ) rip) | rip. rip ∈ dom (dests ξ) } )]
             [ξ. ξ ( dests := (λrip. if ((dests ξ) rip ≠ None ∧ the (precs (rt ξ) rip) ≠ {})
                                     then (dests ξ) rip else None) )]
             groupcast(λξ. pre ξ, λξ. rerr(dests ξ, ip ξ)).AODV()
           ⊕ ⟨ξ. oip ξ ∉ vD (rt ξ)⟩
             AODV()
         )
       )
     )
     ⊕ ⟨ξ. rt ξ = update (rt ξ) (dip ξ) (dsn ξ, kno, val, hops ξ + 1, sip ξ, {}) ⟩
         AODV()
     )"

| "Γ_AODV PRerr = labelled PRerr (
     [ξ. ξ ( dests := (λrip. case (dests ξ) rip of None ==> None
                       | Some rsn ==> if rip ∈ vD (rt ξ) ∧ the (nhop (rt ξ) rip) = sip ξ
                                       ∧ sqn (rt ξ) rip < rsn then Some rsn else None) )]
     [ξ. ξ ( rt := invalidate (rt ξ) (dests ξ) )]
     [ξ. ξ ( store := setRRF (store ξ) (dests ξ))]
     [ξ. ξ ( pre := ∪{ the (precs (rt ξ) rip) | rip. rip ∈ dom (dests ξ) } )]
     [ξ. ξ ( dests := (λrip. if ((dests ξ) rip ≠ None ∧ the (precs (rt ξ) rip) ≠ {})
                             then (dests ξ) rip else None) )]
     groupcast(λξ. pre ξ, λξ. rerr(dests ξ, ip ξ)). AODV())"

declare Γ_AODV.simps [simp del]

lemmas Γ_{AODV_simps} [simp, code] = Γ_AODV.simps [simplified]

fun Γ_{AODV_skeleton}
where
    "Γ_{AODV_skeleton} PAodv = seqp_skeleton (Γ_AODV PAodv)"
  | "Γ_{AODV_skeleton} PNewPkt = seqp_skeleton (Γ_AODV PNewPkt)"
  | "Γ_{AODV_skeleton} PPkt = seqp_skeleton (Γ_AODV PPkt)"
  | "Γ_{AODV_skeleton} PRreq = seqp_skeleton (Γ_AODV PRreq)"
  | "Γ_{AODV_skeleton} PRrep = seqp_skeleton (Γ_AODV PRrep)"
  | "Γ_{AODV_skeleton} PRerr = seqp_skeleton (Γ_AODV PRerr)"

lemma Γ_{AODV_skeleton_wf} [simp]:
  "wellformed Γ_{AODV_skeleton}"
  proof (rule, intro allI)
    fix pn pn'
    show "call(pn') ∉ stermsl (Γ_{AODV_skeleton} pn)"
      by (cases pn) simp_all
  qed

declare Γ_{AODV_skeleton}.simps [simp del]

lemmas Γ_{AODV_skeleton_simps} [simp, code] = Γ_{AODV_skeleton}.simps [simplified Γ_{AODV_simps} seqp_skeleton.simps]

lemma aodv_proc_cases [dest]:
  fixes p pn
  shows "p ∈ ctermsl (Γ_AODV pn) ==>
                                (p ∈ ctermsl (Γ_AODV PAodv) ∨
                                 p ∈ ctermsl (Γ_AODV PNewPkt) ∨
                                 p ∈ ctermsl (Γ_AODV PPkt) ∨
                                 p ∈ ctermsl (Γ_AODV PRreq) ∨
                                 p ∈ ctermsl (Γ_AODV PRrep) ∨
                                 p ∈ ctermsl (Γ_AODV PRerr))"
  by (cases pn) simp_all

definition σ_AODV :: "ip ==> (state × (state, msg, pseqp, pseqp label) seqp) set"
where "σ_AODV i ≡ {(aodv_init i, Γ_AODV PAodv)}"

abbreviation paodv
  :: "ip ==> (state × (state, msg, pseqp, pseqp label) seqp, msg seq_action) automaton"
where
  "paodv i ≡ ( init = σ_AODV i, trans = seqp_sos Γ_AODV )"

lemma aodv_trans: "trans (paodv i) = seqp_sos Γ_AODV"
  by simp

lemma aodv_control_within [simp]: "control_within Γ_AODV (init (paodv i))"
  unfolding σ_{AODV_def} by (rule control_withinI) (auto simp del: Γ_{AODV_simps})

lemma aodv_wf [simp]:
  "wellformed Γ_AODV"
  proof (rule, intro allI)
    fix pn pn'
    show "call(pn') ∉ stermsl (Γ_AODV pn)"
      by (cases pn) simp_all
  qed

lemmas aodv_labels_not_empty [simp] = labels_not_empty [OF aodv_wf]

lemma aodv_ex_label [intro]: "∃l. l∈labels Γ_AODV p"
  by (metis aodv_labels_not_empty all_not_in_conv)

lemma aodv_ex_labelE [elim]:
  assumes "∀l∈labels Γ_AODV p. P l p"
      and "∃p l. P l p ==> Q"
    shows "Q"
  using assms by (metis aodv_ex_label)

lemma aodv_simple_labels [simp]: "simple_labels Γ_AODV"
  proof
    fix pn p
    assume "p∈subterms(Γ_AODV pn)"
    thus "∃!l. labels Γ_AODV p = {l}"
    by (cases pn) (simp_all cong: seqp_congs | elim disjE)+
  qed

lemma σ_{AODV_labels} [simp]: "(ξ, p) ∈ σ_AODV i ==> labels Γ_AODV p = {PAodv-:0}"
  unfolding σ_{AODV_def} by simp

lemma aodv_init_kD_empty [simp]:
  "(ξ, p) ∈ σ_AODV i ==> kD (rt ξ) = {}"
  unfolding σ_{AODV_def} kD_def by simp

lemma aodv_init_sip_not_ip [simp]: "¬(sip (aodv_init i) = i)" by simp

lemma aodv_init_sip_not_ip' [simp]:
  assumes "(ξ, p) ∈ σ_AODV i"
    shows "sip ξ ≠ ip ξ"
  using assms unfolding σ_{AODV_def} by simp

lemma aodv_init_sip_not_i [simp]:
  assumes "(ξ, p) ∈ σ_AODV i"
    shows "sip ξ ≠ i"
  using assms unfolding σ_{AODV_def} by simp

lemma clear_locals_sip_not_ip':
  assumes "ip ξ = i"
    shows "¬(sip (clear_locals ξ) = i)"
  using assms by auto

text ‹Stop the simplifier from descending into process terms.›
declare seqp_congs [cong]

text ‹Configure the main invariant tactic for AODV.›

declare
  Γ_{AODV_simps} [cterms_env]
  aodv_proc_cases [ctermsl_cases]
  seq_invariant_ctermsI [OF aodv_wf aodv_control_within aodv_simple_labels aodv_trans,
                            cterms_intros]
  seq_step_invariant_ctermsI [OF aodv_wf aodv_control_within aodv_simple_labels aodv_trans,
                                 cterms_intros]

end