diff -r e77cb3792503 -r 21d7910d6816 src/HOL/Multivariate_Analysis/Path_Connected.thy --- a/src/HOL/Multivariate_Analysis/Path_Connected.thy Fri Nov 20 12:22:50 2015 +0100 +++ b/src/HOL/Multivariate_Analysis/Path_Connected.thy Fri Nov 20 14:44:53 2015 +0000 @@ -638,6 +638,10 @@ by (simp add: algebra_simps) qed +lemma sum_le_prod1: + fixes a::real shows "\a \ 1; b \ 1\ \ a + b \ 1 + a * b" +by (metis add.commute affine_ineq less_eq_real_def mult.right_neutral) + lemma simple_path_subpath_eq: "simple_path(subpath u v g) \ path(subpath u v g) \ u\v \ @@ -1013,6 +1017,12 @@ lemma simple_path_linepath[intro]: "a \ b \ simple_path (linepath a b)" by (simp add: arc_imp_simple_path arc_linepath) +lemma linepath_trivial [simp]: "linepath a a x = a" + by (simp add: linepath_def real_vector.scale_left_diff_distrib) + +lemma subpath_refl: "subpath a a g = linepath (g a) (g a)" + by (simp add: subpath_def linepath_def algebra_simps) + subsection \Bounding a point away from a path\ @@ -2912,4 +2922,275 @@ apply (auto simp: pathstart_def pathfinish_def elim!: homotopic_with_mono) done +subsection\Group properties for homotopy of paths\ + +text\So taking equivalence classes under homotopy would give the fundamental group\ + +proposition homotopic_paths_rid: + "\path p; path_image p \ s\ \ homotopic_paths s (p +++ linepath (pathfinish p) (pathfinish p)) p" + apply (subst homotopic_paths_sym) + apply (rule homotopic_paths_reparametrize [where f = "\t. if t \ 1 / 2 then 2 *\<^sub>R t else 1"]) + apply (simp_all del: le_divide_eq_numeral1) + apply (subst split_01) + apply (rule continuous_on_cases continuous_intros | force simp: pathfinish_def joinpaths_def)+ + done + +proposition homotopic_paths_lid: + "\path p; path_image p \ s\ \ homotopic_paths s (linepath (pathstart p) (pathstart p) +++ p) p" +using homotopic_paths_rid [of "reversepath p" s] + by (metis homotopic_paths_reversepath path_image_reversepath path_reversepath pathfinish_linepath + pathfinish_reversepath reversepath_joinpaths reversepath_linepath) + +proposition homotopic_paths_assoc: + "\path p; path_image p \ s; path q; path_image q \ s; path r; path_image r \ s; pathfinish p = pathstart q; + pathfinish q = pathstart r\ + \ homotopic_paths s (p +++ (q +++ r)) ((p +++ q) +++ r)" + apply (subst homotopic_paths_sym) + apply (rule homotopic_paths_reparametrize + [where f = "\t. if t \ 1 / 2 then inverse 2 *\<^sub>R t + else if t \ 3 / 4 then t - (1 / 4) + else 2 *\<^sub>R t - 1"]) + apply (simp_all del: le_divide_eq_numeral1) + apply (simp add: subset_path_image_join) + apply (rule continuous_on_cases_1 continuous_intros)+ + apply (auto simp: joinpaths_def) + done + +proposition homotopic_paths_rinv: + assumes "path p" "path_image p \ s" + shows "homotopic_paths s (p +++ reversepath p) (linepath (pathstart p) (pathstart p))" +proof - + have "continuous_on ({0..1} \ {0..1}) (\x. (subpath 0 (fst x) p +++ reversepath (subpath 0 (fst x) p)) (snd x))" + using assms + apply (simp add: joinpaths_def subpath_def reversepath_def path_def del: le_divide_eq_numeral1) + apply (rule continuous_on_cases_le) + apply (rule_tac [2] continuous_on_compose [of _ _ p, unfolded o_def]) + apply (rule continuous_on_compose [of _ _ p, unfolded o_def]) + apply (auto intro!: continuous_intros simp del: eq_divide_eq_numeral1) + apply (force elim!: continuous_on_subset simp add: mult_le_one)+ + done + then show ?thesis + using assms + apply (subst homotopic_paths_sym) + apply (simp add: homotopic_paths_def homotopic_with_def) + apply (rule_tac x="(\y. (subpath 0 (fst y) p +++ reversepath(subpath 0 (fst y) p)) (snd y))" in exI) + apply (simp add: path_defs joinpaths_def subpath_def reversepath_def) + apply (force simp: mult_le_one) + done +qed + +proposition homotopic_paths_linv: + assumes "path p" "path_image p \ s" + shows "homotopic_paths s (reversepath p +++ p) (linepath (pathfinish p) (pathfinish p))" +using homotopic_paths_rinv [of "reversepath p" s] assms by simp + + +subsection\ Homotopy of loops without requiring preservation of endpoints.\ + +definition homotopic_loops :: "'a::topological_space set \ (real \ 'a) \ (real \ 'a) \ bool" where + "homotopic_loops s p q \ + homotopic_with (\r. pathfinish r = pathstart r) {0..1} s p q" + +lemma homotopic_loops: + "homotopic_loops s p q \ + (\h. continuous_on ({0..1::real} \ {0..1}) h \ + image h ({0..1} \ {0..1}) \ s \ + (\x \ {0..1}. h(0,x) = p x) \ + (\x \ {0..1}. h(1,x) = q x) \ + (\t \ {0..1}. pathfinish(h o Pair t) = pathstart(h o Pair t)))" + by (simp add: homotopic_loops_def pathstart_def pathfinish_def homotopic_with) + +proposition homotopic_loops_imp_loop: + "homotopic_loops s p q \ pathfinish p = pathstart p \ pathfinish q = pathstart q" +using homotopic_with_imp_property homotopic_loops_def by blast + +proposition homotopic_loops_imp_path: + "homotopic_loops s p q \ path p \ path q" + unfolding homotopic_loops_def path_def + using homotopic_with_imp_continuous by blast + +proposition homotopic_loops_imp_subset1: + "homotopic_loops s p q \ path_image p \ s" + unfolding homotopic_loops_def path_image_def + using homotopic_with_imp_subset1 by blast + +proposition homotopic_loops_imp_subset2: + "homotopic_loops s p q \ path_image q \ s" + unfolding homotopic_loops_def path_image_def + using homotopic_with_imp_subset2 by blast + +proposition homotopic_loops_refl: + "homotopic_loops s p p \ + path p \ path_image p \ s \ pathfinish p = pathstart p" + by (simp add: homotopic_loops_def homotopic_with_refl path_image_def path_def) + +proposition homotopic_loops_sym: + "homotopic_loops s p q \ homotopic_loops s q p" + by (simp add: homotopic_loops_def homotopic_with_sym) + +proposition homotopic_loops_trans: + "\homotopic_loops s p q; homotopic_loops s q r\ \ homotopic_loops s p r" + unfolding homotopic_loops_def by (blast intro: homotopic_with_trans) + +proposition homotopic_loops_subset: + "\homotopic_loops s p q; s \ t\ \ homotopic_loops t p q" + by (simp add: homotopic_loops_def homotopic_with_subset_right) + +proposition homotopic_loops_eq: + "\path p; path_image p \ s; pathfinish p = pathstart p; \t. t \ {0..1} \ p(t) = q(t)\ + \ homotopic_loops s p q" + unfolding homotopic_loops_def + apply (rule homotopic_with_eq) + apply (rule homotopic_with_refl [where f = p, THEN iffD2]) + apply (simp_all add: path_image_def path_def pathstart_def pathfinish_def) + done + +proposition homotopic_loops_continuous_image: + "\homotopic_loops s f g; continuous_on s h; h ` s \ t\ \ homotopic_loops t (h \ f) (h \ g)" + unfolding homotopic_loops_def + apply (rule homotopic_with_compose_continuous_left) + apply (erule homotopic_with_mono) + by (simp add: pathfinish_def pathstart_def) + + +subsection\Relations between the two variants of homotopy\ + +proposition homotopic_paths_imp_homotopic_loops: + "\homotopic_paths s p q; pathfinish p = pathstart p; pathfinish q = pathstart p\ \ homotopic_loops s p q" + by (auto simp: homotopic_paths_def homotopic_loops_def intro: homotopic_with_mono) + +proposition homotopic_loops_imp_homotopic_paths_null: + assumes "homotopic_loops s p (linepath a a)" + shows "homotopic_paths s p (linepath (pathstart p) (pathstart p))" +proof - + have "path p" by (metis assms homotopic_loops_imp_path) + have ploop: "pathfinish p = pathstart p" by (metis assms homotopic_loops_imp_loop) + have pip: "path_image p \ s" by (metis assms homotopic_loops_imp_subset1) + obtain h where conth: "continuous_on ({0..1::real} \ {0..1}) h" + and hs: "h ` ({0..1} \ {0..1}) \ s" + and [simp]: "\x. x \ {0..1} \ h(0,x) = p x" + and [simp]: "\x. x \ {0..1} \ h(1,x) = a" + and ends: "\t. t \ {0..1} \ pathfinish (h \ Pair t) = pathstart (h \ Pair t)" + using assms by (auto simp: homotopic_loops homotopic_with) + have conth0: "path (\u. h (u, 0))" + unfolding path_def + apply (rule continuous_on_compose [of _ _ h, unfolded o_def]) + apply (force intro: continuous_intros continuous_on_subset [OF conth])+ + done + have pih0: "path_image (\u. h (u, 0)) \ s" + using hs by (force simp: path_image_def) + have c1: "continuous_on ({0..1} \ {0..1}) (\x. h (fst x * snd x, 0))" + apply (rule continuous_on_compose [of _ _ h, unfolded o_def]) + apply (force simp: mult_le_one intro: continuous_intros continuous_on_subset [OF conth])+ + done + have c2: "continuous_on ({0..1} \ {0..1}) (\x. h (fst x - fst x * snd x, 0))" + apply (rule continuous_on_compose [of _ _ h, unfolded o_def]) + apply (force simp: mult_left_le mult_le_one intro: continuous_intros continuous_on_subset [OF conth])+ + apply (rule continuous_on_subset [OF conth]) + apply (auto simp: algebra_simps add_increasing2 mult_left_le) + done + have [simp]: "\t. \0 \ t \ t \ 1\ \ h (t, 1) = h (t, 0)" + using ends by (simp add: pathfinish_def pathstart_def) + have adhoc_le: "c * 4 \ 1 + c * (d * 4)" if "\ d * 4 \ 3" "0 \ c" "c \ 1" for c d::real + proof - + have "c * 3 \ c * (d * 4)" using that less_eq_real_def by auto + with \c \ 1\ show ?thesis by fastforce + qed + have *: "\p x. (path p \ path(reversepath p)) \ + (path_image p \ s \ path_image(reversepath p) \ s) \ + (pathfinish p = pathstart(linepath a a +++ reversepath p) \ + pathstart(reversepath p) = a) \ pathstart p = x + \ homotopic_paths s (p +++ linepath a a +++ reversepath p) (linepath x x)" + by (metis homotopic_paths_lid homotopic_paths_join + homotopic_paths_trans homotopic_paths_sym homotopic_paths_rinv) + have 1: "homotopic_paths s p (p +++ linepath (pathfinish p) (pathfinish p))" + using \path p\ homotopic_paths_rid homotopic_paths_sym pip by blast + moreover have "homotopic_paths s (p +++ linepath (pathfinish p) (pathfinish p)) + (linepath (pathstart p) (pathstart p) +++ p +++ linepath (pathfinish p) (pathfinish p))" + apply (subst homotopic_paths_sym) + using homotopic_paths_lid [of "p +++ linepath (pathfinish p) (pathfinish p)" s] + by (metis 1 homotopic_paths_imp_path homotopic_paths_imp_pathstart homotopic_paths_imp_subset) + moreover have "homotopic_paths s (linepath (pathstart p) (pathstart p) +++ p +++ linepath (pathfinish p) (pathfinish p)) + ((\u. h (u, 0)) +++ linepath a a +++ reversepath (\u. h (u, 0)))" + apply (simp add: homotopic_paths_def homotopic_with_def) + apply (rule_tac x="\y. (subpath 0 (fst y) (\u. h (u, 0)) +++ (\u. h (Pair (fst y) u)) +++ subpath (fst y) 0 (\u. h (u, 0))) (snd y)" in exI) + apply (simp add: subpath_reversepath) + apply (intro conjI homotopic_join_lemma) + using ploop + apply (simp_all add: path_defs joinpaths_def o_def subpath_def conth c1 c2) + apply (force simp: algebra_simps mult_le_one mult_left_le intro: hs [THEN subsetD] adhoc_le) + done + moreover have "homotopic_paths s ((\u. h (u, 0)) +++ linepath a a +++ reversepath (\u. h (u, 0))) + (linepath (pathstart p) (pathstart p))" + apply (rule *) + apply (simp add: pih0 pathstart_def pathfinish_def conth0) + apply (simp add: reversepath_def joinpaths_def) + done + ultimately show ?thesis + by (blast intro: homotopic_paths_trans) +qed + +proposition homotopic_loops_conjugate: + fixes s :: "'a::real_normed_vector set" + assumes "path p" "path q" and pip: "path_image p \ s" and piq: "path_image q \ s" + and papp: "pathfinish p = pathstart q" and qloop: "pathfinish q = pathstart q" + shows "homotopic_loops s (p +++ q +++ reversepath p) q" +proof - + have contp: "continuous_on {0..1} p" using \path p\ [unfolded path_def] by blast + have contq: "continuous_on {0..1} q" using \path q\ [unfolded path_def] by blast + have c1: "continuous_on ({0..1} \ {0..1}) (\x. p ((1 - fst x) * snd x + fst x))" + apply (rule continuous_on_compose [of _ _ p, unfolded o_def]) + apply (force simp: mult_le_one intro!: continuous_intros) + apply (rule continuous_on_subset [OF contp]) + apply (auto simp: algebra_simps add_increasing2 mult_right_le_one_le sum_le_prod1) + done + have c2: "continuous_on ({0..1} \ {0..1}) (\x. p ((fst x - 1) * snd x + 1))" + apply (rule continuous_on_compose [of _ _ p, unfolded o_def]) + apply (force simp: mult_le_one intro!: continuous_intros) + apply (rule continuous_on_subset [OF contp]) + apply (auto simp: algebra_simps add_increasing2 mult_left_le_one_le) + done + have ps1: "\a b. \b * 2 \ 1; 0 \ b; 0 \ a; a \ 1\ \ p ((1 - a) * (2 * b) + a) \ s" + using sum_le_prod1 + by (force simp: algebra_simps add_increasing2 mult_left_le intro: pip [unfolded path_image_def, THEN subsetD]) + have ps2: "\a b. \\ 4 * b \ 3; b \ 1; 0 \ a; a \ 1\ \ p ((a - 1) * (4 * b - 3) + 1) \ s" + apply (rule pip [unfolded path_image_def, THEN subsetD]) + apply (rule image_eqI, blast) + apply (simp add: algebra_simps) + by (metis add_mono_thms_linordered_semiring(1) affine_ineq linear mult.commute mult.left_neutral mult_right_mono not_le + add.commute zero_le_numeral) + have qs: "\a b. \4 * b \ 3; \ b * 2 \ 1\ \ q (4 * b - 2) \ s" + using path_image_def piq by fastforce + have "homotopic_loops s (p +++ q +++ reversepath p) + (linepath (pathstart q) (pathstart q) +++ q +++ linepath (pathstart q) (pathstart q))" + apply (simp add: homotopic_loops_def homotopic_with_def) + apply (rule_tac x="(\y. (subpath (fst y) 1 p +++ q +++ subpath 1 (fst y) p) (snd y))" in exI) + apply (simp add: subpath_refl subpath_reversepath) + apply (intro conjI homotopic_join_lemma) + using papp qloop + apply (simp_all add: path_defs joinpaths_def o_def subpath_def c1 c2) + apply (force simp: contq intro: continuous_on_compose [of _ _ q, unfolded o_def] continuous_on_id continuous_on_snd) + apply (auto simp: ps1 ps2 qs) + done + moreover have "homotopic_loops s (linepath (pathstart q) (pathstart q) +++ q +++ linepath (pathstart q) (pathstart q)) q" + proof - + have "homotopic_paths s (linepath (pathfinish q) (pathfinish q) +++ q) q" + using \path q\ homotopic_paths_lid qloop piq by auto + hence 1: "\f. homotopic_paths s f q \ \ homotopic_paths s f (linepath (pathfinish q) (pathfinish q) +++ q)" + using homotopic_paths_trans by blast + hence "homotopic_paths s (linepath (pathfinish q) (pathfinish q) +++ q +++ linepath (pathfinish q) (pathfinish q)) q" + proof - + have "homotopic_paths s (q +++ linepath (pathfinish q) (pathfinish q)) q" + by (simp add: \path q\ homotopic_paths_rid piq) + thus ?thesis + by (metis (no_types) 1 \path q\ homotopic_paths_join homotopic_paths_rinv homotopic_paths_sym + homotopic_paths_trans qloop pathfinish_linepath piq) + qed + thus ?thesis + by (metis (no_types) qloop homotopic_loops_sym homotopic_paths_imp_homotopic_loops homotopic_paths_imp_pathfinish homotopic_paths_sym) + qed + ultimately show ?thesis + by (blast intro: homotopic_loops_trans) +qed + end