Session Hybrid_Systems_VCs

Theory HS_Preliminaries

(*  Title:       Preliminaries for hybrid systems verification
    Author:      Jonathan Julián Huerta y Munive, 2020
    Maintainer:  Jonathan Julián Huerta y Munive <jonjulian23@gmail.com>
*)

section ‹ Hybrid Systems Preliminaries ›

text ‹Hybrid systems combine continuous dynamics with discrete control. This section contains
auxiliary lemmas for verification of hybrid systems.›

theory HS_Preliminaries
  imports "Ordinary_Differential_Equations.Picard_Lindeloef_Qualitative"
begin

― ‹ Syntax ›

no_notation has_vderiv_on (infix "(has'_vderiv'_on)" 50)

notation has_derivative ("(1(D _  (_))/ _)" [65,65] 61)
     and has_vderiv_on ("(1 D _ = (_)/ on _)" [65,65] 61)
     and norm ("(1_)" [65] 61)

subsection ‹ Real numbers ›

lemma abs_le_eq:
  shows "(r::real) > 0  (¦x¦ < r) = (-r < x  x < r)"
    and "(r::real) > 0  (¦x¦  r) = (-r  x  x  r)"
  by linarith+

lemma real_ivl_eqs:
  assumes "0 < r"
  shows "ball x r = {x-r<--< x+r}"         and "{x-r<--< x+r} = {x-r<..< x+r}"
    and "ball (r / 2) (r / 2) = {0<--<r}"  and "{0<--<r} = {0<..<r}"
    and "ball 0 r = {-r<--<r}"             and "{-r<--<r} = {-r<..<r}"
    and "cball x r = {x-r--x+r}"           and "{x-r--x+r} = {x-r..x+r}"
    and "cball (r / 2) (r / 2) = {0--r}"   and "{0--r} = {0..r}"
    and "cball 0 r = {-r--r}"              and "{-r--r} = {-r..r}"
  unfolding open_segment_eq_real_ivl closed_segment_eq_real_ivl
  using assms by (auto simp: cball_def ball_def dist_norm field_simps)

lemma is_interval_real_nonneg[simp]: "is_interval (Collect ((≤) (0::real)))"
  by (auto simp: is_interval_def)

lemma norm_rotate_eq[simp]:
  fixes x :: "'a:: {banach,real_normed_field}"
  shows "(x * cos t - y * sin t)2 + (x * sin t + y * cos t)2 = x2 + y2"
    and "(x * cos t + y * sin t)2 + (y * cos t - x * sin t)2 = x2 + y2"
proof-
  have "(x * cos t - y * sin t)2 = x2 * (cos t)2 + y2 * (sin t)2 - 2 * (x * cos t) * (y * sin t)"
    by(simp add: power2_diff power_mult_distrib)
  also have "(x * sin t + y * cos t)2 = y2 * (cos t)2 + x2 * (sin t)2 + 2 * (x * cos t) * (y * sin t)"
    by(simp add: power2_sum power_mult_distrib)
  ultimately show "(x * cos t - y * sin t)2 + (x * sin t + y * cos t)2 = x2 + y2"
    by (simp add: Groups.mult_ac(2) Groups.mult_ac(3) right_diff_distrib sin_squared_eq)
  thus "(x * cos t + y * sin t)2 + (y * cos t - x * sin t)2 = x2 + y2"
    by (simp add: add.commute add.left_commute power2_diff power2_sum)
qed


subsection ‹ Single variable derivatives ›

named_theorems poly_derivatives "compilation of optimised miscellaneous derivative rules."

declare has_vderiv_on_const [poly_derivatives]
    and has_vderiv_on_id [poly_derivatives]
    and has_vderiv_on_add[THEN has_vderiv_on_eq_rhs, poly_derivatives]
    and has_vderiv_on_diff[THEN has_vderiv_on_eq_rhs, poly_derivatives]
    and has_vderiv_on_mult[THEN has_vderiv_on_eq_rhs, poly_derivatives]
    and has_vderiv_on_ln[poly_derivatives]

lemma vderiv_on_composeI:
  assumes "D f = f' on g ` T" 
    and " D g = g' on T"
    and "h = (λt. g' t *R f' (g t))"
  shows "D (λt. f (g t)) = h on T"
  apply(subst ssubst[of h], simp)
  using assms has_vderiv_on_compose by auto

lemma vderiv_uminusI[poly_derivatives]:
  "D f = f' on T  g = (λt. - f' t)  D (λt. - f t) = g on T"
  using has_vderiv_on_uminus by auto

lemma vderiv_npowI[poly_derivatives]:
  fixes f::"real  real"
  assumes "n  1" and "D f = f' on T" and "g = (λt. n * (f' t) * (f t)^(n-1))"
  shows "D (λt. (f t)^n) = g on T"
  using assms unfolding has_vderiv_on_def has_vector_derivative_def 
  by (auto intro: derivative_eq_intros simp: field_simps)

