Theory Homotopy

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

section ‹Homotopy of Maps›

theory Homotopy
  imports Path_Connected Product_Topology Uncountable_Sets
begin

definitiontag important› homotopic_with
where
 "homotopic_with P X Y f g 
   (h. continuous_map (prod_topology (top_of_set {0..1::real}) X) Y h 
       (x. h(0, x) = f x) 
       (x. h(1, x) = g x) 
       (t  {0..1}. P(λx. h(t,x))))"

textp›, q› are functions X → Y›, and the property P› restricts all intermediate maps.
We often just want to require that P› fixes some subset, but to include the case of a loop homotopy,
it is convenient to have a general property P›.›

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)

subsectiontag unimportant›‹Trivial properties›

text ‹We often want to just localize the ending function equality or whatever.›
texttag important› ‹%whitespace›
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 
           (h. continuous_map (prod_topology (subtopology euclideanreal {0..1}) X) Y h 
              (x  topspace X. h(0,x) = p x) 
              (x  topspace X. h(1,x) = q x) 
              (t  {0..1}. P(λ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 simp
  by (smt (verit, best) SigmaE assms case_prod_conv continuous_map_eq topspace_prod_topology)

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 (meson continuous_map_subtopology_eu homotopic_with_imp_continuous_maps)

lemma homotopic_with_imp_subset2:
     "homotopic_with_canon P X Y f g  g ` X  Y"
  by (meson continuous_map_subtopology_eu homotopic_with_imp_continuous_maps)

lemma homotopic_with_imp_funspace1:
     "homotopic_with_canon P X Y f g  f  X  Y"
  using homotopic_with_imp_subset1 by blast

lemma homotopic_with_imp_funspace2:
     "homotopic_with_canon P X Y f g  g  X  Y"
  using homotopic_with_imp_subset2 by blast

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‹Homotopy with P is an equivalence relation›

text ‹(on continuous functions mapping X into Y that satisfy P, though this only affects reflexivity)›

lemma homotopic_with_refl [simp]: "homotopic_with P X Y f f  continuous_map X Y f  P f"
  by (metis homotopic_with_equal homotopic_with_imp_continuous_maps 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 flip: image_subset_iff_funcset)
    then show ?thesis
      by (simp add: prod_topology_subtopology(1))
  qed
  show ?thesis
    using assms
    apply (clarsimp simp: 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  (λx. (2 *R fst x, snd x))) y
                             else (k2  (λx. (2 *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  (λx. (2 *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  (λx. (2 *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 *R fst x, snd x))) y = (k2  (λx. (2 *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: 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‹Continuity lemmas›

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)
    homotopic_with q X1 X3 (h  f) (h  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) (λ(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')"
  by (metis assms homotopic_with_compose_continuous_map_left homotopic_with_compose_continuous_map_right homotopic_with_imp_continuous_maps homotopic_with_trans)

proposition homotopic_with_compose_continuous_right:
    "homotopic_with_canon (λf. p (f  h)) X Y f g; continuous_on W h; h  W  X
      homotopic_with_canon p W Y (f  h) (g  h)"
  by (simp add: homotopic_with_compose_continuous_map_right image_subset_iff_funcset)

proposition homotopic_with_compose_continuous_left:
     "homotopic_with_canon (λf. p (h  f)) X Y f g; continuous_on Y h; h  Y  Z
       homotopic_with_canon p X Z (h  f) (h  g)"
  by (simp add: homotopic_with_compose_continuous_map_left image_subset_iff_funcset)

lemma homotopic_from_subtopology:
   "homotopic_with P X X' f g  homotopic_with P (subtopology X S) X' f g"
  by (metis continuous_map_id_subt homotopic_with_compose_continuous_map_right o_id)

lemma homotopic_on_emptyI:
  assumes "P f" "P g"
  shows "homotopic_with P trivial_topology X f g"
  by (metis assms continuous_map_on_empty empty_iff homotopic_with_equal topspace_discrete_topology)

lemma homotopic_on_empty:
   "(homotopic_with P trivial_topology X f g  P f  P g)"
  using homotopic_on_emptyI homotopic_with_imp_property by metis

lemma homotopic_with_canon_on_empty: "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) 
    X = trivial_topology  path_component_of X' a b" (is "?lhs = ?rhs")
proof (cases "X = trivial_topology")
  case False
  then obtain c where c: "c  topspace X"
    by fastforce
  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 | simp add: c)+
    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 (metis c path_component_of_set 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'"
  by (smt (verit, ccfv_SIG) assms homotopic_with)

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)
                          (λz. (f(fst z),g(snd z))) (λ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. (λiI. h i (x i)))"
  shows "homotopic_with q (product_topology X I) (product_topology Y I)
                          (λz. (λiI. (f i) (z i))) (λz. (λiI. (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). λiI. h i (t,z i)"
    have "continuous_map (prod_topology (subtopology euclideanreal {0..1}) (product_topology X I))
                         (Y i) (λx. h i (fst x, snd x i))" if "i  I" for i
    proof -
      have §: "continuous_map (prod_topology (top_of_set {0..1}) (product_topology X I)) (X i) (λ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 § 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) = (λiI. f i (x i))" "?h (1, x) = (λiI. 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‹Homotopic triviality implicitly incorporates path-connectedness.›
lemma homotopic_triviality:
  shows  "(f g. continuous_on S f  f  S  T 
                 continuous_on S g  g  S  T
                  homotopic_with_canon (λx. True) S T f g) 
          (S = {}  path_connected T) 
          (f. continuous_on S f  f  S  T  (c. homotopic_with_canon (λx. True) S T f (λx. c)))"
          (is "?lhs = ?rhs")
proof (cases "S = {}  T = {}")
  case True then show ?thesis
    by (auto simp: homotopic_on_emptyI simp flip: image_subset_iff_funcset)
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 (metis path_component_of_canon_iff topspace_discrete_topology topspace_euclidean_subtopology)
    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 RHS continuous_on S f continuous_on S g f  S  T g  S  T by presburger
      with T have "path_component T c d"
        by (metis False ex_in_conv homotopic_with_imp_subset2 image_subset_iff path_connected_component)
      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‹Homotopy of paths, maintaining the same endpoints›


definitiontag important› homotopic_paths :: "['a set, real  'a, real  'a::topological_space]  bool"
  where
     "homotopic_paths S p q 
       homotopic_with_canon (λr. pathstart r = pathstart p  pathfinish r = pathfinish p) {0..1} S p q"

lemma homotopic_paths:
   "homotopic_paths S p q 
      (h. continuous_on ({0..1} × {0..1}) h 
          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::real}. pathstart(h  Pair t) = pathstart p 
                        pathfinish(h  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"
  using assms homotopic_paths_imp_pathfinish homotopic_paths_imp_pathstart unfolding homotopic_paths_def
  by (smt (verit, ccfv_SIG) homotopic_with_mono homotopic_with_trans)

proposition homotopic_paths_eq:
     "path p; path_image p  S; t. t  {0..1}  p t = q t  homotopic_paths S p q"
  by (smt (verit, best) homotopic_paths homotopic_paths_refl)

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 path p path_def)
  then have "continuous_on {0..1} (p  f)"
    by (meson assms(4) contf continuous_on_compose continuous_on_subset image_subset_iff_funcset)
  then have "path q"
    by (simp add: path_def) (metis q continuous_on_cong)
  have piqs: "path_image q  S"
    by (smt (verit, ccfv_threshold) Pi_iff assms(2) assms(4) assms(7) image_subset_iff path_defs(4))
  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
    by (intro convex_bound_le) (use f01 in auto)
  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  path q 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)) *R ((f  snd) y) + (fst y) *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‹ A slightly ad-hoc but useful lemma in constructing homotopies.›
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 §: "(λt. p (fst t) (2 * snd t)) = ?p  (λ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 §
      by (rule continuous_intros continuous_on_subset [OF p] continuous_on_subset [OF q] | force)+
  qed (use pf in auto simp: mult.commute pathstart_def pathfinish_def)
qed

text‹ Congruence properties of homotopy w.r.t. path-combining operations.›

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: 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 image_subset_iff_funcset)


subsection‹Group properties for homotopy of paths›

texttag important›‹So taking equivalence classes under homotopy would give the fundamental group›

proposition homotopic_paths_rid:
  assumes "path p" "path_image p  S"
  shows "homotopic_paths S (p +++ linepath (pathfinish p) (pathfinish p)) p"
proof -
  have §: "continuous_on {0..1} (λt::real. if t  1/2 then 2 *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 § continuous_on_cases continuous_intros homotopic_paths_reparametrize [where f = "λt. if t  1/2 then 2 *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)

lemma homotopic_paths_rid':
  assumes "path p" "path_image p  s" "x = pathfinish p"
  shows "homotopic_paths s (p +++ linepath x x) p"
  using homotopic_paths_rid[of p s] assms by simp

lemma homotopic_paths_lid':
   "path p; path_image p  s; x = pathstart p  homotopic_paths s (linepath x x +++ p) p"
  using homotopic_paths_lid[of p s] by simp

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 *R t
                           else if  t  3 / 4 then t - (1 / 4)
                           else 2 *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: mult_le_one)+
  qed (auto simp: 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‹Homotopy of loops without requiring preservation of endpoints›

definitiontag important› homotopic_loops :: "'a::topological_space set  (real  'a)  (real  'a)  bool"  where
 "homotopic_loops S p q 
     homotopic_with_canon (λ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  Pair t) = pathstart(h  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  path_image p  S  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: homotopic_loops)

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 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 image_subset_iff_funcset)


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_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 h0[simp]: "x. x  {0..1}  h(0,x) = p x"
             and h1[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 image_subset_iff_funcset)
  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 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))"
    using homotopic_paths_lid [of "p +++ linepath (pathfinish p) (pathfinish p)" S]
    by (metis 1 homotopic_paths_imp_path homotopic_paths_imp_subset homotopic_paths_sym pathstart_join)
  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)))"
    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 (λ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"
      using hs
      unfolding joinpaths_def subpath_def
      by (force simp: algebra_simps mult_le_one mult_left_le  intro: 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 image_subset_iff_funcset)
  qed (use ploop in simp_all add: reversepath_def path_defs joinpaths_def o_def subpath_def conth c1 c2)
  moreover have "homotopic_paths S ((λu. h (u, 0)) +++ linepath a a +++ reversepath (λu. h (u, 0)))
                                   (linepath (pathstart p) (pathstart p))"
    by (rule *; simp add: pih0 pathstart_def pathfinish_def conth0; simp add: reversepath_def joinpaths_def)
  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 path p [unfolded path_def] by blast
  have contq: "continuous_on {0..1} q"  using path q [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 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 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"
      by (smt (verit, best) path q homotopic_paths_imp_path homotopic_paths_imp_subset homotopic_paths_lid 
          homotopic_paths_rid homotopic_paths_trans pathstart_join piq qloop)
    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 path q 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
    obtain pipq: "path_image p  S" "path_image q  S"
      by (metis Un_subset_iff paths path p path q 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 path p path_image p  S 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 path p path q 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 path p path q homotopic_paths_assoc pipq)
    moreover have "homotopic_paths S ((p +++ reversepath q) +++ q) (linepath (pathstart p) (pathstart p) +++ q)"
      by (simp add: path q homotopic_paths_join paths pipq)
    ultimately show ?thesis
      by (metis path q homotopic_paths_imp_path homotopic_paths_lid homotopic_paths_trans path_join_path_ends pathfinish_linepath pipq(2))
  next
    case False
    then show ?thesis
      using path q homotopic_loops_imp_path loops path_join_path_ends by fastforce
  qed
qed


subsectiontag unimportant›‹Homotopy of "nearby" function, paths and loops›

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)) *R f(snd y) + (fst y) *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)) *R (g  snd) y + (fst y) *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)) *R g(snd y) + (fst y) *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 §: "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"
  using homotopic_paths_linear [OF §] by (metis linorder_not_le no norm_minus_commute segment_bound1 subsetI)

