doc-src/TutorialI/Types/Typedef.thy
author nipkow
Wed Dec 06 13:22:58 2000 +0100 (2000-12-06)
changeset 10608 620647438780
parent 10420 ef006735bee8
child 10654 458068404143
permissions -rw-r--r--
*** empty log message ***
nipkow@10366
     1
(*<*)theory Typedef = Main:(*>*)
nipkow@10366
     2
nipkow@10366
     3
section{*Introducing new types*}
nipkow@10366
     4
nipkow@10366
     5
text{*\label{sec:adv-typedef}
nipkow@10366
     6
By now we have seen a number of ways for introducing new types, for example
nipkow@10366
     7
type synonyms, recursive datatypes and records. For most applications, this
nipkow@10366
     8
repertoire should be quite sufficient. Very occasionally you may feel the
nipkow@10366
     9
need for a more advanced type. If you cannot avoid that type, and you are
nipkow@10366
    10
quite certain that it is not definable by any of the standard means,
nipkow@10366
    11
then read on.
nipkow@10366
    12
\begin{warn}
nipkow@10366
    13
  Types in HOL must be non-empty; otherwise the quantifier rules would be
nipkow@10420
    14
  unsound, because $\exists x.\ x=x$ is a theorem.
nipkow@10366
    15
\end{warn}
nipkow@10366
    16
*}
nipkow@10366
    17
nipkow@10366
    18
subsection{*Declaring new types*}
nipkow@10366
    19
nipkow@10366
    20
text{*\label{sec:typedecl}
nipkow@10366
    21
The most trivial way of introducing a new type is by a \bfindex{type
nipkow@10366
    22
declaration}: *}
nipkow@10366
    23
nipkow@10366
    24
typedecl my_new_type
nipkow@10366
    25
nipkow@10366
    26
text{*\noindent\indexbold{*typedecl}%
nipkow@10420
    27
This does not define @{typ my_new_type} at all but merely introduces its
nipkow@10420
    28
name. Thus we know nothing about this type, except that it is
nipkow@10366
    29
non-empty. Such declarations without definitions are
nipkow@10366
    30
useful only if that type can be viewed as a parameter of a theory and we do
nipkow@10366
    31
not intend to impose any restrictions on it. A typical example is given in
nipkow@10366
    32
\S\ref{sec:VMC}, where we define transition relations over an arbitrary type
nipkow@10366
    33
of states without any internal structure.
nipkow@10366
    34
nipkow@10366
    35
In principle we can always get rid of such type declarations by making those
nipkow@10366
    36
types parameters of every other type, thus keeping the theory generic. In
nipkow@10366
    37
practice, however, the resulting clutter can sometimes make types hard to
nipkow@10366
    38
read.
nipkow@10366
    39
nipkow@10366
    40
If you are looking for a quick and dirty way of introducing a new type
nipkow@10366
    41
together with its properties: declare the type and state its properties as
nipkow@10366
    42
axioms. Example:
nipkow@10366
    43
*}
nipkow@10366
    44
nipkow@10366
    45
axioms
nipkow@10420
    46
just_one: "\<exists>x::my_new_type. \<forall>y. x = y"
nipkow@10366
    47
nipkow@10366
    48
text{*\noindent
nipkow@10366
    49
However, we strongly discourage this approach, except at explorative stages
nipkow@10366
    50
of your development. It is extremely easy to write down contradictory sets of
nipkow@10366
    51
axioms, in which case you will be able to prove everything but it will mean
nipkow@10366
    52
nothing.  In the above case it also turns out that the axiomatic approach is
nipkow@10366
    53
unnecessary: a one-element type called @{typ unit} is already defined in HOL.
nipkow@10366
    54
*}
nipkow@10366
    55
nipkow@10366
    56
subsection{*Defining new types*}
nipkow@10366
    57
nipkow@10366
    58
text{*\label{sec:typedef}
nipkow@10366
    59
Now we come to the most general method of safely introducing a new type, the
nipkow@10366
    60
\bfindex{type definition}. All other methods, for example
nipkow@10366
    61
\isacommand{datatype}, are based on it. The principle is extremely simple:
nipkow@10366
    62
any non-empty subset of an existing type can be turned into a new type.  Thus
nipkow@10366
    63
a type definition is merely a notational device: you introduce a new name for
nipkow@10366
    64
a subset of an existing type. This does not add any logical power to HOL,
nipkow@10366
    65
because you could base all your work directly on the subset of the existing
nipkow@10366
    66
type. However, the resulting theories could easily become undigestible
nipkow@10366
    67
because instead of implicit types you would have explicit sets in your
nipkow@10366
    68
formulae.
nipkow@10366
    69
nipkow@10366
    70
Let us work a simple example, the definition of a three-element type.
nipkow@10366
    71
It is easily represented by the first three natural numbers:
nipkow@10366
    72
*}
nipkow@10366
    73
