# Theory Initial_Value_Problem

section‹Initial Value Problems›
theory Initial_Value_Problem
imports
"../ODE_Auxiliarities"
"../Library/Interval_Integral_HK"
"../Library/Gronwall"
begin

lemma clamp_le[simp]: "x ≤ a ⟹ clamp a b x = a" for x::"'a::ordered_euclidean_space"
by (auto simp: clamp_def eucl_le[where 'a='a] intro!: euclidean_eqI[where 'a='a])

lemma clamp_ge[simp]: "a ≤ b ⟹ b ≤ x ⟹ clamp a b x = b" for x::"'a::ordered_euclidean_space"
by (force simp: clamp_def eucl_le[where 'a='a] not_le not_less  intro!: euclidean_eqI[where 'a='a])

abbreviation cfuncset :: "'a::topological_space set ⇒ 'b::metric_space set ⇒ ('a ⇒⇩C 'b) set"
(infixr "→⇩C" 60)
where "A →⇩C B ≡ PiC A (λ_. B)"

lemma closed_segment_translation_zero: "z ∈ {z + a--z + b} ⟷ 0 ∈ {a -- b}"

lemma closed_segment_subset_interval: "is_interval T ⟹ a ∈ T ⟹ b ∈ T ⟹ closed_segment a b ⊆ T"
by (rule closed_segment_subset) (auto intro!: closed_segment_subset is_interval_convex)

definition half_open_segment::"'a::real_vector ⇒ 'a ⇒ 'a set" ("(1{_--<_})")
where "half_open_segment a b = {a -- b} - {b}"

lemma half_open_segment_real:
fixes a b::real
shows "{a --< b} = (if a ≤ b then {a ..< b} else {b <.. a})"
by (auto simp: half_open_segment_def closed_segment_eq_real_ivl)

lemma closure_half_open_segment:
fixes a b::real
shows "closure {a --< b} = (if a = b then {} else {a -- b})"
unfolding closed_segment_eq_real_ivl if_distrib half_open_segment_real
unfolding if_distribR
by simp

lemma half_open_segment_subset[intro, simp]:
"{t0--<t1} ⊆ {t0 -- t1}"
"x ∈ {t0--<t1} ⟹ x ∈ {t0 -- t1}"
by (auto simp: half_open_segment_def)

lemma half_open_segment_closed_segmentI:
"t ∈ {t0 -- t1} ⟹ t ≠ t1 ⟹ t ∈ {t0 --< t1}"
by (auto simp: half_open_segment_def)

lemma islimpt_half_open_segment:
fixes t0 t1 s::real
assumes "t0 ≠ t1" "s ∈ {t0--t1}"
shows "s islimpt {t0--<t1}"
proof -
have "s islimpt {t0..<t1}" if "t0 ≤ s" "s ≤ t1" for s
proof -
have *: "{t0..<t1} - {s} = {t0..<s} ∪ {s<..<t1}"
using that by auto
show ?thesis
using that ‹t0 ≠ t1› *
by (cases "t0 = s") (auto simp: islimpt_in_closure)
qed
moreover have "s islimpt {t1<..t0}" if "t1 ≤ s" "s ≤ t0" for s
proof -
have *: "{t1<..t0} - {s} = {t1<..<s} ∪ {s<..t0}"
using that by auto
show ?thesis
using that ‹t0 ≠ t1› *
by (cases "t0 = s") (auto simp: islimpt_in_closure)
qed
ultimately show ?thesis using assms
by (auto simp: half_open_segment_real closed_segment_eq_real_ivl)
qed

lemma
mem_half_open_segment_eventually_in_closed_segment:
fixes t::real
assumes "t ∈ {t0--<t1'}"
shows "∀⇩F t1' in at t1' within {t0--<t1'}. t ∈ {t0--t1'}"
unfolding half_open_segment_real
proof (split if_split, safe)
assume le: "t0 ≤ t1'"
with assms have t: "t0 ≤ t" "t < t1'"
by (auto simp: half_open_segment_real)
then have "∀⇩F t1' in at t1' within {t0..<t1'}. t0 ≤ t"
by simp
moreover
from tendsto_ident_at ‹t < t1'›
have "∀⇩F t1' in at t1' within {t0..<t1'}. t < t1'"
by (rule order_tendstoD)
ultimately show "∀⇩F t1' in at t1' within {t0..<t1'}. t ∈ {t0--t1'}"
by eventually_elim (auto simp add: closed_segment_eq_real_ivl)
next
assume le: "¬ t0 ≤ t1'"
with assms have t: "t ≤ t0" "t1' < t"
by (auto simp: half_open_segment_real)
then have "∀⇩F t1' in at t1' within {t1'<..t0}. t ≤ t0"
by simp
moreover
from tendsto_ident_at ‹t1' < t›
have "∀⇩F t1' in at t1' within {t1'<..t0}. t1' < t"
by (rule order_tendstoD)
ultimately show "∀⇩F t1' in at t1' within {t1'<..t0}. t ∈ {t0--t1'}"
by eventually_elim (auto simp add: closed_segment_eq_real_ivl)
qed

lemma closed_segment_half_open_segment_subsetI:
fixes x::real shows "x ∈ {t0--<t1} ⟹ {t0--x} ⊆ {t0--<t1}"
by (auto simp: half_open_segment_real closed_segment_eq_real_ivl split: if_split_asm)

lemma dist_component_le:
fixes x y::"'a::euclidean_space"
assumes "i ∈ Basis"
shows "dist (x ∙ i) (y ∙ i) ≤ dist x y"
using assms
by (auto simp: euclidean_dist_l2[of x y] intro: member_le_L2_set)

lemma sum_inner_Basis_one: "i ∈ Basis ⟹ (∑x∈Basis. x ∙ i) = 1"
by (subst sum.mono_neutral_right[where S="{i}"])
(auto simp: inner_not_same_Basis)

lemma cball_in_cbox:
fixes y::"'a::euclidean_space"
shows "cball y r ⊆ cbox (y - r *⇩R One) (y + r *⇩R One)"
unfolding scaleR_sum_right interval_cbox cbox_def
proof safe
fix x i::'a assume "i ∈ Basis" "x ∈ cball y r"
with dist_component_le[OF ‹i ∈ Basis›, of y x]
have "dist (y ∙ i) (x ∙ i) ≤ r" by (simp add: mem_cball)
thus "(y - sum ((*⇩R) r) Basis) ∙ i ≤ x ∙ i"
"x ∙ i ≤ (y + sum ((*⇩R) r) Basis) ∙ i"
sum_distrib_left[symmetric] sum_inner_Basis_one ‹i∈Basis› dist_real_def)
qed

