|
(* Title: HOL/Matrix_LP/Cplex.thy
Author: Steven Obua
*)
theory Cplex
imports SparseMatrix LP ComputeFloat ComputeNumeral
begin
ML_file \<open>Cplex_tools.ML\<close>
ML_file \<open>CplexMatrixConverter.ML\<close>
ML_file \<open>FloatSparseMatrixBuilder.ML\<close>
ML_file \<open>fspmlp.ML\<close>
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 \ A"
"A \ sparse_row_matrix A2"
"sparse_row_matrix c1 \ c"
"c \ sparse_row_matrix c2"
"sparse_row_matrix r1 \ x"
"x \ sparse_row_matrix r2"
"A * x \ sparse_row_matrix (b::('a::lattice_ring) spmat)"
shows
"c * x \ 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 assms)
apply (simp add: sparse_row_matrix_op_simps algebra_simps)
apply (rule mult_le_dual_prts[where A=A, simplified Let_def algebra_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 \ A"
"A \ sparse_row_matrix A2"
"sparse_row_matrix c1 \ c"
"c \ sparse_row_matrix c2"
"sparse_row_matrix r1 \ x"
"x \ sparse_row_matrix r2"
"A * x \ sparse_row_matrix (b::('a::lattice_ring) spmat)"
shows
"c * x \ 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])
ML_file \<open>matrixlp.ML\<close>
end
¤ Dauer der Verarbeitung: 0.0 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
