15178
|
1 |
use "MatrixLP_gensimp.ML";
|
|
2 |
|
|
3 |
signature MATRIX_LP =
|
|
4 |
sig
|
|
5 |
val lp_dual_estimate : string -> int -> thm
|
|
6 |
val simplify : thm -> thm
|
|
7 |
end
|
|
8 |
|
|
9 |
structure MatrixLP : MATRIX_LP =
|
|
10 |
struct
|
|
11 |
|
|
12 |
val _ = SimprocsCodegen.use_simprocs_code sg geninput
|
|
13 |
|
|
14 |
val simp_le_spmat = simp_SparseMatrix_le_spmat_'_mult__'List_list_'_mult__'nat'_'List_list_'_mult__'nat'_'RealDef_real'''''_'List_list_'_mult__'nat'_'List_list_'_mult__'nat'_'RealDef_real'''''_bool'
|
|
15 |
val simp_add_spmat = simp_SparseMatrix_add_spmat_'_mult__'List_list_'_mult__'nat'_'List_list_'_mult__'nat'_'RealDef_real'''''_'List_list_'_mult__'nat'_'List_list_'_mult__'nat'_'RealDef_real'''''_List_list_'_mult__'nat'_'List_list_'_mult__'nat'_'RealDef_real'''''
|
|
16 |
val simp_diff_spmat = simp_SparseMatrix_diff_spmat_'List_list_'_mult__'nat'_'List_list_'_mult__'nat'_'RealDef_real''''_List_list_'_mult__'nat'_'List_list_'_mult__'nat'_'RealDef_real''''_List_list_'_mult__'nat'_'List_list_'_mult__'nat'_'RealDef_real'''''
|
|
17 |
val simp_abs_spmat = simp_SparseMatrix_abs_spmat_'List_list_'_mult__'nat'_'List_list_'_mult__'nat'_'RealDef_real''''_List_list_'_mult__'nat'_'List_list_'_mult__'nat'_'RealDef_real'''''
|
|
18 |
val simp_mult_spmat = simp_SparseMatrix_mult_spmat_'List_list_'_mult__'nat'_'List_list_'_mult__'nat'_'RealDef_real''''_List_list_'_mult__'nat'_'List_list_'_mult__'nat'_'RealDef_real''''_List_list_'_mult__'nat'_'List_list_'_mult__'nat'_'RealDef_real'''''
|
|
19 |
val simp_sorted_sparse_matrix = simp_SparseMatrix_sorted_sparse_matrix
|
|
20 |
val simp_sorted_spvec = simp_SparseMatrix_sorted_spvec
|
|
21 |
|
|
22 |
fun single_arg simp ct = snd (simp (snd (Thm.dest_comb ct)))
|
|
23 |
|
|
24 |
fun double_arg simp ct =
|
|
25 |
let
|
|
26 |
val (a, y) = Thm.dest_comb ct
|
|
27 |
val (_, x) = Thm.dest_comb a
|
|
28 |
in
|
|
29 |
snd (simp x y)
|
|
30 |
end
|
|
31 |
|
|
32 |
fun spmc ct =
|
|
33 |
(case term_of ct of
|
|
34 |
((Const ("SparseMatrix.le_spmat", _)) $ _) =>
|
|
35 |
single_arg simp_le_spmat ct
|
|
36 |
| ((Const ("SparseMatrix.add_spmat", _)) $ _) =>
|
|
37 |
single_arg simp_add_spmat ct
|
|
38 |
| ((Const ("SparseMatrix.diff_spmat", _)) $ _ $ _) =>
|
|
39 |
double_arg simp_diff_spmat ct
|
|
40 |
| ((Const ("SparseMatrix.abs_spmat", _)) $ _) =>
|
|
41 |
single_arg simp_abs_spmat ct
|
|
42 |
| ((Const ("SparseMatrix.mult_spmat", _)) $ _ $ _) =>
|
|
43 |
double_arg simp_mult_spmat ct
|
|
44 |
| ((Const ("SparseMatrix.sorted_sparse_matrix", _)) $ _) =>
|
|
45 |
single_arg simp_sorted_sparse_matrix ct
|
|
46 |
| ((Const ("SparseMatrix.sorted_spvec", ty)) $ _) =>
|
|
47 |
single_arg simp_sorted_spvec ct
|
|
48 |
| _ => raise Fail_conv)
|
|
49 |
|
|
50 |
fun lp_dual_estimate lptfile prec =
|
|
51 |
let
|
|
52 |
val th = inst_real (thm "SparseMatrix.spm_linprog_dual_estimate_1")
|
|
53 |
val sg = sign_of (theory "MatrixLP")
|
|
54 |
val (y, (A1, A2), (c1, c2), b, r) =
|
|
55 |
let
|
|
56 |
open fspmlp
|
|
57 |
val l = load lptfile prec false
|
|
58 |
in
|
|
59 |
(y l, A l, c l, b l, r l)
|
|
60 |
end
|
|
61 |
fun var s x = (cterm_of sg (Var ((s,0), FloatSparseMatrixBuilder.real_spmatT)), x)
|
|
62 |
val th = Thm.instantiate ([], [var "A1" A1, var "A2" A2, var "y" y, var "c1" c1, var "c2" c2, var "r" r, var "b" b]) th
|
|
63 |
in
|
|
64 |
th
|
|
65 |
end
|
|
66 |
|
|
67 |
fun simplify th =
|
|
68 |
let
|
|
69 |
val simp_th = botc spmc (cprop_of th)
|
|
70 |
val th = strip_shyps (equal_elim simp_th th)
|
|
71 |
fun removeTrue th = removeTrue (implies_elim th TrueI) handle _ => th
|
|
72 |
in
|
|
73 |
removeTrue th
|
|
74 |
end
|
|
75 |
|
15180
|
76 |
end
|
15178
|
77 |
|
15180
|
78 |
fun float2real (x,y) = (Real.fromInt x) * (Math.pow (2.0, Real.fromInt y))
|
15178
|
79 |
|
|
80 |
val result = ref ([]:thm list)
|
|
81 |
|
|
82 |
fun run c = timeit (fn () => (result := [MatrixLP.simplify c]; ()))
|
|
83 |
|