--- a/doc-src/TutorialI/Types/document/Typedefs.tex Fri Nov 30 12:18:14 2001 +0100
+++ b/doc-src/TutorialI/Types/document/Typedefs.tex Fri Nov 30 17:55:13 2001 +0100
@@ -78,13 +78,9 @@
Now we come to the most general means of safely introducing a new type, the
\textbf{type definition}. All other means, for example
\isacommand{datatype}, are based on it. The principle is extremely simple:
-any non-empty subset of an existing type can be turned into a new type. Thus
-a type definition is merely a notational device: you introduce a new name for
-a subset of an existing type. This does not add any logical power to HOL,
-because you could base all your work directly on the subset of the existing
-type. However, the resulting theories could easily become indigestible
-because instead of implicit types you would have explicit sets in your
-formulae.
+any non-empty subset of an existing type can be turned into a new type.
+More precisely, the new type is specified to be isomorphic to some
+non-empty subset of an existing type.
Let us work a simple example, the definition of a three-element type.
It is easily represented by the first three natural numbers:%
@@ -108,9 +104,9 @@
%
\begin{isamarkuptext}%
This type definition introduces the new type \isa{three} and asserts
-that it is a copy of the set \isa{{\isacharbraceleft}{\isadigit{0}}{\isasymColon}{\isacharprime}a{\isacharcomma}\ {\isadigit{1}}{\isasymColon}{\isacharprime}a{\isacharcomma}\ {\isadigit{2}}{\isasymColon}{\isacharprime}a{\isacharbraceright}}. This assertion
+that it is a copy of the set \isa{{\isacharbraceleft}{\isadigit{0}}{\isacharcomma}\ {\isadigit{1}}{\isacharcomma}\ {\isadigit{2}}{\isacharbraceright}}. This assertion
is expressed via a bijection between the \emph{type} \isa{three} and the
-\emph{set} \isa{{\isacharbraceleft}{\isadigit{0}}{\isasymColon}{\isacharprime}a{\isacharcomma}\ {\isadigit{1}}{\isasymColon}{\isacharprime}a{\isacharcomma}\ {\isadigit{2}}{\isasymColon}{\isacharprime}a{\isacharbraceright}}. To this end, the command declares the following
+\emph{set} \isa{{\isacharbraceleft}{\isadigit{0}}{\isacharcomma}\ {\isadigit{1}}{\isacharcomma}\ {\isadigit{2}}{\isacharbraceright}}. To this end, the command declares the following
constants behind the scenes:
\begin{center}
\begin{tabular}{rcl}
@@ -151,7 +147,7 @@
%
From this example it should be clear what \isacommand{typedef} does
in general given a name (here \isa{three}) and a set
-(here \isa{{\isacharbraceleft}n{\isachardot}\ n\ {\isasymle}\ {\isacharparenleft}{\isadigit{2}}{\isasymColon}{\isacharprime}a{\isacharparenright}{\isacharbraceright}}).
+(here \isa{{\isacharbraceleft}n{\isachardot}\ n\ {\isasymle}\ {\isadigit{2}}{\isacharbraceright}}).
Our next step is to define the basic functions expected on the new type.
Although this depends on the type at hand, the following strategy works well:
@@ -281,7 +277,7 @@
above lengthy definition can be collapsed into one line:%
\end{isamarkuptext}%
\isamarkuptrue%
-\isacommand{datatype}\ three{\isacharprime}\ {\isacharequal}\ A\ {\isacharbar}\ B\ {\isacharbar}\ C\isamarkupfalse%
+\isacommand{datatype}\ better{\isacharunderscore}three\ {\isacharequal}\ A\ {\isacharbar}\ B\ {\isacharbar}\ C\isamarkupfalse%
%
\begin{isamarkuptext}%
\noindent