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