doc-src/TutorialI/Types/document/Typedefs.tex
author wenzelm
Fri, 18 Jan 2002 18:30:19 +0100
changeset 12815 1f073030b97a
parent 12627 08eee994bf99
child 13750 b5cd10cb106b
permissions -rw-r--r--
tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
11898
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
     1
%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
     2
\begin{isabellebody}%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
     3
\def\isabellecontext{Typedefs}%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
     4
\isamarkupfalse%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
     5
%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
     6
\isamarkupsection{Introducing New Types%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
     7
}
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
     8
\isamarkuptrue%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
     9
%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    10
\begin{isamarkuptext}%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    11
\label{sec:adv-typedef}
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    12
For most applications, a combination of predefined types like \isa{bool} and
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    13
\isa{{\isasymRightarrow}} with recursive datatypes and records is quite sufficient. Very
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    14
occasionally you may feel the need for a more advanced type.  If you
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    15
are certain that your type is not definable by any of the
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    16
standard means, then read on.
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    17
\begin{warn}
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    18
  Types in HOL must be non-empty; otherwise the quantifier rules would be
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    19
  unsound, because $\exists x.\ x=x$ is a theorem.
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    20
\end{warn}%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    21
\end{isamarkuptext}%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    22
\isamarkuptrue%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    23
%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    24
\isamarkupsubsection{Declaring New Types%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    25
}
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    26
\isamarkuptrue%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    27
%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    28
\begin{isamarkuptext}%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    29
\label{sec:typedecl}
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    30
\index{types!declaring|(}%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    31
\index{typedecl@\isacommand {typedecl} (command)}%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    32
The most trivial way of introducing a new type is by a \textbf{type
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    33
declaration}:%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    34
\end{isamarkuptext}%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    35
\isamarkuptrue%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    36
\isacommand{typedecl}\ my{\isacharunderscore}new{\isacharunderscore}type\isamarkupfalse%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    37
%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    38
\begin{isamarkuptext}%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    39
\noindent
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    40
This does not define \isa{my{\isacharunderscore}new{\isacharunderscore}type} at all but merely introduces its
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    41
name. Thus we know nothing about this type, except that it is
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    42
non-empty. Such declarations without definitions are
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    43
useful if that type can be viewed as a parameter of the theory.
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    44
A typical example is given in \S\ref{sec:VMC}, where we define a transition
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    45
relation over an arbitrary type of states.
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    46
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    47
In principle we can always get rid of such type declarations by making those
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    48
types parameters of every other type, thus keeping the theory generic. In
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    49
practice, however, the resulting clutter can make types hard to read.
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    50
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    51
If you are looking for a quick and dirty way of introducing a new type
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    52
together with its properties: declare the type and state its properties as
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    53
axioms. Example:%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    54
\end{isamarkuptext}%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    55
\isamarkuptrue%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    56
\isacommand{axioms}\isanewline
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    57
just{\isacharunderscore}one{\isacharcolon}\ {\isachardoublequote}{\isasymexists}x{\isacharcolon}{\isacharcolon}my{\isacharunderscore}new{\isacharunderscore}type{\isachardot}\ {\isasymforall}y{\isachardot}\ x\ {\isacharequal}\ y{\isachardoublequote}\isamarkupfalse%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    58
%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    59
\begin{isamarkuptext}%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    60
\noindent
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    61
However, we strongly discourage this approach, except at explorative stages
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    62
of your development. It is extremely easy to write down contradictory sets of
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    63
axioms, in which case you will be able to prove everything but it will mean
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    64
nothing.  In the example above, the axiomatic approach is
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    65
unnecessary: a one-element type called \isa{unit} is already defined in HOL.
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    66
\index{types!declaring|)}%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    67
\end{isamarkuptext}%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    68
\isamarkuptrue%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    69
%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    70
\isamarkupsubsection{Defining New Types%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    71
}
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    72
\isamarkuptrue%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    73
%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    74
\begin{isamarkuptext}%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    75
\label{sec:typedef}
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    76
\index{types!defining|(}%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    77
\index{typedecl@\isacommand {typedef} (command)|(}%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    78
Now we come to the most general means of safely introducing a new type, the
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    79
\textbf{type definition}. All other means, for example
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    80
\isacommand{datatype}, are based on it. The principle is extremely simple:
12334
60bf75e157e4 *** empty log message ***
nipkow
parents: 12332
diff changeset
    81
any non-empty subset of an existing type can be turned into a new type.
60bf75e157e4 *** empty log message ***
nipkow
parents: 12332
diff changeset
    82
More precisely, the new type is specified to be isomorphic to some
60bf75e157e4 *** empty log message ***
nipkow
parents: 12332
diff changeset
    83
non-empty subset of an existing type.
11898
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    84
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    85
Let us work a simple example, the definition of a three-element type.
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    86
It is easily represented by the first three natural numbers:%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    87
\end{isamarkuptext}%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    88
\isamarkuptrue%
12473
f41e477576b9 *** empty log message ***
nipkow
parents: 12334
diff changeset
    89
\isacommand{typedef}\ three\ {\isacharequal}\ {\isachardoublequote}{\isacharbraceleft}{\isadigit{0}}{\isacharcolon}{\isacharcolon}nat{\isacharcomma}\ {\isadigit{1}}{\isacharcomma}\ {\isadigit{2}}{\isacharbraceright}{\isachardoublequote}\isamarkupfalse%
11898
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    90
%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    91
\begin{isamarkuptxt}%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    92
\noindent
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    93
In order to enforce that the representing set on the right-hand side is
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    94
non-empty, this definition actually starts a proof to that effect:
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    95
\begin{isabelle}%
12473
f41e477576b9 *** empty log message ***
nipkow
parents: 12334
diff changeset
    96
\ {\isadigit{1}}{\isachardot}\ {\isasymexists}x{\isachardot}\ x\ {\isasymin}\ {\isacharbraceleft}{\isadigit{0}}{\isacharcomma}\ {\isadigit{1}}{\isacharcomma}\ {\isadigit{2}}{\isacharbraceright}%
11898
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    97
\end{isabelle}
12473
f41e477576b9 *** empty log message ***
nipkow
parents: 12334
diff changeset
    98
Fortunately, this is easy enough to show, even \isa{auto} could do it.
f41e477576b9 *** empty log message ***
nipkow
parents: 12334
diff changeset
    99
In general, one has to provide a witness, in our case 0:%
11898
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   100
\end{isamarkuptxt}%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   101
\isamarkuptrue%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   102
\isacommand{apply}{\isacharparenleft}rule{\isacharunderscore}tac\ x\ {\isacharequal}\ {\isadigit{0}}\ \isakeyword{in}\ exI{\isacharparenright}\isanewline
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   103
\isamarkupfalse%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   104
\isacommand{by}\ simp\isamarkupfalse%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   105
%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   106
\begin{isamarkuptext}%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   107
This type definition introduces the new type \isa{three} and asserts
12334
60bf75e157e4 *** empty log message ***
nipkow
parents: 12332
diff changeset
   108
that it is a copy of the set \isa{{\isacharbraceleft}{\isadigit{0}}{\isacharcomma}\ {\isadigit{1}}{\isacharcomma}\ {\isadigit{2}}{\isacharbraceright}}. This assertion
11898
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   109
is expressed via a bijection between the \emph{type} \isa{three} and the
12334
60bf75e157e4 *** empty log message ***
nipkow
parents: 12332
diff changeset
   110
\emph{set} \isa{{\isacharbraceleft}{\isadigit{0}}{\isacharcomma}\ {\isadigit{1}}{\isacharcomma}\ {\isadigit{2}}{\isacharbraceright}}. To this end, the command declares the following
11898
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   111
constants behind the scenes:
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   112
\begin{center}
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   113
\begin{tabular}{rcl}
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   114
\isa{three} &::& \isa{nat\ set} \\
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   115
\isa{Rep{\isacharunderscore}three} &::& \isa{three\ {\isasymRightarrow}\ nat}\\
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   116
\isa{Abs{\isacharunderscore}three} &::& \isa{nat\ {\isasymRightarrow}\ three}
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   117
\end{tabular}
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   118
\end{center}
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   119
where constant \isa{three} is explicitly defined as the representing set:
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   120
\begin{center}
12473
f41e477576b9 *** empty log message ***
nipkow
parents: 12334
diff changeset
   121
\isa{three\ {\isasymequiv}\ {\isacharbraceleft}{\isadigit{0}}{\isacharcomma}\ {\isadigit{1}}{\isacharcomma}\ {\isadigit{2}}{\isacharbraceright}}\hfill(\isa{three{\isacharunderscore}def})
11898
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   122
\end{center}
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   123
The situation is best summarized with the help of the following diagram,
12543
3e355f0f079f New type definition diagram
paulson
parents: 12473
diff changeset
   124
where squares denote types and the irregular region denotes a set:
11898
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   125
\begin{center}
12627
08eee994bf99 updated;
wenzelm
parents: 12543
diff changeset
   126
\includegraphics[scale=.8]{typedef}
11898
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   127
\end{center}
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   128
Finally, \isacommand{typedef} asserts that \isa{Rep{\isacharunderscore}three} is
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   129
surjective on the subset \isa{three} and \isa{Abs{\isacharunderscore}three} and \isa{Rep{\isacharunderscore}three} are inverses of each other:
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   130
\begin{center}
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   131
\begin{tabular}{@ {}r@ {\qquad\qquad}l@ {}}
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   132
\isa{Rep{\isacharunderscore}three\ x\ {\isasymin}\ three} & (\isa{Rep{\isacharunderscore}three}) \\
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   133
\isa{Abs{\isacharunderscore}three\ {\isacharparenleft}Rep{\isacharunderscore}three\ x{\isacharparenright}\ {\isacharequal}\ x} & (\isa{Rep{\isacharunderscore}three{\isacharunderscore}inverse}) \\
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   134
\isa{y\ {\isasymin}\ three\ {\isasymLongrightarrow}\ Rep{\isacharunderscore}three\ {\isacharparenleft}Abs{\isacharunderscore}three\ y{\isacharparenright}\ {\isacharequal}\ y} & (\isa{Abs{\isacharunderscore}three{\isacharunderscore}inverse})
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   135
\end{tabular}
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   136
\end{center}
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   137
%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   138
From this example it should be clear what \isacommand{typedef} does
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   139
in general given a name (here \isa{three}) and a set
12473
f41e477576b9 *** empty log message ***
nipkow
parents: 12334
diff changeset
   140
(here \isa{{\isacharbraceleft}{\isadigit{0}}{\isacharcomma}\ {\isadigit{1}}{\isacharcomma}\ {\isadigit{2}}{\isacharbraceright}}).
11898
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   141
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   142
Our next step is to define the basic functions expected on the new type.
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   143
Although this depends on the type at hand, the following strategy works well:
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   144
\begin{itemize}
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   145
\item define a small kernel of basic functions that can express all other
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   146
functions you anticipate.
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   147
\item define the kernel in terms of corresponding functions on the
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   148
representing type using \isa{Abs} and \isa{Rep} to convert between the
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   149
two levels.
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   150
\end{itemize}
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   151
In our example it suffices to give the three elements of type \isa{three}
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   152
names:%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   153
\end{isamarkuptext}%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   154
\isamarkuptrue%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   155
\isacommand{constdefs}\isanewline
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   156
\ \ A{\isacharcolon}{\isacharcolon}\ three\isanewline
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   157
\ {\isachardoublequote}A\ {\isasymequiv}\ Abs{\isacharunderscore}three\ {\isadigit{0}}{\isachardoublequote}\isanewline
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   158
\ \ B{\isacharcolon}{\isacharcolon}\ three\isanewline
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   159
\ {\isachardoublequote}B\ {\isasymequiv}\ Abs{\isacharunderscore}three\ {\isadigit{1}}{\isachardoublequote}\isanewline
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   160
\ \ C\ {\isacharcolon}{\isacharcolon}\ three\isanewline
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   161
\ {\isachardoublequote}C\ {\isasymequiv}\ Abs{\isacharunderscore}three\ {\isadigit{2}}{\isachardoublequote}\isamarkupfalse%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   162
%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   163
\begin{isamarkuptext}%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   164
So far, everything was easy. But it is clear that reasoning about \isa{three} will be hell if we have to go back to \isa{nat} every time. Thus our
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   165
aim must be to raise our level of abstraction by deriving enough theorems
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   166
about type \isa{three} to characterize it completely. And those theorems
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   167
should be phrased in terms of \isa{A}, \isa{B} and \isa{C}, not \isa{Abs{\isacharunderscore}three} and \isa{Rep{\isacharunderscore}three}. Because of the simplicity of the example,
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   168
we merely need to prove that \isa{A}, \isa{B} and \isa{C} are distinct
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   169
and that they exhaust the type.
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   170
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   171
In processing our \isacommand{typedef} declaration, 
12473
f41e477576b9 *** empty log message ***
nipkow
parents: 12334
diff changeset
   172
Isabelle proves several helpful lemmas. The first two
f41e477576b9 *** empty log message ***
nipkow
parents: 12334
diff changeset
   173
express injectivity of \isa{Rep{\isacharunderscore}three} and \isa{Abs{\isacharunderscore}three}:
11898
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   174
\begin{center}
12473
f41e477576b9 *** empty log message ***
nipkow
parents: 12334
diff changeset
   175
\begin{tabular}{@ {}r@ {\qquad}l@ {}}
f41e477576b9 *** empty log message ***
nipkow
parents: 12334
diff changeset
   176
\isa{{\isacharparenleft}Rep{\isacharunderscore}three\ x\ {\isacharequal}\ Rep{\isacharunderscore}three\ y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharequal}\ y{\isacharparenright}} & (\isa{Rep{\isacharunderscore}three{\isacharunderscore}inject}) \\
f41e477576b9 *** empty log message ***
nipkow
parents: 12334
diff changeset
   177
\begin{tabular}{@ {}l@ {}}
f41e477576b9 *** empty log message ***
nipkow
parents: 12334
diff changeset
   178
\isa{{\isasymlbrakk}x\ {\isasymin}\ three{\isacharsemicolon}\ y\ {\isasymin}\ three\ {\isasymrbrakk}} \\
f41e477576b9 *** empty log message ***
nipkow
parents: 12334
diff changeset
   179
\isa{{\isasymLongrightarrow}\ {\isacharparenleft}Abs{\isacharunderscore}three\ x\ {\isacharequal}\ Abs{\isacharunderscore}three\ y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharequal}\ y{\isacharparenright}}
f41e477576b9 *** empty log message ***
nipkow
parents: 12334
diff changeset
   180
