src/HOL/Analysis/Cartesian_Space.thy
author wenzelm
Mon Mar 25 17:21:26 2019 +0100 (2 months ago)
changeset 69981 3dced198b9ec
parent 69918 eddcc7c726f3
child 70136 f03a01a18c6e
permissions -rw-r--r--
more strict AFP properties;
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
nipkow@69665
     9
section "Linear Algebra on Finite Cartesian Products"
nipkow@69665
    10
immler@68072
    11
theory Cartesian_Space
immler@68072
    12
  imports
immler@68072
    13
    Finite_Cartesian_Product Linear_Algebra
immler@68072
    14
begin
immler@68072
    15
ak2110@69723
    16
subsection%unimportant \<open>Type @{typ \<open>'a ^ 'n\<close>} and fields as vector spaces\<close> (*much of the following
ak2110@69723
    17
is really basic linear algebra, check for overlap? rename subsection?  *)
nipkow@69667
    18
ak2110@69723
    19
definition "cart_basis = {axis i 1 | i. i\<in>UNIV}"
immler@68072
    20
ak2110@69723
    21
lemma finite_cart_basis: "finite (cart_basis)" unfolding cart_basis_def
immler@68072
    22
  using finite_Atleast_Atmost_nat by fastforce
immler@68072
    23
ak2110@69723
    24
lemma card_cart_basis: "card (cart_basis::('a::zero_neq_one^'i) set) = CARD('i)"
immler@68072
    25
  unfolding cart_basis_def Setcompr_eq_image
immler@68072
    26
  by (rule card_image) (auto simp: inj_on_def axis_eq_axis)
immler@68072
    27
ak2110@69723
    28
interpretation vec: vector_space "(*s) "
immler@68072
    29
  by unfold_locales (vector algebra_simps)+
immler@68072
    30
ak2110@69723
    31
lemma independent_cart_basis:
immler@68072
    32
  "vec.independent (cart_basis)"
immler@68072
    33
proof (rule vec.independent_if_scalars_zero)
immler@68072
    34
  show "finite (cart_basis)" using finite_cart_basis .
immler@68072
    35
  fix f::"('a, 'b) vec \<Rightarrow> 'a" and x::"('a, 'b) vec"
immler@68072
    36
  assume eq_0: "(\<Sum>x\<in>cart_basis. f x *s x) = 0" and x_in: "x \<in> cart_basis"
immler@68072
    37
  obtain i where x: "x = axis i 1" using x_in unfolding cart_basis_def by auto
immler@68072
    38
  have sum_eq_0: "(\<Sum>x\<in>(cart_basis) - {x}. f x * (x $ i)) = 0"
immler@68072
    39
  proof (rule sum.neutral, rule ballI)
immler@68072
    40
    fix xa assume xa: "xa \<in> cart_basis - {x}"
immler@68072
    41
    obtain a where a: "xa = axis a 1" and a_not_i: "a \<noteq> i"
immler@68072
    42
      using xa x unfolding cart_basis_def by auto
immler@68072
    43
    have "xa $ i = 0" unfolding a axis_def using a_not_i by auto
immler@68072
    44
    thus "f xa * xa $ i = 0" by simp
immler@68072
    45
  qed
immler@68072
    46
  have "0 = (\<Sum>x\<in>cart_basis. f x *s x) $ i" using eq_0 by simp
immler@68072
    47
  also have "... = (\<Sum>x\<in>cart_basis. (f x *s x) $ i)" unfolding sum_component ..
immler@68072
    48
  also have "... = (\<Sum>x\<in>cart_basis. f x * (x $ i))" unfolding vector_smult_component ..
immler@68072
    49
  also have "... = f x * (x $ i) + (\<Sum>x\<in>(cart_basis) - {x}. f x * (x $ i))"
immler@68072
    50
    by (rule sum.remove[OF finite_cart_basis x_in])
immler@68072
    51
  also have "... =  f x * (x $ i)" unfolding sum_eq_0 by simp
immler@68072
    52
  also have "... = f x" unfolding x axis_def by auto
immler@68072
    53
  finally show "f x = 0" ..
immler@68072
    54
qed
immler@68072
    55
ak2110@69723
    56
lemma span_cart_basis:
immler@68072
    57
  "vec.span (cart_basis) = UNIV"
immler@68072
    58
proof (auto)
immler@68072
    59
  fix x::"('a, 'b) vec"
immler@68072
    60
  let ?f="\<lambda>v. x $ (THE i. v = axis i 1)"
immler@68072
    61
  show "x \<in> vec.span (cart_basis)"
immler@68072
    62
    apply (unfold vec.span_finite[OF finite_cart_basis])
immler@68072
    63
    apply (rule image_eqI[of _ _ ?f])
immler@68072
    64
     apply (subst  vec_eq_iff)
immler@68072
    65
     apply clarify
immler@68072
    66
  proof -
immler@68072
    67
    fix i::'b
immler@68072
    68
    let ?w = "axis i (1::'a)"
immler@68072
    69
    have the_eq_i: "(THE a. ?w = axis a 1) = i"
immler@68072
    70
      by (rule the_equality, auto simp: axis_eq_axis)
immler@68072
    71
    have sum_eq_0: "(\<Sum>v\<in>(cart_basis) - {?w}. x $ (THE i. v = axis i 1) * v $ i) = 0"
immler@68072
    72
    proof (rule sum.neutral, rule ballI)
immler@68072
    73
      fix xa::"('a, 'b) vec"
immler@68072
    74
      assume xa: "xa \<in> cart_basis - {?w}"
immler@68072
    75
      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
    76
      have the_eq_j: "(THE i. xa = axis i 1) = j"
immler@68072
    77
      proof (rule the_equality)
immler@68072
    78
        show "xa = axis j 1" using j .
immler@68072
    79
        show "\<And>i. xa = axis i 1 \<Longrightarrow> i = j" by (metis axis_eq_axis j zero_neq_one)
immler@68072
    80
      qed
immler@68072
    81
      show "x $ (THE i. xa = axis i 1) * xa $ i = 0"
immler@68072
    82
        apply (subst (2) j)
immler@68072
    83
        unfolding the_eq_j unfolding axis_def using i_not_j by simp
immler@68072
    84
    qed
immler@68072
    85
    have "(\<Sum>v\<in>cart_basis. x $ (THE i. v = axis i 1) *s v) $ i =
immler@68072
    86
  (\<Sum>v\<in>cart_basis. (x $ (THE i. v = axis i 1) *s v) $ i)" unfolding sum_component ..
immler@68072
    87
    also have "... = (\<Sum>v\<in>cart_basis. x $ (THE i. v = axis i 1) * v $ i)"
immler@68072
    88
      unfolding vector_smult_component ..
immler@68072
    89
    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
    90
      by (rule sum.remove[OF finite_cart_basis], auto simp add: cart_basis_def)
immler@68072
    91
    also have "... = x $ (THE a. ?w = axis a 1) * ?w $ i" unfolding sum_eq_0 by simp
immler@68072
    92
    also have "... = x $ i" unfolding the_eq_i unfolding axis_def by auto
immler@68072
    93
    finally show "x $ i = (\<Sum>v\<in>cart_basis. x $ (THE i. v = axis i 1) *s v) $ i" by simp
immler@68072
    94
  qed simp
immler@68072
    95
qed
immler@68072
    96
immler@68072
    97
(*Some interpretations:*)
nipkow@69064
    98
interpretation vec: finite_dimensional_vector_space "(*s)" "cart_basis"
immler@68072
    99
  by (unfold_locales, auto simp add: finite_cart_basis independent_cart_basis span_cart_basis)
immler@68072
   100
ak2110@69723
   101
lemma matrix_vector_mul_linear_gen[intro, simp]:
nipkow@69064
   102
  "Vector_Spaces.linear (*s) (*s) ((*v) A)"
immler@68072
   103
  by unfold_locales
immler@68072
   104
    (vector matrix_vector_mult_def sum.distrib algebra_simps)+
immler@68072
   105
ak2110@69723
   106
lemma span_vec_eq: "vec.span X = span X"
immler@68074
   107
  and dim_vec_eq: "vec.dim X = dim X"
immler@68074
   108
  and dependent_vec_eq: "vec.dependent X = dependent X"
immler@68074
   109
  and subspace_vec_eq: "vec.subspace X = subspace X"
immler@68074
   110
  for X::"(real^'n) set"
immler@68074
   111
  unfolding span_raw_def dim_raw_def dependent_raw_def subspace_raw_def
immler@68074
   112
  by (auto simp: scalar_mult_eq_scaleR)
immler@68074
   113
ak2110@69723
   114
lemma linear_componentwise:
immler@68072
   115
  fixes f:: "'a::field ^'m \<Rightarrow> 'a ^ 'n"
nipkow@69064
   116
  assumes lf: "Vector_Spaces.linear (*s) (*s) f"
immler@68072
   117
  shows "(f x)$j = sum (\<lambda>i. (x$i) * (f (axis i 1)$j)) (UNIV :: 'm set)" (is "?lhs = ?rhs")
ak2110@69723
   118
proof -
nipkow@69064
   119
  interpret lf: Vector_Spaces.linear "(*s)" "(*s)" f
immler@68072
   120
    using lf .
immler@68072
   121
  let ?M = "(UNIV :: 'm set)"
immler@68072
   122
  let ?N = "(UNIV :: 'n set)"
immler@68072
   123
  have fM: "finite ?M" by simp
immler@68072
   124
  have "?rhs = (sum (\<lambda>i. (x$i) *s (f (axis i 1))) ?M)$j"
immler@68072
   125
    unfolding sum_component by simp
immler@68072
   126
  then show ?thesis
immler@68072
   127
    unfolding lf.sum[symmetric] lf.scale[symmetric]
immler@68072
   128
    unfolding basis_expansion by auto
immler@68072
   129
qed
immler@68072
   130
nipkow@69064
   131
interpretation vec: Vector_Spaces.linear "(*s)" "(*s)" "(*v) A"
immler@68072
   132
  using matrix_vector_mul_linear_gen.
immler@68072
   133
nipkow@69064
   134
interpretation vec: finite_dimensional_vector_space_pair "(*s)" cart_basis "(*s)" cart_basis ..
immler@68072
   135
ak2110@69723
   136
lemma matrix_works:
nipkow@69064
   137
  assumes lf: "Vector_Spaces.linear (*s) (*s) f"
immler@68072
   138
  shows "matrix f *v x = f (x::'a::field ^ 'n)"
immler@68072
   139
  apply (simp add: matrix_def matrix_vector_mult_def vec_eq_iff mult.commute)
immler@68072
   140
  apply clarify
immler@68072
   141
  apply (rule linear_componentwise[OF lf, symmetric])
immler@68072
   142
  done
immler@68072
   143
ak2110@69723
   144
lemma matrix_of_matrix_vector_mul[simp]: "matrix(\<lambda>x. A *v (x :: 'a::field ^ 'n)) = A"
immler@68072
   145
  by (simp add: matrix_eq matrix_works)
immler@68072
   146
ak2110@69723
   147
lemma matrix_compose_gen:
nipkow@69064
   148
  assumes lf: "Vector_Spaces.linear (*s) (*s) (f::'a::{field}^'n \<Rightarrow> 'a^'m)"
nipkow@69064
   149
    and lg: "Vector_Spaces.linear (*s) (*s) (g::'a^'m \<Rightarrow> 'a^_)"
immler@68072
   150
  shows "matrix (g o f) = matrix g ** matrix f"
immler@68072
   151
  using lf lg Vector_Spaces.linear_compose[OF lf lg] matrix_works[OF Vector_Spaces.linear_compose[OF lf lg]]
immler@68072
   152
  by (simp add: matrix_eq matrix_works matrix_vector_mul_assoc[symmetric] o_def)
immler@68072
   153
ak2110@69723
   154
lemma matrix_compose:
immler@68072
   155
  assumes "linear (f::real^'n \<Rightarrow> real^'m)" "linear (g::real^'m \<Rightarrow> real^_)"
immler@68072
   156
  shows "matrix (g o f) = matrix g ** matrix f"
immler@68072
   157
  using matrix_compose_gen[of f g] assms
immler@68072
   158
  by (simp add: linear_def scalar_mult_eq_scaleR)
immler@68072
   159
ak2110@69723
   160
lemma left_invertible_transpose:
immler@68074
   161
  "(\<exists>(B). B ** transpose (A) = mat (1::'a::comm_semiring_1)) \<longleftrightarrow> (\<exists>(B). A ** B = mat 1)"
immler@68074
   162
  by (metis matrix_transpose_mul transpose_mat transpose_transpose)
immler@68074
   163
ak2110@69723
   164
lemma right_invertible_transpose:
immler@68074
   165
  "(\<exists>(B). transpose (A) ** B = mat (1::'a::comm_semiring_1)) \<longleftrightarrow> (\<exists>(B). B ** A = mat 1)"
immler@68074
   166
  by (metis matrix_transpose_mul transpose_mat transpose_transpose)
immler@68074
   167
ak2110@69723
   168
lemma linear_matrix_vector_mul_eq:
nipkow@69064
   169
  "Vector_Spaces.linear (*s) (*s) f \<longleftrightarrow> linear (f :: real^'n \<Rightarrow> real ^'m)"
immler@68074
   170
  by (simp add: scalar_mult_eq_scaleR linear_def)
immler@68074
   171
ak2110@69723
   172
lemma matrix_vector_mul[simp]:
nipkow@69064
   173
  "Vector_Spaces.linear (*s) (*s) g \<Longrightarrow> (\<lambda>y. matrix g *v y) = g"
immler@68074
   174
  "linear f \<Longrightarrow> (\<lambda>x. matrix f *v x) = f"