nipkow@10366
    74
typedef three = "{n. n \<le> 2}"
nipkow@10366
    75
nipkow@10366
    76
txt{*\noindent\indexbold{*typedef}%
nipkow@10366
    77
In order to enforce that the representing set on the right-hand side is
nipkow@10366
    78
non-empty, this definition actually starts a proof to that effect:
nipkow@10366
    79
@{subgoals[display,indent=0]}
nipkow@10366
    80
Fortunately, this is easy enough to show: take 0 as a witness.
nipkow@10366
    81
*}
nipkow@10366
    82
nipkow@10366
    83
apply(rule_tac x = 0 in exI);
nipkow@10366
    84
by simp
nipkow@10366
    85
nipkow@10366
    86
text{*
nipkow@10366
    87
This type definition introduces the new type @{typ three} and asserts
nipkow@10366
    88
that it is a \emph{copy} of the set @{term"{0,1,2}"}. This assertion
nipkow@10366
    89
is expressed via a bijection between the \emph{type} @{typ three} and the
nipkow@10366
    90
\emph{set} @{term"{0,1,2}"}. To this end, the command declares the following
nipkow@10366
    91
constants behind the scenes:
nipkow@10366
    92
\begin{center}
nipkow@10366
    93
\begin{tabular}{rcl}
nipkow@10366
    94
@{term three} &::& @{typ"nat set"} \\
nipkow@10366
    95
@{term Rep_three} &::& @{typ"three \<Rightarrow> nat"}\\
nipkow@10366
    96
@{term Abs_three} &::& @{typ"nat \<Rightarrow> three"}
nipkow@10366
    97
\end{tabular}
nipkow@10366
    98
\end{center}
nipkow@10366
    99
Constant @{term three} is just an abbreviation (@{thm[source]three_def}):
nipkow@10366
   100
@{thm[display]three_def}
nipkow@10366
   101
The situation is best summarized with the help of the following diagram,
nipkow@10366
   102
where squares are types and circles are sets:
nipkow@10366
   103
\begin{center}
nipkow@10366
   104
\unitlength1mm
nipkow@10366
   105
\thicklines
nipkow@10366
   106
\begin{picture}(100,40)
nipkow@10366
   107
\put(3,13){\framebox(15,15){@{typ three}}}
nipkow@10366
   108
\put(55,5){\framebox(30,30){@{term three}}}
nipkow@10366
   109
\put(70,32){\makebox(0,0){@{typ nat}}}
nipkow@10366
   110
\put(70,20){\circle{40}}
nipkow@10366
   111
\put(10,15){\vector(1,0){60}}
nipkow@10366
   112
\put(25,14){\makebox(0,0)[tl]{@{term Rep_three}}}
nipkow@10366
   113
\put(70,25){\vector(-1,0){60}}
nipkow@10366
   114
\put(25,26){\makebox(0,0)[bl]{@{term Abs_three}}}
nipkow@10366
   115
\end{picture}
nipkow@10366
   116
\end{center}
nipkow@10366
   117
Finally, \isacommand{typedef} asserts that @{term Rep_three} is
nipkow@10366
   118
surjective on the subset @{term three} and @{term Abs_three} and @{term
nipkow@10366
   119
Rep_three} are inverses of each other:
nipkow@10366
   120
\begin{center}
nipkow@10366
   121
\begin{tabular}{rl}
nipkow@10366
   122
@{thm Rep_three[no_vars]} &~~ (@{thm[source]Rep_three}) \\
nipkow@10366
   123
@{thm Rep_three_inverse[no_vars]} &~~ (@{thm[source]Rep_three_inverse}) \\
nipkow@10366
   124
@{thm Abs_three_inverse[no_vars]} &~~ (@{thm[source]Abs_three_inverse})
nipkow@10366
   125
\end{tabular}
nipkow@10366
   126
\end{center}
nipkow@10366
   127
nipkow@10366
   128
From the above example it should be clear what \isacommand{typedef} does
nipkow@10366
   129
in general: simply replace the name @{text three} and the set
nipkow@10366
   130
@{term"{n. n\<le>2}"} by the respective arguments.
nipkow@10366
   131
nipkow@10366
   132
Our next step is to define the basic functions expected on the new type.
nipkow@10366
   133
Although this depends on the type at hand, the following strategy works well:
nipkow@10366
   134
\begin{itemize}
nipkow@10366
   135
\item define a small kernel of basic functions such that all further
nipkow@10366
   136
functions you anticipate can be defined on top of that kernel.
nipkow@10366
   137
\item define the kernel in terms of corresponding functions on the
nipkow@10366
   138
representing type using @{term Abs} and @{term Rep} to convert between the
nipkow@10366
   139
two levels.
nipkow@10366
   140
\end{itemize}
nipkow@10366
   141
In our example it suffices to give the three elements of type @{typ three}
nipkow@10366
   142
names:
nipkow@10366
   143
*}
nipkow@10366
   144
