src/HOL/Matrix/Matrix.thy
changeset 14940 b9ab8babd8b3
parent 14738 83f1a514dcb4
child 15178 5f621aa35c25
     1.1 --- a/src/HOL/Matrix/Matrix.thy	Sun Jun 13 17:57:35 2004 +0200
     1.2 +++ b/src/HOL/Matrix/Matrix.thy	Mon Jun 14 14:20:55 2004 +0200
     1.3 @@ -1,201 +1,127 @@
     1.4  (*  Title:      HOL/Matrix/Matrix.thy
     1.5      ID:         $Id$
     1.6      Author:     Steven Obua
     1.7 -    License:    2004 Technische Universität München
     1.8  *)
     1.9  
    1.10 -theory Matrix = MatrixGeneral:
    1.11 +theory Matrix=MatrixGeneral:
    1.12 +
    1.13 +instance matrix :: (minus) minus 
    1.14 +by intro_classes
    1.15 +
    1.16 +instance matrix :: (plus) plus
    1.17 +by (intro_classes)
    1.18  
    1.19 -axclass almost_matrix_element < zero, plus, times
    1.20 -matrix_add_assoc: "(a+b)+c = a + (b+c)"
    1.21 -matrix_add_commute: "a+b = b+a"
    1.22 +instance matrix :: ("{plus,times}") times
    1.23 +by (intro_classes)
    1.24 +
    1.25 +defs (overloaded)
    1.26 +  plus_matrix_def: "A + B == combine_matrix (op +) A B"
    1.27 +  diff_matrix_def: "A - B == combine_matrix (op -) A B"
    1.28 +  minus_matrix_def: "- A == apply_matrix uminus A"
    1.29 +  times_matrix_def: "A * B == mult_matrix (op *) (op +) A B"
    1.30 +
    1.31 +lemma is_meet_combine_matrix_meet: "is_meet (combine_matrix meet)"
    1.32 +by (simp_all add: is_meet_def le_matrix_def meet_left_le meet_right_le meet_imp_le)
    1.33  
    1.34 -matrix_mult_assoc: "(a*b)*c = a*(b*c)"
    1.35 -matrix_mult_left_0[simp]: "0 * a = 0"
    1.36 -matrix_mult_right_0[simp]: "a * 0 = 0"
    1.37 -
    1.38 -matrix_left_distrib: "(a+b)*c = a*c+b*c"
    1.39 -matrix_right_distrib: "a*(b+c) = a*b+a*c"
    1.40 -
    1.41 -axclass matrix_element < almost_matrix_element
    1.42 -matrix_add_0[simp]: "0+0 = 0"
    1.43 -
    1.44 -instance matrix :: (plus) plus ..
    1.45 -instance matrix :: (times) times ..
    1.46 +instance matrix :: (lordered_ab_group) lordered_ab_group_meet
    1.47 +proof 
    1.48 +  fix A B C :: "('a::lordered_ab_group) matrix"
    1.49 +  show "A + B + C = A + (B + C)"    
    1.50 +    apply (simp add: plus_matrix_def)
    1.51 +    apply (rule combine_matrix_assoc[simplified associative_def, THEN spec, THEN spec, THEN spec])
    1.52 +    apply (simp_all add: add_assoc)
    1.53 +    done
    1.54 +  show "A + B = B + A"
    1.55 +    apply (simp add: plus_matrix_def)
    1.56 +    apply (rule combine_matrix_commute[simplified commutative_def, THEN spec, THEN spec])
    1.57 +    apply (simp_all add: add_commute)
    1.58 +    done
    1.59 +  show "0 + A = A"
    1.60 +    apply (simp add: plus_matrix_def)
    1.61 +    apply (rule combine_matrix_zero_l_neutral[simplified zero_l_neutral_def, THEN spec])
    1.62 +    apply (simp)
    1.63 +    done
    1.64 +  show "- A + A = 0" 
    1.65 +    by (simp add: plus_matrix_def minus_matrix_def Rep_matrix_inject[symmetric] ext)
    1.66 +  show "A - B = A + - B" 
    1.67 +    by (simp add: plus_matrix_def diff_matrix_def minus_matrix_def Rep_matrix_inject[symmetric] ext)
    1.68 +  show "\<exists>m\<Colon>'a matrix \<Rightarrow> 'a matrix \<Rightarrow> 'a matrix. is_meet m"
    1.69 +    by (auto intro: is_meet_combine_matrix_meet)
    1.70 +  assume "A <= B"
    1.71 +  then show "C + A <= C + B"
    1.72 +    apply (simp add: plus_matrix_def)
    1.73 +    apply (rule le_left_combine_matrix)
    1.74 +    apply (simp_all)
    1.75 +    done
    1.76 +qed
    1.77  
    1.78  defs (overloaded)
    1.79 -plus_matrix_def: "A + B == combine_matrix (op +) A B"
    1.80 -times_matrix_def: "A * B == mult_matrix (op *) (op +) A B"
    1.81 +  abs_matrix_def: "abs (A::('a::lordered_ab_group) matrix) == join A (- A)"
    1.82  
    1.83 -instance matrix :: (matrix_element) matrix_element
    1.84 -proof -
    1.85 -  note combine_matrix_assoc2 = combine_matrix_assoc[simplified associative_def, THEN spec, THEN spec, THEN spec]
    1.86 -  {
    1.87 -    fix A::"('a::matrix_element) matrix"
    1.88 -    fix B
    1.89 -    fix C
    1.90 -    have "(A + B) + C = A + (B + C)"
    1.91 -      apply (simp add: plus_matrix_def)
    1.92 -      apply (rule combine_matrix_assoc2)
    1.93 -      by (simp_all add: matrix_add_assoc)
    1.94 -  }
    1.95 -  note plus_assoc = this
    1.96 -  {
    1.97 -    fix A::"('a::matrix_element) matrix"
    1.98 -    fix B
    1.99 -    fix C
   1.100 -    have "(A * B) * C = A * (B * C)"
   1.101 -      apply (simp add: times_matrix_def)
   1.102 -      apply (rule mult_matrix_assoc_simple)
   1.103 -      apply (simp_all add: associative_def commutative_def distributive_def l_distributive_def r_distributive_def)
   1.104 -      apply (auto)
   1.105 -      apply (simp_all add: matrix_add_assoc)
   1.106 -      apply (simp_all add: matrix_add_commute)
   1.107 -      apply (simp_all add: matrix_mult_assoc)
   1.108 -      by (simp_all add: matrix_left_distrib matrix_right_distrib)
   1.109 -  }
   1.110 -  note mult_assoc = this
   1.111 -  note combine_matrix_commute2 = combine_matrix_commute[simplified commutative_def, THEN spec, THEN spec]
   1.112 -  {
   1.113 -    fix A::"('a::matrix_element) matrix"
   1.114 -    fix B
   1.115 -    have "A + B = B + A"
   1.116 -      apply (simp add: plus_matrix_def)
   1.117 -      apply (insert combine_matrix_commute2[of "op +"])
   1.118 -      apply (rule combine_matrix_commute2)
   1.119 -      by (simp add: matrix_add_commute)
   1.120 -  }
   1.121 -  note plus_commute = this
   1.122 -  have plus_zero: "(0::('a::matrix_element) matrix) + 0 = 0"
   1.123 -    apply (simp add: plus_matrix_def)
   1.124 -    apply (rule combine_matrix_zero)
   1.125 -    by (simp)
   1.126 -  have mult_left_zero: "!! A. (0::('a::matrix_element) matrix) * A = 0" by(simp add: times_matrix_def)
   1.127 -  have mult_right_zero: "!! A. A * (0::('a::matrix_element) matrix) = 0" by (simp add: times_matrix_def)
   1.128 -  note l_distributive_matrix2 = l_distributive_matrix[simplified l_distributive_def matrix_left_distrib, THEN spec, THEN spec, THEN spec]
   1.129 -  {
   1.130 -    fix A::"('a::matrix_element) matrix"
   1.131 -    fix B
   1.132 -    fix C
   1.133 -    have "(A + B) * C = A * C + B * C"
   1.134 -      apply (simp add: plus_matrix_def)
   1.135 -      apply (simp add: times_matrix_def)
   1.136 -      apply (rule l_distributive_matrix2)
   1.137 -      apply (simp_all add: associative_def commutative_def l_distributive_def)
   1.138 -      apply (auto)
   1.139 -      apply (simp_all add: matrix_add_assoc)
   1.140 -      apply (simp_all add: matrix_add_commute)
   1.141 -      by (simp_all add: matrix_left_distrib)
   1.142 -  }
   1.143 -  note left_distrib = this
   1.144 -  note r_distributive_matrix2 = r_distributive_matrix[simplified r_distributive_def matrix_right_distrib, THEN spec, THEN spec, THEN spec]
   1.145 -  {
   1.146 -    fix A::"('a::matrix_element) matrix"
   1.147 -    fix B
   1.148 -    fix C
   1.149 -    have "C * (A + B) = C * A + C * B"
   1.150 -      apply (simp add: plus_matrix_def)
   1.151 -      apply (simp add: times_matrix_def)
   1.152 -      apply (rule r_distributive_matrix2)
   1.153 -      apply (simp_all add: associative_def commutative_def r_distributive_def)
   1.154 -      apply (auto)
   1.155 -      apply (simp_all add: matrix_add_assoc)
   1.156 -      apply (simp_all add: matrix_add_commute)
   1.157 -      by (simp_all add: matrix_right_distrib)
   1.158 -  }
   1.159 -  note right_distrib = this
   1.160 -  show "OFCLASS('a matrix, matrix_element_class)"
   1.161 -    apply (intro_classes)
   1.162 -    apply (simp_all add: plus_assoc)
   1.163 -    apply (simp_all add: plus_commute)
   1.164 -    apply (simp_all add: plus_zero)
   1.165 -    apply (simp_all add: mult_assoc)
   1.166 -    apply (simp_all add: mult_left_zero mult_right_zero)
   1.167 -    by (simp_all add: left_distrib right_distrib)
   1.168 +instance matrix :: (lordered_ring) lordered_ring
   1.169 +proof
   1.170 +  fix A B C :: "('a :: lordered_ring) matrix"
   1.171 +  show "A * B * C = A * (B * C)"
   1.172 +    apply (simp add: times_matrix_def)
   1.173 +    apply (rule mult_matrix_assoc)
   1.174 +    apply (simp_all add: associative_def ring_eq_simps)
   1.175 +    done
   1.176 +  show "(A + B) * C = A * C + B * C"
   1.177 +    apply (simp add: times_matrix_def plus_matrix_def)
   1.178 +    apply (rule l_distributive_matrix[simplified l_distributive_def, THEN spec, THEN spec, THEN spec])
   1.179 +    apply (simp_all add: associative_def commutative_def ring_eq_simps)
   1.180 +    done
   1.181 +  show "A * (B + C) = A * B + A * C"
   1.182 +    apply (simp add: times_matrix_def plus_matrix_def)
   1.183 +    apply (rule r_distributive_matrix[simplified r_distributive_def, THEN spec, THEN spec, THEN spec])
   1.184 +    apply (simp_all add: associative_def commutative_def ring_eq_simps)
   1.185 +    done  
   1.186 +  show "abs A = join A (-A)" 
   1.187 +    by (simp add: abs_matrix_def)
   1.188 +  assume a: "A \<le> B"
   1.189 +  assume b: "0 \<le> C"
   1.190 +  from a b show "C * A \<le> C * B"
   1.191 +    apply (simp add: times_matrix_def)
   1.192 +    apply (rule le_left_mult)
   1.193 +    apply (simp_all add: add_mono mult_left_mono)
   1.194 +    done
   1.195 +  from a b show "A * C \<le> B * C"
   1.196 +    apply (simp add: times_matrix_def)
   1.197 +    apply (rule le_right_mult)
   1.198 +    apply (simp_all add: add_mono mult_right_mono)
   1.199 +    done
   1.200  qed
   1.201  
   1.202 -axclass g_almost_semiring < almost_matrix_element
   1.203 -g_add_left_0[simp]: "0 + a = a"
   1.204 -
   1.205 -lemma g_add_right_0[simp]: "(a::'a::g_almost_semiring) + 0 = a"
   1.206 -by (simp add: matrix_add_commute)
   1.207 -
   1.208 -axclass g_semiring < g_almost_semiring
   1.209 -g_add_leftimp_eq: "a+b = a+c \<Longrightarrow> b = c"
   1.210 -
   1.211 -instance g_almost_semiring < matrix_element
   1.212 -  by intro_classes simp
   1.213 -
   1.214 -instance matrix :: (g_almost_semiring) g_almost_semiring
   1.215 -apply (intro_classes)
   1.216 -by (simp add: plus_matrix_def combine_matrix_def combine_infmatrix_def)
   1.217 +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.218 +by (simp add: plus_matrix_def)
   1.219  
   1.220 -lemma RepAbs_matrix_eq_left: " Rep_matrix(Abs_matrix f) = g \<Longrightarrow> \<exists>m. \<forall>j i. m \<le> j \<longrightarrow> f j i = 0 \<Longrightarrow> \<exists>n. \<forall>j i. n \<le> i \<longrightarrow> f j i = 0 \<Longrightarrow> f = g"
   1.221 -by (simp add: RepAbs_matrix)
   1.222 -
   1.223 -lemma RepAbs_matrix_eq_right: "g = Rep_matrix(Abs_matrix f) \<Longrightarrow> \<exists>m. \<forall>j i. m \<le> j \<longrightarrow> f j i = 0 \<Longrightarrow> \<exists>n. \<forall>j i. n \<le> i \<longrightarrow> f j i = 0 \<Longrightarrow> g = f"
   1.224 -by (simp add: RepAbs_matrix)
   1.225 +lemma Rep_matrix_mult: "Rep_matrix ((a::('a::lordered_ring) matrix) * b) j i = 
   1.226 +  foldseq (op +) (% k.  (Rep_matrix a j k) * (Rep_matrix b k i)) (max (ncols a) (nrows b))"
   1.227 +apply (simp add: times_matrix_def)
   1.228 +apply (simp add: Rep_mult_matrix)
   1.229 +done
   1.230 + 
   1.231  
   1.232 -instance matrix :: (g_semiring) g_semiring
   1.233 -apply (intro_classes)
   1.234 -apply (simp add: plus_matrix_def combine_matrix_def combine_infmatrix_def)
   1.235 -apply (subst Rep_matrix_inject[THEN sym])
   1.236 -apply (drule ssubst[OF Rep_matrix_inject, of "% x. x"])
   1.237 -apply (drule RepAbs_matrix_eq_left)
   1.238 -apply (auto)
   1.239 -apply (rule_tac x="max (nrows a) (nrows b)" in exI, simp add: nrows_le)
   1.240 -apply (rule_tac x="max (ncols a) (ncols b)" in exI, simp add: ncols_le)
   1.241 -apply (drule RepAbs_matrix_eq_right)
   1.242 -apply (rule_tac x="max (nrows a) (nrows c)" in exI, simp add: nrows_le)
   1.243 -apply (rule_tac x="max (ncols a) (ncols c)" in exI, simp add: ncols_le)
   1.244 +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.245 +apply (subst Rep_matrix_inject[symmetric])
   1.246  apply (rule ext)+
   1.247 -apply (drule_tac x="x" and y="x" in comb, simp)
   1.248 -apply (drule_tac x="xa" and y="xa" in comb, simp)
   1.249 -apply (drule g_add_leftimp_eq)
   1.250 -by simp
   1.251 -
   1.252 -axclass pordered_matrix_element < matrix_element, order, zero
   1.253 -pordered_add_right_mono: "a <= b \<Longrightarrow> a + c <= b + c"
   1.254 -pordered_mult_left: "0 <= c \<Longrightarrow> a <= b \<Longrightarrow> c*a <= c*b"
   1.255 -pordered_mult_right: "0 <= c \<Longrightarrow> a <= b \<Longrightarrow> a*c <= b*c"
   1.256 -
   1.257 -lemma pordered_add_left_mono: "(a::'a::pordered_matrix_element) <= b \<Longrightarrow> c + a <= c + b"
   1.258 -apply (insert pordered_add_right_mono[of a b c])
   1.259 -by (simp add: matrix_add_commute)
   1.260 +apply (simp)
   1.261 +done
   1.262  
   1.263 -lemma pordered_add: "(a::'a::pordered_matrix_element) <= b \<Longrightarrow> (c::'a::pordered_matrix_element) <= d \<Longrightarrow> a+c <= b+d"
   1.264 -proof -
   1.265 -  assume p1:"a <= b"
   1.266 -  assume p2:"c <= d"
   1.267 -  have "a+c <= b+c" by (rule pordered_add_right_mono)
   1.268 -  also have "\<dots> <= b+d" by (rule pordered_add_left_mono)
   1.269 -  ultimately show "a+c <= b+d" by simp
   1.270 -qed
   1.271 +lemma singleton_matrix_add: "singleton_matrix j i ((a::_::lordered_ab_group)+b) = (singleton_matrix j i a) + (singleton_matrix j i b)"
   1.272 +apply (subst Rep_matrix_inject[symmetric])
   1.273 +apply (rule ext)+
   1.274 +apply (simp)
   1.275 +done
   1.276  
   1.277 -instance matrix :: (pordered_matrix_element) pordered_matrix_element
   1.278 -apply (intro_classes)
   1.279 -apply (simp_all add: plus_matrix_def times_matrix_def)
   1.280 -apply (rule le_combine_matrix)
   1.281 -apply (simp_all)
   1.282 -apply (simp_all add: pordered_add)
   1.283 -apply (rule le_left_mult)
   1.284 -apply (simp_all add: matrix_add_0 g_add_left_0 pordered_add pordered_mult_left matrix_mult_left_0 matrix_mult_right_0)
   1.285 -apply (rule le_right_mult)
   1.286 -by (simp_all add: pordered_add pordered_mult_right)
   1.287 -
   1.288 -axclass pordered_g_semiring < g_semiring, pordered_matrix_element
   1.289 -
   1.290 -instance matrix :: (pordered_g_semiring) pordered_g_semiring ..
   1.291 -
   1.292 -lemma nrows_mult: "nrows ((A::('a::matrix_element) matrix) * B) <= nrows A"
   1.293 +lemma nrows_mult: "nrows ((A::('a::lordered_ring) matrix) * B) <= nrows A"
   1.294  by (simp add: times_matrix_def mult_nrows)
   1.295  
   1.296 -lemma ncols_mult: "ncols ((A::('a::matrix_element) matrix) * B) <= ncols B"
   1.297 +lemma ncols_mult: "ncols ((A::('a::lordered_ring) matrix) * B) <= ncols B"
   1.298  by (simp add: times_matrix_def mult_ncols)
   1.299  
   1.300 -(*
   1.301  constdefs
   1.302 -  one_matrix :: "nat \<Rightarrow> ('a::comm_semiring_1_cancel) matrix"
   1.303 +  one_matrix :: "nat \<Rightarrow> ('a::{zero,one}) matrix"
   1.304    "one_matrix n == Abs_matrix (% j i. if j = i & j < n then 1 else 0)"
   1.305  
   1.306  lemma Rep_one_matrix[simp]: "Rep_matrix (one_matrix n) j i = (if (j = i & j < n) then 1 else 0)"
   1.307 @@ -204,21 +130,21 @@
   1.308  apply (rule exI[of _ n], simp add: split_if)+
   1.309  by (simp add: split_if, arith)
   1.310  
   1.311 -lemma nrows_one_matrix[simp]: "nrows (one_matrix n) = n" (is "?r = _")
   1.312 +lemma nrows_one_matrix[simp]: "nrows ((one_matrix n) :: ('a::axclass_0_neq_1)matrix) = n" (is "?r = _")
   1.313  proof -
   1.314    have "?r <= n" by (simp add: nrows_le)
   1.315 -  moreover have "n <= ?r" by (simp add: le_nrows, arith)
   1.316 +  moreover have "n <= ?r" by (simp add:le_nrows, arith)
   1.317    ultimately show "?r = n" by simp
   1.318  qed
   1.319  
   1.320 -lemma ncols_one_matrix[simp]: "ncols (one_matrix n) = n" (is "?r = _")
   1.321 +lemma ncols_one_matrix[simp]: "ncols ((one_matrix n) :: ('a::axclass_0_neq_1)matrix) = n" (is "?r = _")
   1.322  proof -
   1.323    have "?r <= n" by (simp add: ncols_le)
   1.324    moreover have "n <= ?r" by (simp add: le_ncols, arith)
   1.325    ultimately show "?r = n" by simp
   1.326  qed
   1.327  
   1.328 -lemma one_matrix_mult_right: "ncols A <= n \<Longrightarrow> A * (one_matrix n) = A"
   1.329 +lemma one_matrix_mult_right[simp]: "ncols A <= n \<Longrightarrow> (A::('a::{lordered_ring,ring_1}) matrix) * (one_matrix n) = A"
   1.330  apply (subst Rep_matrix_inject[THEN sym])
   1.331  apply (rule ext)+
   1.332  apply (simp add: times_matrix_def Rep_mult_matrix)
   1.333 @@ -226,7 +152,7 @@
   1.334  apply (simp_all)
   1.335  by (simp add: max_def ncols)
   1.336  
   1.337 -lemma one_matrix_mult_left: "nrows A <= n \<Longrightarrow> (one_matrix n) * A = A"
   1.338 +lemma one_matrix_mult_left[simp]: "nrows A <= n \<Longrightarrow> (one_matrix n) * A = (A::('a::{lordered_ring, ring_1}) matrix)"
   1.339  apply (subst Rep_matrix_inject[THEN sym])
   1.340  apply (rule ext)+
   1.341  apply (simp add: times_matrix_def Rep_mult_matrix)
   1.342 @@ -234,16 +160,131 @@
   1.343  apply (simp_all)
   1.344  by (simp add: max_def nrows)
   1.345  
   1.346 -constdefs
   1.347 -  right_inverse_matrix :: "('a::comm_semiring_1_cancel) matrix \<Rightarrow> 'a matrix \<Rightarrow> bool"
   1.348 -  "right_inverse_matrix A X == (A * X = one_matrix (max (nrows A) (ncols X)))"
   1.349 -  inverse_matrix :: "('a::comm_semiring_1_cancel) matrix \<Rightarrow> 'a matrix \<Rightarrow> bool"
   1.350 -  "inverse_matrix A X == (right_inverse_matrix A X) \<and> (right_inverse_matrix X A)"
   1.351 +lemma transpose_matrix_mult: "transpose_matrix ((A::('a::{lordered_ring,comm_ring}) matrix)*B) = (transpose_matrix B) * (transpose_matrix A)"
   1.352 +apply (simp add: times_matrix_def)
   1.353 +apply (subst transpose_mult_matrix)
   1.354 +apply (simp_all add: mult_commute)
   1.355 +done
   1.356 +
   1.357 +lemma transpose_matrix_add: "transpose_matrix ((A::('a::lordered_ab_group) matrix)+B) = transpose_matrix A + transpose_matrix B"
   1.358 +by (simp add: plus_matrix_def transpose_combine_matrix)
   1.359 +
   1.360 +lemma transpose_matrix_diff: "transpose_matrix ((A::('a::lordered_ab_group) matrix)-B) = transpose_matrix A - transpose_matrix B"
   1.361 +by (simp add: diff_matrix_def transpose_combine_matrix)
   1.362 +
   1.363 +lemma transpose_matrix_minus: "transpose_matrix (-(A::('a::lordered_ring) matrix)) = - transpose_matrix (A::('a::lordered_ring) matrix)"
   1.364 +by (simp add: minus_matrix_def transpose_apply_matrix)
   1.365 +
   1.366 +constdefs 
   1.367 +  right_inverse_matrix :: "('a::{lordered_ring, ring_1}) matrix \<Rightarrow> 'a matrix \<Rightarrow> bool"
   1.368 +  "right_inverse_matrix A X == (A * X = one_matrix (max (nrows A) (ncols X))) \<and> nrows X \<le> ncols A" 
   1.369 +  left_inverse_matrix :: "('a::{lordered_ring, ring_1}) matrix \<Rightarrow> 'a matrix \<Rightarrow> bool"
   1.370 +  "left_inverse_matrix A X == (X * A = one_matrix (max(nrows X) (ncols A))) \<and> ncols X \<le> nrows A" 
   1.371 +  inverse_matrix :: "('a::{lordered_ring, ring_1}) matrix \<Rightarrow> 'a matrix \<Rightarrow> bool"
   1.372 +  "inverse_matrix A X == (right_inverse_matrix A X) \<and> (left_inverse_matrix A X)"
   1.373  
   1.374  lemma right_inverse_matrix_dim: "right_inverse_matrix A X \<Longrightarrow> nrows A = ncols X"
   1.375  apply (insert ncols_mult[of A X], insert nrows_mult[of A X])
   1.376  by (simp add: right_inverse_matrix_def)
   1.377  
   1.378 -text {* to be continued \dots *}
   1.379 -*)
   1.380 +lemma left_inverse_matrix_dim: "left_inverse_matrix A Y \<Longrightarrow> ncols A = nrows Y"
   1.381 +apply (insert ncols_mult[of Y A], insert nrows_mult[of Y A]) 
   1.382 +by (simp add: left_inverse_matrix_def)
   1.383 +
   1.384 +lemma left_right_inverse_matrix_unique: 
   1.385 +  assumes "left_inverse_matrix A Y" "right_inverse_matrix A X"
   1.386 +  shows "X = Y"
   1.387 +proof -
   1.388 +  have "Y = Y * one_matrix (nrows A)" 
   1.389 +    apply (subst one_matrix_mult_right)
   1.390 +    apply (insert prems)
   1.391 +    by (simp_all add: left_inverse_matrix_def)
   1.392 +  also have "\<dots> = Y * (A * X)" 
   1.393 +    apply (insert prems)
   1.394 +    apply (frule right_inverse_matrix_dim)
   1.395 +    by (simp add: right_inverse_matrix_def)
   1.396 +  also have "\<dots> = (Y * A) * X" by (simp add: mult_assoc)
   1.397 +  also have "\<dots> = X" 
   1.398 +    apply (insert prems)
   1.399 +    apply (frule left_inverse_matrix_dim)
   1.400 +    apply (simp_all add:  left_inverse_matrix_def right_inverse_matrix_def one_matrix_mult_left)
   1.401 +    done
   1.402 +  ultimately show "X = Y" by (simp)
   1.403 +qed
   1.404 +
   1.405 +lemma inverse_matrix_inject: "\<lbrakk> inverse_matrix A X; inverse_matrix A Y \<rbrakk> \<Longrightarrow> X = Y"
   1.406 +  by (auto simp add: inverse_matrix_def left_right_inverse_matrix_unique)
   1.407 +
   1.408 +lemma one_matrix_inverse: "inverse_matrix (one_matrix n) (one_matrix n)"
   1.409 +  by (simp add: inverse_matrix_def left_inverse_matrix_def right_inverse_matrix_def)
   1.410 +
   1.411 +lemma zero_imp_mult_zero: "(a::'a::ring) = 0 | b = 0 \<Longrightarrow> a * b = 0"
   1.412 +by auto
   1.413 +
   1.414 +lemma Rep_matrix_zero_imp_mult_zero:
   1.415 +  "! j i k. (Rep_matrix A j k = 0) | (Rep_matrix B k i) = 0  \<Longrightarrow> A * B = (0::('a::lordered_ring) matrix)"
   1.416 +apply (subst Rep_matrix_inject[symmetric])
   1.417 +apply (rule ext)+
   1.418 +apply (auto simp add: Rep_matrix_mult foldseq_zero zero_imp_mult_zero)
   1.419 +done
   1.420 +
   1.421 +lemma add_nrows: "nrows (A::('a::comm_monoid_add) matrix) <= u \<Longrightarrow> nrows B <= u \<Longrightarrow> nrows (A + B) <= u"
   1.422 +apply (simp add: plus_matrix_def)
   1.423 +apply (rule combine_nrows)
   1.424 +apply (simp_all)
   1.425 +done
   1.426 +
   1.427 +lemma move_matrix_row_mult: "move_matrix ((A::('a::lordered_ring) matrix) * B) j 0 = (move_matrix A j 0) * B"
   1.428 +apply (subst Rep_matrix_inject[symmetric])
   1.429 +apply (rule ext)+
   1.430 +apply (auto simp add: Rep_matrix_mult foldseq_zero)
   1.431 +apply (rule_tac foldseq_zerotail[symmetric])
   1.432 +apply (auto simp add: nrows zero_imp_mult_zero max2)
   1.433 +apply (rule order_trans)
   1.434 +apply (rule ncols_move_matrix_le)
   1.435 +apply (simp add: max1)
   1.436 +done
   1.437 +
   1.438 +lemma move_matrix_col_mult: "move_matrix ((A::('a::lordered_ring) matrix) * B) 0 i = A * (move_matrix B 0 i)"
   1.439 +apply (subst Rep_matrix_inject[symmetric])
   1.440 +apply (rule ext)+
   1.441 +apply (auto simp add: Rep_matrix_mult foldseq_zero)
   1.442 +apply (rule_tac foldseq_zerotail[symmetric])
   1.443 +apply (auto simp add: ncols zero_imp_mult_zero max1)
   1.444 +apply (rule order_trans)
   1.445 +apply (rule nrows_move_matrix_le)
   1.446 +apply (simp add: max2)
   1.447 +done
   1.448 +
   1.449 +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.450 +apply (subst Rep_matrix_inject[symmetric])
   1.451 +apply (rule ext)+
   1.452 +apply (simp)
   1.453 +done
   1.454 +
   1.455 +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.456 +by (simp add: move_matrix_ortho[of "A*B"] move_matrix_col_mult move_matrix_row_mult)
   1.457 +
   1.458 +constdefs
   1.459 +  scalar_mult :: "('a::lordered_ring) \<Rightarrow> 'a matrix \<Rightarrow> 'a matrix"
   1.460 +  "scalar_mult a m == apply_matrix (op * a) m"
   1.461 +
   1.462 +lemma scalar_mult_zero[simp]: "scalar_mult y 0 = 0" 
   1.463 +  by (simp add: scalar_mult_def)
   1.464 +
   1.465 +lemma scalar_mult_add: "scalar_mult y (a+b) = (scalar_mult y a) + (scalar_mult y b)"
   1.466 +  by (simp add: scalar_mult_def apply_matrix_add ring_eq_simps)
   1.467 +
   1.468 +lemma Rep_scalar_mult[simp]: "Rep_matrix (scalar_mult y a) j i = y * (Rep_matrix a j i)" 
   1.469 +  by (simp add: scalar_mult_def)
   1.470 +
   1.471 +lemma scalar_mult_singleton[simp]: "scalar_mult y (singleton_matrix j i x) = singleton_matrix j i (y * x)"
   1.472 +  apply (subst Rep_matrix_inject[symmetric])
   1.473 +  apply (rule ext)+
   1.474 +  apply (auto)
   1.475 +  done
   1.476 +
   1.477 +
   1.478 +
   1.479 +
   1.480  end