# HG changeset patch # User immler # Date 1531208315 -7200 # Node ID 67bb59e49834ba962abf07a8d78420ff400a9a55 # Parent 96a49db47c9743b51b6a95b22ed241188361f377 make theorem, corollary, and proposition %important for HOL-Analysis manual diff -r 96a49db47c97 -r 67bb59e49834 src/HOL/Analysis/Connected.thy --- a/src/HOL/Analysis/Connected.thy Mon Jul 09 21:55:40 2018 +0100 +++ b/src/HOL/Analysis/Connected.thy Tue Jul 10 09:38:35 2018 +0200 @@ -776,12 +776,12 @@ subsection \Intersecting chains of compact sets and the Baire property\ -proposition%important bounded_closed_chain: +proposition bounded_closed_chain: fixes \ :: "'a::heine_borel set set" assumes "B \ \" "bounded B" and \: "\S. S \ \ \ closed S" and "{} \ \" and chain: "\S T. S \ \ \ T \ \ \ S \ T \ T \ S" shows "\\ \ {}" -proof%unimportant - +proof - have "B \ \\ \ {}" proof (rule compact_imp_fip) show "compact B" "\T. T \ \ \ closed T" @@ -824,12 +824,12 @@ then show ?thesis by blast qed -corollary%important compact_chain: +corollary compact_chain: fixes \ :: "'a::heine_borel set set" assumes "\S. S \ \ \ compact S" "{} \ \" "\S T. S \ \ \ T \ \ \ S \ T \ T \ S" shows "\ \ \ {}" -proof%unimportant (cases "\ = {}") +proof (cases "\ = {}") case True then show ?thesis by auto next @@ -852,12 +852,12 @@ qed text\The Baire property of dense sets\ -theorem%important Baire: +theorem Baire: fixes S::"'a::{real_normed_vector,heine_borel} set" assumes "closed S" "countable \" and ope: "\T. T \ \ \ openin (subtopology euclidean S) T \ S \ closure T" shows "S \ closure(\\)" -proof%unimportant (cases "\ = {}") +proof (cases "\ = {}") case True then show ?thesis using closure_subset by auto @@ -2443,11 +2443,11 @@ ultimately show ?thesis using that by blast qed -corollary%important compact_uniformly_continuous: +corollary compact_uniformly_continuous: fixes f :: "'a :: metric_space \ 'b :: metric_space" assumes f: "continuous_on S f" and S: "compact S" shows "uniformly_continuous_on S f" - using%unimportant f + using f unfolding continuous_on_iff uniformly_continuous_on_def by (force intro: compact_uniformly_equicontinuous [OF S, of "{f}"]) @@ -2929,11 +2929,11 @@ subsection \Separation between points and sets\ -lemma%important separate_point_closed: +proposition separate_point_closed: fixes s :: "'a::heine_borel set" assumes "closed s" and "a \ s" shows "\d>0. \x\s. d \ dist a x" -proof%unimportant (cases "s = {}") +proof (cases "s = {}") case True then show ?thesis by(auto intro!: exI[where x=1]) next @@ -2944,12 +2944,12 @@ by blast qed -lemma%important separate_compact_closed: +proposition separate_compact_closed: fixes s t :: "'a::heine_borel set" assumes "compact s" and t: "closed t" "s \ t = {}" shows "\d>0. \x\s. \y\t. d \ dist x y" -proof%unimportant cases +proof cases assume "s \ {} \ t \ {}" then have "s \ {}" "t \ {}" by auto let ?inf = "\x. infdist x t" @@ -2964,27 +2964,27 @@ ultimately show ?thesis by auto qed (auto intro!: exI[of _ 1]) -lemma%important separate_closed_compact: +proposition separate_closed_compact: fixes s t :: "'a::heine_borel set" assumes "closed s" and "compact t" and "s \ t = {}" shows "\d>0. \x\s. \y\t. d \ dist x y" -proof%unimportant - +proof - have *: "t \ s = {}" using assms(3) by auto show ?thesis using separate_compact_closed[OF assms(2,1) *] by (force simp: dist_commute) qed -lemma%important compact_in_open_separated: +proposition compact_in_open_separated: fixes A::"'a::heine_borel set" assumes "A \ {}" assumes "compact A" assumes "open B" assumes "A \ B" obtains e where "e > 0" "{x. infdist x A \ e} \ B" -proof%unimportant atomize_elim +proof atomize_elim have "closed (- B)" "compact A" "- B \ A = {}" using assms by (auto simp: open_Diff compact_eq_bounded_closed) from separate_closed_compact[OF this] @@ -3959,12 +3959,12 @@ unfolding complete_def by auto qed -lemma%important injective_imp_isometric: +proposition injective_imp_isometric: fixes f :: "'a::euclidean_space \ 'b::euclidean_space" assumes s: "closed s" "subspace s" and f: "bounded_linear f" "\x\s. f x = 0 \ x = 0" shows "\e>0. \x\s. norm (f x) \ e * norm x" -proof%unimportant (cases "s \ {0::'a}") +proof (cases "s \ {0::'a}") case True have "norm x \ norm (f x)" if "x \ s" for x proof - @@ -4032,11 +4032,11 @@ ultimately show ?thesis by auto qed -lemma%important closed_injective_image_subspace: +proposition closed_injective_image_subspace: fixes f :: "'a::euclidean_space \ 'b::euclidean_space" assumes "subspace s" "bounded_linear f" "\x\s. f x = 0 \ x = 0" "closed s" shows "closed(f  s)" -proof%unimportant - +proof - obtain e where "e > 0" and e: "\x\s. e * norm x \ norm (f x)" using injective_imp_isometric[OF assms(4,1,2,3)] by auto show ?thesis @@ -4182,13 +4182,13 @@ subsection \Banach fixed point theorem (not really topological ...)\ -theorem%important banach_fix: +theorem banach_fix: assumes s: "complete s" "s \ {}" and c: "0 \ c" "c < 1" and f: "f  s \ s" and lipschitz: "\x\s. \y\s. dist (f x) (f y) \ c * dist x y" shows "\!x\s. f x = x" -proof%unimportant - +proof - from c have "1 - c > 0" by simp from s(2) obtain z0 where z0: "z0 \ s" by blast @@ -4338,13 +4338,13 @@ subsection \Edelstein fixed point theorem\ -theorem%important edelstein_fix: +theorem edelstein_fix: fixes s :: "'a::metric_space set" assumes s: "compact s" "s \ {}" and gs: "(g  s) \ s" and dist: "\x\s. \y\s. x \ y \ dist (g x) (g y) < dist x y" shows "\!x\s. g x = x" -proof%unimportant - +proof - let ?D = "(\x. (x, x))  s" have D: "compact ?D" "?D \ {}" by (rule compact_continuous_image) @@ -4693,10 +4693,10 @@ done qed -proposition%important separable: +proposition separable: fixes S :: "'a:: euclidean_space set" obtains T where "countable T" "T \ S" "S \ closure T" -proof%unimportant - +proof - obtain \ :: "'a:: euclidean_space set set" where "countable \" and "{} \ \" @@ -4739,11 +4739,11 @@ qed qed -proposition%important Lindelof: +proposition Lindelof: fixes \ :: "'a::euclidean_space set set" assumes \: "\S. S \ \ \ open S" obtains \' where "\' \ \" "countable \'" "\\' = \\" -proof%unimportant - +proof - obtain \ :: "'a set set" where "countable \" "\C. C \ \ \ open C" and \: "\S. open S \ \U. U \ \ \ S = \U" @@ -5045,11 +5045,11 @@ qed -proposition%important component_diff_connected: +proposition component_diff_connected: fixes S :: "'a::metric_space set" assumes "connected S" "connected U" "S \ U" and C: "C \ components (U - S)" shows "connected(U - C)" - using%unimportant \connected S\ unfolding connected_closedin_eq not_ex de_Morgan_conj + using \connected S\ unfolding connected_closedin_eq not_ex de_Morgan_conj proof clarify fix H3 H4 assume clo3: "closedin (subtopology euclidean (U - C)) H3" @@ -5175,11 +5175,11 @@ by (metis (no_types, lifting) \0 < e\ \open S\ half_gt_zero_iff mem_Collect_eq mem_ball open_contains_ball_eq subsetI) qed -proposition%important tendsto_componentwise_iff: +proposition tendsto_componentwise_iff: fixes f :: "_ \ 'b::euclidean_space" shows "(f \ l) F \ (\i \ Basis. ((\x. (f x \ i)) \ (l \ i)) F)" (is "?lhs = ?rhs") -proof%unimportant +proof assume ?lhs then show ?rhs unfolding tendsto_def diff -r 96a49db47c97 -r 67bb59e49834 src/HOL/Analysis/Continuous_Extension.thy --- a/src/HOL/Analysis/Continuous_Extension.thy Mon Jul 09 21:55:40 2018 +0100 +++ b/src/HOL/Analysis/Continuous_Extension.thy Tue Jul 10 09:38:35 2018 +0200 @@ -13,7 +13,7 @@ text\A difference from HOL Light: all summations over infinite sets equal zero, so the "support" must be made explicit in the summation below!\ -proposition%important subordinate_partition_of_unity: +proposition subordinate_partition_of_unity: fixes S :: "'a :: euclidean_space set" assumes "S \ \\" and opC: "\T. T \ \ \ open T" and fin: "\x. x \ S \ \V. open V \ x \ V \ finite {U \ \. U \ V \ {}}" @@ -22,7 +22,7 @@ and "\x U. \U \ \; x \ S; x \ U\ \ F U x = 0" and "\x. x \ S \ supp_sum (\W. F W x) \ = 1" and "\x. x \ S \ \V. open V \ x \ V \ finite {U \ \. \x\V. F U x \ 0}" -proof%unimportant (cases "\W. W \ \ \ S \ W") +proof (cases "\W. W \ \ \ S \ W") case True then obtain W where "W \ \" "S \ W" by metis then show ?thesis @@ -283,7 +283,7 @@ "\x. f x = b \ x \ T" using assms by (auto intro: Urysohn_local_strong [of UNIV S T]) -proposition%important Urysohn: +proposition Urysohn: assumes US: "closed S" and UT: "closed T" and "S \ T = {}" @@ -292,7 +292,7 @@ "\x. f x \ closed_segment a b" "\x. x \ S \ f x = a" "\x. x \ T \ f x = b" -using%unimportant assms by (auto intro: Urysohn_local [of UNIV S T a b]) + using assms by (auto intro: Urysohn_local [of UNIV S T a b]) subsection\The Dugundji extension theorem and Tietze variants as corollaries\ @@ -300,14 +300,14 @@ text%important\J. Dugundji. An extension of Tietze's theorem. Pacific J. Math. Volume 1, Number 3 (1951), 353-367. https://projecteuclid.org/euclid.pjm/1103052106\ -theorem%important Dugundji: +theorem Dugundji: fixes f :: "'a::euclidean_space \ 'b::real_inner" assumes "convex C" "C \ {}" and cloin: "closedin (subtopology euclidean U) S" and contf: "continuous_on S f" and "f  S \ C" obtains g where "continuous_on U g" "g  U \ C" "\x. x \ S \ g x = f x" -proof%unimportant (cases "S = {}") +proof (cases "S = {}") case True then show thesis apply (rule_tac g="\x. SOME y. y \ C" in that) apply (rule continuous_intros) @@ -475,7 +475,7 @@ qed -corollary%important Tietze: +corollary Tietze: fixes f :: "'a::euclidean_space \ 'b::real_inner" assumes "continuous_on S f" and "closedin (subtopology euclidean U) S" @@ -483,7 +483,7 @@ and "\x. x \ S \ norm(f x) \ B" obtains g where "continuous_on U g" "\x. x \ S \ g x = f x" "\x. x \ U \ norm(g x) \ B" -using%unimportant assms + using assms by (auto simp: image_subset_iff intro: Dugundji [of "cball 0 B" U S f]) corollary Tietze_closed_interval: diff -r 96a49db47c97 -r 67bb59e49834 src/HOL/Analysis/Continuum_Not_Denumerable.thy --- a/src/HOL/Analysis/Continuum_Not_Denumerable.thy Mon Jul 09 21:55:40 2018 +0100 +++ b/src/HOL/Analysis/Continuum_Not_Denumerable.thy Tue Jul 10 09:38:35 2018 +0200 @@ -33,8 +33,8 @@ Nested Interval Property. \ -theorem%important real_non_denum: "\f :: nat \ real. surj f" -proof%unimportant +theorem real_non_denum: "\f :: nat \ real. surj f" +proof assume "\f::nat \ real. surj f" then obtain f :: "nat \ real" where "surj f" .. diff -r 96a49db47c97 -r 67bb59e49834 src/HOL/Analysis/Convex_Euclidean_Space.thy --- a/src/HOL/Analysis/Convex_Euclidean_Space.thy Mon Jul 09 21:55:40 2018 +0100 +++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy Tue Jul 10 09:38:35 2018 +0200 @@ -2005,9 +2005,9 @@ shows "c *\<^sub>R x \ cone hull S" by (metis assms cone_cone_hull hull_inc mem_cone) -proposition%important cone_hull_expl: "cone hull S = {c *\<^sub>R x | c x. c \ 0 \ x \ S}" +proposition cone_hull_expl: "cone hull S = {c *\<^sub>R x | c x. c \ 0 \ x \ S}" (is "?lhs = ?rhs") -proof%unimportant - +proof - { fix x assume "x \ ?rhs" @@ -2089,7 +2089,7 @@ "~ affine_dependent s \ ~ affine_dependent(s - t)" by (meson Diff_subset affine_dependent_subset) -proposition%important affine_dependent_explicit: +proposition affine_dependent_explicit: "affine_dependent p \ (\S u. finite S \ S \ p \ sum u S = 0 \ (\v\S. u v \ 0) \ sum (\v. u v *\<^sub>R v) S = 0)" proof - @@ -2524,7 +2524,7 @@ subsubsection%unimportant \Explicit expression for convex hull\ -proposition%important convex_hull_indexed: +proposition convex_hull_indexed: fixes S :: "'a::real_vector set" shows "convex hull S = {y. \k u x. (\i\{1::nat .. k}. 0 \ u i \ x i \ S) \ @@ -4020,11 +4020,11 @@ by (auto simp: convex_hull_explicit) qed -theorem%important caratheodory: +theorem caratheodory: "convex hull p = {x::'a::euclidean_space. \s. finite s \ s \ p \ card s \ DIM('a) + 1 \ x \ convex hull s}" -proof%unimportant safe +proof safe fix x assume "x \ convex hull p" then obtain s u where "finite s" "s \ p" "card s \ DIM('a) + 1" @@ -5871,10 +5871,10 @@ done qed -theorem%important radon: +theorem radon: assumes "affine_dependent c" obtains m p where "m \ c" "p \ c" "m \ p = {}" "(convex hull m) \ (convex hull p) \ {}" -proof%unimportant - +proof - from assms[unfolded affine_dependent_explicit] obtain s u where "finite s" "s \ c" "sum u s = 0" "\v\s. u v \ 0" "(\v\s. u v *\<^sub>R v) = 0" @@ -5965,12 +5965,12 @@ qed qed -theorem%important helly: +theorem helly: fixes f :: "'a::euclidean_space set set" assumes "card f \ DIM('a) + 1" "\s\f. convex s" and "\t. \t\f; card t = DIM('a) + 1\ \ \t \ {}" shows "\f \ {}" - apply%unimportant (rule helly_induct) + apply (rule helly_induct) using assms apply auto done diff -r 96a49db47c97 -r 67bb59e49834 src/HOL/Analysis/L2_Norm.thy --- a/src/HOL/Analysis/L2_Norm.thy Mon Jul 09 21:55:40 2018 +0100 +++ b/src/HOL/Analysis/L2_Norm.thy Tue Jul 10 09:38:35 2018 +0200 @@ -73,9 +73,9 @@ unfolding L2_set_def by (simp add: sum_nonneg sum_nonneg_eq_0_iff) -lemma %important L2_set_triangle_ineq: +proposition L2_set_triangle_ineq: "L2_set (\i. f i + g i) A \ L2_set f A + L2_set g A" -proof %unimportant (cases "finite A") +proof (cases "finite A") case False thus ?thesis by simp next diff -r 96a49db47c97 -r 67bb59e49834 src/HOL/Analysis/Linear_Algebra.thy --- a/src/HOL/Analysis/Linear_Algebra.thy Mon Jul 09 21:55:40 2018 +0100 +++ b/src/HOL/Analysis/Linear_Algebra.thy Tue Jul 10 09:38:35 2018 +0200 @@ -377,11 +377,11 @@ subsection \Archimedean properties and useful consequences\ text\Bernoulli's inequality\ -proposition%important Bernoulli_inequality: +proposition Bernoulli_inequality: fixes x :: real assumes "-1 \ x" shows "1 + n * x \ (1 + x) ^ n" -proof%unimportant (induct n) +proof (induct n) case 0 then show ?case by simp next diff -r 96a49db47c97 -r 67bb59e49834 src/HOL/Analysis/Measure_Space.thy --- a/src/HOL/Analysis/Measure_Space.thy Mon Jul 09 21:55:40 2018 +0100 +++ b/src/HOL/Analysis/Measure_Space.thy Tue Jul 10 09:38:35 2018 +0200 @@ -1513,7 +1513,7 @@ "f \ measurable M N \ A \ null_sets (distr M N f) \ f - A \ space M \ null_sets M \ A \ sets N" by (auto simp add: null_sets_def emeasure_distr) -lemma%important distr_distr: +proposition distr_distr: "g \ measurable N L \ f \ measurable M N \ distr (distr M N f) L g = distr M L (g \ f)" by (auto simp add: emeasure_distr measurable_space intro!: arg_cong[where f="emeasure M"] measure_eqI) @@ -2804,11 +2804,11 @@ qed auto qed -lemma%important unsigned_Hahn_decomposition: +proposition unsigned_Hahn_decomposition: assumes [simp]: "sets N = sets M" and [measurable]: "A \ sets M" and [simp]: "emeasure M A \ top" "emeasure N A \ top" shows "\Y\sets M. Y \ A \ (\X\sets M. X \ Y \ N X \ M X) \ (\X\sets M. X \ A \ X \ Y = {} \ M X \ N X)" -proof%unimportant - +proof - have "\Y\sets (restrict_space M A). (\X\sets (restrict_space M A). X \ Y \ (restrict_space N A) X \ (restrict_space M A) X) \ (\X\sets (restrict_space M A). X \ Y = {} \ (restrict_space M A) X \ (restrict_space N A) X)" @@ -2867,8 +2867,8 @@ end -lemma%important le_measure: "sets M = sets N \ M \ N \ (\A\sets M. emeasure M A \ emeasure N A)" - apply%unimportant - +proposition le_measure: "sets M = sets N \ M \ N \ (\A\sets M. emeasure M A \ emeasure N A)" + apply - apply (auto simp: le_measure_iff le_fun_def dest: sets_eq_imp_space_eq) subgoal for X by (cases "X \ sets M") (auto simp: emeasure_notin_sets) diff -r 96a49db47c97 -r 67bb59e49834 src/HOL/Analysis/Norm_Arith.thy --- a/src/HOL/Analysis/Norm_Arith.thy Mon Jul 09 21:55:40 2018 +0100 +++ b/src/HOL/Analysis/Norm_Arith.thy Tue Jul 10 09:38:35 2018 +0200 @@ -138,7 +138,7 @@ text \Hence more metric properties.\ -lemma%important dist_triangle_add: +proposition dist_triangle_add: fixes x y x' y' :: "'a::real_normed_vector" shows "dist (x + y) (x' + y') \ dist x x' + dist y y'" by norm diff -r 96a49db47c97 -r 67bb59e49834 src/HOL/Analysis/Path_Connected.thy --- a/src/HOL/Analysis/Path_Connected.thy Mon Jul 09 21:55:40 2018 +0100 +++ b/src/HOL/Analysis/Path_Connected.thy Tue Jul 10 09:38:35 2018 +0200 @@ -1964,11 +1964,11 @@ "2 \ DIM('N::euclidean_space) \ connected(- {a::'N})" by (simp add: path_connected_punctured_universe path_connected_imp_connected) -lemma%important path_connected_sphere: +proposition path_connected_sphere: fixes a :: "'a :: euclidean_space" assumes "2 \ DIM('a)" shows "path_connected(sphere a r)" -proof%unimportant (cases r "0::real" rule: linorder_cases) +proof (cases r "0::real" rule: linorder_cases) case less then show ?thesis by (simp add: path_connected_empty) @@ -2289,23 +2289,23 @@ using path_connected_translation by metis qed -lemma%important path_connected_annulus: +proposition path_connected_annulus: fixes a :: "'N::euclidean_space" assumes "2 \ DIM('N)" shows "path_connected {x. r1 < norm(x - a) \ norm(x - a) < r2}" "path_connected {x. r1 < norm(x - a) \ norm(x - a) \ r2}" "path_connected {x. r1 \ norm(x - a) \ norm(x - a) < r2}" "path_connected {x. r1 \ norm(x - a) \ norm(x - a) \ r2}" - by%unimportant (auto simp: is_interval_def intro!: is_interval_convex convex_imp_path_connected path_connected_2DIM_I [OF assms]) - -lemma%important connected_annulus: + by (auto simp: is_interval_def intro!: is_interval_convex convex_imp_path_connected path_connected_2DIM_I [OF assms]) + +proposition connected_annulus: fixes a :: "'N::euclidean_space" assumes "2 \ DIM('N::euclidean_space)" shows "connected {x. r1 < norm(x - a) \ norm(x - a) < r2}" "connected {x. r1 < norm(x - a) \ norm(x - a) \ r2}" "connected {x. r1 \ norm(x - a) \ norm(x - a) < r2}" "connected {x. r1 \ norm(x - a) \ norm(x - a) \ r2}" - by%unimportant (auto simp: path_connected_annulus [OF assms] path_connected_imp_connected) + by (auto simp: path_connected_annulus [OF assms] path_connected_imp_connected) subsection%unimportant\Relations between components and path components\ @@ -3302,14 +3302,14 @@ subsection\Condition for an open map's image to contain a ball\ -lemma%important ball_subset_open_map_image: +proposition ball_subset_open_map_image: fixes f :: "'a::heine_borel \ 'b :: {real_normed_vector,heine_borel}" assumes contf: "continuous_on (closure S) f" and oint: "open (f  interior S)" and le_no: "\z. z \ frontier S \ r \ norm(f z - f a)" and "bounded S" "a \ S" "0 < r" shows "ball (f a) r \ f  S" -proof%unimportant (cases "f  S = UNIV") +proof (cases "f  S = UNIV") case True then show ?thesis by simp next case False @@ -3868,26 +3868,26 @@ text%important\So taking equivalence classes under homotopy would give the fundamental group\ -proposition%important homotopic_paths_rid: +proposition homotopic_paths_rid: "\path p; path_image p \ s\ \ homotopic_paths s (p +++ linepath (pathfinish p) (pathfinish p)) p" - apply%unimportant (subst homotopic_paths_sym) + apply (subst homotopic_paths_sym) apply (rule homotopic_paths_reparametrize [where f = "\t. if t \ 1 / 2 then 2 *\<^sub>R t else 1"]) apply (simp_all del: le_divide_eq_numeral1) apply (subst split_01) apply (rule continuous_on_cases continuous_intros | force simp: pathfinish_def joinpaths_def)+ done -proposition%important homotopic_paths_lid: +proposition homotopic_paths_lid: "\path p; path_image p \ s\ \ homotopic_paths s (linepath (pathstart p) (pathstart p) +++ p) p" -using%unimportant homotopic_paths_rid [of "reversepath p" s] + using homotopic_paths_rid [of "reversepath p" s] by (metis homotopic_paths_reversepath path_image_reversepath path_reversepath pathfinish_linepath pathfinish_reversepath reversepath_joinpaths reversepath_linepath) -proposition%important homotopic_paths_assoc: +proposition homotopic_paths_assoc: "\path p; path_image p \ s; path q; path_image q \ s; path r; path_image r \ s; pathfinish p = pathstart q; pathfinish q = pathstart r\ \ homotopic_paths s (p +++ (q +++ r)) ((p +++ q) +++ r)" - apply%unimportant (subst homotopic_paths_sym) + apply (subst homotopic_paths_sym) apply (rule homotopic_paths_reparametrize [where f = "\t. if t \ 1 / 2 then inverse 2 *\<^sub>R t else if t \ 3 / 4 then t - (1 / 4) @@ -3898,10 +3898,10 @@ apply (auto simp: joinpaths_def) done -proposition%important homotopic_paths_rinv: +proposition homotopic_paths_rinv: assumes "path p" "path_image p \ s" shows "homotopic_paths s (p +++ reversepath p) (linepath (pathstart p) (pathstart p))" -proof%unimportant - +proof - have "continuous_on ({0..1} \ {0..1}) (\x. (subpath 0 (fst x) p +++ reversepath (subpath 0 (fst x) p)) (snd x))" using assms apply (simp add: joinpaths_def subpath_def reversepath_def path_def del: le_divide_eq_numeral1) @@ -3921,10 +3921,10 @@ done qed -proposition%important homotopic_paths_linv: +proposition homotopic_paths_linv: assumes "path p" "path_image p \ s" shows "homotopic_paths s (reversepath p +++ p) (linepath (pathfinish p) (pathfinish p))" -using%unimportant homotopic_paths_rinv [of "reversepath p" s] assms by simp + using homotopic_paths_rinv [of "reversepath p" s] assms by simp subsection\Homotopy of loops without requiring preservation of endpoints\ @@ -3994,14 +3994,14 @@ subsection\Relations between the two variants of homotopy\ -proposition%important homotopic_paths_imp_homotopic_loops: +proposition homotopic_paths_imp_homotopic_loops: "\homotopic_paths s p q; pathfinish p = pathstart p; pathfinish q = pathstart p\ \ homotopic_loops s p q" - by%unimportant (auto simp: homotopic_paths_def homotopic_loops_def intro: homotopic_with_mono) - -proposition%important homotopic_loops_imp_homotopic_paths_null: + by (auto simp: homotopic_paths_def homotopic_loops_def intro: homotopic_with_mono) + +proposition homotopic_loops_imp_homotopic_paths_null: assumes "homotopic_loops s p (linepath a a)" shows "homotopic_paths s p (linepath (pathstart p) (pathstart p))" -proof%unimportant - +proof - have "path p" by (metis assms homotopic_loops_imp_path) have ploop: "pathfinish p = pathstart p" by (metis assms homotopic_loops_imp_loop) have pip: "path_image p \ s" by (metis assms homotopic_loops_imp_subset) @@ -4069,12 +4069,12 @@ by (blast intro: homotopic_paths_trans) qed -proposition%important homotopic_loops_conjugate: +proposition homotopic_loops_conjugate: fixes s :: "'a::real_normed_vector set" assumes "path p" "path q" and pip: "path_image p \ s" and piq: "path_image q \ s" and papp: "pathfinish p = pathstart q" and qloop: "pathfinish q = pathstart q" shows "homotopic_loops s (p +++ q +++ reversepath p) q" -proof%unimportant - +proof - have contp: "continuous_on {0..1} p" using \path p\ [unfolded path_def] by blast have contq: "continuous_on {0..1} q" using \path q\ [unfolded path_def] by blast have c1: "continuous_on ({0..1} \ {0..1}) (\x. p ((1 - fst x) * snd x + fst x))" @@ -4326,10 +4326,10 @@ using homotopic_join_subpaths2 by blast qed -proposition%important homotopic_join_subpaths: +proposition homotopic_join_subpaths: "\path g; path_image g \ s; u \ {0..1}; v \ {0..1}; w \ {0..1}\ \ homotopic_paths s (subpath u v g +++ subpath v w g) (subpath u w g)" -apply%unimportant (rule le_cases3 [of u v w]) + apply (rule le_cases3 [of u v w]) using homotopic_join_subpaths1 homotopic_join_subpaths2 homotopic_join_subpaths3 by metis+ text\Relating homotopy of trivial loops to path-connectedness.\ @@ -5043,7 +5043,7 @@ subsection\Sort of induction principle for connected sets\ -lemma%important connected_induction: +proposition connected_induction: assumes "connected S" and opD: "\T a. \openin (subtopology euclidean S) T; a \ T\ \ \z. z \ T \ P z" and opI: "\a. a \ S @@ -5051,7 +5051,7 @@ (\x \ T. \y \ T. P x \ P y \ Q x \ Q y)" and etc: "a \ S" "b \ S" "P a" "P b" "Q a" shows "Q b" -proof%unimportant - +proof - have 1: "openin (subtopology euclidean S) {b. \T. openin (subtopology euclidean S) T \ b \ T \ (\x\T. P x \ Q x)}" @@ -5142,14 +5142,14 @@ subsection\Basic properties of local compactness\ -lemma%important locally_compact: +proposition locally_compact: fixes s :: "'a :: metric_space set" shows "locally compact s \ (\x \ s. \u v. x \ u \ u \ v \ v \ s \ openin (subtopology euclidean s) u \ compact v)" (is "?lhs = ?rhs") -proof%unimportant +proof assume ?lhs then show ?rhs apply clarify @@ -5696,12 +5696,12 @@ by (metis \U = S \ V\ inf.bounded_iff openin_imp_subset that) qed -corollary%important Sura_Bura: +corollary Sura_Bura: fixes S :: "'a::euclidean_space set" assumes "locally compact S" "C \ components S" "compact C" shows "C = \ {K. C \ K \ compact K \ openin (subtopology euclidean S) K}" (is "C = ?rhs") -proof%unimportant +proof show "?rhs \ C" proof (clarsimp, rule ccontr) fix x @@ -5831,17 +5831,17 @@ by (metis assms(1) assms(2) assms(3) mem_Collect_eq path_component_subset path_connected_path_component) qed -proposition%important locally_path_connected: +proposition locally_path_connected: "locally path_connected S \ (\v x. openin (subtopology euclidean S) v \ x \ v \ (\u. openin (subtopology euclidean S) u \ path_connected u \ x \ u \ u \ v))" -by%unimportant (metis locally_path_connected_1 locally_path_connected_2 locally_path_connected_3) - -proposition%important locally_path_connected_open_path_component: + by (metis locally_path_connected_1 locally_path_connected_2 locally_path_connected_3) + +proposition locally_path_connected_open_path_component: "locally path_connected S \ (\t x. openin (subtopology euclidean S) t \ x \ t \ openin (subtopology euclidean S) (path_component_set t x))" -by%unimportant (metis locally_path_connected_1 locally_path_connected_2 locally_path_connected_3) + by (metis locally_path_connected_1 locally_path_connected_2 locally_path_connected_3) lemma locally_connected_open_component: "locally connected S \ @@ -5849,14 +5849,14 @@ \ openin (subtopology euclidean S) c)" by (metis components_iff locally_connected_open_connected_component) -proposition%important locally_connected_im_kleinen: +proposition locally_connected_im_kleinen: "locally connected S \ (\v x. openin (subtopology euclidean S) v \ x \ v \ (\u. openin (subtopology euclidean S) u \ x \ u \ u \ v \ (\y. y \ u \ (\c. connected c \ c \ v \ x \ c \ y \ c))))" (is "?lhs = ?rhs") -proof%unimportant +proof assume ?lhs then show ?rhs by (fastforce simp add: locally_connected) @@ -5890,7 +5890,7 @@ done qed -proposition%important locally_path_connected_im_kleinen: +proposition locally_path_connected_im_kleinen: "locally path_connected S \ (\v x. openin (subtopology euclidean S) v \ x \ v \ (\u. openin (subtopology euclidean S) u \ @@ -5898,7 +5898,7 @@ (\y. y \ u \ (\p. path p \ path_image p \ v \ pathstart p = x \ pathfinish p = y))))" (is "?lhs = ?rhs") -proof%unimportant +proof assume ?lhs then show ?rhs apply (simp add: locally_path_connected path_connected_def) @@ -6048,13 +6048,13 @@ shows "open S \ path_component_set S x = connected_component_set S x" by (simp add: open_path_connected_component) -proposition%important locally_connected_quotient_image: +proposition locally_connected_quotient_image: assumes lcS: "locally connected S" and oo: "\T. T \ f  S \ openin (subtopology euclidean S) (S \ f - T) \ openin (subtopology euclidean (f  S)) T" shows "locally connected (f  S)" -proof%unimportant (clarsimp simp: locally_connected_open_component) +proof (clarsimp simp: locally_connected_open_component) fix U C assume opefSU: "openin (subtopology euclidean (f  S)) U" and "C \ components U" then have "C \ U" "U \ f  S" @@ -6114,12 +6114,12 @@ qed text\The proof resembles that above but is not identical!\ -proposition%important locally_path_connected_quotient_image: +proposition locally_path_connected_quotient_image: assumes lcS: "locally path_connected S" and oo: "\T. T \ f  S \ openin (subtopology euclidean S) (S \ f - T) \ openin (subtopology euclidean (f  S)) T" shows "locally path_connected (f  S)" -proof%unimportant (clarsimp simp: locally_path_connected_open_path_component) +proof (clarsimp simp: locally_path_connected_open_path_component) fix U y assume opefSU: "openin (subtopology euclidean (f  S)) U" and "y \ U" then have "path_component_set U y \ U" "U \ f  S" @@ -6345,7 +6345,7 @@ by (rule that [OF \linear f\ \f  S \ T\]) qed -proposition%important isometries_subspaces: +proposition isometries_subspaces: fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set" assumes S: "subspace S" @@ -6356,7 +6356,7 @@ "\x. x \ T \ norm(g x) = norm x" "\x. x \ S \ g(f x) = x" "\x. x \ T \ f(g x) = x" -proof%unimportant - +proof - obtain B where "B \ S" and Borth: "pairwise orthogonal B" and B1: "\x. x \ B \ norm x = 1" and "independent B" "finite B" "card B = dim S" "span B = S" @@ -7815,7 +7815,7 @@ qed qed -proposition%important homeomorphism_moving_points_exists: +proposition homeomorphism_moving_points_exists: fixes S :: "'a::euclidean_space set" assumes 2: "2 \ DIM('a)" "open S" "connected S" "S \ T" "finite K" and KS: "\i. i \ K \ x i \ S \ y i \ S" @@ -7823,7 +7823,7 @@ and S: "S \ T" "T \ affine hull S" "connected S" obtains f g where "homeomorphism T T f g" "\i. i \ K \ f(x i) = y i" "{x. ~ (f x = x \ g x = x)} \ S" "bounded {x. (~ (f x = x \ g x = x))}" -proof%unimportant (cases "S = {}") +proof (cases "S = {}") case True then show ?thesis using KS homeomorphism_ident that by fastforce @@ -8082,12 +8082,12 @@ qed qed -proposition%important homeomorphism_grouping_points_exists: +proposition homeomorphism_grouping_points_exists: fixes S :: "'a::euclidean_space set" assumes "open U" "open S" "connected S" "U \ {}" "finite K" "K \ S" "U \ S" "S \ T" obtains f g where "homeomorphism T T f g" "{x. (~ (f x = x \ g x = x))} \ S" "bounded {x. (~ (f x = x \ g x = x))}" "\x. x \ K \ f x \ U" -proof%unimportant (cases "2 \ DIM('a)") +proof (cases "2 \ DIM('a)") case True have TS: "T \ affine hull S" using affine_hull_open assms by blast @@ -8364,13 +8364,13 @@ qed qed -proposition%important nullhomotopic_from_sphere_extension: +proposition nullhomotopic_from_sphere_extension: fixes f :: "'M::euclidean_space \ 'a::real_normed_vector" shows "(\c. homotopic_with (\x. True) (sphere a r) S f (\x. c)) \ (\g. continuous_on (cball a r) g \ g  (cball a r) \ S \ (\x \ sphere a r. g x = f x))" (is "?lhs = ?rhs") -proof%unimportant (cases r "0::real" rule: linorder_cases) +proof (cases r "0::real" rule: linorder_cases) case equal then show ?thesis apply (auto simp: homotopic_with) diff -r 96a49db47c97 -r 67bb59e49834 src/HOL/Analysis/Product_Vector.thy --- a/src/HOL/Analysis/Product_Vector.thy Mon Jul 09 21:55:40 2018 +0100 +++ b/src/HOL/Analysis/Product_Vector.thy Tue Jul 10 09:38:35 2018 +0200 @@ -314,11 +314,11 @@ subsubsection%unimportant \Pair operations are linear\ -lemma%important bounded_linear_fst: "bounded_linear fst" +proposition bounded_linear_fst: "bounded_linear fst" using fst_add fst_scaleR by (rule bounded_linear_intro [where K=1], simp add: norm_prod_def) -lemma%important bounded_linear_snd: "bounded_linear snd" +proposition bounded_linear_snd: "bounded_linear snd" using snd_add snd_scaleR by (rule bounded_linear_intro [where K=1], simp add: norm_prod_def) @@ -354,10 +354,10 @@ subsubsection%unimportant \Frechet derivatives involving pairs\ -lemma%important has_derivative_Pair [derivative_intros]: +proposition has_derivative_Pair [derivative_intros]: assumes f: "(f has_derivative f') (at x within s)" and g: "(g has_derivative g') (at x within s)" shows "((\x. (f x, g x)) has_derivative (\h. (f' h, g' h))) (at x within s)" -proof%unimportant (rule has_derivativeI_sandwich[of 1]) +proof (rule has_derivativeI_sandwich[of 1]) show "bounded_linear (\h. (f' h, g' h))" using f g by (intro bounded_linear_Pair has_derivative_bounded_linear) let ?Rf = "\y. f y - f x - f' (y - x)" diff -r 96a49db47c97 -r 67bb59e49834 src/HOL/Analysis/Sigma_Algebra.thy --- a/src/HOL/Analysis/Sigma_Algebra.thy Mon Jul 09 21:55:40 2018 +0100 +++ b/src/HOL/Analysis/Sigma_Algebra.thy Tue Jul 10 09:38:35 2018 +0200 @@ -146,13 +146,13 @@ "a \ M \ \ - a \ M" by auto -lemma%important algebra_iff_Un: +proposition algebra_iff_Un: "algebra \ M \ M \ Pow \ \ {} \ M \ (\a \ M. \ - a \ M) \ (\a \ M. \ b \ M. a \ b \ M)" (is "_ \ ?Un") -proof%unimportant +proof assume "algebra \ M" then interpret algebra \ M . show ?Un using sets_into_space by auto @@ -173,12 +173,12 @@ show "algebra \ M" proof qed fact qed -lemma%important algebra_iff_Int: +proposition algebra_iff_Int: "algebra \ M \ M \ Pow \ & {} \ M & (\a \ M. \ - a \ M) & (\a \ M. \ b \ M. a \ b \ M)" (is "_ \ ?Int") -proof%unimportant +proof assume "algebra \ M" then interpret algebra \ M . show ?Int using sets_into_space by auto @@ -1433,7 +1433,7 @@ text%important \The reason to introduce Dynkin-systems is the following induction rules for $\sigma$-algebras generated by a generator closed under intersection.\ -lemma%important sigma_sets_induct_disjoint[consumes 3, case_names basic empty compl union]: +proposition sigma_sets_induct_disjoint[consumes 3, case_names basic empty compl union]: assumes "Int_stable G" and closed: "G \ Pow \" and A: "A \ sigma_sets \ G" @@ -1442,7 +1442,7 @@ and compl: "\A. A \ sigma_sets \ G \ P A \ P (\ - A)" and union: "\A. disjoint_family A \ range A \ sigma_sets \ G \ (\i. P (A i)) \ P (\i::nat. A i)" shows "P A" -proof%unimportant - +proof - let ?D = "{ A \ sigma_sets \ G. P A }" interpret sigma_algebra \ "sigma_sets \ G" using closed by (rule sigma_algebra_sigma_sets) @@ -1633,12 +1633,12 @@ subsubsection \Constructing simple @{typ "'a measure"}\ -lemma%important emeasure_measure_of: +proposition emeasure_measure_of: assumes M: "M = measure_of \ A \" assumes ms: "A \ Pow \" "positive (sets M) \" "countably_additive (sets M) \" assumes X: "X \ sets M" shows "emeasure M X = \ X" -proof%unimportant - +proof - interpret sigma_algebra \ "sigma_sets \ A" by (rule sigma_algebra_sigma_sets) fact have "measure_space \ (sigma_sets \ A) \" using ms M by (simp add: measure_space_def sigma_algebra_sigma_sets) diff -r 96a49db47c97 -r 67bb59e49834 src/HOL/Analysis/Starlike.thy --- a/src/HOL/Analysis/Starlike.thy Mon Jul 09 21:55:40 2018 +0100 +++ b/src/HOL/Analysis/Starlike.thy Tue Jul 10 09:38:35 2018 +0200 @@ -5063,12 +5063,12 @@ subsection\Connectedness of the intersection of a chain\ -proposition%important connected_chain: +proposition connected_chain: fixes \ :: "'a :: euclidean_space set set" assumes cc: "\S. S \ \ \ compact S \ connected S" and linear: "\S T. S \ \ \ T \ \ \ S \ T \ T \ S" shows "connected(\\)" -proof%unimportant (cases "\ = {}") +proof (cases "\ = {}") case True then show ?thesis by auto next @@ -5212,13 +5212,13 @@ by (meson le_max_iff_disj) qed -proposition%important proper_map: +proposition proper_map: fixes f :: "'a::heine_borel \ 'b::heine_borel" assumes "closedin (subtopology euclidean S) K" and com: "\U. \U \ T; compact U\ \ compact (S \ f - U)" and "f  S \ T" shows "closedin (subtopology euclidean T) (f  K)" -proof%unimportant - +proof - have "K \ S" using assms closedin_imp_subset by metis obtain C where "closed C" and Keq: "K = S \ C" @@ -6708,11 +6708,11 @@ by (metis a orthogonal_clauses(1,2,4) span_induct_alt x) -proposition%important Gram_Schmidt_step: +proposition Gram_Schmidt_step: fixes S :: "'a::euclidean_space set" assumes S: "pairwise orthogonal S" and x: "x \ span S" shows "orthogonal x (a - (\b\S. (b \ a / (b \ b)) *\<^sub>R b))" -proof%unimportant - +proof - have "finite S" by (simp add: S pairwise_orthogonal_imp_finite) have "orthogonal (a - (\b\S. (b \ a / (b \ b)) *\<^sub>R b)) x" @@ -6767,11 +6767,11 @@ qed -proposition%important orthogonal_extension: +proposition orthogonal_extension: fixes S :: "'a::euclidean_space set" assumes S: "pairwise orthogonal S" obtains U where "pairwise orthogonal (S \ U)" "span (S \ U) = span (S \ T)" -proof%unimportant - +proof - obtain B where "finite B" "span B = span T" using basis_subspace_exists [of "span T"] subspace_span by metis with orthogonal_extension_aux [of B S] @@ -6827,13 +6827,13 @@ done qed -proposition%important orthonormal_basis_subspace: +proposition orthonormal_basis_subspace: fixes S :: "'a :: euclidean_space set" assumes "subspace S" obtains B where "B \ S" "pairwise orthogonal B" and "\x. x \ B \ norm x = 1" and "independent B" "card B = dim S" "span B = S" -proof%unimportant - +proof - obtain B where "0 \ B" "B \ S" and orth: "pairwise orthogonal B" and "independent B" "card B = dim S" "span B = S" @@ -6864,11 +6864,11 @@ qed -proposition%important orthogonal_to_subspace_exists_gen: +proposition orthogonal_to_subspace_exists_gen: fixes S :: "'a :: euclidean_space set" assumes "span S \ span T" obtains x where "x \ 0" "x \ span T" "\y. y \ span S \ orthogonal x y" -proof%unimportant - +proof - obtain B where "B \ span S" and orthB: "pairwise orthogonal B" and "\x. x \ B \ norm x = 1" and "independent B" "card B = dim S" "span B = span S" @@ -6933,10 +6933,10 @@ by (rule orthogonal_to_subspace_exists) (simp add: orthogonal_commute span_base that) qed -proposition%important orthogonal_subspace_decomp_exists: +proposition orthogonal_subspace_decomp_exists: fixes S :: "'a :: euclidean_space set" obtains y z where "y \ span S" "\w. w \ span S \ orthogonal z w" "x = y + z" -proof%unimportant - +proof - obtain T where "0 \ T" "T \ span S" "pairwise orthogonal T" "independent T" "card T = dim (span S)" "span T = span S" using orthogonal_basis_subspace subspace_span by blast @@ -7030,11 +7030,11 @@ qed qed -proposition%important dim_orthogonal_sum: +proposition dim_orthogonal_sum: fixes A :: "'a::euclidean_space set" assumes "\x y. \x \ A; y \ B\ \ x \ y = 0" shows "dim(A \ B) = dim A + dim B" -proof%unimportant - +proof - have 1: "\x y. \x \ span A; y \ B\ \ x \ y = 0" by (erule span_induct [OF _ subspace_hyperplane2]; simp add: assms) have "\x y. \x \ span A; y \ span B\ \ x \ y = 0" @@ -7163,10 +7163,10 @@ subsection\Lower-dimensional affine subsets are nowhere dense\ -proposition%important dense_complement_subspace: +proposition dense_complement_subspace: fixes S :: "'a :: euclidean_space set" assumes dim_less: "dim T < dim S" and "subspace S" shows "closure(S - T) = S" -proof%unimportant - +proof - have "closure(S - U) = S" if "dim U < dim S" "U \ S" for U proof - have "span U \ span S" @@ -7465,7 +7465,7 @@ subsection\Several Variants of Paracompactness\ -proposition%important paracompact: +proposition paracompact: fixes S :: "'a :: euclidean_space set" assumes "S \ \\" and opC: "\T. T \ \ \ open T" obtains \' where "S \ \ \'" @@ -7473,7 +7473,7 @@ and "\x. x \ S \ \V. open V \ x \ V \ finite {U. U \ \' \ (U \ V \ {})}" -proof%unimportant (cases "S = {}") +proof (cases "S = {}") case True with that show ?thesis by blast next case False @@ -7858,14 +7858,14 @@ subsection\Covering an open set by a countable chain of compact sets\ -proposition%important open_Union_compact_subsets: +proposition open_Union_compact_subsets: fixes S :: "'a::euclidean_space set" assumes "open S" obtains C where "\n. compact(C n)" "\n. C n \ S" "\n. C n \ interior(C(Suc n))" "\(range C) = S" "\K. \compact K; K \ S\ \ \N. \n\N. K \ (C n)" -proof%unimportant (cases "S = {}") +proof (cases "S = {}") case True then show ?thesis by (rule_tac C = "\n. {}" in that) auto diff -r 96a49db47c97 -r 67bb59e49834 src/HOL/Analysis/Topology_Euclidean_Space.thy --- a/src/HOL/Analysis/Topology_Euclidean_Space.thy Mon Jul 09 21:55:40 2018 +0100 +++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy Tue Jul 10 09:38:35 2018 +0200 @@ -640,7 +640,7 @@ subsubsection \Main properties of open sets\ -lemma%important openin_clauses: +proposition openin_clauses: fixes U :: "'a topology" shows "openin U {}" @@ -2765,16 +2765,16 @@ subsection \Limits\ -lemma%important Lim: "(f \ l) net \ trivial_limit net \ (\e>0. eventually (\x. dist (f x) l < e) net)" +proposition Lim: "(f \ l) net \ trivial_limit net \ (\e>0. eventually (\x. dist (f x) l < e) net)" by (auto simp: tendsto_iff trivial_limit_eq) text \Show that they yield usual definitions in the various cases.\ -lemma%important Lim_within_le: "(f \ l)(at a within S) \ +proposition Lim_within_le: "(f \ l)(at a within S) \ (\e>0. \d>0. \x\S. 0 < dist x a \ dist x a \ d \ dist (f x) l < e)" by (auto simp: tendsto_iff eventually_at_le) -lemma%important Lim_within: "(f \ l) (at a within S) \ +proposition Lim_within: "(f \ l) (at a within S) \ (\e >0. \d>0. \x \ S. 0 < dist x a \ dist x a < d \ dist (f x) l < e)" by (auto simp: tendsto_iff eventually_at) @@ -2785,11 +2785,11 @@ apply (rule ex_forward [OF assms [OF half_gt_zero]], auto) done -lemma%important Lim_at: "(f \ l) (at a) \ +proposition Lim_at: "(f \ l) (at a) \ (\e >0. \d>0. \x. 0 < dist x a \ dist x a < d \ dist (f x) l < e)" by (auto simp: tendsto_iff eventually_at) -lemma%important Lim_at_infinity: "(f \ l) at_infinity \ (\e>0. \b. \x. norm x \ b \ dist (f x) l < e)" +proposition Lim_at_infinity: "(f \ l) at_infinity \ (\e>0. \b. \x. norm x \ b \ dist (f x) l < e)" by (auto simp: tendsto_iff eventually_at_infinity) corollary Lim_at_infinityI [intro?]: @@ -3652,12 +3652,12 @@ subsubsection \Bolzano-Weierstrass property\ -lemma%important heine_borel_imp_bolzano_weierstrass: +proposition heine_borel_imp_bolzano_weierstrass: assumes "compact s" and "infinite t" and "t \ s" shows "\x \ s. x islimpt t" -proof%unimportant (rule ccontr) +proof (rule ccontr) assume "\ (\x \ s. x islimpt t)" then obtain f where f: "\x\s. x \ f x \ open (f x) \ (\y\t. y \ f x \ y = x)" unfolding islimpt_def @@ -4170,9 +4170,9 @@ unfolding C_def by (intro exI[of _ "f`T"]) fastforce qed -lemma%important countably_compact_imp_compact_second_countable: +proposition countably_compact_imp_compact_second_countable: "countably_compact U \ compact (U :: 'a :: second_countable_topology set)" -proof%unimportant (rule countably_compact_imp_compact) +proof (rule countably_compact_imp_compact) fix T and x :: 'a assume "open T" "x \ T" from topological_basisE[OF is_basis this] obtain b where @@ -4448,10 +4448,10 @@ shows "seq_compact U \ compact U" using seq_compact_eq_countably_compact countably_compact_eq_compact by blast -lemma%important bolzano_weierstrass_imp_seq_compact: +proposition bolzano_weierstrass_imp_seq_compact: fixes s :: "'a::{t1_space, first_countable_topology} set" shows "\t. infinite t \ t \ s \ (\x \ s. x islimpt t) \ seq_compact s" - by%unimportant (rule countable_acc_point_imp_seq_compact) (metis islimpt_eq_acc_point) + by (rule countable_acc_point_imp_seq_compact) (metis islimpt_eq_acc_point) subsubsection\Totally bounded\ @@ -4459,10 +4459,10 @@ lemma cauchy_def: "Cauchy s \ (\e>0. \N. \m n. m \ N \ n \ N \ dist (s m) (s n) < e)" unfolding Cauchy_def by metis -lemma%important seq_compact_imp_totally_bounded: +proposition seq_compact_imp_totally_bounded: assumes "seq_compact s" shows "\e>0. \k. finite k \ k \ s \ s \ (\x\k. ball x e)" -proof%unimportant - +proof - { fix e::real assume "e > 0" assume *: "\k. finite k \ k \ s \ \ s \ (\x\k. ball x e)" let ?Q = "\x n r. r \ s \ (\m < (n::nat). \ (dist (x m) r < e))" have "\x. \n::nat. ?Q x n (x n)" @@ -4491,11 +4491,11 @@ subsubsection\Heine-Borel theorem\ -lemma%important seq_compact_imp_heine_borel: +proposition seq_compact_imp_heine_borel: fixes s :: "'a :: metric_space set" assumes "seq_compact s" shows "compact s" -proof%unimportant - +proof - from seq_compact_imp_totally_bounded[OF \seq_compact s\] obtain f where f: "\e>0. finite (f e) \ f e \ s \ s \ (\x\f e. ball x e)" unfolding choice_iff' .. @@ -4536,22 +4536,22 @@ qed qed -lemma%important compact_eq_seq_compact_metric: +proposition compact_eq_seq_compact_metric: "compact (s :: 'a::metric_space set) \ seq_compact s" using compact_imp_seq_compact seq_compact_imp_heine_borel by blast -lemma%important compact_def: \ \this is the definition of compactness in HOL Light\ +proposition compact_def: \ \this is the definition of compactness in HOL Light\ "compact (S :: 'a::metric_space set) \ (\f. (\n. f n \ S) \ (\l\S. \r::nat\nat. strict_mono r \ (f \ r) \ l))" unfolding compact_eq_seq_compact_metric seq_compact_def by auto subsubsection \Complete the chain of compactness variants\ -lemma%important compact_eq_bolzano_weierstrass: +proposition compact_eq_bolzano_weierstrass: fixes s :: "'a::metric_space set" shows "compact s \ (\t. infinite t \ t \ s --> (\x \ s. x islimpt t))" (is "?lhs = ?rhs") -proof%unimportant +proof assume ?lhs then show ?rhs using heine_borel_imp_bolzano_weierstrass[of s] by auto @@ -4561,7 +4561,7 @@ unfolding compact_eq_seq_compact_metric by (rule bolzano_weierstrass_imp_seq_compact) qed -lemma%important bolzano_weierstrass_imp_bounded: +proposition bolzano_weierstrass_imp_bounded: "\t. infinite t \ t \ s \ (\x \ s. x islimpt t) \ bounded s" using compact_imp_bounded unfolding compact_eq_bolzano_weierstrass . @@ -4577,12 +4577,12 @@ assumes bounded_imp_convergent_subsequence: "bounded (range f) \ \l r. strict_mono (r::nat\nat) \ ((f \ r) \ l) sequentially" -lemma%important bounded_closed_imp_seq_compact: +proposition bounded_closed_imp_seq_compact: fixes s::"'a::heine_borel set" assumes "bounded s" and "closed s" shows "seq_compact s" -proof%unimportant (unfold seq_compact_def, clarify) +proof (unfold seq_compact_def, clarify) fix f :: "nat \ 'a" assume f: "\n. f n \ s" with \bounded s\ have "bounded (range f)" @@ -4807,12 +4807,12 @@ subsubsection \Completeness\ -lemma%important (in metric_space) completeI: +proposition (in metric_space) completeI: assumes "\f. \n. f n \ s \ Cauchy f \ \l\s. f \ l" shows "complete s" using assms unfolding complete_def by fast -lemma%important (in metric_space) completeE: +proposition (in metric_space) completeE: assumes "complete s" and "\n. f n \ s" and "Cauchy f" obtains l where "l \ s" and "f \ l" using assms unfolding complete_def by fast @@ -4862,10 +4862,10 @@ then show ?thesis unfolding complete_def by auto qed -lemma%important compact_eq_totally_bounded: +proposition compact_eq_totally_bounded: "compact s \ complete s \ (\e>0. \k. finite k \ s \ (\x\k. ball x e))" (is "_ \ ?rhs") -proof%unimportant +proof assume assms: "?rhs" then obtain k where k: "\e. 0 < e \ finite (k e)" "\e. 0 < e \ s \ (\x\k e. ball x e)" by (auto simp: choice_iff') @@ -5069,7 +5069,7 @@ text\Derive the epsilon-delta forms, which we often use as "definitions"\ -lemma%important continuous_within_eps_delta: +proposition continuous_within_eps_delta: "continuous (at x within s) f \ (\e>0. \d>0. \x'\ s. dist x' x < d --> dist (f x') (f x) < e)" unfolding continuous_within and Lim_within by fastforce diff -r 96a49db47c97 -r 67bb59e49834 src/HOL/ROOT --- a/src/HOL/ROOT Mon Jul 09 21:55:40 2018 +0100 +++ b/src/HOL/ROOT Tue Jul 10 09:38:35 2018 +0200 @@ -58,7 +58,7 @@ document_files "root.bib" "root.tex" session "HOL-Analysis" (main timing) in Analysis = HOL + - options [document_tags = "%unimportant", + options [document_tags = "theorem%important,corollary%important,proposition%important,%unimportant", document_variants = "document:manual=-proof,-ML,-unimportant"] sessions "HOL-Library"