Theory ProcState

section ‹The state›

theory ProcState imports Com begin

fun "interpret" :: "expr ⇒ (vname ⇀ 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 ⇀ val) ⇒ vname ⇒ expr ⇒ (vname ⇀ val)"
  where "update cf V e ≡ cf(V:=(interpret e cf))"

abbreviation state_check :: "(vname ⇀ val) ⇒ expr ⇒ val option ⇒ bool"
where "state_check cf b v ≡ (interpret b cf = v)"

end