| author | wenzelm |
| Tue, 19 Jul 2016 09:55:03 +0200 | |
| changeset 63520 | 2803d2b8f85d |
| parent 63167 | 0909deb8059b |
| child 69605 | a96320074298 |
| permissions | -rw-r--r-- |
| 41959 | 1 |
(* Title: HOL/Statespace/StateSpaceLocale.thy |
| 25171 | 2 |
Author: Norbert Schirmer, TU Muenchen |
3 |
*) |
|
4 |
||
| 63167 | 5 |
section \<open>Setup for State Space Locales \label{sec:StateSpaceLocale}\<close>
|
| 25171 | 6 |
|
7 |
theory StateSpaceLocale imports StateFun |
|
|
46950
d0181abdbdac
declare command keywords via theory header, including strict checking outside Pure;
wenzelm
parents:
45358
diff
changeset
|
8 |
keywords "statespace" :: thy_decl |
| 25171 | 9 |
begin |
10 |
||
| 48891 | 11 |
ML_file "state_space.ML" |
12 |
ML_file "state_fun.ML" |
|
| 25171 | 13 |
|
| 63167 | 14 |
text \<open>For every type that is to be stored in a state space, an |
| 25171 | 15 |
instance of this locale is imported in order convert the abstract and |
| 63167 | 16 |
concrete values.\<close> |
| 25171 | 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" |
| 38838 | 21 |
and inject :: "'a \<Rightarrow> 'value" |
| 25171 | 22 |
assumes project_inject_cancel [statefun_simp]: "project (inject x) = x" |
| 45358 | 23 |
begin |
| 25171 | 24 |
|
| 45358 | 25 |
lemma ex_project [statefun_simp]: "\<exists>v. project v = x" |
26 |
proof |
|
27 |
show "project (inject x) = x" |
|
28 |
by (rule project_inject_cancel) |
|
29 |
qed |
|
| 25171 | 30 |
|
| 45358 | 31 |
lemma project_inject_comp_id [statefun_simp]: "project \<circ> inject = id" |
| 25171 | 32 |
by (rule ext) (simp add: project_inject_cancel) |
33 |
||
| 45358 | 34 |
lemma project_inject_comp_cancel[statefun_simp]: "f \<circ> project \<circ> inject = f" |
| 25171 | 35 |
by (rule ext) (simp add: project_inject_cancel) |
36 |
||
| 45358 | 37 |
end |
| 25171 | 38 |
|
| 62390 | 39 |
end |