src/HOL/Statespace/StateSpaceSyntax.thy
author wenzelm
Sun Mar 13 22:55:50 2011 +0100 (2011-03-13)
changeset 41959 b460124855b8
parent 38838 62f6ba39b3d4
child 52143 36ffe23b25f8
permissions -rw-r--r--
tuned headers;
     1 (*  Title:      HOL/Statespace/StateSpaceSyntax.thy
     2     Author:     Norbert Schirmer, TU Muenchen
     3 *)
     4 
     5 header {* Syntax for State Space Lookup and Update \label{sec:StateSpaceSyntax}*}
     6 theory StateSpaceSyntax
     7 imports StateSpaceLocale
     8 begin
     9 
    10 text {* The state space syntax is kept in an extra theory so that you
    11 can choose if you want to use it or not.  *}
    12 
    13 syntax 
    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 
    18 translations
    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 
    24 parse_translation (advanced)
    25 {*
    26  [(@{syntax_const "_statespace_lookup"}, StateSpace.lookup_tr),
    27   (@{syntax_const "_statespace_update"}, StateSpace.update_tr)]
    28 *}
    29 
    30 
    31 print_translation (advanced)
    32 {*
    33  [(@{const_syntax lookup}, StateSpace.lookup_tr'),
    34   (@{const_syntax update}, StateSpace.update_tr')]
    35 *}
    36 
    37 end