doc-src/IsarAdvanced/Codegen/Thy/Program.thy
author haftmann
Wed Oct 01 13:33:54 2008 +0200 (2008-10-01)
changeset 28447 df77ed974a78
parent 28428 fd007794561f
child 28456 7a558c872104
permissions -rw-r--r--
fixed
haftmann@28213
     1
theory Program
haftmann@28419
     2
imports Introduction
haftmann@28213
     3
begin
haftmann@28213
     4
haftmann@28419
     5
section {* Turning Theories into Programs \label{sec:program} *}
haftmann@28213
     6
haftmann@28213
     7
subsection {* The @{text "Isabelle/HOL"} default setup *}
haftmann@28213
     8
haftmann@28419
     9
text {*
haftmann@28419
    10
  We have already seen how by default equations stemming from
haftmann@28419
    11
  @{command definition}/@{command primrec}/@{command fun}
haftmann@28447
    12
  statements are used for code generation.  This default behaviour
haftmann@28447
    13
  can be changed, e.g. by providing different defining equations.
haftmann@28447
    14
  All kinds of customization shown in this section is \emph{safe}
haftmann@28447
    15
  in the sense that the user does not have to worry about
haftmann@28447
    16
  correctness -- all programs generatable that way are partially
haftmann@28447
    17
  correct.
haftmann@28447
    18
*}
haftmann@28447
    19
haftmann@28447
    20
subsection {* Selecting code equations *}
haftmann@28447
    21
haftmann@28447
    22
text {*
haftmann@28447
    23
  Coming back to our introductory example, we
haftmann@28447
    24
  could provide an alternative defining equations for @{const dequeue}
haftmann@28447
    25
  explicitly:
haftmann@28419
    26
*}
haftmann@28419
    27
haftmann@28419
    28
lemma %quoteme [code func]:
haftmann@28447
    29
  "dequeue (Queue xs []) =
haftmann@28447
    30
     (if xs = [] then (None, Queue [] []) else dequeue (Queue [] (rev xs)))"
haftmann@28447
    31
  "dequeue (Queue xs (y # ys)) =
haftmann@28447
    32
     (Some y, Queue xs ys)"
haftmann@28419
    33
  by (cases xs, simp_all) (cases "rev xs", simp_all)
haftmann@28419
    34
haftmann@28419
    35
text {*
haftmann@28419
    36
  \noindent The annotation @{text "[code func]"} is an @{text Isar}
haftmann@28419
    37
  @{text attribute} which states that the given theorems should be
haftmann@28419
    38
  considered as defining equations for a @{text fun} statement --
haftmann@28419
    39
  the corresponding constant is determined syntactically.  The resulting code:
haftmann@28419
    40
*}
haftmann@28419
    41
haftmann@28419
    42
text %quoteme {*@{code_stmts empty enqueue dequeue (Haskell)}*}
haftmann@28419
    43
haftmann@28419
    44
text {*
haftmann@28419
    45
  \noindent You may note that the equality test @{term "xs = []"} has been
haftmann@28419
    46
  replaced by the predicate @{term "null xs"}.  This is due to the default
haftmann@28419
    47
  setup in the \qn{preprocessor} to be discussed further below (\secref{sec:preproc}).
haftmann@28419
    48
haftmann@28419
    49
  Changing the default constructor set of datatypes is also
haftmann@28419
    50
  possible but rarely desired in practice.  See \secref{sec:datatypes} for an example.
haftmann@28419
    51
haftmann@28419
    52
  As told in \secref{sec:concept}, code generation is based
haftmann@28419
    53
  on a structured collection of code theorems.
haftmann@28419
    54
  For explorative purpose, this collection
haftmann@28419
    55
  may be inspected using the @{command code_thms} command:
haftmann@28419
    56
*}
haftmann@28419
    57
haftmann@28419
    58
code_thms %quoteme dequeue
haftmann@28419
    59
haftmann@28419
    60
text {*
haftmann@28419
    61
  \noindent prints a table with \emph{all} defining equations
haftmann@28419
    62
  for @{const dequeue}, including
haftmann@28419
    63
  \emph{all} defining equations those equations depend
haftmann@28419
    64
  on recursively.
haftmann@28419
    65
  
haftmann@28419
    66
  Similarly, the @{command code_deps} command shows a graph
haftmann@28419
    67
  visualising dependencies between defining equations.
haftmann@28419
    68
*}
haftmann@28419
    69
