Theory E_Aodv_Predicates

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

section "Invariant assumptions and properties"

theory E_Aodv_Predicates
imports E_Aodv
begin

text ‹Definitions for expression assumptions on incoming messages and properties of
      outgoing messages.›

abbreviation not_Pkt :: "msg  bool"
where "not_Pkt m  case m of Pkt _ _ _  False | _  True"

definition msg_sender :: "msg  ip"
where "msg_sender m  case m of Rreq _ _ _ _ _ _ ipc _  ipc
                              | Rrep _ _ _ _ ipc  ipc
                              | Rerr _ ipc  ipc
                              | Pkt _ _ ipc  ipc"

lemma msg_sender_simps [simp]:
  "hops dip dsn dsk oip osn sip handled.
                          msg_sender (Rreq hops dip dsn dsk oip osn sip handled) = sip"
  "hops dip dsn oip sip. msg_sender (Rrep hops dip dsn oip sip) = sip"
  "dests sip.            msg_sender (Rerr dests sip) = sip"
  "d dip sip.            msg_sender (Pkt d dip sip) = sip"
  unfolding msg_sender_def by simp_all

definition msg_zhops :: "msg  bool"
where "msg_zhops m  case m of
                                 Rreq hopsc dipc _ _ oipc _ sipc _  hopsc = 0  oipc = sipc
                               | Rrep hopsc dipc _ _ sipc  hopsc = 0  dipc = sipc
                               | _  True"

lemma msg_zhops_simps [simp]:
  "hops dip dsn dsk oip osn sip handled.
           msg_zhops (Rreq hops dip dsn dsk oip osn sip handled) = (hops = 0  oip = sip)"
  "hops dip dsn oip sip. msg_zhops (Rrep hops dip dsn oip sip) = (hops = 0  dip = sip)"
  "dests sip.            msg_zhops (Rerr dests sip)        = True"
  "d dip.                msg_zhops (Newpkt d dip)          = True"
  "d dip sip.            msg_zhops (Pkt d dip sip)         = True"
  unfolding msg_zhops_def by simp_all

definition rreq_rrep_sn :: "msg  bool"
where "rreq_rrep_sn m  case m of Rreq _ _ _ _ _ osnc _ _  osnc  1
                                | Rrep _ _ dsnc _ _  dsnc  1
                                | _  True"

lemma rreq_rrep_sn_simps [simp]:
  "hops dip dsn dsk oip osn sip handled.
           rreq_rrep_sn (Rreq hops dip dsn dsk oip osn sip handled) = (osn  1)"
  "hops dip dsn oip sip. rreq_rrep_sn (Rrep hops dip dsn oip sip) = (dsn  1)"
  "dests sip.            rreq_rrep_sn (Rerr dests sip) = True"
  "d dip.                rreq_rrep_sn (Newpkt d dip)   = True"
  "d dip sip.            rreq_rrep_sn (Pkt d dip sip)  = True"
  unfolding rreq_rrep_sn_def by simp_all

definition rreq_rrep_fresh :: "rt  msg  bool"
where "rreq_rrep_fresh crt m  case m of Rreq hopsc _ _ _ oipc osnc ipcc _  (ipcc  oipc 
                                                oipckD(crt)  (sqn crt oipc > osnc
                                                                 (sqn crt oipc = osnc
                                                                    the (dhops crt oipc)  hopsc
                                                                    the (flag crt oipc) = val)))
                                | Rrep hopsc dipc dsnc _ ipcc  (ipcc  dipc  
                                                                    dipckD(crt)
                                                                   sqn crt dipc = dsnc
                                                                   the (dhops crt dipc) = hopsc
                                                                   the (flag crt dipc) = val)
                                | _  True"

lemma rreq_rrep_fresh [simp]:
  "hops dip dsn dsk oip osn sip handled.
           rreq_rrep_fresh crt (Rreq hops dip dsn dsk oip osn sip handled) =
                               (sip  oip  oipkD(crt)
                                             (sqn crt oip > osn
                                                (sqn crt oip = osn
                                                   the (dhops crt oip)  hops
                                                   the (flag crt oip) = val)))"
  "hops dip dsn oip sip. rreq_rrep_fresh crt (Rrep hops dip dsn oip sip) =
                               (sip  dip  dipkD(crt)
                                               sqn crt dip = dsn
                                               the (dhops crt dip) = hops
                                               the (flag crt dip) = val)"
  "dests sip.            rreq_rrep_fresh crt (Rerr dests sip) = True"
  "d dip.                rreq_rrep_fresh crt (Newpkt d dip)   = True"
  "d dip sip.            rreq_rrep_fresh crt (Pkt d dip sip)  = True"
  unfolding rreq_rrep_fresh_def by simp_all

definition rerr_invalid :: "rt  msg  bool"
where "rerr_invalid crt m  case m of Rerr destsc _  (ripcdom(destsc).
                                            (ripciD(crt)  the (destsc ripc) = sqn crt ripc))
                                | _  True"

lemma rerr_invalid [simp]:
  "hops dip dsn dsk oip osn sip handled.
                           rerr_invalid crt (Rreq hops dip dsn dsk oip osn sip handled) = True"
  "hops dip dsn oip sip. rerr_invalid crt (Rrep hops dip dsn oip sip) = True"
  "dests sip.            rerr_invalid crt (Rerr dests sip) = (ripdom(dests).
                                                 ripiD(crt)  the (dests rip) = sqn crt rip)"
  "d dip.                rerr_invalid crt (Newpkt d dip)   = True"
  "d dip sip.            rerr_invalid crt (Pkt d dip sip)  = True"
  unfolding rerr_invalid_def by simp_all

definition
  initmissing :: "(nat  state option) × 'a  (nat  state) × 'a"
where
  "initmissing σ = (λi. case (fst σ) i of None  aodv_init i | Some s  s, snd σ)"

lemma not_in_net_ips_fst_init_missing [simp]:
  assumes "i  net_ips σ"
    shows "fst (initmissing (netgmap fst σ)) i = aodv_init i"
  using assms unfolding initmissing_def by simp

lemma fst_initmissing_netgmap_pair_fst [simp]:
  "fst (initmissing (netgmap (λ(p, q). (fst (id p), snd (id p), q)) s))
                                               = fst (initmissing (netgmap fst s))"
  unfolding initmissing_def by auto

text ‹We introduce a streamlined alternative to @{term initmissing} with @{term netgmap}
        to simplify invariant statements and thus facilitate their comprehension and
        presentation.›

lemma fst_initmissing_netgmap_default_aodv_init_netlift:
  "fst (initmissing (netgmap fst s)) = default aodv_init (netlift fst s)"
  unfolding initmissing_def default_def
  by (simp add: fst_netgmap_netlift del: One_nat_def)

definition
  netglobal :: "((nat  state)  bool)  ((state × 'b) × 'c) net_state  bool"
where
  "netglobal P  (λs. P (default aodv_init (netlift fst s)))"

end