ad-hoc overloading for standard operations on type Rat.rat;
authorwenzelm
Tue May 31 21:54:10 2016 +0200 (2016-05-31)
changeset 63198c583ca33076a
parent 63197 af562e976038
child 63199 da38571dd5bd
ad-hoc overloading for standard operations on type Rat.rat;
NEWS
src/HOL/Decision_Procs/Dense_Linear_Order.thy
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/Pure/General/rat.ML
     1.1 --- a/NEWS	Tue May 31 19:51:01 2016 +0200
     1.2 +++ b/NEWS	Tue May 31 21:54:10 2016 +0200
     1.3 @@ -344,8 +344,12 @@
     1.4    nn_integral :: 'a measure => ('a => ennreal) => ennreal
     1.5  INCOMPATIBILITY.
     1.6  
     1.7 +
     1.8  *** ML ***
     1.9  
    1.10 +* Ad-hoc overloading for standard operations on type Rat.rat: + - * / =
    1.11 +< <= > >= <>. INCOMPATIBILITY, need to use + instead of +/ etc.
    1.12 +
    1.13  * The ML function "ML" provides easy access to run-time compilation.
    1.14  This is particularly useful for conditional compilation, without
    1.15  requiring separate files.
     2.1 --- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Tue May 31 19:51:01 2016 +0200
     2.2 +++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Tue May 31 21:54:10 2016 +0200
     2.3 @@ -923,7 +923,7 @@
     2.4          val cr = dest_frac c
     2.5          val clt = Thm.dest_fun2 ct
     2.6          val cz = Thm.dest_arg ct
     2.7 -        val neg = cr </ Rat.zero
     2.8 +        val neg = cr < Rat.zero
     2.9          val cthp = Simplifier.rewrite ctxt
    2.10                 (Thm.apply @{cterm "Trueprop"}
    2.11                    (if neg then Thm.apply (Thm.apply clt c) cz
    2.12 @@ -946,7 +946,7 @@
    2.13          val cr = dest_frac c
    2.14          val clt = Thm.dest_fun2 ct
    2.15          val cz = Thm.dest_arg ct
    2.16 -        val neg = cr </ Rat.zero
    2.17 +        val neg = cr < Rat.zero
    2.18          val cthp = Simplifier.rewrite ctxt
    2.19                 (Thm.apply @{cterm "Trueprop"}
    2.20                    (if neg then Thm.apply (Thm.apply clt c) cz
    2.21 @@ -968,7 +968,7 @@
    2.22          val cr = dest_frac c
    2.23          val clt = Thm.cterm_of ctxt (Const (@{const_name ord_class.less}, T --> T --> @{typ bool}))
    2.24          val cz = Thm.dest_arg ct
    2.25 -        val neg = cr </ Rat.zero
    2.26 +        val neg = cr < Rat.zero
    2.27          val cthp = Simplifier.rewrite ctxt
    2.28                 (Thm.apply @{cterm "Trueprop"}
    2.29                    (if neg then Thm.apply (Thm.apply clt c) cz
    2.30 @@ -993,7 +993,7 @@
    2.31          val cr = dest_frac c
    2.32          val clt = Thm.cterm_of ctxt (Const (@{const_name ord_class.less}, T --> T --> @{typ bool}))
    2.33          val cz = Thm.dest_arg ct
    2.34 -        val neg = cr </ Rat.zero
    2.35 +        val neg = cr < Rat.zero
    2.36          val cthp = Simplifier.rewrite ctxt
    2.37                 (Thm.apply @{cterm "Trueprop"}
    2.38                    (if neg then Thm.apply (Thm.apply clt c) cz
     3.1 --- a/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML	Tue May 31 19:51:01 2016 +0200
     3.2 +++ b/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML	Tue May 31 21:54:10 2016 +0200
     3.3 @@ -39,7 +39,7 @@
     3.4   let fun pow r i =
     3.5     if i = 0 then rat_1 else
     3.6     let val d = pow r (i div 2)
     3.7 -   in d */ d */ (if i mod 2 = 0 then rat_1 else r)
     3.8 +   in d * d * (if i mod 2 = 0 then rat_1 else r)
     3.9     end
    3.10   in if i < 0 then pow (Rat.inv r) (~ i) else pow r i end;
    3.11  
    3.12 @@ -47,7 +47,7 @@
    3.13    let
    3.14      val (a,b) = Rat.quotient_of_rat (Rat.abs r)
    3.15      val d = a div b
    3.16 -    val s = if r </ rat_0 then (Rat.neg o Rat.rat_of_int) else Rat.rat_of_int
    3.17 +    val s = if r < rat_0 then (Rat.neg o Rat.rat_of_int) else Rat.rat_of_int
    3.18      val x2 = 2 * (a - (b * d))
    3.19    in s (if x2 >= b then d + 1 else d) end
    3.20  
    3.21 @@ -78,22 +78,22 @@
    3.22  local
    3.23  
    3.24  fun normalize y =
    3.25 -  if abs_rat y </ (rat_1 // rat_10) then normalize (rat_10 */ y) - 1
    3.26 -  else if abs_rat y >=/ rat_1 then normalize (y // rat_10) + 1
    3.27 +  if abs_rat y < (rat_1 / rat_10) then normalize (rat_10 * y) - 1
    3.28 +  else if abs_rat y >= rat_1 then normalize (y / rat_10) + 1
    3.29    else 0
    3.30  
    3.31  in
    3.32  
    3.33  fun decimalize d x =
    3.34 -  if x =/ rat_0 then "0.0"
    3.35 +  if x = rat_0 then "0.0"
    3.36    else
    3.37      let
    3.38        val y = Rat.abs x
    3.39        val e = normalize y
    3.40 -      val z = pow10(~ e) */ y +/ rat_1
    3.41 -      val k = int_of_rat (round_rat(pow10 d */ z))
    3.42 +      val z = pow10(~ e) * y + rat_1
    3.43 +      val k = int_of_rat (round_rat(pow10 d * z))
    3.44      in
    3.45 -      (if x </ rat_0 then "-0." else "0.") ^
    3.46 +      (if x < rat_0 then "-0." else "0.") ^
    3.47        implode (tl (raw_explode(string_of_int k))) ^
    3.48        (if e = 0 then "" else "e" ^ string_of_int e)
    3.49      end
    3.50 @@ -117,7 +117,7 @@
    3.51  
    3.52  type matrix = (int * int) * Rat.rat FuncUtil.Intpairfunc.table;
    3.53  
    3.54 -fun iszero (_, r) = r =/ rat_0;
    3.55 +fun iszero (_, r) = r = rat_0;
    3.56  
    3.57  
    3.58  (* Vectors. Conventionally indexed 1..n.                                     *)
    3.59 @@ -128,8 +128,8 @@
    3.60  
    3.61  fun vector_cmul c (v: vector) =
    3.62    let val n = dim v in
    3.63 -    if c =/ rat_0 then vector_0 n
    3.64 -    else (n,FuncUtil.Intfunc.map (fn _ => fn x => c */ x) (snd v))
    3.65 +    if c = rat_0 then vector_0 n
    3.66 +    else (n,FuncUtil.Intfunc.map (fn _ => fn x => c * x) (snd v))
    3.67    end;
    3.68  
    3.69  fun vector_of_list l =
    3.70 @@ -151,7 +151,7 @@
    3.71  (* Monomials.                                                                *)
    3.72  
    3.73  fun monomial_eval assig m =
    3.74 -  FuncUtil.Ctermfunc.fold (fn (x, k) => fn a => a */ rat_pow (FuncUtil.Ctermfunc.apply assig x) k)
    3.75 +  FuncUtil.Ctermfunc.fold (fn (x, k) => fn a => a * rat_pow (FuncUtil.Ctermfunc.apply assig x) k)
    3.76      m rat_1;
    3.77  
    3.78  val monomial_1 = FuncUtil.Ctermfunc.empty;
    3.79 @@ -169,7 +169,7 @@
    3.80  (* Polynomials.                                                              *)
    3.81  
    3.82  fun eval assig p =
    3.83 -  FuncUtil.Monomialfunc.fold (fn (m, c) => fn a => a +/ c */ monomial_eval assig m) p rat_0;
    3.84 +  FuncUtil.Monomialfunc.fold (fn (m, c) => fn a => a + c * monomial_eval assig m) p rat_0;
    3.85  
    3.86  val poly_0 = FuncUtil.Monomialfunc.empty;
    3.87  
    3.88 @@ -180,28 +180,28 @@
    3.89  fun poly_var x = FuncUtil.Monomialfunc.onefunc (monomial_var x, rat_1);
    3.90  
    3.91  fun poly_const c =
    3.92 -  if c =/ rat_0 then poly_0 else FuncUtil.Monomialfunc.onefunc (monomial_1, c);
    3.93 +  if c = rat_0 then poly_0 else FuncUtil.Monomialfunc.onefunc (monomial_1, c);
    3.94  
    3.95  fun poly_cmul c p =
    3.96 -  if c =/ rat_0 then poly_0
    3.97 -  else FuncUtil.Monomialfunc.map (fn _ => fn x => c */ x) p;
    3.98 +  if c = rat_0 then poly_0
    3.99 +  else FuncUtil.Monomialfunc.map (fn _ => fn x => c * x) p;
   3.100  
   3.101  fun poly_neg p = FuncUtil.Monomialfunc.map (K Rat.neg) p;
   3.102  
   3.103  
   3.104  fun poly_add p1 p2 =
   3.105 -  FuncUtil.Monomialfunc.combine (curry op +/) (fn x => x =/ rat_0) p1 p2;
   3.106 +  FuncUtil.Monomialfunc.combine (curry op +) (fn x => x = rat_0) p1 p2;
   3.107  
   3.108  fun poly_sub p1 p2 = poly_add p1 (poly_neg p2);
   3.109  
   3.110  fun poly_cmmul (c,m) p =
   3.111 -  if c =/ rat_0 then poly_0
   3.112 +  if c = rat_0 then poly_0
   3.113    else
   3.114      if FuncUtil.Ctermfunc.is_empty m
   3.115 -    then FuncUtil.Monomialfunc.map (fn _ => fn d => c */ d) p
   3.116 +    then FuncUtil.Monomialfunc.map (fn _ => fn d => c * d) p
   3.117      else
   3.118        FuncUtil.Monomialfunc.fold (fn (m', d) => fn a =>
   3.119 -          (FuncUtil.Monomialfunc.update (monomial_mul m m', c */ d) a)) p poly_0;
   3.120 +          (FuncUtil.Monomialfunc.update (monomial_mul m m', c * d) a)) p poly_0;
   3.121  
   3.122  fun poly_mul p1 p2 =
   3.123    FuncUtil.Monomialfunc.fold (fn (m, c) => fn a => poly_add (poly_cmmul (c,m) p2) a) p1 poly_0;
   3.124 @@ -323,10 +323,10 @@
   3.125  val numeral = Scan.one isnum
   3.126  val decimalint = Scan.repeat1 numeral >> (rat_of_string o implode)
   3.127  val decimalfrac = Scan.repeat1 numeral
   3.128 -  >> (fn s => rat_of_string(implode s) // pow10 (length s))
   3.129 +  >> (fn s => rat_of_string(implode s) / pow10 (length s))
   3.130  val decimalsig =
   3.131    decimalint -- Scan.option (Scan.$$ "." |-- decimalfrac)
   3.132 -  >> (fn (h,NONE) => h | (h,SOME x) => h +/ x)
   3.133 +  >> (fn (h,NONE) => h | (h,SOME x) => h + x)
   3.134  fun signed prs =
   3.135       $$ "-" |-- prs >> Rat.neg
   3.136    || $$ "+" |-- prs
   3.137 @@ -337,7 +337,7 @@
   3.138  val exponent = ($$ "e" || $$ "E") |-- signed decimalint;
   3.139  
   3.140  val decimal = signed decimalsig -- (emptyin rat_0|| exponent)
   3.141 -  >> (fn (h, x) => h */ pow10 (int_of_rat x));
   3.142 +  >> (fn (h, x) => h * pow10 (int_of_rat x));
   3.143  
   3.144  fun mkparser p s =
   3.145    let val (x,rst) = p (raw_explode s)
   3.146 @@ -359,7 +359,7 @@
   3.147  
   3.148  (* Version for (int*int*int) keys *)
   3.149  local
   3.150 -  fun max_rat x y = if x </ y then y else x
   3.151 +  fun max_rat x y = if x < y then y else x
   3.152    fun common_denominator fld amat acc =
   3.153      fld (fn (_,c) => fn a => lcm_rat (denominator_rat c) a) amat acc
   3.154    fun maximal_element fld amat acc =
   3.155 @@ -374,24 +374,24 @@
   3.156    let
   3.157      val cd1 = fold_rev (common_denominator Inttriplefunc.fold) mats (rat_1)
   3.158      val cd2 = common_denominator FuncUtil.Intfunc.fold (snd obj)  (rat_1)
   3.159 -    val mats' = map (Inttriplefunc.map (fn _ => fn x => cd1 */ x)) mats
   3.160 +    val mats' = map (Inttriplefunc.map (fn _ => fn x => cd1 * x)) mats
   3.161      val obj' = vector_cmul cd2 obj
   3.162      val max1 = fold_rev (maximal_element Inttriplefunc.fold) mats' (rat_0)
   3.163      val max2 = maximal_element FuncUtil.Intfunc.fold (snd obj') (rat_0)
   3.164      val scal1 = pow2 (20 - int_of_float(Math.ln (float_of_rat max1) / Math.ln 2.0))
   3.165      val scal2 = pow2 (20 - int_of_float(Math.ln (float_of_rat max2) / Math.ln 2.0))
   3.166 -    val mats'' = map (Inttriplefunc.map (fn _ => fn x => x */ scal1)) mats'
   3.167 +    val mats'' = map (Inttriplefunc.map (fn _ => fn x => x * scal1)) mats'
   3.168      val obj'' = vector_cmul scal2 obj'
   3.169    in solver obj'' mats'' end
   3.170  end;
   3.171  
   3.172  (* Round a vector to "nice" rationals.                                       *)
   3.173  
   3.174 -fun nice_rational n x = round_rat (n */ x) // n;
   3.175 +fun nice_rational n x = round_rat (n * x) / n;
   3.176  fun nice_vector n ((d,v) : vector) =
   3.177    (d, FuncUtil.Intfunc.fold (fn (i,c) => fn a =>
   3.178        let val y = nice_rational n c in
   3.179 -        if c =/ rat_0 then a
   3.180 +        if c = rat_0 then a
   3.181          else FuncUtil.Intfunc.update (i,y) a
   3.182        end) v FuncUtil.Intfunc.empty): vector
   3.183  
   3.184 @@ -400,16 +400,16 @@
   3.185  (* Stuff for "equations" ((int*int*int)->num functions).                         *)
   3.186  
   3.187  fun tri_equation_cmul c eq =
   3.188 -  if c =/ rat_0 then Inttriplefunc.empty
   3.189 -  else Inttriplefunc.map (fn _ => fn d => c */ d) eq;
   3.190 +  if c = rat_0 then Inttriplefunc.empty
   3.191 +  else Inttriplefunc.map (fn _ => fn d => c * d) eq;
   3.192  
   3.193  fun tri_equation_add eq1 eq2 =
   3.194 -  Inttriplefunc.combine (curry op +/) (fn x => x =/ rat_0) eq1 eq2;
   3.195 +  Inttriplefunc.combine (curry op +) (fn x => x = rat_0) eq1 eq2;
   3.196  
   3.197  fun tri_equation_eval assig eq =
   3.198    let
   3.199      fun value v = Inttriplefunc.apply assig v
   3.200 -  in Inttriplefunc.fold (fn (v, c) => fn a => a +/ value v */ c) eq rat_0 end;
   3.201 +  in Inttriplefunc.fold (fn (v, c) => fn a => a + value v * c) eq rat_0 end;
   3.202  
   3.203  (* Eliminate all variables, in an essentially arbitrary order.               *)
   3.204  
   3.205 @@ -438,11 +438,11 @@
   3.206                val v = choose_variable eq
   3.207                val a = Inttriplefunc.apply eq v
   3.208                val eq' =
   3.209 -                tri_equation_cmul ((Rat.rat_of_int ~1) // a) (Inttriplefunc.delete_safe v eq)
   3.210 +                tri_equation_cmul ((Rat.rat_of_int ~1) / a) (Inttriplefunc.delete_safe v eq)
   3.211                fun elim e =
   3.212                  let val b = Inttriplefunc.tryapplyd e v rat_0 in
   3.213 -                  if b =/ rat_0 then e
   3.214 -                  else tri_equation_add e (tri_equation_cmul (Rat.neg b // a) eq)
   3.215 +                  if b = rat_0 then e
   3.216 +                  else tri_equation_add e (tri_equation_cmul (Rat.neg b / a) eq)
   3.217                  end
   3.218              in
   3.219                eliminate (Inttriplefunc.update(v, eq') (Inttriplefunc.map (K elim) dun))
   3.220 @@ -487,8 +487,8 @@
   3.221        let
   3.222          val a11 = FuncUtil.Intpairfunc.tryapplyd (snd m) (i,i) rat_0
   3.223        in
   3.224 -        if a11 </ rat_0 then raise Failure "diagonalize: not PSD"
   3.225 -        else if a11 =/ rat_0 then
   3.226 +        if a11 < rat_0 then raise Failure "diagonalize: not PSD"
   3.227 +        else if a11 = rat_0 then
   3.228            if FuncUtil.Intfunc.is_empty (snd (row i m))
   3.229            then diagonalize n (i + 1) m
   3.230            else raise Failure "diagonalize: not PSD ___ "
   3.231 @@ -497,7 +497,7 @@
   3.232              val v = row i m
   3.233              val v' =
   3.234                (fst v, FuncUtil.Intfunc.fold (fn (i, c) => fn a =>
   3.235 -                let val y = c // a11
   3.236 +                let val y = c / a11
   3.237                  in if y = rat_0 then a else FuncUtil.Intfunc.update (i,y) a
   3.238                  end) (snd v) FuncUtil.Intfunc.empty)
   3.239              fun upt0 x y a =
   3.240 @@ -508,8 +508,8 @@
   3.241                  iter (i + 1, n) (fn j =>
   3.242                    iter (i + 1, n) (fn k =>
   3.243                      (upt0 (j, k)
   3.244 -                      (FuncUtil.Intpairfunc.tryapplyd (snd m) (j, k) rat_0 -/
   3.245 -                        FuncUtil.Intfunc.tryapplyd (snd v) j rat_0 */
   3.246 +                      (FuncUtil.Intpairfunc.tryapplyd (snd m) (j, k) rat_0 -
   3.247 +                        FuncUtil.Intfunc.tryapplyd (snd v) j rat_0 *
   3.248                          FuncUtil.Intfunc.tryapplyd (snd v') k rat_0))))
   3.249                      FuncUtil.Intpairfunc.empty)
   3.250            in (a11, v') :: diagonalize n (i + 1) m' end
   3.251 @@ -603,10 +603,10 @@
   3.252  
   3.253  (* 3D versions of matrix operations to consider blocks separately.           *)
   3.254  
   3.255 -val bmatrix_add = Inttriplefunc.combine (curry op +/) (fn x => x =/ rat_0);
   3.256 +val bmatrix_add = Inttriplefunc.combine (curry op +) (fn x => x = rat_0);
   3.257  fun bmatrix_cmul c bm =
   3.258 -  if c =/ rat_0 then Inttriplefunc.empty
   3.259 -  else Inttriplefunc.map (fn _ => fn x => c */ x) bm;
   3.260 +  if c = rat_0 then Inttriplefunc.empty
   3.261 +  else Inttriplefunc.map (fn _ => fn x => c * x) bm;
   3.262  
   3.263  val bmatrix_neg = bmatrix_cmul (Rat.rat_of_int ~1);
   3.264  
   3.265 @@ -803,13 +803,13 @@
   3.266          fun trivial_axiom (p, ax) =
   3.267            (case ax of
   3.268              RealArith.Axiom_eq n =>
   3.269 -              if eval FuncUtil.Ctermfunc.empty p <>/ Rat.zero then nth eqs n
   3.270 +              if eval FuncUtil.Ctermfunc.empty p <> Rat.zero then nth eqs n
   3.271                else raise Failure "trivial_axiom: Not a trivial axiom"
   3.272            | RealArith.Axiom_le n =>
   3.273 -              if eval FuncUtil.Ctermfunc.empty p </ Rat.zero then nth les n
   3.274 +              if eval FuncUtil.Ctermfunc.empty p < Rat.zero then nth les n
   3.275                else raise Failure "trivial_axiom: Not a trivial axiom"
   3.276            | RealArith.Axiom_lt n =>
   3.277 -              if eval FuncUtil.Ctermfunc.empty p <=/ Rat.zero then nth lts n
   3.278 +              if eval FuncUtil.Ctermfunc.empty p <= Rat.zero then nth lts n
   3.279                else raise Failure "trivial_axiom: Not a trivial axiom"
   3.280            | _ => error "trivial_axiom: Not a trivial axiom")
   3.281        in
     4.1 --- a/src/HOL/Library/positivstellensatz.ML	Tue May 31 19:51:01 2016 +0200
     4.2 +++ b/src/HOL/Library/positivstellensatz.ML	Tue May 31 21:54:10 2016 +0200
     4.3 @@ -585,27 +585,27 @@
     4.4  
     4.5  (* A linear arithmetic prover *)
     4.6  local
     4.7 -  val linear_add = FuncUtil.Ctermfunc.combine (curry op +/) (fn z => z =/ Rat.zero)
     4.8 -  fun linear_cmul c = FuncUtil.Ctermfunc.map (fn _ => fn x => c */ x)
     4.9 +  val linear_add = FuncUtil.Ctermfunc.combine (curry op +) (fn z => z = Rat.zero)
    4.10 +  fun linear_cmul c = FuncUtil.Ctermfunc.map (fn _ => fn x => c * x)
    4.11    val one_tm = @{cterm "1::real"}
    4.12    fun contradictory p (e,_) = ((FuncUtil.Ctermfunc.is_empty e) andalso not(p Rat.zero)) orelse
    4.13       ((eq_set (op aconvc) (FuncUtil.Ctermfunc.dom e, [one_tm])) andalso
    4.14         not(p(FuncUtil.Ctermfunc.apply e one_tm)))
    4.15  
    4.16    fun linear_ineqs vars (les,lts) =
    4.17 -    case find_first (contradictory (fn x => x >/ Rat.zero)) lts of
    4.18 +    case find_first (contradictory (fn x => x > Rat.zero)) lts of
    4.19        SOME r => r
    4.20      | NONE =>
    4.21 -      (case find_first (contradictory (fn x => x >/ Rat.zero)) les of
    4.22 +      (case find_first (contradictory (fn x => x > Rat.zero)) les of
    4.23           SOME r => r
    4.24         | NONE =>
    4.25           if null vars then error "linear_ineqs: no contradiction" else
    4.26           let
    4.27             val ineqs = les @ lts
    4.28             fun blowup v =
    4.29 -             length(filter (fn (e,_) => FuncUtil.Ctermfunc.tryapplyd e v Rat.zero =/ Rat.zero) ineqs) +
    4.30 -             length(filter (fn (e,_) => FuncUtil.Ctermfunc.tryapplyd e v Rat.zero >/ Rat.zero) ineqs) *
    4.31 -             length(filter (fn (e,_) => FuncUtil.Ctermfunc.tryapplyd e v Rat.zero </ Rat.zero) ineqs)
    4.32 +             length(filter (fn (e,_) => FuncUtil.Ctermfunc.tryapplyd e v Rat.zero = Rat.zero) ineqs) +
    4.33 +             length(filter (fn (e,_) => FuncUtil.Ctermfunc.tryapplyd e v Rat.zero > Rat.zero) ineqs) *
    4.34 +             length(filter (fn (e,_) => FuncUtil.Ctermfunc.tryapplyd e v Rat.zero < Rat.zero) ineqs)
    4.35             val v = fst(hd(sort (fn ((_,i),(_,j)) => int_ord (i,j))
    4.36               (map (fn v => (v,blowup v)) vars)))
    4.37             fun addup (e1,p1) (e2,p2) acc =
    4.38 @@ -613,7 +613,7 @@
    4.39                 val c1 = FuncUtil.Ctermfunc.tryapplyd e1 v Rat.zero
    4.40                 val c2 = FuncUtil.Ctermfunc.tryapplyd e2 v Rat.zero
    4.41               in
    4.42 -               if c1 */ c2 >=/ Rat.zero then acc else
    4.43 +               if c1 * c2 >= Rat.zero then acc else
    4.44                 let
    4.45                   val e1' = linear_cmul (Rat.abs c2) e1
    4.46                   val e2' = linear_cmul (Rat.abs c1) e2
    4.47 @@ -623,13 +623,13 @@
    4.48                 end
    4.49               end
    4.50             val (les0,les1) =
    4.51 -             List.partition (fn (e,_) => FuncUtil.Ctermfunc.tryapplyd e v Rat.zero =/ Rat.zero) les
    4.52 +             List.partition (fn (e,_) => FuncUtil.Ctermfunc.tryapplyd e v Rat.zero = Rat.zero) les
    4.53             val (lts0,lts1) =
    4.54 -             List.partition (fn (e,_) => FuncUtil.Ctermfunc.tryapplyd e v Rat.zero =/ Rat.zero) lts
    4.55 +             List.partition (fn (e,_) => FuncUtil.Ctermfunc.tryapplyd e v Rat.zero = Rat.zero) lts
    4.56             val (lesp,lesn) =
    4.57 -             List.partition (fn (e,_) => FuncUtil.Ctermfunc.tryapplyd e v Rat.zero >/ Rat.zero) les1
    4.58 +             List.partition (fn (e,_) => FuncUtil.Ctermfunc.tryapplyd e v Rat.zero > Rat.zero) les1
    4.59             val (ltsp,ltsn) =
    4.60 -             List.partition (fn (e,_) => FuncUtil.Ctermfunc.tryapplyd e v Rat.zero >/ Rat.zero) lts1
    4.61 +             List.partition (fn (e,_) => FuncUtil.Ctermfunc.tryapplyd e v Rat.zero > Rat.zero) lts1
    4.62             val les' = fold_rev (fn ep1 => fold_rev (addup ep1) lesp) lesn les0
    4.63             val lts' = fold_rev (fn ep1 => fold_rev (addup ep1) (lesp@ltsp)) ltsn
    4.64                        (fold_rev (fn ep1 => fold_rev (addup ep1) (lesn@ltsn)) ltsp lts0)
    4.65 @@ -637,7 +637,7 @@
    4.66           end)
    4.67  
    4.68    fun linear_eqs(eqs,les,lts) =
    4.69 -    case find_first (contradictory (fn x => x =/ Rat.zero)) eqs of
    4.70 +    case find_first (contradictory (fn x => x = Rat.zero)) eqs of
    4.71        SOME r => r
    4.72      | NONE =>
    4.73        (case eqs of
    4.74 @@ -651,9 +651,9 @@
    4.75             val (x,c) = FuncUtil.Ctermfunc.choose (FuncUtil.Ctermfunc.delete_safe one_tm e)
    4.76             fun xform (inp as (t,q)) =
    4.77               let val d = FuncUtil.Ctermfunc.tryapplyd t x Rat.zero in
    4.78 -               if d =/ Rat.zero then inp else
    4.79 +               if d = Rat.zero then inp else
    4.80                 let
    4.81 -                 val k = (Rat.neg d) */ Rat.abs c // c
    4.82 +                 val k = (Rat.neg d) * Rat.abs c / c
    4.83                   val e' = linear_cmul k e
    4.84                   val t' = linear_cmul (Rat.abs c) t
    4.85                   val p' = Eqmul(FuncUtil.Monomialfunc.onefunc (FuncUtil.Ctermfunc.empty, k),p)
     5.1 --- a/src/HOL/Multivariate_Analysis/normarith.ML	Tue May 31 19:51:01 2016 +0200
     5.2 +++ b/src/HOL/Multivariate_Analysis/normarith.ML	Tue May 31 21:54:10 2016 +0200
     5.3 @@ -28,14 +28,14 @@
     5.4              find_normedterms (Thm.dest_arg1 t) (find_normedterms (Thm.dest_arg t) acc)
     5.5        | @{term "op * :: real => _"}$_$_ =>
     5.6              if not (is_ratconst (Thm.dest_arg1 t)) then acc else
     5.7 -            augment_norm (dest_ratconst (Thm.dest_arg1 t) >=/ Rat.zero)
     5.8 +            augment_norm (dest_ratconst (Thm.dest_arg1 t) >= Rat.zero)
     5.9                        (Thm.dest_arg t) acc
    5.10        | _ => augment_norm true t acc
    5.11  
    5.12   val cterm_lincomb_neg = FuncUtil.Ctermfunc.map (K Rat.neg)
    5.13   fun cterm_lincomb_cmul c t =
    5.14 -    if c =/ Rat.zero then FuncUtil.Ctermfunc.empty else FuncUtil.Ctermfunc.map (fn _ => fn x => x */ c) t
    5.15 - fun cterm_lincomb_add l r = FuncUtil.Ctermfunc.combine (curry op +/) (fn x => x =/ Rat.zero) l r
    5.16 +    if c = Rat.zero then FuncUtil.Ctermfunc.empty else FuncUtil.Ctermfunc.map (fn _ => fn x => x * c) t
    5.17 + fun cterm_lincomb_add l r = FuncUtil.Ctermfunc.combine (curry op +) (fn x => x = Rat.zero) l r
    5.18   fun cterm_lincomb_sub l r = cterm_lincomb_add l (cterm_lincomb_neg r)
    5.19   fun cterm_lincomb_eq l r = FuncUtil.Ctermfunc.is_empty (cterm_lincomb_sub l r)
    5.20  
    5.21 @@ -43,8 +43,8 @@
    5.22   val int_lincomb_neg = FuncUtil.Intfunc.map (K Rat.neg)
    5.23  *)
    5.24   fun int_lincomb_cmul c t =
    5.25 -    if c =/ Rat.zero then FuncUtil.Intfunc.empty else FuncUtil.Intfunc.map (fn _ => fn x => x */ c) t
    5.26 - fun int_lincomb_add l r = FuncUtil.Intfunc.combine (curry op +/) (fn x => x =/ Rat.zero) l r
    5.27 +    if c = Rat.zero then FuncUtil.Intfunc.empty else FuncUtil.Intfunc.map (fn _ => fn x => x * c) t
    5.28 + fun int_lincomb_add l r = FuncUtil.Intfunc.combine (curry op +) (fn x => x = Rat.zero) l r
    5.29  (*
    5.30   fun int_lincomb_sub l r = int_lincomb_add l (int_lincomb_neg r)
    5.31   fun int_lincomb_eq l r = FuncUtil.Intfunc.is_empty (int_lincomb_sub l r)
    5.32 @@ -84,7 +84,7 @@
    5.33  fun replacenegnorms cv t = case Thm.term_of t of
    5.34    @{term "op + :: real => _"}$_$_ => binop_conv (replacenegnorms cv) t
    5.35  | @{term "op * :: real => _"}$_$_ =>
    5.36 -    if dest_ratconst (Thm.dest_arg1 t) </ Rat.zero then arg_conv cv t else Thm.reflexive t
    5.37 +    if dest_ratconst (Thm.dest_arg1 t) < Rat.zero then arg_conv cv t else Thm.reflexive t
    5.38  | _ => Thm.reflexive t
    5.39  (*
    5.40  fun flip v eq =
    5.41 @@ -96,7 +96,7 @@
    5.42  |(a::t) => let val res = allsubsets t in
    5.43                 map (cons a) res @ res end
    5.44  fun evaluate env lin =
    5.45 - FuncUtil.Intfunc.fold (fn (x,c) => fn s => s +/ c */ (FuncUtil.Intfunc.apply env x))
    5.46 + FuncUtil.Intfunc.fold (fn (x,c) => fn s => s + c * (FuncUtil.Intfunc.apply env x))
    5.47     lin Rat.zero
    5.48  
    5.49  fun solve (vs,eqs) = case (vs,eqs) of
    5.50 @@ -129,11 +129,11 @@
    5.51      NONE => NONE
    5.52     | SOME soln => SOME (map (fn v => FuncUtil.Intfunc.tryapplyd soln v Rat.zero) vs)
    5.53    val rawvs = map_filter vertex (combinations (length vs) eqs)
    5.54 -  val unset = filter (forall (fn c => c >=/ Rat.zero)) rawvs
    5.55 - in fold_rev (insert (eq_list op =/)) unset []
    5.56 +  val unset = filter (forall (fn c => c >= Rat.zero)) rawvs
    5.57 + in fold_rev (insert (eq_list op =)) unset []
    5.58   end
    5.59  
    5.60 -val subsumes = eq_list (fn (x, y) => Rat.abs x <=/ Rat.abs y)
    5.61 +val subsumes = eq_list (fn (x, y) => Rat.abs x <= Rat.abs y)
    5.62  
    5.63  fun subsume todo dun = case todo of
    5.64   [] => dun
    5.65 @@ -297,18 +297,18 @@
    5.66         fun check_solution v =
    5.67          let
    5.68            val f = fold_rev FuncUtil.Intfunc.update (nvs ~~ v) (FuncUtil.Intfunc.onefunc (0, Rat.one))
    5.69 -        in forall (fn e => evaluate f e =/ Rat.zero) flippedequations
    5.70 +        in forall (fn e => evaluate f e = Rat.zero) flippedequations
    5.71          end
    5.72         val goodverts = filter check_solution rawverts
    5.73         val signfixups = map (fn n => if member (op =) f n then ~1 else 1) nvs
    5.74 -      in map (map2 (fn s => fn c => Rat.rat_of_int s */ c) signfixups) goodverts
    5.75 +      in map (map2 (fn s => fn c => Rat.rat_of_int s * c) signfixups) goodverts
    5.76        end
    5.77       val allverts = fold_rev append (map plausiblevertices (allsubsets nvs)) []
    5.78      in subsume allverts []
    5.79      end
    5.80     fun compute_ineq v =
    5.81      let
    5.82 -     val ths = map_filter (fn (v,t) => if v =/ Rat.zero then NONE
    5.83 +     val ths = map_filter (fn (v,t) => if v = Rat.zero then NONE
    5.84                                       else SOME(norm_cmul_rule v t))
    5.85                              (v ~~ nubs)
    5.86       fun end_itlist f xs = split_last xs |> uncurry (fold_rev f)
     6.1 --- a/src/HOL/Tools/groebner.ML	Tue May 31 19:51:01 2016 +0200
     6.2 +++ b/src/HOL/Tools/groebner.ML	Tue May 31 21:54:10 2016 +0200
     6.3 @@ -80,14 +80,14 @@
     6.4    | (l1,[]) => l1
     6.5    | ((c1,m1)::o1,(c2,m2)::o2) =>
     6.6          if m1 = m2 then
     6.7 -          let val c = c1+/c2 val rest = grob_add o1 o2 in
     6.8 -          if c =/ rat_0 then rest else (c,m1)::rest end
     6.9 +          let val c = c1 + c2 val rest = grob_add o1 o2 in
    6.10 +          if c = rat_0 then rest else (c,m1)::rest end
    6.11          else if morder_lt m2 m1 then (c1,m1)::(grob_add o1 l2)
    6.12          else (c2,m2)::(grob_add l1 o2);
    6.13  
    6.14  fun grob_sub l1 l2 = grob_add l1 (grob_neg l2);
    6.15  
    6.16 -fun grob_mmul (c1,m1) (c2,m2) = (c1*/c2, ListPair.map (op +) (m1, m2));
    6.17 +fun grob_mmul (c1,m1) (c2,m2) = (c1 * c2, ListPair.map (op +) (m1, m2));
    6.18  
    6.19  fun grob_cmul cm pol = map (grob_mmul cm) pol;
    6.20  
    6.21 @@ -99,16 +99,16 @@
    6.22  fun grob_inv l =
    6.23    case l of
    6.24      [(c,vs)] => if (forall (fn x => x = 0) vs) then
    6.25 -                  if (c =/ rat_0) then error "grob_inv: division by zero"
    6.26 -                  else [(rat_1 // c,vs)]
    6.27 +                  if (c = rat_0) then error "grob_inv: division by zero"
    6.28 +                  else [(rat_1 / c,vs)]
    6.29                else error "grob_inv: non-constant divisor polynomial"
    6.30    | _ => error "grob_inv: non-constant divisor polynomial";
    6.31  
    6.32  fun grob_div l1 l2 =
    6.33    case l2 of
    6.34      [(c,l)] => if (forall (fn x => x = 0) l) then
    6.35 -                 if c =/ rat_0 then error "grob_div: division by zero"
    6.36 -                 else grob_cmul (rat_1 // c,l) l1
    6.37 +                 if c = rat_0 then error "grob_div: division by zero"
    6.38 +                 else grob_cmul (rat_1 / c,l) l1
    6.39               else error "grob_div: non-constant divisor polynomial"
    6.40    | _ => error "grob_div: non-constant divisor polynomial";
    6.41  
    6.42 @@ -120,7 +120,7 @@
    6.43  (* Monomial division operation. *)
    6.44  
    6.45  fun mdiv (c1,m1) (c2,m2) =
    6.46 -  (c1//c2,
    6.47 +  (c1 / c2,
    6.48     map2 (fn n1 => fn n2 => if n1 < n2 then error "mdiv" else n1 - n2) m1 m2);
    6.49  
    6.50  (* Lowest common multiple of two monomials. *)
    6.51 @@ -178,8 +178,8 @@
    6.52  fun monic (pol,hist) =
    6.53    if null pol then (pol,hist) else
    6.54    let val (c',m') = hd pol in
    6.55 -  (map (fn (c,m) => (c//c',m)) pol,
    6.56 -   Mmul((rat_1 // c',map (K 0) m'),hist)) end;
    6.57 +  (map (fn (c,m) => (c / c',m)) pol,
    6.58 +   Mmul((rat_1 / c',map (K 0) m'),hist)) end;
    6.59  
    6.60  (* The most popular heuristic is to order critical pairs by LCM monomial.    *)
    6.61  
    6.62 @@ -190,14 +190,14 @@
    6.63      (_,[]) => false
    6.64    | ([],_) => true
    6.65    | ((c1,m1)::o1,(c2,m2)::o2) =>
    6.66 -        c1 </ c2 orelse
    6.67 -        c1 =/ c2 andalso ((morder_lt m1 m2) orelse m1 = m2 andalso poly_lt o1 o2);
    6.68 +        c1 < c2 orelse
    6.69 +        c1 = c2 andalso ((morder_lt m1 m2) orelse m1 = m2 andalso poly_lt o1 o2);
    6.70  
    6.71  fun align  ((p,hp),(q,hq)) =
    6.72    if poly_lt p q then ((p,hp),(q,hq)) else ((q,hq),(p,hp));
    6.73  
    6.74  fun poly_eq p1 p2 =
    6.75 -  eq_list (fn ((c1, m1), (c2, m2)) => c1 =/ c2 andalso (m1: int list) = m2) (p1, p2);
    6.76 +  eq_list (fn ((c1, m1), (c2, m2)) => c1 = c2 andalso (m1: int list) = m2) (p1, p2);
    6.77  
    6.78  fun memx ((p1,_),(p2,_)) ppairs =
    6.79    not (exists (fn ((q1,_),(q2,_)) => poly_eq p1 q1 andalso poly_eq p2 q2) ppairs);
    6.80 @@ -318,7 +318,7 @@
    6.81      let val cert = resolve_proof vars (grobner_refute pols)
    6.82          val l =
    6.83              fold_rev (fold_rev (lcm_rat o denominator_rat o fst) o snd) cert (rat_1) in
    6.84 -        (l,map (fn (i,p) => (i,map (fn (d,m) => (l*/d,m)) p)) cert) end;
    6.85 +        (l,map (fn (i,p) => (i,map (fn (d,m) => (l * d,m)) p)) cert) end;
    6.86  
    6.87  (* Prove a polynomial is in ideal generated by others, using Grobner basis.  *)
    6.88  
    6.89 @@ -608,7 +608,7 @@
    6.90       [(rat_1,map (fn i => if i aconvc tm then 1 else 0) vars)])
    6.91  handle  CTERM _ =>
    6.92   ((let val x = dest_const tm
    6.93 - in if x =/ rat_0 then [] else [(x,map (K 0) vars)]
    6.94 + in if x = rat_0 then [] else [(x,map (K 0) vars)]
    6.95   end)
    6.96   handle ERROR _ =>
    6.97    ((grob_neg(grobify_term vars (ring_dest_neg tm)))
    6.98 @@ -712,9 +712,9 @@
    6.99         val th2 = funpow deg (idom_rule ctxt o HOLogic.conj_intr ctxt th1) neq_01
   6.100        in (vars,l,cert,th2)
   6.101        end)
   6.102 -    val cert_pos = map (fn (i,p) => (i,filter (fn (c,_) => c >/ rat_0) p)) cert
   6.103 +    val cert_pos = map (fn (i,p) => (i,filter (fn (c,_) => c > rat_0) p)) cert
   6.104      val cert_neg = map (fn (i,p) => (i,map (fn (c,m) => (minus_rat c,m))
   6.105 -                                            (filter (fn (c,_) => c </ rat_0) p))) cert
   6.106 +                                            (filter (fn (c,_) => c < rat_0) p))) cert
   6.107      val  herts_pos = map (fn (i,p) => (i,holify_polynomial vars p)) cert_pos
   6.108      val  herts_neg = map (fn (i,p) => (i,holify_polynomial vars p)) cert_neg
   6.109      fun thm_fn pols =
     7.1 --- a/src/Pure/General/rat.ML	Tue May 31 19:51:01 2016 +0200
     7.2 +++ b/src/Pure/General/rat.ML	Tue May 31 21:54:10 2016 +0200
     7.3 @@ -102,17 +102,13 @@
     7.4  
     7.5  end;
     7.6  
     7.7 -infix 7 */ //;
     7.8 -infix 6 +/ -/;
     7.9 -infix 4 =/ </ <=/ >/ >=/ <>/;
    7.10 -
    7.11 -fun a +/ b = Rat.add a b;
    7.12 -fun a -/ b = a +/ Rat.neg b;
    7.13 -fun a */ b = Rat.mult a b;
    7.14 -fun a // b = a */ Rat.inv b;
    7.15 -fun a =/ b = Rat.eq (a, b);
    7.16 -fun a </ b = Rat.lt a b;
    7.17 -fun a <=/ b = Rat.le a b;
    7.18 -fun a >/ b = b </ a;
    7.19 -fun a >=/ b = b <=/ a;
    7.20 -fun a <>/ b = not (a =/ b);
    7.21 +ML_system_overload (uncurry Rat.add) "+";
    7.22 +ML_system_overload (fn (a, b) => Rat.add a (Rat.neg b)) "-";
    7.23 +ML_system_overload (uncurry Rat.mult) "*";
    7.24 +ML_system_overload (fn (a, b) => Rat.mult a (Rat.inv b)) "/";
    7.25 +ML_system_overload Rat.eq "=";
    7.26 +ML_system_overload (uncurry Rat.lt) "<";
    7.27 +ML_system_overload (uncurry Rat.le) "<=";
    7.28 +ML_system_overload (fn (a, b) => Rat.lt b a) ">";
    7.29 +ML_system_overload (fn (a, b) => Rat.le b a) ">=";
    7.30 +ML_system_overload (not o Rat.eq) "<>";