doc-src/Codegen/Thy/document/Program.tex
author haftmann
Tue May 26 12:31:01 2009 +0200 (2009-05-26)
changeset 31254 03a35fbc9dc6
parent 31150 03a87478b89e
child 31544 19b77b1de188
permissions -rw-r--r--
documented print_codeproc command
haftmann@28447
     1
%
haftmann@28447
     2
\begin{isabellebody}%
haftmann@28447
     3
\def\isabellecontext{Program}%
haftmann@28447
     4
%
haftmann@28447
     5
\isadelimtheory
haftmann@28447
     6
%
haftmann@28447
     7
\endisadelimtheory
haftmann@28447
     8
%
haftmann@28447
     9
\isatagtheory
haftmann@28447
    10
\isacommand{theory}\isamarkupfalse%
haftmann@28447
    11
\ Program\isanewline
haftmann@28447
    12
\isakeyword{imports}\ Introduction\isanewline
haftmann@28447
    13
\isakeyword{begin}%
haftmann@28447
    14
\endisatagtheory
haftmann@28447
    15
{\isafoldtheory}%
haftmann@28447
    16
%
haftmann@28447
    17
\isadelimtheory
haftmann@28447
    18
%
haftmann@28447
    19
\endisadelimtheory
haftmann@28447
    20
%
haftmann@28447
    21
\isamarkupsection{Turning Theories into Programs \label{sec:program}%
haftmann@28447
    22
}
haftmann@28447
    23
\isamarkuptrue%
haftmann@28447
    24
%
haftmann@28447
    25
\isamarkupsubsection{The \isa{Isabelle{\isacharslash}HOL} default setup%
haftmann@28447
    26
}
haftmann@28447
    27
\isamarkuptrue%
haftmann@28447
    28
%
haftmann@28447
    29
\begin{isamarkuptext}%
haftmann@28447
    30
We have already seen how by default equations stemming from
haftmann@28447
    31
  \hyperlink{command.definition}{\mbox{\isa{\isacommand{definition}}}}/\hyperlink{command.primrec}{\mbox{\isa{\isacommand{primrec}}}}/\hyperlink{command.fun}{\mbox{\isa{\isacommand{fun}}}}
haftmann@28447
    32
  statements are used for code generation.  This default behaviour
haftmann@29560
    33
  can be changed, e.g. by providing different code equations.
haftmann@28593
    34
  All kinds of customisation shown in this section is \emph{safe}
haftmann@28447
    35
  in the sense that the user does not have to worry about
haftmann@28447
    36
  correctness -- all programs generatable that way are partially
haftmann@28447
    37
  correct.%
haftmann@28447
    38
\end{isamarkuptext}%
haftmann@28447
    39
\isamarkuptrue%
haftmann@28447
    40
%
haftmann@28447
    41
\isamarkupsubsection{Selecting code equations%
haftmann@28447
    42
}
haftmann@28447
    43
\isamarkuptrue%
haftmann@28447
    44
%
haftmann@28447
    45
\begin{isamarkuptext}%
haftmann@28447
    46
Coming back to our introductory example, we
haftmann@29560
    47
  could provide an alternative code equations for \isa{dequeue}
haftmann@28447
    48
  explicitly:%
haftmann@28447
    49
\end{isamarkuptext}%
haftmann@28447
    50
\isamarkuptrue%
haftmann@28447
    51
%
haftmann@28564
    52
\isadelimquote
haftmann@28447
    53
%
haftmann@28564
    54
\endisadelimquote
haftmann@28447
    55
%
haftmann@28564
    56
\isatagquote
haftmann@28447
    57
\isacommand{lemma}\isamarkupfalse%
haftmann@28562
    58
\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
haftmann@29798
    59
\ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\isanewline
haftmann@29798
    60
\ \ \ \ \ {\isacharparenleft}if\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ then\ {\isacharparenleft}None{\isacharcomma}\ AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\isanewline
haftmann@29798
    61
\ \ \ \ \ \ \ else\ dequeue\ {\isacharparenleft}AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharparenleft}rev\ xs{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
haftmann@29798
    62
\ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharparenleft}y\ {\isacharhash}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\isanewline
haftmann@29798
    63
\ \ \ \ \ {\isacharparenleft}Some\ y{\isacharcomma}\ AQueue\ xs\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline
haftmann@28447
    64
\ \ \isacommand{by}\isamarkupfalse%
haftmann@28447
    65
\ {\isacharparenleft}cases\ xs{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}\ {\isacharparenleft}cases\ {\isachardoublequoteopen}rev\ xs{\isachardoublequoteclose}{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}%
haftmann@28564
    66
\endisatagquote
haftmann@28564
    67
{\isafoldquote}%
haftmann@28447
    68
%
haftmann@28564
    69
\isadelimquote
haftmann@28447
    70
%
haftmann@28564
    71
\endisadelimquote
haftmann@28447
    72
%
haftmann@28447
    73
\begin{isamarkuptext}%
haftmann@28562
    74
\noindent The annotation \isa{{\isacharbrackleft}code{\isacharbrackright}} is an \isa{Isar}
haftmann@28447
    75
  \isa{attribute} which states that the given theorems should be
haftmann@29560
    76
  considered as code equations for a \isa{fun} statement --
haftmann@28447
    77
  the corresponding constant is determined syntactically.  The resulting code:%
haftmann@28447
    78
\end{isamarkuptext}%
haftmann@28447
    79
\isamarkuptrue%
haftmann@28447
    80
%
haftmann@28564
    81
\isadelimquote
haftmann@28447
    82
%
haftmann@28564
    83
\endisadelimquote
haftmann@28447
    84
%
haftmann@28564
    85
\isatagquote
haftmann@28447
    86
%
haftmann@28447
    87
\begin{isamarkuptext}%
haftmann@28727
    88
\isatypewriter%
haftmann@28447
    89
\noindent%
wenzelm@29297
    90
\hspace*{0pt}dequeue ::~forall a.~Queue a -> (Maybe a,~Queue a);\\
haftmann@29798
    91
\hspace*{0pt}dequeue (AQueue xs (y :~ys)) = (Just y,~AQueue xs ys);\\
haftmann@29798
    92
\hspace*{0pt}dequeue (AQueue xs []) =\\
haftmann@29798
    93
\hspace*{0pt} ~(if nulla xs then (Nothing,~AQueue [] [])\\
haftmann@29798
    94
\hspace*{0pt} ~~~else dequeue (AQueue [] (rev xs)));%
haftmann@28447
    95
\end{isamarkuptext}%
haftmann@28447
    96
\isamarkuptrue%
haftmann@28447
    97
%
haftmann@28564
    98
\endisatagquote
haftmann@28564
    99
{\isafoldquote}%
haftmann@28447
   100
%
haftmann@28564
   101
\isadelimquote
haftmann@28447
   102
%
haftmann@28564
   103
\endisadelimquote
haftmann@28447
   104
%
haftmann@28447
   105
\begin{isamarkuptext}%
haftmann@28447
   106
\noindent You may note that the equality test \isa{xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}} has been
haftmann@28447
   107
  replaced by the predicate \isa{null\ xs}.  This is due to the default
haftmann@28447
   108
  setup in the \qn{preprocessor} to be discussed further below (\secref{sec:preproc}).
haftmann@28447
   109
haftmann@28447
   110
  Changing the default constructor set of datatypes is also
haftmann@29798
   111
  possible.  See \secref{sec:datatypes} for an example.
haftmann@28447
   112
haftmann@28447
   113
  As told in \secref{sec:concept}, code generation is based
haftmann@28447
   114
  on a structured collection of code theorems.
haftmann@28447
   115
  For explorative purpose, this collection
haftmann@28447
   116
  may be inspected using the \hyperlink{command.code-thms}{\mbox{\isa{\isacommand{code{\isacharunderscore}thms}}}} command:%
haftmann@28447
   117
\end{isamarkuptext}%
haftmann@28447
   118
\isamarkuptrue%
haftmann@28447
   119
%
haftmann@28564
   120
\isadelimquote
haftmann@28447
   121
%
haftmann@28564
   122
\endisadelimquote
haftmann@28447
   123
%
haftmann@28564
   124
\isatagquote
haftmann@28447
   125
\isacommand{code{\isacharunderscore}thms}\isamarkupfalse%
haftmann@28447
   126
\ dequeue%
haftmann@28564
   127
\endisatagquote
haftmann@28564
   128
{\isafoldquote}%
haftmann@28447
   129
%
haftmann@28564
   130
\isadelimquote
haftmann@28447
   131
%
haftmann@28564
   132
\endisadelimquote
haftmann@28447
   133
%
haftmann@28447
   134
\begin{isamarkuptext}%
haftmann@29560
   135
\noindent prints a table with \emph{all} code equations
haftmann@28447
   136
  for \isa{dequeue}, including
haftmann@29560
   137
  \emph{all} code equations those equations depend
haftmann@28447
   138
  on recursively.
haftmann@28447
   139
  
haftmann@28447
   140
  Similarly, the \hyperlink{command.code-deps}{\mbox{\isa{\isacommand{code{\isacharunderscore}deps}}}} command shows a graph
haftmann@29560
   141
  visualising dependencies between code equations.%
haftmann@28447
   142
\end{isamarkuptext}%
haftmann@28447
   143
\isamarkuptrue%
haftmann@28447
   144
%
haftmann@28447
   145
\isamarkupsubsection{\isa{class} and \isa{instantiation}%
haftmann@28447
   146
}
haftmann@28447
   147
\isamarkuptrue%
haftmann@28447
   148
%
haftmann@28447
   149
\begin{isamarkuptext}%
haftmann@28447
   150
Concerning type classes and code generation, let us examine an example
haftmann@28447
   151
  from abstract algebra:%
haftmann@28447
   152
\end{isamarkuptext}%
haftmann@28447
   153
\isamarkuptrue%
haftmann@28447
   154
%
haftmann@28564
   155
\isadelimquote
haftmann@28447
   156
%
haftmann@28564
   157
\endisadelimquote
haftmann@28447
   158
%
haftmann@28564
   159
\isatagquote
haftmann@28447
   160
\isacommand{class}\isamarkupfalse%
haftmann@29798
   161
