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