author | haftmann |
Fri, 23 Mar 2007 09:40:50 +0100 | |
changeset 22507 | 3572bc633d9a |
parent 22423 | c1836b14c63a |
child 22743 | e2b06bfe471a |
permissions | -rw-r--r-- |
15323
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
1 |
(* Title: HOL/Library/EfficientNat.thy |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
2 |
ID: $Id$ |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
3 |
Author: Stefan Berghofer, TU Muenchen |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
4 |
*) |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
5 |
|
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
6 |
header {* Implementation of natural numbers by integers *} |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
7 |
|
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
8 |
theory EfficientNat |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
9 |
imports Main |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
10 |
begin |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
11 |
|
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
12 |
text {* |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
13 |
When generating code for functions on natural numbers, the canonical |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
14 |
representation using @{term "0::nat"} and @{term "Suc"} is unsuitable for |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
15 |
computations involving large numbers. The efficiency of the generated |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
16 |
code can be improved drastically by implementing natural numbers by |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
17 |
integers. To do this, just include this theory. |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
18 |
*} |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
19 |
|
20700 | 20 |
subsection {* Logical rewrites *} |
15323
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
21 |
|
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
22 |
text {* |
20700 | 23 |
A int-to-nat conversion with domain |
24 |
restricted to non-negative ints (in contrast to @{const nat}). |
|
22320 | 25 |
Note that this restriction has no logical relevance and |
26 |
is just a kind of proof hint -- nothing prevents you from |
|
27 |
writing nonsense like @{term "nat_of_int (-4)"} |
|
16770
1f1b1fae30e4
Auxiliary functions to be used in generated code are now defined using "attach".
berghofe
parents:
16295
diff
changeset
|
28 |
*} |
1f1b1fae30e4
Auxiliary functions to be used in generated code are now defined using "attach".
berghofe
parents:
16295
diff
changeset
|
29 |
|
20641 | 30 |
definition |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21287
diff
changeset
|
31 |
nat_of_int :: "int \<Rightarrow> nat" where |
20641 | 32 |
"k \<ge> 0 \<Longrightarrow> nat_of_int k = nat k" |
19889 | 33 |
|
22395 | 34 |
lemma nat_of_int_of_number_of: |
35 |
fixes k |
|
36 |
assumes "k \<ge> 0" |
|
37 |
shows "number_of k = nat_of_int k" |
|
38 |
unfolding nat_of_int_def [OF prems] nat_number_of_def number_of_is_id .. |
|
39 |
||
40 |
lemma nat_of_int_of_number_of_aux: |
|
41 |
fixes k |
|
42 |
assumes "Numeral.Pls \<le> k \<equiv> True" |
|
43 |
shows "k \<ge> 0" |
|
44 |
using prems unfolding Pls_def by simp |
|
45 |
||
20839 | 46 |
lemma nat_of_int_int: |
47 |
"nat_of_int (int n) = n" |
|
48 |
using zero_zle_int nat_of_int_def by simp |
|
49 |
||
19889 | 50 |
text {* |
20700 | 51 |
Case analysis on natural numbers is rephrased using a conditional |
52 |
expression: |
|
15323
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
53 |
*} |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
54 |
|
20839 | 55 |
lemma [code unfold, code noinline]: "nat_case \<equiv> (\<lambda>f g n. if n = 0 then f else g (n - 1))" |
20700 | 56 |
proof - |
57 |
have rewrite: "\<And>f g n. nat_case f g n = (if n = 0 then f else g (n - 1))" |
|
58 |
proof - |
|
59 |
fix f g n |
|
60 |
show "nat_case f g n = (if n = 0 then f else g (n - 1))" |
|
61 |
by (cases n) simp_all |
|
62 |
qed |
|
63 |
show "nat_case \<equiv> (\<lambda>f g n. if n = 0 then f else g (n - 1))" |
|
64 |
by (rule eq_reflection ext rewrite)+ |
|
65 |
qed |
|
15323
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
66 |
|
20839 | 67 |
lemma [code inline]: |
21454 | 68 |
"nat_case f g n = (if n = 0 then f else g (nat_of_int (int n - 1)))" |
69 |
by (cases n) (simp_all add: nat_of_int_int) |
|
20839 | 70 |
|
15323
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
71 |
text {* |
20700 | 72 |
Most standard arithmetic functions on natural numbers are implemented |
73 |
using their counterparts on the integers: |
|
15323
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
74 |
*} |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
75 |
|
20641 | 76 |
lemma [code func]: "0 = nat_of_int 0" |
77 |
by (simp add: nat_of_int_def) |
|
78 |
lemma [code func, code inline]: "1 = nat_of_int 1" |
|
79 |
by (simp add: nat_of_int_def) |
|
80 |
lemma [code func]: "Suc n = n + 1" |
|
81 |
by simp |
|
21874 | 82 |
lemma [code]: "m + n = nat (int m + int n)" |
20641 | 83 |
by arith |
84 |
lemma [code func, code inline]: "m + n = nat_of_int (int m + int n)" |
|
85 |
by (simp add: nat_of_int_def) |
|
86 |
lemma [code, code inline]: "m - n = nat (int m - int n)" |
|
87 |
by arith |
|
21874 | 88 |
lemma [code]: "m * n = nat (int m * int n)" |
20641 | 89 |
unfolding zmult_int by simp |
90 |
lemma [code func, code inline]: "m * n = nat_of_int (int m * int n)" |
|
91 |
proof - |
|
92 |
have "int (m * n) = int m * int n" |
|
93 |
by (induct m) (simp_all add: zadd_zmult_distrib) |
|
94 |
then have "m * n = nat (int m * int n)" by auto |
|
95 |
also have "\<dots> = nat_of_int (int m * int n)" |
|
96 |
proof - |
|
97 |
have "int m \<ge> 0" and "int n \<ge> 0" by auto |
|
98 |
have "int m * int n \<ge> 0" by (rule split_mult_pos_le) auto |
|
99 |
with nat_of_int_def show ?thesis by auto |
|
100 |
qed |
|
101 |
finally show ?thesis . |
|
102 |
qed |
|
103 |
lemma [code]: "m div n = nat (int m div int n)" |
|
104 |
unfolding zdiv_int [symmetric] by simp |
|
105 |
lemma [code func]: "m div n = fst (Divides.divmod m n)" |
|
106 |
unfolding divmod_def by simp |
|
107 |
lemma [code]: "m mod n = nat (int m mod int n)" |
|
108 |
unfolding zmod_int [symmetric] by simp |
|
109 |
lemma [code func]: "m mod n = snd (Divides.divmod m n)" |
|
110 |
unfolding divmod_def by simp |
|
111 |
lemma [code, code inline]: "(m < n) \<longleftrightarrow> (int m < int n)" |
|
112 |
by simp |
|
113 |
lemma [code func, code inline]: "(m \<le> n) \<longleftrightarrow> (int m \<le> int n)" |
|
114 |
by simp |
|
21454 | 115 |
lemma [code func, code inline]: "m = n \<longleftrightarrow> int m = int n" |
116 |
by simp |
|
20641 | 117 |
lemma [code func]: "nat k = (if k < 0 then 0 else nat_of_int k)" |
118 |
proof (cases "k < 0") |
|
119 |
case True then show ?thesis by simp |
|
120 |
next |
|
121 |
case False then show ?thesis by (simp add: nat_of_int_def) |
|
122 |
qed |
|
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20453
diff
changeset
|
123 |
lemma [code func]: |
20641 | 124 |
"int_aux i n = (if int n = 0 then i else int_aux (i + 1) (nat_of_int (int n - 1)))" |
125 |
proof - |
|
126 |
have "0 < n \<Longrightarrow> int n = 1 + int (nat_of_int (int n - 1))" |
|
127 |
proof - |
|
128 |
assume prem: "n > 0" |
|
129 |
then have "int n - 1 \<ge> 0" by auto |
|
130 |
then have "nat_of_int (int n - 1) = nat (int n - 1)" by (simp add: nat_of_int_def) |
|
131 |
with prem show "int n = 1 + int (nat_of_int (int n - 1))" by simp |
|
132 |
qed |
|
133 |
then show ?thesis unfolding int_aux_def by simp |
|
134 |
qed |
|
20356 | 135 |
|
22395 | 136 |
lemma div_nat_code [code func]: |
137 |
"m div k = nat_of_int (fst (divAlg (int m, int k)))" |
|
138 |
unfolding div_def [symmetric] zdiv_int [symmetric] nat_of_int_int .. |
|
139 |
||
140 |
lemma mod_nat_code [code func]: |
|
141 |
"m mod k = nat_of_int (snd (divAlg (int m, int k)))" |
|
142 |
unfolding mod_def [symmetric] zmod_int [symmetric] nat_of_int_int .. |
|
143 |
||
144 |
||
20700 | 145 |
subsection {* Code generator setup for basic functions *} |
146 |
||
147 |
text {* |
|
148 |
@{typ nat} is no longer a datatype but embedded into the integers. |
|
149 |
*} |
|
150 |
||
22507 | 151 |
code_datatype nat_of_int |
152 |
||
20839 | 153 |
code_const "0::nat" |
21113 | 154 |
(SML "!(0 : IntInf.int)") |
21911
e29bcab0c81c
added OCaml code generation (without dictionaries)
haftmann
parents:
21874
diff
changeset
|
155 |
(OCaml "Big'_int.big'_int'_of'_int/ 0") |
21113 | 156 |
(Haskell "0") |
20839 | 157 |
|
158 |
code_const "Suc" |
|
21125 | 159 |
(SML "IntInf.+ ((_), 1)") |
21911
e29bcab0c81c
added OCaml code generation (without dictionaries)
haftmann
parents:
21874
diff
changeset
|
160 |
(OCaml "Big_int.succ'_big'_int") |
21125 | 161 |
(Haskell "!((_) + 1)") |
20839 | 162 |
|
20700 | 163 |
types_code |
164 |
nat ("int") |
|
165 |
attach (term_of) {* |
|
21846 | 166 |
val term_of_nat = HOLogic.mk_number HOLogic.natT o IntInf.fromInt; |
20700 | 167 |
*} |
168 |
attach (test) {* |
|
169 |
fun gen_nat i = random_range 0 i; |
|
170 |
*} |
|
171 |
||
172 |
code_type nat |
|
21113 | 173 |
(SML "IntInf.int") |
21911
e29bcab0c81c
added OCaml code generation (without dictionaries)
haftmann
parents:
21874
diff
changeset
|
174 |
(OCaml "Big'_int.big'_int") |
21113 | 175 |
(Haskell "Integer") |
20700 | 176 |
|
177 |
consts_code |
|
20713
823967ef47f1
renamed 0 and 1 to HOL.zero and HOL.one respectivly; introduced corresponding syntactic classes
haftmann
parents:
20700
diff
changeset
|
178 |
"HOL.zero" :: nat ("0") |
20700 | 179 |
Suc ("(_ + 1)") |
180 |
||
181 |
text {* |
|
182 |
Since natural numbers are implemented |
|
183 |
using integers, the coercion function @{const "int"} of type |
|
184 |
@{typ "nat \<Rightarrow> int"} is simply implemented by the identity function, |
|
185 |
likewise @{const nat_of_int} of type @{typ "int \<Rightarrow> nat"}. |
|
186 |
For the @{const "nat"} function for converting an integer to a natural |
|
187 |
number, we give a specific implementation using an ML function that |
|
188 |
returns its input value, provided that it is non-negative, and otherwise |
|
189 |
returns @{text "0"}. |
|
190 |
*} |
|
191 |
||
192 |
consts_code |
|
193 |
int ("(_)") |
|
194 |
nat ("\<module>nat") |
|
195 |
attach {* |
|
196 |
fun nat i = if i < 0 then 0 else i; |
|
197 |
*} |
|
198 |
||
199 |
code_const int |
|
200 |
(SML "_") |
|
21911
e29bcab0c81c
added OCaml code generation (without dictionaries)
haftmann
parents:
21874
diff
changeset
|
201 |
(OCaml "_") |
20700 | 202 |
(Haskell "_") |
203 |
||
204 |
code_const nat_of_int |
|
205 |
(SML "_") |
|
21911
e29bcab0c81c
added OCaml code generation (without dictionaries)
haftmann
parents:
21874
diff
changeset
|
206 |
(OCaml "_") |
20700 | 207 |
(Haskell "_") |
208 |
||
209 |
||
15323
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
210 |
subsection {* Preprocessors *} |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
211 |
|
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
212 |
text {* |
22395 | 213 |
Natural numerals should be expressed using @{const nat_of_int}. |
214 |
*} |
|
215 |
||
216 |
lemmas [code noinline] = nat_number_of_def |
|
217 |
||
218 |
ML {* |
|
219 |
fun nat_of_int_of_number_of thy cts = |
|
220 |
let |
|
221 |
val simplify_less = Simplifier.rewrite |
|
222 |
(HOL_basic_ss addsimps (@{thms less_numeral_code} @ @{thms less_eq_numeral_code})); |
|
223 |
fun mk_rew (t, ty) = |
|
224 |
if ty = HOLogic.natT andalso IntInf.<= (0, HOLogic.dest_numeral t) then |
|
225 |
Thm.capply @{cterm "(op \<le>) Numeral.Pls"} (Thm.cterm_of thy t) |
|
226 |
|> simplify_less |
|
227 |
|> (fn thm => @{thm nat_of_int_of_number_of_aux} OF [thm]) |
|
228 |
|> (fn thm => @{thm nat_of_int_of_number_of} OF [thm]) |
|
229 |
|> (fn thm => @{thm eq_reflection} OF [thm]) |
|
230 |
|> SOME |
|
231 |
else NONE |
|
232 |
in |
|
233 |
fold (HOLogic.add_numerals_of o Thm.term_of) cts [] |
|
234 |
|> map_filter mk_rew |
|
235 |
end; |
|
236 |
*} |
|
237 |
||
238 |
setup {* |
|
239 |
CodegenData.add_inline_proc ("nat_of_int_of_number_of", nat_of_int_of_number_of) |
|
240 |
*} |
|
241 |
||
242 |
text {* |
|
20700 | 243 |
In contrast to @{term "Suc n"}, the term @{term "n + (1::nat)"} is no longer |
244 |
a constructor term. Therefore, all occurrences of this term in a position |
|
245 |
where a pattern is expected (i.e.\ on the left-hand side of a recursion |
|
246 |
equation or in the arguments of an inductive relation in an introduction |
|
247 |
rule) must be eliminated. |
|
248 |
This can be accomplished by applying the following transformation rules: |
|
15323
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
249 |
*} |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
250 |
|
16900
e294033d1c0f
Rewrote function remove_suc, since it failed on some equations
berghofe
parents:
16861
diff
changeset
|
251 |
theorem Suc_if_eq: "(\<And>n. f (Suc n) = h n) \<Longrightarrow> f 0 = g \<Longrightarrow> |
15323
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
252 |
f n = (if n = 0 then g else h (n - 1))" |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
253 |
by (case_tac n) simp_all |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
254 |
|
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
255 |
theorem Suc_clause: "(\<And>n. P n (Suc n)) \<Longrightarrow> n \<noteq> 0 \<Longrightarrow> P (n - 1) n" |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
256 |
by (case_tac n) simp_all |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
257 |
|
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
258 |
text {* |
20700 | 259 |
The rules above are built into a preprocessor that is plugged into |
260 |
the code generator. Since the preprocessor for introduction rules |
|
261 |
does not know anything about modes, some of the modes that worked |
|
262 |
for the canonical representation of natural numbers may no longer work. |
|
15323
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
263 |
*} |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
264 |
|
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
265 |
(*<*) |
19791 | 266 |
|
15323
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
267 |
ML {* |
19791 | 268 |
local |
269 |
val Suc_if_eq = thm "Suc_if_eq"; |
|
270 |
val Suc_clause = thm "Suc_clause"; |
|
271 |
fun contains_suc t = member (op =) (term_consts t) "Suc"; |
|
272 |
in |
|
15323
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
273 |
|
15396
0a36ccb79481
Preprocessors now transfer theorems to current theory in order to
berghofe
parents:
15323
diff
changeset
|
274 |
fun remove_suc thy thms = |
15323
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
275 |
let |
15396
0a36ccb79481
Preprocessors now transfer theorems to current theory in order to
berghofe
parents:
15323
diff
changeset
|
276 |
val Suc_if_eq' = Thm.transfer thy Suc_if_eq; |
20071
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19889
diff
changeset
|
277 |
val vname = Name.variant (map fst |
20196
9a19e4de6e2e
renamed add_term_varnames to Term.add_varnames (cf. Term.add_vars etc.);
wenzelm
parents:
20105
diff
changeset
|
278 |
(fold (Term.add_varnames o Thm.full_prop_of) thms [])) "x"; |
21911
e29bcab0c81c
added OCaml code generation (without dictionaries)
haftmann
parents:
21874
diff
changeset
|
279 |
val cv = cterm_of thy (Var ((vname, 0), HOLogic.natT)); |
15323
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
280 |
fun lhs_of th = snd (Thm.dest_comb |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
281 |
(fst (Thm.dest_comb (snd (Thm.dest_comb (cprop_of th)))))); |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
282 |
fun rhs_of th = snd (Thm.dest_comb (snd (Thm.dest_comb (cprop_of th)))); |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
283 |
fun find_vars ct = (case term_of ct of |
16900
e294033d1c0f
Rewrote function remove_suc, since it failed on some equations
berghofe
parents:
16861
diff
changeset
|
284 |
(Const ("Suc", _) $ Var _) => [(cv, snd (Thm.dest_comb ct))] |
15323
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
285 |
| _ $ _ => |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
286 |
let val (ct1, ct2) = Thm.dest_comb ct |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
287 |
in |
16900
e294033d1c0f
Rewrote function remove_suc, since it failed on some equations
berghofe
parents:
16861
diff
changeset
|
288 |
map (apfst (fn ct => Thm.capply ct ct2)) (find_vars ct1) @ |
e294033d1c0f
Rewrote function remove_suc, since it failed on some equations
berghofe
parents:
16861
diff
changeset
|
289 |
map (apfst (Thm.capply ct1)) (find_vars ct2) |
15323
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
290 |
end |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
291 |
| _ => []); |
16900
e294033d1c0f
Rewrote function remove_suc, since it failed on some equations
berghofe
parents:
16861
diff
changeset
|
292 |
val eqs = List.concat (map |
15323
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
293 |
(fn th => map (pair th) (find_vars (lhs_of th))) thms); |
16900
e294033d1c0f
Rewrote function remove_suc, since it failed on some equations
berghofe
parents:
16861
diff
changeset
|
294 |
fun mk_thms (th, (ct, cv')) = |
15323
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
295 |
let |
16900
e294033d1c0f
Rewrote function remove_suc, since it failed on some equations
berghofe
parents:
16861
diff
changeset
|
296 |
val th' = |
e294033d1c0f
Rewrote function remove_suc, since it failed on some equations
berghofe
parents:
16861
diff
changeset
|
297 |
Thm.implies_elim |
15396
0a36ccb79481
Preprocessors now transfer theorems to current theory in order to
berghofe
parents:
15323
diff
changeset
|
298 |
(Drule.fconv_rule (Thm.beta_conversion true) |
15323
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
299 |
(Drule.instantiate' |
15531 | 300 |
[SOME (ctyp_of_term ct)] [SOME (Thm.cabs cv ct), |
16900
e294033d1c0f
Rewrote function remove_suc, since it failed on some equations
berghofe
parents:
16861
diff
changeset
|
301 |
SOME (Thm.cabs cv' (rhs_of th)), NONE, SOME cv'] |
e294033d1c0f
Rewrote function remove_suc, since it failed on some equations
berghofe
parents:
16861
diff
changeset
|
302 |
Suc_if_eq')) (Thm.forall_intr cv' th) |
15323
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
303 |
in |
21287 | 304 |
case map_filter (fn th'' => |
20287
8cbcb46c3c09
replaced obsolete standard/freeze_all by Variable.trade;
wenzelm
parents:
20196
diff
changeset
|
305 |
SOME (th'', singleton |
21287 | 306 |
(Variable.trade (K (fn [th'''] => [th''' RS th'])) (Variable.thm_context th'')) th'') |
16900
e294033d1c0f
Rewrote function remove_suc, since it failed on some equations
berghofe
parents:
16861
diff
changeset
|
307 |
handle THM _ => NONE) thms of |
e294033d1c0f
Rewrote function remove_suc, since it failed on some equations
berghofe
parents:
16861
diff
changeset
|
308 |
[] => NONE |
e294033d1c0f
Rewrote function remove_suc, since it failed on some equations
berghofe
parents:
16861
diff
changeset
|
309 |
| thps => |
19791 | 310 |
let val (ths1, ths2) = split_list thps |
22360
26ead7ed4f4b
moved eq_thm etc. to structure Thm in Pure/more_thm.ML;
wenzelm
parents:
22320
diff
changeset
|
311 |
in SOME (subtract Thm.eq_thm (th :: ths1) thms @ ths2) end |
15323
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
312 |
end |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
313 |
in |
19791 | 314 |
case get_first mk_thms eqs of |
16900
e294033d1c0f
Rewrote function remove_suc, since it failed on some equations
berghofe
parents:
16861
diff
changeset
|
315 |
NONE => thms |
e294033d1c0f
Rewrote function remove_suc, since it failed on some equations
berghofe
parents:
16861
diff
changeset
|
316 |
| SOME x => remove_suc thy x |
15323
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
317 |
end; |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
318 |
|
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
319 |
fun eqn_suc_preproc thy ths = |
19791 | 320 |
let |
321 |
val dest = fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of |
|
15323
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
322 |
in |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
323 |
if forall (can dest) ths andalso |
19791 | 324 |
exists (contains_suc o dest) ths |
15396
0a36ccb79481
Preprocessors now transfer theorems to current theory in order to
berghofe
parents:
15323
diff
changeset
|
325 |
then remove_suc thy ths else ths |
15323
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
326 |
end; |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
327 |
|
15396
0a36ccb79481
Preprocessors now transfer theorems to current theory in order to
berghofe
parents:
15323
diff
changeset
|
328 |
fun remove_suc_clause thy thms = |
15323
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
329 |
let |
15396
0a36ccb79481
Preprocessors now transfer theorems to current theory in order to
berghofe
parents:
15323
diff
changeset
|
330 |
val Suc_clause' = Thm.transfer thy Suc_clause; |
20071
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19889
diff
changeset
|
331 |
val vname = Name.variant (map fst |
20196
9a19e4de6e2e
renamed add_term_varnames to Term.add_varnames (cf. Term.add_vars etc.);
wenzelm
parents:
20105
diff
changeset
|
332 |
(fold (Term.add_varnames o Thm.full_prop_of) thms [])) "x"; |
15531 | 333 |
fun find_var (t as Const ("Suc", _) $ (v as Var _)) = SOME (t, v) |
334 |
| find_var (t $ u) = (case find_var t of NONE => find_var u | x => x) |
|
335 |
| find_var _ = NONE; |
|
15323
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
336 |
fun find_thm th = |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
337 |
let val th' = ObjectLogic.atomize_thm th |
15570 | 338 |
in Option.map (pair (th, th')) (find_var (prop_of th')) end |
15323
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
339 |
in |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
340 |
case get_first find_thm thms of |
15531 | 341 |
NONE => thms |
342 |
| SOME ((th, th'), (Sucv, v)) => |
|
15323
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
343 |
let |
16861 | 344 |
val cert = cterm_of (Thm.theory_of_thm th); |
15323
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
345 |
val th'' = ObjectLogic.rulify (Thm.implies_elim |
15396
0a36ccb79481
Preprocessors now transfer theorems to current theory in order to
berghofe
parents:
15323
diff
changeset
|
346 |
(Drule.fconv_rule (Thm.beta_conversion true) |
15323
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
347 |
(Drule.instantiate' [] |
15531 | 348 |
[SOME (cert (lambda v (Abs ("x", HOLogic.natT, |
15323
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
349 |
abstract_over (Sucv, |
19828 | 350 |
HOLogic.dest_Trueprop (prop_of th')))))), |
15531 | 351 |
SOME (cert v)] Suc_clause')) |
15323
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
352 |
(Thm.forall_intr (cert v) th')) |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
353 |
in |
15396
0a36ccb79481
Preprocessors now transfer theorems to current theory in order to
berghofe
parents:
15323
diff
changeset
|
354 |
remove_suc_clause thy (map (fn th''' => |
19617 | 355 |
if (op = o pairself prop_of) (th''', th) then th'' else th''') thms) |
15323
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
356 |
end |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
357 |
end; |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
358 |
|
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
359 |
fun clause_suc_preproc thy ths = |
19791 | 360 |
let |
19828 | 361 |
val dest = fst o HOLogic.dest_mem o HOLogic.dest_Trueprop |
15323
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
362 |
in |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
363 |
if forall (can (dest o concl_of)) ths andalso |
19791 | 364 |
exists (fn th => member (op =) (foldr add_term_consts |
21287 | 365 |
[] (map_filter (try dest) (concl_of th :: prems_of th))) "Suc") ths |
15396
0a36ccb79481
Preprocessors now transfer theorems to current theory in order to
berghofe
parents:
15323
diff
changeset
|
366 |
then remove_suc_clause thy ths else ths |
15323
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
367 |
end; |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
368 |
|
19791 | 369 |
end; (*local*) |
370 |
||
21546 | 371 |
local |
372 |
val meta_eq_to_obj_eq = thm "meta_eq_to_obj_eq"; |
|
373 |
val eq_reflection = thm "eq_reflection"; |
|
374 |
in fun lift_obj_eq f thy = |
|
19791 | 375 |
map (fn thm => thm RS meta_eq_to_obj_eq) |
376 |
#> f thy |
|
21546 | 377 |
#> map (fn thm => thm RS eq_reflection) |
378 |
end |
|
19791 | 379 |
*} |
380 |
||
381 |
setup {* |
|
19603 | 382 |
Codegen.add_preprocessor eqn_suc_preproc |
383 |
#> Codegen.add_preprocessor clause_suc_preproc |
|
22046 | 384 |
#> CodegenData.add_preproc ("eqn_Suc", lift_obj_eq eqn_suc_preproc) |
385 |
#> CodegenData.add_preproc ("clause_Suc", lift_obj_eq clause_suc_preproc) |
|
15323
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
386 |
*} |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
387 |
(*>*) |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
388 |
|
21191 | 389 |
subsection {* Module names *} |
390 |
||
391 |
code_modulename SML |
|
392 |
Nat Integer |
|
393 |
EfficientNat Integer |
|
394 |
||
21911
e29bcab0c81c
added OCaml code generation (without dictionaries)
haftmann
parents:
21874
diff
changeset
|
395 |
code_modulename OCaml |
e29bcab0c81c
added OCaml code generation (without dictionaries)
haftmann
parents:
21874
diff
changeset
|
396 |
Nat Integer |
e29bcab0c81c
added OCaml code generation (without dictionaries)
haftmann
parents:
21874
diff
changeset
|
397 |
EfficientNat Integer |
e29bcab0c81c
added OCaml code generation (without dictionaries)
haftmann
parents:
21874
diff
changeset
|
398 |
|
22395 | 399 |
hide const nat_of_int |
400 |
||
15323
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
401 |
end |