author | wenzelm |
Sat, 07 Apr 2012 16:41:59 +0200 | |
changeset 47389 | e8552cba702d |
parent 47217 | 501b9bbd0d6e |
child 47400 | b7625245a846 |
permissions | -rw-r--r-- |
47108 | 1 |
theory Target_Numeral |
2 |
imports Main Code_Nat |
|
3 |
begin |
|
4 |
||
5 |
subsection {* Type of target language numerals *} |
|
6 |
||
7 |
typedef (open) int = "UNIV \<Colon> int set" |
|
8 |
morphisms int_of of_int .. |
|
9 |
||
10 |
hide_type (open) int |
|
11 |
hide_const (open) of_int |
|
12 |
||
13 |
lemma int_eq_iff: |
|
14 |
"k = l \<longleftrightarrow> int_of k = int_of l" |
|
15 |
using int_of_inject [of k l] .. |
|
16 |
||
17 |
lemma int_eqI: |
|
18 |
"int_of k = int_of l \<Longrightarrow> k = l" |
|
19 |
using int_eq_iff [of k l] by simp |
|
20 |
||
21 |
lemma int_of_int [simp]: |
|
22 |
"int_of (Target_Numeral.of_int k) = k" |
|
23 |
using of_int_inverse [of k] by simp |
|
24 |
||
25 |
lemma of_int_of [simp]: |
|
26 |
"Target_Numeral.of_int (int_of k) = k" |
|
27 |
using int_of_inverse [of k] by simp |
|
28 |
||
29 |
hide_fact (open) int_eq_iff int_eqI |
|
30 |
||
31 |
instantiation Target_Numeral.int :: ring_1 |
|
32 |
begin |
|
33 |
||
34 |
definition |
|
35 |
"0 = Target_Numeral.of_int 0" |
|
36 |
||
37 |
lemma int_of_zero [simp]: |
|
38 |
"int_of 0 = 0" |
|
39 |
by (simp add: zero_int_def) |
|
40 |
||
41 |
definition |
|
42 |
"1 = Target_Numeral.of_int 1" |
|
43 |
||
44 |
lemma int_of_one [simp]: |
|
45 |
"int_of 1 = 1" |
|
46 |
by (simp add: one_int_def) |
|
47 |
||
48 |
definition |
|
49 |
"k + l = Target_Numeral.of_int (int_of k + int_of l)" |
|
50 |
||
51 |
lemma int_of_plus [simp]: |
|
52 |
"int_of (k + l) = int_of k + int_of l" |
|
53 |
by (simp add: plus_int_def) |
|
54 |
||
55 |
definition |
|
56 |
"- k = Target_Numeral.of_int (- int_of k)" |
|
57 |
||
58 |
lemma int_of_uminus [simp]: |
|
59 |
"int_of (- k) = - int_of k" |
|
60 |
by (simp add: uminus_int_def) |
|
61 |
||
62 |
definition |
|
63 |
"k - l = Target_Numeral.of_int (int_of k - int_of l)" |
|
64 |
||
65 |
lemma int_of_minus [simp]: |
|
66 |
"int_of (k - l) = int_of k - int_of l" |
|
67 |
by (simp add: minus_int_def) |
|
68 |
||
69 |
definition |
|
70 |
"k * l = Target_Numeral.of_int (int_of k * int_of l)" |
|
71 |
||
72 |
lemma int_of_times [simp]: |
|
73 |
"int_of (k * l) = int_of k * int_of l" |
|
74 |
by (simp add: times_int_def) |
|
75 |
||
76 |
instance proof |
|
77 |
qed (auto simp add: Target_Numeral.int_eq_iff algebra_simps) |
|
78 |
||
79 |
end |
|
80 |
||
81 |
lemma int_of_of_nat [simp]: |
|
82 |
"int_of (of_nat n) = of_nat n" |
|
83 |
by (induct n) simp_all |
|
84 |
||
85 |
definition nat_of :: "Target_Numeral.int \<Rightarrow> nat" where |
|
86 |
"nat_of k = Int.nat (int_of k)" |
|
87 |
||
88 |
lemma nat_of_of_nat [simp]: |
|
89 |
"nat_of (of_nat n) = n" |
|
90 |
by (simp add: nat_of_def) |
|
91 |
||
92 |
lemma int_of_of_int [simp]: |
|
93 |
"int_of (of_int k) = k" |
|
94 |
by (induct k) (simp_all, simp only: neg_numeral_def numeral_One int_of_uminus int_of_one) |
|
95 |
||
96 |
lemma of_int_of_int [simp, code_abbrev]: |
|
97 |
"Target_Numeral.of_int = of_int" |
|
98 |
by rule (simp add: Target_Numeral.int_eq_iff) |
|
99 |
||
100 |
lemma int_of_numeral [simp]: |
|
101 |
"int_of (numeral k) = numeral k" |
|
102 |
using int_of_of_int [of "numeral k"] by simp |
|
103 |
||
104 |
lemma int_of_neg_numeral [simp]: |
|
105 |
"int_of (neg_numeral k) = neg_numeral k" |
|
106 |
by (simp only: neg_numeral_def int_of_uminus) simp |
|
107 |
||
108 |
lemma int_of_sub [simp]: |
|
109 |
"int_of (Num.sub k l) = Num.sub k l" |
|
110 |
by (simp only: Num.sub_def int_of_minus int_of_numeral) |
|
111 |
||
112 |
instantiation Target_Numeral.int :: "{ring_div, equal, linordered_idom}" |
|
113 |
begin |
|
114 |
||
115 |
definition |
|
116 |
"k div l = of_int (int_of k div int_of l)" |
|
117 |
||
118 |
lemma int_of_div [simp]: |
|
119 |
"int_of (k div l) = int_of k div int_of l" |
|
120 |
by (simp add: div_int_def) |
|
121 |
||
122 |
definition |
|
123 |
"k mod l = of_int (int_of k mod int_of l)" |
|
124 |
||
125 |
lemma int_of_mod [simp]: |
|
126 |
"int_of (k mod l) = int_of k mod int_of l" |
|
127 |
by (simp add: mod_int_def) |
|
128 |
||
129 |
definition |
|
130 |
"\<bar>k\<bar> = of_int \<bar>int_of k\<bar>" |
|
131 |
||
132 |
lemma int_of_abs [simp]: |
|
133 |
"int_of \<bar>k\<bar> = \<bar>int_of k\<bar>" |
|
134 |
by (simp add: abs_int_def) |
|
135 |
||
136 |
definition |
|
137 |
"sgn k = of_int (sgn (int_of k))" |
|
138 |
||
139 |
lemma int_of_sgn [simp]: |
|
140 |
"int_of (sgn k) = sgn (int_of k)" |
|
141 |
by (simp add: sgn_int_def) |
|
142 |
||
143 |
definition |
|
144 |
"k \<le> l \<longleftrightarrow> int_of k \<le> int_of l" |
|
145 |
||
146 |
definition |
|
147 |
"k < l \<longleftrightarrow> int_of k < int_of l" |
|
148 |
||
149 |
definition |
|
150 |
"HOL.equal k l \<longleftrightarrow> HOL.equal (int_of k) (int_of l)" |
|
151 |
||
152 |
instance proof |
|
153 |
qed (auto simp add: Target_Numeral.int_eq_iff algebra_simps |
|
154 |
less_eq_int_def less_int_def equal_int_def equal) |
|
155 |
||
156 |
end |
|
157 |
||
158 |
lemma int_of_min [simp]: |
|
159 |
"int_of (min k l) = min (int_of k) (int_of l)" |
|
160 |
by (simp add: min_def less_eq_int_def) |
|
161 |
||
162 |
lemma int_of_max [simp]: |
|
163 |
"int_of (max k l) = max (int_of k) (int_of l)" |
|
164 |
by (simp add: max_def less_eq_int_def) |
|
165 |
||
166 |
||
167 |
subsection {* Code theorems for target language numerals *} |
|
168 |
||
169 |
text {* Constructors *} |
|
170 |
||
171 |
definition Pos :: "num \<Rightarrow> Target_Numeral.int" where |
|
172 |
[simp, code_abbrev]: "Pos = numeral" |
|
173 |
||
174 |
definition Neg :: "num \<Rightarrow> Target_Numeral.int" where |
|
175 |
[simp, code_abbrev]: "Neg = neg_numeral" |
|
176 |
||
177 |
code_datatype "0::Target_Numeral.int" Pos Neg |
|
178 |
||
179 |
||
180 |
text {* Auxiliary operations *} |
|
181 |
||
182 |
definition dup :: "Target_Numeral.int \<Rightarrow> Target_Numeral.int" where |
|
183 |
[simp]: "dup k = k + k" |
|
184 |
||
185 |
lemma dup_code [code]: |
|
186 |
"dup 0 = 0" |
|
187 |
"dup (Pos n) = Pos (Num.Bit0 n)" |
|
188 |
"dup (Neg n) = Neg (Num.Bit0 n)" |
|
189 |
unfolding Pos_def Neg_def neg_numeral_def |
|
190 |
by (simp_all add: numeral_Bit0) |
|
191 |
||
192 |
definition sub :: "num \<Rightarrow> num \<Rightarrow> Target_Numeral.int" where |
|
193 |
[simp]: "sub m n = numeral m - numeral n" |
|
194 |
||
195 |
lemma sub_code [code]: |
|
196 |
"sub Num.One Num.One = 0" |
|
197 |
"sub (Num.Bit0 m) Num.One = Pos (Num.BitM m)" |
|
198 |
"sub (Num.Bit1 m) Num.One = Pos (Num.Bit0 m)" |
|
199 |
"sub Num.One (Num.Bit0 n) = Neg (Num.BitM n)" |
|
200 |
"sub Num.One (Num.Bit1 n) = Neg (Num.Bit0 n)" |
|
201 |
"sub (Num.Bit0 m) (Num.Bit0 n) = dup (sub m n)" |
|
202 |
"sub (Num.Bit1 m) (Num.Bit1 n) = dup (sub m n)" |
|
203 |
"sub (Num.Bit1 m) (Num.Bit0 n) = dup (sub m n) + 1" |
|
204 |
"sub (Num.Bit0 m) (Num.Bit1 n) = dup (sub m n) - 1" |
|
205 |
unfolding sub_def dup_def numeral.simps Pos_def Neg_def |
|
206 |
neg_numeral_def numeral_BitM |
|
207 |
by (simp_all only: algebra_simps add.comm_neutral) |
|
208 |
||
209 |
||
210 |
text {* Implementations *} |
|
211 |
||
212 |
lemma one_int_code [code, code_unfold]: |
|
213 |
"1 = Pos Num.One" |
|
214 |
by simp |
|
215 |
||
216 |
lemma plus_int_code [code]: |
|
217 |
"k + 0 = (k::Target_Numeral.int)" |
|
218 |
"0 + l = (l::Target_Numeral.int)" |
|
219 |
"Pos m + Pos n = Pos (m + n)" |
|
220 |
"Pos m + Neg n = sub m n" |
|
221 |
"Neg m + Pos n = sub n m" |
|
222 |
"Neg m + Neg n = Neg (m + n)" |
|
223 |
by simp_all |
|
224 |
||
225 |
lemma uminus_int_code [code]: |
|
226 |
"uminus 0 = (0::Target_Numeral.int)" |
|
227 |
"uminus (Pos m) = Neg m" |
|
228 |
"uminus (Neg m) = Pos m" |
|
229 |
by simp_all |
|
230 |
||
231 |
lemma minus_int_code [code]: |
|
232 |
"k - 0 = (k::Target_Numeral.int)" |
|
233 |
"0 - l = uminus (l::Target_Numeral.int)" |
|
234 |
"Pos m - Pos n = sub m n" |
|
235 |
"Pos m - Neg n = Pos (m + n)" |
|
236 |
"Neg m - Pos n = Neg (m + n)" |
|
237 |
"Neg m - Neg n = sub n m" |
|
238 |
by simp_all |
|
239 |
||
240 |
lemma times_int_code [code]: |
|
241 |
"k * 0 = (0::Target_Numeral.int)" |
|
242 |
"0 * l = (0::Target_Numeral.int)" |
|
243 |
"Pos m * Pos n = Pos (m * n)" |
|
244 |
"Pos m * Neg n = Neg (m * n)" |
|
245 |
"Neg m * Pos n = Neg (m * n)" |
|
246 |
"Neg m * Neg n = Pos (m * n)" |
|
247 |
by simp_all |
|
248 |
||
249 |
definition divmod :: "Target_Numeral.int \<Rightarrow> Target_Numeral.int \<Rightarrow> Target_Numeral.int \<times> Target_Numeral.int" where |
|
250 |
"divmod k l = (k div l, k mod l)" |
|
251 |
||
252 |
lemma fst_divmod [simp]: |
|
253 |
"fst (divmod k l) = k div l" |
|
254 |
by (simp add: divmod_def) |
|
255 |
||
256 |
lemma snd_divmod [simp]: |
|
257 |
"snd (divmod k l) = k mod l" |
|
258 |
by (simp add: divmod_def) |
|
259 |
||
260 |
definition divmod_abs :: "Target_Numeral.int \<Rightarrow> Target_Numeral.int \<Rightarrow> Target_Numeral.int \<times> Target_Numeral.int" where |
|
261 |
"divmod_abs k l = (\<bar>k\<bar> div \<bar>l\<bar>, \<bar>k\<bar> mod \<bar>l\<bar>)" |
|
262 |
||
263 |
lemma fst_divmod_abs [simp]: |
|
264 |
"fst (divmod_abs k l) = \<bar>k\<bar> div \<bar>l\<bar>" |
|
265 |
by (simp add: divmod_abs_def) |
|
266 |
||
267 |
lemma snd_divmod_abs [simp]: |
|
268 |
"snd (divmod_abs k l) = \<bar>k\<bar> mod \<bar>l\<bar>" |
|
269 |
by (simp add: divmod_abs_def) |
|
270 |
||
271 |
lemma divmod_abs_terminate_code [code]: |
|
272 |
"divmod_abs (Neg k) (Neg l) = divmod_abs (Pos k) (Pos l)" |
|
273 |
"divmod_abs (Neg k) (Pos l) = divmod_abs (Pos k) (Pos l)" |
|
274 |
"divmod_abs (Pos k) (Neg l) = divmod_abs (Pos k) (Pos l)" |
|
275 |
"divmod_abs j 0 = (0, \<bar>j\<bar>)" |
|
276 |
"divmod_abs 0 j = (0, 0)" |
|
277 |
by (simp_all add: prod_eq_iff) |
|
278 |
||
279 |
lemma divmod_abs_rec_code [code]: |
|
280 |
"divmod_abs (Pos k) (Pos l) = |
|
281 |
(let j = sub k l in |
|
282 |
if j < 0 then (0, Pos k) |
|
283 |
else let (q, r) = divmod_abs j (Pos l) in (q + 1, r))" |
|
284 |
by (auto simp add: prod_eq_iff Target_Numeral.int_eq_iff Let_def prod_case_beta |
|
285 |
sub_non_negative sub_negative div_pos_pos_trivial mod_pos_pos_trivial div_pos_geq mod_pos_geq) |
|
286 |
||
287 |
lemma divmod_code [code]: "divmod k l = |
|
288 |
(if k = 0 then (0, 0) else if l = 0 then (0, k) else |
|
289 |
(apsnd \<circ> times \<circ> sgn) l (if sgn k = sgn l |
|
290 |
then divmod_abs k l |
|
291 |
else (let (r, s) = divmod_abs k l in |
|
292 |
if s = 0 then (- r, 0) else (- r - 1, \<bar>l\<bar> - s))))" |
|
293 |
proof - |
|
294 |
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" |
|
295 |
by (auto simp add: sgn_if) |
|
296 |
have aux2: "\<And>q::int. - int_of k = int_of l * q \<longleftrightarrow> int_of k = int_of l * - q" by auto |
|
297 |
show ?thesis |
|
298 |
by (simp add: prod_eq_iff Target_Numeral.int_eq_iff prod_case_beta aux1) |
|
47159 | 299 |
(auto simp add: zdiv_zminus1_eq_if zmod_zminus1_eq_if div_minus_right mod_minus_right aux2) |
47108 | 300 |
qed |
301 |
||
302 |
lemma div_int_code [code]: |
|
303 |
"k div l = fst (divmod k l)" |
|
304 |
by simp |
|
305 |
||
306 |
lemma div_mod_code [code]: |
|
307 |
"k mod l = snd (divmod k l)" |
|
308 |
by simp |
|
309 |
||
310 |
lemma equal_int_code [code]: |
|
311 |
"HOL.equal 0 (0::Target_Numeral.int) \<longleftrightarrow> True" |
|
312 |
"HOL.equal 0 (Pos l) \<longleftrightarrow> False" |
|
313 |
"HOL.equal 0 (Neg l) \<longleftrightarrow> False" |
|
314 |
"HOL.equal (Pos k) 0 \<longleftrightarrow> False" |
|
315 |
"HOL.equal (Pos k) (Pos l) \<longleftrightarrow> HOL.equal k l" |
|
316 |
"HOL.equal (Pos k) (Neg l) \<longleftrightarrow> False" |
|
317 |
"HOL.equal (Neg k) 0 \<longleftrightarrow> False" |
|
318 |
"HOL.equal (Neg k) (Pos l) \<longleftrightarrow> False" |
|
319 |
"HOL.equal (Neg k) (Neg l) \<longleftrightarrow> HOL.equal k l" |
|
320 |
by (simp_all add: equal Target_Numeral.int_eq_iff) |
|
321 |
||
322 |
lemma equal_int_refl [code nbe]: |
|
323 |
"HOL.equal (k::Target_Numeral.int) k \<longleftrightarrow> True" |
|
324 |
by (fact equal_refl) |
|
325 |
||
326 |
lemma less_eq_int_code [code]: |
|
327 |
"0 \<le> (0::Target_Numeral.int) \<longleftrightarrow> True" |
|
328 |
"0 \<le> Pos l \<longleftrightarrow> True" |
|
329 |
"0 \<le> Neg l \<longleftrightarrow> False" |
|
330 |
"Pos k \<le> 0 \<longleftrightarrow> False" |
|
331 |
"Pos k \<le> Pos l \<longleftrightarrow> k \<le> l" |
|
332 |
"Pos k \<le> Neg l \<longleftrightarrow> False" |
|
333 |
"Neg k \<le> 0 \<longleftrightarrow> True" |
|
334 |
"Neg k \<le> Pos l \<longleftrightarrow> True" |
|
335 |
"Neg k \<le> Neg l \<longleftrightarrow> l \<le> k" |
|
336 |
by (simp_all add: less_eq_int_def) |
|
337 |
||
338 |
lemma less_int_code [code]: |
|
339 |
"0 < (0::Target_Numeral.int) \<longleftrightarrow> False" |
|
340 |
"0 < Pos l \<longleftrightarrow> True" |
|
341 |
"0 < Neg l \<longleftrightarrow> False" |
|
342 |
"Pos k < 0 \<longleftrightarrow> False" |
|
343 |
"Pos k < Pos l \<longleftrightarrow> k < l" |
|
344 |
"Pos k < Neg l \<longleftrightarrow> False" |
|
345 |
"Neg k < 0 \<longleftrightarrow> True" |
|
346 |
"Neg k < Pos l \<longleftrightarrow> True" |
|
347 |
"Neg k < Neg l \<longleftrightarrow> l < k" |
|
348 |
by (simp_all add: less_int_def) |
|
349 |
||
350 |
lemma nat_of_code [code]: |
|
351 |
"nat_of (Neg k) = 0" |
|
352 |
"nat_of 0 = 0" |
|
353 |
"nat_of (Pos k) = nat_of_num k" |
|
354 |
by (simp_all add: nat_of_def nat_of_num_numeral) |
|
355 |
||
356 |
lemma int_of_code [code]: |
|
357 |
"int_of (Neg k) = neg_numeral k" |
|
358 |
"int_of 0 = 0" |
|
359 |
"int_of (Pos k) = numeral k" |
|
360 |
by simp_all |
|
361 |
||
362 |
lemma of_int_code [code]: |
|
363 |
"Target_Numeral.of_int (Int.Neg k) = neg_numeral k" |
|
364 |
"Target_Numeral.of_int 0 = 0" |
|
365 |
"Target_Numeral.of_int (Int.Pos k) = numeral k" |
|
366 |
by simp_all |
|
367 |
||
368 |
definition num_of_int :: "Target_Numeral.int \<Rightarrow> num" where |
|
369 |
"num_of_int = num_of_nat \<circ> nat_of" |
|
370 |
||
371 |
lemma num_of_int_code [code]: |
|
372 |
"num_of_int k = (if k \<le> 1 then Num.One |
|
373 |
else let |
|
374 |
(l, j) = divmod k 2; |
|
375 |
l' = num_of_int l + num_of_int l |
|
376 |
in if j = 0 then l' else l' + Num.One)" |
|
377 |
proof - |
|
378 |
{ |
|
379 |
assume "int_of k mod 2 = 1" |
|
380 |
then have "nat (int_of k mod 2) = nat 1" by simp |
|
381 |
moreover assume *: "1 < int_of k" |
|
382 |
ultimately have **: "nat (int_of k) mod 2 = 1" by (simp add: nat_mod_distrib) |
|
383 |
have "num_of_nat (nat (int_of k)) = |
|
384 |
num_of_nat (2 * (nat (int_of k) div 2) + nat (int_of k) mod 2)" |
|
385 |
by simp |
|
386 |
then have "num_of_nat (nat (int_of k)) = |
|
387 |
num_of_nat (nat (int_of k) div 2 + nat (int_of k) div 2 + nat (int_of k) mod 2)" |
|
47217
501b9bbd0d6e
removed redundant nat-specific copies of theorems
huffman
parents:
47159
diff
changeset
|
388 |
by (simp add: mult_2) |
47108 | 389 |
with ** have "num_of_nat (nat (int_of k)) = |
390 |
num_of_nat (nat (int_of k) div 2 + nat (int_of k) div 2 + 1)" |
|
391 |
by simp |
|
392 |
} |
|
393 |
note aux = this |
|
394 |
show ?thesis |
|
395 |
by (auto simp add: num_of_int_def nat_of_def Let_def prod_case_beta |
|
396 |
not_le Target_Numeral.int_eq_iff less_eq_int_def |
|
397 |
nat_mult_distrib nat_div_distrib num_of_nat_One num_of_nat_plus_distrib |
|
47217
501b9bbd0d6e
removed redundant nat-specific copies of theorems
huffman
parents:
47159
diff
changeset
|
398 |
mult_2 [where 'a=nat] aux add_One) |
47108 | 399 |
qed |
400 |
||
401 |
hide_const (open) int_of nat_of Pos Neg sub dup divmod_abs num_of_int |
|
402 |
||
403 |
||
404 |
subsection {* Serializer setup for target language numerals *} |
|
405 |
||
406 |
code_type Target_Numeral.int |
|
407 |
(SML "IntInf.int") |
|
408 |
(OCaml "Big'_int.big'_int") |
|
409 |
(Haskell "Integer") |
|
410 |
(Scala "BigInt") |
|
411 |
(Eval "int") |
|
412 |
||
413 |
code_instance Target_Numeral.int :: equal |
|
414 |
(Haskell -) |
|
415 |
||
416 |
code_const "0::Target_Numeral.int" |
|
417 |
(SML "0") |
|
418 |
(OCaml "Big'_int.zero'_big'_int") |
|
419 |
(Haskell "0") |
|
420 |
(Scala "BigInt(0)") |
|
421 |
||
422 |
setup {* |
|
423 |
fold (Numeral.add_code @{const_name Target_Numeral.Pos} |
|
424 |
false Code_Printer.literal_numeral) ["SML", "OCaml", "Haskell", "Scala"] |
|
425 |
*} |
|
426 |
||
427 |
setup {* |
|
428 |
fold (Numeral.add_code @{const_name Target_Numeral.Neg} |
|
429 |
true Code_Printer.literal_numeral) ["SML", "OCaml", "Haskell", "Scala"] |
|
430 |
*} |
|
431 |
||
432 |
code_const "plus :: Target_Numeral.int \<Rightarrow> _ \<Rightarrow> _" |
|
433 |
(SML "IntInf.+ ((_), (_))") |
|
434 |
(OCaml "Big'_int.add'_big'_int") |
|
435 |
(Haskell infixl 6 "+") |
|
436 |
(Scala infixl 7 "+") |
|
437 |
(Eval infixl 8 "+") |
|
438 |
||
439 |
code_const "uminus :: Target_Numeral.int \<Rightarrow> _" |
|
440 |
(SML "IntInf.~") |
|
441 |
(OCaml "Big'_int.minus'_big'_int") |
|
442 |
(Haskell "negate") |
|
443 |
(Scala "!(- _)") |
|
444 |
(Eval "~/ _") |
|
445 |
||
446 |
code_const "minus :: Target_Numeral.int \<Rightarrow> _" |
|
447 |
(SML "IntInf.- ((_), (_))") |
|
448 |
(OCaml "Big'_int.sub'_big'_int") |
|
449 |
(Haskell infixl 6 "-") |
|
450 |
(Scala infixl 7 "-") |
|
451 |
(Eval infixl 8 "-") |
|
452 |
||
453 |
code_const Target_Numeral.dup |
|
454 |
(SML "IntInf.*/ (2,/ (_))") |
|
455 |
(OCaml "Big'_int.mult'_big'_int/ 2") |
|
456 |
(Haskell "!(2 * _)") |
|
457 |
(Scala "!(2 * _)") |
|
458 |
(Eval "!(2 * _)") |
|
459 |
||
460 |
code_const Target_Numeral.sub |
|
461 |
(SML "!(raise/ Fail/ \"sub\")") |
|
462 |
(OCaml "failwith/ \"sub\"") |
|
463 |
(Haskell "error/ \"sub\"") |
|
464 |
(Scala "!error(\"sub\")") |
|
465 |
||
466 |
code_const "times :: Target_Numeral.int \<Rightarrow> _ \<Rightarrow> _" |
|
467 |
(SML "IntInf.* ((_), (_))") |
|
468 |
(OCaml "Big'_int.mult'_big'_int") |
|
469 |
(Haskell infixl 7 "*") |
|
470 |
(Scala infixl 8 "*") |
|
471 |
(Eval infixl 9 "*") |
|
472 |
||
473 |
code_const Target_Numeral.divmod_abs |
|
474 |
(SML "IntInf.divMod/ (IntInf.abs _,/ IntInf.abs _)") |
|
475 |
(OCaml "Big'_int.quomod'_big'_int/ (Big'_int.abs'_big'_int _)/ (Big'_int.abs'_big'_int _)") |
|
476 |
(Haskell "divMod/ (abs _)/ (abs _)") |
|
477 |
(Scala "!((k: BigInt) => (l: BigInt) =>/ if (l == 0)/ (BigInt(0), k) else/ (k.abs '/% l.abs))") |
|
478 |
(Eval "Integer.div'_mod/ (abs _)/ (abs _)") |
|
479 |
||
480 |
code_const "HOL.equal :: Target_Numeral.int \<Rightarrow> _ \<Rightarrow> bool" |
|
481 |
(SML "!((_ : IntInf.int) = _)") |
|
482 |
(OCaml "Big'_int.eq'_big'_int") |
|
483 |
(Haskell infix 4 "==") |
|
484 |
(Scala infixl 5 "==") |
|
485 |
(Eval infixl 6 "=") |
|
486 |
||
487 |
code_const "less_eq :: Target_Numeral.int \<Rightarrow> _ \<Rightarrow> bool" |
|
488 |
(SML "IntInf.<= ((_), (_))") |
|
489 |
(OCaml "Big'_int.le'_big'_int") |
|
490 |
(Haskell infix 4 "<=") |
|
491 |
(Scala infixl 4 "<=") |
|
492 |
(Eval infixl 6 "<=") |
|
493 |
||
494 |
code_const "less :: Target_Numeral.int \<Rightarrow> _ \<Rightarrow> bool" |
|
495 |
(SML "IntInf.< ((_), (_))") |
|
496 |
(OCaml "Big'_int.lt'_big'_int") |
|
497 |
(Haskell infix 4 "<") |
|
498 |
(Scala infixl 4 "<") |
|
499 |
(Eval infixl 6 "<") |
|
500 |
||
501 |
ML {* |
|
502 |
structure Target_Numeral = |
|
503 |
struct |
|
504 |
||
505 |
val T = @{typ "Target_Numeral.int"}; |
|
506 |
||
507 |
end; |
|
508 |
*} |
|
509 |
||
510 |
code_reserved Eval Target_Numeral |
|
511 |
||
512 |
code_const "Code_Evaluation.term_of \<Colon> Target_Numeral.int \<Rightarrow> term" |
|
513 |
(Eval "HOLogic.mk'_number/ Target'_Numeral.T") |
|
514 |
||
515 |
code_modulename SML |
|
516 |
Target_Numeral Arith |
|
517 |
||
518 |
code_modulename OCaml |
|
519 |
Target_Numeral Arith |
|
520 |
||
521 |
code_modulename Haskell |
|
522 |
Target_Numeral Arith |
|
523 |
||
524 |
||
525 |
subsection {* Implementation for @{typ int} *} |
|
526 |
||
527 |
code_datatype Target_Numeral.int_of |
|
528 |
||
529 |
lemma [code, code del]: |
|
530 |
"Target_Numeral.of_int = Target_Numeral.of_int" .. |
|
531 |
||
532 |
lemma [code]: |
|
533 |
"Target_Numeral.of_int (Target_Numeral.int_of k) = k" |
|
534 |
by (simp add: Target_Numeral.int_eq_iff) |
|
535 |
||
536 |
declare Int.Pos_def [code] |
|
537 |
||
538 |
lemma [code_abbrev]: |
|
539 |
"Target_Numeral.int_of (Target_Numeral.Pos k) = Int.Pos k" |
|
540 |
by simp |
|
541 |
||
542 |
declare Int.Neg_def [code] |
|
543 |
||
544 |
lemma [code_abbrev]: |
|
545 |
"Target_Numeral.int_of (Target_Numeral.Neg k) = Int.Neg k" |
|
546 |
by simp |
|
547 |
||
548 |
lemma [code]: |
|
549 |
"0 = Target_Numeral.int_of 0" |
|
550 |
by simp |
|
551 |
||
552 |
lemma [code]: |
|
553 |
"1 = Target_Numeral.int_of 1" |
|
554 |
by simp |
|
555 |
||
556 |
lemma [code]: |
|
557 |
"k + l = Target_Numeral.int_of (of_int k + of_int l)" |
|
558 |
by simp |
|
559 |
||
560 |
lemma [code]: |
|
561 |
"- k = Target_Numeral.int_of (- of_int k)" |
|
562 |
by simp |
|
563 |
||
564 |
lemma [code]: |
|
565 |
"k - l = Target_Numeral.int_of (of_int k - of_int l)" |
|
566 |
by simp |
|
567 |
||
568 |
lemma [code]: |
|
569 |
"Int.dup k = Target_Numeral.int_of (Target_Numeral.dup (of_int k))" |
|
570 |
by simp |
|
571 |
||
572 |
lemma [code, code del]: |
|
573 |
"Int.sub = Int.sub" .. |
|
574 |
||
575 |
lemma [code]: |
|
576 |
"k * l = Target_Numeral.int_of (of_int k * of_int l)" |
|
577 |
by simp |
|
578 |
||
579 |
lemma [code]: |
|
580 |
"pdivmod k l = map_pair Target_Numeral.int_of Target_Numeral.int_of |
|
581 |
(Target_Numeral.divmod_abs (of_int k) (of_int l))" |
|
582 |
by (simp add: prod_eq_iff pdivmod_def) |
|
583 |
||
584 |
lemma [code]: |
|
585 |
"k div l = Target_Numeral.int_of (of_int k div of_int l)" |
|
586 |
by simp |
|
587 |
||
588 |
lemma [code]: |
|
589 |
"k mod l = Target_Numeral.int_of (of_int k mod of_int l)" |
|
590 |
by simp |
|
591 |
||
592 |
lemma [code]: |
|
593 |
"HOL.equal k l = HOL.equal (of_int k :: Target_Numeral.int) (of_int l)" |
|
594 |
by (simp add: equal Target_Numeral.int_eq_iff) |
|
595 |
||
596 |
lemma [code]: |
|
597 |
"k \<le> l \<longleftrightarrow> (of_int k :: Target_Numeral.int) \<le> of_int l" |
|
598 |
by (simp add: less_eq_int_def) |
|
599 |
||
600 |
lemma [code]: |
|
601 |
"k < l \<longleftrightarrow> (of_int k :: Target_Numeral.int) < of_int l" |
|
602 |
by (simp add: less_int_def) |
|
603 |
||
604 |
lemma (in ring_1) of_int_code: |
|
605 |
"of_int k = (if k = 0 then 0 |
|
606 |
else if k < 0 then - of_int (- k) |
|
607 |
else let |
|
608 |
(l, j) = divmod_int k 2; |
|
609 |
l' = 2 * of_int l |
|
610 |
in if j = 0 then l' else l' + 1)" |
|
611 |
proof - |
|
612 |
from mod_div_equality have *: "of_int k = of_int (k div 2 * 2 + k mod 2)" by simp |
|
613 |
show ?thesis |
|
614 |
by (simp add: Let_def divmod_int_mod_div mod_2_not_eq_zero_eq_one_int |
|
615 |
of_int_add [symmetric]) (simp add: * mult_commute) |
|
616 |
qed |
|
617 |
||
618 |
declare of_int_code [code] |
|
619 |
||
620 |
||
621 |
subsection {* Implementation for @{typ nat} *} |
|
622 |
||
623 |
definition of_nat :: "nat \<Rightarrow> Target_Numeral.int" where |
|
624 |
[code_abbrev]: "of_nat = Nat.of_nat" |
|
625 |
||
626 |
hide_const (open) of_nat |
|
627 |
||
628 |
lemma int_of_nat [simp]: |
|
629 |
"Target_Numeral.int_of (Target_Numeral.of_nat n) = of_nat n" |
|
630 |
by (simp add: of_nat_def) |
|
631 |
||
632 |
lemma [code abstype]: |
|
633 |
"Target_Numeral.nat_of (Target_Numeral.of_nat n) = n" |
|
634 |
by (simp add: nat_of_def) |
|
635 |
||
636 |
lemma [code_abbrev]: |
|
637 |
"nat (Int.Pos k) = nat_of_num k" |
|
638 |
by (simp add: nat_of_num_numeral) |
|
639 |
||
640 |
lemma [code abstract]: |
|
641 |
"Target_Numeral.of_nat 0 = 0" |
|
642 |
by (simp add: Target_Numeral.int_eq_iff) |
|
643 |
||
644 |
lemma [code abstract]: |
|
645 |
"Target_Numeral.of_nat 1 = 1" |
|
646 |
by (simp add: Target_Numeral.int_eq_iff) |
|
647 |
||
648 |
lemma [code abstract]: |
|
649 |
"Target_Numeral.of_nat (m + n) = of_nat m + of_nat n" |
|
650 |
by (simp add: Target_Numeral.int_eq_iff) |
|
651 |
||
652 |
lemma [code abstract]: |
|
653 |
"Target_Numeral.of_nat (Code_Nat.dup n) = Target_Numeral.dup (of_nat n)" |
|
654 |
by (simp add: Target_Numeral.int_eq_iff Code_Nat.dup_def) |
|
655 |
||
656 |
lemma [code, code del]: |
|
657 |
"Code_Nat.sub = Code_Nat.sub" .. |
|
658 |
||
659 |
lemma [code abstract]: |
|
660 |
"Target_Numeral.of_nat (m - n) = max 0 (of_nat m - of_nat n)" |
|
661 |
by (simp add: Target_Numeral.int_eq_iff) |
|
662 |
||
663 |
lemma [code abstract]: |
|
664 |
"Target_Numeral.of_nat (m * n) = of_nat m * of_nat n" |
|
665 |
by (simp add: Target_Numeral.int_eq_iff of_nat_mult) |
|
666 |
||
667 |
lemma [code abstract]: |
|
668 |
"Target_Numeral.of_nat (m div n) = of_nat m div of_nat n" |
|
669 |
by (simp add: Target_Numeral.int_eq_iff zdiv_int) |
|
670 |
||
671 |
lemma [code abstract]: |
|
672 |
"Target_Numeral.of_nat (m mod n) = of_nat m mod of_nat n" |
|
673 |
by (simp add: Target_Numeral.int_eq_iff zmod_int) |
|
674 |
||
675 |
lemma [code]: |
|
676 |
"Divides.divmod_nat m n = (m div n, m mod n)" |
|
677 |
by (simp add: prod_eq_iff) |
|
678 |
||
679 |
lemma [code]: |
|
680 |
"HOL.equal m n = HOL.equal (of_nat m :: Target_Numeral.int) (of_nat n)" |
|
681 |
by (simp add: equal Target_Numeral.int_eq_iff) |
|
682 |
||
683 |
lemma [code]: |
|
684 |
"m \<le> n \<longleftrightarrow> (of_nat m :: Target_Numeral.int) \<le> of_nat n" |
|
685 |
by (simp add: less_eq_int_def) |
|
686 |
||
687 |
lemma [code]: |
|
688 |
"m < n \<longleftrightarrow> (of_nat m :: Target_Numeral.int) < of_nat n" |
|
689 |
by (simp add: less_int_def) |
|
690 |
||
691 |
lemma num_of_nat_code [code]: |
|
692 |
"num_of_nat = Target_Numeral.num_of_int \<circ> Target_Numeral.of_nat" |
|
693 |
by (simp add: fun_eq_iff num_of_int_def of_nat_def) |
|
694 |
||
695 |
lemma (in semiring_1) of_nat_code: |
|
696 |
"of_nat n = (if n = 0 then 0 |
|
697 |
else let |
|
698 |
(m, q) = divmod_nat n 2; |
|
699 |
m' = 2 * of_nat m |
|
700 |
in if q = 0 then m' else m' + 1)" |
|
701 |
proof - |
|
702 |
from mod_div_equality have *: "of_nat n = of_nat (n div 2 * 2 + n mod 2)" by simp |
|
703 |
show ?thesis |
|
704 |
by (simp add: Let_def divmod_nat_div_mod mod_2_not_eq_zero_eq_one_nat |
|
705 |
of_nat_add [symmetric]) |
|
706 |
(simp add: * mult_commute of_nat_mult add_commute) |
|
707 |
qed |
|
708 |
||
709 |
declare of_nat_code [code] |
|
710 |
||
711 |
text {* Conversions between @{typ nat} and @{typ int} *} |
|
712 |
||
713 |
definition int :: "nat \<Rightarrow> int" where |
|
714 |
[code_abbrev]: "int = of_nat" |
|
715 |
||
716 |
hide_const (open) int |
|
717 |
||
718 |
lemma [code]: |
|
719 |
"Target_Numeral.int n = Target_Numeral.int_of (of_nat n)" |
|
720 |
by (simp add: int_def) |
|
721 |
||
722 |
lemma [code abstract]: |
|
723 |
"Target_Numeral.of_nat (nat k) = max 0 (Target_Numeral.of_int k)" |
|
724 |
by (simp add: of_nat_def of_int_of_nat max_def) |
|
725 |
||
726 |
end |