doc-src/TutorialI/document/types0.tex

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/document/types0.tex	Tue Aug 28 14:37:57 2012 +0200
@@ -0,0 +1,69 @@
+\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{Pairs}    %%%Section "Pairs and Tuples"
+\index{pairs and tuples|)}
+
+\input{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{Overloading}
+
+\index{overloading|)}
+
+\input{Axioms}
+
+\index{type classes|)}
+\index{*class|)}
+
+\input{numerics}             %%%Section "Numbers"
+
+\input{Typedefs}    %%%Section "Introducing New Types"