Matrices form a semiring with 0
authorhoelzl
Mon Jan 11 11:47:38 2010 +0100 (2010-01-11 ago)
changeset 348726ca970cfa873
parent 34310 a3d66403f9c9
child 34873 c6449a41b214
Matrices form a semiring with 0
src/HOL/Matrix/Matrix.thy
     1.1 --- a/src/HOL/Matrix/Matrix.thy	Mon Jan 11 10:55:43 2010 +0100
     1.2 +++ b/src/HOL/Matrix/Matrix.thy	Mon Jan 11 11:47:38 2010 +0100
     1.3 @@ -1559,7 +1559,7 @@
     1.4  instance matrix :: (lordered_ab_group_add) lordered_ab_group_add_meet ..
     1.5  instance matrix :: (lordered_ab_group_add) lordered_ab_group_add_join ..
     1.6  
     1.7 -instance matrix :: (ring) ring
     1.8 +instance matrix :: (semiring_0) semiring_0
     1.9  proof
    1.10    fix A B C :: "'a matrix"
    1.11    show "A * B * C = A * (B * C)"
    1.12 @@ -1577,7 +1577,11 @@
    1.13      apply (rule r_distributive_matrix[simplified r_distributive_def, THEN spec, THEN spec, THEN spec])
    1.14      apply (simp_all add: associative_def commutative_def algebra_simps)
    1.15      done
    1.16 -qed  
    1.17 +  show "0 * A = 0" by (simp add: times_matrix_def)
    1.18 +  show "A * 0 = 0" by (simp add: times_matrix_def)
    1.19 +qed
    1.20 +
    1.21 +instance matrix :: (ring) ring ..
    1.22  
    1.23  instance matrix :: (pordered_ring) pordered_ring
    1.24  proof
    1.25 @@ -1607,7 +1611,7 @@
    1.26    "Rep_matrix ((a::('a::monoid_add)matrix)+b) j i  = (Rep_matrix a j i) + (Rep_matrix b j i)"
    1.27    by (simp add: plus_matrix_def)
    1.28  
    1.29 -lemma Rep_matrix_mult: "Rep_matrix ((a::('a::ring) matrix) * b) j i = 
    1.30 +lemma Rep_matrix_mult: "Rep_matrix ((a::('a::semiring_0) matrix) * b) j i = 
    1.31    foldseq (op +) (% k.  (Rep_matrix a j k) * (Rep_matrix b k i)) (max (ncols a) (nrows b))"
    1.32  apply (simp add: times_matrix_def)
    1.33  apply (simp add: Rep_mult_matrix)
    1.34 @@ -1626,10 +1630,10 @@
    1.35  apply (simp)
    1.36  done
    1.37  
    1.38 -lemma nrows_mult: "nrows ((A::('a::ring) matrix) * B) <= nrows A"
    1.39 +lemma nrows_mult: "nrows ((A::('a::semiring_0) matrix) * B) <= nrows A"
    1.40  by (simp add: times_matrix_def mult_nrows)
    1.41  
    1.42 -lemma ncols_mult: "ncols ((A::('a::ring) matrix) * B) <= ncols B"
    1.43 +lemma ncols_mult: "ncols ((A::('a::semiring_0) matrix) * B) <= ncols B"
    1.44  by (simp add: times_matrix_def mult_ncols)
    1.45  
    1.46  definition
    1.47 @@ -1656,7 +1660,7 @@
    1.48    ultimately show "?r = n" by simp
    1.49  qed
    1.50  
    1.51 -lemma one_matrix_mult_right[simp]: "ncols A <= n \<Longrightarrow> (A::('a::{ring_1}) matrix) * (one_matrix n) = A"
    1.52 +lemma one_matrix_mult_right[simp]: "ncols A <= n \<Longrightarrow> (A::('a::{semiring_1}) matrix) * (one_matrix n) = A"
    1.53  apply (subst Rep_matrix_inject[THEN sym])
    1.54  apply (rule ext)+
    1.55  apply (simp add: times_matrix_def Rep_mult_matrix)
    1.56 @@ -1664,7 +1668,7 @@
    1.57  apply (simp_all)
    1.58  by (simp add: ncols)
    1.59  
    1.60 -lemma one_matrix_mult_left[simp]: "nrows A <= n \<Longrightarrow> (one_matrix n) * A = (A::('a::ring_1) matrix)"
    1.61 +lemma one_matrix_mult_left[simp]: "nrows A <= n \<Longrightarrow> (one_matrix n) * A = (A::('a::semiring_1) matrix)"
    1.62  apply (subst Rep_matrix_inject[THEN sym])
    1.63  apply (rule ext)+
    1.64  apply (simp add: times_matrix_def Rep_mult_matrix)
    1.65 @@ -1730,7 +1734,7 @@
    1.66  lemma one_matrix_inverse: "inverse_matrix (one_matrix n) (one_matrix n)"
    1.67    by (simp add: inverse_matrix_def left_inverse_matrix_def right_inverse_matrix_def)
    1.68  
    1.69 -lemma zero_imp_mult_zero: "(a::'a::ring) = 0 | b = 0 \<Longrightarrow> a * b = 0"
    1.70 +lemma zero_imp_mult_zero: "(a::'a::semiring_0) = 0 | b = 0 \<Longrightarrow> a * b = 0"
    1.71  by auto
    1.72  
    1.73  lemma Rep_matrix_zero_imp_mult_zero:
    1.74 @@ -1746,7 +1750,7 @@
    1.75  apply (simp_all)
    1.76  done
    1.77  
    1.78 -lemma move_matrix_row_mult: "move_matrix ((A::('a::ring) matrix) * B) j 0 = (move_matrix A j 0) * B"
    1.79 +lemma move_matrix_row_mult: "move_matrix ((A::('a::semiring_0) matrix) * B) j 0 = (move_matrix A j 0) * B"
    1.80  apply (subst Rep_matrix_inject[symmetric])
    1.81  apply (rule ext)+
    1.82  apply (auto simp add: Rep_matrix_mult foldseq_zero)
    1.83 @@ -1757,7 +1761,7 @@
    1.84  apply (simp add: max1)
    1.85  done
    1.86  
    1.87 -lemma move_matrix_col_mult: "move_matrix ((A::('a::ring) matrix) * B) 0 i = A * (move_matrix B 0 i)"
    1.88 +lemma move_matrix_col_mult: "move_matrix ((A::('a::semiring_0) matrix) * B) 0 i = A * (move_matrix B 0 i)"
    1.89  apply (subst Rep_matrix_inject[symmetric])
    1.90  apply (rule ext)+
    1.91  apply (auto simp add: Rep_matrix_mult foldseq_zero)
    1.92 @@ -1774,7 +1778,7 @@
    1.93  apply (simp)
    1.94  done
    1.95  
    1.96 -lemma move_matrix_mult: "move_matrix ((A::('a::ring) matrix)*B) j i = (move_matrix A j 0) * (move_matrix B 0 i)"
    1.97 +lemma move_matrix_mult: "move_matrix ((A::('a::semiring_0) matrix)*B) j i = (move_matrix A j 0) * (move_matrix B 0 i)"
    1.98  by (simp add: move_matrix_ortho[of "A*B"] move_matrix_col_mult move_matrix_row_mult)
    1.99  
   1.100  constdefs