Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: symbols_as_interval.pvs Sprache: Isabelle

Original von: Isabelle^©

(*  Title:      HOL/Analysis/Path_Connected.thy
    Authors:    LC Paulson and Robert Himmelmann (TU Muenchen), based on material from HOL Light
*)

section \<open>Homotopy of Maps\<close>

theory Homotopy
  imports Path_Connected Continuum_Not_Denumerable Product_Topology
begin

definition\<^marker>\<open>tag important\<close> homotopic_with
where
"homotopic_with P X Y f g \
   (\<exists>h. continuous_map (prod_topology (top_of_set {0..1::real}) X) Y h \<and>
       (\<forall>x. h(0, x) = f x) \<and>
       (\<forall>x. h(1, x) = g x) \<and>
       (\<forall>t \<in> {0..1}. P(\<lambda>x. h(t,x))))"

text\<open>\<open>p\<close>, \<open>q\<close> are functions \<open>X \<rightarrow> Y\<close>, and the property \<open>P\<close> restricts all intermediate maps.
We often just want to require that \<open>P\<close> fixes some subset, but to include the case of a loop homotopy,
it is convenient to have a general property \<open>P\<close>.\<close>

abbreviation homotopic_with_canon ::
  "[('a::topological_space \ 'b::topological_space) \ bool, 'a set, 'b set, 'a \ 'b, 'a \ 'b] \ bool"
where
"homotopic_with_canon P S T p q \ homotopic_with P (top_of_set S) (top_of_set T) p q"

lemma split_01: "{0..1::real} = {0..1/2} \ {1/2..1}"
  by force

lemma split_01_prod: "{0..1::real} \ X = ({0..1/2} \ X) \ ({1/2..1} \ X)"
  by force

lemma image_Pair_const: "(\x. (x, c)) ` A = A \ {c}"
  by auto

lemma fst_o_paired [simp]: "fst \ (\(x,y). (f x y, g x y)) = (\(x,y). f x y)"
  by auto

lemma snd_o_paired [simp]: "snd \ (\(x,y). (f x y, g x y)) = (\(x,y). g x y)"
  by auto

lemma continuous_on_o_Pair: "\continuous_on (T \ X) h; t \ T\ \ continuous_on X (h \ Pair t)"
  by (fast intro: continuous_intros elim!: continuous_on_subset)

lemma continuous_map_o_Pair:
  assumes h: "continuous_map (prod_topology X Y) Z h" and t: "t \ topspace X"
  shows "continuous_map Y Z (h \ Pair t)"
  by (intro continuous_map_compose [OF _ h] continuous_intros; simp add: t)

subsection\<^marker>\<open>tag unimportant\<close>\<open>Trivial properties\<close>

text \<open>We often want to just localize the ending function equality or whatever.\<close>
text\<^marker>\<open>tag important\<close> \<open>%whitespace\<close>
proposition homotopic_with:
  assumes "\h k. (\x. x \ topspace X \ h x = k x) \ (P h \ P k)"
  shows "homotopic_with P X Y p q \
           (\<exists>h. continuous_map (prod_topology (subtopology euclideanreal {0..1}) X) Y h \<and>
              (\<forall>x \<in> topspace X. h(0,x) = p x) \<and>
              (\<forall>x \<in> topspace X. h(1,x) = q x) \<and>
              (\<forall>t \<in> {0..1}. P(\<lambda>x. h(t, x))))"
  unfolding homotopic_with_def
  apply (rule iffI, blast, clarify)
  apply (rule_tac x="\(u,v). if v \ topspace X then h(u,v) else if u = 0 then p v else q v" in exI)
  apply auto
  using continuous_map_eq apply fastforce
  apply (drule_tac x=t in bspec, force)
  apply (subst assms; simp)
  done

lemma homotopic_with_mono:
  assumes hom: "homotopic_with P X Y f g"
    and Q: "\h. \continuous_map X Y h; P h\ \ Q h"
  shows "homotopic_with Q X Y f g"
  using hom unfolding homotopic_with_def
  by (force simp: o_def dest: continuous_map_o_Pair intro: Q)

lemma homotopic_with_imp_continuous_maps:
    assumes "homotopic_with P X Y f g"
    shows "continuous_map X Y f \ continuous_map X Y g"
proof -
  obtain h :: "real \ 'a \ 'b"
    where conth: "continuous_map (prod_topology (top_of_set {0..1}) X) Y h"
      and h: "\x. h (0, x) = f x" "\x. h (1, x) = g x"
    using assms by (auto simp: homotopic_with_def)
  have *: "t \ {0..1} \ continuous_map X Y (h \ (\x. (t,x)))" for t
    by (rule continuous_map_compose [OF _ conth]) (simp add: o_def continuous_map_pairwise)
  show ?thesis
    using h *[of 0] *[of 1] by (simp add: continuous_map_eq)
qed

lemma homotopic_with_imp_continuous:
    assumes "homotopic_with_canon P X Y f g"
    shows "continuous_on X f \ continuous_on X g"
  by (meson assms continuous_map_subtopology_eu homotopic_with_imp_continuous_maps)

lemma homotopic_with_imp_property:
  assumes "homotopic_with P X Y f g"
  shows "P f \ P g"
proof
  obtain h where h: "\x. h(0, x) = f x" "\x. h(1, x) = g x" and P: "\t. t \ {0..1::real} \ P(\x. h(t,x))"
    using assms by (force simp: homotopic_with_def)
  show "P f" "P g"
    using P [of 0] P [of 1] by (force simp: h)+
qed

lemma homotopic_with_equal:
  assumes "P f" "P g" and contf: "continuous_map X Y f" and fg: "\x. x \ topspace X \ f x = g x"
  shows "homotopic_with P X Y f g"
  unfolding homotopic_with_def
proof (intro exI conjI allI ballI)
  let ?h = "\(t::real,x). if t = 1 then g x else f x"
  show "continuous_map (prod_topology (top_of_set {0..1}) X) Y ?h"
  proof (rule continuous_map_eq)
    show "continuous_map (prod_topology (top_of_set {0..1}) X) Y (f \ snd)"
      by (simp add: contf continuous_map_of_snd)
  qed (auto simp: fg)
  show "P (\x. ?h (t, x))" if "t \ {0..1}" for t
    by (cases "t = 1") (simp_all add: assms)
qed auto

lemma homotopic_with_imp_subset1:
     "homotopic_with_canon P X Y f g \ f ` X \ Y"
  by (simp add: homotopic_with_def image_subset_iff) (metis atLeastAtMost_iff order_refl zero_le_one)

lemma homotopic_with_imp_subset2:
     "homotopic_with_canon P X Y f g \ g ` X \ Y"
  by (simp add: homotopic_with_def image_subset_iff) (metis atLeastAtMost_iff order_refl zero_le_one)

lemma homotopic_with_subset_left:
     "\homotopic_with_canon P X Y f g; Z \ X\ \ homotopic_with_canon P Z Y f g"
  unfolding homotopic_with_def by (auto elim!: continuous_on_subset ex_forward)

lemma homotopic_with_subset_right:
     "\homotopic_with_canon P X Y f g; Y \ Z\ \ homotopic_with_canon P X Z f g"
  unfolding homotopic_with_def by (auto elim!: continuous_on_subset ex_forward)

subsection\<open>Homotopy with P is an equivalence relation\<close>

text \<open>(on continuous functions mapping X into Y that satisfy P, though this only affects reflexivity)\<close>

lemma homotopic_with_refl [simp]: "homotopic_with P X Y f f \ continuous_map X Y f \ P f"
  by (auto simp: homotopic_with_imp_continuous_maps intro: homotopic_with_equal dest: homotopic_with_imp_property)

lemma homotopic_with_symD:
    assumes "homotopic_with P X Y f g"
      shows "homotopic_with P X Y g f"
