src/HOL/Library/EfficientNat.thy
author chaieb
Mon Jun 11 11:06:04 2007 +0200 (2007-06-11)
changeset 23315 df3a7e9ebadb
parent 23269 851b8ea067ac
child 23365 f31794033ae1
permissions -rw-r--r--
tuned Proof
berghofe@15323
     1
(*  Title:      HOL/Library/EfficientNat.thy
berghofe@15323
     2
    ID:         $Id$
berghofe@15323
     3
    Author:     Stefan Berghofer, TU Muenchen
berghofe@15323
     4
*)
berghofe@15323
     5
berghofe@15323
     6
header {* Implementation of natural numbers by integers *}
berghofe@15323
     7
berghofe@15323
     8
theory EfficientNat
haftmann@22804
     9
imports Main Pretty_Int
berghofe@15323
    10
begin
berghofe@15323
    11
berghofe@15323
    12
text {*
berghofe@15323
    13
When generating code for functions on natural numbers, the canonical
berghofe@15323
    14
representation using @{term "0::nat"} and @{term "Suc"} is unsuitable for
berghofe@15323
    15
computations involving large numbers. The efficiency of the generated
berghofe@15323
    16
code can be improved drastically by implementing natural numbers by
berghofe@15323
    17
integers. To do this, just include this theory.
berghofe@15323
    18
*}
berghofe@15323
    19
haftmann@20700
    20
subsection {* Logical rewrites *}
berghofe@15323
    21
berghofe@15323
    22
text {*
haftmann@22845
    23
  An int-to-nat conversion
haftmann@20700
    24
  restricted to non-negative ints (in contrast to @{const nat}).
haftmann@22320
    25
  Note that this restriction has no logical relevance and
haftmann@22320
    26
  is just a kind of proof hint -- nothing prevents you from 
haftmann@22320
    27
  writing nonsense like @{term "nat_of_int (-4)"}
berghofe@16770
    28
*}
berghofe@16770
    29
haftmann@20641
    30
definition
wenzelm@21404
    31
  nat_of_int :: "int \<Rightarrow> nat" where
haftmann@20641
    32
  "k \<ge> 0 \<Longrightarrow> nat_of_int k = nat k"
haftmann@19889
    33
haftmann@22395
    34
lemma nat_of_int_of_number_of:
haftmann@22395
    35
  fixes k
haftmann@22395
    36
  assumes "k \<ge> 0"
haftmann@22804
    37
  shows "number_of k = nat_of_int (number_of k)"
haftmann@22395
    38
  unfolding nat_of_int_def [OF prems] nat_number_of_def number_of_is_id ..
haftmann@22395
    39
haftmann@22395
    40
lemma nat_of_int_of_number_of_aux:
haftmann@22395
    41
  fixes k
haftmann@22395
    42
  assumes "Numeral.Pls \<le> k \<equiv> True"
haftmann@22395
    43
  shows "k \<ge> 0"
haftmann@22395
    44
  using prems unfolding Pls_def by simp
haftmann@22395
    45
haftmann@20839
    46
lemma nat_of_int_int:
haftmann@20839
    47
  "nat_of_int (int n) = n"
haftmann@20839
    48
  using zero_zle_int nat_of_int_def by simp
haftmann@20839
    49
haftmann@19889
    50
text {*
haftmann@20700
    51
  Case analysis on natural numbers is rephrased using a conditional
haftmann@20700
    52
  expression:
berghofe@15323
    53
*}
berghofe@15323
    54
haftmann@22845
    55
lemma [code unfold, code inline del]:
haftmann@22845
    56
  "nat_case \<equiv> (\<lambda>f g n. if n = 0 then f else g (n - 1))"
haftmann@20700
    57
proof -
haftmann@20700
    58
  have rewrite: "\<And>f g n. nat_case f g n = (if n = 0 then f else g (n - 1))"
haftmann@20700
    59
  proof -
haftmann@20700
    60
    fix f g n
haftmann@20700
    61
    show "nat_case f g n = (if n = 0 then f else g (n - 1))"
haftmann@20700
    62
      by (cases n) simp_all
haftmann@20700
    63
  qed
haftmann@20700
    64
  show "nat_case \<equiv> (\<lambda>f g n. if n = 0 then f else g (n - 1))"
haftmann@20700
    65
    by (rule eq_reflection ext rewrite)+ 
haftmann@20700
    66
