isabelle: src/HOL/Statespace/StateSpaceSyntax.thy@a88e07c8d0d5 (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
58889 5b7a9633cfa8 modernized header uniformly as section; wenzelm parents: 52143 diff changeset	5	section {* Syntax for State Space Lookup and Update \label{sec:StateSpaceSyntax}*}
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
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
52143 36ffe23b25f8 syntax translations always depend on context; wenzelm parents: 41959 diff changeset	24	parse_translation
25171 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
52143 36ffe23b25f8 syntax translations always depend on context; wenzelm parents: 41959 diff changeset	31	print_translation
25171 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

author	nipkow
	Mon, 02 Nov 2015 18:35:30 +0100
changeset 61534	a88e07c8d0d5
parent 58889	5b7a9633cfa8
child 63167	0909deb8059b
permissions	-rw-r--r--