lemma vderiv_divI[poly_derivatives]:
  assumes "tT. g t  (0::real)" and "D f = f' on T"and "D g = g' on T" 
    and "h = (λt. (f' t * g t - f t * (g' t)) / (g t)^2)"
  shows "D (λt. (f t)/(g t)) = h on T"
  apply(subgoal_tac "(λt. (f t)/(g t)) = (λt. (f t) * (1/(g t)))")
   apply(erule ssubst, rule poly_derivatives(5)[OF assms(2)])
  apply(rule vderiv_on_composeI[where g=g and f="λt. 1/t" and f'="λt. - 1/t^2", OF _ assms(3)])
  apply(subst has_vderiv_on_def, subst has_vector_derivative_def, clarsimp)
   using assms(1) apply(force intro!: derivative_eq_intros simp: fun_eq_iff power2_eq_square)
   using assms by (auto simp: field_simps power2_eq_square)

lemma vderiv_cosI[poly_derivatives]:
  assumes "D (f::real  real) = f' on T" and "g = (λt. - (f' t) * sin (f t))"
  shows "D (λt. cos (f t)) = g on T"
  apply(rule vderiv_on_composeI[OF _ assms(1), of "λt. cos t"])
  unfolding has_vderiv_on_def has_vector_derivative_def 
  by (auto intro!: derivative_eq_intros simp: assms)

lemma vderiv_sinI[poly_derivatives]:
  assumes "D (f::real  real) = f' on T" and "g = (λt. (f' t) * cos (f t))"
  shows "D (λt. sin (f t)) = g on T"
  apply(rule vderiv_on_composeI[OF _ assms(1), of "λt. sin t"])
  unfolding has_vderiv_on_def has_vector_derivative_def 
  by (auto intro!: derivative_eq_intros simp: assms)

lemma vderiv_expI[poly_derivatives]:
  assumes "D (f::real  real) = f' on T" and "g = (λt. (f' t) * exp (f t))"
  shows "D (λt. exp (f t)) = g on T"
  apply(rule vderiv_on_composeI[OF _ assms(1), of "λt. exp t"])
  unfolding has_vderiv_on_def has_vector_derivative_def 
  by (auto intro!: derivative_eq_intros simp: assms)

― ‹Examples for checking derivatives›

lemma "D (*) a = (λt. a) on T"
  by (auto intro!: poly_derivatives)

lemma "a  0  D (λt. t/a) = (λt. 1/a) on T"
  by (auto intro!: poly_derivatives simp: power2_eq_square)

lemma "(a::real)  0  D f = f' on T  g = (λt. (f' t)/a)  D (λt. (f t)/a) = g on T"
  by (auto intro!: poly_derivatives simp: power2_eq_square)

lemma "tT. f t  (0::real)  D f = f' on T  g = (λt. - a * f' t / (f t)^2)  
  D (λt. a/(f t)) = g on T"
  by (auto intro!: poly_derivatives simp: power2_eq_square)

lemma "D (λt. a * t2 / 2 + v * t + x) = (λt. a * t + v) on T"
  by(auto intro!: poly_derivatives)

lemma "D (λt. v * t - a * t2 / 2 + x) = (λx. v - a * x) on T"
  by(auto intro!: poly_derivatives)

lemma "D x = x' on (λτ. τ + t) ` T  D (λτ. x (τ + t)) = (λτ. x' (τ + t)) on T"
  by (rule vderiv_on_composeI, auto intro: poly_derivatives)

lemma "a  0  D (λt. t/a) = (λt. 1/a) on T"
  by (auto intro!: poly_derivatives simp: power2_eq_square)

lemma "c  0  D (λt. a5 * t^5 + a3 * (t^3 / c) - a2 * exp (t^2) + a1 * cos t + a0) = 
  (λt. 5 * a5 * t^4 + 3 * a3 * (t^2 / c) - 2 * a2 * t * exp (t^2) - a1 * sin t) on T"
  by(auto intro!: poly_derivatives simp: power2_eq_square)

lemma "c  0  D (λt. - a3 * exp (t^3 / c) + a1 * sin t + a2 * t^2) = 
  (λt. a1 * cos t + 2 * a2 * t - 3 * a3 * t^2 / c * exp (t^3 / c)) on T"
  by(auto intro!: poly_derivatives simp: power2_eq_square)

lemma "c  0  D (λt. exp (a * sin (cos (t^4) / c))) = 
  (λt. - 4 * a * t^3 * sin (t^4) / c * cos (cos (t^4) / c) * exp (a * sin (cos (t^4) / c))) on T"
  by (intro poly_derivatives) (auto intro!: poly_derivatives simp: power2_eq_square)


subsection ‹ Intermediate Value Theorem ›

lemma IVT_two_functions:
  fixes f :: "('a::{linear_continuum_topology, real_vector})  
  ('b::{linorder_topology,real_normed_vector,ordered_ab_group_add})"
  assumes conts: "continuous_on {a..b} f" "continuous_on {a..b} g"
      and ahyp: "f a < g a" and bhyp: "g b < f b " and "a  b"
    shows "x{a..b}. f x = g x"
proof-
  let "?h x" = "f x - g x"
  have "?h a  0" and "?h b  0"
    using ahyp bhyp by simp_all
  also have "continuous_on {a..b} ?h"
    using conts continuous_on_diff by blast 
  ultimately obtain x where "a  x" "x  b" and "?h x = 0"
    using IVT'[of "?h"] a  b by blast
  thus ?thesis
    using a  b by auto
qed

lemma IVT_two_functions_real_ivl:
  fixes f :: "real  real"
  assumes conts: "continuous_on {a--b} f" "continuous_on {a--b} g"
      and ahyp: "f a < g a" and bhyp: "g b < f b "
    shows "x{a--b}. f x = g x"
proof(cases "a  b")
  case True
  then show ?thesis 
    using IVT_two_functions assms 
    unfolding closed_segment_eq_real_ivl by auto
next
  case False
  hence "a  b"
    by auto
  hence "continuous_on {b..a} f" "continuous_on {b..a} g"
    using conts False unfolding closed_segment_eq_real_ivl by auto
  hence "x{b..a}. g x = f x"
    using IVT_two_functions[of b a g f] assms(3,4) False by auto
  then show ?thesis  
    using a  b unfolding closed_segment_eq_real_ivl by auto force
qed


subsection ‹ Filters ›

lemma eventually_at_within_mono:
  assumes "t  interior T" and "T  S"
    and "eventually P (at t within T)"
  shows "eventually P (at t within S)"
  by (meson assms eventually_within_interior interior_mono subsetD)

lemma netlimit_at_within_mono:
  fixes t::"'a::{perfect_space,t2_space}"
  assumes "t  interior T" and "T  S"
  shows "netlimit (at t within S) = t"
  using assms(1) interior_mono[OF T  S] netlimit_within_interior by auto

lemma has_derivative_at_within_mono:
  assumes "(t::real)  interior T" and "T  S"
    and "D f  f' at t within T"
  shows "D f  f' at t within S"
  using assms(3) apply(unfold has_derivative_def tendsto_iff, safe)
  unfolding netlimit_at_within_mono[OF assms(1,2)] netlimit_within_interior[OF assms(1)]
  by (rule eventually_at_within_mono[OF assms(1,2)]) simp

lemma eventually_all_finite2:
  fixes P :: "('a::finite)  'b  bool"
  assumes h:"i. eventually (P i) F"
  shows "eventually (λx. i. P i x) F"
proof(unfold eventually_def)
  let ?F = "Rep_filter F"
  have obs: "i. ?F (P i)"
    using h by auto
  have "?F (λx. i  UNIV. P i x)"
    apply(rule finite_induct)
    by(auto intro: eventually_conj simp: obs h)
  thus "?F (λx. i. P i x)"
    by simp
qed

lemma eventually_all_finite_mono:
  fixes P :: "('a::finite)  'b  bool"
  assumes h1: "i. eventually (P i) F"
      and h2: "x. (i. (P i x))  Q x"
  shows "eventually Q F"
proof-
  have "eventually (λx. i. P i x) F"
    using h1 eventually_all_finite2 by blast
  thus "eventually Q F"
    unfolding eventually_def
    using h2 eventually_mono by auto
qed


subsection ‹ Multivariable derivatives ›

definition vec_upd :: "('a^'b)  'b  'a  'a^'b"
  where "vec_upd s i a = (χ j. ((($) s)(i := a)) j)"

lemma vec_upd_eq: "vec_upd s i a = (χ j. if j = i then a else s$j)"
  by (simp add: vec_upd_def)

lemma frechet_vec_lambda:
  fixes f::"real  ('a::banach)^('m::finite)" and x::real and T::"real set"
  defines "x0  netlimit (at x within T)" and "m  real CARD('m)"
  assumes "i. ((λy. (f y $ i - f x0 $ i - (y - x0) *R f' x $ i) /R (y - x0))  0) (at x within T)"
  shows "((λy. (f y - f x0 - (y - x0) *R f' x) /R (y - x0))  0) (at x within T)"
proof(simp add: tendsto_iff, clarify)
  fix ε::real assume "0 < ε"
  let "" = "λy. y - x0" and "?Δf" = "λy. f y - f x0"
  let "?P" = "λi e y. inverse ¦ y¦ * (f y $ i - f x0 $ i -  y *R f' x $ i) < e"
    and "?Q" = "λy. inverse ¦ y¦ * (?Δf y -  y *R f' x) < ε"
  have "0 < ε / sqrt m"
    using 0 < ε by (auto simp: assms)
  hence "i. eventually (λy. ?P i (ε / sqrt m) y) (at x within T)"
    using assms unfolding tendsto_iff by simp
  thus "eventually ?Q (at x within T)"
  proof(rule eventually_all_finite_mono, simp add: norm_vec_def L2_set_def, clarify)
    fix t::real
    let ?c = "inverse ¦t - x0¦" and "?u t" = "λi. f t $ i - f x0 $ i -  t *R f' x $ i"
    assume hyp:"i. ?c * (?u t i) < ε / sqrt m"
    hence "i. (?c *R (?u t i))2 < (ε / sqrt m)2"
      by (simp add: power_strict_mono)
    hence "i. ?c2 * ((?u t i))2 < ε2 / m"
      by (simp add: power_mult_distrib power_divide assms)
    hence "i. ?c2 * ((?u t i))2 < ε2 / m"
      by (auto simp: assms)
    also have "({}::'m set)  UNIV  finite (UNIV :: 'm set)"
      by simp
    ultimately have "(iUNIV. ?c2 * ((?u t i))2) < ((i::'m)UNIV. ε2 / m)"
      by (metis (lifting) sum_strict_mono)
    moreover have "?c2 * (iUNIV. (?u t i)2) = (iUNIV. ?c2 *  (?u t i)2)"
      using sum_distrib_left by blast
    ultimately have "?c2 * (iUNIV. (?u t i)2) < ε2"
      by (simp add: assms)
    hence "sqrt (?c2 * (iUNIV. (?u t i)2)) < sqrt (ε2)"
      using real_sqrt_less_iff by blast
    also have "... = ε"
      using 0 < ε by auto
    moreover have "?c * sqrt (iUNIV. (?u t i)2) = sqrt (?c2 * (iUNIV. (?u t i)2))"
      by (simp add: real_sqrt_mult)
    ultimately show "?c * sqrt (iUNIV. (?u t i)2) < ε"
      by simp
  qed
qed

lemma tendsto_norm_bound:
  "x. G x - L  F x - L  (F  L) net  (G  L) net"
  apply(unfold tendsto_iff dist_norm, clarsimp)
  apply(rule_tac P="λx. F x - L < e" in eventually_mono, simp)
  by (rename_tac e z) (erule_tac x=z in allE, simp)

lemma tendsto_zero_norm_bound:
  "x. G x  F x  (F  0) net  (G  0) net"
  apply(unfold tendsto_iff dist_norm, clarsimp)
  apply(rule_tac P="λx. F x < e" in eventually_mono, simp)
  by (rename_tac e z) (erule_tac x=z in allE, simp)

lemma frechet_vec_nth:
  fixes f::"real  ('a::real_normed_vector)^'m"
  assumes "((λx. (f x - f x0 - (x - x0) *R f' t) /R (x - x0))  0) (at t within T)"
  shows "((λx. (f x $ i - f x0 $ i - (x - x0) *R f' t $ i) /R (x - x0))  0) (at t within T)"
  apply(rule_tac F="(λx. (f x - f x0 - (x - x0) *R f' t) /R (x - x0))" in tendsto_zero_norm_bound)
   apply(clarsimp, rule mult_left_mono)
    apply (metis Finite_Cartesian_Product.norm_nth_le vector_minus_component vector_scaleR_component)
  using assms by simp_all

lemma has_derivative_vec_lambda:
  fixes f::"real  ('a::banach)^('n::finite)"
  assumes "i. D (λt. f t $ i)  (λ h. h *R f' x $ i) (at x within T)"
  shows "D f  (λh. h *R f' x) at x within T"
  apply(unfold has_derivative_def, safe)
   apply(force simp: bounded_linear_def bounded_linear_axioms_def)
  using assms frechet_vec_lambda[of x T ] unfolding has_derivative_def by auto

lemma has_derivative_vec_nth:
  assumes "D f  (λh. h *R f' x) at x within T"
  shows "D (λt. f t $ i)  (λh. h *R f' x $ i) at x within T"
  apply(unfold has_derivative_def, safe)
   apply(force simp: bounded_linear_def bounded_linear_axioms_def)
  using frechet_vec_nth assms unfolding has_derivative_def by auto

lemma has_vderiv_on_vec_eq[simp]:
  fixes x::"real  ('a::banach)^('n::finite)"
  shows "(D x = x' on T) = (i. D (λt. x t $ i) = (λt. x' t $ i) on T)"
  unfolding has_vderiv_on_def has_vector_derivative_def apply safe
  using has_derivative_vec_nth has_derivative_vec_lambda by blast+

end

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

Theory HS_VC_Spartan

(*  Title:       Verification components for hybrid systems 
    Author:      Jonathan Julián Huerta y Munive, 2020
    Maintainer:  Jonathan Julián Huerta y Munive <jonjulian23@gmail.com>
*)

section ‹ Verification components for hybrid systems ›

text ‹ A light-weight version of the verification components. We define the forward box 
operator to compute weakest liberal preconditions (wlps) of hybrid programs. Then we 
introduce three methods for verifying correctness specifications of the continuous 
dynamics of a HS. ›

theory HS_VC_Spartan
  imports HS_ODEs
                        
begin

type_synonym 'a pred = "'a  bool"

no_notation Transitive_Closure.rtrancl ("(_*)" [1000] 999)

notation Union ("μ")
     and g_orbital ("(1x´=_ & _ on _ _ @ _)")


subsection ‹Verification of regular programs›

text ‹ Lemmas for verification condition generation ›

definition fbox :: "('a  'b set)  'b pred  'a pred" ("|_] _" [61,81] 82)
  where "|F] P = (λs. (s'. s'  F s  P s'))"

lemma fbox_iso: "P  Q  |F] P  |F] Q"
  unfolding fbox_def by auto

lemma fbox_anti: "s. F1 s  F2 s  |F2] P  |F1] P"
  unfolding fbox_def by auto

lemma fbox_invariants: 
  assumes "I  |F] I" and "J  |F] J"
  shows "(λs. I s  J s)  |F] (λs. I s  J s)"
    and "(λs. I s  J s)  |F] (λs. I s  J s)"
  using assms unfolding fbox_def by auto

― ‹ Skip ›

abbreviation "skip  (λs. {s})"

lemma fbox_eta[simp]: "fbox skip P = P"
  unfolding fbox_def by simp

― ‹ Tests ›

definition test :: "'a pred  'a  'a set" ("(1¿_?)")
  where "¿P? = (λs. {x. x = s  P x})"

lemma fbox_test[simp]: "(λs. ( |¿P?] Q) s) = (λs. P s  Q s)"
  unfolding fbox_def test_def by simp

― ‹ Assignments ›

definition vec_upd :: "'a^'n  'n  'a  'a^'n"
  where "vec_upd s i a = (χ j. ((($) s)(i := a)) j)"

lemma vec_upd_eq: "vec_upd s i a = (χ j. if j = i then a else s$j)"
  by (simp add: vec_upd_def)

definition assign :: "'n  ('a^'n  'a)  'a^'n  ('a^'n) set" ("(2_ ::= _)" [70, 65] 61) 
  where "(x ::= e) = (λs. {vec_upd s x (e s)})" 

lemma fbox_assign[simp]: "|x ::= e] Q = (λs. Q (χ j. ((($) s)(x := (e s))) j))"
  unfolding vec_upd_def assign_def by (subst fbox_def) simp

― ‹ Nondeterministic assignments ›

definition nondet_assign :: "'n  'a^'n  ('a^'n) set" ("(2_ ::= ? )" [70] 61)
  where "(x ::= ?) = (λs. {(vec_upd s x k)|k. True})"

lemma fbox_nondet_assign[simp]: "|x ::= ?] P = (λs. k. P (χ j. if j = x then k else s$j))"
  unfolding fbox_def nondet_assign_def vec_upd_eq apply(simp add: fun_eq_iff, safe)
  by (erule_tac x="(χ j. if j = x then k else _ $ j)" in allE, auto)

― ‹ Nondeterministic choice ›

lemma fbox_choice: "|(λs. F s  G s)] P = (λs. ( |F] P) s  ( |G] P) s)"
  unfolding fbox_def by auto

lemma le_fbox_choice_iff: "P  |(λs. F s  G s)] Q  P  |F] Q  P  |G] Q"
  unfolding fbox_def by auto

― ‹ Sequential composition ›

definition kcomp :: "('a  'b set)  ('b  'c set)  ('a   'c set)" (infixl ";" 75) where
  "F ; G = μ  𝒫 G  F"

lemma kcomp_eq: "(f ; g) x =  {g y |y. y  f x}"
  unfolding kcomp_def image_def by auto

lemma fbox_kcomp[simp]: "|G ; F] P = |G] |F] P"
  unfolding fbox_def kcomp_def by auto

lemma hoare_kcomp:
  assumes "P  |G] R" "R  |F] Q"
  shows "P  |G ; F] Q"
  apply(subst fbox_kcomp) 
  by (rule order.trans[OF assms(1)]) (rule fbox_iso[OF assms(2)])

― ‹ Conditional statement ›

definition ifthenelse :: "'a pred  ('a  'b set)  ('a  'b set)  ('a  'b set)"
  ("IF _ THEN _ ELSE _" [64,64,64] 63) where 
  "IF P THEN X ELSE Y  (λs. if P s then X s else Y s)"

lemma fbox_if_then_else[simp]:
  "|IF T THEN X ELSE Y] Q = (λs. (T s  ( |X] Q) s)  (¬ T s  ( |Y] Q) s))"
  unfolding fbox_def ifthenelse_def by auto

lemma hoare_if_then_else:
  assumes "(λs. P s  T s)  |X] Q"
    and "(λs. P s  ¬ T s)  |Y] Q"
  shows "P  |IF T THEN X ELSE Y] Q"
  using assms unfolding fbox_def ifthenelse_def by auto

― ‹ Finite iteration ›

definition kpower :: "('a  'a set)  nat  ('a  'a set)" 
  where "kpower f n = (λs. ((;) f ^^ n) skip s)"

lemma kpower_base:
  shows "kpower f 0 s = {s}" and "kpower f (Suc 0) s = f s"
  unfolding kpower_def by(auto simp: kcomp_eq)

lemma kpower_simp: "kpower f (Suc n) s = (f ; kpower f n) s"
  unfolding kcomp_eq 
  apply(induct n)
  unfolding kpower_base 
   apply(force simp: subset_antisym)
  unfolding kpower_def kcomp_eq by simp

definition kleene_star :: "('a  'a set)  ('a  'a set)" ("(_*)" [1000] 999)
  where "(f*) s =  {kpower f n s |n. n  UNIV}"

lemma kpower_inv: 
  fixes F :: "'a  'a set"
  assumes "s. I s  (s'. s'  F s  I s')" 
  shows "s. I s  (s'. s'  (kpower F n s)  I s')"
  apply(clarsimp, induct n)
  unfolding kpower_base kpower_simp 
   apply(simp_all add: kcomp_eq, clarsimp) 
  apply(subgoal_tac "I y", simp)
  using assms by blast

lemma kstar_inv: "I  |F] I  I  |F*] I"
  unfolding kleene_star_def fbox_def 
  apply clarsimp
  apply(unfold le_fun_def, subgoal_tac "x. I x  (s'. s'  F x  I s')")
  using kpower_inv[of I F] by blast simp

lemma fbox_kstarI:
  assumes "P  I" and "I  Q" and "I  |F] I" 
  shows "P  |F*] Q"
proof-
  have "I  |F*] I"
    using assms(3) kstar_inv by blast
  hence "P  |F*] I"
    using assms(1) by auto
  also have "|F*] I  |F*] Q"
    by (rule fbox_iso[OF assms(2)])
  finally show ?thesis .
qed

definition loopi :: "('a  'a set)  'a pred  ('a  'a set)" ("LOOP _ INV _ " [64,64] 63)
  where "LOOP F INV I  (F*)"

lemma change_loopI: "LOOP X INV G = LOOP X INV I"
  unfolding loopi_def by simp

lemma fbox_loopI: "P  I  I  Q  I  |F] I  P  |LOOP F INV I] Q"
  unfolding loopi_def using fbox_kstarI[of "P"] by simp

lemma wp_loopI_break: 
  "P  |Y] I  I  |X] I  I  Q  P  |Y ; (LOOP X INV I)] Q"
  by (rule hoare_kcomp, force) (rule fbox_loopI, auto)


subsection ‹ Verification of hybrid programs ›

text ‹ Verification by providing evolution ›

definition g_evol :: "(('a::ord)  'b  'b)  'b pred  ('b  'a set)  ('b  'b set)" ("EVOL")
  where "EVOL φ G U = (λs. g_orbit (λt. φ t s) G (U s))"

lemma fbox_g_evol[simp]: 
  fixes φ :: "('a::preorder)  'b  'b"
  shows "|EVOL φ G U] Q = (λs. (tU s. (τdown (U s) t. G (φ τ s))  Q (φ t s)))"
  unfolding g_evol_def g_orbit_eq fbox_def by auto

text ‹ Verification by providing solutions ›

lemma fbox_g_orbital: "|x´=f & G on U S @ t0] Q = 
  (λs. XSols f U S t0 s. tU s. (τdown (U s) t. G (X τ))  Q (X t))"
  unfolding fbox_def g_orbital_eq by (auto simp: fun_eq_iff)

context local_flow
begin

lemma fbox_g_ode_subset:
  assumes "s. s  S  0  U s  is_interval (U s)  U s  T"
  shows "|x´= (λt. f) & G on U S @ 0] Q = 
  (λ s. s  S  (t(U s). (τdown (U s) t. G (φ τ s))  Q (φ t s)))"
  apply(unfold fbox_g_orbital fun_eq_iff)
  apply(clarify, rule iffI; clarify)
   apply(force simp: in_ivp_sols assms)
  apply(frule ivp_solsD(2), frule ivp_solsD(3), frule ivp_solsD(4))
  apply(subgoal_tac "τdown (U x) t. X τ = φ τ x")
   apply(clarsimp, fastforce, rule ballI)
  apply(rule ivp_unique_solution[OF _ _ _ _ _ in_ivp_sols])
  using assms by auto
                         
lemma fbox_g_ode: "|x´=(λt. f) & G on (λs. T) S @ 0] Q = 
  (λs. s  S  (tT. (τdown T t. G (φ τ s))  Q (φ t s)))"
  by (subst fbox_g_ode_subset, simp_all add: init_time interval_time)

lemma fbox_g_ode_ivl: "t  0  t  T  |x´=(λt. f) & G on (λs. {0..t}) S @ 0] Q = 
  (λs. s  S  (t{0..t}. (τ{0..t}. G (φ τ s))  Q (φ t s)))"
  apply(subst fbox_g_ode_subset, simp_all add: subintervalI init_time real_Icc_closed_segment)
  by (auto simp: closed_segment_eq_real_ivl)

lemma fbox_orbit: "|γφ] Q = (λs. s  S  ( t  T. Q (φ t s)))"
  unfolding orbit_def fbox_g_ode by simp

end

text ‹ Verification with differential invariants ›

definition g_ode_inv :: "(real  ('a::banach)'a)  'a pred  ('a  real set)  'a set  
  real  'a pred  ('a  'a set)" ("(1x´=_ & _ on _ _ @ _ DINV _ )") 
  where "(x´= f & G on U S @ t0 DINV I) = (x´= f & G on U S @ t0)"

lemma fbox_g_orbital_guard: 
  assumes "H = (λs. G s  Q s)"
  shows "|x´=f & G on U S @ t0] Q = |x´=f & G on U S @ t0] H "
  unfolding fbox_g_orbital using assms by auto

lemma fbox_g_orbital_inv:
  assumes "P  I" and "I  |x´=f & G on U S @ t0] I" and "I  Q"
  shows "P  |x´=f & G on U S @ t0] Q"
  using assms(1) 
  apply(rule order.trans)
  using assms(2) 
  apply(rule order.trans)
  by (rule fbox_iso[OF assms(3)])

lemma fbox_diff_inv[simp]: 
  "(I  |x´=f & G on U S @ t0] I) = diff_invariant I f U S t0 G"
  by (auto simp: diff_invariant_def ivp_sols_def fbox_def g_orbital_eq)

lemma diff_inv_guard_ignore:
  assumes "I  |x´= f & (λs. True) on U S @ t0] I"
  shows "I  |x´= f & G on U S @ t0] I"
  using assms unfolding fbox_diff_inv diff_invariant_eq image_le_pred by auto

context local_flow
begin

lemma fbox_diff_inv_eq: 
  assumes "s. s  S  0  U s  is_interval (U s)  U s  T"
  shows "diff_invariant I (λt. f) U S 0 (λs. True) = 
  ((λs. s  S  I s) = |x´= (λt. f) & (λs. True) on U S @ 0] (λs. s  S  I s))"
  unfolding fbox_diff_inv[symmetric] 
  apply(subst fbox_g_ode_subset[OF assms], simp)+
  apply(clarsimp simp: le_fun_def fun_eq_iff, safe, force)
   apply(erule_tac x=0 in ballE)
  using init_time in_domain ivp(2) assms apply(force, force)
  apply(erule_tac x=x in allE, clarsimp, erule_tac x=t in ballE)
  using in_domain ivp(2) assms by force+

lemma diff_inv_eq_inv_set: 
  "diff_invariant I (λt. f) (λs. T) S 0 (λs. True) = (s. I s  γφ s  {s. I s})"
  unfolding diff_inv_eq_inv_set orbit_def by simp

end

lemma fbox_g_odei: "P  I  I  |x´= f & G on U S @ t0] I  (λs. I s  G s)  Q  
  P  |x´= f & G on U S @ t0 DINV I] Q"
  unfolding g_ode_inv_def 
  apply(rule_tac b="|x´= f & G on U S @ t0] I" in order.trans)
   apply(rule_tac I="I" in fbox_g_orbital_inv, simp_all)
  apply(subst fbox_g_orbital_guard, simp)
  by (rule fbox_iso, force)


subsection ‹ Derivation of the rules of dL ›

text ‹ We derive rules of differential dynamic logic (dL). This allows the components to reason 
in the style of that logic. ›

abbreviation g_dl_ode ::"(('a::banach)'a)  'a pred  'a  'a set" 
  ("(1x´=_ & _)") where "(x´=f & G)  (x´=(λt. f) & G on (λs. {t. t  0}) UNIV @ 0)"

abbreviation g_dl_ode_inv ::"(('a::banach)'a)  'a pred  'a pred  'a  'a set" ("(1x´=_ & _ DINV _)") 
  where "(x´=f & G DINV I)  (x´=(λt. f) & G on (λs. {t. t  0}) UNIV @ 0 DINV I)"

lemma diff_solve_axiom1: 
  assumes "local_flow f UNIV UNIV φ"
  shows "|x´= f & G] Q = 
  (λs. t0. (τ{0..t}. G (φ τ s))  Q (φ t s))"
  by (subst local_flow.fbox_g_ode_subset[OF assms], auto)

lemma diff_solve_axiom2: 
  fixes c::"'a::{heine_borel, banach}"
  shows "|x´=(λs. c) & G] Q = 
  (λs. t0. (τ{0..t}. G (s + τ *R c))  Q (s + t *R c))"
  by (subst local_flow.fbox_g_ode_subset[OF line_is_local_flow, of UNIV], auto)

lemma diff_solve_rule:
  assumes "local_flow f UNIV UNIV φ"
    and "s. P s  (t0. (τ{0..t}. G (φ τ s))  Q (φ t s))"
  shows "P  |x´= f & G] Q"
  using assms by(subst local_flow.fbox_g_ode_subset[OF assms(1)]) auto

lemma diff_weak_axiom1: "( |x´= f & G on U S @ t0] G) s"
  unfolding fbox_def g_orbital_eq by auto

lemma diff_weak_axiom2: "|x´= f & G on T S @ t0] Q = |x´= f & G on T S @ t0] (λs. G s  Q s)"
  unfolding fbox_g_orbital image_def by force
  
lemma diff_weak_rule: "G  Q  P  |x´= f & G on T S @ t0] Q"
  by(auto intro: g_orbitalD simp: le_fun_def g_orbital_eq fbox_def)

lemma fbox_g_orbital_eq_univD:
  assumes "|x´= f & G on U S @ t0] C = (λs. True)" 
    and "τ(down (U s) t). x τ  (x´= f & G on U S @ t0) s"
  shows "τ(down (U s) t). C (x τ)"
proof
  fix τ assume "τ  (down (U s) t)"
  hence "x τ  (x´= f & G on U S @ t0) s" 
    using assms(2) by blast
  also have "s'. s'  (x´= f & G on U S @ t0) s  C s'"
    using assms(1) unfolding fbox_def by meson 
  ultimately show "C (x τ)" 
    by blast
qed

lemma diff_cut_axiom:
  assumes "|x´= f & G on U S @ t0] C = (λs. True)"
  shows "|x´= f & G on U S @ t0] Q = |x´= f & (λs. G s  C s) on U S @ t0] Q"
proof(rule_tac f="λ x. |x] Q" in HOL.arg_cong, rule ext, rule subset_antisym)
  fix s 
  {fix s' assume "s'  (x´= f & G on U S @ t0) s"
    then obtain τ::real and X where x_ivp: "X  Sols f U S t0 s" 
      and "X τ = s'" and "τ  U s" and guard_x:"𝒫 X (down (U s) τ)  {s. G s}"
      using g_orbitalD[of s' "f" G U S t0 s]  by blast
    have "t(down (U s) τ). 𝒫 X (down (U s) t)  {s. G s}"
      using guard_x by (force simp: image_def)
    also have "t(down (U s) τ). t  U s"
      using τ  U s closed_segment_subset_interval by auto
    ultimately have "t(down (U s) τ). X t  (x´= f & G on U S @ t0) s"
      using g_orbitalI[OF x_ivp] by (metis (mono_tags, lifting))
    hence "t(down (U s) τ). C (X t)" 
      using assms unfolding fbox_def by meson
    hence "s'  (x´= f & (λs. G s  C s) on U S @ t0) s"
      using g_orbitalI[OF x_ivp τ  U s] guard_x X τ = s' by fastforce}
  thus "(x´= f & G on U S @ t0) s  (x´= f & (λs. G s  C s) on U S @ t0) s"
    by blast
next show "s. (x´= f & (λs. G s  C s) on U S @ t0) s  (x´= f & G on U S @ t0) s" 
    by (auto simp: g_orbital_eq)
qed

lemma diff_cut_rule:
  assumes fbox_C: "P  |x´= f & G on U S @ t0] C"
    and fbox_Q: "P  |x´= f & (λs. G s  C s) on U S @ t0] Q"
  shows "P  |x´= f & G on U S @ t0] Q"
proof(subst fbox_def, subst g_orbital_eq, clarsimp)
  fix t::real and X::"real  'a" and s assume "P s" and "t  U s"
    and x_ivp:"X  Sols f U S t0 s" 
    and guard_x:"τ. τ  U s  τ  t  G (X τ)"
  have "τ(down (U s) t). X τ  (x´= f & G on U S @ t0) s"
    using g_orbitalI[OF x_ivp] guard_x unfolding image_le_pred by auto
  hence "τ(down (U s) t). C (X τ)" 
    using fbox_C P s by (subst (asm) fbox_def, auto)
  hence "X t  (x´= f & (λs. G s  C s) on U S @ t0) s"
    using guard_x t  U s by (auto intro!: g_orbitalI x_ivp)
  thus "Q (X t)"
    using P s fbox_Q by (subst (asm) fbox_def) auto
qed

lemma diff_inv_axiom1:
  assumes "G s  I s" and "diff_invariant I (λt. f) (λs. {t. t  0}) UNIV 0 G"
  shows "( |x´= f & G] I) s"
  using assms unfolding fbox_g_orbital diff_invariant_eq apply clarsimp
  by (erule_tac x=s in allE, frule ivp_solsD(2), clarsimp)

lemma diff_inv_axiom2:
  assumes "picard_lindeloef (λt. f) UNIV UNIV 0"
    and "s. {t::real. t  0}  picard_lindeloef.ex_ivl (λt. f) UNIV UNIV 0 s"
    and "diff_invariant I (λt. f) (λs. {t::real. t  0}) UNIV 0 G"
  shows "|x´= f & G] I = |(λs. {x. s = x  G s})] I"
proof(unfold fbox_g_orbital, subst fbox_def, clarsimp simp: fun_eq_iff)
  fix s
  let "?ex_ivl s" = "picard_lindeloef.ex_ivl (λt. f) UNIV UNIV 0 s"
  let "?lhs s" = 
    "XSols (λt. f) (λs. {t. t  0}) UNIV 0 s. t0. (τ. 0  τ  τ  t  G (X τ))  I (X t)"
  obtain X where xivp1: "X  Sols (λt. f) (λs. ?ex_ivl s) UNIV 0 s"
    using picard_lindeloef.flow_in_ivp_sols_ex_ivl[OF assms(1)] by auto
  have xivp2: "X  Sols (λt. f) (λs. Collect ((≤) 0)) UNIV 0 s"
    by (rule in_ivp_sols_subset[OF _ _ xivp1], simp_all add: assms(2))
  hence shyp: "X 0 = s"
    using ivp_solsD by auto
  have dinv: "s. I s  ?lhs s"
    using assms(3) unfolding diff_invariant_eq by auto
  {assume "?lhs s" and "G s"
    hence "I s"
      by (erule_tac x=X in ballE, erule_tac x=0 in allE, auto simp: shyp xivp2)}
  hence "?lhs s  (G s  I s)" 
    by blast
  moreover
  {assume "G s  I s"
    hence "?lhs s"
      apply(clarify, subgoal_tac "τ. 0  τ  τ  t  G (X τ)")
       apply(erule_tac x=0 in allE, frule ivp_solsD(2), simp)
      using dinv by blast+}
  ultimately show "?lhs s = (G s  I s)"
    by blast
qed

lemma diff_inv_rule:
  assumes "P  I" and "diff_invariant I f U S t0 G" and "I  Q"
  shows "P  |x´= f & G on U S @ t0] Q"
  apply(rule fbox_g_orbital_inv[OF assms(1) _ assms(3)])
  unfolding fbox_diff_inv using assms(2) .

end

Theory HS_VC_Examples

(*  Title:       Examples of hybrid systems verifications
    Author:      Jonathan Julián Huerta y Munive, 2020
    Maintainer:  Jonathan Julián Huerta y Munive <jonjulian23@gmail.com>
*)

subsection ‹ Examples ›

text ‹ We prove partial correctness specifications of some hybrid systems with our
verification components.›

theory HS_VC_Examples
  imports HS_VC_Spartan

begin


subsubsection ‹Pendulum›

text ‹ The ODEs @{text "x' t = y t"} and {text "y' t = - x t"} describe the circular motion of
a mass attached to a string looked from above. We use @{text "s$1"} to represent the x-coordinate
and @{text "s$2"} for the y-coordinate. We prove that this motion remains circular. ›

abbreviation fpend :: "real^2  real^2" ("f")
  where "f s  (χ i. if i = 1 then s$2 else -s$1)"

abbreviation pend_flow :: "real  real^2  real^2" ("φ")
  where "φ t s  (χ i. if i = 1 then s$1 * cos t + s$2 * sin t else - s$1 * sin t + s$2 * cos t)"

― ‹Verified with annotated dynamics. ›

lemma pendulum_dyn: "(λs. r2 = (s$1)2 + (s$2)2)  |EVOL φ G T] (λs. r2 = (s$1)2 + (s$2)2)"
  by force

― ‹Verified with differential invariants. ›

lemma pendulum_inv: "(λs. r2 = (s$1)2 + (s$2)2)  |x´= f & G] (λs. r2 = (s$1)2 + (s$2)2)"
  by (auto intro!: diff_invariant_rules poly_derivatives)

― ‹Verified with the flow. ›

lemma local_flow_pend: "local_flow f UNIV UNIV φ"
  apply(unfold_locales, simp_all add: local_lipschitz_def lipschitz_on_def vec_eq_iff, clarsimp)
    apply(rule_tac x="1" in exI, clarsimp, rule_tac x=1 in exI)
    apply(simp add: dist_norm norm_vec_def L2_set_def power2_commute UNIV_2)
  by (auto simp: forall_2 intro!: poly_derivatives)

lemma pendulum_flow: "(λs. r2 = (s$1)2 + (s$2)2)  |x´=f & G] (λs. r2 = (s$1)2 + (s$2)2)"
  by (force simp: local_flow.fbox_g_ode_subset[OF local_flow_pend])

no_notation fpend ("f")
        and pend_flow ("φ")


subsubsection ‹ Bouncing Ball ›

text ‹ A ball is dropped from rest at an initial height @{text "h"}. The motion is described with
the free-fall equations @{text "x' t = v t"} and @{text "v' t = g"} where @{text "g"} is the
constant acceleration due to gravity. The bounce is modelled with a variable assignment that
flips the velocity. That is, we model it as a completely elastic collision with the ground. We use 
@{text "s$1"} to represent the ball's height and @{text "s$2"} for its velocity. We prove that the 
ball remains above ground and below its initial resting position. ›

abbreviation fball :: "real  real^2  real^2" ("f")
  where "f g s  (χ i. if i = 1 then s$2 else g)"

abbreviation ball_flow :: "real  real  real^2  real^2" ("φ")
  where "φ g t s  (χ i. if i = 1 then g * t ^ 2/2 + s$2 * t + s$1 else g * t + s$2)"

― ‹Verified with differential invariants. ›

named_theorems bb_real_arith "real arithmetic properties for the bouncing ball."

lemma inv_imp_pos_le[bb_real_arith]:
  assumes "0 > g" and inv: "2 * g * x - 2 * g * h = v * v"
  shows "(x::real)  h"
proof-
  have "v * v = 2 * g * x - 2 * g * h  0 > g"
    using inv and 0 > g by auto
  hence obs:"v * v = 2 * g * (x - h)  0 > g  v * v  0"
    using left_diff_distrib mult.commute by (metis zero_le_square)
  hence "(v * v)/(2 * g) = (x - h)"
    by auto
  also from obs have "(v * v)/(2 * g)  0"
    using divide_nonneg_neg by fastforce
  ultimately have "h - x  0"
    by linarith
  thus ?thesis by auto
qed

lemma "diff_invariant (λs. 2 * g * s$1 - 2 * g * h - s$2 * s$2 = 0) (λt. f g) (λs. UNIV) S t0 G"
  by (auto intro!: poly_derivatives diff_invariant_rules)

lemma bouncing_ball_inv: "g < 0  h  0 
  (λs. s$1 = h  s$2 = 0) 
  |LOOP (
    (x´=(f g) & (λ s. s$1  0) DINV (λs. 2 * g * s$1 - 2 * g * h - s$2 * s$2 = 0)) ;
    (IF (λ s. s$1 = 0) THEN (2 ::= (λs. - s$2)) ELSE skip))
  INV (λs. 0  s$1  2 * g * s$1 - 2 * g * h - s$2 * s$2 = 0)]
  (λs. 0  s$1  s$1  h)"
  apply(rule fbox_loopI, simp_all, force, force simp: bb_real_arith)
  by (rule fbox_g_odei) (auto intro!: poly_derivatives diff_invariant_rules)

― ‹Verified with annotated dynamics. ›

lemma inv_conserv_at_ground[bb_real_arith]:
  assumes invar: "2 * g * x = 2 * g * h + v * v"
    and pos: "g * τ2 / 2 + v * τ + (x::real) = 0"
  shows "2 * g * h + (g * τ + v) * (g * τ + v) = 0"
proof-
  from pos have "g * τ2  + 2 * v * τ + 2 * x = 0" by auto
  then have "g2 * τ2  + 2 * g * v * τ + 2 * g * x = 0"
    by (metis (mono_tags, hide_lams) Groups.mult_ac(1,3) mult_zero_right
        monoid_mult_class.power2_eq_square semiring_class.distrib_left)
  hence "g2 * τ2 + 2 * g * v * τ + v2 + 2 * g * h = 0"
    using invar by (simp add: monoid_mult_class.power2_eq_square)
  hence obs: "(g * τ + v)2 + 2 * g * h = 0"
    apply(subst power2_sum) by (metis (no_types, hide_lams) Groups.add_ac(2, 3)
        Groups.mult_ac(2, 3) monoid_mult_class.power2_eq_square nat_distrib(2))
  thus "2 * g * h + (g * τ + v) * (g * τ + v) = 0"
    by (simp add: add.commute distrib_right power2_eq_square)
qed

lemma inv_conserv_at_air[bb_real_arith]:
  assumes invar: "2 * g * x = 2 * g * h + v * v"
  shows "2 * g * (g * τ2 / 2 + v * τ + (x::real)) =
  2 * g * h + (g * τ + v) * (g * τ + v)" (is "?lhs = ?rhs")
proof-
  have "?lhs = g2 * τ2 + 2 * g * v * τ + 2 * g * x"
    by(auto simp: algebra_simps semiring_normalization_rules(29))
  also have "... = g2 * τ2 + 2 * g * v * τ + 2 * g * h + v * v" (is "... = ?middle")
    by(subst invar, simp)
  finally have "?lhs = ?middle".
  moreover
  {have "?rhs = g * g * (τ * τ) + 2 * g * v * τ + 2 * g * h + v * v"
    by (simp add: Groups.mult_ac(2,3) semiring_class.distrib_left)
  also have "... = ?middle"
    by (simp add: semiring_normalization_rules(29))
  finally have "?rhs = ?middle".}
  ultimately show ?thesis by auto
qed

lemma bouncing_ball_dyn: "g < 0  h  0 
  (λs. s$1 = h  s$2 = 0) 
  |LOOP (
    (EVOL (φ g) (λ s. s$1  0) T) ;
    (IF (λ s. s$1 = 0) THEN (2 ::= (λs. - s$2)) ELSE skip))
  INV (λs. 0  s$1 2 * g * s$1 = 2 * g * h + s$2 * s$2)]
  (λs. 0  s$1  s$1  h)"
  by (rule fbox_loopI) (auto simp: bb_real_arith)

― ‹Verified with the flow. ›

lemma local_flow_ball: "local_flow (f g) UNIV UNIV (φ g)"
  apply(unfold_locales, simp_all add: local_lipschitz_def lipschitz_on_def vec_eq_iff, clarsimp)
    apply(rule_tac x="1/2" in exI, clarsimp, rule_tac x=1 in exI)
    apply(simp add: dist_norm norm_vec_def L2_set_def UNIV_2)
  by (auto simp: forall_2 intro!: poly_derivatives)

lemma bouncing_ball_flow: "g < 0  h  0 
  (λs. s$1 = h  s$2 = 0) 
  |LOOP (
    (x´=(λt. f g) & (λ s. s$1  0) on (λs. UNIV) UNIV @ 0) ;
    (IF (λ s. s$1 = 0) THEN (2 ::= (λs. - s$2)) ELSE skip))
  INV (λs. 0  s$1 2 * g * s$1 = 2 * g * h + s$2 * s$2)]
  (λs. 0  s$1  s$1  h)"
  apply(rule fbox_loopI, simp_all add: local_flow.fbox_g_ode_subset[OF local_flow_ball])
  by (auto simp: bb_real_arith)

