doc-src/TutorialI/Types/types.tex

added warning about inconsistent context to Metis;
it makes more sense here than in Sledgehammer, because Sledgehammer is unsound and there's no point in having people panicking about the consistency of their context when their context is in fact consistent

\chapter{More about Types}
\label{ch:more-types}

So far we have learned about a few basic types (for example \isa{bool} and
\isa{nat}), type abbreviations (\isacommand{types}) and recursive datatypes
(\isacommand{datatype}). This chapter will introduce more
advanced material:
\begin{itemize}
\item Pairs ({\S}\ref{sec:products}) and records ({\S}\ref{sec:records}),
and how to reason about them.
\item Type classes: how to specify and reason about axiomatic collections of
  types ({\S}\ref{sec:axclass}). This section leads on to a discussion of
  Isabelle's numeric types ({\S}\ref{sec:numbers}).  
\item Introducing your own types: how to define types that
  cannot be constructed with any of the basic methods
  ({\S}\ref{sec:adv-typedef}).
\end{itemize}

The material in this section goes beyond the needs of most novices.
Serious users should at least skim the sections as far as type classes.
That material is fairly advanced; read the beginning to understand what it
is about, but consult the rest only when necessary.

\index{pairs and tuples|(}
\input{Types/document/Pairs}    %%%Section "Pairs and Tuples"
\index{pairs and tuples|)}

\input{Types/document/Records}  %%%Section "Records"


\section{Type Classes} %%%Section
\label{sec:axclass}
\index{axiomatic type classes|(}
\index{*axclass|(}

The programming language Haskell has popularized the notion of type
classes: a type class is a set of types with a
common interface: all types in that class must provide the functions
in the interface.  Isabelle offers a similar type class concept: in
addition, properties (\emph{class axioms}) can be specified which any
instance of this type class must obey.  Thus we can talk about a type
$\tau$ being in a class $C$, which is written $\tau :: C$.  This is the case
if $\tau$ satisfies the axioms of $C$. Furthermore, type classes can be
organized in a hierarchy.  Thus there is the notion of a class $D$
being a subclass\index{subclasses} of a class $C$, written $D
< C$. This is the case if all axioms of $C$ are also provable in $D$.

In this section we introduce the most important concepts behind type
classes by means of a running example from algebra.  This should give
you an intuition how to use type classes and to understand
specifications involving type classes.  Type classes are covered more
deeply in a separate tutorial \cite{isabelle-classes}.

\subsection{Overloading}
\label{sec:overloading}
\index{overloading|(}

\input{Types/document/Overloading}

\index{overloading|)}

\input{Types/document/Axioms}

\index{type classes|)}
\index{*class|)}

\input{Types/numerics}             %%%Section "Numbers"

\input{Types/document/Typedefs}    %%%Section "Introducing New Types"