Theory VC_KAD_wf_Examples

(* Title: Verification Component Based on Divergence Kleene Algebra for Total Correctness: Examples
   Author: Victor Gomes, Georg Struth
   Maintainer: Victor Gomes <victor.gomes@cl.cam.ac.uk>
               Georg Struth <g.struth@sheffield.ac.uk> 
*)

subsubsection‹Verification Examples›

theory VC_KAD_wf_Examples
  imports VC_KAD_wf
begin

text ‹The example should be taken with a grain of salt. More work is needed to make 
the while rule cooperate with simplification.›

lemma euclid:
  "rel_nabla (
    ⌈λs::nat store. 0 < s ''y''⌉ ; 
      ((''z'' ::= (λs. s ''y'')) ; 
      (''y'' ::= (λs. s ''x'' mod s ''y'')) ;
      (''x'' ::= (λs. s ''z'')))) 
    = {}
    ⟹
  PRE (λs::nat store. s ''x'' = x ∧ s ''y'' = y)
   (WHILE (λs. s ''y'' ≠ 0) INV (λs. gcd (s ''x'') (s ''y'') = gcd x y) 
    DO
     (''z'' ::= (λs. s ''y''));
     (''y'' ::= (λs. s ''x'' mod s ''y''));
     (''x'' ::= (λs. s ''z''))
    OD)
   POST (λs. s ''x'' = gcd x y)"
  apply (subst rel_fdivka.fbox_arden_whilei[symmetric], simp_all)
  using gcd_red_nat gr0I by force

text ‹The termination assumption is now explicit in the verification proof. Here it is left 
untouched. Means beyond these components are required for discharging it.›

end