\end{tabular} & (\isa{Abs{\isacharunderscore}three{\isacharunderscore}inject}) \\
f41e477576b9 *** empty log message ***
nipkow
parents: 12334
diff changeset
   181
\end{tabular}
11898
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   182
\end{center}
12473
f41e477576b9 *** empty log message ***
nipkow
parents: 12334
diff changeset
   183
The following ones allow to replace some \isa{x{\isacharcolon}{\isacharcolon}three} by
f41e477576b9 *** empty log message ***
nipkow
parents: 12334
diff changeset
   184
\isa{Abs{\isacharunderscore}three{\isacharparenleft}y{\isacharcolon}{\isacharcolon}nat{\isacharparenright}}, and conversely \isa{y} by \isa{Rep{\isacharunderscore}three\ x}:
11898
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   185
\begin{center}
12473
f41e477576b9 *** empty log message ***
nipkow
parents: 12334
diff changeset
   186
\begin{tabular}{@ {}r@ {\qquad}l@ {}}
f41e477576b9 *** empty log message ***
nipkow
parents: 12334
diff changeset
   187
\isa{{\isasymlbrakk}y\ {\isasymin}\ three{\isacharsemicolon}\ {\isasymAnd}x{\isachardot}\ y\ {\isacharequal}\ Rep{\isacharunderscore}three\ x\ {\isasymLongrightarrow}\ P{\isasymrbrakk}\ {\isasymLongrightarrow}\ P} & (\isa{Rep{\isacharunderscore}three{\isacharunderscore}cases}) \\
f41e477576b9 *** empty log message ***
nipkow
parents: 12334
diff changeset
   188
