src/HOL/Matrix_LP/Cplex.thy
author blanchet
Wed Feb 12 08:35:57 2014 +0100 (2014-02-12)
changeset 55415 05f5fdb8d093
parent 48891 c0eafbd55de3
child 69605 a96320074298
permissions -rw-r--r--
renamed 'nat_{case,rec}' to '{case,rec}_nat'
     1 (*  Title:      HOL/Matrix_LP/Cplex.thy
     2     Author:     Steven Obua
     3 *)
     4 
     5 theory Cplex 
     6 imports SparseMatrix LP ComputeFloat ComputeNumeral
     7 begin
     8 
     9 ML_file "Cplex_tools.ML"
    10 ML_file "CplexMatrixConverter.ML"
    11 ML_file "FloatSparseMatrixBuilder.ML"
    12 ML_file "fspmlp.ML"
    13 
    14 lemma spm_mult_le_dual_prts: 
    15   assumes
    16   "sorted_sparse_matrix A1"
    17   "sorted_sparse_matrix A2"
    18   "sorted_sparse_matrix c1"
    19   "sorted_sparse_matrix c2"
    20   "sorted_sparse_matrix y"
    21   "sorted_sparse_matrix r1"
    22   "sorted_sparse_matrix r2"
    23   "sorted_spvec b"
    24   "le_spmat [] y"
    25   "sparse_row_matrix A1 \<le> A"
    26   "A \<le> sparse_row_matrix A2"
    27   "sparse_row_matrix c1 \<le> c"
    28   "c \<le> sparse_row_matrix c2"
    29   "sparse_row_matrix r1 \<le> x"
    30   "x \<le> sparse_row_matrix r2"
    31   "A * x \<le> sparse_row_matrix (b::('a::lattice_ring) spmat)"
    32   shows
    33   "c * x \<le> sparse_row_matrix (add_spmat (mult_spmat y b)
    34   (let s1 = diff_spmat c1 (mult_spmat y A2); s2 = diff_spmat c2 (mult_spmat y A1) in 
    35   add_spmat (mult_spmat (pprt_spmat s2) (pprt_spmat r2)) (add_spmat (mult_spmat (pprt_spmat s1) (nprt_spmat r2)) 
    36   (add_spmat (mult_spmat (nprt_spmat s2) (pprt_spmat r1)) (mult_spmat (nprt_spmat s1) (nprt_spmat r1))))))"
    37   apply (simp add: Let_def)
    38   apply (insert assms)
    39   apply (simp add: sparse_row_matrix_op_simps algebra_simps)  
    40   apply (rule mult_le_dual_prts[where A=A, simplified Let_def algebra_simps])
    41   apply (auto)
    42   done
    43 
    44 lemma spm_mult_le_dual_prts_no_let: 
    45   assumes
    46   "sorted_sparse_matrix A1"
    47   "sorted_sparse_matrix A2"
    48   "sorted_sparse_matrix c1"
    49   "sorted_sparse_matrix c2"
    50   "sorted_sparse_matrix y"
    51   "sorted_sparse_matrix r1"
    52   "sorted_sparse_matrix r2"
    53   "sorted_spvec b"
    54   "le_spmat [] y"
    55   "sparse_row_matrix A1 \<le> A"
    56   "A \<le> sparse_row_matrix A2"
    57   "sparse_row_matrix c1 \<le> c"
    58   "c \<le> sparse_row_matrix c2"
    59   "sparse_row_matrix r1 \<le> x"
    60   "x \<le> sparse_row_matrix r2"
    61   "A * x \<le> sparse_row_matrix (b::('a::lattice_ring) spmat)"
    62   shows
    63   "c * x \<le> sparse_row_matrix (add_spmat (mult_spmat y b)
    64   (mult_est_spmat r1 r2 (diff_spmat c1 (mult_spmat y A2)) (diff_spmat c2 (mult_spmat y A1))))"
    65   by (simp add: assms mult_est_spmat_def spm_mult_le_dual_prts[where A=A, simplified Let_def])
    66 
    67 ML_file "matrixlp.ML"
    68 
    69 end
    70