src/HOL/Matrix_LP/Cplex.thy
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 46988 9f492f5b0cec
child 47455 26315a545e26
permissions -rw-r--r--
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
41959
b460124855b8 tuned headers;
wenzelm
parents: 37764
diff changeset
     1
(*  Title:      HOL/Matrix/Cplex.thy
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
     2
    Author:     Steven Obua
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
     3
*)
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
     4
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
     5
theory Cplex 
32491
d5d8bea0cd94 reorganized Compute theories for HOL-Matrix -- avoiding theory files within main HOL/Tools;
wenzelm
parents: 31816
diff changeset
     6
imports SparseMatrix LP ComputeFloat ComputeNumeral
28637
7aabaf1ba263 reactivated HOL-Matrix;
wenzelm
parents: 27484
diff changeset
     7
uses "Cplex_tools.ML" "CplexMatrixConverter.ML" "FloatSparseMatrixBuilder.ML"
7aabaf1ba263 reactivated HOL-Matrix;
wenzelm
parents: 27484
diff changeset
     8
  "fspmlp.ML" ("matrixlp.ML")
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
     9
begin
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    10
27484
dbb9981c3d18 added marginal setup for code generation
haftmann
parents: 23665
diff changeset
    11
lemma spm_mult_le_dual_prts: 
dbb9981c3d18 added marginal setup for code generation
haftmann
parents: 23665
diff changeset
    12
  assumes
dbb9981c3d18 added marginal setup for code generation
haftmann
parents: 23665
diff changeset
    13
  "sorted_sparse_matrix A1"
dbb9981c3d18 added marginal setup for code generation
haftmann
parents: 23665
diff changeset
    14
  "sorted_sparse_matrix A2"
dbb9981c3d18 added marginal setup for code generation
haftmann
parents: 23665
diff changeset
    15
  "sorted_sparse_matrix c1"
dbb9981c3d18 added marginal setup for code generation
haftmann
parents: 23665
diff changeset
    16
  "sorted_sparse_matrix c2"
dbb9981c3d18 added marginal setup for code generation
haftmann
parents: 23665
diff changeset
    17
  "sorted_sparse_matrix y"
dbb9981c3d18 added marginal setup for code generation
haftmann
parents: 23665
diff changeset
    18
  "sorted_sparse_matrix r1"
dbb9981c3d18 added marginal setup for code generation
haftmann
parents: 23665
diff changeset
    19
  "sorted_sparse_matrix r2"
dbb9981c3d18 added marginal setup for code generation
haftmann
parents: 23665
diff changeset
    20
  "sorted_spvec b"
31816
ffaf6dd53045 replaced recdefs by funs
nipkow
parents: 29804
diff changeset
    21
  "le_spmat [] y"
27484
dbb9981c3d18 added marginal setup for code generation
haftmann
parents: 23665
diff changeset
    22
  "sparse_row_matrix A1 \<le> A"
dbb9981c3d18 added marginal setup for code generation
haftmann
parents: 23665
diff changeset
    23
  "A \<le> sparse_row_matrix A2"
dbb9981c3d18 added marginal setup for code generation
haftmann
parents: 23665
diff changeset
    24
  "sparse_row_matrix c1 \<le> c"
dbb9981c3d18 added marginal setup for code generation
haftmann
parents: 23665
diff changeset
    25
  "c \<le> sparse_row_matrix c2"
dbb9981c3d18 added marginal setup for code generation
haftmann
parents: 23665
diff changeset
    26
  "sparse_row_matrix r1 \<le> x"
dbb9981c3d18 added marginal setup for code generation
haftmann
parents: 23665
diff changeset
    27
  "x \<le> sparse_row_matrix r2"
35028
108662d50512 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 32491
diff changeset
    28
  "A * x \<le> sparse_row_matrix (b::('a::lattice_ring) spmat)"
27484
dbb9981c3d18 added marginal setup for code generation
haftmann
parents: 23665
diff changeset
    29
  shows
31816
ffaf6dd53045 replaced recdefs by funs
nipkow
parents: 29804
diff changeset
    30
  "c * x \<le> sparse_row_matrix (add_spmat (mult_spmat y b)
27484
dbb9981c3d18 added marginal setup for code generation
haftmann
parents: 23665
diff changeset
    31
  (let s1 = diff_spmat c1 (mult_spmat y A2); s2 = diff_spmat c2 (mult_spmat y A1) in 
31816
ffaf6dd53045 replaced recdefs by funs
nipkow
parents: 29804
diff changeset
    32
  add_spmat (mult_spmat (pprt_spmat s2) (pprt_spmat r2)) (add_spmat (mult_spmat (pprt_spmat s1) (nprt_spmat r2)) 
ffaf6dd53045 replaced recdefs by funs
nipkow
parents: 29804
diff changeset
    33
  (add_spmat (mult_spmat (nprt_spmat s2) (pprt_spmat r1)) (mult_spmat (nprt_spmat s1) (nprt_spmat r1))))))"
