equal
deleted
inserted
replaced
1003 apply (simp add: mult_matrix_n_def apply_matrix_def apply_infmatrix_def) |
1003 apply (simp add: mult_matrix_n_def apply_matrix_def apply_infmatrix_def) |
1004 apply (rule comb[of "Abs_matrix" "Abs_matrix"], auto, (rule ext)+) |
1004 apply (rule comb[of "Abs_matrix" "Abs_matrix"], auto, (rule ext)+) |
1005 apply (subst foldseq_almostzero[of _ j]) |
1005 apply (subst foldseq_almostzero[of _ j]) |
1006 apply (simp add: prems)+ |
1006 apply (simp add: prems)+ |
1007 apply (auto) |
1007 apply (auto) |
1008 proof - |
1008 apply (metis comm_monoid_add.mult_1 le_anti_sym le_diff_eq not_neg_nat zero_le_imp_of_nat zle_int) |
1009 fix k |
1009 done |
1010 fix l |
|
1011 assume a:"~neg(int l - int i)" |
|
1012 assume b:"nat (int l - int i) = 0" |
|
1013 from a b have a: "l = i" by(insert not_neg_nat[of "int l - int i"], simp add: a b) |
|
1014 assume c: "i \<noteq> l" |
|
1015 from c a show "fmul (Rep_matrix A k j) e = 0" by blast |
|
1016 qed |
|
1017 |
1010 |
1018 lemma mult_matrix_ext: |
1011 lemma mult_matrix_ext: |
1019 assumes |
1012 assumes |
1020 eprem: |
1013 eprem: |
1021 "? e. (! a b. a \<noteq> b \<longrightarrow> fmul a e \<noteq> fmul b e)" |
1014 "? e. (! a b. a \<noteq> b \<longrightarrow> fmul a e \<noteq> fmul b e)" |