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}) = (xA. 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  (XSols f U S t0 s. (tU 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 "rdown (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 "tU. 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 "tU. 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. tU 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. tcball 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