author  wenzelm 
Sat, 15 Feb 2014 21:11:29 +0100  
changeset 55508  90c42b130652 
parent 43946  ba88bb44c192 
child 58629  a6a6cd499d4e 
permissions  rwrr 
41474  1 
(* Title: HOL/Library/Sum_of_Squares/positivstellensatz_tools.ML 
2 
Author: Philipp Meyer, TU Muenchen 

32645  3 

41474  4 
Functions for generating a certificate from a positivstellensatz and vice 
5 
versa. 

32645  6 
*) 
7 

8 
signature POSITIVSTELLENSATZ_TOOLS = 

9 
sig 

10 
val pss_tree_to_cert : RealArith.pss_tree > string 

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

12 
end 

13 

14 
structure PositivstellensatzTools : POSITIVSTELLENSATZ_TOOLS = 

15 
struct 

16 

17 
(*** certificate generation ***) 

18 

19 
fun string_of_rat r = 

20 
let 

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

22 
in 

23 
if den = 1 then string_of_int nom 

24 
else string_of_int nom ^ "/" ^ string_of_int den 

25 
end 

26 

27 
(* map polynomials to strings *) 

28 

29 
fun string_of_varpow x k = 

30 
let 

31 
val term = term_of x 

55508  32 
val name = 
33 
(case term of 

34 
Free (n, _) => n 

35 
 _ => error "Term in monomial not free variable") 

32645  36 
in 
55508  37 
if k = 1 then name else name ^ "^" ^ string_of_int k 
32645  38 
end 
39 

55508  40 
fun string_of_monomial m = 
41 
if FuncUtil.Ctermfunc.is_empty m then "1" 

42 
else 

43 
let 

44 
val m' = FuncUtil.dest_monomial m 

45 
val vps = fold_rev (fn (x,k) => cons (string_of_varpow x k)) m' [] 

46 
in foldr1 (fn (s, t) => s ^ "*" ^ t) vps end 

32645  47 

48 
fun string_of_cmonomial (m,c) = 

32829
671eb46eb0a3
tuned FuncFun and FuncUtil structure in positivstellensatz.ML
Philipp Meyer
parents:
32828
diff
changeset

49 
if FuncUtil.Ctermfunc.is_empty m then string_of_rat c 
32645  50 
else if c = Rat.one then string_of_monomial m 
55508  51 
else string_of_rat c ^ "*" ^ string_of_monomial m; 
32645  52 

55508  53 
fun string_of_poly p = 
54 
if FuncUtil.Monomialfunc.is_empty p then "0" 

55 
else 

56 
let 

57 
val cms = map string_of_cmonomial 

58 
(sort (prod_ord FuncUtil.monomial_order (K EQUAL)) (FuncUtil.Monomialfunc.dest p)) 

59 
in foldr1 (fn (t1, t2) => t1 ^ " + " ^ t2) cms end; 

32645  60 

32828  61 
fun pss_to_cert (RealArith.Axiom_eq i) = "A=" ^ string_of_int i 
62 
 pss_to_cert (RealArith.Axiom_le i) = "A<=" ^ string_of_int i 

63 
 pss_to_cert (RealArith.Axiom_lt i) = "A<" ^ string_of_int i 

64 
 pss_to_cert (RealArith.Rational_eq r) = "R=" ^ string_of_rat r 

65 
 pss_to_cert (RealArith.Rational_le r) = "R<=" ^ string_of_rat r 

66 
 pss_to_cert (RealArith.Rational_lt r) = "R<" ^ string_of_rat r 

67 
 pss_to_cert (RealArith.Square p) = "[" ^ string_of_poly p ^ "]^2" 

55508  68 
 pss_to_cert (RealArith.Eqmul (p, pss)) = 
69 
"([" ^ string_of_poly p ^ "] * " ^ pss_to_cert pss ^ ")" 

70 
 pss_to_cert (RealArith.Sum (pss1, pss2)) = 

71 
"(" ^ pss_to_cert pss1 ^ " + " ^ pss_to_cert pss2 ^ ")" 

72 
 pss_to_cert (RealArith.Product (pss1, pss2)) = 

73 
"(" ^ pss_to_cert pss1 ^ " * " ^ pss_to_cert pss2 ^ ")" 

32645  74 

32828  75 
fun pss_tree_to_cert RealArith.Trivial = "()" 
76 
 pss_tree_to_cert (RealArith.Cert pss) = "(" ^ pss_to_cert pss ^ ")" 

55508  77 
 pss_tree_to_cert (RealArith.Branch (t1, t2)) = 
