src/HOL/Library/Efficient_Nat.thy
author wenzelm
Wed Sep 12 13:42:28 2012 +0200 (2012-09-12)
changeset 49322 fbb320d02420
parent 48568 084cd758a8ab
child 50023 28f3263d4d1b
permissions -rw-r--r--
tuned headers;
haftmann@23854
     1
(*  Title:      HOL/Library/Efficient_Nat.thy
haftmann@25931
     2
    Author:     Stefan Berghofer, Florian Haftmann, TU Muenchen
haftmann@23854
     3
*)
haftmann@23854
     4
haftmann@25931
     5
header {* Implementation of natural numbers by target-language integers *}
haftmann@23854
     6
haftmann@23854
     7
theory Efficient_Nat
huffman@47108
     8
imports Code_Nat Code_Integer Main
haftmann@23854
     9
begin
haftmann@23854
    10
haftmann@23854
    11
text {*
huffman@47108
    12
  The efficiency of the generated code for natural numbers can be improved
haftmann@25931
    13
  drastically by implementing natural numbers by target-language
haftmann@25931
    14
  integers.  To do this, just include this theory.
haftmann@23854
    15
*}
haftmann@23854
    16
huffman@47108
    17
subsection {* Target language fundamentals *}
haftmann@25931
    18
haftmann@25931
    19
text {*
haftmann@25967
    20
  For ML, we map @{typ nat} to target language integers, where we
haftmann@34899
    21
  ensure that values are always non-negative.
haftmann@25931
    22
*}
haftmann@25931
    23
haftmann@25931
    24
code_type nat
haftmann@27496
    25
  (SML "IntInf.int")
haftmann@25931
    26
  (OCaml "Big'_int.big'_int")
haftmann@37958
    27
  (Eval "int")
haftmann@25931
    28
haftmann@25931
    29
text {*
bulwahn@45185
    30
  For Haskell and Scala we define our own @{typ nat} type.  The reason
haftmann@34899
    31
  is that we have to distinguish type class instances for @{typ nat}
haftmann@34899
    32
  and @{typ int}.
haftmann@25967
    33
*}
haftmann@25967
    34
haftmann@38774
    35
code_include Haskell "Nat"
haftmann@38774
    36
{*newtype Nat = Nat Integer deriving (Eq, Show, Read);
haftmann@25967
    37
haftmann@25967
    38
instance Num Nat where {
haftmann@25967
    39
  fromInteger k = Nat (if k >= 0 then k else 0);
haftmann@25967
    40
  Nat n + Nat m = Nat (n + m);
haftmann@25967
    41
  Nat n - Nat m = fromInteger (n - m);
haftmann@25967
    42
  Nat n * Nat m = Nat (n * m);
haftmann@25967
    43
  abs n = n;
haftmann@25967
    44
  signum _ = 1;
haftmann@25967
    45
  negate n = error "negate Nat";
haftmann@25967
    46
};
haftmann@25967
    47
haftmann@25967
    48
instance Ord Nat where {
haftmann@25967
    49
  Nat n <= Nat m = n <= m;
haftmann@25967
    50
  Nat n < Nat m = n < m;
haftmann@25967
    51
};
haftmann@25967
    52
haftmann@25967
    53
instance Real Nat where {
haftmann@25967
    54
  toRational (Nat n) = toRational n;
haftmann@25967
    55
};
haftmann@25967
    56
haftmann@25967
    57
instance Enum Nat where {
haftmann@25967
    58
  toEnum k = fromInteger (toEnum k);
haftmann@25967
    59
  fromEnum (Nat n) = fromEnum n;
haftmann@25967
    60
};
haftmann@25967
    61
haftmann@25967
    62
instance Integral Nat where {
haftmann@25967
    63
  toInteger (Nat n) = n;
haftmann@25967
    64
  divMod n m = quotRem n m;
haftmann@37958
    65
  quotRem (Nat n) (Nat m)
haftmann@37958
    66
    | (m == 0) = (0, Nat n)
haftmann@37958
    67
    | otherwise = (Nat k, Nat l) where (k, l) = quotRem n m;
haftmann@25967
    68
};
haftmann@25967
    69
*}
haftmann@25967
    70
haftmann@25967
    71
code_reserved Haskell Nat
haftmann@25967
    72
haftmann@38774
    73
