Theory VC_RKAT_Examples
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