# HG changeset patch
# User huffman
# Date 1330339136 -3600
# Node ID 202a09ba37d87078c97391aced6824dbd9a87fd2
# Parent  b07ae33cc4598cf8a9c00309989372e45061b736
avoid using constant Int.neg

diff -r b07ae33cc459 -r 202a09ba37d8 src/HOL/Matrix/Matrix.thy
--- 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  
diff -r b07ae33cc459 -r 202a09ba37d8 src/HOL/Matrix/SparseMatrix.thy
--- 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)"