Theory Ordinary_Differential_Equations.Picard_Lindeloef_Qualitative

theory Picard_Lindeloef_Qualitative
imports Initial_Value_Problem
begin

subsection ‹Picard-Lindeloef On Open Domains›
text‹\label{sec:qpl}›

subsubsection ‹Local Solution with local Lipschitz›
text‹\label{sec:qpl-lipschitz}›

lemma cball_eq_closed_segment_real:
  fixes x e::real
  shows "cball x e = (if e ≥ 0 then {x - e -- x + e} else {})"
  by (auto simp: closed_segment_eq_real_ivl dist_real_def mem_cball)

lemma cube_in_cball:
  fixes x y :: "'a::euclidean_space"
  assumes "r > 0"
  assumes "⋀i. i∈ Basis ⟹ dist (x ∙ i) (y ∙ i) ≤ r / sqrt(DIM('a))"
  shows "y ∈ cball x r"
  unfolding mem_cball euclidean_dist_l2[of x y] L2_set_def
proof -
  have "(∑i∈Basis. (dist (x ∙ i) (y ∙ i))⇧2) ≤ (∑(i::'a)∈Basis. (r / sqrt(DIM('a)))⇧2)"
  proof (intro sum_mono)
    fix i :: 'a
    assume "i ∈ Basis"
    thus "(dist (x ∙ i) (y ∙ i))⇧2 ≤ (r / sqrt(DIM('a)))⇧2"
      using assms
      by (auto intro: sqrt_le_D)
  qed
  moreover
  have "... ≤ r⇧2"
    using assms by (simp add: power_divide)
  ultimately
  show "sqrt (∑i∈Basis. (dist (x ∙ i) (y ∙ i))⇧2) ≤ r"
    using assms by (auto intro!: real_le_lsqrt sum_nonneg)
qed

lemma cbox_in_cball':
  fixes x::"'a::euclidean_space"
  assumes "0 < r"
  shows "∃b > 0. b ≤ r ∧ (∃B. B = (∑i∈Basis. b *⇩R i) ∧ (∀y ∈ cbox (x - B) (x + B). y ∈ cball x r))"
proof (rule, safe)
  have "r / sqrt (real DIM('a)) ≤ r / 1"
    using assms  by (auto simp: divide_simps real_of_nat_ge_one_iff)
  thus "r / sqrt (real DIM('a)) ≤ r" by simp
next
  let ?B = "∑i∈Basis. (r / sqrt (real DIM('a))) *⇩R i"
  show "∃B. B = ?B ∧ (∀y ∈ cbox (x - B) (x + B). y ∈ cball x r)"
  proof (rule, safe)
    fix y::'a
    assume "y ∈ cbox (x - ?B) (x + ?B)"
    hence bounds:
      "⋀i. i ∈ Basis ⟹ (x - ?B) ∙ i ≤ y ∙ i"
      "⋀i. i ∈ Basis ⟹ y ∙ i ≤ (x + ?B) ∙ i"
      by (auto simp: mem_box)
    show "y ∈ cball x r"
    proof (intro cube_in_cball)
      fix i :: 'a
      assume "i∈ Basis"
      with bounds
      have bounds_comp:
        "x ∙ i - r / sqrt (real DIM('a)) ≤ y ∙ i"
        "y ∙ i ≤ x ∙ i + r / sqrt (real DIM('a))"
        by (auto simp: algebra_simps)
      thus "dist (x ∙ i) (y ∙ i) ≤ r / sqrt (real DIM('a))"
        unfolding dist_real_def by simp
    qed (auto simp add: assms)
  qed (rule)
qed (auto simp: assms)

lemma Pair1_in_Basis: "i ∈ Basis ⟹ (i, 0) ∈ Basis"
 and Pair2_in_Basis: "i ∈ Basis ⟹ (0, i) ∈ Basis"
  by (auto simp: Basis_prod_def)

lemma le_real_sqrt_sumsq' [simp]: "y ≤ sqrt (x * x + y * y)"
  by (simp add: power2_eq_square [symmetric])

