# HG changeset patch
# User immler
# Date 1546107673 0
# Node ID b9b7a5e2472ea38de1d850abf05bc2d01ce0742c
# Parent  da2726f78610c3b58fad0951239cb32ea5f37c58# Parent  d466e0a639e4dc7b5f53d3100a25f2a4d26b1fb3
merged

diff -r da2726f78610 -r b9b7a5e2472e src/HOL/Analysis/Measure_Space.thy
--- a/src/HOL/Analysis/Measure_Space.thy	Sat Dec 29 18:45:57 2018 +0100
+++ b/src/HOL/Analysis/Measure_Space.thy	Sat Dec 29 18:21:13 2018 +0000
@@ -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
diff -r da2726f78610 -r b9b7a5e2472e src/HOL/Analysis/Product_Vector.thy
--- a/src/HOL/Analysis/Product_Vector.thy	Sat Dec 29 18:45:57 2018 +0100
+++ b/src/HOL/Analysis/Product_Vector.thy	Sat Dec 29 18:21:13 2018 +0000
@@ -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 -
diff -r da2726f78610 -r b9b7a5e2472e src/HOL/Analysis/Starlike.thy
--- a/src/HOL/Analysis/Starlike.thy	Sat Dec 29 18:45:57 2018 +0100
+++ b/src/HOL/Analysis/Starlike.thy	Sat Dec 29 18:21:13 2018 +0000
@@ -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")