Theory HS_ODEs

(*  Title:       ODEs and Dynamical Systems for HS verification
    Author:      Jonathan Julián Huerta y Munive, 2020
    Maintainer:  Jonathan Julián Huerta y Munive <jonjulian23@gmail.com>
*)

section ‹ Ordinary Differential Equations ›

text ‹Vector fields @{text "f::real ⇒ 'a ⇒ ('a::real_normed_vector)"} represent systems 
of ordinary differential equations (ODEs). Picard-Lindeloef's theorem guarantees existence 
and uniqueness of local solutions to initial value problems involving Lipschitz continuous 
vector fields. A (local) flow @{text "φ::real ⇒ 'a ⇒ ('a::real_normed_vector)"} for such 
a system is the function that maps initial conditions to their unique solutions. In dynamical 
systems, the set of all points @{text "φ t s::'a"} for a fixed @{text "s::'a"} is the flow's 
orbit. If the orbit of each @{text "s ∈ I"} is conatined in @{text I}, then @{text I} is an 
invariant set of this system. This section formalises these concepts with a focus on hybrid 
systems (HS) verification.›

theory HS_ODEs
  imports "HS_Preliminaries"
begin

subsection ‹ Initial value problems and orbits ›

notation image (‹𝒫›)

lemma image_le_pred[simp]: "(𝒫 f A ⊆ {s. G s}) = (∀x∈A. G (f x))"
  unfolding image_def by force

definition ivp_sols :: "(real ⇒ 'a ⇒ ('a::real_normed_vector)) ⇒ ('a ⇒ real set) ⇒ 'a set ⇒ 
  real ⇒ 'a ⇒ (real ⇒ 'a) set" (‹Sols›)
  where "Sols f U S t0 s = {X ∈ U s → S. (D X = (λt. f t (X t)) on U s) ∧ X t0 = s ∧ t0 ∈ U s}"

lemma ivp_solsI: 
  assumes "D X = (λt. f t (X t)) on U s" and "X t0 = s" 
      and "X ∈ U s → S" and "t0 ∈ U s"
    shows "X ∈ Sols f U S t0 s"
  using assms unfolding ivp_sols_def by blast

lemma ivp_solsD:
  assumes "X ∈ Sols f U S t0 s"
  shows "D X = (λt. f t (X t)) on U s" and "X t0 = s" 
    and "X ∈ U s → S" and "t0 ∈ U s"
  using assms unfolding ivp_sols_def by auto

lemma in_ivp_sols_subset:
  "t0 ∈ (U s) ⟹ (U s) ⊆ (T s) ⟹ X ∈ Sols f T S t0 s ⟹ X ∈ Sols f U S t0 s "
  apply(rule ivp_solsI)
  using ivp_solsD(1,2) has_vderiv_on_subset 
     apply blast+
  by (drule ivp_solsD(3)) auto

abbreviation "down U t ≡ {τ ∈ U. τ ≤ t}"

definition g_orbit :: "(('a::ord) ⇒ 'b) ⇒ ('b ⇒ bool) ⇒ 'a set ⇒ 'b set" (‹γ›)
  where "γ X G U = ⋃{𝒫 X (down U t) |t. 𝒫 X (down U t) ⊆ {s. G s}}"

lemma g_orbit_eq: 
  fixes X::"('a::preorder) ⇒ 'b"
  shows "γ X G U = {X t |t. t ∈ U ∧ (∀τ∈down U t. G (X τ))}"
  unfolding g_orbit_def using order_trans by auto blast

