|
16784
|
1 |
(* Title: HOL/Matrix/cplex/Cplex.thy
|
|
|
2 |
ID: $Id$
|
|
|
3 |
Author: Steven Obua
|
|
|
4 |
*)
|
|
|
5 |
|
|
|
6 |
theory Cplex
|
|
27484
|
7 |
imports SparseMatrix LP "~~/src/HOL/Real/Float" "~~/src/HOL/Tools/ComputeNumeral"
|
|
|
8 |
uses "Cplex_tools.ML" "CplexMatrixConverter.ML" "FloatSparseMatrixBuilder.ML" "fspmlp.ML" ("matrixlp.ML")
|
|
16784
|
9 |
begin
|
|
|
10 |
|
|
27484
|
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::lordered_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 prems)
|
|
|
36 |
apply (simp add: sparse_row_matrix_op_simps ring_simps)
|
|
|
37 |
apply (rule mult_le_dual_prts[where A=A, simplified Let_def ring_simps])
|
|
|
38 |
apply (auto)
|
|
|
39 |
done
|
|
16784
|
40 |
|
|
27484
|
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::lordered_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: prems mult_est_spmat_def spm_mult_le_dual_prts[where A=A, simplified Let_def])
|
|
16784
|
63 |
|
|
27484
|
64 |
use "matrixlp.ML"
|
|
16784
|
65 |
|
|
27484
|
66 |
end
|