header {*
\chapter{JinjaThreads source language}
\isaheader{Program State}
*}
theory State imports "../Common/Objects" begin
types
locals = "vname \<rightharpoonup> val" -- "local vars, incl. params and ``this''"
Jstate = "heap × 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