author | wenzelm |
Thu, 18 Apr 2013 17:07:01 +0200 | |
changeset 51717 | 9e7d1c139569 |
parent 47108 | 2a1953f0d20d |
child 53972 | c6297fa1031a |
permissions | -rw-r--r-- |
41474 | 1 |
(* Title: HOL/Library/Sum_of_Squares/sum_of_squares.ML |
32949
aa6c470a962a
eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents:
32839
diff
changeset
|
2 |
Author: Amine Chaieb, University of Cambridge |
aa6c470a962a
eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents:
32839
diff
changeset
|
3 |
Author: Philipp Meyer, TU Muenchen |
32268
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
32150
diff
changeset
|
4 |
|
32839 | 5 |
A tactic for proving nonlinear inequalities. |
32268
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
32150
diff
changeset
|
6 |
*) |
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
32150
diff
changeset
|
7 |
|
32949
aa6c470a962a
eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents:
32839
diff
changeset
|
8 |
signature SUM_OF_SQUARES = |
32268
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
32150
diff
changeset
|
9 |
sig |
32949
aa6c470a962a
eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents:
32839
diff
changeset
|
10 |
datatype proof_method = Certificate of RealArith.pss_tree | Prover of string -> string |
aa6c470a962a
eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents:
32839
diff
changeset
|
11 |
val sos_tac: (RealArith.pss_tree -> unit) -> proof_method -> Proof.context -> int -> tactic |
38805 | 12 |
val trace: bool Config.T |
32332 | 13 |
exception Failure of string; |
32268
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
32150
diff
changeset
|
14 |
end |
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
32150
diff
changeset
|
15 |
|
41474 | 16 |
structure Sum_of_Squares: SUM_OF_SQUARES = |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
17 |
struct |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
18 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
19 |
val rat_0 = Rat.zero; |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
20 |
val rat_1 = Rat.one; |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
21 |
val rat_2 = Rat.two; |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
22 |
val rat_10 = Rat.rat_of_int 10; |
33029 | 23 |
val max = Integer.max; |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
24 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
25 |
val denominator_rat = Rat.quotient_of_rat #> snd #> Rat.rat_of_int; |
32839 | 26 |
fun int_of_rat a = |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
27 |
case Rat.quotient_of_rat a of (i,1) => i | _ => error "int_of_rat: not an int"; |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
28 |
fun lcm_rat x y = Rat.rat_of_int (Integer.lcm (int_of_rat x) (int_of_rat y)); |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
29 |
|
32839 | 30 |
fun rat_pow r i = |
31 |
let fun pow r i = |
|
32 |
if i = 0 then rat_1 else |
|
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
33 |
let val d = pow r (i div 2) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
34 |
in d */ d */ (if i mod 2 = 0 then rat_1 else r) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
35 |
end |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
36 |
in if i < 0 then pow (Rat.inv r) (~ i) else pow r i end; |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
37 |
|
32839 | 38 |
fun round_rat r = |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
39 |
let val (a,b) = Rat.quotient_of_rat (Rat.abs r) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
40 |
val d = a div b |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
41 |
val s = if r </ rat_0 then (Rat.neg o Rat.rat_of_int) else Rat.rat_of_int |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
42 |
val x2 = 2 * (a - (b * d)) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
43 |
in s (if x2 >= b then d + 1 else d) end |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
44 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
45 |
val abs_rat = Rat.abs; |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
46 |
val pow2 = rat_pow rat_2; |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
47 |
val pow10 = rat_pow rat_10; |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
48 |
|
42616
92715b528e78
added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents:
41490
diff
changeset
|
49 |
val trace = Attrib.setup_config_bool @{binding sos_trace} (K false); |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
50 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
51 |
exception Sanity; |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
52 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
53 |
exception Unsolvable; |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
54 |
|
32332 | 55 |
exception Failure of string; |
56 |
||
32645
1cc5b24f5a01
sos method generates and uses proof certificates
Philipp Meyer
parents:
32332
diff
changeset
|
57 |
datatype proof_method = |
1cc5b24f5a01
sos method generates and uses proof certificates
Philipp Meyer
parents:
32332
diff
changeset
|
58 |
Certificate of RealArith.pss_tree |
1cc5b24f5a01
sos method generates and uses proof certificates
Philipp Meyer
parents:
32332
diff
changeset
|
59 |
| Prover of (string -> string) |
1cc5b24f5a01
sos method generates and uses proof certificates
Philipp Meyer
parents:
32332
diff
changeset
|
60 |
|
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
61 |
(* Turn a rational into a decimal string with d sig digits. *) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
62 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
63 |
local |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
64 |
fun normalize y = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
65 |
if abs_rat y </ (rat_1 // rat_10) then normalize (rat_10 */ y) - 1 |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
66 |
else if abs_rat y >=/ rat_1 then normalize (y // rat_10) + 1 |
32839 | 67 |
else 0 |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
68 |
in |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
69 |
fun decimalize d x = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
70 |
if x =/ rat_0 then "0.0" else |
32839 | 71 |
let |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
72 |
val y = Rat.abs x |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
73 |
val e = normalize y |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
74 |
val z = pow10(~ e) */ y +/ rat_1 |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
75 |
val k = int_of_rat (round_rat(pow10 d */ z)) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
76 |
in (if x </ rat_0 then "-0." else "0.") ^ |
40627
becf5d5187cc
renamed raw "explode" function to "raw_explode" to emphasize its meaning;
wenzelm
parents:
39027
diff
changeset
|
77 |
implode(tl(raw_explode(string_of_int k))) ^ |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
78 |
(if e = 0 then "" else "e"^string_of_int e) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
79 |
end |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
80 |
end; |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
81 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
82 |
(* Iterations over numbers, and lists indexed by numbers. *) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
83 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
84 |
fun itern k l f a = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
85 |
case l of |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
86 |
[] => a |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
87 |
| h::t => itern (k + 1) t f (f h k a); |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
88 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
89 |
fun iter (m,n) f a = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
90 |
if n < m then a |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
91 |
else iter (m+1,n) f (f m a); |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
92 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
93 |
(* The main types. *) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
94 |
|
32829
671eb46eb0a3
tuned FuncFun and FuncUtil structure in positivstellensatz.ML
Philipp Meyer
parents:
32828
diff
changeset
|
95 |
type vector = int* Rat.rat FuncUtil.Intfunc.table; |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
96 |
|
32829
671eb46eb0a3
tuned FuncFun and FuncUtil structure in positivstellensatz.ML
Philipp Meyer
parents:
32828
diff
changeset
|
97 |
type matrix = (int*int)*(Rat.rat FuncUtil.Intpairfunc.table); |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
98 |
|
44453 | 99 |
fun iszero (_,r) = r =/ rat_0; |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
100 |
|
32839 | 101 |
|
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
102 |
(* Vectors. Conventionally indexed 1..n. *) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
103 |
|
32829
671eb46eb0a3
tuned FuncFun and FuncUtil structure in positivstellensatz.ML
Philipp Meyer
parents:
32828
diff
changeset
|
104 |
fun vector_0 n = (n,FuncUtil.Intfunc.empty):vector; |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
105 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
106 |
fun dim (v:vector) = fst v; |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
107 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
108 |
fun vector_cmul c (v:vector) = |
32839 | 109 |
let val n = dim v |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
110 |
in if c =/ rat_0 then vector_0 n |
39027 | 111 |
else (n,FuncUtil.Intfunc.map (fn _ => fn x => c */ x) (snd v)) |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
112 |
end; |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
113 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
114 |
fun vector_of_list l = |
32839 | 115 |
let val n = length l |
32829
671eb46eb0a3
tuned FuncFun and FuncUtil structure in positivstellensatz.ML
Philipp Meyer
parents:
32828
diff
changeset
|
116 |
in (n,fold_rev2 (curry FuncUtil.Intfunc.update) (1 upto n) l FuncUtil.Intfunc.empty) :vector |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
117 |
end; |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
118 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
119 |
(* Matrices; again rows and columns indexed from 1. *) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
120 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
121 |
fun dimensions (m:matrix) = fst m; |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
122 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
123 |
fun row k (m:matrix) = |
44453 | 124 |
let val (_,j) = dimensions m |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
125 |
in (j, |
32829
671eb46eb0a3
tuned FuncFun and FuncUtil structure in positivstellensatz.ML
Philipp Meyer
parents:
32828
diff
changeset
|
126 |
FuncUtil.Intpairfunc.fold (fn ((i,j), c) => fn a => if i = k then FuncUtil.Intfunc.update (j,c) a else a) (snd m) FuncUtil.Intfunc.empty ) : vector |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
127 |
end; |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
128 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
129 |
(* Monomials. *) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
130 |
|
32828 | 131 |
fun monomial_eval assig m = |
132 |
FuncUtil.Ctermfunc.fold (fn (x, k) => fn a => a */ rat_pow (FuncUtil.Ctermfunc.apply assig x) k) |
|
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
133 |
m rat_1; |
32829
671eb46eb0a3
tuned FuncFun and FuncUtil structure in positivstellensatz.ML
Philipp Meyer
parents:
32828
diff
changeset
|
134 |
val monomial_1 = FuncUtil.Ctermfunc.empty; |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
135 |
|
32828 | 136 |
fun monomial_var x = FuncUtil.Ctermfunc.onefunc (x, 1); |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
137 |
|
32828 | 138 |
val monomial_mul = |
33002 | 139 |
FuncUtil.Ctermfunc.combine Integer.add (K false); |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
140 |
|
32839 | 141 |
fun monomial_multidegree m = |
44453 | 142 |
FuncUtil.Ctermfunc.fold (fn (_, k) => fn a => k + a) m 0;; |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
143 |
|
32828 | 144 |
fun monomial_variables m = FuncUtil.Ctermfunc.dom m;; |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
145 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
146 |
(* Polynomials. *) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
147 |
|
32828 | 148 |
fun eval assig p = |
149 |
FuncUtil.Monomialfunc.fold (fn (m, c) => fn a => a +/ c */ monomial_eval assig m) p rat_0; |
|
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
150 |
|
32829
671eb46eb0a3
tuned FuncFun and FuncUtil structure in positivstellensatz.ML
Philipp Meyer
parents:
32828
diff
changeset
|
151 |
val poly_0 = FuncUtil.Monomialfunc.empty; |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
152 |
|
32839 | 153 |
fun poly_isconst p = |
44453 | 154 |
FuncUtil.Monomialfunc.fold (fn (m, _) => fn a => FuncUtil.Ctermfunc.is_empty m andalso a) p true; |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
155 |
|
32828 | 156 |
fun poly_var x = FuncUtil.Monomialfunc.onefunc (monomial_var x,rat_1); |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
157 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
158 |
fun poly_const c = |
32828 | 159 |
if c =/ rat_0 then poly_0 else FuncUtil.Monomialfunc.onefunc(monomial_1, c); |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
160 |
|
32828 | 161 |
fun poly_cmul c p = |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
162 |
if c =/ rat_0 then poly_0 |
39027 | 163 |
else FuncUtil.Monomialfunc.map (fn _ => fn x => c */ x) p; |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
164 |
|
39027 | 165 |
fun poly_neg p = FuncUtil.Monomialfunc.map (K Rat.neg) p;; |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
166 |
|
32828 | 167 |
fun poly_add p1 p2 = |
168 |
FuncUtil.Monomialfunc.combine (curry op +/) (fn x => x =/ rat_0) p1 p2; |
|
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
169 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
170 |
fun poly_sub p1 p2 = poly_add p1 (poly_neg p2); |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
171 |
|
32828 | 172 |
fun poly_cmmul (c,m) p = |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
173 |
if c =/ rat_0 then poly_0 |
32839 | 174 |
else if FuncUtil.Ctermfunc.is_empty m |
39027 | 175 |
then FuncUtil.Monomialfunc.map (fn _ => fn d => c */ d) p |
32828 | 176 |
else FuncUtil.Monomialfunc.fold (fn (m', d) => fn a => (FuncUtil.Monomialfunc.update (monomial_mul m m', c */ d) a)) p poly_0; |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
177 |
|
32828 | 178 |
fun poly_mul p1 p2 = |
179 |
FuncUtil.Monomialfunc.fold (fn (m, c) => fn a => poly_add (poly_cmmul (c,m) p2) a) p1 poly_0; |
|
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
180 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
181 |
fun poly_square p = poly_mul p p; |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
182 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
183 |
fun poly_pow p k = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
184 |
if k = 0 then poly_const rat_1 |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
185 |
else if k = 1 then p |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
186 |
else let val q = poly_square(poly_pow p (k div 2)) in |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
187 |
if k mod 2 = 1 then poly_mul p q else q end; |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
188 |
|
32828 | 189 |
fun multidegree p = |
44453 | 190 |
FuncUtil.Monomialfunc.fold (fn (m, _) => fn a => max (monomial_multidegree m) a) p 0; |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
191 |
|
32828 | 192 |
fun poly_variables p = |
44453 | 193 |
sort FuncUtil.cterm_ord (FuncUtil.Monomialfunc.fold_rev (fn (m, _) => union (is_equal o FuncUtil.cterm_ord) (monomial_variables m)) p []);; |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
194 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
195 |
(* Conversion from HOL term. *) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
196 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
197 |
local |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
198 |
val neg_tm = @{cterm "uminus :: real => _"} |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
199 |
val add_tm = @{cterm "op + :: real => _"} |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
200 |
val sub_tm = @{cterm "op - :: real => _"} |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
201 |
val mul_tm = @{cterm "op * :: real => _"} |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
202 |
val inv_tm = @{cterm "inverse :: real => _"} |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
203 |
val div_tm = @{cterm "op / :: real => _"} |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
204 |
val pow_tm = @{cterm "op ^ :: real => _"} |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
205 |
val zero_tm = @{cterm "0:: real"} |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
206 |
val is_numeral = can (HOLogic.dest_number o term_of) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
207 |
fun poly_of_term tm = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
208 |
if tm aconvc zero_tm then poly_0 |
32839 | 209 |
else if RealArith.is_ratconst tm |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
210 |
then poly_const(RealArith.dest_ratconst tm) |
32839 | 211 |
else |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
212 |
(let val (lop,r) = Thm.dest_comb tm |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
213 |
in if lop aconvc neg_tm then poly_neg(poly_of_term r) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
214 |
else if lop aconvc inv_tm then |
32839 | 215 |
let val p = poly_of_term r |
216 |
in if poly_isconst p |
|
32829
671eb46eb0a3
tuned FuncFun and FuncUtil structure in positivstellensatz.ML
Philipp Meyer
parents:
32828
diff
changeset
|
217 |
then poly_const(Rat.inv (eval FuncUtil.Ctermfunc.empty p)) |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
218 |
else error "poly_of_term: inverse of non-constant polyomial" |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
219 |
end |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
220 |
else (let val (opr,l) = Thm.dest_comb lop |
32839 | 221 |
in |
222 |
if opr aconvc pow_tm andalso is_numeral r |
|
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
223 |
then poly_pow (poly_of_term l) ((snd o HOLogic.dest_number o term_of) r) |
32839 | 224 |
else if opr aconvc add_tm |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
225 |
then poly_add (poly_of_term l) (poly_of_term r) |
32839 | 226 |
else if opr aconvc sub_tm |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
227 |
then poly_sub (poly_of_term l) (poly_of_term r) |
32839 | 228 |
else if opr aconvc mul_tm |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
229 |
then poly_mul (poly_of_term l) (poly_of_term r) |
32839 | 230 |
else if opr aconvc div_tm |
231 |
then let |
|
232 |
val p = poly_of_term l |
|
233 |
val q = poly_of_term r |
|
32829
671eb46eb0a3
tuned FuncFun and FuncUtil structure in positivstellensatz.ML
Philipp Meyer
parents:
32828
diff
changeset
|
234 |
in if poly_isconst q then poly_cmul (Rat.inv (eval FuncUtil.Ctermfunc.empty q)) p |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
235 |
else error "poly_of_term: division by non-constant polynomial" |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
236 |
end |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
237 |
else poly_var tm |
32839 | 238 |
|
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
239 |
end |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
240 |
handle CTERM ("dest_comb",_) => poly_var tm) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
241 |
end |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
242 |
handle CTERM ("dest_comb",_) => poly_var tm) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
243 |
in |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
244 |
val poly_of_term = fn tm => |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
245 |
if type_of (term_of tm) = @{typ real} then poly_of_term tm |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
246 |
else error "poly_of_term: term does not have real type" |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
247 |
end; |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
248 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
249 |
(* String of vector (just a list of space-separated numbers). *) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
250 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
251 |
fun sdpa_of_vector (v:vector) = |
32839 | 252 |
let |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
253 |
val n = dim v |
32839 | 254 |
val strs = map (decimalize 20 o (fn i => FuncUtil.Intfunc.tryapplyd (snd v) i rat_0)) (1 upto n) |
32830 | 255 |
in space_implode " " strs ^ "\n" |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
256 |
end; |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
257 |
|
32839 | 258 |
fun triple_int_ord ((a,b,c),(a',b',c')) = |
259 |
prod_ord int_ord (prod_ord int_ord int_ord) |
|
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
260 |
((a,(b,c)),(a',(b',c'))); |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
261 |
structure Inttriplefunc = FuncFun(type key = int*int*int val ord = triple_int_ord); |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
262 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
263 |
fun index_char str chr pos = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
264 |
if pos >= String.size str then ~1 |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
265 |
else if String.sub(str,pos) = chr then pos |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
266 |
else index_char str chr (pos + 1); |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
267 |
fun rat_of_quotient (a,b) = if b = 0 then rat_0 else Rat.rat_of_quotient (a,b); |
32839 | 268 |
fun rat_of_string s = |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
269 |
let val n = index_char s #"/" 0 in |
33035 | 270 |
if n = ~1 then s |> Int.fromString |> the |> Rat.rat_of_int |
32839 | 271 |
else |
32949
aa6c470a962a
eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents:
32839
diff
changeset
|
272 |
let val SOME numer = Int.fromString(String.substring(s,0,n)) |
aa6c470a962a
eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents:
32839
diff
changeset
|
273 |
val SOME den = Int.fromString (String.substring(s,n+1,String.size s - n - 1)) |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
274 |
in rat_of_quotient(numer, den) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
275 |
end |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
276 |
end; |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
277 |
|
36692
54b64d4ad524
farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
haftmann
parents:
36350
diff
changeset
|
278 |
fun isnum x = member (op =) ["0","1","2","3","4","5","6","7","8","9"] x; |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
279 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
280 |
(* More parser basics. *) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
281 |
|
32828 | 282 |
val numeral = Scan.one isnum |
33906 | 283 |
val decimalint = Scan.repeat1 numeral >> (rat_of_string o implode) |
284 |
val decimalfrac = Scan.repeat1 numeral |
|
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
285 |
>> (fn s => rat_of_string(implode s) // pow10 (length s)) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
286 |
val decimalsig = |
32828 | 287 |
decimalint -- Scan.option (Scan.$$ "." |-- decimalfrac) |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
288 |
>> (fn (h,NONE) => h | (h,SOME x) => h +/ x) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
289 |
fun signed prs = |
32839 | 290 |
$$ "-" |-- prs >> Rat.neg |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
291 |
|| $$ "+" |-- prs |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
292 |
|| prs; |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
293 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
294 |
fun emptyin def xs = if null xs then (def,xs) else Scan.fail xs |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
295 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
296 |
val exponent = ($$ "e" || $$ "E") |-- signed decimalint; |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
297 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
298 |
val decimal = signed decimalsig -- (emptyin rat_0|| exponent) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
299 |
>> (fn (h, x) => h */ pow10 (int_of_rat x)); |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
300 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
301 |
fun mkparser p s = |
40627
becf5d5187cc
renamed raw "explode" function to "raw_explode" to emphasize its meaning;
wenzelm
parents:
39027
diff
changeset
|
302 |
let val (x,rst) = p (raw_explode s) |
32839 | 303 |
in if null rst then x |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
304 |
else error "mkparser: unparsed input" |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
305 |
end;; |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
306 |
|
32332 | 307 |
(* Parse back csdp output. *) |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
308 |
|
44453 | 309 |
fun ignore _ = ((),[]) |
33067
a70d5baa53ee
use plain Scan.repeat (NB: Scan.bulk is for cascading sources -- mostly interna use);
wenzelm
parents:
33042
diff
changeset
|
310 |
fun csdpoutput inp = |
a70d5baa53ee
use plain Scan.repeat (NB: Scan.bulk is for cascading sources -- mostly interna use);
wenzelm
parents:
33042
diff
changeset
|
311 |
((decimal -- Scan.repeat (Scan.$$ " " |-- Scan.option decimal) >> |
a70d5baa53ee
use plain Scan.repeat (NB: Scan.bulk is for cascading sources -- mostly interna use);
wenzelm
parents:
33042
diff
changeset
|
312 |
(fn (h,to) => map_filter I ((SOME h)::to))) --| ignore >> vector_of_list) inp |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
313 |
val parse_csdpoutput = mkparser csdpoutput |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
314 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
315 |
(* Try some apparently sensible scaling first. Note that this is purely to *) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
316 |
(* get a cleaner translation to floating-point, and doesn't affect any of *) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
317 |
(* the results, in principle. In practice it seems a lot better when there *) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
318 |
(* are extreme numbers in the original problem. *) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
319 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
320 |
(* Version for (int*int*int) keys *) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
321 |
local |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
322 |
fun max_rat x y = if x </ y then y else x |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
323 |
fun common_denominator fld amat acc = |
44453 | 324 |
fld (fn (_,c) => fn a => lcm_rat (denominator_rat c) a) amat acc |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
325 |
fun maximal_element fld amat acc = |
44453 | 326 |
fld (fn (_,c) => fn maxa => max_rat maxa (abs_rat c)) amat acc |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
327 |
fun float_of_rat x = let val (a,b) = Rat.quotient_of_rat x |
41490
0f1e411a1448
eliminated obsolete LargeInt -- Int is unbounded;
wenzelm
parents:
41474
diff
changeset
|
328 |
in Real.fromInt a / Real.fromInt b end; |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
329 |
fun int_of_float x = (trunc x handle Overflow => 0 | Domain => 0) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
330 |
in |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
331 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
332 |
fun tri_scale_then solver (obj:vector) mats = |
32839 | 333 |
let |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
334 |
val cd1 = fold_rev (common_denominator Inttriplefunc.fold) mats (rat_1) |
32839 | 335 |
val cd2 = common_denominator FuncUtil.Intfunc.fold (snd obj) (rat_1) |
39027 | 336 |
val mats' = map (Inttriplefunc.map (fn _ => fn x => cd1 */ x)) mats |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
337 |
val obj' = vector_cmul cd2 obj |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
338 |
val max1 = fold_rev (maximal_element Inttriplefunc.fold) mats' (rat_0) |
32839 | 339 |
val max2 = maximal_element FuncUtil.Intfunc.fold (snd obj') (rat_0) |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
340 |
val scal1 = pow2 (20 - int_of_float(Math.ln (float_of_rat max1) / Math.ln 2.0)) |
32839 | 341 |
val scal2 = pow2 (20 - int_of_float(Math.ln (float_of_rat max2) / Math.ln 2.0)) |
39027 | 342 |
val mats'' = map (Inttriplefunc.map (fn _ => fn x => x */ scal1)) mats' |
32839 | 343 |
val obj'' = vector_cmul scal2 obj' |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
344 |
in solver obj'' mats'' |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
345 |
end |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
346 |
end; |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
347 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
348 |
(* Round a vector to "nice" rationals. *) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
349 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
350 |
fun nice_rational n x = round_rat (n */ x) // n;; |
32839 | 351 |
fun nice_vector n ((d,v) : vector) = |
352 |
(d, FuncUtil.Intfunc.fold (fn (i,c) => fn a => |
|
353 |
let val y = nice_rational n c |
|
354 |
in if c =/ rat_0 then a |
|
32829
671eb46eb0a3
tuned FuncFun and FuncUtil structure in positivstellensatz.ML
Philipp Meyer
parents:
32828
diff
changeset
|
355 |
else FuncUtil.Intfunc.update (i,y) a end) v FuncUtil.Intfunc.empty):vector |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
356 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
357 |
fun dest_ord f x = is_equal (f x); |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
358 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
359 |
(* Stuff for "equations" ((int*int*int)->num functions). *) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
360 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
361 |
fun tri_equation_cmul c eq = |
39027 | 362 |
if c =/ rat_0 then Inttriplefunc.empty else Inttriplefunc.map (fn _ => fn d => c */ d) eq; |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
363 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
364 |
fun tri_equation_add eq1 eq2 = Inttriplefunc.combine (curry op +/) (fn x => x =/ rat_0) eq1 eq2; |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
365 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
366 |
fun tri_equation_eval assig eq = |
32839 | 367 |
let fun value v = Inttriplefunc.apply assig v |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
368 |
in Inttriplefunc.fold (fn (v, c) => fn a => a +/ value v */ c) eq rat_0 |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
369 |
end; |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
370 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
371 |
(* Eliminate all variables, in an essentially arbitrary order. *) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
372 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
373 |
fun tri_eliminate_all_equations one = |
32839 | 374 |
let |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
375 |
fun choose_variable eq = |
32839 | 376 |
let val (v,_) = Inttriplefunc.choose eq |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
377 |
in if is_equal (triple_int_ord(v,one)) then |
32839 | 378 |
let val eq' = Inttriplefunc.delete_safe v eq |
379 |
in if Inttriplefunc.is_empty eq' then error "choose_variable" |
|
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
380 |
else fst (Inttriplefunc.choose eq') |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
381 |
end |
32839 | 382 |
else v |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
383 |
end |
32839 | 384 |
fun eliminate dun eqs = case eqs of |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
385 |
[] => dun |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
386 |
| eq::oeqs => |
32829
671eb46eb0a3
tuned FuncFun and FuncUtil structure in positivstellensatz.ML
Philipp Meyer
parents:
32828
diff
changeset
|
387 |
if Inttriplefunc.is_empty eq then eliminate dun oeqs else |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
388 |
let val v = choose_variable eq |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
389 |
val a = Inttriplefunc.apply eq v |
32839 | 390 |
val eq' = tri_equation_cmul ((Rat.rat_of_int ~1) // a) |
32829
671eb46eb0a3
tuned FuncFun and FuncUtil structure in positivstellensatz.ML
Philipp Meyer
parents:
32828
diff
changeset
|
391 |
(Inttriplefunc.delete_safe v eq) |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
392 |
fun elim e = |
32839 | 393 |
let val b = Inttriplefunc.tryapplyd e v rat_0 |
394 |
in if b =/ rat_0 then e |
|
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
395 |
else tri_equation_add e (tri_equation_cmul (Rat.neg b // a) eq) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
396 |
end |
39027 | 397 |
in eliminate (Inttriplefunc.update(v, eq') (Inttriplefunc.map (K elim) dun)) |
32839 | 398 |
(map elim oeqs) |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
399 |
end |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
400 |
in fn eqs => |
32839 | 401 |
let |
32829
671eb46eb0a3
tuned FuncFun and FuncUtil structure in positivstellensatz.ML
Philipp Meyer
parents:
32828
diff
changeset
|
402 |
val assig = eliminate Inttriplefunc.empty eqs |
44453 | 403 |
val vs = Inttriplefunc.fold (fn (_, f) => fn a => remove (dest_ord triple_int_ord) one (Inttriplefunc.dom f) @ a) assig [] |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
404 |
in (distinct (dest_ord triple_int_ord) vs,assig) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
405 |
end |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
406 |
end; |
32839 | 407 |
|
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
408 |
(* Multiply equation-parametrized poly by regular poly and add accumulator. *) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
409 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
410 |
fun tri_epoly_pmul p q acc = |
32828 | 411 |
FuncUtil.Monomialfunc.fold (fn (m1, c) => fn a => |
412 |
FuncUtil.Monomialfunc.fold (fn (m2,e) => fn b => |
|
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
413 |
let val m = monomial_mul m1 m2 |
32839 | 414 |
val es = FuncUtil.Monomialfunc.tryapplyd b m Inttriplefunc.empty |
415 |
in FuncUtil.Monomialfunc.update (m,tri_equation_add (tri_equation_cmul c e) es) b |
|
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
416 |
end) q a) p acc ; |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
417 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
418 |
(* Hence produce the "relevant" monomials: those whose squares lie in the *) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
419 |
(* Newton polytope of the monomials in the input. (This is enough according *) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
420 |
(* to Reznik: "Extremal PSD forms with few terms", Duke Math. Journal, *) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
421 |
(* vol 45, pp. 363--374, 1978. *) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
422 |
(* *) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
423 |
(* These are ordered in sort of decreasing degree. In particular the *) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
424 |
(* constant monomial is last; this gives an order in diagonalization of the *) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
425 |
(* quadratic form that will tend to display constants. *) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
426 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
427 |
(* Diagonalize (Cholesky/LDU) the matrix corresponding to a quadratic form. *) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
428 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
429 |
local |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
430 |
fun diagonalize n i m = |
32839 | 431 |
if FuncUtil.Intpairfunc.is_empty (snd m) then [] |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
432 |
else |
32839 | 433 |
let val a11 = FuncUtil.Intpairfunc.tryapplyd (snd m) (i,i) rat_0 |
32332 | 434 |
in if a11 </ rat_0 then raise Failure "diagonalize: not PSD" |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
435 |
else if a11 =/ rat_0 then |
32829
671eb46eb0a3
tuned FuncFun and FuncUtil structure in positivstellensatz.ML
Philipp Meyer
parents:
32828
diff
changeset
|
436 |
if FuncUtil.Intfunc.is_empty (snd (row i m)) then diagonalize n (i + 1) m |
32332 | 437 |
else raise Failure "diagonalize: not PSD ___ " |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
438 |
else |
32839 | 439 |
let |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
440 |
val v = row i m |
32839 | 441 |
val v' = (fst v, FuncUtil.Intfunc.fold (fn (i, c) => fn a => |
442 |
let val y = c // a11 |
|
443 |
in if y = rat_0 then a else FuncUtil.Intfunc.update (i,y) a |
|
32829
671eb46eb0a3
tuned FuncFun and FuncUtil structure in positivstellensatz.ML
Philipp Meyer
parents:
32828
diff
changeset
|
444 |
end) (snd v) FuncUtil.Intfunc.empty) |
32828 | 445 |
fun upt0 x y a = if y = rat_0 then a else FuncUtil.Intpairfunc.update (x,y) a |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
446 |
val m' = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
447 |
((n,n), |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
448 |
iter (i+1,n) (fn j => |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
449 |
iter (i+1,n) (fn k => |
32828 | 450 |
(upt0 (j,k) (FuncUtil.Intpairfunc.tryapplyd (snd m) (j,k) rat_0 -/ FuncUtil.Intfunc.tryapplyd (snd v) j rat_0 */ FuncUtil.Intfunc.tryapplyd (snd v') k rat_0)))) |
32829
671eb46eb0a3
tuned FuncFun and FuncUtil structure in positivstellensatz.ML
Philipp Meyer
parents:
32828
diff
changeset
|
451 |
FuncUtil.Intpairfunc.empty) |
32839 | 452 |
in (a11,v')::diagonalize n (i + 1) m' |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
453 |
end |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
454 |
end |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
455 |
in |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
456 |
fun diag m = |
32839 | 457 |
let |
458 |
val nn = dimensions m |
|
459 |
val n = fst nn |
|
460 |
in if snd nn <> n then error "diagonalize: non-square matrix" |
|
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
461 |
else diagonalize n 1 m |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
462 |
end |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
463 |
end; |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
464 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
465 |
(* Enumeration of monomials with given multidegree bound. *) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
466 |
|
32839 | 467 |
fun enumerate_monomials d vars = |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
468 |
if d < 0 then [] |
32829
671eb46eb0a3
tuned FuncFun and FuncUtil structure in positivstellensatz.ML
Philipp Meyer
parents:
32828
diff
changeset
|
469 |
else if d = 0 then [FuncUtil.Ctermfunc.empty] |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
470 |
else if null vars then [monomial_1] else |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
471 |
let val alts = |
33063 | 472 |
map_range (fn k => let val oths = enumerate_monomials (d - k) (tl vars) |
473 |
in map (fn ks => if k = 0 then ks else FuncUtil.Ctermfunc.update (hd vars, k) ks) oths end) (d + 1) |
|
32830 | 474 |
in flat alts |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
475 |
end; |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
476 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
477 |
(* Enumerate products of distinct input polys with degree <= d. *) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
478 |
(* We ignore any constant input polynomials. *) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
479 |
(* Give the output polynomial and a record of how it was derived. *) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
480 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
481 |
fun enumerate_products d pols = |
32839 | 482 |
if d = 0 then [(poly_const rat_1,RealArith.Rational_lt rat_1)] |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
483 |
else if d < 0 then [] else |
32839 | 484 |
case pols of |
32828 | 485 |
[] => [(poly_const rat_1,RealArith.Rational_lt rat_1)] |
32839 | 486 |
| (p,b)::ps => |
487 |
let val e = multidegree p |
|
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
488 |
in if e = 0 then enumerate_products d ps else |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
489 |
enumerate_products d ps @ |
32828 | 490 |
map (fn (q,c) => (poly_mul p q,RealArith.Product(b,c))) |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
491 |
(enumerate_products (d - e) ps) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
492 |
end |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
493 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
494 |
(* Convert regular polynomial. Note that we treat (0,0,0) as -1. *) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
495 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
496 |
fun epoly_of_poly p = |
32829
671eb46eb0a3
tuned FuncFun and FuncUtil structure in positivstellensatz.ML
Philipp Meyer
parents:
32828
diff
changeset
|
497 |
FuncUtil.Monomialfunc.fold (fn (m,c) => fn a => FuncUtil.Monomialfunc.update (m, Inttriplefunc.onefunc ((0,0,0), Rat.neg c)) a) p FuncUtil.Monomialfunc.empty; |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
498 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
499 |
(* String for block diagonal matrix numbered k. *) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
500 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
501 |
fun sdpa_of_blockdiagonal k m = |
32839 | 502 |
let |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
503 |
val pfx = string_of_int k ^" " |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
504 |
val ents = |
32839 | 505 |
Inttriplefunc.fold |
506 |
(fn ((b,i,j),c) => fn a => if i > j then a else ((b,i,j),c)::a) |
|
507 |
m [] |
|
508 |
val entss = sort (triple_int_ord o pairself fst) ents |
|
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
509 |
in fold_rev (fn ((b,i,j),c) => fn a => |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
510 |
pfx ^ string_of_int b ^ " " ^ string_of_int i ^ " " ^ string_of_int j ^ |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
511 |
" " ^ decimalize 20 c ^ "\n" ^ a) entss "" |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
512 |
end; |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
513 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
514 |
(* SDPA for problem using block diagonal (i.e. multiple SDPs) *) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
515 |
|
32268
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
32150
diff
changeset
|
516 |
fun sdpa_of_blockproblem nblocks blocksizes obj mats = |
32839 | 517 |
let val m = length mats - 1 |
32268
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
32150
diff
changeset
|
518 |
in |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
519 |
string_of_int m ^ "\n" ^ |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
520 |
string_of_int nblocks ^ "\n" ^ |
32830 | 521 |
(space_implode " " (map string_of_int blocksizes)) ^ |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
522 |
"\n" ^ |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
523 |
sdpa_of_vector obj ^ |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
524 |
fold_rev2 (fn k => fn m => fn a => sdpa_of_blockdiagonal (k - 1) m ^ a) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
525 |
(1 upto length mats) mats "" |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
526 |
end; |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
527 |
|
32268
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
32150
diff
changeset
|
528 |
(* Run prover on a problem in block diagonal form. *) |
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
32150
diff
changeset
|
529 |
|
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
32150
diff
changeset
|
530 |
fun run_blockproblem prover nblocks blocksizes obj mats= |
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
32150
diff
changeset
|
531 |
parse_csdpoutput (prover (sdpa_of_blockproblem nblocks blocksizes obj mats)) |
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
32150
diff
changeset
|
532 |
|
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
533 |
(* 3D versions of matrix operations to consider blocks separately. *) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
534 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
535 |
val bmatrix_add = Inttriplefunc.combine (curry op +/) (fn x => x =/ rat_0); |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
536 |
fun bmatrix_cmul c bm = |
32829
671eb46eb0a3
tuned FuncFun and FuncUtil structure in positivstellensatz.ML
Philipp Meyer
parents:
32828
diff
changeset
|
537 |
if c =/ rat_0 then Inttriplefunc.empty |
39027 | 538 |
else Inttriplefunc.map (fn _ => fn x => c */ x) bm; |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
539 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
540 |
val bmatrix_neg = bmatrix_cmul (Rat.rat_of_int ~1); |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
541 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
542 |
(* Smash a block matrix into components. *) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
543 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
544 |
fun blocks blocksizes bm = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
545 |
map (fn (bs,b0) => |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
546 |
let val m = Inttriplefunc.fold |
32829
671eb46eb0a3
tuned FuncFun and FuncUtil structure in positivstellensatz.ML
Philipp Meyer
parents:
32828
diff
changeset
|
547 |
(fn ((b,i,j),c) => fn a => if b = b0 then FuncUtil.Intpairfunc.update ((i,j),c) a else a) bm FuncUtil.Intpairfunc.empty |
44453 | 548 |
val _ = FuncUtil.Intpairfunc.fold (fn ((i,j),_) => fn a => max a (max i j)) m 0 |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
549 |
in (((bs,bs),m):matrix) end) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
550 |
(blocksizes ~~ (1 upto length blocksizes));; |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
551 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
552 |
(* FIXME : Get rid of this !!!*) |
32268
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
32150
diff
changeset
|
553 |
local |
44453 | 554 |
fun tryfind_with msg _ [] = raise Failure msg |
555 |
| tryfind_with _ f (x::xs) = (f x handle Failure s => tryfind_with s f xs); |
|
32839 | 556 |
in |
32268
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
32150
diff
changeset
|
557 |
fun tryfind f = tryfind_with "tryfind" f |
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
32150
diff
changeset
|
558 |
end |
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
32150
diff
changeset
|
559 |
|
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
560 |
(* Positiv- and Nullstellensatz. Flag "linf" forces a linear representation. *) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
561 |
|
32839 | 562 |
|
38805 | 563 |
fun real_positivnullstellensatz_general ctxt prover linf d eqs leqs pol = |
32839 | 564 |
let |
33042 | 565 |
val vars = fold_rev (union (op aconvc) o poly_variables) |
566 |
(pol :: eqs @ map fst leqs) [] |
|
32839 | 567 |
val monoid = if linf then |
32828 | 568 |
(poly_const rat_1,RealArith.Rational_lt rat_1):: |
44453 | 569 |
(filter (fn (p,_) => multidegree p <= d) leqs) |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
570 |
else enumerate_products d leqs |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
571 |
val nblocks = length monoid |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
572 |
fun mk_idmultiplier k p = |
32839 | 573 |
let |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
574 |
val e = d - multidegree p |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
575 |
val mons = enumerate_monomials e vars |
32839 | 576 |
val nons = mons ~~ (1 upto length mons) |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
577 |
in (mons, |
32829
671eb46eb0a3
tuned FuncFun and FuncUtil structure in positivstellensatz.ML
Philipp Meyer
parents:
32828
diff
changeset
|
578 |
fold_rev (fn (m,n) => FuncUtil.Monomialfunc.update(m,Inttriplefunc.onefunc((~k,~n,n),rat_1))) nons FuncUtil.Monomialfunc.empty) |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
579 |
end |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
580 |
|
44453 | 581 |
fun mk_sqmultiplier k (p,_) = |
32839 | 582 |
let |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
583 |
val e = (d - multidegree p) div 2 |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
584 |
val mons = enumerate_monomials e vars |
32839 | 585 |
val nons = mons ~~ (1 upto length mons) |
586 |
in (mons, |
|
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
587 |
fold_rev (fn (m1,n1) => |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
588 |
fold_rev (fn (m2,n2) => fn a => |
32839 | 589 |
let val m = monomial_mul m1 m2 |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
590 |
in if n1 > n2 then a else |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
591 |
let val c = if n1 = n2 then rat_1 else rat_2 |
32839 | 592 |
val e = FuncUtil.Monomialfunc.tryapplyd a m Inttriplefunc.empty |
32828 | 593 |
in FuncUtil.Monomialfunc.update(m, tri_equation_add (Inttriplefunc.onefunc((k,n1,n2), c)) e) a |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
594 |
end |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
595 |
end) nons) |
32829
671eb46eb0a3
tuned FuncFun and FuncUtil structure in positivstellensatz.ML
Philipp Meyer
parents:
32828
diff
changeset
|
596 |
nons FuncUtil.Monomialfunc.empty) |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
597 |
end |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
598 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
599 |
val (sqmonlist,sqs) = split_list (map2 mk_sqmultiplier (1 upto length monoid) monoid) |
44453 | 600 |
val (_(*idmonlist*),ids) = split_list(map2 mk_idmultiplier (1 upto length eqs) eqs) |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
601 |
val blocksizes = map length sqmonlist |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
602 |
val bigsum = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
603 |
fold_rev2 (fn p => fn q => fn a => tri_epoly_pmul p q a) eqs ids |
44453 | 604 |
(fold_rev2 (fn (p,_) => fn s => fn a => tri_epoly_pmul p s a) monoid sqs |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
605 |
(epoly_of_poly(poly_neg pol))) |
44453 | 606 |
val eqns = FuncUtil.Monomialfunc.fold (fn (_,e) => fn a => e::a) bigsum [] |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
607 |
val (pvs,assig) = tri_eliminate_all_equations (0,0,0) eqns |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
608 |
val qvars = (0,0,0)::pvs |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
609 |
val allassig = fold_rev (fn v => Inttriplefunc.update(v,(Inttriplefunc.onefunc(v,rat_1)))) pvs assig |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
610 |
fun mk_matrix v = |
32839 | 611 |
Inttriplefunc.fold (fn ((b,i,j), ass) => fn m => |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
612 |
if b < 0 then m else |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
613 |
let val c = Inttriplefunc.tryapplyd ass v rat_0 |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
614 |
in if c = rat_0 then m else |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
615 |
Inttriplefunc.update ((b,j,i), c) (Inttriplefunc.update ((b,i,j), c) m) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
616 |
end) |
32829
671eb46eb0a3
tuned FuncFun and FuncUtil structure in positivstellensatz.ML
Philipp Meyer
parents:
32828
diff
changeset
|
617 |
allassig Inttriplefunc.empty |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
618 |
val diagents = Inttriplefunc.fold |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
619 |
(fn ((b,i,j), e) => fn a => if b > 0 andalso i = j then tri_equation_add e a else a) |
32829
671eb46eb0a3
tuned FuncFun and FuncUtil structure in positivstellensatz.ML
Philipp Meyer
parents:
32828
diff
changeset
|
620 |
allassig Inttriplefunc.empty |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
621 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
622 |
val mats = map mk_matrix qvars |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
623 |
val obj = (length pvs, |
32828 | 624 |
itern 1 pvs (fn v => fn i => FuncUtil.Intfunc.updatep iszero (i,Inttriplefunc.tryapplyd diagents v rat_0)) |
32829
671eb46eb0a3
tuned FuncFun and FuncUtil structure in positivstellensatz.ML
Philipp Meyer
parents:
32828
diff
changeset
|
625 |
FuncUtil.Intfunc.empty) |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
626 |
val raw_vec = if null pvs then vector_0 0 |
32268
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
32150
diff
changeset
|
627 |
else tri_scale_then (run_blockproblem prover nblocks blocksizes) obj mats |
44453 | 628 |
fun int_element (_,v) i = FuncUtil.Intfunc.tryapplyd v i rat_0 |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
629 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
630 |
fun find_rounding d = |
32839 | 631 |
let |
32949
aa6c470a962a
eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents:
32839
diff
changeset
|
632 |
val _ = |
38805 | 633 |
if Config.get ctxt trace |
32949
aa6c470a962a
eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents:
32839
diff
changeset
|
634 |
then writeln ("Trying rounding with limit "^Rat.string_of_rat d ^ "\n") |
aa6c470a962a
eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents:
32839
diff
changeset
|
635 |
else () |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
636 |
val vec = nice_vector d raw_vec |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
637 |
val blockmat = iter (1,dim vec) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
638 |
(fn i => fn a => bmatrix_add (bmatrix_cmul (int_element vec i) (nth mats i)) a) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
639 |
(bmatrix_neg (nth mats 0)) |
32839 | 640 |
val allmats = blocks blocksizes blockmat |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
641 |
in (vec,map diag allmats) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
642 |
end |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
643 |
val (vec,ratdias) = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
644 |
if null pvs then find_rounding rat_1 |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
645 |
else tryfind find_rounding (map Rat.rat_of_int (1 upto 31) @ |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
646 |
map pow2 (5 upto 66)) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
647 |
val newassigs = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
648 |
fold_rev (fn k => Inttriplefunc.update (nth pvs (k - 1), int_element vec k)) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
649 |
(1 upto dim vec) (Inttriplefunc.onefunc ((0,0,0), Rat.rat_of_int ~1)) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
650 |
val finalassigs = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
651 |
Inttriplefunc.fold (fn (v,e) => fn a => Inttriplefunc.update(v, tri_equation_eval newassigs e) a) allassig newassigs |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
652 |
fun poly_of_epoly p = |
32828 | 653 |
FuncUtil.Monomialfunc.fold (fn (v,e) => fn a => FuncUtil.Monomialfunc.updatep iszero (v,tri_equation_eval finalassigs e) a) |
32829
671eb46eb0a3
tuned FuncFun and FuncUtil structure in positivstellensatz.ML
Philipp Meyer
parents:
32828
diff
changeset
|
654 |
p FuncUtil.Monomialfunc.empty |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
655 |
fun mk_sos mons = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
656 |
let fun mk_sq (c,m) = |
32828 | 657 |
(c,fold_rev (fn k=> fn a => FuncUtil.Monomialfunc.updatep iszero (nth mons (k - 1), int_element m k) a) |
32829
671eb46eb0a3
tuned FuncFun and FuncUtil structure in positivstellensatz.ML
Philipp Meyer
parents:
32828
diff
changeset
|
658 |
(1 upto length mons) FuncUtil.Monomialfunc.empty) |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
659 |
in map mk_sq |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
660 |
end |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
661 |
val sqs = map2 mk_sos sqmonlist ratdias |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
662 |
val cfs = map poly_of_epoly ids |
44453 | 663 |
val msq = filter (fn (_,b) => not (null b)) (map2 pair monoid sqs) |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
664 |
fun eval_sq sqs = fold_rev (fn (c,q) => poly_add (poly_cmul c (poly_mul q q))) sqs poly_0 |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
665 |
val sanity = |
44453 | 666 |
fold_rev (fn ((p,_),s) => poly_add (poly_mul p (eval_sq s))) msq |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
667 |
(fold_rev2 (fn p => fn q => poly_add (poly_mul p q)) cfs eqs |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
668 |
(poly_neg pol)) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
669 |
|
32829
671eb46eb0a3
tuned FuncFun and FuncUtil structure in positivstellensatz.ML
Philipp Meyer
parents:
32828
diff
changeset
|
670 |
in if not(FuncUtil.Monomialfunc.is_empty sanity) then raise Sanity else |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
671 |
(cfs,map (fn (a,b) => (snd a,b)) msq) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
672 |
end |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
673 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
674 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
675 |
(* Iterative deepening. *) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
676 |
|
32839 | 677 |
fun deepen f n = |
32949
aa6c470a962a
eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents:
32839
diff
changeset
|
678 |
(writeln ("Searching with depth limit " ^ string_of_int n); |
aa6c470a962a
eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents:
32839
diff
changeset
|
679 |
(f n handle Failure s => (writeln ("failed with message: " ^ s); deepen f (n + 1)))); |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
680 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
681 |
|
32645
1cc5b24f5a01
sos method generates and uses proof certificates
Philipp Meyer
parents:
32332
diff
changeset
|
682 |
(* Map back polynomials and their composites to a positivstellensatz. *) |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
683 |
|
32828 | 684 |
fun cterm_of_sqterm (c,p) = RealArith.Product(RealArith.Rational_lt c,RealArith.Square p); |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
685 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
686 |
fun cterm_of_sos (pr,sqs) = if null sqs then pr |
32830 | 687 |
else RealArith.Product(pr,foldr1 RealArith.Sum (map cterm_of_sqterm sqs)); |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
688 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
689 |
(* Interface to HOL. *) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
690 |
local |
32828 | 691 |
open Conv |
692 |
val concl = Thm.dest_arg o cprop_of |
|
35408 | 693 |
fun simple_cterm_ord t u = Term_Ord.fast_term_ord (term_of t, term_of u) = LESS |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
694 |
in |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
695 |
(* FIXME: Replace tryfind by get_first !! *) |
32645
1cc5b24f5a01
sos method generates and uses proof certificates
Philipp Meyer
parents:
32332
diff
changeset
|
696 |
fun real_nonlinear_prover proof_method ctxt = |
32839 | 697 |
let |
44453 | 698 |
val {add = _, mul = _, neg = _, pow = _, |
699 |
sub = _, main = real_poly_conv} = |
|
700 |
Semiring_Normalizer.semiring_normalizers_ord_wrapper ctxt |
|
36753
5cf4e9128f22
renamed Normalizer to the more specific Semiring_Normalizer
haftmann
parents:
36751
diff
changeset
|
701 |
(the (Semiring_Normalizer.match ctxt @{cterm "(0::real) + 1"})) |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
702 |
simple_cterm_ord |
32839 | 703 |
fun mainf cert_choice translator (eqs,les,lts) = |
704 |
let |
|
32828 | 705 |
val eq0 = map (poly_of_term o Thm.dest_arg1 o concl) eqs |
706 |
val le0 = map (poly_of_term o Thm.dest_arg o concl) les |
|
707 |
val lt0 = map (poly_of_term o Thm.dest_arg o concl) lts |
|
33063 | 708 |
val eqp0 = map_index (fn (i, t) => (t,RealArith.Axiom_eq i)) eq0 |
709 |
val lep0 = map_index (fn (i, t) => (t,RealArith.Axiom_le i)) le0 |
|
710 |
val ltp0 = map_index (fn (i, t) => (t,RealArith.Axiom_lt i)) lt0 |
|
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
711 |
val (keq,eq) = List.partition (fn (p,_) => multidegree p = 0) eqp0 |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
712 |
val (klep,lep) = List.partition (fn (p,_) => multidegree p = 0) lep0 |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
713 |
val (kltp,ltp) = List.partition (fn (p,_) => multidegree p = 0) ltp0 |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
714 |
fun trivial_axiom (p,ax) = |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
715 |
case ax of |
32839 | 716 |
RealArith.Axiom_eq n => if eval FuncUtil.Ctermfunc.empty p <>/ Rat.zero then nth eqs n |
32332 | 717 |
else raise Failure "trivial_axiom: Not a trivial axiom" |
32839 | 718 |
| RealArith.Axiom_le n => if eval FuncUtil.Ctermfunc.empty p </ Rat.zero then nth les n |
32332 | 719 |
else raise Failure "trivial_axiom: Not a trivial axiom" |
32839 | 720 |
| RealArith.Axiom_lt n => if eval FuncUtil.Ctermfunc.empty p <=/ Rat.zero then nth lts n |
32332 | 721 |
else raise Failure "trivial_axiom: Not a trivial axiom" |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
722 |
| _ => error "trivial_axiom: Not a trivial axiom" |
32839 | 723 |
in |
32645
1cc5b24f5a01
sos method generates and uses proof certificates
Philipp Meyer
parents:
32332
diff
changeset
|
724 |
(let val th = tryfind trivial_axiom (keq @ klep @ kltp) |
1cc5b24f5a01
sos method generates and uses proof certificates
Philipp Meyer
parents:
32332
diff
changeset
|
725 |
in |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
47108
diff
changeset
|
726 |
(fconv_rule (arg_conv (arg1_conv (real_poly_conv ctxt)) |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
47108
diff
changeset
|
727 |
then_conv Numeral_Simprocs.field_comp_conv ctxt) th, |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
47108
diff
changeset
|
728 |
RealArith.Trivial) |
32645
1cc5b24f5a01
sos method generates and uses proof certificates
Philipp Meyer
parents:
32332
diff
changeset
|
729 |
end) |
32839 | 730 |
handle Failure _ => |
32645
1cc5b24f5a01
sos method generates and uses proof certificates
Philipp Meyer
parents:
32332
diff
changeset
|
731 |
(let val proof = |
1cc5b24f5a01
sos method generates and uses proof certificates
Philipp Meyer
parents:
32332
diff
changeset
|
732 |
(case proof_method of Certificate certs => |
1cc5b24f5a01
sos method generates and uses proof certificates
Philipp Meyer
parents:
32332
diff
changeset
|
733 |
(* choose certificate *) |
1cc5b24f5a01
sos method generates and uses proof certificates
Philipp Meyer
parents:
32332
diff
changeset
|
734 |
let |
32828 | 735 |
fun chose_cert [] (RealArith.Cert c) = c |
736 |
| chose_cert (RealArith.Left::s) (RealArith.Branch (l, _)) = chose_cert s l |
|
737 |
| chose_cert (RealArith.Right::s) (RealArith.Branch (_, r)) = chose_cert s r |
|
32645
1cc5b24f5a01
sos method generates and uses proof certificates
Philipp Meyer
parents:
32332
diff
changeset
|
738 |
| chose_cert _ _ = error "certificate tree in invalid form" |
1cc5b24f5a01
sos method generates and uses proof certificates
Philipp Meyer
parents:
32332
diff
changeset
|
739 |
in |
1cc5b24f5a01
sos method generates and uses proof certificates
Philipp Meyer
parents:
32332
diff
changeset
|
740 |
chose_cert cert_choice certs |
1cc5b24f5a01
sos method generates and uses proof certificates
Philipp Meyer
parents:
32332
diff
changeset
|
741 |
end |
1cc5b24f5a01
sos method generates and uses proof certificates
Philipp Meyer
parents:
32332
diff
changeset
|
742 |
| Prover prover => |
1cc5b24f5a01
sos method generates and uses proof certificates
Philipp Meyer
parents:
32332
diff
changeset
|
743 |
(* call prover *) |
32839 | 744 |
let |
32645
1cc5b24f5a01
sos method generates and uses proof certificates
Philipp Meyer
parents:
32332
diff
changeset
|
745 |
val pol = fold_rev poly_mul (map fst ltp) (poly_const Rat.one) |
1cc5b24f5a01
sos method generates and uses proof certificates
Philipp Meyer
parents:
32332
diff
changeset
|
746 |
val leq = lep @ ltp |
1cc5b24f5a01
sos method generates and uses proof certificates
Philipp Meyer
parents:
32332
diff
changeset
|
747 |
fun tryall d = |
1cc5b24f5a01
sos method generates and uses proof certificates
Philipp Meyer
parents:
32332
diff
changeset
|
748 |
let val e = multidegree pol |
1cc5b24f5a01
sos method generates and uses proof certificates
Philipp Meyer
parents:
32332
diff
changeset
|
749 |
val k = if e = 0 then 0 else d div e |
32839 | 750 |
val eq' = map fst eq |
38805 | 751 |
in tryfind (fn i => (d,i,real_positivnullstellensatz_general ctxt prover false d eq' leq |
32645
1cc5b24f5a01
sos method generates and uses proof certificates
Philipp Meyer
parents:
32332
diff
changeset
|
752 |
(poly_neg(poly_pow pol i)))) |
1cc5b24f5a01
sos method generates and uses proof certificates
Philipp Meyer
parents:
32332
diff
changeset
|
753 |
(0 upto k) |
1cc5b24f5a01
sos method generates and uses proof certificates
Philipp Meyer
parents:
32332
diff
changeset
|
754 |
end |
44453 | 755 |
val (_,i,(cert_ideal,cert_cone)) = deepen tryall 0 |
32645
1cc5b24f5a01
sos method generates and uses proof certificates
Philipp Meyer
parents:
32332
diff
changeset
|
756 |
val proofs_ideal = |
44453 | 757 |
map2 (fn q => fn (_,ax) => RealArith.Eqmul(q,ax)) cert_ideal eq |
32645
1cc5b24f5a01
sos method generates and uses proof certificates
Philipp Meyer
parents:
32332
diff
changeset
|
758 |
val proofs_cone = map cterm_of_sos cert_cone |
32828 | 759 |
val proof_ne = if null ltp then RealArith.Rational_lt Rat.one else |
32839 | 760 |
let val p = foldr1 RealArith.Product (map snd ltp) |
32828 | 761 |
in funpow i (fn q => RealArith.Product(p,q)) (RealArith.Rational_lt Rat.one) |
32645
1cc5b24f5a01
sos method generates and uses proof certificates
Philipp Meyer
parents:
32332
diff
changeset
|
762 |
end |
32839 | 763 |
in |
764 |
foldr1 RealArith.Sum (proof_ne :: proofs_ideal @ proofs_cone) |
|
32645
1cc5b24f5a01
sos method generates and uses proof certificates
Philipp Meyer
parents:
32332
diff
changeset
|
765 |
end) |
1cc5b24f5a01
sos method generates and uses proof certificates
Philipp Meyer
parents:
32332
diff
changeset
|
766 |
in |
32828 | 767 |
(translator (eqs,les,lts) proof, RealArith.Cert proof) |
32645
1cc5b24f5a01
sos method generates and uses proof certificates
Philipp Meyer
parents:
32332
diff
changeset
|
768 |
end) |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
769 |
end |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
770 |
in mainf end |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
771 |
end |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
772 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
773 |
fun C f x y = f y x; |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
774 |
(* FIXME : This is very bad!!!*) |
32839 | 775 |
fun subst_conv eqs t = |
776 |
let |
|
46497
89ccf66aa73d
renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
wenzelm
parents:
44469
diff
changeset
|
777 |
val t' = fold (Thm.lambda o Thm.lhs_of) eqs t |
36945 | 778 |
in Conv.fconv_rule (Thm.beta_conversion true) (fold (C Thm.combination) eqs (Thm.reflexive t')) |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
779 |
end |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
780 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
781 |
(* A wrapper that tries to substitute away variables first. *) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
782 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
783 |
local |
32828 | 784 |
open Conv |
35408 | 785 |
fun simple_cterm_ord t u = Term_Ord.fast_term_ord (term_of t, term_of u) = LESS |
32828 | 786 |
val concl = Thm.dest_arg o cprop_of |
32839 | 787 |
val shuffle1 = |
36350 | 788 |
fconv_rule (rewr_conv @{lemma "(a + x == y) == (x == y - (a::real))" by (atomize (full)) (simp add: field_simps) }) |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
789 |
val shuffle2 = |
36350 | 790 |
fconv_rule (rewr_conv @{lemma "(x + a == y) == (x == y - (a::real))" by (atomize (full)) (simp add: field_simps)}) |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
791 |
fun substitutable_monomial fvs tm = case term_of tm of |
32839 | 792 |
Free(_,@{typ real}) => if not (member (op aconvc) fvs tm) then (Rat.one,tm) |
32332 | 793 |
else raise Failure "substitutable_monomial" |
44453 | 794 |
| @{term "op * :: real => _"}$_$(Free _) => |
32828 | 795 |
if RealArith.is_ratconst (Thm.dest_arg1 tm) andalso not (member (op aconvc) fvs (Thm.dest_arg tm)) |
796 |
then (RealArith.dest_ratconst (Thm.dest_arg1 tm),Thm.dest_arg tm) else raise Failure "substitutable_monomial" |
|
44453 | 797 |
| @{term "op + :: real => _"}$_$_ => |
32828 | 798 |
(substitutable_monomial (Thm.add_cterm_frees (Thm.dest_arg tm) fvs) (Thm.dest_arg1 tm) |
799 |
handle Failure _ => substitutable_monomial (Thm.add_cterm_frees (Thm.dest_arg1 tm) fvs) (Thm.dest_arg tm)) |
|
32332 | 800 |
| _ => raise Failure "substitutable_monomial" |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
801 |
|
32839 | 802 |
fun isolate_variable v th = |
32828 | 803 |
let val w = Thm.dest_arg1 (cprop_of th) |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
804 |
in if v aconvc w then th |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
805 |
else case term_of w of |
44453 | 806 |
@{term "op + :: real => _"}$_$_ => |
32839 | 807 |
if Thm.dest_arg1 w aconvc v then shuffle2 th |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
808 |
else isolate_variable v (shuffle1 th) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
809 |
| _ => error "isolate variable : This should not happen?" |
32839 | 810 |
end |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
811 |
in |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
812 |
|
32268
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
32150
diff
changeset
|
813 |
fun real_nonlinear_subst_prover prover ctxt = |
32839 | 814 |
let |
44453 | 815 |
val {add = _, mul = real_poly_mul_conv, neg = _, |
816 |
pow = _, sub = _, main = real_poly_conv} = |
|
817 |
Semiring_Normalizer.semiring_normalizers_ord_wrapper ctxt |
|
36753
5cf4e9128f22
renamed Normalizer to the more specific Semiring_Normalizer
haftmann
parents:
36751
diff
changeset
|
818 |
(the (Semiring_Normalizer.match ctxt @{cterm "(0::real) + 1"})) |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
819 |
simple_cterm_ord |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
820 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
821 |
fun make_substitution th = |
32839 | 822 |
let |
32828 | 823 |
val (c,v) = substitutable_monomial [] (Thm.dest_arg1(concl th)) |
46497
89ccf66aa73d
renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
wenzelm
parents:
44469
diff
changeset
|
824 |
val th1 = Drule.arg_cong_rule (Thm.apply @{cterm "op * :: real => _"} (RealArith.cterm_of_rat (Rat.inv c))) (mk_meta_eq th) |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
47108
diff
changeset
|
825 |
val th2 = fconv_rule (binop_conv (real_poly_mul_conv ctxt)) th1 |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
47108
diff
changeset
|
826 |
in fconv_rule (arg_conv (real_poly_conv ctxt)) (isolate_variable v th2) |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
827 |
end |
32839 | 828 |
fun oprconv cv ct = |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
829 |
let val g = Thm.dest_fun2 ct |
32839 | 830 |
in if g aconvc @{cterm "op <= :: real => _"} |
831 |
orelse g aconvc @{cterm "op < :: real => _"} |
|
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
832 |
then arg_conv cv ct else arg1_conv cv ct |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
833 |
end |
32645
1cc5b24f5a01
sos method generates and uses proof certificates
Philipp Meyer
parents:
32332
diff
changeset
|
834 |
fun mainf cert_choice translator = |
32839 | 835 |
let |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
836 |
fun substfirst(eqs,les,lts) = |
32839 | 837 |
((let |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
838 |
val eth = tryfind make_substitution eqs |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
47108
diff
changeset
|
839 |
val modify = |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
47108
diff
changeset
|
840 |
fconv_rule (arg_conv (oprconv(subst_conv [eth] then_conv (real_poly_conv ctxt)))) |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
841 |
in substfirst |
32839 | 842 |
(filter_out (fn t => (Thm.dest_arg1 o Thm.dest_arg o cprop_of) t |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
843 |
aconvc @{cterm "0::real"}) (map modify eqs), |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
844 |
map modify les,map modify lts) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
845 |
end) |
32645
1cc5b24f5a01
sos method generates and uses proof certificates
Philipp Meyer
parents:
32332
diff
changeset
|
846 |
handle Failure _ => real_nonlinear_prover prover ctxt cert_choice translator (rev eqs, rev les, rev lts)) |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
847 |
in substfirst |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
848 |
end |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
849 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
850 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
851 |
in mainf |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
852 |
end |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
853 |
|
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
854 |
(* Overall function. *) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
855 |
|
32645
1cc5b24f5a01
sos method generates and uses proof certificates
Philipp Meyer
parents:
32332
diff
changeset
|
856 |
fun real_sos prover ctxt = |
32828 | 857 |
RealArith.gen_prover_real_arith ctxt (real_nonlinear_subst_prover prover ctxt) |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
858 |
end; |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
859 |
|
32839 | 860 |
val known_sos_constants = |
861 |
[@{term "op ==>"}, @{term "Trueprop"}, |
|
38795
848be46708dc
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents:
38786
diff
changeset
|
862 |
@{term HOL.implies}, @{term HOL.conj}, @{term HOL.disj}, |
32839 | 863 |
@{term "Not"}, @{term "op = :: bool => _"}, |
864 |
@{term "All :: (real => _) => _"}, @{term "Ex :: (real => _) => _"}, |
|
865 |
@{term "op = :: real => _"}, @{term "op < :: real => _"}, |
|
866 |
@{term "op <= :: real => _"}, |
|
867 |
@{term "op + :: real => _"}, @{term "op - :: real => _"}, |
|
868 |
@{term "op * :: real => _"}, @{term "uminus :: real => _"}, |
|
31512 | 869 |
@{term "op / :: real => _"}, @{term "inverse :: real => _"}, |
32839 | 870 |
@{term "op ^ :: real => _"}, @{term "abs :: real => _"}, |
31512 | 871 |
@{term "min :: real => _"}, @{term "max :: real => _"}, |
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46497
diff
changeset
|
872 |
@{term "0::real"}, @{term "1::real"}, |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46497
diff
changeset
|
873 |
@{term "numeral :: num => nat"}, |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46497
diff
changeset
|
874 |
@{term "numeral :: num => real"}, |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46497
diff
changeset
|
875 |
@{term "neg_numeral :: num => real"}, |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46497
diff
changeset
|
876 |
@{term "Num.Bit0"}, @{term "Num.Bit1"}, @{term "Num.One"}]; |
31512 | 877 |
|
32839 | 878 |
fun check_sos kcts ct = |
31512 | 879 |
let |
880 |
val t = term_of ct |
|
32839 | 881 |
val _ = if not (null (Term.add_tfrees t []) |
882 |
andalso null (Term.add_tvars t [])) |
|
31512 | 883 |
then error "SOS: not sos. Additional type varables" else () |
884 |
val fs = Term.add_frees t [] |
|
32839 | 885 |
val _ = if exists (fn ((_,T)) => not (T = @{typ "real"})) fs |
31512 | 886 |
then error "SOS: not sos. Variables with type not real" else () |
887 |
val vs = Term.add_vars t [] |
|
32839 | 888 |
val _ = if exists (fn ((_,T)) => not (T = @{typ "real"})) vs |
31512 | 889 |
then error "SOS: not sos. Variables with type not real" else () |
890 |
val ukcs = subtract (fn (t,p) => Const p aconv t) kcts (Term.add_consts t []) |
|
32839 | 891 |
val _ = if null ukcs then () |
31512 | 892 |
else error ("SOSO: Unknown constants in Subgoal:" ^ commas (map fst ukcs)) |
893 |
in () end |
|
894 |
||
32838
d9dfd30af9ae
core_sos_tac: SUBPROOF body operates on subgoal 1;
wenzelm
parents:
32831
diff
changeset
|
895 |
fun core_sos_tac print_cert prover = SUBPROOF (fn {concl, context, ...} => |
32831 | 896 |
let |
32838
d9dfd30af9ae
core_sos_tac: SUBPROOF body operates on subgoal 1;
wenzelm
parents:
32831
diff
changeset
|
897 |
val _ = check_sos known_sos_constants concl |
d9dfd30af9ae
core_sos_tac: SUBPROOF body operates on subgoal 1;
wenzelm
parents:
32831
diff
changeset
|
898 |
val (ths, certificates) = real_sos prover context (Thm.dest_arg concl) |
d9dfd30af9ae
core_sos_tac: SUBPROOF body operates on subgoal 1;
wenzelm
parents:
32831
diff
changeset
|
899 |
val _ = print_cert certificates |
d9dfd30af9ae
core_sos_tac: SUBPROOF body operates on subgoal 1;
wenzelm
parents:
32831
diff
changeset
|
900 |
in rtac ths 1 end) |
31131 | 901 |
|
44453 | 902 |
fun default_SOME _ NONE v = SOME v |
903 |
| default_SOME _ (SOME v) _ = SOME v; |
|
31131 | 904 |
|
905 |
fun lift_SOME f NONE a = f a |
|
44453 | 906 |
| lift_SOME _ (SOME a) _ = SOME a; |
31131 | 907 |
|
908 |
||
909 |
local |
|
910 |
val is_numeral = can (HOLogic.dest_number o term_of) |
|
911 |
in |
|
912 |
fun get_denom b ct = case term_of ct of |
|
32839 | 913 |
@{term "op / :: real => _"} $ _ $ _ => |
31131 | 914 |
if is_numeral (Thm.dest_arg ct) then get_denom b (Thm.dest_arg1 ct) |
915 |
else default_SOME (get_denom b) (get_denom b (Thm.dest_arg ct)) (Thm.dest_arg ct, b) |
|
916 |
| @{term "op < :: real => _"} $ _ $ _ => lift_SOME (get_denom true) (get_denom true (Thm.dest_arg ct)) (Thm.dest_arg1 ct) |
|
917 |
| @{term "op <= :: real => _"} $ _ $ _ => lift_SOME (get_denom true) (get_denom true (Thm.dest_arg ct)) (Thm.dest_arg1 ct) |
|
918 |
| _ $ _ => lift_SOME (get_denom b) (get_denom b (Thm.dest_fun ct)) (Thm.dest_arg ct) |
|
919 |
| _ => NONE |
|
920 |
end; |
|
921 |
||
32839 | 922 |
fun elim_one_denom_tac ctxt = |
923 |
CSUBGOAL (fn (P,i) => |
|
924 |
case get_denom false P of |
|
31131 | 925 |
NONE => no_tac |
32839 | 926 |
| SOME (d,ord) => |
927 |
let |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
47108
diff
changeset
|
928 |
val simp_ctxt = |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
47108
diff
changeset
|
929 |
ctxt addsimps @{thms field_simps} |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
47108
diff
changeset
|
930 |
addsimps [@{thm nonzero_power_divide}, @{thm power_divide}] |
32839 | 931 |
val th = instantiate' [] [SOME d, SOME (Thm.dest_arg P)] |
31131 | 932 |
(if ord then @{lemma "(d=0 --> P) & (d>0 --> P) & (d<(0::real) --> P) ==> P" by auto} |
933 |
else @{lemma "(d=0 --> P) & (d ~= (0::real) --> P) ==> P" by blast}) |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
47108
diff
changeset
|
934 |
in rtac th i THEN Simplifier.asm_full_simp_tac simp_ctxt i end); |
31131 | 935 |
|
936 |
fun elim_denom_tac ctxt i = REPEAT (elim_one_denom_tac ctxt i); |
|
937 |
||
32949
aa6c470a962a
eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents:
32839
diff
changeset
|
938 |
fun sos_tac print_cert prover ctxt = |
35625 | 939 |
Object_Logic.full_atomize_tac THEN' |
32949
aa6c470a962a
eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents:
32839
diff
changeset
|
940 |
elim_denom_tac ctxt THEN' |
aa6c470a962a
eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents:
32839
diff
changeset
|
941 |
core_sos_tac print_cert prover ctxt; |
31131 | 942 |
|
31512 | 943 |
end; |