Theory Path_Model_Example

(* Title: Verification Component Based on KAD: Trace Semantics
   Author: Victor Gomes, Georg Struth
   Maintainer: Victor Gomes <victor.gomes@cl.cam.ac.uk>
               Georg Struth <g.struth@sheffield.ac.uk> 
*)

subsection ‹Two Extensions›

subsubsection ‹KAD Component with Trace Semantics›

theory Path_Model_Example
  imports VC_KAD "HOL-Eisbach.Eisbach"
begin

text ‹This component supports the verification of simple while programs
in a partial correctness setting based on a program trace semantics.›

text ‹Program traces are modelled as non-empty paths or state sequences. The non-empty path model 
of Kleene algebra is taken from the AFP entry for Kleene algebra. Here we show that sets of paths form
antidomain Kleene Algebras.›

definition pp_a ::  "'a ppath set ⇒ 'a ppath set" where
  "pp_a X = {(Node u) |u. ¬ (∃v ∈ X. u = pp_first v)}"

interpretation ppath_aka: antidomain_kleene_algebra pp_a "(∪)" pp_prod pp_one "{}" "(⊆)" "(⊂)" pp_star
  apply standard
  apply (clarsimp simp add: pp_prod_def pp_a_def)
  apply (simp add: pp_prod_def pp_a_def, safe, metis pp_first.simps(1) pp_first_pp_fusion)
  by (auto simp: pp_a_def pp_one_def)   

text ‹A verification component can then be built with little effort, by and large reusing
parts of the relational components that are generic with respect to the store.›      

definition pp_gets :: "string ⇒ ('a store ⇒ 'a) ⇒ 'a store ppath set" (‹_ ::= _› [70, 65] 61) where 
  "v ::= e = {Cons s (Node (s (v := e s))) | s. True}"

definition p2pp :: "'a pred ⇒ 'a ppath set" where
  "p2pp P = {Node s |s. P s}"

lemma pp_a_neg [simp]: "pp_a (p2pp Q) = p2pp (-Q)"
  by (force simp add: pp_a_def p2pp_def)

lemma ppath_assign [simp]: "ppath_aka.fbox (v ::= e) (p2pp Q) = p2pp (λs. Q (s(v := e s)))"
  by (force simp: ppath_aka.fbox_def pp_a_def p2pp_def pp_prod_def pp_gets_def)      

no_notation spec_sugar (‹PRE _ _ POST _› [64,64,64] 63)
   and relcomp (infixl ‹;› 70)
   and cond_sugar (‹IF _ THEN _ ELSE _ FI› [64,64,64] 63)
   and whilei_sugar (‹WHILE _ INV _ DO _ OD› [64,64,64] 63)
   and gets (‹_ ::= _› [70, 65] 61)
   and rel_antidomain_kleene_algebra.fbox (‹wp›)
   and rel_antidomain_kleene_algebra.ads_d (‹rdom›)
   and p2r (‹⌈_⌉›)

notation ppath_aka.fbox (‹wp›)
  and ppath_aka.ads_d (‹rdom›)
  and p2pp (‹⌈_⌉›)
  and pp_prod (infixl ‹;› 70)

abbreviation spec_sugar :: "'a pred ⇒ 'a ppath set ⇒ 'a pred ⇒ bool" (‹PRE _ _ POST _› [64,64,64] 63) where
  "PRE P X POST Q ≡ rdom ⌈P⌉ ⊆ wp X ⌈Q⌉"

abbreviation cond_sugar :: "'a pred ⇒ 'a ppath set ⇒ 'a ppath set ⇒ 'a ppath set" (‹IF _ THEN _ ELSE _ FI› [64,64,64] 63) where
  "IF P THEN X ELSE Y FI ≡ ppath_aka.cond ⌈P⌉ X Y"

abbreviation whilei_sugar :: "'a pred ⇒ 'a pred ⇒ 'a ppath set ⇒ 'a ppath set" (‹WHILE _ INV _ DO _ OD› [64,64,64] 63) where
  "WHILE P INV I DO X OD ≡ ppath_aka.whilei ⌈P⌉ ⌈I⌉ X"

lemma [simp]: "p2pp P ∪ p2pp Q = p2pp (P ⊔ Q)"
  by (force simp: p2pp_def)

lemma [simp]: "p2pp P; p2pp Q = p2pp (P ⊓ Q)"
  by (force simp: p2pp_def pp_prod_def)

lemma [intro!]:  "P ≤ Q ⟹ ⌈P⌉ ⊆ ⌈Q⌉"
  by (force simp: p2pp_def)

lemma [simp]: "rdom ⌈P⌉ = ⌈P⌉"
  by (simp add: ppath_aka.addual.ars_r_def)

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)"
  by (rule ppath_aka.fbox_whilei, simp_all, auto simp: p2pp_def rel_ad_def gcd_non_0_nat)

lemma euclid_diff: 
   "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 (rule ppath_aka.fbox_whilei, simp_all)
  apply (simp_all add: p2pp_def) 
  apply auto[2]
  by (safe, metis gcd.commute gcd_diff1_nat le_cases nat_less_le)

lemma varible_swap:
  "PRE (λ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 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. 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 ppath_aka.fbox_whilei_break, auto)
 
text ‹We now reconsider these examples with an Eisbach tactic.›

named_theorems ht

declare ppath_aka.fbox_whilei [ht]
  ppath_aka.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)"
  by (hoare; clarsimp; metis gcd.commute gcd_diff1_nat le_cases nat_less_le)

lemma varible_swap2:
  "PRE (λ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 clarsimp

lemma maximum2: 
  "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_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 auto

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
  apply auto
  apply (metis append.simps append_assoc hd_Cons_tl rev.simps(2))
done

end