# Theory Aodv_Basic

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