--- a/src/HOL/Matrix/Matrix.thy Mon Feb 27 10:56:36 2012 +0100
+++ b/src/HOL/Matrix/Matrix.thy Mon Feb 27 11:38:56 2012 +0100
@@ -849,7 +849,7 @@
"singleton_matrix j i a == Abs_matrix(% m n. if j = m & i = n then a else 0)"
definition move_matrix :: "('a::zero) matrix \<Rightarrow> int \<Rightarrow> int \<Rightarrow> 'a matrix" where
- "move_matrix A y x == Abs_matrix(% j i. if (neg ((int j)-y)) | (neg ((int i)-x)) then 0 else Rep_matrix A (nat ((int j)-y)) (nat ((int i)-x)))"
+ "move_matrix A y x == Abs_matrix(% j i. if (((int j)-y) < 0) | (((int i)-x) < 0) then 0 else Rep_matrix A (nat ((int j)-y)) (nat ((int i)-x)))"
definition take_rows :: "('a::zero) matrix \<Rightarrow> nat \<Rightarrow> 'a matrix" where
"take_rows A r == Abs_matrix(% j i. if (j < r) then (Rep_matrix A j i) else 0)"
@@ -930,7 +930,7 @@
lemma Rep_move_matrix[simp]:
"Rep_matrix (move_matrix A y x) j i =
- (if (neg ((int j)-y)) | (neg ((int i)-x)) then 0 else Rep_matrix A (nat((int j)-y)) (nat((int i)-x)))"
+ (if (((int j)-y) < 0) | (((int i)-x) < 0) then 0 else Rep_matrix A (nat((int j)-y)) (nat((int i)-x)))"
apply (simp add: move_matrix_def)
apply (auto)
by (subst RepAbs_matrix,
@@ -959,8 +959,8 @@
apply (case_tac "j + int u < 0")
apply (simp, arith)
apply (case_tac "i + int v < 0")
- apply (simp add: neg_def, arith)
- apply (simp add: neg_def)
+ apply (simp, arith)
+ apply simp
apply arith
done
@@ -1016,7 +1016,6 @@
apply (subst foldseq_almostzero[of _ j])
apply (simp add: assms)+
apply (auto)
- apply (metis add_0 le_antisym le_diff_eq not_neg_nat zero_le_imp_of_nat zle_int)
done
lemma mult_matrix_ext:
@@ -1440,19 +1439,19 @@
done
lemma move_matrix_le_zero[simp]: "0 <= j \<Longrightarrow> 0 <= i \<Longrightarrow> (move_matrix A j i <= 0) = (A <= (0::('a::{order,zero}) matrix))"
- apply (auto simp add: le_matrix_def neg_def)
+ apply (auto simp add: le_matrix_def)
apply (drule_tac j="ja+(nat j)" and i="ia+(nat i)" in spec2)
apply (auto)
done
lemma move_matrix_zero_le[simp]: "0 <= j \<Longrightarrow> 0 <= i \<Longrightarrow> (0 <= move_matrix A j i) = ((0::('a::{order,zero}) matrix) <= A)"
- apply (auto simp add: le_matrix_def neg_def)
+ apply (auto simp add: le_matrix_def)
apply (drule_tac j="ja+(nat j)" and i="ia+(nat i)" in spec2)
apply (auto)
done
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))"
- apply (auto simp add: le_matrix_def neg_def)
+ apply (auto simp add: le_matrix_def)
apply (drule_tac j="ja+(nat j)" and i="ia+(nat i)" in spec2)
apply (auto)
done
--- a/src/HOL/Matrix/SparseMatrix.thy Mon Feb 27 10:56:36 2012 +0100
+++ b/src/HOL/Matrix/SparseMatrix.thy Mon Feb 27 11:38:56 2012 +0100
@@ -97,7 +97,7 @@
apply (auto)
apply (frule sorted_spvec_cons2, simp)
apply (frule sorted_spvec_cons3, simp)
- apply (simp add: sparse_row_matrix_cons neg_def)
+ apply (simp add: sparse_row_matrix_cons)
done
primrec minus_spvec :: "('a::ab_group_add) spvec \<Rightarrow> 'a spvec"
@@ -273,7 +273,6 @@
apply (simp add: algebra_simps sparse_row_matrix_cons)
apply (simplesubst Rep_matrix_zero_imp_mult_zero)
apply (simp)
- apply (intro strip)
apply (rule disjI2)
apply (intro strip)
apply (subst nrows)
@@ -284,7 +283,6 @@
apply (case_tac "k <= j")
apply (rule_tac m1 = k and n1 = i and a1 = a in ssubst[OF sorted_sparse_row_vector_zero])
apply (simp_all)
- apply (rule impI)
apply (rule disjI2)
apply (rule nrows)
apply (rule order_trans[of _ 1])
@@ -297,7 +295,7 @@
apply (simp)
apply (rule disjI2)
apply (intro strip)
- apply (simp add: sparse_row_matrix_cons neg_def)
+ apply (simp add: sparse_row_matrix_cons)
apply (case_tac "i <= j")
apply (erule sorted_sparse_row_matrix_zero)
apply (simp_all)
@@ -315,7 +313,6 @@
apply (auto)
apply (rule_tac m=k and n = j and a = a and arr=arr in sorted_sparse_row_vector_zero)
apply (simp_all)
- apply (simp add: neg_def)
apply (drule nrows_notzero)
apply (drule nrows_helper)
apply (arith)
@@ -647,7 +644,7 @@
lemma disj_move_sparse_vec_mat[simplified disj_matrices_commute]:
"j <= a \<Longrightarrow> sorted_spvec((a,c)#as) \<Longrightarrow> disj_matrices (move_matrix (sparse_row_vector b) (int j) i) (sparse_row_matrix as)"
- apply (auto simp add: neg_def disj_matrices_def)
+ apply (auto simp add: disj_matrices_def)
apply (drule nrows_notzero)
apply (drule less_le_trans[OF _ nrows_spvec])
apply (subgoal_tac "ja = j")
@@ -664,7 +661,7 @@
lemma disj_move_sparse_row_vector_twice:
"j \<noteq> u \<Longrightarrow> disj_matrices (move_matrix (sparse_row_vector a) j i) (move_matrix (sparse_row_vector b) u v)"
- apply (auto simp add: neg_def disj_matrices_def)
+ apply (auto simp add: disj_matrices_def)
apply (rule nrows, rule order_trans[of _ 1], simp, drule nrows_notzero, drule less_le_trans[OF _ nrows_spvec], arith)+
done
@@ -783,7 +780,7 @@
apply (simplesubst sorted_sparse_row_matrix_zero)
apply auto
apply (simplesubst Rep_sparse_row_vector_zero)
- apply (simp_all add: neg_def)
+ apply simp_all
done
lemma sorted_spvec_minus_spmat: "sorted_spvec A \<Longrightarrow> sorted_spvec (minus_spmat A)"