author | haftmann |
Fri, 10 Feb 2012 22:51:21 +0100 | |
changeset 46531 | eff798e48efc |
parent 44121 | 44adaa6db327 |
child 46540 | 5522e28a566e |
permissions | -rw-r--r-- |
37788 | 1 |
(* Title: HOL/Matrix/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 lp_dual_estimate_prt : string -> int -> thm |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
8 |
val lp_dual_estimate_prt_primitive : |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
9 |
cterm * (cterm * cterm) * (cterm * cterm) * cterm * (cterm * cterm) -> thm |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
10 |
val matrix_compute : cterm -> thm |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
11 |
val matrix_simplify : thm -> thm |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
12 |
val prove_bound : string -> int -> thm |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
13 |
val float2real : string * string -> Real.real |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
14 |
end |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
15 |
|
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
16 |
structure MatrixLP : MATRIX_LP = |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
17 |
struct |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
18 |
|
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
19 |
fun inst_real thm = |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
20 |
let val certT = ctyp_of (Thm.theory_of_thm thm) in |
35021
c839a4c670c6
renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
wenzelm
parents:
32957
diff
changeset
|
21 |
Drule.export_without_context (Thm.instantiate |
44121 | 22 |
([(certT (TVar (hd (Misc_Legacy.term_tvars (prop_of thm)))), certT HOLogic.realT)], []) thm) |
20787
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
23 |
end |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
24 |
|
23665
825bea0266db
adopted to new computing oracle and fixed bugs introduced by tuning
obua
parents:
22964
diff
changeset
|
25 |
local |
825bea0266db
adopted to new computing oracle and fixed bugs introduced by tuning
obua
parents:
22964
diff
changeset
|
26 |
|
28637 | 27 |
val cert = cterm_of @{theory} |
23665
825bea0266db
adopted to new computing oracle and fixed bugs introduced by tuning
obua
parents:
22964
diff
changeset
|
28 |
|
825bea0266db
adopted to new computing oracle and fixed bugs introduced by tuning
obua
parents:
22964
diff
changeset
|
29 |
in |
20787
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
30 |
|
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
31 |
fun lp_dual_estimate_prt_primitive (y, (A1, A2), (c1, c2), b, (r1, r2)) = |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
32 |
let |
27484 | 33 |
val th = inst_real @{thm "spm_mult_le_dual_prts_no_let"} |
22964 | 34 |
fun var s x = (cert (Var ((s,0), FloatSparseMatrixBuilder.spmatT)), x) |
20787
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
35 |
val th = Thm.instantiate ([], [var "A1" A1, var "A2" A2, var "y" y, var "c1" c1, var "c2" c2, |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
36 |
var "r1" r1, var "r2" r2, var "b" b]) th |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
37 |
in th end |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
38 |
|
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
39 |
fun lp_dual_estimate_prt lptfile prec = |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
40 |
let |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
41 |
val certificate = |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
42 |
let |
22964 | 43 |
open Fspmlp |
20787
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
44 |
val l = load lptfile prec false |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
45 |
in |
23665
825bea0266db
adopted to new computing oracle and fixed bugs introduced by tuning
obua
parents:
22964
diff
changeset
|
46 |
(y l |> cert, A l |> pairself cert, c l |> pairself cert, b l |> cert, r12 l |> pairself cert) |
20787
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
47 |
end |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
48 |
in |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
49 |
lp_dual_estimate_prt_primitive certificate |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
50 |
end |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
51 |
|
23665
825bea0266db
adopted to new computing oracle and fixed bugs introduced by tuning
obua
parents:
22964
diff
changeset
|
52 |
end |
20787
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
53 |
|
23665
825bea0266db
adopted to new computing oracle and fixed bugs introduced by tuning
obua
parents:
22964
diff
changeset
|
54 |
local |
27484 | 55 |
val ths = ComputeHOL.prep_thms @{thms "ComputeHOL.compute_list_case" "ComputeHOL.compute_let" |
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29270
diff
changeset
|
56 |
"ComputeHOL.compute_if" "ComputeFloat.arith" "SparseMatrix.sparse_row_matrix_arith_simps" |
27484 | 57 |
"ComputeHOL.compute_bool" "ComputeHOL.compute_pair" |
58 |
"SparseMatrix.sorted_sp_simps" "ComputeNumeral.number_norm" |
|
59 |
"ComputeNumeral.natnorm"}; |
|
28637 | 60 |
val computer = PCompute.make Compute.SML @{theory} ths [] |
23665
825bea0266db
adopted to new computing oracle and fixed bugs introduced by tuning
obua
parents:
22964
diff
changeset
|
61 |
in |
20787
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
62 |
|
23665
825bea0266db
adopted to new computing oracle and fixed bugs introduced by tuning
obua
parents:
22964
diff
changeset
|
63 |
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
|
64 |
|
23665
825bea0266db
adopted to new computing oracle and fixed bugs introduced by tuning
obua
parents:
22964
diff
changeset
|
65 |
end |
825bea0266db
adopted to new computing oracle and fixed bugs introduced by tuning
obua
parents:
22964
diff
changeset
|
66 |
|
20787
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
67 |
fun matrix_simplify th = |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
68 |
let |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
69 |
val simp_th = matrix_compute (cprop_of th) |
36945 | 70 |
val th = Thm.strip_shyps (Thm.equal_elim simp_th th) |
40298
2bdb14323fbf
eliminated fragile catch-all pattern, based on educated guess about the intended exception;
wenzelm
parents:
37788
diff
changeset
|
71 |
fun removeTrue th = removeTrue (Thm.implies_elim th TrueI) handle THM _ => th |
20787
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
72 |
in |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
73 |
removeTrue th |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
74 |
end |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
75 |
|
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
76 |
fun prove_bound lptfile prec = |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
77 |
let |
28637 | 78 |
val th = lp_dual_estimate_prt lptfile prec |
20787
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
79 |
in |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
80 |
matrix_simplify th |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
81 |
end |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
82 |
|
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
83 |
val realFromStr = the o Real.fromString; |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
84 |
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
|
85 |
|
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
86 |
end |