Theory HS_VC_Spartan
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"
unbundle no rtrancl_syntax
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
abbreviation "skip ≡ (λs. {s})"
lemma fbox_eta[simp]: "fbox skip P = P"
unfolding fbox_def by simp
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
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
definition nondet_assign :: "'n ⇒ 'a^'n ⇒ ('a^'n) set" (‹(2_ ::= ? )› [70] 61)
where "(x ::= ?) = (λs. {(vec_upd s x k)|k. True})"
lemma fbox_nondet_assign[simp]: "|x ::= ?] P = (λs. ∀k. P (χ j. if j = x then k else s$j))"
unfolding fbox_def nondet_assign_def vec_upd_eq apply(simp add: fun_eq_iff, safe)
by (erule_tac x="(χ j. if j = x then k else _ $ j)" in allE, auto)
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
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)])
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
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)" (‹(‹notation=‹postfix kleene_star››_⇧*)› [1000] 999)
where "(f⇧*) s = ⋃ {kpower f n s |n. n ∈ UNIV}"
lemma kpower_inv:
fixes F :: "'a ⇒ 'a set"
assumes "∀s. I s ⟶ (∀s'. s' ∈ F s ⟶ I s')"
shows "∀s. I s ⟶ (∀s'. s' ∈ (kpower F n s) ⟶ I s')"
apply(clarsimp, induct n)
unfolding kpower_base kpower_simp
apply(simp_all add: kcomp_eq, clarsimp)
apply(subgoal_tac "I y", simp)
using assms by blast
lemma kstar_inv: "I ≤ |F] I ⟹ I ≤ |F⇧*] I"
unfolding kleene_star_def fbox_def
apply clarsimp
apply(unfold le_fun_def, subgoal_tac "∀x. I x ⟶ (∀s'. s' ∈ F x ⟶ I s')")
using kpower_inv[of I F] by blast simp
lemma fbox_kstarI:
assumes "P ≤ I" and "I ≤ Q" and "I ≤ |F] I"
shows "P ≤ |F⇧*] Q"
proof-
have "I ≤ |F⇧*] I"
using assms(3) kstar_inv by blast
hence "P ≤ |F⇧*] I"
using assms(1) by auto
also have "|F⇧*] I ≤ |F⇧*] Q"
by (rule fbox_iso[OF assms(2)])
finally show ?thesis .
qed
definition loopi :: "('a ⇒ 'a set) ⇒ 'a pred ⇒ ('a ⇒ 'a set)" (‹LOOP _ INV _ › [64,64] 63)
where "LOOP F INV I ≡ (F⇧*)"
lemma change_loopI: "LOOP X INV G = LOOP X INV I"
unfolding loopi_def by simp
lemma fbox_loopI: "P ≤ I ⟹ I ≤ Q ⟹ I ≤ |F] I ⟹ P ≤ |LOOP F INV I] Q"
unfolding loopi_def using fbox_kstarI[of "P"] by simp
lemma wp_loopI_break:
"P ≤ |Y] I ⟹ I ≤ |X] I ⟹ I ≤ Q ⟹ P ≤ |Y ; (LOOP X INV I)] Q"
by (rule hoare_kcomp, force) (rule fbox_loopI, auto)
subsection ‹ Verification of hybrid programs ›
text ‹ Verification by providing evolution ›
definition g_evol :: "(('a::ord) ⇒ 'b ⇒ 'b) ⇒ 'b pred ⇒ ('b ⇒ 'a set) ⇒ ('b ⇒ 'b set)" (‹EVOL›)
where "EVOL φ G U = (λs. g_orbit (λt. φ t s) G (U s))"
lemma fbox_g_evol[simp]:
fixes φ :: "('a::preorder) ⇒ 'b ⇒ 'b"
shows "|EVOL φ G U] Q = (λs. (∀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