Theory State

(*  Title:      JinjaThreads/J/State.thy
    Author:     Tobias Nipkow, Andreas Lochbihler
*)

chapter ‹JinjaThreads source language›

section ‹Program State›

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


type_synonym
  'addr locals = "vname ⇀ 'addr val"      ― ‹local vars, incl. params and ``this''›
type_synonym
  ('addr, 'heap) Jstate = "'heap × 'addr locals"     ― ‹the heap and the local vars›

definition hp :: "'heap × 'x ⇒ 'heap" where "hp ≡ fst"

definition lcl :: "'heap × 'x ⇒ 'x" where "lcl ≡ snd"

lemma hp_conv [simp]: "hp (h, l) = h"
by(simp add: hp_def)

lemma lcl_conv [simp]: "lcl (h, l) = l"
by(simp add: lcl_def)

end