proof -
  let ?I01 = "subtopology euclideanreal {0..1}"
  let ?j = "\y. (1 - fst y, snd y)"
  have 1: "continuous_map (prod_topology ?I01 X) (prod_topology euclideanreal X) ?j"
    by (intro continuous_intros; simp add: continuous_map_subtopology_fst prod_topology_subtopology)
  have *: "continuous_map (prod_topology ?I01 X) (prod_topology ?I01 X) ?j"
  proof -
    have "continuous_map (prod_topology ?I01 X) (subtopology (prod_topology euclideanreal X) ({0..1} \ topspace X)) ?j"
      by (simp add: continuous_map_into_subtopology [OF 1] image_subset_iff)
    then show ?thesis
      by (simp add: prod_topology_subtopology(1))
  qed
  show ?thesis
    using assms
    apply (clarsimp simp add: homotopic_with_def)
    subgoal for h
      by (rule_tac x="h \ (\y. (1 - fst y, snd y))" in exI) (simp add: continuous_map_compose [OF *])
    done
qed

lemma homotopic_with_sym:
   "homotopic_with P X Y f g \ homotopic_with P X Y g f"
  by (metis homotopic_with_symD)

proposition homotopic_with_trans:
    assumes "homotopic_with P X Y f g"  "homotopic_with P X Y g h"
    shows "homotopic_with P X Y f h"
proof -
  let ?X01 = "prod_topology (subtopology euclideanreal {0..1}) X"
  obtain k1 k2
    where contk1: "continuous_map ?X01 Y k1" and contk2: "continuous_map ?X01 Y k2"
      and k12: "\x. k1 (1, x) = g x" "\x. k2 (0, x) = g x"
      "\x. k1 (0, x) = f x" "\x. k2 (1, x) = h x"
      and P:   "\t\{0..1}. P (\x. k1 (t, x))" "\t\{0..1}. P (\x. k2 (t, x))"
    using assms by (auto simp: homotopic_with_def)
  define k where "k \ \y. if fst y \ 1/2
                             then (k1 \<circ> (\<lambda>x. (2 *\<^sub>R fst x, snd x))) y
                             else (k2 \<circ> (\<lambda>x. (2 *\<^sub>R fst x -1, snd x))) y"
  have keq: "k1 (2 * u, v) = k2 (2 * u -1, v)" if "u = 1/2"  for u v
    by (simp add: k12 that)
  show ?thesis
    unfolding homotopic_with_def
  proof (intro exI conjI)
    show "continuous_map ?X01 Y k"
      unfolding k_def
    proof (rule continuous_map_cases_le)
      show fst: "continuous_map ?X01 euclideanreal fst"
        using continuous_map_fst continuous_map_in_subtopology by blast
      show "continuous_map ?X01 euclideanreal (\x. 1/2)"
        by simp
      show "continuous_map (subtopology ?X01 {y \ topspace ?X01. fst y \ 1/2}) Y
               (k1 \<circ> (\<lambda>x. (2 *\<^sub>R fst x, snd x)))"
        apply (intro fst continuous_map_compose [OF _ contk1] continuous_intros continuous_map_into_subtopology continuous_map_from_subtopology | simp)+
        by (force simp: prod_topology_subtopology)
      show "continuous_map (subtopology ?X01 {y \ topspace ?X01. 1/2 \ fst y}) Y
               (k2 \<circ> (\<lambda>x. (2 *\<^sub>R fst x -1, snd x)))"
        apply (intro fst continuous_map_compose [OF _ contk2] continuous_intros continuous_map_into_subtopology continuous_map_from_subtopology | simp)+
        by (force simp: prod_topology_subtopology)
      show "(k1 \ (\x. (2 *\<^sub>R fst x, snd x))) y = (k2 \ (\x. (2 *\<^sub>R fst x -1, snd x))) y"
        if "y \ topspace ?X01" and "fst y = 1/2" for y
        using that by (simp add: keq)
    qed
    show "\x. k (0, x) = f x"
      by (simp add: k12 k_def)
    show "\x. k (1, x) = h x"
      by (simp add: k12 k_def)
    show "\t\{0..1}. P (\x. k (t, x))"
    proof
      fix t show "t\{0..1} \ P (\x. k (t, x))"
        by (cases "t \ 1/2") (auto simp add: k_def P)
    qed
  qed
qed

lemma homotopic_with_id2:
  "(\x. x \ topspace X \ g (f x) = x) \ homotopic_with (\x. True) X X (g \ f) id"
  by (metis comp_apply continuous_map_id eq_id_iff homotopic_with_equal homotopic_with_symD)

subsection\<open>Continuity lemmas\<close>

lemma homotopic_with_compose_continuous_map_left:
  "\homotopic_with p X1 X2 f g; continuous_map X2 X3 h; \j. p j \ q(h \ j)\
   \<Longrightarrow> homotopic_with q X1 X3 (h \<circ> f) (h \<circ> g)"
  unfolding homotopic_with_def
  apply clarify
  subgoal for k
    by (rule_tac x="h \ k" in exI) (rule conjI continuous_map_compose | simp add: o_def)+
  done

lemma homotopic_with_compose_continuous_map_right:
  assumes hom: "homotopic_with p X2 X3 f g" and conth: "continuous_map X1 X2 h"
    and q: "\j. p j \ q(j \ h)"
  shows "homotopic_with q X1 X3 (f \ h) (g \ h)"
