theory Flow
imports
  Picard_Lindeloef_Qualitative
  "~~/src/HOL/Library/Diagonal_Subsequence"
  "../Library/Bounded_Linear_Function"
begin

text {* TODO: replace @{thm differentiable_bound}*}
lemma differentiable_bound_generalized:
  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
  assumes "convex s"
    and "\<forall>x\<in>s. (f has_derivative f' x) (at x within s)"
    and "\<forall>x\<in>s. onorm (f' x) \<le> B"
    and x: "x \<in> s"
    and y: "y \<in> s"
  shows "norm (f x - f y) \<le> B * norm (x - y)"
proof -
  let ?p = "\<lambda>u. x + u *\<^sub>R (y - x)"
  let ?\<phi> = "\<lambda>h. h * B * norm (x - y)"
  have *: "\<And>u. u\<in>{0..1} \<Longrightarrow> x + u *\<^sub>R (y - x) \<in> s"
    using assms(1)[unfolded convex_alt,rule_format,OF x y]
    unfolding scaleR_left_diff_distrib scaleR_right_diff_distrib
    by (auto simp add: algebra_simps)
  have 0: "continuous_on (?p ` {0..1}) f"
    using *
    unfolding continuous_on_eq_continuous_within
    apply -
    apply rule
    apply (rule differentiable_imp_continuous_within)
    unfolding differentiable_def
    apply (rule_tac x="f' xa" in exI)
    apply (rule has_derivative_within_subset)
    apply (rule assms(2)[rule_format])
    apply auto
    done
  from * have 1: "continuous_on {0 .. 1} (f \<circ> ?p)"
    by (intro continuous_intros 0)+
  {
    fix u::real assume u: "u \<in>{0 <..< 1}"
    let ?u = "?p u"
    interpret linear "(f' ?u)"
      using u by (auto intro!: has_derivative_linear assms(2)[rule_format] *)
    have "(f \<circ> ?p has_derivative (f' ?u) \<circ> (\<lambda>u. 0 + u *\<^sub>R (y - x))) (at u within box 0 1)"
      apply (rule diff_chain_within)
      apply (rule derivative_intros)+
      apply (rule has_derivative_within_subset)
      apply (rule assms(2)[rule_format])
      using u *
      apply auto
      done
    hence "((f \<circ> ?p) has_vector_derivative f' ?u (y - x)) (at u)"
      by (simp add: has_derivative_within_open[OF u open_greaterThanLessThan]
        scaleR has_vector_derivative_def o_def)
  } note 2 = this
  {
    have "continuous_on {0..1} ?\<phi>"
      apply (rule continuous_intros)+
      done
  } note 3 = this
  {
    fix u::real assume u: "u \<in>{0 <..< 1}"
    have "(?\<phi> has_vector_derivative B * norm (x - y)) (at u)"
      by (auto simp: has_vector_derivative_def intro!: derivative_eq_intros)
  } note 4 = this
  {
    fix u::real assume u: "u \<in>{0 <..< 1}"
    let ?u = "?p u"
    interpret bounded_linear "(f' ?u)"
      using u by (auto intro!: has_derivative_bounded_linear assms(2)[rule_format] *)
    have "norm (f' ?u (y - x)) \<le> onorm (f' ?u) * norm (y - x)"
      by (rule onorm) fact
    also have "onorm (f' ?u) \<le> B"
      using u by (auto intro!: assms(3)[rule_format] *)
    finally have "norm ((f' ?u) (y - x)) \<le> B * norm (x - y)"
      by (simp add: mult_right_mono norm_minus_commute)
  } note 5 = this
  have "norm (f x - f y) = norm ((f \<circ> (\<lambda>u. x + u *\<^sub>R (y - x))) 1 - (f \<circ> (\<lambda>u. x + u *\<^sub>R (y - x))) 0)"
    by (auto simp add: norm_minus_commute)
  also
  from mvt_more_general[OF zero_less_one 1, OF 3 2 4 5]
  have "norm ((f \<circ> ?p) 1 - (f \<circ> ?p) 0) \<le> B * norm (x - y)"
    by simp
  finally show ?thesis .
qed

lemma eventually_at_shift_zero:
  fixes x::"'b::real_normed_vector"
  shows "eventually (\<lambda>h. P (x + h)) (at 0) \<longleftrightarrow> eventually P (at x)"
proof -
  have "eventually (\<lambda>h. P (x + h)) (at 0) \<longleftrightarrow>
    eventually P (filtermap (op + x) (at 0))"
    by (simp add: eventually_filtermap)
  also have "filtermap (op + x) (at 0) = at x"
    using filtermap_at_shift[of "-x" 0]
    apply (subst add.commute[abs_def])
    apply (simp add: )
    done
  finally show ?thesis .
qed

lemma eventually_at_fst:
  assumes "eventually P (at (fst x))"
  assumes "P (fst x)"
  shows "eventually (\<lambda>h. P (fst h)) (at x)"
  using assms
  unfolding eventually_at_topological
proof safe
  case goal1
  thus ?case
    apply (intro exI[where x="S\<times>UNIV"])
    apply (auto intro!: open_Times)
    apply (metis fst_vimage_eq_Times vimageI)
    done
qed

lemma eventually_at_snd:
  assumes "eventually P (at (snd x))"
  assumes "P (snd x)"
  shows "eventually (\<lambda>h. P (snd h)) (at x)"
  using assms
  unfolding eventually_at_topological
proof safe
  case goal1
  thus ?case
    apply (intro exI[where x="UNIV\<times>S"])
    apply (auto intro!: open_Times)
    apply (metis snd_vimage_eq_Times vimageI)
    done
qed

lemma eventually_at_in_ball: "d > 0 \<Longrightarrow> eventually (\<lambda>y. y \<in> ball x0 d) (at x0)"
  by (auto simp: eventually_at dist_commute intro!: exI[where x=d])

lemma interior_atLeastAtMost:
  fixes a b::real
  assumes "a < b"
  shows "interior {a .. b} = {a <..< b}"
  by (metis assms closure_greaterThanLessThan convex_interior_closure convex_real_interval(8)
    interior_open open_greaterThanLessThan rel_interior_real_box)

lemma real_image_ereal_ivl:
  fixes a b::ereal
  shows
  "real ` {a<..<b} =
  (if a < b then (if a = - \<infinity> then if b = \<infinity> then UNIV else {..<real b}
  else if b = \<infinity> then {real a<..} else {real a <..< real b}) else {})"
  using assms
  apply (cases a b rule: ereal.exhaust[case_product ereal.exhaust])
  apply (auto )
  apply (metis ereal_infinity_cases ereal_infty_less(1) ereal_real' less_ereal.simps(5)
    less_not_sym neq_iff real_less_ereal_iff)
  apply (metis ereal_infinity_cases ereal_less_real_iff ereal_real' less_ereal.simps(2)
    less_ereal.simps(3) less_not_sym neq_iff)
  apply (rename_tac c d e)
  apply (rule_tac x = "ereal e" in image_eqI)
  apply simp
  apply simp
  apply (metis ereal_infinity_cases ereal_less_real_iff less_ereal.simps(3))
  apply (rename_tac c d)
  apply (rule_tac x = "ereal d" in image_eqI)
  apply simp
  apply simp
  using less_ereal.simps(2) real_less_ereal_iff apply blast
  apply (rename_tac c d)
  apply (rule_tac x = "ereal d" in image_eqI)
  apply simp
  apply simp
  apply (rule_tac x = "ereal x" in image_eqI)
  apply auto
  done

lemma nonneg_lipschitz:
  assumes "lipschitz X f L"
  shows "lipschitz X f (abs L)"
  using assms
  by (auto simp: lipschitz_def)

lemma pos_lipschitz:
  assumes "lipschitz X f L"
  shows "lipschitz X f (abs L + 1)"
  using assms
proof (auto simp: lipschitz_def)
  case goal1
  hence "dist (f x) (f y) \<le> L * dist x y"
    by auto
  also have "\<dots> \<le> (abs L + 1) * dist x y"
    by (rule mult_right_mono) auto
  finally show ?case by (simp add: lipschitz_nonneg[OF assms])
qed

lemma
  infdist_attains_inf:
  fixes X::"'a::heine_borel set"
  assumes "closed X"
  assumes "X \<noteq> {}"
  obtains x where "x \<in> X" "infdist y X = dist y x"
proof -
  have "bdd_below (dist y ` X)"
    by auto
  from distance_attains_inf[OF assms, of y]
  obtain x where INF: "x \<in> X" "\<And>z. z \<in> X \<Longrightarrow> dist y x \<le> dist y z" by auto
  have "infdist y X = dist y x"
    by (auto simp: infdist_def assms intro!: antisym cINF_lower[OF _ `x \<in> X`] cINF_greatest[OF assms(2) INF(2)])
  with `x \<in> X` show ?thesis ..
qed

lemma compact_infdist_le:
  fixes A::"'a::heine_borel set"
  assumes "A \<noteq> {}"
  assumes "compact A"
  assumes "e > 0"
  shows "compact {x. infdist x A \<le> e}"
proof -
  from continuous_closed_vimage[of "\<lambda>x. infdist x A" "{0..e}"]
    continuous_infdist[OF continuous_ident, of _ UNIV A]
  have "closed {x. infdist x A \<le> e}" by (auto simp: vimage_def infdist_nonneg)
  moreover
  from assms obtain x0 b where b: "\<And>x. x \<in> A \<Longrightarrow> dist x0 x \<le> b" "closed A"
    by (auto simp: compact_eq_bounded_closed bounded_def)
  have "bounded {x. infdist x A \<le> e}"
    apply (auto simp: bounded_any_center[where a=x0] intro!: exI[where x="b + e"])
  proof -
    case goal1
    from infdist_attains_inf[OF `closed A` `A \<noteq> {}`, of y]
    obtain z where z: "z \<in> A" "infdist y A = dist y z" by blast
    have "dist x0 y \<le> dist y z + dist x0 z"
      by (metis dist_commute dist_triangle)
    also have "dist y z \<le> e" using goal1 z by simp
    also have "dist x0 z \<le> b" using b z by simp
    finally show ?case by arith
  qed
  ultimately show "compact {x. infdist x A \<le> e}" by (simp add: compact_eq_bounded_closed)
qed

lemma compact_in_open_separated:
  fixes A::"'a::heine_borel set"
  assumes "A \<noteq> {}"
  assumes "compact A"
  assumes "open B"
  assumes "A \<subseteq> B"
  obtains e where "e > 0" "{x. infdist x A \<le> e} \<subseteq> B"
proof atomize_elim
  have "closed (- B)" "compact A" "- B \<inter> A = {}"
    using assms by (auto simp: open_Diff compact_eq_bounded_closed)
  from separate_closed_compact[OF this]
  obtain d'::real where d': "d'>0" "\<And>x y. x \<notin> B \<Longrightarrow> y \<in> A \<Longrightarrow> d' \<le> dist x y"
    by auto
  def d \<equiv> "d' / 2"
  hence "d>0" "d < d'" using d' by auto
  with d' have d: "\<And>x y. x \<notin> B \<Longrightarrow> y \<in> A \<Longrightarrow> d < dist x y"
    apply (auto simp: )
    by (metis le_less_trans not_less)
  show "\<exists>e>0. {x. infdist x A \<le> e} \<subseteq> B"
  proof (rule ccontr, auto)
    assume "\<forall>e>0. \<not> {x. infdist x A \<le> e} \<subseteq> B"
    hence "\<forall>e>0. \<exists>x. infdist x A \<le> e \<and> x \<notin> B"
      by auto
    with `d > 0` obtain x where x: "infdist x A \<le> d" "x \<notin> B"
      by auto
    from assms have "closed A" "A \<noteq> {}" by (auto simp: compact_eq_bounded_closed)
    from infdist_attains_inf[OF this] obtain y where y: "y \<in> A" "infdist x A = dist x y" by auto
    have "dist x y \<le> d" using x y by simp
    also have "\<dots> < dist x y" using y d x by auto
    finally show False by simp
  qed
qed

lemma is_interval_real_cball[simp]:
  fixes a b::real
  shows "is_interval (cball a b)"
  by (auto simp: is_interval_convex_1 convex_cball)

lemma integral_minus_sets:
  fixes f::"real \<Rightarrow> 'a::banach"
  shows "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> f integrable_on {0 .. max a b} \<Longrightarrow>integral {0..a} f - integral {0..b} f =
    (if a \<le> b then - integral {a .. b} f else integral {b .. a} f)"
  by (auto simp: algebra_simps integral_combine max_def)

lemma integral_minus_sets':
  fixes f::"real \<Rightarrow> 'a::banach"
  shows "\<not> 0 \<le> a \<Longrightarrow> \<not> 0 \<le> b \<Longrightarrow> f integrable_on {min a b .. 0} \<Longrightarrow>integral {a..0} f - integral {b..0} f =
    (if a \<le> b then integral {a .. b} f else - integral {b .. a} f)"
  by (auto simp: algebra_simps integral_combine integral_combine2 min_def)

lemma continuous_on_imp_absolutely_integrable_on:
  fixes f::"real \<Rightarrow> 'a::banach"
  shows "continuous_on {a..b} f \<Longrightarrow> norm (integral {a..b} f) \<le> integral {a..b} (\<lambda>x. norm (f x))"
  by (rule absolutely_integrable_le[OF absolutely_integrable_onI[OF
    integrable_continuous_real integrable_continuous_real[OF continuous_on_norm]]])

lemma integral_bound:
  fixes f::"real \<Rightarrow> 'a::banach"
  assumes "a \<le> b"
  assumes "continuous_on {a .. b} f"
  assumes "\<And>t. t \<in> {a .. b} \<Longrightarrow> norm (f t) \<le> B"
  shows "norm (integral {a .. b} f) \<le> B * (b - a)"
proof -
  note continuous_on_imp_absolutely_integrable_on[OF assms(2)]
  also have "integral {a..b} (\<lambda>x. norm (f x)) \<le> integral {a..b} (\<lambda>_. B)"
    by (rule integral_le) (auto intro!: integrable_continuous_real continuous_intros assms)
  also have "\<dots> = B * (b - a)" using assms by simp
  finally show ?thesis .
qed

lemma (in ivp) shift_autonomous_solution:
  assumes "is_solution y"
  assumes "x = y o (\<lambda>t.(t + ivp_t0 i - ivp_t0 j))"
  assumes "\<And>s t x. ivp_f i (s, x) = ivp_f i (t, x)"
  assumes "ivp_f j = ivp_f i"
  assumes "ivp_x0 j = ivp_x0 i"
  assumes "ivp_X j = ivp_X i"
  assumes "ivp_T j = op + (ivp_t0 j - ivp_t0 i) ` ivp_T i"
  shows "ivp.is_solution j x"
proof -
  interpret j: ivp j
    using iv_defined
    by (unfold_locales) (auto simp: assms)
  have image_collapse: "(\<lambda>t. t + t0 - ivp_t0 j) ` op + (ivp_t0 j - t0) ` T = ivp_T i"
    by force
  have deriv_id: "\<And>x F. ((\<lambda>t. t + ivp_t0 i - ivp_t0 j) has_vector_derivative 1) F"
    by (auto intro!: derivative_eq_intros simp: has_vector_derivative_def)
  show ?thesis
    using is_solutionD[OF assms(1)]
    apply (intro j.is_solutionI)
    apply (auto simp: assms)
    apply (rule vector_diff_chain_within[THEN vector_derivative_eq_rhs])
    apply (auto simp add: image_collapse assms intro: deriv_id)
    done
qed

lemma (in unique_solution) shift_autonomous_unique_solution:
  assumes "x = y o (\<lambda>t.(t + ivp_t0 i - ivp_t0 j))"
  assumes "\<And>s t x. ivp_f i (s, x) = ivp_f i (t, x)"
  assumes "ivp_f j = ivp_f i"
  assumes "ivp_x0 j = ivp_x0 i"
  assumes "ivp_X j = ivp_X i"
  assumes "ivp_T j = op + (ivp_t0 j - ivp_t0 i) ` ivp_T i"
  shows "unique_solution j"
proof
  interpret j: ivp j
    using iv_defined
    by unfold_locales (auto simp: assms)
  show "j.t0 \<in> j.T" "j.x0 \<in> j.X" using j.iv_defined by auto
  show "\<exists>x. ivp.is_solution j x"
    by (auto simp: assms intro!: exI shift_autonomous_solution[OF is_solution_solution])
  then interpret j: has_solution j by unfold_locales
  fix t y assume t: "t \<in> j.T" and y_sol: "j.is_solution y"
  from t have ts: "t + t0 - j.t0 \<in> T" by (auto simp: assms)
  from y_sol have "is_solution (y o (op + (j.t0 - t0)))"
    by (rule j.shift_autonomous_solution) (force simp: o_def algebra_simps assms)+
  note unique_solution[OF this ts]
  moreover
  from j.is_solution_solution have "is_solution (j.solution o (op + (j.t0 - t0)))"
    by (rule j.shift_autonomous_solution) (force simp: o_def algebra_simps assms)+
  note unique_solution[OF this ts]
  ultimately
  show "y t = j.solution t"
    by simp
qed

lemma (in ivp) shift_initial_value:
  assumes "is_solution y"
  assumes "ivp_t0 j \<in> ivp_T j"
  assumes "ivp_f j = ivp_f i"
  assumes "ivp_x0 j = y (ivp_t0 j)"
  assumes "ivp_X j = ivp_X i"
  assumes "ivp_T j \<subseteq> ivp_T i"
  shows "ivp.is_solution j y"