qed
berghofe@15323
    67
haftmann@20839
    68
lemma [code inline]:
haftmann@22743
    69
  "nat_case = (\<lambda>f g n. if n = 0 then f else g (nat_of_int (int n - 1)))"
haftmann@22845
    70
proof (rule ext)+
haftmann@22743
    71
  fix f g n
haftmann@22743
    72
  show "nat_case f g n = (if n = 0 then f else g (nat_of_int (int n - 1)))"
haftmann@21454
    73
  by (cases n) (simp_all add: nat_of_int_int)
haftmann@22743
    74
qed
haftmann@20839
    75
berghofe@15323
    76
text {*
haftmann@20700
    77
  Most standard arithmetic functions on natural numbers are implemented
haftmann@20700
    78
  using their counterparts on the integers:
berghofe@15323
    79
*}
berghofe@15323
    80
haftmann@20641
    81
lemma [code func]: "0 = nat_of_int 0"
haftmann@20641
    82
  by (simp add: nat_of_int_def)
haftmann@20641
    83
lemma [code func, code inline]:  "1 = nat_of_int 1"
haftmann@20641
    84
  by (simp add: nat_of_int_def)
haftmann@22845
    85
lemma [code func]: "Suc n = nat_of_int (int n + 1)"
haftmann@22845
    86
  by (simp add: nat_of_int_def)
haftmann@21874
    87
lemma [code]: "m + n = nat (int m + int n)"
haftmann@20641
    88
  by arith
haftmann@20641
    89
lemma [code func, code inline]: "m + n = nat_of_int (int m + int n)"
haftmann@20641
    90
  by (simp add: nat_of_int_def)
haftmann@20641
    91
lemma [code, code inline]: "m - n = nat (int m - int n)"
haftmann@20641
    92
  by arith
haftmann@21874
    93
lemma [code]: "m * n = nat (int m * int n)"
haftmann@20641
    94
  unfolding zmult_int by simp
haftmann@20641
    95
lemma [code func, code inline]: "m * n = nat_of_int (int m * int n)"
haftmann@20641
    96
proof -
haftmann@20641
    97
  have "int (m * n) = int m * int n"
haftmann@20641
    98
    by (induct m) (simp_all add: zadd_zmult_distrib)
haftmann@20641
    99
  then have "m * n = nat (int m * int n)" by auto
haftmann@20641
   100
  also have "\<dots> = nat_of_int (int m * int n)"
haftmann@20641
   101
  proof -
haftmann@20641
   102
    have "int m \<ge> 0" and "int n \<ge> 0" by auto
haftmann@20641
   103
    have "int m * int n \<ge> 0" by (rule split_mult_pos_le) auto
haftmann@20641
   104
    with nat_of_int_def show ?thesis by auto
haftmann@20641
   105
  qed
haftmann@20641
   106
  finally show ?thesis .
haftmann@20641
   107
qed  
haftmann@20641
   108
lemma [code]: "m div n = nat (int m div int n)"
haftmann@20641
   109
  unfolding zdiv_int [symmetric] by simp
haftmann@20641
   110
lemma [code func]: "m div n = fst (Divides.divmod m n)"
haftmann@20641
   111
  unfolding divmod_def by simp
haftmann@20641
   112
lemma [code]: "m mod n = nat (int m mod int n)"
haftmann@20641
   113
  unfolding zmod_int [symmetric] by simp
haftmann@20641
   114
lemma [code func]: "m mod n = snd (Divides.divmod m n)"
haftmann@20641
   115
  unfolding divmod_def by simp
haftmann@20641
   116
lemma [code, code inline]: "(m < n) \<longleftrightarrow> (int m < int n)"
haftmann@20641
   117
  by simp
haftmann@20641
   118
lemma [code func, code inline]: "(m \<le> n) \<longleftrightarrow> (int m \<le> int n)"
haftmann@20641
   119
  by simp
haftmann@21454
   120
lemma [code func, code inline]: "m = n \<longleftrightarrow> int m = int n"
haftmann@21454
   121
  by simp
haftmann@20641
   122
lemma [code func]: "nat k = (if k < 0 then 0 else nat_of_int k)"
haftmann@20641
   123
proof (cases "k < 0")
haftmann@20641
   124
  case True then show ?thesis by simp
haftmann@20641
   125
next
haftmann@20641
   126
  case False then show ?thesis by (simp add: nat_of_int_def)