lemma cball_Pair_split_subset: "cball (a, b) c ⊆ cball a c × cball b c"
  by (auto simp: dist_prod_def mem_cball power2_eq_square
      intro: order_trans[OF le_real_sqrt_sumsq] order_trans[OF le_real_sqrt_sumsq'])

lemma cball_times_subset: "cball a (c/2) × cball b (c/2) ⊆ cball (a, b) c"
proof -
  {
    fix a' b'
    have "sqrt ((dist a a')⇧2 + (dist b b')⇧2) ≤ dist a a' + dist b b'"
      by (rule real_le_lsqrt) (auto simp: power2_eq_square algebra_simps)
    also assume "a' ∈ cball a (c / 2)"
    then have "dist a a' ≤ c / 2" by (simp add: mem_cball)
    also assume "b' ∈ cball b (c / 2)"
    then have "dist b b' ≤ c / 2" by (simp add: mem_cball)
    finally have "sqrt ((dist a a')⇧2 + (dist b b')⇧2) ≤ c"
      by simp
  } thus ?thesis by (auto simp: dist_prod_def mem_cball)
qed

lemma eventually_bound_pairE:
  assumes "isCont f (t0, x0)"
  obtains B where
    "B ≥ 1"
    "eventually (λe. ∀x ∈ cball t0 e × cball x0 e. norm (f x) ≤ B) (at_right 0)"
proof -
  from assms[simplified isCont_def, THEN tendstoD, OF zero_less_one]
  obtain d::real where d: "d > 0"
    "⋀x. x ≠ (t0, x0) ⟹ dist x (t0, x0) < d ⟹ dist (f x) (f (t0, x0)) < 1"
    by (auto simp: eventually_at)
  have bound: "norm (f (t, x)) ≤ norm (f (t0, x0)) + 1"
    if "t ∈ cball t0 (d/3)" "x ∈ cball x0 (d/3)" for t x
  proof -
    from that have "norm (f (t, x) - f (t0, x0)) < 1"
      using ‹0 < d›
      unfolding dist_norm[symmetric]
      apply (cases "(t, x) = (t0, x0)", force)
      by (rule d) (auto simp: dist_commute dist_prod_def mem_cball
        intro!: le_less_trans[OF sqrt_sum_squares_le_sum_abs])
    then show ?thesis
      by norm
  qed
  have "norm (f (t0, x0)) + 1 ≥ 1"
    "eventually (λe. ∀x ∈ cball t0 e × cball x0 e.
      norm (f x) ≤ norm (f (t0, x0)) + 1) (at_right 0)"
    using d(1) bound
    by (auto simp: eventually_at dist_real_def mem_cball intro!: exI[where x="d/3"])
  thus ?thesis ..
qed

lemma
  eventually_in_cballs:
  assumes "d > 0" "c > 0"
  shows "eventually (λe. cball t0 (c * e) × (cball x0 e) ⊆ cball (t0, x0) d) (at_right 0)"
  using assms
  by (auto simp: eventually_at dist_real_def field_simps dist_prod_def mem_cball
    intro!: exI[where x="min d (d / c) / 3"]
    order_trans[OF sqrt_sum_squares_le_sum_abs])

lemma cball_eq_sing':
  fixes x :: "'a::{metric_space,perfect_space}"
  shows "cball x e = {y} ⟷ e = 0 ∧ x = y"
  using cball_eq_sing[of x e]
  apply (cases "x = y", force)
  by (metis cball_empty centre_in_cball insert_not_empty not_le singletonD)

locale ll_on_open = interval T for T +
  fixes f::"real ⇒ 'a::{banach, heine_borel} ⇒ 'a" and X
  assumes local_lipschitz: "local_lipschitz T X f"
  assumes cont: "⋀x. x ∈ X ⟹ continuous_on T (λt. f t x)"
  assumes open_domain[intro!, simp]: "open T" "open X"
begin

text ‹all flows on closed segments›

definition csols where
  "csols t0 x0 = {(x, t1). {t0--t1} ⊆ T ∧ x t0 = x0 ∧ (x solves_ode f) {t0--t1} X}"

text ‹the maximal existence interval›

definition "existence_ivl t0 x0 = (⋃(x, t1)∈csols t0 x0 . {t0--t1})"

text ‹witness flow›

definition "csol t0 x0 = (SOME csol. ∀t ∈ existence_ivl t0 x0. (csol t, t) ∈ csols t0 x0)"

text ‹unique flow›

definition flow where "flow t0 x0 = (λt. if t ∈ existence_ivl t0 x0 then csol t0 x0 t t else 0)"

end

locale ll_on_open_it =
  general?:― ‹TODO: why is this qualification necessary? It seems only because of @{thm ll_on_open_it_axioms}›
  ll_on_open + fixes t0::real
  ― ‹if possible, all development should be done with ‹t0› as explicit parameter for initial time:
    then it can be instantiated with ‹0› for autonomous ODEs›

context ll_on_open begin

sublocale ll_on_open_it where t0 = t0  for t0 ..

sublocale continuous_rhs T X f
  by unfold_locales (rule continuous_on_TimesI[OF local_lipschitz cont])

end

context ll_on_open_it begin

lemma ll_on_open_rev[intro, simp]: "ll_on_open (preflect t0 ` T) (λt. - f (preflect t0 t)) X"
  using local_lipschitz interval
  by unfold_locales
    (auto intro!: continuous_intros cont intro: local_lipschitz_compose1
      simp: fun_Compl_def local_lipschitz_minus local_lipschitz_subset open_neg_translation
        image_image preflect_def)

lemma eventually_lipschitz:
  assumes "t0 ∈ T" "x0 ∈ X" "c > 0"
  obtains L where
    "eventually (λu. ∀t' ∈ cball t0 (c * u) ∩ T.
      L-lipschitz_on (cball x0 u ∩ X) (λy. f t' y)) (at_right 0)"
proof -
  from local_lipschitzE[OF local_lipschitz, OF ‹t0 ∈ T› ‹x0 ∈ X›]
  obtain u L where
    "u > 0"
    "⋀t'. t' ∈ cball t0 u ∩ T ⟹ L-lipschitz_on (cball x0 u ∩ X) (λy. f t' y)"
    by auto
  hence "eventually (λu. ∀t' ∈ cball t0 (c * u) ∩ T.
      L-lipschitz_on (cball x0 u ∩ X) (λy. f t' y)) (at_right 0)"
    using ‹u > 0› ‹c > 0›
    by (auto simp: dist_real_def eventually_at divide_simps algebra_simps
      intro!: exI[where x="min u (u / c)"]
      intro: lipschitz_on_subset[where E="cball x0 u ∩ X"])
  thus ?thesis ..
qed

lemmas continuous_on_Times_f = continuous
lemmas continuous_on_f = continuous_rhs_comp

lemma
  lipschitz_on_compact:
  assumes "compact K" "K ⊆ T"
  assumes "compact Y" "Y ⊆ X"
  obtains L where "⋀t. t ∈ K ⟹ L-lipschitz_on Y (f t)"
proof -
  have cont: "⋀x. x ∈ Y ⟹ continuous_on K (λt. f t x)"
    using ‹Y ⊆ X› ‹K ⊆ T›
    by (auto intro!: continuous_on_f continuous_intros)
  from local_lipschitz
  have "local_lipschitz K Y f"
    by (rule local_lipschitz_subset[OF _ ‹K ⊆ T› ‹Y ⊆ X›])
  from local_lipschitz_compact_implies_lipschitz[OF this ‹compact Y› ‹compact K› cont] that
  show ?thesis by metis
qed

lemma csols_empty_iff: "csols t0 x0 = {} ⟷ t0 ∉ T ∨ x0 ∉ X"
proof cases
  assume iv_defined: "t0 ∈ T ∧ x0 ∈ X"
  then have "(λ_. x0, t0) ∈ csols t0 x0"
    by (auto simp: csols_def intro!: solves_ode_singleton)
  then show ?thesis using ‹t0 ∈ T ∧ x0 ∈ X› by auto
qed (auto simp: solves_ode_domainD csols_def)

lemma csols_notempty: "t0 ∈ T ⟹ x0 ∈ X ⟹ csols t0 x0 ≠ {}"
  by (simp add: csols_empty_iff)


lemma existence_ivl_empty_iff[simp]: "existence_ivl t0 x0 = {} ⟷ t0 ∉ T ∨ x0 ∉ X"
  using csols_empty_iff
  by (auto simp: existence_ivl_def)

lemma existence_ivl_empty1[simp]: "t0 ∉ T ⟹ existence_ivl t0 x0 = {}"
  and existence_ivl_empty2[simp]: "x0 ∉ X ⟹ existence_ivl t0 x0 = {}"
  using csols_empty_iff
  by (auto simp: existence_ivl_def)

lemma flow_undefined:
  shows "t0 ∉ T ⟹ flow t0 x0 = (λ_. 0)"
    "x0 ∉ X ⟹ flow t0 x0 = (λ_. 0)"
  using existence_ivl_empty_iff
  by (auto simp: flow_def)

lemma (in ll_on_open) flow_eq_in_existence_ivlI:
  assumes "⋀u. x0 ∈ X ⟹ u ∈ existence_ivl t0 x0 ⟷ g u ∈ existence_ivl s0 x0"
  assumes "⋀u. x0 ∈ X ⟹ u ∈ existence_ivl t0 x0 ⟹ flow t0 x0 u = flow s0 x0 (g u)"
  shows "flow t0 x0 = (λt. flow s0 x0 (g t))"
  apply (cases "x0 ∈ X")
  subgoal using assms by (auto intro!: ext simp: flow_def)
  subgoal by (simp add: flow_undefined)
  done


subsubsection ‹Global maximal flow with local Lipschitz›
text‹\label{sec:qpl-global-flow}›

lemma local_unique_solution:
  assumes iv_defined: "t0 ∈ T" "x0 ∈ X"
  obtains et ex B L
  where "et > 0" "0 < ex" "cball t0 et ⊆ T" "cball x0 ex ⊆ X"
    "unique_on_cylinder t0 (cball t0 et) x0 ex f B L"
proof -
  have "∀⇩F e::real in at_right 0. 0 < e"
    by (auto simp: eventually_at_filter)
  moreover

  from open_Times[OF open_domain] have "open (T × X)" .
  from at_within_open[OF _ this] iv_defined
  have "isCont (λ(t, x). f t x) (t0, x0)"
    using continuous by (auto simp: continuous_on_eq_continuous_within)
  from eventually_bound_pairE[OF this]
  obtain B where B:
    "1 ≤ B" "∀⇩F e in at_right 0. ∀t∈cball t0 e. ∀x∈cball x0 e. norm (f t x) ≤ B"
    by force
  note B(2)
  moreover

  define t where "t ≡ inverse B"
  have te: "⋀e. e > 0 ⟹ t * e > 0"
    using ‹1 ≤ B› by (auto simp: t_def field_simps)
  have t_pos: "t > 0"
    using ‹1 ≤ B› by (auto simp: t_def)

  from B(2) obtain dB where "0 < dB" "0 < dB / 2"
    and dB: "⋀d t x. 0 < d ⟹ d < dB ⟹ t∈cball t0 d ⟹ x∈cball x0 d ⟹
      norm (f t x) ≤ B"
    by (auto simp: eventually_at dist_real_def Ball_def)

  hence dB': "⋀t x. (t, x) ∈ cball (t0, x0) (dB / 2) ⟹ norm (f t x) ≤ B"
    using cball_Pair_split_subset[of t0 x0 "dB / 2"]
    by (auto simp: eventually_at dist_real_def
      simp del: mem_cball
      intro!: dB[where d="dB/2"])
  from eventually_in_cballs[OF ‹0 < dB/2› t_pos, of t0 x0]
  have "∀⇩F e in at_right 0. ∀t∈cball t0 (t * e). ∀x∈cball x0 e. norm (f t x) ≤ B"
    unfolding eventually_at_filter
    by eventually_elim (auto intro!: dB')
  moreover

  from eventually_lipschitz[OF iv_defined t_pos] obtain L where
    "∀⇩F u in at_right 0. ∀t'∈cball t0 (t * u) ∩ T. L-lipschitz_on (cball x0 u ∩ X) (f t')"
    by auto
  moreover
  have "∀⇩F e in at_right 0. cball t0 (t * e) ⊆ T"
    using eventually_open_cball[OF open_domain(1) iv_defined(1)]
    by (subst eventually_filtermap[symmetric, where f="λx. t * x"])
      (simp add: filtermap_times_pos_at_right t_pos)
  moreover
  have "eventually (λe. cball x0 e ⊆ X) (at_right 0)"
    using open_domain(2) iv_defined(2)
    by (rule eventually_open_cball)
  ultimately have "∀⇩F e in at_right 0. 0 < e ∧ cball t0 (t * e) ⊆ T ∧ cball x0 e ⊆ X ∧
    unique_on_cylinder t0 (cball t0 (t * e)) x0 e f B L"
  proof eventually_elim
    case (elim e)
    note ‹0 < e›
    moreover
    note T = ‹cball t0 (t * e) ⊆ T›
    moreover
    note X = ‹cball x0 e ⊆ X›
    moreover
    from elim Int_absorb2[OF ‹cball x0 e ⊆ X›]
    have L: "t' ∈ cball t0 (t * e) ∩ T ⟹ L-lipschitz_on (cball x0 e) (f t')" for t'
      by auto
    from elim have B: "⋀t' x. t' ∈ cball t0 (t * e) ⟹ x ∈ cball x0 e ⟹ norm (f t' x) ≤ B"
      by auto


    have "t * e ≤ e / B"
      by (auto simp: t_def cball_def dist_real_def inverse_eq_divide)

    have "{t0 -- t0 + t * e} ⊆ cball t0 (t * e)"
      using ‹t > 0› ‹e > 0›
      by (auto simp: cball_eq_closed_segment_real closed_segment_eq_real_ivl)
    then have "unique_on_cylinder t0 (cball t0 (t * e)) x0 e f B L"
      using T X ‹t > 0› ‹e > 0› ‹t * e ≤ e / B›
      by unfold_locales
        (auto intro!: continuous_rhs_comp continuous_on_fst continuous_on_snd B L
          continuous_on_id
          simp: split_beta' dist_commute mem_cball)
    ultimately show ?case by auto
  qed
  from eventually_happens[OF this]
  obtain e where "0 < e" "cball t0 (t * e) ⊆ T" "cball x0 e ⊆ X"
    "unique_on_cylinder t0 (cball t0 (t * e)) x0 e f B L"
    by (metis trivial_limit_at_right_real)
  with mult_pos_pos[OF ‹0 < t› ‹0 < e›] show ?thesis ..
qed

lemma mem_existence_ivl_iv_defined:
  assumes "t ∈ existence_ivl t0 x0"
  shows "t0 ∈ T" "x0 ∈ X"
  using assms existence_ivl_empty_iff
  unfolding atomize_conj
  by blast

lemma csol_mem_csols:
  assumes "t ∈ existence_ivl t0 x0"
  shows "(csol t0 x0 t, t) ∈ csols t0 x0"
proof -
  have "∃csol. ∀t ∈ existence_ivl t0 x0. (csol t, t) ∈ csols t0 x0"
  proof (safe intro!: bchoice)
    fix t assume "t ∈ existence_ivl t0 x0"
    then obtain csol t1 where csol: "(csol t, t1) ∈ csols t0 x0" "t ∈ {t0 -- t1}"
      by (auto simp: existence_ivl_def)
    then have "{t0--t} ⊆ {t0 -- t1}"
      by (auto simp: closed_segment_eq_real_ivl)
    then have "(csol t, t) ∈ csols t0 x0" using csol
      by (auto simp: csols_def intro: solves_ode_on_subset)
    then show "∃y. (y, t) ∈ csols t0 x0" by force
  qed
  then have "∀t ∈ existence_ivl t0 x0. (csol t0 x0 t, t) ∈ csols t0 x0"
    unfolding csol_def
    by (rule someI_ex)
  with assms show "?thesis" by auto
qed

lemma csol:
  assumes "t ∈ existence_ivl t0 x0"
  shows "t ∈ T" "{t0--t} ⊆ T" "csol t0 x0 t t0 = x0" "(csol t0 x0 t solves_ode f) {t0--t} X"
  using csol_mem_csols[OF assms]
  by (auto simp: csols_def)

lemma existence_ivl_initial_time_iff[simp]: "t0 ∈ existence_ivl t0 x0 ⟷ t0 ∈ T ∧ x0 ∈ X"
  using csols_empty_iff
  by (auto simp: existence_ivl_def)

lemma existence_ivl_initial_time: "t0 ∈ T ⟹ x0 ∈ X ⟹ t0 ∈ existence_ivl t0 x0"
  by simp

lemmas mem_existence_ivl_subset = csol(1)

lemma existence_ivl_subset:
  "existence_ivl t0 x0 ⊆ T"
  using mem_existence_ivl_subset by blast

lemma is_interval_existence_ivl[intro, simp]: "is_interval (existence_ivl t0 x0)"
  unfolding is_interval_connected_1
  by (auto simp: existence_ivl_def intro!: connected_Union)

lemma connected_existence_ivl[intro, simp]: "connected (existence_ivl t0 x0)"
  using is_interval_connected by blast

lemma in_existence_between_zeroI:
  "t ∈ existence_ivl t0 x0 ⟹ s ∈ {t0 -- t} ⟹ s ∈ existence_ivl t0 x0"
  by (meson existence_ivl_initial_time interval.closed_segment_subset_domainI interval.intro
    is_interval_existence_ivl mem_existence_ivl_iv_defined(1) mem_existence_ivl_iv_defined(2))

lemma segment_subset_existence_ivl:
  assumes "s ∈ existence_ivl t0 x0" "t ∈ existence_ivl t0 x0"
  shows "{s -- t} ⊆ existence_ivl t0 x0"
  using assms is_interval_existence_ivl
  unfolding is_interval_convex_1
  by (rule closed_segment_subset)

lemma flow_initial_time_if: "flow t0 x0 t0 = (if t0 ∈ T ∧ x0 ∈ X then x0 else 0)"
  by (simp add: flow_def csol(3))

lemma flow_initial_time[simp]: "t0 ∈ T ⟹ x0 ∈ X ⟹ flow t0 x0 t0 = x0"
  by (auto simp: flow_initial_time_if)

lemma open_existence_ivl[intro, simp]: "open (existence_ivl t0 x0)"
proof (rule openI)
  fix t assume t: "t ∈ existence_ivl t0 x0"
  note csol = csol[OF this]
  note mem_existence_ivl_iv_defined[OF t]

  have "flow t0 x0 t ∈ X" using ‹t ∈ existence_ivl t0 x0›
    using csol(4) solves_ode_domainD
    by (force simp add: flow_def)

  from ll_on_open_it.local_unique_solution[OF ll_on_open_it_axioms ‹t ∈ T› this]
  obtain et ex B L where lsol:
    "0 < et"
    "0 < ex"
    "cball t et ⊆ T"
    "cball (flow t0 x0 t) ex ⊆ X"
    "unique_on_cylinder t (cball t et) (flow t0 x0 t) ex f B L"
    by metis
  then interpret unique_on_cylinder t "cball t et" "flow t0 x0 t" ex "cball (flow t0 x0 t) ex" f B L
    by auto
  from solution_usolves_ode have lsol_ode: "(solution solves_ode f) (cball t et) (cball (flow t0 x0 t) ex)"
    by (intro usolves_odeD)
  show "∃e>0. ball t e ⊆ existence_ivl t0 x0"
  proof cases
    assume "t = t0"
    show ?thesis
    proof (safe intro!: exI[where x="et"] mult_pos_pos ‹0 < et› ‹0 < ex›)
      fix t' assume "t' ∈ ball t et"
      then have subset: "{t0--t'} ⊆ ball t et"
        by (intro closed_segment_subset) (auto simp: ‹0 < et› ‹0 < ex› ‹t = t0›)
      also have "… ⊆ cball t et" by simp
      also note ‹cball t _ ⊆ T›
      finally have "{t0--t'} ⊆ T" by simp
      moreover have "(solution solves_ode f) {t0--t'} X"
        using lsol_ode
        apply (rule solves_ode_on_subset)
        using subset lsol
        by (auto simp: mem_ball mem_cball)
      ultimately have "(solution, t') ∈ csols t0 x0"
        unfolding csols_def
        using lsol ‹t' ∈ ball _ _› lsol ‹t = t0› solution_iv ‹x0 ∈ X›
        by (auto simp: csols_def)
      then show "t' ∈ existence_ivl t0 x0"
        unfolding existence_ivl_def
        by force
    qed
  next
    assume "t ≠ t0"
    let ?m = "min et (dist t0 t / 2)"
    show ?thesis
    proof (safe intro!: exI[where x = ?m])
      let ?t1' = "if t0 ≤ t then t + et else t - et"
      have lsol_ode: "(solution solves_ode f) {t -- ?t1'} (cball (flow t0 x0 t) ex)"
        by (rule solves_ode_on_subset[OF lsol_ode])
          (insert ‹0 < et› ‹0 < ex›, auto simp: mem_cball closed_segment_eq_real_ivl dist_real_def)
      let ?if = "λta. if ta ∈ {t0--t} then csol t0 x0 t ta else solution ta"
      let ?iff = "λta. if ta ∈ {t0--t} then f ta else f ta"
      have "(?if solves_ode ?iff) ({t0--t} ∪ {t -- ?t1'}) X"
        apply (rule connection_solves_ode[OF csol(4) lsol_ode, unfolded Un_absorb2[OF ‹_ ⊆ X›]])
        using lsol solution_iv ‹t ∈ existence_ivl t0 x0›
        by (auto intro!: simp: closed_segment_eq_real_ivl flow_def split: if_split_asm)
      also have "?iff = f" by auto
      also have Un_eq: "{t0--t} ∪ {t -- ?t1'} = {t0 -- ?t1'}"
        using ‹0 < et› ‹0 < ex›
        by (auto simp: closed_segment_eq_real_ivl)
      finally have continuation: "(?if solves_ode f) {t0--?t1'} X" .
      have subset_T: "{t0 -- ?t1'} ⊆ T"
        unfolding Un_eq[symmetric]
        apply (intro Un_least)
        subgoal using csol by force
        subgoal using _ lsol(3)
          apply (rule order_trans)
          using ‹0 < et› ‹0 < ex›
          by (auto simp: closed_segment_eq_real_ivl subset_iff mem_cball dist_real_def)
        done
      fix t' assume "t' ∈ ball t ?m"
      then have scs: "{t0 -- t'} ⊆ {t0--?t1'}"
        using ‹0 < et› ‹0 < ex›
        by (auto simp: closed_segment_eq_real_ivl dist_real_def abs_real_def mem_ball split: if_split_asm)
      with continuation have "(?if solves_ode f) {t0 -- t'} X"
        by (rule solves_ode_on_subset) simp
      then have "(?if, t') ∈ csols t0 x0"
        using lsol ‹t' ∈ ball _ _› csol scs subset_T
        by (auto simp: csols_def subset_iff)
      then show "t' ∈ existence_ivl t0 x0"
        unfolding existence_ivl_def
        by force
    qed (insert ‹t ≠ t0› ‹0 < et› ‹0 < ex›, simp)
  qed
qed

lemma csols_unique:
  assumes "(x, t1) ∈ csols t0 x0"
  assumes "(y, t2) ∈ csols t0 x0"
  shows "∀t ∈ {t0 -- t1} ∩ {t0 -- t2}. x t = y t"
proof (rule ccontr)
  let ?S = "{t0 -- t1} ∩ {t0 -- t2}"
  let ?Z0 = "(λt. x t - y t) -` {0} ∩ ?S"
  let ?Z = "connected_component_set ?Z0 t0"
  from assms have t1: "t1 ∈ existence_ivl t0 x0" and t2: "t2 ∈ existence_ivl t0 x0"
    and x: "(x solves_ode f) {t0 -- t1} X"
    and y: "(y solves_ode f) {t0 -- t2} X"
    and sub1: "{t0--t1} ⊆ T"
    and sub2: "{t0--t2} ⊆ T"
    and x0: "x t0 = x0"
    and y0: "y t0 = x0"
    by (auto simp: existence_ivl_def csols_def)

  assume "¬ (∀t∈?S. x t = y t)"
  hence "∃t∈?S. x t ≠ y t" by simp
  then obtain t_ne where t_ne: "t_ne ∈ ?S" "x t_ne ≠ y t_ne" ..
  from assms have x: "(x solves_ode f) {t0--t1} X"
    and y:"(y solves_ode f) {t0--t2} X"
    by (auto simp: csols_def)
  have "compact ?S"
    by auto
  have "closed ?Z"
    by (intro closed_connected_component closed_vimage_Int)
      (auto intro!: continuous_intros continuous_on_subset[OF solves_ode_continuous_on[OF x]]
        continuous_on_subset[OF solves_ode_continuous_on[OF y]])
  moreover
  have "t0 ∈ ?Z" using assms
    by (auto simp: csols_def)
  then have "?Z ≠ {}"
    by (auto intro!: exI[where x=t0])
  ultimately
  obtain t_max where max: "t_max ∈ ?Z" "y ∈ ?Z ⟹ dist t_ne t_max ≤ dist t_ne y" for y
    by (blast intro: distance_attains_inf)
  have max_equal_flows: "x t = y t" if "t ∈ {t0 -- t_max}" for t
    using max(1) that
    by (auto simp: connected_component_def vimage_def subset_iff closed_segment_eq_real_ivl
      split: if_split_asm) (metis connected_iff_interval)+
  then have t_ne_outside: "t_ne ∉ {t0 -- t_max}" using t_ne by auto

  have "x t_max = y t_max"
    by (rule max_equal_flows) simp
  have "t_max ∈ ?S" "t_max ∈ T"
    using max sub1 sub2
    by (auto simp: connected_component_def)
  with solves_odeD[OF x]
  have "x t_max ∈ X"
    by auto

  from ll_on_open_it.local_unique_solution[OF ll_on_open_it_axioms ‹t_max ∈ T› ‹x t_max ∈ X›]
  obtain et ex B L
    where "0 < et" "0 < ex"
      and "cball t_max et ⊆ T" "cball (x t_max) ex ⊆ X"
      and "unique_on_cylinder t_max (cball t_max et) (x t_max) ex f B L"
    by metis
  then interpret unique_on_cylinder t_max "cball t_max et" "x t_max" ex "cball (x t_max) ex" f B L
    by auto

  from usolves_ode_on_superset_domain[OF solution_usolves_ode solution_iv ‹cball _ _ ⊆ X›]
  have solution_usolves_on_X: "(solution usolves_ode f from t_max) (cball t_max et) X" by simp

  have ge_imps: "t0 ≤ t1" "t0 ≤ t2" "t0 ≤ t_max" "t_max < t_ne" if "t0 ≤ t_ne"
    using that t_ne_outside ‹0 < et› ‹0 < ex› max(1) ‹t_max ∈ ?S› ‹t_max ∈ T› t_ne x0 y0
    by (auto simp: min_def dist_real_def max_def closed_segment_eq_real_ivl split: if_split_asm)
  have le_imps: "t0 ≥ t1" "t0 ≥ t2" "t0 ≥ t_max" "t_max > t_ne" if "t0 ≥ t_ne"
    using that t_ne_outside ‹0 < et› ‹0 < ex› max(1) ‹t_max ∈ ?S› ‹t_max ∈ T› t_ne x0 y0
    by (auto simp: min_def dist_real_def max_def closed_segment_eq_real_ivl split: if_split_asm)

  define tt where "tt ≡ if t0 ≤ t_ne then min (t_max + et) t_ne else max (t_max - et) t_ne"
  have "tt ∈ cball t_max et" "tt ∈ {t0 -- t1}" "tt ∈ {t0 -- t2}"
    using ge_imps le_imps ‹0 < et› t_ne(1)
    by (auto simp: mem_cball closed_segment_eq_real_ivl tt_def dist_real_def abs_real_def min_def max_def not_less)

  have segment_unsplit: "{t0 -- t_max} ∪ {t_max -- tt} = {t0 -- tt}"
    using ge_imps le_imps ‹0 < et›
    by (auto simp: tt_def closed_segment_eq_real_ivl min_def max_def split: if_split_asm) arith

  have "tt ∈ {t0 -- t1}"
    using ge_imps le_imps ‹0 < et› t_ne(1)
    by (auto simp: tt_def closed_segment_eq_real_ivl min_def max_def split: if_split_asm)

  have "tt ∈ ?Z"
  proof (safe intro!: connected_componentI[where T = "{t0 -- t_max} ∪ {t_max -- tt}"])
    fix s assume s: "s ∈ {t_max -- tt}"
    have "{t_max--s} ⊆ {t_max -- tt}"
      by (rule closed_segment_subset) (auto simp: s)
    also have "… ⊆ cball t_max et"
      using ‹tt ∈ cball t_max et› ‹0 < et›
      by (intro closed_segment_subset) auto
    finally have subset: "{t_max--s} ⊆ cball t_max et" .
    from s show "s ∈ {t0--t1}" "s ∈ {t0--t2}"
      using ge_imps le_imps t_ne ‹0 < et›
      by (auto simp: tt_def min_def max_def closed_segment_eq_real_ivl split: if_split_asm)
    have ivl: "t_max ∈ {t_max -- s}" "is_interval {t_max--s}"
      using ‹tt ∈ cball t_max et› ‹0 < et› s
      by (simp_all add: is_interval_convex_1)
    {
      note ivl subset
      moreover
      have "{t_max--s} ⊆ {t0--t1}"
        using ‹s ∈ {t0 -- t1}› ‹t_max ∈ ?S›
        by (simp add: closed_segment_subset)
      from x this order_refl have "(x solves_ode f) {t_max--s} X"
        by (rule solves_ode_on_subset)
      moreover note solution_iv[symmetric]
      ultimately
      have "x s = solution s"
        by (rule usolves_odeD(4)[OF solution_usolves_on_X]) simp
    } moreover {
      note ivl subset
      moreover
      have "{t_max--s} ⊆ {t0--t2}"
        using ‹s ∈ {t0 -- t2}› ‹t_max ∈ ?S›
        by (simp add: closed_segment_subset)
      from y this order_refl have "(y solves_ode f) {t_max--s} X"
        by (rule solves_ode_on_subset)
      moreover from solution_iv[symmetric] have "y t_max = solution t_max"
        by (simp add: ‹x t_max = y t_max›)
      ultimately
      have "y s = solution s"
        by (rule usolves_odeD[OF solution_usolves_on_X]) simp
    } ultimately show "s ∈ (λt. x t - y t) -` {0}" by simp
  next
    fix s assume s: "s ∈ {t0 -- t_max}"
    then show "s ∈ (λt. x t - y t) -` {0}"
      by (auto intro!: max_equal_flows)
    show "s ∈ {t0--t1}" "s ∈ {t0--t2}"
      by (metis Int_iff ‹t_max ∈ ?S› closed_segment_closed_segment_subset ends_in_segment(1) s)+
  qed (auto simp: segment_unsplit)
  then have "dist t_ne t_max ≤ dist t_ne tt"
    by (rule max)
  moreover have "dist t_ne t_max > dist t_ne tt"
    using le_imps ge_imps ‹0 < et›
    by (auto simp: tt_def dist_real_def)
  ultimately show False by simp
qed

lemma csol_unique:
  assumes t1: "t1 ∈ existence_ivl t0 x0"
  assumes t2: "t2 ∈ existence_ivl t0 x0"
  assumes t: "t ∈ {t0 -- t1}" "t ∈ {t0 -- t2}"
  shows "csol t0 x0 t1 t = csol t0 x0 t2 t"
  using csols_unique[OF csol_mem_csols[OF t1] csol_mem_csols[OF t2]] t
  by simp

lemma flow_vderiv_on_left:
  "(flow t0 x0 has_vderiv_on (λx. f x (flow t0 x0 x))) (existence_ivl t0 x0 ∩ {..t0})"
  unfolding has_vderiv_on_def
proof safe
  fix t
  assume t: "t ∈ existence_ivl t0 x0" "t ≤ t0"
  with open_existence_ivl
  obtain e where "e > 0" and e: "⋀s. s ∈ cball t e ⟹ s ∈ existence_ivl t0 x0"
    by (force simp: open_contains_cball)
  have csol_eq: "csol t0 x0 (t - e) s = flow t0 x0 s" if "t - e ≤ s" "s ≤ t0" for s
    unfolding flow_def
    using that ‹0 < e› t e
    by (auto simp: cball_def dist_real_def abs_real_def closed_segment_eq_real_ivl subset_iff
      intro!: csol_unique in_existence_between_zeroI[of "t - e" x0 s]
      split: if_split_asm)
  from e[of "t - e"] ‹0 < e› have "t - e ∈ existence_ivl t0 x0" by (auto simp: mem_cball)

  let ?l = "existence_ivl t0 x0 ∩ {..t0}"
  let ?s = "{t0 -- t - e}"

  from csol(4)[OF e[of "t - e"]] ‹0 < e›
  have 1: "(csol t0 x0 (t - e) solves_ode f) ?s X"
    by (auto simp: mem_cball)
  have "t ∈ {t0 -- t - e}" using t ‹0 < e› by (auto simp: closed_segment_eq_real_ivl)
  from solves_odeD(1)[OF 1, unfolded has_vderiv_on_def, rule_format, OF this]
  have "(csol t0 x0 (t - e) has_vector_derivative f t (csol t0 x0 (t - e) t)) (at t within ?s)" .
  also have "at t within ?s = (at t within ?l)"
    using t ‹0 < e›
    by (intro at_within_nhd[where S="{t - e <..< t0 + 1}"])
      (auto simp: closed_segment_eq_real_ivl intro!: in_existence_between_zeroI[OF ‹t - e ∈ existence_ivl t0 x0›])
  finally
  have "(csol t0 x0 (t - e) has_vector_derivative f t (csol t0 x0 (t - e) t)) (at t within existence_ivl t0 x0 ∩ {..t0})" .
  also have "csol t0 x0 (t - e) t = flow t0 x0 t"
    using ‹0 < e› ‹t ≤ t0› by (auto intro!: csol_eq)
  finally
  show "(flow t0 x0 has_vector_derivative f t (flow t0 x0 t)) (at t within existence_ivl t0 x0 ∩ {..t0})"
    apply (rule has_vector_derivative_transform_within[where d=e])
    using t ‹0 < e›
    by (auto intro!: csol_eq simp: dist_real_def)
qed

lemma flow_vderiv_on_right:
  "(flow t0 x0 has_vderiv_on (λx. f x (flow t0 x0 x))) (existence_ivl t0 x0 ∩ {t0..})"
  unfolding has_vderiv_on_def
proof safe
  fix t
  assume t: "t ∈ existence_ivl t0 x0" "t0 ≤ t"
  with open_existence_ivl
  obtain e where "e > 0" and e: "⋀s. s ∈ cball t e ⟹ s ∈ existence_ivl t0 x0"
    by (force simp: open_contains_cball)
  have csol_eq: "csol t0 x0 (t + e) s = flow t0 x0 s" if "s ≤ t + e" "t0 ≤ s" for s
    unfolding flow_def
    using e that ‹0 < e›
    by (auto simp: cball_def dist_real_def abs_real_def closed_segment_eq_real_ivl subset_iff
      intro!: csol_unique in_existence_between_zeroI[of "t + e" x0 s]
      split: if_split_asm)
  from e[of "t + e"] ‹0 < e› have "t + e ∈ existence_ivl t0 x0" by (auto simp: mem_cball dist_real_def)

  let ?l = "existence_ivl t0 x0 ∩ {t0..}"
  let ?s = "{t0 -- t + e}"

  from csol(4)[OF e[of "t + e"]] ‹0 < e›
  have 1: "(csol t0 x0 (t + e) solves_ode f) ?s X"
    by (auto simp: dist_real_def mem_cball)
  have "t ∈ {t0 -- t + e}" using t ‹0 < e› by (auto simp: closed_segment_eq_real_ivl)
  from solves_odeD(1)[OF 1, unfolded has_vderiv_on_def, rule_format, OF this]
  have "(csol t0 x0 (t + e) has_vector_derivative f t (csol t0 x0 (t + e) t)) (at t within ?s)" .
  also have "at t within ?s = (at t within ?l)"
    using t ‹0 < e›
    by (intro at_within_nhd[where S="{t0 - 1 <..< t + e}"])
      (auto simp: closed_segment_eq_real_ivl intro!: in_existence_between_zeroI[OF ‹t + e ∈ existence_ivl t0 x0›])
  finally
  have "(csol t0 x0 (t + e) has_vector_derivative f t (csol t0 x0 (t + e) t)) (at t within ?l)" .
  also have "csol t0 x0 (t + e) t = flow t0 x0 t"
    using ‹0 < e› ‹t0 ≤ t› by (auto intro!: csol_eq)
  finally
  show "(flow t0 x0 has_vector_derivative f t (flow t0 x0 t)) (at t within ?l)"
    apply (rule has_vector_derivative_transform_within[where d=e])
    using t ‹0 < e›
    by (auto intro!: csol_eq simp: dist_real_def)
qed

lemma flow_usolves_ode:
  assumes iv_defined: "t0 ∈ T" "x0 ∈ X"
  shows "(flow t0 x0 usolves_ode f from t0) (existence_ivl t0 x0) X"
proof (rule usolves_odeI)
  let ?l = "existence_ivl t0 x0 ∩ {..t0}" and ?r = "existence_ivl t0 x0 ∩ {t0..}"
  let ?split = "?l ∪ ?r"
  have insert_idem: "insert t0 ?l = ?l" "insert t0 ?r = ?r" using iv_defined
    by auto
  from existence_ivl_initial_time have cl_inter: "closure ?l ∩ closure ?r = {t0}"
  proof safe
    from iv_defined have "t0 ∈ ?l" by simp also note closure_subset finally show "t0 ∈ closure ?l" .
    from iv_defined have "t0 ∈ ?r" by simp also note closure_subset finally show "t0 ∈ closure ?r" .
    fix x
    assume xl: "x ∈ closure ?l"
    assume "x ∈ closure ?r"
    also have "closure ?r ⊆ closure {t0..}"
      by (rule closure_mono) simp
    finally have "t0 ≤ x" by simp
    moreover
    {
      note xl
      also have cl: "closure ?l ⊆ closure {..t0}"
        by (rule closure_mono) simp
      finally have "x ≤ t0" by simp
    } ultimately show "x = t0" by simp
  qed
  have "(flow t0 x0 has_vderiv_on (λt. f t (flow t0 x0 t))) ?split"
    by (rule has_vderiv_on_union)
      (auto simp: cl_inter insert_idem flow_vderiv_on_right flow_vderiv_on_left)
  also have "?split = existence_ivl t0 x0"
    by auto
  finally have "(flow t0 x0 has_vderiv_on (λt. f t (flow t0 x0 t))) (existence_ivl t0 x0)" .
  moreover
  have "flow t0 x0 t ∈ X" if "t ∈ existence_ivl t0 x0" for t
    using solves_odeD(2)[OF csol(4)[OF that]] that
    by (simp add: flow_def)
  ultimately show "(flow t0 x0 solves_ode f) (existence_ivl t0 x0) X"
    by (rule solves_odeI)
  show "t0 ∈ existence_ivl t0 x0" using iv_defined by simp
  show "is_interval (existence_ivl t0 x0)" by (simp add: is_interval_existence_ivl)
  fix z t
  assume z: "{t0 -- t} ⊆ existence_ivl t0 x0" "(z solves_ode f) {t0 -- t} X" "z t0 = flow t0 x0 t0"
  then have "t ∈ existence_ivl t0 x0" by auto
  moreover
  from csol[OF this] z have "(z, t) ∈ csols t0 x0" by (auto simp: csols_def)
  moreover have "(csol t0 x0 t, t) ∈ csols t0 x0"
    by (rule csol_mem_csols) fact
  ultimately
  show "z t = flow t0 x0 t"
    unfolding flow_def
    by (auto intro: csols_unique[rule_format])
qed

lemma flow_solves_ode: "t0 ∈ T ⟹ x0 ∈ X ⟹ (flow t0 x0 solves_ode f) (existence_ivl t0 x0) X"
  by (rule usolves_odeD[OF flow_usolves_ode])

lemma equals_flowI:
  assumes "t0 ∈ T'"
    "is_interval T'"
    "T' ⊆ existence_ivl t0 x0"
    "(z solves_ode f) T' X"
    "z t0 = flow t0 x0 t0" "t ∈ T'"
  shows "z t = flow t0 x0 t"
proof -
  from assms have iv_defined: "t0 ∈ T" "x0 ∈ X"
    unfolding atomize_conj
    using assms existence_ivl_subset mem_existence_ivl_iv_defined
    by blast
  show ?thesis
    using assms
    by (rule usolves_odeD[OF flow_usolves_ode[OF iv_defined]])
qed

lemma existence_ivl_maximal_segment:
  assumes "(x solves_ode f) {t0 -- t} X" "x t0 = x0"
  assumes "{t0 -- t} ⊆ T"
  shows "t ∈ existence_ivl t0 x0"
  using assms
  by (auto simp: existence_ivl_def csols_def)

lemma existence_ivl_maximal_interval:
  assumes "(x solves_ode f) S X" "x t0 = x0"
  assumes "t0 ∈ S" "is_interval S" "S ⊆ T"
  shows "S ⊆ existence_ivl t0 x0"
proof
  fix t assume "t ∈ S"
  with assms have subset1: "{t0--t} ⊆ S"
    by (intro closed_segment_subset) (auto simp: is_interval_convex_1)
  with ‹S ⊆ T› have subset2: "{t0 -- t} ⊆ T" by auto
  have "(x solves_ode f) {t0 -- t} X"
    using assms(1) subset1 order_refl
    by (rule solves_ode_on_subset)
  from this ‹x t0 = x0› subset2 show "t ∈ existence_ivl t0 x0"
    by (rule existence_ivl_maximal_segment)
qed

lemma maximal_existence_flow:
  assumes sol: "(x solves_ode f) K X" and iv: "x t0 = x0"
  assumes "is_interval K"
  assumes "t0 ∈ K"
  assumes "K ⊆ T"
  shows "K ⊆ existence_ivl t0 x0" "⋀t. t ∈ K ⟹ flow t0 x0 t = x t"
proof -
  from assms have iv_defined: "t0 ∈ T" "x0 ∈ X"
    unfolding atomize_conj
    using solves_ode_domainD by blast
  show exivl: "K ⊆ existence_ivl t0 x0"
    by (rule existence_ivl_maximal_interval; rule assms)
  show "flow t0 x0 t = x t" if "t ∈ K" for t
    apply (rule sym)
    apply (rule equals_flowI[OF ‹t0 ∈ K› ‹is_interval K› exivl sol _ that])
    by (simp add: iv iv_defined)
qed

lemma maximal_existence_flowI:
  assumes "(x has_vderiv_on (λt. f t (x t))) K"
  assumes "⋀t. t ∈ K ⟹ x t ∈ X"
  assumes "x t0 = x0"
  assumes K: "is_interval K" "t0 ∈ K" "K ⊆ T"
  shows "K ⊆ existence_ivl t0 x0" "⋀t. t ∈ K ⟹ flow t0 x0 t = x t"
proof -
  from assms(1,2) have sol: "(x solves_ode f) K X" by (rule solves_odeI)
  from maximal_existence_flow[OF sol assms(3) K]
  show "K ⊆ existence_ivl t0 x0" "⋀t. t ∈ K ⟹ flow t0 x0 t = x t"
    by auto
qed

lemma flow_in_domain: "t ∈ existence_ivl t0 x0 ⟹ flow t0 x0 t ∈ X"
  using flow_solves_ode solves_ode_domainD local.mem_existence_ivl_iv_defined
  by blast

lemma (in ll_on_open)
  assumes "t ∈ existence_ivl s x"
  assumes "x ∈ X"
  assumes auto: "⋀s t x. x ∈ X ⟹ f s x = f t x"
  assumes "T = UNIV"
  shows mem_existence_ivl_shift_autonomous1: "t - s ∈ existence_ivl 0 x"
    and flow_shift_autonomous1: "flow s x t = flow 0 x (t - s)"
proof -
  have na: "s ∈ T" "x ∈ X" and a: "0 ∈ T" "x ∈ X"
    by (auto simp: assms)

  have tI[simp]: "t ∈ T" for t by (simp add: assms)
  let ?T = "((+) (- s) ` existence_ivl s x)"
  have shifted: "is_interval ?T" "0 ∈ ?T"
    by (auto simp: ‹x ∈ X›)

  have "(λt. t - s) = (+) (- s)" by auto
  with shift_autonomous_solution[OF flow_solves_ode[OF na], of s] flow_in_domain
  have sol: "((λt. flow s x (t + s)) solves_ode f) ?T X"
    by (auto simp: auto ‹x ∈ X›)

  have "flow s x (0 + s) = x" using ‹x ∈ X› flow_initial_time by simp
  from maximal_existence_flow[OF sol this shifted]
  have *: "?T ⊆ existence_ivl 0 x"
    and **: "⋀t. t ∈ ?T ⟹ flow 0 x t = flow s x (t + s)"
    by (auto simp: subset_iff)

  have "t - s ∈ ?T"
    using ‹t ∈ existence_ivl s x›
    by auto
  also note *
  finally show "t - s ∈ existence_ivl 0 x" .

  show "flow s x t = flow 0 x (t - s)"
    using ‹t ∈ existence_ivl s x›
    by (auto simp: **)
qed

lemma (in ll_on_open)
  assumes "t - s ∈ existence_ivl 0 x"
  assumes "x ∈ X"
  assumes auto: "⋀s t x. x ∈ X ⟹ f s x = f t x"
  assumes "T = UNIV"
  shows mem_existence_ivl_shift_autonomous2: "t ∈ existence_ivl s x"
    and flow_shift_autonomous2: "flow s x t = flow 0 x (t - s)"
proof -
  have na: "s ∈ T" "x ∈ X" and a: "0 ∈ T" "x ∈ X"
    by (auto simp: assms)

  let ?T = "((+) s ` existence_ivl 0 x)"
  have shifted: "is_interval ?T" "s ∈ ?T"
    by (auto simp: a)

  have "(λt. t + s) = (+) s"
    by auto
  with shift_autonomous_solution[OF flow_solves_ode[OF a], of "-s"]
    flow_in_domain
  have sol: "((λt. flow 0 x (t - s)) solves_ode f) ?T X"
    by (auto simp: auto algebra_simps)

  have "flow 0 x (s - s) = x"
    by (auto simp: a)
  from maximal_existence_flow[OF sol this shifted]
  have *: "?T ⊆ existence_ivl s x"
    and **: "⋀t. t ∈ ?T ⟹ flow s x t = flow 0 x (t - s)"
    by (auto simp: subset_iff assms)

  have "t ∈ ?T"
    using ‹t - s ∈ existence_ivl 0 x›
    by force
  also note *
  finally show "t ∈ existence_ivl s x" .

  show "flow s x t = flow 0 x (t - s)"
    using ‹t - s ∈ existence_ivl _ _›
    by (subst **; force)
qed

lemma
  flow_eq_rev:
  assumes "t ∈ existence_ivl t0 x0"
  shows "preflect t0 t ∈ ll_on_open.existence_ivl (preflect t0 ` T) (λt. - f (preflect t0 t)) X t0 x0"
    "flow t0 x0 t = ll_on_open.flow (preflect t0 ` T) (λt. - f (preflect t0 t)) X t0 x0 (preflect t0 t)"
proof -
  from mem_existence_ivl_iv_defined[OF assms] have mt0: "t0 ∈ preflect t0 ` existence_ivl t0 x0"
    by (auto simp: preflect_def)
  have subset: "preflect t0 ` existence_ivl t0 x0 ⊆ preflect t0 ` T"
    using existence_ivl_subset
    by (rule image_mono)
  from mt0 subset have "t0 ∈ preflect t0 ` T" by auto

  have sol: "((λt. flow t0 x0 (preflect t0 t)) solves_ode (λt. - f (preflect t0 t))) (preflect t0 ` existence_ivl t0 x0) X"
    using mt0
    by (rule preflect_solution) (auto simp: image_image flow_solves_ode mem_existence_ivl_iv_defined[OF assms])

  have flow0: "flow t0 x0 (preflect t0 t0) = x0" and ivl: "is_interval (preflect t0 ` existence_ivl t0 x0)"
    by (auto simp: preflect_def mem_existence_ivl_iv_defined[OF assms])

  interpret rev: ll_on_open "(preflect t0 ` T)" "(λt. - f (preflect t0 t))" X ..
  from rev.maximal_existence_flow[OF sol flow0 ivl mt0 subset]
  show "preflect t0 t ∈ rev.existence_ivl t0 x0" "flow t0 x0 t = rev.flow t0 x0 (preflect t0 t)"
    using assms by (auto simp: preflect_def)
qed

lemma (in ll_on_open)
  shows rev_flow_eq: "t ∈ ll_on_open.existence_ivl (preflect t0 ` T) (λt. - f (preflect t0 t)) X t0 x0 ⟹
    ll_on_open.flow (preflect t0 ` T) (λt. - f (preflect t0 t)) X t0 x0 t = flow t0 x0 (preflect t0 t)"
  and mem_rev_existence_ivl_eq:
  "t ∈ ll_on_open.existence_ivl (preflect t0 ` T) (λt. - f (preflect t0 t)) X t0 x0 ⟷ preflect t0 t ∈ existence_ivl t0 x0"
proof -
  interpret rev: ll_on_open "(preflect t0 ` T)" "(λt. - f (preflect t0 t))" X ..
  from rev.flow_eq_rev[of _ t0 x0] flow_eq_rev[of "2 * t0 - t" t0 x0]
  show "t ∈ rev.existence_ivl t0 x0 ⟹ rev.flow t0 x0 t = flow t0 x0 (preflect t0 t)"
    "(t ∈ rev.existence_ivl t0 x0) = (preflect t0 t ∈ existence_ivl t0 x0)"
    by (auto simp: preflect_def fun_Compl_def image_image dest: mem_existence_ivl_iv_defined
      rev.mem_existence_ivl_iv_defined)
qed

lemma
  shows rev_existence_ivl_eq: "ll_on_open.existence_ivl (preflect t0 ` T) (λt. - f (preflect t0 t)) X t0 x0 = preflect t0 ` existence_ivl t0 x0"
    and existence_ivl_eq_rev: "existence_ivl t0 x0 = preflect t0 ` ll_on_open.existence_ivl (preflect t0 ` T) (λt. - f (preflect t0 t)) X t0 x0"
  apply safe
  subgoal by (force simp: mem_rev_existence_ivl_eq)
  subgoal by (force simp: mem_rev_existence_ivl_eq)
  subgoal for x by (force intro!: image_eqI[where x="preflect t0 x"] simp: mem_rev_existence_ivl_eq)
  subgoal by (force simp: mem_rev_existence_ivl_eq)
  done

end

end