Theory VC_KAD_dual_Examples

(* Title: Verification Component Based on KAD for Forward Reasoning: 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_dual_Examples
imports VC_KAD_dual

begin

text‹The proofs are essentially the same as with forward boxes.›

lemma euclid:
  "FPRE (λ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)"
  by (rule rel_modal_kleene_algebra.bdia_whilei, auto simp: gcd_non_0_nat)

lemma euclid_diff: 
   "FPRE (λ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 (rule rel_modal_kleene_algebra.bdia_whilei, simp_all)
  apply auto[1]
  by (metis gcd.commute gcd_diff1_nat le_cases nat_less_le)

lemma varible_swap:
  "FPRE (λs. s ''x'' = a ∧ s ''y'' = b)   
    (''z'' ::= (λs. s ''x''));
    (''x'' ::= (λs. s ''y''));
    (''y'' ::= (λs. s ''z''))
   POST (λs. s ''x'' = b ∧ s ''y'' = a)"
  by simp

lemma maximum: 
  "FPRE (λ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: 
  "FPRE (λ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 (rule rel_modal_kleene_algebra.bdia_whilei_break, simp_all, auto simp: p2r_def)

lemma factorial:
  "FPRE (λ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 (rule rel_modal_kleene_algebra.bdia_whilei_break, simp_all, auto simp: p2r_def)
 
lemma my_power:
  "FPRE (λ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 (rule rel_modal_kleene_algebra.bdia_whilei_break, simp_all, auto simp add: p2r_def)

lemma imp_reverse:
  "FPRE (λ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 (rule rel_modal_kleene_algebra.bdia_whilei_break, simp_all)
  apply auto[1]
  by (safe, metis append.simps append_assoc hd_Cons_tl rev.simps(2))

end