src/Pure/General/integer.ML
author paulson
Fri, 05 Oct 2007 09:59:03 +0200
changeset 24854 0ebcd575d3c6
parent 24633 0a3a02066244
child 28308 d4396a28fb29
permissions -rw-r--r--
filtering out some package theorems
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
24633
0a3a02066244 moved Tools/integer.ML to Pure/General/integer.ML;
wenzelm
parents:
diff changeset
     1
(*  Title:      Tools/integer.ML
0a3a02066244 moved Tools/integer.ML to Pure/General/integer.ML;
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
0a3a02066244 moved Tools/integer.ML to Pure/General/integer.ML;
wenzelm
parents:
diff changeset
     3
    Author:     Florian Haftmann, TU Muenchen
0a3a02066244 moved Tools/integer.ML to Pure/General/integer.ML;
wenzelm
parents:
diff changeset
     4
0a3a02066244 moved Tools/integer.ML to Pure/General/integer.ML;
wenzelm
parents:
diff changeset
     5
Unbounded integers.
0a3a02066244 moved Tools/integer.ML to Pure/General/integer.ML;
wenzelm
parents:
diff changeset
     6
*)
0a3a02066244 moved Tools/integer.ML to Pure/General/integer.ML;
wenzelm
parents:
diff changeset
     7
0a3a02066244 moved Tools/integer.ML to Pure/General/integer.ML;
wenzelm
parents:
diff changeset
     8
signature INTEGER =
0a3a02066244 moved Tools/integer.ML to Pure/General/integer.ML;
wenzelm
parents:
diff changeset
     9
sig
0a3a02066244 moved Tools/integer.ML to Pure/General/integer.ML;
wenzelm
parents:
diff changeset
    10
  val sign: int -> order
0a3a02066244 moved Tools/integer.ML to Pure/General/integer.ML;
wenzelm
parents:
diff changeset
    11
  val sum: int list -> int
0a3a02066244 moved Tools/integer.ML to Pure/General/integer.ML;
wenzelm
parents:
diff changeset
    12
  val div_mod: int -> int -> int * int
0a3a02066244 moved Tools/integer.ML to Pure/General/integer.ML;
wenzelm
parents:
diff changeset
    13
  val square: int -> int
0a3a02066244 moved Tools/integer.ML to Pure/General/integer.ML;
wenzelm
parents:
diff changeset
    14
  val pow: int -> int -> int (* exponent -> base -> result *)
0a3a02066244 moved Tools/integer.ML to Pure/General/integer.ML;
wenzelm
parents:
diff changeset
    15
  val gcd: int -> int -> int
0a3a02066244 moved Tools/integer.ML to Pure/General/integer.ML;
wenzelm
parents:
diff changeset
    16
  val gcds: int list -> int
0a3a02066244 moved Tools/integer.ML to Pure/General/integer.ML;
wenzelm
parents:
diff changeset
    17
  val lcm: int -> int -> int
0a3a02066244 moved Tools/integer.ML to Pure/General/integer.ML;
wenzelm
parents:
diff changeset
    18
  val lcms: int list -> int
0a3a02066244 moved Tools/integer.ML to Pure/General/integer.ML;
wenzelm
parents:
diff changeset
    19
end;
0a3a02066244 moved Tools/integer.ML to Pure/General/integer.ML;
wenzelm
parents:
diff changeset
    20
0a3a02066244 moved Tools/integer.ML to Pure/General/integer.ML;
wenzelm
parents:
diff changeset
    21
structure Integer : INTEGER =
0a3a02066244 moved Tools/integer.ML to Pure/General/integer.ML;
wenzelm
parents:
diff changeset
    22
struct
0a3a02066244 moved Tools/integer.ML to Pure/General/integer.ML;
wenzelm
parents:
diff changeset
    23
0a3a02066244 moved Tools/integer.ML to Pure/General/integer.ML;
wenzelm
parents:
diff changeset
    24
fun sign x = int_ord (x, 0);
0a3a02066244 moved Tools/integer.ML to Pure/General/integer.ML;
wenzelm
parents:
diff changeset
    25
0a3a02066244 moved Tools/integer.ML to Pure/General/integer.ML;
wenzelm
parents:
diff changeset
    26
fun sum xs = fold (curry op +) xs 0;
0a3a02066244 moved Tools/integer.ML to Pure/General/integer.ML;
wenzelm
parents:
diff changeset
    27
0a3a02066244 moved Tools/integer.ML to Pure/General/integer.ML;
wenzelm
parents:
diff changeset
    28
