Theory State

(*  Title:      Jinja/J/State.thy

    Author:     Tobias Nipkow
    Copyright   2003 Technische Universitaet Muenchen
*)

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"

definition hp :: "state  heap"
where
  "hp    fst"
definition lcl :: "state  locals"
where
  "lcl    snd"

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