Theory HS_VC_MKA_ndfun
subsection ‹Verification of hybrid programs›
text ‹ We show that non-deterministic functions or state transformers form an antidomain
Kleene algebra. We use this algebra's forward box operator to derive rules for weakest liberal
preconditions (wlps) of regular programs. Finally, we derive our three methods for verifying
correctness specifications for the continuous dynamics of HS. ›
theory HS_VC_MKA_ndfun
imports
"../HS_ODEs"
"HS_VC_MKA"
"../HS_VC_KA_ndfun"
begin
instantiation nd_fun :: (type) antidomain_kleene_algebra
begin
definition "ad f = (λs. if ((f⇩∙) s = {}) then {s} else {})⇧∙"
lemma nd_fun_ad_zero[nd_fun_ka]: "ad x ⋅ x = 0"
and nd_fun_ad[nd_fun_ka]: "ad (x ⋅ y) + ad (x ⋅ ad (ad y)) = ad (x ⋅ ad (ad y))"
and nd_fun_ad_one[nd_fun_ka]: "ad (ad x) + ad x = 1" for x::"'a nd_fun"
unfolding antidomain_op_nd_fun_def times_nd_fun_def plus_nd_fun_def zero_nd_fun_def
by (auto simp: nd_fun_eq_iff kcomp_def one_nd_fun_def)
instance
apply intro_classes
using nd_fun_ka by simp_all
end
subsubsection ‹ Regular programs›
text‹ Now that we know that non-deterministic functions form an Antidomain Kleene Algebra, we give
a lifting operation from predicates to @{typ "'a nd_fun"} and use it to compute weakest liberal
preconditions.›
type_synonym 'a pred = "'a ⇒ bool"
notation fbox (‹wp›)
unbundle no floor_ceiling_syntax
no_notation Relation.relcomp (infixl ‹;› 75)
and Range_Semiring.antirange_semiring_class.ars_r (‹r›)
and antidomain_semiringl.ads_d (‹d›)
abbreviation p2ndf :: "'a pred ⇒ 'a nd_fun" (‹(1⌈_⌉)›)
where "⌈Q⌉ ≡ (λ x::'a. {s::'a. s = x ∧ Q s})⇧∙"
lemma p2ndf_simps[simp]:
"⌈P⌉ ≤ ⌈Q⌉ = (∀s. P s ⟶ Q s)"
"(⌈P⌉ = ⌈Q⌉) = (∀s. P s = Q s)"
"(⌈P⌉ ⋅ ⌈Q⌉) = ⌈λ s. P s ∧ Q s⌉"
"(⌈P⌉ + ⌈Q⌉) = ⌈λ s. P s ∨ Q s⌉"
"ad ⌈P⌉ = ⌈λs. ¬ P s⌉"
"d ⌈P⌉ = ⌈P⌉" "⌈P⌉ ≤ η⇧∙"
unfolding less_eq_nd_fun_def times_nd_fun_def plus_nd_fun_def ads_d_def
by (auto simp: nd_fun_eq_iff kcomp_def le_fun_def antidomain_op_nd_fun_def)
text ‹ Lemmas for verification condition generation ›
lemma wp_nd_fun: "wp F ⌈P⌉ = ⌈λs. ∀s'. s' ∈ ((F⇩∙) s) ⟶ P s'⌉"
apply(simp add: fbox_def antidomain_op_nd_fun_def)
by(rule nd_fun_ext, auto simp: Rep_comp_hom kcomp_prop)
abbreviation skip :: "'a nd_fun"
where "skip ≡ 1"
lemma wp_test[simp]: "wp ⌈P⌉ ⌈Q⌉ = ⌈λs. P s ⟶ Q s⌉"
by (subst wp_nd_fun, simp)
definition assign :: "'b ⇒ ('a^'b ⇒ 'a) ⇒ ('a^'b) nd_fun" (‹(2_ ::= _)› [70, 65] 61)
where "(x ::= e) = (λs. {vec_upd s x (e s)})⇧∙"
lemma wp_assign[simp]: "wp (x ::= e) ⌈Q⌉ = ⌈λs. Q (χ j. ((($) s)(x := (e s))) j)⌉"
unfolding wp_nd_fun nd_fun_eq_iff vec_upd_def assign_def by auto
definition nondet_assign :: "'b ⇒ ('a^'b) nd_fun" (‹(2_ ::= ? )› [70] 61)
where "(x ::= ?) = (λs. {(vec_upd s x k)|k. True})⇧∙"
lemma wp_nondet_assign[simp]: "wp (x ::= ?) ⌈P⌉ = ⌈λs. ∀k. P (χ j. ((($) s)(x := k)) j)⌉"
unfolding wp_nd_fun nondet_assign_def vec_upd_eq apply(clarsimp, safe)
by (erule_tac x="(χ j. if j = x then k else s $ j)" in allE, auto)
lemma le_wp_choice_iff: "⌈P⌉ ≤ wp (X + Y) ⌈Q⌉ ⟷ ⌈P⌉ ≤ wp X ⌈Q⌉ ∧ ⌈P⌉ ≤ wp Y ⌈Q⌉"
using le_fbox_choice_iff[of "⌈P⌉"] by simp
abbreviation seq_comp :: "'a nd_fun ⇒ 'a nd_fun ⇒ 'a nd_fun" (infixl ‹;› 75)
where "f ; g ≡ f ⋅ g"
abbreviation cond_sugar :: "'a pred ⇒ 'a nd_fun ⇒ 'a nd_fun ⇒ 'a nd_fun" (‹IF _ THEN _ ELSE _› [64,64] 63)
where "IF P THEN X ELSE Y ≡ aka_cond ⌈P⌉ X Y"
abbreviation loopi_sugar :: "'a nd_fun ⇒ 'a pred ⇒ 'a nd_fun" (‹LOOP _ INV _ › [64,64] 63)
where "LOOP R INV I ≡ aka_loopi R ⌈I⌉"
lemma change_loopI: "LOOP X INV G = LOOP X INV I"
by (unfold aka_loopi_def, simp)
lemma wp_loopI: "⌈P⌉ ≤ ⌈I⌉ ⟹ ⌈I⌉ ≤ ⌈Q⌉ ⟹ ⌈I⌉ ≤ wp R ⌈I⌉ ⟹ ⌈P⌉ ≤ wp (LOOP R INV I) ⌈Q⌉"
using fbox_loopi[of "⌈P⌉"] by auto
lemma wp_loopI_break:
"⌈P⌉ ≤ wp Y ⌈I⌉ ⟹ ⌈I⌉ ≤ wp X ⌈I⌉ ⟹ ⌈I⌉ ≤ ⌈Q⌉ ⟹ ⌈P⌉ ≤ wp (Y ; (LOOP X INV I)) ⌈Q⌉"
using fbox_loopi_break[of "⌈P⌉"] by auto
subsubsection ‹ Evolution commands ›
text ‹Verification by providing evolution›
definition g_evol :: "(('a::ord) ⇒ 'b ⇒ 'b) ⇒ 'b pred ⇒ ('b ⇒ 'a set) ⇒ 'b nd_fun" (‹EVOL›)
where "EVOL φ G T = (λs. g_orbit (λt. φ t s) G (T s))⇧∙"
lemma wp_g_dyn[simp]:
fixes φ :: "('a::preorder) ⇒ 'b ⇒ 'b"
shows "wp (EVOL φ G U) ⌈Q⌉ = ⌈λs. ∀t∈U s. (∀τ∈down (U s) t. G (φ τ s)) ⟶ Q (φ t s)⌉"
unfolding wp_nd_fun g_evol_def g_orbit_eq by (auto simp: fun_eq_iff)
text ‹Verification by providing solutions›
definition g_ode ::"(real ⇒ ('a::banach) ⇒ 'a) ⇒ 'a pred ⇒ ('a ⇒ real set) ⇒ 'a set ⇒
real ⇒ 'a nd_fun" (‹(1x´= _ & _ on _ _ @ _)›)
where "(x´= f & G on U S @ t⇩0) ≡ (λ s. g_orbital f G U S t⇩0 s)⇧∙"
lemma wp_g_orbital: "wp (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 g_orbital_eq(1) wp_nd_fun g_ode_def by (auto simp: fun_eq_iff)
context local_flow
begin
lemma wp_g_ode_subset:
assumes "⋀s. s ∈ S ⟹ 0 ∈ U s ∧ is_interval (U s) ∧ U s ⊆ T"
shows "wp (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 wp_g_orbital, clarsimp, 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 s) t. X τ = φ τ s")
apply(clarsimp, fastforce, rule ballI)
apply(rule ivp_unique_solution[OF _ _ _ _ _ in_ivp_sols])
using assms by auto
lemma wp_g_ode: "wp (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 wp_g_ode_subset, simp_all add: init_time interval_time)
lemma wp_g_ode_ivl: "t ≥ 0 ⟹ t ∈ T ⟹ wp (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 wp_g_ode_subset, simp_all add: subintervalI init_time real_Icc_closed_segment)
by (auto simp: closed_segment_eq_real_ivl)
lemma wp_orbit: "wp (γ⇧φ⇧∙) ⌈Q⌉ = ⌈λ s. s ∈ S ⟶ (∀ t ∈ T. Q (φ t s))⌉"
unfolding orbit_def wp_g_ode g_ode_def[symmetric] by auto
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 nd_fun" (‹(1x´=_ & _ on _ _ @ _ DINV _ )›)
where "(x´= f & G on U S @ t⇩0 DINV I) = (x´= f & G on U S @ t⇩0)"
lemma wp_g_orbital_guard:
assumes "H = (λs. G s ∧ Q s)"
shows "wp (x´= f & G on U S @ t⇩0) ⌈Q⌉ = wp (x´= f & G on U S @ t⇩0) ⌈H⌉"
unfolding wp_g_orbital using assms by auto
lemma wp_g_orbital_inv:
assumes "⌈P⌉ ≤ ⌈I⌉" and "⌈I⌉ ≤ wp (x´= f & G on U S @ t⇩0) ⌈I⌉" and "⌈I⌉ ≤ ⌈Q⌉"
shows "⌈P⌉ ≤ wp (x´= f & G on U S @ t⇩0) ⌈Q⌉"
using assms(1)
apply(rule order.trans)
using assms(2)
apply(rule order.trans)
apply(rule fbox_iso)
using assms(3) by auto
lemma wp_diff_inv[simp]: "(⌈I⌉ ≤ wp (x´= f & G on U S @ t⇩0) ⌈I⌉) = diff_invariant I f U S t⇩0 G"
unfolding diff_invariant_eq wp_g_orbital by(auto simp: fun_eq_iff)
lemma diff_inv_guard_ignore:
assumes "⌈I⌉ ≤ wp (x´= f & (λs. True) on U S @ t⇩0) ⌈I⌉"
shows "⌈I⌉ ≤ wp (x´= f & G on U S @ t⇩0) ⌈I⌉"
using assms unfolding wp_diff_inv diff_invariant_eq by auto
context local_flow
begin
lemma wp_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⌉ = wp (x´= (λt. f) & (λs. True) on U S @ 0) ⌈λs. s ∈ S ⟶ I s⌉)"
unfolding wp_diff_inv[symmetric]
apply(subst wp_g_ode_subset[OF assms], simp)+
apply(clarsimp, safe, force)
apply(erule_tac x=0 in ballE)
using init_time in_domain ivp(2) assms apply(force, force)
apply(erule_tac x=s 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 auto
end
lemma wp_g_odei: "⌈P⌉ ≤ ⌈I⌉ ⟹ ⌈I⌉ ≤ wp (x´= f & G on U S @ t⇩0) ⌈I⌉ ⟹ ⌈λs. I s ∧ G s⌉ ≤ ⌈Q⌉ ⟹
⌈P⌉ ≤ wp (x´= f & G on U S @ t⇩0 DINV I) ⌈Q⌉"
unfolding g_ode_inv_def
apply(rule_tac b="wp (x´= f & G on U S @ t⇩0) ⌈I⌉" in order.trans)
apply(rule_tac I="I" in wp_g_orbital_inv, simp_all)
apply(subst wp_g_orbital_guard, simp)
by (rule fbox_iso, simp)
subsubsection ‹ 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 nd_fun" (‹(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 nd_fun" (‹(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 "wp (x´= f & G) ⌈Q⌉ =
⌈λs. ∀t≥0. (∀τ∈{0..t}. G (φ τ s)) ⟶ Q (φ t s)⌉"
by (subst local_flow.wp_g_ode_subset[OF assms], auto)
lemma diff_solve_axiom2:
fixes c::"'a::{heine_borel, banach}"
shows "wp (x´=(λs. c) & G) ⌈Q⌉ =
⌈λs. ∀t≥0. (∀τ∈{0..t}. G (s + τ *⇩R c)) ⟶ Q (s + t *⇩R c)⌉"
apply(subst local_flow.wp_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. P s ⟶ (∀t≥0. (∀τ∈{0..t}. G (φ τ s)) ⟶ Q (φ t s))"
shows "⌈P⌉ ≤ wp (x´= f & G) ⌈Q⌉"
using assms by (subst local_flow.wp_g_ode_subset[OF assms(1)], auto)
lemma diff_weak_axiom1: "η⇧∙ ≤ wp (x´= f & G on U S @ t⇩0) ⌈G⌉"
unfolding wp_nd_fun g_ode_def g_orbital_eq less_eq_nd_fun_def
by (auto simp: le_fun_def)
lemma diff_weak_axiom2:
"wp (x´= f & G on T S @ t⇩0) ⌈Q⌉ = wp (x´= f & G on T S @ t⇩0) ⌈λ s. G s ⟶ Q s⌉"
unfolding wp_g_orbital image_def by force
lemma diff_weak_rule:
assumes "⌈G⌉ ≤ ⌈Q⌉"
shows "⌈P⌉ ≤ wp (x´= f & G on U S @ t⇩0) ⌈Q⌉"
using assms by (auto simp: wp_g_orbital)
lemma wp_g_orbit_IdD:
assumes "wp (x´= f & G on U S @ t⇩0) ⌈C⌉ = η⇧∙"
and "∀τ∈(down (U s) t). x τ ∈ g_orbital f G U S t⇩0 s"
shows "∀τ∈(down (U s) t). C (x τ)"
proof
fix τ assume "τ ∈ (down (U s) t)"
hence "x τ ∈ g_orbital f G U S t⇩0 s"
using assms(2) by blast
also have "∀y. y ∈ (g_orbital f G U S t⇩0 s) ⟶ C y"
using assms(1) unfolding wp_nd_fun g_ode_def
by (subst (asm) nd_fun_eq_iff) auto
ultimately show "C (x τ)"
by blast
qed
lemma diff_cut_axiom:
assumes "wp (x´= f & G on U S @ t⇩0) ⌈C⌉ = η⇧∙"
shows "wp (x´= f & G on U S @ t⇩0) ⌈Q⌉ = wp (x´= f & (λs. G s ∧ C s) on U S @ t⇩0) ⌈Q⌉"
proof(rule_tac f="λ x. wp x ⌈Q⌉" in HOL.arg_cong, rule nd_fun_ext, rule subset_antisym)
fix s show "((x´= f & G on U S @ t⇩0)⇩∙) s ⊆ ((x´= f & (λs. G s ∧ C s) on U S @ t⇩0)⇩∙) s"
proof(clarsimp simp: g_ode_def)
fix s' assume "s' ∈ g_orbital f G U S t⇩0 s"
then obtain τ::real and X where x_ivp: "X ∈ ivp_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)› by auto
ultimately have "∀t∈(down (U s) τ). X t ∈ g_orbital f G 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 wp_g_orbit_IdD[OF assms(1)] by blast
thus "s' ∈ g_orbital f (λs. G s ∧ C s) U S t⇩0 s"
using g_orbitalI[OF x_ivp ‹τ ∈ (U s)›] guard_x ‹X τ = s'› by fastforce
qed
next
fix s show "((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 g_ode_def)
qed
lemma diff_cut_rule:
assumes wp_C: "⌈P⌉ ≤ wp (x´= f & G on U S @ t⇩0) ⌈C⌉"
and wp_Q: "⌈P⌉ ≤ wp (x´= f & (λs. G s ∧ C s) on U S @ t⇩0) ⌈Q⌉"
shows "⌈P⌉ ≤ wp (x´= f & G on U S @ t⇩0) ⌈Q⌉"
proof(simp add: wp_nd_fun g_orbital_eq g_ode_def, clarsimp)
fix t::real and X::"real ⇒ 'a" and s assume "P s" and "t ∈ U s"
and x_ivp:"X ∈ ivp_sols f U S t⇩0 s"
and guard_x:"∀x. x ∈ U s ∧ x ≤ t ⟶ G (X x)"
have "∀t∈(down (U s) t). X t ∈ g_orbital f G U S t⇩0 s"
using g_orbitalI[OF x_ivp] guard_x by auto
hence "∀t∈(down (U s) t). C (X t)"
using wp_C ‹P s› by (subst (asm) wp_nd_fun, auto simp: g_ode_def)
hence "X t ∈ g_orbital f (λs. G s ∧ C s) 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› wp_Q by (subst (asm) wp_nd_fun) (auto simp: g_ode_def)
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 ∈ ((wp (x´= f & G) ⌈I⌉)⇩∙) s"
using assms unfolding wp_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 "wp (x´= f & G) ⌈I⌉ = wp ⌈G⌉ ⌈I⌉"
proof(unfold wp_g_orbital, subst wp_nd_fun, 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⌉ ≤ wp (x´= f & G on U S @ t⇩0) ⌈Q⌉"
apply(rule wp_g_orbital_inv[OF assms(1) _ assms(3)])
unfolding wp_diff_inv using assms(2) .
end