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