author | wenzelm |
Wed, 02 Sep 2009 16:25:44 +0200 | |
changeset 32491 | d5d8bea0cd94 |
parent 31817 | 9b34b1449cb7 |
child 35028 | 108662d50512 |
permissions | -rw-r--r-- |
16487 | 1 |
(* Title: HOL/Matrix/SparseMatrix.thy |
2 |
Author: Steven Obua |
|
3 |
*) |
|
4 |
||
27484 | 5 |
theory SparseMatrix |
28637 | 6 |
imports Matrix |
27484 | 7 |
begin |
15009 | 8 |
|
9 |
types |
|
10 |
'a spvec = "(nat * 'a) list" |
|
11 |
'a spmat = "('a spvec) spvec" |
|
12 |
||
27653 | 13 |
definition sparse_row_vector :: "('a::ab_group_add) spvec \<Rightarrow> 'a matrix" where |
27484 | 14 |
sparse_row_vector_def: "sparse_row_vector arr = foldl (% m x. m + (singleton_matrix 0 (fst x) (snd x))) 0 arr" |
15009 | 15 |
|
27653 | 16 |
definition sparse_row_matrix :: "('a::ab_group_add) spmat \<Rightarrow> 'a matrix" where |
27484 | 17 |
sparse_row_matrix_def: "sparse_row_matrix arr = foldl (% m r. m + (move_matrix (sparse_row_vector (snd r)) (int (fst r)) 0)) 0 arr" |
15009 | 18 |
|
27484 | 19 |
code_datatype sparse_row_vector sparse_row_matrix |
20 |
||
21 |
lemma sparse_row_vector_empty [simp]: "sparse_row_vector [] = 0" |
|
15009 | 22 |
by (simp add: sparse_row_vector_def) |
23 |
||
27484 | 24 |
lemma sparse_row_matrix_empty [simp]: "sparse_row_matrix [] = 0" |
15009 | 25 |
by (simp add: sparse_row_matrix_def) |
26 |
||
28562 | 27 |
lemmas [code] = sparse_row_vector_empty [symmetric] |
27484 | 28 |
|
31817 | 29 |
lemma foldl_distrstart: "! a x y. (f (g x y) a = g x (f y a)) \<Longrightarrow> (foldl f (g x y) l = g x (foldl f y l))" |
30 |
by (induct l arbitrary: x y, auto) |
|
15009 | 31 |
|
27653 | 32 |
lemma sparse_row_vector_cons[simp]: |
33 |
"sparse_row_vector (a # arr) = (singleton_matrix 0 (fst a) (snd a)) + (sparse_row_vector arr)" |
|
15009 | 34 |
apply (induct arr) |
35 |
apply (auto simp add: sparse_row_vector_def) |
|
27653 | 36 |
apply (simp add: foldl_distrstart [of "\<lambda>m x. m + singleton_matrix 0 (fst x) (snd x)" "\<lambda>x m. singleton_matrix 0 (fst x) (snd x) + m"]) |
15009 | 37 |
done |
38 |
||
27653 | 39 |
lemma sparse_row_vector_append[simp]: |
40 |
"sparse_row_vector (a @ b) = (sparse_row_vector a) + (sparse_row_vector b)" |
|
41 |
by (induct a) auto |
|
15009 | 42 |
|
43 |
lemma nrows_spvec[simp]: "nrows (sparse_row_vector x) <= (Suc 0)" |
|
44 |
apply (induct x) |
|
45 |
apply (simp_all add: add_nrows) |
|
46 |
done |
|
47 |
||
48 |
lemma sparse_row_matrix_cons: "sparse_row_matrix (a#arr) = ((move_matrix (sparse_row_vector (snd a)) (int (fst a)) 0)) + sparse_row_matrix arr" |
|
49 |
apply (induct arr) |
|
50 |
apply (auto simp add: sparse_row_matrix_def) |
|
51 |
apply (simp add: foldl_distrstart[of "\<lambda>m x. m + (move_matrix (sparse_row_vector (snd x)) (int (fst x)) 0)" |
|
52 |
"% a m. (move_matrix (sparse_row_vector (snd a)) (int (fst a)) 0) + m"]) |
|
53 |
done |
|
54 |
||
55 |
lemma sparse_row_matrix_append: "sparse_row_matrix (arr@brr) = (sparse_row_matrix arr) + (sparse_row_matrix brr)" |
|
56 |
apply (induct arr) |
|
57 |
apply (auto simp add: sparse_row_matrix_cons) |
|
58 |
done |
|
59 |
||
27653 | 60 |
primrec sorted_spvec :: "'a spvec \<Rightarrow> bool" where |
61 |
"sorted_spvec [] = True" |
|
62 |
| sorted_spvec_step: "sorted_spvec (a#as) = (case as of [] \<Rightarrow> True | b#bs \<Rightarrow> ((fst a < fst b) & (sorted_spvec as)))" |
|
15009 | 63 |
|
27653 | 64 |
primrec sorted_spmat :: "'a spmat \<Rightarrow> bool" where |
15009 | 65 |
"sorted_spmat [] = True" |
27653 | 66 |
| "sorted_spmat (a#as) = ((sorted_spvec (snd a)) & (sorted_spmat as))" |
15009 | 67 |
|
68 |
declare sorted_spvec.simps [simp del] |
|
69 |
||
70 |
lemma sorted_spvec_empty[simp]: "sorted_spvec [] = True" |
|
71 |
by (simp add: sorted_spvec.simps) |
|
72 |
||
73 |
lemma sorted_spvec_cons1: "sorted_spvec (a#as) \<Longrightarrow> sorted_spvec as" |
|
74 |
apply (induct as) |
|
75 |
apply (auto simp add: sorted_spvec.simps) |
|
76 |
done |
|
77 |
||
78 |
lemma sorted_spvec_cons2: "sorted_spvec (a#b#t) \<Longrightarrow> sorted_spvec (a#t)" |
|
79 |
apply (induct t) |
|
80 |
apply (auto simp add: sorted_spvec.simps) |
|
81 |
done |
|
82 |
||
83 |
lemma sorted_spvec_cons3: "sorted_spvec(a#b#t) \<Longrightarrow> fst a < fst b" |
|
84 |
apply (auto simp add: sorted_spvec.simps) |
|
85 |
done |
|
86 |
||
31817 | 87 |
lemma sorted_sparse_row_vector_zero[rule_format]: "m <= n \<Longrightarrow> sorted_spvec ((n,a)#arr) \<longrightarrow> Rep_matrix (sparse_row_vector arr) j m = 0" |
15009 | 88 |
apply (induct arr) |
89 |
apply (auto) |
|
90 |
apply (frule sorted_spvec_cons2,simp)+ |
|
91 |
apply (frule sorted_spvec_cons3, simp) |
|
92 |
done |
|
93 |
||
31817 | 94 |
lemma sorted_sparse_row_matrix_zero[rule_format]: "m <= n \<Longrightarrow> sorted_spvec ((n,a)#arr) \<longrightarrow> Rep_matrix (sparse_row_matrix arr) m j = 0" |
15009 | 95 |
apply (induct arr) |
96 |
apply (auto) |
|
97 |
apply (frule sorted_spvec_cons2, simp) |
|
98 |
apply (frule sorted_spvec_cons3, simp) |
|
99 |
apply (simp add: sparse_row_matrix_cons neg_def) |
|
100 |
done |
|
101 |
||
27653 | 102 |
primrec minus_spvec :: "('a::ab_group_add) spvec \<Rightarrow> 'a spvec" where |
15178 | 103 |
"minus_spvec [] = []" |
27484 | 104 |
| "minus_spvec (a#as) = (fst a, -(snd a))#(minus_spvec as)" |
15178 | 105 |
|
27653 | 106 |
primrec abs_spvec :: "('a::lordered_ab_group_add_abs) spvec \<Rightarrow> 'a spvec" where |
15178 | 107 |
"abs_spvec [] = []" |
27484 | 108 |
| "abs_spvec (a#as) = (fst a, abs (snd a))#(abs_spvec as)" |
15178 | 109 |
|
110 |
lemma sparse_row_vector_minus: |
|
111 |
"sparse_row_vector (minus_spvec v) = - (sparse_row_vector v)" |
|
112 |
apply (induct v) |
|
113 |
apply (simp_all add: sparse_row_vector_cons) |
|
114 |
apply (simp add: Rep_matrix_inject[symmetric]) |
|
115 |
apply (rule ext)+ |
|
116 |
apply simp |
|
117 |
done |
|
118 |
||
27653 | 119 |
instance matrix :: (lordered_ab_group_add_abs) lordered_ab_group_add_abs |
120 |
apply default |
|
121 |
unfolding abs_matrix_def .. (*FIXME move*) |
|
122 |
||
15178 | 123 |
lemma sparse_row_vector_abs: |
27653 | 124 |
"sorted_spvec (v :: 'a::lordered_ring spvec) \<Longrightarrow> sparse_row_vector (abs_spvec v) = abs (sparse_row_vector v)" |
15178 | 125 |
apply (induct v) |
27653 | 126 |
apply simp_all |
15178 | 127 |
apply (frule_tac sorted_spvec_cons1, simp) |
128 |
apply (simp only: Rep_matrix_inject[symmetric]) |
|
129 |
apply (rule ext)+ |
|
130 |
apply auto |
|
15236
f289e8ba2bb3
Proofs needed to be updated because induction now preserves name of
nipkow
parents:
15197
diff
changeset
|
131 |
apply (subgoal_tac "Rep_matrix (sparse_row_vector v) 0 a = 0") |
15178 | 132 |
apply (simp) |
133 |
apply (rule sorted_sparse_row_vector_zero) |
|
134 |
apply auto |
|
135 |
done |
|
136 |
||
137 |
lemma sorted_spvec_minus_spvec: |
|
138 |
"sorted_spvec v \<Longrightarrow> sorted_spvec (minus_spvec v)" |
|
139 |
apply (induct v) |
|
140 |
apply (simp) |
|
141 |
apply (frule sorted_spvec_cons1, simp) |
|
15236
f289e8ba2bb3
Proofs needed to be updated because induction now preserves name of
nipkow
parents:
15197
diff
changeset
|
142 |
apply (simp add: sorted_spvec.simps split:list.split_asm) |
15178 | 143 |
done |
144 |
||
145 |
lemma sorted_spvec_abs_spvec: |
|
146 |
"sorted_spvec v \<Longrightarrow> sorted_spvec (abs_spvec v)" |
|
147 |
apply (induct v) |
|
148 |
apply (simp) |
|
149 |
apply (frule sorted_spvec_cons1, simp) |
|
15236
f289e8ba2bb3
Proofs needed to be updated because induction now preserves name of
nipkow
parents:
15197
diff
changeset
|
150 |
apply (simp add: sorted_spvec.simps split:list.split_asm) |
15178 | 151 |
done |
152 |
||
27653 | 153 |
definition |
154 |
"smult_spvec y = map (% a. (fst a, y * snd a))" |
|
15009 | 155 |
|
156 |
lemma smult_spvec_empty[simp]: "smult_spvec y [] = []" |
|
157 |
by (simp add: smult_spvec_def) |
|
158 |
||
159 |
lemma smult_spvec_cons: "smult_spvec y (a#arr) = (fst a, y * (snd a)) # (smult_spvec y arr)" |
|
160 |
by (simp add: smult_spvec_def) |
|
161 |
||
31816 | 162 |
fun addmult_spvec :: "('a::ring) \<Rightarrow> 'a spvec \<Rightarrow> 'a spvec \<Rightarrow> 'a spvec" where |
163 |
"addmult_spvec y arr [] = arr" | |
|
164 |
"addmult_spvec y [] brr = smult_spvec y brr" | |
|
165 |
"addmult_spvec y ((i,a)#arr) ((j,b)#brr) = ( |
|
166 |
if i < j then ((i,a)#(addmult_spvec y arr ((j,b)#brr))) |
|
167 |
else (if (j < i) then ((j, y * b)#(addmult_spvec y ((i,a)#arr) brr)) |
|
168 |
else ((i, a + y*b)#(addmult_spvec y arr brr))))" |
|
169 |
(* Steven used termination "measure (% (y, a, b). length a + (length b))" *) |
|
15009 | 170 |
|
31816 | 171 |
lemma addmult_spvec_empty1[simp]: "addmult_spvec y [] a = smult_spvec y a" |
27484 | 172 |
by (induct a) auto |
15009 | 173 |
|
31816 | 174 |
lemma addmult_spvec_empty2[simp]: "addmult_spvec y a [] = a" |
27484 | 175 |
by (induct a) auto |
15009 | 176 |
|
177 |
lemma sparse_row_vector_map: "(! x y. f (x+y) = (f x) + (f y)) \<Longrightarrow> (f::'a\<Rightarrow>('a::lordered_ring)) 0 = 0 \<Longrightarrow> |
|
178 |
sparse_row_vector (map (% x. (fst x, f (snd x))) a) = apply_matrix f (sparse_row_vector a)" |
|
179 |
apply (induct a) |
|
180 |
apply (simp_all add: apply_matrix_add) |
|
181 |
done |
|
182 |
||
183 |
lemma sparse_row_vector_smult: "sparse_row_vector (smult_spvec y a) = scalar_mult y (sparse_row_vector a)" |
|
184 |
apply (induct a) |
|
185 |
apply (simp_all add: smult_spvec_cons scalar_mult_add) |
|
186 |
done |
|
187 |
||
31816 | 188 |
lemma sparse_row_vector_addmult_spvec: "sparse_row_vector (addmult_spvec (y::'a::lordered_ring) a b) = |
15009 | 189 |
(sparse_row_vector a) + (scalar_mult y (sparse_row_vector b))" |
31817 | 190 |
apply (induct y a b rule: addmult_spvec.induct) |
15009 | 191 |
apply (simp add: scalar_mult_add smult_spvec_cons sparse_row_vector_smult singleton_matrix_add)+ |
192 |
done |
|
193 |
||
31817 | 194 |
lemma sorted_smult_spvec: "sorted_spvec a \<Longrightarrow> sorted_spvec (smult_spvec y a)" |
15009 | 195 |
apply (auto simp add: smult_spvec_def) |
196 |
apply (induct a) |
|
15236
f289e8ba2bb3
Proofs needed to be updated because induction now preserves name of
nipkow
parents:
15197
diff
changeset
|
197 |
apply (auto simp add: sorted_spvec.simps split:list.split_asm) |
15009 | 198 |
done |
199 |
||
31816 | 200 |
lemma sorted_spvec_addmult_spvec_helper: "\<lbrakk>sorted_spvec (addmult_spvec y ((a, b) # arr) brr); aa < a; sorted_spvec ((a, b) # arr); |
201 |
sorted_spvec ((aa, ba) # brr)\<rbrakk> \<Longrightarrow> sorted_spvec ((aa, y * ba) # addmult_spvec y ((a, b) # arr) brr)" |
|
15009 | 202 |
apply (induct brr) |
203 |
apply (auto simp add: sorted_spvec.simps) |
|
204 |
done |
|
205 |
||
206 |
lemma sorted_spvec_addmult_spvec_helper2: |
|
31816 | 207 |
"\<lbrakk>sorted_spvec (addmult_spvec y arr ((aa, ba) # brr)); a < aa; sorted_spvec ((a, b) # arr); sorted_spvec ((aa, ba) # brr)\<rbrakk> |
208 |
\<Longrightarrow> sorted_spvec ((a, b) # addmult_spvec y arr ((aa, ba) # brr))" |
|
15009 | 209 |
apply (induct arr) |
210 |
apply (auto simp add: smult_spvec_def sorted_spvec.simps) |
|
211 |
done |
|
212 |
||
213 |
lemma sorted_spvec_addmult_spvec_helper3[rule_format]: |
|
31816 | 214 |
"sorted_spvec (addmult_spvec y arr brr) \<longrightarrow> sorted_spvec ((aa, b) # arr) \<longrightarrow> sorted_spvec ((aa, ba) # brr) |
215 |
\<longrightarrow> sorted_spvec ((aa, b + y * ba) # (addmult_spvec y arr brr))" |
|
216 |
apply (induct y arr brr rule: addmult_spvec.induct) |
|
217 |
apply (simp_all add: sorted_spvec.simps smult_spvec_def split:list.split) |
|
15009 | 218 |
done |
219 |
||
31817 | 220 |
lemma sorted_addmult_spvec: "sorted_spvec a \<Longrightarrow> sorted_spvec b \<Longrightarrow> sorted_spvec (addmult_spvec y a b)" |
221 |
apply (induct y a b rule: addmult_spvec.induct) |
|
15009 | 222 |
apply (simp_all add: sorted_smult_spvec) |
223 |
apply (rule conjI, intro strip) |
|
31816 | 224 |
apply (case_tac "~(i < j)") |
15009 | 225 |
apply (simp_all) |
226 |
apply (frule_tac as=brr in sorted_spvec_cons1) |
|
227 |
apply (simp add: sorted_spvec_addmult_spvec_helper) |
|
228 |
apply (intro strip | rule conjI)+ |
|
229 |
apply (frule_tac as=arr in sorted_spvec_cons1) |
|
230 |
apply (simp add: sorted_spvec_addmult_spvec_helper2) |
|
231 |
apply (intro strip) |
|
232 |
apply (frule_tac as=arr in sorted_spvec_cons1) |
|
233 |
apply (frule_tac as=brr in sorted_spvec_cons1) |
|
234 |
apply (simp) |
|
235 |
apply (simp_all add: sorted_spvec_addmult_spvec_helper3) |
|
236 |
done |
|
237 |
||
31816 | 238 |
fun mult_spvec_spmat :: "('a::lordered_ring) spvec \<Rightarrow> 'a spvec \<Rightarrow> 'a spmat \<Rightarrow> 'a spvec" where |
239 |
(* recdef mult_spvec_spmat "measure (% (c, arr, brr). (length arr) + (length brr))" *) |
|
240 |
"mult_spvec_spmat c [] brr = c" | |
|
241 |
"mult_spvec_spmat c arr [] = c" | |
|
242 |
"mult_spvec_spmat c ((i,a)#arr) ((j,b)#brr) = ( |
|
243 |
if (i < j) then mult_spvec_spmat c arr ((j,b)#brr) |
|
244 |
else if (j < i) then mult_spvec_spmat c ((i,a)#arr) brr |
|
245 |
else mult_spvec_spmat (addmult_spvec a c b) arr brr)" |
|
15009 | 246 |
|
247 |
lemma sparse_row_mult_spvec_spmat[rule_format]: "sorted_spvec (a::('a::lordered_ring) spvec) \<longrightarrow> sorted_spvec B \<longrightarrow> |
|
31816 | 248 |
sparse_row_vector (mult_spvec_spmat c a B) = (sparse_row_vector c) + (sparse_row_vector a) * (sparse_row_matrix B)" |
15009 | 249 |
proof - |
250 |
have comp_1: "!! a b. a < b \<Longrightarrow> Suc 0 <= nat ((int b)-(int a))" by arith |
|
251 |
have not_iff: "!! a b. a = b \<Longrightarrow> (~ a) = (~ b)" by simp |
|
252 |
have max_helper: "!! a b. ~ (a <= max (Suc a) b) \<Longrightarrow> False" |
|
253 |
by arith |
|
254 |
{ |
|
255 |
fix a |
|
256 |
fix v |
|
257 |
assume a:"a < nrows(sparse_row_vector v)" |
|
258 |
have b:"nrows(sparse_row_vector v) <= 1" by simp |
|
259 |
note dummy = less_le_trans[of a "nrows (sparse_row_vector v)" 1, OF a b] |
|
260 |
then have "a = 0" by simp |
|
261 |
} |
|
262 |
note nrows_helper = this |
|
263 |
show ?thesis |
|
31817 | 264 |
apply (induct c a B rule: mult_spvec_spmat.induct) |
15009 | 265 |
apply simp+ |
266 |
apply (rule conjI) |
|
267 |
apply (intro strip) |
|
268 |
apply (frule_tac as=brr in sorted_spvec_cons1) |
|
29667 | 269 |
apply (simp add: algebra_simps sparse_row_matrix_cons) |
15481 | 270 |
apply (simplesubst Rep_matrix_zero_imp_mult_zero) |
15009 | 271 |
apply (simp) |
272 |
apply (intro strip) |
|
273 |
apply (rule disjI2) |
|
274 |
apply (intro strip) |
|
275 |
apply (subst nrows) |
|
276 |
apply (rule order_trans[of _ 1]) |
|
277 |
apply (simp add: comp_1)+ |
|
278 |
apply (subst Rep_matrix_zero_imp_mult_zero) |
|
279 |
apply (intro strip) |
|
31816 | 280 |
apply (case_tac "k <= j") |
281 |
apply (rule_tac m1 = k and n1 = i and a1 = a in ssubst[OF sorted_sparse_row_vector_zero]) |
|
15009 | 282 |
apply (simp_all) |
283 |
apply (rule impI) |
|
284 |
apply (rule disjI2) |
|
285 |
apply (rule nrows) |
|
286 |
apply (rule order_trans[of _ 1]) |
|
287 |
apply (simp_all add: comp_1) |
|
288 |
||
289 |
apply (intro strip | rule conjI)+ |
|
290 |
apply (frule_tac as=arr in sorted_spvec_cons1) |
|
29667 | 291 |
apply (simp add: algebra_simps) |
15009 | 292 |
apply (subst Rep_matrix_zero_imp_mult_zero) |
293 |
apply (simp) |
|
294 |
apply (rule disjI2) |
|
295 |
apply (intro strip) |
|
296 |
apply (simp add: sparse_row_matrix_cons neg_def) |
|
31816 | 297 |
apply (case_tac "i <= j") |
15009 | 298 |
apply (erule sorted_sparse_row_matrix_zero) |
299 |
apply (simp_all) |
|
300 |
apply (intro strip) |
|
31816 | 301 |
apply (case_tac "i=j") |
15009 | 302 |
apply (simp_all) |
303 |
apply (frule_tac as=arr in sorted_spvec_cons1) |
|
304 |
apply (frule_tac as=brr in sorted_spvec_cons1) |
|
29667 | 305 |
apply (simp add: sparse_row_matrix_cons algebra_simps sparse_row_vector_addmult_spvec) |
15009 | 306 |
apply (rule_tac B1 = "sparse_row_matrix brr" in ssubst[OF Rep_matrix_zero_imp_mult_zero]) |
307 |
apply (auto) |
|
308 |
apply (rule sorted_sparse_row_matrix_zero) |
|
309 |
apply (simp_all) |
|
310 |
apply (rule_tac A1 = "sparse_row_vector arr" in ssubst[OF Rep_matrix_zero_imp_mult_zero]) |
|
311 |
apply (auto) |
|
31816 | 312 |
apply (rule_tac m=k and n = j and a = a and arr=arr in sorted_sparse_row_vector_zero) |
15009 | 313 |
apply (simp_all) |
314 |
apply (simp add: neg_def) |
|
315 |
apply (drule nrows_notzero) |
|
316 |
apply (drule nrows_helper) |
|
317 |
apply (arith) |
|
318 |
||
319 |
apply (subst Rep_matrix_inject[symmetric]) |
|
320 |
apply (rule ext)+ |
|
321 |
apply (simp) |
|
322 |
apply (subst Rep_matrix_mult) |
|
31816 | 323 |
apply (rule_tac j1=j in ssubst[OF foldseq_almostzero]) |
15009 | 324 |
apply (simp_all) |
20432
07ec57376051
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20283
diff
changeset
|
325 |
apply (intro strip, rule conjI) |
15009 | 326 |
apply (intro strip) |
20432
07ec57376051
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20283
diff
changeset
|
327 |
apply (drule_tac max_helper) |
07ec57376051
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20283
diff
changeset
|
328 |
apply (simp) |
07ec57376051
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20283
diff
changeset
|
329 |
apply (auto) |
15009 | 330 |
apply (rule zero_imp_mult_zero) |
331 |
apply (rule disjI2) |
|
332 |
apply (rule nrows) |
|
333 |
apply (rule order_trans[of _ 1]) |
|
20432
07ec57376051
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20283
diff
changeset
|
334 |
apply (simp) |
07ec57376051
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20283
diff
changeset
|
335 |
apply (simp) |
15009 | 336 |
done |
337 |
qed |
|
338 |
||
339 |
lemma sorted_mult_spvec_spmat[rule_format]: |
|
31816 | 340 |
"sorted_spvec (c::('a::lordered_ring) spvec) \<longrightarrow> sorted_spmat B \<longrightarrow> sorted_spvec (mult_spvec_spmat c a B)" |
31817 | 341 |
apply (induct c a B rule: mult_spvec_spmat.induct) |
15009 | 342 |
apply (simp_all add: sorted_addmult_spvec) |
343 |
done |
|
344 |
||
345 |
consts |
|
346 |
mult_spmat :: "('a::lordered_ring) spmat \<Rightarrow> 'a spmat \<Rightarrow> 'a spmat" |
|
347 |
||
348 |
primrec |
|
349 |
"mult_spmat [] A = []" |
|
31816 | 350 |
"mult_spmat (a#as) A = (fst a, mult_spvec_spmat [] (snd a) A)#(mult_spmat as A)" |
15009 | 351 |
|
31817 | 352 |
lemma sparse_row_mult_spmat: |
353 |
"sorted_spmat A \<Longrightarrow> sorted_spvec B \<Longrightarrow> |
|
354 |
sparse_row_matrix (mult_spmat A B) = (sparse_row_matrix A) * (sparse_row_matrix B)" |
|
15009 | 355 |
apply (induct A) |
29667 | 356 |
apply (auto simp add: sparse_row_matrix_cons sparse_row_mult_spvec_spmat algebra_simps move_matrix_mult) |
15009 | 357 |
done |
358 |
||
359 |
lemma sorted_spvec_mult_spmat[rule_format]: |
|
360 |
"sorted_spvec (A::('a::lordered_ring) spmat) \<longrightarrow> sorted_spvec (mult_spmat A B)" |
|
361 |
apply (induct A) |
|
362 |
apply (auto) |
|
363 |
apply (drule sorted_spvec_cons1, simp) |
|
15236
f289e8ba2bb3
Proofs needed to be updated because induction now preserves name of
nipkow
parents:
15197
diff
changeset
|
364 |
apply (case_tac A) |
15009 | 365 |
apply (auto simp add: sorted_spvec.simps) |
366 |
done |
|
367 |
||
31817 | 368 |
lemma sorted_spmat_mult_spmat: |
369 |
"sorted_spmat (B::('a::lordered_ring) spmat) \<Longrightarrow> sorted_spmat (mult_spmat A B)" |
|
15009 | 370 |
apply (induct A) |
371 |
apply (auto simp add: sorted_mult_spvec_spmat) |
|
372 |
done |
|
373 |
||
374 |
||
31816 | 375 |
fun add_spvec :: "('a::lordered_ab_group_add) spvec \<Rightarrow> 'a spvec \<Rightarrow> 'a spvec" where |
376 |
(* "measure (% (a, b). length a + (length b))" *) |
|
377 |
"add_spvec arr [] = arr" | |
|
378 |
"add_spvec [] brr = brr" | |
|
379 |
"add_spvec ((i,a)#arr) ((j,b)#brr) = ( |
|
380 |
if i < j then (i,a)#(add_spvec arr ((j,b)#brr)) |
|
381 |
else if (j < i) then (j,b) # add_spvec ((i,a)#arr) brr |
|
382 |
else (i, a+b) # add_spvec arr brr)" |
|
15009 | 383 |
|
31816 | 384 |
lemma add_spvec_empty1[simp]: "add_spvec [] a = a" |
385 |
by (cases a, auto) |
|
15009 | 386 |
|
31816 | 387 |
lemma sparse_row_vector_add: "sparse_row_vector (add_spvec a b) = (sparse_row_vector a) + (sparse_row_vector b)" |
31817 | 388 |
apply (induct a b rule: add_spvec.induct) |
15009 | 389 |
apply (simp_all add: singleton_matrix_add) |
390 |
done |
|
391 |
||
31816 | 392 |
fun add_spmat :: "('a::lordered_ab_group_add) spmat \<Rightarrow> 'a spmat \<Rightarrow> 'a spmat" where |
393 |
(* "measure (% (A,B). (length A)+(length B))" *) |
|
394 |
"add_spmat [] bs = bs" | |
|
395 |
"add_spmat as [] = as" | |
|
396 |
"add_spmat ((i,a)#as) ((j,b)#bs) = ( |
|
397 |
if i < j then |
|
398 |
(i,a) # add_spmat as ((j,b)#bs) |
|
399 |
else if j < i then |
|
400 |
(j,b) # add_spmat ((i,a)#as) bs |
|
15009 | 401 |
else |
31816 | 402 |
(i, add_spvec a b) # add_spmat as bs)" |
15009 | 403 |
|
31816 | 404 |
lemma add_spmat_Nil2[simp]: "add_spmat as [] = as" |
405 |
by(cases as) auto |
|
406 |
||
407 |
lemma sparse_row_add_spmat: "sparse_row_matrix (add_spmat A B) = (sparse_row_matrix A) + (sparse_row_matrix B)" |
|
31817 | 408 |
apply (induct A B rule: add_spmat.induct) |
15009 | 409 |
apply (auto simp add: sparse_row_matrix_cons sparse_row_vector_add move_matrix_add) |
410 |
done |
|
411 |
||
28562 | 412 |
lemmas [code] = sparse_row_add_spmat [symmetric] |
413 |
lemmas [code] = sparse_row_vector_add [symmetric] |
|
27484 | 414 |
|
31816 | 415 |
lemma sorted_add_spvec_helper1[rule_format]: "add_spvec ((a,b)#arr) brr = (ab, bb) # list \<longrightarrow> (ab = a | (brr \<noteq> [] & ab = fst (hd brr)))" |
15009 | 416 |
proof - |
31816 | 417 |
have "(! x ab a. x = (a,b)#arr \<longrightarrow> add_spvec x brr = (ab, bb) # list \<longrightarrow> (ab = a | (ab = fst (hd brr))))" |
31817 | 418 |
by (induct brr rule: add_spvec.induct) (auto split:if_splits) |
15009 | 419 |
then show ?thesis |
420 |
by (case_tac brr, auto) |
|
421 |
qed |
|
422 |
||
31816 | 423 |
lemma sorted_add_spmat_helper1[rule_format]: "add_spmat ((a,b)#arr) brr = (ab, bb) # list \<longrightarrow> (ab = a | (brr \<noteq> [] & ab = fst (hd brr)))" |
15009 | 424 |
proof - |
31816 | 425 |
have "(! x ab a. x = (a,b)#arr \<longrightarrow> add_spmat x brr = (ab, bb) # list \<longrightarrow> (ab = a | (ab = fst (hd brr))))" |
31817 | 426 |
by (rule add_spmat.induct) (auto split:if_splits) |
15009 | 427 |
then show ?thesis |
428 |
by (case_tac brr, auto) |
|
429 |
qed |
|
430 |
||
31817 | 431 |
lemma sorted_add_spvec_helper: "add_spvec arr brr = (ab, bb) # list \<Longrightarrow> ((arr \<noteq> [] & ab = fst (hd arr)) | (brr \<noteq> [] & ab = fst (hd brr)))" |
432 |
apply (induct arr brr rule: add_spvec.induct) |
|
433 |
apply (auto split:if_splits) |
|
15009 | 434 |
done |
435 |
||
31817 | 436 |
lemma sorted_add_spmat_helper: "add_spmat arr brr = (ab, bb) # list \<Longrightarrow> ((arr \<noteq> [] & ab = fst (hd arr)) | (brr \<noteq> [] & ab = fst (hd brr)))" |
437 |
apply (induct arr brr rule: add_spmat.induct) |
|
438 |
apply (auto split:if_splits) |
|
15009 | 439 |
done |
440 |
||
31816 | 441 |
lemma add_spvec_commute: "add_spvec a b = add_spvec b a" |
31817 | 442 |
by (induct a b rule: add_spvec.induct) auto |
15009 | 443 |
|
31816 | 444 |
lemma add_spmat_commute: "add_spmat a b = add_spmat b a" |
31817 | 445 |
apply (induct a b rule: add_spmat.induct) |
15009 | 446 |
apply (simp_all add: add_spvec_commute) |
447 |
done |
|
448 |
||
31816 | 449 |
lemma sorted_add_spvec_helper2: "add_spvec ((a,b)#arr) brr = (ab, bb) # list \<Longrightarrow> aa < a \<Longrightarrow> sorted_spvec ((aa, ba) # brr) \<Longrightarrow> aa < ab" |
15009 | 450 |
apply (drule sorted_add_spvec_helper1) |
451 |
apply (auto) |
|
452 |
apply (case_tac brr) |
|
453 |
apply (simp_all) |
|
454 |
apply (drule_tac sorted_spvec_cons3) |
|
455 |
apply (simp) |
|
456 |
done |
|
457 |
||
31816 | 458 |
lemma sorted_add_spmat_helper2: "add_spmat ((a,b)#arr) brr = (ab, bb) # list \<Longrightarrow> aa < a \<Longrightarrow> sorted_spvec ((aa, ba) # brr) \<Longrightarrow> aa < ab" |
15009 | 459 |
apply (drule sorted_add_spmat_helper1) |
460 |
apply (auto) |
|
461 |
apply (case_tac brr) |
|
462 |
apply (simp_all) |
|
463 |
apply (drule_tac sorted_spvec_cons3) |
|
464 |
apply (simp) |
|
465 |
done |
|
466 |
||
31816 | 467 |
lemma sorted_spvec_add_spvec[rule_format]: "sorted_spvec a \<longrightarrow> sorted_spvec b \<longrightarrow> sorted_spvec (add_spvec a b)" |
31817 | 468 |
apply (induct a b rule: add_spvec.induct) |
15009 | 469 |
apply (simp_all) |
470 |
apply (rule conjI) |
|
31816 | 471 |
apply (clarsimp) |
15009 | 472 |
apply (frule_tac as=brr in sorted_spvec_cons1) |
473 |
apply (simp) |
|
474 |
apply (subst sorted_spvec_step) |
|
31816 | 475 |
apply (clarsimp simp: sorted_add_spvec_helper2 split: list.split) |
15009 | 476 |
apply (clarify) |
477 |
apply (rule conjI) |
|
478 |
apply (clarify) |
|
479 |
apply (frule_tac as=arr in sorted_spvec_cons1, simp) |
|
480 |
apply (subst sorted_spvec_step) |
|
31816 | 481 |
apply (clarsimp simp: sorted_add_spvec_helper2 add_spvec_commute split: list.split) |
15009 | 482 |
apply (clarify) |
483 |
apply (frule_tac as=arr in sorted_spvec_cons1) |
|
484 |
apply (frule_tac as=brr in sorted_spvec_cons1) |
|
485 |
apply (simp) |
|
486 |
apply (subst sorted_spvec_step) |
|
487 |
apply (simp split: list.split) |
|
31816 | 488 |
apply (clarsimp) |
15009 | 489 |
apply (drule_tac sorted_add_spvec_helper) |
31816 | 490 |
apply (auto simp: neq_Nil_conv) |
15009 | 491 |
apply (drule sorted_spvec_cons3) |
492 |
apply (simp) |
|
493 |
apply (drule sorted_spvec_cons3) |
|
494 |
apply (simp) |
|
495 |
done |
|
496 |
||
31816 | 497 |
lemma sorted_spvec_add_spmat[rule_format]: "sorted_spvec A \<longrightarrow> sorted_spvec B \<longrightarrow> sorted_spvec (add_spmat A B)" |
31817 | 498 |
apply (induct A B rule: add_spmat.induct) |
15009 | 499 |
apply (simp_all) |
500 |
apply (rule conjI) |
|
501 |
apply (intro strip) |
|
502 |
apply (simp) |
|
503 |
apply (frule_tac as=bs in sorted_spvec_cons1) |
|
504 |
apply (simp) |
|
505 |
apply (subst sorted_spvec_step) |
|
506 |
apply (simp split: list.split) |
|
507 |
apply (clarify, simp) |
|
508 |
apply (simp add: sorted_add_spmat_helper2) |
|
509 |
apply (clarify) |
|
510 |
apply (rule conjI) |
|
511 |
apply (clarify) |
|
512 |
apply (frule_tac as=as in sorted_spvec_cons1, simp) |
|
513 |
apply (subst sorted_spvec_step) |
|
31816 | 514 |
apply (clarsimp simp: sorted_add_spmat_helper2 add_spmat_commute split: list.split) |
515 |
apply (clarsimp) |
|
15009 | 516 |
apply (frule_tac as=as in sorted_spvec_cons1) |
517 |
apply (frule_tac as=bs in sorted_spvec_cons1) |
|
518 |
apply (simp) |
|
519 |
apply (subst sorted_spvec_step) |
|
520 |
apply (simp split: list.split) |
|
521 |
apply (clarify, simp) |
|
522 |
apply (drule_tac sorted_add_spmat_helper) |
|
31816 | 523 |
apply (auto simp:neq_Nil_conv) |
15009 | 524 |
apply (drule sorted_spvec_cons3) |
525 |
apply (simp) |
|
526 |
apply (drule sorted_spvec_cons3) |
|
527 |
apply (simp) |
|
528 |
done |
|
529 |
||
31817 | 530 |
lemma sorted_spmat_add_spmat[rule_format]: "sorted_spmat A \<Longrightarrow> sorted_spmat B \<Longrightarrow> sorted_spmat (add_spmat A B)" |
531 |
apply (induct A B rule: add_spmat.induct) |
|
15009 | 532 |
apply (simp_all add: sorted_spvec_add_spvec) |
533 |
done |
|
534 |
||
31816 | 535 |
fun le_spvec :: "('a::lordered_ab_group_add) spvec \<Rightarrow> 'a spvec \<Rightarrow> bool" where |
536 |
(* "measure (% (a,b). (length a) + (length b))" *) |
|
537 |
"le_spvec [] [] = True" | |
|
538 |
"le_spvec ((_,a)#as) [] = (a <= 0 & le_spvec as [])" | |
|
539 |
"le_spvec [] ((_,b)#bs) = (0 <= b & le_spvec [] bs)" | |
|
540 |
"le_spvec ((i,a)#as) ((j,b)#bs) = ( |
|
541 |
if (i < j) then a <= 0 & le_spvec as ((j,b)#bs) |
|
542 |
else if (j < i) then 0 <= b & le_spvec ((i,a)#as) bs |
|
543 |
else a <= b & le_spvec as bs)" |
|
15009 | 544 |
|
31816 | 545 |
fun le_spmat :: "('a::lordered_ab_group_add) spmat \<Rightarrow> 'a spmat \<Rightarrow> bool" where |
546 |
(* "measure (% (a,b). (length a) + (length b))" *) |
|
547 |
"le_spmat [] [] = True" | |
|
548 |
"le_spmat ((i,a)#as) [] = (le_spvec a [] & le_spmat as [])" | |
|
549 |
"le_spmat [] ((j,b)#bs) = (le_spvec [] b & le_spmat [] bs)" | |
|
550 |
"le_spmat ((i,a)#as) ((j,b)#bs) = ( |
|
551 |
if i < j then (le_spvec a [] & le_spmat as ((j,b)#bs)) |
|
552 |
else if j < i then (le_spvec [] b & le_spmat ((i,a)#as) bs) |
|
553 |
else (le_spvec a b & le_spmat as bs))" |
|
15009 | 554 |
|
555 |
constdefs |
|
556 |
disj_matrices :: "('a::zero) matrix \<Rightarrow> 'a matrix \<Rightarrow> bool" |
|
557 |
"disj_matrices A B == (! j i. (Rep_matrix A j i \<noteq> 0) \<longrightarrow> (Rep_matrix B j i = 0)) & (! j i. (Rep_matrix B j i \<noteq> 0) \<longrightarrow> (Rep_matrix A j i = 0))" |
|
558 |
||
24124
4399175e3014
turned simp_depth_limit into configuration option;
wenzelm
parents:
23477
diff
changeset
|
559 |
declare [[simp_depth_limit = 6]] |
15009 | 560 |
|
15580 | 561 |
lemma disj_matrices_contr1: "disj_matrices A B \<Longrightarrow> Rep_matrix A j i \<noteq> 0 \<Longrightarrow> Rep_matrix B j i = 0" |
562 |
by (simp add: disj_matrices_def) |
|
563 |
||
564 |
lemma disj_matrices_contr2: "disj_matrices A B \<Longrightarrow> Rep_matrix B j i \<noteq> 0 \<Longrightarrow> Rep_matrix A j i = 0" |
|
565 |
by (simp add: disj_matrices_def) |
|
566 |
||
567 |
||
15009 | 568 |
lemma disj_matrices_add: "disj_matrices A B \<Longrightarrow> disj_matrices C D \<Longrightarrow> disj_matrices A D \<Longrightarrow> disj_matrices B C \<Longrightarrow> |
25303
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
24124
diff
changeset
|
569 |
(A + B <= C + D) = (A <= C & B <= (D::('a::lordered_ab_group_add) matrix))" |
15009 | 570 |
apply (auto) |
571 |
apply (simp (no_asm_use) only: le_matrix_def disj_matrices_def) |
|
572 |
apply (intro strip) |
|
573 |
apply (erule conjE)+ |
|
574 |
apply (drule_tac j=j and i=i in spec2)+ |
|
575 |
apply (case_tac "Rep_matrix B j i = 0") |
|
576 |
apply (case_tac "Rep_matrix D j i = 0") |
|
577 |
apply (simp_all) |
|
578 |
apply (simp (no_asm_use) only: le_matrix_def disj_matrices_def) |
|
579 |
apply (intro strip) |
|
580 |
apply (erule conjE)+ |
|
581 |
apply (drule_tac j=j and i=i in spec2)+ |
|
582 |
apply (case_tac "Rep_matrix A j i = 0") |
|
583 |
apply (case_tac "Rep_matrix C j i = 0") |
|
584 |
apply (simp_all) |
|
585 |
apply (erule add_mono) |
|
586 |
apply (assumption) |
|
587 |
done |
|
588 |
||
589 |
lemma disj_matrices_zero1[simp]: "disj_matrices 0 B" |
|
590 |
by (simp add: disj_matrices_def) |
|
591 |
||
592 |
lemma disj_matrices_zero2[simp]: "disj_matrices A 0" |
|
593 |
by (simp add: disj_matrices_def) |
|
594 |
||
595 |
lemma disj_matrices_commute: "disj_matrices A B = disj_matrices B A" |
|
596 |
by (auto simp add: disj_matrices_def) |
|
597 |
||
598 |
lemma disj_matrices_add_le_zero: "disj_matrices A B \<Longrightarrow> |
|
25303
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
24124
diff
changeset
|
599 |
(A + B <= 0) = (A <= 0 & (B::('a::lordered_ab_group_add) matrix) <= 0)" |
15009 | 600 |
by (rule disj_matrices_add[of A B 0 0, simplified]) |
601 |
||
602 |
lemma disj_matrices_add_zero_le: "disj_matrices A B \<Longrightarrow> |
|
25303
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
24124
diff
changeset
|
603 |
(0 <= A + B) = (0 <= A & 0 <= (B::('a::lordered_ab_group_add) matrix))" |
15009 | 604 |
by (rule disj_matrices_add[of 0 0 A B, simplified]) |
605 |
||
606 |
lemma disj_matrices_add_x_le: "disj_matrices A B \<Longrightarrow> disj_matrices B C \<Longrightarrow> |
|
25303
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
24124
diff
changeset
|
607 |
(A <= B + C) = (A <= C & 0 <= (B::('a::lordered_ab_group_add) matrix))" |
15009 | 608 |
by (auto simp add: disj_matrices_add[of 0 A B C, simplified]) |
609 |
||
610 |
lemma disj_matrices_add_le_x: "disj_matrices A B \<Longrightarrow> disj_matrices B C \<Longrightarrow> |
|
25303
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
24124
diff
changeset
|
611 |
(B + A <= C) = (A <= C & (B::('a::lordered_ab_group_add) matrix) <= 0)" |
15009 | 612 |
by (auto simp add: disj_matrices_add[of B A 0 C,simplified] disj_matrices_commute) |
613 |
||
614 |
lemma disj_sparse_row_singleton: "i <= j \<Longrightarrow> sorted_spvec((j,y)#v) \<Longrightarrow> disj_matrices (sparse_row_vector v) (singleton_matrix 0 i x)" |
|
615 |
apply (simp add: disj_matrices_def) |
|
616 |
apply (rule conjI) |
|
617 |
apply (rule neg_imp) |
|
618 |
apply (simp) |
|
619 |
apply (intro strip) |
|
620 |
apply (rule sorted_sparse_row_vector_zero) |
|
621 |
apply (simp_all) |
|
622 |
apply (intro strip) |
|
623 |
apply (rule sorted_sparse_row_vector_zero) |
|
624 |
apply (simp_all) |
|
625 |
done |
|
626 |
||
25303
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
24124
diff
changeset
|
627 |
lemma disj_matrices_x_add: "disj_matrices A B \<Longrightarrow> disj_matrices A C \<Longrightarrow> disj_matrices (A::('a::lordered_ab_group_add) matrix) (B+C)" |
15009 | 628 |
apply (simp add: disj_matrices_def) |
629 |
apply (auto) |
|
630 |
apply (drule_tac j=j and i=i in spec2)+ |
|
631 |
apply (case_tac "Rep_matrix B j i = 0") |
|
632 |
apply (case_tac "Rep_matrix C j i = 0") |
|
633 |
apply (simp_all) |
|
634 |
done |
|
635 |
||
25303
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
24124
diff
changeset
|
636 |
lemma disj_matrices_add_x: "disj_matrices A B \<Longrightarrow> disj_matrices A C \<Longrightarrow> disj_matrices (B+C) (A::('a::lordered_ab_group_add) matrix)" |
15009 | 637 |
by (simp add: disj_matrices_x_add disj_matrices_commute) |
638 |
||
639 |
lemma disj_singleton_matrices[simp]: "disj_matrices (singleton_matrix j i x) (singleton_matrix u v y) = (j \<noteq> u | i \<noteq> v | x = 0 | y = 0)" |
|
640 |
by (auto simp add: disj_matrices_def) |
|
641 |
||
642 |
lemma disj_move_sparse_vec_mat[simplified disj_matrices_commute]: |
|
643 |
"j <= a \<Longrightarrow> sorted_spvec((a,c)#as) \<Longrightarrow> disj_matrices (move_matrix (sparse_row_vector b) (int j) i) (sparse_row_matrix as)" |
|
644 |
apply (auto simp add: neg_def disj_matrices_def) |
|
645 |
apply (drule nrows_notzero) |
|
646 |
apply (drule less_le_trans[OF _ nrows_spvec]) |
|
647 |
apply (subgoal_tac "ja = j") |
|
648 |
apply (simp add: sorted_sparse_row_matrix_zero) |
|
649 |
apply (arith) |
|
650 |
apply (rule nrows) |
|
651 |
apply (rule order_trans[of _ 1 _]) |
|
652 |
apply (simp) |
|
653 |
apply (case_tac "nat (int ja - int j) = 0") |
|
654 |
apply (case_tac "ja = j") |
|
655 |
apply (simp add: sorted_sparse_row_matrix_zero) |
|
656 |
apply arith+ |
|
657 |
done |
|
658 |
||
659 |
lemma disj_move_sparse_row_vector_twice: |
|
660 |
"j \<noteq> u \<Longrightarrow> disj_matrices (move_matrix (sparse_row_vector a) j i) (move_matrix (sparse_row_vector b) u v)" |
|
661 |
apply (auto simp add: neg_def disj_matrices_def) |
|
662 |
apply (rule nrows, rule order_trans[of _ 1], simp, drule nrows_notzero, drule less_le_trans[OF _ nrows_spvec], arith)+ |
|
663 |
done |
|
664 |
||
31816 | 665 |
lemma le_spvec_iff_sparse_row_le[rule_format]: "(sorted_spvec a) \<longrightarrow> (sorted_spvec b) \<longrightarrow> (le_spvec a b) = (sparse_row_vector a <= sparse_row_vector b)" |
31817 | 666 |
apply (induct a b rule: le_spvec.induct) |
15178 | 667 |
apply (simp_all add: sorted_spvec_cons1 disj_matrices_add_le_zero disj_matrices_add_zero_le |
668 |
disj_sparse_row_singleton[OF order_refl] disj_matrices_commute) |
|
669 |
apply (rule conjI, intro strip) |
|
670 |
apply (simp add: sorted_spvec_cons1) |
|
671 |
apply (subst disj_matrices_add_x_le) |
|
672 |
apply (simp add: disj_sparse_row_singleton[OF less_imp_le] disj_matrices_x_add disj_matrices_commute) |
|
673 |
apply (simp add: disj_sparse_row_singleton[OF order_refl] disj_matrices_commute) |
|
674 |
apply (simp, blast) |
|
675 |
apply (intro strip, rule conjI, intro strip) |
|
676 |
apply (simp add: sorted_spvec_cons1) |
|
677 |
apply (subst disj_matrices_add_le_x) |
|
678 |
apply (simp_all add: disj_sparse_row_singleton[OF order_refl] disj_sparse_row_singleton[OF less_imp_le] disj_matrices_commute disj_matrices_x_add) |
|
679 |
apply (blast) |
|
680 |
apply (intro strip) |
|
681 |
apply (simp add: sorted_spvec_cons1) |
|
31816 | 682 |
apply (case_tac "a=b", simp_all) |
15178 | 683 |
apply (subst disj_matrices_add) |
684 |
apply (simp_all add: disj_sparse_row_singleton[OF order_refl] disj_matrices_commute) |
|
15009 | 685 |
done |
686 |
||
31816 | 687 |
lemma le_spvec_empty2_sparse_row[rule_format]: "sorted_spvec b \<longrightarrow> le_spvec b [] = (sparse_row_vector b <= 0)" |
15009 | 688 |
apply (induct b) |
689 |
apply (simp_all add: sorted_spvec_cons1) |
|
690 |
apply (intro strip) |
|
691 |
apply (subst disj_matrices_add_le_zero) |
|
31816 | 692 |
apply (auto simp add: disj_matrices_commute disj_sparse_row_singleton[OF order_refl] sorted_spvec_cons1) |
15009 | 693 |
done |
694 |
||
31816 | 695 |
lemma le_spvec_empty1_sparse_row[rule_format]: "(sorted_spvec b) \<longrightarrow> (le_spvec [] b = (0 <= sparse_row_vector b))" |
15009 | 696 |
apply (induct b) |
697 |
apply (simp_all add: sorted_spvec_cons1) |
|
698 |
apply (intro strip) |
|
699 |
apply (subst disj_matrices_add_zero_le) |
|
31816 | 700 |
apply (auto simp add: disj_matrices_commute disj_sparse_row_singleton[OF order_refl] sorted_spvec_cons1) |
15009 | 701 |
done |
702 |
||
703 |
lemma le_spmat_iff_sparse_row_le[rule_format]: "(sorted_spvec A) \<longrightarrow> (sorted_spmat A) \<longrightarrow> (sorted_spvec B) \<longrightarrow> (sorted_spmat B) \<longrightarrow> |
|
31816 | 704 |
le_spmat A B = (sparse_row_matrix A <= sparse_row_matrix B)" |
31817 | 705 |
apply (induct A B rule: le_spmat.induct) |
15009 | 706 |
apply (simp add: sparse_row_matrix_cons disj_matrices_add_le_zero disj_matrices_add_zero_le disj_move_sparse_vec_mat[OF order_refl] |
707 |
disj_matrices_commute sorted_spvec_cons1 le_spvec_empty2_sparse_row le_spvec_empty1_sparse_row)+ |
|
708 |
apply (rule conjI, intro strip) |
|
709 |
apply (simp add: sorted_spvec_cons1) |
|
710 |
apply (subst disj_matrices_add_x_le) |
|
711 |
apply (rule disj_matrices_add_x) |
|
712 |
apply (simp add: disj_move_sparse_row_vector_twice) |
|
713 |
apply (simp add: disj_move_sparse_vec_mat[OF less_imp_le] disj_matrices_commute) |
|
714 |
apply (simp add: disj_move_sparse_vec_mat[OF order_refl] disj_matrices_commute) |
|
715 |
apply (simp, blast) |
|
716 |
apply (intro strip, rule conjI, intro strip) |
|
717 |
apply (simp add: sorted_spvec_cons1) |
|
718 |
apply (subst disj_matrices_add_le_x) |
|
719 |
apply (simp add: disj_move_sparse_vec_mat[OF order_refl]) |
|
720 |
apply (rule disj_matrices_x_add) |
|
721 |
apply (simp add: disj_move_sparse_row_vector_twice) |
|
722 |
apply (simp add: disj_move_sparse_vec_mat[OF less_imp_le] disj_matrices_commute) |
|
723 |
apply (simp, blast) |
|
724 |
apply (intro strip) |
|
31816 | 725 |
apply (case_tac "i=j") |
15009 | 726 |
apply (simp_all) |
727 |
apply (subst disj_matrices_add) |
|
728 |
apply (simp_all add: disj_matrices_commute disj_move_sparse_vec_mat[OF order_refl]) |
|
729 |
apply (simp add: sorted_spvec_cons1 le_spvec_iff_sparse_row_le) |
|
730 |
done |
|
731 |
||
24124
4399175e3014
turned simp_depth_limit into configuration option;
wenzelm
parents:
23477
diff
changeset
|
732 |
declare [[simp_depth_limit = 999]] |
15178 | 733 |
|
31817 | 734 |
primrec abs_spmat :: "('a::lordered_ring) spmat \<Rightarrow> 'a spmat" where |
735 |
"abs_spmat [] = []" | |
|
15178 | 736 |
"abs_spmat (a#as) = (fst a, abs_spvec (snd a))#(abs_spmat as)" |
737 |
||
31817 | 738 |
primrec minus_spmat :: "('a::lordered_ring) spmat \<Rightarrow> 'a spmat" where |
739 |
"minus_spmat [] = []" | |
|
15178 | 740 |
"minus_spmat (a#as) = (fst a, minus_spvec (snd a))#(minus_spmat as)" |
741 |
||
742 |
lemma sparse_row_matrix_minus: |
|
743 |
"sparse_row_matrix (minus_spmat A) = - (sparse_row_matrix A)" |
|
744 |
apply (induct A) |
|
745 |
apply (simp_all add: sparse_row_vector_minus sparse_row_matrix_cons) |
|
746 |
apply (subst Rep_matrix_inject[symmetric]) |
|
747 |
apply (rule ext)+ |
|
748 |
apply simp |
|
749 |
done |
|
15009 | 750 |
|
15178 | 751 |
lemma Rep_sparse_row_vector_zero: "x \<noteq> 0 \<Longrightarrow> Rep_matrix (sparse_row_vector v) x y = 0" |
752 |
proof - |
|
753 |
assume x:"x \<noteq> 0" |
|
754 |
have r:"nrows (sparse_row_vector v) <= Suc 0" by (rule nrows_spvec) |
|
755 |
show ?thesis |
|
756 |
apply (rule nrows) |
|
757 |
apply (subgoal_tac "Suc 0 <= x") |
|
758 |
apply (insert r) |
|
759 |
apply (simp only:) |
|
760 |
apply (insert x) |
|
761 |
apply arith |
|
762 |
done |
|
763 |
qed |
|
764 |
||
765 |
lemma sparse_row_matrix_abs: |
|
766 |
"sorted_spvec A \<Longrightarrow> sorted_spmat A \<Longrightarrow> sparse_row_matrix (abs_spmat A) = abs (sparse_row_matrix A)" |
|
767 |
apply (induct A) |
|
768 |
apply (simp_all add: sparse_row_vector_abs sparse_row_matrix_cons) |
|
769 |
apply (frule_tac sorted_spvec_cons1, simp) |
|
15580 | 770 |
apply (simplesubst Rep_matrix_inject[symmetric]) |
15178 | 771 |
apply (rule ext)+ |
772 |
apply auto |
|
773 |
apply (case_tac "x=a") |
|
774 |
apply (simp) |
|
15481 | 775 |
apply (simplesubst sorted_sparse_row_matrix_zero) |
15178 | 776 |
apply auto |
15481 | 777 |
apply (simplesubst Rep_sparse_row_vector_zero) |
15178 | 778 |
apply (simp_all add: neg_def) |
779 |
done |
|
780 |
||
781 |
lemma sorted_spvec_minus_spmat: "sorted_spvec A \<Longrightarrow> sorted_spvec (minus_spmat A)" |
|
782 |
apply (induct A) |
|
783 |
apply (simp) |
|
784 |
apply (frule sorted_spvec_cons1, simp) |
|
15236
f289e8ba2bb3
Proofs needed to be updated because induction now preserves name of
nipkow
parents:
15197
diff
changeset
|
785 |
apply (simp add: sorted_spvec.simps split:list.split_asm) |
15178 | 786 |
done |
787 |
||
788 |
lemma sorted_spvec_abs_spmat: "sorted_spvec A \<Longrightarrow> sorted_spvec (abs_spmat A)" |
|
789 |
apply (induct A) |
|
790 |
apply (simp) |
|
791 |
apply (frule sorted_spvec_cons1, simp) |
|
15236
f289e8ba2bb3
Proofs needed to be updated because induction now preserves name of
nipkow
parents:
15197
diff
changeset
|
792 |
apply (simp add: sorted_spvec.simps split:list.split_asm) |
15178 | 793 |
done |
794 |
||
795 |
lemma sorted_spmat_minus_spmat: "sorted_spmat A \<Longrightarrow> sorted_spmat (minus_spmat A)" |
|
796 |
apply (induct A) |
|
797 |
apply (simp_all add: sorted_spvec_minus_spvec) |
|
798 |
done |
|
799 |
||
800 |
lemma sorted_spmat_abs_spmat: "sorted_spmat A \<Longrightarrow> sorted_spmat (abs_spmat A)" |
|
801 |
apply (induct A) |
|
802 |
apply (simp_all add: sorted_spvec_abs_spvec) |
|
803 |
done |
|
15009 | 804 |
|
15178 | 805 |
constdefs |
806 |
diff_spmat :: "('a::lordered_ring) spmat \<Rightarrow> 'a spmat \<Rightarrow> 'a spmat" |
|
31816 | 807 |
"diff_spmat A B == add_spmat A (minus_spmat B)" |
15178 | 808 |
|
809 |
lemma sorted_spmat_diff_spmat: "sorted_spmat A \<Longrightarrow> sorted_spmat B \<Longrightarrow> sorted_spmat (diff_spmat A B)" |
|
810 |
by (simp add: diff_spmat_def sorted_spmat_minus_spmat sorted_spmat_add_spmat) |
|
811 |
||
812 |
lemma sorted_spvec_diff_spmat: "sorted_spvec A \<Longrightarrow> sorted_spvec B \<Longrightarrow> sorted_spvec (diff_spmat A B)" |
|
813 |
by (simp add: diff_spmat_def sorted_spvec_minus_spmat sorted_spvec_add_spmat) |
|
814 |
||
815 |
lemma sparse_row_diff_spmat: "sparse_row_matrix (diff_spmat A B ) = (sparse_row_matrix A) - (sparse_row_matrix B)" |
|
816 |
by (simp add: diff_spmat_def sparse_row_add_spmat sparse_row_matrix_minus) |
|
817 |
||
818 |
constdefs |
|
819 |
sorted_sparse_matrix :: "'a spmat \<Rightarrow> bool" |
|
820 |
"sorted_sparse_matrix A == (sorted_spvec A) & (sorted_spmat A)" |
|
821 |
||
822 |
lemma sorted_sparse_matrix_imp_spvec: "sorted_sparse_matrix A \<Longrightarrow> sorted_spvec A" |
|
823 |
by (simp add: sorted_sparse_matrix_def) |
|
824 |
||
825 |
lemma sorted_sparse_matrix_imp_spmat: "sorted_sparse_matrix A \<Longrightarrow> sorted_spmat A" |
|
826 |
by (simp add: sorted_sparse_matrix_def) |
|
827 |
||
828 |
lemmas sorted_sp_simps = |
|
829 |
sorted_spvec.simps |
|
830 |
sorted_spmat.simps |
|
831 |
sorted_sparse_matrix_def |
|
832 |
||
833 |
lemma bool1: "(\<not> True) = False" by blast |
|
834 |
lemma bool2: "(\<not> False) = True" by blast |
|
835 |
lemma bool3: "((P\<Colon>bool) \<and> True) = P" by blast |
|
836 |
lemma bool4: "(True \<and> (P\<Colon>bool)) = P" by blast |
|
837 |
lemma bool5: "((P\<Colon>bool) \<and> False) = False" by blast |
|
838 |
lemma bool6: "(False \<and> (P\<Colon>bool)) = False" by blast |
|
839 |
lemma bool7: "((P\<Colon>bool) \<or> True) = True" by blast |
|
840 |
lemma bool8: "(True \<or> (P\<Colon>bool)) = True" by blast |
|
841 |
lemma bool9: "((P\<Colon>bool) \<or> False) = P" by blast |
|
842 |
lemma bool10: "(False \<or> (P\<Colon>bool)) = P" by blast |
|
843 |
lemmas boolarith = bool1 bool2 bool3 bool4 bool5 bool6 bool7 bool8 bool9 bool10 |
|
844 |
||
845 |
lemma if_case_eq: "(if b then x else y) = (case b of True => x | False => y)" by simp |
|
846 |
||
15580 | 847 |
consts |
25303
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
24124
diff
changeset
|
848 |
pprt_spvec :: "('a::{lordered_ab_group_add}) spvec \<Rightarrow> 'a spvec" |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
24124
diff
changeset
|
849 |
nprt_spvec :: "('a::{lordered_ab_group_add}) spvec \<Rightarrow> 'a spvec" |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
24124
diff
changeset
|
850 |
pprt_spmat :: "('a::{lordered_ab_group_add}) spmat \<Rightarrow> 'a spmat" |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
24124
diff
changeset
|
851 |
nprt_spmat :: "('a::{lordered_ab_group_add}) spmat \<Rightarrow> 'a spmat" |
15580 | 852 |
|
853 |
primrec |
|
854 |
"pprt_spvec [] = []" |
|
855 |
"pprt_spvec (a#as) = (fst a, pprt (snd a)) # (pprt_spvec as)" |
|
856 |
||
857 |
primrec |
|
858 |
"nprt_spvec [] = []" |
|
859 |
"nprt_spvec (a#as) = (fst a, nprt (snd a)) # (nprt_spvec as)" |
|
860 |
||
861 |
primrec |
|
862 |
"pprt_spmat [] = []" |
|
863 |
"pprt_spmat (a#as) = (fst a, pprt_spvec (snd a))#(pprt_spmat as)" |
|
864 |
(*case (pprt_spvec (snd a)) of [] \<Rightarrow> (pprt_spmat as) | y#ys \<Rightarrow> (fst a, y#ys)#(pprt_spmat as))"*) |
|
865 |
||
866 |
primrec |
|
867 |
"nprt_spmat [] = []" |
|
868 |
"nprt_spmat (a#as) = (fst a, nprt_spvec (snd a))#(nprt_spmat as)" |
|
869 |
(*case (nprt_spvec (snd a)) of [] \<Rightarrow> (nprt_spmat as) | y#ys \<Rightarrow> (fst a, y#ys)#(nprt_spmat as))"*) |
|
870 |
||
871 |
||
872 |
lemma pprt_add: "disj_matrices A (B::(_::lordered_ring) matrix) \<Longrightarrow> pprt (A+B) = pprt A + pprt B" |
|
22452
8a86fd2a1bf0
adjusted to new lattice theory developement in Lattices.thy / FixedPoint.thy
haftmann
parents:
20432
diff
changeset
|
873 |
apply (simp add: pprt_def sup_matrix_def) |
15580 | 874 |
apply (simp add: Rep_matrix_inject[symmetric]) |
875 |
apply (rule ext)+ |
|
876 |
apply simp |
|
877 |
apply (case_tac "Rep_matrix A x xa \<noteq> 0") |
|
878 |
apply (simp_all add: disj_matrices_contr1) |
|
879 |
done |
|
880 |
||
881 |
lemma nprt_add: "disj_matrices A (B::(_::lordered_ring) matrix) \<Longrightarrow> nprt (A+B) = nprt A + nprt B" |
|
22452
8a86fd2a1bf0
adjusted to new lattice theory developement in Lattices.thy / FixedPoint.thy
haftmann
parents:
20432
diff
changeset
|
882 |
apply (simp add: nprt_def inf_matrix_def) |
15580 | 883 |
apply (simp add: Rep_matrix_inject[symmetric]) |
884 |
apply (rule ext)+ |
|
885 |
apply simp |
|
886 |
apply (case_tac "Rep_matrix A x xa \<noteq> 0") |
|
887 |
apply (simp_all add: disj_matrices_contr1) |
|
888 |
done |
|
889 |
||
890 |
lemma pprt_singleton[simp]: "pprt (singleton_matrix j i (x::_::lordered_ring)) = singleton_matrix j i (pprt x)" |
|
22452
8a86fd2a1bf0
adjusted to new lattice theory developement in Lattices.thy / FixedPoint.thy
haftmann
parents:
20432
diff
changeset
|
891 |
apply (simp add: pprt_def sup_matrix_def) |
15580 | 892 |
apply (simp add: Rep_matrix_inject[symmetric]) |
893 |
apply (rule ext)+ |
|
894 |
apply simp |
|
895 |
done |
|
896 |
||
897 |
lemma nprt_singleton[simp]: "nprt (singleton_matrix j i (x::_::lordered_ring)) = singleton_matrix j i (nprt x)" |
|
22452
8a86fd2a1bf0
adjusted to new lattice theory developement in Lattices.thy / FixedPoint.thy
haftmann
parents:
20432
diff
changeset
|
898 |
apply (simp add: nprt_def inf_matrix_def) |
15580 | 899 |
apply (simp add: Rep_matrix_inject[symmetric]) |
900 |
apply (rule ext)+ |
|
901 |
apply simp |
|
902 |
done |
|
903 |
||
904 |
lemma less_imp_le: "a < b \<Longrightarrow> a <= (b::_::order)" by (simp add: less_def) |
|
905 |
||
27653 | 906 |
lemma sparse_row_vector_pprt: "sorted_spvec (v :: 'a::lordered_ring spvec) \<Longrightarrow> sparse_row_vector (pprt_spvec v) = pprt (sparse_row_vector v)" |
15580 | 907 |
apply (induct v) |
908 |
apply (simp_all) |
|
909 |
apply (frule sorted_spvec_cons1, auto) |
|
910 |
apply (subst pprt_add) |
|
911 |
apply (subst disj_matrices_commute) |
|
912 |
apply (rule disj_sparse_row_singleton) |
|
913 |
apply auto |
|
914 |
done |
|
915 |
||
27653 | 916 |
lemma sparse_row_vector_nprt: "sorted_spvec (v :: 'a::lordered_ring spvec) \<Longrightarrow> sparse_row_vector (nprt_spvec v) = nprt (sparse_row_vector v)" |
15580 | 917 |
apply (induct v) |
918 |
apply (simp_all) |
|
919 |
apply (frule sorted_spvec_cons1, auto) |
|
920 |
apply (subst nprt_add) |
|
921 |
apply (subst disj_matrices_commute) |
|
922 |
apply (rule disj_sparse_row_singleton) |
|
923 |
apply auto |
|
924 |
done |
|
925 |
||
926 |
||
927 |
lemma pprt_move_matrix: "pprt (move_matrix (A::('a::lordered_ring) matrix) j i) = move_matrix (pprt A) j i" |
|
928 |
apply (simp add: pprt_def) |
|
22452
8a86fd2a1bf0
adjusted to new lattice theory developement in Lattices.thy / FixedPoint.thy
haftmann
parents:
20432
diff
changeset
|
929 |
apply (simp add: sup_matrix_def) |
15580 | 930 |
apply (simp add: Rep_matrix_inject[symmetric]) |
931 |
apply (rule ext)+ |
|
932 |
apply (simp) |
|
933 |
done |
|
934 |
||
935 |
lemma nprt_move_matrix: "nprt (move_matrix (A::('a::lordered_ring) matrix) j i) = move_matrix (nprt A) j i" |
|
936 |
apply (simp add: nprt_def) |
|
22452
8a86fd2a1bf0
adjusted to new lattice theory developement in Lattices.thy / FixedPoint.thy
haftmann
parents:
20432
diff
changeset
|
937 |
apply (simp add: inf_matrix_def) |
15580 | 938 |
apply (simp add: Rep_matrix_inject[symmetric]) |
939 |
apply (rule ext)+ |
|
940 |
apply (simp) |
|
941 |
done |
|
942 |
||
27653 | 943 |
lemma sparse_row_matrix_pprt: "sorted_spvec (m :: 'a::lordered_ring spmat) \<Longrightarrow> sorted_spmat m \<Longrightarrow> sparse_row_matrix (pprt_spmat m) = pprt (sparse_row_matrix m)" |
15580 | 944 |
apply (induct m) |
945 |
apply simp |
|
946 |
apply simp |
|
947 |
apply (frule sorted_spvec_cons1) |
|
948 |
apply (simp add: sparse_row_matrix_cons sparse_row_vector_pprt) |
|
949 |
apply (subst pprt_add) |
|
950 |
apply (subst disj_matrices_commute) |
|
951 |
apply (rule disj_move_sparse_vec_mat) |
|
952 |
apply auto |
|
953 |
apply (simp add: sorted_spvec.simps) |
|
954 |
apply (simp split: list.split) |
|
955 |
apply auto |
|
956 |
apply (simp add: pprt_move_matrix) |
|
957 |
done |
|
958 |
||
27653 | 959 |
lemma sparse_row_matrix_nprt: "sorted_spvec (m :: 'a::lordered_ring spmat) \<Longrightarrow> sorted_spmat m \<Longrightarrow> sparse_row_matrix (nprt_spmat m) = nprt (sparse_row_matrix m)" |
15580 | 960 |
apply (induct m) |
961 |
apply simp |
|
962 |
apply simp |
|
963 |
apply (frule sorted_spvec_cons1) |
|
964 |
apply (simp add: sparse_row_matrix_cons sparse_row_vector_nprt) |
|
965 |
apply (subst nprt_add) |
|
966 |
apply (subst disj_matrices_commute) |
|
967 |
apply (rule disj_move_sparse_vec_mat) |
|
968 |
apply auto |
|
969 |
apply (simp add: sorted_spvec.simps) |
|
970 |
apply (simp split: list.split) |
|
971 |
apply auto |
|
972 |
apply (simp add: nprt_move_matrix) |
|
973 |
done |
|
974 |
||
975 |
lemma sorted_pprt_spvec: "sorted_spvec v \<Longrightarrow> sorted_spvec (pprt_spvec v)" |
|
976 |
apply (induct v) |
|
977 |
apply (simp) |
|
978 |
apply (frule sorted_spvec_cons1) |
|
979 |
apply simp |
|
980 |
apply (simp add: sorted_spvec.simps split:list.split_asm) |
|
981 |
done |
|
982 |
||
983 |
lemma sorted_nprt_spvec: "sorted_spvec v \<Longrightarrow> sorted_spvec (nprt_spvec v)" |
|
984 |
apply (induct v) |
|
985 |
apply (simp) |
|
986 |
apply (frule sorted_spvec_cons1) |
|
987 |
apply simp |
|
988 |
apply (simp add: sorted_spvec.simps split:list.split_asm) |
|
989 |
done |
|
990 |
||
991 |
lemma sorted_spvec_pprt_spmat: "sorted_spvec m \<Longrightarrow> sorted_spvec (pprt_spmat m)" |
|
992 |
apply (induct m) |
|
993 |
apply (simp) |
|
994 |
apply (frule sorted_spvec_cons1) |
|
995 |
apply simp |
|
996 |
apply (simp add: sorted_spvec.simps split:list.split_asm) |
|
997 |
done |
|
998 |
||
999 |
lemma sorted_spvec_nprt_spmat: "sorted_spvec m \<Longrightarrow> sorted_spvec (nprt_spmat m)" |
|
1000 |
apply (induct m) |
|
1001 |
apply (simp) |
|
1002 |
apply (frule sorted_spvec_cons1) |
|
1003 |
apply simp |
|
1004 |
apply (simp add: sorted_spvec.simps split:list.split_asm) |
|
1005 |
done |
|
1006 |
||
1007 |
lemma sorted_spmat_pprt_spmat: "sorted_spmat m \<Longrightarrow> sorted_spmat (pprt_spmat m)" |
|
1008 |
apply (induct m) |
|
1009 |
apply (simp_all add: sorted_pprt_spvec) |
|
1010 |
done |
|
1011 |
||
1012 |
lemma sorted_spmat_nprt_spmat: "sorted_spmat m \<Longrightarrow> sorted_spmat (nprt_spmat m)" |
|
1013 |
apply (induct m) |
|
1014 |
apply (simp_all add: sorted_nprt_spvec) |
|
1015 |
done |
|
1016 |
||
1017 |
constdefs |
|
1018 |
mult_est_spmat :: "('a::lordered_ring) spmat \<Rightarrow> 'a spmat \<Rightarrow> 'a spmat \<Rightarrow> 'a spmat \<Rightarrow> 'a spmat" |
|
1019 |
"mult_est_spmat r1 r2 s1 s2 == |
|
31816 | 1020 |
add_spmat (mult_spmat (pprt_spmat s2) (pprt_spmat r2)) (add_spmat (mult_spmat (pprt_spmat s1) (nprt_spmat r2)) |
1021 |
(add_spmat (mult_spmat (nprt_spmat s2) (pprt_spmat r1)) (mult_spmat (nprt_spmat s1) (nprt_spmat r1))))" |
|
15580 | 1022 |
|
1023 |
lemmas sparse_row_matrix_op_simps = |
|
1024 |
sorted_sparse_matrix_imp_spmat sorted_sparse_matrix_imp_spvec |
|
1025 |
sparse_row_add_spmat sorted_spvec_add_spmat sorted_spmat_add_spmat |
|
1026 |
sparse_row_diff_spmat sorted_spvec_diff_spmat sorted_spmat_diff_spmat |
|
1027 |
sparse_row_matrix_minus sorted_spvec_minus_spmat sorted_spmat_minus_spmat |
|
1028 |
sparse_row_mult_spmat sorted_spvec_mult_spmat sorted_spmat_mult_spmat |
|
1029 |
sparse_row_matrix_abs sorted_spvec_abs_spmat sorted_spmat_abs_spmat |
|
1030 |
le_spmat_iff_sparse_row_le |
|
1031 |
sparse_row_matrix_pprt sorted_spvec_pprt_spmat sorted_spmat_pprt_spmat |
|
1032 |
sparse_row_matrix_nprt sorted_spvec_nprt_spmat sorted_spmat_nprt_spmat |
|
1033 |
||
1034 |
lemma zero_eq_Numeral0: "(0::_::number_ring) = Numeral0" by simp |
|
1035 |
||
1036 |
lemmas sparse_row_matrix_arith_simps[simplified zero_eq_Numeral0] = |
|
1037 |
mult_spmat.simps mult_spvec_spmat.simps |
|
1038 |
addmult_spvec.simps |
|
1039 |
smult_spvec_empty smult_spvec_cons |
|
1040 |
add_spmat.simps add_spvec.simps |
|
1041 |
minus_spmat.simps minus_spvec.simps |
|
1042 |
abs_spmat.simps abs_spvec.simps |
|
1043 |
diff_spmat_def |
|
1044 |
le_spmat.simps le_spvec.simps |
|
1045 |
pprt_spmat.simps pprt_spvec.simps |
|
1046 |
nprt_spmat.simps nprt_spvec.simps |
|
1047 |
mult_est_spmat_def |
|
1048 |
||
1049 |
||
1050 |
(*lemma spm_linprog_dual_estimate_1: |
|
15178 | 1051 |
assumes |
1052 |
"sorted_sparse_matrix A1" |
|
1053 |
"sorted_sparse_matrix A2" |
|
1054 |
"sorted_sparse_matrix c1" |
|
1055 |
"sorted_sparse_matrix c2" |
|
1056 |
"sorted_sparse_matrix y" |
|
1057 |
"sorted_spvec b" |
|
1058 |
"sorted_spvec r" |
|
1059 |
"le_spmat ([], y)" |
|
1060 |
"A * x \<le> sparse_row_matrix (b::('a::lordered_ring) spmat)" |
|
1061 |
"sparse_row_matrix A1 <= A" |
|
1062 |
"A <= sparse_row_matrix A2" |
|
1063 |
"sparse_row_matrix c1 <= c" |
|
1064 |
"c <= sparse_row_matrix c2" |
|
1065 |
"abs x \<le> sparse_row_matrix r" |
|
1066 |
shows |
|
1067 |
"c * x \<le> sparse_row_matrix (add_spmat (mult_spmat y b, mult_spmat (add_spmat (add_spmat (mult_spmat y (diff_spmat A2 A1), |
|
1068 |
abs_spmat (diff_spmat (mult_spmat y A1) c1)), diff_spmat c2 c1)) r))" |
|
1069 |
by (insert prems, simp add: sparse_row_matrix_op_simps linprog_dual_estimate_1[where A=A]) |
|
15580 | 1070 |
*) |
15009 | 1071 |
|
1072 |
end |