author  Philipp Meyer 
Tue, 22 Sep 2009 11:26:46 +0200  
changeset 32646  962b4354ed90 
parent 32645  1cc5b24f5a01 
child 32828  ad76967c703d 
permissions  rwrr 
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 

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

85 
val str = Scan.this_string 
32645  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 

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 

96 
(* polynomial parser *) 

97 

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

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

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

101 

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

102 
fun parse_varpow ctxt = parse_id  Scan.optional (str "^"  nat) 1 >> 
32645  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 = 

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

109 
rat_int  str "*"  (parse_monomial ctxt) >> swap  
32645  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 = 

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

119 
(str "A="  int >> Axiom_eq)  
962b4354ed90
used standard fold function and type aliases
Philipp Meyer
parents:
32645
diff
changeset

120 
(str "A<="  int >> Axiom_le)  
962b4354ed90
used standard fold function and type aliases
Philipp Meyer
parents:
32645
diff
changeset

121 
(str "A<"  int >> Axiom_lt) 
32645  122 

123 
val parse_rational = 

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

124 
(str "R="  rat_int >> Rational_eq)  
962b4354ed90
used standard fold function and type aliases
Philipp Meyer
parents:
32645
diff
changeset

125 
(str "R<="  rat_int >> Rational_le)  
962b4354ed90
used standard fold function and type aliases
Philipp Meyer
parents:
32645
diff
changeset

126 
(str "R<"  rat_int >> Rational_lt) 
32645  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  

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

135 
str "["  pp  str "]^2" >> Square  
962b4354ed90
used standard fold function and type aliases
Philipp Meyer
parents:
32645
diff
changeset

136 
str "(["  pp  str "]*"  pc  str ")" >> Eqmul  
962b4354ed90
used standard fold function and type aliases
Philipp Meyer
parents:
32645
diff
changeset

137 
str "("  pc  str "*"  pc  str ")" >> Product  
962b4354ed90
used standard fold function and type aliases
Philipp Meyer
parents:
32645
diff
changeset

138 
str "("  pc  str "+"  pc  str ")" >> Sum) input 
32645  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 

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

146 
(str "()" >> K Trivial  
962b4354ed90
used standard fold function and type aliases
Philipp Meyer
parents:
32645
diff
changeset

147 
str "("  pc  str ")" >> Cert  
962b4354ed90
used standard fold function and type aliases
Philipp Meyer
parents:
32645
diff
changeset

148 
str "("  pt  str "&"  pt  str ")" >> Branch) input 
32645  149 
end 
150 

151 
(* scanner *) 

152 

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

153 
fun cert_to_pss_tree ctxt input_str = Symbol.scanner "bad certificate" (parse_cert_tree ctxt) 
962b4354ed90
used standard fold function and type aliases
Philipp Meyer
parents:
32645
diff
changeset

154 
(filter_out Symbol.is_blank (Symbol.explode input_str)) 
32645  155 

156 
end 

157 

158 