author  wenzelm 
Fri, 06 Mar 2015 15:58:56 +0100  
changeset 59621  291934bac95e 
parent 59582  0fbed69ff081 
child 63201  f151704c08e4 
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 

58629  10 
val print_cert: RealArith.pss_tree > string 
11 
val read_cert: Proof.context > string > RealArith.pss_tree 

32645  12 
end 
13 

58629  14 
structure Positivstellensatz_Tools : POSITIVSTELLENSATZ_TOOLS = 
32645  15 
struct 
16 

58629  17 
(** print certificate **) 
18 

19 
local 

32645  20 

21 
fun string_of_rat r = 

22 
let 

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

24 
in 

25 
if den = 1 then string_of_int nom 

26 
else string_of_int nom ^ "/" ^ string_of_int den 

27 
end 

28 

58629  29 

32645  30 
(* map polynomials to strings *) 
31 

32 
fun string_of_varpow x k = 

33 
let 

59582  34 
val term = Thm.term_of x 
55508  35 
val name = 
36 
(case term of 

37 
Free (n, _) => n 

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

32645  39 
in 
55508  40 
if k = 1 then name else name ^ "^" ^ string_of_int k 
32645  41 
end 
42 

55508  43 
fun string_of_monomial m = 
44 
if FuncUtil.Ctermfunc.is_empty m then "1" 

45 
else 

46 
let 

47 
val m' = FuncUtil.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 end 

32645  50 

51 
fun string_of_cmonomial (m,c) = 

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

52 
if FuncUtil.Ctermfunc.is_empty m then string_of_rat c 
32645  53 
else if c = Rat.one then string_of_monomial m 
58629  54 
else string_of_rat c ^ "*" ^ string_of_monomial m 
32645  55 

55508  56 
fun string_of_poly p = 
57 
if FuncUtil.Monomialfunc.is_empty p then "0" 

58 
else 

59 
let 

60 
val cms = map string_of_cmonomial 

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

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

64 

65 
(* print cert *) 

32645  66 

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

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

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

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

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

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

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

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

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

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

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

32645  80 

58629  81 
in 
82 

83 
fun print_cert RealArith.Trivial = "()" 

84 
 print_cert (RealArith.Cert pss) = "(" ^ pss_to_cert pss ^ ")" 

85 
 print_cert (RealArith.Branch (t1, t2)) = 

86 
"(" ^ print_cert t1 ^ " & " ^ print_cert t2 ^ ")" 

87 

88 
end 

55508  89 

32645  90 

58629  91 

92 
(** read certificate **) 

32645  93 

58629  94 
local 
95 

96 
(* basic parsers *) 

32645  97 

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

98 
val str = Scan.this_string 
32645  99 

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

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

32645  103 

104 
val nat = number 

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

106 
val rat = int  str "/"  int >> Rat.rat_of_quotient 
32645  107 
val rat_int = rat  int >> Rat.rat_of_int 
108 

55508  109 

58629  110 
(* polynomial parsers *) 
32645  111 

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

112 
fun repeat_sep s f = f ::: Scan.repeat (str s  f) 
32645  113 

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

115 

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

116 
fun parse_varpow ctxt = parse_id  Scan.optional (str "^"  nat) 1 >> 
59621
291934bac95e
Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents:
59582
diff
changeset

117 
(fn (x, k) => (Thm.cterm_of ctxt (Free (x, @{typ real})), k)) 
32645  118 

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

33339  120 
(fn xs => fold FuncUtil.Ctermfunc.update xs FuncUtil.Ctermfunc.empty) 
32645  121 

122 
fun parse_cmonomial ctxt = 

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

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

125 
rat_int >> (fn r => (FuncUtil.Ctermfunc.empty, r)) 
32645  126 

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

33339  128 
(fn xs => fold FuncUtil.Monomialfunc.update xs FuncUtil.Monomialfunc.empty) 
32645  129 

55508  130 

58629  131 
(* positivstellensatz parsers *) 
32645  132 

133 
val parse_axiom = 

32828  134 
(str "A="  int >> RealArith.Axiom_eq)  
135 
(str "A<="  int >> RealArith.Axiom_le)  

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

32645  137 

138 
val parse_rational = 

32828  139 
(str "R="  rat_int >> RealArith.Rational_eq)  
140 
(str "R<="  rat_int >> RealArith.Rational_le)  

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

32645  142 

143 
fun parse_cert ctxt input = 

144 
let 

145 
val pc = parse_cert ctxt 

146 
val pp = parse_poly ctxt 

147 
in 

55508  148 
(parse_axiom  
149 
parse_rational  

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

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

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

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

32645  154 
end 
155 

156 
fun parse_cert_tree ctxt input = 

157 
let 

158 
val pc = parse_cert ctxt 

159 
val pt = parse_cert_tree ctxt 

160 
in 

55508  161 
(str "()" >> K RealArith.Trivial  
162 
str "("  pc  str ")" >> RealArith.Cert  

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

32645  164 
end 
165 

58629  166 
in 
55508  167 

58629  168 
fun read_cert ctxt input_str = 
43946  169 
Symbol.scanner "Bad certificate" (parse_cert_tree ctxt) 
170 
(filter_out Symbol.is_blank (Symbol.explode input_str)) 

32645  171 

172 
end 

173 

58629  174 
end 
175 