Theory VC_KAT_Examples2

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

subsubsection ‹Verification Examples with Automated VCG›

theory VC_KAT_Examples2
  imports VC_KAT "HOL-Eisbach.Eisbach"
begin

text ‹The following simple tactic for verification condition generation has been 
implemented with the Eisbach proof methods language.›

named_theorems hl_intro

declare sH_while_inv [hl_intro]
  rel_kat.H_seq [hl_intro]
  H_assign_var [hl_intro]
  rel_kat.H_cond [hl_intro]

method hoare = (rule hl_intro; hoare?)

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 hoare
   using gcd_red_nat 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'')"
   by hoare auto

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 hoare 
   apply auto[3]
   apply (clarsimp, metis (no_types, lifting) Cons_eq_appendI append_eq_append_conv2 hd_Cons_tl rev.simps(2) self_append_conv)
   by simp

end