Theory Aodv_Basic

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

section "Basic data types and constants"

theory Aodv_Basic
imports Main AWN.AWN_SOS
begin

text ‹These definitions are shared with all variants.›

type_synonym rreqid = nat
type_synonym sqn = nat

datatype k = Known | Unknown
abbreviation kno where "kno  Known"
abbreviation unk where "unk  Unknown"

datatype p = NoRequestRequired | RequestRequired
abbreviation noreq where "noreq  NoRequestRequired"
abbreviation req where "req  RequestRequired"

datatype f = Valid | Invalid
abbreviation val where "val  Valid"
abbreviation inv where "inv  Invalid"

lemma not_ks [simp]:                                      
   "(x  kno) = (x = unk)"
   "(x  unk) = (x = kno)"
  by (cases x, clarsimp+)+

lemma not_ps [simp]:
  "(x  noreq) = (x = req)"
  "(x  req) = (x = noreq)"
  by (cases x, clarsimp+)+

lemma not_ffs [simp]:
  "(x  val) = (x = inv)"
  "(x  inv) = (x = val)"
  by (cases x, clarsimp+)+

end