src/HOL/Analysis/Cartesian_Space.thy
author nipkow
Sat Dec 29 15:43:53 2018 +0100 (6 months ago)
changeset 69529 4ab9657b3257
parent 69064 5840724b1d71
child 69665 60110f6d0b4e
child 69677 a06b204527e6
permissions -rw-r--r--
capitalize proper names in lemma names
wenzelm@68189
     1
(*  Title:      HOL/Analysis/Cartesian_Space.thy
wenzelm@68189
     2
    Author:     Amine Chaieb, University of Cambridge
wenzelm@68189
     3
    Author:     Jose Divasón <jose.divasonm at unirioja.es>
wenzelm@68189
     4
    Author:     Jesús Aransay <jesus-maria.aransay at unirioja.es>
wenzelm@68189
     5
    Author:     Johannes Hölzl, VU Amsterdam
wenzelm@68189
     6
    Author:     Fabian Immler, TUM
immler@68072
     7
*)
wenzelm@68189
     8
immler@68072
     9
theory Cartesian_Space
immler@68072
    10
  imports
immler@68072
    11
    Finite_Cartesian_Product Linear_Algebra
immler@68072
    12
begin
immler@68072
    13
ak2110@68833
    14
definition%unimportant "cart_basis = {axis i 1 | i. i\<in>UNIV}"
immler@68072
    15
ak2110@68833
    16
lemma%unimportant finite_cart_basis: "finite (cart_basis)" unfolding cart_basis_def
immler@68072
    17
  using finite_Atleast_Atmost_nat by fastforce
immler@68072
    18
ak2110@68833
    19
lemma%unimportant card_cart_basis: "card (cart_basis::('a::zero_neq_one^'i) set) = CARD('i)"
immler@68072
    20
  unfolding cart_basis_def Setcompr_eq_image
immler@68072
    21
  by (rule card_image) (auto simp: inj_on_def axis_eq_axis)
immler@68072
    22
nipkow@69064
    23
interpretation vec: vector_space "(*s) "
immler@68072
    24
  by unfold_locales (vector algebra_simps)+
immler@68072
    25
ak2110@68833
    26
lemma%unimportant independent_cart_basis:
immler@68072
    27
  "vec.independent (cart_basis)"
immler@68072
    28
proof (rule vec.independent_if_scalars_zero)
immler@68072
    29
  show "finite (cart_basis)" using finite_cart_basis .
immler@68072
    30
  fix f::"('a, 'b) vec \<Rightarrow> 'a" and x::"('a, 'b) vec"
immler@68072
    31
  assume eq_0: "(\<Sum>x\<in>cart_basis. f x *s x) = 0" and x_in: "x \<in> cart_basis"
immler@68072
    32
  obtain i where x: "x = axis i 1" using x_in unfolding cart_basis_def by auto
immler@68072
    33
  have sum_eq_0: "(\<Sum>x\<in>(cart_basis) - {x}. f x * (x $ i)) = 0"
immler@68072
    34
  proof (rule sum.neutral, rule ballI)
immler@68072
    35
    fix xa assume xa: "xa \<in> cart_basis - {x}"
immler@68072
    36
    obtain a where a: "xa = axis a 1" and a_not_i: "a \<noteq> i"
immler@68072
    37
      using xa x unfolding cart_basis_def by auto
immler@68072
    38
    have "xa $ i = 0" unfolding a axis_def using a_not_i by auto
immler@68072
    39
    thus "f xa * xa $ i = 0" by simp
immler@68072
    40
  qed
immler@68072
    41
  have "0 = (\<Sum>x\<in>cart_basis. f x *s x) $ i" using eq_0 by simp
immler@68072
    42
  also have "... = (\<Sum>x\<in>cart_basis. (f x *s x) $ i)" unfolding sum_component ..
immler@68072
    43
  also have "... = (\<Sum>x\<in>cart_basis. f x * (x $ i))" unfolding vector_smult_component ..
immler@68072
    44
  also have "... = f x * (x $ i) + (\<Sum>x\<in>(cart_basis) - {x}. f x * (x $ i))"
immler@68072
    45
    by (rule sum.remove[OF finite_cart_basis x_in])
immler@68072
    46
  also have "... =  f x * (x $ i)" unfolding sum_eq_0 by simp
immler@68072
    47
  also have "... = f x" unfolding x axis_def by auto
immler@68072
    48
  finally show "f x = 0" ..
immler@68072
    49
qed
immler@68072
    50
ak2110@68833
    51
lemma%unimportant span_cart_basis:
immler@68072
    52
  "vec.span (cart_basis) = UNIV"
immler@68072
    53
proof (auto)
immler@68072
    54
  fix x::"('a, 'b) vec"
immler@68072
    55
  let ?f="\<lambda>v. x $ (THE i. v = axis i 1)"
