author | wenzelm |
Sun, 13 Mar 2011 22:55:50 +0100 | |
changeset 41959 | b460124855b8 |
parent 37764 | 3489daf839d5 |
child 46543 | c7c289ce9ad2 |
permissions | -rw-r--r-- |
41959 | 1 |
(* Title: HOL/Matrix/Cplex.thy |
16784 | 2 |
Author: Steven Obua |
3 |
*) |
|
4 |
||
5 |
theory Cplex |
|
32491
d5d8bea0cd94
reorganized Compute theories for HOL-Matrix -- avoiding theory files within main HOL/Tools;
wenzelm
parents:
31816
diff
changeset
|
6 |
imports SparseMatrix LP ComputeFloat ComputeNumeral |
28637 | 7 |
uses "Cplex_tools.ML" "CplexMatrixConverter.ML" "FloatSparseMatrixBuilder.ML" |
8 |
"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" |
|
31816 | 21 |
"le_spmat [] y" |
27484 | 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" |
|
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
32491
diff
changeset
|
28 |
"A * x \<le> sparse_row_matrix (b::('a::lattice_ring) spmat)" |
27484 | 29 |
shows |
31816 | 30 |
"c * x \<le> sparse_row_matrix (add_spmat (mult_spmat y b) |
27484 | 31 |
(let s1 = diff_spmat c1 (mult_spmat y A2); s2 = diff_spmat c2 (mult_spmat y A1) in |
31816 | 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))))))" |
|
27484 | 34 |
apply (simp add: Let_def) |
28637 | 35 |
apply (insert assms) |
29667 | 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]) |
|
27484 | 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" |
|
31816 | 51 |
"le_spmat [] y" |
27484 | 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" |
|
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
32491
diff
changeset
|
58 |
"A * x \<le> sparse_row_matrix (b::('a::lattice_ring) spmat)" |
27484 | 59 |
shows |
31816 | 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))))" |
|
28637 | 62 |
by (simp add: assms 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 |