author | wenzelm |
Mon, 25 Mar 2019 16:45:08 +0100 | |
changeset 69980 | f2e3adfd916f |
parent 69729 | 4591221824f6 |
child 73019 | 05e2cab9af8b |
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 |
|
68028 | 23 |
val radicify: int -> int -> int -> int list (* base -> number of positions -> value -> coefficients *) |
24 |
val eval_radix: int -> int list -> int (* base -> coefficients -> value *) |
|
24633 | 25 |
end; |
26 |
||
27 |
structure Integer : INTEGER = |
|
28 |
struct |
|
29 |
||
33029 | 30 |
fun min x y = Int.min (x, y); |
31 |
fun max x y = Int.max (x, y); |
|
32 |
||
33002 | 33 |
fun add x y = x + y; |
34 |
fun mult x y = x * y; |
|
24633 | 35 |
|
33002 | 36 |
fun sum xs = fold add xs 0; |
37 |
fun prod xs = fold mult xs 1; |
|
38 |
||
39 |
fun sign x = int_ord (x, 0); |
|
24633 | 40 |
|
41 |
fun div_mod x y = IntInf.divMod (x, y); |
|
42 |
||
43 |
fun square x = x * x; |
|
44 |
||
69729 | 45 |
fun pow k l = IntInf.pow (l, k); |
24633 | 46 |
|
63227
d3ed7f00e818
Integer.lcm normalizes the sign as in HOL/GCD.thy;
wenzelm
parents:
33029
diff
changeset
|
47 |
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
|
48 |
fun lcm x y = abs (PolyML.IntInf.lcm (x, y)); |
24633 | 49 |
|
63227
d3ed7f00e818
Integer.lcm normalizes the sign as in HOL/GCD.thy;
wenzelm
parents:
33029
diff
changeset
|
50 |
fun gcds [] = 0 |
d3ed7f00e818
Integer.lcm normalizes the sign as in HOL/GCD.thy;
wenzelm
parents:
33029
diff
changeset
|
51 |
| gcds (x :: xs) = fold gcd xs x; |
24633 | 52 |
|
63227
d3ed7f00e818
Integer.lcm normalizes the sign as in HOL/GCD.thy;
wenzelm
parents:
33029
diff
changeset
|
53 |
fun lcms [] = 1 |
d3ed7f00e818
Integer.lcm normalizes the sign as in HOL/GCD.thy;
wenzelm
parents:
33029
diff
changeset
|
54 |
| lcms (x :: xs) = abs (Library.foldl PolyML.IntInf.lcm (x, xs)); |
24633 | 55 |
|
68028 | 56 |
fun radicify base len k = |
57 |
let |
|
58 |
val _ = if base < 2 |
|
59 |
then error ("Bad radix base: " ^ string_of_int base) else (); |
|
60 |
fun shift i = swap (div_mod i base); |
|
61 |
in funpow_yield len shift k |> fst end; |
|
62 |
||
63 |
fun eval_radix base ks = |
|
64 |
fold_rev (fn k => fn i => k + i * base) ks 0; |
|
65 |
||
24633 | 66 |
end; |