lemma homotopic_loops_nearby_explicit:
  assumes §: "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"
  using homotopic_loops_linear [OF §] by (metis linorder_not_le no norm_minus_commute segment_bound1 subsetI)

lemma homotopic_nearby_paths:
  fixes g h :: "real  'a::euclidean_space"
  assumes "path g" "open S" "path_image g  S"
    shows "e. 0 < e 
               (h. path h 
                    pathstart h = pathstart g  pathfinish h = pathfinish g 
                    (t  {0..1}. norm(h t - g t) < e)  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] e > 0
    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 
               (h. path h  pathfinish h = pathstart h 
                    (t  {0..1}. norm(h t - g t) < e)  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] e > 0
    by (fastforce simp: path_image_def intro!: homotopic_loops_nearby_explicit assms exI)
qed


subsection‹ Homotopy and subpaths›

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 u  v 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 u  v v  w)
  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 path g 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)) *R (2 * (v - u)) *R t
                               else inverse((w - u)) *R ((v - u) + (w - v) *R (2 *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: 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 -
  obtain wvg: "path (subpath w v g)" "path_image (subpath w v g)  S" 
     and wug: "path (subpath w u g)" "path_image (subpath w u g)  S"
     and vug: "path (subpath v u g)" "path_image (subpath v u g)  S"
    by (meson path g pag path_image_subpath_subset path_subpath subset_trans u v w)
  have "homotopic_paths S (subpath u w g +++ subpath w v g) 
                          ((subpath u v g +++ subpath v w g) +++ subpath w v g)"
    by (simp add: hom homotopic_paths_join homotopic_paths_sym wvg)
  also have "homotopic_paths S   (subpath u v g +++ subpath v w g +++ subpath w v g)"
    using wvg vug path g
    by (metis homotopic_paths_assoc homotopic_paths_sym path_image_subpath_commute path_subpath
        pathfinish_subpath pathstart_subpath u v w)
  also have "homotopic_paths S  (subpath u v g +++ linepath (pathfinish (subpath u v g)) (pathfinish (subpath u v g)))"
    using wvg vug path g
    by (metis homotopic_paths_join homotopic_paths_linv homotopic_paths_refl path_image_subpath_commute
        path_subpath pathfinish_subpath pathstart_join pathstart_subpath reversepath_subpath u v)
  also have "homotopic_paths S  (subpath u v g)"
    using vug path g by (metis homotopic_paths_rid path_image_subpath_commute path_subpath u v)
  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}
     homotopic_paths S (subpath u v g +++ subpath v w g) (subpath u w g)"
  by (smt (verit, del_insts) homotopic_join_subpaths1 homotopic_join_subpaths2 homotopic_join_subpaths3)

text‹Relating homotopy of trivial loops to path-connectedness.›

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: homotopic_loops_def homotopic_with_def path_defs Pi_iff)
qed