haftmann@28419
    70
subsection {* @{text class} and @{text instantiation} *}
haftmann@28419
    71
haftmann@28419
    72
text {*
haftmann@28447
    73
  Concerning type classes and code generation, let us examine an example
haftmann@28419
    74
  from abstract algebra:
haftmann@28419
    75
*}
haftmann@28419
    76
haftmann@28419
    77
class %quoteme semigroup = type +
haftmann@28419
    78
  fixes mult :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<otimes>" 70)
haftmann@28419
    79
  assumes assoc: "(x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)"
haftmann@28419
    80
haftmann@28419
    81
class %quoteme monoid = semigroup +
haftmann@28419
    82
  fixes neutral :: 'a ("\<one>")
haftmann@28419
    83
  assumes neutl: "\<one> \<otimes> x = x"
haftmann@28419
    84
    and neutr: "x \<otimes> \<one> = x"
haftmann@28419
    85
haftmann@28419
    86
instantiation %quoteme nat :: monoid
haftmann@28419
    87
begin
haftmann@28419
    88
haftmann@28419
    89
primrec %quoteme mult_nat where
haftmann@28419
    90
    "0 \<otimes> n = (0\<Colon>nat)"
haftmann@28419
    91
  | "Suc m \<otimes> n = n + m \<otimes> n"
haftmann@28419
    92
haftmann@28419
    93
definition %quoteme neutral_nat where
haftmann@28419
    94
  "\<one> = Suc 0"
haftmann@28213
    95
haftmann@28419
    96
lemma %quoteme add_mult_distrib:
haftmann@28419
    97
  fixes n m q :: nat
haftmann@28419
    98
  shows "(n + m) \<otimes> q = n \<otimes> q + m \<otimes> q"
haftmann@28419
    99
  by (induct n) simp_all
haftmann@28419
   100
haftmann@28419
   101
instance %quoteme proof
haftmann@28419
   102
  fix m n q :: nat
haftmann@28419
   103
  show "m \<otimes> n \<otimes> q = m \<otimes> (n \<otimes> q)"
haftmann@28419
   104
    by (induct m) (simp_all add: add_mult_distrib)
haftmann@28419
   105
  show "\<one> \<otimes> n = n"
haftmann@28419
   106
    by (simp add: neutral_nat_def)
haftmann@28419
   107
  show "m \<otimes> \<one> = m"
haftmann@28419
   108
    by (induct m) (simp_all add: neutral_nat_def)
haftmann@28419
   109
qed
haftmann@28419
   110
haftmann@28419
   111
end %quoteme
haftmann@28419
   112
haftmann@28419
   113
text {*
haftmann@28419
   114
  \noindent We define the natural operation of the natural numbers
haftmann@28419
   115
  on monoids:
haftmann@28419
   116
*}
haftmann@28419
   117
haftmann@28447
   118
primrec %quoteme (in monoid) pow :: "nat \<Rightarrow> 'a \<Rightarrow> 'a" where
haftmann@28419
   119
    "pow 0 a = \<one>"
haftmann@28419
   120
  | "pow (Suc n) a = a \<otimes> pow n a"
haftmann@28419
   121
haftmann@28419
   122
text {*
haftmann@28419
   123
  \noindent This we use to define the discrete exponentiation function:
haftmann@28419
   124
*}
haftmann@28419
   125
haftmann@28419
   126
definition %quoteme bexp :: "nat \<Rightarrow> nat" where
haftmann@28419
   127
  "bexp n = pow n (Suc (Suc 0))"
haftmann@28419
   128
haftmann@28419
   129
text {*
haftmann@28419
   130
  \noindent The corresponding code:
haftmann@28419
   131
*}
haftmann@28419
   132
haftmann@28419
   133
text %quoteme {*@{code_stmts bexp (Haskell)}*}
haftmann@28419
   134
haftmann@28419
   135
text {*
haftmann@28447
   136
  \noindent This is a convenient place to show how explicit dictionary construction
haftmann@28419
   137
  manifests in generated code (here, the same example in @{text SML}):
haftmann@28419
   138
*}
haftmann@28419
   139
