more adhoc overloading;
authorwenzelm
Wed Jun 01 19:23:18 2016 +0200 (2016-06-01)
changeset 632110bec0d1d9998
parent 63210 a0685d2b420b
child 63212 cc9c1f6a6b88
more adhoc overloading;
eliminated pointless Rat.eq: this is an equality type;
tuned;
NEWS
src/HOL/Library/Sum_of_Squares/sum_of_squares.ML
src/HOL/Library/positivstellensatz.ML
src/HOL/Multivariate_Analysis/normarith.ML
src/HOL/Tools/groebner.ML
src/HOL/Tools/lin_arith.ML
src/Pure/General/rat.ML
     1.1 --- a/NEWS	Wed Jun 01 17:46:12 2016 +0200
     1.2 +++ b/NEWS	Wed Jun 01 19:23:18 2016 +0200
     1.3 @@ -348,7 +348,7 @@
     1.4  *** ML ***
     1.5  
     1.6  * Ad-hoc overloading for standard operations on type Rat.rat: + - * / =
     1.7 -< <= > >= <>. INCOMPATIBILITY, need to use + instead of +/ etc.
     1.8 +< <= > >= <> ~ abs. INCOMPATIBILITY, need to use + instead of +/ etc.
     1.9  
    1.10  * The ML function "ML" provides easy access to run-time compilation.
    1.11  This is particularly useful for conditional compilation, without
     2.1 --- a/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML	Wed Jun 01 17:46:12 2016 +0200
     2.2 +++ b/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML	Wed Jun 01 19:23:18 2016 +0200
     2.3 @@ -41,16 +41,12 @@
     2.4  
     2.5  fun round_rat r =
     2.6    let
     2.7 -    val (a,b) = Rat.dest (Rat.abs r)
     2.8 +    val (a,b) = Rat.dest (abs r)
     2.9      val d = a div b
    2.10 -    val s = if r < @0 then (Rat.neg o Rat.of_int) else Rat.of_int
    2.11 +    val s = if r < @0 then ~ o Rat.of_int else Rat.of_int
    2.12      val x2 = 2 * (a - (b * d))
    2.13    in s (if x2 >= b then d + 1 else d) end
    2.14  
    2.15 -val abs_rat = Rat.abs;
    2.16 -val pow2 = rat_pow @2;
    2.17 -val pow10 = rat_pow @10;
    2.18 -
    2.19  
    2.20  val trace = Attrib.setup_config_bool @{binding sos_trace} (K false);
    2.21  val debug = Attrib.setup_config_bool @{binding sos_debug} (K false);
    2.22 @@ -74,8 +70,8 @@
    2.23  local
    2.24  
    2.25  fun normalize y =
    2.26 -  if abs_rat y < @1/10 then normalize (@10 * y) - 1
    2.27 -  else if abs_rat y >= @1 then normalize (y / @10) + 1
    2.28 +  if abs y < @1/10 then normalize (@10 * y) - 1
    2.29 +  else if abs y >= @1 then normalize (y / @10) + 1
    2.30    else 0
    2.31  
    2.32  in
    2.33 @@ -84,10 +80,10 @@
    2.34    if x = @0 then "0.0"
    2.35    else
    2.36      let
    2.37 -      val y = Rat.abs x
    2.38 +      val y = abs x
    2.39        val e = normalize y
    2.40 -      val z = pow10(~ e) * y + @1
    2.41 -      val k = int_of_rat (round_rat(pow10 d * z))
    2.42 +      val z = rat_pow @10 (~ e) * y + @1
    2.43 +      val k = int_of_rat (round_rat (rat_pow @10 d * z))
    2.44      in
    2.45        (if x < @0 then "-0." else "0.") ^
    2.46        implode (tl (raw_explode(string_of_int k))) ^
    2.47 @@ -182,7 +178,7 @@
    2.48    if c = @0 then poly_0
    2.49    else FuncUtil.Monomialfunc.map (fn _ => fn x => c * x) p;
    2.50  
    2.51 -fun poly_neg p = FuncUtil.Monomialfunc.map (K Rat.neg) p;
    2.52 +fun poly_neg p = FuncUtil.Monomialfunc.map (K ~) p;
    2.53  
    2.54  
    2.55  fun poly_add p1 p2 =
    2.56 @@ -319,7 +315,7 @@
    2.57  val numeral = Scan.one isnum
    2.58  val decimalint = Scan.repeat1 numeral >> (rat_of_string o implode)
    2.59  val decimalfrac = Scan.repeat1 numeral
    2.60 -  >> (fn s => rat_of_string(implode s) / pow10 (length s))
    2.61 +  >> (fn s => rat_of_string(implode s) / rat_pow @10 (length s))
    2.62  val decimalsig =
    2.63    decimalint -- Scan.option (Scan.$$ "." |-- decimalfrac)
    2.64    >> (fn (h,NONE) => h | (h,SOME x) => h + x)
    2.65 @@ -333,7 +329,7 @@
    2.66  val exponent = ($$ "e" || $$ "E") |-- signed decimalint;
    2.67  
    2.68  val decimal = signed decimalsig -- (emptyin @0|| exponent)
    2.69 -  >> (fn (h, x) => h * pow10 (int_of_rat x));
    2.70 +  >> (fn (h, x) => h * rat_pow @10 (int_of_rat x));
    2.71  
    2.72  fun mkparser p s =
    2.73    let val (x,rst) = p (raw_explode s)
    2.74 @@ -359,7 +355,7 @@
    2.75    fun common_denominator fld amat acc =
    2.76      fld (fn (_,c) => fn a => lcm_rat (denominator_rat c) a) amat acc
    2.77    fun maximal_element fld amat acc =
    2.78 -    fld (fn (_,c) => fn maxa => max_rat maxa (abs_rat c)) amat acc
    2.79 +    fld (fn (_,c) => fn maxa => max_rat maxa (abs c)) amat acc
    2.80    fun float_of_rat x =
    2.81      let val (a,b) = Rat.dest x
    2.82      in Real.fromInt a / Real.fromInt b end;
    2.83 @@ -374,8 +370,8 @@
    2.84      val obj' = vector_cmul cd2 obj
    2.85      val max1 = fold_rev (maximal_element Inttriplefunc.fold) mats' @0
    2.86      val max2 = maximal_element FuncUtil.Intfunc.fold (snd obj') @0
    2.87 -    val scal1 = pow2 (20 - int_of_float(Math.ln (float_of_rat max1) / Math.ln 2.0))
    2.88 -    val scal2 = pow2 (20 - int_of_float(Math.ln (float_of_rat max2) / Math.ln 2.0))
    2.89 +    val scal1 = rat_pow @2 (20 - int_of_float(Math.ln (float_of_rat max1) / Math.ln 2.0))
    2.90 +    val scal2 = rat_pow @2 (20 - int_of_float(Math.ln (float_of_rat max2) / Math.ln 2.0))
    2.91      val mats'' = map (Inttriplefunc.map (fn _ => fn x => x * scal1)) mats'
    2.92      val obj'' = vector_cmul scal2 obj'
    2.93    in solver obj'' mats'' end
    2.94 @@ -438,7 +434,7 @@
    2.95                fun elim e =
    2.96                  let val b = Inttriplefunc.tryapplyd e v @0 in
    2.97                    if b = @0 then e
    2.98 -                  else tri_equation_add e (tri_equation_cmul (Rat.neg b / a) eq)
    2.99 +                  else tri_equation_add e (tri_equation_cmul (~ b / a) eq)
   2.100                  end
   2.101              in
   2.102                eliminate (Inttriplefunc.update(v, eq') (Inttriplefunc.map (K elim) dun))
   2.103 @@ -559,7 +555,7 @@
   2.104  
   2.105  fun epoly_of_poly p =
   2.106    FuncUtil.Monomialfunc.fold (fn (m, c) => fn a =>
   2.107 -      FuncUtil.Monomialfunc.update (m, Inttriplefunc.onefunc ((0, 0, 0), Rat.neg c)) a)
   2.108 +      FuncUtil.Monomialfunc.update (m, Inttriplefunc.onefunc ((0, 0, 0), ~ c)) a)
   2.109      p FuncUtil.Monomialfunc.empty;
   2.110  
   2.111  (* String for block diagonal matrix numbered k.                              *)
   2.112 @@ -725,7 +721,7 @@
   2.113        in (vec, map diag allmats) end
   2.114      val (vec, ratdias) =
   2.115        if null pvs then find_rounding @1
   2.116 -      else tryfind find_rounding (map Rat.of_int (1 upto 31) @ map pow2 (5 upto 66))
   2.117 +      else tryfind find_rounding (map Rat.of_int (1 upto 31) @ map (rat_pow @2) (5 upto 66))
   2.118      val newassigs =
   2.119        fold_rev (fn k => Inttriplefunc.update (nth pvs (k - 1), int_element vec k))
   2.120          (1 upto dim vec) (Inttriplefunc.onefunc ((0, 0, 0), Rat.of_int ~1))
     3.1 --- a/src/HOL/Library/positivstellensatz.ML	Wed Jun 01 17:46:12 2016 +0200
     3.2 +++ b/src/HOL/Library/positivstellensatz.ML	Wed Jun 01 19:23:18 2016 +0200
     3.3 @@ -615,10 +615,10 @@
     3.4               in
     3.5                 if c1 * c2 >= @0 then acc else
     3.6                 let
     3.7 -                 val e1' = linear_cmul (Rat.abs c2) e1
     3.8 -                 val e2' = linear_cmul (Rat.abs c1) e2
     3.9 -                 val p1' = Product(Rational_lt(Rat.abs c2),p1)
    3.10 -                 val p2' = Product(Rational_lt(Rat.abs c1),p2)
    3.11 +                 val e1' = linear_cmul (abs c2) e1
    3.12 +                 val e2' = linear_cmul (abs c1) e2
    3.13 +                 val p1' = Product(Rational_lt (abs c2), p1)
    3.14 +                 val p2' = Product(Rational_lt (abs c1), p2)
    3.15                 in (linear_add e1' e2',Sum(p1',p2'))::acc
    3.16                 end
    3.17               end
    3.18 @@ -653,11 +653,11 @@
    3.19               let val d = FuncUtil.Ctermfunc.tryapplyd t x @0 in
    3.20                 if d = @0 then inp else
    3.21                 let
    3.22 -                 val k = (Rat.neg d) * Rat.abs c / c
    3.23 +                 val k = ~ d * abs c / c
    3.24                   val e' = linear_cmul k e
    3.25 -                 val t' = linear_cmul (Rat.abs c) t
    3.26 +                 val t' = linear_cmul (abs c) t
    3.27                   val p' = Eqmul(FuncUtil.Monomialfunc.onefunc (FuncUtil.Ctermfunc.empty, k),p)
    3.28 -                 val q' = Product(Rational_lt(Rat.abs c),q)
    3.29 +                 val q' = Product(Rational_lt (abs c), q)
    3.30                 in (linear_add e' t',Sum(p',q'))
    3.31                 end
    3.32               end
     4.1 --- a/src/HOL/Multivariate_Analysis/normarith.ML	Wed Jun 01 17:46:12 2016 +0200
     4.2 +++ b/src/HOL/Multivariate_Analysis/normarith.ML	Wed Jun 01 19:23:18 2016 +0200
     4.3 @@ -32,7 +32,7 @@
     4.4                        (Thm.dest_arg t) acc
     4.5        | _ => augment_norm true t acc
     4.6  
     4.7 - val cterm_lincomb_neg = FuncUtil.Ctermfunc.map (K Rat.neg)
     4.8 + val cterm_lincomb_neg = FuncUtil.Ctermfunc.map (K ~)
     4.9   fun cterm_lincomb_cmul c t =
    4.10      if c = @0 then FuncUtil.Ctermfunc.empty else FuncUtil.Ctermfunc.map (fn _ => fn x => x * c) t
    4.11   fun cterm_lincomb_add l r = FuncUtil.Ctermfunc.combine (curry op +) (fn x => x = @0) l r
    4.12 @@ -40,7 +40,7 @@
    4.13   fun cterm_lincomb_eq l r = FuncUtil.Ctermfunc.is_empty (cterm_lincomb_sub l r)
    4.14  
    4.15  (*
    4.16 - val int_lincomb_neg = FuncUtil.Intfunc.map (K Rat.neg)
    4.17 + val int_lincomb_neg = FuncUtil.Intfunc.map (K ~)
    4.18  *)
    4.19   fun int_lincomb_cmul c t =
    4.20      if c = @0 then FuncUtil.Intfunc.empty else FuncUtil.Intfunc.map (fn _ => fn x => x * c) t
    4.21 @@ -89,7 +89,7 @@
    4.22  (*
    4.23  fun flip v eq =
    4.24    if FuncUtil.Ctermfunc.defined eq v
    4.25 -  then FuncUtil.Ctermfunc.update (v, Rat.neg (FuncUtil.Ctermfunc.apply eq v)) eq else eq
    4.26 +  then FuncUtil.Ctermfunc.update (v, ~ (FuncUtil.Ctermfunc.apply eq v)) eq else eq
    4.27  *)
    4.28  fun allsubsets s = case s of
    4.29    [] => [[]]
    4.30 @@ -109,7 +109,7 @@
    4.31         then
    4.32          let
    4.33           val c = FuncUtil.Intfunc.apply eq v
    4.34 -         val vdef = int_lincomb_cmul (Rat.neg (Rat.inv c)) eq
    4.35 +         val vdef = int_lincomb_cmul (~ (Rat.inv c)) eq
    4.36           fun eliminate eqn = if not (FuncUtil.Intfunc.defined eqn v) then eqn
    4.37                               else int_lincomb_add (int_lincomb_cmul (FuncUtil.Intfunc.apply eqn v) vdef) eqn
    4.38          in (case solve (remove (op =) v vs, map eliminate oeqs) of
    4.39 @@ -254,7 +254,7 @@
    4.40  
    4.41  fun int_flip v eq =
    4.42    if FuncUtil.Intfunc.defined eq v
    4.43 -  then FuncUtil.Intfunc.update (v, Rat.neg (FuncUtil.Intfunc.apply eq v)) eq else eq;
    4.44 +  then FuncUtil.Intfunc.update (v, ~ (FuncUtil.Intfunc.apply eq v)) eq else eq;
    4.45  
    4.46  local
    4.47   val pth_zero = @{thm norm_zero}
    4.48 @@ -283,8 +283,10 @@
    4.49      let
    4.50       fun coefficients x =
    4.51        let
    4.52 -       val inp = if FuncUtil.Ctermfunc.defined d x then FuncUtil.Intfunc.onefunc (0, Rat.neg(FuncUtil.Ctermfunc.apply d x))
    4.53 -                      else FuncUtil.Intfunc.empty
    4.54 +       val inp =
    4.55 +        if FuncUtil.Ctermfunc.defined d x
    4.56 +        then FuncUtil.Intfunc.onefunc (0, ~ (FuncUtil.Ctermfunc.apply d x))
    4.57 +        else FuncUtil.Intfunc.empty
    4.58        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
    4.59        end
    4.60       val equations = map coefficients vvs
     5.1 --- a/src/HOL/Tools/groebner.ML	Wed Jun 01 17:46:12 2016 +0200
     5.2 +++ b/src/HOL/Tools/groebner.ML	Wed Jun 01 19:23:18 2016 +0200
     5.3 @@ -32,7 +32,6 @@
     5.4    if is_binop ct ct' then Thm.dest_binop ct'
     5.5    else raise CTERM ("dest_binary: bad binop", [ct, ct'])
     5.6  
     5.7 -val minus_rat = Rat.neg;
     5.8  val denominator_rat = Rat.dest #> snd #> Rat.of_int;
     5.9  fun int_of_rat a =
    5.10      case Rat.dest a of (i,1) => i | _ => error "int_of_rat: not an int";
    5.11 @@ -70,7 +69,7 @@
    5.12  
    5.13  (* Arithmetic on canonical polynomials. *)
    5.14  
    5.15 -fun grob_neg l = map (fn (c,m) => (minus_rat c,m)) l;
    5.16 +fun grob_neg l = map (fn (c,m) => (Rat.neg c,m)) l;
    5.17  
    5.18  fun grob_add l1 l2 =
    5.19    case (l1,l2) of
    5.20 @@ -131,8 +130,8 @@
    5.21    case pol of
    5.22      [] => error "reduce1"
    5.23    | cm1::cms => ((let val (c,m) = mdiv cm cm1 in
    5.24 -                    (grob_cmul (minus_rat c,m) cms,
    5.25 -                     Mmul((minus_rat c,m),hpol)) end)
    5.26 +                    (grob_cmul (~ c, m) cms,
    5.27 +                     Mmul ((~ c,m),hpol)) end)
    5.28                  handle  ERROR _ => error "reduce1");
    5.29  
    5.30  (* Try this for all polynomials in a basis.  *)
    5.31 @@ -169,7 +168,7 @@
    5.32          (grob_sub (grob_cmul (mdiv cm cm1) ptl1)
    5.33                    (grob_cmul (mdiv cm cm2) ptl2),
    5.34           Add(Mmul(mdiv cm cm1,his1),
    5.35 -             Mmul(mdiv (minus_rat(fst cm),snd cm) cm2,his2)));
    5.36 +             Mmul(mdiv (~ (fst cm),snd cm) cm2,his2)));
    5.37  
    5.38  (* Make a polynomial monic.                                                  *)
    5.39  
    5.40 @@ -711,7 +710,7 @@
    5.41        in (vars,l,cert,th2)
    5.42        end)
    5.43      val cert_pos = map (fn (i,p) => (i,filter (fn (c,_) => c > @0) p)) cert
    5.44 -    val cert_neg = map (fn (i,p) => (i,map (fn (c,m) => (minus_rat c,m))
    5.45 +    val cert_neg = map (fn (i,p) => (i,map (fn (c,m) => (~ c,m))
    5.46                                              (filter (fn (c,_) => c < @0) p))) cert
    5.47      val  herts_pos = map (fn (i,p) => (i,holify_polynomial vars p)) cert_pos
    5.48      val  herts_neg = map (fn (i,p) => (i,holify_polynomial vars p)) cert_neg
     6.1 --- a/src/HOL/Tools/lin_arith.ML	Wed Jun 01 17:46:12 2016 +0200
     6.2 +++ b/src/HOL/Tools/lin_arith.ML	Wed Jun 01 19:23:18 2016 +0200
     6.3 @@ -171,7 +171,7 @@
     6.4          end
     6.5        else (SOME atom, m)
     6.6      (* terms that evaluate to numeric constants *)
     6.7 -    | demult (Const (@{const_name Groups.uminus}, _) $ t, m) = demult (t, Rat.neg m)
     6.8 +    | demult (Const (@{const_name Groups.uminus}, _) $ t, m) = demult (t, ~ m)
     6.9      | demult (Const (@{const_name Groups.zero}, _), _) = (NONE, @0)
    6.10      | demult (Const (@{const_name Groups.one}, _), m) = (NONE, m)
    6.11      (*Warning: in rare cases (neg_)numeral encloses a non-numeral,
    6.12 @@ -200,9 +200,9 @@
    6.13    fun poly (Const (@{const_name Groups.plus}, _) $ s $ t,
    6.14          m : Rat.rat, pi : (term * Rat.rat) list * Rat.rat) = poly (s, m, poly (t, m, pi))
    6.15      | poly (all as Const (@{const_name Groups.minus}, T) $ s $ t, m, pi) =
    6.16 -        if nT T then add_atom all m pi else poly (s, m, poly (t, Rat.neg m, pi))
    6.17 +        if nT T then add_atom all m pi else poly (s, m, poly (t, ~ m, pi))
    6.18      | poly (all as Const (@{const_name Groups.uminus}, T) $ t, m, pi) =
    6.19 -        if nT T then add_atom all m pi else poly (t, Rat.neg m, pi)
    6.20 +        if nT T then add_atom all m pi else poly (t, ~ m, pi)
    6.21      | poly (Const (@{const_name Groups.zero}, _), _, pi) =
    6.22          pi
    6.23      | poly (Const (@{const_name Groups.one}, _), m, (p, i)) =
     7.1 --- a/src/Pure/General/rat.ML	Wed Jun 01 17:46:12 2016 +0200
     7.2 +++ b/src/Pure/General/rat.ML	Wed Jun 01 19:23:18 2016 +0200
     7.3 @@ -13,7 +13,6 @@
     7.4    val dest: rat -> int * int
     7.5    val string_of_rat: rat -> string
     7.6    val signed_string_of_rat: rat -> string
     7.7 -  val eq: rat * rat -> bool
     7.8    val ord: rat * rat -> order
     7.9    val le: rat -> rat -> bool
    7.10    val lt: rat -> rat -> bool
    7.11 @@ -36,7 +35,7 @@
    7.12    let val m = PolyML.IntInf.lcm (q1, q2)
    7.13    in ((p1 * (m div q1), p2 * (m div q2)), m) end;
    7.14  
    7.15 -fun make (p, 0) = raise Div
    7.16 +fun make (_, 0) = raise Div
    7.17    | make (p, q) =
    7.18      let
    7.19        val m = PolyML.IntInf.gcd (p, q);
    7.20 @@ -53,8 +52,6 @@
    7.21  fun signed_string_of_rat (Rat (p, 1)) = signed_string_of_int p
    7.22    | signed_string_of_rat (Rat (p, q)) = signed_string_of_int p ^ "/" ^ string_of_int q;
    7.23  
    7.24 -fun eq (Rat (p1, q1), Rat (p2, q2)) = (p1 = p2 andalso q1 = q2);
    7.25 -
    7.26  fun ord (Rat (p1, q1), Rat (p2, q2)) =
    7.27    (case (Integer.sign p1, Integer.sign p2) of
    7.28      (LESS, EQUAL) => LESS
    7.29 @@ -66,12 +63,12 @@
    7.30    | (GREATER, EQUAL) => GREATER
    7.31    | _ => int_ord (fst (common (p1, q1) (p2, q2))));
    7.32  
    7.33 -fun le a b = not (ord (a, b) = GREATER);
    7.34 +fun le a b = ord (a, b) <> GREATER;
    7.35  fun lt a b = ord (a, b) = LESS;
    7.36  
    7.37  fun sign (Rat (p, _)) = Integer.sign p;
    7.38  
    7.39 -fun abs (Rat (p, q)) = Rat (Int.abs p, q);
    7.40 +fun abs (r as Rat (p, q)) = if p < 0 then Rat (~ p, q) else r;
    7.41  
    7.42  fun add (Rat (p1, q1)) (Rat (p2, q2)) =
    7.43    let val ((m1, m2), n) = common (p1, q1) (p2, q2)
    7.44 @@ -100,11 +97,11 @@
    7.45  ML_system_overload (fn (a, b) => Rat.add a (Rat.neg b)) "-";
    7.46  ML_system_overload (uncurry Rat.mult) "*";
    7.47  ML_system_overload (fn (a, b) => Rat.mult a (Rat.inv b)) "/";
    7.48 -ML_system_overload Rat.eq "=";
    7.49  ML_system_overload (uncurry Rat.lt) "<";
    7.50  ML_system_overload (uncurry Rat.le) "<=";
    7.51  ML_system_overload (fn (a, b) => Rat.lt b a) ">";
    7.52  ML_system_overload (fn (a, b) => Rat.le b a) ">=";
    7.53 -ML_system_overload (not o Rat.eq) "<>";
    7.54 +ML_system_overload Rat.neg "~";
    7.55 +ML_system_overload Rat.abs "abs";
    7.56  
    7.57  ML_system_pp (fn _ => fn _ => fn x => Pretty.to_polyml (Pretty.str ("@" ^ Rat.string_of_rat x)));