Theory VC_KAD
section ‹Components Based on Kleene Algebra with Domain›
theory VC_KAD
imports KAD.Modal_Kleene_Algebra_Models "../P2S2R"
begin
subsection‹Verification Component for Backward Reasoning›
text ‹This component supports the verification of simple while programs
in a partial correctness setting.›
no_notation Archimedean_Field.ceiling ("⌈_⌉")
no_notation Archimedean_Field.floor ("⌊_⌋")
notation p2r ("⌈_⌉")
notation r2p ("⌊_⌋")
context antidomain_kleene_algebra
begin
subsubsection ‹Additional Facts for KAD›
lemma fbox_shunt: "d p ⋅ d q ≤ |x] t ⟷ d p ≤ ad q + |x] t"
by (metis a_6 a_antitone' a_loc add_commute addual.ars_r_def am_d_def da_shunt2 fbox_def)
subsubsection ‹Syntax for Conditionals and Loops›
definition cond :: "'a ⇒ 'a ⇒ 'a ⇒ 'a" ("if _ then _ else _ fi" [64,64,64] 63) where
"if p then x else y fi = d p ⋅ x + ad p ⋅ y"
definition while :: "'a ⇒ 'a ⇒ 'a" ("while _ do _ od" [64,64] 63) where
"while p do x od = (d p ⋅ x)⇧⋆ ⋅ ad p"
definition whilei :: "'a ⇒ 'a ⇒ 'a ⇒ 'a" ("while _ inv _ do _ od" [64,64,64] 63) where
"while p inv i do x od = while p do x od"
subsubsection ‹Basic Weakest (Liberal) Precondition Calculus›
text ‹In the setting of Kleene algebra with domain, the wlp operator is the forward modal box operator
of antidomain Kleene algebra.›
lemma fbox_export1: "ad p + |x] q = |d p ⋅ x] q"
using a_d_add_closure addual.ars_r_def fbox_def fbox_mult by auto
lemma fbox_export2: "|x] p ≤ |x ⋅ ad q] (d p ⋅ ad q)"
proof -
{fix t
have "d t ⋅ x ≤ x ⋅ d p ⟹ d t ⋅ x ⋅ ad q ≤ x ⋅ ad q ⋅ d p ⋅ ad q"
by (metis (full_types) a_comm_var a_mult_idem ads_d_def am2 ds.ddual.mult_assoc phl_export2)
hence "d t ≤ |x] p ⟹ d t ≤ |x ⋅ ad q] (d p ⋅ ad q)"
by (metis a_closure' addual.ars_r_def ans_d_def dka.dsg3 ds.ddual.mult_assoc fbox_def fbox_demodalisation3)
}
thus ?thesis
by (metis a_closure' addual.ars_r_def ans_d_def fbox_def order_refl)
qed
lemma fbox_export3: "|x ⋅ ad p] q = |x] (d p + d q)"
using a_de_morgan_var_3 ds.ddual.mult_assoc fbox_def by auto
lemma fbox_seq [simp]: "|x ⋅ y] q = |x] |y] q"
by (simp add: fbox_mult)
lemma fbox_seq_var: "p' ≤ |y] q ⟹ p ≤ |x] p' ⟹ p ≤ |x ⋅ y] q"
proof -
assume h1: "p ≤ |x] p'" and h2: "p' ≤ |y] q"
hence "|x] p' ≤ |x] |y] q"
by (simp add: dka.dom_iso fbox_iso)
thus ?thesis
by (metis h1 dual_order.trans fbox_seq)
qed
lemma fbox_cond_var [simp]: "|if p then x else y fi] q = (ad p + |x] q) ⋅ (d p + |y] q)"
using cond_def a_closure' ads_d_def ans_d_def fbox_add2 fbox_export1 by auto
lemma fbox_cond_aux1 [simp]: "d p ⋅ |if p then x else y fi] q = d p ⋅ |x] q"
proof -
have "d p ⋅ |if p then x else y fi] q = d p ⋅ |x] q ⋅ (d p + d ( |y] q))"
using a_d_add_closure addual.ars_r_def ds.ddual.mult_assoc fbox_def fbox_cond_var by auto
thus ?thesis
by (metis addual.ars_r_def am2 dka.dns5 ds.ddual.mult_assoc fbox_def)
qed
lemma fbox_cond_aux2 [simp]: "ad p ⋅ |if p then x else y fi] q = ad p ⋅ |y] q"
by (metis cond_def a_closure' add_commute addual.ars_r_def ans_d_def fbox_cond_aux1)
lemma fbox_cond [simp]: "|if p then x else y fi] q = (d p ⋅ |x] q) + (ad p ⋅ |y] q)"
proof -
have "|if p then x else y fi] q = (d p + ad p) ⋅ |if p then x else y fi] q"
by (simp add: addual.ars_r_def)
thus ?thesis
by (metis distrib_right' fbox_cond_aux1 fbox_cond_aux2)
qed
lemma fbox_cond_var2 [simp]: "|if p then x else y fi] q = if p then |x] q else |y] q fi"
using cond_def fbox_cond by auto
lemma fbox_while_unfold: "|while t do x od] p = (d t + d p) ⋅ (ad t + |x] |while t do x od] p)"
by (metis fbox_export1 fbox_export3 dka.dom_add_closed fbox_star_unfold_var while_def)
lemma fbox_while_var1: "d t ⋅ |while t do x od] p = d t ⋅ |x] |while t do x od] p"
by (metis fbox_while_unfold a_mult_add ads_d_def dka.dns5 ds.ddual.mult_assoc join.sup_commute)
lemma fbox_while_var2: "ad t ⋅ |while t do x od] p ≤ d p"
proof -
have "ad t ⋅ |while t do x od] p = ad t ⋅ (d t + d p) ⋅ (ad t + |x] |while t do x od] p)"
by (metis fbox_while_unfold ds.ddual.mult_assoc)
also have "... = ad t ⋅ d p ⋅ (ad t + |x] |while t do x od] p)"
by (metis a_de_morgan_var_3 addual.ars_r_def dka.dom_add_closed s4)
also have "... ≤ d p ⋅ (ad t + |x] |while t do x od] p)"
using a_subid_aux1' mult_isor by blast
finally show ?thesis
by (metis a_de_morgan_var_3 a_mult_idem addual.ars_r_def ans4 dka.dsr5 dpdz.domain_1'' dual_order.trans fbox_def)
qed
lemma fbox_while: "d p ⋅ d t ≤ |x] p ⟹ d p ≤ |while t do x od] (d p ⋅ ad t)"
proof -
assume "d p ⋅ d t ≤ |x] p"
hence "d p ≤ |d t ⋅ x] p"
by (simp add: fbox_export1 fbox_shunt)
hence "d p ≤ |(d t ⋅ x)⇧⋆] p"
by (simp add: fbox_star_induct_var)
thus ?thesis
using order_trans while_def fbox_export2 by presburger
qed
lemma fbox_while_var: "d p = |d t ⋅ x] p ⟹ d p ≤ |while t do x od] (d p ⋅ ad t)"
by (metis eq_refl fbox_export1 fbox_shunt fbox_while)
lemma fbox_whilei: "d p ≤ d i ⟹ d i ⋅ ad t ≤ d q ⟹ d i ⋅ d t ≤ |x] i ⟹ d p ≤ |while t inv i do x od] q"
proof -
assume a1: "d p ≤ d i" and a2: "d i ⋅ ad t ≤ d q" and "d i ⋅ d t ≤ |x] i"
hence "d i ≤ |while t inv i do x od] (d i ⋅ ad t)"
by (simp add: fbox_while whilei_def)
also have "... ≤ |while t inv i do x od] q"
using a2 dka.dom_iso fbox_iso by fastforce
finally show ?thesis
using a1 dual_order.trans by blast
qed
text ‹The next rule is used for dealing with while loops after a series of sequential steps.›
lemma fbox_whilei_break: "d p ≤ |y] i ⟹ d i ⋅ ad t ≤ d q ⟹ d i ⋅ d t ≤ |x] i ⟹ d p ≤ |y ⋅ (while t inv i do x od)] q"
apply (rule fbox_seq_var, rule fbox_whilei, simp_all, blast)
using fbox_simp by auto
text ‹Finally we derive a frame rule.›
lemma fbox_frame: "d p ⋅ x ≤ x ⋅ d p ⟹ d q ≤ |x] t ⟹ d p ⋅ d q ≤ |x] (d p ⋅ d t)"
using dual.mult_isol_var fbox_add1 fbox_demodalisation3 fbox_simp by auto
lemma fbox_frame_var: "d p ≤ |x] p ⟹ d q ≤ |x] t ⟹ d p ⋅ d q ≤ |x] (d p ⋅ d t)"
using fbox_frame fbox_demodalisation3 fbox_simp by auto
end
subsubsection ‹Store and Assignment›
type_synonym 'a store = "string ⇒ 'a"
notation rel_antidomain_kleene_algebra.fbox ("wp")
and rel_antidomain_kleene_algebra.fdia ("relfdia")
definition gets :: "string ⇒ ('a store ⇒ 'a) ⇒ 'a store rel" ("_ ::= _" [70, 65] 61) where
"v ::= e = {(s,s (v := e s)) |s. True}"
lemma assign_prop: "⌈λs. P (s (v := e s))⌉ ; (v ::= e) = (v ::= e) ; ⌈P⌉"
by (auto simp add: p2r_def gets_def)
lemma wp_assign [simp]: "wp (v ::= e) ⌈Q⌉ = ⌈λs. Q (s (v := e s))⌉"
by (auto simp: rel_antidomain_kleene_algebra.fbox_def gets_def rel_ad_def p2r_def)
lemma wp_assign_var [simp]: "⌊wp (v ::= e) ⌈Q⌉⌋ = (λs. Q (s (v := e s)))"
by (simp, auto simp: r2p_def p2r_def)
lemma wp_assign_det: "wp (v ::= e) ⌈Q⌉ = relfdia (v ::= e) ⌈Q⌉"
by (auto simp add: rel_antidomain_kleene_algebra.fbox_def rel_antidomain_kleene_algebra.fdia_def gets_def p2r_def rel_ad_def, fast)
subsubsection ‹Simplifications›
notation rel_antidomain_kleene_algebra.ads_d ("rdom")
abbreviation spec_sugar :: "'a pred ⇒ 'a rel ⇒ 'a pred ⇒ bool" ("PRE _ _ POST _" [64,64,64] 63) where
"PRE P X POST Q ≡ rdom ⌈P⌉ ⊆ wp X ⌈Q⌉"
abbreviation cond_sugar :: "'a pred ⇒ 'a rel ⇒ 'a rel ⇒ 'a rel" ("IF _ THEN _ ELSE _ FI" [64,64,64] 63) where
"IF P THEN X ELSE Y FI ≡ rel_antidomain_kleene_algebra.cond ⌈P⌉ X Y"
abbreviation whilei_sugar :: "'a pred ⇒ 'a pred ⇒ 'a rel ⇒ 'a rel" ("WHILE _ INV _ DO _ OD" [64,64,64] 63) where
"WHILE P INV I DO X OD ≡ rel_antidomain_kleene_algebra.whilei ⌈P⌉ ⌈I⌉ X"
lemma d_p2r [simp]: "rdom ⌈P⌉ = ⌈P⌉"
by (simp add: p2r_def rel_antidomain_kleene_algebra.ads_d_def rel_ad_def)
lemma p2r_conj_hom_var_symm [simp]: "⌈P⌉ ; ⌈Q⌉ = ⌈P ⊓ Q⌉"
by (simp add: p2r_conj_hom_var)
lemma p2r_neg_hom [simp]: "rel_ad ⌈P⌉ = ⌈- P⌉"
by (simp add: rel_ad_def p2r_def)
lemma wp_trafo: "⌊wp X ⌈Q⌉⌋ = (λs. ∀s'. (s,s') ∈ X ⟶ Q s')"
by (auto simp: rel_antidomain_kleene_algebra.fbox_def rel_ad_def p2r_def r2p_def)
lemma wp_trafo_var: "⌊wp X ⌈Q⌉⌋ s = (∀s'. (s,s') ∈ X ⟶ Q s')"
by (simp add: wp_trafo)
lemma wp_simp: "rdom ⌈⌊wp X Q⌋⌉ = wp X Q"
by (metis d_p2r rel_antidomain_kleene_algebra.a_subid' rel_antidomain_kleene_algebra.addual.bbox_def rpr)
lemma wp_simp_var [simp]: "wp ⌈P⌉ ⌈Q⌉ = ⌈- P ⊔ Q⌉"
by (simp add: rel_antidomain_kleene_algebra.fbox_def)
lemma impl_prop [simp]: "⌈P⌉ ⊆ ⌈Q⌉ ⟷ (∀s. P s ⟶ Q s)"
by (auto simp: p2r_def)
lemma p2r_eq_prop [simp]: "⌈P⌉ = ⌈Q⌉ ⟷ (∀s. P s ⟷ Q s)"
by (auto simp: p2r_def)
lemma impl_prop_var [simp]: "rdom ⌈P⌉ ⊆ rdom ⌈Q⌉ ⟷ (∀s. P s ⟶ Q s)"
by simp
lemma p2r_eq_prop_var [simp]: "rdom ⌈P⌉ = rdom ⌈Q⌉ ⟷ (∀s. P s ⟷ Q s)"
by simp
lemma wp_whilei: "(∀s. P s ⟶ I s) ⟹ (∀s. (I ⊓ -T) s ⟶ Q s) ⟹ (∀s. (I ⊓ T) s ⟶ ⌊wp X ⌈I⌉⌋ s)
⟹ (∀s. P s ⟶ ⌊wp (WHILE T INV I DO X OD) ⌈Q⌉⌋ s)"
apply (simp only: impl_prop_var[symmetric] wp_simp)
by (rule rel_antidomain_kleene_algebra.fbox_whilei, simp_all, simp_all add: p2r_def)
end