src/HOL/Matrix/Matrix.thy
changeset 27653 180e28bab764
parent 27580 e16f4baa3db6
child 28562 4e74209f113e
     1.1 --- a/src/HOL/Matrix/Matrix.thy	Fri Jul 18 18:25:56 2008 +0200
     1.2 +++ b/src/HOL/Matrix/Matrix.thy	Fri Jul 18 18:25:57 2008 +0200
     1.3 @@ -1489,7 +1489,7 @@
     1.4  
     1.5  end
     1.6  
     1.7 -instantiation matrix :: (lordered_ab_group_add) abs
     1.8 +instantiation matrix :: ("{lattice, uminus, zero}") abs
     1.9  begin
    1.10  
    1.11  definition
    1.12 @@ -1499,14 +1499,29 @@
    1.13  
    1.14  end
    1.15  
    1.16 -instance matrix :: (lordered_ab_group_add) lordered_ab_group_add_meet
    1.17 -proof 
    1.18 -  fix A B C :: "('a::lordered_ab_group_add) matrix"
    1.19 +instance matrix :: (monoid_add) monoid_add
    1.20 +proof
    1.21 +  fix A B C :: "'a matrix"
    1.22    show "A + B + C = A + (B + C)"    
    1.23      apply (simp add: plus_matrix_def)
    1.24      apply (rule combine_matrix_assoc[simplified associative_def, THEN spec, THEN spec, THEN spec])
    1.25      apply (simp_all add: add_assoc)
    1.26      done
    1.27 +  show "0 + A = A"
    1.28 +    apply (simp add: plus_matrix_def)
    1.29 +    apply (rule combine_matrix_zero_l_neutral[simplified zero_l_neutral_def, THEN spec])
    1.30 +    apply (simp)
    1.31 +    done
    1.32 +  show "A + 0 = A"
    1.33 +    apply (simp add: plus_matrix_def)
    1.34 +    apply (rule combine_matrix_zero_r_neutral [simplified zero_r_neutral_def, THEN spec])
    1.35 +    apply (simp)
    1.36 +    done
    1.37 +qed
    1.38 +
    1.39 +instance matrix :: (comm_monoid_add) comm_monoid_add
    1.40 +proof
    1.41 +  fix A B :: "'a matrix"
    1.42    show "A + B = B + A"
    1.43      apply (simp add: plus_matrix_def)
    1.44      apply (rule combine_matrix_commute[simplified commutative_def, THEN spec, THEN spec])
    1.45 @@ -1517,10 +1532,29 @@
    1.46      apply (rule combine_matrix_zero_l_neutral[simplified zero_l_neutral_def, THEN spec])
    1.47      apply (simp)
    1.48      done
    1.49 +qed
    1.50 +
    1.51 +instance matrix :: (group_add) group_add
    1.52 +proof
    1.53 +  fix A B :: "'a matrix"
    1.54 +  show "- A + A = 0" 
    1.55 +    by (simp add: plus_matrix_def minus_matrix_def Rep_matrix_inject[symmetric] ext)
    1.56 +  show "A - B = A + - B"
    1.57 +    by (simp add: plus_matrix_def diff_matrix_def minus_matrix_def Rep_matrix_inject [symmetric] ext diff_minus)
    1.58 +qed
    1.59 +
    1.60 +instance matrix :: (ab_group_add) ab_group_add
    1.61 +proof
    1.62 +  fix A B :: "'a matrix"
    1.63    show "- A + A = 0" 
    1.64      by (simp add: plus_matrix_def minus_matrix_def Rep_matrix_inject[symmetric] ext)
    1.65    show "A - B = A + - B" 
    1.66      by (simp add: plus_matrix_def diff_matrix_def minus_matrix_def Rep_matrix_inject[symmetric] ext)
    1.67 +qed
    1.68 +
    1.69 +instance matrix :: (pordered_ab_group_add) pordered_ab_group_add
    1.70 +proof
    1.71 +  fix A B C :: "'a matrix"
    1.72    assume "A <= B"
    1.73    then show "C + A <= C + B"
    1.74      apply (simp add: plus_matrix_def)
    1.75 @@ -1528,10 +1562,13 @@
    1.76      apply (simp_all)
    1.77      done
    1.78  qed
    1.79 +  
    1.80 +instance matrix :: (lordered_ab_group_add) lordered_ab_group_add_meet ..
    1.81 +instance matrix :: (lordered_ab_group_add) lordered_ab_group_add_join ..
    1.82  
    1.83 -instance matrix :: (lordered_ring) lordered_ring
    1.84 +instance matrix :: (ring) ring
    1.85  proof
    1.86 -  fix A B C :: "('a :: lordered_ring) matrix"
    1.87 +  fix A B C :: "'a matrix"
    1.88    show "A * B * C = A * (B * C)"
    1.89      apply (simp add: times_matrix_def)
    1.90      apply (rule mult_matrix_assoc)
    1.91 @@ -1546,9 +1583,12 @@
    1.92      apply (simp add: times_matrix_def plus_matrix_def)
    1.93      apply (rule r_distributive_matrix[simplified r_distributive_def, THEN spec, THEN spec, THEN spec])
    1.94      apply (simp_all add: associative_def commutative_def ring_simps)
    1.95 -    done  
    1.96 -  show "abs A = sup A (-A)" 
    1.97 -    by (simp add: abs_matrix_def)
    1.98 +    done
    1.99 +qed  
   1.100 +
   1.101 +instance matrix :: (pordered_ring) pordered_ring
   1.102 +proof
   1.103 +  fix A B C :: "'a matrix"
   1.104    assume a: "A \<le> B"
   1.105    assume b: "0 \<le> C"
   1.106    from a b show "C * A \<le> C * B"
   1.107 @@ -1561,34 +1601,42 @@
   1.108      apply (rule le_right_mult)
   1.109      apply (simp_all add: add_mono mult_right_mono)
   1.110      done
   1.111 -qed 
   1.112 +qed
   1.113 +
   1.114 +instance matrix :: (lordered_ring) lordered_ring
   1.115 +proof
   1.116 +  fix A B C :: "('a :: lordered_ring) matrix"
   1.117 +  show "abs A = sup A (-A)" 
   1.118 +    by (simp add: abs_matrix_def)
   1.119 +qed
   1.120  
   1.121  lemma Rep_matrix_add[simp]:
   1.122 -  "Rep_matrix ((a::('a::lordered_ab_group_add)matrix)+b) j i  = (Rep_matrix a j i) + (Rep_matrix b j i)"
   1.123 -by (simp add: plus_matrix_def)
   1.124 +  "Rep_matrix ((a::('a::monoid_add)matrix)+b) j i  = (Rep_matrix a j i) + (Rep_matrix b j i)"
   1.125 +  by (simp add: plus_matrix_def)
   1.126  
   1.127 -lemma Rep_matrix_mult: "Rep_matrix ((a::('a::lordered_ring) matrix) * b) j i = 
   1.128 +lemma Rep_matrix_mult: "Rep_matrix ((a::('a::ring) matrix) * b) j i = 
   1.129    foldseq (op +) (% k.  (Rep_matrix a j k) * (Rep_matrix b k i)) (max (ncols a) (nrows b))"
   1.130  apply (simp add: times_matrix_def)
   1.131  apply (simp add: Rep_mult_matrix)
   1.132  done
   1.133  
   1.134 -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.135 +lemma apply_matrix_add: "! x y. f (x+y) = (f x) + (f y) \<Longrightarrow> f 0 = (0::'a)
   1.136 +  \<Longrightarrow> apply_matrix f ((a::('a::monoid_add) matrix) + b) = (apply_matrix f a) + (apply_matrix f b)"
   1.137  apply (subst Rep_matrix_inject[symmetric])
   1.138  apply (rule ext)+
   1.139  apply (simp)
   1.140  done
   1.141  
   1.142 -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.143 +lemma singleton_matrix_add: "singleton_matrix j i ((a::_::monoid_add)+b) = (singleton_matrix j i a) + (singleton_matrix j i b)"
   1.144  apply (subst Rep_matrix_inject[symmetric])
   1.145  apply (rule ext)+
   1.146  apply (simp)
   1.147  done
   1.148  
   1.149 -lemma nrows_mult: "nrows ((A::('a::lordered_ring) matrix) * B) <= nrows A"
   1.150 +lemma nrows_mult: "nrows ((A::('a::ring) matrix) * B) <= nrows A"
   1.151  by (simp add: times_matrix_def mult_nrows)
   1.152  
   1.153 -lemma ncols_mult: "ncols ((A::('a::lordered_ring) matrix) * B) <= ncols B"
   1.154 +lemma ncols_mult: "ncols ((A::('a::ring) matrix) * B) <= ncols B"
   1.155  by (simp add: times_matrix_def mult_ncols)
   1.156  
   1.157  definition
   1.158 @@ -1615,7 +1663,7 @@
   1.159    ultimately show "?r = n" by simp
   1.160  qed
   1.161  
   1.162 -lemma one_matrix_mult_right[simp]: "ncols A <= n \<Longrightarrow> (A::('a::{lordered_ring,ring_1}) matrix) * (one_matrix n) = A"
   1.163 +lemma one_matrix_mult_right[simp]: "ncols A <= n \<Longrightarrow> (A::('a::{ring_1}) matrix) * (one_matrix n) = A"
   1.164  apply (subst Rep_matrix_inject[THEN sym])
   1.165  apply (rule ext)+
   1.166  apply (simp add: times_matrix_def Rep_mult_matrix)
   1.167 @@ -1623,7 +1671,7 @@
   1.168  apply (simp_all)
   1.169  by (simp add: max_def ncols)
   1.170  
   1.171 -lemma one_matrix_mult_left[simp]: "nrows A <= n \<Longrightarrow> (one_matrix n) * A = (A::('a::{lordered_ring, ring_1}) matrix)"
   1.172 +lemma one_matrix_mult_left[simp]: "nrows A <= n \<Longrightarrow> (one_matrix n) * A = (A::('a::ring_1) matrix)"
   1.173  apply (subst Rep_matrix_inject[THEN sym])
   1.174  apply (rule ext)+
   1.175  apply (simp add: times_matrix_def Rep_mult_matrix)
   1.176 @@ -1631,27 +1679,27 @@
   1.177  apply (simp_all)
   1.178  by (simp add: max_def nrows)
   1.179  
   1.180 -lemma transpose_matrix_mult: "transpose_matrix ((A::('a::{lordered_ring,comm_ring}) matrix)*B) = (transpose_matrix B) * (transpose_matrix A)"
   1.181 +lemma transpose_matrix_mult: "transpose_matrix ((A::('a::comm_ring) matrix)*B) = (transpose_matrix B) * (transpose_matrix A)"
   1.182  apply (simp add: times_matrix_def)
   1.183  apply (subst transpose_mult_matrix)
   1.184  apply (simp_all add: mult_commute)
   1.185  done
   1.186  
   1.187 -lemma transpose_matrix_add: "transpose_matrix ((A::('a::lordered_ab_group_add) matrix)+B) = transpose_matrix A + transpose_matrix B"
   1.188 +lemma transpose_matrix_add: "transpose_matrix ((A::('a::monoid_add) matrix)+B) = transpose_matrix A + transpose_matrix B"
   1.189  by (simp add: plus_matrix_def transpose_combine_matrix)
   1.190  
   1.191 -lemma transpose_matrix_diff: "transpose_matrix ((A::('a::lordered_ab_group_add) matrix)-B) = transpose_matrix A - transpose_matrix B"
   1.192 +lemma transpose_matrix_diff: "transpose_matrix ((A::('a::group_add) matrix)-B) = transpose_matrix A - transpose_matrix B"
   1.193  by (simp add: diff_matrix_def transpose_combine_matrix)
   1.194  
   1.195 -lemma transpose_matrix_minus: "transpose_matrix (-(A::('a::lordered_ring) matrix)) = - transpose_matrix (A::('a::lordered_ring) matrix)"
   1.196 +lemma transpose_matrix_minus: "transpose_matrix (-(A::('a::group_add) matrix)) = - transpose_matrix (A::'a matrix)"
   1.197  by (simp add: minus_matrix_def transpose_apply_matrix)
   1.198  
   1.199  constdefs 
   1.200 -  right_inverse_matrix :: "('a::{lordered_ring, ring_1}) matrix \<Rightarrow> 'a matrix \<Rightarrow> bool"
   1.201 +  right_inverse_matrix :: "('a::{ring_1}) matrix \<Rightarrow> 'a matrix \<Rightarrow> bool"
   1.202    "right_inverse_matrix A X == (A * X = one_matrix (max (nrows A) (ncols X))) \<and> nrows X \<le> ncols A" 
   1.203 -  left_inverse_matrix :: "('a::{lordered_ring, ring_1}) matrix \<Rightarrow> 'a matrix \<Rightarrow> bool"
   1.204 +  left_inverse_matrix :: "('a::{ring_1}) matrix \<Rightarrow> 'a matrix \<Rightarrow> bool"
   1.205    "left_inverse_matrix A X == (X * A = one_matrix (max(nrows X) (ncols A))) \<and> ncols X \<le> nrows A" 
   1.206 -  inverse_matrix :: "('a::{lordered_ring, ring_1}) matrix \<Rightarrow> 'a matrix \<Rightarrow> bool"
   1.207 +  inverse_matrix :: "('a::{ring_1}) matrix \<Rightarrow> 'a matrix \<Rightarrow> bool"
   1.208    "inverse_matrix A X == (right_inverse_matrix A X) \<and> (left_inverse_matrix A X)"
   1.209  
   1.210  lemma right_inverse_matrix_dim: "right_inverse_matrix A X \<Longrightarrow> nrows A = ncols X"
   1.211 @@ -1699,13 +1747,13 @@
   1.212  apply (auto simp add: Rep_matrix_mult foldseq_zero zero_imp_mult_zero)
   1.213  done
   1.214  
   1.215 -lemma add_nrows: "nrows (A::('a::comm_monoid_add) matrix) <= u \<Longrightarrow> nrows B <= u \<Longrightarrow> nrows (A + B) <= u"
   1.216 +lemma add_nrows: "nrows (A::('a::monoid_add) matrix) <= u \<Longrightarrow> nrows B <= u \<Longrightarrow> nrows (A + B) <= u"
   1.217  apply (simp add: plus_matrix_def)
   1.218  apply (rule combine_nrows)
   1.219  apply (simp_all)
   1.220  done
   1.221  
   1.222 -lemma move_matrix_row_mult: "move_matrix ((A::('a::lordered_ring) matrix) * B) j 0 = (move_matrix A j 0) * B"
   1.223 +lemma move_matrix_row_mult: "move_matrix ((A::('a::ring) matrix) * B) j 0 = (move_matrix A j 0) * B"
   1.224  apply (subst Rep_matrix_inject[symmetric])
   1.225  apply (rule ext)+
   1.226  apply (auto simp add: Rep_matrix_mult foldseq_zero)
   1.227 @@ -1716,7 +1764,7 @@
   1.228  apply (simp add: max1)
   1.229  done
   1.230  
   1.231 -lemma move_matrix_col_mult: "move_matrix ((A::('a::lordered_ring) matrix) * B) 0 i = A * (move_matrix B 0 i)"
   1.232 +lemma move_matrix_col_mult: "move_matrix ((A::('a::ring) matrix) * B) 0 i = A * (move_matrix B 0 i)"
   1.233  apply (subst Rep_matrix_inject[symmetric])
   1.234  apply (rule ext)+
   1.235  apply (auto simp add: Rep_matrix_mult foldseq_zero)
   1.236 @@ -1727,17 +1775,17 @@
   1.237  apply (simp add: max2)
   1.238  done
   1.239  
   1.240 -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.241 +lemma move_matrix_add: "((move_matrix (A + B) j i)::(('a::monoid_add) matrix)) = (move_matrix A j i) + (move_matrix B j i)" 
   1.242  apply (subst Rep_matrix_inject[symmetric])
   1.243  apply (rule ext)+
   1.244  apply (simp)
   1.245  done
   1.246  
   1.247 -lemma move_matrix_mult: "move_matrix ((A::('a::lordered_ring) matrix)*B) j i = (move_matrix A j 0) * (move_matrix B 0 i)"
   1.248 +lemma move_matrix_mult: "move_matrix ((A::('a::ring) matrix)*B) j i = (move_matrix A j 0) * (move_matrix B 0 i)"
   1.249  by (simp add: move_matrix_ortho[of "A*B"] move_matrix_col_mult move_matrix_row_mult)
   1.250  
   1.251  constdefs
   1.252 -  scalar_mult :: "('a::lordered_ring) \<Rightarrow> 'a matrix \<Rightarrow> 'a matrix"
   1.253 +  scalar_mult :: "('a::ring) \<Rightarrow> 'a matrix \<Rightarrow> 'a matrix"
   1.254    "scalar_mult a m == apply_matrix (op * a) m"
   1.255  
   1.256  lemma scalar_mult_zero[simp]: "scalar_mult y 0 = 0" 
   1.257 @@ -1755,10 +1803,10 @@
   1.258  apply (auto)
   1.259  done
   1.260  
   1.261 -lemma Rep_minus[simp]: "Rep_matrix (-(A::_::lordered_ab_group_add)) x y = - (Rep_matrix A x y)"
   1.262 +lemma Rep_minus[simp]: "Rep_matrix (-(A::_::group_add)) x y = - (Rep_matrix A x y)"
   1.263  by (simp add: minus_matrix_def)
   1.264  
   1.265 -lemma Rep_abs[simp]: "Rep_matrix (abs (A::_::lordered_ring)) x y = abs (Rep_matrix A x y)"
   1.266 +lemma Rep_abs[simp]: "Rep_matrix (abs (A::_::lordered_ab_group_add)) x y = abs (Rep_matrix A x y)"
   1.267  by (simp add: abs_lattice sup_matrix_def)
   1.268  
   1.269  end