Theory Explicit_Path_Homotopy_Scaffold

theory Explicit_Path_Homotopy_Scaffold
  imports "HOL-Analysis.Homotopy"
begin

section ‹Explicit-topology paths and homotopies›

text ‹
  HOL-Analysis already provides paths and homotopies for subsets of a type. For
  the pushout-oriented development, however, it is convenient to work directly
  with arbitrary topologies. This theory therefore rephrases the basic path and
  homotopy notions in explicit-topology form.
›

definition loopin_space ::
  "'a topology ⇒ 'a ⇒ (real ⇒ 'a) set"
where
  "loopin_space X x = {p. pathin X p ∧ p 0 = x ∧ p 1 = x}"

definition homotopic_pathsin ::
  "'a topology ⇒ (real ⇒ 'a) ⇒ (real ⇒ 'a) ⇒ bool"
where
  "homotopic_pathsin X p q ≡
     homotopic_with (λr. r 0 = p 0 ∧ r 1 = p 1) (top_of_set {0..1}) X p q"

definition homotopic_loopsin ::
  "'a topology ⇒ (real ⇒ 'a) ⇒ (real ⇒ 'a) ⇒ bool"
where
  "homotopic_loopsin X p q ≡
     homotopic_with (λr. r 1 = r 0) (top_of_set {0..1}) X p q"

definition reversepathin :: "(real ⇒ 'a) ⇒ real ⇒ 'a"
where
  "reversepathin p = (λt. p (1 - t))"

definition joinpathin :: "(real ⇒ 'a) ⇒ (real ⇒ 'a) ⇒ real ⇒ 'a"
where
  "joinpathin p q = (λt. if t ≤ 1 / 2 then p (2 * t) else q (2 * t - 1))"

definition subpathin :: "real ⇒ real ⇒ (real ⇒ 'a) ⇒ real ⇒ 'a"
where
  "subpathin u v p = (λt. p ((v - u) * t + u))"

lemma reversepathin_eq_reversepath [simp]:
  "reversepathin p = reversepath p"
  unfolding reversepathin_def reversepath_def by simp

lemma reversepathin_reversepathin [simp]:
  "reversepathin (reversepathin p) = p"
  unfolding reversepathin_def by (rule ext) simp

lemma joinpathin_eq_joinpaths [simp]:
  "joinpathin p q = p +++ q"
  unfolding joinpathin_def joinpaths_def by simp

lemma subpathin_image:
  "subpathin u v p ` {0..1} = p ` closed_segment u v"
  by (simp add: subpathin_def image_image closed_segment_real_eq algebra_simps)

lemma subpathin_image_eq:
  assumes "u ≤ v"
  shows "subpathin u v p ` {0..1} = p ` {u..v}"
  using assms by (simp add: subpathin_image closed_segment_eq_real_ivl)

lemma subpathin_0_1 [simp]:
  "subpathin 0 1 p = p"
  unfolding subpathin_def by (rule ext) simp

lemma joinpathin_subpathin_middle [simp]:
  "joinpathin (subpathin 0 (1 / 2) p) (subpathin (1 / 2) 1 p) = p"
  unfolding joinpathin_def subpathin_def
  by (rule ext) (auto simp: field_simps)

lemma continuous_map_top01_id:
  "continuous_map (top_of_set {0..1}) euclideanreal id"
  by (rule continuous_map_into_fulltopology[OF continuous_map_id])

lemma loopin_spaceI:
  assumes "pathin X p"
    and "p 0 = x"
    and "p 1 = x"
  shows "p ∈ loopin_space X x"
  using assms unfolding loopin_space_def by blast

lemma loopin_spaceE:
  assumes "p ∈ loopin_space X x"
  obtains "pathin X p" "p 0 = x" "p 1 = x"
  using assms unfolding loopin_space_def by blast

lemma constant_loopin_in_space:
  assumes "x ∈ topspace X"
  shows "(λ_. x) ∈ loopin_space X x"
  using assms unfolding loopin_space_def by auto

lemma pathin_image_subset_topspace:
  assumes "pathin X p"
  shows "p ` {0..1} ⊆ topspace X"
proof -
  have "p ∈ {0..1} → topspace X"
    using assms by (rule path_image_subset_topspace)
  then show ?thesis
    by auto
qed

lemma pathin_reversepathin:
  assumes "pathin X p"
  shows "pathin X (reversepathin p)"
proof -
  have rev_cont: "continuous_map (top_of_set {0..1}) (top_of_set {0..1}) (λt::real. 1 - t)"
    by (intro continuous_map_into_subtopology continuous_intros) auto
  have "continuous_map (top_of_set {0..1}) X (p ∘ (λt::real. 1 - t))"
    using rev_cont assms unfolding pathin_def by (rule continuous_map_compose)
  then show ?thesis
    unfolding pathin_def reversepathin_def by (simp add: o_def)
qed

lemma pathin_joinpathin:
  assumes p: "pathin X p"
    and q: "pathin X q"
    and pq: "p 1 = q 0"
  shows "pathin X (joinpathin p q)"
proof -
  let ?T01 = "subtopology euclideanreal {0..1}"
  have p_cont: "continuous_map ?T01 X p"
    using p unfolding pathin_def .
  have q_cont: "continuous_map ?T01 X q"
    using q unfolding pathin_def .
  have left_scale_eu:
    "continuous_map (subtopology ?T01 {x ∈ topspace ?T01. 2 * x ≤ 1}) euclideanreal (λx::real. 2 * x)"
  proof -
    have "continuous_map ?T01 euclideanreal (λx::real. 2 * x)"
      by (simp add: continuous_map_iff_continuous continuous_intros)
    then show ?thesis
      by (rule continuous_map_from_subtopology)
  qed
  have left_scale_range:
    "(λx::real. 2 * x) ∈ topspace (subtopology ?T01 {x ∈ topspace ?T01. 2 * x ≤ 1}) → {0..1}"
  proof
    fix x :: real
    assume x_in: "x ∈ topspace (subtopology ?T01 {x ∈ topspace ?T01. 2 * x ≤ 1})"
    then have x01: "x ∈ {0..1}" and x_half: "2 * x ≤ 1"
      by auto
    from x01 have x_ge0: "0 ≤ x"
      by auto
    have lower: "0 ≤ 2 * x"
      using x_ge0 by linarith
    show "2 * x ∈ {0..1}"
      using lower x_half by simp
  qed
  have left_scale_cont:
    "continuous_map (subtopology ?T01 {x ∈ topspace ?T01. 2 * x ≤ 1}) ?T01 (λx::real. 2 * x)"
    by (rule continuous_map_into_subtopology[OF left_scale_eu left_scale_range])
  have left_cont_comp:
    "continuous_map (subtopology ?T01 {x ∈ topspace ?T01. 2 * x ≤ 1}) X
      (p ∘ (λx::real. 2 * x))"
    by (rule continuous_map_compose[OF left_scale_cont p_cont])
  have left_eq:
    "(p ∘ (λx::real. 2 * x)) = (λx::real. p (2 * x))"
    by (auto simp: fun_eq_iff o_def)
  from left_cont_comp have left_cont:
    "continuous_map (subtopology ?T01 {x ∈ topspace ?T01. 2 * x ≤ 1}) X (λx::real. p (2 * x))"
    by (simp only: left_eq)
  have right_shift_eu:
    "continuous_map (subtopology ?T01 {x ∈ topspace ?T01. 1 ≤ 2 * x}) euclideanreal (λx::real. 2 * x - 1)"
  proof -
    have "continuous_map ?T01 euclideanreal (λx::real. 2 * x - 1)"
      by (simp add: continuous_map_iff_continuous continuous_intros)
    then show ?thesis
      by (rule continuous_map_from_subtopology)
  qed
  have right_shift_range:
    "(λx::real. 2 * x - 1) ∈ topspace (subtopology ?T01 {x ∈ topspace ?T01. 1 ≤ 2 * x}) → {0..1}"
  proof
    fix x :: real
    assume x_in: "x ∈ topspace (subtopology ?T01 {x ∈ topspace ?T01. 1 ≤ 2 * x})"
    then have x01: "x ∈ {0..1}" and x_half: "1 ≤ 2 * x"
      by auto
    from x01 have x_le1: "x ≤ 1"
      by auto
    have lower: "0 ≤ 2 * x - 1"
      using x_half by linarith
    have upper: "2 * x - 1 ≤ 1"
      using x_le1 by linarith
    show "2 * x - 1 ∈ {0..1}"
      using lower upper by simp
  qed
  have right_shift_cont:
    "continuous_map (subtopology ?T01 {x ∈ topspace ?T01. 1 ≤ 2 * x}) ?T01 (λx::real. 2 * x - 1)"
    by (rule continuous_map_into_subtopology[OF right_shift_eu right_shift_range])
  have right_cont_comp:
    "continuous_map (subtopology ?T01 {x ∈ topspace ?T01. 1 ≤ 2 * x}) X
      (q ∘ (λx::real. 2 * x - 1))"
    by (rule continuous_map_compose[OF right_shift_cont q_cont])
  have right_eq:
    "(q ∘ (λx::real. 2 * x - 1)) = (λx::real. q (2 * x - 1))"
    by (auto simp: fun_eq_iff o_def)
  from right_cont_comp have right_cont:
    "continuous_map (subtopology ?T01 {x ∈ topspace ?T01. 1 ≤ 2 * x}) X (λx::real. q (2 * x - 1))"
    by (simp only: right_eq)
  have cont_if:
    "continuous_map ?T01 X (λx::real. if 2 * x ≤ 1 then p (2 * x) else q (2 * x - 1))"
  proof (rule continuous_map_cases_le[where p = "λx::real. 2 * x" and q = "λ_. 1"])
    show "continuous_map ?T01 euclideanreal (λx::real. 2 * x)"
      by (simp add: continuous_map_iff_continuous continuous_intros)
    show "continuous_map ?T01 euclideanreal (λ_. 1)"
      by simp
    show "continuous_map (subtopology ?T01 {x ∈ topspace ?T01. 2 * x ≤ 1}) X (λx::real. p (2 * x))"
      by (rule left_cont)
    show "continuous_map (subtopology ?T01 {x ∈ topspace ?T01. 1 ≤ 2 * x}) X (λx::real. q (2 * x - 1))"
      by (rule right_cont)
    show "p (2 * x) = q (2 * x - 1)"
      if "x ∈ topspace ?T01" "(λx::real. 2 * x) x = (λ_. 1) x" for x
      using pq that by simp
  qed
  have cont_join: "continuous_map ?T01 X (joinpathin p q)"
  proof (rule continuous_map_eq[OF cont_if])
    fix x :: real
    assume x_in: "x ∈ topspace ?T01"
    show "(λx::real. if 2 * x ≤ 1 then p (2 * x) else q (2 * x - 1)) x = joinpathin p q x"
      using x_in by (simp add: joinpathin_def field_simps)
  qed
  show ?thesis
    using cont_join unfolding pathin_def .
