author wenzelm Wed, 01 Jun 2016 19:23:18 +0200 changeset 63211 0bec0d1d9998 parent 63210 a0685d2b420b child 63212 cc9c1f6a6b88
 NEWS file | annotate | diff | comparison | revisions src/HOL/Library/Sum_of_Squares/sum_of_squares.ML file | annotate | diff | comparison | revisions src/HOL/Library/positivstellensatz.ML file | annotate | diff | comparison | revisions src/HOL/Multivariate_Analysis/normarith.ML file | annotate | diff | comparison | revisions src/HOL/Tools/groebner.ML file | annotate | diff | comparison | revisions src/HOL/Tools/lin_arith.ML file | annotate | diff | comparison | revisions src/Pure/General/rat.ML file | annotate | diff | comparison | revisions
```--- a/NEWS	Wed Jun 01 17:46:12 2016 +0200
+++ b/NEWS	Wed Jun 01 19:23:18 2016 +0200
@@ -348,7 +348,7 @@
*** ML ***

-< <= > >= <>. INCOMPATIBILITY, need to use + instead of +/ etc.
+< <= > >= <> ~ abs. INCOMPATIBILITY, need to use + instead of +/ etc.

This is particularly useful for conditional compilation, without```
```--- a/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML	Wed Jun 01 17:46:12 2016 +0200
+++ b/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML	Wed Jun 01 19:23:18 2016 +0200
@@ -41,16 +41,12 @@

fun round_rat r =
let
-    val (a,b) = Rat.dest (Rat.abs r)
+    val (a,b) = Rat.dest (abs r)
val d = a div b
-    val s = if r < @0 then (Rat.neg o Rat.of_int) else Rat.of_int
+    val s = if r < @0 then ~ o Rat.of_int else Rat.of_int
val x2 = 2 * (a - (b * d))
in s (if x2 >= b then d + 1 else d) end

-val abs_rat = Rat.abs;
-val pow2 = rat_pow @2;
-val pow10 = rat_pow @10;
-

val trace = Attrib.setup_config_bool @{binding sos_trace} (K false);
val debug = Attrib.setup_config_bool @{binding sos_debug} (K false);
@@ -74,8 +70,8 @@
local

fun normalize y =
-  if abs_rat y < @1/10 then normalize (@10 * y) - 1
-  else if abs_rat y >= @1 then normalize (y / @10) + 1
+  if abs y < @1/10 then normalize (@10 * y) - 1
+  else if abs y >= @1 then normalize (y / @10) + 1
else 0

in
@@ -84,10 +80,10 @@
if x = @0 then "0.0"
else
let
-      val y = Rat.abs x
+      val y = abs x
val e = normalize y
-      val z = pow10(~ e) * y + @1
-      val k = int_of_rat (round_rat(pow10 d * z))
+      val z = rat_pow @10 (~ e) * y + @1
+      val k = int_of_rat (round_rat (rat_pow @10 d * z))
in
(if x < @0 then "-0." else "0.") ^
implode (tl (raw_explode(string_of_int k))) ^
@@ -182,7 +178,7 @@
if c = @0 then poly_0
else FuncUtil.Monomialfunc.map (fn _ => fn x => c * x) p;

-fun poly_neg p = FuncUtil.Monomialfunc.map (K Rat.neg) p;
+fun poly_neg p = FuncUtil.Monomialfunc.map (K ~) p;

@@ -319,7 +315,7 @@
val numeral = Scan.one isnum
val decimalint = Scan.repeat1 numeral >> (rat_of_string o implode)
val decimalfrac = Scan.repeat1 numeral
-  >> (fn s => rat_of_string(implode s) / pow10 (length s))
+  >> (fn s => rat_of_string(implode s) / rat_pow @10 (length s))
val decimalsig =
decimalint -- Scan.option (Scan.\$\$ "." |-- decimalfrac)
>> (fn (h,NONE) => h | (h,SOME x) => h + x)
@@ -333,7 +329,7 @@
val exponent = (\$\$ "e" || \$\$ "E") |-- signed decimalint;

val decimal = signed decimalsig -- (emptyin @0|| exponent)
-  >> (fn (h, x) => h * pow10 (int_of_rat x));
+  >> (fn (h, x) => h * rat_pow @10 (int_of_rat x));

fun mkparser p s =
let val (x,rst) = p (raw_explode s)
@@ -359,7 +355,7 @@
fun common_denominator fld amat acc =
fld (fn (_,c) => fn a => lcm_rat (denominator_rat c) a) amat acc
fun maximal_element fld amat acc =
-    fld (fn (_,c) => fn maxa => max_rat maxa (abs_rat c)) amat acc
+    fld (fn (_,c) => fn maxa => max_rat maxa (abs c)) amat acc
fun float_of_rat x =
let val (a,b) = Rat.dest x
in Real.fromInt a / Real.fromInt b end;
@@ -374,8 +370,8 @@
val obj' = vector_cmul cd2 obj
val max1 = fold_rev (maximal_element Inttriplefunc.fold) mats' @0
val max2 = maximal_element FuncUtil.Intfunc.fold (snd obj') @0
-    val scal1 = pow2 (20 - int_of_float(Math.ln (float_of_rat max1) / Math.ln 2.0))
-    val scal2 = pow2 (20 - int_of_float(Math.ln (float_of_rat max2) / Math.ln 2.0))
+    val scal1 = rat_pow @2 (20 - int_of_float(Math.ln (float_of_rat max1) / Math.ln 2.0))
+    val scal2 = rat_pow @2 (20 - int_of_float(Math.ln (float_of_rat max2) / Math.ln 2.0))
val mats'' = map (Inttriplefunc.map (fn _ => fn x => x * scal1)) mats'
val obj'' = vector_cmul scal2 obj'
in solver obj'' mats'' end
@@ -438,7 +434,7 @@
fun elim e =
let val b = Inttriplefunc.tryapplyd e v @0 in
if b = @0 then e
-                  else tri_equation_add e (tri_equation_cmul (Rat.neg b / a) eq)
+                  else tri_equation_add e (tri_equation_cmul (~ b / a) eq)
end
in
eliminate (Inttriplefunc.update(v, eq') (Inttriplefunc.map (K elim) dun))
@@ -559,7 +555,7 @@

fun epoly_of_poly p =
FuncUtil.Monomialfunc.fold (fn (m, c) => fn a =>
-      FuncUtil.Monomialfunc.update (m, Inttriplefunc.onefunc ((0, 0, 0), Rat.neg c)) a)
+      FuncUtil.Monomialfunc.update (m, Inttriplefunc.onefunc ((0, 0, 0), ~ c)) a)
p FuncUtil.Monomialfunc.empty;

(* String for block diagonal matrix numbered k.                              *)
@@ -725,7 +721,7 @@
in (vec, map diag allmats) end
val (vec, ratdias) =
if null pvs then find_rounding @1
-      else tryfind find_rounding (map Rat.of_int (1 upto 31) @ map pow2 (5 upto 66))
+      else tryfind find_rounding (map Rat.of_int (1 upto 31) @ map (rat_pow @2) (5 upto 66))
val newassigs =
fold_rev (fn k => Inttriplefunc.update (nth pvs (k - 1), int_element vec k))
(1 upto dim vec) (Inttriplefunc.onefunc ((0, 0, 0), Rat.of_int ~1))```
```--- a/src/HOL/Library/positivstellensatz.ML	Wed Jun 01 17:46:12 2016 +0200
+++ b/src/HOL/Library/positivstellensatz.ML	Wed Jun 01 19:23:18 2016 +0200
@@ -615,10 +615,10 @@
in
if c1 * c2 >= @0 then acc else
let
-                 val e1' = linear_cmul (Rat.abs c2) e1
-                 val e2' = linear_cmul (Rat.abs c1) e2
-                 val p1' = Product(Rational_lt(Rat.abs c2),p1)
-                 val p2' = Product(Rational_lt(Rat.abs c1),p2)
+                 val e1' = linear_cmul (abs c2) e1
+                 val e2' = linear_cmul (abs c1) e2
+                 val p1' = Product(Rational_lt (abs c2), p1)
+                 val p2' = Product(Rational_lt (abs c1), p2)
end
end
@@ -653,11 +653,11 @@
let val d = FuncUtil.Ctermfunc.tryapplyd t x @0 in
if d = @0 then inp else
let
-                 val k = (Rat.neg d) * Rat.abs c / c
+                 val k = ~ d * abs c / c
val e' = linear_cmul k e
-                 val t' = linear_cmul (Rat.abs c) t
+                 val t' = linear_cmul (abs c) t
val p' = Eqmul(FuncUtil.Monomialfunc.onefunc (FuncUtil.Ctermfunc.empty, k),p)
-                 val q' = Product(Rational_lt(Rat.abs c),q)
+                 val q' = Product(Rational_lt (abs c), q)
end
end```
```--- a/src/HOL/Multivariate_Analysis/normarith.ML	Wed Jun 01 17:46:12 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/normarith.ML	Wed Jun 01 19:23:18 2016 +0200
@@ -32,7 +32,7 @@
(Thm.dest_arg t) acc
| _ => augment_norm true t acc

- val cterm_lincomb_neg = FuncUtil.Ctermfunc.map (K Rat.neg)
+ val cterm_lincomb_neg = FuncUtil.Ctermfunc.map (K ~)
fun cterm_lincomb_cmul c t =
if c = @0 then FuncUtil.Ctermfunc.empty else FuncUtil.Ctermfunc.map (fn _ => fn x => x * c) t
fun cterm_lincomb_add l r = FuncUtil.Ctermfunc.combine (curry op +) (fn x => x = @0) l r
@@ -40,7 +40,7 @@
fun cterm_lincomb_eq l r = FuncUtil.Ctermfunc.is_empty (cterm_lincomb_sub l r)

(*
- val int_lincomb_neg = FuncUtil.Intfunc.map (K Rat.neg)
+ val int_lincomb_neg = FuncUtil.Intfunc.map (K ~)
*)
fun int_lincomb_cmul c t =
if c = @0 then FuncUtil.Intfunc.empty else FuncUtil.Intfunc.map (fn _ => fn x => x * c) t
@@ -89,7 +89,7 @@
(*
fun flip v eq =
if FuncUtil.Ctermfunc.defined eq v
-  then FuncUtil.Ctermfunc.update (v, Rat.neg (FuncUtil.Ctermfunc.apply eq v)) eq else eq
+  then FuncUtil.Ctermfunc.update (v, ~ (FuncUtil.Ctermfunc.apply eq v)) eq else eq
*)
fun allsubsets s = case s of
[] => [[]]
@@ -109,7 +109,7 @@
then
let
val c = FuncUtil.Intfunc.apply eq v
-         val vdef = int_lincomb_cmul (Rat.neg (Rat.inv c)) eq
+         val vdef = int_lincomb_cmul (~ (Rat.inv c)) eq
fun eliminate eqn = if not (FuncUtil.Intfunc.defined eqn v) then eqn
else int_lincomb_add (int_lincomb_cmul (FuncUtil.Intfunc.apply eqn v) vdef) eqn
in (case solve (remove (op =) v vs, map eliminate oeqs) of
@@ -254,7 +254,7 @@

fun int_flip v eq =
if FuncUtil.Intfunc.defined eq v
-  then FuncUtil.Intfunc.update (v, Rat.neg (FuncUtil.Intfunc.apply eq v)) eq else eq;
+  then FuncUtil.Intfunc.update (v, ~ (FuncUtil.Intfunc.apply eq v)) eq else eq;

local
val pth_zero = @{thm norm_zero}
@@ -283,8 +283,10 @@
let
fun coefficients x =
let
-       val inp = if FuncUtil.Ctermfunc.defined d x then FuncUtil.Intfunc.onefunc (0, Rat.neg(FuncUtil.Ctermfunc.apply d x))
-                      else FuncUtil.Intfunc.empty
+       val inp =
+        if FuncUtil.Ctermfunc.defined d x
+        then FuncUtil.Intfunc.onefunc (0, ~ (FuncUtil.Ctermfunc.apply d x))
+        else FuncUtil.Intfunc.empty
in fold_rev (fn (f,v) => fn g => if FuncUtil.Ctermfunc.defined f x then FuncUtil.Intfunc.update (v, FuncUtil.Ctermfunc.apply f x) g else g) srccombs inp
end
val equations = map coefficients vvs```
```--- a/src/HOL/Tools/groebner.ML	Wed Jun 01 17:46:12 2016 +0200
+++ b/src/HOL/Tools/groebner.ML	Wed Jun 01 19:23:18 2016 +0200
@@ -32,7 +32,6 @@
if is_binop ct ct' then Thm.dest_binop ct'
else raise CTERM ("dest_binary: bad binop", [ct, ct'])

-val minus_rat = Rat.neg;
val denominator_rat = Rat.dest #> snd #> Rat.of_int;
fun int_of_rat a =
case Rat.dest a of (i,1) => i | _ => error "int_of_rat: not an int";
@@ -70,7 +69,7 @@

(* Arithmetic on canonical polynomials. *)

-fun grob_neg l = map (fn (c,m) => (minus_rat c,m)) l;
+fun grob_neg l = map (fn (c,m) => (Rat.neg c,m)) l;

case (l1,l2) of
@@ -131,8 +130,8 @@
case pol of
[] => error "reduce1"
| cm1::cms => ((let val (c,m) = mdiv cm cm1 in
-                    (grob_cmul (minus_rat c,m) cms,
-                     Mmul((minus_rat c,m),hpol)) end)
+                    (grob_cmul (~ c, m) cms,
+                     Mmul ((~ c,m),hpol)) end)
handle  ERROR _ => error "reduce1");

(* Try this for all polynomials in a basis.  *)
@@ -169,7 +168,7 @@
(grob_sub (grob_cmul (mdiv cm cm1) ptl1)
(grob_cmul (mdiv cm cm2) ptl2),
-             Mmul(mdiv (minus_rat(fst cm),snd cm) cm2,his2)));
+             Mmul(mdiv (~ (fst cm),snd cm) cm2,his2)));

(* Make a polynomial monic.                                                  *)

@@ -711,7 +710,7 @@
in (vars,l,cert,th2)
end)
val cert_pos = map (fn (i,p) => (i,filter (fn (c,_) => c > @0) p)) cert
-    val cert_neg = map (fn (i,p) => (i,map (fn (c,m) => (minus_rat c,m))
+    val cert_neg = map (fn (i,p) => (i,map (fn (c,m) => (~ c,m))
(filter (fn (c,_) => c < @0) p))) cert
val  herts_pos = map (fn (i,p) => (i,holify_polynomial vars p)) cert_pos
val  herts_neg = map (fn (i,p) => (i,holify_polynomial vars p)) cert_neg```
```--- a/src/HOL/Tools/lin_arith.ML	Wed Jun 01 17:46:12 2016 +0200
+++ b/src/HOL/Tools/lin_arith.ML	Wed Jun 01 19:23:18 2016 +0200
@@ -171,7 +171,7 @@
end
else (SOME atom, m)
(* terms that evaluate to numeric constants *)
-    | demult (Const (@{const_name Groups.uminus}, _) \$ t, m) = demult (t, Rat.neg m)
+    | demult (Const (@{const_name Groups.uminus}, _) \$ t, m) = demult (t, ~ m)
| demult (Const (@{const_name Groups.zero}, _), _) = (NONE, @0)
| demult (Const (@{const_name Groups.one}, _), m) = (NONE, m)
(*Warning: in rare cases (neg_)numeral encloses a non-numeral,
@@ -200,9 +200,9 @@
fun poly (Const (@{const_name Groups.plus}, _) \$ s \$ t,
m : Rat.rat, pi : (term * Rat.rat) list * Rat.rat) = poly (s, m, poly (t, m, pi))
| poly (all as Const (@{const_name Groups.minus}, T) \$ s \$ t, m, pi) =
-        if nT T then add_atom all m pi else poly (s, m, poly (t, Rat.neg m, pi))
+        if nT T then add_atom all m pi else poly (s, m, poly (t, ~ m, pi))
| poly (all as Const (@{const_name Groups.uminus}, T) \$ t, m, pi) =
-        if nT T then add_atom all m pi else poly (t, Rat.neg m, pi)
+        if nT T then add_atom all m pi else poly (t, ~ m, pi)
| poly (Const (@{const_name Groups.zero}, _), _, pi) =
pi
| poly (Const (@{const_name Groups.one}, _), m, (p, i)) =```
```--- a/src/Pure/General/rat.ML	Wed Jun 01 17:46:12 2016 +0200
+++ b/src/Pure/General/rat.ML	Wed Jun 01 19:23:18 2016 +0200
@@ -13,7 +13,6 @@
val dest: rat -> int * int
val string_of_rat: rat -> string
val signed_string_of_rat: rat -> string
-  val eq: rat * rat -> bool
val ord: rat * rat -> order
val le: rat -> rat -> bool
val lt: rat -> rat -> bool
@@ -36,7 +35,7 @@
let val m = PolyML.IntInf.lcm (q1, q2)
in ((p1 * (m div q1), p2 * (m div q2)), m) end;

-fun make (p, 0) = raise Div
+fun make (_, 0) = raise Div
| make (p, q) =
let
val m = PolyML.IntInf.gcd (p, q);
@@ -53,8 +52,6 @@
fun signed_string_of_rat (Rat (p, 1)) = signed_string_of_int p
| signed_string_of_rat (Rat (p, q)) = signed_string_of_int p ^ "/" ^ string_of_int q;

-fun eq (Rat (p1, q1), Rat (p2, q2)) = (p1 = p2 andalso q1 = q2);
-
fun ord (Rat (p1, q1), Rat (p2, q2)) =
(case (Integer.sign p1, Integer.sign p2) of
(LESS, EQUAL) => LESS
@@ -66,12 +63,12 @@
| (GREATER, EQUAL) => GREATER
| _ => int_ord (fst (common (p1, q1) (p2, q2))));

-fun le a b = not (ord (a, b) = GREATER);
+fun le a b = ord (a, b) <> GREATER;
fun lt a b = ord (a, b) = LESS;

fun sign (Rat (p, _)) = Integer.sign p;

-fun abs (Rat (p, q)) = Rat (Int.abs p, q);
+fun abs (r as Rat (p, q)) = if p < 0 then Rat (~ p, q) else r;

fun add (Rat (p1, q1)) (Rat (p2, q2)) =
let val ((m1, m2), n) = common (p1, q1) (p2, q2)
@@ -100,11 +97,11 @@