haftmann@28419
   140
text %quoteme {*@{code_stmts bexp (SML)}*}
haftmann@28419
   141
haftmann@28447
   142
text {*
haftmann@28447
   143
  \noindent Note the parameters with trailing underscore (@{verbatim "A_"})
haftmann@28447
   144
    which are the dictionary parameters.
haftmann@28447
   145
*}
haftmann@28419
   146
haftmann@28419
   147
subsection {* The preprocessor \label{sec:preproc} *}
haftmann@28419
   148
haftmann@28419
   149
text {*
haftmann@28419
   150
  Before selected function theorems are turned into abstract
haftmann@28419
   151
  code, a chain of definitional transformation steps is carried
haftmann@28419
   152
  out: \emph{preprocessing}.  In essence, the preprocessor
haftmann@28419
   153
  consists of two components: a \emph{simpset} and \emph{function transformers}.
haftmann@28419
   154
haftmann@28419
   155
  The \emph{simpset} allows to employ the full generality of the Isabelle
haftmann@28419
   156
  simplifier.  Due to the interpretation of theorems
haftmann@28419
   157
  as defining equations, rewrites are applied to the right
haftmann@28419
   158
  hand side and the arguments of the left hand side of an
haftmann@28419
   159
  equation, but never to the constant heading the left hand side.
haftmann@28419
   160
  An important special case are \emph{inline theorems} which may be
haftmann@28419
   161
  declared and undeclared using the
haftmann@28419
   162
  \emph{code inline} or \emph{code inline del} attribute respectively.
haftmann@28213
   163
haftmann@28419
   164
  Some common applications:
haftmann@28419
   165
*}
haftmann@28419
   166
haftmann@28419
   167
text_raw {*
haftmann@28419
   168
  \begin{itemize}
haftmann@28419
   169
*}
haftmann@28419
   170
haftmann@28419
   171
text {*
haftmann@28419
   172
     \item replacing non-executable constructs by executable ones:
haftmann@28419
   173
*}     
haftmann@28419
   174
haftmann@28419
   175
lemma %quoteme [code inline]:
haftmann@28419
   176
  "x \<in> set xs \<longleftrightarrow> x mem xs" by (induct xs) simp_all
haftmann@28419
   177
haftmann@28419
   178
text {*
haftmann@28419
   179
     \item eliminating superfluous constants:
haftmann@28419
   180
*}
haftmann@28419
   181
haftmann@28419
   182
lemma %quoteme [code inline]:
haftmann@28419
   183
  "1 = Suc 0" by simp
haftmann@28419
   184
haftmann@28419
   185
text {*
haftmann@28419
   186
     \item replacing executable but inconvenient constructs:
haftmann@28419
   187
*}
haftmann@28419
   188
haftmann@28419
   189
lemma %quoteme [code inline]:
haftmann@28419
   190
  "xs = [] \<longleftrightarrow> List.null xs" by (induct xs) simp_all
haftmann@28419
   191
haftmann@28419
   192
text_raw {*
haftmann@28419
   193
  \end{itemize}
haftmann@28419
   194
*}
haftmann@28419
   195
haftmann@28419
   196
text {*
haftmann@28447
   197
  \noindent \emph{Function transformers} provide a very general interface,
haftmann@28419
   198
  transforming a list of function theorems to another
haftmann@28419
   199
  list of function theorems, provided that neither the heading
haftmann@28419
   200
  constant nor its type change.  The @{term "0\<Colon>nat"} / @{const Suc}
haftmann@28419
   201
  pattern elimination implemented in
haftmann@28419
   202
  theory @{text Efficient_Nat} (see \secref{eff_nat}) uses this
haftmann@28419
   203
  interface.
haftmann@28419
   204
haftmann@28419
   205
  \noindent The current setup of the preprocessor may be inspected using
haftmann@28419
   206
  the @{command print_codesetup} command.
haftmann@28419
   207
  @{command code_thms} provides a convenient
haftmann@28419
   208
  mechanism to inspect the impact of a preprocessor setup
haftmann@28419
   209
  on defining equations.
haftmann@28419
   210
haftmann@28419
   211
  \begin{warn}
haftmann@28419
   212
    The attribute \emph{code unfold}
haftmann@28447
   213
    associated with the @{text "SML code generator"} also applies to
haftmann@28447
   214
    the @{text "generic code generator"}:
haftmann@28447
   215
    \emph{code unfold} implies \emph{code inline}.
haftmann@28419
   216
  \end{warn}
haftmann@28419
   217
*}
haftmann@28419
   218
