src/HOL/Statespace/StateSpaceSyntax.thy
changeset 25171 4a9c25bffc9b
child 35114 b1fd1d756e20
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Statespace/StateSpaceSyntax.thy	Wed Oct 24 18:36:09 2007 +0200
     1.3 @@ -0,0 +1,42 @@
     1.4 +(*  Title:      StateSpaceSyntax.thy
     1.5 +    ID:         $Id$
     1.6 +    Author:     Norbert Schirmer, TU Muenchen
     1.7 +*)
     1.8 +
     1.9 +header {* Syntax for State Space Lookup and Update \label{sec:StateSpaceSyntax}*}
    1.10 +theory StateSpaceSyntax
    1.11 +imports StateSpaceLocale
    1.12 +
    1.13 +begin
    1.14 +
    1.15 +text {* The state space syntax is kept in an extra theory so that you
    1.16 +can choose if you want to use it or not.  *}
    1.17 +
    1.18 +syntax 
    1.19 + "_statespace_lookup" :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'c" ("_\<cdot>_" [60,60] 60)
    1.20 + "_statespace_update" :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'c \<Rightarrow> ('a \<Rightarrow> 'b)"
    1.21 + "_statespace_updates" :: "('a \<Rightarrow> 'b) \<Rightarrow> updbinds \<Rightarrow> ('a \<Rightarrow> 'b)" ("_<_>" [900,0] 900)
    1.22 +
    1.23 +translations
    1.24 +  "_statespace_updates f (_updbinds b bs)"  == 
    1.25 +     "_statespace_updates (_statespace_updates f b) bs"
    1.26 +  "s<x:=y>"                     == "_statespace_update s x y"
    1.27 +
    1.28 +
    1.29 +parse_translation (advanced)
    1.30 +{*
    1.31 +[("_statespace_lookup",StateSpace.lookup_tr),
    1.32 + ("_get",StateSpace.lookup_tr),
    1.33 + ("_statespace_update",StateSpace.update_tr)] 
    1.34 +*}
    1.35 +
    1.36 +
    1.37 +print_translation (advanced)
    1.38 +{*
    1.39 +[("lookup",StateSpace.lookup_tr'),
    1.40 + ("StateFun.lookup",StateSpace.lookup_tr'),
    1.41 + ("update",StateSpace.update_tr'),
    1.42 + ("StateFun.update",StateSpace.update_tr')] 
    1.43 +*}
    1.44 +
    1.45 +end
    1.46 \ No newline at end of file