diff -r 7414ce0256e1 -r fde093888c16 src/HOL/Analysis/Cartesian_Space.thy --- a/src/HOL/Analysis/Cartesian_Space.thy Mon Aug 27 22:58:36 2018 +0200 +++ b/src/HOL/Analysis/Cartesian_Space.thy Tue Aug 28 13:28:39 2018 +0100 @@ -11,19 +11,19 @@ Finite_Cartesian_Product Linear_Algebra begin -definition "cart_basis = {axis i 1 | i. i\UNIV}" +definition%unimportant "cart_basis = {axis i 1 | i. i\UNIV}" -lemma finite_cart_basis: "finite (cart_basis)" unfolding cart_basis_def +lemma%unimportant finite_cart_basis: "finite (cart_basis)" unfolding cart_basis_def using finite_Atleast_Atmost_nat by fastforce -lemma card_cart_basis: "card (cart_basis::('a::zero_neq_one^'i) set) = CARD('i)" +lemma%unimportant card_cart_basis: "card (cart_basis::('a::zero_neq_one^'i) set) = CARD('i)" unfolding cart_basis_def Setcompr_eq_image by (rule card_image) (auto simp: inj_on_def axis_eq_axis) interpretation vec: vector_space "( *s) " by unfold_locales (vector algebra_simps)+ -lemma independent_cart_basis: +lemma%unimportant independent_cart_basis: "vec.independent (cart_basis)" proof (rule vec.independent_if_scalars_zero) show "finite (cart_basis)" using finite_cart_basis . @@ -48,7 +48,7 @@ finally show "f x = 0" .. qed -lemma span_cart_basis: +lemma%unimportant span_cart_basis: "vec.span (cart_basis) = UNIV" proof (auto) fix x::"('a, 'b) vec" @@ -93,12 +93,12 @@ interpretation vec: finite_dimensional_vector_space "( *s)" "cart_basis" by (unfold_locales, auto simp add: finite_cart_basis independent_cart_basis span_cart_basis) -lemma matrix_vector_mul_linear_gen[intro, simp]: +lemma%unimportant matrix_vector_mul_linear_gen[intro, simp]: "Vector_Spaces.linear ( *s) ( *s) (( *v) A)" by unfold_locales (vector matrix_vector_mult_def sum.distrib algebra_simps)+ -lemma span_vec_eq: "vec.span X = span X" +lemma%important span_vec_eq: "vec.span X = span X" and dim_vec_eq: "vec.dim X = dim X" and dependent_vec_eq: "vec.dependent X = dependent X" and subspace_vec_eq: "vec.subspace X = subspace X" @@ -106,11 +106,11 @@ unfolding span_raw_def dim_raw_def dependent_raw_def subspace_raw_def by (auto simp: scalar_mult_eq_scaleR) -lemma linear_componentwise: +lemma%important linear_componentwise: fixes f:: "'a::field ^'m \ 'a ^ 'n" assumes lf: "Vector_Spaces.linear ( *s) ( *s) f" shows "(f x)$j = sum (\i. (x$i) * (f (axis i 1)$j)) (UNIV :: 'm set)" (is "?lhs = ?rhs") -proof - +proof%unimportant - interpret lf: Vector_Spaces.linear "( *s)" "( *s)" f using lf . let ?M = "(UNIV :: 'm set)" @@ -128,7 +128,7 @@ interpretation vec: finite_dimensional_vector_space_pair "( *s)" cart_basis "( *s)" cart_basis .. -lemma matrix_works: +lemma%unimportant 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) @@ -136,45 +136,45 @@ apply (rule linear_componentwise[OF lf, symmetric]) done -lemma matrix_of_matrix_vector_mul[simp]: "matrix(\x. A *v (x :: 'a::field ^ 'n)) = A" +lemma%unimportant matrix_of_matrix_vector_mul[simp]: "matrix(\x. A *v (x :: 'a::field ^ 'n)) = A" by (simp add: matrix_eq matrix_works) -lemma matrix_compose_gen: +lemma%unimportant matrix_compose_gen: assumes lf: "Vector_Spaces.linear ( *s) ( *s) (f::'a::{field}^'n \ 'a^'m)" and lg: "Vector_Spaces.linear ( *s) ( *s) (g::'a^'m \ 'a^_)" shows "matrix (g o f) = matrix g ** matrix f" using lf lg Vector_Spaces.linear_compose[OF lf lg] matrix_works[OF Vector_Spaces.linear_compose[OF lf lg]] by (simp add: matrix_eq matrix_works matrix_vector_mul_assoc[symmetric] o_def) -lemma matrix_compose: +lemma%unimportant matrix_compose: assumes "linear (f::real^'n \ real^'m)" "linear (g::real^'m \ real^_)" shows "matrix (g o f) = matrix g ** matrix f" using matrix_compose_gen[of f g] assms by (simp add: linear_def scalar_mult_eq_scaleR) -lemma left_invertible_transpose: +lemma%unimportant left_invertible_transpose: "(\(B). B ** transpose (A) = mat (1::'a::comm_semiring_1)) \ (\(B). A ** B = mat 1)" by (metis matrix_transpose_mul transpose_mat transpose_transpose) -lemma right_invertible_transpose: +lemma%unimportant right_invertible_transpose: "(\(B). transpose (A) ** B = mat (1::'a::comm_semiring_1)) \ (\(B). B ** A = mat 1)" by (metis matrix_transpose_mul transpose_mat transpose_transpose) -lemma linear_matrix_vector_mul_eq: +lemma%unimportant linear_matrix_vector_mul_eq: "Vector_Spaces.linear ( *s) ( *s) f \ linear (f :: real^'n \ real ^'m)" by (simp add: scalar_mult_eq_scaleR linear_def) -lemma matrix_vector_mul[simp]: +lemma%unimportant matrix_vector_mul[simp]: "Vector_Spaces.linear ( *s) ( *s) g \ (\y. matrix g *v y) = g" "linear f \ (\x. matrix f *v x) = f" "bounded_linear f \ (\x. matrix f *v x) = f" for f :: "real^'n \ real ^'m" by (simp_all add: ext matrix_works linear_matrix_vector_mul_eq linear_linear) -lemma matrix_left_invertible_injective: +lemma%important matrix_left_invertible_injective: fixes A :: "'a::field^'n^'m" shows "(\B. B ** A = mat 1) \ inj (( *v) A)" -proof safe +proof%unimportant safe fix B assume B: "B ** A = mat 1" show "inj (( *v) A)" @@ -192,15 +192,15 @@ by metis qed -lemma matrix_left_invertible_ker: +lemma%unimportant 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) -lemma matrix_right_invertible_surjective: +lemma%important matrix_right_invertible_surjective: "(\B. (A::'a::field^'n^'m) ** (B::'a::field^'m^'n) = mat 1) \ surj (\x. A *v x)" -proof - +proof%unimportant - { fix B :: "'a ^'m^'n" assume AB: "A ** B = mat 1" { fix x :: "'a ^ 'm" @@ -223,12 +223,12 @@ ultimately show ?thesis unfolding surj_def by blast qed -lemma matrix_left_invertible_independent_columns: +lemma%important matrix_left_invertible_independent_columns: fixes A :: "'a::{field}^'n^'m" shows "(\(B::'a ^'m^'n). B ** A = mat 1) \ (\c. sum (\i. c i *s column i A) (UNIV :: 'n set) = 0 \ (\i. c i = 0))" (is "?lhs \ ?rhs") -proof - +proof%unimportant - let ?U = "UNIV :: 'n set" { assume k: "\x. A *v x = 0 \ x = 0" { fix c i @@ -250,7 +250,7 @@ ultimately show ?thesis unfolding matrix_left_invertible_ker by auto qed -lemma matrix_right_invertible_independent_rows: +lemma%unimportant 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))" @@ -258,10 +258,10 @@ matrix_left_invertible_independent_columns by (simp add:) -lemma matrix_right_invertible_span_columns: +lemma%important matrix_right_invertible_span_columns: "(\(B::'a::field ^'n^'m). (A::'a ^'m^'n) ** B = mat 1) \ vec.span (columns A) = UNIV" (is "?lhs = ?rhs") -proof - +proof%unimportant - let ?U = "UNIV :: 'm set" have fU: "finite ?U" by simp have lhseq: "?lhs \ (\y. \(x::'a^'m). sum (\i. (x$i) *s column i A) ?U = y)" @@ -322,21 +322,21 @@ ultimately show ?thesis by blast qed -lemma matrix_left_invertible_span_rows_gen: +lemma%unimportant 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 .. -lemma matrix_left_invertible_span_rows: +lemma%unimportant matrix_left_invertible_span_rows: "(\(B::real^'m^'n). B ** (A::real^'n^'m) = mat 1) \ span (rows A) = UNIV" using matrix_left_invertible_span_rows_gen[of A] by (simp add: span_vec_eq) -lemma matrix_left_right_inverse: +lemma%important matrix_left_right_inverse: fixes A A' :: "'a::{field}^'n^'n" shows "A ** A' = mat 1 \ A' ** A = mat 1" -proof - +proof%unimportant - { fix A A' :: "'a ^'n^'n" assume AA': "A ** A' = mat 1" have sA: "surj (( *v) A)" @@ -356,21 +356,21 @@ then show ?thesis by blast qed -lemma invertible_left_inverse: +lemma%unimportant invertible_left_inverse: fixes A :: "'a::{field}^'n^'n" shows "invertible A \ (\(B::'a^'n^'n). B ** A = mat 1)" by (metis invertible_def matrix_left_right_inverse) -lemma invertible_right_inverse: +lemma%unimportant invertible_right_inverse: fixes A :: "'a::{field}^'n^'n" shows "invertible A \ (\(B::'a^'n^'n). A** B = mat 1)" by (metis invertible_def matrix_left_right_inverse) -lemma invertible_mult: +lemma%important invertible_mult: assumes inv_A: "invertible A" and inv_B: "invertible B" shows "invertible (A**B)" -proof - +proof%unimportant - obtain A' where AA': "A ** A' = mat 1" and A'A: "A' ** A = mat 1" using inv_A unfolding invertible_def by blast obtain B' where BB': "B ** B' = mat 1" and B'B: "B' ** B = mat 1" @@ -393,28 +393,28 @@ qed qed -lemma transpose_invertible: +lemma%unimportant transpose_invertible: fixes A :: "real^'n^'n" assumes "invertible A" shows "invertible (transpose A)" by (meson assms invertible_def matrix_left_right_inverse right_invertible_transpose) -lemma vector_matrix_mul_assoc: +lemma%important vector_matrix_mul_assoc: fixes v :: "('a::comm_semiring_1)^'n" shows "(v v* M) v* N = v v* (M ** N)" -proof - +proof%unimportant - 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 -lemma matrix_scaleR_vector_ac: +lemma%unimportant matrix_scaleR_vector_ac: fixes A :: "real^('m::finite)^'n" shows "A *v (k *\<^sub>R v) = k *\<^sub>R A *v v" by (metis matrix_vector_mult_scaleR transpose_scalar vector_scaleR_matrix_ac vector_transpose_matrix) -lemma scaleR_matrix_vector_assoc: +lemma%unimportant scaleR_matrix_vector_assoc: fixes A :: "real^('m::finite)^'n" shows "k *\<^sub>R (A *v v) = k *\<^sub>R A *v v" by (metis matrix_scaleR_vector_ac matrix_vector_mult_scaleR) @@ -430,8 +430,8 @@ and BasisB :: "('b set)" and f :: "('b=>'c)" -lemma vec_dim_card: "vec.dim (UNIV::('a::{field}^'n) set) = CARD ('n)" -proof - +lemma%important vec_dim_card: "vec.dim (UNIV::('a::{field}^'n) set) = CARD ('n)" +proof%unimportant - 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 ..