src/HOL/Matrix/Matrix.thy
author haftmann
Wed Jan 02 15:14:17 2008 +0100 (2008-01-02 ago)
changeset 25764 878c37886eed
parent 25502 9200b36280c0
child 27484 dbb9981c3d18
permissions -rw-r--r--
removed some legacy instantiations
     1 (*  Title:      HOL/Matrix/Matrix.thy
     2     ID:         $Id$
     3     Author:     Steven Obua
     4 *)
     5 
     6 theory Matrix
     7 imports MatrixGeneral
     8 begin
     9 
    10 instantiation matrix :: ("{zero, lattice}") lattice
    11 begin
    12 
    13 definition
    14   "inf = combine_matrix inf"
    15 
    16 definition
    17   "sup = combine_matrix sup"
    18 
    19 instance
    20   by default (auto simp add: inf_le1 inf_le2 le_infI le_matrix_def inf_matrix_def sup_matrix_def)
    21 
    22 end
    23 
    24 instantiation matrix :: ("{plus, zero}") plus
    25 begin
    26 
    27 definition
    28   plus_matrix_def: "A + B = combine_matrix (op +) A B"
    29 
    30 instance ..
    31 
    32 end
    33 
    34 instantiation matrix :: ("{uminus, zero}") uminus
    35 begin
    36 
    37 definition
    38   minus_matrix_def: "- A = apply_matrix uminus A"
    39 
    40 instance ..
    41 
    42 end
    43 
    44 instantiation matrix :: ("{minus, zero}") minus
    45 begin
    46 
    47 definition
    48   diff_matrix_def: "A - B = combine_matrix (op -) A B"
    49 
    50 instance ..
    51 
    52 end
    53 
    54 instantiation matrix :: ("{plus, times, zero}") times
    55 begin
    56 
    57 definition
    58   times_matrix_def: "A * B = mult_matrix (op *) (op +) A B"
    59 
    60 instance ..
    61 
    62 end
    63 
    64 instantiation matrix :: (lordered_ab_group_add) abs
    65 begin
    66 
    67 definition
    68   abs_matrix_def: "abs (A \<Colon> 'a matrix) = sup A (- A)"
    69 
    70 instance ..
    71 
    72 end
    73 
    74 instance matrix :: (lordered_ab_group_add) lordered_ab_group_add_meet
    75 proof 
    76   fix A B C :: "('a::lordered_ab_group_add) matrix"
    77   show "A + B + C = A + (B + C)"    
    78     apply (simp add: plus_matrix_def)
    79     apply (rule combine_matrix_assoc[simplified associative_def, THEN spec, THEN spec, THEN spec])
    80     apply (simp_all add: add_assoc)
    81     done
    82   show "A + B = B + A"
    83     apply (simp add: plus_matrix_def)
    84     apply (rule combine_matrix_commute[simplified commutative_def, THEN spec, THEN spec])
    85     apply (simp_all add: add_commute)
    86     done
    87   show "0 + A = A"
    88     apply (simp add: plus_matrix_def)
    89     apply (rule combine_matrix_zero_l_neutral[simplified zero_l_neutral_def, THEN spec])
    90     apply (simp)
    91     done
    92   show "- A + A = 0" 
    93     by (simp add: plus_matrix_def minus_matrix_def Rep_matrix_inject[symmetric] ext)
    94   show "A - B = A + - B" 
    95     by (simp add: plus_matrix_def diff_matrix_def minus_matrix_def Rep_matrix_inject[symmetric] ext)
    96   assume "A <= B"
    97   then show "C + A <= C + B"
    98     apply (simp add: plus_matrix_def)
    99     apply (rule le_left_combine_matrix)
   100     apply (simp_all)
   101     done
   102 qed
   103 
   104 instance matrix :: (lordered_ring) lordered_ring
   105 proof
   106   fix A B C :: "('a :: lordered_ring) matrix"
   107   show "A * B * C = A * (B * C)"
   108     apply (simp add: times_matrix_def)
   109     apply (rule mult_matrix_assoc)
   110     apply (simp_all add: associative_def ring_simps)
   111     done
   112   show "(A + B) * C = A * C + B * C"
   113     apply (simp add: times_matrix_def plus_matrix_def)
   114     apply (rule l_distributive_matrix[simplified l_distributive_def, THEN spec, THEN spec, THEN spec])
   115     apply (simp_all add: associative_def commutative_def ring_simps)
   116     done
   117   show "A * (B + C) = A * B + A * C"
   118     apply (simp add: times_matrix_def plus_matrix_def)
   119     apply (rule r_distributive_matrix[simplified r_distributive_def, THEN spec, THEN spec, THEN spec])
   120     apply (simp_all add: associative_def commutative_def ring_simps)
   121     done  
   122   show "abs A = sup A (-A)" 
   123     by (simp add: abs_matrix_def)
   124   assume a: "A \<le> B"
   125   assume b: "0 \<le> C"
   126   from a b show "C * A \<le> C * B"
   127     apply (simp add: times_matrix_def)
   128     apply (rule le_left_mult)
   129     apply (simp_all add: add_mono mult_left_mono)
   130     done
   131   from a b show "A * C \<le> B * C"
   132     apply (simp add: times_matrix_def)
   133     apply (rule le_right_mult)
   134     apply (simp_all add: add_mono mult_right_mono)
   135     done
   136 qed 
   137 
   138 lemma Rep_matrix_add[simp]:
   139   "Rep_matrix ((a::('a::lordered_ab_group_add)matrix)+b) j i  = (Rep_matrix a j i) + (Rep_matrix b j i)"
   140 by (simp add: plus_matrix_def)
   141 
   142 lemma Rep_matrix_mult: "Rep_matrix ((a::('a::lordered_ring) matrix) * b) j i = 
   143   foldseq (op +) (% k.  (Rep_matrix a j k) * (Rep_matrix b k i)) (max (ncols a) (nrows b))"
   144 apply (simp add: times_matrix_def)
   145 apply (simp add: Rep_mult_matrix)
   146 done
   147 
   148 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)"
   149 apply (subst Rep_matrix_inject[symmetric])
   150 apply (rule ext)+
   151 apply (simp)
   152 done
   153 
   154 lemma singleton_matrix_add: "singleton_matrix j i ((a::_::lordered_ab_group_add)+b) = (singleton_matrix j i a) + (singleton_matrix j i b)"
   155 apply (subst Rep_matrix_inject[symmetric])
   156 apply (rule ext)+
   157 apply (simp)
   158 done
   159 
   160 lemma nrows_mult: "nrows ((A::('a::lordered_ring) matrix) * B) <= nrows A"
   161 by (simp add: times_matrix_def mult_nrows)
   162 
   163 lemma ncols_mult: "ncols ((A::('a::lordered_ring) matrix) * B) <= ncols B"
   164 by (simp add: times_matrix_def mult_ncols)
   165 
   166 definition
   167   one_matrix :: "nat \<Rightarrow> ('a::{zero,one}) matrix" where
   168   "one_matrix n = Abs_matrix (% j i. if j = i & j < n then 1 else 0)"
   169 
   170 lemma Rep_one_matrix[simp]: "Rep_matrix (one_matrix n) j i = (if (j = i & j < n) then 1 else 0)"
   171 apply (simp add: one_matrix_def)
   172 apply (simplesubst RepAbs_matrix)
   173 apply (rule exI[of _ n], simp add: split_if)+
   174 by (simp add: split_if)
   175 
   176 lemma nrows_one_matrix[simp]: "nrows ((one_matrix n) :: ('a::zero_neq_one)matrix) = n" (is "?r = _")
   177 proof -
   178   have "?r <= n" by (simp add: nrows_le)
   179   moreover have "n <= ?r" by (simp add:le_nrows, arith)
   180   ultimately show "?r = n" by simp
   181 qed
   182 
   183 lemma ncols_one_matrix[simp]: "ncols ((one_matrix n) :: ('a::zero_neq_one)matrix) = n" (is "?r = _")
   184 proof -
   185   have "?r <= n" by (simp add: ncols_le)
   186   moreover have "n <= ?r" by (simp add: le_ncols, arith)
   187   ultimately show "?r = n" by simp
   188 qed
   189 
   190 lemma one_matrix_mult_right[simp]: "ncols A <= n \<Longrightarrow> (A::('a::{lordered_ring,ring_1}) matrix) * (one_matrix n) = A"
   191 apply (subst Rep_matrix_inject[THEN sym])
   192 apply (rule ext)+
   193 apply (simp add: times_matrix_def Rep_mult_matrix)
   194 apply (rule_tac j1="xa" in ssubst[OF foldseq_almostzero])
   195 apply (simp_all)
   196 by (simp add: max_def ncols)
   197 
   198 lemma one_matrix_mult_left[simp]: "nrows A <= n \<Longrightarrow> (one_matrix n) * A = (A::('a::{lordered_ring, ring_1}) matrix)"
   199 apply (subst Rep_matrix_inject[THEN sym])
   200 apply (rule ext)+
   201 apply (simp add: times_matrix_def Rep_mult_matrix)
   202 apply (rule_tac j1="x" in ssubst[OF foldseq_almostzero])
   203 apply (simp_all)
   204 by (simp add: max_def nrows)
   205 
   206 lemma transpose_matrix_mult: "transpose_matrix ((A::('a::{lordered_ring,comm_ring}) matrix)*B) = (transpose_matrix B) * (transpose_matrix A)"
   207 apply (simp add: times_matrix_def)
   208 apply (subst transpose_mult_matrix)
   209 apply (simp_all add: mult_commute)
   210 done
   211 
   212 lemma transpose_matrix_add: "transpose_matrix ((A::('a::lordered_ab_group_add) matrix)+B) = transpose_matrix A + transpose_matrix B"
   213 by (simp add: plus_matrix_def transpose_combine_matrix)
   214 
   215 lemma transpose_matrix_diff: "transpose_matrix ((A::('a::lordered_ab_group_add) matrix)-B) = transpose_matrix A - transpose_matrix B"
   216 by (simp add: diff_matrix_def transpose_combine_matrix)
   217 
   218 lemma transpose_matrix_minus: "transpose_matrix (-(A::('a::lordered_ring) matrix)) = - transpose_matrix (A::('a::lordered_ring) matrix)"
   219 by (simp add: minus_matrix_def transpose_apply_matrix)
   220 
   221 constdefs 
   222   right_inverse_matrix :: "('a::{lordered_ring, ring_1}) matrix \<Rightarrow> 'a matrix \<Rightarrow> bool"
   223   "right_inverse_matrix A X == (A * X = one_matrix (max (nrows A) (ncols X))) \<and> nrows X \<le> ncols A" 
   224   left_inverse_matrix :: "('a::{lordered_ring, ring_1}) matrix \<Rightarrow> 'a matrix \<Rightarrow> bool"
   225   "left_inverse_matrix A X == (X * A = one_matrix (max(nrows X) (ncols A))) \<and> ncols X \<le> nrows A" 
   226   inverse_matrix :: "('a::{lordered_ring, ring_1}) matrix \<Rightarrow> 'a matrix \<Rightarrow> bool"
   227   "inverse_matrix A X == (right_inverse_matrix A X) \<and> (left_inverse_matrix A X)"
   228 
   229 lemma right_inverse_matrix_dim: "right_inverse_matrix A X \<Longrightarrow> nrows A = ncols X"
   230 apply (insert ncols_mult[of A X], insert nrows_mult[of A X])
   231 by (simp add: right_inverse_matrix_def)
   232 
   233 lemma left_inverse_matrix_dim: "left_inverse_matrix A Y \<Longrightarrow> ncols A = nrows Y"
   234 apply (insert ncols_mult[of Y A], insert nrows_mult[of Y A]) 
   235 by (simp add: left_inverse_matrix_def)
   236 
   237 lemma left_right_inverse_matrix_unique: 
   238   assumes "left_inverse_matrix A Y" "right_inverse_matrix A X"
   239   shows "X = Y"
   240 proof -
   241   have "Y = Y * one_matrix (nrows A)" 
   242     apply (subst one_matrix_mult_right)
   243     apply (insert prems)
   244     by (simp_all add: left_inverse_matrix_def)
   245   also have "\<dots> = Y * (A * X)" 
   246     apply (insert prems)
   247     apply (frule right_inverse_matrix_dim)
   248     by (simp add: right_inverse_matrix_def)
   249   also have "\<dots> = (Y * A) * X" by (simp add: mult_assoc)
   250   also have "\<dots> = X" 
   251     apply (insert prems)
   252     apply (frule left_inverse_matrix_dim)
   253     apply (simp_all add:  left_inverse_matrix_def right_inverse_matrix_def one_matrix_mult_left)
   254     done
   255   ultimately show "X = Y" by (simp)
   256 qed
   257 
   258 lemma inverse_matrix_inject: "\<lbrakk> inverse_matrix A X; inverse_matrix A Y \<rbrakk> \<Longrightarrow> X = Y"
   259   by (auto simp add: inverse_matrix_def left_right_inverse_matrix_unique)
   260 
   261 lemma one_matrix_inverse: "inverse_matrix (one_matrix n) (one_matrix n)"
   262   by (simp add: inverse_matrix_def left_inverse_matrix_def right_inverse_matrix_def)
   263 
   264 lemma zero_imp_mult_zero: "(a::'a::ring) = 0 | b = 0 \<Longrightarrow> a * b = 0"
   265 by auto
   266 
   267 lemma Rep_matrix_zero_imp_mult_zero:
   268   "! j i k. (Rep_matrix A j k = 0) | (Rep_matrix B k i) = 0  \<Longrightarrow> A * B = (0::('a::lordered_ring) matrix)"
   269 apply (subst Rep_matrix_inject[symmetric])
   270 apply (rule ext)+
   271 apply (auto simp add: Rep_matrix_mult foldseq_zero zero_imp_mult_zero)
   272 done
   273 
   274 lemma add_nrows: "nrows (A::('a::comm_monoid_add) matrix) <= u \<Longrightarrow> nrows B <= u \<Longrightarrow> nrows (A + B) <= u"
   275 apply (simp add: plus_matrix_def)
   276 apply (rule combine_nrows)
   277 apply (simp_all)
   278 done
   279 
   280 lemma move_matrix_row_mult: "move_matrix ((A::('a::lordered_ring) matrix) * B) j 0 = (move_matrix A j 0) * B"
   281 apply (subst Rep_matrix_inject[symmetric])
   282 apply (rule ext)+
   283 apply (auto simp add: Rep_matrix_mult foldseq_zero)
   284 apply (rule_tac foldseq_zerotail[symmetric])
   285 apply (auto simp add: nrows zero_imp_mult_zero max2)
   286 apply (rule order_trans)
   287 apply (rule ncols_move_matrix_le)
   288 apply (simp add: max1)
   289 done
   290 
   291 lemma move_matrix_col_mult: "move_matrix ((A::('a::lordered_ring) matrix) * B) 0 i = A * (move_matrix B 0 i)"
   292 apply (subst Rep_matrix_inject[symmetric])
   293 apply (rule ext)+
   294 apply (auto simp add: Rep_matrix_mult foldseq_zero)
   295 apply (rule_tac foldseq_zerotail[symmetric])
   296 apply (auto simp add: ncols zero_imp_mult_zero max1)
   297 apply (rule order_trans)
   298 apply (rule nrows_move_matrix_le)
   299 apply (simp add: max2)
   300 done
   301 
   302 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)" 
   303 apply (subst Rep_matrix_inject[symmetric])
   304 apply (rule ext)+
   305 apply (simp)
   306 done
   307 
   308 lemma move_matrix_mult: "move_matrix ((A::('a::lordered_ring) matrix)*B) j i = (move_matrix A j 0) * (move_matrix B 0 i)"
   309 by (simp add: move_matrix_ortho[of "A*B"] move_matrix_col_mult move_matrix_row_mult)
   310 
   311 constdefs
   312   scalar_mult :: "('a::lordered_ring) \<Rightarrow> 'a matrix \<Rightarrow> 'a matrix"
   313   "scalar_mult a m == apply_matrix (op * a) m"
   314 
   315 lemma scalar_mult_zero[simp]: "scalar_mult y 0 = 0" 
   316 by (simp add: scalar_mult_def)
   317 
   318 lemma scalar_mult_add: "scalar_mult y (a+b) = (scalar_mult y a) + (scalar_mult y b)"
   319 by (simp add: scalar_mult_def apply_matrix_add ring_simps)
   320 
   321 lemma Rep_scalar_mult[simp]: "Rep_matrix (scalar_mult y a) j i = y * (Rep_matrix a j i)" 
   322 by (simp add: scalar_mult_def)
   323 
   324 lemma scalar_mult_singleton[simp]: "scalar_mult y (singleton_matrix j i x) = singleton_matrix j i (y * x)"
   325 apply (subst Rep_matrix_inject[symmetric])
   326 apply (rule ext)+
   327 apply (auto)
   328 done
   329 
   330 lemma Rep_minus[simp]: "Rep_matrix (-(A::_::lordered_ab_group_add)) x y = - (Rep_matrix A x y)"
   331 by (simp add: minus_matrix_def)
   332 
   333 lemma Rep_abs[simp]: "Rep_matrix (abs (A::_::lordered_ring)) x y = abs (Rep_matrix A x y)"
   334 by (simp add: abs_lattice sup_matrix_def)
   335 
   336 end