15 "ComputeHOL.compute_if" "ComputeFloat.arith" "SparseMatrix.sparse_row_matrix_arith_simps" |
15 "ComputeHOL.compute_if" "ComputeFloat.arith" "SparseMatrix.sparse_row_matrix_arith_simps" |
16 "ComputeHOL.compute_bool" "ComputeHOL.compute_pair" |
16 "ComputeHOL.compute_bool" "ComputeHOL.compute_pair" |
17 "SparseMatrix.sorted_sp_simps" |
17 "SparseMatrix.sorted_sp_simps" |
18 "ComputeNumeral.natnorm"}; (*"ComputeNumeral.number_norm"*) |
18 "ComputeNumeral.natnorm"}; (*"ComputeNumeral.number_norm"*) |
19 |
19 |
20 val spm_mult_le_dual_prts_no_let_real = @{thm "spm_mult_le_dual_prts_no_let" [where ?'a = real]} |
|
21 |
|
22 fun lp_dual_estimate_prt lptfile prec = |
|
23 let |
|
24 val cert = cterm_of @{theory} |
|
25 fun var s x = (cert (Var ((s, 0), FloatSparseMatrixBuilder.spmatT)), x) |
|
26 val l = Fspmlp.load lptfile prec false |
|
27 val (y, (A1, A2), (c1, c2), b, (r1, r2)) = |
|
28 let |
|
29 open Fspmlp |
|
30 in |
|
31 (y l |> cert, A l |> pairself cert, c l |> pairself cert, b l |> cert, r12 l |> pairself cert) |
|
32 end |
|
33 in |
|
34 Thm.instantiate ([], |
|
35 [var "A1" A1, var "A2" A2, var "y" y, var "c1" c1, var "c2" c2, var "r1" r1, var "r2" r2, var "b" b]) |
|
36 spm_mult_le_dual_prts_no_let_real |
|
37 end |
|
38 |
|
39 val computer = PCompute.make Compute.SML @{theory} compute_thms [] |
20 val computer = PCompute.make Compute.SML @{theory} compute_thms [] |
40 |
21 |
41 fun matrix_compute c = hd (PCompute.rewrite computer [c]) |
22 fun matrix_compute c = hd (PCompute.rewrite computer [c]) |
42 |
23 |
43 fun matrix_simplify th = |
24 fun matrix_simplify th = |