# HG changeset patch
# User wenzelm
# Date 1464786627 -7200
# Node ID 97b721666890a7512cec6f94e9f50410c1702268
# Parent  921a5be5413293388825d402a5e07c97c109c808
prefer rat numberals;

diff -r 921a5be54132 -r 97b721666890 src/HOL/Decision_Procs/Dense_Linear_Order.thy
--- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Wed Jun 01 15:01:43 2016 +0200
+++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Wed Jun 01 15:10:27 2016 +0200
@@ -923,7 +923,7 @@
         val cr = dest_frac c
         val clt = Thm.dest_fun2 ct
         val cz = Thm.dest_arg ct
-        val neg = cr < Rat.zero
+        val neg = cr < @0
         val cthp = Simplifier.rewrite ctxt
                (Thm.apply @{cterm "Trueprop"}
                   (if neg then Thm.apply (Thm.apply clt c) cz
@@ -946,7 +946,7 @@
         val cr = dest_frac c
         val clt = Thm.dest_fun2 ct
         val cz = Thm.dest_arg ct
-        val neg = cr < Rat.zero
+        val neg = cr < @0
         val cthp = Simplifier.rewrite ctxt
                (Thm.apply @{cterm "Trueprop"}
                   (if neg then Thm.apply (Thm.apply clt c) cz
@@ -968,7 +968,7 @@
         val cr = dest_frac c
         val clt = Thm.cterm_of ctxt (Const (@{const_name ord_class.less}, T --> T --> @{typ bool}))
         val cz = Thm.dest_arg ct
-        val neg = cr < Rat.zero
+        val neg = cr < @0
         val cthp = Simplifier.rewrite ctxt
                (Thm.apply @{cterm "Trueprop"}
                   (if neg then Thm.apply (Thm.apply clt c) cz
@@ -993,7 +993,7 @@
         val cr = dest_frac c
         val clt = Thm.cterm_of ctxt (Const (@{const_name ord_class.less}, T --> T --> @{typ bool}))
         val cz = Thm.dest_arg ct
-        val neg = cr < Rat.zero
+        val neg = cr < @0
         val cthp = Simplifier.rewrite ctxt
                (Thm.apply @{cterm "Trueprop"}
                   (if neg then Thm.apply (Thm.apply clt c) cz
diff -r 921a5be54132 -r 97b721666890 src/HOL/Library/Sum_of_Squares/positivstellensatz_tools.ML
--- a/src/HOL/Library/Sum_of_Squares/positivstellensatz_tools.ML	Wed Jun 01 15:01:43 2016 +0200
+++ b/src/HOL/Library/Sum_of_Squares/positivstellensatz_tools.ML	Wed Jun 01 15:10:27 2016 +0200
@@ -50,7 +50,7 @@
 
 fun string_of_cmonomial (m,c) =
   if FuncUtil.Ctermfunc.is_empty m then string_of_rat c
-  else if c = Rat.one then string_of_monomial m
+  else if c = @1 then string_of_monomial m
   else string_of_rat c ^ "*" ^ string_of_monomial m
 
 fun string_of_poly p =
@@ -121,7 +121,7 @@
 
 fun parse_cmonomial ctxt =
   rat_int --| str "*" -- (parse_monomial ctxt) >> swap ||
-  (parse_monomial ctxt) >> (fn m => (m, Rat.one)) ||
+  (parse_monomial ctxt) >> (fn m => (m, @1)) ||
   rat_int >> (fn r => (FuncUtil.Ctermfunc.empty, r))
 
 fun parse_poly ctxt = repeat_sep "+" (parse_cmonomial ctxt) >>
diff -r 921a5be54132 -r 97b721666890 src/HOL/Library/Sum_of_Squares/sum_of_squares.ML
--- a/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML	Wed Jun 01 15:01:43 2016 +0200
+++ b/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML	Wed Jun 01 15:10:27 2016 +0200
@@ -19,10 +19,6 @@
 structure Sum_of_Squares: SUM_OF_SQUARES =
 struct
 
-val rat_0 = Rat.zero;
-val rat_1 = Rat.one;
-val rat_2 = Rat.two;
-val rat_10 = Rat.of_int 10;
 val max = Integer.max;
 
 val denominator_rat = Rat.dest #> snd #> Rat.of_int;
@@ -37,9 +33,9 @@
 
 fun rat_pow r i =
  let fun pow r i =
-   if i = 0 then rat_1 else
+   if i = 0 then @1 else
    let val d = pow r (i div 2)
-   in d * d * (if i mod 2 = 0 then rat_1 else r)
+   in d * d * (if i mod 2 = 0 then @1 else r)
    end
  in if i < 0 then pow (Rat.inv r) (~ i) else pow r i end;
 
@@ -47,13 +43,13 @@
   let
     val (a,b) = Rat.dest (Rat.abs r)
     val d = a div b
-    val s = if r < rat_0 then (Rat.neg o Rat.of_int) else Rat.of_int
+    val s = if r < @0 then (Rat.neg o Rat.of_int) else Rat.of_int
     val x2 = 2 * (a - (b * d))
   in s (if x2 >= b then d + 1 else d) end
 
 val abs_rat = Rat.abs;
-val pow2 = rat_pow rat_2;
-val pow10 = rat_pow rat_10;
+val pow2 = rat_pow @2;
+val pow10 = rat_pow @10;
 
 
 val trace = Attrib.setup_config_bool @{binding sos_trace} (K false);
@@ -78,22 +74,22 @@
 local
 
 fun normalize y =
-  if abs_rat y < (rat_1 / rat_10) then normalize (rat_10 * y) - 1
-  else if abs_rat y >= rat_1 then normalize (y / rat_10) + 1
+  if abs_rat y < @1/10 then normalize (@10 * y) - 1
+  else if abs_rat y >= @1 then normalize (y / @10) + 1
   else 0
 
 in
 
 fun decimalize d x =
-  if x = rat_0 then "0.0"
+  if x = @0 then "0.0"
   else
     let
       val y = Rat.abs x
       val e = normalize y
-      val z = pow10(~ e) * y + rat_1
+      val z = pow10(~ e) * y + @1
       val k = int_of_rat (round_rat(pow10 d * z))
     in
-      (if x < rat_0 then "-0." else "0.") ^
+      (if x < @0 then "-0." else "0.") ^
       implode (tl (raw_explode(string_of_int k))) ^
       (if e = 0 then "" else "e" ^ string_of_int e)
     end
@@ -117,7 +113,7 @@
 
 type matrix = (int * int) * Rat.rat FuncUtil.Intpairfunc.table;
 
-fun iszero (_, r) = r = rat_0;
+fun iszero (_, r) = r = @0;
 
 
 (* Vectors. Conventionally indexed 1..n.                                     *)
@@ -128,7 +124,7 @@
 
 fun vector_cmul c (v: vector) =
   let val n = dim v in
-    if c = rat_0 then vector_0 n
+    if c = @0 then vector_0 n
     else (n,FuncUtil.Intfunc.map (fn _ => fn x => c * x) (snd v))
   end;
 
@@ -152,7 +148,7 @@
 
 fun monomial_eval assig m =
   FuncUtil.Ctermfunc.fold (fn (x, k) => fn a => a * rat_pow (FuncUtil.Ctermfunc.apply assig x) k)
-    m rat_1;
+    m @1;
 
 val monomial_1 = FuncUtil.Ctermfunc.empty;
 
@@ -169,7 +165,7 @@
 (* Polynomials.                                                              *)
 
 fun eval assig p =
-  FuncUtil.Monomialfunc.fold (fn (m, c) => fn a => a + c * monomial_eval assig m) p rat_0;
+  FuncUtil.Monomialfunc.fold (fn (m, c) => fn a => a + c * monomial_eval assig m) p @0;
 
 val poly_0 = FuncUtil.Monomialfunc.empty;
 
@@ -177,25 +173,25 @@
   FuncUtil.Monomialfunc.fold (fn (m, _) => fn a => FuncUtil.Ctermfunc.is_empty m andalso a)
     p true;
 
-fun poly_var x = FuncUtil.Monomialfunc.onefunc (monomial_var x, rat_1);
+fun poly_var x = FuncUtil.Monomialfunc.onefunc (monomial_var x, @1);
 
 fun poly_const c =
-  if c = rat_0 then poly_0 else FuncUtil.Monomialfunc.onefunc (monomial_1, c);
+  if c = @0 then poly_0 else FuncUtil.Monomialfunc.onefunc (monomial_1, c);
 
 fun poly_cmul c p =
-  if c = rat_0 then poly_0
+  if c = @0 then poly_0
   else FuncUtil.Monomialfunc.map (fn _ => fn x => c * x) p;
 
 fun poly_neg p = FuncUtil.Monomialfunc.map (K Rat.neg) p;
 
 
 fun poly_add p1 p2 =
-  FuncUtil.Monomialfunc.combine (curry op +) (fn x => x = rat_0) p1 p2;
+  FuncUtil.Monomialfunc.combine (curry op +) (fn x => x = @0) p1 p2;
 
 fun poly_sub p1 p2 = poly_add p1 (poly_neg p2);
 
 fun poly_cmmul (c,m) p =
-  if c = rat_0 then poly_0
+  if c = @0 then poly_0
   else
     if FuncUtil.Ctermfunc.is_empty m
     then FuncUtil.Monomialfunc.map (fn _ => fn d => c * d) p
@@ -209,7 +205,7 @@
 fun poly_square p = poly_mul p p;
 
 fun poly_pow p k =
-  if k = 0 then poly_const rat_1
+  if k = 0 then poly_const @1
   else if k = 1 then p
   else
     let val q = poly_square(poly_pow p (k div 2))
@@ -289,7 +285,7 @@
   let
     val n = dim v
     val strs =
-      map (decimalize 20 o (fn i => FuncUtil.Intfunc.tryapplyd (snd v) i rat_0)) (1 upto n)
+      map (decimalize 20 o (fn i => FuncUtil.Intfunc.tryapplyd (snd v) i @0)) (1 upto n)
   in space_implode " " strs ^ "\n" end;
 
 fun triple_int_ord ((a, b, c), (a', b', c')) =
@@ -302,7 +298,7 @@
   else index_char str chr (pos + 1);
 
 fun rat_of_quotient (a,b) =
-  if b = 0 then rat_0 else Rat.make (a, b);
+  if b = 0 then @0 else Rat.make (a, b);
 
 fun rat_of_string s =
   let val n = index_char s #"/" 0 in
@@ -336,7 +332,7 @@
 
 val exponent = ($$ "e" || $$ "E") |-- signed decimalint;
 
-val decimal = signed decimalsig -- (emptyin rat_0|| exponent)
+val decimal = signed decimalsig -- (emptyin @0|| exponent)
   >> (fn (h, x) => h * pow10 (int_of_rat x));
 
 fun mkparser p s =
@@ -372,12 +368,12 @@
 
 fun tri_scale_then solver (obj:vector) mats =
   let
-    val cd1 = fold_rev (common_denominator Inttriplefunc.fold) mats (rat_1)
-    val cd2 = common_denominator FuncUtil.Intfunc.fold (snd obj)  (rat_1)
+    val cd1 = fold_rev (common_denominator Inttriplefunc.fold) mats @1
+    val cd2 = common_denominator FuncUtil.Intfunc.fold (snd obj) @1
     val mats' = map (Inttriplefunc.map (fn _ => fn x => cd1 * x)) mats
     val obj' = vector_cmul cd2 obj
-    val max1 = fold_rev (maximal_element Inttriplefunc.fold) mats' (rat_0)
-    val max2 = maximal_element FuncUtil.Intfunc.fold (snd obj') (rat_0)
+    val max1 = fold_rev (maximal_element Inttriplefunc.fold) mats' @0
+    val max2 = maximal_element FuncUtil.Intfunc.fold (snd obj') @0
     val scal1 = pow2 (20 - int_of_float(Math.ln (float_of_rat max1) / Math.ln 2.0))
     val scal2 = pow2 (20 - int_of_float(Math.ln (float_of_rat max2) / Math.ln 2.0))
     val mats'' = map (Inttriplefunc.map (fn _ => fn x => x * scal1)) mats'
@@ -391,7 +387,7 @@
 fun nice_vector n ((d,v) : vector) =
   (d, FuncUtil.Intfunc.fold (fn (i,c) => fn a =>
       let val y = nice_rational n c in
-        if c = rat_0 then a
+        if c = @0 then a
         else FuncUtil.Intfunc.update (i,y) a
       end) v FuncUtil.Intfunc.empty): vector
 
@@ -400,16 +396,16 @@
 (* Stuff for "equations" ((int*int*int)->num functions).                         *)
 
 fun tri_equation_cmul c eq =
-  if c = rat_0 then Inttriplefunc.empty
+  if c = @0 then Inttriplefunc.empty
   else Inttriplefunc.map (fn _ => fn d => c * d) eq;
 
 fun tri_equation_add eq1 eq2 =
-  Inttriplefunc.combine (curry op +) (fn x => x = rat_0) eq1 eq2;
+  Inttriplefunc.combine (curry op +) (fn x => x = @0) eq1 eq2;
 
 fun tri_equation_eval assig eq =
   let
     fun value v = Inttriplefunc.apply assig v
-  in Inttriplefunc.fold (fn (v, c) => fn a => a + value v * c) eq rat_0 end;
+  in Inttriplefunc.fold (fn (v, c) => fn a => a + value v * c) eq @0 end;
 
 (* Eliminate all variables, in an essentially arbitrary order.               *)
 
@@ -440,8 +436,8 @@
               val eq' =
                 tri_equation_cmul ((Rat.of_int ~1) / a) (Inttriplefunc.delete_safe v eq)
               fun elim e =
-                let val b = Inttriplefunc.tryapplyd e v rat_0 in
-                  if b = rat_0 then e
+                let val b = Inttriplefunc.tryapplyd e v @0 in
+                  if b = @0 then e
                   else tri_equation_add e (tri_equation_cmul (Rat.neg b / a) eq)
                 end
             in
@@ -485,10 +481,10 @@
     if FuncUtil.Intpairfunc.is_empty (snd m) then []
     else
       let
-        val a11 = FuncUtil.Intpairfunc.tryapplyd (snd m) (i,i) rat_0
+        val a11 = FuncUtil.Intpairfunc.tryapplyd (snd m) (i,i) @0
       in
-        if a11 < rat_0 then raise Failure "diagonalize: not PSD"
-        else if a11 = rat_0 then
+        if a11 < @0 then raise Failure "diagonalize: not PSD"
+        else if a11 = @0 then
           if FuncUtil.Intfunc.is_empty (snd (row i m))
           then diagonalize n (i + 1) m
           else raise Failure "diagonalize: not PSD ___ "
@@ -498,19 +494,19 @@
             val v' =
               (fst v, FuncUtil.Intfunc.fold (fn (i, c) => fn a =>
                 let val y = c / a11
-                in if y = rat_0 then a else FuncUtil.Intfunc.update (i,y) a
+                in if y = @0 then a else FuncUtil.Intfunc.update (i,y) a
                 end) (snd v) FuncUtil.Intfunc.empty)
             fun upt0 x y a =
-              if y = rat_0 then a
+              if y = @0 then a
               else FuncUtil.Intpairfunc.update (x,y) a
             val m' =
               ((n, n),
                 iter (i + 1, n) (fn j =>
                   iter (i + 1, n) (fn k =>
                     (upt0 (j, k)
-                      (FuncUtil.Intpairfunc.tryapplyd (snd m) (j, k) rat_0 -
-                        FuncUtil.Intfunc.tryapplyd (snd v) j rat_0 *
-                        FuncUtil.Intfunc.tryapplyd (snd v') k rat_0))))
+                      (FuncUtil.Intpairfunc.tryapplyd (snd m) (j, k) @0 -
+                        FuncUtil.Intfunc.tryapplyd (snd v) j @0 *
+                        FuncUtil.Intfunc.tryapplyd (snd v') k @0))))
                     FuncUtil.Intpairfunc.empty)
           in (a11, v') :: diagonalize n (i + 1) m' end
       end
@@ -545,11 +541,11 @@
 (* Give the output polynomial and a record of how it was derived.            *)
 
 fun enumerate_products d pols =
-  if d = 0 then [(poly_const rat_1,RealArith.Rational_lt rat_1)]
+  if d = 0 then [(poly_const @1, RealArith.Rational_lt @1)]
   else if d < 0 then []
   else
     (case pols of
-      [] => [(poly_const rat_1, RealArith.Rational_lt rat_1)]
+      [] => [(poly_const @1, RealArith.Rational_lt @1)]
     | (p, b) :: ps =>
         let val e = multidegree p in
           if e = 0 then enumerate_products d ps
@@ -603,9 +599,9 @@
 
 (* 3D versions of matrix operations to consider blocks separately.           *)
 
-val bmatrix_add = Inttriplefunc.combine (curry op +) (fn x => x = rat_0);
+val bmatrix_add = Inttriplefunc.combine (curry op +) (fn x => x = @0);
 fun bmatrix_cmul c bm =
-  if c = rat_0 then Inttriplefunc.empty
+  if c = @0 then Inttriplefunc.empty
   else Inttriplefunc.map (fn _ => fn x => c * x) bm;
 
 val bmatrix_neg = bmatrix_cmul (Rat.of_int ~1);
@@ -641,7 +637,7 @@
         (pol :: eqs @ map fst leqs) []
     val monoid =
       if linf then
-        (poly_const rat_1,RealArith.Rational_lt rat_1)::
+        (poly_const @1, RealArith.Rational_lt @1)::
         (filter (fn (p,_) => multidegree p <= d) leqs)
       else enumerate_products d leqs
     val nblocks = length monoid
@@ -653,7 +649,7 @@
       in
         (mons,
           fold_rev (fn (m, n) =>
-            FuncUtil.Monomialfunc.update (m, Inttriplefunc.onefunc ((~k, ~n, n), rat_1)))
+            FuncUtil.Monomialfunc.update (m, Inttriplefunc.onefunc ((~k, ~n, n), @1)))
           nons FuncUtil.Monomialfunc.empty)
       end
 
@@ -670,7 +666,7 @@
                 if n1 > n2 then a
                 else
                   let
-                    val c = if n1 = n2 then rat_1 else rat_2
+                    val c = if n1 = n2 then @1 else @2
                     val e = FuncUtil.Monomialfunc.tryapplyd a m Inttriplefunc.empty
                   in
                     FuncUtil.Monomialfunc.update
@@ -690,13 +686,13 @@
     val (pvs, assig) = tri_eliminate_all_equations (0, 0, 0) eqns
     val qvars = (0, 0, 0) :: pvs
     val allassig =
-      fold_rev (fn v => Inttriplefunc.update (v, (Inttriplefunc.onefunc (v, rat_1)))) pvs assig
+      fold_rev (fn v => Inttriplefunc.update (v, (Inttriplefunc.onefunc (v, @1)))) pvs assig
     fun mk_matrix v =
       Inttriplefunc.fold (fn ((b, i, j), ass) => fn m =>
           if b < 0 then m
           else
-            let val c = Inttriplefunc.tryapplyd ass v rat_0 in
-              if c = rat_0 then m
+            let val c = Inttriplefunc.tryapplyd ass v @0 in
+              if c = @0 then m
               else Inttriplefunc.update ((b, j, i), c) (Inttriplefunc.update ((b, i, j), c) m)
             end)
         allassig Inttriplefunc.empty
@@ -709,12 +705,12 @@
     val obj =
       (length pvs,
         itern 1 pvs (fn v => fn i =>
-          FuncUtil.Intfunc.updatep iszero (i,Inttriplefunc.tryapplyd diagents v rat_0))
+          FuncUtil.Intfunc.updatep iszero (i,Inttriplefunc.tryapplyd diagents v @0))
           FuncUtil.Intfunc.empty)
     val raw_vec =
       if null pvs then vector_0 0
       else tri_scale_then (run_blockproblem prover nblocks blocksizes) obj mats
-    fun int_element (_, v) i = FuncUtil.Intfunc.tryapplyd v i rat_0
+    fun int_element (_, v) i = FuncUtil.Intfunc.tryapplyd v i @0
 
     fun find_rounding d =
       let
@@ -728,7 +724,7 @@
         val allmats = blocks blocksizes blockmat
       in (vec, map diag allmats) end
     val (vec, ratdias) =
-      if null pvs then find_rounding rat_1
+      if null pvs then find_rounding @1
       else tryfind find_rounding (map Rat.of_int (1 upto 31) @ map pow2 (5 upto 66))
     val newassigs =
       fold_rev (fn k => Inttriplefunc.update (nth pvs (k - 1), int_element vec k))
@@ -803,13 +799,13 @@
         fun trivial_axiom (p, ax) =
           (case ax of
             RealArith.Axiom_eq n =>
-              if eval FuncUtil.Ctermfunc.empty p <> Rat.zero then nth eqs n
+              if eval FuncUtil.Ctermfunc.empty p <> @0 then nth eqs n
               else raise Failure "trivial_axiom: Not a trivial axiom"
           | RealArith.Axiom_le n =>
-              if eval FuncUtil.Ctermfunc.empty p < Rat.zero then nth les n
+              if eval FuncUtil.Ctermfunc.empty p < @0 then nth les n
               else raise Failure "trivial_axiom: Not a trivial axiom"
           | RealArith.Axiom_lt n =>
-              if eval FuncUtil.Ctermfunc.empty p <= Rat.zero then nth lts n
+              if eval FuncUtil.Ctermfunc.empty p <= @0 then nth lts n
               else raise Failure "trivial_axiom: Not a trivial axiom"
           | _ => error "trivial_axiom: Not a trivial axiom")
       in
@@ -834,7 +830,7 @@
               | Prover prover =>
                   (* call prover *)
                   let
-                    val pol = fold_rev poly_mul (map fst ltp) (poly_const Rat.one)
+                    val pol = fold_rev poly_mul (map fst ltp) (poly_const @1)
                     val leq = lep @ ltp
                     fun tryall d =
                       let
@@ -852,11 +848,11 @@
                       map2 (fn q => fn (_,ax) => RealArith.Eqmul(q,ax)) cert_ideal eq
                     val proofs_cone = map cterm_of_sos cert_cone
                     val proof_ne =
-                      if null ltp then RealArith.Rational_lt Rat.one
+                      if null ltp then RealArith.Rational_lt @1
                       else
                         let val p = foldr1 RealArith.Product (map snd ltp) in
                           funpow i (fn q => RealArith.Product (p, q))
-                            (RealArith.Rational_lt Rat.one)
+                            (RealArith.Rational_lt @1)
                         end
                   in
                     foldr1 RealArith.Sum (proof_ne :: proofs_ideal @ proofs_cone)
@@ -892,7 +888,7 @@
   fun substitutable_monomial fvs tm =
     (case Thm.term_of tm of
       Free (_, @{typ real}) =>
-        if not (member (op aconvc) fvs tm) then (Rat.one, tm)
+        if not (member (op aconvc) fvs tm) then (@1, tm)
         else raise Failure "substitutable_monomial"
     | @{term "op * :: real => _"} $ _ $ (Free _) =>
         if RealArith.is_ratconst (Thm.dest_arg1 tm) andalso
diff -r 921a5be54132 -r 97b721666890 src/HOL/Library/positivstellensatz.ML
--- a/src/HOL/Library/positivstellensatz.ML	Wed Jun 01 15:01:43 2016 +0200
+++ b/src/HOL/Library/positivstellensatz.ML	Wed Jun 01 15:10:27 2016 +0200
@@ -338,7 +338,7 @@
 
 fun cterm_of_cmonomial (m,c) =
   if FuncUtil.Ctermfunc.is_empty m then cterm_of_rat c
-  else if c = Rat.one then cterm_of_monomial m
+  else if c = @1 then cterm_of_monomial m
   else Thm.apply (Thm.apply @{cterm "op *::real => _"} (cterm_of_rat c)) (cterm_of_monomial m);
 
 fun cterm_of_poly p =
@@ -585,35 +585,35 @@
 
 (* A linear arithmetic prover *)
 local
-  val linear_add = FuncUtil.Ctermfunc.combine (curry op +) (fn z => z = Rat.zero)
+  val linear_add = FuncUtil.Ctermfunc.combine (curry op +) (fn z => z = @0)
   fun linear_cmul c = FuncUtil.Ctermfunc.map (fn _ => fn x => c * x)
   val one_tm = @{cterm "1::real"}
-  fun contradictory p (e,_) = ((FuncUtil.Ctermfunc.is_empty e) andalso not(p Rat.zero)) orelse
+  fun contradictory p (e,_) = ((FuncUtil.Ctermfunc.is_empty e) andalso not(p @0)) orelse
      ((eq_set (op aconvc) (FuncUtil.Ctermfunc.dom e, [one_tm])) andalso
        not(p(FuncUtil.Ctermfunc.apply e one_tm)))
 
   fun linear_ineqs vars (les,lts) =
-    case find_first (contradictory (fn x => x > Rat.zero)) lts of
+    case find_first (contradictory (fn x => x > @0)) lts of
       SOME r => r
     | NONE =>
-      (case find_first (contradictory (fn x => x > Rat.zero)) les of
+      (case find_first (contradictory (fn x => x > @0)) les of
          SOME r => r
        | NONE =>
          if null vars then error "linear_ineqs: no contradiction" else
          let
            val ineqs = les @ lts
            fun blowup v =
-             length(filter (fn (e,_) => FuncUtil.Ctermfunc.tryapplyd e v Rat.zero = Rat.zero) ineqs) +
-             length(filter (fn (e,_) => FuncUtil.Ctermfunc.tryapplyd e v Rat.zero > Rat.zero) ineqs) *
-             length(filter (fn (e,_) => FuncUtil.Ctermfunc.tryapplyd e v Rat.zero < Rat.zero) ineqs)
+             length(filter (fn (e,_) => FuncUtil.Ctermfunc.tryapplyd e v @0 = @0) ineqs) +
+             length(filter (fn (e,_) => FuncUtil.Ctermfunc.tryapplyd e v @0 > @0) ineqs) *
+             length(filter (fn (e,_) => FuncUtil.Ctermfunc.tryapplyd e v @0 < @0) ineqs)
            val v = fst(hd(sort (fn ((_,i),(_,j)) => int_ord (i,j))
              (map (fn v => (v,blowup v)) vars)))
            fun addup (e1,p1) (e2,p2) acc =
              let
-               val c1 = FuncUtil.Ctermfunc.tryapplyd e1 v Rat.zero
-               val c2 = FuncUtil.Ctermfunc.tryapplyd e2 v Rat.zero
+               val c1 = FuncUtil.Ctermfunc.tryapplyd e1 v @0
+               val c2 = FuncUtil.Ctermfunc.tryapplyd e2 v @0
              in
-               if c1 * c2 >= Rat.zero then acc else
+               if c1 * c2 >= @0 then acc else
                let
                  val e1' = linear_cmul (Rat.abs c2) e1
                  val e2' = linear_cmul (Rat.abs c1) e2
@@ -623,13 +623,13 @@
                end
              end
            val (les0,les1) =
-             List.partition (fn (e,_) => FuncUtil.Ctermfunc.tryapplyd e v Rat.zero = Rat.zero) les
+             List.partition (fn (e,_) => FuncUtil.Ctermfunc.tryapplyd e v @0 = @0) les
            val (lts0,lts1) =
-             List.partition (fn (e,_) => FuncUtil.Ctermfunc.tryapplyd e v Rat.zero = Rat.zero) lts
+             List.partition (fn (e,_) => FuncUtil.Ctermfunc.tryapplyd e v @0 = @0) lts
            val (lesp,lesn) =
-             List.partition (fn (e,_) => FuncUtil.Ctermfunc.tryapplyd e v Rat.zero > Rat.zero) les1
+             List.partition (fn (e,_) => FuncUtil.Ctermfunc.tryapplyd e v @0 > @0) les1
            val (ltsp,ltsn) =
-             List.partition (fn (e,_) => FuncUtil.Ctermfunc.tryapplyd e v Rat.zero > Rat.zero) lts1
+             List.partition (fn (e,_) => FuncUtil.Ctermfunc.tryapplyd e v @0 > @0) lts1
            val les' = fold_rev (fn ep1 => fold_rev (addup ep1) lesp) lesn les0
            val lts' = fold_rev (fn ep1 => fold_rev (addup ep1) (lesp@ltsp)) ltsn
                       (fold_rev (fn ep1 => fold_rev (addup ep1) (lesn@ltsn)) ltsp lts0)
@@ -637,7 +637,7 @@
          end)
 
   fun linear_eqs(eqs,les,lts) =
-    case find_first (contradictory (fn x => x = Rat.zero)) eqs of
+    case find_first (contradictory (fn x => x = @0)) eqs of
       SOME r => r
     | NONE =>
       (case eqs of
@@ -650,8 +650,8 @@
          let
            val (x,c) = FuncUtil.Ctermfunc.choose (FuncUtil.Ctermfunc.delete_safe one_tm e)
            fun xform (inp as (t,q)) =
-             let val d = FuncUtil.Ctermfunc.tryapplyd t x Rat.zero in
-               if d = Rat.zero then inp else
+             let val d = FuncUtil.Ctermfunc.tryapplyd t x @0 in
+               if d = @0 then inp else
                let
                  val k = (Rat.neg d) * Rat.abs c / c
                  val e' = linear_cmul k e
@@ -674,12 +674,12 @@
 
   fun lin_of_hol ct =
     if ct aconvc @{cterm "0::real"} then FuncUtil.Ctermfunc.empty
-    else if not (is_comb ct) then FuncUtil.Ctermfunc.onefunc (ct, Rat.one)
+    else if not (is_comb ct) then FuncUtil.Ctermfunc.onefunc (ct, @1)
     else if is_ratconst ct then FuncUtil.Ctermfunc.onefunc (one_tm, dest_ratconst ct)
     else
       let val (lop,r) = Thm.dest_comb ct
       in
-        if not (is_comb lop) then FuncUtil.Ctermfunc.onefunc (ct, Rat.one)
+        if not (is_comb lop) then FuncUtil.Ctermfunc.onefunc (ct, @1)
         else
           let val (opr,l) = Thm.dest_comb lop
           in
@@ -687,7 +687,7 @@
             then linear_add (lin_of_hol l) (lin_of_hol r)
             else if opr aconvc @{cterm "op * :: real =>_"}
                     andalso is_ratconst l then FuncUtil.Ctermfunc.onefunc (r, dest_ratconst l)
-            else FuncUtil.Ctermfunc.onefunc (ct, Rat.one)
+            else FuncUtil.Ctermfunc.onefunc (ct, @1)
           end
       end
 
@@ -707,7 +707,7 @@
     val aliens = filter is_alien
       (fold_rev (union (op aconvc) o FuncUtil.Ctermfunc.dom)
                 (eq_pols @ le_pols @ lt_pols) [])
-    val le_pols' = le_pols @ map (fn v => FuncUtil.Ctermfunc.onefunc (v,Rat.one)) aliens
+    val le_pols' = le_pols @ map (fn v => FuncUtil.Ctermfunc.onefunc (v,@1)) aliens
     val (_,proof) = linear_prover (eq_pols,le_pols',lt_pols)
     val le' = le @ map (fn a => Thm.instantiate' [] [SOME (Thm.dest_arg a)] @{thm of_nat_0_le_iff}) aliens
   in ((translator (eq,le',lt) proof), Trivial)
diff -r 921a5be54132 -r 97b721666890 src/HOL/Multivariate_Analysis/normarith.ML
--- a/src/HOL/Multivariate_Analysis/normarith.ML	Wed Jun 01 15:01:43 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/normarith.ML	Wed Jun 01 15:10:27 2016 +0200
@@ -28,14 +28,14 @@
             find_normedterms (Thm.dest_arg1 t) (find_normedterms (Thm.dest_arg t) acc)
       | @{term "op * :: real => _"}$_$_ =>
             if not (is_ratconst (Thm.dest_arg1 t)) then acc else
-            augment_norm (dest_ratconst (Thm.dest_arg1 t) >= Rat.zero)
+            augment_norm (dest_ratconst (Thm.dest_arg1 t) >= @0)
                       (Thm.dest_arg t) acc
       | _ => augment_norm true t acc
 
  val cterm_lincomb_neg = FuncUtil.Ctermfunc.map (K Rat.neg)
  fun cterm_lincomb_cmul c t =
-    if c = Rat.zero then FuncUtil.Ctermfunc.empty else FuncUtil.Ctermfunc.map (fn _ => fn x => x * c) t
- fun cterm_lincomb_add l r = FuncUtil.Ctermfunc.combine (curry op +) (fn x => x = Rat.zero) l r
+    if c = @0 then FuncUtil.Ctermfunc.empty else FuncUtil.Ctermfunc.map (fn _ => fn x => x * c) t
+ fun cterm_lincomb_add l r = FuncUtil.Ctermfunc.combine (curry op +) (fn x => x = @0) l r
  fun cterm_lincomb_sub l r = cterm_lincomb_add l (cterm_lincomb_neg r)
  fun cterm_lincomb_eq l r = FuncUtil.Ctermfunc.is_empty (cterm_lincomb_sub l r)
 
@@ -43,8 +43,8 @@
  val int_lincomb_neg = FuncUtil.Intfunc.map (K Rat.neg)
 *)
  fun int_lincomb_cmul c t =
-    if c = Rat.zero then FuncUtil.Intfunc.empty else FuncUtil.Intfunc.map (fn _ => fn x => x * c) t
- fun int_lincomb_add l r = FuncUtil.Intfunc.combine (curry op +) (fn x => x = Rat.zero) l r
+    if c = @0 then FuncUtil.Intfunc.empty else FuncUtil.Intfunc.map (fn _ => fn x => x * c) t
+ fun int_lincomb_add l r = FuncUtil.Intfunc.combine (curry op +) (fn x => x = @0) l r
 (*
  fun int_lincomb_sub l r = int_lincomb_add l (int_lincomb_neg r)
  fun int_lincomb_eq l r = FuncUtil.Intfunc.is_empty (int_lincomb_sub l r)
@@ -64,11 +64,11 @@
    let
      val b = ((snd o HOLogic.dest_number o term_of o Thm.dest_arg) t = 0
                handle TERM _=> false)
-   in if b then FuncUtil.Ctermfunc.onefunc (t,Rat.one)
+   in if b then FuncUtil.Ctermfunc.onefunc (t,@1)
       else FuncUtil.Ctermfunc.empty
    end
 *)
- | _ => FuncUtil.Ctermfunc.onefunc (t,Rat.one)
+ | _ => FuncUtil.Ctermfunc.onefunc (t,@1)
 
  fun vector_lincombs ts =
   fold_rev
@@ -84,7 +84,7 @@
 fun replacenegnorms cv t = case Thm.term_of t of
   @{term "op + :: real => _"}$_$_ => binop_conv (replacenegnorms cv) t
 | @{term "op * :: real => _"}$_$_ =>
-    if dest_ratconst (Thm.dest_arg1 t) < Rat.zero then arg_conv cv t else Thm.reflexive t
+    if dest_ratconst (Thm.dest_arg1 t) < @0 then arg_conv cv t else Thm.reflexive t
 | _ => Thm.reflexive t
 (*
 fun flip v eq =
@@ -97,10 +97,10 @@
                map (cons a) res @ res end
 fun evaluate env lin =
  FuncUtil.Intfunc.fold (fn (x,c) => fn s => s + c * (FuncUtil.Intfunc.apply env x))
-   lin Rat.zero
+   lin @0
 
 fun solve (vs,eqs) = case (vs,eqs) of
-  ([],[]) => SOME (FuncUtil.Intfunc.onefunc (0,Rat.one))
+  ([],[]) => SOME (FuncUtil.Intfunc.onefunc (0,@1))
  |(_,eq::oeqs) =>
    (case filter (member (op =) vs) (FuncUtil.Intfunc.dom eq) of (*FIXME use find_first here*)
      [] => NONE
@@ -127,9 +127,9 @@
  let
   fun vertex cmb = case solve(vs,cmb) of
     NONE => NONE
-   | SOME soln => SOME (map (fn v => FuncUtil.Intfunc.tryapplyd soln v Rat.zero) vs)
+   | SOME soln => SOME (map (fn v => FuncUtil.Intfunc.tryapplyd soln v @0) vs)
   val rawvs = map_filter vertex (combinations (length vs) eqs)
-  val unset = filter (forall (fn c => c >= Rat.zero)) rawvs
+  val unset = filter (forall (fn c => c >= @0)) rawvs
  in fold_rev (insert (eq_list op =)) unset []
  end
 
@@ -242,7 +242,7 @@
 (* FIXME
 | Const(@{const_name vec},_)$n =>
   let val n = Thm.dest_arg ct
-  in if is_ratconst n andalso not (dest_ratconst n =/ Rat.zero)
+  in if is_ratconst n andalso not (dest_ratconst n =/ @0)
      then Thm.reflexive ct else apply_pth1 ct
   end
 *)
@@ -288,7 +288,7 @@
       in fold_rev (fn (f,v) => fn g => if FuncUtil.Ctermfunc.defined f x then FuncUtil.Intfunc.update (v, FuncUtil.Ctermfunc.apply f x) g else g) srccombs inp
       end
      val equations = map coefficients vvs
-     val inequalities = map (fn n => FuncUtil.Intfunc.onefunc (n,Rat.one)) nvs
+     val inequalities = map (fn n => FuncUtil.Intfunc.onefunc (n,@1)) nvs
      fun plausiblevertices f =
       let
        val flippedequations = map (fold_rev int_flip f) equations
@@ -296,8 +296,8 @@
        val rawverts = vertices nvs constraints
        fun check_solution v =
         let
-          val f = fold_rev FuncUtil.Intfunc.update (nvs ~~ v) (FuncUtil.Intfunc.onefunc (0, Rat.one))
-        in forall (fn e => evaluate f e = Rat.zero) flippedequations
+          val f = fold_rev FuncUtil.Intfunc.update (nvs ~~ v) (FuncUtil.Intfunc.onefunc (0, @1))
+        in forall (fn e => evaluate f e = @0) flippedequations
         end
        val goodverts = filter check_solution rawverts
        val signfixups = map (fn n => if member (op =) f n then ~1 else 1) nvs
@@ -308,7 +308,7 @@
     end
    fun compute_ineq v =
     let
-     val ths = map_filter (fn (v,t) => if v = Rat.zero then NONE
+     val ths = map_filter (fn (v,t) => if v = @0 then NONE
                                      else SOME(norm_cmul_rule v t))
                             (v ~~ nubs)
      fun end_itlist f xs = split_last xs |> uncurry (fold_rev f)
diff -r 921a5be54132 -r 97b721666890 src/HOL/Tools/groebner.ML
--- a/src/HOL/Tools/groebner.ML	Wed Jun 01 15:01:43 2016 +0200
+++ b/src/HOL/Tools/groebner.ML	Wed Jun 01 15:10:27 2016 +0200
@@ -32,8 +32,6 @@
   if is_binop ct ct' then Thm.dest_binop ct'
   else raise CTERM ("dest_binary: bad binop", [ct, ct'])
 
-val rat_0 = Rat.zero;
-val rat_1 = Rat.one;
 val minus_rat = Rat.neg;
 val denominator_rat = Rat.dest #> snd #> Rat.of_int;
 fun int_of_rat a =
@@ -81,7 +79,7 @@
   | ((c1,m1)::o1,(c2,m2)::o2) =>
         if m1 = m2 then
           let val c = c1 + c2 val rest = grob_add o1 o2 in
-          if c = rat_0 then rest else (c,m1)::rest end
+          if c = @0 then rest else (c,m1)::rest end
         else if morder_lt m2 m1 then (c1,m1)::(grob_add o1 l2)
         else (c2,m2)::(grob_add l1 o2);
 
@@ -99,22 +97,22 @@
 fun grob_inv l =
   case l of
     [(c,vs)] => if (forall (fn x => x = 0) vs) then
-                  if (c = rat_0) then error "grob_inv: division by zero"
-                  else [(rat_1 / c,vs)]
+                  if c = @0 then error "grob_inv: division by zero"
+                  else [(@1 / c,vs)]
               else error "grob_inv: non-constant divisor polynomial"
   | _ => error "grob_inv: non-constant divisor polynomial";
 
 fun grob_div l1 l2 =
   case l2 of
     [(c,l)] => if (forall (fn x => x = 0) l) then
-                 if c = rat_0 then error "grob_div: division by zero"
-                 else grob_cmul (rat_1 / c,l) l1
+                 if c = @0 then error "grob_div: division by zero"
+                 else grob_cmul (@1 / c,l) l1
              else error "grob_div: non-constant divisor polynomial"
   | _ => error "grob_div: non-constant divisor polynomial";
 
 fun grob_pow vars l n =
   if n < 0 then error "grob_pow: negative power"
-  else if n = 0 then [(rat_1,map (K 0) vars)]
+  else if n = 0 then [(@1,map (K 0) vars)]
   else grob_mul l (grob_pow vars l (n - 1));
 
 (* Monomial division operation. *)
@@ -125,7 +123,7 @@
 
 (* Lowest common multiple of two monomials. *)
 
-fun mlcm (_,m1) (_,m2) = (rat_1, ListPair.map Int.max (m1, m2));
+fun mlcm (_,m1) (_,m2) = (@1, ListPair.map Int.max (m1, m2));
 
 (* Reduce monomial cm by polynomial pol, returning replacement for cm.  *)
 
@@ -179,7 +177,7 @@
   if null pol then (pol,hist) else
   let val (c',m') = hd pol in
   (map (fn (c,m) => (c / c',m)) pol,
-   Mmul((rat_1 / c',map (K 0) m'),hist)) end;
+   Mmul((@1 / c',map (K 0) m'),hist)) end;
 
 (* The most popular heuristic is to order critical pairs by LCM monomial.    *)
 
@@ -299,7 +297,7 @@
 fun resolve_proof vars prf =
   case prf of
     Start(~1) => []
-  | Start m => [(m,[(rat_1,map (K 0) vars)])]
+  | Start m => [(m,[(@1,map (K 0) vars)])]
   | Mmul(pol,lin) =>
         let val lis = resolve_proof vars lin in
             map (fn (n,p) => (n,grob_cmul pol p)) lis end
@@ -317,7 +315,7 @@
 fun grobner_weak vars pols =
     let val cert = resolve_proof vars (grobner_refute pols)
         val l =
-            fold_rev (fold_rev (lcm_rat o denominator_rat o fst) o snd) cert (rat_1) in
+            fold_rev (fold_rev (lcm_rat o denominator_rat o fst) o snd) cert @1 in
         (l,map (fn (i,p) => (i,map (fn (d,m) => (l * d,m)) p)) cert) end;
 
 (* Prove a polynomial is in ideal generated by others, using Grobner basis.  *)
@@ -331,8 +329,8 @@
 
 fun grobner_strong vars pols pol =
     let val vars' = @{cterm "True"}::vars
-        val grob_z = [(rat_1,1::(map (K 0) vars))]
-        val grob_1 = [(rat_1,(map (K 0) vars'))]
+        val grob_z = [(@1, 1::(map (K 0) vars))]
+        val grob_1 = [(@1, (map (K 0) vars'))]
         fun augment p= map (fn (c,m) => (c,0::m)) p
         val pols' = map augment pols
         val pol' = augment pol
@@ -605,10 +603,10 @@
 
 fun grobify_term vars tm =
 ((if not (member (op aconvc) vars tm) then raise CTERM ("Not a variable", [tm]) else
-     [(rat_1,map (fn i => if i aconvc tm then 1 else 0) vars)])
+     [(@1, map (fn i => if i aconvc tm then 1 else 0) vars)])
 handle  CTERM _ =>
  ((let val x = dest_const tm
- in if x = rat_0 then [] else [(x,map (K 0) vars)]
+ in if x = @0 then [] else [(x,map (K 0) vars)]
  end)
  handle ERROR _ =>
   ((grob_neg(grobify_term vars (ring_dest_neg tm)))
@@ -662,15 +660,15 @@
    in end_itlist ring_mk_mul (mk_const c :: xps)
   end
  fun holify_polynomial vars p =
-     if null p then mk_const (rat_0)
+     if null p then mk_const @0
      else end_itlist ring_mk_add (map (holify_monomial vars) p)
  in holify_polynomial
  end ;
 
 fun idom_rule ctxt = simplify (put_simpset HOL_basic_ss ctxt addsimps [idom_thm]);
 fun prove_nz n = eqF_elim
-                 (ring_eq_conv(mk_binop eq_tm (mk_const n) (mk_const(rat_0))));
-val neq_01 = prove_nz (rat_1);
+                 (ring_eq_conv(mk_binop eq_tm (mk_const n) (mk_const @0)));
+val neq_01 = prove_nz @1;
 fun neq_rule n th = [prove_nz n, th] MRS neq_thm;
 fun mk_add th1 = Thm.combination (Drule.arg_cong_rule ring_add_tm th1);
 
@@ -712,13 +710,13 @@
        val th2 = funpow deg (idom_rule ctxt o HOLogic.conj_intr ctxt th1) neq_01
       in (vars,l,cert,th2)
       end)
-    val cert_pos = map (fn (i,p) => (i,filter (fn (c,_) => c > rat_0) p)) cert
+    val cert_pos = map (fn (i,p) => (i,filter (fn (c,_) => c > @0) p)) cert
     val cert_neg = map (fn (i,p) => (i,map (fn (c,m) => (minus_rat c,m))
-                                            (filter (fn (c,_) => c < rat_0) p))) cert
+                                            (filter (fn (c,_) => c < @0) p))) cert
     val  herts_pos = map (fn (i,p) => (i,holify_polynomial vars p)) cert_pos
     val  herts_neg = map (fn (i,p) => (i,holify_polynomial vars p)) cert_neg
     fun thm_fn pols =
-        if null pols then Thm.reflexive(mk_const rat_0) else
+        if null pols then Thm.reflexive(mk_const @0) else
         end_itlist mk_add
             (map (fn (i,p) => Drule.arg_cong_rule (Thm.apply ring_mul_tm p)
               (nth eths i |> mk_meta_eq)) pols)
diff -r 921a5be54132 -r 97b721666890 src/HOL/Tools/lin_arith.ML
--- a/src/HOL/Tools/lin_arith.ML	Wed Jun 01 15:01:43 2016 +0200
+++ b/src/HOL/Tools/lin_arith.ML	Wed Jun 01 15:10:27 2016 +0200
@@ -156,11 +156,11 @@
          if we choose to do so here, the simpset used by arith must be able to
          perform the same simplifications. *)
       (* quotient 's / t', where the denominator t can be NONE *)
-      (* Note: will raise Rat.DIVZERO iff m' is Rat.zero *)
+      (* Note: will raise Rat.DIVZERO iff m' is @0 *)
       if of_field_sort thy (domain_type T) then
         let
           val (os',m') = demult (s, m);
-          val (ot',p) = demult (t, Rat.one)
+          val (ot',p) = demult (t, @1)
         in (case (os',ot') of
             (SOME s', SOME t') => SOME (mC $ s' $ t')
           | (SOME s', NONE) => SOME s'
@@ -172,7 +172,7 @@
       else (SOME atom, m)
     (* terms that evaluate to numeric constants *)
     | demult (Const (@{const_name Groups.uminus}, _) $ t, m) = demult (t, Rat.neg m)
-    | demult (Const (@{const_name Groups.zero}, _), _) = (NONE, Rat.zero)
+    | demult (Const (@{const_name Groups.zero}, _), _) = (NONE, @0)
     | demult (Const (@{const_name Groups.one}, _), m) = (NONE, m)
     (*Warning: in rare cases (neg_)numeral encloses a non-numeral,
       in which case dest_numeral raises TERM; hence all the handles below.
@@ -227,8 +227,8 @@
         if member (op =) inj_consts f then poly (x, m, pi) else add_atom all m pi
     | poly (all, m, pi) =
         add_atom all m pi
-  val (p, i) = poly (lhs, Rat.one, ([], Rat.zero))
-  val (q, j) = poly (rhs, Rat.one, ([], Rat.zero))
+  val (p, i) = poly (lhs, @1, ([], @0))
+  val (q, j) = poly (rhs, @1, ([], @0))
 in
   case rel of
     @{const_name Orderings.less}    => SOME (p, i, "<", q, j)