Theory ProcState

header {* \isaheader{The state} *}

theory ProcState imports Com begin

fun "interpret" :: "expr => (vname \<rightharpoonup> val) => val option"
where Val: "interpret (Val v) cf = Some v"
  | Var: "interpret (Var V) cf = cf V"
  | BinOp: "interpret (e⇣1«bop»e⇣2) cf = 
    (case interpret e⇣1 cf of None => None
                         | Some v⇣1 => (case interpret e⇣2 cf of None => None
                                                           | Some v⇣2 => (
      case binop bop v⇣1 v⇣2 of None => None | Some v => Some v)))"


abbreviation update :: "(vname \<rightharpoonup> val) => vname => expr => (vname \<rightharpoonup> val)"
  where "update cf V e ≡ cf(V:=(interpret e cf))"

abbreviation state_check :: "(vname \<rightharpoonup> val) => expr => val option => bool"
where "state_check cf b v ≡ (interpret b cf = v)"

end