Quelle  OAodv.thy

(*  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 σ_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