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 (e1«bop»e2) cf = 
    (case interpret e1 cf of None  None
                         | Some v1  (case interpret e2 cf of None  None
                                                           | Some v2  (
      case binop bop v1 v2 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)"