haftmann@28419
   219
subsection {* Datatypes \label{sec:datatypes} *}
haftmann@28419
   220
haftmann@28419
   221
text {*
haftmann@28419
   222
  Conceptually, any datatype is spanned by a set of
haftmann@28419
   223
  \emph{constructors} of type @{text "\<tau> = \<dots> \<Rightarrow> \<kappa> \<alpha>\<^isub>1 \<dots> \<alpha>\<^isub>n"}
haftmann@28419
   224
  where @{text "{\<alpha>\<^isub>1, \<dots>, \<alpha>\<^isub>n}"} is excactly the set of \emph{all}
haftmann@28419
   225
  type variables in @{text "\<tau>"}.  The HOL datatype package
haftmann@28419
   226
  by default registers any new datatype in the table
haftmann@28419
   227
  of datatypes, which may be inspected using
haftmann@28419
   228
  the @{command print_codesetup} command.
haftmann@28419
   229
haftmann@28419
   230
  In some cases, it may be convenient to alter or
haftmann@28419
   231
  extend this table;  as an example, we will develop an alternative
haftmann@28419
   232
  representation of natural numbers as binary digits, whose
haftmann@28419
   233
  size does increase logarithmically with its value, not linear
haftmann@28419
   234
  \footnote{Indeed, the @{theory Efficient_Nat} theory (see \ref{eff_nat})
haftmann@28419
   235
    does something similar}.  First, the digit representation:
haftmann@28419
   236
*}
haftmann@28419
   237
haftmann@28419
   238
definition %quoteme Dig0 :: "nat \<Rightarrow> nat" where
haftmann@28419
   239
  "Dig0 n = 2 * n"
haftmann@28419
   240
haftmann@28419
   241
definition %quoteme  Dig1 :: "nat \<Rightarrow> nat" where
haftmann@28419
   242
  "Dig1 n = Suc (2 * n)"
haftmann@28213
   243
haftmann@28419
   244
text {*
haftmann@28447
   245
  \noindent We will use these two \qt{digits} to represent natural numbers
haftmann@28419
   246
  in binary digits, e.g.:
haftmann@28419
   247
*}
haftmann@28419
   248
haftmann@28419
   249
lemma %quoteme 42: "42 = Dig0 (Dig1 (Dig0 (Dig1 (Dig0 1))))"
haftmann@28419
   250
  by (simp add: Dig0_def Dig1_def)
haftmann@28419
   251
haftmann@28419
   252
text {*
haftmann@28419
   253
  \noindent Of course we also have to provide proper code equations for
haftmann@28419
   254
  the operations, e.g. @{term "op + \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat"}:
haftmann@28419
   255
*}
haftmann@28419
   256
haftmann@28419
   257
lemma %quoteme plus_Dig [code func]:
haftmann@28419
   258
  "0 + n = n"
haftmann@28419
   259
  "m + 0 = m"
haftmann@28419
   260
  "1 + Dig0 n = Dig1 n"
haftmann@28419
   261
  "Dig0 m + 1 = Dig1 m"
haftmann@28419
   262
  "1 + Dig1 n = Dig0 (n + 1)"
haftmann@28419
   263
  "Dig1 m + 1 = Dig0 (m + 1)"
haftmann@28419
   264
  "Dig0 m + Dig0 n = Dig0 (m + n)"
haftmann@28419
   265
  "Dig0 m + Dig1 n = Dig1 (m + n)"
haftmann@28419
   266
  "Dig1 m + Dig0 n = Dig1 (m + n)"
haftmann@28419
   267
  "Dig1 m + Dig1 n = Dig0 (m + n + 1)"
haftmann@28419
   268
  by (simp_all add: Dig0_def Dig1_def)
haftmann@28419
   269
