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