no_notation fball ("f")
        and ball_flow ("φ")


subsubsection ‹ Thermostat ›

text ‹ A thermostat has a chronometer, a thermometer and a switch to turn on and off a heater.
At most every @{text "t"} minutes, it sets its chronometer to @{term "0::real"}, it registers
the room temperature, and it turns the heater on (or off) based on this reading. The temperature
follows the ODE @{text "T' = - a * (T - U)"} where @{text "U"} is @{text "L ≥ 0"} when the heater
is on, and @{text "0"} when it is off. We use @{term "1::4"} to denote the room's temperature,
@{term "2::4"} is time as measured by the thermostat's chronometer, @{term "3::4"} is the
temperature detected by the thermometer, and @{term "4::4"} states whether the heater is on
(@{text "s$4 = 1"}) or off (@{text "s$4 = 0"}). We prove that the thermostat keeps the room's
temperature between @{text "Tmin"} and @{text "Tmax"}. ›

abbreviation temp_vec_field :: "real  real  real^4  real^4" ("f")
  where "f a L s  (χ i. if i = 2 then 1 else (if i = 1 then - a * (s$1 - L) else 0))"

abbreviation temp_flow :: "real  real  real  real^4  real^4" ("φ")
  where "φ a L t s  (χ i. if i = 1 then - exp(-a * t) * (L - s$1) + L else
  (if i = 2 then t + s$2 else s$i))"

