--- 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 \<open>Intersecting chains of compact sets and the Baire property\<close>
-proposition%important bounded_closed_chain:
+proposition bounded_closed_chain:
fixes \<F> :: "'a::heine_borel set set"
assumes "B \<in> \<F>" "bounded B" and \<F>: "\<And>S. S \<in> \<F> \<Longrightarrow> closed S" and "{} \<notin> \<F>"
and chain: "\<And>S T. S \<in> \<F> \<and> T \<in> \<F> \<Longrightarrow> S \<subseteq> T \<or> T \<subseteq> S"
shows "\<Inter>\<F> \<noteq> {}"
-proof%unimportant -
+proof -
have "B \<inter> \<Inter>\<F> \<noteq> {}"
proof (rule compact_imp_fip)
show "compact B" "\<And>T. T \<in> \<F> \<Longrightarrow> closed T"
@@ -824,12 +824,12 @@
then show ?thesis by blast
qed
-corollary%important compact_chain:
+corollary compact_chain:
fixes \<F> :: "'a::heine_borel set set"
assumes "\<And>S. S \<in> \<F> \<Longrightarrow> compact S" "{} \<notin> \<F>"
"\<And>S T. S \<in> \<F> \<and> T \<in> \<F> \<Longrightarrow> S \<subseteq> T \<or> T \<subseteq> S"
shows "\<Inter> \<F> \<noteq> {}"
-proof%unimportant (cases "\<F> = {}")
+proof (cases "\<F> = {}")
case True
then show ?thesis by auto
next
@@ -852,12 +852,12 @@
qed
text\<open>The Baire property of dense sets\<close>
-theorem%important Baire:
+theorem Baire:
fixes S::"'a::{real_normed_vector,heine_borel} set"
assumes "closed S" "countable \<G>"
and ope: "\<And>T. T \<in> \<G> \<Longrightarrow> openin (subtopology euclidean S) T \<and> S \<subseteq> closure T"
shows "S \<subseteq> closure(\<Inter>\<G>)"
-proof%unimportant (cases "\<G> = {}")
+proof (cases "\<G> = {}")
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 \<Rightarrow> '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 \<open>Separation between points and sets\<close>
-lemma%important separate_point_closed:
+proposition separate_point_closed:
fixes s :: "'a::heine_borel set"
assumes "closed s" and "a \<notin> s"
shows "\<exists>d>0. \<forall>x\<in>s. d \<le> 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 \<inter> t = {}"
shows "\<exists>d>0. \<forall>x\<in>s. \<forall>y\<in>t. d \<le> dist x y"
-proof%unimportant cases
+proof cases
assume "s \<noteq> {} \<and> t \<noteq> {}"
then have "s \<noteq> {}" "t \<noteq> {}" by auto
let ?inf = "\<lambda>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 \<inter> t = {}"
shows "\<exists>d>0. \<forall>x\<in>s. \<forall>y\<in>t. d \<le> dist x y"
-proof%unimportant -
+proof -
have *: "t \<inter> 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 \<noteq> {}"
assumes "compact A"
assumes "open B"
assumes "A \<subseteq> B"
obtains e where "e > 0" "{x. infdist x A \<le> e} \<subseteq> B"
-proof%unimportant atomize_elim
+proof atomize_elim
have "closed (- B)" "compact A" "- B \<inter> 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 \<Rightarrow> 'b::euclidean_space"
assumes s: "closed s" "subspace s"
and f: "bounded_linear f" "\<forall>x\<in>s. f x = 0 \<longrightarrow> x = 0"
shows "\<exists>e>0. \<forall>x\<in>s. norm (f x) \<ge> e * norm x"
-proof%unimportant (cases "s \<subseteq> {0::'a}")
+proof (cases "s \<subseteq> {0::'a}")
case True
have "norm x \<le> norm (f x)" if "x \<in> 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 \<Rightarrow> 'b::euclidean_space"
assumes "subspace s" "bounded_linear f" "\<forall>x\<in>s. f x = 0 \<longrightarrow> x = 0" "closed s"
shows "closed(f ` s)"
-proof%unimportant -
+proof -
obtain e where "e > 0" and e: "\<forall>x\<in>s. e * norm x \<le> norm (f x)"
using injective_imp_isometric[OF assms(4,1,2,3)] by auto
show ?thesis
@@ -4182,13 +4182,13 @@
subsection \<open>Banach fixed point theorem (not really topological ...)\<close>
-theorem%important banach_fix:
+theorem banach_fix:
assumes s: "complete s" "s \<noteq> {}"
and c: "0 \<le> c" "c < 1"
and f: "f ` s \<subseteq> s"
and lipschitz: "\<forall>x\<in>s. \<forall>y\<in>s. dist (f x) (f y) \<le> c * dist x y"
shows "\<exists>!x\<in>s. f x = x"
-proof%unimportant -
+proof -
from c have "1 - c > 0" by simp
from s(2) obtain z0 where z0: "z0 \<in> s" by blast
@@ -4338,13 +4338,13 @@
subsection \<open>Edelstein fixed point theorem\<close>
-theorem%important edelstein_fix:
+theorem edelstein_fix:
fixes s :: "'a::metric_space set"
assumes s: "compact s" "s \<noteq> {}"
and gs: "(g ` s) \<subseteq> s"
and dist: "\<forall>x\<in>s. \<forall>y\<in>s. x \<noteq> y \<longrightarrow> dist (g x) (g y) < dist x y"
shows "\<exists>!x\<in>s. g x = x"
-proof%unimportant -
+proof -
let ?D = "(\<lambda>x. (x, x)) ` s"
have D: "compact ?D" "?D \<noteq> {}"
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 \<subseteq> S" "S \<subseteq> closure T"
-proof%unimportant -
+proof -
obtain \<B> :: "'a:: euclidean_space set set"
where "countable \<B>"
and "{} \<notin> \<B>"
@@ -4739,11 +4739,11 @@
qed
qed
-proposition%important Lindelof:
+proposition Lindelof:
fixes \<F> :: "'a::euclidean_space set set"
assumes \<F>: "\<And>S. S \<in> \<F> \<Longrightarrow> open S"
obtains \<F>' where "\<F>' \<subseteq> \<F>" "countable \<F>'" "\<Union>\<F>' = \<Union>\<F>"
-proof%unimportant -
+proof -
obtain \<B> :: "'a set set"
where "countable \<B>" "\<And>C. C \<in> \<B> \<Longrightarrow> open C"
and \<B>: "\<And>S. open S \<Longrightarrow> \<exists>U. U \<subseteq> \<B> \<and> S = \<Union>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 \<subseteq> U" and C: "C \<in> components (U - S)"
shows "connected(U - C)"
- using%unimportant \<open>connected S\<close> unfolding connected_closedin_eq not_ex de_Morgan_conj
+ using \<open>connected S\<close> 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) \<open>0 < e\<close> \<open>open S\<close> 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 :: "_ \<Rightarrow> 'b::euclidean_space"
shows "(f \<longlongrightarrow> l) F \<longleftrightarrow> (\<forall>i \<in> Basis. ((\<lambda>x. (f x \<bullet> i)) \<longlongrightarrow> (l \<bullet> i)) F)"
(is "?lhs = ?rhs")
-proof%unimportant
+proof
assume ?lhs
then show ?rhs
unfolding tendsto_def
--- 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\<open>A difference from HOL Light: all summations over infinite sets equal zero,
so the "support" must be made explicit in the summation below!\<close>
-proposition%important subordinate_partition_of_unity:
+proposition subordinate_partition_of_unity:
fixes S :: "'a :: euclidean_space set"
assumes "S \<subseteq> \<Union>\<C>" and opC: "\<And>T. T \<in> \<C> \<Longrightarrow> open T"
and fin: "\<And>x. x \<in> S \<Longrightarrow> \<exists>V. open V \<and> x \<in> V \<and> finite {U \<in> \<C>. U \<inter> V \<noteq> {}}"
@@ -22,7 +22,7 @@
and "\<And>x U. \<lbrakk>U \<in> \<C>; x \<in> S; x \<notin> U\<rbrakk> \<Longrightarrow> F U x = 0"
and "\<And>x. x \<in> S \<Longrightarrow> supp_sum (\<lambda>W. F W x) \<C> = 1"
and "\<And>x. x \<in> S \<Longrightarrow> \<exists>V. open V \<and> x \<in> V \<and> finite {U \<in> \<C>. \<exists>x\<in>V. F U x \<noteq> 0}"
-proof%unimportant (cases "\<exists>W. W \<in> \<C> \<and> S \<subseteq> W")
+proof (cases "\<exists>W. W \<in> \<C> \<and> S \<subseteq> W")
case True
then obtain W where "W \<in> \<C>" "S \<subseteq> W" by metis
then show ?thesis
@@ -283,7 +283,7 @@
"\<And>x. f x = b \<longleftrightarrow> x \<in> 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 \<inter> T = {}"
@@ -292,7 +292,7 @@
"\<And>x. f x \<in> closed_segment a b"
"\<And>x. x \<in> S \<Longrightarrow> f x = a"
"\<And>x. x \<in> T \<Longrightarrow> 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\<open>The Dugundji extension theorem and Tietze variants as corollaries\<close>
@@ -300,14 +300,14 @@
text%important\<open>J. Dugundji. An extension of Tietze's theorem. Pacific J. Math. Volume 1, Number 3 (1951), 353-367.
https://projecteuclid.org/euclid.pjm/1103052106\<close>
-theorem%important Dugundji:
+theorem Dugundji:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_inner"
assumes "convex C" "C \<noteq> {}"
and cloin: "closedin (subtopology euclidean U) S"
and contf: "continuous_on S f" and "f ` S \<subseteq> C"
obtains g where "continuous_on U g" "g ` U \<subseteq> C"
"\<And>x. x \<in> S \<Longrightarrow> g x = f x"
-proof%unimportant (cases "S = {}")
+proof (cases "S = {}")
case True then show thesis
apply (rule_tac g="\<lambda>x. SOME y. y \<in> C" in that)
apply (rule continuous_intros)
@@ -475,7 +475,7 @@
qed
-corollary%important Tietze:
+corollary Tietze:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_inner"
assumes "continuous_on S f"
and "closedin (subtopology euclidean U) S"
@@ -483,7 +483,7 @@
and "\<And>x. x \<in> S \<Longrightarrow> norm(f x) \<le> B"
obtains g where "continuous_on U g" "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
"\<And>x. x \<in> U \<Longrightarrow> norm(g x) \<le> 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:
--- 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.
\<close>
-theorem%important real_non_denum: "\<nexists>f :: nat \<Rightarrow> real. surj f"
-proof%unimportant
+theorem real_non_denum: "\<nexists>f :: nat \<Rightarrow> real. surj f"
+proof
assume "\<exists>f::nat \<Rightarrow> real. surj f"
then obtain f :: "nat \<Rightarrow> real" where "surj f" ..
--- 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 \<in> 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 \<ge> 0 \<and> x \<in> S}"
+proposition cone_hull_expl: "cone hull S = {c *\<^sub>R x | c x. c \<ge> 0 \<and> x \<in> S}"
(is "?lhs = ?rhs")
-proof%unimportant -
+proof -
{
fix x
assume "x \<in> ?rhs"
@@ -2089,7 +2089,7 @@
"~ affine_dependent s \<Longrightarrow> ~ affine_dependent(s - t)"
by (meson Diff_subset affine_dependent_subset)
-proposition%important affine_dependent_explicit:
+proposition affine_dependent_explicit:
"affine_dependent p \<longleftrightarrow>
(\<exists>S u. finite S \<and> S \<subseteq> p \<and> sum u S = 0 \<and> (\<exists>v\<in>S. u v \<noteq> 0) \<and> sum (\<lambda>v. u v *\<^sub>R v) S = 0)"
proof -
@@ -2524,7 +2524,7 @@
subsubsection%unimportant \<open>Explicit expression for convex hull\<close>
-proposition%important convex_hull_indexed:
+proposition convex_hull_indexed:
fixes S :: "'a::real_vector set"
shows "convex hull S =
{y. \<exists>k u x. (\<forall>i\<in>{1::nat .. k}. 0 \<le> u i \<and> x i \<in> S) \<and>
@@ -4020,11 +4020,11 @@
by (auto simp: convex_hull_explicit)
qed
-theorem%important caratheodory:
+theorem caratheodory:
"convex hull p =
{x::'a::euclidean_space. \<exists>s. finite s \<and> s \<subseteq> p \<and>
card s \<le> DIM('a) + 1 \<and> x \<in> convex hull s}"
-proof%unimportant safe
+proof safe
fix x
assume "x \<in> convex hull p"
then obtain s u where "finite s" "s \<subseteq> p" "card s \<le> DIM('a) + 1"
@@ -5871,10 +5871,10 @@
done
qed
-theorem%important radon:
+theorem radon:
assumes "affine_dependent c"
obtains m p where "m \<subseteq> c" "p \<subseteq> c" "m \<inter> p = {}" "(convex hull m) \<inter> (convex hull p) \<noteq> {}"
-proof%unimportant -
+proof -
from assms[unfolded affine_dependent_explicit]
obtain s u where
"finite s" "s \<subseteq> c" "sum u s = 0" "\<exists>v\<in>s. u v \<noteq> 0" "(\<Sum>v\<in>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 \<ge> DIM('a) + 1" "\<forall>s\<in>f. convex s"
and "\<And>t. \<lbrakk>t\<subseteq>f; card t = DIM('a) + 1\<rbrakk> \<Longrightarrow> \<Inter>t \<noteq> {}"
shows "\<Inter>f \<noteq> {}"
- apply%unimportant (rule helly_induct)
+ apply (rule helly_induct)
using assms
apply auto
done
--- 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 (\<lambda>i. f i + g i) A \<le> L2_set f A + L2_set g A"
-proof %unimportant (cases "finite A")
+proof (cases "finite A")
case False
thus ?thesis by simp
next
--- 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 \<open>Archimedean properties and useful consequences\<close>
text\<open>Bernoulli's inequality\<close>
-proposition%important Bernoulli_inequality:
+proposition Bernoulli_inequality:
fixes x :: real
assumes "-1 \<le> x"
shows "1 + n * x \<le> (1 + x) ^ n"
-proof%unimportant (induct n)
+proof (induct n)
case 0
then show ?case by simp
next
--- 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 \<in> measurable M N \<Longrightarrow> A \<in> null_sets (distr M N f) \<longleftrightarrow> f -` A \<inter> space M \<in> null_sets M \<and> A \<in> sets N"
by (auto simp add: null_sets_def emeasure_distr)
-lemma%important distr_distr:
+proposition distr_distr:
"g \<in> measurable N L \<Longrightarrow> f \<in> measurable M N \<Longrightarrow> distr (distr M N f) L g = distr M L (g \<circ> 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 \<in> sets M"
and [simp]: "emeasure M A \<noteq> top" "emeasure N A \<noteq> top"
shows "\<exists>Y\<in>sets M. Y \<subseteq> A \<and> (\<forall>X\<in>sets M. X \<subseteq> Y \<longrightarrow> N X \<le> M X) \<and> (\<forall>X\<in>sets M. X \<subseteq> A \<longrightarrow> X \<inter> Y = {} \<longrightarrow> M X \<le> N X)"
-proof%unimportant -
+proof -
have "\<exists>Y\<in>sets (restrict_space M A).
(\<forall>X\<in>sets (restrict_space M A). X \<subseteq> Y \<longrightarrow> (restrict_space N A) X \<le> (restrict_space M A) X) \<and>
(\<forall>X\<in>sets (restrict_space M A). X \<inter> Y = {} \<longrightarrow> (restrict_space M A) X \<le> (restrict_space N A) X)"
@@ -2867,8 +2867,8 @@
end
-lemma%important le_measure: "sets M = sets N \<Longrightarrow> M \<le> N \<longleftrightarrow> (\<forall>A\<in>sets M. emeasure M A \<le> emeasure N A)"
- apply%unimportant -
+proposition le_measure: "sets M = sets N \<Longrightarrow> M \<le> N \<longleftrightarrow> (\<forall>A\<in>sets M. emeasure M A \<le> 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 \<in> sets M") (auto simp: emeasure_notin_sets)
--- 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 \<open>Hence more metric properties.\<close>
-lemma%important dist_triangle_add:
+proposition dist_triangle_add:
fixes x y x' y' :: "'a::real_normed_vector"
shows "dist (x + y) (x' + y') \<le> dist x x' + dist y y'"
by norm
--- 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 \<le> DIM('N::euclidean_space) \<Longrightarrow> 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 \<le> 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 \<le> DIM('N)"
shows "path_connected {x. r1 < norm(x - a) \<and> norm(x - a) < r2}"
"path_connected {x. r1 < norm(x - a) \<and> norm(x - a) \<le> r2}"
"path_connected {x. r1 \<le> norm(x - a) \<and> norm(x - a) < r2}"
"path_connected {x. r1 \<le> norm(x - a) \<and> norm(x - a) \<le> 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 \<le> DIM('N::euclidean_space)"
shows "connected {x. r1 < norm(x - a) \<and> norm(x - a) < r2}"
"connected {x. r1 < norm(x - a) \<and> norm(x - a) \<le> r2}"
"connected {x. r1 \<le> norm(x - a) \<and> norm(x - a) < r2}"
"connected {x. r1 \<le> norm(x - a) \<and> norm(x - a) \<le> 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\<open>Relations between components and path components\<close>
@@ -3302,14 +3302,14 @@
subsection\<open>Condition for an open map's image to contain a ball\<close>
-lemma%important ball_subset_open_map_image:
+proposition ball_subset_open_map_image:
fixes f :: "'a::heine_borel \<Rightarrow> 'b :: {real_normed_vector,heine_borel}"
assumes contf: "continuous_on (closure S) f"
and oint: "open (f ` interior S)"
and le_no: "\<And>z. z \<in> frontier S \<Longrightarrow> r \<le> norm(f z - f a)"
and "bounded S" "a \<in> S" "0 < r"
shows "ball (f a) r \<subseteq> 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\<open>So taking equivalence classes under homotopy would give the fundamental group\<close>
-proposition%important homotopic_paths_rid:
+proposition homotopic_paths_rid:
"\<lbrakk>path p; path_image p \<subseteq> s\<rbrakk> \<Longrightarrow> 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 = "\<lambda>t. if t \<le> 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:
"\<lbrakk>path p; path_image p \<subseteq> s\<rbrakk> \<Longrightarrow> 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:
"\<lbrakk>path p; path_image p \<subseteq> s; path q; path_image q \<subseteq> s; path r; path_image r \<subseteq> s; pathfinish p = pathstart q;
pathfinish q = pathstart r\<rbrakk>
\<Longrightarrow> 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 = "\<lambda>t. if t \<le> 1 / 2 then inverse 2 *\<^sub>R t
else if t \<le> 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 \<subseteq> s"
shows "homotopic_paths s (p +++ reversepath p) (linepath (pathstart p) (pathstart p))"
-proof%unimportant -
+proof -
have "continuous_on ({0..1} \<times> {0..1}) (\<lambda>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 \<subseteq> 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\<open>Homotopy of loops without requiring preservation of endpoints\<close>
@@ -3994,14 +3994,14 @@
subsection\<open>Relations between the two variants of homotopy\<close>
-proposition%important homotopic_paths_imp_homotopic_loops:
+proposition homotopic_paths_imp_homotopic_loops:
"\<lbrakk>homotopic_paths s p q; pathfinish p = pathstart p; pathfinish q = pathstart p\<rbrakk> \<Longrightarrow> 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 \<subseteq> 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 \<subseteq> s" and piq: "path_image q \<subseteq> 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 \<open>path p\<close> [unfolded path_def] by blast
have contq: "continuous_on {0..1} q" using \<open>path q\<close> [unfolded path_def] by blast
have c1: "continuous_on ({0..1} \<times> {0..1}) (\<lambda>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:
"\<lbrakk>path g; path_image g \<subseteq> s; u \<in> {0..1}; v \<in> {0..1}; w \<in> {0..1}\<rbrakk>
\<Longrightarrow> 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\<open>Relating homotopy of trivial loops to path-connectedness.\<close>
@@ -5043,7 +5043,7 @@
subsection\<open>Sort of induction principle for connected sets\<close>
-lemma%important connected_induction:
+proposition connected_induction:
assumes "connected S"
and opD: "\<And>T a. \<lbrakk>openin (subtopology euclidean S) T; a \<in> T\<rbrakk> \<Longrightarrow> \<exists>z. z \<in> T \<and> P z"
and opI: "\<And>a. a \<in> S
@@ -5051,7 +5051,7 @@
(\<forall>x \<in> T. \<forall>y \<in> T. P x \<and> P y \<and> Q x \<longrightarrow> Q y)"
and etc: "a \<in> S" "b \<in> S" "P a" "P b" "Q a"
shows "Q b"
-proof%unimportant -
+proof -
have 1: "openin (subtopology euclidean S)
{b. \<exists>T. openin (subtopology euclidean S) T \<and>
b \<in> T \<and> (\<forall>x\<in>T. P x \<longrightarrow> Q x)}"
@@ -5142,14 +5142,14 @@
subsection\<open>Basic properties of local compactness\<close>
-lemma%important locally_compact:
+proposition locally_compact:
fixes s :: "'a :: metric_space set"
shows
"locally compact s \<longleftrightarrow>
(\<forall>x \<in> s. \<exists>u v. x \<in> u \<and> u \<subseteq> v \<and> v \<subseteq> s \<and>
openin (subtopology euclidean s) u \<and> compact v)"
(is "?lhs = ?rhs")
-proof%unimportant
+proof
assume ?lhs
then show ?rhs
apply clarify
@@ -5696,12 +5696,12 @@
by (metis \<open>U = S \<inter> V\<close> 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 \<in> components S" "compact C"
shows "C = \<Inter> {K. C \<subseteq> K \<and> compact K \<and> openin (subtopology euclidean S) K}"
(is "C = ?rhs")
-proof%unimportant
+proof
show "?rhs \<subseteq> 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 \<longleftrightarrow>
(\<forall>v x. openin (subtopology euclidean S) v \<and> x \<in> v
\<longrightarrow> (\<exists>u. openin (subtopology euclidean S) u \<and> path_connected u \<and> x \<in> u \<and> u \<subseteq> 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 \<longleftrightarrow>
(\<forall>t x. openin (subtopology euclidean S) t \<and> x \<in> t
\<longrightarrow> 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 \<longleftrightarrow>
@@ -5849,14 +5849,14 @@
\<longrightarrow> 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 \<longleftrightarrow>
(\<forall>v x. openin (subtopology euclidean S) v \<and> x \<in> v
\<longrightarrow> (\<exists>u. openin (subtopology euclidean S) u \<and>
x \<in> u \<and> u \<subseteq> v \<and>
(\<forall>y. y \<in> u \<longrightarrow> (\<exists>c. connected c \<and> c \<subseteq> v \<and> x \<in> c \<and> y \<in> 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 \<longleftrightarrow>
(\<forall>v x. openin (subtopology euclidean S) v \<and> x \<in> v
\<longrightarrow> (\<exists>u. openin (subtopology euclidean S) u \<and>
@@ -5898,7 +5898,7 @@
(\<forall>y. y \<in> u \<longrightarrow> (\<exists>p. path p \<and> path_image p \<subseteq> v \<and>
pathstart p = x \<and> 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 \<Longrightarrow> 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: "\<And>T. T \<subseteq> f ` S
\<Longrightarrow> openin (subtopology euclidean S) (S \<inter> f -` T) \<longleftrightarrow>
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 \<in> components U"
then have "C \<subseteq> U" "U \<subseteq> f ` S"
@@ -6114,12 +6114,12 @@
qed
text\<open>The proof resembles that above but is not identical!\<close>
-proposition%important locally_path_connected_quotient_image:
+proposition locally_path_connected_quotient_image:
assumes lcS: "locally path_connected S"
and oo: "\<And>T. T \<subseteq> f ` S
\<Longrightarrow> openin (subtopology euclidean S) (S \<inter> f -` T) \<longleftrightarrow> 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 \<in> U"
then have "path_component_set U y \<subseteq> U" "U \<subseteq> f ` S"
@@ -6345,7 +6345,7 @@
by (rule that [OF \<open>linear f\<close> \<open>f ` S \<subseteq> T\<close>])
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 @@
"\<And>x. x \<in> T \<Longrightarrow> norm(g x) = norm x"
"\<And>x. x \<in> S \<Longrightarrow> g(f x) = x"
"\<And>x. x \<in> T \<Longrightarrow> f(g x) = x"
-proof%unimportant -
+proof -
obtain B where "B \<subseteq> S" and Borth: "pairwise orthogonal B"
and B1: "\<And>x. x \<in> B \<Longrightarrow> 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 \<le> DIM('a)" "open S" "connected S" "S \<subseteq> T" "finite K"
and KS: "\<And>i. i \<in> K \<Longrightarrow> x i \<in> S \<and> y i \<in> S"
@@ -7823,7 +7823,7 @@
and S: "S \<subseteq> T" "T \<subseteq> affine hull S" "connected S"
obtains f g where "homeomorphism T T f g" "\<And>i. i \<in> K \<Longrightarrow> f(x i) = y i"
"{x. ~ (f x = x \<and> g x = x)} \<subseteq> S" "bounded {x. (~ (f x = x \<and> 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 \<noteq> {}" "finite K" "K \<subseteq> S" "U \<subseteq> S" "S \<subseteq> T"
obtains f g where "homeomorphism T T f g" "{x. (~ (f x = x \<and> g x = x))} \<subseteq> S"
"bounded {x. (~ (f x = x \<and> g x = x))}" "\<And>x. x \<in> K \<Longrightarrow> f x \<in> U"
-proof%unimportant (cases "2 \<le> DIM('a)")
+proof (cases "2 \<le> DIM('a)")
case True
have TS: "T \<subseteq> 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 \<Rightarrow> 'a::real_normed_vector"
shows "(\<exists>c. homotopic_with (\<lambda>x. True) (sphere a r) S f (\<lambda>x. c)) \<longleftrightarrow>
(\<exists>g. continuous_on (cball a r) g \<and> g ` (cball a r) \<subseteq> S \<and>
(\<forall>x \<in> 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)
--- 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 \<open>Pair operations are linear\<close>
-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 \<open>Frechet derivatives involving pairs\<close>
-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 "((\<lambda>x. (f x, g x)) has_derivative (\<lambda>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 (\<lambda>h. (f' h, g' h))"
using f g by (intro bounded_linear_Pair has_derivative_bounded_linear)
let ?Rf = "\<lambda>y. f y - f x - f' (y - x)"
--- 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 \<in> M \<Longrightarrow> \<Omega> - a \<in> M"
by auto
-lemma%important algebra_iff_Un:
+proposition algebra_iff_Un:
"algebra \<Omega> M \<longleftrightarrow>
M \<subseteq> Pow \<Omega> \<and>
{} \<in> M \<and>
(\<forall>a \<in> M. \<Omega> - a \<in> M) \<and>
(\<forall>a \<in> M. \<forall> b \<in> M. a \<union> b \<in> M)" (is "_ \<longleftrightarrow> ?Un")
-proof%unimportant
+proof
assume "algebra \<Omega> M"
then interpret algebra \<Omega> M .
show ?Un using sets_into_space by auto
@@ -173,12 +173,12 @@
show "algebra \<Omega> M" proof qed fact
qed
-lemma%important algebra_iff_Int:
+proposition algebra_iff_Int:
"algebra \<Omega> M \<longleftrightarrow>
M \<subseteq> Pow \<Omega> & {} \<in> M &
(\<forall>a \<in> M. \<Omega> - a \<in> M) &
(\<forall>a \<in> M. \<forall> b \<in> M. a \<inter> b \<in> M)" (is "_ \<longleftrightarrow> ?Int")
-proof%unimportant
+proof
assume "algebra \<Omega> M"
then interpret algebra \<Omega> M .
show ?Int using sets_into_space by auto
@@ -1433,7 +1433,7 @@
text%important \<open>The reason to introduce Dynkin-systems is the following induction rules for $\sigma$-algebras
generated by a generator closed under intersection.\<close>
-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 \<subseteq> Pow \<Omega>"
and A: "A \<in> sigma_sets \<Omega> G"
@@ -1442,7 +1442,7 @@
and compl: "\<And>A. A \<in> sigma_sets \<Omega> G \<Longrightarrow> P A \<Longrightarrow> P (\<Omega> - A)"
and union: "\<And>A. disjoint_family A \<Longrightarrow> range A \<subseteq> sigma_sets \<Omega> G \<Longrightarrow> (\<And>i. P (A i)) \<Longrightarrow> P (\<Union>i::nat. A i)"
shows "P A"
-proof%unimportant -
+proof -
let ?D = "{ A \<in> sigma_sets \<Omega> G. P A }"
interpret sigma_algebra \<Omega> "sigma_sets \<Omega> G"
using closed by (rule sigma_algebra_sigma_sets)
@@ -1633,12 +1633,12 @@
subsubsection \<open>Constructing simple @{typ "'a measure"}\<close>
-lemma%important emeasure_measure_of:
+proposition emeasure_measure_of:
assumes M: "M = measure_of \<Omega> A \<mu>"
assumes ms: "A \<subseteq> Pow \<Omega>" "positive (sets M) \<mu>" "countably_additive (sets M) \<mu>"
assumes X: "X \<in> sets M"
shows "emeasure M X = \<mu> X"
-proof%unimportant -
+proof -
interpret sigma_algebra \<Omega> "sigma_sets \<Omega> A" by (rule sigma_algebra_sigma_sets) fact
have "measure_space \<Omega> (sigma_sets \<Omega> A) \<mu>"
using ms M by (simp add: measure_space_def sigma_algebra_sigma_sets)
--- 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\<open>Connectedness of the intersection of a chain\<close>
-proposition%important connected_chain:
+proposition connected_chain:
fixes \<F> :: "'a :: euclidean_space set set"
assumes cc: "\<And>S. S \<in> \<F> \<Longrightarrow> compact S \<and> connected S"
and linear: "\<And>S T. S \<in> \<F> \<and> T \<in> \<F> \<Longrightarrow> S \<subseteq> T \<or> T \<subseteq> S"
shows "connected(\<Inter>\<F>)"
-proof%unimportant (cases "\<F> = {}")
+proof (cases "\<F> = {}")
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 \<Rightarrow> 'b::heine_borel"
assumes "closedin (subtopology euclidean S) K"
and com: "\<And>U. \<lbrakk>U \<subseteq> T; compact U\<rbrakk> \<Longrightarrow> compact (S \<inter> f -` U)"
and "f ` S \<subseteq> T"
shows "closedin (subtopology euclidean T) (f ` K)"
-proof%unimportant -
+proof -
have "K \<subseteq> S"
using assms closedin_imp_subset by metis
obtain C where "closed C" and Keq: "K = S \<inter> 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 \<in> span S"
shows "orthogonal x (a - (\<Sum>b\<in>S. (b \<bullet> a / (b \<bullet> b)) *\<^sub>R b))"
-proof%unimportant -
+proof -
have "finite S"
by (simp add: S pairwise_orthogonal_imp_finite)
have "orthogonal (a - (\<Sum>b\<in>S. (b \<bullet> a / (b \<bullet> 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 \<union> U)" "span (S \<union> U) = span (S \<union> 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 \<subseteq> S" "pairwise orthogonal B"
and "\<And>x. x \<in> B \<Longrightarrow> norm x = 1"
and "independent B" "card B = dim S" "span B = S"
-proof%unimportant -
+proof -
obtain B where "0 \<notin> B" "B \<subseteq> 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 \<subset> span T"
obtains x where "x \<noteq> 0" "x \<in> span T" "\<And>y. y \<in> span S \<Longrightarrow> orthogonal x y"
-proof%unimportant -
+proof -
obtain B where "B \<subseteq> span S" and orthB: "pairwise orthogonal B"
and "\<And>x. x \<in> B \<Longrightarrow> 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 \<in> span S" "\<And>w. w \<in> span S \<Longrightarrow> orthogonal z w" "x = y + z"
-proof%unimportant -
+proof -
obtain T where "0 \<notin> T" "T \<subseteq> 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 "\<And>x y. \<lbrakk>x \<in> A; y \<in> B\<rbrakk> \<Longrightarrow> x \<bullet> y = 0"
shows "dim(A \<union> B) = dim A + dim B"
-proof%unimportant -
+proof -
have 1: "\<And>x y. \<lbrakk>x \<in> span A; y \<in> B\<rbrakk> \<Longrightarrow> x \<bullet> y = 0"
by (erule span_induct [OF _ subspace_hyperplane2]; simp add: assms)
have "\<And>x y. \<lbrakk>x \<in> span A; y \<in> span B\<rbrakk> \<Longrightarrow> x \<bullet> y = 0"
@@ -7163,10 +7163,10 @@
subsection\<open>Lower-dimensional affine subsets are nowhere dense\<close>
-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 \<subseteq> S" for U
proof -
have "span U \<subset> span S"
@@ -7465,7 +7465,7 @@
subsection\<open>Several Variants of Paracompactness\<close>
-proposition%important paracompact:
+proposition paracompact:
fixes S :: "'a :: euclidean_space set"
assumes "S \<subseteq> \<Union>\<C>" and opC: "\<And>T. T \<in> \<C> \<Longrightarrow> open T"
obtains \<C>' where "S \<subseteq> \<Union> \<C>'"
@@ -7473,7 +7473,7 @@
and "\<And>x. x \<in> S
\<Longrightarrow> \<exists>V. open V \<and> x \<in> V \<and>
finite {U. U \<in> \<C>' \<and> (U \<inter> V \<noteq> {})}"
-proof%unimportant (cases "S = {}")
+proof (cases "S = {}")
case True with that show ?thesis by blast
next
case False
@@ -7858,14 +7858,14 @@
subsection\<open>Covering an open set by a countable chain of compact sets\<close>
-proposition%important open_Union_compact_subsets:
+proposition open_Union_compact_subsets:
fixes S :: "'a::euclidean_space set"
assumes "open S"
obtains C where "\<And>n. compact(C n)" "\<And>n. C n \<subseteq> S"
"\<And>n. C n \<subseteq> interior(C(Suc n))"
"\<Union>(range C) = S"
"\<And>K. \<lbrakk>compact K; K \<subseteq> S\<rbrakk> \<Longrightarrow> \<exists>N. \<forall>n\<ge>N. K \<subseteq> (C n)"
-proof%unimportant (cases "S = {}")
+proof (cases "S = {}")
case True
then show ?thesis
by (rule_tac C = "\<lambda>n. {}" in that) auto
--- 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 \<open>Main properties of open sets\<close>
-lemma%important openin_clauses:
+proposition openin_clauses:
fixes U :: "'a topology"
shows
"openin U {}"
@@ -2765,16 +2765,16 @@
subsection \<open>Limits\<close>
-lemma%important Lim: "(f \<longlongrightarrow> l) net \<longleftrightarrow> trivial_limit net \<or> (\<forall>e>0. eventually (\<lambda>x. dist (f x) l < e) net)"
+proposition Lim: "(f \<longlongrightarrow> l) net \<longleftrightarrow> trivial_limit net \<or> (\<forall>e>0. eventually (\<lambda>x. dist (f x) l < e) net)"
by (auto simp: tendsto_iff trivial_limit_eq)
text \<open>Show that they yield usual definitions in the various cases.\<close>
-lemma%important Lim_within_le: "(f \<longlongrightarrow> l)(at a within S) \<longleftrightarrow>
+proposition Lim_within_le: "(f \<longlongrightarrow> l)(at a within S) \<longleftrightarrow>
(\<forall>e>0. \<exists>d>0. \<forall>x\<in>S. 0 < dist x a \<and> dist x a \<le> d \<longrightarrow> dist (f x) l < e)"
by (auto simp: tendsto_iff eventually_at_le)
-lemma%important Lim_within: "(f \<longlongrightarrow> l) (at a within S) \<longleftrightarrow>
+proposition Lim_within: "(f \<longlongrightarrow> l) (at a within S) \<longleftrightarrow>
(\<forall>e >0. \<exists>d>0. \<forall>x \<in> S. 0 < dist x a \<and> dist x a < d \<longrightarrow> 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 \<longlongrightarrow> l) (at a) \<longleftrightarrow>
+proposition Lim_at: "(f \<longlongrightarrow> l) (at a) \<longleftrightarrow>
(\<forall>e >0. \<exists>d>0. \<forall>x. 0 < dist x a \<and> dist x a < d \<longrightarrow> dist (f x) l < e)"
by (auto simp: tendsto_iff eventually_at)
-lemma%important Lim_at_infinity: "(f \<longlongrightarrow> l) at_infinity \<longleftrightarrow> (\<forall>e>0. \<exists>b. \<forall>x. norm x \<ge> b \<longrightarrow> dist (f x) l < e)"
+proposition Lim_at_infinity: "(f \<longlongrightarrow> l) at_infinity \<longleftrightarrow> (\<forall>e>0. \<exists>b. \<forall>x. norm x \<ge> b \<longrightarrow> dist (f x) l < e)"
by (auto simp: tendsto_iff eventually_at_infinity)
corollary Lim_at_infinityI [intro?]:
@@ -3652,12 +3652,12 @@
subsubsection \<open>Bolzano-Weierstrass property\<close>
-lemma%important heine_borel_imp_bolzano_weierstrass:
+proposition heine_borel_imp_bolzano_weierstrass:
assumes "compact s"
and "infinite t"
and "t \<subseteq> s"
shows "\<exists>x \<in> s. x islimpt t"
-proof%unimportant (rule ccontr)
+proof (rule ccontr)
assume "\<not> (\<exists>x \<in> s. x islimpt t)"
then obtain f where f: "\<forall>x\<in>s. x \<in> f x \<and> open (f x) \<and> (\<forall>y\<in>t. y \<in> f x \<longrightarrow> 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 \<Longrightarrow> 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 \<in> T"
from topological_basisE[OF is_basis this] obtain b where
@@ -4448,10 +4448,10 @@
shows "seq_compact U \<longleftrightarrow> 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 "\<forall>t. infinite t \<and> t \<subseteq> s \<longrightarrow> (\<exists>x \<in> s. x islimpt t) \<Longrightarrow> 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\<open>Totally bounded\<close>
@@ -4459,10 +4459,10 @@
lemma cauchy_def: "Cauchy s \<longleftrightarrow> (\<forall>e>0. \<exists>N. \<forall>m n. m \<ge> N \<and> n \<ge> N \<longrightarrow> 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 "\<forall>e>0. \<exists>k. finite k \<and> k \<subseteq> s \<and> s \<subseteq> (\<Union>x\<in>k. ball x e)"
-proof%unimportant -
+proof -
{ fix e::real assume "e > 0" assume *: "\<And>k. finite k \<Longrightarrow> k \<subseteq> s \<Longrightarrow> \<not> s \<subseteq> (\<Union>x\<in>k. ball x e)"
let ?Q = "\<lambda>x n r. r \<in> s \<and> (\<forall>m < (n::nat). \<not> (dist (x m) r < e))"
have "\<exists>x. \<forall>n::nat. ?Q x n (x n)"
@@ -4491,11 +4491,11 @@
subsubsection\<open>Heine-Borel theorem\<close>
-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 \<open>seq_compact s\<close>]
obtain f where f: "\<forall>e>0. finite (f e) \<and> f e \<subseteq> s \<and> s \<subseteq> (\<Union>x\<in>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) \<longleftrightarrow> seq_compact s"
using compact_imp_seq_compact seq_compact_imp_heine_borel by blast
-lemma%important compact_def: \<comment> \<open>this is the definition of compactness in HOL Light\<close>
+proposition compact_def: \<comment> \<open>this is the definition of compactness in HOL Light\<close>
"compact (S :: 'a::metric_space set) \<longleftrightarrow>
(\<forall>f. (\<forall>n. f n \<in> S) \<longrightarrow> (\<exists>l\<in>S. \<exists>r::nat\<Rightarrow>nat. strict_mono r \<and> (f \<circ> r) \<longlonglongrightarrow> l))"
unfolding compact_eq_seq_compact_metric seq_compact_def by auto
subsubsection \<open>Complete the chain of compactness variants\<close>
-lemma%important compact_eq_bolzano_weierstrass:
+proposition compact_eq_bolzano_weierstrass:
fixes s :: "'a::metric_space set"
shows "compact s \<longleftrightarrow> (\<forall>t. infinite t \<and> t \<subseteq> s --> (\<exists>x \<in> 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:
"\<forall>t. infinite t \<and> t \<subseteq> s \<longrightarrow> (\<exists>x \<in> s. x islimpt t) \<Longrightarrow> bounded s"
using compact_imp_bounded unfolding compact_eq_bolzano_weierstrass .
@@ -4577,12 +4577,12 @@
assumes bounded_imp_convergent_subsequence:
"bounded (range f) \<Longrightarrow> \<exists>l r. strict_mono (r::nat\<Rightarrow>nat) \<and> ((f \<circ> r) \<longlongrightarrow> 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 \<Rightarrow> 'a"
assume f: "\<forall>n. f n \<in> s"
with \<open>bounded s\<close> have "bounded (range f)"
@@ -4807,12 +4807,12 @@
subsubsection \<open>Completeness\<close>
-lemma%important (in metric_space) completeI:
+proposition (in metric_space) completeI:
assumes "\<And>f. \<forall>n. f n \<in> s \<Longrightarrow> Cauchy f \<Longrightarrow> \<exists>l\<in>s. f \<longlonglongrightarrow> 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 "\<forall>n. f n \<in> s" and "Cauchy f"
obtains l where "l \<in> s" and "f \<longlonglongrightarrow> 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 \<longleftrightarrow> complete s \<and> (\<forall>e>0. \<exists>k. finite k \<and> s \<subseteq> (\<Union>x\<in>k. ball x e))"
(is "_ \<longleftrightarrow> ?rhs")
-proof%unimportant
+proof
assume assms: "?rhs"
then obtain k where k: "\<And>e. 0 < e \<Longrightarrow> finite (k e)" "\<And>e. 0 < e \<Longrightarrow> s \<subseteq> (\<Union>x\<in>k e. ball x e)"
by (auto simp: choice_iff')
@@ -5069,7 +5069,7 @@
text\<open>Derive the epsilon-delta forms, which we often use as "definitions"\<close>
-lemma%important continuous_within_eps_delta:
+proposition continuous_within_eps_delta:
"continuous (at x within s) f \<longleftrightarrow> (\<forall>e>0. \<exists>d>0. \<forall>x'\<in> s. dist x' x < d --> dist (f x') (f x) < e)"
unfolding continuous_within and Lim_within by fastforce
--- 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"