27484
dbb9981c3d18 added marginal setup for code generation
haftmann
parents: 23665
diff changeset
    34
  apply (simp add: Let_def)
28637
7aabaf1ba263 reactivated HOL-Matrix;
wenzelm
parents: 27484
diff changeset
    35
  apply (insert assms)
29667
53103fc8ffa3 Replaced group_ and ring_simps by algebra_simps;
nipkow
parents: 28637
diff changeset
    36
  apply (simp add: sparse_row_matrix_op_simps algebra_simps)  
53103fc8ffa3 Replaced group_ and ring_simps by algebra_simps;
nipkow
parents: 28637
diff changeset
    37
  apply (rule mult_le_dual_prts[where A=A, simplified Let_def algebra_simps])
27484
dbb9981c3d18 added marginal setup for code generation
haftmann
parents: 23665
diff changeset
    38
  apply (auto)
dbb9981c3d18 added marginal setup for code generation
haftmann
parents: 23665
diff changeset
    39
  done
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    40
27484
dbb9981c3d18 added marginal setup for code generation
haftmann
parents: 23665
diff changeset
    41
lemma spm_mult_le_dual_prts_no_let: 
dbb9981c3d18 added marginal setup for code generation
haftmann
parents: 23665
diff changeset
    42
  assumes
dbb9981c3d18 added marginal setup for code generation
haftmann
parents: 23665
diff changeset
    43
  "sorted_sparse_matrix A1"
dbb9981c3d18 added marginal setup for code generation
haftmann
parents: 23665
diff changeset
    44
  "sorted_sparse_matrix A2"
dbb9981c3d18 added marginal setup for code generation
haftmann
parents: 23665
diff changeset
    45
  "sorted_sparse_matrix c1"
dbb9981c3d18 added marginal setup for code generation
haftmann
parents: 23665
diff changeset
    46
  "sorted_sparse_matrix c2"
dbb9981c3d18 added marginal setup for code generation
haftmann
parents: 23665
diff changeset
    47
  "sorted_sparse_matrix y"
dbb9981c3d18 added marginal setup for code generation
haftmann
parents: 23665
diff changeset
    48
  "sorted_sparse_matrix r1"
dbb9981c3d18 added marginal setup for code generation
haftmann
parents: 23665
diff changeset
    49
  "sorted_sparse_matrix r2"
dbb9981c3d18 added marginal setup for code generation
haftmann
parents: 23665
diff changeset
    50
  "sorted_spvec b"
31816
ffaf6dd53045 replaced recdefs by funs
nipkow
parents: 29804
diff changeset
    51
  "le_spmat [] y"
27484
dbb9981c3d18 added marginal setup for code generation
haftmann
parents: 23665
diff changeset
    52
  "sparse_row_matrix A1 \<le> A"
dbb9981c3d18 added marginal setup for code generation
haftmann
parents: 23665
diff changeset
    53
  "A \<le> sparse_row_matrix A2"
dbb9981c3d18 added marginal setup for code generation
haftmann
parents: 23665
diff changeset
    54
  "sparse_row_matrix c1 \<le> c"
dbb9981c3d18 added marginal setup for code generation
haftmann
parents: 23665
diff changeset
    55
  "c \<le> sparse_row_matrix c2"
dbb9981c3d18 added marginal setup for code generation
haftmann
parents: 23665
diff changeset
    56
  "sparse_row_matrix r1 \<le> x"
dbb9981c3d18 added marginal setup for code generation
haftmann
parents: 23665
diff changeset
    57
  "x \<le> sparse_row_matrix r2"
35028
108662d50512 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 32491
diff changeset
    58
  "A * x \<le> sparse_row_matrix (b::('a::lattice_ring) spmat)"
27484
dbb9981c3d18 added marginal setup for code generation
haftmann
parents: 23665
diff changeset
    59
  shows
31816
ffaf6dd53045 replaced recdefs by funs
nipkow
parents: 29804
diff changeset
    60
  "c * x \<le> sparse_row_matrix (add_spmat (mult_spmat y b)
ffaf6dd53045 replaced recdefs by funs
nipkow
parents: 29804
diff changeset
    61
  (mult_est_spmat r1 r2 (diff_spmat c1 (mult_spmat y A2)) (diff_spmat c2 (mult_spmat y A1))))"
28637
7aabaf1ba263 reactivated HOL-Matrix;
wenzelm
parents: 27484
diff changeset
    62
  by (simp add: assms mult_est_spmat_def spm_mult_le_dual_prts[where A=A, simplified Let_def])
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    63
27484
dbb9981c3d18 added marginal setup for code generation
haftmann
parents: 23665
diff changeset
    64
use "matrixlp.ML"
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    65
27484
dbb9981c3d18 added marginal setup for code generation
haftmann
parents: 23665
diff changeset
    66
end
46543
c7c289ce9ad2 tuned whitespace
haftmann
parents: 41959
diff changeset
    67