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