src/HOL/Library/EfficientNat.thy
 author paulson Tue Jun 28 15:27:45 2005 +0200 (2005-06-28) changeset 16587 b34c8aa657a5 parent 16295 cd7a83dae4f9 child 16770 1f1b1fae30e4 permissions -rw-r--r--
Constant "If" is now local
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 nat ("int")
34 consts_code
35   0 :: nat ("0")
36   Suc ("(_ + 1)")
37   nat ("nat")
38   int ("(_)")
40 ML {*
41 fun nat i = if i < 0 then 0 else i;
42 *}
44 text {*
45 Case analysis on natural numbers is rephrased using a conditional
46 expression:
47 *}
49 lemma [code unfold]: "nat_case \<equiv> (\<lambda>f g n. if n = 0 then f else g (n - 1))"
50   apply (rule eq_reflection ext)+
51   apply (case_tac n)
52   apply simp_all
53   done
55 text {*
56 Most standard arithmetic functions on natural numbers are implemented
57 using their counterparts on the integers:
58 *}
60 lemma [code]: "m - n = nat (int m - int n)" by arith
61 lemma [code]: "m + n = nat (int m + int n)" by arith
62 lemma [code]: "m * n = nat (int m * int n)"
63   by (simp add: zmult_int)
64 lemma [code]: "m div n = nat (int m div int n)"
65   by (simp add: zdiv_int [symmetric])
66 lemma [code]: "m mod n = nat (int m mod int n)"
67   by (simp add: zmod_int [symmetric])
68 lemma [code]: "(m < n) = (int m < int n)"
69   by simp
71 subsection {* Preprocessors *}
73 text {*
74 In contrast to @{term "Suc n"}, the term @{term "n + (1::nat)"} is no longer
75 a constructor term. Therefore, all occurrences of this term in a position
76 where a pattern is expected (i.e.\ on the left-hand side of a recursion
77 equation or in the arguments of an inductive relation in an introduction
78 rule) must be eliminated.
79 This can be accomplished by applying the following transformation rules:
80 *}
82 theorem Suc_if_eq: "f 0 = g \<Longrightarrow> (\<And>n. f (Suc n) = h n) \<Longrightarrow>
83   f n = (if n = 0 then g else h (n - 1))"
84   by (case_tac n) simp_all
86 theorem Suc_clause: "(\<And>n. P n (Suc n)) \<Longrightarrow> n \<noteq> 0 \<Longrightarrow> P (n - 1) n"
87   by (case_tac n) simp_all
89 text {*
90 The rules above are built into a preprocessor that is plugged into
91 the code generator. Since the preprocessor for introduction rules
92 does not know anything about modes, some of the modes that worked
93 for the canonical representation of natural numbers may no longer work.
94 *}
96 (*<*)
97 ML {*
98 val Suc_if_eq = thm "Suc_if_eq";
100 fun remove_suc thy thms =
101   let
102     val Suc_if_eq' = Thm.transfer thy Suc_if_eq;
103     val ctzero = cterm_of (sign_of Main.thy) HOLogic.zero;
104     val vname = variant (map fst
105       (Library.foldl add_term_varnames ([], map prop_of thms))) "x";
106     val cv = cterm_of (sign_of Main.thy) (Var ((vname, 0), HOLogic.natT));
107     fun lhs_of th = snd (Thm.dest_comb
108       (fst (Thm.dest_comb (snd (Thm.dest_comb (cprop_of th))))));
109     fun rhs_of th = snd (Thm.dest_comb (snd (Thm.dest_comb (cprop_of th))));
110     fun find_vars ct = (case term_of ct of
111         (Const ("Suc", _) \$ Var _) => [((cv, ctzero), snd (Thm.dest_comb ct))]
112       | _ \$ _ =>
113         let val (ct1, ct2) = Thm.dest_comb ct
114         in
115           map (apfst (pairself (fn ct => Thm.capply ct ct2))) (find_vars ct1) @
116           map (apfst (pairself (Thm.capply ct1))) (find_vars ct2)
117         end
118       | _ => []);
119     val eqs1 = List.concat (map
120       (fn th => map (pair th) (find_vars (lhs_of th))) thms);
121     val eqs2 = map (fn x as (_, ((_, ctzero), _)) => (x, List.mapPartial (fn th =>
122       SOME (th, Thm.cterm_match (lhs_of th, ctzero))
123         handle Pattern.MATCH => NONE) thms)) eqs1;
124     fun distinct_vars vs = forall is_Var vs andalso null (duplicates vs);
125     val eqs2' = map (apsnd (List.filter (fn (_, (_, s)) =>
126       distinct_vars (map (term_of o snd) s)))) eqs2;
127     fun mk_thms b ((th, ((ct, _), cv')), (th', s) :: _) =
128       let
129         val th'' = Thm.instantiate s th';
130         val th''' =
131           Thm.implies_elim (Thm.implies_elim
132            (Drule.fconv_rule (Thm.beta_conversion true)
133              (Drule.instantiate'
134                [SOME (ctyp_of_term ct)] [SOME (Thm.cabs cv ct),
135                  SOME (rhs_of th''), SOME (Thm.cabs cv' (rhs_of th)), SOME cv']
136                Suc_if_eq')) th'') (Thm.forall_intr cv' th)
137       in
138         List.mapPartial (fn thm =>
139           if thm = th then SOME th'''
140           else if b andalso thm = th' then NONE
141           else SOME thm) thms
142       end
143   in
144     case Library.find_first (not o null o snd) eqs2' of
145       NONE => (case Library.find_first (not o null o snd) eqs2 of
146         NONE => thms
147       | SOME x => remove_suc thy (mk_thms false x))
148     | SOME x => remove_suc thy (mk_thms true x)
149   end;
151 fun eqn_suc_preproc thy ths =
152   let val dest = fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of
153   in
154     if forall (can dest) ths andalso
155       exists (fn th => "Suc" mem term_consts (dest th)) ths
156     then remove_suc thy ths else ths
157   end;
159 val Suc_clause = thm "Suc_clause";
161 fun remove_suc_clause thy thms =
162   let
163     val Suc_clause' = Thm.transfer thy Suc_clause;
164     val vname = variant (map fst
165       (Library.foldl add_term_varnames ([], map prop_of thms))) "x";
166     fun find_var (t as Const ("Suc", _) \$ (v as Var _)) = SOME (t, v)
167       | find_var (t \$ u) = (case find_var t of NONE => find_var u | x => x)
168       | find_var _ = NONE;
169     fun find_thm th =
170       let val th' = ObjectLogic.atomize_thm th
171       in Option.map (pair (th, th')) (find_var (prop_of th')) end
172   in
173     case get_first find_thm thms of
174       NONE => thms
175     | SOME ((th, th'), (Sucv, v)) =>
176         let
177           val cert = cterm_of (sign_of_thm th);
178           val th'' = ObjectLogic.rulify (Thm.implies_elim
179             (Drule.fconv_rule (Thm.beta_conversion true)
180               (Drule.instantiate' []
181                 [SOME (cert (lambda v (Abs ("x", HOLogic.natT,
182                    abstract_over (Sucv,
183                      HOLogic.dest_Trueprop (prop_of th')))))),
184                  SOME (cert v)] Suc_clause'))
185             (Thm.forall_intr (cert v) th'))
186         in
187           remove_suc_clause thy (map (fn th''' =>
188             if th''' = th then th'' else th''') thms)
189         end
190   end;
192 fun clause_suc_preproc thy ths =
193   let val dest = fst o HOLogic.dest_mem o HOLogic.dest_Trueprop
194   in
195     if forall (can (dest o concl_of)) ths andalso
196       exists (fn th => "Suc" mem foldr add_term_consts
197         [] (List.mapPartial (try dest) (concl_of th :: prems_of th))) ths
198     then remove_suc_clause thy ths else ths
199   end;
201 val suc_preproc_setup =