Theory VC_RKAT

(* Title: Refinement Component Based on KAT
   Author: Victor Gomes, Georg Struth
   Maintainer: Victor Gomes <victor.gomes@cl.cam.ac.uk>
               Georg Struth <g.struth@sheffield.ac.uk> 
*)

theory VC_RKAT
  imports "../RKAT_Models"

begin

text ‹This component supports the step-wise refinement of simple while programs
in a partial correctness setting.›

subsubsection ‹Assignment Laws›

text ‹The store model is taken from KAT›

lemma R_assign: "(∀s. P s ⟶ Q (s (v := e s))) ⟹ (v ::= e) ⊆ rel_R ⌈P⌉ ⌈Q⌉"
proof - 
  assume "(∀s. P s ⟶ Q (s (v := e s)))"
  hence "rel_kat.H ⌈P⌉ (v ::= e) ⌈Q⌉"
    by (rule H_assign_var)
  thus ?thesis
    by (rule rel_rkat.R2)
qed

lemma R_assignr: "(∀s. Q' s ⟶ Q (s (v := e s))) ⟹ (rel_R ⌈P⌉ ⌈Q'⌉) ; (v ::= e) ⊆ rel_R ⌈P⌉ ⌈Q⌉"  
  by (metis H_assign_var rel_kat.H_seq rel_rkat.R1 rel_rkat.R2)   

lemma R_assignl: "(∀s. P s ⟶ P' (s (v := e s))) ⟹ (v ::= e) ; (rel_R ⌈P'⌉ ⌈Q⌉) ⊆ rel_R ⌈P⌉ ⌈Q⌉"
  by (metis H_assign_var rel_kat.H_seq rel_rkat.R1 rel_rkat.R2)

subsubsection ‹Simplified Refinement Laws›

lemma R_cons: "(∀s. P s ⟶ P' s) ⟹ (∀s. Q' s ⟶ Q s) ⟹ rel_R ⌈P'⌉ ⌈Q'⌉ ⊆ rel_R ⌈P⌉ ⌈Q⌉"
  by (simp add: rel_rkat.R1 rel_rkat.R2 sH_cons_1 sH_cons_2)

lemma if_then_else_ref: "X ⊆ X' ⟹ Y ⊆ Y' ⟹ IF P THEN X ELSE Y FI ⊆ IF P THEN X' ELSE Y' FI"
  by (auto simp: rel_kat.ifthenelse_def)
                                     
lemma while_ref: "X ⊆ X' ⟹ WHILE P DO X OD ⊆ WHILE P DO X' OD"
  by (simp add: rel_kat.while_def rel_dioid.mult_isol rel_dioid.mult_isor rel_kleene_algebra.star_iso)
                                                               
end