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