--- a/src/HOL/Matrix/cplex/Cplex.thy Thu Jul 03 20:53:44 2008 +0200
+++ b/src/HOL/Matrix/cplex/Cplex.thy Fri Jul 04 07:39:01 2008 +0200
@@ -4,11 +4,63 @@
*)
theory Cplex
-imports FloatSparseMatrix "~~/src/HOL/Tools/ComputeNumeral"
-uses "Cplex_tools.ML" "CplexMatrixConverter.ML" "FloatSparseMatrixBuilder.ML" "fspmlp.ML"
+imports SparseMatrix LP "~~/src/HOL/Real/Float" "~~/src/HOL/Tools/ComputeNumeral"
+uses "Cplex_tools.ML" "CplexMatrixConverter.ML" "FloatSparseMatrixBuilder.ML" "fspmlp.ML" ("matrixlp.ML")
begin
-end
+lemma spm_mult_le_dual_prts:
+ assumes
+ "sorted_sparse_matrix A1"
+ "sorted_sparse_matrix A2"
+ "sorted_sparse_matrix c1"
+ "sorted_sparse_matrix c2"
+ "sorted_sparse_matrix y"
+ "sorted_sparse_matrix r1"
+ "sorted_sparse_matrix r2"
+ "sorted_spvec b"
+ "le_spmat ([], y)"
+ "sparse_row_matrix A1 \<le> A"
+ "A \<le> sparse_row_matrix A2"
+ "sparse_row_matrix c1 \<le> c"
+ "c \<le> sparse_row_matrix c2"
+ "sparse_row_matrix r1 \<le> x"
+ "x \<le> sparse_row_matrix r2"
+ "A * x \<le> sparse_row_matrix (b::('a::lordered_ring) spmat)"
+ shows
+ "c * x \<le> sparse_row_matrix (add_spmat (mult_spmat y b,
+ (let s1 = diff_spmat c1 (mult_spmat y A2); s2 = diff_spmat c2 (mult_spmat y A1) in
+ add_spmat (mult_spmat (pprt_spmat s2) (pprt_spmat r2), add_spmat (mult_spmat (pprt_spmat s1) (nprt_spmat r2),
+ add_spmat (mult_spmat (nprt_spmat s2) (pprt_spmat r1), mult_spmat (nprt_spmat s1) (nprt_spmat r1)))))))"
+ apply (simp add: Let_def)
+ apply (insert prems)
+ apply (simp add: sparse_row_matrix_op_simps ring_simps)
+ apply (rule mult_le_dual_prts[where A=A, simplified Let_def ring_simps])
+ apply (auto)
+ done
+lemma spm_mult_le_dual_prts_no_let:
+ assumes
+ "sorted_sparse_matrix A1"
+ "sorted_sparse_matrix A2"
+ "sorted_sparse_matrix c1"
+ "sorted_sparse_matrix c2"
+ "sorted_sparse_matrix y"
+ "sorted_sparse_matrix r1"
+ "sorted_sparse_matrix r2"
+ "sorted_spvec b"
+ "le_spmat ([], y)"
+ "sparse_row_matrix A1 \<le> A"
+ "A \<le> sparse_row_matrix A2"
+ "sparse_row_matrix c1 \<le> c"
+ "c \<le> sparse_row_matrix c2"
+ "sparse_row_matrix r1 \<le> x"
+ "x \<le> sparse_row_matrix r2"
+ "A * x \<le> sparse_row_matrix (b::('a::lordered_ring) spmat)"
+ shows
+ "c * x \<le> sparse_row_matrix (add_spmat (mult_spmat y b,
+ mult_est_spmat r1 r2 (diff_spmat c1 (mult_spmat y A2)) (diff_spmat c2 (mult_spmat y A1))))"
+ by (simp add: prems mult_est_spmat_def spm_mult_le_dual_prts[where A=A, simplified Let_def])
+use "matrixlp.ML"
+end