proof -
  interpret j: ivp j
    using iv_defined is_solutionD(3)[OF assms(1)] assms
    by (unfold_locales) auto
  show ?thesis
    using is_solutionD[OF assms(1)] assms
    by (auto intro!: j.is_solutionI has_vector_derivative_within_subset[where t="j.T" and s = T])
qed


lemma has_real_derivative_within_subset:
  "(f has_real_derivative f') (at x within s) \<Longrightarrow> t \<subseteq> s \<Longrightarrow> (f has_real_derivative f') (at x within t)"
  by (simp add: has_field_derivative_iff_has_vector_derivative has_vector_derivative_within_subset)

lemma has_real_derivative_continuous_on:
  "(\<And>x. x \<in> s \<Longrightarrow> (f has_real_derivative f' x) (at x within s)) \<Longrightarrow> continuous_on s f"
  by (metis DERIV_continuous continuous_on_eq_continuous_within)

lemma
  integral_has_real_derivative:
  "continuous_on {a .. b} g \<Longrightarrow> a \<le> t \<Longrightarrow> t \<le> b \<Longrightarrow>
    ((\<lambda>x. integral {a..x} g) has_real_derivative g t) (at t within {a..b})"
  using integral_has_vector_derivative[of a b g t]
  by (auto simp: has_field_derivative_iff_has_vector_derivative)

lemma
  derivative_quotient_bound:
  assumes g_deriv: "\<And>t. t \<in> {a .. b} \<Longrightarrow> (g has_real_derivative g' t) (at t within {a .. b})"
  assumes frac_le: "\<And>t. t \<in> {a .. b} \<Longrightarrow> g' t / g t \<le> K"
  assumes g'_cont: "continuous_on {a .. b} g'"
  assumes g_pos: "\<And>t. t \<in> {a .. b} \<Longrightarrow> g t > 0"
  assumes t_in: "t \<in> {a .. b}"
  shows "g t \<le> g a * exp (K * (t - a))"
