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_Index 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 inline]:
30 "0 = (Numeral0 :: nat)"
32 lemmas [code post] = zero_nat_code [symmetric]
34 lemma one_nat_code [code, code inline]:
35 "1 = (Numeral1 :: nat)"
37 lemmas [code post] = one_nat_code [symmetric]
39 lemma Suc_code [code]:
43 lemma plus_nat_code [code]:
44 "n + m = nat (of_nat n + of_nat m)"
47 lemma minus_nat_code [code]:
48 "n - m = nat (of_nat n - of_nat m)"
51 lemma times_nat_code [code]:
52 "n * m = nat (of_nat n * of_nat m)"
53 unfolding of_nat_mult [symmetric] by simp
55 text {* Specialized @{term "op div \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat"}
56 and @{term "op mod \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat"} operations. *}
58 definition divmod_aux :: "nat \<Rightarrow> nat \<Rightarrow> nat \<times> nat" where
59 [code del]: "divmod_aux = Divides.divmod"
62 "Divides.divmod n m = (if m = 0 then (0, n) else divmod_aux n m)"
63 unfolding divmod_aux_def divmod_div_mod by simp
65 lemma divmod_aux_code [code]:
66 "divmod_aux n m = (nat (of_nat n div of_nat m), nat (of_nat n mod of_nat m))"
67 unfolding divmod_aux_def divmod_div_mod zdiv_int [symmetric] zmod_int [symmetric] by simp
69 lemma eq_nat_code [code]:
70 "eq_class.eq n m \<longleftrightarrow> eq_class.eq (of_nat n \<Colon> int) (of_nat m)"
73 lemma eq_nat_refl [code nbe]:
74 "eq_class.eq (n::nat) n \<longleftrightarrow> True"
77 lemma less_eq_nat_code [code]:
78 "n \<le> m \<longleftrightarrow> (of_nat n \<Colon> int) \<le> of_nat m"
81 lemma less_nat_code [code]:
82 "n < m \<longleftrightarrow> (of_nat n \<Colon> int) < of_nat m"
85 subsection {* Case analysis *}
88 Case analysis on natural numbers is rephrased using a conditional
92 lemma [code, code unfold]:
93 "nat_case = (\<lambda>f g n. if n = 0 then f else g (n - 1))"
94 by (auto simp add: expand_fun_eq dest!: gr0_implies_Suc)
97 subsection {* Preprocessors *}
100 In contrast to @{term "Suc n"}, the term @{term "n + (1::nat)"} is no longer
101 a constructor term. Therefore, all occurrences of this term in a position
102 where a pattern is expected (i.e.\ on the left-hand side of a recursion
103 equation or in the arguments of an inductive relation in an introduction
104 rule) must be eliminated.
105 This can be accomplished by applying the following transformation rules:
108 lemma Suc_if_eq': "(\<And>n. f (Suc n) = h n) \<Longrightarrow> f 0 = g \<Longrightarrow>
109 f n = (if n = 0 then g else h (n - 1))"
110 by (cases n) simp_all
112 lemma Suc_if_eq: "(\<And>n. f (Suc n) \<equiv> h n) \<Longrightarrow> f 0 \<equiv> g \<Longrightarrow>
113 f n \<equiv> if n = 0 then g else h (n - 1)"
114 by (rule eq_reflection, rule Suc_if_eq')
115 (rule meta_eq_to_obj_eq, assumption,
116 rule meta_eq_to_obj_eq, assumption)
118 lemma Suc_clause: "(\<And>n. P n (Suc n)) \<Longrightarrow> n \<noteq> 0 \<Longrightarrow> P (n - 1) n"
119 by (cases n) simp_all
122 The rules above are built into a preprocessor that is plugged into
123 the code generator. Since the preprocessor for introduction rules
124 does not know anything about modes, some of the modes that worked
125 for the canonical representation of natural numbers may no longer work.
132 fun gen_remove_suc Suc_if_eq dest_judgement thy thms =
134 val vname = Name.variant (map fst
135 (fold (Term.add_var_names o Thm.full_prop_of) thms [])) "n";
136 val cv = cterm_of thy (Var ((vname, 0), HOLogic.natT));
137 fun lhs_of th = snd (Thm.dest_comb
138 (fst (Thm.dest_comb (dest_judgement (cprop_of th)))));
139 fun rhs_of th = snd (Thm.dest_comb (dest_judgement (cprop_of th)));
140 fun find_vars ct = (case term_of ct of
141 (Const (@{const_name Suc}, _) $ Var _) => [(cv, snd (Thm.dest_comb ct))]
143 let val (ct1, ct2) = Thm.dest_comb ct
145 map (apfst (fn ct => Thm.capply ct ct2)) (find_vars ct1) @
146 map (apfst (Thm.capply ct1)) (find_vars ct2)
150 (fn th => map (pair th) (find_vars (lhs_of th))) thms;
151 fun mk_thms (th, (ct, cv')) =
155 (Conv.fconv_rule (Thm.beta_conversion true)
157 [SOME (ctyp_of_term ct)] [SOME (Thm.cabs cv ct),
158 SOME (Thm.cabs cv' (rhs_of th)), NONE, SOME cv']
159 Suc_if_eq)) (Thm.forall_intr cv' th)
161 case map_filter (fn th'' =>
162 SOME (th'', singleton
163 (Variable.trade (K (fn [th'''] => [th''' RS th'])) (Variable.thm_context th'')) th'')
164 handle THM _ => NONE) thms of
167 let val (ths1, ths2) = split_list thps
168 in SOME (subtract Thm.eq_thm (th :: ths1) thms @ ths2) end
170 in get_first mk_thms eqs end;
172 fun gen_eqn_suc_preproc Suc_if_eq dest_judgement dest_lhs thy thms =
174 val dest = dest_lhs o prop_of;
175 val contains_suc = exists_Const (fn (c, _) => c = @{const_name Suc});
177 if forall (can dest) thms andalso exists (contains_suc o dest) thms
178 then perhaps_loop (gen_remove_suc Suc_if_eq dest_judgement thy) thms
182 val eqn_suc_preproc = Code.simple_functrans (gen_eqn_suc_preproc
183 @{thm Suc_if_eq} I (fst o Logic.dest_equals));
185 fun eqn_suc_preproc' thy thms = gen_eqn_suc_preproc
186 @{thm Suc_if_eq'} (snd o Thm.dest_comb) (fst o HOLogic.dest_eq o HOLogic.dest_Trueprop) thy thms
189 fun remove_suc_clause thy thms =
191 val vname = Name.variant (map fst
192 (fold (Term.add_var_names o Thm.full_prop_of) thms [])) "x";
193 fun find_var (t as Const (@{const_name Suc}, _) $ (v as Var _)) = SOME (t, v)
194 | find_var (t $ u) = (case find_var t of NONE => find_var u | x => x)
197 let val th' = Conv.fconv_rule ObjectLogic.atomize th
198 in Option.map (pair (th, th')) (find_var (prop_of th')) end
200 case get_first find_thm thms of
202 | SOME ((th, th'), (Sucv, v)) =>
204 val cert = cterm_of (Thm.theory_of_thm th);
205 val th'' = ObjectLogic.rulify (Thm.implies_elim
206 (Conv.fconv_rule (Thm.beta_conversion true)
207 (Drule.instantiate' []
208 [SOME (cert (lambda v (Abs ("x", HOLogic.natT,
210 HOLogic.dest_Trueprop (prop_of th')))))),
211 SOME (cert v)] @{thm Suc_clause}))
212 (Thm.forall_intr (cert v) th'))
214 remove_suc_clause thy (map (fn th''' =>
215 if (op = o pairself prop_of) (th''', th) then th'' else th''') thms)
219 fun clause_suc_preproc thy ths =
221 val dest = fst o HOLogic.dest_mem o HOLogic.dest_Trueprop
223 if forall (can (dest o concl_of)) ths andalso
224 exists (fn th => exists (exists_Const (fn (c, _) => c = @{const_name Suc}))
225 (map_filter (try dest) (concl_of th :: prems_of th))) ths
226 then remove_suc_clause thy ths else ths
230 Codegen.add_preprocessor eqn_suc_preproc'
231 #> Codegen.add_preprocessor clause_suc_preproc
232 #> Code.add_functrans ("eqn_Suc", eqn_suc_preproc)
239 subsection {* Target language setup *}
242 For ML, we map @{typ nat} to target language integers, where we
243 assert that values are always non-negative.
248 (OCaml "Big'_int.big'_int")
253 val term_of_nat = HOLogic.mk_number HOLogic.natT;
257 let val n = random_range 0 i
258 in (n, fn () => term_of_nat n) end;
262 For Haskell we define our own @{typ nat} type. The reason
263 is that we have to distinguish type class instances
264 for @{typ nat} and @{typ int}.
267 code_include Haskell "Nat" {*
268 newtype Nat = Nat Integer deriving (Show, Eq);
270 instance Num Nat where {
271 fromInteger k = Nat (if k >= 0 then k else 0);
272 Nat n + Nat m = Nat (n + m);
273 Nat n - Nat m = fromInteger (n - m);
274 Nat n * Nat m = Nat (n * m);
277 negate n = error "negate Nat";
280 instance Ord Nat where {
281 Nat n <= Nat m = n <= m;
282 Nat n < Nat m = n < m;
285 instance Real Nat where {
286 toRational (Nat n) = toRational n;
289 instance Enum Nat where {
290 toEnum k = fromInteger (toEnum k);
291 fromEnum (Nat n) = fromEnum n;
294 instance Integral Nat where {
295 toInteger (Nat n) = n;
296 divMod n m = quotRem n m;
297 quotRem (Nat n) (Nat m) = (Nat k, Nat l) where (k, l) = quotRem n m;
301 code_reserved Haskell Nat
306 code_instance nat :: eq
313 lemma [code inline, symmetric, code post]:
314 "nat (number_of i) = number_nat_inst.number_of_nat i"
315 -- {* this interacts as desired with @{thm nat_number_of_def} *}
316 by (simp add: number_nat_inst.number_of_nat)
319 fold (Numeral.add_code @{const_name number_nat_inst.number_of_nat}
320 true false) ["SML", "OCaml", "Haskell"]
324 Since natural numbers are implemented
325 using integers in ML, the coercion function @{const "of_nat"} of type
326 @{typ "nat \<Rightarrow> int"} is simply implemented by the identity function.
327 For the @{const "nat"} function for converting an integer to a natural
328 number, we give a specific implementation using an ML function that
329 returns its input value, provided that it is non-negative, and otherwise
334 int :: "nat \<Rightarrow> int"
336 [code del]: "int = of_nat"
338 lemma int_code' [code]:
339 "int (number_of l) = (if neg (number_of l \<Colon> int) then 0 else number_of l)"
340 unfolding int_nat_number_of [folded int_def] ..
342 lemma nat_code' [code]:
343 "nat (number_of l) = (if neg (number_of l \<Colon> int) then 0 else number_of l)"
344 unfolding nat_number_of_def number_of_is_id neg_def by simp
346 lemma of_nat_int [code unfold]:
347 "of_nat = int" by (simp add: int_def)
348 declare of_nat_int [symmetric, code post]
358 fun nat i = if i < 0 then 0 else i;
362 (SML "IntInf.max/ (/0,/ _)")
363 (OCaml "Big'_int.max'_big'_int/ Big'_int.zero'_big'_int")
365 text {* For Haskell, things are slightly different again. *}
367 code_const int and nat
368 (Haskell "toInteger" and "fromInteger")
370 text {* Conversion from and to indices. *}
372 code_const Code_Index.of_nat
374 (OCaml "Big'_int.int'_of'_big'_int")
377 code_const Code_Index.nat_of
378 (SML "IntInf.fromInt")
379 (OCaml "Big'_int.big'_int'_of'_int")
382 text {* Using target language arithmetic operations whenever appropriate *}
384 code_const "op + \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat"
385 (SML "IntInf.+ ((_), (_))")
386 (OCaml "Big'_int.add'_big'_int")
387 (Haskell infixl 6 "+")
389 code_const "op * \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat"
390 (SML "IntInf.* ((_), (_))")
391 (OCaml "Big'_int.mult'_big'_int")
392 (Haskell infixl 7 "*")
394 code_const divmod_aux
395 (SML "IntInf.divMod/ ((_),/ (_))")
396 (OCaml "Big'_int.quomod'_big'_int")
399 code_const "eq_class.eq \<Colon> nat \<Rightarrow> nat \<Rightarrow> bool"
400 (SML "!((_ : IntInf.int) = _)")
401 (OCaml "Big'_int.eq'_big'_int")
402 (Haskell infixl 4 "==")
404 code_const "op \<le> \<Colon> nat \<Rightarrow> nat \<Rightarrow> bool"
405 (SML "IntInf.<= ((_), (_))")
406 (OCaml "Big'_int.le'_big'_int")
407 (Haskell infix 4 "<=")
409 code_const "op < \<Colon> nat \<Rightarrow> nat \<Rightarrow> bool"
410 (SML "IntInf.< ((_), (_))")
411 (OCaml "Big'_int.lt'_big'_int")
412 (Haskell infix 4 "<")
418 "op + \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat" ("(_ +/ _)")
419 "op * \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat" ("(_ */ _)")
420 "op \<le> \<Colon> nat \<Rightarrow> nat \<Rightarrow> bool" ("(_ <=/ _)")
421 "op < \<Colon> nat \<Rightarrow> nat \<Rightarrow> bool" ("(_ </ _)")
424 text {* Evaluation *}
426 lemma [code, code del]:
427 "(Code_Eval.term_of \<Colon> nat \<Rightarrow> term) = Code_Eval.term_of" ..
429 code_const "Code_Eval.term_of \<Colon> nat \<Rightarrow> term"
430 (SML "HOLogic.mk'_number/ HOLogic.natT")
433 text {* Module names *}
438 Ring_and_Field Integer
439 Efficient_Nat Integer
441 code_modulename OCaml
444 Ring_and_Field Integer
445 Efficient_Nat Integer
447 code_modulename Haskell
450 Ring_and_Field Integer
451 Efficient_Nat Integer