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