(*
    Author:      Norbert Schirmer
    Maintainer:  Norbert Schirmer, norbert.schirmer at web de

Copyright (C) 2004-2008 Norbert Schirmer
Copyright (c) 2022 Apple Inc. All rights reserved.

*)

section ‹State Space Template›
theory StateSpace imports Hoare
begin

record 'g state = "globals"::'g

definition
  upd_globals:: "('g → 'g) → ('g,'z) state_scheme → ('g,'z) state_scheme"
where
  "upd_globals upd s = s(globals := upd (globals s))"

named_theorems state_simp

lemma upd_globals_conv [state_simp]: "upd_globals f = (λs. s(globals := f (globals s)))"
  by (rule ext) (simp add: upd_globals_def)

record ('g, 'l) state_locals = "'g state" +
  locals :: 'l

(*
record ('g, 'n, 'val) stateSP = "'g state" +
  locals :: "'n \<Rightarrow> 'val"
*)

type_synonym ('g, 'n, 'val) stateSP = "('g, 'n → 'val) state_locals"
type_synonym ('g, 'n, 'val, 'x) stateSP_scheme = "('g, 'n → 'val, 'x) state_locals_scheme"


end