|
15178
|
1 |
open BasisLibrary;
|
|
|
2 |
|
|
|
3 |
use "Cplex.ML";
|
|
|
4 |
use "CplexMatrixConverter.ML";
|
|
|
5 |
use "ExactFloatingPoint.ML";
|
|
|
6 |
use "FloatArith.ML";
|
|
|
7 |
use "FloatSparseMatrixBuilder.ML";
|
|
|
8 |
use "fspmlp.ML";
|
|
|
9 |
use "codegen_prep.ML";
|
|
|
10 |
use "eq_codegen.ML";
|
|
|
11 |
use "conv.ML";
|
|
|
12 |
|
|
|
13 |
|
|
|
14 |
val th = theory "MatrixLP"
|
|
|
15 |
val sg = sign_of th
|
|
|
16 |
|
|
|
17 |
fun prep x = standard (mk_meta_eq x)
|
|
|
18 |
|
|
|
19 |
fun inst_real thm = standard (Thm.instantiate ([(fst (hd (term_tvars (prop_of thm))),
|
|
|
20 |
ctyp_of sg HOLogic.realT)], []) thm);
|
|
|
21 |
|
|
|
22 |
val spm_lp_dual_estimate_simp =
|
|
|
23 |
(thms "Float.arith_no_let") @
|
|
|
24 |
(map inst_real (thms "SparseMatrix.sparse_row_matrix_arith_simps")) @
|
|
|
25 |
(thms "SparseMatrix.sorted_sp_simps") @
|
|
|
26 |
[thm "Product_Type.fst_conv", thm "Product_Type.snd_conv"] @
|
|
|
27 |
(thms "SparseMatrix.boolarith")
|
|
|
28 |
|
|
|
29 |
val simp_with = Simplifier.simplify (HOL_basic_ss addsimps [thm "SparseMatrix.if_case_eq", thm "Float.norm_0_1"])
|
|
|
30 |
|
|
|
31 |
val spm_lp_dual_estimate_simp = map simp_with spm_lp_dual_estimate_simp
|
|
|
32 |
|
|
|
33 |
val geninput = codegen_prep.prepare_thms spm_lp_dual_estimate_simp
|
|
|
34 |
|
|
|
35 |
val _ = SimprocsCodegen.use_simprocs_code sg geninput
|