src/HOL/Statespace/StateSpaceSyntax.thy
author wenzelm
Sat May 25 15:37:53 2013 +0200 (2013-05-25)
changeset 52143 36ffe23b25f8
parent 41959 b460124855b8
child 58889 5b7a9633cfa8
permissions -rw-r--r--
syntax translations always depend on context;
wenzelm@41959
     1
(*  Title:      HOL/Statespace/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
begin
schirmer@25171
     9
schirmer@25171
    10
text {* The state space syntax is kept in an extra theory so that you
schirmer@25171
    11
can choose if you want to use it or not.  *}
schirmer@25171
    12
schirmer@25171
    13
syntax 
wenzelm@35114
    14
  "_statespace_lookup" :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'c"  ("_\<cdot>_" [60, 60] 60)
wenzelm@35114
    15
  "_statespace_update" :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'c \<Rightarrow> ('a \<Rightarrow> 'b)"
wenzelm@35114
    16
  "_statespace_updates" :: "('a \<Rightarrow> 'b) \<Rightarrow> updbinds \<Rightarrow> ('a \<Rightarrow> 'b)"  ("_<_>" [900, 0] 900)
schirmer@25171
    17
schirmer@25171
    18
translations
wenzelm@35114
    19
  "_statespace_updates f (_updbinds b bs)" ==
wenzelm@35114
    20
    "_statespace_updates (_statespace_updates f b) bs"
wenzelm@35114
    21
  "s<x:=y>" == "_statespace_update s x y"
schirmer@25171
    22
schirmer@25171
    23
wenzelm@52143
    24
parse_translation
schirmer@25171
    25
{*
wenzelm@35114
    26
 [(@{syntax_const "_statespace_lookup"}, StateSpace.lookup_tr),
wenzelm@35114
    27
  (@{syntax_const "_statespace_update"}, StateSpace.update_tr)]
schirmer@25171
    28
*}
schirmer@25171
    29
schirmer@25171
    30
wenzelm@52143
    31
print_translation
schirmer@25171
    32
{*
wenzelm@35114
    33
 [(@{const_syntax lookup}, StateSpace.lookup_tr'),
wenzelm@35114
    34
  (@{const_syntax update}, StateSpace.update_tr')]
schirmer@25171
    35
*}
schirmer@25171
    36
wenzelm@35114
    37
end