code_include Scala "Nat"
haftmann@38968
    74
{*object Nat {
haftmann@34899
    75
haftmann@34899
    76
  def apply(numeral: BigInt): Nat = new Nat(numeral max 0)
haftmann@34899
    77
  def apply(numeral: Int): Nat = Nat(BigInt(numeral))
haftmann@34899
    78
  def apply(numeral: String): Nat = Nat(BigInt(numeral))
haftmann@34899
    79
haftmann@34899
    80
}
haftmann@34899
    81
haftmann@34899
    82
class Nat private(private val value: BigInt) {
haftmann@34899
    83
haftmann@34899
    84
  override def hashCode(): Int = this.value.hashCode()
haftmann@34899
    85
haftmann@34899
    86
  override def equals(that: Any): Boolean = that match {
haftmann@34899
    87
    case that: Nat => this equals that
haftmann@34899
    88
    case _ => false
haftmann@34899
    89
  }
haftmann@34899
    90
haftmann@34899
    91
  override def toString(): String = this.value.toString
haftmann@34899
    92
haftmann@34899
    93
  def equals(that: Nat): Boolean = this.value == that.value
haftmann@34899
    94
haftmann@34899
    95
  def as_BigInt: BigInt = this.value
haftmann@39781
    96
  def as_Int: Int = if (this.value >= scala.Int.MinValue && this.value <= scala.Int.MaxValue)
haftmann@34944
    97
      this.value.intValue
haftmann@37969
    98
    else error("Int value out of range: " + this.value.toString)
haftmann@34899
    99
haftmann@34899
   100
  def +(that: Nat): Nat = new Nat(this.value + that.value)
haftmann@37223
   101
  def -(that: Nat): Nat = Nat(this.value - that.value)
haftmann@34899
   102
  def *(that: Nat): Nat = new Nat(this.value * that.value)
haftmann@34899
   103
haftmann@34899
   104
  def /%(that: Nat): (Nat, Nat) = if (that.value == 0) (new Nat(0), this)
haftmann@34899
   105
    else {
haftmann@34899
   106
      val (k, l) = this.value /% that.value
haftmann@34899
   107
      (new Nat(k), new Nat(l))
haftmann@34899
   108
    }
haftmann@34899
   109
haftmann@34899
   110
  def <=(that: Nat): Boolean = this.value <= that.value
haftmann@34899
   111
haftmann@34899
   112
  def <(that: Nat): Boolean = this.value < that.value
haftmann@34899
   113
haftmann@34899
   114
}
haftmann@34899
   115
*}
haftmann@34899
   116
haftmann@34899
   117
code_reserved Scala Nat
haftmann@34899
   118
haftmann@25967
   119
code_type nat
haftmann@29793
   120
  (Haskell "Nat.Nat")
haftmann@38968
   121
  (Scala "Nat")
haftmann@25967
   122
haftmann@38857
   123
code_instance nat :: equal
haftmann@25967
   124
  (Haskell -)
haftmann@25967
   125
haftmann@25931
   126
setup {*
huffman@47108
   127
  fold (Numeral.add_code @{const_name nat_of_num}
haftmann@37958
   128
    false Code_Printer.literal_positive_numeral) ["SML", "OCaml", "Haskell", "Scala"]
haftmann@25931
   129
*}
haftmann@25931
   130
huffman@47108
   131
code_const "0::nat"
huffman@47108
   132
  (SML "0")
huffman@47108
   133
  (OCaml "Big'_int.zero'_big'_int")
huffman@47108
   134
  (Haskell "0")
huffman@47108
   135
  (Scala "Nat(0)")
huffman@47108
   136
huffman@47108
   137
huffman@47108
   138
subsection {* Conversions *}
huffman@47108
   139
haftmann@25931
   140
text {*
haftmann@25931
   141
  Since natural numbers are implemented
huffman@47108
   142
  using integers in ML, the coercion function @{term "int"} of type
haftmann@25931
   143
  @{typ "nat \<Rightarrow> int"} is simply implemented by the identity function.
haftmann@37388
   144
  For the @{const nat} function for converting an integer to a natural
huffman@47108
   145
  number, we give a specific implementation using an ML expression that
haftmann@25931
   146
  returns its input value, provided that it is non-negative, and otherwise
haftmann@25931
   147
  returns @{text "0"}.
haftmann@25931
   148
*}
haftmann@25931
   149
haftmann@32073
   150
definition int :: "nat \<Rightarrow> int" where
huffman@47108
   151
  [code_abbrev]: "int = of_nat"
haftmann@32073
   152
haftmann@25931
   153
code_const int
haftmann@25931
   154
  (SML "_")
haftmann@25931
   155
  (OCaml "_")
haftmann@25931
   156
haftmann@25967
   157
code_const nat
haftmann@43653
   158
  (SML "IntInf.max/ (0,/ _)")
haftmann@25967
   159
  (OCaml "Big'_int.max'_big'_int/ Big'_int.zero'_big'_int")
huffman@47108
   160
  (Eval "Integer.max/ 0")
