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