Theory HS_Preliminaries

(*  Title:       Preliminaries for hybrid systems verification
    Author:      Jonathan Julián Huerta y Munive, 2021
    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

― ‹ Notation ›

bundle derivative_notation
begin

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)

end

bundle derivative_no_notation
begin

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

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

end

unbundle derivative_notation

notation norm ("_")

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

lemma sum_eq_Sum:
  assumes "inj_on f A"
  shows "(xA. f x) = ( {f x |x. x  A})"
proof-
  have "( {f x |x. x  A}) = ( (f ` A))"
    apply(auto simp: image_def)
    by (rule_tac f=Sum in arg_cong, auto)
  also have "... = (xA. f x)"
    by (subst sum.image_eq[OF assms], simp)
  finally show "(xA. f x) = ( {f x |x. x  A})"
    by simp
qed

lemma triangle_norm_vec_le_sum: "x  (iUNIV. x $ i)"
  by (simp add: L2_set_le_sum norm_vec_def)


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 has_derivative_vec_nth[derivative_intros]: 
  "D (λs. s $ i)  (λs. s $ i) (at x within S)"
  by (clarsimp simp: has_derivative_within) standard

lemma bounded_linear_component:
  "(bounded_linear f)  (i. bounded_linear (λx. (f x) $ i))" (is "?lhs = ?rhs")
proof
  assume ?lhs 
  thus ?rhs
    apply(clarsimp, rule_tac f="(λx. x $ i)" in bounded_linear_compose)
     apply(simp_all add: bounded_linear_def bounded_linear_axioms_def linear_iff)
    by (rule_tac x=1 in exI, clarsimp) (meson Finite_Cartesian_Product.norm_nth_le)
next
  assume ?rhs
  hence "(i. K. x. f x $ i  x * K)" "linear f"
    by (auto simp: bounded_linear_def bounded_linear_axioms_def linear_iff vec_eq_iff)
  then obtain F where F: "i x. f x $ i  x * F i"
    by metis
  have "f x  x * sum F UNIV" for x
  proof -
    have "norm (f x)  (iUNIV. f x $ i)"
      by (simp add: L2_set_le_sum norm_vec_def)
    also have "...  (iUNIV. norm x * F i)"
      by (metis F sum_mono)
    also have "... = norm x * sum F UNIV"
      by (simp add: sum_distrib_left)
    finally show ?thesis .
  qed
  then show ?lhs
    by (force simp: bounded_linear_def bounded_linear_axioms_def linear f)
qed

lemma open_preimage_nth:
  "open S  open {s::('a::real_normed_vector^'n::finite). s $ i  S}"
  unfolding open_contains_ball apply clarsimp
  apply(erule_tac x="x$i" in ballE; clarsimp)
  apply(rule_tac x=e in exI; clarsimp simp: dist_norm subset_eq ball_def)
  apply(rename_tac x e y, erule_tac x="y$i" in allE)
  using Finite_Cartesian_Product.norm_nth_le
  by (metis le_less_trans vector_minus_component)

lemma tendsto_nth_iff: ― ‹ following @{thm tendsto_componentwise_iff}
  fixes l::"'a::real_normed_vector^'n::finite"
  defines "m  real CARD('n)"
  shows "(f  l) F  (i. ((λx. f x $ i)  l $ i) F)" (is "?lhs = ?rhs")
proof
  assume ?lhs
  thus ?rhs
    unfolding tendsto_def
    by (clarify, drule_tac x="{s. s $ i  S}" in spec) (auto simp: open_preimage_nth)
next
  assume ?rhs
  thus ?lhs
  proof(unfold tendsto_iff dist_norm, clarify)
    fix ε::real assume "0 < ε"
    assume evnt_h: "i ε. 0 < ε  (F x in F. f x $ i - l $ i < ε)"
    {fix x assume hyp: "i. f x $ i - l $ i < (ε/m)"
      have "f x - l  (iUNIV. f x $ i - l $ i)"
        using triangle_norm_vec_le_sum[of "f x - l"] by auto
      also have "... < ((i::'n)UNIV. (ε/m))"
        apply(rule sum_strict_mono[of UNIV "λi. f x $ i - l $ i" "λi. ε/m"])
        using hyp by auto
      also have "... = m * (ε/m)"
        unfolding assms by simp
      finally have "f x - l < ε" 
        unfolding assms by simp}
    hence key: "x. i. f x $ i - l $ i < (ε/m)  f x - l < ε"
      by blast
    have obs: "F x in F. i. f x $ i - l $ i < (ε/m)"
      apply(rule eventually_all_finite)
      using 0 < ε evnt_h unfolding assms by auto
    thus "F x in F. f x - l < ε"
      by (rule eventually_mono[OF _ key], simp)
  qed
qed

lemma has_derivative_component[simp]: ― ‹ following @{thm has_derivative_componentwise_within}
  "(D f  f' at x within S)  (i. D (λs. f s $ i)  (λs. f' s $ i) at x within S)"
  by (simp add: has_derivative_within tendsto_nth_iff 
      bounded_linear_component all_conj_distrib)

lemma has_vderiv_on_component[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 by auto

lemma frechet_tendsto_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)"
  using assms by (simp add: tendsto_nth_iff)

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_tendsto_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

end