a first shot at tagging for HOL-Analysis manual
authorimmler
Fri Apr 06 17:34:50 2018 +0200 (13 months ago)
changeset 679620acdcd8f4ba1
parent 67961 9c31678d2139
child 67963 9541f2c5ce8d
a first shot at tagging for HOL-Analysis manual
src/HOL/Analysis/Cartesian_Euclidean_Space.thy
src/HOL/Analysis/Connected.thy
src/HOL/Analysis/Continuous_Extension.thy
src/HOL/Analysis/Continuum_Not_Denumerable.thy
src/HOL/Analysis/Convex_Euclidean_Space.thy
src/HOL/Analysis/Euclidean_Space.thy
src/HOL/Analysis/Inner_Product.thy
src/HOL/Analysis/Linear_Algebra.thy
src/HOL/Analysis/Measurable.thy
src/HOL/Analysis/Measure_Space.thy
src/HOL/Analysis/Norm_Arith.thy
src/HOL/Analysis/Path_Connected.thy
src/HOL/Analysis/Product_Vector.thy
src/HOL/Analysis/Sigma_Algebra.thy
src/HOL/Analysis/Starlike.thy
src/HOL/Analysis/Topology_Euclidean_Space.thy
     1.1 --- a/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Thu Apr 05 06:15:02 2018 +0000
     1.2 +++ b/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Fri Apr 06 17:34:50 2018 +0200
     1.3 @@ -468,6 +468,12 @@
     1.4  
     1.5  text\<open>Matrix notation. NB: an MxN matrix is of type @{typ "'a^'n^'m"}, not @{typ "'a^'m^'n"}\<close>
     1.6  
     1.7 +definition map_matrix::"('a \<Rightarrow> 'b) \<Rightarrow> (('a, 'i::finite)vec, 'j::finite) vec \<Rightarrow> (('b, 'i)vec, 'j) vec" where
     1.8 +  "map_matrix f x = (\<chi> i j. f (x $ i $ j))"
     1.9 +
    1.10 +lemma nth_map_matrix[simp]: "map_matrix f x $ i $ j = f (x $ i $ j)"
    1.11 +  by (simp add: map_matrix_def)
    1.12 +
    1.13  definition matrix_matrix_mult :: "('a::semiring_1) ^'n^'m \<Rightarrow> 'a ^'p^'n \<Rightarrow> 'a ^ 'p ^'m"
    1.14      (infixl "**" 70)
    1.15    where "m ** m' == (\<chi> i j. sum (\<lambda>k. ((m$i)$k) * ((m'$k)$j)) (UNIV :: 'n set)) ::'a ^ 'p ^'m"
     2.1 --- a/src/HOL/Analysis/Connected.thy	Thu Apr 05 06:15:02 2018 +0000
     2.2 +++ b/src/HOL/Analysis/Connected.thy	Fri Apr 06 17:34:50 2018 +0200
     2.3 @@ -8,7 +8,7 @@
     2.4  imports Topology_Euclidean_Space
     2.5  begin
     2.6  
     2.7 -subsection \<open>More properties of closed balls, spheres, etc.\<close>
     2.8 +subsection%unimportant \<open>More properties of closed balls, spheres, etc.\<close>
     2.9  
    2.10  lemma mem_interior_cball: "x \<in> interior S \<longleftrightarrow> (\<exists>e>0. cball x e \<subseteq> S)"
    2.11    apply (simp add: interior_def, safe)
    2.12 @@ -345,7 +345,7 @@
    2.13    shows "closed (sphere a r)"
    2.14  by (simp add: compact_imp_closed)
    2.15  
    2.16 -subsection \<open>Connectedness\<close>
    2.17 +subsection%unimportant \<open>Connectedness\<close>
    2.18  
    2.19  lemma connected_local:
    2.20   "connected S \<longleftrightarrow>
    2.21 @@ -410,7 +410,7 @@
    2.22  
    2.23  subsection \<open>Connected components, considered as a connectedness relation or a set\<close>
    2.24  
    2.25 -definition "connected_component s x y \<equiv> \<exists>t. connected t \<and> t \<subseteq> s \<and> x \<in> t \<and> y \<in> t"
    2.26 +definition%important "connected_component s x y \<equiv> \<exists>t. connected t \<and> t \<subseteq> s \<and> x \<in> t \<and> y \<in> t"
    2.27  
    2.28  abbreviation "connected_component_set s x \<equiv> Collect (connected_component s x)"
    2.29  
    2.30 @@ -610,7 +610,7 @@
    2.31  
    2.32  subsection \<open>The set of connected components of a set\<close>
    2.33  
    2.34 -definition components:: "'a::topological_space set \<Rightarrow> 'a set set"
    2.35 +definition%important components:: "'a::topological_space set \<Rightarrow> 'a set set"
    2.36    where "components s \<equiv> connected_component_set s ` s"
    2.37  
    2.38  lemma components_iff: "s \<in> components u \<longleftrightarrow> (\<exists>x. x \<in> u \<and> s = connected_component_set u x)"
    2.39 @@ -776,12 +776,12 @@
    2.40  
    2.41  subsection \<open>Intersecting chains of compact sets and the Baire property\<close>
    2.42  
    2.43 -proposition bounded_closed_chain:
    2.44 +proposition%important bounded_closed_chain:
    2.45    fixes \<F> :: "'a::heine_borel set set"
    2.46    assumes "B \<in> \<F>" "bounded B" and \<F>: "\<And>S. S \<in> \<F> \<Longrightarrow> closed S" and "{} \<notin> \<F>"
    2.47        and chain: "\<And>S T. S \<in> \<F> \<and> T \<in> \<F> \<Longrightarrow> S \<subseteq> T \<or> T \<subseteq> S"
    2.48      shows "\<Inter>\<F> \<noteq> {}"
    2.49 -proof -
    2.50 +proof%unimportant -
    2.51    have "B \<inter> \<Inter>\<F> \<noteq> {}"
    2.52    proof (rule compact_imp_fip)
    2.53      show "compact B" "\<And>T. T \<in> \<F> \<Longrightarrow> closed T"
    2.54 @@ -824,12 +824,12 @@
    2.55    then show ?thesis by blast
    2.56  qed
    2.57  
    2.58 -corollary compact_chain:
    2.59 +corollary%important compact_chain:
    2.60    fixes \<F> :: "'a::heine_borel set set"
    2.61    assumes "\<And>S. S \<in> \<F> \<Longrightarrow> compact S" "{} \<notin> \<F>"
    2.62            "\<And>S T. S \<in> \<F> \<and> T \<in> \<F> \<Longrightarrow> S \<subseteq> T \<or> T \<subseteq> S"
    2.63      shows "\<Inter> \<F> \<noteq> {}"
    2.64 -proof (cases "\<F> = {}")
    2.65 +proof%unimportant (cases "\<F> = {}")
    2.66    case True
    2.67    then show ?thesis by auto
    2.68  next
    2.69 @@ -852,12 +852,12 @@
    2.70  qed
    2.71  
    2.72  text\<open>The Baire property of dense sets\<close>
    2.73 -theorem Baire:
    2.74 +theorem%important Baire:
    2.75    fixes S::"'a::{real_normed_vector,heine_borel} set"
    2.76    assumes "closed S" "countable \<G>"
    2.77        and ope: "\<And>T. T \<in> \<G> \<Longrightarrow> openin (subtopology euclidean S) T \<and> S \<subseteq> closure T"
    2.78   shows "S \<subseteq> closure(\<Inter>\<G>)"
    2.79 -proof (cases "\<G> = {}")
    2.80 +proof%unimportant (cases "\<G> = {}")
    2.81    case True
    2.82    then show ?thesis
    2.83      using closure_subset by auto
    2.84 @@ -961,7 +961,7 @@
    2.85    qed
    2.86  qed
    2.87  
    2.88 -subsection\<open>Some theorems on sups and infs using the notion "bounded".\<close>
    2.89 +subsection%unimportant \<open>Some theorems on sups and infs using the notion "bounded".\<close>
    2.90  
    2.91  lemma bounded_real: "bounded (S::real set) \<longleftrightarrow> (\<exists>a. \<forall>x\<in>S. \<bar>x\<bar> \<le> a)"
    2.92    by (simp add: bounded_iff)
    2.93 @@ -1139,7 +1139,7 @@
    2.94  qed
    2.95  
    2.96  
    2.97 -subsection\<open>Relations among convergence and absolute convergence for power series.\<close>
    2.98 +subsection%unimportant\<open>Relations among convergence and absolute convergence for power series.\<close>
    2.99  
   2.100  lemma summable_imp_bounded:
   2.101    fixes f :: "nat \<Rightarrow> 'a::real_normed_vector"
   2.102 @@ -1166,7 +1166,7 @@
   2.103      done
   2.104  qed
   2.105  
   2.106 -subsection \<open>Bounded closed nest property (proof does not use Heine-Borel)\<close>
   2.107 +subsection%unimportant \<open>Bounded closed nest property (proof does not use Heine-Borel)\<close>
   2.108  
   2.109  lemma bounded_closed_nest:
   2.110    fixes s :: "nat \<Rightarrow> ('a::heine_borel) set"
   2.111 @@ -1286,7 +1286,7 @@
   2.112  
   2.113  subsection \<open>Infimum Distance\<close>
   2.114  
   2.115 -definition "infdist x A = (if A = {} then 0 else INF a:A. dist x a)"
   2.116 +definition%important "infdist x A = (if A = {} then 0 else INF a:A. dist x a)"
   2.117  
   2.118  lemma bdd_below_image_dist[intro, simp]: "bdd_below (dist x ` A)"
   2.119    by (auto intro!: zero_le_dist)
   2.120 @@ -1515,7 +1515,7 @@
   2.121      by (simp add: compact_eq_bounded_closed)
   2.122  qed
   2.123  
   2.124 -subsection \<open>Equality of continuous functions on closure and related results.\<close>
   2.125 +subsection%unimportant \<open>Equality of continuous functions on closure and related results.\<close>
   2.126  
   2.127  lemma continuous_closedin_preimage_constant:
   2.128    fixes f :: "_ \<Rightarrow> 'b::t1_space"
   2.129 @@ -1618,7 +1618,7 @@
   2.130    qed
   2.131  qed
   2.132  
   2.133 -subsection \<open>A function constant on a set\<close>
   2.134 +subsection%unimportant \<open>A function constant on a set\<close>
   2.135  
   2.136  definition constant_on  (infixl "(constant'_on)" 50)
   2.137    where "f constant_on A \<equiv> \<exists>y. \<forall>x\<in>A. f x = y"
   2.138 @@ -1639,7 +1639,7 @@
   2.139  using continuous_constant_on_closure [OF contf] cof unfolding constant_on_def
   2.140  by metis
   2.141  
   2.142 -subsection\<open>Relating linear images to open/closed/interior/closure\<close>
   2.143 +subsection%unimportant\<open>Relating linear images to open/closed/interior/closure\<close>
   2.144  
   2.145  proposition open_surjective_linear_image:
   2.146    fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::euclidean_space"
   2.147 @@ -1786,7 +1786,7 @@
   2.148    qed
   2.149  qed
   2.150  
   2.151 -subsection\<open> Theorems relating continuity and uniform continuity to closures\<close>
   2.152 +subsection%unimportant\<open> Theorems relating continuity and uniform continuity to closures\<close>
   2.153  
   2.154  lemma continuous_on_closure:
   2.155     "continuous_on (closure S) f \<longleftrightarrow>
   2.156 @@ -2047,7 +2047,7 @@
   2.157    shows "bounded(f ` S)"
   2.158    by (metis (no_types, lifting) assms bounded_closure_image compact_closure compact_continuous_image compact_eq_bounded_closed image_cong uniformly_continuous_imp_continuous uniformly_continuous_on_extension_on_closure)
   2.159  
   2.160 -subsection \<open>Making a continuous function avoid some value in a neighbourhood.\<close>
   2.161 +subsection%unimportant \<open>Making a continuous function avoid some value in a neighbourhood.\<close>
   2.162  
   2.163  lemma continuous_within_avoid:
   2.164    fixes f :: "'a::metric_space \<Rightarrow> 'b::t1_space"
   2.165 @@ -2097,7 +2097,7 @@
   2.166    using continuous_at_avoid[of x f a] assms(4)
   2.167    by auto
   2.168  
   2.169 -subsection\<open>Quotient maps\<close>
   2.170 +subsection%unimportant\<open>Quotient maps\<close>
   2.171  
   2.172  lemma quotient_map_imp_continuous_open:
   2.173    assumes T: "f ` S \<subseteq> T"
   2.174 @@ -2447,15 +2447,15 @@
   2.175    ultimately show ?thesis using that by blast
   2.176  qed
   2.177  
   2.178 -corollary compact_uniformly_continuous:
   2.179 +corollary%important compact_uniformly_continuous:
   2.180    fixes f :: "'a :: metric_space \<Rightarrow> 'b :: metric_space"
   2.181    assumes f: "continuous_on S f" and S: "compact S"
   2.182    shows "uniformly_continuous_on S f"
   2.183 -  using f
   2.184 +  using%unimportant f
   2.185      unfolding continuous_on_iff uniformly_continuous_on_def
   2.186      by (force intro: compact_uniformly_equicontinuous [OF S, of "{f}"])
   2.187  
   2.188 -subsection \<open>Topological stuff about the set of Reals\<close>
   2.189 +subsection%unimportant \<open>Topological stuff about the set of Reals\<close>
   2.190  
   2.191  lemma open_real:
   2.192    fixes s :: "real set"
   2.193 @@ -2492,7 +2492,7 @@
   2.194    unfolding continuous_on_iff dist_norm by simp
   2.195  
   2.196  
   2.197 -subsection \<open>Cartesian products\<close>
   2.198 +subsection%unimportant \<open>Cartesian products\<close>
   2.199  
   2.200  lemma bounded_Times:
   2.201    assumes "bounded s" "bounded t"
   2.202 @@ -2668,7 +2668,7 @@
   2.203  
   2.204  subsection \<open>The diameter of a set.\<close>
   2.205  
   2.206 -definition diameter :: "'a::metric_space set \<Rightarrow> real" where
   2.207 +definition%important diameter :: "'a::metric_space set \<Rightarrow> real" where
   2.208    "diameter S = (if S = {} then 0 else SUP (x,y):S\<times>S. dist x y)"
   2.209  
   2.210  lemma diameter_empty [simp]: "diameter{} = 0"
   2.211 @@ -2933,11 +2933,11 @@
   2.212  
   2.213  subsection \<open>Separation between points and sets\<close>
   2.214  
   2.215 -lemma separate_point_closed:
   2.216 +lemma%important separate_point_closed:
   2.217    fixes s :: "'a::heine_borel set"
   2.218    assumes "closed s" and "a \<notin> s"
   2.219    shows "\<exists>d>0. \<forall>x\<in>s. d \<le> dist a x"
   2.220 -proof (cases "s = {}")
   2.221 +proof%unimportant (cases "s = {}")
   2.222    case True
   2.223    then show ?thesis by(auto intro!: exI[where x=1])
   2.224  next
   2.225 @@ -2948,12 +2948,12 @@
   2.226      by blast
   2.227  qed
   2.228  
   2.229 -lemma separate_compact_closed:
   2.230 +lemma%important separate_compact_closed:
   2.231    fixes s t :: "'a::heine_borel set"
   2.232    assumes "compact s"
   2.233      and t: "closed t" "s \<inter> t = {}"
   2.234    shows "\<exists>d>0. \<forall>x\<in>s. \<forall>y\<in>t. d \<le> dist x y"
   2.235 -proof cases
   2.236 +proof%unimportant cases
   2.237    assume "s \<noteq> {} \<and> t \<noteq> {}"
   2.238    then have "s \<noteq> {}" "t \<noteq> {}" by auto
   2.239    let ?inf = "\<lambda>x. infdist x t"
   2.240 @@ -2968,27 +2968,27 @@
   2.241    ultimately show ?thesis by auto
   2.242  qed (auto intro!: exI[of _ 1])
   2.243  
   2.244 -lemma separate_closed_compact:
   2.245 +lemma%important separate_closed_compact:
   2.246    fixes s t :: "'a::heine_borel set"
   2.247    assumes "closed s"
   2.248      and "compact t"
   2.249      and "s \<inter> t = {}"
   2.250    shows "\<exists>d>0. \<forall>x\<in>s. \<forall>y\<in>t. d \<le> dist x y"
   2.251 -proof -
   2.252 +proof%unimportant -
   2.253    have *: "t \<inter> s = {}"
   2.254      using assms(3) by auto
   2.255    show ?thesis
   2.256      using separate_compact_closed[OF assms(2,1) *] by (force simp: dist_commute)
   2.257  qed
   2.258  
   2.259 -lemma compact_in_open_separated:
   2.260 +lemma%important compact_in_open_separated:
   2.261    fixes A::"'a::heine_borel set"
   2.262    assumes "A \<noteq> {}"
   2.263    assumes "compact A"
   2.264    assumes "open B"
   2.265    assumes "A \<subseteq> B"
   2.266    obtains e where "e > 0" "{x. infdist x A \<le> e} \<subseteq> B"
   2.267 -proof atomize_elim
   2.268 +proof%unimportant atomize_elim
   2.269    have "closed (- B)" "compact A" "- B \<inter> A = {}"
   2.270      using assms by (auto simp: open_Diff compact_eq_bounded_closed)
   2.271    from separate_closed_compact[OF this]
   2.272 @@ -3014,7 +3014,7 @@
   2.273  qed
   2.274  
   2.275  
   2.276 -subsection \<open>Compact sets and the closure operation.\<close>
   2.277 +subsection%unimportant \<open>Compact sets and the closure operation.\<close>
   2.278  
   2.279  lemma closed_scaling:
   2.280    fixes S :: "'a::real_normed_vector set"
   2.281 @@ -3165,7 +3165,7 @@
   2.282  done
   2.283  
   2.284  
   2.285 -subsection \<open>Closure of halfspaces and hyperplanes\<close>
   2.286 +subsection%unimportant \<open>Closure of halfspaces and hyperplanes\<close>
   2.287  
   2.288  lemma continuous_on_closed_Collect_le:
   2.289    fixes f g :: "'a::t2_space \<Rightarrow> real"
   2.290 @@ -3492,7 +3492,7 @@
   2.291  
   2.292  subsection \<open>Homeomorphisms\<close>
   2.293  
   2.294 -definition "homeomorphism s t f g \<longleftrightarrow>
   2.295 +definition%important "homeomorphism s t f g \<longleftrightarrow>
   2.296    (\<forall>x\<in>s. (g(f x) = x)) \<and> (f ` s = t) \<and> continuous_on s f \<and>
   2.297    (\<forall>y\<in>t. (f(g y) = y)) \<and> (g ` t = s) \<and> continuous_on t g"
   2.298  
   2.299 @@ -3812,7 +3812,7 @@
   2.300  using assms unfolding homeomorphic_def homeomorphism_def by (metis connected_continuous_image)
   2.301  
   2.302  
   2.303 -subsection\<open>Inverse function property for open/closed maps\<close>
   2.304 +subsection%unimportant\<open>Inverse function property for open/closed maps\<close>
   2.305  
   2.306  lemma continuous_on_inverse_open_map:
   2.307    assumes contf: "continuous_on S f"
   2.308 @@ -3963,12 +3963,12 @@
   2.309      unfolding complete_def by auto
   2.310  qed
   2.311  
   2.312 -lemma injective_imp_isometric:
   2.313 +lemma%important injective_imp_isometric:
   2.314    fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   2.315    assumes s: "closed s" "subspace s"
   2.316      and f: "bounded_linear f" "\<forall>x\<in>s. f x = 0 \<longrightarrow> x = 0"
   2.317    shows "\<exists>e>0. \<forall>x\<in>s. norm (f x) \<ge> e * norm x"
   2.318 -proof (cases "s \<subseteq> {0::'a}")
   2.319 +proof%unimportant (cases "s \<subseteq> {0::'a}")
   2.320    case True
   2.321    have "norm x \<le> norm (f x)" if "x \<in> s" for x
   2.322    proof -
   2.323 @@ -4036,11 +4036,11 @@
   2.324    ultimately show ?thesis by auto
   2.325  qed
   2.326  
   2.327 -lemma closed_injective_image_subspace:
   2.328 +lemma%important closed_injective_image_subspace:
   2.329    fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   2.330    assumes "subspace s" "bounded_linear f" "\<forall>x\<in>s. f x = 0 \<longrightarrow> x = 0" "closed s"
   2.331    shows "closed(f ` s)"
   2.332 -proof -
   2.333 +proof%unimportant -
   2.334    obtain e where "e > 0" and e: "\<forall>x\<in>s. e * norm x \<le> norm (f x)"
   2.335      using injective_imp_isometric[OF assms(4,1,2,3)] by auto
   2.336    show ?thesis
   2.337 @@ -4049,7 +4049,7 @@
   2.338  qed
   2.339  
   2.340  
   2.341 -subsection \<open>Some properties of a canonical subspace\<close>
   2.342 +subsection%unimportant \<open>Some properties of a canonical subspace\<close>
   2.343  
   2.344  lemma subspace_substandard: "subspace {x::'a::euclidean_space. (\<forall>i\<in>Basis. P i \<longrightarrow> x\<bullet>i = 0)}"
   2.345    by (auto simp: subspace_def inner_add_left)
   2.346 @@ -4157,7 +4157,7 @@
   2.347  qed
   2.348  
   2.349  
   2.350 -subsection \<open>Affine transformations of intervals\<close>
   2.351 +subsection%unimportant \<open>Affine transformations of intervals\<close>
   2.352  
   2.353  lemma real_affinity_le: "0 < m \<Longrightarrow> m * x + c \<le> y \<longleftrightarrow> x \<le> inverse m * y + - (c / m)"
   2.354    for m :: "'a::linordered_field"
   2.355 @@ -4186,13 +4186,13 @@
   2.356  
   2.357  subsection \<open>Banach fixed point theorem (not really topological ...)\<close>
   2.358  
   2.359 -theorem banach_fix:
   2.360 +theorem%important banach_fix:
   2.361    assumes s: "complete s" "s \<noteq> {}"
   2.362      and c: "0 \<le> c" "c < 1"
   2.363      and f: "f ` s \<subseteq> s"
   2.364      and lipschitz: "\<forall>x\<in>s. \<forall>y\<in>s. dist (f x) (f y) \<le> c * dist x y"
   2.365    shows "\<exists>!x\<in>s. f x = x"
   2.366 -proof -
   2.367 +proof%unimportant -
   2.368    from c have "1 - c > 0" by simp
   2.369  
   2.370    from s(2) obtain z0 where z0: "z0 \<in> s" by blast
   2.371 @@ -4342,13 +4342,13 @@
   2.372  
   2.373  subsection \<open>Edelstein fixed point theorem\<close>
   2.374  
   2.375 -theorem edelstein_fix:
   2.376 +theorem%important edelstein_fix:
   2.377    fixes s :: "'a::metric_space set"
   2.378    assumes s: "compact s" "s \<noteq> {}"
   2.379      and gs: "(g ` s) \<subseteq> s"
   2.380      and dist: "\<forall>x\<in>s. \<forall>y\<in>s. x \<noteq> y \<longrightarrow> dist (g x) (g y) < dist x y"
   2.381    shows "\<exists>!x\<in>s. g x = x"
   2.382 -proof -
   2.383 +proof%unimportant -
   2.384    let ?D = "(\<lambda>x. (x, x)) ` s"
   2.385    have D: "compact ?D" "?D \<noteq> {}"
   2.386      by (rule compact_continuous_image)
   2.387 @@ -4697,10 +4697,10 @@
   2.388      done
   2.389  qed
   2.390  
   2.391 -proposition separable:
   2.392 +proposition%important separable:
   2.393    fixes S :: "'a:: euclidean_space set"
   2.394    obtains T where "countable T" "T \<subseteq> S" "S \<subseteq> closure T"
   2.395 -proof -
   2.396 +proof%unimportant -
   2.397    obtain \<B> :: "'a:: euclidean_space set set"
   2.398      where "countable \<B>"
   2.399        and "{} \<notin> \<B>"
   2.400 @@ -4743,11 +4743,11 @@
   2.401    qed
   2.402  qed
   2.403  
   2.404 -proposition Lindelof:
   2.405 +proposition%important Lindelof:
   2.406    fixes \<F> :: "'a::euclidean_space set set"
   2.407    assumes \<F>: "\<And>S. S \<in> \<F> \<Longrightarrow> open S"
   2.408    obtains \<F>' where "\<F>' \<subseteq> \<F>" "countable \<F>'" "\<Union>\<F>' = \<Union>\<F>"
   2.409 -proof -
   2.410 +proof%unimportant -
   2.411    obtain \<B> :: "'a set set"
   2.412      where "countable \<B>" "\<And>C. C \<in> \<B> \<Longrightarrow> open C"
   2.413        and \<B>: "\<And>S. open S \<Longrightarrow> \<exists>U. U \<subseteq> \<B> \<and> S = \<Union>U"
   2.414 @@ -5049,11 +5049,11 @@
   2.415  qed
   2.416  
   2.417  
   2.418 -proposition component_diff_connected:
   2.419 +proposition%important component_diff_connected:
   2.420    fixes S :: "'a::metric_space set"
   2.421    assumes "connected S" "connected U" "S \<subseteq> U" and C: "C \<in> components (U - S)"
   2.422    shows "connected(U - C)"
   2.423 -  using \<open>connected S\<close> unfolding connected_closedin_eq not_ex de_Morgan_conj
   2.424 +  using%unimportant \<open>connected S\<close> unfolding connected_closedin_eq not_ex de_Morgan_conj
   2.425  proof clarify
   2.426    fix H3 H4 
   2.427    assume clo3: "closedin (subtopology euclidean (U - C)) H3" 
   2.428 @@ -5093,7 +5093,7 @@
   2.429      by auto
   2.430  qed
   2.431  
   2.432 -subsection\<open> Finite intersection property\<close>
   2.433 +subsection%unimportant\<open> Finite intersection property\<close>
   2.434  
   2.435  text\<open>Also developed in HOL's toplogical spaces theory, but the Heine-Borel type class isn't available there.\<close>
   2.436  
   2.437 @@ -5149,7 +5149,7 @@
   2.438  by (simp add: closed_limpt islimpt_insert sequence_unique_limpt)
   2.439  
   2.440  
   2.441 -subsection\<open>Componentwise limits and continuity\<close>
   2.442 +subsection%unimportant\<open>Componentwise limits and continuity\<close>
   2.443  
   2.444  text\<open>But is the premise really necessary? Need to generalise @{thm euclidean_dist_l2}\<close>
   2.445  lemma Euclidean_dist_upper: "i \<in> Basis \<Longrightarrow> dist (x \<bullet> i) (y \<bullet> i) \<le> dist x y"
   2.446 @@ -5179,11 +5179,11 @@
   2.447      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)
   2.448  qed
   2.449  
   2.450 -proposition tendsto_componentwise_iff:
   2.451 +proposition%important tendsto_componentwise_iff:
   2.452    fixes f :: "_ \<Rightarrow> 'b::euclidean_space"
   2.453    shows "(f \<longlongrightarrow> l) F \<longleftrightarrow> (\<forall>i \<in> Basis. ((\<lambda>x. (f x \<bullet> i)) \<longlongrightarrow> (l \<bullet> i)) F)"
   2.454           (is "?lhs = ?rhs")
   2.455 -proof
   2.456 +proof%unimportant
   2.457    assume ?lhs
   2.458    then show ?rhs
   2.459      unfolding tendsto_def
   2.460 @@ -5267,9 +5267,9 @@
   2.461      by (force simp: bounded_linear_def bounded_linear_axioms_def \<open>linear f'\<close>)
   2.462  qed
   2.463  
   2.464 -subsection\<open>Pasting functions together\<close>
   2.465 -
   2.466 -subsubsection\<open>on open sets\<close>
   2.467 +subsection%unimportant\<open>Pasting functions together\<close>
   2.468 +
   2.469 +subsubsection%unimportant\<open>on open sets\<close>
   2.470  
   2.471  lemma pasting_lemma:
   2.472    fixes f :: "'i \<Rightarrow> 'a::topological_space \<Rightarrow> 'b::topological_space"
   2.473 @@ -5311,7 +5311,7 @@
   2.474      by (metis (no_types, lifting) IntD2 IntI f someI_ex)
   2.475  qed
   2.476  
   2.477 -subsubsection\<open>Likewise on closed sets, with a finiteness assumption\<close>
   2.478 +subsubsection%unimportant\<open>Likewise on closed sets, with a finiteness assumption\<close>
   2.479  
   2.480  lemma pasting_lemma_closed:
   2.481    fixes f :: "'i \<Rightarrow> 'a::topological_space \<Rightarrow> 'b::topological_space"
   2.482 @@ -5436,7 +5436,7 @@
   2.483  qed
   2.484  
   2.485  
   2.486 -subsection\<open>Constancy of a function from a connected set into a finite, disconnected or discrete set\<close>
   2.487 +subsection%unimportant\<open>Constancy of a function from a connected set into a finite, disconnected or discrete set\<close>
   2.488  
   2.489  text\<open>Still missing: versions for a set that is smaller than R, or countable.\<close>
   2.490  
   2.491 @@ -5595,7 +5595,7 @@
   2.492  
   2.493  
   2.494  
   2.495 -subsection \<open>Continuous Extension\<close>
   2.496 +subsection%unimportant \<open>Continuous Extension\<close>
   2.497  
   2.498  definition clamp :: "'a::euclidean_space \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a" where
   2.499    "clamp a b x = (if (\<forall>i\<in>Basis. a \<bullet> i \<le> b \<bullet> i)
     3.1 --- a/src/HOL/Analysis/Continuous_Extension.thy	Thu Apr 05 06:15:02 2018 +0000
     3.2 +++ b/src/HOL/Analysis/Continuous_Extension.thy	Fri Apr 06 17:34:50 2018 +0200
     3.3 @@ -13,7 +13,7 @@
     3.4  text\<open>A difference from HOL Light: all summations over infinite sets equal zero,
     3.5     so the "support" must be made explicit in the summation below!\<close>
     3.6  
     3.7 -proposition subordinate_partition_of_unity:
     3.8 +proposition%important subordinate_partition_of_unity:
     3.9    fixes S :: "'a :: euclidean_space set"
    3.10    assumes "S \<subseteq> \<Union>\<C>" and opC: "\<And>T. T \<in> \<C> \<Longrightarrow> open T"
    3.11        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> {}}"
    3.12 @@ -22,7 +22,7 @@
    3.13        and "\<And>x U. \<lbrakk>U \<in> \<C>; x \<in> S; x \<notin> U\<rbrakk> \<Longrightarrow> F U x = 0"
    3.14        and "\<And>x. x \<in> S \<Longrightarrow> supp_sum (\<lambda>W. F W x) \<C> = 1"
    3.15        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}"
    3.16 -proof (cases "\<exists>W. W \<in> \<C> \<and> S \<subseteq> W")
    3.17 +proof%unimportant (cases "\<exists>W. W \<in> \<C> \<and> S \<subseteq> W")
    3.18    case True
    3.19      then obtain W where "W \<in> \<C>" "S \<subseteq> W" by metis
    3.20      then show ?thesis
    3.21 @@ -283,7 +283,7 @@
    3.22            "\<And>x. f x = b \<longleftrightarrow> x \<in> T"
    3.23  using assms by (auto intro: Urysohn_local_strong [of UNIV S T])
    3.24  
    3.25 -proposition Urysohn:
    3.26 +proposition%important Urysohn:
    3.27    assumes US: "closed S"
    3.28        and UT: "closed T"
    3.29        and "S \<inter> T = {}"
    3.30 @@ -292,22 +292,22 @@
    3.31            "\<And>x. f x \<in> closed_segment a b"
    3.32            "\<And>x. x \<in> S \<Longrightarrow> f x = a"
    3.33            "\<And>x. x \<in> T \<Longrightarrow> f x = b"
    3.34 -using assms by (auto intro: Urysohn_local [of UNIV S T a b])
    3.35 +using%unimportant assms by (auto intro: Urysohn_local [of UNIV S T a b])
    3.36  
    3.37  
    3.38  subsection\<open> The Dugundji extension theorem, and Tietze variants as corollaries.\<close>
    3.39  
    3.40 -text\<open>J. Dugundji. An extension of Tietze's theorem. Pacific J. Math. Volume 1, Number 3 (1951), 353-367.
    3.41 +text%important\<open>J. Dugundji. An extension of Tietze's theorem. Pacific J. Math. Volume 1, Number 3 (1951), 353-367.
    3.42  http://projecteuclid.org/euclid.pjm/1103052106\<close>
    3.43  
    3.44 -theorem Dugundji:
    3.45 +theorem%important Dugundji:
    3.46    fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_inner"
    3.47    assumes "convex C" "C \<noteq> {}"
    3.48        and cloin: "closedin (subtopology euclidean U) S"
    3.49        and contf: "continuous_on S f" and "f ` S \<subseteq> C"
    3.50    obtains g where "continuous_on U g" "g ` U \<subseteq> C"
    3.51                    "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
    3.52 -proof (cases "S = {}")
    3.53 +proof%unimportant (cases "S = {}")
    3.54    case True then show thesis
    3.55      apply (rule_tac g="\<lambda>x. SOME y. y \<in> C" in that)
    3.56        apply (rule continuous_intros)
    3.57 @@ -475,7 +475,7 @@
    3.58  qed
    3.59  
    3.60  
    3.61 -corollary Tietze:
    3.62 +corollary%important Tietze:
    3.63    fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_inner"
    3.64    assumes "continuous_on S f"
    3.65        and "closedin (subtopology euclidean U) S"
    3.66 @@ -483,7 +483,7 @@
    3.67        and "\<And>x. x \<in> S \<Longrightarrow> norm(f x) \<le> B"
    3.68    obtains g where "continuous_on U g" "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
    3.69                    "\<And>x. x \<in> U \<Longrightarrow> norm(g x) \<le> B"
    3.70 -using assms
    3.71 +using%unimportant assms
    3.72  by (auto simp: image_subset_iff intro: Dugundji [of "cball 0 B" U S f])
    3.73  
    3.74  corollary Tietze_closed_interval:
     4.1 --- a/src/HOL/Analysis/Continuum_Not_Denumerable.thy	Thu Apr 05 06:15:02 2018 +0000
     4.2 +++ b/src/HOL/Analysis/Continuum_Not_Denumerable.thy	Fri Apr 06 17:34:50 2018 +0200
     4.3 @@ -11,7 +11,7 @@
     4.4    "HOL-Library.Countable_Set"
     4.5  begin
     4.6  
     4.7 -subsection \<open>Abstract\<close>
     4.8 +subsection%unimportant \<open>Abstract\<close>
     4.9  
    4.10  text \<open>
    4.11    The following document presents a proof that the Continuum is uncountable.
    4.12 @@ -33,8 +33,8 @@
    4.13    Nested Interval Property.
    4.14  \<close>
    4.15  
    4.16 -theorem real_non_denum: "\<nexists>f :: nat \<Rightarrow> real. surj f"
    4.17 -proof
    4.18 +theorem%important real_non_denum: "\<nexists>f :: nat \<Rightarrow> real. surj f"
    4.19 +proof%unimportant
    4.20    assume "\<exists>f::nat \<Rightarrow> real. surj f"
    4.21    then obtain f :: "nat \<Rightarrow> real" where "surj f" ..
    4.22  
     5.1 --- a/src/HOL/Analysis/Convex_Euclidean_Space.thy	Thu Apr 05 06:15:02 2018 +0000
     5.2 +++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy	Fri Apr 06 17:34:50 2018 +0200
     5.3 @@ -177,7 +177,7 @@
     5.4  
     5.5  subsection \<open>Convexity\<close>
     5.6  
     5.7 -definition convex :: "'a::real_vector set \<Rightarrow> bool"
     5.8 +definition%important convex :: "'a::real_vector set \<Rightarrow> bool"
     5.9    where "convex s \<longleftrightarrow> (\<forall>x\<in>s. \<forall>y\<in>s. \<forall>u\<ge>0. \<forall>v\<ge>0. u + v = 1 \<longrightarrow> u *\<^sub>R x + v *\<^sub>R y \<in> s)"
    5.10  
    5.11  lemma convexI:
    5.12 @@ -350,7 +350,7 @@
    5.13    by (simp add: convex_def scaleR_conv_of_real)
    5.14  
    5.15  
    5.16 -subsection \<open>Explicit expressions for convexity in terms of arbitrary sums\<close>
    5.17 +subsection%unimportant \<open>Explicit expressions for convexity in terms of arbitrary sums\<close>
    5.18  
    5.19  lemma convex_sum:
    5.20    fixes C :: "'a::real_vector set"
    5.21 @@ -503,7 +503,7 @@
    5.22  
    5.23  subsection \<open>Functions that are convex on a set\<close>
    5.24  
    5.25 -definition convex_on :: "'a::real_vector set \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> bool"
    5.26 +definition%important convex_on :: "'a::real_vector set \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> bool"
    5.27    where "convex_on s f \<longleftrightarrow>
    5.28      (\<forall>x\<in>s. \<forall>y\<in>s. \<forall>u\<ge>0. \<forall>v\<ge>0. u + v = 1 \<longrightarrow> f (u *\<^sub>R x + v *\<^sub>R y) \<le> u * f x + v * f y)"
    5.29  
    5.30 @@ -624,7 +624,7 @@
    5.31  qed
    5.32  
    5.33  
    5.34 -subsection \<open>Arithmetic operations on sets preserve convexity\<close>
    5.35 +subsection%unimportant \<open>Arithmetic operations on sets preserve convexity\<close>
    5.36  
    5.37  lemma convex_linear_image:
    5.38    assumes "linear f"
    5.39 @@ -1087,7 +1087,7 @@
    5.40  qed
    5.41  
    5.42  
    5.43 -subsection \<open>Convexity of real functions\<close>
    5.44 +subsection%unimportant \<open>Convexity of real functions\<close>
    5.45  
    5.46  lemma convex_on_realI:
    5.47    assumes "connected A"
    5.48 @@ -1406,7 +1406,7 @@
    5.49  
    5.50  subsection \<open>Affine set and affine hull\<close>
    5.51  
    5.52 -definition affine :: "'a::real_vector set \<Rightarrow> bool"
    5.53 +definition%important affine :: "'a::real_vector set \<Rightarrow> bool"
    5.54    where "affine s \<longleftrightarrow> (\<forall>x\<in>s. \<forall>y\<in>s. \<forall>u v. u + v = 1 \<longrightarrow> u *\<^sub>R x + v *\<^sub>R y \<in> s)"
    5.55  
    5.56  lemma affine_alt: "affine s \<longleftrightarrow> (\<forall>x\<in>s. \<forall>y\<in>s. \<forall>u::real. (1 - u) *\<^sub>R x + u *\<^sub>R y \<in> s)"
    5.57 @@ -1444,7 +1444,7 @@
    5.58    by (simp add: affine_def algebra_simps) (metis distrib_right mult.left_neutral)
    5.59  
    5.60  
    5.61 -subsubsection \<open>Some explicit formulations (from Lars Schewe)\<close>
    5.62 +subsubsection%unimportant \<open>Some explicit formulations (from Lars Schewe)\<close>
    5.63  
    5.64  lemma affine:
    5.65    fixes V::"'a::real_vector set"
    5.66 @@ -1668,7 +1668,7 @@
    5.67  qed
    5.68  
    5.69  
    5.70 -subsubsection \<open>Stepping theorems and hence small special cases\<close>
    5.71 +subsubsection%unimportant \<open>Stepping theorems and hence small special cases\<close>
    5.72  
    5.73  lemma affine_hull_empty[simp]: "affine hull {} = {}"
    5.74    by (rule hull_unique) auto
    5.75 @@ -1806,7 +1806,7 @@
    5.76    by (metis add_uminus_conv_diff mem_affine_3_minus real_vector.scale_minus_left)
    5.77  
    5.78  
    5.79 -subsubsection \<open>Some relations between affine hull and subspaces\<close>
    5.80 +subsubsection%unimportant \<open>Some relations between affine hull and subspaces\<close>
    5.81  
    5.82  lemma affine_hull_insert_subset_span:
    5.83    "affine hull (insert a s) \<subseteq> {a + v| v . v \<in> span {x - a | x . x \<in> s}}"
    5.84 @@ -1867,7 +1867,7 @@
    5.85    using affine_hull_insert_span[of a "s - {a}", unfolded insert_Diff[OF assms]] by auto
    5.86  
    5.87  
    5.88 -subsubsection \<open>Parallel affine sets\<close>
    5.89 +subsubsection%unimportant \<open>Parallel affine sets\<close>
    5.90  
    5.91  definition affine_parallel :: "'a::real_vector set \<Rightarrow> 'a::real_vector set \<Rightarrow> bool"
    5.92    where "affine_parallel S T \<longleftrightarrow> (\<exists>a. T = (\<lambda>x. a + x) ` S)"
    5.93 @@ -1974,7 +1974,7 @@
    5.94    unfolding subspace_def affine_def by auto
    5.95  
    5.96  
    5.97 -subsubsection \<open>Subspace parallel to an affine set\<close>
    5.98 +subsubsection%unimportant \<open>Subspace parallel to an affine set\<close>
    5.99  
   5.100  lemma subspace_affine: "subspace S \<longleftrightarrow> affine S \<and> 0 \<in> S"
   5.101  proof -
   5.102 @@ -2100,7 +2100,7 @@
   5.103  
   5.104  subsection \<open>Cones\<close>
   5.105  
   5.106 -definition cone :: "'a::real_vector set \<Rightarrow> bool"
   5.107 +definition%important cone :: "'a::real_vector set \<Rightarrow> bool"
   5.108    where "cone s \<longleftrightarrow> (\<forall>x\<in>s. \<forall>c\<ge>0. c *\<^sub>R x \<in> s)"
   5.109  
   5.110  lemma cone_empty[intro, simp]: "cone {}"
   5.111 @@ -2214,9 +2214,9 @@
   5.112    shows "c *\<^sub>R x \<in> cone hull S"
   5.113    by (metis assms cone_cone_hull hull_inc mem_cone)
   5.114  
   5.115 -lemma cone_hull_expl: "cone hull S = {c *\<^sub>R x | c x. c \<ge> 0 \<and> x \<in> S}"
   5.116 +lemma%important cone_hull_expl: "cone hull S = {c *\<^sub>R x | c x. c \<ge> 0 \<and> x \<in> S}"
   5.117    (is "?lhs = ?rhs")
   5.118 -proof -
   5.119 +proof%unimportant -
   5.120    {
   5.121      fix x
   5.122      assume "x \<in> ?rhs"
   5.123 @@ -2282,7 +2282,7 @@
   5.124  
   5.125  subsection \<open>Affine dependence and consequential theorems (from Lars Schewe)\<close>
   5.126  
   5.127 -definition affine_dependent :: "'a::real_vector set \<Rightarrow> bool"
   5.128 +definition%important affine_dependent :: "'a::real_vector set \<Rightarrow> bool"
   5.129    where "affine_dependent s \<longleftrightarrow> (\<exists>x\<in>s. x \<in> affine hull (s - {x}))"
   5.130  
   5.131  lemma affine_dependent_subset:
   5.132 @@ -2299,11 +2299,11 @@
   5.133     "~ affine_dependent s \<Longrightarrow> ~ affine_dependent(s - t)"
   5.134  by (meson Diff_subset affine_dependent_subset)
   5.135  
   5.136 -lemma affine_dependent_explicit:
   5.137 +lemma%important affine_dependent_explicit:
   5.138    "affine_dependent p \<longleftrightarrow>
   5.139      (\<exists>s u. finite s \<and> s \<subseteq> p \<and> sum u s = 0 \<and>
   5.140        (\<exists>v\<in>s. u v \<noteq> 0) \<and> sum (\<lambda>v. u v *\<^sub>R v) s = 0)"
   5.141 -  unfolding affine_dependent_def affine_hull_explicit mem_Collect_eq
   5.142 +  unfolding%unimportant affine_dependent_def affine_hull_explicit mem_Collect_eq
   5.143    apply rule
   5.144    apply (erule bexE, erule exE, erule exE)
   5.145    apply (erule conjE)+
   5.146 @@ -2365,7 +2365,7 @@
   5.147  qed
   5.148  
   5.149  
   5.150 -subsection \<open>Connectedness of convex sets\<close>
   5.151 +subsection%unimportant \<open>Connectedness of convex sets\<close>
   5.152  
   5.153  lemma connectedD:
   5.154    "connected S \<Longrightarrow> open A \<Longrightarrow> open B \<Longrightarrow> S \<subseteq> A \<union> B \<Longrightarrow> A \<inter> B \<inter> S = {} \<Longrightarrow> A \<inter> S = {} \<or> B \<inter> S = {}"
   5.155 @@ -2558,7 +2558,7 @@
   5.156    by auto
   5.157  
   5.158  
   5.159 -subsubsection \<open>Convex hull is "preserved" by a linear function\<close>
   5.160 +subsubsection%unimportant \<open>Convex hull is "preserved" by a linear function\<close>
   5.161  
   5.162  lemma convex_hull_linear_image:
   5.163    assumes f: "linear f"
   5.164 @@ -2616,7 +2616,7 @@
   5.165  qed
   5.166  
   5.167  
   5.168 -subsubsection \<open>Stepping theorems for convex hulls of finite sets\<close>
   5.169 +subsubsection%unimportant \<open>Stepping theorems for convex hulls of finite sets\<close>
   5.170  
   5.171  lemma convex_hull_empty[simp]: "convex hull {} = {}"
   5.172    by (rule hull_unique) auto
   5.173 @@ -2742,16 +2742,16 @@
   5.174    using diff_eq_eq apply fastforce
   5.175    by (metis add.group_left_neutral add_le_imp_le_diff diff_add_cancel)
   5.176  
   5.177 -subsubsection \<open>Explicit expression for convex hull\<close>
   5.178 -
   5.179 -lemma convex_hull_indexed:
   5.180 +subsubsection%unimportant \<open>Explicit expression for convex hull\<close>
   5.181 +
   5.182 +lemma%important convex_hull_indexed:
   5.183    fixes s :: "'a::real_vector set"
   5.184    shows "convex hull s =
   5.185      {y. \<exists>k u x.
   5.186        (\<forall>i\<in>{1::nat .. k}. 0 \<le> u i \<and> x i \<in> s) \<and>
   5.187        (sum u {1..k} = 1) \<and> (sum (\<lambda>i. u i *\<^sub>R x i) {1..k} = y)}"
   5.188    (is "?xyz = ?hull")
   5.189 -  apply (rule hull_unique)
   5.190 +  apply%unimportant (rule hull_unique)
   5.191    apply rule
   5.192    defer
   5.193    apply (rule convexI)
   5.194 @@ -2887,7 +2887,7 @@
   5.195  qed
   5.196  
   5.197  
   5.198 -subsubsection \<open>Another formulation from Lars Schewe\<close>
   5.199 +subsubsection%unimportant \<open>Another formulation from Lars Schewe\<close>
   5.200  
   5.201  lemma convex_hull_explicit:
   5.202    fixes p :: "'a::real_vector set"
   5.203 @@ -2991,7 +2991,7 @@
   5.204  qed
   5.205  
   5.206  
   5.207 -subsubsection \<open>A stepping theorem for that expansion\<close>
   5.208 +subsubsection%unimportant \<open>A stepping theorem for that expansion\<close>
   5.209  
   5.210  lemma convex_hull_finite_step:
   5.211    fixes s :: "'a::real_vector set"
   5.212 @@ -3061,7 +3061,7 @@
   5.213  qed
   5.214  
   5.215  
   5.216 -subsubsection \<open>Hence some special cases\<close>
   5.217 +subsubsection%unimportant \<open>Hence some special cases\<close>
   5.218  
   5.219  lemma convex_hull_2:
   5.220    "convex hull {a,b} = {u *\<^sub>R a + v *\<^sub>R b | u v. 0 \<le> u \<and> 0 \<le> v \<and> u + v = 1}"
   5.221 @@ -3141,7 +3141,7 @@
   5.222  qed
   5.223  
   5.224  
   5.225 -subsection \<open>Relations among closure notions and corresponding hulls\<close>
   5.226 +subsection%unimportant \<open>Relations among closure notions and corresponding hulls\<close>
   5.227  
   5.228  lemma affine_imp_convex: "affine s \<Longrightarrow> convex s"
   5.229    unfolding affine_def convex_def by auto
   5.230 @@ -3306,7 +3306,7 @@
   5.231  qed
   5.232  
   5.233  
   5.234 -subsection \<open>Some Properties of Affine Dependent Sets\<close>
   5.235 +subsection%unimportant \<open>Some Properties of Affine Dependent Sets\<close>
   5.236  
   5.237  lemma affine_independent_0 [simp]: "\<not> affine_dependent {}"
   5.238    by (simp add: affine_dependent_def)
   5.239 @@ -3546,7 +3546,7 @@
   5.240  
   5.241  subsection \<open>Affine Dimension of a Set\<close>
   5.242  
   5.243 -definition aff_dim :: "('a::euclidean_space) set \<Rightarrow> int"
   5.244 +definition%important aff_dim :: "('a::euclidean_space) set \<Rightarrow> int"
   5.245    where "aff_dim V =
   5.246    (SOME d :: int.
   5.247      \<exists>B. affine hull B = affine hull V \<and> \<not> affine_dependent B \<and> of_nat (card B) = d + 1)"
   5.248 @@ -4417,11 +4417,11 @@
   5.249      by (auto simp add: convex_hull_explicit)
   5.250  qed
   5.251  
   5.252 -theorem caratheodory:
   5.253 +theorem%important caratheodory:
   5.254    "convex hull p =
   5.255      {x::'a::euclidean_space. \<exists>s. finite s \<and> s \<subseteq> p \<and>
   5.256        card s \<le> DIM('a) + 1 \<and> x \<in> convex hull s}"
   5.257 -proof safe
   5.258 +proof%unimportant safe
   5.259    fix x
   5.260    assume "x \<in> convex hull p"
   5.261    then obtain s u where "finite s" "s \<subseteq> p" "card s \<le> DIM('a) + 1"
   5.262 @@ -4444,7 +4444,7 @@
   5.263  
   5.264  subsection \<open>Relative interior of a set\<close>
   5.265  
   5.266 -definition "rel_interior S =
   5.267 +definition%important "rel_interior S =
   5.268    {x. \<exists>T. openin (subtopology euclidean (affine hull S)) T \<and> x \<in> T \<and> T \<subseteq> S}"
   5.269  
   5.270  lemma rel_interior_mono:
   5.271 @@ -4769,7 +4769,7 @@
   5.272  
   5.273  subsubsection \<open>Relative open sets\<close>
   5.274  
   5.275 -definition "rel_open S \<longleftrightarrow> rel_interior S = S"
   5.276 +definition%important "rel_open S \<longleftrightarrow> rel_interior S = S"
   5.277  
   5.278  lemma rel_open: "rel_open S \<longleftrightarrow> openin (subtopology euclidean (affine hull S)) S"
   5.279    unfolding rel_open_def rel_interior_def
   5.280 @@ -4970,7 +4970,7 @@
   5.281  qed
   5.282  
   5.283  
   5.284 -subsubsection\<open>Relative interior preserves under linear transformations\<close>
   5.285 +subsubsection%unimportant\<open>Relative interior preserves under linear transformations\<close>
   5.286  
   5.287  lemma rel_interior_translation_aux:
   5.288    fixes a :: "'n::euclidean_space"
   5.289 @@ -5134,7 +5134,7 @@
   5.290    by auto
   5.291  
   5.292  
   5.293 -subsection\<open>Some Properties of subset of standard basis\<close>
   5.294 +subsection%unimportant\<open>Some Properties of subset of standard basis\<close>
   5.295  
   5.296  lemma affine_hull_substd_basis:
   5.297    assumes "d \<subseteq> Basis"
   5.298 @@ -5151,7 +5151,7 @@
   5.299    by (metis Int_absorb1 Int_absorb2 convex_hull_subset_affine_hull hull_hull hull_mono hull_subset)
   5.300  
   5.301  
   5.302 -subsection \<open>Openness and compactness are preserved by convex hull operation.\<close>
   5.303 +subsection%unimportant \<open>Openness and compactness are preserved by convex hull operation.\<close>
   5.304  
   5.305  lemma open_convex_hull[intro]:
   5.306    fixes s :: "'a::real_normed_vector set"
   5.307 @@ -5422,7 +5422,7 @@
   5.308  qed
   5.309  
   5.310  
   5.311 -subsection \<open>Extremal points of a simplex are some vertices.\<close>
   5.312 +subsection%unimportant \<open>Extremal points of a simplex are some vertices.\<close>
   5.313  
   5.314  lemma dist_increases_online:
   5.315    fixes a b d :: "'a::real_inner"
   5.316 @@ -5623,7 +5623,7 @@
   5.317  
   5.318  subsection \<open>Closest point of a convex set is unique, with a continuous projection.\<close>
   5.319  
   5.320 -definition closest_point :: "'a::{real_inner,heine_borel} set \<Rightarrow> 'a \<Rightarrow> 'a"
   5.321 +definition%important closest_point :: "'a::{real_inner,heine_borel} set \<Rightarrow> 'a \<Rightarrow> 'a"
   5.322    where "closest_point s a = (SOME x. x \<in> s \<and> (\<forall>y\<in>s. dist a x \<le> dist a y))"
   5.323  
   5.324  lemma closest_point_exists:
   5.325 @@ -5811,7 +5811,7 @@
   5.326  qed
   5.327  
   5.328  
   5.329 -subsubsection \<open>Various point-to-set separating/supporting hyperplane theorems.\<close>
   5.330 +subsubsection%unimportant \<open>Various point-to-set separating/supporting hyperplane theorems.\<close>
   5.331  
   5.332  lemma supporting_hyperplane_closed_point:
   5.333    fixes z :: "'a::{real_inner,heine_borel}"
   5.334 @@ -5933,7 +5933,7 @@
   5.335  qed
   5.336  
   5.337  
   5.338 -subsubsection \<open>Now set-to-set for closed/compact sets\<close>
   5.339 +subsubsection%unimportant \<open>Now set-to-set for closed/compact sets\<close>
   5.340  
   5.341  lemma separating_hyperplane_closed_compact:
   5.342    fixes S :: "'a::euclidean_space set"
   5.343 @@ -6024,7 +6024,7 @@
   5.344  qed
   5.345  
   5.346  
   5.347 -subsubsection \<open>General case without assuming closure and getting non-strict separation\<close>
   5.348 +subsubsection%unimportant \<open>General case without assuming closure and getting non-strict separation\<close>
   5.349  
   5.350  lemma separating_hyperplane_set_0:
   5.351    assumes "convex s" "(0::'a::euclidean_space) \<notin> s"
   5.352 @@ -6082,7 +6082,7 @@
   5.353  qed
   5.354  
   5.355  
   5.356 -subsection \<open>More convexity generalities\<close>
   5.357 +subsection%unimportant \<open>More convexity generalities\<close>
   5.358  
   5.359  lemma convex_closure [intro,simp]:
   5.360    fixes s :: "'a::real_normed_vector set"
   5.361 @@ -6132,7 +6132,7 @@
   5.362    using hull_subset[of s convex] convex_hull_empty by auto
   5.363  
   5.364  
   5.365 -subsection \<open>Moving and scaling convex hulls.\<close>
   5.366 +subsection%unimportant \<open>Moving and scaling convex hulls.\<close>
   5.367  
   5.368  lemma convex_hull_set_plus:
   5.369    "convex hull (s + t) = convex hull s + convex hull t"
   5.370 @@ -6159,7 +6159,7 @@
   5.371    by(simp only: image_image[symmetric] convex_hull_scaling convex_hull_translation)
   5.372  
   5.373  
   5.374 -subsection \<open>Convexity of cone hulls\<close>
   5.375 +subsection%unimportant \<open>Convexity of cone hulls\<close>
   5.376  
   5.377  lemma convex_cone_hull:
   5.378    assumes "convex S"
   5.379 @@ -6227,7 +6227,7 @@
   5.380      using \<open>S \<noteq> {}\<close> cone_iff[of "convex hull S"] by auto
   5.381  qed
   5.382  
   5.383 -subsection \<open>Convex set as intersection of halfspaces\<close>
   5.384 +subsection%unimportant \<open>Convex set as intersection of halfspaces\<close>
   5.385  
   5.386  lemma convex_halfspace_intersection:
   5.387    fixes s :: "('a::euclidean_space) set"
   5.388 @@ -6381,10 +6381,10 @@
   5.389      done
   5.390  qed
   5.391  
   5.392 -lemma radon:
   5.393 +theorem%important radon:
   5.394    assumes "affine_dependent c"
   5.395    obtains m p where "m \<subseteq> c" "p \<subseteq> c" "m \<inter> p = {}" "(convex hull m) \<inter> (convex hull p) \<noteq> {}"
   5.396 -proof -
   5.397 +proof%unimportant -
   5.398    from assms[unfolded affine_dependent_explicit]
   5.399    obtain s u where
   5.400        "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"
   5.401 @@ -6503,12 +6503,12 @@
   5.402    qed auto
   5.403  qed
   5.404  
   5.405 -lemma helly:
   5.406 +theorem%important helly:
   5.407    fixes f :: "'a::euclidean_space set set"
   5.408    assumes "card f \<ge> DIM('a) + 1" "\<forall>s\<in>f. convex s"
   5.409      and "\<forall>t\<subseteq>f. card t = DIM('a) + 1 \<longrightarrow> \<Inter>t \<noteq> {}"
   5.410    shows "\<Inter>f \<noteq> {}"
   5.411 -  apply (rule helly_induct)
   5.412 +  apply%unimportant (rule helly_induct)
   5.413    using assms
   5.414    apply auto
   5.415    done
   5.416 @@ -6516,7 +6516,7 @@
   5.417  
   5.418  subsection \<open>Epigraphs of convex functions\<close>
   5.419  
   5.420 -definition "epigraph s (f :: _ \<Rightarrow> real) = {xy. fst xy \<in> s \<and> f (fst xy) \<le> snd xy}"
   5.421 +definition%important "epigraph s (f :: _ \<Rightarrow> real) = {xy. fst xy \<in> s \<and> f (fst xy) \<le> snd xy}"
   5.422  
   5.423  lemma mem_epigraph: "(x, y) \<in> epigraph s f \<longleftrightarrow> x \<in> s \<and> f x \<le> y"
   5.424    unfolding epigraph_def by auto
   5.425 @@ -6545,7 +6545,7 @@
   5.426    by (simp add: convex_epigraph)
   5.427  
   5.428  
   5.429 -subsubsection \<open>Use this to derive general bound property of convex function\<close>
   5.430 +subsubsection%unimportant \<open>Use this to derive general bound property of convex function\<close>
   5.431  
   5.432  lemma convex_on:
   5.433    assumes "convex s"
   5.434 @@ -6572,7 +6572,7 @@
   5.435    done
   5.436  
   5.437  
   5.438 -subsection \<open>Convexity of general and special intervals\<close>
   5.439 +subsection%unimportant \<open>Convexity of general and special intervals\<close>
   5.440  
   5.441  lemma is_interval_convex:
   5.442    fixes s :: "'a::euclidean_space set"
   5.443 @@ -6657,7 +6657,7 @@
   5.444       "\<lbrakk>connected S; aff_dim S \<noteq> 0; a \<in> S\<rbrakk> \<Longrightarrow> a islimpt S"
   5.445    using aff_dim_sing connected_imp_perfect by blast
   5.446  
   5.447 -subsection \<open>On \<open>real\<close>, \<open>is_interval\<close>, \<open>convex\<close> and \<open>connected\<close> are all equivalent.\<close>
   5.448 +subsection%unimportant \<open>On \<open>real\<close>, \<open>is_interval\<close>, \<open>convex\<close> and \<open>connected\<close> are all equivalent.\<close>
   5.449  
   5.450  lemma mem_is_interval_1_I:
   5.451    fixes a b c::real
   5.452 @@ -6742,7 +6742,7 @@
   5.453    by (auto simp: is_interval_convex_1 convex_cball)
   5.454  
   5.455  
   5.456 -subsection \<open>Another intermediate value theorem formulation\<close>
   5.457 +subsection%unimportant \<open>Another intermediate value theorem formulation\<close>
   5.458  
   5.459  lemma ivt_increasing_component_on_1:
   5.460    fixes f :: "real \<Rightarrow> 'a::euclidean_space"
   5.461 @@ -6787,7 +6787,7 @@
   5.462    by (rule ivt_decreasing_component_on_1) (auto simp: continuous_at_imp_continuous_on)
   5.463  
   5.464  
   5.465 -subsection \<open>A bound within a convex hull, and so an interval\<close>
   5.466 +subsection%unimportant \<open>A bound within a convex hull, and so an interval\<close>
   5.467  
   5.468  lemma convex_on_convex_hull_bound:
   5.469    assumes "convex_on (convex hull s) f"
   5.470 @@ -6992,7 +6992,7 @@
   5.471      done
   5.472  qed
   5.473  
   5.474 -subsubsection\<open>Representation of any interval as a finite convex hull\<close>
   5.475 +subsubsection%unimportant\<open>Representation of any interval as a finite convex hull\<close>
   5.476  
   5.477  lemma image_stretch_interval:
   5.478    "(\<lambda>x. \<Sum>k\<in>Basis. (m k * (x\<bullet>k)) *\<^sub>R k) ` cbox a (b::'a::euclidean_space) =
   5.479 @@ -7069,7 +7069,7 @@
   5.480  qed
   5.481  
   5.482  
   5.483 -subsection \<open>Bounded convex function on open set is continuous\<close>
   5.484 +subsection%unimportant \<open>Bounded convex function on open set is continuous\<close>
   5.485  
   5.486  lemma convex_on_bounded_continuous:
   5.487    fixes s :: "('a::real_normed_vector) set"
   5.488 @@ -7186,7 +7186,7 @@
   5.489  qed
   5.490  
   5.491  
   5.492 -subsection \<open>Upper bound on a ball implies upper and lower bounds\<close>
   5.493 +subsection%unimportant \<open>Upper bound on a ball implies upper and lower bounds\<close>
   5.494  
   5.495  lemma convex_bounds_lemma:
   5.496    fixes x :: "'a::real_normed_vector"
   5.497 @@ -7220,7 +7220,7 @@
   5.498  qed
   5.499  
   5.500  
   5.501 -subsubsection \<open>Hence a convex function on an open set is continuous\<close>
   5.502 +subsubsection%unimportant \<open>Hence a convex function on an open set is continuous\<close>
   5.503  
   5.504  lemma real_of_nat_ge_one_iff: "1 \<le> real (n::nat) \<longleftrightarrow> 1 \<le> n"
   5.505    by auto
     6.1 --- a/src/HOL/Analysis/Euclidean_Space.thy	Thu Apr 05 06:15:02 2018 +0000
     6.2 +++ b/src/HOL/Analysis/Euclidean_Space.thy	Fri Apr 06 17:34:50 2018 +0200
     6.3 @@ -12,7 +12,7 @@
     6.4  
     6.5  subsection \<open>Type class of Euclidean spaces\<close>
     6.6  
     6.7 -class euclidean_space = real_inner +
     6.8 +class%important euclidean_space = real_inner +
     6.9    fixes Basis :: "'a set"
    6.10    assumes nonempty_Basis [simp]: "Basis \<noteq> {}"
    6.11    assumes finite_Basis [simp]: "finite Basis"
    6.12 @@ -152,7 +152,7 @@
    6.13      using False by (auto simp: inner_sum_left)
    6.14  qed
    6.15  
    6.16 -subsection \<open>Subclass relationships\<close>
    6.17 +subsection%unimportant \<open>Subclass relationships\<close>
    6.18  
    6.19  instance euclidean_space \<subseteq> perfect_space
    6.20  proof
    6.21 @@ -175,9 +175,9 @@
    6.22  
    6.23  subsection \<open>Class instances\<close>
    6.24  
    6.25 -subsubsection \<open>Type @{typ real}\<close>
    6.26 +subsubsection%unimportant \<open>Type @{typ real}\<close>
    6.27  
    6.28 -instantiation real :: euclidean_space
    6.29 +instantiation%important real :: euclidean_space
    6.30  begin
    6.31  
    6.32  definition
    6.33 @@ -191,9 +191,9 @@
    6.34  lemma DIM_real[simp]: "DIM(real) = 1"
    6.35    by simp
    6.36  
    6.37 -subsubsection \<open>Type @{typ complex}\<close>
    6.38 +subsubsection%unimportant \<open>Type @{typ complex}\<close>
    6.39  
    6.40 -instantiation complex :: euclidean_space
    6.41 +instantiation%important complex :: euclidean_space
    6.42  begin
    6.43  
    6.44  definition Basis_complex_def: "Basis = {1, \<i>}"
    6.45 @@ -206,9 +206,9 @@
    6.46  lemma DIM_complex[simp]: "DIM(complex) = 2"
    6.47    unfolding Basis_complex_def by simp
    6.48  
    6.49 -subsubsection \<open>Type @{typ "'a \<times> 'b"}\<close>
    6.50 +subsubsection%unimportant \<open>Type @{typ "'a \<times> 'b"}\<close>
    6.51  
    6.52 -instantiation prod :: (euclidean_space, euclidean_space) euclidean_space
    6.53 +instantiation%important prod :: (euclidean_space, euclidean_space) euclidean_space
    6.54  begin
    6.55  
    6.56  definition
     7.1 --- a/src/HOL/Analysis/Inner_Product.thy	Thu Apr 05 06:15:02 2018 +0000
     7.2 +++ b/src/HOL/Analysis/Inner_Product.thy	Fri Apr 06 17:34:50 2018 +0200
     7.3 @@ -27,7 +27,7 @@
     7.4  setup \<open>Sign.add_const_constraint
     7.5    (@{const_name norm}, SOME @{typ "'a::norm \<Rightarrow> real"})\<close>
     7.6  
     7.7 -class real_inner = real_vector + sgn_div_norm + dist_norm + uniformity_dist + open_uniformity +
     7.8 +class%important real_inner = real_vector + sgn_div_norm + dist_norm + uniformity_dist + open_uniformity +
     7.9    fixes inner :: "'a \<Rightarrow> 'a \<Rightarrow> real"
    7.10    assumes inner_commute: "inner x y = inner y x"
    7.11    and inner_add_left: "inner (x + y) z = inner x z + inner y z"
    7.12 @@ -236,7 +236,7 @@
    7.13  
    7.14  subsection \<open>Class instances\<close>
    7.15  
    7.16 -instantiation real :: real_inner
    7.17 +instantiation%important real :: real_inner
    7.18  begin
    7.19  
    7.20  definition inner_real_def [simp]: "inner = ( * )"
    7.21 @@ -265,7 +265,7 @@
    7.22      and real_inner_1_right[simp]: "inner x 1 = x"
    7.23    by simp_all
    7.24  
    7.25 -instantiation complex :: real_inner
    7.26 +instantiation%important complex :: real_inner
    7.27  begin
    7.28  
    7.29  definition inner_complex_def:
    7.30 @@ -357,7 +357,7 @@
    7.31  
    7.32  subsection \<open>Gradient derivative\<close>
    7.33  
    7.34 -definition
    7.35 +definition%important
    7.36    gderiv ::
    7.37      "['a::real_inner \<Rightarrow> real, 'a, 'a] \<Rightarrow> bool"
    7.38            ("(GDERIV (_)/ (_)/ :> (_))" [1000, 1000, 60] 60)
     8.1 --- a/src/HOL/Analysis/Linear_Algebra.thy	Thu Apr 05 06:15:02 2018 +0000
     8.2 +++ b/src/HOL/Analysis/Linear_Algebra.thy	Fri Apr 06 17:34:50 2018 +0200
     8.3 @@ -36,7 +36,7 @@
     8.4  
     8.5  subsection \<open>A generic notion of "hull" (convex, affine, conic hull and closure).\<close>
     8.6  
     8.7 -definition hull :: "('a set \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a set"  (infixl "hull" 75)
     8.8 +definition%important hull :: "('a set \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a set"  (infixl "hull" 75)
     8.9    where "S hull s = \<Inter>{t. S t \<and> s \<subseteq> t}"
    8.10  
    8.11  lemma hull_same: "S s \<Longrightarrow> S hull s = s"
    8.12 @@ -109,10 +109,10 @@
    8.13  
    8.14  subsection \<open>Linear functions.\<close>
    8.15  
    8.16 -lemma linear_iff:
    8.17 +lemma%important linear_iff:
    8.18    "linear f \<longleftrightarrow> (\<forall>x y. f (x + y) = f x + f y) \<and> (\<forall>c x. f (c *\<^sub>R x) = c *\<^sub>R f x)"
    8.19    (is "linear f \<longleftrightarrow> ?rhs")
    8.20 -proof
    8.21 +proof%unimportant
    8.22    assume "linear f"
    8.23    then interpret f: linear f .
    8.24    show "?rhs" by (simp add: f.add f.scaleR)
    8.25 @@ -230,11 +230,11 @@
    8.26  
    8.27  subsection \<open>Subspaces of vector spaces\<close>
    8.28  
    8.29 -definition (in real_vector) subspace :: "'a set \<Rightarrow> bool"
    8.30 +definition%important (in real_vector) subspace :: "'a set \<Rightarrow> bool"
    8.31    where "subspace S \<longleftrightarrow> 0 \<in> S \<and> (\<forall>x \<in> S. \<forall>y \<in> S. x + y \<in> S) \<and> (\<forall>c. \<forall>x \<in> S. c *\<^sub>R x \<in> S)"
    8.32  
    8.33 -definition (in real_vector) "span S = (subspace hull S)"
    8.34 -definition (in real_vector) "dependent S \<longleftrightarrow> (\<exists>a \<in> S. a \<in> span (S - {a}))"
    8.35 +definition%important (in real_vector) "span S = (subspace hull S)"
    8.36 +definition%important (in real_vector) "dependent S \<longleftrightarrow> (\<exists>a \<in> S. a \<in> span (S - {a}))"
    8.37  abbreviation (in real_vector) "independent s \<equiv> \<not> dependent s"
    8.38  
    8.39  text \<open>Closure properties of subspaces.\<close>
    8.40 @@ -284,7 +284,7 @@
    8.41   apply (metis add.assoc add.left_commute)
    8.42  using scaleR_add_right by blast
    8.43  
    8.44 -subsection \<open>Properties of span\<close>
    8.45 +subsection%unimportant \<open>Properties of span\<close>
    8.46  
    8.47  lemma (in real_vector) span_mono: "A \<subseteq> B \<Longrightarrow> span A \<subseteq> span B"
    8.48    by (metis span_def hull_mono)
    8.49 @@ -1351,7 +1351,7 @@
    8.50  qed
    8.51  
    8.52  
    8.53 -subsection \<open>More interesting properties of the norm.\<close>
    8.54 +subsection%unimportant \<open>More interesting properties of the norm.\<close>
    8.55  
    8.56  lemma cond_application_beta: "(if b then f else g) x = (if b then f x else g x)"
    8.57    by auto
    8.58 @@ -1498,11 +1498,11 @@
    8.59  
    8.60  subsection \<open>Orthogonality.\<close>
    8.61  
    8.62 +definition%important (in real_inner) "orthogonal x y \<longleftrightarrow> x \<bullet> y = 0"
    8.63 +
    8.64  context real_inner
    8.65  begin
    8.66  
    8.67 -definition "orthogonal x y \<longleftrightarrow> x \<bullet> y = 0"
    8.68 -
    8.69  lemma orthogonal_self: "orthogonal x x \<longleftrightarrow> x = 0"
    8.70    by (simp add: orthogonal_def)
    8.71  
    8.72 @@ -1567,7 +1567,7 @@
    8.73  
    8.74  subsection \<open>Bilinear functions.\<close>
    8.75  
    8.76 -definition "bilinear f \<longleftrightarrow> (\<forall>x. linear (\<lambda>y. f x y)) \<and> (\<forall>y. linear (\<lambda>x. f x y))"
    8.77 +definition%important "bilinear f \<longleftrightarrow> (\<forall>x. linear (\<lambda>y. f x y)) \<and> (\<forall>y. linear (\<lambda>x. f x y))"
    8.78  
    8.79  lemma bilinear_ladd: "bilinear h \<Longrightarrow> h (x + y) z = h x z + h y z"
    8.80    by (simp add: bilinear_def linear_iff)
    8.81 @@ -1630,7 +1630,7 @@
    8.82  
    8.83  subsection \<open>Adjoints.\<close>
    8.84  
    8.85 -definition "adjoint f = (SOME f'. \<forall>x y. f x \<bullet> y = x \<bullet> f' y)"
    8.86 +definition%important "adjoint f = (SOME f'. \<forall>x y. f x \<bullet> y = x \<bullet> f' y)"
    8.87  
    8.88  lemma adjoint_unique:
    8.89    assumes "\<forall>x y. inner (f x) y = inner x (g y)"
    8.90 @@ -1701,7 +1701,7 @@
    8.91    by (rule adjoint_unique, simp add: adjoint_clauses [OF lf])
    8.92  
    8.93  
    8.94 -subsection \<open>Interlude: Some properties of real sets\<close>
    8.95 +subsection%unimportant \<open>Interlude: Some properties of real sets\<close>
    8.96  
    8.97  lemma seq_mono_lemma:
    8.98    assumes "\<forall>(n::nat) \<ge> m. (d n :: real) < e n"
    8.99 @@ -1754,11 +1754,11 @@
   8.100  subsection \<open>Archimedean properties and useful consequences\<close>
   8.101  
   8.102  text\<open>Bernoulli's inequality\<close>
   8.103 -proposition Bernoulli_inequality:
   8.104 +proposition%important Bernoulli_inequality:
   8.105    fixes x :: real
   8.106    assumes "-1 \<le> x"
   8.107      shows "1 + n * x \<le> (1 + x) ^ n"
   8.108 -proof (induct n)
   8.109 +proof%unimportant (induct n)
   8.110    case 0
   8.111    then show ?case by simp
   8.112  next
   8.113 @@ -1844,7 +1844,7 @@
   8.114    done
   8.115  
   8.116  
   8.117 -subsection \<open>Euclidean Spaces as Typeclass\<close>
   8.118 +subsection%unimportant \<open>Euclidean Spaces as Typeclass\<close>
   8.119  
   8.120  lemma independent_Basis: "independent Basis"
   8.121    unfolding dependent_def
   8.122 @@ -1905,7 +1905,7 @@
   8.123  qed
   8.124  
   8.125  
   8.126 -subsection \<open>Linearity and Bilinearity continued\<close>
   8.127 +subsection%unimportant \<open>Linearity and Bilinearity continued\<close>
   8.128  
   8.129  lemma linear_bounded:
   8.130    fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
   8.131 @@ -2074,7 +2074,7 @@
   8.132  by (metis linear_imp_has_derivative differentiable_def)
   8.133  
   8.134  
   8.135 -subsection \<open>We continue.\<close>
   8.136 +subsection%unimportant \<open>We continue.\<close>
   8.137  
   8.138  lemma independent_bound:
   8.139    fixes S :: "'a::euclidean_space set"
   8.140 @@ -2879,7 +2879,7 @@
   8.141  
   8.142  subsection \<open>Infinity norm\<close>
   8.143  
   8.144 -definition "infnorm (x::'a::euclidean_space) = Sup {\<bar>x \<bullet> b\<bar> |b. b \<in> Basis}"
   8.145 +definition%important "infnorm (x::'a::euclidean_space) = Sup {\<bar>x \<bullet> b\<bar> |b. b \<in> Basis}"
   8.146  
   8.147  lemma infnorm_set_image:
   8.148    fixes x :: "'a::euclidean_space"
   8.149 @@ -3115,7 +3115,7 @@
   8.150  
   8.151  subsection \<open>Collinearity\<close>
   8.152  
   8.153 -definition collinear :: "'a::real_vector set \<Rightarrow> bool"
   8.154 +definition%important collinear :: "'a::real_vector set \<Rightarrow> bool"
   8.155    where "collinear S \<longleftrightarrow> (\<exists>u. \<forall>x \<in> S. \<forall> y \<in> S. \<exists>c. x - y = c *\<^sub>R u)"
   8.156  
   8.157  lemma collinear_alt:
     9.1 --- a/src/HOL/Analysis/Measurable.thy	Thu Apr 05 06:15:02 2018 +0000
     9.2 +++ b/src/HOL/Analysis/Measurable.thy	Fri Apr 06 17:34:50 2018 +0200
     9.3 @@ -1,13 +1,13 @@
     9.4  (*  Title:      HOL/Analysis/Measurable.thy
     9.5      Author:     Johannes Hölzl <hoelzl@in.tum.de>
     9.6  *)
     9.7 +section \<open>Measurability prover\<close>
     9.8  theory Measurable
     9.9    imports
    9.10      Sigma_Algebra
    9.11      "HOL-Library.Order_Continuity"
    9.12  begin
    9.13  
    9.14 -subsection \<open>Measurability prover\<close>
    9.15  
    9.16  lemma (in algebra) sets_Collect_finite_All:
    9.17    assumes "\<And>i. i \<in> S \<Longrightarrow> {x\<in>\<Omega>. P i x} \<in> M" "finite S"
    9.18 @@ -64,10 +64,10 @@
    9.19  attribute_setup measurable_cong = Measurable.cong_thm_attr
    9.20    "add congurence rules to measurability prover"
    9.21  
    9.22 -method_setup measurable = \<open> Scan.lift (Scan.succeed (METHOD o Measurable.measurable_tac)) \<close>
    9.23 +method_setup%important measurable = \<open> Scan.lift (Scan.succeed (METHOD o Measurable.measurable_tac)) \<close>
    9.24    "measurability prover"
    9.25  
    9.26 -simproc_setup measurable ("A \<in> sets M" | "f \<in> measurable M N") = \<open>K Measurable.simproc\<close>
    9.27 +simproc_setup%important measurable ("A \<in> sets M" | "f \<in> measurable M N") = \<open>K Measurable.simproc\<close>
    9.28  
    9.29  setup \<open>
    9.30    Global_Theory.add_thms_dynamic (@{binding measurable}, Measurable.get_all)
    9.31 @@ -380,7 +380,7 @@
    9.32    unfolding pred_def
    9.33    by (auto intro!: sets.sets_Collect_countable_All' sets.sets_Collect_countable_Ex' assms)
    9.34  
    9.35 -subsection \<open>Measurability for (co)inductive predicates\<close>
    9.36 +subsection%unimportant \<open>Measurability for (co)inductive predicates\<close>
    9.37  
    9.38  lemma measurable_bot[measurable]: "bot \<in> measurable M (count_space UNIV)"
    9.39    by (simp add: bot_fun_def)
    10.1 --- a/src/HOL/Analysis/Measure_Space.thy	Thu Apr 05 06:15:02 2018 +0000
    10.2 +++ b/src/HOL/Analysis/Measure_Space.thy	Fri Apr 06 17:34:50 2018 +0200
    10.3 @@ -11,7 +11,7 @@
    10.4    Measurable "HOL-Library.Extended_Nonnegative_Real"
    10.5  begin
    10.6  
    10.7 -subsection "Relate extended reals and the indicator function"
    10.8 +subsection%unimportant "Relate extended reals and the indicator function"
    10.9  
   10.10  lemma suminf_cmult_indicator:
   10.11    fixes f :: "nat \<Rightarrow> ennreal"
   10.12 @@ -59,7 +59,7 @@
   10.13    represent sigma algebras (with an arbitrary emeasure).
   10.14  \<close>
   10.15  
   10.16 -subsection "Extend binary sets"
   10.17 +subsection%unimportant "Extend binary sets"
   10.18  
   10.19  lemma LIMSEQ_binaryset:
   10.20    assumes f: "f {} = 0"
   10.21 @@ -91,7 +91,7 @@
   10.22    shows "f {} = 0 \<Longrightarrow> (\<Sum>n. f (binaryset A B n)) = f A + f B"
   10.23    by (metis binaryset_sums sums_unique)
   10.24  
   10.25 -subsection \<open>Properties of a premeasure @{term \<mu>}\<close>
   10.26 +subsection%unimportant \<open>Properties of a premeasure @{term \<mu>}\<close>
   10.27  
   10.28  text \<open>
   10.29    The definitions for @{const positive} and @{const countably_additive} should be here, by they are
   10.30 @@ -442,7 +442,7 @@
   10.31    using empty_continuous_imp_continuous_from_below[OF f fin] cont
   10.32    by blast
   10.33  
   10.34 -subsection \<open>Properties of @{const emeasure}\<close>
   10.35 +subsection%unimportant \<open>Properties of @{const emeasure}\<close>
   10.36  
   10.37  lemma emeasure_positive: "positive (sets M) (emeasure M)"
   10.38    by (cases M) (auto simp: sets_def emeasure_def Abs_measure_inverse measure_space_def)
   10.39 @@ -881,7 +881,7 @@
   10.40  
   10.41  subsection \<open>\<open>\<mu>\<close>-null sets\<close>
   10.42  
   10.43 -definition null_sets :: "'a measure \<Rightarrow> 'a set set" where
   10.44 +definition%important null_sets :: "'a measure \<Rightarrow> 'a set set" where
   10.45    "null_sets M = {N\<in>sets M. emeasure M N = 0}"
   10.46  
   10.47  lemma null_setsD1[dest]: "A \<in> null_sets M \<Longrightarrow> emeasure M A = 0"
   10.48 @@ -989,7 +989,7 @@
   10.49  
   10.50  subsection \<open>The almost everywhere filter (i.e.\ quantifier)\<close>
   10.51  
   10.52 -definition ae_filter :: "'a measure \<Rightarrow> 'a filter" where
   10.53 +definition%important ae_filter :: "'a measure \<Rightarrow> 'a filter" where
   10.54    "ae_filter M = (INF N:null_sets M. principal (space M - N))"
   10.55  
   10.56  abbreviation almost_everywhere :: "'a measure \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" where
   10.57 @@ -1265,7 +1265,7 @@
   10.58  
   10.59  subsection \<open>\<open>\<sigma>\<close>-finite Measures\<close>
   10.60  
   10.61 -locale sigma_finite_measure =
   10.62 +locale%important sigma_finite_measure =
   10.63    fixes M :: "'a measure"
   10.64    assumes sigma_finite_countable:
   10.65      "\<exists>A::'a set set. countable A \<and> A \<subseteq> sets M \<and> (\<Union>A) = space M \<and> (\<forall>a\<in>A. emeasure M a \<noteq> \<infinity>)"
   10.66 @@ -1387,7 +1387,7 @@
   10.67  
   10.68  subsection \<open>Measure space induced by distribution of @{const measurable}-functions\<close>
   10.69  
   10.70 -definition distr :: "'a measure \<Rightarrow> 'b measure \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b measure" where
   10.71 +definition%important distr :: "'a measure \<Rightarrow> 'b measure \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b measure" where
   10.72    "distr M N f = measure_of (space N) (sets N) (\<lambda>A. emeasure M (f -` A \<inter> space M))"
   10.73  
   10.74  lemma
   10.75 @@ -1513,12 +1513,12 @@
   10.76    "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"
   10.77    by (auto simp add: null_sets_def emeasure_distr)
   10.78  
   10.79 -lemma distr_distr:
   10.80 +lemma%important distr_distr:
   10.81    "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)"
   10.82    by (auto simp add: emeasure_distr measurable_space
   10.83             intro!: arg_cong[where f="emeasure M"] measure_eqI)
   10.84  
   10.85 -subsection \<open>Real measure values\<close>
   10.86 +subsection%unimportant \<open>Real measure values\<close>
   10.87  
   10.88  lemma ring_of_finite_sets: "ring_of_sets (space M) {A\<in>sets M. emeasure M A \<noteq> top}"
   10.89  proof (rule ring_of_setsI)
   10.90 @@ -1705,7 +1705,7 @@
   10.91  
   10.92  subsection \<open>Set of measurable sets with finite measure\<close>
   10.93  
   10.94 -definition fmeasurable :: "'a measure \<Rightarrow> 'a set set"
   10.95 +definition%important fmeasurable :: "'a measure \<Rightarrow> 'a set set"
   10.96  where
   10.97    "fmeasurable M = {A\<in>sets M. emeasure M A < \<infinity>}"
   10.98  
   10.99 @@ -1972,7 +1972,7 @@
  10.100  
  10.101  subsection \<open>Measure spaces with @{term "emeasure M (space M) < \<infinity>"}\<close>
  10.102  
  10.103 -locale finite_measure = sigma_finite_measure M for M +
  10.104 +locale%important finite_measure = sigma_finite_measure M for M +
  10.105    assumes finite_emeasure_space: "emeasure M (space M) \<noteq> top"
  10.106  
  10.107  lemma finite_measureI[Pure.intro!]:
  10.108 @@ -2194,7 +2194,7 @@
  10.109      using bound[of x] sets_eq_imp_space_eq[OF sets] by (simp add: iter)
  10.110  qed (auto simp add: iter le_fun_def INF_apply[abs_def] intro!: meas cont)
  10.111  
  10.112 -subsection \<open>Counting space\<close>
  10.113 +subsection%unimportant \<open>Counting space\<close>
  10.114  
  10.115  lemma strict_monoI_Suc:
  10.116    assumes ord [simp]: "(\<And>n. f n < f (Suc n))" shows "strict_mono f"
  10.117 @@ -2343,7 +2343,7 @@
  10.118    show "sigma_finite_measure (count_space A)" ..
  10.119  qed
  10.120  
  10.121 -subsection \<open>Measure restricted to space\<close>
  10.122 +subsection%unimportant \<open>Measure restricted to space\<close>
  10.123  
  10.124  lemma emeasure_restrict_space:
  10.125    assumes "\<Omega> \<inter> space M \<in> sets M" "A \<subseteq> \<Omega>"
  10.126 @@ -2502,7 +2502,7 @@
  10.127    finally show "emeasure M X = emeasure N X" .
  10.128  qed fact
  10.129  
  10.130 -subsection \<open>Null measure\<close>
  10.131 +subsection%unimportant \<open>Null measure\<close>
  10.132  
  10.133  definition "null_measure M = sigma (space M) (sets M)"
  10.134  
  10.135 @@ -2525,7 +2525,7 @@
  10.136  
  10.137  subsection \<open>Scaling a measure\<close>
  10.138  
  10.139 -definition scale_measure :: "ennreal \<Rightarrow> 'a measure \<Rightarrow> 'a measure"
  10.140 +definition%important scale_measure :: "ennreal \<Rightarrow> 'a measure \<Rightarrow> 'a measure"
  10.141  where
  10.142    "scale_measure r M = measure_of (space M) (sets M) (\<lambda>A. r * emeasure M A)"
  10.143  
  10.144 @@ -2703,11 +2703,11 @@
  10.145    qed auto
  10.146  qed
  10.147  
  10.148 -lemma unsigned_Hahn_decomposition:
  10.149 +lemma%important unsigned_Hahn_decomposition:
  10.150    assumes [simp]: "sets N = sets M" and [measurable]: "A \<in> sets M"
  10.151      and [simp]: "emeasure M A \<noteq> top" "emeasure N A \<noteq> top"
  10.152    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)"
  10.153 -proof -
  10.154 +proof%unimportant -
  10.155    have "\<exists>Y\<in>sets (restrict_space M A).
  10.156      (\<forall>X\<in>sets (restrict_space M A). X \<subseteq> Y \<longrightarrow> (restrict_space N A) X \<le> (restrict_space M A) X) \<and>
  10.157      (\<forall>X\<in>sets (restrict_space M A). X \<inter> Y = {} \<longrightarrow> (restrict_space M A) X \<le> (restrict_space N A) X)"
  10.158 @@ -2728,12 +2728,12 @@
  10.159      done
  10.160  qed
  10.161  
  10.162 -text \<open>
  10.163 +text%important \<open>
  10.164    Define a lexicographical order on @{type measure}, in the order space, sets and measure. The parts
  10.165    of the lexicographical order are point-wise ordered.
  10.166  \<close>
  10.167  
  10.168 -instantiation measure :: (type) order_bot
  10.169 +instantiation%important measure :: (type) order_bot
  10.170  begin
  10.171  
  10.172  inductive less_eq_measure :: "'a measure \<Rightarrow> 'a measure \<Rightarrow> bool" where
  10.173 @@ -2746,10 +2746,10 @@
  10.174      if sets M = sets N then emeasure M \<le> emeasure N else sets M \<subseteq> sets N else space M \<subseteq> space N)"
  10.175    by (auto elim: less_eq_measure.cases intro: less_eq_measure.intros)
  10.176  
  10.177 -definition less_measure :: "'a measure \<Rightarrow> 'a measure \<Rightarrow> bool" where
  10.178 +definition%important less_measure :: "'a measure \<Rightarrow> 'a measure \<Rightarrow> bool" where
  10.179    "less_measure M N \<longleftrightarrow> (M \<le> N \<and> \<not> N \<le> M)"
  10.180  
  10.181 -definition bot_measure :: "'a measure" where
  10.182 +definition%important bot_measure :: "'a measure" where
  10.183    "bot_measure = sigma {} {}"
  10.184  
  10.185  lemma
  10.186 @@ -2766,13 +2766,14 @@
  10.187  
  10.188  end
  10.189  
  10.190 -lemma le_measure: "sets M = sets N \<Longrightarrow> M \<le> N \<longleftrightarrow> (\<forall>A\<in>sets M. emeasure M A \<le> emeasure N A)"
  10.191 +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)"
  10.192 +  apply%unimportant -
  10.193    apply (auto simp: le_measure_iff le_fun_def dest: sets_eq_imp_space_eq)
  10.194    subgoal for X
  10.195      by (cases "X \<in> sets M") (auto simp: emeasure_notin_sets)
  10.196    done
  10.197  
  10.198 -definition sup_measure' :: "'a measure \<Rightarrow> 'a measure \<Rightarrow> 'a measure"
  10.199 +definition%important sup_measure' :: "'a measure \<Rightarrow> 'a measure \<Rightarrow> 'a measure"
  10.200  where
  10.201    "sup_measure' A B = measure_of (space A) (sets A) (\<lambda>X. SUP Y:sets A. emeasure A (X \<inter> Y) + emeasure B (X \<inter> - Y))"
  10.202  
  10.203 @@ -2900,7 +2901,7 @@
  10.204    qed
  10.205  qed simp_all
  10.206  
  10.207 -definition sup_lexord :: "'a \<Rightarrow> 'a \<Rightarrow> ('a \<Rightarrow> 'b::order) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a"
  10.208 +definition%important sup_lexord :: "'a \<Rightarrow> 'a \<Rightarrow> ('a \<Rightarrow> 'b::order) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a"
  10.209  where
  10.210    "sup_lexord A B k s c =
  10.211      (if k A = k B then c else if \<not> k A \<le> k B \<and> \<not> k B \<le> k A then s else if k B \<le> k A then A else B)"
  10.212 @@ -2926,10 +2927,10 @@
  10.213       (simp_all add: eq_commute[of _ "sets x"] le_measure_iff emeasure_sigma le_fun_def
  10.214                      sigma_sets_superset_generator sigma_sets_le_sets_iff)
  10.215  
  10.216 -instantiation measure :: (type) semilattice_sup
  10.217 +instantiation%important measure :: (type) semilattice_sup
  10.218  begin
  10.219  
  10.220 -definition sup_measure :: "'a measure \<Rightarrow> 'a measure \<Rightarrow> 'a measure"
  10.221 +definition%important sup_measure :: "'a measure \<Rightarrow> 'a measure \<Rightarrow> 'a measure"
  10.222  where
  10.223    "sup_measure A B =
  10.224      sup_lexord A B space (sigma (space A \<union> space B) {})
  10.225 @@ -3057,7 +3058,7 @@
  10.226      by (simp add: A(3))
  10.227  qed
  10.228  
  10.229 -instantiation measure :: (type) complete_lattice
  10.230 +instantiation%important measure :: (type) complete_lattice
  10.231  begin
  10.232  
  10.233  interpretation sup_measure: comm_monoid_set sup "bot :: 'a measure"
  10.234 @@ -3092,7 +3093,7 @@
  10.235    "finite I \<Longrightarrow> I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> sets i = sets M) \<Longrightarrow> sets (sup_measure.F id I) = sets M"
  10.236    by (induction I rule: finite_ne_induct) (simp_all add: sets_sup)
  10.237  
  10.238 -definition Sup_measure' :: "'a measure set \<Rightarrow> 'a measure"
  10.239 +definition%important Sup_measure' :: "'a measure set \<Rightarrow> 'a measure"
  10.240  where
  10.241    "Sup_measure' M = measure_of (\<Union>a\<in>M. space a) (\<Union>a\<in>M. sets a)
  10.242      (\<lambda>X. (SUP P:{P. finite P \<and> P \<subseteq> M }. sup_measure.F id P X))"
  10.243 @@ -3163,20 +3164,20 @@
  10.244      using assms * by auto
  10.245  qed (rule UN_space_closed)
  10.246  
  10.247 -definition Sup_measure :: "'a measure set \<Rightarrow> 'a measure"
  10.248 +definition%important Sup_measure :: "'a measure set \<Rightarrow> 'a measure"
  10.249  where
  10.250    "Sup_measure = Sup_lexord space (Sup_lexord sets Sup_measure'
  10.251      (\<lambda>U. sigma (\<Union>u\<in>U. space u) (\<Union>u\<in>U. sets u))) (\<lambda>U. sigma (\<Union>u\<in>U. space u) {})"
  10.252  
  10.253 -definition Inf_measure :: "'a measure set \<Rightarrow> 'a measure"
  10.254 +definition%important Inf_measure :: "'a measure set \<Rightarrow> 'a measure"
  10.255  where
  10.256    "Inf_measure A = Sup {x. \<forall>a\<in>A. x \<le> a}"
  10.257  
  10.258 -definition inf_measure :: "'a measure \<Rightarrow> 'a measure \<Rightarrow> 'a measure"
  10.259 +definition%important inf_measure :: "'a measure \<Rightarrow> 'a measure \<Rightarrow> 'a measure"
  10.260  where
  10.261    "inf_measure a b = Inf {a, b}"
  10.262  
  10.263 -definition top_measure :: "'a measure"
  10.264 +definition%important top_measure :: "'a measure"
  10.265  where
  10.266    "top_measure = Inf {}"
  10.267  
  10.268 @@ -3417,7 +3418,7 @@
  10.269    qed
  10.270  qed
  10.271  
  10.272 -subsubsection \<open>Supremum of a set of $\sigma$-algebras\<close>
  10.273 +subsubsection%unimportant \<open>Supremum of a set of $\sigma$-algebras\<close>
  10.274  
  10.275  lemma space_Sup_eq_UN: "space (Sup M) = (\<Union>x\<in>M. space x)"
  10.276    unfolding Sup_measure_def
    11.1 --- a/src/HOL/Analysis/Norm_Arith.thy	Thu Apr 05 06:15:02 2018 +0000
    11.2 +++ b/src/HOL/Analysis/Norm_Arith.thy	Fri Apr 06 17:34:50 2018 +0200
    11.3 @@ -131,14 +131,14 @@
    11.4  
    11.5  ML_file "normarith.ML"
    11.6  
    11.7 -method_setup norm = \<open>
    11.8 +method_setup%important norm = \<open>
    11.9    Scan.succeed (SIMPLE_METHOD' o NormArith.norm_arith_tac)
   11.10  \<close> "prove simple linear statements about vector norms"
   11.11  
   11.12  
   11.13  text \<open>Hence more metric properties.\<close>
   11.14  
   11.15 -lemma dist_triangle_add:
   11.16 +lemma%important dist_triangle_add:
   11.17    fixes x y x' y' :: "'a::real_normed_vector"
   11.18    shows "dist (x + y) (x' + y') \<le> dist x x' + dist y y'"
   11.19    by norm
    12.1 --- a/src/HOL/Analysis/Path_Connected.thy	Thu Apr 05 06:15:02 2018 +0000
    12.2 +++ b/src/HOL/Analysis/Path_Connected.thy	Fri Apr 06 17:34:50 2018 +0200
    12.3 @@ -10,34 +10,34 @@
    12.4  
    12.5  subsection \<open>Paths and Arcs\<close>
    12.6  
    12.7 -definition path :: "(real \<Rightarrow> 'a::topological_space) \<Rightarrow> bool"
    12.8 +definition%important path :: "(real \<Rightarrow> 'a::topological_space) \<Rightarrow> bool"
    12.9    where "path g \<longleftrightarrow> continuous_on {0..1} g"
   12.10  
   12.11 -definition pathstart :: "(real \<Rightarrow> 'a::topological_space) \<Rightarrow> 'a"
   12.12 +definition%important pathstart :: "(real \<Rightarrow> 'a::topological_space) \<Rightarrow> 'a"
   12.13    where "pathstart g = g 0"
   12.14  
   12.15 -definition pathfinish :: "(real \<Rightarrow> 'a::topological_space) \<Rightarrow> 'a"
   12.16 +definition%important pathfinish :: "(real \<Rightarrow> 'a::topological_space) \<Rightarrow> 'a"
   12.17    where "pathfinish g = g 1"
   12.18  
   12.19 -definition path_image :: "(real \<Rightarrow> 'a::topological_space) \<Rightarrow> 'a set"
   12.20 +definition%important path_image :: "(real \<Rightarrow> 'a::topological_space) \<Rightarrow> 'a set"
   12.21    where "path_image g = g ` {0 .. 1}"
   12.22  
   12.23 -definition reversepath :: "(real \<Rightarrow> 'a::topological_space) \<Rightarrow> real \<Rightarrow> 'a"
   12.24 +definition%important reversepath :: "(real \<Rightarrow> 'a::topological_space) \<Rightarrow> real \<Rightarrow> 'a"
   12.25    where "reversepath g = (\<lambda>x. g(1 - x))"
   12.26  
   12.27 -definition joinpaths :: "(real \<Rightarrow> 'a::topological_space) \<Rightarrow> (real \<Rightarrow> 'a) \<Rightarrow> real \<Rightarrow> 'a"
   12.28 +definition%important joinpaths :: "(real \<Rightarrow> 'a::topological_space) \<Rightarrow> (real \<Rightarrow> 'a) \<Rightarrow> real \<Rightarrow> 'a"
   12.29      (infixr "+++" 75)
   12.30    where "g1 +++ g2 = (\<lambda>x. if x \<le> 1/2 then g1 (2 * x) else g2 (2 * x - 1))"
   12.31  
   12.32 -definition simple_path :: "(real \<Rightarrow> 'a::topological_space) \<Rightarrow> bool"
   12.33 +definition%important simple_path :: "(real \<Rightarrow> 'a::topological_space) \<Rightarrow> bool"
   12.34    where "simple_path g \<longleftrightarrow>
   12.35       path g \<and> (\<forall>x\<in>{0..1}. \<forall>y\<in>{0..1}. g x = g y \<longrightarrow> x = y \<or> x = 0 \<and> y = 1 \<or> x = 1 \<and> y = 0)"
   12.36  
   12.37 -definition arc :: "(real \<Rightarrow> 'a :: topological_space) \<Rightarrow> bool"
   12.38 +definition%important arc :: "(real \<Rightarrow> 'a :: topological_space) \<Rightarrow> bool"
   12.39    where "arc g \<longleftrightarrow> path g \<and> inj_on g {0..1}"
   12.40  
   12.41  
   12.42 -subsection\<open>Invariance theorems\<close>
   12.43 +subsection%unimportant\<open>Invariance theorems\<close>
   12.44  
   12.45  lemma path_eq: "path p \<Longrightarrow> (\<And>t. t \<in> {0..1} \<Longrightarrow> p t = q t) \<Longrightarrow> path q"
   12.46    using continuous_on_eq path_def by blast
   12.47 @@ -132,7 +132,7 @@
   12.48    using assms inj_on_eq_iff [of f]
   12.49    by (auto simp: arc_def inj_on_def path_linear_image_eq)
   12.50  
   12.51 -subsection\<open>Basic lemmas about paths\<close>
   12.52 +subsection%unimportant\<open>Basic lemmas about paths\<close>
   12.53  
   12.54  lemma continuous_on_path: "path f \<Longrightarrow> t \<subseteq> {0..1} \<Longrightarrow> continuous_on t f"
   12.55    using continuous_on_subset path_def by blast
   12.56 @@ -301,7 +301,7 @@
   12.57      done
   12.58  qed
   12.59  
   12.60 -section \<open>Path Images\<close>
   12.61 +section%unimportant \<open>Path Images\<close>
   12.62  
   12.63  lemma bounded_path_image: "path g \<Longrightarrow> bounded(path_image g)"
   12.64    by (simp add: compact_imp_bounded compact_path_image)
   12.65 @@ -394,7 +394,7 @@
   12.66    by (auto simp: simple_path_def path_image_def inj_on_def less_eq_real_def Ball_def)
   12.67  
   12.68  
   12.69 -subsection\<open>Simple paths with the endpoints removed\<close>
   12.70 +subsection%unimportant\<open>Simple paths with the endpoints removed\<close>
   12.71  
   12.72  lemma simple_path_endless:
   12.73      "simple_path c \<Longrightarrow> path_image c - {pathstart c,pathfinish c} = c ` {0<..<1}"
   12.74 @@ -417,7 +417,7 @@
   12.75    by (simp add: simple_path_endless)
   12.76  
   12.77  
   12.78 -subsection\<open>The operations on paths\<close>
   12.79 +subsection%unimportant\<open>The operations on paths\<close>
   12.80  
   12.81  lemma path_image_subset_reversepath: "path_image(reversepath g) \<le> path_image g"
   12.82    by (auto simp: path_image_def reversepath_def)
   12.83 @@ -565,7 +565,7 @@
   12.84    by (rule ext) (auto simp: mult.commute)
   12.85  
   12.86  
   12.87 -subsection\<open>Some reversed and "if and only if" versions of joining theorems\<close>
   12.88 +subsection%unimportant\<open>Some reversed and "if and only if" versions of joining theorems\<close>
   12.89  
   12.90  lemma path_join_path_ends:
   12.91    fixes g1 :: "real \<Rightarrow> 'a::metric_space"
   12.92 @@ -698,7 +698,7 @@
   12.93  using pathfinish_in_path_image by (fastforce simp: arc_join_eq)
   12.94  
   12.95  
   12.96 -subsection\<open>The joining of paths is associative\<close>
   12.97 +subsection%unimportant\<open>The joining of paths is associative\<close>
   12.98  
   12.99  lemma path_assoc:
  12.100      "\<lbrakk>pathfinish p = pathstart q; pathfinish q = pathstart r\<rbrakk>
  12.101 @@ -748,7 +748,7 @@
  12.102        \<Longrightarrow> arc(p +++ (q +++ r)) \<longleftrightarrow> arc((p +++ q) +++ r)"
  12.103  by (simp add: arc_simple_path simple_path_assoc)
  12.104  
  12.105 -subsubsection\<open>Symmetry and loops\<close>
  12.106 +subsubsection%unimportant\<open>Symmetry and loops\<close>
  12.107  
  12.108  lemma path_sym:
  12.109      "\<lbrakk>pathfinish p = pathstart q; pathfinish q = pathstart p\<rbrakk> \<Longrightarrow> path(p +++ q) \<longleftrightarrow> path(q +++ p)"
  12.110 @@ -767,7 +767,7 @@
  12.111  
  12.112  section\<open>Choosing a subpath of an existing path\<close>
  12.113  
  12.114 -definition subpath :: "real \<Rightarrow> real \<Rightarrow> (real \<Rightarrow> 'a) \<Rightarrow> real \<Rightarrow> 'a::real_normed_vector"
  12.115 +definition%important subpath :: "real \<Rightarrow> real \<Rightarrow> (real \<Rightarrow> 'a) \<Rightarrow> real \<Rightarrow> 'a::real_normed_vector"
  12.116    where "subpath a b g \<equiv> \<lambda>x. g((b - a) * x + a)"
  12.117  
  12.118  lemma path_image_subpath_gen:
  12.119 @@ -945,7 +945,7 @@
  12.120  lemma join_subpaths_middle: "subpath (0) ((1 / 2)) p +++ subpath ((1 / 2)) 1 p = p"
  12.121    by (rule ext) (simp add: joinpaths_def subpath_def divide_simps)
  12.122  
  12.123 -subsection\<open>There is a subpath to the frontier\<close>
  12.124 +subsection%unimportant\<open>There is a subpath to the frontier\<close>
  12.125  
  12.126  lemma subpath_to_frontier_explicit:
  12.127      fixes S :: "'a::metric_space set"
  12.128 @@ -1063,7 +1063,7 @@
  12.129  
  12.130  subsection \<open>shiftpath: Reparametrizing a closed curve to start at some chosen point\<close>
  12.131  
  12.132 -definition shiftpath :: "real \<Rightarrow> (real \<Rightarrow> 'a::topological_space) \<Rightarrow> real \<Rightarrow> 'a"
  12.133 +definition%important shiftpath :: "real \<Rightarrow> (real \<Rightarrow> 'a::topological_space) \<Rightarrow> real \<Rightarrow> 'a"
  12.134    where "shiftpath a f = (\<lambda>x. if (a + x) \<le> 1 then f (a + x) else f (a + x - 1))"
  12.135  
  12.136  lemma pathstart_shiftpath: "a \<le> 1 \<Longrightarrow> pathstart (shiftpath a g) = g a"
  12.137 @@ -1179,7 +1179,7 @@
  12.138  
  12.139  subsection \<open>Special case of straight-line paths\<close>
  12.140  
  12.141 -definition linepath :: "'a::real_normed_vector \<Rightarrow> 'a \<Rightarrow> real \<Rightarrow> 'a"
  12.142 +definition%important linepath :: "'a::real_normed_vector \<Rightarrow> 'a \<Rightarrow> real \<Rightarrow> 'a"
  12.143    where "linepath a b = (\<lambda>x. (1 - x) *\<^sub>R a + x *\<^sub>R b)"
  12.144  
  12.145  lemma pathstart_linepath[simp]: "pathstart (linepath a b) = a"
  12.146 @@ -1259,7 +1259,7 @@
  12.147  qed
  12.148  
  12.149  
  12.150 -subsection\<open>Segments via convex hulls\<close>
  12.151 +subsection%unimportant\<open>Segments via convex hulls\<close>
  12.152  
  12.153  lemma segments_subset_convex_hull:
  12.154      "closed_segment a b \<subseteq> (convex hull {a,b,c})"
  12.155 @@ -1379,7 +1379,7 @@
  12.156      by (force simp: inj_on_def)
  12.157  qed
  12.158  
  12.159 -subsection \<open>Bounding a point away from a path\<close>
  12.160 +subsection%unimportant \<open>Bounding a point away from a path\<close>
  12.161  
  12.162  lemma not_on_path_ball:
  12.163    fixes g :: "real \<Rightarrow> 'a::heine_borel"
  12.164 @@ -1416,10 +1416,10 @@
  12.165  
  12.166  section \<open>Path component, considered as a "joinability" relation (from Tom Hales)\<close>
  12.167  
  12.168 -definition "path_component s x y \<longleftrightarrow>
  12.169 +definition%important "path_component s x y \<longleftrightarrow>
  12.170    (\<exists>g. path g \<and> path_image g \<subseteq> s \<and> pathstart g = x \<and> pathfinish g = y)"
  12.171  
  12.172 -abbreviation
  12.173 +abbreviation%important
  12.174     "path_component_set s x \<equiv> Collect (path_component s x)"
  12.175  
  12.176  lemmas path_defs = path_def pathstart_def pathfinish_def path_image_def path_component_def
  12.177 @@ -1471,7 +1471,7 @@
  12.178    done
  12.179  
  12.180  
  12.181 -subsubsection \<open>Path components as sets\<close>
  12.182 +subsubsection%unimportant \<open>Path components as sets\<close>
  12.183  
  12.184  lemma path_component_set:
  12.185    "path_component_set s x =
  12.186 @@ -1495,7 +1495,7 @@
  12.187  
  12.188  subsection \<open>Path connectedness of a space\<close>
  12.189  
  12.190 -definition "path_connected s \<longleftrightarrow>
  12.191 +definition%important "path_connected s \<longleftrightarrow>
  12.192    (\<forall>x\<in>s. \<forall>y\<in>s. \<exists>g. path g \<and> path_image g \<subseteq> s \<and> pathstart g = x \<and> pathfinish g = y)"
  12.193  
  12.194  lemma path_connected_component: "path_connected s \<longleftrightarrow> (\<forall>x\<in>s. \<forall>y\<in>s. path_component s x y)"
  12.195 @@ -1806,7 +1806,7 @@
  12.196      using path_component_eq_empty by auto
  12.197  qed
  12.198  
  12.199 -subsection\<open>Lemmas about path-connectedness\<close>
  12.200 +subsection%unimportant\<open>Lemmas about path-connectedness\<close>
  12.201  
  12.202  lemma path_connected_linear_image:
  12.203    fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
  12.204 @@ -1878,7 +1878,7 @@
  12.205  using is_interval_connected_1 is_interval_path_connected path_connected_imp_connected by blast
  12.206  
  12.207  
  12.208 -subsection\<open>Path components\<close>
  12.209 +subsection%unimportant\<open>Path components\<close>
  12.210  
  12.211  lemma Union_path_component [simp]:
  12.212     "Union {path_component_set S x |x. x \<in> S} = S"
  12.213 @@ -1990,11 +1990,11 @@
  12.214    "2 \<le> DIM('N::euclidean_space) \<Longrightarrow> connected(- {a::'N})"
  12.215    by (simp add: path_connected_punctured_universe path_connected_imp_connected)
  12.216  
  12.217 -lemma path_connected_sphere:
  12.218 +lemma%important path_connected_sphere:
  12.219    fixes a :: "'a :: euclidean_space"
  12.220    assumes "2 \<le> DIM('a)"
  12.221    shows "path_connected(sphere a r)"
  12.222 -proof (cases r "0::real" rule: linorder_cases)
  12.223 +proof%unimportant (cases r "0::real" rule: linorder_cases)
  12.224    case less
  12.225    then show ?thesis
  12.226      by (simp add: path_connected_empty)
  12.227 @@ -2315,26 +2315,26 @@
  12.228      using path_connected_translation by metis
  12.229  qed
  12.230  
  12.231 -lemma path_connected_annulus:
  12.232 +lemma%important path_connected_annulus:
  12.233    fixes a :: "'N::euclidean_space"
  12.234    assumes "2 \<le> DIM('N)"
  12.235    shows "path_connected {x. r1 < norm(x - a) \<and> norm(x - a) < r2}"
  12.236          "path_connected {x. r1 < norm(x - a) \<and> norm(x - a) \<le> r2}"
  12.237          "path_connected {x. r1 \<le> norm(x - a) \<and> norm(x - a) < r2}"
  12.238          "path_connected {x. r1 \<le> norm(x - a) \<and> norm(x - a) \<le> r2}"
  12.239 -  by (auto simp: is_interval_def intro!: is_interval_convex convex_imp_path_connected path_connected_2DIM_I [OF assms])
  12.240 -
  12.241 -lemma connected_annulus:
  12.242 +  by%unimportant (auto simp: is_interval_def intro!: is_interval_convex convex_imp_path_connected path_connected_2DIM_I [OF assms])
  12.243 +
  12.244 +lemma%important connected_annulus:
  12.245    fixes a :: "'N::euclidean_space"
  12.246    assumes "2 \<le> DIM('N::euclidean_space)"
  12.247    shows "connected {x. r1 < norm(x - a) \<and> norm(x - a) < r2}"
  12.248          "connected {x. r1 < norm(x - a) \<and> norm(x - a) \<le> r2}"
  12.249          "connected {x. r1 \<le> norm(x - a) \<and> norm(x - a) < r2}"
  12.250          "connected {x. r1 \<le> norm(x - a) \<and> norm(x - a) \<le> r2}"
  12.251 -  by (auto simp: path_connected_annulus [OF assms] path_connected_imp_connected)
  12.252 -
  12.253 -
  12.254 -subsection\<open>Relations between components and path components\<close>
  12.255 +  by%unimportant (auto simp: path_connected_annulus [OF assms] path_connected_imp_connected)
  12.256 +
  12.257 +
  12.258 +subsection%unimportant\<open>Relations between components and path components\<close>
  12.259  
  12.260  lemma open_connected_component:
  12.261    fixes s :: "'a::real_normed_vector set"
  12.262 @@ -2439,7 +2439,7 @@
  12.263  qed
  12.264  
  12.265  
  12.266 -subsection\<open>Existence of unbounded components\<close>
  12.267 +subsection%unimportant\<open>Existence of unbounded components\<close>
  12.268  
  12.269  lemma cobounded_unbounded_component:
  12.270      fixes s :: "'a :: euclidean_space set"
  12.271 @@ -2527,13 +2527,13 @@
  12.272  
  12.273  section\<open>The "inside" and "outside" of a set\<close>
  12.274  
  12.275 -text\<open>The inside comprises the points in a bounded connected component of the set's complement.
  12.276 +text%important\<open>The inside comprises the points in a bounded connected component of the set's complement.
  12.277    The outside comprises the points in unbounded connected component of the complement.\<close>
  12.278  
  12.279 -definition inside where
  12.280 +definition%important inside where
  12.281    "inside s \<equiv> {x. (x \<notin> s) \<and> bounded(connected_component_set ( - s) x)}"
  12.282  
  12.283 -definition outside where
  12.284 +definition%important outside where
  12.285    "outside s \<equiv> -s \<inter> {x. ~ bounded(connected_component_set (- s) x)}"
  12.286  
  12.287  lemma outside: "outside s = {x. ~ bounded(connected_component_set (- s) x)}"
  12.288 @@ -3329,14 +3329,14 @@
  12.289  
  12.290  subsection\<open>Condition for an open map's image to contain a ball\<close>
  12.291  
  12.292 -lemma ball_subset_open_map_image:
  12.293 +lemma%important ball_subset_open_map_image:
  12.294    fixes f :: "'a::heine_borel \<Rightarrow> 'b :: {real_normed_vector,heine_borel}"
  12.295    assumes contf: "continuous_on (closure S) f"
  12.296        and oint: "open (f ` interior S)"
  12.297        and le_no: "\<And>z. z \<in> frontier S \<Longrightarrow> r \<le> norm(f z - f a)"
  12.298        and "bounded S" "a \<in> S" "0 < r"
  12.299      shows "ball (f a) r \<subseteq> f ` S"
  12.300 -proof (cases "f ` S = UNIV")
  12.301 +proof%unimportant (cases "f ` S = UNIV")
  12.302    case True then show ?thesis by simp
  12.303  next
  12.304    case False
  12.305 @@ -3382,10 +3382,10 @@
  12.306  
  12.307  section\<open> Homotopy of maps p,q : X=>Y with property P of all intermediate maps.\<close>
  12.308  
  12.309 -text\<open> We often just want to require that it fixes some subset, but to take in
  12.310 +text%important\<open> We often just want to require that it fixes some subset, but to take in
  12.311    the case of a loop homotopy, it's convenient to have a general property P.\<close>
  12.312  
  12.313 -definition homotopic_with ::
  12.314 +definition%important homotopic_with ::
  12.315    "[('a::topological_space \<Rightarrow> 'b::topological_space) \<Rightarrow> bool, 'a set, 'b set, 'a \<Rightarrow> 'b, 'a \<Rightarrow> 'b] \<Rightarrow> bool"
  12.316  where
  12.317   "homotopic_with P X Y p q \<equiv>
  12.318 @@ -3487,7 +3487,7 @@
  12.319  qed
  12.320  
  12.321  
  12.322 -subsection\<open> Trivial properties.\<close>
  12.323 +subsection%unimportant\<open> Trivial properties.\<close>
  12.324  
  12.325  lemma homotopic_with_imp_property: "homotopic_with P X Y f g \<Longrightarrow> P f \<and> P g"
  12.326    unfolding homotopic_with_def Ball_def
  12.327 @@ -3745,7 +3745,7 @@
  12.328  subsection\<open>Homotopy of paths, maintaining the same endpoints.\<close>
  12.329  
  12.330  
  12.331 -definition homotopic_paths :: "['a set, real \<Rightarrow> 'a, real \<Rightarrow> 'a::topological_space] \<Rightarrow> bool"
  12.332 +definition%important homotopic_paths :: "['a set, real \<Rightarrow> 'a, real \<Rightarrow> 'a::topological_space] \<Rightarrow> bool"
  12.333    where
  12.334       "homotopic_paths s p q \<equiv>
  12.335         homotopic_with (\<lambda>r. pathstart r = pathstart p \<and> pathfinish r = pathfinish p) {0..1} s p q"
  12.336 @@ -3897,28 +3897,28 @@
  12.337  
  12.338  subsection\<open>Group properties for homotopy of paths\<close>
  12.339  
  12.340 -text\<open>So taking equivalence classes under homotopy would give the fundamental group\<close>
  12.341 -
  12.342 -proposition homotopic_paths_rid:
  12.343 +text%important\<open>So taking equivalence classes under homotopy would give the fundamental group\<close>
  12.344 +
  12.345 +proposition%important homotopic_paths_rid:
  12.346      "\<lbrakk>path p; path_image p \<subseteq> s\<rbrakk> \<Longrightarrow> homotopic_paths s (p +++ linepath (pathfinish p) (pathfinish p)) p"
  12.347 -  apply (subst homotopic_paths_sym)
  12.348 +  apply%unimportant (subst homotopic_paths_sym)
  12.349    apply (rule homotopic_paths_reparametrize [where f = "\<lambda>t. if  t \<le> 1 / 2 then 2 *\<^sub>R t else 1"])
  12.350    apply (simp_all del: le_divide_eq_numeral1)
  12.351    apply (subst split_01)
  12.352    apply (rule continuous_on_cases continuous_intros | force simp: pathfinish_def joinpaths_def)+
  12.353    done
  12.354  
  12.355 -proposition homotopic_paths_lid:
  12.356 +proposition%important homotopic_paths_lid:
  12.357     "\<lbrakk>path p; path_image p \<subseteq> s\<rbrakk> \<Longrightarrow> homotopic_paths s (linepath (pathstart p) (pathstart p) +++ p) p"
  12.358 -using homotopic_paths_rid [of "reversepath p" s]
  12.359 +using%unimportant homotopic_paths_rid [of "reversepath p" s]
  12.360    by (metis homotopic_paths_reversepath path_image_reversepath path_reversepath pathfinish_linepath
  12.361          pathfinish_reversepath reversepath_joinpaths reversepath_linepath)
  12.362  
  12.363 -proposition homotopic_paths_assoc:
  12.364 +proposition%important homotopic_paths_assoc:
  12.365     "\<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;
  12.366       pathfinish q = pathstart r\<rbrakk>
  12.367      \<Longrightarrow> homotopic_paths s (p +++ (q +++ r)) ((p +++ q) +++ r)"
  12.368 -  apply (subst homotopic_paths_sym)
  12.369 +  apply%unimportant (subst homotopic_paths_sym)
  12.370    apply (rule homotopic_paths_reparametrize
  12.371             [where f = "\<lambda>t. if  t \<le> 1 / 2 then inverse 2 *\<^sub>R t
  12.372                             else if  t \<le> 3 / 4 then t - (1 / 4)
  12.373 @@ -3929,10 +3929,10 @@
  12.374    apply (auto simp: joinpaths_def)
  12.375    done
  12.376  
  12.377 -proposition homotopic_paths_rinv:
  12.378 +proposition%important homotopic_paths_rinv:
  12.379    assumes "path p" "path_image p \<subseteq> s"
  12.380      shows "homotopic_paths s (p +++ reversepath p) (linepath (pathstart p) (pathstart p))"
  12.381 -proof -
  12.382 +proof%unimportant -
  12.383    have "continuous_on ({0..1} \<times> {0..1}) (\<lambda>x. (subpath 0 (fst x) p +++ reversepath (subpath 0 (fst x) p)) (snd x))"
  12.384      using assms
  12.385      apply (simp add: joinpaths_def subpath_def reversepath_def path_def del: le_divide_eq_numeral1)
  12.386 @@ -3952,15 +3952,15 @@
  12.387      done
  12.388  qed
  12.389  
  12.390 -proposition homotopic_paths_linv:
  12.391 +proposition%important homotopic_paths_linv:
  12.392    assumes "path p" "path_image p \<subseteq> s"
  12.393      shows "homotopic_paths s (reversepath p +++ p) (linepath (pathfinish p) (pathfinish p))"
  12.394 -using homotopic_paths_rinv [of "reversepath p" s] assms by simp
  12.395 +using%unimportant homotopic_paths_rinv [of "reversepath p" s] assms by simp
  12.396  
  12.397  
  12.398  subsection\<open> Homotopy of loops without requiring preservation of endpoints.\<close>
  12.399  
  12.400 -definition homotopic_loops :: "'a::topological_space set \<Rightarrow> (real \<Rightarrow> 'a) \<Rightarrow> (real \<Rightarrow> 'a) \<Rightarrow> bool"  where
  12.401 +definition%important homotopic_loops :: "'a::topological_space set \<Rightarrow> (real \<Rightarrow> 'a) \<Rightarrow> (real \<Rightarrow> 'a) \<Rightarrow> bool"  where
  12.402   "homotopic_loops s p q \<equiv>
  12.403       homotopic_with (\<lambda>r. pathfinish r = pathstart r) {0..1} s p q"
  12.404  
  12.405 @@ -4025,14 +4025,14 @@
  12.406  
  12.407  subsection\<open>Relations between the two variants of homotopy\<close>
  12.408  
  12.409 -proposition homotopic_paths_imp_homotopic_loops:
  12.410 +proposition%important homotopic_paths_imp_homotopic_loops:
  12.411      "\<lbrakk>homotopic_paths s p q; pathfinish p = pathstart p; pathfinish q = pathstart p\<rbrakk> \<Longrightarrow> homotopic_loops s p q"
  12.412 -  by (auto simp: homotopic_paths_def homotopic_loops_def intro: homotopic_with_mono)
  12.413 -
  12.414 -proposition homotopic_loops_imp_homotopic_paths_null:
  12.415 +  by%unimportant (auto simp: homotopic_paths_def homotopic_loops_def intro: homotopic_with_mono)
  12.416 +
  12.417 +proposition%important homotopic_loops_imp_homotopic_paths_null:
  12.418    assumes "homotopic_loops s p (linepath a a)"
  12.419      shows "homotopic_paths s p (linepath (pathstart p) (pathstart p))"
  12.420 -proof -
  12.421 +proof%unimportant -
  12.422    have "path p" by (metis assms homotopic_loops_imp_path)
  12.423    have ploop: "pathfinish p = pathstart p" by (metis assms homotopic_loops_imp_loop)
  12.424    have pip: "path_image p \<subseteq> s" by (metis assms homotopic_loops_imp_subset)
  12.425 @@ -4100,12 +4100,12 @@
  12.426      by (blast intro: homotopic_paths_trans)
  12.427  qed
  12.428  
  12.429 -proposition homotopic_loops_conjugate:
  12.430 +proposition%important homotopic_loops_conjugate:
  12.431    fixes s :: "'a::real_normed_vector set"
  12.432    assumes "path p" "path q" and pip: "path_image p \<subseteq> s" and piq: "path_image q \<subseteq> s"
  12.433        and papp: "pathfinish p = pathstart q" and qloop: "pathfinish q = pathstart q"
  12.434      shows "homotopic_loops s (p +++ q +++ reversepath p) q"
  12.435 -proof -
  12.436 +proof%unimportant -
  12.437    have contp: "continuous_on {0..1} p"  using \<open>path p\<close> [unfolded path_def] by blast
  12.438    have contq: "continuous_on {0..1} q"  using \<open>path q\<close> [unfolded path_def] by blast
  12.439    have c1: "continuous_on ({0..1} \<times> {0..1}) (\<lambda>x. p ((1 - fst x) * snd x + fst x))"
  12.440 @@ -4197,7 +4197,7 @@
  12.441  qed
  12.442  
  12.443  
  12.444 -subsection\<open> Homotopy of "nearby" function, paths and loops.\<close>
  12.445 +subsection%unimportant\<open> Homotopy of "nearby" function, paths and loops.\<close>
  12.446  
  12.447  lemma homotopic_with_linear:
  12.448    fixes f g :: "_ \<Rightarrow> 'b::real_normed_vector"
  12.449 @@ -4358,10 +4358,10 @@
  12.450      using homotopic_join_subpaths2 by blast
  12.451  qed
  12.452  
  12.453 -proposition homotopic_join_subpaths:
  12.454 +proposition%important homotopic_join_subpaths:
  12.455     "\<lbrakk>path g; path_image g \<subseteq> s; u \<in> {0..1}; v \<in> {0..1}; w \<in> {0..1}\<rbrakk>
  12.456      \<Longrightarrow> homotopic_paths s (subpath u v g +++ subpath v w g) (subpath u w g)"
  12.457 -apply (rule le_cases3 [of u v w])
  12.458 +apply%unimportant (rule le_cases3 [of u v w])
  12.459  using homotopic_join_subpaths1 homotopic_join_subpaths2 homotopic_join_subpaths3 by metis+
  12.460  
  12.461  text\<open>Relating homotopy of trivial loops to path-connectedness.\<close>
  12.462 @@ -4399,9 +4399,9 @@
  12.463  
  12.464  subsection\<open>Simply connected sets\<close>
  12.465  
  12.466 -text\<open>defined as "all loops are homotopic (as loops)\<close>
  12.467 -
  12.468 -definition simply_connected where
  12.469 +text%important\<open>defined as "all loops are homotopic (as loops)\<close>
  12.470 +
  12.471 +definition%important simply_connected where
  12.472    "simply_connected S \<equiv>
  12.473          \<forall>p q. path p \<and> pathfinish p = pathstart p \<and> path_image p \<subseteq> S \<and>
  12.474                path q \<and> pathfinish q = pathstart q \<and> path_image q \<subseteq> S
  12.475 @@ -4583,7 +4583,7 @@
  12.476  
  12.477  subsection\<open>Contractible sets\<close>
  12.478  
  12.479 -definition contractible where
  12.480 +definition%important contractible where
  12.481   "contractible S \<equiv> \<exists>a. homotopic_with (\<lambda>x. True) S S id (\<lambda>x. a)"
  12.482  
  12.483  proposition contractible_imp_simply_connected:
  12.484 @@ -4846,7 +4846,7 @@
  12.485  
  12.486  subsection\<open>Local versions of topological properties in general\<close>
  12.487  
  12.488 -definition locally :: "('a::topological_space set \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> bool"
  12.489 +definition%important locally :: "('a::topological_space set \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> bool"
  12.490  where
  12.491   "locally P S \<equiv>
  12.492          \<forall>w x. openin (subtopology euclidean S) w \<and> x \<in> w
  12.493 @@ -5077,7 +5077,7 @@
  12.494  
  12.495  subsection\<open>Sort of induction principle for connected sets\<close>
  12.496  
  12.497 -lemma connected_induction:
  12.498 +lemma%important connected_induction:
  12.499    assumes "connected S"
  12.500        and opD: "\<And>T a. \<lbrakk>openin (subtopology euclidean S) T; a \<in> T\<rbrakk> \<Longrightarrow> \<exists>z. z \<in> T \<and> P z"
  12.501        and opI: "\<And>a. a \<in> S
  12.502 @@ -5085,7 +5085,7 @@
  12.503                       (\<forall>x \<in> T. \<forall>y \<in> T. P x \<and> P y \<and> Q x \<longrightarrow> Q y)"
  12.504        and etc: "a \<in> S" "b \<in> S" "P a" "P b" "Q a"
  12.505      shows "Q b"
  12.506 -proof -
  12.507 +proof%unimportant -
  12.508    have 1: "openin (subtopology euclidean S)
  12.509               {b. \<exists>T. openin (subtopology euclidean S) T \<and>
  12.510                       b \<in> T \<and> (\<forall>x\<in>T. P x \<longrightarrow> Q x)}"
  12.511 @@ -5176,14 +5176,14 @@
  12.512  
  12.513  subsection\<open>Basic properties of local compactness\<close>
  12.514  
  12.515 -lemma locally_compact:
  12.516 +lemma%important locally_compact:
  12.517    fixes s :: "'a :: metric_space set"
  12.518    shows
  12.519      "locally compact s \<longleftrightarrow>
  12.520       (\<forall>x \<in> s. \<exists>u v. x \<in> u \<and> u \<subseteq> v \<and> v \<subseteq> s \<and>
  12.521                      openin (subtopology euclidean s) u \<and> compact v)"
  12.522       (is "?lhs = ?rhs")
  12.523 -proof
  12.524 +proof%unimportant
  12.525    assume ?lhs
  12.526    then show ?rhs
  12.527      apply clarify
  12.528 @@ -5730,12 +5730,12 @@
  12.529      by (metis \<open>U = S \<inter> V\<close> inf.bounded_iff openin_imp_subset that)
  12.530  qed
  12.531  
  12.532 -corollary Sura_Bura:
  12.533 +corollary%important Sura_Bura:
  12.534    fixes S :: "'a::euclidean_space set"
  12.535    assumes "locally compact S" "C \<in> components S" "compact C"
  12.536    shows "C = \<Inter> {K. C \<subseteq> K \<and> compact K \<and> openin (subtopology euclidean S) K}"
  12.537           (is "C = ?rhs")
  12.538 -proof
  12.539 +proof%unimportant
  12.540    show "?rhs \<subseteq> C"
  12.541    proof (clarsimp, rule ccontr)
  12.542      fix x
  12.543 @@ -5865,17 +5865,17 @@
  12.544      by (metis assms(1) assms(2) assms(3) mem_Collect_eq path_component_subset path_connected_path_component)
  12.545  qed
  12.546  
  12.547 -proposition locally_path_connected:
  12.548 +proposition%important locally_path_connected:
  12.549    "locally path_connected S \<longleftrightarrow>
  12.550     (\<forall>v x. openin (subtopology euclidean S) v \<and> x \<in> v
  12.551            \<longrightarrow> (\<exists>u. openin (subtopology euclidean S) u \<and> path_connected u \<and> x \<in> u \<and> u \<subseteq> v))"
  12.552 -by (metis locally_path_connected_1 locally_path_connected_2 locally_path_connected_3)
  12.553 -
  12.554 -proposition locally_path_connected_open_path_component:
  12.555 +by%unimportant (metis locally_path_connected_1 locally_path_connected_2 locally_path_connected_3)
  12.556 +
  12.557 +proposition%important locally_path_connected_open_path_component:
  12.558    "locally path_connected S \<longleftrightarrow>
  12.559     (\<forall>t x. openin (subtopology euclidean S) t \<and> x \<in> t
  12.560            \<longrightarrow> openin (subtopology euclidean S) (path_component_set t x))"
  12.561 -by (metis locally_path_connected_1 locally_path_connected_2 locally_path_connected_3)
  12.562 +by%unimportant (metis locally_path_connected_1 locally_path_connected_2 locally_path_connected_3)
  12.563  
  12.564  lemma locally_connected_open_component:
  12.565    "locally connected S \<longleftrightarrow>
  12.566 @@ -5883,14 +5883,14 @@
  12.567            \<longrightarrow> openin (subtopology euclidean S) c)"
  12.568  by (metis components_iff locally_connected_open_connected_component)
  12.569  
  12.570 -proposition locally_connected_im_kleinen:
  12.571 +proposition%important locally_connected_im_kleinen:
  12.572    "locally connected S \<longleftrightarrow>
  12.573     (\<forall>v x. openin (subtopology euclidean S) v \<and> x \<in> v
  12.574         \<longrightarrow> (\<exists>u. openin (subtopology euclidean S) u \<and>
  12.575                  x \<in> u \<and> u \<subseteq> v \<and>
  12.576                  (\<forall>y. y \<in> u \<longrightarrow> (\<exists>c. connected c \<and> c \<subseteq> v \<and> x \<in> c \<and> y \<in> c))))"
  12.577     (is "?lhs = ?rhs")
  12.578 -proof
  12.579 +proof%unimportant
  12.580    assume ?lhs
  12.581    then show ?rhs
  12.582      by (fastforce simp add: locally_connected)
  12.583 @@ -5924,7 +5924,7 @@
  12.584      done
  12.585  qed
  12.586  
  12.587 -proposition locally_path_connected_im_kleinen:
  12.588 +proposition%important locally_path_connected_im_kleinen:
  12.589    "locally path_connected S \<longleftrightarrow>
  12.590     (\<forall>v x. openin (subtopology euclidean S) v \<and> x \<in> v
  12.591         \<longrightarrow> (\<exists>u. openin (subtopology euclidean S) u \<and>
  12.592 @@ -5932,7 +5932,7 @@
  12.593                  (\<forall>y. y \<in> u \<longrightarrow> (\<exists>p. path p \<and> path_image p \<subseteq> v \<and>
  12.594                                  pathstart p = x \<and> pathfinish p = y))))"
  12.595     (is "?lhs = ?rhs")
  12.596 -proof
  12.597 +proof%unimportant
  12.598    assume ?lhs
  12.599    then show ?rhs
  12.600      apply (simp add: locally_path_connected path_connected_def)
  12.601 @@ -6082,13 +6082,13 @@
  12.602    shows "open S \<Longrightarrow> path_component_set S x = connected_component_set S x"
  12.603  by (simp add: open_path_connected_component)
  12.604  
  12.605 -proposition locally_connected_quotient_image:
  12.606 +proposition%important locally_connected_quotient_image:
  12.607    assumes lcS: "locally connected S"
  12.608        and oo: "\<And>T. T \<subseteq> f ` S
  12.609                  \<Longrightarrow> openin (subtopology euclidean S) (S \<inter> f -` T) \<longleftrightarrow>
  12.610                      openin (subtopology euclidean (f ` S)) T"
  12.611      shows "locally connected (f ` S)"
  12.612 -proof (clarsimp simp: locally_connected_open_component)
  12.613 +proof%unimportant (clarsimp simp: locally_connected_open_component)
  12.614    fix U C
  12.615    assume opefSU: "openin (subtopology euclidean (f ` S)) U" and "C \<in> components U"
  12.616    then have "C \<subseteq> U" "U \<subseteq> f ` S"
  12.617 @@ -6148,12 +6148,12 @@
  12.618  qed
  12.619  
  12.620  text\<open>The proof resembles that above but is not identical!\<close>
  12.621 -proposition locally_path_connected_quotient_image:
  12.622 +proposition%important locally_path_connected_quotient_image:
  12.623    assumes lcS: "locally path_connected S"
  12.624        and oo: "\<And>T. T \<subseteq> f ` S
  12.625                  \<Longrightarrow> openin (subtopology euclidean S) (S \<inter> f -` T) \<longleftrightarrow> openin (subtopology euclidean (f ` S)) T"
  12.626      shows "locally path_connected (f ` S)"
  12.627 -proof (clarsimp simp: locally_path_connected_open_path_component)
  12.628 +proof%unimportant (clarsimp simp: locally_path_connected_open_path_component)
  12.629    fix U y
  12.630    assume opefSU: "openin (subtopology euclidean (f ` S)) U" and "y \<in> U"
  12.631    then have "path_component_set U y \<subseteq> U" "U \<subseteq> f ` S"
  12.632 @@ -6221,7 +6221,7 @@
  12.633      by metis
  12.634  qed
  12.635  
  12.636 -subsection\<open>Components, continuity, openin, closedin\<close>
  12.637 +subsection%unimportant\<open>Components, continuity, openin, closedin\<close>
  12.638  
  12.639  lemma continuous_on_components_gen:
  12.640   fixes f :: "'a::topological_space \<Rightarrow> 'b::topological_space"
  12.641 @@ -6324,7 +6324,8 @@
  12.642    fixes S :: "'a::real_normed_vector set"
  12.643    assumes S: "closed S" and c: " c \<in> components(-S)"
  12.644      shows "closed (S \<union> c)"
  12.645 -by (metis Compl_eq_Diff_UNIV S c closed_closedin closedin_Un_complement_component locally_connected_UNIV subtopology_UNIV)
  12.646 +  by (metis Compl_eq_Diff_UNIV S c closed_closedin closedin_Un_complement_component
  12.647 +      locally_connected_UNIV subtopology_UNIV)
  12.648  
  12.649  
  12.650  subsection\<open>Existence of isometry between subspaces of same dimension\<close>
  12.651 @@ -6381,7 +6382,7 @@
  12.652      by (rule that [OF \<open>linear f\<close> \<open>f ` S \<subseteq> T\<close>])
  12.653  qed
  12.654  
  12.655 -proposition isometries_subspaces:
  12.656 +proposition%important isometries_subspaces:
  12.657    fixes S :: "'a::euclidean_space set"
  12.658      and T :: "'b::euclidean_space set"
  12.659    assumes S: "subspace S"
  12.660 @@ -6392,7 +6393,7 @@
  12.661                      "\<And>x. x \<in> T \<Longrightarrow> norm(g x) = norm x"
  12.662                      "\<And>x. x \<in> S \<Longrightarrow> g(f x) = x"
  12.663                      "\<And>x. x \<in> T \<Longrightarrow> f(g x) = x"
  12.664 -proof -
  12.665 +proof%unimportant -
  12.666    obtain B where "B \<subseteq> S" and Borth: "pairwise orthogonal B"
  12.667               and B1: "\<And>x. x \<in> B \<Longrightarrow> norm x = 1"
  12.668               and "independent B" "finite B" "card B = dim S" "span B = S"
  12.669 @@ -6549,7 +6550,7 @@
  12.670  
  12.671  subsection\<open>Retracts, in a general sense, preserve (co)homotopic triviality)\<close>
  12.672  
  12.673 -locale Retracts =
  12.674 +locale%important Retracts =
  12.675    fixes s h t k
  12.676    assumes conth: "continuous_on s h"
  12.677        and imh: "h ` s = t"
  12.678 @@ -6715,7 +6716,7 @@
  12.679  
  12.680  subsection\<open>Homotopy equivalence\<close>
  12.681  
  12.682 -definition homotopy_eqv :: "'a::topological_space set \<Rightarrow> 'b::topological_space set \<Rightarrow> bool"
  12.683 +definition%important homotopy_eqv :: "'a::topological_space set \<Rightarrow> 'b::topological_space set \<Rightarrow> bool"
  12.684               (infix "homotopy'_eqv" 50)
  12.685    where "S homotopy_eqv T \<equiv>
  12.686          \<exists>f g. continuous_on S f \<and> f ` S \<subseteq> T \<and>
  12.687 @@ -7003,7 +7004,7 @@
  12.688    shows "\<lbrakk>contractible S; S homeomorphic T\<rbrakk> \<Longrightarrow> contractible T"
  12.689    by (metis homeomorphic_contractible_eq)
  12.690  
  12.691 -subsection\<open>Misc other results\<close>
  12.692 +subsection%unimportant\<open>Misc other results\<close>
  12.693  
  12.694  lemma bounded_connected_Compl_real:
  12.695    fixes S :: "real set"
  12.696 @@ -7047,7 +7048,7 @@
  12.697      by blast
  12.698  qed
  12.699  
  12.700 -subsection\<open>Some Uncountable Sets\<close>
  12.701 +subsection%unimportant\<open>Some Uncountable Sets\<close>
  12.702  
  12.703  lemma uncountable_closed_segment:
  12.704    fixes a :: "'a::real_normed_vector"
  12.705 @@ -7186,7 +7187,7 @@
  12.706    by (simp add: arc_imp_simple_path assms simple_path_image_uncountable)
  12.707  
  12.708  
  12.709 -subsection\<open> Some simple positive connection theorems\<close>
  12.710 +subsection%unimportant\<open> Some simple positive connection theorems\<close>
  12.711  
  12.712  proposition path_connected_convex_diff_countable:
  12.713    fixes U :: "'a::euclidean_space set"
  12.714 @@ -7453,7 +7454,7 @@
  12.715  
  12.716  subsection\<open> Self-homeomorphisms shuffling points about in various ways.\<close>
  12.717  
  12.718 -subsubsection\<open>The theorem \<open>homeomorphism_moving_points_exists\<close>\<close>
  12.719 +subsubsection%unimportant\<open>The theorem \<open>homeomorphism_moving_points_exists\<close>\<close>
  12.720  
  12.721  lemma homeomorphism_moving_point_1:
  12.722    fixes a :: "'a::euclidean_space"
  12.723 @@ -7845,7 +7846,7 @@
  12.724    qed
  12.725  qed
  12.726  
  12.727 -proposition homeomorphism_moving_points_exists:
  12.728 +proposition%important homeomorphism_moving_points_exists:
  12.729    fixes S :: "'a::euclidean_space set"
  12.730    assumes 2: "2 \<le> DIM('a)" "open S" "connected S" "S \<subseteq> T" "finite K"
  12.731        and KS: "\<And>i. i \<in> K \<Longrightarrow> x i \<in> S \<and> y i \<in> S"
  12.732 @@ -7853,7 +7854,7 @@
  12.733        and S: "S \<subseteq> T" "T \<subseteq> affine hull S" "connected S"
  12.734    obtains f g where "homeomorphism T T f g" "\<And>i. i \<in> K \<Longrightarrow> f(x i) = y i"
  12.735                      "{x. ~ (f x = x \<and> g x = x)} \<subseteq> S" "bounded {x. (~ (f x = x \<and> g x = x))}"
  12.736 -proof (cases "S = {}")
  12.737 +proof%unimportant (cases "S = {}")
  12.738    case True
  12.739    then show ?thesis
  12.740      using KS homeomorphism_ident that by fastforce
  12.741 @@ -7875,7 +7876,7 @@
  12.742  qed
  12.743  
  12.744  
  12.745 -subsubsection\<open>The theorem \<open>homeomorphism_grouping_points_exists\<close>\<close>
  12.746 +subsubsection%unimportant\<open>The theorem \<open>homeomorphism_grouping_points_exists\<close>\<close>
  12.747  
  12.748  lemma homeomorphism_grouping_point_1:
  12.749    fixes a::real and c::real
  12.750 @@ -8112,12 +8113,12 @@
  12.751    qed
  12.752  qed
  12.753  
  12.754 -proposition homeomorphism_grouping_points_exists:
  12.755 +proposition%important homeomorphism_grouping_points_exists:
  12.756    fixes S :: "'a::euclidean_space set"
  12.757    assumes "open U" "open S" "connected S" "U \<noteq> {}" "finite K" "K \<subseteq> S" "U \<subseteq> S" "S \<subseteq> T"
  12.758    obtains f g where "homeomorphism T T f g" "{x. (~ (f x = x \<and> g x = x))} \<subseteq> S"
  12.759                      "bounded {x. (~ (f x = x \<and> g x = x))}" "\<And>x. x \<in> K \<Longrightarrow> f x \<in> U"
  12.760 -proof (cases "2 \<le> DIM('a)")
  12.761 +proof%unimportant (cases "2 \<le> DIM('a)")
  12.762    case True
  12.763    have TS: "T \<subseteq> affine hull S"
  12.764      using affine_hull_open assms by blast
  12.765 @@ -8401,13 +8402,13 @@
  12.766    qed
  12.767  qed
  12.768  
  12.769 -proposition nullhomotopic_from_sphere_extension:
  12.770 +proposition%important nullhomotopic_from_sphere_extension:
  12.771    fixes f :: "'M::euclidean_space \<Rightarrow> 'a::real_normed_vector"
  12.772    shows  "(\<exists>c. homotopic_with (\<lambda>x. True) (sphere a r) S f (\<lambda>x. c)) \<longleftrightarrow>
  12.773            (\<exists>g. continuous_on (cball a r) g \<and> g ` (cball a r) \<subseteq> S \<and>
  12.774                 (\<forall>x \<in> sphere a r. g x = f x))"
  12.775           (is "?lhs = ?rhs")
  12.776 -proof (cases r "0::real" rule: linorder_cases)
  12.777 +proof%unimportant (cases r "0::real" rule: linorder_cases)
  12.778    case less
  12.779    then show ?thesis by simp
  12.780  next
    13.1 --- a/src/HOL/Analysis/Product_Vector.thy	Thu Apr 05 06:15:02 2018 +0000
    13.2 +++ b/src/HOL/Analysis/Product_Vector.thy	Fri Apr 06 17:34:50 2018 +0200
    13.3 @@ -12,7 +12,7 @@
    13.4  
    13.5  subsection \<open>Product is a real vector space\<close>
    13.6  
    13.7 -instantiation prod :: (real_vector, real_vector) real_vector
    13.8 +instantiation%important prod :: (real_vector, real_vector) real_vector
    13.9  begin
   13.10  
   13.11  definition scaleR_prod_def:
   13.12 @@ -46,10 +46,10 @@
   13.13  
   13.14  (* TODO: Product of uniform spaces and compatibility with metric_spaces! *)
   13.15  
   13.16 -instantiation prod :: (metric_space, metric_space) dist
   13.17 +instantiation%important prod :: (metric_space, metric_space) dist
   13.18  begin
   13.19  
   13.20 -definition dist_prod_def[code del]:
   13.21 +definition%important dist_prod_def[code del]:
   13.22    "dist x y = sqrt ((dist (fst x) (fst y))\<^sup>2 + (dist (snd x) (snd y))\<^sup>2)"
   13.23  
   13.24  instance ..
   13.25 @@ -68,7 +68,7 @@
   13.26  
   13.27  declare uniformity_Abort[where 'a="'a :: metric_space \<times> 'b :: metric_space", code]
   13.28  
   13.29 -instantiation prod :: (metric_space, metric_space) metric_space
   13.30 +instantiation%important prod :: (metric_space, metric_space) metric_space
   13.31  begin
   13.32  
   13.33  lemma dist_Pair_Pair: "dist (a, b) (c, d) = sqrt ((dist a c)\<^sup>2 + (dist b d)\<^sup>2)"
   13.34 @@ -186,8 +186,8 @@
   13.35  
   13.36  subsection \<open>Product is a complete metric space\<close>
   13.37  
   13.38 -instance prod :: (complete_space, complete_space) complete_space
   13.39 -proof
   13.40 +instance%important prod :: (complete_space, complete_space) complete_space
   13.41 +proof%unimportant
   13.42    fix X :: "nat \<Rightarrow> 'a \<times> 'b" assume "Cauchy X"
   13.43    have 1: "(\<lambda>n. fst (X n)) \<longlonglongrightarrow> lim (\<lambda>n. fst (X n))"
   13.44      using Cauchy_fst [OF \<open>Cauchy X\<close>]
   13.45 @@ -203,7 +203,7 @@
   13.46  
   13.47  subsection \<open>Product is a normed vector space\<close>
   13.48  
   13.49 -instantiation prod :: (real_normed_vector, real_normed_vector) real_normed_vector
   13.50 +instantiation%important prod :: (real_normed_vector, real_normed_vector) real_normed_vector
   13.51  begin
   13.52  
   13.53  definition norm_prod_def[code del]:
   13.54 @@ -245,13 +245,13 @@
   13.55  
   13.56  instance prod :: (banach, banach) banach ..
   13.57  
   13.58 -subsubsection \<open>Pair operations are linear\<close>
   13.59 +subsubsection%unimportant \<open>Pair operations are linear\<close>
   13.60  
   13.61 -lemma bounded_linear_fst: "bounded_linear fst"
   13.62 +lemma%important bounded_linear_fst: "bounded_linear fst"
   13.63    using fst_add fst_scaleR
   13.64    by (rule bounded_linear_intro [where K=1], simp add: norm_prod_def)
   13.65  
   13.66 -lemma bounded_linear_snd: "bounded_linear snd"
   13.67 +lemma%important bounded_linear_snd: "bounded_linear snd"
   13.68    using snd_add snd_scaleR
   13.69    by (rule bounded_linear_intro [where K=1], simp add: norm_prod_def)
   13.70  
   13.71 @@ -285,12 +285,12 @@
   13.72    then show "\<exists>K. \<forall>x. norm (f x, g x) \<le> norm x * K" ..
   13.73  qed
   13.74  
   13.75 -subsubsection \<open>Frechet derivatives involving pairs\<close>
   13.76 +subsubsection%unimportant \<open>Frechet derivatives involving pairs\<close>
   13.77  
   13.78 -lemma has_derivative_Pair [derivative_intros]:
   13.79 +lemma%important has_derivative_Pair [derivative_intros]:
   13.80    assumes f: "(f has_derivative f') (at x within s)" and g: "(g has_derivative g') (at x within s)"
   13.81    shows "((\<lambda>x. (f x, g x)) has_derivative (\<lambda>h. (f' h, g' h))) (at x within s)"
   13.82 -proof (rule has_derivativeI_sandwich[of 1])
   13.83 +proof%unimportant (rule has_derivativeI_sandwich[of 1])
   13.84    show "bounded_linear (\<lambda>h. (f' h, g' h))"
   13.85      using f g by (intro bounded_linear_Pair has_derivative_bounded_linear)
   13.86    let ?Rf = "\<lambda>y. f y - f x - f' (y - x)"
   13.87 @@ -319,7 +319,7 @@
   13.88    unfolding split_beta' .
   13.89  
   13.90  
   13.91 -subsubsection \<open>Vector derivatives involving pairs\<close>
   13.92 +subsubsection%unimportant \<open>Vector derivatives involving pairs\<close>
   13.93  
   13.94  lemma has_vector_derivative_Pair[derivative_intros]:
   13.95    assumes "(f has_vector_derivative f') (at x within s)"
   13.96 @@ -331,7 +331,7 @@
   13.97  
   13.98  subsection \<open>Product is an inner product space\<close>
   13.99  
  13.100 -instantiation prod :: (real_inner, real_inner) real_inner
  13.101 +instantiation%important prod :: (real_inner, real_inner) real_inner
  13.102  begin
  13.103  
  13.104  definition inner_prod_def:
    14.1 --- a/src/HOL/Analysis/Sigma_Algebra.thy	Thu Apr 05 06:15:02 2018 +0000
    14.2 +++ b/src/HOL/Analysis/Sigma_Algebra.thy	Fri Apr 06 17:34:50 2018 +0200
    14.3 @@ -5,7 +5,7 @@
    14.4      translated by Lawrence Paulson.
    14.5  *)
    14.6  
    14.7 -section \<open>Describing measurable sets\<close>
    14.8 +section \<open>Sigma Algebra\<close>
    14.9  
   14.10  theory Sigma_Algebra
   14.11  imports
   14.12 @@ -27,7 +27,7 @@
   14.13  
   14.14  subsection \<open>Families of sets\<close>
   14.15  
   14.16 -locale subset_class =
   14.17 +locale%important subset_class =
   14.18    fixes \<Omega> :: "'a set" and M :: "'a set set"
   14.19    assumes space_closed: "M \<subseteq> Pow \<Omega>"
   14.20  
   14.21 @@ -36,7 +36,7 @@
   14.22  
   14.23  subsubsection \<open>Semiring of sets\<close>
   14.24  
   14.25 -locale semiring_of_sets = subset_class +
   14.26 +locale%important semiring_of_sets = subset_class +
   14.27    assumes empty_sets[iff]: "{} \<in> M"
   14.28    assumes Int[intro]: "\<And>a b. a \<in> M \<Longrightarrow> b \<in> M \<Longrightarrow> a \<inter> b \<in> M"
   14.29    assumes Diff_cover:
   14.30 @@ -71,7 +71,9 @@
   14.31    with assms show ?thesis by auto
   14.32  qed
   14.33  
   14.34 -locale ring_of_sets = semiring_of_sets +
   14.35 +subsubsection \<open>Ring of sets\<close>
   14.36 +
   14.37 +locale%important ring_of_sets = semiring_of_sets +
   14.38    assumes Un [intro]: "\<And>a b. a \<in> M \<Longrightarrow> b \<in> M \<Longrightarrow> a \<union> b \<in> M"
   14.39  
   14.40  lemma (in ring_of_sets) finite_Union [intro]:
   14.41 @@ -135,20 +137,22 @@
   14.42    with assms show ?thesis by auto
   14.43  qed
   14.44  
   14.45 -locale algebra = ring_of_sets +
   14.46 +subsubsection \<open>Algebra of sets\<close>
   14.47 +
   14.48 +locale%important algebra = ring_of_sets +
   14.49    assumes top [iff]: "\<Omega> \<in> M"
   14.50  
   14.51  lemma (in algebra) compl_sets [intro]:
   14.52    "a \<in> M \<Longrightarrow> \<Omega> - a \<in> M"
   14.53    by auto
   14.54  
   14.55 -lemma algebra_iff_Un:
   14.56 +lemma%important algebra_iff_Un:
   14.57    "algebra \<Omega> M \<longleftrightarrow>
   14.58      M \<subseteq> Pow \<Omega> \<and>
   14.59      {} \<in> M \<and>
   14.60      (\<forall>a \<in> M. \<Omega> - a \<in> M) \<and>
   14.61      (\<forall>a \<in> M. \<forall> b \<in> M. a \<union> b \<in> M)" (is "_ \<longleftrightarrow> ?Un")
   14.62 -proof
   14.63 +proof%unimportant
   14.64    assume "algebra \<Omega> M"
   14.65    then interpret algebra \<Omega> M .
   14.66    show ?Un using sets_into_space by auto
   14.67 @@ -169,12 +173,12 @@
   14.68    show "algebra \<Omega> M" proof qed fact
   14.69  qed
   14.70  
   14.71 -lemma algebra_iff_Int:
   14.72 +lemma%important algebra_iff_Int:
   14.73       "algebra \<Omega> M \<longleftrightarrow>
   14.74         M \<subseteq> Pow \<Omega> & {} \<in> M &
   14.75         (\<forall>a \<in> M. \<Omega> - a \<in> M) &
   14.76         (\<forall>a \<in> M. \<forall> b \<in> M. a \<inter> b \<in> M)" (is "_ \<longleftrightarrow> ?Int")
   14.77 -proof
   14.78 +proof%unimportant
   14.79    assume "algebra \<Omega> M"
   14.80    then interpret algebra \<Omega> M .
   14.81    show ?Int using sets_into_space by auto
   14.82 @@ -214,7 +218,7 @@
   14.83    "X \<subseteq> S \<Longrightarrow> algebra S { {}, X, S - X, S }"
   14.84    by (auto simp: algebra_iff_Int)
   14.85  
   14.86 -subsubsection \<open>Restricted algebras\<close>
   14.87 +subsubsection%unimportant \<open>Restricted algebras\<close>
   14.88  
   14.89  abbreviation (in algebra)
   14.90    "restricted_space A \<equiv> ((\<inter>) A) ` M"
   14.91 @@ -225,7 +229,7 @@
   14.92  
   14.93  subsubsection \<open>Sigma Algebras\<close>
   14.94  
   14.95 -locale sigma_algebra = algebra +
   14.96 +locale%important sigma_algebra = algebra +
   14.97    assumes countable_nat_UN [intro]: "\<And>A. range A \<subseteq> M \<Longrightarrow> (\<Union>i::nat. A i) \<in> M"
   14.98  
   14.99  lemma (in algebra) is_sigma_algebra:
  14.100 @@ -423,7 +427,7 @@
  14.101    shows "sigma_algebra S { {}, X, S - X, S }"
  14.102    using algebra.is_sigma_algebra[OF algebra_single_set[OF \<open>X \<subseteq> S\<close>]] by simp
  14.103  
  14.104 -subsubsection \<open>Binary Unions\<close>
  14.105 +subsubsection%unimportant \<open>Binary Unions\<close>
  14.106  
  14.107  definition binary :: "'a \<Rightarrow> 'a \<Rightarrow> nat \<Rightarrow> 'a"
  14.108    where "binary a b =  (\<lambda>x. b)(0 := a)"
  14.109 @@ -447,10 +451,10 @@
  14.110  
  14.111  subsubsection \<open>Initial Sigma Algebra\<close>
  14.112  
  14.113 -text \<open>Sigma algebras can naturally be created as the closure of any set of
  14.114 +text%important \<open>Sigma algebras can naturally be created as the closure of any set of
  14.115    M with regard to the properties just postulated.\<close>
  14.116  
  14.117 -inductive_set sigma_sets :: "'a set \<Rightarrow> 'a set set \<Rightarrow> 'a set set"
  14.118 +inductive_set%important sigma_sets :: "'a set \<Rightarrow> 'a set set \<Rightarrow> 'a set set"
  14.119    for sp :: "'a set" and A :: "'a set set"
  14.120    where
  14.121      Basic[intro, simp]: "a \<in> A \<Longrightarrow> a \<in> sigma_sets sp A"
  14.122 @@ -796,7 +800,7 @@
  14.123    thus "(\<Union>i::nat. A i) \<in> M" by (simp add: UN_disjointed_eq)
  14.124  qed
  14.125  
  14.126 -subsubsection \<open>Ring generated by a semiring\<close>
  14.127 +subsubsection%unimportant \<open>Ring generated by a semiring\<close>
  14.128  
  14.129  definition (in semiring_of_sets)
  14.130    "generated_ring = { \<Union>C | C. C \<subseteq> M \<and> finite C \<and> disjoint C }"
  14.131 @@ -927,7 +931,7 @@
  14.132      by (blast intro!: sigma_sets_mono elim: generated_ringE)
  14.133  qed (auto intro!: generated_ringI_Basic sigma_sets_mono)
  14.134  
  14.135 -subsubsection \<open>A Two-Element Series\<close>
  14.136 +subsubsection%unimportant \<open>A Two-Element Series\<close>
  14.137  
  14.138  definition binaryset :: "'a set \<Rightarrow> 'a set \<Rightarrow> nat \<Rightarrow> 'a set"
  14.139    where "binaryset A B = (\<lambda>x. {})(0 := A, Suc 0 := B)"
  14.140 @@ -943,7 +947,7 @@
  14.141  
  14.142  subsubsection \<open>Closed CDI\<close>
  14.143  
  14.144 -definition closed_cdi where
  14.145 +definition%important closed_cdi where
  14.146    "closed_cdi \<Omega> M \<longleftrightarrow>
  14.147     M \<subseteq> Pow \<Omega> &
  14.148     (\<forall>s \<in> M. \<Omega> - s \<in> M) &
  14.149 @@ -1177,7 +1181,7 @@
  14.150  
  14.151  subsubsection \<open>Dynkin systems\<close>
  14.152  
  14.153 -locale dynkin_system = subset_class +
  14.154 +locale%important dynkin_system = subset_class +
  14.155    assumes space: "\<Omega> \<in> M"
  14.156      and   compl[intro!]: "\<And>A. A \<in> M \<Longrightarrow> \<Omega> - A \<in> M"
  14.157      and   UN[intro!]: "\<And>A. disjoint_family A \<Longrightarrow> range A \<subseteq> M
  14.158 @@ -1239,7 +1243,7 @@
  14.159  
  14.160  subsubsection "Intersection sets systems"
  14.161  
  14.162 -definition "Int_stable M \<longleftrightarrow> (\<forall> a \<in> M. \<forall> b \<in> M. a \<inter> b \<in> M)"
  14.163 +definition%important "Int_stable M \<longleftrightarrow> (\<forall> a \<in> M. \<forall> b \<in> M. a \<inter> b \<in> M)"
  14.164  
  14.165  lemma (in algebra) Int_stable: "Int_stable M"
  14.166    unfolding Int_stable_def by auto
  14.167 @@ -1279,7 +1283,7 @@
  14.168  
  14.169  subsubsection "Smallest Dynkin systems"
  14.170  
  14.171 -definition dynkin where
  14.172 +definition%important dynkin where
  14.173    "dynkin \<Omega> M =  (\<Inter>{D. dynkin_system \<Omega> D \<and> M \<subseteq> D})"
  14.174  
  14.175  lemma dynkin_system_dynkin:
  14.176 @@ -1426,10 +1430,10 @@
  14.177  
  14.178  subsubsection \<open>Induction rule for intersection-stable generators\<close>
  14.179  
  14.180 -text \<open>The reason to introduce Dynkin-systems is the following induction rules for $\sigma$-algebras
  14.181 +text%important \<open>The reason to introduce Dynkin-systems is the following induction rules for $\sigma$-algebras
  14.182  generated by a generator closed under intersection.\<close>
  14.183  
  14.184 -lemma sigma_sets_induct_disjoint[consumes 3, case_names basic empty compl union]:
  14.185 +lemma%important sigma_sets_induct_disjoint[consumes 3, case_names basic empty compl union]:
  14.186    assumes "Int_stable G"
  14.187      and closed: "G \<subseteq> Pow \<Omega>"
  14.188      and A: "A \<in> sigma_sets \<Omega> G"
  14.189 @@ -1438,7 +1442,7 @@
  14.190      and compl: "\<And>A. A \<in> sigma_sets \<Omega> G \<Longrightarrow> P A \<Longrightarrow> P (\<Omega> - A)"
  14.191      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)"
  14.192    shows "P A"
  14.193 -proof -
  14.194 +proof%unimportant -
  14.195    let ?D = "{ A \<in> sigma_sets \<Omega> G. P A }"
  14.196    interpret sigma_algebra \<Omega> "sigma_sets \<Omega> G"
  14.197      using closed by (rule sigma_algebra_sigma_sets)
  14.198 @@ -1452,34 +1456,34 @@
  14.199  
  14.200  subsection \<open>Measure type\<close>
  14.201  
  14.202 -definition positive :: "'a set set \<Rightarrow> ('a set \<Rightarrow> ennreal) \<Rightarrow> bool" where
  14.203 +definition%important positive :: "'a set set \<Rightarrow> ('a set \<Rightarrow> ennreal) \<Rightarrow> bool" where
  14.204    "positive M \<mu> \<longleftrightarrow> \<mu> {} = 0"
  14.205  
  14.206 -definition countably_additive :: "'a set set \<Rightarrow> ('a set \<Rightarrow> ennreal) \<Rightarrow> bool" where
  14.207 +definition%important countably_additive :: "'a set set \<Rightarrow> ('a set \<Rightarrow> ennreal) \<Rightarrow> bool" where
  14.208    "countably_additive M f \<longleftrightarrow> (\<forall>A. range A \<subseteq> M \<longrightarrow> disjoint_family A \<longrightarrow> (\<Union>i. A i) \<in> M \<longrightarrow>
  14.209      (\<Sum>i. f (A i)) = f (\<Union>i. A i))"
  14.210  
  14.211 -definition measure_space :: "'a set \<Rightarrow> 'a set set \<Rightarrow> ('a set \<Rightarrow> ennreal) \<Rightarrow> bool" where
  14.212 +definition%important measure_space :: "'a set \<Rightarrow> 'a set set \<Rightarrow> ('a set \<Rightarrow> ennreal) \<Rightarrow> bool" where
  14.213    "measure_space \<Omega> A \<mu> \<longleftrightarrow> sigma_algebra \<Omega> A \<and> positive A \<mu> \<and> countably_additive A \<mu>"
  14.214  
  14.215 -typedef 'a measure = "{(\<Omega>::'a set, A, \<mu>). (\<forall>a\<in>-A. \<mu> a = 0) \<and> measure_space \<Omega> A \<mu> }"
  14.216 -proof
  14.217 +typedef%important 'a measure = "{(\<Omega>::'a set, A, \<mu>). (\<forall>a\<in>-A. \<mu> a = 0) \<and> measure_space \<Omega> A \<mu> }"
  14.218 +proof%unimportant
  14.219    have "sigma_algebra UNIV {{}, UNIV}"
  14.220      by (auto simp: sigma_algebra_iff2)
  14.221    then show "(UNIV, {{}, UNIV}, \<lambda>A. 0) \<in> {(\<Omega>, A, \<mu>). (\<forall>a\<in>-A. \<mu> a = 0) \<and> measure_space \<Omega> A \<mu>} "
  14.222      by (auto simp: measure_space_def positive_def countably_additive_def)
  14.223  qed
  14.224  
  14.225 -definition space :: "'a measure \<Rightarrow> 'a set" where
  14.226 +definition%important space :: "'a measure \<Rightarrow> 'a set" where
  14.227    "space M = fst (Rep_measure M)"
  14.228  
  14.229 -definition sets :: "'a measure \<Rightarrow> 'a set set" where
  14.230 +definition%important sets :: "'a measure \<Rightarrow> 'a set set" where
  14.231    "sets M = fst (snd (Rep_measure M))"
  14.232  
  14.233 -definition emeasure :: "'a measure \<Rightarrow> 'a set \<Rightarrow> ennreal" where
  14.234 +definition%important emeasure :: "'a measure \<Rightarrow> 'a set \<Rightarrow> ennreal" where
  14.235    "emeasure M = snd (snd (Rep_measure M))"
  14.236  
  14.237 -definition measure :: "'a measure \<Rightarrow> 'a set \<Rightarrow> real" where
  14.238 +definition%important measure :: "'a measure \<Rightarrow> 'a set \<Rightarrow> real" where
  14.239    "measure M A = enn2real (emeasure M A)"
  14.240  
  14.241  declare [[coercion sets]]
  14.242 @@ -1494,7 +1498,7 @@
  14.243  interpretation sets: sigma_algebra "space M" "sets M" for M :: "'a measure"
  14.244    using measure_space[of M] by (auto simp: measure_space_def)
  14.245  
  14.246 -definition measure_of :: "'a set \<Rightarrow> 'a set set \<Rightarrow> ('a set \<Rightarrow> ennreal) \<Rightarrow> 'a measure" where
  14.247 +definition%important measure_of :: "'a set \<Rightarrow> 'a set set \<Rightarrow> ('a set \<Rightarrow> ennreal) \<Rightarrow> 'a measure" where
  14.248    "measure_of \<Omega> A \<mu> = Abs_measure (\<Omega>, if A \<subseteq> Pow \<Omega> then sigma_sets \<Omega> A else {{}, \<Omega>},
  14.249      \<lambda>a. if a \<in> sigma_sets \<Omega> A \<and> measure_space \<Omega> (sigma_sets \<Omega> A) \<mu> then \<mu> a else 0)"
  14.250  
  14.251 @@ -1629,12 +1633,12 @@
  14.252  
  14.253  subsubsection \<open>Constructing simple @{typ "'a measure"}\<close>
  14.254  
  14.255 -lemma emeasure_measure_of:
  14.256 +lemma%important emeasure_measure_of:
  14.257    assumes M: "M = measure_of \<Omega> A \<mu>"
  14.258    assumes ms: "A \<subseteq> Pow \<Omega>" "positive (sets M) \<mu>" "countably_additive (sets M) \<mu>"
  14.259    assumes X: "X \<in> sets M"
  14.260    shows "emeasure M X = \<mu> X"
  14.261 -proof -
  14.262 +proof%unimportant -
  14.263    interpret sigma_algebra \<Omega> "sigma_sets \<Omega> A" by (rule sigma_algebra_sigma_sets) fact
  14.264    have "measure_space \<Omega> (sigma_sets \<Omega> A) \<mu>"
  14.265      using ms M by (simp add: measure_space_def sigma_algebra_sigma_sets)
  14.266 @@ -1711,7 +1715,7 @@
  14.267  
  14.268  subsubsection \<open>Measurable functions\<close>
  14.269  
  14.270 -definition measurable :: "'a measure \<Rightarrow> 'b measure \<Rightarrow> ('a \<Rightarrow> 'b) set" (infixr "\<rightarrow>\<^sub>M" 60) where
  14.271 +definition%important measurable :: "'a measure \<Rightarrow> 'b measure \<Rightarrow> ('a \<Rightarrow> 'b) set" (infixr "\<rightarrow>\<^sub>M" 60) where
  14.272    "measurable A B = {f \<in> space A \<rightarrow> space B. \<forall>y \<in> sets B. f -` y \<inter> space A \<in> sets A}"
  14.273  
  14.274  lemma measurableI:
  14.275 @@ -1873,7 +1877,7 @@
  14.276  
  14.277  subsubsection \<open>Counting space\<close>
  14.278  
  14.279 -definition count_space :: "'a set \<Rightarrow> 'a measure" where
  14.280 +definition%important count_space :: "'a set \<Rightarrow> 'a measure" where
  14.281    "count_space \<Omega> = measure_of \<Omega> (Pow \<Omega>) (\<lambda>A. if finite A then of_nat (card A) else \<infinity>)"
  14.282  
  14.283  lemma
  14.284 @@ -1949,7 +1953,7 @@
  14.285    "space N = {} \<Longrightarrow> f \<in> measurable M N \<longleftrightarrow> space M = {}"
  14.286    by (auto simp add: measurable_def Pi_iff)
  14.287  
  14.288 -subsubsection \<open>Extend measure\<close>
  14.289 +subsubsection%unimportant \<open>Extend measure\<close>
  14.290  
  14.291  definition "extend_measure \<Omega> I G \<mu> =
  14.292    (if (\<exists>\<mu>'. (\<forall>i\<in>I. \<mu>' (G i) = \<mu> i) \<and> measure_space \<Omega> (sigma_sets \<Omega> (G`I)) \<mu>') \<and> \<not> (\<forall>i\<in>I. \<mu> i = 0)
  14.293 @@ -2011,7 +2015,7 @@
  14.294  
  14.295  subsection \<open>The smallest $\sigma$-algebra regarding a function\<close>
  14.296  
  14.297 -definition
  14.298 +definition%important
  14.299    "vimage_algebra X f M = sigma X {f -` A \<inter> X | A. A \<in> sets M}"
  14.300  
  14.301  lemma space_vimage_algebra[simp]: "space (vimage_algebra X f M) = X"
    15.1 --- a/src/HOL/Analysis/Starlike.thy	Thu Apr 05 06:15:02 2018 +0000
    15.2 +++ b/src/HOL/Analysis/Starlike.thy	Fri Apr 06 17:34:50 2018 +0200
    15.3 @@ -15,7 +15,7 @@
    15.4  
    15.5  subsection \<open>Midpoint\<close>
    15.6  
    15.7 -definition midpoint :: "'a::real_vector \<Rightarrow> 'a \<Rightarrow> 'a"
    15.8 +definition%important midpoint :: "'a::real_vector \<Rightarrow> 'a \<Rightarrow> 'a"
    15.9    where "midpoint a b = (inverse (2::real)) *\<^sub>R (a + b)"
   15.10  
   15.11  lemma midpoint_idem [simp]: "midpoint x x = x"
   15.12 @@ -94,10 +94,10 @@
   15.13  
   15.14  subsection \<open>Line segments\<close>
   15.15  
   15.16 -definition closed_segment :: "'a::real_vector \<Rightarrow> 'a \<Rightarrow> 'a set"
   15.17 +definition%important closed_segment :: "'a::real_vector \<Rightarrow> 'a \<Rightarrow> 'a set"
   15.18    where "closed_segment a b = {(1 - u) *\<^sub>R a + u *\<^sub>R b | u::real. 0 \<le> u \<and> u \<le> 1}"
   15.19  
   15.20 -definition open_segment :: "'a::real_vector \<Rightarrow> 'a \<Rightarrow> 'a set" where
   15.21 +definition%important open_segment :: "'a::real_vector \<Rightarrow> 'a \<Rightarrow> 'a set" where
   15.22    "open_segment a b \<equiv> closed_segment a b - {a,b}"
   15.23  
   15.24  lemmas segment = open_segment_def closed_segment_def
   15.25 @@ -599,7 +599,7 @@
   15.26  
   15.27  subsection\<open>Starlike sets\<close>
   15.28  
   15.29 -definition "starlike S \<longleftrightarrow> (\<exists>a\<in>S. \<forall>x\<in>S. closed_segment a x \<subseteq> S)"
   15.30 +definition%important "starlike S \<longleftrightarrow> (\<exists>a\<in>S. \<forall>x\<in>S. closed_segment a x \<subseteq> S)"
   15.31  
   15.32  lemma starlike_UNIV [simp]: "starlike UNIV"
   15.33    by (simp add: starlike_def)
   15.34 @@ -662,7 +662,7 @@
   15.35      by (meson hull_mono inf_mono subset_insertI subset_refl)
   15.36  qed
   15.37  
   15.38 -subsection\<open>More results about segments\<close>
   15.39 +subsection%unimportant\<open>More results about segments\<close>
   15.40  
   15.41  lemma dist_half_times2:
   15.42    fixes a :: "'a :: real_normed_vector"
   15.43 @@ -884,7 +884,7 @@
   15.44  
   15.45  subsection\<open>Betweenness\<close>
   15.46  
   15.47 -definition "between = (\<lambda>(a,b) x. x \<in> closed_segment a b)"
   15.48 +definition%important "between = (\<lambda>(a,b) x. x \<in> closed_segment a b)"
   15.49  
   15.50  lemma betweenI:
   15.51    assumes "0 \<le> u" "u \<le> 1" "x = (1 - u) *\<^sub>R a + u *\<^sub>R b"
   15.52 @@ -1055,7 +1055,7 @@
   15.53    by (auto simp: between_mem_segment closed_segment_eq_real_ivl)
   15.54  
   15.55  
   15.56 -subsection \<open>Shrinking towards the interior of a convex set\<close>
   15.57 +subsection%unimportant \<open>Shrinking towards the interior of a convex set\<close>
   15.58  
   15.59  lemma mem_interior_convex_shrink:
   15.60    fixes s :: "'a::euclidean_space set"
   15.61 @@ -1249,7 +1249,7 @@
   15.62  qed
   15.63  
   15.64  
   15.65 -subsection \<open>Some obvious but surprisingly hard simplex lemmas\<close>
   15.66 +subsection%unimportant \<open>Some obvious but surprisingly hard simplex lemmas\<close>
   15.67  
   15.68  lemma simplex:
   15.69    assumes "finite s"
   15.70 @@ -1693,7 +1693,7 @@
   15.71  qed
   15.72  
   15.73  
   15.74 -subsection \<open>Relative interior of convex set\<close>
   15.75 +subsection%unimportant \<open>Relative interior of convex set\<close>
   15.76  
   15.77  lemma rel_interior_convex_nonempty_aux:
   15.78    fixes S :: "'n::euclidean_space set"
   15.79 @@ -2081,7 +2081,7 @@
   15.80  
   15.81  subsection\<open>The relative frontier of a set\<close>
   15.82  
   15.83 -definition "rel_frontier S = closure S - rel_interior S"
   15.84 +definition%important "rel_frontier S = closure S - rel_interior S"
   15.85  
   15.86  lemma rel_frontier_empty [simp]: "rel_frontier {} = {}"
   15.87    by (simp add: rel_frontier_def)
   15.88 @@ -2460,7 +2460,7 @@
   15.89  qed
   15.90  
   15.91  
   15.92 -subsubsection \<open>Relative interior and closure under common operations\<close>
   15.93 +subsubsection%unimportant \<open>Relative interior and closure under common operations\<close>
   15.94  
   15.95  lemma rel_interior_inter_aux: "\<Inter>{rel_interior S |S. S \<in> I} \<subseteq> \<Inter>I"
   15.96  proof -
   15.97 @@ -3150,7 +3150,7 @@
   15.98      by (force simp: rel_frontier_def rel_interior_Times assms closure_Times)
   15.99  
  15.100  
  15.101 -subsubsection \<open>Relative interior of convex cone\<close>
  15.102 +subsubsection%unimportant \<open>Relative interior of convex cone\<close>
  15.103  
  15.104  lemma cone_rel_interior:
  15.105    fixes S :: "'m::euclidean_space set"
  15.106 @@ -3423,7 +3423,7 @@
  15.107  qed
  15.108  
  15.109  
  15.110 -subsection \<open>Convexity on direct sums\<close>
  15.111 +subsection%unimportant \<open>Convexity on direct sums\<close>
  15.112  
  15.113  lemma closure_sum:
  15.114    fixes S T :: "'a::real_normed_vector set"
  15.115 @@ -3794,7 +3794,7 @@
  15.116      using \<open>y < x\<close> by (simp add: field_simps)
  15.117  qed simp
  15.118  
  15.119 -subsection\<open>Explicit formulas for interior and relative interior of convex hull\<close>
  15.120 +subsection%unimportant\<open>Explicit formulas for interior and relative interior of convex hull\<close>
  15.121  
  15.122  lemma at_within_cbox_finite:
  15.123    assumes "x \<in> box a b" "x \<notin> S" "finite S"
  15.124 @@ -4157,7 +4157,7 @@
  15.125      by (metis Diff_cancel convex_hull_singleton insert_absorb2 open_segment_def segment_convex_hull)
  15.126  qed
  15.127  
  15.128 -subsection\<open>Similar results for closure and (relative or absolute) frontier.\<close>
  15.129 +subsection%unimportant\<open>Similar results for closure and (relative or absolute) frontier.\<close>
  15.130  
  15.131  lemma closure_convex_hull [simp]:
  15.132    fixes s :: "'a::euclidean_space set"
  15.133 @@ -4315,7 +4315,7 @@
  15.134  
  15.135  subsection \<open>Coplanarity, and collinearity in terms of affine hull\<close>
  15.136  
  15.137 -definition coplanar  where
  15.138 +definition%important coplanar  where
  15.139     "coplanar s \<equiv> \<exists>u v w. s \<subseteq> affine hull {u,v,w}"
  15.140  
  15.141  lemma collinear_affine_hull:
  15.142 @@ -4767,7 +4767,7 @@
  15.143  
  15.144  subsection\<open>The infimum of the distance between two sets\<close>
  15.145  
  15.146 -definition setdist :: "'a::metric_space set \<Rightarrow> 'a set \<Rightarrow> real" where
  15.147 +definition%important setdist :: "'a::metric_space set \<Rightarrow> 'a set \<Rightarrow> real" where
  15.148    "setdist s t \<equiv>
  15.149         (if s = {} \<or> t = {} then 0
  15.150          else Inf {dist x y| x y. x \<in> s \<and> y \<in> t})"
  15.151 @@ -5003,7 +5003,7 @@
  15.152           \<Longrightarrow> setdist {x} S > 0"
  15.153    using less_eq_real_def setdist_eq_0_closedin by fastforce
  15.154  
  15.155 -subsection\<open>Basic lemmas about hyperplanes and halfspaces\<close>
  15.156 +subsection%unimportant\<open>Basic lemmas about hyperplanes and halfspaces\<close>
  15.157  
  15.158  lemma hyperplane_eq_Ex:
  15.159    assumes "a \<noteq> 0" obtains x where "a \<bullet> x = b"
  15.160 @@ -5056,7 +5056,7 @@
  15.161  using halfspace_eq_empty_le [of "-a" "-b"]
  15.162  by simp
  15.163  
  15.164 -subsection\<open>Use set distance for an easy proof of separation properties\<close>
  15.165 +subsection%unimportant\<open>Use set distance for an easy proof of separation properties\<close>
  15.166  
  15.167  proposition separation_closures:
  15.168    fixes S :: "'a::euclidean_space set"
  15.169 @@ -5150,12 +5150,12 @@
  15.170  
  15.171  subsection\<open>Connectedness of the intersection of a chain\<close>
  15.172  
  15.173 -proposition connected_chain:
  15.174 +proposition%important connected_chain:
  15.175    fixes \<F> :: "'a :: euclidean_space set set"
  15.176    assumes cc: "\<And>S. S \<in> \<F> \<Longrightarrow> compact S \<and> connected S"
  15.177        and linear: "\<And>S T. S \<in> \<F> \<and> T \<in> \<F> \<Longrightarrow> S \<subseteq> T \<or> T \<subseteq> S"
  15.178    shows "connected(\<Inter>\<F>)"
  15.179 -proof (cases "\<F> = {}")
  15.180 +proof%unimportant (cases "\<F> = {}")
  15.181    case True then show ?thesis
  15.182      by auto
  15.183  next
  15.184 @@ -5299,13 +5299,13 @@
  15.185        by (meson le_max_iff_disj)
  15.186  qed
  15.187  
  15.188 -proposition proper_map:
  15.189 +proposition%important proper_map:
  15.190    fixes f :: "'a::heine_borel \<Rightarrow> 'b::heine_borel"
  15.191    assumes "closedin (subtopology euclidean S) K"
  15.192        and com: "\<And>U. \<lbrakk>U \<subseteq> T; compact U\<rbrakk> \<Longrightarrow> compact (S \<inter> f -` U)"
  15.193        and "f ` S \<subseteq> T"
  15.194      shows "closedin (subtopology euclidean T) (f ` K)"
  15.195 -proof -
  15.196 +proof%unimportant -
  15.197    have "K \<subseteq> S"
  15.198      using assms closedin_imp_subset by metis
  15.199    obtain C where "closed C" and Keq: "K = S \<inter> C"
  15.200 @@ -5387,7 +5387,7 @@
  15.201      by (simp add: continuous_on_closed * closedin_imp_subset)
  15.202  qed
  15.203  
  15.204 -subsection\<open>Trivial fact: convexity equals connectedness for collinear sets\<close>
  15.205 +subsection%unimportant\<open>Trivial fact: convexity equals connectedness for collinear sets\<close>
  15.206  
  15.207  lemma convex_connected_collinear:
  15.208    fixes S :: "'a::euclidean_space set"
  15.209 @@ -5605,7 +5605,7 @@
  15.210      by (simp add: clo closedin_closed_Int)
  15.211  qed
  15.212  
  15.213 -subsubsection\<open>Representing affine hull as a finite intersection of hyperplanes\<close>
  15.214 +subsubsection%unimportant\<open>Representing affine hull as a finite intersection of hyperplanes\<close>
  15.215  
  15.216  proposition affine_hull_convex_Int_nonempty_interior:
  15.217    fixes S :: "'a::real_normed_vector set"
  15.218 @@ -5778,7 +5778,7 @@
  15.219          (if a = 0 \<and> r > 0 then -1 else DIM('a))"
  15.220  using aff_dim_halfspace_le [of "-a" "-r"] by simp
  15.221  
  15.222 -subsection\<open>Properties of special hyperplanes\<close>
  15.223 +subsection%unimportant\<open>Properties of special hyperplanes\<close>
  15.224  
  15.225  lemma subspace_hyperplane: "subspace {x. a \<bullet> x = 0}"
  15.226    by (simp add: subspace_def inner_right_distrib)
  15.227 @@ -5925,7 +5925,7 @@
  15.228    shows "a \<noteq> 0 \<Longrightarrow> aff_dim {x. a \<bullet> x = r} = DIM('a) - 1"
  15.229  by (metis aff_dim_eq_hyperplane affine_hull_eq affine_hyperplane)
  15.230  
  15.231 -subsection\<open>Some stepping theorems\<close>
  15.232 +subsection%unimportant\<open>Some stepping theorems\<close>
  15.233  
  15.234  lemma dim_empty [simp]: "dim ({} :: 'a::euclidean_space set) = 0"
  15.235    by (force intro!: dim_unique)
  15.236 @@ -6092,7 +6092,7 @@
  15.237      by (metis One_nat_def \<open>a \<noteq> 0\<close> affine_bounded_eq_lowdim affine_hyperplane bounded_hyperplane_eq_trivial_0)
  15.238  qed
  15.239  
  15.240 -subsection\<open>General case without assuming closure and getting non-strict separation\<close>
  15.241 +subsection%unimportant\<open>General case without assuming closure and getting non-strict separation\<close>
  15.242  
  15.243  proposition separating_hyperplane_closed_point_inset:
  15.244    fixes S :: "'a::euclidean_space set"
  15.245 @@ -6280,7 +6280,7 @@
  15.246  by (metis assms convex_closure convex_rel_interior_closure)
  15.247  
  15.248  
  15.249 -subsection\<open> Some results on decomposing convex hulls: intersections, simplicial subdivision\<close>
  15.250 +subsection%unimportant\<open> Some results on decomposing convex hulls: intersections, simplicial subdivision\<close>
  15.251  
  15.252  lemma
  15.253    fixes s :: "'a::euclidean_space set"
  15.254 @@ -6636,7 +6636,7 @@
  15.255    qed
  15.256  qed
  15.257  
  15.258 -subsection\<open>Misc results about span\<close>
  15.259 +subsection%unimportant\<open>Misc results about span\<close>
  15.260  
  15.261  lemma eq_span_insert_eq:
  15.262    assumes "(x - y) \<in> span S"
  15.263 @@ -7026,11 +7026,11 @@
  15.264  apply (simp add: x)
  15.265  done
  15.266  
  15.267 -proposition Gram_Schmidt_step:
  15.268 +proposition%important Gram_Schmidt_step:
  15.269    fixes S :: "'a::euclidean_space set"
  15.270    assumes S: "pairwise orthogonal S" and x: "x \<in> span S"
  15.271      shows "orthogonal x (a - (\<Sum>b\<in>S. (b \<bullet> a / (b \<bullet> b)) *\<^sub>R b))"
  15.272 -proof -
  15.273 +proof%unimportant -
  15.274    have "finite S"
  15.275      by (simp add: S pairwise_orthogonal_imp_finite)
  15.276    have "orthogonal (a - (\<Sum>b\<in>S. (b \<bullet> a / (b \<bullet> b)) *\<^sub>R b)) x"
  15.277 @@ -7087,11 +7087,11 @@
  15.278  qed
  15.279  
  15.280  
  15.281 -proposition orthogonal_extension:
  15.282 +proposition%important orthogonal_extension:
  15.283    fixes S :: "'a::euclidean_space set"
  15.284    assumes S: "pairwise orthogonal S"
  15.285    obtains U where "pairwise orthogonal (S \<union> U)" "span (S \<union> U) = span (S \<union> T)"
  15.286 -proof -
  15.287 +proof%unimportant -
  15.288    obtain B where "finite B" "span B = span T"
  15.289      using basis_subspace_exists [of "span T"] subspace_span by auto
  15.290    with orthogonal_extension_aux [of B S]
  15.291 @@ -7149,13 +7149,13 @@
  15.292      done
  15.293  qed
  15.294  
  15.295 -proposition orthonormal_basis_subspace:
  15.296 +proposition%important orthonormal_basis_subspace:
  15.297    fixes S :: "'a :: euclidean_space set"
  15.298    assumes "subspace S"
  15.299    obtains B where "B \<subseteq> S" "pairwise orthogonal B"
  15.300                and "\<And>x. x \<in> B \<Longrightarrow> norm x = 1"
  15.301                and "independent B" "card B = dim S" "span B = S"
  15.302 -proof -
  15.303 +proof%unimportant -
  15.304    obtain B where "0 \<notin> B" "B \<subseteq> S"
  15.305               and orth: "pairwise orthogonal B"
  15.306               and "independent B" "card B = dim S" "span B = S"
  15.307 @@ -7186,11 +7186,11 @@
  15.308  qed
  15.309  
  15.310  
  15.311 -proposition orthogonal_to_subspace_exists_gen:
  15.312 +proposition%important orthogonal_to_subspace_exists_gen:
  15.313    fixes S :: "'a :: euclidean_space set"
  15.314    assumes "span S \<subset> span T"
  15.315    obtains x where "x \<noteq> 0" "x \<in> span T" "\<And>y. y \<in> span S \<Longrightarrow> orthogonal x y"
  15.316 -proof -
  15.317 +proof%unimportant -
  15.318    obtain B where "B \<subseteq> span S" and orthB: "pairwise orthogonal B"
  15.319               and "\<And>x. x \<in> B \<Longrightarrow> norm x = 1"
  15.320               and "independent B" "card B = dim S" "span B = span S"
  15.321 @@ -7249,10 +7249,10 @@
  15.322      by (rule orthogonal_to_subspace_exists) (simp add: orthogonal_commute span_clauses(1) that)
  15.323  qed
  15.324  
  15.325 -proposition orthogonal_subspace_decomp_exists:
  15.326 +proposition%important orthogonal_subspace_decomp_exists:
  15.327    fixes S :: "'a :: euclidean_space set"
  15.328    obtains y z where "y \<in> span S" "\<And>w. w \<in> span S \<Longrightarrow> orthogonal z w" "x = y + z"
  15.329 -proof -
  15.330 +proof%unimportant -
  15.331    obtain T where "0 \<notin> T" "T \<subseteq> span S" "pairwise orthogonal T" "independent T" "card T = dim (span S)" "span T = span S"
  15.332      using orthogonal_basis_subspace subspace_span by blast
  15.333    let ?a = "\<Sum>b\<in>T. (b \<bullet> x / (b \<bullet> b)) *\<^sub>R b"
  15.334 @@ -7341,11 +7341,11 @@
  15.335    qed
  15.336  qed
  15.337  
  15.338 -proposition dim_orthogonal_sum:
  15.339 +proposition%important dim_orthogonal_sum:
  15.340    fixes A :: "'a::euclidean_space set"
  15.341    assumes "\<And>x y. \<lbrakk>x \<in> A; y \<in> B\<rbrakk> \<Longrightarrow> x \<bullet> y = 0"
  15.342      shows "dim(A \<union> B) = dim A + dim B"
  15.343 -proof -
  15.344 +proof%unimportant -
  15.345    have 1: "\<And>x y. \<lbrakk>x \<in> span A; y \<in> B\<rbrakk> \<Longrightarrow> x \<bullet> y = 0"
  15.346      by (erule span_induct [OF _ subspace_hyperplane2]; simp add: assms)
  15.347    have "\<And>x y. \<lbrakk>x \<in> span A; y \<in> span B\<rbrakk> \<Longrightarrow> x \<bullet> y = 0"
  15.348 @@ -7472,10 +7472,10 @@
  15.349  
  15.350  subsection\<open>Lower-dimensional affine subsets are nowhere dense.\<close>
  15.351  
  15.352 -proposition dense_complement_subspace:
  15.353 +proposition%important dense_complement_subspace:
  15.354    fixes S :: "'a :: euclidean_space set"
  15.355    assumes dim_less: "dim T < dim S" and "subspace S" shows "closure(S - T) = S"
  15.356 -proof -
  15.357 +proof%unimportant -
  15.358    have "closure(S - U) = S" if "dim U < dim S" "U \<subseteq> S" for U
  15.359    proof -
  15.360      have "span U \<subset> span S"
  15.361 @@ -7583,7 +7583,7 @@
  15.362    by (simp add: assms dense_complement_convex)
  15.363  
  15.364  
  15.365 -subsection\<open>Parallel slices, etc.\<close>
  15.366 +subsection%unimportant\<open>Parallel slices, etc.\<close>
  15.367  
  15.368  text\<open> If we take a slice out of a set, we can do it perpendicularly,
  15.369    with the normal vector to the slice parallel to the affine hull.\<close>
  15.370 @@ -7811,7 +7811,7 @@
  15.371  
  15.372  subsection\<open>Several Variants of Paracompactness\<close>
  15.373  
  15.374 -proposition paracompact:
  15.375 +proposition%important paracompact:
  15.376    fixes S :: "'a :: euclidean_space set"
  15.377    assumes "S \<subseteq> \<Union>\<C>" and opC: "\<And>T. T \<in> \<C> \<Longrightarrow> open T"
  15.378    obtains \<C>' where "S \<subseteq> \<Union> \<C>'"
  15.379 @@ -7819,7 +7819,7 @@
  15.380                 and "\<And>x. x \<in> S
  15.381                         \<Longrightarrow> \<exists>V. open V \<and> x \<in> V \<and>
  15.382                                 finite {U. U \<in> \<C>' \<and> (U \<inter> V \<noteq> {})}"
  15.383 -proof (cases "S = {}")
  15.384 +proof%unimportant (cases "S = {}")
  15.385    case True with that show ?thesis by blast
  15.386  next
  15.387    case False
  15.388 @@ -7955,7 +7955,7 @@
  15.389  using paracompact_closedin [of UNIV S \<C>] assms by auto
  15.390  
  15.391    
  15.392 -subsection\<open>Closed-graph characterization of continuity\<close>
  15.393 +subsection%unimportant\<open>Closed-graph characterization of continuity\<close>
  15.394  
  15.395  lemma continuous_closed_graph_gen:
  15.396    fixes T :: "'b::real_normed_vector set"
  15.397 @@ -8026,7 +8026,7 @@
  15.398      by (rule continuous_on_Un_local_open [OF opS opT])
  15.399  qed
  15.400    
  15.401 -subsection\<open>The union of two collinear segments is another segment\<close>
  15.402 +subsection%unimportant\<open>The union of two collinear segments is another segment\<close>
  15.403  
  15.404  proposition in_convex_hull_exchange:
  15.405    fixes a :: "'a::euclidean_space"
  15.406 @@ -8204,14 +8204,14 @@
  15.407  
  15.408  subsection\<open>Covering an open set by a countable chain of compact sets\<close>
  15.409    
  15.410 -proposition open_Union_compact_subsets:
  15.411 +proposition%important open_Union_compact_subsets:
  15.412    fixes S :: "'a::euclidean_space set"
  15.413    assumes "open S"
  15.414    obtains C where "\<And>n. compact(C n)" "\<And>n. C n \<subseteq> S"
  15.415                    "\<And>n. C n \<subseteq> interior(C(Suc n))"
  15.416                    "\<Union>(range C) = S"
  15.417                    "\<And>K. \<lbrakk>compact K; K \<subseteq> S\<rbrakk> \<Longrightarrow> \<exists>N. \<forall>n\<ge>N. K \<subseteq> (C n)"
  15.418 -proof (cases "S = {}")
  15.419 +proof%unimportant (cases "S = {}")
  15.420    case True
  15.421    then show ?thesis
  15.422      by (rule_tac C = "\<lambda>n. {}" in that) auto
    16.1 --- a/src/HOL/Analysis/Topology_Euclidean_Space.thy	Thu Apr 05 06:15:02 2018 +0000
    16.2 +++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy	Fri Apr 06 17:34:50 2018 +0200
    16.3 @@ -131,7 +131,7 @@
    16.4  context topological_space
    16.5  begin
    16.6  
    16.7 -definition "topological_basis B \<longleftrightarrow>
    16.8 +definition%important "topological_basis B \<longleftrightarrow>
    16.9    (\<forall>b\<in>B. open b) \<and> (\<forall>x. open x \<longrightarrow> (\<exists>B'. B' \<subseteq> B \<and> \<Union>B' = x))"
   16.10  
   16.11  lemma topological_basis:
   16.12 @@ -257,7 +257,7 @@
   16.13  
   16.14  subsection \<open>Countable Basis\<close>
   16.15  
   16.16 -locale countable_basis =
   16.17 +locale%important countable_basis =
   16.18    fixes B :: "'a::topological_space set set"
   16.19    assumes is_basis: "topological_basis B"
   16.20      and countable_basis: "countable B"
   16.21 @@ -578,19 +578,19 @@
   16.22    then show ?thesis using B(1) by auto
   16.23  qed
   16.24  
   16.25 -subsection \<open>Polish spaces\<close>
   16.26 +subsection%important \<open>Polish spaces\<close>
   16.27  
   16.28  text \<open>Textbooks define Polish spaces as completely metrizable.
   16.29    We assume the topology to be complete for a given metric.\<close>
   16.30  
   16.31 -class polish_space = complete_space + second_countable_topology
   16.32 +class%important polish_space = complete_space + second_countable_topology
   16.33  
   16.34  subsection \<open>General notion of a topology as a value\<close>
   16.35  
   16.36 -definition "istopology L \<longleftrightarrow>
   16.37 +definition%important "istopology L \<longleftrightarrow>
   16.38    L {} \<and> (\<forall>S T. L S \<longrightarrow> L T \<longrightarrow> L (S \<inter> T)) \<and> (\<forall>K. Ball K L \<longrightarrow> L (\<Union>K))"
   16.39  
   16.40 -typedef 'a topology = "{L::('a set) \<Rightarrow> bool. istopology L}"
   16.41 +typedef%important 'a topology = "{L::('a set) \<Rightarrow> bool. istopology L}"
   16.42    morphisms "openin" "topology"
   16.43    unfolding istopology_def by blast
   16.44  
   16.45 @@ -620,7 +620,7 @@
   16.46  
   16.47  subsubsection \<open>Main properties of open sets\<close>
   16.48  
   16.49 -lemma openin_clauses:
   16.50 +lemma%important openin_clauses:
   16.51    fixes U :: "'a topology"
   16.52    shows
   16.53      "openin U {}"
   16.54 @@ -683,7 +683,7 @@
   16.55  
   16.56  subsubsection \<open>Closed sets\<close>
   16.57  
   16.58 -definition "closedin U S \<longleftrightarrow> S \<subseteq> topspace U \<and> openin U (topspace U - S)"
   16.59 +definition%important "closedin U S \<longleftrightarrow> S \<subseteq> topspace U \<and> openin U (topspace U - S)"
   16.60  
   16.61  lemma closedin_subset: "closedin U S \<Longrightarrow> S \<subseteq> topspace U"
   16.62    by (metis closedin_def)
   16.63 @@ -755,7 +755,7 @@
   16.64  
   16.65  subsubsection \<open>Subspace topology\<close>
   16.66  
   16.67 -definition "subtopology U V = topology (\<lambda>T. \<exists>S. T = S \<inter> V \<and> openin U S)"
   16.68 +definition%important "subtopology U V = topology (\<lambda>T. \<exists>S. T = S \<inter> V \<and> openin U S)"
   16.69  
   16.70  lemma istopology_subtopology: "istopology (\<lambda>T. \<exists>S. T = S \<inter> V \<and> openin U S)"
   16.71    (is "istopology ?L")
   16.72 @@ -870,7 +870,7 @@
   16.73  
   16.74  subsubsection \<open>The standard Euclidean topology\<close>
   16.75  
   16.76 -definition euclidean :: "'a::topological_space topology"
   16.77 +definition%important euclidean :: "'a::topological_space topology"
   16.78    where "euclidean = topology open"
   16.79  
   16.80  lemma open_openin: "open S \<longleftrightarrow> openin euclidean S"
   16.81 @@ -1054,13 +1054,13 @@
   16.82  
   16.83  subsection \<open>Open and closed balls\<close>
   16.84  
   16.85 -definition ball :: "'a::metric_space \<Rightarrow> real \<Rightarrow> 'a set"
   16.86 +definition%important ball :: "'a::metric_space \<Rightarrow> real \<Rightarrow> 'a set"
   16.87    where "ball x e = {y. dist x y < e}"
   16.88  
   16.89 -definition cball :: "'a::metric_space \<Rightarrow> real \<Rightarrow> 'a set"
   16.90 +definition%important cball :: "'a::metric_space \<Rightarrow> real \<Rightarrow> 'a set"
   16.91    where "cball x e = {y. dist x y \<le> e}"
   16.92  
   16.93 -definition sphere :: "'a::metric_space \<Rightarrow> real \<Rightarrow> 'a set"
   16.94 +definition%important sphere :: "'a::metric_space \<Rightarrow> real \<Rightarrow> 'a set"
   16.95    where "sphere x e = {y. dist x y = e}"
   16.96  
   16.97  lemma mem_ball [simp]: "y \<in> ball x e \<longleftrightarrow> dist x y < e"
   16.98 @@ -1327,11 +1327,11 @@
   16.99  corollary Zero_neq_One[iff]: "0 \<noteq> One"
  16.100    by (metis One_non_0)
  16.101  
  16.102 -definition (in euclidean_space) eucl_less (infix "<e" 50)
  16.103 +definition%important (in euclidean_space) eucl_less (infix "<e" 50)
  16.104    where "eucl_less a b \<longleftrightarrow> (\<forall>i\<in>Basis. a \<bullet> i < b \<bullet> i)"
  16.105  
  16.106 -definition box_eucl_less: "box a b = {x. a <e x \<and> x <e b}"
  16.107 -definition "cbox a b = {x. \<forall>i\<in>Basis. a \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> b \<bullet> i}"
  16.108 +definition%important box_eucl_less: "box a b = {x. a <e x \<and> x <e b}"
  16.109 +definition%important "cbox a b = {x. \<forall>i\<in>Basis. a \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> b \<bullet> i}"
  16.110  
  16.111  lemma box_def: "box a b = {x. \<forall>i\<in>Basis. a \<bullet> i < x \<bullet> i \<and> x \<bullet> i < b \<bullet> i}"
  16.112    and in_box_eucl_less: "x \<in> box a b \<longleftrightarrow> a <e x \<and> x <e b"
  16.113 @@ -1873,9 +1873,9 @@
  16.114      by (auto simp: box_def inner_sum_left inner_Basis sum.If_cases)
  16.115  qed
  16.116  
  16.117 -text \<open>Intervals in general, including infinite and mixtures of open and closed.\<close>
  16.118 -
  16.119 -definition "is_interval (s::('a::euclidean_space) set) \<longleftrightarrow>
  16.120 +subsection \<open>Intervals in general, including infinite and mixtures of open and closed.\<close>
  16.121 +
  16.122 +definition%important "is_interval (s::('a::euclidean_space) set) \<longleftrightarrow>
  16.123    (\<forall>a\<in>s. \<forall>b\<in>s. \<forall>x. (\<forall>i\<in>Basis. ((a\<bullet>i \<le> x\<bullet>i \<and> x\<bullet>i \<le> b\<bullet>i) \<or> (b\<bullet>i \<le> x\<bullet>i \<and> x\<bullet>i \<le> a\<bullet>i))) \<longrightarrow> x \<in> s)"
  16.124  
  16.125  lemma is_interval_1:
  16.126 @@ -2053,7 +2053,7 @@
  16.127  
  16.128  subsection \<open>Limit points\<close>
  16.129  
  16.130 -definition (in topological_space) islimpt:: "'a \<Rightarrow> 'a set \<Rightarrow> bool"  (infixr "islimpt" 60)
  16.131 +definition%important (in topological_space) islimpt:: "'a \<Rightarrow> 'a set \<Rightarrow> bool"  (infixr "islimpt" 60)
  16.132    where "x islimpt S \<longleftrightarrow> (\<forall>T. x\<in>T \<longrightarrow> open T \<longrightarrow> (\<exists>y\<in>S. y\<in>T \<and> y\<noteq>x))"
  16.133  
  16.134  lemma islimptI:
  16.135 @@ -2191,7 +2191,7 @@
  16.136  
  16.137  subsection \<open>Interior of a Set\<close>
  16.138  
  16.139 -definition "interior S = \<Union>{T. open T \<and> T \<subseteq> S}"
  16.140 +definition%important "interior S = \<Union>{T. open T \<and> T \<subseteq> S}"
  16.141  
  16.142  lemma interiorI [intro?]:
  16.143    assumes "open T" and "x \<in> T" and "T \<subseteq> S"
  16.144 @@ -2359,7 +2359,7 @@
  16.145  
  16.146  subsection \<open>Closure of a Set\<close>
  16.147  
  16.148 -definition "closure S = S \<union> {x | x. x islimpt S}"
  16.149 +definition%important "closure S = S \<union> {x | x. x islimpt S}"
  16.150  
  16.151  lemma interior_closure: "interior S = - (closure (- S))"
  16.152    by (auto simp: interior_def closure_def islimpt_def)
  16.153 @@ -2635,7 +2635,7 @@
  16.154  
  16.155  subsection \<open>Frontier (also known as boundary)\<close>
  16.156  
  16.157 -definition "frontier S = closure S - interior S"
  16.158 +definition%important "frontier S = closure S - interior S"
  16.159  
  16.160  lemma frontier_closed [iff]: "closed (frontier S)"
  16.161    by (simp add: frontier_def closed_Diff)
  16.162 @@ -2726,7 +2726,7 @@
  16.163  qed
  16.164  
  16.165  
  16.166 -subsection \<open>Filters and the ``eventually true'' quantifier\<close>
  16.167 +subsection%unimportant \<open>Filters and the ``eventually true'' quantifier\<close>
  16.168  
  16.169  definition indirection :: "'a::real_normed_vector \<Rightarrow> 'a \<Rightarrow> 'a filter"  (infixr "indirection" 70)
  16.170    where "a indirection v = at a within {b. \<exists>c\<ge>0. b - a = scaleR c v}"
  16.171 @@ -2794,16 +2794,16 @@
  16.172  
  16.173  subsection \<open>Limits\<close>
  16.174  
  16.175 -lemma Lim: "(f \<longlongrightarrow> l) net \<longleftrightarrow> trivial_limit net \<or> (\<forall>e>0. eventually (\<lambda>x. dist (f x) l < e) net)"
  16.176 +lemma%important Lim: "(f \<longlongrightarrow> l) net \<longleftrightarrow> trivial_limit net \<or> (\<forall>e>0. eventually (\<lambda>x. dist (f x) l < e) net)"
  16.177    by (auto simp: tendsto_iff trivial_limit_eq)
  16.178  
  16.179  text \<open>Show that they yield usual definitions in the various cases.\<close>
  16.180  
  16.181 -lemma Lim_within_le: "(f \<longlongrightarrow> l)(at a within S) \<longleftrightarrow>
  16.182 +lemma%important Lim_within_le: "(f \<longlongrightarrow> l)(at a within S) \<longleftrightarrow>
  16.183      (\<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)"
  16.184    by (auto simp: tendsto_iff eventually_at_le)
  16.185  
  16.186 -lemma Lim_within: "(f \<longlongrightarrow> l) (at a within S) \<longleftrightarrow>
  16.187 +lemma%important Lim_within: "(f \<longlongrightarrow> l) (at a within S) \<longleftrightarrow>
  16.188      (\<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)"
  16.189    by (auto simp: tendsto_iff eventually_at)
  16.190  
  16.191 @@ -2814,11 +2814,11 @@
  16.192    apply (rule ex_forward [OF assms [OF half_gt_zero]], auto)
  16.193    done
  16.194  
  16.195 -lemma Lim_at: "(f \<longlongrightarrow> l) (at a) \<longleftrightarrow>
  16.196 +lemma%important Lim_at: "(f \<longlongrightarrow> l) (at a) \<longleftrightarrow>
  16.197      (\<forall>e >0. \<exists>d>0. \<forall>x. 0 < dist x a \<and> dist x a < d  \<longrightarrow> dist (f x) l < e)"
  16.198    by (auto simp: tendsto_iff eventually_at)
  16.199  
  16.200 -lemma 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)"
  16.201 +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)"
  16.202    by (auto simp: tendsto_iff eventually_at_infinity)
  16.203  
  16.204  corollary Lim_at_infinityI [intro?]:
  16.205 @@ -3411,7 +3411,7 @@
  16.206  subsection \<open>Boundedness\<close>
  16.207  
  16.208    (* FIXME: This has to be unified with BSEQ!! *)
  16.209 -definition (in metric_space) bounded :: "'a set \<Rightarrow> bool"
  16.210 +definition%important (in metric_space) bounded :: "'a set \<Rightarrow> bool"
  16.211    where "bounded S \<longleftrightarrow> (\<exists>x e. \<forall>y\<in>S. dist x y \<le> e)"
  16.212  
  16.213  lemma bounded_subset_cball: "bounded S \<longleftrightarrow> (\<exists>e x. S \<subseteq> cball x e \<and> 0 \<le> e)"
  16.214 @@ -3690,12 +3690,12 @@
  16.215  
  16.216  subsubsection \<open>Bolzano-Weierstrass property\<close>
  16.217  
  16.218 -lemma heine_borel_imp_bolzano_weierstrass:
  16.219 +lemma%important heine_borel_imp_bolzano_weierstrass:
  16.220    assumes "compact s"
  16.221      and "infinite t"
  16.222      and "t \<subseteq> s"
  16.223    shows "\<exists>x \<in> s. x islimpt t"
  16.224 -proof (rule ccontr)
  16.225 +proof%unimportant (rule ccontr)
  16.226    assume "\<not> (\<exists>x \<in> s. x islimpt t)"
  16.227    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)"
  16.228      unfolding islimpt_def
  16.229 @@ -4157,7 +4157,7 @@
  16.230    with \<open>U \<inter> \<Inter>A = {}\<close> show False by auto
  16.231  qed
  16.232  
  16.233 -definition "countably_compact U \<longleftrightarrow>
  16.234 +definition%important "countably_compact U \<longleftrightarrow>
  16.235      (\<forall>A. countable A \<longrightarrow> (\<forall>a\<in>A. open a) \<longrightarrow> U \<subseteq> \<Union>A \<longrightarrow> (\<exists>T\<subseteq>A. finite T \<and> U \<subseteq> \<Union>T))"
  16.236  
  16.237  lemma countably_compactE:
  16.238 @@ -4208,9 +4208,9 @@
  16.239      unfolding C_def by (intro exI[of _ "f`T"]) fastforce
  16.240  qed
  16.241  
  16.242 -lemma countably_compact_imp_compact_second_countable:
  16.243 +lemma%important countably_compact_imp_compact_second_countable:
  16.244    "countably_compact U \<Longrightarrow> compact (U :: 'a :: second_countable_topology set)"
  16.245 -proof (rule countably_compact_imp_compact)
  16.246 +proof%unimportant (rule countably_compact_imp_compact)
  16.247    fix T and x :: 'a
  16.248    assume "open T" "x \<in> T"
  16.249    from topological_basisE[OF is_basis this] obtain b where
  16.250 @@ -4225,7 +4225,7 @@
  16.251  
  16.252  subsubsection\<open>Sequential compactness\<close>
  16.253  
  16.254 -definition seq_compact :: "'a::topological_space set \<Rightarrow> bool"
  16.255 +definition%important seq_compact :: "'a::topological_space set \<Rightarrow> bool"
  16.256    where "seq_compact S \<longleftrightarrow>
  16.257      (\<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) \<longlongrightarrow> l) sequentially))"
  16.258  
  16.259 @@ -4486,10 +4486,10 @@
  16.260    shows "seq_compact U \<longleftrightarrow> compact U"
  16.261    using seq_compact_eq_countably_compact countably_compact_eq_compact by blast
  16.262  
  16.263 -lemma bolzano_weierstrass_imp_seq_compact:
  16.264 +lemma%important bolzano_weierstrass_imp_seq_compact:
  16.265    fixes s :: "'a::{t1_space, first_countable_topology} set"
  16.266    shows "\<forall>t. infinite t \<and> t \<subseteq> s \<longrightarrow> (\<exists>x \<in> s. x islimpt t) \<Longrightarrow> seq_compact s"
  16.267 -  by (rule countable_acc_point_imp_seq_compact) (metis islimpt_eq_acc_point)
  16.268 +  by%unimportant (rule countable_acc_point_imp_seq_compact) (metis islimpt_eq_acc_point)
  16.269  
  16.270  
  16.271  subsubsection\<open>Totally bounded\<close>
  16.272 @@ -4497,10 +4497,10 @@
  16.273  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)"
  16.274    unfolding Cauchy_def by metis
  16.275  
  16.276 -lemma seq_compact_imp_totally_bounded:
  16.277 +lemma%important seq_compact_imp_totally_bounded:
  16.278    assumes "seq_compact s"
  16.279    shows "\<forall>e>0. \<exists>k. finite k \<and> k \<subseteq> s \<and> s \<subseteq> (\<Union>x\<in>k. ball x e)"
  16.280 -proof -
  16.281 +proof%unimportant -
  16.282    { 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)"
  16.283      let ?Q = "\<lambda>x n r. r \<in> s \<and> (\<forall>m < (n::nat). \<not> (dist (x m) r < e))"
  16.284      have "\<exists>x. \<forall>n::nat. ?Q x n (x n)"
  16.285 @@ -4529,11 +4529,11 @@
  16.286  
  16.287  subsubsection\<open>Heine-Borel theorem\<close>
  16.288  
  16.289 -lemma seq_compact_imp_heine_borel:
  16.290 +lemma%important seq_compact_imp_heine_borel:
  16.291    fixes s :: "'a :: metric_space set"
  16.292    assumes "seq_compact s"
  16.293    shows "compact s"
  16.294 -proof -
  16.295 +proof%unimportant -
  16.296    from seq_compact_imp_totally_bounded[OF \<open>seq_compact s\<close>]
  16.297    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)"
  16.298      unfolding choice_iff' ..
  16.299 @@ -4574,22 +4574,22 @@
  16.300    qed
  16.301  qed
  16.302  
  16.303 -lemma compact_eq_seq_compact_metric:
  16.304 +lemma%important compact_eq_seq_compact_metric:
  16.305    "compact (s :: 'a::metric_space set) \<longleftrightarrow> seq_compact s"
  16.306    using compact_imp_seq_compact seq_compact_imp_heine_borel by blast
  16.307  
  16.308 -lemma compact_def: \<comment> \<open>this is the definition of compactness in HOL Light\<close>
  16.309 +lemma%important compact_def: \<comment> \<open>this is the definition of compactness in HOL Light\<close>
  16.310    "compact (S :: 'a::metric_space set) \<longleftrightarrow>
  16.311     (\<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))"
  16.312    unfolding compact_eq_seq_compact_metric seq_compact_def by auto
  16.313  
  16.314  subsubsection \<open>Complete the chain of compactness variants\<close>
  16.315  
  16.316 -lemma compact_eq_bolzano_weierstrass:
  16.317 +lemma%important compact_eq_bolzano_weierstrass:
  16.318    fixes s :: "'a::metric_space set"
  16.319    shows "compact s \<longleftrightarrow> (\<forall>t. infinite t \<and> t \<subseteq> s --> (\<exists>x \<in> s. x islimpt t))"
  16.320    (is "?lhs = ?rhs")
  16.321 -proof
  16.322 +proof%unimportant
  16.323    assume ?lhs
  16.324    then show ?rhs
  16.325      using heine_borel_imp_bolzano_weierstrass[of s] by auto
  16.326 @@ -4599,7 +4599,7 @@
  16.327      unfolding compact_eq_seq_compact_metric by (rule bolzano_weierstrass_imp_seq_compact)
  16.328  qed
  16.329  
  16.330 -lemma bolzano_weierstrass_imp_bounded:
  16.331 +lemma%important bolzano_weierstrass_imp_bounded:
  16.332    "\<forall>t. infinite t \<and> t \<subseteq> s \<longrightarrow> (\<exists>x \<in> s. x islimpt t) \<Longrightarrow> bounded s"
  16.333    using compact_imp_bounded unfolding compact_eq_bolzano_weierstrass .
  16.334  
  16.335 @@ -4611,16 +4611,16 @@
  16.336    Heine-Borel property if every closed and bounded subset is compact.
  16.337  \<close>
  16.338  
  16.339 -class heine_borel = metric_space +
  16.340 +class%important heine_borel = metric_space +
  16.341    assumes bounded_imp_convergent_subsequence:
  16.342      "bounded (range f) \<Longrightarrow> \<exists>l r. strict_mono (r::nat\<Rightarrow>nat) \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially"
  16.343  
  16.344 -lemma bounded_closed_imp_seq_compact:
  16.345 +lemma%important bounded_closed_imp_seq_compact:
  16.346    fixes s::"'a::heine_borel set"
  16.347    assumes "bounded s"
  16.348      and "closed s"
  16.349    shows "seq_compact s"
  16.350 -proof (unfold seq_compact_def, clarify)
  16.351 +proof%unimportant (unfold seq_compact_def, clarify)
  16.352    fix f :: "nat \<Rightarrow> 'a"
  16.353    assume f: "\<forall>n. f n \<in> s"
  16.354    with \<open>bounded s\<close> have "bounded (range f)"
  16.355 @@ -4690,8 +4690,8 @@
  16.356      by (metis of_nat_le_iff Int_subset_iff \<open>K \<subseteq> S\<close> real_arch_simple subset_cball subset_trans)
  16.357  qed auto
  16.358  
  16.359 -instance real :: heine_borel
  16.360 -proof
  16.361 +instance%important real :: heine_borel
  16.362 +proof%unimportant
  16.363    fix f :: "nat \<Rightarrow> real"
  16.364    assume f: "bounded (range f)"
  16.365    obtain r :: "nat \<Rightarrow> nat" where r: "strict_mono r" "monoseq (f \<circ> r)"
  16.366 @@ -4771,8 +4771,8 @@
  16.367       (auto intro!: assms bounded_linear_inner_left bounded_linear_image
  16.368         simp: euclidean_representation)
  16.369  
  16.370 -instance euclidean_space \<subseteq> heine_borel
  16.371 -proof
  16.372 +instance%important euclidean_space \<subseteq> heine_borel
  16.373 +proof%unimportant
  16.374    fix f :: "nat \<Rightarrow> 'a"
  16.375    assume f: "bounded (range f)"
  16.376    then obtain l::'a and r where r: "strict_mono r"
  16.377 @@ -4818,8 +4818,8 @@
  16.378    unfolding bounded_def
  16.379    by (metis (no_types, hide_lams) dist_snd_le image_iff order.trans)
  16.380  
  16.381 -instance prod :: (heine_borel, heine_borel) heine_borel
  16.382 -proof
  16.383 +instance%important prod :: (heine_borel, heine_borel) heine_borel
  16.384 +proof%unimportant
  16.385    fix f :: "nat \<Rightarrow> 'a \<times> 'b"
  16.386    assume f: "bounded (range f)"
  16.387    then have "bounded (fst ` range f)"
  16.388 @@ -4845,12 +4845,12 @@
  16.389  
  16.390  subsubsection \<open>Completeness\<close>
  16.391  
  16.392 -lemma (in metric_space) completeI:
  16.393 +lemma%important (in metric_space) completeI:
  16.394    assumes "\<And>f. \<forall>n. f n \<in> s \<Longrightarrow> Cauchy f \<Longrightarrow> \<exists>l\<in>s. f \<longlonglongrightarrow> l"
  16.395    shows "complete s"
  16.396    using assms unfolding complete_def by fast
  16.397  
  16.398 -lemma (in metric_space) completeE:
  16.399 +lemma%important (in metric_space) completeE:
  16.400    assumes "complete s" and "\<forall>n. f n \<in> s" and "Cauchy f"
  16.401    obtains l where "l \<in> s" and "f \<longlonglongrightarrow> l"
  16.402    using assms unfolding complete_def by fast
  16.403 @@ -4900,10 +4900,10 @@
  16.404    then show ?thesis unfolding complete_def by auto
  16.405  qed
  16.406  
  16.407 -lemma compact_eq_totally_bounded:
  16.408 +lemma%important compact_eq_totally_bounded:
  16.409    "compact s \<longleftrightarrow> complete s \<and> (\<forall>e>0. \<exists>k. finite k \<and> s \<subseteq> (\<Union>x\<in>k. ball x e))"
  16.410      (is "_ \<longleftrightarrow> ?rhs")
  16.411 -proof
  16.412 +proof%unimportant
  16.413    assume assms: "?rhs"
  16.414    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)"
  16.415      by (auto simp: choice_iff')
  16.416 @@ -5107,7 +5107,7 @@
  16.417  
  16.418  text\<open>Derive the epsilon-delta forms, which we often use as "definitions"\<close>
  16.419  
  16.420 -lemma continuous_within_eps_delta:
  16.421 +lemma%important continuous_within_eps_delta:
  16.422    "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)"
  16.423    unfolding continuous_within and Lim_within  by fastforce
  16.424  
  16.425 @@ -5435,7 +5435,7 @@
  16.426    by (force intro: Lim_transform_within)
  16.427  
  16.428  
  16.429 -subsubsection \<open>Structural rules for pointwise continuity\<close>
  16.430 +subsubsection%unimportant \<open>Structural rules for pointwise continuity\<close>
  16.431  
  16.432  lemma continuous_infnorm[continuous_intros]:
  16.433    "continuous F f \<Longrightarrow> continuous F (\<lambda>x. infnorm (f x))"
  16.434 @@ -5447,7 +5447,7 @@
  16.435    shows "continuous F (\<lambda>x. inner (f x) (g x))"
  16.436    using assms unfolding continuous_def by (rule tendsto_inner)
  16.437  
  16.438 -subsubsection \<open>Structural rules for setwise continuity\<close>
  16.439 +subsubsection%unimportant \<open>Structural rules for setwise continuity\<close>
  16.440  
  16.441  lemma continuous_on_infnorm[continuous_intros]:
  16.442    "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. infnorm (f x))"
  16.443 @@ -5461,7 +5461,7 @@
  16.444    using bounded_bilinear_inner assms
  16.445    by (rule bounded_bilinear.continuous_on)
  16.446  
  16.447 -subsubsection \<open>Structural rules for uniform continuity\<close>
  16.448 +subsubsection%unimportant \<open>Structural rules for uniform continuity\<close>
  16.449  
  16.450  lemma uniformly_continuous_on_dist[continuous_intros]:
  16.451    fixes f g :: "'a::metric_space \<Rightarrow> 'b::metric_space"
  16.452 @@ -5653,7 +5653,7 @@
  16.453      shows "closedin (subtopology euclidean S) (S \<inter> f -` T)"
  16.454  using assms continuous_on_closed by blast
  16.455  
  16.456 -subsection \<open>Half-global and completely global cases.\<close>
  16.457 +subsection%unimportant \<open>Half-global and completely global cases.\<close>
  16.458  
  16.459  lemma continuous_openin_preimage_gen:
  16.460    assumes "continuous_on S f"  "open T"
  16.461 @@ -5743,7 +5743,7 @@
  16.462    with \<open>x = f y\<close> show "x \<in> f ` interior S" ..
  16.463  qed
  16.464  
  16.465 -subsection \<open>Topological properties of linear functions.\<close>
  16.466 +subsection%unimportant \<open>Topological properties of linear functions.\<close>
  16.467  
  16.468  lemma linear_lim_0:
  16.469    assumes "bounded_linear f"
  16.470 @@ -5771,7 +5771,7 @@
  16.471    "bounded_linear f \<Longrightarrow> continuous_on s f"
  16.472    using continuous_at_imp_continuous_on[of s f] using linear_continuous_at[of f] by auto
  16.473  
  16.474 -subsection \<open>Intervals\<close>
  16.475 +subsection%unimportant \<open>Intervals\<close>
  16.476  
  16.477  text \<open>Openness of halfspaces.\<close>
  16.478