Theory State

(*  Title:      JinjaDCI/J/State.thy

    Author:     Tobias Nipkow, Susannah Mansky
    Copyright   2003 Technische Universitaet Muenchen, 2019-20 UIUC

    Based on the Jinja theory J/State.thy by Tobias Nipkow
*)

section ‹ Program State ›

theory State imports "../Common/Exceptions" begin

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

definition hp :: "state ⇒ heap"
where
  "hp  ≡  fst"
definition lcl :: "state ⇒ locals"
where
  "lcl  ≡  fst ∘ snd"
definition shp :: "state ⇒ sheap"
where
  "shp  ≡  snd ∘ snd"

(*<*)
declare hp_def[simp] lcl_def[simp] shp_def[simp]
(*>*)

end