proof -
  obtain k
    where contk: "continuous_map (prod_topology (subtopology euclideanreal {0..1}) X2) X3 k"
      and k: "\x. k (0, x) = f x" "\x. k (1, x) = g x" and p: "\t. t\{0..1} \ p (\x. k (t, x))"
    using hom unfolding homotopic_with_def by blast
  have hsnd: "continuous_map (prod_topology (subtopology euclideanreal {0..1}) X1) X2 (h \ snd)"
    by (rule continuous_map_compose [OF continuous_map_snd conth])
  let ?h = "k \ (\(t,x). (t,h x))"
  show ?thesis
    unfolding homotopic_with_def
  proof (intro exI conjI allI ballI)
    have "continuous_map (prod_topology (top_of_set {0..1}) X1)
     (prod_topology (top_of_set {0..1::real}) X2) (\<lambda>(t, x). (t, h x))"
      by (metis (mono_tags, lifting) case_prod_beta' comp_def continuous_map_eq continuous_map_fst continuous_map_pairedI hsnd)
    then show "continuous_map (prod_topology (subtopology euclideanreal {0..1}) X1) X3 ?h"
      by (intro conjI continuous_map_compose [OF _ contk])
    show "q (\x. ?h (t, x))" if "t \ {0..1}" for t
      using q [OF p [OF that]] by (simp add: o_def)
  qed (auto simp: k)
qed

corollary homotopic_compose:
  assumes "homotopic_with (\x. True) X Y f f'" "homotopic_with (\x. True) Y Z g g'"
  shows "homotopic_with (\x. True) X Z (g \ f) (g' \ f')"
proof (rule homotopic_with_trans [where g = "g \ f'"])
  show "homotopic_with (\x. True) X Z (g \ f) (g \ f')"
    using assms by (simp add: homotopic_with_compose_continuous_map_left homotopic_with_imp_continuous_maps)
  show "homotopic_with (\x. True) X Z (g \ f') (g' \ f')"
    using assms by (simp add: homotopic_with_compose_continuous_map_right homotopic_with_imp_continuous_maps)
qed

proposition homotopic_with_compose_continuous_right:
    "\homotopic_with_canon (\f. p (f \ h)) X Y f g; continuous_on W h; h ` W \ X\
     \<Longrightarrow> homotopic_with_canon p W Y (f \<circ> h) (g \<circ> h)"
  apply (clarsimp simp add: homotopic_with_def)
  subgoal for k
    apply (rule_tac x="k \ (\y. (fst y, h (snd y)))" in exI)
    by (intro conjI continuous_intros continuous_on_compose2 [where f=snd and g=h]; fastforce simp: o_def elim: continuous_on_subset)
  done

proposition homotopic_with_compose_continuous_left:
     "\homotopic_with_canon (\f. p (h \ f)) X Y f g; continuous_on Y h; h ` Y \ Z\
      \<Longrightarrow> homotopic_with_canon p X Z (h \<circ> f) (h \<circ> g)"
  apply (clarsimp simp add: homotopic_with_def)
  subgoal for k
  apply (rule_tac x="h \ k" in exI)
    by (intro conjI continuous_intros continuous_on_compose [where f=snd and g=h, unfolded o_def]; fastforce simp: o_def elim: continuous_on_subset)
  done

lemma homotopic_from_subtopology:
   "homotopic_with P X X' f g \ homotopic_with P (subtopology X s) X' f g"
  unfolding homotopic_with_def
  by (force simp add: continuous_map_from_subtopology prod_topology_subtopology(2) elim!: ex_forward)

lemma homotopic_on_emptyI:
    assumes "topspace X = {}" "P f" "P g"
    shows "homotopic_with P X X' f g"
  unfolding homotopic_with_def
proof (intro exI conjI ballI)
  show "P (\x. (\(t,x). if t = 0 then f x else g x) (t, x))" if "t \ {0..1}" for t::real
    by (cases "t = 0", auto simp: assms)
qed (auto simp: continuous_map_atin assms)

lemma homotopic_on_empty:
   "topspace X = {} \ (homotopic_with P X X' f g \ P f \ P g)"
  using homotopic_on_emptyI homotopic_with_imp_property by metis

lemma homotopic_with_canon_on_empty [simp]: "homotopic_with_canon (\x. True) {} t f g"
  by (auto intro: homotopic_with_equal)

lemma homotopic_constant_maps:
   "homotopic_with (\x. True) X X' (\x. a) (\x. b) \
    topspace X = {} \<or> path_component_of X' a b" (is "?lhs = ?rhs")
proof (cases "topspace X = {}")
  case False
  then obtain c where c: "c \ topspace X"
    by blast
  have "\g. continuous_map (top_of_set {0..1::real}) X' g \ g 0 = a \ g 1 = b"
    if "x \ topspace X" and hom: "homotopic_with (\x. True) X X' (\x. a) (\x. b)" for x
  proof -
    obtain h :: "real \ 'a \ 'b"
      where conth: "continuous_map (prod_topology (top_of_set {0..1}) X) X' h"
        and h: "\x. h (0, x) = a" "\x. h (1, x) = b"
      using hom by (auto simp: homotopic_with_def)
    have cont: "continuous_map (top_of_set {0..1}) X' (h \ (\t. (t, c)))"
      by (rule continuous_map_compose [OF _ conth] continuous_intros c | simp)+
    then show ?thesis
      by (force simp: h)
  qed
  moreover have "homotopic_with (\x. True) X X' (\x. g 0) (\x. g 1)"
    if "x \ topspace X" "a = g 0" "b = g 1" "continuous_map (top_of_set {0..1}) X' g"
    for x and g :: "real \ 'b"
    unfolding homotopic_with_def
    by (force intro!: continuous_map_compose continuous_intros c that)
  ultimately show ?thesis
    using False by (auto simp: path_component_of_def pathin_def)
qed (simp add: homotopic_on_empty)

proposition homotopic_with_eq:
   assumes h: "homotopic_with P X Y f g"
       and f': "\x. x \ topspace X \ f' x = f x"
       and g': "\x. x \ topspace X \ g' x = g x"
       and P:  "(\h k. (\x. x \ topspace X \ h x = k x) \ P h \ P k)"
   shows "homotopic_with P X Y f' g'"
  using h unfolding homotopic_with_def
  apply clarify
  subgoal for h
    apply (rule_tac x="\(u,v). if v \ topspace X then h(u,v) else if u = 0 then f' v else g' v" in exI)
    apply (simp add: f' g', safe)
     apply (fastforce intro: continuous_map_eq)
    apply (subst P; fastforce)
    done
  done

lemma homotopic_with_prod_topology:
  assumes "homotopic_with p X1 Y1 f f'" and "homotopic_with q X2 Y2 g g'"
    and r: "\i j. \p i; q j\ \ r(\(x,y). (i x, j y))"
  shows "homotopic_with r (prod_topology X1 X2) (prod_topology Y1 Y2)
                          (\<lambda>z. (f(fst z),g(snd z))) (\<lambda>z. (f'(fst z), g'(snd z)))"
proof -
  obtain h
    where h: "continuous_map (prod_topology (subtopology euclideanreal {0..1}) X1) Y1 h"
      and h0: "\x. h (0, x) = f x"
      and h1: "\x. h (1, x) = f' x"
      and p: "\t. \0 \ t; t \ 1\ \ p (\x. h (t,x))"
    using assms unfolding homotopic_with_def by auto
  obtain k
    where k: "continuous_map (prod_topology (subtopology euclideanreal {0..1}) X2) Y2 k"
      and k0: "\x. k (0, x) = g x"
      and k1: "\x. k (1, x) = g' x"
      and q: "\t. \0 \ t; t \ 1\ \ q (\x. k (t,x))"
    using assms unfolding homotopic_with_def by auto
  let ?hk = "\(t,x,y). (h(t,x), k(t,y))"
  show ?thesis
    unfolding homotopic_with_def
  proof (intro conjI allI exI)
    show "continuous_map (prod_topology (subtopology euclideanreal {0..1}) (prod_topology X1 X2))
                         (prod_topology Y1 Y2) ?hk"
      unfolding continuous_map_pairwise case_prod_unfold
      by (rule conjI continuous_map_pairedI continuous_intros continuous_map_id [unfolded id_def]
          continuous_map_fst_of [unfolded o_def] continuous_map_snd_of [unfolded o_def]
          continuous_map_compose [OF _ h, unfolded o_def]
          continuous_map_compose [OF _ k, unfolded o_def])+
  next
    fix x
    show "?hk (0, x) = (f (fst x), g (snd x))" "?hk (1, x) = (f' (fst x), g' (snd x))"
      by (auto simp: case_prod_beta h0 k0 h1 k1)
  qed (auto simp: p q r)
qed

lemma homotopic_with_product_topology:
  assumes ht: "\i. i \ I \ homotopic_with (p i) (X i) (Y i) (f i) (g i)"
    and pq: "\h. (\i. i \ I \ p i (h i)) \ q(\x. (\i\I. h i (x i)))"
  shows "homotopic_with q (product_topology X I) (product_topology Y I)
                          (\<lambda>z. (\<lambda>i\<in>I. (f i) (z i))) (\<lambda>z. (\<lambda>i\<in>I. (g i) (z i)))"
proof -
  obtain h
    where h: "\i. i \ I \ continuous_map (prod_topology (subtopology euclideanreal {0..1}) (X i)) (Y i) (h i)"
      and h0: "\i x. i \ I \ h i (0, x) = f i x"
      and h1: "\i x. i \ I \ h i (1, x) = g i x"
      and p: "\i t. \i \ I; t \ {0..1}\ \ p i (\x. h i (t,x))"
    using ht unfolding homotopic_with_def by metis
  show ?thesis
    unfolding homotopic_with_def
  proof (intro conjI allI exI)
    let ?h = "\(t,z). \i\I. h i (t,z i)"
    have "continuous_map (prod_topology (subtopology euclideanreal {0..1}) (product_topology X I))
                         (Y i) (\<lambda>x. h i (fst x, snd x i))" if "i \<in> I" for i
    proof -
      have \<section>: "continuous_map (prod_topology (top_of_set {0..1}) (product_topology X I)) (X i) (\<lambda>x. snd x i)"
        using continuous_map_componentwise continuous_map_snd that by fastforce
      show ?thesis
        unfolding continuous_map_pairwise case_prod_unfold
        by (intro conjI that \<section> continuous_intros continuous_map_compose [OF _ h, unfolded o_def])
    qed
    then show "continuous_map (prod_topology (subtopology euclideanreal {0..1}) (product_topology X I))
         (product_topology Y I) ?h"
      by (auto simp: continuous_map_componentwise case_prod_beta)
    show "?h (0, x) = (\i\I. f i (x i))" "?h (1, x) = (\i\I. g i (x i))" for x
      by (auto simp: case_prod_beta h0 h1)
    show "\t\{0..1}. q (\x. ?h (t, x))"
      by (force intro: p pq)
  qed
qed

text\<open>Homotopic triviality implicitly incorporates path-connectedness.\<close>
lemma homotopic_triviality:
  shows  "(\f g. continuous_on S f \ f ` S \ T \
                 continuous_on S g \<and> g ` S \<subseteq> T
                 \<longrightarrow> homotopic_with_canon (\<lambda>x. True) S T f g) \<longleftrightarrow>
          (S = {} \<or> path_connected T) \<and>
          (\<forall>f. continuous_on S f \<and> f ` S \<subseteq> T \<longrightarrow> (\<exists>c. homotopic_with_canon (\<lambda>x. True) S T f (\<lambda>x. c)))"
          (is "?lhs = ?rhs")
proof (cases "S = {} \ T = {}")
  case True then show ?thesis
    by (auto simp: homotopic_on_emptyI)
next
  case False show ?thesis
  proof
    assume LHS [rule_format]: ?lhs
    have pab: "path_component T a b" if "a \ T" "b \ T" for a b
    proof -
      have "homotopic_with_canon (\x. True) S T (\x. a) (\x. b)"
        by (simp add: LHS image_subset_iff that)
      then show ?thesis
        using False homotopic_constant_maps [of "top_of_set S" "top_of_set T" a b] by auto
    qed
    moreover
    have "\c. homotopic_with_canon (\x. True) S T f (\x. c)" if "continuous_on S f" "f ` S \ T" for f
      using False LHS continuous_on_const that by blast
    ultimately show ?rhs
      by (simp add: path_connected_component)
  next
    assume RHS: ?rhs
    with False have T: "path_connected T"
      by blast
    show ?lhs
    proof clarify
      fix f g
      assume "continuous_on S f" "f ` S \ T" "continuous_on S g" "g ` S \ T"
      obtain c d where c: "homotopic_with_canon (\x. True) S T f (\x. c)" and d: "homotopic_with_canon (\x. True) S T g (\x. d)"
        using False \<open>continuous_on S f\<close> \<open>f ` S \<subseteq> T\<close>  RHS \<open>continuous_on S g\<close> \<open>g ` S \<subseteq> T\<close> by blast
      then have "c \ T" "d \ T"
        using False homotopic_with_imp_continuous_maps by fastforce+
      with T have "path_component T c d"
        using path_connected_component by blast
      then have "homotopic_with_canon (\x. True) S T (\x. c) (\x. d)"
        by (simp add: homotopic_constant_maps)
      with c d show "homotopic_with_canon (\x. True) S T f g"
        by (meson homotopic_with_symD homotopic_with_trans)
    qed
  qed
qed

subsection\<open>Homotopy of paths, maintaining the same endpoints\<close>

definition\<^marker>\<open>tag important\<close> homotopic_paths :: "['a set, real \<Rightarrow> 'a, real \<Rightarrow> 'a::topological_space] \<Rightarrow> bool"
  where
     "homotopic_paths s p q \
       homotopic_with_canon (\<lambda>r. pathstart r = pathstart p \<and> pathfinish r = pathfinish p) {0..1} s p q"

lemma homotopic_paths:
   "homotopic_paths s p q \
      (\<exists>h. continuous_on ({0..1} \<times> {0..1}) h \<and>
          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::real}. pathstart(h \<circ> Pair t) = pathstart p \<and>
                        pathfinish(h \<circ> Pair t) = pathfinish p))"
  by (auto simp: homotopic_paths_def homotopic_with pathstart_def pathfinish_def)

