Theory HS_VC_KAT
section ‹ Verification components with KAT ›
text ‹ We use Kleene algebras with tests to derive rules for verification condition generation and
refinement laws. ›
theory HS_VC_KAT
imports KAT_and_DRA.PHL_KAT
begin
subsection ‹ Hoare logic in KAT ›
text ‹ Here we derive the rules of Hoare Logic. ›
notation t (‹𝔱𝔱›)
hide_const t
no_notation if_then_else (‹if _ then _ else _ fi› [64,64,64] 63)
and HOL.If (‹(‹notation=‹mixfix if expression››if (_)/ then (_)/ else (_))› [0, 0, 10] 10)
and while (‹while _ do _ od› [64,64] 63)
context kat
begin
definition Hoare :: "'a ⇒ 'a ⇒ 'a ⇒ bool" (‹H›) where
"H p x q ⟷ 𝔱𝔱 p ⋅ x ≤ x ⋅ 𝔱𝔱 q"
lemma H_consl: "𝔱𝔱 p ≤ 𝔱𝔱 p' ⟹ H p' x q ⟹ H p x q"
using Hoare_def phl_cons1 by blast
lemma H_consr: "𝔱𝔱 q' ≤ 𝔱𝔱 q ⟹ H p x q' ⟹ H p x q"
using Hoare_def phl_cons2 by blast
lemma H_cons: "𝔱𝔱 p ≤ 𝔱𝔱 p' ⟹ 𝔱𝔱 q' ≤ 𝔱𝔱 q ⟹ H p' x q' ⟹ H p x q"
by (simp add: H_consl H_consr)
lemma H_skip: "H p 1 p"
by (simp add: Hoare_def)
lemma H_abort: "H p 0 q"
by (simp add: Hoare_def)
lemma H_seq: "H p x r ⟹ H r y q ⟹ H p (x ⋅ y) q"
by (simp add: Hoare_def phl_seq)
lemma H_choice: "H p x q ⟹ H p y q ⟹ H p (x + y) q"
using local.distrib_left local.join.sup.mono by (auto simp: Hoare_def)
definition kat_cond :: "'a ⇒ 'a ⇒ 'a ⇒ 'a" (‹if _ then _ else _› [64,64,64] 63) where
"if p then x else y = (𝔱𝔱 p ⋅ x + n p ⋅ y)"
lemma H_var: "H p x q ⟷ 𝔱𝔱 p ⋅ x ⋅ n q = 0"
by (metis Hoare_def n_kat_3 t_n_closed)
lemma H_cond_iff: "H p (if r then x else y) q ⟷ H (𝔱𝔱 p ⋅ 𝔱𝔱 r) x q ∧ H (𝔱𝔱 p ⋅ n r) y q"
proof -
have "H p (if r then x else y) q ⟷ 𝔱𝔱 p ⋅ (𝔱𝔱 r ⋅ x + n r ⋅ y) ⋅ n q = 0"
by (simp add: H_var kat_cond_def)
also have "... ⟷ 𝔱𝔱 p ⋅ 𝔱𝔱 r ⋅ x ⋅ n q + 𝔱𝔱 p ⋅ n r ⋅ y ⋅ n q = 0"
by (simp add: distrib_left mult_assoc)
also have "... ⟷ 𝔱𝔱 p ⋅ 𝔱𝔱 r ⋅ x ⋅ n q = 0 ∧ 𝔱𝔱 p ⋅ n r ⋅ y ⋅ n q = 0"
by (metis add_0_left no_trivial_inverse)
finally show ?thesis
by (metis H_var test_mult)
qed
lemma H_cond: "H (𝔱𝔱 p ⋅ 𝔱𝔱 r) x q ⟹ H (𝔱𝔱 p ⋅ n r) y q ⟹ H p (if r then x else y) q"
by (simp add: H_cond_iff)
definition kat_while :: "'a ⇒ 'a ⇒ 'a" (‹while _ do _› [64,64] 63) where
"while b do x = (𝔱𝔱 b ⋅ x)⇧⋆ ⋅ n b"
definition kat_while_inv :: "'a ⇒ 'a ⇒ 'a ⇒ 'a" (‹while _ inv _ do _› [64,64,64] 63) where
"while p inv i do x = while p do x"
lemma H_exp1: "H (𝔱𝔱 p ⋅ 𝔱𝔱 r) x q ⟹ H p (𝔱𝔱 r ⋅ x) q"
using Hoare_def n_de_morgan_var2 phl.ht_at_phl_export1 by auto
lemma H_while: "H (𝔱𝔱 p ⋅ 𝔱𝔱 r) x p ⟹ H p (while r do x) (𝔱𝔱 p ⋅ n r)"
proof -
assume a1: "H (𝔱𝔱 p ⋅ 𝔱𝔱 r) x p"
have "𝔱𝔱 (𝔱𝔱 p ⋅ n r) = n r ⋅ 𝔱𝔱 p ⋅ n r"
using n_preserve test_mult by presburger
then show ?thesis
using a1 Hoare_def H_exp1 conway.phl.it_simr phl_export2 kat_while_def by auto
qed
lemma H_while_inv: "𝔱𝔱 p ≤ 𝔱𝔱 i ⟹ 𝔱𝔱 i ⋅ n r ≤ 𝔱𝔱 q ⟹ H (𝔱𝔱 i ⋅ 𝔱𝔱 r) x i ⟹ H p (while r inv i do x) q"
by (metis H_cons H_while test_mult kat_while_inv_def)
lemma H_star: "H i x i ⟹ H i (x⇧⋆) i"
unfolding Hoare_def using star_sim2 by blast
lemma H_star_inv:
assumes "𝔱𝔱 p ≤ 𝔱𝔱 i" and "H i x i" and "(𝔱𝔱 i) ≤ (𝔱𝔱 q)"
shows "H p (x⇧⋆) q"
proof-
have "H i (x⇧⋆) i"
using assms(2) H_star by blast
hence "H p (x⇧⋆) i"
unfolding Hoare_def using assms(1) phl_cons1 by blast
thus ?thesis
unfolding Hoare_def using assms(3) phl_cons2 by blast
qed
definition kat_loop_inv :: "'a ⇒ 'a ⇒ 'a" (‹loop _ inv _ › [64,64] 63)
where "loop x inv i = x⇧⋆"
lemma H_loop: "H p x p ⟹ H p (loop x inv i) p"
unfolding kat_loop_inv_def by (rule H_star)
lemma H_loop_inv: "𝔱𝔱 p ≤ 𝔱𝔱 i ⟹ H i x i ⟹ 𝔱𝔱 i ≤ 𝔱𝔱 q ⟹ H p (loop x inv i) q"
unfolding kat_loop_inv_def using H_star_inv by blast
lemma H_inv: "𝔱𝔱 p ≤ 𝔱𝔱 i ⟹ 𝔱𝔱 i ≤ 𝔱𝔱 q ⟹ H i x i ⟹ H p x q"
by (rule_tac p'=i and q'=i in H_cons)
lemma H_inv_plus: "𝔱𝔱 i = i ⟹ 𝔱𝔱 j = j ⟹ H i x i ⟹ H j x j ⟹ H (i + j) x (i + j)"
unfolding Hoare_def using combine_common_factor
by (smt add_commute add.left_commute distrib_left join.sup.absorb_iff1 t_add_closed)
lemma H_inv_mult: "𝔱𝔱 i = i ⟹ 𝔱𝔱 j = j ⟹ H i x i ⟹ H j x j ⟹ H (i ⋅ j) x (i ⋅ j)"
unfolding Hoare_def by (smt n_kat_2 n_mult_comm t_mult_closure mult_assoc)
end
subsection ‹ refinement KAT ›
text ‹ Here we derive the laws of the refinement calculus. ›
class rkat = kat +
fixes Ref :: "'a ⇒ 'a ⇒ 'a"
assumes spec_def: "x ≤ Ref p q ⟷ H p x q"
begin
lemma R1: "H p (Ref p q) q"
using spec_def by blast
lemma R2: "H p x q ⟹ x ≤ Ref p q"
by (simp add: spec_def)
lemma R_cons: "𝔱𝔱 p ≤ 𝔱𝔱 p' ⟹ 𝔱𝔱 q' ≤ 𝔱𝔱 q ⟹ Ref p' q' ≤ Ref p q"
proof -
assume h1: "𝔱𝔱 p ≤ 𝔱𝔱 p'" and h2: "𝔱𝔱 q' ≤ 𝔱𝔱 q"
have "H p' (Ref p' q') q'"
by (simp add: R1)
hence "H p (Ref p' q') q"
using h1 h2 H_consl H_consr by blast
thus ?thesis
by (rule R2)
qed
lemma R_skip: "1 ≤ Ref p p"
proof -
have "H p 1 p"
by (simp add: H_skip)
thus ?thesis
by (rule R2)
qed
lemma R_zero_one: "x ≤ Ref 0 1"
proof -
have "H 0 x 1"
by (simp add: Hoare_def)
thus ?thesis
by (rule R2)
qed
lemma R_one_zero: "Ref 1 0 = 0"
proof -
have "H 1 (Ref 1 0) 0"
by (simp add: R1)
thus ?thesis
by (simp add: Hoare_def join.le_bot)
qed
lemma R_abort: "0 ≤ Ref p q"
using bot_least by force
lemma R_seq: "(Ref p r) ⋅ (Ref r q) ≤ Ref p q"
proof -
have "H p (Ref p r) r" and "H r (Ref r q) q"
by (simp add: R1)+
hence "H p ((Ref p r) ⋅ (Ref r q)) q"
by (rule H_seq)
thus ?thesis
by (rule R2)
qed
lemma R_choice: "(Ref p q) + (Ref p q) ≤ Ref p q"
unfolding spec_def by (rule H_choice) (rule R1)+
lemma R_cond: "if v then (Ref (𝔱𝔱 v ⋅ 𝔱𝔱 p) q) else (Ref (n v ⋅ 𝔱𝔱 p) q) ≤ Ref p q"
proof -
have "H (𝔱𝔱 v ⋅ 𝔱𝔱 p) (Ref (𝔱𝔱 v ⋅ 𝔱𝔱 p) q) q" and "H (n v ⋅ 𝔱𝔱 p) (Ref (n v ⋅ 𝔱𝔱 p) q) q"
by (simp add: R1)+
hence "H p (if v then (Ref (𝔱𝔱 v ⋅ 𝔱𝔱 p) q) else (Ref (n v ⋅ 𝔱𝔱 p) q)) q"
by (simp add: H_cond n_mult_comm)
thus ?thesis
by (rule R2)
qed
lemma R_while: "while q do (Ref (𝔱𝔱 p ⋅ 𝔱𝔱 q) p) ≤ Ref p (𝔱𝔱 p ⋅ n q)"
proof -
have "H (𝔱𝔱 p ⋅ 𝔱𝔱 q) (Ref (𝔱𝔱 p ⋅ 𝔱𝔱 q) p) p"
by (simp_all add: R1)
hence "H p (while q do (Ref (𝔱𝔱 p ⋅ 𝔱𝔱 q) p)) (𝔱𝔱 p ⋅ n q)"
by (simp add: H_while)
thus ?thesis
by (rule R2)
qed
lemma R_star: "(Ref i i)⇧⋆ ≤ Ref i i"
proof -
have "H i (Ref i i) i"
using R1 by blast
hence "H i ((Ref i i)⇧⋆) i"
using H_star by blast
thus "Ref i i⇧⋆ ≤ Ref i i"
by (rule R2)
qed
lemma R_loop: "loop (Ref p p) inv i ≤ Ref p p"
unfolding kat_loop_inv_def by (rule R_star)
lemma R_inv: "𝔱𝔱 p ≤ 𝔱𝔱 i ⟹ 𝔱𝔱 i ≤ 𝔱𝔱 q ⟹ Ref i i ≤ Ref p q"
using R_cons by force
end
end