
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 "\<lbrakk>a \<le> 1; b \<le> 1\<rbrakk> \<Longrightarrow> a + b \<le> 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) \<longleftrightarrow>
      path(subpath u v g) \<and> u\<noteq>v \<and>
@@ -1013,6 +1017,12 @@
 lemma simple_path_linepath[intro]: "a \<noteq> b \<Longrightarrow> 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 \<open>Bounding a point away from a path\<close>
 
@@ -2912,4 +2922,275 @@
   apply (auto simp: pathstart_def pathfinish_def elim!: homotopic_with_mono)
   done
 
+subsection\<open>Group properties for homotopy of paths\<close>
+
+text\<open>So taking equivalence classes under homotopy would give the fundamental group\<close>
+
+proposition homotopic_paths_rid:
+    "\<lbrakk>path p; path_image p \<subseteq> s\<rbrakk> \<Longrightarrow> homotopic_paths s (p +++ linepath (pathfinish p) (pathfinish p)) p"
+  apply (subst homotopic_paths_sym)
+  apply (rule homotopic_paths_reparametrize [where f = "\<lambda>t. if  t \<le> 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:
+   "\<lbrakk>path p; path_image p \<subseteq> s\<rbrakk> \<Longrightarrow> 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:
+   "\<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;
+     pathfinish q = pathstart r\<rbrakk>
+    \<Longrightarrow> homotopic_paths s (p +++ (q +++ r)) ((p +++ q) +++ r)"
+  apply (subst homotopic_paths_sym)
+  apply (rule homotopic_paths_reparametrize
+           [where f = "\<lambda>t. if  t \<le> 1 / 2 then inverse 2 *\<^sub>R t
+                           else if  t \<le> 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 \<subseteq> s"
+    shows "homotopic_paths s (p +++ reversepath p) (linepath (pathstart p) (pathstart p))"
+proof -
+  have "continuous_on ({0..1} \<times> {0..1}) (\<lambda>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="(\<lambda>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 \<subseteq> 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\<open> Homotopy of loops without requiring preservation of endpoints.\<close>
+
+definition homotopic_loops :: "'a::topological_space set \<Rightarrow> (real \<Rightarrow> 'a) \<Rightarrow> (real \<Rightarrow> 'a) \<Rightarrow> bool"  where
+ "homotopic_loops s p q \<equiv>
+     homotopic_with (\<lambda>r. pathfinish r = pathstart r) {0..1} s p q"
+
+lemma homotopic_loops:
+   "homotopic_loops s p q \<longleftrightarrow>
+      (\<exists>h. continuous_on ({0..1::real} \<times> {0..1}) h \<and>
+          image h ({0..1} \<times> {0..1}) \<subseteq> s \<and>
+          (\<forall>x \<in> {0..1}. h(0,x) = p x) \<and>
+          (\<forall>x \<in> {0..1}. h(1,x) = q x) \<and>
+          (\<forall>t \<in> {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 \<Longrightarrow> pathfinish p = pathstart p \<and> pathfinish q = pathstart q"
+using homotopic_with_imp_property homotopic_loops_def by blast
+
+proposition homotopic_loops_imp_path:
+     "homotopic_loops s p q \<Longrightarrow> path p \<and> 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 \<Longrightarrow> path_image p \<subseteq> 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 \<Longrightarrow> path_image q \<subseteq> s"
+  unfolding homotopic_loops_def path_image_def
+  using homotopic_with_imp_subset2 by blast
+
+proposition homotopic_loops_refl:
+     "homotopic_loops s p p \<longleftrightarrow>
+      path p \<and> path_image p \<subseteq> s \<and> 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 \<longleftrightarrow> homotopic_loops s q p"
+  by (simp add: homotopic_loops_def homotopic_with_sym)
+
+proposition homotopic_loops_trans:
+   "\<lbrakk>homotopic_loops s p q; homotopic_loops s q r\<rbrakk> \<Longrightarrow> homotopic_loops s p r"
+  unfolding homotopic_loops_def by (blast intro: homotopic_with_trans)
+
+proposition homotopic_loops_subset:
+   "\<lbrakk>homotopic_loops s p q; s \<subseteq> t\<rbrakk> \<Longrightarrow> homotopic_loops t p q"
+  by (simp add: homotopic_loops_def homotopic_with_subset_right)
+
+proposition homotopic_loops_eq:
+   "\<lbrakk>path p; path_image p \<subseteq> s; pathfinish p = pathstart p; \<And>t. t \<in> {0..1} \<Longrightarrow> p(t) = q(t)\<rbrakk>
+          \<Longrightarrow> 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:
+   "\<lbrakk>homotopic_loops s f g; continuous_on s h; h ` s \<subseteq> t\<rbrakk> \<Longrightarrow> homotopic_loops t (h \<circ> f) (h \<circ> 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\<open>Relations between the two variants of homotopy\<close>
+
+proposition homotopic_paths_imp_homotopic_loops:
+    "\<lbrakk>homotopic_paths s p q; pathfinish p = pathstart p; pathfinish q = pathstart p\<rbrakk> \<Longrightarrow> 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 \<subseteq> s" by (metis assms homotopic_loops_imp_subset1)
+  obtain h where conth: "continuous_on ({0..1::real} \<times> {0..1}) h"
+             and hs: "h ` ({0..1} \<times> {0..1}) \<subseteq> s"
+             and [simp]: "\<And>x. x \<in> {0..1} \<Longrightarrow> h(0,x) = p x"
+             and [simp]: "\<And>x. x \<in> {0..1} \<Longrightarrow> h(1,x) = a"
+             and ends: "\<And>t. t \<in> {0..1} \<Longrightarrow> pathfinish (h \<circ> Pair t) = pathstart (h \<circ> Pair t)"
+    using assms by (auto simp: homotopic_loops homotopic_with)
+  have conth0: "path (\<lambda>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 (\<lambda>u. h (u, 0)) \<subseteq> s"
+    using hs by (force simp: path_image_def)
+  have c1: "continuous_on ({0..1} \<times> {0..1}) (\<lambda>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} \<times> {0..1}) (\<lambda>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]: "\<And>t. \<lbrakk>0 \<le> t \<and> t \<le> 1\<rbrakk> \<Longrightarrow> h (t, 1) = h (t, 0)"
+    using ends by (simp add: pathfinish_def pathstart_def)
+  have adhoc_le: "c * 4 \<le> 1 + c * (d * 4)" if "\<not> d * 4 \<le> 3" "0 \<le> c" "c \<le> 1" for c d::real
+  proof -
+    have "c * 3 \<le> c * (d * 4)" using that less_eq_real_def by auto
+    with \<open>c \<le> 1\<close> show ?thesis by fastforce
+  qed
+  have *: "\<And>p x. (path p \<and> path(reversepath p)) \<and>
+                  (path_image p \<subseteq> s \<and> path_image(reversepath p) \<subseteq> s) \<and>
+                  (pathfinish p = pathstart(linepath a a +++ reversepath p) \<and>
+                   pathstart(reversepath p) = a) \<and> pathstart p = x
+                  \<Longrightarrow> 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 \<open>path p\<close> 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)) 
+                                   ((\<lambda>u. h (u, 0)) +++ linepath a a +++ reversepath (\<lambda>u. h (u, 0)))"
+    apply (simp add: homotopic_paths_def homotopic_with_def)
+    apply (rule_tac x="\<lambda>y. (subpath 0 (fst y) (\<lambda>u. h (u, 0)) +++ (\<lambda>u. h (Pair (fst y) u)) +++ subpath (fst y) 0 (\<lambda>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 ((\<lambda>u. h (u, 0)) +++ linepath a a +++ reversepath (\<lambda>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 \<subseteq> s" and piq: "path_image q \<subseteq> 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 \<open>path p\<close> [unfolded path_def] by blast
+  have contq: "continuous_on {0..1} q"  using \<open>path q\<close> [unfolded path_def] by blast
+  have c1: "continuous_on ({0..1} \<times> {0..1}) (\<lambda>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} \<times> {0..1}) (\<lambda>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: "\<And>a b. \<lbrakk>b * 2 \<le> 1; 0 \<le> b; 0 \<le> a; a \<le> 1\<rbrakk> \<Longrightarrow> p ((1 - a) * (2 * b) + a) \<in> 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: "\<And>a b. \<lbrakk>\<not> 4 * b \<le> 3; b \<le> 1; 0 \<le> a; a \<le> 1\<rbrakk> \<Longrightarrow> p ((a - 1) * (4 * b - 3) + 1) \<in> 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: "\<And>a b. \<lbrakk>4 * b \<le> 3; \<not> b * 2 \<le> 1\<rbrakk> \<Longrightarrow> q (4 * b - 2) \<in> 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="(\<lambda>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 \<open>path q\<close> homotopic_paths_lid qloop piq by auto
+    hence 1: "\<And>f. homotopic_paths s f q \<or> \<not> 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: \<open>path q\<close> homotopic_paths_rid piq)
+      thus ?thesis
+        by (metis (no_types) 1 \<open>path q\<close> 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




