32645

1 
(* Title: positivstellensatz_tools.ML


2 
Author: Philipp Meyer, TU Muenchen


3 


4 
Functions for generating a certificate from a positivstellensatz and vice versa


5 
*)


6 


7 
signature POSITIVSTELLENSATZ_TOOLS =


8 
sig


9 
val pss_tree_to_cert : RealArith.pss_tree > string


10 


11 
val cert_to_pss_tree : Proof.context > string > RealArith.pss_tree


12 


13 
end


14 


15 


16 
structure PositivstellensatzTools : POSITIVSTELLENSATZ_TOOLS =


17 
struct


18 


19 
open RealArith FuncUtil


20 


21 
(*** certificate generation ***)


22 


23 
fun string_of_rat r =


24 
let


25 
val (nom, den) = Rat.quotient_of_rat r


26 
in


27 
if den = 1 then string_of_int nom


28 
else string_of_int nom ^ "/" ^ string_of_int den


29 
end


30 


31 
(* map polynomials to strings *)


32 


33 
fun string_of_varpow x k =


34 
let


35 
val term = term_of x


36 
val name = case term of


37 
Free (n, _) => n


38 
 _ => error "Term in monomial not free variable"


39 
in


40 
if k = 1 then name else name ^ "^" ^ string_of_int k


41 
end


42 


43 
fun string_of_monomial m =


44 
if Ctermfunc.is_undefined m then "1"


45 
else


46 
let


47 
val m' = dest_monomial 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


50 
end


51 


52 
fun string_of_cmonomial (m,c) =


53 
if Ctermfunc.is_undefined m then string_of_rat c


54 
else if c = Rat.one then string_of_monomial m


55 
else (string_of_rat c) ^ "*" ^ (string_of_monomial m);


56 


57 
fun string_of_poly p =


58 
if Monomialfunc.is_undefined p then "0"


59 
else


60 
let


61 
val cms = map string_of_cmonomial


62 
(sort (prod_ord monomial_order (K EQUAL)) (Monomialfunc.graph p))


63 
in foldr1 (fn (t1, t2) => t1 ^ " + " ^ t2) cms


64 
end;


65 


66 
fun pss_to_cert (Axiom_eq i) = "A=" ^ string_of_int i


67 
 pss_to_cert (Axiom_le i) = "A<=" ^ string_of_int i


68 
 pss_to_cert (Axiom_lt i) = "A<" ^ string_of_int i


69 
 pss_to_cert (Rational_eq r) = "R=" ^ string_of_rat r


70 
 pss_to_cert (Rational_le r) = "R<=" ^ string_of_rat r


71 
 pss_to_cert (Rational_lt r) = "R<" ^ string_of_rat r


72 
 pss_to_cert (Square p) = "[" ^ string_of_poly p ^ "]^2"


73 
 pss_to_cert (Eqmul (p, pss)) = "([" ^ string_of_poly p ^ "] * " ^ pss_to_cert pss ^ ")"


74 
 pss_to_cert (Sum (pss1, pss2)) = "(" ^ pss_to_cert pss1 ^ " + " ^ pss_to_cert pss2 ^ ")"


75 
 pss_to_cert (Product (pss1, pss2)) = "(" ^ pss_to_cert pss1 ^ " * " ^ pss_to_cert pss2 ^ ")"


76 


77 
fun pss_tree_to_cert Trivial = "()"


78 
 pss_tree_to_cert (Cert pss) = "(" ^ pss_to_cert pss ^ ")"


79 
 pss_tree_to_cert (Branch (t1, t2)) = "(" ^ pss_tree_to_cert t1 ^ " & " ^ pss_tree_to_cert t2 ^ ")"


80 


81 
(*** certificate parsing ***)


82 


83 
(* basic parser *)


84 


85 
fun $$ k = Scan.this_string k


86 


87 
val number = Scan.repeat1 (Scan.one Symbol.is_ascii_digit >>


88 
(fn s => ord s  ord "0")) >>


89 
foldl1 (fn (n, d) => n * 10 + d)


90 


91 
val nat = number


92 
val int = Scan.optional ($$ "~" >> K ~1) 1  nat >> op *;


93 
val rat = int  $$ "/"  int >> Rat.rat_of_quotient


94 
val rat_int = rat  int >> Rat.rat_of_int


95 


96 
(* polynomial parser *)


97 


98 
fun repeat_sep s f = f ::: Scan.repeat ($$ s  f)


99 


100 
val parse_id = Scan.one Symbol.is_letter ::: Scan.many Symbol.is_letdig >> implode


101 


102 
fun parse_varpow ctxt = parse_id  Scan.optional ($$ "^"  nat) 1 >>


103 
(fn (x, k) => (cterm_of (Context.theory_of_proof ctxt) (Free (x, @{typ real})), k))


104 


105 
fun parse_monomial ctxt = repeat_sep "*" (parse_varpow ctxt) >>


106 
foldl (uncurry Ctermfunc.update) Ctermfunc.undefined


107 


108 
fun parse_cmonomial ctxt =


109 
rat_int  $$ "*"  (parse_monomial ctxt) >> swap 


110 
(parse_monomial ctxt) >> (fn m => (m, Rat.one)) 


111 
rat_int >> (fn r => (Ctermfunc.undefined, r))


112 


113 
fun parse_poly ctxt = repeat_sep "+" (parse_cmonomial ctxt) >>


114 
foldl (uncurry Monomialfunc.update) Monomialfunc.undefined


115 


116 
(* positivstellensatz parser *)


117 


118 
val parse_axiom =


119 
($$ "A="  int >> Axiom_eq) 


120 
($$ "A<="  int >> Axiom_le) 


121 
($$ "A<"  int >> Axiom_lt)


122 


123 
val parse_rational =


124 
($$ "R="  rat_int >> Rational_eq) 


125 
($$ "R<="  rat_int >> Rational_le) 


126 
($$ "R<"  rat_int >> Rational_lt)


127 


128 
fun parse_cert ctxt input =


129 
let


130 
val pc = parse_cert ctxt


131 
val pp = parse_poly ctxt


132 
in


133 
(parse_axiom 


134 
parse_rational 


135 
$$ "["  pp  $$ "]^2" >> Square 


136 
$$ "(["  pp  $$ "]*"  pc  $$ ")" >> Eqmul 


137 
$$ "("  pc  $$ "*"  pc  $$ ")" >> Product 


138 
$$ "("  pc  $$ "+"  pc  $$ ")" >> Sum) input


139 
end


140 


141 
fun parse_cert_tree ctxt input =


142 
let


143 
val pc = parse_cert ctxt


144 
val pt = parse_cert_tree ctxt


145 
in


146 
($$ "()" >> K Trivial 


147 
$$ "("  pc  $$ ")" >> Cert 


148 
$$ "("  pt  $$ "&"  pt  $$ ")" >> Branch) input


149 
end


150 


151 
(* scanner *)


152 


153 
fun cert_to_pss_tree ctxt str = Symbol.scanner "bad certificate" (parse_cert_tree ctxt)


154 
(filter_out Symbol.is_blank (Symbol.explode str))


155 


156 
end


157 


158 
