src/HOL/Statespace/StateSpaceSyntax.thy
author haftmann
Sun Oct 08 22:28:22 2017 +0200 (23 months ago)
changeset 66816 212a3334e7da
parent 63167 0909deb8059b
child 69597 ff784d5a5bfb
permissions -rw-r--r--
more fundamental definition of div and mod on int
wenzelm@41959
     1
(*  Title:      HOL/Statespace/StateSpaceSyntax.thy
schirmer@25171
     2
    Author:     Norbert Schirmer, TU Muenchen
schirmer@25171
     3
*)
schirmer@25171
     4
wenzelm@63167
     5
section \<open>Syntax for State Space Lookup and Update \label{sec:StateSpaceSyntax}\<close>
schirmer@25171
     6
theory StateSpaceSyntax
schirmer@25171
     7
imports StateSpaceLocale
schirmer@25171
     8
begin
schirmer@25171
     9
wenzelm@63167
    10
text \<open>The state space syntax is kept in an extra theory so that you
wenzelm@63167
    11
can choose if you want to use it or not.\<close>
schirmer@25171
    12
schirmer@25171
    13
syntax 
wenzelm@35114
    14
  "_statespace_lookup" :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'c"  ("_\<cdot>_" [60, 60] 60)
wenzelm@35114
    15
  "_statespace_update" :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'c \<Rightarrow> ('a \<Rightarrow> 'b)"
wenzelm@35114
    16
  "_statespace_updates" :: "('a \<Rightarrow> 'b) \<Rightarrow> updbinds \<Rightarrow> ('a \<Rightarrow> 'b)"  ("_<_>" [900, 0] 900)
schirmer@25171
    17
schirmer@25171
    18
translations
wenzelm@35114
    19
  "_statespace_updates f (_updbinds b bs)" ==
wenzelm@35114
    20
    "_statespace_updates (_statespace_updates f b) bs"
wenzelm@35114
    21
  "s<x:=y>" == "_statespace_update s x y"
schirmer@25171
    22
schirmer@25171
    23
wenzelm@52143
    24
parse_translation
wenzelm@63167
    25
\<open>
wenzelm@35114
    26
 [(@{syntax_const "_statespace_lookup"}, StateSpace.lookup_tr),
wenzelm@35114
    27
  (@{syntax_const "_statespace_update"}, StateSpace.update_tr)]
wenzelm@63167
    28
\<close>
schirmer@25171
    29
schirmer@25171
    30
wenzelm@52143
    31
print_translation
wenzelm@63167
    32
\<open>
wenzelm@35114
    33
 [(@{const_syntax lookup}, StateSpace.lookup_tr'),
wenzelm@35114
    34
  (@{const_syntax update}, StateSpace.update_tr')]
wenzelm@63167
    35
\<close>
schirmer@25171
    36
wenzelm@35114
    37
end