proposition homotopic_paths_imp_pathstart:
     "homotopic_paths s p q \ pathstart p = pathstart q"
  by (metis (mono_tags, lifting) homotopic_paths_def homotopic_with_imp_property)

proposition homotopic_paths_imp_pathfinish:
     "homotopic_paths s p q \ pathfinish p = pathfinish q"
  by (metis (mono_tags, lifting) homotopic_paths_def homotopic_with_imp_property)

lemma homotopic_paths_imp_path:
     "homotopic_paths s p q \ path p \ path q"
  using homotopic_paths_def homotopic_with_imp_continuous_maps path_def continuous_map_subtopology_eu by blast

lemma homotopic_paths_imp_subset:
     "homotopic_paths s p q \ path_image p \ s \ path_image q \ s"
  by (metis (mono_tags) continuous_map_subtopology_eu homotopic_paths_def homotopic_with_imp_continuous_maps path_image_def)

proposition homotopic_paths_refl [simp]: "homotopic_paths s p p \ path p \ path_image p \ s"
  by (simp add: homotopic_paths_def path_def path_image_def)

proposition homotopic_paths_sym: "homotopic_paths s p q \ homotopic_paths s q p"
  by (metis (mono_tags) homotopic_paths_def homotopic_paths_imp_pathfinish homotopic_paths_imp_pathstart homotopic_with_symD)

proposition homotopic_paths_sym_eq: "homotopic_paths s p q \ homotopic_paths s q p"
  by (metis homotopic_paths_sym)

proposition homotopic_paths_trans [trans]:
  assumes "homotopic_paths s p q" "homotopic_paths s q r"
  shows "homotopic_paths s p r"
proof -
  have "pathstart q = pathstart p" "pathfinish q = pathfinish p"
    using assms by (simp_all add: homotopic_paths_imp_pathstart homotopic_paths_imp_pathfinish)
  then have "homotopic_with_canon (\f. pathstart f = pathstart p \ pathfinish f = pathfinish p) {0..1} s q r"
    using \<open>homotopic_paths s q r\<close> homotopic_paths_def by force
  then show ?thesis
    using assms homotopic_paths_def homotopic_with_trans by blast
qed

proposition homotopic_paths_eq:
     "\path p; path_image p \ s; \t. t \ {0..1} \ p t = q t\ \ homotopic_paths s p q"
  unfolding homotopic_paths_def
  by (rule homotopic_with_eq)
     (auto simp: path_def pathstart_def pathfinish_def path_image_def elim: continuous_on_eq)

proposition homotopic_paths_reparametrize:
  assumes "path p"
      and pips: "path_image p \ s"
      and contf: "continuous_on {0..1} f"
      and f01:"f ` {0..1} \ {0..1}"
      and [simp]: "f(0) = 0" "f(1) = 1"
      and q: "\t. t \ {0..1} \ q(t) = p(f t)"
    shows "homotopic_paths s p q"
proof -
  have contp: "continuous_on {0..1} p"
    by (metis \<open>path p\<close> path_def)
  then have "continuous_on {0..1} (p \ f)"
    using contf continuous_on_compose continuous_on_subset f01 by blast
  then have "path q"
    by (simp add: path_def) (metis q continuous_on_cong)
  have piqs: "path_image q \ s"
    by (metis (no_types, hide_lams) pips f01 image_subset_iff path_image_def q)
  have fb0: "\a b. \0 \ a; a \ 1; 0 \ b; b \ 1\ \ 0 \ (1 - a) * f b + a * b"
    using f01 by force
  have fb1: "\0 \ a; a \ 1; 0 \ b; b \ 1\ \ (1 - a) * f b + a * b \ 1" for a b
    using f01 [THEN subsetD, of "f b"] by (simp add: convex_bound_le)
  have "homotopic_paths s q p"
  proof (rule homotopic_paths_trans)
    show "homotopic_paths s q (p \ f)"
      using q by (force intro: homotopic_paths_eq [OF  \<open>path q\<close> piqs])
  next
    show "homotopic_paths s (p \ f) p"
      using pips [unfolded path_image_def]
      apply (simp add: homotopic_paths_def homotopic_with_def)
      apply (rule_tac x="p \ (\y. (1 - (fst y)) *\<^sub>R ((f \ snd) y) + (fst y) *\<^sub>R snd y)" in exI)
      apply (rule conjI contf continuous_intros continuous_on_subset [OF contp] | simp)+
      by (auto simp: fb0 fb1 pathstart_def pathfinish_def)
  qed
  then show ?thesis
    by (simp add: homotopic_paths_sym)