lemma homotopic_loops_imp_path_component_value:
  "homotopic_loops S p q; 0  t; t  1  path_component S (p t) (q t)"
  apply (clarsimp simp: 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"
  using homotopic_loops_imp_path_component_value path_component_imp_homotopic_points by fastforce

lemma path_connected_eq_homotopic_points:
  "path_connected S 
      (a b. a  S  b  S  homotopic_loops S (linepath a a) (linepath b b))"
  by (auto simp: path_connected_def path_component_def homotopic_points_eq_path_component)


subsection‹Simply connected sets›

texttag important›‹defined as "all loops are homotopic (as loops)›

definitiontag important› simply_connected where
  "simply_connected S 
        p q. path p  pathfinish p = pathstart p  path_image p  S 
              path q  pathfinish q = pathstart q  path_image q  S
               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 
            (p a. path p  path_image p  S  pathfinish p = pathstart p  a  S
                   homotopic_loops S p (linepath a a))"
        (is "?lhs = ?rhs")
proof
  assume ?rhs then show ?lhs
    unfolding simply_connected_def
    by (metis pathfinish_in_path_image subsetD  homotopic_loops_trans homotopic_loops_sym)
qed (force simp: simply_connected_def)

lemma simply_connected_eq_contractible_loop_some:
  fixes S :: "_::real_normed_vector set"
  shows "simply_connected S 
                path_connected S 
                (p. path p  path_image p  S  pathfinish p = pathstart p
                     (a. a  S  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 ?rhs
  then show ?lhs
    by (meson homotopic_loops_trans path_connected_eq_homotopic_points simply_connected_eq_contractible_loop_any)
qed

lemma simply_connected_eq_contractible_loop_all:
  fixes S :: "_::real_normed_vector set"
  shows "simply_connected S 
         S = {} 
         (a  S. p. path p  path_image p  S  pathfinish p = pathstart p
                 homotopic_loops S p (linepath a a))"
  by (meson ex_in_conv homotopic_loops_sym homotopic_loops_trans simply_connected_def simply_connected_eq_contractible_loop_any)

lemma simply_connected_eq_contractible_path:
  fixes S :: "_::real_normed_vector set"
  shows "simply_connected S 
           path_connected S 
           (p. path p  path_image p  S  pathfinish p = pathstart p
             homotopic_paths S p (linepath (pathstart p) (pathstart p)))"
     (is "?lhs = ?rhs")
proof
  assume ?lhs
  then show ?rhs
    unfolding simply_connected_imp_path_connected
    by (metis simply_connected_eq_contractible_loop_some homotopic_loops_imp_homotopic_paths_null)
next
  assume  ?rhs
  then show ?lhs
    using homotopic_paths_imp_homotopic_loops simply_connected_eq_contractible_loop_some by fastforce
qed

lemma simply_connected_eq_homotopic_paths:
  fixes S :: "_::real_normed_vector set"
  shows "simply_connected S 
          path_connected S 
          (p q. path p  path_image p  S 
                path q  path_image q  S 
                pathstart q = pathstart p  pathfinish q = pathfinish p
                 homotopic_paths S p q)"
         (is "?lhs = ?rhs")
proof
  assume ?lhs
  then have pc: "path_connected S"
        and *:  "p. path p; path_image p  S;
                       pathfinish p = pathstart p
                       homotopic_paths S p (linepath (pathstart p) (pathstart p))"
    by (auto simp: simply_connected_eq_contractible_path)
  have "homotopic_paths S p q"
        if "path p" "path_image p  S" "path q"
           "path_image q  S" "pathstart q = pathstart p"
           "pathfinish q = pathfinish p" for p q
  proof -
    have "homotopic_paths S p (p +++ reversepath q +++ q)"
      using that
      by (smt (verit, best) homotopic_paths_join homotopic_paths_linv homotopic_paths_rid homotopic_paths_sym 
          homotopic_paths_trans pathstart_linepath)
    also have "homotopic_paths S  ((p +++ reversepath q) +++ q)"
      by (simp add: that homotopic_paths_assoc)
    also have "homotopic_paths S  (linepath (pathstart q) (pathstart q) +++ q)"
      using * [of "p +++ reversepath q"] that
      by (simp add: homotopic_paths_assoc homotopic_paths_join path_image_join)
    also have "homotopic_paths S  q"
      using that homotopic_paths_lid by blast
    finally show ?thesis .
  qed
  then show ?rhs
    by (blast intro: pc *)
next
  assume ?rhs
  then show ?lhs
    by (force simp: simply_connected_eq_contractible_path)
qed

proposition simply_connected_Times:
  fixes S :: "'a::real_normed_vector set" and T :: "'b::real_normed_vector set"
  assumes S: "simply_connected S" and T: "simply_connected T"
    shows "simply_connected(S × T)"
proof -
  have "homotopic_loops (S × T) p (linepath (a, b) (a, b))"
       if "path p" "path_image p  S × T" "p 1 = p 0" "a  S" "b  T"
       for p a b
  proof -
    have "path (fst  p)"
      by (simp add: continuous_on_fst