fun div_mod x y = IntInf.divMod (x, y);
0a3a02066244 moved Tools/integer.ML to Pure/General/integer.ML;
wenzelm
parents:
diff changeset
    29
0a3a02066244 moved Tools/integer.ML to Pure/General/integer.ML;
wenzelm
parents:
diff changeset
    30
fun square x = x * x;
0a3a02066244 moved Tools/integer.ML to Pure/General/integer.ML;
wenzelm
parents:
diff changeset
    31
0a3a02066244 moved Tools/integer.ML to Pure/General/integer.ML;
wenzelm
parents:
diff changeset
    32
fun pow k l =
0a3a02066244 moved Tools/integer.ML to Pure/General/integer.ML;
wenzelm
parents:
diff changeset
    33
  let
0a3a02066244 moved Tools/integer.ML to Pure/General/integer.ML;
wenzelm
parents:
diff changeset
    34
    fun pw 0 _ = 1
0a3a02066244 moved Tools/integer.ML to Pure/General/integer.ML;
wenzelm
parents:
diff changeset
    35
      | pw 1 l = l
0a3a02066244 moved Tools/integer.ML to Pure/General/integer.ML;
wenzelm
parents:
diff changeset
    36
      | pw k l =
0a3a02066244 moved Tools/integer.ML to Pure/General/integer.ML;
wenzelm
parents:
diff changeset
    37
          let
0a3a02066244 moved Tools/integer.ML to Pure/General/integer.ML;
wenzelm
parents:
diff changeset
    38
            val (k', r) = div_mod k 2;
0a3a02066244 moved Tools/integer.ML to Pure/General/integer.ML;
wenzelm
parents:
diff changeset
    39
            val l' = pw k' (l * l);
0a3a02066244 moved Tools/integer.ML to Pure/General/integer.ML;
wenzelm
parents:
diff changeset
    40
          in if r = 0 then l' else l' * l end;
0a3a02066244 moved Tools/integer.ML to Pure/General/integer.ML;
wenzelm
parents:
diff changeset
    41
  in
0a3a02066244 moved Tools/integer.ML to Pure/General/integer.ML;
wenzelm
parents:
diff changeset
    42
    if k < 0
0a3a02066244 moved Tools/integer.ML to Pure/General/integer.ML;
wenzelm
parents:
diff changeset
    43
    then error "pow: negative exponent"
0a3a02066244 moved Tools/integer.ML to Pure/General/integer.ML;
wenzelm
parents:
diff changeset
    44
    else pw k l
0a3a02066244 moved Tools/integer.ML to Pure/General/integer.ML;
wenzelm
parents:
diff changeset
    45
  end;
0a3a02066244 moved Tools/integer.ML to Pure/General/integer.ML;
wenzelm
parents:
diff changeset
    46
0a3a02066244 moved Tools/integer.ML to Pure/General/integer.ML;
wenzelm
parents:
diff changeset
    47
fun gcd x y =
0a3a02066244 moved Tools/integer.ML to Pure/General/integer.ML;
wenzelm
parents:
diff changeset
    48
  let
0a3a02066244 moved Tools/integer.ML to Pure/General/integer.ML;
wenzelm
parents:
diff changeset
    49
    fun gxd x y = if y = 0 then x else gxd y (x mod y)
0a3a02066244 moved Tools/integer.ML to Pure/General/integer.ML;
wenzelm
parents:
diff changeset
    50
  in if x < y then gxd y x else gxd x y end;
0a3a02066244 moved Tools/integer.ML to Pure/General/integer.ML;
wenzelm
parents:
diff changeset
    51
0a3a02066244 moved Tools/integer.ML to Pure/General/integer.ML;
wenzelm
parents:
diff changeset
    52
fun gcds xs = fold gcd xs 0;
0a3a02066244 moved Tools/integer.ML to Pure/General/integer.ML;
wenzelm
parents:
diff changeset
    53
0a3a02066244 moved Tools/integer.ML to Pure/General/integer.ML;
wenzelm
parents:
diff changeset
    54
fun lcm x y = (x * y) div (gcd x y);
0a3a02066244 moved Tools/integer.ML to Pure/General/integer.ML;
wenzelm
parents:
diff changeset
    55
fun lcms xs = fold lcm xs 1;
0a3a02066244 moved Tools/integer.ML to Pure/General/integer.ML;
wenzelm
parents:
diff changeset
    56
0a3a02066244 moved Tools/integer.ML to Pure/General/integer.ML;
wenzelm
parents:
diff changeset
    57
end;
0a3a02066244 moved Tools/integer.ML to Pure/General/integer.ML;
wenzelm
parents:
diff changeset
    58