author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 46988  9f492f5b0cec 
child 47455  26315a545e26 
permissions  rwrr 
41959  1 
(* Title: HOL/Matrix/Cplex.thy 
16784  2 
Author: Steven Obua 
3 
*) 

4 

5 
theory Cplex 

32491
d5d8bea0cd94
reorganized Compute theories for HOLMatrix  avoiding theory files within main HOL/Tools;
wenzelm
parents:
31816
diff
changeset

6 
imports SparseMatrix LP ComputeFloat ComputeNumeral 
28637  7 
uses "Cplex_tools.ML" "CplexMatrixConverter.ML" "FloatSparseMatrixBuilder.ML" 
8 
"fspmlp.ML" ("matrixlp.ML") 

16784  9 
begin 
10 

27484  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" 

31816  21 
"le_spmat [] y" 
27484  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" 

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  29 
shows 
31816  30 
"c * x \<le> sparse_row_matrix (add_spmat (mult_spmat y b) 
27484  31 
(let s1 = diff_spmat c1 (mult_spmat y A2); s2 = diff_spmat c2 (mult_spmat y A1) in 
31816  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))))))" 

27484  34 
apply (simp add: Let_def) 
28637  35 
apply (insert assms) 
29667  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]) 

27484  38 
apply (auto) 
39 
done 

16784  40 

27484  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" 

31816  51 
"le_spmat [] y" 
27484  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" 

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  59 
shows 
31816  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))))" 

28637  62 
by (simp add: assms mult_est_spmat_def spm_mult_le_dual_prts[where A=A, simplified Let_def]) 
16784  63 

27484  64 
use "matrixlp.ML" 
16784  65 

27484  66 
end 
46543  67 