― ‹Verified with the flow. ›

lemma norm_diff_temp_dyn: "0 < a  f a L s1 - f a L s2 = ¦a¦ * ¦s1$1 - s2$1¦"
proof(simp add: norm_vec_def L2_set_def, unfold UNIV_4, simp)
  assume a1: "0 < a"
  have f2: "r ra. ¦(r::real) + - ra¦ = ¦ra + - r¦"
    by (metis abs_minus_commute minus_real_def)
  have "r ra rb. (r::real) * ra + - (r * rb) = r * (ra + - rb)"
    by (metis minus_real_def right_diff_distrib)
  hence "¦a * (s1$1 + - L) + - (a * (s2$1 + - L))¦ = a * ¦s1$1 + - s2$1¦"
    using a1 by (simp add: abs_mult)
  thus "¦a * (s2$1 - L) - a * (s1$1 - L)¦ = a * ¦s1$1 - s2$1¦"
    using f2 minus_real_def by presburger
qed

lemma local_lipschitz_temp_dyn:
  assumes "0 < (a::real)"
  shows "local_lipschitz UNIV UNIV (λt::real. f a L)"
  apply(unfold local_lipschitz_def lipschitz_on_def dist_norm)
  apply(clarsimp, rule_tac x=1 in exI, clarsimp, rule_tac x=a in exI)
  using assms
  apply(simp add: norm_diff_temp_dyn)
  apply(simp add: norm_vec_def L2_set_def, unfold UNIV_4, clarsimp)
  unfolding real_sqrt_abs[symmetric] by (rule real_le_lsqrt) auto