definition g_orbital :: "(real ⇒ 'a ⇒ 'a) ⇒ ('a ⇒ bool) ⇒ ('a ⇒ real set) ⇒ 'a set ⇒ real ⇒ 
  ('a::real_normed_vector) ⇒ 'a set" 
  where "g_orbital f G U S t0 s = ⋃{γ X G (U s) |X. X ∈ ivp_sols f U S t0 s}"

lemma g_orbital_eq: "g_orbital f G U S t0 s = 
  {X t |t X. t ∈ U s ∧ 𝒫 X (down (U s) t) ⊆ {s. G s} ∧ X ∈ Sols f U S t0 s }" 
  unfolding g_orbital_def ivp_sols_def g_orbit_eq by auto

lemma g_orbitalI:
  assumes "X ∈ Sols f U S t0 s"
    and "t ∈ U s" and "(𝒫 X (down (U s) t) ⊆ {s. G s})"
  shows "X t ∈ g_orbital f G U S t0 s"
  using assms unfolding g_orbital_eq(1) by auto

lemma g_orbitalD:
  assumes "s' ∈ g_orbital f G U S t0 s"
  obtains X and t where "X ∈ Sols f U S t0 s"
  and "X t = s'" and "t ∈ U s" and "(𝒫 X (down (U s) t) ⊆ {s. G s})"
  using assms unfolding g_orbital_def g_orbit_eq by auto

lemma "g_orbital f G U S t0 s = {X t |t X. X t ∈ γ X G (U s) ∧ X ∈ Sols f U S t0 s}"
  unfolding g_orbital_eq g_orbit_eq by auto

lemma "X ∈ Sols f U S t0 s ⟹ γ X G (U s) ⊆ g_orbital f G U S t0 s"
  unfolding g_orbital_eq g_orbit_eq by auto

lemma "g_orbital f G U S t0 s ⊆ g_orbital f (λs. True) U S t0 s"
  unfolding g_orbital_eq by auto

no_notation g_orbit (‹γ›)


subsection ‹ Differential Invariants ›

definition diff_invariant :: "('a ⇒ bool) ⇒ (real ⇒ ('a::real_normed_vector) ⇒ 'a) ⇒ 
  ('a ⇒ real set) ⇒ 'a set ⇒ real ⇒ ('a ⇒ bool) ⇒ bool" 
  where "diff_invariant I f U S t0 G ≡ (⋃ ∘ (𝒫 (g_orbital f G U S t0))) {s. I s} ⊆ {s. I s}"

lemma diff_invariant_eq: "diff_invariant I f U S t0 G = 
  (∀s. I s ⟶ (∀X∈Sols f U S t0 s. (∀t∈U s.(∀τ∈(down (U s) t). G (X τ)) ⟶ I (X t))))"
  unfolding diff_invariant_def g_orbital_eq image_le_pred by auto

lemma diff_inv_eq_inv_set:
  "diff_invariant I f U S t0 G = (∀s. I s ⟶ (g_orbital f G U S t0 s) ⊆ {s. I s})"
  unfolding diff_invariant_eq g_orbital_eq image_le_pred by auto

lemma "diff_invariant I f U S t0 (λs. True) ⟹ diff_invariant I f U S t0 G"
  unfolding diff_invariant_eq by auto

named_theorems diff_invariant_rules "rules for certifying differential invariants."

lemma diff_invariant_eq_rule [diff_invariant_rules]:
  assumes Uhyp: "⋀s. s ∈ S ⟹ is_interval (U s)"
    and dX: "⋀X. (D X = (λτ. f τ (X τ)) on U(X t0)) ⟹ (D (λτ. μ(X τ)-ν(X τ)) = ((*R) 0) on U(X t0))"
  shows "diff_invariant (λs. μ s = ν s) f U S t0 G"
proof(simp add: diff_invariant_eq ivp_sols_def, clarsimp)
  fix X t 
  assume xivp:"D X = (λτ. f τ (X τ)) on U (X t0)" "μ (X t0) = ν (X t0)" "X ∈ U (X t0) → S"
    and tHyp:"t ∈ U (X t0)" and t0Hyp: "t0 ∈ U (X t0)" 
  hence "{t0--t} ⊆ U (X t0)"
    using closed_segment_subset_interval[OF Uhyp t0Hyp tHyp] by blast
  hence "D (λτ. μ (X τ) - ν (X τ)) = (λτ. τ *R 0) on {t0--t}"
    using has_vderiv_on_subset[OF dX[OF xivp(1)]] by auto
  then obtain τ where "μ (X t) - ν (X t) - (μ (X t0) - ν (X t0)) = (t - t0) * τ *R 0"
    using mvt_very_simple_closed_segmentE by blast
  thus "μ (X t) = ν (X t)" 
    by (simp add: xivp(2))
qed

lemma diff_invariant_leq_rule [diff_invariant_rules]:
  fixes μ::"'a::banach ⇒ real"
  assumes Uhyp: "⋀s. s ∈ S ⟹ is_interval (U s)"
    and Gg: "⋀X. (D X = (λτ. f τ (X τ)) on U(X t0)) ⟹ (∀τ∈U(X t0). τ > t0 ⟶ G (X τ) ⟶ μ' (X τ) ≥ ν' (X τ))"
    and Gl: "⋀X. (D X = (λτ. f τ (X τ)) on U(X t0)) ⟹ (∀τ∈U(X t0). τ < t0 ⟶ μ' (X τ) ≤ ν' (X τ))"
    and dX: "⋀X. (D X = (λτ. f τ (X τ)) on U(X t0)) ⟹ D (λτ. μ(X τ)-ν(X τ)) = (λτ. μ'(X τ)-ν'(X τ)) on U(X t0)"
  shows "diff_invariant (λs. ν s ≤ μ s) f U S t0 G"
proof(simp_all add: diff_invariant_eq ivp_sols_def, safe)
  fix X t assume Ghyp: "∀τ. τ ∈ U (X t0) ∧ τ ≤ t ⟶ G (X τ)"
  assume xivp: "D X = (λx. f x (X x)) on U (X t0)" "ν (X t0) ≤ μ (X t0)" "X ∈ U (X t0) → S"
  assume tHyp: "t ∈ U (X t0)" and t0Hyp: "t0 ∈ U (X t0)" 
  hence obs1: "{t0--t} ⊆ U (X t0)" "{t0<--<t} ⊆ U (X t0)"
    using closed_segment_subset_interval[OF Uhyp t0Hyp tHyp] xivp(3) segment_open_subset_closed
    by (force, metis PiE ‹X t0 ∈ S ⟹ {t0--t} ⊆ U (X t0)› dual_order.trans)
  hence obs2: "D (λτ. μ (X τ) - ν (X τ)) = (λτ. μ' (X τ) - ν' (X τ)) on {t0--t}"
    using has_vderiv_on_subset[OF dX[OF xivp(1)]] by auto
  {assume "t ≠ t0"
    then obtain r where rHyp: "r ∈ {t0<--<t}" 
      and "(μ(X t)-ν(X t)) - (μ(X t0)-ν(X t0)) = (λτ. τ*(μ'(X r)-ν'(X r))) (t - t0)"
      using mvt_simple_closed_segmentE obs2 by blast
    hence mvt: "μ(X t)-ν(X t) = (t - t0)*(μ'(X r)-ν'(X r)) + (μ(X t0)-ν(X t0))"
      by force
    have primed: "⋀τ. τ ∈ U (X t0) ⟹ τ > t0 ⟹ G (X τ) ⟹ μ' (X τ) ≥ ν' (X τ)" 
      "⋀τ. τ ∈ U (X t0) ⟹ τ < t0 ⟹ μ' (X τ) ≤ ν' (X τ)"
      using Gg[OF xivp(1)] Gl[OF xivp(1)] by auto
    have "t > t0 ⟹ r > t0 ∧ G (X r)" "¬ t0 ≤ t ⟹ r < t0" "r ∈ U (X t0)"
      using ‹r ∈ {t0<--<t}› obs1 Ghyp
      unfolding open_segment_eq_real_ivl closed_segment_eq_real_ivl by auto
    moreover have "r > t0 ⟹ G (X r) ⟹ (μ'(X r)- ν'(X r)) ≥ 0" "r < t0 ⟹ (μ'(X r)-ν'(X r)) ≤ 0"
      using primed(1,2)[OF ‹r ∈ U (X t0)›] by auto
    ultimately have "(t - t0) * (μ'(X r)-ν'(X r)) ≥ 0"
      by (case_tac "t ≥ t0", force, auto simp: split_mult_pos_le)
    hence "(t - t0) * (μ'(X r)-ν'(X r)) + (μ(X t0)-ν(X t0)) ≥ 0"
      using xivp(2) by auto
    hence "ν (X t) ≤ μ (X t)"
      using mvt by simp}
  thus "ν (X t) ≤ μ (X t)"
    using xivp by blast
qed

lemma diff_invariant_less_rule [diff_invariant_rules]:
  fixes μ::"'a::banach ⇒ real"
  assumes Uhyp: "⋀s. s ∈ S ⟹ is_interval (U s)"
    and Gg: "⋀X. (D X = (λτ. f τ (X τ)) on U(X t0)) ⟹ (∀τ∈U(X t0). τ > t0 ⟶ G (X τ) ⟶ μ' (X τ) ≥ ν' (X τ))"
    and Gl: "⋀X. (D X = (λτ. f τ (X τ)) on U(X t0)) ⟹ (∀τ∈U(X t0). τ < t0 ⟶ μ' (X τ) ≤ ν' (X τ))"
    and dX: "⋀X. (D X = (λτ. f τ (X τ)) on U(X t0)) ⟹ D (λτ. μ(X τ)-ν(X τ)) = (λτ. μ'(X τ)-ν'(X τ)) on U(X t0)"
  shows "diff_invariant (λs. ν s < μ s) f U S t0 G"
proof(simp_all add: diff_invariant_eq ivp_sols_def, safe)
  fix X t assume Ghyp: "∀τ. τ ∈ U (X t0) ∧ τ ≤ t ⟶ G (X τ)"
  assume xivp: "D X = (λx. f x (X x)) on U (X t0)" "ν (X t0) < μ (X t0)" "X ∈ U (X t0) → S"
  assume tHyp: "t ∈ U (X t0)" and t0Hyp: "t0 ∈ U (X t0)" 
  hence obs1: "{t0--t} ⊆ U (X t0)" "{t0<--<t} ⊆ U (X t0)"
    using closed_segment_subset_interval[OF Uhyp t0Hyp tHyp] xivp(3) segment_open_subset_closed
    by (force, metis PiE ‹X t0 ∈ S ⟹ {t0--t} ⊆ U (X t0)› dual_order.trans)
  hence obs2: "D (λτ. μ (X τ) - ν (X τ)) = (λτ. μ' (X τ) - ν' (X τ)) on {t0--t}"
    using has_vderiv_on_subset[OF dX[OF xivp(1)]] by auto
  {assume "t ≠ t0"
    then obtain r where rHyp: "r ∈ {t0<--<t}" 
      and "(μ(X t)-ν(X t)) - (μ(X t0)-ν(X t0)) = (λτ. τ*(μ'(X r)-ν'(X r))) (t - t0)"
      using mvt_simple_closed_segmentE obs2 by blast
    hence mvt: "μ(X t)-ν(X t) = (t - t0)*(μ'(X r)-ν'(X r)) + (μ(X t0)-ν(X t0))"
      by force
    have primed: "⋀τ. τ ∈ U (X t0) ⟹ τ > t0 ⟹ G (X τ) ⟹ μ' (X τ) ≥ ν' (X τ)" 
      "⋀τ. τ ∈ U (X t0) ⟹ τ < t0 ⟹ μ' (X τ) ≤ ν' (X τ)"
      using Gg[OF xivp(1)] Gl[OF xivp(1)] by auto
    have "t > t0 ⟹ r > t0 ∧ G (X r)" "¬ t0 ≤ t ⟹ r < t0" "r ∈ U (X t0)"
      using ‹r ∈ {t0<--<t}› obs1 Ghyp
      unfolding open_segment_eq_real_ivl closed_segment_eq_real_ivl by auto
    moreover have "r > t0 ⟹ G (X r) ⟹ (μ'(X r)- ν'(X r)) ≥ 0" "r < t0 ⟹ (μ'(X r)-ν'(X r)) ≤ 0"
      using primed(1,2)[OF ‹r ∈ U (X t0)›] by auto
    ultimately have "(t - t0) * (μ'(X r)-ν'(X r)) ≥ 0"
      by (case_tac "t ≥ t0", force, auto simp: split_mult_pos_le)
    hence "(t - t0) * (μ'(X r)-ν'(X r)) + (μ(X t0)-ν(X t0)) > 0"
      using xivp(2) by auto
    hence "ν (X t) < μ (X t)"
      using mvt by simp}
  thus "ν (X t) < μ (X t)"
    using xivp by blast
qed

lemma diff_invariant_nleq_rule:
  fixes μ::"'a::banach ⇒ real"
  shows "diff_invariant (λs. ¬ ν s ≤ μ s) f U S t0 G ⟷ diff_invariant (λs. ν s > μ s) f U S t0 G"
  unfolding diff_invariant_eq apply safe
  by (clarsimp, erule_tac x=s in allE, simp, erule_tac x=X in ballE, force, force)+

lemma diff_invariant_neq_rule [diff_invariant_rules]:
  fixes μ::"'a::banach ⇒ real"
  assumes "diff_invariant (λs. ν s < μ s) f U S t0 G"
    and "diff_invariant (λs. ν s > μ s) f U S t0 G"
  shows "diff_invariant (λs. ν s ≠ μ s) f U S t0 G"
proof(unfold diff_invariant_eq, clarsimp)
  fix s::'a and X::"real ⇒ 'a" and t::real
  assume "ν s ≠ μ s" and Xhyp: "X ∈ Sols f U S t0 s" 
     and thyp: "t ∈ U s" and Ghyp: "∀τ. τ ∈ U s ∧ τ ≤ t ⟶ G (X τ)"
  hence "ν s < μ s ∨ ν s > μ s"
    by linarith
  moreover have "ν s < μ s ⟹ ν (X t) < μ (X t)"
    using assms(1) Xhyp thyp Ghyp unfolding diff_invariant_eq by auto
  moreover have "ν s > μ s ⟹ ν (X t) > μ (X t)"
    using assms(2) Xhyp thyp Ghyp unfolding diff_invariant_eq by auto
  ultimately show "ν (X t) = μ (X t) ⟹ False"
    by auto
qed

lemma diff_invariant_neq_rule_converse:
  fixes μ::"'a::banach ⇒ real"
  assumes Uhyp: "⋀s. s ∈ S ⟹ is_interval (U s)" "⋀s t. s ∈ S ⟹ t ∈ U s ⟹ t0 ≤ t"
    and conts: "⋀X. (D X = (λτ. f τ (X τ)) on U(X t0)) ⟹ continuous_on (𝒫 X (U (X t0))) ν"
      "⋀X. (D X = (λτ. f τ (X τ)) on U(X t0)) ⟹ continuous_on (𝒫 X (U (X t0))) μ"
    and dI:"diff_invariant (λs. ν s ≠ μ s) f U S t0 G"
  shows "diff_invariant (λs. ν s < μ s) f U S t0 G"
proof(unfold diff_invariant_eq ivp_sols_def, clarsimp)
  fix X t assume Ghyp: "∀τ. τ ∈ U (X t0) ∧ τ ≤ t ⟶ G (X τ)"
  assume xivp: "D X = (λx. f x (X x)) on U (X t0)" "ν (X t0) < μ (X t0)" "X ∈ U (X t0) → S"
  assume tHyp: "t ∈ U (X t0)" and t0Hyp: "t0 ∈ U (X t0)"
  hence "t0 ≤ t" and "μ (X t) ≠ ν (X t)"
    using xivp(3) Uhyp(2) apply force
    using dI tHyp xivp(2) Ghyp ivp_solsI[of X f U "X t0", OF xivp(1) _ xivp(3) t0Hyp]
    unfolding diff_invariant_eq by force
  moreover
  {assume ineq2:"ν (X t) > μ (X t)"
    note continuous_on_compose[OF vderiv_on_continuous_on[OF xivp(1)]]
    hence "continuous_on (U (X t0)) (ν ∘ X)" and "continuous_on (U (X t0)) (μ ∘ X)"
      using xivp(1) conts by blast+
    also have "{t0--t} ⊆ U (X t0)"
      using closed_segment_subset_interval[OF Uhyp(1) t0Hyp tHyp] xivp(3) t0Hyp by auto
    ultimately have "continuous_on {t0--t} (λτ. ν (X τ))" 
      and "continuous_on {t0--t} (λτ. μ (X τ))"
      using continuous_on_subset by auto
    then obtain τ where "τ ∈ {t0--t}" "μ (X τ) = ν (X τ)"
      using IVT_two_functions_real_ivl[OF _ _ xivp(2) ineq2] by force
    hence "∀r∈down (U (X t0)) τ. G (X r)" and "τ ∈ U (X t0)"
      using Ghyp ‹τ ∈ {t0--t}› ‹t0 ≤ t› ‹{t0--t} ⊆ U (X t0)› 
      by (auto simp: closed_segment_eq_real_ivl)
    hence "μ (X τ) ≠ ν (X τ)"
      using dI tHyp xivp(2) ivp_solsI[of X f U "X t0", OF xivp(1) _ xivp(3) t0Hyp]
      unfolding diff_invariant_eq by force
    hence "False"
      using ‹μ (X τ) = ν (X τ)› by blast}
  ultimately show "ν (X t) < μ (X t)"
    by fastforce
qed

lemma diff_invariant_conj_rule [diff_invariant_rules]:
  assumes "diff_invariant I1 f U S t0 G"
    and "diff_invariant I2 f U S t0 G"
  shows "diff_invariant (λs. I1 s ∧ I2 s) f U S t0 G"
  using assms unfolding diff_invariant_def by auto

lemma diff_invariant_disj_rule [diff_invariant_rules]:
  assumes "diff_invariant I1 f U S t0 G"
    and "diff_invariant I2 f U S t0 G"
  shows "diff_invariant (λs. I1 s ∨ I2 s) f U S t0 G"
  using assms unfolding diff_invariant_def by auto

subsection ‹ Picard-Lindeloef ›

text‹ A locale with the assumptions of Picard-Lindeloef's theorem. It extends 
@{term "ll_on_open_it"} by providing an initial time @{term "t0 ∈ T"}.›

locale picard_lindeloef =
  fixes f::"real ⇒ ('a::{heine_borel,banach}) ⇒ 'a" and T::"real set" and S::"'a set" and t0::real
  assumes open_domain: "open T" "open S"
    and interval_time: "is_interval T"
    and init_time: "t0 ∈ T"
    and cont_vec_field: "∀s ∈ S. continuous_on T (λt. f t s)"
    and lipschitz_vec_field: "local_lipschitz T S f"
begin

sublocale ll_on_open_it T f S t0
  by (unfold_locales) (auto simp: cont_vec_field lipschitz_vec_field interval_time open_domain) 

lemma ll_on_open: "ll_on_open T f S"
  using local.general.ll_on_open_axioms .

lemmas subintervalI = closed_segment_subset_domain
   and init_time_ex_ivl = existence_ivl_initial_time[OF init_time]
   and flow_at_init[simp] = general.flow_initial_time[OF init_time]
                               
abbreviation "ex_ivl s ≡ existence_ivl t0 s"

lemma flow_has_vderiv_on_ex_ivl:
  assumes "s ∈ S"
  shows "D flow t0 s = (λt. f t (flow t0 s t)) on ex_ivl s"
  using flow_usolves_ode[OF init_time ‹s ∈ S›] 
  unfolding usolves_ode_from_def solves_ode_def by blast

lemma flow_funcset_ex_ivl:
  assumes "s ∈ S"
  shows "flow t0 s ∈ ex_ivl s → S"
  using flow_usolves_ode[OF init_time ‹s ∈ S›] 
  unfolding usolves_ode_from_def solves_ode_def by blast

lemma flow_in_ivp_sols_ex_ivl:
  assumes "s ∈ S"
  shows "flow t0 s ∈ Sols f (λs. ex_ivl s) S t0 s"
  using flow_has_vderiv_on_ex_ivl[OF assms] apply(rule ivp_solsI)
    apply(simp_all add: init_time assms)
  by (rule flow_funcset_ex_ivl[OF assms])

lemma csols_eq: "csols t0 s = {(x, t). t ∈ T ∧  x ∈ Sols f (λs. {t0--t}) S t0 s}"
  unfolding ivp_sols_def csols_def solves_ode_def 
  using closed_segment_subset_domain init_time by auto

lemma subset_ex_ivlI:
  "Y1 ∈ Sols f (λs. T) S t0 s ⟹ {t0--t} ⊆ T ⟹ A ⊆ {t0--t} ⟹ A ⊆ ex_ivl s"
  apply(clarsimp simp: existence_ivl_def)
  apply(subgoal_tac "t0 ∈ T", clarsimp simp: csols_eq)
   apply(rule_tac x=Y1 in exI, rule_tac x=t in exI, safe, force)
  by (rule in_ivp_sols_subset[where T="λs. T"], auto)

lemma unique_solution: ― ‹ proved for a subset of T for general applications ›
  assumes "s ∈ S" and "t0 ∈ U" and "t ∈ U" 
    and "is_interval U" and "U ⊆ ex_ivl s" 
    and xivp: "D Y1 = (λt. f t (Y1 t)) on U" "Y1 t0 = s" "Y1 ∈ U → S"
    and yivp: "D Y2 = (λt. f t (Y2 t)) on U" "Y2 t0 = s" "Y2 ∈ U → S"
  shows "Y1 t = Y2 t"
proof-
  have "t0 ∈ T"
    using assms existence_ivl_subset by auto
  have key: "(flow t0 s usolves_ode f from t0) (ex_ivl s) S"
    using flow_usolves_ode[OF ‹t0 ∈ T› ‹s ∈ S›] .
  hence "∀t∈U. Y1 t = flow t0 s t"
    unfolding usolves_ode_from_def solves_ode_def apply safe
    by (erule_tac x=Y1 in allE, erule_tac x=U in allE, auto simp: assms)
  also have "∀t∈U. Y2 t = flow t0 s t"
    using key unfolding usolves_ode_from_def solves_ode_def apply safe
    by (erule_tac x=Y2 in allE, erule_tac x=U in allE, auto simp: assms)
  ultimately show "Y1 t = Y2 t"
    using assms by auto
qed

text ‹Applications of lemma @{text "unique_solution"}: ›

lemma unique_solution_closed_ivl:
  assumes xivp: "D X = (λt. f t (X t)) on {t0--t}" "X t0 = s" "X ∈ {t0--t} → S" and "t ∈ T"
    and yivp: "D Y = (λt. f t (Y t)) on {t0--t}" "Y t0 = s" "Y ∈ {t0--t} → S" and "s ∈ S" 
  shows "X t = Y t"
  apply(rule unique_solution[OF ‹s ∈ S›, of "{t0--t}"], simp_all add: assms)
  apply(unfold existence_ivl_def csols_eq ivp_sols_def, clarsimp)
  using xivp ‹t ∈ T› by blast

lemma solution_eq_flow:
  assumes xivp: "D X = (λt. f t (X t)) on ex_ivl s" "X t0 = s" "X ∈ ex_ivl s → S" 
    and "t ∈ ex_ivl s" and "s ∈ S" 
  shows "X t = flow t0 s t"
  apply(rule unique_solution[OF ‹s ∈ S› init_time_ex_ivl ‹t ∈ ex_ivl s›])
  using flow_has_vderiv_on_ex_ivl flow_funcset_ex_ivl ‹s ∈ S› by (auto simp: assms)

lemma ivp_unique_solution:
  assumes "s ∈ S" and ivl: "is_interval (U s)" and "U s ⊆ T" and "t ∈ U s" 
    and ivp1: "Y1 ∈ Sols f U S t0 s" and ivp2: "Y2 ∈ Sols f U S t0 s"
  shows "Y1 t = Y2 t"
proof(rule unique_solution[OF ‹s ∈ S›, of "{t0--t}"], simp_all)
  have "t0 ∈ U s"
    using ivp_solsD[OF ivp1] by auto
  hence obs0: "{t0--t} ⊆ U s"
    using closed_segment_subset_interval[OF ivl] ‹t ∈ U s› by blast
  moreover have obs1: "Y1 ∈ Sols f (λs. {t0--t}) S t0 s"
    by (rule in_ivp_sols_subset[OF _ calculation(1) ivp1], simp)
  moreover have obs2: "Y2 ∈ Sols f (λs. {t0--t}) S t0 s"
    by (rule in_ivp_sols_subset[OF _ calculation(1) ivp2], simp)
  ultimately show "{t0--t} ⊆ ex_ivl s"
    apply(unfold existence_ivl_def csols_eq, clarsimp)
    apply(rule_tac x=Y1 in exI, rule_tac x=t in exI)
    using ‹t ∈ U s› and ‹U s ⊆ T› by force
  show "D Y1 = (λt. f t (Y1 t)) on {t0--t}"
    by (rule ivp_solsD[OF in_ivp_sols_subset[OF _ _ ivp1]], simp_all add: obs0)
  show "D Y2 = (λt. f t (Y2 t)) on {t0--t}"
    by (rule ivp_solsD[OF in_ivp_sols_subset[OF _ _ ivp2]], simp_all add: obs0)
  show "Y1 t0 = s" and "Y2 t0 = s"
    using ivp_solsD[OF ivp1] ivp_solsD[OF ivp2] by auto
  show "Y1 ∈ {t0--t} → S" and "Y2 ∈ {t0--t} → S"
    using ivp_solsD[OF obs1] ivp_solsD[OF obs2] by auto
qed

lemma g_orbital_orbit:
  assumes "s ∈ S" and ivl: "is_interval (U s)" and "U s ⊆ T"
    and ivp: "Y ∈ Sols f U S t0 s"
  shows "g_orbital f G U S t0 s = g_orbit Y G (U s)"
proof-
  have eq1: "∀Z ∈ Sols f U S t0 s. ∀t∈U s. Z t = Y t"
    by (clarsimp, rule ivp_unique_solution[OF assms(1,2,3) _ _ ivp], auto)
  have "g_orbital f G U S t0 s ⊆ g_orbit (λt. Y t) G (U s)"
  proof
    fix x assume "x ∈ g_orbital f G U S t0 s"
    then obtain Z and t 
      where z_def: "x = Z t ∧ t ∈ U s ∧ (∀τ∈down (U s) t. G (Z τ)) ∧ Z ∈ Sols f U S t0 s"
      unfolding g_orbital_eq by auto
    hence "{t0--t} ⊆ U s"
      using closed_segment_subset_interval[OF ivl ivp_solsD(4)[OF ivp]] by blast
    hence "∀τ∈{t0--t}. Z τ = Y τ"
      using z_def apply clarsimp
      by (rule ivp_unique_solution[OF assms(1,2,3) _ _ ivp], auto)
    thus "x ∈ g_orbit Y G (U s)"
      using z_def eq1 unfolding g_orbit_eq by simp metis
  qed
  moreover have "g_orbit Y G (U s) ⊆ g_orbital f G U S t0 s"
    apply(unfold g_orbital_eq g_orbit_eq ivp_sols_def, clarsimp)
    apply(rule_tac x=t in exI, rule_tac x=Y in exI)
    using ivp_solsD[OF ivp] by auto
  ultimately show ?thesis
    by blast
qed

end

lemma local_lipschitz_add: 
  fixes f1 f2 :: "real ⇒ 'a::banach ⇒ 'a"
  assumes "local_lipschitz T S f1"
      and "local_lipschitz T S f2" 
    shows "local_lipschitz T S (λt s. f1 t s + f2 t s)"
proof(unfold local_lipschitz_def, clarsimp)
  fix s and t assume "s ∈ S" and "t ∈ T"
  obtain ε1 L1 where "ε1 > 0" and L1: "⋀τ. τ∈cball t ε1 ∩ T ⟹ L1-lipschitz_on (cball s ε1 ∩ S) (f1 τ)"
    using local_lipschitzE[OF assms(1) ‹t ∈ T› ‹s ∈ S›] by blast
  obtain ε2 L2 where "ε2 > 0" and L2: "⋀τ. τ∈cball t ε2 ∩ T ⟹ L2-lipschitz_on (cball s ε2 ∩ S) (f2 τ)"
    using local_lipschitzE[OF assms(2) ‹t ∈ T› ‹s ∈ S›] by blast
  have ballH: "cball s (min ε1 ε2) ∩ S ⊆ cball s ε1 ∩ S" "cball s (min ε1 ε2) ∩ S ⊆ cball s ε2 ∩ S"
    by auto
  have obs1: "∀τ∈cball t ε1 ∩ T. L1-lipschitz_on (cball s (min ε1 ε2) ∩ S) (f1 τ)"
    using lipschitz_on_subset[OF L1 ballH(1)] by blast
  also have obs2: "∀τ∈cball t ε2 ∩ T. L2-lipschitz_on (cball s (min ε1 ε2) ∩ S) (f2 τ)"
    using lipschitz_on_subset[OF L2 ballH(2)] by blast
  ultimately have "∀τ∈cball t (min ε1 ε2) ∩ T. 
    (L1 + L2)-lipschitz_on (cball s (min ε1 ε2) ∩ S) (λs. f1 τ s + f2 τ s)"
    using lipschitz_on_add by fastforce
  thus "∃u>0. ∃L. ∀t∈cball t u ∩ T. L-lipschitz_on (cball s u ∩ S) (λs. f1 t s + f2 t s)"
    apply(rule_tac x="min ε1 ε2" in exI)
    using ‹ε1 > 0› ‹ε2 > 0› by force
qed

lemma picard_lindeloef_add: "picard_lindeloef f1 T S t0 ⟹ picard_lindeloef f2 T S t0 ⟹ 
  picard_lindeloef (λt s. f1 t s + f2 t s) T S t0"
  unfolding picard_lindeloef_def apply(clarsimp, rule conjI)
  using continuous_on_add apply fastforce
  using local_lipschitz_add by blast

lemma picard_lindeloef_constant: "picard_lindeloef (λt s. c) UNIV UNIV t0"
  apply(unfold_locales, simp_all add: local_lipschitz_def lipschitz_on_def, clarsimp)
  by (rule_tac x=1 in exI, clarsimp, rule_tac x="1/2" in exI, simp)


subsection ‹ Flows for ODEs ›

text‹ A locale designed for verification of hybrid systems. The user can select the interval 
of existence and the defining flow equation via the variables @{term "T"} and @{term "φ"}.›

locale local_flow = picard_lindeloef "(λ t. f)" T S 0 
  for f::"'a::{heine_borel,banach} ⇒ 'a" and T S L +
  fixes φ :: "real ⇒ 'a ⇒ 'a"
  assumes ivp:
    "⋀ t s. t ∈ T ⟹ s ∈ S ⟹ D (λt. φ t s) = (λt. f (φ t s)) on {0--t}"
    "⋀ s. s ∈ S ⟹ φ 0 s = s"
    "⋀ t s. t ∈ T ⟹ s ∈ S ⟹ (λt. φ t s) ∈ {0--t} → S"
begin

lemma in_ivp_sols_ivl: 
  assumes "t ∈ T" "s ∈ S"
  shows "(λt. φ t s) ∈ Sols (λt. f) (λs. {0--t}) S 0 s"
  apply(rule ivp_solsI)
  using ivp assms by auto

lemma eq_solution_ivl:
  assumes xivp: "D X = (λt. f (X t)) on {0--t}" "X 0 = s" "X ∈ {0--t} → S" 
    and indom: "t ∈ T" "s ∈ S"
  shows "X t = φ t s"
  apply(rule unique_solution_closed_ivl[OF xivp ‹t ∈ T›])
  using ‹s ∈ S› ivp indom by auto

lemma ex_ivl_eq:
  assumes "s ∈ S"
  shows "ex_ivl s = T"
  using existence_ivl_subset[of s] apply safe
  unfolding existence_ivl_def csols_eq
  using in_ivp_sols_ivl[OF _ assms] by blast

lemma has_derivative_on_open1: 
  assumes  "t > 0" "t ∈ T" "s ∈ S"
  obtains B where "t ∈ B" and "open B" and "B ⊆ T"
    and "D (λτ. φ τ s) ↦ (λτ. τ *R f (φ t s)) at t within B" 
proof-
  obtain r::real where rHyp: "r > 0" "ball t r ⊆ T"
    using open_contains_ball_eq open_domain(1) ‹t ∈ T› by blast
  moreover have "t + r/2 > 0"
    using ‹r > 0› ‹t > 0› by auto
  moreover have "{0--t} ⊆ T" 
    using subintervalI[OF init_time ‹t ∈ T›] .
  ultimately have subs: "{0<--<t + r/2} ⊆ T"
    unfolding abs_le_eq abs_le_eq real_ivl_eqs[OF ‹t > 0›] real_ivl_eqs[OF ‹t + r/2 > 0›] 
    by clarify (case_tac "t < x", simp_all add: cball_def ball_def dist_norm subset_eq field_simps)
  have "t + r/2 ∈ T"
    using rHyp unfolding real_ivl_eqs[OF rHyp(1)] by (simp add: subset_eq)
  hence "{0--t + r/2} ⊆ T"
    using subintervalI[OF init_time] by blast
  hence "(D (λt. φ t s) = (λt. f (φ t s)) on {0--(t + r/2)})"
    using ivp(1)[OF _ ‹s ∈ S›] by auto
  hence vderiv: "(D (λt. φ t s) = (λt. f (φ t s)) on {0<--<t + r/2})"
    apply(rule has_vderiv_on_subset)
    unfolding real_ivl_eqs[OF ‹t + r/2 > 0›] by auto
  have "t ∈ {0<--<t + r/2}"
    unfolding real_ivl_eqs[OF ‹t + r/2 > 0›] using rHyp ‹t > 0› by simp
  moreover have "D (λτ. φ τ s) ↦ (λτ. τ *R f (φ t s)) (at t within {0<--<t + r/2})"
    using vderiv calculation unfolding has_vderiv_on_def has_vector_derivative_def by blast
  moreover have "open {0<--<t + r/2}"
    unfolding real_ivl_eqs[OF ‹t + r/2 > 0›] by simp
  ultimately show ?thesis
    using subs that by blast
qed

lemma has_derivative_on_open2: 
  assumes "t < 0" "t ∈ T" "s ∈ S"
  obtains B where "t ∈ B" and "open B" and "B ⊆ T"
    and "D (λτ. φ τ s) ↦ (λτ. τ *R f (φ t s)) at t within B" 
proof-
  obtain r::real where rHyp: "r > 0" "ball t r ⊆ T"
    using open_contains_ball_eq open_domain(1) ‹t ∈ T› by blast
  moreover have "t - r/2 < 0"
    using ‹r > 0› ‹t < 0› by auto
  moreover have "{0--t} ⊆ T" 
    using subintervalI[OF init_time ‹t ∈ T›] .
  ultimately have subs: "{0<--<t - r/2} ⊆ T"
    unfolding open_segment_eq_real_ivl closed_segment_eq_real_ivl
      real_ivl_eqs[OF rHyp(1)] by(auto simp: subset_eq)
  have "t - r/2 ∈ T"
    using rHyp unfolding real_ivl_eqs by (simp add: subset_eq)
  hence "{0--t - r/2} ⊆ T"
    using subintervalI[OF init_time] by blast
  hence "(D (λt. φ t s) = (λt. f (φ t s)) on {0--(t - r/2)})"
    using ivp(1)[OF _ ‹s ∈ S›] by auto
  hence vderiv: "(D (λt. φ t s) = (λt. f (φ t s)) on {0<--<t - r/2})"
    apply(rule has_vderiv_on_subset)
    unfolding open_segment_eq_real_ivl closed_segment_eq_real_ivl by auto
  have "t ∈ {0<--<t - r/2}"
    unfolding open_segment_eq_real_ivl using rHyp ‹t < 0› by simp
  moreover have "D (λτ. φ τ s) ↦ (λτ. τ *R f (φ t s)) (at t within {0<--<t - r/2})"
    using vderiv calculation unfolding has_vderiv_on_def has_vector_derivative_def by blast
  moreover have "open {0<--<t - r/2}"
    unfolding open_segment_eq_real_ivl by simp
  ultimately show ?thesis
    using subs that by blast
qed

lemma has_derivative_on_open3: 
  assumes "s ∈ S"
  obtains B where "0 ∈ B" and "open B" and "B ⊆ T"
    and "D (λτ. φ τ s) ↦ (λτ. τ *R f (φ 0 s)) at 0 within B" 
proof-
  obtain r::real where rHyp: "r > 0" "ball 0 r ⊆ T"
    using open_contains_ball_eq open_domain(1) init_time by blast
  hence "r/2 ∈ T" "-r/2 ∈ T" "r/2 > 0"
    unfolding real_ivl_eqs by auto
  hence subs: "{0--r/2} ⊆ T" "{0--(-r/2)} ⊆ T"
    using subintervalI[OF init_time] by auto
  hence "(D (λt. φ t s) = (λt. f (φ t s)) on {0--r/2})"
    "(D (λt. φ t s) = (λt. f (φ t s)) on {0--(-r/2)})"
    using ivp(1)[OF _ ‹s ∈ S›] by auto
  also have "{0--r/2} = {0--r/2} ∪ closure {0--r/2} ∩ closure {0--(-r/2)}"
    "{0--(-r/2)} = {0--(-r/2)} ∪ closure {0--r/2} ∩ closure {0--(-r/2)}"
    unfolding closed_segment_eq_real_ivl ‹r/2 > 0› by auto
  ultimately have vderivs:
    "(D (λt. φ t s) = (λt. f (φ t s)) on {0--r/2} ∪ closure {0--r/2} ∩ closure {0--(-r/2)})"
    "(D (λt. φ t s) = (λt. f (φ t s)) on {0--(-r/2)} ∪ closure {0--r/2} ∩ closure {0--(-r/2)})"
    unfolding closed_segment_eq_real_ivl ‹r/2 > 0› by auto
  have obs: "0 ∈ {-r/2<--<r/2}"
    unfolding open_segment_eq_real_ivl using ‹r/2 > 0› by auto
  have union: "{-r/2--r/2} = {0--r/2} ∪ {0--(-r/2)}"
    unfolding closed_segment_eq_real_ivl by auto
  hence "(D (λt. φ t s) = (λt. f (φ t s)) on {-r/2--r/2})"
    using has_vderiv_on_union[OF vderivs] by simp
  hence "(D (λt. φ t s) = (λt. f (φ t s)) on {-r/2<--<r/2})"
    using has_vderiv_on_subset[OF _ segment_open_subset_closed[of "-r/2" "r/2"]] by auto
  hence "D (λτ. φ τ s) ↦ (λτ. τ *R f (φ 0 s)) (at 0 within {-r/2<--<r/2})"
    unfolding has_vderiv_on_def has_vector_derivative_def using obs by blast
  moreover have "open {-r/2<--<r/2}"
    unfolding open_segment_eq_real_ivl by simp
  moreover have "{-r/2<--<r/2} ⊆ T"
    using subs union segment_open_subset_closed by blast 
  ultimately show ?thesis
    using obs that by blast
qed

lemma has_derivative_on_open: 
  assumes "t ∈ T" "s ∈ S"
  obtains B where "t ∈ B" and "open B" and "B ⊆ T"
    and "D (λτ. φ τ s) ↦ (λτ. τ *R f (φ t s)) at t within B" 
  apply(subgoal_tac "t < 0 ∨ t = 0 ∨ t > 0")
  using has_derivative_on_open1[OF _ assms] has_derivative_on_open2[OF _ assms]
    has_derivative_on_open3[OF ‹s ∈ S›] by blast force

lemma in_domain:
  assumes "s ∈ S"
  shows "(λt. φ t s) ∈ T → S"
  using ivp(3)[OF _ assms] by blast

lemma has_vderiv_on_domain:
  assumes "s ∈ S"
  shows "D (λt. φ t s) = (λt. f (φ t s)) on T"
proof(unfold has_vderiv_on_def has_vector_derivative_def, clarsimp)
  fix t assume "t ∈ T"
  then obtain B where "t ∈ B" and "open B" and "B ⊆ T" 
    and Dhyp: "D (λt. φ t s) ↦ (λτ. τ *R f (φ t s)) at t within B"
    using assms has_derivative_on_open[OF ‹t ∈ T›] by blast
  hence "t ∈ interior B"
    using interior_eq by auto
  thus "D (λt. φ t s) ↦ (λτ. τ *R f (φ t s)) at t within T"
    using has_derivative_at_within_mono[OF _ ‹B ⊆ T› Dhyp] by blast
qed

lemma in_ivp_sols: 
  assumes "s ∈ S" and "0 ∈ U s" and "U s ⊆ T"
  shows "(λt. φ t s) ∈ Sols (λt. f) U S 0 s"
  apply(rule in_ivp_sols_subset[OF _ _ ivp_solsI, of _ _ _ "λs. T"])
  using  ivp(2)[OF ‹s ∈ S›] has_vderiv_on_domain[OF ‹s ∈ S›] 
    in_domain[OF ‹s ∈ S›] assms by auto

lemma eq_solution:
  assumes "s ∈ S" and "is_interval (U s)" and "U s ⊆ T" and "t ∈ U s"
    and xivp: "X ∈ Sols (λt. f) U S 0 s"
  shows "X t = φ t s"
  apply(rule ivp_unique_solution[OF assms], rule in_ivp_sols)
  by (simp_all add: ivp_solsD(4)[OF xivp] assms)

lemma ivp_sols_collapse: 
  assumes "T = UNIV" and "s ∈ S"
  shows "Sols (λt. f) (λs. T) S 0 s = {(λt. φ t s)}"
  apply (safe, simp_all add: fun_eq_iff, clarsimp)
   apply(rule eq_solution[of _ "λs. T"]; simp add: assms)
  by (rule in_ivp_sols; simp add: assms)

lemma additive_in_ivp_sols:
  assumes "s ∈ S" and "𝒫 (λτ. τ + t) T ⊆ T"
  shows "(λτ. φ (τ + t) s) ∈ Sols (λt. f) (λs. T) S 0 (φ (0 + t) s)"
  apply(rule ivp_solsI[OF vderiv_on_composeI])
       apply(rule has_vderiv_on_subset[OF has_vderiv_on_domain])
  using in_domain assms init_time by (auto intro!: poly_derivatives)

lemma is_monoid_action:
  assumes "s ∈ S" and "T = UNIV"
  shows "φ 0 s = s" and "φ (t1 + t2) s = φ t1 (φ t2 s)"
proof-
  show "φ 0 s = s"
    using ivp assms by simp
  have "φ (0 + t2) s = φ t2 s" 
    by simp
  also have "φ (0 + t2) s ∈ S"
    using in_domain assms by auto
  ultimately show "φ (t1 + t2) s = φ t1 (φ t2 s)"
    using eq_solution[OF _ _ _ _ additive_in_ivp_sols] assms by auto
qed

lemma g_orbital_collapses: 
  assumes "s ∈ S" and "is_interval (U s)" and "U s ⊆ T" and "0 ∈ U s"
  shows "g_orbital (λt. f) G U S 0 s = {φ t s| t. t ∈ U s ∧ (∀τ∈down (U s) t. G (φ τ s))}"
  apply (subst g_orbital_orbit[of _ _ "λt. φ t s"], simp_all add: assms g_orbit_eq)
  by (rule in_ivp_sols, simp_all add: assms)

definition orbit :: "'a ⇒ 'a set" (‹γφ›)
  where "γφ s = g_orbital (λt. f) (λs. True) (λs. T) S 0 s"

lemma orbit_eq: 
  assumes "s ∈ S"
  shows "γφ s = {φ t s| t. t ∈ T}"
  apply(unfold orbit_def, subst g_orbital_collapses)
  by (simp_all add: assms init_time interval_time)

lemma true_g_orbit_eq:
  assumes "s ∈ S"
  shows "g_orbit (λt. φ t s) (λs. True) T = γφ s"
  unfolding g_orbit_eq orbit_eq[OF assms] by simp

end

lemma line_is_local_flow: 
  "0 ∈ T ⟹ is_interval T ⟹ open T ⟹ local_flow (λ s. c) T UNIV (λ t s. s + t *R c)"
  apply(unfold_locales, simp_all add: local_lipschitz_def lipschitz_on_def, clarsimp)
   apply(rule_tac x=1 in exI, clarsimp, rule_tac x="1/2" in exI, simp)
  apply(rule_tac f'1="λ s. 0" and g'1="λ s. c" in has_vderiv_on_add[THEN has_vderiv_on_eq_rhs])
    apply(rule derivative_intros, simp)+
  by simp_all

end