# HG changeset patch # User nipkow # Date 1547635686 -3600 # Node ID d51e5e41fafe5fbd5c60c03980f8dec9d549ec30 # Parent 60110f6d0b4e239e9c403e9ea93182cd820d282e Reorg of material diff -r 60110f6d0b4e -r d51e5e41fafe src/HOL/Analysis/Cartesian_Euclidean_Space.thy --- a/src/HOL/Analysis/Cartesian_Euclidean_Space.thy Wed Jan 16 10:27:57 2019 +0100 +++ b/src/HOL/Analysis/Cartesian_Euclidean_Space.thy Wed Jan 16 11:48:06 2019 +0100 @@ -187,31 +187,6 @@ shows "A ** transpose A = (\ i j. inner (row i A) (row j A))" by (simp add: matrix_matrix_mult_def vec_eq_iff transpose_def row_def inner_vec_def) -text\Two sometimes fruitful ways of looking at matrix-vector multiplication.\ - -lemma%important matrix_mult_dot: "A *v x = (\ i. inner (A$i) x)" - by (simp add: matrix_vector_mult_def inner_vec_def) - -lemma%unimportant 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 - -lemma%important matrix_adjoint: assumes lf: "linear (f :: real^'n \ real ^'m)" - shows "matrix(adjoint f) = transpose(matrix f)" -proof%unimportant - - 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 - lemma%unimportant matrix_vector_mul_bounded_linear[intro, simp]: "bounded_linear ((*v) A)" for A :: "'a::{euclidean_space,real_algebra_1}^'n^'m" using matrix_vector_mul_linear[of A] by (simp add: linear_conv_bounded_linear linear_matrix_vector_mul_eq) @@ -703,16 +678,6 @@ then show "?A \ vec.span ?B" by auto qed (simp add: card_image inj_on_def axis_eq_axis) -lemma%unimportant dim_subset_UNIV_cart_gen: - fixes S :: "('a::field^'n) set" - shows "vec.dim S \ CARD('n)" - by (metis vec.dim_eq_full vec.dim_subset_UNIV vec.span_UNIV vec_dim_card) - -lemma%unimportant dim_subset_UNIV_cart: - fixes S :: "(real^'n) set" - shows "dim S \ CARD('n)" - using dim_subset_UNIV_cart_gen[of S] by (simp add: dim_vec_eq) - lemma%unimportant affinity_inverses: assumes m0: "m \ (0::'a::field)" shows "(\x. m *s x + c) \ (\x. inverse(m) *s x + (-(inverse(m) *s c))) = id" @@ -813,13 +778,7 @@ vector_cart[of "\j. frechet_derivative f (at x) j $ k"] by (simp add: Basis_vec_def axis_eq_axis inner_axis jacobian_def matrix_def) -subsection%unimportant \Lemmas for working on \<^typ>\real^1\\ - -lemma forall_1[simp]: "(\i::1. P i) \ P 1" - by (metis (full_types) num1_eq_iff) - -lemma ex_1[simp]: "(\x::1. P x) \ P 1" - by auto (metis (full_types) num1_eq_iff) +subsection%unimportant \Lemmas for working on \real^1/2/3\\ lemma exhaust_2: fixes x :: 2 @@ -865,24 +824,6 @@ lemma sum_3: "sum f (UNIV::3 set) = f 1 + f 2 + f 3" unfolding UNIV_3 by (simp add: ac_simps) -lemma num1_eqI: - fixes a::num1 shows "a = b" - by (metis (full_types) UNIV_1 UNIV_I empty_iff insert_iff) - -lemma num1_eq1 [simp]: - fixes a::num1 shows "a = 1" - by (rule num1_eqI) - -instantiation num1 :: linorder begin -definition "a < b \ Rep_num1 a < Rep_num1 b" -definition "a \ b \ Rep_num1 a \ Rep_num1 b" -instance - by intro_classes (auto simp: less_eq_num1_def less_num1_def intro: num1_eqI) -end - -instance num1 :: wellorder - by intro_classes (auto simp: less_eq_num1_def less_num1_def) - subsection%unimportant\The collapse of the general concepts to dimension one\ lemma vector_one: "(x::'a ^1) = (\ i. (x$1))" @@ -908,171 +849,6 @@ lemma dist_real: "dist(x::real ^ 1) y = \(x$1) - (y$1)\" by (auto simp add: norm_real dist_norm) -subsection%important\ Rank of a matrix\ - -text\Equivalence of row and column rank is taken from George Mackiw's paper, Mathematics Magazine 1995, p. 285.\ - -lemma%unimportant 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 - -lemma%unimportant matrix_vector_mult_in_columnspace: - fixes A :: "real^'n^'m" - shows "(A *v x) \ span(columns A)" - using matrix_vector_mult_in_columnspace_gen[of A x] by (simp add: span_vec_eq) - -lemma%important orthogonal_nullspace_rowspace: - fixes A :: "real^'n^'m" - assumes 0: "A *v x = 0" and y: "y \ span(rows A)" - shows "orthogonal x y" - using y -proof%unimportant (induction rule: span_induct) - case base - then show ?case - by (simp add: subspace_orthogonal_to_vector) -next - case (step v) - then obtain i where "v = row i A" - by (auto simp: rows_def) - with 0 show ?case - unfolding orthogonal_def inner_vec_def matrix_vector_mult_def row_def - by (simp add: mult.commute) (metis (no_types) vec_lambda_beta zero_index) -qed - -lemma%unimportant nullspace_inter_rowspace: - fixes A :: "real^'n^'m" - shows "A *v x = 0 \ x \ span(rows A) \ x = 0" - using orthogonal_nullspace_rowspace orthogonal_self span_zero matrix_vector_mult_0_right - by blast - -lemma%unimportant matrix_vector_mul_injective_on_rowspace: - fixes A :: "real^'n^'m" - shows "\A *v x = A *v y; x \ span(rows A); y \ span(rows A)\ \ x = y" - using nullspace_inter_rowspace [of A "x-y"] - by (metis diff_eq_diff_eq diff_self matrix_vector_mult_diff_distrib span_diff) - -definition%important rank :: "'a::field^'n^'m=>nat" - where row_rank_def_gen: "rank A \ vec.dim(rows A)" - -lemma%important row_rank_def: "rank A = dim (rows A)" for A::"real^'n^'m" - by%unimportant (auto simp: row_rank_def_gen dim_vec_eq) - -lemma%important dim_rows_le_dim_columns: - fixes A :: "real^'n^'m" - shows "dim(rows A) \ dim(columns A)" -proof%unimportant - - have "dim (span (rows A)) \ dim (span (columns A))" - proof - - obtain B where "independent B" "span(rows A) \ span B" - and B: "B \ span(rows A)""card B = dim (span(rows A))" - using basis_exists [of "span(rows A)"] by metis - with span_subspace have eq: "span B = span(rows A)" - by auto - then have inj: "inj_on ((*v) A) (span B)" - by (simp add: inj_on_def matrix_vector_mul_injective_on_rowspace) - 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) - also have "\ \ dim (span (columns A))" - using _ ind - by (rule independent_card_le_dim) (auto intro!: matrix_vector_mult_in_columnspace) - finally show ?thesis . - qed - then show ?thesis - by (simp add: dim_span) -qed - -lemma%unimportant column_rank_def: - fixes A :: "real^'n^'m" - shows "rank A = dim(columns A)" - unfolding row_rank_def - by (metis columns_transpose dim_rows_le_dim_columns le_antisym rows_transpose) - -lemma%unimportant rank_transpose: - fixes A :: "real^'n^'m" - shows "rank(transpose A) = rank A" - by (metis column_rank_def row_rank_def rows_transpose) - -lemma%unimportant matrix_vector_mult_basis: - fixes A :: "real^'n^'m" - shows "A *v (axis k 1) = column k A" - by (simp add: cart_eq_inner_axis column_def matrix_mult_dot) - -lemma%unimportant columns_image_basis: - fixes A :: "real^'n^'m" - shows "columns A = (*v) A ` (range (\i. axis i 1))" - by (force simp: columns_def matrix_vector_mult_basis [symmetric]) - -lemma%important rank_dim_range: - fixes A :: "real^'n^'m" - shows "rank A = dim(range (\x. A *v x))" - unfolding column_rank_def -proof%unimportant (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 - -lemma%unimportant rank_bound: - fixes A :: "real^'n^'m" - shows "rank A \ min CARD('m) (CARD('n))" - by (metis (mono_tags, lifting) dim_subset_UNIV_cart min.bounded_iff - column_rank_def row_rank_def) - -lemma%unimportant full_rank_injective: - fixes A :: "real^'n^'m" - shows "rank A = CARD('n) \ inj ((*v) A)" - by (simp add: matrix_left_invertible_injective [symmetric] matrix_left_invertible_span_rows row_rank_def - dim_eq_full [symmetric] card_cart_basis vec.dimension_def) - -lemma%unimportant 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) - -lemma%unimportant rank_I: "rank(mat 1::real^'n^'n) = CARD('n)" - by (simp add: full_rank_injective inj_on_def) - -lemma%unimportant 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]) - -lemma%unimportant matrix_nonfull_linear_equations_eq: - fixes A :: "real^'n^'m" - shows "(\x. (x \ 0) \ A *v x = 0) \ rank A \ CARD('n)" - by (meson matrix_left_invertible_injective full_rank_injective matrix_left_invertible_ker) - -lemma%unimportant rank_eq_0: "rank A = 0 \ A = 0" and rank_0 [simp]: "rank (0::real^'n^'m) = 0" - for A :: "real^'n^'m" - by (auto simp: rank_dim_range matrix_eq) - -lemma%important rank_mul_le_right: - fixes A :: "real^'n^'m" and B :: "real^'p^'n" - shows "rank(A ** B) \ rank B" -proof%unimportant - - have "rank(A ** B) \ dim ((*v) A ` range ((*v) B))" - by (auto simp: rank_dim_range image_comp o_def matrix_vector_mul_assoc) - also have "\ \ rank B" - by (simp add: rank_dim_range dim_image_le) - finally show ?thesis . -qed - -lemma%unimportant rank_mul_le_left: - fixes A :: "real^'n^'m" and B :: "real^'p^'n" - shows "rank(A ** B) \ rank A" - by (metis matrix_transpose_mul rank_mul_le_right rank_transpose) - subsection%unimportant\Routine results connecting the types \<^typ>\real^1\ and \<^typ>\real\\ lemma vector_one_nth [simp]: diff -r 60110f6d0b4e -r d51e5e41fafe src/HOL/Analysis/Cartesian_Space.thy --- a/src/HOL/Analysis/Cartesian_Space.thy Wed Jan 16 10:27:57 2019 +0100 +++ b/src/HOL/Analysis/Cartesian_Space.thy Wed Jan 16 11:48:06 2019 +0100 @@ -462,4 +462,209 @@ lemma dimension_eq_1[code_unfold]: "vector_space_over_itself.dimension TYPE('a::field)= 1" unfolding vector_space_over_itself.dimension_def by simp + +lemma%unimportant dim_subset_UNIV_cart_gen: + fixes S :: "('a::field^'n) set" + shows "vec.dim S \ CARD('n)" + by (metis vec.dim_eq_full vec.dim_subset_UNIV vec.span_UNIV vec_dim_card) + +lemma%unimportant dim_subset_UNIV_cart: + fixes S :: "(real^'n) set" + shows "dim S \ CARD('n)" + using dim_subset_UNIV_cart_gen[of S] by (simp add: dim_vec_eq) + +text\Two sometimes fruitful ways of looking at matrix-vector multiplication.\ + +lemma%important matrix_mult_dot: "A *v x = (\ i. inner (A$i) x)" + by (simp add: matrix_vector_mult_def inner_vec_def) + +lemma%unimportant 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 + +lemma%important matrix_adjoint: assumes lf: "linear (f :: real^'n \ real ^'m)" + shows "matrix(adjoint f) = transpose(matrix f)" +proof%unimportant - + 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 + + +subsection%important\ Rank of a matrix\ + +text\Equivalence of row and column rank is taken from George Mackiw's paper, Mathematics Magazine 1995, p. 285.\ + +lemma%unimportant 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 + +lemma%unimportant matrix_vector_mult_in_columnspace: + fixes A :: "real^'n^'m" + shows "(A *v x) \ span(columns A)" + using matrix_vector_mult_in_columnspace_gen[of A x] by (simp add: span_vec_eq) + +lemma subspace_orthogonal_to_vector: "subspace {y. orthogonal x y}" + by (simp add: subspace_def orthogonal_clauses) + +lemma%important orthogonal_nullspace_rowspace: + fixes A :: "real^'n^'m" + assumes 0: "A *v x = 0" and y: "y \ span(rows A)" + shows "orthogonal x y" + using y +proof%unimportant (induction rule: span_induct) + case base + then show ?case + by (simp add: subspace_orthogonal_to_vector) +next + case (step v) + then obtain i where "v = row i A" + by (auto simp: rows_def) + with 0 show ?case + unfolding orthogonal_def inner_vec_def matrix_vector_mult_def row_def + by (simp add: mult.commute) (metis (no_types) vec_lambda_beta zero_index) +qed + +lemma%unimportant nullspace_inter_rowspace: + fixes A :: "real^'n^'m" + shows "A *v x = 0 \ x \ span(rows A) \ x = 0" + using orthogonal_nullspace_rowspace orthogonal_self span_zero matrix_vector_mult_0_right + by blast + +lemma%unimportant matrix_vector_mul_injective_on_rowspace: + fixes A :: "real^'n^'m" + shows "\A *v x = A *v y; x \ span(rows A); y \ span(rows A)\ \ x = y" + using nullspace_inter_rowspace [of A "x-y"] + by (metis diff_eq_diff_eq diff_self matrix_vector_mult_diff_distrib span_diff) + +definition%important rank :: "'a::field^'n^'m=>nat" + where row_rank_def_gen: "rank A \ vec.dim(rows A)" + +lemma%important row_rank_def: "rank A = dim (rows A)" for A::"real^'n^'m" + by%unimportant (auto simp: row_rank_def_gen dim_vec_eq) + +lemma%important dim_rows_le_dim_columns: + fixes A :: "real^'n^'m" + shows "dim(rows A) \ dim(columns A)" +proof%unimportant - + have "dim (span (rows A)) \ dim (span (columns A))" + proof - + obtain B where "independent B" "span(rows A) \ span B" + and B: "B \ span(rows A)""card B = dim (span(rows A))" + using basis_exists [of "span(rows A)"] by metis + with span_subspace have eq: "span B = span(rows A)" + by auto + then have inj: "inj_on ((*v) A) (span B)" + by (simp add: inj_on_def matrix_vector_mul_injective_on_rowspace) + 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) + also have "\ \ dim (span (columns A))" + using _ ind + by (rule independent_card_le_dim) (auto intro!: matrix_vector_mult_in_columnspace) + finally show ?thesis . + qed + then show ?thesis + by (simp add: dim_span) +qed + +lemma%unimportant column_rank_def: + fixes A :: "real^'n^'m" + shows "rank A = dim(columns A)" + unfolding row_rank_def + by (metis columns_transpose dim_rows_le_dim_columns le_antisym rows_transpose) + +lemma%unimportant rank_transpose: + fixes A :: "real^'n^'m" + shows "rank(transpose A) = rank A" + by (metis column_rank_def row_rank_def rows_transpose) + +lemma%unimportant matrix_vector_mult_basis: + fixes A :: "real^'n^'m" + shows "A *v (axis k 1) = column k A" + by (simp add: cart_eq_inner_axis column_def matrix_mult_dot) + +lemma%unimportant columns_image_basis: + fixes A :: "real^'n^'m" + shows "columns A = (*v) A ` (range (\i. axis i 1))" + by (force simp: columns_def matrix_vector_mult_basis [symmetric]) + +lemma%important rank_dim_range: + fixes A :: "real^'n^'m" + shows "rank A = dim(range (\x. A *v x))" + unfolding column_rank_def +proof%unimportant (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 + +lemma%unimportant rank_bound: + fixes A :: "real^'n^'m" + shows "rank A \ min CARD('m) (CARD('n))" + by (metis (mono_tags, lifting) dim_subset_UNIV_cart min.bounded_iff + column_rank_def row_rank_def) + +lemma%unimportant full_rank_injective: + fixes A :: "real^'n^'m" + shows "rank A = CARD('n) \ inj ((*v) A)" + by (simp add: matrix_left_invertible_injective [symmetric] matrix_left_invertible_span_rows row_rank_def + dim_eq_full [symmetric] card_cart_basis vec.dimension_def) + +lemma%unimportant 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) + +lemma%unimportant rank_I: "rank(mat 1::real^'n^'n) = CARD('n)" + by (simp add: full_rank_injective inj_on_def) + +lemma%unimportant 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]) + +lemma%unimportant matrix_nonfull_linear_equations_eq: + fixes A :: "real^'n^'m" + shows "(\x. (x \ 0) \ A *v x = 0) \ rank A \ CARD('n)" + by (meson matrix_left_invertible_injective full_rank_injective matrix_left_invertible_ker) + +lemma%unimportant rank_eq_0: "rank A = 0 \ A = 0" and rank_0 [simp]: "rank (0::real^'n^'m) = 0" + for A :: "real^'n^'m" + by (auto simp: rank_dim_range matrix_eq) + +lemma%important rank_mul_le_right: + fixes A :: "real^'n^'m" and B :: "real^'p^'n" + shows "rank(A ** B) \ rank B" +proof%unimportant - + have "rank(A ** B) \ dim ((*v) A ` range ((*v) B))" + by (auto simp: rank_dim_range image_comp o_def matrix_vector_mul_assoc) + also have "\ \ rank B" + by (simp add: rank_dim_range dim_image_le) + finally show ?thesis . +qed + +lemma%unimportant rank_mul_le_left: + fixes A :: "real^'n^'m" and B :: "real^'p^'n" + shows "rank(A ** B) \ rank A" + by (metis matrix_transpose_mul rank_mul_le_right rank_transpose) + end \ No newline at end of file diff -r 60110f6d0b4e -r d51e5e41fafe src/HOL/Library/Numeral_Type.thy --- a/src/HOL/Library/Numeral_Type.thy Wed Jan 16 10:27:57 2019 +0100 +++ b/src/HOL/Library/Numeral_Type.thy Wed Jan 16 11:48:06 2019 +0100 @@ -45,6 +45,8 @@ unfolding type_definition.card [OF type_definition_bit1] by simp +subsection \@{typ num1}\ + instance num1 :: finite proof show "finite (UNIV::num1 set)" @@ -62,6 +64,42 @@ end +lemma num1_eq_iff: "(x::num1) = (y::num1) \ True" + by (induct x, induct y) simp + +instantiation num1 :: "{comm_ring,comm_monoid_mult,numeral}" +begin + +instance + by standard (simp_all add: num1_eq_iff) + +end + +lemma num1_eqI: + fixes a::num1 shows "a = b" +by(simp add: num1_eq_iff) + +lemma num1_eq1 [simp]: + fixes a::num1 shows "a = 1" + by (rule num1_eqI) + +lemma forall_1[simp]: "(\i::num1. P i) \ P 1" + by (metis (full_types) num1_eq_iff) + +lemma ex_1[simp]: "(\x::num1. P x) \ P 1" + by auto (metis (full_types) num1_eq_iff) + +instantiation num1 :: linorder begin +definition "a < b \ Rep_num1 a < Rep_num1 b" +definition "a \ b \ Rep_num1 a \ Rep_num1 b" +instance + by intro_classes (auto simp: less_eq_num1_def less_num1_def intro: num1_eqI) +end + +instance num1 :: wellorder + by intro_classes (auto simp: less_eq_num1_def less_num1_def) + + instance bit0 :: (finite) card2 proof show "finite (UNIV::'a bit0 set)" @@ -195,17 +233,6 @@ \<^typ>\num1\, since 0 and 1 are not distinct. \ -instantiation num1 :: "{comm_ring,comm_monoid_mult,numeral}" -begin - -lemma num1_eq_iff: "(x::num1) = (y::num1) \ True" - by (induct x, induct y) simp - -instance - by standard (simp_all add: num1_eq_iff) - -end - instantiation bit0 and bit1 :: (finite) "{zero,one,plus,times,uminus,minus}" begin @@ -360,8 +387,7 @@ definition "enum_class.enum_ex P = P (1 :: num1)" instance by intro_classes - (auto simp add: enum_num1_def enum_all_num1_def enum_ex_num1_def num1_eq_iff Ball_def, - (metis (full_types) num1_eq_iff)+) + (auto simp add: enum_num1_def enum_all_num1_def enum_ex_num1_def num1_eq_iff Ball_def) end instantiation num0 and num1 :: card_UNIV begin