1 (* Title: HOL/Matrix/SparseMatrix.thy
11 'a spvec = "(nat * 'a) list"
12 'a spmat = "('a spvec) spvec"
14 definition sparse_row_vector :: "('a::ab_group_add) spvec \<Rightarrow> 'a matrix" where
15 sparse_row_vector_def: "sparse_row_vector arr = foldl (% m x. m + (singleton_matrix 0 (fst x) (snd x))) 0 arr"
17 definition sparse_row_matrix :: "('a::ab_group_add) spmat \<Rightarrow> 'a matrix" where
18 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"
20 code_datatype sparse_row_vector sparse_row_matrix
22 lemma sparse_row_vector_empty [simp]: "sparse_row_vector [] = 0"
23 by (simp add: sparse_row_vector_def)
25 lemma sparse_row_matrix_empty [simp]: "sparse_row_matrix [] = 0"
26 by (simp add: sparse_row_matrix_def)
28 lemmas [code] = sparse_row_vector_empty [symmetric]
30 lemma foldl_distrstart[rule_format]: "! a x y. (f (g x y) a = g x (f y a)) \<Longrightarrow> ! x y. (foldl f (g x y) l = g x (foldl f y l))"
33 lemma sparse_row_vector_cons[simp]:
34 "sparse_row_vector (a # arr) = (singleton_matrix 0 (fst a) (snd a)) + (sparse_row_vector arr)"
36 apply (auto simp add: sparse_row_vector_def)
37 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"])
40 lemma sparse_row_vector_append[simp]:
41 "sparse_row_vector (a @ b) = (sparse_row_vector a) + (sparse_row_vector b)"
44 lemma nrows_spvec[simp]: "nrows (sparse_row_vector x) <= (Suc 0)"
46 apply (simp_all add: add_nrows)
49 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"
51 apply (auto simp add: sparse_row_matrix_def)
52 apply (simp add: foldl_distrstart[of "\<lambda>m x. m + (move_matrix (sparse_row_vector (snd x)) (int (fst x)) 0)"
53 "% a m. (move_matrix (sparse_row_vector (snd a)) (int (fst a)) 0) + m"])
56 lemma sparse_row_matrix_append: "sparse_row_matrix (arr@brr) = (sparse_row_matrix arr) + (sparse_row_matrix brr)"
58 apply (auto simp add: sparse_row_matrix_cons)
61 primrec sorted_spvec :: "'a spvec \<Rightarrow> bool" where
62 "sorted_spvec [] = True"
63 | sorted_spvec_step: "sorted_spvec (a#as) = (case as of [] \<Rightarrow> True | b#bs \<Rightarrow> ((fst a < fst b) & (sorted_spvec as)))"
65 primrec sorted_spmat :: "'a spmat \<Rightarrow> bool" where
66 "sorted_spmat [] = True"
67 | "sorted_spmat (a#as) = ((sorted_spvec (snd a)) & (sorted_spmat as))"
69 declare sorted_spvec.simps [simp del]
71 lemma sorted_spvec_empty[simp]: "sorted_spvec [] = True"
72 by (simp add: sorted_spvec.simps)
74 lemma sorted_spvec_cons1: "sorted_spvec (a#as) \<Longrightarrow> sorted_spvec as"
76 apply (auto simp add: sorted_spvec.simps)
79 lemma sorted_spvec_cons2: "sorted_spvec (a#b#t) \<Longrightarrow> sorted_spvec (a#t)"
81 apply (auto simp add: sorted_spvec.simps)
84 lemma sorted_spvec_cons3: "sorted_spvec(a#b#t) \<Longrightarrow> fst a < fst b"
85 apply (auto simp add: sorted_spvec.simps)
88 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"
91 apply (frule sorted_spvec_cons2,simp)+
92 apply (frule sorted_spvec_cons3, simp)
95 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"
98 apply (frule sorted_spvec_cons2, simp)
99 apply (frule sorted_spvec_cons3, simp)
100 apply (simp add: sparse_row_matrix_cons neg_def)
103 primrec minus_spvec :: "('a::ab_group_add) spvec \<Rightarrow> 'a spvec" where
104 "minus_spvec [] = []"
105 | "minus_spvec (a#as) = (fst a, -(snd a))#(minus_spvec as)"
107 primrec abs_spvec :: "('a::lordered_ab_group_add_abs) spvec \<Rightarrow> 'a spvec" where
109 | "abs_spvec (a#as) = (fst a, abs (snd a))#(abs_spvec as)"
111 lemma sparse_row_vector_minus:
112 "sparse_row_vector (minus_spvec v) = - (sparse_row_vector v)"
114 apply (simp_all add: sparse_row_vector_cons)
115 apply (simp add: Rep_matrix_inject[symmetric])
120 instance matrix :: (lordered_ab_group_add_abs) lordered_ab_group_add_abs
122 unfolding abs_matrix_def .. (*FIXME move*)
124 lemma sparse_row_vector_abs:
125 "sorted_spvec (v :: 'a::lordered_ring spvec) \<Longrightarrow> sparse_row_vector (abs_spvec v) = abs (sparse_row_vector v)"
128 apply (frule_tac sorted_spvec_cons1, simp)
129 apply (simp only: Rep_matrix_inject[symmetric])
132 apply (subgoal_tac "Rep_matrix (sparse_row_vector v) 0 a = 0")
134 apply (rule sorted_sparse_row_vector_zero)
138 lemma sorted_spvec_minus_spvec:
139 "sorted_spvec v \<Longrightarrow> sorted_spvec (minus_spvec v)"
142 apply (frule sorted_spvec_cons1, simp)
143 apply (simp add: sorted_spvec.simps split:list.split_asm)
146 lemma sorted_spvec_abs_spvec:
147 "sorted_spvec v \<Longrightarrow> sorted_spvec (abs_spvec v)"
150 apply (frule sorted_spvec_cons1, simp)
151 apply (simp add: sorted_spvec.simps split:list.split_asm)
155 "smult_spvec y = map (% a. (fst a, y * snd a))"
157 lemma smult_spvec_empty[simp]: "smult_spvec y [] = []"
158 by (simp add: smult_spvec_def)
160 lemma smult_spvec_cons: "smult_spvec y (a#arr) = (fst a, y * (snd a)) # (smult_spvec y arr)"
161 by (simp add: smult_spvec_def)
163 consts addmult_spvec :: "('a::ring) * 'a spvec * 'a spvec \<Rightarrow> 'a spvec"
164 recdef addmult_spvec "measure (% (y, a, b). length a + (length b))"
165 "addmult_spvec (y, arr, []) = arr"
166 "addmult_spvec (y, [], brr) = smult_spvec y brr"
167 "addmult_spvec (y, a#arr, b#brr) = (
168 if (fst a) < (fst b) then (a#(addmult_spvec (y, arr, b#brr)))
169 else (if (fst b < fst a) then ((fst b, y * (snd b))#(addmult_spvec (y, a#arr, brr)))
170 else ((fst a, (snd a)+ y*(snd b))#(addmult_spvec (y, arr,brr)))))"
172 lemma addmult_spvec_empty1[simp]: "addmult_spvec (y, [], a) = smult_spvec y a"
175 lemma addmult_spvec_empty2[simp]: "addmult_spvec (y, a, []) = a"
178 lemma sparse_row_vector_map: "(! x y. f (x+y) = (f x) + (f y)) \<Longrightarrow> (f::'a\<Rightarrow>('a::lordered_ring)) 0 = 0 \<Longrightarrow>
179 sparse_row_vector (map (% x. (fst x, f (snd x))) a) = apply_matrix f (sparse_row_vector a)"
181 apply (simp_all add: apply_matrix_add)
184 lemma sparse_row_vector_smult: "sparse_row_vector (smult_spvec y a) = scalar_mult y (sparse_row_vector a)"
186 apply (simp_all add: smult_spvec_cons scalar_mult_add)
189 lemma sparse_row_vector_addmult_spvec: "sparse_row_vector (addmult_spvec (y::'a::lordered_ring, a, b)) =
190 (sparse_row_vector a) + (scalar_mult y (sparse_row_vector b))"
191 apply (rule addmult_spvec.induct[of _ y])
192 apply (simp add: scalar_mult_add smult_spvec_cons sparse_row_vector_smult singleton_matrix_add)+
195 lemma sorted_smult_spvec[rule_format]: "sorted_spvec a \<Longrightarrow> sorted_spvec (smult_spvec y a)"
196 apply (auto simp add: smult_spvec_def)
198 apply (auto simp add: sorted_spvec.simps split:list.split_asm)
201 lemma sorted_spvec_addmult_spvec_helper: "\<lbrakk>sorted_spvec (addmult_spvec (y, (a, b) # arr, brr)); aa < a; sorted_spvec ((a, b) # arr);
202 sorted_spvec ((aa, ba) # brr)\<rbrakk> \<Longrightarrow> sorted_spvec ((aa, y * ba) # addmult_spvec (y, (a, b) # arr, brr))"
204 apply (auto simp add: sorted_spvec.simps)
205 apply (simp split: list.split)
207 apply (simp split: list.split)
211 lemma sorted_spvec_addmult_spvec_helper2:
212 "\<lbrakk>sorted_spvec (addmult_spvec (y, arr, (aa, ba) # brr)); a < aa; sorted_spvec ((a, b) # arr); sorted_spvec ((aa, ba) # brr)\<rbrakk>
213 \<Longrightarrow> sorted_spvec ((a, b) # addmult_spvec (y, arr, (aa, ba) # brr))"
215 apply (auto simp add: smult_spvec_def sorted_spvec.simps)
216 apply (simp split: list.split)
220 lemma sorted_spvec_addmult_spvec_helper3[rule_format]:
221 "sorted_spvec (addmult_spvec (y, arr, brr)) \<longrightarrow> sorted_spvec ((aa, b) # arr) \<longrightarrow> sorted_spvec ((aa, ba) # brr)
222 \<longrightarrow> sorted_spvec ((aa, b + y * ba) # (addmult_spvec (y, arr, brr)))"
223 apply (rule addmult_spvec.induct[of _ y arr brr])
224 apply (simp_all add: sorted_spvec.simps smult_spvec_def)
227 lemma sorted_addmult_spvec[rule_format]: "sorted_spvec a \<longrightarrow> sorted_spvec b \<longrightarrow> sorted_spvec (addmult_spvec (y, a, b))"
228 apply (rule addmult_spvec.induct[of _ y a b])
229 apply (simp_all add: sorted_smult_spvec)
230 apply (rule conjI, intro strip)
231 apply (case_tac "~(a < aa)")
233 apply (frule_tac as=brr in sorted_spvec_cons1)
234 apply (simp add: sorted_spvec_addmult_spvec_helper)
235 apply (intro strip | rule conjI)+
236 apply (frule_tac as=arr in sorted_spvec_cons1)
237 apply (simp add: sorted_spvec_addmult_spvec_helper2)
239 apply (frule_tac as=arr in sorted_spvec_cons1)
240 apply (frule_tac as=brr in sorted_spvec_cons1)
242 apply (simp_all add: sorted_spvec_addmult_spvec_helper3)
246 mult_spvec_spmat :: "('a::lordered_ring) spvec * 'a spvec * 'a spmat \<Rightarrow> 'a spvec"
247 recdef mult_spvec_spmat "measure (% (c, arr, brr). (length arr) + (length brr))"
248 "mult_spvec_spmat (c, [], brr) = c"
249 "mult_spvec_spmat (c, arr, []) = c"
250 "mult_spvec_spmat (c, a#arr, b#brr) = (
251 if ((fst a) < (fst b)) then (mult_spvec_spmat (c, arr, b#brr))
252 else (if ((fst b) < (fst a)) then (mult_spvec_spmat (c, a#arr, brr))
253 else (mult_spvec_spmat (addmult_spvec (snd a, c, snd b), arr, brr))))"
255 lemma sparse_row_mult_spvec_spmat[rule_format]: "sorted_spvec (a::('a::lordered_ring) spvec) \<longrightarrow> sorted_spvec B \<longrightarrow>
256 sparse_row_vector (mult_spvec_spmat (c, a, B)) = (sparse_row_vector c) + (sparse_row_vector a) * (sparse_row_matrix B)"
258 have comp_1: "!! a b. a < b \<Longrightarrow> Suc 0 <= nat ((int b)-(int a))" by arith
259 have not_iff: "!! a b. a = b \<Longrightarrow> (~ a) = (~ b)" by simp
260 have max_helper: "!! a b. ~ (a <= max (Suc a) b) \<Longrightarrow> False"
265 assume a:"a < nrows(sparse_row_vector v)"
266 have b:"nrows(sparse_row_vector v) <= 1" by simp
267 note dummy = less_le_trans[of a "nrows (sparse_row_vector v)" 1, OF a b]
268 then have "a = 0" by simp
270 note nrows_helper = this
272 apply (rule mult_spvec_spmat.induct)
276 apply (frule_tac as=brr in sorted_spvec_cons1)
277 apply (simp add: ring_simps sparse_row_matrix_cons)
278 apply (simplesubst Rep_matrix_zero_imp_mult_zero)
284 apply (rule order_trans[of _ 1])
285 apply (simp add: comp_1)+
286 apply (subst Rep_matrix_zero_imp_mult_zero)
288 apply (case_tac "k <= aa")
289 apply (rule_tac m1 = k and n1 = a and a1 = b in ssubst[OF sorted_sparse_row_vector_zero])
294 apply (rule order_trans[of _ 1])
295 apply (simp_all add: comp_1)
297 apply (intro strip | rule conjI)+
298 apply (frule_tac as=arr in sorted_spvec_cons1)
299 apply (simp add: ring_simps)
300 apply (subst Rep_matrix_zero_imp_mult_zero)
304 apply (simp add: sparse_row_matrix_cons neg_def)
305 apply (case_tac "a <= aa")
306 apply (erule sorted_sparse_row_matrix_zero)
309 apply (case_tac "a=aa")
311 apply (frule_tac as=arr in sorted_spvec_cons1)
312 apply (frule_tac as=brr in sorted_spvec_cons1)
313 apply (simp add: sparse_row_matrix_cons ring_simps sparse_row_vector_addmult_spvec)
314 apply (rule_tac B1 = "sparse_row_matrix brr" in ssubst[OF Rep_matrix_zero_imp_mult_zero])
316 apply (rule sorted_sparse_row_matrix_zero)
318 apply (rule_tac A1 = "sparse_row_vector arr" in ssubst[OF Rep_matrix_zero_imp_mult_zero])
320 apply (rule_tac m=k and n = aa and a = b and arr=arr in sorted_sparse_row_vector_zero)
322 apply (simp add: neg_def)
323 apply (drule nrows_notzero)
324 apply (drule nrows_helper)
327 apply (subst Rep_matrix_inject[symmetric])
330 apply (subst Rep_matrix_mult)
331 apply (rule_tac j1=aa in ssubst[OF foldseq_almostzero])
333 apply (intro strip, rule conjI)
335 apply (drule_tac max_helper)
338 apply (rule zero_imp_mult_zero)
341 apply (rule order_trans[of _ 1])
347 lemma sorted_mult_spvec_spmat[rule_format]:
348 "sorted_spvec (c::('a::lordered_ring) spvec) \<longrightarrow> sorted_spmat B \<longrightarrow> sorted_spvec (mult_spvec_spmat (c, a, B))"
349 apply (rule mult_spvec_spmat.induct[of _ c a B])
350 apply (simp_all add: sorted_addmult_spvec)
354 mult_spmat :: "('a::lordered_ring) spmat \<Rightarrow> 'a spmat \<Rightarrow> 'a spmat"
357 "mult_spmat [] A = []"
358 "mult_spmat (a#as) A = (fst a, mult_spvec_spmat ([], snd a, A))#(mult_spmat as A)"
360 lemma sparse_row_mult_spmat[rule_format]:
361 "sorted_spmat A \<longrightarrow> sorted_spvec B \<longrightarrow> sparse_row_matrix (mult_spmat A B) = (sparse_row_matrix A) * (sparse_row_matrix B)"
363 apply (auto simp add: sparse_row_matrix_cons sparse_row_mult_spvec_spmat ring_simps move_matrix_mult)
366 lemma sorted_spvec_mult_spmat[rule_format]:
367 "sorted_spvec (A::('a::lordered_ring) spmat) \<longrightarrow> sorted_spvec (mult_spmat A B)"
370 apply (drule sorted_spvec_cons1, simp)
372 apply (auto simp add: sorted_spvec.simps)
375 lemma sorted_spmat_mult_spmat[rule_format]:
376 "sorted_spmat (B::('a::lordered_ring) spmat) \<longrightarrow> sorted_spmat (mult_spmat A B)"
378 apply (auto simp add: sorted_mult_spvec_spmat)
382 add_spvec :: "('a::lordered_ab_group_add) spvec * 'a spvec \<Rightarrow> 'a spvec"
383 add_spmat :: "('a::lordered_ab_group_add) spmat * 'a spmat \<Rightarrow> 'a spmat"
385 recdef add_spvec "measure (% (a, b). length a + (length b))"
386 "add_spvec (arr, []) = arr"
387 "add_spvec ([], brr) = brr"
388 "add_spvec (a#arr, b#brr) = (
389 if (fst a) < (fst b) then (a#(add_spvec (arr, b#brr)))
390 else (if (fst b < fst a) then (b#(add_spvec (a#arr, brr)))
391 else ((fst a, (snd a)+(snd b))#(add_spvec (arr,brr)))))"
393 lemma add_spvec_empty1[simp]: "add_spvec ([], a) = a"
396 lemma add_spvec_empty2[simp]: "add_spvec (a, []) = a"
399 lemma sparse_row_vector_add: "sparse_row_vector (add_spvec (a,b)) = (sparse_row_vector a) + (sparse_row_vector b)"
400 apply (rule add_spvec.induct[of _ a b])
401 apply (simp_all add: singleton_matrix_add)
404 recdef add_spmat "measure (% (A,B). (length A)+(length B))"
405 "add_spmat ([], bs) = bs"
406 "add_spmat (as, []) = as"
407 "add_spmat (a#as, b#bs) = (
408 if fst a < fst b then
409 (a#(add_spmat (as, b#bs)))
410 else (if fst b < fst a then
411 (b#(add_spmat (a#as, bs)))
413 ((fst a, add_spvec (snd a, snd b))#(add_spmat (as, bs)))))"
415 lemma sparse_row_add_spmat: "sparse_row_matrix (add_spmat (A, B)) = (sparse_row_matrix A) + (sparse_row_matrix B)"
416 apply (rule add_spmat.induct)
417 apply (auto simp add: sparse_row_matrix_cons sparse_row_vector_add move_matrix_add)
420 lemmas [code] = sparse_row_add_spmat [symmetric]
421 lemmas [code] = sparse_row_vector_add [symmetric]
423 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)))"
425 have "(! x ab a. x = (a,b)#arr \<longrightarrow> add_spvec (x, brr) = (ab, bb) # list \<longrightarrow> (ab = a | (ab = fst (hd brr))))"
426 by (rule add_spvec.induct[of _ _ brr], auto)
428 by (case_tac brr, auto)
431 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)))"
433 have "(! x ab a. x = (a,b)#arr \<longrightarrow> add_spmat (x, brr) = (ab, bb) # list \<longrightarrow> (ab = a | (ab = fst (hd brr))))"
434 by (rule add_spmat.induct[of _ _ brr], auto)
436 by (case_tac brr, auto)
439 lemma sorted_add_spvec_helper[rule_format]: "add_spvec (arr, brr) = (ab, bb) # list \<longrightarrow> ((arr \<noteq> [] & ab = fst (hd arr)) | (brr \<noteq> [] & ab = fst (hd brr)))"
440 apply (rule add_spvec.induct[of _ arr brr])
444 lemma sorted_add_spmat_helper[rule_format]: "add_spmat (arr, brr) = (ab, bb) # list \<longrightarrow> ((arr \<noteq> [] & ab = fst (hd arr)) | (brr \<noteq> [] & ab = fst (hd brr)))"
445 apply (rule add_spmat.induct[of _ arr brr])
449 lemma add_spvec_commute: "add_spvec (a, b) = add_spvec (b, a)"
450 by (rule add_spvec.induct[of _ a b], auto)
452 lemma add_spmat_commute: "add_spmat (a, b) = add_spmat (b, a)"
453 apply (rule add_spmat.induct[of _ a b])
454 apply (simp_all add: add_spvec_commute)
457 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"
458 apply (drule sorted_add_spvec_helper1)
462 apply (drule_tac sorted_spvec_cons3)
466 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"
467 apply (drule sorted_add_spmat_helper1)
471 apply (drule_tac sorted_spvec_cons3)
475 lemma sorted_spvec_add_spvec[rule_format]: "sorted_spvec a \<longrightarrow> sorted_spvec b \<longrightarrow> sorted_spvec (add_spvec (a, b))"
476 apply (rule add_spvec.induct[of _ a b])
481 apply (frule_tac as=brr in sorted_spvec_cons1)
483 apply (subst sorted_spvec_step)
484 apply (simp split: list.split)
485 apply (clarify, simp)
486 apply (simp add: sorted_add_spvec_helper2)
489 apply (case_tac "a=aa")
492 apply (frule_tac as=arr in sorted_spvec_cons1, simp)
493 apply (subst sorted_spvec_step)
494 apply (simp split: list.split)
495 apply (clarify, simp)
496 apply (simp add: sorted_add_spvec_helper2 add_spvec_commute)
497 apply (case_tac "a=aa")
500 apply (frule_tac as=arr in sorted_spvec_cons1)
501 apply (frule_tac as=brr in sorted_spvec_cons1)
503 apply (subst sorted_spvec_step)
504 apply (simp split: list.split)
505 apply (clarify, simp)
506 apply (drule_tac sorted_add_spvec_helper)
510 apply (drule sorted_spvec_cons3)
514 apply (drule sorted_spvec_cons3)
518 lemma sorted_spvec_add_spmat[rule_format]: "sorted_spvec A \<longrightarrow> sorted_spvec B \<longrightarrow> sorted_spvec (add_spmat (A, B))"
519 apply (rule add_spmat.induct[of _ A B])
524 apply (frule_tac as=bs in sorted_spvec_cons1)
526 apply (subst sorted_spvec_step)
527 apply (simp split: list.split)
528 apply (clarify, simp)
529 apply (simp add: sorted_add_spmat_helper2)
532 apply (case_tac "a=aa")
535 apply (frule_tac as=as in sorted_spvec_cons1, simp)
536 apply (subst sorted_spvec_step)
537 apply (simp split: list.split)
538 apply (clarify, simp)
539 apply (simp add: sorted_add_spmat_helper2 add_spmat_commute)
540 apply (case_tac "a=aa")
543 apply (frule_tac as=as in sorted_spvec_cons1)
544 apply (frule_tac as=bs in sorted_spvec_cons1)
546 apply (subst sorted_spvec_step)
547 apply (simp split: list.split)
548 apply (clarify, simp)
549 apply (drule_tac sorted_add_spmat_helper)
553 apply (drule sorted_spvec_cons3)
557 apply (drule sorted_spvec_cons3)
561 lemma sorted_spmat_add_spmat[rule_format]: "sorted_spmat A \<longrightarrow> sorted_spmat B \<longrightarrow> sorted_spmat (add_spmat (A, B))"
562 apply (rule add_spmat.induct[of _ A B])
563 apply (simp_all add: sorted_spvec_add_spvec)
567 le_spvec :: "('a::lordered_ab_group_add) spvec * 'a spvec \<Rightarrow> bool"
568 le_spmat :: "('a::lordered_ab_group_add) spmat * 'a spmat \<Rightarrow> bool"
570 recdef le_spvec "measure (% (a,b). (length a) + (length b))"
571 "le_spvec ([], []) = True"
572 "le_spvec (a#as, []) = ((snd a <= 0) & (le_spvec (as, [])))"
573 "le_spvec ([], b#bs) = ((0 <= snd b) & (le_spvec ([], bs)))"
574 "le_spvec (a#as, b#bs) = (
575 if (fst a < fst b) then
576 ((snd a <= 0) & (le_spvec (as, b#bs)))
577 else (if (fst b < fst a) then
578 ((0 <= snd b) & (le_spvec (a#as, bs)))
580 ((snd a <= snd b) & (le_spvec (as, bs)))))"
582 recdef le_spmat "measure (% (a,b). (length a) + (length b))"
583 "le_spmat ([], []) = True"
584 "le_spmat (a#as, []) = (le_spvec (snd a, []) & (le_spmat (as, [])))"
585 "le_spmat ([], b#bs) = (le_spvec ([], snd b) & (le_spmat ([], bs)))"
586 "le_spmat (a#as, b#bs) = (
587 if fst a < fst b then
588 (le_spvec(snd a,[]) & le_spmat(as, b#bs))
589 else (if (fst b < fst a) then
590 (le_spvec([], snd b) & le_spmat(a#as, bs))
592 (le_spvec(snd a, snd b) & le_spmat (as, bs))))"
595 disj_matrices :: "('a::zero) matrix \<Rightarrow> 'a matrix \<Rightarrow> bool"
596 "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))"
598 declare [[simp_depth_limit = 6]]
600 lemma disj_matrices_contr1: "disj_matrices A B \<Longrightarrow> Rep_matrix A j i \<noteq> 0 \<Longrightarrow> Rep_matrix B j i = 0"
601 by (simp add: disj_matrices_def)
603 lemma disj_matrices_contr2: "disj_matrices A B \<Longrightarrow> Rep_matrix B j i \<noteq> 0 \<Longrightarrow> Rep_matrix A j i = 0"
604 by (simp add: disj_matrices_def)
607 lemma disj_matrices_add: "disj_matrices A B \<Longrightarrow> disj_matrices C D \<Longrightarrow> disj_matrices A D \<Longrightarrow> disj_matrices B C \<Longrightarrow>
608 (A + B <= C + D) = (A <= C & B <= (D::('a::lordered_ab_group_add) matrix))"
610 apply (simp (no_asm_use) only: le_matrix_def disj_matrices_def)
613 apply (drule_tac j=j and i=i in spec2)+
614 apply (case_tac "Rep_matrix B j i = 0")
615 apply (case_tac "Rep_matrix D j i = 0")
617 apply (simp (no_asm_use) only: le_matrix_def disj_matrices_def)
620 apply (drule_tac j=j and i=i in spec2)+
621 apply (case_tac "Rep_matrix A j i = 0")
622 apply (case_tac "Rep_matrix C j i = 0")
624 apply (erule add_mono)
628 lemma disj_matrices_zero1[simp]: "disj_matrices 0 B"
629 by (simp add: disj_matrices_def)
631 lemma disj_matrices_zero2[simp]: "disj_matrices A 0"
632 by (simp add: disj_matrices_def)
634 lemma disj_matrices_commute: "disj_matrices A B = disj_matrices B A"
635 by (auto simp add: disj_matrices_def)
637 lemma disj_matrices_add_le_zero: "disj_matrices A B \<Longrightarrow>
638 (A + B <= 0) = (A <= 0 & (B::('a::lordered_ab_group_add) matrix) <= 0)"
639 by (rule disj_matrices_add[of A B 0 0, simplified])
641 lemma disj_matrices_add_zero_le: "disj_matrices A B \<Longrightarrow>
642 (0 <= A + B) = (0 <= A & 0 <= (B::('a::lordered_ab_group_add) matrix))"
643 by (rule disj_matrices_add[of 0 0 A B, simplified])
645 lemma disj_matrices_add_x_le: "disj_matrices A B \<Longrightarrow> disj_matrices B C \<Longrightarrow>
646 (A <= B + C) = (A <= C & 0 <= (B::('a::lordered_ab_group_add) matrix))"
647 by (auto simp add: disj_matrices_add[of 0 A B C, simplified])
649 lemma disj_matrices_add_le_x: "disj_matrices A B \<Longrightarrow> disj_matrices B C \<Longrightarrow>
650 (B + A <= C) = (A <= C & (B::('a::lordered_ab_group_add) matrix) <= 0)"
651 by (auto simp add: disj_matrices_add[of B A 0 C,simplified] disj_matrices_commute)
653 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)"
654 apply (simp add: disj_matrices_def)
659 apply (rule sorted_sparse_row_vector_zero)
662 apply (rule sorted_sparse_row_vector_zero)
666 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)"
667 apply (simp add: disj_matrices_def)
669 apply (drule_tac j=j and i=i in spec2)+
670 apply (case_tac "Rep_matrix B j i = 0")
671 apply (case_tac "Rep_matrix C j i = 0")
675 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)"
676 by (simp add: disj_matrices_x_add disj_matrices_commute)
678 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)"
679 by (auto simp add: disj_matrices_def)
681 lemma disj_move_sparse_vec_mat[simplified disj_matrices_commute]:
682 "j <= a \<Longrightarrow> sorted_spvec((a,c)#as) \<Longrightarrow> disj_matrices (move_matrix (sparse_row_vector b) (int j) i) (sparse_row_matrix as)"
683 apply (auto simp add: neg_def disj_matrices_def)
684 apply (drule nrows_notzero)
685 apply (drule less_le_trans[OF _ nrows_spvec])
686 apply (subgoal_tac "ja = j")
687 apply (simp add: sorted_sparse_row_matrix_zero)
690 apply (rule order_trans[of _ 1 _])
692 apply (case_tac "nat (int ja - int j) = 0")
693 apply (case_tac "ja = j")
694 apply (simp add: sorted_sparse_row_matrix_zero)
698 lemma disj_move_sparse_row_vector_twice:
699 "j \<noteq> u \<Longrightarrow> disj_matrices (move_matrix (sparse_row_vector a) j i) (move_matrix (sparse_row_vector b) u v)"
700 apply (auto simp add: neg_def disj_matrices_def)
701 apply (rule nrows, rule order_trans[of _ 1], simp, drule nrows_notzero, drule less_le_trans[OF _ nrows_spvec], arith)+
704 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)"
705 apply (rule le_spvec.induct)
706 apply (simp_all add: sorted_spvec_cons1 disj_matrices_add_le_zero disj_matrices_add_zero_le
707 disj_sparse_row_singleton[OF order_refl] disj_matrices_commute)
708 apply (rule conjI, intro strip)
709 apply (simp add: sorted_spvec_cons1)
710 apply (subst disj_matrices_add_x_le)
711 apply (simp add: disj_sparse_row_singleton[OF less_imp_le] disj_matrices_x_add disj_matrices_commute)
712 apply (simp add: disj_sparse_row_singleton[OF order_refl] disj_matrices_commute)
714 apply (intro strip, rule conjI, intro strip)
715 apply (simp add: sorted_spvec_cons1)
716 apply (subst disj_matrices_add_le_x)
717 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)
720 apply (simp add: sorted_spvec_cons1)
721 apply (case_tac "a=aa", simp_all)
722 apply (subst disj_matrices_add)
723 apply (simp_all add: disj_sparse_row_singleton[OF order_refl] disj_matrices_commute)
726 lemma le_spvec_empty2_sparse_row[rule_format]: "(sorted_spvec b) \<longrightarrow> (le_spvec (b,[]) = (sparse_row_vector b <= 0))"
728 apply (simp_all add: sorted_spvec_cons1)
730 apply (subst disj_matrices_add_le_zero)
731 apply (simp add: disj_matrices_commute disj_sparse_row_singleton sorted_spvec_cons1)
732 apply (rule_tac y = "snd a" in disj_sparse_row_singleton[OF order_refl])
736 lemma le_spvec_empty1_sparse_row[rule_format]: "(sorted_spvec b) \<longrightarrow> (le_spvec ([],b) = (0 <= sparse_row_vector b))"
738 apply (simp_all add: sorted_spvec_cons1)
740 apply (subst disj_matrices_add_zero_le)
741 apply (simp add: disj_matrices_commute disj_sparse_row_singleton sorted_spvec_cons1)
742 apply (rule_tac y = "snd a" in disj_sparse_row_singleton[OF order_refl])
746 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>
747 le_spmat(A, B) = (sparse_row_matrix A <= sparse_row_matrix B)"
748 apply (rule le_spmat.induct)
749 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]
750 disj_matrices_commute sorted_spvec_cons1 le_spvec_empty2_sparse_row le_spvec_empty1_sparse_row)+
751 apply (rule conjI, intro strip)
752 apply (simp add: sorted_spvec_cons1)
753 apply (subst disj_matrices_add_x_le)
754 apply (rule disj_matrices_add_x)
755 apply (simp add: disj_move_sparse_row_vector_twice)
756 apply (simp add: disj_move_sparse_vec_mat[OF less_imp_le] disj_matrices_commute)
757 apply (simp add: disj_move_sparse_vec_mat[OF order_refl] disj_matrices_commute)
759 apply (intro strip, rule conjI, intro strip)
760 apply (simp add: sorted_spvec_cons1)
761 apply (subst disj_matrices_add_le_x)
762 apply (simp add: disj_move_sparse_vec_mat[OF order_refl])
763 apply (rule disj_matrices_x_add)
764 apply (simp add: disj_move_sparse_row_vector_twice)
765 apply (simp add: disj_move_sparse_vec_mat[OF less_imp_le] disj_matrices_commute)
768 apply (case_tac "a=aa")
770 apply (subst disj_matrices_add)
771 apply (simp_all add: disj_matrices_commute disj_move_sparse_vec_mat[OF order_refl])
772 apply (simp add: sorted_spvec_cons1 le_spvec_iff_sparse_row_le)
775 declare [[simp_depth_limit = 999]]
778 abs_spmat :: "('a::lordered_ring) spmat \<Rightarrow> 'a spmat"
779 minus_spmat :: "('a::lordered_ring) spmat \<Rightarrow> 'a spmat"
783 "abs_spmat (a#as) = (fst a, abs_spvec (snd a))#(abs_spmat as)"
786 "minus_spmat [] = []"
787 "minus_spmat (a#as) = (fst a, minus_spvec (snd a))#(minus_spmat as)"
789 lemma sparse_row_matrix_minus:
790 "sparse_row_matrix (minus_spmat A) = - (sparse_row_matrix A)"
792 apply (simp_all add: sparse_row_vector_minus sparse_row_matrix_cons)
793 apply (subst Rep_matrix_inject[symmetric])
798 lemma Rep_sparse_row_vector_zero: "x \<noteq> 0 \<Longrightarrow> Rep_matrix (sparse_row_vector v) x y = 0"
800 assume x:"x \<noteq> 0"
801 have r:"nrows (sparse_row_vector v) <= Suc 0" by (rule nrows_spvec)
804 apply (subgoal_tac "Suc 0 <= x")
812 lemma sparse_row_matrix_abs:
813 "sorted_spvec A \<Longrightarrow> sorted_spmat A \<Longrightarrow> sparse_row_matrix (abs_spmat A) = abs (sparse_row_matrix A)"
815 apply (simp_all add: sparse_row_vector_abs sparse_row_matrix_cons)
816 apply (frule_tac sorted_spvec_cons1, simp)
817 apply (simplesubst Rep_matrix_inject[symmetric])
820 apply (case_tac "x=a")
822 apply (simplesubst sorted_sparse_row_matrix_zero)
824 apply (simplesubst Rep_sparse_row_vector_zero)
825 apply (simp_all add: neg_def)
828 lemma sorted_spvec_minus_spmat: "sorted_spvec A \<Longrightarrow> sorted_spvec (minus_spmat A)"
831 apply (frule sorted_spvec_cons1, simp)
832 apply (simp add: sorted_spvec.simps split:list.split_asm)
835 lemma sorted_spvec_abs_spmat: "sorted_spvec A \<Longrightarrow> sorted_spvec (abs_spmat A)"
838 apply (frule sorted_spvec_cons1, simp)
839 apply (simp add: sorted_spvec.simps split:list.split_asm)
842 lemma sorted_spmat_minus_spmat: "sorted_spmat A \<Longrightarrow> sorted_spmat (minus_spmat A)"
844 apply (simp_all add: sorted_spvec_minus_spvec)
847 lemma sorted_spmat_abs_spmat: "sorted_spmat A \<Longrightarrow> sorted_spmat (abs_spmat A)"
849 apply (simp_all add: sorted_spvec_abs_spvec)
853 diff_spmat :: "('a::lordered_ring) spmat \<Rightarrow> 'a spmat \<Rightarrow> 'a spmat"
854 "diff_spmat A B == add_spmat (A, minus_spmat B)"
856 lemma sorted_spmat_diff_spmat: "sorted_spmat A \<Longrightarrow> sorted_spmat B \<Longrightarrow> sorted_spmat (diff_spmat A B)"
857 by (simp add: diff_spmat_def sorted_spmat_minus_spmat sorted_spmat_add_spmat)
859 lemma sorted_spvec_diff_spmat: "sorted_spvec A \<Longrightarrow> sorted_spvec B \<Longrightarrow> sorted_spvec (diff_spmat A B)"
860 by (simp add: diff_spmat_def sorted_spvec_minus_spmat sorted_spvec_add_spmat)
862 lemma sparse_row_diff_spmat: "sparse_row_matrix (diff_spmat A B ) = (sparse_row_matrix A) - (sparse_row_matrix B)"
863 by (simp add: diff_spmat_def sparse_row_add_spmat sparse_row_matrix_minus)
866 sorted_sparse_matrix :: "'a spmat \<Rightarrow> bool"
867 "sorted_sparse_matrix A == (sorted_spvec A) & (sorted_spmat A)"
869 lemma sorted_sparse_matrix_imp_spvec: "sorted_sparse_matrix A \<Longrightarrow> sorted_spvec A"
870 by (simp add: sorted_sparse_matrix_def)
872 lemma sorted_sparse_matrix_imp_spmat: "sorted_sparse_matrix A \<Longrightarrow> sorted_spmat A"
873 by (simp add: sorted_sparse_matrix_def)
875 lemmas sorted_sp_simps =
878 sorted_sparse_matrix_def
880 lemma bool1: "(\<not> True) = False" by blast
881 lemma bool2: "(\<not> False) = True" by blast
882 lemma bool3: "((P\<Colon>bool) \<and> True) = P" by blast
883 lemma bool4: "(True \<and> (P\<Colon>bool)) = P" by blast
884 lemma bool5: "((P\<Colon>bool) \<and> False) = False" by blast
885 lemma bool6: "(False \<and> (P\<Colon>bool)) = False" by blast
886 lemma bool7: "((P\<Colon>bool) \<or> True) = True" by blast
887 lemma bool8: "(True \<or> (P\<Colon>bool)) = True" by blast
888 lemma bool9: "((P\<Colon>bool) \<or> False) = P" by blast
889 lemma bool10: "(False \<or> (P\<Colon>bool)) = P" by blast
890 lemmas boolarith = bool1 bool2 bool3 bool4 bool5 bool6 bool7 bool8 bool9 bool10
892 lemma if_case_eq: "(if b then x else y) = (case b of True => x | False => y)" by simp
895 pprt_spvec :: "('a::{lordered_ab_group_add}) spvec \<Rightarrow> 'a spvec"
896 nprt_spvec :: "('a::{lordered_ab_group_add}) spvec \<Rightarrow> 'a spvec"
897 pprt_spmat :: "('a::{lordered_ab_group_add}) spmat \<Rightarrow> 'a spmat"
898 nprt_spmat :: "('a::{lordered_ab_group_add}) spmat \<Rightarrow> 'a spmat"
902 "pprt_spvec (a#as) = (fst a, pprt (snd a)) # (pprt_spvec as)"
906 "nprt_spvec (a#as) = (fst a, nprt (snd a)) # (nprt_spvec as)"
910 "pprt_spmat (a#as) = (fst a, pprt_spvec (snd a))#(pprt_spmat as)"
911 (*case (pprt_spvec (snd a)) of [] \<Rightarrow> (pprt_spmat as) | y#ys \<Rightarrow> (fst a, y#ys)#(pprt_spmat as))"*)
915 "nprt_spmat (a#as) = (fst a, nprt_spvec (snd a))#(nprt_spmat as)"
916 (*case (nprt_spvec (snd a)) of [] \<Rightarrow> (nprt_spmat as) | y#ys \<Rightarrow> (fst a, y#ys)#(nprt_spmat as))"*)
919 lemma pprt_add: "disj_matrices A (B::(_::lordered_ring) matrix) \<Longrightarrow> pprt (A+B) = pprt A + pprt B"
920 apply (simp add: pprt_def sup_matrix_def)
921 apply (simp add: Rep_matrix_inject[symmetric])
924 apply (case_tac "Rep_matrix A x xa \<noteq> 0")
925 apply (simp_all add: disj_matrices_contr1)
928 lemma nprt_add: "disj_matrices A (B::(_::lordered_ring) matrix) \<Longrightarrow> nprt (A+B) = nprt A + nprt B"
929 apply (simp add: nprt_def inf_matrix_def)
930 apply (simp add: Rep_matrix_inject[symmetric])
933 apply (case_tac "Rep_matrix A x xa \<noteq> 0")
934 apply (simp_all add: disj_matrices_contr1)
937 lemma pprt_singleton[simp]: "pprt (singleton_matrix j i (x::_::lordered_ring)) = singleton_matrix j i (pprt x)"
938 apply (simp add: pprt_def sup_matrix_def)
939 apply (simp add: Rep_matrix_inject[symmetric])
944 lemma nprt_singleton[simp]: "nprt (singleton_matrix j i (x::_::lordered_ring)) = singleton_matrix j i (nprt x)"
945 apply (simp add: nprt_def inf_matrix_def)
946 apply (simp add: Rep_matrix_inject[symmetric])
951 lemma less_imp_le: "a < b \<Longrightarrow> a <= (b::_::order)" by (simp add: less_def)
953 lemma sparse_row_vector_pprt: "sorted_spvec (v :: 'a::lordered_ring spvec) \<Longrightarrow> sparse_row_vector (pprt_spvec v) = pprt (sparse_row_vector v)"
956 apply (frule sorted_spvec_cons1, auto)
957 apply (subst pprt_add)
958 apply (subst disj_matrices_commute)
959 apply (rule disj_sparse_row_singleton)
963 lemma sparse_row_vector_nprt: "sorted_spvec (v :: 'a::lordered_ring spvec) \<Longrightarrow> sparse_row_vector (nprt_spvec v) = nprt (sparse_row_vector v)"
966 apply (frule sorted_spvec_cons1, auto)
967 apply (subst nprt_add)
968 apply (subst disj_matrices_commute)
969 apply (rule disj_sparse_row_singleton)
974 lemma pprt_move_matrix: "pprt (move_matrix (A::('a::lordered_ring) matrix) j i) = move_matrix (pprt A) j i"
975 apply (simp add: pprt_def)
976 apply (simp add: sup_matrix_def)
977 apply (simp add: Rep_matrix_inject[symmetric])
982 lemma nprt_move_matrix: "nprt (move_matrix (A::('a::lordered_ring) matrix) j i) = move_matrix (nprt A) j i"
983 apply (simp add: nprt_def)
984 apply (simp add: inf_matrix_def)
985 apply (simp add: Rep_matrix_inject[symmetric])
990 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)"
994 apply (frule sorted_spvec_cons1)
995 apply (simp add: sparse_row_matrix_cons sparse_row_vector_pprt)
996 apply (subst pprt_add)
997 apply (subst disj_matrices_commute)
998 apply (rule disj_move_sparse_vec_mat)
1000 apply (simp add: sorted_spvec.simps)
1001 apply (simp split: list.split)
1003 apply (simp add: pprt_move_matrix)
1006 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)"
1010 apply (frule sorted_spvec_cons1)
1011 apply (simp add: sparse_row_matrix_cons sparse_row_vector_nprt)
1012 apply (subst nprt_add)
1013 apply (subst disj_matrices_commute)
1014 apply (rule disj_move_sparse_vec_mat)
1016 apply (simp add: sorted_spvec.simps)
1017 apply (simp split: list.split)
1019 apply (simp add: nprt_move_matrix)
1022 lemma sorted_pprt_spvec: "sorted_spvec v \<Longrightarrow> sorted_spvec (pprt_spvec v)"
1025 apply (frule sorted_spvec_cons1)
1027 apply (simp add: sorted_spvec.simps split:list.split_asm)
1030 lemma sorted_nprt_spvec: "sorted_spvec v \<Longrightarrow> sorted_spvec (nprt_spvec v)"
1033 apply (frule sorted_spvec_cons1)
1035 apply (simp add: sorted_spvec.simps split:list.split_asm)
1038 lemma sorted_spvec_pprt_spmat: "sorted_spvec m \<Longrightarrow> sorted_spvec (pprt_spmat m)"
1041 apply (frule sorted_spvec_cons1)
1043 apply (simp add: sorted_spvec.simps split:list.split_asm)
1046 lemma sorted_spvec_nprt_spmat: "sorted_spvec m \<Longrightarrow> sorted_spvec (nprt_spmat m)"
1049 apply (frule sorted_spvec_cons1)
1051 apply (simp add: sorted_spvec.simps split:list.split_asm)
1054 lemma sorted_spmat_pprt_spmat: "sorted_spmat m \<Longrightarrow> sorted_spmat (pprt_spmat m)"
1056 apply (simp_all add: sorted_pprt_spvec)
1059 lemma sorted_spmat_nprt_spmat: "sorted_spmat m \<Longrightarrow> sorted_spmat (nprt_spmat m)"
1061 apply (simp_all add: sorted_nprt_spvec)
1065 mult_est_spmat :: "('a::lordered_ring) spmat \<Rightarrow> 'a spmat \<Rightarrow> 'a spmat \<Rightarrow> 'a spmat \<Rightarrow> 'a spmat"
1066 "mult_est_spmat r1 r2 s1 s2 ==
1067 add_spmat (mult_spmat (pprt_spmat s2) (pprt_spmat r2), add_spmat (mult_spmat (pprt_spmat s1) (nprt_spmat r2),
1068 add_spmat (mult_spmat (nprt_spmat s2) (pprt_spmat r1), mult_spmat (nprt_spmat s1) (nprt_spmat r1))))"
1070 lemmas sparse_row_matrix_op_simps =
1071 sorted_sparse_matrix_imp_spmat sorted_sparse_matrix_imp_spvec
1072 sparse_row_add_spmat sorted_spvec_add_spmat sorted_spmat_add_spmat
1073 sparse_row_diff_spmat sorted_spvec_diff_spmat sorted_spmat_diff_spmat
1074 sparse_row_matrix_minus sorted_spvec_minus_spmat sorted_spmat_minus_spmat
1075 sparse_row_mult_spmat sorted_spvec_mult_spmat sorted_spmat_mult_spmat
1076 sparse_row_matrix_abs sorted_spvec_abs_spmat sorted_spmat_abs_spmat
1077 le_spmat_iff_sparse_row_le
1078 sparse_row_matrix_pprt sorted_spvec_pprt_spmat sorted_spmat_pprt_spmat
1079 sparse_row_matrix_nprt sorted_spvec_nprt_spmat sorted_spmat_nprt_spmat
1081 lemma zero_eq_Numeral0: "(0::_::number_ring) = Numeral0" by simp
1083 lemmas sparse_row_matrix_arith_simps[simplified zero_eq_Numeral0] =
1084 mult_spmat.simps mult_spvec_spmat.simps
1086 smult_spvec_empty smult_spvec_cons
1087 add_spmat.simps add_spvec.simps
1088 minus_spmat.simps minus_spvec.simps
1089 abs_spmat.simps abs_spvec.simps
1091 le_spmat.simps le_spvec.simps
1092 pprt_spmat.simps pprt_spvec.simps
1093 nprt_spmat.simps nprt_spvec.simps
1097 (*lemma spm_linprog_dual_estimate_1:
1099 "sorted_sparse_matrix A1"
1100 "sorted_sparse_matrix A2"
1101 "sorted_sparse_matrix c1"
1102 "sorted_sparse_matrix c2"
1103 "sorted_sparse_matrix y"
1107 "A * x \<le> sparse_row_matrix (b::('a::lordered_ring) spmat)"
1108 "sparse_row_matrix A1 <= A"
1109 "A <= sparse_row_matrix A2"
1110 "sparse_row_matrix c1 <= c"
1111 "c <= sparse_row_matrix c2"
1112 "abs x \<le> sparse_row_matrix r"
1114 "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),
1115 abs_spmat (diff_spmat (mult_spmat y A1) c1)), diff_spmat c2 c1)) r))"
1116 by (insert prems, simp add: sparse_row_matrix_op_simps linprog_dual_estimate_1[where A=A])