lemma local_flow_temp: "a > 0  local_flow (f a L) UNIV UNIV (φ a L)"
  by (unfold_locales, auto intro!: poly_derivatives local_lipschitz_temp_dyn simp: forall_4 vec_eq_iff)

lemma temp_dyn_down_real_arith:
  assumes "a > 0" and Thyps: "0 < Tmin" "Tmin  T" "T  Tmax"
    and thyps: "0  (t::real)" "τ{0..t}. τ  - (ln (Tmin / T) / a) "
  shows "Tmin  exp (-a * t) * T" and "exp (-a * t) * T  Tmax"
proof-
  have "0  t  t  - (ln (Tmin / T) / a)"
    using thyps by auto
  hence "ln (Tmin / T)  - a * t  - a * t  0"
    using assms(1) divide_le_cancel by fastforce
  also have "Tmin / T > 0"
    using Thyps by auto
  ultimately have obs: "Tmin / T  exp (-a * t)" "exp (-a * t)  1"
    using exp_ln exp_le_one_iff by (metis exp_less_cancel_iff not_less, simp)
  thus "Tmin  exp (-a * t) * T"
    using Thyps by (simp add: pos_divide_le_eq)
  show "exp (-a * t) * T  Tmax"
    using Thyps mult_left_le_one_le[OF _ exp_ge_zero obs(2), of T]
      less_eq_real_def order_trans_rules(23) by blast
qed

lemma temp_dyn_up_real_arith:
  assumes "a > 0" and Thyps: "Tmin  T" "T  Tmax" "Tmax < (L::real)"
    and thyps: "0  t" "τ{0..t}. τ  - (ln ((L - Tmax) / (L - T)) / a) "
  shows "L - Tmax  exp (-(a * t)) * (L - T)"
    and "L - exp (-(a * t)) * (L - T)  Tmax"
    and "Tmin  L - exp (-(a * t)) * (L - T)"
proof-
  have "0  t  t  - (ln ((L - Tmax) / (L - T)) / a)"
    using thyps by auto
  hence "ln ((L - Tmax) / (L - T))  - a * t  - a * t  0"
    using assms(1) divide_le_cancel by fastforce
  also have "(L - Tmax) / (L - T) > 0"
    using Thyps by auto
  ultimately have "(L - Tmax) / (L - T)  exp (-a * t)  exp (-a * t)  1"
    using exp_ln exp_le_one_iff by (metis exp_less_cancel_iff not_less)
  moreover have "L - T > 0"
    using Thyps by auto
  ultimately have obs: "(L - Tmax)  exp (-a * t) * (L - T)  exp (-a * t) * (L - T)  (L - T)"
    by (simp add: pos_divide_le_eq)
  thus "(L - Tmax)  exp (-(a * t)) * (L - T)"
    by auto
  thus "L - exp (-(a * t)) * (L - T)  Tmax"
    by auto
  show "Tmin  L - exp (-(a * t)) * (L - T)"
    using Thyps and obs by auto
qed

lemmas fbox_temp_dyn = local_flow.fbox_g_ode_subset[OF local_flow_temp]

lemma thermostat:
  assumes "a > 0" and "0 < Tmin" and "Tmax < L"
  shows "(λs. Tmin  s$1  s$1  Tmax  s$4 = 0) 
  |LOOP
    ― ‹control›
    ((2 ::= (λs. 0));(3 ::= (λs. s$1));
    (IF (λs. s$4 = 0  s$3  Tmin + 1) THEN (4 ::= (λs.1)) ELSE
    (IF (λs. s$4 = 1  s$3  Tmax - 1) THEN (4 ::= (λs.0)) ELSE skip));
    ― ‹dynamics›
    (IF (λs. s$4 = 0) THEN (x´= f a 0 & (λs. s$2  - (ln (Tmin/s$3))/a))
    ELSE (x´= f a L & (λs. s$2  - (ln ((L-Tmax)/(L-s$3)))/a))) )
  INV (λs. Tmin s$1  s$1  Tmax  (s$4 = 0  s$4 = 1))]
  (λs. Tmin  s$1  s$1  Tmax)"
  apply(rule fbox_loopI, simp_all add: fbox_temp_dyn[OF assms(1)] le_fun_def)
  using temp_dyn_up_real_arith[OF assms(1) _ _ assms(3), of Tmin]
    and temp_dyn_down_real_arith[OF assms(1,2), of _ Tmax] by auto

no_notation temp_vec_field ("f")
        and temp_flow ("φ")

subsubsection ‹ Tank ›

text ‹ A controller turns a water pump on and off to keep the level of water @{text "h"} in a tank
within an acceptable range @{text "hmin ≤ h ≤ hmax"}. Just like in the previous example, after 
each intervention, the controller registers the current level of water and resets its chronometer,
then it changes the status of the water pump accordingly. The level of water grows linearly 
@{text "h' = k"} at a rate of @{text "k = ci-co"} if the pump is on, and at a rate of 
@{text "k = -co"} if the pump is off. We use @{term "1::4"} to denote the tank's level of water,
@{term "2::4"} is time as measured by the controller's chronometer, @{term "3::4"} is the
level of water measured by the chronometer, and @{term "4::4"} states whether the pump is on
(@{text "s$4 = 1"}) or off (@{text "s$4 = 0"}). We prove that the controller keeps the level of
water between @{text "hmin"} and @{text "hmax"}. ›

abbreviation tank_vec_field :: "real  real^4  real^4" ("f")
  where "f k s  (χ i. if i = 2 then 1 else (if i = 1 then k else 0))"

abbreviation tank_flow :: "real  real  real^4  real^4" ("φ")
  where "φ k τ s  (χ i. if i = 1 then k * τ + s$1 else 
  (if i = 2 then τ + s$2 else s$i))"

abbreviation tank_guard :: "real  real  real^4  bool" ("G")
  where "G Hm k s  s$2  (Hm - s$3)/k"

abbreviation tank_loop_inv :: "real  real  real^4  bool" ("I")
  where "I hmin hmax s  hmin  s$1  s$1  hmax  (s$4 = 0  s$4 = 1)"

abbreviation tank_diff_inv :: "real  real  real  real^4  bool" ("dI")
  where "dI hmin hmax k s  s$1 = k * s$2 + s$3  0  s$2  
    hmin  s$3  s$3  hmax  (s$4 =0  s$4 = 1)"

lemma local_flow_tank: "local_flow (f k) UNIV UNIV (φ k)"
  apply (unfold_locales, unfold local_lipschitz_def lipschitz_on_def, simp_all, clarsimp)
  apply(rule_tac x="1/2" in exI, clarsimp, rule_tac x=1 in exI)
  apply(simp add: dist_norm norm_vec_def L2_set_def, unfold UNIV_4)
  by (auto intro!: poly_derivatives simp: vec_eq_iff)

lemma tank_arith:
  assumes "0  (τ::real)" and "0 < co" and "co < ci"
  shows "τ{0..τ}. τ  - ((hmin - y) / co)   hmin  y - co * τ"
    and "τ{0..τ}. τ  (hmax - y) / (ci - co)   (ci - co) * τ + y  hmax"
    and "hmin  y  hmin  (ci - co) * τ + y"
    and "y  hmax  y - co * τ  hmax"
  apply(simp_all add: field_simps le_divide_eq assms)
  using assms apply (meson add_mono less_eq_real_def mult_left_mono)
  using assms by (meson add_increasing2 less_eq_real_def mult_nonneg_nonneg) 

