author | Christian Sternagel |
Thu, 30 Aug 2012 15:44:03 +0900 | |
changeset 49093 | fdc301f592c4 |
parent 47455 | 26315a545e26 |
child 51989 | 700693cb96f1 |
permissions | -rw-r--r-- |
47455 | 1 |
(* Title: HOL/Matrix_LP/matrixlp.ML |
20787
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
2 |
Author: Steven Obua |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
3 |
*) |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
4 |
|
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
5 |
signature MATRIX_LP = |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
6 |
sig |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
7 |
val matrix_compute : cterm -> thm |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
8 |
val matrix_simplify : thm -> thm |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
9 |
val prove_bound : string -> int -> thm |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
10 |
val float2real : string * string -> Real.real |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
11 |
end |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
12 |
|
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
13 |
structure MatrixLP : MATRIX_LP = |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
14 |
struct |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
15 |
|
46540 | 16 |
val compute_thms = ComputeHOL.prep_thms @{thms "ComputeHOL.compute_list_case" "ComputeHOL.compute_let" |
17 |
"ComputeHOL.compute_if" "ComputeFloat.arith" "SparseMatrix.sparse_row_matrix_arith_simps" |
|
18 |
"ComputeHOL.compute_bool" "ComputeHOL.compute_pair" |
|
46544 | 19 |
"SparseMatrix.sorted_sp_simps" |
20 |
"ComputeNumeral.natnorm"}; (*"ComputeNumeral.number_norm"*) |
|
23665
825bea0266db
adopted to new computing oracle and fixed bugs introduced by tuning
obua
parents:
22964
diff
changeset
|
21 |
|
46540 | 22 |
val spm_mult_le_dual_prts_no_let_real = @{thm "spm_mult_le_dual_prts_no_let" [where ?'a = real]} |
20787
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
23 |
|
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
24 |
fun lp_dual_estimate_prt lptfile prec = |
46540 | 25 |
let |
26 |
val cert = cterm_of @{theory} |
|
27 |
fun var s x = (cert (Var ((s, 0), FloatSparseMatrixBuilder.spmatT)), x) |
|
28 |
val l = Fspmlp.load lptfile prec false |
|
29 |
val (y, (A1, A2), (c1, c2), b, (r1, r2)) = |
|
30 |
let |
|
31 |
open Fspmlp |
|
32 |
in |
|
33 |
(y l |> cert, A l |> pairself cert, c l |> pairself cert, b l |> cert, r12 l |> pairself cert) |
|
34 |
end |
|
35 |
in |
|
36 |
Thm.instantiate ([], |
|
37 |
[var "A1" A1, var "A2" A2, var "y" y, var "c1" c1, var "c2" c2, var "r1" r1, var "r2" r2, var "b" b]) |
|
38 |
spm_mult_le_dual_prts_no_let_real |
|
39 |
end |
|
20787
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
40 |
|
46540 | 41 |
val computer = PCompute.make Compute.SML @{theory} compute_thms [] |
20787
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
42 |
|
23665
825bea0266db
adopted to new computing oracle and fixed bugs introduced by tuning
obua
parents:
22964
diff
changeset
|
43 |
fun matrix_compute c = hd (PCompute.rewrite computer [c]) |
20787
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
44 |
|
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
45 |
fun matrix_simplify th = |
46540 | 46 |
let |
47 |
val simp_th = matrix_compute (cprop_of th) |
|
48 |
val th = Thm.strip_shyps (Thm.equal_elim simp_th th) |
|
49 |
fun removeTrue th = removeTrue (Thm.implies_elim th TrueI) handle THM _ => th |
|
50 |
in |
|
51 |
removeTrue th |
|
52 |
end |
|
20787
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
53 |
|
46541 | 54 |
val prove_bound = matrix_simplify oo lp_dual_estimate_prt; |
20787
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
55 |
|
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
56 |
val realFromStr = the o Real.fromString; |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
57 |
fun float2real (x, y) = realFromStr x * Math.pow (2.0, realFromStr y); |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
58 |
|
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
59 |
end |