Theory State

(*  Title:       CoreC++
    Author:      Tobias Nipkow
    Maintainer:  Daniel Wasserrab <wasserra at fmi.uni-passau.de>
*)

section ‹Program State›

theory State imports Exceptions begin

type_synonym
  locals = "vname ⇀ val"      ― ‹local vars, incl. params and ``this''›
type_synonym
  state  = "heap × locals"

definition hp :: "state ⇒ heap" where
  "hp  ≡  fst"

definition lcl :: "state ⇒ locals" where
  "lcl  ≡  snd"

declare hp_def[simp] lcl_def[simp]

end