lemma tank_flow:
  assumes "0 < co" and "co < ci"
  shows "I hmin hmax 
  |LOOP 
    ― ‹control›
    ((2 ::=(λs.0));(3 ::=(λs. s$1));
    (IF (λs. s$4 = 0  s$3  hmin + 1) THEN (4 ::= (λs.1)) ELSE 
    (IF (λs. s$4 = 1  s$3  hmax - 1) THEN (4 ::= (λs.0)) ELSE skip));
    ― ‹dynamics›
    (IF (λs. s$4 = 0) THEN (x´= f (ci-co) & (G hmax (ci-co))) 
     ELSE (x´= f (-co) & (G hmin (-co)))) ) INV I hmin hmax]  
  I hmin hmax"
  apply(rule fbox_loopI, simp_all add: le_fun_def)
  apply(clarsimp simp: le_fun_def local_flow.fbox_g_ode_subset[OF local_flow_tank])
  using assms tank_arith[OF _ assms] by auto

no_notation tank_vec_field ("f")
        and tank_flow ("φ")
        and tank_loop_inv ("I")
        and tank_diff_inv ("dI")
        and tank_guard ("G")

end

Theory HS_VC_PT

(*  Title:       Verification components with predicate transformers
    Author:      Jonathan Julián Huerta y Munive, 2020
    Maintainer:  Jonathan Julián Huerta y Munive <jonjulian23@gmail.com>
*)

section ‹ Verification components with Predicate Transformers ›

text ‹ We use the categorical forward box operator @{text fb} to compute weakest liberal 
preconditions (wlps) of hybrid programs. Then we repeat the three methods for verifying 
correctness specifications of the continuous dynamics of a HS. ›

theory HS_VC_PT
  imports 
    "Transformer_Semantics.Kleisli_Quantaloid"
    "../HS_ODEs" 
                        
begin

no_notation bres (infixr "" 60)
        and dagger ("_" [101] 100)
        and "Relation.relcomp" (infixl ";" 75) 
        and eta ("η")
        and kcomp (infixl "K" 75)

type_synonym 'a pred = "'a  bool"

notation eta ("skip")
     and kcomp (infixl ";" 75)
     and g_orbital ("(1x´=_ & _ on _ _ @ _)")


subsection ‹Verification of regular programs›

text ‹Properties of the forward box operator. ›

lemma "fb F S = (  𝒫 (- opK F)) (- S)"
  unfolding ffb_def map_dual_def dual_set_def klift_def by simp

lemma "fb F S = {s. F s  S}"
  by (auto simp: ffb_def kop_def klift_def map_dual_def dual_set_def f2r_def r2f_def)

lemma ffb_eq: "fb F S = {s. s'. s'  F s  s'  S}"
  by (auto simp: ffb_def kop_def klift_def map_dual_def dual_set_def f2r_def r2f_def)

lemma ffb_iso: "P  Q  fb F P  fb F Q"
  unfolding ffb_eq by auto

lemma ffb_invariants: 
  assumes "{s. I s}  fb F {s. I s}" and "{s. J s}  fb F {s. J s}"
  shows "{s. I s  J s}  fb F {s. I s  J s}"
    and "{s. I s  J s}  fb F {s. I s  J s}"
  using assms unfolding ffb_eq by auto

― ‹ Skip ›

lemma ffb_skip[simp]: "fb skip S = S"
  unfolding ffb_def by(simp add: kop_def klift_def map_dual_def)

― ‹ Tests ›

definition test :: "'a pred  'a  'a set" ("(1¿_?)")
  where "¿P? = (λs. {x. x = s  P x})"

lemma ffb_test[simp]: "fb ¿P? Q = {s. P s  s  Q}"
  unfolding ffb_eq test_def by simp

― ‹ Assignments ›

definition assign :: "'n  ('a^'n  'a)  ('a^'n)  ('a^'n) set" ("(2_ ::= _)" [70, 65] 61) 
  where "(x ::= e) = (λs. {vec_upd s x (e s)})" 

lemma ffb_assign[simp]: "fb (x ::= e) Q = {s. (χ j. ((($) s)(x := (e s))) j)  Q}"
  unfolding vec_upd_def assign_def by (subst ffb_eq) simp

― ‹ Nondeterministic assignments ›

definition nondet_assign :: "'n  'a^'n  ('a^'n) set" ("(2_ ::= ? )" [70] 61)
  where "(x ::= ?) = (λs. {(vec_upd s x k)|k. True})"

lemma fbox_nondet_assign[simp]: "fb (x ::= ?) P = {s. k. (χ j. if j = x then k else s$j)  P}"
  unfolding ffb_eq nondet_assign_def vec_upd_eq apply(simp add: fun_eq_iff, safe)
  by (erule_tac x="(χ j. if j = x then k else _ $ j)" in allE, auto)

― ‹ Nondeterministic choice ›

lemma ffb_choice: "fb (λs. F s  G s) P = fb F P  fb G P"
  unfolding ffb_eq by auto

lemma le_ffb_choice_iff: "P  fb (λs. F s  G s) Q  P  fb F Q  P  fb G Q"
  unfolding ffb_eq by auto

― ‹ Sequential composition ›

lemma ffb_kcomp[simp]: "fb (G ; F) P = fb G (fb F P)"
  unfolding ffb_eq by (auto simp: kcomp_def)

lemma hoare_kcomp:
  assumes "P  fb F R" "R  fb G Q"
  shows "P  fb (F ; G) Q"
  apply(subst ffb_kcomp) 
  by (rule order.trans[OF assms(1)]) (rule ffb_iso[OF assms(2)])

― ‹ Conditional statement ›

definition ifthenelse :: "'a pred  ('a  'b set)  ('a  'b set)  ('a  'b set)"
  ("IF _ THEN _ ELSE _" [64,64,64] 63) where 
  "IF P THEN X ELSE Y = (λ x. if P x then X x else Y x)"

lemma ffb_if_then_else[simp]:
  "fb (IF T THEN X ELSE Y) Q = {s. T s  s  fb X Q}  {s. ¬ T s  s  fb Y Q}"
  unfolding ffb_eq ifthenelse_def by auto

lemma hoare_if_then_else:
  assumes "P  {s. T s}  fb X Q"
    and "P  {s. ¬ T s}  fb Y Q"
  shows "P  fb (IF T THEN X ELSE Y) Q"
  using assms 
  apply(subst ffb_eq)
  apply(subst (asm) ffb_eq)+
  unfolding ifthenelse_def by auto

― ‹ Finite iteration ›

lemma kpower_inv: "I  {s. y. y  F s  y  I}  I  {s. y. y  (kpower F n s)  y  I}"
  apply(induct n, simp)
  apply simp
  by(auto simp: kcomp_prop) 

lemma kstar_inv: "I  fb F I  I  fb (kstar F) I"
  unfolding kstar_def ffb_eq apply clarsimp
  using kpower_inv by blast

lemma ffb_kstarI:
  assumes "P  I" and "I  Q" and "I  fb F I"
  shows "P  fb (kstar F) Q"
proof-
  have "I  fb (kstar F) I"
    using assms(3) kstar_inv by blast
  hence "P  fb (kstar F) I"
    using assms(1) by auto
  also have "fb (kstar F) I  fb (kstar F) Q"
    by (rule ffb_iso[OF assms(2)])
  finally show ?thesis .
qed

definition loopi :: "('a  'a set)  'a pred  ('a  'a set)" ("LOOP _ INV _ " [64,64] 63)
  where "LOOP F INV I  (kstar F)"

lemma change_loopI: "LOOP X INV G = LOOP X INV I"
  unfolding loopi_def by simp

lemma ffb_loopI: "P  {s. I s}   {s. I s}  Q  {s. I s}  fb F {s. I s}  P  fb (LOOP F INV I) Q"
  unfolding loopi_def using ffb_kstarI[of "P"] by simp

lemma ffb_loopI_break: 
  "P  fb Y {s. I s}  {s. I s}  fb X {s. I s}  {s. I s}  Q  P  fb (Y ; (LOOP X INV I)) Q"
  by (rule hoare_kcomp, force) (rule ffb_loopI, auto)


subsection ‹Verification of hybrid programs›

text ‹Verification by providing evolution›

definition g_evol :: "(('a::ord)  'b  'b)  'b pred  ('b  'a set)  ('b  'b set)" ("EVOL")
  where "EVOL φ G U = (λs. g_orbit (λt. φ t s) G (U s))"

lemma fbox_g_evol[simp]: 
  fixes φ :: "('a::preorder)  'b  'b"
  shows "fb (EVOL φ G U) Q = {s. (tU s. (τdown (U s) t. G (φ τ s))  (φ t s)  Q)}"
  unfolding g_evol_def g_orbit_eq ffb_eq by auto

text ‹Verification by providing solutions›

lemma ffb_g_orbital: "fb (x´= f & G on U S @ t0) Q = 
  {s. XSols f U S t0 s. tU s. (τdown (U s) t. G (X τ))  (X t)  Q}"
  unfolding ffb_eq g_orbital_eq by (auto simp: fun_eq_iff)

context local_flow
begin

lemma ffb_g_ode_subset:
  assumes "s. s  S  0  U s  is_interval (U s)  U s  T"
  shows "fb (x´= (λt. f) & G on U S @ 0) Q = 
  {s. s  S  (t(U s). (τdown (U s) t. G (φ τ s))  (φ t s)  Q)}"
  apply(unfold ffb_g_orbital set_eq_iff)
  apply(clarify, rule iffI; clarify)
   apply(force simp: in_ivp_sols assms)
  apply(frule ivp_solsD(2), frule ivp_solsD(3), frule ivp_solsD(4))
  apply(subgoal_tac "τdown (U x) t. X τ = φ τ x")
   apply(clarsimp, fastforce, rule ballI)
  apply(rule ivp_unique_solution[OF _ _ _ _ _ in_ivp_sols])
  using assms by auto

lemma ffb_g_ode: "fb (x´= (λt. f) & G on (λs. T) S @ 0) Q = 
  {s. s  S  (tT. (τdown T t. G (φ τ s))  (φ t s)  Q)}" (is "_ = ?wlp")
  by (subst ffb_g_ode_subset, simp_all add: init_time interval_time)

lemma ffb_g_ode_ivl: "t  0  t  T  fb (x´=(λt. f) & G on (λs. {0..t}) S @ 0) Q = 
  {s. s  S  (t{0..t}. (τ{0..t}. G (φ τ s))  (φ t s)  Q)}"
  apply(subst ffb_g_ode_subset, simp_all add: subintervalI init_time real_Icc_closed_segment)
  by (auto simp: closed_segment_eq_real_ivl)

lemma ffb_orbit: "fb γφ Q = {s. s  S  ( t  T. φ t s  Q)}"
  unfolding orbit_def ffb_g_ode by simp

end

text ‹ Verification with differential invariants ›

definition g_ode_inv :: "(real  ('a::banach)'a)  'a pred  ('a  real set)  'a set  
  real  'a pred  ('a  'a set)" ("(1x´=_ & _ on _ _ @ _ DINV _ )") 
  where "(x´= f & G on U S @ t0 DINV I) = (x´= f & G on U S @ t0)"

lemma ffb_g_orbital_guard: 
  assumes "H = (λs. G s  Q s)"
  shows "fb (x´= f & G on U S @ t0) {s. Q s} = fb (x´= f & G on U S @ t0) {s. H s}"
  unfolding ffb_g_orbital using assms by auto

lemma ffb_g_orbital_inv:
  assumes "P  I" and "I  fb (x´= f & G on U S @ t0) I" and "I  Q"
  shows "P  fb (x´= f & G on U S @ t0) Q"
  using assms(1) 
  apply(rule order.trans)
  using assms(2) 
  apply(rule order.trans)
  by (rule ffb_iso[OF assms(3)])

lemma ffb_diff_inv[simp]: 
  "({s. I s}  fb (x´= f & G on U S @ t0) {s. I s}) = diff_invariant I f U S t0 G"
  by (auto simp: diff_invariant_def ivp_sols_def ffb_eq g_orbital_eq)

lemma bdf_diff_inv:
  "diff_invariant I f U S t0 G = (bd (x´= f & G on U S @ t0) {s. I s}  {s. I s})"
  unfolding ffb_fbd_galois_var by (auto simp: diff_invariant_def ivp_sols_def ffb_eq g_orbital_eq)

