equal
deleted
inserted
replaced
23 "A \<le> sparse_row_matrix A2" |
23 "A \<le> sparse_row_matrix A2" |
24 "sparse_row_matrix c1 \<le> c" |
24 "sparse_row_matrix c1 \<le> c" |
25 "c \<le> sparse_row_matrix c2" |
25 "c \<le> sparse_row_matrix c2" |
26 "sparse_row_matrix r1 \<le> x" |
26 "sparse_row_matrix r1 \<le> x" |
27 "x \<le> sparse_row_matrix r2" |
27 "x \<le> sparse_row_matrix r2" |
28 "A * x \<le> sparse_row_matrix (b::('a::lordered_ring) spmat)" |
28 "A * x \<le> sparse_row_matrix (b::('a::lattice_ring) spmat)" |
29 shows |
29 shows |
30 "c * x \<le> sparse_row_matrix (add_spmat (mult_spmat y b) |
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 |
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)) |
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))))))" |
33 (add_spmat (mult_spmat (nprt_spmat s2) (pprt_spmat r1)) (mult_spmat (nprt_spmat s1) (nprt_spmat r1))))))" |
53 "A \<le> sparse_row_matrix A2" |
53 "A \<le> sparse_row_matrix A2" |
54 "sparse_row_matrix c1 \<le> c" |
54 "sparse_row_matrix c1 \<le> c" |
55 "c \<le> sparse_row_matrix c2" |
55 "c \<le> sparse_row_matrix c2" |
56 "sparse_row_matrix r1 \<le> x" |
56 "sparse_row_matrix r1 \<le> x" |
57 "x \<le> sparse_row_matrix r2" |
57 "x \<le> sparse_row_matrix r2" |
58 "A * x \<le> sparse_row_matrix (b::('a::lordered_ring) spmat)" |
58 "A * x \<le> sparse_row_matrix (b::('a::lattice_ring) spmat)" |
59 shows |
59 shows |
60 "c * x \<le> sparse_row_matrix (add_spmat (mult_spmat y b) |
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))))" |
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]) |
62 by (simp add: assms mult_est_spmat_def spm_mult_le_dual_prts[where A=A, simplified Let_def]) |
63 |
63 |