# HG changeset patch
# User wenzelm
# Date 1465049444 -7200
# Node ID d3ed7f00e81883c12f972709adecd3f7310de33d
# Parent  d8884c111bca15d5375a45cf5cdb5ca99cf4e355
Integer.lcm normalizes the sign as in HOL/GCD.thy;
tuned;

diff -r d8884c111bca -r d3ed7f00e818 NEWS
--- a/NEWS	Fri Jun 03 22:27:01 2016 +0200
+++ b/NEWS	Sat Jun 04 16:10:44 2016 +0200
@@ -347,6 +347,11 @@
 
 *** ML ***
 
+* Integer.gcd and Integer.lcm use efficient operations from the Poly/ML
+(notably for big integers). Subtle change of semantics: Integer.gcd and
+Integer.lcm both normalize the sign, results are never negative. This
+coincides with the definitions in HOL/GCD.thy. INCOMPATIBILITY.
+
 * Structure Rat for rational numbers is now an integral part of
 Isabelle/ML, with special notation @int/nat or @int for numerals (an
 abbreviation for antiquotation @{Pure.rat argument}) and ML pretty
diff -r d8884c111bca -r d3ed7f00e818 src/Provers/Arith/fast_lin_arith.ML
--- a/src/Provers/Arith/fast_lin_arith.ML	Fri Jun 03 22:27:01 2016 +0200
+++ b/src/Provers/Arith/fast_lin_arith.ML	Sat Jun 04 16:10:44 2016 +0200
@@ -248,7 +248,7 @@
 
 fun elim_var v (i1 as Lineq(_,ty1,l1,_)) (i2 as Lineq(_,ty2,l2,_)) =
   let val c1 = nth l1 v and c2 = nth l2 v
-      val m = Integer.lcm (abs c1) (abs c2)
+      val m = Integer.lcm c1 c2
       val m1 = m div (abs c1) and m2 = m div (abs c2)
       val (n1,n2) =
         if (c1 >= 0) = (c2 >= 0)
@@ -483,7 +483,7 @@
 
 fun integ(rlhs,r,rel,rrhs,s,d) =
 let val (rn,rd) = Rat.dest r and (sn,sd) = Rat.dest s
-    val m = Integer.lcms(map (abs o snd o Rat.dest) (r :: s :: map snd rlhs @ map snd rrhs))
+    val m = Integer.lcms(map (snd o Rat.dest) (r :: s :: map snd rlhs @ map snd rrhs))
     fun mult(t,r) =
         let val (i,j) = Rat.dest r
         in (t,i * (m div j)) end
diff -r d8884c111bca -r d3ed7f00e818 src/Pure/General/integer.ML
--- a/src/Pure/General/integer.ML	Fri Jun 03 22:27:01 2016 +0200
+++ b/src/Pure/General/integer.ML	Sat Jun 04 16:10:44 2016 +0200
@@ -17,8 +17,8 @@
   val square: int -> int
   val pow: int -> int -> int (* exponent -> base -> result *)
   val gcd: int -> int -> int
+  val lcm: int -> int -> int
   val gcds: int list -> int
-  val lcm: int -> int -> int
   val lcms: int list -> int
 end;
 
@@ -55,15 +55,13 @@
     else pw k l
   end;
 
-fun gcd x y =
-  let
-    fun gxd x y = if y = 0 then x else gxd y (x mod y)
-  in if x < y then gxd y x else gxd x y end;
+fun gcd x y = PolyML.IntInf.gcd (x, y);
+fun lcm x y = abs (PolyML.IntInf.lcm (x, y));
 
-fun gcds xs = fold gcd xs 0;
+fun gcds [] = 0
+  | gcds (x :: xs) = fold gcd xs x;
 
-fun lcm x y = (x * y) div (gcd x y);
-fun lcms xs = fold lcm xs 1;
+fun lcms [] = 1
+  | lcms (x :: xs) = abs (Library.foldl PolyML.IntInf.lcm (x, xs));
 
 end;
-
diff -r d8884c111bca -r d3ed7f00e818 src/Pure/General/rat.ML
--- a/src/Pure/General/rat.ML	Fri Jun 03 22:27:01 2016 +0200
+++ b/src/Pure/General/rat.ML	Sat Jun 04 16:10:44 2016 +0200
@@ -34,13 +34,13 @@
 fun of_int i = Rat (i, 1);
 
 fun common (p1, q1) (p2, q2) =
-  let val m = PolyML.IntInf.lcm (q1, q2)
+  let val m = Integer.lcm q1 q2
   in ((p1 * (m div q1), p2 * (m div q2)), m) end;
 
 fun make (_, 0) = raise Div
   | make (p, q) =
     let
-      val m = PolyML.IntInf.gcd (p, q);
+      val m = Integer.gcd p q;
       val (p', q') = (p div m, q div m);
     in Rat (if q' < 0 then (~ p', ~ q') else (p', q')) end