|
1 (* Title: StateSpaceSyntax.thy |
|
2 ID: $Id$ |
|
3 Author: Norbert Schirmer, TU Muenchen |
|
4 *) |
|
5 |
|
6 header {* Syntax for State Space Lookup and Update \label{sec:StateSpaceSyntax}*} |
|
7 theory StateSpaceSyntax |
|
8 imports StateSpaceLocale |
|
9 |
|
10 begin |
|
11 |
|
12 text {* The state space syntax is kept in an extra theory so that you |
|
13 can choose if you want to use it or not. *} |
|
14 |
|
15 syntax |
|
16 "_statespace_lookup" :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'c" ("_\<cdot>_" [60,60] 60) |
|
17 "_statespace_update" :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'c \<Rightarrow> ('a \<Rightarrow> 'b)" |
|
18 "_statespace_updates" :: "('a \<Rightarrow> 'b) \<Rightarrow> updbinds \<Rightarrow> ('a \<Rightarrow> 'b)" ("_<_>" [900,0] 900) |
|
19 |
|
20 translations |
|
21 "_statespace_updates f (_updbinds b bs)" == |
|
22 "_statespace_updates (_statespace_updates f b) bs" |
|
23 "s<x:=y>" == "_statespace_update s x y" |
|
24 |
|
25 |
|
26 parse_translation (advanced) |
|
27 {* |
|
28 [("_statespace_lookup",StateSpace.lookup_tr), |
|
29 ("_get",StateSpace.lookup_tr), |
|
30 ("_statespace_update",StateSpace.update_tr)] |
|
31 *} |
|
32 |
|
33 |
|
34 print_translation (advanced) |
|
35 {* |
|
36 [("lookup",StateSpace.lookup_tr'), |
|
37 ("StateFun.lookup",StateSpace.lookup_tr'), |
|
38 ("update",StateSpace.update_tr'), |
|
39 ("StateFun.update",StateSpace.update_tr')] |
|
40 *} |
|
41 |
|
42 end |