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