src/HOL/Matrix/SparseMatrix.thy
 changeset 15178 5f621aa35c25 parent 15009 8c89f588c7aa child 15197 19e735596e51
```     1.1 --- a/src/HOL/Matrix/SparseMatrix.thy	Fri Sep 03 10:27:05 2004 +0200
1.2 +++ b/src/HOL/Matrix/SparseMatrix.thy	Fri Sep 03 17:10:36 2004 +0200
1.3 @@ -94,9 +94,62 @@
1.4    done
1.5
1.6  consts
1.7 +  abs_spvec :: "('a::lordered_ring) spvec \<Rightarrow> 'a spvec"
1.8 +  minus_spvec ::  "('a::lordered_ring) spvec \<Rightarrow> 'a spvec"
1.9    smult_spvec :: "('a::lordered_ring) \<Rightarrow> 'a spvec \<Rightarrow> 'a spvec"
1.10    addmult_spvec :: "('a::lordered_ring) * 'a spvec * 'a spvec \<Rightarrow> 'a spvec"
1.11
1.12 +primrec
1.13 +  "minus_spvec [] = []"
1.14 +  "minus_spvec (a#as) = (fst a, -(snd a))#(minus_spvec as)"
1.15 +
1.16 +primrec
1.17 +  "abs_spvec [] = []"
1.18 +  "abs_spvec (a#as) = (fst a, abs (snd a))#(abs_spvec as)"
1.19 +
1.20 +lemma sparse_row_vector_minus:
1.21 +  "sparse_row_vector (minus_spvec v) = - (sparse_row_vector v)"
1.22 +  apply (induct v)
1.23 +  apply (simp_all add: sparse_row_vector_cons)
1.24 +  apply (simp add: Rep_matrix_inject[symmetric])
1.25 +  apply (rule ext)+
1.26 +  apply simp
1.27 +  done
1.28 +
1.29 +lemma sparse_row_vector_abs:
1.30 +  "sorted_spvec v \<Longrightarrow> sparse_row_vector (abs_spvec v) = abs (sparse_row_vector v)"
1.31 +  apply (induct v)
1.32 +  apply (simp_all add: sparse_row_vector_cons)
1.33 +  apply (frule_tac sorted_spvec_cons1, simp)
1.34 +  apply (simp only: Rep_matrix_inject[symmetric])
1.35 +  apply (rule ext)+
1.36 +  apply auto
1.37 +  apply (subgoal_tac "Rep_matrix (sparse_row_vector list) 0 a = 0")
1.38 +  apply (simp)
1.39 +  apply (rule sorted_sparse_row_vector_zero)
1.40 +  apply auto
1.41 +  done
1.42 +
1.43 +lemma sorted_spvec_minus_spvec:
1.44 +  "sorted_spvec v \<Longrightarrow> sorted_spvec (minus_spvec v)"
1.45 +  apply (induct v)
1.46 +  apply (simp)
1.47 +  apply (frule sorted_spvec_cons1, simp)
1.48 +  apply (simp add: sorted_spvec.simps)
1.49 +  apply (case_tac list)
1.50 +  apply (simp_all)
1.51 +  done
1.52 +
1.53 +lemma sorted_spvec_abs_spvec:
1.54 +  "sorted_spvec v \<Longrightarrow> sorted_spvec (abs_spvec v)"
1.55 +  apply (induct v)
1.56 +  apply (simp)
1.57 +  apply (frule sorted_spvec_cons1, simp)
1.58 +  apply (simp add: sorted_spvec.simps)
1.59 +  apply (case_tac list)
1.60 +  apply (simp_all)
1.61 +  done
1.62 +
1.63  defs
1.64    smult_spvec_def: "smult_spvec y arr == map (% a. (fst a, y * snd a)) arr"
1.65
1.66 @@ -542,9 +595,6 @@
1.67    else
1.68      (le_spvec(snd a, snd b) & le_spmat (as, bs))))"
1.69
1.70 -lemma spec2: "! j i. P j i \<Longrightarrow> P j i" by blast
1.71 -lemma neg_imp: "(\<not> Q \<longrightarrow> \<not> P) \<Longrightarrow> P \<longrightarrow> Q" by blast
1.72 -
1.73  constdefs
1.74    disj_matrices :: "('a::zero) matrix \<Rightarrow> 'a matrix \<Rightarrow> bool"
1.75    "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))"
1.76 @@ -597,22 +647,6 @@
1.77    (B + A <= C) = (A <= C &  (B::('a::lordered_ab_group) matrix) <= 0)"
1.79
1.80 -lemma singleton_le_zero[simp]: "(singleton_matrix j i x <= 0) = (x <= (0::'a::{order,zero}))"
1.81 -  apply (auto)
1.82 -  apply (simp add: le_matrix_def)
1.83 -  apply (drule_tac j=j and i=i in spec2)
1.84 -  apply (simp)
1.85 -  apply (simp add: le_matrix_def)
1.86 -  done
1.87 -
1.88 -lemma singleton_ge_zero[simp]: "(0 <= singleton_matrix j i x) = ((0::'a::{order,zero}) <= x)"
1.89 -  apply (auto)
1.90 -  apply (simp add: le_matrix_def)
1.91 -  apply (drule_tac j=j and i=i in spec2)
1.92 -  apply (simp)
1.93 -  apply (simp add: le_matrix_def)
1.94 -  done
1.95 -
1.96  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)"
1.98    apply (rule conjI)
1.99 @@ -641,27 +675,6 @@
1.100  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)"
1.101    by (auto simp add: disj_matrices_def)
1.102
1.103 -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)"
1.104 -  apply (rule le_spvec.induct)
1.106 -  apply (rule conjI, intro strip)
1.107 -  apply (simp add: sorted_spvec_cons1)
1.110 -  apply (simp add: disj_sparse_row_singleton[OF order_refl] disj_matrices_commute)
1.111 -  apply (simp, blast)
1.112 -  apply (intro strip, rule conjI, intro strip)
1.113 -  apply (simp add: sorted_spvec_cons1)
1.116 -  apply (blast)
1.117 -  apply (intro strip)
1.118 -  apply (simp add: sorted_spvec_cons1)
1.119 -  apply (case_tac "a=aa", simp_all)
1.121 -  apply (simp_all add: disj_sparse_row_singleton[OF order_refl] disj_matrices_commute)
1.122 -  done
1.123 -
1.124  lemma disj_move_sparse_vec_mat[simplified disj_matrices_commute]:
1.125    "j <= a \<Longrightarrow> sorted_spvec((a,c)#as) \<Longrightarrow> disj_matrices (move_matrix (sparse_row_vector b) (int j) i) (sparse_row_matrix as)"
1.126    apply (auto simp add: neg_def disj_matrices_def)
1.127 @@ -685,24 +698,28 @@
1.128    apply (rule nrows, rule order_trans[of _ 1], simp, drule nrows_notzero, drule less_le_trans[OF _ nrows_spvec], arith)+
1.129    done
1.130
1.131 -lemma move_matrix_le_zero[simp]: "0 <= j \<Longrightarrow> 0 <= i \<Longrightarrow> (move_matrix A j i <= 0) = (A <= (0::('a::{order,zero}) matrix))"
1.132 -  apply (auto simp add: le_matrix_def neg_def)
1.133 -  apply (drule_tac j="ja+(nat j)" and i="ia+(nat i)" in spec2)
1.134 -  apply (auto)
1.135 +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)"
1.136 +  apply (rule le_spvec.induct)
1.138 +    disj_sparse_row_singleton[OF order_refl] disj_matrices_commute)
1.139 +  apply (rule conjI, intro strip)
1.140 +  apply (simp add: sorted_spvec_cons1)
1.143 +  apply (simp add: disj_sparse_row_singleton[OF order_refl] disj_matrices_commute)
1.144 +  apply (simp, blast)
1.145 +  apply (intro strip, rule conjI, intro strip)
1.146 +  apply (simp add: sorted_spvec_cons1)
1.149 +  apply (blast)
1.150 +  apply (intro strip)
1.151 +  apply (simp add: sorted_spvec_cons1)
1.152 +  apply (case_tac "a=aa", simp_all)
1.154 +  apply (simp_all add: disj_sparse_row_singleton[OF order_refl] disj_matrices_commute)
1.155    done
1.156
1.157 -lemma move_matrix_zero_le[simp]: "0 <= j \<Longrightarrow> 0 <= i \<Longrightarrow> (0 <= move_matrix A j i) = ((0::('a::{order,zero}) matrix) <= A)"
1.158 -  apply (auto simp add: le_matrix_def neg_def)
1.159 -  apply (drule_tac j="ja+(nat j)" and i="ia+(nat i)" in spec2)
1.160 -  apply (auto)
1.161 -  done
1.162 -
1.163 -lemma move_matrix_le_move_matrix_iff[simp]: "0 <= j \<Longrightarrow> 0 <= i \<Longrightarrow> (move_matrix A j i <= move_matrix B j i) = (A <= (B::('a::{order,zero}) matrix))"
1.164 -  apply (auto simp add: le_matrix_def neg_def)
1.165 -  apply (drule_tac j="ja+(nat j)" and i="ia+(nat i)" in spec2)
1.166 -  apply (auto)
1.167 -  done
1.168 -
1.169  lemma le_spvec_empty2_sparse_row[rule_format]: "(sorted_spvec b) \<longrightarrow> (le_spvec (b,[]) = (sparse_row_vector b <= 0))"
1.170    apply (induct b)
1.172 @@ -752,39 +769,169 @@
1.173    apply (simp add: sorted_spvec_cons1 le_spvec_iff_sparse_row_le)
1.174    done
1.175
1.176 -term smult_spvec
1.179 -term mult_spvec_spmat
1.180 -term mult_spmat
1.182 -term le_spvec
1.183 -term le_spmat
1.184 -term sorted_spvec
1.185 -term sorted_spmat
1.186 +ML {* simp_depth_limit := 999 *}
1.187 +
1.188 +consts
1.189 +   abs_spmat :: "('a::lordered_ring) spmat \<Rightarrow> 'a spmat"
1.190 +   minus_spmat :: "('a::lordered_ring) spmat \<Rightarrow> 'a spmat"
1.191 +
1.192 +primrec
1.193 +  "abs_spmat [] = []"
1.194 +  "abs_spmat (a#as) = (fst a, abs_spvec (snd a))#(abs_spmat as)"
1.195 +
1.196 +primrec
1.197 +  "minus_spmat [] = []"
1.198 +  "minus_spmat (a#as) = (fst a, minus_spvec (snd a))#(minus_spmat as)"
1.199 +
1.200 +lemma sparse_row_matrix_minus:
1.201 +  "sparse_row_matrix (minus_spmat A) = - (sparse_row_matrix A)"
1.202 +  apply (induct A)
1.203 +  apply (simp_all add: sparse_row_vector_minus sparse_row_matrix_cons)
1.204 +  apply (subst Rep_matrix_inject[symmetric])
1.205 +  apply (rule ext)+
1.206 +  apply simp
1.207 +  done
1.208
1.209 -thm sparse_row_mult_spmat
1.211 -thm le_spmat_iff_sparse_row_le
1.212 +lemma Rep_sparse_row_vector_zero: "x \<noteq> 0 \<Longrightarrow> Rep_matrix (sparse_row_vector v) x y = 0"
1.213 +proof -
1.214 +  assume x:"x \<noteq> 0"
1.215 +  have r:"nrows (sparse_row_vector v) <= Suc 0" by (rule nrows_spvec)
1.216 +  show ?thesis
1.217 +    apply (rule nrows)
1.218 +    apply (subgoal_tac "Suc 0 <= x")
1.219 +    apply (insert r)
1.220 +    apply (simp only:)
1.221 +    apply (insert x)
1.222 +    apply arith
1.223 +    done
1.224 +qed
1.225 +
1.226 +lemma sparse_row_matrix_abs:
1.227 +  "sorted_spvec A \<Longrightarrow> sorted_spmat A \<Longrightarrow> sparse_row_matrix (abs_spmat A) = abs (sparse_row_matrix A)"
1.228 +  apply (induct A)
1.229 +  apply (simp_all add: sparse_row_vector_abs sparse_row_matrix_cons)
1.230 +  apply (frule_tac sorted_spvec_cons1, simp)
1.231 +  apply (subst Rep_matrix_inject[symmetric])
1.232 +  apply (rule ext)+
1.233 +  apply auto
1.234 +  apply (case_tac "x=a")
1.235 +  apply (simp)
1.236 +  apply (subst sorted_sparse_row_matrix_zero)
1.237 +  apply auto
1.238 +  apply (subst Rep_sparse_row_vector_zero)
1.239 +  apply (simp_all add: neg_def)
1.240 +  done
1.241 +
1.242 +lemma sorted_spvec_minus_spmat: "sorted_spvec A \<Longrightarrow> sorted_spvec (minus_spmat A)"
1.243 +  apply (induct A)
1.244 +  apply (simp)
1.245 +  apply (frule sorted_spvec_cons1, simp)
1.246 +  apply (simp add: sorted_spvec.simps)
1.247 +  apply (case_tac list)
1.248 +  apply (simp_all)
1.249 +  done
1.250 +
1.251 +lemma sorted_spvec_abs_spmat: "sorted_spvec A \<Longrightarrow> sorted_spvec (abs_spmat A)"
1.252 +  apply (induct A)
1.253 +  apply (simp)
1.254 +  apply (frule sorted_spvec_cons1, simp)
1.255 +  apply (simp add: sorted_spvec.simps)
1.256 +  apply (case_tac list)
1.257 +  apply (simp_all)
1.258 +  done
1.259 +
1.260 +lemma sorted_spmat_minus_spmat: "sorted_spmat A \<Longrightarrow> sorted_spmat (minus_spmat A)"
1.261 +  apply (induct A)
1.262 +  apply (simp_all add: sorted_spvec_minus_spvec)
1.263 +  done
1.264 +
1.265 +lemma sorted_spmat_abs_spmat: "sorted_spmat A \<Longrightarrow> sorted_spmat (abs_spmat A)"
1.266 +  apply (induct A)
1.267 +  apply (simp_all add: sorted_spvec_abs_spvec)
1.268 +  done
1.269
1.270 -thm sorted_spvec_mult_spmat
1.271 -thm sorted_spmat_mult_spmat
1.274 +constdefs
1.275 +  diff_spmat :: "('a::lordered_ring) spmat \<Rightarrow> 'a spmat \<Rightarrow> 'a spmat"
1.276 +  "diff_spmat A B == add_spmat (A, minus_spmat B)"
1.277 +
1.278 +lemma sorted_spmat_diff_spmat: "sorted_spmat A \<Longrightarrow> sorted_spmat B \<Longrightarrow> sorted_spmat (diff_spmat A B)"
1.280 +
1.281 +lemma sorted_spvec_diff_spmat: "sorted_spvec A \<Longrightarrow> sorted_spvec B \<Longrightarrow> sorted_spvec (diff_spmat A B)"
1.283 +
1.284 +lemma sparse_row_diff_spmat: "sparse_row_matrix (diff_spmat A B ) = (sparse_row_matrix A) - (sparse_row_matrix B)"
1.286 +
1.287 +constdefs
1.288 +  sorted_sparse_matrix :: "'a spmat \<Rightarrow> bool"
1.289 +  "sorted_sparse_matrix A == (sorted_spvec A) & (sorted_spmat A)"
1.290 +
1.291 +lemma sorted_sparse_matrix_imp_spvec: "sorted_sparse_matrix A \<Longrightarrow> sorted_spvec A"
1.292 +  by (simp add: sorted_sparse_matrix_def)
1.293 +
1.294 +lemma sorted_sparse_matrix_imp_spmat: "sorted_sparse_matrix A \<Longrightarrow> sorted_spmat A"
1.295 +  by (simp add: sorted_sparse_matrix_def)
1.296 +
1.297 +lemmas sparse_row_matrix_op_simps =
1.298 +  sorted_sparse_matrix_imp_spmat sorted_sparse_matrix_imp_spvec
1.300 +  sparse_row_diff_spmat sorted_spvec_diff_spmat sorted_spmat_diff_spmat
1.301 +  sparse_row_matrix_minus sorted_spvec_minus_spmat sorted_spmat_minus_spmat
1.302 +  sparse_row_mult_spmat sorted_spvec_mult_spmat sorted_spmat_mult_spmat
1.303 +  sparse_row_matrix_abs sorted_spvec_abs_spmat sorted_spmat_abs_spmat
1.304 +  le_spmat_iff_sparse_row_le
1.305 +
1.306 +lemma zero_eq_Numeral0: "(0::_::number_ring) = Numeral0" by simp
1.307
1.308 -thm smult_spvec_empty
1.309 -thm smult_spvec_cons
1.313 -thm mult_spvec_spmat.simps
1.314 -thm mult_spmat.simps
1.315 -thm le_spvec.simps
1.316 -thm le_spmat.simps
1.317 -thm sorted_spvec.simps
1.318 -thm sorted_spmat.simps
1.319 +lemmas sparse_row_matrix_arith_simps[simplified zero_eq_Numeral0] =
1.320 +  mult_spmat.simps mult_spvec_spmat.simps
1.322 +  smult_spvec_empty smult_spvec_cons
1.324 +  minus_spmat.simps minus_spvec.simps
1.325 +  abs_spmat.simps abs_spvec.simps
1.326 +  diff_spmat_def
1.327 +  le_spmat.simps le_spvec.simps
1.328 +
1.329 +lemmas sorted_sp_simps =
1.330 +  sorted_spvec.simps
1.331 +  sorted_spmat.simps
1.332 +  sorted_sparse_matrix_def
1.333 +
1.334 +lemma bool1: "(\<not> True) = False"  by blast
1.335 +lemma bool2: "(\<not> False) = True"  by blast
1.336 +lemma bool3: "((P\<Colon>bool) \<and> True) = P" by blast
1.337 +lemma bool4: "(True \<and> (P\<Colon>bool)) = P" by blast
1.338 +lemma bool5: "((P\<Colon>bool) \<and> False) = False" by blast
1.339 +lemma bool6: "(False \<and> (P\<Colon>bool)) = False" by blast
1.340 +lemma bool7: "((P\<Colon>bool) \<or> True) = True" by blast
1.341 +lemma bool8: "(True \<or> (P\<Colon>bool)) = True" by blast
1.342 +lemma bool9: "((P\<Colon>bool) \<or> False) = P" by blast
1.343 +lemma bool10: "(False \<or> (P\<Colon>bool)) = P" by blast
1.344 +lemmas boolarith = bool1 bool2 bool3 bool4 bool5 bool6 bool7 bool8 bool9 bool10
1.345 +
1.346 +lemma if_case_eq: "(if b then x else y) = (case b of True => x | False => y)" by simp
1.347 +
1.348 +lemma spm_linprog_dual_estimate_1:
1.349 +  assumes
1.350 +  "sorted_sparse_matrix A1"
1.351 +  "sorted_sparse_matrix A2"
1.352 +  "sorted_sparse_matrix c1"
1.353 +  "sorted_sparse_matrix c2"
1.354 +  "sorted_sparse_matrix y"
1.355 +  "sorted_spvec b"
1.356 +  "sorted_spvec r"
1.357 +  "le_spmat ([], y)"
1.358 +  "A * x \<le> sparse_row_matrix (b::('a::lordered_ring) spmat)"
1.359 +  "sparse_row_matrix A1 <= A"
1.360 +  "A <= sparse_row_matrix A2"
1.361 +  "sparse_row_matrix c1 <= c"
1.362 +  "c <= sparse_row_matrix c2"
1.363 +  "abs x \<le> sparse_row_matrix r"
1.364 +  shows
1.365 +  "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),
1.366 +  abs_spmat (diff_spmat (mult_spmat y A1) c1)), diff_spmat c2 c1)) r))"
1.367 +  by (insert prems, simp add: sparse_row_matrix_op_simps linprog_dual_estimate_1[where A=A])
1.368
1.369  end
1.370 -
1.371 -
1.372 -
```