immler@68072
    56
  show "x \<in> vec.span (cart_basis)"
immler@68072
    57
    apply (unfold vec.span_finite[OF finite_cart_basis])
immler@68072
    58
    apply (rule image_eqI[of _ _ ?f])
immler@68072
    59
     apply (subst  vec_eq_iff)
immler@68072
    60
     apply clarify
immler@68072
    61
  proof -
immler@68072
    62
    fix i::'b
immler@68072
    63
    let ?w = "axis i (1::'a)"
immler@68072
    64
    have the_eq_i: "(THE a. ?w = axis a 1) = i"
immler@68072
    65
      by (rule the_equality, auto simp: axis_eq_axis)
immler@68072
    66
    have sum_eq_0: "(\<Sum>v\<in>(cart_basis) - {?w}. x $ (THE i. v = axis i 1) * v $ i) = 0"
immler@68072
    67
    proof (rule sum.neutral, rule ballI)
immler@68072
    68
      fix xa::"('a, 'b) vec"
immler@68072
    69
      assume xa: "xa \<in> cart_basis - {?w}"
immler@68072
    70
      obtain j where j: "xa = axis j 1" and i_not_j: "i \<noteq> j" using xa unfolding cart_basis_def by auto
immler@68072
    71
      have the_eq_j: "(THE i. xa = axis i 1) = j"
immler@68072
    72
      proof (rule the_equality)
immler@68072
    73
        show "xa = axis j 1" using j .
immler@68072
    74
        show "\<And>i. xa = axis i 1 \<Longrightarrow> i = j" by (metis axis_eq_axis j zero_neq_one)
immler@68072
    75
      qed
immler@68072
    76
      show "x $ (THE i. xa = axis i 1) * xa $ i = 0"
immler@68072
    77
        apply (subst (2) j)
immler@68072
    78
        unfolding the_eq_j unfolding axis_def using i_not_j by simp
immler@68072
    79
    qed
immler@68072
    80
    have "(\<Sum>v\<in>cart_basis. x $ (THE i. v = axis i 1) *s v) $ i =
immler@68072
    81
  (\<Sum>v\<in>cart_basis. (x $ (THE i. v = axis i 1) *s v) $ i)" unfolding sum_component ..
immler@68072
    82
    also have "... = (\<Sum>v\<in>cart_basis. x $ (THE i. v = axis i 1) * v $ i)"
immler@68072
    83
      unfolding vector_smult_component ..
immler@68072
    84
    also have "... = x $ (THE a. ?w = axis a 1) * ?w $ i + (\<Sum>v\<in>(cart_basis) - {?w}. x $ (THE i. v = axis i 1) * v $ i)"
immler@68072
    85
      by (rule sum.remove[OF finite_cart_basis], auto simp add: cart_basis_def)
immler@68072
    86
    also have "... = x $ (THE a. ?w = axis a 1) * ?w $ i" unfolding sum_eq_0 by simp
immler@68072
    87
    also have "... = x $ i" unfolding the_eq_i unfolding axis_def by auto
immler@68072
    88
    finally show "x $ i = (\<Sum>v\<in>cart_basis. x $ (THE i. v = axis i 1) *s v) $ i" by simp
immler@68072
    89
  qed simp
immler@68072
    90
qed
immler@68072
    91
immler@68072
    92
(*Some interpretations:*)
nipkow@69064
    93
interpretation vec: finite_dimensional_vector_space "(*s)" "cart_basis"
immler@68072
    94
  by (unfold_locales, auto simp add: finite_cart_basis independent_cart_basis span_cart_basis)
immler@68072
    95
ak2110@68833
    96
lemma%unimportant matrix_vector_mul_linear_gen[intro, simp]:
nipkow@69064
    97
  "Vector_Spaces.linear (*s) (*s) ((*v) A)"
immler@68072
    98
  by unfold_locales
immler@68072
    99
    (vector matrix_vector_mult_def sum.distrib algebra_simps)+
immler@68072
   100
ak2110@68833
   101
lemma%important span_vec_eq: "vec.span X = span X"
immler@68074
   102
  and dim_vec_eq: "vec.dim X = dim X"
immler@68074
   103
  and dependent_vec_eq: "vec.dependent X = dependent X"
immler@68074
   104
  and subspace_vec_eq: "vec.subspace X = subspace X"
immler@68074
   105
  for X::"(real^'n) set"
immler@68074
   106
  unfolding span_raw_def dim_raw_def dependent_raw_def subspace_raw_def
immler@68074
   107
  by (auto simp: scalar_mult_eq_scaleR)
immler@68074
   108
ak2110@68833
   109
lemma%important linear_componentwise:
immler@68072
   110
  fixes f:: "'a::field ^'m \<Rightarrow> 'a ^ 'n"
nipkow@69064
   111
  assumes lf: "Vector_Spaces.linear (*s) (*s) f"
