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