# 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∥_∥)"  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 = 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"
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 "∀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)

― ‹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 "∀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}) ⇒
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 "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)" proof(simp add: tendsto_iff, clarify) fix ε::real assume "0 < ε" let "?Δ" = "λy. y - x⇩0" and "?Δf" = "λy. f y - f x⇩0" let "?P" = "λi e y. inverse ¦?Δ y¦ * (∥f y$ i - f x⇩0 $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 - x⇩0¦" and "?u t" = "λi. f t $i - f x⇩0$ 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. ?c⇧2 * ((∥?u t i∥))⇧2 < ε⇧2 / m" by (simp add: power_mult_distrib power_divide assms) hence "∀i. ?c⇧2 * ((∥?u t i∥))⇧2 < ε⇧2 / m" by (auto simp: assms) also have "({}::'m set) ≠ UNIV ∧ finite (UNIV :: 'm set)" by simp ultimately have "(∑i∈UNIV. ?c⇧2 * ((∥?u t i∥))⇧2) < (∑(i::'m)∈UNIV. ε⇧2 / m)" by (metis (lifting) sum_strict_mono) moreover have "?c⇧2 * (∑i∈UNIV. (∥?u t i∥)⇧2) = (∑i∈UNIV. ?c⇧2 * (∥?u t i∥)⇧2)" using sum_distrib_left by blast ultimately have "?c⇧2 * (∑i∈UNIV. (∥?u t i∥)⇧2) < ε⇧2" by (simp add: assms) hence "sqrt (?c⇧2 * (∑i∈UNIV. (∥?u t i∥)⇧2)) < sqrt (ε⇧2)" using real_sqrt_less_iff by blast also have "... = ε" using ‹0 < ε› by auto moreover have "?c * sqrt (∑i∈UNIV. (∥?u t i∥)⇧2) = sqrt (?c⇧2 * (∑i∈UNIV. (∥?u t i∥)⇧2))" by (simp add: real_sqrt_mult) ultimately show "?c * sqrt (∑i∈UNIV. (∥?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 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

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}) = (∀x∈A. G (f x))"
unfolding image_def by force

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

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

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

lemma in_ivp_sols_subset:
"t⇩0 ∈ (U s) ⟹ (U s) ⊆ (T s) ⟹ X ∈ Sols f T S t⇩0 s ⟹ X ∈ Sols f U S t⇩0 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 t⇩0 s = ⋃{γ X G (U s) |X. X ∈ ivp_sols f U S t⇩0 s}"

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

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

lemma g_orbitalD:
assumes "s' ∈ g_orbital f G U S t⇩0 s"
obtains X and t where "X ∈ Sols f U S t⇩0 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 t⇩0 s = {X t |t X. X t ∈ γ X G (U s) ∧ X ∈ Sols f U S t⇩0 s}"
unfolding g_orbital_eq g_orbit_eq by auto

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

lemma "g_orbital f G U S t⇩0 s ⊆ g_orbital f (λs. True) U S t⇩0 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 t⇩0 G ≡ (⋃ ∘ (𝒫 (g_orbital f G U S t⇩0))) {s. I s} ⊆ {s. I s}"

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

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

