equal
deleted
inserted
replaced
336 apply (rule ext)+ |
336 apply (rule ext)+ |
337 apply (simp) |
337 apply (simp) |
338 apply (subst Rep_matrix_mult) |
338 apply (subst Rep_matrix_mult) |
339 apply (rule_tac j1=aa in ssubst[OF foldseq_almostzero]) |
339 apply (rule_tac j1=aa in ssubst[OF foldseq_almostzero]) |
340 apply (simp_all) |
340 apply (simp_all) |
|
341 apply (intro strip, rule conjI) |
341 apply (intro strip) |
342 apply (intro strip) |
|
343 apply (drule_tac max_helper) |
|
344 apply (simp) |
|
345 apply (auto) |
342 apply (rule zero_imp_mult_zero) |
346 apply (rule zero_imp_mult_zero) |
343 apply (rule disjI2) |
347 apply (rule disjI2) |
344 apply (rule nrows) |
348 apply (rule nrows) |
345 apply (rule order_trans[of _ 1]) |
349 apply (rule order_trans[of _ 1]) |
346 apply auto |
350 apply (simp) |
|
351 apply (simp) |
347 done |
352 done |
348 qed |
353 qed |
349 |
354 |
350 lemma sorted_mult_spvec_spmat[rule_format]: |
355 lemma sorted_mult_spvec_spmat[rule_format]: |
351 "sorted_spvec (c::('a::lordered_ring) spvec) \<longrightarrow> sorted_spmat B \<longrightarrow> sorted_spvec (mult_spvec_spmat (c, a, B))" |
356 "sorted_spvec (c::('a::lordered_ring) spvec) \<longrightarrow> sorted_spmat B \<longrightarrow> sorted_spvec (mult_spvec_spmat (c, a, B))" |