theory Foo
  imports "HOL-Complex_Analysis.Complex_Analysis"
begin

text \<open>
  A continuously differentiable function from the reals to a vector space.
\<close>
definition C1_on :: "real set \<Rightarrow> (real \<Rightarrow> 'a :: real_normed_vector) \<Rightarrow> bool" where
  "C1_on S f \<longleftrightarrow> (\<exists>D. (\<forall>x \<in> S. (f has_vector_derivative (D x)) (at x within S)) \<and> continuous_on S D)"


text \<open>
  A piecewise continuously differentiable function from the reals to a vector space.
  See \<^url>\<open>https://proofwiki.org/wiki/Definition:Piecewise_Continuously_Differentiable_Function\<close>.
\<close>
definition piecewise_C1_on :: "real set \<Rightarrow> (real \<Rightarrow> 'a :: real_normed_vector) \<Rightarrow> bool" where
  "piecewise_C1_on A f \<longleftrightarrow> continuous_on A f \<and> (\<exists>X. X division_of A \<and> (\<forall>Y\<in>X. C1_on Y f))"

lemma C1_imp_piecewise_C1: "C1_on S f \<Longrightarrow> piecewise_C1_on A f"
  sorry

lemma piecewise_C1_imp_continuous:
  assumes "piecewise_C1_on A f"
  shows   "continuous_on A f"
  using assms unfolding piecewise_C1_on_def by blast


text \<open>
  The one-sided derivatives exist everywhere.
\<close>
lemma piecewise_C1_imp_differentiable_left:
  assumes "piecewise_C1_on {a..b} f" "x \<in> {a<..b}"
  shows   "f differentiable at_left x"
  sorry

lemma piecewise_C1_imp_differentiable_right:
  assumes "piecewise_C1_on {a..b} f" "x \<in> {a..<b}"
  shows   "f differentiable at_right x"
  sorry


text \<open>
  The left- and right-sided limits of the derivative exist.
\<close>
lemma piecewise_C1_imp_deriv_tendsto_left:
  assumes "piecewise_C1_on {a..b} f" "x \<in> {a<..b}"
  shows   "((\<lambda>t. vector_derivative f (at t)) \<longlongrightarrow> vector_derivative f (at_left x)) (at_left x)"
  sorry

lemma piecewise_C1_imp_deriv_tendsto_right:
  assumes "piecewise_C1_on {a..b} f" "x \<in> {a..<b}"
  shows   "((\<lambda>t. vector_derivative f (at t)) \<longlongrightarrow> vector_derivative f (at_right x)) (at_right x)"
  sorry


text \<open>
  A smooth path without corners, e.g.\ a line or a circular arc.
\<close>
definition C1_path :: "(real \<Rightarrow> 'a :: real_normed_vector) \<Rightarrow> bool" where
  "C1_path p \<longleftrightarrow> C1_on {0..1} p"


text \<open>
  A piecewise smooth path, i.e.\ possibly with corners. Can be seen as a concatenation of
  finitely many smooth paths.
\<close>
definition valid_path where "valid_path p \<longleftrightarrow> piecewise_C1_on {0..1} p"

lemma C1_path_imp_valid_path: "C1_path p \<Longrightarrow> valid_path p"
  unfolding C1_path_def valid_path_def using C1_imp_piecewise_C1 by blast

lemma valid_path_join:
  assumes "valid_path p" "valid_path q" "pathfinish p = pathstart q"
  shows   "valid_path (p +++ q)"
  sorry



text \<open>
  An attempt at a general definition of $C^n$-smoothness for functions from the reals to a
  vector space. $n$ can be a natural number of $\infty$.
  Note that $C^0$-smoothness means ``continuous'', $C^1$ means ``continuously differentiable''.
\<close>
definition smooth_on :: "enat \<Rightarrow> real set \<Rightarrow> (real \<Rightarrow> 'a :: real_normed_vector) \<Rightarrow> bool"
  ("C\<^bsup>_\<^esup>-smooth'_on" [1000]) where
  "C\<^bsup>n\<^esup>-smooth_on S f  \<longleftrightarrow>
     (let D = (\<lambda>g x. vector_derivative g (at x within S))
      in  (\<forall>k. enat k < n \<longrightarrow> (\<forall>x\<in>S. (D ^^ k) f differentiable (at x within S))) \<and>
          (\<forall>k. enat k \<le> n \<longrightarrow> continuous_on S ((D ^^ k) f)))"

lemma C1_on_altdef: "C1_on S f \<longleftrightarrow> C\<^bsup>1\<^esup>-smooth_on S f"
  sorry

end