haftmann@25967
   161
haftmann@35689
   162
text {* For Haskell and Scala, things are slightly different again. *}
haftmann@25967
   163
haftmann@25967
   164
code_const int and nat
haftmann@48431
   165
  (Haskell "Prelude.toInteger" and "Prelude.fromInteger")
haftmann@38968
   166
  (Scala "!_.as'_BigInt" and "Nat")
haftmann@25931
   167
huffman@47108
   168
text {* Alternativ implementation for @{const of_nat} *}
huffman@47108
   169
huffman@47108
   170
lemma [code]:
huffman@47108
   171
  "of_nat n = (if n = 0 then 0 else
huffman@47108
   172
     let
huffman@47108
   173
       (q, m) = divmod_nat n 2;
huffman@47108
   174
       q' = 2 * of_nat q
huffman@47108
   175
     in if m = 0 then q' else q' + 1)"
huffman@47108
   176
proof -
huffman@47108
   177
  from mod_div_equality have *: "of_nat n = of_nat (n div 2 * 2 + n mod 2)" by simp
huffman@47108
   178
  show ?thesis
huffman@47108
   179
    apply (simp add: Let_def divmod_nat_div_mod mod_2_not_eq_zero_eq_one_nat
huffman@47108
   180
      of_nat_mult
huffman@47108
   181
      of_nat_add [symmetric])
huffman@47108
   182
    apply (auto simp add: of_nat_mult)
huffman@47108
   183
    apply (simp add: * of_nat_mult add_commute mult_commute)
huffman@47108
   184
    done
huffman@47108
   185
qed
huffman@47108
   186
huffman@47108
   187
text {* Conversion from and to code numerals *}
haftmann@25931
   188
haftmann@31205
   189
code_const Code_Numeral.of_nat
haftmann@25967
   190
  (SML "IntInf.toInt")
haftmann@31377
   191
  (OCaml "_")
haftmann@48431
   192
  (Haskell "!(Prelude.fromInteger/ ./ Prelude.toInteger)")
haftmann@38968
   193
  (Scala "!Natural(_.as'_BigInt)")
haftmann@37958
   194
  (Eval "_")
haftmann@25967
   195
haftmann@31205
   196
code_const Code_Numeral.nat_of
haftmann@25931
   197
  (SML "IntInf.fromInt")
haftmann@31377
   198
  (OCaml "_")
haftmann@48431
   199
  (Haskell "!(Prelude.fromInteger/ ./ Prelude.toInteger)")
haftmann@38968
   200
  (Scala "!Nat(_.as'_BigInt)")
haftmann@37958
   201
  (Eval "_")
haftmann@25931
   202
huffman@47108
   203
huffman@47108
   204
subsection {* Target language arithmetic *}
haftmann@25931
   205
huffman@47108
   206
code_const "plus \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat"
huffman@47108
   207
  (SML "IntInf.+/ ((_),/ (_))")
haftmann@25931
   208
  (OCaml "Big'_int.add'_big'_int")
haftmann@25931
   209
  (Haskell infixl 6 "+")
haftmann@34899
   210
  (Scala infixl 7 "+")
haftmann@37958
   211
  (Eval infixl 8 "+")
haftmann@34899
   212
huffman@47108
   213
code_const "minus \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat"
huffman@47108
   214
  (SML "IntInf.max/ (0, IntInf.-/ ((_),/ (_)))")
huffman@47108
   215
  (OCaml "Big'_int.max'_big'_int/ Big'_int.zero'_big'_int/ (Big'_int.sub'_big'_int/ _/ _)")
haftmann@34899
   216
  (Haskell infixl 6 "-")
haftmann@34899
   217
  (Scala infixl 7 "-")
huffman@47108
   218
  (Eval "Integer.max/ 0/ (_ -/ _)")
haftmann@25931
   219
huffman@47108
   220
code_const Code_Nat.dup
huffman@47108
   221
  (SML "IntInf.*/ (2,/ (_))")
huffman@47108
   222
  (OCaml "Big'_int.mult'_big'_int/ 2")
huffman@47108
   223
  (Haskell "!(2 * _)")
huffman@47108
   224
  (Scala "!(2 * _)")
huffman@47108
   225
  (Eval "!(2 * _)")
huffman@47108
   226
huffman@47108
   227
code_const Code_Nat.sub
huffman@47108
   228
  (SML "!(raise/ Fail/ \"sub\")")
huffman@47108
   229
  (OCaml "failwith/ \"sub\"")
huffman@47108
   230
  (Haskell "error/ \"sub\"")
haftmann@48073
   231
  (Scala "!sys.error(\"sub\")")
