author  wenzelm 
Sat, 08 Jan 2011 17:39:51 +0100  
changeset 41474  60d091240485 
parent 37744  src/HOL/Library/Sum_Of_Squares/positivstellensatz_tools.ML@3daaf23b9ab4 
child 42361  23f352990944 
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 

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

13 
end 

14 

15 

16 
structure PositivstellensatzTools : POSITIVSTELLENSATZ_TOOLS = 

17 
struct 

18 

19 
(*** certificate generation ***) 

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 

29 
(* map polynomials to strings *) 

30 

31 
fun string_of_varpow x k = 

32 
let 

33 
val term = term_of x 

34 
val name = case term of 

35 
Free (n, _) => n 

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

37 
in 

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

39 
end 

40 

41 
fun string_of_monomial m = 

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

42 
if FuncUtil.Ctermfunc.is_empty m then "1" 
32645  43 
else 
44 
let 

32828  45 
val m' = FuncUtil.dest_monomial m 
32645  46 
val vps = fold_rev (fn (x,k) => cons (string_of_varpow x k)) m' [] 
47 
in foldr1 (fn (s, t) => s ^ "*" ^ t) vps 

48 
end 

49 

50 
fun string_of_cmonomial (m,c) = 

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

51 
if FuncUtil.Ctermfunc.is_empty m then string_of_rat c 
32645  52 
else if c = Rat.one then string_of_monomial m 
53 
else (string_of_rat c) ^ "*" ^ (string_of_monomial m); 

54 

55 
fun string_of_poly p = 

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

56 
if FuncUtil.Monomialfunc.is_empty p then "0" 
32645  57 
else 
58 
let 

59 
val cms = map string_of_cmonomial 

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

60 
(sort (prod_ord FuncUtil.monomial_order (K EQUAL)) (FuncUtil.Monomialfunc.dest p)) 
32645  61 
in foldr1 (fn (t1, t2) => t1 ^ " + " ^ t2) cms 
62 
end; 

63 

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

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

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

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

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

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

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

72 
 pss_to_cert (RealArith.Sum (pss1, pss2)) = "(" ^ pss_to_cert pss1 ^ " + " ^ pss_to_cert pss2 ^ ")" 

73 
 pss_to_cert (RealArith.Product (pss1, pss2)) = "(" ^ 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 ^ ")" 

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

32645  78 

79 
(*** certificate parsing ***) 

80 

81 
(* basic parser *) 

82 

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

83 
val str = Scan.this_string 
32645  84 

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

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

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

88 

89 
val nat = number 

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

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

91 
val rat = int  str "/"  int >> Rat.rat_of_quotient 
32645  92 
val rat_int = rat  int >> Rat.rat_of_int 
93 

94 
(* polynomial parser *) 

95 

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

96 
fun repeat_sep s f = f ::: Scan.repeat (str s  f) 
32645  97 

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

99 

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

100 
fun parse_varpow ctxt = parse_id  Scan.optional (str "^"  nat) 1 >> 
33030  101 
(fn (x, k) => (cterm_of (ProofContext.theory_of ctxt) (Free (x, @{typ real})), k)) 
32645  102 

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

33339  104 
(fn xs => fold FuncUtil.Ctermfunc.update xs FuncUtil.Ctermfunc.empty) 
32645  105 

106 
fun parse_cmonomial ctxt = 

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

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

109 
rat_int >> (fn r => (FuncUtil.Ctermfunc.empty, r)) 
32645  110 

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

33339  112 
(fn xs => fold FuncUtil.Monomialfunc.update xs FuncUtil.Monomialfunc.empty) 
32645  113 

114 
(* positivstellensatz parser *) 

115 

116 
val parse_axiom = 

32828  117 
(str "A="  int >> RealArith.Axiom_eq)  
118 
(str "A<="  int >> RealArith.Axiom_le)  

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

32645  120 

121 
val parse_rational = 

32828  122 
(str "R="  rat_int >> RealArith.Rational_eq)  
123 
(str "R<="  rat_int >> RealArith.Rational_le)  

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

32645  125 

126 
fun parse_cert ctxt input = 

127 
let 

128 
val pc = parse_cert ctxt 

129 
val pp = parse_poly ctxt 

130 
in 

131 
(parse_axiom  

132 
parse_rational  

32828  133 
str "["  pp  str "]^2" >> RealArith.Square  
134 
str "(["  pp  str "]*"  pc  str ")" >> RealArith.Eqmul  

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

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

32645  137 
end 
138 

139 
fun parse_cert_tree ctxt input = 

140 
let 

141 
val pc = parse_cert ctxt 

142 
val pt = parse_cert_tree ctxt 

143 
in 

32828  144 
(str "()" >> K RealArith.Trivial  
145 
str "("  pc  str ")" >> RealArith.Cert  

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

32645  147 
end 
148 

149 
(* scanner *) 

150 

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

151 
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

152 
(filter_out Symbol.is_blank (Symbol.explode input_str)) 
32645  153 

154 
end 

155 

156 