qed

lemma homotopic_paths_subset: "\homotopic_paths s p q; s \ t\ \ homotopic_paths t p q"
  unfolding homotopic_paths by fast

text\<open> A slightly ad-hoc but useful lemma in constructing homotopies.\<close>
lemma continuous_on_homotopic_join_lemma:
  fixes q :: "[real,real] \ 'a::topological_space"
  assumes p: "continuous_on ({0..1} \ {0..1}) (\y. p (fst y) (snd y))" (is "continuous_on ?A ?p")
      and q: "continuous_on ({0..1} \ {0..1}) (\y. q (fst y) (snd y))" (is "continuous_on ?A ?q")
      and pf: "\t. t \ {0..1} \ pathfinish(p t) = pathstart(q t)"
    shows "continuous_on ({0..1} \ {0..1}) (\y. (p(fst y) +++ q(fst y)) (snd y))"
proof -
  have \<section>: "(\<lambda>t. p (fst t) (2 * snd t)) = ?p \<circ> (\<lambda>y. (fst y, 2 * snd y))"
          "(\t. q (fst t) (2 * snd t - 1)) = ?q \ (\y. (fst y, 2 * snd y - 1))"
    by force+
  show ?thesis
    unfolding joinpaths_def
  proof (rule continuous_on_cases_le)
    show "continuous_on {y \ ?A. snd y \ 1/2} (\t. p (fst t) (2 * snd t))"
         "continuous_on {y \ ?A. 1/2 \ snd y} (\t. q (fst t) (2 * snd t - 1))"
         "continuous_on ?A snd"
      unfolding \<section>
      by (rule continuous_intros continuous_on_subset [OF p] continuous_on_subset [OF q] | force)+
  qed (use pf in \<open>auto simp: mult.commute pathstart_def pathfinish_def\<close>)
qed

text\<open> Congruence properties of homotopy w.r.t. path-combining operations.\<close>

lemma homotopic_paths_reversepath_D:
      assumes "homotopic_paths s p q"
      shows   "homotopic_paths s (reversepath p) (reversepath q)"
  using assms
  apply (simp add: homotopic_paths_def homotopic_with_def, clarify)
  apply (rule_tac x="h \ (\x. (fst x, 1 - snd x))" in exI)
  apply (rule conjI continuous_intros)+
  apply (auto simp: reversepath_def pathstart_def pathfinish_def elim!: continuous_on_subset)
  done

proposition homotopic_paths_reversepath:
     "homotopic_paths s (reversepath p) (reversepath q) \ homotopic_paths s p q"
  using homotopic_paths_reversepath_D by force

proposition homotopic_paths_join:
    "\homotopic_paths s p p'; homotopic_paths s q q'; pathfinish p = pathstart q\ \ homotopic_paths s (p +++ q) (p' +++ q')"
  apply (clarsimp simp add: homotopic_paths_def homotopic_with_def)
  apply (rename_tac k1 k2)
  apply (rule_tac x="(\y. ((k1 \ Pair (fst y)) +++ (k2 \ Pair (fst y))) (snd y))" in exI)
  apply (intro conjI continuous_intros continuous_on_homotopic_join_lemma; force simp: joinpaths_def pathstart_def pathfinish_def path_image_def)
  done

proposition homotopic_paths_continuous_image:
    "\homotopic_paths s f g; continuous_on s h; h ` s \ t\ \ homotopic_paths t (h \ f) (h \ g)"
  unfolding homotopic_paths_def
  by (simp add: homotopic_with_compose_continuous_map_left pathfinish_compose pathstart_compose)

subsection\<open>Group properties for homotopy of paths\<close>

text\<^marker>\<open>tag important\<close>\<open>So taking equivalence classes under homotopy would give the fundamental group\<close>

proposition homotopic_paths_rid:
  assumes "path p" "path_image p \ s"
  shows "homotopic_paths s (p +++ linepath (pathfinish p) (pathfinish p)) p"
proof -
  have \<section>: "continuous_on {0..1} (\<lambda>t::real. if t \<le> 1/2 then 2 *\<^sub>R t else 1)"
    unfolding split_01
    by (rule continuous_on_cases continuous_intros | force simp: pathfinish_def joinpaths_def)+
  show ?thesis
    apply (rule homotopic_paths_sym)
    using assms unfolding pathfinish_def joinpaths_def
    by (intro \<section> continuous_on_cases continuous_intros homotopic_paths_reparametrize [where f = "\<lambda>t. if t \<le> 1/2 then 2 *\<^sub>R t else 1"]; force)
