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