section ‹Setup for State Space Locales \label{sec:StateSpaceLocale}›
theory StateSpaceLocale imports StateFun
keywords "statespace" :: thy_defn
begin
ML_file ‹state_space.ML›
ML_file ‹state_fun.ML›
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 ∘ inject = id"
by (rule ext) (simp add: project_inject_cancel)
lemma project_inject_comp_cancel[statefun_simp]: "f ∘ project ∘ inject = f"
by (rule ext) (simp add: project_inject_cancel)
end
end