equal
deleted
inserted
replaced
873 apply (subst nrows_le) |
873 apply (subst nrows_le) |
874 apply (simp add: singleton_matrix_def, auto) |
874 apply (simp add: singleton_matrix_def, auto) |
875 apply (subst RepAbs_matrix) |
875 apply (subst RepAbs_matrix) |
876 apply auto |
876 apply auto |
877 apply (simp add: Suc_le_eq) |
877 apply (simp add: Suc_le_eq) |
878 apply (rule not_leE) |
878 apply (rule not_le_imp_less) |
879 apply (subst nrows_le) |
879 apply (subst nrows_le) |
880 by simp |
880 by simp |
881 qed |
881 qed |
882 |
882 |
883 lemma ncols_singleton[simp]: "ncols(singleton_matrix j i e) = (if e = 0 then 0 else Suc i)" |
883 lemma ncols_singleton[simp]: "ncols(singleton_matrix j i e) = (if e = 0 then 0 else Suc i)" |
889 apply (subst ncols_le) |
889 apply (subst ncols_le) |
890 apply (simp add: singleton_matrix_def, auto) |
890 apply (simp add: singleton_matrix_def, auto) |
891 apply (subst RepAbs_matrix) |
891 apply (subst RepAbs_matrix) |
892 apply auto |
892 apply auto |
893 apply (simp add: Suc_le_eq) |
893 apply (simp add: Suc_le_eq) |
894 apply (rule not_leE) |
894 apply (rule not_le_imp_less) |
895 apply (subst ncols_le) |
895 apply (subst ncols_le) |
896 by simp |
896 by simp |
897 qed |
897 qed |
898 |
898 |
899 lemma combine_singleton: "f 0 0 = 0 \<Longrightarrow> combine_matrix f (singleton_matrix j i a) (singleton_matrix j i b) = singleton_matrix j i (f a b)" |
899 lemma combine_singleton: "f 0 0 = 0 \<Longrightarrow> combine_matrix f (singleton_matrix j i a) (singleton_matrix j i b) = singleton_matrix j i (f a b)" |