\ semigroup\ {\isacharequal}\isanewline
haftmann@28447
   162
\ \ \isakeyword{fixes}\ mult\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}\ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymotimes}{\isachardoublequoteclose}\ {\isadigit{7}}{\isadigit{0}}{\isacharparenright}\isanewline
haftmann@28447
   163
\ \ \isakeyword{assumes}\ assoc{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}x\ {\isasymotimes}\ y{\isacharparenright}\ {\isasymotimes}\ z\ {\isacharequal}\ x\ {\isasymotimes}\ {\isacharparenleft}y\ {\isasymotimes}\ z{\isacharparenright}{\isachardoublequoteclose}\isanewline
haftmann@28447
   164
\isanewline
haftmann@28447
   165
\isacommand{class}\isamarkupfalse%
haftmann@28447
   166
\ monoid\ {\isacharequal}\ semigroup\ {\isacharplus}\isanewline
haftmann@28447
   167
\ \ \isakeyword{fixes}\ neutral\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\ {\isacharparenleft}{\isachardoublequoteopen}{\isasymone}{\isachardoublequoteclose}{\isacharparenright}\isanewline
haftmann@28447
   168
\ \ \isakeyword{assumes}\ neutl{\isacharcolon}\ {\isachardoublequoteopen}{\isasymone}\ {\isasymotimes}\ x\ {\isacharequal}\ x{\isachardoublequoteclose}\isanewline
haftmann@28447
   169
\ \ \ \ \isakeyword{and}\ neutr{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ x{\isachardoublequoteclose}\isanewline
haftmann@28447
   170
\isanewline
haftmann@28447
   171
\isacommand{instantiation}\isamarkupfalse%
haftmann@28447
   172
\ nat\ {\isacharcolon}{\isacharcolon}\ monoid\isanewline
haftmann@28447
   173
\isakeyword{begin}\isanewline
haftmann@28447
   174
\isanewline
haftmann@28447
   175
\isacommand{primrec}\isamarkupfalse%
haftmann@28447
   176
\ mult{\isacharunderscore}nat\ \isakeyword{where}\isanewline
haftmann@28447
   177
\ \ \ \ {\isachardoublequoteopen}{\isadigit{0}}\ {\isasymotimes}\ n\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}nat{\isacharparenright}{\isachardoublequoteclose}\isanewline
haftmann@28447
   178
\ \ {\isacharbar}\ {\isachardoublequoteopen}Suc\ m\ {\isasymotimes}\ n\ {\isacharequal}\ n\ {\isacharplus}\ m\ {\isasymotimes}\ n{\isachardoublequoteclose}\isanewline
haftmann@28447
   179
\isanewline
haftmann@28447
   180
\isacommand{definition}\isamarkupfalse%
haftmann@28447
   181
\ neutral{\isacharunderscore}nat\ \isakeyword{where}\isanewline
haftmann@28447
   182
\ \ {\isachardoublequoteopen}{\isasymone}\ {\isacharequal}\ Suc\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
haftmann@28447
   183
\isanewline
haftmann@28447
   184
\isacommand{lemma}\isamarkupfalse%
haftmann@28447
   185
\ add{\isacharunderscore}mult{\isacharunderscore}distrib{\isacharcolon}\isanewline
haftmann@28447
   186
\ \ \isakeyword{fixes}\ n\ m\ q\ {\isacharcolon}{\isacharcolon}\ nat\isanewline
haftmann@28447
   187
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}{\isacharparenleft}n\ {\isacharplus}\ m{\isacharparenright}\ {\isasymotimes}\ q\ {\isacharequal}\ n\ {\isasymotimes}\ q\ {\isacharplus}\ m\ {\isasymotimes}\ q{\isachardoublequoteclose}\isanewline
haftmann@28447
   188
\ \ \isacommand{by}\isamarkupfalse%
haftmann@28447
   189
\ {\isacharparenleft}induct\ n{\isacharparenright}\ simp{\isacharunderscore}all\isanewline
haftmann@28447
   190
\isanewline
haftmann@28447
   191
\isacommand{instance}\isamarkupfalse%
haftmann@28447
   192
\ \isacommand{proof}\isamarkupfalse%
haftmann@28447
   193
\isanewline
haftmann@28447
   194
\ \ \isacommand{fix}\isamarkupfalse%
haftmann@28447
   195
\ m\ n\ q\ {\isacharcolon}{\isacharcolon}\ nat\isanewline
haftmann@28447
   196
\ \ \isacommand{show}\isamarkupfalse%
haftmann@28447
   197
\ {\isachardoublequoteopen}m\ {\isasymotimes}\ n\ {\isasymotimes}\ q\ {\isacharequal}\ m\ {\isasymotimes}\ {\isacharparenleft}n\ {\isasymotimes}\ q{\isacharparenright}{\isachardoublequoteclose}\isanewline
haftmann@28447
   198
\ \ \ \ \isacommand{by}\isamarkupfalse%
haftmann@28447
   199
\ {\isacharparenleft}induct\ m{\isacharparenright}\ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ add{\isacharunderscore}mult{\isacharunderscore}distrib{\isacharparenright}\isanewline
haftmann@28447
   200
\ \ \isacommand{show}\isamarkupfalse%
haftmann@28447
   201
\ {\isachardoublequoteopen}{\isasymone}\ {\isasymotimes}\ n\ {\isacharequal}\ n{\isachardoublequoteclose}\isanewline
haftmann@28447
   202
\ \ \ \ \isacommand{by}\isamarkupfalse%
haftmann@28447
   203
\ {\isacharparenleft}simp\ add{\isacharcolon}\ neutral{\isacharunderscore}nat{\isacharunderscore}def{\isacharparenright}\isanewline
haftmann@28447
   204
\ \ \isacommand{show}\isamarkupfalse%
haftmann@28447
   205
\ {\isachardoublequoteopen}m\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ m{\isachardoublequoteclose}\isanewline
haftmann@28447
   206
\ \ \ \ \isacommand{by}\isamarkupfalse%
haftmann@28447
   207
\ {\isacharparenleft}induct\ m{\isacharparenright}\ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ neutral{\isacharunderscore}nat{\isacharunderscore}def{\isacharparenright}\isanewline
haftmann@28447
   208
\isacommand{qed}\isamarkupfalse%
haftmann@28447
   209
\isanewline
haftmann@28447
   210
\isanewline
haftmann@28447
   211
\isacommand{end}\isamarkupfalse%
haftmann@28447
   212
%
haftmann@28564
   213
\endisatagquote
haftmann@28564
   214
{\isafoldquote}%
haftmann@28447
   215
%
haftmann@28564
   216
\isadelimquote
haftmann@28447
   217
%
haftmann@28564
   218
\endisadelimquote
haftmann@28447
   219
%
haftmann@28447
   220
\begin{isamarkuptext}%
haftmann@28447
   221
\noindent We define the natural operation of the natural numbers
haftmann@28447
   222
  on monoids:%
haftmann@28447
   223
\end{isamarkuptext}%
haftmann@28447
   224
\isamarkuptrue%
haftmann@28447
   225
%
haftmann@28564
   226
\isadelimquote
haftmann@28447
   227
%
haftmann@28564
   228
\endisadelimquote
haftmann@28447
   229
%
haftmann@28564
   230
\isatagquote
haftmann@28447
   231
\isacommand{primrec}\isamarkupfalse%
haftmann@28447
   232
\ {\isacharparenleft}\isakeyword{in}\ monoid{\isacharparenright}\ pow\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
haftmann@28447
   233
\ \ \ \ {\isachardoublequoteopen}pow\ {\isadigit{0}}\ a\ {\isacharequal}\ {\isasymone}{\isachardoublequoteclose}\isanewline
haftmann@28447
   234
\ \ {\isacharbar}\ {\isachardoublequoteopen}pow\ {\isacharparenleft}Suc\ n{\isacharparenright}\ a\ {\isacharequal}\ a\ {\isasymotimes}\ pow\ n\ a{\isachardoublequoteclose}%
haftmann@28564
   235
\endisatagquote
haftmann@28564
   236
{\isafoldquote}%
haftmann@28447
   237
%
haftmann@28564
   238
\isadelimquote
haftmann@28447
   239
%
haftmann@28564
   240
\endisadelimquote
haftmann@28447
   241
%
haftmann@28447
   242
\begin{isamarkuptext}%
haftmann@28447
   243
\noindent This we use to define the discrete exponentiation function:%
haftmann@28447
   244
\end{isamarkuptext}%
haftmann@28447
   245
\isamarkuptrue%
haftmann@28447
   246
%
haftmann@28564
   247
\isadelimquote
haftmann@28447
   248
%
haftmann@28564
   249
\endisadelimquote
haftmann@28447
   250
%
haftmann@28564
   251
\isatagquote
haftmann@28447
   252
\isacommand{definition}\isamarkupfalse%
haftmann@28447
   253
\ bexp\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
haftmann@28447
   254
\ \ {\isachardoublequoteopen}bexp\ n\ {\isacharequal}\ pow\ n\ {\isacharparenleft}Suc\ {\isacharparenleft}Suc\ {\isadigit{0}}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}%
haftmann@28564
   255
\endisatagquote
haftmann@28564
   256
{\isafoldquote}%
haftmann@28447
   257
%
haftmann@28564
   258
\isadelimquote
haftmann@28447
   259
%
haftmann@28564
   260
\endisadelimquote
haftmann@28447
   261
%
haftmann@28447
   262
\begin{isamarkuptext}%
haftmann@28447
   263
\noindent The corresponding code:%
haftmann@28447
   264
\end{isamarkuptext}%
haftmann@28447
   265
\isamarkuptrue%
haftmann@28447
   266
%
haftmann@28564
   267
\isadelimquote
haftmann@28447
   268
%
haftmann@28564
   269
\endisadelimquote
haftmann@28447
   270
%
haftmann@28564
   271
\isatagquote
haftmann@28447
   272
%
haftmann@28447
   273
\begin{isamarkuptext}%
haftmann@28727
   274
\isatypewriter%
haftmann@28447
   275
\noindent%
haftmann@28714
   276
\hspace*{0pt}module Example where {\char123}\\
haftmann@28714
   277
\hspace*{0pt}\\
haftmann@28714
   278
