diff -r 818666de6c24 -r 180e28bab764 src/HOL/Matrix/SparseMatrix.thy
--- a/src/HOL/Matrix/SparseMatrix.thy	Fri Jul 18 18:25:56 2008 +0200
+++ b/src/HOL/Matrix/SparseMatrix.thy	Fri Jul 18 18:25:57 2008 +0200
@@ -4,17 +4,17 @@
 *)
 
 theory SparseMatrix
-imports Matrix
+imports "./Matrix"
 begin
 
 types 
   'a spvec = "(nat * 'a) list"
   'a spmat = "('a spvec) spvec"
 
-definition sparse_row_vector :: "('a::lordered_ring) spvec \<Rightarrow> 'a matrix" where
+definition sparse_row_vector :: "('a::ab_group_add) spvec \<Rightarrow> 'a matrix" where
   sparse_row_vector_def: "sparse_row_vector arr = foldl (% m x. m + (singleton_matrix 0 (fst x) (snd x))) 0 arr"
 
-definition sparse_row_matrix :: "('a::lordered_ring) spmat \<Rightarrow> 'a matrix" where
+definition sparse_row_matrix :: "('a::ab_group_add) spmat \<Rightarrow> 'a matrix" where
   sparse_row_matrix_def: "sparse_row_matrix arr = foldl (% m r. m + (move_matrix (sparse_row_vector (snd r)) (int (fst r)) 0)) 0 arr"
 
 code_datatype sparse_row_vector sparse_row_matrix
@@ -30,14 +30,16 @@
 lemma foldl_distrstart[rule_format]: "! a x y. (f (g x y) a = g x (f y a)) \<Longrightarrow> ! x y. (foldl f (g x y) l = g x (foldl f y l))"
   by (induct l, auto)
 
-lemma sparse_row_vector_cons[simp]: "sparse_row_vector (a#arr) = (singleton_matrix 0 (fst a) (snd a)) + (sparse_row_vector arr)"
+lemma sparse_row_vector_cons[simp]:
+  "sparse_row_vector (a # arr) = (singleton_matrix 0 (fst a) (snd a)) + (sparse_row_vector arr)"
   apply (induct arr)
   apply (auto simp add: sparse_row_vector_def)
-  apply (simp add: foldl_distrstart[of "\<lambda>m x. m + singleton_matrix 0 (fst x) (snd x)" "\<lambda>x m. singleton_matrix 0 (fst x) (snd x) + m"])
+  apply (simp add: foldl_distrstart [of "\<lambda>m x. m + singleton_matrix 0 (fst x) (snd x)" "\<lambda>x m. singleton_matrix 0 (fst x) (snd x) + m"])
   done
 
-lemma sparse_row_vector_append[simp]: "sparse_row_vector (a @ b) = (sparse_row_vector a) + (sparse_row_vector b)"
-  by (induct a, auto)
+lemma sparse_row_vector_append[simp]:
+  "sparse_row_vector (a @ b) = (sparse_row_vector a) + (sparse_row_vector b)"
+  by (induct a) auto
 
 lemma nrows_spvec[simp]: "nrows (sparse_row_vector x) <= (Suc 0)"
   apply (induct x)
@@ -56,17 +58,13 @@
   apply (auto simp add: sparse_row_matrix_cons)
   done
 
-consts
-  sorted_spvec :: "'a spvec \<Rightarrow> bool"
-  sorted_spmat :: "'a spmat \<Rightarrow> bool"
+primrec sorted_spvec :: "'a spvec \<Rightarrow> bool" where
+  "sorted_spvec [] = True"
+  | sorted_spvec_step: "sorted_spvec (a#as) = (case as of [] \<Rightarrow> True | b#bs \<Rightarrow> ((fst a < fst b) & (sorted_spvec as)))" 
 
-primrec
+primrec sorted_spmat :: "'a spmat \<Rightarrow> bool" where
   "sorted_spmat [] = True"
-  "sorted_spmat (a#as) = ((sorted_spvec (snd a)) & (sorted_spmat as))"
-
-primrec
-  "sorted_spvec [] = True"
-sorted_spvec_step:  "sorted_spvec (a#as) = (case as of [] \<Rightarrow> True | b#bs \<Rightarrow> ((fst a < fst b) & (sorted_spvec as)))" 
+  | "sorted_spmat (a#as) = ((sorted_spvec (snd a)) & (sorted_spmat as))"
 
 declare sorted_spvec.simps [simp del]
 
@@ -102,14 +100,11 @@
   apply (simp add: sparse_row_matrix_cons neg_def)
   done
 
-consts
-  smult_spvec :: "('a::lordered_ring) \<Rightarrow> 'a spvec \<Rightarrow> 'a spvec" 
-
-primrec minus_spvec ::  "('a::lordered_ring) spvec \<Rightarrow> 'a spvec" where
+primrec minus_spvec :: "('a::ab_group_add) spvec \<Rightarrow> 'a spvec" where
   "minus_spvec [] = []"
   | "minus_spvec (a#as) = (fst a, -(snd a))#(minus_spvec as)"
 
