src/HOL/Statespace/StateSpaceSyntax.thy
author wenzelm
Thu May 26 17:51:22 2016 +0200 (2016-05-26)
changeset 63167 0909deb8059b
parent 58889 5b7a9633cfa8
child 69597 ff784d5a5bfb
permissions -rw-r--r--
isabelle update_cartouches -c -t;
     1 (*  Title:      HOL/Statespace/StateSpaceSyntax.thy
     2     Author:     Norbert Schirmer, TU Muenchen
     3 *)
     4 
     5 section \<open>Syntax for State Space Lookup and Update \label{sec:StateSpaceSyntax}\<close>
     6 theory StateSpaceSyntax
     7 imports StateSpaceLocale
     8 begin
     9 
    10 text \<open>The state space syntax is kept in an extra theory so that you
    11 can choose if you want to use it or not.\<close>
    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
    25 \<open>
    26  [(@{syntax_const "_statespace_lookup"}, StateSpace.lookup_tr),
    27   (@{syntax_const "_statespace_update"}, StateSpace.update_tr)]
    28 \<close>
    29 
    30 
    31 print_translation
    32 \<open>
    33  [(@{const_syntax lookup}, StateSpace.lookup_tr'),
    34   (@{const_syntax update}, StateSpace.update_tr')]
    35 \<close>
    36 
    37 end