wneuper/isa: src/HOL/Matrix/Matrix.thy@83f1a514dcb4

     1 (*  Title:      HOL/Matrix/Matrix.thy

     2     ID:         $Id$

     3     Author:     Steven Obua

     4     License:    2004 Technische Universität München

     5 *)

     7 theory Matrix = MatrixGeneral:

     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"

    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"

    17 matrix_left_distrib: "(a+b)*c = a*c+b*c"

    18 matrix_right_distrib: "a*(b+c) = a*b+a*c"

    20 axclass matrix_element < almost_matrix_element

    21 matrix_add_0[simp]: "0+0 = 0"

    23 instance matrix :: (plus) plus ..

    24 instance matrix :: (times) times ..

    26 defs (overloaded)

    27 plus_matrix_def: "A + B == combine_matrix (op +) A B"

    28 times_matrix_def: "A * B == mult_matrix (op *) (op +) A B"

    30 instance matrix :: (matrix_element) matrix_element

    31 proof -

    32   note combine_matrix_assoc2 = combine_matrix_assoc[simplified associative_def, THEN spec, THEN spec, THEN spec]

    33   {

    34     fix A::"('a::matrix_element) matrix"

    35     fix B

    36     fix C

    37     have "(A + B) + C = A + (B + C)"

    38       apply (simp add: plus_matrix_def)

    39       apply (rule combine_matrix_assoc2)

    40       by (simp_all add: matrix_add_assoc)

    41   }

    42   note plus_assoc = this

    43   {

    44     fix A::"('a::matrix_element) matrix"

    45     fix B

    46     fix C

    47     have "(A * B) * C = A * (B * C)"

    48       apply (simp add: times_matrix_def)

    49       apply (rule mult_matrix_assoc_simple)

    50       apply (simp_all add: associative_def commutative_def distributive_def l_distributive_def r_distributive_def)

    51       apply (auto)

    52       apply (simp_all add: matrix_add_assoc)

    53       apply (simp_all add: matrix_add_commute)

    54       apply (simp_all add: matrix_mult_assoc)

    55       by (simp_all add: matrix_left_distrib matrix_right_distrib)

    56   }

    57   note mult_assoc = this

    58   note combine_matrix_commute2 = combine_matrix_commute[simplified commutative_def, THEN spec, THEN spec]

    59   {

    60     fix A::"('a::matrix_element) matrix"

    61     fix B

    62     have "A + B = B + A"

    63       apply (simp add: plus_matrix_def)

    64       apply (insert combine_matrix_commute2[of "op +"])

    65       apply (rule combine_matrix_commute2)

    66       by (simp add: matrix_add_commute)

    67   }

    68   note plus_commute = this

    69   have plus_zero: "(0::('a::matrix_element) matrix) + 0 = 0"

    70     apply (simp add: plus_matrix_def)

    71     apply (rule combine_matrix_zero)

    72     by (simp)

    73   have mult_left_zero: "!! A. (0::('a::matrix_element) matrix) * A = 0" by(simp add: times_matrix_def)

    74   have mult_right_zero: "!! A. A * (0::('a::matrix_element) matrix) = 0" by (simp add: times_matrix_def)

    75   note l_distributive_matrix2 = l_distributive_matrix[simplified l_distributive_def matrix_left_distrib, THEN spec, THEN spec, THEN spec]

    76   {

    77     fix A::"('a::matrix_element) matrix"

    78     fix B

    79     fix C

    80     have "(A + B) * C = A * C + B * C"

    81       apply (simp add: plus_matrix_def)

    82       apply (simp add: times_matrix_def)

    83       apply (rule l_distributive_matrix2)

    84       apply (simp_all add: associative_def commutative_def l_distributive_def)

    85       apply (auto)

    86       apply (simp_all add: matrix_add_assoc)

    87       apply (simp_all add: matrix_add_commute)

    88       by (simp_all add: matrix_left_distrib)

    89   }

    90   note left_distrib = this

    91   note r_distributive_matrix2 = r_distributive_matrix[simplified r_distributive_def matrix_right_distrib, THEN spec, THEN spec, THEN spec]

    92   {

    93     fix A::"('a::matrix_element) matrix"

    94     fix B

    95     fix C

    96     have "C * (A + B) = C * A + C * B"

    97       apply (simp add: plus_matrix_def)

    98       apply (simp add: times_matrix_def)

    99       apply (rule r_distributive_matrix2)

   100       apply (simp_all add: associative_def commutative_def r_distributive_def)

   101       apply (auto)

   102       apply (simp_all add: matrix_add_assoc)

   103       apply (simp_all add: matrix_add_commute)

   104       by (simp_all add: matrix_right_distrib)

   105   }

   106   note right_distrib = this

   107   show "OFCLASS('a matrix, matrix_element_class)"

   108     apply (intro_classes)

   109     apply (simp_all add: plus_assoc)

   110     apply (simp_all add: plus_commute)

   111     apply (simp_all add: plus_zero)

   112     apply (simp_all add: mult_assoc)

   113     apply (simp_all add: mult_left_zero mult_right_zero)

   114     by (simp_all add: left_distrib right_distrib)

   115 qed

   117 axclass g_almost_semiring < almost_matrix_element

   118 g_add_left_0[simp]: "0 + a = a"

   120 lemma g_add_right_0[simp]: "(a::'a::g_almost_semiring) + 0 = a"

   121 by (simp add: matrix_add_commute)

   123 axclass g_semiring < g_almost_semiring

   124 g_add_leftimp_eq: "a+b = a+c \<Longrightarrow> b = c"

   126 instance g_almost_semiring < matrix_element

   127   by intro_classes simp

   129 instance matrix :: (g_almost_semiring) g_almost_semiring

   130 apply (intro_classes)

   131 by (simp add: plus_matrix_def combine_matrix_def combine_infmatrix_def)

   133 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"

   134 by (simp add: RepAbs_matrix)

   136 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"

   137 by (simp add: RepAbs_matrix)

   139 instance matrix :: (g_semiring) g_semiring

   140 apply (intro_classes)

   141 apply (simp add: plus_matrix_def combine_matrix_def combine_infmatrix_def)

   142 apply (subst Rep_matrix_inject[THEN sym])

   143 apply (drule ssubst[OF Rep_matrix_inject, of "% x. x"])

   144 apply (drule RepAbs_matrix_eq_left)

   145 apply (auto)

   146 apply (rule_tac x="max (nrows a) (nrows b)" in exI, simp add: nrows_le)

   147 apply (rule_tac x="max (ncols a) (ncols b)" in exI, simp add: ncols_le)

   148 apply (drule RepAbs_matrix_eq_right)

   149 apply (rule_tac x="max (nrows a) (nrows c)" in exI, simp add: nrows_le)

   150 apply (rule_tac x="max (ncols a) (ncols c)" in exI, simp add: ncols_le)

   151 apply (rule ext)+

   152 apply (drule_tac x="x" and y="x" in comb, simp)

   153 apply (drule_tac x="xa" and y="xa" in comb, simp)

   154 apply (drule g_add_leftimp_eq)

   155 by simp

   157 axclass pordered_matrix_element < matrix_element, order, zero

   158 pordered_add_right_mono: "a <= b \<Longrightarrow> a + c <= b + c"

   159 pordered_mult_left: "0 <= c \<Longrightarrow> a <= b \<Longrightarrow> c*a <= c*b"

   160 pordered_mult_right: "0 <= c \<Longrightarrow> a <= b \<Longrightarrow> a*c <= b*c"

   162 lemma pordered_add_left_mono: "(a::'a::pordered_matrix_element) <= b \<Longrightarrow> c + a <= c + b"

   163 apply (insert pordered_add_right_mono[of a b c])

   164 by (simp add: matrix_add_commute)

   166 lemma pordered_add: "(a::'a::pordered_matrix_element) <= b \<Longrightarrow> (c::'a::pordered_matrix_element) <= d \<Longrightarrow> a+c <= b+d"

   167 proof -

   168   assume p1:"a <= b"

   169   assume p2:"c <= d"

   170   have "a+c <= b+c" by (rule pordered_add_right_mono)

   171   also have "\<dots> <= b+d" by (rule pordered_add_left_mono)

   172   ultimately show "a+c <= b+d" by simp

   173 qed

   175 instance matrix :: (pordered_matrix_element) pordered_matrix_element

   176 apply (intro_classes)

   177 apply (simp_all add: plus_matrix_def times_matrix_def)

   178 apply (rule le_combine_matrix)

   179 apply (simp_all)

   180 apply (simp_all add: pordered_add)

   181 apply (rule le_left_mult)

   182 apply (simp_all add: matrix_add_0 g_add_left_0 pordered_add pordered_mult_left matrix_mult_left_0 matrix_mult_right_0)

   183 apply (rule le_right_mult)

   184 by (simp_all add: pordered_add pordered_mult_right)

   186 axclass pordered_g_semiring < g_semiring, pordered_matrix_element

   188 instance matrix :: (pordered_g_semiring) pordered_g_semiring ..

   190 lemma nrows_mult: "nrows ((A::('a::matrix_element) matrix) * B) <= nrows A"

   191 by (simp add: times_matrix_def mult_nrows)

   193 lemma ncols_mult: "ncols ((A::('a::matrix_element) matrix) * B) <= ncols B"

   194 by (simp add: times_matrix_def mult_ncols)

   196 (*

   197 constdefs

   198   one_matrix :: "nat \<Rightarrow> ('a::comm_semiring_1_cancel) matrix"

   199   "one_matrix n == Abs_matrix (% j i. if j = i & j < n then 1 else 0)"

   201 lemma Rep_one_matrix[simp]: "Rep_matrix (one_matrix n) j i = (if (j = i & j < n) then 1 else 0)"

   202 apply (simp add: one_matrix_def)

   203 apply (subst RepAbs_matrix)

   204 apply (rule exI[of _ n], simp add: split_if)+

   205 by (simp add: split_if, arith)

   207 lemma nrows_one_matrix[simp]: "nrows (one_matrix n) = n" (is "?r = _")

   208 proof -

   209   have "?r <= n" by (simp add: nrows_le)

   210   moreover have "n <= ?r" by (simp add: le_nrows, arith)

   211   ultimately show "?r = n" by simp

   212 qed

   214 lemma ncols_one_matrix[simp]: "ncols (one_matrix n) = n" (is "?r = _")

   215 proof -

   216   have "?r <= n" by (simp add: ncols_le)

   217   moreover have "n <= ?r" by (simp add: le_ncols, arith)

   218   ultimately show "?r = n" by simp

   219 qed

   221 lemma one_matrix_mult_right: "ncols A <= n \<Longrightarrow> A * (one_matrix n) = A"

   222 apply (subst Rep_matrix_inject[THEN sym])

   223 apply (rule ext)+

   224 apply (simp add: times_matrix_def Rep_mult_matrix)

   225 apply (rule_tac j1="xa" in ssubst[OF foldseq_almostzero])

   226 apply (simp_all)

   227 by (simp add: max_def ncols)

   229 lemma one_matrix_mult_left: "nrows A <= n \<Longrightarrow> (one_matrix n) * A = A"

   230 apply (subst Rep_matrix_inject[THEN sym])

   231 apply (rule ext)+

   232 apply (simp add: times_matrix_def Rep_mult_matrix)

   233 apply (rule_tac j1="x" in ssubst[OF foldseq_almostzero])

   234 apply (simp_all)

   235 by (simp add: max_def nrows)

   237 constdefs

   238   right_inverse_matrix :: "('a::comm_semiring_1_cancel) matrix \<Rightarrow> 'a matrix \<Rightarrow> bool"

   239   "right_inverse_matrix A X == (A * X = one_matrix (max (nrows A) (ncols X)))"

   240   inverse_matrix :: "('a::comm_semiring_1_cancel) matrix \<Rightarrow> 'a matrix \<Rightarrow> bool"

   241   "inverse_matrix A X == (right_inverse_matrix A X) \<and> (right_inverse_matrix X A)"

   243 lemma right_inverse_matrix_dim: "right_inverse_matrix A X \<Longrightarrow> nrows A = ncols X"

   244 apply (insert ncols_mult[of A X], insert nrows_mult[of A X])

   245 by (simp add: right_inverse_matrix_def)

   247 text {* to be continued \dots *}

   248 *)

   249 end

author	obua
	Tue, 11 May 2004 20:11:08 +0200
changeset 14738	83f1a514dcb4
parent 14724	021264410f87
child 14940	b9ab8babd8b3
permissions	-rw-r--r--