Theory State_Concretization

theory State_Concretization
  imports "Voblint_VIMP.VIMP_Syntax" Abstract_Domain
begin

section ‹The stores an abstract state describes›

text ‹
  Every kind of abstract state, pointwise or relational, denotes a set of
  stores. ‹γ d› is that set for every state type: each state theory
  registers its own concretization under this one constant with
  ‹adhoc_overloading›, and the type of ‹d› selects it.
›

text ‹The class parameter \<^const>‹gamma› gives up its own notation here, so that ‹γ›
  has exactly one production in every theory that sees this one.›

no_notation gamma ("γ")

consts gamma_S :: "'s ⇒ 'v set" ("γ")

adhoc_overloading gamma_S == gamma

text ‹
  An executable state is read back as the abstract state it represents, given the
  classifier that tells locals from globals. ‹readback 𝒢 x› is that reading for
  every executable representation, registered the same way, so a concretization of an
  executable state is ‹γ (readback 𝒢 x)› whatever its representation. Its notation
  ‹ρ⇘𝒢⇙ x› is opt-in, in the bundle ‹default_st_syntax›.
›

consts readback :: "(vname ⇒ bool) ⇒ 'e ⇒ 'a"

end