moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
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
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 = divmod"
62 "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 (case_tac n) simp_all
112 lemma Suc_clause: "(\<And>n. P n (Suc n)) \<Longrightarrow> n \<noteq> 0 \<Longrightarrow> P (n - 1) n"
113 by (case_tac n) simp_all
116 The rules above are built into a preprocessor that is plugged into
117 the code generator. Since the preprocessor for introduction rules
118 does not know anything about modes, some of the modes that worked
119 for the canonical representation of natural numbers may no longer work.
126 fun remove_suc thy thms =
128 val vname = Name.variant (map fst
129 (fold (Term.add_var_names o Thm.full_prop_of) thms [])) "x";
130 val cv = cterm_of thy (Var ((vname, 0), HOLogic.natT));
131 fun lhs_of th = snd (Thm.dest_comb
132 (fst (Thm.dest_comb (snd (Thm.dest_comb (cprop_of th))))));
133 fun rhs_of th = snd (Thm.dest_comb (snd (Thm.dest_comb (cprop_of th))));
134 fun find_vars ct = (case term_of ct of
135 (Const ("Suc", _) $ Var _) => [(cv, snd (Thm.dest_comb ct))]
137 let val (ct1, ct2) = Thm.dest_comb ct
139 map (apfst (fn ct => Thm.capply ct ct2)) (find_vars ct1) @
140 map (apfst (Thm.capply ct1)) (find_vars ct2)
144 (fn th => map (pair th) (find_vars (lhs_of th))) thms;
145 fun mk_thms (th, (ct, cv')) =
149 (Conv.fconv_rule (Thm.beta_conversion true)
151 [SOME (ctyp_of_term ct)] [SOME (Thm.cabs cv ct),
152 SOME (Thm.cabs cv' (rhs_of th)), NONE, SOME cv']
153 @{thm Suc_if_eq})) (Thm.forall_intr cv' th)
155 case map_filter (fn th'' =>
156 SOME (th'', singleton
157 (Variable.trade (K (fn [th'''] => [th''' RS th'])) (Variable.thm_context th'')) th'')
158 handle THM _ => NONE) thms of
161 let val (ths1, ths2) = split_list thps
162 in SOME (subtract Thm.eq_thm (th :: ths1) thms @ ths2) end
164 in case get_first mk_thms eqs of
166 | SOME x => remove_suc thy x
169 fun eqn_suc_preproc thy ths =
171 val dest = fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of;
172 fun contains_suc t = member (op =) (OldTerm.term_consts t) @{const_name Suc};
174 if forall (can dest) ths andalso
175 exists (contains_suc o dest) ths
176 then remove_suc thy ths else ths
179 fun remove_suc_clause thy thms =
181 val vname = Name.variant (map fst
182 (fold (Term.add_var_names o Thm.full_prop_of) thms [])) "x";
183 fun find_var (t as Const (@{const_name Suc}, _) $ (v as Var _)) = SOME (t, v)
184 | find_var (t $ u) = (case find_var t of NONE => find_var u | x => x)
187 let val th' = Conv.fconv_rule ObjectLogic.atomize th
188 in Option.map (pair (th, th')) (find_var (prop_of th')) end
190 case get_first find_thm thms of
192 | SOME ((th, th'), (Sucv, v)) =>
194 val cert = cterm_of (Thm.theory_of_thm th);
195 val th'' = ObjectLogic.rulify (Thm.implies_elim
196 (Conv.fconv_rule (Thm.beta_conversion true)
197 (Drule.instantiate' []
198 [SOME (cert (lambda v (Abs ("x", HOLogic.natT,
200 HOLogic.dest_Trueprop (prop_of th')))))),
201 SOME (cert v)] @{thm Suc_clause}))
202 (Thm.forall_intr (cert v) th'))
204 remove_suc_clause thy (map (fn th''' =>
205 if (op = o pairself prop_of) (th''', th) then th'' else th''') thms)
209 fun clause_suc_preproc thy ths =
211 val dest = fst o HOLogic.dest_mem o HOLogic.dest_Trueprop
213 if forall (can (dest o concl_of)) ths andalso
214 exists (fn th => member (op =) (foldr OldTerm.add_term_consts
215 [] (map_filter (try dest) (concl_of th :: prems_of th))) "Suc") ths
216 then remove_suc_clause thy ths else ths
219 fun lift f thy eqns1 =
221 val eqns2 = burrow_fst Drule.zero_var_indexes_list eqns1;
222 val thms3 = try (map fst
223 #> map (fn thm => thm RS @{thm meta_eq_to_obj_eq})
225 #> map (fn thm => thm RS @{thm eq_reflection})
226 #> map (Conv.fconv_rule Drule.beta_eta_conversion)) eqns2;
227 val thms4 = Option.map Drule.zero_var_indexes_list thms3;
230 | SOME thms4 => if Thm.eq_thms (map fst eqns2, thms4)
231 then NONE else SOME (map (apfst (AxClass.overload thy) o Code_Unit.mk_eqn thy) thms4)
236 Codegen.add_preprocessor eqn_suc_preproc
237 #> Codegen.add_preprocessor clause_suc_preproc
238 #> Code.add_functrans ("eqn_Suc", lift eqn_suc_preproc)
239 #> Code.add_functrans ("clause_Suc", lift clause_suc_preproc)
246 subsection {* Target language setup *}
249 For ML, we map @{typ nat} to target language integers, where we
250 assert that values are always non-negative.
255 (OCaml "Big'_int.big'_int")
260 val term_of_nat = HOLogic.mk_number HOLogic.natT;
264 let val n = random_range 0 i
265 in (n, fn () => term_of_nat n) end;
269 For Haskell we define our own @{typ nat} type. The reason
270 is that we have to distinguish type class instances
271 for @{typ nat} and @{typ int}.
274 code_include Haskell "Nat" {*
275 newtype Nat = Nat Integer deriving (Show, Eq);
277 instance Num Nat where {
278 fromInteger k = Nat (if k >= 0 then k else 0);
279 Nat n + Nat m = Nat (n + m);
280 Nat n - Nat m = fromInteger (n - m);
281 Nat n * Nat m = Nat (n * m);
284 negate n = error "negate Nat";
287 instance Ord Nat where {
288 Nat n <= Nat m = n <= m;
289 Nat n < Nat m = n < m;
292 instance Real Nat where {
293 toRational (Nat n) = toRational n;
296 instance Enum Nat where {
297 toEnum k = fromInteger (toEnum k);
298 fromEnum (Nat n) = fromEnum n;
301 instance Integral Nat where {
302 toInteger (Nat n) = n;
303 divMod n m = quotRem n m;
304 quotRem (Nat n) (Nat m) = (Nat k, Nat l) where (k, l) = quotRem n m;
308 code_reserved Haskell Nat
313 code_instance nat :: eq
320 lemma [code inline, symmetric, code post]:
321 "nat (number_of i) = number_nat_inst.number_of_nat i"
322 -- {* this interacts as desired with @{thm nat_number_of_def} *}
323 by (simp add: number_nat_inst.number_of_nat)
326 fold (Numeral.add_code @{const_name number_nat_inst.number_of_nat}
327 true false) ["SML", "OCaml", "Haskell"]
331 Since natural numbers are implemented
332 using integers in ML, the coercion function @{const "of_nat"} of type
333 @{typ "nat \<Rightarrow> int"} is simply implemented by the identity function.
334 For the @{const "nat"} function for converting an integer to a natural
335 number, we give a specific implementation using an ML function that
336 returns its input value, provided that it is non-negative, and otherwise
341 int :: "nat \<Rightarrow> int"
343 [code del]: "int = of_nat"
345 lemma int_code' [code]:
346 "int (number_of l) = (if neg (number_of l \<Colon> int) then 0 else number_of l)"
347 unfolding int_nat_number_of [folded int_def] ..
349 lemma nat_code' [code]:
350 "nat (number_of l) = (if neg (number_of l \<Colon> int) then 0 else number_of l)"
351 unfolding nat_number_of_def number_of_is_id neg_def by simp
353 lemma of_nat_int [code unfold]:
354 "of_nat = int" by (simp add: int_def)
355 declare of_nat_int [symmetric, code post]
365 fun nat i = if i < 0 then 0 else i;
369 (SML "IntInf.max/ (/0,/ _)")
370 (OCaml "Big'_int.max'_big'_int/ Big'_int.zero'_big'_int")
372 text {* For Haskell, things are slightly different again. *}
374 code_const int and nat
375 (Haskell "toInteger" and "fromInteger")
377 text {* Conversion from and to indices. *}
379 code_const index_of_nat
381 (OCaml "Big'_int.int'_of'_big'_int")
384 code_const nat_of_index
385 (SML "IntInf.fromInt")
386 (OCaml "Big'_int.big'_int'_of'_int")
389 text {* Using target language arithmetic operations whenever appropriate *}
391 code_const "op + \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat"
392 (SML "IntInf.+ ((_), (_))")
393 (OCaml "Big'_int.add'_big'_int")
394 (Haskell infixl 6 "+")
396 code_const "op * \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat"
397 (SML "IntInf.* ((_), (_))")
398 (OCaml "Big'_int.mult'_big'_int")
399 (Haskell infixl 7 "*")
401 code_const divmod_aux
402 (SML "IntInf.divMod/ ((_),/ (_))")
403 (OCaml "Big'_int.quomod'_big'_int")
406 code_const "eq_class.eq \<Colon> nat \<Rightarrow> nat \<Rightarrow> bool"
407 (SML "!((_ : IntInf.int) = _)")
408 (OCaml "Big'_int.eq'_big'_int")
409 (Haskell infixl 4 "==")
411 code_const "op \<le> \<Colon> nat \<Rightarrow> nat \<Rightarrow> bool"
412 (SML "IntInf.<= ((_), (_))")
413 (OCaml "Big'_int.le'_big'_int")
414 (Haskell infix 4 "<=")
416 code_const "op < \<Colon> nat \<Rightarrow> nat \<Rightarrow> bool"
417 (SML "IntInf.< ((_), (_))")
418 (OCaml "Big'_int.lt'_big'_int")
419 (Haskell infix 4 "<")
425 "op + \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat" ("(_ +/ _)")
426 "op * \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat" ("(_ */ _)")
427 "op \<le> \<Colon> nat \<Rightarrow> nat \<Rightarrow> bool" ("(_ <=/ _)")
428 "op < \<Colon> nat \<Rightarrow> nat \<Rightarrow> bool" ("(_ </ _)")
431 text {* Evaluation *}
433 lemma [code, code del]:
434 "(Code_Eval.term_of \<Colon> nat \<Rightarrow> term) = Code_Eval.term_of" ..
436 code_const "Code_Eval.term_of \<Colon> nat \<Rightarrow> term"
437 (SML "HOLogic.mk'_number/ HOLogic.natT")
440 text {* Module names *}
445 Ring_and_Field Integer
446 Efficient_Nat Integer
448 code_modulename OCaml
451 Ring_and_Field Integer
452 Efficient_Nat Integer
454 code_modulename Haskell
457 Ring_and_Field Integer
458 Efficient_Nat Integer