Theory D_Aodv_Predicates
section "Invariant assumptions and properties"
theory D_Aodv_Predicates
imports D_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 rreqid dip dsn dsk oip osn sip handled.
msg_sender (Rreq hops rreqid 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 rreqid dip dsn dsk oip osn sip handled.
msg_zhops (Rreq hops rreqid 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 rreqid dip dsn dsk oip osn sip handled.
rreq_rrep_sn (Rreq hops rreqid 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 ⟶
oipc∈kD(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 ⟶
dipc∈kD(crt)
∧ sqn crt dipc = dsnc
∧ the (dhops crt dipc) = hopsc
∧ the (flag crt dipc) = val)
| _ ⇒ True"
lemma rreq_rrep_fresh [simp]:
"⋀hops rreqid dip dsn dsk oip osn sip handled.
rreq_rrep_fresh crt (Rreq hops rreqid dip dsn dsk oip osn sip handled) =
(sip ≠ oip ⟶ oip∈kD(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 ⟶ dip∈kD(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 _ ⇒ (∀ripc∈dom(destsc).
(ripc∈iD(crt) ∧ the (destsc ripc) = sqn crt ripc))
| _ ⇒ True"
lemma rerr_invalid [simp]:
"⋀hops rreqid dip dsn dsk oip osn sip handled.
rerr_invalid crt (Rreq hops rreqid 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) = (∀rip∈dom(dests).
rip∈iD(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