immler@68072
   112
  shows "(f x)$j = sum (\<lambda>i. (x$i) * (f (axis i 1)$j)) (UNIV :: 'm set)" (is "?lhs = ?rhs")
ak2110@68833
   113
proof%unimportant -
nipkow@69064
   114
  interpret lf: Vector_Spaces.linear "(*s)" "(*s)" f
immler@68072
   115
    using lf .
immler@68072
   116
  let ?M = "(UNIV :: 'm set)"
immler@68072
   117
  let ?N = "(UNIV :: 'n set)"
immler@68072
   118
  have fM: "finite ?M" by simp
immler@68072
   119
  have "?rhs = (sum (\<lambda>i. (x$i) *s (f (axis i 1))) ?M)$j"
immler@68072
   120
    unfolding sum_component by simp
immler@68072
   121
  then show ?thesis
immler@68072
   122
    unfolding lf.sum[symmetric] lf.scale[symmetric]
immler@68072
   123
    unfolding basis_expansion by auto
immler@68072
   124
qed
immler@68072
   125
nipkow@69064
   126
interpretation vec: Vector_Spaces.linear "(*s)" "(*s)" "(*v) A"
immler@68072
   127
  using matrix_vector_mul_linear_gen.
immler@68072
   128
nipkow@69064
   129
interpretation vec: finite_dimensional_vector_space_pair "(*s)" cart_basis "(*s)" cart_basis ..
immler@68072
   130
ak2110@68833
   131
lemma%unimportant matrix_works:
nipkow@69064
   132
  assumes lf: "Vector_Spaces.linear (*s) (*s) f"
immler@68072
   133
  shows "matrix f *v x = f (x::'a::field ^ 'n)"
immler@68072
   134
  apply (simp add: matrix_def matrix_vector_mult_def vec_eq_iff mult.commute)
immler@68072
   135
  apply clarify
immler@68072
   136
  apply (rule linear_componentwise[OF lf, symmetric])
immler@68072
   137
  done
immler@68072
   138
ak2110@68833
   139
lemma%unimportant matrix_of_matrix_vector_mul[simp]: "matrix(\<lambda>x. A *v (x :: 'a::field ^ 'n)) = A"
immler@68072
   140
  by (simp add: matrix_eq matrix_works)
immler@68072
   141
ak2110@68833
   142
lemma%unimportant matrix_compose_gen:
nipkow@69064
   143
  assumes lf: "Vector_Spaces.linear (*s) (*s) (f::'a::{field}^'n \<Rightarrow> 'a^'m)"
nipkow@69064
   144
    and lg: "Vector_Spaces.linear (*s) (*s) (g::'a^'m \<Rightarrow> 'a^_)"
immler@68072
   145
  shows "matrix (g o f) = matrix g ** matrix f"
immler@68072
   146
  using lf lg Vector_Spaces.linear_compose[OF lf lg] matrix_works[OF Vector_Spaces.linear_compose[OF lf lg]]
immler@68072
   147
  by (simp add: matrix_eq matrix_works matrix_vector_mul_assoc[symmetric] o_def)
immler@68072
   148
ak2110@68833
   149
lemma%unimportant matrix_compose:
immler@68072
   150
  assumes "linear (f::real^'n \<Rightarrow> real^'m)" "linear (g::real^'m \<Rightarrow> real^_)"
immler@68072
   151
  shows "matrix (g o f) = matrix g ** matrix f"
immler@68072
   152
  using matrix_compose_gen[of f g] assms
immler@68072
   153
  by (simp add: linear_def scalar_mult_eq_scaleR)
immler@68072
   154
ak2110@68833
   155
lemma%unimportant left_invertible_transpose:
immler@68074
   156
  "(\<exists>(B). B ** transpose (A) = mat (1::'a::comm_semiring_1)) \<longleftrightarrow> (\<exists>(B). A ** B = mat 1)"
immler@68074
   157
  by (metis matrix_transpose_mul transpose_mat transpose_transpose)
immler@68074
   158
ak2110@68833
   159
lemma%unimportant right_invertible_transpose:
immler@68074
   160
  "(\<exists>(B). transpose (A) ** B = mat (1::'a::comm_semiring_1)) \<longleftrightarrow> (\<exists>(B). B ** A = mat 1)"
immler@68074
   161
  by (metis matrix_transpose_mul transpose_mat transpose_transpose)
immler@68074
   162
ak2110@68833
   163
lemma%unimportant linear_matrix_vector_mul_eq:
nipkow@69064
   164
  "Vector_Spaces.linear (*s) (*s) f \<longleftrightarrow> linear (f :: real^'n \<Rightarrow> real ^'m)"
immler@68074
   165
  by (simp add: scalar_mult_eq_scaleR linear_def)
immler@68074
   166
ak2110@68833
   167
