# HG changeset patch # User Angeliki KoutsoukouArgyraki # Date 1547674053 0 # Node ID a06b204527e689e10ba41cc9f31a1a94ce79329e # Parent a03a63b81f446eafc88b91b29cf6eeed4a080dd9 updated tagging for 9 theories: Cross3, Determinants, Tagged_Division, Change_of_Vars, Extended_Real_Limits, Fashoda, Finite_Cartesian_Product, Function_Topology, Finite_Product_Measure diff -r a03a63b81f44 -r a06b204527e6 NEWS --- a/NEWS Mon Jan 14 18:35:03 2019 +0000 +++ b/NEWS Wed Jan 16 21:27:33 2019 +0000 @@ -76,9 +76,10 @@ * Code generation: command 'export_code' without file keyword exports code as regular theory export, which can be materialized using the -command-line tool "isabelle export", or browsed in Isabelle/jEdit via -the "isabelle-export:" file-system. To get generated code dumped into -output, use "file \\". Minor INCOMPATIBILITY. +command-line tool "isabelle export" or 'export_files' in the session +ROOT, or browsed in Isabelle/jEdit via the "isabelle-export:" +file-system. To get generated code dumped into output, use "file \\". +Minor INCOMPATIBILITY. * Simplified syntax setup for big operators under image. In rare situations, type conversions are not inserted implicitly any longer diff -r a03a63b81f44 -r a06b204527e6 src/Doc/System/Sessions.thy --- a/src/Doc/System/Sessions.thy Mon Jan 14 18:35:03 2019 +0000 +++ b/src/Doc/System/Sessions.thy Wed Jan 16 21:27:33 2019 +0000 @@ -76,7 +76,8 @@ ; document_files: @'document_files' ('(' dir ')')? (@{syntax embedded}+) ; - export_files: @'export_files' ('(' dir ')')? (@{syntax embedded}+) + export_files: @'export_files' ('(' dir ')')? ('[' nat ']')? \ + (@{syntax embedded}+) \ \<^descr> \isakeyword{session}~\A = B + body\ defines a new session \A\ based on @@ -143,11 +144,14 @@ original directory hierarchy of \base_dir\. The default \base_dir\ is \<^verbatim>\document\ within the session root directory. - \<^descr> \isakeyword{export_files}~\(\\isakeyword{in}~\target_dir) patterns\ writes - theory exports to the file-system: the \target_dir\ specification is - relative to the session root directory; its default is \<^verbatim>\export\. Exports - are selected via \patterns\ as in @{tool_ref export} - (\secref{sec:tool-export}). + \<^descr> \isakeyword{export_files}~\(\\isakeyword{in}~\target_dir) [number] + patterns\ writes theory exports to the file-system: the \target_dir\ + specification is relative to the session root directory; its default is + \<^verbatim>\export\. Exports are selected via \patterns\ as in @{tool_ref export} + (\secref{sec:tool-export}). The number given in brackets (default: 0) + specifies elements that should be pruned from each name: it allows to reduce + the resulting directory hierarchy at the danger of overwriting files due to + loss of uniqueness. \ @@ -563,6 +567,7 @@ -l list exports -n no build of session -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) + -p NUM prune path of exported files by NUM elements -s system build mode for session image -x PATTERN extract files matching pattern (e.g.\ "*:**" for all) @@ -594,6 +599,10 @@ Option \<^verbatim>\-O\ specifies an alternative output directory for option \<^verbatim>\-x\: the default is \<^verbatim>\export\ within the current directory. Each theory creates its own sub-directory hierarchy, using the session-qualified theory name. + + Option \<^verbatim>\-p\ specifies the number of elements that should be pruned from + each name: it allows to reduce the resulting directory hierarchy at the + danger of overwriting files due to loss of uniqueness. \ diff -r a03a63b81f44 -r a06b204527e6 src/HOL/Analysis/Cartesian_Euclidean_Space.thy --- a/src/HOL/Analysis/Cartesian_Euclidean_Space.thy Mon Jan 14 18:35:03 2019 +0000 +++ b/src/HOL/Analysis/Cartesian_Euclidean_Space.thy Wed Jan 16 21:27:33 2019 +0000 @@ -179,117 +179,18 @@ by force qed -lemma%unimportant matrix_mult_transpose_dot_column: - shows "transpose A ** A = (\ i j. inner (column i A) (column j A))" - by (simp add: matrix_matrix_mult_def vec_eq_iff transpose_def column_def inner_vec_def) - -lemma%unimportant matrix_mult_transpose_dot_row: - 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) -lemma%unimportant (* FIX ME needs name*) +lemma%unimportant fixes A :: "'a::{euclidean_space,real_algebra_1}^'n^'m" shows matrix_vector_mult_linear_continuous_at [continuous_intros]: "isCont ((*v) A) z" and matrix_vector_mult_linear_continuous_on [continuous_intros]: "continuous_on S ((*v) A)" by (simp_all add: linear_continuous_at linear_continuous_on) -lemma%unimportant scalar_invertible: - fixes A :: "('a::real_algebra_1)^'m^'n" - assumes "k \ 0" and "invertible A" - shows "invertible (k *\<^sub>R A)" -proof - - obtain A' where "A ** A' = mat 1" and "A' ** A = mat 1" - using assms unfolding invertible_def by auto - with \k \ 0\ - have "(k *\<^sub>R A) ** ((1/k) *\<^sub>R A') = mat 1" "((1/k) *\<^sub>R A') ** (k *\<^sub>R A) = mat 1" - by (simp_all add: assms matrix_scalar_ac) - thus "invertible (k *\<^sub>R A)" - unfolding invertible_def by auto -qed -lemma%unimportant scalar_invertible_iff: - fixes A :: "('a::real_algebra_1)^'m^'n" - assumes "k \ 0" and "invertible A" - shows "invertible (k *\<^sub>R A) \ k \ 0 \ invertible A" - by (simp add: assms scalar_invertible) - -lemma%unimportant vector_transpose_matrix [simp]: "x v* transpose A = A *v x" - unfolding transpose_def vector_matrix_mult_def matrix_vector_mult_def - by simp - -lemma%unimportant transpose_matrix_vector [simp]: "transpose A *v x = x v* A" - unfolding transpose_def vector_matrix_mult_def matrix_vector_mult_def - by simp - -lemma%unimportant vector_scalar_commute: - fixes A :: "'a::{field}^'m^'n" - shows "A *v (c *s x) = c *s (A *v x)" - by (simp add: vector_scalar_mult_def matrix_vector_mult_def mult_ac sum_distrib_left) - -lemma%unimportant scalar_vector_matrix_assoc: - fixes k :: "'a::{field}" and x :: "'a::{field}^'n" and A :: "'a^'m^'n" - shows "(k *s x) v* A = k *s (x v* A)" - by (metis transpose_matrix_vector vector_scalar_commute) - -lemma%unimportant vector_matrix_mult_0 [simp]: "0 v* A = 0" - unfolding vector_matrix_mult_def by (simp add: zero_vec_def) - -lemma%unimportant vector_matrix_mult_0_right [simp]: "x v* 0 = 0" - unfolding vector_matrix_mult_def by (simp add: zero_vec_def) - -lemma%unimportant vector_matrix_mul_rid [simp]: - fixes v :: "('a::semiring_1)^'n" - shows "v v* mat 1 = v" - by (metis matrix_vector_mul_lid transpose_mat vector_transpose_matrix) - -lemma%unimportant scaleR_vector_matrix_assoc: - fixes k :: real and x :: "real^'n" and A :: "real^'m^'n" - shows "(k *\<^sub>R x) v* A = k *\<^sub>R (x v* A)" - by (metis matrix_vector_mult_scaleR transpose_matrix_vector) - -lemma%important vector_scaleR_matrix_ac: - fixes k :: real and x :: "real^'n" and A :: "real^'m^'n" - shows "x v* (k *\<^sub>R A) = k *\<^sub>R (x v* A)" -proof%unimportant - - have "x v* (k *\<^sub>R A) = (k *\<^sub>R x) v* A" - unfolding vector_matrix_mult_def - by (simp add: algebra_simps) - with scaleR_vector_matrix_assoc - show "x v* (k *\<^sub>R A) = k *\<^sub>R (x v* A)" - by auto -qed - - -subsection%important\Some bounds on components etc. relative to operator norm\ +subsection%important\Bounds on components etc.\ relative to operator norm\ lemma%important norm_column_le_onorm: fixes A :: "real^'n^'m" @@ -366,26 +267,6 @@ finally show "norm (A *v x) \ CARD('m) * real (CARD('n)) * B * norm x" . qed -subsection%important \lambda skolemization on cartesian products\ - -lemma%important lambda_skolem: "(\i. \x. P i x) \ - (\x::'a ^ 'n. \i. P i (x $ i))" (is "?lhs \ ?rhs") -proof%unimportant - - 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%unimportant rational_approximation: assumes "e > 0" @@ -416,36 +297,6 @@ lemma%unimportant vector_sub_project_orthogonal_cart: "(b::real^'n) \ (x - ((b \ x) / (b \ b)) *s b) = 0" unfolding inner_simps scalar_mult_eq_scaleR by auto - -text \The same result in terms of square matrices.\ - - -text \Considering an n-element vector as an n-by-1 or 1-by-n matrix.\ - -definition%unimportant "rowvector v = (\ i j. (v$j))" - -definition%unimportant "columnvector v = (\ i j. (v$i))" - -lemma%unimportant transpose_columnvector: "transpose(columnvector v) = rowvector v" - by (simp add: transpose_def rowvector_def columnvector_def vec_eq_iff) - -lemma%unimportant transpose_rowvector: "transpose(rowvector v) = columnvector v" - by (simp add: transpose_def columnvector_def rowvector_def vec_eq_iff) - -lemma%unimportant dot_rowvector_columnvector: "columnvector (A *v v) = A ** columnvector v" - by (vector columnvector_def matrix_matrix_mult_def matrix_vector_mult_def) - -lemma%unimportant dot_matrix_product: - "(x::real^'n) \ y = (((rowvector x ::real^'n^1) ** (columnvector y :: real^1^'n))$1)$1" - by (vector matrix_matrix_mult_def rowvector_def columnvector_def inner_vec_def) - -lemma%unimportant dot_matrix_vector_mul: - 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 .. - lemma%unimportant infnorm_cart:"infnorm (x::real^'n) = Sup {\x$i\ |i. i\UNIV}" by (simp add: infnorm_def inner_axis Basis_vec_def) (metis (lifting) inner_axis real_inner_1_right) @@ -626,16 +477,16 @@ by (simp add: is_interval_def Ball_def Basis_vec_def inner_axis imp_ex) lemma%unimportant closed_halfspace_component_le_cart: "closed {x::real^'n. x$i \ a}" - by (simp add: closed_Collect_le continuous_on_const continuous_on_id continuous_on_component) + by (simp add: closed_Collect_le continuous_on_component) lemma%unimportant closed_halfspace_component_ge_cart: "closed {x::real^'n. x$i \ a}" - by (simp add: closed_Collect_le continuous_on_const continuous_on_id continuous_on_component) + by (simp add: closed_Collect_le continuous_on_component) lemma%unimportant open_halfspace_component_lt_cart: "open {x::real^'n. x$i < a}" - by (simp add: open_Collect_less continuous_on_const continuous_on_id continuous_on_component) + by (simp add: open_Collect_less continuous_on_component) lemma%unimportant open_halfspace_component_gt_cart: "open {x::real^'n. x$i > a}" - by (simp add: open_Collect_less continuous_on_const continuous_on_id continuous_on_component) + by (simp add: open_Collect_less continuous_on_component) lemma%unimportant Lim_component_le_cart: fixes f :: "'a \ real^'n" @@ -676,79 +527,6 @@ unfolding Collect_all_eq by (simp add: closed_INT) qed -lemma%important dim_substandard_cart: "vec.dim {x::'a::field^'n. \i. i \ d \ x$i = 0} = card d" - (is "vec.dim ?A = _") -proof%unimportant (rule vec.dim_unique) - let ?B = "((\x. axis x 1) ` d)" - have subset_basis: "?B \ cart_basis" - by (auto simp: cart_basis_def) - show "?B \ ?A" - by (auto simp: axis_def) - show "vec.independent ((\x. axis x 1) ` d)" - using subset_basis - by (rule vec.independent_mono[OF vec.independent_Basis]) - have "x \ vec.span ?B" if "\i. i \ d \ x $ i = 0" for x::"'a^'n" - proof - - have "finite ?B" - using subset_basis finite_cart_basis - by (rule finite_subset) - have "x = (\i\UNIV. x $ i *s axis i 1)" - by (rule basis_expansion[symmetric]) - also have "\ = (\i\d. (x $ i) *s axis i 1)" - by (rule sum.mono_neutral_cong_right) (auto simp: that) - also have "\ \ vec.span ?B" - by (simp add: vec.span_sum vec.span_clauses) - finally show "x \ vec.span ?B" . - qed - 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" - "(\x. inverse(m) *s x + (-(inverse(m) *s c))) \ (\x. m *s x + c) = id" - using m0 - by (auto simp add: fun_eq_iff vector_add_ldistrib diff_conv_add_uminus simp del: add_uminus_conv_diff) - -lemma%important vector_affinity_eq: - assumes m0: "(m::'a::field) \ 0" - shows "m *s x + c = y \ x = inverse m *s y + -(inverse m *s c)" -proof%unimportant - assume h: "m *s x + c = y" - 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) -next - assume h: "x = inverse m *s y + - (inverse m *s c)" - show "m *s x + c = y" unfolding h - using m0 by (simp add: vector_smult_assoc vector_ssub_ldistrib) -qed - -lemma%unimportant 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 - -lemma%unimportant vector_cart: - fixes f :: "real^'n \ real" - shows "(\ i. f (axis i 1)) = (\i\Basis. f i *\<^sub>R i)" - unfolding euclidean_eq_iff[where 'a="real^'n"] - by simp (simp add: Basis_vec_def inner_axis) - -lemma%unimportant const_vector_cart:"((\ i. d)::real^'n) = (\i\Basis. d *\<^sub>R i)" - by (rule vector_cart) - subsection%important "Convex Euclidean Space" lemma%unimportant Cart_1:"(1::real^'n) = \Basis" @@ -801,7 +579,7 @@ qed -subsection%important \Component of the differential must be zero if it exists at a local +text%important \Component of the differential must be zero if it exists at a local maximum or minimum for that corresponding component\ lemma%important differential_zero_maxmin_cart: @@ -813,282 +591,8 @@ 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) - -lemma exhaust_2: - fixes x :: 2 - 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 -qed - -lemma forall_2: "(\i::2. P i) \ P 1 \ P 2" - by (metis exhaust_2) - -lemma exhaust_3: - fixes x :: 3 - 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 show ?case by auto -qed - -lemma forall_3: "(\i::3. P i) \ P 1 \ P 2 \ P 3" - by (metis exhaust_3) - -lemma UNIV_1 [simp]: "UNIV = {1::1}" - by (auto simp add: num1_eq_iff) - -lemma UNIV_2: "UNIV = {1::2, 2::2}" - using exhaust_2 by auto - -lemma UNIV_3: "UNIV = {1::3, 2::3, 3::3}" - using exhaust_3 by auto - -lemma sum_1: "sum f (UNIV::1 set) = f 1" - unfolding UNIV_1 by simp - -lemma sum_2: "sum f (UNIV::2 set) = f 1 + f 2" - unfolding UNIV_2 by simp - -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 :: cart_one -begin - -instance -proof - show "CARD(1) = Suc 0" by auto -qed - -end - -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))" - 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 - -lemma norm_vector_1: "norm (x :: _^1) = norm (x$1)" - by (simp add: norm_vec_def) - -lemma dist_vector_1: - fixes x :: "'a::real_normed_vector^1" - shows "dist x y = dist (x$1) (y$1)" - by (simp add: dist_norm norm_vector_1) - -lemma norm_real: "norm(x::real ^ 1) = \x$1\" - by (simp add: norm_vector_1) - -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]: - fixes x :: "'a^1" shows "vec (x $ 1) = x" - by (metis vec_def vector_one) - lemma vec_cbox_1_eq [simp]: shows "vec ` cbox u v = cbox (vec u) (vec v ::real^1)" by (force simp: Basis_vec_def cart_eq_inner_axis [symmetric] mem_box) @@ -1119,76 +623,6 @@ qed qed simp -lemma tendsto_at_within_vector_1: - fixes S :: "'a :: metric_space set" - assumes "(f \ fx) (at x within S)" - shows "((\y::'a^1. \ i. f (y $ 1)) \ (vec fx::'a^1)) (at (vec x) within vec ` S)" -proof (rule topological_tendstoI) - fix T :: "('a^1) set" - assume "open T" "vec fx \ T" - have "\\<^sub>F x in at x within S. f x \ (\x. x $ 1) ` T" - using \open T\ \vec fx \ T\ assms open_image_vec_nth tendsto_def by fastforce - then show "\\<^sub>F x::'a^1 in at (vec x) within vec ` S. (\ i. f (x $ 1)) \ T" - unfolding eventually_at dist_norm [symmetric] - by (rule ex_forward) - (use \open T\ in - \fastforce simp: dist_norm dist_vec_def L2_set_def image_iff vector_one open_vec_def\) -qed - -lemma has_derivative_vector_1: - assumes der_g: "(g has_derivative (\x. x * g' a)) (at a within S)" - 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 (drule tendsto_at_within_vector_1, vector) - apply (auto simp: algebra_simps eventually_at tendsto_def) - done - - -subsection%unimportant\Explicit vector construction from lists\ - -definition "vector l = (\ i. foldr (\x f n. fun_upd (f (n+1)) n x) l (\n x. 0) 1 i)" - -lemma vector_1 [simp]: "(vector[x]) $1 = x" - unfolding vector_def by simp - -lemma vector_2 [simp]: "(vector[x,y]) $1 = x" "(vector[x,y] :: 'a^2)$2 = (y::'a::zero)" - unfolding vector_def by simp_all - -lemma vector_3 [simp]: - "(vector [x,y,z] ::('a::zero)^3)$1 = x" - "(vector [x,y,z] ::('a::zero)^3)$2 = y" - "(vector [x,y,z] ::('a::zero)^3)$3 = z" - unfolding vector_def by simp_all - -lemma forall_vector_1: "(\v::'a::zero^1. P v) \ (\x. P(vector[x]))" - 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 - -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 - -lemma bounded_linear_component_cart[intro]: "bounded_linear (\x::real^'n. x $ k)" - apply (rule bounded_linear_intro[where K=1]) - using component_le_norm_cart[of _ k] unfolding real_norm_def by auto lemma interval_split_cart: "{a..b::real^'n} \ {x. x$k \ c} = {a .. (\ i. if i = k then min (b$k) c else b$i)}" @@ -1201,6 +635,5 @@ lemmas cartesian_euclidean_space_uniform_limit_intros[uniform_limit_intros] = bounded_linear.uniform_limit[OF blinfun.bounded_linear_right] bounded_linear.uniform_limit[OF bounded_linear_vec_nth] - bounded_linear.uniform_limit[OF bounded_linear_component_cart] end diff -r a03a63b81f44 -r a06b204527e6 src/HOL/Analysis/Cartesian_Space.thy --- a/src/HOL/Analysis/Cartesian_Space.thy Mon Jan 14 18:35:03 2019 +0000 +++ b/src/HOL/Analysis/Cartesian_Space.thy Wed Jan 16 21:27:33 2019 +0000 @@ -6,11 +6,15 @@ Author: Fabian Immler, TUM *) +section "Linear Algebra on Finite Cartesian Products" + theory Cartesian_Space imports Finite_Cartesian_Product Linear_Algebra begin +subsection \Type @{typ \'a ^ 'n\} and fields as vector spaces\ + definition%unimportant "cart_basis = {axis i 1 | i. i\UNIV}" lemma%unimportant finite_cart_basis: "finite (cart_basis)" unfolding cart_basis_def @@ -20,7 +24,7 @@ unfolding cart_basis_def Setcompr_eq_image by (rule card_image) (auto simp: inj_on_def axis_eq_axis) -interpretation vec: vector_space "(*s) " +interpretation%important vec: vector_space "(*s) " by unfold_locales (vector algebra_simps)+ lemma%unimportant independent_cart_basis: @@ -448,8 +452,8 @@ finally show ?thesis . qed -interpretation vector_space_over_itself: vector_space "(*) :: 'a::field => 'a => 'a" - by unfold_locales (simp_all add: algebra_simps) +interpretation%important vector_space_over_itself: vector_space "(*) :: 'a::field \ 'a \ 'a" +by unfold_locales (simp_all add: algebra_simps) lemmas [simp del] = vector_space_over_itself.scale_scale @@ -460,4 +464,470 @@ 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) + + +subsection%unimportant \Lemmas for working on \real^1/2/3\\ + +lemma exhaust_2: + fixes x :: 2 + 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 +qed + +lemma forall_2: "(\i::2. P i) \ P 1 \ P 2" + by (metis exhaust_2) + +lemma exhaust_3: + fixes x :: 3 + 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 show ?case by auto +qed + +lemma forall_3: "(\i::3. P i) \ P 1 \ P 2 \ P 3" + by (metis exhaust_3) + +lemma UNIV_1 [simp]: "UNIV = {1::1}" + by (auto simp add: num1_eq_iff) + +lemma UNIV_2: "UNIV = {1::2, 2::2}" + using exhaust_2 by auto + +lemma UNIV_3: "UNIV = {1::3, 2::3, 3::3}" + using exhaust_3 by auto + +lemma sum_1: "sum f (UNIV::1 set) = f 1" + unfolding UNIV_1 by simp + +lemma sum_2: "sum f (UNIV::2 set) = f 1 + f 2" + unfolding UNIV_2 by simp + +lemma sum_3: "sum f (UNIV::3 set) = f 1 + f 2 + f 3" + unfolding UNIV_3 by (simp add: ac_simps) + +subsection%unimportant\The collapse of the general concepts to dimension one\ + +lemma vector_one: "(x::'a ^1) = (\ i. (x$1))" + 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 + +lemma norm_vector_1: "norm (x :: _^1) = norm (x$1)" + by (simp add: norm_vec_def) + +lemma dist_vector_1: + fixes x :: "'a::real_normed_vector^1" + shows "dist x y = dist (x$1) (y$1)" + by (simp add: dist_norm norm_vector_1) + +lemma norm_real: "norm(x::real ^ 1) = \x$1\" + by (simp add: norm_vector_1) + +lemma dist_real: "dist(x::real ^ 1) y = \(x$1) - (y$1)\" + by (auto simp add: norm_real dist_norm) + + +subsection%unimportant\Routine results connecting the types \<^typ>\real^1\ and \<^typ>\real\\ + +lemma vector_one_nth [simp]: + fixes x :: "'a^1" shows "vec (x $ 1) = x" + by (metis vec_def vector_one) + +lemma tendsto_at_within_vector_1: + fixes S :: "'a :: metric_space set" + assumes "(f \ fx) (at x within S)" + shows "((\y::'a^1. \ i. f (y $ 1)) \ (vec fx::'a^1)) (at (vec x) within vec ` S)" +proof (rule topological_tendstoI) + fix T :: "('a^1) set" + assume "open T" "vec fx \ T" + have "\\<^sub>F x in at x within S. f x \ (\x. x $ 1) ` T" + using \open T\ \vec fx \ T\ assms open_image_vec_nth tendsto_def by fastforce + then show "\\<^sub>F x::'a^1 in at (vec x) within vec ` S. (\ i. f (x $ 1)) \ T" + unfolding eventually_at dist_norm [symmetric] + by (rule ex_forward) + (use \open T\ in + \fastforce simp: dist_norm dist_vec_def L2_set_def image_iff vector_one open_vec_def\) +qed + +lemma has_derivative_vector_1: + assumes der_g: "(g has_derivative (\x. x * g' a)) (at a within S)" + 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 (drule tendsto_at_within_vector_1, vector) + apply (auto simp: algebra_simps eventually_at tendsto_def) + done + + +subsection%unimportant\Explicit vector construction from lists\ + +definition "vector l = (\ i. foldr (\x f n. fun_upd (f (n+1)) n x) l (\n x. 0) 1 i)" + +lemma vector_1 [simp]: "(vector[x]) $1 = x" + unfolding vector_def by simp + +lemma vector_2 [simp]: "(vector[x,y]) $1 = x" "(vector[x,y] :: 'a^2)$2 = (y::'a::zero)" + unfolding vector_def by simp_all + +lemma vector_3 [simp]: + "(vector [x,y,z] ::('a::zero)^3)$1 = x" + "(vector [x,y,z] ::('a::zero)^3)$2 = y" + "(vector [x,y,z] ::('a::zero)^3)$3 = z" + unfolding vector_def by simp_all + +lemma forall_vector_1: "(\v::'a::zero^1. P v) \ (\x. P(vector[x]))" + 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 + +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 + +subsection%unimportant \lambda skolemization on cartesian products\ + +lemma%important lambda_skolem: "(\i. \x. P i x) \ + (\x::'a ^ 'n. \i. P i (x $ i))" (is "?lhs \ ?rhs") +proof%unimportant - + 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 + + +text \The same result in terms of square matrices.\ + + +text \Considering an n-element vector as an n-by-1 or 1-by-n matrix.\ + +definition%unimportant "rowvector v = (\ i j. (v$j))" + +definition%unimportant "columnvector v = (\ i j. (v$i))" + +lemma%unimportant transpose_columnvector: "transpose(columnvector v) = rowvector v" + by (simp add: transpose_def rowvector_def columnvector_def vec_eq_iff) + +lemma%unimportant transpose_rowvector: "transpose(rowvector v) = columnvector v" + by (simp add: transpose_def columnvector_def rowvector_def vec_eq_iff) + +lemma%unimportant dot_rowvector_columnvector: "columnvector (A *v v) = A ** columnvector v" + by (vector columnvector_def matrix_matrix_mult_def matrix_vector_mult_def) + +lemma%unimportant dot_matrix_product: + "(x::real^'n) \ y = (((rowvector x ::real^'n^1) ** (columnvector y :: real^1^'n))$1)$1" + by (vector matrix_matrix_mult_def rowvector_def columnvector_def inner_vec_def) + +lemma%unimportant dot_matrix_vector_mul: + 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 .. + + +lemma%important dim_substandard_cart: "vec.dim {x::'a::field^'n. \i. i \ d \ x$i = 0} = card d" + (is "vec.dim ?A = _") +proof%unimportant (rule vec.dim_unique) + let ?B = "((\x. axis x 1) ` d)" + have subset_basis: "?B \ cart_basis" + by (auto simp: cart_basis_def) + show "?B \ ?A" + by (auto simp: axis_def) + show "vec.independent ((\x. axis x 1) ` d)" + using subset_basis + by (rule vec.independent_mono[OF vec.independent_Basis]) + have "x \ vec.span ?B" if "\i. i \ d \ x $ i = 0" for x::"'a^'n" + proof - + have "finite ?B" + using subset_basis finite_cart_basis + by (rule finite_subset) + have "x = (\i\UNIV. x $ i *s axis i 1)" + by (rule basis_expansion[symmetric]) + also have "\ = (\i\d. (x $ i) *s axis i 1)" + by (rule sum.mono_neutral_cong_right) (auto simp: that) + also have "\ \ vec.span ?B" + by (simp add: vec.span_sum vec.span_clauses) + finally show "x \ vec.span ?B" . + qed + then show "?A \ vec.span ?B" by auto +qed (simp add: card_image inj_on_def axis_eq_axis) + +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" + "(\x. inverse(m) *s x + (-(inverse(m) *s c))) \ (\x. m *s x + c) = id" + using m0 + by (auto simp add: fun_eq_iff vector_add_ldistrib diff_conv_add_uminus simp del: add_uminus_conv_diff) + +lemma%important vector_affinity_eq: + assumes m0: "(m::'a::field) \ 0" + shows "m *s x + c = y \ x = inverse m *s y + -(inverse m *s c)" +proof%unimportant + assume h: "m *s x + c = y" + 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) +next + assume h: "x = inverse m *s y + - (inverse m *s c)" + show "m *s x + c = y" unfolding h + using m0 by (simp add: vector_smult_assoc vector_ssub_ldistrib) +qed + +lemma%unimportant 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 + +lemma%unimportant vector_cart: + fixes f :: "real^'n \ real" + shows "(\ i. f (axis i 1)) = (\i\Basis. f i *\<^sub>R i)" + unfolding euclidean_eq_iff[where 'a="real^'n"] + by simp (simp add: Basis_vec_def inner_axis) + +lemma%unimportant const_vector_cart:"((\ i. d)::real^'n) = (\i\Basis. d *\<^sub>R i)" + by (rule vector_cart) + end \ No newline at end of file diff -r a03a63b81f44 -r a06b204527e6 src/HOL/Analysis/Change_Of_Vars.thy --- a/src/HOL/Analysis/Change_Of_Vars.thy Mon Jan 14 18:35:03 2019 +0000 +++ b/src/HOL/Analysis/Change_Of_Vars.thy Wed Jan 16 21:27:33 2019 +0000 @@ -10,8 +10,11 @@ begin subsection%important\Induction on matrix row operations\ - -lemma%unimportant induct_matrix_row_operations: +(*FIX move first 3 lemmas of subsection to linear algebra, contain technical tools on matrix operations. +Keep the rest of the subsection contents in this theory but rename the subsection, they refer +to lebesgue measure +*) +lemma induct_matrix_row_operations: fixes P :: "real^'n^'n \ bool" assumes zero_row: "\A i. row i A = 0 \ P A" and diagonal: "\A. (\i j. i \ j \ A$i$j = 0) \ P A" @@ -120,7 +123,7 @@ by blast qed -lemma%unimportant induct_matrix_elementary: +lemma induct_matrix_elementary: fixes P :: "real^'n^'n \ bool" assumes mult: "\A B. \P A; P B\ \ P(A ** B)" and zero_row: "\A i. row i A = 0 \ P A" @@ -151,7 +154,7 @@ by (rule induct_matrix_row_operations [OF zero_row diagonal swap row]) qed -lemma%unimportant induct_matrix_elementary_alt: +lemma induct_matrix_elementary_alt: fixes P :: "real^'n^'n \ bool" assumes mult: "\A B. \P A; P B\ \ P(A ** B)" and zero_row: "\A i. row i A = 0 \ P A" @@ -185,11 +188,11 @@ by (rule induct_matrix_elementary) (auto intro: assms *) qed -lemma%unimportant matrix_vector_mult_matrix_matrix_mult_compose: +lemma matrix_vector_mult_matrix_matrix_mult_compose: "(*v) (A ** B) = (*v) A \ (*v) B" by (auto simp: matrix_vector_mul_assoc) -lemma%unimportant induct_linear_elementary: +lemma induct_linear_elementary: fixes f :: "real^'n \ real^'n" assumes "linear f" and comp: "\f g. \linear f; linear g; P f; P g\ \ P(f \ g)" @@ -250,14 +253,14 @@ qed -proposition%important +proposition (*FIX needs name *) fixes a :: "real^'n" assumes "m \ n" and ab_ne: "cbox a b \ {}" and an: "0 \ a$n" shows measurable_shear_interval: "(\x. \ i. if i = m then x$m + x$n else x$i) ` (cbox a b) \ lmeasurable" (is "?f ` _ \ _") and measure_shear_interval: "measure lebesgue ((\x. \ i. if i = m then x$m + x$n else x$i) ` cbox a b) = measure lebesgue (cbox a b)" (is "?Q") -proof%unimportant - +proof - have lin: "linear ?f" by (rule linearI) (auto simp: plus_vec_def scaleR_vec_def algebra_simps) show fab: "?f ` cbox a b \ lmeasurable" @@ -359,13 +362,13 @@ qed -proposition%important +proposition (*FIX needs name *) fixes S :: "(real^'n) set" assumes "S \ lmeasurable" shows measurable_stretch: "((\x. \ k. m k * x$k) ` S) \ lmeasurable" (is "?f ` S \ _") and measure_stretch: "measure lebesgue ((\x. \ k. m k * x$k) ` S) = \prod m UNIV\ * measure lebesgue S" (is "?MEQ") -proof%unimportant - +proof - have "(?f ` S) \ lmeasurable \ ?MEQ" proof (cases "\k. m k \ 0") case True @@ -463,12 +466,12 @@ qed -proposition%important +proposition (*FIX needs name *) fixes f :: "real^'n::{finite,wellorder} \ real^'n::_" assumes "linear f" "S \ lmeasurable" shows measurable_linear_image: "(f ` S) \ lmeasurable" and measure_linear_image: "measure lebesgue (f ` S) = \det (matrix f)\ * measure lebesgue S" (is "?Q f S") -proof%unimportant - +proof - have "\S \ lmeasurable. (f ` S) \ lmeasurable \ ?Q f S" proof (rule induct_linear_elementary [OF \linear f\]; intro ballI) fix f g and S :: "(real,'n) vec set" @@ -611,7 +614,7 @@ qed -lemma%unimportant +lemma (* needs name *) fixes f :: "real^'n::{finite,wellorder} \ real^'n::_" assumes f: "orthogonal_transformation f" and S: "S \ lmeasurable" shows measurable_orthogonal_image: "f ` S \ lmeasurable" @@ -634,10 +637,10 @@ inductive%important gdelta :: "'a::topological_space set \ bool" where "(\n::nat. open (F n)) \ gdelta (\(F ` UNIV))" -lemma%important fsigma_Union_compact: +proposition fsigma_Union_compact: fixes S :: "'a::{real_normed_vector,heine_borel} set" shows "fsigma S \ (\F::nat \ 'a set. range F \ Collect compact \ S = \(F ` UNIV))" -proof%unimportant safe +proof safe assume "fsigma S" then obtain F :: "nat \ 'a set" where F: "range F \ Collect closed" "S = \(F ` UNIV)" by (meson fsigma.cases image_subsetI mem_Collect_eq) @@ -668,7 +671,7 @@ by (simp add: compact_imp_closed fsigma.intros image_subset_iff) qed -lemma%unimportant gdelta_imp_fsigma: "gdelta S \ fsigma (- S)" +lemma gdelta_imp_fsigma: "gdelta S \ fsigma (- S)" proof (induction rule: gdelta.induct) case (1 F) have "- \(F ` UNIV) = (\i. -(F i))" @@ -677,7 +680,7 @@ by (simp add: fsigma.intros closed_Compl 1) qed -lemma%unimportant fsigma_imp_gdelta: "fsigma S \ gdelta (- S)" +lemma fsigma_imp_gdelta: "fsigma S \ gdelta (- S)" proof (induction rule: fsigma.induct) case (1 F) have "- \(F ` UNIV) = (\i. -(F i))" @@ -686,11 +689,11 @@ by (simp add: 1 gdelta.intros open_closed) qed -lemma%unimportant gdelta_complement: "gdelta(- S) \ fsigma S" +lemma gdelta_complement: "gdelta(- S) \ fsigma S" using fsigma_imp_gdelta gdelta_imp_fsigma by force text\A Lebesgue set is almost an \F_sigma\ or \G_delta\.\ -lemma%unimportant lebesgue_set_almost_fsigma: +lemma lebesgue_set_almost_fsigma: assumes "S \ sets lebesgue" obtains C T where "fsigma C" "negligible T" "C \ T = S" "disjnt C T" proof - @@ -725,7 +728,7 @@ qed qed -lemma%unimportant lebesgue_set_almost_gdelta: +lemma lebesgue_set_almost_gdelta: assumes "S \ sets lebesgue" obtains C T where "gdelta C" "negligible T" "S \ T = C" "disjnt S T" proof - @@ -743,12 +746,12 @@ qed -proposition%important measure_semicontinuous_with_hausdist_explicit: +proposition measure_semicontinuous_with_hausdist_explicit: assumes "bounded S" and neg: "negligible(frontier S)" and "e > 0" obtains d where "d > 0" "\T. \T \ lmeasurable; \y. y \ T \ \x. x \ S \ dist x y < d\ \ measure lebesgue T < measure lebesgue S + e" -proof%unimportant (cases "S = {}") +proof (cases "S = {}") case True with that \e > 0\ show ?thesis by force next @@ -812,10 +815,10 @@ qed qed -proposition%important lebesgue_regular_inner: +proposition lebesgue_regular_inner: assumes "S \ sets lebesgue" obtains K C where "negligible K" "\n::nat. compact(C n)" "S = (\n. C n) \ K" -proof%unimportant - +proof - have "\T. closed T \ T \ S \ (S - T) \ lmeasurable \ measure lebesgue (S - T) < (1/2)^n" for n using sets_lebesgue_inner_closed assms by (metis sets_lebesgue_inner_closed zero_less_divide_1_iff zero_less_numeral zero_less_power) @@ -865,7 +868,7 @@ qed -lemma%unimportant sets_lebesgue_continuous_image: +lemma sets_lebesgue_continuous_image: assumes T: "T \ sets lebesgue" and contf: "continuous_on S f" and negim: "\T. \negligible T; T \ S\ \ negligible(f ` T)" and "T \ S" shows "f ` T \ sets lebesgue" @@ -890,7 +893,7 @@ by (simp add: Teq image_Un image_Union) qed -lemma%unimportant differentiable_image_in_sets_lebesgue: +lemma differentiable_image_in_sets_lebesgue: fixes f :: "'m::euclidean_space \ 'n::euclidean_space" assumes S: "S \ sets lebesgue" and dim: "DIM('m) \ DIM('n)" and f: "f differentiable_on S" shows "f`S \ sets lebesgue" @@ -902,7 +905,7 @@ by (auto simp: intro!: negligible_differentiable_image_negligible [OF dim]) qed auto -lemma%unimportant sets_lebesgue_on_continuous_image: +lemma sets_lebesgue_on_continuous_image: assumes S: "S \ sets lebesgue" and X: "X \ sets (lebesgue_on S)" and contf: "continuous_on S f" and negim: "\T. \negligible T; T \ S\ \ negligible(f ` T)" shows "f ` X \ sets (lebesgue_on (f ` S))" @@ -917,7 +920,7 @@ by (auto simp: sets_restrict_space_iff) qed -lemma%unimportant differentiable_image_in_sets_lebesgue_on: +lemma differentiable_image_in_sets_lebesgue_on: fixes f :: "'m::euclidean_space \ 'n::euclidean_space" assumes S: "S \ sets lebesgue" and X: "X \ sets (lebesgue_on S)" and dim: "DIM('m) \ DIM('n)" and f: "f differentiable_on S" @@ -931,7 +934,7 @@ qed -proposition%important +proposition (*FIX needs name *) fixes f :: "real^'n::{finite,wellorder} \ real^'n::_" assumes S: "S \ lmeasurable" and deriv: "\x. x \ S \ (f has_derivative f' x) (at x within S)" @@ -941,7 +944,7 @@ "f ` S \ lmeasurable" and measure_bounded_differentiable_image: "measure lebesgue (f ` S) \ B * measure lebesgue S" (is "?M") -proof%unimportant - +proof - have "f ` S \ lmeasurable \ measure lebesgue (f ` S) \ B * measure lebesgue S" proof (cases "B < 0") case True @@ -1167,13 +1170,13 @@ then show "f ` S \ lmeasurable" ?M by blast+ qed -lemma%important +proposition (*FIX needs name *) fixes f :: "real^'n::{finite,wellorder} \ real^'n::_" assumes S: "S \ lmeasurable" and deriv: "\x. x \ S \ (f has_derivative f' x) (at x within S)" and int: "(\x. \det (matrix (f' x))\) integrable_on S" shows m_diff_image_weak: "f ` S \ lmeasurable \ measure lebesgue (f ` S) \ integral S (\x. \det (matrix (f' x))\)" -proof%unimportant - +proof - let ?\ = "measure lebesgue" have aint_S: "(\x. \det (matrix (f' x))\) absolutely_integrable_on S" using int unfolding absolutely_integrable_on_def by auto @@ -1365,7 +1368,7 @@ qed -theorem%important +theorem (*FIX needs name *) fixes f :: "real^'n::{finite,wellorder} \ real^'n::_" assumes S: "S \ sets lebesgue" and deriv: "\x. x \ S \ (f has_derivative f' x) (at x within S)" @@ -1373,7 +1376,7 @@ shows measurable_differentiable_image: "f ` S \ lmeasurable" and measure_differentiable_image: "measure lebesgue (f ` S) \ integral S (\x. \det (matrix (f' x))\)" (is "?M") -proof%unimportant - +proof - let ?I = "\n::nat. cbox (vec (-n)) (vec n) \ S" let ?\ = "measure lebesgue" have "x \ cbox (vec (- real (nat \norm x\))) (vec (real (nat \norm x\)))" for x :: "real^'n::_" @@ -1418,7 +1421,7 @@ qed -lemma%unimportant borel_measurable_simple_function_limit_increasing: +lemma borel_measurable_simple_function_limit_increasing: fixes f :: "'a::euclidean_space \ real" shows "(f \ borel_measurable lebesgue \ (\x. 0 \ f x)) \ (\g. (\n x. 0 \ g n x \ g n x \ f x) \ (\n x. g n x \ (g(Suc n) x)) \ @@ -1617,7 +1620,7 @@ subsection%important\Borel measurable Jacobian determinant\ -lemma%unimportant lemma_partial_derivatives0: +lemma lemma_partial_derivatives0: fixes f :: "'a::euclidean_space \ 'b::euclidean_space" assumes "linear f" and lim0: "((\x. f x /\<^sub>R norm x) \ 0) (at 0 within S)" and lb: "\v. v \ 0 \ (\k>0. \e>0. \x. x \ S - {0} \ norm x < e \ k * norm x \ \v \ x\)" @@ -1690,7 +1693,7 @@ mem_Collect_eq module_hom_zero span_base span_raw_def) qed -lemma%unimportant lemma_partial_derivatives: +lemma lemma_partial_derivatives: fixes f :: "'a::euclidean_space \ 'b::euclidean_space" assumes "linear f" and lim: "((\x. f (x - a) /\<^sub>R norm (x - a)) \ 0) (at a within S)" and lb: "\v. v \ 0 \ (\k>0. \e>0. \x \ S - {a}. norm(a - x) < e \ k * norm(a - x) \ \v \ (x - a)\)" @@ -1708,12 +1711,12 @@ qed -proposition%important borel_measurable_partial_derivatives: +proposition borel_measurable_partial_derivatives: fixes f :: "real^'m::{finite,wellorder} \ real^'n" assumes S: "S \ sets lebesgue" and f: "\x. x \ S \ (f has_derivative f' x) (at x within S)" shows "(\x. (matrix(f' x)$m$n)) \ borel_measurable (lebesgue_on S)" -proof%unimportant - +proof - have contf: "continuous_on S f" using continuous_on_eq_continuous_within f has_derivative_continuous by blast have "{x \ S. (matrix (f' x)$m$n) \ b} \ sets lebesgue" for b @@ -2299,7 +2302,7 @@ qed -theorem%important borel_measurable_det_Jacobian: +theorem borel_measurable_det_Jacobian: fixes f :: "real^'n::{finite,wellorder} \ real^'n::_" assumes S: "S \ sets lebesgue" and f: "\x. x \ S \ (f has_derivative f' x) (at x within S)" shows "(\x. det(matrix(f' x))) \ borel_measurable (lebesgue_on S)" @@ -2313,7 +2316,7 @@ assumes "S \ sets lebesgue" shows "f \ borel_measurable (lebesgue_on S) \ (\T. T \ sets borel \ {x \ S. f x \ T} \ sets lebesgue)" -proof%unimportant - +proof - have "{x. (if x \ S then f x else 0) \ T} \ sets lebesgue \ {x \ S. f x \ T} \ sets lebesgue" if "T \ sets borel" for T proof (cases "0 \ T") @@ -2335,7 +2338,7 @@ by blast qed -lemma%unimportant sets_lebesgue_almost_borel: +lemma sets_lebesgue_almost_borel: assumes "S \ sets lebesgue" obtains B N where "B \ sets borel" "negligible N" "B \ N = S" proof - @@ -2345,7 +2348,7 @@ by (metis negligible_iff_null_sets negligible_subset null_sets_completionI that) qed -lemma%unimportant double_lebesgue_sets: +lemma double_lebesgue_sets: assumes S: "S \ sets lebesgue" and T: "T \ sets lebesgue" and fim: "f ` S \ T" shows "(\U. U \ sets lebesgue \ U \ T \ {x \ S. f x \ U} \ sets lebesgue) \ f \ borel_measurable (lebesgue_on S) \ @@ -2390,7 +2393,7 @@ subsection%important\Simplest case of Sard's theorem (we don't need continuity of derivative)\ -lemma%important Sard_lemma00: +lemma Sard_lemma00: fixes P :: "'b::euclidean_space set" assumes "a \ 0" and a: "a *\<^sub>R i \ 0" and i: "i \ Basis" and P: "P \ {x. a *\<^sub>R i \ x = 0}" @@ -2398,7 +2401,7 @@ obtains S where "S \ lmeasurable" and "{z. norm z \ m \ (\t \ P. norm(z - t) \ e)} \ S" and "measure lebesgue S \ (2 * e) * (2 * m) ^ (DIM('b) - 1)" -proof%unimportant - +proof - have "a > 0" using assms by simp let ?v = "(\j\Basis. (if j = i then e else m) *\<^sub>R j)" @@ -2426,7 +2429,7 @@ qed text\As above, but reorienting the vector (HOL Light's @text{GEOM\_BASIS\_MULTIPLE\_TAC})\ -lemma%unimportant Sard_lemma0: +lemma Sard_lemma0: fixes P :: "(real^'n::{finite,wellorder}) set" assumes "a \ 0" and P: "P \ {x. a \ x = 0}" and "0 \ m" "0 \ e" @@ -2486,13 +2489,13 @@ qed text\As above, but translating the sets (HOL Light's @text{GEN\_GEOM\_ORIGIN\_TAC})\ -lemma%important Sard_lemma1: +lemma Sard_lemma1: fixes P :: "(real^'n::{finite,wellorder}) set" assumes P: "dim P < CARD('n)" and "0 \ m" "0 \ e" obtains S where "S \ lmeasurable" and "{z. norm(z - w) \ m \ (\t \ P. norm(z - w - t) \ e)} \ S" and "measure lebesgue S \ (2 * e) * (2 * m) ^ (CARD('n) - 1)" -proof%unimportant - +proof - obtain a where "a \ 0" "P \ {x. a \ x = 0}" using lowdim_subset_hyperplane [of P] P span_base by auto then obtain S where S: "S \ lmeasurable" @@ -2510,7 +2513,7 @@ qed qed -lemma%important Sard_lemma2: +lemma Sard_lemma2: fixes f :: "real^'m::{finite,wellorder} \ real^'n::{finite,wellorder}" assumes mlen: "CARD('m) \ CARD('n)" (is "?m \ ?n") and "B > 0" "bounded S" @@ -2518,7 +2521,7 @@ and rank: "\x. x \ S \ rank(matrix(f' x)) < CARD('n)" and B: "\x. x \ S \ onorm(f' x) \ B" shows "negligible(f ` S)" -proof%unimportant - +proof - have lin_f': "\x. x \ S \ linear(f' x)" using derS has_derivative_linear by blast show ?thesis @@ -2725,13 +2728,13 @@ qed -theorem%important baby_Sard: +theorem baby_Sard: fixes f :: "real^'m::{finite,wellorder} \ real^'n::{finite,wellorder}" assumes mlen: "CARD('m) \ CARD('n)" and der: "\x. x \ S \ (f has_derivative f' x) (at x within S)" and rank: "\x. x \ S \ rank(matrix(f' x)) < CARD('n)" shows "negligible(f ` S)" -proof%unimportant - +proof - let ?U = "\n. {x \ S. norm(x) \ n \ onorm(f' x) \ real n}" have "\x. x \ S \ \n. norm x \ real n \ onorm (f' x) \ real n" by (meson linear order_trans real_arch_simple) @@ -2753,7 +2756,7 @@ subsection%important\A one-way version of change-of-variables not assuming injectivity. \ -lemma%important integral_on_image_ubound_weak: +lemma integral_on_image_ubound_weak: fixes f :: "real^'n::{finite,wellorder} \ real" assumes S: "S \ sets lebesgue" and f: "f \ borel_measurable (lebesgue_on (g ` S))" @@ -2764,7 +2767,7 @@ shows "f integrable_on (g ` S) \ integral (g ` S) f \ integral S (\x. \det (matrix (g' x))\ * f(g x))" (is "_ \ _ \ ?b") -proof%unimportant - +proof - let ?D = "\x. \det (matrix (g' x))\" have cont_g: "continuous_on S g" using der_g has_derivative_continuous_on by blast @@ -2942,14 +2945,14 @@ qed -lemma%important integral_on_image_ubound_nonneg: +lemma integral_on_image_ubound_nonneg: fixes f :: "real^'n::{finite,wellorder} \ real" assumes nonneg_fg: "\x. x \ S \ 0 \ f(g x)" and der_g: "\x. x \ S \ (g has_derivative g' x) (at x within S)" and intS: "(\x. \det (matrix (g' x))\ * f(g x)) integrable_on S" shows "f integrable_on (g ` S) \ integral (g ` S) f \ integral S (\x. \det (matrix (g' x))\ * f(g x))" (is "_ \ _ \ ?b") -proof%unimportant - +proof - let ?D = "\x. det (matrix (g' x))" define S' where "S' \ {x \ S. ?D x * f(g x) \ 0}" then have der_gS': "\x. x \ S' \ (g has_derivative g' x) (at x within S')" @@ -3072,7 +3075,7 @@ qed -lemma%unimportant absolutely_integrable_on_image_real: +proposition absolutely_integrable_on_image_real: fixes f :: "real^'n::{finite,wellorder} \ real" and g :: "real^'n::_ \ real^'n::_" assumes der_g: "\x. x \ S \ (g has_derivative g' x) (at x within S)" and intS: "(\x. \det (matrix (g' x))\ * f(g x)) absolutely_integrable_on S" @@ -3147,7 +3150,7 @@ qed -proposition%important absolutely_integrable_on_image: +proposition absolutely_integrable_on_image: fixes f :: "real^'m::{finite,wellorder} \ real^'n" and g :: "real^'m::_ \ real^'m::_" assumes der_g: "\x. x \ S \ (g has_derivative g' x) (at x within S)" and intS: "(\x. \det (matrix (g' x))\ *\<^sub>R f(g x)) absolutely_integrable_on S" @@ -3155,7 +3158,7 @@ apply (rule absolutely_integrable_componentwise [OF absolutely_integrable_on_image_real [OF der_g]]) using%unimportant absolutely_integrable_component [OF intS] by%unimportant auto -proposition%important integral_on_image_ubound: +proposition integral_on_image_ubound: fixes f :: "real^'n::{finite,wellorder} \ real" and g :: "real^'n::_ \ real^'n::_" assumes"\x. x \ S \ 0 \ f(g x)" and "\x. x \ S \ (g has_derivative g' x) (at x within S)" @@ -3169,7 +3172,7 @@ text\The classic change-of-variables theorem. We have two versions with quite general hypotheses, the first that the transforming function has a continuous inverse, the second that the base set is Lebesgue measurable.\ -lemma%unimportant cov_invertible_nonneg_le: +lemma cov_invertible_nonneg_le: fixes f :: "real^'n::{finite,wellorder} \ real" and g :: "real^'n::_ \ real^'n::_" assumes der_g: "\x. x \ S \ (g has_derivative g' x) (at x within S)" and der_h: "\y. y \ T \ (h has_derivative h' y) (at y within T)" @@ -3240,7 +3243,7 @@ qed -lemma%unimportant cov_invertible_nonneg_eq: +lemma cov_invertible_nonneg_eq: fixes f :: "real^'n::{finite,wellorder} \ real" and g :: "real^'n::_ \ real^'n::_" assumes "\x. x \ S \ (g has_derivative g' x) (at x within S)" and "\y. y \ T \ (h has_derivative h' y) (at y within T)" @@ -3253,7 +3256,7 @@ by (simp add: has_integral_iff) (meson eq_iff) -lemma%unimportant cov_invertible_real: +lemma cov_invertible_real: fixes f :: "real^'n::{finite,wellorder} \ real" and g :: "real^'n::_ \ real^'n::_" assumes der_g: "\x. x \ S \ (g has_derivative g' x) (at x within S)" and der_h: "\y. y \ T \ (h has_derivative h' y) (at y within T)" @@ -3419,7 +3422,7 @@ qed -lemma%unimportant cv_inv_version3: +lemma cv_inv_version3: fixes f :: "real^'m::{finite,wellorder} \ real^'n" and g :: "real^'m::_ \ real^'m::_" assumes der_g: "\x. x \ S \ (g has_derivative g' x) (at x within S)" and der_h: "\y. y \ T \ (h has_derivative h' y) (at y within T)" @@ -3445,7 +3448,7 @@ qed -lemma%unimportant cv_inv_version4: +lemma cv_inv_version4: fixes f :: "real^'m::{finite,wellorder} \ real^'n" and g :: "real^'m::_ \ real^'m::_" assumes der_g: "\x. x \ S \ (g has_derivative g' x) (at x within S) \ invertible(matrix(g' x))" and hg: "\x. x \ S \ continuous_on (g ` S) h \ h(g x) = x" @@ -3470,7 +3473,7 @@ qed -proposition%important has_absolute_integral_change_of_variables_invertible: +proposition has_absolute_integral_change_of_variables_invertible: fixes f :: "real^'m::{finite,wellorder} \ real^'n" and g :: "real^'m::_ \ real^'m::_" assumes der_g: "\x. x \ S \ (g has_derivative g' x) (at x within S)" and hg: "\x. x \ S \ h(g x) = x" @@ -3478,7 +3481,7 @@ shows "(\x. \det (matrix (g' x))\ *\<^sub>R f(g x)) absolutely_integrable_on S \ integral S (\x. \det (matrix (g' x))\ *\<^sub>R f(g x)) = b \ f absolutely_integrable_on (g ` S) \ integral (g ` S) f = b" (is "?lhs = ?rhs") -proof%unimportant - +proof - let ?S = "{x \ S. invertible (matrix (g' x))}" and ?D = "\x. \det (matrix (g' x))\ *\<^sub>R f(g x)" have *: "?D absolutely_integrable_on ?S \ integral ?S ?D = b \ f absolutely_integrable_on (g ` ?S) \ integral (g ` ?S) f = b" @@ -3514,7 +3517,7 @@ -lemma%unimportant has_absolute_integral_change_of_variables_compact: +proposition has_absolute_integral_change_of_variables_compact: fixes f :: "real^'m::{finite,wellorder} \ real^'n" and g :: "real^'m::_ \ real^'m::_" assumes "compact S" and der_g: "\x. x \ S \ (g has_derivative g' x) (at x within S)" @@ -3532,7 +3535,7 @@ qed -lemma%unimportant has_absolute_integral_change_of_variables_compact_family: +lemma has_absolute_integral_change_of_variables_compact_family: fixes f :: "real^'m::{finite,wellorder} \ real^'n" and g :: "real^'m::_ \ real^'m::_" assumes compact: "\n::nat. compact (F n)" and der_g: "\x. x \ (\n. F n) \ (g has_derivative g' x) (at x within (\n. F n))" @@ -3711,7 +3714,7 @@ qed -proposition%important has_absolute_integral_change_of_variables: +proposition has_absolute_integral_change_of_variables: fixes f :: "real^'m::{finite,wellorder} \ real^'n" and g :: "real^'m::_ \ real^'m::_" assumes S: "S \ sets lebesgue" and der_g: "\x. x \ S \ (g has_derivative g' x) (at x within S)" @@ -3719,7 +3722,7 @@ shows "(\x. \det (matrix (g' x))\ *\<^sub>R f(g x)) absolutely_integrable_on S \ integral S (\x. \det (matrix (g' x))\ *\<^sub>R f(g x)) = b \ f absolutely_integrable_on (g ` S) \ integral (g ` S) f = b" -proof%unimportant - +proof - obtain C N where "fsigma C" "negligible N" and CNS: "C \ N = S" and "disjnt C N" using lebesgue_set_almost_fsigma [OF S] . then obtain F :: "nat \ (real^'m::_) set" @@ -3773,16 +3776,16 @@ qed -corollary%important absolutely_integrable_change_of_variables: +corollary absolutely_integrable_change_of_variables: fixes f :: "real^'m::{finite,wellorder} \ real^'n" and g :: "real^'m::_ \ real^'m::_" assumes "S \ sets lebesgue" and "\x. x \ S \ (g has_derivative g' x) (at x within S)" and "inj_on g S" shows "f absolutely_integrable_on (g ` S) \ (\x. \det (matrix (g' x))\ *\<^sub>R f(g x)) absolutely_integrable_on S" - using%unimportant assms has_absolute_integral_change_of_variables by%unimportant blast + using assms has_absolute_integral_change_of_variables by blast -corollary%important integral_change_of_variables: +corollary integral_change_of_variables: fixes f :: "real^'m::{finite,wellorder} \ real^'n" and g :: "real^'m::_ \ real^'m::_" assumes S: "S \ sets lebesgue" and der_g: "\x. x \ S \ (g has_derivative g' x) (at x within S)" @@ -3790,10 +3793,10 @@ and disj: "(f absolutely_integrable_on (g ` S) \ (\x. \det (matrix (g' x))\ *\<^sub>R f(g x)) absolutely_integrable_on S)" shows "integral (g ` S) f = integral S (\x. \det (matrix (g' x))\ *\<^sub>R f(g x))" - using%unimportant has_absolute_integral_change_of_variables [OF S der_g inj] disj - by%unimportant blast + using has_absolute_integral_change_of_variables [OF S der_g inj] disj + by blast -lemma%unimportant has_absolute_integral_change_of_variables_1: +lemma has_absolute_integral_change_of_variables_1: fixes f :: "real \ real^'n::{finite,wellorder}" and g :: "real \ real" assumes S: "S \ sets lebesgue" and der_g: "\x. x \ S \ (g has_vector_derivative g' x) (at x within S)" @@ -3832,19 +3835,19 @@ qed -corollary%important absolutely_integrable_change_of_variables_1: +corollary absolutely_integrable_change_of_variables_1: fixes f :: "real \ real^'n::{finite,wellorder}" and g :: "real \ real" assumes S: "S \ sets lebesgue" and der_g: "\x. x \ S \ (g has_vector_derivative g' x) (at x within S)" and inj: "inj_on g S" shows "(f absolutely_integrable_on g ` S \ (\x. \g' x\ *\<^sub>R f(g x)) absolutely_integrable_on S)" - using%unimportant has_absolute_integral_change_of_variables_1 [OF assms] by%unimportant auto + using has_absolute_integral_change_of_variables_1 [OF assms] by auto subsection%important\Change of variables for integrals: special case of linear function\ -lemma%unimportant has_absolute_integral_change_of_variables_linear: +lemma has_absolute_integral_change_of_variables_linear: fixes f :: "real^'m::{finite,wellorder} \ real^'n" and g :: "real^'m::_ \ real^'m::_" assumes "linear g" shows "(\x. \det (matrix g)\ *\<^sub>R f(g x)) absolutely_integrable_on S \ @@ -3869,14 +3872,14 @@ qed (use h in auto) qed -lemma%unimportant absolutely_integrable_change_of_variables_linear: +lemma absolutely_integrable_change_of_variables_linear: fixes f :: "real^'m::{finite,wellorder} \ real^'n" and g :: "real^'m::_ \ real^'m::_" assumes "linear g" shows "(\x. \det (matrix g)\ *\<^sub>R f(g x)) absolutely_integrable_on S \ f absolutely_integrable_on (g ` S)" using assms has_absolute_integral_change_of_variables_linear by blast -lemma%unimportant absolutely_integrable_on_linear_image: +lemma absolutely_integrable_on_linear_image: fixes f :: "real^'m::{finite,wellorder} \ real^'n" and g :: "real^'m::_ \ real^'m::_" assumes "linear g" shows "f absolutely_integrable_on (g ` S) @@ -3884,12 +3887,12 @@ unfolding assms absolutely_integrable_change_of_variables_linear [OF assms, symmetric] absolutely_integrable_on_scaleR_iff by (auto simp: set_integrable_def) -lemma%important integral_change_of_variables_linear: +lemma integral_change_of_variables_linear: fixes f :: "real^'m::{finite,wellorder} \ real^'n" and g :: "real^'m::_ \ real^'m::_" assumes "linear g" and "f absolutely_integrable_on (g ` S) \ (f \ g) absolutely_integrable_on S" shows "integral (g ` S) f = \det (matrix g)\ *\<^sub>R integral S (f \ g)" -proof%unimportant - +proof - have "((\x. \det (matrix g)\ *\<^sub>R f (g x)) absolutely_integrable_on S) \ (f absolutely_integrable_on g ` S)" using absolutely_integrable_on_linear_image assms by blast moreover @@ -3903,18 +3906,18 @@ subsection%important\Change of variable for measure\ -lemma%unimportant has_measure_differentiable_image: +lemma has_measure_differentiable_image: fixes f :: "real^'n::{finite,wellorder} \ real^'n::_" assumes "S \ sets lebesgue" and "\x. x \ S \ (f has_derivative f' x) (at x within S)" and "inj_on f S" shows "f ` S \ lmeasurable \ measure lebesgue (f ` S) = m \ ((\x. \det (matrix (f' x))\) has_integral m) S" - using%unimportant has_absolute_integral_change_of_variables [OF assms, of "\x. (1::real^1)" "vec m"] - unfolding%unimportant absolutely_integrable_on_1_iff integral_on_1_eq integrable_on_1_iff absolutely_integrable_on_def - by%unimportant (auto simp: has_integral_iff lmeasurable_iff_integrable_on lmeasure_integral) + using has_absolute_integral_change_of_variables [OF assms, of "\x. (1::real^1)" "vec m"] + unfolding absolutely_integrable_on_1_iff integral_on_1_eq integrable_on_1_iff absolutely_integrable_on_def + by (auto simp: has_integral_iff lmeasurable_iff_integrable_on lmeasure_integral) -lemma%unimportant measurable_differentiable_image_eq: +lemma measurable_differentiable_image_eq: fixes f :: "real^'n::{finite,wellorder} \ real^'n::_" assumes "S \ sets lebesgue" and "\x. x \ S \ (f has_derivative f' x) (at x within S)" @@ -3923,23 +3926,23 @@ using has_measure_differentiable_image [OF assms] by blast -lemma%important measurable_differentiable_image_alt: +lemma measurable_differentiable_image_alt: fixes f :: "real^'n::{finite,wellorder} \ real^'n::_" assumes "S \ sets lebesgue" and "\x. x \ S \ (f has_derivative f' x) (at x within S)" and "inj_on f S" shows "f ` S \ lmeasurable \ (\x. \det (matrix (f' x))\) absolutely_integrable_on S" - using%unimportant measurable_differentiable_image_eq [OF assms] - by%unimportant (simp only: absolutely_integrable_on_iff_nonneg) + using measurable_differentiable_image_eq [OF assms] + by (simp only: absolutely_integrable_on_iff_nonneg) -lemma%important measure_differentiable_image_eq: +lemma measure_differentiable_image_eq: fixes f :: "real^'n::{finite,wellorder} \ real^'n::_" assumes S: "S \ sets lebesgue" and der_f: "\x. x \ S \ (f has_derivative f' x) (at x within S)" and inj: "inj_on f S" and intS: "(\x. \det (matrix (f' x))\) integrable_on S" shows "measure lebesgue (f ` S) = integral S (\x. \det (matrix (f' x))\)" - using%unimportant measurable_differentiable_image_eq [OF S der_f inj] + using measurable_differentiable_image_eq [OF S der_f inj] assms has_measure_differentiable_image by%unimportant blast end diff -r a03a63b81f44 -r a06b204527e6 src/HOL/Analysis/Cross3.thy --- a/src/HOL/Analysis/Cross3.thy Mon Jan 14 18:35:03 2019 +0000 +++ b/src/HOL/Analysis/Cross3.thy Wed Jan 16 21:27:33 2019 +0000 @@ -79,14 +79,14 @@ hide_fact (open) left_diff_distrib right_diff_distrib -lemma%important Jacobi: "x \ (y \ z) + y \ (z \ x) + z \ (x \ y) = 0" for x::"real^3" +proposition Jacobi: "x \ (y \ z) + y \ (z \ x) + z \ (x \ y) = 0" for x::"real^3" by%unimportant (simp add: cross3_simps) -lemma%important Lagrange: "x \ (y \ z) = (x \ z) *\<^sub>R y - (x \ y) *\<^sub>R z" +proposition Lagrange: "x \ (y \ z) = (x \ z) *\<^sub>R y - (x \ y) *\<^sub>R z" by%unimportant (simp add: cross3_simps) (metis (full_types) exhaust_3) -lemma cross_triple: "(x \ y) \ z = (y \ z) \ x" - by (simp add: cross3_def inner_vec_def sum_3 vec_eq_iff algebra_simps) +proposition cross_triple: "(x \ y) \ z = (y \ z) \ x" + by%unimportant (simp add: cross3_def inner_vec_def sum_3 vec_eq_iff algebra_simps) lemma cross_components: "(x \ y)$1 = x$2 * y$3 - y$2 * x$3" "(x \ y)$2 = x$3 * y$1 - y$3 * x$1" "(x \ y)$3 = x$1 * y$2 - y$1 * x$2" @@ -126,15 +126,15 @@ lemma cross_cross_det: "(w \ x) \ (y \ z) = det(vector[w,x,z]) *\<^sub>R y - det(vector[w,x,y]) *\<^sub>R z" using exhaust_3 by (force simp add: cross3_simps) -lemma%important dot_cross: "(w \ x) \ (y \ z) = (w \ y) * (x \ z) - (w \ z) * (x \ y)" +proposition dot_cross: "(w \ x) \ (y \ z) = (w \ y) * (x \ z) - (w \ z) * (x \ y)" by%unimportant (force simp add: cross3_simps) -lemma norm_cross: "(norm (x \ y))\<^sup>2 = (norm x)\<^sup>2 * (norm y)\<^sup>2 - (x \ y)\<^sup>2" +proposition norm_cross: "(norm (x \ y))\<^sup>2 = (norm x)\<^sup>2 * (norm y)\<^sup>2 - (x \ y)\<^sup>2" unfolding power2_norm_eq_inner power_mult_distrib by (simp add: cross3_simps power2_eq_square) -lemma%important cross_eq_0: "x \ y = 0 \ collinear{0,x,y}" -proof%unimportant - +lemma cross_eq_0: "x \ y = 0 \ collinear{0,x,y}" +proof - have "x \ y = 0 \ norm (x \ y) = 0" by simp also have "... \ (norm x * norm y)\<^sup>2 = (x \ y)\<^sup>2" @@ -175,10 +175,10 @@ apply (simp add: vector_matrix_mult_def matrix_vector_mult_def forall_3 cross3_simps) done -lemma%important cross_orthogonal_matrix: +lemma cross_orthogonal_matrix: assumes "orthogonal_matrix A" shows "(A *v x) \ (A *v y) = det A *\<^sub>R (A *v (x \ y))" -proof%unimportant - +proof - have "mat 1 = transpose (A ** transpose A)" by (metis (no_types) assms orthogonal_matrix_def transpose_mat) then show ?thesis @@ -191,10 +191,10 @@ lemma cross_rotoinversion_matrix: "rotoinversion_matrix A \ (A *v x) \ (A *v y) = - A *v (x \ y)" by (simp add: rotoinversion_matrix_def cross_orthogonal_matrix scaleR_matrix_vector_assoc) -lemma%important cross_orthogonal_transformation: +lemma cross_orthogonal_transformation: assumes "orthogonal_transformation f" shows "(f x) \ (f y) = det(matrix f) *\<^sub>R f(x \ y)" -proof%unimportant - +proof - have orth: "orthogonal_matrix (matrix f)" using assms orthogonal_transformation_matrix by blast have "matrix f *v z = f z" for z @@ -208,7 +208,7 @@ \ (f x) \ (f y) = f(x \ y)" by (simp add: cross_orthogonal_transformation orthogonal_transformation) -subsection%unimportant \Continuity\ +subsection%important \Continuity\ lemma continuous_cross: "\continuous F f; continuous F g\ \ continuous F (\x. (f x) \ (g x))" apply (subst continuous_componentwise) diff -r a03a63b81f44 -r a06b204527e6 src/HOL/Analysis/Determinants.thy --- a/src/HOL/Analysis/Determinants.thy Mon Jan 14 18:35:03 2019 +0000 +++ b/src/HOL/Analysis/Determinants.thy Wed Jan 16 21:27:33 2019 +0000 @@ -15,19 +15,19 @@ definition%important trace :: "'a::semiring_1^'n^'n \ 'a" where "trace A = sum (\i. ((A$i)$i)) (UNIV::'n set)" -lemma%unimportant trace_0: "trace (mat 0) = 0" +lemma trace_0: "trace (mat 0) = 0" by (simp add: trace_def mat_def) -lemma%unimportant trace_I: "trace (mat 1 :: 'a::semiring_1^'n^'n) = of_nat(CARD('n))" +lemma trace_I: "trace (mat 1 :: 'a::semiring_1^'n^'n) = of_nat(CARD('n))" by (simp add: trace_def mat_def) -lemma%unimportant trace_add: "trace ((A::'a::comm_semiring_1^'n^'n) + B) = trace A + trace B" +lemma trace_add: "trace ((A::'a::comm_semiring_1^'n^'n) + B) = trace A + trace B" by (simp add: trace_def sum.distrib) -lemma%unimportant trace_sub: "trace ((A::'a::comm_ring_1^'n^'n) - B) = trace A - trace B" +lemma trace_sub: "trace ((A::'a::comm_ring_1^'n^'n) - B) = trace A - trace B" by (simp add: trace_def sum_subtractf) -lemma%important trace_mul_sym: "trace ((A::'a::comm_semiring_1^'n^'m) ** B) = trace (B**A)" +lemma trace_mul_sym: "trace ((A::'a::comm_semiring_1^'n^'m) ** B) = trace (B**A)" apply (simp add: trace_def matrix_matrix_mult_def) apply (subst sum.swap) apply (simp add: mult.commute) @@ -42,8 +42,8 @@ text \Basic determinant properties\ -lemma%important det_transpose [simp]: "det (transpose A) = det (A::'a::comm_ring_1 ^'n^'n)" -proof%unimportant - +proposition det_transpose [simp]: "det (transpose A) = det (A::'a::comm_ring_1 ^'n^'n)" +proof - let ?di = "\A i j. A$i$j" let ?U = "(UNIV :: 'n set)" have fU: "finite ?U" by simp @@ -80,7 +80,7 @@ by (subst sum_permutations_inverse) (blast intro: sum.cong) qed -lemma%unimportant det_lowerdiagonal: +lemma det_lowerdiagonal: fixes A :: "'a::comm_ring_1^('n::{finite,wellorder})^('n::{finite,wellorder})" assumes ld: "\i j. i < j \ A$i$j = 0" shows "det A = prod (\i. A$i$i) (UNIV:: 'n set)" @@ -107,11 +107,11 @@ unfolding det_def by (simp add: sign_id) qed -lemma%important det_upperdiagonal: +lemma det_upperdiagonal: fixes A :: "'a::comm_ring_1^'n::{finite,wellorder}^'n::{finite,wellorder}" assumes ld: "\i j. i > j \ A$i$j = 0" shows "det A = prod (\i. A$i$i) (UNIV:: 'n set)" -proof%unimportant - +proof - let ?U = "UNIV:: 'n set" let ?PU = "{p. p permutes ?U}" let ?pp = "(\p. of_int (sign p) * prod (\i. A$i$p i) (UNIV :: 'n set))" @@ -134,11 +134,11 @@ unfolding det_def by (simp add: sign_id) qed -lemma%important det_diagonal: +proposition det_diagonal: fixes A :: "'a::comm_ring_1^'n^'n" assumes ld: "\i j. i \ j \ A$i$j = 0" shows "det A = prod (\i. A$i$i) (UNIV::'n set)" -proof%unimportant - +proof - let ?U = "UNIV:: 'n set" let ?PU = "{p. p permutes ?U}" let ?pp = "\p. of_int (sign p) * prod (\i. A$i$p i) (UNIV :: 'n set)" @@ -161,13 +161,13 @@ unfolding det_def by (simp add: sign_id) qed -lemma%unimportant det_I [simp]: "det (mat 1 :: 'a::comm_ring_1^'n^'n) = 1" +lemma det_I [simp]: "det (mat 1 :: 'a::comm_ring_1^'n^'n) = 1" by (simp add: det_diagonal mat_def) -lemma%unimportant det_0 [simp]: "det (mat 0 :: 'a::comm_ring_1^'n^'n) = 0" +lemma det_0 [simp]: "det (mat 0 :: 'a::comm_ring_1^'n^'n) = 0" by (simp add: det_def prod_zero power_0_left) -lemma%unimportant det_permute_rows: +lemma det_permute_rows: fixes A :: "'a::comm_ring_1^'n^'n" assumes p: "p permutes (UNIV :: 'n::finite set)" shows "det (\ i. A$p i :: 'a^'n^'n) = of_int (sign p) * det A" @@ -204,11 +204,11 @@ done qed -lemma%important det_permute_columns: +lemma det_permute_columns: fixes A :: "'a::comm_ring_1^'n^'n" assumes p: "p permutes (UNIV :: 'n set)" shows "det(\ i j. A$i$ p j :: 'a^'n^'n) = of_int (sign p) * det A" -proof%unimportant - +proof - let ?Ap = "\ i j. A$i$ p j :: 'a^'n^'n" let ?At = "transpose A" have "of_int (sign p) * det A = det (transpose (\ i. transpose A $ p i))" @@ -220,7 +220,7 @@ by simp qed -lemma%unimportant det_identical_columns: +lemma det_identical_columns: fixes A :: "'a::comm_ring_1^'n^'n" assumes jk: "j \ k" and r: "column j A = column k A" @@ -300,24 +300,24 @@ finally show "det A = 0" by simp qed -lemma%unimportant det_identical_rows: +lemma det_identical_rows: fixes A :: "'a::comm_ring_1^'n^'n" assumes ij: "i \ j" and r: "row i A = row j A" shows "det A = 0" by (metis column_transpose det_identical_columns det_transpose ij r) -lemma%unimportant det_zero_row: +lemma det_zero_row: fixes A :: "'a::{idom, ring_char_0}^'n^'n" and F :: "'b::{field}^'m^'m" shows "row i A = 0 \ det A = 0" and "row j F = 0 \ det F = 0" by (force simp: row_def det_def vec_eq_iff sign_nz intro!: sum.neutral)+ -lemma%unimportant det_zero_column: +lemma det_zero_column: fixes A :: "'a::{idom, ring_char_0}^'n^'n" and F :: "'b::{field}^'m^'m" shows "column i A = 0 \ det A = 0" and "column j F = 0 \ det F = 0" unfolding atomize_conj atomize_imp by (metis det_transpose det_zero_row row_transpose) -lemma%unimportant det_row_add: +lemma det_row_add: fixes a b c :: "'n::finite \ _ ^ 'n" shows "det((\ i. if i = k then a i + b i else c i)::'a::comm_ring_1^'n^'n) = det((\ i. if i = k then a i else c i)::'a::comm_ring_1^'n^'n) + @@ -358,7 +358,7 @@ by (simp add: field_simps) qed auto -lemma%unimportant det_row_mul: +lemma det_row_mul: fixes a b :: "'n::finite \ _ ^ 'n" shows "det((\ i. if i = k then c *s a i else b i)::'a::comm_ring_1^'n^'n) = c * det((\ i. if i = k then a i else b i)::'a::comm_ring_1^'n^'n)" @@ -395,7 +395,7 @@ by (simp add: field_simps) qed auto -lemma%unimportant det_row_0: +lemma det_row_0: fixes b :: "'n::finite \ _ ^ 'n" shows "det((\ i. if i = k then 0 else b i)::'a::comm_ring_1^'n^'n) = 0" using det_row_mul[of k 0 "\i. 1" b] @@ -403,11 +403,11 @@ apply (simp only: vector_smult_lzero) done -lemma%important det_row_operation: +lemma det_row_operation: fixes A :: "'a::{comm_ring_1}^'n^'n" assumes ij: "i \ j" shows "det (\ k. if k = i then row i A + c *s row j A else row k A) = det A" -proof%unimportant - +proof - let ?Z = "(\ k. if k = i then row j A else row k A) :: 'a ^'n^'n" have th: "row i ?Z = row j ?Z" by (vector row_def) have th2: "((\ k. if k = i then row i A else row k A) :: 'a^'n^'n) = A" @@ -417,7 +417,7 @@ by simp qed -lemma%unimportant det_row_span: +lemma det_row_span: fixes A :: "'a::{field}^'n^'n" assumes x: "x \ vec.span {row j A |j. j \ i}" shows "det (\ k. if k = i then row i A + x else row k A) = det A" @@ -449,10 +449,10 @@ unfolding scalar_mult_eq_scaleR . qed -lemma%unimportant matrix_id [simp]: "det (matrix id) = 1" +lemma matrix_id [simp]: "det (matrix id) = 1" by (simp add: matrix_id_mat_1) -lemma%important det_matrix_scaleR [simp]: "det (matrix (((*\<^sub>R) r)) :: real^'n^'n) = r ^ CARD('n::finite)" +lemma det_matrix_scaleR [simp]: "det (matrix (((*\<^sub>R) r)) :: real^'n^'n) = r ^ CARD('n::finite)" apply (subst det_diagonal) apply (auto simp: matrix_def mat_def) apply (simp add: cart_eq_inner_axis inner_axis_axis) @@ -463,7 +463,7 @@ exact duplicates by considering the rows/columns as a set. \ -lemma%unimportant det_dependent_rows: +lemma det_dependent_rows: fixes A:: "'a::{field}^'n^'n" assumes d: "vec.dependent (rows A)" shows "det A = 0" @@ -491,23 +491,23 @@ qed qed -lemma%unimportant det_dependent_columns: +lemma det_dependent_columns: assumes d: "vec.dependent (columns (A::real^'n^'n))" shows "det A = 0" by (metis d det_dependent_rows rows_transpose det_transpose) text \Multilinearity and the multiplication formula\ -lemma%unimportant Cart_lambda_cong: "(\x. f x = g x) \ (vec_lambda f::'a^'n) = (vec_lambda g :: 'a^'n)" +lemma Cart_lambda_cong: "(\x. f x = g x) \ (vec_lambda f::'a^'n) = (vec_lambda g :: 'a^'n)" by auto -lemma%unimportant det_linear_row_sum: +lemma det_linear_row_sum: assumes fS: "finite S" shows "det ((\ i. if i = k then sum (a i) S else c i)::'a::comm_ring_1^'n^'n) = sum (\j. det ((\ i. if i = k then a i j else c i)::'a^'n^'n)) S" using fS by (induct rule: finite_induct; simp add: det_row_0 det_row_add cong: if_cong) -lemma%unimportant finite_bounded_functions: +lemma finite_bounded_functions: assumes fS: "finite S" shows "finite {f. (\i \ {1.. (k::nat)}. f i \ S) \ (\i. i \ {1 .. k} \ f i = i)}" proof (induct k) @@ -532,14 +532,14 @@ qed -lemma%important det_linear_rows_sum_lemma: +lemma det_linear_rows_sum_lemma: assumes fS: "finite S" and fT: "finite T" shows "det ((\ i. if i \ T then sum (a i) S else c i):: 'a::comm_ring_1^'n^'n) = sum (\f. det((\ i. if i \ T then a i (f i) else c i)::'a^'n^'n)) {f. (\i \ T. f i \ S) \ (\i. i \ T \ f i = i)}" using fT -proof%unimportant (induct T arbitrary: a c set: finite) +proof (induct T arbitrary: a c set: finite) case empty have th0: "\x y. (\ i. if i \ {} then x i else y i) = (\ i. y i)" by vector @@ -577,7 +577,7 @@ (auto intro!: cong[OF refl[of det]] simp: vec_eq_iff) qed -lemma%unimportant det_linear_rows_sum: +lemma det_linear_rows_sum: fixes S :: "'n::finite set" assumes fS: "finite S" shows "det (\ i. sum (a i) S) = @@ -589,12 +589,12 @@ show ?thesis by simp qed -lemma%unimportant matrix_mul_sum_alt: +lemma matrix_mul_sum_alt: fixes A B :: "'a::comm_ring_1^'n^'n" shows "A ** B = (\ i. sum (\k. A$i$k *s B $ k) (UNIV :: 'n set))" by (vector matrix_matrix_mult_def sum_component) -lemma%unimportant det_rows_mul: +lemma det_rows_mul: "det((\ i. c i *s a i)::'a::comm_ring_1^'n^'n) = prod (\i. c i) (UNIV:: 'n set) * det((\ i. a i)::'a^'n^'n)" proof (simp add: det_def sum_distrib_left cong add: prod.cong, rule sum.cong) @@ -612,10 +612,10 @@ by (simp add: field_simps) qed rule -lemma%important det_mul: +proposition det_mul: fixes A B :: "'a::comm_ring_1^'n^'n" shows "det (A ** B) = det A * det B" -proof%unimportant - +proof - let ?U = "UNIV :: 'n set" let ?F = "{f. (\i \ ?U. f i \ ?U) \ (\i. i \ ?U \ f i = i)}" let ?PU = "{p. p permutes ?U}" @@ -714,10 +714,10 @@ subsection%important \Relation to invertibility\ -lemma%important invertible_det_nz: +proposition invertible_det_nz: fixes A::"'a::{field}^'n^'n" shows "invertible A \ det A \ 0" -proof%unimportant (cases "invertible A") +proof (cases "invertible A") case True then obtain B :: "'a^'n^'n" where B: "A ** B = mat 1" unfolding invertible_right_inverse by blast @@ -748,7 +748,7 @@ qed -lemma%unimportant det_nz_iff_inj_gen: +lemma det_nz_iff_inj_gen: fixes f :: "'a::field^'n \ 'a::field^'n" assumes "Vector_Spaces.linear (*s) (*s) f" shows "det (matrix f) \ 0 \ inj f" @@ -763,14 +763,14 @@ by (metis assms invertible_det_nz invertible_left_inverse matrix_compose_gen matrix_id_mat_1) qed -lemma%unimportant det_nz_iff_inj: +lemma det_nz_iff_inj: fixes f :: "real^'n \ real^'n" assumes "linear f" shows "det (matrix f) \ 0 \ inj f" using det_nz_iff_inj_gen[of f] assms unfolding linear_matrix_vector_mul_eq . -lemma%unimportant det_eq_0_rank: +lemma det_eq_0_rank: fixes A :: "real^'n^'n" shows "det A = 0 \ rank A < CARD('n)" using invertible_det_nz [of A] @@ -778,11 +778,11 @@ subsubsection%important \Invertibility of matrices and corresponding linear functions\ -lemma%important matrix_left_invertible_gen: +proposition matrix_left_invertible_gen: fixes f :: "'a::field^'m \ 'a::field^'n" assumes "Vector_Spaces.linear (*s) (*s) f" shows "((\B. B ** matrix f = mat 1) \ (\g. Vector_Spaces.linear (*s) (*s) g \ g \ f = id))" -proof%unimportant safe +proof safe fix B assume 1: "B ** matrix f = mat 1" show "\g. Vector_Spaces.linear (*s) (*s) g \ g \ f = id" @@ -801,12 +801,12 @@ then show "\B. B ** matrix f = mat 1" .. qed -lemma%unimportant matrix_left_invertible: +lemma matrix_left_invertible: "linear f \ ((\B. B ** matrix f = mat 1) \ (\g. linear g \ g \ f = id))" for f::"real^'m \ real^'n" using matrix_left_invertible_gen[of f] by (auto simp: linear_matrix_vector_mul_eq) -lemma%unimportant matrix_right_invertible_gen: +lemma matrix_right_invertible_gen: fixes f :: "'a::field^'m \ 'a^'n" assumes "Vector_Spaces.linear (*s) (*s) f" shows "((\B. matrix f ** B = mat 1) \ (\g. Vector_Spaces.linear (*s) (*s) g \ f \ g = id))" @@ -829,12 +829,12 @@ then show "\B. matrix f ** B = mat 1" .. qed -lemma%unimportant matrix_right_invertible: +lemma matrix_right_invertible: "linear f \ ((\B. matrix f ** B = mat 1) \ (\g. linear g \ f \ g = id))" for f::"real^'m \ real^'n" using matrix_right_invertible_gen[of f] by (auto simp: linear_matrix_vector_mul_eq) -lemma%unimportant matrix_invertible_gen: +lemma matrix_invertible_gen: fixes f :: "'a::field^'m \ 'a::field^'n" assumes "Vector_Spaces.linear (*s) (*s) f" shows "invertible (matrix f) \ (\g. Vector_Spaces.linear (*s) (*s) g \ f \ g = id \ g \ f = id)" @@ -847,13 +847,13 @@ by (metis assms invertible_def matrix_compose_gen matrix_id_mat_1) qed -lemma%unimportant matrix_invertible: +lemma matrix_invertible: "linear f \ invertible (matrix f) \ (\g. linear g \ f \ g = id \ g \ f = id)" for f::"real^'m \ real^'n" using matrix_invertible_gen[of f] by (auto simp: linear_matrix_vector_mul_eq) -lemma%unimportant invertible_eq_bij: +lemma invertible_eq_bij: fixes m :: "'a::field^'m^'n" shows "invertible m \ bij ((*v) m)" using matrix_invertible_gen[OF matrix_vector_mul_linear_gen, of m, simplified matrix_of_matrix_vector_mul] @@ -863,13 +863,13 @@ subsection%important \Cramer's rule\ -lemma%important cramer_lemma_transpose: +proposition cramer_lemma_transpose: fixes A:: "'a::{field}^'n^'n" and x :: "'a::{field}^'n" shows "det ((\ i. if i = k then sum (\i. x$i *s row i A) (UNIV::'n set) else row i A)::'a::{field}^'n^'n) = x$k * det A" (is "?lhs = ?rhs") -proof%unimportant - +proof - let ?U = "UNIV :: 'n set" let ?Uk = "?U - {k}" have U: "?U = insert k ?Uk" @@ -899,10 +899,10 @@ done qed -lemma%important cramer_lemma: +proposition cramer_lemma: fixes A :: "'a::{field}^'n^'n" shows "det((\ i j. if j = k then (A *v x)$i else A$i$j):: 'a::{field}^'n^'n) = x$k * det A" -proof%unimportant - +proof - let ?U = "UNIV :: 'n set" have *: "\c. sum (\i. c i *s row i (transpose A)) ?U = sum (\i. c i *s column i A) ?U" by (auto intro: sum.cong) @@ -916,11 +916,11 @@ done qed -lemma%important cramer: +theorem cramer: fixes A ::"'a::{field}^'n^'n" assumes d0: "det A \ 0" shows "A *v x = b \ x = (\ k. det(\ i j. if j=k then b$i else A$i$j) / det A)" -proof%unimportant - +proof - from d0 obtain B where B: "A ** B = mat 1" "B ** A = mat 1" unfolding invertible_det_nz[symmetric] invertible_def by blast @@ -948,7 +948,7 @@ definition%important "orthogonal_matrix (Q::'a::semiring_1^'n^'n) \ transpose Q ** Q = mat 1 \ Q ** transpose Q = mat 1" -lemma%unimportant orthogonal_transformation: +lemma orthogonal_transformation: "orthogonal_transformation f \ linear f \ (\v. norm (f v) = norm v)" unfolding orthogonal_transformation_def apply auto @@ -957,70 +957,70 @@ apply (simp add: dot_norm linear_add[symmetric]) done -lemma%unimportant orthogonal_transformation_id [simp]: "orthogonal_transformation (\x. x)" +lemma orthogonal_transformation_id [simp]: "orthogonal_transformation (\x. x)" by (simp add: linear_iff orthogonal_transformation_def) -lemma%unimportant orthogonal_orthogonal_transformation: +lemma orthogonal_orthogonal_transformation: "orthogonal_transformation f \ orthogonal (f x) (f y) \ orthogonal x y" by (simp add: orthogonal_def orthogonal_transformation_def) -lemma%unimportant orthogonal_transformation_compose: +lemma orthogonal_transformation_compose: "\orthogonal_transformation f; orthogonal_transformation g\ \ orthogonal_transformation(f \ g)" by (auto simp: orthogonal_transformation_def linear_compose) -lemma%unimportant orthogonal_transformation_neg: +lemma orthogonal_transformation_neg: "orthogonal_transformation(\x. -(f x)) \ orthogonal_transformation f" by (auto simp: orthogonal_transformation_def dest: linear_compose_neg) -lemma%unimportant orthogonal_transformation_scaleR: "orthogonal_transformation f \ f (c *\<^sub>R v) = c *\<^sub>R f v" +lemma orthogonal_transformation_scaleR: "orthogonal_transformation f \ f (c *\<^sub>R v) = c *\<^sub>R f v" by (simp add: linear_iff orthogonal_transformation_def) -lemma%unimportant orthogonal_transformation_linear: +lemma orthogonal_transformation_linear: "orthogonal_transformation f \ linear f" by (simp add: orthogonal_transformation_def) -lemma%unimportant orthogonal_transformation_inj: +lemma orthogonal_transformation_inj: "orthogonal_transformation f \ inj f" unfolding orthogonal_transformation_def inj_on_def by (metis vector_eq) -lemma%unimportant orthogonal_transformation_surj: +lemma orthogonal_transformation_surj: "orthogonal_transformation f \ surj f" for f :: "'a::euclidean_space \ 'a::euclidean_space" by (simp add: linear_injective_imp_surjective orthogonal_transformation_inj orthogonal_transformation_linear) -lemma%unimportant orthogonal_transformation_bij: +lemma orthogonal_transformation_bij: "orthogonal_transformation f \ bij f" for f :: "'a::euclidean_space \ 'a::euclidean_space" by (simp add: bij_def orthogonal_transformation_inj orthogonal_transformation_surj) -lemma%unimportant orthogonal_transformation_inv: +lemma orthogonal_transformation_inv: "orthogonal_transformation f \ orthogonal_transformation (inv f)" for f :: "'a::euclidean_space \ 'a::euclidean_space" by (metis (no_types, hide_lams) bijection.inv_right bijection_def inj_linear_imp_inv_linear orthogonal_transformation orthogonal_transformation_bij orthogonal_transformation_inj) -lemma%unimportant orthogonal_transformation_norm: +lemma orthogonal_transformation_norm: "orthogonal_transformation f \ norm (f x) = norm x" by (metis orthogonal_transformation) -lemma%unimportant orthogonal_matrix: "orthogonal_matrix (Q:: real ^'n^'n) \ transpose Q ** Q = mat 1" +lemma orthogonal_matrix: "orthogonal_matrix (Q:: real ^'n^'n) \ transpose Q ** Q = mat 1" by (metis matrix_left_right_inverse orthogonal_matrix_def) -lemma%unimportant orthogonal_matrix_id: "orthogonal_matrix (mat 1 :: _^'n^'n)" +lemma orthogonal_matrix_id: "orthogonal_matrix (mat 1 :: _^'n^'n)" by (simp add: orthogonal_matrix_def) -lemma%unimportant orthogonal_matrix_mul: +lemma orthogonal_matrix_mul: fixes A :: "real ^'n^'n" assumes "orthogonal_matrix A" "orthogonal_matrix B" shows "orthogonal_matrix(A ** B)" using assms by (simp add: orthogonal_matrix matrix_transpose_mul matrix_left_right_inverse matrix_mul_assoc) -lemma%important orthogonal_transformation_matrix: +proposition orthogonal_transformation_matrix: fixes f:: "real^'n \ real^'n" shows "orthogonal_transformation f \ linear f \ orthogonal_matrix(matrix f)" (is "?lhs \ ?rhs") -proof%unimportant - +proof - let ?mf = "matrix f" let ?ot = "orthogonal_transformation f" let ?U = "UNIV :: 'n set" @@ -1063,11 +1063,11 @@ by (auto simp: linear_def scalar_mult_eq_scaleR) qed -lemma%important det_orthogonal_matrix: +theorem det_orthogonal_matrix: fixes Q:: "'a::linordered_idom^'n^'n" assumes oQ: "orthogonal_matrix Q" shows "det Q = 1 \ det Q = - 1" -proof%unimportant - +proof - have "Q ** transpose Q = mat 1" by (metis oQ orthogonal_matrix_def) then have "det (Q ** transpose Q) = det (mat 1:: 'a^'n^'n)" @@ -1078,20 +1078,20 @@ by (simp add: square_eq_1_iff) qed -lemma%important orthogonal_transformation_det [simp]: +lemma orthogonal_transformation_det [simp]: fixes f :: "real^'n \ real^'n" shows "orthogonal_transformation f \ \det (matrix f)\ = 1" - using%unimportant det_orthogonal_matrix orthogonal_transformation_matrix by fastforce + using det_orthogonal_matrix orthogonal_transformation_matrix by fastforce subsection%important \Linearity of scaling, and hence isometry, that preserves origin\ -lemma%important scaling_linear: +lemma scaling_linear: fixes f :: "'a::real_inner \ 'a::real_inner" assumes f0: "f 0 = 0" and fd: "\x y. dist (f x) (f y) = c * dist x y" shows "linear f" -proof%unimportant - +proof - { fix v w have "norm (f x) = c * norm x" for x @@ -1105,13 +1105,13 @@ by (simp add: inner_add field_simps) qed -lemma%unimportant isometry_linear: +lemma isometry_linear: "f (0::'a::real_inner) = (0::'a) \ \x y. dist(f x) (f y) = dist x y \ linear f" by (rule scaling_linear[where c=1]) simp_all text \Hence another formulation of orthogonal transformation\ -lemma%important orthogonal_transformation_isometry: +lemma 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) @@ -1119,7 +1119,7 @@ by (metis dist_0_norm) -lemma%unimportant image_orthogonal_transformation_ball: +lemma image_orthogonal_transformation_ball: fixes f :: "'a::euclidean_space \ 'a" assumes "orthogonal_transformation f" shows "f ` ball x r = ball (f x) r" @@ -1135,7 +1135,7 @@ by (auto simp: orthogonal_transformation_isometry) qed -lemma%unimportant image_orthogonal_transformation_cball: +lemma image_orthogonal_transformation_cball: fixes f :: "'a::euclidean_space \ 'a" assumes "orthogonal_transformation f" shows "f ` cball x r = cball (f x) r" @@ -1153,29 +1153,29 @@ subsection%important \ We can find an orthogonal matrix taking any unit vector to any other\ -lemma%unimportant orthogonal_matrix_transpose [simp]: +lemma orthogonal_matrix_transpose [simp]: "orthogonal_matrix(transpose A) \ orthogonal_matrix A" by (auto simp: orthogonal_matrix_def) -lemma%unimportant orthogonal_matrix_orthonormal_columns: +lemma orthogonal_matrix_orthonormal_columns: fixes A :: "real^'n^'n" shows "orthogonal_matrix A \ (\i. norm(column i A) = 1) \ (\i j. i \ j \ orthogonal (column i A) (column j A))" by (auto simp: orthogonal_matrix matrix_mult_transpose_dot_column vec_eq_iff mat_def norm_eq_1 orthogonal_def) -lemma%unimportant orthogonal_matrix_orthonormal_rows: +lemma orthogonal_matrix_orthonormal_rows: fixes A :: "real^'n^'n" shows "orthogonal_matrix A \ (\i. norm(row i A) = 1) \ (\i j. i \ j \ orthogonal (row i A) (row j A))" using orthogonal_matrix_orthonormal_columns [of "transpose A"] by simp -lemma%important orthogonal_matrix_exists_basis: +theorem orthogonal_matrix_exists_basis: fixes a :: "real^'n" assumes "norm a = 1" obtains A where "orthogonal_matrix A" "A *v (axis k 1) = a" -proof%unimportant - +proof - obtain S where "a \ S" "pairwise orthogonal S" and noS: "\x. x \ S \ norm x = 1" and "independent S" "card S = CARD('n)" "span S = UNIV" using vector_in_orthonormal_basis assms by force @@ -1198,11 +1198,11 @@ qed qed -lemma%unimportant orthogonal_transformation_exists_1: +lemma orthogonal_transformation_exists_1: fixes a b :: "real^'n" assumes "norm a = 1" "norm b = 1" obtains f where "orthogonal_transformation f" "f a = b" -proof%unimportant - +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" @@ -1220,11 +1220,11 @@ qed qed -lemma%important orthogonal_transformation_exists: +theorem orthogonal_transformation_exists: fixes a b :: "real^'n" assumes "norm a = norm b" obtains f where "orthogonal_transformation f" "f a = b" -proof%unimportant (cases "a = 0 \ b = 0") +proof (cases "a = 0 \ b = 0") case True with assms show ?thesis using that by force @@ -1248,12 +1248,12 @@ subsection%important \Can extend an isometry from unit sphere\ -lemma%important isometry_sphere_extend: +lemma isometry_sphere_extend: fixes f:: "'a::real_inner \ 'a" assumes f1: "\x. norm x = 1 \ norm (f x) = 1" and fd1: "\x y. \norm x = 1; norm y = 1\ \ dist (f x) (f y) = dist x y" shows "\g. orthogonal_transformation g \ (\x. norm x = 1 \ g x = f x)" -proof%unimportant - +proof - { fix x y x' y' u v u' v' :: "'a" assume H: "x = norm x *\<^sub>R u" "y = norm y *\<^sub>R v" @@ -1291,26 +1291,26 @@ definition%important "rotation_matrix Q \ orthogonal_matrix Q \ det Q = 1" definition%important "rotoinversion_matrix Q \ orthogonal_matrix Q \ det Q = - 1" -lemma%important orthogonal_rotation_or_rotoinversion: +lemma orthogonal_rotation_or_rotoinversion: fixes Q :: "'a::linordered_idom^'n^'n" shows " orthogonal_matrix Q \ rotation_matrix Q \ rotoinversion_matrix Q" - by%unimportant (metis rotoinversion_matrix_def rotation_matrix_def det_orthogonal_matrix) + by (metis rotoinversion_matrix_def rotation_matrix_def det_orthogonal_matrix) text \Explicit formulas for low dimensions\ -lemma%unimportant prod_neutral_const: "prod f {(1::nat)..1} = f 1" +lemma prod_neutral_const: "prod f {(1::nat)..1} = f 1" by simp -lemma%unimportant prod_2: "prod f {(1::nat)..2} = f 1 * f 2" +lemma prod_2: "prod f {(1::nat)..2} = f 1 * f 2" by (simp add: eval_nat_numeral atLeastAtMostSuc_conv mult.commute) -lemma%unimportant prod_3: "prod f {(1::nat)..3} = f 1 * f 2 * f 3" +lemma prod_3: "prod f {(1::nat)..3} = f 1 * f 2 * f 3" by (simp add: eval_nat_numeral atLeastAtMostSuc_conv mult.commute) -lemma%unimportant det_1: "det (A::'a::comm_ring_1^1^1) = A$1$1" +lemma det_1: "det (A::'a::comm_ring_1^1^1) = A$1$1" by (simp add: det_def sign_id) -lemma%unimportant det_2: "det (A::'a::comm_ring_1^2^2) = A$1$1 * A$2$2 - A$1$2 * A$2$1" +lemma det_2: "det (A::'a::comm_ring_1^2^2) = A$1$1 * A$2$2 - A$1$2 * A$2$1" proof - have f12: "finite {2::2}" "1 \ {2::2}" by auto show ?thesis @@ -1320,7 +1320,7 @@ by (simp add: sign_swap_id sign_id swap_id_eq) qed -lemma%unimportant det_3: +lemma det_3: "det (A::'a::comm_ring_1^3^3) = A$1$1 * A$2$2 * A$3$3 + A$1$2 * A$2$3 * A$3$1 + @@ -1344,7 +1344,7 @@ text\ Slightly stronger results giving rotation, but only in two or more dimensions\ -lemma%unimportant rotation_matrix_exists_basis: +lemma rotation_matrix_exists_basis: fixes a :: "real^'n" assumes 2: "2 \ CARD('n)" and "norm a = 1" obtains A where "rotation_matrix A" "A *v (axis k 1) = a" @@ -1383,7 +1383,7 @@ qed qed -lemma%unimportant rotation_exists_1: +lemma rotation_exists_1: fixes a :: "real^'n" assumes "2 \ CARD('n)" "norm a = 1" "norm b = 1" obtains f where "orthogonal_transformation f" "det(matrix f) = 1" "f a = b" @@ -1406,7 +1406,7 @@ qed qed -lemma%unimportant rotation_exists: +lemma rotation_exists: fixes a :: "real^'n" assumes 2: "2 \ CARD('n)" and eq: "norm a = norm b" obtains f where "orthogonal_transformation f" "det(matrix f) = 1" "f a = b" @@ -1428,7 +1428,7 @@ with f show thesis .. qed -lemma%unimportant rotation_rightward_line: +lemma rotation_rightward_line: fixes a :: "real^'n" obtains f where "orthogonal_transformation f" "2 \ CARD('n) \ det(matrix f) = 1" "f(norm a *\<^sub>R axis k 1) = a" diff -r a03a63b81f44 -r a06b204527e6 src/HOL/Analysis/Extended_Real_Limits.thy --- a/src/HOL/Analysis/Extended_Real_Limits.thy Mon Jan 14 18:35:03 2019 +0000 +++ b/src/HOL/Analysis/Extended_Real_Limits.thy Wed Jan 16 21:27:33 2019 +0000 @@ -16,23 +16,23 @@ "HOL-Library.Indicator_Function" begin -lemma%important compact_UNIV: +lemma compact_UNIV: "compact (UNIV :: 'a::{complete_linorder,linorder_topology,second_countable_topology} set)" - using%unimportant compact_complete_linorder + using compact_complete_linorder by (auto simp: seq_compact_eq_compact[symmetric] seq_compact_def) -lemma%important compact_eq_closed: +lemma compact_eq_closed: fixes S :: "'a::{complete_linorder,linorder_topology,second_countable_topology} set" shows "compact S \ closed S" using%unimportant closed_Int_compact[of S, OF _ compact_UNIV] compact_imp_closed by auto -lemma%important closed_contains_Sup_cl: +lemma closed_contains_Sup_cl: fixes S :: "'a::{complete_linorder,linorder_topology,second_countable_topology} set" assumes "closed S" and "S \ {}" shows "Sup S \ S" -proof%unimportant - +proof - from compact_eq_closed[of S] compact_attains_sup[of S] assms obtain s where S: "s \ S" "\t\S. t \ s" by auto @@ -42,12 +42,12 @@ by simp qed -lemma%important closed_contains_Inf_cl: +lemma closed_contains_Inf_cl: fixes S :: "'a::{complete_linorder,linorder_topology,second_countable_topology} set" assumes "closed S" and "S \ {}" shows "Inf S \ S" -proof%unimportant - +proof - from compact_eq_closed[of S] compact_attains_inf[of S] assms obtain s where S: "s \ S" "\t\S. s \ t" by auto @@ -57,7 +57,7 @@ by simp qed -instance enat :: second_countable_topology +instance%unimportant enat :: second_countable_topology proof show "\B::enat set set. countable B \ open = generate_topology B" proof (intro exI conjI) @@ -66,8 +66,8 @@ qed (simp add: open_enat_def) qed -instance%important ereal :: second_countable_topology -proof%unimportant (standard, intro exI conjI) +instance%unimportant ereal :: second_countable_topology +proof (standard, intro exI conjI) let ?B = "(\r\\. {{..< r}, {r <..}} :: ereal set set)" show "countable ?B" by (auto intro: countable_rat) @@ -98,8 +98,8 @@ text \This is a copy from \ereal :: second_countable_topology\. Maybe find a common super class of topological spaces where the rational numbers are densely embedded ?\ -instance%important ennreal :: second_countable_topology -proof%unimportant (standard, intro exI conjI) +instance ennreal :: second_countable_topology +proof (standard, intro exI conjI) let ?B = "(\r\\. {{..< r}, {r <..}} :: ennreal set set)" show "countable ?B" by (auto intro: countable_rat) @@ -128,13 +128,13 @@ qed qed -lemma%important ereal_open_closed_aux: +lemma ereal_open_closed_aux: fixes S :: "ereal set" assumes "open S" and "closed S" and S: "(-\) \ S" shows "S = {}" -proof%unimportant (rule ccontr) +proof (rule ccontr) assume "\ ?thesis" then have *: "Inf S \ S" @@ -172,10 +172,10 @@ by auto qed -lemma%important ereal_open_closed: +lemma ereal_open_closed: fixes S :: "ereal set" shows "open S \ closed S \ S = {} \ S = UNIV" -proof%unimportant - +proof - { assume lhs: "open S \ closed S" { @@ -196,10 +196,10 @@ by auto qed -lemma%important ereal_open_atLeast: +lemma ereal_open_atLeast: fixes x :: ereal shows "open {x..} \ x = -\" -proof%unimportant +proof assume "x = -\" then have "{x..} = UNIV" by auto @@ -215,12 +215,12 @@ by (simp add: bot_ereal_def atLeast_eq_UNIV_iff) qed -lemma%important mono_closed_real: +lemma mono_closed_real: fixes S :: "real set" assumes mono: "\y z. y \ S \ y \ z \ z \ S" and "closed S" shows "S = {} \ S = UNIV \ (\a. S = {a..})" -proof%unimportant - +proof - { assume "S \ {}" { assume ex: "\B. \x\S. B \ x" @@ -261,12 +261,12 @@ by blast qed -lemma%important mono_closed_ereal: +lemma mono_closed_ereal: fixes S :: "real set" assumes mono: "\y z. y \ S \ y \ z \ z \ S" and "closed S" shows "\a. S = {x. a \ ereal x}" -proof%unimportant - +proof - { assume "S = {}" then have ?thesis @@ -296,11 +296,11 @@ using mono_closed_real[of S] assms by auto qed -lemma%important Liminf_within: +lemma Liminf_within: fixes f :: "'a::metric_space \ 'b::complete_lattice" shows "Liminf (at x within S) f = (SUP e\{0<..}. INF y\(S \ ball x e - {x}). f y)" unfolding Liminf_def eventually_at -proof%unimportant (rule SUP_eq, simp_all add: Ball_def Bex_def, safe) +proof (rule SUP_eq, simp_all add: Ball_def Bex_def, safe) fix P d assume "0 < d" and "\y. y \ S \ y \ x \ dist y x < d \ P y" then have "S \ ball x d - {x} \ {x. P x}" @@ -316,11 +316,11 @@ (auto intro!: INF_mono exI[of _ d] simp: dist_commute) qed -lemma%important Limsup_within: +lemma Limsup_within: fixes f :: "'a::metric_space \ 'b::complete_lattice" shows "Limsup (at x within S) f = (INF e\{0<..}. SUP y\(S \ ball x e - {x}). f y)" unfolding Limsup_def eventually_at -proof%unimportant (rule INF_eq, simp_all add: Ball_def Bex_def, safe) +proof (rule INF_eq, simp_all add: Ball_def Bex_def, safe) fix P d assume "0 < d" and "\y. y \ S \ y \ x \ dist y x < d \ P y" then have "S \ ball x d - {x} \ {x. P x}" @@ -357,7 +357,7 @@ done -subsection%important \Extended-Real.thy\ (*FIX title *) +subsection%important \Extended-Real.thy\ (*FIX ME change title *) lemma sum_constant_ereal: fixes a::ereal @@ -377,10 +377,10 @@ ultimately show ?thesis by (metis (mono_tags, lifting) eventually_mono) qed -lemma%important ereal_Inf_cmult: +lemma ereal_Inf_cmult: assumes "c>(0::real)" shows "Inf {ereal c * x |x. P x} = ereal c * Inf {x. P x}" -proof%unimportant - +proof - have "(\x::ereal. c * x) (Inf {x::ereal. P x}) = Inf ((\x::ereal. c * x)`{x::ereal. P x})" apply (rule mono_bij_Inf) apply (simp add: assms ereal_mult_left_mono less_imp_le mono_def) @@ -399,12 +399,12 @@ It is much more convenient in many situations, see for instance the proof of \tendsto_sum_ereal\ below.\ -lemma%important tendsto_add_ereal_PInf: +lemma tendsto_add_ereal_PInf: fixes y :: ereal assumes y: "y \ -\" assumes f: "(f \ \) F" and g: "(g \ y) F" shows "((\x. f x + g x) \ \) F" -proof%unimportant - +proof - have "\C. eventually (\x. g x > ereal C) F" proof (cases y) case (real r) @@ -437,12 +437,12 @@ that \- (x + y)\ is in general different from \(- x) + (- y)\ in ereal creates difficulties, so it is more efficient to copy the previous proof.\ -lemma%important tendsto_add_ereal_MInf: +lemma tendsto_add_ereal_MInf: fixes y :: ereal assumes y: "y \ \" assumes f: "(f \ -\) F" and g: "(g \ y) F" shows "((\x. f x + g x) \ -\) F" -proof%unimportant - +proof - have "\C. eventually (\x. g x < ereal C) F" proof (cases y) case (real r) @@ -470,12 +470,12 @@ then show ?thesis by (simp add: tendsto_MInfty) qed -lemma%important tendsto_add_ereal_general1: +lemma tendsto_add_ereal_general1: fixes x y :: ereal assumes y: "\y\ \ \" assumes f: "(f \ x) F" and g: "(g \ y) F" shows "((\x. f x + g x) \ x + y) F" -proof%unimportant (cases x) +proof (cases x) case (real r) have a: "\x\ \ \" by (simp add: real) show ?thesis by (rule tendsto_add_ereal[OF a, OF y, OF f, OF g]) @@ -488,12 +488,12 @@ by (metis abs_ereal.simps(3) ereal_MInfty_eq_plus) qed -lemma%important tendsto_add_ereal_general2: +lemma tendsto_add_ereal_general2: fixes x y :: ereal assumes x: "\x\ \ \" and f: "(f \ x) F" and g: "(g \ y) F" shows "((\x. f x + g x) \ x + y) F" -proof%unimportant - +proof - have "((\x. g x + f x) \ x + y) F" using tendsto_add_ereal_general1[OF x, OF g, OF f] add.commute[of "y", of "x"] by simp moreover have "\x. g x + f x = f x + g x" using add.commute by auto @@ -503,12 +503,12 @@ text \The next lemma says that the addition is continuous on \ereal\, except at the pairs \(-\, \)\ and \(\, -\)\.\ -lemma%important tendsto_add_ereal_general [tendsto_intros]: +lemma tendsto_add_ereal_general [tendsto_intros]: fixes x y :: ereal assumes "\((x=\ \ y=-\) \ (x=-\ \ y=\))" and f: "(f \ x) F" and g: "(g \ y) F" shows "((\x. f x + g x) \ x + y) F" -proof%unimportant (cases x) +proof (cases x) case (real r) show ?thesis apply (rule tendsto_add_ereal_general2) using real assms by auto @@ -528,10 +528,10 @@ ereal times ereal, except at \(\, 0)\ and \(-\, 0)\ and \(0, \)\ and \(0, -\)\, starting with specific situations.\ -lemma%important tendsto_mult_real_ereal: +lemma tendsto_mult_real_ereal: assumes "(u \ ereal l) F" "(v \ ereal m) F" shows "((\n. u n * v n) \ ereal l * ereal m) F" -proof%unimportant - +proof - have ureal: "eventually (\n. u n = ereal(real_of_ereal(u n))) F" by (rule real_lim_then_eventually_real[OF assms(1)]) then have "((\n. ereal(real_of_ereal(u n))) \ ereal l) F" using assms by auto then have limu: "((\n. real_of_ereal(u n)) \ l) F" by auto @@ -551,11 +551,11 @@ then show ?thesis using * filterlim_cong by fastforce qed -lemma%important tendsto_mult_ereal_PInf: +lemma tendsto_mult_ereal_PInf: fixes f g::"_ \ ereal" assumes "(f \ l) F" "l>0" "(g \ \) F" shows "((\x. f x * g x) \ \) F" -proof%unimportant - +proof - obtain a::real where "0 < ereal a" "a < l" using assms(2) using ereal_dense2 by blast have *: "eventually (\x. f x > a) F" using \a < l\ assms(1) by (simp add: order_tendsto_iff) { @@ -579,11 +579,11 @@ then show ?thesis by (auto simp add: tendsto_PInfty) qed -lemma%important tendsto_mult_ereal_pos: +lemma tendsto_mult_ereal_pos: fixes f g::"_ \ ereal" assumes "(f \ l) F" "(g \ m) F" "l>0" "m>0" shows "((\x. f x * g x) \ l * m) F" -proof%unimportant (cases) +proof (cases) assume *: "l = \ \ m = \" then show ?thesis proof (cases) @@ -618,11 +618,11 @@ shows "sgn(l) * sgn(l) = 1" apply (cases l) using assms by (auto simp add: one_ereal_def sgn_if) -lemma%important tendsto_mult_ereal [tendsto_intros]: +lemma tendsto_mult_ereal [tendsto_intros]: fixes f g::"_ \ ereal" assumes "(f \ l) F" "(g \ m) F" "\((l=0 \ abs(m) = \) \ (m=0 \ abs(l) = \))" shows "((\x. f x * g x) \ l * m) F" -proof%unimportant (cases) +proof (cases) assume "l=0 \ m=0" then have "abs(l) \ \" "abs(m) \ \" using assms(3) by auto then obtain lr mr where "l = ereal lr" "m = ereal mr" by auto @@ -661,11 +661,11 @@ subsubsection%important \Continuity of division\ -lemma%important tendsto_inverse_ereal_PInf: +lemma tendsto_inverse_ereal_PInf: fixes u::"_ \ ereal" assumes "(u \ \) F" shows "((\x. 1/ u x) \ 0) F" -proof%unimportant - +proof - { fix e::real assume "e>0" have "1/e < \" by auto @@ -702,11 +702,11 @@ shows "(u \ l) F \ l \ 0 \ ((\x. 1/ u x) \ 1/l) F" using tendsto_inverse unfolding inverse_eq_divide . -lemma%important tendsto_inverse_ereal [tendsto_intros]: +lemma tendsto_inverse_ereal [tendsto_intros]: fixes u::"_ \ ereal" assumes "(u \ l) F" "l \ 0" shows "((\x. 1/ u x) \ 1/l) F" -proof%unimportant (cases l) +proof (cases l) case (real r) then have "r \ 0" using assms(2) by auto then have "1/l = ereal(1/r)" using real by (simp add: one_ereal_def) @@ -747,11 +747,11 @@ then show ?thesis unfolding v_def using Lim_transform_eventually[OF *] \ 1/l = 0 \ by auto qed -lemma%important tendsto_divide_ereal [tendsto_intros]: +lemma tendsto_divide_ereal [tendsto_intros]: fixes f g::"_ \ ereal" assumes "(f \ l) F" "(g \ m) F" "m \ 0" "\(abs(l) = \ \ abs(m) = \)" shows "((\x. f x / g x) \ l / m) F" -proof%unimportant - +proof - define h where "h = (\x. 1/ g x)" have *: "(h \ 1/m) F" unfolding h_def using assms(2) assms(3) tendsto_inverse_ereal by auto have "((\x. f x * h x) \ l * (1/m)) F" @@ -766,11 +766,11 @@ text \The assumptions of @{thm tendsto_diff_ereal} are too strong, we weaken them here.\ -lemma%important tendsto_diff_ereal_general [tendsto_intros]: +lemma tendsto_diff_ereal_general [tendsto_intros]: fixes u v::"'a \ ereal" assumes "(u \ l) F" "(v \ m) F" "\((l = \ \ m = \) \ (l = -\ \ m = -\))" shows "((\n. u n - v n) \ l - m) F" -proof%unimportant - +proof - have "((\n. u n + (-v n)) \ l + (-m)) F" apply (intro tendsto_intros assms) using assms by (auto simp add: ereal_uminus_eq_reorder) then show ?thesis by (simp add: minus_ereal_def) @@ -780,11 +780,11 @@ "(\ n::nat. real n) \ \" by (simp add: filterlim_real_sequentially tendsto_PInfty_eq_at_top) -lemma%important tendsto_at_top_pseudo_inverse [tendsto_intros]: +lemma tendsto_at_top_pseudo_inverse [tendsto_intros]: fixes u::"nat \ nat" assumes "LIM n sequentially. u n :> at_top" shows "LIM n sequentially. Inf {N. u N \ n} :> at_top" -proof%unimportant - +proof - { fix C::nat define M where "M = Max {u n| n. n \ C}+1" @@ -811,11 +811,11 @@ then show ?thesis using filterlim_at_top by auto qed -lemma%important pseudo_inverse_finite_set: +lemma pseudo_inverse_finite_set: fixes u::"nat \ nat" assumes "LIM n sequentially. u n :> at_top" shows "finite {N. u N \ n}" -proof%unimportant - +proof - fix n have "eventually (\N. u N \ n+1) sequentially" using assms by (simp add: filterlim_at_top) @@ -860,11 +860,11 @@ then show ?thesis by auto qed -lemma%important ereal_truncation_real_top [tendsto_intros]: +lemma ereal_truncation_real_top [tendsto_intros]: fixes x::ereal assumes "x \ - \" shows "(\n::nat. real_of_ereal(min x n)) \ x" -proof%unimportant (cases x) +proof (cases x) case (real r) then obtain K::nat where "K>0" "K > abs(r)" using reals_Archimedean2 gr0I by auto then have "min x n = x" if "n \ K" for n apply (subst real, subst real, auto) using that eq_iff by fastforce @@ -878,10 +878,10 @@ then show ?thesis using id_nat_ereal_tendsto_PInf PInf by auto qed (simp add: assms) -lemma%important ereal_truncation_bottom [tendsto_intros]: +lemma ereal_truncation_bottom [tendsto_intros]: fixes x::ereal shows "(\n::nat. max x (- real n)) \ x" -proof%unimportant (cases x) +proof (cases x) case (real r) then obtain K::nat where "K>0" "K > abs(r)" using reals_Archimedean2 gr0I by auto then have "max x (-real n) = x" if "n \ K" for n apply (subst real, subst real, auto) using that eq_iff by fastforce @@ -899,11 +899,11 @@ then show ?thesis by auto qed -lemma%important ereal_truncation_real_bottom [tendsto_intros]: +lemma ereal_truncation_real_bottom [tendsto_intros]: fixes x::ereal assumes "x \ \" shows "(\n::nat. real_of_ereal(max x (- real n))) \ x" -proof%unimportant (cases x) +proof (cases x) case (real r) then obtain K::nat where "K>0" "K > abs(r)" using reals_Archimedean2 gr0I by auto then have "max x (-real n) = x" if "n \ K" for n apply (subst real, subst real, auto) using that eq_iff by fastforce @@ -931,9 +931,9 @@ qed(simp) -lemma%important continuous_ereal_abs: +lemma continuous_ereal_abs: "continuous_on (UNIV::ereal set) abs" -proof%unimportant - +proof - have "continuous_on ({..0} \ {(0::ereal)..}) abs" apply (rule continuous_on_closed_Un, auto) apply (rule iffD1[OF continuous_on_cong, of "{..0}" _ "\x. -x"]) @@ -970,11 +970,11 @@ then show ?thesis by auto qed -lemma%important tendsto_mult_ennreal [tendsto_intros]: +lemma tendsto_mult_ennreal [tendsto_intros]: fixes l m::ennreal assumes "(u \ l) F" "(v \ m) F" "\((l = 0 \ m = \) \ (l = \ \ m = 0))" shows "((\n. u n * v n) \ l * m) F" -proof%unimportant - +proof - have "((\n. e2ennreal(enn2ereal (u n) * enn2ereal (v n))) \ e2ennreal(enn2ereal l * enn2ereal m)) F" apply (intro tendsto_intros) using assms apply auto using enn2ereal_inject zero_ennreal.rep_eq by fastforce+ @@ -987,9 +987,9 @@ qed -subsection%important \monoset\ +subsection%important \monoset\ (*FIX ME title *) -definition%important (in order) mono_set: +definition (in order) mono_set: "mono_set S \ (\x y. x \ y \ x \ S \ y \ S)" lemma (in order) mono_greaterThan [intro, simp]: "mono_set {B<..}" unfolding mono_set by auto @@ -997,11 +997,11 @@ lemma (in order) mono_UNIV [intro, simp]: "mono_set UNIV" unfolding mono_set by auto lemma (in order) mono_empty [intro, simp]: "mono_set {}" unfolding mono_set by auto -lemma%important (in complete_linorder) mono_set_iff: +lemma (in complete_linorder) mono_set_iff: fixes S :: "'a set" defines "a \ Inf S" shows "mono_set S \ S = {a <..} \ S = {a..}" (is "_ = ?c") -proof%unimportant +proof assume "mono_set S" then have mono: "\x y. x \ y \ x \ S \ y \ S" by (auto simp: mono_set) @@ -1043,12 +1043,12 @@ by (metis Inf_UNIV atLeast_eq_UNIV_iff closed_ereal_atLeast ereal_open_closed mono_empty mono_set_iff open_ereal_greaterThan) -lemma%important ereal_Liminf_Sup_monoset: +lemma ereal_Liminf_Sup_monoset: fixes f :: "'a \ ereal" shows "Liminf net f = Sup {l. \S. open S \ mono_set S \ l \ S \ eventually (\x. f x \ S) net}" (is "_ = Sup ?A") -proof%unimportant (safe intro!: Liminf_eqI complete_lattice_class.Sup_upper complete_lattice_class.Sup_least) +proof (safe intro!: Liminf_eqI complete_lattice_class.Sup_upper complete_lattice_class.Sup_least) fix P assume P: "eventually P net" fix S @@ -1082,12 +1082,12 @@ qed qed -lemma%important ereal_Limsup_Inf_monoset: +lemma ereal_Limsup_Inf_monoset: fixes f :: "'a \ ereal" shows "Limsup net f = Inf {l. \S. open S \ mono_set (uminus ` S) \ l \ S \ eventually (\x. f x \ S) net}" (is "_ = Inf ?A") -proof%unimportant (safe intro!: Limsup_eqI complete_lattice_class.Inf_lower complete_lattice_class.Inf_greatest) +proof (safe intro!: Limsup_eqI complete_lattice_class.Inf_lower complete_lattice_class.Inf_greatest) fix P assume P: "eventually P net" fix S @@ -1121,11 +1121,11 @@ qed qed -lemma%important liminf_bounded_open: +lemma liminf_bounded_open: fixes x :: "nat \ ereal" shows "x0 \ liminf x \ (\S. open S \ mono_set S \ x0 \ S \ (\N. \n\N. x n \ S))" (is "_ \ ?P x0") -proof%unimportant +proof assume "?P x0" then show "x0 \ liminf x" unfolding ereal_Liminf_Sup_monoset eventually_sequentially @@ -1159,11 +1159,11 @@ by auto qed -lemma%important limsup_finite_then_bounded: +lemma limsup_finite_then_bounded: fixes u::"nat \ real" assumes "limsup u < \" shows "\C. \n. u n \ C" -proof%unimportant - +proof - obtain C where C: "limsup u < C" "C < \" using assms ereal_dense2 by blast then have "C = ereal(real_of_ereal C)" using ereal_real by force have "eventually (\n. u n < C) sequentially" using C(1) unfolding Limsup_def @@ -1273,11 +1273,11 @@ then show ?case using Suc.IH by simp qed (auto) -lemma%important Limsup_obtain: +lemma Limsup_obtain: fixes u::"_ \ 'a :: complete_linorder" assumes "Limsup F u > c" shows "\i. u i > c" -proof%unimportant - +proof - have "(INF P\{P. eventually P F}. SUP x\{x. P x}. u x) > c" using assms by (simp add: Limsup_def) then show ?thesis by (metis eventually_True mem_Collect_eq less_INF_D less_SUP_iff) qed @@ -1285,10 +1285,10 @@ text \The next lemma is extremely useful, as it often makes it possible to reduce statements about limsups to statements about limits.\ -lemma%important limsup_subseq_lim: +lemma limsup_subseq_lim: fixes u::"nat \ 'a :: {complete_linorder, linorder_topology}" shows "\r::nat\nat. strict_mono r \ (u o r) \ limsup u" -proof%unimportant (cases) +proof (cases) assume "\n. \p>n. \m\p. u m \ u p" then have "\r. \n. (\m\r n. u m \ u (r n)) \ r n < r (Suc n)" by (intro dependent_nat_choice) (auto simp: conj_commute) @@ -1378,10 +1378,10 @@ then show ?thesis using \strict_mono r\ by auto qed -lemma%important liminf_subseq_lim: +lemma liminf_subseq_lim: fixes u::"nat \ 'a :: {complete_linorder, linorder_topology}" shows "\r::nat\nat. strict_mono r \ (u o r) \ liminf u" -proof%unimportant (cases) +proof (cases) assume "\n. \p>n. \m\p. u m \ u p" then have "\r. \n. (\m\r n. u m \ u (r n)) \ r n < r (Suc n)" by (intro dependent_nat_choice) (auto simp: conj_commute) @@ -1476,10 +1476,10 @@ subsequences thanks to \limsup_subseq_lim\. The statement for limits follows for instance from \tendsto_add_ereal_general\.\ -lemma%important ereal_limsup_add_mono: +lemma ereal_limsup_add_mono: fixes u v::"nat \ ereal" shows "limsup (\n. u n + v n) \ limsup u + limsup v" -proof%unimportant (cases) +proof (cases) assume "(limsup u = \) \ (limsup v = \)" then have "limsup u + limsup v = \" by simp then show ?thesis by auto @@ -1522,11 +1522,11 @@ This explains why there are more assumptions in the next lemma dealing with liminfs that in the previous one about limsups.\ -lemma%important ereal_liminf_add_mono: +lemma ereal_liminf_add_mono: fixes u v::"nat \ ereal" assumes "\((liminf u = \ \ liminf v = -\) \ (liminf u = -\ \ liminf v = \))" shows "liminf (\n. u n + v n) \ liminf u + liminf v" -proof%unimportant (cases) +proof (cases) assume "(liminf u = -\) \ (liminf v = -\)" then have *: "liminf u + liminf v = -\" using assms by auto show ?thesis by (simp add: *) @@ -1565,11 +1565,11 @@ then show ?thesis unfolding w_def by simp qed -lemma%important ereal_limsup_lim_add: +lemma ereal_limsup_lim_add: fixes u v::"nat \ ereal" assumes "u \ a" "abs(a) \ \" shows "limsup (\n. u n + v n) = a + limsup v" -proof%unimportant - +proof - have "limsup u = a" using assms(1) using tendsto_iff_Liminf_eq_Limsup trivial_limit_at_top_linorder by blast have "(\n. -u n) \ -a" using assms(1) by auto then have "limsup (\n. -u n) = -a" using tendsto_iff_Liminf_eq_Limsup trivial_limit_at_top_linorder by blast @@ -1596,11 +1596,11 @@ then show ?thesis using up by simp qed -lemma%important ereal_limsup_lim_mult: +lemma ereal_limsup_lim_mult: fixes u v::"nat \ ereal" assumes "u \ a" "a>0" "a \ \" shows "limsup (\n. u n * v n) = a * limsup v" -proof%unimportant - +proof - define w where "w = (\n. u n * v n)" obtain r where r: "strict_mono r" "(v o r) \ limsup v" using limsup_subseq_lim by auto have "(u o r) \ a" using assms(1) LIMSEQ_subseq_LIMSEQ r by auto @@ -1626,11 +1626,11 @@ then show ?thesis using I unfolding w_def by auto qed -lemma%important ereal_liminf_lim_mult: +lemma ereal_liminf_lim_mult: fixes u v::"nat \ ereal" assumes "u \ a" "a>0" "a \ \" shows "liminf (\n. u n * v n) = a * liminf v" -proof%unimportant - +proof - define w where "w = (\n. u n * v n)" obtain r where r: "strict_mono r" "(v o r) \ liminf v" using liminf_subseq_lim by auto have "(u o r) \ a" using assms(1) LIMSEQ_subseq_LIMSEQ r by auto @@ -1656,11 +1656,11 @@ then show ?thesis using I unfolding w_def by auto qed -lemma%important ereal_liminf_lim_add: +lemma ereal_liminf_lim_add: fixes u v::"nat \ ereal" assumes "u \ a" "abs(a) \ \" shows "liminf (\n. u n + v n) = a + liminf v" -proof%unimportant - +proof - have "liminf u = a" using assms(1) tendsto_iff_Liminf_eq_Limsup trivial_limit_at_top_linorder by blast then have *: "abs(liminf u) \ \" using assms(2) by auto have "(\n. -u n) \ -a" using assms(1) by auto @@ -1689,10 +1689,10 @@ then show ?thesis using up by simp qed -lemma%important ereal_liminf_limsup_add: +lemma ereal_liminf_limsup_add: fixes u v::"nat \ ereal" shows "liminf (\n. u n + v n) \ liminf u + limsup v" -proof%unimportant (cases) +proof (cases) assume "limsup v = \ \ liminf u = \" then show ?thesis by auto next @@ -1741,12 +1741,12 @@ done -lemma%important liminf_minus_ennreal: +lemma liminf_minus_ennreal: fixes u v::"nat \ ennreal" shows "(\n. v n \ u n) \ liminf (\n. u n - v n) \ limsup u - limsup v" unfolding liminf_SUP_INF limsup_INF_SUP including ennreal.lifting -proof%unimportant (transfer, clarsimp) +proof (transfer, clarsimp) fix v u :: "nat \ ereal" assume *: "\x. 0 \ v x" "\x. 0 \ u x" "\n. v n \ u n" moreover have "0 \ limsup u - limsup v" using * by (intro ereal_diff_positive Limsup_mono always_eventually) simp @@ -1759,7 +1759,7 @@ by (auto simp: * ereal_diff_positive max.absorb2 liminf_SUP_INF[symmetric] limsup_INF_SUP[symmetric] ereal_liminf_limsup_minus) qed -subsection%unimportant "Relate extended reals and the indicator function" +subsection%important "Relate extended reals and the indicator function" lemma ereal_indicator_le_0: "(indicator S x::ereal) \ 0 \ x \ S" by (auto split: split_indicator simp: one_ereal_def) diff -r a03a63b81f44 -r a06b204527e6 src/HOL/Analysis/Fashoda_Theorem.thy --- a/src/HOL/Analysis/Fashoda_Theorem.thy Mon Jan 14 18:35:03 2019 +0000 +++ b/src/HOL/Analysis/Fashoda_Theorem.thy Wed Jan 16 21:27:33 2019 +0000 @@ -30,14 +30,14 @@ apply (rule, rule continuous_interval_bij) done -lemma%important in_interval_interval_bij: +lemma in_interval_interval_bij: fixes a b u v x :: "'a::euclidean_space" assumes "x \ cbox a b" and "cbox u v \ {}" shows "interval_bij (a, b) (u, v) x \ cbox u v" apply (simp only: interval_bij_def split_conv mem_box inner_sum_left_Basis cong: ball_cong) apply safe -proof%unimportant - +proof - fix i :: 'a assume i: "i \ Basis" have "cbox a b \ {}" @@ -89,7 +89,7 @@ shows "\x$1\ \ 1" and "\x$2\ \ 1" using assms unfolding infnorm_eq_1_2 by auto -lemma%important fashoda_unit: +proposition fashoda_unit: fixes f g :: "real \ real^2" assumes "f ` {-1 .. 1} \ cbox (-1) 1" and "g ` {-1 .. 1} \ cbox (-1) 1" @@ -99,7 +99,7 @@ and "f 1$1 = 1" "g (- 1) $2 = -1" and "g 1 $2 = 1" shows "\s\{-1 .. 1}. \t\{-1 .. 1}. f s = g t" -proof%unimportant (rule ccontr) +proof (rule ccontr) assume "\ ?thesis" note as = this[unfolded bex_simps,rule_format] define sqprojection @@ -256,7 +256,7 @@ qed qed -lemma%important fashoda_unit_path: +proposition fashoda_unit_path: fixes f g :: "real \ real^2" assumes "path f" and "path g" @@ -267,7 +267,7 @@ and "(pathstart g)$2 = -1" and "(pathfinish g)$2 = 1" obtains z where "z \ path_image f" and "z \ path_image g" -proof%unimportant - +proof - note assms=assms[unfolded path_def pathstart_def pathfinish_def path_image_def] define iscale where [abs_def]: "iscale z = inverse 2 *\<^sub>R (z + 1)" for z :: real have isc: "iscale ` {- 1..1} \ {0..1}" @@ -312,7 +312,7 @@ done qed -lemma%important fashoda: +theorem fashoda: fixes b :: "real^2" assumes "path f" and "path g" @@ -323,7 +323,7 @@ and "(pathstart g)$2 = a$2" and "(pathfinish g)$2 = b$2" obtains z where "z \ path_image f" and "z \ path_image g" -proof%unimportant - +proof - fix P Q S presume "P \ Q \ S" "P \ thesis" and "Q \ thesis" and "S \ thesis" then show thesis @@ -632,7 +632,7 @@ subsection%important \Useful Fashoda corollary pointed out to me by Tom Hales\(*FIXME change title? *) -lemma%important fashoda_interlace: +corollary fashoda_interlace: fixes a :: "real^2" assumes "path f" and "path g" @@ -646,7 +646,7 @@ and "(pathstart g)$1 < (pathfinish f)$1" and "(pathfinish f)$1 < (pathfinish g)$1" obtains z where "z \ path_image f" and "z \ path_image g" -proof%unimportant - +proof - have "cbox a b \ {}" using path_image_nonempty[of f] using assms(3) by auto note ab=this[unfolded interval_eq_empty_cart not_ex forall_2 not_less] diff -r a03a63b81f44 -r a06b204527e6 src/HOL/Analysis/Finite_Cartesian_Product.thy --- a/src/HOL/Analysis/Finite_Cartesian_Product.thy Mon Jan 14 18:35:03 2019 +0000 +++ b/src/HOL/Analysis/Finite_Cartesian_Product.thy Wed Jan 16 21:27:33 2019 +0000 @@ -13,7 +13,7 @@ "HOL-Library.FuncSet" begin -subsection%unimportant \Finite Cartesian products, with indexing and lambdas\ +subsection%important \Finite Cartesian products, with indexing and lambdas\ typedef ('a, 'b) vec = "UNIV :: ('b::finite \ 'a) set" morphisms vec_nth vec_lambda .. @@ -104,10 +104,10 @@ by (auto elim!: countableE) qed -lemma%important infinite_UNIV_vec: +lemma infinite_UNIV_vec: assumes "infinite (UNIV :: 'a set)" shows "infinite (UNIV :: ('a^'b) set)" -proof%unimportant (subst bij_betw_finite) +proof (subst bij_betw_finite) show "bij_betw vec_nth UNIV (Pi (UNIV :: 'b set) (\_. UNIV :: 'a set))" by (intro bij_betwI[of _ _ _ vec_lambda]) (auto simp: vec_eq_iff) have "infinite (PiE (UNIV :: 'b set) (\_. UNIV :: 'a set))" (is "infinite ?A") @@ -125,9 +125,9 @@ finally show "infinite (Pi (UNIV :: 'b set) (\_. UNIV :: 'a set))" . qed -lemma%important CARD_vec [simp]: +lemma CARD_vec [simp]: "CARD('a^'b) = CARD('a) ^ CARD('b)" -proof%unimportant (cases "finite (UNIV :: 'a set)") +proof (cases "finite (UNIV :: 'a set)") case True show ?thesis proof (subst bij_betw_same_card) @@ -143,7 +143,7 @@ qed qed (simp_all add: infinite_UNIV_vec) -lemma%unimportant countable_vector: +lemma countable_vector: fixes B:: "'n::finite \ 'a set" assumes "\i. countable (B i)" shows "countable {V. \i::'n::finite. V $ i \ B i}" @@ -165,7 +165,7 @@ by (simp add: image_comp o_def vec_nth_inverse) qed -subsection%unimportant \Group operations and class instances\ +subsection%important \Group operations and class instances\ instantiation vec :: (zero, finite) zero begin @@ -230,7 +230,7 @@ by standard (simp_all add: vec_eq_iff) -subsection%unimportant\Basic componentwise operations on vectors\ +subsection%important\Basic componentwise operations on vectors\ instantiation vec :: (times, finite) times begin @@ -295,12 +295,12 @@ text\Also the scalar-vector multiplication.\ -definition vector_scalar_mult:: "'a::times \ 'a ^ 'n \ 'a ^ 'n" (infixl "*s" 70) +definition%important vector_scalar_mult:: "'a::times \ 'a ^ 'n \ 'a ^ 'n" (infixl "*s" 70) where "c *s x = (\ i. c * (x$i))" text \scalar product\ -definition scalar_product :: "'a :: semiring_1 ^ 'n \ 'a ^ 'n \ 'a" where +definition%important scalar_product :: "'a :: semiring_1 ^ 'n \ 'a ^ 'n \ 'a" where "scalar_product v w = (\ i \ UNIV. v $ i * w $ i)" @@ -311,7 +311,7 @@ definition%important "scaleR \ (\ r x. (\ i. scaleR r (x$i)))" -lemma%important vector_scaleR_component [simp]: "(scaleR r x)$i = scaleR r (x$i)" +lemma vector_scaleR_component [simp]: "(scaleR r x)$i = scaleR r (x$i)" unfolding scaleR_vec_def by simp instance%unimportant @@ -330,7 +330,7 @@ (\x\S. \A. (\i. open (A i) \ x$i \ A i) \ (\y. (\i. y$i \ A i) \ y \ S))" -instance proof%unimportant +instance proof show "open (UNIV :: ('a ^ 'b) set)" unfolding open_vec_def by auto next @@ -358,30 +358,30 @@ end -lemma%unimportant open_vector_box: "\i. open (S i) \ open {x. \i. x $ i \ S i}" +lemma open_vector_box: "\i. open (S i) \ open {x. \i. x $ i \ S i}" unfolding open_vec_def by auto -lemma%unimportant open_vimage_vec_nth: "open S \ open ((\x. x $ i) -` S)" +lemma open_vimage_vec_nth: "open S \ open ((\x. x $ i) -` S)" unfolding open_vec_def apply clarify apply (rule_tac x="\k. if k = i then S else UNIV" in exI, simp) done -lemma%unimportant closed_vimage_vec_nth: "closed S \ closed ((\x. x $ i) -` S)" +lemma closed_vimage_vec_nth: "closed S \ closed ((\x. x $ i) -` S)" unfolding closed_open vimage_Compl [symmetric] by (rule open_vimage_vec_nth) -lemma%unimportant closed_vector_box: "\i. closed (S i) \ closed {x. \i. x $ i \ S i}" +lemma closed_vector_box: "\i. closed (S i) \ closed {x. \i. x $ i \ S i}" proof - have "{x. \i. x $ i \ S i} = (\i. (\x. x $ i) -` S i)" by auto thus "\i. closed (S i) \ closed {x. \i. x $ i \ S i}" by (simp add: closed_INT closed_vimage_vec_nth) qed -lemma%important tendsto_vec_nth [tendsto_intros]: +lemma tendsto_vec_nth [tendsto_intros]: assumes "((\x. f x) \ a) net" shows "((\x. f x $ i) \ a $ i) net" -proof%unimportant (rule topological_tendstoI) +proof (rule topological_tendstoI) fix S assume "open S" "a $ i \ S" then have "open ((\y. y $ i) -` S)" "a \ ((\y. y $ i) -` S)" by (simp_all add: open_vimage_vec_nth) @@ -391,13 +391,13 @@ by simp qed -lemma%unimportant isCont_vec_nth [simp]: "isCont f a \ isCont (\x. f x $ i) a" +lemma isCont_vec_nth [simp]: "isCont f a \ isCont (\x. f x $ i) a" unfolding isCont_def by (rule tendsto_vec_nth) -lemma%important vec_tendstoI: +lemma vec_tendstoI: assumes "\i. ((\x. f x $ i) \ a $ i) net" shows "((\x. f x) \ a) net" -proof%unimportant (rule topological_tendstoI) +proof (rule topological_tendstoI) fix S assume "open S" and "a \ S" then obtain A where A: "\i. open (A i)" "\i. a $ i \ A i" and S: "\y. \i. y $ i \ A i \ y \ S" @@ -410,13 +410,13 @@ by (rule eventually_mono, simp add: S) qed -lemma%unimportant tendsto_vec_lambda [tendsto_intros]: +lemma tendsto_vec_lambda [tendsto_intros]: assumes "\i. ((\x. f x i) \ a i) net" shows "((\x. \ i. f x i) \ (\ i. a i)) net" using assms by (simp add: vec_tendstoI) -lemma%important open_image_vec_nth: assumes "open S" shows "open ((\x. x $ i) ` S)" -proof%unimportant (rule openI) +lemma open_image_vec_nth: assumes "open S" shows "open ((\x. x $ i) ` S)" +proof (rule openI) fix a assume "a \ (\x. x $ i) ` S" then obtain z where "a = z $ i" and "z \ S" .. then obtain A where A: "\i. open (A i) \ z $ i \ A i" @@ -470,10 +470,10 @@ instantiation%unimportant vec :: (metric_space, finite) metric_space begin -lemma%important dist_vec_nth_le: "dist (x $ i) (y $ i) \ dist x y" +lemma dist_vec_nth_le: "dist (x $ i) (y $ i) \ dist x y" unfolding dist_vec_def by (rule member_le_L2_set) simp_all -instance proof%unimportant +instance proof fix x y :: "'a ^ 'b" show "dist x y = 0 \ x = y" unfolding dist_vec_def @@ -532,15 +532,15 @@ end -lemma%important Cauchy_vec_nth: +lemma Cauchy_vec_nth: "Cauchy (\n. X n) \ Cauchy (\n. X n $ i)" unfolding Cauchy_def by (fast intro: le_less_trans [OF dist_vec_nth_le]) -lemma%important vec_CauchyI: +lemma vec_CauchyI: fixes X :: "nat \ 'a::metric_space ^ 'n" assumes X: "\i. Cauchy (\n. X n $ i)" shows "Cauchy (\n. X n)" -proof%unimportant (rule metric_CauchyI) +proof (rule metric_CauchyI) fix r :: real assume "0 < r" hence "0 < r / of_nat CARD('n)" (is "0 < ?s") by simp define N where "N i = (LEAST N. \m\N. \n\N. dist (X m $ i) (X n $ i) < ?s)" for i @@ -591,7 +591,7 @@ definition%important "sgn (x::'a^'b) = scaleR (inverse (norm x)) x" -instance proof%unimportant +instance proof fix a :: real and x y :: "'a ^ 'b" show "norm x = 0 \ x = 0" unfolding norm_vec_def @@ -613,32 +613,32 @@ end -lemma%unimportant norm_nth_le: "norm (x $ i) \ norm x" +lemma norm_nth_le: "norm (x $ i) \ norm x" unfolding norm_vec_def by (rule member_le_L2_set) simp_all -lemma%important norm_le_componentwise_cart: +lemma norm_le_componentwise_cart: fixes x :: "'a::real_normed_vector^'n" assumes "\i. norm(x$i) \ norm(y$i)" shows "norm x \ norm y" - unfolding%unimportant norm_vec_def - by%unimportant (rule L2_set_mono) (auto simp: assms) + unfolding norm_vec_def + by (rule L2_set_mono) (auto simp: assms) -lemma%unimportant component_le_norm_cart: "\x$i\ \ norm x" +lemma component_le_norm_cart: "\x$i\ \ norm x" apply (simp add: norm_vec_def) apply (rule member_le_L2_set, simp_all) done -lemma%unimportant norm_bound_component_le_cart: "norm x \ e ==> \x$i\ \ e" +lemma norm_bound_component_le_cart: "norm x \ e ==> \x$i\ \ e" by (metis component_le_norm_cart order_trans) -lemma%unimportant norm_bound_component_lt_cart: "norm x < e ==> \x$i\ < e" +lemma norm_bound_component_lt_cart: "norm x < e ==> \x$i\ < e" by (metis component_le_norm_cart le_less_trans) -lemma%unimportant norm_le_l1_cart: "norm x \ sum(\i. \x$i\) UNIV" +lemma norm_le_l1_cart: "norm x \ sum(\i. \x$i\) UNIV" by (simp add: norm_vec_def L2_set_le_sum) -lemma%unimportant bounded_linear_vec_nth: "bounded_linear (\x. x $ i)" +lemma bounded_linear_vec_nth: "bounded_linear (\x. x $ i)" apply standard apply (rule vector_add_component) apply (rule vector_scaleR_component) @@ -655,7 +655,7 @@ definition%important "inner x y = sum (\i. inner (x$i) (y$i)) UNIV" -instance proof%unimportant +instance proof fix r :: real and x y z :: "'a ^ 'b" show "inner x y = inner y x" unfolding inner_vec_def @@ -686,13 +686,13 @@ definition%important "axis k x = (\ i. if i = k then x else 0)" -lemma%unimportant axis_nth [simp]: "axis i x $ i = x" +lemma axis_nth [simp]: "axis i x $ i = x" unfolding axis_def by simp -lemma%unimportant axis_eq_axis: "axis i x = axis j y \ x = y \ i = j \ x = 0 \ y = 0" +lemma axis_eq_axis: "axis i x = axis j y \ x = y \ i = j \ x = 0 \ y = 0" unfolding axis_def vec_eq_iff by auto -lemma%unimportant inner_axis_axis: +lemma inner_axis_axis: "inner (axis i x) (axis j y) = (if i = j then inner x y else 0)" unfolding inner_vec_def apply (cases "i = j") @@ -702,10 +702,10 @@ apply (rule sum.neutral, simp add: axis_def) done -lemma%unimportant inner_axis: "inner x (axis i y) = inner (x $ i) y" +lemma inner_axis: "inner x (axis i y) = inner (x $ i) y" by (simp add: inner_vec_def axis_def sum.remove [where x=i]) -lemma%unimportant inner_axis': "inner(axis i y) x = inner y (x $ i)" +lemma inner_axis': "inner(axis i y) x = inner y (x $ i)" by (simp add: inner_axis inner_commute) instantiation%unimportant vec :: (euclidean_space, finite) euclidean_space @@ -713,7 +713,7 @@ definition%important "Basis = (\i. \u\Basis. {axis i u})" -instance proof%unimportant +instance proof show "(Basis :: ('a ^ 'b) set) \ {}" unfolding Basis_vec_def by simp next @@ -732,8 +732,8 @@ by (simp add: inner_axis euclidean_all_zero_iff vec_eq_iff) qed -lemma%important DIM_cart [simp]: "DIM('a^'b) = CARD('b) * DIM('a)" -proof%unimportant - +proposition DIM_cart [simp]: "DIM('a^'b) = CARD('b) * DIM('a)" +proof - have "card (\i::'b. \u::'a\Basis. {axis i u}) = (\i::'b\UNIV. card (\u::'a\Basis. {axis i u}))" by (rule card_UN_disjoint) (auto simp: axis_eq_axis) also have "... = CARD('b) * DIM('a)" @@ -744,30 +744,30 @@ end -lemma%unimportant norm_axis_1 [simp]: "norm (axis m (1::real)) = 1" +lemma norm_axis_1 [simp]: "norm (axis m (1::real)) = 1" by (simp add: inner_axis' norm_eq_1) -lemma%important sum_norm_allsubsets_bound_cart: +lemma sum_norm_allsubsets_bound_cart: fixes f:: "'a \ real ^'n" assumes fP: "finite P" and fPs: "\Q. Q \ P \ norm (sum f Q) \ e" shows "sum (\x. norm (f x)) P \ 2 * real CARD('n) * e" - using%unimportant sum_norm_allsubsets_bound[OF assms] - by%unimportant simp + using sum_norm_allsubsets_bound[OF assms] + by simp -lemma%unimportant cart_eq_inner_axis: "a $ i = inner a (axis i 1)" +lemma cart_eq_inner_axis: "a $ i = inner a (axis i 1)" by (simp add: inner_axis) -lemma%unimportant axis_eq_0_iff [simp]: +lemma axis_eq_0_iff [simp]: shows "axis m x = 0 \ x = 0" by (simp add: axis_def vec_eq_iff) -lemma%unimportant axis_in_Basis_iff [simp]: "axis i a \ Basis \ a \ Basis" +lemma axis_in_Basis_iff [simp]: "axis i a \ Basis \ a \ Basis" by (auto simp: Basis_vec_def axis_eq_axis) text\Mapping each basis element to the corresponding finite index\ definition axis_index :: "('a::comm_ring_1)^'n \ 'n" where "axis_index v \ SOME i. v = axis i 1" -lemma%unimportant axis_inverse: +lemma axis_inverse: fixes v :: "real^'n" assumes "v \ Basis" shows "\i. v = axis i 1" @@ -778,20 +778,20 @@ by (force simp add: vec_eq_iff) qed -lemma%unimportant axis_index: +lemma axis_index: fixes v :: "real^'n" assumes "v \ Basis" shows "v = axis (axis_index v) 1" by (metis (mono_tags) assms axis_inverse axis_index_def someI_ex) -lemma%unimportant axis_index_axis [simp]: +lemma axis_index_axis [simp]: fixes UU :: "real^'n" shows "(axis_index (axis u 1 :: real^'n)) = (u::'n)" by (simp add: axis_eq_axis axis_index_def) subsection%unimportant \A naive proof procedure to lift really trivial arithmetic stuff from the basis of the vector space\ -lemma%unimportant sum_cong_aux: +lemma sum_cong_aux: "(\x. x \ A \ f x = g x) \ sum f A = sum g A" by (auto intro: sum.cong) @@ -823,22 +823,22 @@ end \ "lift trivial vector statements to real arith statements" -lemma%unimportant vec_0[simp]: "vec 0 = 0" by vector -lemma%unimportant vec_1[simp]: "vec 1 = 1" by vector +lemma vec_0[simp]: "vec 0 = 0" by vector +lemma vec_1[simp]: "vec 1 = 1" by vector -lemma%unimportant vec_inj[simp]: "vec x = vec y \ x = y" by vector +lemma vec_inj[simp]: "vec x = vec y \ x = y" by vector -lemma%unimportant vec_in_image_vec: "vec x \ (vec ` S) \ x \ S" by auto +lemma vec_in_image_vec: "vec x \ (vec ` S) \ x \ S" by auto -lemma%unimportant vec_add: "vec(x + y) = vec x + vec y" by vector -lemma%unimportant vec_sub: "vec(x - y) = vec x - vec y" by vector -lemma%unimportant vec_cmul: "vec(c * x) = c *s vec x " by vector -lemma%unimportant vec_neg: "vec(- x) = - vec x " by vector +lemma vec_add: "vec(x + y) = vec x + vec y" by vector +lemma vec_sub: "vec(x - y) = vec x - vec y" by vector +lemma vec_cmul: "vec(c * x) = c *s vec x " by vector +lemma vec_neg: "vec(- x) = - vec x " by vector -lemma%unimportant vec_scaleR: "vec(c * x) = c *\<^sub>R vec x" +lemma vec_scaleR: "vec(c * x) = c *\<^sub>R vec x" by vector -lemma%unimportant vec_sum: +lemma vec_sum: assumes "finite S" shows "vec(sum f S) = sum (vec \ f) S" using assms @@ -852,24 +852,24 @@ text\Obvious "component-pushing".\ -lemma%unimportant vec_component [simp]: "vec x $ i = x" +lemma vec_component [simp]: "vec x $ i = x" by vector -lemma%unimportant vector_mult_component [simp]: "(x * y)$i = x$i * y$i" +lemma vector_mult_component [simp]: "(x * y)$i = x$i * y$i" by vector -lemma%unimportant vector_smult_component [simp]: "(c *s y)$i = c * (y$i)" +lemma vector_smult_component [simp]: "(c *s y)$i = c * (y$i)" by vector -lemma%unimportant cond_component: "(if b then x else y)$i = (if b then x$i else y$i)" by vector +lemma cond_component: "(if b then x else y)$i = (if b then x$i else y$i)" by vector -lemmas%unimportant vector_component = +lemmas vector_component = vec_component vector_add_component vector_mult_component vector_smult_component vector_minus_component vector_uminus_component vector_scaleR_component cond_component -subsection%unimportant \Some frequently useful arithmetic lemmas over vectors\ +subsection%important \Some frequently useful arithmetic lemmas over vectors\ instance vec :: (semigroup_mult, finite) semigroup_mult by standard (vector mult.assoc) @@ -1011,7 +1011,7 @@ definition%important map_matrix::"('a \ 'b) \ (('a, 'i::finite)vec, 'j::finite) vec \ (('b, 'i)vec, 'j) vec" where "map_matrix f x = (\ i j. f (x $ i $ j))" -lemma%unimportant nth_map_matrix[simp]: "map_matrix f x $ i $ j = f (x $ i $ j)" +lemma nth_map_matrix[simp]: "map_matrix f x $ i $ j = f (x $ i $ j)" by (simp add: map_matrix_def) definition%important matrix_matrix_mult :: "('a::semiring_1) ^'n^'m \ 'a ^'p^'n \ 'a ^ 'p ^'m" @@ -1034,17 +1034,17 @@ definition%unimportant "rows(A::'a^'n^'m) = { row i A | i. i \ (UNIV :: 'm set)}" definition%unimportant "columns(A::'a^'n^'m) = { column i A | i. i \ (UNIV :: 'n set)}" -lemma%unimportant times0_left [simp]: "(0::'a::semiring_1^'n^'m) ** (A::'a ^'p^'n) = 0" +lemma times0_left [simp]: "(0::'a::semiring_1^'n^'m) ** (A::'a ^'p^'n) = 0" by (simp add: matrix_matrix_mult_def zero_vec_def) -lemma%unimportant times0_right [simp]: "(A::'a::semiring_1^'n^'m) ** (0::'a ^'p^'n) = 0" +lemma times0_right [simp]: "(A::'a::semiring_1^'n^'m) ** (0::'a ^'p^'n) = 0" by (simp add: matrix_matrix_mult_def zero_vec_def) -lemma%unimportant mat_0[simp]: "mat 0 = 0" by (vector mat_def) -lemma%unimportant matrix_add_ldistrib: "(A ** (B + C)) = (A ** B) + (A ** C)" +lemma mat_0[simp]: "mat 0 = 0" by (vector mat_def) +lemma matrix_add_ldistrib: "(A ** (B + C)) = (A ** B) + (A ** C)" by (vector matrix_matrix_mult_def sum.distrib[symmetric] field_simps) -lemma%unimportant matrix_mul_lid [simp]: +lemma matrix_mul_lid [simp]: fixes A :: "'a::semiring_1 ^ 'm ^ 'n" shows "mat 1 ** A = A" apply (simp add: matrix_matrix_mult_def mat_def) @@ -1053,7 +1053,7 @@ mult_1_left mult_zero_left if_True UNIV_I) done -lemma%unimportant matrix_mul_rid [simp]: +lemma matrix_mul_rid [simp]: fixes A :: "'a::semiring_1 ^ 'm ^ 'n" shows "A ** mat 1 = A" apply (simp add: matrix_matrix_mult_def mat_def) @@ -1062,39 +1062,39 @@ mult_1_right mult_zero_right if_True UNIV_I cong: if_cong) done -lemma%unimportant matrix_mul_assoc: "A ** (B ** C) = (A ** B) ** C" +proposition matrix_mul_assoc: "A ** (B ** C) = (A ** B) ** C" apply (vector matrix_matrix_mult_def sum_distrib_left sum_distrib_right mult.assoc) apply (subst sum.swap) apply simp done -lemma%unimportant matrix_vector_mul_assoc: "A *v (B *v x) = (A ** B) *v x" +proposition matrix_vector_mul_assoc: "A *v (B *v x) = (A ** B) *v x" apply (vector matrix_matrix_mult_def matrix_vector_mult_def sum_distrib_left sum_distrib_right mult.assoc) apply (subst sum.swap) apply simp done -lemma%unimportant scalar_matrix_assoc: +lemma scalar_matrix_assoc: fixes A :: "('a::real_algebra_1)^'m^'n" shows "k *\<^sub>R (A ** B) = (k *\<^sub>R A) ** B" by (simp add: matrix_matrix_mult_def sum_distrib_left mult_ac vec_eq_iff scaleR_sum_right) -lemma%unimportant matrix_scalar_ac: +lemma matrix_scalar_ac: fixes A :: "('a::real_algebra_1)^'m^'n" shows "A ** (k *\<^sub>R B) = k *\<^sub>R A ** B" by (simp add: matrix_matrix_mult_def sum_distrib_left mult_ac vec_eq_iff) -lemma%unimportant matrix_vector_mul_lid [simp]: "mat 1 *v x = (x::'a::semiring_1 ^ 'n)" +lemma matrix_vector_mul_lid [simp]: "mat 1 *v x = (x::'a::semiring_1 ^ 'n)" apply (vector matrix_vector_mult_def mat_def) apply (simp add: if_distrib if_distribR sum.delta' cong del: if_weak_cong) done -lemma%unimportant matrix_transpose_mul: +lemma matrix_transpose_mul: "transpose(A ** B) = transpose B ** transpose (A::'a::comm_semiring_1^_^_)" by (simp add: matrix_matrix_mult_def transpose_def vec_eq_iff mult.commute) -lemma%unimportant matrix_eq: +lemma matrix_eq: fixes A B :: "'a::semiring_1 ^ 'n ^ 'm" shows "A = B \ (\x. A *v x = B *v x)" (is "?lhs \ ?rhs") apply auto @@ -1107,49 +1107,49 @@ sum.delta[OF finite] cong del: if_weak_cong) done -lemma%unimportant matrix_vector_mul_component: "(A *v x)$k = inner (A$k) x" +lemma matrix_vector_mul_component: "(A *v x)$k = inner (A$k) x" by (simp add: matrix_vector_mult_def inner_vec_def) -lemma%unimportant dot_lmul_matrix: "inner ((x::real ^_) v* A) y = inner x (A *v y)" +lemma dot_lmul_matrix: "inner ((x::real ^_) v* A) y = inner x (A *v y)" apply (simp add: inner_vec_def matrix_vector_mult_def vector_matrix_mult_def sum_distrib_right sum_distrib_left ac_simps) apply (subst sum.swap) apply simp done -lemma%unimportant transpose_mat [simp]: "transpose (mat n) = mat n" +lemma transpose_mat [simp]: "transpose (mat n) = mat n" by (vector transpose_def mat_def) -lemma%unimportant transpose_transpose [simp]: "transpose(transpose A) = A" +lemma transpose_transpose [simp]: "transpose(transpose A) = A" by (vector transpose_def) -lemma%unimportant row_transpose [simp]: "row i (transpose A) = column i A" +lemma row_transpose [simp]: "row i (transpose A) = column i A" by (simp add: row_def column_def transpose_def vec_eq_iff) -lemma%unimportant column_transpose [simp]: "column i (transpose A) = row i A" +lemma column_transpose [simp]: "column i (transpose A) = row i A" by (simp add: row_def column_def transpose_def vec_eq_iff) -lemma%unimportant rows_transpose [simp]: "rows(transpose A) = columns A" +lemma rows_transpose [simp]: "rows(transpose A) = columns A" by (auto simp add: rows_def columns_def intro: set_eqI) -lemma%unimportant columns_transpose [simp]: "columns(transpose A) = rows A" +lemma columns_transpose [simp]: "columns(transpose A) = rows A" by (metis transpose_transpose rows_transpose) -lemma%unimportant transpose_scalar: "transpose (k *\<^sub>R A) = k *\<^sub>R transpose A" +lemma transpose_scalar: "transpose (k *\<^sub>R A) = k *\<^sub>R transpose A" unfolding transpose_def by (simp add: vec_eq_iff) -lemma%unimportant transpose_iff [iff]: "transpose A = transpose B \ A = B" +lemma transpose_iff [iff]: "transpose A = transpose B \ A = B" by (metis transpose_transpose) -lemma%unimportant matrix_mult_sum: +lemma matrix_mult_sum: "(A::'a::comm_semiring_1^'n^'m) *v x = sum (\i. (x$i) *s column i A) (UNIV:: 'n set)" by (simp add: matrix_vector_mult_def vec_eq_iff column_def mult.commute) -lemma%unimportant vector_componentwise: +lemma vector_componentwise: "(x::'a::ring_1^'n) = (\ j. \i\UNIV. (x$i) * (axis i 1 :: 'a^'n) $ j)" by (simp add: axis_def if_distrib sum.If_cases vec_eq_iff) -lemma%unimportant basis_expansion: "sum (\i. (x$i) *s axis i 1) UNIV = (x::('a::ring_1) ^'n)" +lemma basis_expansion: "sum (\i. (x$i) *s axis i 1) UNIV = (x::('a::ring_1) ^'n)" by (auto simp add: axis_def vec_eq_iff if_distrib sum.If_cases cong del: if_weak_cong) @@ -1158,51 +1158,51 @@ definition%important matrix :: "('a::{plus,times, one, zero}^'m \ 'a ^ 'n) \ 'a^'m^'n" where "matrix f = (\ i j. (f(axis j 1))$i)" -lemma%unimportant matrix_id_mat_1: "matrix id = mat 1" +lemma matrix_id_mat_1: "matrix id = mat 1" by (simp add: mat_def matrix_def axis_def) -lemma%unimportant matrix_scaleR: "(matrix ((*\<^sub>R) r)) = mat r" +lemma matrix_scaleR: "(matrix ((*\<^sub>R) r)) = mat r" by (simp add: mat_def matrix_def axis_def if_distrib cong: if_cong) -lemma%unimportant matrix_vector_mul_linear[intro, simp]: "linear (\x. A *v (x::'a::real_algebra_1 ^ _))" +lemma matrix_vector_mul_linear[intro, simp]: "linear (\x. A *v (x::'a::real_algebra_1 ^ _))" by (simp add: linear_iff matrix_vector_mult_def vec_eq_iff field_simps sum_distrib_left sum.distrib scaleR_right.sum) -lemma%unimportant vector_matrix_left_distrib [algebra_simps]: +lemma vector_matrix_left_distrib [algebra_simps]: shows "(x + y) v* A = x v* A + y v* A" unfolding vector_matrix_mult_def by (simp add: algebra_simps sum.distrib vec_eq_iff) -lemma%unimportant matrix_vector_right_distrib [algebra_simps]: +lemma matrix_vector_right_distrib [algebra_simps]: "A *v (x + y) = A *v x + A *v y" by (vector matrix_vector_mult_def sum.distrib distrib_left) -lemma%unimportant matrix_vector_mult_diff_distrib [algebra_simps]: +lemma matrix_vector_mult_diff_distrib [algebra_simps]: fixes A :: "'a::ring_1^'n^'m" shows "A *v (x - y) = A *v x - A *v y" by (vector matrix_vector_mult_def sum_subtractf right_diff_distrib) -lemma%unimportant matrix_vector_mult_scaleR[algebra_simps]: +lemma matrix_vector_mult_scaleR[algebra_simps]: fixes A :: "real^'n^'m" shows "A *v (c *\<^sub>R x) = c *\<^sub>R (A *v x)" using linear_iff matrix_vector_mul_linear by blast -lemma%unimportant matrix_vector_mult_0_right [simp]: "A *v 0 = 0" +lemma matrix_vector_mult_0_right [simp]: "A *v 0 = 0" by (simp add: matrix_vector_mult_def vec_eq_iff) -lemma%unimportant matrix_vector_mult_0 [simp]: "0 *v w = 0" +lemma matrix_vector_mult_0 [simp]: "0 *v w = 0" by (simp add: matrix_vector_mult_def vec_eq_iff) -lemma%unimportant matrix_vector_mult_add_rdistrib [algebra_simps]: +lemma matrix_vector_mult_add_rdistrib [algebra_simps]: "(A + B) *v x = (A *v x) + (B *v x)" by (vector matrix_vector_mult_def sum.distrib distrib_right) -lemma%unimportant matrix_vector_mult_diff_rdistrib [algebra_simps]: +lemma matrix_vector_mult_diff_rdistrib [algebra_simps]: fixes A :: "'a :: ring_1^'n^'m" shows "(A - B) *v x = (A *v x) - (B *v x)" by (vector matrix_vector_mult_def sum_subtractf left_diff_distrib) -lemma%unimportant matrix_vector_column: +lemma matrix_vector_column: "(A::'a::comm_semiring_1^'n^_) *v x = sum (\i. (x$i) *s ((transpose A)$i)) (UNIV:: 'n set)" by (simp add: matrix_vector_mult_def transpose_def vec_eq_iff mult.commute) @@ -1215,17 +1215,17 @@ "matrix_inv(A:: 'a::semiring_1^'n^'m) = (SOME A'::'a^'m^'n. A ** A' = mat 1 \ A' ** A = mat 1)" -lemma%unimportant inj_matrix_vector_mult: +lemma inj_matrix_vector_mult: fixes A::"'a::field^'n^'m" assumes "invertible A" shows "inj ((*v) A)" by (metis assms inj_on_inverseI invertible_def matrix_vector_mul_assoc matrix_vector_mul_lid) -lemma%important scalar_invertible: +lemma scalar_invertible: fixes A :: "('a::real_algebra_1)^'m^'n" assumes "k \ 0" and "invertible A" shows "invertible (k *\<^sub>R A)" -proof%unimportant - +proof - obtain A' where "A ** A' = mat 1" and "A' ** A = mat 1" using assms unfolding invertible_def by auto with \k \ 0\ @@ -1235,50 +1235,50 @@ unfolding invertible_def by auto qed -lemma%unimportant scalar_invertible_iff: +lemma scalar_invertible_iff: fixes A :: "('a::real_algebra_1)^'m^'n" assumes "k \ 0" and "invertible A" shows "invertible (k *\<^sub>R A) \ k \ 0 \ invertible A" by (simp add: assms scalar_invertible) -lemma%unimportant vector_transpose_matrix [simp]: "x v* transpose A = A *v x" +lemma vector_transpose_matrix [simp]: "x v* transpose A = A *v x" unfolding transpose_def vector_matrix_mult_def matrix_vector_mult_def by simp -lemma%unimportant transpose_matrix_vector [simp]: "transpose A *v x = x v* A" +lemma transpose_matrix_vector [simp]: "transpose A *v x = x v* A" unfolding transpose_def vector_matrix_mult_def matrix_vector_mult_def by simp -lemma%unimportant vector_scalar_commute: +lemma vector_scalar_commute: fixes A :: "'a::{field}^'m^'n" shows "A *v (c *s x) = c *s (A *v x)" by (simp add: vector_scalar_mult_def matrix_vector_mult_def mult_ac sum_distrib_left) -lemma%unimportant scalar_vector_matrix_assoc: +lemma scalar_vector_matrix_assoc: fixes k :: "'a::{field}" and x :: "'a::{field}^'n" and A :: "'a^'m^'n" shows "(k *s x) v* A = k *s (x v* A)" by (metis transpose_matrix_vector vector_scalar_commute) -lemma%unimportant vector_matrix_mult_0 [simp]: "0 v* A = 0" +lemma vector_matrix_mult_0 [simp]: "0 v* A = 0" unfolding vector_matrix_mult_def by (simp add: zero_vec_def) -lemma%unimportant vector_matrix_mult_0_right [simp]: "x v* 0 = 0" +lemma vector_matrix_mult_0_right [simp]: "x v* 0 = 0" unfolding vector_matrix_mult_def by (simp add: zero_vec_def) -lemma%unimportant vector_matrix_mul_rid [simp]: +lemma vector_matrix_mul_rid [simp]: fixes v :: "('a::semiring_1)^'n" shows "v v* mat 1 = v" by (metis matrix_vector_mul_lid transpose_mat vector_transpose_matrix) -lemma%unimportant scaleR_vector_matrix_assoc: +lemma scaleR_vector_matrix_assoc: fixes k :: real and x :: "real^'n" and A :: "real^'m^'n" shows "(k *\<^sub>R x) v* A = k *\<^sub>R (x v* A)" by (metis matrix_vector_mult_scaleR transpose_matrix_vector) -lemma%important vector_scaleR_matrix_ac: +lemma vector_scaleR_matrix_ac: fixes k :: real and x :: "real^'n" and A :: "real^'m^'n" shows "x v* (k *\<^sub>R A) = k *\<^sub>R (x v* A)" -proof%unimportant - +proof - have "x v* (k *\<^sub>R A) = (k *\<^sub>R x) v* A" unfolding vector_matrix_mult_def by (simp add: algebra_simps) diff -r a03a63b81f44 -r a06b204527e6 src/HOL/Analysis/Finite_Product_Measure.thy --- a/src/HOL/Analysis/Finite_Product_Measure.thy Mon Jan 14 18:35:03 2019 +0000 +++ b/src/HOL/Analysis/Finite_Product_Measure.thy Wed Jan 16 21:27:33 2019 +0000 @@ -8,14 +8,14 @@ imports Binary_Product_Measure begin -lemma%unimportant PiE_choice: "(\f\Pi\<^sub>E I F. \i\I. P i (f i)) \ (\i\I. \x\F i. P i x)" +lemma PiE_choice: "(\f\Pi\<^sub>E I F. \i\I. P i (f i)) \ (\i\I. \x\F i. P i x)" by (auto simp: Bex_def PiE_iff Ball_def dest!: choice_iff'[THEN iffD1]) (force intro: exI[of _ "restrict f I" for f]) -lemma%unimportant case_prod_const: "(\(i, j). c) = (\_. c)" +lemma case_prod_const: "(\(i, j). c) = (\_. c)" by auto -subsubsection%unimportant \More about Function restricted by \<^const>\extensional\\ +subsubsection \More about Function restricted by \<^const>\extensional\\ definition "merge I J = (\(x, y) i. if i \ I then x i else if i \ J then y i else undefined)" @@ -116,42 +116,42 @@ definition%important prod_emb where "prod_emb I M K X = (\x. restrict x K) -` X \ (\\<^sub>E i\I. space (M i))" -lemma%important prod_emb_iff: +lemma prod_emb_iff: "f \ prod_emb I M K X \ f \ extensional I \ (restrict f K \ X) \ (\i\I. f i \ space (M i))" unfolding%unimportant prod_emb_def PiE_def by auto -lemma%unimportant +lemma shows prod_emb_empty[simp]: "prod_emb M L K {} = {}" and prod_emb_Un[simp]: "prod_emb M L K (A \ B) = prod_emb M L K A \ prod_emb M L K B" and prod_emb_Int: "prod_emb M L K (A \ B) = prod_emb M L K A \ prod_emb M L K B" and prod_emb_UN[simp]: "prod_emb M L K (\i\I. F i) = (\i\I. prod_emb M L K (F i))" and prod_emb_INT[simp]: "I \ {} \ prod_emb M L K (\i\I. F i) = (\i\I. prod_emb M L K (F i))" and prod_emb_Diff[simp]: "prod_emb M L K (A - B) = prod_emb M L K A - prod_emb M L K B" - by%unimportant (auto simp: prod_emb_def) + by (auto simp: prod_emb_def) -lemma%unimportant prod_emb_PiE: "J \ I \ (\i. i \ J \ E i \ space (M i)) \ +lemma prod_emb_PiE: "J \ I \ (\i. i \ J \ E i \ space (M i)) \ prod_emb I M J (\\<^sub>E i\J. E i) = (\\<^sub>E i\I. if i \ J then E i else space (M i))" by (force simp: prod_emb_def PiE_iff if_split_mem2) -lemma%unimportant prod_emb_PiE_same_index[simp]: +lemma prod_emb_PiE_same_index[simp]: "(\i. i \ I \ E i \ space (M i)) \ prod_emb I M I (Pi\<^sub>E I E) = Pi\<^sub>E I E" by (auto simp: prod_emb_def PiE_iff) -lemma%unimportant prod_emb_trans[simp]: +lemma prod_emb_trans[simp]: "J \ K \ K \ L \ prod_emb L M K (prod_emb K M J X) = prod_emb L M J X" by (auto simp add: Int_absorb1 prod_emb_def PiE_def) -lemma%unimportant prod_emb_Pi: +lemma prod_emb_Pi: assumes "X \ (\ j\J. sets (M j))" "J \ K" shows "prod_emb K M J (Pi\<^sub>E J X) = (\\<^sub>E i\K. if i \ J then X i else space (M i))" using assms sets.space_closed by (auto simp: prod_emb_def PiE_iff split: if_split_asm) blast+ -lemma%unimportant prod_emb_id: +lemma prod_emb_id: "B \ (\\<^sub>E i\L. space (M i)) \ prod_emb L M L B = B" by (auto simp: prod_emb_def subset_eq extensional_restrict) -lemma%unimportant prod_emb_mono: +lemma prod_emb_mono: "F \ G \ prod_emb A M B F \ prod_emb A M B G" by (auto simp: prod_emb_def) @@ -173,20 +173,20 @@ translations "\\<^sub>M x\I. M" == "CONST PiM I (%x. M)" -lemma%important extend_measure_cong: +lemma extend_measure_cong: assumes "\ = \'" "I = I'" "G = G'" "\i. i \ I' \ \ i = \' i" shows "extend_measure \ I G \ = extend_measure \' I' G' \'" - unfolding%unimportant extend_measure_def by (auto simp add: assms) + unfolding extend_measure_def by (auto simp add: assms) -lemma%unimportant Pi_cong_sets: +lemma Pi_cong_sets: "\I = J; \x. x \ I \ M x = N x\ \ Pi I M = Pi J N" unfolding Pi_def by auto -lemma%important PiM_cong: +lemma PiM_cong: assumes "I = J" "\x. x \ I \ M x = N x" shows "PiM I M = PiM J N" unfolding PiM_def -proof%unimportant (rule extend_measure_cong, goal_cases) +proof (rule extend_measure_cong, goal_cases) case 1 show ?case using assms by (subst assms(1), intro PiE_cong[of J "\i. space (M i)" "\i. space (N i)"]) simp_all @@ -206,14 +206,14 @@ qed -lemma%unimportant prod_algebra_sets_into_space: +lemma prod_algebra_sets_into_space: "prod_algebra I M \ Pow (\\<^sub>E i\I. space (M i))" by (auto simp: prod_emb_def prod_algebra_def) -lemma%important prod_algebra_eq_finite: +lemma prod_algebra_eq_finite: assumes I: "finite I" shows "prod_algebra I M = {(\\<^sub>E i\I. X i) |X. X \ (\ j\I. sets (M j))}" (is "?L = ?R") -proof%unimportant (intro iffI set_eqI) +proof (intro iffI set_eqI) fix A assume "A \ ?L" then obtain J E where J: "J \ {} \ I = {}" "finite J" "J \ I" "\i\J. E i \ sets (M i)" and A: "A = prod_emb I M J (\\<^sub>E j\J. E j)" @@ -232,32 +232,32 @@ by (auto simp: prod_algebra_def) qed -lemma%unimportant prod_algebraI: +lemma prod_algebraI: "finite J \ (J \ {} \ I = {}) \ J \ I \ (\i. i \ J \ E i \ sets (M i)) \ prod_emb I M J (\\<^sub>E j\J. E j) \ prod_algebra I M" by (auto simp: prod_algebra_def) -lemma%unimportant prod_algebraI_finite: +lemma prod_algebraI_finite: "finite I \ (\i\I. E i \ sets (M i)) \ (Pi\<^sub>E I E) \ prod_algebra I M" using prod_algebraI[of I I E M] prod_emb_PiE_same_index[of I E M, OF sets.sets_into_space] by simp -lemma%unimportant Int_stable_PiE: "Int_stable {Pi\<^sub>E J E | E. \i\I. E i \ sets (M i)}" +lemma Int_stable_PiE: "Int_stable {Pi\<^sub>E J E | E. \i\I. E i \ sets (M i)}" proof (safe intro!: Int_stableI) fix E F assume "\i\I. E i \ sets (M i)" "\i\I. F i \ sets (M i)" then show "\G. Pi\<^sub>E J E \ Pi\<^sub>E J F = Pi\<^sub>E J G \ (\i\I. G i \ sets (M i))" by (auto intro!: exI[of _ "\i. E i \ F i"] simp: PiE_Int) qed -lemma%unimportant prod_algebraE: +lemma prod_algebraE: assumes A: "A \ prod_algebra I M" obtains J E where "A = prod_emb I M J (\\<^sub>E j\J. E j)" "finite J" "J \ {} \ I = {}" "J \ I" "\i. i \ J \ E i \ sets (M i)" using A by (auto simp: prod_algebra_def) -lemma%important prod_algebraE_all: +lemma prod_algebraE_all: assumes A: "A \ prod_algebra I M" obtains E where "A = Pi\<^sub>E I E" "E \ (\ i\I. sets (M i))" -proof%unimportant - +proof - from A obtain E J where A: "A = prod_emb I M J (Pi\<^sub>E J E)" and J: "J \ I" and E: "E \ (\ i\J. sets (M i))" by (auto simp: prod_algebra_def) @@ -270,7 +270,7 @@ ultimately show ?thesis using that by auto qed -lemma%unimportant Int_stable_prod_algebra: "Int_stable (prod_algebra I M)" +lemma Int_stable_prod_algebra: "Int_stable (prod_algebra I M)" proof (unfold Int_stable_def, safe) fix A assume "A \ prod_algebra I M" from prod_algebraE[OF this] guess J E . note A = this @@ -291,11 +291,11 @@ finally show "A \ B \ prod_algebra I M" . qed -lemma%unimportant prod_algebra_mono: +proposition prod_algebra_mono: assumes space: "\i. i \ I \ space (E i) = space (F i)" assumes sets: "\i. i \ I \ sets (E i) \ sets (F i)" shows "prod_algebra I E \ prod_algebra I F" -proof%unimportant +proof fix A assume "A \ prod_algebra I E" then obtain J G where J: "J \ {} \ I = {}" "finite J" "J \ I" and A: "A = prod_emb I E J (\\<^sub>E i\J. G i)" @@ -315,18 +315,17 @@ apply auto done qed - -lemma%unimportant prod_algebra_cong: +proposition prod_algebra_cong: assumes "I = J" and sets: "(\i. i \ I \ sets (M i) = sets (N i))" shows "prod_algebra I M = prod_algebra J N" -proof%unimportant - +proof - have space: "\i. i \ I \ space (M i) = space (N i)" using sets_eq_imp_space_eq[OF sets] by auto with sets show ?thesis unfolding \I = J\ by (intro antisym prod_algebra_mono) auto qed -lemma%unimportant space_in_prod_algebra: +lemma space_in_prod_algebra: "(\\<^sub>E i\I. space (M i)) \ prod_algebra I M" proof cases assume "I = {}" then show ?thesis @@ -341,26 +340,26 @@ finally show ?thesis . qed -lemma%unimportant space_PiM: "space (\\<^sub>M i\I. M i) = (\\<^sub>E i\I. space (M i))" +lemma space_PiM: "space (\\<^sub>M i\I. M i) = (\\<^sub>E i\I. space (M i))" using prod_algebra_sets_into_space unfolding PiM_def prod_algebra_def by (intro space_extend_measure) simp -lemma%unimportant prod_emb_subset_PiM[simp]: "prod_emb I M K X \ space (PiM I M)" +lemma prod_emb_subset_PiM[simp]: "prod_emb I M K X \ space (PiM I M)" by (auto simp: prod_emb_def space_PiM) -lemma%unimportant space_PiM_empty_iff[simp]: "space (PiM I M) = {} \ (\i\I. space (M i) = {})" +lemma space_PiM_empty_iff[simp]: "space (PiM I M) = {} \ (\i\I. space (M i) = {})" by (auto simp: space_PiM PiE_eq_empty_iff) -lemma%unimportant undefined_in_PiM_empty[simp]: "(\x. undefined) \ space (PiM {} M)" +lemma undefined_in_PiM_empty[simp]: "(\x. undefined) \ space (PiM {} M)" by (auto simp: space_PiM) -lemma%unimportant sets_PiM: "sets (\\<^sub>M i\I. M i) = sigma_sets (\\<^sub>E i\I. space (M i)) (prod_algebra I M)" +lemma sets_PiM: "sets (\\<^sub>M i\I. M i) = sigma_sets (\\<^sub>E i\I. space (M i)) (prod_algebra I M)" using prod_algebra_sets_into_space unfolding PiM_def prod_algebra_def by (intro sets_extend_measure) simp -lemma%important sets_PiM_single: "sets (PiM I M) = +proposition sets_PiM_single: "sets (PiM I M) = sigma_sets (\\<^sub>E i\I. space (M i)) {{f\\\<^sub>E i\I. space (M i). f i \ A} | i A. i \ I \ A \ sets (M i)}" (is "_ = sigma_sets ?\ ?R") unfolding sets_PiM -proof%unimportant (rule sigma_sets_eqI) +proof (rule sigma_sets_eqI) interpret R: sigma_algebra ?\ "sigma_sets ?\ ?R" by (rule sigma_algebra_sigma_sets) auto fix A assume "A \ prod_algebra I M" from prod_algebraE[OF this] guess J X . note X = this @@ -388,7 +387,7 @@ finally show "A \ sigma_sets ?\ (prod_algebra I M)" . qed -lemma%unimportant sets_PiM_eq_proj: +lemma sets_PiM_eq_proj: "I \ {} \ sets (PiM I M) = sets (SUP i\I. vimage_algebra (\\<^sub>E i\I. space (M i)) (\x. x i) (M i))" apply (simp add: sets_PiM_single) apply (subst sets_Sup_eq[where X="\\<^sub>E i\I. space (M i)"]) @@ -400,18 +399,18 @@ apply (auto intro!: arg_cong2[where f=sigma_sets]) done -lemma%unimportant (*FIX ME needs name *) +lemma (*FIX ME needs name *) shows space_PiM_empty: "space (Pi\<^sub>M {} M) = {\k. undefined}" and sets_PiM_empty: "sets (Pi\<^sub>M {} M) = { {}, {\k. undefined} }" by (simp_all add: space_PiM sets_PiM_single image_constant sigma_sets_empty_eq) -lemma%important sets_PiM_sigma: +proposition sets_PiM_sigma: assumes \_cover: "\i. i \ I \ \S\E i. countable S \ \ i = \S" assumes E: "\i. i \ I \ E i \ Pow (\ i)" assumes J: "\j. j \ J \ finite j" "\J = I" defines "P \ {{f\(\\<^sub>E i\I. \ i). \i\j. f i \ A i} | A j. j \ J \ A \ Pi j E}" shows "sets (\\<^sub>M i\I. sigma (\ i) (E i)) = sets (sigma (\\<^sub>E i\I. \ i) P)" -proof%unimportant cases +proof cases assume "I = {}" with \\J = I\ have "P = {{\_. undefined}} \ P = {}" by (auto simp: P_def) @@ -495,21 +494,21 @@ finally show "?thesis" . qed -lemma%unimportant sets_PiM_in_sets: +lemma sets_PiM_in_sets: assumes space: "space N = (\\<^sub>E i\I. space (M i))" assumes sets: "\i A. i \ I \ A \ sets (M i) \ {x\space N. x i \ A} \ sets N" shows "sets (\\<^sub>M i \ I. M i) \ sets N" unfolding sets_PiM_single space[symmetric] by (intro sets.sigma_sets_subset subsetI) (auto intro: sets) -lemma%unimportant sets_PiM_cong[measurable_cong]: +lemma sets_PiM_cong[measurable_cong]: assumes "I = J" "\i. i \ J \ sets (M i) = sets (N i)" shows "sets (PiM I M) = sets (PiM J N)" using assms sets_eq_imp_space_eq[OF assms(2)] by (simp add: sets_PiM_single cong: PiE_cong conj_cong) -lemma%important sets_PiM_I: +lemma sets_PiM_I: assumes "finite J" "J \ I" "\i\J. E i \ sets (M i)" shows "prod_emb I M J (\\<^sub>E j\J. E j) \ sets (\\<^sub>M i\I. M i)" -proof%unimportant cases +proof cases assume "J = {}" then have "prod_emb I M J (\\<^sub>E j\J. E j) = (\\<^sub>E j\I. space (M j))" by (auto simp: prod_emb_def) @@ -520,7 +519,7 @@ by (force simp add: sets_PiM prod_algebra_def) qed -lemma%unimportant measurable_PiM: +proposition measurable_PiM: assumes space: "f \ space N \ (\\<^sub>E i\I. space (M i))" assumes sets: "\X J. J \ {} \ I = {} \ finite J \ J \ I \ (\i. i \ J \ X i \ sets (M i)) \ f -` prod_emb I M J (Pi\<^sub>E J X) \ space N \ sets N" @@ -532,13 +531,13 @@ with sets[of J X] show "f -` A \ space N \ sets N" by auto qed -lemma%important measurable_PiM_Collect: +lemma measurable_PiM_Collect: assumes space: "f \ space N \ (\\<^sub>E i\I. space (M i))" assumes sets: "\X J. J \ {} \ I = {} \ finite J \ J \ I \ (\i. i \ J \ X i \ sets (M i)) \ {\\space N. \i\J. f \ i \ X i} \ sets N" shows "f \ measurable N (PiM I M)" using sets_PiM prod_algebra_sets_into_space space -proof%unimportant (rule measurable_sigma_sets) +proof (rule measurable_sigma_sets) fix A assume "A \ prod_algebra I M" from prod_algebraE[OF this] guess J X . note X = this then have "f -` A \ space N = {\ \ space N. \i\J. f \ i \ X i}" @@ -547,7 +546,7 @@ finally show "f -` A \ space N \ sets N" . qed -lemma%unimportant measurable_PiM_single: +lemma measurable_PiM_single: assumes space: "f \ space N \ (\\<^sub>E i\I. space (M i))" assumes sets: "\A i. i \ I \ A \ sets (M i) \ {\ \ space N. f \ i \ A} \ sets N" shows "f \ measurable N (PiM I M)" @@ -561,11 +560,11 @@ finally show "f -` A \ space N \ sets N" . qed (auto simp: space) -lemma%important measurable_PiM_single': +lemma measurable_PiM_single': assumes f: "\i. i \ I \ f i \ measurable N (M i)" and "(\\ i. f i \) \ space N \ (\\<^sub>E i\I. space (M i))" shows "(\\ i. f i \) \ measurable N (Pi\<^sub>M I M)" -proof%unimportant (rule measurable_PiM_single) +proof (rule measurable_PiM_single) fix A i assume A: "i \ I" "A \ sets (M i)" then have "{\ \ space N. f i \ \ A} = f i -` A \ space N" by auto @@ -573,12 +572,12 @@ using A f by (auto intro!: measurable_sets) qed fact -lemma%unimportant sets_PiM_I_finite[measurable]: +lemma sets_PiM_I_finite[measurable]: assumes "finite I" and sets: "(\i. i \ I \ E i \ sets (M i))" shows "(\\<^sub>E j\I. E j) \ sets (\\<^sub>M i\I. M i)" using sets_PiM_I[of I I E M] sets.sets_into_space[OF sets] \finite I\ sets by auto -lemma%unimportant measurable_component_singleton[measurable (raw)]: +lemma measurable_component_singleton[measurable (raw)]: assumes "i \ I" shows "(\x. x i) \ measurable (Pi\<^sub>M I M) (M i)" proof (unfold measurable_def, intro CollectI conjI ballI) fix A assume "A \ sets (M i)" @@ -589,30 +588,30 @@ using \A \ sets (M i)\ \i \ I\ by (auto intro!: sets_PiM_I) qed (insert \i \ I\, auto simp: space_PiM) -lemma%unimportant measurable_component_singleton'[measurable_dest]: +lemma measurable_component_singleton'[measurable_dest]: assumes f: "f \ measurable N (Pi\<^sub>M I M)" assumes g: "g \ measurable L N" assumes i: "i \ I" shows "(\x. (f (g x)) i) \ measurable L (M i)" using measurable_compose[OF measurable_compose[OF g f] measurable_component_singleton, OF i] . -lemma%unimportant measurable_PiM_component_rev: +lemma measurable_PiM_component_rev: "i \ I \ f \ measurable (M i) N \ (\x. f (x i)) \ measurable (PiM I M) N" by simp -lemma%unimportant measurable_case_nat[measurable (raw)]: +lemma measurable_case_nat[measurable (raw)]: assumes [measurable (raw)]: "i = 0 \ f \ measurable M N" "\j. i = Suc j \ (\x. g x j) \ measurable M N" shows "(\x. case_nat (f x) (g x) i) \ measurable M N" by (cases i) simp_all -lemma%unimportant measurable_case_nat'[measurable (raw)]: +lemma measurable_case_nat'[measurable (raw)]: assumes fg[measurable]: "f \ measurable N M" "g \ measurable N (\\<^sub>M i\UNIV. M)" shows "(\x. case_nat (f x) (g x)) \ measurable N (\\<^sub>M i\UNIV. M)" using fg[THEN measurable_space] by (auto intro!: measurable_PiM_single' simp add: space_PiM PiE_iff split: nat.split) -lemma%unimportant measurable_add_dim[measurable]: +lemma measurable_add_dim[measurable]: "(\(f, y). f(i := y)) \ measurable (Pi\<^sub>M I M \\<^sub>M M i) (Pi\<^sub>M (insert i I) M)" (is "?f \ measurable ?P ?I") proof (rule measurable_PiM_single) @@ -626,12 +625,12 @@ finally show "{\ \ space ?P. case_prod (\f. fun_upd f i) \ j \ A} \ sets ?P" . qed (auto simp: space_pair_measure space_PiM PiE_def) -lemma%important measurable_fun_upd: +proposition measurable_fun_upd: assumes I: "I = J \ {i}" assumes f[measurable]: "f \ measurable N (PiM J M)" assumes h[measurable]: "h \ measurable N (M i)" shows "(\x. (f x) (i := h x)) \ measurable N (PiM I M)" -proof%unimportant (intro measurable_PiM_single') +proof (intro measurable_PiM_single') fix j assume "j \ I" then show "(\\. ((f \)(i := h \)) j) \ measurable N (M j)" unfolding I by (cases "j = i") auto next @@ -640,14 +639,14 @@ by (auto simp: space_PiM PiE_iff extensional_def) qed -lemma%unimportant measurable_component_update: +lemma measurable_component_update: "x \ space (Pi\<^sub>M I M) \ i \ I \ (\v. x(i := v)) \ measurable (M i) (Pi\<^sub>M (insert i I) M)" by simp -lemma%important measurable_merge[measurable]: +lemma measurable_merge[measurable]: "merge I J \ measurable (Pi\<^sub>M I M \\<^sub>M Pi\<^sub>M J M) (Pi\<^sub>M (I \ J) M)" (is "?f \ measurable ?P ?U") -proof%unimportant (rule measurable_PiM_single) +proof (rule measurable_PiM_single) fix i A assume A: "A \ sets (M i)" "i \ I \ J" then have "{\ \ space ?P. merge I J \ i \ A} = (if i \ I then ((\x. x i) \ fst) -` A \ space ?P else ((\x. x i) \ snd) -` A \ space ?P)" @@ -658,7 +657,7 @@ finally show "{\ \ space ?P. merge I J \ i \ A} \ sets ?P" . qed (auto simp: space_pair_measure space_PiM PiE_iff merge_def extensional_def) -lemma%unimportant measurable_restrict[measurable (raw)]: +lemma measurable_restrict[measurable (raw)]: assumes X: "\i. i \ I \ X i \ measurable N (M i)" shows "(\x. \i\I. X i x) \ measurable N (Pi\<^sub>M I M)" proof (rule measurable_PiM_single) @@ -669,14 +668,14 @@ using A X by (auto intro!: measurable_sets) qed (insert X, auto simp add: PiE_def dest: measurable_space) -lemma%unimportant measurable_abs_UNIV: +lemma measurable_abs_UNIV: "(\n. (\\. f n \) \ measurable M (N n)) \ (\\ n. f n \) \ measurable M (PiM UNIV N)" by (intro measurable_PiM_single) (auto dest: measurable_space) -lemma%unimportant measurable_restrict_subset: "J \ L \ (\f. restrict f J) \ measurable (Pi\<^sub>M L M) (Pi\<^sub>M J M)" +lemma measurable_restrict_subset: "J \ L \ (\f. restrict f J) \ measurable (Pi\<^sub>M L M) (Pi\<^sub>M J M)" by (intro measurable_restrict measurable_component_singleton) auto -lemma%unimportant measurable_restrict_subset': +lemma measurable_restrict_subset': assumes "J \ L" "\x. x \ J \ sets (M x) = sets (N x)" shows "(\f. restrict f J) \ measurable (Pi\<^sub>M L M) (Pi\<^sub>M J N)" proof- @@ -687,12 +686,12 @@ finally show ?thesis . qed -lemma%unimportant measurable_prod_emb[intro, simp]: +lemma measurable_prod_emb[intro, simp]: "J \ L \ X \ sets (Pi\<^sub>M J M) \ prod_emb L M J X \ sets (Pi\<^sub>M L M)" unfolding prod_emb_def space_PiM[symmetric] by (auto intro!: measurable_sets measurable_restrict measurable_component_singleton) -lemma%unimportant merge_in_prod_emb: +lemma merge_in_prod_emb: assumes "y \ space (PiM I M)" "x \ X" and X: "X \ sets (Pi\<^sub>M J M)" and "J \ I" shows "merge J I (x, y) \ prod_emb I M J X" using assms sets.sets_into_space[OF X] @@ -700,7 +699,7 @@ cong: if_cong restrict_cong) (simp add: extensional_def) -lemma%unimportant prod_emb_eq_emptyD: +lemma prod_emb_eq_emptyD: assumes J: "J \ I" and ne: "space (PiM I M) \ {}" and X: "X \ sets (Pi\<^sub>M J M)" and *: "prod_emb I M J X = {}" shows "X = {}" @@ -711,19 +710,19 @@ from merge_in_prod_emb[OF this \x\X\ X J] * show "x \ {}" by auto qed -lemma%unimportant sets_in_Pi_aux: +lemma sets_in_Pi_aux: "finite I \ (\j. j \ I \ {x\space (M j). x \ F j} \ sets (M j)) \ {x\space (PiM I M). x \ Pi I F} \ sets (PiM I M)" by (simp add: subset_eq Pi_iff) -lemma%unimportant sets_in_Pi[measurable (raw)]: +lemma sets_in_Pi[measurable (raw)]: "finite I \ f \ measurable N (PiM I M) \ (\j. j \ I \ {x\space (M j). x \ F j} \ sets (M j)) \ Measurable.pred N (\x. f x \ Pi I F)" unfolding pred_def by (rule measurable_sets_Collect[of f N "PiM I M", OF _ sets_in_Pi_aux]) auto -lemma%unimportant sets_in_extensional_aux: +lemma sets_in_extensional_aux: "{x\space (PiM I M). x \ extensional I} \ sets (PiM I M)" proof - have "{x\space (PiM I M). x \ extensional I} = space (PiM I M)" @@ -731,12 +730,12 @@ then show ?thesis by simp qed -lemma%unimportant sets_in_extensional[measurable (raw)]: +lemma sets_in_extensional[measurable (raw)]: "f \ measurable N (PiM I M) \ Measurable.pred N (\x. f x \ extensional I)" unfolding pred_def by (rule measurable_sets_Collect[of f N "PiM I M", OF _ sets_in_extensional_aux]) auto -lemma%unimportant sets_PiM_I_countable: +lemma sets_PiM_I_countable: assumes I: "countable I" and E: "\i. i \ I \ E i \ sets (M i)" shows "Pi\<^sub>E I E \ sets (Pi\<^sub>M I M)" proof cases assume "I \ {}" @@ -747,11 +746,11 @@ finally show ?thesis . qed (simp add: sets_PiM_empty) -lemma%important sets_PiM_D_countable: +lemma sets_PiM_D_countable: assumes A: "A \ PiM I M" shows "\J\I. \X\PiM J M. countable J \ A = prod_emb I M J X" using A[unfolded sets_PiM_single] -proof%unimportant induction +proof induction case (Basic A) then obtain i X where *: "i \ I" "X \ sets (M i)" and "A = {f \ \\<^sub>E i\I. space (M i). f i \ X}" by auto @@ -783,12 +782,12 @@ qed(auto intro: X) qed -lemma%important measure_eqI_PiM_finite: +proposition measure_eqI_PiM_finite: assumes [simp]: "finite I" "sets P = PiM I M" "sets Q = PiM I M" assumes eq: "\A. (\i. i \ I \ A i \ sets (M i)) \ P (Pi\<^sub>E I A) = Q (Pi\<^sub>E I A)" assumes A: "range A \ prod_algebra I M" "(\i. A i) = space (PiM I M)" "\i::nat. P (A i) \ \" shows "P = Q" -proof%unimportant (rule measure_eqI_generator_eq[OF Int_stable_prod_algebra prod_algebra_sets_into_space]) +proof (rule measure_eqI_generator_eq[OF Int_stable_prod_algebra prod_algebra_sets_into_space]) show "range A \ prod_algebra I M" "(\i. A i) = (\\<^sub>E i\I. space (M i))" "\i. P (A i) \ \" unfolding space_PiM[symmetric] by fact+ fix X assume "X \ prod_algebra I M" @@ -799,13 +798,13 @@ unfolding X by (subst (1 2) prod_emb_Pi) (auto simp: eq) qed (simp_all add: sets_PiM) -lemma%important measure_eqI_PiM_infinite: +proposition measure_eqI_PiM_infinite: assumes [simp]: "sets P = PiM I M" "sets Q = PiM I M" assumes eq: "\A J. finite J \ J \ I \ (\i. i \ J \ A i \ sets (M i)) \ P (prod_emb I M J (Pi\<^sub>E J A)) = Q (prod_emb I M J (Pi\<^sub>E J A))" assumes A: "finite_measure P" shows "P = Q" -proof%unimportant (rule measure_eqI_generator_eq[OF Int_stable_prod_algebra prod_algebra_sets_into_space]) +proof (rule measure_eqI_generator_eq[OF Int_stable_prod_algebra prod_algebra_sets_into_space]) interpret finite_measure P by fact define i where "i = (SOME i. i \ I)" have i: "I \ {} \ i \ I" @@ -839,12 +838,12 @@ fixes I :: "'i set" assumes finite_index: "finite I" -lemma%important (in finite_product_sigma_finite) sigma_finite_pairs: +proposition (in finite_product_sigma_finite) sigma_finite_pairs: "\F::'i \ nat \ 'a set. (\i\I. range (F i) \ sets (M i)) \ (\k. \i\I. emeasure (M i) (F i k) \ \) \ incseq (\k. \\<^sub>E i\I. F i k) \ (\k. \\<^sub>E i\I. F i k) = space (PiM I M)" -proof%unimportant - +proof - have "\i::'i. \F::nat \ 'a set. range F \ sets (M i) \ incseq F \ (\i. F i) = space (M i) \ (\k. emeasure (M i) (F k) \ \)" using M.sigma_finite_incseq by metis from choice[OF this] guess F :: "'i \ nat \ 'a set" .. @@ -870,7 +869,7 @@ qed qed -lemma%unimportant emeasure_PiM_empty[simp]: "emeasure (PiM {} M) {\_. undefined} = 1" +lemma emeasure_PiM_empty[simp]: "emeasure (PiM {} M) {\_. undefined} = 1" proof - let ?\ = "\A. if A = {} then 0 else (1::ennreal)" have "emeasure (Pi\<^sub>M {} M) (prod_emb {} M {} (\\<^sub>E i\{}. {})) = 1" @@ -887,12 +886,12 @@ by simp qed -lemma%unimportant PiM_empty: "PiM {} M = count_space {\_. undefined}" +lemma PiM_empty: "PiM {} M = count_space {\_. undefined}" by (rule measure_eqI) (auto simp add: sets_PiM_empty) -lemma%important (in product_sigma_finite) emeasure_PiM: +lemma (in product_sigma_finite) emeasure_PiM: "finite I \ (\i. i\I \ A i \ sets (M i)) \ emeasure (PiM I M) (Pi\<^sub>E I A) = (\i\I. emeasure (M i) (A i))" -proof%unimportant (induct I arbitrary: A rule: finite_induct) +proof (induct I arbitrary: A rule: finite_induct) case (insert i I) interpret finite_product_sigma_finite M I by standard fact have "finite (insert i I)" using \finite I\ by auto @@ -947,7 +946,7 @@ by (subst (asm) prod_emb_PiE_same_index) (auto intro!: sets.sets_into_space) qed simp -lemma%unimportant (in product_sigma_finite) PiM_eqI: +lemma (in product_sigma_finite) PiM_eqI: assumes I[simp]: "finite I" and P: "sets P = PiM I M" assumes eq: "\A. (\i. i \ I \ A i \ sets (M i)) \ P (Pi\<^sub>E I A) = (\i\I. emeasure (M i) (A i))" shows "P = PiM I M" @@ -965,7 +964,7 @@ qed qed -lemma%unimportant (in product_sigma_finite) sigma_finite: +lemma (in product_sigma_finite) sigma_finite: assumes "finite I" shows "sigma_finite_measure (PiM I M)" proof @@ -986,11 +985,11 @@ sublocale finite_product_sigma_finite \ sigma_finite_measure "Pi\<^sub>M I M" using sigma_finite[OF finite_index] . -lemma%unimportant (in finite_product_sigma_finite) measure_times: +lemma (in finite_product_sigma_finite) measure_times: "(\i. i \ I \ A i \ sets (M i)) \ emeasure (Pi\<^sub>M I M) (Pi\<^sub>E I A) = (\i\I. emeasure (M i) (A i))" using emeasure_PiM[OF finite_index] by auto -lemma%unimportant (in product_sigma_finite) nn_integral_empty: +lemma (in product_sigma_finite) nn_integral_empty: "0 \ f (\k. undefined) \ integral\<^sup>N (Pi\<^sub>M {} M) f = f (\k. undefined)" by (simp add: PiM_empty nn_integral_count_space_finite max.absorb2) @@ -998,7 +997,7 @@ assumes IJ[simp]: "I \ J = {}" and fin: "finite I" "finite J" shows "distr (Pi\<^sub>M I M \\<^sub>M Pi\<^sub>M J M) (Pi\<^sub>M (I \ J) M) (merge I J) = Pi\<^sub>M (I \ J) M" (is "?D = ?P") -proof%unimportant (rule PiM_eqI) +proof (rule PiM_eqI) interpret I: finite_product_sigma_finite M I by standard fact interpret J: finite_product_sigma_finite M J by standard fact fix A assume A: "\i. i \ I \ J \ A i \ sets (M i)" @@ -1010,12 +1009,12 @@ (auto simp: * J.emeasure_pair_measure_Times I.measure_times J.measure_times prod.union_disjoint) qed (insert fin, simp_all) -lemma%important (in product_sigma_finite) product_nn_integral_fold: +proposition (in product_sigma_finite) product_nn_integral_fold: assumes IJ: "I \ J = {}" "finite I" "finite J" and f[measurable]: "f \ borel_measurable (Pi\<^sub>M (I \ J) M)" shows "integral\<^sup>N (Pi\<^sub>M (I \ J) M) f = (\\<^sup>+ x. (\\<^sup>+ y. f (merge I J (x, y)) \(Pi\<^sub>M J M)) \(Pi\<^sub>M I M))" -proof%unimportant - +proof - interpret I: finite_product_sigma_finite M I by standard fact interpret J: finite_product_sigma_finite M J by standard fact interpret P: pair_sigma_finite "Pi\<^sub>M I M" "Pi\<^sub>M J M" by standard @@ -1030,7 +1029,7 @@ done qed -lemma%unimportant (in product_sigma_finite) distr_singleton: +lemma (in product_sigma_finite) distr_singleton: "distr (Pi\<^sub>M {i} M) (M i) (\x. x i) = M i" (is "?D = _") proof (intro measure_eqI[symmetric]) interpret I: finite_product_sigma_finite M "{i}" by standard simp @@ -1042,7 +1041,7 @@ by (simp add: emeasure_distr measurable_component_singleton) qed simp -lemma%unimportant (in product_sigma_finite) product_nn_integral_singleton: +lemma (in product_sigma_finite) product_nn_integral_singleton: assumes f: "f \ borel_measurable (M i)" shows "integral\<^sup>N (Pi\<^sub>M {i} M) (\x. f (x i)) = integral\<^sup>N (M i) f" proof - @@ -1054,11 +1053,11 @@ done qed -lemma%important (in product_sigma_finite) product_nn_integral_insert: +proposition (in product_sigma_finite) product_nn_integral_insert: assumes I[simp]: "finite I" "i \ I" and f: "f \ borel_measurable (Pi\<^sub>M (insert i I) M)" shows "integral\<^sup>N (Pi\<^sub>M (insert i I) M) f = (\\<^sup>+ x. (\\<^sup>+ y. f (x(i := y)) \(M i)) \(Pi\<^sub>M I M))" -proof%unimportant - +proof - interpret I: finite_product_sigma_finite M I by standard auto interpret i: finite_product_sigma_finite M "{i}" by standard auto have IJ: "I \ {i} = {}" and insert: "I \ {i} = insert i I" @@ -1078,7 +1077,7 @@ qed qed -lemma%unimportant (in product_sigma_finite) product_nn_integral_insert_rev: +lemma (in product_sigma_finite) product_nn_integral_insert_rev: assumes I[simp]: "finite I" "i \ I" and [measurable]: "f \ borel_measurable (Pi\<^sub>M (insert i I) M)" shows "integral\<^sup>N (Pi\<^sub>M (insert i I) M) f = (\\<^sup>+ y. (\\<^sup>+ x. f (x(i := y)) \(Pi\<^sub>M I M)) \(M i))" @@ -1089,7 +1088,7 @@ apply measurable done -lemma%unimportant (in product_sigma_finite) product_nn_integral_prod: +lemma (in product_sigma_finite) product_nn_integral_prod: assumes "finite I" "\i. i \ I \ f i \ borel_measurable (M i)" shows "(\\<^sup>+ x. (\i\I. f i (x i)) \Pi\<^sub>M I M) = (\i\I. integral\<^sup>N (M i) (f i))" using assms proof (induction I) @@ -1112,11 +1111,11 @@ done qed (simp add: space_PiM) -lemma%important (in product_sigma_finite) product_nn_integral_pair: +proposition (in product_sigma_finite) product_nn_integral_pair: assumes [measurable]: "case_prod f \ borel_measurable (M x \\<^sub>M M y)" assumes xy: "x \ y" shows "(\\<^sup>+\. f (\ x) (\ y) \PiM {x, y} M) = (\\<^sup>+z. f (fst z) (snd z) \(M x \\<^sub>M M y))" -proof%unimportant - +proof - interpret psm: pair_sigma_finite "M x" "M y" unfolding pair_sigma_finite_def using sigma_finite_measures by simp_all have "{x, y} = {y, x}" by auto @@ -1129,7 +1128,7 @@ finally show ?thesis . qed -lemma%unimportant (in product_sigma_finite) distr_component: +lemma (in product_sigma_finite) distr_component: "distr (M i) (Pi\<^sub>M {i} M) (\x. \i\{i}. x) = Pi\<^sub>M {i} M" (is "?D = ?P") proof (intro PiM_eqI) fix A assume A: "\ia. ia \ {i} \ A ia \ sets (M ia)" @@ -1139,7 +1138,7 @@ by (subst emeasure_distr) (auto intro!: sets_PiM_I_finite measurable_restrict) qed simp_all -lemma%unimportant (in product_sigma_finite) +lemma (in product_sigma_finite) assumes IJ: "I \ J = {}" "finite I" "finite J" and A: "A \ sets (Pi\<^sub>M (I \ J) M)" shows emeasure_fold_integral: "emeasure (Pi\<^sub>M (I \ J) M) A = (\\<^sup>+x. emeasure (Pi\<^sub>M J M) ((\y. merge I J (x, y)) -` A \ space (Pi\<^sub>M J M)) \Pi\<^sub>M I M)" (is ?I) @@ -1164,11 +1163,11 @@ by (simp add: vimage_comp comp_def space_pair_measure cong: measurable_cong) qed -lemma%unimportant sets_Collect_single: +lemma sets_Collect_single: "i \ I \ A \ sets (M i) \ { x \ space (Pi\<^sub>M I M). x i \ A } \ sets (Pi\<^sub>M I M)" by simp -lemma%unimportant pair_measure_eq_distr_PiM: +lemma pair_measure_eq_distr_PiM: fixes M1 :: "'a measure" and M2 :: "'a measure" assumes "sigma_finite_measure M1" "sigma_finite_measure M2" shows "(M1 \\<^sub>M M2) = distr (Pi\<^sub>M UNIV (case_bool M1 M2)) (M1 \\<^sub>M M2) (\x. (x True, x False))" @@ -1195,7 +1194,7 @@ by (subst emeasure_distr) (auto simp: measurable_pair_iff) qed simp -lemma%unimportant infprod_in_sets[intro]: +lemma infprod_in_sets[intro]: fixes E :: "nat \ 'a set" assumes E: "\i. E i \ sets (M i)" shows "Pi UNIV E \ sets (\\<^sub>M i\UNIV::nat set. M i)" proof - diff -r a03a63b81f44 -r a06b204527e6 src/HOL/Analysis/Function_Topology.thy --- a/src/HOL/Analysis/Function_Topology.thy Mon Jan 14 18:35:03 2019 +0000 +++ b/src/HOL/Analysis/Function_Topology.thy Wed Jan 16 21:27:33 2019 +0000 @@ -61,6 +61,8 @@ I realized afterwards that this theory has a lot in common with \<^file>\~~/src/HOL/Library/Finite_Map.thy\. \ + + subsection%important \Topology without type classes\ subsubsection%important \The topology generated by some (open) subsets\ @@ -78,14 +80,14 @@ | UN: "(\k. k \ K \ generate_topology_on S k) \ generate_topology_on S (\K)" | Basis: "s \ S \ generate_topology_on S s" -lemma%unimportant istopology_generate_topology_on: +lemma istopology_generate_topology_on: "istopology (generate_topology_on S)" unfolding istopology_def by (auto intro: generate_topology_on.intros) text \The basic property of the topology generated by a set \S\ is that it is the smallest topology containing all the elements of \S\:\ -lemma%unimportant generate_topology_on_coarsest: +lemma generate_topology_on_coarsest: assumes "istopology T" "\s. s \ S \ T s" "generate_topology_on S s0" @@ -96,17 +98,17 @@ abbreviation%unimportant topology_generated_by::"('a set set) \ ('a topology)" where "topology_generated_by S \ topology (generate_topology_on S)" -lemma%unimportant openin_topology_generated_by_iff: +lemma openin_topology_generated_by_iff: "openin (topology_generated_by S) s \ generate_topology_on S s" using topology_inverse'[OF istopology_generate_topology_on[of S]] by simp -lemma%unimportant openin_topology_generated_by: +lemma openin_topology_generated_by: "openin (topology_generated_by S) s \ generate_topology_on S s" using openin_topology_generated_by_iff by auto -lemma%important topology_generated_by_topspace: +lemma topology_generated_by_topspace: "topspace (topology_generated_by S) = (\S)" -proof%unimportant +proof { fix s assume "openin (topology_generated_by S) s" then have "generate_topology_on S s" by (rule openin_topology_generated_by) @@ -121,9 +123,9 @@ unfolding topspace_def using openin_topology_generated_by_iff by auto qed -lemma%important topology_generated_by_Basis: +lemma topology_generated_by_Basis: "s \ S \ openin (topology_generated_by S) s" -by%unimportant (simp only: openin_topology_generated_by_iff, auto simp: generate_topology_on.Basis) + by (simp only: openin_topology_generated_by_iff, auto simp: generate_topology_on.Basis) lemma generate_topology_on_Inter: "\finite \; \K. K \ \ \ generate_topology_on \ K; \ \ {}\ \ generate_topology_on \ (\\)" @@ -266,28 +268,28 @@ where "continuous_on_topo T1 T2 f = ((\ U. openin T2 U \ openin T1 (f-`U \ topspace(T1))) \ (f`(topspace T1) \ (topspace T2)))" -lemma%important continuous_on_continuous_on_topo: +lemma continuous_on_continuous_on_topo: "continuous_on s f \ continuous_on_topo (subtopology euclidean s) euclidean f" -unfolding%unimportant continuous_on_open_invariant openin_open vimage_def continuous_on_topo_def + unfolding continuous_on_open_invariant openin_open vimage_def continuous_on_topo_def topspace_euclidean_subtopology open_openin topspace_euclidean by fast -lemma%unimportant continuous_on_topo_UNIV: +lemma continuous_on_topo_UNIV: "continuous_on UNIV f \ continuous_on_topo euclidean euclidean f" using continuous_on_continuous_on_topo[of UNIV f] subtopology_UNIV[of euclidean] by auto -lemma%important continuous_on_topo_open [intro]: +lemma continuous_on_topo_open [intro]: "continuous_on_topo T1 T2 f \ openin T2 U \ openin T1 (f-`U \ topspace(T1))" -unfolding%unimportant continuous_on_topo_def by auto + unfolding continuous_on_topo_def by auto -lemma%unimportant continuous_on_topo_topspace [intro]: +lemma continuous_on_topo_topspace [intro]: "continuous_on_topo T1 T2 f \ f`(topspace T1) \ (topspace T2)" unfolding continuous_on_topo_def by auto -lemma%important continuous_on_generated_topo_iff: +lemma continuous_on_generated_topo_iff: "continuous_on_topo T1 (topology_generated_by S) f \ ((\U. U \ S \ openin T1 (f-`U \ topspace(T1))) \ (f`(topspace T1) \ (\ S)))" unfolding continuous_on_topo_def topology_generated_by_topspace -proof%unimportant (auto simp add: topology_generated_by_Basis) +proof (auto simp add: topology_generated_by_Basis) assume H: "\U. U \ S \ openin T1 (f -` U \ topspace T1)" fix U assume "openin (topology_generated_by S) U" then have "generate_topology_on S U" by (rule openin_topology_generated_by) @@ -309,17 +311,17 @@ qed (auto simp add: H) qed -lemma%important continuous_on_generated_topo: +lemma continuous_on_generated_topo: assumes "\U. U \S \ openin T1 (f-`U \ topspace(T1))" "f`(topspace T1) \ (\ S)" shows "continuous_on_topo T1 (topology_generated_by S) f" -using%unimportant assms continuous_on_generated_topo_iff by blast + using assms continuous_on_generated_topo_iff by blast -lemma%important continuous_on_topo_compose: +proposition continuous_on_topo_compose: assumes "continuous_on_topo T1 T2 f" "continuous_on_topo T2 T3 g" shows "continuous_on_topo T1 T3 (g o f)" -using%unimportant assms unfolding continuous_on_topo_def -proof%unimportant (auto) + using assms unfolding continuous_on_topo_def +proof (auto) fix U :: "'c set" assume H: "openin T3 U" have "openin T1 (f -` (g -` U \ topspace T2) \ topspace T1)" @@ -330,7 +332,7 @@ by simp qed (blast) -lemma%unimportant continuous_on_topo_preimage_topspace [intro]: +lemma continuous_on_topo_preimage_topspace [intro]: assumes "continuous_on_topo T1 T2 f" shows "f-`(topspace T2) \ topspace T1 = topspace T1" using assms unfolding continuous_on_topo_def by auto @@ -349,9 +351,9 @@ definition%important pullback_topology::"('a set) \ ('a \ 'b) \ ('b topology) \ ('a topology)" where "pullback_topology A f T = topology (\S. \U. openin T U \ S = f-`U \ A)" -lemma%important istopology_pullback_topology: +lemma istopology_pullback_topology: "istopology (\S. \U. openin T U \ S = f-`U \ A)" -unfolding%unimportant istopology_def proof (auto) + unfolding istopology_def proof (auto) fix K assume "\S\K. \U. openin T U \ S = f -` U \ A" then have "\U. \S\K. openin T (U S) \ S = f-`(U S) \ A" by (rule bchoice) @@ -362,19 +364,19 @@ then show "\V. openin T V \ \K = f -` V \ A" by auto qed -lemma%unimportant openin_pullback_topology: +lemma openin_pullback_topology: "openin (pullback_topology A f T) S \ (\U. openin T U \ S = f-`U \ A)" unfolding pullback_topology_def topology_inverse'[OF istopology_pullback_topology] by auto -lemma%unimportant topspace_pullback_topology: +lemma topspace_pullback_topology: "topspace (pullback_topology A f T) = f-`(topspace T) \ A" by (auto simp add: topspace_def openin_pullback_topology) -lemma%important continuous_on_topo_pullback [intro]: +proposition continuous_on_topo_pullback [intro]: assumes "continuous_on_topo T1 T2 g" shows "continuous_on_topo (pullback_topology A f T1) T2 (g o f)" unfolding continuous_on_topo_def -proof%unimportant (auto) +proof (auto) fix U::"'b set" assume "openin T2 U" then have "openin T1 (g-`U \ topspace T1)" using assms unfolding continuous_on_topo_def by auto @@ -394,11 +396,11 @@ using assms unfolding continuous_on_topo_def by auto qed -lemma%important continuous_on_topo_pullback' [intro]: +proposition continuous_on_topo_pullback' [intro]: assumes "continuous_on_topo T1 T2 (f o g)" "topspace T1 \ g-`A" shows "continuous_on_topo T1 (pullback_topology A f T2) g" unfolding continuous_on_topo_def -proof%unimportant (auto) +proof (auto) fix U assume "openin (pullback_topology A f T2) U" then have "\V. openin T2 V \ U = f-`V \ A" unfolding openin_pullback_topology by auto @@ -547,9 +549,9 @@ done qed -lemma%important topspace_product_topology: +lemma topspace_product_topology: "topspace (product_topology T I) = (\\<^sub>E i\I. topspace(T i))" -proof%unimportant +proof show "topspace (product_topology T I) \ (\\<^sub>E i\I. topspace (T i))" unfolding product_topology_def topology_generated_by_topspace unfolding topspace_def by auto @@ -559,16 +561,16 @@ unfolding product_topology_def using PiE_def by (auto simp add: topology_generated_by_topspace) qed -lemma%unimportant product_topology_basis: +lemma product_topology_basis: assumes "\i. openin (T i) (X i)" "finite {i. X i \ topspace (T i)}" shows "openin (product_topology T I) (\\<^sub>E i\I. X i)" unfolding product_topology_def by (rule topology_generated_by_Basis) (use assms in auto) -lemma%important product_topology_open_contains_basis: +proposition product_topology_open_contains_basis: assumes "openin (product_topology T I) U" "x \ U" shows "\X. x \ (\\<^sub>E i\I. X i) \ (\i. openin (T i) (X i)) \ finite {i. X i \ topspace (T i)} \ (\\<^sub>E i\I. X i) \ U" -proof%unimportant - +proof - have "generate_topology_on {(\\<^sub>E i\I. X i) |X. (\i. openin (T i) (X i)) \ finite {i. X i \ topspace (T i)}} U" using assms unfolding product_topology_def by (intro openin_topology_generated_by) auto then have "\x. x\U \ \X. x \ (\\<^sub>E i\I. X i) \ (\i. openin (T i) (X i)) \ finite {i. X i \ topspace (T i)} \ (\\<^sub>E i\I. X i) \ U" @@ -717,7 +719,7 @@ text \The basic property of the product topology is the continuity of projections:\ -lemma%unimportant continuous_on_topo_product_coordinates [simp]: +lemma continuous_on_topo_product_coordinates [simp]: assumes "i \ I" shows "continuous_on_topo (product_topology T I) (T i) (\x. x i)" proof - @@ -739,12 +741,12 @@ by (auto simp add: assms topspace_product_topology PiE_iff) qed -lemma%important continuous_on_topo_coordinatewise_then_product [intro]: +lemma continuous_on_topo_coordinatewise_then_product [intro]: assumes "\i. i \ I \ continuous_on_topo T1 (T i) (\x. f x i)" "\i x. i \ I \ x \ topspace T1 \ f x i = undefined" shows "continuous_on_topo T1 (product_topology T I) f" unfolding product_topology_def -proof%unimportant (rule continuous_on_generated_topo) +proof (rule continuous_on_generated_topo) fix U assume "U \ {Pi\<^sub>E I X |X. (\i. openin (T i) (X i)) \ finite {i. X i \ topspace (T i)}}" then obtain X where H: "U = Pi\<^sub>E I X" "\i. openin (T i) (X i)" "finite {i. X i \ topspace (T i)}" by blast @@ -772,7 +774,7 @@ using assms unfolding continuous_on_topo_def by auto qed -lemma%unimportant continuous_on_topo_product_then_coordinatewise [intro]: +lemma continuous_on_topo_product_then_coordinatewise [intro]: assumes "continuous_on_topo T1 (product_topology T I) f" shows "\i. i \ I \ continuous_on_topo T1 (T i) (\x. f x i)" "\i x. i \ I \ x \ topspace T1 \ f x i = undefined" @@ -794,7 +796,7 @@ using \i \ I\ by (auto simp add: PiE_iff extensional_def) qed -lemma%unimportant continuous_on_restrict: +lemma continuous_on_restrict: assumes "J \ I" shows "continuous_on_topo (product_topology T I) (product_topology T J) (\x. restrict x J)" proof (rule continuous_on_topo_coordinatewise_then_product) @@ -817,7 +819,7 @@ definition%important open_fun_def: "open U = openin (product_topology (\i. euclidean) UNIV) U" -instance proof%unimportant +instance proof have "topspace (product_topology (\(i::'a). euclidean::('b topology)) UNIV) = UNIV" unfolding topspace_product_topology topspace_euclidean by auto then show "open (UNIV::('a \ 'b) set)" @@ -826,15 +828,15 @@ end -lemma%unimportant euclidean_product_topology: +lemma euclidean_product_topology: "euclidean = product_topology (\i. euclidean::('b::topological_space) topology) UNIV" by (metis open_openin topology_eq open_fun_def) -lemma%important product_topology_basis': +proposition product_topology_basis': fixes x::"'i \ 'a" and U::"'i \ ('b::topological_space) set" assumes "finite I" "\i. i \ I \ open (U i)" shows "open {f. \i\I. f (x i) \ U i}" -proof%unimportant - +proof - define J where "J = x`I" define V where "V = (\y. if y \ J then \{U i|i. i\I \ x i = y} else UNIV)" define X where "X = (\y. if y \ J then V y else UNIV)" @@ -864,24 +866,24 @@ text \The results proved in the general situation of products of possibly different spaces have their counterparts in this simpler setting.\ -lemma%unimportant continuous_on_product_coordinates [simp]: +lemma continuous_on_product_coordinates [simp]: "continuous_on UNIV (\x. x i::('b::topological_space))" unfolding continuous_on_topo_UNIV euclidean_product_topology by (rule continuous_on_topo_product_coordinates, simp) -lemma%unimportant continuous_on_coordinatewise_then_product [intro, continuous_intros]: +lemma continuous_on_coordinatewise_then_product [intro, continuous_intros]: assumes "\i. continuous_on UNIV (\x. f x i)" shows "continuous_on UNIV f" using assms unfolding continuous_on_topo_UNIV euclidean_product_topology by (rule continuous_on_topo_coordinatewise_then_product, simp) -lemma%unimportant continuous_on_product_then_coordinatewise: +lemma continuous_on_product_then_coordinatewise: assumes "continuous_on UNIV f" shows "continuous_on UNIV (\x. f x i)" using assms unfolding continuous_on_topo_UNIV euclidean_product_topology by (rule continuous_on_topo_product_then_coordinatewise(1), simp) -lemma%unimportant continuous_on_product_coordinatewise_iff: +lemma continuous_on_product_coordinatewise_iff: "continuous_on UNIV f \ (\i. continuous_on UNIV (\x. f x i))" by (auto intro: continuous_on_product_then_coordinatewise) @@ -891,7 +893,7 @@ of product spaces, but they have more to do with countability and could be put in the corresponding theory.\ -lemma%unimportant countable_nat_product_event_const: +lemma countable_nat_product_event_const: fixes F::"'a set" and a::'a assumes "a \ F" "countable F" shows "countable {x::(nat \ 'a). (\i. x i \ F) \ finite {i. x i \ a}}" @@ -928,7 +930,7 @@ then show ?thesis using countable_subset[OF *] by auto qed -lemma%unimportant countable_product_event_const: +lemma countable_product_event_const: fixes F::"('a::countable) \ 'b set" and b::'b assumes "\i. countable (F i)" shows "countable {f::('a \ 'b). (\i. f i \ F i) \ (finite {i. f i \ b})}" @@ -961,7 +963,7 @@ qed instance "fun" :: (countable, first_countable_topology) first_countable_topology -proof%unimportant +proof fix x::"'a \ 'b" have "\A::('b \ nat \ 'b set). \x. (\i. x \ A x i \ open (A x i)) \ (\S. open S \ x \ S \ (\i. A x i \ S))" apply (rule choice) using first_countable_basis by auto @@ -1033,11 +1035,11 @@ using \countable K\ \\k. k \ K \ x \ k\ \\k. k \ K \ open k\ Inc by auto qed -lemma%important product_topology_countable_basis: +proposition product_topology_countable_basis: shows "\K::(('a::countable \ 'b::second_countable_topology) set set). topological_basis K \ countable K \ (\k\K. \X. (k = Pi\<^sub>E UNIV X) \ (\i. open (X i)) \ finite {i. X i \ UNIV})" -proof%unimportant - +proof - obtain B::"'b set set" where B: "countable B \ topological_basis B" using ex_countable_basis by auto then have "B \ {}" by (meson UNIV_I empty_iff open_UNIV topological_basisE) @@ -1140,15 +1142,15 @@ definition%important strong_operator_topology::"('a::real_normed_vector \\<^sub>L'b::real_normed_vector) topology" where "strong_operator_topology = pullback_topology UNIV blinfun_apply euclidean" -lemma%unimportant strong_operator_topology_topspace: +lemma strong_operator_topology_topspace: "topspace strong_operator_topology = UNIV" unfolding strong_operator_topology_def topspace_pullback_topology topspace_euclidean by auto -lemma%important strong_operator_topology_basis: +lemma strong_operator_topology_basis: fixes f::"('a::real_normed_vector \\<^sub>L'b::real_normed_vector)" and U::"'i \ 'b set" and x::"'i \ 'a" assumes "finite I" "\i. i \ I \ open (U i)" shows "openin strong_operator_topology {f. \i\I. blinfun_apply f (x i) \ U i}" -proof%unimportant - +proof - have "open {g::('a\'b). \i\I. g (x i) \ U i}" by (rule product_topology_basis'[OF assms]) moreover have "{f. \i\I. blinfun_apply f (x i) \ U i} @@ -1158,16 +1160,16 @@ unfolding strong_operator_topology_def open_openin apply (subst openin_pullback_topology) by auto qed -lemma%important strong_operator_topology_continuous_evaluation: +lemma strong_operator_topology_continuous_evaluation: "continuous_on_topo strong_operator_topology euclidean (\f. blinfun_apply f x)" -proof%unimportant - +proof - have "continuous_on_topo strong_operator_topology euclidean ((\f. f x) o blinfun_apply)" unfolding strong_operator_topology_def apply (rule continuous_on_topo_pullback) using continuous_on_topo_UNIV continuous_on_product_coordinates by fastforce then show ?thesis unfolding comp_def by simp qed -lemma%unimportant continuous_on_strong_operator_topo_iff_coordinatewise: +lemma continuous_on_strong_operator_topo_iff_coordinatewise: "continuous_on_topo T strong_operator_topology f \ (\x. continuous_on_topo T euclidean (\y. blinfun_apply (f y) x))" proof (auto) @@ -1190,9 +1192,9 @@ by (auto simp add: \continuous_on_topo T euclidean (blinfun_apply o f)\) qed -lemma%important strong_operator_topology_weaker_than_euclidean: +lemma strong_operator_topology_weaker_than_euclidean: "continuous_on_topo euclidean strong_operator_topology (\f. f)" -by%unimportant (subst continuous_on_strong_operator_topo_iff_coordinatewise, + by (subst continuous_on_strong_operator_topo_iff_coordinatewise, auto simp add: continuous_on_topo_UNIV[symmetric] linear_continuous_on) @@ -1226,9 +1228,9 @@ spaces. It would thus be desirable to hide them once the instance is proved, but I do not know how to do this.\ -lemma%important dist_fun_le_dist_first_terms: +lemma dist_fun_le_dist_first_terms: "dist x y \ 2 * Max {dist (x (from_nat n)) (y (from_nat n))|n. n \ N} + (1/2)^N" -proof%unimportant - +proof - have "(\n. (1 / 2) ^ (n+Suc N) * min (dist (x (from_nat (n+Suc N))) (y (from_nat (n+Suc N)))) 1) = (\n. (1 / 2) ^ (Suc N) * ((1/2) ^ n * min (dist (x (from_nat (n+Suc N))) (y (from_nat (n+Suc N)))) 1))" by (rule suminf_cong, simp add: power_add) @@ -1276,7 +1278,7 @@ finally show ?thesis unfolding M_def by simp qed -lemma%unimportant open_fun_contains_ball_aux: +lemma open_fun_contains_ball_aux: assumes "open (U::(('a \ 'b) set))" "x \ U" shows "\e>0. {y. dist x y < e} \ U" @@ -1339,7 +1341,7 @@ then show "\m>0. {y. dist x y < m} \ U" using * by blast qed -lemma%unimportant ball_fun_contains_open_aux: +lemma ball_fun_contains_open_aux: fixes x::"('a \ 'b)" and e::real assumes "e>0" shows "\U. open U \ x \ U \ U \ {y. dist x y < e}" @@ -1386,7 +1388,7 @@ ultimately show ?thesis by auto qed -lemma%unimportant fun_open_ball_aux: +lemma fun_open_ball_aux: fixes U::"('a \ 'b) set" shows "open U \ (\x\U. \e>0. \y. dist x y < e \ y \ U)" proof (auto) @@ -1575,7 +1577,7 @@ -subsection%important \Measurability\ (*FIX ME mv *) +subsection%important \Measurability\ (*FIX ME move? *) text \There are two natural sigma-algebras on a product space: the borel sigma algebra, generated by open sets in the product, and the product sigma algebra, countably generated by @@ -1593,11 +1595,11 @@ compare it with the product sigma algebra as explained above. \ -lemma%unimportant measurable_product_coordinates [measurable (raw)]: +lemma measurable_product_coordinates [measurable (raw)]: "(\x. x i) \ measurable borel borel" by (rule borel_measurable_continuous_on1[OF continuous_on_product_coordinates]) -lemma%unimportant measurable_product_then_coordinatewise: +lemma measurable_product_then_coordinatewise: fixes f::"'a \ 'b \ ('c::topological_space)" assumes [measurable]: "f \ borel_measurable M" shows "(\x. f x i) \ borel_measurable M" @@ -1611,10 +1613,10 @@ of the product sigma algebra that is more similar to the one we used above for the product topology.\ -lemma%important sets_PiM_finite: +lemma sets_PiM_finite: "sets (Pi\<^sub>M I M) = sigma_sets (\\<^sub>E i\I. space (M i)) {(\\<^sub>E i\I. X i) |X. (\i. X i \ sets (M i)) \ finite {i. X i \ space (M i)}}" -proof%unimportant +proof have "{(\\<^sub>E i\I. X i) |X. (\i. X i \ sets (M i)) \ finite {i. X i \ space (M i)}} \ sets (Pi\<^sub>M I M)" proof (auto) fix X assume H: "\i. X i \ sets (M i)" "finite {i. X i \ space (M i)}" @@ -1654,9 +1656,9 @@ done qed -lemma%important sets_PiM_subset_borel: +lemma sets_PiM_subset_borel: "sets (Pi\<^sub>M UNIV (\_. borel)) \ sets borel" -proof%unimportant - +proof - have *: "Pi\<^sub>E UNIV X \ sets borel" if [measurable]: "\i. X i \ sets borel" "finite {i. X i \ UNIV}" for X::"'a \ 'b set" proof - define I where "I = {i. X i \ UNIV}" @@ -1673,9 +1675,9 @@ by (simp add: * sets.sigma_sets_subset') qed -lemma%important sets_PiM_equal_borel: +proposition sets_PiM_equal_borel: "sets (Pi\<^sub>M UNIV (\i::('a::countable). borel::('b::second_countable_topology measure))) = sets borel" -proof%unimportant +proof obtain K::"('a \ 'b) set set" where K: "topological_basis K" "countable K" "\k. k \ K \ \X. (k = Pi\<^sub>E UNIV X) \ (\i. open (X i)) \ finite {i. X i \ UNIV}" using product_topology_countable_basis by fast @@ -1700,11 +1702,11 @@ unfolding borel_def by auto qed (simp add: sets_PiM_subset_borel) -lemma%important measurable_coordinatewise_then_product: +lemma measurable_coordinatewise_then_product: fixes f::"'a \ ('b::countable) \ ('c::second_countable_topology)" assumes [measurable]: "\i. (\x. f x i) \ borel_measurable M" shows "f \ borel_measurable M" -proof%unimportant - +proof - have "f \ measurable M (Pi\<^sub>M UNIV (\_. borel))" by (rule measurable_PiM_single', auto simp add: assms) then show ?thesis using sets_PiM_equal_borel measurable_cong_sets by blast diff -r a03a63b81f44 -r a06b204527e6 src/HOL/Analysis/Henstock_Kurzweil_Integration.thy --- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Mon Jan 14 18:35:03 2019 +0000 +++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Wed Jan 16 21:27:33 2019 +0000 @@ -7489,7 +7489,7 @@ fixes f :: "'n::euclidean_space \ real^'m" assumes "f integrable_on s" shows "integral s (\x. f x $ k) = integral s f $ k" - using integral_linear[OF assms(1) bounded_linear_component_cart,unfolded o_def] . + using integral_linear[OF assms(1) bounded_linear_vec_nth,unfolded o_def] . lemma content_closed_interval: fixes a :: "'a::ordered_euclidean_space" diff -r a03a63b81f44 -r a06b204527e6 src/HOL/Analysis/Tagged_Division.thy --- a/src/HOL/Analysis/Tagged_Division.thy Mon Jan 14 18:35:03 2019 +0000 +++ b/src/HOL/Analysis/Tagged_Division.thy Wed Jan 16 21:27:33 2019 +0000 @@ -32,7 +32,7 @@ subsection%unimportant \Sundries\ -(*FIXME restructure this entire section consists of single lemma *) + text\A transitive relation is well-founded if all initial segments are finite.\ lemma wf_finite_segments: @@ -55,7 +55,7 @@ by (simp add: field_simps) qed -subsection%unimportant \Some useful lemmas about intervals\ +subsection%important \Some useful lemmas about intervals\ lemma interior_subset_union_intervals: assumes "i = cbox a b" @@ -152,22 +152,22 @@ lemmas interval_bounds = interval_upperbound interval_lowerbound -lemma%important +lemma fixes X::"real set" shows interval_upperbound_real[simp]: "interval_upperbound X = Sup X" and interval_lowerbound_real[simp]: "interval_lowerbound X = Inf X" - by%unimportant (auto simp: interval_upperbound_def interval_lowerbound_def) + by (auto simp: interval_upperbound_def interval_lowerbound_def) -lemma%important interval_bounds'[simp]: +lemma interval_bounds'[simp]: assumes "cbox a b \ {}" shows "interval_upperbound (cbox a b) = b" and "interval_lowerbound (cbox a b) = a" - using%unimportant assms unfolding box_ne_empty by auto + using assms unfolding box_ne_empty by auto -lemma%important interval_upperbound_Times: +lemma interval_upperbound_Times: assumes "A \ {}" and "B \ {}" shows "interval_upperbound (A \ B) = (interval_upperbound A, interval_upperbound B)" -proof%unimportant- +proof- from assms have fst_image_times': "A = fst ` (A \ B)" by simp have "(\i\Basis. (SUP x\A \ B. x \ (i, 0)) *\<^sub>R i) = (\i\Basis. (SUP x\A. x \ i) *\<^sub>R i)" by (subst (2) fst_image_times') (simp del: fst_image_times add: o_def inner_Pair_0) @@ -178,10 +178,10 @@ by (subst sum_Basis_prod_eq) (auto simp add: sum_prod) qed -lemma%important interval_lowerbound_Times: +lemma interval_lowerbound_Times: assumes "A \ {}" and "B \ {}" shows "interval_lowerbound (A \ B) = (interval_lowerbound A, interval_lowerbound B)" -proof%unimportant- +proof- from assms have fst_image_times': "A = fst ` (A \ B)" by simp have "(\i\Basis. (INF x\A \ B. x \ (i, 0)) *\<^sub>R i) = (\i\Basis. (INF x\A. x \ i) *\<^sub>R i)" by (subst (2) fst_image_times') (simp del: fst_image_times add: o_def inner_Pair_0) @@ -226,11 +226,11 @@ using equation_minus_iff by (auto simp: gauge_def surj_def intro!: open_surjective_linear_image linear_uminus) -lemma%important gauge_Inter: +lemma gauge_Inter: assumes "finite S" and "\u. u\S \ gauge (f u)" shows "gauge (\x. \{f u x | u. u \ S})" -proof%unimportant - +proof - have *: "\x. {f u x |u. u \ S} = (\u. f u x) ` S" by auto show ?thesis @@ -238,12 +238,12 @@ using assms unfolding Ball_def Inter_iff mem_Collect_eq gauge_def by auto qed -lemma%important gauge_existence_lemma: +lemma gauge_existence_lemma: "(\x. \d :: real. p x \ 0 < d \ q d x) \ (\x. \d>0. p x \ q d x)" - by%unimportant (metis zero_less_one) + by (metis zero_less_one) -subsection%unimportant \Attempt a systematic general set of "offset" results for components\ -(*FIXME Restructure *) +subsection%important \Attempt a systematic general set of "offset" results for components\ +(*FIXME Restructure, the subsection consists only of 1 lemma *) lemma gauge_modify: assumes "(\S. open S \ open {x. f(x) \ S})" "gauge d" shows "gauge (\x. {y. f y \ d (f x)})" @@ -605,10 +605,10 @@ qed qed -proposition%important partial_division_extend_interval: +proposition partial_division_extend_interval: assumes "p division_of (\p)" "(\p) \ cbox a b" obtains q where "p \ q" "q division_of cbox a (b::'a::euclidean_space)" -proof%unimportant (cases "p = {}") +proof (cases "p = {}") case True obtain q where "q division_of (cbox a b)" by (rule elementary_interval) @@ -687,11 +687,11 @@ "p division_of S \ \a b. S \ cbox a (b::'a::euclidean_space)" by (meson bounded_subset_cbox_symmetric elementary_bounded) -lemma%important division_union_intervals_exists: +proposition division_union_intervals_exists: fixes a b :: "'a::euclidean_space" assumes "cbox a b \ {}" obtains p where "(insert (cbox a b) p) division_of (cbox a b \ cbox c d)" -proof%unimportant (cases "cbox c d = {}") +proof (cases "cbox c d = {}") case True with assms that show ?thesis by force next @@ -739,11 +739,11 @@ shows "\f division_of \\f" using assms by (auto intro!: division_ofI) -lemma%important elementary_union_interval: +lemma elementary_union_interval: fixes a b :: "'a::euclidean_space" assumes "p division_of \p" obtains q where "q division_of (cbox a b \ \p)" -proof%unimportant (cases "p = {} \ cbox a b = {}") +proof (cases "p = {} \ cbox a b = {}") case True obtain p where "p division_of (cbox a b)" by (rule elementary_interval) @@ -855,11 +855,11 @@ using that by auto qed -lemma%important elementary_union: +lemma elementary_union: fixes S T :: "'a::euclidean_space set" assumes "ps division_of S" "pt division_of T" obtains p where "p division_of (S \ T)" -proof%unimportant - +proof - have *: "S \ T = \ps \ \pt" using assms unfolding division_of_def by auto show ?thesis @@ -868,13 +868,13 @@ by (simp add: * that) qed -lemma%important partial_division_extend: +lemma partial_division_extend: fixes T :: "'a::euclidean_space set" assumes "p division_of S" and "q division_of T" and "S \ T" obtains r where "p \ r" and "r division_of T" -proof%unimportant - +proof - note divp = division_ofD[OF assms(1)] and divq = division_ofD[OF assms(2)] obtain a b where ab: "T \ cbox a b" using elementary_subset_cbox[OF assms(2)] by auto @@ -931,7 +931,7 @@ qed -lemma%important division_split: +lemma division_split: fixes a :: "'a::euclidean_space" assumes "p division_of (cbox a b)" and k: "k\Basis" @@ -939,7 +939,7 @@ (is "?p1 division_of ?I1") and "{l \ {x. x\k \ c} | l. l \ p \ l \ {x. x\k \ c} \ {}} division_of (cbox a b \ {x. x\k \ c})" (is "?p2 division_of ?I2") -proof%unimportant (rule_tac[!] division_ofI) +proof (rule_tac[!] division_ofI) note p = division_ofD[OF assms(1)] show "finite ?p1" "finite ?p2" using p(1) by auto @@ -1020,14 +1020,14 @@ lemma tagged_division_of_finite: "s tagged_division_of i \ finite s" unfolding tagged_division_of_def tagged_partial_division_of_def by auto -lemma%important tagged_division_of: +lemma tagged_division_of: "s tagged_division_of i \ finite s \ (\x K. (x, K) \ s \ x \ K \ K \ i \ (\a b. K = cbox a b)) \ (\x1 K1 x2 K2. (x1, K1) \ s \ (x2, K2) \ s \ (x1, K1) \ (x2, K2) \ interior K1 \ interior K2 = {}) \ (\{K. \x. (x,K) \ s} = i)" - unfolding%unimportant tagged_division_of_def tagged_partial_division_of_def by auto + unfolding tagged_division_of_def tagged_partial_division_of_def by auto lemma tagged_division_ofI: assumes "finite s" @@ -1052,10 +1052,10 @@ and "(\{K. \x. (x,K) \ s} = i)" using assms unfolding tagged_division_of by blast+ -lemma%important division_of_tagged_division: +lemma division_of_tagged_division: assumes "s tagged_division_of i" shows "(snd ` s) division_of i" -proof%unimportant (rule division_ofI) +proof (rule division_ofI) note assm = tagged_division_ofD[OF assms] show "\(snd ` s) = i" "finite (snd ` s)" using assm by auto @@ -1073,10 +1073,10 @@ using assm(5) k'(2) xk by blast qed -lemma%important partial_division_of_tagged_division: +lemma partial_division_of_tagged_division: assumes "s tagged_partial_division_of i" shows "(snd ` s) division_of \(snd ` s)" -proof%unimportant (rule division_ofI) +proof (rule division_ofI) note assm = tagged_partial_division_ofD[OF assms] show "finite (snd ` s)" "\(snd ` s) = \(snd ` s)" using assm by auto @@ -1121,12 +1121,12 @@ unfolding box_real[symmetric] by (rule tagged_division_of_self) -lemma%important tagged_division_Un: +lemma tagged_division_Un: assumes "p1 tagged_division_of s1" and "p2 tagged_division_of s2" and "interior s1 \ interior s2 = {}" shows "(p1 \ p2) tagged_division_of (s1 \ s2)" -proof%unimportant (rule tagged_division_ofI) +proof (rule tagged_division_ofI) note p1 = tagged_division_ofD[OF assms(1)] note p2 = tagged_division_ofD[OF assms(2)] show "finite (p1 \ p2)" @@ -1149,12 +1149,12 @@ by (metis "*" UnE assms(1) assms(2) inf_sup_aci(1) p2(5) tagged_division_ofD(3) xk xk'(1) xk'(2)) qed -lemma%important tagged_division_Union: +lemma tagged_division_Union: assumes "finite I" and tag: "\i. i\I \ pfn i tagged_division_of i" and disj: "\i1 i2. \i1 \ I; i2 \ I; i1 \ i2\ \ interior(i1) \ interior(i2) = {}" shows "\(pfn ` I) tagged_division_of (\I)" -proof%unimportant (rule tagged_division_ofI) +proof (rule tagged_division_ofI) note assm = tagged_division_ofD[OF tag] show "finite (\(pfn ` I))" using assms by auto @@ -1229,13 +1229,13 @@ unfolding box_real[symmetric] by (rule tagged_division_Un_interval) -lemma%important tagged_division_split_left_inj: +lemma tagged_division_split_left_inj: assumes d: "d tagged_division_of i" and tags: "(x1, K1) \ d" "(x2, K2) \ d" and "K1 \ K2" and eq: "K1 \ {x. x \ k \ c} = K2 \ {x. x \ k \ c}" shows "interior (K1 \ {x. x\k \ c}) = {}" -proof%unimportant - +proof - have "interior (K1 \ K2) = {} \ (x2, K2) = (x1, K1)" using tags d by (metis (no_types) interior_Int tagged_division_ofD(5)) then show ?thesis @@ -1255,11 +1255,11 @@ using eq \K1 \ K2\ by (metis (no_types) inf_assoc inf_bot_left inf_left_idem interior_Int old.prod.inject) qed -lemma%important (in comm_monoid_set) over_tagged_division_lemma: +lemma (in comm_monoid_set) over_tagged_division_lemma: assumes "p tagged_division_of i" and "\u v. box u v = {} \ d (cbox u v) = \<^bold>1" shows "F (\(_, k). d k) p = F d (snd ` p)" -proof%unimportant - +proof - have *: "(\(_ ,k). d k) = d \ snd" by (simp add: fun_eq_iff) note assm = tagged_division_ofD[OF assms(1)] @@ -1293,7 +1293,7 @@ \<^typ>\bool\.\ paragraph%important \Using additivity of lifted function to encode definedness.\ -text%important \%whitespace\ +text \%whitespace\ definition%important lift_option :: "('a \ 'b \ 'c) \ 'a option \ 'b option \ 'c option" where "lift_option f a' b' = Option.bind a' (\a. Option.bind b' (\b. Some (f a b)))" @@ -1307,7 +1307,7 @@ lemma%important comm_monoid_lift_option: assumes "comm_monoid f z" shows "comm_monoid (lift_option f) (Some z)" -proof%unimportant - +proof - from assms interpret comm_monoid f z . show ?thesis by standard (auto simp: lift_option_def ac_simps split: bind_split) @@ -1334,16 +1334,16 @@ paragraph \Division points\ -text%important \%whitespace\ +text \%whitespace\ definition%important "division_points (k::('a::euclidean_space) set) d = {(j,x). j \ Basis \ (interval_lowerbound k)\j < x \ x < (interval_upperbound k)\j \ (\i\d. (interval_lowerbound i)\j = x \ (interval_upperbound i)\j = x)}" -lemma%important division_points_finite: +lemma division_points_finite: fixes i :: "'a::euclidean_space set" assumes "d division_of i" shows "finite (division_points i d)" -proof%unimportant - +proof - note assm = division_ofD[OF assms] let ?M = "\j. {(j,x)|x. (interval_lowerbound i)\j < x \ x < (interval_upperbound i)\j \ (\i\d. (interval_lowerbound i)\j = x \ (interval_upperbound i)\j = x)}" @@ -1353,7 +1353,7 @@ unfolding * using assm by auto qed -lemma%important division_points_subset: +lemma division_points_subset: fixes a :: "'a::euclidean_space" assumes "d division_of (cbox a b)" and "\i\Basis. a\i < b\i" "a\k < c" "c < b\k" @@ -1362,7 +1362,7 @@ division_points (cbox a b) d" (is ?t1) and "division_points (cbox a b \ {x. x\k \ c}) {l \ {x. x\k \ c} | l . l \ d \ \(l \ {x. x\k \ c} = {})} \ division_points (cbox a b) d" (is ?t2) -proof%unimportant - +proof - note assm = division_ofD[OF assms(1)] have *: "\i\Basis. a\i \ b\i" "\i\Basis. a\i \ (\i\Basis. (if i = k then min (b \ k) c else b \ i) *\<^sub>R i) \ i" @@ -1423,7 +1423,7 @@ by force qed -lemma%important division_points_psubset: +lemma division_points_psubset: fixes a :: "'a::euclidean_space" assumes d: "d division_of (cbox a b)" and altb: "\i\Basis. a\i < b\i" "a\k < c" "c < b\k" @@ -1434,7 +1434,7 @@ division_points (cbox a b) d" (is "?D1 \ ?D") and "division_points (cbox a b \ {x. x\k \ c}) {l \ {x. x\k \ c} | l. l\d \ l \ {x. x\k \ c} \ {}} \ division_points (cbox a b) d" (is "?D2 \ ?D") -proof%unimportant - +proof - have ab: "\i\Basis. a\i \ b\i" using altb by (auto intro!:less_imp_le) obtain u v where l: "l = cbox u v" @@ -1485,13 +1485,13 @@ using \K1 \ \\ \K1 \ K2\ by auto qed -lemma%important division_split_right_inj: +lemma division_split_right_inj: fixes S :: "'a::euclidean_space set" assumes div: "\ division_of S" and eq: "K1 \ {x::'a. x\k \ c} = K2 \ {x. x\k \ c}" and "K1 \ \" "K2 \ \" "K1 \ K2" shows "interior (K1 \ {x. x\k \ c}) = {}" -proof%unimportant - +proof - have "interior K2 \ interior {a. a \ k \ c} = interior K1 \ interior {a. a \ k \ c}" by (metis (no_types) eq interior_Int) moreover have "\A. interior A \ interior K2 = {} \ A = K2 \ A \ \" @@ -1515,13 +1515,13 @@ unfolding * ** interval_split[OF assms] by (rule refl) qed -lemma%important division_doublesplit: +lemma division_doublesplit: fixes a :: "'a::euclidean_space" assumes "p division_of (cbox a b)" and k: "k \ Basis" shows "(\l. l \ {x. \x\k - c\ \ e}) ` {l\p. l \ {x. \x\k - c\ \ e} \ {}} division_of (cbox a b \ {x. \x\k - c\ \ e})" -proof%unimportant - +proof - have *: "\x c. \x - c\ \ e \ x \ c - e \ x \ c + e" by auto have **: "\p q p' q'. p division_of q \ p = p' \ q = q' \ p' division_of q'" @@ -1560,9 +1560,9 @@ using box_empty_imp [of One "-One"] by simp qed -lemma%important division: +lemma division: "F g d = g (cbox a b)" if "d division_of (cbox a b)" -proof%unimportant - +proof - define C where [abs_def]: "C = card (division_points (cbox a b) d)" then show ?thesis using that proof (induction C arbitrary: a b d rule: less_induct) @@ -1747,10 +1747,10 @@ qed qed -lemma%important tagged_division: +proposition tagged_division: assumes "d tagged_division_of (cbox a b)" shows "F (\(_, l). g l) d = g (cbox a b)" -proof%unimportant - +proof - have "F (\(_, k). g k) d = F g (snd ` d)" using assms box_empty_imp by (rule over_tagged_division_lemma) then show ?thesis @@ -1830,12 +1830,12 @@ subsection%important \Special case of additivity we need for the FTC\ (*fix add explanation here *) -lemma%important additive_tagged_division_1: +lemma additive_tagged_division_1: fixes f :: "real \ 'a::real_normed_vector" assumes "a \ b" and "p tagged_division_of {a..b}" shows "sum (\(x,k). f(Sup k) - f(Inf k)) p = f b - f a" -proof%unimportant - +proof - let ?f = "(\k::(real) set. if k = {} then 0 else f(interval_upperbound k) - f(interval_lowerbound k))" interpret operative_real plus 0 ?f rewrites "comm_monoid_set.F (+) 0 = sum" @@ -1881,21 +1881,21 @@ lemma fine_Un: "d fine p1 \ d fine p2 \ d fine (p1 \ p2)" unfolding fine_def by blast -lemma%important fine_Union: "(\p. p \ ps \ d fine p) \ d fine (\ps)" +lemma fine_Union: "(\p. p \ ps \ d fine p) \ d fine (\ps)" unfolding fine_def by auto -lemma%unimportant fine_subset: "p \ q \ d fine q \ d fine p" +lemma fine_subset: "p \ q \ d fine q \ d fine p" unfolding fine_def by blast subsection%important \Some basic combining lemmas\ -lemma%important tagged_division_Union_exists: +lemma tagged_division_Union_exists: assumes "finite I" and "\i\I. \p. p tagged_division_of i \ d fine p" and "\i1\I. \i2\I. i1 \ i2 \ interior i1 \ interior i2 = {}" and "\I = i" obtains p where "p tagged_division_of i" and "d fine p" -proof%unimportant - +proof - obtain pfn where pfn: "\x. x \ I \ pfn x tagged_division_of x" "\x. x \ I \ d fine pfn x" @@ -1913,17 +1913,17 @@ fixes i :: "'n::euclidean_space set" shows "s division_of i \ closed i" unfolding division_of_def by fastforce - +(* FIXME structure here, do not have one lemma in each subsection *) subsection%important \General bisection principle for intervals; might be useful elsewhere\ - -lemma%important interval_bisection_step: +(* FIXME move? *) +lemma interval_bisection_step: fixes type :: "'a::euclidean_space" assumes emp: "P {}" and Un: "\S T. \P S; P T; interior(S) \ interior(T) = {}\ \ P (S \ T)" and non: "\ P (cbox a (b::'a))" obtains c d where "\ P (cbox c d)" and "\i. i \ Basis \ a\i \ c\i \ c\i \ d\i \ d\i \ b\i \ 2 * (d\i - c\i) \ b\i - a\i" -proof%unimportant - +proof - have "cbox a b \ {}" using emp non by metis then have ab: "\i. i\Basis \ a \ i \ b \ i" @@ -2029,14 +2029,14 @@ by (metis (no_types, lifting) assms(3) that) qed -lemma%important interval_bisection: +lemma interval_bisection: fixes type :: "'a::euclidean_space" assumes "P {}" and Un: "\S T. \P S; P T; interior(S) \ interior(T) = {}\ \ P (S \ T)" and "\ P (cbox a (b::'a))" obtains x where "x \ cbox a b" and "\e>0. \c d. x \ cbox c d \ cbox c d \ ball x e \ cbox c d \ cbox a b \ \ P (cbox c d)" -proof%unimportant - +proof - have "\x. \y. \ P (cbox (fst x) (snd x)) \ (\ P (cbox (fst y) (snd y)) \ (\i\Basis. fst x\i \ fst y\i \ fst y\i \ snd y\i \ snd y\i \ snd x\i \ 2 * (snd y\i - fst y\i) \ snd x\i - fst x\i))" (is "\x. ?P x") @@ -2182,11 +2182,11 @@ subsection%important \Cousin's lemma\ -lemma%important fine_division_exists: +lemma fine_division_exists: (*FIXME rename(?) *) fixes a b :: "'a::euclidean_space" assumes "gauge g" obtains p where "p tagged_division_of (cbox a b)" "g fine p" -proof%unimportant (cases "\p. p tagged_division_of (cbox a b) \ g fine p") +proof (cases "\p. p tagged_division_of (cbox a b) \ g fine p") case True then show ?thesis using that by auto @@ -2228,14 +2228,14 @@ subsection%important \A technical lemma about "refinement" of division\ -lemma%important tagged_division_finer: +lemma tagged_division_finer: fixes p :: "('a::euclidean_space \ ('a::euclidean_space set)) set" assumes ptag: "p tagged_division_of (cbox a b)" and "gauge d" obtains q where "q tagged_division_of (cbox a b)" and "d fine q" and "\(x,k) \ p. k \ d(x) \ (x,k) \ q" -proof%unimportant - +proof - have p: "finite p" "p tagged_partial_division_of (cbox a b)" using ptag unfolding tagged_division_of_def by auto have "(\q. q tagged_division_of (\{k. \x. (x,k) \ p}) \ d fine q \ (\(x,k) \ p. k \ d(x) \ (x,k) \ q))" @@ -2307,7 +2307,7 @@ lemma is an obvious multidimensional generalization of Lemma 3, p65 of Swartz's "Introduction to Gauge Integrals". \ -proposition%important covering_lemma: +proposition covering_lemma: assumes "S \ cbox a b" "box a b \ {}" "gauge g" obtains \ where "countable \" "\\ \ cbox a b" @@ -2316,7 +2316,7 @@ "\K. K \ \ \ \x \ S \ K. K \ g x" "\u v. cbox u v \ \ \ \n. \i \ Basis. v \ i - u \ i = (b \ i - a \ i) / 2^n" "S \ \\" -proof%unimportant - +proof - have aibi: "\i. i \ Basis \ a \ i \ b \ i" and normab: "0 < norm(b - a)" using \box a b \ {}\ box_eq_empty box_sing by fastforce+ let ?K0 = "\(n, f::'a\nat). @@ -2578,11 +2578,11 @@ definition%important division_filter :: "'a::euclidean_space set \ ('a \ 'a set) set filter" where "division_filter s = (INF g\{g. gauge g}. principal {p. p tagged_division_of s \ g fine p})" -lemma%important eventually_division_filter: +proposition eventually_division_filter: "(\\<^sub>F p in division_filter s. P p) \ (\g. gauge g \ (\p. p tagged_division_of s \ g fine p \ P p))" - unfolding%unimportant division_filter_def -proof%unimportant (subst eventually_INF_base; clarsimp) + unfolding division_filter_def +proof (subst eventually_INF_base; clarsimp) fix g1 g2 :: "'a \ 'a set" show "gauge g1 \ gauge g2 \ \x. gauge x \ {p. p tagged_division_of s \ x fine p} \ {p. p tagged_division_of s \ g1 fine p} \ {p. p tagged_division_of s \ x fine p} \ {p. p tagged_division_of s \ g2 fine p}" @@ -2593,7 +2593,7 @@ unfolding trivial_limit_def eventually_division_filter by (auto elim: fine_division_exists) -lemma%important eventually_division_filter_tagged_division: +lemma eventually_division_filter_tagged_division: "eventually (\p. p tagged_division_of s) (division_filter s)" unfolding eventually_division_filter by (intro exI[of _ "\x. ball x 1"]) auto diff -r a03a63b81f44 -r a06b204527e6 src/HOL/Library/Cardinality.thy --- a/src/HOL/Library/Cardinality.thy Mon Jan 14 18:35:03 2019 +0000 +++ b/src/HOL/Library/Cardinality.thy Wed Jan 16 21:27:33 2019 +0000 @@ -153,6 +153,19 @@ lemma one_le_card_finite [simp]: "Suc 0 \ CARD('a::finite)" by (simp add: less_Suc_eq_le [symmetric]) + +class CARD_1 = + assumes CARD_1: "CARD ('a) = 1" +begin + +subclass finite +proof + from CARD_1 show "finite (UNIV :: 'a set)" + by (auto intro!: card_ge_0_finite) +qed + +end + text \Class for cardinality "at least 2"\ class card2 = finite + diff -r a03a63b81f44 -r a06b204527e6 src/HOL/Library/Numeral_Type.thy --- a/src/HOL/Library/Numeral_Type.thy Mon Jan 14 18:35:03 2019 +0000 +++ b/src/HOL/Library/Numeral_Type.thy Wed Jan 16 21:27:33 2019 +0000 @@ -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)" @@ -52,6 +54,52 @@ using finite by (rule finite_imageI) qed +instantiation num1 :: CARD_1 +begin + +instance +proof + show "CARD(num1) = 1" by auto +qed + +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)" @@ -185,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 @@ -350,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 diff -r a03a63b81f44 -r a06b204527e6 src/Pure/General/path.ML --- a/src/Pure/General/path.ML Mon Jan 14 18:35:03 2019 +0000 +++ b/src/Pure/General/path.ML Wed Jan 16 21:27:33 2019 +0000 @@ -14,6 +14,7 @@ val root: T val named_root: string -> T val parent: T + val make: string list -> T val basic: string -> T val variable: string -> T val has_parent: T -> bool @@ -22,7 +23,6 @@ val starts_basic: T -> bool val append: T -> T -> T val appends: T list -> T - val make: string list -> T val implode: T -> string val explode: string -> T val decode: T XML.Decode.T @@ -88,6 +88,7 @@ val current = Path []; val root = Path [Root ""]; fun named_root s = Path [root_elem s]; +val make = Path o rev o map basic_elem; fun basic s = Path [basic_elem s]; fun variable s = Path [variable_elem s]; val parent = Path [Parent]; @@ -117,7 +118,6 @@ fun append (Path xs) (Path ys) = Path (fold_rev apply ys xs); fun appends paths = Library.foldl (uncurry append) (current, paths); -val make = appends o map basic; fun norm elems = fold_rev apply elems []; diff -r a03a63b81f44 -r a06b204527e6 src/Pure/General/path.scala --- a/src/Pure/General/path.scala Mon Jan 14 18:35:03 2019 +0000 +++ b/src/Pure/General/path.scala Wed Jan 16 21:27:33 2019 +0000 @@ -73,6 +73,7 @@ val current: Path = new Path(Nil) val root: Path = new Path(List(Root(""))) def named_root(s: String): Path = new Path(List(root_elem(s))) + def make(elems: List[String]): Path = new Path(elems.reverse.map(basic_elem(_))) def basic(s: String): Path = new Path(List(basic_elem(s))) def variable(s: String): Path = new Path(List(variable_elem(s))) val parent: Path = new Path(List(Parent)) diff -r a03a63b81f44 -r a06b204527e6 src/Pure/Pure.thy --- a/src/Pure/Pure.thy Mon Jan 14 18:35:03 2019 +0000 +++ b/src/Pure/Pure.thy Wed Jan 16 21:27:33 2019 +0000 @@ -22,6 +22,7 @@ "hide_class" "hide_type" "hide_const" "hide_fact" :: thy_decl and "external_file" "bibtex_file" :: thy_load and "generate_file" :: thy_decl + and "export_generated_files" :: diag and "ML_file" "ML_file_debug" "ML_file_no_debug" :: thy_load % "ML" and "SML_file" "SML_file_debug" "SML_file_no_debug" :: thy_load % "ML" and "SML_import" "SML_export" "ML_export" :: thy_decl % "ML" @@ -125,6 +126,26 @@ (Parse.position Parse.path -- (\<^keyword>\=\ |-- Parse.input Parse.embedded) >> Generated_Files.generate_file_cmd); + val _ = + Outer_Syntax.command \<^command_keyword>\export_generated_files\ + "export generated files from this or other theories" + (Scan.repeat Parse.name_position >> (fn names => + Toplevel.keep (fn st => + let + val ctxt = Toplevel.context_of st; + val thy = Toplevel.theory_of st; + val other_thys = + if null names then [thy] + else map (Theory.check {long = false} ctxt) names; + val paths = Generated_Files.export_files thy other_thys; + in + if not (null paths) then + (writeln (Export.message thy ""); + writeln (cat_lines (paths |> map (fn (path, pos) => + Markup.markup (Markup.entityN, Position.def_properties_of pos) + (quote (Path.implode path)))))) + else () + end))); in end\ diff -r a03a63b81f44 -r a06b204527e6 src/Pure/Thy/export.scala --- a/src/Pure/Thy/export.scala Mon Jan 14 18:35:03 2019 +0000 +++ b/src/Pure/Thy/export.scala Wed Jan 16 21:27:33 2019 +0000 @@ -259,6 +259,7 @@ session_name: String, export_dir: Path, progress: Progress = No_Progress, + export_prune: Int = 0, export_list: Boolean = false, export_patterns: List[String] = Nil, export_prefix: String = "") @@ -287,7 +288,13 @@ name <- group.map(_._2).sorted entry <- read_entry(db, session_name, theory_name, name) } { - val path = export_dir + Path.basic(theory_name) + Path.explode(name) + val elems = theory_name :: space_explode('/', name) + val path = + if (elems.length < export_prune + 1) { + error("Cannot prune path by " + export_prune + " element(s): " + Path.make(elems)) + } + else export_dir + Path.make(elems.drop(export_prune)) + progress.echo(export_prefix + "export " + path) Isabelle_System.mkdirs(path.dir) Bytes.write(path, entry.uncompressed(cache = store.xz_cache)) @@ -311,6 +318,7 @@ var export_list = false var no_build = false var options = Options.init() + var export_prune = 0 var system_mode = false var export_patterns: List[String] = Nil @@ -323,6 +331,7 @@ -l list exports -n no build of session -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) + -p NUM prune path of exported files by NUM elements -s system build mode for session image -x PATTERN extract files matching pattern (e.g. "*:**" for all) @@ -338,6 +347,7 @@ "l" -> (_ => export_list = true), "n" -> (_ => no_build = true), "o:" -> (arg => options = options + arg), + "p:" -> (arg => export_prune = Value.Int.parse(arg)), "s" -> (_ => system_mode = true), "x:" -> (arg => export_patterns ::= arg)) @@ -366,7 +376,7 @@ /* export files */ val store = Sessions.store(options, system_mode) - export_files(store, session_name, export_dir, progress = progress, + export_files(store, session_name, export_dir, progress = progress, export_prune = export_prune, export_list = export_list, export_patterns = export_patterns) }) } diff -r a03a63b81f44 -r a06b204527e6 src/Pure/Thy/sessions.ML --- a/src/Pure/Thy/sessions.ML Mon Jan 14 18:35:03 2019 +0000 +++ b/src/Pure/Thy/sessions.ML Wed Jan 16 21:27:33 2019 +0000 @@ -35,9 +35,13 @@ Parse.!!! (Scan.optional in_path ("document", Position.none) -- Scan.repeat1 (Parse.position Parse.path)); +val prune = + Scan.optional (Parse.$$$ "[" |-- Parse.!!! (Parse.nat --| Parse.$$$ "]")) 0; + val export_files = Parse.$$$ "export_files" |-- - Parse.!!! (Scan.optional in_path ("export", Position.none) -- Scan.repeat1 Parse.embedded); + Parse.!!! + (Scan.optional in_path ("export", Position.none) -- prune -- Scan.repeat1 Parse.embedded); in @@ -95,7 +99,7 @@ in () end); val _ = - export_files |> List.app (fn (export_dir, _) => + export_files |> List.app (fn ((export_dir, _), _) => ignore (Resources.check_path ctxt session_dir export_dir)); in () end)); diff -r a03a63b81f44 -r a06b204527e6 src/Pure/Thy/sessions.scala --- a/src/Pure/Thy/sessions.scala Mon Jan 14 18:35:03 2019 +0000 +++ b/src/Pure/Thy/sessions.scala Wed Jan 16 21:27:33 2019 +0000 @@ -515,7 +515,7 @@ theories: List[(Options, List[(String, Position.T)])], global_theories: List[String], document_files: List[(Path, Path)], - export_files: List[(Path, List[String])], + export_files: List[(Path, Int, List[String])], meta_digest: SHA1.Digest) { def deps: List[String] = parent.toList ::: imports @@ -568,7 +568,7 @@ entry.document_files.map({ case (s1, s2) => (Path.explode(s1), Path.explode(s2)) }) val export_files = - entry.export_files.map({ case (dir, pats) => (Path.explode(dir), pats) }) + entry.export_files.map({ case (dir, prune, pats) => (Path.explode(dir), prune, pats) }) val meta_digest = SHA1.digest((name, chapter, entry.parent, entry.options, entry.imports, @@ -831,7 +831,7 @@ imports: List[String], theories: List[(List[Options.Spec], List[((String, Position.T), Boolean)])], document_files: List[(String, String)], - export_files: List[(String, List[String])]) extends Entry + export_files: List[(String, Int, List[String])]) extends Entry { def theories_no_position: List[(List[Options.Spec], List[(String, Boolean)])] = theories.map({ case (a, b) => (a, b.map({ case ((c, _), d) => (c, d) })) }) @@ -870,9 +870,11 @@ $$$(DOCUMENT_FILES) ~! ((in_path | success("document")) ~ rep1(path)) ^^ { case _ ~ (x ~ y) => y.map((x, _)) } + val prune = $$$("[") ~! (nat ~ $$$("]")) ^^ { case _ ~ (x ~ _) => x } | success(0) + val export_files = - $$$(EXPORT_FILES) ~! ((in_path | success("export")) ~ rep1(embedded)) ^^ - { case _ ~ (x ~ y) => (x, y) } + $$$(EXPORT_FILES) ~! ((in_path | success("export")) ~ prune ~ rep1(embedded)) ^^ + { case _ ~ (x ~ y ~ z) => (x, y, z) } command(SESSION) ~! (position(session_name) ~ diff -r a03a63b81f44 -r a06b204527e6 src/Pure/Tools/build.scala --- a/src/Pure/Tools/build.scala Mon Jan 14 18:35:03 2019 +0000 +++ b/src/Pure/Tools/build.scala Wed Jan 16 21:27:33 2019 +0000 @@ -335,9 +335,10 @@ Isabelle_System.rm_tree(export_tmp_dir) if (result1.ok) { - for ((dir, pats) <- info.export_files) { + for ((dir, prune, pats) <- info.export_files) { Export.export_files(store, name, info.dir + dir, progress = if (verbose) progress else No_Progress, + export_prune = prune, export_patterns = pats, export_prefix = name + ": ") } diff -r a03a63b81f44 -r a06b204527e6 src/Pure/Tools/generated_files.ML --- a/src/Pure/Tools/generated_files.ML Mon Jan 14 18:35:03 2019 +0000 +++ b/src/Pure/Tools/generated_files.ML Wed Jan 16 21:27:33 2019 +0000 @@ -7,9 +7,9 @@ signature GENERATED_FILES = sig val add_files: (Path.T * Position.T) * string -> theory -> theory - val get_files: theory -> (Path.T * string) list - val write_files: theory -> Path.T -> Path.T list - val export_files: theory -> Path.T list + val get_files: theory -> {path: Path.T, pos: Position.T, text: string} list + val write_files: theory -> Path.T -> (Path.T * Position.T) list + val export_files: theory -> theory list -> (Path.T * Position.T) list type file_type = {name: string, ext: string, make_comment: string -> string, make_string: string -> string} val file_type: @@ -67,18 +67,21 @@ | NONE => (path, (pos, text)) :: files)) end; -val get_files = map (apsnd #2) o rev o #1 o Data.get; +val get_files = + map (fn (path, (pos, text)) => {path = path, pos = pos, text = text}) o rev o #1 o Data.get; fun write_files thy dir = - get_files thy |> map (fn (path, text) => + get_files thy |> map (fn {path, pos, text} => let val path' = Path.expand (Path.append dir path); val _ = Isabelle_System.mkdirs (Path.dir path'); val _ = File.generate path' text; - in path end); + in (path, pos) end); -fun export_files thy = - get_files thy |> map (fn (path, text) => (Export.export thy (Path.implode path) [text]; path)); +fun export_files thy other_thys = + other_thys |> maps (fn other_thy => + get_files other_thy |> map (fn {path, pos, text} => + (Export.export thy (Path.implode path) [text]; (path, pos)))); (* file types *) diff -r a03a63b81f44 -r a06b204527e6 src/Tools/Haskell/Haskell.thy --- a/src/Tools/Haskell/Haskell.thy Mon Jan 14 18:35:03 2019 +0000 +++ b/src/Tools/Haskell/Haskell.thy Wed Jan 16 21:27:33 2019 +0000 @@ -1924,6 +1924,6 @@ return () \ -ML_command \Generated_Files.export_files \<^theory>\ +export_generated_files end diff -r a03a63b81f44 -r a06b204527e6 src/Tools/Haskell/Test.thy --- a/src/Tools/Haskell/Test.thy Mon Jan 14 18:35:03 2019 +0000 +++ b/src/Tools/Haskell/Test.thy Wed Jan 16 21:27:33 2019 +0000 @@ -14,7 +14,7 @@ val files = Generated_Files.write_files \<^theory>\Haskell\ src_dir; val modules = files - |> map (Path.implode #> unsuffix ".hs" #> space_explode "/" #> space_implode "."); + |> map (#1 #> Path.implode #> unsuffix ".hs" #> space_explode "/" #> space_implode "."); val _ = GHC.new_project tmp_dir {name = "isabelle",