src/HOL/Library/Sum_of_Squares/positivstellensatz_tools.ML
changeset 63205 97b721666890
parent 63201 f151704c08e4
child 63208 3251e9dfea91
equal deleted inserted replaced
63204:921a5be54132 63205:97b721666890
    48       val vps = fold_rev (fn (x,k) => cons (string_of_varpow x k)) m' []
    48       val vps = fold_rev (fn (x,k) => cons (string_of_varpow x k)) m' []
    49     in foldr1 (fn (s, t) => s ^ "*" ^ t) vps end
    49     in foldr1 (fn (s, t) => s ^ "*" ^ t) vps end
    50 
    50 
    51 fun string_of_cmonomial (m,c) =
    51 fun string_of_cmonomial (m,c) =
    52   if FuncUtil.Ctermfunc.is_empty m then string_of_rat c
    52   if FuncUtil.Ctermfunc.is_empty m then string_of_rat c
    53   else if c = Rat.one then string_of_monomial m
    53   else if c = @1 then string_of_monomial m
    54   else string_of_rat c ^ "*" ^ string_of_monomial m
    54   else string_of_rat c ^ "*" ^ string_of_monomial m
    55 
    55 
    56 fun string_of_poly p =
    56 fun string_of_poly p =
    57   if FuncUtil.Monomialfunc.is_empty p then "0"
    57   if FuncUtil.Monomialfunc.is_empty p then "0"
    58   else
    58   else
   119 fun parse_monomial ctxt = repeat_sep "*" (parse_varpow ctxt) >>
   119 fun parse_monomial ctxt = repeat_sep "*" (parse_varpow ctxt) >>
   120   (fn xs => fold FuncUtil.Ctermfunc.update xs FuncUtil.Ctermfunc.empty)
   120   (fn xs => fold FuncUtil.Ctermfunc.update xs FuncUtil.Ctermfunc.empty)
   121 
   121 
   122 fun parse_cmonomial ctxt =
   122 fun parse_cmonomial ctxt =
   123   rat_int --| str "*" -- (parse_monomial ctxt) >> swap ||
   123   rat_int --| str "*" -- (parse_monomial ctxt) >> swap ||
   124   (parse_monomial ctxt) >> (fn m => (m, Rat.one)) ||
   124   (parse_monomial ctxt) >> (fn m => (m, @1)) ||
   125   rat_int >> (fn r => (FuncUtil.Ctermfunc.empty, r))
   125   rat_int >> (fn r => (FuncUtil.Ctermfunc.empty, r))
   126 
   126 
   127 fun parse_poly ctxt = repeat_sep "+" (parse_cmonomial ctxt) >>
   127 fun parse_poly ctxt = repeat_sep "+" (parse_cmonomial ctxt) >>
   128   (fn xs => fold FuncUtil.Monomialfunc.update xs FuncUtil.Monomialfunc.empty)
   128   (fn xs => fold FuncUtil.Monomialfunc.update xs FuncUtil.Monomialfunc.empty)
   129 
   129