lemma%unimportant matrix_vector_mul[simp]:
nipkow@69064
   168
  "Vector_Spaces.linear (*s) (*s) g \<Longrightarrow> (\<lambda>y. matrix g *v y) = g"
immler@68074
   169
  "linear f \<Longrightarrow> (\<lambda>x. matrix f *v x) = f"
immler@68074
   170
  "bounded_linear f \<Longrightarrow> (\<lambda>x. matrix f *v x) = f"
immler@68074
   171
  for f :: "real^'n \<Rightarrow> real ^'m"
immler@68074
   172
  by (simp_all add: ext matrix_works linear_matrix_vector_mul_eq linear_linear)
immler@68074
   173
ak2110@68833
   174
lemma%important matrix_left_invertible_injective:
immler@68074
   175
  fixes A :: "'a::field^'n^'m"
nipkow@69064
   176
  shows "(\<exists>B. B ** A = mat 1) \<longleftrightarrow> inj ((*v) A)"
ak2110@68833
   177
proof%unimportant safe
immler@68074
   178
  fix B
immler@68074
   179
  assume B: "B ** A = mat 1"
nipkow@69064
   180
  show "inj ((*v) A)"
immler@68074
   181
    unfolding inj_on_def
immler@68074
   182
      by (metis B matrix_vector_mul_assoc matrix_vector_mul_lid)
immler@68074
   183
next
nipkow@69064
   184
  assume "inj ((*v) A)"
immler@68074
   185
  from vec.linear_injective_left_inverse[OF matrix_vector_mul_linear_gen this]
nipkow@69064
   186
  obtain g where "Vector_Spaces.linear (*s) (*s) g" and g: "g \<circ> (*v) A = id"
immler@68074
   187
    by blast
immler@68074
   188
  have "matrix g ** A = mat 1"
nipkow@69064
   189
    by (metis matrix_vector_mul_linear_gen \<open>Vector_Spaces.linear (*s) (*s) g\<close> g matrix_compose_gen
immler@68074
   190
        matrix_eq matrix_id_mat_1 matrix_vector_mul(1))
immler@68074
   191
  then show "\<exists>B. B ** A = mat 1"
immler@68074
   192
    by metis
immler@68072
   193
qed
immler@68072
   194
ak2110@68833
   195
lemma%unimportant matrix_left_invertible_ker:
immler@68072
   196
  "(\<exists>B. (B::'a::{field} ^'m^'n) ** (A::'a::{field}^'n^'m) = mat 1) \<longleftrightarrow> (\<forall>x. A *v x = 0 \<longrightarrow> x = 0)"
immler@68072
   197
  unfolding matrix_left_invertible_injective
immler@68072
   198
  using vec.inj_on_iff_eq_0[OF vec.subspace_UNIV, of A]
immler@68072
   199
  by (simp add: inj_on_def)
immler@68072
   200
ak2110@68833
   201
lemma%important matrix_right_invertible_surjective:
immler@68074
   202
  "(\<exists>B. (A::'a::field^'n^'m) ** (B::'a::field^'m^'n) = mat 1) \<longleftrightarrow> surj (\<lambda>x. A *v x)"
ak2110@68833
   203
proof%unimportant -
immler@68074
   204
  { fix B :: "'a ^'m^'n"
immler@68074
   205
    assume AB: "A ** B = mat 1"
immler@68074
   206
    { fix x :: "'a ^ 'm"
immler@68074
   207
      have "A *v (B *v x) = x"
immler@68074
   208
        by (simp add: matrix_vector_mul_assoc AB) }
nipkow@69064
   209
    hence "surj ((*v) A)" unfolding surj_def by metis }
immler@68074
   210
  moreover
nipkow@69064
   211
  { assume sf: "surj ((*v) A)"
immler@68074
   212
    from vec.linear_surjective_right_inverse[OF _ this]
nipkow@69064
   213
    obtain g:: "'a ^'m \<Rightarrow> 'a ^'n" where g: "Vector_Spaces.linear (*s) (*s) g" "(*v) A \<circ> g = id"
immler@68074
   214
      by blast
immler@68074
   215
immler@68074
   216
    have "A ** (matrix g) = mat 1"
immler@68074
   217
      unfolding matrix_eq  matrix_vector_mul_lid
immler@68074
   218
        matrix_vector_mul_assoc[symmetric] matrix_works[OF g(1)]
immler@68074
   219
      using g(2) unfolding o_def fun_eq_iff id_def
immler@68074
   220
      .
immler@68074
   221
    hence "\<exists>B. A ** (B::'a^'m^'n) = mat 1" by blast
immler@68074
   222
  }
immler@68074
   223
  ultimately show ?thesis unfolding surj_def by blast
immler@68074
   224
qed
immler@68074
   225
ak2110@68833
   226
