src/HOL/Matrix/Matrix.thy
author wenzelm
Fri Apr 23 20:49:26 2004 +0200 (2004-04-23 ago)
changeset 14662 d2c6a0f030ab
parent 14593 90c88e7ef62d
child 14691 e1eedc8cad37
permissions -rw-r--r--
proper document setup;
     1 (*  Title:      HOL/Matrix/Matrix.thy
     2     ID:         $Id$
     3     Author:     Steven Obua
     4     License:    2004 Technische Universität München
     5 *)
     6 
     7 theory Matrix = MatrixGeneral:
     8 
     9 axclass almost_matrix_element < zero, plus, times
    10 matrix_add_assoc: "(a+b)+c = a + (b+c)"
    11 matrix_add_commute: "a+b = b+a"
    12 
    13 matrix_mult_assoc: "(a*b)*c = a*(b*c)"
    14 matrix_mult_left_0[simp]: "0 * a = 0"
    15 matrix_mult_right_0[simp]: "a * 0 = 0"
    16 
    17 matrix_left_distrib: "(a+b)*c = a*c+b*c"
    18 matrix_right_distrib: "a*(b+c) = a*b+a*c"
    19 
    20 axclass matrix_element < almost_matrix_element
    21 matrix_add_0[simp]: "0+0 = 0"
    22 
    23 instance matrix :: (plus) plus
    24 by (intro_classes)
    25 
    26 instance matrix :: (times) times
    27 by (intro_classes)
    28 
    29 defs (overloaded)
    30 plus_matrix_def: "A + B == combine_matrix (op +) A B"
    31 times_matrix_def: "A * B == mult_matrix (op *) (op +) A B"
    32 
    33 instance matrix :: (matrix_element) matrix_element
    34 proof -
    35   note combine_matrix_assoc2 = combine_matrix_assoc[simplified associative_def, THEN spec, THEN spec, THEN spec]
    36   {
    37     fix A::"('a::matrix_element) matrix"
    38     fix B
    39     fix C
    40     have "(A + B) + C = A + (B + C)"
    41       apply (simp add: plus_matrix_def)
    42       apply (rule combine_matrix_assoc2)
    43       by (simp_all add: matrix_add_assoc)
    44   }
    45   note plus_assoc = this
    46   {
    47     fix A::"('a::matrix_element) matrix"
    48     fix B
    49     fix C
    50     have "(A * B) * C = A * (B * C)"
    51       apply (simp add: times_matrix_def)
    52       apply (rule mult_matrix_assoc_simple)
    53       apply (simp_all add: associative_def commutative_def distributive_def l_distributive_def r_distributive_def)
    54       apply (auto)
    55       apply (simp_all add: matrix_add_assoc)
    56       apply (simp_all add: matrix_add_commute)
    57       apply (simp_all add: matrix_mult_assoc)
    58       by (simp_all add: matrix_left_distrib matrix_right_distrib)
    59   }
    60   note mult_assoc = this
    61   note combine_matrix_commute2 = combine_matrix_commute[simplified commutative_def, THEN spec, THEN spec]
    62   {
    63     fix A::"('a::matrix_element) matrix"
    64     fix B
    65     have "A + B = B + A"
    66       apply (simp add: plus_matrix_def)
    67       apply (insert combine_matrix_commute2[of "op +"])
    68       apply (rule combine_matrix_commute2)
    69       by (simp add: matrix_add_commute)
    70   }
    71   note plus_commute = this
    72   have plus_zero: "(0::('a::matrix_element) matrix) + 0 = 0"
    73     apply (simp add: plus_matrix_def)
    74     apply (rule combine_matrix_zero)
    75     by (simp)
    76   have mult_left_zero: "!! A. (0::('a::matrix_element) matrix) * A = 0" by(simp add: times_matrix_def)
    77   have mult_right_zero: "!! A. A * (0::('a::matrix_element) matrix) = 0" by (simp add: times_matrix_def)
    78   note l_distributive_matrix2 = l_distributive_matrix[simplified l_distributive_def matrix_left_distrib, THEN spec, THEN spec, THEN spec]
    79   {
    80     fix A::"('a::matrix_element) matrix"
    81     fix B
    82     fix C
    83     have "(A + B) * C = A * C + B * C"
    84       apply (simp add: plus_matrix_def)
    85       apply (simp add: times_matrix_def)
    86       apply (rule l_distributive_matrix2)
    87       apply (simp_all add: associative_def commutative_def l_distributive_def)
    88       apply (auto)
    89       apply (simp_all add: matrix_add_assoc)
    90       apply (simp_all add: matrix_add_commute)
    91       by (simp_all add: matrix_left_distrib)
    92   }
    93   note left_distrib = this
    94   note r_distributive_matrix2 = r_distributive_matrix[simplified r_distributive_def matrix_right_distrib, THEN spec, THEN spec, THEN spec]
    95   {
    96     fix A::"('a::matrix_element) matrix"
    97     fix B
    98     fix C
    99     have "C * (A + B) = C * A + C * B"
   100       apply (simp add: plus_matrix_def)
   101       apply (simp add: times_matrix_def)
   102       apply (rule r_distributive_matrix2)
   103       apply (simp_all add: associative_def commutative_def r_distributive_def)
   104       apply (auto)
   105       apply (simp_all add: matrix_add_assoc)
   106       apply (simp_all add: matrix_add_commute)
   107       by (simp_all add: matrix_right_distrib)
   108   }
   109   note right_distrib = this
   110   show "OFCLASS('a matrix, matrix_element_class)"
   111     apply (intro_classes)
   112     apply (simp_all add: plus_assoc)
   113     apply (simp_all add: plus_commute)
   114     apply (simp_all add: plus_zero)
   115     apply (simp_all add: mult_assoc)
   116     apply (simp_all add: mult_left_zero mult_right_zero)
   117     by (simp_all add: left_distrib right_distrib)
   118 qed
   119 
   120 axclass g_almost_semiring < almost_matrix_element
   121 g_add_left_0[simp]: "0 + a = a"
   122 
   123 lemma g_add_right_0[simp]: "(a::'a::g_almost_semiring) + 0 = a"
   124 by (simp add: matrix_add_commute)
   125 
   126 axclass g_semiring < g_almost_semiring
   127 g_add_leftimp_eq: "a+b = a+c \<Longrightarrow> b = c"
   128 
   129 instance g_almost_semiring < matrix_element
   130 by (intro_classes, simp)
   131 
   132 instance semiring < g_semiring
   133 apply (intro_classes)
   134 apply (simp_all add: add_ac)
   135 by (simp_all add: mult_assoc left_distrib right_distrib)
   136 
   137 instance matrix :: (g_almost_semiring) g_almost_semiring
   138 apply (intro_classes)
   139 by (simp add: plus_matrix_def combine_matrix_def combine_infmatrix_def)
   140 
   141 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"
   142 by (simp add: RepAbs_matrix)
   143 
   144 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"
   145 by (simp add: RepAbs_matrix)
   146 
   147 instance matrix :: (g_semiring) g_semiring
   148 apply (intro_classes)
   149 apply (simp add: plus_matrix_def combine_matrix_def combine_infmatrix_def)
   150 apply (subst Rep_matrix_inject[THEN sym])
   151 apply (drule ssubst[OF Rep_matrix_inject, of "% x. x"])
   152 apply (drule RepAbs_matrix_eq_left)
   153 apply (auto)
   154 apply (rule_tac x="max (nrows a) (nrows b)" in exI, simp add: nrows_le)
   155 apply (rule_tac x="max (ncols a) (ncols b)" in exI, simp add: ncols_le)
   156 apply (drule RepAbs_matrix_eq_right)
   157 apply (rule_tac x="max (nrows a) (nrows c)" in exI, simp add: nrows_le)
   158 apply (rule_tac x="max (ncols a) (ncols c)" in exI, simp add: ncols_le)
   159 apply (rule ext)+
   160 apply (drule_tac x="x" and y="x" in comb, simp)
   161 apply (drule_tac x="xa" and y="xa" in comb, simp)
   162 apply (drule g_add_leftimp_eq)
   163 by simp
   164 
   165 axclass pordered_matrix_element < matrix_element, order, zero
   166 pordered_add_right_mono: "a <= b \<Longrightarrow> a + c <= b + c"
   167 pordered_mult_left: "0 <= c \<Longrightarrow> a <= b \<Longrightarrow> c*a <= c*b"
   168 pordered_mult_right: "0 <= c \<Longrightarrow> a <= b \<Longrightarrow> a*c <= b*c"
   169 
   170 lemma pordered_add_left_mono: "(a::'a::pordered_matrix_element) <= b \<Longrightarrow> c + a <= c + b"
   171 apply (insert pordered_add_right_mono[of a b c])
   172 by (simp add: matrix_add_commute)
   173 
   174 lemma pordered_add: "(a::'a::pordered_matrix_element) <= b \<Longrightarrow> (c::'a::pordered_matrix_element) <= d \<Longrightarrow> a+c <= b+d"
   175 proof -
   176   assume p1:"a <= b"
   177   assume p2:"c <= d"
   178   have "a+c <= b+c" by (rule pordered_add_right_mono)
   179   also have "\<dots> <= b+d" by (rule pordered_add_left_mono)
   180   ultimately show "a+c <= b+d" by simp
   181 qed
   182 
   183 instance matrix :: (pordered_matrix_element) pordered_matrix_element
   184 apply (intro_classes)
   185 apply (simp_all add: plus_matrix_def times_matrix_def)
   186 apply (rule le_combine_matrix)
   187 apply (simp_all)
   188 apply (simp_all add: pordered_add)
   189 apply (rule le_left_mult)
   190 apply (simp_all add: matrix_add_0 g_add_left_0 pordered_add pordered_mult_left matrix_mult_left_0 matrix_mult_right_0)
   191 apply (rule le_right_mult)
   192 by (simp_all add: pordered_add pordered_mult_right)
   193 
   194 axclass pordered_g_semiring < g_semiring, pordered_matrix_element
   195 
   196 instance almost_ordered_semiring < pordered_g_semiring
   197 apply (intro_classes)
   198 by (simp_all add: add_right_mono mult_right_mono mult_left_mono)
   199 
   200 instance matrix :: (pordered_g_semiring) pordered_g_semiring
   201 by (intro_classes)
   202 
   203 lemma nrows_mult: "nrows ((A::('a::matrix_element) matrix) * B) <= nrows A"
   204 by (simp add: times_matrix_def mult_nrows)
   205 
   206 lemma ncols_mult: "ncols ((A::('a::matrix_element) matrix) * B) <= ncols B"
   207 by (simp add: times_matrix_def mult_ncols)
   208 
   209 constdefs
   210   one_matrix :: "nat \<Rightarrow> ('a::semiring) matrix"
   211   "one_matrix n == Abs_matrix (% j i. if j = i & j < n then 1 else 0)"
   212 
   213 lemma Rep_one_matrix[simp]: "Rep_matrix (one_matrix n) j i = (if (j = i & j < n) then 1 else 0)"
   214 apply (simp add: one_matrix_def)
   215 apply (subst RepAbs_matrix)
   216 apply (rule exI[of _ n], simp add: split_if)+
   217 by (simp add: split_if, arith)
   218 
   219 lemma nrows_one_matrix[simp]: "nrows (one_matrix n) = n" (is "?r = _")
   220 proof -
   221   have "?r <= n" by (simp add: nrows_le)
   222   moreover have "n <= ?r" by (simp add: le_nrows, arith)
   223   ultimately show "?r = n" by simp
   224 qed
   225 
   226 lemma ncols_one_matrix[simp]: "ncols (one_matrix n) = n" (is "?r = _")
   227 proof -
   228   have "?r <= n" by (simp add: ncols_le)
   229   moreover have "n <= ?r" by (simp add: le_ncols, arith)
   230   ultimately show "?r = n" by simp
   231 qed
   232 
   233 lemma one_matrix_mult_right: "ncols A <= n \<Longrightarrow> A * (one_matrix n) = A"
   234 apply (subst Rep_matrix_inject[THEN sym])
   235 apply (rule ext)+
   236 apply (simp add: times_matrix_def Rep_mult_matrix)
   237 apply (rule_tac j1="xa" in ssubst[OF foldseq_almostzero])
   238 apply (simp_all)
   239 by (simp add: max_def ncols)
   240 
   241 lemma one_matrix_mult_left: "nrows A <= n \<Longrightarrow> (one_matrix n) * A = A"
   242 apply (subst Rep_matrix_inject[THEN sym])
   243 apply (rule ext)+
   244 apply (simp add: times_matrix_def Rep_mult_matrix)
   245 apply (rule_tac j1="x" in ssubst[OF foldseq_almostzero])
   246 apply (simp_all)
   247 by (simp add: max_def nrows)
   248 
   249 constdefs
   250   right_inverse_matrix :: "('a::semiring) matrix \<Rightarrow> 'a matrix \<Rightarrow> bool"
   251   "right_inverse_matrix A X == (A * X = one_matrix (max (nrows A) (ncols X)))"
   252   inverse_matrix :: "('a::semiring) matrix \<Rightarrow> 'a matrix \<Rightarrow> bool"
   253   "inverse_matrix A X == (right_inverse_matrix A X) \<and> (right_inverse_matrix X A)"
   254 
   255 lemma right_inverse_matrix_dim: "right_inverse_matrix A X \<Longrightarrow> nrows A = ncols X"
   256 apply (insert ncols_mult[of A X], insert nrows_mult[of A X])
   257 by (simp add: right_inverse_matrix_def)
   258 
   259 text {* to be continued \dots *}
   260 
   261 end