nipkow@10366
   145
constdefs
nipkow@10366
   146
  A:: three
nipkow@10366
   147
 "A \<equiv> Abs_three 0"
nipkow@10366
   148
  B:: three
nipkow@10366
   149
 "B \<equiv> Abs_three 1"
nipkow@10366
   150
  C :: three
nipkow@10366
   151
 "C \<equiv> Abs_three 2";
nipkow@10366
   152
nipkow@10366
   153
text{*
nipkow@10366
   154
So far, everything was easy. But it is clear that reasoning about @{typ
nipkow@10366
   155
three} will be hell if we have to go back to @{typ nat} every time. Thus our
nipkow@10366
   156
aim must be to raise our level of abstraction by deriving enough theorems
nipkow@10366
   157
about type @{typ three} to characterize it completely. And those theorems
nipkow@10366
   158
should be phrased in terms of @{term A}, @{term B} and @{term C}, not @{term
nipkow@10366
   159
Abs_three} and @{term Rep_three}. Because of the simplicity of the example,
nipkow@10366
   160
we merely need to prove that @{term A}, @{term B} and @{term C} are distinct
nipkow@10366
   161
and that they exhaust the type.
nipkow@10366
   162
nipkow@10366
   163
We start with a helpful version of injectivity of @{term Abs_three} on the
nipkow@10366
   164
representing subset:
nipkow@10366
   165
*}
nipkow@10366
   166
nipkow@10366
   167
lemma [simp]:
nipkow@10366
   168
 "\<lbrakk> x \<in> three; y \<in> three \<rbrakk> \<Longrightarrow> (Abs_three x = Abs_three y) = (x=y)";
nipkow@10366
   169
nipkow@10366
   170
