|
1 (* Title: HOL/Library/Code_Numeral_Types.thy |
|
2 Author: Florian Haftmann, TU Muenchen |
|
3 *) |
|
4 |
|
5 header {* Numeric types for code generation onto target language numerals only *} |
|
6 |
|
7 theory Code_Numeral_Types |
|
8 imports Main Nat_Transfer Divides Lifting |
|
9 begin |
|
10 |
|
11 subsection {* Type of target language integers *} |
|
12 |
|
13 typedef integer = "UNIV \<Colon> int set" |
|
14 morphisms int_of_integer integer_of_int .. |
|
15 |
|
16 lemma integer_eq_iff: |
|
17 "k = l \<longleftrightarrow> int_of_integer k = int_of_integer l" |
|
18 using int_of_integer_inject [of k l] .. |
|
19 |
|
20 lemma integer_eqI: |
|
21 "int_of_integer k = int_of_integer l \<Longrightarrow> k = l" |
|
22 using integer_eq_iff [of k l] by simp |
|
23 |
|
24 lemma int_of_integer_integer_of_int [simp]: |
|
25 "int_of_integer (integer_of_int k) = k" |
|
26 using integer_of_int_inverse [of k] by simp |
|
27 |
|
28 lemma integer_of_int_int_of_integer [simp]: |
|
29 "integer_of_int (int_of_integer k) = k" |
|
30 using int_of_integer_inverse [of k] by simp |
|
31 |
|
32 instantiation integer :: ring_1 |
|
33 begin |
|
34 |
|
35 definition |
|
36 "0 = integer_of_int 0" |
|
37 |
|
38 lemma int_of_integer_zero [simp]: |
|
39 "int_of_integer 0 = 0" |
|
40 by (simp add: zero_integer_def) |
|
41 |
|
42 definition |
|
43 "1 = integer_of_int 1" |
|
44 |
|
45 lemma int_of_integer_one [simp]: |
|
46 "int_of_integer 1 = 1" |
|
47 by (simp add: one_integer_def) |
|
48 |
|
49 definition |
|
50 "k + l = integer_of_int (int_of_integer k + int_of_integer l)" |
|
51 |
|
52 lemma int_of_integer_plus [simp]: |
|
53 "int_of_integer (k + l) = int_of_integer k + int_of_integer l" |
|
54 by (simp add: plus_integer_def) |
|
55 |
|
56 definition |
|
57 "- k = integer_of_int (- int_of_integer k)" |
|
58 |
|
59 lemma int_of_integer_uminus [simp]: |
|
60 "int_of_integer (- k) = - int_of_integer k" |
|
61 by (simp add: uminus_integer_def) |
|
62 |
|
63 definition |
|
64 "k - l = integer_of_int (int_of_integer k - int_of_integer l)" |
|
65 |
|
66 lemma int_of_integer_minus [simp]: |
|
67 "int_of_integer (k - l) = int_of_integer k - int_of_integer l" |
|
68 by (simp add: minus_integer_def) |
|
69 |
|
70 definition |
|
71 "k * l = integer_of_int (int_of_integer k * int_of_integer l)" |
|
72 |
|
73 lemma int_of_integer_times [simp]: |
|
74 "int_of_integer (k * l) = int_of_integer k * int_of_integer l" |
|
75 by (simp add: times_integer_def) |
|
76 |
|
77 instance proof |
|
78 qed (auto simp add: integer_eq_iff algebra_simps) |
|
79 |
|
80 end |
|
81 |
|
82 lemma int_of_integer_of_nat [simp]: |
|
83 "int_of_integer (of_nat n) = of_nat n" |
|
84 by (induct n) simp_all |
|
85 |
|
86 definition nat_of_integer :: "integer \<Rightarrow> nat" |
|
87 where |
|
88 "nat_of_integer k = Int.nat (int_of_integer k)" |
|
89 |
|
90 lemma nat_of_integer_of_nat [simp]: |
|
91 "nat_of_integer (of_nat n) = n" |
|
92 by (simp add: nat_of_integer_def) |
|
93 |
|
94 lemma int_of_integer_of_int [simp]: |
|
95 "int_of_integer (of_int k) = k" |
|
96 by (induct k) (simp_all, simp only: neg_numeral_def numeral_One int_of_integer_uminus int_of_integer_one) |
|
97 |
|
98 lemma integer_integer_of_int_eq_of_integer_integer_of_int [simp, code_abbrev]: |
|
99 "integer_of_int = of_int" |
|
100 by rule (simp add: integer_eq_iff) |
|
101 |
|
102 lemma of_int_integer_of [simp]: |
|
103 "of_int (int_of_integer k) = (k :: integer)" |
|
104 by (simp add: integer_eq_iff) |
|
105 |
|
106 lemma int_of_integer_numeral [simp]: |
|
107 "int_of_integer (numeral k) = numeral k" |
|
108 using int_of_integer_of_int [of "numeral k"] by simp |
|
109 |
|
110 lemma int_of_integer_neg_numeral [simp]: |
|
111 "int_of_integer (neg_numeral k) = neg_numeral k" |
|
112 by (simp only: neg_numeral_def int_of_integer_uminus) simp |
|
113 |
|
114 lemma int_of_integer_sub [simp]: |
|
115 "int_of_integer (Num.sub k l) = Num.sub k l" |
|
116 by (simp only: Num.sub_def int_of_integer_minus int_of_integer_numeral) |
|
117 |
|
118 instantiation integer :: "{ring_div, equal, linordered_idom}" |
|
119 begin |
|
120 |
|
121 definition |
|
122 "k div l = of_int (int_of_integer k div int_of_integer l)" |
|
123 |
|
124 lemma int_of_integer_div [simp]: |
|
125 "int_of_integer (k div l) = int_of_integer k div int_of_integer l" |
|
126 by (simp add: div_integer_def) |
|
127 |
|
128 definition |
|
129 "k mod l = of_int (int_of_integer k mod int_of_integer l)" |
|
130 |
|
131 lemma int_of_integer_mod [simp]: |
|
132 "int_of_integer (k mod l) = int_of_integer k mod int_of_integer l" |
|
133 by (simp add: mod_integer_def) |
|
134 |
|
135 definition |
|
136 "\<bar>k\<bar> = of_int \<bar>int_of_integer k\<bar>" |
|
137 |
|
138 lemma int_of_integer_abs [simp]: |
|
139 "int_of_integer \<bar>k\<bar> = \<bar>int_of_integer k\<bar>" |
|
140 by (simp add: abs_integer_def) |
|
141 |
|
142 definition |
|
143 "sgn k = of_int (sgn (int_of_integer k))" |
|
144 |
|
145 lemma int_of_integer_sgn [simp]: |
|
146 "int_of_integer (sgn k) = sgn (int_of_integer k)" |
|
147 by (simp add: sgn_integer_def) |
|
148 |
|
149 definition |
|
150 "k \<le> l \<longleftrightarrow> int_of_integer k \<le> int_of_integer l" |
|
151 |
|
152 definition |
|
153 "k < l \<longleftrightarrow> int_of_integer k < int_of_integer l" |
|
154 |
|
155 definition |
|
156 "HOL.equal k l \<longleftrightarrow> HOL.equal (int_of_integer k) (int_of_integer l)" |
|
157 |
|
158 instance proof |
|
159 qed (auto simp add: integer_eq_iff algebra_simps |
|
160 less_eq_integer_def less_integer_def equal_integer_def equal |
|
161 intro: mult_strict_right_mono) |
|
162 |
|
163 end |
|
164 |
|
165 lemma int_of_integer_min [simp]: |
|
166 "int_of_integer (min k l) = min (int_of_integer k) (int_of_integer l)" |
|
167 by (simp add: min_def less_eq_integer_def) |
|
168 |
|
169 lemma int_of_integer_max [simp]: |
|
170 "int_of_integer (max k l) = max (int_of_integer k) (int_of_integer l)" |
|
171 by (simp add: max_def less_eq_integer_def) |
|
172 |
|
173 lemma nat_of_integer_non_positive [simp]: |
|
174 "k \<le> 0 \<Longrightarrow> nat_of_integer k = 0" |
|
175 by (simp add: nat_of_integer_def less_eq_integer_def) |
|
176 |
|
177 lemma of_nat_of_integer [simp]: |
|
178 "of_nat (nat_of_integer k) = max 0 k" |
|
179 by (simp add: nat_of_integer_def integer_eq_iff less_eq_integer_def max_def) |
|
180 |
|
181 |
|
182 subsection {* Code theorems for target language integers *} |
|
183 |
|
184 text {* Constructors *} |
|
185 |
|
186 definition Pos :: "num \<Rightarrow> integer" |
|
187 where |
|
188 [simp, code_abbrev]: "Pos = numeral" |
|
189 |
|
190 definition Neg :: "num \<Rightarrow> integer" |
|
191 where |
|
192 [simp, code_abbrev]: "Neg = neg_numeral" |
|
193 |
|
194 code_datatype "0::integer" Pos Neg |
|
195 |
|
196 |
|
197 text {* Auxiliary operations *} |
|
198 |
|
199 definition dup :: "integer \<Rightarrow> integer" |
|
200 where |
|
201 [simp]: "dup k = k + k" |
|
202 |
|
203 lemma dup_code [code]: |
|
204 "dup 0 = 0" |
|
205 "dup (Pos n) = Pos (Num.Bit0 n)" |
|
206 "dup (Neg n) = Neg (Num.Bit0 n)" |
|
207 unfolding Pos_def Neg_def neg_numeral_def |
|
208 by (simp_all add: numeral_Bit0) |
|
209 |
|
210 definition sub :: "num \<Rightarrow> num \<Rightarrow> integer" |
|
211 where |
|
212 [simp]: "sub m n = numeral m - numeral n" |
|
213 |
|
214 lemma sub_code [code]: |
|
215 "sub Num.One Num.One = 0" |
|
216 "sub (Num.Bit0 m) Num.One = Pos (Num.BitM m)" |
|
217 "sub (Num.Bit1 m) Num.One = Pos (Num.Bit0 m)" |
|
218 "sub Num.One (Num.Bit0 n) = Neg (Num.BitM n)" |
|
219 "sub Num.One (Num.Bit1 n) = Neg (Num.Bit0 n)" |
|
220 "sub (Num.Bit0 m) (Num.Bit0 n) = dup (sub m n)" |
|
221 "sub (Num.Bit1 m) (Num.Bit1 n) = dup (sub m n)" |
|
222 "sub (Num.Bit1 m) (Num.Bit0 n) = dup (sub m n) + 1" |
|
223 "sub (Num.Bit0 m) (Num.Bit1 n) = dup (sub m n) - 1" |
|
224 unfolding sub_def dup_def numeral.simps Pos_def Neg_def |
|
225 neg_numeral_def numeral_BitM |
|
226 by (simp_all only: algebra_simps add.comm_neutral) |
|
227 |
|
228 |
|
229 text {* Implementations *} |
|
230 |
|
231 lemma one_integer_code [code, code_unfold]: |
|
232 "1 = Pos Num.One" |
|
233 by simp |
|
234 |
|
235 lemma plus_integer_code [code]: |
|
236 "k + 0 = (k::integer)" |
|
237 "0 + l = (l::integer)" |
|
238 "Pos m + Pos n = Pos (m + n)" |
|
239 "Pos m + Neg n = sub m n" |
|
240 "Neg m + Pos n = sub n m" |
|
241 "Neg m + Neg n = Neg (m + n)" |
|
242 by simp_all |
|
243 |
|
244 lemma uminus_integer_code [code]: |
|
245 "uminus 0 = (0::integer)" |
|
246 "uminus (Pos m) = Neg m" |
|
247 "uminus (Neg m) = Pos m" |
|
248 by simp_all |
|
249 |
|
250 lemma minus_integer_code [code]: |
|
251 "k - 0 = (k::integer)" |
|
252 "0 - l = uminus (l::integer)" |
|
253 "Pos m - Pos n = sub m n" |
|
254 "Pos m - Neg n = Pos (m + n)" |
|
255 "Neg m - Pos n = Neg (m + n)" |
|
256 "Neg m - Neg n = sub n m" |
|
257 by simp_all |
|
258 |
|
259 lemma abs_integer_code [code]: |
|
260 "\<bar>k\<bar> = (if (k::integer) < 0 then - k else k)" |
|
261 by simp |
|
262 |
|
263 lemma sgn_integer_code [code]: |
|
264 "sgn k = (if k = 0 then 0 else if (k::integer) < 0 then - 1 else 1)" |
|
265 by simp |
|
266 |
|
267 lemma times_integer_code [code]: |
|
268 "k * 0 = (0::integer)" |
|
269 "0 * l = (0::integer)" |
|
270 "Pos m * Pos n = Pos (m * n)" |
|
271 "Pos m * Neg n = Neg (m * n)" |
|
272 "Neg m * Pos n = Neg (m * n)" |
|
273 "Neg m * Neg n = Pos (m * n)" |
|
274 by simp_all |
|
275 |
|
276 definition divmod_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer \<times> integer" |
|
277 where |
|
278 "divmod_integer k l = (k div l, k mod l)" |
|
279 |
|
280 lemma fst_divmod [simp]: |
|
281 "fst (divmod_integer k l) = k div l" |
|
282 by (simp add: divmod_integer_def) |
|
283 |
|
284 lemma snd_divmod [simp]: |
|
285 "snd (divmod_integer k l) = k mod l" |
|
286 by (simp add: divmod_integer_def) |
|
287 |
|
288 definition divmod_abs :: "integer \<Rightarrow> integer \<Rightarrow> integer \<times> integer" |
|
289 where |
|
290 "divmod_abs k l = (\<bar>k\<bar> div \<bar>l\<bar>, \<bar>k\<bar> mod \<bar>l\<bar>)" |
|
291 |
|
292 lemma fst_divmod_abs [simp]: |
|
293 "fst (divmod_abs k l) = \<bar>k\<bar> div \<bar>l\<bar>" |
|
294 by (simp add: divmod_abs_def) |
|
295 |
|
296 lemma snd_divmod_abs [simp]: |
|
297 "snd (divmod_abs k l) = \<bar>k\<bar> mod \<bar>l\<bar>" |
|
298 by (simp add: divmod_abs_def) |
|
299 |
|
300 lemma divmod_abs_terminate_code [code]: |
|
301 "divmod_abs (Neg k) (Neg l) = divmod_abs (Pos k) (Pos l)" |
|
302 "divmod_abs (Neg k) (Pos l) = divmod_abs (Pos k) (Pos l)" |
|
303 "divmod_abs (Pos k) (Neg l) = divmod_abs (Pos k) (Pos l)" |
|
304 "divmod_abs j 0 = (0, \<bar>j\<bar>)" |
|
305 "divmod_abs 0 j = (0, 0)" |
|
306 by (simp_all add: prod_eq_iff) |
|
307 |
|
308 lemma divmod_abs_rec_code [code]: |
|
309 "divmod_abs (Pos k) (Pos l) = |
|
310 (let j = sub k l in |
|
311 if j < 0 then (0, Pos k) |
|
312 else let (q, r) = divmod_abs j (Pos l) in (q + 1, r))" |
|
313 by (auto simp add: prod_eq_iff integer_eq_iff Let_def prod_case_beta |
|
314 sub_non_negative sub_negative div_pos_pos_trivial mod_pos_pos_trivial div_pos_geq mod_pos_geq) |
|
315 |
|
316 lemma divmod_integer_code [code]: "divmod_integer k l = |
|
317 (if k = 0 then (0, 0) else if l = 0 then (0, k) else |
|
318 (apsnd \<circ> times \<circ> sgn) l (if sgn k = sgn l |
|
319 then divmod_abs k l |
|
320 else (let (r, s) = divmod_abs k l in |
|
321 if s = 0 then (- r, 0) else (- r - 1, \<bar>l\<bar> - s))))" |
|
322 proof - |
|
323 have aux1: "\<And>k l::int. sgn k = sgn l \<longleftrightarrow> k = 0 \<and> l = 0 \<or> 0 < l \<and> 0 < k \<or> l < 0 \<and> k < 0" |
|
324 by (auto simp add: sgn_if) |
|
325 have aux2: "\<And>q::int. - int_of_integer k = int_of_integer l * q \<longleftrightarrow> int_of_integer k = int_of_integer l * - q" by auto |
|
326 show ?thesis |
|
327 by (simp add: prod_eq_iff integer_eq_iff prod_case_beta aux1) |
|
328 (auto simp add: zdiv_zminus1_eq_if zmod_zminus1_eq_if div_minus_right mod_minus_right aux2) |
|
329 qed |
|
330 |
|
331 lemma div_integer_code [code]: |
|
332 "k div l = fst (divmod_integer k l)" |
|
333 by simp |
|
334 |
|
335 lemma mod_integer_code [code]: |
|
336 "k mod l = snd (divmod_integer k l)" |
|
337 by simp |
|
338 |
|
339 lemma equal_integer_code [code]: |
|
340 "HOL.equal 0 (0::integer) \<longleftrightarrow> True" |
|
341 "HOL.equal 0 (Pos l) \<longleftrightarrow> False" |
|
342 "HOL.equal 0 (Neg l) \<longleftrightarrow> False" |
|
343 "HOL.equal (Pos k) 0 \<longleftrightarrow> False" |
|
344 "HOL.equal (Pos k) (Pos l) \<longleftrightarrow> HOL.equal k l" |
|
345 "HOL.equal (Pos k) (Neg l) \<longleftrightarrow> False" |
|
346 "HOL.equal (Neg k) 0 \<longleftrightarrow> False" |
|
347 "HOL.equal (Neg k) (Pos l) \<longleftrightarrow> False" |
|
348 "HOL.equal (Neg k) (Neg l) \<longleftrightarrow> HOL.equal k l" |
|
349 by (simp_all add: equal integer_eq_iff) |
|
350 |
|
351 lemma equal_integer_refl [code nbe]: |
|
352 "HOL.equal (k::integer) k \<longleftrightarrow> True" |
|
353 by (fact equal_refl) |
|
354 |
|
355 lemma less_eq_integer_code [code]: |
|
356 "0 \<le> (0::integer) \<longleftrightarrow> True" |
|
357 "0 \<le> Pos l \<longleftrightarrow> True" |
|
358 "0 \<le> Neg l \<longleftrightarrow> False" |
|
359 "Pos k \<le> 0 \<longleftrightarrow> False" |
|
360 "Pos k \<le> Pos l \<longleftrightarrow> k \<le> l" |
|
361 "Pos k \<le> Neg l \<longleftrightarrow> False" |
|
362 "Neg k \<le> 0 \<longleftrightarrow> True" |
|
363 "Neg k \<le> Pos l \<longleftrightarrow> True" |
|
364 "Neg k \<le> Neg l \<longleftrightarrow> l \<le> k" |
|
365 by (simp_all add: less_eq_integer_def) |
|
366 |
|
367 lemma less_integer_code [code]: |
|
368 "0 < (0::integer) \<longleftrightarrow> False" |
|
369 "0 < Pos l \<longleftrightarrow> True" |
|
370 "0 < Neg l \<longleftrightarrow> False" |
|
371 "Pos k < 0 \<longleftrightarrow> False" |
|
372 "Pos k < Pos l \<longleftrightarrow> k < l" |
|
373 "Pos k < Neg l \<longleftrightarrow> False" |
|
374 "Neg k < 0 \<longleftrightarrow> True" |
|
375 "Neg k < Pos l \<longleftrightarrow> True" |
|
376 "Neg k < Neg l \<longleftrightarrow> l < k" |
|
377 by (simp_all add: less_integer_def) |
|
378 |
|
379 definition integer_of_num :: "num \<Rightarrow> integer" |
|
380 where |
|
381 "integer_of_num = numeral" |
|
382 |
|
383 lemma integer_of_num [code]: |
|
384 "integer_of_num num.One = 1" |
|
385 "integer_of_num (num.Bit0 n) = (let k = integer_of_num n in k + k)" |
|
386 "integer_of_num (num.Bit1 n) = (let k = integer_of_num n in k + k + 1)" |
|
387 by (simp_all only: Let_def) (simp_all only: integer_of_num_def numeral.simps) |
|
388 |
|
389 definition num_of_integer :: "integer \<Rightarrow> num" |
|
390 where |
|
391 "num_of_integer = num_of_nat \<circ> nat_of_integer" |
|
392 |
|
393 lemma num_of_integer_code [code]: |
|
394 "num_of_integer k = (if k \<le> 1 then Num.One |
|
395 else let |
|
396 (l, j) = divmod_integer k 2; |
|
397 l' = num_of_integer l; |
|
398 l'' = l' + l' |
|
399 in if j = 0 then l'' else l'' + Num.One)" |
|
400 proof - |
|
401 { |
|
402 assume "int_of_integer k mod 2 = 1" |
|
403 then have "nat (int_of_integer k mod 2) = nat 1" by simp |
|
404 moreover assume *: "1 < int_of_integer k" |
|
405 ultimately have **: "nat (int_of_integer k) mod 2 = 1" by (simp add: nat_mod_distrib) |
|
406 have "num_of_nat (nat (int_of_integer k)) = |
|
407 num_of_nat (2 * (nat (int_of_integer k) div 2) + nat (int_of_integer k) mod 2)" |
|
408 by simp |
|
409 then have "num_of_nat (nat (int_of_integer k)) = |
|
410 num_of_nat (nat (int_of_integer k) div 2 + nat (int_of_integer k) div 2 + nat (int_of_integer k) mod 2)" |
|
411 by (simp add: mult_2) |
|
412 with ** have "num_of_nat (nat (int_of_integer k)) = |
|
413 num_of_nat (nat (int_of_integer k) div 2 + nat (int_of_integer k) div 2 + 1)" |
|
414 by simp |
|
415 } |
|
416 note aux = this |
|
417 show ?thesis |
|
418 by (auto simp add: num_of_integer_def nat_of_integer_def Let_def prod_case_beta |
|
419 not_le integer_eq_iff less_eq_integer_def |
|
420 nat_mult_distrib nat_div_distrib num_of_nat_One num_of_nat_plus_distrib |
|
421 mult_2 [where 'a=nat] aux add_One) |
|
422 qed |
|
423 |
|
424 lemma nat_of_integer_code [code]: |
|
425 "nat_of_integer k = (if k \<le> 0 then 0 |
|
426 else let |
|
427 (l, j) = divmod_integer k 2; |
|
428 l' = nat_of_integer l; |
|
429 l'' = l' + l' |
|
430 in if j = 0 then l'' else l'' + 1)" |
|
431 proof - |
|
432 obtain j where "k = integer_of_int j" |
|
433 proof |
|
434 show "k = integer_of_int (int_of_integer k)" by simp |
|
435 qed |
|
436 moreover have "2 * (j div 2) = j - j mod 2" |
|
437 by (simp add: zmult_div_cancel mult_commute) |
|
438 ultimately show ?thesis |
|
439 by (auto simp add: split_def Let_def mod_integer_def nat_of_integer_def not_le |
|
440 nat_add_distrib [symmetric] Suc_nat_eq_nat_zadd1) |
|
441 qed |
|
442 |
|
443 lemma int_of_integer_code [code]: |
|
444 "int_of_integer k = (if k < 0 then - (int_of_integer (- k)) |
|
445 else if k = 0 then 0 |
|
446 else let |
|
447 (l, j) = divmod_integer k 2; |
|
448 l' = 2 * int_of_integer l |
|
449 in if j = 0 then l' else l' + 1)" |
|
450 by (auto simp add: split_def Let_def integer_eq_iff zmult_div_cancel) |
|
451 |
|
452 lemma integer_of_int_code [code]: |
|
453 "integer_of_int k = (if k < 0 then - (integer_of_int (- k)) |
|
454 else if k = 0 then 0 |
|
455 else let |
|
456 (l, j) = divmod_int k 2; |
|
457 l' = 2 * integer_of_int l |
|
458 in if j = 0 then l' else l' + 1)" |
|
459 by (auto simp add: split_def Let_def integer_eq_iff zmult_div_cancel) |
|
460 |
|
461 hide_const (open) Pos Neg sub dup divmod_abs |
|
462 |
|
463 |
|
464 subsection {* Serializer setup for target language integers *} |
|
465 |
|
466 code_reserved Eval abs |
|
467 |
|
468 code_type integer |
|
469 (SML "IntInf.int") |
|
470 (OCaml "Big'_int.big'_int") |
|
471 (Haskell "Integer") |
|
472 (Scala "BigInt") |
|
473 (Eval "int") |
|
474 |
|
475 code_instance integer :: equal |
|
476 (Haskell -) |
|
477 |
|
478 code_const "0::integer" |
|
479 (SML "0") |
|
480 (OCaml "Big'_int.zero'_big'_int") |
|
481 (Haskell "0") |
|
482 (Scala "BigInt(0)") |
|
483 |
|
484 setup {* |
|
485 fold (Numeral.add_code @{const_name Code_Numeral_Types.Pos} |
|
486 false Code_Printer.literal_numeral) ["SML", "OCaml", "Haskell", "Scala"] |
|
487 *} |
|
488 |
|
489 setup {* |
|
490 fold (Numeral.add_code @{const_name Code_Numeral_Types.Neg} |
|
491 true Code_Printer.literal_numeral) ["SML", "OCaml", "Haskell", "Scala"] |
|
492 *} |
|
493 |
|
494 code_const "plus :: integer \<Rightarrow> _ \<Rightarrow> _" |
|
495 (SML "IntInf.+ ((_), (_))") |
|
496 (OCaml "Big'_int.add'_big'_int") |
|
497 (Haskell infixl 6 "+") |
|
498 (Scala infixl 7 "+") |
|
499 (Eval infixl 8 "+") |
|
500 |
|
501 code_const "uminus :: integer \<Rightarrow> _" |
|
502 (SML "IntInf.~") |
|
503 (OCaml "Big'_int.minus'_big'_int") |
|
504 (Haskell "negate") |
|
505 (Scala "!(- _)") |
|
506 (Eval "~/ _") |
|
507 |
|
508 code_const "minus :: integer \<Rightarrow> _" |
|
509 (SML "IntInf.- ((_), (_))") |
|
510 (OCaml "Big'_int.sub'_big'_int") |
|
511 (Haskell infixl 6 "-") |
|
512 (Scala infixl 7 "-") |
|
513 (Eval infixl 8 "-") |
|
514 |
|
515 code_const Code_Numeral_Types.dup |
|
516 (SML "IntInf.*/ (2,/ (_))") |
|
517 (OCaml "Big'_int.mult'_big'_int/ (Big'_int.big'_int'_of'_int/ 2)") |
|
518 (Haskell "!(2 * _)") |
|
519 (Scala "!(2 * _)") |
|
520 (Eval "!(2 * _)") |
|
521 |
|
522 code_const Code_Numeral_Types.sub |
|
523 (SML "!(raise/ Fail/ \"sub\")") |
|
524 (OCaml "failwith/ \"sub\"") |
|
525 (Haskell "error/ \"sub\"") |
|
526 (Scala "!sys.error(\"sub\")") |
|
527 |
|
528 code_const "times :: integer \<Rightarrow> _ \<Rightarrow> _" |
|
529 (SML "IntInf.* ((_), (_))") |
|
530 (OCaml "Big'_int.mult'_big'_int") |
|
531 (Haskell infixl 7 "*") |
|
532 (Scala infixl 8 "*") |
|
533 (Eval infixl 9 "*") |
|
534 |
|
535 code_const Code_Numeral_Types.divmod_abs |
|
536 (SML "IntInf.divMod/ (IntInf.abs _,/ IntInf.abs _)") |
|
537 (OCaml "Big'_int.quomod'_big'_int/ (Big'_int.abs'_big'_int _)/ (Big'_int.abs'_big'_int _)") |
|
538 (Haskell "divMod/ (abs _)/ (abs _)") |
|
539 (Scala "!((k: BigInt) => (l: BigInt) =>/ if (l == 0)/ (BigInt(0), k) else/ (k.abs '/% l.abs))") |
|
540 (Eval "Integer.div'_mod/ (abs _)/ (abs _)") |
|
541 |
|
542 code_const "HOL.equal :: integer \<Rightarrow> _ \<Rightarrow> bool" |
|
543 (SML "!((_ : IntInf.int) = _)") |
|
544 (OCaml "Big'_int.eq'_big'_int") |
|
545 (Haskell infix 4 "==") |
|
546 (Scala infixl 5 "==") |
|
547 (Eval infixl 6 "=") |
|
548 |
|
549 code_const "less_eq :: integer \<Rightarrow> _ \<Rightarrow> bool" |
|
550 (SML "IntInf.<= ((_), (_))") |
|
551 (OCaml "Big'_int.le'_big'_int") |
|
552 (Haskell infix 4 "<=") |
|
553 (Scala infixl 4 "<=") |
|
554 (Eval infixl 6 "<=") |
|
555 |
|
556 code_const "less :: integer \<Rightarrow> _ \<Rightarrow> bool" |
|
557 (SML "IntInf.< ((_), (_))") |
|
558 (OCaml "Big'_int.lt'_big'_int") |
|
559 (Haskell infix 4 "<") |
|
560 (Scala infixl 4 "<") |
|
561 (Eval infixl 6 "<") |
|
562 |
|
563 code_modulename SML |
|
564 Code_Numeral_Types Arith |
|
565 |
|
566 code_modulename OCaml |
|
567 Code_Numeral_Types Arith |
|
568 |
|
569 code_modulename Haskell |
|
570 Code_Numeral_Types Arith |
|
571 |
|
572 |
|
573 subsection {* Type of target language naturals *} |
|
574 |
|
575 typedef natural = "UNIV \<Colon> nat set" |
|
576 morphisms nat_of_natural natural_of_nat .. |
|
577 |
|
578 lemma natural_eq_iff [termination_simp]: |
|
579 "m = n \<longleftrightarrow> nat_of_natural m = nat_of_natural n" |
|
580 using nat_of_natural_inject [of m n] .. |
|
581 |
|
582 lemma natural_eqI: |
|
583 "nat_of_natural m = nat_of_natural n \<Longrightarrow> m = n" |
|
584 using natural_eq_iff [of m n] by simp |
|
585 |
|
586 lemma nat_of_natural_of_nat_inverse [simp]: |
|
587 "nat_of_natural (natural_of_nat n) = n" |
|
588 using natural_of_nat_inverse [of n] by simp |
|
589 |
|
590 lemma natural_of_nat_of_natural_inverse [simp]: |
|
591 "natural_of_nat (nat_of_natural n) = n" |
|
592 using nat_of_natural_inverse [of n] by simp |
|
593 |
|
594 instantiation natural :: "{comm_monoid_diff, semiring_1}" |
|
595 begin |
|
596 |
|
597 definition |
|
598 "0 = natural_of_nat 0" |
|
599 |
|
600 lemma nat_of_natural_zero [simp]: |
|
601 "nat_of_natural 0 = 0" |
|
602 by (simp add: zero_natural_def) |
|
603 |
|
604 definition |
|
605 "1 = natural_of_nat 1" |
|
606 |
|
607 lemma nat_of_natural_one [simp]: |
|
608 "nat_of_natural 1 = 1" |
|
609 by (simp add: one_natural_def) |
|
610 |
|
611 definition |
|
612 "m + n = natural_of_nat (nat_of_natural m + nat_of_natural n)" |
|
613 |
|
614 lemma nat_of_natural_plus [simp]: |
|
615 "nat_of_natural (m + n) = nat_of_natural m + nat_of_natural n" |
|
616 by (simp add: plus_natural_def) |
|
617 |
|
618 definition |
|
619 "m - n = natural_of_nat (nat_of_natural m - nat_of_natural n)" |
|
620 |
|
621 lemma nat_of_natural_minus [simp]: |
|
622 "nat_of_natural (m - n) = nat_of_natural m - nat_of_natural n" |
|
623 by (simp add: minus_natural_def) |
|
624 |
|
625 definition |
|
626 "m * n = natural_of_nat (nat_of_natural m * nat_of_natural n)" |
|
627 |
|
628 lemma nat_of_natural_times [simp]: |
|
629 "nat_of_natural (m * n) = nat_of_natural m * nat_of_natural n" |
|
630 by (simp add: times_natural_def) |
|
631 |
|
632 instance proof |
|
633 qed (auto simp add: natural_eq_iff algebra_simps) |
|
634 |
|
635 end |
|
636 |
|
637 lemma nat_of_natural_of_nat [simp]: |
|
638 "nat_of_natural (of_nat n) = n" |
|
639 by (induct n) simp_all |
|
640 |
|
641 lemma natural_of_nat_of_nat [simp, code_abbrev]: |
|
642 "natural_of_nat = of_nat" |
|
643 by rule (simp add: natural_eq_iff) |
|
644 |
|
645 lemma of_nat_of_natural [simp]: |
|
646 "of_nat (nat_of_natural n) = n" |
|
647 using natural_of_nat_of_natural_inverse [of n] by simp |
|
648 |
|
649 lemma nat_of_natural_numeral [simp]: |
|
650 "nat_of_natural (numeral k) = numeral k" |
|
651 using nat_of_natural_of_nat [of "numeral k"] by simp |
|
652 |
|
653 instantiation natural :: "{semiring_div, equal, linordered_semiring}" |
|
654 begin |
|
655 |
|
656 definition |
|
657 "m div n = natural_of_nat (nat_of_natural m div nat_of_natural n)" |
|
658 |
|
659 lemma nat_of_natural_div [simp]: |
|
660 "nat_of_natural (m div n) = nat_of_natural m div nat_of_natural n" |
|
661 by (simp add: div_natural_def) |
|
662 |
|
663 definition |
|
664 "m mod n = natural_of_nat (nat_of_natural m mod nat_of_natural n)" |
|
665 |
|
666 lemma nat_of_natural_mod [simp]: |
|
667 "nat_of_natural (m mod n) = nat_of_natural m mod nat_of_natural n" |
|
668 by (simp add: mod_natural_def) |
|
669 |
|
670 definition |
|
671 [termination_simp]: "m \<le> n \<longleftrightarrow> nat_of_natural m \<le> nat_of_natural n" |
|
672 |
|
673 definition |
|
674 [termination_simp]: "m < n \<longleftrightarrow> nat_of_natural m < nat_of_natural n" |
|
675 |
|
676 definition |
|
677 "HOL.equal m n \<longleftrightarrow> HOL.equal (nat_of_natural m) (nat_of_natural n)" |
|
678 |
|
679 instance proof |
|
680 qed (auto simp add: natural_eq_iff algebra_simps |
|
681 less_eq_natural_def less_natural_def equal_natural_def equal) |
|
682 |
|
683 end |
|
684 |
|
685 lemma nat_of_natural_min [simp]: |
|
686 "nat_of_natural (min k l) = min (nat_of_natural k) (nat_of_natural l)" |
|
687 by (simp add: min_def less_eq_natural_def) |
|
688 |
|
689 lemma nat_of_natural_max [simp]: |
|
690 "nat_of_natural (max k l) = max (nat_of_natural k) (nat_of_natural l)" |
|
691 by (simp add: max_def less_eq_natural_def) |
|
692 |
|
693 definition natural_of_integer :: "integer \<Rightarrow> natural" |
|
694 where |
|
695 "natural_of_integer = of_nat \<circ> nat_of_integer" |
|
696 |
|
697 definition integer_of_natural :: "natural \<Rightarrow> integer" |
|
698 where |
|
699 "integer_of_natural = of_nat \<circ> nat_of_natural" |
|
700 |
|
701 lemma natural_of_integer_of_natural [simp]: |
|
702 "natural_of_integer (integer_of_natural n) = n" |
|
703 by (simp add: natural_of_integer_def integer_of_natural_def natural_eq_iff) |
|
704 |
|
705 lemma integer_of_natural_of_integer [simp]: |
|
706 "integer_of_natural (natural_of_integer k) = max 0 k" |
|
707 by (simp add: natural_of_integer_def integer_of_natural_def integer_eq_iff) |
|
708 |
|
709 lemma int_of_integer_of_natural [simp]: |
|
710 "int_of_integer (integer_of_natural n) = of_nat (nat_of_natural n)" |
|
711 by (simp add: integer_of_natural_def) |
|
712 |
|
713 lemma integer_of_natural_of_nat [simp]: |
|
714 "integer_of_natural (of_nat n) = of_nat n" |
|
715 by (simp add: integer_eq_iff) |
|
716 |
|
717 lemma [measure_function]: |
|
718 "is_measure nat_of_natural" by (rule is_measure_trivial) |
|
719 |
|
720 |
|
721 subsection {* Inductive represenation of target language naturals *} |
|
722 |
|
723 definition Suc :: "natural \<Rightarrow> natural" |
|
724 where |
|
725 "Suc = natural_of_nat \<circ> Nat.Suc \<circ> nat_of_natural" |
|
726 |
|
727 lemma nat_of_natural_Suc [simp]: |
|
728 "nat_of_natural (Suc n) = Nat.Suc (nat_of_natural n)" |
|
729 by (simp add: Suc_def) |
|
730 |
|
731 rep_datatype "0::natural" Suc |
|
732 proof - |
|
733 fix P :: "natural \<Rightarrow> bool" |
|
734 fix n :: natural |
|
735 assume "P 0" then have init: "P (natural_of_nat 0)" by simp |
|
736 assume "\<And>n. P n \<Longrightarrow> P (Suc n)" |
|
737 then have "\<And>n. P (natural_of_nat n) \<Longrightarrow> P (Suc (natural_of_nat n))" . |
|
738 then have step: "\<And>n. P (natural_of_nat n) \<Longrightarrow> P (natural_of_nat (Nat.Suc n))" |
|
739 by (simp add: Suc_def) |
|
740 from init step have "P (natural_of_nat (nat_of_natural n))" |
|
741 by (rule nat.induct) |
|
742 with natural_of_nat_of_natural_inverse show "P n" by simp |
|
743 qed (simp_all add: natural_eq_iff) |
|
744 |
|
745 lemma natural_case [case_names nat, cases type: natural]: |
|
746 fixes m :: natural |
|
747 assumes "\<And>n. m = of_nat n \<Longrightarrow> P" |
|
748 shows P |
|
749 by (rule assms [of "nat_of_natural m"]) simp |
|
750 |
|
751 lemma [simp, code]: |
|
752 "natural_size = nat_of_natural" |
|
753 proof (rule ext) |
|
754 fix n |
|
755 show "natural_size n = nat_of_natural n" |
|
756 by (induct n) simp_all |
|
757 qed |
|
758 |
|
759 lemma [simp, code]: |
|
760 "size = nat_of_natural" |
|
761 proof (rule ext) |
|
762 fix n |
|
763 show "size n = nat_of_natural n" |
|
764 by (induct n) simp_all |
|
765 qed |
|
766 |
|
767 lemma natural_decr [termination_simp]: |
|
768 "n \<noteq> 0 \<Longrightarrow> nat_of_natural n - Nat.Suc 0 < nat_of_natural n" |
|
769 by (simp add: natural_eq_iff) |
|
770 |
|
771 lemma natural_zero_minus_one: |
|
772 "(0::natural) - 1 = 0" |
|
773 by simp |
|
774 |
|
775 lemma Suc_natural_minus_one: |
|
776 "Suc n - 1 = n" |
|
777 by (simp add: natural_eq_iff) |
|
778 |
|
779 hide_const (open) Suc |
|
780 |
|
781 |
|
782 subsection {* Code refinement for target language naturals *} |
|
783 |
|
784 definition Nat :: "integer \<Rightarrow> natural" |
|
785 where |
|
786 "Nat = natural_of_integer" |
|
787 |
|
788 lemma [code abstype]: |
|
789 "Nat (integer_of_natural n) = n" |
|
790 by (unfold Nat_def) (fact natural_of_integer_of_natural) |
|
791 |
|
792 lemma [code abstract]: |
|
793 "integer_of_natural (natural_of_nat n) = of_nat n" |
|
794 by simp |
|
795 |
|
796 lemma [code abstract]: |
|
797 "integer_of_natural (natural_of_integer k) = max 0 k" |
|
798 by simp |
|
799 |
|
800 lemma [code_abbrev]: |
|
801 "natural_of_integer (Code_Numeral_Types.Pos k) = numeral k" |
|
802 by (simp add: nat_of_integer_def natural_of_integer_def) |
|
803 |
|
804 lemma [code abstract]: |
|
805 "integer_of_natural 0 = 0" |
|
806 by (simp add: integer_eq_iff) |
|
807 |
|
808 lemma [code abstract]: |
|
809 "integer_of_natural 1 = 1" |
|
810 by (simp add: integer_eq_iff) |
|
811 |
|
812 lemma [code abstract]: |
|
813 "integer_of_natural (Code_Numeral_Types.Suc n) = integer_of_natural n + 1" |
|
814 by (simp add: integer_eq_iff) |
|
815 |
|
816 lemma [code]: |
|
817 "nat_of_natural = nat_of_integer \<circ> integer_of_natural" |
|
818 by (simp add: integer_of_natural_def fun_eq_iff) |
|
819 |
|
820 lemma [code, code_unfold]: |
|
821 "natural_case f g n = (if n = 0 then f else g (n - 1))" |
|
822 by (cases n rule: natural.exhaust) (simp_all, simp add: Suc_def) |
|
823 |
|
824 declare natural.recs [code del] |
|
825 |
|
826 lemma [code abstract]: |
|
827 "integer_of_natural (m + n) = integer_of_natural m + integer_of_natural n" |
|
828 by (simp add: integer_eq_iff) |
|
829 |
|
830 lemma [code abstract]: |
|
831 "integer_of_natural (m - n) = max 0 (integer_of_natural m - integer_of_natural n)" |
|
832 by (simp add: integer_eq_iff) |
|
833 |
|
834 lemma [code abstract]: |
|
835 "integer_of_natural (m * n) = integer_of_natural m * integer_of_natural n" |
|
836 by (simp add: integer_eq_iff of_nat_mult) |
|
837 |
|
838 lemma [code abstract]: |
|
839 "integer_of_natural (m div n) = integer_of_natural m div integer_of_natural n" |
|
840 by (simp add: integer_eq_iff zdiv_int) |
|
841 |
|
842 lemma [code abstract]: |
|
843 "integer_of_natural (m mod n) = integer_of_natural m mod integer_of_natural n" |
|
844 by (simp add: integer_eq_iff zmod_int) |
|
845 |
|
846 lemma [code]: |
|
847 "HOL.equal m n \<longleftrightarrow> HOL.equal (integer_of_natural m) (integer_of_natural n)" |
|
848 by (simp add: equal natural_eq_iff integer_eq_iff) |
|
849 |
|
850 lemma [code nbe]: |
|
851 "HOL.equal n (n::natural) \<longleftrightarrow> True" |
|
852 by (simp add: equal) |
|
853 |
|
854 lemma [code]: |
|
855 "m \<le> n \<longleftrightarrow> (integer_of_natural m) \<le> integer_of_natural n" |
|
856 by (simp add: less_eq_natural_def less_eq_integer_def) |
|
857 |
|
858 lemma [code]: |
|
859 "m < n \<longleftrightarrow> (integer_of_natural m) < integer_of_natural n" |
|
860 by (simp add: less_natural_def less_integer_def) |
|
861 |
|
862 hide_const (open) Nat |
|
863 |
|
864 |
|
865 code_reflect Code_Numeral_Types |
|
866 datatypes natural = _ |
|
867 functions integer_of_natural natural_of_integer |
|
868 |
|
869 end |
|
870 |