isabelle: src/HOL/Statespace/StateSpaceSyntax.thy@1ffd5a055acf (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
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	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
4a9c25bffc9b added Statespace library schirmer parents: diff changeset	24	parse_translation (advanced)
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
4a9c25bffc9b added Statespace library schirmer parents: diff changeset	31	print_translation (advanced)
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	haftmann
	Sat, 15 Sep 2012 20:14:29 +0200
changeset 49388	1ffd5a055acf
parent 41959	b460124855b8
child 52143	36ffe23b25f8
permissions	-rw-r--r--