\hspace*{0pt}\\
wenzelm@30121
   279
\hspace*{0pt}data Nat = Zero{\char95}nat | Suc Nat;\\
haftmann@28714
   280
\hspace*{0pt}\\
haftmann@28714
   281
\hspace*{0pt}class Semigroup a where {\char123}\\
haftmann@28714
   282
\hspace*{0pt} ~mult ::~a -> a -> a;\\
haftmann@28714
   283
\hspace*{0pt}{\char125};\\
haftmann@28714
   284
\hspace*{0pt}\\
haftmann@28714
   285
\hspace*{0pt}class (Semigroup a) => Monoid a where {\char123}\\
haftmann@28714
   286
\hspace*{0pt} ~neutral ::~a;\\
haftmann@28714
   287
\hspace*{0pt}{\char125};\\
haftmann@28714
   288
\hspace*{0pt}\\
wenzelm@29297
   289
\hspace*{0pt}pow ::~forall a.~(Monoid a) => Nat -> a -> a;\\
haftmann@28714
   290
\hspace*{0pt}pow Zero{\char95}nat a = neutral;\\
haftmann@28714
   291
\hspace*{0pt}pow (Suc n) a = mult a (pow n a);\\
haftmann@28714
   292
\hspace*{0pt}\\
haftmann@28714
   293
\hspace*{0pt}plus{\char95}nat ::~Nat -> Nat -> Nat;\\
haftmann@28714
   294
\hspace*{0pt}plus{\char95}nat (Suc m) n = plus{\char95}nat m (Suc n);\\
haftmann@28714
   295
\hspace*{0pt}plus{\char95}nat Zero{\char95}nat n = n;\\
haftmann@28714
   296
\hspace*{0pt}\\
haftmann@28714
   297
\hspace*{0pt}neutral{\char95}nat ::~Nat;\\
haftmann@28714
   298
\hspace*{0pt}neutral{\char95}nat = Suc Zero{\char95}nat;\\
haftmann@28714
   299
\hspace*{0pt}\\
haftmann@28714
   300
\hspace*{0pt}mult{\char95}nat ::~Nat -> Nat -> Nat;\\
haftmann@28714
   301
\hspace*{0pt}mult{\char95}nat Zero{\char95}nat n = Zero{\char95}nat;\\
haftmann@28714
   302
\hspace*{0pt}mult{\char95}nat (Suc m) n = plus{\char95}nat n (mult{\char95}nat m n);\\
haftmann@28714
   303
\hspace*{0pt}\\
haftmann@28714
   304
\hspace*{0pt}instance Semigroup Nat where {\char123}\\
haftmann@28714
   305
\hspace*{0pt} ~mult = mult{\char95}nat;\\
haftmann@28714
   306
\hspace*{0pt}{\char125};\\
haftmann@28714
   307
\hspace*{0pt}\\
haftmann@28714
   308
\hspace*{0pt}instance Monoid Nat where {\char123}\\
haftmann@28714
   309
\hspace*{0pt} ~neutral = neutral{\char95}nat;\\
haftmann@28714
   310
\hspace*{0pt}{\char125};\\
haftmann@28714
   311
\hspace*{0pt}\\
haftmann@28714
   312
\hspace*{0pt}bexp ::~Nat -> Nat;\\
haftmann@28714
   313
\hspace*{0pt}bexp n = pow n (Suc (Suc Zero{\char95}nat));\\
haftmann@28714
   314
\hspace*{0pt}\\
haftmann@28714
   315
\hspace*{0pt}{\char125}%
haftmann@28447
   316
\end{isamarkuptext}%
haftmann@28447
   317
\isamarkuptrue%
haftmann@28447
   318
%
haftmann@28564
   319
\endisatagquote
haftmann@28564
   320
{\isafoldquote}%
haftmann@28447
   321
%
haftmann@28564
   322
\isadelimquote
haftmann@28447
   323
%
haftmann@28564
   324
\endisadelimquote
haftmann@28447
   325
%
haftmann@28447
   326
\begin{isamarkuptext}%
haftmann@28447
   327
\noindent This is a convenient place to show how explicit dictionary construction
haftmann@28447
   328
  manifests in generated code (here, the same example in \isa{SML}):%
haftmann@28447
   329
\end{isamarkuptext}%
haftmann@28447
   330
\isamarkuptrue%
haftmann@28447
   331
%
haftmann@28564
   332
\isadelimquote
haftmann@28447
   333
%
haftmann@28564
   334
\endisadelimquote
haftmann@28447
   335
%
haftmann@28564
   336
\isatagquote
haftmann@28447
   337
%
haftmann@28447
   338
\begin{isamarkuptext}%
haftmann@28727
   339
\isatypewriter%
haftmann@28447
   340
\noindent%
haftmann@28714
   341
\hspace*{0pt}structure Example = \\
haftmann@28714
   342
\hspace*{0pt}struct\\
haftmann@28714
   343
\hspace*{0pt}\\
wenzelm@30121
   344
\hspace*{0pt}datatype nat = Zero{\char95}nat | Suc of nat;\\
haftmann@28714
   345
\hspace*{0pt}\\
haftmann@28714
   346
\hspace*{0pt}type 'a semigroup = {\char123}mult :~'a -> 'a -> 'a{\char125};\\
haftmann@28714
   347
