1 (* Title: HOL/Matrix/cplex/Cplex.thy |
|
2 Author: Steven Obua |
|
3 *) |
|
4 |
|
5 theory Cplex |
|
6 imports SparseMatrix LP ComputeFloat ComputeNumeral |
|
7 uses "Cplex_tools.ML" "CplexMatrixConverter.ML" "FloatSparseMatrixBuilder.ML" |
|
8 "fspmlp.ML" ("matrixlp.ML") |
|
9 begin |
|
10 |
|
11 lemma spm_mult_le_dual_prts: |
|
12 assumes |
|
13 "sorted_sparse_matrix A1" |
|
14 "sorted_sparse_matrix A2" |
|
15 "sorted_sparse_matrix c1" |
|
16 "sorted_sparse_matrix c2" |
|
17 "sorted_sparse_matrix y" |
|
18 "sorted_sparse_matrix r1" |
|
19 "sorted_sparse_matrix r2" |
|
20 "sorted_spvec b" |
|
21 "le_spmat [] y" |
|
22 "sparse_row_matrix A1 \<le> A" |
|
23 "A \<le> sparse_row_matrix A2" |
|
24 "sparse_row_matrix c1 \<le> c" |
|
25 "c \<le> sparse_row_matrix c2" |
|
26 "sparse_row_matrix r1 \<le> x" |
|
27 "x \<le> sparse_row_matrix r2" |
|
28 "A * x \<le> sparse_row_matrix (b::('a::lattice_ring) spmat)" |
|
29 shows |
|
30 "c * x \<le> sparse_row_matrix (add_spmat (mult_spmat y b) |
|
31 (let s1 = diff_spmat c1 (mult_spmat y A2); s2 = diff_spmat c2 (mult_spmat y A1) in |
|
32 add_spmat (mult_spmat (pprt_spmat s2) (pprt_spmat r2)) (add_spmat (mult_spmat (pprt_spmat s1) (nprt_spmat r2)) |
|
33 (add_spmat (mult_spmat (nprt_spmat s2) (pprt_spmat r1)) (mult_spmat (nprt_spmat s1) (nprt_spmat r1))))))" |
|
34 apply (simp add: Let_def) |
|
35 apply (insert assms) |
|
36 apply (simp add: sparse_row_matrix_op_simps algebra_simps) |
|
37 apply (rule mult_le_dual_prts[where A=A, simplified Let_def algebra_simps]) |
|
38 apply (auto) |
|
39 done |
|
40 |
|
41 lemma spm_mult_le_dual_prts_no_let: |
|
42 assumes |
|
43 "sorted_sparse_matrix A1" |
|
44 "sorted_sparse_matrix A2" |
|
45 "sorted_sparse_matrix c1" |
|
46 "sorted_sparse_matrix c2" |
|
47 "sorted_sparse_matrix y" |
|
48 "sorted_sparse_matrix r1" |
|
49 "sorted_sparse_matrix r2" |
|
50 "sorted_spvec b" |
|
51 "le_spmat [] y" |
|
52 "sparse_row_matrix A1 \<le> A" |
|
53 "A \<le> sparse_row_matrix A2" |
|
54 "sparse_row_matrix c1 \<le> c" |
|
55 "c \<le> sparse_row_matrix c2" |
|
56 "sparse_row_matrix r1 \<le> x" |
|
57 "x \<le> sparse_row_matrix r2" |
|
58 "A * x \<le> sparse_row_matrix (b::('a::lattice_ring) spmat)" |
|
59 shows |
|
60 "c * x \<le> sparse_row_matrix (add_spmat (mult_spmat y b) |
|
61 (mult_est_spmat r1 r2 (diff_spmat c1 (mult_spmat y A2)) (diff_spmat c2 (mult_spmat y A1))))" |
|
62 by (simp add: assms mult_est_spmat_def spm_mult_le_dual_prts[where A=A, simplified Let_def]) |
|
63 |
|
64 use "matrixlp.ML" |
|
65 |
|
66 end |
|