1(*  Title:      HOL/Statespace/StateSpaceLocale.thy
2    Author:     Norbert Schirmer, TU Muenchen
3*)
4
5section \<open>Setup for State Space Locales \label{sec:StateSpaceLocale}\<close>
6
7theory StateSpaceLocale imports StateFun 
8keywords "statespace" :: thy_decl
9begin
10
11ML_file "state_space.ML"
12ML_file "state_fun.ML"
13
14text \<open>For every type that is to be stored in a state space, an
15instance of this locale is imported in order convert the abstract and
16concrete values.\<close>
17
18
19locale project_inject =
20 fixes project :: "'value \<Rightarrow> 'a"
21  and inject :: "'a \<Rightarrow> 'value"
22 assumes project_inject_cancel [statefun_simp]: "project (inject x) = x"
23begin
24
25lemma ex_project [statefun_simp]: "\<exists>v. project v = x"
26proof
27  show "project (inject x) = x"
28    by (rule project_inject_cancel)
29qed
30
31lemma project_inject_comp_id [statefun_simp]: "project \<circ> inject = id"
32  by (rule ext) (simp add: project_inject_cancel)
33
34lemma project_inject_comp_cancel[statefun_simp]: "f \<circ> project \<circ> inject = f"
35  by (rule ext) (simp add: project_inject_cancel)
36
37end
38
39end
40