haftmann@20641
   127
qed
krauss@20523
   128
lemma [code func]:
haftmann@20641
   129
  "int_aux i n = (if int n = 0 then i else int_aux (i + 1) (nat_of_int (int n - 1)))"
haftmann@20641
   130
proof -
haftmann@20641
   131
  have "0 < n \<Longrightarrow> int n = 1 + int (nat_of_int (int n - 1))"
haftmann@20641
   132
  proof -
haftmann@20641
   133
    assume prem: "n > 0"
haftmann@20641
   134
    then have "int n - 1 \<ge> 0" by auto
haftmann@20641
   135
    then have "nat_of_int (int n - 1) = nat (int n - 1)" by (simp add: nat_of_int_def)
haftmann@20641
   136
    with prem show "int n = 1 + int (nat_of_int (int n - 1))" by simp
haftmann@20641
   137
  qed
haftmann@20641
   138
  then show ?thesis unfolding int_aux_def by simp
haftmann@20641
   139
qed
haftmann@20356
   140
haftmann@22395
   141
lemma div_nat_code [code func]:
haftmann@22395
   142
  "m div k = nat_of_int (fst (divAlg (int m, int k)))"
haftmann@22395
   143
  unfolding div_def [symmetric] zdiv_int [symmetric] nat_of_int_int ..
haftmann@22395
   144
haftmann@22395
   145
lemma mod_nat_code [code func]:
haftmann@22395
   146
  "m mod k = nat_of_int (snd (divAlg (int m, int k)))"
haftmann@22395
   147
  unfolding mod_def [symmetric] zmod_int [symmetric] nat_of_int_int ..
haftmann@22395
   148
haftmann@22395
   149
haftmann@20700
   150
subsection {* Code generator setup for basic functions *}
haftmann@20700
   151
haftmann@20700
   152
text {*
haftmann@20700
   153
  @{typ nat} is no longer a datatype but embedded into the integers.
haftmann@20700
   154
*}
haftmann@20700
   155
haftmann@22507
   156
code_datatype nat_of_int
haftmann@22507
   157
haftmann@22804
   158
code_type nat
haftmann@22804
   159
  (SML "IntInf.int")
haftmann@22804
   160
  (OCaml "Big'_int.big'_int")
haftmann@22804
   161
  (Haskell "Integer")
haftmann@20839
   162
haftmann@20700
   163
types_code
haftmann@20700
   164
  nat ("int")
haftmann@20700
   165
attach (term_of) {*
wenzelm@21846
   166
val term_of_nat = HOLogic.mk_number HOLogic.natT o IntInf.fromInt;
haftmann@20700
   167
*}
haftmann@20700
   168
attach (test) {*
haftmann@20700
   169
fun gen_nat i = random_range 0 i;
haftmann@20700
   170
*}
haftmann@20700
   171
haftmann@20700
   172
consts_code
haftmann@22921
   173
  "0 \<Colon> nat" ("0")
haftmann@20700
   174
  Suc ("(_ + 1)")
haftmann@20700
   175
haftmann@20700
   176
text {*
haftmann@20700
   177
  Since natural numbers are implemented
haftmann@20700
   178
  using integers, the coercion function @{const "int"} of type
haftmann@20700
   179
  @{typ "nat \<Rightarrow> int"} is simply implemented by the identity function,
haftmann@20700
   180
  likewise @{const nat_of_int} of type @{typ "int \<Rightarrow> nat"}.
haftmann@20700
   181
  For the @{const "nat"} function for converting an integer to a natural
haftmann@20700
   182
  number, we give a specific implementation using an ML function that
haftmann@20700
   183
  returns its input value, provided that it is non-negative, and otherwise
haftmann@20700
   184
  returns @{text "0"}.
haftmann@20700
   185
*}
haftmann@20700
   186
haftmann@20700
   187
consts_code
haftmann@20700
   188
  int ("(_)")
haftmann@20700
   189
  nat ("\<module>nat")
haftmann@20700
   190
attach {*
haftmann@20700
   191
fun nat i = if i < 0 then 0 else i;
haftmann@20700
   192
*}
haftmann@20700
   193
haftmann@20700
   194
code_const int
haftmann@20700
   195
  (SML "_")
haftmann@21911
   196
  (OCaml "_")
haftmann@20700
   197
  (Haskell "_")
haftmann@20700
   198
haftmann@20700
   199
