Theory VC_KAT_Examples

(* Title: Verification 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 ‹Verification Examples›

theory VC_KAT_Examples
  imports VC_KAT
begin

lemma euclid:
  "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 (rule sH_while_inv)
  apply simp_all
  apply force
  apply (intro rel_kat.H_seq)
  apply (subst H_assign, simp)+
  apply (intro H_assign_var)
  using gcd_red_nat by auto

lemma maximum: 
  "PRE (λs:: nat store. True)
   (IF (λs. s ''x'' ≥ s ''y'') 
    THEN (''z'' ::= (λs. s ''x''))
    ELSE (''z'' ::= (λs. s ''y''))
    FI)
   POST (λs. s ''z'' = max (s ''x'') (s ''y''))"
  by auto

lemma integer_division: 
  "PRE (λs::nat store. s ''x'' ≥ 0)
    (''q'' ::= (λs. 0)); 
    (''r'' ::= (λs. s ''x''));
    (WHILE (λs. s ''y'' ≤ s ''r'') INV (λs. s ''x'' = s ''q'' * s ''y'' + s ''r'' ∧ s ''r'' ≥ 0)
     DO
      (''q'' ::= (λs. s ''q'' + 1));
      (''r'' ::= (λs. s ''r'' - s ''y''))
      OD)
   POST (λs. s ''x'' = s ''q'' * s ''y'' + s ''r'' ∧ s ''r'' ≥ 0 ∧ s ''r'' < s ''y'')"
  apply (intro rel_kat.H_seq, subst sH_while_inv, simp_all)
  apply auto[1]
  apply (intro rel_kat.H_seq)
  by (subst H_assign, simp_all)+

lemma imp_reverse:
  "PRE (λs:: 'a list store. s ''x'' = X)
   (''y'' ::= (λs. []));
   (WHILE (λs. s ''x'' ≠ []) INV (λs. rev (s ''x'') @ s ''y'' = rev X)
    DO 
     (''y'' ::= (λs. hd (s ''x'') # s ''y'')); 
     (''x'' ::= (λs. tl (s ''x'')))
    OD) 
   POST (λs. s ''y''= rev X )"
  apply (intro rel_kat.H_seq, rule sH_while_inv)
  apply auto[2]
  apply (rule rel_kat.H_seq, rule H_assign_var)
  apply auto[1]
  apply (rule H_assign_var)
  apply (clarsimp, metis append.simps(1) append.simps(2) append_assoc hd_Cons_tl rev.simps(2))
  by simp

end