author | wenzelm |
Fri, 03 Nov 2017 19:16:41 +0100 | |
changeset 66996 | 22ca0f37f491 |
parent 63227 | d3ed7f00e818 |
child 66997 | 17eb23e43630 |
permissions | -rw-r--r-- |
28308 | 1 |
(* Title: Pure/General/integer.ML |
24633 | 2 |
Author: Florian Haftmann, TU Muenchen |
3 |
||
33002 | 4 |
Auxiliary operations on (unbounded) integers. |
24633 | 5 |
*) |
6 |
||
7 |
signature INTEGER = |
|
8 |
sig |
|
33029 | 9 |
val min: int -> int -> int |
10 |
val max: int -> int -> int |
|
33002 | 11 |
val add: int -> int -> int |
12 |
val mult: int -> int -> int |
|
13 |
val sum: int list -> int |
|
14 |
val prod: int list -> int |
|
24633 | 15 |
val sign: int -> order |
16 |
val div_mod: int -> int -> int * int |
|
17 |
val square: int -> int |
|
18 |
val pow: int -> int -> int (* exponent -> base -> result *) |
|
19 |
val gcd: int -> int -> int |
|
63227
d3ed7f00e818
Integer.lcm normalizes the sign as in HOL/GCD.thy;
wenzelm
parents:
33029
diff
changeset
|
20 |
val lcm: int -> int -> int |
24633 | 21 |
val gcds: int list -> int |
22 |
val lcms: int list -> int |
|
23 |
end; |
|
24 |
||
25 |
structure Integer : INTEGER = |
|
26 |
struct |
|
27 |
||
33029 | 28 |
fun min x y = Int.min (x, y); |
29 |
fun max x y = Int.max (x, y); |
|
30 |
||
33002 | 31 |
fun add x y = x + y; |
32 |
fun mult x y = x * y; |
|
24633 | 33 |
|
33002 | 34 |
fun sum xs = fold add xs 0; |
35 |
fun prod xs = fold mult xs 1; |
|
36 |
||
37 |
fun sign x = int_ord (x, 0); |
|
24633 | 38 |
|
39 |
fun div_mod x y = IntInf.divMod (x, y); |
|
40 |
||
41 |
fun square x = x * x; |
|
42 |
||
43 |
fun pow k l = |
|
44 |
let |
|
45 |
fun pw 0 _ = 1 |
|
46 |
| pw 1 l = l |
|
47 |
| pw k l = |
|
48 |
let |
|
49 |
val (k', r) = div_mod k 2; |
|
50 |
val l' = pw k' (l * l); |
|
51 |
in if r = 0 then l' else l' * l end; |
|
52 |
in |
|
53 |
if k < 0 |
|
66996 | 54 |
then IntInf.pow (l, k) |
24633 | 55 |
else pw k l |
56 |
end; |
|
57 |
||
63227
d3ed7f00e818
Integer.lcm normalizes the sign as in HOL/GCD.thy;
wenzelm
parents:
33029
diff
changeset
|
58 |
fun gcd x y = PolyML.IntInf.gcd (x, y); |
d3ed7f00e818
Integer.lcm normalizes the sign as in HOL/GCD.thy;
wenzelm
parents:
33029
diff
changeset
|
59 |
fun lcm x y = abs (PolyML.IntInf.lcm (x, y)); |
24633 | 60 |
|
63227
d3ed7f00e818
Integer.lcm normalizes the sign as in HOL/GCD.thy;
wenzelm
parents:
33029
diff
changeset
|
61 |
fun gcds [] = 0 |
d3ed7f00e818
Integer.lcm normalizes the sign as in HOL/GCD.thy;
wenzelm
parents:
33029
diff
changeset
|
62 |
| gcds (x :: xs) = fold gcd xs x; |
24633 | 63 |
|
63227
d3ed7f00e818
Integer.lcm normalizes the sign as in HOL/GCD.thy;
wenzelm
parents:
33029
diff
changeset
|
64 |
fun lcms [] = 1 |
d3ed7f00e818
Integer.lcm normalizes the sign as in HOL/GCD.thy;
wenzelm
parents:
33029
diff
changeset
|
65 |
| lcms (x :: xs) = abs (Library.foldl PolyML.IntInf.lcm (x, xs)); |
24633 | 66 |
|
67 |
end; |