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