Theory VC_KAD_scratch
subsection‹Component Based on Kleene Algebra with Domain›
text ‹This component supports the verification and step-wise refinement of simple while programs
in a partial correctness setting.›
theory VC_KAD_scratch
imports Main
begin
subsubsection ‹KAD: Definitions and Basic Properties›
notation times (infixl ‹⋅› 70)
class plus_ord = plus + ord +
assumes less_eq_def: "x ≤ y ⟷ x + y = y"
and less_def: "x < y ⟷ x ≤ y ∧ x ≠ y"
class dioid = semiring + one + zero + plus_ord +
assumes add_idem [simp]: "x + x = x"
and mult_onel [simp]: "1 ⋅ x = x"
and mult_oner [simp]: "x ⋅ 1 = x"
and add_zerol [simp]: "0 + x = x"
and annil [simp]: "0 ⋅ x = 0"
and annir [simp]: "x ⋅ 0 = 0"
begin
subclass monoid_mult
by (standard, simp_all)
subclass order
by (standard, simp_all add: less_def less_eq_def add_commute, auto, metis add_assoc)
lemma mult_isor: "x ≤ y ⟹ x ⋅ z ≤ y ⋅ z"
by (metis distrib_right less_eq_def)
lemma mult_isol: "x ≤ y ⟹ z ⋅ x ≤ z ⋅ y"
by (metis distrib_left less_eq_def)
lemma add_iso: "x ≤ y ⟹ z + x ≤ z + y"
by (metis add.semigroup_axioms add_idem less_eq_def semigroup.assoc)
lemma add_ub: "x ≤ x + y"
by (metis add_assoc add_idem less_eq_def)
lemma add_lub: "x + y ≤ z ⟷ x ≤ z ∧ y ≤ z"
by (metis add_assoc add_ub add.left_commute less_eq_def)
end
class kleene_algebra = dioid +
fixes star :: "'a ⇒ 'a" (‹_⇧⋆› [101] 100)
assumes star_unfoldl: "1 + x ⋅ x⇧⋆ ≤ x⇧⋆"
and star_unfoldr: "1 + x⇧⋆ ⋅ x ≤ x⇧⋆"
and star_inductl: "z + x ⋅ y ≤ y ⟹ x⇧⋆ ⋅ z ≤ y"
and star_inductr: "z + y ⋅ x ≤ y ⟹ z ⋅ x⇧⋆ ≤ y"
begin
lemma star_sim: "x ⋅ y ≤ z ⋅ x ⟹ x ⋅ y⇧⋆ ≤ z⇧⋆ ⋅ x"
proof -
assume "x ⋅ y ≤ z ⋅ x"
hence "x + z⇧⋆ ⋅ x ⋅ y ≤ x + z⇧⋆ ⋅ z ⋅ x"
by (metis add_lub distrib_left eq_refl less_eq_def mult_assoc)
also have "... ≤ z⇧⋆ ⋅ x"
using add_lub mult_isor star_unfoldr by fastforce
finally show ?thesis
by (simp add: star_inductr)
qed
end
class antidomain_kleene_algebra = kleene_algebra +
fixes ad :: "'a ⇒ 'a" (‹ad›)
assumes as1 [simp]: "ad x ⋅ x = 0"
and as2 [simp]: "ad (x ⋅ y) + ad (x ⋅ ad (ad y)) = ad (x ⋅ ad (ad y))"
and as3 [simp]: "ad (ad x) + ad x = 1"
begin
definition dom_op :: "'a ⇒ 'a" (‹d›) where
"d x = ad (ad x)"
lemma a_subid_aux: "ad x ⋅ y ≤ y"
by (metis add_commute add_ub as3 mult_1_left mult_isor)
lemma d1_a [simp]: "d x ⋅ x = x"
by (metis add_commute dom_op_def add_zerol as1 as3 distrib_right mult_1_left)
lemma a_mul_d [simp]: "ad x ⋅ d x = 0"
by (metis add_commute dom_op_def add_zerol as1 as2 distrib_right mult_1_left)
lemma a_d_closed [simp]: "d (ad x) = ad x"
by (metis d1_a dom_op_def add_zerol as1 as3 distrib_left mult_1_right)
lemma a_idem [simp]: "ad x ⋅ ad x = ad x"
by (metis a_d_closed d1_a)
lemma meet_ord: "ad x ≤ ad y ⟷ ad x ⋅ ad y = ad x"
by (metis a_d_closed a_subid_aux d1_a order.antisym mult_1_right mult_isol)
lemma d_wloc: "x ⋅ y = 0 ⟷ x ⋅ d y = 0"
by (metis a_subid_aux d1_a dom_op_def add_ub order.antisym as1 as2 mult_1_right mult_assoc)
lemma gla_1: "ad x ⋅ y = 0 ⟹ ad x ≤ ad y"
by (metis a_subid_aux d_wloc dom_op_def add_zerol as3 distrib_left mult_1_right)
lemma a2_eq [simp]: "ad (x ⋅ d y) = ad (x ⋅ y)"
by (metis a_mul_d d1_a dom_op_def gla_1 add_ub order.antisym as1 as2 mult_assoc)
lemma a_supdist: "ad (x + y) ≤ ad x"
by (metis add_commute gla_1 add_ub add_zerol as1 distrib_left less_eq_def)
lemma a_antitone: "x ≤ y ⟹ ad y ≤ ad x"
by (metis a_supdist less_eq_def)
lemma a_comm: "ad x ⋅ ad y = ad y ⋅ ad x"
proof -
{ fix x y
have "ad x ⋅ ad y = d (ad x ⋅ ad y) ⋅ ad x ⋅ ad y"
by (simp add: mult_assoc)
also have "... ≤ d (ad y) ⋅ ad x"
by (metis a_antitone a_d_closed a_subid_aux mult_oner a_subid_aux dom_op_def mult_isol mult_isor meet_ord)
finally have "ad x ⋅ ad y ≤ ad y ⋅ ad x"
by simp }
thus ?thesis
by (simp add: order.antisym)
qed
lemma a_closed [simp]: "d (ad x ⋅ ad y) = ad x ⋅ ad y"
proof -
have f1: "⋀x y. ad x ≤ ad (ad y ⋅ x)"
by (simp add: a_antitone a_subid_aux)
have "⋀x y. d (ad x ⋅ y) ≤ ad x"
by (metis a2_eq a_antitone a_comm a_d_closed dom_op_def f1)
hence "⋀x y. d (ad x ⋅ y) ⋅ y = ad x ⋅ y"
by (metis d1_a dom_op_def meet_ord mult_assoc)
thus ?thesis
by (metis a_comm a_idem dom_op_def)
qed
lemma a_exp [simp]: "ad (ad x ⋅ y) = d x + ad y"
proof (rule order.antisym)
have "ad (ad x ⋅ y) ⋅ ad x ⋅ d y = 0"
using d_wloc mult_assoc by fastforce
hence a: "ad (ad x ⋅ y) ⋅ d y ≤ d x"
by (metis a_closed a_comm dom_op_def gla_1 mult_assoc)
have "ad (ad x ⋅ y) = ad (ad x ⋅ y) ⋅ d y + ad (ad x ⋅ y) ⋅ ad y"
by (metis dom_op_def as3 distrib_left mult_oner)
also have "... ≤ d x + ad (ad x ⋅ y) ⋅ ad y"
using a add_lub dual_order.trans by blast
finally show "ad (ad x ⋅ y) ≤ d x + ad y"
by (metis a_antitone a_comm a_subid_aux meet_ord)
next
have "ad y ≤ ad (ad x ⋅ y)"
by (simp add: a_antitone a_subid_aux)
thus "d x + ad y ≤ ad (ad x ⋅ y)"
by (metis a2_eq a_antitone a_comm a_subid_aux dom_op_def add_lub)
qed
lemma d1_sum_var: "x + y ≤ (d x + d y) ⋅ (x + y)"
proof -
have "x + y = d x ⋅ x + d y ⋅ y"
by simp
also have "... ≤ (d x + d y) ⋅ x + (d x + d y) ⋅ y"
by (metis add_commute add_lub add_ub combine_common_factor)
finally show ?thesis
by (simp add: distrib_left)
qed
lemma a4: "ad (x + y) = ad x ⋅ ad y"
proof (rule order.antisym)
show "ad (x + y) ≤ ad x ⋅ ad y"
by (metis a_supdist add_commute mult_isor meet_ord)
hence "ad x ⋅ ad y = ad x ⋅ ad y + ad (x + y)"
using less_eq_def add_commute by simp
also have "... = ad (ad (ad x ⋅ ad y) ⋅ (x + y))"
by (metis a_closed a_exp)
finally show "ad x ⋅ ad y ≤ ad (x + y)"
using a_antitone d1_sum_var dom_op_def by auto
qed
lemma kat_prop: "d x ⋅ y ≤ y ⋅ d z ⟷ d x ⋅ y ⋅ ad z = 0"
proof
show "d x ⋅ y ≤ y ⋅ d z ⟹ d x ⋅ y ⋅ ad z = 0"
by (metis add_commute dom_op_def add_zerol annir as1 less_eq_def mult_isor mult_assoc)
next
assume h: "d x ⋅ y ⋅ ad z = 0"
hence "d x ⋅ y = d x ⋅ y ⋅ d z + d x ⋅ y ⋅ ad z"
by (metis dom_op_def as3 distrib_left mult_1_right)
thus "d x ⋅ y ≤ y ⋅ d z"
by (metis a_subid_aux add_commute dom_op_def h add_zerol mult_assoc)
qed
lemma shunt: "ad x ≤ ad y + ad z ⟷ ad x ⋅ d y ≤ ad z"
proof
assume "ad x ≤ ad y + ad z"
hence "ad x ⋅ d y ≤ ad y ⋅ d y + ad z ⋅ d y"
by (metis distrib_right mult_isor)
thus " ad x ⋅ d y ≤ ad z"
by (metis a_closed a_d_closed a_exp a_mul_d a_supdist dom_op_def dual_order.trans less_eq_def)
next
assume h: "ad x ⋅ d y ≤ ad z"
have "ad x = ad x ⋅ ad y + ad x ⋅ d y"
by (metis add_commute dom_op_def as3 distrib_left mult_1_right)
also have "... ≤ ad x ⋅ ad y + ad z"
using h add_lub dual_order.trans by blast
also have "... ≤ ad y + ad z"
by (metis a_subid_aux add_commute add_lub add_ub dual_order.trans)
finally show "ad x ≤ ad y + ad z"
by simp
qed
subsubsection ‹wp Calculus›
definition if_then_else :: "'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 while_inv :: "'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"
definition wp :: "'a ⇒ 'a ⇒ 'a" where
"wp x p = ad (x ⋅ ad p)"
lemma demod: " d p ≤ wp x q ⟷ d p ⋅ x ≤ x ⋅ d q"
by (metis as1 dom_op_def gla_1 kat_prop meet_ord mult_assoc wp_def)
lemma wp_weaken: "wp x p ≤ wp (x ⋅ ad q) (d p ⋅ ad q)"
by (metis a4 a_antitone a_d_closed a_mul_d dom_op_def gla_1 mult_isol mult_assoc wp_def)
lemma wp_seq [simp]: "wp (x ⋅ y) q = wp x (wp y q)"
using a2_eq dom_op_def mult_assoc wp_def by auto
lemma wp_seq_var: "p ≤ wp x r ⟹ r ≤ wp y q ⟹ p ≤ wp (x ⋅ y) q"
proof -
assume a1: "p ≤ wp x r"
assume a2: "r ≤ wp y q"
have "∀z. ¬ wp x r ≤ z ∨ p ≤ z"
using a1 dual_order.trans by blast
then show ?thesis
using a2 a_antitone mult_isol wp_def wp_seq by auto
qed
lemma wp_cond_var [simp]: "wp (if p then x else y fi) q = (ad p + wp x q) ⋅ (d p + wp y q)"
using a4 a_d_closed dom_op_def if_then_else_def distrib_right mult_assoc wp_def by auto
lemma wp_cond_aux1 [simp]: "d p ⋅ wp (if p then x else y fi) q = d p ⋅ wp x q"
proof -
have "d p ⋅ wp (if p then x else y fi) q = ad (ad p) ⋅ (ad p + wp x q) ⋅ (d p + wp y q)"
using dom_op_def mult.semigroup_axioms semigroup.assoc wp_cond_var by fastforce
also have "... = wp x q ⋅ d p ⋅ (d p + d (wp y q))"
using a_comm a_d_closed dom_op_def distrib_left wp_def by auto
also have "... = wp x q ⋅ d p"
by (metis a_exp dom_op_def add_ub meet_ord mult_assoc)
finally show ?thesis
by (simp add: a_comm dom_op_def wp_def)
qed
lemma wp_cond_aux2 [simp]: "ad p ⋅ wp (if p then x else y fi) q = ad p ⋅ wp y q"
by (metis (no_types) abel_semigroup.commute if_then_else_def a_d_closed add.abel_semigroup_axioms dom_op_def wp_cond_aux1)
lemma wp_cond [simp]: "wp (if p then x else y fi) q = (d p ⋅ wp x q) + (ad p ⋅ wp y q)"
by (metis as3 distrib_right dom_op_def mult_1_left wp_cond_aux2 wp_cond_aux1)
lemma wp_star_induct_var: "d q ≤ wp x q ⟹ d q ≤ wp (x⇧⋆) q"
using demod star_sim by blast
lemma wp_while: "d p ⋅ d r ≤ wp x p ⟹ d p ≤ wp (while r do x od) (d p ⋅ ad r)"
proof -
assume "d p ⋅ d r ≤ wp x p"
hence "d p ≤ wp (d r ⋅ x) p"
using dom_op_def mult.semigroup_axioms semigroup.assoc shunt wp_def by fastforce
hence "d p ≤ wp ((d r ⋅ x)⇧⋆) p"
using wp_star_induct_var by blast
thus ?thesis
by (simp add: while_def) (use local.dual_order.trans wp_weaken in fastforce)
qed
lemma wp_while_inv: "d p ≤ d i ⟹ d i ⋅ ad r ≤ d q ⟹ d i ⋅ d r ≤ wp x i ⟹ d p ≤ wp (while r inv i do x od) q"
proof -
assume a1: "d p ≤ d i" and a2: "d i ⋅ ad r ≤ d q" and "d i ⋅ d r ≤ wp x i"
hence "d i ≤ wp (while r inv i do x od) (d i ⋅ ad r)"
by (simp add: while_inv_def wp_while)
also have "... ≤ wp (while r inv i do x od) q"
by (metis a2 a_antitone a_d_closed dom_op_def mult_isol wp_def)
finally show ?thesis
using a1 dual_order.trans by blast
qed
lemma wp_while_inv_break: "d p ≤ wp y i ⟹ d i ⋅ ad r ≤ d q ⟹ d i ⋅ d r ≤ wp x i ⟹ d p ≤ wp (y ⋅ (while r inv i do x od)) q"
by (metis dom_op_def eq_refl mult_1_left mult_1_right wp_def wp_seq wp_seq_var wp_while_inv)
end
subsubsection ‹Soundness and Relation KAD›
notation relcomp (infixl ‹;› 70)
interpretation rel_d: dioid Id "{}" "(∪)" "(;)" "(⊆)" "(⊂)"
by (standard, auto)
lemma (in dioid) pow_inductl: "z + x ⋅ y ≤ y ⟹ x ^ i ⋅ z ≤ y"
apply (induct i; clarsimp simp add: add_lub)
by (metis local.dual_order.trans local.mult_isol mult_assoc)
lemma (in dioid) pow_inductr: "z + y ⋅ x ≤ y ⟹ z ⋅ x ^ i ≤ y"
apply (induct i; clarsimp simp add: add_lub)
proof -
fix i
assume "z ⋅ x ^ i ≤ y" "z ≤ y" "y ⋅ x ≤ y"
hence "(z ⋅ x ^ i) ⋅ x ≤ y"
using local.dual_order.trans local.mult_isor by blast
thus "z ⋅ (x ⋅ x ^ i) ≤ y"
by (simp add: mult_assoc local.power_commutes)
qed
lemma power_is_relpow: "rel_d.power X i = X ^^ i"
by (induct i, simp_all add: relpow_commute)
lemma rel_star_def: "X^* = (⋃i. rel_d.power X i)"
by (simp add: power_is_relpow rtrancl_is_UN_relpow)
lemma rel_star_contl: "X ; Y^* = (⋃i. X ; rel_d.power Y i)"
by (simp add: rel_star_def relcomp_UNION_distrib)
lemma rel_star_contr: "X^* ; Y = (⋃i. (rel_d.power X i) ; Y)"
by (simp add: rel_star_def relcomp_UNION_distrib2)
definition rel_ad :: "'a rel ⇒ 'a rel" where
"rel_ad R = {(x,x) | x. ¬ (∃y. (x,y) ∈ R)}"
interpretation rel_aka: antidomain_kleene_algebra Id "{}" "(∪)" "(;)" "(⊆)" "(⊂)" rtrancl rel_ad
apply standard
apply auto[2]
by (auto simp: rel_star_contr rel_d.pow_inductl rel_star_contl SUP_least rel_d.pow_inductr rel_ad_def)
subsubsection ‹Embedding Predicates in Relations›
type_synonym 'a pred = "'a ⇒ bool"
abbreviation p2r :: "'a pred ⇒ 'a rel" (‹⌈_⌉›) where
"⌈P⌉ ≡ {(s,s) |s. P s}"
lemma d_p2r [simp]: "rel_aka.dom_op ⌈P⌉ = ⌈P⌉"
by (auto simp: rel_aka.dom_op_def rel_ad_def)
lemma p2r_neg_hom [simp]: "rel_ad ⌈P⌉ = ⌈λs. ¬P s⌉"
by (auto simp: rel_ad_def)
lemma p2r_conj_hom [simp]: "⌈P⌉ ∩ ⌈Q⌉ = ⌈λs. P s ∧ Q s⌉"
by auto
lemma p2r_conj_hom_var [simp]: "⌈P⌉ ; ⌈Q⌉ = ⌈λs. P s ∧ Q s⌉"
by auto
lemma p2r_disj_hom [simp]: "⌈P⌉ ∪ ⌈Q⌉ = ⌈λs. P s ∨ Q s⌉"
by auto
subsubsection ‹Store and Assignment›
type_synonym 'a store = "string ⇒ 'a"
definition gets :: "string ⇒ ('a store ⇒ 'a) ⇒ 'a store rel" (‹_ ::= _› [70, 65] 61) where
"v ::= e = {(s,s (v := e s)) |s. True}"
lemma wp_assign [simp]: "rel_aka.wp (v ::= e) ⌈Q⌉ = ⌈λs. Q (s (v := e s))⌉"
by (auto simp: rel_aka.wp_def gets_def rel_ad_def)
abbreviation spec_sugar :: "'a pred ⇒ 'a rel ⇒ 'a pred ⇒ bool" (‹PRE _ _ POST _› [64,64,64] 63) where
"PRE P X POST Q ≡ rel_aka.dom_op ⌈P⌉ ⊆ rel_aka.wp X ⌈Q⌉"
abbreviation if_then_else_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_aka.if_then_else ⌈P⌉ X Y"
abbreviation while_inv_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_aka.while_inv ⌈P⌉ ⌈I⌉ X"
subsubsection ‹Verification Example›
lemma euclid:
"PRE (λs::nat store. s ''x'' = x ∧ s ''y'' = y)
(WHILE (λs. s ''y'' ≠ 0) INV (λs. gcd (s ''x'') (s ''y'') = gcd x y)
DO
(''z'' ::= (λs. s ''y''));
(''y'' ::= (λs. s ''x'' mod s ''y''));
(''x'' ::= (λs. s ''z''))
OD)
POST (λs. s ''x'' = gcd x y)"
apply (rule rel_aka.wp_while_inv, simp_all) using gcd_red_nat by auto
context antidomain_kleene_algebra
begin
subsubsection‹Propositional Hoare Logic›
definition H :: "'a ⇒ 'a ⇒ 'a ⇒ bool" where
"H p x q ⟷ d p ≤ wp x q"
lemma H_skip: "H p 1 p"
by (simp add: H_def dom_op_def wp_def)
lemma H_cons: "d p ≤ d p' ⟹ d q' ≤ d q ⟹ H p' x q' ⟹ H p x q"
by (meson H_def demod mult_isol order_trans)
lemma H_seq: "H p x r ⟹ H r y q ⟹ H p (x ⋅ y) q"
by (metis H_def a_d_closed demod dom_op_def wp_seq_var)
lemma H_cond: "H (d p ⋅ d r) x q ⟹ H (d p ⋅ ad r) y q ⟹ H p (if r then x else y fi) q"
proof -
assume h1: "H (d p ⋅ d r) x q" and h2: "H (d p ⋅ ad r) y q"
hence h3: "d p ⋅ d r ≤ wp x q" and h4: "d p ⋅ ad r ≤ wp y q"
using H_def a_closed dom_op_def apply auto[1]
using H_def h2 a_closed dom_op_def by auto
hence h5: "d p ≤ ad r + wp x q" and h6: "d p ≤ d r + wp y q"
apply (simp add: dom_op_def shunt wp_def)
using h4 a_d_closed dom_op_def shunt wp_def by auto
hence "d p ≤ d p ⋅ (d r + wp y q)"
by (metis a_idem distrib_left dom_op_def less_eq_def)
also have "... ≤ (ad r + wp x q) ⋅ (d r + wp y q)"
by (simp add: h5 mult_isor)
finally show ?thesis
by (simp add: H_def)
qed
lemma H_loop: "H (d p ⋅ d r) x p ⟹ H p (while r do x od) (d p ⋅ ad r)"
by (metis (full_types) H_def a_closed dom_op_def wp_while)
lemma H_while_inv: "d p ≤ d i ⟹ d i ⋅ ad r ≤ d q ⟹ H (d i ⋅ d r) x i ⟹ H p (while r inv i do x od) q"
using H_def a_closed dom_op_def wp_while_inv by auto
end
subsubsection‹Definition of Refinement KAD›
class rkad = antidomain_kleene_algebra +
fixes R :: "'a ⇒ 'a ⇒ 'a"
assumes R_def: "x ≤ R p q ⟷ d p ≤ wp x q"
begin
subsubsection ‹Propositional Refinement Calculus›
lemma HR: "H p x q ⟷ x ≤ R p q"
by (simp add: H_def R_def)
lemma wp_R1: "d p ≤ wp (R p q) q"
using R_def by blast
lemma wp_R2: "x ≤ R (wp x q) q"
by (simp add: R_def wp_def)
lemma wp_R3: "d p ≤ wp x q ⟹ x ≤ R p q"
by (simp add: R_def)
lemma H_R1: "H p (R p q) q"
by (simp add: HR)
lemma H_R2: "H p x q ⟹ x ≤ R p q"
by (simp add: HR)
lemma R_skip: "1 ≤ R p p"
by (simp add: H_R2 H_skip)
lemma R_cons: "d p ≤ d p' ⟹ d q' ≤ d q ⟹ R p' q' ≤ R p q"
by (simp add: H_R1 H_R2 H_cons)
lemma R_seq: "(R p r) ⋅ (R r q) ≤ R p q"
using H_R1 H_R2 H_seq by blast
lemma R_cond: "if v then (R (d v ⋅ d p) q) else (R (ad v ⋅ d p) q) fi ≤ R p q"
by (simp add: H_R1 H_R2 H_cond a_comm dom_op_def)
lemma R_loop: "while q do (R (d p ⋅ d q) p) od ≤ R p (d p ⋅ ad q)"
by (simp add: H_R1 H_R2 H_loop)
end
subsubsection ‹Soundness and Relation RKAD›
definition rel_R :: "'a rel ⇒ 'a rel ⇒ 'a rel" where
"rel_R P Q = ⋃{X. rel_aka.dom_op P ⊆ rel_aka.wp X Q}"
interpretation rel_rkad: rkad Id "{}" "(∪)" "(;)" "(⊆)" "(⊂)" rtrancl rel_ad rel_R
by (standard, auto simp: rel_R_def rel_aka.dom_op_def rel_ad_def rel_aka.wp_def, blast)
subsubsection ‹Assignment Laws›
lemma R_assign: "(∀s. P s ⟶ Q (s (v := e s))) ⟹ (v ::= e) ⊆ rel_R ⌈P⌉ ⌈Q⌉"
by (auto simp: rel_rkad.R_def)
lemma H_assign_var: "(∀s. P s ⟶ Q (s (v := e s))) ⟹ rel_aka.H ⌈P⌉ (v ::= e) ⌈Q⌉"
by (auto simp: rel_aka.H_def rel_aka.dom_op_def rel_ad_def gets_def rel_aka.wp_def)
lemma R_assignr: "(∀s. Q' s ⟶ Q (s (v := e s))) ⟹ (rel_R ⌈P⌉ ⌈Q'⌉) ; (v ::= e) ⊆ rel_R ⌈P⌉ ⌈Q⌉"
apply (subst rel_rkad.HR[symmetric], rule rel_aka.H_seq) defer
by (erule H_assign_var, simp add: rel_rkad.H_R1)
lemma R_assignl: "(∀s. P s ⟶ P' (s (v := e s))) ⟹ (v ::= e) ; (rel_R ⌈P'⌉ ⌈Q⌉) ⊆ rel_R ⌈P⌉ ⌈Q⌉"
by (subst rel_rkad.HR[symmetric], rule rel_aka.H_seq, erule H_assign_var, simp add: rel_rkad.H_R1)
subsubsection ‹Refinement Example›
lemma var_swap_ref1:
"rel_R ⌈λs. s ''x'' = a ∧ s ''y'' = b⌉ ⌈λs. s ''x'' = b ∧ s ''y'' = a⌉
⊇ (''z'' ::= (λs. s ''x'')); rel_R ⌈λs. s ''z'' = a ∧ s ''y'' = b⌉ ⌈λs. s ''x'' = b ∧ s ''y'' = a⌉"
by (rule R_assignl, auto)
lemma var_swap_ref2:
"rel_R ⌈λs. s ''z'' = a ∧ s ''y'' = b⌉ ⌈λs. s ''x'' = b ∧ s ''y'' = a⌉
⊇ (''x'' ::= (λs. s ''y'')); rel_R ⌈λs. s ''z'' = a ∧ s ''x'' = b⌉ ⌈λs. s ''x'' = b ∧ s ''y'' = a⌉"
by (rule R_assignl, auto)
lemma var_swap_ref3:
"rel_R ⌈λs. s ''z'' = a ∧ s ''x'' = b⌉ ⌈λs. s ''x'' = b ∧ s ''y'' = a⌉
⊇ (''y'' ::= (λs. s ''z'')); rel_R ⌈λs. s ''x'' = b ∧ s ''y'' = a⌉ ⌈λs. s ''x'' = b ∧ s ''y'' = a⌉"
by (rule R_assignl, auto)
lemma var_swap_ref_var:
"rel_R ⌈λs. s ''x'' = a ∧ s ''y'' = b⌉ ⌈λs. s ''x'' = b ∧ s ''y'' = a⌉
⊇ (''z'' ::= (λs. s ''x'')); (''x'' ::= (λs. s ''y'')); (''y'' ::= (λs. s ''z''))"
using var_swap_ref1 var_swap_ref2 var_swap_ref3 rel_rkad.R_skip by fastforce
end