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