code_const nat_of_int
haftmann@20700
   200
  (SML "_")
haftmann@21911
   201
  (OCaml "_")
haftmann@20700
   202
  (Haskell "_")
haftmann@20700
   203
haftmann@20700
   204
berghofe@15323
   205
subsection {* Preprocessors *}
berghofe@15323
   206
berghofe@15323
   207
text {*
haftmann@22395
   208
  Natural numerals should be expressed using @{const nat_of_int}.
haftmann@22395
   209
*}
haftmann@22395
   210
haftmann@22845
   211
lemmas [code inline del] = nat_number_of_def
haftmann@22395
   212
haftmann@22395
   213
ML {*
haftmann@22395
   214
fun nat_of_int_of_number_of thy cts =
haftmann@22395
   215
  let
haftmann@22395
   216
    val simplify_less = Simplifier.rewrite 
haftmann@22395
   217
      (HOL_basic_ss addsimps (@{thms less_numeral_code} @ @{thms less_eq_numeral_code}));
haftmann@22395
   218
    fun mk_rew (t, ty) =
haftmann@22395
   219
      if ty = HOLogic.natT andalso IntInf.<= (0, HOLogic.dest_numeral t) then
haftmann@22395
   220
        Thm.capply @{cterm "(op \<le>) Numeral.Pls"} (Thm.cterm_of thy t)
haftmann@22395
   221
        |> simplify_less
haftmann@22395
   222
        |> (fn thm => @{thm nat_of_int_of_number_of_aux} OF [thm])
haftmann@22395
   223
        |> (fn thm => @{thm nat_of_int_of_number_of} OF [thm])
haftmann@22395
   224
        |> (fn thm => @{thm eq_reflection} OF [thm])
haftmann@22395
   225
        |> SOME
haftmann@22395
   226
      else NONE
haftmann@22395
   227
  in
wenzelm@23269
   228
    fold (HOLogic.add_numerals o Thm.term_of) cts []
haftmann@22395
   229
    |> map_filter mk_rew
haftmann@22395
   230
  end;
haftmann@22395
   231
*}
haftmann@22395
   232
haftmann@22395
   233
setup {*
haftmann@22395
   234
  CodegenData.add_inline_proc ("nat_of_int_of_number_of", nat_of_int_of_number_of)
haftmann@22395
   235
*}
haftmann@22395
   236
haftmann@22395
   237
text {*
haftmann@20700
   238
  In contrast to @{term "Suc n"}, the term @{term "n + (1::nat)"} is no longer
haftmann@20700
   239
  a constructor term. Therefore, all occurrences of this term in a position
haftmann@20700
   240
  where a pattern is expected (i.e.\ on the left-hand side of a recursion
haftmann@20700
   241
  equation or in the arguments of an inductive relation in an introduction
haftmann@20700
   242
  rule) must be eliminated.
haftmann@20700
   243
  This can be accomplished by applying the following transformation rules:
berghofe@15323
   244
*}
berghofe@15323
   245
berghofe@16900
   246
theorem Suc_if_eq: "(\<And>n. f (Suc n) = h n) \<Longrightarrow> f 0 = g \<Longrightarrow>
berghofe@15323
   247
  f n = (if n = 0 then g else h (n - 1))"
berghofe@15323
   248
  by (case_tac n) simp_all
berghofe@15323
   249
berghofe@15323
   250
theorem Suc_clause: "(\<And>n. P n (Suc n)) \<Longrightarrow> n \<noteq> 0 \<Longrightarrow> P (n - 1) n"
berghofe@15323
   251
  by (case_tac n) simp_all
berghofe@15323
   252
berghofe@15323
   253
text {*
haftmann@20700
   254
  The rules above are built into a preprocessor that is plugged into
haftmann@20700
   255
  the code generator. Since the preprocessor for introduction rules
haftmann@20700
   256
  does not know anything about modes, some of the modes that worked
haftmann@20700
   257
  for the canonical representation of natural numbers may no longer work.
berghofe@15323
   258
*}
berghofe@15323
   259
berghofe@15323
   260
(*<*)
haftmann@19791
   261
berghofe@15323
   262