78 
"(" ^ pss_tree_to_cert t1 ^ " & " ^ pss_tree_to_cert t2 ^ ")" 

79 

32645  80 

81 
(*** certificate parsing ***) 

82 

83 
(* basic parser *) 

84 

32646
962b4354ed90
used standard fold function and type aliases
Philipp Meyer
parents:
32645
diff
changeset

85 
val str = Scan.this_string 
32645  86 

55508  87 
val number = 
88 
Scan.repeat1 (Scan.one Symbol.is_ascii_digit >> (fn s => ord s  ord "0")) 

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

32645  90 

91 
val nat = number 

32646
962b4354ed90
used standard fold function and type aliases
Philipp Meyer
parents:
32645
diff
changeset

92 
val int = Scan.optional (str "~" >> K ~1) 1  nat >> op *; 
962b4354ed90
used standard fold function and type aliases
Philipp Meyer
parents:
32645
diff
changeset

93 
val rat = int  str "/"  int >> Rat.rat_of_quotient 
32645  94 
val rat_int = rat  int >> Rat.rat_of_int 
95 

55508  96 

32645  97 
(* polynomial parser *) 
98 

32646
962b4354ed90
used standard fold function and type aliases
Philipp Meyer
parents:
32645
diff
changeset

99 
fun repeat_sep s f = f ::: Scan.repeat (str s  f) 
32645  100 

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

102 

32646
962b4354ed90
used standard fold function and type aliases
Philipp Meyer
parents:
32645
diff
changeset

103 
fun parse_varpow ctxt = parse_id  Scan.optional (str "^"  nat) 1 >> 
55508  104 
(fn (x, k) => (cterm_of (Proof_Context.theory_of ctxt) (Free (x, @{typ real})), k)) 
32645  105 

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

33339  107 
(fn xs => fold FuncUtil.Ctermfunc.update xs FuncUtil.Ctermfunc.empty) 
32645  108 

109 
fun parse_cmonomial ctxt = 

32646
962b4354ed90
used standard fold function and type aliases
Philipp Meyer
parents:
32645
diff
changeset

110 
rat_int  str "*"  (parse_monomial ctxt) >> swap  
32645  111 
(parse_monomial ctxt) >> (fn m => (m, Rat.one))  
32829
671eb46eb0a3
tuned FuncFun and FuncUtil structure in positivstellensatz.ML
Philipp Meyer
parents:
32828
diff
changeset

112 
rat_int >> (fn r => (FuncUtil.Ctermfunc.empty, r)) 
32645  113 

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

33339  115 
(fn xs => fold FuncUtil.Monomialfunc.update xs FuncUtil.Monomialfunc.empty) 
32645  116 

55508  117 

32645  118 
(* positivstellensatz parser *) 
119 

120 
val parse_axiom = 

32828  121 
(str "A="  int >> RealArith.Axiom_eq)  
122 
(str "A<="  int >> RealArith.Axiom_le)  

123 
(str "A<"  int >> RealArith.Axiom_lt) 

32645  124 

125 
val parse_rational = 

32828  126 
(str "R="  rat_int >> RealArith.Rational_eq)  
127 
(str "R<="  rat_int >> RealArith.Rational_le)  

128 
(str "R<"  rat_int >> RealArith.Rational_lt) 

32645  129 

130 
fun parse_cert ctxt input = 

131 
let 

132 
val pc = parse_cert ctxt 

133 
val pp = parse_poly ctxt 

134 
in 

55508  135 
(parse_axiom  
136 
parse_rational  

137 
str "["  pp  str "]^2" >> RealArith.Square  

138 
str "(["  pp  str "]*"  pc  str ")" >> RealArith.Eqmul  

139 
str "("  pc  str "*"  pc  str ")" >> RealArith.Product  

140 
str "("  pc  str "+"  pc  str ")" >> RealArith.Sum) input 

32645  141 
end 
142 

143 
fun parse_cert_tree ctxt input = 

144 
let 

145 
val pc = parse_cert ctxt 

146 
val pt = parse_cert_tree ctxt 

147 
in 

55508  148 
(str "()" >> K RealArith.Trivial  
149 
str "("  pc  str ")" >> RealArith.Cert  

150 
str "("  pt  str "&"  pt  str ")" >> RealArith.Branch) input 

32645  151 
end 
152 

55508  153 

32645  154 
(* scanner *) 
155 

43946  156 
fun cert_to_pss_tree ctxt input_str = 
157 
Symbol.scanner "Bad certificate" (parse_cert_tree ctxt) 

158 
(filter_out Symbol.is_blank (Symbol.explode input_str)) 

32645  159 

160 
end 

161 