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 "(iBasis. (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 "...  r2"
    using assms by (simp add: power_divide)
  ultimately
  show "sqrt (iBasis. (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 = (iBasis. 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 = "iBasis. (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. tcball t0 e. xcball 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  tcball t0 d  xcball 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. tcball t0 (t * e). xcball 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