src/HOL/Library/Sum_of_Squares/positivstellensatz_tools.ML
changeset 63208 3251e9dfea91
parent 63205 97b721666890
child 67271 48ef58c6cf4c
--- a/src/HOL/Library/Sum_of_Squares/positivstellensatz_tools.ML	Wed Jun 01 15:19:44 2016 +0200
+++ b/src/HOL/Library/Sum_of_Squares/positivstellensatz_tools.ML	Wed Jun 01 15:33:45 2016 +0200
@@ -18,15 +18,6 @@
 
 local
 
-fun string_of_rat r =
-  let
-    val (nom, den) = Rat.dest r
-  in
-    if den = 1 then string_of_int nom
-    else string_of_int nom ^ "/" ^ string_of_int den
-  end
-
-
 (* map polynomials to strings *)
 
 fun string_of_varpow x k =
@@ -49,9 +40,9 @@
     in foldr1 (fn (s, t) => s ^ "*" ^ t) vps end
 
 fun string_of_cmonomial (m,c) =
-  if FuncUtil.Ctermfunc.is_empty m then string_of_rat c
+  if FuncUtil.Ctermfunc.is_empty m then Rat.string_of_rat c
   else if c = @1 then string_of_monomial m
-  else string_of_rat c ^ "*" ^ string_of_monomial m
+  else Rat.string_of_rat c ^ "*" ^ string_of_monomial m
 
 fun string_of_poly p =
   if FuncUtil.Monomialfunc.is_empty p then "0"
@@ -67,9 +58,9 @@
 fun pss_to_cert (RealArith.Axiom_eq i) = "A=" ^ string_of_int i
   | pss_to_cert (RealArith.Axiom_le i) = "A<=" ^ string_of_int i
   | pss_to_cert (RealArith.Axiom_lt i) = "A<" ^ string_of_int i
-  | pss_to_cert (RealArith.Rational_eq r) = "R=" ^ string_of_rat r
-  | pss_to_cert (RealArith.Rational_le r) = "R<=" ^ string_of_rat r
-  | pss_to_cert (RealArith.Rational_lt r) = "R<" ^ string_of_rat r
+  | pss_to_cert (RealArith.Rational_eq r) = "R=" ^ Rat.string_of_rat r
+  | pss_to_cert (RealArith.Rational_le r) = "R<=" ^ Rat.string_of_rat r
+  | pss_to_cert (RealArith.Rational_lt r) = "R<" ^ Rat.string_of_rat r
   | pss_to_cert (RealArith.Square p) = "[" ^ string_of_poly p ^ "]^2"
   | pss_to_cert (RealArith.Eqmul (p, pss)) =
       "([" ^ string_of_poly p ^ "] * " ^ pss_to_cert pss ^ ")"