\isa{{\isacharparenleft}{\isasymAnd}y{\isachardot}\ {\isasymlbrakk}x\ {\isacharequal}\ Abs{\isacharunderscore}three\ y{\isacharsemicolon}\ y\ {\isasymin}\ three{\isasymrbrakk}\ {\isasymLongrightarrow}\ P{\isacharparenright}\ {\isasymLongrightarrow}\ P} & (\isa{Abs{\isacharunderscore}three{\isacharunderscore}cases}) \\
f41e477576b9 *** empty log message ***
nipkow
parents: 12334
diff changeset
   189
\isa{{\isasymlbrakk}y\ {\isasymin}\ three{\isacharsemicolon}\ {\isasymAnd}x{\isachardot}\ P\ {\isacharparenleft}Rep{\isacharunderscore}three\ x{\isacharparenright}{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ y} & (\isa{Rep{\isacharunderscore}three{\isacharunderscore}induct}) \\
f41e477576b9 *** empty log message ***
nipkow
parents: 12334
diff changeset
   190
\isa{{\isacharparenleft}{\isasymAnd}y{\isachardot}\ y\ {\isasymin}\ three\ {\isasymLongrightarrow}\ P\ {\isacharparenleft}Abs{\isacharunderscore}three\ y{\isacharparenright}{\isacharparenright}\ {\isasymLongrightarrow}\ P\ x} & (\isa{Abs{\isacharunderscore}three{\isacharunderscore}induct}) \\
f41e477576b9 *** empty log message ***
nipkow
parents: 12334
diff changeset
   191
\end{tabular}
11898
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   192
\end{center}
12473
f41e477576b9 *** empty log message ***
nipkow
parents: 12334
diff changeset
   193
These theorems are proved for any type definition, with \isa{three}
f41e477576b9 *** empty log message ***
nipkow
parents: 12334
diff changeset
   194
replaced by the name of the type in question.
f41e477576b9 *** empty log message ***
nipkow
parents: 12334
diff changeset
   195
11898
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   196
Distinctness of \isa{A}, \isa{B} and \isa{C} follows immediately
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   197
if we expand their definitions and rewrite with the injectivity
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   198
of \isa{Abs{\isacharunderscore}three}:%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   199
\end{isamarkuptext}%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   200
\isamarkuptrue%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   201
\isacommand{lemma}\ {\isachardoublequote}A\ {\isasymnoteq}\ B\ {\isasymand}\ B\ {\isasymnoteq}\ A\ {\isasymand}\ A\ {\isasymnoteq}\ C\ {\isasymand}\ C\ {\isasymnoteq}\ A\ {\isasymand}\ B\ {\isasymnoteq}\ C\ {\isasymand}\ C\ {\isasymnoteq}\ B{\isachardoublequote}\isanewline
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   202
\isamarkupfalse%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   203
\isacommand{by}{\isacharparenleft}simp\ add{\isacharcolon}\ Abs{\isacharunderscore}three{\isacharunderscore}inject\ A{\isacharunderscore}def\ B{\isacharunderscore}def\ C{\isacharunderscore}def\ three{\isacharunderscore}def{\isacharparenright}\isamarkupfalse%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   204
%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   205
\begin{isamarkuptext}%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   206
\noindent
12473
f41e477576b9 *** empty log message ***
nipkow
parents: 12334
diff changeset
   207
Of course we rely on the simplifier to solve goals like \isa{{\isadigit{0}}\ {\isasymnoteq}\ {\isadigit{1}}}.
11898
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   208
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   209
The fact that \isa{A}, \isa{B} and \isa{C} exhaust type \isa{three} is
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   210
best phrased as a case distinction theorem: if you want to prove \isa{P\ x}
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   211
(where \isa{x} is of type \isa{three}) it suffices to prove \isa{P\ A},
12473
f41e477576b9 *** empty log message ***
nipkow
parents: 12334
diff changeset
   212
\isa{P\ B} and \isa{P\ C}:%
11898
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   213
\end{isamarkuptext}%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   214
\isamarkuptrue%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   215
\isacommand{lemma}\ three{\isacharunderscore}cases{\isacharcolon}\ {\isachardoublequote}{\isasymlbrakk}\ P\ A{\isacharsemicolon}\ P\ B{\isacharsemicolon}\ P\ C\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ x{\isachardoublequote}\isamarkupfalse%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   216
%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   217
\begin{isamarkuptxt}%
12473
f41e477576b9 *** empty log message ***
nipkow
parents: 12334
diff changeset
   218
\noindent Again this follows easily from a pre-proved general theorem:%
11898
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   219
\end{isamarkuptxt}%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   220
\isamarkuptrue%
12815
wenzelm
parents: 12627
diff changeset
   221
\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ x\ rule{\isacharcolon}\ Abs{\isacharunderscore}three{\isacharunderscore}induct{\isacharparenright}\isamarkupfalse%
11898
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   222
%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   223
\begin{isamarkuptxt}%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   224
\begin{isabelle}%
12473
f41e477576b9 *** empty log message ***
nipkow
parents: 12334
diff changeset
   225
\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}y{\isachardot}\ {\isasymlbrakk}P\ A{\isacharsemicolon}\ P\ B{\isacharsemicolon}\ P\ C{\isacharsemicolon}\ y\ {\isasymin}\ three{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ {\isacharparenleft}Abs{\isacharunderscore}three\ y{\isacharparenright}%
11898
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   226
\end{isabelle}
12473
f41e477576b9 *** empty log message ***
nipkow
parents: 12334
diff changeset
   227
Simplification with \isa{three{\isacharunderscore}def} leads to the disjunction \isa{y\ {\isacharequal}\ {\isadigit{0}}\ {\isasymor}\ y\ {\isacharequal}\ {\isadigit{1}}\ {\isasymor}\ y\ {\isacharequal}\ {\isadigit{2}}} which \isa{auto} separates into three
f41e477576b9 *** empty log message ***
nipkow
parents: 12334
diff changeset
   228
subgoals, each of which is easily solved by simplification:%
11898
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   229
\end{isamarkuptxt}%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   230
\isamarkuptrue%
12473
f41e477576b9 *** empty log message ***
nipkow
parents: 12334
diff changeset
   231
\isacommand{apply}{\isacharparenleft}auto\ simp\ add{\isacharcolon}\ three{\isacharunderscore}def\ A{\isacharunderscore}def\ B{\isacharunderscore}def\ C{\isacharunderscore}def{\isacharparenright}\isanewline
11898
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   232
\isamarkupfalse%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   233
\isacommand{done}\isamarkupfalse%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   234
%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   235
\begin{isamarkuptext}%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   236
\noindent
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   237
This concludes the derivation of the characteristic theorems for
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   238
type \isa{three}.
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   239
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   240
The attentive reader has realized long ago that the
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   241
above lengthy definition can be collapsed into one line:%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   242
\end{isamarkuptext}%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   243
\isamarkuptrue%
12334
60bf75e157e4 *** empty log message ***
nipkow
parents: 12332
diff changeset
   244
\isacommand{datatype}\ better{\isacharunderscore}three\ {\isacharequal}\ A\ {\isacharbar}\ B\ {\isacharbar}\ C\isamarkupfalse%
11898
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   245
%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   246
\begin{isamarkuptext}%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   247
\noindent
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   248
In fact, the \isacommand{datatype} command performs internally more or less
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   249
the same derivations as we did, which gives you some idea what life would be
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   250
like without \isacommand{datatype}.
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   251
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   252
Although \isa{three} could be defined in one line, we have chosen this
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   253
example to demonstrate \isacommand{typedef} because its simplicity makes the
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   254
key concepts particularly easy to grasp. If you would like to see a
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   255
non-trivial example that cannot be defined more directly, we recommend the
12473
f41e477576b9 *** empty log message ***
nipkow
parents: 12334
diff changeset
   256
definition of \emph{finite multisets} in the Library~\cite{HOL-Library}.
11898
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   257
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   258
Let us conclude by summarizing the above procedure for defining a new type.
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   259
Given some abstract axiomatic description $P$ of a type $ty$ in terms of a
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   260
set of functions $F$, this involves three steps:
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   261
\begin{enumerate}
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   262
\item Find an appropriate type $\tau$ and subset $A$ which has the desired
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   263
  properties $P$, and make a type definition based on this representation.
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   264
\item Define the required functions $F$ on $ty$ by lifting
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   265
analogous functions on the representation via $Abs_ty$ and $Rep_ty$.
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   266
\item Prove that $P$ holds for $ty$ by lifting $P$ from the representation.
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   267
\end{enumerate}
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   268
You can now forget about the representation and work solely in terms of the
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   269
abstract functions $F$ and properties $P$.%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   270
\index{typedecl@\isacommand {typedef} (command)|)}%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   271
\index{types!defining|)}%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   272
\end{isamarkuptext}%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   273
\isamarkuptrue%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   274
\isamarkupfalse%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   275
\end{isabellebody}%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   276
%%% Local Variables:
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   277
%%% mode: latex
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   278
%%% TeX-master: "root"
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   279
%%% End: