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