| author | hoelzl |
| Thu, 05 Feb 2009 11:45:15 +0100 | |
| changeset 29804 | e15b74577368 |
| parent 29667 | 53103fc8ffa3 |
| child 31816 | ffaf6dd53045 |
| permissions | -rw-r--r-- |
| 16784 | 1 |
(* Title: HOL/Matrix/cplex/Cplex.thy |
2 |
ID: $Id$ |
|
3 |
Author: Steven Obua |
|
4 |
*) |
|
5 |
||
6 |
theory Cplex |
|
|
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
7 |
imports SparseMatrix LP "~~/src/HOL/Tools/ComputeFloat" "~~/src/HOL/Tools/ComputeNumeral" |
| 28637 | 8 |
uses "Cplex_tools.ML" "CplexMatrixConverter.ML" "FloatSparseMatrixBuilder.ML" |
9 |
"fspmlp.ML" ("matrixlp.ML")
|
|
| 16784 | 10 |
begin |
11 |
||
| 27484 | 12 |
lemma spm_mult_le_dual_prts: |
13 |
assumes |
|
14 |
"sorted_sparse_matrix A1" |
|
15 |
"sorted_sparse_matrix A2" |
|
16 |
"sorted_sparse_matrix c1" |
|
17 |
"sorted_sparse_matrix c2" |
|
18 |
"sorted_sparse_matrix y" |
|
19 |
"sorted_sparse_matrix r1" |
|
20 |
"sorted_sparse_matrix r2" |
|
21 |
"sorted_spvec b" |
|
22 |
"le_spmat ([], y)" |
|
23 |
"sparse_row_matrix A1 \<le> A" |
|
24 |
"A \<le> sparse_row_matrix A2" |
|
25 |
"sparse_row_matrix c1 \<le> c" |
|
26 |
"c \<le> sparse_row_matrix c2" |
|
27 |
"sparse_row_matrix r1 \<le> x" |
|
28 |
"x \<le> sparse_row_matrix r2" |
|
29 |
"A * x \<le> sparse_row_matrix (b::('a::lordered_ring) spmat)"
|
|
30 |
shows |
|
31 |
"c * x \<le> sparse_row_matrix (add_spmat (mult_spmat y b, |
|
32 |
(let s1 = diff_spmat c1 (mult_spmat y A2); s2 = diff_spmat c2 (mult_spmat y A1) in |
|
33 |
add_spmat (mult_spmat (pprt_spmat s2) (pprt_spmat r2), add_spmat (mult_spmat (pprt_spmat s1) (nprt_spmat r2), |
|
34 |
add_spmat (mult_spmat (nprt_spmat s2) (pprt_spmat r1), mult_spmat (nprt_spmat s1) (nprt_spmat r1)))))))" |
|
35 |
apply (simp add: Let_def) |
|
| 28637 | 36 |
apply (insert assms) |
| 29667 | 37 |
apply (simp add: sparse_row_matrix_op_simps algebra_simps) |
38 |
apply (rule mult_le_dual_prts[where A=A, simplified Let_def algebra_simps]) |
|
| 27484 | 39 |
apply (auto) |
40 |
done |
|
| 16784 | 41 |
|
| 27484 | 42 |
lemma spm_mult_le_dual_prts_no_let: |
43 |
assumes |
|
44 |
"sorted_sparse_matrix A1" |
|
45 |
"sorted_sparse_matrix A2" |
|
46 |
"sorted_sparse_matrix c1" |
|
47 |
"sorted_sparse_matrix c2" |
|
48 |
"sorted_sparse_matrix y" |
|
49 |
"sorted_sparse_matrix r1" |
|
50 |
"sorted_sparse_matrix r2" |
|
51 |
"sorted_spvec b" |
|
52 |
"le_spmat ([], y)" |
|
53 |
"sparse_row_matrix A1 \<le> A" |
|
54 |
"A \<le> sparse_row_matrix A2" |
|
55 |
"sparse_row_matrix c1 \<le> c" |
|
56 |
"c \<le> sparse_row_matrix c2" |
|
57 |
"sparse_row_matrix r1 \<le> x" |
|
58 |
"x \<le> sparse_row_matrix r2" |
|
59 |
"A * x \<le> sparse_row_matrix (b::('a::lordered_ring) spmat)"
|
|
60 |
shows |
|
61 |
"c * x \<le> sparse_row_matrix (add_spmat (mult_spmat y b, |
|
62 |
mult_est_spmat r1 r2 (diff_spmat c1 (mult_spmat y A2)) (diff_spmat c2 (mult_spmat y A1))))" |
|
| 28637 | 63 |
by (simp add: assms mult_est_spmat_def spm_mult_le_dual_prts[where A=A, simplified Let_def]) |
| 16784 | 64 |
|
| 27484 | 65 |
use "matrixlp.ML" |
| 16784 | 66 |
|
| 27484 | 67 |
end |