--- a/src/HOL/Analysis/Measure_Space.thy Sat Dec 29 17:38:29 2018 +0100
+++ b/src/HOL/Analysis/Measure_Space.thy Sat Dec 29 17:46:48 2018 +0100
@@ -1749,7 +1749,7 @@
using emeasure_mono[of "a - b" a M] * by (auto simp: fmeasurable_def)
qed
-subsection\<open>Measurable sets formed by unions and intersections\<close>
+subsection%unimportant\<open>Measurable sets formed by unions and intersections\<close>
lemma fmeasurable_Diff: "A \<in> fmeasurable M \<Longrightarrow> B \<in> sets M \<Longrightarrow> A - B \<in> fmeasurable M"
using fmeasurableI2[of A M "A - B"] by auto
--- a/src/HOL/Analysis/Product_Vector.thy Sat Dec 29 17:38:29 2018 +0100
+++ b/src/HOL/Analysis/Product_Vector.thy Sat Dec 29 17:46:48 2018 +0100
@@ -16,17 +16,17 @@
by force
-subsection \<open>Product is a module\<close>
+subsection \<open>Product is a Module\<close>
locale module_prod = module_pair begin
definition scale :: "'a \<Rightarrow> 'b \<times> 'c \<Rightarrow> 'b \<times> 'c"
where "scale a v = (s1 a (fst v), s2 a (snd v))"
-lemma scale_prod: "scale x (a, b) = (s1 x a, s2 x b)"
+lemma%important scale_prod: "scale x (a, b) = (s1 x a, s2 x b)"
by (auto simp: scale_def)
-sublocale p: module scale
+sublocale%important p: module scale
proof qed (simp_all add: scale_def
m1.scale_left_distrib m1.scale_right_distrib m2.scale_left_distrib m2.scale_right_distrib)
@@ -56,7 +56,7 @@
end
-subsection \<open>Product is a real vector space\<close>
+subsection \<open>Product is a Real Vector Space\<close>
instantiation prod :: (real_vector, real_vector) real_vector
begin
@@ -70,7 +70,7 @@
lemma snd_scaleR [simp]: "snd (scaleR r A) = scaleR r (snd A)"
unfolding scaleR_prod_def by simp
-lemma scaleR_Pair [simp]: "scaleR r (a, b) = (scaleR r a, scaleR r b)"
+proposition scaleR_Pair [simp]: "scaleR r (a, b) = (scaleR r a, scaleR r b)"
unfolding scaleR_prod_def by simp
instance
@@ -109,20 +109,20 @@
extend_basis_raw_def dim_raw_def linear_def
by (rule refl)+
-subsection \<open>Product is a metric space\<close>
+subsection \<open>Product is a Metric Space\<close>
(* TODO: Product of uniform spaces and compatibility with metric_spaces! *)
-instantiation prod :: (metric_space, metric_space) dist
+instantiation%unimportant prod :: (metric_space, metric_space) dist
begin
-definition%important dist_prod_def[code del]:
+definition dist_prod_def[code del]:
"dist x y = sqrt ((dist (fst x) (fst y))\<^sup>2 + (dist (snd x) (snd y))\<^sup>2)"
instance ..
end
-instantiation prod :: (metric_space, metric_space) uniformity_dist
+instantiation%unimportant prod :: (metric_space, metric_space) uniformity_dist
begin
definition [code del]:
@@ -138,7 +138,7 @@
instantiation prod :: (metric_space, metric_space) metric_space
begin
-lemma dist_Pair_Pair: "dist (a, b) (c, d) = sqrt ((dist a c)\<^sup>2 + (dist b d)\<^sup>2)"
+proposition dist_Pair_Pair: "dist (a, b) (c, d) = sqrt ((dist a c)\<^sup>2 + (dist b d)\<^sup>2)"
unfolding dist_prod_def by simp
lemma dist_fst_le: "dist (fst x) (fst y) \<le> dist x y"
@@ -251,7 +251,7 @@
then show "\<exists>n0. \<forall>m\<ge>n0. \<forall>n\<ge>n0. dist (X m, Y m) (X n, Y n) < r" ..
qed
-subsection \<open>Product is a complete metric space\<close>
+subsection \<open>Product is a Complete Metric Space\<close>
instance%important prod :: (complete_space, complete_space) complete_space
proof%unimportant
@@ -268,7 +268,7 @@
by (rule convergentI)
qed
-subsection \<open>Product is a normed vector space\<close>
+subsection \<open>Product is a Normed Vector Space\<close>
instantiation prod :: (real_normed_vector, real_normed_vector) real_normed_vector
begin
@@ -279,7 +279,7 @@
definition sgn_prod_def:
"sgn (x::'a \<times> 'b) = scaleR (inverse (norm x)) x"
-lemma norm_Pair: "norm (a, b) = sqrt ((norm a)\<^sup>2 + (norm b)\<^sup>2)"
+proposition norm_Pair: "norm (a, b) = sqrt ((norm a)\<^sup>2 + (norm b)\<^sup>2)"
unfolding norm_prod_def by simp
instance
@@ -310,15 +310,15 @@
declare [[code abort: "norm::('a::real_normed_vector*'b::real_normed_vector) \<Rightarrow> real"]]
-instance prod :: (banach, banach) banach ..
+instance%important prod :: (banach, banach) banach ..
subsubsection%unimportant \<open>Pair operations are linear\<close>
-proposition bounded_linear_fst: "bounded_linear fst"
+lemma bounded_linear_fst: "bounded_linear fst"
using fst_add fst_scaleR
by (rule bounded_linear_intro [where K=1], simp add: norm_prod_def)
-proposition bounded_linear_snd: "bounded_linear snd"
+lemma bounded_linear_snd: "bounded_linear snd"
using snd_add snd_scaleR
by (rule bounded_linear_intro [where K=1], simp add: norm_prod_def)
@@ -355,7 +355,8 @@
subsubsection%unimportant \<open>Frechet derivatives involving pairs\<close>
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)"
+ 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 (rule has_derivativeI_sandwich[of 1])
show "bounded_linear (\<lambda>h. (f' h, g' h))"
@@ -455,6 +456,8 @@
qed
done
+subsection \<open>Product is Finite Dimensional\<close>
+
lemma (in finite_dimensional_vector_space) zero_not_in_Basis[simp]: "0 \<notin> Basis"
using dependent_zero local.independent_Basis by blast
@@ -492,7 +495,7 @@
Basis_pair_def)
qed
-lemma dim_Times:
+proposition dim_Times:
assumes "vs1.subspace S" "vs2.subspace T"
shows "p.dim(S \<times> T) = vs1.dim S + vs2.dim T"
proof -
--- a/src/HOL/Analysis/Starlike.thy Sat Dec 29 17:38:29 2018 +0100
+++ b/src/HOL/Analysis/Starlike.thy Sat Dec 29 17:46:48 2018 +0100
@@ -4979,7 +4979,7 @@
subsection%unimportant\<open>Use set distance for an easy proof of separation properties\<close>
-proposition separation_closures:
+proposition%unimportant separation_closures:
fixes S :: "'a::euclidean_space set"
assumes "S \<inter> closure T = {}" "T \<inter> closure S = {}"
obtains U V where "U \<inter> V = {}" "open U" "open V" "S \<subseteq> U" "T \<subseteq> V"
@@ -5525,7 +5525,7 @@
subsubsection%unimportant\<open>Representing affine hull as a finite intersection of hyperplanes\<close>
-proposition affine_hull_convex_Int_nonempty_interior:
+proposition%unimportant affine_hull_convex_Int_nonempty_interior:
fixes S :: "'a::real_normed_vector set"
assumes "convex S" "S \<inter> interior T \<noteq> {}"
shows "affine hull (S \<inter> T) = affine hull S"
@@ -5696,7 +5696,7 @@
(if a = 0 \<and> r > 0 then -1 else DIM('a))"
using aff_dim_halfspace_le [of "-a" "-r"] by simp
-subsection%unimportant\<open>Properties of special hyperplanes\<close>
+subsection\<open>Properties of special hyperplanes\<close>
lemma subspace_hyperplane: "subspace {x. a \<bullet> x = 0}"
by (simp add: subspace_def inner_right_distrib)
@@ -5973,7 +5973,7 @@
subsection%unimportant\<open>General case without assuming closure and getting non-strict separation\<close>
-proposition separating_hyperplane_closed_point_inset:
+proposition%unimportant separating_hyperplane_closed_point_inset:
fixes S :: "'a::euclidean_space set"
assumes "convex S" "closed S" "S \<noteq> {}" "z \<notin> S"
obtains a b where "a \<in> S" "(a - z) \<bullet> z < b" "\<And>x. x \<in> S \<Longrightarrow> b < (a - z) \<bullet> x"
@@ -6010,7 +6010,7 @@
by simp (metis \<open>0 \<notin> S\<close>)
-proposition separating_hyperplane_set_0_inspan:
+proposition%unimportant separating_hyperplane_set_0_inspan:
fixes S :: "'a::euclidean_space set"
assumes "convex S" "S \<noteq> {}" "0 \<notin> S"
obtains a where "a \<in> span S" "a \<noteq> 0" "\<And>x. x \<in> S \<Longrightarrow> 0 \<le> a \<bullet> x"
@@ -6101,7 +6101,7 @@
done
qed
-proposition supporting_hyperplane_rel_boundary:
+proposition%unimportant supporting_hyperplane_rel_boundary:
fixes S :: "'a::euclidean_space set"
assumes "convex S" "x \<in> S" and xno: "x \<notin> rel_interior S"
obtains a where "a \<noteq> 0"
@@ -6204,7 +6204,7 @@
qed
-proposition affine_hull_Int:
+proposition%unimportant affine_hull_Int:
fixes s :: "'a::euclidean_space set"
assumes "\<not> affine_dependent(s \<union> t)"
shows "affine hull (s \<inter> t) = affine hull s \<inter> affine hull t"
@@ -6212,7 +6212,7 @@
apply (simp add: hull_mono)
by (simp add: affine_hull_Int_subset assms)
-proposition convex_hull_Int:
+proposition%unimportant convex_hull_Int:
fixes s :: "'a::euclidean_space set"
assumes "\<not> affine_dependent(s \<union> t)"
shows "convex hull (s \<inter> t) = convex hull s \<inter> convex hull t"
@@ -6220,7 +6220,7 @@
apply (simp add: hull_mono)
by (simp add: convex_hull_Int_subset assms)
-proposition
+proposition%unimportant
fixes s :: "'a::euclidean_space set set"
assumes "\<not> affine_dependent (\<Union>s)"
shows affine_hull_Inter: "affine hull (\<Inter>s) = (\<Inter>t\<in>s. affine hull t)" (is "?A")
@@ -6250,7 +6250,7 @@
by auto
qed
-proposition in_convex_hull_exchange_unique:
+proposition%unimportant in_convex_hull_exchange_unique:
fixes S :: "'a::euclidean_space set"
assumes naff: "\<not> affine_dependent S" and a: "a \<in> convex hull S"
and S: "T \<subseteq> S" "T' \<subseteq> S"
@@ -6398,7 +6398,7 @@
qed
qed
-corollary convex_hull_exchange_Int:
+corollary%unimportant convex_hull_exchange_Int:
fixes a :: "'a::euclidean_space"
assumes "\<not> affine_dependent S" "a \<in> convex hull S" "T \<subseteq> S" "T' \<subseteq> S"
shows "(convex hull (insert a T)) \<inter> (convex hull (insert a T')) =
@@ -6551,7 +6551,7 @@
by (simp add: subs) (metis (lifting) span_eq_iff subs)
qed
-proposition affine_hyperplane_sums_eq_UNIV:
+proposition%unimportant affine_hyperplane_sums_eq_UNIV:
fixes S :: "'a :: euclidean_space set"
assumes "affine S"
and "S \<inter> {v. a \<bullet> v = b} \<noteq> {}"
@@ -6786,7 +6786,7 @@
by (rule_tac U=U in that) (auto simp: span_Un)
qed
-corollary orthogonal_extension_strong:
+corollary%unimportant orthogonal_extension_strong:
fixes S :: "'a::euclidean_space set"
assumes S: "pairwise orthogonal S"
obtains U where "U \<inter> (insert 0 S) = {}" "pairwise orthogonal (S \<union> U)"
@@ -6869,7 +6869,7 @@
qed
-proposition orthogonal_to_subspace_exists_gen:
+proposition%unimportant 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"
@@ -6915,7 +6915,7 @@
qed
qed
-corollary orthogonal_to_subspace_exists:
+corollary%unimportant orthogonal_to_subspace_exists:
fixes S :: "'a :: euclidean_space set"
assumes "dim S < DIM('a)"
obtains x where "x \<noteq> 0" "\<And>y. y \<in> span S \<Longrightarrow> orthogonal x y"
@@ -6927,7 +6927,7 @@
by (auto simp: span_UNIV)
qed
-corollary orthogonal_to_vector_exists:
+corollary%unimportant orthogonal_to_vector_exists:
fixes x :: "'a :: euclidean_space"
assumes "2 \<le> DIM('a)"
obtains y where "y \<noteq> 0" "orthogonal x y"
@@ -6938,9 +6938,12 @@
by (rule orthogonal_to_subspace_exists) (simp add: orthogonal_commute span_base that)
qed
-proposition orthogonal_subspace_decomp_exists:
+proposition%unimportant 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"
+ obtains y z
+ where "y \<in> span S"
+ and "\<And>w. w \<in> span S \<Longrightarrow> orthogonal z w"
+ and "x = y + z"
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"
@@ -7223,7 +7226,7 @@
by force
qed
-corollary dense_complement_affine:
+corollary%unimportant dense_complement_affine:
fixes S :: "'a :: euclidean_space set"
assumes less: "aff_dim T < aff_dim S" and "affine S" shows "closure(S - T) = S"
proof (cases "S \<inter> T = {}")
@@ -7243,7 +7246,7 @@
by (metis closure_translation translation_diff translation_invert)
qed
-corollary dense_complement_openin_affine_hull:
+corollary%unimportant dense_complement_openin_affine_hull:
fixes S :: "'a :: euclidean_space set"
assumes less: "aff_dim T < aff_dim S"
and ope: "openin (subtopology euclidean (affine hull S)) S"
@@ -7257,7 +7260,7 @@
by (metis Int_Diff aff_dim_affine_hull affine_affine_hull dense_complement_affine hull_subset inf.orderE less)
qed
-corollary dense_complement_convex:
+corollary%unimportant dense_complement_convex:
fixes S :: "'a :: euclidean_space set"
assumes "aff_dim T < aff_dim S" "convex S"
shows "closure(S - T) = closure S"
@@ -7272,7 +7275,7 @@
by (metis Diff_mono \<open>convex S\<close> closure_mono convex_closure_rel_interior order_refl rel_interior_subset)
qed
-corollary dense_complement_convex_closed:
+corollary%unimportant dense_complement_convex_closed:
fixes S :: "'a :: euclidean_space set"
assumes "aff_dim T < aff_dim S" "convex S" "closed S"
shows "closure(S - T) = S"
@@ -7284,7 +7287,7 @@
text\<open> If we take a slice out of a set, we can do it perpendicularly,
with the normal vector to the slice parallel to the affine hull.\<close>
-proposition affine_parallel_slice:
+proposition%unimportant affine_parallel_slice:
fixes S :: "'a :: euclidean_space set"
assumes "affine S"
and "S \<inter> {x. a \<bullet> x \<le> b} \<noteq> {}"
@@ -7468,7 +7471,7 @@
by (rule that)
qed
-subsection\<open>Several Variants of Paracompactness\<close>
+subsection\<open>Paracompactness\<close>
proposition paracompact:
fixes S :: "'a :: euclidean_space set"
@@ -7602,7 +7605,7 @@
qed
qed
-corollary paracompact_closed:
+corollary%unimportant paracompact_closed:
fixes S :: "'a :: euclidean_space set"
assumes "closed S"
and opC: "\<And>T. T \<in> \<C> \<Longrightarrow> open T"
@@ -7687,7 +7690,7 @@
subsection%unimportant\<open>The union of two collinear segments is another segment\<close>
-proposition in_convex_hull_exchange:
+proposition%unimportant in_convex_hull_exchange:
fixes a :: "'a::euclidean_space"
assumes a: "a \<in> convex hull S" and xS: "x \<in> convex hull S"
obtains b where "b \<in> S" "x \<in> convex hull (insert a (S - {b}))"
@@ -7964,10 +7967,10 @@
subsection\<open>Orthogonal complement\<close>
-definition orthogonal_comp ("_\<^sup>\<bottom>" [80] 80)
+definition%important orthogonal_comp ("_\<^sup>\<bottom>" [80] 80)
where "orthogonal_comp W \<equiv> {x. \<forall>y \<in> W. orthogonal y x}"
-lemma subspace_orthogonal_comp: "subspace (W\<^sup>\<bottom>)"
+proposition subspace_orthogonal_comp: "subspace (W\<^sup>\<bottom>)"
unfolding subspace_def orthogonal_comp_def orthogonal_def
by (auto simp: inner_right_distrib)
@@ -8002,7 +8005,7 @@
by (meson assms subsetCE subspace_add)
qed
-lemma subspace_sum_orthogonal_comp:
+proposition subspace_sum_orthogonal_comp:
fixes U :: "'a :: euclidean_space set"
assumes "subspace U"
shows "U + U\<^sup>\<bottom> = UNIV"
@@ -8080,7 +8083,7 @@
apply (simp add: adjoint_works assms(1) inner_commute)
by (metis adjoint_works all_zero_iff assms(1) inner_commute)
-subsection\<open> A non-injective linear function maps into a hyperplane.\<close>
+subsection%unimportant \<open>A non-injective linear function maps into a hyperplane.\<close>
lemma linear_surj_adj_imp_inj:
fixes f :: "'m::euclidean_space \<Rightarrow> 'n::euclidean_space"
@@ -8139,7 +8142,7 @@
by (simp add: \<open>surj f\<close> adjoint_adjoint adjoint_linear assms linear_surj_adj_imp_inj)
qed
-proposition linear_singular_into_hyperplane:
+lemma linear_singular_into_hyperplane:
fixes f :: "'n::euclidean_space \<Rightarrow> 'n"
assumes "linear f"
shows "\<not> inj f \<longleftrightarrow> (\<exists>a. a \<noteq> 0 \<and> (\<forall>x. a \<bullet> f x = 0))" (is "_ = ?rhs")