--- a/src/HOL/Matrix/cplex/Cplex.thy Fri Jun 26 20:54:15 2009 +0200
+++ b/src/HOL/Matrix/cplex/Cplex.thy Sat Jun 27 09:43:41 2009 +0200
@@ -19,7 +19,7 @@
"sorted_sparse_matrix r1"
"sorted_sparse_matrix r2"
"sorted_spvec b"
- "le_spmat ([], y)"
+ "le_spmat [] y"
"sparse_row_matrix A1 \<le> A"
"A \<le> sparse_row_matrix A2"
"sparse_row_matrix c1 \<le> c"
@@ -28,10 +28,10 @@
"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,
+ "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)))))))"
+ 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 assms)
apply (simp add: sparse_row_matrix_op_simps algebra_simps)
@@ -49,7 +49,7 @@
"sorted_sparse_matrix r1"
"sorted_sparse_matrix r2"
"sorted_spvec b"
- "le_spmat ([], y)"
+ "le_spmat [] y"
"sparse_row_matrix A1 \<le> A"
"A \<le> sparse_row_matrix A2"
"sparse_row_matrix c1 \<le> c"
@@ -58,8 +58,8 @@
"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))))"
+ "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: assms mult_est_spmat_def spm_mult_le_dual_prts[where A=A, simplified Let_def])
use "matrixlp.ML"