src/HOL/Library/positivstellensatz.ML

     in foldr1 (fn (s, t) => Thm.apply (Thm.apply @{cterm "op * :: real => _"} s) t) vps
     end
 
 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 =
   if FuncUtil.Monomialfunc.is_empty p then @{cterm "0::real"}
   else

   in f
   end;
 
 (* 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
                  val p1' = Product(Rational_lt(Rat.abs c2),p1)
                  val p2' = Product(Rational_lt(Rat.abs c1),p2)
                in (linear_add e1' e2',Sum(p1',p2'))::acc
                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)
          in linear_ineqs (remove (op aconvc) v vars) (les',lts')
          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
          [] =>
          let val vars = remove (op aconvc) one_tm

        | (e,p)::es =>
          if FuncUtil.Ctermfunc.is_empty e then linear_eqs (es,les,lts) else
          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
                  val t' = linear_cmul (Rat.abs c) t
                  val p' = Eqmul(FuncUtil.Monomialfunc.onefunc (FuncUtil.Ctermfunc.empty, k),p)

     in linear_eqs(eqs,les,lts)
     end
 
   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
             if opr aconvc @{cterm "op + :: real =>_"}
             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
 
   fun is_alien ct =
     case Thm.term_of ct of

     val le_pols = map rhs le
     val lt_pols = map rhs lt
     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)
   end
 end;