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.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.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.25 +  "Rep_matrix ((a::('a::lordered_ab_group_add)matrix)+b) j i  = (Rep_matrix a j i) + (Rep_matrix b j i)"
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.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.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.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)"