author wenzelm Sat, 04 Jun 2016 16:10:44 +0200 changeset 63227 d3ed7f00e818 parent 63226 d8884c111bca child 63228 acfa595636c7
Integer.lcm normalizes the sign as in HOL/GCD.thy; tuned;
 NEWS file | annotate | diff | comparison | revisions src/Provers/Arith/fast_lin_arith.ML file | annotate | diff | comparison | revisions src/Pure/General/integer.ML file | annotate | diff | comparison | revisions src/Pure/General/rat.ML file | annotate | diff | comparison | revisions
```--- 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```
```--- 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```
```--- 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;
-```
```--- 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
```