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 fun eqn_suc_preproc thy = map fst
183 #> gen_eqn_suc_preproc
184 @{thm Suc_if_eq} I (fst o Logic.dest_equals) thy
185 #> (Option.map o map) (Code_Unit.mk_eqn thy);
187 fun eqn_suc_preproc' thy thms = gen_eqn_suc_preproc
188 @{thm Suc_if_eq'} (snd o Thm.dest_comb) (fst o HOLogic.dest_eq o HOLogic.dest_Trueprop) thy thms
191 fun remove_suc_clause thy thms =
193 val vname = Name.variant (map fst
194 (fold (Term.add_var_names o Thm.full_prop_of) thms [])) "x";
195 fun find_var (t as Const (@{const_name Suc}, _) $ (v as Var _)) = SOME (t, v)
196 | find_var (t $ u) = (case find_var t of NONE => find_var u | x => x)
199 let val th' = Conv.fconv_rule ObjectLogic.atomize th
200 in Option.map (pair (th, th')) (find_var (prop_of th')) end
202 case get_first find_thm thms of
204 | SOME ((th, th'), (Sucv, v)) =>
206 val cert = cterm_of (Thm.theory_of_thm th);
207 val th'' = ObjectLogic.rulify (Thm.implies_elim
208 (Conv.fconv_rule (Thm.beta_conversion true)
209 (Drule.instantiate' []
210 [SOME (cert (lambda v (Abs ("x", HOLogic.natT,
212 HOLogic.dest_Trueprop (prop_of th')))))),
213 SOME (cert v)] @{thm Suc_clause}))
214 (Thm.forall_intr (cert v) th'))
216 remove_suc_clause thy (map (fn th''' =>
217 if (op = o pairself prop_of) (th''', th) then th'' else th''') thms)
221 fun clause_suc_preproc thy ths =
223 val dest = fst o HOLogic.dest_mem o HOLogic.dest_Trueprop
225 if forall (can (dest o concl_of)) ths andalso
226 exists (fn th => exists (exists_Const (fn (c, _) => c = @{const_name Suc}))
227 (map_filter (try dest) (concl_of th :: prems_of th))) ths
228 then remove_suc_clause thy ths else ths
232 Codegen.add_preprocessor eqn_suc_preproc'
233 #> Codegen.add_preprocessor clause_suc_preproc
234 #> Code.add_functrans ("eqn_Suc", eqn_suc_preproc)
241 subsection {* Target language setup *}
244 For ML, we map @{typ nat} to target language integers, where we
245 assert that values are always non-negative.
250 (OCaml "Big'_int.big'_int")
255 val term_of_nat = HOLogic.mk_number HOLogic.natT;
259 let val n = random_range 0 i
260 in (n, fn () => term_of_nat n) end;
264 For Haskell we define our own @{typ nat} type. The reason
265 is that we have to distinguish type class instances
266 for @{typ nat} and @{typ int}.
269 code_include Haskell "Nat" {*
270 newtype Nat = Nat Integer deriving (Show, Eq);
272 instance Num Nat where {
273 fromInteger k = Nat (if k >= 0 then k else 0);
274 Nat n + Nat m = Nat (n + m);
275 Nat n - Nat m = fromInteger (n - m);
276 Nat n * Nat m = Nat (n * m);
279 negate n = error "negate Nat";
282 instance Ord Nat where {
283 Nat n <= Nat m = n <= m;
284 Nat n < Nat m = n < m;
287 instance Real Nat where {
288 toRational (Nat n) = toRational n;
291 instance Enum Nat where {
292 toEnum k = fromInteger (toEnum k);
293 fromEnum (Nat n) = fromEnum n;
296 instance Integral Nat where {
297 toInteger (Nat n) = n;
298 divMod n m = quotRem n m;
299 quotRem (Nat n) (Nat m) = (Nat k, Nat l) where (k, l) = quotRem n m;
303 code_reserved Haskell Nat
308 code_instance nat :: eq
315 lemma [code inline, symmetric, code post]:
316 "nat (number_of i) = number_nat_inst.number_of_nat i"
317 -- {* this interacts as desired with @{thm nat_number_of_def} *}
318 by (simp add: number_nat_inst.number_of_nat)
321 fold (Numeral.add_code @{const_name number_nat_inst.number_of_nat}
322 true false) ["SML", "OCaml", "Haskell"]
326 Since natural numbers are implemented
327 using integers in ML, the coercion function @{const "of_nat"} of type
328 @{typ "nat \<Rightarrow> int"} is simply implemented by the identity function.
329 For the @{const "nat"} function for converting an integer to a natural
330 number, we give a specific implementation using an ML function that
331 returns its input value, provided that it is non-negative, and otherwise
336 int :: "nat \<Rightarrow> int"
338 [code del]: "int = of_nat"
340 lemma int_code' [code]:
341 "int (number_of l) = (if neg (number_of l \<Colon> int) then 0 else number_of l)"
342 unfolding int_nat_number_of [folded int_def] ..
344 lemma nat_code' [code]:
345 "nat (number_of l) = (if neg (number_of l \<Colon> int) then 0 else number_of l)"
346 unfolding nat_number_of_def number_of_is_id neg_def by simp
348 lemma of_nat_int [code unfold]:
349 "of_nat = int" by (simp add: int_def)
350 declare of_nat_int [symmetric, code post]
360 fun nat i = if i < 0 then 0 else i;
364 (SML "IntInf.max/ (/0,/ _)")
365 (OCaml "Big'_int.max'_big'_int/ Big'_int.zero'_big'_int")
367 text {* For Haskell, things are slightly different again. *}
369 code_const int and nat
370 (Haskell "toInteger" and "fromInteger")
372 text {* Conversion from and to indices. *}
374 code_const Code_Index.of_nat
376 (OCaml "Big'_int.int'_of'_big'_int")
379 code_const Code_Index.nat_of
380 (SML "IntInf.fromInt")
381 (OCaml "Big'_int.big'_int'_of'_int")
384 text {* Using target language arithmetic operations whenever appropriate *}
386 code_const "op + \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat"
387 (SML "IntInf.+ ((_), (_))")
388 (OCaml "Big'_int.add'_big'_int")
389 (Haskell infixl 6 "+")
391 code_const "op * \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat"
392 (SML "IntInf.* ((_), (_))")
393 (OCaml "Big'_int.mult'_big'_int")
394 (Haskell infixl 7 "*")
396 code_const divmod_aux
397 (SML "IntInf.divMod/ ((_),/ (_))")
398 (OCaml "Big'_int.quomod'_big'_int")
401 code_const "eq_class.eq \<Colon> nat \<Rightarrow> nat \<Rightarrow> bool"
402 (SML "!((_ : IntInf.int) = _)")
403 (OCaml "Big'_int.eq'_big'_int")
404 (Haskell infixl 4 "==")
406 code_const "op \<le> \<Colon> nat \<Rightarrow> nat \<Rightarrow> bool"
407 (SML "IntInf.<= ((_), (_))")
408 (OCaml "Big'_int.le'_big'_int")
409 (Haskell infix 4 "<=")
411 code_const "op < \<Colon> nat \<Rightarrow> nat \<Rightarrow> bool"
412 (SML "IntInf.< ((_), (_))")
413 (OCaml "Big'_int.lt'_big'_int")
414 (Haskell infix 4 "<")
420 "op + \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat" ("(_ +/ _)")
421 "op * \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat" ("(_ */ _)")
422 "op \<le> \<Colon> nat \<Rightarrow> nat \<Rightarrow> bool" ("(_ <=/ _)")
423 "op < \<Colon> nat \<Rightarrow> nat \<Rightarrow> bool" ("(_ </ _)")
426 text {* Evaluation *}
428 lemma [code, code del]:
429 "(Code_Eval.term_of \<Colon> nat \<Rightarrow> term) = Code_Eval.term_of" ..
431 code_const "Code_Eval.term_of \<Colon> nat \<Rightarrow> term"
432 (SML "HOLogic.mk'_number/ HOLogic.natT")
435 text {* Module names *}
440 Ring_and_Field Integer
441 Efficient_Nat Integer
443 code_modulename OCaml
446 Ring_and_Field Integer
447 Efficient_Nat Integer
449 code_modulename Haskell
452 Ring_and_Field Integer
453 Efficient_Nat Integer