Theory VC_KAT_scratch
section ‹Two Standalone Components›
theory VC_KAT_scratch
imports Main
begin
subsection ‹Component Based on Kleene Algebra with Tests›
text ‹This component supports the verification and step-wise refinement of simple while programs
in a partial correctness setting.›
subsubsection ‹KAT: Definition 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
apply (standard, simp_all add: less_def less_eq_def add_commute)
apply force
by (metis add_assoc)
lemma mult_isol: "x ≤ y ⟹ z ⋅ x ≤ z ⋅ y"
by (metis distrib_left less_eq_def)
lemma mult_isor: "x ≤ y ⟹ x ⋅ z ≤ y ⋅ z"
by (metis distrib_right less_eq_def)
lemma add_iso: "x ≤ y ⟹ x + z ≤ y + z"
by (metis (no_types, lifting) abel_semigroup.commute add.abel_semigroup_axioms add.semigroup_axioms add_idem less_eq_def semigroup.assoc)
lemma add_lub: "x + y ≤ z ⟷ x ≤ z ∧ y ≤ z"
by (metis add_assoc add.left_commute add_idem 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 kat = kleene_algebra +
fixes at :: "'a ⇒ 'a"
assumes test_one [simp]: "at (at 1) = 1"
and test_mult [simp]: "at (at (at (at x) ⋅ at (at y))) = at (at y) ⋅ at (at x)"
and test_mult_comp [simp]: "at x ⋅ at (at x) = 0"
and test_de_morgan: "at x + at y = at (at (at x) ⋅ at (at y))"
begin
definition t_op :: "'a ⇒ 'a" ("t_" [100] 101) where
"t x = at (at x)"
lemma t_n [simp]: "t (at x) = at x"
by (metis add_idem test_de_morgan test_mult t_op_def)
lemma t_comm: "t x ⋅ t y = t y ⋅ t x"
by (metis add_commute test_de_morgan test_mult t_op_def)
lemma t_idem [simp]: "t x ⋅ t x = t x"
by (metis add_idem test_de_morgan test_mult t_op_def)
lemma t_mult_closed [simp]: "t (t x ⋅ t y) = t x ⋅ t y"
using t_comm t_op_def by auto
subsubsection‹Propositional Hoare Logic›
definition H :: "'a ⇒ 'a ⇒ 'a ⇒ bool" where
"H p x q ⟷ t p ⋅ x ≤ x ⋅ t q"
definition if_then_else :: "'a ⇒ 'a ⇒ 'a ⇒ 'a" ("if _ then _ else _ fi" [64,64,64] 63) where
"if p then x else y fi = t p ⋅ x + at p ⋅ y"
definition while :: "'a ⇒ 'a ⇒ 'a" ("while _ do _ od" [64,64] 63) where
"while p do x od = (t p ⋅ x)⇧⋆ ⋅ at 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"
lemma H_skip: "H p 1 p"
by (simp add: H_def)
lemma H_cons: "t p ≤ t p' ⟹ t q' ≤ t q ⟹ H p' x q' ⟹ H p x q"
by (meson H_def mult_isol mult_isor order.trans)
lemma H_seq: "H r y q ⟹ H p x r ⟹ H p (x ⋅ y) q"
proof -
assume h1: "H p x r" and h2: "H r y q"
hence h3: "t p ⋅ x ≤ x ⋅ t r" and h4: "t r ⋅ y ≤ y ⋅ t q"
using H_def apply blast using H_def h2 by blast
hence "t p ⋅ x ⋅ y ≤ x ⋅ t r ⋅ y"
using mult_isor by blast
also have "... ≤ x ⋅ y ⋅ t q"
by (simp add: h4 mult_isol mult_assoc)
finally show ?thesis
by (simp add: H_def mult_assoc)
qed
lemma H_cond: "H (t p ⋅ t r) x q ⟹ H (t p ⋅ at r) y q ⟹ H p (if r then x else y fi) q"
proof -
assume h1: "H (t p ⋅ t r) x q" and h2: "H (t p ⋅ at r) y q"
hence h3: "t r ⋅ t p ⋅ t r ⋅ x ≤ t r ⋅ x ⋅ t q" and h4: "at r ⋅ t p ⋅ at r ⋅ y ≤ at r ⋅ y ⋅ t q"
by (simp add: H_def mult_isol mult_assoc, metis H_def h2 mult_isol mult_assoc t_mult_closed t_n)
hence h5: "t p ⋅ t r ⋅ x ≤ t r ⋅ x ⋅ t q" and h6: "t p ⋅ at r ⋅ y ≤ at r ⋅ y ⋅ t q"
by (simp add: mult_assoc t_comm, metis h4 mult_assoc t_comm t_idem t_n)
have "t p ⋅ (t r ⋅ x + at r ⋅ y) = t p ⋅ t r ⋅ x + t p ⋅ at r ⋅ y"
by (simp add: distrib_left mult_assoc)
also have "... ≤ t r ⋅ x ⋅ t q + t p ⋅ at r ⋅ y"
using h5 add_iso by blast
also have "... ≤ t r ⋅ x ⋅ t q + at r ⋅ y ⋅ t q"
by (simp add: add_commute h6 add_iso)
finally show ?thesis
by (simp add: H_def if_then_else_def distrib_right)
qed
lemma H_loop: "H (t p ⋅ t r) x p ⟹ H p (while r do x od) (t p ⋅ at r)"
proof -
assume "H (t p ⋅ t r) x p"
hence "t r ⋅ t p ⋅ t r ⋅ x ≤ t r ⋅ x ⋅ t p"
by (metis H_def distrib_left less_eq_def mult_assoc t_mult_closed)
hence "t p ⋅ t r ⋅ x ≤ t r ⋅ x ⋅ t p"
by (simp add: mult_assoc t_comm)
hence "t p ⋅ (t r ⋅ x)⇧⋆ ⋅ at r ≤ (t r ⋅ x)⇧⋆ ⋅ t p ⋅ at r"
by (metis mult_isor star_sim mult_assoc)
hence "t p ⋅ (t r ⋅ x)⇧⋆ ⋅ at r ≤ (t r ⋅ x)⇧⋆ ⋅ at r ⋅ t p ⋅ at r"
by (metis mult_assoc t_comm t_idem t_n)
thus ?thesis
by (metis H_def mult_assoc t_mult_closed t_n while_def)
qed
lemma H_while_inv: "t p ≤ t i ⟹ t i ⋅ at r ≤ t q ⟹ H (t i ⋅ t r) x i ⟹ H p (while r inv i do x od) q"
by (metis H_cons H_loop t_mult_closed t_n while_inv_def)
end
subsubsection‹Soundness and Relation KAT›
notation relcomp (infixl ";" 70)
interpretation rel_d: dioid Id "{}" "(∪)" "(;)" "(⊆)" "(⊂)"
by (standard, auto)
lemma (in dioid) power_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) power_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_at :: "'a rel ⇒ 'a rel" where
"rel_at X = Id ∩ - X"
interpretation rel_kat: kat Id "{}" "(∪)" "(;)" "(⊆)" "(⊂)" rtrancl rel_at
apply standard
apply auto[2]
by (auto simp: rel_star_contr rel_d.power_inductl rel_star_contl SUP_least rel_d.power_inductr rel_at_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 t_p2r [simp]: "rel_kat.t_op ⌈P⌉ = ⌈P⌉"
by (auto simp add: rel_kat.t_op_def rel_at_def)
lemma p2r_neg_hom [simp]: "rel_at ⌈P⌉ = ⌈λs. ¬ P s⌉"
by (auto simp: rel_at_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
lemma impl_prop [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 H_assign: "rel_kat.H ⌈λs. P (s (v := e s))⌉ (v ::= e) ⌈P⌉"
by (auto simp: gets_def rel_kat.H_def rel_kat.t_op_def rel_at_def)
lemma H_assign_var: "(∀s. P s ⟶ Q (s (v := e s))) ⟹ rel_kat.H ⌈P⌉ (v ::= e) ⌈Q⌉"
by (auto simp: gets_def rel_kat.H_def rel_kat.t_op_def rel_at_def)
abbreviation H_sugar :: "'a pred ⇒ 'a rel ⇒ 'a pred ⇒ bool" ("PRE _ _ POST _" [64,64,64] 63) where
"PRE P X POST Q ≡ rel_kat.H ⌈P⌉ 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_kat.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_kat.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_kat.H_while_inv, simp_all, clarsimp)
apply (intro rel_kat.H_seq)
apply (subst H_assign, simp)+
apply (rule H_assign_var)
using gcd_red_nat by auto
subsubsection ‹Definition of Refinement KAT›
class rkat = kat +
fixes R :: "'a ⇒ 'a ⇒ 'a"
assumes R1: "H p (R p q) q"
and R2: "H p x q ⟹ x ≤ R p q"
begin
subsubsection ‹Propositional Refinement Calculus›
lemma R_skip: "1 ≤ R p p"
by (simp add: H_skip R2)
lemma R_cons: "t p ≤ t p' ⟹ t q' ≤ t q ⟹ R p' q' ≤ R p q"
by (simp add: H_cons R2 R1)
lemma R_seq: "(R p r) ⋅ (R r q) ≤ R p q"
using H_seq R2 R1 by blast
lemma R_cond: "if v then (R (t v ⋅ t p) q) else (R (at v ⋅ t p) q) fi ≤ R p q"
by (metis H_cond R1 R2 t_comm t_n)
lemma R_loop: "while q do (R (t p ⋅ t q) p) od ≤ R p (t p ⋅ at q)"
by (simp add: H_loop R2 R1)
end
subsubsection ‹Soundness and Relation RKAT›
definition rel_R :: "'a rel ⇒ 'a rel ⇒ 'a rel" where
"rel_R P Q = ⋃{X. rel_kat.H P X Q}"
interpretation rel_rkat: rkat Id "{}" "(∪)" "(;)" "(⊆)" "(⊂)" rtrancl rel_at rel_R
by (standard, auto simp: rel_R_def rel_kat.H_def rel_kat.t_op_def rel_at_def)
subsubsection ‹Assignment Laws›
lemma R_assign: "(∀s. P s ⟶ Q (s (v := e s))) ⟹ (v ::= e) ⊆ rel_R ⌈P⌉ ⌈Q⌉"
by (simp add: H_assign_var rel_rkat.R2)
lemma R_assignr: "(∀s. Q' s ⟶ Q (s (v := e s))) ⟹ (rel_R ⌈P⌉ ⌈Q'⌉) ; (v ::= e) ⊆ rel_R ⌈P⌉ ⌈Q⌉"
proof -
assume a1: "∀s. Q' s ⟶ Q (s(v := e s))"
have "∀p pa cs f. ∃fa. (p fa ∨ cs ::= f ⊆ rel_R ⌈p⌉ ⌈pa⌉) ∧ (¬ pa (fa(cs := f fa::'a)) ∨ cs ::= f ⊆ rel_R ⌈p⌉ ⌈pa⌉)"
using R_assign by blast
hence "v ::= e ⊆ rel_R ⌈Q'⌉ ⌈Q⌉"
using a1 by blast
thus ?thesis
by (meson dual_order.trans rel_d.mult_isol rel_rkat.R_seq)
qed
lemma R_assignl: "(∀s. P s ⟶ P' (s (v := e s))) ⟹ (v ::= e) ; (rel_R ⌈P'⌉ ⌈Q⌉) ⊆ rel_R ⌈P⌉ ⌈Q⌉"
proof -
assume a1: "∀s. P s ⟶ P' (s(v := e s))"
have "∀p pa cs f. ∃fa. (p fa ∨ cs ::= f ⊆ rel_R ⌈p⌉ ⌈pa⌉) ∧ (¬ pa (fa(cs := f fa::'a)) ∨ cs ::= f ⊆ rel_R ⌈p⌉ ⌈pa⌉)"
using R_assign by blast
then have "v ::= e ⊆ rel_R ⌈P⌉ ⌈P'⌉"
using a1 by blast
then show ?thesis
by (meson dual_order.trans rel_d.mult_isor rel_rkat.R_seq)
qed
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_rkat.R_skip by fastforce
end