lemma diff_inv_guard_ignore:
  assumes "{s. I s}  fb (x´= f & (λs. True) on U S @ t0) {s. I s}"
  shows "{s. I s}  fb (x´= f & G on U S @ t0) {s. I s}"
  using assms unfolding ffb_diff_inv diff_invariant_eq image_le_pred by auto

context local_flow
begin

lemma ffb_diff_inv_eq: 
  assumes "s. s  S  0  U s  is_interval (U s)  U s  T"
  shows "diff_invariant I (λt. f) U S 0 (λs. True) = 
  ({s. s  S  I s} = fb (x´= (λt. f) & (λs. True) on U S @ 0) {s. s  S  I s})"
 unfolding ffb_diff_inv[symmetric] 
  apply(subst ffb_g_ode_subset[OF assms], simp)+
  apply(clarsimp simp: set_eq_iff, safe, force)
   apply(erule_tac x=0 in ballE)
  using init_time in_domain ivp(2) assms apply(force, force)
  apply(erule_tac x=x in allE, clarsimp, erule_tac x=t in ballE)
  using in_domain ivp(2) assms by force+

lemma diff_inv_eq_inv_set:
  "diff_invariant I (λt. f) (λs. T) S 0 (λs. True) = (s. I s  γφ s  {s. I s})"
  unfolding diff_inv_eq_inv_set orbit_def by simp

end

lemma ffb_g_odei: "P  {s. I s}  {s. I s}  fb (x´= f & G on U S @ t0) {s. I s}  
  {s. I s  G s}  Q  P  fb (x´= f & G on U S @ t0 DINV I) Q"
  unfolding g_ode_inv_def 
  apply(rule_tac b="fb (x´= f & G on U S @ t0) {s. I s}" in order.trans)
   apply(rule_tac I="{s. I s}" in ffb_g_orbital_inv, simp_all)
  apply(subst ffb_g_orbital_guard, simp)
  by (rule ffb_iso, force)

subsection ‹ Derivation of the rules of dL ›

text‹ We derive domain specific rules of differential dynamic logic (dL). First we present a 
generalised version, then we show the rules as instances of the general ones.›

abbreviation g_dl_orbit ::"(('a::banach)'a)  'a pred  'a  'a set" ("(1x´=_ & _)") 
  where "(x´=f & G)  (x´=(λt. f) & G on (λs. {t. t  0}) UNIV @ 0)"

abbreviation g_dl_ode_inv ::"(('a::banach)'a)  'a pred  'a pred  'a  'a set" ("(1x´=_ & _ DINV _)") 
  where "(x´=f & G DINV I)  (x´=(λt. f) & G on (λs. {t. t  0}) UNIV @ 0 DINV I)"

lemma diff_solve_axiom1: 
  assumes "local_flow f UNIV UNIV φ"
  shows "fb (x´= f & G) Q = 
  {s. t0. (τ{0..t}. G (φ τ s))  (φ t s)  Q}"
  by (subst local_flow.ffb_g_ode_subset[OF assms], auto)

lemma diff_solve_axiom2: 
  fixes c::"'a::{heine_borel, banach}"
  shows "fb (x´=(λs. c) & G) Q = 
  {s. t0. (τ{0..t}. G (s + τ *R c))  (s + t *R c)  Q}"
  apply(subst local_flow.ffb_g_ode_subset[where φ="(λt s. s + t *R c)" and T=UNIV])
  by (rule line_is_local_flow, auto)

lemma diff_solve_rule:
  assumes "local_flow f UNIV UNIV φ"
    and "s. s  P  (t0. (τ{0..t}. G (φ τ s))  (φ t s)  Q)"
  shows "P  fb (x´= f & G) Q"
  using assms by(subst local_flow.ffb_g_ode_subset[OF assms(1)]) auto

lemma diff_weak_axiom1: "s  (fb (x´= f & G on U S @ t0) {s. G s})"
  unfolding ffb_eq g_orbital_eq by auto

lemma diff_weak_axiom2: "fb (x´= f & G on T S @ t0) Q = fb (x´= f & G on T S @ t0) {s. G s  s  Q}"
  unfolding ffb_g_orbital image_def by force
    
lemma diff_weak_rule: "{s. G s}  Q  P  fb (x´= f & G on T S @ t0) Q"
  by(auto intro: g_orbitalD simp: le_fun_def g_orbital_eq ffb_eq)

lemma ffb_g_orbital_eq_univD:
  assumes "fb (x´= f & G on U S @ t0) {s. C s} = UNIV" 
    and "τ(down (U s) t). x τ  (x´= f & G on U S @ t0) s"
  shows "τ(down (U s) t). C (x τ)"
proof
  fix τ assume "τ  (down (U s) t)"
  hence "x τ  (x´= f & G on U S @ t0) s" 
    using assms(2) by blast
  also have "y. y  (x´= f & G on U S @ t0) s  C y" 
    using assms(1) unfolding ffb_eq by fastforce
  ultimately show "C (x τ)" by blast
qed

lemma diff_cut_axiom:
  assumes "fb (x´= f & G on U S @ t0) {s. C s} = UNIV"
  shows "fb (x´= f & G on U S @ t0) Q = fb (x´= f & (λs. G s  C s) on U S @ t0) Q"
