1.1 --- a/doc-src/TutorialI/Types/document/Typedefs.tex Thu Jul 26 16:08:16 2012 +0200
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,340 +0,0 @@
1.4 -%
1.5 -\begin{isabellebody}%
1.6 -\def\isabellecontext{Typedefs}%
1.7 -%
1.8 -\isadelimtheory
1.9 -%
1.10 -\endisadelimtheory
1.11 -%
1.12 -\isatagtheory
1.13 -%
1.14 -\endisatagtheory
1.15 -{\isafoldtheory}%
1.16 -%
1.17 -\isadelimtheory
1.18 -%
1.19 -\endisadelimtheory
1.20 -%
1.21 -\isamarkupsection{Introducing New Types%
1.22 -}
1.23 -\isamarkuptrue%
1.24 -%
1.25 -\begin{isamarkuptext}%
1.26 -\label{sec:adv-typedef}
1.27 -For most applications, a combination of predefined types like \isa{bool} and
1.28 -\isa{{\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}} with recursive datatypes and records is quite sufficient. Very
1.29 -occasionally you may feel the need for a more advanced type. If you
1.30 -are certain that your type is not definable by any of the
1.31 -standard means, then read on.
1.32 -\begin{warn}
1.33 - Types in HOL must be non-empty; otherwise the quantifier rules would be
1.34 - unsound, because $\exists x.\ x=x$ is a theorem.
1.35 -\end{warn}%
1.36 -\end{isamarkuptext}%
1.37 -\isamarkuptrue%
1.38 -%
1.39 -\isamarkupsubsection{Declaring New Types%
1.40 -}
1.41 -\isamarkuptrue%
1.42 -%
1.43 -\begin{isamarkuptext}%
1.44 -\label{sec:typedecl}
1.45 -\index{types!declaring|(}%
1.46 -\index{typedecl@\isacommand {typedecl} (command)}%
1.47 -The most trivial way of introducing a new type is by a \textbf{type
1.48 -declaration}:%
1.49 -\end{isamarkuptext}%
1.50 -\isamarkuptrue%
1.51 -\isacommand{typedecl}\isamarkupfalse%
1.52 -\ my{\isaliteral{5F}{\isacharunderscore}}new{\isaliteral{5F}{\isacharunderscore}}type%
1.53 -\begin{isamarkuptext}%
1.54 -\noindent
1.55 -This does not define \isa{my{\isaliteral{5F}{\isacharunderscore}}new{\isaliteral{5F}{\isacharunderscore}}type} at all but merely introduces its
1.56 -name. Thus we know nothing about this type, except that it is
1.57 -non-empty. Such declarations without definitions are
1.58 -useful if that type can be viewed as a parameter of the theory.
1.59 -A typical example is given in \S\ref{sec:VMC}, where we define a transition
1.60 -relation over an arbitrary type of states.
1.61 -
1.62 -In principle we can always get rid of such type declarations by making those
1.63 -types parameters of every other type, thus keeping the theory generic. In
1.64 -practice, however, the resulting clutter can make types hard to read.
1.65 -
1.66 -If you are looking for a quick and dirty way of introducing a new type
1.67 -together with its properties: declare the type and state its properties as
1.68 -axioms. Example:%
1.69 -\end{isamarkuptext}%
1.70 -\isamarkuptrue%
1.71 -\isacommand{axioms}\isamarkupfalse%
1.72 -\isanewline
1.73 -just{\isaliteral{5F}{\isacharunderscore}}one{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}x{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}my{\isaliteral{5F}{\isacharunderscore}}new{\isaliteral{5F}{\isacharunderscore}}type{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}y{\isaliteral{2E}{\isachardot}}\ x\ {\isaliteral{3D}{\isacharequal}}\ y{\isaliteral{22}{\isachardoublequoteclose}}%
1.74 -\begin{isamarkuptext}%
1.75 -\noindent
1.76 -However, we strongly discourage this approach, except at explorative stages
1.77 -of your development. It is extremely easy to write down contradictory sets of
1.78 -axioms, in which case you will be able to prove everything but it will mean
1.79 -nothing. In the example above, the axiomatic approach is
1.80 -unnecessary: a one-element type called \isa{unit} is already defined in HOL.
1.81 -\index{types!declaring|)}%
1.82 -\end{isamarkuptext}%
1.83 -\isamarkuptrue%
1.84 -%
1.85 -\isamarkupsubsection{Defining New Types%
1.86 -}
1.87 -\isamarkuptrue%
1.88 -%
1.89 -\begin{isamarkuptext}%
1.90 -\label{sec:typedef}
1.91 -\index{types!defining|(}%
1.92 -\index{typedecl@\isacommand {typedef} (command)|(}%
1.93 -Now we come to the most general means of safely introducing a new type, the
1.94 -\textbf{type definition}. All other means, for example
1.95 -\isacommand{datatype}, are based on it. The principle is extremely simple:
1.96 -any non-empty subset of an existing type can be turned into a new type.
1.97 -More precisely, the new type is specified to be isomorphic to some
1.98 -non-empty subset of an existing type.
1.99 -
1.100 -Let us work a simple example, the definition of a three-element type.
1.101 -It is easily represented by the first three natural numbers:%
1.102 -\end{isamarkuptext}%
1.103 -\isamarkuptrue%
1.104 -\isacommand{typedef}\isamarkupfalse%
1.105 -\ three\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{7B}{\isacharbraceleft}}{\isadigit{0}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}nat{\isaliteral{2C}{\isacharcomma}}\ {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isadigit{2}}{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequoteclose}}%
1.106 -\isadelimproof
1.107 -%
1.108 -\endisadelimproof
1.109 -%
1.110 -\isatagproof
1.111 -%
1.112 -\begin{isamarkuptxt}%
1.113 -\noindent
1.114 -In order to enforce that the representing set on the right-hand side is
1.115 -non-empty, this definition actually starts a proof to that effect:
1.116 -\begin{isabelle}%
1.117 -\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C6578697374733E}{\isasymexists}}x{\isaliteral{2E}{\isachardot}}\ x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ {\isaliteral{7B}{\isacharbraceleft}}{\isadigit{0}}{\isaliteral{2C}{\isacharcomma}}\ {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isadigit{2}}{\isaliteral{7D}{\isacharbraceright}}%
1.118 -\end{isabelle}
1.119 -Fortunately, this is easy enough to show, even \isa{auto} could do it.
1.120 -In general, one has to provide a witness, in our case 0:%
1.121 -\end{isamarkuptxt}%
1.122 -\isamarkuptrue%
1.123 -\isacommand{apply}\isamarkupfalse%
1.124 -{\isaliteral{28}{\isacharparenleft}}rule{\isaliteral{5F}{\isacharunderscore}}tac\ x\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}\ \isakeyword{in}\ exI{\isaliteral{29}{\isacharparenright}}\isanewline
1.125 -\isacommand{by}\isamarkupfalse%
1.126 -\ simp%
1.127 -\endisatagproof
1.128 -{\isafoldproof}%
1.129 -%
1.130 -\isadelimproof
1.131 -%
1.132 -\endisadelimproof
1.133 -%
1.134 -\begin{isamarkuptext}%
1.135 -This type definition introduces the new type \isa{three} and asserts
1.136 -that it is a copy of the set \isa{{\isaliteral{7B}{\isacharbraceleft}}{\isadigit{0}}{\isaliteral{2C}{\isacharcomma}}\ {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isadigit{2}}{\isaliteral{7D}{\isacharbraceright}}}. This assertion
1.137 -is expressed via a bijection between the \emph{type} \isa{three} and the
1.138 -\emph{set} \isa{{\isaliteral{7B}{\isacharbraceleft}}{\isadigit{0}}{\isaliteral{2C}{\isacharcomma}}\ {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isadigit{2}}{\isaliteral{7D}{\isacharbraceright}}}. To this end, the command declares the following
1.139 -constants behind the scenes:
1.140 -\begin{center}
1.141 -\begin{tabular}{rcl}
1.142 -\isa{three} &::& \isa{nat\ set} \\
1.143 -\isa{Rep{\isaliteral{5F}{\isacharunderscore}}three} &::& \isa{three\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat}\\
1.144 -\isa{Abs{\isaliteral{5F}{\isacharunderscore}}three} &::& \isa{nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ three}
1.145 -\end{tabular}
1.146 -\end{center}
1.147 -where constant \isa{three} is explicitly defined as the representing set:
1.148 -\begin{center}
1.149 -\isa{three\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ {\isaliteral{7B}{\isacharbraceleft}}{\isadigit{0}}{\isaliteral{2C}{\isacharcomma}}\ {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isadigit{2}}{\isaliteral{7D}{\isacharbraceright}}}\hfill(\isa{three{\isaliteral{5F}{\isacharunderscore}}def})
1.150 -\end{center}
1.151 -The situation is best summarized with the help of the following diagram,
1.152 -where squares denote types and the irregular region denotes a set:
1.153 -\begin{center}
1.154 -\includegraphics[scale=.8]{typedef}
1.155 -\end{center}
1.156 -Finally, \isacommand{typedef} asserts that \isa{Rep{\isaliteral{5F}{\isacharunderscore}}three} is
1.157 -surjective on the subset \isa{three} and \isa{Abs{\isaliteral{5F}{\isacharunderscore}}three} and \isa{Rep{\isaliteral{5F}{\isacharunderscore}}three} are inverses of each other:
1.158 -\begin{center}
1.159 -\begin{tabular}{@ {}r@ {\qquad\qquad}l@ {}}
1.160 -\isa{Rep{\isaliteral{5F}{\isacharunderscore}}three\ x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ three} & (\isa{Rep{\isaliteral{5F}{\isacharunderscore}}three}) \\
1.161 -\isa{Abs{\isaliteral{5F}{\isacharunderscore}}three\ {\isaliteral{28}{\isacharparenleft}}Rep{\isaliteral{5F}{\isacharunderscore}}three\ x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ x} & (\isa{Rep{\isaliteral{5F}{\isacharunderscore}}three{\isaliteral{5F}{\isacharunderscore}}inverse}) \\
1.162 -\isa{y\ {\isaliteral{5C3C696E3E}{\isasymin}}\ three\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ Rep{\isaliteral{5F}{\isacharunderscore}}three\ {\isaliteral{28}{\isacharparenleft}}Abs{\isaliteral{5F}{\isacharunderscore}}three\ y{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ y} & (\isa{Abs{\isaliteral{5F}{\isacharunderscore}}three{\isaliteral{5F}{\isacharunderscore}}inverse})
1.163 -\end{tabular}
1.164 -\end{center}
1.165 -%
1.166 -From this example it should be clear what \isacommand{typedef} does
1.167 -in general given a name (here \isa{three}) and a set
1.168 -(here \isa{{\isaliteral{7B}{\isacharbraceleft}}{\isadigit{0}}{\isaliteral{2C}{\isacharcomma}}\ {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isadigit{2}}{\isaliteral{7D}{\isacharbraceright}}}).
1.169 -
1.170 -Our next step is to define the basic functions expected on the new type.
1.171 -Although this depends on the type at hand, the following strategy works well:
1.172 -\begin{itemize}
1.173 -\item define a small kernel of basic functions that can express all other
1.174 -functions you anticipate.
1.175 -\item define the kernel in terms of corresponding functions on the
1.176 -representing type using \isa{Abs} and \isa{Rep} to convert between the
1.177 -two levels.
1.178 -\end{itemize}
1.179 -In our example it suffices to give the three elements of type \isa{three}
1.180 -names:%
1.181 -\end{isamarkuptext}%
1.182 -\isamarkuptrue%
1.183 -\isacommand{definition}\isamarkupfalse%
1.184 -\ A\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ three\ \isakeyword{where}\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ Abs{\isaliteral{5F}{\isacharunderscore}}three\ {\isadigit{0}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
1.185 -\isacommand{definition}\isamarkupfalse%
1.186 -\ B\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ three\ \isakeyword{where}\ {\isaliteral{22}{\isachardoublequoteopen}}B\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ Abs{\isaliteral{5F}{\isacharunderscore}}three\ {\isadigit{1}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
1.187 -\isacommand{definition}\isamarkupfalse%
1.188 -\ C\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ three\ \isakeyword{where}\ {\isaliteral{22}{\isachardoublequoteopen}}C\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ Abs{\isaliteral{5F}{\isacharunderscore}}three\ {\isadigit{2}}{\isaliteral{22}{\isachardoublequoteclose}}%
1.189 -\begin{isamarkuptext}%
1.190 -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
1.191 -aim must be to raise our level of abstraction by deriving enough theorems
1.192 -about type \isa{three} to characterize it completely. And those theorems
1.193 -should be phrased in terms of \isa{A}, \isa{B} and \isa{C}, not \isa{Abs{\isaliteral{5F}{\isacharunderscore}}three} and \isa{Rep{\isaliteral{5F}{\isacharunderscore}}three}. Because of the simplicity of the example,
1.194 -we merely need to prove that \isa{A}, \isa{B} and \isa{C} are distinct
1.195 -and that they exhaust the type.
1.196 -
1.197 -In processing our \isacommand{typedef} declaration,
1.198 -Isabelle proves several helpful lemmas. The first two
1.199 -express injectivity of \isa{Rep{\isaliteral{5F}{\isacharunderscore}}three} and \isa{Abs{\isaliteral{5F}{\isacharunderscore}}three}:
1.200 -\begin{center}
1.201 -\begin{tabular}{@ {}r@ {\qquad}l@ {}}
1.202 -\isa{{\isaliteral{28}{\isacharparenleft}}Rep{\isaliteral{5F}{\isacharunderscore}}three\ x\ {\isaliteral{3D}{\isacharequal}}\ Rep{\isaliteral{5F}{\isacharunderscore}}three\ y{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{3D}{\isacharequal}}\ y{\isaliteral{29}{\isacharparenright}}} & (\isa{Rep{\isaliteral{5F}{\isacharunderscore}}three{\isaliteral{5F}{\isacharunderscore}}inject}) \\
1.203 -\begin{tabular}{@ {}l@ {}}
1.204 -\isa{{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ three{\isaliteral{3B}{\isacharsemicolon}}\ y\ {\isaliteral{5C3C696E3E}{\isasymin}}\ three\ {\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}} \\
1.205 -\isa{{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}Abs{\isaliteral{5F}{\isacharunderscore}}three\ x\ {\isaliteral{3D}{\isacharequal}}\ Abs{\isaliteral{5F}{\isacharunderscore}}three\ y{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{3D}{\isacharequal}}\ y{\isaliteral{29}{\isacharparenright}}}
1.206 -\end{tabular} & (\isa{Abs{\isaliteral{5F}{\isacharunderscore}}three{\isaliteral{5F}{\isacharunderscore}}inject}) \\
1.207 -\end{tabular}
1.208 -\end{center}
1.209 -The following ones allow to replace some \isa{x{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}three} by
1.210 -\isa{Abs{\isaliteral{5F}{\isacharunderscore}}three{\isaliteral{28}{\isacharparenleft}}y{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}nat{\isaliteral{29}{\isacharparenright}}}, and conversely \isa{y} by \isa{Rep{\isaliteral{5F}{\isacharunderscore}}three\ x}:
1.211 -\begin{center}
1.212 -\begin{tabular}{@ {}r@ {\qquad}l@ {}}
1.213 -\isa{{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}y\ {\isaliteral{5C3C696E3E}{\isasymin}}\ three{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ y\ {\isaliteral{3D}{\isacharequal}}\ Rep{\isaliteral{5F}{\isacharunderscore}}three\ x\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P} & (\isa{Rep{\isaliteral{5F}{\isacharunderscore}}three{\isaliteral{5F}{\isacharunderscore}}cases}) \\
1.214 -\isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C416E643E}{\isasymAnd}}y{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}x\ {\isaliteral{3D}{\isacharequal}}\ Abs{\isaliteral{5F}{\isacharunderscore}}three\ y{\isaliteral{3B}{\isacharsemicolon}}\ y\ {\isaliteral{5C3C696E3E}{\isasymin}}\ three{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P} & (\isa{Abs{\isaliteral{5F}{\isacharunderscore}}three{\isaliteral{5F}{\isacharunderscore}}cases}) \\
1.215 -\isa{{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}y\ {\isaliteral{5C3C696E3E}{\isasymin}}\ three{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ P\ {\isaliteral{28}{\isacharparenleft}}Rep{\isaliteral{5F}{\isacharunderscore}}three\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ y} & (\isa{Rep{\isaliteral{5F}{\isacharunderscore}}three{\isaliteral{5F}{\isacharunderscore}}induct}) \\
1.216 -\isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C416E643E}{\isasymAnd}}y{\isaliteral{2E}{\isachardot}}\ y\ {\isaliteral{5C3C696E3E}{\isasymin}}\ three\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ {\isaliteral{28}{\isacharparenleft}}Abs{\isaliteral{5F}{\isacharunderscore}}three\ y{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ x} & (\isa{Abs{\isaliteral{5F}{\isacharunderscore}}three{\isaliteral{5F}{\isacharunderscore}}induct}) \\
1.217 -\end{tabular}
1.218 -\end{center}
1.219 -These theorems are proved for any type definition, with \isa{three}
1.220 -replaced by the name of the type in question.
1.221 -
1.222 -Distinctness of \isa{A}, \isa{B} and \isa{C} follows immediately
1.223 -if we expand their definitions and rewrite with the injectivity
1.224 -of \isa{Abs{\isaliteral{5F}{\isacharunderscore}}three}:%
1.225 -\end{isamarkuptext}%
1.226 -\isamarkuptrue%
1.227 -\isacommand{lemma}\isamarkupfalse%
1.228 -\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ B\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ A\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ C\ {\isaliteral{5C3C616E643E}{\isasymand}}\ C\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ C\ {\isaliteral{5C3C616E643E}{\isasymand}}\ C\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
1.229 -%
1.230 -\isadelimproof
1.231 -%
1.232 -\endisadelimproof
1.233 -%
1.234 -\isatagproof
1.235 -\isacommand{by}\isamarkupfalse%
1.236 -{\isaliteral{28}{\isacharparenleft}}simp\ add{\isaliteral{3A}{\isacharcolon}}\ Abs{\isaliteral{5F}{\isacharunderscore}}three{\isaliteral{5F}{\isacharunderscore}}inject\ A{\isaliteral{5F}{\isacharunderscore}}def\ B{\isaliteral{5F}{\isacharunderscore}}def\ C{\isaliteral{5F}{\isacharunderscore}}def\ three{\isaliteral{5F}{\isacharunderscore}}def{\isaliteral{29}{\isacharparenright}}%
1.237 -\endisatagproof
1.238 -{\isafoldproof}%
1.239 -%
1.240 -\isadelimproof
1.241 -%
1.242 -\endisadelimproof
1.243 -%
1.244 -\begin{isamarkuptext}%
1.245 -\noindent
1.246 -Of course we rely on the simplifier to solve goals like \isa{{\isadigit{0}}\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ {\isadigit{1}}}.
1.247 -
1.248 -The fact that \isa{A}, \isa{B} and \isa{C} exhaust type \isa{three} is
1.249 -best phrased as a case distinction theorem: if you want to prove \isa{P\ x}
1.250 -(where \isa{x} is of type \isa{three}) it suffices to prove \isa{P\ A},
1.251 -\isa{P\ B} and \isa{P\ C}:%
1.252 -\end{isamarkuptext}%
1.253 -\isamarkuptrue%
1.254 -\isacommand{lemma}\isamarkupfalse%
1.255 -\ three{\isaliteral{5F}{\isacharunderscore}}cases{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}\ P\ A{\isaliteral{3B}{\isacharsemicolon}}\ P\ B{\isaliteral{3B}{\isacharsemicolon}}\ P\ C\ {\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ x{\isaliteral{22}{\isachardoublequoteclose}}%
1.256 -\isadelimproof
1.257 -%
1.258 -\endisadelimproof
1.259 -%
1.260 -\isatagproof
1.261 -%
1.262 -\begin{isamarkuptxt}%
1.263 -\noindent Again this follows easily using the induction principle stemming from the type definition:%
1.264 -\end{isamarkuptxt}%
1.265 -\isamarkuptrue%
1.266 -\isacommand{apply}\isamarkupfalse%
1.267 -{\isaliteral{28}{\isacharparenleft}}induct{\isaliteral{5F}{\isacharunderscore}}tac\ x{\isaliteral{29}{\isacharparenright}}%
1.268 -\begin{isamarkuptxt}%
1.269 -\begin{isabelle}%
1.270 -\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}y{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}P\ A{\isaliteral{3B}{\isacharsemicolon}}\ P\ B{\isaliteral{3B}{\isacharsemicolon}}\ P\ C{\isaliteral{3B}{\isacharsemicolon}}\ y\ {\isaliteral{5C3C696E3E}{\isasymin}}\ three{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ {\isaliteral{28}{\isacharparenleft}}Abs{\isaliteral{5F}{\isacharunderscore}}three\ y{\isaliteral{29}{\isacharparenright}}%
1.271 -\end{isabelle}
1.272 -Simplification with \isa{three{\isaliteral{5F}{\isacharunderscore}}def} leads to the disjunction \isa{y\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}\ {\isaliteral{5C3C6F723E}{\isasymor}}\ y\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{1}}\ {\isaliteral{5C3C6F723E}{\isasymor}}\ y\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{2}}} which \isa{auto} separates into three
1.273 -subgoals, each of which is easily solved by simplification:%
1.274 -\end{isamarkuptxt}%
1.275 -\isamarkuptrue%
1.276 -\isacommand{apply}\isamarkupfalse%
1.277 -{\isaliteral{28}{\isacharparenleft}}auto\ simp\ add{\isaliteral{3A}{\isacharcolon}}\ three{\isaliteral{5F}{\isacharunderscore}}def\ A{\isaliteral{5F}{\isacharunderscore}}def\ B{\isaliteral{5F}{\isacharunderscore}}def\ C{\isaliteral{5F}{\isacharunderscore}}def{\isaliteral{29}{\isacharparenright}}\isanewline
1.278 -\isacommand{done}\isamarkupfalse%
1.279 -%
1.280 -\endisatagproof
1.281 -{\isafoldproof}%
1.282 -%
1.283 -\isadelimproof
1.284 -%
1.285 -\endisadelimproof
1.286 -%
1.287 -\begin{isamarkuptext}%
1.288 -\noindent
1.289 -This concludes the derivation of the characteristic theorems for
1.290 -type \isa{three}.
1.291 -
1.292 -The attentive reader has realized long ago that the
1.293 -above lengthy definition can be collapsed into one line:%
1.294 -\end{isamarkuptext}%
1.295 -\isamarkuptrue%
1.296 -\isacommand{datatype}\isamarkupfalse%
1.297 -\ better{\isaliteral{5F}{\isacharunderscore}}three\ {\isaliteral{3D}{\isacharequal}}\ A\ {\isaliteral{7C}{\isacharbar}}\ B\ {\isaliteral{7C}{\isacharbar}}\ C%
1.298 -\begin{isamarkuptext}%
1.299 -\noindent
1.300 -In fact, the \isacommand{datatype} command performs internally more or less
1.301 -the same derivations as we did, which gives you some idea what life would be
1.302 -like without \isacommand{datatype}.
1.303 -
1.304 -Although \isa{three} could be defined in one line, we have chosen this
1.305 -example to demonstrate \isacommand{typedef} because its simplicity makes the
1.306 -key concepts particularly easy to grasp. If you would like to see a
1.307 -non-trivial example that cannot be defined more directly, we recommend the
1.308 -definition of \emph{finite multisets} in the Library~\cite{HOL-Library}.
1.309 -
1.310 -Let us conclude by summarizing the above procedure for defining a new type.
1.311 -Given some abstract axiomatic description $P$ of a type $ty$ in terms of a
1.312 -set of functions $F$, this involves three steps:
1.313 -\begin{enumerate}
1.314 -\item Find an appropriate type $\tau$ and subset $A$ which has the desired
1.315 - properties $P$, and make a type definition based on this representation.
1.316 -\item Define the required functions $F$ on $ty$ by lifting
1.317 -analogous functions on the representation via $Abs_ty$ and $Rep_ty$.
1.318 -\item Prove that $P$ holds for $ty$ by lifting $P$ from the representation.
1.319 -\end{enumerate}
1.320 -You can now forget about the representation and work solely in terms of the
1.321 -abstract functions $F$ and properties $P$.%
1.322 -\index{typedecl@\isacommand {typedef} (command)|)}%
1.323 -\index{types!defining|)}%
1.324 -\end{isamarkuptext}%
1.325 -\isamarkuptrue%
1.326 -%
1.327 -\isadelimtheory
1.328 -%
1.329 -\endisadelimtheory
1.330 -%
1.331 -\isatagtheory
1.332 -%
1.333 -\endisatagtheory
1.334 -{\isafoldtheory}%
1.335 -%
1.336 -\isadelimtheory
1.337 -%
1.338 -\endisadelimtheory
1.339 -\end{isabellebody}%
1.340 -%%% Local Variables:
1.341 -%%% mode: latex
1.342 -%%% TeX-master: "root"
1.343 -%%% End: