(*
  Material originally from HOL Light, ported by Larry Paulson, moved here by Manuel Eberl
*)
section✐‹tag unimportant› ‹Smooth paths›
theory Smooth_Paths
  imports Retracts
begin

subsection✐‹tag unimportant› ‹Homeomorphisms of arc images›

lemma path_connected_arc_complement:
  fixes γ :: "real → 'a::euclidean_space"
  assumes "arc γ" "2 ≤ DIM('a)"
  shows "path_connected(- path_image γ)"
proof -
  have "path_image γ homeomorphic {0..1::real}"
    by (simp add: assms homeomorphic_arc_image_interval)
  then show ?thesis
    by (intro path_connected_complement_homeomorphic_convex_compact) (auto simp: assms)
qed

lemma connected_arc_complement:
  fixes γ :: "real → 'a::euclidean_space"
  assumes "arc γ" "2 ≤ DIM('a)"
  shows "connected(- path_image γ)"
  by (simp add: assms path_connected_arc_complement path_connected_imp_connected)

lemma inside_arc_empty:
  fixes γ :: "real → 'a::euclidean_space"
  assumes "arc γ"
    shows "inside(path_image γ) = {}"
proof (cases "DIM('a) = 1")
  case True
  then show ?thesis
    using assms connected_arc_image connected_convex_1_gen inside_convex by blast
next
  case False
  then have "connected (- path_image γ)"
      by (metis DIM_ge_Suc0 One_nat_def Suc_1 antisym assms connected_arc_complement not_less_eq_eq)
    then
  show ?thesis
    by (simp add: assms bounded_arc_image inside_bounded_complement_connected_empty)
qed

lemma inside_simple_curve_imp_closed:
  fixes γ :: "real → 'a::euclidean_space"
    shows "[simple_path γ; x ∈ inside(path_image γ)] ==> pathfinish γ = pathstart γ"
  using arc_simple_path  inside_arc_empty by blast


subsection ‹Piecewise differentiability of paths›

lemma continuous_on_joinpaths_D1:
  assumes "continuous_on {0..1} (g1 +++ g2)"
  shows "continuous_on {0..1} g1"
proof (rule continuous_on_eq)
  have "continuous_on {0..1/2} (g1 +++ g2)"
    using assms continuous_on_subset split_01 by auto
  then show "continuous_on {0..1} (g1 +++ g2 ∘ (*) (inverse 2))"
    by (intro continuous_intros) force
qed (auto simp: joinpaths_def)

lemma continuous_on_joinpaths_D2:
    "[continuous_on {0..1} (g1 +++ g2); pathfinish g1 = pathstart g2] ==> continuous_on {0..1} g2"
  using path_def path_join by blast

lemma piecewise_differentiable_D1:
  assumes "(g1 +++ g2) piecewise_differentiable_on {0..1}"
  shows "g1 piecewise_differentiable_on {0..1}"
proof -
  obtain S where cont: "continuous_on {0..1} g1" and "finite S"
    and S: "∧x. x ∈ {0..1} - S ==> g1 +++ g2 differentiable at x within {0..1}"
    using assms unfolding piecewise_differentiable_on_def
    by (blast dest!: continuous_on_joinpaths_D1)
  show ?thesis
    unfolding piecewise_differentiable_on_def
  proof (intro exI conjI ballI cont)
    show "finite (insert 1 (((*)2) ` S))"
      by (simp add: ‹finite S›)
    show "g1 differentiable at x within {0..1}" if "x ∈ {0..1} - insert 1 ((*) 2 ` S)" for x
    proof (rule_tac d="dist (x/2) (1/2)" in differentiable_transform_within)
      have "g1 +++ g2 differentiable at (x / 2) within {0..1/2}"
        by (rule differentiable_subset [OF S [of "x/2"]] | use that in force)+
      then show "g1 +++ g2 ∘ (*) (inverse 2) differentiable at x within {0..1}"
        using image_affinity_atLeastAtMost_div [of 2 0 "0::real" 1]
        by (auto intro: differentiable_chain_within)
    qed (use that in ‹auto simp: joinpaths_def›)
  qed
qed

lemma piecewise_differentiable_D2:
  assumes "(g1 +++ g2) piecewise_differentiable_on {0..1}" and eq: "pathfinish g1 = pathstart g2"
  shows "g2 piecewise_differentiable_on {0..1}"
proof -
  have [simp]: "g1 1 = g2 0"
    using eq by (simp add: pathfinish_def pathstart_def)
  obtain S where cont: "continuous_on {0..1} g2" and "finite S"
    and S: "∧x. x ∈ {0..1} - S ==> g1 +++ g2 differentiable at x within {0..1}"
    using assms unfolding piecewise_differentiable_on_def
    by (blast dest!: continuous_on_joinpaths_D2)
  show ?thesis
    unfolding piecewise_differentiable_on_def
  proof (intro exI conjI ballI cont)
    show "finite (insert 0 ((λx. 2*x-1)`S))"
      by (simp add: ‹finite S›)
    show "g2 differentiable at x within {0..1}" if "x ∈ {0..1} - insert 0 ((λx. 2*x-1)`S)" for x
    proof (rule_tac d="dist ((x+1)/2) (1/2)" in differentiable_transform_within)
      have x2: "(x + 1) / 2 ∉ S"
        using that
        apply (clarsimp simp: image_iff)
        by (metis add.commute add_diff_cancel_left' mult_2 field_sum_of_halves)
      have "g1 +++ g2 ∘ (λx. (x+1) / 2) differentiable at x within {0..1}"
        by (rule differentiable_chain_within differentiable_subset [OF S [of "(x+1)/2"]] | use x2 that in force)+
      then show "g1 +++ g2 ∘ (λx. (x+1) / 2) differentiable at x within {0..1}"
        by (auto intro: differentiable_chain_within)
      show "(g1 +++ g2 ∘ (λx. (x + 1) / 2)) x' = g2 x'" if "x' ∈ {0..1}" "dist x' x < dist ((x + 1) / 2) (1/2)" for x'
      proof -
        have [simp]: "(2*x'+2)/2 = x'+1"
          by (simp add: field_split_simps)
        show ?thesis
          using that by (auto simp: joinpaths_def)
      qed
    qed (use that in ‹auto simp: joinpaths_def›)
  qed
qed

lemma piecewise_C1_differentiable_D1:
  fixes g1 :: "real → 'a::real_normed_field"
  assumes "(g1 +++ g2) piecewise_C1_differentiable_on {0..1}"
    shows "g1 piecewise_C1_differentiable_on {0..1}"
proof -
  obtain S where "finite S"
             and co12: "continuous_on ({0..1} - S) (λx. vector_derivative (g1 +++ g2) (at x))"
             and g12D: "∀x∈{0..1} - S. g1 +++ g2 differentiable at x"
    using assms  by (auto simp: piecewise_C1_differentiable_on_def C1_differentiable_on_eq)
  have g1D: "g1 differentiable at x" if "x ∈ {0..1} - insert 1 ((*) 2 ` S)" for x
  proof (rule differentiable_transform_within)
    show "g1 +++ g2 ∘ (*) (inverse 2) differentiable at x"
      using that g12D
      unfolding joinpaths_def
      by (intro differentiable_chain_at derivative_intros | force)+
    show "∧x'. [dist x' x < dist (x/2) (1/2)]
          ==> (g1 +++ g2 ∘ (*) (inverse 2)) x' = g1 x'"
      using that by (auto simp: dist_real_def joinpaths_def)
  qed (use that in ‹auto simp: dist_real_def›)
  have [simp]: "vector_derivative (g1 ∘ (*) 2) (at (x/2)) = 2 *<sub>R</sub> vector_derivative g1 (at x)"
               if "x ∈ {0..1} - insert 1 ((*) 2 ` S)" for x
    apply (subst vector_derivative_chain_at)
    using that
    apply (rule derivative_eq_intros g1D | simp)+
    done
  have "continuous_on ({0..1/2} - insert (1/2) S) (λx. vector_derivative (g1 +++ g2) (at x))"
    using co12 by (rule continuous_on_subset) force
  then have coDhalf: "continuous_on ({0..1/2} - insert (1/2) S) (λx. vector_derivative (g1 ∘ (*)2) (at x))"
  proof (rule continuous_on_eq [OF _ vector_derivative_at])
    show "(g1 +++ g2 has_vector_derivative vector_derivative (g1 ∘ (*) 2) (at x)) (at x)"
      if "x ∈ {0..1/2} - insert (1/2) S" for x
    proof (rule has_vector_derivative_transform_within)
      show "(g1 ∘ (*) 2 has_vector_derivative vector_derivative (g1 ∘ (*) 2) (at x)) (at x)"
        using that
        by (force intro: g1D differentiable_chain_at simp: vector_derivative_works [symmetric])
      show "∧x'. [dist x' x < dist x (1/2)] ==> (g1 ∘ (*) 2) x' = (g1 +++ g2) x'"
        using that by (auto simp: dist_norm joinpaths_def)
    qed (use that in ‹auto simp: dist_norm›)
  qed
  have "continuous_on ({0..1} - insert 1 ((*) 2 ` S))
                      ((λx. 1/2 * vector_derivative (g1 ∘ (*)2) (at x)) ∘ (*)(1/2))"
    using coDhalf
    apply (intro continuous_intros)
    by (simp add: scaleR_conv_of_real image_set_diff image_image)
  then have con_g1: "continuous_on ({0..1} - insert 1 ((*) 2 ` S)) (λx. vector_derivative g1 (at x))"
    by (rule continuous_on_eq) (simp add: scaleR_conv_of_real)
  have "continuous_on {0..1} g1"
    using continuous_on_joinpaths_D1 assms piecewise_C1_differentiable_on_def by blast
  with ‹finite S› show ?thesis
    apply (clarsimp simp add: piecewise_C1_differentiable_on_def C1_differentiable_on_eq)
    apply (rule_tac x="insert 1 (((*)2)`S)" in exI)
    apply (simp add: g1D con_g1)
  done
qed

lemma piecewise_C1_differentiable_D2:
  fixes g2 :: "real → 'a::real_normed_field"
  assumes "(g1 +++ g2) piecewise_C1_differentiable_on {0..1}" "pathfinish g1 = pathstart g2"
    shows "g2 piecewise_C1_differentiable_on {0..1}"
proof -
  obtain S where "finite S"
             and co12: "continuous_on ({0..1} - S) (λx. vector_derivative (g1 +++ g2) (at x))"
             and g12D: "∀x∈{0..1} - S. g1 +++ g2 differentiable at x"
    using assms  by (auto simp: piecewise_C1_differentiable_on_def C1_differentiable_on_eq)
  have g2D: "g2 differentiable at x" if "x ∈ {0..1} - insert 0 ((λx. 2*x-1) ` S)" for x
  proof (rule differentiable_transform_within)
    show "g1 +++ g2 ∘ (λx. (x + 1) / 2) differentiable at x"
      using g12D that
      unfolding joinpaths_def
      apply (drule_tac x= "(x+1) / 2" in bspec, force simp: field_split_simps)
      apply (rule differentiable_chain_at derivative_intros | force)+
      done
    show "∧x'. dist x' x < dist ((x + 1) / 2) (1/2) ==> (g1 +++ g2 ∘ (λx. (x + 1) / 2)) x' = g2 x'"
      using that by (auto simp: dist_real_def joinpaths_def field_simps)
    qed (use that in ‹auto simp: dist_norm›)
  have [simp]: "vector_derivative (g2 ∘ (λx. 2*x-1)) (at ((x+1)/2)) = 2 *<sub>R</sub> vector_derivative g2 (at x)"
               if "x ∈ {0..1} - insert 0 ((λx. 2*x-1) ` S)" for x
    using that  by (auto simp: vector_derivative_chain_at field_split_simps g2D)
  have "continuous_on ({1/2..1} - insert (1/2) S) (λx. vector_derivative (g1 +++ g2) (at x))"
    using co12 by (rule continuous_on_subset) force
  then have coDhalf: "continuous_on ({1/2..1} - insert (1/2) S) (λx. vector_derivative (g2 ∘ (λx. 2*x-1)) (at x))"
  proof (rule continuous_on_eq [OF _ vector_derivative_at])
    show "(g1 +++ g2 has_vector_derivative vector_derivative (g2 ∘ (λx. 2 * x - 1)) (at x))
          (at x)"
      if "x ∈ {1 / 2..1} - insert (1 / 2) S" for x
    proof (rule_tac f="g2 ∘ (λx. 2*x-1)" and d="dist (3/4) ((x+1)/2)" in has_vector_derivative_transform_within)
      show "(g2 ∘ (λx. 2 * x - 1) has_vector_derivative vector_derivative (g2 ∘ (λx. 2 * x - 1)) (at x))
            (at x)"
        using that by (force intro: g2D differentiable_chain_at simp: vector_derivative_works [symmetric])
      show "∧x'. [dist x' x < dist (3 / 4) ((x + 1) / 2)] ==> (g2 ∘ (λx. 2 * x - 1)) x' = (g1 +++ g2) x'"
        using that by (auto simp: dist_norm joinpaths_def add_divide_distrib)
    qed (use that in ‹auto simp: dist_norm›)
  qed
  have [simp]: "((λx. (x+1) / 2) ` ({0..1} - insert 0 ((λx. 2 * x - 1) ` S))) = ({1/2..1} - insert (1/2) S)"
    apply (simp add: image_set_diff inj_on_def image_image)
    apply (auto simp: image_affinity_atLeastAtMost_div add_divide_distrib)
    done
  have "continuous_on ({0..1} - insert 0 ((λx. 2*x-1) ` S))
                      ((λx. 1/2 * vector_derivative (g2 ∘ (λx. 2*x-1)) (at x)) ∘ (λx. (x+1)/2))"
    by (rule continuous_intros | simp add:  coDhalf)+
  then have con_g2: "continuous_on ({0..1} - insert 0 ((λx. 2*x-1) ` S)) (λx. vector_derivative g2 (at x))"
    by (rule continuous_on_eq) (simp add: scaleR_conv_of_real)
  have "continuous_on {0..1} g2"
    using continuous_on_joinpaths_D2 assms piecewise_C1_differentiable_on_def by blast
  with ‹finite S› show ?thesis
    by (meson C1_differentiable_on_eq con_g2 finite_imageI finite_insert g2D piecewise_C1_differentiable_on_def)
qed


subsection ‹Valid paths, and their start and finish›

definition✐‹tag important› valid_path :: "(real → 'a :: real_normed_vector) → bool"
  where "valid_path f ≡ f piecewise_C1_differentiable_on {0..1::real}"

definition closed_path :: "(real → 'a :: real_normed_vector) → bool"
  where "closed_path g ≡ g 0 = g 1"

text‹In particular, all results for paths apply›

lemma valid_path_imp_path: "valid_path g ==> path g"
  by (simp add: path_def piecewise_C1_differentiable_on_def valid_path_def)

lemma connected_valid_path_image: "valid_path g ==> connected(path_image g)"
  by (metis connected_path_image valid_path_imp_path)

lemma compact_valid_path_image: "valid_path g ==> compact(path_image g)"
  by (metis compact_path_image valid_path_imp_path)

lemma bounded_valid_path_image: "valid_path g ==> bounded(path_image g)"
  by (metis bounded_path_image valid_path_imp_path)

lemma closed_valid_path_image: "valid_path g ==> closed(path_image g)"
  by (metis closed_path_image valid_path_imp_path)

lemma valid_path_translation_eq: "valid_path ((+)d ∘ p) ⟷ valid_path p"
  by (simp add: valid_path_def piecewise_C1_differentiable_on_translation_eq)
 
lemma valid_path_compose:
  assumes "valid_path g"
      and der: "∧x. x ∈ path_image g ==> f field_differentiable (at x)"
      and con: "continuous_on (path_image g) (deriv f)"
    shows "valid_path (f ∘ g)"
proof -
  obtain S where "finite S" and g_diff: "g C1_differentiable_on {0..1} - S"
    using ‹valid_path g› unfolding valid_path_def piecewise_C1_differentiable_on_def by auto
  have "f ∘ g differentiable at t" when "t∈{0..1} - S" for t
    proof (rule differentiable_chain_at)
      show "g differentiable at t" using ‹valid_path g›
        by (meson C1_differentiable_on_eq ‹g C1_differentiable_on {0..1} - S› that)
    next
      have "g t∈path_image g" using that DiffD1 image_eqI path_image_def by metis
      then show "f differentiable at (g t)"
        using der[THEN field_differentiable_imp_differentiable] by auto
    qed
  moreover have "continuous_on ({0..1} - S) (λx. vector_derivative (f ∘ g) (at x))"
    proof (rule continuous_on_eq [where f = "λx. vector_derivative g (at x) * deriv f (g x)"],
        rule continuous_intros)
      show "continuous_on ({0..1} - S) (λx. vector_derivative g (at x))"
        using g_diff C1_differentiable_on_eq by auto
    next
      have "continuous_on {0..1} (λx. deriv f (g x))"
        using continuous_on_compose[OF _ con[unfolded path_image_def],unfolded comp_def]
          ‹valid_path g› piecewise_C1_differentiable_on_def valid_path_def
        by blast
      then show "continuous_on ({0..1} - S) (λx. deriv f (g x))"
        using continuous_on_subset by blast
    next
      show "vector_derivative g (at t) * deriv f (g t) = vector_derivative (f ∘ g) (at t)"
          when "t ∈ {0..1} - S" for t
        by (metis C1_differentiable_on_eq DiffD1 der g_diff imageI path_image_def that 
                  vector_derivative_chain_at_general)
    qed
  ultimately have "f ∘ g C1_differentiable_on {0..1} - S"
    using C1_differentiable_on_eq by blast
  moreover have "path (f ∘ g)"
    using der
    by (simp add: path_continuous_image[OF valid_path_imp_path[OF ‹valid_path g›]] continuous_at_imp_continuous_on field_differentiable_imp_continuous_at)
  ultimately show ?thesis unfolding valid_path_def piecewise_C1_differentiable_on_def path_def
    using ‹finite S› by auto
qed
  
lemma valid_path_uminus_comp[simp]:
  fixes g::"real → 'a ::real_normed_field"
  shows "valid_path (uminus ∘ g) ⟷ valid_path g"
proof 
  show "valid_path g ==> valid_path (uminus ∘ g)" for g::"real → 'a"
    by (auto intro!: valid_path_compose derivative_intros)  
  then show "valid_path g" when "valid_path (uminus ∘ g)"
    by (metis fun.map_comp group_add_class.minus_comp_minus id_comp that)
qed

lemma valid_path_offset[simp]:
  shows "valid_path (λt. g t - z) ⟷ valid_path g"  
proof 
  show *: "valid_path (g::real→'a) ==> valid_path (λt. g t - z)" for g z
    unfolding valid_path_def
    by (fastforce intro:derivative_intros C1_differentiable_imp_piecewise piecewise_C1_differentiable_diff)
  show "valid_path (λt. g t - z) ==> valid_path g"
    using *[of "λt. g t - z" "-z",simplified] .
qed

lemma valid_path_imp_reverse:
  assumes "valid_path g"
    shows "valid_path(reversepath g)"
proof -
  obtain S where "finite S" and S: "g C1_differentiable_on ({0..1} - S)"
    using assms by (auto simp: valid_path_def piecewise_C1_differentiable_on_def)
  then have "finite ((-) 1 ` S)"
    by auto
  moreover have "(reversepath g C1_differentiable_on ({0..1} - (-) 1 ` S))"
    unfolding reversepath_def
    apply (rule C1_differentiable_compose [of "λx::real. 1-x" _ g, unfolded o_def])
    using S
    by (force simp: finite_vimageI inj_on_def C1_differentiable_on_eq elim!: continuous_on_subset)+
  ultimately show ?thesis using assms
    by (auto simp: valid_path_def piecewise_C1_differentiable_on_def path_def [symmetric])
qed

lemma valid_path_reversepath [simp]: "valid_path(reversepath g) ⟷ valid_path g"
  using valid_path_imp_reverse by force

lemma valid_path_join:
  assumes "valid_path g1" "valid_path g2" "pathfinish g1 = pathstart g2"
    shows "valid_path(g1 +++ g2)"
proof -
  have "g1 1 = g2 0"
    using assms by (auto simp: pathfinish_def pathstart_def)
  moreover have "(g1 ∘ (λx. 2*x)) piecewise_C1_differentiable_on {0..1/2}"
    apply (rule piecewise_C1_differentiable_compose)
    using assms
    apply (auto simp: valid_path_def piecewise_C1_differentiable_on_def continuous_on_joinpaths)
    apply (force intro: finite_vimageI [where h = "(*)2"] inj_onI)
    done
  moreover have "(g2 ∘ (λx. 2*x-1)) piecewise_C1_differentiable_on {1/2..1}"
    apply (rule piecewise_C1_differentiable_compose)
    using assms unfolding valid_path_def piecewise_C1_differentiable_on_def
    by (auto intro!: continuous_intros finite_vimageI [where h = "(λx. 2*x - 1)"] inj_onI
             simp: image_affinity_atLeastAtMost_diff continuous_on_joinpaths)
  ultimately show ?thesis
    unfolding valid_path_def continuous_on_joinpaths joinpaths_def
    by (intro piecewise_C1_differentiable_cases) (auto simp: o_def)
qed

lemma valid_path_join_D1:
  fixes g1 :: "real → 'a::real_normed_field"
  shows "valid_path (g1 +++ g2) ==> valid_path g1"
  unfolding valid_path_def
  by (rule piecewise_C1_differentiable_D1)

lemma valid_path_join_D2:
  fixes g2 :: "real → 'a::real_normed_field"
  shows "[valid_path (g1 +++ g2); pathfinish g1 = pathstart g2] ==> valid_path g2"
  unfolding valid_path_def
  by (rule piecewise_C1_differentiable_D2)

lemma valid_path_join_eq [simp]:
  fixes g2 :: "real → 'a::real_normed_field"
  shows "pathfinish g1 = pathstart g2 ==> (valid_path(g1 +++ g2) ⟷ valid_path g1 ∧ valid_path g2)"
  using valid_path_join_D1 valid_path_join_D2 valid_path_join by blast

lemma valid_path_shiftpath [intro]:
  assumes "valid_path g" "pathfinish g = pathstart g" "a ∈ {0..1}"
    shows "valid_path(shiftpath a g)"
  using assms
  unfolding valid_path_def shiftpath_alt_def
  apply (intro piecewise_C1_differentiable_cases)
      apply (simp_all add: add.commute)
    apply (rule piecewise_C1_differentiable_affine [of g 1 a, simplified o_def scaleR_one])
    apply (force simp: pathfinish_def pathstart_def elim: piecewise_C1_differentiable_on_subset)
   apply (rule piecewise_C1_differentiable_affine [of g 1 "a-1", simplified o_def scaleR_one algebra_simps])
   apply (auto simp: pathfinish_def pathstart_def elim: piecewise_C1_differentiable_on_subset)
  done

lemma vector_derivative_linepath_within:
    "x ∈ {0..1} ==> vector_derivative (linepath a b) (at x within {0..1}) = b - a"
  by (simp add: has_vector_derivative_linepath_within vector_derivative_at_within_ivl)

lemma vector_derivative_linepath_at [simp]: "vector_derivative (linepath a b) (at x) = b - a"
  by (simp add: has_vector_derivative_linepath_within vector_derivative_at)

lemma valid_path_linepath [iff]: "valid_path (linepath a b)"
  using C1_differentiable_on_eq piecewise_C1_differentiable_on_def valid_path_def by fastforce

lemma valid_path_subpath:
  fixes g :: "real → 'a :: real_normed_vector"
  assumes "valid_path g" "u ∈ {0..1}" "v ∈ {0..1}"
    shows "valid_path(subpath u v g)"
proof (cases "v=u")
  case True
  then show ?thesis
    unfolding valid_path_def subpath_def
    by (force intro: C1_differentiable_on_const C1_differentiable_imp_piecewise)
next
  case False
  let ?f = "λx. ((v-u) * x + u)"
  have "(g ∘ ?f) piecewise_C1_differentiable_on {0..1}"
  proof (rule piecewise_C1_differentiable_compose)
    show "?f piecewise_C1_differentiable_on {0..1}"
      by (simp add: C1_differentiable_imp_piecewise)
    have "g piecewise_C1_differentiable_on (if u ≤ v then {u..v} else {v..u})"
      using assms piecewise_C1_differentiable_on_subset valid_path_def by force
    then show "g piecewise_C1_differentiable_on ?f ` {0..1}"
      by (simp add: image_affinity_atLeastAtMost split: if_split_asm)
    show "∧x. finite ({0..1} ∩ ?f -` {x})"
      using False
      by (simp add: Int_commute [of "{0..1}"] inj_on_def crossproduct_eq finite_vimage_IntI)
  qed
  then show ?thesis
    by (auto simp: o_def valid_path_def subpath_def)
qed

lemma valid_path_rectpath [simp, intro]: "valid_path (rectpath a b)"
  by (simp add: Let_def rectpath_def)

lemma linear_image_valid_path:
  fixes p :: "real → 'a :: euclidean_space"
  assumes  "valid_path p" "linear f"
  shows    "valid_path (f ∘ p)"
  unfolding valid_path_def piecewise_C1_differentiable_on_def
proof (intro conjI)
  from assms have "path p"
    by (simp add: valid_path_imp_path)
  thus "continuous_on {0..1} (f ∘ p)"
    unfolding o_def path_def by (intro linear_continuous_on_compose[OF _ assms(2)])
  from assms(1) obtain S where S: "finite S" "p C1_differentiable_on {0..1} - S"
    by (auto simp: valid_path_def piecewise_C1_differentiable_on_def)
  from S(2) obtain p' :: "real → 'a"
    where p': "∧x. x ∈ {0..1} - S ==> (p has_vector_derivative p' x) (at x)"
              "continuous_on ({0..1} - S) p'"
    by (fastforce simp: C1_differentiable_on_def)

  have "(f ∘ p has_vector_derivative f (p' x)) (at x)" if "x ∈ {0..1} - S" for x
    by (rule vector_derivative_diff_chain_within [OF p'(1)[OF that]]
             linear_imp_has_derivative assms)+
  moreover have "continuous_on ({0..1} - S) (λx. f (p' x))"
    by (rule linear_continuous_on_compose [OF p'(2) assms(2)])
  ultimately have "f ∘ p C1_differentiable_on {0..1} - S"
    unfolding C1_differentiable_on_def by (intro exI[of _ "λx. f (p' x)"]) fast
  thus "∃S. finite S ∧ f ∘ p C1_differentiable_on {0..1} - S"
    using ‹finite S› by blast
qed

lemma valid_path_times:
  fixes γ::"real → 'a ::real_normed_field"
  assumes "c≠0"
  shows "valid_path ((*) c ∘ γ) = valid_path γ"
proof 
  assume "valid_path ((*) c ∘ γ)"
  then have "valid_path ((*) (1/c) ∘ ((*) c ∘ γ))"
    by (simp add: valid_path_compose)
  then show "valid_path γ" 
    unfolding comp_def using ‹c≠0› by auto
next
  assume "valid_path γ"
  then show "valid_path ((*) c ∘ γ)"
    by (simp add: valid_path_compose)
qed

lemma path_compose_cnj_iff [simp]: "path (cnj ∘ p) ⟷ path p"
proof -
  have "path (cnj ∘ p)" if "path p" for p
    by (intro path_continuous_image continuous_intros that)
  from this[of p] and this[of "cnj ∘ p"] show ?thesis
    by (auto simp: o_def)
qed

lemma valid_path_cnj:
  fixes g::"real → complex"
    shows "valid_path (cnj ∘ g) = valid_path g"
proof
  show valid:"valid_path (cnj ∘ g)" if "valid_path g" for g
  proof -
    obtain S where "finite S" and g_diff: "g C1_differentiable_on {0..1} - S"
      using ‹valid_path g› unfolding valid_path_def piecewise_C1_differentiable_on_def by auto
  
    have g_diff':"g differentiable at t" when "t∈{0..1} - S" for t
      by (meson C1_differentiable_on_eq ‹g C1_differentiable_on {0..1} - S› that)
    then have "(cnj ∘ g) differentiable at t" when "t∈{0..1} - S" for t
      using bounded_linear_cnj bounded_linear_imp_differentiable differentiable_chain_at that by blast
    moreover have "continuous_on ({0..1} - S)
        (λx. vector_derivative (cnj ∘ g) (at x))"
    proof -
      have "continuous_on ({0..1} - S)
          (λx. vector_derivative (cnj ∘ g) (at x))
        = continuous_on ({0..1} - S)
          (λx. cnj (vector_derivative g (at x)))"
        apply (rule continuous_on_cong[OF refl])
        unfolding comp_def using g_diff'
        using has_vector_derivative_cnj vector_derivative_at vector_derivative_works by blast
      also have "…"
        apply (intro continuous_intros)
        using C1_differentiable_on_eq g_diff by blast
      finally show ?thesis .
    qed
    ultimately have "cnj ∘ g C1_differentiable_on {0..1} - S"
      using C1_differentiable_on_eq by blast
    moreover have "path (cnj ∘ g)"
      apply (rule path_continuous_image[OF valid_path_imp_path[OF ‹valid_path g›]])
      by (intro continuous_intros)
    ultimately show ?thesis unfolding valid_path_def piecewise_C1_differentiable_on_def path_def
      using ‹finite S› by auto
  qed
  from this[of "cnj o g"]
  show "valid_path (cnj ∘ g) ==> valid_path g"
    unfolding comp_def by simp
qed

end