1 (* Title: HOL/Library/Efficient_Nat.thy
2 Author: Stefan Berghofer, Florian Haftmann, TU Muenchen
5 header {* Implementation of natural numbers by target-language integers *}
8 imports Code_Integer Main
12 When generating code for functions on natural numbers, the
13 canonical representation using @{term "0::nat"} and
14 @{term Suc} is unsuitable for computations involving large
15 numbers. The efficiency of the generated code can be improved
16 drastically by implementing natural numbers by target-language
17 integers. To do this, just include this theory.
20 subsection {* Basic arithmetic *}
23 Most standard arithmetic functions on natural numbers are implemented
24 using their counterparts on the integers:
27 code_datatype number_nat_inst.number_of_nat
29 lemma zero_nat_code [code, code_unfold]:
30 "0 = (Numeral0 :: nat)"
33 lemma one_nat_code [code, code_unfold]:
34 "1 = (Numeral1 :: nat)"
37 lemma Suc_code [code]:
41 lemma plus_nat_code [code]:
42 "n + m = nat (of_nat n + of_nat m)"
45 lemma minus_nat_code [code]:
46 "n - m = nat (of_nat n - of_nat m)"
49 lemma times_nat_code [code]:
50 "n * m = nat (of_nat n * of_nat m)"
51 unfolding of_nat_mult [symmetric] by simp
53 lemma divmod_nat_code [code]:
54 "divmod_nat n m = map_pair nat nat (pdivmod (of_nat n) (of_nat m))"
55 by (simp add: map_pair_def split_def pdivmod_def nat_div_distrib nat_mod_distrib divmod_nat_div_mod)
57 lemma eq_nat_code [code]:
58 "HOL.equal n m \<longleftrightarrow> HOL.equal (of_nat n \<Colon> int) (of_nat m)"
61 lemma eq_nat_refl [code nbe]:
62 "HOL.equal (n::nat) n \<longleftrightarrow> True"
65 lemma less_eq_nat_code [code]:
66 "n \<le> m \<longleftrightarrow> (of_nat n \<Colon> int) \<le> of_nat m"
69 lemma less_nat_code [code]:
70 "n < m \<longleftrightarrow> (of_nat n \<Colon> int) < of_nat m"
73 subsection {* Case analysis *}
76 Case analysis on natural numbers is rephrased using a conditional
80 lemma [code, code_unfold]:
81 "nat_case = (\<lambda>f g n. if n = 0 then f else g (n - 1))"
82 by (auto simp add: fun_eq_iff dest!: gr0_implies_Suc)
85 subsection {* Preprocessors *}
88 In contrast to @{term "Suc n"}, the term @{term "n + (1::nat)"} is no longer
89 a constructor term. Therefore, all occurrences of this term in a position
90 where a pattern is expected (i.e.\ on the left-hand side of a recursion
91 equation or in the arguments of an inductive relation in an introduction
92 rule) must be eliminated.
93 This can be accomplished by applying the following transformation rules:
96 lemma Suc_if_eq: "(\<And>n. f (Suc n) \<equiv> h n) \<Longrightarrow> f 0 \<equiv> g \<Longrightarrow>
97 f n \<equiv> if n = 0 then g else h (n - 1)"
98 by (rule eq_reflection) (cases n, simp_all)
100 lemma Suc_clause: "(\<And>n. P n (Suc n)) \<Longrightarrow> n \<noteq> 0 \<Longrightarrow> P (n - 1) n"
101 by (cases n) simp_all
104 The rules above are built into a preprocessor that is plugged into
105 the code generator. Since the preprocessor for introduction rules
106 does not know anything about modes, some of the modes that worked
107 for the canonical representation of natural numbers may no longer work.
114 fun remove_suc thy thms =
116 val vname = singleton (Name.variant_list (map fst
117 (fold (Term.add_var_names o Thm.full_prop_of) thms []))) "n";
118 val cv = cterm_of thy (Var ((vname, 0), HOLogic.natT));
119 fun lhs_of th = snd (Thm.dest_comb
120 (fst (Thm.dest_comb (cprop_of th))));
121 fun rhs_of th = snd (Thm.dest_comb (cprop_of th));
122 fun find_vars ct = (case term_of ct of
123 (Const (@{const_name Suc}, _) $ Var _) => [(cv, snd (Thm.dest_comb ct))]
125 let val (ct1, ct2) = Thm.dest_comb ct
127 map (apfst (fn ct => Thm.capply ct ct2)) (find_vars ct1) @
128 map (apfst (Thm.capply ct1)) (find_vars ct2)
132 (fn th => map (pair th) (find_vars (lhs_of th))) thms;
133 fun mk_thms (th, (ct, cv')) =
137 (Conv.fconv_rule (Thm.beta_conversion true)
139 [SOME (ctyp_of_term ct)] [SOME (Thm.cabs cv ct),
140 SOME (Thm.cabs cv' (rhs_of th)), NONE, SOME cv']
141 @{thm Suc_if_eq})) (Thm.forall_intr cv' th)
143 case map_filter (fn th'' =>
144 SOME (th'', singleton
145 (Variable.trade (K (fn [th'''] => [th''' RS th']))
146 (Variable.global_thm_context th'')) th'')
147 handle THM _ => NONE) thms of
150 let val (ths1, ths2) = split_list thps
151 in SOME (subtract Thm.eq_thm (th :: ths1) thms @ ths2) end
153 in get_first mk_thms eqs end;
155 fun eqn_suc_base_preproc thy thms =
157 val dest = fst o Logic.dest_equals o prop_of;
158 val contains_suc = exists_Const (fn (c, _) => c = @{const_name Suc});
160 if forall (can dest) thms andalso exists (contains_suc o dest) thms
161 then thms |> perhaps_loop (remove_suc thy) |> (Option.map o map) Drule.zero_var_indexes
165 val eqn_suc_preproc = Code_Preproc.simple_functrans eqn_suc_base_preproc;
169 Code_Preproc.add_functrans ("eqn_Suc", eqn_suc_preproc)
176 subsection {* Target language setup *}
179 For ML, we map @{typ nat} to target language integers, where we
180 ensure that values are always non-negative.
185 (OCaml "Big'_int.big'_int")
189 For Haskell and Scala we define our own @{typ nat} type. The reason
190 is that we have to distinguish type class instances for @{typ nat}
194 code_include Haskell "Nat"
195 {*newtype Nat = Nat Integer deriving (Eq, Show, Read);
197 instance Num Nat where {
198 fromInteger k = Nat (if k >= 0 then k else 0);
199 Nat n + Nat m = Nat (n + m);
200 Nat n - Nat m = fromInteger (n - m);
201 Nat n * Nat m = Nat (n * m);
204 negate n = error "negate Nat";
207 instance Ord Nat where {
208 Nat n <= Nat m = n <= m;
209 Nat n < Nat m = n < m;
212 instance Real Nat where {
213 toRational (Nat n) = toRational n;
216 instance Enum Nat where {
217 toEnum k = fromInteger (toEnum k);
218 fromEnum (Nat n) = fromEnum n;
221 instance Integral Nat where {
222 toInteger (Nat n) = n;
223 divMod n m = quotRem n m;
224 quotRem (Nat n) (Nat m)
225 | (m == 0) = (0, Nat n)
226 | otherwise = (Nat k, Nat l) where (k, l) = quotRem n m;
230 code_reserved Haskell Nat
232 code_include Scala "Nat"
235 def apply(numeral: BigInt): Nat = new Nat(numeral max 0)
236 def apply(numeral: Int): Nat = Nat(BigInt(numeral))
237 def apply(numeral: String): Nat = Nat(BigInt(numeral))
241 class Nat private(private val value: BigInt) {
243 override def hashCode(): Int = this.value.hashCode()
245 override def equals(that: Any): Boolean = that match {
246 case that: Nat => this equals that
250 override def toString(): String = this.value.toString
252 def equals(that: Nat): Boolean = this.value == that.value
254 def as_BigInt: BigInt = this.value
255 def as_Int: Int = if (this.value >= scala.Int.MinValue && this.value <= scala.Int.MaxValue)
257 else error("Int value out of range: " + this.value.toString)
259 def +(that: Nat): Nat = new Nat(this.value + that.value)
260 def -(that: Nat): Nat = Nat(this.value - that.value)
261 def *(that: Nat): Nat = new Nat(this.value * that.value)
263 def /%(that: Nat): (Nat, Nat) = if (that.value == 0) (new Nat(0), this)
265 val (k, l) = this.value /% that.value
266 (new Nat(k), new Nat(l))
269 def <=(that: Nat): Boolean = this.value <= that.value
271 def <(that: Nat): Boolean = this.value < that.value
276 code_reserved Scala Nat
282 code_instance nat :: equal
290 "number_nat_inst.number_of_nat i = nat (number_of i)"
291 -- {* this interacts as desired with @{thm nat_number_of_def} *}
292 by (simp add: number_nat_inst.number_of_nat)
295 fold (Numeral.add_code @{const_name number_nat_inst.number_of_nat}
296 false Code_Printer.literal_positive_numeral) ["SML", "OCaml", "Haskell", "Scala"]
300 Since natural numbers are implemented
301 using integers in ML, the coercion function @{const "of_nat"} of type
302 @{typ "nat \<Rightarrow> int"} is simply implemented by the identity function.
303 For the @{const nat} function for converting an integer to a natural
304 number, we give a specific implementation using an ML function that
305 returns its input value, provided that it is non-negative, and otherwise
309 definition int :: "nat \<Rightarrow> int" where
310 [code del, code_abbrev]: "int = of_nat"
312 lemma int_code' [code]:
313 "int (number_of l) = (if neg (number_of l \<Colon> int) then 0 else number_of l)"
314 unfolding int_nat_number_of [folded int_def] ..
316 lemma nat_code' [code]:
317 "nat (number_of l) = (if neg (number_of l \<Colon> int) then 0 else number_of l)"
318 unfolding nat_number_of_def number_of_is_id neg_def by simp
320 lemma of_nat_int: (* FIXME delete candidate *)
321 "of_nat = int" by (simp add: int_def)
323 lemma of_nat_aux_int [code_unfold]:
324 "of_nat_aux (\<lambda>i. i + 1) k 0 = int k"
325 by (simp add: int_def Nat.of_nat_code)
332 (SML "IntInf.max/ (0,/ _)")
333 (OCaml "Big'_int.max'_big'_int/ Big'_int.zero'_big'_int")
334 (Eval "Integer.max/ _/ 0")
336 text {* For Haskell and Scala, things are slightly different again. *}
338 code_const int and nat
339 (Haskell "toInteger" and "fromInteger")
340 (Scala "!_.as'_BigInt" and "Nat")
342 text {* Conversion from and to code numerals. *}
344 code_const Code_Numeral.of_nat
347 (Haskell "!(fromInteger/ ./ toInteger)")
348 (Scala "!Natural(_.as'_BigInt)")
351 code_const Code_Numeral.nat_of
352 (SML "IntInf.fromInt")
354 (Haskell "!(fromInteger/ ./ toInteger)")
355 (Scala "!Nat(_.as'_BigInt)")
358 text {* Using target language arithmetic operations whenever appropriate *}
360 code_const "op + \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat"
361 (SML "IntInf.+ ((_), (_))")
362 (OCaml "Big'_int.add'_big'_int")
363 (Haskell infixl 6 "+")
367 code_const "op - \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat"
368 (Haskell infixl 6 "-")
371 code_const "op * \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat"
372 (SML "IntInf.* ((_), (_))")
373 (OCaml "Big'_int.mult'_big'_int")
374 (Haskell infixl 7 "*")
378 code_const divmod_nat
379 (SML "IntInf.divMod/ ((_),/ (_))")
380 (OCaml "Big'_int.quomod'_big'_int")
382 (Scala infixl 8 "/%")
383 (Eval "Integer.div'_mod")
385 code_const "HOL.equal \<Colon> nat \<Rightarrow> nat \<Rightarrow> bool"
386 (SML "!((_ : IntInf.int) = _)")
387 (OCaml "Big'_int.eq'_big'_int")
388 (Haskell infix 4 "==")
389 (Scala infixl 5 "==")
392 code_const "op \<le> \<Colon> nat \<Rightarrow> nat \<Rightarrow> bool"
393 (SML "IntInf.<= ((_), (_))")
394 (OCaml "Big'_int.le'_big'_int")
395 (Haskell infix 4 "<=")
396 (Scala infixl 4 "<=")
399 code_const "op < \<Colon> nat \<Rightarrow> nat \<Rightarrow> bool"
400 (SML "IntInf.< ((_), (_))")
401 (OCaml "Big'_int.lt'_big'_int")
402 (Haskell infix 4 "<")
407 text {* Evaluation *}
409 lemma [code, code del]:
410 "(Code_Evaluation.term_of \<Colon> nat \<Rightarrow> term) = Code_Evaluation.term_of" ..
412 code_const "Code_Evaluation.term_of \<Colon> nat \<Rightarrow> term"
413 (SML "HOLogic.mk'_number/ HOLogic.natT")
415 text {* Evaluation with @{text "Quickcheck_Narrowing"} does not work, as
416 @{text "code_module"} is very aggressive leading to bad Haskell code.
417 Therefore, we simply deactivate the narrowing-based quickcheck from here on.
420 declare [[quickcheck_narrowing_active = false]]
422 text {* Module names *}
427 code_modulename OCaml
430 code_modulename Haskell