lemma centered_cbox_in_cball:
shows "cbox (- r *⇩R One) (r *⇩R One::'a::euclidean_space) ⊆
cball 0 (sqrt(DIM('a)) * r)"
proof
fix x::'a
have "norm x ≤ sqrt(DIM('a)) * infnorm x"
by (rule norm_le_infnorm)
also
assume "x ∈ cbox (- r *⇩R One) (r *⇩R One)"
hence "infnorm x ≤ r"
by (auto simp: infnorm_def mem_box intro!: cSup_least)
finally show "x ∈ cball 0 (sqrt(DIM('a)) * r)"
by (auto simp: dist_norm mult_left_mono mem_cball)
qed

subsection ‹Solutions of IVPs \label{sec:solutions}›

definition
solves_ode :: "(real ⇒ 'a::real_normed_vector) ⇒ (real ⇒ 'a ⇒ 'a) ⇒ real set ⇒ 'a set ⇒ bool"
(infix "(solves'_ode)" 50)
where
"(y solves_ode f) T X ⟷ (y has_vderiv_on (λt. f t (y t))) T ∧ y ∈ T → X"

lemma solves_odeI:
assumes solves_ode_vderivD: "(y has_vderiv_on (λt. f t (y t))) T"
and solves_ode_domainD: "⋀t. t ∈ T ⟹ y t ∈ X"
shows "(y solves_ode f) T X"
using assms
by (auto simp: solves_ode_def)

lemma solves_odeD:
assumes "(y solves_ode f) T X"
shows solves_ode_vderivD: "(y has_vderiv_on (λt. f t (y t))) T"
and solves_ode_domainD: "⋀t. t ∈ T ⟹ y t ∈ X"
using assms
by (auto simp: solves_ode_def)

lemma solves_ode_continuous_on: "(y solves_ode f) T X ⟹ continuous_on T y"
by (auto intro!: vderiv_on_continuous_on simp: solves_ode_def)

lemma solves_ode_congI:
assumes "(x solves_ode f) T X"
assumes "⋀t. t ∈ T ⟹ x t = y t"
assumes "⋀t. t ∈ T ⟹ f t (x t) = g t (x t)"
assumes "T = S" "X = Y"
shows "(y solves_ode g) S Y"
using assms
by (auto simp: solves_ode_def Pi_iff)

lemma solves_ode_cong[cong]:
assumes "⋀t. t ∈ T ⟹ x t = y t"
assumes "⋀t. t ∈ T ⟹ f t (x t) = g t (x t)"
assumes "T = S" "X = Y"
shows "(x solves_ode f) T X ⟷ (y solves_ode g) S Y"
using assms
by (auto simp: solves_ode_def Pi_iff)

lemma solves_ode_on_subset:
assumes "(x solves_ode f) S Y"
assumes "T ⊆ S" "Y ⊆ X"
shows "(x solves_ode f) T X"
using assms
by (auto simp: solves_ode_def has_vderiv_on_subset)

lemma preflect_solution:
assumes "t0 ∈ T"
assumes sol: "((λt. x (preflect t0 t)) solves_ode (λt x. - f (preflect t0 t) x)) (preflect t0  T) X"
shows "(x solves_ode f) T X"
proof (rule solves_odeI)
from solves_odeD[OF sol]
have xm_deriv: "(x o preflect t0 has_vderiv_on (λt. - f (preflect t0 t) (x (preflect t0 t)))) (preflect t0  T)"
and xm_mem: "t ∈ preflect t0  T ⟹ x (preflect t0 t) ∈ X" for t
by simp_all
have "(x o preflect t0 o preflect t0 has_vderiv_on (λt. f t (x t))) T"
apply (rule has_vderiv_on_eq_rhs)
apply (rule has_vderiv_on_compose)
apply (rule xm_deriv)
apply (auto simp: preflect_def intro!: derivative_intros)
done
then show "(x has_vderiv_on (λt. f t (x t))) T"
show "x t ∈ X" if "t ∈ T" for t
using that xm_mem[of "preflect t0 t"]
by (auto simp: preflect_def)
qed

lemma solution_preflect:
assumes "t0 ∈ T"
assumes sol: "(x solves_ode f) T X"
shows "((λt. x (preflect t0 t)) solves_ode (λt x. - f (preflect t0 t) x)) (preflect t0  T) X"
using sol ‹t0 ∈ T›
by (simp_all add: preflect_def image_image preflect_solution[of t0])

lemma solution_eq_preflect_solution:
assumes "t0 ∈ T"
shows "(x solves_ode f) T X ⟷ ((λt. x (preflect t0 t)) solves_ode (λt x. - f (preflect t0 t) x)) (preflect t0  T) X"
using solution_preflect[OF ‹t0 ∈ T›] preflect_solution[OF ‹t0 ∈ T›]
by blast

lemma shift_autonomous_solution:
assumes sol: "(x solves_ode f) T X"
assumes auto: "⋀s t. s ∈ T ⟹ f s (x s) = f t (x s)"
shows "((λt. x (t + t0)) solves_ode f) ((λt. t - t0)  T) X"
using solves_odeD[OF sol]
apply (intro solves_odeI)
apply (rule has_vderiv_on_compose'[of x, THEN has_vderiv_on_eq_rhs])
apply (auto simp: image_image intro!: auto derivative_intros)
done

lemma solves_ode_singleton: "y t0 ∈ X ⟹ (y solves_ode f) {t0} X"
by (auto intro!: solves_odeI has_vderiv_on_singleton)

subsubsection‹Connecting solutions›
text‹\label{sec:combining-solutions}›

lemma connection_solves_ode:
assumes x: "(x solves_ode f) T X"
assumes y: "(y solves_ode g) S Y"
assumes conn_T: "closure S ∩ closure T ⊆ T"
assumes conn_S: "closure S ∩ closure T ⊆ S"
assumes conn_x: "⋀t. t ∈ closure S ⟹ t ∈ closure T ⟹ x t = y t"
assumes conn_f: "⋀t. t ∈ closure S ⟹ t ∈ closure T ⟹ f t (y t) = g t (y t)"
shows "((λt. if t ∈ T then x t else y t) solves_ode (λt. if t ∈ T then f t else g t)) (T ∪ S) (X ∪ Y)"
proof (rule solves_odeI)
from solves_odeD(2)[OF x] solves_odeD(2)[OF y]
show "t ∈ T ∪ S ⟹ (if t ∈ T then x t else y t) ∈ X ∪ Y" for t
by auto
show "((λt. if t ∈ T then x t else y t) has_vderiv_on (λt. (if t ∈ T then f t else g t) (if t ∈ T then x t else y t))) (T ∪ S)"
apply (rule has_vderiv_on_If[OF refl, THEN has_vderiv_on_eq_rhs])
unfolding Un_absorb2[OF conn_T] Un_absorb2[OF conn_S]
apply (rule solves_odeD(1)[OF x])
apply (rule solves_odeD(1)[OF y])
apply (simp_all add: conn_T conn_S Un_absorb2 conn_x conn_f)
done
qed

lemma
solves_ode_subset_range:
assumes x: "(x solves_ode f) T X"
assumes s: "x  T ⊆ Y"
shows "(x solves_ode f) T Y"
using assms
by (auto intro!: solves_odeI dest!: solves_odeD)

subsection ‹unique solution with initial value›

definition
usolves_ode_from :: "(real ⇒ 'a::real_normed_vector) ⇒ (real ⇒ 'a ⇒ 'a) ⇒ real ⇒ real set ⇒ 'a set ⇒ bool"
("((_) usolves'_ode (_) from (_))" [10, 10, 10] 10)
― ‹TODO: no idea about mixfix and precedences, check this!›
where
"(y usolves_ode f from t0) T X ⟷ (y solves_ode f) T X ∧ t0 ∈ T ∧ is_interval T ∧
(∀z T'. t0 ∈ T' ∧ is_interval T' ∧ T' ⊆ T ∧ (z solves_ode f) T' X ⟶ z t0 = y t0 ⟶ (∀t ∈ T'. z t = y t))"

text ‹uniqueness of solution can depend on domain ‹X›:›

lemma
"((λ_. 0::real) usolves_ode (λ_. sqrt) from 0) {0..} {0}"
"((λt. t⇧2 / 4) solves_ode (λ_. sqrt)) {0..} {0..}"
"(λt. t⇧2 / 4) 0 = (λ_. 0::real) 0"
by (auto intro!: derivative_eq_intros
simp: has_vderiv_on_def has_vector_derivative_def usolves_ode_from_def solves_ode_def
is_interval_ci real_sqrt_divide)

text ‹TODO: show that if solution stays in interior, then domain can be enlarged! (?)›

lemma usolves_odeD:
assumes "(y usolves_ode f from t0) T X"
shows "(y solves_ode f) T X"
and "t0 ∈ T"
and "is_interval T"
and "⋀z T' t. t0 ∈ T' ⟹ is_interval T' ⟹ T' ⊆ T ⟹(z solves_ode f) T' X ⟹ z t0 = y t0 ⟹ t ∈ T' ⟹ z t = y t"
using assms
unfolding usolves_ode_from_def
by blast+

lemma usolves_ode_rawI:
assumes "(y solves_ode f) T X" "t0 ∈ T" "is_interval T"
assumes "⋀z T' t. t0 ∈ T' ⟹ is_interval T' ⟹ T' ⊆ T ⟹ (z solves_ode f) T' X ⟹ z t0 = y t0 ⟹ t ∈ T' ⟹ z t = y t"
shows "(y usolves_ode f from t0) T X"
using assms
unfolding usolves_ode_from_def
by blast

lemma usolves_odeI:
assumes "(y solves_ode f) T X" "t0 ∈ T" "is_interval T"
assumes usol: "⋀z t. {t0 -- t} ⊆ T ⟹ (z solves_ode f) {t0 -- t} X ⟹ z t0 = y t0 ⟹ z t = y t"
shows "(y usolves_ode f from t0) T X"
proof (rule usolves_ode_rawI; fact?)
fix z T' t
assume T': "t0 ∈ T'" "is_interval T'" "T' ⊆ T"
and z: "(z solves_ode f) T' X" and iv: "z t0 = y t0" and t: "t ∈ T'"
have subset_T': "{t0 -- t} ⊆ T'"
by (rule closed_segment_subset_interval; fact)
with z have sol_cs: "(z solves_ode f) {t0 -- t} X"
by (rule solves_ode_on_subset[OF _ _ order_refl])
from subset_T' have subset_T: "{t0 -- t} ⊆ T"
using ‹T' ⊆ T› by simp
from usol[OF subset_T sol_cs iv]
show "z t = y t" by simp
qed

lemma is_interval_singleton[intro,simp]: "is_interval {t0}"
by (auto simp: is_interval_def intro!: euclidean_eqI[where 'a='a])

lemma usolves_ode_singleton: "x t0 ∈ X ⟹ (x usolves_ode f from t0) {t0} X"
by (auto intro!: usolves_odeI solves_ode_singleton)

lemma usolves_ode_congI:
assumes x: "(x usolves_ode f from t0) T X"
assumes "⋀t. t ∈ T ⟹ x t = y t"
assumes "⋀t y. t ∈ T ⟹ y ∈ X ⟹ f t y = g t y"― ‹TODO: weaken this assumption?!›
assumes "t0 = s0"
assumes "T = S"
assumes "X = Y"
shows "(y usolves_ode g from s0) S Y"
proof (rule usolves_ode_rawI)
from assms x have "(y solves_ode f) S Y"
then show "(y solves_ode g) S Y"
by (rule solves_ode_congI) (use assms in ‹auto simp: usolves_ode_from_def dest!: solves_ode_domainD›)
from assms show "s0 ∈ S" "is_interval S"
next
fix z T' t
assume hyps: "s0 ∈ T'" "is_interval T'" "T' ⊆ S" "(z solves_ode g) T' Y" "z s0 = y s0" "t ∈ T'"
from ‹(z solves_ode g) T' Y›
have zsol: "(z solves_ode f) T' Y"
by (rule solves_ode_congI) (use assms hyps in ‹auto dest!: solves_ode_domainD›)
have "z t = x t"
by (rule x[THEN usolves_odeD(4),where T' = T'])
(use zsol ‹s0 ∈ T'› ‹is_interval T'› ‹T' ⊆ S› ‹T = S› ‹z s0 = y s0› ‹t ∈ T'› assms in auto)
also have "y t = x t" using assms ‹t ∈ T'› ‹T' ⊆ S› ‹T = S› by auto
finally show "z t = y t" by simp
qed

lemma usolves_ode_cong[cong]:
assumes "⋀t. t ∈ T ⟹ x t = y t"
assumes "⋀t y. t ∈ T ⟹ y ∈ X ⟹ f t y = g t y"― ‹TODO: weaken this assumption?!›
assumes "t0 = s0"
assumes "T = S"
assumes "X = Y"
shows "(x usolves_ode f from t0) T X ⟷ (y usolves_ode g from s0) S Y"
apply (rule iffI)
subgoal by (rule usolves_ode_congI[OF _ assms]; assumption)
subgoal by (metis assms(1) assms(2) assms(3) assms(4) assms(5) usolves_ode_congI)
done

lemma shift_autonomous_unique_solution:
assumes usol: "(x usolves_ode f from t0) T X"
assumes auto: "⋀s t x. x ∈ X ⟹ f s x = f t x"
shows "((λt. x (t + t0 - t1)) usolves_ode f from t1) ((+) (t1 - t0)  T) X"
proof (rule usolves_ode_rawI)
from usolves_odeD[OF usol]
have sol: "(x solves_ode f) T X"
and "t0 ∈ T"
and "is_interval T"
and unique: "t0 ∈ T' ⟹ is_interval T' ⟹ T' ⊆ T ⟹ (z solves_ode f) T' X ⟹ z t0 = x t0 ⟹ t ∈ T' ⟹ z t = x t"
for z T' t
by blast+
have "(λt. t + t1 - t0) = (+) (t1 - t0)"
with shift_autonomous_solution[OF sol auto, of "t0 - t1"] solves_odeD[OF sol]
show "((λt. x (t + t0 - t1)) solves_ode f) ((+) (t1 - t0)  T) X"
from ‹t0 ∈ T› show "t1 ∈ (+) (t1 - t0)  T" by auto
from ‹is_interval T›
show "is_interval ((+) (t1 - t0)  T)"
by simp
fix z T' t
assume z: "(z solves_ode f) T' X"
and t0': "t1 ∈ T'" "T' ⊆ (+) (t1 - t0)  T"
and shift: "z t1 = x (t1 + t0 - t1)"
and t: "t ∈ T'"
and ivl: "is_interval T'"

let ?z = "(λt. z (t + (t1 - t0)))"

have "(?z solves_ode f) ((λt. t - (t1 - t0))  T') X"
apply (rule shift_autonomous_solution[OF z, of "t1 - t0"])
using solves_odeD[OF z]
by (auto intro!: auto)
with _ _ _ have "?z ((t + (t0 - t1))) = x (t + (t0 - t1))"
apply (rule unique[where z = ?z ])
using shift t t0' ivl
by auto
then show "z t = x (t + t0 - t1)"
qed

lemma three_intervals_lemma:
fixes a b c::real
assumes a: "a ∈ A - B"
and b: "b ∈ B - A"
and c: "c ∈ A ∩ B"
and iA: "is_interval A" and iB: "is_interval B"
and aI: "a ∈ I"
and bI: "b ∈ I"
and iI: "is_interval I"
shows "c ∈ I"
apply (rule mem_is_intervalI[OF iI aI bI])
using iA iB
apply (auto simp: is_interval_def)
apply (metis Diff_iff Int_iff a b c le_cases)
apply (metis Diff_iff Int_iff a b c le_cases)
done

lemma connection_usolves_ode:
assumes x: "(x usolves_ode f from tx) T X"
assumes y: "⋀t. t ∈ closure S ∩ closure T ⟹ (y usolves_ode g from t) S X"
assumes conn_T: "closure S ∩ closure T ⊆ T"
assumes conn_S: "closure S ∩ closure T ⊆ S"
assumes conn_t: "t ∈ closure S ∩ closure T"
assumes conn_x: "⋀t. t ∈ closure S ⟹ t ∈ closure T ⟹ x t = y t"
assumes conn_f: "⋀t x. t ∈ closure S ⟹ t ∈ closure T ⟹ x ∈ X ⟹ f t x = g t x"
shows "((λt. if t ∈ T then x t else y t) usolves_ode (λt. if t ∈ T then f t else g t) from tx) (T ∪ S) X"
apply (rule usolves_ode_rawI)
apply (subst Un_absorb[of X, symmetric])
apply (rule connection_solves_ode[OF usolves_odeD(1)[OF x] usolves_odeD(1)[OF y[OF conn_t]] conn_T conn_S conn_x conn_f])
subgoal by assumption
subgoal by assumption
subgoal by assumption
subgoal by assumption
subgoal using solves_odeD(2)[OF usolves_odeD(1)[OF x]] conn_T by (auto simp add: conn_x[symmetric])
subgoal using usolves_odeD(2)[OF x] by auto
subgoal using usolves_odeD(3)[OF x] usolves_odeD(3)[OF y]
apply (rule is_real_interval_union)
using conn_T conn_S conn_t by auto
subgoal premises prems for z TS' s
proof -
from ‹(z solves_ode _) _ _›
have "(z solves_ode (λt. if t ∈ T then f t else g t)) (T ∩ TS') X"
by (rule solves_ode_on_subset) auto
then have z_f: "(z solves_ode f) (T ∩ TS') X"
by (subst solves_ode_cong) auto

from prems(4)
have "(z solves_ode (λt. if t ∈ T then f t else g t)) (S ∩ TS') X"
by (rule solves_ode_on_subset) auto
then have z_g: "(z solves_ode g) (S ∩ TS') X"
apply (rule solves_ode_congI)
subgoal by simp
subgoal by clarsimp (meson closure_subset conn_f contra_subsetD prems(4) solves_ode_domainD)
subgoal by simp
subgoal by simp
done
have "tx ∈ T" using assms using usolves_odeD(2)[OF x] by auto

have "z tx = x tx" using assms prems
by (simp add: ‹tx ∈ T›)

from usolves_odeD(4)[OF x _ _ _ ‹(z solves_ode f) _ _›, of s] prems
have "z s = x s" if "s ∈ T" using that ‹tx ∈ T› ‹z tx = x tx›
by (auto simp: is_interval_Int usolves_odeD(3)[OF x] ‹is_interval TS'›)

moreover

{
assume "s ∉ T"
then have "s ∈ S" using prems assms by auto
{
assume "tx ∉ S"
then have "tx ∈ T - S" using ‹tx ∈ T› by simp
moreover have "s ∈ S - T" using ‹s ∉ T› ‹s ∈ S› by blast
ultimately have "t ∈ TS'"
apply (rule three_intervals_lemma)
subgoal using assms by auto
subgoal using usolves_odeD(3)[OF x] .
subgoal using usolves_odeD(3)[OF y[OF conn_t]] .
subgoal using ‹tx ∈ TS'› .
subgoal using ‹s ∈ TS'› .
subgoal using ‹is_interval TS'› .
done
with assms have t: "t ∈ closure S ∩ closure T ∩ TS'" by simp

then have "t ∈ S" "t ∈ T" "t ∈ TS'" using assms by auto
have "z t = x t"
apply (rule usolves_odeD(4)[OF x _ _ _ z_f, of t])
using ‹t ∈ TS'› ‹t ∈ T› prems assms ‹tx ∈ T› usolves_odeD(3)[OF x]
by (auto intro!: is_interval_Int)
with assms have "z t = y t" using t by auto

from usolves_odeD(4)[OF y[OF conn_t] _ _ _ z_g, of s] prems
have "z s = y s" using ‹s ∉ T› assms ‹z t = y t› t ‹t ∈ S›
‹is_interval TS'› usolves_odeD(3)[OF y[OF conn_t]]
by (auto simp: is_interval_Int)
} moreover {
assume "tx ∈ S"
with prems closure_subset ‹tx ∈ T›
have tx: "tx ∈ closure S ∩ closure T ∩ TS'" by force

then have "tx ∈ S" "tx ∈ T" "tx ∈ TS'" using assms by auto
have "z tx = x tx"
apply (rule usolves_odeD(4)[OF x _ _ _ z_f, of tx])
using ‹tx ∈ TS'› ‹tx ∈ T› prems assms ‹tx ∈ T› usolves_odeD(3)[OF x]
by (auto intro!: is_interval_Int)
with assms have "z tx = y tx" using tx by auto

from usolves_odeD(4)[OF y[where t=tx] _ _ _ z_g, of s] prems
have "z s = y s" using ‹s ∉ T› assms ‹z tx = y tx› tx ‹tx ∈ S›
‹is_interval TS'› usolves_odeD(3)[OF y]
by (auto simp: is_interval_Int)
} ultimately have "z s = y s" by blast
}
ultimately
show "z s = (if s ∈ T then x s else y s)" by simp
qed
done

lemma usolves_ode_union_closed:
assumes x: "(x usolves_ode f from tx) T X"
assumes y: "⋀t. t ∈ closure S ∩ closure T ⟹ (x usolves_ode f from t) S X"
assumes conn_T: "closure S ∩ closure T ⊆ T"
assumes conn_S: "closure S ∩ closure T ⊆ S"
assumes conn_t: "t ∈ closure S ∩ closure T"
shows "(x usolves_ode f from tx) (T ∪ S) X"
using connection_usolves_ode[OF assms] by simp

lemma usolves_ode_solves_odeI:
assumes "(x usolves_ode f from tx) T X"
assumes "(y solves_ode f) T X" "y tx = x tx"
shows "(y usolves_ode f from tx) T X"
using assms(1)
apply (rule usolves_ode_congI)
subgoal using assms by (metis set_eq_subset usolves_odeD(2) usolves_odeD(3) usolves_odeD(4))
by auto

lemma usolves_ode_subset_range:
assumes x: "(x usolves_ode f from t0) T X"
assumes r: "x  T ⊆ Y" and "Y ⊆ X"
shows "(x usolves_ode f from t0) T Y"
proof (rule usolves_odeI)
note usolves_odeD[OF x]
show "(x solves_ode f) T Y" by (rule solves_ode_subset_range; fact)
show "t0 ∈ T" "is_interval T" by fact+
fix z t
assume s: "{t0 -- t} ⊆ T" and z: "(z solves_ode f) {t0 -- t} Y" and z0: "z t0 = x t0"
then have "t0 ∈ {t0 -- t}" "is_interval {t0 -- t}"
by auto
moreover note s
moreover have "(z solves_ode f) {t0--t} X"
using solves_odeD[OF z] ‹Y ⊆ X›
by (intro solves_ode_subset_range[OF z]) force
moreover note z0
moreover have "t ∈ {t0 -- t}" by simp
ultimately show "z t = x t"
by (rule usolves_odeD[OF x])
qed

subsection ‹ivp on interval›

context
fixes t0 t1::real and T
defines "T ≡ closed_segment t0 t1"
begin

lemma is_solution_ext_cont:
"continuous_on T x ⟹ (ext_cont x (min t0 t1) (max t0 t1) solves_ode f) T X = (x solves_ode f) T X"
by (rule solves_ode_cong) (auto simp add: T_def min_def max_def closed_segment_eq_real_ivl)

lemma solution_fixed_point:
fixes x:: "real ⇒ 'a::banach"
assumes x: "(x solves_ode f) T X" and t: "t ∈ T"
shows "x t0 + ivl_integral t0 t (λt. f t (x t)) = x t"
proof -
from solves_odeD(1)[OF x, unfolded T_def]
have "(x has_vderiv_on (λt. f t (x t))) (closed_segment t0 t)"
by (rule has_vderiv_on_subset) (insert ‹t ∈ T›, auto simp: closed_segment_eq_real_ivl T_def)
from fundamental_theorem_of_calculus_ivl_integral[OF this]
have "((λt. f t (x t)) has_ivl_integral x t - x t0) t0 t" .
from this[THEN ivl_integral_unique]
show ?thesis by simp
qed

lemma solution_fixed_point_left:
fixes x:: "real ⇒ 'a::banach"
assumes x: "(x solves_ode f) T X" and t: "t ∈ T"
shows "x t1 - ivl_integral t t1 (λt. f t (x t)) = x t"
proof -
from solves_odeD(1)[OF x, unfolded T_def]
have "(x has_vderiv_on (λt. f t (x t))) (closed_segment t t1)"
by (rule has_vderiv_on_subset) (insert ‹t ∈ T›, auto simp: closed_segment_eq_real_ivl T_def)
from fundamental_theorem_of_calculus_ivl_integral[OF this]
have "((λt. f t (x t)) has_ivl_integral x t1 - x t) t t1" .
from this[THEN ivl_integral_unique]
show ?thesis by simp
qed

lemma solution_fixed_pointI:
fixes x:: "real ⇒ 'a::banach"
assumes cont_f: "continuous_on (T × X) (λ(t, x). f t x)"
assumes cont_x: "continuous_on T x"
assumes defined: "⋀t. t ∈ T ⟹ x t ∈ X"
assumes fp: "⋀t. t ∈ T ⟹ x t = x t0 + ivl_integral t0 t (λt. f t (x t))"
shows "(x solves_ode f) T X"
proof (rule solves_odeI)
note [continuous_intros] = continuous_on_compose_Pair[OF cont_f]
have "((λt. x t0 + ivl_integral t0 t (λt. f t (x t))) has_vderiv_on (λt. f t (x t))) T"
using cont_x defined
by (auto intro!: derivative_eq_intros ivl_integral_has_vector_derivative
continuous_intros
simp: has_vderiv_on_def T_def)
with fp show "(x has_vderiv_on (λt. f t (x t))) T" by simp

end

lemma solves_ode_half_open_segment_continuation:
fixes f::"real ⇒ 'a ⇒ 'a::banach"
assumes ode: "(x solves_ode f) {t0 --< t1} X"
assumes continuous: "continuous_on ({t0 -- t1} × X) (λ(t, x). f t x)"
assumes "compact X"
assumes "t0 ≠ t1"
obtains l where
"(x ⤏ l) (at t1 within {t0 --< t1})"
"((λt. if t = t1 then l else x t) solves_ode f) {t0 -- t1} X"
proof -
note [continuous_intros] = continuous_on_compose_Pair[OF continuous]
have "compact ((λ(t, x). f t x)  ({t0 -- t1} × X))"
by (auto intro!: compact_continuous_image continuous_intros compact_Times ‹compact X›
simp: split_beta)
then obtain B where "B > 0" and B: "⋀t x. t ∈ {t0 -- t1} ⟹ x ∈ X ⟹ norm (f t x) ≤ B"
by (auto dest!: compact_imp_bounded simp: bounded_pos)

have uc: "uniformly_continuous_on {t0 --< t1} x"
apply (rule lipschitz_on_uniformly_continuous[where L=B])
apply (rule bounded_vderiv_on_imp_lipschitz)
apply (rule solves_odeD[OF ode])
using solves_odeD(2)[OF ode] ‹0 < B›
by (auto simp: closed_segment_eq_real_ivl half_open_segment_real subset_iff
intro!: B split: if_split_asm)

have "t1 ∈ closure ({t0 --< t1})"
using closure_half_open_segment[of t0 t1] ‹t0 ≠ t1›
by simp
from uniformly_continuous_on_extension_on_closure[OF uc]
obtain g where uc_g: "uniformly_continuous_on {t0--t1} g"
and xg: "(⋀t. t ∈ {t0 --< t1} ⟹ x t = g t)"
using closure_half_open_segment[of t0 t1] ‹t0 ≠ t1›
by metis

from uc_g[THEN uniformly_continuous_imp_continuous, unfolded continuous_on_def]
have "(g ⤏ g t) (at t within {t0--t1})" if "t∈{t0--t1}" for t
using that by auto
then have g_tendsto: "(g ⤏ g t) (at t within {t0--<t1})" if "t∈{t0--t1}" for t
using that by (auto intro: tendsto_within_subset half_open_segment_subset)
then have x_tendsto: "(x ⤏ g t) (at t within {t0--<t1})" if "t∈{t0--t1}" for t
using that
by (subst Lim_cong_within[OF refl refl refl xg]) auto
then have "(x ⤏ g t1) (at t1 within {t0 --< t1})"
by auto
moreover
have nbot: "at s within {t0--<t1} ≠ bot" if "s ∈ {t0--t1}" for s
using that ‹t0 ≠ t1›
by (auto simp: trivial_limit_within islimpt_half_open_segment)
have g_mem: "s ∈ {t0--t1} ⟹ g s ∈ X" for s
apply (rule Lim_in_closed_set[OF compact_imp_closed[OF ‹compact X›] _ _ x_tendsto])
using solves_odeD(2)[OF ode] ‹t0 ≠ t1›
by (auto intro!: simp: eventually_at_filter nbot)
have "(g solves_ode f) {t0 -- t1} X"
apply (rule solution_fixed_pointI[OF continuous])
subgoal by (auto intro!: uc_g uniformly_continuous_imp_continuous)
subgoal by (rule g_mem)
subgoal premises prems for s
proof -
{
fix s
assume s: "s ∈ {t0--<t1}"
with prems have subs: "{t0--s} ⊆ {t0--<t1}"
by (auto simp: half_open_segment_real closed_segment_eq_real_ivl)
with ode have sol: "(x solves_ode f) ({t0--s}) X"
by (rule solves_ode_on_subset) (rule order_refl)
from subs have inner_eq: "t ∈ {t0 -- s} ⟹ x t = g t" for t
by (intro xg) auto
from solution_fixed_point[OF sol, of s]
have "g t0 + ivl_integral t0 s (λt. f t (g t)) - g s = 0"
using s prems ‹t0 ≠ t1›
by (auto simp: inner_eq cong: ivl_integral_cong)
} note fp = this

from prems have subs: "{t0--s} ⊆ {t0--t1}"
by (auto simp: closed_segment_eq_real_ivl)
have int: "(λt. f t (g t)) integrable_on {t0--t1}"
using prems subs
by (auto intro!: integrable_continuous_closed_segment continuous_intros g_mem
uc_g[THEN uniformly_continuous_imp_continuous, THEN continuous_on_subset])
note ivl_tendsto[tendsto_intros] =
indefinite_ivl_integral_continuous(1)[OF int, unfolded continuous_on_def, rule_format]

from subs half_open_segment_subset
have "((λs. g t0 + ivl_integral t0 s (λt. f t (g t)) - g s) ⤏
g t0 + ivl_integral t0 s (λt. f t (g t)) - g s) (at s within {t0 --< t1})"
using subs
by (auto intro!: tendsto_intros ivl_tendsto[THEN tendsto_within_subset]
g_tendsto[THEN tendsto_within_subset])
moreover
have "((λs. g t0 + ivl_integral t0 s (λt. f t (g t)) - g s) ⤏ 0) (at s within {t0 --< t1})"
apply (subst Lim_cong_within[OF refl refl refl, where g="λ_. 0"])
subgoal by (subst fp) auto
subgoal by simp
done
ultimately have "g t0 + ivl_integral t0 s (λt. f t (g t)) - g s = 0"
using nbot prems tendsto_unique by blast
then show "g s = g t0 + ivl_integral t0 s (λt. f t (g t))" by simp
qed
done
then have "((λt. if t = t1 then g t1 else x t) solves_ode f) {t0--t1} X"
apply (rule solves_ode_congI)
using xg ‹t0 ≠ t1›
by (auto simp: half_open_segment_closed_segmentI)
ultimately show ?thesis ..
qed

subsection ‹Picard-Lindeloef on set of functions into closed set›
text‹\label{sec:plclosed}›

locale continuous_rhs = fixes T X f
assumes continuous: "continuous_on (T × X) (λ(t, x). f t x)"
begin

lemma continuous_rhs_comp[continuous_intros]:
assumes [continuous_intros]: "continuous_on S g"
assumes [continuous_intros]: "continuous_on S h"
assumes "g  S ⊆ T"
assumes "h  S ⊆ X"
shows "continuous_on S (λx. f (g x) (h x))"
using continuous_on_compose_Pair[OF continuous assms(1,2)] assms(3,4)
by auto

end

locale global_lipschitz =
fixes T X f and L::real
assumes lipschitz: "⋀t. t ∈ T ⟹ L-lipschitz_on X (λx. f t x)"

locale closed_domain =
fixes X assumes closed: "closed X"

locale interval = fixes T::"real set"
assumes interval: "is_interval T"
begin

lemma closed_segment_subset_domain: "t0 ∈ T ⟹ t ∈ T ⟹ closed_segment t0 t ⊆ T"

lemma closed_segment_subset_domainI: "t0 ∈ T ⟹ t ∈ T ⟹ s ∈ closed_segment t0 t ⟹ s ∈ T"
using closed_segment_subset_domain by force

lemma convex[intro, simp]: "convex T"
and connected[intro, simp]: "connected T"
by (simp_all add: interval is_interval_connected is_interval_convex )

end

locale nonempty_set = fixes T assumes nonempty_set: "T ≠ {}"

locale compact_interval = interval + nonempty_set T +
assumes compact_time: "compact T"
begin

definition "tmin = Inf T"
definition "tmax = Sup T"

lemma
shows tmin: "t ∈ T ⟹ tmin ≤ t" "tmin ∈ T"
and tmax: "t ∈ T ⟹ t ≤ tmax" "tmax ∈ T"
using nonempty_set
by (auto intro!: cInf_lower cSup_upper bounded_imp_bdd_below bounded_imp_bdd_above
compact_imp_bounded compact_time closed_contains_Inf closed_contains_Sup compact_imp_closed
simp: tmin_def tmax_def)

lemma tmin_le_tmax[intro, simp]: "tmin ≤ tmax"
using nonempty_set tmin tmax by auto

lemma T_def: "T = {tmin .. tmax}"
using closed_segment_subset_interval[OF interval tmin(2) tmax(2)]
by (auto simp: closed_segment_eq_real_ivl subset_iff intro!: tmin tmax)

lemma mem_T_I[intro, simp]: "tmin ≤ t ⟹ t ≤ tmax ⟹ t ∈ T"
using interval mem_is_interval_1_I tmax(2) tmin(2) by blast

end

locale self_mapping = interval T for T +
fixes t0::real and x0 f X
assumes iv_defined: "t0 ∈ T" "x0 ∈ X"
assumes self_mapping:
"⋀x t. t ∈ T ⟹ x t0 = x0 ⟹ x ∈ closed_segment t0 t → X ⟹
continuous_on (closed_segment t0 t) x ⟹ x t0 + ivl_integral t0 t (λt. f t (x t)) ∈ X"
begin

sublocale nonempty_set T using iv_defined by unfold_locales auto

lemma closed_segment_iv_subset_domain: "t ∈ T ⟹ closed_segment t0 t ⊆ T"

end

locale unique_on_closed =
compact_interval T +
self_mapping T t0 x0 f X +
continuous_rhs T X f +
closed_domain X +
global_lipschitz T X f L for t0::real and T and x0::"'a::banach" and f X L
begin

lemma T_split: "T = {tmin .. t0} ∪ {t0 .. tmax}"
by (metis T_def atLeastAtMost_iff iv_defined(1) ivl_disj_un_two_touch(4))

lemma L_nonneg: "0 ≤ L"
by (auto intro!: lipschitz_on_nonneg[OF lipschitz] iv_defined)

text ‹Picard Iteration›

definition P_inner where "P_inner x t = x0 + ivl_integral t0 t (λt. f  t (x t))"

definition P::"(real ⇒⇩C 'a) ⇒ (real ⇒⇩C 'a)"
where "P x = (SOME g::real⇒⇩C 'a.
(∀t ∈ T. g t = P_inner x t) ∧
(∀t≤tmin. g t = P_inner x tmin) ∧
(∀t≥tmax. g t = P_inner x tmax))"

lemma cont_P_inner_ivl:
"x ∈ T →⇩C X ⟹ continuous_on {tmin..tmax} (P_inner (apply_bcontfun x))"
apply (auto simp: real_Icc_closed_segment P_inner_def Pi_iff mem_PiC_iff
intro!: continuous_intros indefinite_ivl_integral_continuous_subset
integrable_continuous_closed_segment tmin(1) tmax(1))
using closed_segment_subset_domainI tmax(2) tmin(2) apply blast
using closed_segment_subset_domainI tmax(2) tmin(2) apply blast
using T_def closed_segment_eq_real_ivl iv_defined(1) by auto

lemma P_inner_t0[simp]: "P_inner g t0 = x0"

lemma t0_cs_tmin_tmax: "t0 ∈ {tmin--tmax}" and cs_tmin_tmax_subset: "{tmin--tmax} ⊆ T"
using iv_defined T_def closed_segment_eq_real_ivl
by auto

lemma
P_eqs:
assumes "x ∈ T →⇩C X"
shows P_eq_P_inner: "t ∈ T ⟹ P x t = P_inner x t"
and P_le_tmin: "t ≤ tmin ⟹ P x t = P_inner x tmin"
and P_ge_tmax: "t ≥ tmax ⟹ P x t = P_inner x tmax"
unfolding atomize_conj atomize_imp
proof goal_cases
case 1
obtain g where
"t ∈ {tmin .. tmax} ⟹ apply_bcontfun g t = P_inner (apply_bcontfun x) t"
"apply_bcontfun g t = P_inner (apply_bcontfun x) (clamp tmin tmax t)"
for t
by (metis continuous_on_cbox_bcontfunE cont_P_inner_ivl[OF assms(1)] cbox_interval)
with T_def have "∃g::real⇒⇩C 'a.
(∀t ∈ T. g t = P_inner x t) ∧
(∀t≤tmin. g t = P_inner x tmin) ∧
(∀t≥tmax. g t = P_inner x tmax)"
by (auto intro!: exI[where x=g])
then have "(∀t ∈ T. P x t = P_inner x t) ∧
(∀t≤tmin. P x t = P_inner x tmin) ∧
(∀t≥tmax. P x t = P_inner x tmax)"
unfolding P_def
by (rule someI_ex)
then show ?case using T_def by auto
qed

lemma P_if_eq:
"x ∈ T →⇩C X ⟹
P x t = (if tmin ≤ t ∧ t ≤ tmax then P_inner x t else if t ≥ tmax then P_inner x tmax else P_inner x tmin)"
by (auto simp: P_eqs)

lemma dist_P_le:
assumes y: "y ∈ T →⇩C X" and z: "z ∈ T →⇩C X"
assumes le: "⋀t. tmin ≤ t ⟹ t ≤ tmax ⟹ dist (P_inner y t) (P_inner z t) ≤ R"
assumes "0 ≤ R"
shows "dist (P y t) (P z t) ≤ R"
by (cases "t ≤ tmin"; cases "t ≥ tmax") (auto simp: P_eqs y z not_le intro!: le)

lemma P_def':
assumes "t ∈ T"
assumes "fixed_point ∈ T →⇩C X"
shows "(P fixed_point) t = x0 + ivl_integral t0 t (λx. f x (fixed_point x))"
by (simp add: P_eq_P_inner assms P_inner_def)

definition "iter_space = PiC T ((λ_. X)(t0:={x0}))"

lemma iter_spaceI:
assumes "g ∈ T →⇩C X" "g t0 = x0"
shows "g ∈ iter_space"
using assms
by (simp add: iter_space_def mem_PiC_iff Pi_iff)

lemma iter_spaceD:
assumes "g ∈ iter_space"
shows "g ∈ T →⇩C X" "apply_bcontfun g t0 = x0"
using assms iv_defined
by (auto simp add: iter_space_def mem_PiC_iff split: if_splits)

lemma const_in_iter_space: "const_bcontfun x0 ∈ iter_space"
by (auto simp: iter_space_def iv_defined mem_PiC_iff)

lemma closed_iter_space: "closed iter_space"
by (auto simp: iter_space_def intro!: closed_PiC closed)

lemma iter_space_notempty: "iter_space ≠ {}"
using const_in_iter_space by blast

lemma clamp_in_eq[simp]: fixes a x b::real shows "a ≤ x ⟹ x ≤ b ⟹ clamp a b x = x"
by (auto simp: clamp_def)

lemma P_self_mapping:
assumes in_space: "g ∈ iter_space"
shows "P g ∈ iter_space"
proof (rule iter_spaceI)
show x0: "P g t0 = x0"
by (auto simp: P_def' iv_defined iter_spaceD[OF in_space])
from iter_spaceD(1)[OF in_space] show "P g ∈ T →⇩C X"
unfolding mem_PiC_iff Pi_iff
apply (auto simp: mem_PiC_iff Pi_iff P_def')
apply (auto simp: iter_spaceD(2)[OF in_space, symmetric] intro!: self_mapping)
using closed_segment_subset_domainI iv_defined(1) by blast
qed

lemma continuous_on_T: "continuous_on {tmin .. tmax} g ⟹ continuous_on T g"
using T_def by auto

lemma T_closed_segment_subsetI[intro, simp]: "t ∈ {tmin--tmax} ⟹ t ∈ T"
and T_subsetI[intro, simp]: "tmin ≤ t ⟹ t ≤ tmax ⟹ t ∈ T"
by (subst T_def, simp add: closed_segment_eq_real_ivl)+

lemma t0_mem_closed_segment[intro, simp]: "t0 ∈ {tmin--tmax}"
using T_def iv_defined

lemma tmin_le_t0[intro, simp]: "tmin ≤ t0"
and tmax_ge_t0[intro, simp]: "tmax ≥ t0"
using t0_mem_closed_segment
unfolding closed_segment_eq_real_ivl
by simp_all

lemma apply_bcontfun_solution_fixed_point:
assumes ode: "(apply_bcontfun x solves_ode f) T X"
assumes iv: "x t0 = x0"
assumes t: "t ∈ T"
shows "P x t = x t"
proof -
have "t ∈ {t0 -- t}" by simp
have ode': "(apply_bcontfun x solves_ode f) {t0--t} X" "t ∈ {t0 -- t}"
using ode T_def closed_segment_eq_real_ivl t apply auto
using closed_segment_iv_subset_domain solves_ode_on_subset apply fastforce
using closed_segment_iv_subset_domain solves_ode_on_subset apply fastforce
done
from solves_odeD[OF ode]
have x: "x ∈ T →⇩C X" by (auto simp: mem_PiC_iff)
from solution_fixed_point[OF ode'] iv
show ?thesis
unfolding P_def'[OF t x]
by simp
qed

lemma
solution_in_iter_space:
assumes ode: "(apply_bcontfun z solves_ode f) T X"
assumes iv: "z t0 = x0"
shows "z ∈ iter_space" (is "?z ∈ _")
proof -
from T_def ode have ode: "(z solves_ode f) {tmin -- tmax} X"
have "(?z solves_ode f) T X"
using is_solution_ext_cont[OF solves_ode_continuous_on[OF ode], of f X] ode T_def
by (auto simp: min_def max_def closed_segment_eq_real_ivl)
then have "z ∈ T →⇩C X"
by (auto simp add: solves_ode_def mem_PiC_iff)
thus "?z ∈ iter_space"
by (auto simp: iv intro!: iter_spaceI)
qed

end

locale unique_on_bounded_closed = unique_on_closed +
assumes lipschitz_bound: "⋀s t. s ∈ T ⟹ t ∈ T ⟹ abs (s - t) * L < 1"
begin

lemma lipschitz_bound_maxmin: "(tmax - tmin) * L < 1"
using lipschitz_bound[of tmax tmin]
by auto

lemma lipschitz_P:
shows "((tmax - tmin) * L)-lipschitz_on iter_space P"
proof (rule lipschitz_onI)
have "t0 ∈ T" by (simp add: iv_defined)
then show "0 ≤ (tmax - tmin) * L"
using T_def
by (auto intro!: mult_nonneg_nonneg lipschitz lipschitz_on_nonneg[OF lipschitz]
iv_defined)
fix y z
assume "y ∈ iter_space" and "z ∈ iter_space"
hence y_defined: "y ∈ (T →⇩C X)" and "y t0 = x0"
and z_defined: "z ∈ (T →⇩C X)" and "y t0 = x0"
by (auto dest: iter_spaceD)
have defined: "s ∈ T" "y s ∈ X" "z s ∈ X" if "s ∈ closed_segment tmin tmax" for s
using y_defined z_defined that T_def
by (auto simp: mem_PiC_iff)
{
note [intro, simp] = integrable_continuous_closed_segment
fix t
assume t_bounds: "tmin ≤ t" "t ≤ tmax"
then have cs_subs: "closed_segment t0 t ⊆ closed_segment tmin tmax"
by (auto simp: closed_segment_eq_real_ivl)
then have cs_subs_ext: "⋀ta. ta ∈ {t0--t} ⟹ ta ∈ {tmin--tmax}" by auto

have "norm (P_inner y t - P_inner z t) =
norm (ivl_integral t0 t (λt. f t (y t) - f t (z t)))"
by (subst ivl_integral_diff)
(auto intro!: integrable_continuous_closed_segment continuous_intros defined cs_subs_ext simp: P_inner_def)
also have "... ≤ abs (ivl_integral t0 t (λt. norm (f t (y t) - f t (z t))))"
by (rule ivl_integral_norm_bound_ivl_integral)
(auto intro!: ivl_integral_norm_bound_ivl_integral continuous_intros integrable_continuous_closed_segment
simp: defined cs_subs_ext)
also have "... ≤ abs (ivl_integral t0 t (λt. L * norm (y t - z t)))"
using lipschitz t_bounds T_def y_defined z_defined cs_subs
by (intro norm_ivl_integral_le) (auto intro!: continuous_intros integrable_continuous_closed_segment
simp add: dist_norm lipschitz_on_def mem_PiC_iff Pi_iff)
also have "... ≤ abs (ivl_integral t0 t (λt. L * norm (y - z)))"
using norm_bounded[of "y - z"]
L_nonneg
by (intro norm_ivl_integral_le) (auto intro!: continuous_intros mult_left_mono)
also have "... = L * abs (t - t0) * norm (y - z)"
using t_bounds L_nonneg by (simp add: abs_mult)
also have "... ≤ L * (tmax - tmin) * norm (y - z)"
using t_bounds zero_le_dist L_nonneg cs_subs tmin_le_t0 tmax_ge_t0
by (auto intro!: mult_right_mono mult_left_mono simp: closed_segment_eq_real_ivl abs_real_def
simp del: tmin_le_t0 tmax_ge_t0 split: if_split_asm)
finally
have "dist (P_inner y t) (P_inner z t) ≤ (tmax - tmin) * L * dist y z"
} note * = this
show "dist (P y) (P z) ≤ (tmax - tmin) * L * dist y z"
by (auto intro!: dist_bound dist_P_le * y_defined z_defined mult_nonneg_nonneg L_nonneg)
qed

lemma fixed_point_unique: "∃!x∈iter_space. P x = x"
using lipschitz lipschitz_bound_maxmin lipschitz_P T_def
complete_UNIV iv_defined
by (intro banach_fix)
(auto
intro: P_self_mapping split_mult_pos_le
intro!: closed_iter_space iter_space_notempty mult_nonneg_nonneg
simp: lipschitz_on_def complete_eq_closed)

definition fixed_point where
"fixed_point = (THE x. x ∈ iter_space ∧ P x = x)"

lemma fixed_point':
"fixed_point ∈ iter_space ∧ P fixed_point = fixed_point"
unfolding fixed_point_def using fixed_point_unique
by (rule theI')

lemma fixed_point:
"fixed_point ∈ iter_space" "P fixed_point = fixed_point"
using fixed_point' by simp_all

lemma fixed_point_equality': "x ∈ iter_space ∧ P x = x ⟹ fixed_point = x"
unfolding fixed_point_def using fixed_point_unique
by (rule the1_equality)

lemma fixed_point_equality: "x ∈ iter_space ⟹ P x = x ⟹ fixed_point = x"
using fixed_point_equality'[of x] by auto

lemma fixed_point_iv: "fixed_point t0 = x0"
and fixed_point_domain: "x ∈ T ⟹ fixed_point x ∈ X"
using fixed_point
by (force dest: iter_spaceD simp: mem_PiC_iff)+

lemma fixed_point_has_vderiv_on: "(fixed_point has_vderiv_on (λt. f t (fixed_point t))) T"
proof -
have "continuous_on T (λx. f x (fixed_point x))"
using fixed_point_domain
by (auto intro!: continuous_intros)
then have "((λu. x0 + ivl_integral t0 u (λx. f x (fixed_point x))) has_vderiv_on (λt. f t (fixed_point t))) T"
by (auto intro!: derivative_intros ivl_integral_has_vderiv_on_compact_interval interval compact_time)
then show ?thesis
proof (rule has_vderiv_eq)
fix t
assume t: "t ∈ T"
have "fixed_point t = P fixed_point t"
using fixed_point by simp
also have "… = x0 + ivl_integral t0 t (λx. f x (fixed_point x))"
using t fixed_point_domain
by (auto simp: P_def' mem_PiC_iff)
finally show "x0 + ivl_integral t0 t (λx. f x (fixed_point x)) = fixed_point t" by simp
qed (insert T_def, auto simp: closed_segment_eq_real_ivl)
qed

lemma fixed_point_solution:
shows "(fixed_point solves_ode f) T X"
using fixed_point_has_vderiv_on fixed_point_domain
by (rule solves_odeI)

subsubsection ‹Unique solution›
text‹\label{sec:ivp-ubs}›

lemma solves_ode_equals_fixed_point:
assumes ode: "(x solves_ode f) T X"
assumes iv: "x t0 = x0"
assumes t: "t ∈ T"
shows "x t = fixed_point t"
proof -
from solves_ode_continuous_on[OF ode] T_def
have "continuous_on (cbox tmin tmax) x" by simp
from continuous_on_cbox_bcontfunE[OF this]
obtain g where g:
"t ∈ {tmin .. tmax} ⟹ apply_bcontfun g t = x t"
"apply_bcontfun g t = x (clamp tmin tmax t)"
for t
by (metis interval_cbox)
with ode T_def have ode_g: "(g solves_ode f) T X"
by (metis (no_types, lifting) solves_ode_cong)
have "x t = g t"
using t T_def
by (intro g[symmetric]) auto
also
have "g t0 = x0" "g ∈ T →⇩C X"
using iv g solves_odeD(2)[OF ode_g]
unfolding mem_PiC_iff atLeastAtMost_iff
by blast+
then have "g ∈ iter_space"
by (intro iter_spaceI)
then have "g = fixed_point"
apply (rule fixed_point_equality[symmetric])
apply (rule bcontfun_eqI)
subgoal for t
using apply_bcontfun_solution_fixed_point[OF ode_g ‹g t0 = x0›, of tmin]
apply_bcontfun_solution_fixed_point[OF ode_g ‹g t0 = x0›, of tmax]
apply_bcontfun_solution_fixed_point[OF ode_g ‹g t0 = x0›, of t]
using T_def
by (fastforce simp: P_eqs not_le ‹g ∈ T →⇩C X› g)
done
finally show ?thesis .
qed

lemma solves_ode_on_closed_segment_equals_fixed_point:
assumes ode: "(x solves_ode f) {t0 -- t1'} X"
assumes iv: "x t0 = x0"
assumes subset: "{t0--t1'} ⊆ T"
assumes t_mem: "t ∈ {t0--t1'}"
shows "x t = fixed_point t"
proof -
have subsetI: "t ∈ {t0--t1'} ⟹ t ∈ T" for t
using subset by auto
interpret s: unique_on_bounded_closed t0 "{t0--t1'}" x0 f X L
apply - apply unfold_locales
subgoal by simp
subgoal by simp
subgoal by simp
subgoal using iv_defined by simp
subgoal by (intro self_mapping subsetI)
subgoal by (rule continuous_on_subset[OF continuous]) (auto simp: subsetI )
subgoal by (rule lipschitz) (auto simp: subsetI)
subgoal by (auto intro!: subsetI lipschitz_bound)
done
have "x t = s.fixed_point t"
by (rule s.solves_ode_equals_fixed_point; fact)
moreover
have "fixed_point t = s.fixed_point t"
by (intro s.solves_ode_equals_fixed_point solves_ode_on_subset[OF fixed_point_solution] assms
fixed_point_iv order_refl subset t_mem)
ultimately show ?thesis by simp
qed

lemma unique_solution:
assumes ivp1: "(x solves_ode f) T X" "x t0 = x0"
assumes ivp2: "(y solves_ode f) T X" "y t0 = x0"
assumes "t ∈ T"
shows "x t = y t"
using solves_ode_equals_fixed_point[OF ivp1 ‹t ∈ T›]
solves_ode_equals_fixed_point[OF ivp2 ‹t ∈ T›]
by simp

lemma fixed_point_usolves_ode: "(fixed_point usolves_ode f from t0) T X"
apply (rule usolves_odeI[OF fixed_point_solution])
subgoal by (rule interval)
subgoal
using fixed_point_iv solves_ode_on_closed_segment_equals_fixed_point
by auto
done

end

lemma closed_segment_Un:
fixes a b c::real
assumes "b ∈ closed_segment a c"
shows "closed_segment a b ∪ closed_segment b c = closed_segment a c"
using assms
by (auto simp: closed_segment_eq_real_ivl)

lemma closed_segment_closed_segment_subset:
fixes s::real and i::nat
assumes "s ∈ closed_segment a b"
assumes "a ∈ closed_segment c d" "b ∈ closed_segment c d"
shows "s ∈ closed_segment c d"
using assms
by (auto simp: closed_segment_eq_real_ivl split: if_split_asm)

context unique_on_closed begin

context― ‹solution until t1›
fixes t1::real
assumes mem_t1: "t1 ∈ T"
begin

lemma subdivide_count_ex: "∃n. L * abs (t1 - t0) / (Suc n) < 1"
by auto (meson add_strict_increasing less_numeral_extra(1) real_arch_simple)

definition "subdivide_count = (SOME n. L * abs (t1 - t0) / Suc n < 1)"

lemma subdivide_count: "L * abs (t1 - t0) / Suc subdivide_count < 1"
unfolding subdivide_count_def
using subdivide_count_ex
by (rule someI_ex)

lemma subdivide_lipschitz:
assumes "¦s - t¦ ≤ abs (t1 - t0) / Suc subdivide_count"
shows "¦s - t¦ * L < 1"
proof -
from assms L_nonneg
have "¦s - t¦ * L ≤ abs (t1 - t0) / Suc subdivide_count * L"
by (rule mult_right_mono)
also have "… < 1"
using subdivide_count
finally show ?thesis .
qed

lemma subdivide_lipschitz_lemma:
assumes st: "s ∈ {a -- b}" "t ∈ {a -- b}"
assumes "abs (b - a) ≤ abs (t1 - t0) / Suc subdivide_count"
shows "¦s - t¦ * L < 1"
apply (rule subdivide_lipschitz)
apply (rule order_trans[where y="abs (b - a)"])
using assms
by (auto simp: closed_segment_eq_real_ivl split: if_splits)

definition "step = (t1 - t0) / Suc subdivide_count"

lemma last_step: "t0 + real (Suc subdivide_count) * step = t1"
by (auto simp: step_def)

lemma step_in_segment:
assumes "0 ≤ i" "i ≤ real (Suc subdivide_count)"
shows "t0 + i * step ∈ closed_segment t0 t1"
unfolding closed_segment_eq_real_ivl step_def
proof (clarsimp, safe)
assume "t0 ≤ t1"
then have "(t1 - t0) * i ≤ (t1 - t0) * (1 + subdivide_count)"
using assms
by (auto intro!: mult_left_mono)
then show "t0 + i * (t1 - t0) / (1 + real subdivide_count) ≤ t1"
next
assume "¬t0 ≤ t1"
then have "(1 + subdivide_count) * (t0 - t1) ≥ i * (t0 - t1)"
using assms
by (auto intro!: mult_right_mono)
then show "t1 ≤ t0 + i * (t1 - t0) / (1 + real subdivide_count)"
show "i * (t1 - t0) / (1 + real subdivide_count) ≤ 0"
using ‹¬t0 ≤ t1›
by (auto simp: divide_simps mult_le_0_iff assms)
qed (auto intro!: divide_nonneg_nonneg mult_nonneg_nonneg assms)

lemma subset_T1:
fixes s::real and i::nat
assumes "s ∈ closed_segment t0 (t0 + i * step)"
assumes "i ≤ Suc subdivide_count"
shows "s ∈ {t0 -- t1}"
using closed_segment_closed_segment_subset assms of_nat_le_iff of_nat_0_le_iff step_in_segment
by blast

lemma subset_T: "{t0 -- t1} ⊆ T" and subset_TI: "s ∈ {t0 -- t1} ⟹ s ∈ T"
using closed_segment_iv_subset_domain mem_t1 by blast+

primrec psolution::"nat ⇒ real ⇒ 'a" where
"psolution 0 t = x0"
| "psolution (Suc i) t = unique_on_bounded_closed.fixed_point
(t0 + real i * step) {t0 + real i * step -- t0 + real (Suc i) * step}
(psolution i (t0 + real i * step)) f X t"

definition "psolutions t = psolution (LEAST i. t ∈ closed_segment (t0 + real (i - 1) * step) (t0 + real i * step)) t"

lemma psolutions_usolves_until_step:
assumes i_le: "i ≤ Suc subdivide_count"
shows "(psolutions usolves_ode f from t0) (closed_segment t0 (t0 + real i * step)) X"
proof cases
assume "t0 = t1"
then have "step = 0"
unfolding step_def by simp
then show ?thesis by (simp add: psolutions_def iv_defined usolves_ode_singleton)
next
assume "t0 ≠ t1"
then have "step ≠ 0"
define S where "S ≡ λi. closed_segment (t0 + real (i - 1) * step) (t0 + real i * step)"
have solution_eq: "psolutions ≡ λt. psolution (LEAST i. t ∈ S i) t"
show ?thesis
unfolding solution_eq
using i_le
proof (induction i)
case 0 then show ?case by (simp add: iv_defined usolves_ode_singleton S_def)
next
case (Suc i)
let ?sol = "λt. psolution (LEAST i. t ∈ S i) t"
let ?pi = "t0 + real (i - Suc 0) * step" and ?i = "t0 + real i * step" and ?si = "t0 + (1 + real i) * step"
from Suc have ui: "(?sol usolves_ode f from t0) (closed_segment t0 (t0 + real i * step)) X"
by simp

from usolves_odeD(1)[OF Suc.IH] Suc
have IH_sol: "(?sol solves_ode f) (closed_segment t0 ?i) X"
by simp

have Least_eq_t0[simp]: "(LEAST n. t0 ∈ S n) = 0"
by (rule Least_equality) (auto simp add: S_def)
have Least_eq[simp]: "(LEAST n. t0 + real i * step ∈ S n) = i" for i
apply (rule Least_equality)
(auto simp add`