1.1 --- a/src/HOL/Matrix/Matrix.thy Mon Feb 27 10:56:36 2012 +0100
1.2 +++ b/src/HOL/Matrix/Matrix.thy Mon Feb 27 11:38:56 2012 +0100
1.3 @@ -849,7 +849,7 @@
1.4 "singleton_matrix j i a == Abs_matrix(% m n. if j = m & i = n then a else 0)"
1.5
1.6 definition move_matrix :: "('a::zero) matrix \<Rightarrow> int \<Rightarrow> int \<Rightarrow> 'a matrix" where
1.7 - "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)))"
1.8 + "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)))"
1.9
1.10 definition take_rows :: "('a::zero) matrix \<Rightarrow> nat \<Rightarrow> 'a matrix" where
1.11 "take_rows A r == Abs_matrix(% j i. if (j < r) then (Rep_matrix A j i) else 0)"
1.12 @@ -930,7 +930,7 @@
1.13
1.14 lemma Rep_move_matrix[simp]:
1.15 "Rep_matrix (move_matrix A y x) j i =
1.16 - (if (neg ((int j)-y)) | (neg ((int i)-x)) then 0 else Rep_matrix A (nat((int j)-y)) (nat((int i)-x)))"
1.17 + (if (((int j)-y) < 0) | (((int i)-x) < 0) then 0 else Rep_matrix A (nat((int j)-y)) (nat((int i)-x)))"
1.18 apply (simp add: move_matrix_def)
1.19 apply (auto)
1.20 by (subst RepAbs_matrix,
1.21 @@ -959,8 +959,8 @@
1.22 apply (case_tac "j + int u < 0")
1.23 apply (simp, arith)
1.24 apply (case_tac "i + int v < 0")
1.25 - apply (simp add: neg_def, arith)
1.26 - apply (simp add: neg_def)
1.27 + apply (simp, arith)
1.28 + apply simp
1.29 apply arith
1.30 done
1.31
1.32 @@ -1016,7 +1016,6 @@
1.33 apply (subst foldseq_almostzero[of _ j])
1.34 apply (simp add: assms)+
1.35 apply (auto)
1.36 - apply (metis add_0 le_antisym le_diff_eq not_neg_nat zero_le_imp_of_nat zle_int)
1.37 done
1.38
1.39 lemma mult_matrix_ext:
1.40 @@ -1440,19 +1439,19 @@
1.41 done
1.42
1.43 lemma move_matrix_le_zero[simp]: "0 <= j \<Longrightarrow> 0 <= i \<Longrightarrow> (move_matrix A j i <= 0) = (A <= (0::('a::{order,zero}) matrix))"
1.44 - apply (auto simp add: le_matrix_def neg_def)
1.45 + apply (auto simp add: le_matrix_def)
1.46 apply (drule_tac j="ja+(nat j)" and i="ia+(nat i)" in spec2)
1.47 apply (auto)
1.48 done
1.49
1.50 lemma move_matrix_zero_le[simp]: "0 <= j \<Longrightarrow> 0 <= i \<Longrightarrow> (0 <= move_matrix A j i) = ((0::('a::{order,zero}) matrix) <= A)"
1.51 - apply (auto simp add: le_matrix_def neg_def)
1.52 + apply (auto simp add: le_matrix_def)
1.53 apply (drule_tac j="ja+(nat j)" and i="ia+(nat i)" in spec2)
1.54 apply (auto)
1.55 done
1.56
1.57 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))"
1.58 - apply (auto simp add: le_matrix_def neg_def)
1.59 + apply (auto simp add: le_matrix_def)
1.60 apply (drule_tac j="ja+(nat j)" and i="ia+(nat i)" in spec2)
1.61 apply (auto)
1.62 done
2.1 --- a/src/HOL/Matrix/SparseMatrix.thy Mon Feb 27 10:56:36 2012 +0100
2.2 +++ b/src/HOL/Matrix/SparseMatrix.thy Mon Feb 27 11:38:56 2012 +0100
2.3 @@ -97,7 +97,7 @@
2.4 apply (auto)
2.5 apply (frule sorted_spvec_cons2, simp)
2.6 apply (frule sorted_spvec_cons3, simp)
2.7 - apply (simp add: sparse_row_matrix_cons neg_def)
2.8 + apply (simp add: sparse_row_matrix_cons)
2.9 done
2.10
2.11 primrec minus_spvec :: "('a::ab_group_add) spvec \<Rightarrow> 'a spvec"
2.12 @@ -273,7 +273,6 @@
2.13 apply (simp add: algebra_simps sparse_row_matrix_cons)
2.14 apply (simplesubst Rep_matrix_zero_imp_mult_zero)
2.15 apply (simp)
2.16 - apply (intro strip)
2.17 apply (rule disjI2)
2.18 apply (intro strip)
2.19 apply (subst nrows)
2.20 @@ -284,7 +283,6 @@
2.21 apply (case_tac "k <= j")
2.22 apply (rule_tac m1 = k and n1 = i and a1 = a in ssubst[OF sorted_sparse_row_vector_zero])
2.23 apply (simp_all)
2.24 - apply (rule impI)
2.25 apply (rule disjI2)
2.26 apply (rule nrows)
2.27 apply (rule order_trans[of _ 1])
2.28 @@ -297,7 +295,7 @@
2.29 apply (simp)
2.30 apply (rule disjI2)
2.31 apply (intro strip)
2.32 - apply (simp add: sparse_row_matrix_cons neg_def)
2.33 + apply (simp add: sparse_row_matrix_cons)
2.34 apply (case_tac "i <= j")
2.35 apply (erule sorted_sparse_row_matrix_zero)
2.36 apply (simp_all)
2.37 @@ -315,7 +313,6 @@
2.38 apply (auto)
2.39 apply (rule_tac m=k and n = j and a = a and arr=arr in sorted_sparse_row_vector_zero)
2.40 apply (simp_all)
2.41 - apply (simp add: neg_def)
2.42 apply (drule nrows_notzero)
2.43 apply (drule nrows_helper)
2.44 apply (arith)
2.45 @@ -647,7 +644,7 @@
2.46
2.47 lemma disj_move_sparse_vec_mat[simplified disj_matrices_commute]:
2.48 "j <= a \<Longrightarrow> sorted_spvec((a,c)#as) \<Longrightarrow> disj_matrices (move_matrix (sparse_row_vector b) (int j) i) (sparse_row_matrix as)"
2.49 - apply (auto simp add: neg_def disj_matrices_def)
2.50 + apply (auto simp add: disj_matrices_def)
2.51 apply (drule nrows_notzero)
2.52 apply (drule less_le_trans[OF _ nrows_spvec])
2.53 apply (subgoal_tac "ja = j")
2.54 @@ -664,7 +661,7 @@
2.55
2.56 lemma disj_move_sparse_row_vector_twice:
2.57 "j \<noteq> u \<Longrightarrow> disj_matrices (move_matrix (sparse_row_vector a) j i) (move_matrix (sparse_row_vector b) u v)"
2.58 - apply (auto simp add: neg_def disj_matrices_def)
2.59 + apply (auto simp add: disj_matrices_def)
2.60 apply (rule nrows, rule order_trans[of _ 1], simp, drule nrows_notzero, drule less_le_trans[OF _ nrows_spvec], arith)+
2.61 done
2.62
2.63 @@ -783,7 +780,7 @@
2.64 apply (simplesubst sorted_sparse_row_matrix_zero)
2.65 apply auto
2.66 apply (simplesubst Rep_sparse_row_vector_zero)
2.67 - apply (simp_all add: neg_def)
2.68 + apply simp_all
2.69 done
2.70
2.71 lemma sorted_spvec_minus_spmat: "sorted_spvec A \<Longrightarrow> sorted_spvec (minus_spmat A)"