doc-src/IsarRef/logics.tex

 
-\chapter{Object-logic specific elements}\label{ch:logics}
+\chapter{Object-logic Specific Elements}\label{ch:logics}
 
 \section{General logic setup}\label{sec:object-logic}
 
 \indexisarcmd{judgment}
 \indexisarmeth{atomize}\indexisaratt{atomize}

 \end{descr}
 
 
 \section{HOL}
 
-\subsection{Primitive types}\label{sec:typedef}
+\subsection{Primitive types}\label{sec:hol-typedef}
 
 \indexisarcmdof{HOL}{typedecl}\indexisarcmdof{HOL}{typedef}
 \begin{matharray}{rcl}
   \isarcmd{typedecl} & : & \isartrans{theory}{theory} \\
   \isarcmd{typedef} & : & \isartrans{theory}{proof(prove)} \\

   parameters to be introduced.
 
 \end{descr}
 
 
-\section{Records}\label{sec:hol-record}
+\subsection{Records}\label{sec:hol-record}
 
 In principle, records merely generalize the concept of tuples where components
 may be addressed by labels instead of just position.  The logical
 infrastructure of records in Isabelle/HOL is slightly more advanced, though,
 supporting truly extensible record schemes.  This admits operations that are
 polymorphic with respect to record extension, yielding ``object-oriented''
 effects like (single) inheritance.  See also \cite{NaraschewskiW-TPHOLs98} for
 more details on object-oriented verification and record subtyping in HOL.
 
 
-\subsection{Basic concepts}
+\subsubsection{Basic concepts}
 
 Isabelle/HOL supports both \emph{fixed} and \emph{schematic} records at the
 level of terms and types.  The notation is as follows:
 
 \begin{center}

 {\S}\ref{sec:hol-record-thms}).  See also the Isabelle/HOL tutorial
 \cite{isabelle-hol-book} for further instructions on using records in
 practice.
 
 
-\subsection{Record specifications}\label{sec:hol-record-def}
+\subsubsection{Record specifications}\label{sec:hol-record-def}
 
 \indexisarcmdof{HOL}{record}
 \begin{matharray}{rcl}
   \isarcmd{record} & : & \isartrans{theory}{theory} \\
 \end{matharray}

   $(\vec\alpha, \zeta) \, t_scheme$ made an abbreviation for $\record{\vec c
     \ty \vec\sigma\fs \more \ty \zeta}$.
 
 \end{descr}
 
-\subsection{Record operations}\label{sec:hol-record-ops}
+\subsubsection{Record operations}\label{sec:hol-record-ops}
 
 Any record definition of the form presented above produces certain standard
 operations.  Selectors and updates are provided for any field, including the
 improper one ``$more$''.  There are also cumulative record constructor
 functions.  To simplify the presentation below, we assume for now that

 \end{matharray}
 
 \noindent Note that $t{\dtt}make$ and $t{\dtt}fields$ are actually coincide for root records.
 
 
-\subsection{Derived rules and proof tools}\label{sec:hol-record-thms}
+\subsubsection{Derived rules and proof tools}\label{sec:hol-record-thms}
 
 The record package proves several results internally, declaring these facts to
 appropriate proof tools.  This enables users to reason about record structures
 quite comfortably.  Assume that $t$ is a record type as specified above.
 

   elimination rules, $\isarkeyword{inductive_cases}$ provides case split
   theorems at the theory level for later use,
 \end{descr}
 
 
-\subsection{Generating executable code}
+\subsection{Executable code}
 
 Isabelle/Pure provides a generic infrastructure to support code generation
 from executable specifications, both functional and relational programs.
 Isabelle/HOL instantiates these mechanisms in a way that is amenable to
 end-user applications.  See \cite{isabelle-HOL} for further information (this