Theory A_OAodv

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

section "The `open' AODV model"

theory A_OAodv
imports A_Aodv AWN.OAWN_SOS_Labels AWN.OAWN_Convert
begin

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

definition σAODV' :: "((ip  state) × ((state, msg, pseqp, pseqp label) seqp)) set"
where "σAODV'  {(λi. aodv_init i, ΓAODV PAodv)}"

abbreviation opaodv
  :: "ip  ((ip  state) × (state, msg, pseqp, pseqp label) seqp, msg seq_action) automaton"
where
  "opaodv i   init = σAODV', trans = oseqp_sos ΓAODV i "

lemma initiali_aodv [intro!, simp]: "initiali i (init (opaodv i)) (init (paodv i))"
  unfolding σAODV_def σAODV'_def by rule simp_all

lemma oaodv_control_within [simp]: "control_within ΓAODV (init (opaodv i))"
  unfolding σAODV'_def by (rule control_withinI) (auto simp del: ΓAODV_simps)

lemma σAODV'_labels [simp]: "(σ, p)  σAODV'   labels ΓAODV p = {PAodv-:0}"
  unfolding σAODV'_def by simp

lemma oaodv_init_kD_empty [simp]:
  "(σ, p)  σAODV'  kD (rt (σ i)) = {}"
  unfolding σAODV'_def kD_def by simp

lemma oaodv_init_vD_empty [simp]:
  "(σ, p)  σAODV'  vD (rt (σ i)) = {}"
  unfolding σAODV'_def vD_def by simp

lemma oaodv_trans: "trans (opaodv i) = oseqp_sos ΓAODV 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