immler@68074
   175
  "bounded_linear f \<Longrightarrow> (\<lambda>x. matrix f *v x) = f"
immler@68074
   176
  for f :: "real^'n \<Rightarrow> real ^'m"
immler@68074
   177
  by (simp_all add: ext matrix_works linear_matrix_vector_mul_eq linear_linear)
immler@68074
   178
ak2110@69723
   179
lemma matrix_left_invertible_injective:
immler@68074
   180
  fixes A :: "'a::field^'n^'m"
nipkow@69064
   181
  shows "(\<exists>B. B ** A = mat 1) \<longleftrightarrow> inj ((*v) A)"
ak2110@69723
   182
proof safe
immler@68074
   183
  fix B
immler@68074
   184
  assume B: "B ** A = mat 1"
nipkow@69064
   185
  show "inj ((*v) A)"
immler@68074
   186
    unfolding inj_on_def
immler@68074
   187
      by (metis B matrix_vector_mul_assoc matrix_vector_mul_lid)
immler@68074
   188
next
nipkow@69064
   189
  assume "inj ((*v) A)"
immler@68074
   190
  from vec.linear_injective_left_inverse[OF matrix_vector_mul_linear_gen this]
nipkow@69064
   191
  obtain g where "Vector_Spaces.linear (*s) (*s) g" and g: "g \<circ> (*v) A = id"
immler@68074
   192
    by blast
immler@68074
   193
  have "matrix g ** A = mat 1"
nipkow@69064
   194
    by (metis matrix_vector_mul_linear_gen \<open>Vector_Spaces.linear (*s) (*s) g\<close> g matrix_compose_gen
immler@68074
   195
        matrix_eq matrix_id_mat_1 matrix_vector_mul(1))
immler@68074
   196
  then show "\<exists>B. B ** A = mat 1"
immler@68074
   197
    by metis
immler@68072
   198
qed
immler@68072
   199
ak2110@69723
   200
lemma matrix_left_invertible_ker:
immler@68072
   201
  "(\<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
   202
  unfolding matrix_left_invertible_injective
immler@68072
   203
  using vec.inj_on_iff_eq_0[OF vec.subspace_UNIV, of A]
immler@68072
   204
  by (simp add: inj_on_def)
immler@68072
   205
ak2110@69723
   206
lemma matrix_right_invertible_surjective:
immler@68074
   207
  "(\<exists>B. (A::'a::field^'n^'m) ** (B::'a::field^'m^'n) = mat 1) \<longleftrightarrow> surj (\<lambda>x. A *v x)"
ak2110@69723
   208
proof -
immler@68074
   209
  { fix B :: "'a ^'m^'n"
immler@68074
   210
    assume AB: "A ** B = mat 1"
immler@68074
   211
    { fix x :: "'a ^ 'm"
immler@68074
   212
      have "A *v (B *v x) = x"
immler@68074
   213
        by (simp add: matrix_vector_mul_assoc AB) }
nipkow@69064
   214
    hence "surj ((*v) A)" unfolding surj_def by metis }
immler@68074
   215
  moreover
nipkow@69064
   216
  { assume sf: "surj ((*v) A)"
immler@68074
   217
    from vec.linear_surjective_right_inverse[OF _ this]
nipkow@69064
   218
    obtain g:: "'a ^'m \<Rightarrow> 'a ^'n" where g: "Vector_Spaces.linear (*s) (*s) g" "(*v) A \<circ> g = id"
immler@68074
   219
      by blast
immler@68074
   220
immler@68074
   221
    have "A ** (matrix g) = mat 1"
immler@68074
   222
      unfolding matrix_eq  matrix_vector_mul_lid
immler@68074
   223
        matrix_vector_mul_assoc[symmetric] matrix_works[OF g(1)]
immler@68074
   224
      using g(2) unfolding o_def fun_eq_iff id_def
immler@68074
   225
      .
immler@68074
   226
    hence "\<exists>B. A ** (B::'a^'m^'n) = mat 1" by blast
immler@68074
   227
  }
immler@68074
   228
  ultimately show ?thesis unfolding surj_def by blast
immler@68074
   229
qed
immler@68074
   230
ak2110@69723
   231
lemma matrix_left_invertible_independent_columns:
immler@68072
   232
  fixes A :: "'a::{field}^'n^'m"
immler@68072
   233
  shows "(\<exists>(B::'a ^'m^'n). B ** A = mat 1) \<longleftrightarrow>
