src/HOL/Library/EfficientNat.thy
 author wenzelm Thu Jan 19 21:22:08 2006 +0100 (2006-01-19 ago) changeset 18708 4b3dadb4fe33 parent 18702 7dc7dcd63224 child 18757 f0d901bc0686 permissions -rw-r--r--
setup: theory -> theory;
1 (*  Title:      HOL/Library/EfficientNat.thy
2     ID:         \$Id\$
3     Author:     Stefan Berghofer, TU Muenchen
4 *)
6 header {* Implementation of natural numbers by integers *}
8 theory EfficientNat
9 imports Main
10 begin
12 text {*
13 When generating code for functions on natural numbers, the canonical
14 representation using @{term "0::nat"} and @{term "Suc"} is unsuitable for
15 computations involving large numbers. The efficiency of the generated
16 code can be improved drastically by implementing natural numbers by
17 integers. To do this, just include this theory.
18 *}
20 subsection {* Basic functions *}
22 text {*
23 The implementation of @{term "0::nat"} and @{term "Suc"} using the
24 ML integers is straightforward. Since natural numbers are implemented
25 using integers, the coercion function @{term "int"} of type
26 @{typ "nat \<Rightarrow> int"} is simply implemented by the identity function.
27 For the @{term "nat"} function for converting an integer to a natural
28 number, we give a specific implementation using an ML function that
29 returns its input value, provided that it is non-negative, and otherwise
30 returns @{text "0"}.
31 *}
33 types_code
34   nat ("int")
35 attach (term_of) {*
36 fun term_of_nat 0 = Const ("0", HOLogic.natT)
37   | term_of_nat 1 = Const ("1", HOLogic.natT)
38   | term_of_nat i = HOLogic.number_of_const HOLogic.natT \$
39       HOLogic.mk_bin (IntInf.fromInt i);
40 *}
41 attach (test) {*
42 fun gen_nat i = random_range 0 i;
43 *}
45 consts_code
46   0 :: nat ("0")
47   Suc ("(_ + 1)")
48   nat ("\<module>nat")
49 attach {*
50 fun nat i = if i < 0 then 0 else i;
51 *}
52   int ("(_)")
54 (* code_syntax_tyco nat
55   ml (atom "InfInt.int")
56   haskell (atom "Integer")
58 code_syntax_const 0 :: nat
59   ml ("0 : InfInt.int")
60   haskell (atom "0")
62 code_syntax_const Suc
63   ml (infixl 8 "_ + 1")
64   haskell (infixl 6 "_ + 1")
66 code_primconst nat
67 ml {*
68 fun nat i = if i < 0 then 0 else i;
69 *}
71 nat i = if i < 0 then 0 else i
72 *} *)
74 text {*
75 Case analysis on natural numbers is rephrased using a conditional
76 expression:
77 *}
79 lemma [code unfold]: "nat_case \<equiv> (\<lambda>f g n. if n = 0 then f else g (n - 1))"
80   apply (rule eq_reflection ext)+
81   apply (case_tac n)
82   apply simp_all
83   done
85 text {*
86 Most standard arithmetic functions on natural numbers are implemented
87 using their counterparts on the integers:
88 *}
90 lemma [code]: "m - n = nat (int m - int n)" by arith
91 lemma [code]: "m + n = nat (int m + int n)" by arith
92 lemma [code]: "m * n = nat (int m * int n)"
93   by (simp add: zmult_int)
94 lemma [code]: "m div n = nat (int m div int n)"
95   by (simp add: zdiv_int [symmetric])
96 lemma [code]: "m mod n = nat (int m mod int n)"
97   by (simp add: zmod_int [symmetric])
98 lemma [code]: "(m < n) = (int m < int n)"
99   by simp
101 subsection {* Preprocessors *}
103 text {*
104 In contrast to @{term "Suc n"}, the term @{term "n + (1::nat)"} is no longer
105 a constructor term. Therefore, all occurrences of this term in a position
106 where a pattern is expected (i.e.\ on the left-hand side of a recursion
107 equation or in the arguments of an inductive relation in an introduction
108 rule) must be eliminated.
109 This can be accomplished by applying the following transformation rules:
110 *}
112 theorem Suc_if_eq: "(\<And>n. f (Suc n) = h n) \<Longrightarrow> f 0 = g \<Longrightarrow>
113   f n = (if n = 0 then g else h (n - 1))"
114   by (case_tac n) simp_all
116 theorem Suc_clause: "(\<And>n. P n (Suc n)) \<Longrightarrow> n \<noteq> 0 \<Longrightarrow> P (n - 1) n"
117   by (case_tac n) simp_all
119 text {*
120 The rules above are built into a preprocessor that is plugged into
121 the code generator. Since the preprocessor for introduction rules
122 does not know anything about modes, some of the modes that worked
123 for the canonical representation of natural numbers may no longer work.
124 *}
126 (*<*)
127 ML {*
128 val Suc_if_eq = thm "Suc_if_eq";
130 fun remove_suc thy thms =
131   let
132     val Suc_if_eq' = Thm.transfer thy Suc_if_eq;
133     val vname = variant (map fst
134       (fold (add_term_varnames o Thm.full_prop_of) thms [])) "x";
135     val cv = cterm_of Main.thy (Var ((vname, 0), HOLogic.natT));
136     fun lhs_of th = snd (Thm.dest_comb
137       (fst (Thm.dest_comb (snd (Thm.dest_comb (cprop_of th))))));
138     fun rhs_of th = snd (Thm.dest_comb (snd (Thm.dest_comb (cprop_of th))));
139     fun find_vars ct = (case term_of ct of
140         (Const ("Suc", _) \$ Var _) => [(cv, snd (Thm.dest_comb ct))]
141       | _ \$ _ =>
142         let val (ct1, ct2) = Thm.dest_comb ct
143         in
144           map (apfst (fn ct => Thm.capply ct ct2)) (find_vars ct1) @
145           map (apfst (Thm.capply ct1)) (find_vars ct2)
146         end
147       | _ => []);
148     val eqs = List.concat (map
149       (fn th => map (pair th) (find_vars (lhs_of th))) thms);
150     fun mk_thms (th, (ct, cv')) =
151       let
152         val th' =
153           Thm.implies_elim
154            (Drule.fconv_rule (Thm.beta_conversion true)
155              (Drule.instantiate'
156                [SOME (ctyp_of_term ct)] [SOME (Thm.cabs cv ct),
157                  SOME (Thm.cabs cv' (rhs_of th)), NONE, SOME cv']
158                Suc_if_eq')) (Thm.forall_intr cv' th)
159       in
160         case List.mapPartial (fn th'' =>
161             SOME (th'', standard (Drule.freeze_all th'' RS th'))
162           handle THM _ => NONE) thms of
163             [] => NONE
164           | thps =>
165               let val (ths1, ths2) = ListPair.unzip thps
166               in SOME (gen_rems eq_thm (thms, th :: ths1) @ ths2) end
167       end
168   in
169     case Library.get_first mk_thms eqs of
170       NONE => thms
171     | SOME x => remove_suc thy x
172   end;
174 fun eqn_suc_preproc thy ths =
175   let val dest = fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of
176   in
177     if forall (can dest) ths andalso
178       exists (fn th => "Suc" mem term_consts (dest th)) ths
179     then remove_suc thy ths else ths
180   end;
182 val Suc_clause = thm "Suc_clause";
184 fun remove_suc_clause thy thms =
185   let
186     val Suc_clause' = Thm.transfer thy Suc_clause;
187     val vname = variant (map fst
188       (fold (add_term_varnames o Thm.full_prop_of) thms [])) "x";
189     fun find_var (t as Const ("Suc", _) \$ (v as Var _)) = SOME (t, v)
190       | find_var (t \$ u) = (case find_var t of NONE => find_var u | x => x)
191       | find_var _ = NONE;
192     fun find_thm th =
193       let val th' = ObjectLogic.atomize_thm th
194       in Option.map (pair (th, th')) (find_var (prop_of th')) end
195   in
196     case get_first find_thm thms of
197       NONE => thms
198     | SOME ((th, th'), (Sucv, v)) =>
199         let
200           val cert = cterm_of (Thm.theory_of_thm th);
201           val th'' = ObjectLogic.rulify (Thm.implies_elim
202             (Drule.fconv_rule (Thm.beta_conversion true)
203               (Drule.instantiate' []
204                 [SOME (cert (lambda v (Abs ("x", HOLogic.natT,
205                    abstract_over (Sucv,
206                      HOLogic.dest_Trueprop (prop_of th')))))),
207                  SOME (cert v)] Suc_clause'))
208             (Thm.forall_intr (cert v) th'))
209         in
210           remove_suc_clause thy (map (fn th''' =>
211             if th''' = th then th'' else th''') thms)
212         end
213   end;
215 fun clause_suc_preproc thy ths =
216   let val dest = fst o HOLogic.dest_mem o HOLogic.dest_Trueprop
217   in
218     if forall (can (dest o concl_of)) ths andalso
219       exists (fn th => "Suc" mem foldr add_term_consts
220         [] (List.mapPartial (try dest) (concl_of th :: prems_of th))) ths
221     then remove_suc_clause thy ths else ths
222   end;
224 val suc_preproc_setup =
225   Codegen.add_preprocessor eqn_suc_preproc #>