Theory OAodv

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

section "The `open' AODV model"

theory OAodv
imports Aodv AWN.OAWN_SOS_Labels AWN.OAWN_Convert
begin

text ‹Definitions for stating and proving global network properties over individual processes.›

definition σ⇩A⇩O⇩D⇩V' :: "((ip ⇒ state) × ((state, msg, pseqp, pseqp label) seqp)) set"
where "σ⇩A⇩O⇩D⇩V' ≡ {(λi. aodv_init i, Γ⇩A⇩O⇩D⇩V PAodv)}"

abbreviation opaodv
  :: "ip ⇒ ((ip ⇒ state) × (state, msg, pseqp, pseqp label) seqp, msg seq_action) automaton"
where
  "opaodv i ≡ ⦇ init = σ⇩A⇩O⇩D⇩V', trans = oseqp_sos Γ⇩A⇩O⇩D⇩V i ⦈"

lemma initiali_aodv [intro!, simp]: "initiali i (init (opaodv i)) (init (paodv i))"
  unfolding σ⇩A⇩O⇩D⇩V_def σ⇩A⇩O⇩D⇩V'_def by rule simp_all

lemma oaodv_control_within [simp]: "control_within Γ⇩A⇩O⇩D⇩V (init (opaodv i))"
  unfolding σ⇩A⇩O⇩D⇩V'_def by (rule control_withinI) (auto simp del: Γ⇩A⇩O⇩D⇩V_simps)

lemma σ⇩A⇩O⇩D⇩V'_labels [simp]: "(σ, p) ∈ σ⇩A⇩O⇩D⇩V' ⟹  labels Γ⇩A⇩O⇩D⇩V p = {PAodv-:0}"
  unfolding σ⇩A⇩O⇩D⇩V'_def by simp

lemma oaodv_init_kD_empty [simp]:
  "(σ, p) ∈ σ⇩A⇩O⇩D⇩V' ⟹ kD (rt (σ i)) = {}"
  unfolding σ⇩A⇩O⇩D⇩V'_def kD_def by simp

lemma oaodv_init_vD_empty [simp]:
  "(σ, p) ∈ σ⇩A⇩O⇩D⇩V' ⟹ vD (rt (σ i)) = {}"
  unfolding σ⇩A⇩O⇩D⇩V'_def vD_def by simp

lemma oaodv_trans: "trans (opaodv i) = oseqp_sos Γ⇩A⇩O⇩D⇩V i"
  by simp

declare
  oseq_invariant_ctermsI [OF aodv_wf oaodv_control_within aodv_simple_labels oaodv_trans, cterms_intros]
  oseq_step_invariant_ctermsI [OF aodv_wf oaodv_control_within aodv_simple_labels oaodv_trans, cterms_intros]

end