\hspace*{0pt}fun mult (A{\char95}:'a semigroup) = {\char35}mult A{\char95};\\
haftmann@28714
   348
\hspace*{0pt}\\
wenzelm@29297
   349
\hspace*{0pt}type 'a monoid = {\char123}Program{\char95}{\char95}semigroup{\char95}monoid :~'a semigroup,~neutral :~'a{\char125};\\
haftmann@28714
   350
\hspace*{0pt}fun semigroup{\char95}monoid (A{\char95}:'a monoid) = {\char35}Program{\char95}{\char95}semigroup{\char95}monoid A{\char95};\\
haftmann@28714
   351
\hspace*{0pt}fun neutral (A{\char95}:'a monoid) = {\char35}neutral A{\char95};\\
haftmann@28714
   352
\hspace*{0pt}\\
haftmann@28714
   353
\hspace*{0pt}fun pow A{\char95}~Zero{\char95}nat a = neutral A{\char95}\\
haftmann@28714
   354
\hspace*{0pt} ~| pow A{\char95}~(Suc n) a = mult (semigroup{\char95}monoid A{\char95}) a (pow A{\char95}~n a);\\
haftmann@28714
   355
\hspace*{0pt}\\
haftmann@28714
   356
\hspace*{0pt}fun plus{\char95}nat (Suc m) n = plus{\char95}nat m (Suc n)\\
haftmann@28714
   357
\hspace*{0pt} ~| plus{\char95}nat Zero{\char95}nat n = n;\\
haftmann@28714
   358
\hspace*{0pt}\\
wenzelm@29297
   359
\hspace*{0pt}val neutral{\char95}nat :~nat = Suc Zero{\char95}nat\\
haftmann@28714
   360
\hspace*{0pt}\\
haftmann@28714
   361
\hspace*{0pt}fun mult{\char95}nat Zero{\char95}nat n = Zero{\char95}nat\\
haftmann@28714
   362
\hspace*{0pt} ~| mult{\char95}nat (Suc m) n = plus{\char95}nat n (mult{\char95}nat m n);\\
haftmann@28714
   363
\hspace*{0pt}\\
haftmann@28714
   364
\hspace*{0pt}val semigroup{\char95}nat = {\char123}mult = mult{\char95}nat{\char125}~:~nat semigroup;\\
haftmann@28714
   365
\hspace*{0pt}\\
haftmann@28714
   366
\hspace*{0pt}val monoid{\char95}nat =\\
wenzelm@29297
   367
\hspace*{0pt} ~{\char123}Program{\char95}{\char95}semigroup{\char95}monoid = semigroup{\char95}nat,~neutral = neutral{\char95}nat{\char125}~:\\
haftmann@28714
   368
\hspace*{0pt} ~nat monoid;\\
haftmann@28714
   369
\hspace*{0pt}\\
haftmann@28714
   370
\hspace*{0pt}fun bexp n = pow monoid{\char95}nat n (Suc (Suc Zero{\char95}nat));\\
haftmann@28714
   371
\hspace*{0pt}\\
wenzelm@29297
   372
\hspace*{0pt}end;~(*struct Example*)%
haftmann@28447
   373
\end{isamarkuptext}%
haftmann@28447
   374
\isamarkuptrue%
haftmann@28447
   375
%
haftmann@28564
   376
\endisatagquote
haftmann@28564
   377
{\isafoldquote}%
haftmann@28447
   378
%
haftmann@28564
   379
\isadelimquote
haftmann@28447
   380
%
haftmann@28564
   381
\endisadelimquote
haftmann@28447
   382
%
haftmann@28447
   383
\begin{isamarkuptext}%
haftmann@28447
   384
\noindent Note the parameters with trailing underscore (\verb|A_|)
haftmann@28447
   385
    which are the dictionary parameters.%
haftmann@28447
   386
\end{isamarkuptext}%
haftmann@28447
   387
\isamarkuptrue%
haftmann@28447
   388
%
haftmann@28447
   389
\isamarkupsubsection{The preprocessor \label{sec:preproc}%
haftmann@28447
   390
}
haftmann@28447
   391
\isamarkuptrue%
haftmann@28447
   392
%
haftmann@28447
   393
\begin{isamarkuptext}%
haftmann@28447
   394
Before selected function theorems are turned into abstract
haftmann@28447
   395
  code, a chain of definitional transformation steps is carried
haftmann@28447
   396
  out: \emph{preprocessing}.  In essence, the preprocessor
haftmann@28447
   397
  consists of two components: a \emph{simpset} and \emph{function transformers}.
haftmann@28447
   398
haftmann@28447
   399
  The \emph{simpset} allows to employ the full generality of the Isabelle
haftmann@28447
   400
  simplifier.  Due to the interpretation of theorems
haftmann@29560
   401
  as code equations, rewrites are applied to the right
haftmann@28447
   402
  hand side and the arguments of the left hand side of an
haftmann@28447
   403
  equation, but never to the constant heading the left hand side.
haftmann@28447
   404
  An important special case are \emph{inline theorems} which may be
haftmann@28447
   405
  declared and undeclared using the
haftmann@28447
   406
  \emph{code inline} or \emph{code inline del} attribute respectively.
haftmann@28447
   407
haftmann@28447
   408
  Some common applications:%
haftmann@28447
   409
\end{isamarkuptext}%
haftmann@28447
   410
\isamarkuptrue%
haftmann@28447
   411
%
haftmann@28447
   412
\begin{itemize}
haftmann@28447
   413
%
haftmann@28447
   414
\begin{isamarkuptext}%
haftmann@28447
   415
\item replacing non-executable constructs by executable ones:%
haftmann@28447
   416
\end{isamarkuptext}%
haftmann@28447
   417
\isamarkuptrue%
haftmann@28447
   418
%
haftmann@28564
   419
\isadelimquote
haftmann@28447
   420
%
haftmann@28564
   421
\endisadelimquote
haftmann@28447
   422
%
haftmann@28564
   423
\isatagquote
haftmann@28447
   424
\isacommand{lemma}\isamarkupfalse%
haftmann@28447
   425
\ {\isacharbrackleft}code\ inline{\isacharbrackright}{\isacharcolon}\isanewline
haftmann@28447
   426
\ \ {\isachardoublequoteopen}x\ {\isasymin}\ set\ xs\ {\isasymlongleftrightarrow}\ x\ mem\ xs{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
haftmann@28447
   427
\ {\isacharparenleft}induct\ xs{\isacharparenright}\ simp{\isacharunderscore}all%
haftmann@28564
   428
\endisatagquote
haftmann@28564
   429
{\isafoldquote}%
haftmann@28447
   430
%
haftmann@28564
   431
\isadelimquote
haftmann@28447
   432
%
haftmann@28564
   433
\endisadelimquote
haftmann@28447
   434
%
haftmann@28447
   435
\begin{isamarkuptext}%
haftmann@28447
   436
\item eliminating superfluous constants:%
haftmann@28447
   437
\end{isamarkuptext}%
haftmann@28447
   438
\isamarkuptrue%
haftmann@28447
   439
%
haftmann@28564
   440
\isadelimquote
haftmann@28447
   441
%
haftmann@28564
   442
\endisadelimquote
haftmann@28447
   443
%
haftmann@28564
   444
\isatagquote
haftmann@28447
   445
\isacommand{lemma}\isamarkupfalse%
haftmann@28447
   446
\ {\isacharbrackleft}code\ inline{\isacharbrackright}{\isacharcolon}\isanewline
haftmann@28447
   447
\ \ {\isachardoublequoteopen}{\isadigit{1}}\ {\isacharequal}\ Suc\ {\isadigit{0}}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
haftmann@28447
   448
\ simp%
haftmann@28564
   449
\endisatagquote
haftmann@28564
   450
{\isafoldquote}%
haftmann@28447
   451
%
haftmann@28564
   452
\isadelimquote
haftmann@28447
   453
%
haftmann@28564
   454
\endisadelimquote
haftmann@28447
   455
%
haftmann@28447
   456
\begin{isamarkuptext}%
haftmann@28447
   457
\item replacing executable but inconvenient constructs:%
haftmann@28447
   458
\end{isamarkuptext}%
haftmann@28447
   459
\isamarkuptrue%
haftmann@28447
   460
%
haftmann@28564
   461
\isadelimquote
haftmann@28447
   462
%
haftmann@28564
   463
\endisadelimquote
haftmann@28447
   464
%
haftmann@28564
   465
\isatagquote
haftmann@28447
   466
\isacommand{lemma}\isamarkupfalse%
haftmann@28447
   467
\ {\isacharbrackleft}code\ inline{\isacharbrackright}{\isacharcolon}\isanewline
haftmann@28447
   468
\ \ {\isachardoublequoteopen}xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymlongleftrightarrow}\ List{\isachardot}null\ xs{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
haftmann@28447
   469
\ {\isacharparenleft}induct\ xs{\isacharparenright}\ simp{\isacharunderscore}all%
haftmann@28564
   470
\endisatagquote
haftmann@28564
   471
{\isafoldquote}%
haftmann@28447
   472
%
haftmann@28564
   473
\isadelimquote
haftmann@28447
   474
%
haftmann@28564
   475
\endisadelimquote
haftmann@28447
   476
%
haftmann@28447
   477
\end{itemize}
haftmann@28447
   478
%
haftmann@28447
   479
\begin{isamarkuptext}%
haftmann@28447
   480
\noindent \emph{Function transformers} provide a very general interface,
haftmann@28447
   481
  transforming a list of function theorems to another
haftmann@28447
   482
  list of function theorems, provided that neither the heading
haftmann@28447
   483
  constant nor its type change.  The \isa{{\isadigit{0}}} / \isa{Suc}
haftmann@28447
   484
  pattern elimination implemented in
haftmann@28447
   485
  theory \isa{Efficient{\isacharunderscore}Nat} (see \secref{eff_nat}) uses this
haftmann@28447
   486
  interface.
haftmann@28447
   487
haftmann@28447
   488
  \noindent The current setup of the preprocessor may be inspected using
haftmann@31254
   489
  the \hyperlink{command.print-codeproc}{\mbox{\isa{\isacommand{print{\isacharunderscore}codeproc}}}} command.
haftmann@28447
   490
  \hyperlink{command.code-thms}{\mbox{\isa{\isacommand{code{\isacharunderscore}thms}}}} provides a convenient
haftmann@28447
   491
  mechanism to inspect the impact of a preprocessor setup
haftmann@29560
   492
  on code equations.
haftmann@28447
   493
haftmann@28447
   494
  \begin{warn}
haftmann@28447
   495
    The attribute \emph{code unfold}
haftmann@28447
   496
    associated with the \isa{SML\ code\ generator} also applies to
haftmann@28447
   497
    the \isa{generic\ code\ generator}:
haftmann@28447
   498
    \emph{code unfold} implies \emph{code inline}.
haftmann@28447
   499
  \end{warn}%
haftmann@28447
   500
\end{isamarkuptext}%
haftmann@28447
   501
\isamarkuptrue%
haftmann@28447
   502
%
haftmann@28447
   503
\isamarkupsubsection{Datatypes \label{sec:datatypes}%
haftmann@28447
   504
}
haftmann@28447
   505
\isamarkuptrue%
haftmann@28447
   506
%
haftmann@28447
   507
\begin{isamarkuptext}%
haftmann@28447
   508
Conceptually, any datatype is spanned by a set of
haftmann@29798
   509
  \emph{constructors} of type \isa{{\isasymtau}\ {\isacharequal}\ {\isasymdots}\ {\isasymRightarrow}\ {\isasymkappa}\ {\isasymalpha}\isactrlisub {\isadigit{1}}\ {\isasymdots}\ {\isasymalpha}\isactrlisub n} where \isa{{\isacharbraceleft}{\isasymalpha}\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlisub n{\isacharbraceright}} is exactly the set of \emph{all} type variables in
haftmann@29798
   510
  \isa{{\isasymtau}}.  The HOL datatype package by default registers any new
haftmann@29798
   511
  datatype in the table of datatypes, which may be inspected using the
haftmann@29798
   512
  \hyperlink{command.print-codesetup}{\mbox{\isa{\isacommand{print{\isacharunderscore}codesetup}}}} command.
haftmann@28447
   513
haftmann@29798
   514
  In some cases, it is appropriate to alter or extend this table.  As
haftmann@29798
   515
  an example, we will develop an alternative representation of the
haftmann@29798
   516
  queue example given in \secref{sec:intro}.  The amortised
haftmann@29798
   517
  representation is convenient for generating code but exposes its
haftmann@29798
   518
  \qt{implementation} details, which may be cumbersome when proving
haftmann@29798
   519
  theorems about it.  Therefore, here a simple, straightforward
haftmann@29798
   520
  representation of queues:%
haftmann@29798
   521
\end{isamarkuptext}%
haftmann@29798
   522
\isamarkuptrue%
haftmann@29798
   523
%
haftmann@29798
   524
\isadelimquote
haftmann@29798
   525
%
haftmann@29798
   526
\endisadelimquote
haftmann@29798
   527
%
haftmann@29798
   528
\isatagquote
haftmann@29798
   529
\isacommand{datatype}\isamarkupfalse%
haftmann@29798
   530
\ {\isacharprime}a\ queue\ {\isacharequal}\ Queue\ {\isachardoublequoteopen}{\isacharprime}a\ list{\isachardoublequoteclose}\isanewline
haftmann@29798
   531
\isanewline
haftmann@29798
   532
\isacommand{definition}\isamarkupfalse%
haftmann@29798
   533
\ empty\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
haftmann@29798
   534
\ \ {\isachardoublequoteopen}empty\ {\isacharequal}\ Queue\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
haftmann@29798
   535
\isanewline
haftmann@29798
   536
\isacommand{primrec}\isamarkupfalse%
haftmann@29798
   537
\ enqueue\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ queue\ {\isasymRightarrow}\ {\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
haftmann@29798
   538
\ \ {\isachardoublequoteopen}enqueue\ x\ {\isacharparenleft}Queue\ xs{\isacharparenright}\ {\isacharequal}\ Queue\ {\isacharparenleft}xs\ {\isacharat}\ {\isacharbrackleft}x{\isacharbrackright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
haftmann@29798
   539
\isanewline
haftmann@29798
   540
\isacommand{fun}\isamarkupfalse%
haftmann@29798
   541
\ dequeue\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ queue\ {\isasymRightarrow}\ {\isacharprime}a\ option\ {\isasymtimes}\ {\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
haftmann@29798
   542
\ \ \ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}Queue\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}None{\isacharcomma}\ Queue\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
haftmann@29798
   543
\ \ {\isacharbar}\ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}Queue\ {\isacharparenleft}x\ {\isacharhash}\ xs{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}Some\ x{\isacharcomma}\ Queue\ xs{\isacharparenright}{\isachardoublequoteclose}%
haftmann@29798
   544
\endisatagquote
haftmann@29798
   545
{\isafoldquote}%
haftmann@29798
   546
%
haftmann@29798
   547
\isadelimquote
haftmann@29798
   548
%
haftmann@29798
   549
\endisadelimquote
haftmann@29798
   550
%
haftmann@29798
   551
\begin{isamarkuptext}%
haftmann@29798
   552
\noindent This we can use directly for proving;  for executing,
haftmann@29798
   553
  we provide an alternative characterisation:%
haftmann@28447
   554
\end{isamarkuptext}%
haftmann@28447
   555
\isamarkuptrue%
haftmann@28447
   556
%
haftmann@28564
   557
\isadelimquote
haftmann@28447
   558
%
haftmann@28564
   559
\endisadelimquote
haftmann@28447
   560
%
haftmann@28564
   561
\isatagquote
haftmann@28447
   562
\isacommand{definition}\isamarkupfalse%
haftmann@29798
   563
\ AQueue\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
haftmann@29798
   564
\ \ {\isachardoublequoteopen}AQueue\ xs\ ys\ {\isacharequal}\ Queue\ {\isacharparenleft}ys\ {\isacharat}\ rev\ xs{\isacharparenright}{\isachardoublequoteclose}\isanewline
haftmann@28447
   565
\isanewline
haftmann@29798
   566
\isacommand{code{\isacharunderscore}datatype}\isamarkupfalse%
haftmann@29798
   567
\ AQueue%
haftmann@28564
   568
\endisatagquote
haftmann@28564
   569
{\isafoldquote}%
haftmann@28447
   570
%
haftmann@28564
   571
\isadelimquote
haftmann@28447
   572
%
haftmann@28564
   573
\endisadelimquote
haftmann@28447
   574
%
haftmann@28447
   575
\begin{isamarkuptext}%
haftmann@30227
   576
\noindent Here we define a \qt{constructor} \isa{AQueue} which
haftmann@29798
   577
  is defined in terms of \isa{Queue} and interprets its arguments
haftmann@29798
   578
  according to what the \emph{content} of an amortised queue is supposed
haftmann@29798
   579
  to be.  Equipped with this, we are able to prove the following equations
haftmann@29798
   580
  for our primitive queue operations which \qt{implement} the simple
haftmann@29798
   581
  queues in an amortised fashion:%
haftmann@28447
   582
\end{isamarkuptext}%
haftmann@28447
   583
\isamarkuptrue%
haftmann@28447
   584
%
haftmann@28564
   585
\isadelimquote
haftmann@28447
   586
%
haftmann@28564
   587
\endisadelimquote
haftmann@28447
   588
%
haftmann@28564
   589
\isatagquote
haftmann@28447
   590
\isacommand{lemma}\isamarkupfalse%
haftmann@29798
   591
\ empty{\isacharunderscore}AQueue\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
haftmann@29798
   592
\ \ {\isachardoublequoteopen}empty\ {\isacharequal}\ AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
haftmann@29798
   593
\ \ \isacommand{unfolding}\isamarkupfalse%
haftmann@29798
   594
\ AQueue{\isacharunderscore}def\ empty{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
haftmann@29798
   595
\ simp\isanewline
haftmann@29798
   596
\isanewline
haftmann@29798
   597
\isacommand{lemma}\isamarkupfalse%
haftmann@29798
   598
\ enqueue{\isacharunderscore}AQueue\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
haftmann@29798
   599
\ \ {\isachardoublequoteopen}enqueue\ x\ {\isacharparenleft}AQueue\ xs\ ys{\isacharparenright}\ {\isacharequal}\ AQueue\ {\isacharparenleft}x\ {\isacharhash}\ xs{\isacharparenright}\ ys{\isachardoublequoteclose}\isanewline
haftmann@29798
   600
\ \ \isacommand{unfolding}\isamarkupfalse%
haftmann@29798
   601
\ AQueue{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
haftmann@29798
   602
\ simp\isanewline
haftmann@29798
   603
\isanewline
haftmann@29798
   604
\isacommand{lemma}\isamarkupfalse%
haftmann@29798
   605
\ dequeue{\isacharunderscore}AQueue\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
haftmann@29798
   606
\ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\isanewline
haftmann@29798
   607
\ \ \ \ {\isacharparenleft}if\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ then\ {\isacharparenleft}None{\isacharcomma}\ AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\isanewline
haftmann@29798
   608
\ \ \ \ else\ dequeue\ {\isacharparenleft}AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharparenleft}rev\ xs{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
haftmann@29798
   609
\ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharparenleft}y\ {\isacharhash}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}Some\ y{\isacharcomma}\ AQueue\ xs\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline
haftmann@29798
   610
\ \ \isacommand{unfolding}\isamarkupfalse%
haftmann@29798
   611
\ AQueue{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
haftmann@29798
   612
\ simp{\isacharunderscore}all%
haftmann@28564
   613
\endisatagquote
haftmann@28564
   614
{\isafoldquote}%
haftmann@28447
   615
%
haftmann@28564
   616
\isadelimquote
haftmann@28447
   617
%
haftmann@28564
   618
\endisadelimquote
haftmann@28447
   619
%
haftmann@28447
   620
\begin{isamarkuptext}%
haftmann@29798
   621
\noindent For completeness, we provide a substitute for the
haftmann@29798
   622
  \isa{case} combinator on queues:%
haftmann@28447
   623
\end{isamarkuptext}%
haftmann@28447
   624
\isamarkuptrue%
haftmann@28447
   625
%
haftmann@28564
   626
\isadelimquote
haftmann@28447
   627
%
haftmann@28564
   628
\endisadelimquote
haftmann@28447
   629
%
haftmann@28564
   630
\isatagquote
haftmann@29798
   631
\isacommand{lemma}\isamarkupfalse%
haftmann@30227
   632
\ queue{\isacharunderscore}case{\isacharunderscore}AQueue\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
haftmann@30227
   633
\ \ {\isachardoublequoteopen}queue{\isacharunderscore}case\ f\ {\isacharparenleft}AQueue\ xs\ ys{\isacharparenright}\ {\isacharequal}\ f\ {\isacharparenleft}ys\ {\isacharat}\ rev\ xs{\isacharparenright}{\isachardoublequoteclose}\isanewline
haftmann@29798
   634
\ \ \isacommand{unfolding}\isamarkupfalse%
haftmann@30227
   635
\ AQueue{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
haftmann@29798
   636
\ simp%
haftmann@28564
   637
\endisatagquote
haftmann@28564
   638
{\isafoldquote}%
haftmann@28447
   639
%
haftmann@28564
   640
\isadelimquote
haftmann@28447
   641
%
haftmann@28564
   642
\endisadelimquote
haftmann@28447
   643
%
haftmann@28447
   644
\begin{isamarkuptext}%
haftmann@29798
   645
\noindent The resulting code looks as expected:%
haftmann@28447
   646
\end{isamarkuptext}%
haftmann@28447
   647
\isamarkuptrue%
haftmann@28447
   648
%
haftmann@28564
   649
\isadelimquote
haftmann@28447
   650
%
haftmann@28564
   651
\endisadelimquote
haftmann@28447
   652
%
haftmann@28564
   653
\isatagquote
haftmann@28447
   654
%
haftmann@28447
   655
\begin{isamarkuptext}%
haftmann@28727
   656
\isatypewriter%
haftmann@28447
   657
\noindent%
haftmann@28714
   658
\hspace*{0pt}structure Example = \\
haftmann@28714
   659
\hspace*{0pt}struct\\
haftmann@28714
   660
\hspace*{0pt}\\
haftmann@29798
   661
\hspace*{0pt}fun foldl f a [] = a\\
haftmann@29798
   662
\hspace*{0pt} ~| foldl f a (x ::~xs) = foldl f (f a x) xs;\\
haftmann@29798
   663
\hspace*{0pt}\\
haftmann@29798
   664
\hspace*{0pt}fun rev xs = foldl (fn xsa => fn x => x ::~xsa) [] xs;\\
haftmann@29798
   665
\hspace*{0pt}\\
haftmann@29798
   666
\hspace*{0pt}fun null [] = true\\
haftmann@29798
   667
\hspace*{0pt} ~| null (x ::~xs) = false;\\
haftmann@28714
   668
\hspace*{0pt}\\
haftmann@29798
   669
\hspace*{0pt}datatype 'a queue = AQueue of 'a list * 'a list;\\
haftmann@29798
   670
\hspace*{0pt}\\
haftmann@29798
   671
\hspace*{0pt}val empty :~'a queue = AQueue ([],~[])\\
haftmann@29798
   672
\hspace*{0pt}\\
haftmann@29798
   673
\hspace*{0pt}fun dequeue (AQueue (xs,~y ::~ys)) = (SOME y,~AQueue (xs,~ys))\\
haftmann@29798
   674
\hspace*{0pt} ~| dequeue (AQueue (xs,~[])) =\\
haftmann@29798
   675
\hspace*{0pt} ~~~(if null xs then (NONE,~AQueue ([],~[]))\\
haftmann@29798
   676
\hspace*{0pt} ~~~~~else dequeue (AQueue ([],~rev xs)));\\
haftmann@29798
   677
\hspace*{0pt}\\
haftmann@29798
   678
\hspace*{0pt}fun enqueue x (AQueue (xs,~ys)) = AQueue (x ::~xs,~ys);\\
haftmann@28714
   679
\hspace*{0pt}\\
wenzelm@29297
   680
\hspace*{0pt}end;~(*struct Example*)%
haftmann@28447
   681
\end{isamarkuptext}%
haftmann@28447
   682
\isamarkuptrue%
haftmann@28447
   683
%
haftmann@28564
   684
\endisatagquote
haftmann@28564
   685
{\isafoldquote}%
haftmann@28447
   686
%
haftmann@28564
   687
\isadelimquote
haftmann@28447
   688
%
haftmann@28564
   689
\endisadelimquote
haftmann@28447
   690
%
haftmann@28447
   691
\begin{isamarkuptext}%
haftmann@29798
   692
\noindent From this example, it can be glimpsed that using own
haftmann@29798
   693
  constructor sets is a little delicate since it changes the set of
haftmann@29798
   694
  valid patterns for values of that type.  Without going into much
haftmann@29798
   695
  detail, here some practical hints:
haftmann@28447
   696
haftmann@28447
   697
  \begin{itemize}
haftmann@29798
   698
haftmann@29798
   699
    \item When changing the constructor set for datatypes, take care
haftmann@30227
   700
      to provide alternative equations for the \isa{case} combinator.
haftmann@29798
   701
haftmann@29798
   702
    \item Values in the target language need not to be normalised --
haftmann@29798
   703
      different values in the target language may represent the same
haftmann@29798
   704
      value in the logic.
haftmann@29798
   705
haftmann@29798
   706
    \item Usually, a good methodology to deal with the subtleties of
haftmann@29798
   707
      pattern matching is to see the type as an abstract type: provide
haftmann@29798
   708
      a set of operations which operate on the concrete representation
haftmann@29798
   709
      of the type, and derive further operations by combinations of
haftmann@29798
   710
      these primitive ones, without relying on a particular
haftmann@29798
   711
      representation.
haftmann@29798
   712
haftmann@28447
   713
  \end{itemize}%
haftmann@28447
   714
\end{isamarkuptext}%
haftmann@28447
   715
\isamarkuptrue%
haftmann@28447
   716
%
haftmann@30938
   717
\isamarkupsubsection{Equality%
haftmann@28447
   718
}
haftmann@28447
   719
\isamarkuptrue%
haftmann@28447
   720
%
haftmann@28447
   721
\begin{isamarkuptext}%
haftmann@28447
   722
Surely you have already noticed how equality is treated
haftmann@28447
   723
  by the code generator:%
haftmann@28447
   724
\end{isamarkuptext}%
haftmann@28447
   725
\isamarkuptrue%
haftmann@28447
   726
%
haftmann@28564
   727
\isadelimquote
haftmann@28447
   728
%
haftmann@28564
   729
\endisadelimquote
haftmann@28447
   730
%
haftmann@28564
   731
\isatagquote
haftmann@28447
   732
\isacommand{primrec}\isamarkupfalse%
haftmann@28447
   733
\ collect{\isacharunderscore}duplicates\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
haftmann@28447
   734
\ \ {\isachardoublequoteopen}collect{\isacharunderscore}duplicates\ xs\ ys\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ xs{\isachardoublequoteclose}\isanewline
haftmann@28447
   735
\ \ {\isacharbar}\ {\isachardoublequoteopen}collect{\isacharunderscore}duplicates\ xs\ ys\ {\isacharparenleft}z{\isacharhash}zs{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ z\ {\isasymin}\ set\ xs\isanewline
haftmann@28447
   736
\ \ \ \ \ \ then\ if\ z\ {\isasymin}\ set\ ys\isanewline
haftmann@28447
   737
\ \ \ \ \ \ \ \ then\ collect{\isacharunderscore}duplicates\ xs\ ys\ zs\isanewline
haftmann@28447
   738
\ \ \ \ \ \ \ \ else\ collect{\isacharunderscore}duplicates\ xs\ {\isacharparenleft}z{\isacharhash}ys{\isacharparenright}\ zs\isanewline
haftmann@28447
   739
\ \ \ \ \ \ else\ collect{\isacharunderscore}duplicates\ {\isacharparenleft}z{\isacharhash}xs{\isacharparenright}\ {\isacharparenleft}z{\isacharhash}ys{\isacharparenright}\ zs{\isacharparenright}{\isachardoublequoteclose}%
haftmann@28564
   740
\endisatagquote
haftmann@28564
   741
{\isafoldquote}%
haftmann@28447
   742
%
haftmann@28564
   743
\isadelimquote
haftmann@28447
   744
%
haftmann@28564
   745
\endisadelimquote
haftmann@28447
   746
%
haftmann@28447
   747
\begin{isamarkuptext}%
haftmann@28447
   748
\noindent The membership test during preprocessing is rewritten,
haftmann@28447
   749
  resulting in \isa{op\ mem}, which itself
haftmann@28447
   750
  performs an explicit equality check.%
haftmann@28447
   751
\end{isamarkuptext}%
haftmann@28447
   752
\isamarkuptrue%
haftmann@28447
   753
%
haftmann@28564
   754
\isadelimquote
haftmann@28447
   755
%
haftmann@28564
   756
\endisadelimquote
haftmann@28447
   757
%
haftmann@28564
   758
\isatagquote
haftmann@28447
   759
%
haftmann@28447
   760
\begin{isamarkuptext}%
haftmann@28727
   761
\isatypewriter%
haftmann@28447
   762
\noindent%
haftmann@28714
   763
\hspace*{0pt}structure Example = \\
haftmann@28714
   764
\hspace*{0pt}struct\\
haftmann@28714
   765
\hspace*{0pt}\\
haftmann@28714
   766
\hspace*{0pt}type 'a eq = {\char123}eq :~'a -> 'a -> bool{\char125};\\
haftmann@28714
   767
\hspace*{0pt}fun eq (A{\char95}:'a eq) = {\char35}eq A{\char95};\\
haftmann@28714
   768
\hspace*{0pt}\\
haftmann@31045
   769
\hspace*{0pt}fun eqa A{\char95}~a b = eq A{\char95}~a b;\\
haftmann@28714
   770
\hspace*{0pt}\\
haftmann@28714
   771
\hspace*{0pt}fun member A{\char95}~x [] = false\\
haftmann@31045
   772
\hspace*{0pt} ~| member A{\char95}~x (y ::~ys) = eqa A{\char95}~x y orelse member A{\char95}~x ys;\\
haftmann@28714
   773
\hspace*{0pt}\\
haftmann@28714
   774
\hspace*{0pt}fun collect{\char95}duplicates A{\char95}~xs ys [] = xs\\
haftmann@28714
   775
\hspace*{0pt} ~| collect{\char95}duplicates A{\char95}~xs ys (z ::~zs) =\\
haftmann@28714
   776
\hspace*{0pt} ~~~(if member A{\char95}~z xs\\
haftmann@28714
   777
\hspace*{0pt} ~~~~~then (if member A{\char95}~z ys then collect{\char95}duplicates A{\char95}~xs ys zs\\
haftmann@28714
   778
\hspace*{0pt} ~~~~~~~~~~~~else collect{\char95}duplicates A{\char95}~xs (z ::~ys) zs)\\
haftmann@28714
   779
\hspace*{0pt} ~~~~~else collect{\char95}duplicates A{\char95}~(z ::~xs) (z ::~ys) zs);\\
haftmann@28714
   780
\hspace*{0pt}\\
wenzelm@29297
   781
\hspace*{0pt}end;~(*struct Example*)%
haftmann@28447
   782
\end{isamarkuptext}%
haftmann@28447
   783
\isamarkuptrue%
haftmann@28447
   784
%
haftmann@28564
   785
\endisatagquote
haftmann@28564
   786
{\isafoldquote}%
haftmann@28447
   787
%
haftmann@28564
   788
\isadelimquote
haftmann@28447
   789
%
haftmann@28564
   790
\endisadelimquote
haftmann@28447
   791
%
haftmann@28447
   792
\begin{isamarkuptext}%
haftmann@28447
   793
\noindent Obviously, polymorphic equality is implemented the Haskell
haftmann@28447
   794
  way using a type class.  How is this achieved?  HOL introduces
haftmann@28447
   795
  an explicit class \isa{eq} with a corresponding operation
haftmann@28447
   796
  \isa{eq{\isacharunderscore}class{\isachardot}eq} such that \isa{eq{\isacharunderscore}class{\isachardot}eq\ {\isacharequal}\ op\ {\isacharequal}}.
haftmann@28447
   797
  The preprocessing framework does the rest by propagating the
haftmann@29560
   798
  \isa{eq} constraints through all dependent code equations.
haftmann@28447
   799
  For datatypes, instances of \isa{eq} are implicitly derived
haftmann@28447
   800
  when possible.  For other types, you may instantiate \isa{eq}
haftmann@28447
   801
  manually like any other type class.
haftmann@28447
   802
haftmann@28447
   803
  Though this \isa{eq} class is designed to get rarely in
haftmann@30938
   804
  the way, in some cases the automatically derived code equations
haftmann@28447
   805
  for equality on a particular type may not be appropriate.
haftmann@28447
   806
  As example, watch the following datatype representing
haftmann@28447
   807
  monomorphic parametric types (where type constructors
haftmann@28447
   808
  are referred to by natural numbers):%
haftmann@28447
   809
\end{isamarkuptext}%
haftmann@28447
   810
\isamarkuptrue%
haftmann@28447
   811
%
haftmann@28564
   812
\isadelimquote
haftmann@28447
   813
%
haftmann@28564
   814
\endisadelimquote
haftmann@28447
   815
%
haftmann@28564
   816
\isatagquote
haftmann@28447
   817
\isacommand{datatype}\isamarkupfalse%
haftmann@28447
   818
\ monotype\ {\isacharequal}\ Mono\ nat\ {\isachardoublequoteopen}monotype\ list{\isachardoublequoteclose}%
haftmann@28564
   819
\endisatagquote
haftmann@28564
   820
{\isafoldquote}%
haftmann@28447
   821
%
haftmann@28564
   822
\isadelimquote
haftmann@28447
   823
%
haftmann@28564
   824
\endisadelimquote
haftmann@28447
   825
%
haftmann@28447
   826
\isadelimproof
haftmann@28447
   827
%
haftmann@28447
   828
\endisadelimproof
haftmann@28447
   829
%
haftmann@28447
   830
\isatagproof
haftmann@28447
   831
%
haftmann@28447
   832
\endisatagproof
haftmann@28447
   833
{\isafoldproof}%
haftmann@28447
   834
%
haftmann@28447
   835
\isadelimproof
haftmann@28447
   836
%
haftmann@28447
   837
\endisadelimproof
haftmann@28447
   838
%
haftmann@28447
   839
\begin{isamarkuptext}%
haftmann@28462
   840
\noindent Then code generation for SML would fail with a message
haftmann@28447
   841
  that the generated code contains illegal mutual dependencies:
haftmann@28462
   842
  the theorem \isa{eq{\isacharunderscore}class{\isachardot}eq\ {\isacharparenleft}Mono\ tyco{\isadigit{1}}\ typargs{\isadigit{1}}{\isacharparenright}\ {\isacharparenleft}Mono\ tyco{\isadigit{2}}\ typargs{\isadigit{2}}{\isacharparenright}\ {\isasymequiv}\ eq{\isacharunderscore}class{\isachardot}eq\ tyco{\isadigit{1}}\ tyco{\isadigit{2}}\ {\isasymand}\ eq{\isacharunderscore}class{\isachardot}eq\ typargs{\isadigit{1}}\ typargs{\isadigit{2}}} already requires the
haftmann@28447
   843
  instance \isa{monotype\ {\isasymColon}\ eq}, which itself requires
haftmann@28462
   844
  \isa{eq{\isacharunderscore}class{\isachardot}eq\ {\isacharparenleft}Mono\ tyco{\isadigit{1}}\ typargs{\isadigit{1}}{\isacharparenright}\ {\isacharparenleft}Mono\ tyco{\isadigit{2}}\ typargs{\isadigit{2}}{\isacharparenright}\ {\isasymequiv}\ eq{\isacharunderscore}class{\isachardot}eq\ tyco{\isadigit{1}}\ tyco{\isadigit{2}}\ {\isasymand}\ eq{\isacharunderscore}class{\isachardot}eq\ typargs{\isadigit{1}}\ typargs{\isadigit{2}}};  Haskell has no problem with mutually
haftmann@28462
   845
  recursive \isa{instance} and \isa{function} definitions,
haftmann@28593
   846
  but the SML serialiser does not support this.
haftmann@28447
   847
haftmann@28447
   848
  In such cases, you have to provide your own equality equations
haftmann@28447
   849
  involving auxiliary constants.  In our case,
haftmann@28447
   850
  \isa{list{\isacharunderscore}all{\isadigit{2}}} can do the job:%
haftmann@28447
   851
\end{isamarkuptext}%
haftmann@28447
   852
\isamarkuptrue%
haftmann@28447
   853
%
haftmann@28564
   854
\isadelimquote
haftmann@28447
   855
%
haftmann@28564
   856
\endisadelimquote
haftmann@28447
   857
%
haftmann@28564
   858
\isatagquote
haftmann@28447
   859
\isacommand{lemma}\isamarkupfalse%
haftmann@28562
   860
\ monotype{\isacharunderscore}eq{\isacharunderscore}list{\isacharunderscore}all{\isadigit{2}}\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
haftmann@28447
   861
\ \ {\isachardoublequoteopen}eq{\isacharunderscore}class{\isachardot}eq\ {\isacharparenleft}Mono\ tyco{\isadigit{1}}\ typargs{\isadigit{1}}{\isacharparenright}\ {\isacharparenleft}Mono\ tyco{\isadigit{2}}\ typargs{\isadigit{2}}{\isacharparenright}\ {\isasymlongleftrightarrow}\isanewline
haftmann@28462
   862
\ \ \ \ \ eq{\isacharunderscore}class{\isachardot}eq\ tyco{\isadigit{1}}\ tyco{\isadigit{2}}\ {\isasymand}\ list{\isacharunderscore}all{\isadigit{2}}\ eq{\isacharunderscore}class{\isachardot}eq\ typargs{\isadigit{1}}\ typargs{\isadigit{2}}{\isachardoublequoteclose}\isanewline
haftmann@28447
   863
\ \ \isacommand{by}\isamarkupfalse%
haftmann@28447
   864
\ {\isacharparenleft}simp\ add{\isacharcolon}\ eq\ list{\isacharunderscore}all{\isadigit{2}}{\isacharunderscore}eq\ {\isacharbrackleft}symmetric{\isacharbrackright}{\isacharparenright}%
haftmann@28564
   865
\endisatagquote
haftmann@28564
   866
{\isafoldquote}%
haftmann@28447
   867
%
haftmann@28564
   868
\isadelimquote
haftmann@28447
   869
%
haftmann@28564
   870
\endisadelimquote
haftmann@28447
   871
%
haftmann@28447
   872
\begin{isamarkuptext}%
haftmann@28447
   873
\noindent does not depend on instance \isa{monotype\ {\isasymColon}\ eq}:%
haftmann@28447
   874
\end{isamarkuptext}%
haftmann@28447
   875
\isamarkuptrue%
haftmann@28447
   876
%
haftmann@28564
   877
\isadelimquote
haftmann@28447
   878
%
haftmann@28564
   879
\endisadelimquote
haftmann@28447
   880
%
haftmann@28564
   881
\isatagquote
haftmann@28447
   882
%
haftmann@28447
   883
\begin{isamarkuptext}%
haftmann@28727
   884
\isatypewriter%
haftmann@28447
   885
\noindent%
haftmann@28714
   886
\hspace*{0pt}structure Example = \\
haftmann@28714
   887
\hspace*{0pt}struct\\
haftmann@28714
   888
\hspace*{0pt}\\
wenzelm@30121
   889
\hspace*{0pt}datatype nat = Zero{\char95}nat | Suc of nat;\\
haftmann@28714
   890
\hspace*{0pt}\\
haftmann@28714
   891
\hspace*{0pt}fun null [] = true\\
haftmann@28714
   892
\hspace*{0pt} ~| null (x ::~xs) = false;\\
haftmann@28714
   893
\hspace*{0pt}\\
haftmann@31150
   894
\hspace*{0pt}fun eq{\char95}nat (Suc nat') Zero{\char95}nat = false\\
haftmann@31150
   895
\hspace*{0pt} ~| eq{\char95}nat Zero{\char95}nat (Suc nat') = false\\
haftmann@28714
   896
\hspace*{0pt} ~| eq{\char95}nat (Suc nat) (Suc nat') = eq{\char95}nat nat nat'\\
haftmann@28714
   897
\hspace*{0pt} ~| eq{\char95}nat Zero{\char95}nat Zero{\char95}nat = true;\\
haftmann@28714
   898
\hspace*{0pt}\\
haftmann@28714
   899
\hspace*{0pt}datatype monotype = Mono of nat * monotype list;\\
haftmann@28714
   900
\hspace*{0pt}\\
haftmann@28714
   901
\hspace*{0pt}fun list{\char95}all2 p (x ::~xs) (y ::~ys) = p x y andalso list{\char95}all2 p xs ys\\
haftmann@28714
   902
\hspace*{0pt} ~| list{\char95}all2 p xs [] = null xs\\
haftmann@28714
   903
\hspace*{0pt} ~| list{\char95}all2 p [] ys = null ys;\\
haftmann@28714
   904
\hspace*{0pt}\\
wenzelm@29297
   905
\hspace*{0pt}fun eq{\char95}monotype (Mono (tyco1,~typargs1)) (Mono (tyco2,~typargs2)) =\\
haftmann@28714
   906
\hspace*{0pt} ~eq{\char95}nat tyco1 tyco2 andalso list{\char95}all2 eq{\char95}monotype typargs1 typargs2;\\
haftmann@28714
   907
\hspace*{0pt}\\
wenzelm@29297
   908
\hspace*{0pt}end;~(*struct Example*)%
haftmann@28447
   909
\end{isamarkuptext}%
haftmann@28447
   910
\isamarkuptrue%
haftmann@28447
   911
%
haftmann@28564
   912
\endisatagquote
haftmann@28564
   913
{\isafoldquote}%
haftmann@28447
   914
%
haftmann@28564
   915
\isadelimquote
haftmann@28447
   916
%
haftmann@28564
   917
\endisadelimquote
haftmann@28447
   918
%
haftmann@28462
   919
\isamarkupsubsection{Explicit partiality%
haftmann@28447
   920
}
haftmann@28447
   921
\isamarkuptrue%
haftmann@28447
   922
%
haftmann@28447
   923
\begin{isamarkuptext}%
haftmann@28462
   924
Partiality usually enters the game by partial patterns, as
haftmann@28462
   925
  in the following example, again for amortised queues:%
haftmann@28462
   926
\end{isamarkuptext}%
haftmann@28462
   927
\isamarkuptrue%
haftmann@28462
   928
%
haftmann@28564
   929
\isadelimquote
haftmann@28462
   930
%
haftmann@28564
   931
\endisadelimquote
haftmann@28462
   932
%
haftmann@28564
   933
\isatagquote
haftmann@29798
   934
\isacommand{definition}\isamarkupfalse%
haftmann@28462
   935
\ strict{\isacharunderscore}dequeue\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ queue\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
haftmann@29798
   936
\ \ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue\ q\ {\isacharequal}\ {\isacharparenleft}case\ dequeue\ q\isanewline
haftmann@29798
   937
\ \ \ \ of\ {\isacharparenleft}Some\ x{\isacharcomma}\ q{\isacharprime}{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}x{\isacharcomma}\ q{\isacharprime}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
haftmann@29798
   938
\isanewline
haftmann@29798
   939
\isacommand{lemma}\isamarkupfalse%
haftmann@29798
   940
\ strict{\isacharunderscore}dequeue{\isacharunderscore}AQueue\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
haftmann@29798
   941
\ \ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharparenleft}y\ {\isacharhash}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}y{\isacharcomma}\ AQueue\ xs\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline
haftmann@29798
   942
\ \ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\isanewline
haftmann@29798
   943
\ \ \ \ {\isacharparenleft}case\ rev\ xs\ of\ y\ {\isacharhash}\ ys\ {\isasymRightarrow}\ {\isacharparenleft}y{\isacharcomma}\ AQueue\ {\isacharbrackleft}{\isacharbrackright}\ ys{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
haftmann@29798
   944
\ \ \isacommand{by}\isamarkupfalse%
haftmann@29798
   945
\ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ strict{\isacharunderscore}dequeue{\isacharunderscore}def\ dequeue{\isacharunderscore}AQueue\ split{\isacharcolon}\ list{\isachardot}splits{\isacharparenright}%
haftmann@28564
   946
\endisatagquote
haftmann@28564
   947
{\isafoldquote}%
haftmann@28462
   948
%
haftmann@28564
   949
\isadelimquote
haftmann@28462
   950
%
haftmann@28564
   951
\endisadelimquote
haftmann@28462
   952
%
haftmann@28462
   953
\begin{isamarkuptext}%
haftmann@28462
   954
\noindent In the corresponding code, there is no equation
haftmann@30227
   955
  for the pattern \isa{AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}}:%
haftmann@28462
   956
\end{isamarkuptext}%
haftmann@28462
   957
\isamarkuptrue%
haftmann@28462
   958
%
haftmann@28564
   959
\isadelimquote
haftmann@28462
   960
%
haftmann@28564
   961
\endisadelimquote
haftmann@28462
   962
%
haftmann@28564
   963
\isatagquote
haftmann@28462
   964
%
haftmann@28462
   965
\begin{isamarkuptext}%
haftmann@28727
   966
\isatypewriter%
haftmann@28462
   967
\noindent%
wenzelm@29297
   968
\hspace*{0pt}strict{\char95}dequeue ::~forall a.~Queue a -> (a,~Queue a);\\
haftmann@29798
   969
\hspace*{0pt}strict{\char95}dequeue (AQueue xs []) =\\
haftmann@28714
   970
\hspace*{0pt} ~let {\char123}\\
haftmann@28714
   971
\hspace*{0pt} ~~~(y :~ys) = rev xs;\\
haftmann@29798
   972
\hspace*{0pt} ~{\char125}~in (y,~AQueue [] ys);\\
haftmann@29798
   973
\hspace*{0pt}strict{\char95}dequeue (AQueue xs (y :~ys)) = (y,~AQueue xs ys);%
haftmann@28462
   974
\end{isamarkuptext}%
haftmann@28462
   975
\isamarkuptrue%
haftmann@28462
   976
%
haftmann@28564
   977
\endisatagquote
haftmann@28564
   978
{\isafoldquote}%
haftmann@28462
   979
%
haftmann@28564
   980
\isadelimquote
haftmann@28462
   981
%
haftmann@28564
   982
\endisadelimquote
haftmann@28462
   983
%
haftmann@28462
   984
\begin{isamarkuptext}%
haftmann@28462
   985
\noindent In some cases it is desirable to have this
haftmann@28462
   986
  pseudo-\qt{partiality} more explicitly, e.g.~as follows:%
haftmann@28462
   987
\end{isamarkuptext}%
haftmann@28462
   988
\isamarkuptrue%
haftmann@28462
   989
%
haftmann@28564
   990
\isadelimquote
haftmann@28462
   991
%
haftmann@28564
   992
\endisadelimquote
haftmann@28462
   993
%
haftmann@28564
   994
\isatagquote
haftmann@28462
   995
\isacommand{axiomatization}\isamarkupfalse%
haftmann@28462
   996
\ empty{\isacharunderscore}queue\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\isanewline
haftmann@28462
   997
\isanewline
haftmann@29798
   998
\isacommand{definition}\isamarkupfalse%
haftmann@28462
   999
\ strict{\isacharunderscore}dequeue{\isacharprime}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ queue\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
haftmann@29798
  1000
\ \ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue{\isacharprime}\ q\ {\isacharequal}\ {\isacharparenleft}case\ dequeue\ q\ of\ {\isacharparenleft}Some\ x{\isacharcomma}\ q{\isacharprime}{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}x{\isacharcomma}\ q{\isacharprime}{\isacharparenright}\ {\isacharbar}\ {\isacharunderscore}\ {\isasymRightarrow}\ empty{\isacharunderscore}queue{\isacharparenright}{\isachardoublequoteclose}\isanewline
haftmann@28462
  1001
\isanewline
haftmann@29798
  1002
\isacommand{lemma}\isamarkupfalse%
haftmann@29798
  1003
\ strict{\isacharunderscore}dequeue{\isacharprime}{\isacharunderscore}AQueue\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
haftmann@29798
  1004
\ \ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue{\isacharprime}\ {\isacharparenleft}AQueue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ then\ empty{\isacharunderscore}queue\isanewline
haftmann@29798
  1005
\ \ \ \ \ else\ strict{\isacharunderscore}dequeue{\isacharprime}\ {\isacharparenleft}AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharparenleft}rev\ xs{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
haftmann@29798
  1006
\ \ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue{\isacharprime}\ {\isacharparenleft}AQueue\ xs\ {\isacharparenleft}y\ {\isacharhash}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\isanewline
haftmann@29798
  1007
\ \ \ \ \ {\isacharparenleft}y{\isacharcomma}\ AQueue\ xs\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline
haftmann@29798
  1008
\ \ \isacommand{by}\isamarkupfalse%
haftmann@29798
  1009
\ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ strict{\isacharunderscore}dequeue{\isacharprime}{\isacharunderscore}def\ dequeue{\isacharunderscore}AQueue\ split{\isacharcolon}\ list{\isachardot}splits{\isacharparenright}%
haftmann@28564
  1010
\endisatagquote
haftmann@28564
  1011
{\isafoldquote}%
haftmann@28462
  1012
%
haftmann@28564
  1013
\isadelimquote
haftmann@28462
  1014
%
haftmann@28564
  1015
\endisadelimquote
haftmann@28462
  1016
%
haftmann@28462
  1017
\begin{isamarkuptext}%
haftmann@29798
  1018
Observe that on the right hand side of the definition of \isa{strict{\isacharunderscore}dequeue{\isacharprime}} the constant \isa{empty{\isacharunderscore}queue} occurs
haftmann@29798
  1019
  which is unspecified.
haftmann@28462
  1020
haftmann@29798
  1021
  Normally, if constants without any code equations occur in a
haftmann@29798
  1022
  program, the code generator complains (since in most cases this is
haftmann@29798
  1023
  not what the user expects).  But such constants can also be thought
haftmann@29798
  1024
  of as function definitions with no equations which always fail,
haftmann@29798
  1025
  since there is never a successful pattern match on the left hand
haftmann@29798
  1026
  side.  In order to categorise a constant into that category
haftmann@29798
  1027
  explicitly, use \hyperlink{command.code-abort}{\mbox{\isa{\isacommand{code{\isacharunderscore}abort}}}}:%
haftmann@28462
  1028
\end{isamarkuptext}%
haftmann@28462
  1029
\isamarkuptrue%
haftmann@28462
  1030
%
haftmann@28564
  1031
\isadelimquote
haftmann@28462
  1032
%
haftmann@28564
  1033
\endisadelimquote
haftmann@28462
  1034
%
haftmann@28564
  1035
\isatagquote
haftmann@28462
  1036
\isacommand{code{\isacharunderscore}abort}\isamarkupfalse%
haftmann@28462
  1037
\ empty{\isacharunderscore}queue%
haftmann@28564
  1038
\endisatagquote
haftmann@28564
  1039
{\isafoldquote}%
haftmann@28462
  1040
%
haftmann@28564
  1041
\isadelimquote
haftmann@28462
  1042
%
haftmann@28564
  1043
\endisadelimquote
haftmann@28462
  1044
%
haftmann@28462
  1045
\begin{isamarkuptext}%
haftmann@28462
  1046
\noindent Then the code generator will just insert an error or
haftmann@28462
  1047
  exception at the appropriate position:%
haftmann@28462
  1048
\end{isamarkuptext}%
haftmann@28462
  1049
\isamarkuptrue%
haftmann@28462
  1050
%
haftmann@28564
  1051
\isadelimquote
haftmann@28462
  1052
%
haftmann@28564
  1053
\endisadelimquote
haftmann@28462
  1054
%
haftmann@28564
  1055
\isatagquote
haftmann@28462
  1056
%
haftmann@28462
  1057
\begin{isamarkuptext}%
haftmann@28727
  1058
\isatypewriter%
haftmann@28462
  1059
\noindent%
wenzelm@29297
  1060
\hspace*{0pt}empty{\char95}queue ::~forall a.~a;\\
haftmann@28714
  1061
\hspace*{0pt}empty{\char95}queue = error {\char34}empty{\char95}queue{\char34};\\
haftmann@28714
  1062
\hspace*{0pt}\\
wenzelm@29297
  1063
\hspace*{0pt}strict{\char95}dequeue' ::~forall a.~Queue a -> (a,~Queue a);\\
haftmann@29798
  1064
\hspace*{0pt}strict{\char95}dequeue' (AQueue xs (y :~ys)) = (y,~AQueue xs ys);\\
haftmann@29798
  1065
\hspace*{0pt}strict{\char95}dequeue' (AQueue xs []) =\\
haftmann@29798
  1066
\hspace*{0pt} ~(if nulla xs then empty{\char95}queue\\
haftmann@29798
  1067
\hspace*{0pt} ~~~else strict{\char95}dequeue' (AQueue [] (rev xs)));%
haftmann@28462
  1068
\end{isamarkuptext}%
haftmann@28462
  1069
\isamarkuptrue%
haftmann@28462
  1070
%
haftmann@28564
  1071
\endisatagquote
haftmann@28564
  1072
{\isafoldquote}%
haftmann@28462
  1073
%
haftmann@28564
  1074
\isadelimquote
haftmann@28462
  1075
%
haftmann@28564
  1076
\endisadelimquote
haftmann@28462
  1077
%
haftmann@28462
  1078
\begin{isamarkuptext}%
haftmann@28462
  1079
\noindent This feature however is rarely needed in practice.
haftmann@28462
  1080
  Note also that the \isa{HOL} default setup already declares
haftmann@28462
  1081
  \isa{undefined} as \hyperlink{command.code-abort}{\mbox{\isa{\isacommand{code{\isacharunderscore}abort}}}}, which is most
haftmann@28462
  1082
  likely to be used in such situations.%
haftmann@28447
  1083
\end{isamarkuptext}%
haftmann@28447
  1084
\isamarkuptrue%
haftmann@28447
  1085
%
haftmann@28447
  1086
\isadelimtheory
haftmann@28447
  1087
%
haftmann@28447
  1088
\endisadelimtheory
haftmann@28447
  1089
%
haftmann@28447
  1090
\isatagtheory
haftmann@28447
  1091
\isacommand{end}\isamarkupfalse%
haftmann@28447
  1092
%
haftmann@28447
  1093
\endisatagtheory
haftmann@28447
  1094
{\isafoldtheory}%
haftmann@28447
  1095
%
haftmann@28447
  1096
\isadelimtheory
haftmann@28447
  1097
%
haftmann@28447
  1098
\endisadelimtheory
haftmann@28447
  1099
\isanewline
haftmann@28462
  1100
\ \end{isabellebody}%
haftmann@28447
  1101
%%% Local Variables:
haftmann@28447
  1102
%%% mode: latex
haftmann@28447
  1103
%%% TeX-master: "root"
haftmann@28447
  1104
%%% End: