src/HOL/Matrix_LP/Cplex.thy
author wenzelm
Tue Oct 10 19:23:03 2017 +0200 (2017-10-10)
changeset 66831 29ea2b900a05
parent 48891 c0eafbd55de3
child 69605 a96320074298
permissions -rw-r--r--
tuned: each session has at most one defining entry;
wenzelm@47455
     1
(*  Title:      HOL/Matrix_LP/Cplex.thy
obua@16784
     2
    Author:     Steven Obua
obua@16784
     3
*)
obua@16784
     4
obua@16784
     5
theory Cplex 
wenzelm@32491
     6
imports SparseMatrix LP ComputeFloat ComputeNumeral
obua@16784
     7
begin
obua@16784
     8
wenzelm@48891
     9
ML_file "Cplex_tools.ML"
wenzelm@48891
    10
ML_file "CplexMatrixConverter.ML"
wenzelm@48891
    11
ML_file "FloatSparseMatrixBuilder.ML"
wenzelm@48891
    12
ML_file "fspmlp.ML"
wenzelm@48891
    13
haftmann@27484
    14
lemma spm_mult_le_dual_prts: 
haftmann@27484
    15
  assumes
haftmann@27484
    16
  "sorted_sparse_matrix A1"
haftmann@27484
    17
  "sorted_sparse_matrix A2"
haftmann@27484
    18
  "sorted_sparse_matrix c1"
haftmann@27484
    19
  "sorted_sparse_matrix c2"
haftmann@27484
    20
  "sorted_sparse_matrix y"
haftmann@27484
    21
  "sorted_sparse_matrix r1"
haftmann@27484
    22
  "sorted_sparse_matrix r2"
haftmann@27484
    23
  "sorted_spvec b"
nipkow@31816
    24
  "le_spmat [] y"
haftmann@27484
    25
  "sparse_row_matrix A1 \<le> A"
haftmann@27484
    26
  "A \<le> sparse_row_matrix A2"
haftmann@27484
    27
  "sparse_row_matrix c1 \<le> c"
haftmann@27484
    28
  "c \<le> sparse_row_matrix c2"
haftmann@27484
    29
  "sparse_row_matrix r1 \<le> x"
haftmann@27484
    30
  "x \<le> sparse_row_matrix r2"
haftmann@35028
    31
  "A * x \<le> sparse_row_matrix (b::('a::lattice_ring) spmat)"
haftmann@27484
    32
  shows
nipkow@31816
    33
  "c * x \<le> sparse_row_matrix (add_spmat (mult_spmat y b)
haftmann@27484
    34
  (let s1 = diff_spmat c1 (mult_spmat y A2); s2 = diff_spmat c2 (mult_spmat y A1) in 
nipkow@31816
    35
  add_spmat (mult_spmat (pprt_spmat s2) (pprt_spmat r2)) (add_spmat (mult_spmat (pprt_spmat s1) (nprt_spmat r2)) 
nipkow@31816
    36
  (add_spmat (mult_spmat (nprt_spmat s2) (pprt_spmat r1)) (mult_spmat (nprt_spmat s1) (nprt_spmat r1))))))"
haftmann@27484
    37
  apply (simp add: Let_def)
wenzelm@28637
    38
  apply (insert assms)
nipkow@29667
    39
  apply (simp add: sparse_row_matrix_op_simps algebra_simps)  
nipkow@29667
    40
  apply (rule mult_le_dual_prts[where A=A, simplified Let_def algebra_simps])
haftmann@27484
    41
  apply (auto)
haftmann@27484
    42
  done
obua@16784
    43
haftmann@27484
    44
lemma spm_mult_le_dual_prts_no_let: 
haftmann@27484
    45
  assumes
haftmann@27484
    46
  "sorted_sparse_matrix A1"
haftmann@27484
    47
  "sorted_sparse_matrix A2"
haftmann@27484
    48
  "sorted_sparse_matrix c1"
haftmann@27484
    49
  "sorted_sparse_matrix c2"
haftmann@27484
    50
  "sorted_sparse_matrix y"
haftmann@27484
    51
  "sorted_sparse_matrix r1"
haftmann@27484
    52
  "sorted_sparse_matrix r2"
haftmann@27484
    53
  "sorted_spvec b"
nipkow@31816
    54
  "le_spmat [] y"
haftmann@27484
    55
  "sparse_row_matrix A1 \<le> A"
haftmann@27484
    56
  "A \<le> sparse_row_matrix A2"
haftmann@27484
    57
  "sparse_row_matrix c1 \<le> c"
haftmann@27484
    58
  "c \<le> sparse_row_matrix c2"
haftmann@27484
    59
  "sparse_row_matrix r1 \<le> x"
haftmann@27484
    60
  "x \<le> sparse_row_matrix r2"
haftmann@35028
    61
  "A * x \<le> sparse_row_matrix (b::('a::lattice_ring) spmat)"
haftmann@27484
    62
  shows
nipkow@31816
    63
  "c * x \<le> sparse_row_matrix (add_spmat (mult_spmat y b)
nipkow@31816
    64
  (mult_est_spmat r1 r2 (diff_spmat c1 (mult_spmat y A2)) (diff_spmat c2 (mult_spmat y A1))))"
wenzelm@28637
    65
  by (simp add: assms mult_est_spmat_def spm_mult_le_dual_prts[where A=A, simplified Let_def])
obua@16784
    66
wenzelm@48891
    67
ML_file "matrixlp.ML"
obua@16784
    68
haftmann@27484
    69
end
haftmann@46543
    70