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.78  by (auto simp add: disj_matrices_add[of B A 0 C,simplified] disj_matrices_commute)
    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.97    apply (simp add: disj_matrices_def)
    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.105 -  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)
   1.106 -  apply (rule conjI, intro strip)
   1.107 -  apply (simp add: sorted_spvec_cons1)
   1.108 -  apply (subst disj_matrices_add_x_le)
   1.109 -  apply (simp add: disj_sparse_row_singleton[OF less_imp_le] disj_matrices_x_add disj_matrices_commute)
   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.114 -  apply (subst disj_matrices_add_le_x)
   1.115 -  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)
   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.120 -  apply (subst disj_matrices_add)
   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.137 +  apply (simp_all add: sorted_spvec_cons1 disj_matrices_add_le_zero disj_matrices_add_zero_le 
   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.141 +  apply (subst disj_matrices_add_x_le)
   1.142 +  apply (simp add: disj_sparse_row_singleton[OF less_imp_le] disj_matrices_x_add disj_matrices_commute)
   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.147 +  apply (subst disj_matrices_add_le_x)
   1.148 +  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)
   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.153 +  apply (subst disj_matrices_add)
   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.171    apply (simp_all add: sorted_spvec_cons1)
   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.177 -term addmult_spvec
   1.178 -term add_spvec
   1.179 -term mult_spvec_spmat
   1.180 -term mult_spmat
   1.181 -term add_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.210 -thm sparse_row_add_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.272 -thm sorted_spvec_add_spmat
   1.273 -thm sorted_spmat_add_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.279 +  by (simp add: diff_spmat_def sorted_spmat_minus_spmat sorted_spmat_add_spmat)
   1.280 +
   1.281 +lemma sorted_spvec_diff_spmat: "sorted_spvec A \<Longrightarrow> sorted_spvec B \<Longrightarrow> sorted_spvec (diff_spmat A B)"
   1.282 +  by (simp add: diff_spmat_def sorted_spvec_minus_spmat sorted_spvec_add_spmat)
   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.285 +  by (simp add: diff_spmat_def sparse_row_add_spmat sparse_row_matrix_minus)
   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.299 +  sparse_row_add_spmat sorted_spvec_add_spmat sorted_spmat_add_spmat
   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.310 -thm addmult_spvec.simps
   1.311 -thm add_spvec.simps
   1.312 -thm add_spmat.simps
   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.321 +  addmult_spvec.simps 
   1.322 +  smult_spvec_empty smult_spvec_cons
   1.323 +  add_spmat.simps add_spvec.simps
   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 -