header {* Setup for State Space Locales \label{sec:StateSpaceLocale}*}

theory StateSpaceLocale imports StateFun

keywords "statespace" :: thy_decl

begin

ML_file "state_space.ML"

ML_file "state_fun.ML"

setup StateFun.setup

text {* For every type that is to be stored in a state space, an

instance of this locale is imported in order convert the abstract and

concrete values.*}

locale project_inject =

fixes project :: "'value => 'a"

and inject :: "'a => 'value"

assumes project_inject_cancel [statefun_simp]: "project (inject x) = x"

begin

lemma ex_project [statefun_simp]: "∃v. project v = x"

proof

show "project (inject x) = x"

by (rule project_inject_cancel)

qed

lemma project_inject_comp_id [statefun_simp]: "project o inject = id"

by (rule ext) (simp add: project_inject_cancel)

lemma project_inject_comp_cancel[statefun_simp]: "f o project o inject = f"

by (rule ext) (simp add: project_inject_cancel)

end

end