qed

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\<rbrakk>
    \<Longrightarrow> 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 \<le> 3 / 4 then t - (1 / 4)
                           else 2 *\<^sub>R t - 1"])
  apply (simp_all del: le_divide_eq_numeral1 add: subset_path_image_join)
  apply (rule continuous_on_cases_1 continuous_intros | 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 p: "continuous_on {0..1} p"
    using assms by (auto simp: path_def)
  let ?A = "{0..1} \ {0..1}"
  have "continuous_on ?A (\x. (subpath 0 (fst x) p +++ reversepath (subpath 0 (fst x) p)) (snd x))"
    unfolding joinpaths_def subpath_def reversepath_def path_def add_0_right diff_0_right
  proof (rule continuous_on_cases_le)
    show "continuous_on {x \ ?A. snd x \ 1/2} (\t. p (fst t * (2 * snd t)))"
         "continuous_on {x \ ?A. 1/2 \ snd x} (\t. p (fst t * (1 - (2 * snd t - 1))))"
         "continuous_on ?A snd"
      by (intro continuous_on_compose2 [OF p] continuous_intros; auto simp add: mult_le_one)+
  qed (auto simp add: algebra_simps)
  then show ?thesis
    using assms
    apply (subst homotopic_paths_sym_eq)
    unfolding 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 (force simp: mult_le_one path_defs joinpaths_def subpath_def reversepath_def)
    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\<open>Homotopy of loops without requiring preservation of endpoints\<close>

definition\<^marker>\<open>tag important\<close> homotopic_loops :: "'a::topological_space set \<Rightarrow> (real \<Rightarrow> 'a) \<Rightarrow> (real \<Rightarrow> 'a) \<Rightarrow> bool"  where
"homotopic_loops s p q \
     homotopic_with_canon (\<lambda>r. pathfinish r = pathstart r) {0..1} s p q"

lemma homotopic_loops:
   "homotopic_loops s p q \
      (\<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 \<circ> Pair t) = pathstart(h \<circ> 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_maps continuous_map_subtopology_eu by blast

proposition homotopic_loops_imp_subset:
     "homotopic_loops s p q \ path_image p \ s \ path_image q \ s"
  unfolding homotopic_loops_def path_image_def
  by (meson continuous_map_subtopology_eu homotopic_with_imp_continuous_maps)

proposition homotopic_loops_refl:
     "homotopic_loops s p p \
      path p \<and> path_image p \<subseteq> s \<and> pathfinish p = pathstart p"
  by (simp add: homotopic_loops_def 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_sym_eq: "homotopic_loops s p q \ homotopic_loops s q p"
  by (metis homotopic_loops_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 (fastforce simp add: homotopic_loops)

proposition homotopic_loops_eq:
   "\path p; path_image p \ s; pathfinish p = pathstart p; \t. t \ {0..1} \ p(t) = q(t)\
          \<Longrightarrow> homotopic_loops s p q"
  unfolding homotopic_loops_def path_image_def path_def pathstart_def pathfinish_def
  by (auto intro: homotopic_with_eq [OF homotopic_with_refl [where f = p, THEN iffD2]])

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
  by (simp add: homotopic_with_compose_continuous_map_left pathfinish_def pathstart_def)

subsection\<open>Relations between the two variants of homotopy\<close>

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_with_def homotopic_paths_def homotopic_loops_def)

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_subset)
  let ?A = "{0..1::real} \ {0..1::real}"
  obtain h where conth: "continuous_on ?A h"
             and hs: "h ` ?A \ 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
  proof (rule continuous_on_compose [of _ _ h, unfolded o_def])
    show "continuous_on ((\x. (x, 0)) ` {0..1}) h"
      by (force intro: continuous_on_subset [OF conth])
  qed (force intro: continuous_intros)
  have pih0: "path_image (\u. h (u, 0)) \ s"
    using hs by (force simp: path_image_def)
  have c1: "continuous_on ?A (\x. h (fst x * snd x, 0))"
  proof (rule continuous_on_compose [of _ _ h, unfolded o_def])
    show "continuous_on ((\x. (fst x * snd x, 0)) ` ?A) h"
      by (force simp: mult_le_one intro: continuous_on_subset [OF conth])
  qed (force intro: continuous_intros)+
  have c2: "continuous_on ?A (\x. h (fst x - fst x * snd x, 0))"
  proof (rule continuous_on_compose [of _ _ h, unfolded o_def])
    show "continuous_on ((\x. (fst x - fst x * snd x, 0)) ` ?A) h"
      by (auto simp: algebra_simps add_increasing2 mult_left_le intro: continuous_on_subset [OF conth])
  qed (force intro: continuous_intros)
  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 \<open>c \<le> 1\<close> show ?thesis by fastforce
  qed
  have *: "\p x. \path p \ path(reversepath p);
                  path_image p \<subseteq> s \<and> path_image(reversepath p) \<subseteq> s;
                  pathfinish p = pathstart(linepath a a +++ reversepath p) \<and>
                   pathstart(reversepath p) = a \<and> pathstart p = x\<rbrakk>
                  \<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 (rule 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)))"
    unfolding homotopic_paths_def homotopic_with_def
  proof (intro exI strip conjI)
    let ?h = "\y. (subpath 0 (fst y) (\u. h (u, 0)) +++ (\u. h (Pair (fst y) u))
               +++ subpath (fst y) 0 (\<lambda>u. h (u, 0))) (snd y)"
    have "continuous_on ?A ?h"
      by (intro continuous_on_homotopic_join_lemma; simp add: path_defs joinpaths_def subpath_def conth c1 c2)
    moreover have "?h ` ?A \ s"
      unfolding joinpaths_def subpath_def
      by (force simp: algebra_simps mult_le_one mult_left_le intro: hs [THEN subsetD] adhoc_le)
  ultimately show "continuous_map (prod_topology (top_of_set {0..1}) (top_of_set {0..1}))
                         (top_of_set s) ?h"
    by (simp add: subpath_reversepath)
  qed (use ploop in \<open>simp_all add: reversepath_def path_defs joinpaths_def o_def subpath_def conth c1 c2\<close>)
  moreover have "homotopic_paths s ((\u. h (u, 0)) +++ linepath a a +++ reversepath (\u. h (u, 0)))
                                   (linepath (pathstart p) (pathstart p))"
  proof (rule *; simp add: pih0 pathstart_def pathfinish_def conth0)
    show "a = (linepath a a +++ reversepath (\u. h (u, 0))) 0 \ reversepath (\u. h (u, 0)) 0 = a"
      by (simp_all add: reversepath_def joinpaths_def)
  qed
  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 pq: "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
  let ?A = "{0..1::real} \ {0..1::real}"
  have c1: "continuous_on ?A (\x. p ((1 - fst x) * snd x + fst x))"
  proof (rule continuous_on_compose [of _ _ p, unfolded o_def])
    show "continuous_on ((\x. (1 - fst x) * snd x + fst x) ` ?A) p"
      by (auto intro: continuous_on_subset [OF contp] simp: algebra_simps add_increasing2 mult_right_le_one_le sum_le_prod1)
  qed (force intro: continuous_intros)
  have c2: "continuous_on ?A (\x. p ((fst x - 1) * snd x + 1))"
  proof (rule continuous_on_compose [of _ _ p, unfolded o_def])
    show "continuous_on ((\x. (fst x - 1) * snd x + 1) ` ?A) p"
      by (auto intro: continuous_on_subset [OF contp] simp: algebra_simps add_increasing2 mult_left_le_one_le)
  qed (force intro: continuous_intros)

  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
              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))"
    unfolding homotopic_loops_def homotopic_with_def
  proof (intro exI strip conjI)
    let ?h = "(\y. (subpath (fst y) 1 p +++ q +++ subpath 1 (fst y) p) (snd y))"
    have "continuous_on ?A (\y. q (snd y))"
      by (force simp: contq intro: continuous_on_compose [of _ _ q, unfolded o_def] continuous_on_id continuous_on_snd)
    then have "continuous_on ?A ?h"
      using pq qloop
      by (intro continuous_on_homotopic_join_lemma) (auto simp: path_defs joinpaths_def subpath_def c1 c2)
    then show "continuous_map (prod_topology (top_of_set {0..1}) (top_of_set {0..1})) (top_of_set s) ?h"
      by (auto simp: joinpaths_def subpath_def  ps1 ps2 qs)
    show "?h (1,x) = (linepath (pathstart q) (pathstart q) +++ q +++ linepath (pathstart q) (pathstart q)) x"  for x
      using pq by (simp add: pathfinish_def subpath_refl)
  qed (auto simp: subpath_reversepath)
  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: "\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: \<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

lemma homotopic_paths_loop_parts:
  assumes loops: "homotopic_loops S (p +++ reversepath q) (linepath a a)" and "path q"
  shows "homotopic_paths S p q"
proof -
  have paths: "homotopic_paths S (p +++ reversepath q) (linepath (pathstart p) (pathstart p))"
    using homotopic_loops_imp_homotopic_paths_null [OF loops] by simp
  then have "path p"
    using \<open>path q\<close> homotopic_loops_imp_path loops path_join path_join_path_ends path_reversepath by blast
  show ?thesis
  proof (cases "pathfinish p = pathfinish q")
    case True
    have pipq: "path_image p \ S" "path_image q \ S"
      by (metis Un_subset_iff paths \<open>path p\<close> \<open>path q\<close> homotopic_loops_imp_subset homotopic_paths_imp_path loops
           path_image_join path_image_reversepath path_imp_reversepath path_join_eq)+
    have "homotopic_paths S p (p +++ (linepath (pathfinish p) (pathfinish p)))"
      using \<open>path p\<close> \<open>path_image p \<subseteq> S\<close> homotopic_paths_rid homotopic_paths_sym by blast
    moreover have "homotopic_paths S (p +++ (linepath (pathfinish p) (pathfinish p))) (p +++ (reversepath q +++ q))"
      by (simp add: True \<open>path p\<close> \<open>path q\<close> pipq homotopic_paths_join homotopic_paths_linv homotopic_paths_sym)
    moreover have "homotopic_paths S (p +++ (reversepath q +++ q)) ((p +++ reversepath q) +++ q)"
      by (simp add: True \<open>path p\<close> \<open>path q\<close> homotopic_paths_assoc pipq)
    moreover have "homotopic_paths S ((p +++ reversepath q) +++ q) (linepath (pathstart p) (pathstart p) +++ q)"
      by (simp add: \<open>path q\<close> homotopic_paths_join paths pipq)
    moreover then have "homotopic_paths S (linepath (pathstart p) (pathstart p) +++ q) q"
      by (metis \<open>path q\<close> homotopic_paths_imp_path homotopic_paths_lid linepath_trivial path_join_path_ends pathfinish_def pipq(2))
    ultimately show ?thesis
      using homotopic_paths_trans by metis
  next
    case False
    then show ?thesis
      using \<open>path q\<close> homotopic_loops_imp_path loops path_join_path_ends by fastforce
  qed