ML {*
haftmann@19791
   263
local
haftmann@19791
   264
  val Suc_if_eq = thm "Suc_if_eq";
haftmann@19791
   265
  val Suc_clause = thm "Suc_clause";
haftmann@19791
   266
  fun contains_suc t = member (op =) (term_consts t) "Suc";
haftmann@19791
   267
in
berghofe@15323
   268
berghofe@15396
   269
fun remove_suc thy thms =
berghofe@15323
   270
  let
berghofe@15396
   271
    val Suc_if_eq' = Thm.transfer thy Suc_if_eq;
wenzelm@20071
   272
    val vname = Name.variant (map fst
wenzelm@20196
   273
      (fold (Term.add_varnames o Thm.full_prop_of) thms [])) "x";
haftmann@21911
   274
    val cv = cterm_of thy (Var ((vname, 0), HOLogic.natT));
berghofe@15323
   275
    fun lhs_of th = snd (Thm.dest_comb
berghofe@15323
   276
      (fst (Thm.dest_comb (snd (Thm.dest_comb (cprop_of th))))));
berghofe@15323
   277
    fun rhs_of th = snd (Thm.dest_comb (snd (Thm.dest_comb (cprop_of th))));
berghofe@15323
   278
    fun find_vars ct = (case term_of ct of
berghofe@16900
   279
        (Const ("Suc", _) $ Var _) => [(cv, snd (Thm.dest_comb ct))]
berghofe@15323
   280
      | _ $ _ =>
berghofe@15323
   281
        let val (ct1, ct2) = Thm.dest_comb ct
berghofe@15323
   282
        in 
berghofe@16900
   283
          map (apfst (fn ct => Thm.capply ct ct2)) (find_vars ct1) @
berghofe@16900
   284
          map (apfst (Thm.capply ct1)) (find_vars ct2)
berghofe@15323
   285
        end
berghofe@15323
   286
      | _ => []);
berghofe@16900
   287
    val eqs = List.concat (map
berghofe@15323
   288
      (fn th => map (pair th) (find_vars (lhs_of th))) thms);
berghofe@16900
   289
    fun mk_thms (th, (ct, cv')) =
berghofe@15323
   290
      let
berghofe@16900
   291
        val th' =
berghofe@16900
   292
          Thm.implies_elim
wenzelm@22900
   293
           (Conv.fconv_rule (Thm.beta_conversion true)
berghofe@15323
   294
             (Drule.instantiate'
skalberg@15531
   295
               [SOME (ctyp_of_term ct)] [SOME (Thm.cabs cv ct),
berghofe@16900
   296
                 SOME (Thm.cabs cv' (rhs_of th)), NONE, SOME cv']
berghofe@16900
   297
               Suc_if_eq')) (Thm.forall_intr cv' th)
berghofe@15323
   298
      in
wenzelm@21287
   299
        case map_filter (fn th'' =>
wenzelm@20287
   300
            SOME (th'', singleton
wenzelm@21287
   301
              (Variable.trade (K (fn [th'''] => [th''' RS th'])) (Variable.thm_context th'')) th'')
berghofe@16900
   302
          handle THM _ => NONE) thms of
berghofe@16900
   303
            [] => NONE
berghofe@16900
   304
          | thps =>
haftmann@19791
   305
              let val (ths1, ths2) = split_list thps
wenzelm@22360
   306
              in SOME (subtract Thm.eq_thm (th :: ths1) thms @ ths2) end
berghofe@15323
   307
      end
berghofe@15323
   308
  in
haftmann@19791
   309
    case get_first mk_thms eqs of
berghofe@16900
   310
      NONE => thms
berghofe@16900
   311
    | SOME x => remove_suc thy x
berghofe@15323
   312
  end;
berghofe@15323
   313
berghofe@15323
   314
fun eqn_suc_preproc thy ths =
haftmann@19791
   315
  let
haftmann@19791
   316
    val dest = fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of
berghofe@15323
   317
  in
berghofe@15323
   318
    if forall (can dest) ths andalso
haftmann@19791
   319
      exists (contains_suc o dest) ths
berghofe@15396
   320
    then remove_suc thy ths else ths
berghofe@15323
   321
  end;
berghofe@15323
   322
berghofe@15396
   323
fun remove_suc_clause thy thms =
berghofe@15323
   324
  let
berghofe@15396
   325
    val Suc_clause' = Thm.transfer thy Suc_clause;
wenzelm@20071
   326
    val vname = Name.variant (map fst
wenzelm@20196
   327
      (fold (Term.add_varnames o Thm.full_prop_of) thms [])) "x";
skalberg@15531
   328
    fun find_var (t as Const ("Suc", _) $ (v as Var _)) = SOME (t, v)
skalberg@15531
   329
      | find_var (t $ u) = (case find_var t of NONE => find_var u | x => x)
skalberg@15531
   330
      | find_var _ = NONE;
berghofe@15323
   331
    fun find_thm th =
berghofe@15323
   332
      let val th' = ObjectLogic.atomize_thm th
skalberg@15570
   333
      in Option.map (pair (th, th')) (find_var (prop_of th')) end
berghofe@15323
   334
  in
berghofe@15323
   335
    case get_first find_thm thms of
skalberg@15531
   336
      NONE => thms
skalberg@15531
   337
    | SOME ((th, th'), (Sucv, v)) =>
berghofe@15323
   338
        let
wenzelm@16861
   339
          val cert = cterm_of (Thm.theory_of_thm th);
berghofe@15323
   340
          val th'' = ObjectLogic.rulify (Thm.implies_elim
wenzelm@22900
   341
            (Conv.fconv_rule (Thm.beta_conversion true)
berghofe@15323
   342
              (Drule.instantiate' []
skalberg@15531
   343
                [SOME (cert (lambda v (Abs ("x", HOLogic.natT,
berghofe@15323
   344
                   abstract_over (Sucv,
berghofe@19828
   345
                     HOLogic.dest_Trueprop (prop_of th')))))),
skalberg@15531
   346
                 SOME (cert v)] Suc_clause'))
berghofe@15323
   347
            (Thm.forall_intr (cert v) th'))
berghofe@15323
   348
        in
berghofe@15396
   349
          remove_suc_clause thy (map (fn th''' =>
wenzelm@19617
   350
            if (op = o pairself prop_of) (th''', th) then th'' else th''') thms)
berghofe@15323
   351
        end
berghofe@15323
   352
  end;
berghofe@15323
   353
berghofe@15323
   354
fun clause_suc_preproc thy ths =
haftmann@19791
   355
  let
berghofe@19828
   356
    val dest = fst o HOLogic.dest_mem o HOLogic.dest_Trueprop
berghofe@15323
   357
  in
berghofe@15323
   358
    if forall (can (dest o concl_of)) ths andalso
haftmann@19791
   359
      exists (fn th => member (op =) (foldr add_term_consts
wenzelm@21287
   360
        [] (map_filter (try dest) (concl_of th :: prems_of th))) "Suc") ths
berghofe@15396
   361
    then remove_suc_clause thy ths else ths
berghofe@15323
   362
  end;
berghofe@15323
   363
haftmann@19791
   364
end; (*local*)
haftmann@19791
   365
haftmann@22743
   366
fun lift_obj_eq f thy =
haftmann@22743
   367
  map (fn thm => thm RS @{thm meta_eq_to_obj_eq})
haftmann@19791
   368
  #> f thy
haftmann@22928
   369
  #> map (fn thm => thm RS @{thm eq_reflection})
haftmann@22928
   370
  #> map (Conv.fconv_rule Drule.beta_eta_conversion)
haftmann@19791
   371
*}
haftmann@19791
   372
haftmann@19791
   373
setup {*
haftmann@19603
   374
  Codegen.add_preprocessor eqn_suc_preproc
haftmann@19603
   375
  #> Codegen.add_preprocessor clause_suc_preproc
haftmann@22046
   376
  #> CodegenData.add_preproc ("eqn_Suc", lift_obj_eq eqn_suc_preproc)
haftmann@22046
   377
  #> CodegenData.add_preproc ("clause_Suc", lift_obj_eq clause_suc_preproc)
berghofe@15323
   378
*}
berghofe@15323
   379
(*>*)
berghofe@15323
   380
haftmann@21191
   381
subsection {* Module names *}
haftmann@21191
   382
haftmann@21191
   383
code_modulename SML
haftmann@21191
   384
  Nat Integer
haftmann@21191
   385
  EfficientNat Integer
haftmann@21191
   386
haftmann@21911
   387
code_modulename OCaml
haftmann@21911
   388
  Nat Integer
haftmann@21911
   389
  EfficientNat Integer
haftmann@21911
   390
haftmann@23017
   391
code_modulename Haskell
haftmann@23017
   392
  Nat Integer
haftmann@23017
   393
  EfficientNat Integer
haftmann@23017
   394
haftmann@22395
   395
hide const nat_of_int
haftmann@22395
   396
berghofe@15323
   397
end