Theory HS_VC_KAT_Examples_ndfun
subsection ‹ Examples ›
text ‹ We prove partial correctness specifications of some hybrid systems with our
refinement and verification components.›
theory HS_VC_KAT_Examples_ndfun
imports
HS_VC_KAT_ndfun
"HOL-Eisbach.Eisbach"
begin
named_theorems hoare_intros
declare H_assignl [hoare_intros]
and H_cond [hoare_intros]
and local_flow.H_g_ode_subset [hoare_intros]
and H_g_ode_inv [hoare_intros]
method body_hoare
= (rule hoare_intros,(simp)?; body_hoare?)
method hyb_hoare for P::"'a pred"
= (rule H_loopI, rule H_seq[where R=P]; body_hoare?)
named_theorems refine_intros "selected refinement lemmas"
declare R_loopI [refine_intros]
and R_loop_mono [refine_intros]
and R_cond_law [refine_intros]
and R_cond_mono [refine_intros]
and R_while_law [refine_intros]
and R_assignl [refine_intros]
and R_seq_law [refine_intros]
and R_seq_mono [refine_intros]
and R_g_evol_law [refine_intros]
and R_skip [refine_intros]
and R_g_ode_inv [refine_intros]
method refinement
= (rule refine_intros; (refinement)?)
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 "φ τ s ≡ (χ i. if i = 1 then s$1 ⋅ cos τ + s$2 ⋅ sin τ
else - s$1 ⋅ sin τ + s$2 ⋅ cos τ)"
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 simp
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)
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 (subst local_flow.sH_g_ode_subset[OF local_flow_pend], simp_all)
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 τ s ≡ (χ i. if i=1 then g ⋅ τ ^ 2/2 + s$2 ⋅ τ + s$1 else g ⋅ τ + s$2)"
named_theorems bb_real_arith "real arithmetic properties for the bouncing ball."
lemma [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 fball_invariant:
fixes g h :: real
defines dinv: "I ≡ (λs. 2 ⋅ g ⋅ s$1 - 2 ⋅ g ⋅ h - (s$2 ⋅ s$2) = 0)"
shows "diff_invariant I (λt. f g) (λs. UNIV) UNIV 0 G"
unfolding dinv apply(rule diff_invariant_rules, simp)
by(auto intro!: poly_derivatives)
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)
) ❙{λs. 0 ≤ s$1 ∧ s$1 ≤ h❙}"
apply(hyb_hoare "λs::real^2. 0 ≤ s$1 ∧ 2 ⋅ g ⋅ s$1 = 2 ⋅ g ⋅ h + s$2 ⋅ s$2")
using fball_invariant by (auto simp: bb_real_arith intro!: poly_derivatives diff_invariant_rules)
lemma [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"
and "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) 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) 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: monoid_mult_class.power2_eq_square)
have "2 ⋅ g ⋅ h + (- ((g ⋅ τ) + v))⇧2 = 0"
using obs by (metis Groups.add_ac(2) power2_minus)
thus "2 ⋅ g ⋅ h + (- (g ⋅ τ) - v) ⋅ (- (g ⋅ τ) - v) = 0"
by (simp add: monoid_mult_class.power2_eq_square)
qed
lemma [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 ⋅ τ ⋅ (g ⋅ τ + v) + 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❙}"
apply(hyb_hoare "λs::real^2. 0 ≤ s$1 ∧ 2 ⋅ g ⋅ s$1 = 2 ⋅ g ⋅ h + s$2 ⋅ s$2")
by (auto simp: bb_real_arith)
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´= f g & (λ s. s$1 ≥ 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 H_loopI; (rule H_seq[where R="λs. 0 ≤ s$1 ∧ 2 ⋅ g ⋅ s$1 = 2 ⋅ g ⋅ h + s$2 ⋅ s$2"])?)
apply(subst local_flow.sH_g_ode_subset[OF local_flow_ball])
by (auto simp: bb_real_arith)
lemma R_bb_assign: "g < (0::real) ⟹ 0 ≤ h ⟹
2 ::= (λs. - s$2) ≤ Ref
⌈λs. s$1 = 0 ∧ 0 ≤ s$1 ∧ 2 ⋅ g ⋅ s$1 = 2 ⋅ g ⋅ h + s$2 ⋅ s$2⌉
⌈λs. 0 ≤ s$1 ∧ 2 ⋅ g ⋅ s$1 = 2 ⋅ g ⋅ h + s$2 ⋅ s$2⌉"
by (rule R_assign_law, auto)
lemma R_bouncing_ball_dyn:
assumes "g < 0" and "h ≥ 0"
shows "Ref ⌈λs. s$1 = h ∧ s$2 = 0⌉ ⌈λs. 0 ≤ s$1 ∧ s$1 ≤ h⌉ ≥
(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))"
apply(refinement; (rule R_bb_assign[OF assms])?)
using assms 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 therm_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 therm_guard :: "real ⇒ real ⇒ real ⇒ real ⇒ real^4 ⇒ bool" (‹G›)
where "G Tmin Tmax a L s ≡ (s$2 ≤ - (ln ((L-(if L=0 then Tmin else Tmax))/(L-s$3)))/a)"
abbreviation therm_loop_inv :: "real ⇒ real ⇒ real^4 ⇒ bool" (‹I›)
where "I Tmin Tmax s ≡ Tmin ≤ s$1 ∧ s$1 ≤ Tmax ∧ (s$4 = 0 ∨ s$4 = 1)"
abbreviation therm_flow :: "real ⇒ real ⇒ real ⇒ real^4 ⇒ real^4" (‹φ›)
where "φ a L τ s ≡ (χ i. if i = 1 then - exp(-a * τ) * (L - s$1) + L else
(if i = 2 then τ + s$2 else s$i))"
lemma norm_diff_therm_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_therm_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_all add: norm_diff_therm_dyn)
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_therm: "a > 0 ⟹ local_flow (f a L) UNIV UNIV (φ a L)"
by (unfold_locales, auto intro!: poly_derivatives local_lipschitz_therm_dyn
simp: forall_4 vec_eq_iff)
lemma therm_dyn_down_real_arith:
assumes "a > 0" and Thyps: "0 < Tmin" "Tmin ≤ T" "T ≤ Tmax"
and thyps: "0 ≤ (τ::real)" "∀τ∈{0..τ}. τ ≤ - (ln (Tmin / T) / a) "
shows "Tmin ≤ exp (-a * τ) * T" and "exp (-a * τ) * T ≤ Tmax"
proof-
have "0 ≤ τ ∧ τ ≤ - (ln (Tmin / T) / a)"
using thyps by auto
hence "ln (Tmin / T) ≤ - a * τ ∧ - a * τ ≤ 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 * τ)" "exp (-a * τ) ≤ 1"
using exp_ln exp_le_one_iff by (metis exp_less_cancel_iff not_less, simp)
thus "Tmin ≤ exp (-a * τ) * T"
using Thyps by (simp add: pos_divide_le_eq)
show "exp (-a * τ) * 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 therm_dyn_up_real_arith:
assumes "a > 0" and Thyps: "Tmin ≤ T" "T ≤ Tmax" "Tmax < (L::real)"
and thyps: "0 ≤ τ" "∀τ∈{0..τ}. τ ≤ - (ln ((L - Tmax) / (L - T)) / a) "
shows "L - Tmax ≤ exp (-(a * τ)) * (L - T)"
and "L - exp (-(a * τ)) * (L - T) ≤ Tmax"
and "Tmin ≤ L - exp (-(a * τ)) * (L - T)"
proof-
have "0 ≤ τ ∧ τ ≤ - (ln ((L - Tmax) / (L - T)) / a)"
using thyps by auto
hence "ln ((L - Tmax) / (L - T)) ≤ - a * τ ∧ - a * τ ≤ 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 * τ) ∧ exp (-a * τ) ≤ 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 * τ) * (L - T) ∧ exp (-a * τ) * (L - T) ≤ (L - T)"
by (simp add: pos_divide_le_eq)
thus "(L - Tmax) ≤ exp (-(a * τ)) * (L - T)"
by auto
thus "L - exp (-(a * τ)) * (L - T) ≤ Tmax"
by auto
show "Tmin ≤ L - exp (-(a * τ)) * (L - T)"
using Thyps and obs by auto
qed
lemmas H_g_ode_therm = local_flow.sH_g_ode_ivl[OF local_flow_therm _ UNIV_I]
lemma thermostat_flow:
assumes "0 < a" and "0 ≤ τ" and "0 < Tmin" and "Tmax < L"
shows "❙{I Tmin Tmax❙}
(LOOP (
(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);
(IF (λs. s$4 = 0) THEN
(x´= (λt. f a 0) & G Tmin Tmax a 0 on (λs. {0..τ}) UNIV @ 0)
ELSE
(x´= (λt. f a L) & G Tmin Tmax a L on (λs. {0..τ}) UNIV @ 0))
) INV I Tmin Tmax)
❙{I Tmin Tmax❙}"
apply(rule H_loopI)
apply(rule_tac R="λs. I Tmin Tmax s ∧ s$2=0 ∧ s$3 = s$1" in H_seq)
apply(rule_tac R="λs. I Tmin Tmax s∧ s$2=0 ∧ s$3 = s$1" in H_seq)
apply(rule_tac R="λs. I Tmin Tmax s ∧ s$2 = 0" in H_seq, simp, simp)
apply(rule H_cond, simp_all add: H_g_ode_therm[OF assms(1,2)])+
using therm_dyn_up_real_arith[OF assms(1) _ _ assms(4), of Tmin]
and therm_dyn_down_real_arith[OF assms(1,3), of _ Tmax] by auto
lemma R_therm_dyn_down:
assumes "a > 0" and "0 ≤ τ" and "0 < Tmin" and "Tmax < L"
shows "Ref ⌈λs. s$4 = 0 ∧ I Tmin Tmax s ∧ s$2 = 0 ∧ s$3 = s$1⌉ ⌈I Tmin Tmax⌉ ≥
(x´= (λt. f a 0) & G Tmin Tmax a 0 on (λs. {0..τ}) UNIV @ 0)"
apply(rule local_flow.R_g_ode_ivl[OF local_flow_therm])
using assms therm_dyn_down_real_arith[OF assms(1,3), of _ Tmax] by auto
lemma R_therm_dyn_up:
assumes "a > 0" and "0 ≤ τ" and "0 < Tmin" and "Tmax < L"
shows "Ref ⌈λs. s$4 ≠ 0 ∧ I Tmin Tmax s ∧ s$2 = 0 ∧ s$3 = s$1⌉ ⌈I Tmin Tmax⌉ ≥
(x´= (λt. f a L) & G Tmin Tmax a L on (λs. {0..τ}) UNIV @ 0)"
apply(rule local_flow.R_g_ode_ivl[OF local_flow_therm])
using assms therm_dyn_up_real_arith[OF assms(1) _ _ assms(4), of Tmin] by auto
lemma R_therm_dyn:
assumes "a > 0" and "0 ≤ τ" and "0 < Tmin" and "Tmax < L"
shows "Ref ⌈λs. I Tmin Tmax s ∧ s$2 = 0 ∧ s$3 = s$1⌉ ⌈I Tmin Tmax⌉ ≥
(IF (λs. s$4 = 0) THEN
(x´= (λt. f a 0) & G Tmin Tmax a 0 on (λs. {0..τ}) UNIV @ 0)
ELSE
(x´= (λt. f a L) & G Tmin Tmax a L on (λs. {0..τ}) UNIV @ 0))"
apply(rule order_trans, rule R_cond_mono)
using R_therm_dyn_down[OF assms] R_therm_dyn_up[OF assms] by (auto intro!: R_cond)
lemma R_therm_assign1: "Ref ⌈I Tmin Tmax⌉ ⌈λs. I Tmin Tmax s ∧ s$2 = 0⌉ ≥ (2 ::= (λs. 0))"
by (auto simp: R_assign_law)
lemma R_therm_assign2:
"Ref ⌈λs. I Tmin Tmax s ∧ s$2 = 0⌉ ⌈λs. I Tmin Tmax s ∧ s$2 = 0 ∧ s$3 = s$1⌉ ≥ (3 ::= (λs. s$1))"
by (auto simp: R_assign_law)
lemma R_therm_ctrl:
"Ref ⌈I Tmin Tmax⌉ ⌈λs. I Tmin Tmax s ∧ s$2 = 0 ∧ s$3 = s$1⌉ ≥
(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)"
apply(refinement, rule R_therm_assign1, rule R_therm_assign2)
by (rule R_assign_law, simp)+ auto
lemma R_therm_loop: "Ref ⌈I Tmin Tmax⌉ ⌈I Tmin Tmax⌉ ≥
(LOOP
Ref ⌈I Tmin Tmax⌉ ⌈λs. I Tmin Tmax s ∧ s$2 = 0 ∧ s$3 = s$1⌉;
Ref ⌈λs. I Tmin Tmax s ∧ s$2 = 0 ∧ s$3 = s$1⌉ ⌈I Tmin Tmax⌉
INV I Tmin Tmax)"
by (intro R_loop R_seq, simp_all)
lemma R_thermostat_flow:
assumes "a > 0" and "0 ≤ τ" and "0 < Tmin" and "Tmax < L"
shows "Ref ⌈I Tmin Tmax⌉ ⌈I Tmin Tmax⌉ ≥
(LOOP (
(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);
(IF (λs. s$4 = 0) THEN
(x´= (λt. f a 0) & G Tmin Tmax a 0 on (λs. {0..τ}) UNIV @ 0)
ELSE
(x´= (λt. f a L) & G Tmin Tmax a L on (λs. {0..τ}) UNIV @ 0))
) INV I Tmin Tmax)"
by (intro order_trans[OF _ R_therm_loop] R_loop_mono
R_seq_mono R_therm_ctrl R_therm_dyn[OF assms])
no_notation therm_vec_field (‹f›)
and therm_flow (‹φ›)
and therm_guard (‹G›)
and therm_loop_inv (‹I›)
subsubsection ‹ Water tank ›
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)
lemmas H_g_ode_tank = local_flow.sH_g_ode_ivl[OF local_flow_tank _ UNIV_I]
lemma tank_flow:
assumes "0 ≤ τ" and "0 < c⇩o" and "c⇩o < c⇩i"
shows "❙{I hmin hmax❙}
(LOOP
((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));
(IF (λs. s$4 = 0) THEN (x´= (λt. f (c⇩i-c⇩o)) & G hmax (c⇩i-c⇩o) on (λs. {0..τ}) UNIV @ 0)
ELSE (x´= (λt. f (-c⇩o)) & G hmin (-c⇩o) on (λs. {0..τ}) UNIV @ 0)) )
INV I hmin hmax)
❙{I hmin hmax❙}"
apply(rule H_loopI)
apply(rule_tac R="λs. I hmin hmax s ∧ s$2=0 ∧ s$3 = s$1" in H_seq)
apply(rule_tac R="λs. I hmin hmax s ∧ s$2=0 ∧ s$3 = s$1" in H_seq)
apply(rule_tac R="λs. I hmin hmax s ∧ s$2=0" in H_seq, simp, simp)
apply(rule H_cond, simp_all add: H_g_ode_tank[OF assms(1)])
using assms tank_arith[OF _ assms(2,3)] by auto
lemma tank_diff_inv:
"0 ≤ τ ⟹ diff_invariant (dI hmin hmax k) (λt. f k) (λs. {0..τ}) UNIV 0 Guard"
apply(intro diff_invariant_conj_rule)
apply(force intro!: poly_derivatives diff_invariant_rules)
apply(rule_tac ν'="λt. 0" and μ'="λt. 1" in diff_invariant_leq_rule, simp_all, presburger)
apply(rule_tac ν'="λt. 0" and μ'="λt. 0" in diff_invariant_leq_rule, simp_all)
apply(force intro!: poly_derivatives)+
by (auto intro!: poly_derivatives diff_invariant_rules)
lemma tank_inv_arith1:
assumes "0 ≤ (τ::real)" and "c⇩o < c⇩i" and b: "hmin ≤ y⇩0" and g: "τ ≤ (hmax - y⇩0) / (c⇩i - c⇩o)"
shows "hmin ≤ (c⇩i - c⇩o) ⋅ τ + y⇩0" and "(c⇩i - c⇩o) ⋅ τ + y⇩0 ≤ hmax"
proof-
have "(c⇩i - c⇩o) ⋅ τ ≤ (hmax - y⇩0)"
using g assms(2,3) by (metis diff_gt_0_iff_gt mult.commute pos_le_divide_eq)
thus "(c⇩i - c⇩o) ⋅ τ + y⇩0 ≤ hmax"
by auto
show "hmin ≤ (c⇩i - c⇩o) ⋅ τ + y⇩0"
using b assms(1,2) by (metis add.commute add_increasing2 diff_ge_0_iff_ge
less_eq_real_def mult_nonneg_nonneg)
qed
lemma tank_inv_arith2:
assumes "0 ≤ (τ::real)" and "0 < c⇩o" and b: "y⇩0 ≤ hmax" and g: "τ ≤ - ((hmin - y⇩0) / c⇩o)"
shows "hmin ≤ y⇩0 - c⇩o ⋅ τ" and "y⇩0 - c⇩o ⋅ τ ≤ hmax"
proof-
have "τ ⋅ c⇩o ≤ y⇩0 - hmin"
using g ‹0 < c⇩o› pos_le_minus_divide_eq by fastforce
thus "hmin ≤ y⇩0 - c⇩o ⋅ τ"
by (auto simp: mult.commute)
show "y⇩0 - c⇩o ⋅ τ ≤ hmax"
using b assms(1,2) by (smt mult_nonneg_nonneg)
qed
lemma tank_inv:
assumes "0 ≤ τ" and "0 < c⇩o" and "c⇩o < c⇩i"
shows "❙{I hmin hmax❙}
(LOOP
((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));
(IF (λs. s$4 = 0) THEN
(x´= (λt. f (c⇩i-c⇩o)) & G hmax (c⇩i-c⇩o) on (λs. {0..τ}) UNIV @ 0 DINV (dI hmin hmax (c⇩i-c⇩o)))
ELSE
(x´= (λt. f (-c⇩o)) & G hmin (-c⇩o) on (λs. {0..τ}) UNIV @ 0 DINV (dI hmin hmax (-c⇩o)))) )
INV I hmin hmax)
❙{I hmin hmax❙}"
apply(rule H_loopI)
apply(rule_tac R="λs. I hmin hmax s ∧ s$2=0 ∧ s$3 = s$1" in H_seq)
apply(rule_tac R="λs. I hmin hmax s ∧ s$2=0 ∧ s$3 = s$1" in H_seq)
apply(rule_tac R="λs. I hmin hmax s ∧ s$2=0" in H_seq, simp, simp)
apply(rule H_cond, simp, simp)+
apply(rule H_cond, rule H_g_ode_inv)
using assms tank_inv_arith1 apply(force simp: tank_diff_inv, simp, clarsimp)
apply(rule H_g_ode_inv)
using assms tank_diff_inv[of _ "-c⇩o" hmin hmax] tank_inv_arith2 by auto
abbreviation tank_ctrl :: "real ⇒ real ⇒ (real^4) nd_fun" (‹ctrl›)
where "ctrl hmin hmax ≡ ((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)))"
abbreviation tank_dyn_dinv :: "real ⇒ real ⇒ real ⇒ real ⇒ real ⇒ (real^4) nd_fun" (‹dyn›)
where "dyn c⇩i c⇩o hmin hmax τ ≡ (IF (λs. s$4 = 0) THEN
(x´= (λt. f (c⇩i-c⇩o)) & G hmax (c⇩i-c⇩o) on (λs. {0..τ}) UNIV @ 0 DINV (dI hmin hmax (c⇩i-c⇩o)))
ELSE
(x´= (λt. f (-c⇩o)) & G hmin (-c⇩o) on (λs. {0..τ}) UNIV @ 0 DINV (dI hmin hmax (-c⇩o))))"
abbreviation "tank_dinv c⇩i c⇩o hmin hmax τ ≡ LOOP (ctrl hmin hmax ; dyn c⇩i c⇩o hmin hmax τ) INV (I hmin hmax)"
lemma R_tank_inv:
assumes "0 ≤ τ" and "0 < c⇩o" and "c⇩o < c⇩i"
shows "Ref ⌈I hmin hmax⌉ ⌈I hmin hmax⌉ ≥
(LOOP
((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));
(IF (λs. s$4 = 0) THEN
(x´= (λt. f (c⇩i-c⇩o)) & G hmax (c⇩i-c⇩o) on (λs. {0..τ}) UNIV @ 0 DINV (dI hmin hmax (c⇩i-c⇩o)))
ELSE
(x´= (λt. f (-c⇩o)) & G hmin (-c⇩o) on (λs. {0..τ}) UNIV @ 0 DINV (dI hmin hmax (-c⇩o)))) )
INV I hmin hmax)"
proof-
have "Ref ⌈I hmin hmax⌉ ⌈I hmin hmax⌉ ≥
LOOP (
(2 ::= (λs. 0)); (Ref ⌈λs. I hmin hmax s ∧ s$2 = 0⌉ ⌈I hmin hmax⌉)
) INV I hmin hmax" (is "_ ≥ ?R")
by (refinement, auto)
moreover have
"?R ≥ LOOP (
(2 ::= (λs. 0));(3 ::=(λs. s$1));
(Ref ⌈λs. I hmin hmax s ∧ s$2 = 0 ∧ s$3=s$1⌉ ⌈I hmin hmax⌉)
) INV I hmin hmax" (is "_ ≥ ?R")
by (simp only: mult.assoc, refinement, auto)
moreover have
"?R ≥ LOOP (
ctrl hmin hmax;
(Ref ⌈λs. I hmin hmax s ∧ s$2 = 0 ∧ s$3=s$1⌉ ⌈I hmin hmax⌉)
) INV I hmin hmax" (is "_ ≥ ?R")
by (simp only: mult.assoc, refinement; (force)?, (rule R_assign_law)?) auto
moreover have
"?R ≥ LOOP (ctrl hmin hmax; dyn c⇩i c⇩o hmin hmax τ) INV I hmin hmax"
apply(simp only: mult.assoc, refinement; ((rule tank_diff_inv[OF assms(1)])? | (simp)?))
using tank_inv_arith1 tank_inv_arith2 assms by auto
ultimately show ?thesis
by auto
qed
no_notation tank_vec_field (‹f›)
and tank_flow (‹φ›)
and tank_guard (‹G›)
and tank_loop_inv (‹I›)
and tank_diff_inv (‹dI›)
end