Theory HS_Preliminaries
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
open_bundle derivative_syntax
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
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 = x⇧2 + y⇧2"
and "(x * cos t + y * sin t)⇧2 + (y * cos t - x * sin t)⇧2 = x⇧2 + y⇧2"
proof-
have "(x * cos t - y * sin t)⇧2 = x⇧2 * (cos t)⇧2 + y⇧2 * (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 = y⇧2 * (cos t)⇧2 + x⇧2 * (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 = x⇧2 + y⇧2"
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 = x⇧2 + y⇧2"
by (simp add: add.commute add.left_commute power2_diff power2_sum)
qed
lemma sum_eq_Sum:
assumes "inj_on f A"
shows "(∑x∈A. 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 "... = (∑x∈A. f x)"
by (subst sum.image_eq[OF assms], simp)
finally show "(∑x∈A. f x) = (∑ {f x |x. x ∈ A})"
by simp
qed
lemma triangle_norm_vec_le_sum: "∥x∥ ≤ (∑i∈UNIV. ∥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 "∀t∈T. 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)
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 "∀t∈T. 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 * t⇧2 / 2 + v * t + x) = (λt. a * t + v) on T"
by(auto intro!: poly_derivatives)
lemma "D (λt. v * t - a * t⇧2 / 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) ≤ (∑i∈UNIV. ∥f x $ i∥)"
by (simp add: L2_set_le_sum norm_vec_def)
also have "... ≤ (∑i∈UNIV. 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:
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∥ ≤ (∑i∈UNIV. ∥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]:
"(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 "x⇩0 ≡ netlimit (at x within T)" and "m ≡ real CARD('m)"
assumes "∀i. ((λy. (f y $ i - f x⇩0 $ i - (y - x⇩0) *⇩R f' x $ i) /⇩R (∥y - x⇩0∥)) ⤏ 0) (at x within T)"
shows "((λy. (f y - f x⇩0 - (y - x⇩0) *⇩R f' x) /⇩R (∥y - x⇩0∥)) ⤏ 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 x⇩0 - (x - x⇩0) *⇩R f' t) /⇩R (∥x - x⇩0∥)) ⤏ 0) (at t within T)"
shows "((λx. (f x $ i - f x⇩0 $ i - (x - x⇩0) *⇩R f' t $ i) /⇩R (∥x - x⇩0∥)) ⤏ 0) (at t within T)"
apply(rule_tac F="(λx. (f x - f x⇩0 - (x - x⇩0) *⇩R f' t) /⇩R (∥x - x⇩0∥))" 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