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