src/HOL/Statespace/StateSpaceSyntax.thy

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Statespace/StateSpaceSyntax.thy	Wed Oct 24 18:36:09 2007 +0200
@@ -0,0 +1,42 @@
+(*  Title:      StateSpaceSyntax.thy
+    ID:         $Id$
+    Author:     Norbert Schirmer, TU Muenchen
+*)
+
+header {* Syntax for State Space Lookup and Update \label{sec:StateSpaceSyntax}*}
+theory StateSpaceSyntax
+imports StateSpaceLocale
+
+begin
+
+text {* The state space syntax is kept in an extra theory so that you
+can choose if you want to use it or not.  *}
+
+syntax 
+ "_statespace_lookup" :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'c" ("_\<cdot>_" [60,60] 60)
+ "_statespace_update" :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'c \<Rightarrow> ('a \<Rightarrow> 'b)"
+ "_statespace_updates" :: "('a \<Rightarrow> 'b) \<Rightarrow> updbinds \<Rightarrow> ('a \<Rightarrow> 'b)" ("_<_>" [900,0] 900)
+
+translations
+  "_statespace_updates f (_updbinds b bs)"  == 
+     "_statespace_updates (_statespace_updates f b) bs"
+  "s<x:=y>"                     == "_statespace_update s x y"
+
+
+parse_translation (advanced)
+{*
+[("_statespace_lookup",StateSpace.lookup_tr),
+ ("_get",StateSpace.lookup_tr),
+ ("_statespace_update",StateSpace.update_tr)] 
+*}
+
+
+print_translation (advanced)
+{*
+[("lookup",StateSpace.lookup_tr'),
+ ("StateFun.lookup",StateSpace.lookup_tr'),
+ ("update",StateSpace.update_tr'),
+ ("StateFun.update",StateSpace.update_tr')] 
+*}
+
+end
\ No newline at end of file