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

25171 4a9c25bffc9b added Statespace library schirmer parents: diff changeset	1	(* Title: StateSpaceSyntax.thy
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
4a9c25bffc9b added Statespace library schirmer parents: diff changeset	9	begin
4a9c25bffc9b added Statespace library schirmer parents: diff changeset	10
4a9c25bffc9b added Statespace library schirmer parents: diff changeset	11	text {* The state space syntax is kept in an extra theory so that you
4a9c25bffc9b added Statespace library schirmer parents: diff changeset	12	can choose if you want to use it or not. *}
4a9c25bffc9b added Statespace library schirmer parents: diff changeset	13
4a9c25bffc9b added Statespace library schirmer parents: diff changeset	14	syntax
35114 b1fd1d756e20 formal markup of @{syntax_const} and @{const_syntax}; wenzelm parents: 25171 diff changeset	15	"_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	16	"_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	17	"_statespace_updates" :: "('a \<Rightarrow> 'b) \<Rightarrow> updbinds \<Rightarrow> ('a \<Rightarrow> 'b)" ("_<_>" [900, 0] 900)
25171 4a9c25bffc9b added Statespace library schirmer parents: diff changeset	18
4a9c25bffc9b added Statespace library schirmer parents: diff changeset	19	translations
35114 b1fd1d756e20 formal markup of @{syntax_const} and @{const_syntax}; wenzelm parents: 25171 diff changeset	20	"_statespace_updates f (_updbinds b bs)" ==
b1fd1d756e20 formal markup of @{syntax_const} and @{const_syntax}; wenzelm parents: 25171 diff changeset	21	"_statespace_updates (_statespace_updates f b) bs"
b1fd1d756e20 formal markup of @{syntax_const} and @{const_syntax}; wenzelm parents: 25171 diff changeset	22	"s<x:=y>" == "_statespace_update s x y"
25171 4a9c25bffc9b added Statespace library schirmer parents: diff changeset	23
4a9c25bffc9b added Statespace library schirmer parents: diff changeset	24
4a9c25bffc9b added Statespace library schirmer parents: diff changeset	25	parse_translation (advanced)
4a9c25bffc9b added Statespace library schirmer parents: diff changeset	26	{*
35114 b1fd1d756e20 formal markup of @{syntax_const} and @{const_syntax}; wenzelm parents: 25171 diff changeset	27	[(@{syntax_const "_statespace_lookup"}, StateSpace.lookup_tr),
b1fd1d756e20 formal markup of @{syntax_const} and @{const_syntax}; wenzelm parents: 25171 diff changeset	28	(@{syntax_const "_statespace_update"}, StateSpace.update_tr)]
25171 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
4a9c25bffc9b added Statespace library schirmer parents: diff changeset	32	print_translation (advanced)
4a9c25bffc9b added Statespace library schirmer parents: diff changeset	33	{*
35114 b1fd1d756e20 formal markup of @{syntax_const} and @{const_syntax}; wenzelm parents: 25171 diff changeset	34	[(@{const_syntax lookup}, StateSpace.lookup_tr'),
b1fd1d756e20 formal markup of @{syntax_const} and @{const_syntax}; wenzelm parents: 25171 diff changeset	35	(@{const_syntax update}, StateSpace.update_tr')]
25171 4a9c25bffc9b added Statespace library schirmer parents: diff changeset	36	*}
4a9c25bffc9b added Statespace library schirmer parents: diff changeset	37
35114 b1fd1d756e20 formal markup of @{syntax_const} and @{const_syntax}; wenzelm parents: 25171 diff changeset	38	end

author	haftmann
	Thu, 29 Apr 2010 15:00:41 +0200
changeset 36533	f8df589ca2a5
parent 35114	b1fd1d756e20
child 38838	62f6ba39b3d4
permissions	-rw-r--r--