huffman@47108
   232
huffman@47108
   233
code_const "times \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat"
huffman@47108
   234
  (SML "IntInf.*/ ((_),/ (_))")
haftmann@25931
   235
  (OCaml "Big'_int.mult'_big'_int")
haftmann@25931
   236
  (Haskell infixl 7 "*")
haftmann@34899
   237
  (Scala infixl 8 "*")
haftmann@37958
   238
  (Eval infixl 9 "*")
haftmann@25931
   239
haftmann@37958
   240
code_const divmod_nat
haftmann@26009
   241
  (SML "IntInf.divMod/ ((_),/ (_))")
haftmann@26009
   242
  (OCaml "Big'_int.quomod'_big'_int")
haftmann@26009
   243
  (Haskell "divMod")
haftmann@34899
   244
  (Scala infixl 8 "/%")
haftmann@37958
   245
  (Eval "Integer.div'_mod")
haftmann@25931
   246
haftmann@38857
   247
code_const "HOL.equal \<Colon> nat \<Rightarrow> nat \<Rightarrow> bool"
haftmann@25931
   248
  (SML "!((_ : IntInf.int) = _)")
haftmann@25931
   249
  (OCaml "Big'_int.eq'_big'_int")
haftmann@39272
   250
  (Haskell infix 4 "==")
haftmann@34899
   251
  (Scala infixl 5 "==")
haftmann@37958
   252
  (Eval infixl 6 "=")
haftmann@25931
   253
huffman@47108
   254
code_const "less_eq \<Colon> nat \<Rightarrow> nat \<Rightarrow> bool"
huffman@47108
   255
  (SML "IntInf.<=/ ((_),/ (_))")
haftmann@25931
   256
  (OCaml "Big'_int.le'_big'_int")
haftmann@25931
   257
  (Haskell infix 4 "<=")
haftmann@34899
   258
  (Scala infixl 4 "<=")
haftmann@37958
   259
  (Eval infixl 6 "<=")
haftmann@25931
   260
huffman@47108
   261
code_const "less \<Colon> nat \<Rightarrow> nat \<Rightarrow> bool"
huffman@47108
   262
  (SML "IntInf.</ ((_),/ (_))")
haftmann@25931
   263
  (OCaml "Big'_int.lt'_big'_int")
haftmann@25931
   264
  (Haskell infix 4 "<")
haftmann@34899
   265
  (Scala infixl 4 "<")
haftmann@37958
   266
  (Eval infixl 6 "<")
haftmann@25931
   267
huffman@47108
   268
code_const Num.num_of_nat
huffman@47108
   269
  (SML "!(raise/ Fail/ \"num'_of'_nat\")")
huffman@47108
   270
  (OCaml "failwith/ \"num'_of'_nat\"")
huffman@47108
   271
  (Haskell "error/ \"num'_of'_nat\"")
haftmann@48073
   272
  (Scala "!sys.error(\"num'_of'_nat\")")
haftmann@25931
   273
huffman@47108
   274
huffman@47108
   275
subsection {* Evaluation *}
haftmann@28228
   276
haftmann@28562
   277
lemma [code, code del]:
haftmann@32657
   278
  "(Code_Evaluation.term_of \<Colon> nat \<Rightarrow> term) = Code_Evaluation.term_of" ..
haftmann@28228
   279
haftmann@32657
   280
code_const "Code_Evaluation.term_of \<Colon> nat \<Rightarrow> term"
haftmann@28228
   281
  (SML "HOLogic.mk'_number/ HOLogic.natT")
haftmann@28228
   282
huffman@47108
   283
text {*
haftmann@48568
   284
  Evaluation with @{text "Quickcheck_Narrowing"} does not work yet,
haftmann@48568
   285
  since a couple of questions how to perform evaluations in Haskell are not that
haftmann@48568
   286
  clear yet.  Therefore, we simply deactivate the narrowing-based quickcheck
haftmann@48568
   287
  from here on.
bulwahn@45793
   288
*}
bulwahn@45793
   289
bulwahn@45793
   290
declare [[quickcheck_narrowing_active = false]] 
haftmann@28228
   291
haftmann@23854
   292
haftmann@23854
   293
code_modulename SML
haftmann@33364
   294
  Efficient_Nat Arith
haftmann@23854
   295
haftmann@23854
   296
code_modulename OCaml
haftmann@33364
   297
  Efficient_Nat Arith
haftmann@23854
   298
haftmann@23854
   299
code_modulename Haskell
haftmann@33364
   300
  Efficient_Nat Arith
haftmann@23854
   301
huffman@47108
   302
hide_const (open) int
haftmann@23854
   303
haftmann@23854
   304
end