lemma "diff_invariant I f U S t⇩0 (λs. True) ⟹ diff_invariant I f U S t⇩0 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 t⇩0)) ⟹ (D (λτ. μ(X τ)-ν(X τ)) = ((*⇩R) 0) on U(X t⇩0))"
shows "diff_invariant (λs. μ s = ν s) f U S t⇩0 G"
proof(simp add: diff_invariant_eq ivp_sols_def, clarsimp)
fix X t
assume xivp:"D X = (λτ. f τ (X τ)) on U (X t⇩0)" "μ (X t⇩0) = ν (X t⇩0)" "X ∈ U (X t⇩0) → S"
and tHyp:"t ∈ U (X t⇩0)" and t0Hyp: "t⇩0 ∈ U (X t⇩0)"
hence "{t⇩0--t} ⊆ U (X t⇩0)"
using closed_segment_subset_interval[OF Uhyp t0Hyp tHyp] by blast
hence "D (λτ. μ (X τ) - ν (X τ)) = (λτ. τ *⇩R 0) on {t⇩0--t}"
using has_vderiv_on_subset[OF dX[OF xivp(1)]] by auto
then obtain τ where "μ (X t) - ν (X t) - (μ (X t⇩0) - ν (X t⇩0)) = (t - t⇩0) * τ *⇩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 t⇩0)) ⟹ (∀τ∈U(X t⇩0). τ > t⇩0 ⟶ G (X τ) ⟶ μ' (X τ) ≥ ν' (X τ))"
and Gl: "⋀X. (D X = (λτ. f τ (X τ)) on U(X t⇩0)) ⟹ (∀τ∈U(X t⇩0). τ < t⇩0 ⟶ μ' (X τ) ≤ ν' (X τ))"
and dX: "⋀X. (D X = (λτ. f τ (X τ)) on U(X t⇩0)) ⟹ D (λτ. μ(X τ)-ν(X τ)) = (λτ. μ'(X τ)-ν'(X τ)) on U(X t⇩0)"
shows "diff_invariant (λs. ν s ≤ μ s) f U S t⇩0 G"
proof(simp_all add: diff_invariant_eq ivp_sols_def, safe)
fix X t assume Ghyp: "∀τ. τ ∈ U (X t⇩0) ∧ τ ≤ t ⟶ G (X τ)"
assume xivp: "D X = (λx. f x (X x)) on U (X t⇩0)" "ν (X t⇩0) ≤ μ (X t⇩0)" "X ∈ U (X t⇩0) → S"
assume tHyp: "t ∈ U (X t⇩0)" and t0Hyp: "t⇩0 ∈ U (X t⇩0)"
hence obs1: "{t⇩0--t} ⊆ U (X t⇩0)" "{t⇩0<--<t} ⊆ U (X t⇩0)"
using closed_segment_subset_interval[OF Uhyp t0Hyp tHyp] xivp(3) segment_open_subset_closed
by (force, metis PiE ‹X t⇩0 ∈ S ⟹ {t⇩0--t} ⊆ U (X t⇩0)› dual_order.trans)
hence obs2: "D (λτ. μ (X τ) - ν (X τ)) = (λτ. μ' (X τ) - ν' (X τ)) on {t⇩0--t}"
using has_vderiv_on_subset[OF dX[OF xivp(1)]] by auto
{assume "t ≠ t⇩0"
then obtain r where rHyp: "r ∈ {t⇩0<--<t}"
and "(μ(X t)-ν(X t)) - (μ(X t⇩0)-ν(X t⇩0)) = (λτ. τ*(μ'(X r)-ν'(X r))) (t - t⇩0)"
using mvt_simple_closed_segmentE obs2 by blast
hence mvt: "μ(X t)-ν(X t) = (t - t⇩0)*(μ'(X r)-ν'(X r)) + (μ(X t⇩0)-ν(X t⇩0))"
by force
have primed: "⋀τ. τ ∈ U (X t⇩0) ⟹ τ > t⇩0 ⟹ G (X τ) ⟹ μ' (X τ) ≥ ν' (X τ)"
"⋀τ. τ ∈ U (X t⇩0) ⟹ τ < t⇩0 ⟹ μ' (X τ) ≤ ν' (X τ)"
using Gg[OF xivp(1)] Gl[OF xivp(1)] by auto
have "t > t⇩0 ⟹ r > t⇩0 ∧ G (X r)" "¬ t⇩0 ≤ t ⟹ r < t⇩0" "r ∈ U (X t⇩0)"
using ‹r ∈ {t⇩0<--<t}› obs1 Ghyp
unfolding open_segment_eq_real_ivl closed_segment_eq_real_ivl by auto
moreover have "r > t⇩0 ⟹ G (X r) ⟹ (μ'(X r)- ν'(X r)) ≥ 0" "r < t⇩0 ⟹ (μ'(X r)-ν'(X r)) ≤ 0"
using primed(1,2)[OF ‹r ∈ U (X t⇩0)›] by auto
ultimately have "(t - t⇩0) * (μ'(X r)-ν'(X r)) ≥ 0"
by (case_tac "t ≥ t⇩0", force, auto simp: split_mult_pos_le)
hence "(t - t⇩0) * (μ'(X r)-ν'(X r)) + (μ(X t⇩0)-ν(X t⇩0)) ≥ 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 t⇩0)) ⟹ (∀τ∈U(X t⇩0). τ > t⇩0 ⟶ G (X τ) ⟶ μ' (X τ) ≥ ν' (X τ))"
and Gl: "⋀X. (D X = (λτ. f τ (X τ)) on U(X t⇩0)) ⟹ (∀τ∈U(X t⇩0). τ < t⇩0 ⟶ μ' (X τ) ≤ ν' (X τ))"
and dX: "⋀X. (D X = (λτ. f τ (X τ)) on U(X t⇩0)) ⟹ D (λτ. μ(X τ)-ν(X τ)) = (λτ. μ'(X τ)-ν'(X τ)) on U(X t⇩0)"
shows "diff_invariant (λs. ν s < μ s) f U S t⇩0 G"
proof(simp_all add: diff_invariant_eq ivp_sols_def, safe)
fix X t assume Ghyp: "∀τ. τ ∈ U (X t⇩0) ∧ τ ≤ t ⟶ G (X τ)"
assume xivp: "D X = (λx. f x (X x)) on U (X t⇩0)" "ν (X t⇩0) < μ (X t⇩0)" "X ∈ U (X t⇩0) → S"
assume tHyp: "t ∈ U (X t⇩0)" and t0Hyp: "t⇩0 ∈ U (X t⇩0)"
hence obs1: "{t⇩0--t} ⊆ U (X t⇩0)" "{t⇩0<--<t} ⊆ U (X t⇩0)"
using closed_segment_subset_interval[OF Uhyp t0Hyp tHyp] xivp(3) segment_open_subset_closed
by (force, metis PiE ‹X t⇩0 ∈ S ⟹ {t⇩0--t} ⊆ U (X t⇩0)› dual_order.trans)
hence obs2: "D (λτ. μ (X τ) - ν (X τ)) = (λτ. μ' (X τ) - ν' (X τ)) on {t⇩0--t}"
using has_vderiv_on_subset[OF dX[OF xivp(1)]] by auto
{assume "t ≠ t⇩0"
then obtain r where rHyp: "r ∈ {t⇩0<--<t}"
and "(μ(X t)-ν(X t)) - (μ(X t⇩0)-ν(X t⇩0)) = (λτ. τ*(μ'(X r)-ν'(X r))) (t - t⇩0)"
using mvt_simple_closed_segmentE obs2 by blast
hence mvt: "μ(X t)-ν(X t) = (t - t⇩0)*(μ'(X r)-ν'(X r)) + (μ(X t⇩0)-ν(X t⇩0))"
by force
have primed: "⋀τ. τ ∈ U (X t⇩0) ⟹ τ > t⇩0 ⟹ G (X τ) ⟹ μ' (X τ) ≥ ν' (X τ)"
"⋀τ. τ ∈ U (X t⇩0) ⟹ τ < t⇩0 ⟹ μ' (X τ) ≤ ν' (X τ)"
using Gg[OF xivp(1)] Gl[OF xivp(1)] by auto
have "t > t⇩0 ⟹ r > t⇩0 ∧ G (X r)" "¬ t⇩0 ≤ t ⟹ r < t⇩0" "r ∈ U (X t⇩0)"
using ‹r ∈ {t⇩0<--<t}› obs1 Ghyp
unfolding open_segment_eq_real_ivl closed_segment_eq_real_ivl by auto
moreover have "r > t⇩0 ⟹ G (X r) ⟹ (μ'(X r)- ν'(X r)) ≥ 0" "r < t⇩0 ⟹ (μ'(X r)-ν'(X r)) ≤ 0"
using primed(1,2)[OF ‹r ∈ U (X t⇩0)›] by auto
ultimately have "(t - t⇩0) * (μ'(X r)-ν'(X r)) ≥ 0"
by (case_tac "t ≥ t⇩0", force, auto simp: split_mult_pos_le)
hence "(t - t⇩0) * (μ'(X r)-ν'(X r)) + (μ(X t⇩0)-ν(X t⇩0)) > 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 t⇩0 G ⟷ diff_invariant (λs. ν s > μ s) f U S t⇩0 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 t⇩0 G"
and "diff_invariant (λs. ν s > μ s) f U S t⇩0 G"
shows "diff_invariant (λs. ν s ≠ μ s) f U S t⇩0 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 t⇩0 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 ⟹ t⇩0 ≤ t"
and conts: "⋀X. (D X = (λτ. f τ (X τ)) on U(X t⇩0)) ⟹ continuous_on (𝒫 X (U (X t⇩0))) ν"
"⋀X. (D X = (λτ. f τ (X τ)) on U(X t⇩0)) ⟹ continuous_on (𝒫 X (U (X t⇩0))) μ"
and dI:"diff_invariant (λs. ν s ≠ μ s) f U S t⇩0 G"
shows "diff_invariant (λs. ν s < μ s) f U S t⇩0 G"
proof(unfold diff_invariant_eq ivp_sols_def, clarsimp)
fix X t assume Ghyp: "∀τ. τ ∈ U (X t⇩0) ∧ τ ≤ t ⟶ G (X τ)"
assume xivp: "D X = (λx. f x (X x)) on U (X t⇩0)" "ν (X t⇩0) < μ (X t⇩0)" "X ∈ U (X t⇩0) → S"
assume tHyp: "t ∈ U (X t⇩0)" and t0Hyp: "t⇩0 ∈ U (X t⇩0)"
hence "t⇩0 ≤ 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 t⇩0", 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 t⇩0)) (ν ∘ X)" and "continuous_on (U (X t⇩0)) (μ ∘ X)"
using xivp(1) conts by blast+
also have "{t⇩0--t} ⊆ U (X t⇩0)"
using closed_segment_subset_interval[OF Uhyp(1) t0Hyp tHyp] xivp(3) t0Hyp by auto
ultimately have "continuous_on {t⇩0--t} (λτ. ν (X τ))"
and "continuous_on {t⇩0--t} (λτ. μ (X τ))"
using continuous_on_subset by auto
then obtain τ where "τ ∈ {t⇩0--t}" "μ (X τ) = ν (X τ)"
using IVT_two_functions_real_ivl[OF _ _ xivp(2) ineq2] by force
hence "∀r∈down (U (X t⇩0)) τ. G (X r)" and "τ ∈ U (X t⇩0)"
using Ghyp ‹τ ∈ {t⇩0--t}› ‹t⇩0 ≤ t› ‹{t⇩0--t} ⊆ U (X t⇩0)›
by (auto simp: closed_segment_eq_real_ivl)
hence "μ (X τ) ≠ ν (X τ)"
using dI tHyp xivp(2) ivp_solsI[of X f U "X t⇩0", 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 I⇩1 f U S t⇩0 G"
and "diff_invariant I⇩2 f U S t⇩0 G"
shows "diff_invariant (λs. I⇩1 s ∧ I⇩2 s) f U S t⇩0 G"
using assms unfolding diff_invariant_def by auto

lemma diff_invariant_disj_rule [diff_invariant_rules]:
assumes "diff_invariant I⇩1 f U S t⇩0 G"
and "diff_invariant I⇩2 f U S t⇩0 G"
shows "diff_invariant (λs. I⇩1 s ∨ I⇩2 s) f U S t⇩0 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 "t⇩0 ∈ T"}.›

locale picard_lindeloef =
fixes f::"real ⇒ ('a::{heine_borel,banach}) ⇒ 'a" and T::"real set" and S::"'a set" and t⇩0::real
assumes open_domain: "open T" "open S"
and interval_time: "is_interval T"
and init_time: "t⇩0 ∈ 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 t⇩0
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 t⇩0 s"

lemma flow_has_vderiv_on_ex_ivl:
assumes "s ∈ S"
shows "D flow t⇩0 s = (λt. f t (flow t⇩0 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 t⇩0 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 t⇩0 s ∈ Sols f (λs. ex_ivl s) S t⇩0 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 t⇩0 s = {(x, t). t ∈ T ∧  x ∈ Sols f (λs. {t⇩0--t}) S t⇩0 s}"
unfolding ivp_sols_def csols_def solves_ode_def
using closed_segment_subset_domain init_time by auto

lemma subset_ex_ivlI:
"Y⇩1 ∈ Sols f (λs. T) S t⇩0 s ⟹ {t⇩0--t} ⊆ T ⟹ A ⊆ {t⇩0--t} ⟹ A ⊆ ex_ivl s"
apply(clarsimp simp: existence_ivl_def)
apply(subgoal_tac "t⇩0 ∈ T", clarsimp simp: csols_eq)
apply(rule_tac x=Y⇩1 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 "t⇩0 ∈ U" and "t ∈ U"
and "is_interval U" and "U ⊆ ex_ivl s"
and xivp: "D Y⇩1 = (λt. f t (Y⇩1 t)) on U" "Y⇩1 t⇩0 = s" "Y⇩1 ∈ U → S"
and yivp: "D Y⇩2 = (λt. f t (Y⇩2 t)) on U" "Y⇩2 t⇩0 = s" "Y⇩2 ∈ U → S"
shows "Y⇩1 t = Y⇩2 t"
proof-
have "t⇩0 ∈ T"
using assms existence_ivl_subset by auto
have key: "(flow t⇩0 s usolves_ode f from t⇩0) (ex_ivl s) S"
using flow_usolves_ode[OF ‹t⇩0 ∈ T› ‹s ∈ S›] .
hence "∀t∈U. Y⇩1 t = flow t⇩0 s t"
unfolding usolves_ode_from_def solves_ode_def apply safe
by (erule_tac x=Y⇩1 in allE, erule_tac x=U in allE, auto simp: assms)
also have "∀t∈U. Y⇩2 t = flow t⇩0 s t"
using key unfolding usolves_ode_from_def solves_ode_def apply safe
by (erule_tac x=Y⇩2 in allE, erule_tac x=U in allE, auto simp: assms)
ultimately show "Y⇩1 t = Y⇩2 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 {t⇩0--t}" "X t⇩0 = s" "X ∈ {t⇩0--t} → S" and "t ∈ T"
and yivp: "D Y = (λt. f t (Y t)) on {t⇩0--t}" "Y t⇩0 = s" "Y ∈ {t⇩0--t} → S" and "s ∈ S"
shows "X t = Y t"
apply(rule unique_solution[OF ‹s ∈ S›, of "{t⇩0--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 t⇩0 = s" "X ∈ ex_ivl s → S"
and "t ∈ ex_ivl s" and "s ∈ S"
shows "X t = flow t⇩0 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: "Y⇩1 ∈ Sols f U S t⇩0 s" and ivp2: "Y⇩2 ∈ Sols f U S t⇩0 s"
shows "Y⇩1 t = Y⇩2 t"
proof(rule unique_solution[OF ‹s ∈ S›, of "{t⇩0--t}"], simp_all)
have "t⇩0 ∈ U s"
using ivp_solsD[OF ivp1] by auto
hence obs0: "{t⇩0--t} ⊆ U s"
using closed_segment_subset_interval[OF ivl] ‹t ∈ U s› by blast
moreover have obs1: "Y⇩1 ∈ Sols f (λs. {t⇩0--t}) S t⇩0 s"
by (rule in_ivp_sols_subset[OF _ calculation(1) ivp1], simp)
moreover have obs2: "Y⇩2 ∈ Sols f (λs. {t⇩0--t}) S t⇩0 s"
by (rule in_ivp_sols_subset[OF _ calculation(1) ivp2], simp)
ultimately show "{t⇩0--t} ⊆ ex_ivl s"
apply(unfold existence_ivl_def csols_eq, clarsimp)
apply(rule_tac x=Y⇩1 in exI, rule_tac x=t in exI)
using ‹t ∈ U s› and ‹U s ⊆ T› by force
show "D Y⇩1 = (λt. f t (Y⇩1 t)) on {t⇩0--t}"
by (rule ivp_solsD[OF in_ivp_sols_subset[OF _ _ ivp1]], simp_all add: obs0)
show "D Y⇩2 = (λt. f t (Y⇩2 t)) on {t⇩0--t}"
by (rule ivp_solsD[OF in_ivp_sols_subset[OF _ _ ivp2]], simp_all add: obs0)
show "Y⇩1 t⇩0 = s" and "Y⇩2 t⇩0 = s"
using ivp_solsD[OF ivp1] ivp_solsD[OF ivp2] by auto
show "Y⇩1 ∈ {t⇩0--t} → S" and "Y⇩2 ∈ {t⇩0--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 t⇩0 s"
shows "g_orbital f G U S t⇩0 s = g_orbit Y G (U s)"
proof-
have eq1: "∀Z ∈ Sols f U S t⇩0 s. ∀t∈U s. Z t = Y t"
by (clarsimp, rule ivp_unique_solution[OF assms(1,2,3) _ _ ivp], auto)
have "g_orbital f G U S t⇩0 s ⊆ g_orbit (λt. Y t) G (U s)"
proof
fix x assume "x ∈ g_orbital f G U S t⇩0 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 t⇩0 s"
unfolding g_orbital_eq by auto
hence "{t⇩0--t} ⊆ U s"
using closed_segment_subset_interval[OF ivl ivp_solsD(4)[OF ivp]] by blast
hence "∀τ∈{t⇩0--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 t⇩0 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

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

lemma picard_lindeloef_add: "picard_lindeloef f1 T S t⇩0 ⟹ picard_lindeloef f2 T S t⇩0 ⟹
picard_lindeloef (λt s. f1 t s + f2 t s) T S t⇩0"
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 t⇩0"
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)

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 "φ (t⇩1 + t⇩2) s = φ t⇩1 (φ t⇩2 s)"
proof-
show "φ 0 s = s"
using ivp assms by simp
have "φ (0 + t⇩2) s = φ t⇩2 s"
by simp
also have "φ (0 + t⇩2) s ∈ S"
using in_domain assms by auto
ultimately show "φ (t⇩1 + t⇩2) s = φ t⇩1 (φ t⇩2 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 ("(_⇧*)"  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. F⇩1 s ⊆ F⇩2 s ⟹ |F⇩2] P ≤ |F⇩1] 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_ ::= ? )"  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)" ("(_⇧*)"  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. (∀t∈U 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 @ t⇩0] Q = (λs. ∀X∈Sols f U S t⇩0 s. ∀t∈U 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 ⟶ (∀t∈T. (∀τ∈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 @ t⇩0 DINV I) = (x´= f & G on U S @ t⇩0)" lemma fbox_g_orbital_guard: assumes "H = (λs. G s ∧ Q s)" shows "|x´=f & G on U S @ t⇩0] Q = |x´=f & G on U S @ t⇩0] 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 @ t⇩0] I" and "I ≤ Q" shows "P ≤ |x´=f & G on U S @ t⇩0] 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 @ t⇩0] I) = diff_invariant I f U S t⇩0 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 @ t⇩0] I" shows "I ≤ |x´= f & G on U S @ t⇩0] 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 @ t⇩0] I ⟹ (λs. I s ∧ G s) ≤ Q ⟹ P ≤ |x´= f & G on U S @ t⇩0 DINV I] Q" unfolding g_ode_inv_def apply(rule_tac b="|x´= f & G on U S @ t⇩0] 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. ∀t≥0. (∀τ∈{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. ∀t≥0. (∀τ∈{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 ⟶ (∀t≥0. (∀τ∈{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 @ t⇩0] G) s" unfolding fbox_def g_orbital_eq by auto lemma diff_weak_axiom2: "|x´= f & G on T S @ t⇩0] Q = |x´= f & G on T S @ t⇩0] (λ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 @ t⇩0] 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 @ t⇩0] C = (λs. True)" and "∀τ∈(down (U s) t). x τ ∈ (x´= f & G on U S @ t⇩0) s" shows "∀τ∈(down (U s) t). C (x τ)" proof fix τ assume "τ ∈ (down (U s) t)" hence "x τ ∈ (x´= f & G on U S @ t⇩0) s" using assms(2) by blast also have "∀s'. s' ∈ (x´= f & G on U S @ t⇩0) 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 @ t⇩0] C = (λs. True)" shows "|x´= f & G on U S @ t⇩0] Q = |x´= f & (λs. G s ∧ C s) on U S @ t⇩0] 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 @ t⇩0) s" then obtain τ::real and X where x_ivp: "X ∈ Sols f U S t⇩0 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 t⇩0 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 @ t⇩0) 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 @ t⇩0) s" using g_orbitalI[OF x_ivp ‹τ ∈ U s›] guard_x ‹X τ = s'› by fastforce} thus "(x´= f & G on U S @ t⇩0) s ⊆ (x´= f & (λs. G s ∧ C s) on U S @ t⇩0) s" by blast next show "⋀s. (x´= f & (λs. G s ∧ C s) on U S @ t⇩0) s ⊆ (x´= f & G on U S @ t⇩0) s" by (auto simp: g_orbital_eq) qed lemma diff_cut_rule: assumes fbox_C: "P ≤ |x´= f & G on U S @ t⇩0] C" and fbox_Q: "P ≤ |x´= f & (λs. G s ∧ C s) on U S @ t⇩0] Q" shows "P ≤ |x´= f & G on U S @ t⇩0] 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 t⇩0 s" and guard_x:"∀τ. τ ∈ U s ∧ τ ≤ t ⟶ G (X τ)" have "∀τ∈(down (U s) t). X τ ∈ (x´= f & G on U S @ t⇩0) 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 @ t⇩0) 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" = "∀X∈Sols (λt. f) (λs. {t. t ≥ 0}) UNIV 0 s. ∀t≥0. (∀τ. 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 t⇩0 G" and "I ≤ Q" shows "P ≤ |x´= f & G on U S @ t⇩0] 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. r⇧2 = (s$1)⇧2 + (s$2)⇧2) ≤ |EVOL φ G T] (λs. r⇧2 = (s$1)⇧2 + (s$2)⇧2)" by force ― ‹Verified with differential invariants. › lemma pendulum_inv: "(λs. r⇧2 = (s$1)⇧2 + (s$2)⇧2) ≤ |x´= f & G] (λs. r⇧2 = (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. r⇧2 = (s$1)⇧2 + (s$2)⇧2) ≤ |x´=f & G] (λs. r⇧2 = (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 t⇩0 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 "g⇧2 * τ⇧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 "g⇧2 * τ⇧2 + 2 * g * v * τ + v⇧2 + 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"
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 = g⇧2 * τ⇧2 + 2 * g * v * τ + 2 * g * x"
by(auto simp: algebra_simps semiring_normalization_rules(29))
also have "... = g⇧2 * τ⇧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 s⇩1 - f a L s⇩2∥ = ¦a¦ * ¦s⇩1$1 - s⇩2$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 * (s⇩1$1 + - L) + - (a * (s⇩2$1 + - L))¦ = a * ¦s⇩1$1 + - s⇩2$1¦"
using a1 by (simp add: abs_mult)
thus "¦a * (s⇩2$1 - L) - a * (s⇩1$1 - L)¦ = a * ¦s⇩1$1 - s⇩2$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_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 = c⇩i-c⇩o"} if the pump is on, and at a rate of @{text "k = -c⇩o"} 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 < c⇩o" and "c⇩o < c⇩i"
shows "∀τ∈{0..τ}. τ ≤ - ((hmin - y) / c⇩o) ⟹  hmin ≤ y - c⇩o * τ"
and "∀τ∈{0..τ}. τ ≤ (hmax - y) / (c⇩i - c⇩o) ⟹  (c⇩i - c⇩o) * τ + y ≤ hmax"
and "hmin ≤ y ⟹ hmin ≤ (c⇩i - c⇩o) * τ + y"
and "y ≤ hmax ⟹ y - c⇩o * τ ≤ 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 < c⇩o" and "c⇩o < c⇩i"
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 (c⇩i-c⇩o) & (G hmax (c⇩i-c⇩o)))
ELSE (x´= f (-c⇩o) & (G hmin (-c⇩o)))) ) 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 ("_⇧†"  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 = (⋂ ∘ 𝒫 (- op⇩K 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_ ::= ? )"  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. (∀t∈U 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 @ t⇩0) Q = {s. ∀X∈Sols f U S t⇩0 s. ∀t∈U 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 ⟶ (∀t∈T. (∀τ∈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 @ t⇩0 DINV I) = (x´= f & G on U S @ t⇩0)" lemma ffb_g_orbital_guard: assumes "H = (λs. G s ∧ Q s)" shows "fb⇩ℱ (x´= f & G on U S @ t⇩0) {s. Q s} = fb⇩ℱ (x´= f & G on U S @ t⇩0) {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 @ t⇩0) I" and "I ≤ Q" shows "P ≤ fb⇩ℱ (x´= f & G on U S @ t⇩0) 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 @ t⇩0) {s. I s}) = diff_invariant I f U S t⇩0 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 t⇩0 G = (bd⇩ℱ (x´= f & G on U S @ t⇩0) {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 @ t⇩0) {s. I s}" shows "{s. I s} ≤ fb⇩ℱ (x´= f & G on U S @ t⇩0) {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 @ t⇩0) {s. I s} ⟹ {s. I s ∧ G s} ≤ Q ⟹ P ≤ fb⇩ℱ (x´= f & G on U S @ t⇩0 DINV I) Q" unfolding g_ode_inv_def apply(rule_tac b="fb⇩ℱ (x´= f & G on U S @ t⇩0) {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. ∀t≥0. (∀τ∈{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. ∀t≥0. (∀τ∈{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 ⟶ (∀t≥0. (∀τ∈{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 @ t⇩0) {s. G s})" unfolding ffb_eq g_orbital_eq by auto lemma diff_weak_axiom2: "fb⇩ℱ (x´= f & G on T S @ t⇩0) Q = fb⇩ℱ (x´= f & G on T S @ t⇩0) {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 @ t⇩0) 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 @ t⇩0) {s. C s} = UNIV" and "∀τ∈(down (U s) t). x τ ∈ (x´= f & G on U S @ t⇩0) s" shows "∀τ∈(down (U s) t). C (x τ)" proof fix τ assume "τ ∈ (down (U s) t)" hence "x τ ∈ (x´= f & G on U S @ t⇩0) s" using assms(2) by blast also have "∀y. y ∈ (x´= f & G on U S @ t⇩0) 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 @ t⇩0) {s. C s} = UNIV" shows "fb⇩ℱ (x´= f & G on U S @ t⇩0) Q = fb⇩ℱ (x´= f & (λs. G s ∧ C s) on U S @ t⇩0) 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 @ t⇩0) s" then obtain τ::real and X where x_ivp: "X ∈ Sols f U S t⇩0 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 t⇩0 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 @ t⇩0) 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 @ t⇩0) 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 @ t⇩0) s ⊆ (x´= f & (λs. G s ∧ C s) on U S @ t⇩0) s" by blast next show "⋀s. (x´= f & (λs. G s ∧ C s) on U S @ t⇩0) s ⊆ (x´= f & G on U S @ t⇩0) s" by (auto simp: g_orbital_eq) qed lemma diff_cut_rule: assumes ffb_C: "P ≤ fb⇩ℱ (x´= f & G on U S @ t⇩0) {s. C s}" and ffb_Q: "P ≤ fb⇩ℱ (x´= f & (λs. G s ∧ C s) on U S @ t⇩0) Q" shows "P ≤ fb⇩ℱ (x´= f & G on U S @ t⇩0) 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 t⇩0 s" and guard_x:"∀τ. τ ∈ (U s) ∧ τ ≤ t ⟶ G (X τ)" have "∀τ∈(down (U s) t). X τ ∈ (x´= f & G on U S @ t⇩0) 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 @ t⇩0) 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" = "∀X∈Sols (λt. f) (λs. {t. t ≥ 0}) UNIV 0 s. ∀t≥0. (∀τ. 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 t⇩0 G" and "{s. I s} ≤ Q" shows "P ≤ fb⇩ℱ (x´= f & G on U S @ t⇩0) 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. r⇧2 = (s$1)⇧2 + (s$2)⇧2} ≤ fb⇩ℱ (EVOL φ G T) {s. r⇧2 = (s$1)⇧2 + (s$2)⇧2}" by force ― ‹Verified with differential invariants. › lemma pendulum_inv: "{s. r⇧2 = (s$1)⇧2 + (s$2)⇧2} ≤ fb⇩ℱ (x´= f & G) {s. r⇧2 = (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. r⇧2 = (s$1)⇧2 + (s$2)⇧2} ≤ fb⇩ℱ (x´= f & G) {s. r⇧2 = (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 "g⇧2 * τ⇧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 "g⇧2 * τ⇧2 + 2 * g * v * τ + v⇧2 + 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 = g⇧2 * τ⇧2 + 2 * g * v * τ + 2 * g * x" by(auto simp: algebra_simps semiring_normalization_rules(29)) also have "... = g⇧2 * τ⇧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 s⇩1 - f a L s⇩2∥ = ¦a¦ * ¦s⇩1$1 - s⇩2$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 * (s⇩1$1 + - L) + - (a * (s⇩2$1 + - L))¦ = a * ¦s⇩1$1 + - s⇩2$1¦" using a1 by (simp add: abs_mult) thus "¦a * (s⇩2$1 - L) - a * (s⇩1$1 - L)¦ = a * ¦s⇩1$1 - s⇩2\$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_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"