# Theory 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 (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)"

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 ≠ {}"

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)
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"])
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)"

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

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
{
note ivl subset
moreover
have "{t_max--s} ⊆ {t0--t1}"
using ‹s ∈ {t0 -- t1}› ‹t_max ∈ ?S›
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›
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
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])
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
`