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