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