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