Theory RKAT
subsection ‹Refinement Component›
theory RKAT
imports "AVC_KAT/VC_KAT"
begin
subsubsection‹RKAT: Definition and Basic Properties›
text ‹A refinement KAT is a KAT expanded by Morgan's specification statement.›
class rkat = kat +
fixes R :: "'a ⇒ 'a ⇒ 'a"
assumes spec_def: "x ≤ R p q ⟷ H p x q"
begin
lemma R1: "H p (R p q) q"
using spec_def by blast
lemma R2: "H p x q ⟹ x ≤ R p q"
by (simp add: spec_def)
subsubsection‹Propositional Refinement Calculus›
lemma R_skip: "1 ≤ R p p"
proof -
have "H p 1 p"
by (simp add: H_skip)
thus ?thesis
by (rule R2)
qed
lemma R_cons: "t p ≤ t p' ⟹ t q' ≤ t q ⟹ R p' q' ≤ R p q"
proof -
assume h1: "t p ≤ t p'" and h2: "t q' ≤ t q"
have "H p' (R p' q') q'"
by (simp add: R1)
hence "H p (R p' q') q"
using h1 h2 H_cons_1 H_cons_2 by blast
thus ?thesis
by (rule R2)
qed
lemma R_seq: "(R p r) ⋅ (R r q) ≤ R p q"
proof -
have "H p (R p r) r" and "H r (R r q) q"
by (simp add: R1)+
hence "H p ((R p r) ⋅ (R r q)) q"
by (rule H_seq_swap)
thus ?thesis
by (rule R2)
qed
lemma R_cond: "if v then (R (t v ⋅ t p) q) else (R (n v ⋅ t p) q) fi ≤ R p q"
proof -
have "H (t v ⋅ t p) (R (t v ⋅ t p) q) q" and "H (n v ⋅ t p) (R (n v ⋅ t p) q) q"
by (simp add: R1)+
hence "H p (if v then (R (t v ⋅ t p) q) else (R (n v ⋅ t p) q) fi) q"
by (simp add: H_cond n_mult_comm)
thus ?thesis
by (rule R2)
qed
lemma R_loop: "while q do (R (t p ⋅ t q) p) od ≤ R p (t p ⋅ n q)"
proof -
have "H (t p ⋅ t q) (R (t p ⋅ t q) p) p"
by (simp_all add: R1)
hence "H p (while q do (R (t p ⋅ t q) p) od) (t p ⋅ n q)"
by (simp add: H_loop)
thus ?thesis
by (rule R2)
qed
lemma R_zero_one: "x ≤ R 0 1"
proof -
have "H 0 x 1"
by (simp add: H_def)
thus ?thesis
by (rule R2)
qed
lemma R_one_zero: "R 1 0 = 0"
proof -
have "H 1 (R 1 0) 0"
by (simp add: R1)
thus ?thesis
by (simp add: H_def join.le_bot)
qed
end
end