qed

lemma pathin_subpathin:
  assumes p: "pathin X p"
    and u: "u ∈ {0..1}"
    and v: "v ∈ {0..1}"
  shows "pathin X (subpathin u v p)"
proof -  
  have aff_cont:
    "continuous_map (top_of_set {0..1}) (top_of_set {0..1}) (λt::real. (v - u) * t + u)"
  proof -
    have aff_cont_eu:
      "continuous_map (top_of_set {0..1}) euclideanreal (λt::real. (v - u) * t + u)"
      by (simp add: continuous_map_iff_continuous continuous_intros)
    have aff_range:
      "(λt::real. (v - u) * t + u) ∈ topspace (top_of_set {0..1}) → {0..1}"
    proof
      fix x :: real
      assume x_in: "x ∈ topspace (top_of_set {0..1})"
      have x01: "x ∈ {0..1}"
        using x_in by simp
      have nonneg: "0 ≤ x * v + (1 - x) * u"
        using u v x01 by (intro add_nonneg_nonneg mult_nonneg_nonneg) auto
      moreover have le1: "x * v + (1 - x) * u ≤ 1"
        using u v x01 by (intro convex_bound_le) auto
      ultimately show "((v - u) * x + u) ∈ {0..1}"
        by (simp add: algebra_simps)
    qed
    show ?thesis
      using aff_cont_eu aff_range by (auto simp: continuous_map_in_subtopology)
  qed
  have "continuous_map (top_of_set {0..1}) X (p ∘ (λt::real. (v - u) * t + u))"
    using aff_cont p unfolding pathin_def by (rule continuous_map_compose)
  then show ?thesis
    unfolding pathin_def subpathin_def by (simp add: o_def)
qed

