Theory VC_KAD_Examples2

(* Title: Verification Component Based on KAD: 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_KAD_Examples2
imports VC_KAD "HOL-Eisbach.Eisbach"
begin

text ‹We have provide a simple tactic in the Eisbach proof method language. Additional simplification
steps are sometimes needed to bring the resulting verification conditions into shape for first-order automated
theorem proving.›


named_theorems ht

declare rel_antidomain_kleene_algebra.fbox_whilei [ht]
  rel_antidomain_kleene_algebra.fbox_seq_var [ht]
  subset_refl[ht]

method hoare = (rule ht; hoare?)

lemma euclid2:
  "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 euclid_diff2: 
   "PRE (λs::nat store. s ''x'' = x ∧ s ''y'' = y ∧ x > 0 ∧ y > 0)
    (WHILE (λs. s ''x''≠ s ''y'') INV (λs. gcd (s ''x'') (s ''y'') = gcd x y) 
     DO
        (IF (λs. s ''x'' >  s ''y'')
         THEN (''x'' ::= (λs. s ''x'' - s ''y''))
         ELSE (''y'' ::= (λs. s ''y'' - s ''x''))
         FI)
    OD)
    POST (λs. s ''x'' = gcd x y)"
  apply (hoare, simp_all) 
  apply auto[1]
  by (metis gcd.commute gcd_diff1_nat le_cases nat_less_le)

lemma integer_division2: 
  "PRE (λs::nat store. x ≥ 0)
    (''q'' ::= (λs. 0)); 
    (''r'' ::= (λs. x));
    (WHILE (λs. y ≤ s ''r'') INV (λs. x = s ''q'' * y + s ''r'' ∧ s ''r'' ≥ 0)
     DO
      (''q'' ::= (λs. s ''q'' + 1));
      (''r'' ::= (λs. s ''r'' - y))
      OD)
   POST (λs. x = s ''q'' * y + s ''r'' ∧ s ''r'' ≥ 0 ∧ s ''r'' < y)"
   by hoare simp_all

lemma factorial2:
  "PRE (λs::nat store. True)
   (''x'' ::= (λs. 0));
   (''y'' ::= (λs. 1));
   (WHILE (λs. s ''x'' ≠ x0) INV (λs. s ''y'' = fact (s ''x''))
   DO
     (''x'' ::= (λs. s ''x'' + 1));
     (''y'' ::= (λs. s ''y'' ⋅ s ''x''))
   OD)
   POST (λs. s ''y'' = fact x0)"
  by hoare simp_all

lemma my_power2:
  "PRE (λs::nat store. True)
   (''i'' ::= (λs. 0));
   (''y'' ::= (λs. 1));
   (WHILE (λs. s ''i'' < n) INV (λs. s ''y'' = x ^ (s ''i'') ∧ s ''i'' ≤ n)
     DO
       (''y'' ::= (λs. (s ''y'') * x));
       (''i'' ::= (λs. s ''i'' + 1))
     OD)
   POST (λs. s ''y'' = x ^ n)"
  by hoare auto

lemma imp_reverse2:
  "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, simp_all)
  apply auto[1]
  by (clarsimp, metis append.simps append_assoc hd_Cons_tl rev.simps(2))

end