diff -r 37abfe400ae6 -r b22f39c54e8c src/HOL/Analysis/Cartesian_Space.thy --- a/src/HOL/Analysis/Cartesian_Space.thy Fri Aug 04 19:17:49 2023 +0200 +++ b/src/HOL/Analysis/Cartesian_Space.thy Sun Aug 06 18:29:09 2023 +0100 @@ -30,70 +30,66 @@ interpretation vec: vector_space "(*s) " by unfold_locales (vector algebra_simps)+ -lemma independent_cart_basis: - "vec.independent (cart_basis)" +lemma independent_cart_basis: "vec.independent (cart_basis)" proof (rule vec.independent_if_scalars_zero) show "finite (cart_basis)" using finite_cart_basis . fix f::"('a, 'b) vec \ 'a" and x::"('a, 'b) vec" assume eq_0: "(\x\cart_basis. f x *s x) = 0" and x_in: "x \ cart_basis" obtain i where x: "x = axis i 1" using x_in unfolding cart_basis_def by auto have sum_eq_0: "(\x\(cart_basis) - {x}. f x * (x $ i)) = 0" - proof (rule sum.neutral, rule ballI) - fix xa assume xa: "xa \ cart_basis - {x}" - obtain a where a: "xa = axis a 1" and a_not_i: "a \ i" - using xa x unfolding cart_basis_def by auto - have "xa $ i = 0" unfolding a axis_def using a_not_i by auto - thus "f xa * xa $ i = 0" by simp + proof (intro sum.neutral ballI) + fix y assume y: "y \ cart_basis - {x}" + obtain a where a: "y = axis a 1" and a_not_i: "a \ i" + using y x unfolding cart_basis_def by auto + have "y $ i = 0" unfolding a axis_def using a_not_i by auto + thus "f y * y $ i = 0" by simp qed have "0 = (\x\cart_basis. f x *s x) $ i" using eq_0 by simp - also have "... = (\x\cart_basis. (f x *s x) $ i)" unfolding sum_component .. - also have "... = (\x\cart_basis. f x * (x $ i))" unfolding vector_smult_component .. - also have "... = f x * (x $ i) + (\x\(cart_basis) - {x}. f x * (x $ i))" + also have "\ = (\x\cart_basis. (f x *s x) $ i)" unfolding sum_component .. + also have "\ = (\x\cart_basis. f x * (x $ i))" unfolding vector_smult_component .. + also have "\ = f x * (x $ i) + (\x\(cart_basis) - {x}. f x * (x $ i))" by (rule sum.remove[OF finite_cart_basis x_in]) - also have "... = f x * (x $ i)" unfolding sum_eq_0 by simp - also have "... = f x" unfolding x axis_def by auto + also have "\ = f x * (x $ i)" unfolding sum_eq_0 by simp + also have "\ = f x" unfolding x axis_def by auto finally show "f x = 0" .. qed -lemma span_cart_basis: - "vec.span (cart_basis) = UNIV" -proof (auto) - fix x::"('a, 'b) vec" - let ?f="\v. x $ (THE i. v = axis i 1)" - show "x \ vec.span (cart_basis)" - apply (unfold vec.span_finite[OF finite_cart_basis]) - apply (rule image_eqI[of _ _ ?f]) - apply (subst vec_eq_iff) - apply clarify +lemma span_cart_basis [simp]: "vec.span (cart_basis) = UNIV" +proof - + have "x \ vec.span cart_basis" for x :: "('a, 'b) vec" proof - - fix i::'b - let ?w = "axis i (1::'a)" - have the_eq_i: "(THE a. ?w = axis a 1) = i" - by (rule the_equality, auto simp: axis_eq_axis) - have sum_eq_0: "(\v\(cart_basis) - {?w}. x $ (THE i. v = axis i 1) * v $ i) = 0" - proof (rule sum.neutral, rule ballI) - fix xa::"('a, 'b) vec" - assume xa: "xa \ cart_basis - {?w}" - obtain j where j: "xa = axis j 1" and i_not_j: "i \ j" using xa unfolding cart_basis_def by auto - have the_eq_j: "(THE i. xa = axis i 1) = j" - proof (rule the_equality) - show "xa = axis j 1" using j . - show "\i. xa = axis i 1 \ i = j" by (metis axis_eq_axis j zero_neq_one) + let ?f="\v. x $ (THE i. v = axis i 1)" + have "x $ i = (\v\cart_basis. x $ (THE i. v = axis i 1) *s v) $ i" for i::'b + proof - + let ?w = "axis i (1::'a)" + have the_eq_i: "(THE a. ?w = axis a 1) = i" + by (rule the_equality, auto simp: axis_eq_axis) + have sum_eq_0: "(\v\(cart_basis) - {?w}. x $ (THE i. v = axis i 1) * v $ i) = 0" + proof (intro sum.neutral ballI) + fix y:: "('a, 'b) vec" + assume y: "y \ cart_basis - {?w}" + obtain j where j: "y = axis j 1" and i_not_j: "i \ j" + using y unfolding cart_basis_def by auto + have the_eq_j: "(THE i. y = axis i 1) = j" + by (simp add: axis_eq_axis j) + show "x $ (THE i. y = axis i 1) * y $ i = 0" + by (simp add: axis_def i_not_j j) qed - show "x $ (THE i. xa = axis i 1) * xa $ i = 0" - apply (subst (2) j) - unfolding the_eq_j unfolding axis_def using i_not_j by simp + have "(\v\cart_basis. x $ (THE i. v = axis i 1) *s v) $ i + = (\v\cart_basis. x $ (THE i. v = axis i 1) * v $ i)" + by force + also have "\ = x $ (THE a. ?w = axis a 1) * ?w $ i + (\v\(cart_basis) - {?w}. x $ (THE i. v = axis i 1) * v $ i)" + by (rule sum.remove[OF finite_cart_basis], auto simp add: cart_basis_def) + also have "\ = x $ (THE a. ?w = axis a 1) * ?w $ i" + unfolding sum_eq_0 by simp + also have "\ = x $ i" + unfolding the_eq_i unfolding axis_def by auto + finally show ?thesis by simp qed - have "(\v\cart_basis. x $ (THE i. v = axis i 1) *s v) $ i = - (\v\cart_basis. (x $ (THE i. v = axis i 1) *s v) $ i)" unfolding sum_component .. - also have "... = (\v\cart_basis. x $ (THE i. v = axis i 1) * v $ i)" - unfolding vector_smult_component .. - also have "... = x $ (THE a. ?w = axis a 1) * ?w $ i + (\v\(cart_basis) - {?w}. x $ (THE i. v = axis i 1) * v $ i)" - by (rule sum.remove[OF finite_cart_basis], auto simp add: cart_basis_def) - also have "... = x $ (THE a. ?w = axis a 1) * ?w $ i" unfolding sum_eq_0 by simp - also have "... = x $ i" unfolding the_eq_i unfolding axis_def by auto - finally show "x $ i = (\v\cart_basis. x $ (THE i. v = axis i 1) *s v) $ i" by simp - qed simp + then show "x \ vec.span (cart_basis)" + by (metis (no_types, lifting) vec.span_base vec.span_scale vec.span_sum vec_eq_iff) + qed + then show ?thesis by auto qed (*Some interpretations:*) @@ -138,10 +134,12 @@ lemma matrix_works: assumes lf: "Vector_Spaces.linear (*s) (*s) f" shows "matrix f *v x = f (x::'a::field ^ 'n)" - apply (simp add: matrix_def matrix_vector_mult_def vec_eq_iff mult.commute) - apply clarify - apply (rule linear_componentwise[OF lf, symmetric]) - done +proof - + have "\i. (\j\UNIV. x $ j * f (axis j 1) $ i) = f x $ i" + by (simp add: Cartesian_Space.linear_componentwise lf) + then show ?thesis + by (simp add: matrix_def matrix_vector_mult_def vec_eq_iff mult.commute) +qed lemma matrix_of_matrix_vector_mul[simp]: "matrix(\x. A *v (x :: 'a::field ^ 'n)) = A" by (simp add: matrix_eq matrix_works) @@ -190,44 +188,27 @@ next assume "inj ((*v) A)" from vec.linear_injective_left_inverse[OF matrix_vector_mul_linear_gen this] - obtain g where "Vector_Spaces.linear (*s) (*s) g" and g: "g \ (*v) A = id" + obtain g where "Vector_Spaces.linear (*s) (*s) g" and "g \ (*v) A = id" by blast - have "matrix g ** A = mat 1" - by (metis matrix_vector_mul_linear_gen \Vector_Spaces.linear (*s) (*s) g\ g matrix_compose_gen - matrix_eq matrix_id_mat_1 matrix_vector_mul(1)) + then have "matrix g ** A = mat 1" + by (metis matrix_compose_gen matrix_id_mat_1 matrix_of_matrix_vector_mul vec.linear_axioms) then show "\B. B ** A = mat 1" by metis qed lemma matrix_left_invertible_ker: "(\B. (B::'a::{field} ^'m^'n) ** (A::'a::{field}^'n^'m) = mat 1) \ (\x. A *v x = 0 \ x = 0)" - unfolding matrix_left_invertible_injective - using vec.inj_on_iff_eq_0[OF vec.subspace_UNIV, of A] - by (simp add: inj_on_def) + by (simp add: matrix_left_invertible_injective vec.inj_iff_eq_0) lemma matrix_right_invertible_surjective: "(\B. (A::'a::field^'n^'m) ** (B::'a::field^'m^'n) = mat 1) \ surj (\x. A *v x)" proof - - { fix B :: "'a ^'m^'n" - assume AB: "A ** B = mat 1" - { fix x :: "'a ^ 'm" - have "A *v (B *v x) = x" - by (simp add: matrix_vector_mul_assoc AB) } - hence "surj ((*v) A)" unfolding surj_def by metis } - moreover - { assume sf: "surj ((*v) A)" - from vec.linear_surjective_right_inverse[OF _ this] - obtain g:: "'a ^'m \ 'a ^'n" where g: "Vector_Spaces.linear (*s) (*s) g" "(*v) A \ g = id" - by blast - - have "A ** (matrix g) = mat 1" - unfolding matrix_eq matrix_vector_mul_lid - matrix_vector_mul_assoc[symmetric] matrix_works[OF g(1)] - using g(2) unfolding o_def fun_eq_iff id_def - . - hence "\B. A ** (B::'a^'m^'n) = mat 1" by blast - } - ultimately show ?thesis unfolding surj_def by blast + have "\B x. A ** B = mat 1 \ \y. x = A *v y" + by (metis matrix_vector_mul_assoc matrix_vector_mul_lid) + moreover have "\x. \xa. x = A *v xa \ \B. A ** B = mat 1" + by (metis (mono_tags, lifting) matrix_compose_gen matrix_id_mat_1 matrix_of_matrix_vector_mul surj_def vec.linear_axioms vec.linear_surjective_right_inverse) + ultimately show ?thesis + by (auto simp: image_def set_eq_iff) qed lemma matrix_left_invertible_independent_columns: @@ -237,33 +218,20 @@ (is "?lhs \ ?rhs") proof - let ?U = "UNIV :: 'n set" - { assume k: "\x. A *v x = 0 \ x = 0" - { fix c i - assume c: "sum (\i. c i *s column i A) ?U = 0" and i: "i \ ?U" - let ?x = "\ i. c i" - have th0:"A *v ?x = 0" - using c - by (vector matrix_mult_sum) - from k[rule_format, OF th0] i - have "c i = 0" by (vector vec_eq_iff)} - hence ?rhs by blast } - moreover - { assume H: ?rhs - { fix x assume x: "A *v x = 0" - let ?c = "\i. ((x$i ):: 'a)" - from H[rule_format, of ?c, unfolded matrix_mult_sum[symmetric], OF x] - have "x = 0" by vector } - } - ultimately show ?thesis unfolding matrix_left_invertible_ker by auto + have "c i = 0" + if "\x. A *v x = 0 \ x = 0" "sum (\i. c i *s column i A) ?U = 0" for c i + by (metis (no_types) UNIV_I matrix_mult_sum vec_lambda_eta vec_nth_cases zero_vec_def that) + moreover have "x = 0" if "A *v x = 0" ?rhs for x + by (metis (full_types) matrix_mult_sum that vec_eq_iff zero_index) + ultimately show ?thesis + unfolding matrix_left_invertible_ker by auto qed lemma matrix_right_invertible_independent_rows: fixes A :: "'a::{field}^'n^'m" shows "(\(B::'a^'m^'n). A ** B = mat 1) \ - (\c. sum (\i. c i *s row i A) (UNIV :: 'm set) = 0 \ (\i. c i = 0))" - unfolding left_invertible_transpose[symmetric] - matrix_left_invertible_independent_columns - by (simp add:) + (\c. sum (\i::'m. c i *s row i A) UNIV = 0 \ (\i. c i = 0))" + by (simp add: matrix_left_invertible_independent_columns flip: left_invertible_transpose) lemma matrix_right_invertible_span_columns: "(\(B::'a::field ^'n^'m). (A::'a ^'m^'n) ** B = mat 1) \ @@ -277,14 +245,10 @@ have rhseq: "?rhs \ (\x. x \ vec.span (columns A))" by blast { assume h: ?lhs { fix x:: "'a ^'n" - from h[unfolded lhseq, rule_format, of x] obtain y :: "'a ^'m" - where y: "sum (\i. (y$i) *s column i A) ?U = x" by blast - have "x \ vec.span (columns A)" - unfolding y[symmetric] scalar_mult_eq_scaleR - proof (rule vec.span_sum [OF vec.span_scale]) - show "column i A \ vec.span (columns A)" for i - using columns_def vec.span_superset by auto - qed + obtain y :: "'a ^'m" where y: "sum (\i. (y$i) *s column i A) ?U = x" + using h lhseq by blast + then have "x \ vec.span (columns A)" + by (metis (mono_tags, lifting) columns_def mem_Collect_eq vec.span_base vec.span_scale vec.span_sum) } then have ?rhs unfolding rhseq by blast } moreover @@ -313,14 +277,14 @@ using i(1) by (simp add: field_simps) have "sum (\xa. if xa = i then (c + (x$i)) * ((column xa A)$j) else (x$xa) * ((column xa A$j))) ?U = sum (\xa. (if xa = i then c * ((column i A)$j) else 0) + ((x$xa) * ((column xa A)$j))) ?U" - by (rule sum.cong[OF refl]) (use th in blast) + using th by force also have "\ = sum (\xa. if xa = i then c * ((column i A)$j) else 0) ?U + sum (\xa. ((x$xa) * ((column xa A)$j))) ?U" by (simp add: sum.distrib) also have "\ = c * ((column i A)$j) + sum (\xa. ((x$xa) * ((column xa A)$j))) ?U" - unfolding sum.delta[OF fU] - using i(1) by simp + unfolding sum.delta[OF fU] using i(1) by simp finally show "sum (\xa. if xa = i then (c + (x$i)) * ((column xa A)$j) - else (x$xa) * ((column xa A$j))) ?U = c * ((column i A)$j) + sum (\xa. ((x$xa) * ((column xa A)$j))) ?U" . + else (x$xa) * ((column xa A$j))) ?U + = c * ((column i A)$j) + sum (\xa. ((x$xa) * ((column xa A)$j))) ?U" . qed qed } @@ -331,10 +295,7 @@ lemma matrix_left_invertible_span_rows_gen: "(\(B::'a^'m^'n). B ** (A::'a::field^'n^'m) = mat 1) \ vec.span (rows A) = UNIV" - unfolding right_invertible_transpose[symmetric] - unfolding columns_transpose[symmetric] - unfolding matrix_right_invertible_span_columns - .. + by (metis columns_transpose matrix_right_invertible_span_columns right_invertible_transpose) lemma matrix_left_invertible_span_rows: "(\(B::real^'m^'n). B ** (A::real^'n^'m) = mat 1) \ span (rows A) = UNIV" @@ -348,17 +309,13 @@ assume AA': "A ** A' = mat 1" have sA: "surj ((*v) A)" using AA' matrix_right_invertible_surjective by auto - from vec.linear_surjective_isomorphism[OF matrix_vector_mul_linear_gen sA] obtain f' :: "'a ^'n \ 'a ^'n" - where f': "Vector_Spaces.linear (*s) (*s) f'" "\x. f' (A *v x) = x" "\x. A *v f' x = x" by blast - have th: "matrix f' ** A = mat 1" - by (simp add: matrix_eq matrix_works[OF f'(1)] - matrix_vector_mul_assoc[symmetric] f'(2)[rule_format]) - hence "(matrix f' ** A) ** A' = mat 1 ** A'" by simp - hence "matrix f' = A'" - by (simp add: matrix_mul_assoc[symmetric] AA') - hence "matrix f' ** A = A' ** A" by simp - hence "A' ** A = mat 1" by (simp add: th) + where f': "Vector_Spaces.linear (*s) (*s) f'" "\x. f' (A *v x) = x" "\x. A *v f' x = x" + using sA vec.linear_surjective_isomorphism by blast + have "matrix f' ** A = mat 1" + by (metis f' matrix_eq matrix_vector_mul_assoc matrix_vector_mul_lid matrix_works) + hence "A' ** A = mat 1" + by (metis AA' matrix_mul_assoc matrix_mul_lid) } then show ?thesis by blast qed @@ -382,22 +339,12 @@ using inv_A unfolding invertible_def by blast obtain B' where BB': "B ** B' = mat 1" and B'B: "B' ** B = mat 1" using inv_B unfolding invertible_def by blast - show ?thesis - proof (unfold invertible_def, rule exI[of _ "B'**A'"], rule conjI) - have "A ** B ** (B' ** A') = A ** (B ** (B' ** A'))" - using matrix_mul_assoc[of A B "(B' ** A')", symmetric] . - also have "... = A ** (B ** B' ** A')" unfolding matrix_mul_assoc[of B "B'" "A'"] .. - also have "... = A ** (mat 1 ** A')" unfolding BB' .. - also have "... = A ** A'" unfolding matrix_mul_lid .. - also have "... = mat 1" unfolding AA' .. - finally show "A ** B ** (B' ** A') = mat (1::'a)" . - have "B' ** A' ** (A ** B) = B' ** (A' ** (A ** B))" using matrix_mul_assoc[of B' A' "(A ** B)", symmetric] . - also have "... = B' ** (A' ** A ** B)" unfolding matrix_mul_assoc[of A' A B] .. - also have "... = B' ** (mat 1 ** B)" unfolding A'A .. - also have "... = B' ** B" unfolding matrix_mul_lid .. - also have "... = mat 1" unfolding B'B .. - finally show "B' ** A' ** (A ** B) = mat 1" . - qed + have "A ** B ** (B' ** A') = mat 1" + by (metis AA' BB' matrix_mul_assoc matrix_mul_rid) + moreover have "B' ** A' ** (A ** B) = mat 1" + by (metis A'A B'B matrix_mul_assoc matrix_mul_rid) + ultimately show ?thesis + using invertible_def by blast qed lemma transpose_invertible: @@ -409,12 +356,7 @@ lemma vector_matrix_mul_assoc: fixes v :: "('a::comm_semiring_1)^'n" shows "(v v* M) v* N = v v* (M ** N)" -proof - - from matrix_vector_mul_assoc - have "transpose N *v (transpose M *v v) = (transpose N ** transpose M) *v v" by fast - thus "(v v* M) v* N = v v* (M ** N)" - by (simp add: matrix_transpose_mul [symmetric]) -qed + by (metis (no_types, opaque_lifting) matrix_transpose_mul matrix_vector_mul_assoc transpose_matrix_vector) lemma matrix_scaleR_vector_ac: fixes A :: "real^('m::finite)^'n" @@ -426,8 +368,7 @@ shows "k *\<^sub>R (A *v v) = k *\<^sub>R A *v v" by (metis matrix_scaleR_vector_ac matrix_vector_mult_scaleR) -(*Finally, some interesting theorems and interpretations that don't appear in any file of the - library.*) +subsection \Some interesting theorems and interpretations\ locale linear_first_finite_dimensional_vector_space = l?: Vector_Spaces.linear scaleB scaleC f + @@ -438,25 +379,10 @@ and f :: "('b=>'c)" lemma vec_dim_card: "vec.dim (UNIV::('a::{field}^'n) set) = CARD ('n)" -proof - - let ?f="\i::'n. axis i (1::'a)" - have "vec.dim (UNIV::('a::{field}^'n) set) = card (cart_basis::('a^'n) set)" - unfolding vec.dim_UNIV .. - also have "... = card ({i. i\ UNIV}::('n) set)" - proof (rule bij_betw_same_card[of ?f, symmetric], unfold bij_betw_def, auto) - show "inj (\i::'n. axis i (1::'a))" by (simp add: inj_on_def axis_eq_axis) - fix i::'n - show "axis i 1 \ cart_basis" unfolding cart_basis_def by auto - fix x::"'a^'n" - assume "x \ cart_basis" - thus "x \ range (\i. axis i 1)" unfolding cart_basis_def by auto - qed - also have "... = CARD('n)" by auto - finally show ?thesis . -qed + by (simp add: card_cart_basis) interpretation vector_space_over_itself: vector_space "(*) :: 'a::field \ 'a \ 'a" -by unfold_locales (simp_all add: algebra_simps) + by unfold_locales (simp_all add: algebra_simps) lemmas [simp del] = vector_space_over_itself.scale_scale @@ -484,24 +410,12 @@ by (simp add: matrix_vector_mult_def inner_vec_def) lemma adjoint_matrix: "adjoint(\x. (A::real^'n^'m) *v x) = (\x. transpose A *v x)" - apply (rule adjoint_unique) - apply (simp add: transpose_def inner_vec_def matrix_vector_mult_def - sum_distrib_right sum_distrib_left) - apply (subst sum.swap) - apply (simp add: ac_simps) - done + by (metis adjoint_unique dot_lmul_matrix vector_transpose_matrix) -lemma matrix_adjoint: assumes lf: "linear (f :: real^'n \ real ^'m)" +lemma matrix_adjoint: + assumes lf: "linear (f :: real^'n \ real ^'m)" shows "matrix(adjoint f) = transpose(matrix f)" -proof - - have "matrix(adjoint f) = matrix(adjoint ((*v) (matrix f)))" - by (simp add: lf) - also have "\ = transpose(matrix f)" - unfolding adjoint_matrix matrix_of_matrix_vector_mul - apply rule - done - finally show ?thesis . -qed + by (metis adjoint_matrix assms matrix_of_matrix_vector_mul matrix_vector_mul(2)) subsection\ Rank of a matrix\ @@ -511,10 +425,8 @@ lemma matrix_vector_mult_in_columnspace_gen: fixes A :: "'a::field^'n^'m" shows "(A *v x) \ vec.span(columns A)" - apply (simp add: matrix_vector_column columns_def transpose_def column_def) - apply (intro vec.span_sum vec.span_scale) - apply (force intro: vec.span_base) - done + unfolding columns_def + by (metis (mono_tags, lifting) matrix_mult_sum mem_Collect_eq vec.span_base vec.span_scale vec.span_sum) lemma matrix_vector_mult_in_columnspace: fixes A :: "real^'n^'m" @@ -576,9 +488,7 @@ then have ind: "independent ((*v) A ` B)" by (rule linear_independent_injective_image [OF Finite_Cartesian_Product.matrix_vector_mul_linear \independent B\]) have "dim (span (rows A)) \ card ((*v) A ` B)" - unfolding B(2)[symmetric] - using inj - by (auto simp: card_image inj_on_subset span_superset) + by (metis B(2) card_image inj inj_on_subset order.refl span_superset) also have "\ \ dim (span (columns A))" using _ ind by (rule independent_card_le_dim) (auto intro!: matrix_vector_mult_in_columnspace) @@ -613,13 +523,7 @@ fixes A :: "real^'n^'m" shows "rank A = dim(range (\x. A *v x))" unfolding column_rank_def -proof (rule span_eq_dim) - have "span (columns A) \ span (range ((*v) A))" (is "?l \ ?r") - by (simp add: columns_image_basis image_subsetI span_mono) - then show "?l = ?r" - by (metis (no_types, lifting) image_subset_iff matrix_vector_mult_in_columnspace - span_eq span_span) -qed + by (smt (verit, best) columns_image_basis dim_span image_subset_iff iso_tuple_UNIV_I matrix_vector_mult_in_columnspace span_eq) lemma rank_bound: fixes A :: "real^'n^'m" @@ -636,8 +540,7 @@ lemma full_rank_surjective: fixes A :: "real^'n^'m" shows "rank A = CARD('m) \ surj ((*v) A)" - by (simp add: matrix_right_invertible_surjective [symmetric] left_invertible_transpose [symmetric] - matrix_left_invertible_injective full_rank_injective [symmetric] rank_transpose) + by (metis (no_types, opaque_lifting) dim_eq_full dim_vec_eq rank_dim_range span_vec_eq vec.span_UNIV vec.span_image vec_dim_card) lemma rank_I: "rank(mat 1::real^'n^'n) = CARD('n)" by (simp add: full_rank_injective inj_on_def) @@ -645,7 +548,7 @@ lemma less_rank_noninjective: fixes A :: "real^'n^'m" shows "rank A < CARD('n) \ \ inj ((*v) A)" -using less_le rank_bound by (auto simp: full_rank_injective [symmetric]) + using less_le rank_bound by (auto simp: full_rank_injective [symmetric]) lemma matrix_nonfull_linear_equations_eq: fixes A :: "real^'n^'m" @@ -680,9 +583,10 @@ shows "x = 1 \ x = 2" proof (induct x) case (of_int z) - then have "0 \ z" and "z < 2" by simp_all - then have "z = 0 | z = 1" by arith - then show ?case by auto + then have "z = 0 | z = 1" + by fastforce + then show ?case + by auto qed lemma forall_2: "(\i::2. P i) \ P 1 \ P 2" @@ -693,8 +597,7 @@ shows "x = 1 \ x = 2 \ x = 3" proof (induct x) case (of_int z) - then have "0 \ z" and "z < 3" by simp_all - then have "z = 0 \ z = 1 \ z = 2" by arith + then have "z = 0 \ z = 1 \ z = 2" by fastforce then show ?case by auto qed @@ -706,8 +609,7 @@ shows "x = 1 \ x = 2 \ x = 3 \ x = 4" proof (induct x) case (of_int z) - then have "0 \ z" and "z < 4" by simp_all - then have "z = 0 \ z = 1 \ z = 2 \ z = 3" by arith + then have "z = 0 \ z = 1 \ z = 2 \ z = 3" by fastforce then show ?case by auto qed @@ -744,10 +646,7 @@ by (simp add: vec_eq_iff) lemma forall_one: "(\(x::'a ^1). P x) \ (\x. P(\ i. x))" - apply auto - apply (erule_tac x= "x$1" in allE) - apply (simp only: vector_one[symmetric]) - done + by (metis vector_one) lemma norm_vector_1: "norm (x :: _^1) = norm (x$1)" by (simp add: norm_vec_def) @@ -791,7 +690,7 @@ shows "((\x. vec (g (x $ 1))) has_derivative (*\<^sub>R) (g' a)) (at ((vec a)::real^1) within vec ` S)" using der_g - apply (auto simp: Deriv.has_derivative_within bounded_linear_scaleR_right norm_vector_1) + apply (clarsimp simp: Deriv.has_derivative_within bounded_linear_scaleR_right norm_vector_1) apply (drule tendsto_at_within_vector_1, vector) apply (auto simp: algebra_simps eventually_at tendsto_def) done @@ -817,46 +716,33 @@ by (metis vector_1 vector_one) lemma forall_vector_2: "(\v::'a::zero^2. P v) \ (\x y. P(vector[x, y]))" - apply auto - apply (erule_tac x="v$1" in allE) - apply (erule_tac x="v$2" in allE) - apply (subgoal_tac "vector [v$1, v$2] = v") - apply simp - apply (vector vector_def) - apply (simp add: forall_2) - done +proof - + have "P v" if "\x y. P (vector [x, y])" for v + proof - + have "vector [v$1, v$2] = v" + by (smt (verit, best) exhaust_2 vec_eq_iff vector_2) + then show ?thesis + by (metis that) + qed + then show ?thesis by auto +qed lemma forall_vector_3: "(\v::'a::zero^3. P v) \ (\x y z. P(vector[x, y, z]))" - apply auto - apply (erule_tac x="v$1" in allE) - apply (erule_tac x="v$2" in allE) - apply (erule_tac x="v$3" in allE) - apply (subgoal_tac "vector [v$1, v$2, v$3] = v") - apply simp - apply (vector vector_def) - apply (simp add: forall_3) - done +proof - + have "P v" if "\x y z. P (vector [x, y, z])" for v + proof - + have "vector [v$1, v$2, v$3] = v" + by (smt (verit, best) exhaust_3 vec_eq_iff vector_3) + then show ?thesis + by (metis that) + qed + then show ?thesis by auto +qed subsection\<^marker>\tag unimportant\ \lambda skolemization on cartesian products\ -lemma lambda_skolem: "(\i. \x. P i x) \ - (\x::'a ^ 'n. \i. P i (x $ i))" (is "?lhs \ ?rhs") -proof - - let ?S = "(UNIV :: 'n set)" - { assume H: "?rhs" - then have ?lhs by auto } - moreover - { assume H: "?lhs" - then obtain f where f:"\i. P i (f i)" unfolding choice_iff by metis - let ?x = "(\ i. (f i)) :: 'a ^ 'n" - { fix i - from f have "P i (f i)" by metis - then have "P i (?x $ i)" by auto - } - hence "\i. P i (?x$i)" by metis - hence ?rhs by metis } - ultimately show ?thesis by metis -qed +lemma lambda_skolem: "(\i. \x. P i x) \ (\x::'a ^ 'n. \i. P i (x $ i))" + by (metis vec_lambda_beta) text \The same result in terms of square matrices.\ @@ -885,8 +771,7 @@ fixes A B :: "real ^'n ^'n" and x y :: "real ^'n" shows "(A *v x) \ (B *v y) = (((rowvector x :: real^'n^1) ** ((transpose A ** B) ** (columnvector y :: real ^1^'n)))$1)$1" - unfolding dot_matrix_product transpose_columnvector[symmetric] - dot_rowvector_columnvector matrix_transpose_mul matrix_mul_assoc .. + by (metis dot_lmul_matrix dot_matrix_product dot_rowvector_columnvector matrix_mul_assoc vector_transpose_matrix) lemma dim_substandard_cart: "vec.dim {x::'a::field^'n. \i. i \ d \ x$i = 0} = card d" @@ -931,7 +816,7 @@ hence "m *s x = y - c" by (simp add: field_simps) hence "inverse m *s (m *s x) = inverse m *s (y - c)" by simp then show "x = inverse m *s y + - (inverse m *s c)" - using m0 by (simp add: vector_smult_assoc vector_ssub_ldistrib) + by (simp add: m0 vec.scale_right_diff_distrib) next assume h: "x = inverse m *s y + - (inverse m *s c)" show "m *s x + c = y" unfolding h @@ -940,8 +825,7 @@ lemma vector_eq_affinity: "(m::'a::field) \ 0 ==> (y = m *s x + c \ inverse(m) *s y + -(inverse(m) *s c) = x)" - using vector_affinity_eq[where m=m and x=x and y=y and c=c] - by metis + by (metis vector_affinity_eq) lemma vector_cart: fixes f :: "real^'n \ real" @@ -1017,14 +901,9 @@ by blast } moreover - { - assume lf: "Vector_Spaces.linear (*s) (*s) f" and om: "orthogonal_matrix ?mf" - from lf om have ?lhs - unfolding orthogonal_matrix_def norm_eq orthogonal_transformation - apply (simp only: matrix_works[OF lf, symmetric] dot_matrix_vector_mul) - apply (simp add: dot_matrix_product linear_def scalar_mult_eq_scaleR) - done - } + have ?lhs if "Vector_Spaces.linear (*s) (*s) f" and "orthogonal_matrix ?mf" + using that unfolding orthogonal_matrix_def norm_eq orthogonal_transformation + by (metis dot_matrix_product dot_matrix_vector_mul linear_matrix_vector_mul_eq matrix_mul_lid matrix_vector_mul(2)) ultimately show ?thesis by (auto simp: linear_def scalar_mult_eq_scaleR) qed @@ -1052,7 +931,7 @@ (\i j. i \ j \ orthogonal (row i A) (row j A))" using orthogonal_matrix_orthonormal_columns [of "transpose A"] by simp -proposition orthogonal_matrix_exists_basis: +proposition orthogonal_matrix_exists_basis: fixes a :: "real^'n" assumes "norm a = 1" obtains A where "orthogonal_matrix A" "A *v (axis k 1) = a" @@ -1084,16 +963,13 @@ assumes "norm a = 1" "norm b = 1" obtains f where "orthogonal_transformation f" "f a = b" proof - - obtain k::'n where True - by simp - 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" + obtain k A B where AB: "orthogonal_matrix A" "orthogonal_matrix B" and eq: "A *v (axis k 1) = a" "B *v (axis k 1) = b" using orthogonal_matrix_exists_basis assms by metis let ?f = "\x. (B ** transpose A) *v x" show thesis proof show "orthogonal_transformation ?f" - by (subst orthogonal_transformation_matrix) - (auto simp: AB orthogonal_matrix_mul) + by (simp add: AB orthogonal_matrix_mul orthogonal_transformation_matrix) next show "?f a = b" using \orthogonal_matrix A\ unfolding orthogonal_matrix_def @@ -1101,7 +977,7 @@ qed qed -proposition orthogonal_transformation_exists: +proposition orthogonal_transformation_exists: fixes a b :: "real^'n" assumes "norm a = norm b" obtains f where "orthogonal_transformation f" "f a = b" @@ -1114,16 +990,7 @@ then obtain f where f: "orthogonal_transformation f" and eq: "f (a /\<^sub>R norm a) = (b /\<^sub>R norm b)" by (auto intro: orthogonal_transformation_exists_1 [of "a /\<^sub>R norm a" "b /\<^sub>R norm b"]) show ?thesis - proof - interpret linear f - using f by (simp add: orthogonal_transformation_linear) - have "f a /\<^sub>R norm a = f (a /\<^sub>R norm a)" - by (simp add: scale) - also have "\ = b /\<^sub>R norm a" - by (simp add: eq assms [symmetric]) - finally show "f a = b" - using False by auto - qed (use f in auto) + using False assms eq f orthogonal_transformation_scaleR that by fastforce qed @@ -1157,9 +1024,7 @@ proposition orthogonal_transformation_isometry: "orthogonal_transformation f \ f(0::'a::real_inner) = (0::'a) \ (\x y. dist(f x) (f y) = dist x y)" unfolding orthogonal_transformation - apply (auto simp: linear_0 isometry_linear) - apply (metis (no_types, opaque_lifting) dist_norm linear_diff) - by (metis dist_0_norm) + by (metis dist_0_norm dist_norm isometry_linear linear_0 linear_diff) text \Can extend an isometry from unit sphere:\ @@ -1369,10 +1234,7 @@ apply (simp add: if_if_eq_conj sum.neutral conj_commute cong: conj_cong) done show ?thesis - apply (subst eq) - apply (intro mult idplus that) - apply (auto intro: diagonal) - done + unfolding eq by (intro mult idplus that) (auto intro: diagonal) qed show ?thesis by (rule induct_matrix_elementary) (auto intro: assms *)