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