1(* Title: HOL/Statespace/StateSpaceSyntax.thy 2 Author: Norbert Schirmer, TU Muenchen 3*) 4 5section \<open>Syntax for State Space Lookup and Update \label{sec:StateSpaceSyntax}\<close> 6theory StateSpaceSyntax 7imports StateSpaceLocale 8begin 9 10text \<open>The state space syntax is kept in an extra theory so that you 11can choose if you want to use it or not.\<close> 12 13syntax 14 "_statespace_lookup" :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'c" ("_\<cdot>_" [60, 60] 60) 15 "_statespace_update" :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'c \<Rightarrow> ('a \<Rightarrow> 'b)" 16 "_statespace_updates" :: "('a \<Rightarrow> 'b) \<Rightarrow> updbinds \<Rightarrow> ('a \<Rightarrow> 'b)" ("_<_>" [900, 0] 900) 17 18translations 19 "_statespace_updates f (_updbinds b bs)" == 20 "_statespace_updates (_statespace_updates f b) bs" 21 "s<x:=y>" == "_statespace_update s x y" 22 23 24parse_translation 25\<open> 26 [(@{syntax_const "_statespace_lookup"}, StateSpace.lookup_tr), 27 (@{syntax_const "_statespace_update"}, StateSpace.update_tr)] 28\<close> 29 30 31print_translation 32\<open> 33 [(@{const_syntax lookup}, StateSpace.lookup_tr'), 34 (@{const_syntax update}, StateSpace.update_tr')] 35\<close> 36 37end 38