author | Christian Sternagel |
Wed, 29 Aug 2012 12:24:26 +0900 | |
changeset 49084 | e3973567ed4f |
parent 48075 | ec5e62b868eb |
child 49834 | b27bbb021df1 |
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 |
||
47400
b7625245a846
explicit constructor Nat leaves nat_of as conversion
haftmann
parents:
47217
diff
changeset
|
166 |
lemma of_nat_nat_of [simp]: |
b7625245a846
explicit constructor Nat leaves nat_of as conversion
haftmann
parents:
47217
diff
changeset
|
167 |
"of_nat (nat_of k) = max 0 k" |
b7625245a846
explicit constructor Nat leaves nat_of as conversion
haftmann
parents:
47217
diff
changeset
|
168 |
by (simp add: nat_of_def Target_Numeral.int_eq_iff less_eq_int_def max_def) |
b7625245a846
explicit constructor Nat leaves nat_of as conversion
haftmann
parents:
47217
diff
changeset
|
169 |
|
47108 | 170 |
|
171 |
subsection {* Code theorems for target language numerals *} |
|
172 |
||
173 |
text {* Constructors *} |
|
174 |
||
175 |
definition Pos :: "num \<Rightarrow> Target_Numeral.int" where |
|
176 |
[simp, code_abbrev]: "Pos = numeral" |
|
177 |
||
178 |
definition Neg :: "num \<Rightarrow> Target_Numeral.int" where |
|
179 |
[simp, code_abbrev]: "Neg = neg_numeral" |
|
180 |
||
181 |
code_datatype "0::Target_Numeral.int" Pos Neg |
|
182 |
||
183 |
||
184 |
text {* Auxiliary operations *} |
|
185 |
||
186 |
definition dup :: "Target_Numeral.int \<Rightarrow> Target_Numeral.int" where |
|
187 |
[simp]: "dup k = k + k" |
|
188 |
||
189 |
lemma dup_code [code]: |
|
190 |
"dup 0 = 0" |
|
191 |
"dup (Pos n) = Pos (Num.Bit0 n)" |
|
192 |
"dup (Neg n) = Neg (Num.Bit0 n)" |
|
193 |
unfolding Pos_def Neg_def neg_numeral_def |
|
194 |
by (simp_all add: numeral_Bit0) |
|
195 |
||
196 |
definition sub :: "num \<Rightarrow> num \<Rightarrow> Target_Numeral.int" where |
|
197 |
[simp]: "sub m n = numeral m - numeral n" |
|
198 |
||
199 |
lemma sub_code [code]: |
|
200 |
"sub Num.One Num.One = 0" |
|
201 |
"sub (Num.Bit0 m) Num.One = Pos (Num.BitM m)" |
|
202 |
"sub (Num.Bit1 m) Num.One = Pos (Num.Bit0 m)" |
|
203 |
"sub Num.One (Num.Bit0 n) = Neg (Num.BitM n)" |
|
204 |
"sub Num.One (Num.Bit1 n) = Neg (Num.Bit0 n)" |
|
205 |
"sub (Num.Bit0 m) (Num.Bit0 n) = dup (sub m n)" |
|
206 |
"sub (Num.Bit1 m) (Num.Bit1 n) = dup (sub m n)" |
|
207 |
"sub (Num.Bit1 m) (Num.Bit0 n) = dup (sub m n) + 1" |
|
208 |
"sub (Num.Bit0 m) (Num.Bit1 n) = dup (sub m n) - 1" |
|
209 |
unfolding sub_def dup_def numeral.simps Pos_def Neg_def |
|
210 |
neg_numeral_def numeral_BitM |
|
211 |
by (simp_all only: algebra_simps add.comm_neutral) |
|
212 |
||
213 |
||
214 |
text {* Implementations *} |
|
215 |
||
216 |
lemma one_int_code [code, code_unfold]: |
|
217 |
"1 = Pos Num.One" |
|
218 |
by simp |
|
219 |
||
220 |
lemma plus_int_code [code]: |
|
221 |
"k + 0 = (k::Target_Numeral.int)" |
|
222 |
"0 + l = (l::Target_Numeral.int)" |
|
223 |
"Pos m + Pos n = Pos (m + n)" |
|
224 |
"Pos m + Neg n = sub m n" |
|
225 |
"Neg m + Pos n = sub n m" |
|
226 |
"Neg m + Neg n = Neg (m + n)" |
|
227 |
by simp_all |
|
228 |
||
229 |
lemma uminus_int_code [code]: |
|
230 |
"uminus 0 = (0::Target_Numeral.int)" |
|
231 |
"uminus (Pos m) = Neg m" |
|
232 |
"uminus (Neg m) = Pos m" |
|
233 |
by simp_all |
|
234 |
||
235 |
lemma minus_int_code [code]: |
|
236 |
"k - 0 = (k::Target_Numeral.int)" |
|
237 |
"0 - l = uminus (l::Target_Numeral.int)" |
|
238 |
"Pos m - Pos n = sub m n" |
|
239 |
"Pos m - Neg n = Pos (m + n)" |
|
240 |
"Neg m - Pos n = Neg (m + n)" |
|
241 |
"Neg m - Neg n = sub n m" |
|
242 |
by simp_all |
|
243 |
||
244 |
lemma times_int_code [code]: |
|
245 |
"k * 0 = (0::Target_Numeral.int)" |
|
246 |
"0 * l = (0::Target_Numeral.int)" |
|
247 |
"Pos m * Pos n = Pos (m * n)" |
|
248 |
"Pos m * Neg n = Neg (m * n)" |
|
249 |
"Neg m * Pos n = Neg (m * n)" |
|
250 |
"Neg m * Neg n = Pos (m * n)" |
|
251 |
by simp_all |
|
252 |
||
253 |
definition divmod :: "Target_Numeral.int \<Rightarrow> Target_Numeral.int \<Rightarrow> Target_Numeral.int \<times> Target_Numeral.int" where |
|
254 |
"divmod k l = (k div l, k mod l)" |
|
255 |
||
256 |
lemma fst_divmod [simp]: |
|
257 |
"fst (divmod k l) = k div l" |
|
258 |
by (simp add: divmod_def) |
|
259 |
||
260 |
lemma snd_divmod [simp]: |
|
261 |
"snd (divmod k l) = k mod l" |
|
262 |
by (simp add: divmod_def) |
|
263 |
||
264 |
definition divmod_abs :: "Target_Numeral.int \<Rightarrow> Target_Numeral.int \<Rightarrow> Target_Numeral.int \<times> Target_Numeral.int" where |
|
265 |
"divmod_abs k l = (\<bar>k\<bar> div \<bar>l\<bar>, \<bar>k\<bar> mod \<bar>l\<bar>)" |
|
266 |
||
267 |
lemma fst_divmod_abs [simp]: |
|
268 |
"fst (divmod_abs k l) = \<bar>k\<bar> div \<bar>l\<bar>" |
|
269 |
by (simp add: divmod_abs_def) |
|
270 |
||
271 |
lemma snd_divmod_abs [simp]: |
|
272 |
"snd (divmod_abs k l) = \<bar>k\<bar> mod \<bar>l\<bar>" |
|
273 |
by (simp add: divmod_abs_def) |
|
274 |
||
275 |
lemma divmod_abs_terminate_code [code]: |
|
276 |
"divmod_abs (Neg k) (Neg l) = divmod_abs (Pos k) (Pos l)" |
|
277 |
"divmod_abs (Neg k) (Pos l) = divmod_abs (Pos k) (Pos l)" |
|
278 |
"divmod_abs (Pos k) (Neg l) = divmod_abs (Pos k) (Pos l)" |
|
279 |
"divmod_abs j 0 = (0, \<bar>j\<bar>)" |
|
280 |
"divmod_abs 0 j = (0, 0)" |
|
281 |
by (simp_all add: prod_eq_iff) |
|
282 |
||
283 |
lemma divmod_abs_rec_code [code]: |
|
284 |
"divmod_abs (Pos k) (Pos l) = |
|
285 |
(let j = sub k l in |
|
286 |
if j < 0 then (0, Pos k) |
|
287 |
else let (q, r) = divmod_abs j (Pos l) in (q + 1, r))" |
|
288 |
by (auto simp add: prod_eq_iff Target_Numeral.int_eq_iff Let_def prod_case_beta |
|
289 |
sub_non_negative sub_negative div_pos_pos_trivial mod_pos_pos_trivial div_pos_geq mod_pos_geq) |
|
290 |
||
291 |
lemma divmod_code [code]: "divmod k l = |
|
292 |
(if k = 0 then (0, 0) else if l = 0 then (0, k) else |
|
293 |
(apsnd \<circ> times \<circ> sgn) l (if sgn k = sgn l |
|
294 |
then divmod_abs k l |
|
295 |
else (let (r, s) = divmod_abs k l in |
|
296 |
if s = 0 then (- r, 0) else (- r - 1, \<bar>l\<bar> - s))))" |
|
297 |
proof - |
|
298 |
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" |
|
299 |
by (auto simp add: sgn_if) |
|
300 |
have aux2: "\<And>q::int. - int_of k = int_of l * q \<longleftrightarrow> int_of k = int_of l * - q" by auto |
|
301 |
show ?thesis |
|
302 |
by (simp add: prod_eq_iff Target_Numeral.int_eq_iff prod_case_beta aux1) |
|
47159 | 303 |
(auto simp add: zdiv_zminus1_eq_if zmod_zminus1_eq_if div_minus_right mod_minus_right aux2) |
47108 | 304 |
qed |
305 |
||
306 |
lemma div_int_code [code]: |
|
307 |
"k div l = fst (divmod k l)" |
|
308 |
by simp |
|
309 |
||
310 |
lemma div_mod_code [code]: |
|
311 |
"k mod l = snd (divmod k l)" |
|
312 |
by simp |
|
313 |
||
314 |
lemma equal_int_code [code]: |
|
315 |
"HOL.equal 0 (0::Target_Numeral.int) \<longleftrightarrow> True" |
|
316 |
"HOL.equal 0 (Pos l) \<longleftrightarrow> False" |
|
317 |
"HOL.equal 0 (Neg l) \<longleftrightarrow> False" |
|
318 |
"HOL.equal (Pos k) 0 \<longleftrightarrow> False" |
|
319 |
"HOL.equal (Pos k) (Pos l) \<longleftrightarrow> HOL.equal k l" |
|
320 |
"HOL.equal (Pos k) (Neg l) \<longleftrightarrow> False" |
|
321 |
"HOL.equal (Neg k) 0 \<longleftrightarrow> False" |
|
322 |
"HOL.equal (Neg k) (Pos l) \<longleftrightarrow> False" |
|
323 |
"HOL.equal (Neg k) (Neg l) \<longleftrightarrow> HOL.equal k l" |
|
324 |
by (simp_all add: equal Target_Numeral.int_eq_iff) |
|
325 |
||
326 |
lemma equal_int_refl [code nbe]: |
|
327 |
"HOL.equal (k::Target_Numeral.int) k \<longleftrightarrow> True" |
|
328 |
by (fact equal_refl) |
|
329 |
||
330 |
lemma less_eq_int_code [code]: |
|
331 |
"0 \<le> (0::Target_Numeral.int) \<longleftrightarrow> True" |
|
332 |
"0 \<le> Pos l \<longleftrightarrow> True" |
|
333 |
"0 \<le> Neg l \<longleftrightarrow> False" |
|
334 |
"Pos k \<le> 0 \<longleftrightarrow> False" |
|
335 |
"Pos k \<le> Pos l \<longleftrightarrow> k \<le> l" |
|
336 |
"Pos k \<le> Neg l \<longleftrightarrow> False" |
|
337 |
"Neg k \<le> 0 \<longleftrightarrow> True" |
|
338 |
"Neg k \<le> Pos l \<longleftrightarrow> True" |
|
339 |
"Neg k \<le> Neg l \<longleftrightarrow> l \<le> k" |
|
340 |
by (simp_all add: less_eq_int_def) |
|
341 |
||
342 |
lemma less_int_code [code]: |
|
343 |
"0 < (0::Target_Numeral.int) \<longleftrightarrow> False" |
|
344 |
"0 < Pos l \<longleftrightarrow> True" |
|
345 |
"0 < Neg l \<longleftrightarrow> False" |
|
346 |
"Pos k < 0 \<longleftrightarrow> False" |
|
347 |
"Pos k < Pos l \<longleftrightarrow> k < l" |
|
348 |
"Pos k < Neg l \<longleftrightarrow> False" |
|
349 |
"Neg k < 0 \<longleftrightarrow> True" |
|
350 |
"Neg k < Pos l \<longleftrightarrow> True" |
|
351 |
"Neg k < Neg l \<longleftrightarrow> l < k" |
|
352 |
by (simp_all add: less_int_def) |
|
353 |
||
354 |
lemma nat_of_code [code]: |
|
355 |
"nat_of (Neg k) = 0" |
|
356 |
"nat_of 0 = 0" |
|
357 |
"nat_of (Pos k) = nat_of_num k" |
|
358 |
by (simp_all add: nat_of_def nat_of_num_numeral) |
|
359 |
||
360 |
lemma int_of_code [code]: |
|
361 |
"int_of (Neg k) = neg_numeral k" |
|
362 |
"int_of 0 = 0" |
|
363 |
"int_of (Pos k) = numeral k" |
|
364 |
by simp_all |
|
365 |
||
366 |
lemma of_int_code [code]: |
|
367 |
"Target_Numeral.of_int (Int.Neg k) = neg_numeral k" |
|
368 |
"Target_Numeral.of_int 0 = 0" |
|
369 |
"Target_Numeral.of_int (Int.Pos k) = numeral k" |
|
370 |
by simp_all |
|
371 |
||
372 |
definition num_of_int :: "Target_Numeral.int \<Rightarrow> num" where |
|
373 |
"num_of_int = num_of_nat \<circ> nat_of" |
|
374 |
||
375 |
lemma num_of_int_code [code]: |
|
376 |
"num_of_int k = (if k \<le> 1 then Num.One |
|
377 |
else let |
|
378 |
(l, j) = divmod k 2; |
|
379 |
l' = num_of_int l + num_of_int l |
|
380 |
in if j = 0 then l' else l' + Num.One)" |
|
381 |
proof - |
|
382 |
{ |
|
383 |
assume "int_of k mod 2 = 1" |
|
384 |
then have "nat (int_of k mod 2) = nat 1" by simp |
|
385 |
moreover assume *: "1 < int_of k" |
|
386 |
ultimately have **: "nat (int_of k) mod 2 = 1" by (simp add: nat_mod_distrib) |
|
387 |
have "num_of_nat (nat (int_of k)) = |
|
388 |
num_of_nat (2 * (nat (int_of k) div 2) + nat (int_of k) mod 2)" |
|
389 |
by simp |
|
390 |
then have "num_of_nat (nat (int_of k)) = |
|
391 |
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
|
392 |
by (simp add: mult_2) |
47108 | 393 |
with ** have "num_of_nat (nat (int_of k)) = |
394 |
num_of_nat (nat (int_of k) div 2 + nat (int_of k) div 2 + 1)" |
|
395 |
by simp |
|
396 |
} |
|
397 |
note aux = this |
|
398 |
show ?thesis |
|
399 |
by (auto simp add: num_of_int_def nat_of_def Let_def prod_case_beta |
|
400 |
not_le Target_Numeral.int_eq_iff less_eq_int_def |
|
401 |
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
|
402 |
mult_2 [where 'a=nat] aux add_One) |
47108 | 403 |
qed |
404 |
||
405 |
hide_const (open) int_of nat_of Pos Neg sub dup divmod_abs num_of_int |
|
406 |
||
407 |
||
408 |
subsection {* Serializer setup for target language numerals *} |
|
409 |
||
410 |
code_type Target_Numeral.int |
|
411 |
(SML "IntInf.int") |
|
412 |
(OCaml "Big'_int.big'_int") |
|
413 |
(Haskell "Integer") |
|
414 |
(Scala "BigInt") |
|
415 |
(Eval "int") |
|
416 |
||
417 |
code_instance Target_Numeral.int :: equal |
|
418 |
(Haskell -) |
|
419 |
||
420 |
code_const "0::Target_Numeral.int" |
|
421 |
(SML "0") |
|
422 |
(OCaml "Big'_int.zero'_big'_int") |
|
423 |
(Haskell "0") |
|
424 |
(Scala "BigInt(0)") |
|
425 |
||
426 |
setup {* |
|
427 |
fold (Numeral.add_code @{const_name Target_Numeral.Pos} |
|
428 |
false Code_Printer.literal_numeral) ["SML", "OCaml", "Haskell", "Scala"] |
|
429 |
*} |
|
430 |
||
431 |
setup {* |
|
432 |
fold (Numeral.add_code @{const_name Target_Numeral.Neg} |
|
433 |
true Code_Printer.literal_numeral) ["SML", "OCaml", "Haskell", "Scala"] |
|
434 |
*} |
|
435 |
||
436 |
code_const "plus :: Target_Numeral.int \<Rightarrow> _ \<Rightarrow> _" |
|
437 |
(SML "IntInf.+ ((_), (_))") |
|
438 |
(OCaml "Big'_int.add'_big'_int") |
|
439 |
(Haskell infixl 6 "+") |
|
440 |
(Scala infixl 7 "+") |
|
441 |
(Eval infixl 8 "+") |
|
442 |
||
443 |
code_const "uminus :: Target_Numeral.int \<Rightarrow> _" |
|
444 |
(SML "IntInf.~") |
|
445 |
(OCaml "Big'_int.minus'_big'_int") |
|
446 |
(Haskell "negate") |
|
447 |
(Scala "!(- _)") |
|
448 |
(Eval "~/ _") |
|
449 |
||
450 |
code_const "minus :: Target_Numeral.int \<Rightarrow> _" |
|
451 |
(SML "IntInf.- ((_), (_))") |
|
452 |
(OCaml "Big'_int.sub'_big'_int") |
|
453 |
(Haskell infixl 6 "-") |
|
454 |
(Scala infixl 7 "-") |
|
455 |
(Eval infixl 8 "-") |
|
456 |
||
457 |
code_const Target_Numeral.dup |
|
458 |
(SML "IntInf.*/ (2,/ (_))") |
|
459 |
(OCaml "Big'_int.mult'_big'_int/ 2") |
|
460 |
(Haskell "!(2 * _)") |
|
461 |
(Scala "!(2 * _)") |
|
462 |
(Eval "!(2 * _)") |
|
463 |
||
464 |
code_const Target_Numeral.sub |
|
465 |
(SML "!(raise/ Fail/ \"sub\")") |
|
466 |
(OCaml "failwith/ \"sub\"") |
|
467 |
(Haskell "error/ \"sub\"") |
|
48073
1b609a7837ef
prefer sys.error over plain error in Scala to avoid deprecation warning
haftmann
parents:
47830
diff
changeset
|
468 |
(Scala "!sys.error(\"sub\")") |
47108 | 469 |
|
470 |
code_const "times :: Target_Numeral.int \<Rightarrow> _ \<Rightarrow> _" |
|
471 |
(SML "IntInf.* ((_), (_))") |
|
472 |
(OCaml "Big'_int.mult'_big'_int") |
|
473 |
(Haskell infixl 7 "*") |
|
474 |
(Scala infixl 8 "*") |
|
475 |
(Eval infixl 9 "*") |
|
476 |
||
477 |
code_const Target_Numeral.divmod_abs |
|
478 |
(SML "IntInf.divMod/ (IntInf.abs _,/ IntInf.abs _)") |
|
479 |
(OCaml "Big'_int.quomod'_big'_int/ (Big'_int.abs'_big'_int _)/ (Big'_int.abs'_big'_int _)") |
|
480 |
(Haskell "divMod/ (abs _)/ (abs _)") |
|
481 |
(Scala "!((k: BigInt) => (l: BigInt) =>/ if (l == 0)/ (BigInt(0), k) else/ (k.abs '/% l.abs))") |
|
482 |
(Eval "Integer.div'_mod/ (abs _)/ (abs _)") |
|
483 |
||
484 |
code_const "HOL.equal :: Target_Numeral.int \<Rightarrow> _ \<Rightarrow> bool" |
|
485 |
(SML "!((_ : IntInf.int) = _)") |
|
486 |
(OCaml "Big'_int.eq'_big'_int") |
|
487 |
(Haskell infix 4 "==") |
|
488 |
(Scala infixl 5 "==") |
|
489 |
(Eval infixl 6 "=") |
|
490 |
||
491 |
code_const "less_eq :: Target_Numeral.int \<Rightarrow> _ \<Rightarrow> bool" |
|
492 |
(SML "IntInf.<= ((_), (_))") |
|
493 |
(OCaml "Big'_int.le'_big'_int") |
|
494 |
(Haskell infix 4 "<=") |
|
495 |
(Scala infixl 4 "<=") |
|
496 |
(Eval infixl 6 "<=") |
|
497 |
||
498 |
code_const "less :: Target_Numeral.int \<Rightarrow> _ \<Rightarrow> bool" |
|
499 |
(SML "IntInf.< ((_), (_))") |
|
500 |
(OCaml "Big'_int.lt'_big'_int") |
|
501 |
(Haskell infix 4 "<") |
|
502 |
(Scala infixl 4 "<") |
|
503 |
(Eval infixl 6 "<") |
|
504 |
||
505 |
ML {* |
|
506 |
structure Target_Numeral = |
|
507 |
struct |
|
508 |
||
509 |
val T = @{typ "Target_Numeral.int"}; |
|
510 |
||
511 |
end; |
|
512 |
*} |
|
513 |
||
514 |
code_reserved Eval Target_Numeral |
|
515 |
||
516 |
code_const "Code_Evaluation.term_of \<Colon> Target_Numeral.int \<Rightarrow> term" |
|
517 |
(Eval "HOLogic.mk'_number/ Target'_Numeral.T") |
|
518 |
||
519 |
code_modulename SML |
|
520 |
Target_Numeral Arith |
|
521 |
||
522 |
code_modulename OCaml |
|
523 |
Target_Numeral Arith |
|
524 |
||
525 |
code_modulename Haskell |
|
526 |
Target_Numeral Arith |
|
527 |
||
528 |
||
529 |
subsection {* Implementation for @{typ int} *} |
|
530 |
||
531 |
code_datatype Target_Numeral.int_of |
|
532 |
||
533 |
lemma [code, code del]: |
|
534 |
"Target_Numeral.of_int = Target_Numeral.of_int" .. |
|
535 |
||
536 |
lemma [code]: |
|
537 |
"Target_Numeral.of_int (Target_Numeral.int_of k) = k" |
|
538 |
by (simp add: Target_Numeral.int_eq_iff) |
|
539 |
||
540 |
declare Int.Pos_def [code] |
|
541 |
||
542 |
lemma [code_abbrev]: |
|
543 |
"Target_Numeral.int_of (Target_Numeral.Pos k) = Int.Pos k" |
|
544 |
by simp |
|
545 |
||
546 |
declare Int.Neg_def [code] |
|
547 |
||
548 |
lemma [code_abbrev]: |
|
549 |
"Target_Numeral.int_of (Target_Numeral.Neg k) = Int.Neg k" |
|
550 |
by simp |
|
551 |
||
552 |
lemma [code]: |
|
553 |
"0 = Target_Numeral.int_of 0" |
|
554 |
by simp |
|
555 |
||
556 |
lemma [code]: |
|
557 |
"1 = Target_Numeral.int_of 1" |
|
558 |
by simp |
|
559 |
||
560 |
lemma [code]: |
|
561 |
"k + l = Target_Numeral.int_of (of_int k + of_int l)" |
|
562 |
by simp |
|
563 |
||
564 |
lemma [code]: |
|
565 |
"- k = Target_Numeral.int_of (- of_int k)" |
|
566 |
by simp |
|
567 |
||
568 |
lemma [code]: |
|
569 |
"k - l = Target_Numeral.int_of (of_int k - of_int l)" |
|
570 |
by simp |
|
571 |
||
572 |
lemma [code]: |
|
573 |
"Int.dup k = Target_Numeral.int_of (Target_Numeral.dup (of_int k))" |
|
574 |
by simp |
|
575 |
||
576 |
lemma [code, code del]: |
|
577 |
"Int.sub = Int.sub" .. |
|
578 |
||
579 |
lemma [code]: |
|
580 |
"k * l = Target_Numeral.int_of (of_int k * of_int l)" |
|
581 |
by simp |
|
582 |
||
583 |
lemma [code]: |
|
584 |
"pdivmod k l = map_pair Target_Numeral.int_of Target_Numeral.int_of |
|
585 |
(Target_Numeral.divmod_abs (of_int k) (of_int l))" |
|
586 |
by (simp add: prod_eq_iff pdivmod_def) |
|
587 |
||
588 |
lemma [code]: |
|
589 |
"k div l = Target_Numeral.int_of (of_int k div of_int l)" |
|
590 |
by simp |
|
591 |
||
592 |
lemma [code]: |
|
593 |
"k mod l = Target_Numeral.int_of (of_int k mod of_int l)" |
|
594 |
by simp |
|
595 |
||
596 |
lemma [code]: |
|
597 |
"HOL.equal k l = HOL.equal (of_int k :: Target_Numeral.int) (of_int l)" |
|
598 |
by (simp add: equal Target_Numeral.int_eq_iff) |
|
599 |
||
600 |
lemma [code]: |
|
601 |
"k \<le> l \<longleftrightarrow> (of_int k :: Target_Numeral.int) \<le> of_int l" |
|
602 |
by (simp add: less_eq_int_def) |
|
603 |
||
604 |
lemma [code]: |
|
605 |
"k < l \<longleftrightarrow> (of_int k :: Target_Numeral.int) < of_int l" |
|
606 |
by (simp add: less_int_def) |
|
607 |
||
608 |
lemma (in ring_1) of_int_code: |
|
609 |
"of_int k = (if k = 0 then 0 |
|
610 |
else if k < 0 then - of_int (- k) |
|
611 |
else let |
|
612 |
(l, j) = divmod_int k 2; |
|
613 |
l' = 2 * of_int l |
|
614 |
in if j = 0 then l' else l' + 1)" |
|
615 |
proof - |
|
616 |
from mod_div_equality have *: "of_int k = of_int (k div 2 * 2 + k mod 2)" by simp |
|
617 |
show ?thesis |
|
618 |
by (simp add: Let_def divmod_int_mod_div mod_2_not_eq_zero_eq_one_int |
|
619 |
of_int_add [symmetric]) (simp add: * mult_commute) |
|
620 |
qed |
|
621 |
||
622 |
declare of_int_code [code] |
|
623 |
||
624 |
||
625 |
subsection {* Implementation for @{typ nat} *} |
|
626 |
||
47400
b7625245a846
explicit constructor Nat leaves nat_of as conversion
haftmann
parents:
47217
diff
changeset
|
627 |
definition Nat :: "Target_Numeral.int \<Rightarrow> nat" where |
b7625245a846
explicit constructor Nat leaves nat_of as conversion
haftmann
parents:
47217
diff
changeset
|
628 |
"Nat = Target_Numeral.nat_of" |
b7625245a846
explicit constructor Nat leaves nat_of as conversion
haftmann
parents:
47217
diff
changeset
|
629 |
|
47108 | 630 |
definition of_nat :: "nat \<Rightarrow> Target_Numeral.int" where |
631 |
[code_abbrev]: "of_nat = Nat.of_nat" |
|
632 |
||
47400
b7625245a846
explicit constructor Nat leaves nat_of as conversion
haftmann
parents:
47217
diff
changeset
|
633 |
hide_const (open) of_nat Nat |
47108 | 634 |
|
47830 | 635 |
lemma [code_unfold]: |
636 |
"Int.nat (Target_Numeral.int_of k) = Target_Numeral.nat_of k" |
|
637 |
by (simp add: nat_of_def) |
|
638 |
||
47108 | 639 |
lemma int_of_nat [simp]: |
640 |
"Target_Numeral.int_of (Target_Numeral.of_nat n) = of_nat n" |
|
641 |
by (simp add: of_nat_def) |
|
642 |
||
643 |
lemma [code abstype]: |
|
47400
b7625245a846
explicit constructor Nat leaves nat_of as conversion
haftmann
parents:
47217
diff
changeset
|
644 |
"Target_Numeral.Nat (Target_Numeral.of_nat n) = n" |
b7625245a846
explicit constructor Nat leaves nat_of as conversion
haftmann
parents:
47217
diff
changeset
|
645 |
by (simp add: Nat_def nat_of_def) |
b7625245a846
explicit constructor Nat leaves nat_of as conversion
haftmann
parents:
47217
diff
changeset
|
646 |
|
b7625245a846
explicit constructor Nat leaves nat_of as conversion
haftmann
parents:
47217
diff
changeset
|
647 |
lemma [code abstract]: |
b7625245a846
explicit constructor Nat leaves nat_of as conversion
haftmann
parents:
47217
diff
changeset
|
648 |
"Target_Numeral.of_nat (Target_Numeral.nat_of k) = max 0 k" |
b7625245a846
explicit constructor Nat leaves nat_of as conversion
haftmann
parents:
47217
diff
changeset
|
649 |
by (simp add: of_nat_def) |
47108 | 650 |
|
651 |
lemma [code_abbrev]: |
|
652 |
"nat (Int.Pos k) = nat_of_num k" |
|
653 |
by (simp add: nat_of_num_numeral) |
|
654 |
||
655 |
lemma [code abstract]: |
|
656 |
"Target_Numeral.of_nat 0 = 0" |
|
657 |
by (simp add: Target_Numeral.int_eq_iff) |
|
658 |
||
659 |
lemma [code abstract]: |
|
660 |
"Target_Numeral.of_nat 1 = 1" |
|
661 |
by (simp add: Target_Numeral.int_eq_iff) |
|
662 |
||
663 |
lemma [code abstract]: |
|
48075
ec5e62b868eb
apply preprocessing simpset also to rhs of abstract code equations
haftmann
parents:
48073
diff
changeset
|
664 |
"Target_Numeral.of_nat (m + n) = of_nat m + of_nat n" |
47108 | 665 |
by (simp add: Target_Numeral.int_eq_iff) |
666 |
||
667 |
lemma [code abstract]: |
|
48075
ec5e62b868eb
apply preprocessing simpset also to rhs of abstract code equations
haftmann
parents:
48073
diff
changeset
|
668 |
"Target_Numeral.of_nat (Code_Nat.dup n) = Target_Numeral.dup (of_nat n)" |
47108 | 669 |
by (simp add: Target_Numeral.int_eq_iff Code_Nat.dup_def) |
670 |
||
671 |
lemma [code, code del]: |
|
672 |
"Code_Nat.sub = Code_Nat.sub" .. |
|
673 |
||
674 |
lemma [code abstract]: |
|
48075
ec5e62b868eb
apply preprocessing simpset also to rhs of abstract code equations
haftmann
parents:
48073
diff
changeset
|
675 |
"Target_Numeral.of_nat (m - n) = max 0 (of_nat m - of_nat n)" |
47108 | 676 |
by (simp add: Target_Numeral.int_eq_iff) |
677 |
||
678 |
lemma [code abstract]: |
|
48075
ec5e62b868eb
apply preprocessing simpset also to rhs of abstract code equations
haftmann
parents:
48073
diff
changeset
|
679 |
"Target_Numeral.of_nat (m * n) = of_nat m * of_nat n" |
47108 | 680 |
by (simp add: Target_Numeral.int_eq_iff of_nat_mult) |
681 |
||
682 |
lemma [code abstract]: |
|
48075
ec5e62b868eb
apply preprocessing simpset also to rhs of abstract code equations
haftmann
parents:
48073
diff
changeset
|
683 |
"Target_Numeral.of_nat (m div n) = of_nat m div of_nat n" |
47108 | 684 |
by (simp add: Target_Numeral.int_eq_iff zdiv_int) |
685 |
||
686 |
lemma [code abstract]: |
|
48075
ec5e62b868eb
apply preprocessing simpset also to rhs of abstract code equations
haftmann
parents:
48073
diff
changeset
|
687 |
"Target_Numeral.of_nat (m mod n) = of_nat m mod of_nat n" |
47108 | 688 |
by (simp add: Target_Numeral.int_eq_iff zmod_int) |
689 |
||
690 |
lemma [code]: |
|
691 |
"Divides.divmod_nat m n = (m div n, m mod n)" |
|
692 |
by (simp add: prod_eq_iff) |
|
693 |
||
694 |
lemma [code]: |
|
695 |
"HOL.equal m n = HOL.equal (of_nat m :: Target_Numeral.int) (of_nat n)" |
|
696 |
by (simp add: equal Target_Numeral.int_eq_iff) |
|
697 |
||
698 |
lemma [code]: |
|
699 |
"m \<le> n \<longleftrightarrow> (of_nat m :: Target_Numeral.int) \<le> of_nat n" |
|
700 |
by (simp add: less_eq_int_def) |
|
701 |
||
702 |
lemma [code]: |
|
703 |
"m < n \<longleftrightarrow> (of_nat m :: Target_Numeral.int) < of_nat n" |
|
704 |
by (simp add: less_int_def) |
|
705 |
||
706 |
lemma num_of_nat_code [code]: |
|
48075
ec5e62b868eb
apply preprocessing simpset also to rhs of abstract code equations
haftmann
parents:
48073
diff
changeset
|
707 |
"num_of_nat = Target_Numeral.num_of_int \<circ> of_nat" |
47108 | 708 |
by (simp add: fun_eq_iff num_of_int_def of_nat_def) |
709 |
||
710 |
lemma (in semiring_1) of_nat_code: |
|
711 |
"of_nat n = (if n = 0 then 0 |
|
712 |
else let |
|
713 |
(m, q) = divmod_nat n 2; |
|
714 |
m' = 2 * of_nat m |
|
715 |
in if q = 0 then m' else m' + 1)" |
|
716 |
proof - |
|
717 |
from mod_div_equality have *: "of_nat n = of_nat (n div 2 * 2 + n mod 2)" by simp |
|
718 |
show ?thesis |
|
719 |
by (simp add: Let_def divmod_nat_div_mod mod_2_not_eq_zero_eq_one_nat |
|
720 |
of_nat_add [symmetric]) |
|
721 |
(simp add: * mult_commute of_nat_mult add_commute) |
|
722 |
qed |
|
723 |
||
724 |
declare of_nat_code [code] |
|
725 |
||
726 |
text {* Conversions between @{typ nat} and @{typ int} *} |
|
727 |
||
728 |
definition int :: "nat \<Rightarrow> int" where |
|
729 |
[code_abbrev]: "int = of_nat" |
|
730 |
||
731 |
hide_const (open) int |
|
732 |
||
733 |
lemma [code]: |
|
734 |
"Target_Numeral.int n = Target_Numeral.int_of (of_nat n)" |
|
735 |
by (simp add: int_def) |
|
736 |
||
737 |
lemma [code abstract]: |
|
738 |
"Target_Numeral.of_nat (nat k) = max 0 (Target_Numeral.of_int k)" |
|
739 |
by (simp add: of_nat_def of_int_of_nat max_def) |
|
740 |
||
741 |
end |
|
47819
d402ac2288b8
rhs of abstract code equations are not subject to preprocessing: inline code abbrevs explicitly
haftmann
parents:
47487
diff
changeset
|
742 |