lemma pathin_subdivision_open_cover:
  assumes p: "pathin X p"
    and cover: "p ` {0..1} ⊆ ⋃𝒰"
    and openU: "⋀U. U ∈ 𝒰 ⟹ openin X U"
  shows "∃n::nat. 0 < n ∧
      (∀i<n. ∃U∈𝒰.
        subpathin (real i / real n) (real (Suc i) / real n) p ` {0..1} ⊆ U)"
proof -
  have U_nonempty: "𝒰 ≠ {}"
  proof
    assume "𝒰 = {}"
    moreover have "p 0 ∈ p ` {0..1}"
      by auto
    ultimately show False
      using cover by auto
  qed
  define W where
    "W U = (SOME T. open T ∧ {t ∈ {0..1}. p t ∈ U} = {0..1} ∩ T)" for U
  have pre_open: "openin (top_of_set {0..1}) {t ∈ {0..1}. p t ∈ U}" if U_in: "U ∈ 𝒰" for U
    using p openU[OF U_in]
    unfolding pathin_def continuous_map_def
    by auto
  have W_spec:
      "open (W U)"
      "{t ∈ {0..1}. p t ∈ U} = {0..1} ∩ W U"
    if U_in: "U ∈ 𝒰" for U
  proof -
    from pre_open[OF U_in] obtain T where
        T_open: "open T"
        and T_eq: "{t ∈ {0..1}. p t ∈ U} = {0..1} ∩ T"
      by (auto simp: openin_open)
    have "open (W U) ∧ {t ∈ {0..1}. p t ∈ U} = {0..1} ∩ W U"
      unfolding W_def
      by (rule someI_ex) (use T_open T_eq in blast)
    then show "open (W U)" "{t ∈ {0..1}. p t ∈ U} = {0..1} ∩ W U"
      by auto
  qed
  have interval_cover: "{0..1} ⊆ ⋃(W ` 𝒰)"
  proof
    fix t :: real
    assume t_in: "t ∈ {0..1}"
    have "p t ∈ p ` {0..1}"
      using t_in by blast
    then obtain U where U_in: "U ∈ 𝒰" and pU: "p t ∈ U"
      using cover by blast
    have "{t ∈ {0..1}. p t ∈ U} = {0..1} ∩ W U"
      by (rule W_spec(2)[OF U_in])
    then have "t ∈ W U"
      using t_in pU by auto
    then show "t ∈ ⋃(W ` 𝒰)"
      using U_in by blast
  qed
  have open_W_image: "open B" if "B ∈ W ` 𝒰" for B
  proof -
    from that obtain U where U_in: "U ∈ 𝒰" and B_eq: "B = W U"
      by blast
    show "open B"
      unfolding B_eq by (rule W_spec(1)[OF U_in])
  qed
  have W_nonempty: "W ` 𝒰 ≠ {}"
    using U_nonempty by auto
  have compact01: "compact ({0..1::real})"
    by (rule compact_Icc)
  from Lebesgue_number_lemma[OF compact01 W_nonempty interval_cover open_W_image]
  obtain δ where δ_pos: "0 < δ"
    and δ_cover:
      "⋀T. T ⊆ {0..1} ⟹ diameter T < δ ⟹ ∃B∈W ` 𝒰. T ⊆ B"
    by blast
  obtain m where m: "inverse (of_nat (Suc m)) < δ"
    using reals_Archimedean[OF δ_pos] by blast
  let ?n = "Suc m"
  have segment_cover:
    "∃U∈𝒰. subpathin (real i / real ?n) (real (Suc i) / real ?n) p ` {0..1} ⊆ U"
    if i_lt: "i < ?n" for i
  proof -
    let ?a = "real i / real ?n"
    let ?b = "real (Suc i) / real ?n"
    let ?T = "{?a..?b}"
    have a01: "?a ∈ {0..1}"
      using i_lt by auto
    have b01: "?b ∈ {0..1}"
      using i_lt by auto
    have ab: "?a ≤ ?b"
      using i_lt by (simp add: field_simps)
    have T_subset: "?T ⊆ {0..1}"
      using a01 b01 by auto
    have "diameter ?T = ?b - ?a"
      using ab by simp
    also have "… = 1 / real ?n"
      by (simp add: field_simps)
    also have "… < δ"
      using m by (simp add: divide_inverse)
    finally have T_small: "diameter ?T < δ" .
    from δ_cover[OF T_subset T_small] obtain B where
        B_in: "B ∈ W ` 𝒰"
        and T_B: "?T ⊆ B"
      by blast
    obtain U where U_in: "U ∈ 𝒰" and B_eq: "B = W U"
      using B_in by blast
    have pre_eq: "{t ∈ {0..1}. p t ∈ U} = {0..1} ∩ W U"
      by (rule W_spec(2)[OF U_in])
    have subpath_subset: "subpathin ?a ?b p ` {0..1} ⊆ U"
    proof
      fix x
      assume x_in: "x ∈ subpathin ?a ?b p ` {0..1}"
      then obtain t where t_in: "t ∈ {0..1}" and x_eq: "x = subpathin ?a ?b p t"
        by blast
      have s_in_T: "((?b - ?a) * t + ?a) ∈ ?T"
      proof -
        from t_in have t_ge0: "0 ≤ t" and t_le1: "t ≤ 1"
          by auto
        have diff_nonneg: "0 ≤ ?b - ?a"
          using ab by linarith
        have term_nonneg: "0 ≤ (?b - ?a) * t"
          by (rule mult_nonneg_nonneg[OF diff_nonneg t_ge0])
        have term_le: "(?b - ?a) * t ≤ (?b - ?a) * 1"
          using t_le1 diff_nonneg by (rule mult_left_mono)
        have lower: "?a ≤ (?b - ?a) * t + ?a"
          using term_nonneg by linarith
        have upper: "(?b - ?a) * t + ?a ≤ ?b"
          using term_le by simp
        show ?thesis
          using lower upper by simp
      qed
      have s_in_unit: "((?b - ?a) * t + ?a) ∈ {0..1}"
        using s_in_T T_subset by blast
      have s_in_W: "((?b - ?a) * t + ?a) ∈ W U"
        using s_in_T T_B B_eq by auto
      have "((?b - ?a) * t + ?a) ∈ {t ∈ {0..1}. p t ∈ U}"
        using s_in_unit s_in_W pre_eq by auto
      then show "x ∈ U"
        using x_eq by (simp add: subpathin_def)
    qed
    then show ?thesis
      using U_in by blast
  qed
  show ?thesis
    by (rule exI[of _ ?n]) (use segment_cover in auto)
qed

lemma loopin_space_joinpathin:
  assumes p: "p ∈ loopin_space X x"
    and q: "q ∈ loopin_space X x"
  shows "joinpathin p q ∈ loopin_space X x"
proof -
  from p obtain p_in where p_in: "pathin X p" "p 0 = x" "p 1 = x"
    by (rule loopin_spaceE)
  from q obtain q_in where q_in: "pathin X q" "q 0 = x" "q 1 = x"
    by (rule loopin_spaceE)
  have "pathin X (joinpathin p q)"
    by (rule pathin_joinpathin[OF p_in(1) q_in(1)]) (simp add: p_in q_in)
  moreover have "joinpathin p q 0 = x" "joinpathin p q 1 = x"
    by (simp_all add: joinpathin_def p_in q_in)
  ultimately show ?thesis
    by (rule loopin_spaceI)
qed

lemma homotopic_pathsin_top_of_set [simp]:
  "homotopic_pathsin (top_of_set S) p q ⟷ homotopic_paths S p q"
  unfolding homotopic_pathsin_def homotopic_paths_def
  by (simp add: pathstart_def pathfinish_def)

lemma homotopic_loopsin_top_of_set [simp]:
  "homotopic_loopsin (top_of_set S) p q ⟷ homotopic_loops S p q"
  unfolding homotopic_loopsin_def homotopic_loops_def
  by (simp add: pathstart_def pathfinish_def)

lemma homotopic_pathsin_imp_pathin:
  assumes "homotopic_pathsin X p q"
  shows "pathin X p" "pathin X q"
  using assms unfolding homotopic_pathsin_def pathin_def
  by (auto dest: homotopic_with_imp_continuous_maps)

lemma homotopic_pathsin_imp_endpoints:
  assumes "homotopic_pathsin X p q"
  shows "q 0 = p 0" "q 1 = p 1"
  using assms unfolding homotopic_pathsin_def
  by (auto dest: homotopic_with_imp_property)

lemma homotopic_pathsin_refl [simp]:
  "homotopic_pathsin X p p ⟷ pathin X p"
  unfolding homotopic_pathsin_def pathin_def
  by (simp add: homotopic_with_refl)

lemma homotopic_pathsin_sym:
  assumes "homotopic_pathsin X p q"
  shows "homotopic_pathsin X q p"
proof -
  have "q 0 = p 0" "q 1 = p 1"
    using assms by (rule homotopic_pathsin_imp_endpoints)+
  with assms show ?thesis
    unfolding homotopic_pathsin_def
    by (simp add: homotopic_with_sym)
qed

lemma homotopic_pathsin_trans:
  assumes "homotopic_pathsin X p q"
    and "homotopic_pathsin X q r"
  shows "homotopic_pathsin X p r"
proof -
  have q: "q 0 = p 0" "q 1 = p 1"
    using assms(1) by (rule homotopic_pathsin_imp_endpoints)+
  have pq: "homotopic_with (λs. s 0 = p 0 ∧ s 1 = p 1) (top_of_set {0..1}) X p q"
    using assms(1) unfolding homotopic_pathsin_def .
  have qr: "homotopic_with (λs. s 0 = p 0 ∧ s 1 = p 1) (top_of_set {0..1}) X q r"
    using assms(2) q unfolding homotopic_pathsin_def by simp
  from pq qr show ?thesis
    unfolding homotopic_pathsin_def by (rule homotopic_with_trans)
qed

lemma homotopic_pathsin_eq:
  assumes "pathin X p"
    and "⋀t. t ∈ {0..1} ⟹ p t = q t"
  shows "homotopic_pathsin X p q"
proof -
  have "continuous_map (top_of_set {0..1}) X p"
    using assms(1) unfolding pathin_def by simp
  moreover have "∀x∈topspace (top_of_set {0..1}). p x = q x"
    using assms(2) by simp
  ultimately show ?thesis
    unfolding homotopic_pathsin_def
     by (intro homotopic_with_equal) auto
qed

lemma continuous_map_homotopic_joinpathin_lemma:
  fixes p q :: "real ⇒ real ⇒ 'a"
  assumes p:
      "continuous_map (prod_topology (top_of_set {0..1}) (top_of_set {0..1})) X
        (λy. p (fst y) (snd y))"
    and q:
      "continuous_map (prod_topology (top_of_set {0..1}) (top_of_set {0..1})) X
        (λy. q (fst y) (snd y))"
    and pq: "⋀t. t ∈ {0..1} ⟹ p t 1 = q t 0"
  shows
    "continuous_map (prod_topology (top_of_set {0..1}) (top_of_set {0..1})) X
      (λy. joinpathin (p (fst y)) (q (fst y)) (snd y))"
proof -
  let ?T01 = "subtopology euclideanreal {0..1}"
  let ?A = "prod_topology ?T01 ?T01"
  have sect:
    "(λt. p (fst t) (2 * snd t)) = (λy. p (fst y) (snd y)) ∘ (λy. (fst y, 2 * snd y))"
    "(λt. q (fst t) (2 * snd t - 1)) = (λy. q (fst y) (snd y)) ∘ (λy. (fst y, 2 * snd y - 1))"
    by force+
  show ?thesis
    unfolding joinpathin_def
  proof (rule continuous_map_cases_le)
    show "continuous_map ?A euclideanreal snd"
      by (rule continuous_map_into_fulltopology[OF continuous_map_snd])
    show "continuous_map ?A euclideanreal (λ_. 1 / 2)"
      by simp
    have left_pair_cont:
      "continuous_map (subtopology ?A {y ∈ topspace ?A. snd y ≤ 1 / 2}) ?A
        (λt. (fst t, 2 * snd t))"
  proof (rule continuous_map_pairedI)
      show "continuous_map (subtopology ?A {y ∈ topspace ?A. snd y ≤ 1 / 2}) ?T01 fst"
        by (rule continuous_map_from_subtopology[OF continuous_map_fst])
      show "continuous_map (subtopology ?A {y ∈ topspace ?A. snd y ≤ 1 / 2}) ?T01 (λt. 2 * snd t)"
      proof -
        have snd_cont:
          "continuous_map (subtopology ?A {y ∈ topspace ?A. snd y ≤ 1 / 2}) euclideanreal snd"
          by (rule continuous_map_into_fulltopology[OF continuous_map_subtopology_snd])
        have scale_cont:
          "continuous_map (subtopology ?A {y ∈ topspace ?A. snd y ≤ 1 / 2}) euclideanreal
            (λt. 2 * snd t)"
          using snd_cont by (intro continuous_intros)
        have scale_range:
          "(λt. 2 * snd t) ∈
            topspace (subtopology ?A {y ∈ topspace ?A. snd y ≤ 1 / 2}) → {0..1}"
        proof
          fix t :: "real × real"
          assume t_in: "t ∈ topspace (subtopology ?A {y ∈ topspace ?A. snd y ≤ 1 / 2})"
          then have tA: "t ∈ topspace ?A" and t_half: "snd t ≤ 1 / 2"
            by auto
          have snd01: "snd t ∈ {0..1}"
            using tA by (auto simp: topspace_prod_topology)
          from snd01 have snd_ge0: "0 ≤ snd t" and snd_le1: "snd t ≤ 1"
            by auto
          have lower: "0 ≤ 2 * (snd t :: real)"
            using snd_ge0 by linarith
          have upper: "2 * (snd t :: real) ≤ 1"
            using t_half by linarith
          have bounds: "0 ≤ 2 * (snd t :: real) ∧ 2 * (snd t :: real) ≤ 1"
            using lower upper by blast
          show "2 * (snd t :: real) ∈ {0..1}"
          proof -
            from bounds have lower': "0 ≤ 2 * (snd t :: real)" and upper': "2 * (snd t :: real) ≤ 1"
              by auto
            show ?thesis
              using lower' upper' by (auto simp: atLeastAtMost_iff)
          qed
        qed
        show ?thesis
          by (rule continuous_map_into_subtopology[OF scale_cont scale_range])
      qed
    qed
    have left_comp:
      "continuous_map (subtopology ?A {y ∈ topspace ?A. snd y ≤ 1 / 2}) X
        (((λy. p (fst y) (snd y)) ∘ (λy. (fst y, 2 * snd y))))"
      by (rule continuous_map_compose[OF left_pair_cont p])
    show "continuous_map (subtopology ?A {y ∈ topspace ?A. snd y ≤ 1 / 2}) X
            (λt. p (fst t) (2 * snd t))"
      using left_comp by (simp add: o_def)
    have right_pair_cont:
      "continuous_map (subtopology ?A {y ∈ topspace ?A. 1 / 2 ≤ snd y}) ?A
        (λt. (fst t, 2 * snd t - 1))"
  proof (rule continuous_map_pairedI)
      show "continuous_map (subtopology ?A {y ∈ topspace ?A. 1 / 2 ≤ snd y}) ?T01 fst"
        by (rule continuous_map_from_subtopology[OF continuous_map_fst])
      show "continuous_map (subtopology ?A {y ∈ topspace ?A. 1 / 2 ≤ snd y}) ?T01 (λt. 2 * (snd t :: real) - 1)"
      proof -
        have snd_cont:
          "continuous_map (subtopology ?A {y ∈ topspace ?A. 1 / 2 ≤ snd y}) euclideanreal snd"
          by (rule continuous_map_into_fulltopology[OF continuous_map_subtopology_snd])
        have affine_cont:
          "continuous_map (subtopology ?A {y ∈ topspace ?A. 1 / 2 ≤ snd y}) euclideanreal
            (λt. 2 * (snd t :: real) - 1)"
          using snd_cont by (intro continuous_intros)
        have affine_range:
          "(λt. 2 * (snd t :: real) - 1) ∈
            topspace (subtopology ?A {y ∈ topspace ?A. 1 / 2 ≤ snd y}) → {0..1}"
        proof
          fix t :: "real × real"
          assume t_in: "t ∈ topspace (subtopology ?A {y ∈ topspace ?A. 1 / 2 ≤ snd y})"
          then have tA: "t ∈ topspace ?A" and t_half: "1 / 2 ≤ snd t"
            by auto
          have snd01: "snd t ∈ {0..1}"
            using tA by (auto simp: topspace_prod_topology)
          from snd01 have snd_ge0: "0 ≤ snd t" and snd_le1: "snd t ≤ 1"
            by auto
          have lower: "0 ≤ 2 * (snd t :: real) - 1"
            using t_half by linarith
          have upper: "2 * (snd t :: real) - 1 ≤ 1"
            using snd_le1 by linarith
          show "2 * (snd t :: real) - 1 ∈ {0..1}"
            using lower upper by (auto simp: atLeastAtMost_iff)
        qed
        show ?thesis
          by (rule continuous_map_into_subtopology[OF affine_cont affine_range])
      qed
    qed
    have right_comp:
      "continuous_map (subtopology ?A {y ∈ topspace ?A. 1 / 2 ≤ snd y}) X
        (((λy. q (fst y) (snd y)) ∘ (λy. (fst y, 2 * snd y - 1))))"
      by (rule continuous_map_compose[OF right_pair_cont q])
    show "continuous_map (subtopology ?A {y ∈ topspace ?A. 1 / 2 ≤ snd y}) X
            (λt. q (fst t) (2 * snd t - 1))"
      using right_comp by (simp add: o_def)
    show "p (fst y) (2 * snd y) = q (fst y) (2 * snd y - 1)"
      if "y ∈ topspace ?A" "snd y = 1 / 2" for y
    proof -
      have fst01: "fst y ∈ {0..1}"
        using that(1) by (auto simp: topspace_prod_topology)
      have mid1: "2 * snd y = 1"
        using that(2) by simp
      have mid0: "2 * snd y - 1 = 0"
        using that(2) by simp
      have "p (fst y) 1 = q (fst y) 0"
        by (rule pq[OF fst01])
      then show ?thesis
        using mid1 mid0 by simp
    qed
  qed
qed

lemma homotopic_pathsin_continuous_image:
  assumes pq: "homotopic_pathsin X p q"
    and h: "continuous_map X Y f"
  shows "homotopic_pathsin Y (f ∘ p) (f ∘ q)"
proof -
  have pq': "homotopic_with (λr. r 0 = p 0 ∧ r 1 = p 1) (top_of_set {0..1}) X p q"
    using pq unfolding homotopic_pathsin_def .
  show ?thesis
    unfolding homotopic_pathsin_def
     by (rule homotopic_with_compose_continuous_map_left[OF pq' h]) simp
qed

lemma homotopic_pathsin_reversepathin_D:
  assumes "homotopic_pathsin X p q"
  shows "homotopic_pathsin X (reversepathin p) (reversepathin q)"
proof -
  have rev_cont: "continuous_map (top_of_set {0..1}) (top_of_set {0..1}) (λt::real. 1 - t)"
    by (intro continuous_map_into_subtopology continuous_intros) auto
  have pq':
    "homotopic_with (λr. r 0 = p 0 ∧ r 1 = p 1) (top_of_set {0..1}) X p q"
    using assms unfolding homotopic_pathsin_def .
  have "homotopic_with (λr. r 0 = reversepathin p 0 ∧ r 1 = reversepathin p 1)
      (top_of_set {0..1}) X (p ∘ (λt::real. 1 - t)) (q ∘ (λt::real. 1 - t))"
  proof (rule homotopic_with_compose_continuous_map_right[OF pq' rev_cont])
    fix j :: "real ⇒ 'a"
    assume j_end: "j 0 = p 0 ∧ j 1 = p 1"
    show "(λr. r 0 = reversepathin p 0 ∧ r 1 = reversepathin p 1)
        (j ∘ (λt::real. 1 - t))"
      using j_end by (simp add: reversepathin_def)
  qed
  then show ?thesis
    unfolding homotopic_pathsin_def reversepathin_def o_def .
qed

lemma homotopic_pathsin_reversepathin:
  "homotopic_pathsin X (reversepathin p) (reversepathin q) ⟷ homotopic_pathsin X p q"
  using homotopic_pathsin_reversepathin_D by force

lemma homotopic_pathsin_joinpathin:
  assumes pp': "homotopic_pathsin X p p'"
    and qq': "homotopic_pathsin X q q'"
    and pq: "p 1 = q 0"
  shows "homotopic_pathsin X (joinpathin p q) (joinpathin p' q')"
proof -
  let ?T01 = "subtopology euclideanreal {0..1}"
  let ?A = "prod_topology ?T01 ?T01"
  obtain h1 :: "real × real ⇒ 'a" where
      h1_cont: "continuous_map (prod_topology (top_of_set {0..1}) (top_of_set {0..1})) X h1"
    and h1_0: "∀x. h1 (0, x) = p x"
    and h1_1: "∀x. h1 (1, x) = p' x"
    and h1_prop: "∀t∈{0..1}. h1 (t, 0) = p 0 ∧ h1 (t, 1) = p 1"
    using pp' unfolding homotopic_pathsin_def homotopic_with_def by auto
  obtain h2 :: "real × real ⇒ 'a" where
      h2_cont: "continuous_map (prod_topology (top_of_set {0..1}) (top_of_set {0..1})) X h2"
    and h2_0: "∀x. h2 (0, x) = q x"
    and h2_1: "∀x. h2 (1, x) = q' x"
    and h2_prop: "∀t∈{0..1}. h2 (t, 0) = q 0 ∧ h2 (t, 1) = q 1"
    using qq' unfolding homotopic_pathsin_def homotopic_with_def by auto
  define k1 where "k1 t x = h1 (t, x)" for t x
  define k2 where "k2 t x = h2 (t, x)" for t x
  have k1_cont: "continuous_map ?A X (λy. k1 (fst y) (snd y))"
  proof -
    have "(λy. k1 (fst y) (snd y)) = h1"
      unfolding k1_def by (auto simp: fun_eq_iff)
    then show ?thesis
      using h1_cont by simp
  qed
  have k2_cont: "continuous_map ?A X (λy. k2 (fst y) (snd y))"
  proof -
    have "(λy. k2 (fst y) (snd y)) = h2"
      unfolding k2_def by (auto simp: fun_eq_iff)
    then show ?thesis
      using h2_cont by simp
  qed
  have k1_0: "∀x. k1 0 x = p x"
    unfolding k1_def using h1_0 by simp
  have k1_1: "∀x. k1 1 x = p' x"
    unfolding k1_def using h1_1 by simp
  have k2_0: "∀x. k2 0 x = q x"
    unfolding k2_def using h2_0 by simp
  have k2_1: "∀x. k2 1 x = q' x"
    unfolding k2_def using h2_1 by simp
  have k1_prop: "∀t∈{0..1}. k1 t 0 = p 0 ∧ k1 t 1 = p 1"
    unfolding k1_def using h1_prop by simp
  have k2_prop: "∀t∈{0..1}. k2 t 0 = q 0 ∧ k2 t 1 = q 1"
    unfolding k2_def using h2_prop by simp
  have mid_eq: "k1 t 1 = k2 t 0" if "t ∈ {0..1}" for t
    using k1_prop[rule_format, OF that] k2_prop[rule_format, OF that] pq by auto
  show ?thesis
    unfolding homotopic_pathsin_def homotopic_with_def
  proof (rule exI[where x = "λy. joinpathin (k1 (fst y)) (k2 (fst y)) (snd y)"], intro conjI)
    show "continuous_map ?A X (λy. joinpathin (k1 (fst y)) (k2 (fst y)) (snd y))"
      by (rule continuous_map_homotopic_joinpathin_lemma[OF k1_cont k2_cont]) (rule mid_eq)
    show "∀x::real. (λy. joinpathin (k1 (fst y)) (k2 (fst y)) (snd y)) (0, x) = joinpathin p q x"
    proof
      fix x :: real
      show "(λy. joinpathin (k1 (fst y)) (k2 (fst y)) (snd y)) (0, x) = joinpathin p q x"
        using k1_0 k2_0 by (cases "x ≤ 1 / 2") (auto simp: joinpathin_def)
    qed
    show "∀x::real. (λy. joinpathin (k1 (fst y)) (k2 (fst y)) (snd y)) (1, x) = joinpathin p' q' x"
    proof
      fix x :: real
      show "(λy. joinpathin (k1 (fst y)) (k2 (fst y)) (snd y)) (1, x) = joinpathin p' q' x"
        using k1_1 k2_1 by (cases "x ≤ 1 / 2") (auto simp: joinpathin_def)
    qed
    show "∀t∈{0..1}. (λr. r 0 = joinpathin p q 0 ∧ r 1 = joinpathin p q 1)
          (λx. (λy. joinpathin (k1 (fst y)) (k2 (fst y)) (snd y)) (t, x))"
    proof
      fix t :: real
      assume t: "t ∈ {0..1}"
      have k1t0: "k1 t 0 = p 0"
        using k1_prop[rule_format, OF t] by auto
      have k2t1: "k2 t 1 = q 1"
        using k2_prop[rule_format, OF t] by auto
      show "(λr. r 0 = joinpathin p q 0 ∧ r 1 = joinpathin p q 1)
            (λx. (λy. joinpathin (k1 (fst y)) (k2 (fst y)) (snd y)) (t, x))"
        using k1t0 k2t1 by (simp add: joinpathin_def)
    qed
  qed
qed

lemma homotopic_pathsin_reparametrize:
  assumes p: "pathin X p"
    and contf: "continuous_map (top_of_set {0..1}) (top_of_set {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_pathsin X p q"
proof -
  have pf: "pathin X (p ∘ f)"
    using contf p unfolding pathin_def by (rule continuous_map_compose)
  have qf': "homotopic_pathsin X (p ∘ f) q"
    using pf q by (intro homotopic_pathsin_eq) auto
  have qf: "homotopic_pathsin X q (p ∘ f)"
    by (rule homotopic_pathsin_sym[OF qf'])
  have fp: "homotopic_pathsin X (p ∘ f) p"
    unfolding homotopic_pathsin_def homotopic_with_def
  proof (rule exI[where x = "p ∘ (λy. (1 - fst y) * ((f ∘ snd) y) + fst y * snd y)"], intro conjI)
    have snd_cont:
      "continuous_map (prod_topology (top_of_set {0..1}) (top_of_set {0..1}))
        (top_of_set {0..1}) snd"
      by (rule continuous_map_snd)
    have fst_cont:
      "continuous_map (prod_topology (top_of_set {0..1}) (top_of_set {0..1}))
        (top_of_set {0..1}) fst"
      by (rule continuous_map_fst)
    have fsnd_cont:
      "continuous_map (prod_topology (top_of_set {0..1}) (top_of_set {0..1}))
        (top_of_set {0..1}) (f ∘ snd)"
      by (rule continuous_map_compose[OF snd_cont contf])
    have param_cont_eu:
      "continuous_map (prod_topology (top_of_set {0..1}) (top_of_set {0..1})) euclideanreal
        (λy. (1 - fst y) * ((f ∘ snd) y) + fst y * snd y)"
      using fst_cont snd_cont fsnd_cont
      by (intro continuous_intros
          continuous_map_into_fulltopology[OF fst_cont]
          continuous_map_into_fulltopology[OF snd_cont]
          continuous_map_into_fulltopology[OF fsnd_cont])
    have param_range:
      "(λy. (1 - fst y) * ((f ∘ snd) y) + fst y * snd y) ∈
        topspace (prod_topology (top_of_set {0..1}) (top_of_set {0..1})) → {0..1}"
    proof
      fix y :: "real × real"
      assume y_in: "y ∈ topspace (prod_topology (top_of_set {0..1}) (top_of_set {0..1}))"
      have fst01: "fst y ∈ {0..1}" and snd01: "snd y ∈ {0..1}"
        using y_in by (auto simp: topspace_prod_topology)
      have fsnd01: "f (snd y) ∈ {0..1}"
        using f01 snd01 by auto
      have nonneg: "0 ≤ (1 - fst y) * (f (snd y)) + fst y * snd y"
        using fst01 snd01 fsnd01 by (intro add_nonneg_nonneg mult_nonneg_nonneg) auto
      moreover have le1: "(1 - fst y) * (f (snd y)) + fst y * snd y ≤ 1"
        using fst01 snd01 fsnd01 by (intro convex_bound_le) auto
      ultimately show "((1 - fst y) * ((f ∘ snd) y) + fst y * snd y) ∈ {0..1}"
        by simp
    qed
    have param_cont:
      "continuous_map (prod_topology (top_of_set {0..1}) (top_of_set {0..1}))
        (top_of_set {0..1}) (λy. (1 - fst y) * ((f ∘ snd) y) + fst y * snd y)"
      using param_cont_eu param_range by (simp add: continuous_map_in_subtopology)
    show "continuous_map
            (prod_topology (top_of_set {0..1}) (top_of_set {0..1})) X
            (p ∘ (λy. (1 - fst y) * ((f ∘ snd) y) + fst y * snd y))"
      using p unfolding pathin_def by (rule continuous_map_compose[OF param_cont])
    show "∀x::real. (p ∘ (λy. (1 - fst y) * ((f ∘ snd) y) + fst y * snd y)) (0, x) = (p ∘ f) x"
    proof
      fix x :: real
      show "(p ∘ (λy. (1 - fst y) * ((f ∘ snd) y) + fst y * snd y)) (0, x) = (p ∘ f) x"
        by (simp add: o_def algebra_simps)
    qed
    show "∀x::real. (p ∘ (λy. (1 - fst y) * ((f ∘ snd) y) + fst y * snd y)) (1, x) = p x"
    proof
      fix x :: real
      show "(p ∘ (λy. (1 - fst y) * ((f ∘ snd) y) + fst y * snd y)) (1, x) = p x"
        by (simp add: o_def algebra_simps)
    qed
    show "∀t∈{0..1}. (λr. r 0 = (p ∘ f) 0 ∧ r 1 = (p ∘ f) 1)
          (λx. (p ∘ (λy. (1 - fst y) * ((f ∘ snd) y) + fst y * snd y)) (t, x))"
    proof
      fix t :: real
      assume t: "t ∈ {0..1}"
      show "(λr. r 0 = (p ∘ f) 0 ∧ r 1 = (p ∘ f) 1)
          (λx::real. (p ∘ (λy. (1 - fst y) * ((f ∘ snd) y) + fst y * snd y)) (t, x))"
      proof -
        have end0: "(λx::real. (p ∘ (λy. (1 - fst y) * ((f ∘ snd) y) + fst y * snd y)) (t, x)) 0 = (p ∘ f) 0"
          by (simp add: o_def algebra_simps)
        have end1: "(λx::real. (p ∘ (λy. (1 - fst y) * ((f ∘ snd) y) + fst y * snd y)) (t, x)) 1 = (p ∘ f) 1"
          by (simp add: o_def algebra_simps)
        from end0 end1 show ?thesis
          by (simp add: o_def)
      qed
    qed
  qed
  have "homotopic_pathsin X q p"
    by (rule homotopic_pathsin_trans[OF qf fp])
  then show ?thesis
    by (rule homotopic_pathsin_sym)
qed

lemma homotopic_pathsin_rid_const:
  assumes p: "pathin X p"
  shows "homotopic_pathsin X (joinpathin p (λ_. p 1)) p"
proof -
  have contf: "continuous_map (top_of_set {0..1}) (top_of_set {0..1})
                 (λt::real. if t ≤ 1 / 2 then 2 * t else 1)"
  proof (rule continuous_map_into_subtopology)
    show "continuous_map (top_of_set {0..1}) euclideanreal
            (λt::real. if t ≤ 1 / 2 then 2 * t else 1)"
    proof (rule continuous_map_cases_le[where p = "λt::real. t" and q = "λ_. 1 / 2"])
      show "continuous_map (top_of_set {0..1}) euclideanreal (λt::real. t)"
        by (simp add: continuous_map_iff_continuous)
      show "continuous_map (top_of_set {0..1}) euclideanreal (λ_. 1 / 2)"
        by simp
      show "continuous_map (subtopology (top_of_set {0..1}) {x ∈ topspace (top_of_set {0..1}). x ≤ 1 / 2})
              euclideanreal (λt::real. 2 * t)"
      proof -
        have "continuous_map (top_of_set {0..1}) euclideanreal (λt::real. 2 * t)"
          by (simp add: continuous_map_iff_continuous continuous_intros)
        then show ?thesis
          by (rule continuous_map_from_subtopology)
      qed
      show "continuous_map (subtopology (top_of_set {0..1}) {x ∈ topspace (top_of_set {0..1}). 1 / 2 ≤ x})
              euclideanreal (λ_::real. 1)"
        by simp
      show "2 * x = (1::real)" if "x ∈ topspace (top_of_set {0..1})" "x = 1 / 2" for x
        using that by simp
    qed
    show "(λt::real. if t ≤ 1 / 2 then 2 * t else 1) ∈ topspace (top_of_set {0..1}) → {0..1}"
      by auto
  qed
  show ?thesis
    apply (rule homotopic_pathsin_sym)
    apply (rule homotopic_pathsin_reparametrize[where f = "λt::real. if t ≤ 1 / 2 then 2 * t else 1"])
    using p contf
    apply (auto simp: joinpathin_def)
    done
qed

lemma homotopic_pathsin_lid_const:
  assumes p: "pathin X p"
  shows "homotopic_pathsin X (joinpathin (λ_. p 0) p) p"
proof -
  have contf: "continuous_map (top_of_set {0..1}) (top_of_set {0..1})
                 (λt::real. if t ≤ 1 / 2 then 0 else 2 * t - 1)"
  proof (rule continuous_map_into_subtopology)
    show "continuous_map (top_of_set {0..1}) euclideanreal
            (λt::real. if t ≤ 1 / 2 then 0 else 2 * t - 1)"
    proof (rule continuous_map_cases_le[where p = "λt::real. t" and q = "λ_. 1 / 2"])
      show "continuous_map (top_of_set {0..1}) euclideanreal (λt::real. t)"
        by (simp add: continuous_map_iff_continuous)
      show "continuous_map (top_of_set {0..1}) euclideanreal (λ_. 1 / 2)"
        by simp
      show "continuous_map (subtopology (top_of_set {0..1}) {x ∈ topspace (top_of_set {0..1}). x ≤ 1 / 2})
              euclideanreal (λ_::real. 0)"
        by simp
      show "continuous_map (subtopology (top_of_set {0..1}) {x ∈ topspace (top_of_set {0..1}). 1 / 2 ≤ x})
              euclideanreal (λt::real. 2 * t - 1)"
      proof -
        have "continuous_map (top_of_set {0..1}) euclideanreal (λt::real. 2 * t - 1)"
          by (simp add: continuous_map_iff_continuous continuous_intros)
        then show ?thesis
          by (rule continuous_map_from_subtopology)
      qed
      show "(0::real) = 2 * x - 1" if "x ∈ topspace (top_of_set {0..1})" "x = 1 / 2" for x
        using that by simp
    qed
    show "(λt::real. if t ≤ 1 / 2 then 0 else 2 * t - 1) ∈ topspace (top_of_set {0..1}) → {0..1}"
      by auto
  qed
  show ?thesis
    apply (rule homotopic_pathsin_sym)
    apply (rule homotopic_pathsin_reparametrize[where f = "λt::real. if t ≤ 1 / 2 then 0 else 2 * t - 1"])
    using p contf
    apply (auto simp: joinpathin_def)
    done
qed

lemma homotopic_pathsin_assoc:
  assumes p: "pathin X p"
    and q: "pathin X q"
    and r: "pathin X r"
    and pq: "p 1 = q 0"
    and qr: "q 1 = r 0"
  shows "homotopic_pathsin X (joinpathin p (joinpathin q r)) (joinpathin (joinpathin p q) r)"
proof -
  let ?f = "λt::real. if t ≤ 1 / 2 then inverse 2 * t else if t ≤ 3 / 4 then t - 1 / 4 else 2 * t - 1"
  have contf_on: "continuous_on {0..1} ?f"
  proof (rule continuous_on_cases_1)
    show "continuous_on {t ∈ {0..1}. t ≤ 1 / 2} (λt::real. inverse 2 * t)"
      by (intro continuous_intros)
    show "continuous_on {t ∈ {0..1}. 1 / 2 ≤ t}
            (λt::real. if t ≤ 3 / 4 then t - 1 / 4 else 2 * t - 1)"
    proof (rule continuous_on_cases_1)
      show "continuous_on {t ∈ {t ∈ {0..1}. 1 / 2 ≤ t}. t ≤ 3 / 4} (λt::real. t - 1 / 4)"
        by (intro continuous_intros)
      show "continuous_on {t ∈ {t ∈ {0..1}. 1 / 2 ≤ t}. 3 / 4 ≤ t} (λt::real. 2 * t - 1)"
        by (intro continuous_intros)
      show "(3 / 4::real) ∈ {t ∈ {0..1}. (1 / 2::real) ≤ t} ⟹
          (3 / 4::real) - 1 / 4 = 2 * (3 / 4) - 1"
        by simp
    qed
    show "(1 / 2::real) ∈ {0..1} ⟹
        inverse 2 * (1 / 2::real) =
          (if (1 / 2::real) ≤ 3 / 4 then 1 / 2 - 1 / 4 else 2 * (1 / 2) - 1)"
      by simp
  qed
  have contf_eu: "continuous_map (top_of_set {0..1}) euclideanreal ?f"
    using contf_on by simp
  have contf:
    "continuous_map (top_of_set {0..1}) (top_of_set {0..1}) ?f"
    using contf_eu by (rule continuous_map_into_subtopology) auto
  have join_pq: "pathin X (joinpathin p q)"
    by (rule pathin_joinpathin[OF p q pq])
  have join_qr: "pathin X (joinpathin q r)"
    by (rule pathin_joinpathin[OF q r qr])
  have join_pq_end: "joinpathin p q 1 = r 0"
    using qr by (simp add: joinpathin_def)
  have join_pq_r: "pathin X (joinpathin (joinpathin p q) r)"
    by (rule pathin_joinpathin[OF join_pq r join_pq_end])
  have join_pq_r_expanded:
    "pathin X (λt. if t * 2 ≤ 1
        then if 2 * t * 2 ≤ 1 then p (2 * (2 * t)) else q (2 * (2 * t) - 1)
        else r (2 * t - 1))"
    using join_pq_r by (simp add: joinpathin_def)
  show ?thesis
    apply (rule homotopic_pathsin_sym)
    apply (rule homotopic_pathsin_reparametrize[
        where f = ?f])
    using contf join_pq_r_expanded join_pq_r join_pq r qr join_qr p q pq
    apply (auto simp: joinpathin_def field_simps algebra_simps)
    apply (rule arg_cong[where f = q])
    apply (simp add: field_simps)
    done
qed

lemma homotopic_pathsin_rinv_const:
  assumes p: "pathin X p"
  shows "homotopic_pathsin X (joinpathin p (reversepathin p)) (λ_. p 0)"
proof -
  let ?T01 = "subtopology euclideanreal {0..1}"
  let ?A = "prod_topology ?T01 ?T01"
  let ?h =
    "λy. if snd y ≤ 1 / 2
      then p (fst y * (2 * snd y))
      else p (fst y * (1 - (2 * snd y - 1)))"
  have p_cont: "continuous_map ?T01 X p"
    using p unfolding pathin_def .
  have h_cont: "continuous_map ?A X ?h"
  proof (rule continuous_map_cases_le)
    show "continuous_map ?A euclideanreal snd"
      by (rule continuous_map_into_fulltopology[OF continuous_map_snd])
    show "continuous_map ?A euclideanreal (λ_. 1 / 2)"
      by simp
    have left_param_cont_eu:
      "continuous_map (subtopology ?A {y ∈ topspace ?A. snd y ≤ 1 / 2}) euclideanreal
        (λt. fst t * (2 * snd t))"
      by (intro continuous_intros
          continuous_map_into_fulltopology[OF continuous_map_subtopology_fst]
          continuous_map_into_fulltopology[OF continuous_map_subtopology_snd])
    have left_param_cont:
      "continuous_map (subtopology ?A {y ∈ topspace ?A. snd y ≤ 1 / 2}) ?T01
        (λt. fst t * (2 * snd t))"
    proof -
      have left_param_range:
        "(λt. fst t * (2 * snd t)) ∈
          topspace (subtopology ?A {y ∈ topspace ?A. snd y ≤ 1 / 2}) → {0..1}"
      proof
        fix t :: "real × real"
        assume t_in: "t ∈ topspace (subtopology ?A {y ∈ topspace ?A. snd y ≤ 1 / 2})"
        then have tA: "t ∈ topspace ?A" and t_half: "snd t ≤ 1 / 2"
          by auto
        have fst01: "fst t ∈ {0..1}" and snd01: "snd t ∈ {0..1}"
          using tA by (auto simp: topspace_prod_topology)
        from snd01 have snd_ge0: "0 ≤ snd t" and snd_le1: "snd t ≤ 1"
          by auto
        have scale01: "2 * (snd t :: real) ∈ {0..1}"
        proof -
          have lower: "0 ≤ 2 * (snd t :: real)"
            using snd_ge0 by linarith
          have upper: "2 * (snd t :: real) ≤ 1"
            using t_half by linarith
          show "2 * (snd t :: real) ∈ {0..1}"
            using lower upper by auto
        qed
        show "fst t * (2 * (snd t :: real)) ∈ {0..1}"
        proof - 
          from fst01 have fst_ge0: "0 ≤ fst t" and fst_le1: "fst t ≤ 1"
            by auto
          from scale01 have scale_ge0: "0 ≤ 2 * (snd t :: real)" and scale_le1: "2 * (snd t :: real) ≤ 1"
            by auto
          have lower: "0 ≤ fst t * (2 * (snd t :: real))"
            by (rule mult_nonneg_nonneg[OF fst_ge0 scale_ge0])
          have upper: "fst t * (2 * (snd t :: real)) ≤ 1"
            by (rule mult_le_one[OF fst_le1 scale_ge0 scale_le1])
          have bounds:
            "0 ≤ fst t * (2 * (snd t :: real)) ∧ fst t * (2 * (snd t :: real)) ≤ 1"
            using lower upper by blast
          show "fst t * (2 * (snd t :: real)) ∈ {0..1}"
          proof -
            from bounds have lower': "0 ≤ fst t * (2 * (snd t :: real))"
              and upper': "fst t * (2 * (snd t :: real)) ≤ 1"
              by auto
            show ?thesis
              using lower' upper' by (auto simp: atLeastAtMost_iff)
          qed
        qed
      qed
      show ?thesis
        by (rule continuous_map_into_subtopology[OF left_param_cont_eu left_param_range])
    qed
    show "continuous_map (subtopology ?A {y ∈ topspace ?A. snd y ≤ 1 / 2}) X
            (λt. p (fst t * (2 * snd t)))"
    proof -
      have left_comp:
        "continuous_map (subtopology ?A {y ∈ topspace ?A. snd y ≤ 1 / 2}) X
          (p ∘ (λt. fst t * (2 * snd t)))"
        by (rule continuous_map_compose[OF left_param_cont p_cont])
      have left_eq: "(λt. p (fst t * (2 * snd t))) = p ∘ (λt. fst t * (2 * snd t))"
        by (auto simp: fun_eq_iff)
      show ?thesis
        using left_comp left_eq by simp
    qed
    have right_param_cont_eu:
      "continuous_map (subtopology ?A {y ∈ topspace ?A. 1 / 2 ≤ snd y}) euclideanreal
        (λt. fst t * (1 - (2 * snd t - 1)))"
      by (intro continuous_intros
          continuous_map_into_fulltopology[OF continuous_map_subtopology_fst]
          continuous_map_into_fulltopology[OF continuous_map_subtopology_snd])
    have right_param_cont:
      "continuous_map (subtopology ?A {y ∈ topspace ?A. 1 / 2 ≤ snd y}) ?T01
        (λt. fst t * (1 - (2 * snd t - 1)))"
    proof -
      have right_param_range:
        "(λt. fst t * (1 - (2 * snd t - 1))) ∈
          topspace (subtopology ?A {y ∈ topspace ?A. 1 / 2 ≤ snd y}) → {0..1}"
      proof
        fix t :: "real × real"
        assume t_in: "t ∈ topspace (subtopology ?A {y ∈ topspace ?A. 1 / 2 ≤ snd y})"
        then have tA: "t ∈ topspace ?A" and t_half: "1 / 2 ≤ snd t"
          by auto
        have fst01: "fst t ∈ {0..1}" and snd01: "snd t ∈ {0..1}"
          using tA by (auto simp: topspace_prod_topology)
        from snd01 have snd_ge0: "0 ≤ snd t" and snd_le1: "snd t ≤ 1"
          by auto
        have scale01: "1 - (2 * (snd t :: real) - 1) ∈ {0..1}"
        proof -
          have lower: "0 ≤ 1 - (2 * (snd t :: real) - 1)"
            using snd_le1 by linarith
          have upper: "1 - (2 * (snd t :: real) - 1) ≤ 1"
            using t_half by linarith
          show "1 - (2 * (snd t :: real) - 1) ∈ {0..1}"
            using lower upper by force
        qed
        show "fst t * (1 - (2 * (snd t :: real) - 1)) ∈ {0..1}"
        proof - 
          from fst01 have fst_ge0: "0 ≤ fst t" and fst_le1: "fst t ≤ 1"
            by auto
          from scale01 have scale_ge0: "0 ≤ 1 - (2 * (snd t :: real) - 1)"
            and scale_le1: "1 - (2 * (snd t :: real) - 1) ≤ 1"
            by auto
          have lower: "0 ≤ fst t * (1 - (2 * (snd t :: real) - 1))"
            by (rule mult_nonneg_nonneg[OF fst_ge0 scale_ge0])
          have upper: "fst t * (1 - (2 * (snd t :: real) - 1)) ≤ 1"
            by (rule mult_le_one[OF fst_le1 scale_ge0 scale_le1])
          show "fst t * (1 - (2 * (snd t :: real) - 1)) ∈ {0..1}"
            using lower upper by force
        qed
      qed
      show ?thesis
        using right_param_cont_eu right_param_range by (simp add: continuous_map_in_subtopology)
    qed
    show "continuous_map (subtopology ?A {y ∈ topspace ?A. 1 / 2 ≤ snd y}) X
            (λt. p (fst t * (1 - (2 * snd t - 1))))"
    proof -
      have right_comp:
        "continuous_map (subtopology ?A {y ∈ topspace ?A. 1 / 2 ≤ snd y}) X
          (p ∘ (λt. fst t * (1 - (2 * snd t - 1))))"
        by (rule continuous_map_compose[OF right_param_cont p_cont])
      have right_eq:
        "(λt. p (fst t * (1 - (2 * snd t - 1)))) =
          p ∘ (λt. fst t * (1 - (2 * snd t - 1)))"
        by (auto simp: fun_eq_iff)
      show ?thesis
        using right_comp right_eq by simp
    qed
    show "p (fst y * (2 * snd y)) = p (fst y * (1 - (2 * snd y - 1)))"
      if "y ∈ topspace ?A" "snd y = 1 / 2" for y
    proof -
      have mid1: "2 * snd y = (1::real)"
        using that(2) by simp
      have mid0: "2 * snd y - 1 = (0::real)"
        using that(2) by simp
      show ?thesis
        using mid1 mid0 by simp
    qed
  qed
  have hom_const_join: "homotopic_pathsin X (λ_. p 0) (joinpathin p (reversepathin p))"
    unfolding homotopic_pathsin_def homotopic_with_def
  proof (rule exI[where x = ?h], intro conjI)
    show "continuous_map ?A X ?h"
      by (rule h_cont)
    show "∀x::real. ?h (0, x) = (λ_. p 0) x"
      by simp
    show "∀x::real. ?h (1, x) = joinpathin p (reversepathin p) x"
      by (auto simp: joinpathin_def reversepathin_def)
    show "∀t∈{0..1}. (λr. r 0 = p 0 ∧ r 1 = p 0) (λx. ?h (t, x))"
      by simp
  qed
  show ?thesis
    by (rule homotopic_pathsin_sym[OF hom_const_join])
qed

lemma homotopic_pathsin_linv_const:
  assumes p: "pathin X p"
  shows "homotopic_pathsin X (joinpathin (reversepathin p) p) (λ_. p 1)"
proof -
  have "homotopic_pathsin X (joinpathin (reversepathin p) (reversepathin (reversepathin p)))
      (λ_. reversepathin p 0)"
    using pathin_reversepathin[OF p] by (rule homotopic_pathsin_rinv_const)
  then show ?thesis
    by (simp add: reversepathin_def)
qed

lemma homotopic_loopsin_imp_pathin:
  assumes "homotopic_loopsin X p q"
  shows "pathin X p" "pathin X q"
  using assms unfolding homotopic_loopsin_def pathin_def
  by (auto dest: homotopic_with_imp_continuous_maps)

lemma homotopic_loopsin_imp_loop:
  assumes "homotopic_loopsin X p q"
  shows "p 1 = p 0" "q 1 = q 0"
  using assms unfolding homotopic_loopsin_def
  by (auto dest: homotopic_with_imp_property)

lemma homotopic_loopsin_refl [simp]:
  "homotopic_loopsin X p p ⟷ pathin X p ∧ p 1 = p 0"
  unfolding homotopic_loopsin_def pathin_def
  by (simp add: homotopic_with_refl)

lemma homotopic_loopsin_sym:
  assumes "homotopic_loopsin X p q"
  shows "homotopic_loopsin X q p"
  using assms unfolding homotopic_loopsin_def
  by (simp add: homotopic_with_sym)

lemma homotopic_loopsin_trans:
  assumes "homotopic_loopsin X p q"
    and "homotopic_loopsin X q r"
  shows "homotopic_loopsin X p r"
  using assms unfolding homotopic_loopsin_def
  by (blast intro: homotopic_with_trans)

lemma loopin_space_reversepathin:
  assumes "p ∈ loopin_space X x"
  shows "reversepathin p ∈ loopin_space X x"
proof -
  from assms obtain p_in where p_in: "pathin X p" "p 0 = x" "p 1 = x"
    by (rule loopin_spaceE)
  have path_rev: "pathin X (reversepathin p)"
    using p_in(1) by (rule pathin_reversepathin)
  have start_rev: "reversepathin p 0 = x"
    using p_in(3) by (simp add: reversepathin_def)
  have finish_rev: "reversepathin p 1 = x"
    using p_in(2) by (simp add: reversepathin_def)
  show ?thesis
    unfolding loopin_space_def using path_rev start_rev finish_rev by blast
qed

end