--- a/src/HOL/Analysis/Arcwise_Connected.thy Mon Aug 27 22:58:36 2018 +0200
+++ b/src/HOL/Analysis/Arcwise_Connected.thy Tue Aug 28 13:28:39 2018 +0100
@@ -9,14 +9,14 @@
begin
-subsection\<open>The Brouwer reduction theorem\<close>
+subsection%important \<open>The Brouwer reduction theorem\<close>
-theorem Brouwer_reduction_theorem_gen:
+theorem%important Brouwer_reduction_theorem_gen:
fixes S :: "'a::euclidean_space set"
assumes "closed S" "\<phi> S"
and \<phi>: "\<And>F. \<lbrakk>\<And>n. closed(F n); \<And>n. \<phi>(F n); \<And>n. F(Suc n) \<subseteq> F n\<rbrakk> \<Longrightarrow> \<phi>(\<Inter>range F)"
obtains T where "T \<subseteq> S" "closed T" "\<phi> T" "\<And>U. \<lbrakk>U \<subseteq> S; closed U; \<phi> U\<rbrakk> \<Longrightarrow> \<not> (U \<subset> T)"
-proof -
+proof%unimportant -
obtain B :: "nat \<Rightarrow> 'a set"
where "inj B" "\<And>n. open(B n)" and open_cov: "\<And>S. open S \<Longrightarrow> \<exists>K. S = \<Union>(B ` K)"
by (metis Setcompr_eq_image that univ_second_countable_sequence)
@@ -79,13 +79,13 @@
qed
qed
-corollary Brouwer_reduction_theorem:
+corollary%important Brouwer_reduction_theorem:
fixes S :: "'a::euclidean_space set"
assumes "compact S" "\<phi> S" "S \<noteq> {}"
and \<phi>: "\<And>F. \<lbrakk>\<And>n. compact(F n); \<And>n. F n \<noteq> {}; \<And>n. \<phi>(F n); \<And>n. F(Suc n) \<subseteq> F n\<rbrakk> \<Longrightarrow> \<phi>(\<Inter>range F)"
obtains T where "T \<subseteq> S" "compact T" "T \<noteq> {}" "\<phi> T"
"\<And>U. \<lbrakk>U \<subseteq> S; closed U; U \<noteq> {}; \<phi> U\<rbrakk> \<Longrightarrow> \<not> (U \<subset> T)"
-proof (rule Brouwer_reduction_theorem_gen [of S "\<lambda>T. T \<noteq> {} \<and> T \<subseteq> S \<and> \<phi> T"])
+proof%unimportant (rule Brouwer_reduction_theorem_gen [of S "\<lambda>T. T \<noteq> {} \<and> T \<subseteq> S \<and> \<phi> T"])
fix F
assume cloF: "\<And>n. closed (F n)"
and F: "\<And>n. F n \<noteq> {} \<and> F n \<subseteq> S \<and> \<phi> (F n)" and Fsub: "\<And>n. F (Suc n) \<subseteq> F n"
@@ -107,14 +107,14 @@
qed (meson assms compact_imp_closed seq_compact_closed_subset seq_compact_eq_compact)+
-subsection\<open>Arcwise Connections\<close>
+subsection%important\<open>Arcwise Connections\<close>(*FIX ME this subsection is empty(?) *)
-subsection\<open>Density of points with dyadic rational coordinates\<close>
+subsection%important\<open>Density of points with dyadic rational coordinates\<close>
-proposition closure_dyadic_rationals:
+proposition%important closure_dyadic_rationals:
"closure (\<Union>k. \<Union>f \<in> Basis \<rightarrow> \<int>.
{ \<Sum>i :: 'a :: euclidean_space \<in> Basis. (f i / 2^k) *\<^sub>R i }) = UNIV"
-proof -
+proof%unimportant -
have "x \<in> closure (\<Union>k. \<Union>f \<in> Basis \<rightarrow> \<int>. {\<Sum>i \<in> Basis. (f i / 2^k) *\<^sub>R i})" for x::'a
proof (clarsimp simp: closure_approachable)
fix e::real
@@ -152,9 +152,9 @@
then show ?thesis by auto
qed
-corollary closure_rational_coordinates:
+corollary%important closure_rational_coordinates:
"closure (\<Union>f \<in> Basis \<rightarrow> \<rat>. { \<Sum>i :: 'a :: euclidean_space \<in> Basis. f i *\<^sub>R i }) = UNIV"
-proof -
+proof%unimportant -
have *: "(\<Union>k. \<Union>f \<in> Basis \<rightarrow> \<int>. { \<Sum>i::'a \<in> Basis. (f i / 2^k) *\<^sub>R i })
\<subseteq> (\<Union>f \<in> Basis \<rightarrow> \<rat>. { \<Sum>i \<in> Basis. f i *\<^sub>R i })"
proof clarsimp
@@ -168,7 +168,7 @@
using closure_dyadic_rationals closure_mono [OF *] by blast
qed
-lemma closure_dyadic_rationals_in_convex_set:
+lemma%unimportant closure_dyadic_rationals_in_convex_set:
"\<lbrakk>convex S; interior S \<noteq> {}\<rbrakk>
\<Longrightarrow> closure(S \<inter>
(\<Union>k. \<Union>f \<in> Basis \<rightarrow> \<int>.
@@ -176,7 +176,7 @@
closure S"
by (simp add: closure_dyadic_rationals closure_convex_Int_superset)
-lemma closure_rationals_in_convex_set:
+lemma%unimportant closure_rationals_in_convex_set:
"\<lbrakk>convex S; interior S \<noteq> {}\<rbrakk>
\<Longrightarrow> closure(S \<inter> (\<Union>f \<in> Basis \<rightarrow> \<rat>. { \<Sum>i :: 'a :: euclidean_space \<in> Basis. f i *\<^sub>R i })) =
closure S"
@@ -187,11 +187,11 @@
path connection is equivalent to arcwise connection for distinct points.
The proof is based on Whyburn's "Topological Analysis".\<close>
-lemma closure_dyadic_rationals_in_convex_set_pos_1:
+lemma%important closure_dyadic_rationals_in_convex_set_pos_1:
fixes S :: "real set"
assumes "convex S" and intnz: "interior S \<noteq> {}" and pos: "\<And>x. x \<in> S \<Longrightarrow> 0 \<le> x"
shows "closure(S \<inter> (\<Union>k m. {of_nat m / 2^k})) = closure S"
-proof -
+proof%unimportant -
have "\<exists>m. f 1/2^k = real m / 2^k" if "(f 1) / 2^k \<in> S" "f 1 \<in> \<int>" for k and f :: "real \<Rightarrow> real"
using that by (force simp: Ints_def zero_le_divide_iff power_le_zero_eq dest: pos zero_le_imp_eq_int)
then have "S \<inter> (\<Union>k m. {real m / 2^k}) = S \<inter>
@@ -202,13 +202,13 @@
qed
-definition dyadics :: "'a::field_char_0 set" where "dyadics \<equiv> \<Union>k m. {of_nat m / 2^k}"
+definition%important dyadics :: "'a::field_char_0 set" where "dyadics \<equiv> \<Union>k m. {of_nat m / 2^k}"
-lemma real_in_dyadics [simp]: "real m \<in> dyadics"
+lemma%unimportant real_in_dyadics [simp]: "real m \<in> dyadics"
apply (simp add: dyadics_def)
by (metis divide_numeral_1 numeral_One power_0)
-lemma nat_neq_4k1: "of_nat m \<noteq> (4 * of_nat k + 1) / (2 * 2^n :: 'a::field_char_0)"
+lemma%unimportant nat_neq_4k1: "of_nat m \<noteq> (4 * of_nat k + 1) / (2 * 2^n :: 'a::field_char_0)"
proof
assume "of_nat m = (4 * of_nat k + 1) / (2 * 2^n :: 'a)"
then have "of_nat (m * (2 * 2^n)) = (of_nat (Suc (4 * k)) :: 'a)"
@@ -221,8 +221,8 @@
by simp
qed
-lemma nat_neq_4k3: "of_nat m \<noteq> (4 * of_nat k + 3) / (2 * 2^n :: 'a::field_char_0)"
-proof
+lemma%important nat_neq_4k3: "of_nat m \<noteq> (4 * of_nat k + 3) / (2 * 2^n :: 'a::field_char_0)"
+proof%unimportant
assume "of_nat m = (4 * of_nat k + 3) / (2 * 2^n :: 'a)"
then have "of_nat (m * (2 * 2^n)) = (of_nat (4 * k + 3) :: 'a)"
by (simp add: divide_simps)
@@ -234,10 +234,10 @@
by simp
qed
-lemma iff_4k:
+lemma%important iff_4k:
assumes "r = real k" "odd k"
shows "(4 * real m + r) / (2 * 2^n) = (4 * real m' + r) / (2 * 2 ^ n') \<longleftrightarrow> m=m' \<and> n=n'"
-proof -
+proof%unimportant -
{ assume "(4 * real m + r) / (2 * 2^n) = (4 * real m' + r) / (2 * 2 ^ n')"
then have "real ((4 * m + k) * (2 * 2 ^ n')) = real ((4 * m' + k) * (2 * 2^n))"
using assms by (auto simp: field_simps)
@@ -254,8 +254,8 @@
then show ?thesis by blast
qed
-lemma neq_4k1_k43: "(4 * real m + 1) / (2 * 2^n) \<noteq> (4 * real m' + 3) / (2 * 2 ^ n')"
-proof
+lemma%important neq_4k1_k43: "(4 * real m + 1) / (2 * 2^n) \<noteq> (4 * real m' + 3) / (2 * 2 ^ n')"
+proof%unimportant
assume "(4 * real m + 1) / (2 * 2^n) = (4 * real m' + 3) / (2 * 2 ^ n')"
then have "real (Suc (4 * m) * (2 * 2 ^ n')) = real ((4 * m' + 3) * (2 * 2^n))"
by (auto simp: field_simps)
@@ -271,11 +271,11 @@
using even_Suc by presburger
qed
-lemma dyadic_413_cases:
+lemma%important dyadic_413_cases:
obtains "(of_nat m::'a::field_char_0) / 2^k \<in> Nats"
| m' k' where "k' < k" "(of_nat m:: 'a) / 2^k = of_nat (4*m' + 1) / 2^Suc k'"
| m' k' where "k' < k" "(of_nat m:: 'a) / 2^k = of_nat (4*m' + 3) / 2^Suc k'"
-proof (cases "m>0")
+proof%unimportant (cases "m>0")
case False
then have "m=0" by simp
with that show ?thesis by auto
@@ -324,11 +324,11 @@
qed
-lemma dyadics_iff:
+lemma%important dyadics_iff:
"(dyadics :: 'a::field_char_0 set) =
Nats \<union> (\<Union>k m. {of_nat (4*m + 1) / 2^Suc k}) \<union> (\<Union>k m. {of_nat (4*m + 3) / 2^Suc k})"
(is "_ = ?rhs")
-proof
+proof%unimportant
show "dyadics \<subseteq> ?rhs"
unfolding dyadics_def
apply clarify
@@ -355,14 +355,14 @@
apply (fastforce simp add: dyadics_iff Nats_def field_simps)+
done
-lemma dyadics_levels: "dyadics = (\<Union>K. \<Union>k<K. \<Union> m. {of_nat m / 2^k})"
+lemma%unimportant dyadics_levels: "dyadics = (\<Union>K. \<Union>k<K. \<Union> m. {of_nat m / 2^k})"
unfolding dyadics_def by auto
-lemma dyad_rec_level_termination:
+lemma%important dyad_rec_level_termination:
assumes "k < K"
shows "dyad_rec_dom(b, l, r, real m / 2^k)"
using assms
-proof (induction K arbitrary: k m)
+proof%unimportant (induction K arbitrary: k m)
case 0
then show ?case by auto
next
@@ -427,22 +427,22 @@
qed
-lemma dyad_rec_termination: "x \<in> dyadics \<Longrightarrow> dyad_rec_dom(b,l,r,x)"
+lemma%unimportant dyad_rec_termination: "x \<in> dyadics \<Longrightarrow> dyad_rec_dom(b,l,r,x)"
by (auto simp: dyadics_levels intro: dyad_rec_level_termination)
-lemma dyad_rec_of_nat [simp]: "dyad_rec b l r (real m) = b m"
+lemma%unimportant dyad_rec_of_nat [simp]: "dyad_rec b l r (real m) = b m"
by (simp add: dyad_rec.psimps dyad_rec_termination)
-lemma dyad_rec_41 [simp]: "dyad_rec b l r ((4 * real m + 1) / 2 ^ (Suc n)) = l (dyad_rec b l r ((2*m + 1) / 2^n))"
+lemma%unimportant dyad_rec_41 [simp]: "dyad_rec b l r ((4 * real m + 1) / 2 ^ (Suc n)) = l (dyad_rec b l r ((2*m + 1) / 2^n))"
apply (rule dyad_rec.psimps)
by (metis dyad_rec_level_termination lessI add.commute of_nat_Suc of_nat_mult of_nat_numeral)
-lemma dyad_rec_43 [simp]: "dyad_rec b l r ((4 * real m + 3) / 2 ^ (Suc n)) = r (dyad_rec b l r ((2*m + 1) / 2^n))"
+lemma%unimportant dyad_rec_43 [simp]: "dyad_rec b l r ((4 * real m + 3) / 2 ^ (Suc n)) = r (dyad_rec b l r ((2*m + 1) / 2^n))"
apply (rule dyad_rec.psimps)
by (metis dyad_rec_level_termination lessI of_nat_add of_nat_mult of_nat_numeral)
-lemma dyad_rec_41_times2:
+lemma%unimportant dyad_rec_41_times2:
assumes "n > 0"
shows "dyad_rec b l r (2 * ((4 * real m + 1) / 2^Suc n)) = l (dyad_rec b l r (2 * (2 * real m + 1) / 2^n))"
proof -
@@ -461,10 +461,10 @@
finally show ?thesis .
qed
-lemma dyad_rec_43_times2:
+lemma%important dyad_rec_43_times2:
assumes "n > 0"
shows "dyad_rec b l r (2 * ((4 * real m + 3) / 2^Suc n)) = r (dyad_rec b l r (2 * (2 * real m + 1) / 2^n))"
-proof -
+proof%unimportant -
obtain n' where n': "n = Suc n'"
using assms not0_implies_Suc by blast
have "dyad_rec b l r (2 * ((4 * real m + 3) / 2^Suc n)) = dyad_rec b l r ((2 * (4 * real m + 3)) / (2 * 2^n))"
@@ -480,22 +480,22 @@
finally show ?thesis .
qed
-definition dyad_rec2
+definition%important dyad_rec2
where "dyad_rec2 u v lc rc x =
dyad_rec (\<lambda>z. (u,v)) (\<lambda>(a,b). (a, lc a b (midpoint a b))) (\<lambda>(a,b). (rc a b (midpoint a b), b)) (2*x)"
abbreviation leftrec where "leftrec u v lc rc x \<equiv> fst (dyad_rec2 u v lc rc x)"
abbreviation rightrec where "rightrec u v lc rc x \<equiv> snd (dyad_rec2 u v lc rc x)"
-lemma leftrec_base: "leftrec u v lc rc (real m / 2) = u"
+lemma%unimportant leftrec_base: "leftrec u v lc rc (real m / 2) = u"
by (simp add: dyad_rec2_def)
-lemma leftrec_41: "n > 0 \<Longrightarrow> leftrec u v lc rc ((4 * real m + 1) / 2 ^ (Suc n)) = leftrec u v lc rc ((2 * real m + 1) / 2^n)"
+lemma%unimportant leftrec_41: "n > 0 \<Longrightarrow> leftrec u v lc rc ((4 * real m + 1) / 2 ^ (Suc n)) = leftrec u v lc rc ((2 * real m + 1) / 2^n)"
apply (simp only: dyad_rec2_def dyad_rec_41_times2)
apply (simp add: case_prod_beta)
done
-lemma leftrec_43: "n > 0 \<Longrightarrow>
+lemma%unimportant leftrec_43: "n > 0 \<Longrightarrow>
leftrec u v lc rc ((4 * real m + 3) / 2 ^ (Suc n)) =
rc (leftrec u v lc rc ((2 * real m + 1) / 2^n)) (rightrec u v lc rc ((2 * real m + 1) / 2^n))
(midpoint (leftrec u v lc rc ((2 * real m + 1) / 2^n)) (rightrec u v lc rc ((2 * real m + 1) / 2^n)))"
@@ -503,10 +503,10 @@
apply (simp add: case_prod_beta)
done
-lemma rightrec_base: "rightrec u v lc rc (real m / 2) = v"
+lemma%unimportant rightrec_base: "rightrec u v lc rc (real m / 2) = v"
by (simp add: dyad_rec2_def)
-lemma rightrec_41: "n > 0 \<Longrightarrow>
+lemma%unimportant rightrec_41: "n > 0 \<Longrightarrow>
rightrec u v lc rc ((4 * real m + 1) / 2 ^ (Suc n)) =
lc (leftrec u v lc rc ((2 * real m + 1) / 2^n)) (rightrec u v lc rc ((2 * real m + 1) / 2^n))
(midpoint (leftrec u v lc rc ((2 * real m + 1) / 2^n)) (rightrec u v lc rc ((2 * real m + 1) / 2^n)))"
@@ -514,24 +514,24 @@
apply (simp add: case_prod_beta)
done
-lemma rightrec_43: "n > 0 \<Longrightarrow> rightrec u v lc rc ((4 * real m + 3) / 2 ^ (Suc n)) = rightrec u v lc rc ((2 * real m + 1) / 2^n)"
+lemma%unimportant rightrec_43: "n > 0 \<Longrightarrow> rightrec u v lc rc ((4 * real m + 3) / 2 ^ (Suc n)) = rightrec u v lc rc ((2 * real m + 1) / 2^n)"
apply (simp only: dyad_rec2_def dyad_rec_43_times2)
apply (simp add: case_prod_beta)
done
-lemma dyadics_in_open_unit_interval:
+lemma%unimportant dyadics_in_open_unit_interval:
"{0<..<1} \<inter> (\<Union>k m. {real m / 2^k}) = (\<Union>k. \<Union>m \<in> {0<..<2^k}. {real m / 2^k})"
by (auto simp: divide_simps)
-theorem homeomorphic_monotone_image_interval:
+theorem%important homeomorphic_monotone_image_interval:
fixes f :: "real \<Rightarrow> 'a::{real_normed_vector,complete_space}"
assumes cont_f: "continuous_on {0..1} f"
and conn: "\<And>y. connected ({0..1} \<inter> f -` {y})"
and f_1not0: "f 1 \<noteq> f 0"
shows "(f ` {0..1}) homeomorphic {0..1::real}"
-proof -
+proof%unimportant -
have "\<exists>c d. a \<le> c \<and> c \<le> m \<and> m \<le> d \<and> d \<le> b \<and>
(\<forall>x \<in> {c..d}. f x = f m) \<and>
(\<forall>x \<in> {a..<c}. (f x \<noteq> f m)) \<and>
@@ -1664,11 +1664,11 @@
qed
-theorem path_contains_arc:
+theorem%important path_contains_arc:
fixes p :: "real \<Rightarrow> 'a::{complete_space,real_normed_vector}"
assumes "path p" and a: "pathstart p = a" and b: "pathfinish p = b" and "a \<noteq> b"
obtains q where "arc q" "path_image q \<subseteq> path_image p" "pathstart q = a" "pathfinish q = b"
-proof -
+proof%unimportant -
have ucont_p: "uniformly_continuous_on {0..1} p"
using \<open>path p\<close> unfolding path_def
by (metis compact_Icc compact_uniformly_continuous)
@@ -1961,12 +1961,12 @@
qed
-corollary path_connected_arcwise:
+corollary%important path_connected_arcwise:
fixes S :: "'a::{complete_space,real_normed_vector} set"
shows "path_connected S \<longleftrightarrow>
(\<forall>x \<in> S. \<forall>y \<in> S. x \<noteq> y \<longrightarrow> (\<exists>g. arc g \<and> path_image g \<subseteq> S \<and> pathstart g = x \<and> pathfinish g = y))"
(is "?lhs = ?rhs")
-proof (intro iffI impI ballI)
+proof%unimportant (intro iffI impI ballI)
fix x y
assume "path_connected S" "x \<in> S" "y \<in> S" "x \<noteq> y"
then obtain p where p: "path p" "path_image p \<subseteq> S" "pathstart p = x" "pathfinish p = y"
@@ -1992,23 +1992,23 @@
qed
-corollary arc_connected_trans:
+corollary%important arc_connected_trans:
fixes g :: "real \<Rightarrow> 'a::{complete_space,real_normed_vector}"
assumes "arc g" "arc h" "pathfinish g = pathstart h" "pathstart g \<noteq> pathfinish h"
obtains i where "arc i" "path_image i \<subseteq> path_image g \<union> path_image h"
"pathstart i = pathstart g" "pathfinish i = pathfinish h"
- by (metis (no_types, hide_lams) arc_imp_path assms path_contains_arc path_image_join path_join pathfinish_join pathstart_join)
+ by%unimportant (metis (no_types, hide_lams) arc_imp_path assms path_contains_arc path_image_join path_join pathfinish_join pathstart_join)
-subsection\<open>Accessibility of frontier points\<close>
+subsection%important\<open>Accessibility of frontier points\<close>
-lemma dense_accessible_frontier_points:
+lemma%important dense_accessible_frontier_points:
fixes S :: "'a::{complete_space,real_normed_vector} set"
assumes "open S" and opeSV: "openin (subtopology euclidean (frontier S)) V" and "V \<noteq> {}"
obtains g where "arc g" "g ` {0..<1} \<subseteq> S" "pathstart g \<in> S" "pathfinish g \<in> V"
-proof -
+proof%unimportant -
obtain z where "z \<in> V"
using \<open>V \<noteq> {}\<close> by auto
then obtain r where "r > 0" and r: "ball z r \<inter> frontier S \<subseteq> V"
@@ -2099,12 +2099,12 @@
qed
-lemma dense_accessible_frontier_points_connected:
+lemma%important dense_accessible_frontier_points_connected:
fixes S :: "'a::{complete_space,real_normed_vector} set"
assumes "open S" "connected S" "x \<in> S" "V \<noteq> {}"
and ope: "openin (subtopology euclidean (frontier S)) V"
obtains g where "arc g" "g ` {0..<1} \<subseteq> S" "pathstart g = x" "pathfinish g \<in> V"
-proof -
+proof%unimportant -
have "V \<subseteq> frontier S"
using ope openin_imp_subset by blast
with \<open>open S\<close> \<open>x \<in> S\<close> have "x \<notin> V"
@@ -2134,14 +2134,14 @@
using h \<open>pathfinish g \<in> V\<close> by auto
qed
-lemma dense_access_fp_aux:
+lemma%important dense_access_fp_aux:
fixes S :: "'a::{complete_space,real_normed_vector} set"
assumes S: "open S" "connected S"
and opeSU: "openin (subtopology euclidean (frontier S)) U"
and opeSV: "openin (subtopology euclidean (frontier S)) V"
and "V \<noteq> {}" "\<not> U \<subseteq> V"
obtains g where "arc g" "pathstart g \<in> U" "pathfinish g \<in> V" "g ` {0<..<1} \<subseteq> S"
-proof -
+proof%unimportant -
have "S \<noteq> {}"
using opeSV \<open>V \<noteq> {}\<close> by (metis frontier_empty openin_subtopology_empty)
then obtain x where "x \<in> S" by auto
@@ -2181,14 +2181,14 @@
qed
qed
-lemma dense_accessible_frontier_point_pairs:
+lemma%important dense_accessible_frontier_point_pairs:
fixes S :: "'a::{complete_space,real_normed_vector} set"
assumes S: "open S" "connected S"
and opeSU: "openin (subtopology euclidean (frontier S)) U"
and opeSV: "openin (subtopology euclidean (frontier S)) V"
and "U \<noteq> {}" "V \<noteq> {}" "U \<noteq> V"
obtains g where "arc g" "pathstart g \<in> U" "pathfinish g \<in> V" "g ` {0<..<1} \<subseteq> S"
-proof -
+proof%unimportant -
consider "\<not> U \<subseteq> V" | "\<not> V \<subseteq> U"
using \<open>U \<noteq> V\<close> by blast
then show ?thesis