txt{*\noindent
nipkow@10366
   171
We prove both directions separately. From @{prop"Abs_three x = Abs_three y"}
nipkow@10366
   172
we derive @{prop"Rep_three(Abs_three x) = Rep_three(Abs_three y)"} (via
nipkow@10366
   173
@{thm[source]arg_cong}: @{thm arg_cong}), and thus the required @{prop"x =
nipkow@10366
   174
y"} by simplification with @{thm[source]Abs_three_inverse}. The other direction
nipkow@10366
   175
is trivial by simplification:
nipkow@10366
   176
*}
nipkow@10366
   177
nipkow@10366
   178
apply(rule iffI);
nipkow@10366
   179
 apply(drule_tac f = Rep_three in arg_cong);
nipkow@10366
   180
 apply(simp add:Abs_three_inverse);
nipkow@10366
   181
by simp;
nipkow@10366
   182
nipkow@10366
   183
text{*\noindent
nipkow@10366
   184
Analogous lemmas can be proved in the same way for arbitrary type definitions.
nipkow@10366
   185
nipkow@10366
   186
Distinctness of @{term A}, @{term B} and @{term C} follows immediately
nipkow@10366
   187
if we expand their definitions and rewrite with the above simplification rule:
nipkow@10366
   188
*}
nipkow@10366
   189
nipkow@10366
   190
lemma "A \<noteq> B \<and> B \<noteq> A \<and> A \<noteq> C \<and> C \<noteq> A \<and> B \<noteq> C \<and> C \<noteq> B";
nipkow@10366
   191
by(simp add:A_def B_def C_def three_def);
nipkow@10366
   192
nipkow@10366
   193
text{*\noindent
nipkow@10366
   194
Of course we rely on the simplifier to solve goals like @{prop"0 \<noteq> 1"}.
nipkow@10366
   195
nipkow@10366
   196
The fact that @{term A}, @{term B} and @{term C} exhaust type @{typ three} is
nipkow@10366
   197
best phrased as a case distinction theorem: if you want to prove @{prop"P x"}
nipkow@10366
   198
(where @{term x} is of type @{typ three}) it suffices to prove @{prop"P A"},
nipkow@10366
   199
@{prop"P B"} and @{prop"P C"}. First we prove the analogous proposition for the
nipkow@10366
   200
representation: *}
nipkow@10366
   201
nipkow@10366
   202
lemma cases_lemma: "\<lbrakk> Q 0; Q 1; Q 2; n : three \<rbrakk> \<Longrightarrow>  Q(n::nat)";
nipkow@10366
   203
nipkow@10366
   204
txt{*\noindent
nipkow@10366
   205
Expanding @{thm[source]three_def} yields the premise @{prop"n\<le>2"}. Repeated
nipkow@10366
   206
elimination with @{thm[source]le_SucE}
nipkow@10366
   207
@{thm[display]le_SucE}
nipkow@10366
   208
reduces @{prop"n\<le>2"} to the three cases @{prop"n\<le>0"}, @{prop"n=1"} and
nipkow@10366
   209
@{prop"n=2"} which are trivial for simplification:
nipkow@10366
   210
*}
nipkow@10366
   211
nipkow@10366
   212
apply(simp add:three_def);
nipkow@10366
   213
apply((erule le_SucE)+);
nipkow@10366
   214
apply simp_all;
nipkow@10366
   215
done
nipkow@10366
   216
nipkow@10366
   217
text{*
nipkow@10366
   218
Now the case distinction lemma on type @{typ three} is easy to derive if you know how to:
nipkow@10366
   219
*}
nipkow@10366
   220
nipkow@10366
   221
lemma three_cases: "\<lbrakk> P A; P B; P C \<rbrakk> \<Longrightarrow> P x";
nipkow@10366
   222
nipkow@10366
   223
txt{*\noindent
nipkow@10366
   224
We start by replacing the @{term x} by @{term"Abs_three(Rep_three x)"}:
nipkow@10366
   225
*}
nipkow@10366
   226
nipkow@10366
   227
apply(rule subst[OF Rep_three_inverse]);
nipkow@10366
   228
nipkow@10366
   229
txt{*\noindent
nipkow@10366
   230
This substitution step worked nicely because there was just a single
nipkow@10366
   231
occurrence of a term of type @{typ three}, namely @{term x}.
nipkow@10366
   232
When we now apply the above lemma, @{term Q} becomes @{term"\<lambda>n. P(Abs_three
nipkow@10366
   233
n)"} because @{term"Rep_three x"} is the only term of type @{typ nat}:
nipkow@10366
   234
*}
nipkow@10366
   235
nipkow@10366
   236
apply(rule cases_lemma);
nipkow@10366
   237
nipkow@10366
   238
txt{*
nipkow@10366
   239
@{subgoals[display,indent=0]}
nipkow@10366
   240
The resulting subgoals are easily solved by simplification:
nipkow@10366
   241
*}
nipkow@10366
   242
nipkow@10366
   243
apply(simp_all add:A_def B_def C_def Rep_three);
nipkow@10366
   244
done
nipkow@10366
   245
nipkow@10366
   246
text{*\noindent
nipkow@10366
   247
This concludes the derivation of the characteristic theorems for
nipkow@10366
   248
type @{typ three}.
nipkow@10366
   249
nipkow@10366
   250
The attentive reader has realized long ago that the
nipkow@10366
   251
above lengthy definition can be collapsed into one line:
nipkow@10366
   252
*}
nipkow@10366
   253
nipkow@10366
   254
datatype three' = A | B | C;
nipkow@10366
   255
nipkow@10366
   256
text{*\noindent
nipkow@10366
   257
In fact, the \isacommand{datatype} command performs internally more or less
nipkow@10366
   258
the same derivations as we did, which gives you some idea what life would be
nipkow@10366
   259
like without \isacommand{datatype}.
nipkow@10366
   260
nipkow@10366
   261
Although @{typ three} could be defined in one line, we have chosen this
nipkow@10366
   262
example to demonstrate \isacommand{typedef} because its simplicity makes the
nipkow@10366
   263
key concepts particularly easy to grasp. If you would like to see a
nipkow@10366
   264
nontrivial example that cannot be defined more directly, we recommend the
nipkow@10366
   265
definition of \emph{finite multisets} in the HOL library.
nipkow@10366
   266
nipkow@10366
   267
Let us conclude by summarizing the above procedure for defining a new type.
nipkow@10366
   268
Given some abstract axiomatic description $P$ of a type $ty$ in terms of a
nipkow@10366
   269
set of functions $F$, this involves three steps:
nipkow@10366
   270
\begin{enumerate}
nipkow@10366
   271
\item Find an appropriate type $\tau$ and subset $A$ which has the desired
nipkow@10366
   272
  properties $P$, and make a type definition based on this representation.
nipkow@10366
   273
\item Define the required functions $F$ on $ty$ by lifting
nipkow@10366
   274
analogous functions on the representation via $Abs_ty$ and $Rep_ty$.
nipkow@10366
   275
\item Prove that $P$ holds for $ty$ by lifting $P$ from the representation.
nipkow@10366
   276
\end{enumerate}
nipkow@10366
   277
You can now forget about the representation and work solely in terms of the
nipkow@10366
   278
abstract functions $F$ and properties $P$.
nipkow@10366
   279
*}
nipkow@10366
   280
nipkow@10366
   281
(*<*)end(*>*)