qed

subsection\<^marker>\<open>tag unimportant\<close>\<open>Homotopy of "nearby" function, paths and loops\<close>

lemma homotopic_with_linear:
  fixes f g :: "_ \ 'b::real_normed_vector"
  assumes contf: "continuous_on S f"
      and contg:"continuous_on S g"
      and sub: "\x. x \ S \ closed_segment (f x) (g x) \ t"
    shows "homotopic_with_canon (\z. True) S t f g"
  unfolding homotopic_with_def
  apply (rule_tac x="\y. ((1 - (fst y)) *\<^sub>R f(snd y) + (fst y) *\<^sub>R g(snd y))" in exI)
  using sub closed_segment_def
     by (fastforce intro: continuous_intros continuous_on_subset [OF contf] continuous_on_compose2 [where g=f]
            continuous_on_subset [OF contg] continuous_on_compose2 [where g=g])

lemma homotopic_paths_linear:
  fixes g h :: "real \ 'a::real_normed_vector"
  assumes "path g" "path h" "pathstart h = pathstart g" "pathfinish h = pathfinish g"
          "\t. t \ {0..1} \ closed_segment (g t) (h t) \ S"
    shows "homotopic_paths S g h"
  using assms
  unfolding path_def
  apply (simp add: closed_segment_def pathstart_def pathfinish_def homotopic_paths_def homotopic_with_def)
  apply (rule_tac x="\y. ((1 - (fst y)) *\<^sub>R (g \ snd) y + (fst y) *\<^sub>R (h \ snd) y)" in exI)
  apply (intro conjI subsetI continuous_intros; force)
  done

lemma homotopic_loops_linear:
  fixes g h :: "real \ 'a::real_normed_vector"
  assumes "path g" "path h" "pathfinish g = pathstart g" "pathfinish h = pathstart h"
          "\t x. t \ {0..1} \ closed_segment (g t) (h t) \ S"
    shows "homotopic_loops S g h"
  using assms
  unfolding path_defs homotopic_loops_def homotopic_with_def
  apply (rule_tac x="\y. ((1 - (fst y)) *\<^sub>R g(snd y) + (fst y) *\<^sub>R h(snd y))" in exI)
  by (force simp: closed_segment_def intro!: continuous_intros intro: continuous_on_compose2 [where g=g] continuous_on_compose2 [where g=h])

lemma homotopic_paths_nearby_explicit:
  assumes \<section>: "path g" "path h" "pathstart h = pathstart g" "pathfinish h = pathfinish g"
      and no: "\t x. \t \ {0..1}; x \ S\ \ norm(h t - g t) < norm(g t - x)"
    shows "homotopic_paths S g h"
proof (rule homotopic_paths_linear [OF \<section>])
  show "\t. t \ {0..1} \ closed_segment (g t) (h t) \ S"
  by (metis no segment_bound(1) subsetI norm_minus_commute not_le)
qed

lemma homotopic_loops_nearby_explicit:
  assumes \<section>: "path g" "path h" "pathfinish g = pathstart g" "pathfinish h = pathstart h"
      and no: "\t x. \t \ {0..1}; x \ S\ \ norm(h t - g t) < norm(g t - x)"
    shows "homotopic_loops S g h"
proof (rule homotopic_loops_linear [OF \<section>])
  show "\t. t \ {0..1} \ closed_segment (g t) (h t) \ S"
  by (metis no segment_bound(1) subsetI norm_minus_commute not_le)
qed

lemma homotopic_nearby_paths:
  fixes g h :: "real \ 'a::euclidean_space"
  assumes "path g" "open S" "path_image g \ S"
    shows "\e. 0 < e \
               (\<forall>h. path h \<and>
                    pathstart h = pathstart g \<and> pathfinish h = pathfinish g \<and>
                    (\<forall>t \<in> {0..1}. norm(h t - g t) < e) \<longrightarrow> homotopic_paths S g h)"
proof -
  obtain e where "e > 0" and e: "\x y. x \ path_image g \ y \ - S \ e \ dist x y"
    using separate_compact_closed [of "path_image g" "-S"] assms by force
  show ?thesis
    using e [unfolded dist_norm] \<open>e > 0\<close>
    by (fastforce simp: path_image_def intro!: homotopic_paths_nearby_explicit assms exI)
qed

lemma homotopic_nearby_loops:
  fixes g h :: "real \ 'a::euclidean_space"
  assumes "path g" "open S" "path_image g \ S" "pathfinish g = pathstart g"
    shows "\e. 0 < e \
               (\<forall>h. path h \<and> pathfinish h = pathstart h \<and>
                    (\<forall>t \<in> {0..1}. norm(h t - g t) < e) \<longrightarrow> homotopic_loops S g h)"
proof -
  obtain e where "e > 0" and e: "\x y. x \ path_image g \ y \ - S \ e \ dist x y"
    using separate_compact_closed [of "path_image g" "-S"] assms by force
  show ?thesis
    using e [unfolded dist_norm] \<open>e > 0\<close>
    by (fastforce simp: path_image_def intro!: homotopic_loops_nearby_explicit assms exI)
qed

subsection\<open> Homotopy and subpaths\<close>

lemma homotopic_join_subpaths1:
  assumes "path g" and pag: "path_image g \ s"
      and u: "u \ {0..1}" and v: "v \ {0..1}" and w: "w \ {0..1}" "u \ v" "v \ w"
    shows "homotopic_paths s (subpath u v g +++ subpath v w g) (subpath u w g)"
proof -
  have 1: "t * 2 \ 1 \ u + t * (v * 2) \ v + t * (u * 2)" for t
    using affine_ineq \<open>u \<le> v\<close> by fastforce
  have 2: "t * 2 > 1 \ u + (2*t - 1) * v \ v + (2*t - 1) * w" for t
    by (metis add_mono_thms_linordered_semiring(1) diff_gt_0_iff_gt less_eq_real_def mult.commute mult_right_mono \<open>u \<le> v\<close> \<open>v \<le> w\<close>)
  have t2: "\t::real. t*2 = 1 \ t = 1/2" by auto
  have "homotopic_paths (path_image g) (subpath u v g +++ subpath v w g) (subpath u w g)"
  proof (cases "w = u")
    case True
    then show ?thesis
      by (metis \<open>path g\<close> homotopic_paths_rinv path_image_subpath_subset path_subpath pathstart_subpath reversepath_subpath subpath_refl u v)
  next
    case False
    let ?f = "\t. if t \ 1/2 then inverse((w - u)) *\<^sub>R (2 * (v - u)) *\<^sub>R t
                               else inverse((w - u)) *\<^sub>R ((v - u) + (w - v) *\<^sub>R (2 *\<^sub>R t - 1))"
    show ?thesis
    proof (rule homotopic_paths_sym [OF homotopic_paths_reparametrize [where f = ?f]])
      show "path (subpath u w g)"
        using assms(1) path_subpath u w(1) by blast
      show "path_image (subpath u w g) \ path_image g"
        by (meson path_image_subpath_subset u w(1))
      show "continuous_on {0..1} ?f"
        unfolding split_01
        by (rule continuous_on_cases continuous_intros | force simp: pathfinish_def joinpaths_def dest!: t2)+
      show "?f ` {0..1} \ {0..1}"
        using False assms
        by (force simp: field_simps not_le mult_left_mono affine_ineq dest!: 1 2)
      show "(subpath u v g +++ subpath v w g) t = subpath u w g (?f t)" if "t \ {0..1}" for t
        using assms
        unfolding joinpaths_def subpath_def by (auto simp add: divide_simps add.commute mult.commute mult.left_commute)
    qed (use False in auto)
  qed
  then show ?thesis
    by (rule homotopic_paths_subset [OF _ pag])
qed

lemma homotopic_join_subpaths2:
  assumes "homotopic_paths s (subpath u v g +++ subpath v w g) (subpath u w g)"
    shows "homotopic_paths s (subpath w v g +++ subpath v u g) (subpath w u g)"