proof -
  from assms have g_nonzero: "\<And>t. t \<in> {a .. b} \<Longrightarrow> g t \<noteq> 0"
    by fastforce
  have frac_integrable: "\<And>t. t \<in> {a .. b} \<Longrightarrow> (\<lambda>t. g' t / g t) integrable_on {a..t}"
    by (force simp: g_nonzero intro: assms has_real_derivative_within_subset[OF g_deriv]
      continuous_on_subset[OF g'_cont] continuous_intros
      has_real_derivative_continuous_on)
  have "\<And>t. t \<in> {a..b} \<Longrightarrow> ((\<lambda>t. g' t / g t) has_integral ln (g t) - ln (g a)) {a .. t}"
    by (rule fundamental_theorem_of_calculus)
      (auto intro!: derivative_eq_intros assms has_real_derivative_within_subset[OF assms(1)]
        simp: has_field_derivative_iff_has_vector_derivative[symmetric])
  hence *: "\<And>t. t \<in> {a .. b} \<Longrightarrow> ln (g t) - ln (g a) = integral {a .. t} (\<lambda>t. g' t / g t)"
    using integrable_integral[OF frac_integrable]
    by (rule has_integral_unique[where f = "\<lambda>t. g' t / g t"])
  from * t_in have "ln (g t) - ln (g a) = integral {a .. t} (\<lambda>t. g' t / g t)" .
  also have "\<dots> \<le> integral {a .. t} (\<lambda>_. K)"
    using `t \<in> {a .. b}`
    by (intro integral_le) (auto intro!: frac_integrable frac_le integral_le)
  also have "\<dots> = K * (t - a)" using `t \<in> {a .. b}`
    by simp
  finally have "ln (g t) \<le> K * (t - a) + ln (g a)" (is "?lhs \<le> ?rhs")
    by simp
  hence "exp ?lhs \<le> exp ?rhs"
    by simp
  thus ?thesis
    using `t \<in> {a .. b}` g_pos
    by (simp add: ac_simps exp_add del: exp_le_cancel_iff)
qed

lemma gronwall:
  fixes g K C and t::real
  defines "G \<equiv> \<lambda>t. C + K * integral {0 .. t} (\<lambda>s. g s)"
  assumes g_le_G: "\<And>t. 0 \<le> t \<Longrightarrow> t \<le> a \<Longrightarrow> g t \<le> G t"
  assumes g_cont: "continuous_on {0 .. a} g"
  assumes g_nonneg: "\<And>t. 0 \<le> t \<Longrightarrow> t \<le> a \<Longrightarrow> g t \<ge> 0"
  assumes pos: "C > 0" "K > 0"
  assumes "0 \<le> t" "t \<le> a"
  shows "g t \<le> C * exp (K * t)"
proof -
  have G_pos: "\<And>t. 0 \<le> t \<Longrightarrow> t \<le> a \<Longrightarrow> 0 < G t"
    by (auto simp: G_def intro!: add_pos_nonneg mult_nonneg_nonneg integral_nonneg
      integrable_continuous_real assms intro: less_imp_le continuous_on_subset)
  have "g t \<le> G t" using assms by auto
  also
  {
    have "\<And>t. 0 \<le> t \<Longrightarrow> t \<le> a \<Longrightarrow> (G has_real_derivative K * g t) (at t within {0 .. a})"
      by (auto intro!: derivative_eq_intros integral_has_real_derivative g_cont simp: G_def)
    moreover
    {
      fix t assume "t \<in> {0 .. a}"
      hence "K * g t / G t \<le> K * G t / G t"        using pos g_le_G G_pos
        by (intro divide_right_mono mult_left_mono) (auto intro!: less_imp_le)
      also have "\<dots> = K"
        using G_pos[of t] `t \<in> {0 .. a}` by simp
      finally have "K * g t / G t \<le> K" .
    }
    ultimately have "G t \<le> G 0 * exp (K * (t - 0))"
      by (rule derivative_quotient_bound)
        (auto intro!: continuous_intros g_cont G_pos `0 \<le> t` `t \<le> a` simp: field_simps pos)
  }
  also have "G 0 = C"
    by (simp add: G_def)
  finally show ?thesis
    by simp
qed

locale compact_continuously_diff =
  derivative_on_convex T X f "\<lambda>(t, x) (dt, dx). f' x dx"
    for T X and f::"(real \<times> 'a::{banach,perfect_space,heine_borel}) \<Rightarrow> 'a"
    and f'::"'a \<Rightarrow> 'a blinfun" +
  assumes compact_domain: "compact X"
  assumes continuous_derivative: "continuous_on X f'"
  assumes nonempty_domains: "T \<noteq> {}" "X \<noteq> {}"
begin

lemma
  f_comp_derivative[derivative_intros]:
  assumes "t \<in> T" "x \<in> X"
  shows "((\<lambda>a. f (t, a)) has_derivative blinfun_apply (f' x)) (at x within X)"
proof -
  have "(f o (\<lambda>a. (t, a)) has_derivative blinfun_apply (f' x)) (at x within X)"
    by (auto intro!: derivative_eq_intros refl has_derivative_within_subset[OF f'] assms)
  thus ?thesis by (simp add: o_def)
qed

lemma ex_onorm_bound:
  "\<exists>B. \<forall>x \<in> X. norm (f' x) \<le> B"
proof -
  from _ compact_domain have "compact (f' ` X)"
    apply (rule compact_continuous_image)
    apply (rule continuous_derivative)
    done
  hence "bounded (f' ` X)" by (rule compact_imp_bounded)
  thus ?thesis
    by (auto simp add: bounded_iff cball_def norm_blinfun.rep_eq)
qed

definition "onorm_bound = (SOME B. \<forall>x \<in> X. norm (f' x) \<le> B)"

lemma onorm_bound: assumes "x \<in> X" shows "norm (f' x) \<le> onorm_bound"
  unfolding onorm_bound_def
  using someI_ex[OF ex_onorm_bound] assms
  by blast

sublocale closed_domain X
  using compact_domain by unfold_locales (rule compact_imp_closed)

sublocale global_lipschitz T X f onorm_bound
proof (unfold_locales, rule lipschitzI)
  fix t z y
  assume "t \<in> T" "y \<in> X" "z \<in> X"
  hence "norm (f (t, y) - f (t, z)) \<le> onorm_bound * norm (y - z)"
    apply (intro differentiable_bound_generalized[where f'=f'])
    defer
    defer
    defer
    apply assumption
    apply assumption
    apply (rule convex)
    defer
    apply rule
    using onorm_bound
    by (auto intro!: derivative_eq_intros onorm_bound simp: norm_blinfun_def)
  thus "dist (f (t, y)) (f (t, z)) \<le> onorm_bound * dist y z"
    by (auto simp: dist_norm norm_Pair)
next
  from nonempty_domains obtain x where x: "x \<in> X" by auto
  show "0 \<le> onorm_bound"
    apply (rule order_trans)
    apply (rule onorm_pos_le)
    using onorm_bound[OF x]
    by (auto simp: norm_blinfun_def)
qed

end

locale unique_on_compact_continuously_diff = self_mapping i +
  compact_continuously_diff T X f
  for i::"'a::{banach,perfect_space,heine_borel} ivp"
begin

sublocale unique_on_closed i t1 onorm_bound
  by unfold_locales (auto intro!: f' has_derivative_continuous_on)

end

locale c1_on_open =
  fixes f::"'a::{banach, perfect_space, heine_borel} \<Rightarrow> 'a" and f' X
  assumes open_domain[simp]: "open X"
  assumes derivative_rhs: "\<And>x. x \<in> X \<Longrightarrow> (f has_derivative blinfun_apply (f' x)) (at x)"
  assumes continuous_derivative: "continuous_on X f'"
begin

lemma c1_on_open_rev[intro, simp]: "c1_on_open (-f) (-f') X"
  using derivative_rhs continuous_derivative
  by unfold_locales (auto intro!: continuous_intros derivative_eq_intros
    simp: fun_Compl_def)

lemma derivative_rhs_compose[derivative_intros]:
  "((g has_derivative g') (at x within s)) \<Longrightarrow> g x \<in> X \<Longrightarrow>
    ((\<lambda>x. f (g x)) has_derivative (\<lambda>xa. blinfun_apply (f' (g x)) (g' xa))) (at x within s)"
  by (metis has_derivative_compose[of g g' x s f "f' (g x)"] derivative_rhs)

sublocale local_lipschitz UNIV X "\<lambda>(t::real, x). f x"
proof (unfold_locales, safe)
  fix t::real and x::'a
  assume "t \<in> UNIV"
  assume "x \<in> X"
  with open_contains_cball[of "UNIV::real set"] open_UNIV
    open_contains_cball[of X] open_domain
  obtain u v where uv: "cball t u \<subseteq> UNIV" "cball x v \<subseteq> X" "u > 0" "v > 0"
    by blast
  let ?T = "cball t u" and ?X = "cball x v"
  have "bounded ?X" by simp
  have "compact (cball x v)"
    by simp
  interpret compact_continuously_diff ?T ?X "\<lambda>(t, x). f x" f'
    apply unfold_locales
    using uv
    apply (auto simp: convex_cball cball_eq_empty)
    apply (auto intro!: derivative_eq_intros simp: split_beta')
    defer
    apply (rule continuous_on_subset)
    apply (rule continuous_derivative)
    apply (rule uv)
    done
  have "lipschitz ?X f onorm_bound"
    using lipschitz[of t] uv
    by auto
  thus "\<exists>u>0. \<exists>L. \<forall>t'\<in>cball t u \<inter> UNIV. lipschitz (cball x u \<inter> X) f L"
    by (intro exI[where x=v]) (auto intro!: exI[where x=onorm_bound] `0 < v` simp: Int_absorb2 uv)
qed

subsection {* Autonomous IVP on maximal existence interval *}

context
  fixes x0
  assumes iv_in: "x0 \<in> X"
begin

definition "outer_ivp = \<lparr>
  ivp_f = (\<lambda>(t, x). f x),
  ivp_t0 = 0,
  ivp_x0 = x0,
  ivp_T = UNIV,
  ivp_X = X \<rparr>"

interpretation outer_ivp: ivp outer_ivp
  by default (auto simp: outer_ivp_def iv_in)

interpretation outer_ivp: ivp_open outer_ivp
  by default (auto simp: outer_ivp_def open_domain)

interpretation outer_ivp: continuous_rhs "ivp_T outer_ivp" "ivp_X outer_ivp" "ivp_f outer_ivp"
  by default (auto simp: outer_ivp_def intro!: has_derivative_continuous_on derivative_eq_intros)

interpretation outer_ivp: unique_on_open outer_ivp
  apply intro_locales
  apply (simp add: outer_ivp_def)
  apply unfold_locales
  done

definition "maximal_existence_bounds =
  (SOME (a::ereal, b::ereal). outer_ivp.maximal_existence_interval (real ` {a <..< b}))"

lemma maximal_existence_bounds:
  "outer_ivp.maximal_existence_interval (real ` {fst maximal_existence_bounds<..<snd maximal_existence_bounds})"
proof -
  obtain a b::ereal where "outer_ivp.maximal_existence_interval (real ` {a <..< b})"
    by (metis outer_ivp.maximal_existence_intervalE)
  hence "\<exists>x. case x of (a::ereal, b::ereal) \<Rightarrow> outer_ivp.maximal_existence_interval (real ` {a <..< b})"
    by (auto intro!: exI[where x="(a, b)"])
  from someI_ex[OF this]
  show "outer_ivp.maximal_existence_interval (real ` {fst maximal_existence_bounds<..<snd maximal_existence_bounds})"
    by (auto simp: maximal_existence_bounds_def)
qed

definition "inf_existence = fst maximal_existence_bounds"
definition "sup_existence = snd maximal_existence_bounds"

lemma inf_sup_existence:
  "outer_ivp.maximal_existence_interval (real ` {inf_existence<..<sup_existence})"
  by (simp add: inf_existence_def sup_existence_def maximal_existence_bounds)

definition "existence_ivl = real ` {inf_existence <..< sup_existence}"

lemma open_existence_ivl[simp]: "open existence_ivl"
  by (simp add: existence_ivl_def open_real_image)

lemma is_interval_existence_ivl[simp]: "is_interval existence_ivl"
  by (auto simp: existence_ivl_def is_interval_real_ereal_oo)

definition "existence_ivp = \<lparr>
  ivp_f = (\<lambda>(t, x). f x),
  ivp_t0 = 0,
  ivp_x0 = x0,
  ivp_T = existence_ivl,
  ivp_X = X \<rparr>"

lemma existence_ivp_simps[simp]:
  "ivp_f existence_ivp = (\<lambda>(t, x). f x)"
  "ivp_t0 existence_ivp = 0"
  "ivp_x0 existence_ivp = x0"
  "ivp_T existence_ivp = existence_ivl"
  "ivp_X existence_ivp = X"
  by (simp_all add: existence_ivp_def)

interpretation existence_ivp: ivp existence_ivp
  using inf_sup_existence[unfolded outer_ivp.maximal_existence_interval_def]
  by unfold_locales (auto simp: existence_ivl_def iv_in outer_ivp_def)

lemma existence_ivl_zero[intro, simp]: "0 \<in> existence_ivl"
  using existence_ivp.iv_defined
  by (auto simp: existence_ivp_def existence_ivl_def)

lemma existence_ivp: "unique_solution existence_ivp"
  using inf_sup_existence[unfolded outer_ivp.maximal_existence_interval_def]
  by (simp add: outer_ivp_def existence_ivp_def existence_ivl_def)

interpretation existence_ivp: unique_solution existence_ivp
  by (rule existence_ivp)

interpretation existence_ivp: unique_on_open existence_ivp
  apply unfold_locales
  apply (simp add: )
  using outer_ivp.openX apply simp
  using outer_ivp.lipschitz apply (simp add: outer_ivp_def)
proof auto
  case goal1
  from this(1)[THEN spec, of t, THEN bspec, OF goal1(3)]
  show ?case by auto
next
  case goal2
  have "(existence_ivl \<times> X) \<subseteq> ivp_T outer_ivp \<times> ivp_X outer_ivp"
    by (auto simp: outer_ivp_def)
  from continuous_on_subset[OF outer_ivp.continuous this]
  show ?case by (simp add: outer_ivp_def)
qed

lemma fixes a::real shows double_nonneg_le: "a * 2 \<le> b \<Longrightarrow> a \<ge> 0 \<Longrightarrow> a \<le> b"
  by arith

lemma
  local_unique_solutions:
  obtains t u L
  where "\<And>x. x \<in> cball x0 u \<Longrightarrow> unique_solution (existence_ivp \<lparr>ivp_x0 := x, ivp_T := cball 0 t, ivp_X := cball x u\<rparr>)"
    "\<And>x. x \<in> cball x0 u \<Longrightarrow> cball x u \<subseteq> X"
    "lipschitz (cball x0 (2 * u)) f L"
    "cball x0 (2 * u) \<subseteq> X"
    "0 < t" "0 < u"
proof -
  from existence_ivp.eventually_unique_solution
  obtain B L t where t: "0 < t"
  and ev:
    "eventually
      (\<lambda>e. 0 < e \<and>
        cball (existence_ivp.t0) (t * e) \<subseteq> existence_ivp.T \<and>
        cball (existence_ivp.x0) e \<subseteq> existence_ivp.X \<and>
        unique_on_cylinder (existence_ivp \<lparr>ivp_T := cball existence_ivp.t0 (t * e),
        ivp_X := cball existence_ivp.x0 e\<rparr>) (t * e) e B L (cball existence_ivp.x0 e))
      (at_right 0)" .
  from eventually_happens[OF ev] obtain e where e:
    "e > 0"
    "cball (existence_ivp.t0) (t * e) \<subseteq> existence_ivp.T"
    "cball (existence_ivp.x0) e \<subseteq> existence_ivp.X"
    "unique_on_cylinder (existence_ivp \<lparr>ivp_T := cball existence_ivp.t0 (t * e),
        ivp_X := cball existence_ivp.x0 e\<rparr>) (t * e) e B L (cball existence_ivp.x0 e)"
    by auto
  then interpret cyl!: unique_on_cylinder "existence_ivp \<lparr>ivp_T := cball existence_ivp.t0 (t * e),
    ivp_X := cball existence_ivp.x0 e\<rparr>" "t * e" e B L "cball existence_ivp.x0 e" by-assumption
  def e' \<equiv> "e / 2"
  have lips: "lipschitz (cball x0 (2 * e')) f L" "cball x0 (2 * e') \<subseteq> X"
    using cyl.global_lipschitz.lipschitz(1)[of 0] e t
    by (auto simp add: e'_def)
  from e t have e'_pos: "e' > 0" by (simp add: e'_def)
  with t have te_pos: "t * e' > 0" by simp
  {
    fix x0'::'a
    assume x0': "x0' \<in> cball x0 e'"
    let ?i' = "existence_ivp \<lparr>ivp_x0 := x0', ivp_T := cball 0 (t * e'), ivp_X := cball x0' e'\<rparr>"
    interpret cyl': cylinder ?i' "t * e'" e'
      using e'_pos t
      by unfold_locales (auto simp: dist_real_def)
    {
      fix b
      assume d: "dist x0' b \<le> e'"
      have "dist x0 b \<le> dist x0 x0' + dist x0' b"
        by (rule dist_triangle)
      also have "\<dots> \<le> e' + e'"
        using x0' d by simp
      also have "\<dots> \<le> e" by (simp add: e'_def)
      finally have "dist x0 b \<le> e" .
    } note triangle = this

    have subs1: "cball 0 (t * e') \<subseteq> cball 0 (t * e)"
      and subs2: "cball x0' e' \<subseteq> cball x0 e"
      and subs: "cball 0 (t * e') \<times> cball x0' e' \<subseteq> cball 0 (t * e) \<times> cball x0 e"
      using e'_pos x0'
      by (auto simp: e'_def triangle dest!: double_nonneg_le)
    interpret cyl': solution_in_cylinder ?i' "t * e'"  e' B
      using cyl.norm_f cyl.e_bounded cyl.continuous subs
      by unfold_locales (force simp: e'_def intro: continuous_on_subset)+
    interpret cyl': unique_on_cylinder ?i' "t * e'" e' B L "(cball x0 e)"
      using cyl.global_lipschitz.lipschitz(1)[simplified, of 0] t cyl.global_lipschitz.lipschitz e'_pos x0' subs
      by unfold_locales (auto simp: e'_def triangle)
    have un: "unique_solution ?i'"
      by unfold_locales
    from subs2 e have subs: "cball x0' e' \<subseteq> X" by simp
    note un this
  } thus thesis using lips te_pos e'_pos ..
qed

definition "flow t = existence_ivp.solution t"

lemma in_existence_between_zeroI: "t \<in> existence_ivl \<Longrightarrow> s \<in> {t..0} \<union> {0..t} \<Longrightarrow> s \<in> existence_ivl"
  apply (auto simp: existence_ivl_def dest!: )
  apply (rule_tac x="ereal s" in image_eqI)
  apply auto
  apply (case_tac x)
  apply auto
  apply (metis less_ereal.simps(1) less_trans sup.semilattice_strict_iff_order)
  apply (case_tac x)
  using existence_ivl_zero[simplified existence_ivl_def]
  apply auto
  apply (case_tac xa)
  apply auto
  apply (metis dual_order.strict_trans2 ereal_less_eq(3))
  apply (rule_tac x="ereal s" in image_eqI)
  apply auto
  apply (case_tac x)
  apply auto
  apply (case_tac xa)
  apply auto
  apply (metis ereal_less_eq(3) order.strict_trans2)
  apply (case_tac x)
  apply auto
  apply (case_tac xa)
  apply auto
  by (metis less_ereal.simps(1) less_trans sup.semilattice_strict_iff_order)

lemma flow_in_domain: "t \<in> existence_ivl \<Longrightarrow> flow t \<in> X"
  using existence_ivp.is_solutionD[OF existence_ivp.is_solution_solution]
  by (auto simp: flow_def)

lemma maximal_existence_flow:
  assumes "ivp.is_solution i x"
  assumes "i = \<lparr> ivp_f = (\<lambda>(t, x). f x), ivp_t0 = 0, ivp_x0 = x0, ivp_T = K, ivp_X = X \<rparr>"
  assumes "is_interval K"
  assumes "0 \<in> K"
  shows "K \<subseteq> existence_ivl"
    "\<And>t. t \<in> K \<Longrightarrow> flow t = x t"
  using inf_sup_existence[unfolded outer_ivp.maximal_existence_interval_def] assms
  by (auto simp add: outer_ivp_def existence_ivp_def flow_def existence_ivl_def)

lemma maximal_existence_flow_shifted:
  assumes "ivp i"
  assumes "ivp.is_solution i x"
  assumes "ivp_f i = ivp_f existence_ivp"
  assumes "ivp_T i = K"
  assumes "ivp_X i = X"
  assumes "x t0 = x0"
  assumes "is_interval K"
  assumes "t0 \<in> K"
  shows "op + (-t0) ` K \<subseteq> existence_ivl"
    "\<And>t s. s \<in> K \<Longrightarrow> s = t0 + t \<Longrightarrow> flow t = x s"
proof -
  interpret i: ivp i by fact
  interpret i: has_solution i
    by unfold_locales (blast intro: assms)
  let ?ex_res = "existence_ivp \<lparr>ivp_T := op + (-t0) ` K\<rparr>"
  have image_collapse: "op + t0 ` op + (- t0) ` K = K"
    by force
  interpret ex_res: ivp ?ex_res
    by unfold_locales (auto simp: `x0 \<in> X`, auto simp: assms)
  have ex_res_sol: "ex_res.is_solution (x \<circ> op + t0)"
    apply (rule ex_res.is_solutionI)
    using i.is_solutionD[OF assms(2)]
    apply (auto simp: o_def assms)
    apply (subst o_def[symmetric]) back back --"TODO: make ex-res-sol a separate lemma, stronger than @{thm ivp.shift_autonomous_solution}"
    apply (rule vector_diff_chain_within[THEN vector_derivative_eq_rhs])
    apply (auto simp: o_def assms ac_simps image_collapse has_vector_derivative_def
      intro!: derivative_eq_intros)
    done
  then interpret ex_res: has_solution ?ex_res
    by unfold_locales blast
  from ex_res_sol
  show "op + (- t0) ` K \<subseteq> existence_ivl"
    by (rule maximal_existence_flow) (auto simp: assms is_interval_translation)
  fix t s assume s: "s \<in> K" "s = t0 + t" hence t: "t \<in> op + (-t0) ` K" by force
  from ex_res_sol
  have "flow t = (x o (op + t0)) t"
    by (rule maximal_existence_flow[where K=ex_res.T]) (auto simp: assms is_interval_translation t)
  thus "flow t = x s" by (simp add: s)
qed

lemma unique_on_intersection:
  assumes "t \<in> ivp_T i \<inter> ivp_T j"
  assumes "has_solution i"
  assumes "has_solution j"
  assumes "ivp_X i = ivp_X existence_ivp"
  assumes "ivp_X j = ivp_X existence_ivp"
  assumes "ivp_f i = ivp_f existence_ivp"
  assumes "ivp_f j = ivp_f existence_ivp"
  assumes "is_interval (ivp_T i)"
  assumes "is_interval (ivp_T j)"
  assumes "ti \<in> ivp_T i \<inter> ivp_T j"
  assumes "ivp.solution i ti = x0"
  assumes "ivp.solution j ti = x0"
  shows "ivp.solution i t = ivp.solution j t"
proof -
  interpret i: has_solution i by fact
  interpret j: has_solution j by fact
  have [simp]: "ivp i" "ivp j" by unfold_locales
  have "flow (t - ti) = i.solution t"
    using assms
    by (intro maximal_existence_flow_shifted) (auto simp: assms)
  moreover
  have "flow (t - ti) = j.solution t"
    using assms
    by (intro maximal_existence_flow_shifted) (auto simp: assms)
  ultimately show ?thesis by simp
qed

lemma flow_zero[simp]: "flow 0 = x0"
  using existence_ivp.is_solutionD(1)[OF existence_ivp.is_solution_solution]
  by (auto simp: flow_def existence_ivp_def)

lemma flow_has_derivative:
  assumes "t \<in> existence_ivl"
  shows "(flow has_derivative (\<lambda>i. i *\<^sub>R f (flow t))) (at t)"
proof -
  have "(flow has_derivative (\<lambda>i. i *\<^sub>R f (flow t))) (at t within existence_ivl)"
    using existence_ivp.solution_has_deriv[of t] assms
    unfolding flow_def[abs_def]
    by (auto simp: has_vector_derivative_def)
  thus ?thesis
    by (simp add: at_within_open[OF assms open_existence_ivl])
qed


lemma
  flow_eq_rev:
  assumes "t \<in> existence_ivl"
  shows "flow t = c1_on_open.flow (- f) X x0 (- t)" "- t \<in> c1_on_open.existence_ivl (- f) X x0"
proof -
  interpret rev!: c1_on_open "-f" "-f'" ..
  have "ivp.solution existence_ivp \<circ> uminus = (\<lambda>t. flow (- t))"
    by (auto simp: flow_def)
  with existence_ivp.mirror_solution[OF existence_ivp.is_solution_solution, simplified]
  have *: "ivp.is_solution (existence_ivp \<lparr>ivp_f := \<lambda>(t, x). (- f) x, ivp_T := uminus ` existence_ivl\<rparr>)
     (\<lambda>t. flow (- t))"
     by auto
  from rev.maximal_existence_flow[where K="uminus ` existence_ivl", OF `x0 \<in> X` *]
  have "uminus ` existence_ivl \<subseteq> c1_on_open.existence_ivl (- f) X x0"
    "\<And>t. t \<in> uminus ` existence_ivl \<Longrightarrow> c1_on_open.flow (- f) X x0 t = flow (- t)"
    by auto
  thus "flow t = rev.flow x0 (-t)" "-t \<in> rev.existence_ivl x0"
    using assms by auto
qed

lemma rev_flow_eq: "t \<in> c1_on_open.existence_ivl (- f) X x0 \<Longrightarrow> c1_on_open.flow (- f) X x0 t = flow (-t)"
  and rev_existence_ivl_eq: "t \<in> c1_on_open.existence_ivl (- f) X x0 <-> - t \<in> existence_ivl"
proof -
  interpret rev!: c1_on_open "-f" "-f'" ..
  from rev.flow_eq_rev[OF `x0 \<in> X`, of t] flow_eq_rev[of "-t"]
  show "t \<in> c1_on_open.existence_ivl (- f) X x0 \<Longrightarrow> c1_on_open.flow (- f) X x0 t = flow (-t)"
    "t \<in> c1_on_open.existence_ivl (- f) X x0 <-> - t \<in> existence_ivl"
    by (auto simp: fun_Compl_def `x0 \<in> X`)
qed

end

lemma
  assumes s: "s \<in> existence_ivl x0"
  assumes t: "t \<in> existence_ivl (flow x0 s)"
  assumes [simp]: "x0 \<in> X"
  shows flow_trans: "flow x0 (s + t) = flow (flow x0 s) t"
    and existence_ivl_trans: "s + t \<in> existence_ivl x0"
proof -
  from existence_ivp[OF `x0 \<in> X`]
  interpret u0: unique_solution "existence_ivp x0" .
  let ?u0r = "(existence_ivp x0)\<lparr>ivp_T:=if s \<ge> 0 then {0..s} else {s..0}\<rparr>"
  interpret u0r: ivp ?u0r
    by unfold_locales auto
  interpret u0r: has_solution ?u0r
    apply unfold_locales
    apply (rule exI)
    apply (rule u0.solution_on_subset[OF _ _ u0.is_solution_solution])
    apply (auto intro!: in_existence_between_zeroI[OF `x0 \<in> X` s])
    done
  note flow_in_domain[OF `x0 \<in> X` s, simp]
  from existence_ivp[OF this]
  interpret u1: unique_solution "existence_ivp (flow x0 s)" by simp
  let ?u1 = "(existence_ivp (flow x0 s))\<lparr>ivp_T:=if t \<ge> 0 then {0..t} else {t..0}\<rparr>"
  interpret u1r: ivp ?u1
    by unfold_locales auto
  interpret u1r: has_solution ?u1
    apply unfold_locales
    apply (rule exI)
    apply (rule u1.solution_on_subset[OF _ _ u1.is_solution_solution])
    apply (auto intro!: in_existence_between_zeroI[OF `(flow x0 s) \<in> X` t])
    done
  let ?u1s = "(existence_ivp (flow x0 s))\<lparr>ivp_t0:=s, ivp_T:=if t \<ge> 0 then {s..s + t} else {s + t..s}\<rparr>"
  interpret u1s: ivp ?u1s
    by unfold_locales auto
  interpret u1s: has_solution ?u1s
    apply unfold_locales
    apply (rule exI)
    using u1r.is_solution_solution
    apply (rule u1r.shift_autonomous_solution)
    apply (auto simp add: image_add_atLeastAtMost)
    done
  let ?c = "(existence_ivp x0)\<lparr>ivp_T:=ivp_T ?u0r \<union> ivp_T ?u1s\<rparr>"
  interpret conn: ivp ?c
    by unfold_locales auto
  interpret conn: connected_solutions ?c ?u0r ?u1s u0r.solution
  proof unfold_locales
    show "u0r.is_solution u0r.solution" by simp
  next
    assume "conn.t0 \<notin> u0r.T"
    thus "u1s.solution conn.t0 = conn.x0"
      by (simp split: split_if_asm)
  next
    assume "conn.t0 \<in> u0r.T"
    thus "u0r.solution conn.t0 = conn.x0"
      using u0r.solution_t0
      by (simp split: split_if_asm)
  next
    fix t assume t: "t \<in> u0r.T \<inter> u1s.T"
    have fr: "flow x0 s = u0r.solution s"
     by (intro maximal_existence_flow[OF `x0 \<in> X`, where i="?u0r" and K="ivp_T ?u0r"])
       (auto simp: is_interval_closed_interval)
    have fs: "flow x0 s = u1s.solution s"
      using u1s.solution_t0
      by simp
    from t show "u0r.solution t = u1s.solution t"
      apply (rule unique_on_intersection[OF `flow x0 s \<in> X`])
      apply fact apply fact
      apply simp
      apply simp
      apply simp
      apply simp
      apply (simp add: is_interval_closed_interval)
      apply (simp add: is_interval_closed_interval)
      apply (auto simp: is_interval_closed_interval s)
      using fr[symmetric] fs[symmetric]
      apply auto
      done
  qed auto
  have "flow x0 (s + t) = (conn.connection (s + t))"
    by (rule maximal_existence_flow[OF `x0 \<in> X` conn.is_solution_connection, where K="ivp_T ?c"])
      (auto simp: is_interval_closed_interval is_real_interval_union)
  also have "conn.connection (s + t) = u1s.solution (s + t)"
    by (rule conn.connection_eq_solution2) simp
  also
  from u1s.is_solution_solution
  have "u1r.is_solution (u1s.solution o op + s)"
    by (rule u1s.shift_autonomous_solution) (auto simp: o_def ac_simps image_add_atLeastAtMost)
  hence "flow (flow x0 s) t = ((u1s.solution o op + s) t)"
    by (rule maximal_existence_flow(2)[OF `(flow x0 s) \<in> X`, where K="ivp_T ?u1"])
      (auto simp: is_interval_closed_interval is_real_interval_union)
  then have "u1s.solution (s + t) = flow (flow x0 s) t"
    by simp
  finally show "flow x0 (s + t) = flow (flow x0 s) t" .
  have "s + t \<in> conn.T"
    by simp
  also have "\<dots> \<subseteq> existence_ivl x0" using conn.is_solution_connection
    by (rule maximal_existence_flow[OF `x0 \<in> X`])
      (auto simp: is_interval_closed_interval is_real_interval_union)
  finally show "s + t \<in> existence_ivl x0" .
qed

lemma
  assumes t: "t \<in> existence_ivl x0"
  assumes [simp]: "x0 \<in> X"
  shows flows_reverse: "flow (flow x0 t) (-t) = x0"
    and existence_ivl_reverse: "-t \<in> existence_ivl (flow x0 t)"
proof -
  from existence_ivp[OF `x0 \<in> X`]
  interpret u0: unique_solution "existence_ivp x0" .

  note flow_in_domain[OF `x0 \<in> X` t]
  from existence_ivp[OF this]
  interpret u1: unique_solution "existence_ivp (flow x0 t)" .

  have in_existenceI: "\<And>x. x \<in> (if t \<ge> 0 then {0 .. t} else {t .. 0}) \<Longrightarrow> x \<in> existence_ivl x0"
    by (rule in_existence_between_zeroI[OF `x0\<in>X` t]) (force split: split_if_asm)
  hence existence_superset: "op + t ` (if t \<ge> 0 then {-t .. 0} else {0 .. -t}) \<subseteq>
      ivp_T (c1_on_open.existence_ivp f X x0)"
    by auto

  have is_sol: "ivp.is_solution
     \<lparr>ivp_f = \<lambda>(t, x). f x, ivp_t0 = 0, ivp_x0 = flow x0 t, ivp_T = if 0 \<le> t then {- t..0} else {0..- t}, ivp_X = X\<rparr>
     (ivp.solution (c1_on_open.existence_ivp f X x0) \<circ> op + t)"
    apply (rule ivp.is_solutionI)
    apply unfold_locales
    apply simp
    apply simp
    apply (metis `flow x0 t \<in> X`)
    apply (simp add: flow_def)
    apply (rule has_vector_derivative_within_subset)
    apply (rule vector_diff_chain_within[THEN vector_derivative_eq_rhs])
    apply (force simp: has_vector_derivative_def intro!: derivative_eq_intros)
    apply (rule has_vector_derivative_within_subset)
    apply (rule u0.is_solutionD[OF u0.is_solution_solution])
    apply simp
    apply (rule in_existenceI) apply force
    apply (rule existence_superset)
    apply (auto split: split_if_asm intro!: u0.is_solutionD[OF u0.is_solution_solution, simplified] in_existenceI)
    done
  hence "flow (flow x0 t) (-t) = ((u0.solution o op + t)(-t))"
    by (rule maximal_existence_flow[OF `flow x0 t \<in> X`])
      (auto simp: is_interval_closed_interval)
  thus "flow (flow x0 t) (-t) = x0"
    using u0.solution_t0
    by simp
  have "-t \<in> (if t \<ge> 0 then {-t .. 0} else {0 .. -t})"
    by auto
  also have "\<dots> \<subseteq> existence_ivl (flow x0 t)" using is_sol
    by (rule maximal_existence_flow[OF `flow x0 t \<in> X`]) (auto simp: is_interval_closed_interval)
  finally show "-t \<in> existence_ivl (flow x0 t)" .
qed


lemma
  assumes iv: "x t0 = flow x0 s"
  assumes deriv: "\<And>t. t \<in> T \<Longrightarrow> (x has_vector_derivative f (x t)) (at t within T)"
  assumes dom: "\<And>t. t \<in> T \<Longrightarrow> x t \<in> X"
  assumes tx: "tx = t0 + t - s"
  assumes subs: "{t0 .. tx} \<union> {tx .. t0} \<subseteq> T"
  assumes s: "s \<in> existence_ivl x0"
  assumes [simp]: "x0 \<in> X"
  shows flow_eqI: "flow x0 t = x tx"
    and in_existence_ivlI: "t \<in> existence_ivl x0"
proof -
  have [simp]: "flow x0 s \<in> X"
    by (metis assms(7) flow_in_domain s)
  let ?i = "\<lparr>ivp_f = (\<lambda>(t, x). f x), ivp_t0 = t0, ivp_x0 = x t0, ivp_T = {t0 .. tx} \<union> {tx .. t0}, ivp_X = X\<rparr>"
  interpret ivp ?i
    using subs
    by unfold_locales (auto intro!: dom dest!: contra_subsetD)
  have x_sol: "is_solution x"
    using subs
    by (intro is_solutionI) (auto intro!:
      has_vector_derivative_within_subset[where s = T and t="{t0..tx}\<union>{tx .. t0}"] deriv dom)
  interpret has_solution ?i
    by unfold_locales (blast intro: x_sol)
  have "t - s \<in> op + (-t0) ` ({t0 .. tx} \<union> {tx .. t0})"
    by (force simp: tx)
  also have "\<dots> \<subseteq> existence_ivl (flow x0 s)"
    apply (rule maximal_existence_flow_shifted[where i = ?i])
    apply (metis assms(7) flow_in_domain s)
    apply fact apply fact
    apply simp
    apply simp
    apply simp
    defer
    apply (rule is_real_interval_union)
    apply (simp add: is_interval_closed_interval)
    apply (simp add: is_interval_closed_interval)
    apply (simp add: tx)
    apply (simp add: tx algebra_simps le_cases)
    apply (metis le_cases)
    using solution_t0
    apply (simp add: iv)
    done
  finally have diff: "t - s \<in> existence_ivl (flow x0 s)" .
  have "flow x0 t = flow x0 (s + (t - s))" by simp
  also have "\<dots> = flow (flow x0 s) (t - s)"
    apply (subst flow_trans)
    apply (rule s)
    apply (auto simp: `x0 \<in> X` diff)
    done
  also have "\<dots> = x tx"
    apply (rule maximal_existence_flow_shifted[where i = ?i])
    apply simp
    apply fact
    apply fact
    apply simp
    apply simp
    apply simp
    apply (rule iv)
    apply (rule is_real_interval_union)
    apply (auto simp: is_real_interval_union is_interval_closed_interval tx)
    done
  finally show "flow x0 t = x tx" .
  have "s + (t - s) \<in> existence_ivl x0"
    by (rule existence_ivl_trans) (auto simp: diff s)
  thus "t \<in> existence_ivl x0" by simp
qed

lemma flow_has_vector_derivative:
  assumes "x \<in> X" "t \<in> existence_ivl x"
  shows "(flow x has_vector_derivative f (flow x t)) (at t)"
  using flow_has_derivative[OF assms]
  by (simp add: has_vector_derivative_def)

lemma flow_has_vector_derivative_at_0:
  assumes "x \<in> X" "t \<in> existence_ivl x"
  shows "((\<lambda>h. flow x (t + h)) has_vector_derivative f (flow x t)) (at 0)"
proof -
  from flow_has_vector_derivative[OF assms]
  have
    "(op + t has_vector_derivative 1) (at 0)"
    "(flow x has_vector_derivative f (flow x t)) (at (t + 0))"
    by (auto intro!: derivative_eq_intros)
  from vector_diff_chain_at[OF this]
  show ?thesis by (simp add: o_def)
qed

lemma
  assumes in_domain: "x \<in> X"
  assumes "t \<in> existence_ivl x"
  shows ivl_subset_existence_ivl: "{0 .. t} \<subseteq> existence_ivl x"
    and ivl_subset_existence_ivl': "{t .. 0} \<subseteq> existence_ivl x"
    and closed_segment_subset_existence_ivl: "closed_segment 0 t \<subseteq> existence_ivl x"
  using assms
  by (auto simp: closed_segment_real intro: is_interval_existence_ivl[OF in_domain, THEN mem_is_intervalI, of 0 t])

lemma flow_fixed_point:
  assumes t: "0 \<le> t" "t \<in> existence_ivl x"
  assumes "x \<in> X"
  shows "flow x t = x + integral {0..t} (\<lambda>t. f (flow x t))"
proof -
  have "\<forall>s\<in>{0 .. t}. (flow x has_vector_derivative f (flow x s)) (at s within {0 .. t})"
    using ivl_subset_existence_ivl[OF `x \<in> X` t(2)]
    by (auto intro!: flow_has_vector_derivative[OF `x \<in> X`] intro: has_vector_derivative_at_within)
  from fundamental_theorem_of_calculus[OF t(1) this]
  have "((\<lambda>t. f (flow x t)) has_integral flow x t - flow x 0) {0..t}"
    by simp
  from this[THEN integral_unique]
  show ?thesis by (simp add: `x \<in> X`)
qed

lemma flow_fixed_point':
  assumes t: "t \<le> 0" "t \<in> existence_ivl x"
  assumes "x \<in> X"
  shows "flow x t = x - integral {t..0} (\<lambda>t. f (flow x t))"
proof -
  have "\<forall>s\<in>{t .. 0}. (flow x has_vector_derivative f (flow x s)) (at s within {t .. 0})"
    using ivl_subset_existence_ivl'[OF `x \<in> X` t(2)]
    by (auto intro!: flow_has_vector_derivative[OF `x \<in> X`] intro: has_vector_derivative_at_within)
  from fundamental_theorem_of_calculus[OF t(1) this]
  have "((\<lambda>t. f (flow x t)) has_integral flow x 0 - flow x t) {t .. 0}"
    by simp
  from this[THEN integral_unique]
  show ?thesis by (simp add: `x \<in> X` algebra_simps)
qed

lemma flow_fixed_point'':
  assumes t: "t \<in> existence_ivl x"
  assumes "x \<in> X"
  shows "flow x t = x + (if 0 \<le> t then 1 else -1) *\<^sub>R integral (closed_segment 0 t) (\<lambda>t. f (flow x t))"
  using assms
  by (auto simp add: closed_segment_real flow_fixed_point flow_fixed_point')

lemma f_continuous: "x \<in> X \<Longrightarrow> continuous (at x) f"
  apply (rule has_derivative_continuous)
  apply (rule derivative_rhs)
  apply assumption
  done

lemma f_continuous_on: "continuous_on X f"
  by (auto intro!: f_continuous continuous_at_imp_continuous_on)

lemma flow_continuous: "x \<in> X \<Longrightarrow> t \<in> existence_ivl x \<Longrightarrow> continuous (at t) (flow x)"
  apply (rule has_derivative_continuous)
  apply (rule flow_has_derivative)
  apply assumption+
  done

lemma flow_tendsto: "x \<in> X \<Longrightarrow> t0 \<in> existence_ivl x \<Longrightarrow> (t ---> t0) F \<Longrightarrow> ((\<lambda>s. flow x (t s)) ---> flow x t0) F"
  by (rule isCont_tendsto_compose[OF flow_continuous, of x t0 t F])

lemma flow_continuous_on: "x \<in> X \<Longrightarrow> continuous_on (existence_ivl x) (flow x)"
  by (auto intro!: flow_continuous continuous_at_imp_continuous_on)

lemma f_flow_continuous:
  assumes "t \<in> existence_ivl x" "x \<in> X"
  shows "isCont (\<lambda>t. f (flow x t)) t"
proof -
  have "isCont (f o (\<lambda>t. flow x t)) t"
    apply (rule continuous_intros)
    apply (auto intro!:  assms flow_continuous f_continuous flow_in_domain
      continuous_within_subset[OF f_continuous])
    done
  thus ?thesis by (simp add: o_def)
qed

lemma exponential_initial_condition_nonneg:
  assumes "t \<ge> 0"
  assumes y0: "t \<in> existence_ivl y0" and "y0 \<in> Y"
  assumes z0: "t \<in> existence_ivl z0" and "z0 \<in> Y"
  assumes "Y \<subseteq> X"
  assumes remain: "\<And>s. s \<in> {0 .. t} \<Longrightarrow> flow y0 s \<in> Y" "\<And>s. s \<in> {0 .. t} \<Longrightarrow> flow z0 s \<in> Y"
  assumes lipschitz: "lipschitz Y f K"
  shows "norm (flow y0 t - flow z0 t) \<le> norm (y0 - z0) * exp ((K + 1) * t)"
proof cases
  assume "y0 = z0"
  thus ?thesis
    by simp
next
  assume ne: "y0 \<noteq> z0"
  def K' \<equiv> "K + 1"
  from lipschitz have "lipschitz Y f K'"
  proof (auto simp: lipschitz_def K'_def)
    case goal1
    hence "dist (f x) (f y) \<le> K * dist x y"
      by auto
    also have "\<dots> \<le> (K + 1) * dist x y"
      by (rule mult_right_mono) auto
    finally show ?case .
  qed
  from assms have inX: "y0 \<in> X" "z0 \<in> X" by auto
  def v \<equiv> "\<lambda>t. norm (flow y0 t - flow z0 t)"
  {
    fix s
    assume s: "s \<in> {0 .. t}" hence "s \<ge> 0" by auto
    with s ivl_subset_existence_ivl[OF `y0 \<in> X` y0]  ivl_subset_existence_ivl[OF `z0 \<in> X` z0]
    have
      y0': "s \<in> existence_ivl y0" and
      z0': "s \<in> existence_ivl z0"
      by auto
    have int: "flow y0 s - flow z0 s = y0 - z0 + integral {0 .. s} (\<lambda>t. f (flow y0 t) - f (flow z0 t))"
      unfolding v_def
      apply (subst flow_fixed_point[OF `s \<ge> 0` y0' `y0 \<in> X`])
      apply (subst flow_fixed_point[OF `s \<ge> 0` z0' `z0 \<in> X`])
      apply (auto simp: algebra_simps)
      apply (subst integral_sub)
      using ivl_subset_existence_ivl[OF `y0 \<in> X` y0'] ivl_subset_existence_ivl[OF `z0 \<in> X` z0']
      apply (auto intro!: integrable_continuous_real continuous_at_imp_continuous_on f_flow_continuous
        `y0 \<in> X` `z0 \<in> X`)
      done
    have "v s \<le> v 0 + K' *  integral {0 .. s} (\<lambda>t. v t)"
      using ivl_subset_existence_ivl[OF `y0 \<in> X` y0'] ivl_subset_existence_ivl[OF `z0 \<in> X` z0'] s
      by (subst integral_mult) (auto simp add: integral_mult v_def int inX intro!: norm_triangle_le integral_norm_bound_integral
        integrable_continuous_real continuous_intros continuous_at_imp_continuous_on flow_continuous
        f_flow_continuous lipschitz_norm_leI[OF `lipschitz _ _ K'`] remain)
  } note le = this
  have cont: "continuous_on {0..t} v"
    using ivl_subset_existence_ivl[OF `y0 \<in> X` y0] ivl_subset_existence_ivl[OF `z0 \<in> X` z0] inX
    by (auto simp: v_def intro!: continuous_at_imp_continuous_on continuous_intros flow_continuous)
  have nonneg: "\<And>t. v t \<ge> 0"
    by (auto simp: v_def)
  from ne have pos: "v 0 > 0"
    by (auto simp: v_def inX)
  have lippos: "K' > 0"
  proof -
    have "0 \<le> dist (f y0) (f z0)" by simp
    also from lipschitzD[OF lipschitz `y0 \<in> Y` `z0 \<in> Y`] ne
    have "\<dots> \<le> K * dist y0 z0"
      by simp
    finally have "0 \<le> K"
      by (metis dist_le_zero_iff ne zero_le_mult_iff)
    thus ?thesis by (simp add: K'_def)
  qed
  from gronwall[OF le cont nonneg pos lippos]
  have "v t \<le> v 0 * exp (K' * t)"
    using `0 \<le> t` by simp
  thus ?thesis
    by (simp add: v_def K'_def inX)
qed

lemma lipschitz_minus_fun: "lipschitz Y (- f) K \<longleftrightarrow> lipschitz Y f K"
  by (auto simp: lipschitz_def dist_minus)

lemma exponential_initial_condition:
  assumes y0: "t \<in> existence_ivl y0" and "y0 \<in> Y"
  assumes z0: "t \<in> existence_ivl z0" and "z0 \<in> Y"
  assumes "Y \<subseteq> X"
  assumes remain: "\<And>s. s \<in> closed_segment 0 t \<Longrightarrow> flow y0 s \<in> Y" "\<And>s. s \<in> closed_segment 0 t \<Longrightarrow> flow z0 s \<in> Y"
  assumes lipschitz: "lipschitz Y f K"
  shows "norm (flow y0 t - flow z0 t) \<le> norm (y0 - z0) * exp ((K + 1) * abs t)"
  using assms
proof cases
  assume "0 \<le> t"
  have "norm (flow y0 t - flow z0 t) \<le> norm (y0 - z0) * exp ((K + 1) * t)"
    apply (rule exponential_initial_condition_nonneg)
    apply fact apply fact apply fact apply fact apply fact apply fact
    using remain lipschitz apply (auto simp: closed_segment_real)
    done
  thus ?thesis
    using `0 \<le> t` by simp
next
  have "y0 \<in> X" "z0 \<in> X" using assms by auto
  {
    fix s y0 Y assume "y0 \<in> X" and remain: "\<And>s. s \<in> closed_segment 0 t \<Longrightarrow> flow y0 s \<in> Y"
      and y0: "t \<in> existence_ivl y0"
      and s: "s \<in> {0..- t}"
    have "c1_on_open.flow (- f) X y0 s = c1_on_open.flow (- f) X y0 (- (- s))" by simp
    also have "\<dots> = flow y0 (- s)"
      apply (rule flow_eq_rev(1)[symmetric])
      apply fact
      by (metis `y0 \<in> X` `s \<in> {0..- t}` atLeastAtMost_iff contra_subsetD ivl_subset_existence_ivl' minus_minus neg_le_0_iff_le neg_le_iff_le y0)
    also have "\<dots> \<in> Y"
      apply (rule remain)
      using s by (simp add: closed_segment_real)
    finally
    have "c1_on_open.flow (- f) X y0 s \<in> Y"
      .
  } note remain_rev = this
  interpret rev: c1_on_open "-f" "-f'" ..
  assume "\<not> t \<ge> 0"
  hence "0 \<le> - t" by simp
  hence "norm (rev.flow y0 (-t) - rev.flow z0 (-t)) \<le>
    norm (y0 - z0) * exp ((K + 1) * (- t))"
    apply (rule rev.exponential_initial_condition_nonneg)
    apply (rule flow_eq_rev[OF `y0 \<in> X` y0])
    apply fact
    apply (rule flow_eq_rev[OF `z0 \<in> X` z0])
    apply fact
    apply fact
    apply (rule remain_rev)
    apply (rule `y0 \<in> X`)
    apply (rule remain) apply assumption
    apply (rule y0) apply assumption
    apply (rule remain_rev)
    apply (rule `z0 \<in> X`)
    apply (rule remain) apply assumption
    apply (rule z0) apply assumption
    unfolding lipschitz_minus_fun
    apply fact
    done
  thus ?thesis
    using `0 \<le> - t`
    by (simp add: flow_eq_rev[OF `y0 \<in> X` y0] flow_eq_rev[OF `z0 \<in> X` z0])
qed

lemma
  existence_ivl_cballs:
  fixes x assumes "x \<in> X"
  obtains t u L
  where
    "\<And>y. y \<in> cball x u \<Longrightarrow> cball 0 t \<subseteq> existence_ivl y"
    "\<And>s y. y \<in> cball x u \<Longrightarrow> s \<in> cball 0 t \<Longrightarrow> flow y s \<in> cball y u"
    "lipschitz (cball 0 t\<times>cball x u) (\<lambda>(t, x). flow x t) L"
    "\<And>y. y \<in> cball x u \<Longrightarrow> cball y u \<subseteq> X"
    "0 < t" "0 < u"
proof -
  from local_unique_solutions[OF `x \<in> X`]
  obtain t u L where usol: "\<And>y. y \<in> cball x u \<Longrightarrow>
    unique_solution (c1_on_open.existence_ivp f X x \<lparr>ivp_x0 := y, ivp_T := cball 0 t, ivp_X := cball y u\<rparr>)"
    and subs: "\<And>y. y \<in> cball x u \<Longrightarrow> cball y u \<subseteq> X"
    and lipschitz: "lipschitz (cball x (2*u)) f L"
    and subs': "cball x (2 * u) \<subseteq> X"
    and tu: "0 < t" "0 < u"
    by metis
  {
    fix y assume y: "y \<in> cball x u"
    from subs[OF y] `0 < u` have "y \<in> X" by auto
    from usol[OF y] interpret unique_solution
      "(c1_on_open.existence_ivp f X x \<lparr>ivp_x0 := y, ivp_T := cball 0 t, ivp_X := cball y u\<rparr>)"
      .
    have "cball 0 t \<subseteq> existence_ivl y"
      using `y \<in> X`
      apply (rule maximal_existence_flow)
      apply (rule is_solution_on_superset_domain[where X'=X])
      apply (rule is_solution_solution)
      defer
      using `0 < t` subs y
      by (auto simp: is_interval_closed_interval existence_ivp_def[OF `x \<in> X`])
    note eivl = this
    {
      fix s::real assume s: "s \<in> cball 0 t"
      have "flow y s = solution s"
        apply (rule maximal_existence_flow)
        apply fact
        apply (rule is_solution_on_superset_domain[where X'=X])
        apply (rule is_solution_solution)
        apply simp
        apply (rule subs)
        apply (rule y)
        apply (simp add: existence_ivp_def[OF `x \<in> X`])
        using s tu
        by (auto simp: is_interval_closed_interval)
      also
      from s is_solutionD(3)[OF is_solution_solution]
      have "\<dots> \<in> cball y u"
        by (auto simp del: mem_cball)
      finally have "flow y s \<in> cball y u" .
    }
    note eivl this
  } note * = this
  note *
  moreover
  have cont_on_f_flow: "\<And>x1 S. S \<subseteq> cball 0 t \<Longrightarrow> x1 \<in> cball x u \<Longrightarrow> continuous_on S (\<lambda>t. f (flow x1 t))"
    using subs[of x] `u > 0` *(1)
    by (auto intro!: continuous_at_imp_continuous_on f_flow_continuous)
  from compact_imp_bounded[OF compact_continuous_image[OF lipschitz_imp_continuous_on[OF lipschitz], OF compact_cball]]
  obtain B where B: "\<And>y. y \<in> cball x (2 * u) \<Longrightarrow> norm (f y) \<le> B" "B > 0"
    by (auto simp: bounded_pos cball_def)
  {
    fix s::real and x1 assume s: "s \<in> cball 0 t" and x1: "x1 \<in> cball x u"
    from *(2)[OF x1 s] have "flow x1 s \<in> cball x1 u" .
    also have "\<dots> \<subseteq> cball x (2 * u)"
      using x1 by (auto intro!: dist_triangle_le[OF add_mono, of _ x1 u _ u, simplified] simp: dist_commute)
    finally have "flow x1 s \<in> cball x (2 * u)" .
  } note flow_in_cball = this
(*
  from compact_imp_bounded[OF compact_continuous_image[OF cont_on_f_flow, OF order_refl _ compact_cball]]
  obtain B where B: "\<And>s x1. s \<in> cball 0 t \<Longrightarrow> x1 \<in> cball x u \<Longrightarrow> norm (f (flow x1 s)) \<le> B" "B \<ge> 0"
    by (auto simp: bounded_iff cball_def)
*)
  have "lipschitz (cball 0 t\<times>cball x u) (\<lambda>(t, x). flow x t) (B + exp ((L + 1) * \<bar>t\<bar>))"
  proof (rule lipschitzI, safe)
    fix t1 t2 :: real and x1 x2
    assume t1: "t1 \<in> cball 0 t" and t2: "t2 \<in> cball 0 t"
      and x1: "x1 \<in> cball x u" and x2: "x2 \<in> cball x u"
    have t1_ex: "t1 \<in> existence_ivl x1" and "t2 \<in> existence_ivl x1" "t2 \<in> existence_ivl x2" "x1 \<in> cball x (2*u)" "x2 \<in> cball x (2*u)"
      using *(1)[OF x1] *(1)[OF x2] t1 t2 x1 x2 tu by auto
    have "dist (flow x1 t1) (flow x2 t2) \<le>
      dist (flow x1 t1) (flow x1 t2) + dist (flow x1 t2) (flow x2 t2)"
      by (rule dist_triangle)
    also have "dist (flow x1 t2) (flow x2 t2) \<le> dist x1 x2 * exp ((L + 1) * \<bar>t2\<bar>)"
      unfolding dist_norm
    proof (rule exponential_initial_condition[of t2 x1 "cball x (2*u)" x2])
      fix s assume "s \<in> closed_segment 0 t2" hence s: "s \<in> cball 0 t"
        using t2 by (auto simp: dist_real_def closed_segment_real split: split_if_asm)
      show "flow x1 s \<in> cball x (2 * u)"
        by (rule flow_in_cball[OF s x1])
      show "flow x2 s \<in> cball x (2 * u)"
        by (rule flow_in_cball[OF s x2])
    qed fact+
    also have "\<dots> \<le> dist x1 x2 * exp ((L + 1) * \<bar>t\<bar>)"
      using `u > 0` t2
      by (auto intro!: mult_left_mono add_nonneg_nonneg lipschitz[THEN lipschitz_nonneg]
        simp: cball_eq_empty cball_eq_sing' dist_real_def)
    also
    have "dist (flow x1 t1) (flow x1 t2) \<le> dist t1 t2 * B"
      apply (subst flow_fixed_point'')
      defer defer
      apply (subst (2)flow_fixed_point'')
      apply (auto simp: closed_segment_real dist_norm)
      apply fact
      using x1 subs[of x] `u > 0` apply force
      apply (subst integral_minus_sets) apply assumption apply assumption
      defer
      apply simp
      defer
      apply (subst integral_combine2) apply simp apply simp defer
      defer
      apply (subst norm_minus_cancel[symmetric])
      apply simp
      apply (subst integral_combine2) apply simp apply simp defer
      defer
      apply (subst integral_minus_sets')
      using t1 t2 t1_ex x1 flow_in_cball[OF _ x1]
      apply (auto intro!: order_trans[OF integral_bound[where B=B]] cont_on_f_flow B
        integrable_continuous_real
        simp: dist_real_def integral_minus_sets')
      done
    finally have "dist (flow x1 t1) (flow x2 t2) \<le> dist t1 t2 * B + dist x1 x2 * exp ((L + 1) * \<bar>t\<bar>)" by arith
    also have "\<dots> \<le> dist (t1, x1) (t2, x2) * B + dist (t1, x1) (t2, x2) * exp ((L + 1) * \<bar>t\<bar>)"
      using `B > 0`
      by (auto intro!: add_mono mult_right_mono simp: dist_prod_def)
    finally show "dist (flow x1 t1) (flow x2 t2)
       \<le> (B + exp ((L + 1) * \<bar>t\<bar>)) * dist (t1, x1) (t2, x2)" by (simp add: algebra_simps)
  qed (simp add: `0 < B` less_imp_le)
  ultimately
  show thesis using subs tu ..
qed

lemma compact_implies_lipschitz:
  assumes "compact A" "A \<subseteq> X"
  obtains L where "lipschitz A f L"
proof -
  from compact_continuous_image[OF f_continuous_on[THEN continuous_on_subset[OF _ `A \<subseteq> _`]] `compact A`]
  have "compact (f ` A)" .
  then obtain M where M: "\<And>a. a \<in> A \<Longrightarrow> norm (f a) \<le> M" "M > 0"
    by (force simp: bounded_pos Ball_def dest!: compact_imp_bounded)
  {
    assume *: "\<And>n::nat. \<not>lipschitz A f n"
    {
      fix n::nat
      from *[of n] obtain x y where "x \<in> A" "y \<in> A" "norm (f y - f x) > n * norm (y - x)"
        by (auto simp: lipschitz_def dist_norm)
      hence "\<exists>x y. x \<in> A \<and> y \<in> A \<and> norm (f y - f x) > n * norm (y - x)"
        by (auto simp: lipschitz_def dist_norm)
    } then obtain x y::"nat \<Rightarrow> 'a" where xy: "\<And>n. x n \<in> A" "\<And>n. y n \<in> A"
      "\<And>n. norm (f (y n) - f (x n)) > n * norm (y n - x n)"
      by metis
    with assms obtain lx rx where lx': "lx \<in> A" "subseq rx" "(x o rx) ----> lx"
      by (metis compact_def)
    with xy have "\<And>n. (y o rx) n \<in> A" by auto
    with assms obtain ly ry where ly': "ly \<in> A" "subseq ry" "((y o rx) o ry) ----> ly"
      by (metis compact_def)
    with lx' have lx: "(x o (rx o ry)) ----> lx" (is "?x ----> _") and ly: "(y o (rx o ry)) ----> ly" (is "?y ----> _")
      by (metis LIMSEQ_subseq_LIMSEQ fun.map_comp)+
    hence "(\<lambda>n. ?y n - ?x n) ----> ly - lx"
      by (metis tendsto_diff)
    moreover
    have "eventually (\<lambda>n::nat. n > 0) sequentially"
      by (metis eventually_at_top_dense)
    hence "eventually (\<lambda>n. norm (?y n - ?x n) \<le> norm (2 * M / n) * 1) sequentially"
    proof eventually_elim
      case (elim n)
      hence "rx (ry n) > 0"
        by (metis less_nat_zero_code lx'(2) ly'(2) neq0_conv subseq_mono)
      hence "norm (?y n - ?x n) < norm (f (?y n) - f (?x n)) / rx (ry n)"
        using xy(3)[of "rx (ry n)"]
        by (auto simp: field_simps)
      also have "\<dots> \<le> 2 * M / n"
        apply (rule frac_le)
        apply simp
        apply (rule norm_triangle_le_sub)
        apply (simp add: )
        unfolding mult_2
        apply (rule add_mono)
        apply (rule M)
        apply (rule xy)
        apply (rule M)
        apply (rule xy)
        using elim apply simp
        apply simp
        by (metis le_trans lx'(2) ly'(2) seq_suble)
      finally show ?case using M by simp
    qed
    with _ have "(\<lambda>n. ?y n - ?x n) ----> 0"
      apply (rule tendsto_0_le)
      apply (rule tendsto_divide_0)
      apply (rule tendsto_const)
      by (metis filterlim_at_top_imp_at_infinity filterlim_real_sequentially)
    ultimately have "lx = ly"
      by (metis (poly_guards_query) eq_iff_diff_eq_0 limI)
    with assms lx' have "lx \<in> X" by auto
    with lipschitz obtain u L where L: "u > 0" "lipschitz (cball lx u \<inter> X) f L"
      by (auto dest!: spec[where x=0] intro!: exI[where x=0])
    hence "L \<ge> 0" by (auto intro!: lipschitz_nonneg)
    from L ly lx `lx = ly`
    have "eventually (\<lambda>n. ?y n \<in> ball lx u) sequentially"
      "eventually (\<lambda>n. ?x n \<in> ball lx u) sequentially"
      by (auto simp: dist_commute Lim)
    moreover have "eventually (\<lambda>n. n > L) sequentially"
      by (metis `0 \<le> L` eventually_at_top_dense natfloor_less_iff)
    ultimately
    have "eventually (\<lambda>_. False) sequentially"
    proof eventually_elim
      case (elim n)
      hence "norm  (f (?y n) - f (?x n)) \<le> L * norm (?y n - ?x n)"
        using assms xy
        unfolding dist_norm[symmetric]
        by (intro lipschitzD[OF L(2)]) auto
      also have "\<dots> \<le> n * norm (?y n - ?x n)"
        using elim by (intro mult_right_mono) auto
      also have "\<dots> \<le> rx (ry n) * norm (?y n - ?x n)"
        apply (intro mult_right_mono)
        apply (metis lx'(2) ly'(2) order.trans real_of_nat_le_iff seq_suble)
        apply simp
        done
      also have "\<dots> < norm  (f (?y n) - f (?x n))"
        by (auto intro!: xy(3))
      finally show ?case by simp
    qed
    hence False
      by simp
  } then obtain L where "lipschitz A f L" by auto
  thus ?thesis ..
qed

lemma
  flow_leaves_compact_ivl:
  assumes "x0 \<in> X"
  assumes "sup_existence x0 < \<infinity>"
  assumes "compact K"
  assumes "K \<subseteq> X"
  obtains t where "t \<ge> 0" "t \<in> existence_ivl x0" "flow x0 t \<notin> K"
proof (atomize_elim, rule ccontr, auto)
  assume "\<forall>t. t \<in> c1_on_open.existence_ivl f X x0 \<longrightarrow> 0 \<le> t \<longrightarrow> flow x0 t \<in> K"
  note flow_in_K = this[rule_format]
  from existence_ivl_zero[OF `x0 \<in> X`] have ninfty: "inf_existence x0 \<noteq> \<infinity>" "sup_existence x0 \<noteq> -\<infinity>"
    by (auto simp: existence_ivl_def[OF `x0 \<in> X`])
  with assms obtain b where b: "sup_existence x0 = ereal b"
    by (cases "sup_existence x0") auto
  hence b_gt: "b > inf_existence x0" "b > 0" using existence_ivl_zero[OF `x0 \<in> X`]
    apply (auto simp add: existence_ivl_def assms)
    by (metis ereal_infinity_cases ereal_less_eq(1) less_ereal.simps(3) not_le real_less_ereal_iff)

  have in_existence_ivlI: "\<And>t. 0 \<le> t \<Longrightarrow> t < b \<Longrightarrow> t \<in> existence_ivl x0"
    using b apply (auto simp: existence_ivl_def assms)
    using ninfty existence_ivl_zero[OF `x0 \<in> X`]
    apply (auto simp: existence_ivl_def assms real_image_ereal_ivl b
      split: split_if_asm)
    done

  have "compact (f ` K)"
    by (intro compact_continuous_image continuous_on_subset[OF f_continuous_on] assms)
  hence "bounded (f ` K)" by (simp add: compact_eq_bounded_closed)
  then obtain M where M: "\<And>x. x \<in> K \<Longrightarrow> norm (f x) \<le> M" "M > 0"
    by (auto simp: bounded_pos)
  {
    fix t1 t2 assume "0 \<le> t1" "t1 < t2" and t1: "t1 \<in> existence_ivl x0" and t2: "t2 \<in> existence_ivl x0"
    let ?I = "\<lambda>ivl. (\<lambda>t. f (flow x0 t)) integrable_on ivl"
    have I[simp]: "?I {0 .. t1}" "?I {0 .. t2}" "?I {t1 .. t2}" "?I {t1 .. 0}"
      using closed_segment_subset_existence_ivl[OF `x0 \<in> X` t1]
         closed_segment_subset_existence_ivl[OF `x0 \<in> X` t2] `t1 < t2`
      by (force intro!: integrable_continuous_real continuous_at_imp_continuous_on
        f_flow_continuous `x0 \<in> X` simp: closed_segment_real split: split_if_asm)+
    hence "flow x0 t2 - flow x0 t1 = integral {t1..t2} (\<lambda>t. f (flow x0 t))"
      --"TODO: extract as lemma and use elsewhere as well"
      unfolding flow_fixed_point''[OF `t1 \<in> existence_ivl x0` `x0 \<in> X`]
        flow_fixed_point''[OF `t2 \<in> existence_ivl x0` `x0 \<in> X`]
      using `t1 < t2`
      by (auto simp: closed_segment_real algebra_simps integral_combine integral_combine2 I)
    also have "norm \<dots> \<le> M * (t2 - t1)"
      apply (rule integral_bound)
      using closed_segment_subset_existence_ivl[OF `x0 \<in> X` t1]
         closed_segment_subset_existence_ivl[OF `x0 \<in> X` t2] `0 \<le> t1` `t1 < t2`
      apply (auto intro!: flow_in_K M continuous_at_imp_continuous_on
        f_flow_continuous `x0 \<in> X`
        simp: closed_segment_real split: split_if_asm)
      done
    finally have "dist (flow x0 t2) (flow x0 t1) \<le> M * (t2 - t1)" by (simp add: dist_norm)
  } -- "TODO: do I need really need Cauchy in the following?!"
  hence dist_flow_le: "\<And>t1 t2. 0 \<le> t1 \<Longrightarrow> 0 \<le> t2 \<Longrightarrow> t1 \<in> existence_ivl x0 \<Longrightarrow> t2 \<in> existence_ivl x0 \<Longrightarrow>
      dist (flow x0 t1) (flow x0 t2) \<le> M * abs (t2 - t1)"
    apply (auto simp: abs_real_def dist_commute not_less)
    apply (metis dist_commute)
    by (metis (erased, hide_lams) diff_self dist_le_zero_iff less_eq_real_def mult.commute mult_zero_left)

  have ev1: "eventually (\<lambda>n. b -  1 / n > inf_existence x0) sequentially"
    using _ b_gt(1)
    apply (rule order_tendstoD)
    apply simp
    apply (rule tendsto_eq_intros)
    apply (rule tendsto_intros)
    unfolding inverse_eq_divide[symmetric]
    apply (rule seq_harmonic)
    apply auto
    done
  have ev2: "eventually (\<lambda>n. n > 0) sequentially"
    by (metis eventually_at_top_dense)
  have ev3: "eventually (\<lambda>n. 1 / n < b) sequentially"
    apply (rule order_tendstoD)
    unfolding inverse_eq_divide[symmetric]
    apply (rule seq_harmonic)
    apply fact
    done
  from eventually_conj[OF ev1 eventually_conj[OF ev2 ev3], THEN eventually_happens]
  obtain N::nat where N: "N > 0" "inf_existence x0 < (b - 1 / N)" "1 / N < b"
    by auto
  let ?f = "\<lambda>n::nat. flow x0 (b - 1/n)"
  let ?fN = "?f o (op + N)"
  have "Cauchy ?f"
  proof (rule metric_CauchyI)
    case goal1
    have "(\<lambda>n. M * inverse n) ----> 0"
      apply (rule tendsto_eq_intros)
      apply (rule tendsto_intros)
      unfolding inverse_eq_divide[symmetric]
      apply (rule seq_harmonic)
      apply auto
      done
    hence "(\<lambda>n. M / n) ----> 0"
      by (simp add: inverse_eq_divide)
    hence "eventually (\<lambda>n. M / n < e/2) sequentially"
      by (metis (poly_guards_query) goal1 half_gt_zero_iff order_tendsto_iff)
    from eventually_conj[OF this eventually_conj[OF ev1 eventually_conj[OF ev2 ev3]], THEN eventually_happens]
    obtain N::nat where N: "N > 0" "M / real N < e / 2" "inf_existence x0 < (b - 1 / N)" "1 / N < b"
      by auto
    {
      fix n m assume "n \<ge> N" "m \<ge> N"
      with N have nm: "n > 0" "m > 0" "b - 1 / N \<le> b - 1 / n" "b - 1 / N \<le> b - 1 / m" " 1/ n \<le> 1 / N"
        by (auto intro!: divide_left_mono)
      from le_less_trans[OF `1 / n \<le> 1/N` `1/N < b`] have "1/n < b" .
      with nm have "dist (flow x0 (b - 1 / n)) (flow x0 (b - 1 / m)) \<le> M * abs (b - 1 / m - (b - 1 / n))"
        apply (intro dist_flow_le)
        using b N ninfty
        apply (auto simp: existence_ivl_def[OF `x0 \<in> X`] real_image_ereal_ivl)
        apply (cases "inf_existence x0")
        apply (auto simp: existence_ivl_def[OF `x0 \<in> X`] real_image_ereal_ivl)[4]
        apply (cases "inf_existence x0")
        apply (auto simp: existence_ivl_def[OF `x0 \<in> X`] real_image_ereal_ivl)
        apply (metis add.commute diff_less_iff(4) diff_self inverse_eq_divide inverse_positive_iff_positive less_le_trans max.semilattice_strict_iff_order not_less real_of_nat_gt_zero_cancel_iff)
        apply (cases "inf_existence x0")
        apply (auto simp: existence_ivl_def[OF `x0 \<in> X`] real_image_ereal_ivl)
        apply (cases "inf_existence x0")
        apply (auto simp: existence_ivl_def[OF `x0 \<in> X`] real_image_ereal_ivl)
        apply (metis add.commute diff_less_iff(4) diff_self inverse_eq_divide inverse_positive_iff_positive less_le_trans max.semilattice_strict_iff_order not_less real_of_nat_gt_zero_cancel_iff)
        done
      also have "\<dots> \<le> M * (1 / m + 1 / n)"
        using `M > 0` by (auto intro!: mult_left_mono order_trans[OF abs_triangle_ineq4])
      also have "\<dots> \<le> M / m + M / n" by (simp add: algebra_simps)
      also have "\<dots> \<le> M / N + M / N" using nm `n \<ge> N` `m \<ge> N` `M>0` `0 < N`
        by (intro add_mono) (auto intro!: divide_left_mono mult_pos_pos)
      also have "\<dots> < e / 2 + e / 2" using N by (intro add_strict_mono) simp
      also have "\<dots> = e" by simp
      finally have "dist (flow x0 (b - 1 / n)) (flow x0 (b - 1 / m)) < e" .
    }
    thus ?case by blast
  qed
  hence "Cauchy (?fN)"
    apply (rule Cauchy_subseq_Cauchy)
    by (metis nat_add_left_cancel_less subseq_def)
  moreover
  have "(\<forall>n. (?fN) n \<in> K)"
    using ninfty b_gt `0 < N` N
    apply (auto intro!: add_pos_nonneg flow_in_K simp: existence_ivl_def `x0 \<in> X` real_image_ereal_ivl b)
  proof -
    case goal1
    have "inf_existence x0 < (b - 1 / N)" by fact
    also have "\<dots> \<le> (b - 1 / (N + n))"
      using `0 < N`
      by (auto intro!: divide_left_mono mult_pos_pos add_pos_nonneg)
    finally show ?case
      apply auto
      by (metis ereal_infinity_cases goal1(1,7) ninfty(1) real_less_ereal_iff)
  next
    case goal2
    have "1 / (real N + real n) \<le> 1 / N"
      by (auto intro!: divide_left_mono mult_pos_pos add_pos_nonneg `0 < N`)
    also note `\<dots> < b`
    finally show ?case by simp
  qed
  ultimately
  have "\<exists>l\<in>K. (?fN) ----> l"
    using `compact K`
    by (auto simp: compact_eq_bounded_closed complete_eq_closed[symmetric] complete_def)
  then obtain x1 where x1: "x1 \<in> K" "(?fN) ----> x1" by metis
  hence "x1 \<in> X" using assms by auto

  have flow_at_b: "(flow x0 ---> x1) (at b within {0 .. b})"
  proof (rule tendstoI)
    fix e::real assume "0 < e" hence "0 < e / 2" by auto
    from x1(2)[THEN tendstoD, OF this] have ev3: "eventually (\<lambda>n. dist ((?fN) n) x1 < e/2) sequentially" .
    have "eventually (\<lambda>n. 1 / n < e / (2 * M)) sequentially"
      apply (rule order_tendstoD[where y =0])
      unfolding inverse_eq_divide[symmetric]
      apply (rule seq_harmonic)
      apply (auto intro!: divide_pos_pos `0 < e` `0 < M`)
      done
    hence ev4: "eventually (\<lambda>n. 1 / (N + n) < e / (2 * M)) sequentially"
      using ev2
    proof eventually_elim
      case elim
      hence "1 / real (N + n) < 1 / n" by (auto intro!: divide_strict_left_mono `0 < N`)
      also have "\<dots> < e / (2 * M)"  by fact
      finally show ?case .
    qed
    from eventually_conj[OF ev3 eventually_conj [OF ev4 ev2]]
    obtain N' where N': "dist (?fN N') x1 < e / 2" "N' > 0" "1 / (N + N') < e / (2 * M)"
      by (auto dest!: eventually_happens)

    have "eventually (\<lambda>x. x < b) (at b within {0 .. b})"
      by (auto simp: eventually_at_filter)
    moreover
    have "eventually (\<lambda>x. x > b - 1 / (real N' + real N)) (at b within {0 .. b})"
      apply (rule order_tendstoD)
      apply (rule tendsto_intros)
      using N'
      apply simp
      done
    moreover
    have "eventually (\<lambda>x. x < b - (1 / real (N + N') - e / 2 / M)) (at b within {0 .. b})"
      apply (rule order_tendstoD)
      apply (rule tendsto_intros)
      using N'
      apply simp
      done
    hence "eventually (\<lambda>x. x - (b - 1 / real (N + N')) < e / 2 / M) (at b within {0 .. b})"
      by (simp add: algebra_simps)
    moreover
    have "eventually (\<lambda>x. x > 0) (at b within {0 .. b})" "eventually (\<lambda>x. x < b) (at b within {0 .. b})"
      using b_gt apply -
      apply (rule order_tendstoD)
      apply (rule tendsto_intros) apply simp
      apply (auto simp: eventually_at_filter)
      done
    moreover
    hence "eventually (\<lambda>x. x \<in> existence_ivl x0) (at b within {0 .. b})"
      by eventually_elim (auto simp: in_existence_ivlI)
    ultimately have "eventually (\<lambda>x. dist (flow x0 x) (?fN N') < e / 2) (at b within {0 .. b})"
    proof eventually_elim
      case elim
      thus ?case
        unfolding o_def
        apply -
        apply (rule le_less_trans)
        apply (rule dist_flow_le)
        apply simp
      proof -
        case goal1
        have "1 / real (N + N') \<le> 1 / N"
          by (auto intro!: divide_left_mono mult_pos_pos add_pos_nonneg `0 < N`)
        also have "\<dots> < b" by fact
        finally show ?case by simp
      next
        case goal3
        have "inf_existence x0 < ereal (b - 1 / N)"
          by fact
        also have "\<dots> \<le> b - 1 / (N + N')"
          using `N > 0` `N' > 0`
          by (auto intro!: divide_left_mono mult_pos_pos add_pos_nonneg)
        finally show ?case
          using ninfty N goal3 b_gt
          apply (auto simp: existence_ivl_def `x0 \<in> X` real_image_ereal_ivl b)[1]
          apply (metis ereal_infinity_cases real_less_ereal_iff)
          done
      next
        case goal4
        hence "\<bar>b - 1 / real (N + N') - x\<bar> = x - (b - 1 / real (N + N'))"
          using `N > 0` `N' > 0`
          by (auto simp: abs_real_def algebra_simps)
        also have "M * \<dots> < M * (e / 2 / M)"
          by (rule mult_strict_left_mono) fact+
        also have "\<dots> = e / 2"
          using `0 < M` by simp
        finally show ?case .
      qed
    qed
    thus "eventually (\<lambda>x. dist (flow x0 x) x1 < e) (at b within {0 .. b})"
    proof eventually_elim
      case elim
      have "dist (flow x0 x) x1 \<le> dist (flow x0 x) (?fN N') + dist (?fN N') x1"
        by (rule dist_triangle)
      also note elim
      also note N'(1)
      finally show ?case by simp
    qed
  qed

  def u \<equiv> "\<lambda>t. if t < b then flow x0 t else x1"
  {
    fix s assume s: "0 < s" "s < b"
    hence "s \<in> interior {0 .. b}"
      by (simp add: interior_atLeastAtMost)
    hence "at s within {0 .. b} = at s"
      by (subst at_within_interior) auto
    also
    have "at s = at s within {0 <..< b}"
      using s by (subst (2) at_within_open) auto
    also have "((\<lambda>t. u t) ---> u s) \<dots>"
      using s
      apply (auto simp: u_def)
      apply (subst filterlim_cong)
      apply (rule refl)
      apply (rule refl)
      defer
      apply (rule flow_tendsto[where t="\<lambda>x. x"])
      apply (simp add: `x0 \<in> X`)
      apply (simp add: in_existence_ivlI)
      apply (rule tendsto_intros)
      apply (auto simp: eventually_at_filter `x0 \<in> X` intro!: in_existence_ivlI)
      done
    finally have "(u ---> u s) (at s within {0..b})" .
  } note u_below_b = this
  have "((\<lambda>t. u t) ---> u b) (at b within {0 .. b})"
    unfolding u_def
    apply (auto )
    apply (subst filterlim_cong)
    apply (rule refl)
    apply (rule refl)
    defer
    apply (rule flow_at_b)
    apply (auto simp: eventually_at_filter)
    done
  hence u_at_b: "((\<lambda>t. u t) ---> u b) (at b within {0 .. b})"
    by (rule tendsto_within_subset) auto
  have ev_less: "eventually (\<lambda>x. x < b) (at 0 within {0 .. b})"
      apply (rule order_tendstoD)
      apply (rule tendsto_intros)
      using `0 < b`
      apply simp
      done
  have u_at_0: "((\<lambda>t. u t) ---> u 0) (at 0 within {0 .. b})"
    using `0 < b`
    apply (auto simp: u_def)
    apply (subst filterlim_cong)
    apply (rule refl)
    apply (rule refl)
    defer
    apply (rule flow_tendsto[where t="\<lambda>x. x"])
    apply (simp add: `x0 \<in> X`)
    apply (simp add: in_existence_ivlI)
    apply (rule tendsto_intros)
    using ev_less
    unfolding eventually_at_filter
    apply eventually_elim
    apply auto
    done

  with u_at_b u_below_b have "\<And>s. 0 \<le> s \<Longrightarrow> s \<le> b \<Longrightarrow> (u ---> u s) (at s within {0 .. b})"
    apply (case_tac "s = b", simp)
    apply (case_tac "s = 0", simp)
    apply simp
    done
  hence u_cont: "continuous_on {0 .. b} u"
    by (auto simp: continuous_on)
  moreover
  {
    fix t assume t: "0 \<le> t" "t < b"
    hence "u t = x0 + integral {0 .. t} (\<lambda>s. f (u s))"
      by (subst integral_spike[where s="{b}" and g = "\<lambda>s. f (flow x0 s)"])
        (auto simp: u_def flow_fixed_point `x0 \<in> X` not_less in_existence_ivlI)
  } note u_fixed_point = this
  have fixed_point_tendsto: "((\<lambda>t. x0 + integral {0 .. t} (\<lambda>s. f (u s))) --->
    x0 + integral {0 .. b} (\<lambda>s. f (u s))) (at b within {0 .. b})"
    apply (rule tendsto_intros)
    apply (rule tendsto_intros)
    apply (rule indefinite_integral_continuous[unfolded continuous_on, rule_format])
    using `0 < b`
    apply (auto intro!: integrable_continuous_real f_continuous)
    using _ u_cont refl
    apply (rule continuous_on_compose2)
    apply (rule continuous_on_subset)
    apply (rule f_continuous_on)
    apply (auto simp: u_def intro!: flow_in_domain `x0 \<in> X` `x1 \<in> X` in_existence_ivlI)
    done
  have u_tendsto: "(u ---> x0 + integral {0 .. b} (\<lambda>s. f (u s))) (at b within {0 .. b})"
    apply (subst filterlim_cong)
    apply (rule refl)
    apply (rule refl)
    defer
    apply (rule fixed_point_tendsto)
    apply (auto simp: eventually_at_filter u_fixed_point)
    done
  with _ u_at_b have "u b = x0 + integral {0..b} (\<lambda>s. f (u s))"
    apply (rule tendsto_unique)
    apply (auto simp: trivial_limit_within open_dist intro!: islimptI)
  proof -
    case goal1
    then obtain e where e: "e > 0" "\<And>y. dist y b < e \<Longrightarrow> y \<in> T" by auto
    show ?case
      apply (intro bexI[where x="max (b - e/2) (b/2)"])
      apply safe
      apply (rule e)
      using e(1) `0 < b`
      apply (auto simp add: dist_real_def abs_real_def min_def not_le)
      done
  qed
  with u_fixed_point have "\<And>s. 0 \<le> s \<Longrightarrow> s \<le> b \<Longrightarrow> u s = x0 + integral {0..s} (\<lambda>s. f (u s))"
    by (case_tac "s = b") auto
  moreover have "continuous_on {0..b} (f \<circ> u)"
    apply (rule continuous_on_compose)
    using u_cont
    apply (auto intro!: continuous_at_imp_continuous_on
      continuous_within_subset[OF f_continuous]
      simp: o_def continuous_on_eq_continuous_within)
    apply (auto simp: u_def `x1 : X` intro!: flow_in_domain `x0 \<in> X` in_existence_ivlI)
    done
  ultimately
  have u_vderiv: "\<And>s. 0 \<le> s \<Longrightarrow> s \<le> b \<Longrightarrow> (u has_vector_derivative f (u s)) (at s within {0 .. b})"
    apply (auto intro!: derivative_intros simp: o_def)
    apply (rule has_vector_derivative_imp[where f="\<lambda>s. x0 + integral {0..s} (\<lambda>s. f (u s))" and s="{0..b}"])
    defer defer defer
    apply (rule refl)
    apply (rule refl)
    apply (rule derivative_eq_intros)
    apply (rule derivative_eq_intros)
    apply (rule refl)
    apply (rule integral_has_vector_derivative[of 0 b "f o u", simplified o_def])
    apply force
    apply force
    apply force
    apply force
    apply force
    apply force
    done

  interpret i: ivp "\<lparr>ivp_f = \<lambda>(t, x). f x, ivp_t0 = 0, ivp_x0 = x0, ivp_T = {0..b}, ivp_X = X\<rparr>"
    by unfold_locales (auto simp: `0 < b` less_imp_le `x0 \<in> X`)
  have "i.is_solution u"
  proof (default, auto)
    show "u 0 = x0" by (auto simp: u_def `0 < b` `x0 \<in> X`)
    fix t assume t: "0 \<le> t" "t \<le> b"
    thus "(u has_vector_derivative f (u t)) (at t within {0..b})"
      by (rule u_vderiv)
    from t show "u t \<in> X"
      by (auto simp: u_def `x0 \<in> X` `x1 \<in> X` intro!: flow_in_domain in_existence_ivlI)
  qed
  with `x0 \<in> X` have "{0 .. b} \<subseteq> existence_ivl x0"
    using `0 < b` by (auto simp: is_interval_closed_interval maximal_existence_flow)
  hence "b \<in> existence_ivl x0" using `0 < b`
    by auto
  thus False
    using b_gt(2) real_less_ereal_iff
    by (auto simp: existence_ivl_def `x0 \<in> X` b) auto
qed

lemma
  global_right_existence_interval:
  assumes "b \<ge> 0"
  assumes b: "b \<in> existence_ivl x0"
  assumes x0: "x0 \<in> X"
  obtains d K where "d > 0" "K > 0"
    "ball x0 d \<subseteq> X"
    "\<And>y. y \<in> ball x0 d \<Longrightarrow> b \<in> existence_ivl y"
    "\<And>t y. y \<in> ball x0 d \<Longrightarrow> t \<in> {0 .. b} \<Longrightarrow> dist (flow x0 t) (flow y t) \<le> dist x0 y * exp (K * abs t)"
    "\<And>e. e > 0 \<Longrightarrow> eventually (\<lambda>y. \<forall>t \<in> {0 .. b}. dist (flow x0 t) (flow y t) < e) (at x0)"
proof -
  def seg \<equiv> "(\<lambda>t. flow x0 t) ` (closed_segment 0 b)"
  have [simp]: "x0 \<in> seg"
    by (auto simp: seg_def intro!: image_eqI[where x=0] simp: closed_segment_real x0)
  have "seg \<noteq> {}" by (auto simp: seg_def closed_segment_real)
  moreover
  have "compact seg"
    using x0 b
    apply (auto simp: seg_def closed_segment_real
      intro!: compact_continuous_image continuous_at_imp_continuous_on flow_continuous)
    apply (metis (erased, hide_lams) atLeastAtMost_iff closed_segment_real closed_segment_subset_existence_ivl contra_subsetD order.trans)
    apply (metis (erased, hide_lams) atLeastAtMost_iff closed_segment_real closed_segment_subset_existence_ivl contra_subsetD)
    done
  moreover note open_domain
  moreover have "seg \<subseteq> X"
    using closed_segment_subset_existence_ivl[OF x0 b]
    by (auto simp: seg_def intro!: flow_in_domain x0)
  ultimately
  obtain e where e: "0 < e" "{x. infdist x seg \<le> e} \<subseteq> X"
    by (rule compact_in_open_separated)
  def A \<equiv> "{x. infdist x seg \<le> e}"
  have "compact A"
    unfolding A_def
    by (rule compact_infdist_le) fact+
  moreover
  have "A \<subseteq> X" using e by (simp add: A_def)
  ultimately obtain K' where "lipschitz A f K'"
    by (rule compact_implies_lipschitz)
  hence K': "lipschitz A f (abs K')"
    by (rule nonneg_lipschitz)
  def K \<equiv> "abs K' + 1"
  have "0 < K" "0 \<le> K"
    by (auto simp: K_def)
  have K: "lipschitz A f K"
    unfolding K_def
    using `lipschitz A f K'`
    by (rule pos_lipschitz)

  have [simp]: "x0 \<in> A" using `0 < e` by (auto simp: A_def)


  def d \<equiv> "min e (e * exp (-K * b))"
  hence d: "0 < d" "d \<le> e" "d \<le> e * exp (-K * b)"
    using e by auto

  {
    fix t assume "0 \<le> t" "t \<le> b"
    hence "d * exp (K * t) \<le> d * exp (K * b)"
      using `0 \<le> K` `0 < d`
      by (auto intro!: mult_left_mono)
    also have "d * exp (K * b) \<le> e"
      using d by (auto simp: exp_minus field_simps)
    finally have "d * exp (K * t) \<le> e" .
  } note d_times_exp_le = this
  have "ball x0 d \<subseteq> X" using d `A \<subseteq> X`
    by (auto simp: A_def dist_commute intro!: infdist_le2[where a=x0])
  {
    fix y
    assume y: "y \<in> ball x0 d"
    hence "y \<in> A" using d
      by (auto simp: A_def dist_commute intro!: infdist_le2[where a=x0])
    hence "y \<in> X" using `A \<subseteq> X` by auto
    {
      fix t::real assume t: "0 \<le> t" "t \<in> existence_ivl y" "t \<le> b"
      have "flow y t \<in> A"
      proof (rule ccontr)
        assume flow_out: "flow y t \<notin> A"
        obtain t' where t':
          "0 \<le> t'"
          "t' \<le> t"
          "\<And>t. t \<in> {0 .. t'} \<Longrightarrow> flow x0 t \<in> A"
          "infdist (flow y t') seg \<ge> e"
          "\<And>t. t \<in> {0 .. t'} \<Longrightarrow> flow y t \<in> A"
        proof -
          let ?out = "((\<lambda>t. infdist (flow y t) seg) -` {e..}) \<inter> {0..t}"
          have "compact ?out"
            unfolding compact_eq_bounded_closed
          proof safe
            show "bounded ?out" by (auto intro!: bounded_closed_interval)
            have "continuous_on {0 .. t} ((\<lambda>t. infdist (flow y t) seg))"
              apply (auto intro!: continuous_at_imp_continuous_on
                continuous_intros flow_continuous `y \<in> X`)
              by (metis `y \<in> X` atLeastAtMost_iff ivl_subset_existence_ivl subset_eq t(2))
            thus "closed ?out"
              by (simp add: continuous_on_closed_vimage)
          qed
          moreover
          have "t \<in> (\<lambda>t. infdist (flow y t) seg) -` {e..} \<inter> {0..t}"
            using flow_out `0 \<le> t`
            by (auto simp: A_def)
          hence "?out \<noteq> {}"
            by blast
          ultimately have "\<exists>s\<in>?out. \<forall>t\<in>?out. s \<le> t"
            by (rule compact_attains_inf)
          then obtain t' where t':
            "\<And>s. e \<le> infdist (flow y s) seg \<Longrightarrow> 0 \<le> s \<Longrightarrow> s \<le> t \<Longrightarrow> t' \<le> s"
            "e \<le> infdist (flow y t') seg"
            "0 \<le> t'" "t' \<le> t"
            by (auto simp: vimage_def Ball_def) metis
          {
            fix s assume s: "s \<in> {0 .. t'}"
            hence "s \<in> closed_segment 0 b"
              using `t \<le> b` t' by (auto simp: closed_segment_real)
            hence "flow x0 s \<in> A"
              using s `e > 0` by (auto simp: seg_def A_def)
          } note flow_in = this
          {
            assume "t' = 0"
            hence "flow y t' \<in> A"
              apply (auto simp:  A_def `y \<in> X`)
              apply (rule infdist_le2[where a=x0])
              using y d by (auto simp: dist_commute)
          } moreover {
            fix s assume s: "s \<in> {0 ..< t'}"
            hence "s \<in> closed_segment 0 b"
              using `t \<le> b` t' by (auto simp: closed_segment_real)
            from t'(1)[of s]
            have "t' > s \<Longrightarrow> 0 \<le> s \<Longrightarrow> s \<le> t \<Longrightarrow> e > infdist (flow y s) seg"
              by force
            hence "flow y s \<in> A"
              using s t' `e > 0` by (auto simp: seg_def A_def)
          } moreover
          note left_of_in = this
          have "closed A" using `compact A` by (auto simp: compact_eq_bounded_closed)
          have "((\<lambda>s. flow y s) ---> flow y t') (at_left t')"
            apply (rule flow_tendsto)
            using ivl_subset_existence_ivl[OF `y \<in> X` t(2)] t' `y \<in> X`
            by (auto intro!: tendsto_intros)
          with `closed A` _ _ have "t' \<noteq> 0 \<Longrightarrow> flow y t' \<in> A"
            apply (rule Lim_in_closed_set)
            apply auto
          proof -
            case goal1
            hence "t' > 0" using t' by auto
            hence "eventually (\<lambda>x. x \<ge> 0) (at_left t')"
              by (metis eventually_at_left less_imp_le)
            thus "eventually (\<lambda>x. flow y x \<in> A) (at_left t')"
              unfolding eventually_at_filter
              by eventually_elim (auto intro!: left_of_in)
          qed
          ultimately have flow_y_in: "\<And>s. s \<in> {0 .. t'} \<Longrightarrow> flow y s \<in> A"
            by (case_tac "s = t'") auto
          have              "0 \<le> t'"
          "t' \<le> t"
          "\<And>t. t \<in> {0 .. t'} \<Longrightarrow> flow x0 t \<in> A"
          "infdist (flow y t') seg \<ge> e"
          "\<And>t. t \<in> {0 .. t'} \<Longrightarrow> flow y t \<in> A"
            apply (auto )
            apply fact+
            apply (metis atLeastAtMost_iff flow_in)
            apply (metis t'(2))
            by (metis flow_y_in atLeastAtMost_iff)
          thus ?thesis ..
        qed
        {
          fix s assume s: "s \<in> {0 .. t'}"
          hence "0 \<le> s" by simp
          have "s \<le> b"
            using  t t' s b
            using ivl_subset_existence_ivl[OF `y \<in> X` t(2)]
            using ivl_subset_existence_ivl[OF x0 b]
            by auto
          hence sx0: "s \<in> existence_ivl x0"
            using s ivl_subset_existence_ivl[OF x0 b]
            by auto
          have sy: "s \<in> existence_ivl y"
            using ivl_subset_existence_ivl[OF `y \<in> X` t(2)] s t'
            by auto
          have int: "flow y s - flow x0 s = y - x0 + (integral {0 .. s} (\<lambda>t. f (flow y t)) - integral {0 .. s} (\<lambda>t. f (flow x0 t)))"
            unfolding flow_fixed_point[OF `0 \<le> s` sx0 x0]
              flow_fixed_point[OF `0 \<le> s` sy `y \<in> X`]
            by (simp add: algebra_simps)
          have "norm (flow y s - flow x0 s) \<le> norm (y - x0) +
            norm (integral {0 .. s} (\<lambda>t. f (flow y t)) - integral {0 .. s} (\<lambda>t. f (flow x0 t)))"
            unfolding int
            by (rule norm_triangle_ineq)
          also
          have "norm (integral {0 .. s} (\<lambda>t. f (flow y t)) - integral {0 .. s} (\<lambda>t. f (flow x0 t))) =
            norm (integral {0 .. s} (\<lambda>t. f (flow y t) - f (flow x0 t)))"
            using ivl_subset_existence_ivl[OF _ sx0] ivl_subset_existence_ivl[OF _ sy]
            by (subst integral_sub)
              (auto intro!: integrable_continuous_real continuous_at_imp_continuous_on
              f_flow_continuous `y \<in> X` `x0 \<in> X`)
          also have "\<dots> \<le> (integral {0 .. s} (\<lambda>t. norm (f (flow y t) - f (flow x0 t))))"
            apply (rule integral_norm_bound_integral)
            using ivl_subset_existence_ivl[OF _ sx0] ivl_subset_existence_ivl[OF _ sy]
            by (auto intro!: integrable_continuous_real continuous_at_imp_continuous_on
                continuous_intros f_flow_continuous `y \<in> X` `x0 \<in> X`)
          also have "\<dots> \<le> (integral {0 .. s} (\<lambda>t. K * norm ((flow y t) - (flow x0 t))))"
            apply (auto intro!: integral_le)
            using ivl_subset_existence_ivl[OF _ sx0] ivl_subset_existence_ivl[OF _ sy]
            apply (auto intro!: integrable_continuous_real continuous_at_imp_continuous_on
              lipschitz_norm_leI[OF K]
                continuous_intros f_flow_continuous flow_continuous `y \<in> X` `x0 \<in> X`)
            apply -
            apply (metis atLeastAtMost_iff order_trans s t'(5))
            by (metis atLeastAtMost_iff order_trans s t'(3))
          also have "\<dots> = K * integral {0 .. s} (\<lambda>t. norm (flow y t - flow x0 t))"
            apply (subst integral_mult)
            using ivl_subset_existence_ivl[OF _ sx0] ivl_subset_existence_ivl[OF _ sy]
            by (auto intro!: integrable_continuous_real continuous_at_imp_continuous_on
              lipschitz_norm_leI[OF K]
                continuous_intros f_flow_continuous flow_continuous `y \<in> X` `x0 \<in> X`)
          finally have norm: "norm (flow y s - flow x0 s) \<le> norm (y - x0) + K * integral {0 .. s} (\<lambda>t. norm (flow y t - flow x0 t))"
            by arith
          note norm `s \<le> b` sx0 sy
        } note norm_le = this
        from norm_le(2) t' have "t' \<in> closed_segment 0 b"
          by (auto simp: closed_segment_real)
        hence "infdist (flow y t') seg \<le> dist (flow y t') (flow x0 t')"
          by (auto simp: seg_def infdist_le)
        also have "\<dots> \<le> norm (flow y t' - flow x0 t')"
          by (simp add: dist_norm)
        also have "\<dots> \<le> norm (y - x0) * exp (K * \<bar>t'\<bar>)"
          unfolding K_def
          apply (rule exponential_initial_condition[OF _ _ _ _ _ _ _ K'])
          apply (metis atLeastAtMost_iff local.norm_le(4) order_refl t'(1))
          apply (metis `y \<in> A`)
          apply (metis atLeastAtMost_iff local.norm_le(3) order_refl t'(1))
          using e apply (simp add: A_def)
          apply fact
          apply (metis closed_segment_real t'(1,5))
          apply (metis closed_segment_real t'(1,3))
          done
        also have "\<dots> < d * exp (K * t)"
          apply (rule mult_less_le_imp_less)
          using y d t' t
          by (auto simp: dist_norm[symmetric] dist_commute intro!: mult_mono `0 \<le> K`)
        also have "\<dots> \<le> e"
          apply (rule d_times_exp_le)
          apply fact+
          done
        finally
        have "infdist (flow y t') seg < e" .
        with `infdist (flow y t') seg \<ge> e` show False
          by (auto simp: frontier_def)
      qed
    } note in_A = this

    have b_in: "b \<in> existence_ivl y"
    proof (rule ccontr)
      assume "b \<notin> existence_ivl y"
      hence disj: "b \<le> inf_existence y \<or> sup_existence y \<le> b"
        apply (auto simp: existence_ivl_def[OF `y \<in> X`]
          real_image_ereal_ivl split: split_if_asm)
        apply (metis ereal_infinity_cases ereal_less_real_iff not_le)
        apply (metis ereal_infinity_cases not_le real_less_ereal_iff)
        apply (metis ereal_infinity_cases ereal_less_eq(1) not_le real_less_ereal_iff)
        by (metis ereal_infinity_cases ereal_less_eq(2) ereal_less_real_iff not_less)
        from existence_ivl_zero[OF `y \<in> X`]
      have "0 \<le> sup_existence y"
        apply (auto simp add: real_image_ereal_ivl existence_ivl_def[OF `y \<in> X`]
          split: split_if_asm)
        apply (metis less_imp_le zero_less_real_of_ereal)+
        done
      with existence_ivl_zero[OF `y \<in> X`] `0 \<le> b` disj
      have sup_le: "sup_existence y \<le> b"
        apply (auto simp: `y \<in> X` existence_ivl_def)
        by (metis ereal_infinity_cases ereal_less_eq(1) ereal_less_real_iff le_less_trans less_ereal.simps(3) not_less)
      {
        fix t::real assume t: "0 \<le> t" "t \<in> existence_ivl y"
        hence "t < b"
          using sup_le
          apply (auto simp: existence_ivl_def[OF `y \<in> X`] real_less_ereal_iff)
          by (metis less_ereal.simps(1) less_le_trans)
        note in_A[OF t less_imp_le[OF this]]
      } note in_A = this
      from sup_le have "sup_existence y < \<infinity>"
        by auto
      from flow_leaves_compact_ivl[OF `y \<in> X` this `compact A` `A \<subseteq> X`]
      obtain t where t: "0 \<le> t" "t \<in> existence_ivl y" "flow y t \<notin> A" by auto
      from in_A[OF t(1,2)] t(3)
      show False
        by simp
    qed
    {
      fix t assume t: "t \<in> {0 .. b}"
      also note ivl_subset_existence_ivl[OF `y \<in> X` b_in]
      finally have t_in: "t \<in> existence_ivl y" .

      note t
      also note ivl_subset_existence_ivl[OF `x0 \<in> X` assms(2)]
      finally have t_in': "t \<in> existence_ivl x0" .
      have "norm (flow y t - flow x0 t) \<le> norm (y - x0) * exp (K * \<bar>t\<bar>)"
        unfolding K_def
        apply (rule exponential_initial_condition[OF t_in `y \<in> A` t_in' `x0 \<in> A` `A \<subseteq> X` _ _ K'])
        defer
        using t `0 < e` apply (auto simp: A_def seg_def closed_segment_real)[1]
        apply (rule in_A)
        using t ivl_subset_existence_ivl[OF `y \<in> X` b_in]
        apply (auto simp: closed_segment_real split: split_if_asm)
        done
      hence "dist (flow x0 t) (flow y t) \<le> dist x0 y * exp (K * \<bar>t\<bar>)"
        by (auto simp: dist_norm[symmetric] dist_commute)
    }
    note b_in this
  } note * = `d > 0` `K > 0` `ball x0 d \<subseteq> X` this
  moreover
  {
    fix e::real assume "0 < e"
    have "eventually (\<lambda>y. y \<in> ball x0 d) (at x0)"
      using `d > 0`
      by (rule eventually_at_in_ball)
    hence "eventually (\<lambda>y. \<forall>t\<in>{0..b}. dist (flow x0 t) (flow y t) \<le> dist x0 y * exp (K * \<bar>t\<bar>)) (at x0)"
      by eventually_elim (safe intro!: *)
    moreover
    have "eventually (\<lambda>y. \<forall>t\<in>{0..b}. dist x0 y * exp (K * \<bar>t\<bar>) \<le> dist x0 y * exp (K * b)) (at x0)"
      apply eventually_elim
      using `0 \<le> b` `0 < K`
      apply (auto intro!: mult_left_mono)
      done
    moreover
    have "eventually (\<lambda>y. dist x0 y * exp (K * b) < e) (at x0)"
      using `0 < e` by (auto intro!: order_tendstoD tendsto_eq_intros)
    ultimately
    have "eventually (\<lambda>y. \<forall>t\<in>{0..b}. dist (flow x0 t) (flow y t) < e) (at x0)"
      by eventually_elim force
  }
  ultimately show ?thesis ..
qed

lemma
  global_left_existence_interval:
  assumes "b \<le> 0"
  assumes b: "b \<in> existence_ivl x0"
  assumes x0: "x0 \<in> X"
  obtains d K where "d > 0" "K > 0"
    "ball x0 d \<subseteq> X"
    "\<And>y. y \<in> ball x0 d \<Longrightarrow> b \<in> existence_ivl y"
    "\<And>t y. y \<in> ball x0 d \<Longrightarrow> t \<in> {b .. 0} \<Longrightarrow> dist (flow x0 t) (flow y t) \<le> dist x0 y * exp (K * abs t)"
    "\<And>e. e > 0 \<Longrightarrow> eventually (\<lambda>y. \<forall>t \<in> {b .. 0}. dist (flow x0 t) (flow y t) < e) (at x0)"
proof -
  interpret rev!: c1_on_open "-f" "-f'"
    using derivative_rhs continuous_derivative
    by unfold_locales (auto intro!: continuous_intros derivative_eq_intros
      simp: fun_Compl_def)
  from assms have "-b \<ge> 0" "-b \<in> rev.existence_ivl x0"
    by (auto simp: flow_eq_rev)
  from rev.global_right_existence_interval[OF this `x0 \<in> X`]
  obtain d K where dK: "d > 0" "K > 0"
    "ball x0 d \<subseteq> X"
    "\<And>y. y \<in> ball x0 d \<Longrightarrow> -b \<in> rev.existence_ivl y"
    "\<And>t y. y \<in> ball x0 d \<Longrightarrow> t \<in> {0 .. -b} \<Longrightarrow> dist (rev.flow x0 t) (rev.flow y t) \<le> dist x0 y * exp (K * abs t)"
    "\<And>e. e > 0 \<Longrightarrow> eventually (\<lambda>y. \<forall>t \<in> {0 .. -b}. dist (rev.flow x0 t) (rev.flow y t) < e) (at x0)"
    by (auto simp: rev_flow_eq rev_existence_ivl_eq `x0 \<in> X`)
  from dK(3,4) have 4: "\<And>y. y \<in> ball x0 d \<Longrightarrow> b \<in> existence_ivl y"
    by (metis minus_minus rev_existence_ivl_eq subsetCE)
  {
    fix t y assume yt: "y \<in> ball x0 d" "t \<in> {b .. 0}"
    with dK(3) have yx0: "y \<in> X" "x0 \<in> ball x0 d" using `d > 0` by auto
    from yt yx0 rev.closed_segment_subset_existence_ivl[OF _ dK(4)[OF yt(1)]]
    have "- t \<in> c1_on_open.existence_ivl (- f) X y"
      by (auto simp: closed_segment_real)
    moreover
    from yt `x0 \<in> X` rev.closed_segment_subset_existence_ivl[OF _ dK(4)[OF `x0 \<in> ball x0 d`]]
    have "- t \<in> c1_on_open.existence_ivl (- f) X x0"
      by (auto simp: closed_segment_real)
    ultimately
    have "dist (flow x0 t) (flow y t) \<le> dist x0 y * exp (K * abs t)"
      using yt dK(5)[of y "-t"] rev_flow_eq[OF `x0 \<in> X`, of "-t"] rev_flow_eq[OF `y \<in> X`, of "-t"]
      by (auto simp: dist_commute closed_segment_real)
  } note 5 = this
  {
    fix e::real assume "0 < e"
    have "eventually (\<lambda>y. y \<in> ball x0 d) (at x0)"
      using `d > 0` by (rule eventually_at_in_ball)
    hence "eventually (\<lambda>y. \<forall>t\<in>{0..-b}. dist (rev.flow x0 t) (rev.flow y t)
        = dist (flow x0 (-t)) (flow y (-t))) (at x0)"
    proof eventually_elim
      case elim
      hence "y \<in> X" "-b \<in> rev.existence_ivl y" using dK by auto
      from rev.closed_segment_subset_existence_ivl[OF this]
        rev.closed_segment_subset_existence_ivl[OF `x0 \<in> X` `-b \<in> rev.existence_ivl x0`]
      show ?case
        by (force simp: `x0 \<in> X` `y \<in> X` closed_segment_real rev_flow_eq)
    qed
    moreover
    note dK(6)[OF `0 < e`]
    ultimately
    have "eventually (\<lambda>y. \<forall>t\<in>{b..0}. dist (flow x0 t) (flow y t) < e) (at x0)"
      by eventually_elim (auto simp: dest: bspec[where x="-t" for t])
  } note 6 = this
  from dK(1-3) 4 5 6 show ?thesis ..
qed

lemma
  global_existence_interval:
  assumes a: "a \<in> existence_ivl x0"
  assumes b: "b \<in> existence_ivl x0"
  assumes le: "a \<le> b"
  assumes x0: "x0 \<in> X"
  obtains d K where "d > 0" "K > 0"
    "ball x0 d \<subseteq> X"
    "\<And>y. y \<in> ball x0 d \<Longrightarrow> a \<in> existence_ivl y"
    "\<And>y. y \<in> ball x0 d \<Longrightarrow> b \<in> existence_ivl y"
    "\<And>t y. y \<in> ball x0 d \<Longrightarrow> t \<in> {a .. b} \<Longrightarrow> dist (flow x0 t) (flow y t) \<le> dist x0 y * exp (K * abs t)"
    "\<And>e. e > 0 \<Longrightarrow> eventually (\<lambda>y. \<forall>t \<in> {a .. b}. dist (flow x0 t) (flow y t) < e) (at x0)"
proof -
  {
    assume nonneg: "a \<ge> 0" "b \<ge> 0"
    from global_right_existence_interval[OF `b \<ge> 0` b x0] guess d K . note dK = this
    hence "d > 0" "K > 0"
      "ball x0 d \<subseteq> X"
      "\<And>y. y \<in> ball x0 d \<Longrightarrow> a \<in> existence_ivl y"
      "\<And>y. y \<in> ball x0 d \<Longrightarrow> b \<in> existence_ivl y"
      "\<And>t y. y \<in> ball x0 d \<Longrightarrow> t \<in> {a .. b} \<Longrightarrow> dist (flow x0 t) (flow y t) \<le> dist x0 y * exp (K * abs t)"
      "\<And>e. e > 0 \<Longrightarrow> eventually (\<lambda>y. \<forall>t \<in> {a .. b}. dist (flow x0 t) (flow y t) < e) (at x0)"
      using nonneg
    proof (auto intro!: dK)
      case goal1
      hence "y \<in> X" "b \<in> c1_on_open.existence_ivl f X y" by auto
      from ivl_subset_existence_ivl[OF this] le nonneg
      show ?case by auto
    next
      case goal2
      from goal2(7)[OF `0 < e`]
      have "eventually (\<lambda>y. \<forall>t\<in>{0..b}. dist (flow x0 t) (flow y t) < e) (at x0)"
        .
      thus ?case
        apply eventually_elim
        using le nonneg
        apply (auto )
        done
    qed
    hence ?thesis ..
  } moreover {
    assume nonpos: "0 \<ge> a" "0 \<ge> b"
    from global_left_existence_interval[OF `0 \<ge> a` a x0] guess d K . note dK = this
    hence "d > 0" "K > 0"
      "ball x0 d \<subseteq> X"
      "\<And>y. y \<in> ball x0 d \<Longrightarrow> a \<in> existence_ivl y"
      "\<And>y. y \<in> ball x0 d \<Longrightarrow> b \<in> existence_ivl y"
      "\<And>t y. y \<in> ball x0 d \<Longrightarrow> t \<in> {a .. b} \<Longrightarrow> dist (flow x0 t) (flow y t) \<le> dist x0 y * exp (K * abs t)"
      "\<And>e. e > 0 \<Longrightarrow> eventually (\<lambda>y. \<forall>t \<in> {a .. b}. dist (flow x0 t) (flow y t) < e) (at x0)"
      using nonpos
    proof (auto intro!: dK)
      case goal1
      hence "y \<in> X" "a \<in> c1_on_open.existence_ivl f X y" by auto
      from ivl_subset_existence_ivl'[OF this] le nonpos
      show ?case by auto
    next
      case goal2
      from goal2(7)[OF `0 < e`]
      have "eventually (\<lambda>y. \<forall>t\<in>{a..0}. dist (flow x0 t) (flow y t) < e) (at x0)"
        .
      thus ?case
        apply eventually_elim
        using le nonpos
        apply (auto )
        done
    qed
    hence ?thesis ..
  } moreover {
    assume lr: "a \<le> 0" "0 \<le> b"
    from global_left_existence_interval[OF `0 \<ge> a` a x0] guess d1 K1 . note dK1 = this
    from global_right_existence_interval[OF `b \<ge> 0` b x0] guess d2 K2 . note dK2 = this
    from dK1 dK2 have "min d1 d2 > 0" "max K1 K2 > 0"
      "ball x0 (min d1 d2) \<subseteq> X"
      "\<And>y. y \<in> ball x0 (min d1 d2) \<Longrightarrow> a \<in> existence_ivl y"
      "\<And>y. y \<in> ball x0 (min d1 d2) \<Longrightarrow> b \<in> existence_ivl y"
      "\<And>t y. y \<in> ball x0 (min d1 d2) \<Longrightarrow> t \<in> {a .. b} \<Longrightarrow> dist (flow x0 t) (flow y t) \<le> dist x0 y * exp (max K1 K2 * abs t)"
      "\<And>e. e > 0 \<Longrightarrow> eventually (\<lambda>y. \<forall>t \<in> {a .. b}. dist (flow x0 t) (flow y t) < e) (at x0)"
      using lr
    proof (auto intro!: dK1 dK2)
      case goal1
      show ?case
      proof cases
        assume "0 \<le> t"
        have "dist (flow x0 t) (flow y t) \<le> dist x0 y * exp (K2 * \<bar>t\<bar>)"
          apply (auto intro!: dK2)
          using goal1 `0 \<le> t`
          by auto
        also have "\<dots> \<le> dist x0 y * exp (max K1 K2 * abs t)"
          by (auto simp: intro!: mult_left_mono mult_right_mono)
        finally show ?case .
      next
        assume "\<not>0 \<le> t"
        have "dist (flow x0 t) (flow y t) \<le> dist x0 y * exp (K1 * \<bar>t\<bar>)"
          apply (auto intro!: dK1)
          using goal1 `\<not>0 \<le> t`
          by auto
        also have "\<dots> \<le> dist x0 y * exp (max K1 K2 * abs t)"
          by (auto simp: intro!: mult_left_mono mult_right_mono)
        finally show ?case .
      qed
    next
      case goal2
      from dK1(6)[OF `0 < e`] dK2(6)[OF `0 < e`]
      show ?case
        by eventually_elim auto
    qed
    hence ?thesis ..
  } ultimately show ?thesis using le by arith
qed

lemma open_state_space: "open (Sigma X existence_ivl)"
  and flow_continuous_on_state_space: "continuous_on (Sigma X existence_ivl) (\<lambda>(x, t). flow x t)"
proof (safe intro!: openI continuous_at_imp_continuous_on)
  fix t x assume "x \<in> X" and t: "t \<in> existence_ivl x"
  with open_existence_ivl[OF `x \<in> X`] obtain e where e: "e > 0" "cball t e \<subseteq> existence_ivl x"
    by (metis open_contains_cball)
  hence "t - e \<in> existence_ivl x" "t + e \<in> existence_ivl x" "t - e \<le> t + e"
    by (auto simp: cball_def dist_real_def)
  from global_existence_interval[OF this `x \<in> X`] guess d K . note dK = this
  let ?T = "ball x d \<times> ball t e"
  have "open ?T" by (auto intro!: open_Times)
  moreover have "(x, t) \<in> ?T" by (auto simp: dK `0 < e`)
  moreover have "?T \<subseteq> Sigma X existence_ivl"
  proof safe
    fix s y assume y: "y \<in> ball x d" and s: "s \<in> ball t e"
    with `ball x d \<subseteq> X` show "y \<in> X" by auto
    have "ball t e \<subseteq> closed_segment 0 (t - e) \<union> closed_segment 0 (t + e)"
      by (auto simp: closed_segment_real dist_real_def)
    with s closed_segment_subset_existence_ivl[OF `y \<in> X` dK(4)[OF y]]
      closed_segment_subset_existence_ivl[OF `y \<in> X` dK(5)[OF y]]
    show "s \<in> existence_ivl y"
      by auto
  qed
  ultimately show "\<exists>T. open T \<and> (x, t) \<in> T \<and> T \<subseteq> Sigma X (c1_on_open.existence_ivl f X)"
    by blast
  {
    fix eps :: real assume "eps > 0"
    have "eventually (\<lambda>xa. norm (flow (x + fst xa) (t + snd xa) - flow x t) =
      norm (flow (x + fst xa) (t + snd xa) - flow x (t + snd xa) + (flow x (t + snd xa) - flow x t))) (at 0)"
      by auto
    moreover
    have "eventually (\<lambda>xa. norm (flow (x + fst xa) (t + snd xa) - flow x (t + snd xa) + (flow x (t + snd xa) - flow x t)) \<le>
      norm (flow (x + fst xa) (t + snd xa) - flow x (t + snd xa)) + norm (flow x (t + snd xa) - flow x t)) (at 0)"
      by eventually_elim (rule norm_triangle_ineq)
    moreover
    have "eventually (\<lambda>xa. t + snd xa \<in> ball t e) (at 0)"
      by (auto simp: dist_real_def intro!: order_tendstoD[OF _ `0 < e`]) (auto intro!: tendsto_eq_intros)
    moreover from dK(7)[OF `eps > 0`]
    have "eventually (\<lambda>h. \<forall>t\<in>{t - e..t + e}. dist (flow x t) (flow (x + h) t) < eps) (at (fst (0::'a*real)))"
      apply (subst (asm) eventually_at_shift_zero[symmetric])
      apply simp
      done
    hence "eventually (\<lambda>h::(_ * real). \<forall>t\<in>{t - e..t + e}. dist (flow x t) (flow (x + fst h) t) < eps) (at 0)"
      apply (rule eventually_at_fst)
      using `eps > 0` apply simp done
    moreover
    have "eventually (\<lambda>h. norm (flow x (t + h) - flow x t) < eps) (at (snd (0::'a*real)))"
      using flow_continuous[OF `x \<in> X` t, unfolded isCont_def, THEN tendstoD, OF `eps > 0`]
      by (subst (asm) eventually_at_shift_zero[symmetric]) (auto simp: dist_norm)
    hence "eventually (\<lambda>h::('a * _). norm (flow x (t + snd h) - flow x t) < eps) (at 0)"
      apply (rule eventually_at_snd)
      using `eps > 0` apply simp done
    ultimately
    have "eventually (\<lambda>xa. norm (flow (x + fst xa) (t + snd xa) - flow x t) < 2 * eps) (at 0)"
    proof eventually_elim
      case elim
      note elim(1)
      also note elim(2)
      also note elim(5)
      also
      from elim(3) have "t + snd xa \<in> {t - e..t + e}" by (auto simp: dist_real_def algebra_simps)
      from elim(4)[rule_format, OF this]
      have "norm (c1_on_open.flow f X (x + fst xa) (t + snd xa) - c1_on_open.flow f X x (t + snd xa)) < eps"
        by (auto simp: dist_commute dist_norm[symmetric])
      finally
      show ?case by simp
    qed
  } note ** = this
  {
    fix eps::real assume "eps > 0"
    hence "eps / 2 > 0" by simp
    from **[OF this]
    have *: "eventually (\<lambda>xa. norm (flow (x + fst xa) (t + snd xa) - flow x t) < eps) (at 0)"
      by auto
  } note * = this
  show "isCont (\<lambda>(x, y). flow x y) (x, t)"
    unfolding isCont_iff
    apply (rule LIM_zero_cancel)
    apply (auto simp: split_beta' norm_conv_dist[symmetric] intro!: tendstoI *)
    done
qed

lemma flow_isCont_state_space: "x \<in> X \<Longrightarrow> t \<in> existence_ivl x \<Longrightarrow> isCont (\<lambda>(x, t). flow x t) (x, t)"
  using flow_continuous_on_state_space
  by (auto simp: continuous_on_eq_continuous_within at_within_open[OF _ open_state_space])

end

end
