122 apply (simp_all add: sparse_row_vector_cons) |
122 apply (simp_all add: sparse_row_vector_cons) |
123 apply (frule_tac sorted_spvec_cons1, simp) |
123 apply (frule_tac sorted_spvec_cons1, simp) |
124 apply (simp only: Rep_matrix_inject[symmetric]) |
124 apply (simp only: Rep_matrix_inject[symmetric]) |
125 apply (rule ext)+ |
125 apply (rule ext)+ |
126 apply auto |
126 apply auto |
127 apply (subgoal_tac "Rep_matrix (sparse_row_vector list) 0 a = 0") |
127 apply (subgoal_tac "Rep_matrix (sparse_row_vector v) 0 a = 0") |
128 apply (simp) |
128 apply (simp) |
129 apply (rule sorted_sparse_row_vector_zero) |
129 apply (rule sorted_sparse_row_vector_zero) |
130 apply auto |
130 apply auto |
131 done |
131 done |
132 |
132 |
133 lemma sorted_spvec_minus_spvec: |
133 lemma sorted_spvec_minus_spvec: |
134 "sorted_spvec v \<Longrightarrow> sorted_spvec (minus_spvec v)" |
134 "sorted_spvec v \<Longrightarrow> sorted_spvec (minus_spvec v)" |
135 apply (induct v) |
135 apply (induct v) |
136 apply (simp) |
136 apply (simp) |
137 apply (frule sorted_spvec_cons1, simp) |
137 apply (frule sorted_spvec_cons1, simp) |
138 apply (simp add: sorted_spvec.simps) |
138 apply (simp add: sorted_spvec.simps split:list.split_asm) |
139 apply (case_tac list) |
|
140 apply (simp_all) |
|
141 done |
139 done |
142 |
140 |
143 lemma sorted_spvec_abs_spvec: |
141 lemma sorted_spvec_abs_spvec: |
144 "sorted_spvec v \<Longrightarrow> sorted_spvec (abs_spvec v)" |
142 "sorted_spvec v \<Longrightarrow> sorted_spvec (abs_spvec v)" |
145 apply (induct v) |
143 apply (induct v) |
146 apply (simp) |
144 apply (simp) |
147 apply (frule sorted_spvec_cons1, simp) |
145 apply (frule sorted_spvec_cons1, simp) |
148 apply (simp add: sorted_spvec.simps) |
146 apply (simp add: sorted_spvec.simps split:list.split_asm) |
149 apply (case_tac list) |
|
150 apply (simp_all) |
|
151 done |
147 done |
152 |
148 |
153 defs |
149 defs |
154 smult_spvec_def: "smult_spvec y arr == map (% a. (fst a, y * snd a)) arr" |
150 smult_spvec_def: "smult_spvec y arr == map (% a. (fst a, y * snd a)) arr" |
155 |
151 |
191 done |
187 done |
192 |
188 |
193 lemma sorted_smult_spvec[rule_format]: "sorted_spvec a \<Longrightarrow> sorted_spvec (smult_spvec y a)" |
189 lemma sorted_smult_spvec[rule_format]: "sorted_spvec a \<Longrightarrow> sorted_spvec (smult_spvec y a)" |
194 apply (auto simp add: smult_spvec_def) |
190 apply (auto simp add: smult_spvec_def) |
195 apply (induct a) |
191 apply (induct a) |
196 apply (auto simp add: sorted_spvec.simps) |
192 apply (auto simp add: sorted_spvec.simps split:list.split_asm) |
197 apply (case_tac list) |
|
198 apply (auto) |
|
199 done |
193 done |
200 |
194 |
201 lemma sorted_spvec_addmult_spvec_helper: "\<lbrakk>sorted_spvec (addmult_spvec (y, (a, b) # arr, brr)); aa < a; sorted_spvec ((a, b) # arr); |
195 lemma sorted_spvec_addmult_spvec_helper: "\<lbrakk>sorted_spvec (addmult_spvec (y, (a, b) # arr, brr)); aa < a; sorted_spvec ((a, b) # arr); |
202 sorted_spvec ((aa, ba) # brr)\<rbrakk> \<Longrightarrow> sorted_spvec ((aa, y * ba) # addmult_spvec (y, (a, b) # arr, brr))" |
196 sorted_spvec ((aa, ba) # brr)\<rbrakk> \<Longrightarrow> sorted_spvec ((aa, y * ba) # addmult_spvec (y, (a, b) # arr, brr))" |
203 apply (induct brr) |
197 apply (induct brr) |
368 lemma sorted_spvec_mult_spmat[rule_format]: |
362 lemma sorted_spvec_mult_spmat[rule_format]: |
369 "sorted_spvec (A::('a::lordered_ring) spmat) \<longrightarrow> sorted_spvec (mult_spmat A B)" |
363 "sorted_spvec (A::('a::lordered_ring) spmat) \<longrightarrow> sorted_spvec (mult_spmat A B)" |
370 apply (induct A) |
364 apply (induct A) |
371 apply (auto) |
365 apply (auto) |
372 apply (drule sorted_spvec_cons1, simp) |
366 apply (drule sorted_spvec_cons1, simp) |
373 apply (case_tac list) |
367 apply (case_tac A) |
374 apply (auto simp add: sorted_spvec.simps) |
368 apply (auto simp add: sorted_spvec.simps) |
375 done |
369 done |
376 |
370 |
377 lemma sorted_spmat_mult_spmat[rule_format]: |
371 lemma sorted_spmat_mult_spmat[rule_format]: |
378 "sorted_spmat (B::('a::lordered_ring) spmat) \<longrightarrow> sorted_spmat (mult_spmat A B)" |
372 "sorted_spmat (B::('a::lordered_ring) spmat) \<longrightarrow> sorted_spmat (mult_spmat A B)" |
819 |
813 |
820 lemma sorted_spvec_minus_spmat: "sorted_spvec A \<Longrightarrow> sorted_spvec (minus_spmat A)" |
814 lemma sorted_spvec_minus_spmat: "sorted_spvec A \<Longrightarrow> sorted_spvec (minus_spmat A)" |
821 apply (induct A) |
815 apply (induct A) |
822 apply (simp) |
816 apply (simp) |
823 apply (frule sorted_spvec_cons1, simp) |
817 apply (frule sorted_spvec_cons1, simp) |
824 apply (simp add: sorted_spvec.simps) |
818 apply (simp add: sorted_spvec.simps split:list.split_asm) |
825 apply (case_tac list) |
|
826 apply (simp_all) |
|
827 done |
819 done |
828 |
820 |
829 lemma sorted_spvec_abs_spmat: "sorted_spvec A \<Longrightarrow> sorted_spvec (abs_spmat A)" |
821 lemma sorted_spvec_abs_spmat: "sorted_spvec A \<Longrightarrow> sorted_spvec (abs_spmat A)" |
830 apply (induct A) |
822 apply (induct A) |
831 apply (simp) |
823 apply (simp) |
832 apply (frule sorted_spvec_cons1, simp) |
824 apply (frule sorted_spvec_cons1, simp) |
833 apply (simp add: sorted_spvec.simps) |
825 apply (simp add: sorted_spvec.simps split:list.split_asm) |
834 apply (case_tac list) |
|
835 apply (simp_all) |
|
836 done |
826 done |
837 |
827 |
838 lemma sorted_spmat_minus_spmat: "sorted_spmat A \<Longrightarrow> sorted_spmat (minus_spmat A)" |
828 lemma sorted_spmat_minus_spmat: "sorted_spmat A \<Longrightarrow> sorted_spmat (minus_spmat A)" |
839 apply (induct A) |
829 apply (induct A) |
840 apply (simp_all add: sorted_spvec_minus_spvec) |
830 apply (simp_all add: sorted_spvec_minus_spvec) |