lemma%important matrix_left_invertible_independent_columns:
immler@68072
   227
  fixes A :: "'a::{field}^'n^'m"
immler@68072
   228
  shows "(\<exists>(B::'a ^'m^'n). B ** A = mat 1) \<longleftrightarrow>
immler@68072
   229
      (\<forall>c. sum (\<lambda>i. c i *s column i A) (UNIV :: 'n set) = 0 \<longrightarrow> (\<forall>i. c i = 0))"
immler@68072
   230
    (is "?lhs \<longleftrightarrow> ?rhs")
ak2110@68833
   231
proof%unimportant -
immler@68072
   232
  let ?U = "UNIV :: 'n set"
immler@68072
   233
  { assume k: "\<forall>x. A *v x = 0 \<longrightarrow> x = 0"
immler@68072
   234
    { fix c i
immler@68072
   235
      assume c: "sum (\<lambda>i. c i *s column i A) ?U = 0" and i: "i \<in> ?U"
immler@68072
   236
      let ?x = "\<chi> i. c i"
immler@68072
   237
      have th0:"A *v ?x = 0"
immler@68072
   238
        using c
immler@68072
   239
        by (vector matrix_mult_sum)
immler@68072
   240
      from k[rule_format, OF th0] i
immler@68072
   241
      have "c i = 0" by (vector vec_eq_iff)}
immler@68072
   242
    hence ?rhs by blast }
immler@68072
   243
  moreover
immler@68072
   244
  { assume H: ?rhs
immler@68072
   245
    { fix x assume x: "A *v x = 0"
immler@68072
   246
      let ?c = "\<lambda>i. ((x$i ):: 'a)"
immler@68072
   247
      from H[rule_format, of ?c, unfolded matrix_mult_sum[symmetric], OF x]
immler@68072
   248
      have "x = 0" by vector }
immler@68072
   249
  }
immler@68072
   250
  ultimately show ?thesis unfolding matrix_left_invertible_ker by auto
immler@68072
   251
qed
immler@68072
   252
ak2110@68833
   253
lemma%unimportant matrix_right_invertible_independent_rows:
immler@68072
   254
  fixes A :: "'a::{field}^'n^'m"
immler@68072
   255
  shows "(\<exists>(B::'a^'m^'n). A ** B = mat 1) \<longleftrightarrow>
immler@68072
   256
    (\<forall>c. sum (\<lambda>i. c i *s row i A) (UNIV :: 'm set) = 0 \<longrightarrow> (\<forall>i. c i = 0))"
immler@68072
   257
  unfolding left_invertible_transpose[symmetric]
immler@68072
   258
    matrix_left_invertible_independent_columns
immler@68072
   259
  by (simp add:)
immler@68072
   260
ak2110@68833
   261
lemma%important matrix_right_invertible_span_columns:
immler@68074
   262
  "(\<exists>(B::'a::field ^'n^'m). (A::'a ^'m^'n) ** B = mat 1) \<longleftrightarrow>
immler@68074
   263
    vec.span (columns A) = UNIV" (is "?lhs = ?rhs")
ak2110@68833
   264
proof%unimportant -
immler@68074
   265
  let ?U = "UNIV :: 'm set"
immler@68074
   266
  have fU: "finite ?U" by simp
immler@68074
   267
  have lhseq: "?lhs \<longleftrightarrow> (\<forall>y. \<exists>(x::'a^'m). sum (\<lambda>i. (x$i) *s column i A) ?U = y)"
immler@68074
   268
    unfolding matrix_right_invertible_surjective matrix_mult_sum surj_def
immler@68074
   269
    by (simp add: eq_commute)
immler@68074
   270
  have rhseq: "?rhs \<longleftrightarrow> (\<forall>x. x \<in> vec.span (columns A))" by blast
immler@68074
   271
  { assume h: ?lhs
immler@68074
   272
    { fix x:: "'a ^'n"
immler@68074
   273
      from h[unfolded lhseq, rule_format, of x] obtain y :: "'a ^'m"
immler@68074
   274
        where y: "sum (\<lambda>i. (y$i) *s column i A) ?U = x" by blast
immler@68074
   275
      have "x \<in> vec.span (columns A)"
immler@68074
   276
        unfolding y[symmetric] scalar_mult_eq_scaleR
immler@68074
   277
      proof (rule vec.span_sum [OF vec.span_scale])
immler@68074
   278
        show "column i A \<in> vec.span (columns A)" for i
immler@68074
   279
          using columns_def vec.span_superset by auto
immler@68074
   280
      qed
immler@68074
   281
    }
immler@68074
   282
    then have ?rhs unfolding rhseq by blast }
immler@68074
   283
  moreover
immler@68074
   284
  { assume h:?rhs
immler@68074
   285
    let ?P = "\<lambda>(y::'a ^'n). \<exists>(x::'a^'m). sum (\<lambda>i. (x$i) *s column i A) ?U = y"
immler@68074
   286
    { fix y
immler@68074
   287
      have "y \<in> vec.span (columns A)"
immler@68074
   288
        unfolding h by blast
immler@68074
   289
      then have "?P y"
immler@68074
   290
      proof (induction rule: vec.span_induct_alt)
immler@68074
   291
        case base
immler@68074
   292
        then show ?case
immler@68074
   293
          by (metis (full_types) matrix_mult_sum matrix_vector_mult_0_right)
immler@68074
   294
      next
immler@68074
   295
        case (step c y1 y2)
immler@68074
   296
        from step obtain i where i: "i \<in> ?U" "y1 = column i A"
immler@68074
   297
          unfolding columns_def by blast
immler@68074
   298
        obtain x:: "'a ^'m" where x: "sum (\<lambda>i. (x$i) *s column i A) ?U = y2"
immler@68074
   299
          using step by blast
immler@68074
   300
        let ?x = "(\<chi> j. if j = i then c + (x$i) else (x$j))::'a^'m"
immler@68074
   301
        show ?case
immler@68074
   302
        proof (rule exI[where x= "?x"], vector, auto simp add: i x[symmetric] if_distrib distrib_left if_distribR cong del: if_weak_cong)
immler@68074
   303
          fix j
immler@68074
   304
          have th: "\<forall>xa \<in> ?U. (if xa = i then (c + (x$i)) * ((column xa A)$j)
immler@68074
   305
              else (x$xa) * ((column xa A$j))) = (if xa = i then c * ((column i A)$j) else 0) + ((x$xa) * ((column xa A)$j))"
immler@68074
   306
            using i(1) by (simp add: field_simps)
immler@68074
   307
          have "sum (\<lambda>xa. if xa = i then (c + (x$i)) * ((column xa A)$j)
immler@68074
   308
              else (x$xa) * ((column xa A$j))) ?U = sum (\<lambda>xa. (if xa = i then c * ((column i A)$j) else 0) + ((x$xa) * ((column xa A)$j))) ?U"
immler@68074
   309
            by (rule sum.cong[OF refl]) (use th in blast)
immler@68074
   310
          also have "\<dots> = sum (\<lambda>xa. if xa = i then c * ((column i A)$j) else 0) ?U + sum (\<lambda>xa. ((x$xa) * ((column xa A)$j))) ?U"
immler@68074
   311
            by (simp add: sum.distrib)
immler@68074
   312
          also have "\<dots> = c * ((column i A)$j) + sum (\<lambda>xa. ((x$xa) * ((column xa A)$j))) ?U"
immler@68074
   313
            unfolding sum.delta[OF fU]
immler@68074
   314
            using i(1) by simp
immler@68074
   315
          finally show "sum (\<lambda>xa. if xa = i then (c + (x$i)) * ((column xa A)$j)
immler@68074
   316
            else (x$xa) * ((column xa A$j))) ?U = c * ((column i A)$j) + sum (\<lambda>xa. ((x$xa) * ((column xa A)$j))) ?U" .
immler@68074
   317
        qed
immler@68074
   318
      qed
immler@68074
   319
    }
immler@68074
   320
    then have ?lhs unfolding lhseq ..
immler@68074
   321
  }
immler@68074
   322
  ultimately show ?thesis by blast
immler@68074
   323
qed
immler@68074
   324
ak2110@68833
   325
lemma%unimportant matrix_left_invertible_span_rows_gen:
immler@68074
   326
  "(\<exists>(B::'a^'m^'n). B ** (A::'a::field^'n^'m) = mat 1) \<longleftrightarrow> vec.span (rows A) = UNIV"
immler@68074
   327
  unfolding right_invertible_transpose[symmetric]
immler@68074
   328
  unfolding columns_transpose[symmetric]
immler@68074
   329
  unfolding matrix_right_invertible_span_columns
immler@68074
   330
  ..
immler@68074
   331
ak2110@68833
   332
lemma%unimportant matrix_left_invertible_span_rows:
immler@68074
   333
  "(\<exists>(B::real^'m^'n). B ** (A::real^'n^'m) = mat 1) \<longleftrightarrow> span (rows A) = UNIV"
immler@68074
   334
  using matrix_left_invertible_span_rows_gen[of A] by (simp add: span_vec_eq)
immler@68074
   335
ak2110@68833
   336
lemma%important matrix_left_right_inverse:
immler@68072
   337
  fixes A A' :: "'a::{field}^'n^'n"
immler@68072
   338
  shows "A ** A' = mat 1 \<longleftrightarrow> A' ** A = mat 1"
ak2110@68833
   339
proof%unimportant -
immler@68072
   340
  { fix A A' :: "'a ^'n^'n"
immler@68072
   341
    assume AA': "A ** A' = mat 1"
nipkow@69064
   342
    have sA: "surj ((*v) A)"
immler@68073
   343
      using AA' matrix_right_invertible_surjective by auto
immler@68072
   344
    from vec.linear_surjective_isomorphism[OF matrix_vector_mul_linear_gen sA]
immler@68072
   345
    obtain f' :: "'a ^'n \<Rightarrow> 'a ^'n"
nipkow@69064
   346
      where f': "Vector_Spaces.linear (*s) (*s) f'" "\<forall>x. f' (A *v x) = x" "\<forall>x. A *v f' x = x" by blast
immler@68072
   347
    have th: "matrix f' ** A = mat 1"
immler@68072
   348
      by (simp add: matrix_eq matrix_works[OF f'(1)]
immler@68072
   349
          matrix_vector_mul_assoc[symmetric] f'(2)[rule_format])
immler@68072
   350
    hence "(matrix f' ** A) ** A' = mat 1 ** A'" by simp
immler@68072
   351
    hence "matrix f' = A'"
immler@68072
   352
      by (simp add: matrix_mul_assoc[symmetric] AA')
immler@68072
   353
    hence "matrix f' ** A = A' ** A" by simp
immler@68072
   354
    hence "A' ** A = mat 1" by (simp add: th)
immler@68072
   355
  }
immler@68072
   356
  then show ?thesis by blast
immler@68072
   357
qed
immler@68072
   358
ak2110@68833
   359
lemma%unimportant invertible_left_inverse:
immler@68072
   360
  fixes A :: "'a::{field}^'n^'n"
immler@68072
   361
  shows "invertible A \<longleftrightarrow> (\<exists>(B::'a^'n^'n). B ** A = mat 1)"
immler@68072
   362
  by (metis invertible_def matrix_left_right_inverse)
immler@68072
   363
ak2110@68833
   364
lemma%unimportant invertible_right_inverse:
immler@68072
   365
  fixes A :: "'a::{field}^'n^'n"
immler@68072
   366
  shows "invertible A \<longleftrightarrow> (\<exists>(B::'a^'n^'n). A** B = mat 1)"
immler@68072
   367
  by (metis invertible_def matrix_left_right_inverse)
immler@68072
   368
ak2110@68833
   369
lemma%important invertible_mult:
immler@68073
   370
  assumes inv_A: "invertible A"
immler@68073
   371
  and inv_B: "invertible B"
immler@68073
   372
  shows "invertible (A**B)"
ak2110@68833
   373
proof%unimportant -
immler@68073
   374
  obtain A' where AA': "A ** A' = mat 1" and A'A: "A' ** A = mat 1" 
immler@68073
   375
    using inv_A unfolding invertible_def by blast
immler@68073
   376
  obtain B' where BB': "B ** B' = mat 1" and B'B: "B' ** B = mat 1" 
immler@68073
   377
    using inv_B unfolding invertible_def by blast
immler@68073
   378
  show ?thesis
immler@68073
   379
  proof (unfold invertible_def, rule exI[of _ "B'**A'"], rule conjI)
immler@68073
   380
    have "A ** B ** (B' ** A') = A ** (B ** (B' ** A'))" 
immler@68073
   381
      using matrix_mul_assoc[of A B "(B' ** A')", symmetric] .
immler@68073
   382
    also have "... = A ** (B ** B' ** A')" unfolding matrix_mul_assoc[of B "B'" "A'"] ..
immler@68073
   383
    also have "... = A ** (mat 1 ** A')" unfolding BB' ..
immler@68073
   384
    also have "... = A ** A'" unfolding matrix_mul_lid ..
immler@68073
   385
    also have "... = mat 1" unfolding AA' ..
immler@68073
   386
    finally show "A ** B ** (B' ** A') = mat (1::'a)" .    
immler@68073
   387
    have "B' ** A' ** (A ** B) = B' ** (A' ** (A ** B))" using matrix_mul_assoc[of B' A' "(A ** B)", symmetric] .
immler@68073
   388
    also have "... =  B' ** (A' ** A ** B)" unfolding matrix_mul_assoc[of A' A B] ..
immler@68073
   389
    also have "... =  B' ** (mat 1 ** B)" unfolding A'A ..
immler@68073
   390
    also have "... = B' ** B"  unfolding matrix_mul_lid ..
immler@68073
   391
    also have "... = mat 1" unfolding B'B ..
immler@68073
   392
    finally show "B' ** A' ** (A ** B) = mat 1" .
immler@68073
   393
  qed
immler@68073
   394
qed
immler@68073
   395
ak2110@68833
   396
lemma%unimportant transpose_invertible:
immler@68073
   397
  fixes A :: "real^'n^'n"
immler@68073
   398
  assumes "invertible A"
immler@68073
   399
  shows "invertible (transpose A)"
immler@68073
   400
  by (meson assms invertible_def matrix_left_right_inverse right_invertible_transpose)
immler@68073
   401
ak2110@68833
   402
lemma%important vector_matrix_mul_assoc:
immler@68073
   403
  fixes v :: "('a::comm_semiring_1)^'n"
immler@68073
   404
  shows "(v v* M) v* N = v v* (M ** N)"
ak2110@68833
   405
proof%unimportant -
immler@68073
   406
  from matrix_vector_mul_assoc
immler@68073
   407
  have "transpose N *v (transpose M *v v) = (transpose N ** transpose M) *v v" by fast
immler@68073
   408
  thus "(v v* M) v* N = v v* (M ** N)"
immler@68073
   409
    by (simp add: matrix_transpose_mul [symmetric])
immler@68073
   410
qed
immler@68073
   411
ak2110@68833
   412
lemma%unimportant matrix_scaleR_vector_ac:
immler@68073
   413
  fixes A :: "real^('m::finite)^'n"
immler@68073
   414
  shows "A *v (k *\<^sub>R v) = k *\<^sub>R A *v v"
immler@68073
   415
  by (metis matrix_vector_mult_scaleR transpose_scalar vector_scaleR_matrix_ac vector_transpose_matrix)
immler@68073
   416
ak2110@68833
   417
lemma%unimportant scaleR_matrix_vector_assoc:
immler@68073
   418
  fixes A :: "real^('m::finite)^'n"
immler@68073
   419
  shows "k *\<^sub>R (A *v v) = k *\<^sub>R A *v v"
immler@68073
   420
  by (metis matrix_scaleR_vector_ac matrix_vector_mult_scaleR)
immler@68073
   421
immler@68072
   422
(*Finally, some interesting theorems and interpretations that don't appear in any file of the
immler@68072
   423
  library.*)
immler@68072
   424
immler@68072
   425
locale linear_first_finite_dimensional_vector_space =
immler@68072
   426
  l?: Vector_Spaces.linear scaleB scaleC f +
immler@68072
   427
  B?: finite_dimensional_vector_space scaleB BasisB
immler@68072
   428
  for scaleB :: "('a::field => 'b::ab_group_add => 'b)" (infixr "*b" 75)
immler@68072
   429
  and scaleC :: "('a => 'c::ab_group_add => 'c)" (infixr "*c" 75)
immler@68072
   430
  and BasisB :: "('b set)"
immler@68072
   431
  and f :: "('b=>'c)"
immler@68072
   432
ak2110@68833
   433
lemma%important vec_dim_card: "vec.dim (UNIV::('a::{field}^'n) set) = CARD ('n)"
ak2110@68833
   434
proof%unimportant -
immler@68072
   435
  let ?f="\<lambda>i::'n. axis i (1::'a)"
immler@68072
   436
  have "vec.dim (UNIV::('a::{field}^'n) set) = card (cart_basis::('a^'n) set)"
immler@68072
   437
    unfolding vec.dim_UNIV ..
immler@68072
   438
  also have "... = card ({i. i\<in> UNIV}::('n) set)"
immler@68072
   439
    proof (rule bij_betw_same_card[of ?f, symmetric], unfold bij_betw_def, auto)
immler@68072
   440
      show "inj (\<lambda>i::'n. axis i (1::'a))"  by (simp add: inj_on_def axis_eq_axis)
immler@68072
   441
      fix i::'n
immler@68072
   442
      show "axis i 1 \<in> cart_basis" unfolding cart_basis_def by auto
immler@68072
   443
      fix x::"'a^'n"
immler@68072
   444
      assume "x \<in> cart_basis"
immler@68072
   445
      thus "x \<in> range (\<lambda>i. axis i 1)" unfolding cart_basis_def by auto
immler@68072
   446
    qed
immler@68072
   447
  also have "... = CARD('n)" by auto
immler@68072
   448
  finally show ?thesis .
immler@68072
   449
qed
immler@68072
   450
nipkow@69064
   451
interpretation vector_space_over_itself: vector_space "(*) :: 'a::field => 'a => 'a"
immler@68072
   452
  by unfold_locales (simp_all add: algebra_simps)
immler@68072
   453
immler@68072
   454
lemmas [simp del] = vector_space_over_itself.scale_scale
immler@68072
   455
immler@68072
   456
interpretation vector_space_over_itself: finite_dimensional_vector_space
nipkow@69064
   457
  "(*) :: 'a::field => 'a => 'a" "{1}"
immler@68072
   458
  by unfold_locales (auto simp: vector_space_over_itself.span_singleton)
immler@68072
   459
immler@68072
   460
lemma dimension_eq_1[code_unfold]: "vector_space_over_itself.dimension TYPE('a::field)= 1"
immler@68072
   461
  unfolding vector_space_over_itself.dimension_def by simp
immler@68072
   462
immler@68072
   463
end