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: "\x::my_new_type. \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 \ 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 \ nat"}\\  nipkow@10366  96 @{term Abs_three} &::& @{typ"nat \ 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\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 \ Abs_three 0"  nipkow@10366  148  B:: three  nipkow@10366  149  "B \ Abs_three 1"  nipkow@10366  150  C :: three  nipkow@10366  151  "C \ 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  "\ x \ three; y \ three \ \ (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 \ B \ B \ A \ A \ C \ C \ A \ B \ C \ C \ 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 \ 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: "\ Q 0; Q 1; Q 2; n : three \ \ Q(n::nat)";  nipkow@10366  203 nipkow@10366  204 txt{*\noindent  nipkow@10366  205 Expanding @{thm[source]three_def} yields the premise @{prop"n\2"}. Repeated  nipkow@10366  206 elimination with @{thm[source]le_SucE}  nipkow@10366  207 @{thm[display]le_SucE}  nipkow@10366  208 reduces @{prop"n\2"} to the three cases @{prop"n\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: "\ P A; P B; P C \ \ 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"\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(*>*)