src/HOL/Statespace/StateSpaceSyntax.thy
author wenzelm
Sun, 13 Mar 2011 22:55:50 +0100
changeset 41959 b460124855b8
parent 38838 62f6ba39b3d4
child 52143 36ffe23b25f8
permissions -rw-r--r--
tuned headers;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
41959
b460124855b8 tuned headers;
wenzelm
parents: 38838
diff changeset
     1
(*  Title:      HOL/Statespace/StateSpaceSyntax.thy
25171
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
     2
    Author:     Norbert Schirmer, TU Muenchen
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
     3
*)
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
     4
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
     5
header {* Syntax for State Space Lookup and Update \label{sec:StateSpaceSyntax}*}
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
     6
theory StateSpaceSyntax
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
     7
imports StateSpaceLocale
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
     8
begin
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
     9
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
    10
text {* The state space syntax is kept in an extra theory so that you
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
    11
can choose if you want to use it or not.  *}
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
    12
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
    13
syntax 
35114
b1fd1d756e20 formal markup of @{syntax_const} and @{const_syntax};
wenzelm
parents: 25171
diff changeset
    14
  "_statespace_lookup" :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'c"  ("_\<cdot>_" [60, 60] 60)
b1fd1d756e20 formal markup of @{syntax_const} and @{const_syntax};
wenzelm
parents: 25171
diff changeset
    15
  "_statespace_update" :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'c \<Rightarrow> ('a \<Rightarrow> 'b)"
b1fd1d756e20 formal markup of @{syntax_const} and @{const_syntax};
wenzelm
parents: 25171
diff changeset
    16
  "_statespace_updates" :: "('a \<Rightarrow> 'b) \<Rightarrow> updbinds \<Rightarrow> ('a \<Rightarrow> 'b)"  ("_<_>" [900, 0] 900)
25171
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
    17
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
    18
translations
35114
b1fd1d756e20 formal markup of @{syntax_const} and @{const_syntax};
wenzelm
parents: 25171
diff changeset
    19
  "_statespace_updates f (_updbinds b bs)" ==
b1fd1d756e20 formal markup of @{syntax_const} and @{const_syntax};
wenzelm
parents: 25171
diff changeset
    20
    "_statespace_updates (_statespace_updates f b) bs"
b1fd1d756e20 formal markup of @{syntax_const} and @{const_syntax};
wenzelm
parents: 25171
diff changeset
    21
  "s<x:=y>" == "_statespace_update s x y"
25171
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
    22
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
    23
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
    24
parse_translation (advanced)
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
    25
{*
35114
b1fd1d756e20 formal markup of @{syntax_const} and @{const_syntax};
wenzelm
parents: 25171
diff changeset
    26
 [(@{syntax_const "_statespace_lookup"}, StateSpace.lookup_tr),
b1fd1d756e20 formal markup of @{syntax_const} and @{const_syntax};
wenzelm
parents: 25171
diff changeset
    27
  (@{syntax_const "_statespace_update"}, StateSpace.update_tr)]
25171
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
    28
*}
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
    29
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
    30
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
    31
print_translation (advanced)
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
    32
{*
35114
b1fd1d756e20 formal markup of @{syntax_const} and @{const_syntax};
wenzelm
parents: 25171
diff changeset
    33
 [(@{const_syntax lookup}, StateSpace.lookup_tr'),
b1fd1d756e20 formal markup of @{syntax_const} and @{const_syntax};
wenzelm
parents: 25171
diff changeset
    34
  (@{const_syntax update}, StateSpace.update_tr')]
25171
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
    35
*}
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
    36
35114
b1fd1d756e20 formal markup of @{syntax_const} and @{const_syntax};
wenzelm
parents: 25171
diff changeset
    37
end