isabelle: src/HOL/Statespace/StateSpaceSyntax.thy@2803d2b8f85d (annotated)

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
63167 0909deb8059b isabelle update_cartouches -c -t; wenzelm parents: 58889 diff changeset	5	section \<open>Syntax for State Space Lookup and Update \label{sec:StateSpaceSyntax}\<close>
25171 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
63167 0909deb8059b isabelle update_cartouches -c -t; wenzelm parents: 58889 diff changeset	10	text \<open>The state space syntax is kept in an extra theory so that you
0909deb8059b isabelle update_cartouches -c -t; wenzelm parents: 58889 diff changeset	11	can choose if you want to use it or not.\<close>
25171 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
52143 36ffe23b25f8 syntax translations always depend on context; wenzelm parents: 41959 diff changeset	24	parse_translation
63167 0909deb8059b isabelle update_cartouches -c -t; wenzelm parents: 58889 diff changeset	25	\<open>
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)]
63167 0909deb8059b isabelle update_cartouches -c -t; wenzelm parents: 58889 diff changeset	28	\<close>
25171 4a9c25bffc9b added Statespace library schirmer parents: diff changeset	29
4a9c25bffc9b added Statespace library schirmer parents: diff changeset	30
52143 36ffe23b25f8 syntax translations always depend on context; wenzelm parents: 41959 diff changeset	31	print_translation
63167 0909deb8059b isabelle update_cartouches -c -t; wenzelm parents: 58889 diff changeset	32	\<open>
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')]
63167 0909deb8059b isabelle update_cartouches -c -t; wenzelm parents: 58889 diff changeset	35	\<close>
25171 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

author	wenzelm
	Tue, 19 Jul 2016 09:55:03 +0200
changeset 63520	2803d2b8f85d
parent 63167	0909deb8059b
child 69597	ff784d5a5bfb
permissions	-rw-r--r--