src/HOL/Library/Sum_of_Squares/positivstellensatz_tools.ML
changeset 63201 f151704c08e4
parent 59621 291934bac95e
child 63205 97b721666890
equal deleted inserted replaced
63200:6eccfe9f5ef1 63201:f151704c08e4
    18 
    18 
    19 local
    19 local
    20 
    20 
    21 fun string_of_rat r =
    21 fun string_of_rat r =
    22   let
    22   let
    23     val (nom, den) = Rat.quotient_of_rat r
    23     val (nom, den) = Rat.dest r
    24   in
    24   in
    25     if den = 1 then string_of_int nom
    25     if den = 1 then string_of_int nom
    26     else string_of_int nom ^ "/" ^ string_of_int den
    26     else string_of_int nom ^ "/" ^ string_of_int den
    27   end
    27   end
    28 
    28 
   101   Scan.repeat1 (Scan.one Symbol.is_ascii_digit >> (fn s => ord s - ord "0"))
   101   Scan.repeat1 (Scan.one Symbol.is_ascii_digit >> (fn s => ord s - ord "0"))
   102     >> foldl1 (fn (n, d) => n * 10 + d)
   102     >> foldl1 (fn (n, d) => n * 10 + d)
   103 
   103 
   104 val nat = number
   104 val nat = number
   105 val int = Scan.optional (str "~" >> K ~1) 1 -- nat >> op *
   105 val int = Scan.optional (str "~" >> K ~1) 1 -- nat >> op *
   106 val rat = int --| str "/" -- int >> Rat.rat_of_quotient
   106 val rat = int --| str "/" -- int >> Rat.make
   107 val rat_int = rat || int >> Rat.rat_of_int
   107 val rat_int = rat || int >> Rat.of_int
   108 
   108 
   109 
   109 
   110 (* polynomial parsers *)
   110 (* polynomial parsers *)
   111 
   111 
   112 fun repeat_sep s f = f ::: Scan.repeat (str s |-- f)
   112 fun repeat_sep s f = f ::: Scan.repeat (str s |-- f)