src/HOL/Matrix/Matrix.thy
changeset 25303 0699e20feabd
parent 23879 4776af8be741
child 25502 9200b36280c0
     1.1 --- a/src/HOL/Matrix/Matrix.thy	Mon Nov 05 23:17:03 2007 +0100
     1.2 +++ b/src/HOL/Matrix/Matrix.thy	Tue Nov 06 08:47:25 2007 +0100
     1.3 @@ -22,12 +22,12 @@
     1.4  instance matrix :: ("{plus, times, zero}") times
     1.5    times_matrix_def: "A * B \<equiv> mult_matrix (op *) (op +) A B" ..
     1.6  
     1.7 -instance matrix :: (lordered_ab_group) abs
     1.8 +instance matrix :: (lordered_ab_group_add) abs
     1.9    abs_matrix_def: "abs A \<equiv> sup A (- A)" ..
    1.10  
    1.11 -instance matrix :: (lordered_ab_group) lordered_ab_group_meet
    1.12 +instance matrix :: (lordered_ab_group_add) lordered_ab_group_add_meet
    1.13  proof 
    1.14 -  fix A B C :: "('a::lordered_ab_group) matrix"
    1.15 +  fix A B C :: "('a::lordered_ab_group_add) matrix"
    1.16    show "A + B + C = A + (B + C)"    
    1.17      apply (simp add: plus_matrix_def)
    1.18      apply (rule combine_matrix_assoc[simplified associative_def, THEN spec, THEN spec, THEN spec])
    1.19 @@ -89,7 +89,8 @@
    1.20      done
    1.21  qed 
    1.22  
    1.23 -lemma Rep_matrix_add[simp]: "Rep_matrix ((a::('a::lordered_ab_group)matrix)+b) j i  = (Rep_matrix a j i) + (Rep_matrix b j i)"
    1.24 +lemma Rep_matrix_add[simp]:
    1.25 +  "Rep_matrix ((a::('a::lordered_ab_group_add)matrix)+b) j i  = (Rep_matrix a j i) + (Rep_matrix b j i)"
    1.26  by (simp add: plus_matrix_def)
    1.27  
    1.28  lemma Rep_matrix_mult: "Rep_matrix ((a::('a::lordered_ring) matrix) * b) j i = 
    1.29 @@ -98,13 +99,13 @@
    1.30  apply (simp add: Rep_mult_matrix)
    1.31  done
    1.32  
    1.33 -lemma apply_matrix_add: "! x y. f (x+y) = (f x) + (f y) \<Longrightarrow> f 0 = (0::'a) \<Longrightarrow> apply_matrix f ((a::('a::lordered_ab_group) matrix) + b) = (apply_matrix f a) + (apply_matrix f b)"
    1.34 +lemma apply_matrix_add: "! x y. f (x+y) = (f x) + (f y) \<Longrightarrow> f 0 = (0::'a) \<Longrightarrow> apply_matrix f ((a::('a::lordered_ab_group_add) matrix) + b) = (apply_matrix f a) + (apply_matrix f b)"
    1.35  apply (subst Rep_matrix_inject[symmetric])
    1.36  apply (rule ext)+
    1.37  apply (simp)
    1.38  done
    1.39  
    1.40 -lemma singleton_matrix_add: "singleton_matrix j i ((a::_::lordered_ab_group)+b) = (singleton_matrix j i a) + (singleton_matrix j i b)"
    1.41 +lemma singleton_matrix_add: "singleton_matrix j i ((a::_::lordered_ab_group_add)+b) = (singleton_matrix j i a) + (singleton_matrix j i b)"
    1.42  apply (subst Rep_matrix_inject[symmetric])
    1.43  apply (rule ext)+
    1.44  apply (simp)
    1.45 @@ -162,10 +163,10 @@
    1.46  apply (simp_all add: mult_commute)
    1.47  done
    1.48  
    1.49 -lemma transpose_matrix_add: "transpose_matrix ((A::('a::lordered_ab_group) matrix)+B) = transpose_matrix A + transpose_matrix B"
    1.50 +lemma transpose_matrix_add: "transpose_matrix ((A::('a::lordered_ab_group_add) matrix)+B) = transpose_matrix A + transpose_matrix B"
    1.51  by (simp add: plus_matrix_def transpose_combine_matrix)
    1.52  
    1.53 -lemma transpose_matrix_diff: "transpose_matrix ((A::('a::lordered_ab_group) matrix)-B) = transpose_matrix A - transpose_matrix B"
    1.54 +lemma transpose_matrix_diff: "transpose_matrix ((A::('a::lordered_ab_group_add) matrix)-B) = transpose_matrix A - transpose_matrix B"
    1.55  by (simp add: diff_matrix_def transpose_combine_matrix)
    1.56  
    1.57  lemma transpose_matrix_minus: "transpose_matrix (-(A::('a::lordered_ring) matrix)) = - transpose_matrix (A::('a::lordered_ring) matrix)"
    1.58 @@ -252,7 +253,7 @@
    1.59  apply (simp add: max2)
    1.60  done
    1.61  
    1.62 -lemma move_matrix_add: "((move_matrix (A + B) j i)::(('a::lordered_ab_group) matrix)) = (move_matrix A j i) + (move_matrix B j i)" 
    1.63 +lemma move_matrix_add: "((move_matrix (A + B) j i)::(('a::lordered_ab_group_add) matrix)) = (move_matrix A j i) + (move_matrix B j i)" 
    1.64  apply (subst Rep_matrix_inject[symmetric])
    1.65  apply (rule ext)+
    1.66  apply (simp)
    1.67 @@ -280,7 +281,7 @@
    1.68  apply (auto)
    1.69  done
    1.70  
    1.71 -lemma Rep_minus[simp]: "Rep_matrix (-(A::_::lordered_ab_group)) x y = - (Rep_matrix A x y)"
    1.72 +lemma Rep_minus[simp]: "Rep_matrix (-(A::_::lordered_ab_group_add)) x y = - (Rep_matrix A x y)"
    1.73  by (simp add: minus_matrix_def)
    1.74  
    1.75  lemma Rep_abs[simp]: "Rep_matrix (abs (A::_::lordered_ring)) x y = abs (Rep_matrix A x y)"