# 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

definition✐‹tag 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))))"

text‹‹p›, ‹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)

subsection✐‹tag unimportant›‹Trivial properties›

text ‹We often want to just localize the ending function equality or whatever.›
text✐‹tag 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. (λi∈I. h i (x i)))"
shows "homotopic_with q (product_topology X I) (product_topology Y I)
(λz. (λi∈I. (f i) (z i))) (λz. (λi∈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) (λ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) = (λ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‹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›

definition✐‹tag 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›

text✐‹tag 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)

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›

definition✐‹tag 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
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

subsection✐‹tag 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›

text✐‹tag important›‹defined as "all loops are homotopic (as loops)›

definition✐‹tag 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 Path_Connected.path_continuous_image [OF ‹path p›])
moreover have "path_image (fst ∘ p) ⊆ S"
using that by (force simp: path_image_def)
ultimately have p1: "homotopic_loops S (fst ∘ p) (linepath a a)"
using S that
by (simp add: simply_connected_eq_contractible_loop_any pathfinish_def pathstart_def)
have "path (snd ∘ p)"
by (simp add: continuous_on_snd Path_Connected.path_continuous_image [OF <```