changeset 38054 | acd48ef85bfc |
parent 37826 | 4c0a5e35931a |
child 38764 | e6a18808873c |
child 38773 | f9837065b5e8 |
38053:9102e859dc0b | 38054:acd48ef85bfc |
---|---|
53 |
53 |
54 lemma num_of_nat_inverse: "0 < n \<Longrightarrow> nat_of_num (num_of_nat n) = n" |
54 lemma num_of_nat_inverse: "0 < n \<Longrightarrow> nat_of_num (num_of_nat n) = n" |
55 by (induct n) (simp_all add: nat_of_num_inc) |
55 by (induct n) (simp_all add: nat_of_num_inc) |
56 |
56 |
57 lemma num_eq_iff: "x = y \<longleftrightarrow> nat_of_num x = nat_of_num y" |
57 lemma num_eq_iff: "x = y \<longleftrightarrow> nat_of_num x = nat_of_num y" |
58 apply safe |
58 proof |
59 apply (drule arg_cong [where f=num_of_nat]) |
59 assume "nat_of_num x = nat_of_num y" |
60 apply (simp add: nat_of_num_inverse) |
60 then have "num_of_nat (nat_of_num x) = num_of_nat (nat_of_num y)" by simp |
61 done |
61 then show "x = y" by (simp add: nat_of_num_inverse) |
62 qed simp |
|
62 |
63 |
63 lemma num_induct [case_names One inc]: |
64 lemma num_induct [case_names One inc]: |
64 fixes P :: "num \<Rightarrow> bool" |
65 fixes P :: "num \<Rightarrow> bool" |
65 assumes One: "P One" |
66 assumes One: "P One" |
66 and inc: "\<And>x. P x \<Longrightarrow> P (inc x)" |
67 and inc: "\<And>x. P x \<Longrightarrow> P (inc x)" |
79 with n show "P x" |
80 with n show "P x" |
80 by (simp add: nat_of_num_inverse) |
81 by (simp add: nat_of_num_inverse) |
81 qed |
82 qed |
82 |
83 |
83 text {* |
84 text {* |
84 From now on, there are two possible models for @{typ num}: |
85 From now on, there are two possible models for @{typ num}: as |
85 as positive naturals (rule @{text "num_induct"}) |
86 positive naturals (rule @{text "num_induct"}) and as digit |
86 and as digit representation (rules @{text "num.induct"}, @{text "num.cases"}). |
87 representation (rules @{text "num.induct"}, @{text "num.cases"}). |
87 |
88 |
88 It is not entirely clear in which context it is better to use |
89 It is not entirely clear in which context it is better to use the |
89 the one or the other, or whether the construction should be reversed. |
90 one or the other, or whether the construction should be reversed. |
90 *} |
91 *} |
91 |
92 |
92 |
93 |
93 subsection {* Numeral operations *} |
94 subsection {* Numeral operations *} |
94 |
95 |
152 "Dig1 n * Dig0 m = Dig0 (n * Dig0 m + m)" |
153 "Dig1 n * Dig0 m = Dig0 (n * Dig0 m + m)" |
153 "Dig1 n * Dig1 m = Dig1 (n * Dig1 m + m)" |
154 "Dig1 n * Dig1 m = Dig1 (n * Dig1 m + m)" |
154 by (simp_all add: num_eq_iff nat_of_num_add nat_of_num_mult |
155 by (simp_all add: num_eq_iff nat_of_num_add nat_of_num_mult |
155 left_distrib right_distrib) |
156 left_distrib right_distrib) |
156 |
157 |
157 lemma Dig_eq: |
|
158 "One = One \<longleftrightarrow> True" |
|
159 "One = Dig0 n \<longleftrightarrow> False" |
|
160 "One = Dig1 n \<longleftrightarrow> False" |
|
161 "Dig0 m = One \<longleftrightarrow> False" |
|
162 "Dig1 m = One \<longleftrightarrow> False" |
|
163 "Dig0 m = Dig0 n \<longleftrightarrow> m = n" |
|
164 "Dig0 m = Dig1 n \<longleftrightarrow> False" |
|
165 "Dig1 m = Dig0 n \<longleftrightarrow> False" |
|
166 "Dig1 m = Dig1 n \<longleftrightarrow> m = n" |
|
167 by simp_all |
|
168 |
|
169 lemma less_eq_num_code [numeral, simp, code]: |
158 lemma less_eq_num_code [numeral, simp, code]: |
170 "One \<le> n \<longleftrightarrow> True" |
159 "One \<le> n \<longleftrightarrow> True" |
171 "Dig0 m \<le> One \<longleftrightarrow> False" |
160 "Dig0 m \<le> One \<longleftrightarrow> False" |
172 "Dig1 m \<le> One \<longleftrightarrow> False" |
161 "Dig1 m \<le> One \<longleftrightarrow> False" |
173 "Dig0 m \<le> Dig0 n \<longleftrightarrow> m \<le> n" |
162 "Dig0 m \<le> Dig0 n \<longleftrightarrow> m \<le> n" |
205 |
194 |
206 text {* A double-and-decrement function *} |
195 text {* A double-and-decrement function *} |
207 |
196 |
208 primrec DigM :: "num \<Rightarrow> num" where |
197 primrec DigM :: "num \<Rightarrow> num" where |
209 "DigM One = One" |
198 "DigM One = One" |
210 | "DigM (Dig0 n) = Dig1 (DigM n)" |
199 | "DigM (Dig0 n) = Dig1 (DigM n)" |
211 | "DigM (Dig1 n) = Dig1 (Dig0 n)" |
200 | "DigM (Dig1 n) = Dig1 (Dig0 n)" |
212 |
201 |
213 lemma DigM_plus_one: "DigM n + One = Dig0 n" |
202 lemma DigM_plus_one: "DigM n + One = Dig0 n" |
214 by (induct n) simp_all |
203 by (induct n) simp_all |
215 |
204 |
216 lemma add_One_commute: "One + n = n + One" |
205 lemma add_One_commute: "One + n = n + One" |
217 by (induct n) simp_all |
206 by (induct n) simp_all |
218 |
207 |
219 lemma one_plus_DigM: "One + DigM n = Dig0 n" |
208 lemma one_plus_DigM: "One + DigM n = Dig0 n" |
220 unfolding add_One_commute DigM_plus_one .. |
209 by (simp add: add_One_commute DigM_plus_one) |
221 |
210 |
222 text {* Squaring and exponentiation *} |
211 text {* Squaring and exponentiation *} |
223 |
212 |
224 primrec square :: "num \<Rightarrow> num" where |
213 primrec square :: "num \<Rightarrow> num" where |
225 "square One = One" |
214 "square One = One" |
226 | "square (Dig0 n) = Dig0 (Dig0 (square n))" |
215 | "square (Dig0 n) = Dig0 (Dig0 (square n))" |
227 | "square (Dig1 n) = Dig1 (Dig0 (square n + n))" |
216 | "square (Dig1 n) = Dig1 (Dig0 (square n + n))" |
228 |
217 |
229 primrec pow :: "num \<Rightarrow> num \<Rightarrow> num" |
218 primrec pow :: "num \<Rightarrow> num \<Rightarrow> num" where |
230 where |
|
231 "pow x One = x" |
219 "pow x One = x" |
232 | "pow x (Dig0 y) = square (pow x y)" |
220 | "pow x (Dig0 y) = square (pow x y)" |
233 | "pow x (Dig1 y) = x * square (pow x y)" |
221 | "pow x (Dig1 y) = x * square (pow x y)" |
234 |
222 |
235 |
223 |
243 class semiring_numeral = semiring + monoid_mult |
231 class semiring_numeral = semiring + monoid_mult |
244 begin |
232 begin |
245 |
233 |
246 primrec of_num :: "num \<Rightarrow> 'a" where |
234 primrec of_num :: "num \<Rightarrow> 'a" where |
247 of_num_One [numeral]: "of_num One = 1" |
235 of_num_One [numeral]: "of_num One = 1" |
248 | "of_num (Dig0 n) = of_num n + of_num n" |
236 | "of_num (Dig0 n) = of_num n + of_num n" |
249 | "of_num (Dig1 n) = of_num n + of_num n + 1" |
237 | "of_num (Dig1 n) = of_num n + of_num n + 1" |
250 |
238 |
251 lemma of_num_inc: "of_num (inc x) = of_num x + 1" |
239 lemma of_num_inc: "of_num (inc n) = of_num n + 1" |
252 by (induct x) (simp_all add: add_ac) |
240 by (induct n) (simp_all add: add_ac) |
253 |
241 |
254 lemma of_num_add: "of_num (m + n) = of_num m + of_num n" |
242 lemma of_num_add: "of_num (m + n) = of_num m + of_num n" |
255 apply (induct n rule: num_induct) |
243 by (induct n rule: num_induct) (simp_all add: add_One add_inc of_num_inc add_ac) |
256 apply (simp_all add: add_One add_inc of_num_inc add_ac) |
|
257 done |
|
258 |
244 |
259 lemma of_num_mult: "of_num (m * n) = of_num m * of_num n" |
245 lemma of_num_mult: "of_num (m * n) = of_num m * of_num n" |
260 apply (induct n rule: num_induct) |
246 by (induct n rule: num_induct) (simp_all add: mult_One mult_inc of_num_add of_num_inc right_distrib) |
261 apply (simp add: mult_One) |
|
262 apply (simp add: mult_inc of_num_add of_num_inc right_distrib) |
|
263 done |
|
264 |
247 |
265 declare of_num.simps [simp del] |
248 declare of_num.simps [simp del] |
266 |
249 |
267 end |
250 end |
268 |
|
269 text {* |
|
270 ML stuff and syntax. |
|
271 *} |
|
272 |
251 |
273 ML {* |
252 ML {* |
274 fun mk_num k = |
253 fun mk_num k = |
275 if k > 1 then |
254 if k > 1 then |
276 let |
255 let |
283 fun dest_num @{term One} = 1 |
262 fun dest_num @{term One} = 1 |
284 | dest_num (@{term Dig0} $ n) = 2 * dest_num n |
263 | dest_num (@{term Dig0} $ n) = 2 * dest_num n |
285 | dest_num (@{term Dig1} $ n) = 2 * dest_num n + 1 |
264 | dest_num (@{term Dig1} $ n) = 2 * dest_num n + 1 |
286 | dest_num t = raise TERM ("dest_num", [t]); |
265 | dest_num t = raise TERM ("dest_num", [t]); |
287 |
266 |
288 (*FIXME these have to gain proper context via morphisms phi*) |
267 fun mk_numeral phi T k = Morphism.term phi (Const (@{const_name of_num}, @{typ num} --> T)) |
289 |
|
290 fun mk_numeral T k = Const (@{const_name of_num}, @{typ num} --> T) |
|
291 $ mk_num k |
268 $ mk_num k |
292 |
269 |
293 fun dest_numeral (Const (@{const_name of_num}, Type ("fun", [@{typ num}, T])) $ t) = |
270 fun dest_numeral phi (u $ t) = |
294 (T, dest_num t) |
271 if Term.aconv_untyped (u, Morphism.term phi (Const (@{const_name of_num}, dummyT))) |
272 then (range_type (fastype_of u), dest_num t) |
|
273 else raise TERM ("dest_numeral", [u, t]); |
|
295 *} |
274 *} |
296 |
275 |
297 syntax |
276 syntax |
298 "_Numerals" :: "xnum \<Rightarrow> 'a" ("_") |
277 "_Numerals" :: "xnum \<Rightarrow> 'a" ("_") |
299 |
278 |
333 | T' => if T' = dummyT then t' else raise Match |
312 | T' => if T' = dummyT then t' else raise Match |
334 end; |
313 end; |
335 in [(@{const_syntax of_num}, num_tr')] end |
314 in [(@{const_syntax of_num}, num_tr')] end |
336 *} |
315 *} |
337 |
316 |
317 |
|
338 subsection {* Class-specific numeral rules *} |
318 subsection {* Class-specific numeral rules *} |
339 |
|
340 text {* |
|
341 @{const of_num} is a morphism. |
|
342 *} |
|
343 |
319 |
344 subsubsection {* Class @{text semiring_numeral} *} |
320 subsubsection {* Class @{text semiring_numeral} *} |
345 |
321 |
346 context semiring_numeral |
322 context semiring_numeral |
347 begin |
323 begin |
348 |
324 |
349 abbreviation "Num1 \<equiv> of_num One" |
325 abbreviation "Num1 \<equiv> of_num One" |
350 |
326 |
351 text {* |
327 text {* |
352 Alas, there is still the duplication of @{term 1}, |
328 Alas, there is still the duplication of @{term 1}, although the |
353 thought the duplicated @{term 0} has disappeared. |
329 duplicated @{term 0} has disappeared. We could get rid of it by |
354 We could get rid of it by replacing the constructor |
330 replacing the constructor @{term 1} in @{typ num} by two |
355 @{term 1} in @{typ num} by two constructors |
331 constructors @{text two} and @{text three}, resulting in a further |
356 @{text two} and @{text three}, resulting in a further |
|
357 blow-up. But it could be worth the effort. |
332 blow-up. But it could be worth the effort. |
358 *} |
333 *} |
359 |
334 |
360 lemma of_num_plus_one [numeral]: |
335 lemma of_num_plus_one [numeral]: |
361 "of_num n + 1 = of_num (n + One)" |
336 "of_num n + 1 = of_num (n + One)" |
365 "1 + of_num n = of_num (One + n)" |
340 "1 + of_num n = of_num (One + n)" |
366 by (simp only: of_num_add of_num_One) |
341 by (simp only: of_num_add of_num_One) |
367 |
342 |
368 lemma of_num_plus [numeral]: |
343 lemma of_num_plus [numeral]: |
369 "of_num m + of_num n = of_num (m + n)" |
344 "of_num m + of_num n = of_num (m + n)" |
370 unfolding of_num_add .. |
345 by (simp only: of_num_add) |
371 |
346 |
372 lemma of_num_times_one [numeral]: |
347 lemma of_num_times_one [numeral]: |
373 "of_num n * 1 = of_num n" |
348 "of_num n * 1 = of_num n" |
374 by simp |
349 by simp |
375 |
350 |
381 "of_num m * of_num n = of_num (m * n)" |
356 "of_num m * of_num n = of_num (m * n)" |
382 unfolding of_num_mult .. |
357 unfolding of_num_mult .. |
383 |
358 |
384 end |
359 end |
385 |
360 |
386 subsubsection {* |
361 |
387 Structures with a zero: class @{text semiring_1} |
362 subsubsection {* Structures with a zero: class @{text semiring_1} *} |
388 *} |
|
389 |
363 |
390 context semiring_1 |
364 context semiring_1 |
391 begin |
365 begin |
392 |
366 |
393 subclass semiring_numeral .. |
367 subclass semiring_numeral .. |
420 have "of_num n = nat_of_num n" |
394 have "of_num n = nat_of_num n" |
421 by (induct n) (simp_all add: of_num.simps) |
395 by (induct n) (simp_all add: of_num.simps) |
422 then show "nat_of_num n = of_num n" by simp |
396 then show "nat_of_num n = of_num n" by simp |
423 qed |
397 qed |
424 |
398 |
425 subsubsection {* |
399 |
426 Equality: class @{text semiring_char_0} |
400 subsubsection {* Equality: class @{text semiring_char_0} *} |
427 *} |
|
428 |
401 |
429 context semiring_char_0 |
402 context semiring_char_0 |
430 begin |
403 begin |
431 |
404 |
432 lemma of_num_eq_iff [numeral]: "of_num m = of_num n \<longleftrightarrow> m = n" |
405 lemma of_num_eq_iff [numeral]: "of_num m = of_num n \<longleftrightarrow> m = n" |
439 lemma one_eq_of_num_iff [numeral]: "1 = of_num n \<longleftrightarrow> One = n" |
412 lemma one_eq_of_num_iff [numeral]: "1 = of_num n \<longleftrightarrow> One = n" |
440 using of_num_eq_iff [of One n] by (simp add: of_num_One) |
413 using of_num_eq_iff [of One n] by (simp add: of_num_One) |
441 |
414 |
442 end |
415 end |
443 |
416 |
444 subsubsection {* |
417 |
445 Comparisons: class @{text linordered_semidom} |
418 subsubsection {* Comparisons: class @{text linordered_semidom} *} |
446 *} |
419 |
447 |
420 text {* |
448 text {* Could be perhaps more general than here. *} |
421 Perhaps the underlying structure could even |
422 be more general than @{text linordered_semidom}. |
|
423 *} |
|
449 |
424 |
450 context linordered_semidom |
425 context linordered_semidom |
451 begin |
426 begin |
452 |
427 |
453 lemma of_num_pos [numeral]: "0 < of_num n" |
428 lemma of_num_pos [numeral]: "0 < of_num n" |
454 by (induct n) (simp_all add: of_num.simps add_pos_pos) |
429 by (induct n) (simp_all add: of_num.simps add_pos_pos) |
430 |
|
431 lemma of_num_not_zero [numeral]: "of_num n \<noteq> 0" |
|
432 using of_num_pos [of n] by simp |
|
455 |
433 |
456 lemma of_num_less_eq_iff [numeral]: "of_num m \<le> of_num n \<longleftrightarrow> m \<le> n" |
434 lemma of_num_less_eq_iff [numeral]: "of_num m \<le> of_num n \<longleftrightarrow> m \<le> n" |
457 proof - |
435 proof - |
458 have "of_nat (of_num m) \<le> of_nat (of_num n) \<longleftrightarrow> m \<le> n" |
436 have "of_nat (of_num m) \<le> of_nat (of_num n) \<longleftrightarrow> m \<le> n" |
459 unfolding less_eq_num_def nat_of_num_of_num of_nat_le_iff .. |
437 unfolding less_eq_num_def nat_of_num_of_num of_nat_le_iff .. |
497 proof - |
475 proof - |
498 have "- of_num m < 0" by (simp add: of_num_pos) |
476 have "- of_num m < 0" by (simp add: of_num_pos) |
499 also have "0 < of_num n" by (simp add: of_num_pos) |
477 also have "0 < of_num n" by (simp add: of_num_pos) |
500 finally show ?thesis . |
478 finally show ?thesis . |
501 qed |
479 qed |
480 |
|
481 lemma minus_of_num_not_equal_of_num: "- of_num m \<noteq> of_num n" |
|
482 using minus_of_num_less_of_num_iff [of m n] by simp |
|
502 |
483 |
503 lemma minus_of_num_less_one_iff: "- of_num n < 1" |
484 lemma minus_of_num_less_one_iff: "- of_num n < 1" |
504 using minus_of_num_less_of_num_iff [of n One] by (simp add: of_num_One) |
485 using minus_of_num_less_of_num_iff [of n One] by (simp add: of_num_One) |
505 |
486 |
506 lemma minus_one_less_of_num_iff: "- 1 < of_num n" |
487 lemma minus_one_less_of_num_iff: "- 1 < of_num n" |
555 of_num_le_minus_one_iff |
536 of_num_le_minus_one_iff |
556 one_le_minus_one_iff |
537 one_le_minus_one_iff |
557 |
538 |
558 lemmas less_signed_numeral_special [numeral] = |
539 lemmas less_signed_numeral_special [numeral] = |
559 minus_of_num_less_of_num_iff |
540 minus_of_num_less_of_num_iff |
541 minus_of_num_not_equal_of_num |
|
560 minus_of_num_less_one_iff |
542 minus_of_num_less_one_iff |
561 minus_one_less_of_num_iff |
543 minus_one_less_of_num_iff |
562 minus_one_less_one_iff |
544 minus_one_less_one_iff |
563 of_num_less_minus_of_num_iff |
545 of_num_less_minus_of_num_iff |
564 one_less_minus_of_num_iff |
546 one_less_minus_of_num_iff |
565 of_num_less_minus_one_iff |
547 of_num_less_minus_one_iff |
566 one_less_minus_one_iff |
548 one_less_minus_one_iff |
567 |
549 |
568 end |
550 end |
569 |
551 |
570 subsubsection {* |
552 subsubsection {* Structures with subtraction: class @{text semiring_1_minus} *} |
571 Structures with subtraction: class @{text semiring_1_minus} |
|
572 *} |
|
573 |
553 |
574 class semiring_minus = semiring + minus + zero + |
554 class semiring_minus = semiring + minus + zero + |
575 assumes minus_inverts_plus1: "a + b = c \<Longrightarrow> c - b = a" |
555 assumes minus_inverts_plus1: "a + b = c \<Longrightarrow> c - b = a" |
576 assumes minus_minus_zero_inverts_plus1: "a + b = c \<Longrightarrow> b - c = 0 - a" |
556 assumes minus_minus_zero_inverts_plus1: "a + b = c \<Longrightarrow> b - c = 0 - a" |
577 begin |
557 begin |
610 fun cdest_of_num ct = (snd o split_last o snd o Drule.strip_comb) ct; |
590 fun cdest_of_num ct = (snd o split_last o snd o Drule.strip_comb) ct; |
611 fun cdest_minus ct = case (rev o snd o Drule.strip_comb) ct of [n, m] => (m, n); |
591 fun cdest_minus ct = case (rev o snd o Drule.strip_comb) ct of [n, m] => (m, n); |
612 fun attach_num ct = (dest_num (Thm.term_of ct), ct); |
592 fun attach_num ct = (dest_num (Thm.term_of ct), ct); |
613 fun cdifference t = (pairself (attach_num o cdest_of_num) o cdest_minus) t; |
593 fun cdifference t = (pairself (attach_num o cdest_of_num) o cdest_minus) t; |
614 val simplify = MetaSimplifier.rewrite false (map mk_meta_eq @{thms Dig_plus_eval}); |
594 val simplify = MetaSimplifier.rewrite false (map mk_meta_eq @{thms Dig_plus_eval}); |
615 fun cert ck cl cj = @{thm eqTrueE} OF [@{thm meta_eq_to_obj_eq} OF [simplify (Drule.list_comb (@{cterm "op = :: num \<Rightarrow> _"}, |
595 fun cert ck cl cj = @{thm eqTrueE} OF [@{thm meta_eq_to_obj_eq} |
616 [Drule.list_comb (@{cterm "op + :: num \<Rightarrow> _"}, [ck, cl]), cj]))]]; |
596 OF [simplify (Drule.list_comb (@{cterm "op = :: num \<Rightarrow> _"}, |
597 [Drule.list_comb (@{cterm "op + :: num \<Rightarrow> _"}, [ck, cl]), cj]))]]; |
|
617 in fn phi => fn _ => fn ct => case try cdifference ct |
598 in fn phi => fn _ => fn ct => case try cdifference ct |
618 of NONE => (NONE) |
599 of NONE => (NONE) |
619 | SOME ((k, ck), (l, cl)) => SOME (let val j = k - l in if j = 0 |
600 | SOME ((k, ck), (l, cl)) => SOME (let val j = k - l in if j = 0 |
620 then MetaSimplifier.rewrite false [mk_meta_eq (Morphism.thm phi @{thm Dig_of_num_zero})] ct |
601 then MetaSimplifier.rewrite false [mk_meta_eq (Morphism.thm phi @{thm Dig_of_num_zero})] ct |
621 else mk_meta_eq (let |
602 else mk_meta_eq (let |
649 "1 - of_num (Dig1 n) = 0 - of_num (Dig0 n)" |
630 "1 - of_num (Dig1 n) = 0 - of_num (Dig0 n)" |
650 by (auto intro: minus_minus_zero_inverts_plus1 simp add: DigM_plus_one of_num.simps of_num_plus_one) |
631 by (auto intro: minus_minus_zero_inverts_plus1 simp add: DigM_plus_one of_num.simps of_num_plus_one) |
651 |
632 |
652 end |
633 end |
653 |
634 |
654 subsubsection {* |
635 |
655 Structures with negation: class @{text ring_1} |
636 subsubsection {* Structures with negation: class @{text ring_1} *} |
656 *} |
|
657 |
637 |
658 context ring_1 |
638 context ring_1 |
659 begin |
639 begin |
660 |
640 |
661 subclass semiring_1_minus |
641 subclass semiring_1_minus proof |
662 proof qed (simp_all add: algebra_simps) |
642 qed (simp_all add: algebra_simps) |
663 |
643 |
664 lemma Dig_zero_minus_of_num [numeral]: |
644 lemma Dig_zero_minus_of_num [numeral]: |
665 "0 - of_num n = - of_num n" |
645 "0 - of_num n = - of_num n" |
666 by simp |
646 by simp |
667 |
647 |
694 |
674 |
695 declare of_int_1 [numeral] |
675 declare of_int_1 [numeral] |
696 |
676 |
697 end |
677 end |
698 |
678 |
699 subsubsection {* |
679 |
700 Structures with exponentiation |
680 subsubsection {* Structures with exponentiation *} |
701 *} |
|
702 |
681 |
703 lemma of_num_square: "of_num (square x) = of_num x * of_num x" |
682 lemma of_num_square: "of_num (square x) = of_num x * of_num x" |
704 by (induct x) |
683 by (induct x) |
705 (simp_all add: of_num.simps of_num_add algebra_simps) |
684 (simp_all add: of_num.simps of_num_add algebra_simps) |
706 |
685 |
727 by (induct n rule: num_induct) (simp_all add: of_num.simps of_num_inc) |
706 by (induct n rule: num_induct) (simp_all add: of_num.simps of_num_inc) |
728 |
707 |
729 declare power_one [numeral] |
708 declare power_one [numeral] |
730 |
709 |
731 |
710 |
732 subsubsection {* |
711 subsubsection {* Greetings to @{typ nat}. *} |
733 Greetings to @{typ nat}. |
712 |
734 *} |
713 instance nat :: semiring_1_minus proof |
735 |
714 qed simp_all |
736 instance nat :: semiring_1_minus proof qed simp_all |
|
737 |
715 |
738 lemma Suc_of_num [numeral]: "Suc (of_num n) = of_num (n + One)" |
716 lemma Suc_of_num [numeral]: "Suc (of_num n) = of_num (n + One)" |
739 unfolding of_num_plus_one [symmetric] by simp |
717 unfolding of_num_plus_one [symmetric] by simp |
740 |
718 |
741 lemma nat_number: |
719 lemma nat_number: |
746 by (simp_all add: of_num.simps DigM_plus_one Suc_of_num) |
724 by (simp_all add: of_num.simps DigM_plus_one Suc_of_num) |
747 |
725 |
748 declare diff_0_eq_0 [numeral] |
726 declare diff_0_eq_0 [numeral] |
749 |
727 |
750 |
728 |
729 subsection {* Proof tools setup *} |
|
730 |
|
731 subsubsection {* Numeral equations as default simplification rules *} |
|
732 |
|
733 declare (in semiring_numeral) of_num_One [simp] |
|
734 declare (in semiring_numeral) of_num_plus_one [simp] |
|
735 declare (in semiring_numeral) of_num_one_plus [simp] |
|
736 declare (in semiring_numeral) of_num_plus [simp] |
|
737 declare (in semiring_numeral) of_num_times [simp] |
|
738 |
|
739 declare (in semiring_1) of_nat_of_num [simp] |
|
740 |
|
741 declare (in semiring_char_0) of_num_eq_iff [simp] |
|
742 declare (in semiring_char_0) of_num_eq_one_iff [simp] |
|
743 declare (in semiring_char_0) one_eq_of_num_iff [simp] |
|
744 |
|
745 declare (in linordered_semidom) of_num_pos [simp] |
|
746 declare (in linordered_semidom) of_num_not_zero [simp] |
|
747 declare (in linordered_semidom) of_num_less_eq_iff [simp] |
|
748 declare (in linordered_semidom) of_num_less_eq_one_iff [simp] |
|
749 declare (in linordered_semidom) one_less_eq_of_num_iff [simp] |
|
750 declare (in linordered_semidom) of_num_less_iff [simp] |
|
751 declare (in linordered_semidom) of_num_less_one_iff [simp] |
|
752 declare (in linordered_semidom) one_less_of_num_iff [simp] |
|
753 declare (in linordered_semidom) of_num_nonneg [simp] |
|
754 declare (in linordered_semidom) of_num_less_zero_iff [simp] |
|
755 declare (in linordered_semidom) of_num_le_zero_iff [simp] |
|
756 |
|
757 declare (in linordered_idom) le_signed_numeral_special [simp] |
|
758 declare (in linordered_idom) less_signed_numeral_special [simp] |
|
759 |
|
760 declare (in semiring_1_minus) Dig_of_num_minus_one [simp] |
|
761 declare (in semiring_1_minus) Dig_one_minus_of_num [simp] |
|
762 |
|
763 declare (in ring_1) Dig_plus_uminus [simp] |
|
764 declare (in ring_1) of_int_of_num [simp] |
|
765 |
|
766 declare power_of_num [simp] |
|
767 declare power_zero_of_num [simp] |
|
768 declare power_minus_Dig0 [simp] |
|
769 declare power_minus_Dig1 [simp] |
|
770 |
|
771 declare Suc_of_num [simp] |
|
772 |
|
773 |
|
774 subsubsection {* Reorientation of equalities *} |
|
775 |
|
776 setup {* |
|
777 Reorient_Proc.add |
|
778 (fn Const(@{const_name of_num}, _) $ _ => true |
|
779 | Const(@{const_name uminus}, _) $ |
|
780 (Const(@{const_name of_num}, _) $ _) => true |
|
781 | _ => false) |
|
782 *} |
|
783 |
|
784 simproc_setup reorient_num ("of_num n = x" | "- of_num m = y") = Reorient_Proc.proc |
|
785 |
|
786 |
|
787 subsubsection {* Constant folding for multiplication in semirings *} |
|
788 |
|
789 context semiring_numeral |
|
790 begin |
|
791 |
|
792 lemma mult_of_num_commute: "x * of_num n = of_num n * x" |
|
793 by (induct n) |
|
794 (simp_all only: of_num.simps left_distrib right_distrib mult_1_left mult_1_right) |
|
795 |
|
796 definition |
|
797 "commutes_with a b \<longleftrightarrow> a * b = b * a" |
|
798 |
|
799 lemma commutes_with_commute: "commutes_with a b \<Longrightarrow> a * b = b * a" |
|
800 unfolding commutes_with_def . |
|
801 |
|
802 lemma commutes_with_left_commute: "commutes_with a b \<Longrightarrow> a * (b * c) = b * (a * c)" |
|
803 unfolding commutes_with_def by (simp only: mult_assoc [symmetric]) |
|
804 |
|
805 lemma commutes_with_numeral: "commutes_with x (of_num n)" "commutes_with (of_num n) x" |
|
806 unfolding commutes_with_def by (simp_all add: mult_of_num_commute) |
|
807 |
|
808 lemmas mult_ac_numeral = |
|
809 mult_assoc |
|
810 commutes_with_commute |
|
811 commutes_with_left_commute |
|
812 commutes_with_numeral |
|
813 |
|
814 end |
|
815 |
|
816 ML {* |
|
817 structure Semiring_Times_Assoc_Data : ASSOC_FOLD_DATA = |
|
818 struct |
|
819 val assoc_ss = HOL_ss addsimps @{thms mult_ac_numeral} |
|
820 val eq_reflection = eq_reflection |
|
821 fun is_numeral (Const(@{const_name of_num}, _) $ _) = true |
|
822 | is_numeral _ = false; |
|
823 end; |
|
824 |
|
825 structure Semiring_Times_Assoc = Assoc_Fold (Semiring_Times_Assoc_Data); |
|
826 *} |
|
827 |
|
828 simproc_setup semiring_assoc_fold' ("(a::'a::semiring_numeral) * b") = |
|
829 {* fn phi => fn ss => fn ct => |
|
830 Semiring_Times_Assoc.proc ss (Thm.term_of ct) *} |
|
831 |
|
832 |
|
751 subsection {* Code generator setup for @{typ int} *} |
833 subsection {* Code generator setup for @{typ int} *} |
752 |
834 |
753 definition Pls :: "num \<Rightarrow> int" where |
835 text {* Reversing standard setup *} |
754 [simp, code_post]: "Pls n = of_num n" |
836 |
755 |
837 lemma [code_unfold del]: "(0::int) \<equiv> Numeral0" by simp |
756 definition Mns :: "num \<Rightarrow> int" where |
838 lemma [code_unfold del]: "(1::int) \<equiv> Numeral1" by simp |
757 [simp, code_post]: "Mns n = - of_num n" |
839 declare zero_is_num_zero [code_unfold del] |
758 |
840 declare one_is_num_one [code_unfold del] |
759 code_datatype "0::int" Pls Mns |
|
760 |
|
761 lemmas [code_unfold] = Pls_def [symmetric] Mns_def [symmetric] |
|
762 |
|
763 definition sub :: "num \<Rightarrow> num \<Rightarrow> int" where |
|
764 [simp]: "sub m n = (of_num m - of_num n)" |
|
765 |
|
766 definition dup :: "int \<Rightarrow> int" where |
|
767 "dup k = 2 * k" |
|
768 |
|
769 lemma Dig_sub [code]: |
|
770 "sub One One = 0" |
|
771 "sub (Dig0 m) One = of_num (DigM m)" |
|
772 "sub (Dig1 m) One = of_num (Dig0 m)" |
|
773 "sub One (Dig0 n) = - of_num (DigM n)" |
|
774 "sub One (Dig1 n) = - of_num (Dig0 n)" |
|
775 "sub (Dig0 m) (Dig0 n) = dup (sub m n)" |
|
776 "sub (Dig1 m) (Dig1 n) = dup (sub m n)" |
|
777 "sub (Dig1 m) (Dig0 n) = dup (sub m n) + 1" |
|
778 "sub (Dig0 m) (Dig1 n) = dup (sub m n) - 1" |
|
779 apply (simp_all add: dup_def algebra_simps) |
|
780 apply (simp_all add: of_num_plus one_plus_DigM)[4] |
|
781 apply (simp_all add: of_num.simps) |
|
782 done |
|
783 |
|
784 lemma dup_code [code]: |
|
785 "dup 0 = 0" |
|
786 "dup (Pls n) = Pls (Dig0 n)" |
|
787 "dup (Mns n) = Mns (Dig0 n)" |
|
788 by (simp_all add: dup_def of_num.simps) |
|
789 |
841 |
790 lemma [code, code del]: |
842 lemma [code, code del]: |
791 "(1 :: int) = 1" |
843 "(1 :: int) = 1" |
792 "(op + :: int \<Rightarrow> int \<Rightarrow> int) = op +" |
844 "(op + :: int \<Rightarrow> int \<Rightarrow> int) = op +" |
793 "(uminus :: int \<Rightarrow> int) = uminus" |
845 "(uminus :: int \<Rightarrow> int) = uminus" |
796 "(eq_class.eq :: int \<Rightarrow> int \<Rightarrow> bool) = eq_class.eq" |
848 "(eq_class.eq :: int \<Rightarrow> int \<Rightarrow> bool) = eq_class.eq" |
797 "(op \<le> :: int \<Rightarrow> int \<Rightarrow> bool) = op \<le>" |
849 "(op \<le> :: int \<Rightarrow> int \<Rightarrow> bool) = op \<le>" |
798 "(op < :: int \<Rightarrow> int \<Rightarrow> bool) = op <" |
850 "(op < :: int \<Rightarrow> int \<Rightarrow> bool) = op <" |
799 by rule+ |
851 by rule+ |
800 |
852 |
853 text {* Constructors *} |
|
854 |
|
855 definition Pls :: "num \<Rightarrow> int" where |
|
856 [simp, code_post]: "Pls n = of_num n" |
|
857 |
|
858 definition Mns :: "num \<Rightarrow> int" where |
|
859 [simp, code_post]: "Mns n = - of_num n" |
|
860 |
|
861 code_datatype "0::int" Pls Mns |
|
862 |
|
863 lemmas [code_unfold] = Pls_def [symmetric] Mns_def [symmetric] |
|
864 |
|
865 text {* Auxiliary operations *} |
|
866 |
|
867 definition dup :: "int \<Rightarrow> int" where |
|
868 [simp]: "dup k = k + k" |
|
869 |
|
870 lemma Dig_dup [code]: |
|
871 "dup 0 = 0" |
|
872 "dup (Pls n) = Pls (Dig0 n)" |
|
873 "dup (Mns n) = Mns (Dig0 n)" |
|
874 by (simp_all add: of_num.simps) |
|
875 |
|
876 definition sub :: "num \<Rightarrow> num \<Rightarrow> int" where |
|
877 [simp]: "sub m n = (of_num m - of_num n)" |
|
878 |
|
879 lemma Dig_sub [code]: |
|
880 "sub One One = 0" |
|
881 "sub (Dig0 m) One = of_num (DigM m)" |
|
882 "sub (Dig1 m) One = of_num (Dig0 m)" |
|
883 "sub One (Dig0 n) = - of_num (DigM n)" |
|
884 "sub One (Dig1 n) = - of_num (Dig0 n)" |
|
885 "sub (Dig0 m) (Dig0 n) = dup (sub m n)" |
|
886 "sub (Dig1 m) (Dig1 n) = dup (sub m n)" |
|
887 "sub (Dig1 m) (Dig0 n) = dup (sub m n) + 1" |
|
888 "sub (Dig0 m) (Dig1 n) = dup (sub m n) - 1" |
|
889 by (simp_all add: algebra_simps num_eq_iff nat_of_num_add) |
|
890 |
|
891 text {* Implementations *} |
|
892 |
|
801 lemma one_int_code [code]: |
893 lemma one_int_code [code]: |
802 "1 = Pls One" |
894 "1 = Pls One" |
803 by (simp add: of_num_One) |
895 by (simp add: of_num_One) |
804 |
896 |
805 lemma plus_int_code [code]: |
897 lemma plus_int_code [code]: |
806 "k + 0 = (k::int)" |
898 "k + 0 = (k::int)" |
807 "0 + l = (l::int)" |
899 "0 + l = (l::int)" |
808 "Pls m + Pls n = Pls (m + n)" |
900 "Pls m + Pls n = Pls (m + n)" |
809 "Pls m - Pls n = sub m n" |
901 "Pls m + Mns n = sub m n" |
902 "Mns m + Pls n = sub n m" |
|
810 "Mns m + Mns n = Mns (m + n)" |
903 "Mns m + Mns n = Mns (m + n)" |
811 "Mns m - Mns n = sub n m" |
904 by simp_all |
812 by (simp_all add: of_num_add) |
|
813 |
905 |
814 lemma uminus_int_code [code]: |
906 lemma uminus_int_code [code]: |
815 "uminus 0 = (0::int)" |
907 "uminus 0 = (0::int)" |
816 "uminus (Pls m) = Mns m" |
908 "uminus (Pls m) = Mns m" |
817 "uminus (Mns m) = Pls m" |
909 "uminus (Mns m) = Pls m" |
822 "0 - l = uminus (l::int)" |
914 "0 - l = uminus (l::int)" |
823 "Pls m - Pls n = sub m n" |
915 "Pls m - Pls n = sub m n" |
824 "Pls m - Mns n = Pls (m + n)" |
916 "Pls m - Mns n = Pls (m + n)" |
825 "Mns m - Pls n = Mns (m + n)" |
917 "Mns m - Pls n = Mns (m + n)" |
826 "Mns m - Mns n = sub n m" |
918 "Mns m - Mns n = sub n m" |
827 by (simp_all add: of_num_add) |
919 by simp_all |
828 |
920 |
829 lemma times_int_code [code]: |
921 lemma times_int_code [code]: |
830 "k * 0 = (0::int)" |
922 "k * 0 = (0::int)" |
831 "0 * l = (0::int)" |
923 "0 * l = (0::int)" |
832 "Pls m * Pls n = Pls (m * n)" |
924 "Pls m * Pls n = Pls (m * n)" |
833 "Pls m * Mns n = Mns (m * n)" |
925 "Pls m * Mns n = Mns (m * n)" |
834 "Mns m * Pls n = Mns (m * n)" |
926 "Mns m * Pls n = Mns (m * n)" |
835 "Mns m * Mns n = Pls (m * n)" |
927 "Mns m * Mns n = Pls (m * n)" |
836 by (simp_all add: of_num_mult) |
928 by simp_all |
837 |
929 |
838 lemma eq_int_code [code]: |
930 lemma eq_int_code [code]: |
839 "eq_class.eq 0 (0::int) \<longleftrightarrow> True" |
931 "eq_class.eq 0 (0::int) \<longleftrightarrow> True" |
840 "eq_class.eq 0 (Pls l) \<longleftrightarrow> False" |
932 "eq_class.eq 0 (Pls l) \<longleftrightarrow> False" |
841 "eq_class.eq 0 (Mns l) \<longleftrightarrow> False" |
933 "eq_class.eq 0 (Mns l) \<longleftrightarrow> False" |
843 "eq_class.eq (Pls k) (Pls l) \<longleftrightarrow> eq_class.eq k l" |
935 "eq_class.eq (Pls k) (Pls l) \<longleftrightarrow> eq_class.eq k l" |
844 "eq_class.eq (Pls k) (Mns l) \<longleftrightarrow> False" |
936 "eq_class.eq (Pls k) (Mns l) \<longleftrightarrow> False" |
845 "eq_class.eq (Mns k) 0 \<longleftrightarrow> False" |
937 "eq_class.eq (Mns k) 0 \<longleftrightarrow> False" |
846 "eq_class.eq (Mns k) (Pls l) \<longleftrightarrow> False" |
938 "eq_class.eq (Mns k) (Pls l) \<longleftrightarrow> False" |
847 "eq_class.eq (Mns k) (Mns l) \<longleftrightarrow> eq_class.eq k l" |
939 "eq_class.eq (Mns k) (Mns l) \<longleftrightarrow> eq_class.eq k l" |
848 using of_num_pos [of l, where ?'a = int] of_num_pos [of k, where ?'a = int] |
940 by (auto simp add: eq dest: sym) |
849 by (simp_all add: of_num_eq_iff eq) |
|
850 |
941 |
851 lemma less_eq_int_code [code]: |
942 lemma less_eq_int_code [code]: |
852 "0 \<le> (0::int) \<longleftrightarrow> True" |
943 "0 \<le> (0::int) \<longleftrightarrow> True" |
853 "0 \<le> Pls l \<longleftrightarrow> True" |
944 "0 \<le> Pls l \<longleftrightarrow> True" |
854 "0 \<le> Mns l \<longleftrightarrow> False" |
945 "0 \<le> Mns l \<longleftrightarrow> False" |
856 "Pls k \<le> Pls l \<longleftrightarrow> k \<le> l" |
947 "Pls k \<le> Pls l \<longleftrightarrow> k \<le> l" |
857 "Pls k \<le> Mns l \<longleftrightarrow> False" |
948 "Pls k \<le> Mns l \<longleftrightarrow> False" |
858 "Mns k \<le> 0 \<longleftrightarrow> True" |
949 "Mns k \<le> 0 \<longleftrightarrow> True" |
859 "Mns k \<le> Pls l \<longleftrightarrow> True" |
950 "Mns k \<le> Pls l \<longleftrightarrow> True" |
860 "Mns k \<le> Mns l \<longleftrightarrow> l \<le> k" |
951 "Mns k \<le> Mns l \<longleftrightarrow> l \<le> k" |
861 using of_num_pos [of l, where ?'a = int] of_num_pos [of k, where ?'a = int] |
952 by simp_all |
862 by (simp_all add: of_num_less_eq_iff) |
|
863 |
953 |
864 lemma less_int_code [code]: |
954 lemma less_int_code [code]: |
865 "0 < (0::int) \<longleftrightarrow> False" |
955 "0 < (0::int) \<longleftrightarrow> False" |
866 "0 < Pls l \<longleftrightarrow> True" |
956 "0 < Pls l \<longleftrightarrow> True" |
867 "0 < Mns l \<longleftrightarrow> False" |
957 "0 < Mns l \<longleftrightarrow> False" |
869 "Pls k < Pls l \<longleftrightarrow> k < l" |
959 "Pls k < Pls l \<longleftrightarrow> k < l" |
870 "Pls k < Mns l \<longleftrightarrow> False" |
960 "Pls k < Mns l \<longleftrightarrow> False" |
871 "Mns k < 0 \<longleftrightarrow> True" |
961 "Mns k < 0 \<longleftrightarrow> True" |
872 "Mns k < Pls l \<longleftrightarrow> True" |
962 "Mns k < Pls l \<longleftrightarrow> True" |
873 "Mns k < Mns l \<longleftrightarrow> l < k" |
963 "Mns k < Mns l \<longleftrightarrow> l < k" |
874 using of_num_pos [of l, where ?'a = int] of_num_pos [of k, where ?'a = int] |
964 by simp_all |
875 by (simp_all add: of_num_less_iff) |
|
876 |
|
877 lemma [code_unfold del]: "(0::int) \<equiv> Numeral0" by simp |
|
878 lemma [code_unfold del]: "(1::int) \<equiv> Numeral1" by simp |
|
879 declare zero_is_num_zero [code_unfold del] |
|
880 declare one_is_num_one [code_unfold del] |
|
881 |
965 |
882 hide_const (open) sub dup |
966 hide_const (open) sub dup |
883 |
967 |
884 |
968 text {* Pretty literals *} |
885 subsection {* Numeral equations as default simplification rules *} |
969 |
886 |
970 ML {* |
887 declare (in semiring_numeral) of_num_One [simp] |
971 local open Code_Thingol in |
888 declare (in semiring_numeral) of_num_plus_one [simp] |
972 |
889 declare (in semiring_numeral) of_num_one_plus [simp] |
973 fun add_code print target = |
890 declare (in semiring_numeral) of_num_plus [simp] |
974 let |
891 declare (in semiring_numeral) of_num_times [simp] |
975 fun dest_num one' dig0' dig1' thm = |
892 |
976 let |
893 declare (in semiring_1) of_nat_of_num [simp] |
977 fun dest_dig (IConst (c, _)) = if c = dig0' then 0 |
894 |
978 else if c = dig1' then 1 |
895 declare (in semiring_char_0) of_num_eq_iff [simp] |
979 else Code_Printer.eqn_error thm "Illegal numeral expression: illegal dig" |
896 declare (in semiring_char_0) of_num_eq_one_iff [simp] |
980 | dest_dig _ = Code_Printer.eqn_error thm "Illegal numeral expression: illegal digit"; |
897 declare (in semiring_char_0) one_eq_of_num_iff [simp] |
981 fun dest_num (IConst (c, _)) = if c = one' then 1 |
898 |
982 else Code_Printer.eqn_error thm "Illegal numeral expression: illegal leading digit" |
899 declare (in linordered_semidom) of_num_pos [simp] |
983 | dest_num (t1 `$ t2) = 2 * dest_num t2 + dest_dig t1 |
900 declare (in linordered_semidom) of_num_less_eq_iff [simp] |
984 | dest_num _ = Code_Printer.eqn_error thm "Illegal numeral expression: illegal term"; |
901 declare (in linordered_semidom) of_num_less_eq_one_iff [simp] |
985 in dest_num end; |
902 declare (in linordered_semidom) one_less_eq_of_num_iff [simp] |
986 fun pretty sgn literals [one', dig0', dig1'] _ thm _ _ [(t, _)] = |
903 declare (in linordered_semidom) of_num_less_iff [simp] |
987 (Code_Printer.str o print literals o sgn o dest_num one' dig0' dig1' thm) t |
904 declare (in linordered_semidom) of_num_less_one_iff [simp] |
988 fun add_syntax (c, sgn) = Code_Target.add_syntax_const target c |
905 declare (in linordered_semidom) one_less_of_num_iff [simp] |
989 (SOME (Code_Printer.complex_const_syntax |
906 declare (in linordered_semidom) of_num_nonneg [simp] |
990 (1, ([@{const_name One}, @{const_name Dig0}, @{const_name Dig1}], |
907 declare (in linordered_semidom) of_num_less_zero_iff [simp] |
991 pretty sgn)))); |
908 declare (in linordered_semidom) of_num_le_zero_iff [simp] |
992 in |
909 |
993 add_syntax (@{const_name Pls}, I) |
910 declare (in linordered_idom) le_signed_numeral_special [simp] |
994 #> add_syntax (@{const_name Mns}, (fn k => ~ k)) |
911 declare (in linordered_idom) less_signed_numeral_special [simp] |
995 end; |
912 |
996 |
913 declare (in semiring_1_minus) Dig_of_num_minus_one [simp] |
997 end |
914 declare (in semiring_1_minus) Dig_one_minus_of_num [simp] |
998 *} |
915 |
999 |
916 declare (in ring_1) Dig_plus_uminus [simp] |
1000 hide_const (open) One Dig0 Dig1 |
917 declare (in ring_1) of_int_of_num [simp] |
1001 |
918 |
1002 |
919 declare power_of_num [simp] |
1003 subsection {* Toy examples *} |
920 declare power_zero_of_num [simp] |
1004 |
921 declare power_minus_Dig0 [simp] |
1005 definition "foo \<longleftrightarrow> #4 * #2 + #7 = (#8 :: nat)" |
922 declare power_minus_Dig1 [simp] |
1006 definition "bar \<longleftrightarrow> #4 * #2 + #7 \<ge> (#8 :: int) - #3" |
923 |
1007 |
924 declare Suc_of_num [simp] |
1008 code_thms foo bar |
925 |
1009 export_code foo bar checking SML OCaml? Haskell? Scala? |
926 |
1010 |
927 subsection {* Simplification Procedures *} |
1011 text {* This is an ad-hoc @{text Code_Integer} setup. *} |
928 |
|
929 subsubsection {* Reorientation of equalities *} |
|
930 |
1012 |
931 setup {* |
1013 setup {* |
932 Reorient_Proc.add |
1014 fold (add_code Code_Printer.literal_numeral) |
933 (fn Const(@{const_name of_num}, _) $ _ => true |
1015 [Code_ML.target_SML, Code_ML.target_OCaml, Code_Haskell.target, Code_Scala.target] |
934 | Const(@{const_name uminus}, _) $ |
1016 *} |
935 (Const(@{const_name of_num}, _) $ _) => true |
1017 |
936 | _ => false) |
1018 code_type int |
937 *} |
1019 (SML "IntInf.int") |
938 |
1020 (OCaml "Big'_int.big'_int") |
939 simproc_setup reorient_num ("of_num n = x" | "- of_num m = y") = Reorient_Proc.proc |
1021 (Haskell "Integer") |
940 |
1022 (Scala "BigInt") |
941 |
1023 (Eval "int") |
942 subsubsection {* Constant folding for multiplication in semirings *} |
1024 |
943 |
1025 code_const "0::int" |
944 context semiring_numeral |
1026 (SML "0/ :/ IntInf.int") |
945 begin |
1027 (OCaml "Big'_int.zero") |
946 |
1028 (Haskell "0") |
947 lemma mult_of_num_commute: "x * of_num n = of_num n * x" |
1029 (Scala "BigInt(0)") |
948 by (induct n) |
1030 (Eval "0/ :/ int") |
949 (simp_all only: of_num.simps left_distrib right_distrib mult_1_left mult_1_right) |
1031 |
950 |
1032 code_const Int.pred |
951 definition |
1033 (SML "IntInf.- ((_), 1)") |
952 "commutes_with a b \<longleftrightarrow> a * b = b * a" |
1034 (OCaml "Big'_int.pred'_big'_int") |
953 |
1035 (Haskell "!(_/ -/ 1)") |
954 lemma commutes_with_commute: "commutes_with a b \<Longrightarrow> a * b = b * a" |
1036 (Scala "!(_/ -/ 1)") |
955 unfolding commutes_with_def . |
1037 (Eval "!(_/ -/ 1)") |
956 |
1038 |
957 lemma commutes_with_left_commute: "commutes_with a b \<Longrightarrow> a * (b * c) = b * (a * c)" |
1039 code_const Int.succ |
958 unfolding commutes_with_def by (simp only: mult_assoc [symmetric]) |
1040 (SML "IntInf.+ ((_), 1)") |
959 |
1041 (OCaml "Big'_int.succ'_big'_int") |
960 lemma commutes_with_numeral: "commutes_with x (of_num n)" "commutes_with (of_num n) x" |
1042 (Haskell "!(_/ +/ 1)") |
961 unfolding commutes_with_def by (simp_all add: mult_of_num_commute) |
1043 (Scala "!(_/ +/ 1)") |
962 |
1044 (Eval "!(_/ +/ 1)") |
963 lemmas mult_ac_numeral = |
1045 |
964 mult_assoc |
1046 code_const "op + \<Colon> int \<Rightarrow> int \<Rightarrow> int" |
965 commutes_with_commute |
1047 (SML "IntInf.+ ((_), (_))") |
966 commutes_with_left_commute |
1048 (OCaml "Big'_int.add'_big'_int") |
967 commutes_with_numeral |
1049 (Haskell infixl 6 "+") |
968 |
1050 (Scala infixl 7 "+") |
969 end |
1051 (Eval infixl 8 "+") |
970 |
1052 |
971 ML {* |
1053 code_const "uminus \<Colon> int \<Rightarrow> int" |
972 structure Semiring_Times_Assoc_Data : ASSOC_FOLD_DATA = |
1054 (SML "IntInf.~") |
973 struct |
1055 (OCaml "Big'_int.minus'_big'_int") |
974 val assoc_ss = HOL_ss addsimps @{thms mult_ac_numeral} |
1056 (Haskell "negate") |
975 val eq_reflection = eq_reflection |
1057 (Scala "!(- _)") |
976 fun is_numeral (Const(@{const_name of_num}, _) $ _) = true |
1058 (Eval "~/ _") |
977 | is_numeral _ = false; |
1059 |
978 end; |
1060 code_const "op - \<Colon> int \<Rightarrow> int \<Rightarrow> int" |
979 |
1061 (SML "IntInf.- ((_), (_))") |
980 structure Semiring_Times_Assoc = Assoc_Fold (Semiring_Times_Assoc_Data); |
1062 (OCaml "Big'_int.sub'_big'_int") |
981 *} |
1063 (Haskell infixl 6 "-") |
982 |
1064 (Scala infixl 7 "-") |
983 simproc_setup semiring_assoc_fold' ("(a::'a::semiring_numeral) * b") = |
1065 (Eval infixl 8 "-") |
984 {* fn phi => fn ss => fn ct => |
1066 |
985 Semiring_Times_Assoc.proc ss (Thm.term_of ct) *} |
1067 code_const "op * \<Colon> int \<Rightarrow> int \<Rightarrow> int" |
986 |
1068 (SML "IntInf.* ((_), (_))") |
987 |
1069 (OCaml "Big'_int.mult'_big'_int") |
988 subsection {* Toy examples *} |
1070 (Haskell infixl 7 "*") |
989 |
1071 (Scala infixl 8 "*") |
990 definition "bar \<longleftrightarrow> #4 * #2 + #7 = (#8 :: nat) \<and> #4 * #2 + #7 \<ge> (#8 :: int) - #3" |
1072 (Eval infixl 9 "*") |
991 |
1073 |
992 code_thms bar |
1074 code_const pdivmod |
993 |
1075 (SML "IntInf.divMod/ (IntInf.abs _,/ IntInf.abs _)") |
994 export_code bar checking SML OCaml? Haskell? |
1076 (OCaml "Big'_int.quomod'_big'_int/ (Big'_int.abs'_big'_int _)/ (Big'_int.abs'_big'_int _)") |
995 |
1077 (Haskell "divMod/ (abs _)/ (abs _)") |
996 end |
1078 (Scala "!((k: BigInt) => (l: BigInt) =>/ if (l == 0)/ (BigInt(0), k) else/ (k.abs '/% l.abs))") |
1079 (Eval "Integer.div'_mod/ (abs _)/ (abs _)") |
|
1080 |
|
1081 code_const "eq_class.eq \<Colon> int \<Rightarrow> int \<Rightarrow> bool" |
|
1082 (SML "!((_ : IntInf.int) = _)") |
|
1083 (OCaml "Big'_int.eq'_big'_int") |
|
1084 (Haskell infixl 4 "==") |
|
1085 (Scala infixl 5 "==") |
|
1086 (Eval infixl 6 "=") |
|
1087 |
|
1088 code_const "op \<le> \<Colon> int \<Rightarrow> int \<Rightarrow> bool" |
|
1089 (SML "IntInf.<= ((_), (_))") |
|
1090 (OCaml "Big'_int.le'_big'_int") |
|
1091 (Haskell infix 4 "<=") |
|
1092 (Scala infixl 4 "<=") |
|
1093 (Eval infixl 6 "<=") |
|
1094 |
|
1095 code_const "op < \<Colon> int \<Rightarrow> int \<Rightarrow> bool" |
|
1096 (SML "IntInf.< ((_), (_))") |
|
1097 (OCaml "Big'_int.lt'_big'_int") |
|
1098 (Haskell infix 4 "<") |
|
1099 (Scala infixl 4 "<") |
|
1100 (Eval infixl 6 "<") |
|
1101 |
|
1102 code_const Code_Numeral.int_of |
|
1103 (SML "IntInf.fromInt") |
|
1104 (OCaml "_") |
|
1105 (Haskell "toInteger") |
|
1106 (Scala "!_.as'_BigInt") |
|
1107 (Eval "_") |
|
1108 |
|
1109 export_code foo bar checking SML OCaml? Haskell? Scala? |
|
1110 |
|
1111 end |