Theory StateSpace

(*
    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 ⇒ '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