src/HOL/Library/Sum_of_Squares/positivstellensatz_tools.ML
changeset 67271 48ef58c6cf4c
parent 63208 3251e9dfea91
equal deleted inserted replaced
67270:f18c774acde4 67271:48ef58c6cf4c
   103 fun repeat_sep s f = f ::: Scan.repeat (str s |-- f)
   103 fun repeat_sep s f = f ::: Scan.repeat (str s |-- f)
   104 
   104 
   105 val parse_id = Scan.one Symbol.is_letter ::: Scan.many Symbol.is_letdig >> implode
   105 val parse_id = Scan.one Symbol.is_letter ::: Scan.many Symbol.is_letdig >> implode
   106 
   106 
   107 fun parse_varpow ctxt = parse_id -- Scan.optional (str "^" |-- nat) 1 >>
   107 fun parse_varpow ctxt = parse_id -- Scan.optional (str "^" |-- nat) 1 >>
   108   (fn (x, k) => (Thm.cterm_of ctxt (Free (x, @{typ real})), k))
   108   (fn (x, k) => (Thm.cterm_of ctxt (Free (x, \<^typ>\<open>real\<close>)), k))
   109 
   109 
   110 fun parse_monomial ctxt = repeat_sep "*" (parse_varpow ctxt) >>
   110 fun parse_monomial ctxt = repeat_sep "*" (parse_varpow ctxt) >>
   111   (fn xs => fold FuncUtil.Ctermfunc.update xs FuncUtil.Ctermfunc.empty)
   111   (fn xs => fold FuncUtil.Ctermfunc.update xs FuncUtil.Ctermfunc.empty)
   112 
   112 
   113 fun parse_cmonomial ctxt =
   113 fun parse_cmonomial ctxt =