haftmann@28419
   270
text {*
haftmann@28419
   271
  \noindent We then instruct the code generator to view @{term "0\<Colon>nat"},
haftmann@28419
   272
  @{term "1\<Colon>nat"}, @{term Dig0} and @{term Dig1} as
haftmann@28419
   273
  datatype constructors:
haftmann@28419
   274
*}
haftmann@28419
   275
haftmann@28419
   276
code_datatype %quoteme "0\<Colon>nat" "1\<Colon>nat" Dig0 Dig1
haftmann@28419
   277
haftmann@28419
   278
text {*
haftmann@28419
   279
  \noindent For the former constructor @{term Suc}, we provide a code
haftmann@28419
   280
  equation and remove some parts of the default code generator setup
haftmann@28419
   281
  which are an obstacle here:
haftmann@28419
   282
*}
haftmann@28419
   283
haftmann@28419
   284
lemma %quoteme Suc_Dig [code func]:
haftmann@28419
   285
  "Suc n = n + 1"
haftmann@28419
   286
  by simp
haftmann@28419
   287
haftmann@28419
   288
declare %quoteme One_nat_def [code inline del]
haftmann@28419
   289
declare %quoteme add_Suc_shift [code func del] 
haftmann@28419
   290
haftmann@28419
   291
text {*
haftmann@28419
   292
  \noindent This yields the following code:
haftmann@28419
   293
*}
haftmann@28419
   294
haftmann@28419
   295
text %quoteme {*@{code_stmts "op + \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat" (SML)}*}
haftmann@28419
   296
haftmann@28419
   297
text {*
haftmann@28447
   298
  \noindent From this example, it can be easily glimpsed that using own constructor sets
haftmann@28419
   299
  is a little delicate since it changes the set of valid patterns for values
haftmann@28419
   300
  of that type.  Without going into much detail, here some practical hints:
haftmann@28419
   301
haftmann@28419
   302
  \begin{itemize}
haftmann@28419
   303
    \item When changing the constructor set for datatypes, take care to
haftmann@28419
   304
      provide an alternative for the @{text case} combinator (e.g.~by replacing
haftmann@28419
   305
      it using the preprocessor).
haftmann@28419
   306
    \item Values in the target language need not to be normalised -- different
haftmann@28419
   307
      values in the target language may represent the same value in the
haftmann@28419
   308
      logic (e.g. @{term "Dig1 0 = 1"}).
haftmann@28419
   309
    \item Usually, a good methodology to deal with the subtleties of pattern
haftmann@28419
   310
      matching is to see the type as an abstract type: provide a set
haftmann@28419
   311
      of operations which operate on the concrete representation of the type,
haftmann@28419
   312
      and derive further operations by combinations of these primitive ones,
haftmann@28419
   313
      without relying on a particular representation.
haftmann@28419
   314
  \end{itemize}
haftmann@28419
   315
*}
haftmann@28419
   316
haftmann@28419
   317
code_datatype %invisible "0::nat" Suc
haftmann@28419
   318
declare %invisible plus_Dig [code func del]
haftmann@28419
   319
declare %invisible One_nat_def [code inline]
haftmann@28419
   320
declare %invisible add_Suc_shift [code func] 
haftmann@28419
   321
lemma %invisible [code func]: "0 + n = (n \<Colon> nat)" by simp
haftmann@28419
   322
haftmann@28213
   323
haftmann@28213
   324
subsection {* Equality and wellsortedness *}
haftmann@28213
   325
haftmann@28419
   326
text {*
haftmann@28419
   327
  Surely you have already noticed how equality is treated
haftmann@28419
   328
  by the code generator:
haftmann@28419
   329
*}
haftmann@28419
   330
haftmann@28447
   331
primrec %quoteme collect_duplicates :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where
haftmann@28447
   332
  "collect_duplicates xs ys [] = xs"
haftmann@28419
   333
  | "collect_duplicates xs ys (z#zs) = (if z \<in> set xs
haftmann@28419
   334
      then if z \<in> set ys
haftmann@28419
   335
        then collect_duplicates xs ys zs