proof(rule_tac f="λ x. fb x Q" in HOL.arg_cong, rule ext, rule subset_antisym)
  fix s 
  {fix s' assume "s'  (x´= f & G on U S @ t0) s"
    then obtain τ::real and X where x_ivp: "X  Sols f U S t0 s" 
      and "X τ = s'" and "τ  (U s)" and guard_x:"𝒫 X (down (U s) τ)  {s. G s}"
      using g_orbitalD[of s' "f" G _ S t0 s]  by blast
    have "t(down (U s) τ). 𝒫 X (down (U s) t)  {s. G s}"
      using guard_x by (force simp: image_def)
    also have "t(down (U s) τ). t  (U s)"
      using τ  (U s) closed_segment_subset_interval by auto
    ultimately have "t(down (U s) τ). X t  (x´= f & G on U S @ t0) s"
      using g_orbitalI[OF x_ivp] by (metis (mono_tags, lifting))
    hence "t(down (U s) τ). C (X t)" 
      using assms unfolding ffb_eq by fastforce
    hence "s'  (x´= f & (λs. G s  C s) on U S @ t0) s"
      using g_orbitalI[OF x_ivp τ  (U s)] guard_x X τ = s' 
      unfolding image_le_pred by fastforce}
  thus "(x´= f & G on U S @ t0) s  (x´= f & (λs. G s  C s) on U S @ t0) s"
    by blast
next show "s. (x´= f & (λs. G s  C s) on U S @ t0) s  (x´= f & G on U S @ t0) s" 
    by (auto simp: g_orbital_eq)
qed

lemma diff_cut_rule:
  assumes ffb_C: "P  fb (x´= f & G on U S @ t0) {s. C s}"
    and ffb_Q: "P  fb (x´= f & (λs. G s  C s) on U S @ t0) Q"
  shows "P  fb (x´= f & G on U S @ t0) Q"
proof(subst ffb_eq, subst g_orbital_eq, clarsimp)
  fix t::real and X::"real  'a" and s assume "s  P" and "t  (U s)"
    and x_ivp:"X  Sols f U S t0 s" 
    and guard_x:"τ. τ  (U s)  τ  t  G (X τ)"
  have "τ(down (U s) t). X τ  (x´= f & G on U S @ t0) s"
    using g_orbitalI[OF x_ivp] guard_x unfolding image_le_pred by auto
  hence "τ(down (U s) t). C (X τ)" 
    using ffb_C s  P by (subst (asm) ffb_eq, auto)
  hence "X t  (x´= f & (λs. G s  C s) on U S @ t0) s"
    using guard_x t  (U s) by (auto intro!: g_orbitalI x_ivp)
  thus "(X t)  Q"
    using s  P ffb_Q by (subst (asm) ffb_eq) auto
qed

lemma diff_inv_axiom1:
  assumes "G s  I s" and "diff_invariant I (λt. f) (λs. {t. t  0}) UNIV 0 G"
  shows "s  (fb (x´= f & G) {s. I s})"
  using assms unfolding ffb_g_orbital diff_invariant_eq apply clarsimp
  by (erule_tac x=s in allE, frule ivp_solsD(2), clarsimp)

lemma diff_inv_axiom2:
  assumes "picard_lindeloef (λt. f) UNIV UNIV 0"
    and "s. {t::real. t  0}  picard_lindeloef.ex_ivl (λt. f) UNIV UNIV 0 s"
    and "diff_invariant I (λt. f) (λs. {t::real. t  0}) UNIV 0 G"
  shows "fb (x´= f & G) {s. I s} = fb (λs. {x. s = x  G s}) {s. I s}"
proof(unfold ffb_g_orbital, subst ffb_eq, clarsimp simp: set_eq_iff)
  fix s
  let "?ex_ivl s" = "picard_lindeloef.ex_ivl (λt. f) UNIV UNIV 0 s"
  let "?lhs s" = 
    "XSols (λt. f) (λs. {t. t  0}) UNIV 0 s. t0. (τ. 0  τ  τ  t  G (X τ))  I (X t)"
  obtain X where xivp1: "X  Sols (λt. f) (λs. ?ex_ivl s) UNIV 0 s"
    using picard_lindeloef.flow_in_ivp_sols_ex_ivl[OF assms(1)] by auto
  have xivp2: "X  Sols (λt. f) (λs. Collect ((≤) 0)) UNIV 0 s"
    by (rule in_ivp_sols_subset[OF _ _ xivp1], simp_all add: assms(2))
  hence shyp: "X 0 = s"
    using ivp_solsD by auto
  have dinv: "s. I s  ?lhs s"
    using assms(3) unfolding diff_invariant_eq by auto
  {assume "?lhs s" and "G s"
    hence "I s"
      by (erule_tac x=X in ballE, erule_tac x=0 in allE, auto simp: shyp xivp2)}
  hence "?lhs s  (G s  I s)" 
    by blast
  moreover
  {assume "G s  I s"
    hence "?lhs s"
      apply(clarify, subgoal_tac "τ. 0  τ  τ  t  G (X τ)")
       apply(erule_tac x=0 in allE, frule ivp_solsD(2), simp)
      using dinv by blast+}
  ultimately show "?lhs s = (G s  I s)"
    by blast
qed

lemma diff_inv_rule:
  assumes "P  {s. I s}" and "diff_invariant I f U S t0 G" and "{s. I s}  Q"
  shows "P  fb (x´= f & G on U S @ t0) Q"
  apply(rule ffb_g_orbital_inv[OF assms(1) _ assms(3)])
  unfolding ffb_diff_inv using assms(2) .

end

Theory HS_VC_PT_Examples

(*  Title:       Examples of hybrid systems verifications
    Author:      Jonathan Julián Huerta y Munive, 2020
    Maintainer:  Jonathan Julián Huerta y Munive <jonjulian23@gmail.com>
*)

subsection ‹ Examples ›

text ‹ We prove partial correctness specifications of some hybrid systems with our
recently described verification components.›

theory HS_VC_PT_Examples
  imports HS_VC_PT

begin


subsubsection ‹ Pendulum ›

text ‹ The ODEs @{text "x' t = y t"} and {text "y' t = - x t"} describe the circular motion of
a mass attached to a string looked from above. We use @{text "s$1"} to represent the x-coordinate
and @{text "s$2"} for the y-coordinate. We prove that this motion remains circular. ›

abbreviation fpend :: "real^2  real^2" ("f")
  where "f s  (χ i. if i = 1 then s$2 else -s$1)"

abbreviation pend_flow :: "real  real^2  real^2" ("φ")
  where "φ t s  (χ i. if i = 1 then s$1 * cos t + s$2 * sin t else - s$1 * sin t + s$2 * cos t)"

― ‹Verified by providing the dynamics›

lemma pendulum_dyn: "{s. r2 = (s$1)2 + (s$2)2}  fb (EVOL φ G T) {s. r2 = (s$1)2 + (s$2)2}"
  by force

― ‹Verified with differential invariants. ›

lemma pendulum_inv: "{s. r2 = (s$1)2 + (s$2)2}  fb (x´= f & G) {s. r2 = (s$1)2 + (s$2)2}"
  by (auto intro!: diff_invariant_rules poly_derivatives)

― ‹Verified with the flow. ›

lemma local_flow_pend: "local_flow f UNIV UNIV φ"
  apply(unfold_locales, simp_all add: local_lipschitz_def lipschitz_on_def vec_eq_iff, clarsimp)
    apply(rule_tac x="1" in exI, clarsimp, rule_tac x=1 in exI)
    apply(simp add: dist_norm norm_vec_def L2_set_def power2_commute UNIV_2)
  by (auto simp: forall_2 intro!: poly_derivatives)

lemma pendulum_flow: "{s. r2 = (s$1)2 + (s$2)2}  fb (x´= f & G) {s. r2 = (s$1)2 + (s$2)2}"
  by (force simp: local_flow.ffb_g_ode_subset[OF local_flow_pend])

no_notation fpend ("f")
        and pend_flow ("φ")


subsubsection ‹ Bouncing Ball ›

text ‹ A ball is dropped from rest at an initial height @{text "h"}. The motion is described with
the free-fall equations @{text "x' t = v t"} and @{text "v' t = g"} where @{text "g"} is the
constant acceleration due to gravity. The bounce is modelled with a variable assignment that
flips the velocity. That is, we model it as a completely elastic collision with the ground. We use 
@{text "s$1"} to represent the ball's height and @{text "s$2"} for its velocity. We prove that the 
ball remains above ground and below its initial resting position. ›

abbreviation fball :: "real  real^2  real^2" ("f")
  where "f g s  (χ i. if i = 1 then s$2 else g)"

abbreviation ball_flow :: "real  real  real^2  real^2" ("φ")
  where "φ g t s  (χ i. if i = 1 then g * t ^ 2/2 + s$2 * t + s$1 else g * t + s$2)"

― ‹Verified with differential invariants. ›

named_theorems bb_real_arith "real arithmetic properties for the bouncing ball."

lemma inv_imp_pos_le[bb_real_arith]:
  assumes "0 > g" and inv: "2 * g * x - 2 * g * h = v * v"
  shows "(x::real)  h"
proof-
  have "v * v = 2 * g * x - 2 * g * h  0 > g"
    using inv and 0 > g by auto
  hence obs:"v * v = 2 * g * (x - h)  0 > g  v * v  0"
    using left_diff_distrib mult.commute by (metis zero_le_square)
  hence "(v * v)/(2 * g) = (x - h)"
    by auto
  also from obs have "(v * v)/(2 * g)  0"
    using divide_nonneg_neg by fastforce
  ultimately have "h - x  0"
    by linarith
  thus ?thesis by auto
qed

lemma bouncing_ball_inv: "g < 0  h  0 
  {s. s$1 = h  s$2 = 0}  fb
  (LOOP (
    (x´=(f g) & (λ s. s$1  0) DINV (λs. 2 * g * s$1 - 2 * g * h - s$2 * s$2 = 0)) ;
    (IF (λ s. s$1 = 0) THEN (2 ::= (λs. - s$2)) ELSE skip))
  INV (λs. 0  s$1 2 * g * s$1 - 2 * g * h - s$2 * s$2 = 0))
  {s. 0  s$1  s$1  h}"
  apply(rule ffb_loopI, simp_all)
    apply(force, force simp: bb_real_arith)
  apply(rule ffb_g_odei)
  by (auto intro!: diff_invariant_rules poly_derivatives simp: bb_real_arith)

― ‹Verified with annotated dynamics. ›

lemma inv_conserv_at_ground[bb_real_arith]:
  assumes invar: "2 * g * x = 2 * g * h + v * v"
    and pos: "g * τ2 / 2 + v * τ + (x::real) = 0"
  shows "2 * g * h + (g * τ * (g * τ + v) + v * (g * τ + v)) = 0"
proof-
  from pos have "g * τ2  + 2 * v * τ + 2 * x = 0" by auto
  then have "g2 * τ2  + 2 * g * v * τ + 2 * g * x = 0"
    by (metis (mono_tags, hide_lams) Groups.mult_ac(1,3) mult_zero_right
        monoid_mult_class.power2_eq_square semiring_class.distrib_left)
  hence "g2 * τ2 + 2 * g * v * τ + v2 + 2 * g * h = 0"
    using invar by (simp add: monoid_mult_class.power2_eq_square)
  hence obs: "(g * τ + v)2 + 2 * g * h = 0"
    apply(subst power2_sum) by (metis (no_types, hide_lams) Groups.add_ac(2, 3)
        Groups.mult_ac(2, 3) monoid_mult_class.power2_eq_square nat_distrib(2))
  thus "2 * g * h + (g * τ * (g * τ + v) + v * (g * τ + v)) = 0"
    by (simp add: add.commute distrib_right power2_eq_square)
qed

lemma inv_conserv_at_air[bb_real_arith]:
  assumes invar: "2 * g * x = 2 * g * h + v * v"
  shows "2 * g * (g * τ2 / 2 + v * τ + (x::real)) =
  2 * g * h + (g * τ + v) * (g * τ + v)" (is "?lhs = ?rhs")
proof-
  have "?lhs = g2 * τ2 + 2 * g * v * τ + 2 * g * x"
    by(auto simp: algebra_simps semiring_normalization_rules(29))
  also have "... = g2 * τ2 + 2 * g * v * τ + 2 * g * h + v * v" (is "... = ?middle")
    by(subst invar, simp)
  finally have "?lhs = ?middle".
  moreover
  {have "?rhs = g * g * (τ * τ) + 2 * g * v * τ + 2 * g * h + v * v"
    by (simp add: Groups.mult_ac(2,3) semiring_class.distrib_left)
  also have "... = ?middle"
    by (simp add: semiring_normalization_rules(29))
  finally have "?rhs = ?middle".}
  ultimately show ?thesis by auto
qed

lemma bouncing_ball_dyn: "g < 0  h  0 
  {s. s$1 = h  s$2 = 0}  fb
  (LOOP (
    (EVOL (φ g) (λ s. s$1  0) T) ;
    (IF (λ s. s$1 = 0) THEN (2 ::= (λs. - s$2)) ELSE skip))
  INV (λs. 0  s$1  2 * g * s$1 = 2 * g * h + s$2 * s$2))
  {s. 0  s$1  s$1  h}"
  by (rule ffb_loopI) (auto simp: bb_real_arith)

― ‹Verified with the flow. ›

lemma local_flow_ball: "local_flow (f g) UNIV UNIV (φ g)"
  apply(unfold_locales, simp_all add: local_lipschitz_def lipschitz_on_def vec_eq_iff, clarsimp)
    apply(rule_tac x="1/2" in exI, clarsimp, rule_tac x=1 in exI)
    apply(simp add: dist_norm norm_vec_def L2_set_def UNIV_2)
  by (auto simp: forall_2 intro!: poly_derivatives)

lemma bouncing_ball_flow: "g < 0  h  0 
  {s. s$1 = h  s$2 = 0}  fb
  (LOOP (
    (x´=(λt. f g) & (λ s. s$1  0) on (λs. UNIV) UNIV @ 0) ;
    (IF (λ s. s$1 = 0) THEN (2 ::= (λs. - s$2)) ELSE skip))
  INV (λs. 0  s$1  2 * g * s$1 = 2 * g * h + s$2 * s$2))
  {s. 0  s$1  s$1  h}"
  by (rule ffb_loopI) (auto simp: bb_real_arith local_flow.ffb_g_ode[OF local_flow_ball])

no_notation fball ("f")
        and ball_flow ("φ")


subsubsection ‹ Thermostat ›

text ‹ A thermostat has a chronometer, a thermometer and a switch to turn on and off a heater.
At most every @{text "t"} minutes, it sets its chronometer to @{term "0::real"}, it registers
the room temperature, and it turns the heater on (or off) based on this reading. The temperature
follows the ODE @{text "T' = - a * (T - U)"} where @{text "U"} is @{text "L ≥ 0"} when the heater
is on, and @{text "0"} when it is off. We use @{term "1::4"} to denote the room's temperature,
@{term "2::4"} is time as measured by the thermostat's chronometer, @{term "3::4"} is the
temperature detected by the thermometer, and @{term "4::4"} states whether the heater is on
(@{text "s$4 = 1"}) or off (@{text "s$4 = 0"}). We prove that the thermostat keeps the room's
temperature between @{text "Tmin"} and @{text "Tmax"}. ›

abbreviation temp_vec_field :: "real  real  real^4  real^4" ("f")
  where "f a L s  (χ i. if i = 2 then 1 else (if i = 1 then - a * (s$1 - L) else 0))"

abbreviation temp_flow :: "real  real  real  real^4  real^4" ("φ")
  where "φ a L t s  (χ i. if i = 1 then - exp(-a * t) * (L - s$1) + L else
  (if i = 2 then t + s$2 else s$i))"

― ‹Verified with the flow. ›

lemma norm_diff_temp_dyn: "0 < a  f a L s1 - f a L s2 = ¦a¦ * ¦s1$1 - s2$1¦"
proof(simp add: norm_vec_def L2_set_def, unfold UNIV_4, simp)
  assume a1: "0 < a"
  have f2: "r ra. ¦(r::real) + - ra¦ = ¦ra + - r¦"
    by (metis abs_minus_commute minus_real_def)
  have "r ra rb. (r::real) * ra + - (r * rb) = r * (ra + - rb)"
    by (metis minus_real_def right_diff_distrib)
  hence "¦a * (s1$1 + - L) + - (a * (s2$1 + - L))¦ = a * ¦s1$1 + - s2$1¦"
    using a1 by (simp add: abs_mult)
  thus "¦a * (s2$1 - L) - a * (s1$1 - L)¦ = a * ¦s1$1 - s2$1¦"
    using f2 minus_real_def by presburger
qed

lemma local_lipschitz_temp_dyn:
  assumes "0 < (a::real)"
  shows "local_lipschitz UNIV UNIV (λt::real. f a L)"
  apply(unfold local_lipschitz_def lipschitz_on_def dist_norm)
  apply(clarsimp, rule_tac x=1 in exI, clarsimp, rule_tac x=a in exI)
  using assms
  apply(simp_all add: norm_diff_temp_dyn)
  apply(simp add: norm_vec_def L2_set_def, unfold UNIV_4, clarsimp)
  unfolding real_sqrt_abs[symmetric] by (rule real_le_lsqrt) auto

lemma local_flow_temp: "a > 0  local_flow (f a L) UNIV UNIV (φ a L)"
  by (unfold_locales, auto intro!: poly_derivatives local_lipschitz_temp_dyn simp: forall_4 vec_eq_iff)

lemma temp_dyn_down_real_arith:
  assumes "a > 0" and Thyps: "0 < Tmin" "Tmin  T" "T  Tmax"
    and thyps: "0  (t::real)" "τ{0..t}. τ  - (ln (Tmin / T) / a) "
  shows "Tmin  exp (-a * t) * T" and "exp (-a * t) * T  Tmax"
proof-
  have "0  t  t  - (ln (Tmin / T) / a)"
    using thyps by auto
  hence "ln (Tmin / T)  - a * t  - a * t  0"
    using assms(1) divide_le_cancel by fastforce
  also have "Tmin / T > 0"
    using Thyps by auto
  ultimately have obs: "Tmin / T  exp (-a * t)" "exp (-a * t)  1"
    using exp_ln exp_le_one_iff by (metis exp_less_cancel_iff not_less, simp)
  thus "Tmin  exp (-a * t) * T"
    using Thyps by (simp add: pos_divide_le_eq)
  show "exp (-a * t) * T  Tmax"
    using Thyps mult_left_le_one_le[OF _ exp_ge_zero obs(2), of T]
      less_eq_real_def order_trans_rules(23) by blast
qed

lemma temp_dyn_up_real_arith:
  assumes "a > 0"