immler@68072
   234
      (\<forall>c. sum (\<lambda>i. c i *s column i A) (UNIV :: 'n set) = 0 \<longrightarrow> (\<forall>i. c i = 0))"
immler@68072
   235
    (is "?lhs \<longleftrightarrow> ?rhs")
ak2110@69723
   236
proof -
immler@68072
   237
  let ?U = "UNIV :: 'n set"
immler@68072
   238
  { assume k: "\<forall>x. A *v x = 0 \<longrightarrow> x = 0"
immler@68072
   239
    { fix c i
immler@68072
   240
      assume c: "sum (\<lambda>i. c i *s column i A) ?U = 0" and i: "i \<in> ?U"
immler@68072
   241
      let ?x = "\<chi> i. c i"
immler@68072
   242
      have th0:"A *v ?x = 0"
immler@68072
   243
        using c
immler@68072
   244
        by (vector matrix_mult_sum)
immler@68072
   245
      from k[rule_format, OF th0] i
immler@68072
   246
      have "c i = 0" by (vector vec_eq_iff)}
immler@68072
   247
    hence ?rhs by blast }
immler@68072
   248
  moreover
immler@68072
   249
  { assume H: ?rhs
immler@68072
   250
    { fix x assume x: "A *v x = 0"
immler@68072
   251
      let ?c = "\<lambda>i. ((x$i ):: 'a)"
immler@68072
   252
      from H[rule_format, of ?c, unfolded matrix_mult_sum[symmetric], OF x]
immler@68072
   253
      have "x = 0" by vector }
immler@68072
   254
  }
immler@68072
   255
  ultimately show ?thesis unfolding matrix_left_invertible_ker by auto
immler@68072
   256
qed
immler@68072
   257
ak2110@69723
   258
lemma matrix_right_invertible_independent_rows:
immler@68072
   259
  fixes A :: "'a::{field}^'n^'m"
immler@68072
   260
  shows "(\<exists>(B::'a^'m^'n). A ** B = mat 1) \<longleftrightarrow>
immler@68072
   261
    (\<forall>c. sum (\<lambda>i. c i *s row i A) (UNIV :: 'm set) = 0 \<longrightarrow> (\<forall>i. c i = 0))"
immler@68072
   262
  unfolding left_invertible_transpose[symmetric]
immler@68072
   263
    matrix_left_invertible_independent_columns
immler@68072
   264
  by (simp add:)
immler@68072
   265
ak2110@69723
   266
lemma matrix_right_invertible_span_columns:
immler@68074
   267
  "(\<exists>(B::'a::field ^'n^'m). (A::'a ^'m^'n) ** B = mat 1) \<longleftrightarrow>
immler@68074
   268
    vec.span (columns A) = UNIV" (is "?lhs = ?rhs")
ak2110@69723
   269
proof -
immler@68074
   270
  let ?U = "UNIV :: 'm set"
immler@68074
   271
  have fU: "finite ?U" by simp
immler@68074
   272
  have lhseq: "?lhs \<longleftrightarrow> (\<forall>y. \<exists>(x::'a^'m). sum (\<lambda>i. (x$i) *s column i A) ?U = y)"
immler@68074
   273
    unfolding matrix_right_invertible_surjective matrix_mult_sum surj_def
immler@68074
   274
    by (simp add: eq_commute)
immler@68074
   275
  have rhseq: "?rhs \<longleftrightarrow> (\<forall>x. x \<in> vec.span (columns A))" by blast
immler@68074
   276
  { assume h: ?lhs
immler@68074
   277
    { fix x:: "'a ^'n"
immler@68074
   278
      from h[unfolded lhseq, rule_format, of x] obtain y :: "'a ^'m"
immler@68074
   279
        where y: "sum (\<lambda>i. (y$i) *s column i A) ?U = x" by blast
immler@68074
   280
      have "x \<in> vec.span (columns A)"
immler@68074
   281
        unfolding y[symmetric] scalar_mult_eq_scaleR
immler@68074
   282
      proof (rule vec.span_sum [OF vec.span_scale])
immler@68074
   283
        show "column i A \<in> vec.span (columns A)" for i
immler@68074
   284
          using columns_def vec.span_superset by auto
immler@68074
   285
      qed
immler@68074
   286
    }
immler@68074
   287
    then have ?rhs unfolding rhseq by blast }
immler@68074
   288
  moreover
immler@68074
   289
  { assume h:?rhs
immler@68074
   290
    let ?P = "\<lambda>(y::'a ^'n). \<exists>(x::'a^'m). sum (\<lambda>i. (x$i) *s column i A) ?U = y"
immler@68074
   291
    { fix y
immler@68074
   292
      have "y \<in> vec.span (columns A)"
immler@68074
   293
        unfolding h by blast
immler@68074
   294
      then have "?P y"
immler@68074
   295
      proof (induction rule: vec.span_induct_alt)
immler@68074
   296
        case base
immler@68074
   297
        then show ?case
immler@68074
   298
          by (metis (full_types) matrix_mult_sum matrix_vector_mult_0_right)
immler@68074
   299
      next
immler@68074
   300
        case (step c y1 y2)
immler@68074
   301
        from step obtain i where i: "i \<in> ?U" "y1 = column i A"
immler@68074
   302
          unfolding columns_def by blast
immler@68074
   303
        obtain x:: "'a ^'m" where x: "sum (\<lambda>i. (x$i) *s column i A) ?U = y2"
immler@68074
   304
          using step by blast
immler@68074
   305
        let ?x = "(\<chi> j. if j = i then c + (x$i) else (x$j))::'a^'m"
immler@68074
   306
        show ?case
immler@68074
   307
        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
   308
          fix j
immler@68074
   309
          have th: "\<forall>xa \<in> ?U. (if xa = i then (c + (x$i)) * ((column xa A)$j)
immler@68074
   310
              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
   311
            using i(1) by (simp add: field_simps)
immler@68074
   312
          have "sum (\<lambda>xa. if xa = i then (c + (x$i)) * ((column xa A)$j)
immler@68074
   313
              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
   314
            by (rule sum.cong[OF refl]) (use th in blast)
immler@68074
   315
          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
   316
            by (simp add: sum.distrib)
immler@68074
   317
          also have "\<dots> = c * ((column i A)$j) + sum (\<lambda>xa. ((x$xa) * ((column xa A)$j))) ?U"
immler@68074
   318
            unfolding sum.delta[OF fU]
immler@68074
   319
            using i(1) by simp
immler@68074
   320
          finally show "sum (\<lambda>xa. if xa = i then (c + (x$i)) * ((column xa A)$j)
immler@68074
   321
            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
   322
        qed
immler@68074
   323
      qed
immler@68074
   324
    }
immler@68074
   325
    then have ?lhs unfolding lhseq ..
immler@68074
   326
  }
immler@68074
   327
  ultimately show ?thesis by blast
immler@68074
   328
qed
immler@68074
   329
ak2110@69723
   330
lemma matrix_left_invertible_span_rows_gen:
immler@68074
   331
  "(\<exists>(B::'a^'m^'n). B ** (A::'a::field^'n^'m) = mat 1) \<longleftrightarrow> vec.span (rows A) = UNIV"
immler@68074
   332
  unfolding right_invertible_transpose[symmetric]
immler@68074
   333
  unfolding columns_transpose[symmetric]
immler@68074
   334
  unfolding matrix_right_invertible_span_columns
immler@68074
   335
  ..
immler@68074
   336
ak2110@69723
   337
lemma matrix_left_invertible_span_rows:
immler@68074
   338
  "(\<exists>(B::real^'m^'n). B ** (A::real^'n^'m) = mat 1) \<longleftrightarrow> span (rows A) = UNIV"
immler@68074
   339
  using matrix_left_invertible_span_rows_gen[of A] by (simp add: span_vec_eq)
immler@68074
   340
ak2110@69723
   341
lemma matrix_left_right_inverse:
immler@68072
   342
  fixes A A' :: "'a::{field}^'n^'n"
immler@68072
   343
  shows "A ** A' = mat 1 \<longleftrightarrow> A' ** A = mat 1"
ak2110@69723
   344
proof -
immler@68072
   345
  { fix A A' :: "'a ^'n^'n"
immler@68072
   346
    assume AA': "A ** A' = mat 1"
nipkow@69064
   347
    have sA: "surj ((*v) A)"
immler@68073
   348
      using AA' matrix_right_invertible_surjective by auto
immler@68072
   349
    from vec.linear_surjective_isomorphism[OF matrix_vector_mul_linear_gen sA]
immler@68072
   350
    obtain f' :: "'a ^'n \<Rightarrow> 'a ^'n"
nipkow@69064
   351
      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
   352
    have th: "matrix f' ** A = mat 1"
immler@68072
   353
      by (simp add: matrix_eq matrix_works[OF f'(1)]
immler@68072
   354
          matrix_vector_mul_assoc[symmetric] f'(2)[rule_format])
immler@68072
   355
    hence "(matrix f' ** A) ** A' = mat 1 ** A'" by simp
immler@68072
   356
    hence "matrix f' = A'"
immler@68072
   357
      by (simp add: matrix_mul_assoc[symmetric] AA')
immler@68072
   358
    hence "matrix f' ** A = A' ** A" by simp
immler@68072
   359
    hence "A' ** A = mat 1" by (simp add: th)
immler@68072
   360
  }
immler@68072
   361
  then show ?thesis by blast
immler@68072
   362
qed
immler@68072
   363
ak2110@69723
   364
lemma invertible_left_inverse:
immler@68072
   365
  fixes A :: "'a::{field}^'n^'n"
immler@68072
   366
  shows "invertible A \<longleftrightarrow> (\<exists>(B::'a^'n^'n). B ** A = mat 1)"
immler@68072
   367
  by (metis invertible_def matrix_left_right_inverse)
immler@68072
   368
ak2110@69723
   369
lemma invertible_right_inverse:
immler@68072
   370
  fixes A :: "'a::{field}^'n^'n"
immler@68072
   371
  shows "invertible A \<longleftrightarrow> (\<exists>(B::'a^'n^'n). A** B = mat 1)"
immler@68072
   372
  by (metis invertible_def matrix_left_right_inverse)
immler@68072
   373
ak2110@69723
   374
lemma invertible_mult:
immler@68073
   375
  assumes inv_A: "invertible A"
immler@68073
   376
  and inv_B: "invertible B"
immler@68073
   377
  shows "invertible (A**B)"
ak2110@69723
   378
proof -
immler@68073
   379
  obtain A' where AA': "A ** A' = mat 1" and A'A: "A' ** A = mat 1" 
immler@68073
   380
    using inv_A unfolding invertible_def by blast
immler@68073
   381
  obtain B' where BB': "B ** B' = mat 1" and B'B: "B' ** B = mat 1" 
immler@68073
   382
    using inv_B unfolding invertible_def by blast
immler@68073
   383
  show ?thesis
immler@68073
   384
  proof (unfold invertible_def, rule exI[of _ "B'**A'"], rule conjI)
immler@68073
   385
    have "A ** B ** (B' ** A') = A ** (B ** (B' ** A'))" 
immler@68073
   386
      using matrix_mul_assoc[of A B "(B' ** A')", symmetric] .
immler@68073
   387
    also have "... = A ** (B ** B' ** A')" unfolding matrix_mul_assoc[of B "B'" "A'"] ..
immler@68073
   388
    also have "... = A ** (mat 1 ** A')" unfolding BB' ..
immler@68073
   389
    also have "... = A ** A'" unfolding matrix_mul_lid ..
immler@68073
   390
    also have "... = mat 1" unfolding AA' ..
immler@68073
   391
    finally show "A ** B ** (B' ** A') = mat (1::'a)" .    
immler@68073
   392
    have "B' ** A' ** (A ** B) = B' ** (A' ** (A ** B))" using matrix_mul_assoc[of B' A' "(A ** B)", symmetric] .
immler@68073
   393
    also have "... =  B' ** (A' ** A ** B)" unfolding matrix_mul_assoc[of A' A B] ..
immler@68073
   394
    also have "... =  B' ** (mat 1 ** B)" unfolding A'A ..
immler@68073
   395
    also have "... = B' ** B"  unfolding matrix_mul_lid ..
immler@68073
   396
    also have "... = mat 1" unfolding B'B ..
immler@68073
   397
    finally show "B' ** A' ** (A ** B) = mat 1" .
immler@68073
   398
  qed
immler@68073
   399
qed
immler@68073
   400
ak2110@69723
   401
lemma transpose_invertible:
immler@68073
   402
  fixes A :: "real^'n^'n"
immler@68073
   403
  assumes "invertible A"
immler@68073
   404
  shows "invertible (transpose A)"
immler@68073
   405
  by (meson assms invertible_def matrix_left_right_inverse right_invertible_transpose)
immler@68073
   406
ak2110@69723
   407
lemma vector_matrix_mul_assoc:
immler@68073
   408
  fixes v :: "('a::comm_semiring_1)^'n"
immler@68073
   409
  shows "(v v* M) v* N = v v* (M ** N)"
ak2110@69723
   410
proof -
immler@68073
   411
  from matrix_vector_mul_assoc
immler@68073
   412
  have "transpose N *v (transpose M *v v) = (transpose N ** transpose M) *v v" by fast
immler@68073
   413
  thus "(v v* M) v* N = v v* (M ** N)"
immler@68073
   414
    by (simp add: matrix_transpose_mul [symmetric])
immler@68073
   415
qed
immler@68073
   416
ak2110@69723
   417
lemma matrix_scaleR_vector_ac:
immler@68073
   418
  fixes A :: "real^('m::finite)^'n"
immler@68073
   419
  shows "A *v (k *\<^sub>R v) = k *\<^sub>R A *v v"
immler@68073
   420
  by (metis matrix_vector_mult_scaleR transpose_scalar vector_scaleR_matrix_ac vector_transpose_matrix)
immler@68073
   421
ak2110@69723
   422
lemma scaleR_matrix_vector_assoc:
immler@68073
   423
  fixes A :: "real^('m::finite)^'n"
immler@68073
   424
  shows "k *\<^sub>R (A *v v) = k *\<^sub>R A *v v"
immler@68073
   425
  by (metis matrix_scaleR_vector_ac matrix_vector_mult_scaleR)
immler@68073
   426
immler@68072
   427
(*Finally, some interesting theorems and interpretations that don't appear in any file of the
immler@68072
   428
  library.*)
immler@68072
   429
immler@68072
   430
locale linear_first_finite_dimensional_vector_space =
immler@68072
   431
  l?: Vector_Spaces.linear scaleB scaleC f +
immler@68072
   432
  B?: finite_dimensional_vector_space scaleB BasisB
immler@68072
   433
  for scaleB :: "('a::field => 'b::ab_group_add => 'b)" (infixr "*b" 75)
immler@68072
   434
  and scaleC :: "('a => 'c::ab_group_add => 'c)" (infixr "*c" 75)
immler@68072
   435
  and BasisB :: "('b set)"
immler@68072
   436
  and f :: "('b=>'c)"
immler@68072
   437
ak2110@69723
   438
lemma vec_dim_card: "vec.dim (UNIV::('a::{field}^'n) set) = CARD ('n)"
ak2110@69723
   439
proof -
immler@68072
   440
  let ?f="\<lambda>i::'n. axis i (1::'a)"
immler@68072
   441
  have "vec.dim (UNIV::('a::{field}^'n) set) = card (cart_basis::('a^'n) set)"
immler@68072
   442
    unfolding vec.dim_UNIV ..
immler@68072
   443
  also have "... = card ({i. i\<in> UNIV}::('n) set)"
immler@68072
   444
    proof (rule bij_betw_same_card[of ?f, symmetric], unfold bij_betw_def, auto)
immler@68072
   445
      show "inj (\<lambda>i::'n. axis i (1::'a))"  by (simp add: inj_on_def axis_eq_axis)
immler@68072
   446
      fix i::'n
immler@68072
   447
      show "axis i 1 \<in> cart_basis" unfolding cart_basis_def by auto
immler@68072
   448
      fix x::"'a^'n"
immler@68072
   449
      assume "x \<in> cart_basis"
immler@68072
   450
      thus "x \<in> range (\<lambda>i. axis i 1)" unfolding cart_basis_def by auto
immler@68072
   451
    qed
immler@68072
   452
  also have "... = CARD('n)" by auto
immler@68072
   453
  finally show ?thesis .
immler@68072
   454
qed
immler@68072
   455
ak2110@69723
   456
interpretation vector_space_over_itself: vector_space "(*) :: 'a::field \<Rightarrow> 'a \<Rightarrow> 'a"
nipkow@69667
   457
by unfold_locales (simp_all add: algebra_simps)
immler@68072
   458
immler@68072
   459
lemmas [simp del] = vector_space_over_itself.scale_scale
immler@68072
   460
immler@68072
   461
interpretation vector_space_over_itself: finite_dimensional_vector_space
nipkow@69064
   462
  "(*) :: 'a::field => 'a => 'a" "{1}"
immler@68072
   463
  by unfold_locales (auto simp: vector_space_over_itself.span_singleton)
immler@68072
   464
immler@68072
   465
lemma dimension_eq_1[code_unfold]: "vector_space_over_itself.dimension TYPE('a::field)= 1"
immler@68072
   466
  unfolding vector_space_over_itself.dimension_def by simp
immler@68072
   467
nipkow@69666
   468
ak2110@69723
   469
lemma dim_subset_UNIV_cart_gen:
nipkow@69666
   470
  fixes S :: "('a::field^'n) set"
nipkow@69666
   471
  shows "vec.dim S \<le> CARD('n)"
nipkow@69666
   472
  by (metis vec.dim_eq_full vec.dim_subset_UNIV vec.span_UNIV vec_dim_card)
nipkow@69666
   473
ak2110@69723
   474
lemma dim_subset_UNIV_cart:
nipkow@69666
   475
  fixes S :: "(real^'n) set"
nipkow@69666
   476
  shows "dim S \<le> CARD('n)"
nipkow@69666
   477
  using dim_subset_UNIV_cart_gen[of S] by (simp add: dim_vec_eq)
nipkow@69666
   478
nipkow@69666
   479
text\<open>Two sometimes fruitful ways of looking at matrix-vector multiplication.\<close>
nipkow@69666
   480
ak2110@69723
   481
lemma matrix_mult_dot: "A *v x = (\<chi> i. inner (A$i) x)"
nipkow@69666
   482
  by (simp add: matrix_vector_mult_def inner_vec_def)
nipkow@69666
   483
ak2110@69723
   484
lemma adjoint_matrix: "adjoint(\<lambda>x. (A::real^'n^'m) *v x) = (\<lambda>x. transpose A *v x)"
nipkow@69666
   485
  apply (rule adjoint_unique)
nipkow@69666
   486
  apply (simp add: transpose_def inner_vec_def matrix_vector_mult_def
nipkow@69666
   487
    sum_distrib_right sum_distrib_left)
nipkow@69666
   488
  apply (subst sum.swap)
nipkow@69666
   489
  apply (simp add:  ac_simps)
nipkow@69666
   490
  done
nipkow@69666
   491
ak2110@69723
   492
lemma matrix_adjoint: assumes lf: "linear (f :: real^'n \<Rightarrow> real ^'m)"
nipkow@69666
   493
  shows "matrix(adjoint f) = transpose(matrix f)"
ak2110@69723
   494
proof -
nipkow@69666
   495
  have "matrix(adjoint f) = matrix(adjoint ((*v) (matrix f)))"
nipkow@69666
   496
    by (simp add: lf)
nipkow@69666
   497
  also have "\<dots> = transpose(matrix f)"
nipkow@69666
   498
    unfolding adjoint_matrix matrix_of_matrix_vector_mul
nipkow@69666
   499
    apply rule
nipkow@69666
   500
    done
nipkow@69666
   501
  finally show ?thesis .
nipkow@69666
   502
qed
nipkow@69666
   503
nipkow@69666
   504
immler@69683
   505
subsection\<open> Rank of a matrix\<close>
nipkow@69666
   506
nipkow@69666
   507
text\<open>Equivalence of row and column rank is taken from George Mackiw's paper, Mathematics Magazine 1995, p. 285.\<close>
nipkow@69666
   508
ak2110@69723
   509
lemma matrix_vector_mult_in_columnspace_gen:
nipkow@69666
   510
  fixes A :: "'a::field^'n^'m"
nipkow@69666
   511
  shows "(A *v x) \<in> vec.span(columns A)"
nipkow@69666
   512
  apply (simp add: matrix_vector_column columns_def transpose_def column_def)
nipkow@69666
   513
  apply (intro vec.span_sum vec.span_scale)
nipkow@69666
   514
  apply (force intro: vec.span_base)
nipkow@69666
   515
  done
nipkow@69666
   516
ak2110@69723
   517
lemma matrix_vector_mult_in_columnspace:
nipkow@69666
   518
  fixes A :: "real^'n^'m"
nipkow@69666
   519
  shows "(A *v x) \<in> span(columns A)"
nipkow@69666
   520
  using matrix_vector_mult_in_columnspace_gen[of A x] by (simp add: span_vec_eq)
nipkow@69666
   521
nipkow@69666
   522
lemma subspace_orthogonal_to_vector: "subspace {y. orthogonal x y}"
nipkow@69666
   523
  by (simp add: subspace_def orthogonal_clauses)
nipkow@69666
   524
ak2110@69723
   525
lemma orthogonal_nullspace_rowspace:
nipkow@69666
   526
  fixes A :: "real^'n^'m"
nipkow@69666
   527
  assumes 0: "A *v x = 0" and y: "y \<in> span(rows A)"
nipkow@69666
   528
  shows "orthogonal x y"
nipkow@69666
   529
  using y
ak2110@69723
   530
proof (induction rule: span_induct)
nipkow@69666
   531
  case base
nipkow@69666
   532
  then show ?case
nipkow@69666
   533
    by (simp add: subspace_orthogonal_to_vector)
nipkow@69666
   534
next
nipkow@69666
   535
  case (step v)
nipkow@69666
   536
  then obtain i where "v = row i A"
nipkow@69666
   537
    by (auto simp: rows_def)
nipkow@69666
   538
  with 0 show ?case
nipkow@69666
   539
    unfolding orthogonal_def inner_vec_def matrix_vector_mult_def row_def
nipkow@69666
   540
    by (simp add: mult.commute) (metis (no_types) vec_lambda_beta zero_index)
nipkow@69666
   541
qed
nipkow@69666
   542
ak2110@69723
   543
lemma nullspace_inter_rowspace:
nipkow@69666
   544
  fixes A :: "real^'n^'m"
nipkow@69666
   545
  shows "A *v x = 0 \<and> x \<in> span(rows A) \<longleftrightarrow> x = 0"
nipkow@69666
   546
  using orthogonal_nullspace_rowspace orthogonal_self span_zero matrix_vector_mult_0_right
nipkow@69666
   547
  by blast
nipkow@69666
   548
ak2110@69723
   549
lemma matrix_vector_mul_injective_on_rowspace:
nipkow@69666
   550
  fixes A :: "real^'n^'m"
nipkow@69666
   551
  shows "\<lbrakk>A *v x = A *v y; x \<in> span(rows A); y \<in> span(rows A)\<rbrakk> \<Longrightarrow> x = y"
nipkow@69666
   552
  using nullspace_inter_rowspace [of A "x-y"]
nipkow@69666
   553
  by (metis diff_eq_diff_eq diff_self matrix_vector_mult_diff_distrib span_diff)
nipkow@69666
   554
nipkow@69666
   555
definition%important rank :: "'a::field^'n^'m=>nat"
nipkow@69666
   556
  where row_rank_def_gen: "rank A \<equiv> vec.dim(rows A)"
nipkow@69666
   557
ak2110@69723
   558
lemma row_rank_def: "rank A = dim (rows A)" for A::"real^'n^'m"
ak2110@69723
   559
  by (auto simp: row_rank_def_gen dim_vec_eq)
nipkow@69666
   560
ak2110@69723
   561
lemma dim_rows_le_dim_columns:
nipkow@69666
   562
  fixes A :: "real^'n^'m"
nipkow@69666
   563
  shows "dim(rows A) \<le> dim(columns A)"
ak2110@69723
   564
proof -
nipkow@69666
   565
  have "dim (span (rows A)) \<le> dim (span (columns A))"
nipkow@69666
   566
  proof -
nipkow@69666
   567
    obtain B where "independent B" "span(rows A) \<subseteq> span B"
nipkow@69666
   568
              and B: "B \<subseteq> span(rows A)""card B = dim (span(rows A))"
nipkow@69666
   569
      using basis_exists [of "span(rows A)"] by metis
nipkow@69666
   570
    with span_subspace have eq: "span B = span(rows A)"
nipkow@69666
   571
      by auto
nipkow@69666
   572
    then have inj: "inj_on ((*v) A) (span B)"
nipkow@69666
   573
      by (simp add: inj_on_def matrix_vector_mul_injective_on_rowspace)
nipkow@69666
   574
    then have ind: "independent ((*v) A ` B)"
nipkow@69666
   575
      by (rule linear_independent_injective_image [OF Finite_Cartesian_Product.matrix_vector_mul_linear \<open>independent B\<close>])
nipkow@69666
   576
    have "dim (span (rows A)) \<le> card ((*v) A ` B)"
nipkow@69666
   577
      unfolding B(2)[symmetric]
nipkow@69666
   578
      using inj
nipkow@69666
   579
      by (auto simp: card_image inj_on_subset span_superset)
nipkow@69666
   580
    also have "\<dots> \<le> dim (span (columns A))"
nipkow@69666
   581
      using _ ind
nipkow@69666
   582
      by (rule independent_card_le_dim) (auto intro!: matrix_vector_mult_in_columnspace)
nipkow@69666
   583
    finally show ?thesis .
nipkow@69666
   584
  qed
nipkow@69666
   585
  then show ?thesis
nipkow@69666
   586
    by (simp add: dim_span)
nipkow@69666
   587
qed
nipkow@69666
   588
ak2110@69723
   589
lemma column_rank_def:
nipkow@69666
   590
  fixes A :: "real^'n^'m"
nipkow@69666
   591
  shows "rank A = dim(columns A)"
nipkow@69666
   592
  unfolding row_rank_def
nipkow@69666
   593
  by (metis columns_transpose dim_rows_le_dim_columns le_antisym rows_transpose)
nipkow@69666
   594
ak2110@69723
   595
lemma rank_transpose:
nipkow@69666
   596
  fixes A :: "real^'n^'m"
nipkow@69666
   597
  shows "rank(transpose A) = rank A"
nipkow@69666
   598
  by (metis column_rank_def row_rank_def rows_transpose)
nipkow@69666
   599
ak2110@69723
   600
lemma matrix_vector_mult_basis:
nipkow@69666
   601
  fixes A :: "real^'n^'m"
nipkow@69666
   602
  shows "A *v (axis k 1) = column k A"
nipkow@69666
   603
  by (simp add: cart_eq_inner_axis column_def matrix_mult_dot)
nipkow@69666
   604
ak2110@69723
   605
lemma columns_image_basis:
nipkow@69666
   606
  fixes A :: "real^'n^'m"
nipkow@69666
   607
  shows "columns A = (*v) A ` (range (\<lambda>i. axis i 1))"
nipkow@69666
   608
  by (force simp: columns_def matrix_vector_mult_basis [symmetric])
nipkow@69666
   609
ak2110@69723
   610
lemma rank_dim_range:
nipkow@69666
   611
  fixes A :: "real^'n^'m"
nipkow@69666
   612
  shows "rank A = dim(range (\<lambda>x. A *v x))"
nipkow@69666
   613
  unfolding column_rank_def
ak2110@69723
   614
proof (rule span_eq_dim)
nipkow@69666
   615
  have "span (columns A) \<subseteq> span (range ((*v) A))" (is "?l \<subseteq> ?r")
nipkow@69666
   616
    by (simp add: columns_image_basis image_subsetI span_mono)
nipkow@69666
   617
  then show "?l = ?r"
nipkow@69666
   618
    by (metis (no_types, lifting) image_subset_iff matrix_vector_mult_in_columnspace
nipkow@69666
   619
        span_eq span_span)
nipkow@69666
   620
qed
nipkow@69666
   621
ak2110@69723
   622
lemma rank_bound:
nipkow@69666
   623
  fixes A :: "real^'n^'m"
nipkow@69666
   624
  shows "rank A \<le> min CARD('m) (CARD('n))"
nipkow@69666
   625
  by (metis (mono_tags, lifting) dim_subset_UNIV_cart min.bounded_iff
nipkow@69666
   626
      column_rank_def row_rank_def)
nipkow@69666
   627
ak2110@69723
   628
lemma full_rank_injective:
nipkow@69666
   629
  fixes A :: "real^'n^'m"
nipkow@69666
   630
  shows "rank A = CARD('n) \<longleftrightarrow> inj ((*v) A)"
nipkow@69666
   631
  by (simp add: matrix_left_invertible_injective [symmetric] matrix_left_invertible_span_rows row_rank_def
nipkow@69666
   632
      dim_eq_full [symmetric] card_cart_basis vec.dimension_def)
nipkow@69666
   633
ak2110@69723
   634
lemma full_rank_surjective:
nipkow@69666
   635
  fixes A :: "real^'n^'m"
nipkow@69666
   636
  shows "rank A = CARD('m) \<longleftrightarrow> surj ((*v) A)"
nipkow@69666
   637
  by (simp add: matrix_right_invertible_surjective [symmetric] left_invertible_transpose [symmetric]
nipkow@69666
   638
                matrix_left_invertible_injective full_rank_injective [symmetric] rank_transpose)
nipkow@69666
   639
ak2110@69723
   640
lemma rank_I: "rank(mat 1::real^'n^'n) = CARD('n)"
nipkow@69666
   641
  by (simp add: full_rank_injective inj_on_def)
nipkow@69666
   642
ak2110@69723
   643
lemma less_rank_noninjective:
nipkow@69666
   644
  fixes A :: "real^'n^'m"
nipkow@69666
   645
  shows "rank A < CARD('n) \<longleftrightarrow> \<not> inj ((*v) A)"
nipkow@69666
   646
using less_le rank_bound by (auto simp: full_rank_injective [symmetric])
nipkow@69666
   647
ak2110@69723
   648
lemma matrix_nonfull_linear_equations_eq:
nipkow@69666
   649
  fixes A :: "real^'n^'m"
nipkow@69666
   650
  shows "(\<exists>x. (x \<noteq> 0) \<and> A *v x = 0) \<longleftrightarrow> rank A \<noteq> CARD('n)"
nipkow@69666
   651
  by (meson matrix_left_invertible_injective full_rank_injective matrix_left_invertible_ker)
nipkow@69666
   652
ak2110@69723
   653
lemma rank_eq_0: "rank A = 0 \<longleftrightarrow> A = 0" and rank_0 [simp]: "rank (0::real^'n^'m) = 0"
nipkow@69666
   654
  for A :: "real^'n^'m"
nipkow@69666
   655
  by (auto simp: rank_dim_range matrix_eq)
nipkow@69666
   656
ak2110@69723
   657
lemma rank_mul_le_right:
nipkow@69666
   658
  fixes A :: "real^'n^'m" and B :: "real^'p^'n"
nipkow@69666
   659
  shows "rank(A ** B) \<le> rank B"
ak2110@69723
   660
proof -
nipkow@69666
   661
  have "rank(A ** B) \<le> dim ((*v) A ` range ((*v) B))"
nipkow@69666
   662
    by (auto simp: rank_dim_range image_comp o_def matrix_vector_mul_assoc)
nipkow@69666
   663
  also have "\<dots> \<le> rank B"
nipkow@69666
   664
    by (simp add: rank_dim_range dim_image_le)
nipkow@69666
   665
  finally show ?thesis .
nipkow@69666
   666
qed
nipkow@69666
   667
ak2110@69723
   668
lemma rank_mul_le_left:
nipkow@69666
   669
  fixes A :: "real^'n^'m" and B :: "real^'p^'n"
nipkow@69666
   670
  shows "rank(A ** B) \<le> rank A"
nipkow@69666
   671
  by (metis matrix_transpose_mul rank_mul_le_right rank_transpose)
nipkow@69666
   672
nipkow@69669
   673
lp15@69918
   674
subsection%unimportant \<open>Lemmas for working on \<open>real^1/2/3/4\<close>\<close>
nipkow@69669
   675
nipkow@69669
   676
lemma exhaust_2:
nipkow@69669
   677
  fixes x :: 2
nipkow@69669
   678
  shows "x = 1 \<or> x = 2"
nipkow@69669
   679
proof (induct x)
nipkow@69669
   680
  case (of_int z)
nipkow@69669
   681
  then have "0 \<le> z" and "z < 2" by simp_all
nipkow@69669
   682
  then have "z = 0 | z = 1" by arith
nipkow@69669
   683
  then show ?case by auto
nipkow@69669
   684
qed
nipkow@69669
   685
nipkow@69669
   686
lemma forall_2: "(\<forall>i::2. P i) \<longleftrightarrow> P 1 \<and> P 2"
nipkow@69669
   687
  by (metis exhaust_2)
nipkow@69669
   688
nipkow@69669
   689
lemma exhaust_3:
nipkow@69669
   690
  fixes x :: 3
nipkow@69669
   691
  shows "x = 1 \<or> x = 2 \<or> x = 3"
nipkow@69669
   692
proof (induct x)
nipkow@69669
   693
  case (of_int z)
nipkow@69669
   694
  then have "0 \<le> z" and "z < 3" by simp_all
nipkow@69669
   695
  then have "z = 0 \<or> z = 1 \<or> z = 2" by arith
nipkow@69669
   696
  then show ?case by auto
nipkow@69669
   697
qed
nipkow@69669
   698
nipkow@69669
   699
lemma forall_3: "(\<forall>i::3. P i) \<longleftrightarrow> P 1 \<and> P 2 \<and> P 3"
nipkow@69669
   700
  by (metis exhaust_3)
nipkow@69669
   701
lp15@69918
   702
lemma exhaust_4:
lp15@69918
   703
  fixes x :: 4
lp15@69918
   704
  shows "x = 1 \<or> x = 2 \<or> x = 3 \<or> x = 4"
lp15@69918
   705
proof (induct x)
lp15@69918
   706
  case (of_int z)
lp15@69918
   707
  then have "0 \<le> z" and "z < 4" by simp_all
lp15@69918
   708
  then have "z = 0 \<or> z = 1 \<or> z = 2 \<or> z = 3" by arith
lp15@69918
   709
  then show ?case by auto
lp15@69918
   710
qed
lp15@69918
   711
lp15@69918
   712
lemma forall_4: "(\<forall>i::4. P i) \<longleftrightarrow> P 1 \<and> P 2 \<and> P 3 \<and> P 4"
lp15@69918
   713
  by (metis exhaust_4)
lp15@69918
   714
nipkow@69669
   715
lemma UNIV_1 [simp]: "UNIV = {1::1}"
nipkow@69669
   716
  by (auto simp add: num1_eq_iff)
nipkow@69669
   717
nipkow@69669
   718
lemma UNIV_2: "UNIV = {1::2, 2::2}"
nipkow@69669
   719
  using exhaust_2 by auto
nipkow@69669
   720
nipkow@69669
   721
lemma UNIV_3: "UNIV = {1::3, 2::3, 3::3}"
nipkow@69669
   722
  using exhaust_3 by auto
nipkow@69669
   723
lp15@69918
   724
lemma UNIV_4: "UNIV = {1::4, 2::4, 3::4, 4::4}"
lp15@69918
   725
  using exhaust_4 by auto
lp15@69918
   726
nipkow@69669
   727
lemma sum_1: "sum f (UNIV::1 set) = f 1"
nipkow@69669
   728
  unfolding UNIV_1 by simp
nipkow@69669
   729
nipkow@69669
   730
lemma sum_2: "sum f (UNIV::2 set) = f 1 + f 2"
nipkow@69669
   731
  unfolding UNIV_2 by simp
nipkow@69669
   732
nipkow@69669
   733
lemma sum_3: "sum f (UNIV::3 set) = f 1 + f 2 + f 3"
nipkow@69669
   734
  unfolding UNIV_3 by (simp add: ac_simps)
nipkow@69669
   735
lp15@69918
   736
lemma sum_4: "sum f (UNIV::4 set) = f 1 + f 2 + f 3 + f 4"
lp15@69918
   737
  unfolding UNIV_4 by (simp add: ac_simps)
lp15@69918
   738
nipkow@69669
   739
subsection%unimportant\<open>The collapse of the general concepts to dimension one\<close>
nipkow@69669
   740
nipkow@69669
   741
lemma vector_one: "(x::'a ^1) = (\<chi> i. (x$1))"
nipkow@69669
   742
  by (simp add: vec_eq_iff)
nipkow@69669
   743
nipkow@69669
   744
lemma forall_one: "(\<forall>(x::'a ^1). P x) \<longleftrightarrow> (\<forall>x. P(\<chi> i. x))"
nipkow@69669
   745
  apply auto
nipkow@69669
   746
  apply (erule_tac x= "x$1" in allE)
nipkow@69669
   747
  apply (simp only: vector_one[symmetric])
nipkow@69669
   748
  done
nipkow@69669
   749
nipkow@69669
   750
lemma norm_vector_1: "norm (x :: _^1) = norm (x$1)"
nipkow@69669
   751
  by (simp add: norm_vec_def)
nipkow@69669
   752
nipkow@69669
   753
lemma dist_vector_1:
nipkow@69669
   754
  fixes x :: "'a::real_normed_vector^1"
nipkow@69669
   755
  shows "dist x y = dist (x$1) (y$1)"
nipkow@69669
   756
  by (simp add: dist_norm norm_vector_1)
nipkow@69669
   757
nipkow@69669
   758
lemma norm_real: "norm(x::real ^ 1) = \<bar>x$1\<bar>"
nipkow@69669
   759
  by (simp add: norm_vector_1)
nipkow@69669
   760
nipkow@69669
   761
lemma dist_real: "dist(x::real ^ 1) y = \<bar>(x$1) - (y$1)\<bar>"
nipkow@69669
   762
  by (auto simp add: norm_real dist_norm)
nipkow@69669
   763
nipkow@69669
   764
nipkow@69669
   765
subsection%unimportant\<open>Routine results connecting the types \<^typ>\<open>real^1\<close> and \<^typ>\<open>real\<close>\<close>
nipkow@69669
   766
nipkow@69669
   767
lemma vector_one_nth [simp]:
nipkow@69669
   768
  fixes x :: "'a^1" shows "vec (x $ 1) = x"
nipkow@69669
   769
  by (metis vec_def vector_one)
nipkow@69669
   770
nipkow@69669
   771
lemma tendsto_at_within_vector_1:
nipkow@69669
   772
  fixes S :: "'a :: metric_space set"
nipkow@69669
   773
  assumes "(f \<longlongrightarrow> fx) (at x within S)"
nipkow@69669
   774
  shows "((\<lambda>y::'a^1. \<chi> i. f (y $ 1)) \<longlongrightarrow> (vec fx::'a^1)) (at (vec x) within vec ` S)"
nipkow@69669
   775
proof (rule topological_tendstoI)
nipkow@69669
   776
  fix T :: "('a^1) set"
nipkow@69669
   777
  assume "open T" "vec fx \<in> T"
nipkow@69669
   778
  have "\<forall>\<^sub>F x in at x within S. f x \<in> (\<lambda>x. x $ 1) ` T"
nipkow@69669
   779
    using \<open>open T\<close> \<open>vec fx \<in> T\<close> assms open_image_vec_nth tendsto_def by fastforce
nipkow@69669
   780
  then show "\<forall>\<^sub>F x::'a^1 in at (vec x) within vec ` S. (\<chi> i. f (x $ 1)) \<in> T"
nipkow@69669
   781
    unfolding eventually_at dist_norm [symmetric]
nipkow@69669
   782
    by (rule ex_forward)
nipkow@69669
   783
       (use \<open>open T\<close> in 
nipkow@69669
   784
         \<open>fastforce simp: dist_norm dist_vec_def L2_set_def image_iff vector_one open_vec_def\<close>)
nipkow@69669
   785
qed
nipkow@69669
   786
nipkow@69669
   787
lemma has_derivative_vector_1:
nipkow@69669
   788
  assumes der_g: "(g has_derivative (\<lambda>x. x * g' a)) (at a within S)"
nipkow@69669
   789
  shows "((\<lambda>x. vec (g (x $ 1))) has_derivative (*\<^sub>R) (g' a))
nipkow@69669
   790
         (at ((vec a)::real^1) within vec ` S)"
nipkow@69669
   791
    using der_g
nipkow@69669
   792
    apply (auto simp: Deriv.has_derivative_within bounded_linear_scaleR_right norm_vector_1)
nipkow@69669
   793
    apply (drule tendsto_at_within_vector_1, vector)
nipkow@69669
   794
    apply (auto simp: algebra_simps eventually_at tendsto_def)
nipkow@69669
   795
    done
nipkow@69669
   796
nipkow@69669
   797
nipkow@69669
   798
subsection%unimportant\<open>Explicit vector construction from lists\<close>
nipkow@69669
   799
nipkow@69669
   800
definition "vector l = (\<chi> i. foldr (\<lambda>x f n. fun_upd (f (n+1)) n x) l (\<lambda>n x. 0) 1 i)"
nipkow@69669
   801
nipkow@69669
   802
lemma vector_1 [simp]: "(vector[x]) $1 = x"
nipkow@69669
   803
  unfolding vector_def by simp
nipkow@69669
   804
nipkow@69669
   805
lemma vector_2 [simp]: "(vector[x,y]) $1 = x" "(vector[x,y] :: 'a^2)$2 = (y::'a::zero)"
nipkow@69669
   806
  unfolding vector_def by simp_all
nipkow@69669
   807
nipkow@69669
   808
lemma vector_3 [simp]:
nipkow@69669
   809
 "(vector [x,y,z] ::('a::zero)^3)$1 = x"
nipkow@69669
   810
 "(vector [x,y,z] ::('a::zero)^3)$2 = y"
nipkow@69669
   811
 "(vector [x,y,z] ::('a::zero)^3)$3 = z"
nipkow@69669
   812
  unfolding vector_def by simp_all
nipkow@69669
   813
nipkow@69669
   814
lemma forall_vector_1: "(\<forall>v::'a::zero^1. P v) \<longleftrightarrow> (\<forall>x. P(vector[x]))"
nipkow@69669
   815
  by (metis vector_1 vector_one)
nipkow@69669
   816
nipkow@69669
   817
lemma forall_vector_2: "(\<forall>v::'a::zero^2. P v) \<longleftrightarrow> (\<forall>x y. P(vector[x, y]))"
nipkow@69669
   818
  apply auto
nipkow@69669
   819
  apply (erule_tac x="v$1" in allE)
nipkow@69669
   820
  apply (erule_tac x="v$2" in allE)
nipkow@69669
   821
  apply (subgoal_tac "vector [v$1, v$2] = v")
nipkow@69669
   822
  apply simp
nipkow@69669
   823
  apply (vector vector_def)
nipkow@69669
   824
  apply (simp add: forall_2)
nipkow@69669
   825
  done
nipkow@69669
   826
nipkow@69669
   827
lemma forall_vector_3: "(\<forall>v::'a::zero^3. P v) \<longleftrightarrow> (\<forall>x y z. P(vector[x, y, z]))"
nipkow@69669
   828
  apply auto
nipkow@69669
   829
  apply (erule_tac x="v$1" in allE)
nipkow@69669
   830
  apply (erule_tac x="v$2" in allE)
nipkow@69669
   831
  apply (erule_tac x="v$3" in allE)
nipkow@69669
   832
  apply (subgoal_tac "vector [v$1, v$2, v$3] = v")
nipkow@69669
   833
  apply simp
nipkow@69669
   834
  apply (vector vector_def)
nipkow@69669
   835
  apply (simp add: forall_3)
nipkow@69669
   836
  done
nipkow@69669
   837
nipkow@69669
   838
subsection%unimportant \<open>lambda skolemization on cartesian products\<close>
nipkow@69669
   839
ak2110@69723
   840
lemma lambda_skolem: "(\<forall>i. \<exists>x. P i x) \<longleftrightarrow>
nipkow@69669
   841
   (\<exists>x::'a ^ 'n. \<forall>i. P i (x $ i))" (is "?lhs \<longleftrightarrow> ?rhs")
ak2110@69723
   842
proof -
nipkow@69669
   843
  let ?S = "(UNIV :: 'n set)"
nipkow@69669
   844
  { assume H: "?rhs"
nipkow@69669
   845
    then have ?lhs by auto }
nipkow@69669
   846
  moreover
nipkow@69669
   847
  { assume H: "?lhs"
nipkow@69669
   848
    then obtain f where f:"\<forall>i. P i (f i)" unfolding choice_iff by metis
nipkow@69669
   849
    let ?x = "(\<chi> i. (f i)) :: 'a ^ 'n"
nipkow@69669
   850
    { fix i
nipkow@69669
   851
      from f have "P i (f i)" by metis
nipkow@69669
   852
      then have "P i (?x $ i)" by auto
nipkow@69669
   853
    }
nipkow@69669
   854
    hence "\<forall>i. P i (?x$i)" by metis
nipkow@69669
   855
    hence ?rhs by metis }
nipkow@69669
   856
  ultimately show ?thesis by metis
nipkow@69669
   857
qed
nipkow@69669
   858
nipkow@69669
   859
nipkow@69669
   860
text \<open>The same result in terms of square matrices.\<close>
nipkow@69669
   861
nipkow@69669
   862
nipkow@69669
   863
text \<open>Considering an n-element vector as an n-by-1 or 1-by-n matrix.\<close>
nipkow@69669
   864
ak2110@69723
   865
definition "rowvector v = (\<chi> i j. (v$j))"
nipkow@69669
   866
ak2110@69723
   867
definition "columnvector v = (\<chi> i j. (v$i))"
nipkow@69669
   868
ak2110@69723
   869
lemma transpose_columnvector: "transpose(columnvector v) = rowvector v"
nipkow@69669
   870
  by (simp add: transpose_def rowvector_def columnvector_def vec_eq_iff)
nipkow@69669
   871
ak2110@69723
   872
lemma transpose_rowvector: "transpose(rowvector v) = columnvector v"
nipkow@69669
   873
  by (simp add: transpose_def columnvector_def rowvector_def vec_eq_iff)
nipkow@69669
   874
ak2110@69723
   875
lemma dot_rowvector_columnvector: "columnvector (A *v v) = A ** columnvector v"
nipkow@69669
   876
  by (vector columnvector_def matrix_matrix_mult_def matrix_vector_mult_def)
nipkow@69669
   877
ak2110@69723
   878
lemma dot_matrix_product:
nipkow@69669
   879
  "(x::real^'n) \<bullet> y = (((rowvector x ::real^'n^1) ** (columnvector y :: real^1^'n))$1)$1"
nipkow@69669
   880
  by (vector matrix_matrix_mult_def rowvector_def columnvector_def inner_vec_def)
nipkow@69669
   881
ak2110@69723
   882
lemma dot_matrix_vector_mul:
nipkow@69669
   883
  fixes A B :: "real ^'n ^'n" and x y :: "real ^'n"
nipkow@69669
   884
  shows "(A *v x) \<bullet> (B *v y) =
nipkow@69669
   885
      (((rowvector x :: real^'n^1) ** ((transpose A ** B) ** (columnvector y :: real ^1^'n)))$1)$1"
nipkow@69669
   886
  unfolding dot_matrix_product transpose_columnvector[symmetric]
nipkow@69669
   887
    dot_rowvector_columnvector matrix_transpose_mul matrix_mul_assoc ..
nipkow@69669
   888
nipkow@69669
   889
ak2110@69723
   890
lemma dim_substandard_cart: "vec.dim {x::'a::field^'n. \<forall>i. i \<notin> d \<longrightarrow> x$i = 0} = card d"
nipkow@69669
   891
  (is "vec.dim ?A = _")
ak2110@69723
   892
proof (rule vec.dim_unique)
nipkow@69669
   893
  let ?B = "((\<lambda>x. axis x 1) ` d)"
nipkow@69669
   894
  have subset_basis: "?B \<subseteq> cart_basis"
nipkow@69669
   895
    by (auto simp: cart_basis_def)
nipkow@69669
   896
  show "?B \<subseteq> ?A"
nipkow@69669
   897
    by (auto simp: axis_def)
nipkow@69669
   898
  show "vec.independent ((\<lambda>x. axis x 1) ` d)"
nipkow@69669
   899
    using subset_basis
nipkow@69669
   900
    by (rule vec.independent_mono[OF vec.independent_Basis])
nipkow@69669
   901
  have "x \<in> vec.span ?B" if "\<forall>i. i \<notin> d \<longrightarrow> x $ i = 0" for x::"'a^'n"
nipkow@69669
   902
  proof -
nipkow@69669
   903
    have "finite ?B"
nipkow@69669
   904
      using subset_basis finite_cart_basis
nipkow@69669
   905
      by (rule finite_subset)
nipkow@69669
   906
    have "x = (\<Sum>i\<in>UNIV. x $ i *s axis i 1)"
nipkow@69669
   907
      by (rule basis_expansion[symmetric])
nipkow@69669
   908
    also have "\<dots> = (\<Sum>i\<in>d. (x $ i) *s axis i 1)"
nipkow@69669
   909
      by (rule sum.mono_neutral_cong_right) (auto simp: that)
nipkow@69669
   910
    also have "\<dots> \<in> vec.span ?B"
nipkow@69669
   911
      by (simp add: vec.span_sum vec.span_clauses)
nipkow@69669
   912
    finally show "x \<in> vec.span ?B" .
nipkow@69669
   913
  qed
nipkow@69669
   914
  then show "?A \<subseteq> vec.span ?B" by auto
nipkow@69669
   915
qed (simp add: card_image inj_on_def axis_eq_axis)
nipkow@69669
   916
ak2110@69723
   917
lemma affinity_inverses:
nipkow@69669
   918
  assumes m0: "m \<noteq> (0::'a::field)"
nipkow@69669
   919
  shows "(\<lambda>x. m *s x + c) \<circ> (\<lambda>x. inverse(m) *s x + (-(inverse(m) *s c))) = id"
nipkow@69669
   920
  "(\<lambda>x. inverse(m) *s x + (-(inverse(m) *s c))) \<circ> (\<lambda>x. m *s x + c) = id"
nipkow@69669
   921
  using m0
nipkow@69669
   922
  by (auto simp add: fun_eq_iff vector_add_ldistrib diff_conv_add_uminus simp del: add_uminus_conv_diff)
nipkow@69669
   923
ak2110@69723
   924
lemma vector_affinity_eq:
nipkow@69669
   925
  assumes m0: "(m::'a::field) \<noteq> 0"
nipkow@69669
   926
  shows "m *s x + c = y \<longleftrightarrow> x = inverse m *s y + -(inverse m *s c)"
ak2110@69723
   927
proof
nipkow@69669
   928
  assume h: "m *s x + c = y"
nipkow@69669
   929
  hence "m *s x = y - c" by (simp add: field_simps)
nipkow@69669
   930
  hence "inverse m *s (m *s x) = inverse m *s (y - c)" by simp
nipkow@69669
   931
  then show "x = inverse m *s y + - (inverse m *s c)"
nipkow@69669
   932
    using m0 by (simp add: vector_smult_assoc vector_ssub_ldistrib)
nipkow@69669
   933
next
nipkow@69669
   934
  assume h: "x = inverse m *s y + - (inverse m *s c)"
nipkow@69669
   935
  show "m *s x + c = y" unfolding h
nipkow@69669
   936
    using m0 by (simp add: vector_smult_assoc vector_ssub_ldistrib)
nipkow@69669
   937
qed
nipkow@69669
   938
ak2110@69723
   939
lemma vector_eq_affinity:
nipkow@69669
   940
    "(m::'a::field) \<noteq> 0 ==> (y = m *s x + c \<longleftrightarrow> inverse(m) *s y + -(inverse(m) *s c) = x)"
nipkow@69669
   941
  using vector_affinity_eq[where m=m and x=x and y=y and c=c]
nipkow@69669
   942
  by metis
nipkow@69669
   943
ak2110@69723
   944
lemma vector_cart:
nipkow@69669
   945
  fixes f :: "real^'n \<Rightarrow> real"
nipkow@69669
   946
  shows "(\<chi> i. f (axis i 1)) = (\<Sum>i\<in>Basis. f i *\<^sub>R i)"
nipkow@69669
   947
  unfolding euclidean_eq_iff[where 'a="real^'n"]
nipkow@69669
   948
  by simp (simp add: Basis_vec_def inner_axis)
nipkow@69669
   949
ak2110@69723
   950
lemma const_vector_cart:"((\<chi> i. d)::real^'n) = (\<Sum>i\<in>Basis. d *\<^sub>R i)"
nipkow@69669
   951
  by (rule vector_cart)
nipkow@69669
   952
immler@69675
   953
subsection%unimportant \<open>Explicit formulas for low dimensions\<close>
immler@69675
   954
ak2110@69723
   955
lemma  prod_neutral_const: "prod f {(1::nat)..1} = f 1"
immler@69675
   956
  by simp
immler@69675
   957
ak2110@69723
   958
lemma  prod_2: "prod f {(1::nat)..2} = f 1 * f 2"
immler@69675
   959
  by (simp add: eval_nat_numeral atLeastAtMostSuc_conv mult.commute)
immler@69675
   960
ak2110@69723
   961
lemma  prod_3: "prod f {(1::nat)..3} = f 1 * f 2 * f 3"
immler@69675
   962
  by (simp add: eval_nat_numeral atLeastAtMostSuc_conv mult.commute)
immler@69675
   963
immler@69675
   964
immler@69683
   965
subsection  \<open>Orthogonality of a matrix\<close>
immler@69675
   966
immler@69675
   967
definition%important  "orthogonal_matrix (Q::'a::semiring_1^'n^'n) \<longleftrightarrow>
immler@69675
   968
  transpose Q ** Q = mat 1 \<and> Q ** transpose Q = mat 1"
immler@69675
   969
ak2110@69723
   970
lemma  orthogonal_matrix: "orthogonal_matrix (Q:: real ^'n^'n) \<longleftrightarrow> transpose Q ** Q = mat 1"
immler@69675
   971
  by (metis matrix_left_right_inverse orthogonal_matrix_def)
immler@69675
   972
ak2110@69723
   973
lemma  orthogonal_matrix_id: "orthogonal_matrix (mat 1 :: _^'n^'n)"
immler@69675
   974
  by (simp add: orthogonal_matrix_def)
immler@69675
   975
ak2110@69723
   976
proposition  orthogonal_matrix_mul:
immler@69675
   977
  fixes A :: "real ^'n^'n"
immler@69675
   978
  assumes  "orthogonal_matrix A" "orthogonal_matrix B"
immler@69675
   979
  shows "orthogonal_matrix(A ** B)"
immler@69675
   980
  using assms
immler@69675
   981
  by (simp add: orthogonal_matrix matrix_transpose_mul matrix_left_right_inverse matrix_mul_assoc)
immler@69675
   982
ak2110@69723
   983
proposition  orthogonal_transformation_matrix:
immler@69675
   984
  fixes f:: "real^'n \<Rightarrow> real^'n"
immler@69675
   985
  shows "orthogonal_transformation f \<longleftrightarrow> linear f \<and> orthogonal_matrix(matrix f)"
immler@69675
   986
  (is "?lhs \<longleftrightarrow> ?rhs")
ak2110@69723
   987
proof -
immler@69675
   988
  let ?mf = "matrix f"
immler@69675
   989
  let ?ot = "orthogonal_transformation f"
immler@69675
   990
  let ?U = "UNIV :: 'n set"
immler@69675
   991
  have fU: "finite ?U" by simp
immler@69675
   992
  let ?m1 = "mat 1 :: real ^'n^'n"
immler@69675
   993
  {
immler@69675
   994
    assume ot: ?ot
immler@69675
   995
    from ot have lf: "Vector_Spaces.linear (*s) (*s) f" and fd: "\<And>v w. f v \<bullet> f w = v \<bullet> w"
immler@69675
   996
      unfolding orthogonal_transformation_def orthogonal_matrix linear_def scalar_mult_eq_scaleR
immler@69675
   997
      by blast+
immler@69675
   998
    {
immler@69675
   999
      fix i j
immler@69675
  1000
      let ?A = "transpose ?mf ** ?mf"
immler@69675
  1001
      have th0: "\<And>b (x::'a::comm_ring_1). (if b then 1 else 0)*x = (if b then x else 0)"
immler@69675
  1002
        "\<And>b (x::'a::comm_ring_1). x*(if b then 1 else 0) = (if b then x else 0)"
immler@69675
  1003
        by simp_all
immler@69675
  1004
      from fd[of "axis i 1" "axis j 1",
immler@69675
  1005
        simplified matrix_works[OF lf, symmetric] dot_matrix_vector_mul]
immler@69675
  1006
      have "?A$i$j = ?m1 $ i $ j"
immler@69675
  1007
        by (simp add: inner_vec_def matrix_matrix_mult_def columnvector_def rowvector_def
immler@69675
  1008
            th0 sum.delta[OF fU] mat_def axis_def)
immler@69675
  1009
    }
immler@69675
  1010
    then have "orthogonal_matrix ?mf"
immler@69675
  1011
      unfolding orthogonal_matrix
immler@69675
  1012
      by vector
immler@69675
  1013
    with lf have ?rhs
immler@69675
  1014
      unfolding linear_def scalar_mult_eq_scaleR
immler@69675
  1015
      by blast
immler@69675
  1016
  }
immler@69675
  1017
  moreover
immler@69675
  1018
  {
immler@69675
  1019
    assume lf: "Vector_Spaces.linear (*s) (*s) f" and om: "orthogonal_matrix ?mf"
immler@69675
  1020
    from lf om have ?lhs
immler@69675
  1021
      unfolding orthogonal_matrix_def norm_eq orthogonal_transformation
immler@69675
  1022
      apply (simp only: matrix_works[OF lf, symmetric] dot_matrix_vector_mul)
immler@69675
  1023
      apply (simp add: dot_matrix_product linear_def scalar_mult_eq_scaleR)
immler@69675
  1024
      done
immler@69675
  1025
  }
immler@69675
  1026
  ultimately show ?thesis
immler@69675
  1027
    by (auto simp: linear_def scalar_mult_eq_scaleR)
immler@69675
  1028
qed
immler@69675
  1029
immler@69675
  1030
immler@69683
  1031
subsection \<open> We can find an orthogonal matrix taking any unit vector to any other\<close>
immler@69675
  1032
ak2110@69723
  1033
lemma  orthogonal_matrix_transpose [simp]:
immler@69675
  1034
     "orthogonal_matrix(transpose A) \<longleftrightarrow> orthogonal_matrix A"
immler@69675
  1035
  by (auto simp: orthogonal_matrix_def)
immler@69675
  1036
ak2110@69723
  1037
lemma  orthogonal_matrix_orthonormal_columns:
immler@69675
  1038
  fixes A :: "real^'n^'n"
immler@69675
  1039
  shows "orthogonal_matrix A \<longleftrightarrow>
immler@69675
  1040
          (\<forall>i. norm(column i A) = 1) \<and>
immler@69675
  1041
          (\<forall>i j. i \<noteq> j \<longrightarrow> orthogonal (column i A) (column j A))"
immler@69675
  1042
  by (auto simp: orthogonal_matrix matrix_mult_transpose_dot_column vec_eq_iff mat_def norm_eq_1 orthogonal_def)
immler@69675
  1043
ak2110@69723
  1044
lemma  orthogonal_matrix_orthonormal_rows:
immler@69675
  1045
  fixes A :: "real^'n^'n"
immler@69675
  1046
  shows "orthogonal_matrix A \<longleftrightarrow>
immler@69675
  1047
          (\<forall>i. norm(row i A) = 1) \<and>
immler@69675
  1048
          (\<forall>i j. i \<noteq> j \<longrightarrow> orthogonal (row i A) (row j A))"
immler@69675
  1049
  using orthogonal_matrix_orthonormal_columns [of "transpose A"] by simp
immler@69675
  1050
ak2110@69723
  1051
proposition  orthogonal_matrix_exists_basis:
immler@69675
  1052
  fixes a :: "real^'n"
immler@69675
  1053
  assumes "norm a = 1"
immler@69675
  1054
  obtains A where "orthogonal_matrix A" "A *v (axis k 1) = a"
ak2110@69723
  1055
proof -
immler@69675
  1056
  obtain S where "a \<in> S" "pairwise orthogonal S" and noS: "\<And>x. x \<in> S \<Longrightarrow> norm x = 1"
immler@69675
  1057
   and "independent S" "card S = CARD('n)" "span S = UNIV"
immler@69675
  1058
    using vector_in_orthonormal_basis assms by force
immler@69675
  1059
  then obtain f0 where "bij_betw f0 (UNIV::'n set) S"
immler@69675
  1060
    by (metis finite_class.finite_UNIV finite_same_card_bij finiteI_independent)
immler@69675
  1061
  then obtain f where f: "bij_betw f (UNIV::'n set) S" and a: "a = f k"
immler@69675
  1062
    using bij_swap_iff [of k "inv f0 a" f0]
immler@69675
  1063
    by (metis UNIV_I \<open>a \<in> S\<close> bij_betw_inv_into_right bij_betw_swap_iff swap_apply(1))
immler@69675
  1064
  show thesis
immler@69675
  1065
  proof
immler@69675
  1066
    have [simp]: "\<And>i. norm (f i) = 1"
immler@69675
  1067
      using bij_betwE [OF \<open>bij_betw f UNIV S\<close>] by (blast intro: noS)
immler@69675
  1068
    have [simp]: "\<And>i j. i \<noteq> j \<Longrightarrow> orthogonal (f i) (f j)"
immler@69675
  1069
      using \<open>pairwise orthogonal S\<close> \<open>bij_betw f UNIV S\<close>
immler@69675
  1070
      by (auto simp: pairwise_def bij_betw_def inj_on_def)
immler@69675
  1071
    show "orthogonal_matrix (\<chi> i j. f j $ i)"
immler@69675
  1072
      by (simp add: orthogonal_matrix_orthonormal_columns column_def)
immler@69675
  1073
    show "(\<chi> i j. f j $ i) *v axis k 1 = a"
immler@69675
  1074
      by (simp add: matrix_vector_mult_def axis_def a if_distrib cong: if_cong)
immler@69675
  1075
  qed
immler@69675
  1076
qed
immler@69675
  1077
ak2110@69723
  1078
lemma  orthogonal_transformation_exists_1:
immler@69675
  1079
  fixes a b :: "real^'n"
immler@69675
  1080
  assumes "norm a = 1" "norm b = 1"
immler@69675
  1081
  obtains f where "orthogonal_transformation f" "f a = b"
ak2110@69723
  1082
proof -
immler@69675
  1083
  obtain k::'n where True
immler@69675
  1084
    by simp
immler@69675
  1085
  obtain A B where AB: "orthogonal_matrix A" "orthogonal_matrix B" and eq: "A *v (axis k 1) = a" "B *v (axis k 1) = b"
immler@69675
  1086
    using orthogonal_matrix_exists_basis assms by metis
immler@69675
  1087
  let ?f = "\<lambda>x. (B ** transpose A) *v x"
immler@69675
  1088
  show thesis
immler@69675
  1089
  proof
immler@69675
  1090
    show "orthogonal_transformation ?f"
immler@69675
  1091
      by (subst orthogonal_transformation_matrix)
immler@69675
  1092
        (auto simp: AB orthogonal_matrix_mul)
immler@69675
  1093
  next
immler@69675
  1094
    show "?f a = b"
immler@69675
  1095
      using \<open>orthogonal_matrix A\<close> unfolding orthogonal_matrix_def
immler@69675
  1096
      by (metis eq matrix_mul_rid matrix_vector_mul_assoc)
immler@69675
  1097
  qed
immler@69675
  1098
qed
immler@69675
  1099
ak2110@69723
  1100
proposition  orthogonal_transformation_exists:
immler@69675
  1101
  fixes a b :: "real^'n"
immler@69675
  1102
  assumes "norm a = norm b"
immler@69675
  1103
  obtains f where "orthogonal_transformation f" "f a = b"
ak2110@69723
  1104
proof (cases "a = 0 \<or> b = 0")
immler@69675
  1105
  case True
immler@69675
  1106
  with assms show ?thesis
immler@69675
  1107
    using that by force
immler@69675
  1108
next
immler@69675
  1109
  case False
immler@69675
  1110
  then obtain f where f: "orthogonal_transformation f" and eq: "f (a /\<^sub>R norm a) = (b /\<^sub>R norm b)"
immler@69675
  1111
    by (auto intro: orthogonal_transformation_exists_1 [of "a /\<^sub>R norm a" "b /\<^sub>R norm b"])
immler@69675
  1112
  show ?thesis
immler@69675
  1113
  proof
immler@69675
  1114
    interpret linear f
immler@69675
  1115
      using f by (simp add: orthogonal_transformation_linear)
immler@69675
  1116
    have "f a /\<^sub>R norm a = f (a /\<^sub>R norm a)"
immler@69675
  1117
      by (simp add: scale)
immler@69675
  1118
    also have "\<dots> = b /\<^sub>R norm a"
immler@69675
  1119
      by (simp add: eq assms [symmetric])
immler@69675
  1120
    finally show "f a = b"
immler@69675
  1121
      using False by auto
immler@69675
  1122
  qed (use f in auto)
immler@69675
  1123
qed
immler@69675
  1124
immler@69675
  1125
immler@69683
  1126
subsection  \<open>Linearity of scaling, and hence isometry, that preserves origin\<close>
immler@69675
  1127
ak2110@69723
  1128
lemma  scaling_linear:
immler@69675
  1129
  fixes f :: "'a::real_inner \<Rightarrow> 'a::real_inner"
immler@69675
  1130
  assumes f0: "f 0 = 0"
immler@69675
  1131
    and fd: "\<forall>x y. dist (f x) (f y) = c * dist x y"
immler@69675
  1132
  shows "linear f"
ak2110@69723
  1133
proof -
immler@69675
  1134
  {
immler@69675
  1135
    fix v w
immler@69675
  1136
    have "norm (f x) = c * norm x" for x
immler@69675
  1137
      by (metis dist_0_norm f0 fd)
immler@69675
  1138
    then have "f v \<bullet> f w = c\<^sup>2 * (v \<bullet> w)"
immler@69675
  1139
      unfolding dot_norm_neg dist_norm[symmetric]
immler@69675
  1140
      by (simp add: fd power2_eq_square field_simps)
immler@69675
  1141
  }
immler@69675
  1142
  then show ?thesis
immler@69675
  1143
    unfolding linear_iff vector_eq[where 'a="'a"] scalar_mult_eq_scaleR
immler@69675
  1144
    by (simp add: inner_add field_simps)
immler@69675
  1145
qed
immler@69675
  1146
ak2110@69723
  1147
lemma  isometry_linear:
immler@69675
  1148
  "f (0::'a::real_inner) = (0::'a) \<Longrightarrow> \<forall>x y. dist(f x) (f y) = dist x y \<Longrightarrow> linear f"
immler@69675
  1149
  by (rule scaling_linear[where c=1]) simp_all
immler@69675
  1150
immler@69675
  1151
text \<open>Hence another formulation of orthogonal transformation\<close>
immler@69675
  1152
ak2110@69723
  1153
proposition  orthogonal_transformation_isometry:
immler@69675
  1154
  "orthogonal_transformation f \<longleftrightarrow> f(0::'a::real_inner) = (0::'a) \<and> (\<forall>x y. dist(f x) (f y) = dist x y)"
immler@69675
  1155
  unfolding orthogonal_transformation
immler@69675
  1156
  apply (auto simp: linear_0 isometry_linear)
immler@69675
  1157
   apply (metis (no_types, hide_lams) dist_norm linear_diff)
immler@69675
  1158
  by (metis dist_0_norm)
immler@69675
  1159
immler@69675
  1160
immler@69683
  1161
subsection  \<open>Can extend an isometry from unit sphere\<close>
immler@69675
  1162
ak2110@69723
  1163
lemma  isometry_sphere_extend:
immler@69675
  1164
  fixes f:: "'a::real_inner \<Rightarrow> 'a"
immler@69675
  1165
  assumes f1: "\<And>x. norm x = 1 \<Longrightarrow> norm (f x) = 1"
immler@69675
  1166
    and fd1: "\<And>x y. \<lbrakk>norm x = 1; norm y = 1\<rbrakk> \<Longrightarrow> dist (f x) (f y) = dist x y"
immler@69675
  1167
  shows "\<exists>g. orthogonal_transformation g \<and> (\<forall>x. norm x = 1 \<longrightarrow> g x = f x)"
ak2110@69723
  1168
proof -
immler@69675
  1169
  {
immler@69675
  1170
    fix x y x' y' u v u' v' :: "'a"
immler@69675
  1171
    assume H: "x = norm x *\<^sub>R u" "y = norm y *\<^sub>R v"
immler@69675
  1172
              "x' = norm x *\<^sub>R u'" "y' = norm y *\<^sub>R v'"
immler@69675
  1173
      and J: "norm u = 1" "norm u' = 1" "norm v = 1" "norm v' = 1" "norm(u' - v') = norm(u - v)"
immler@69675
  1174
    then have *: "u \<bullet> v = u' \<bullet> v' + v' \<bullet> u' - v \<bullet> u "
immler@69675
  1175
      by (simp add: norm_eq norm_eq_1 inner_add inner_diff)
immler@69675
  1176
    have "norm (norm x *\<^sub>R u' - norm y *\<^sub>R v') = norm (norm x *\<^sub>R u - norm y *\<^sub>R v)"
immler@69675
  1177
      using J by (simp add: norm_eq norm_eq_1 inner_diff * field_simps)
immler@69675
  1178
    then have "norm(x' - y') = norm(x - y)"
immler@69675
  1179
      using H by metis
immler@69675
  1180
  }
immler@69675
  1181
  note norm_eq = this
immler@69675
  1182
  let ?g = "\<lambda>x. if x = 0 then 0 else norm x *\<^sub>R f (x /\<^sub>R norm x)"
immler@69675
  1183
  have thfg: "?g x = f x" if "norm x = 1" for x
immler@69675
  1184
    using that by auto
immler@69675
  1185
  have thd: "dist (?g x) (?g y) = dist x y" for x y
immler@69675
  1186
  proof (cases "x=0 \<or> y=0")
immler@69675
  1187
    case False
immler@69675
  1188
    show "dist (?g x) (?g y) = dist x y"
immler@69675
  1189
      unfolding dist_norm
immler@69675
  1190
    proof (rule norm_eq)
immler@69675
  1191
      show "x = norm x *\<^sub>R (x /\<^sub>R norm x)" "y = norm y *\<^sub>R (y /\<^sub>R norm y)"
immler@69675
  1192
           "norm (f (x /\<^sub>R norm x)) = 1" "norm (f (y /\<^sub>R norm y)) = 1"
immler@69675
  1193
        using False f1 by auto
immler@69675
  1194
    qed (use False in \<open>auto simp: field_simps intro: f1 fd1[unfolded dist_norm]\<close>)
immler@69675
  1195
  qed (auto simp: f1)
immler@69675
  1196
  show ?thesis
immler@69675
  1197
    unfolding orthogonal_transformation_isometry
immler@69675
  1198
    by (rule exI[where x= ?g]) (metis thfg thd)
immler@69675
  1199
qed
immler@69675
  1200
immler@69683
  1201
subsection\<open>Induction on matrix row operations\<close>
immler@69675
  1202
ak2110@69723
  1203
lemma induct_matrix_row_operations:
immler@69675
  1204
  fixes P :: "real^'n^'n \<Rightarrow> bool"
immler@69675
  1205
  assumes zero_row: "\<And>A i. row i A = 0 \<Longrightarrow> P A"
immler@69675
  1206
    and diagonal: "\<And>A. (\<And>i j. i \<noteq> j \<Longrightarrow> A$i$j = 0) \<Longrightarrow> P A"
immler@69675
  1207
    and swap_cols: "\<And>A m n. \<lbrakk>P A; m \<noteq> n\<rbrakk> \<Longrightarrow> P(\<chi> i j. A $ i $ Fun.swap m n id j)"
immler@69675
  1208
    and row_op: "\<And>A m n c. \<lbrakk>P A; m \<noteq> n\<rbrakk>
immler@69675
  1209
                   \<Longrightarrow> P(\<chi> i. if i = m then row m A + c *\<^sub>R row n A else row i A)"
immler@69675
  1210
  shows "P A"
immler@69675
  1211
proof -
immler@69675
  1212
  have "P A" if "(\<And>i j. \<lbrakk>j \<in> -K;  i \<noteq> j\<rbrakk> \<Longrightarrow> A$i$j = 0)" for A K
immler@69675
  1213
  proof -
immler@69675
  1214
    have "finite K"
immler@69675
  1215
      by simp
immler@69675
  1216
    then show ?thesis using that
immler@69675
  1217
    proof (induction arbitrary: A rule: finite_induct)
immler@69675
  1218
      case empty
immler@69675
  1219
      with diagonal show ?case
immler@69675
  1220
        by simp
immler@69675
  1221
    next
immler@69675
  1222
      case (insert k K)
immler@69675
  1223
      note insertK = insert
immler@69675
  1224
      have "P A" if kk: "A$k$k \<noteq> 0"
immler@69675
  1225
        and 0: "\<And>i j. \<lbrakk>j \<in> - insert k K; i \<noteq> j\<rbrakk> \<Longrightarrow> A$i$j = 0"
immler@69675
  1226
               "\<And>i. \<lbrakk>i \<in> -L; i \<noteq> k\<rbrakk> \<Longrightarrow> A$i$k = 0" for A L
immler@69675
  1227
      proof -
immler@69675
  1228
        have "finite L"
immler@69675
  1229
          by simp
immler@69675
  1230
        then show ?thesis using 0 kk
immler@69675
  1231
        proof (induction arbitrary: A rule: finite_induct)
immler@69675
  1232
          case (empty B)
immler@69675
  1233
          show ?case
immler@69675
  1234
          proof (rule insertK)
immler@69675
  1235
            fix i j
immler@69675
  1236
            assume "i \<in> - K" "j \<noteq> i"
immler@69675
  1237
            show "B $ j $ i = 0"
immler@69675
  1238
              using \<open>j \<noteq> i\<close> \<open>i \<in> - K\<close> empty
immler@69675
  1239
              by (metis ComplD ComplI Compl_eq_Diff_UNIV Diff_empty UNIV_I insert_iff)
immler@69675
  1240
          qed
immler@69675
  1241
        next
immler@69675
  1242
          case (insert l L B)
immler@69675
  1243
          show ?case
immler@69675
  1244
          proof (cases "k = l")
immler@69675
  1245
            case True
immler@69675
  1246
            with insert show ?thesis
immler@69675
  1247
              by auto
immler@69675
  1248
          next
immler@69675
  1249
            case False
immler@69675
  1250
            let ?C = "\<chi> i. if i = l then row l B - (B $ l $ k / B $ k $ k) *\<^sub>R row k B else row i B"
immler@69675
  1251
            have 1: "\<lbrakk>j \<in> - insert k K; i \<noteq> j\<rbrakk> \<Longrightarrow> ?C $ i $ j = 0" for j i
immler@69675
  1252
              by (auto simp: insert.prems(1) row_def)
immler@69675
  1253
            have 2: "?C $ i $ k = 0"
immler@69675
  1254
              if "i \<in> - L" "i \<noteq> k" for i
immler@69675
  1255
            proof (cases "i=l")
immler@69675
  1256
              case True
immler@69675
  1257
              with that insert.prems show ?thesis
immler@69675
  1258
                by (simp add: row_def)
immler@69675
  1259
            next
immler@69675
  1260
              case False
immler@69675
  1261
              with that show ?thesis
immler@69675
  1262
                by (simp add: insert.prems(2) row_def)
immler@69675
  1263
            qed
immler@69675
  1264
            have 3: "?C $ k $ k \<noteq> 0"
immler@69675
  1265
              by (auto simp: insert.prems row_def \<open>k \<noteq> l\<close>)
immler@69675
  1266
            have PC: "P ?C"
immler@69675
  1267
              using insert.IH [OF 1 2 3] by auto
immler@69675
  1268
            have eqB: "(\<chi> i. if i = l then row l ?C + (B $ l $ k / B $ k $ k) *\<^sub>R row k ?C else row i ?C) = B"
immler@69675
  1269
              using \<open>k \<noteq> l\<close> by (simp add: vec_eq_iff row_def)
immler@69675
  1270
            show ?thesis
immler@69675
  1271
              using row_op [OF PC, of l k, where c = "B$l$k / B$k$k"] eqB \<open>k \<noteq> l\<close>
immler@69675
  1272
              by (simp add: cong: if_cong)
immler@69675
  1273
          qed
immler@69675
  1274
        qed
immler@69675
  1275
      qed
immler@69675
  1276
      then have nonzero_hyp: "P A"
immler@69675
  1277
        if kk: "A$k$k \<noteq> 0" and zeroes: "\<And>i j. j \<in> - insert k K \<and> i\<noteq>j \<Longrightarrow> A$i$j = 0" for A
immler@69675
  1278
        by (auto simp: intro!: kk zeroes)
immler@69675
  1279
      show ?case
immler@69675
  1280
      proof (cases "row k A = 0")
immler@69675
  1281
        case True
immler@69675
  1282
        with zero_row show ?thesis by auto
immler@69675
  1283
      next
immler@69675
  1284
        case False
immler@69675
  1285
        then obtain l where l: "A$k$l \<noteq> 0"
immler@69675
  1286
          by (auto simp: row_def zero_vec_def vec_eq_iff)
immler@69675
  1287
        show ?thesis
immler@69675
  1288
        proof (cases "k = l")
immler@69675
  1289
          case True
immler@69675
  1290
          with l nonzero_hyp insert.prems show ?thesis
immler@69675
  1291
            by blast
immler@69675
  1292
        next
immler@69675
  1293
          case False
immler@69675
  1294
          have *: "A $ i $ Fun.swap k l id j = 0" if "j \<noteq> k" "j \<notin> K" "i \<noteq> j" for i j
immler@69675
  1295
            using False l insert.prems that
immler@69675
  1296
            by (auto simp: swap_def insert split: if_split_asm)
immler@69675
  1297
          have "P (\<chi> i j. (\<chi> i j. A $ i $ Fun.swap k l id j) $ i $ Fun.swap k l id j)"
immler@69675
  1298
            by (rule swap_cols [OF nonzero_hyp False]) (auto simp: l *)
immler@69675
  1299
          moreover
immler@69675
  1300
          have "(\<chi> i j. (\<chi> i j. A $ i $ Fun.swap k l id j) $ i $ Fun.swap k l id j) = A"
immler@69675
  1301
            by (vector Fun.swap_def)
immler@69675
  1302
          ultimately show ?thesis
immler@69675
  1303
            by simp
immler@69675
  1304
        qed
immler@69675
  1305
      qed
immler@69675
  1306
    qed
immler@69675
  1307
  qed
immler@69675
  1308
  then show ?thesis
immler@69675
  1309
    by blast
immler@69675
  1310
qed
immler@69675
  1311
ak2110@69723
  1312
lemma induct_matrix_elementary:
immler@69675
  1313
  fixes P :: "real^'n^'n \<Rightarrow> bool"
immler@69675
  1314
  assumes mult: "\<And>A B. \<lbrakk>P A; P B\<rbrakk> \<Longrightarrow> P(A ** B)"
immler@69675
  1315
    and zero_row: "\<And>A i. row i A = 0 \<Longrightarrow> P A"
immler@69675
  1316
    and diagonal: "\<And>A. (\<And>i j. i \<noteq> j \<Longrightarrow> A$i$j = 0) \<Longrightarrow> P A"
immler@69675
  1317
    and swap1: "\<And>m n. m \<noteq> n \<Longrightarrow> P(\<chi> i j. mat 1 $ i $ Fun.swap m n id j)"
immler@69675
  1318
    and idplus: "\<And>m n c. m \<noteq> n \<Longrightarrow> P(\<chi> i j. if i = m \<and> j = n then c else of_bool (i = j))"
immler@69675
  1319
  shows "P A"
immler@69675
  1320
proof -
immler@69675
  1321
  have swap: "P (\<chi> i j. A $ i $ Fun.swap m n id j)"  (is "P ?C")
immler@69675
  1322
    if "P A" "m \<noteq> n" for A m n
immler@69675
  1323
  proof -
immler@69675
  1324
    have "A ** (\<chi> i j. mat 1 $ i $ Fun.swap m n id j) = ?C"
immler@69675
  1325
      by (simp add: matrix_matrix_mult_def mat_def vec_eq_iff if_distrib sum.delta_remove)
immler@69675
  1326
    then show ?thesis
immler@69675
  1327
      using mult swap1 that by metis
immler@69675
  1328
  qed
immler@69675
  1329
  have row: "P (\<chi> i. if i = m then row m A + c *\<^sub>R row n A else row i A)"  (is "P ?C")
immler@69675
  1330
    if "P A" "m \<noteq> n" for A m n c
immler@69675
  1331
  proof -
immler@69675
  1332
    let ?B = "\<chi> i j. if i = m \<and> j = n then c else of_bool (i = j)"
immler@69675
  1333
    have "?B ** A = ?C"
immler@69675
  1334
      using \<open>m \<noteq> n\<close> unfolding matrix_matrix_mult_def row_def of_bool_def
immler@69675
  1335
      by (auto simp: vec_eq_iff if_distrib [of "\<lambda>x. x * y" for y] sum.remove cong: if_cong)
immler@69675
  1336
    then show ?thesis
immler@69675
  1337
      by (rule subst) (auto simp: that mult idplus)
immler@69675
  1338
  qed
immler@69675
  1339
  show ?thesis
immler@69675
  1340
    by (rule induct_matrix_row_operations [OF zero_row diagonal swap row])
immler@69675
  1341
qed
immler@69675
  1342
ak2110@69723
  1343
lemma induct_matrix_elementary_alt:
immler@69675
  1344
  fixes P :: "real^'n^'n \<Rightarrow> bool"
immler@69675
  1345
  assumes mult: "\<And>A B. \<lbrakk>P A; P B\<rbrakk> \<Longrightarrow> P(A ** B)"
immler@69675
  1346
    and zero_row: "\<And>A i. row i A = 0 \<Longrightarrow> P A"
immler@69675
  1347
    and diagonal: "\<And>A. (\<And>i j. i \<noteq> j \<Longrightarrow> A$i$j = 0) \<Longrightarrow> P A"
immler@69675
  1348
    and swap1: "\<And>m n. m \<noteq> n \<Longrightarrow> P(\<chi> i j. mat 1 $ i $ Fun.swap m n id j)"
immler@69675
  1349
    and idplus: "\<And>m n. m \<noteq> n \<Longrightarrow> P(\<chi> i j. of_bool (i = m \<and> j = n \<or> i = j))"
immler@69675
  1350
  shows "P A"
immler@69675
  1351
proof -
immler@69675
  1352
  have *: "P (\<chi> i j. if i = m \<and> j = n then c else of_bool (i = j))"
immler@69675
  1353
    if "m \<noteq> n" for m n c
immler@69675
  1354
  proof (cases "c = 0")
immler@69675
  1355
    case True
immler@69675
  1356
    with diagonal show ?thesis by auto
immler@69675
  1357
  next
immler@69675
  1358
    case False
immler@69675
  1359
    then have eq: "(\<chi> i j. if i = m \<and> j = n then c else of_bool (i = j)) =
immler@69675
  1360
                      (\<chi> i j. if i = j then (if j = n then inverse c else 1) else 0) **
immler@69675
  1361
                      (\<chi> i j. of_bool (i = m \<and> j = n \<or> i = j)) **
immler@69675
  1362
                      (\<chi> i j. if i = j then if j = n then c else 1 else 0)"
immler@69675
  1363
      using \<open>m \<noteq> n\<close>
immler@69675
  1364
      apply (simp add: matrix_matrix_mult_def vec_eq_iff of_bool_def if_distrib [of "\<lambda>x. y * x" for y] cong: if_cong)
immler@69675
  1365
      apply (simp add: if_if_eq_conj sum.neutral conj_commute cong: conj_cong)
immler@69675
  1366
      done
immler@69675
  1367
    show ?thesis
immler@69675
  1368
      apply (subst eq)
immler@69675
  1369
      apply (intro mult idplus that)
immler@69675
  1370
       apply (auto intro: diagonal)
immler@69675
  1371
      done
immler@69675
  1372
  qed
immler@69675
  1373
  show ?thesis
immler@69675
  1374
    by (rule induct_matrix_elementary) (auto intro: assms *)
immler@69675
  1375
qed
immler@69675
  1376
ak2110@69723
  1377
lemma matrix_vector_mult_matrix_matrix_mult_compose:
immler@69675
  1378
  "(*v) (A ** B) = (*v) A \<circ> (*v) B"
immler@69675
  1379
  by (auto simp: matrix_vector_mul_assoc)
immler@69675
  1380
ak2110@69723
  1381
lemma induct_linear_elementary:
immler@69675
  1382
  fixes f :: "real^'n \<Rightarrow> real^'n"
immler@69675
  1383
  assumes "linear f"
immler@69675
  1384
    and comp: "\<And>f g. \<lbrakk>linear f; linear g; P f; P g\<rbrakk> \<Longrightarrow> P(f \<circ> g)"
immler@69675
  1385
    and zeroes: "\<And>f i. \<lbrakk>linear f; \<And>x. (f x) $ i = 0\<rbrakk> \<Longrightarrow> P f"
immler@69675
  1386
    and const: "\<And>c. P(\<lambda>x. \<chi> i. c i * x$i)"
immler@69675
  1387
    and swap: "\<And>m n::'n. m \<noteq> n \<Longrightarrow> P(\<lambda>x. \<chi> i. x $ Fun.swap m n id i)"
immler@69675
  1388
    and idplus: "\<And>m n::'n. m \<noteq> n \<Longrightarrow> P(\<lambda>x. \<chi> i. if i = m then x$m + x$n else x$i)"
immler@69675
  1389
  shows "P f"
immler@69675
  1390
proof -
immler@69675
  1391
  have "P ((*v) A)" for A
immler@69675
  1392
  proof (rule induct_matrix_elementary_alt)
immler@69675
  1393
    fix A B
immler@69675
  1394
    assume "P ((*v) A)" and "P ((*v) B)"
immler@69675
  1395
    then show "P ((*v) (A ** B))"
immler@69675
  1396
      by (auto simp add: matrix_vector_mult_matrix_matrix_mult_compose matrix_vector_mul_linear
immler@69675
  1397
          intro!: comp)
immler@69675
  1398
  next
immler@69675
  1399
    fix A :: "real^'n^'n" and i
immler@69675
  1400
    assume "row i A = 0"
immler@69675
  1401
    show "P ((*v) A)"
immler@69675
  1402
      using matrix_vector_mul_linear
immler@69675
  1403
      by (rule zeroes[where i=i])
immler@69675
  1404
        (metis \<open>row i A = 0\<close> inner_zero_left matrix_vector_mul_component row_def vec_lambda_eta)
immler@69675
  1405
  next
immler@69675
  1406
    fix A :: "real^'n^'n"
immler@69675
  1407
    assume 0: "\<And>i j. i \<noteq> j \<Longrightarrow> A $ i $ j = 0"
immler@69675
  1408
    have "A $ i $ i * x $ i = (\<Sum>j\<in>UNIV. A $ i $ j * x $ j)" for x and i :: "'n"
immler@69675
  1409
      by (simp add: 0 comm_monoid_add_class.sum.remove [where x=i])
immler@69675
  1410
    then have "(\<lambda>x. \<chi> i. A $ i $ i * x $ i) = ((*v) A)"
immler@69675
  1411
      by (auto simp: 0 matrix_vector_mult_def)
immler@69675
  1412
    then show "P ((*v) A)"
immler@69675
  1413
      using const [of "\<lambda>i. A $ i $ i"] by simp
immler@69675
  1414
  next
immler@69675
  1415
    fix m n :: "'n"
immler@69675
  1416
    assume "m \<noteq> n"
immler@69675
  1417
    have eq: "(\<Sum>j\<in>UNIV. if i = Fun.swap m n id j then x $ j else 0) =
immler@69675
  1418
              (\<Sum>j\<in>UNIV. if j = Fun.swap m n id i then x $ j else 0)"
immler@69675
  1419
      for i and x :: "real^'n"
immler@69675
  1420
      unfolding swap_def by (rule sum.cong) auto
immler@69675
  1421
    have "(\<lambda>x::real^'n. \<chi> i. x $ Fun.swap m n id i) = ((*v) (\<chi> i j. if i = Fun.swap m n id j then 1 else 0))"
immler@69675
  1422
      by (auto simp: mat_def matrix_vector_mult_def eq if_distrib [of "\<lambda>x. x * y" for y] cong: if_cong)
immler@69675
  1423
    with swap [OF \<open>m \<noteq> n\<close>] show "P ((*v) (\<chi> i j. mat 1 $ i $ Fun.swap m n id j))"
immler@69675
  1424
      by (simp add: mat_def matrix_vector_mult_def)
immler@69675
  1425
  next
immler@69675
  1426
    fix m n :: "'n"
immler@69675
  1427
    assume "m \<noteq> n"
immler@69675
  1428
    then have "x $ m + x $ n = (\<Sum>j\<in>UNIV. of_bool (j = n \<or> m = j) * x $ j)" for x :: "real^'n"
immler@69675
  1429
      by (auto simp: of_bool_def if_distrib [of "\<lambda>x. x * y" for y] sum.remove cong: if_cong)
immler@69675
  1430
    then have "(\<lambda>x::real^'n. \<chi> i. if i = m then x $ m + x $ n else x $ i) =
immler@69675
  1431
               ((*v) (\<chi> i j. of_bool (i = m \<and> j = n \<or> i = j)))"
immler@69675
  1432
      unfolding matrix_vector_mult_def of_bool_def
immler@69675
  1433
      by (auto simp: vec_eq_iff if_distrib [of "\<lambda>x. x * y" for y] cong: if_cong)
immler@69675
  1434
    then show "P ((*v) (\<chi> i j. of_bool (i = m \<and> j = n \<or> i = j)))"
immler@69675
  1435
      using idplus [OF \<open>m \<noteq> n\<close>] by simp
immler@69675
  1436
  qed
immler@69675
  1437
  then show ?thesis
immler@69675
  1438
    by (metis \<open>linear f\<close> matrix_vector_mul)
immler@69675
  1439
qed
immler@69675
  1440
immler@68072
  1441
end