Theory VC_RKAT_Examples

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

subsubsection ‹Refinement Examples›

theory VC_RKAT_Examples 
  imports VC_RKAT
begin

text ‹Currently  there is only one example, and no tactic for automating refinement proofs is provided.›

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