by (metis assms homotopic_paths_reversepath_D pathfinish_subpath pathstart_subpath reversepath_joinpaths reversepath_subpath)

lemma homotopic_join_subpaths3:
  assumes hom: "homotopic_paths s (subpath u v g +++ subpath v w g) (subpath u w g)"
      and "path g" and pag: "path_image g \ s"
      and u: "u \ {0..1}" and v: "v \ {0..1}" and w: "w \ {0..1}"
    shows "homotopic_paths s (subpath v w g +++ subpath w u g) (subpath v u g)"
proof -
  have "homotopic_paths s (subpath u w g +++ subpath w v g) ((subpath u v g +++ subpath v w g) +++ subpath w v g)"
  proof (rule homotopic_paths_join)
    show "homotopic_paths s (subpath u w g) (subpath u v g +++ subpath v w g)"
      using hom homotopic_paths_sym_eq by blast
    show "homotopic_paths s (subpath w v g) (subpath w v g)"
      by (metis \<open>path g\<close> homotopic_paths_eq pag path_image_subpath_subset path_subpath subset_trans v w)
  qed auto
  also have "homotopic_paths s ((subpath u v g +++ subpath v w g) +++ subpath w v g) (subpath u v g +++ subpath v w g +++ subpath w v g)"
    by (rule homotopic_paths_sym [OF homotopic_paths_assoc])
       (use assms in \<open>simp_all add: path_image_subpath_subset [THEN order_trans]\<close>)
  also have "homotopic_paths s (subpath u v g +++ subpath v w g +++ subpath w v g)
                               (subpath u v g +++ linepath (pathfinish (subpath u v g)) (pathfinish (subpath u v g)))"
  proof (rule homotopic_paths_join; simp)
    show "path (subpath u v g) \ path_image (subpath u v g) \ s"
      by (metis \<open>path g\<close> order.trans pag path_image_subpath_subset path_subpath u v)
    show "homotopic_paths s (subpath v w g +++ subpath w v g) (linepath (g v) (g v))"
      by (metis (no_types, lifting) \<open>path g\<close> homotopic_paths_linv order_trans pag path_image_subpath_subset path_subpath pathfinish_subpath reversepath_subpath v w)
  qed
  also have "homotopic_paths s (subpath u v g +++ linepath (pathfinish (subpath u v g)) (pathfinish (subpath u v g))) (subpath u v g)"
  proof (rule homotopic_paths_rid)
    show "path (subpath u v g)"
      using \<open>path g\<close> path_subpath u v by blast
    show "path_image (subpath u v g) \ s"
      by (meson \<open>path g\<close> order.trans pag path_image_subpath_subset u v)
  qed
  finally have "homotopic_paths s (subpath u w g +++ subpath w v g) (subpath u v g)" .
  then show ?thesis
    using homotopic_join_subpaths2 by blast
qed

proposition homotopic_join_subpaths:
   "\path g; path_image g \ s; u \ {0..1}; v \ {0..1}; w \ {0..1}\
    \<Longrightarrow> homotopic_paths s (subpath u v g +++ subpath v w g) (subpath u w g)"
  using le_cases3 [of u v w] homotopic_join_subpaths1 homotopic_join_subpaths2 homotopic_join_subpaths3
  by metis

text\<open>Relating homotopy of trivial loops to path-connectedness.\<close>

lemma path_component_imp_homotopic_points:
  assumes "path_component S a b"
  shows "homotopic_loops S (linepath a a) (linepath b b)"
proof -
  obtain g :: "real \ 'a" where g: "continuous_on {0..1} g" "g ` {0..1} \ S" "g 0 = a" "g 1 = b"
    using assms by (auto simp: path_defs)
  then have "continuous_on ({0..1} \ {0..1}) (g \ fst)"
    by (fastforce intro!: continuous_intros)+
  with g show ?thesis
    by (auto simp add: homotopic_loops_def homotopic_with_def path_defs image_subset_iff)
qed

lemma homotopic_loops_imp_path_component_value:
   "\homotopic_loops S p q; 0 \ t; t \ 1\
        \<Longrightarrow> path_component S (p t) (q t)"
apply (clarsimp simp add: homotopic_loops_def homotopic_with_def path_defs)
apply (rule_tac x="h \ (\u. (u, t))" in exI)
apply (fastforce elim!: continuous_on_subset intro!: continuous_intros)
done

lemma homotopic_points_eq_path_component:
   "homotopic_loops S (linepath a a) (linepath b b) \ path_component S a b"
by (auto simp: path_component_imp_homotopic_points
         dest: homotopic_loops_imp_path_component_value [where t=1])

lemma path_connected_eq_homotopic_points:
    "path_connected S \
      (\<forall>a b. a \<in> S \<and> b \<in> S \<longrightarrow> homotopic_loops S (linepath a a) (linepath b b))"
by (auto simp: path_connected_def path_component_def homotopic_points_eq_path_component)

subsection\<open>Simply connected sets\<close>

text\<^marker>\<open>tag important\<close>\<open>defined as "all loops are homotopic (as loops)\<close>

definition\<^marker>\<open>tag important\<close> simply_connected where
  "simply_connected S \
        \<forall>p q. path p \<and> pathfinish p = pathstart p \<and> path_image p \<subseteq> S \<and>
              path q \<and> pathfinish q = pathstart q \<and> path_image q \<subseteq> S
              \<longrightarrow> homotopic_loops S p q"

lemma simply_connected_empty [iff]: "simply_connected {}"
  by (simp add: simply_connected_def)

lemma simply_connected_imp_path_connected:
  fixes S :: "_::real_normed_vector set"
  shows "simply_connected S \ path_connected S"
by (simp add: simply_connected_def path_connected_eq_homotopic_points)

lemma simply_connected_imp_connected:
  fixes S :: "_::real_normed_vector set"
  shows "simply_connected S \ connected S"
by (simp add: path_connected_imp_connected simply_connected_imp_path_connected)

lemma simply_connected_eq_contractible_loop_any:
  fixes S :: "_::real_normed_vector set"
  shows "simply_connected S \
            (\<forall>p a. path p \<and> path_image p \<subseteq> S \<and> pathfinish p = pathstart p \<and> a \<in> S
                  \<longrightarrow> homotopic_loops S p (linepath a a))"
        (is "?lhs = ?rhs")
proof
  assume ?lhs then show ?rhs
    unfolding simply_connected_def by force
next
  assume ?rhs then show ?lhs
    unfolding simply_connected_def
    by (metis pathfinish_in_path_image subsetD  homotopic_loops_trans homotopic_loops_sym)
qed

lemma simply_connected_eq_contractible_loop_some:
  fixes S :: "_::real_normed_vector set"
  shows "simply_connected S \
                path_connected S \<and>
                (\<forall>p. path p \<and> path_image p \<subseteq> S \<and> pathfinish p = pathstart p
                    \<longrightarrow> (\<exists>a. a \<in> S \<and> homotopic_loops S p (linepath a a)))"
     (is "?lhs = ?rhs")
proof
  assume ?lhs
  then show ?rhs
  using simply_connected_eq_contractible_loop_any by (blast intro: simply_connected_imp_path_connected)
next
  assume r: ?rhs
  note pa = r [THEN conjunct2, rule_format]
  show ?lhs
  proof (clarsimp simp add: simply_connected_eq_contractible_loop_any)
    fix p a
    assume "path p" and "path_image p \ S" "pathfinish p = pathstart p"
      and "a \ S"
    with pa [of p] show "homotopic_loops S p (linepath a a)"
      using homotopic_loops_trans path_connected_eq_homotopic_points r by blast
  qed
qed

lemma simply_connected_eq_contractible_loop_all:
  fixes S :: "_::real_normed_vector set"
  shows "simply_connected S \
         S = {} \<or>
--> --------------------

--> maximum size reached

--> --------------------

¤ Dauer der Verarbeitung: 0.814 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.