prefer rat numberals;
authorwenzelm
Wed Jun 01 15:10:27 2016 +0200 (2016-06-01)
changeset 6320597b721666890
parent 63204 921a5be54132
child 63206 13b67739af09
prefer rat numberals;
src/HOL/Decision_Procs/Dense_Linear_Order.thy
src/HOL/Library/Sum_of_Squares/positivstellensatz_tools.ML
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
     1.1 --- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Wed Jun 01 15:01:43 2016 +0200
     1.2 +++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Wed Jun 01 15:10:27 2016 +0200
     1.3 @@ -923,7 +923,7 @@
     1.4          val cr = dest_frac c
     1.5          val clt = Thm.dest_fun2 ct
     1.6          val cz = Thm.dest_arg ct
     1.7 -        val neg = cr < Rat.zero
     1.8 +        val neg = cr < @0
     1.9          val cthp = Simplifier.rewrite ctxt
    1.10                 (Thm.apply @{cterm "Trueprop"}
    1.11                    (if neg then Thm.apply (Thm.apply clt c) cz
    1.12 @@ -946,7 +946,7 @@
    1.13          val cr = dest_frac c
    1.14          val clt = Thm.dest_fun2 ct
    1.15          val cz = Thm.dest_arg ct
    1.16 -        val neg = cr < Rat.zero
    1.17 +        val neg = cr < @0
    1.18          val cthp = Simplifier.rewrite ctxt
    1.19                 (Thm.apply @{cterm "Trueprop"}
    1.20                    (if neg then Thm.apply (Thm.apply clt c) cz
    1.21 @@ -968,7 +968,7 @@
    1.22          val cr = dest_frac c
    1.23          val clt = Thm.cterm_of ctxt (Const (@{const_name ord_class.less}, T --> T --> @{typ bool}))
    1.24          val cz = Thm.dest_arg ct
    1.25 -        val neg = cr < Rat.zero
    1.26 +        val neg = cr < @0
    1.27          val cthp = Simplifier.rewrite ctxt
    1.28                 (Thm.apply @{cterm "Trueprop"}
    1.29                    (if neg then Thm.apply (Thm.apply clt c) cz
    1.30 @@ -993,7 +993,7 @@
    1.31          val cr = dest_frac c
    1.32          val clt = Thm.cterm_of ctxt (Const (@{const_name ord_class.less}, T --> T --> @{typ bool}))
    1.33          val cz = Thm.dest_arg ct
    1.34 -        val neg = cr < Rat.zero
    1.35 +        val neg = cr < @0
    1.36          val cthp = Simplifier.rewrite ctxt
    1.37                 (Thm.apply @{cterm "Trueprop"}
    1.38                    (if neg then Thm.apply (Thm.apply clt c) cz
     2.1 --- a/src/HOL/Library/Sum_of_Squares/positivstellensatz_tools.ML	Wed Jun 01 15:01:43 2016 +0200
     2.2 +++ b/src/HOL/Library/Sum_of_Squares/positivstellensatz_tools.ML	Wed Jun 01 15:10:27 2016 +0200
     2.3 @@ -50,7 +50,7 @@
     2.4  
     2.5  fun string_of_cmonomial (m,c) =
     2.6    if FuncUtil.Ctermfunc.is_empty m then string_of_rat c
     2.7 -  else if c = Rat.one then string_of_monomial m
     2.8 +  else if c = @1 then string_of_monomial m
     2.9    else string_of_rat c ^ "*" ^ string_of_monomial m
    2.10  
    2.11  fun string_of_poly p =
    2.12 @@ -121,7 +121,7 @@
    2.13  
    2.14  fun parse_cmonomial ctxt =
    2.15    rat_int --| str "*" -- (parse_monomial ctxt) >> swap ||
    2.16 -  (parse_monomial ctxt) >> (fn m => (m, Rat.one)) ||
    2.17 +  (parse_monomial ctxt) >> (fn m => (m, @1)) ||
    2.18    rat_int >> (fn r => (FuncUtil.Ctermfunc.empty, r))
    2.19  
    2.20  fun parse_poly ctxt = repeat_sep "+" (parse_cmonomial ctxt) >>
     3.1 --- a/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML	Wed Jun 01 15:01:43 2016 +0200
     3.2 +++ b/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML	Wed Jun 01 15:10:27 2016 +0200
     3.3 @@ -19,10 +19,6 @@
     3.4  structure Sum_of_Squares: SUM_OF_SQUARES =
     3.5  struct
     3.6  
     3.7 -val rat_0 = Rat.zero;
     3.8 -val rat_1 = Rat.one;
     3.9 -val rat_2 = Rat.two;
    3.10 -val rat_10 = Rat.of_int 10;
    3.11  val max = Integer.max;
    3.12  
    3.13  val denominator_rat = Rat.dest #> snd #> Rat.of_int;
    3.14 @@ -37,9 +33,9 @@
    3.15  
    3.16  fun rat_pow r i =
    3.17   let fun pow r i =
    3.18 -   if i = 0 then rat_1 else
    3.19 +   if i = 0 then @1 else
    3.20     let val d = pow r (i div 2)
    3.21 -   in d * d * (if i mod 2 = 0 then rat_1 else r)
    3.22 +   in d * d * (if i mod 2 = 0 then @1 else r)
    3.23     end
    3.24   in if i < 0 then pow (Rat.inv r) (~ i) else pow r i end;
    3.25  
    3.26 @@ -47,13 +43,13 @@
    3.27    let
    3.28      val (a,b) = Rat.dest (Rat.abs r)
    3.29      val d = a div b
    3.30 -    val s = if r < rat_0 then (Rat.neg o Rat.of_int) else Rat.of_int
    3.31 +    val s = if r < @0 then (Rat.neg o Rat.of_int) else Rat.of_int
    3.32      val x2 = 2 * (a - (b * d))
    3.33    in s (if x2 >= b then d + 1 else d) end
    3.34  
    3.35  val abs_rat = Rat.abs;
    3.36 -val pow2 = rat_pow rat_2;
    3.37 -val pow10 = rat_pow rat_10;
    3.38 +val pow2 = rat_pow @2;
    3.39 +val pow10 = rat_pow @10;
    3.40  
    3.41  
    3.42  val trace = Attrib.setup_config_bool @{binding sos_trace} (K false);
    3.43 @@ -78,22 +74,22 @@
    3.44  local
    3.45  
    3.46  fun normalize y =
    3.47 -  if abs_rat y < (rat_1 / rat_10) then normalize (rat_10 * y) - 1
    3.48 -  else if abs_rat y >= rat_1 then normalize (y / rat_10) + 1
    3.49 +  if abs_rat y < @1/10 then normalize (@10 * y) - 1
    3.50 +  else if abs_rat y >= @1 then normalize (y / @10) + 1
    3.51    else 0
    3.52  
    3.53  in
    3.54  
    3.55  fun decimalize d x =
    3.56 -  if x = rat_0 then "0.0"
    3.57 +  if x = @0 then "0.0"
    3.58    else
    3.59      let
    3.60        val y = Rat.abs x
    3.61        val e = normalize y
    3.62 -      val z = pow10(~ e) * y + rat_1
    3.63 +      val z = pow10(~ e) * y + @1
    3.64        val k = int_of_rat (round_rat(pow10 d * z))
    3.65      in
    3.66 -      (if x < rat_0 then "-0." else "0.") ^
    3.67 +      (if x < @0 then "-0." else "0.") ^
    3.68        implode (tl (raw_explode(string_of_int k))) ^
    3.69        (if e = 0 then "" else "e" ^ string_of_int e)
    3.70      end
    3.71 @@ -117,7 +113,7 @@
    3.72  
    3.73  type matrix = (int * int) * Rat.rat FuncUtil.Intpairfunc.table;
    3.74  
    3.75 -fun iszero (_, r) = r = rat_0;
    3.76 +fun iszero (_, r) = r = @0;
    3.77  
    3.78  
    3.79  (* Vectors. Conventionally indexed 1..n.                                     *)
    3.80 @@ -128,7 +124,7 @@
    3.81  
    3.82  fun vector_cmul c (v: vector) =
    3.83    let val n = dim v in
    3.84 -    if c = rat_0 then vector_0 n
    3.85 +    if c = @0 then vector_0 n
    3.86      else (n,FuncUtil.Intfunc.map (fn _ => fn x => c * x) (snd v))
    3.87    end;
    3.88  
    3.89 @@ -152,7 +148,7 @@
    3.90  
    3.91  fun monomial_eval assig m =
    3.92    FuncUtil.Ctermfunc.fold (fn (x, k) => fn a => a * rat_pow (FuncUtil.Ctermfunc.apply assig x) k)
    3.93 -    m rat_1;
    3.94 +    m @1;
    3.95  
    3.96  val monomial_1 = FuncUtil.Ctermfunc.empty;
    3.97  
    3.98 @@ -169,7 +165,7 @@
    3.99  (* Polynomials.                                                              *)
   3.100  
   3.101  fun eval assig p =
   3.102 -  FuncUtil.Monomialfunc.fold (fn (m, c) => fn a => a + c * monomial_eval assig m) p rat_0;
   3.103 +  FuncUtil.Monomialfunc.fold (fn (m, c) => fn a => a + c * monomial_eval assig m) p @0;
   3.104  
   3.105  val poly_0 = FuncUtil.Monomialfunc.empty;
   3.106  
   3.107 @@ -177,25 +173,25 @@
   3.108    FuncUtil.Monomialfunc.fold (fn (m, _) => fn a => FuncUtil.Ctermfunc.is_empty m andalso a)
   3.109      p true;
   3.110  
   3.111 -fun poly_var x = FuncUtil.Monomialfunc.onefunc (monomial_var x, rat_1);
   3.112 +fun poly_var x = FuncUtil.Monomialfunc.onefunc (monomial_var x, @1);
   3.113  
   3.114  fun poly_const c =
   3.115 -  if c = rat_0 then poly_0 else FuncUtil.Monomialfunc.onefunc (monomial_1, c);
   3.116 +  if c = @0 then poly_0 else FuncUtil.Monomialfunc.onefunc (monomial_1, c);
   3.117  
   3.118  fun poly_cmul c p =
   3.119 -  if c = rat_0 then poly_0
   3.120 +  if c = @0 then poly_0
   3.121    else FuncUtil.Monomialfunc.map (fn _ => fn x => c * x) p;
   3.122  
   3.123  fun poly_neg p = FuncUtil.Monomialfunc.map (K Rat.neg) p;
   3.124  
   3.125  
   3.126  fun poly_add p1 p2 =
   3.127 -  FuncUtil.Monomialfunc.combine (curry op +) (fn x => x = rat_0) p1 p2;
   3.128 +  FuncUtil.Monomialfunc.combine (curry op +) (fn x => x = @0) p1 p2;
   3.129  
   3.130  fun poly_sub p1 p2 = poly_add p1 (poly_neg p2);
   3.131  
   3.132  fun poly_cmmul (c,m) p =
   3.133 -  if c = rat_0 then poly_0
   3.134 +  if c = @0 then poly_0
   3.135    else
   3.136      if FuncUtil.Ctermfunc.is_empty m
   3.137      then FuncUtil.Monomialfunc.map (fn _ => fn d => c * d) p
   3.138 @@ -209,7 +205,7 @@
   3.139  fun poly_square p = poly_mul p p;
   3.140  
   3.141  fun poly_pow p k =
   3.142 -  if k = 0 then poly_const rat_1
   3.143 +  if k = 0 then poly_const @1
   3.144    else if k = 1 then p
   3.145    else
   3.146      let val q = poly_square(poly_pow p (k div 2))
   3.147 @@ -289,7 +285,7 @@
   3.148    let
   3.149      val n = dim v
   3.150      val strs =
   3.151 -      map (decimalize 20 o (fn i => FuncUtil.Intfunc.tryapplyd (snd v) i rat_0)) (1 upto n)
   3.152 +      map (decimalize 20 o (fn i => FuncUtil.Intfunc.tryapplyd (snd v) i @0)) (1 upto n)
   3.153    in space_implode " " strs ^ "\n" end;
   3.154  
   3.155  fun triple_int_ord ((a, b, c), (a', b', c')) =
   3.156 @@ -302,7 +298,7 @@
   3.157    else index_char str chr (pos + 1);
   3.158  
   3.159  fun rat_of_quotient (a,b) =
   3.160 -  if b = 0 then rat_0 else Rat.make (a, b);
   3.161 +  if b = 0 then @0 else Rat.make (a, b);
   3.162  
   3.163  fun rat_of_string s =
   3.164    let val n = index_char s #"/" 0 in
   3.165 @@ -336,7 +332,7 @@
   3.166  
   3.167  val exponent = ($$ "e" || $$ "E") |-- signed decimalint;
   3.168  
   3.169 -val decimal = signed decimalsig -- (emptyin rat_0|| exponent)
   3.170 +val decimal = signed decimalsig -- (emptyin @0|| exponent)
   3.171    >> (fn (h, x) => h * pow10 (int_of_rat x));
   3.172  
   3.173  fun mkparser p s =
   3.174 @@ -372,12 +368,12 @@
   3.175  
   3.176  fun tri_scale_then solver (obj:vector) mats =
   3.177    let
   3.178 -    val cd1 = fold_rev (common_denominator Inttriplefunc.fold) mats (rat_1)
   3.179 -    val cd2 = common_denominator FuncUtil.Intfunc.fold (snd obj)  (rat_1)
   3.180 +    val cd1 = fold_rev (common_denominator Inttriplefunc.fold) mats @1
   3.181 +    val cd2 = common_denominator FuncUtil.Intfunc.fold (snd obj) @1
   3.182      val mats' = map (Inttriplefunc.map (fn _ => fn x => cd1 * x)) mats
   3.183      val obj' = vector_cmul cd2 obj
   3.184 -    val max1 = fold_rev (maximal_element Inttriplefunc.fold) mats' (rat_0)
   3.185 -    val max2 = maximal_element FuncUtil.Intfunc.fold (snd obj') (rat_0)
   3.186 +    val max1 = fold_rev (maximal_element Inttriplefunc.fold) mats' @0
   3.187 +    val max2 = maximal_element FuncUtil.Intfunc.fold (snd obj') @0
   3.188      val scal1 = pow2 (20 - int_of_float(Math.ln (float_of_rat max1) / Math.ln 2.0))
   3.189      val scal2 = pow2 (20 - int_of_float(Math.ln (float_of_rat max2) / Math.ln 2.0))
   3.190      val mats'' = map (Inttriplefunc.map (fn _ => fn x => x * scal1)) mats'
   3.191 @@ -391,7 +387,7 @@
   3.192  fun nice_vector n ((d,v) : vector) =
   3.193    (d, FuncUtil.Intfunc.fold (fn (i,c) => fn a =>
   3.194        let val y = nice_rational n c in
   3.195 -        if c = rat_0 then a
   3.196 +        if c = @0 then a
   3.197          else FuncUtil.Intfunc.update (i,y) a
   3.198        end) v FuncUtil.Intfunc.empty): vector
   3.199  
   3.200 @@ -400,16 +396,16 @@
   3.201  (* Stuff for "equations" ((int*int*int)->num functions).                         *)
   3.202  
   3.203  fun tri_equation_cmul c eq =
   3.204 -  if c = rat_0 then Inttriplefunc.empty
   3.205 +  if c = @0 then Inttriplefunc.empty
   3.206    else Inttriplefunc.map (fn _ => fn d => c * d) eq;
   3.207  
   3.208  fun tri_equation_add eq1 eq2 =
   3.209 -  Inttriplefunc.combine (curry op +) (fn x => x = rat_0) eq1 eq2;
   3.210 +  Inttriplefunc.combine (curry op +) (fn x => x = @0) eq1 eq2;
   3.211  
   3.212  fun tri_equation_eval assig eq =
   3.213    let
   3.214      fun value v = Inttriplefunc.apply assig v
   3.215 -  in Inttriplefunc.fold (fn (v, c) => fn a => a + value v * c) eq rat_0 end;
   3.216 +  in Inttriplefunc.fold (fn (v, c) => fn a => a + value v * c) eq @0 end;
   3.217  
   3.218  (* Eliminate all variables, in an essentially arbitrary order.               *)
   3.219  
   3.220 @@ -440,8 +436,8 @@
   3.221                val eq' =
   3.222                  tri_equation_cmul ((Rat.of_int ~1) / a) (Inttriplefunc.delete_safe v eq)
   3.223                fun elim e =
   3.224 -                let val b = Inttriplefunc.tryapplyd e v rat_0 in
   3.225 -                  if b = rat_0 then e
   3.226 +                let val b = Inttriplefunc.tryapplyd e v @0 in
   3.227 +                  if b = @0 then e
   3.228                    else tri_equation_add e (tri_equation_cmul (Rat.neg b / a) eq)
   3.229                  end
   3.230              in
   3.231 @@ -485,10 +481,10 @@
   3.232      if FuncUtil.Intpairfunc.is_empty (snd m) then []
   3.233      else
   3.234        let
   3.235 -        val a11 = FuncUtil.Intpairfunc.tryapplyd (snd m) (i,i) rat_0
   3.236 +        val a11 = FuncUtil.Intpairfunc.tryapplyd (snd m) (i,i) @0
   3.237        in
   3.238 -        if a11 < rat_0 then raise Failure "diagonalize: not PSD"
   3.239 -        else if a11 = rat_0 then
   3.240 +        if a11 < @0 then raise Failure "diagonalize: not PSD"
   3.241 +        else if a11 = @0 then
   3.242            if FuncUtil.Intfunc.is_empty (snd (row i m))
   3.243            then diagonalize n (i + 1) m
   3.244            else raise Failure "diagonalize: not PSD ___ "
   3.245 @@ -498,19 +494,19 @@
   3.246              val v' =
   3.247                (fst v, FuncUtil.Intfunc.fold (fn (i, c) => fn a =>
   3.248                  let val y = c / a11
   3.249 -                in if y = rat_0 then a else FuncUtil.Intfunc.update (i,y) a
   3.250 +                in if y = @0 then a else FuncUtil.Intfunc.update (i,y) a
   3.251                  end) (snd v) FuncUtil.Intfunc.empty)
   3.252              fun upt0 x y a =
   3.253 -              if y = rat_0 then a
   3.254 +              if y = @0 then a
   3.255                else FuncUtil.Intpairfunc.update (x,y) a
   3.256              val m' =
   3.257                ((n, n),
   3.258                  iter (i + 1, n) (fn j =>
   3.259                    iter (i + 1, n) (fn k =>
   3.260                      (upt0 (j, k)
   3.261 -                      (FuncUtil.Intpairfunc.tryapplyd (snd m) (j, k) rat_0 -
   3.262 -                        FuncUtil.Intfunc.tryapplyd (snd v) j rat_0 *
   3.263 -                        FuncUtil.Intfunc.tryapplyd (snd v') k rat_0))))
   3.264 +                      (FuncUtil.Intpairfunc.tryapplyd (snd m) (j, k) @0 -
   3.265 +                        FuncUtil.Intfunc.tryapplyd (snd v) j @0 *
   3.266 +                        FuncUtil.Intfunc.tryapplyd (snd v') k @0))))
   3.267                      FuncUtil.Intpairfunc.empty)
   3.268            in (a11, v') :: diagonalize n (i + 1) m' end
   3.269        end
   3.270 @@ -545,11 +541,11 @@
   3.271  (* Give the output polynomial and a record of how it was derived.            *)
   3.272  
   3.273  fun enumerate_products d pols =
   3.274 -  if d = 0 then [(poly_const rat_1,RealArith.Rational_lt rat_1)]
   3.275 +  if d = 0 then [(poly_const @1, RealArith.Rational_lt @1)]
   3.276    else if d < 0 then []
   3.277    else
   3.278      (case pols of
   3.279 -      [] => [(poly_const rat_1, RealArith.Rational_lt rat_1)]
   3.280 +      [] => [(poly_const @1, RealArith.Rational_lt @1)]
   3.281      | (p, b) :: ps =>
   3.282          let val e = multidegree p in
   3.283            if e = 0 then enumerate_products d ps
   3.284 @@ -603,9 +599,9 @@
   3.285  
   3.286  (* 3D versions of matrix operations to consider blocks separately.           *)
   3.287  
   3.288 -val bmatrix_add = Inttriplefunc.combine (curry op +) (fn x => x = rat_0);
   3.289 +val bmatrix_add = Inttriplefunc.combine (curry op +) (fn x => x = @0);
   3.290  fun bmatrix_cmul c bm =
   3.291 -  if c = rat_0 then Inttriplefunc.empty
   3.292 +  if c = @0 then Inttriplefunc.empty
   3.293    else Inttriplefunc.map (fn _ => fn x => c * x) bm;
   3.294  
   3.295  val bmatrix_neg = bmatrix_cmul (Rat.of_int ~1);
   3.296 @@ -641,7 +637,7 @@
   3.297          (pol :: eqs @ map fst leqs) []
   3.298      val monoid =
   3.299        if linf then
   3.300 -        (poly_const rat_1,RealArith.Rational_lt rat_1)::
   3.301 +        (poly_const @1, RealArith.Rational_lt @1)::
   3.302          (filter (fn (p,_) => multidegree p <= d) leqs)
   3.303        else enumerate_products d leqs
   3.304      val nblocks = length monoid
   3.305 @@ -653,7 +649,7 @@
   3.306        in
   3.307          (mons,
   3.308            fold_rev (fn (m, n) =>
   3.309 -            FuncUtil.Monomialfunc.update (m, Inttriplefunc.onefunc ((~k, ~n, n), rat_1)))
   3.310 +            FuncUtil.Monomialfunc.update (m, Inttriplefunc.onefunc ((~k, ~n, n), @1)))
   3.311            nons FuncUtil.Monomialfunc.empty)
   3.312        end
   3.313  
   3.314 @@ -670,7 +666,7 @@
   3.315                  if n1 > n2 then a
   3.316                  else
   3.317                    let
   3.318 -                    val c = if n1 = n2 then rat_1 else rat_2
   3.319 +                    val c = if n1 = n2 then @1 else @2
   3.320                      val e = FuncUtil.Monomialfunc.tryapplyd a m Inttriplefunc.empty
   3.321                    in
   3.322                      FuncUtil.Monomialfunc.update
   3.323 @@ -690,13 +686,13 @@
   3.324      val (pvs, assig) = tri_eliminate_all_equations (0, 0, 0) eqns
   3.325      val qvars = (0, 0, 0) :: pvs
   3.326      val allassig =
   3.327 -      fold_rev (fn v => Inttriplefunc.update (v, (Inttriplefunc.onefunc (v, rat_1)))) pvs assig
   3.328 +      fold_rev (fn v => Inttriplefunc.update (v, (Inttriplefunc.onefunc (v, @1)))) pvs assig
   3.329      fun mk_matrix v =
   3.330        Inttriplefunc.fold (fn ((b, i, j), ass) => fn m =>
   3.331            if b < 0 then m
   3.332            else
   3.333 -            let val c = Inttriplefunc.tryapplyd ass v rat_0 in
   3.334 -              if c = rat_0 then m
   3.335 +            let val c = Inttriplefunc.tryapplyd ass v @0 in
   3.336 +              if c = @0 then m
   3.337                else Inttriplefunc.update ((b, j, i), c) (Inttriplefunc.update ((b, i, j), c) m)
   3.338              end)
   3.339          allassig Inttriplefunc.empty
   3.340 @@ -709,12 +705,12 @@
   3.341      val obj =
   3.342        (length pvs,
   3.343          itern 1 pvs (fn v => fn i =>
   3.344 -          FuncUtil.Intfunc.updatep iszero (i,Inttriplefunc.tryapplyd diagents v rat_0))
   3.345 +          FuncUtil.Intfunc.updatep iszero (i,Inttriplefunc.tryapplyd diagents v @0))
   3.346            FuncUtil.Intfunc.empty)
   3.347      val raw_vec =
   3.348        if null pvs then vector_0 0
   3.349        else tri_scale_then (run_blockproblem prover nblocks blocksizes) obj mats
   3.350 -    fun int_element (_, v) i = FuncUtil.Intfunc.tryapplyd v i rat_0
   3.351 +    fun int_element (_, v) i = FuncUtil.Intfunc.tryapplyd v i @0
   3.352  
   3.353      fun find_rounding d =
   3.354        let
   3.355 @@ -728,7 +724,7 @@
   3.356          val allmats = blocks blocksizes blockmat
   3.357        in (vec, map diag allmats) end
   3.358      val (vec, ratdias) =
   3.359 -      if null pvs then find_rounding rat_1
   3.360 +      if null pvs then find_rounding @1
   3.361        else tryfind find_rounding (map Rat.of_int (1 upto 31) @ map pow2 (5 upto 66))
   3.362      val newassigs =
   3.363        fold_rev (fn k => Inttriplefunc.update (nth pvs (k - 1), int_element vec k))
   3.364 @@ -803,13 +799,13 @@
   3.365          fun trivial_axiom (p, ax) =
   3.366            (case ax of
   3.367              RealArith.Axiom_eq n =>
   3.368 -              if eval FuncUtil.Ctermfunc.empty p <> Rat.zero then nth eqs n
   3.369 +              if eval FuncUtil.Ctermfunc.empty p <> @0 then nth eqs n
   3.370                else raise Failure "trivial_axiom: Not a trivial axiom"
   3.371            | RealArith.Axiom_le n =>
   3.372 -              if eval FuncUtil.Ctermfunc.empty p < Rat.zero then nth les n
   3.373 +              if eval FuncUtil.Ctermfunc.empty p < @0 then nth les n
   3.374                else raise Failure "trivial_axiom: Not a trivial axiom"
   3.375            | RealArith.Axiom_lt n =>
   3.376 -              if eval FuncUtil.Ctermfunc.empty p <= Rat.zero then nth lts n
   3.377 +              if eval FuncUtil.Ctermfunc.empty p <= @0 then nth lts n
   3.378                else raise Failure "trivial_axiom: Not a trivial axiom"
   3.379            | _ => error "trivial_axiom: Not a trivial axiom")
   3.380        in
   3.381 @@ -834,7 +830,7 @@
   3.382                | Prover prover =>
   3.383                    (* call prover *)
   3.384                    let
   3.385 -                    val pol = fold_rev poly_mul (map fst ltp) (poly_const Rat.one)
   3.386 +                    val pol = fold_rev poly_mul (map fst ltp) (poly_const @1)
   3.387                      val leq = lep @ ltp
   3.388                      fun tryall d =
   3.389                        let
   3.390 @@ -852,11 +848,11 @@
   3.391                        map2 (fn q => fn (_,ax) => RealArith.Eqmul(q,ax)) cert_ideal eq
   3.392                      val proofs_cone = map cterm_of_sos cert_cone
   3.393                      val proof_ne =
   3.394 -                      if null ltp then RealArith.Rational_lt Rat.one
   3.395 +                      if null ltp then RealArith.Rational_lt @1
   3.396                        else
   3.397                          let val p = foldr1 RealArith.Product (map snd ltp) in
   3.398                            funpow i (fn q => RealArith.Product (p, q))
   3.399 -                            (RealArith.Rational_lt Rat.one)
   3.400 +                            (RealArith.Rational_lt @1)
   3.401                          end
   3.402                    in
   3.403                      foldr1 RealArith.Sum (proof_ne :: proofs_ideal @ proofs_cone)
   3.404 @@ -892,7 +888,7 @@
   3.405    fun substitutable_monomial fvs tm =
   3.406      (case Thm.term_of tm of
   3.407        Free (_, @{typ real}) =>
   3.408 -        if not (member (op aconvc) fvs tm) then (Rat.one, tm)
   3.409 +        if not (member (op aconvc) fvs tm) then (@1, tm)
   3.410          else raise Failure "substitutable_monomial"
   3.411      | @{term "op * :: real => _"} $ _ $ (Free _) =>
   3.412          if RealArith.is_ratconst (Thm.dest_arg1 tm) andalso
     4.1 --- a/src/HOL/Library/positivstellensatz.ML	Wed Jun 01 15:01:43 2016 +0200
     4.2 +++ b/src/HOL/Library/positivstellensatz.ML	Wed Jun 01 15:10:27 2016 +0200
     4.3 @@ -338,7 +338,7 @@
     4.4  
     4.5  fun cterm_of_cmonomial (m,c) =
     4.6    if FuncUtil.Ctermfunc.is_empty m then cterm_of_rat c
     4.7 -  else if c = Rat.one then cterm_of_monomial m
     4.8 +  else if c = @1 then cterm_of_monomial m
     4.9    else Thm.apply (Thm.apply @{cterm "op *::real => _"} (cterm_of_rat c)) (cterm_of_monomial m);
    4.10  
    4.11  fun cterm_of_poly p =
    4.12 @@ -585,35 +585,35 @@
    4.13  
    4.14  (* A linear arithmetic prover *)
    4.15  local
    4.16 -  val linear_add = FuncUtil.Ctermfunc.combine (curry op +) (fn z => z = Rat.zero)
    4.17 +  val linear_add = FuncUtil.Ctermfunc.combine (curry op +) (fn z => z = @0)
    4.18    fun linear_cmul c = FuncUtil.Ctermfunc.map (fn _ => fn x => c * x)
    4.19    val one_tm = @{cterm "1::real"}
    4.20 -  fun contradictory p (e,_) = ((FuncUtil.Ctermfunc.is_empty e) andalso not(p Rat.zero)) orelse
    4.21 +  fun contradictory p (e,_) = ((FuncUtil.Ctermfunc.is_empty e) andalso not(p @0)) orelse
    4.22       ((eq_set (op aconvc) (FuncUtil.Ctermfunc.dom e, [one_tm])) andalso
    4.23         not(p(FuncUtil.Ctermfunc.apply e one_tm)))
    4.24  
    4.25    fun linear_ineqs vars (les,lts) =
    4.26 -    case find_first (contradictory (fn x => x > Rat.zero)) lts of
    4.27 +    case find_first (contradictory (fn x => x > @0)) lts of
    4.28        SOME r => r
    4.29      | NONE =>
    4.30 -      (case find_first (contradictory (fn x => x > Rat.zero)) les of
    4.31 +      (case find_first (contradictory (fn x => x > @0)) les of
    4.32           SOME r => r
    4.33         | NONE =>
    4.34           if null vars then error "linear_ineqs: no contradiction" else
    4.35           let
    4.36             val ineqs = les @ lts
    4.37             fun blowup v =
    4.38 -             length(filter (fn (e,_) => FuncUtil.Ctermfunc.tryapplyd e v Rat.zero = Rat.zero) ineqs) +
    4.39 -             length(filter (fn (e,_) => FuncUtil.Ctermfunc.tryapplyd e v Rat.zero > Rat.zero) ineqs) *
    4.40 -             length(filter (fn (e,_) => FuncUtil.Ctermfunc.tryapplyd e v Rat.zero < Rat.zero) ineqs)
    4.41 +             length(filter (fn (e,_) => FuncUtil.Ctermfunc.tryapplyd e v @0 = @0) ineqs) +
    4.42 +             length(filter (fn (e,_) => FuncUtil.Ctermfunc.tryapplyd e v @0 > @0) ineqs) *
    4.43 +             length(filter (fn (e,_) => FuncUtil.Ctermfunc.tryapplyd e v @0 < @0) ineqs)
    4.44             val v = fst(hd(sort (fn ((_,i),(_,j)) => int_ord (i,j))
    4.45               (map (fn v => (v,blowup v)) vars)))
    4.46             fun addup (e1,p1) (e2,p2) acc =
    4.47               let
    4.48 -               val c1 = FuncUtil.Ctermfunc.tryapplyd e1 v Rat.zero
    4.49 -               val c2 = FuncUtil.Ctermfunc.tryapplyd e2 v Rat.zero
    4.50 +               val c1 = FuncUtil.Ctermfunc.tryapplyd e1 v @0
    4.51 +               val c2 = FuncUtil.Ctermfunc.tryapplyd e2 v @0
    4.52               in
    4.53 -               if c1 * c2 >= Rat.zero then acc else
    4.54 +               if c1 * c2 >= @0 then acc else
    4.55                 let
    4.56                   val e1' = linear_cmul (Rat.abs c2) e1
    4.57                   val e2' = linear_cmul (Rat.abs c1) e2
    4.58 @@ -623,13 +623,13 @@
    4.59                 end
    4.60               end
    4.61             val (les0,les1) =
    4.62 -             List.partition (fn (e,_) => FuncUtil.Ctermfunc.tryapplyd e v Rat.zero = Rat.zero) les
    4.63 +             List.partition (fn (e,_) => FuncUtil.Ctermfunc.tryapplyd e v @0 = @0) les
    4.64             val (lts0,lts1) =
    4.65 -             List.partition (fn (e,_) => FuncUtil.Ctermfunc.tryapplyd e v Rat.zero = Rat.zero) lts
    4.66 +             List.partition (fn (e,_) => FuncUtil.Ctermfunc.tryapplyd e v @0 = @0) lts
    4.67             val (lesp,lesn) =
    4.68 -             List.partition (fn (e,_) => FuncUtil.Ctermfunc.tryapplyd e v Rat.zero > Rat.zero) les1
    4.69 +             List.partition (fn (e,_) => FuncUtil.Ctermfunc.tryapplyd e v @0 > @0) les1
    4.70             val (ltsp,ltsn) =
    4.71 -             List.partition (fn (e,_) => FuncUtil.Ctermfunc.tryapplyd e v Rat.zero > Rat.zero) lts1
    4.72 +             List.partition (fn (e,_) => FuncUtil.Ctermfunc.tryapplyd e v @0 > @0) lts1
    4.73             val les' = fold_rev (fn ep1 => fold_rev (addup ep1) lesp) lesn les0
    4.74             val lts' = fold_rev (fn ep1 => fold_rev (addup ep1) (lesp@ltsp)) ltsn
    4.75                        (fold_rev (fn ep1 => fold_rev (addup ep1) (lesn@ltsn)) ltsp lts0)
    4.76 @@ -637,7 +637,7 @@
    4.77           end)
    4.78  
    4.79    fun linear_eqs(eqs,les,lts) =
    4.80 -    case find_first (contradictory (fn x => x = Rat.zero)) eqs of
    4.81 +    case find_first (contradictory (fn x => x = @0)) eqs of
    4.82        SOME r => r
    4.83      | NONE =>
    4.84        (case eqs of
    4.85 @@ -650,8 +650,8 @@
    4.86           let
    4.87             val (x,c) = FuncUtil.Ctermfunc.choose (FuncUtil.Ctermfunc.delete_safe one_tm e)
    4.88             fun xform (inp as (t,q)) =
    4.89 -             let val d = FuncUtil.Ctermfunc.tryapplyd t x Rat.zero in
    4.90 -               if d = Rat.zero then inp else
    4.91 +             let val d = FuncUtil.Ctermfunc.tryapplyd t x @0 in
    4.92 +               if d = @0 then inp else
    4.93                 let
    4.94                   val k = (Rat.neg d) * Rat.abs c / c
    4.95                   val e' = linear_cmul k e
    4.96 @@ -674,12 +674,12 @@
    4.97  
    4.98    fun lin_of_hol ct =
    4.99      if ct aconvc @{cterm "0::real"} then FuncUtil.Ctermfunc.empty
   4.100 -    else if not (is_comb ct) then FuncUtil.Ctermfunc.onefunc (ct, Rat.one)
   4.101 +    else if not (is_comb ct) then FuncUtil.Ctermfunc.onefunc (ct, @1)
   4.102      else if is_ratconst ct then FuncUtil.Ctermfunc.onefunc (one_tm, dest_ratconst ct)
   4.103      else
   4.104        let val (lop,r) = Thm.dest_comb ct
   4.105        in
   4.106 -        if not (is_comb lop) then FuncUtil.Ctermfunc.onefunc (ct, Rat.one)
   4.107 +        if not (is_comb lop) then FuncUtil.Ctermfunc.onefunc (ct, @1)
   4.108          else
   4.109            let val (opr,l) = Thm.dest_comb lop
   4.110            in
   4.111 @@ -687,7 +687,7 @@
   4.112              then linear_add (lin_of_hol l) (lin_of_hol r)
   4.113              else if opr aconvc @{cterm "op * :: real =>_"}
   4.114                      andalso is_ratconst l then FuncUtil.Ctermfunc.onefunc (r, dest_ratconst l)
   4.115 -            else FuncUtil.Ctermfunc.onefunc (ct, Rat.one)
   4.116 +            else FuncUtil.Ctermfunc.onefunc (ct, @1)
   4.117            end
   4.118        end
   4.119  
   4.120 @@ -707,7 +707,7 @@
   4.121      val aliens = filter is_alien
   4.122        (fold_rev (union (op aconvc) o FuncUtil.Ctermfunc.dom)
   4.123                  (eq_pols @ le_pols @ lt_pols) [])
   4.124 -    val le_pols' = le_pols @ map (fn v => FuncUtil.Ctermfunc.onefunc (v,Rat.one)) aliens
   4.125 +    val le_pols' = le_pols @ map (fn v => FuncUtil.Ctermfunc.onefunc (v,@1)) aliens
   4.126      val (_,proof) = linear_prover (eq_pols,le_pols',lt_pols)
   4.127      val le' = le @ map (fn a => Thm.instantiate' [] [SOME (Thm.dest_arg a)] @{thm of_nat_0_le_iff}) aliens
   4.128    in ((translator (eq,le',lt) proof), Trivial)
     5.1 --- a/src/HOL/Multivariate_Analysis/normarith.ML	Wed Jun 01 15:01:43 2016 +0200
     5.2 +++ b/src/HOL/Multivariate_Analysis/normarith.ML	Wed Jun 01 15:10:27 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) >= @0)
     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 = @0 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 = @0) 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 = @0 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 = @0) 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 @@ -64,11 +64,11 @@
    5.33     let
    5.34       val b = ((snd o HOLogic.dest_number o term_of o Thm.dest_arg) t = 0
    5.35                 handle TERM _=> false)
    5.36 -   in if b then FuncUtil.Ctermfunc.onefunc (t,Rat.one)
    5.37 +   in if b then FuncUtil.Ctermfunc.onefunc (t,@1)
    5.38        else FuncUtil.Ctermfunc.empty
    5.39     end
    5.40  *)
    5.41 - | _ => FuncUtil.Ctermfunc.onefunc (t,Rat.one)
    5.42 + | _ => FuncUtil.Ctermfunc.onefunc (t,@1)
    5.43  
    5.44   fun vector_lincombs ts =
    5.45    fold_rev
    5.46 @@ -84,7 +84,7 @@
    5.47  fun replacenegnorms cv t = case Thm.term_of t of
    5.48    @{term "op + :: real => _"}$_$_ => binop_conv (replacenegnorms cv) t
    5.49  | @{term "op * :: real => _"}$_$_ =>
    5.50 -    if dest_ratconst (Thm.dest_arg1 t) < Rat.zero then arg_conv cv t else Thm.reflexive t
    5.51 +    if dest_ratconst (Thm.dest_arg1 t) < @0 then arg_conv cv t else Thm.reflexive t
    5.52  | _ => Thm.reflexive t
    5.53  (*
    5.54  fun flip v eq =
    5.55 @@ -97,10 +97,10 @@
    5.56                 map (cons a) res @ res end
    5.57  fun evaluate env lin =
    5.58   FuncUtil.Intfunc.fold (fn (x,c) => fn s => s + c * (FuncUtil.Intfunc.apply env x))
    5.59 -   lin Rat.zero
    5.60 +   lin @0
    5.61  
    5.62  fun solve (vs,eqs) = case (vs,eqs) of
    5.63 -  ([],[]) => SOME (FuncUtil.Intfunc.onefunc (0,Rat.one))
    5.64 +  ([],[]) => SOME (FuncUtil.Intfunc.onefunc (0,@1))
    5.65   |(_,eq::oeqs) =>
    5.66     (case filter (member (op =) vs) (FuncUtil.Intfunc.dom eq) of (*FIXME use find_first here*)
    5.67       [] => NONE
    5.68 @@ -127,9 +127,9 @@
    5.69   let
    5.70    fun vertex cmb = case solve(vs,cmb) of
    5.71      NONE => NONE
    5.72 -   | SOME soln => SOME (map (fn v => FuncUtil.Intfunc.tryapplyd soln v Rat.zero) vs)
    5.73 +   | SOME soln => SOME (map (fn v => FuncUtil.Intfunc.tryapplyd soln v @0) vs)
    5.74    val rawvs = map_filter vertex (combinations (length vs) eqs)
    5.75 -  val unset = filter (forall (fn c => c >= Rat.zero)) rawvs
    5.76 +  val unset = filter (forall (fn c => c >= @0)) rawvs
    5.77   in fold_rev (insert (eq_list op =)) unset []
    5.78   end
    5.79  
    5.80 @@ -242,7 +242,7 @@
    5.81  (* FIXME
    5.82  | Const(@{const_name vec},_)$n =>
    5.83    let val n = Thm.dest_arg ct
    5.84 -  in if is_ratconst n andalso not (dest_ratconst n =/ Rat.zero)
    5.85 +  in if is_ratconst n andalso not (dest_ratconst n =/ @0)
    5.86       then Thm.reflexive ct else apply_pth1 ct
    5.87    end
    5.88  *)
    5.89 @@ -288,7 +288,7 @@
    5.90        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
    5.91        end
    5.92       val equations = map coefficients vvs
    5.93 -     val inequalities = map (fn n => FuncUtil.Intfunc.onefunc (n,Rat.one)) nvs
    5.94 +     val inequalities = map (fn n => FuncUtil.Intfunc.onefunc (n,@1)) nvs
    5.95       fun plausiblevertices f =
    5.96        let
    5.97         val flippedequations = map (fold_rev int_flip f) equations
    5.98 @@ -296,8 +296,8 @@
    5.99         val rawverts = vertices nvs constraints
   5.100         fun check_solution v =
   5.101          let
   5.102 -          val f = fold_rev FuncUtil.Intfunc.update (nvs ~~ v) (FuncUtil.Intfunc.onefunc (0, Rat.one))
   5.103 -        in forall (fn e => evaluate f e = Rat.zero) flippedequations
   5.104 +          val f = fold_rev FuncUtil.Intfunc.update (nvs ~~ v) (FuncUtil.Intfunc.onefunc (0, @1))
   5.105 +        in forall (fn e => evaluate f e = @0) flippedequations
   5.106          end
   5.107         val goodverts = filter check_solution rawverts
   5.108         val signfixups = map (fn n => if member (op =) f n then ~1 else 1) nvs
   5.109 @@ -308,7 +308,7 @@
   5.110      end
   5.111     fun compute_ineq v =
   5.112      let
   5.113 -     val ths = map_filter (fn (v,t) => if v = Rat.zero then NONE
   5.114 +     val ths = map_filter (fn (v,t) => if v = @0 then NONE
   5.115                                       else SOME(norm_cmul_rule v t))
   5.116                              (v ~~ nubs)
   5.117       fun end_itlist f xs = split_last xs |> uncurry (fold_rev f)
     6.1 --- a/src/HOL/Tools/groebner.ML	Wed Jun 01 15:01:43 2016 +0200
     6.2 +++ b/src/HOL/Tools/groebner.ML	Wed Jun 01 15:10:27 2016 +0200
     6.3 @@ -32,8 +32,6 @@
     6.4    if is_binop ct ct' then Thm.dest_binop ct'
     6.5    else raise CTERM ("dest_binary: bad binop", [ct, ct'])
     6.6  
     6.7 -val rat_0 = Rat.zero;
     6.8 -val rat_1 = Rat.one;
     6.9  val minus_rat = Rat.neg;
    6.10  val denominator_rat = Rat.dest #> snd #> Rat.of_int;
    6.11  fun int_of_rat a =
    6.12 @@ -81,7 +79,7 @@
    6.13    | ((c1,m1)::o1,(c2,m2)::o2) =>
    6.14          if m1 = m2 then
    6.15            let val c = c1 + c2 val rest = grob_add o1 o2 in
    6.16 -          if c = rat_0 then rest else (c,m1)::rest end
    6.17 +          if c = @0 then rest else (c,m1)::rest end
    6.18          else if morder_lt m2 m1 then (c1,m1)::(grob_add o1 l2)
    6.19          else (c2,m2)::(grob_add l1 o2);
    6.20  
    6.21 @@ -99,22 +97,22 @@
    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 = @0 then error "grob_inv: division by zero"
    6.28 +                  else [(@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 = @0 then error "grob_div: division by zero"
    6.38 +                 else grob_cmul (@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  fun grob_pow vars l n =
    6.43    if n < 0 then error "grob_pow: negative power"
    6.44 -  else if n = 0 then [(rat_1,map (K 0) vars)]
    6.45 +  else if n = 0 then [(@1,map (K 0) vars)]
    6.46    else grob_mul l (grob_pow vars l (n - 1));
    6.47  
    6.48  (* Monomial division operation. *)
    6.49 @@ -125,7 +123,7 @@
    6.50  
    6.51  (* Lowest common multiple of two monomials. *)
    6.52  
    6.53 -fun mlcm (_,m1) (_,m2) = (rat_1, ListPair.map Int.max (m1, m2));
    6.54 +fun mlcm (_,m1) (_,m2) = (@1, ListPair.map Int.max (m1, m2));
    6.55  
    6.56  (* Reduce monomial cm by polynomial pol, returning replacement for cm.  *)
    6.57  
    6.58 @@ -179,7 +177,7 @@
    6.59    if null pol then (pol,hist) else
    6.60    let val (c',m') = hd pol in
    6.61    (map (fn (c,m) => (c / c',m)) pol,
    6.62 -   Mmul((rat_1 / c',map (K 0) m'),hist)) end;
    6.63 +   Mmul((@1 / c',map (K 0) m'),hist)) end;
    6.64  
    6.65  (* The most popular heuristic is to order critical pairs by LCM monomial.    *)
    6.66  
    6.67 @@ -299,7 +297,7 @@
    6.68  fun resolve_proof vars prf =
    6.69    case prf of
    6.70      Start(~1) => []
    6.71 -  | Start m => [(m,[(rat_1,map (K 0) vars)])]
    6.72 +  | Start m => [(m,[(@1,map (K 0) vars)])]
    6.73    | Mmul(pol,lin) =>
    6.74          let val lis = resolve_proof vars lin in
    6.75              map (fn (n,p) => (n,grob_cmul pol p)) lis end
    6.76 @@ -317,7 +315,7 @@
    6.77  fun grobner_weak vars pols =
    6.78      let val cert = resolve_proof vars (grobner_refute pols)
    6.79          val l =
    6.80 -            fold_rev (fold_rev (lcm_rat o denominator_rat o fst) o snd) cert (rat_1) in
    6.81 +            fold_rev (fold_rev (lcm_rat o denominator_rat o fst) o snd) cert @1 in
    6.82          (l,map (fn (i,p) => (i,map (fn (d,m) => (l * d,m)) p)) cert) end;
    6.83  
    6.84  (* Prove a polynomial is in ideal generated by others, using Grobner basis.  *)
    6.85 @@ -331,8 +329,8 @@
    6.86  
    6.87  fun grobner_strong vars pols pol =
    6.88      let val vars' = @{cterm "True"}::vars
    6.89 -        val grob_z = [(rat_1,1::(map (K 0) vars))]
    6.90 -        val grob_1 = [(rat_1,(map (K 0) vars'))]
    6.91 +        val grob_z = [(@1, 1::(map (K 0) vars))]
    6.92 +        val grob_1 = [(@1, (map (K 0) vars'))]
    6.93          fun augment p= map (fn (c,m) => (c,0::m)) p
    6.94          val pols' = map augment pols
    6.95          val pol' = augment pol
    6.96 @@ -605,10 +603,10 @@
    6.97  
    6.98  fun grobify_term vars tm =
    6.99  ((if not (member (op aconvc) vars tm) then raise CTERM ("Not a variable", [tm]) else
   6.100 -     [(rat_1,map (fn i => if i aconvc tm then 1 else 0) vars)])
   6.101 +     [(@1, map (fn i => if i aconvc tm then 1 else 0) vars)])
   6.102  handle  CTERM _ =>
   6.103   ((let val x = dest_const tm
   6.104 - in if x = rat_0 then [] else [(x,map (K 0) vars)]
   6.105 + in if x = @0 then [] else [(x,map (K 0) vars)]
   6.106   end)
   6.107   handle ERROR _ =>
   6.108    ((grob_neg(grobify_term vars (ring_dest_neg tm)))
   6.109 @@ -662,15 +660,15 @@
   6.110     in end_itlist ring_mk_mul (mk_const c :: xps)
   6.111    end
   6.112   fun holify_polynomial vars p =
   6.113 -     if null p then mk_const (rat_0)
   6.114 +     if null p then mk_const @0
   6.115       else end_itlist ring_mk_add (map (holify_monomial vars) p)
   6.116   in holify_polynomial
   6.117   end ;
   6.118  
   6.119  fun idom_rule ctxt = simplify (put_simpset HOL_basic_ss ctxt addsimps [idom_thm]);
   6.120  fun prove_nz n = eqF_elim
   6.121 -                 (ring_eq_conv(mk_binop eq_tm (mk_const n) (mk_const(rat_0))));
   6.122 -val neq_01 = prove_nz (rat_1);
   6.123 +                 (ring_eq_conv(mk_binop eq_tm (mk_const n) (mk_const @0)));
   6.124 +val neq_01 = prove_nz @1;
   6.125  fun neq_rule n th = [prove_nz n, th] MRS neq_thm;
   6.126  fun mk_add th1 = Thm.combination (Drule.arg_cong_rule ring_add_tm th1);
   6.127  
   6.128 @@ -712,13 +710,13 @@
   6.129         val th2 = funpow deg (idom_rule ctxt o HOLogic.conj_intr ctxt th1) neq_01
   6.130        in (vars,l,cert,th2)
   6.131        end)
   6.132 -    val cert_pos = map (fn (i,p) => (i,filter (fn (c,_) => c > rat_0) p)) cert
   6.133 +    val cert_pos = map (fn (i,p) => (i,filter (fn (c,_) => c > @0) p)) cert
   6.134      val cert_neg = map (fn (i,p) => (i,map (fn (c,m) => (minus_rat c,m))
   6.135 -                                            (filter (fn (c,_) => c < rat_0) p))) cert
   6.136 +                                            (filter (fn (c,_) => c < @0) p))) cert
   6.137      val  herts_pos = map (fn (i,p) => (i,holify_polynomial vars p)) cert_pos
   6.138      val  herts_neg = map (fn (i,p) => (i,holify_polynomial vars p)) cert_neg
   6.139      fun thm_fn pols =
   6.140 -        if null pols then Thm.reflexive(mk_const rat_0) else
   6.141 +        if null pols then Thm.reflexive(mk_const @0) else
   6.142          end_itlist mk_add
   6.143              (map (fn (i,p) => Drule.arg_cong_rule (Thm.apply ring_mul_tm p)
   6.144                (nth eths i |> mk_meta_eq)) pols)
     7.1 --- a/src/HOL/Tools/lin_arith.ML	Wed Jun 01 15:01:43 2016 +0200
     7.2 +++ b/src/HOL/Tools/lin_arith.ML	Wed Jun 01 15:10:27 2016 +0200
     7.3 @@ -156,11 +156,11 @@
     7.4           if we choose to do so here, the simpset used by arith must be able to
     7.5           perform the same simplifications. *)
     7.6        (* quotient 's / t', where the denominator t can be NONE *)
     7.7 -      (* Note: will raise Rat.DIVZERO iff m' is Rat.zero *)
     7.8 +      (* Note: will raise Rat.DIVZERO iff m' is @0 *)
     7.9        if of_field_sort thy (domain_type T) then
    7.10          let
    7.11            val (os',m') = demult (s, m);
    7.12 -          val (ot',p) = demult (t, Rat.one)
    7.13 +          val (ot',p) = demult (t, @1)
    7.14          in (case (os',ot') of
    7.15              (SOME s', SOME t') => SOME (mC $ s' $ t')
    7.16            | (SOME s', NONE) => SOME s'
    7.17 @@ -172,7 +172,7 @@
    7.18        else (SOME atom, m)
    7.19      (* terms that evaluate to numeric constants *)
    7.20      | demult (Const (@{const_name Groups.uminus}, _) $ t, m) = demult (t, Rat.neg m)
    7.21 -    | demult (Const (@{const_name Groups.zero}, _), _) = (NONE, Rat.zero)
    7.22 +    | demult (Const (@{const_name Groups.zero}, _), _) = (NONE, @0)
    7.23      | demult (Const (@{const_name Groups.one}, _), m) = (NONE, m)
    7.24      (*Warning: in rare cases (neg_)numeral encloses a non-numeral,
    7.25        in which case dest_numeral raises TERM; hence all the handles below.
    7.26 @@ -227,8 +227,8 @@
    7.27          if member (op =) inj_consts f then poly (x, m, pi) else add_atom all m pi
    7.28      | poly (all, m, pi) =
    7.29          add_atom all m pi
    7.30 -  val (p, i) = poly (lhs, Rat.one, ([], Rat.zero))
    7.31 -  val (q, j) = poly (rhs, Rat.one, ([], Rat.zero))
    7.32 +  val (p, i) = poly (lhs, @1, ([], @0))
    7.33 +  val (q, j) = poly (rhs, @1, ([], @0))
    7.34  in
    7.35    case rel of
    7.36      @{const_name Orderings.less}    => SOME (p, i, "<", q, j)