-primrec abs_spvec ::  "('a::lordered_ring) spvec \<Rightarrow> 'a spvec" where
+primrec abs_spvec ::  "('a::lordered_ab_group_add_abs) spvec \<Rightarrow> 'a spvec" where
   "abs_spvec [] = []"
   | "abs_spvec (a#as) = (fst a, abs (snd a))#(abs_spvec as)"
 
@@ -122,10 +117,14 @@
   apply simp
   done
 
+instance matrix :: (lordered_ab_group_add_abs) lordered_ab_group_add_abs
+apply default
+unfolding abs_matrix_def .. (*FIXME move*)
+
 lemma sparse_row_vector_abs:
-  "sorted_spvec v \<Longrightarrow> sparse_row_vector (abs_spvec v) = abs (sparse_row_vector v)"
+  "sorted_spvec (v :: 'a::lordered_ring spvec) \<Longrightarrow> sparse_row_vector (abs_spvec v) = abs (sparse_row_vector v)"
   apply (induct v)
-  apply (simp_all add: sparse_row_vector_cons)
+  apply simp_all
   apply (frule_tac sorted_spvec_cons1, simp)
   apply (simp only: Rep_matrix_inject[symmetric])
   apply (rule ext)+
@@ -152,8 +151,8 @@
   apply (simp add: sorted_spvec.simps split:list.split_asm)
   done
   
-defs
-  smult_spvec_def: "smult_spvec y arr == map (% a. (fst a, y * snd a)) arr"  
+definition
+  "smult_spvec y = map (% a. (fst a, y * snd a))"  
 
 lemma smult_spvec_empty[simp]: "smult_spvec y [] = []"
   by (simp add: smult_spvec_def)
@@ -161,7 +160,7 @@
 lemma smult_spvec_cons: "smult_spvec y (a#arr) = (fst a, y * (snd a)) # (smult_spvec y arr)"
   by (simp add: smult_spvec_def)
 
-consts addmult_spvec :: "('a::lordered_ring) * 'a spvec * 'a spvec \<Rightarrow> 'a spvec"
+consts addmult_spvec :: "('a::ring) * 'a spvec * 'a spvec \<Rightarrow> 'a spvec"
 recdef addmult_spvec "measure (% (y, a, b). length a + (length b))"
   "addmult_spvec (y, arr, []) = arr"
   "addmult_spvec (y, [], brr) = smult_spvec y brr"
@@ -951,7 +950,7 @@
 
 lemma less_imp_le: "a < b \<Longrightarrow> a <= (b::_::order)" by (simp add: less_def)
 
-lemma sparse_row_vector_pprt: "sorted_spvec v \<Longrightarrow> sparse_row_vector (pprt_spvec v) = pprt (sparse_row_vector v)"
+lemma sparse_row_vector_pprt: "sorted_spvec (v :: 'a::lordered_ring spvec) \<Longrightarrow> sparse_row_vector (pprt_spvec v) = pprt (sparse_row_vector v)"
   apply (induct v)
   apply (simp_all)
   apply (frule sorted_spvec_cons1, auto)
@@ -961,7 +960,7 @@
   apply auto
   done
 
-lemma sparse_row_vector_nprt: "sorted_spvec v \<Longrightarrow> sparse_row_vector (nprt_spvec v) = nprt (sparse_row_vector v)"
+lemma sparse_row_vector_nprt: "sorted_spvec (v :: 'a::lordered_ring spvec) \<Longrightarrow> sparse_row_vector (nprt_spvec v) = nprt (sparse_row_vector v)"
   apply (induct v)
   apply (simp_all)
   apply (frule sorted_spvec_cons1, auto)
@@ -988,7 +987,7 @@
   apply (simp)
   done
 
-lemma sparse_row_matrix_pprt: "sorted_spvec m \<Longrightarrow> sorted_spmat m \<Longrightarrow> sparse_row_matrix (pprt_spmat m) = pprt (sparse_row_matrix m)"
+lemma sparse_row_matrix_pprt: "sorted_spvec (m :: 'a::lordered_ring spmat) \<Longrightarrow> sorted_spmat m \<Longrightarrow> sparse_row_matrix (pprt_spmat m) = pprt (sparse_row_matrix m)"
   apply (induct m)
   apply simp
   apply simp
@@ -1004,7 +1003,7 @@
   apply (simp add: pprt_move_matrix)
   done
 
-lemma sparse_row_matrix_nprt: "sorted_spvec m \<Longrightarrow> sorted_spmat m \<Longrightarrow> sparse_row_matrix (nprt_spmat m) = nprt (sparse_row_matrix m)"
+lemma sparse_row_matrix_nprt: "sorted_spvec (m :: 'a::lordered_ring spmat) \<Longrightarrow> sorted_spmat m \<Longrightarrow> sparse_row_matrix (nprt_spmat m) = nprt (sparse_row_matrix m)"
   apply (induct m)
   apply simp
   apply simp