Theory HS_VC_MKA
section ‹ Verification components with MKA ›
text ‹ We use the forward box operator of antidomain Kleene algebras to derive rules for weakest
liberal preconditions (wlps) of regular programs. ›
theory HS_VC_MKA
imports "KAD.Modal_Kleene_Algebra"
begin
subsection ‹ Verification in AKA ›
text ‹Here we derive verification components with weakest liberal preconditions based on
antidomain Kleene algebra ›
no_notation Range_Semiring.antirange_semiring_class.ars_r (‹r›)
and HOL.If (‹(‹notation=‹mixfix if expression››if (_)/ then (_)/ else (_))› [0, 0, 10] 10)
notation zero_class.zero (‹0›)
context antidomain_kleene_algebra
begin
lemma "|1] x = d x"
using fbox_one .
lemma "|0] q = 1"
using fbox_zero .
lemma "|x ⋅ y] q = |x] |y] q"
using fbox_mult .
declare fbox_mult [simp]
lemma "|x + y] q = |x] q ⋅ |y] q"
using fbox_add2 .
lemma le_fbox_choice_iff: "d p ≤ |x + y]q ⟷ (d p ≤ |x]q) ∧ (d p ≤ |y]q)"
by (metis local.a_closure' local.ads_d_def local.dnsz.dom_glb_eq local.fbox_add2 local.fbox_def)
definition aka_cond :: "'a ⇒ 'a ⇒ 'a ⇒ 'a" (‹if _ then _ else _› [64,64,64] 63)
where "if p then x else y = d p ⋅ x + ad p ⋅ y"
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_cond [simp]: "|if p then x else y] q = (ad p + |x] q) ⋅ (d p + |y] q)"
using fbox_export1 local.ans_d_def local.fbox_mult
unfolding aka_cond_def ads_d_def fbox_def by auto
lemma fbox_cond2: "|if p then x else y] q = (d p ⋅ |x] q) + (ad p ⋅ |y] q)" (is "?lhs = ?d1 + ?d2")
proof -
have obs: "?lhs = d p ⋅ ?lhs + ad p ⋅ ?lhs"
by (metis (no_types, lifting) local.a_closure' local.a_de_morgan fbox_def ans_d_def
ads_d_def local.am2 local.am5_lem local.dka.dsg3 local.dka.dsr5)
have "d p ⋅ ?lhs = d p ⋅ |x] q ⋅ (d p + d ( |y] q))"
using fbox_cond local.a_d_add_closure local.ads_d_def
local.ds.ddual.mult_assoc local.fbox_def by auto
also have "... = d p ⋅ |x] q"
by (metis local.ads_d_def local.am2 local.dka.dns5 local.ds.ddual.mult_assoc local.fbox_def)
finally have "d p ⋅ ?lhs = d p ⋅ |x] q" .
moreover have "ad p ⋅ ?lhs = ad p ⋅ |y] q"
by (metis add_commute fbox_cond local.a_closure' local.a_mult_add ads_d_def ans_d_def
local.dnsz.dns5 local.ds.ddual.mult_assoc local.fbox_def)
ultimately show ?thesis
using obs by simp
qed
definition aka_whilei :: "'a ⇒ 'a ⇒ 'a ⇒ 'a" (‹while _ do _ inv _› [64,64,64] 63) where
"while t do x inv i = (d t ⋅ x)⇧⋆ ⋅ ad t"
lemma fbox_frame: "d p ⋅ x ≤ x ⋅ d p ⟹ d q ≤ |x] r ⟹ d p ⋅ d q ≤ |x] (d p ⋅ d r)"
using dual.mult_isol_var fbox_add1 fbox_demodalisation3 fbox_simp by auto
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)
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_while: "d p ⋅ d t ≤ |x] p ⟹ d p ≤ |(d t ⋅ x)⇧⋆ ⋅ ad t] (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 fbox_export2 by presburger
qed
lemma fbox_whilei:
assumes "d p ≤ d i" and "d i ⋅ ad t ≤ d q" and "d i ⋅ d t ≤ |x] i"
shows "d p ≤ |while t do x inv i] q"
proof-
have "d i ≤ |(d t ⋅ x)⇧⋆ ⋅ ad t] (d i ⋅ ad t)"
using fbox_while assms by blast
also have "... ≤ |(d t ⋅ x)⇧⋆ ⋅ ad t] q"
by (metis assms(2) local.dka.dom_iso local.dka.domain_invol local.fbox_iso)
finally show ?thesis
unfolding aka_whilei_def
using assms(1) local.dual_order.trans by blast
qed
lemma fbox_seq_var: "p ≤ |x] p' ⟹ p' ≤ |y] q ⟹ p ≤ |x ⋅ y] q"
proof -
assume h1: "p ≤ |x] p'" and h2: "p' ≤ |y] q"
hence "|x] p' ≤ |x] |y] q"
by (metis ads_d_def fbox_antitone_var fbox_dom fbox_iso)
thus ?thesis
by (metis dual_order.trans fbox_mult h1)
qed
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 do x inv i)] q"
apply (rule fbox_seq_var[OF _ fbox_whilei])
using fbox_simp by auto
definition aka_loopi :: "'a ⇒ 'a ⇒ 'a" (‹loop _ inv _ › [64,64] 63)
where "loop x inv i = x⇧⋆"
lemma "d p ≤ |x] p ⟹ d p ≤ |x⇧⋆] p"
using fbox_star_induct_var .
lemma fbox_loopi: "p ≤ d i ⟹ d i ≤ |x] i ⟹ d i ≤ d q ⟹ p ≤ |loop x inv i] q"
unfolding aka_loopi_def by (meson dual_order.trans fbox_iso fbox_star_induct_var)
lemma fbox_loopi_break:
"p ≤ |y] d i ⟹ d i ≤ |x] i ⟹ d i ≤ d q ⟹ p ≤ |y ⋅ (loop x inv i)] q"
by (rule fbox_seq_var, force) (rule fbox_loopi, auto)
lemma "p ≤ i ⟹ i ≤ |x]i ⟹ i ≤ q ⟹ p ≤ |x]q"
by (metis local.ads_d_def local.dpdz.dom_iso local.dual_order.trans local.fbox_iso)
lemma "p ≤ d i ⟹ d i ≤ |x]i ⟹ i ≤ d q ⟹ p ≤ |x]q"
by (metis local.a_4 local.a_antitone' local.a_subid_aux2 ads_d_def order.antisym fbox_def
local.dka.dsg1 local.dual.mult_isol_var local.dual_order.trans local.order.refl)
lemma "(i ≤ |x] i) ∨ (j ≤ |x] j) ⟹ (i + j) ≤ |x] (i + j)"
oops
lemma "d i ≤ |x] i ⟹ d j ≤ |x] j ⟹ (d i + d j) ≤ |x] (d i + d j)"
by (metis (no_types, lifting) dual_order.trans fbox_simp fbox_subdist join.le_supE join.le_supI)
lemma plus_inv: "i ≤ |x] i ⟹ j ≤ |x] j ⟹ (i + j) ≤ |x] (i + j)"
by (metis ads_d_def dka.dsr5 fbox_simp fbox_subdist join.sup_mono order_trans)
lemma mult_inv: "d i ≤ |x] i ⟹ d j ≤ |x] j ⟹ (d i ⋅ d j) ≤ |x] (d i ⋅ d j)"
using fbox_demodalisation3 fbox_frame fbox_simp by auto
end
end