src/HOL/Statespace/StateSpaceSyntax.thy
author wenzelm
Thu Feb 11 22:55:16 2010 +0100 (2010-02-11)
changeset 35114 b1fd1d756e20
parent 25171 4a9c25bffc9b
child 38838 62f6ba39b3d4
permissions -rw-r--r--
formal markup of @{syntax_const} and @{const_syntax};
authentic syntax for extra robustness;
schirmer@25171
     1
(*  Title:      StateSpaceSyntax.thy
schirmer@25171
     2
    Author:     Norbert Schirmer, TU Muenchen
schirmer@25171
     3
*)
schirmer@25171
     4
schirmer@25171
     5
header {* Syntax for State Space Lookup and Update \label{sec:StateSpaceSyntax}*}
schirmer@25171
     6
theory StateSpaceSyntax
schirmer@25171
     7
imports StateSpaceLocale
schirmer@25171
     8
schirmer@25171
     9
begin
schirmer@25171
    10
schirmer@25171
    11
text {* The state space syntax is kept in an extra theory so that you
schirmer@25171
    12
can choose if you want to use it or not.  *}
schirmer@25171
    13
schirmer@25171
    14
syntax 
wenzelm@35114
    15
  "_statespace_lookup" :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'c"  ("_\<cdot>_" [60, 60] 60)
wenzelm@35114
    16
  "_statespace_update" :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'c \<Rightarrow> ('a \<Rightarrow> 'b)"
wenzelm@35114
    17
  "_statespace_updates" :: "('a \<Rightarrow> 'b) \<Rightarrow> updbinds \<Rightarrow> ('a \<Rightarrow> 'b)"  ("_<_>" [900, 0] 900)
schirmer@25171
    18
schirmer@25171
    19
translations
wenzelm@35114
    20
  "_statespace_updates f (_updbinds b bs)" ==
wenzelm@35114
    21
    "_statespace_updates (_statespace_updates f b) bs"
wenzelm@35114
    22
  "s<x:=y>" == "_statespace_update s x y"
schirmer@25171
    23
schirmer@25171
    24
schirmer@25171
    25
parse_translation (advanced)
schirmer@25171
    26
{*
wenzelm@35114
    27
 [(@{syntax_const "_statespace_lookup"}, StateSpace.lookup_tr),
wenzelm@35114
    28
  (@{syntax_const "_statespace_update"}, StateSpace.update_tr)]
schirmer@25171
    29
*}
schirmer@25171
    30
schirmer@25171
    31
schirmer@25171
    32
print_translation (advanced)
schirmer@25171
    33
{*
wenzelm@35114
    34
 [(@{const_syntax lookup}, StateSpace.lookup_tr'),
wenzelm@35114
    35
  (@{const_syntax update}, StateSpace.update_tr')]
schirmer@25171
    36
*}
schirmer@25171
    37
wenzelm@35114
    38
end