src/HOL/Matrix/SparseMatrix.thy
changeset 25303 0699e20feabd
parent 24124 4399175e3014
child 26300 03def556e26e
     1.1 --- a/src/HOL/Matrix/SparseMatrix.thy	Mon Nov 05 23:17:03 2007 +0100
     1.2 +++ b/src/HOL/Matrix/SparseMatrix.thy	Tue Nov 06 08:47:25 2007 +0100
     1.3 @@ -387,8 +387,8 @@
     1.4    done
     1.5  
     1.6  consts
     1.7 -  add_spvec :: "('a::lordered_ab_group) spvec * 'a spvec \<Rightarrow> 'a spvec"
     1.8 -  add_spmat :: "('a::lordered_ab_group) spmat * 'a spmat \<Rightarrow> 'a spmat"
     1.9 +  add_spvec :: "('a::lordered_ab_group_add) spvec * 'a spvec \<Rightarrow> 'a spvec"
    1.10 +  add_spmat :: "('a::lordered_ab_group_add) spmat * 'a spmat \<Rightarrow> 'a spmat"
    1.11  
    1.12  recdef add_spvec "measure (% (a, b). length a + (length b))"
    1.13    "add_spvec (arr, []) = arr"
    1.14 @@ -569,8 +569,8 @@
    1.15    done
    1.16  
    1.17  consts
    1.18 -  le_spvec :: "('a::lordered_ab_group) spvec * 'a spvec \<Rightarrow> bool" 
    1.19 -  le_spmat :: "('a::lordered_ab_group) spmat * 'a spmat \<Rightarrow> bool" 
    1.20 +  le_spvec :: "('a::lordered_ab_group_add) spvec * 'a spvec \<Rightarrow> bool" 
    1.21 +  le_spmat :: "('a::lordered_ab_group_add) spmat * 'a spmat \<Rightarrow> bool" 
    1.22  
    1.23  recdef le_spvec "measure (% (a,b). (length a) + (length b))" 
    1.24    "le_spvec ([], []) = True"
    1.25 @@ -610,7 +610,7 @@
    1.26  
    1.27  
    1.28  lemma disj_matrices_add: "disj_matrices A B \<Longrightarrow> disj_matrices C D \<Longrightarrow> disj_matrices A D \<Longrightarrow> disj_matrices B C \<Longrightarrow> 
    1.29 -  (A + B <= C + D) = (A <= C & B <= (D::('a::lordered_ab_group) matrix))"
    1.30 +  (A + B <= C + D) = (A <= C & B <= (D::('a::lordered_ab_group_add) matrix))"
    1.31    apply (auto)
    1.32    apply (simp (no_asm_use) only: le_matrix_def disj_matrices_def)
    1.33    apply (intro strip)
    1.34 @@ -640,19 +640,19 @@
    1.35  by (auto simp add: disj_matrices_def)
    1.36  
    1.37  lemma disj_matrices_add_le_zero: "disj_matrices A B \<Longrightarrow>
    1.38 -  (A + B <= 0) = (A <= 0 & (B::('a::lordered_ab_group) matrix) <= 0)"
    1.39 +  (A + B <= 0) = (A <= 0 & (B::('a::lordered_ab_group_add) matrix) <= 0)"
    1.40  by (rule disj_matrices_add[of A B 0 0, simplified])
    1.41   
    1.42  lemma disj_matrices_add_zero_le: "disj_matrices A B \<Longrightarrow>
    1.43 -  (0 <= A + B) = (0 <= A & 0 <= (B::('a::lordered_ab_group) matrix))"
    1.44 +  (0 <= A + B) = (0 <= A & 0 <= (B::('a::lordered_ab_group_add) matrix))"
    1.45  by (rule disj_matrices_add[of 0 0 A B, simplified])
    1.46  
    1.47  lemma disj_matrices_add_x_le: "disj_matrices A B \<Longrightarrow> disj_matrices B C \<Longrightarrow> 
    1.48 -  (A <= B + C) = (A <= C & 0 <= (B::('a::lordered_ab_group) matrix))"
    1.49 +  (A <= B + C) = (A <= C & 0 <= (B::('a::lordered_ab_group_add) matrix))"
    1.50  by (auto simp add: disj_matrices_add[of 0 A B C, simplified])
    1.51  
    1.52  lemma disj_matrices_add_le_x: "disj_matrices A B \<Longrightarrow> disj_matrices B C \<Longrightarrow> 
    1.53 -  (B + A <= C) = (A <= C &  (B::('a::lordered_ab_group) matrix) <= 0)"
    1.54 +  (B + A <= C) = (A <= C &  (B::('a::lordered_ab_group_add) matrix) <= 0)"
    1.55  by (auto simp add: disj_matrices_add[of B A 0 C,simplified] disj_matrices_commute)
    1.56  
    1.57  lemma disj_sparse_row_singleton: "i <= j \<Longrightarrow> sorted_spvec((j,y)#v) \<Longrightarrow> disj_matrices (sparse_row_vector v) (singleton_matrix 0 i x)"
    1.58 @@ -668,7 +668,7 @@
    1.59    apply (simp_all)
    1.60    done 
    1.61  
    1.62 -lemma disj_matrices_x_add: "disj_matrices A B \<Longrightarrow> disj_matrices A C \<Longrightarrow> disj_matrices (A::('a::lordered_ab_group) matrix) (B+C)"
    1.63 +lemma disj_matrices_x_add: "disj_matrices A B \<Longrightarrow> disj_matrices A C \<Longrightarrow> disj_matrices (A::('a::lordered_ab_group_add) matrix) (B+C)"
    1.64    apply (simp add: disj_matrices_def)
    1.65    apply (auto)
    1.66    apply (drule_tac j=j and i=i in spec2)+
    1.67 @@ -677,7 +677,7 @@
    1.68    apply (simp_all)
    1.69    done
    1.70  
    1.71 -lemma disj_matrices_add_x: "disj_matrices A B \<Longrightarrow> disj_matrices A C \<Longrightarrow> disj_matrices (B+C) (A::('a::lordered_ab_group) matrix)" 
    1.72 +lemma disj_matrices_add_x: "disj_matrices A B \<Longrightarrow> disj_matrices A C \<Longrightarrow> disj_matrices (B+C) (A::('a::lordered_ab_group_add) matrix)" 
    1.73    by (simp add: disj_matrices_x_add disj_matrices_commute)
    1.74  
    1.75  lemma disj_singleton_matrices[simp]: "disj_matrices (singleton_matrix j i x) (singleton_matrix u v y) = (j \<noteq> u | i \<noteq> v | x = 0 | y = 0)" 
    1.76 @@ -897,10 +897,10 @@
    1.77  lemma if_case_eq: "(if b then x else y) = (case b of True => x | False => y)" by simp
    1.78  
    1.79  consts
    1.80 -  pprt_spvec :: "('a::{lordered_ab_group}) spvec \<Rightarrow> 'a spvec"
    1.81 -  nprt_spvec :: "('a::{lordered_ab_group}) spvec \<Rightarrow> 'a spvec"
    1.82 -  pprt_spmat :: "('a::{lordered_ab_group}) spmat \<Rightarrow> 'a spmat"
    1.83 -  nprt_spmat :: "('a::{lordered_ab_group}) spmat \<Rightarrow> 'a spmat"
    1.84 +  pprt_spvec :: "('a::{lordered_ab_group_add}) spvec \<Rightarrow> 'a spvec"
    1.85 +  nprt_spvec :: "('a::{lordered_ab_group_add}) spvec \<Rightarrow> 'a spvec"
    1.86 +  pprt_spmat :: "('a::{lordered_ab_group_add}) spmat \<Rightarrow> 'a spmat"
    1.87 +  nprt_spmat :: "('a::{lordered_ab_group_add}) spmat \<Rightarrow> 'a spmat"
    1.88  
    1.89  primrec
    1.90    "pprt_spvec [] = []"