src/HOL/Matrix/Cplex.thy
author wenzelm
Fri Dec 17 17:43:54 2010 +0100 (2010-12-17)
changeset 41229 d797baa3d57c
parent 37764 3489daf839d5
child 41959 b460124855b8
permissions -rw-r--r--
replaced command 'nonterminals' by slightly modernized version 'nonterminal';
     1 (*  Title:      HOL/Matrix/cplex/Cplex.thy
     2     Author:     Steven Obua
     3 *)
     4 
     5 theory Cplex 
     6 imports SparseMatrix LP ComputeFloat ComputeNumeral
     7 uses "Cplex_tools.ML" "CplexMatrixConverter.ML" "FloatSparseMatrixBuilder.ML"
     8   "fspmlp.ML" ("matrixlp.ML")
     9 begin
    10 
    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"
    21   "le_spmat [] y"
    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"
    28   "A * x \<le> sparse_row_matrix (b::('a::lattice_ring) spmat)"
    29   shows
    30   "c * x \<le> sparse_row_matrix (add_spmat (mult_spmat y b)
    31   (let s1 = diff_spmat c1 (mult_spmat y A2); s2 = diff_spmat c2 (mult_spmat y A1) in 
    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))))))"
    34   apply (simp add: Let_def)
    35   apply (insert assms)
    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])
    38   apply (auto)
    39   done
    40 
    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"
    51   "le_spmat [] y"
    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"
    58   "A * x \<le> sparse_row_matrix (b::('a::lattice_ring) spmat)"
    59   shows
    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))))"
    62   by (simp add: assms mult_est_spmat_def spm_mult_le_dual_prts[where A=A, simplified Let_def])
    63 
    64 use "matrixlp.ML"
    65 
    66 end