author | wenzelm |
Sun, 06 Nov 2011 16:29:22 +0100 | |
changeset 45358 | 4849133d7a78 |
parent 41959 | b460124855b8 |
child 46950 | d0181abdbdac |
permissions | -rw-r--r-- |
41959 | 1 |
(* Title: HOL/Statespace/StateSpaceLocale.thy |
25171 | 2 |
Author: Norbert Schirmer, TU Muenchen |
3 |
*) |
|
4 |
||
5 |
header {* Setup for State Space Locales \label{sec:StateSpaceLocale}*} |
|
6 |
||
7 |
theory StateSpaceLocale imports StateFun |
|
25174 | 8 |
uses "state_space.ML" "state_fun.ML" |
25171 | 9 |
begin |
10 |
||
11 |
setup StateFun.setup |
|
12 |
||
13 |
text {* For every type that is to be stored in a state space, an |
|
14 |
instance of this locale is imported in order convert the abstract and |
|
15 |
concrete values.*} |
|
16 |
||
17 |
||
29247
95d3a82857e5
adapted statespace module to new locales;
Norbert Schirmer <norbert.schirmer@web.de>
parents:
29235
diff
changeset
|
18 |
locale project_inject = |
25171 | 19 |
fixes project :: "'value \<Rightarrow> 'a" |
38838 | 20 |
and inject :: "'a \<Rightarrow> 'value" |
25171 | 21 |
assumes project_inject_cancel [statefun_simp]: "project (inject x) = x" |
45358 | 22 |
begin |
25171 | 23 |
|
45358 | 24 |
lemma ex_project [statefun_simp]: "\<exists>v. project v = x" |
25 |
proof |
|
26 |
show "project (inject x) = x" |
|
27 |
by (rule project_inject_cancel) |
|
28 |
qed |
|
25171 | 29 |
|
45358 | 30 |
lemma project_inject_comp_id [statefun_simp]: "project \<circ> inject = id" |
25171 | 31 |
by (rule ext) (simp add: project_inject_cancel) |
32 |
||
45358 | 33 |
lemma project_inject_comp_cancel[statefun_simp]: "f \<circ> project \<circ> inject = f" |
25171 | 34 |
by (rule ext) (simp add: project_inject_cancel) |
35 |
||
45358 | 36 |
end |
25171 | 37 |
|
38 |
end |