1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Matrix_LP/Cplex.thy	Sat Mar 17 12:52:40 2012 +0100
     1.3 @@ -0,0 +1,67 @@
     1.4 +(*  Title:      HOL/Matrix/Cplex.thy
     1.5 +    Author:     Steven Obua
     1.6 +*)
     1.7 +
     1.8 +theory Cplex 
     1.9 +imports SparseMatrix LP ComputeFloat ComputeNumeral
    1.10 +uses "Cplex_tools.ML" "CplexMatrixConverter.ML" "FloatSparseMatrixBuilder.ML"
    1.11 +  "fspmlp.ML" ("matrixlp.ML")
    1.12 +begin
    1.13 +
    1.14 +lemma spm_mult_le_dual_prts: 
    1.15 +  assumes
    1.16 +  "sorted_sparse_matrix A1"
    1.17 +  "sorted_sparse_matrix A2"
    1.18 +  "sorted_sparse_matrix c1"
    1.19 +  "sorted_sparse_matrix c2"
    1.20 +  "sorted_sparse_matrix y"
    1.21 +  "sorted_sparse_matrix r1"
    1.22 +  "sorted_sparse_matrix r2"
    1.23 +  "sorted_spvec b"
    1.24 +  "le_spmat [] y"
    1.25 +  "sparse_row_matrix A1 \<le> A"
    1.26 +  "A \<le> sparse_row_matrix A2"
    1.27 +  "sparse_row_matrix c1 \<le> c"
    1.28 +  "c \<le> sparse_row_matrix c2"
    1.29 +  "sparse_row_matrix r1 \<le> x"
    1.30 +  "x \<le> sparse_row_matrix r2"
    1.31 +  "A * x \<le> sparse_row_matrix (b::('a::lattice_ring) spmat)"
    1.32 +  shows
    1.33 +  "c * x \<le> sparse_row_matrix (add_spmat (mult_spmat y b)
    1.34 +  (let s1 = diff_spmat c1 (mult_spmat y A2); s2 = diff_spmat c2 (mult_spmat y A1) in 
    1.35 +  add_spmat (mult_spmat (pprt_spmat s2) (pprt_spmat r2)) (add_spmat (mult_spmat (pprt_spmat s1) (nprt_spmat r2)) 
    1.36 +  (add_spmat (mult_spmat (nprt_spmat s2) (pprt_spmat r1)) (mult_spmat (nprt_spmat s1) (nprt_spmat r1))))))"
    1.37 +  apply (simp add: Let_def)
    1.38 +  apply (insert assms)
    1.39 +  apply (simp add: sparse_row_matrix_op_simps algebra_simps)  
    1.40 +  apply (rule mult_le_dual_prts[where A=A, simplified Let_def algebra_simps])
    1.41 +  apply (auto)
    1.42 +  done
    1.43 +
    1.44 +lemma spm_mult_le_dual_prts_no_let: 
    1.45 +  assumes
    1.46 +  "sorted_sparse_matrix A1"
    1.47 +  "sorted_sparse_matrix A2"
    1.48 +  "sorted_sparse_matrix c1"
    1.49 +  "sorted_sparse_matrix c2"
    1.50 +  "sorted_sparse_matrix y"
    1.51 +  "sorted_sparse_matrix r1"
    1.52 +  "sorted_sparse_matrix r2"
    1.53 +  "sorted_spvec b"
    1.54 +  "le_spmat [] y"
    1.55 +  "sparse_row_matrix A1 \<le> A"
    1.56 +  "A \<le> sparse_row_matrix A2"
    1.57 +  "sparse_row_matrix c1 \<le> c"
    1.58 +  "c \<le> sparse_row_matrix c2"
    1.59 +  "sparse_row_matrix r1 \<le> x"
    1.60 +  "x \<le> sparse_row_matrix r2"
    1.61 +  "A * x \<le> sparse_row_matrix (b::('a::lattice_ring) spmat)"
    1.62 +  shows
    1.63 +  "c * x \<le> sparse_row_matrix (add_spmat (mult_spmat y b)
    1.64 +  (mult_est_spmat r1 r2 (diff_spmat c1 (mult_spmat y A2)) (diff_spmat c2 (mult_spmat y A1))))"
    1.65 +  by (simp add: assms mult_est_spmat_def spm_mult_le_dual_prts[where A=A, simplified Let_def])
    1.66 +
    1.67 +use "matrixlp.ML"
    1.68 +
    1.69 +end
    1.70 +