src/HOL/Matrix/SparseMatrix.thy
 author obua Tue Jun 29 10:07:56 2004 +0200 (2004-06-29) changeset 15009 8c89f588c7aa child 15178 5f621aa35c25 permissions -rw-r--r--
support for sparse matrices
 obua@15009 ` 1` ```theory SparseMatrix = Matrix: ``` obua@15009 ` 2` obua@15009 ` 3` ```types ``` obua@15009 ` 4` ``` 'a spvec = "(nat * 'a) list" ``` obua@15009 ` 5` ``` 'a spmat = "('a spvec) spvec" ``` obua@15009 ` 6` obua@15009 ` 7` ```consts ``` obua@15009 ` 8` ``` sparse_row_vector :: "('a::lordered_ring) spvec \ 'a matrix" ``` obua@15009 ` 9` ``` sparse_row_matrix :: "('a::lordered_ring) spmat \ 'a matrix" ``` obua@15009 ` 10` obua@15009 ` 11` ```defs ``` obua@15009 ` 12` ``` sparse_row_vector_def : "sparse_row_vector arr == foldl (% m x. m + (singleton_matrix 0 (fst x) (snd x))) 0 arr" ``` obua@15009 ` 13` ``` 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" ``` obua@15009 ` 14` obua@15009 ` 15` ```lemma sparse_row_vector_empty[simp]: "sparse_row_vector [] = 0" ``` obua@15009 ` 16` ``` by (simp add: sparse_row_vector_def) ``` obua@15009 ` 17` obua@15009 ` 18` ```lemma sparse_row_matrix_empty[simp]: "sparse_row_matrix [] = 0" ``` obua@15009 ` 19` ``` by (simp add: sparse_row_matrix_def) ``` obua@15009 ` 20` obua@15009 ` 21` ```lemma foldl_distrstart[rule_format]: "! a x y. (f (g x y) a = g x (f y a)) \ ! x y. (foldl f (g x y) l = g x (foldl f y l))" ``` obua@15009 ` 22` ``` by (induct l, auto) ``` obua@15009 ` 23` obua@15009 ` 24` ```lemma sparse_row_vector_cons[simp]: "sparse_row_vector (a#arr) = (singleton_matrix 0 (fst a) (snd a)) + (sparse_row_vector arr)" ``` obua@15009 ` 25` ``` apply (induct arr) ``` obua@15009 ` 26` ``` apply (auto simp add: sparse_row_vector_def) ``` obua@15009 ` 27` ``` apply (simp add: foldl_distrstart[of "\m x. m + singleton_matrix 0 (fst x) (snd x)" "\x m. singleton_matrix 0 (fst x) (snd x) + m"]) ``` obua@15009 ` 28` ``` done ``` obua@15009 ` 29` obua@15009 ` 30` ```lemma sparse_row_vector_append[simp]: "sparse_row_vector (a @ b) = (sparse_row_vector a) + (sparse_row_vector b)" ``` obua@15009 ` 31` ``` by (induct a, auto) ``` obua@15009 ` 32` obua@15009 ` 33` ```lemma nrows_spvec[simp]: "nrows (sparse_row_vector x) <= (Suc 0)" ``` obua@15009 ` 34` ``` apply (induct x) ``` obua@15009 ` 35` ``` apply (simp_all add: add_nrows) ``` obua@15009 ` 36` ``` done ``` obua@15009 ` 37` obua@15009 ` 38` ```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" ``` obua@15009 ` 39` ``` apply (induct arr) ``` obua@15009 ` 40` ``` apply (auto simp add: sparse_row_matrix_def) ``` obua@15009 ` 41` ``` apply (simp add: foldl_distrstart[of "\m x. m + (move_matrix (sparse_row_vector (snd x)) (int (fst x)) 0)" ``` obua@15009 ` 42` ``` "% a m. (move_matrix (sparse_row_vector (snd a)) (int (fst a)) 0) + m"]) ``` obua@15009 ` 43` ``` done ``` obua@15009 ` 44` obua@15009 ` 45` ```lemma sparse_row_matrix_append: "sparse_row_matrix (arr@brr) = (sparse_row_matrix arr) + (sparse_row_matrix brr)" ``` obua@15009 ` 46` ``` apply (induct arr) ``` obua@15009 ` 47` ``` apply (auto simp add: sparse_row_matrix_cons) ``` obua@15009 ` 48` ``` done ``` obua@15009 ` 49` obua@15009 ` 50` ```consts ``` obua@15009 ` 51` ``` sorted_spvec :: "'a spvec \ bool" ``` obua@15009 ` 52` ``` sorted_spmat :: "'a spmat \ bool" ``` obua@15009 ` 53` obua@15009 ` 54` ```primrec ``` obua@15009 ` 55` ``` "sorted_spmat [] = True" ``` obua@15009 ` 56` ``` "sorted_spmat (a#as) = ((sorted_spvec (snd a)) & (sorted_spmat as))" ``` obua@15009 ` 57` obua@15009 ` 58` ```primrec ``` obua@15009 ` 59` ``` "sorted_spvec [] = True" ``` obua@15009 ` 60` ```sorted_spvec_step: "sorted_spvec (a#as) = (case as of [] \ True | b#bs \ ((fst a < fst b) & (sorted_spvec as)))" ``` obua@15009 ` 61` obua@15009 ` 62` ```declare sorted_spvec.simps [simp del] ``` obua@15009 ` 63` obua@15009 ` 64` ```lemma sorted_spvec_empty[simp]: "sorted_spvec [] = True" ``` obua@15009 ` 65` ```by (simp add: sorted_spvec.simps) ``` obua@15009 ` 66` obua@15009 ` 67` ```lemma sorted_spvec_cons1: "sorted_spvec (a#as) \ sorted_spvec as" ``` obua@15009 ` 68` ```apply (induct as) ``` obua@15009 ` 69` ```apply (auto simp add: sorted_spvec.simps) ``` obua@15009 ` 70` ```done ``` obua@15009 ` 71` obua@15009 ` 72` ```lemma sorted_spvec_cons2: "sorted_spvec (a#b#t) \ sorted_spvec (a#t)" ``` obua@15009 ` 73` ```apply (induct t) ``` obua@15009 ` 74` ```apply (auto simp add: sorted_spvec.simps) ``` obua@15009 ` 75` ```done ``` obua@15009 ` 76` obua@15009 ` 77` ```lemma sorted_spvec_cons3: "sorted_spvec(a#b#t) \ fst a < fst b" ``` obua@15009 ` 78` ```apply (auto simp add: sorted_spvec.simps) ``` obua@15009 ` 79` ```done ``` obua@15009 ` 80` obua@15009 ` 81` ```lemma sorted_sparse_row_vector_zero[rule_format]: "m <= n \ sorted_spvec ((n,a)#arr) \ Rep_matrix (sparse_row_vector arr) j m = 0" ``` obua@15009 ` 82` ```apply (induct arr) ``` obua@15009 ` 83` ```apply (auto) ``` obua@15009 ` 84` ```apply (frule sorted_spvec_cons2,simp)+ ``` obua@15009 ` 85` ```apply (frule sorted_spvec_cons3, simp) ``` obua@15009 ` 86` ```done ``` obua@15009 ` 87` obua@15009 ` 88` ```lemma sorted_sparse_row_matrix_zero[rule_format]: "m <= n \ sorted_spvec ((n,a)#arr) \ Rep_matrix (sparse_row_matrix arr) m j = 0" ``` obua@15009 ` 89` ``` apply (induct arr) ``` obua@15009 ` 90` ``` apply (auto) ``` obua@15009 ` 91` ``` apply (frule sorted_spvec_cons2, simp) ``` obua@15009 ` 92` ``` apply (frule sorted_spvec_cons3, simp) ``` obua@15009 ` 93` ``` apply (simp add: sparse_row_matrix_cons neg_def) ``` obua@15009 ` 94` ``` done ``` obua@15009 ` 95` obua@15009 ` 96` ```consts ``` obua@15009 ` 97` ``` smult_spvec :: "('a::lordered_ring) \ 'a spvec \ 'a spvec" ``` obua@15009 ` 98` ``` addmult_spvec :: "('a::lordered_ring) * 'a spvec * 'a spvec \ 'a spvec" ``` obua@15009 ` 99` obua@15009 ` 100` ```defs ``` obua@15009 ` 101` ``` smult_spvec_def: "smult_spvec y arr == map (% a. (fst a, y * snd a)) arr" ``` obua@15009 ` 102` obua@15009 ` 103` ```lemma smult_spvec_empty[simp]: "smult_spvec y [] = []" ``` obua@15009 ` 104` ``` by (simp add: smult_spvec_def) ``` obua@15009 ` 105` obua@15009 ` 106` ```lemma smult_spvec_cons: "smult_spvec y (a#arr) = (fst a, y * (snd a)) # (smult_spvec y arr)" ``` obua@15009 ` 107` ``` by (simp add: smult_spvec_def) ``` obua@15009 ` 108` obua@15009 ` 109` ```recdef addmult_spvec "measure (% (y, a, b). length a + (length b))" ``` obua@15009 ` 110` ``` "addmult_spvec (y, arr, []) = arr" ``` obua@15009 ` 111` ``` "addmult_spvec (y, [], brr) = smult_spvec y brr" ``` obua@15009 ` 112` ``` "addmult_spvec (y, a#arr, b#brr) = ( ``` obua@15009 ` 113` ``` if (fst a) < (fst b) then (a#(addmult_spvec (y, arr, b#brr))) ``` obua@15009 ` 114` ``` else (if (fst b < fst a) then ((fst b, y * (snd b))#(addmult_spvec (y, a#arr, brr))) ``` obua@15009 ` 115` ``` else ((fst a, (snd a)+ y*(snd b))#(addmult_spvec (y, arr,brr)))))" ``` obua@15009 ` 116` obua@15009 ` 117` ```lemma addmult_spvec_empty1[simp]: "addmult_spvec (y, [], a) = smult_spvec y a" ``` obua@15009 ` 118` ``` by (induct a, auto) ``` obua@15009 ` 119` obua@15009 ` 120` ```lemma addmult_spvec_empty2[simp]: "addmult_spvec (y, a, []) = a" ``` obua@15009 ` 121` ``` by (induct a, auto) ``` obua@15009 ` 122` obua@15009 ` 123` ```lemma sparse_row_vector_map: "(! x y. f (x+y) = (f x) + (f y)) \ (f::'a\('a::lordered_ring)) 0 = 0 \ ``` obua@15009 ` 124` ``` sparse_row_vector (map (% x. (fst x, f (snd x))) a) = apply_matrix f (sparse_row_vector a)" ``` obua@15009 ` 125` ``` apply (induct a) ``` obua@15009 ` 126` ``` apply (simp_all add: apply_matrix_add) ``` obua@15009 ` 127` ``` done ``` obua@15009 ` 128` obua@15009 ` 129` ```lemma sparse_row_vector_smult: "sparse_row_vector (smult_spvec y a) = scalar_mult y (sparse_row_vector a)" ``` obua@15009 ` 130` ``` apply (induct a) ``` obua@15009 ` 131` ``` apply (simp_all add: smult_spvec_cons scalar_mult_add) ``` obua@15009 ` 132` ``` done ``` obua@15009 ` 133` obua@15009 ` 134` ```lemma sparse_row_vector_addmult_spvec: "sparse_row_vector (addmult_spvec (y::'a::lordered_ring, a, b)) = ``` obua@15009 ` 135` ``` (sparse_row_vector a) + (scalar_mult y (sparse_row_vector b))" ``` obua@15009 ` 136` ``` apply (rule addmult_spvec.induct[of _ y]) ``` obua@15009 ` 137` ``` apply (simp add: scalar_mult_add smult_spvec_cons sparse_row_vector_smult singleton_matrix_add)+ ``` obua@15009 ` 138` ``` apply (case_tac "a=aa") ``` obua@15009 ` 139` ``` apply (auto) ``` obua@15009 ` 140` ``` done ``` obua@15009 ` 141` obua@15009 ` 142` ```lemma sorted_smult_spvec[rule_format]: "sorted_spvec a \ sorted_spvec (smult_spvec y a)" ``` obua@15009 ` 143` ``` apply (auto simp add: smult_spvec_def) ``` obua@15009 ` 144` ``` apply (induct a) ``` obua@15009 ` 145` ``` apply (auto simp add: sorted_spvec.simps) ``` obua@15009 ` 146` ``` apply (case_tac list) ``` obua@15009 ` 147` ``` apply (auto) ``` obua@15009 ` 148` ``` done ``` obua@15009 ` 149` obua@15009 ` 150` ```lemma sorted_spvec_addmult_spvec_helper: "\sorted_spvec (addmult_spvec (y, (a, b) # arr, brr)); aa < a; sorted_spvec ((a, b) # arr); ``` obua@15009 ` 151` ``` sorted_spvec ((aa, ba) # brr)\ \ sorted_spvec ((aa, y * ba) # addmult_spvec (y, (a, b) # arr, brr))" ``` obua@15009 ` 152` ``` apply (induct brr) ``` obua@15009 ` 153` ``` apply (auto simp add: sorted_spvec.simps) ``` obua@15009 ` 154` ``` apply (simp split: list.split) ``` obua@15009 ` 155` ``` apply (auto) ``` obua@15009 ` 156` ``` apply (simp split: list.split) ``` obua@15009 ` 157` ``` apply (auto) ``` obua@15009 ` 158` ``` done ``` obua@15009 ` 159` obua@15009 ` 160` ```lemma sorted_spvec_addmult_spvec_helper2: ``` obua@15009 ` 161` ``` "\sorted_spvec (addmult_spvec (y, arr, (aa, ba) # brr)); a < aa; sorted_spvec ((a, b) # arr); sorted_spvec ((aa, ba) # brr)\ ``` obua@15009 ` 162` ``` \ sorted_spvec ((a, b) # addmult_spvec (y, arr, (aa, ba) # brr))" ``` obua@15009 ` 163` ``` apply (induct arr) ``` obua@15009 ` 164` ``` apply (auto simp add: smult_spvec_def sorted_spvec.simps) ``` obua@15009 ` 165` ``` apply (simp split: list.split) ``` obua@15009 ` 166` ``` apply (auto) ``` obua@15009 ` 167` ``` done ``` obua@15009 ` 168` obua@15009 ` 169` ```lemma sorted_spvec_addmult_spvec_helper3[rule_format]: ``` obua@15009 ` 170` ``` "sorted_spvec (addmult_spvec (y, arr, brr)) \ sorted_spvec ((aa, b) # arr) \ sorted_spvec ((aa, ba) # brr) ``` obua@15009 ` 171` ``` \ sorted_spvec ((aa, b + y * ba) # (addmult_spvec (y, arr, brr)))" ``` obua@15009 ` 172` ``` apply (rule addmult_spvec.induct[of _ y arr brr]) ``` obua@15009 ` 173` ``` apply (simp_all add: sorted_spvec.simps smult_spvec_def) ``` obua@15009 ` 174` ``` done ``` obua@15009 ` 175` obua@15009 ` 176` ```lemma sorted_addmult_spvec[rule_format]: "sorted_spvec a \ sorted_spvec b \ sorted_spvec (addmult_spvec (y, a, b))" ``` obua@15009 ` 177` ``` apply (rule addmult_spvec.induct[of _ y a b]) ``` obua@15009 ` 178` ``` apply (simp_all add: sorted_smult_spvec) ``` obua@15009 ` 179` ``` apply (rule conjI, intro strip) ``` obua@15009 ` 180` ``` apply (case_tac "~(a < aa)") ``` obua@15009 ` 181` ``` apply (simp_all) ``` obua@15009 ` 182` ``` apply (frule_tac as=brr in sorted_spvec_cons1) ``` obua@15009 ` 183` ``` apply (simp add: sorted_spvec_addmult_spvec_helper) ``` obua@15009 ` 184` ``` apply (intro strip | rule conjI)+ ``` obua@15009 ` 185` ``` apply (frule_tac as=arr in sorted_spvec_cons1) ``` obua@15009 ` 186` ``` apply (simp add: sorted_spvec_addmult_spvec_helper2) ``` obua@15009 ` 187` ``` apply (intro strip) ``` obua@15009 ` 188` ``` apply (frule_tac as=arr in sorted_spvec_cons1) ``` obua@15009 ` 189` ``` apply (frule_tac as=brr in sorted_spvec_cons1) ``` obua@15009 ` 190` ``` apply (simp) ``` obua@15009 ` 191` ``` apply (case_tac "a=aa") ``` obua@15009 ` 192` ``` apply (simp_all add: sorted_spvec_addmult_spvec_helper3) ``` obua@15009 ` 193` ``` done ``` obua@15009 ` 194` obua@15009 ` 195` ```consts ``` obua@15009 ` 196` ``` mult_spvec_spmat :: "('a::lordered_ring) spvec * 'a spvec * 'a spmat \ 'a spvec" ``` obua@15009 ` 197` obua@15009 ` 198` ```recdef mult_spvec_spmat "measure (% (c, arr, brr). (length arr) + (length brr))" ``` obua@15009 ` 199` ``` "mult_spvec_spmat (c, [], brr) = c" ``` obua@15009 ` 200` ``` "mult_spvec_spmat (c, arr, []) = c" ``` obua@15009 ` 201` ``` "mult_spvec_spmat (c, a#arr, b#brr) = ( ``` obua@15009 ` 202` ``` if ((fst a) < (fst b)) then (mult_spvec_spmat (c, arr, b#brr)) ``` obua@15009 ` 203` ``` else (if ((fst b) < (fst a)) then (mult_spvec_spmat (c, a#arr, brr)) ``` obua@15009 ` 204` ``` else (mult_spvec_spmat (addmult_spvec (snd a, c, snd b), arr, brr))))" ``` obua@15009 ` 205` obua@15009 ` 206` ```lemma sparse_row_mult_spvec_spmat[rule_format]: "sorted_spvec (a::('a::lordered_ring) spvec) \ sorted_spvec B \ ``` obua@15009 ` 207` ``` sparse_row_vector (mult_spvec_spmat (c, a, B)) = (sparse_row_vector c) + (sparse_row_vector a) * (sparse_row_matrix B)" ``` obua@15009 ` 208` ```proof - ``` obua@15009 ` 209` ``` have comp_1: "!! a b. a < b \ Suc 0 <= nat ((int b)-(int a))" by arith ``` obua@15009 ` 210` ``` have not_iff: "!! a b. a = b \ (~ a) = (~ b)" by simp ``` obua@15009 ` 211` ``` have max_helper: "!! a b. ~ (a <= max (Suc a) b) \ False" ``` obua@15009 ` 212` ``` by arith ``` obua@15009 ` 213` ``` { ``` obua@15009 ` 214` ``` fix a ``` obua@15009 ` 215` ``` fix v ``` obua@15009 ` 216` ``` assume a:"a < nrows(sparse_row_vector v)" ``` obua@15009 ` 217` ``` have b:"nrows(sparse_row_vector v) <= 1" by simp ``` obua@15009 ` 218` ``` note dummy = less_le_trans[of a "nrows (sparse_row_vector v)" 1, OF a b] ``` obua@15009 ` 219` ``` then have "a = 0" by simp ``` obua@15009 ` 220` ``` } ``` obua@15009 ` 221` ``` note nrows_helper = this ``` obua@15009 ` 222` ``` show ?thesis ``` obua@15009 ` 223` ``` apply (rule mult_spvec_spmat.induct) ``` obua@15009 ` 224` ``` apply simp+ ``` obua@15009 ` 225` ``` apply (rule conjI) ``` obua@15009 ` 226` ``` apply (intro strip) ``` obua@15009 ` 227` ``` apply (frule_tac as=brr in sorted_spvec_cons1) ``` obua@15009 ` 228` ``` apply (simp add: ring_eq_simps sparse_row_matrix_cons) ``` obua@15009 ` 229` ``` apply (subst Rep_matrix_zero_imp_mult_zero) ``` obua@15009 ` 230` ``` apply (simp) ``` obua@15009 ` 231` ``` apply (intro strip) ``` obua@15009 ` 232` ``` apply (rule disjI2) ``` obua@15009 ` 233` ``` apply (intro strip) ``` obua@15009 ` 234` ``` apply (subst nrows) ``` obua@15009 ` 235` ``` apply (rule order_trans[of _ 1]) ``` obua@15009 ` 236` ``` apply (simp add: comp_1)+ ``` obua@15009 ` 237` ``` apply (subst Rep_matrix_zero_imp_mult_zero) ``` obua@15009 ` 238` ``` apply (intro strip) ``` obua@15009 ` 239` ``` apply (case_tac "k <= aa") ``` obua@15009 ` 240` ``` apply (rule_tac m1 = k and n1 = a and a1 = b in ssubst[OF sorted_sparse_row_vector_zero]) ``` obua@15009 ` 241` ``` apply (simp_all) ``` obua@15009 ` 242` ``` apply (rule impI) ``` obua@15009 ` 243` ``` apply (rule disjI2) ``` obua@15009 ` 244` ``` apply (rule nrows) ``` obua@15009 ` 245` ``` apply (rule order_trans[of _ 1]) ``` obua@15009 ` 246` ``` apply (simp_all add: comp_1) ``` obua@15009 ` 247` ``` ``` obua@15009 ` 248` ``` apply (intro strip | rule conjI)+ ``` obua@15009 ` 249` ``` apply (frule_tac as=arr in sorted_spvec_cons1) ``` obua@15009 ` 250` ``` apply (simp add: ring_eq_simps) ``` obua@15009 ` 251` ``` apply (subst Rep_matrix_zero_imp_mult_zero) ``` obua@15009 ` 252` ``` apply (simp) ``` obua@15009 ` 253` ``` apply (rule disjI2) ``` obua@15009 ` 254` ``` apply (intro strip) ``` obua@15009 ` 255` ``` apply (simp add: sparse_row_matrix_cons neg_def) ``` obua@15009 ` 256` ``` apply (case_tac "a <= aa") ``` obua@15009 ` 257` ``` apply (erule sorted_sparse_row_matrix_zero) ``` obua@15009 ` 258` ``` apply (simp_all) ``` obua@15009 ` 259` ``` apply (intro strip) ``` obua@15009 ` 260` ``` apply (case_tac "a=aa") ``` obua@15009 ` 261` ``` apply (simp_all) ``` obua@15009 ` 262` ``` apply (frule_tac as=arr in sorted_spvec_cons1) ``` obua@15009 ` 263` ``` apply (frule_tac as=brr in sorted_spvec_cons1) ``` obua@15009 ` 264` ``` apply (simp add: sparse_row_matrix_cons ring_eq_simps sparse_row_vector_addmult_spvec) ``` obua@15009 ` 265` ``` apply (rule_tac B1 = "sparse_row_matrix brr" in ssubst[OF Rep_matrix_zero_imp_mult_zero]) ``` obua@15009 ` 266` ``` apply (auto) ``` obua@15009 ` 267` ``` apply (rule sorted_sparse_row_matrix_zero) ``` obua@15009 ` 268` ``` apply (simp_all) ``` obua@15009 ` 269` ``` apply (rule_tac A1 = "sparse_row_vector arr" in ssubst[OF Rep_matrix_zero_imp_mult_zero]) ``` obua@15009 ` 270` ``` apply (auto) ``` obua@15009 ` 271` ``` apply (rule_tac m=k and n = aa and a = b and arr=arr in sorted_sparse_row_vector_zero) ``` obua@15009 ` 272` ``` apply (simp_all) ``` obua@15009 ` 273` ``` apply (simp add: neg_def) ``` obua@15009 ` 274` ``` apply (drule nrows_notzero) ``` obua@15009 ` 275` ``` apply (drule nrows_helper) ``` obua@15009 ` 276` ``` apply (arith) ``` obua@15009 ` 277` ``` ``` obua@15009 ` 278` ``` apply (subst Rep_matrix_inject[symmetric]) ``` obua@15009 ` 279` ``` apply (rule ext)+ ``` obua@15009 ` 280` ``` apply (simp) ``` obua@15009 ` 281` ``` apply (subst Rep_matrix_mult) ``` obua@15009 ` 282` ``` apply (rule_tac j1=aa in ssubst[OF foldseq_almostzero]) ``` obua@15009 ` 283` ``` apply (simp_all) ``` obua@15009 ` 284` ``` apply (intro strip, rule conjI) ``` obua@15009 ` 285` ``` apply (intro strip) ``` obua@15009 ` 286` ``` apply (drule_tac max_helper) ``` obua@15009 ` 287` ``` apply (simp) ``` obua@15009 ` 288` ``` apply (auto) ``` obua@15009 ` 289` ``` apply (rule zero_imp_mult_zero) ``` obua@15009 ` 290` ``` apply (rule disjI2) ``` obua@15009 ` 291` ``` apply (rule nrows) ``` obua@15009 ` 292` ``` apply (rule order_trans[of _ 1]) ``` obua@15009 ` 293` ``` apply (simp) ``` obua@15009 ` 294` ``` apply (simp) ``` obua@15009 ` 295` ``` done ``` obua@15009 ` 296` ```qed ``` obua@15009 ` 297` obua@15009 ` 298` ```lemma sorted_mult_spvec_spmat[rule_format]: ``` obua@15009 ` 299` ``` "sorted_spvec (c::('a::lordered_ring) spvec) \ sorted_spmat B \ sorted_spvec (mult_spvec_spmat (c, a, B))" ``` obua@15009 ` 300` ``` apply (rule mult_spvec_spmat.induct[of _ c a B]) ``` obua@15009 ` 301` ``` apply (simp_all add: sorted_addmult_spvec) ``` obua@15009 ` 302` ``` done ``` obua@15009 ` 303` obua@15009 ` 304` ```consts ``` obua@15009 ` 305` ``` mult_spmat :: "('a::lordered_ring) spmat \ 'a spmat \ 'a spmat" ``` obua@15009 ` 306` obua@15009 ` 307` ```primrec ``` obua@15009 ` 308` ``` "mult_spmat [] A = []" ``` obua@15009 ` 309` ``` "mult_spmat (a#as) A = (fst a, mult_spvec_spmat ([], snd a, A))#(mult_spmat as A)" ``` obua@15009 ` 310` obua@15009 ` 311` ```lemma sparse_row_mult_spmat[rule_format]: ``` obua@15009 ` 312` ``` "sorted_spmat A \ sorted_spvec B \ sparse_row_matrix (mult_spmat A B) = (sparse_row_matrix A) * (sparse_row_matrix B)" ``` obua@15009 ` 313` ``` apply (induct A) ``` obua@15009 ` 314` ``` apply (auto simp add: sparse_row_matrix_cons sparse_row_mult_spvec_spmat ring_eq_simps move_matrix_mult) ``` obua@15009 ` 315` ``` done ``` obua@15009 ` 316` obua@15009 ` 317` ```lemma sorted_spvec_mult_spmat[rule_format]: ``` obua@15009 ` 318` ``` "sorted_spvec (A::('a::lordered_ring) spmat) \ sorted_spvec (mult_spmat A B)" ``` obua@15009 ` 319` ``` apply (induct A) ``` obua@15009 ` 320` ``` apply (auto) ``` obua@15009 ` 321` ``` apply (drule sorted_spvec_cons1, simp) ``` obua@15009 ` 322` ``` apply (case_tac list) ``` obua@15009 ` 323` ``` apply (auto simp add: sorted_spvec.simps) ``` obua@15009 ` 324` ``` done ``` obua@15009 ` 325` obua@15009 ` 326` ```lemma sorted_spmat_mult_spmat[rule_format]: ``` obua@15009 ` 327` ``` "sorted_spmat (B::('a::lordered_ring) spmat) \ sorted_spmat (mult_spmat A B)" ``` obua@15009 ` 328` ``` apply (induct A) ``` obua@15009 ` 329` ``` apply (auto simp add: sorted_mult_spvec_spmat) ``` obua@15009 ` 330` ``` done ``` obua@15009 ` 331` obua@15009 ` 332` ```consts ``` obua@15009 ` 333` ``` add_spvec :: "('a::lordered_ab_group) spvec * 'a spvec \ 'a spvec" ``` obua@15009 ` 334` ``` add_spmat :: "('a::lordered_ab_group) spmat * 'a spmat \ 'a spmat" ``` obua@15009 ` 335` obua@15009 ` 336` ```recdef add_spvec "measure (% (a, b). length a + (length b))" ``` obua@15009 ` 337` ``` "add_spvec (arr, []) = arr" ``` obua@15009 ` 338` ``` "add_spvec ([], brr) = brr" ``` obua@15009 ` 339` ``` "add_spvec (a#arr, b#brr) = ( ``` obua@15009 ` 340` ``` if (fst a) < (fst b) then (a#(add_spvec (arr, b#brr))) ``` obua@15009 ` 341` ``` else (if (fst b < fst a) then (b#(add_spvec (a#arr, brr))) ``` obua@15009 ` 342` ``` else ((fst a, (snd a)+(snd b))#(add_spvec (arr,brr)))))" ``` obua@15009 ` 343` obua@15009 ` 344` ```lemma add_spvec_empty1[simp]: "add_spvec ([], a) = a" ``` obua@15009 ` 345` ``` by (induct a, auto) ``` obua@15009 ` 346` obua@15009 ` 347` ```lemma add_spvec_empty2[simp]: "add_spvec (a, []) = a" ``` obua@15009 ` 348` ``` by (induct a, auto) ``` obua@15009 ` 349` obua@15009 ` 350` ```lemma sparse_row_vector_add: "sparse_row_vector (add_spvec (a,b)) = (sparse_row_vector a) + (sparse_row_vector b)" ``` obua@15009 ` 351` ``` apply (rule add_spvec.induct[of _ a b]) ``` obua@15009 ` 352` ``` apply (simp_all add: singleton_matrix_add) ``` obua@15009 ` 353` ``` apply (case_tac "a = aa") ``` obua@15009 ` 354` ``` apply (simp_all) ``` obua@15009 ` 355` ``` done ``` obua@15009 ` 356` obua@15009 ` 357` ```recdef add_spmat "measure (% (A,B). (length A)+(length B))" ``` obua@15009 ` 358` ``` "add_spmat ([], bs) = bs" ``` obua@15009 ` 359` ``` "add_spmat (as, []) = as" ``` obua@15009 ` 360` ``` "add_spmat (a#as, b#bs) = ( ``` obua@15009 ` 361` ``` if fst a < fst b then ``` obua@15009 ` 362` ``` (a#(add_spmat (as, b#bs))) ``` obua@15009 ` 363` ``` else (if fst b < fst a then ``` obua@15009 ` 364` ``` (b#(add_spmat (a#as, bs))) ``` obua@15009 ` 365` ``` else ``` obua@15009 ` 366` ``` ((fst a, add_spvec (snd a, snd b))#(add_spmat (as, bs)))))" ``` obua@15009 ` 367` obua@15009 ` 368` ```lemma sparse_row_add_spmat: "sparse_row_matrix (add_spmat (A, B)) = (sparse_row_matrix A) + (sparse_row_matrix B)" ``` obua@15009 ` 369` ``` apply (rule add_spmat.induct) ``` obua@15009 ` 370` ``` apply (auto simp add: sparse_row_matrix_cons sparse_row_vector_add move_matrix_add) ``` obua@15009 ` 371` ``` apply (case_tac "a=aa", simp, simp)+ ``` obua@15009 ` 372` ``` done ``` obua@15009 ` 373` obua@15009 ` 374` ```lemma sorted_add_spvec_helper1[rule_format]: "add_spvec ((a,b)#arr, brr) = (ab, bb) # list \ (ab = a | (brr \ [] & ab = fst (hd brr)))" ``` obua@15009 ` 375` ``` proof - ``` obua@15009 ` 376` ``` have "(! x ab a. x = (a,b)#arr \ add_spvec (x, brr) = (ab, bb) # list \ (ab = a | (ab = fst (hd brr))))" ``` obua@15009 ` 377` ``` by (rule add_spvec.induct[of _ _ brr], auto) ``` obua@15009 ` 378` ``` then show ?thesis ``` obua@15009 ` 379` ``` by (case_tac brr, auto) ``` obua@15009 ` 380` ``` qed ``` obua@15009 ` 381` obua@15009 ` 382` ```lemma sorted_add_spmat_helper1[rule_format]: "add_spmat ((a,b)#arr, brr) = (ab, bb) # list \ (ab = a | (brr \ [] & ab = fst (hd brr)))" ``` obua@15009 ` 383` ``` proof - ``` obua@15009 ` 384` ``` have "(! x ab a. x = (a,b)#arr \ add_spmat (x, brr) = (ab, bb) # list \ (ab = a | (ab = fst (hd brr))))" ``` obua@15009 ` 385` ``` by (rule add_spmat.induct[of _ _ brr], auto) ``` obua@15009 ` 386` ``` then show ?thesis ``` obua@15009 ` 387` ``` by (case_tac brr, auto) ``` obua@15009 ` 388` ``` qed ``` obua@15009 ` 389` obua@15009 ` 390` ```lemma sorted_add_spvec_helper[rule_format]: "add_spvec (arr, brr) = (ab, bb) # list \ ((arr \ [] & ab = fst (hd arr)) | (brr \ [] & ab = fst (hd brr)))" ``` obua@15009 ` 391` ``` apply (rule add_spvec.induct[of _ arr brr]) ``` obua@15009 ` 392` ``` apply (auto) ``` obua@15009 ` 393` ``` done ``` obua@15009 ` 394` obua@15009 ` 395` ```lemma sorted_add_spmat_helper[rule_format]: "add_spmat (arr, brr) = (ab, bb) # list \ ((arr \ [] & ab = fst (hd arr)) | (brr \ [] & ab = fst (hd brr)))" ``` obua@15009 ` 396` ``` apply (rule add_spmat.induct[of _ arr brr]) ``` obua@15009 ` 397` ``` apply (auto) ``` obua@15009 ` 398` ``` done ``` obua@15009 ` 399` obua@15009 ` 400` ```lemma add_spvec_commute: "add_spvec (a, b) = add_spvec (b, a)" ``` obua@15009 ` 401` ``` by (rule add_spvec.induct[of _ a b], auto) ``` obua@15009 ` 402` obua@15009 ` 403` ```lemma add_spmat_commute: "add_spmat (a, b) = add_spmat (b, a)" ``` obua@15009 ` 404` ``` apply (rule add_spmat.induct[of _ a b]) ``` obua@15009 ` 405` ``` apply (simp_all add: add_spvec_commute) ``` obua@15009 ` 406` ``` done ``` obua@15009 ` 407` ``` ``` obua@15009 ` 408` ```lemma sorted_add_spvec_helper2: "add_spvec ((a,b)#arr, brr) = (ab, bb) # list \ aa < a \ sorted_spvec ((aa, ba) # brr) \ aa < ab" ``` obua@15009 ` 409` ``` apply (drule sorted_add_spvec_helper1) ``` obua@15009 ` 410` ``` apply (auto) ``` obua@15009 ` 411` ``` apply (case_tac brr) ``` obua@15009 ` 412` ``` apply (simp_all) ``` obua@15009 ` 413` ``` apply (drule_tac sorted_spvec_cons3) ``` obua@15009 ` 414` ``` apply (simp) ``` obua@15009 ` 415` ``` done ``` obua@15009 ` 416` obua@15009 ` 417` ```lemma sorted_add_spmat_helper2: "add_spmat ((a,b)#arr, brr) = (ab, bb) # list \ aa < a \ sorted_spvec ((aa, ba) # brr) \ aa < ab" ``` obua@15009 ` 418` ``` apply (drule sorted_add_spmat_helper1) ``` obua@15009 ` 419` ``` apply (auto) ``` obua@15009 ` 420` ``` apply (case_tac brr) ``` obua@15009 ` 421` ``` apply (simp_all) ``` obua@15009 ` 422` ``` apply (drule_tac sorted_spvec_cons3) ``` obua@15009 ` 423` ``` apply (simp) ``` obua@15009 ` 424` ``` done ``` obua@15009 ` 425` obua@15009 ` 426` ```lemma sorted_spvec_add_spvec[rule_format]: "sorted_spvec a \ sorted_spvec b \ sorted_spvec (add_spvec (a, b))" ``` obua@15009 ` 427` ``` apply (rule add_spvec.induct[of _ a b]) ``` obua@15009 ` 428` ``` apply (simp_all) ``` obua@15009 ` 429` ``` apply (rule conjI) ``` obua@15009 ` 430` ``` apply (intro strip) ``` obua@15009 ` 431` ``` apply (simp) ``` obua@15009 ` 432` ``` apply (frule_tac as=brr in sorted_spvec_cons1) ``` obua@15009 ` 433` ``` apply (simp) ``` obua@15009 ` 434` ``` apply (subst sorted_spvec_step) ``` obua@15009 ` 435` ``` apply (simp split: list.split) ``` obua@15009 ` 436` ``` apply (clarify, simp) ``` obua@15009 ` 437` ``` apply (simp add: sorted_add_spvec_helper2) ``` obua@15009 ` 438` ``` apply (clarify) ``` obua@15009 ` 439` ``` apply (rule conjI) ``` obua@15009 ` 440` ``` apply (case_tac "a=aa") ``` obua@15009 ` 441` ``` apply (simp) ``` obua@15009 ` 442` ``` apply (clarify) ``` obua@15009 ` 443` ``` apply (frule_tac as=arr in sorted_spvec_cons1, simp) ``` obua@15009 ` 444` ``` apply (subst sorted_spvec_step) ``` obua@15009 ` 445` ``` apply (simp split: list.split) ``` obua@15009 ` 446` ``` apply (clarify, simp) ``` obua@15009 ` 447` ``` apply (simp add: sorted_add_spvec_helper2 add_spvec_commute) ``` obua@15009 ` 448` ``` apply (case_tac "a=aa") ``` obua@15009 ` 449` ``` apply (simp_all) ``` obua@15009 ` 450` ``` apply (clarify) ``` obua@15009 ` 451` ``` apply (frule_tac as=arr in sorted_spvec_cons1) ``` obua@15009 ` 452` ``` apply (frule_tac as=brr in sorted_spvec_cons1) ``` obua@15009 ` 453` ``` apply (simp) ``` obua@15009 ` 454` ``` apply (subst sorted_spvec_step) ``` obua@15009 ` 455` ``` apply (simp split: list.split) ``` obua@15009 ` 456` ``` apply (clarify, simp) ``` obua@15009 ` 457` ``` apply (drule_tac sorted_add_spvec_helper) ``` obua@15009 ` 458` ``` apply (auto) ``` obua@15009 ` 459` ``` apply (case_tac arr) ``` obua@15009 ` 460` ``` apply (simp_all) ``` obua@15009 ` 461` ``` apply (drule sorted_spvec_cons3) ``` obua@15009 ` 462` ``` apply (simp) ``` obua@15009 ` 463` ``` apply (case_tac brr) ``` obua@15009 ` 464` ``` apply (simp_all) ``` obua@15009 ` 465` ``` apply (drule sorted_spvec_cons3) ``` obua@15009 ` 466` ``` apply (simp) ``` obua@15009 ` 467` ``` done ``` obua@15009 ` 468` obua@15009 ` 469` ```lemma sorted_spvec_add_spmat[rule_format]: "sorted_spvec A \ sorted_spvec B \ sorted_spvec (add_spmat (A, B))" ``` obua@15009 ` 470` ``` apply (rule add_spmat.induct[of _ A B]) ``` obua@15009 ` 471` ``` apply (simp_all) ``` obua@15009 ` 472` ``` apply (rule conjI) ``` obua@15009 ` 473` ``` apply (intro strip) ``` obua@15009 ` 474` ``` apply (simp) ``` obua@15009 ` 475` ``` apply (frule_tac as=bs in sorted_spvec_cons1) ``` obua@15009 ` 476` ``` apply (simp) ``` obua@15009 ` 477` ``` apply (subst sorted_spvec_step) ``` obua@15009 ` 478` ``` apply (simp split: list.split) ``` obua@15009 ` 479` ``` apply (clarify, simp) ``` obua@15009 ` 480` ``` apply (simp add: sorted_add_spmat_helper2) ``` obua@15009 ` 481` ``` apply (clarify) ``` obua@15009 ` 482` ``` apply (rule conjI) ``` obua@15009 ` 483` ``` apply (case_tac "a=aa") ``` obua@15009 ` 484` ``` apply (simp) ``` obua@15009 ` 485` ``` apply (clarify) ``` obua@15009 ` 486` ``` apply (frule_tac as=as in sorted_spvec_cons1, simp) ``` obua@15009 ` 487` ``` apply (subst sorted_spvec_step) ``` obua@15009 ` 488` ``` apply (simp split: list.split) ``` obua@15009 ` 489` ``` apply (clarify, simp) ``` obua@15009 ` 490` ``` apply (simp add: sorted_add_spmat_helper2 add_spmat_commute) ``` obua@15009 ` 491` ``` apply (case_tac "a=aa") ``` obua@15009 ` 492` ``` apply (simp_all) ``` obua@15009 ` 493` ``` apply (clarify) ``` obua@15009 ` 494` ``` apply (frule_tac as=as in sorted_spvec_cons1) ``` obua@15009 ` 495` ``` apply (frule_tac as=bs in sorted_spvec_cons1) ``` obua@15009 ` 496` ``` apply (simp) ``` obua@15009 ` 497` ``` apply (subst sorted_spvec_step) ``` obua@15009 ` 498` ``` apply (simp split: list.split) ``` obua@15009 ` 499` ``` apply (clarify, simp) ``` obua@15009 ` 500` ``` apply (drule_tac sorted_add_spmat_helper) ``` obua@15009 ` 501` ``` apply (auto) ``` obua@15009 ` 502` ``` apply (case_tac as) ``` obua@15009 ` 503` ``` apply (simp_all) ``` obua@15009 ` 504` ``` apply (drule sorted_spvec_cons3) ``` obua@15009 ` 505` ``` apply (simp) ``` obua@15009 ` 506` ``` apply (case_tac bs) ``` obua@15009 ` 507` ``` apply (simp_all) ``` obua@15009 ` 508` ``` apply (drule sorted_spvec_cons3) ``` obua@15009 ` 509` ``` apply (simp) ``` obua@15009 ` 510` ``` done ``` obua@15009 ` 511` obua@15009 ` 512` ```lemma sorted_spmat_add_spmat[rule_format]: "sorted_spmat A \ sorted_spmat B \ sorted_spmat (add_spmat (A, B))" ``` obua@15009 ` 513` ``` apply (rule add_spmat.induct[of _ A B]) ``` obua@15009 ` 514` ``` apply (simp_all add: sorted_spvec_add_spvec) ``` obua@15009 ` 515` ``` done ``` obua@15009 ` 516` obua@15009 ` 517` ```consts ``` obua@15009 ` 518` ``` le_spvec :: "('a::lordered_ab_group) spvec * 'a spvec \ bool" ``` obua@15009 ` 519` ``` le_spmat :: "('a::lordered_ab_group) spmat * 'a spmat \ bool" ``` obua@15009 ` 520` obua@15009 ` 521` ```recdef le_spvec "measure (% (a,b). (length a) + (length b))" ``` obua@15009 ` 522` ``` "le_spvec ([], []) = True" ``` obua@15009 ` 523` ``` "le_spvec (a#as, []) = ((snd a <= 0) & (le_spvec (as, [])))" ``` obua@15009 ` 524` ``` "le_spvec ([], b#bs) = ((0 <= snd b) & (le_spvec ([], bs)))" ``` obua@15009 ` 525` ``` "le_spvec (a#as, b#bs) = ( ``` obua@15009 ` 526` ``` if (fst a < fst b) then ``` obua@15009 ` 527` ``` ((snd a <= 0) & (le_spvec (as, b#bs))) ``` obua@15009 ` 528` ``` else (if (fst b < fst a) then ``` obua@15009 ` 529` ``` ((0 <= snd b) & (le_spvec (a#as, bs))) ``` obua@15009 ` 530` ``` else ``` obua@15009 ` 531` ``` ((snd a <= snd b) & (le_spvec (as, bs)))))" ``` obua@15009 ` 532` obua@15009 ` 533` ```recdef le_spmat "measure (% (a,b). (length a) + (length b))" ``` obua@15009 ` 534` ``` "le_spmat ([], []) = True" ``` obua@15009 ` 535` ``` "le_spmat (a#as, []) = (le_spvec (snd a, []) & (le_spmat (as, [])))" ``` obua@15009 ` 536` ``` "le_spmat ([], b#bs) = (le_spvec ([], snd b) & (le_spmat ([], bs)))" ``` obua@15009 ` 537` ``` "le_spmat (a#as, b#bs) = ( ``` obua@15009 ` 538` ``` if fst a < fst b then ``` obua@15009 ` 539` ``` (le_spvec(snd a,[]) & le_spmat(as, b#bs)) ``` obua@15009 ` 540` ``` else (if (fst b < fst a) then ``` obua@15009 ` 541` ``` (le_spvec([], snd b) & le_spmat(a#as, bs)) ``` obua@15009 ` 542` ``` else ``` obua@15009 ` 543` ``` (le_spvec(snd a, snd b) & le_spmat (as, bs))))" ``` obua@15009 ` 544` obua@15009 ` 545` ```lemma spec2: "! j i. P j i \ P j i" by blast ``` obua@15009 ` 546` ```lemma neg_imp: "(\ Q \ \ P) \ P \ Q" by blast ``` obua@15009 ` 547` obua@15009 ` 548` ```constdefs ``` obua@15009 ` 549` ``` disj_matrices :: "('a::zero) matrix \ 'a matrix \ bool" ``` obua@15009 ` 550` ``` "disj_matrices A B == (! j i. (Rep_matrix A j i \ 0) \ (Rep_matrix B j i = 0)) & (! j i. (Rep_matrix B j i \ 0) \ (Rep_matrix A j i = 0))" ``` obua@15009 ` 551` obua@15009 ` 552` ```ML {* simp_depth_limit := 2 *} ``` obua@15009 ` 553` obua@15009 ` 554` ```lemma disj_matrices_add: "disj_matrices A B \ disj_matrices C D \ disj_matrices A D \ disj_matrices B C \ ``` obua@15009 ` 555` ``` (A + B <= C + D) = (A <= C & B <= (D::('a::lordered_ab_group) matrix))" ``` obua@15009 ` 556` ``` apply (auto) ``` obua@15009 ` 557` ``` apply (simp (no_asm_use) only: le_matrix_def disj_matrices_def) ``` obua@15009 ` 558` ``` apply (intro strip) ``` obua@15009 ` 559` ``` apply (erule conjE)+ ``` obua@15009 ` 560` ``` apply (drule_tac j=j and i=i in spec2)+ ``` obua@15009 ` 561` ``` apply (case_tac "Rep_matrix B j i = 0") ``` obua@15009 ` 562` ``` apply (case_tac "Rep_matrix D j i = 0") ``` obua@15009 ` 563` ``` apply (simp_all) ``` obua@15009 ` 564` ``` apply (simp (no_asm_use) only: le_matrix_def disj_matrices_def) ``` obua@15009 ` 565` ``` apply (intro strip) ``` obua@15009 ` 566` ``` apply (erule conjE)+ ``` obua@15009 ` 567` ``` apply (drule_tac j=j and i=i in spec2)+ ``` obua@15009 ` 568` ``` apply (case_tac "Rep_matrix A j i = 0") ``` obua@15009 ` 569` ``` apply (case_tac "Rep_matrix C j i = 0") ``` obua@15009 ` 570` ``` apply (simp_all) ``` obua@15009 ` 571` ``` apply (erule add_mono) ``` obua@15009 ` 572` ``` apply (assumption) ``` obua@15009 ` 573` ``` done ``` obua@15009 ` 574` obua@15009 ` 575` ```lemma disj_matrices_zero1[simp]: "disj_matrices 0 B" ``` obua@15009 ` 576` ```by (simp add: disj_matrices_def) ``` obua@15009 ` 577` obua@15009 ` 578` ```lemma disj_matrices_zero2[simp]: "disj_matrices A 0" ``` obua@15009 ` 579` ```by (simp add: disj_matrices_def) ``` obua@15009 ` 580` obua@15009 ` 581` ```lemma disj_matrices_commute: "disj_matrices A B = disj_matrices B A" ``` obua@15009 ` 582` ```by (auto simp add: disj_matrices_def) ``` obua@15009 ` 583` obua@15009 ` 584` ```lemma disj_matrices_add_le_zero: "disj_matrices A B \ ``` obua@15009 ` 585` ``` (A + B <= 0) = (A <= 0 & (B::('a::lordered_ab_group) matrix) <= 0)" ``` obua@15009 ` 586` ```by (rule disj_matrices_add[of A B 0 0, simplified]) ``` obua@15009 ` 587` ``` ``` obua@15009 ` 588` ```lemma disj_matrices_add_zero_le: "disj_matrices A B \ ``` obua@15009 ` 589` ``` (0 <= A + B) = (0 <= A & 0 <= (B::('a::lordered_ab_group) matrix))" ``` obua@15009 ` 590` ```by (rule disj_matrices_add[of 0 0 A B, simplified]) ``` obua@15009 ` 591` obua@15009 ` 592` ```lemma disj_matrices_add_x_le: "disj_matrices A B \ disj_matrices B C \ ``` obua@15009 ` 593` ``` (A <= B + C) = (A <= C & 0 <= (B::('a::lordered_ab_group) matrix))" ``` obua@15009 ` 594` ```by (auto simp add: disj_matrices_add[of 0 A B C, simplified]) ``` obua@15009 ` 595` obua@15009 ` 596` ```lemma disj_matrices_add_le_x: "disj_matrices A B \ disj_matrices B C \ ``` obua@15009 ` 597` ``` (B + A <= C) = (A <= C & (B::('a::lordered_ab_group) matrix) <= 0)" ``` obua@15009 ` 598` ```by (auto simp add: disj_matrices_add[of B A 0 C,simplified] disj_matrices_commute) ``` obua@15009 ` 599` obua@15009 ` 600` ```lemma singleton_le_zero[simp]: "(singleton_matrix j i x <= 0) = (x <= (0::'a::{order,zero}))" ``` obua@15009 ` 601` ``` apply (auto) ``` obua@15009 ` 602` ``` apply (simp add: le_matrix_def) ``` obua@15009 ` 603` ``` apply (drule_tac j=j and i=i in spec2) ``` obua@15009 ` 604` ``` apply (simp) ``` obua@15009 ` 605` ``` apply (simp add: le_matrix_def) ``` obua@15009 ` 606` ``` done ``` obua@15009 ` 607` obua@15009 ` 608` ```lemma singleton_ge_zero[simp]: "(0 <= singleton_matrix j i x) = ((0::'a::{order,zero}) <= x)" ``` obua@15009 ` 609` ``` apply (auto) ``` obua@15009 ` 610` ``` apply (simp add: le_matrix_def) ``` obua@15009 ` 611` ``` apply (drule_tac j=j and i=i in spec2) ``` obua@15009 ` 612` ``` apply (simp) ``` obua@15009 ` 613` ``` apply (simp add: le_matrix_def) ``` obua@15009 ` 614` ``` done ``` obua@15009 ` 615` obua@15009 ` 616` ```lemma disj_sparse_row_singleton: "i <= j \ sorted_spvec((j,y)#v) \ disj_matrices (sparse_row_vector v) (singleton_matrix 0 i x)" ``` obua@15009 ` 617` ``` apply (simp add: disj_matrices_def) ``` obua@15009 ` 618` ``` apply (rule conjI) ``` obua@15009 ` 619` ``` apply (rule neg_imp) ``` obua@15009 ` 620` ``` apply (simp) ``` obua@15009 ` 621` ``` apply (intro strip) ``` obua@15009 ` 622` ``` apply (rule sorted_sparse_row_vector_zero) ``` obua@15009 ` 623` ``` apply (simp_all) ``` obua@15009 ` 624` ``` apply (intro strip) ``` obua@15009 ` 625` ``` apply (rule sorted_sparse_row_vector_zero) ``` obua@15009 ` 626` ``` apply (simp_all) ``` obua@15009 ` 627` ``` done ``` obua@15009 ` 628` obua@15009 ` 629` ```lemma disj_matrices_x_add: "disj_matrices A B \ disj_matrices A C \ disj_matrices (A::('a::lordered_ab_group) matrix) (B+C)" ``` obua@15009 ` 630` ``` apply (simp add: disj_matrices_def) ``` obua@15009 ` 631` ``` apply (auto) ``` obua@15009 ` 632` ``` apply (drule_tac j=j and i=i in spec2)+ ``` obua@15009 ` 633` ``` apply (case_tac "Rep_matrix B j i = 0") ``` obua@15009 ` 634` ``` apply (case_tac "Rep_matrix C j i = 0") ``` obua@15009 ` 635` ``` apply (simp_all) ``` obua@15009 ` 636` ``` done ``` obua@15009 ` 637` obua@15009 ` 638` ```lemma disj_matrices_add_x: "disj_matrices A B \ disj_matrices A C \ disj_matrices (B+C) (A::('a::lordered_ab_group) matrix)" ``` obua@15009 ` 639` ``` by (simp add: disj_matrices_x_add disj_matrices_commute) ``` obua@15009 ` 640` obua@15009 ` 641` ```lemma disj_singleton_matrices[simp]: "disj_matrices (singleton_matrix j i x) (singleton_matrix u v y) = (j \ u | i \ v | x = 0 | y = 0)" ``` obua@15009 ` 642` ``` by (auto simp add: disj_matrices_def) ``` obua@15009 ` 643` obua@15009 ` 644` ```lemma le_spvec_iff_sparse_row_le[rule_format]: "(sorted_spvec a) \ (sorted_spvec b) \ (le_spvec (a,b)) = (sparse_row_vector a <= sparse_row_vector b)" ``` obua@15009 ` 645` ``` apply (rule le_spvec.induct) ``` obua@15009 ` 646` ``` apply (simp_all add: sorted_spvec_cons1 disj_matrices_add_le_zero disj_matrices_add_zero_le disj_sparse_row_singleton[OF order_refl] disj_matrices_commute) ``` obua@15009 ` 647` ``` apply (rule conjI, intro strip) ``` obua@15009 ` 648` ``` apply (simp add: sorted_spvec_cons1) ``` obua@15009 ` 649` ``` apply (subst disj_matrices_add_x_le) ``` obua@15009 ` 650` ``` apply (simp add: disj_sparse_row_singleton[OF less_imp_le] disj_matrices_x_add disj_matrices_commute) ``` obua@15009 ` 651` ``` apply (simp add: disj_sparse_row_singleton[OF order_refl] disj_matrices_commute) ``` obua@15009 ` 652` ``` apply (simp, blast) ``` obua@15009 ` 653` ``` apply (intro strip, rule conjI, intro strip) ``` obua@15009 ` 654` ``` apply (simp add: sorted_spvec_cons1) ``` obua@15009 ` 655` ``` apply (subst disj_matrices_add_le_x) ``` obua@15009 ` 656` ``` 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) ``` obua@15009 ` 657` ``` apply (blast) ``` obua@15009 ` 658` ``` apply (intro strip) ``` obua@15009 ` 659` ``` apply (simp add: sorted_spvec_cons1) ``` obua@15009 ` 660` ``` apply (case_tac "a=aa", simp_all) ``` obua@15009 ` 661` ``` apply (subst disj_matrices_add) ``` obua@15009 ` 662` ``` apply (simp_all add: disj_sparse_row_singleton[OF order_refl] disj_matrices_commute) ``` obua@15009 ` 663` ``` done ``` obua@15009 ` 664` obua@15009 ` 665` ```lemma disj_move_sparse_vec_mat[simplified disj_matrices_commute]: ``` obua@15009 ` 666` ``` "j <= a \ sorted_spvec((a,c)#as) \ disj_matrices (move_matrix (sparse_row_vector b) (int j) i) (sparse_row_matrix as)" ``` obua@15009 ` 667` ``` apply (auto simp add: neg_def disj_matrices_def) ``` obua@15009 ` 668` ``` apply (drule nrows_notzero) ``` obua@15009 ` 669` ``` apply (drule less_le_trans[OF _ nrows_spvec]) ``` obua@15009 ` 670` ``` apply (subgoal_tac "ja = j") ``` obua@15009 ` 671` ``` apply (simp add: sorted_sparse_row_matrix_zero) ``` obua@15009 ` 672` ``` apply (arith) ``` obua@15009 ` 673` ``` apply (rule nrows) ``` obua@15009 ` 674` ``` apply (rule order_trans[of _ 1 _]) ``` obua@15009 ` 675` ``` apply (simp) ``` obua@15009 ` 676` ``` apply (case_tac "nat (int ja - int j) = 0") ``` obua@15009 ` 677` ``` apply (case_tac "ja = j") ``` obua@15009 ` 678` ``` apply (simp add: sorted_sparse_row_matrix_zero) ``` obua@15009 ` 679` ``` apply arith+ ``` obua@15009 ` 680` ``` done ``` obua@15009 ` 681` obua@15009 ` 682` ```lemma disj_move_sparse_row_vector_twice: ``` obua@15009 ` 683` ``` "j \ u \ disj_matrices (move_matrix (sparse_row_vector a) j i) (move_matrix (sparse_row_vector b) u v)" ``` obua@15009 ` 684` ``` apply (auto simp add: neg_def disj_matrices_def) ``` obua@15009 ` 685` ``` apply (rule nrows, rule order_trans[of _ 1], simp, drule nrows_notzero, drule less_le_trans[OF _ nrows_spvec], arith)+ ``` obua@15009 ` 686` ``` done ``` obua@15009 ` 687` obua@15009 ` 688` ```lemma move_matrix_le_zero[simp]: "0 <= j \ 0 <= i \ (move_matrix A j i <= 0) = (A <= (0::('a::{order,zero}) matrix))" ``` obua@15009 ` 689` ``` apply (auto simp add: le_matrix_def neg_def) ``` obua@15009 ` 690` ``` apply (drule_tac j="ja+(nat j)" and i="ia+(nat i)" in spec2) ``` obua@15009 ` 691` ``` apply (auto) ``` obua@15009 ` 692` ``` done ``` obua@15009 ` 693` obua@15009 ` 694` ```lemma move_matrix_zero_le[simp]: "0 <= j \ 0 <= i \ (0 <= move_matrix A j i) = ((0::('a::{order,zero}) matrix) <= A)" ``` obua@15009 ` 695` ``` apply (auto simp add: le_matrix_def neg_def) ``` obua@15009 ` 696` ``` apply (drule_tac j="ja+(nat j)" and i="ia+(nat i)" in spec2) ``` obua@15009 ` 697` ``` apply (auto) ``` obua@15009 ` 698` ``` done ``` obua@15009 ` 699` obua@15009 ` 700` ```lemma move_matrix_le_move_matrix_iff[simp]: "0 <= j \ 0 <= i \ (move_matrix A j i <= move_matrix B j i) = (A <= (B::('a::{order,zero}) matrix))" ``` obua@15009 ` 701` ``` apply (auto simp add: le_matrix_def neg_def) ``` obua@15009 ` 702` ``` apply (drule_tac j="ja+(nat j)" and i="ia+(nat i)" in spec2) ``` obua@15009 ` 703` ``` apply (auto) ``` obua@15009 ` 704` ``` done ``` obua@15009 ` 705` obua@15009 ` 706` ```lemma le_spvec_empty2_sparse_row[rule_format]: "(sorted_spvec b) \ (le_spvec (b,[]) = (sparse_row_vector b <= 0))" ``` obua@15009 ` 707` ``` apply (induct b) ``` obua@15009 ` 708` ``` apply (simp_all add: sorted_spvec_cons1) ``` obua@15009 ` 709` ``` apply (intro strip) ``` obua@15009 ` 710` ``` apply (subst disj_matrices_add_le_zero) ``` obua@15009 ` 711` ``` apply (simp add: disj_matrices_commute disj_sparse_row_singleton sorted_spvec_cons1) ``` obua@15009 ` 712` ``` apply (rule_tac y = "snd a" in disj_sparse_row_singleton[OF order_refl]) ``` obua@15009 ` 713` ``` apply (simp_all) ``` obua@15009 ` 714` ``` done ``` obua@15009 ` 715` obua@15009 ` 716` ```lemma le_spvec_empty1_sparse_row[rule_format]: "(sorted_spvec b) \ (le_spvec ([],b) = (0 <= sparse_row_vector b))" ``` obua@15009 ` 717` ``` apply (induct b) ``` obua@15009 ` 718` ``` apply (simp_all add: sorted_spvec_cons1) ``` obua@15009 ` 719` ``` apply (intro strip) ``` obua@15009 ` 720` ``` apply (subst disj_matrices_add_zero_le) ``` obua@15009 ` 721` ``` apply (simp add: disj_matrices_commute disj_sparse_row_singleton sorted_spvec_cons1) ``` obua@15009 ` 722` ``` apply (rule_tac y = "snd a" in disj_sparse_row_singleton[OF order_refl]) ``` obua@15009 ` 723` ``` apply (simp_all) ``` obua@15009 ` 724` ``` done ``` obua@15009 ` 725` obua@15009 ` 726` ```lemma le_spmat_iff_sparse_row_le[rule_format]: "(sorted_spvec A) \ (sorted_spmat A) \ (sorted_spvec B) \ (sorted_spmat B) \ ``` obua@15009 ` 727` ``` le_spmat(A, B) = (sparse_row_matrix A <= sparse_row_matrix B)" ``` obua@15009 ` 728` ``` apply (rule le_spmat.induct) ``` obua@15009 ` 729` ``` 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] ``` obua@15009 ` 730` ``` disj_matrices_commute sorted_spvec_cons1 le_spvec_empty2_sparse_row le_spvec_empty1_sparse_row)+ ``` obua@15009 ` 731` ``` apply (rule conjI, intro strip) ``` obua@15009 ` 732` ``` apply (simp add: sorted_spvec_cons1) ``` obua@15009 ` 733` ``` apply (subst disj_matrices_add_x_le) ``` obua@15009 ` 734` ``` apply (rule disj_matrices_add_x) ``` obua@15009 ` 735` ``` apply (simp add: disj_move_sparse_row_vector_twice) ``` obua@15009 ` 736` ``` apply (simp add: disj_move_sparse_vec_mat[OF less_imp_le] disj_matrices_commute) ``` obua@15009 ` 737` ``` apply (simp add: disj_move_sparse_vec_mat[OF order_refl] disj_matrices_commute) ``` obua@15009 ` 738` ``` apply (simp, blast) ``` obua@15009 ` 739` ``` apply (intro strip, rule conjI, intro strip) ``` obua@15009 ` 740` ``` apply (simp add: sorted_spvec_cons1) ``` obua@15009 ` 741` ``` apply (subst disj_matrices_add_le_x) ``` obua@15009 ` 742` ``` apply (simp add: disj_move_sparse_vec_mat[OF order_refl]) ``` obua@15009 ` 743` ``` apply (rule disj_matrices_x_add) ``` obua@15009 ` 744` ``` apply (simp add: disj_move_sparse_row_vector_twice) ``` obua@15009 ` 745` ``` apply (simp add: disj_move_sparse_vec_mat[OF less_imp_le] disj_matrices_commute) ``` obua@15009 ` 746` ``` apply (simp, blast) ``` obua@15009 ` 747` ``` apply (intro strip) ``` obua@15009 ` 748` ``` apply (case_tac "a=aa") ``` obua@15009 ` 749` ``` apply (simp_all) ``` obua@15009 ` 750` ``` apply (subst disj_matrices_add) ``` obua@15009 ` 751` ``` apply (simp_all add: disj_matrices_commute disj_move_sparse_vec_mat[OF order_refl]) ``` obua@15009 ` 752` ``` apply (simp add: sorted_spvec_cons1 le_spvec_iff_sparse_row_le) ``` obua@15009 ` 753` ``` done ``` obua@15009 ` 754` obua@15009 ` 755` ```term smult_spvec ``` obua@15009 ` 756` ```term addmult_spvec ``` obua@15009 ` 757` ```term add_spvec ``` obua@15009 ` 758` ```term mult_spvec_spmat ``` obua@15009 ` 759` ```term mult_spmat ``` obua@15009 ` 760` ```term add_spmat ``` obua@15009 ` 761` ```term le_spvec ``` obua@15009 ` 762` ```term le_spmat ``` obua@15009 ` 763` ```term sorted_spvec ``` obua@15009 ` 764` ```term sorted_spmat ``` obua@15009 ` 765` obua@15009 ` 766` ```thm sparse_row_mult_spmat ``` obua@15009 ` 767` ```thm sparse_row_add_spmat ``` obua@15009 ` 768` ```thm le_spmat_iff_sparse_row_le ``` obua@15009 ` 769` obua@15009 ` 770` ```thm sorted_spvec_mult_spmat ``` obua@15009 ` 771` ```thm sorted_spmat_mult_spmat ``` obua@15009 ` 772` ```thm sorted_spvec_add_spmat ``` obua@15009 ` 773` ```thm sorted_spmat_add_spmat ``` obua@15009 ` 774` obua@15009 ` 775` ```thm smult_spvec_empty ``` obua@15009 ` 776` ```thm smult_spvec_cons ``` obua@15009 ` 777` ```thm addmult_spvec.simps ``` obua@15009 ` 778` ```thm add_spvec.simps ``` obua@15009 ` 779` ```thm add_spmat.simps ``` obua@15009 ` 780` ```thm mult_spvec_spmat.simps ``` obua@15009 ` 781` ```thm mult_spmat.simps ``` obua@15009 ` 782` ```thm le_spvec.simps ``` obua@15009 ` 783` ```thm le_spmat.simps ``` obua@15009 ` 784` ```thm sorted_spvec.simps ``` obua@15009 ` 785` ```thm sorted_spmat.simps ``` obua@15009 ` 786` obua@15009 ` 787` ```end ``` obua@15009 ` 788` obua@15009 ` 789` obua@15009 ` 790`