haftmann@28419
   336
        else collect_duplicates xs (z#ys) zs
haftmann@28419
   337
      else collect_duplicates (z#xs) (z#ys) zs)"
haftmann@28419
   338
haftmann@28419
   339
text {*
haftmann@28428
   340
  \noindent The membership test during preprocessing is rewritten,
haftmann@28419
   341
  resulting in @{const List.member}, which itself
haftmann@28419
   342
  performs an explicit equality check.
haftmann@28419
   343
*}
haftmann@28419
   344
haftmann@28419
   345
text %quoteme {*@{code_stmts collect_duplicates (SML)}*}
haftmann@28419
   346
haftmann@28419
   347
text {*
haftmann@28419
   348
  \noindent Obviously, polymorphic equality is implemented the Haskell
haftmann@28419
   349
  way using a type class.  How is this achieved?  HOL introduces
haftmann@28419
   350
  an explicit class @{class eq} with a corresponding operation
haftmann@28419
   351
  @{const eq_class.eq} such that @{thm eq [no_vars]}.
haftmann@28447
   352
  The preprocessing framework does the rest by propagating the
haftmann@28447
   353
  @{class eq} constraints through all dependent defining equations.
haftmann@28419
   354
  For datatypes, instances of @{class eq} are implicitly derived
haftmann@28419
   355
  when possible.  For other types, you may instantiate @{text eq}
haftmann@28419
   356
  manually like any other type class.
haftmann@28419
   357
haftmann@28419
   358
  Though this @{text eq} class is designed to get rarely in
haftmann@28419
   359
  the way, a subtlety
haftmann@28419
   360
  enters the stage when definitions of overloaded constants
haftmann@28419
   361
  are dependent on operational equality.  For example, let
haftmann@28447
   362
  us define a lexicographic ordering on tuples
haftmann@28447
   363
  (also see theory @{theory Product_ord}):
haftmann@28419
   364
*}
haftmann@28419
   365
haftmann@28447
   366
instantiation %quoteme "*" :: (order, order) order
haftmann@28419
   367
begin
haftmann@28419
   368
haftmann@28428
   369
definition %quoteme [code func del]:
haftmann@28447
   370
  "x \<le> y \<longleftrightarrow> fst x < fst y \<or> fst x = fst y \<and> snd x \<le> snd y"
haftmann@28428
   371
haftmann@28428
   372
definition %quoteme [code func del]:
haftmann@28447
   373
  "x < y \<longleftrightarrow> fst x < fst y \<or> fst x = fst y \<and> snd x < snd y"
haftmann@28419
   374
haftmann@28447
   375
instance %quoteme proof
haftmann@28447
   376
qed (auto simp: less_eq_prod_def less_prod_def intro: order_less_trans)
haftmann@28419
   377
haftmann@28428
   378
end %quoteme
haftmann@28419
   379
haftmann@28447
   380
lemma %quoteme order_prod [code func]:
haftmann@28447
   381
  "(x1 \<Colon> 'a\<Colon>order, y1 \<Colon> 'b\<Colon>order) < (x2, y2) \<longleftrightarrow>
haftmann@28447
   382
     x1 < x2 \<or> x1 = x2 \<and> y1 < y2"
haftmann@28447
   383
  "(x1 \<Colon> 'a\<Colon>order, y1 \<Colon> 'b\<Colon>order) \<le> (x2, y2) \<longleftrightarrow>
haftmann@28447
   384
     x1 < x2 \<or> x1 = x2 \<and> y1 \<le> y2"
haftmann@28447
   385
  by (simp_all add: less_prod_def less_eq_prod_def)
haftmann@28419
   386
haftmann@28419
   387
text {*
haftmann@28428
   388
  \noindent Then code generation will fail.  Why?  The definition
haftmann@28419
   389
  of @{term "op \<le>"} depends on equality on both arguments,
haftmann@28419
   390
  which are polymorphic and impose an additional @{class eq}
haftmann@28447
   391
  class constraint, which the preprocessor does not propagate
haftmann@28447
   392
  (for technical reasons).
haftmann@28419
   393
haftmann@28419
   394
  The solution is to add @{class eq} explicitly to the first sort arguments in the
haftmann@28419
   395
  code theorems:
haftmann@28419
   396
*}
haftmann@28419
   397
haftmann@28447
   398
lemma %quoteme order_prod_code [code func]:
haftmann@28447
   399
  "(x1 \<Colon> 'a\<Colon>{order, eq}, y1 \<Colon> 'b\<Colon>order) < (x2, y2) \<longleftrightarrow>
haftmann@28447
   400
     x1 < x2 \<or> x1 = x2 \<and> y1 < y2"
haftmann@28447
   401
  "(x1 \<Colon> 'a\<Colon>{order, eq}, y1 \<Colon> 'b\<Colon>order) \<le> (x2, y2) \<longleftrightarrow>
haftmann@28447
   402
     x1 < x2 \<or> x1 = x2 \<and> y1 \<le> y2"
haftmann@28447
   403
  by (simp_all add: less_prod_def less_eq_prod_def)
haftmann@28419
   404
haftmann@28419
   405
text {*
haftmann@28419
   406
  \noindent Then code generation succeeds:
haftmann@28419
   407
*}
haftmann@28419
   408
haftmann@28447
   409
text %quoteme {*@{code_stmts "op \<le> \<Colon> _ \<times> _ \<Rightarrow> _ \<times> _ \<Rightarrow> bool" (SML)}*}
haftmann@28419
   410
haftmann@28419
   411
text {*
haftmann@28419
   412
  In some cases, the automatically derived defining equations
haftmann@28419
   413
  for equality on a particular type may not be appropriate.
haftmann@28419
   414
  As example, watch the following datatype representing
haftmann@28419
   415
  monomorphic parametric types (where type constructors
haftmann@28419
   416
  are referred to by natural numbers):
haftmann@28419
   417
*}
haftmann@28419
   418
haftmann@28419
   419
datatype %quoteme monotype = Mono nat "monotype list"
haftmann@28419
   420
(*<*)
haftmann@28419
   421
lemma monotype_eq:
haftmann@28419
   422
  "Mono tyco1 typargs1 = Mono tyco2 typargs2 \<equiv> 
haftmann@28419
   423
     tyco1 = tyco2 \<and> typargs1 = typargs2" by simp
haftmann@28419
   424
(*>*)
haftmann@28419
   425
haftmann@28419
   426
text {*
haftmann@28419
   427
  Then code generation for SML would fail with a message
haftmann@28419
   428
  that the generated code contains illegal mutual dependencies:
haftmann@28419
   429
  the theorem @{thm monotype_eq [no_vars]} already requires the
haftmann@28419
   430
  instance @{text "monotype \<Colon> eq"}, which itself requires
haftmann@28419
   431
  @{thm monotype_eq [no_vars]};  Haskell has no problem with mutually
haftmann@28428
   432
  recursive @{text inst} and @{text fun} definitions,
haftmann@28419
   433
  but the SML serializer does not support this.
haftmann@28419
   434
haftmann@28447
   435
  In such cases, you have to provide your own equality equations
haftmann@28419
   436
  involving auxiliary constants.  In our case,
haftmann@28419
   437
  @{const [show_types] list_all2} can do the job:
haftmann@28419
   438
*}
haftmann@28419
   439
haftmann@28419
   440
lemma %quoteme monotype_eq_list_all2 [code func]:
haftmann@28419
   441
  "eq_class.eq (Mono tyco1 typargs1) (Mono tyco2 typargs2) \<longleftrightarrow>
haftmann@28419
   442
     tyco1 = tyco2 \<and> list_all2 eq_class.eq typargs1 typargs2"
haftmann@28419
   443
  by (simp add: eq list_all2_eq [symmetric])
haftmann@28419
   444
haftmann@28419
   445
text {*
haftmann@28419
   446
  \noindent does not depend on instance @{text "monotype \<Colon> eq"}:
haftmann@28419
   447
*}
haftmann@28419
   448
haftmann@28419
   449
text %quoteme {*@{code_stmts "eq_class.eq :: monotype \<Rightarrow> monotype \<Rightarrow> bool" (SML)}*}
haftmann@28419
   450
haftmann@28419
   451
haftmann@28213
   452
subsection {* Partiality *}
haftmann@28213
   453
haftmann@28419
   454
text {* @{command "code_abort"}, examples: maps *}
haftmann@28213
   455
haftmann@28213
   456
end