Theory VC_KAD_dual
subsection‹Verification Component for Forward Reasoning›
theory VC_KAD_dual
imports VC_KAD
begin
context modal_kleene_algebra
begin
text ‹This component supports the verification of simple while programs
in a partial correctness setting.›
subsubsection ‹Basic Strongest Postcondition Calculus›
text ‹In modal Kleene algebra, strongest postconditions are backward diamond operators. These
are linked with forward boxes aka weakest preconditions by a Galois connection. This duality has been
implemented in the AFP entry for Kleene algebra with domain and is picked up automatically in
the following proofs.›
lemma r_ad [simp]: "r (ad p) = ad p"
using a_closure addual.ars_r_def am_d_def domrangefix by auto
lemma bdia_export1: "⟨x| (r p ⋅ r t) = ⟨r t ⋅ x| p"
by (metis ardual.ads_d_def ardual.ds.ddual.rsr2 ardual.ds.fdia_mult bdia_def)
lemma bdia_export2: "r p ⋅ ⟨x| q = ⟨x ⋅ r p| q"
using ardual.ads_d_def ardual.am2 ardual.fdia_export_2 bdia_def by auto
lemma bdia_seq [simp]: "⟨x ⋅ y| q = ⟨y| ⟨x| q"
by (simp add: ardual.ds.fdia_mult)
lemma bdia_seq_var: "⟨x| p ≤ p' ⟹ ⟨y| p' ≤ q ⟹ ⟨x ⋅ y| p ≤ q"
by (metis ardual.ds.fd_subdist_1 ardual.ds.fdia_mult dual_order.trans join.sup_absorb2)
lemma bdia_cond_var [simp]: "⟨if p then x else y fi| q = ⟨x| (d p ⋅ r q) + ⟨y| (ad p ⋅ r q)"
by (metis (no_types, lifting) bdia_export1 a4' a_de_morgan a_de_morgan_var_3 a_subid_aux1' ardual.ds.fdia_add2 dka.dnso1 dka.dsg4 domrange dpdz.dnso1 cond_def join.sup.absorb_iff1 rangedom)
lemma bdia_while: "⟨x| (d t ⋅ r p) ≤ r p ⟹ ⟨while t do x od| p ≤ r p ⋅ ad t"
proof -
assume "⟨x| (d t ⋅ r p) ≤ r p"
hence "⟨d t ⋅ x| p ≤ r p"
by (metis bdia_export1 dka.dsg4 domrange rangedom)
hence "⟨(d t ⋅ x)⇧⋆| p ≤ r p"
by (meson ardual.fdemodalisation22 ardual.kat_2_equiv_opp star_sim1)
hence "r (ad t) ⋅ ⟨(d t ⋅ x)⇧⋆| p ≤ r p ⋅ ad t"
by (metis ardual.dpdz.dsg4 ars_r_def mult_isol r_ad)
thus ?thesis
by (metis bdia_export2 while_def r_ad)
qed
lemma bdia_whilei: "r p ≤ r i ⟹ r i ⋅ ad t ≤ r q ⟹ ⟨x| (d t ⋅ r i) ≤ r i ⟹ ⟨while t inv i do x od| p ≤ r q"
proof -
assume a1: "r p ≤ r i" and a2: "r i ⋅ ad t ≤ r q" and "⟨x| (d t ⋅ r i) ≤ r i"
hence "⟨while t inv i do x od| i ≤ r i ⋅ ad t"
by (simp add: bdia_while whilei_def)
hence "⟨while t inv i do x od| i ≤ r q"
using a2 dual_order.trans by blast
hence "r i ≤ |while t inv i do x od] r q"
using ars_r_def box_diamond_galois_1 domrange by fastforce
hence "r p ≤ |while t inv i do x od] r q"
using a1 dual_order.trans by blast
thus ?thesis
using ars_r_def box_diamond_galois_1 domrange by fastforce
qed
lemma bdia_whilei_break: "⟨y| p ≤ r i ⟹ r i ⋅ ad t ≤ r q ⟹ ⟨x| (d t ⋅ r i) ≤ r i ⟹ ⟨y ⋅ (while t inv i do x od)| p ≤ r q"
using bdia_whilei ardual.ads_d_def ardual.ds.fdia_mult bdia_def by auto
end
subsubsection ‹Floyd's Assignment Rule›
lemma bdia_assign [simp]: "rel_antirange_kleene_algebra.bdia (v ::= e) ⌈P⌉ = ⌈λs. ∃w. s v = e (s(v := w)) ∧ P (s(v:=w))⌉"
apply (simp add: rel_antirange_kleene_algebra.bdia_def gets_def p2r_def rel_ar_def)
apply safe
by (metis fun_upd_apply fun_upd_triv fun_upd_upd, fastforce)
lemma d_p2r [simp]: "rel_antirange_kleene_algebra.ars_r ⌈P⌉ = ⌈P⌉"
by (simp add: p2r_def rel_antirange_kleene_algebra.ars_r_def rel_ar_def)
abbreviation fspec_sugar :: "'a pred ⇒ 'a rel ⇒ 'a pred ⇒ bool" ("FPRE _ _ POST _" [64,64,64] 63) where
"FPRE P X POST Q ≡ rel_antirange_kleene_algebra.bdia X ⌈P⌉ ⊆ rel_antirange_kleene_algebra.ars_r ⌈Q⌉"
end