# HG changeset patch
# User nipkow
# Date 1246088621 -7200
# Node ID ffaf6dd5304504dc239cdbe711ea5631a90e10b1
# Parent  52ec1ca1456bd6230688a3c69f98a34b6fa3cfe2
replaced recdefs by funs

diff -r 52ec1ca1456b -r ffaf6dd53045 src/HOL/Matrix/SparseMatrix.thy
--- a/src/HOL/Matrix/SparseMatrix.thy	Fri Jun 26 20:54:15 2009 +0200
+++ b/src/HOL/Matrix/SparseMatrix.thy	Sat Jun 27 09:43:41 2009 +0200
@@ -160,19 +160,19 @@
 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::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"
-  "addmult_spvec (y, a#arr, b#brr) = (
-    if (fst a) < (fst b) then (a#(addmult_spvec (y, arr, b#brr))) 
-    else (if (fst b < fst a) then ((fst b, y * (snd b))#(addmult_spvec (y, a#arr, brr)))
-    else ((fst a, (snd a)+ y*(snd b))#(addmult_spvec (y, arr,brr)))))"
+fun addmult_spvec :: "('a::ring) \<Rightarrow> 'a spvec \<Rightarrow> 'a spvec \<Rightarrow> 'a spvec" where
+  "addmult_spvec y arr [] = arr" |
+  "addmult_spvec y [] brr = smult_spvec y brr" |
+  "addmult_spvec y ((i,a)#arr) ((j,b)#brr) = (
+    if i < j then ((i,a)#(addmult_spvec y arr ((j,b)#brr))) 
+    else (if (j < i) then ((j, y * b)#(addmult_spvec y ((i,a)#arr) brr))
+    else ((i, a + y*b)#(addmult_spvec y arr brr))))"
+(* Steven used termination "measure (% (y, a, b). length a + (length b))" *)
 
-lemma addmult_spvec_empty1[simp]: "addmult_spvec (y, [], a) = smult_spvec y a"
+lemma addmult_spvec_empty1[simp]: "addmult_spvec y [] a = smult_spvec y a"
   by (induct a) auto
 
-lemma addmult_spvec_empty2[simp]: "addmult_spvec (y, a, []) = a"
+lemma addmult_spvec_empty2[simp]: "addmult_spvec y a [] = a"
   by (induct a) auto
 
 lemma sparse_row_vector_map: "(! x y. f (x+y) = (f x) + (f y)) \<Longrightarrow> (f::'a\<Rightarrow>('a::lordered_ring)) 0 = 0 \<Longrightarrow> 
@@ -186,7 +186,7 @@
   apply (simp_all add: smult_spvec_cons scalar_mult_add)
   done
 
-lemma sparse_row_vector_addmult_spvec: "sparse_row_vector (addmult_spvec (y::'a::lordered_ring, a, b)) = 
+lemma sparse_row_vector_addmult_spvec: "sparse_row_vector (addmult_spvec (y::'a::lordered_ring) a b) = 
   (sparse_row_vector a) + (scalar_mult y (sparse_row_vector b))"
   apply (rule addmult_spvec.induct[of _ y])
   apply (simp add: scalar_mult_add smult_spvec_cons sparse_row_vector_smult singleton_matrix_add)+
@@ -198,37 +198,31 @@
   apply (auto simp add: sorted_spvec.simps split:list.split_asm)
   done
 
-lemma sorted_spvec_addmult_spvec_helper: "\<lbrakk>sorted_spvec (addmult_spvec (y, (a, b) # arr, brr)); aa < a; sorted_spvec ((a, b) # arr); 
-  sorted_spvec ((aa, ba) # brr)\<rbrakk> \<Longrightarrow> sorted_spvec ((aa, y * ba) # addmult_spvec (y, (a, b) # arr, brr))"  
+lemma sorted_spvec_addmult_spvec_helper: "\<lbrakk>sorted_spvec (addmult_spvec y ((a, b) # arr) brr); aa < a; sorted_spvec ((a, b) # arr); 
+  sorted_spvec ((aa, ba) # brr)\<rbrakk> \<Longrightarrow> sorted_spvec ((aa, y * ba) # addmult_spvec y ((a, b) # arr) brr)"  
   apply (induct brr)
   apply (auto simp add: sorted_spvec.simps)
-  apply (simp split: list.split)
-  apply (auto)
-  apply (simp split: list.split)
-  apply (auto)
   done
 
 lemma sorted_spvec_addmult_spvec_helper2: 
- "\<lbrakk>sorted_spvec (addmult_spvec (y, arr, (aa, ba) # brr)); a < aa; sorted_spvec ((a, b) # arr); sorted_spvec ((aa, ba) # brr)\<rbrakk>
-       \<Longrightarrow> sorted_spvec ((a, b) # addmult_spvec (y, arr, (aa, ba) # brr))"
+ "\<lbrakk>sorted_spvec (addmult_spvec y arr ((aa, ba) # brr)); a < aa; sorted_spvec ((a, b) # arr); sorted_spvec ((aa, ba) # brr)\<rbrakk>
+       \<Longrightarrow> sorted_spvec ((a, b) # addmult_spvec y arr ((aa, ba) # brr))"
   apply (induct arr)
   apply (auto simp add: smult_spvec_def sorted_spvec.simps)
-  apply (simp split: list.split)
-  apply (auto)
   done
 
 lemma sorted_spvec_addmult_spvec_helper3[rule_format]:
-  "sorted_spvec (addmult_spvec (y, arr, brr)) \<longrightarrow> sorted_spvec ((aa, b) # arr) \<longrightarrow> sorted_spvec ((aa, ba) # brr)
-     \<longrightarrow> sorted_spvec ((aa, b + y * ba) # (addmult_spvec (y, arr, brr)))"
-  apply (rule addmult_spvec.induct[of _ y arr brr])
-  apply (simp_all add: sorted_spvec.simps smult_spvec_def)
+  "sorted_spvec (addmult_spvec y arr brr) \<longrightarrow> sorted_spvec ((aa, b) # arr) \<longrightarrow> sorted_spvec ((aa, ba) # brr)
+     \<longrightarrow> sorted_spvec ((aa, b + y * ba) # (addmult_spvec y arr brr))"
+  apply (induct y arr brr rule: addmult_spvec.induct)
+  apply (simp_all add: sorted_spvec.simps smult_spvec_def split:list.split)
   done
 
-lemma sorted_addmult_spvec[rule_format]: "sorted_spvec a \<longrightarrow> sorted_spvec b \<longrightarrow> sorted_spvec (addmult_spvec (y, a, b))"
+lemma sorted_addmult_spvec[rule_format]: "sorted_spvec a \<longrightarrow> sorted_spvec b \<longrightarrow> sorted_spvec (addmult_spvec y a b)"
   apply (rule addmult_spvec.induct[of _ y a b])
   apply (simp_all add: sorted_smult_spvec)
   apply (rule conjI, intro strip)
-  apply (case_tac "~(a < aa)")
+  apply (case_tac "~(i < j)")
   apply (simp_all)
   apply (frule_tac as=brr in sorted_spvec_cons1)
   apply (simp add: sorted_spvec_addmult_spvec_helper)
@@ -242,18 +236,17 @@
   apply (simp_all add: sorted_spvec_addmult_spvec_helper3)
   done
 
-consts 
-  mult_spvec_spmat :: "('a::lordered_ring) spvec * 'a spvec * 'a spmat  \<Rightarrow> 'a spvec"
-recdef mult_spvec_spmat "measure (% (c, arr, brr). (length arr) + (length brr))"
-  "mult_spvec_spmat (c, [], brr) = c"
-  "mult_spvec_spmat (c, arr, []) = c"
-  "mult_spvec_spmat (c, a#arr, b#brr) = (
-     if ((fst a) < (fst b)) then (mult_spvec_spmat (c, arr, b#brr))
-     else (if ((fst b) < (fst a)) then (mult_spvec_spmat (c, a#arr, brr)) 
-     else (mult_spvec_spmat (addmult_spvec (snd a, c, snd b), arr, brr))))"
+fun mult_spvec_spmat :: "('a::lordered_ring) spvec \<Rightarrow> 'a spvec \<Rightarrow> 'a spmat  \<Rightarrow> 'a spvec" where
+(* recdef mult_spvec_spmat "measure (% (c, arr, brr). (length arr) + (length brr))" *)
+  "mult_spvec_spmat c [] brr = c" |
+  "mult_spvec_spmat c arr [] = c" |
+  "mult_spvec_spmat c ((i,a)#arr) ((j,b)#brr) = (
+     if (i < j) then mult_spvec_spmat c arr ((j,b)#brr)
+     else if (j < i) then mult_spvec_spmat c ((i,a)#arr) brr 
+     else mult_spvec_spmat (addmult_spvec a c b) arr brr)"
 
 lemma sparse_row_mult_spvec_spmat[rule_format]: "sorted_spvec (a::('a::lordered_ring) spvec) \<longrightarrow> sorted_spvec B \<longrightarrow> 
-  sparse_row_vector (mult_spvec_spmat (c, a, B)) = (sparse_row_vector c) + (sparse_row_vector a) * (sparse_row_matrix B)"
+  sparse_row_vector (mult_spvec_spmat c a B) = (sparse_row_vector c) + (sparse_row_vector a) * (sparse_row_matrix B)"
 proof -
   have comp_1: "!! a b. a < b \<Longrightarrow> Suc 0 <= nat ((int b)-(int a))" by arith
   have not_iff: "!! a b. a = b \<Longrightarrow> (~ a) = (~ b)" by simp
@@ -285,8 +278,8 @@
     apply (simp add: comp_1)+
     apply (subst Rep_matrix_zero_imp_mult_zero)
     apply (intro strip)
-    apply (case_tac "k <= aa")
-    apply (rule_tac m1 = k and n1 = a and a1 = b in ssubst[OF sorted_sparse_row_vector_zero])
+    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)
@@ -302,11 +295,11 @@
     apply (rule disjI2)
     apply (intro strip)
     apply (simp add: sparse_row_matrix_cons neg_def)
-    apply (case_tac "a <= aa")  
+    apply (case_tac "i <= j")  
     apply (erule sorted_sparse_row_matrix_zero)  
     apply (simp_all)
     apply (intro strip)
-    apply (case_tac "a=aa")
+    apply (case_tac "i=j")
     apply (simp_all)
     apply (frule_tac as=arr in sorted_spvec_cons1)
     apply (frule_tac as=brr in sorted_spvec_cons1)
@@ -317,7 +310,7 @@
     apply (simp_all)
     apply (rule_tac A1 = "sparse_row_vector arr" in ssubst[OF Rep_matrix_zero_imp_mult_zero])
     apply (auto)
-    apply (rule_tac m=k and n = aa and a = b and arr=arr in sorted_sparse_row_vector_zero)
+    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)
@@ -328,7 +321,7 @@
     apply (rule ext)+
     apply (simp)
     apply (subst Rep_matrix_mult)
-    apply (rule_tac j1=aa in ssubst[OF foldseq_almostzero])
+    apply (rule_tac j1=j in ssubst[OF foldseq_almostzero])
     apply (simp_all)
     apply (intro strip, rule conjI)
     apply (intro strip)
@@ -345,7 +338,7 @@
 qed
 
 lemma sorted_mult_spvec_spmat[rule_format]: 
-  "sorted_spvec (c::('a::lordered_ring) spvec) \<longrightarrow> sorted_spmat B \<longrightarrow> sorted_spvec (mult_spvec_spmat (c, a, B))"
+  "sorted_spvec (c::('a::lordered_ring) spvec) \<longrightarrow> sorted_spmat B \<longrightarrow> sorted_spvec (mult_spvec_spmat c a B)"
   apply (rule mult_spvec_spmat.induct[of _ c a B])
   apply (simp_all add: sorted_addmult_spvec)
   done
@@ -355,7 +348,7 @@
 
 primrec 
   "mult_spmat [] A = []"
-  "mult_spmat (a#as) A = (fst a, mult_spvec_spmat ([], snd a, A))#(mult_spmat as A)"
+  "mult_spmat (a#as) A = (fst a, mult_spvec_spmat [] (snd a) A)#(mult_spmat as A)"
 
 lemma sparse_row_mult_spmat[rule_format]: 
   "sorted_spmat A \<longrightarrow> sorted_spvec B \<longrightarrow> sparse_row_matrix (mult_spmat A B) = (sparse_row_matrix A) * (sparse_row_matrix B)"
@@ -378,41 +371,40 @@
   apply (auto simp add: sorted_mult_spvec_spmat) 
   done
 
-consts
-  add_spvec :: "('a::lordered_ab_group_add) spvec * 'a spvec \<Rightarrow> 'a spvec"
-  add_spmat :: "('a::lordered_ab_group_add) spmat * 'a spmat \<Rightarrow> 'a spmat"
 
-recdef add_spvec "measure (% (a, b). length a + (length b))"
-  "add_spvec (arr, []) = arr"
-  "add_spvec ([], brr) = brr"
-  "add_spvec (a#arr, b#brr) = (
-  if (fst a) < (fst b) then (a#(add_spvec (arr, b#brr))) 
-     else (if (fst b < fst a) then (b#(add_spvec (a#arr, brr)))
-     else ((fst a, (snd a)+(snd b))#(add_spvec (arr,brr)))))"
+fun add_spvec :: "('a::lordered_ab_group_add) spvec \<Rightarrow> 'a spvec \<Rightarrow> 'a spvec" where
+(* "measure (% (a, b). length a + (length b))" *)
+  "add_spvec arr [] = arr" |
+  "add_spvec [] brr = brr" |
+  "add_spvec ((i,a)#arr) ((j,b)#brr) = (
+  if i < j then (i,a)#(add_spvec arr ((j,b)#brr)) 
+     else if (j < i) then (j,b) # add_spvec ((i,a)#arr) brr
+     else (i, a+b) # add_spvec arr brr)"
 
-lemma add_spvec_empty1[simp]: "add_spvec ([], a) = a"
-  by (induct a, auto)
+lemma add_spvec_empty1[simp]: "add_spvec [] a = a"
+by (cases a, auto)
 
-lemma add_spvec_empty2[simp]: "add_spvec (a, []) = a"
-  by (induct a, auto)
-
-lemma sparse_row_vector_add: "sparse_row_vector (add_spvec (a,b)) = (sparse_row_vector a) + (sparse_row_vector b)"
+lemma sparse_row_vector_add: "sparse_row_vector (add_spvec a b) = (sparse_row_vector a) + (sparse_row_vector b)"
   apply (rule add_spvec.induct[of _ a b])
   apply (simp_all add: singleton_matrix_add)
   done
 
-recdef add_spmat "measure (% (A,B). (length A)+(length B))"
-  "add_spmat ([], bs) = bs"
-  "add_spmat (as, []) = as"
-  "add_spmat (a#as, b#bs) = (
-  if fst a < fst b then 
-    (a#(add_spmat (as, b#bs)))
-  else (if fst b < fst a then
-    (b#(add_spmat (a#as, bs)))
+fun add_spmat :: "('a::lordered_ab_group_add) spmat \<Rightarrow> 'a spmat \<Rightarrow> 'a spmat" where
+(* "measure (% (A,B). (length A)+(length B))" *)
+  "add_spmat [] bs = bs" |
+  "add_spmat as [] = as" |
+  "add_spmat ((i,a)#as) ((j,b)#bs) = (
+  if i < j then 
+    (i,a) # add_spmat as ((j,b)#bs)
+  else if j < i then
+    (j,b) # add_spmat ((i,a)#as) bs
   else
-    ((fst a, add_spvec (snd a, snd b))#(add_spmat (as, bs)))))"
+    (i, add_spvec a b) # add_spmat as bs)"
 
-lemma sparse_row_add_spmat: "sparse_row_matrix (add_spmat (A, B)) = (sparse_row_matrix A) + (sparse_row_matrix B)"
+lemma add_spmat_Nil2[simp]: "add_spmat as [] = as"
+by(cases as) auto
+
+lemma sparse_row_add_spmat: "sparse_row_matrix (add_spmat A B) = (sparse_row_matrix A) + (sparse_row_matrix B)"
   apply (rule add_spmat.induct)
   apply (auto simp add: sparse_row_matrix_cons sparse_row_vector_add move_matrix_add)
   done
@@ -420,41 +412,41 @@
 lemmas [code] = sparse_row_add_spmat [symmetric]
 lemmas [code] = sparse_row_vector_add [symmetric]
 
-lemma sorted_add_spvec_helper1[rule_format]: "add_spvec ((a,b)#arr, brr) = (ab, bb) # list \<longrightarrow> (ab = a | (brr \<noteq> [] & ab = fst (hd brr)))"
+lemma sorted_add_spvec_helper1[rule_format]: "add_spvec ((a,b)#arr) brr = (ab, bb) # list \<longrightarrow> (ab = a | (brr \<noteq> [] & ab = fst (hd brr)))"
   proof - 
-    have "(! x ab a. x = (a,b)#arr \<longrightarrow> add_spvec (x, brr) = (ab, bb) # list \<longrightarrow> (ab = a | (ab = fst (hd brr))))"
-      by (rule add_spvec.induct[of _ _ brr], auto)
+    have "(! x ab a. x = (a,b)#arr \<longrightarrow> add_spvec x brr = (ab, bb) # list \<longrightarrow> (ab = a | (ab = fst (hd brr))))"
+      by (rule add_spvec.induct[of _ _ brr]) (auto split:if_splits)
     then show ?thesis
       by (case_tac brr, auto)
   qed
 
-lemma sorted_add_spmat_helper1[rule_format]: "add_spmat ((a,b)#arr, brr) = (ab, bb) # list \<longrightarrow> (ab = a | (brr \<noteq> [] & ab = fst (hd brr)))"
+lemma sorted_add_spmat_helper1[rule_format]: "add_spmat ((a,b)#arr) brr = (ab, bb) # list \<longrightarrow> (ab = a | (brr \<noteq> [] & ab = fst (hd brr)))"
   proof - 
-    have "(! x ab a. x = (a,b)#arr \<longrightarrow> add_spmat (x, brr) = (ab, bb) # list \<longrightarrow> (ab = a | (ab = fst (hd brr))))"
-      by (rule add_spmat.induct[of _ _ brr], auto)
+    have "(! x ab a. x = (a,b)#arr \<longrightarrow> add_spmat x brr = (ab, bb) # list \<longrightarrow> (ab = a | (ab = fst (hd brr))))"
+      by (rule add_spmat.induct[of _ _ brr], auto split:if_splits)
     then show ?thesis
       by (case_tac brr, auto)
   qed
 
-lemma sorted_add_spvec_helper[rule_format]: "add_spvec (arr, brr) = (ab, bb) # list \<longrightarrow> ((arr \<noteq> [] & ab = fst (hd arr)) | (brr \<noteq> [] & ab = fst (hd brr)))"
+lemma sorted_add_spvec_helper[rule_format]: "add_spvec arr brr = (ab, bb) # list \<longrightarrow> ((arr \<noteq> [] & ab = fst (hd arr)) | (brr \<noteq> [] & ab = fst (hd brr)))"
   apply (rule add_spvec.induct[of _ arr brr])
   apply (auto)
   done
 
-lemma sorted_add_spmat_helper[rule_format]: "add_spmat (arr, brr) = (ab, bb) # list \<longrightarrow> ((arr \<noteq> [] & ab = fst (hd arr)) | (brr \<noteq> [] & ab = fst (hd brr)))"
+lemma sorted_add_spmat_helper[rule_format]: "add_spmat arr brr = (ab, bb) # list \<longrightarrow> ((arr \<noteq> [] & ab = fst (hd arr)) | (brr \<noteq> [] & ab = fst (hd brr)))"
   apply (rule add_spmat.induct[of _ arr brr])
   apply (auto)
   done
 
-lemma add_spvec_commute: "add_spvec (a, b) = add_spvec (b, a)"
+lemma add_spvec_commute: "add_spvec a b = add_spvec b a"
   by (rule add_spvec.induct[of _ a b], auto)
 
-lemma add_spmat_commute: "add_spmat (a, b) = add_spmat (b, a)"
+lemma add_spmat_commute: "add_spmat a b = add_spmat b a"
   apply (rule add_spmat.induct[of _ a b])
   apply (simp_all add: add_spvec_commute)
   done
   
-lemma sorted_add_spvec_helper2: "add_spvec ((a,b)#arr, brr) = (ab, bb) # list \<Longrightarrow> aa < a \<Longrightarrow> sorted_spvec ((aa, ba) # brr) \<Longrightarrow> aa < ab"
+lemma sorted_add_spvec_helper2: "add_spvec ((a,b)#arr) brr = (ab, bb) # list \<Longrightarrow> aa < a \<Longrightarrow> sorted_spvec ((aa, ba) # brr) \<Longrightarrow> aa < ab"
   apply (drule sorted_add_spvec_helper1)
   apply (auto)
   apply (case_tac brr)
@@ -463,7 +455,7 @@
   apply (simp)
   done
 
-lemma sorted_add_spmat_helper2: "add_spmat ((a,b)#arr, brr) = (ab, bb) # list \<Longrightarrow> aa < a \<Longrightarrow> sorted_spvec ((aa, ba) # brr) \<Longrightarrow> aa < ab"
+lemma sorted_add_spmat_helper2: "add_spmat ((a,b)#arr) brr = (ab, bb) # list \<Longrightarrow> aa < a \<Longrightarrow> sorted_spvec ((aa, ba) # brr) \<Longrightarrow> aa < ab"
   apply (drule sorted_add_spmat_helper1)
   apply (auto)
   apply (case_tac brr)
@@ -472,50 +464,37 @@
   apply (simp)
   done
 
-lemma sorted_spvec_add_spvec[rule_format]: "sorted_spvec a \<longrightarrow> sorted_spvec b \<longrightarrow> sorted_spvec (add_spvec (a, b))"
+lemma sorted_spvec_add_spvec[rule_format]: "sorted_spvec a \<longrightarrow> sorted_spvec b \<longrightarrow> sorted_spvec (add_spvec a b)"
   apply (rule add_spvec.induct[of _ a b])
   apply (simp_all)
   apply (rule conjI)
-  apply (intro strip)
-  apply (simp)
+  apply (clarsimp)
   apply (frule_tac as=brr in sorted_spvec_cons1)
   apply (simp)
   apply (subst sorted_spvec_step)
-  apply (simp split: list.split)
-  apply (clarify, simp)
-  apply (simp add: sorted_add_spvec_helper2)
+  apply (clarsimp simp: sorted_add_spvec_helper2 split: list.split)
   apply (clarify)
   apply (rule conjI)
-  apply (case_tac "a=aa")
-  apply (simp)
   apply (clarify)
   apply (frule_tac as=arr in sorted_spvec_cons1, simp)
   apply (subst sorted_spvec_step)
-  apply (simp split: list.split)
-  apply (clarify, simp)
-  apply (simp add: sorted_add_spvec_helper2 add_spvec_commute)
-  apply (case_tac "a=aa")
-  apply (simp_all)
+  apply (clarsimp simp: sorted_add_spvec_helper2 add_spvec_commute split: list.split)
   apply (clarify)
   apply (frule_tac as=arr in sorted_spvec_cons1)
   apply (frule_tac as=brr in sorted_spvec_cons1)
   apply (simp)
   apply (subst sorted_spvec_step)
   apply (simp split: list.split)
-  apply (clarify, simp)
+  apply (clarsimp)
   apply (drule_tac sorted_add_spvec_helper)
-  apply (auto)
-  apply (case_tac arr)
-  apply (simp_all)
+  apply (auto simp: neq_Nil_conv)
   apply (drule sorted_spvec_cons3)
   apply (simp)
-  apply (case_tac brr)
-  apply (simp_all)
   apply (drule sorted_spvec_cons3)
   apply (simp)
   done
 
-lemma sorted_spvec_add_spmat[rule_format]: "sorted_spvec A \<longrightarrow> sorted_spvec B \<longrightarrow> sorted_spvec (add_spmat (A, B))"
+lemma sorted_spvec_add_spmat[rule_format]: "sorted_spvec A \<longrightarrow> sorted_spvec B \<longrightarrow> sorted_spvec (add_spmat A B)"
   apply (rule add_spmat.induct[of _ A B])
   apply (simp_all)
   apply (rule conjI)
@@ -529,17 +508,11 @@
   apply (simp add: sorted_add_spmat_helper2)
   apply (clarify)
   apply (rule conjI)
-  apply (case_tac "a=aa")
-  apply (simp)
   apply (clarify)
   apply (frule_tac as=as in sorted_spvec_cons1, simp)
   apply (subst sorted_spvec_step)
-  apply (simp split: list.split)
-  apply (clarify, simp)
-  apply (simp add: sorted_add_spmat_helper2 add_spmat_commute)
-  apply (case_tac "a=aa")
-  apply (simp_all)
-  apply (clarify)
+  apply (clarsimp simp: sorted_add_spmat_helper2 add_spmat_commute split: list.split)
+  apply (clarsimp)
   apply (frule_tac as=as in sorted_spvec_cons1)
   apply (frule_tac as=bs in sorted_spvec_cons1)
   apply (simp)
@@ -547,49 +520,37 @@
   apply (simp split: list.split)
   apply (clarify, simp)
   apply (drule_tac sorted_add_spmat_helper)
-  apply (auto)
-  apply (case_tac as)
-  apply (simp_all)
+  apply (auto simp:neq_Nil_conv)
   apply (drule sorted_spvec_cons3)
   apply (simp)
-  apply (case_tac bs)
-  apply (simp_all)
   apply (drule sorted_spvec_cons3)
   apply (simp)
   done
 
-lemma sorted_spmat_add_spmat[rule_format]: "sorted_spmat A \<longrightarrow> sorted_spmat B \<longrightarrow> sorted_spmat (add_spmat (A, B))"
+lemma sorted_spmat_add_spmat[rule_format]: "sorted_spmat A \<longrightarrow> sorted_spmat B \<longrightarrow> sorted_spmat (add_spmat A B)"
   apply (rule add_spmat.induct[of _ A B])
   apply (simp_all add: sorted_spvec_add_spvec)
   done
 
-consts
-  le_spvec :: "('a::lordered_ab_group_add) spvec * 'a spvec \<Rightarrow> bool" 
-  le_spmat :: "('a::lordered_ab_group_add) spmat * 'a spmat \<Rightarrow> bool" 
+fun le_spvec :: "('a::lordered_ab_group_add) spvec \<Rightarrow> 'a spvec \<Rightarrow> bool" where
+(* "measure (% (a,b). (length a) + (length b))" *)
+  "le_spvec [] [] = True" |
+  "le_spvec ((_,a)#as) [] = (a <= 0 & le_spvec as [])" |
+  "le_spvec [] ((_,b)#bs) = (0 <= b & le_spvec [] bs)" |
+  "le_spvec ((i,a)#as) ((j,b)#bs) = (
+  if (i < j) then a <= 0 & le_spvec as ((j,b)#bs)
+  else if (j < i) then 0 <= b & le_spvec ((i,a)#as) bs
+  else a <= b & le_spvec as bs)"
 
-recdef le_spvec "measure (% (a,b). (length a) + (length b))" 
-  "le_spvec ([], []) = True"
-  "le_spvec (a#as, []) = ((snd a <= 0) & (le_spvec (as, [])))"
-  "le_spvec ([], b#bs) = ((0 <= snd b) & (le_spvec ([], bs)))"
-  "le_spvec (a#as, b#bs) = (
-  if (fst a < fst b) then 
-    ((snd a <= 0) & (le_spvec (as, b#bs)))
-  else (if (fst b < fst a) then
-    ((0 <= snd b) & (le_spvec (a#as, bs)))
-  else 
-    ((snd a <= snd b) & (le_spvec (as, bs)))))"
-
-recdef le_spmat "measure (% (a,b). (length a) + (length b))"
-  "le_spmat ([], []) = True"
-  "le_spmat (a#as, []) = (le_spvec (snd a, []) & (le_spmat (as, [])))"
-  "le_spmat ([], b#bs) = (le_spvec ([], snd b) & (le_spmat ([], bs)))"
-  "le_spmat (a#as, b#bs) = (
-  if fst a < fst b then
-    (le_spvec(snd a,[]) & le_spmat(as, b#bs))
-  else (if (fst b < fst a) then 
-    (le_spvec([], snd b) & le_spmat(a#as, bs))
-  else
-    (le_spvec(snd a, snd b) & le_spmat (as, bs))))"
+fun le_spmat :: "('a::lordered_ab_group_add) spmat \<Rightarrow> 'a spmat \<Rightarrow> bool" where
+(* "measure (% (a,b). (length a) + (length b))" *)
+  "le_spmat [] [] = True" |
+  "le_spmat ((i,a)#as) [] = (le_spvec a [] & le_spmat as [])" |
+  "le_spmat [] ((j,b)#bs) = (le_spvec [] b & le_spmat [] bs)" |
+  "le_spmat ((i,a)#as) ((j,b)#bs) = (
+  if i < j then (le_spvec a [] & le_spmat as ((j,b)#bs))
+  else if j < i then (le_spvec [] b & le_spmat ((i,a)#as) bs)
+  else (le_spvec a b & le_spmat as bs))"
 
 constdefs
   disj_matrices :: "('a::zero) matrix \<Rightarrow> 'a matrix \<Rightarrow> bool"
@@ -701,7 +662,7 @@
   apply (rule nrows, rule order_trans[of _ 1], simp, drule nrows_notzero, drule less_le_trans[OF _ nrows_spvec], arith)+
   done
 
-lemma le_spvec_iff_sparse_row_le[rule_format]: "(sorted_spvec a) \<longrightarrow> (sorted_spvec b) \<longrightarrow> (le_spvec (a,b)) = (sparse_row_vector a <= sparse_row_vector b)"
+lemma le_spvec_iff_sparse_row_le[rule_format]: "(sorted_spvec a) \<longrightarrow> (sorted_spvec b) \<longrightarrow> (le_spvec a b) = (sparse_row_vector a <= sparse_row_vector b)"
   apply (rule le_spvec.induct)
   apply (simp_all add: sorted_spvec_cons1 disj_matrices_add_le_zero disj_matrices_add_zero_le 
     disj_sparse_row_singleton[OF order_refl] disj_matrices_commute)
@@ -718,33 +679,29 @@
   apply (blast)
   apply (intro strip)
   apply (simp add: sorted_spvec_cons1)
-  apply (case_tac "a=aa", simp_all)
+  apply (case_tac "a=b", simp_all)
   apply (subst disj_matrices_add)
   apply (simp_all add: disj_sparse_row_singleton[OF order_refl] disj_matrices_commute)
   done
 
-lemma le_spvec_empty2_sparse_row[rule_format]: "(sorted_spvec b) \<longrightarrow> (le_spvec (b,[]) = (sparse_row_vector b <= 0))"
+lemma le_spvec_empty2_sparse_row[rule_format]: "sorted_spvec b \<longrightarrow> le_spvec b [] = (sparse_row_vector b <= 0)"
   apply (induct b)
   apply (simp_all add: sorted_spvec_cons1)
   apply (intro strip)
   apply (subst disj_matrices_add_le_zero)
-  apply (simp add: disj_matrices_commute disj_sparse_row_singleton sorted_spvec_cons1)
-  apply (rule_tac y = "snd a" in disj_sparse_row_singleton[OF order_refl])
-  apply (simp_all)
+  apply (auto simp add: disj_matrices_commute disj_sparse_row_singleton[OF order_refl] sorted_spvec_cons1)
   done
 
-lemma le_spvec_empty1_sparse_row[rule_format]: "(sorted_spvec b) \<longrightarrow> (le_spvec ([],b) = (0 <= sparse_row_vector b))"
+lemma le_spvec_empty1_sparse_row[rule_format]: "(sorted_spvec b) \<longrightarrow> (le_spvec [] b = (0 <= sparse_row_vector b))"
   apply (induct b)
   apply (simp_all add: sorted_spvec_cons1)
   apply (intro strip)
   apply (subst disj_matrices_add_zero_le)
-  apply (simp add: disj_matrices_commute disj_sparse_row_singleton sorted_spvec_cons1)
-  apply (rule_tac y = "snd a" in disj_sparse_row_singleton[OF order_refl])
-  apply (simp_all)
+  apply (auto simp add: disj_matrices_commute disj_sparse_row_singleton[OF order_refl] sorted_spvec_cons1)
   done
 
 lemma le_spmat_iff_sparse_row_le[rule_format]: "(sorted_spvec A) \<longrightarrow> (sorted_spmat A) \<longrightarrow> (sorted_spvec B) \<longrightarrow> (sorted_spmat B) \<longrightarrow> 
-  le_spmat(A, B) = (sparse_row_matrix A <= sparse_row_matrix B)"
+  le_spmat A B = (sparse_row_matrix A <= sparse_row_matrix B)"
   apply (rule le_spmat.induct)
   apply (simp add: sparse_row_matrix_cons disj_matrices_add_le_zero disj_matrices_add_zero_le disj_move_sparse_vec_mat[OF order_refl] 
     disj_matrices_commute sorted_spvec_cons1 le_spvec_empty2_sparse_row le_spvec_empty1_sparse_row)+ 
@@ -765,7 +722,7 @@
   apply (simp add: disj_move_sparse_vec_mat[OF less_imp_le] disj_matrices_commute)
   apply (simp, blast)
   apply (intro strip)
-  apply (case_tac "a=aa")
+  apply (case_tac "i=j")
   apply (simp_all)
   apply (subst disj_matrices_add)
   apply (simp_all add: disj_matrices_commute disj_move_sparse_vec_mat[OF order_refl])
@@ -851,7 +808,7 @@
 
 constdefs
   diff_spmat :: "('a::lordered_ring) spmat \<Rightarrow> 'a spmat \<Rightarrow> 'a spmat"
-  "diff_spmat A B == add_spmat (A, minus_spmat B)"
+  "diff_spmat A B == add_spmat A (minus_spmat B)"
 
 lemma sorted_spmat_diff_spmat: "sorted_spmat A \<Longrightarrow> sorted_spmat B \<Longrightarrow> sorted_spmat (diff_spmat A B)"
   by (simp add: diff_spmat_def sorted_spmat_minus_spmat sorted_spmat_add_spmat)
@@ -1064,8 +1021,8 @@
 constdefs
   mult_est_spmat :: "('a::lordered_ring) spmat \<Rightarrow> 'a spmat \<Rightarrow> 'a spmat \<Rightarrow> 'a spmat \<Rightarrow> 'a spmat"
   "mult_est_spmat r1 r2 s1 s2 == 
-  add_spmat (mult_spmat (pprt_spmat s2) (pprt_spmat r2), add_spmat (mult_spmat (pprt_spmat s1) (nprt_spmat r2), 
-  add_spmat (mult_spmat (nprt_spmat s2) (pprt_spmat r1), mult_spmat (nprt_spmat s1) (nprt_spmat r1))))"  
+  add_spmat (mult_spmat (pprt_spmat s2) (pprt_spmat r2)) (add_spmat (mult_spmat (pprt_spmat s1) (nprt_spmat r2)) 
+  (add_spmat (mult_spmat (nprt_spmat s2) (pprt_spmat r1)) (mult_spmat (nprt_spmat s1) (nprt_spmat r1))))"  
 
 lemmas sparse_row_matrix_op_simps =
   sorted_sparse_matrix_imp_spmat sorted_sparse_matrix_imp_spvec
diff -r 52ec1ca1456b -r ffaf6dd53045 src/HOL/Matrix/cplex/Cplex.thy
--- a/src/HOL/Matrix/cplex/Cplex.thy	Fri Jun 26 20:54:15 2009 +0200
+++ b/src/HOL/Matrix/cplex/Cplex.thy	Sat Jun 27 09:43:41 2009 +0200
@@ -19,7 +19,7 @@
   "sorted_sparse_matrix r1"
   "sorted_sparse_matrix r2"
   "sorted_spvec b"
-  "le_spmat ([], y)"
+  "le_spmat [] y"
   "sparse_row_matrix A1 \<le> A"
   "A \<le> sparse_row_matrix A2"
   "sparse_row_matrix c1 \<le> c"
@@ -28,10 +28,10 @@
   "x \<le> sparse_row_matrix r2"
   "A * x \<le> sparse_row_matrix (b::('a::lordered_ring) spmat)"
   shows
-  "c * x \<le> sparse_row_matrix (add_spmat (mult_spmat y b,
+  "c * x \<le> sparse_row_matrix (add_spmat (mult_spmat y b)
   (let s1 = diff_spmat c1 (mult_spmat y A2); s2 = diff_spmat c2 (mult_spmat y A1) in 
-  add_spmat (mult_spmat (pprt_spmat s2) (pprt_spmat r2), add_spmat (mult_spmat (pprt_spmat s1) (nprt_spmat r2), 
-  add_spmat (mult_spmat (nprt_spmat s2) (pprt_spmat r1), mult_spmat (nprt_spmat s1) (nprt_spmat r1)))))))"
+  add_spmat (mult_spmat (pprt_spmat s2) (pprt_spmat r2)) (add_spmat (mult_spmat (pprt_spmat s1) (nprt_spmat r2)) 
+  (add_spmat (mult_spmat (nprt_spmat s2) (pprt_spmat r1)) (mult_spmat (nprt_spmat s1) (nprt_spmat r1))))))"
   apply (simp add: Let_def)
   apply (insert assms)
   apply (simp add: sparse_row_matrix_op_simps algebra_simps)  
@@ -49,7 +49,7 @@
   "sorted_sparse_matrix r1"
   "sorted_sparse_matrix r2"
   "sorted_spvec b"
-  "le_spmat ([], y)"
+  "le_spmat [] y"
   "sparse_row_matrix A1 \<le> A"
   "A \<le> sparse_row_matrix A2"
   "sparse_row_matrix c1 \<le> c"
@@ -58,8 +58,8 @@
   "x \<le> sparse_row_matrix r2"
   "A * x \<le> sparse_row_matrix (b::('a::lordered_ring) spmat)"
   shows
-  "c * x \<le> sparse_row_matrix (add_spmat (mult_spmat y b,
-  mult_est_spmat r1 r2 (diff_spmat c1 (mult_spmat y A2)) (diff_spmat c2 (mult_spmat y A1))))"
+  "c * x \<le> sparse_row_matrix (add_spmat (mult_spmat y b)
+  (mult_est_spmat r1 r2 (diff_spmat c1 (mult_spmat y A2)) (diff_spmat c2 (mult_spmat y A1))))"
   by (simp add: assms mult_est_spmat_def spm_mult_le_dual_prts[where A=A, simplified Let_def])
 
 use "matrixlp.ML"