Integer.lcm normalizes the sign as in HOL/GCD.thy;
authorwenzelm
Sat Jun 04 16:10:44 2016 +0200 (2016-06-04)
changeset 63227d3ed7f00e818
parent 63226 d8884c111bca
child 63228 acfa595636c7
Integer.lcm normalizes the sign as in HOL/GCD.thy;
tuned;
NEWS
src/Provers/Arith/fast_lin_arith.ML
src/Pure/General/integer.ML
src/Pure/General/rat.ML
     1.1 --- a/NEWS	Fri Jun 03 22:27:01 2016 +0200
     1.2 +++ b/NEWS	Sat Jun 04 16:10:44 2016 +0200
     1.3 @@ -347,6 +347,11 @@
     1.4  
     1.5  *** ML ***
     1.6  
     1.7 +* Integer.gcd and Integer.lcm use efficient operations from the Poly/ML
     1.8 +(notably for big integers). Subtle change of semantics: Integer.gcd and
     1.9 +Integer.lcm both normalize the sign, results are never negative. This
    1.10 +coincides with the definitions in HOL/GCD.thy. INCOMPATIBILITY.
    1.11 +
    1.12  * Structure Rat for rational numbers is now an integral part of
    1.13  Isabelle/ML, with special notation @int/nat or @int for numerals (an
    1.14  abbreviation for antiquotation @{Pure.rat argument}) and ML pretty
     2.1 --- a/src/Provers/Arith/fast_lin_arith.ML	Fri Jun 03 22:27:01 2016 +0200
     2.2 +++ b/src/Provers/Arith/fast_lin_arith.ML	Sat Jun 04 16:10:44 2016 +0200
     2.3 @@ -248,7 +248,7 @@
     2.4  
     2.5  fun elim_var v (i1 as Lineq(_,ty1,l1,_)) (i2 as Lineq(_,ty2,l2,_)) =
     2.6    let val c1 = nth l1 v and c2 = nth l2 v
     2.7 -      val m = Integer.lcm (abs c1) (abs c2)
     2.8 +      val m = Integer.lcm c1 c2
     2.9        val m1 = m div (abs c1) and m2 = m div (abs c2)
    2.10        val (n1,n2) =
    2.11          if (c1 >= 0) = (c2 >= 0)
    2.12 @@ -483,7 +483,7 @@
    2.13  
    2.14  fun integ(rlhs,r,rel,rrhs,s,d) =
    2.15  let val (rn,rd) = Rat.dest r and (sn,sd) = Rat.dest s
    2.16 -    val m = Integer.lcms(map (abs o snd o Rat.dest) (r :: s :: map snd rlhs @ map snd rrhs))
    2.17 +    val m = Integer.lcms(map (snd o Rat.dest) (r :: s :: map snd rlhs @ map snd rrhs))
    2.18      fun mult(t,r) =
    2.19          let val (i,j) = Rat.dest r
    2.20          in (t,i * (m div j)) end
     3.1 --- a/src/Pure/General/integer.ML	Fri Jun 03 22:27:01 2016 +0200
     3.2 +++ b/src/Pure/General/integer.ML	Sat Jun 04 16:10:44 2016 +0200
     3.3 @@ -17,8 +17,8 @@
     3.4    val square: int -> int
     3.5    val pow: int -> int -> int (* exponent -> base -> result *)
     3.6    val gcd: int -> int -> int
     3.7 +  val lcm: int -> int -> int
     3.8    val gcds: int list -> int
     3.9 -  val lcm: int -> int -> int
    3.10    val lcms: int list -> int
    3.11  end;
    3.12  
    3.13 @@ -55,15 +55,13 @@
    3.14      else pw k l
    3.15    end;
    3.16  
    3.17 -fun gcd x y =
    3.18 -  let
    3.19 -    fun gxd x y = if y = 0 then x else gxd y (x mod y)
    3.20 -  in if x < y then gxd y x else gxd x y end;
    3.21 +fun gcd x y = PolyML.IntInf.gcd (x, y);
    3.22 +fun lcm x y = abs (PolyML.IntInf.lcm (x, y));
    3.23  
    3.24 -fun gcds xs = fold gcd xs 0;
    3.25 +fun gcds [] = 0
    3.26 +  | gcds (x :: xs) = fold gcd xs x;
    3.27  
    3.28 -fun lcm x y = (x * y) div (gcd x y);
    3.29 -fun lcms xs = fold lcm xs 1;
    3.30 +fun lcms [] = 1
    3.31 +  | lcms (x :: xs) = abs (Library.foldl PolyML.IntInf.lcm (x, xs));
    3.32  
    3.33  end;
    3.34 -
     4.1 --- a/src/Pure/General/rat.ML	Fri Jun 03 22:27:01 2016 +0200
     4.2 +++ b/src/Pure/General/rat.ML	Sat Jun 04 16:10:44 2016 +0200
     4.3 @@ -34,13 +34,13 @@
     4.4  fun of_int i = Rat (i, 1);
     4.5  
     4.6  fun common (p1, q1) (p2, q2) =
     4.7 -  let val m = PolyML.IntInf.lcm (q1, q2)
     4.8 +  let val m = Integer.lcm q1 q2
     4.9    in ((p1 * (m div q1), p2 * (m div q2)), m) end;
    4.10  
    4.11  fun make (_, 0) = raise Div
    4.12    | make (p, q) =
    4.13      let
    4.14 -      val m = PolyML.IntInf.gcd (p, q);
    4.15 +      val m = Integer.gcd p q;
    4.16        val (p', q') = (p div m, q div m);
    4.17      in Rat (if q' < 0 then (~ p', ~ q') else (p', q')) end
    4.18