1\documentclass[11pt,a4paper]{article}
2\usepackage{isabelle,isabellesym}
3% this should be the last package used
4\usepackage{pdfsetup}
5
6% urls in roman style, theory text in math-similar italics
7\urlstyle{rm}
8\isabellestyle{it}
9
10
11\begin{document}
12
13\title{State Spaces: The Locale Way}
14\author{Norbert Schirmer}
15\maketitle
16
17\tableofcontents
18
19\parindent 0pt\parskip 0.5ex
20
21\section{Introduction}
22
23These theories introduce a new command called \isacommand{statespace}.
24It's usage is similar to \isacommand{record}s. However, the command
25does not introduce a new type but an abstract specification based on
26the locale infrastructure. This leads to extra flexibility in
27composing state space components, in particular multiple inheritance
28and renaming of components.
29
30The state space infrastructure basically manages the following things:
31\begin{itemize}
32\item distinctness of field names
33\item projections~/ injections from~/ to an abstract \emph{value} type
34\item syntax translations for lookup and update, hiding the
35  projections and injections
36\item simplification procedure for lookups~/ updates, similar to
37  records
38\end{itemize}
39
40
41\paragraph{Overview}
42In Section \ref{sec:DistinctTreeProver} we define distinctness of the
43nodes in a binary tree and provide the basic prover tools to support
44efficient distinctness reasoning for field names managed by state
45spaces. The state is represented as a function from (abstract) names
46to (abstract) values as introduced in Section \ref{sec:StateFun}. The
47basic setup for state spaces is in Section
48\ref{sec:StateSpaceLocale}. Some syntax for lookup and updates is
49added in Section \ref{sec:StateSpaceSyntax}. Finally Section
50\ref{sec:Examples} explains the usage of state spaces by examples.
51
52
53% generated text of all theories
54\input{session}
55
56% optional bibliography
57%\bibliographystyle{abbrv}
58%\bibliography{root}
59
60\end{document}
61
62%%% Local Variables:
63%%% mode: latex
64%%% TeX-master: t
65%%% End:
66