Theory VC_KAT

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

section ‹Components Based on Kleene Algebra with Tests›

subsection ‹Verification Component›      

text ‹This component supports the verification of simple while programs
in a partial correctness setting.›

theory VC_KAT
imports "../P2S2R"
        KAT_and_DRA.PHL_KAT 
        KAT_and_DRA.KAT_Models

begin

text‹This first part changes some of the facts from the AFP KAT theories. It should be added to KAT in the next AFP version. 
Currently these facts provide an interface between the KAT theories and the verification component.›

no_notation if_then_else ("if _ then _ else _ fi" [64,64,64] 63)
no_notation while ("while _ do _ od" [64,64] 63)
no_notation Archimedean_Field.ceiling ("⌈_⌉")

notation relcomp (infixl ";" 70)               
notation p2r ("⌈_⌉")

context kat 
begin

subsubsection ‹Definitions of Hoare Triple›

definition H :: "'a ⇒ 'a ⇒ 'a ⇒ bool" where
  "H p x q ⟷ t p ⋅ x ≤ x ⋅ t q" 

lemma H_var1: "H p x q ⟷ t p ⋅ x ⋅ n q = 0"
  by (metis H_def n_kat_3 t_n_closed)

lemma H_var2: "H p x q ⟷ t p ⋅ x = t p ⋅ x ⋅ t q"
  by (simp add: H_def n_kat_2)

subsubsection ‹Syntax for Conditionals and Loops›

definition ifthenelse :: "'a ⇒ 'a ⇒ 'a ⇒ 'a" ("if _ then _ else _ fi" [64,64,64] 63) where
  "if p then x else y fi = (t p ⋅ x + n p ⋅ y)"

definition while :: "'a ⇒ 'a ⇒ 'a" ("while _ do _ od" [64,64] 63) where
  "while b do x od = (t b ⋅ x)⇧⋆ ⋅ n b"

definition while_inv :: "'a ⇒ 'a ⇒ 'a ⇒ 'a" ("while _ inv _ do _ od" [64,64,64] 63) where
  "while p inv i do x od = while p do x od"

subsubsection ‹Propositional Hoare Logic›

lemma H_skip:  "H p 1 p"
  by (simp add: H_def)

lemma H_cons_1: "t p ≤ t p' ⟹ H p' x q ⟹ H p x q"
  using H_def phl_cons1 by blast

lemma H_cons_2: "t q' ≤ t q ⟹ H p x q' ⟹ H p x q"
  using H_def phl_cons2 by blast          

lemma H_cons: "t p ≤ t p' ⟹ t q' ≤ t q ⟹ H p' x q' ⟹ H p x q"
  by (simp add: H_cons_1 H_cons_2)

lemma H_seq_swap: "H p x r ⟹ H r y q ⟹ H p (x ⋅ y) q"
  by (simp add: H_def phl_seq)

lemma H_seq: "H r y q ⟹ H p x r ⟹ H p (x ⋅ y) q"
  by (simp add: H_seq_swap)

lemma H_exp1: "H (t p ⋅ t r) x q ⟹ H p (t r ⋅ x) q"
  using H_def n_de_morgan_var2 phl.ht_at_phl_export1 by auto

lemma H_exp2: "H p x q ⟹ H p (x ⋅ t r) (t q ⋅ t r)"
  by (metis H_def phl.ht_at_phl_export2 test_mult)

lemma H_cond_iff: "H p (if r then x else y fi) q ⟷ H (t p ⋅ t r) x q ∧ H (t p ⋅ n r) y q"
proof -
  have "H p (if r then x else y fi) q ⟷ t p ⋅ (t r ⋅ x + n r ⋅ y) ⋅ n q = 0"
    by (simp add: H_var1 ifthenelse_def)
  also have "... ⟷ t p ⋅ t r ⋅ x ⋅ n q + t p ⋅ n r ⋅ y ⋅ n q = 0"
    by (simp add: distrib_left mult_assoc)
  also have "... ⟷ t p ⋅ t r ⋅ x ⋅ n q = 0 ∧ t p ⋅ n r ⋅ y ⋅ n q = 0"
    by (metis add_0_left no_trivial_inverse)
  finally show ?thesis
    by (metis H_var1 test_mult)
qed

lemma H_cond: "H (t p ⋅ t r) x q ⟹ H (t p ⋅ n r) y q ⟹ H p (if r then x else y fi) q"
  by (simp add: H_cond_iff)

lemma H_loop: "H (t p ⋅ t r) x p ⟹ H p (while r do x od) (t p ⋅ n r)"
proof -
  assume a1: "H (t p ⋅ t r) x p"
  have "t (t p ⋅ n r) = n r ⋅ t p ⋅ n r"
    using n_preserve test_mult by presburger
  then show ?thesis
    using a1 H_def H_exp1 conway.phl.it_simr phl_export2 while_def by auto
qed

lemma H_while_inv: "t p ≤ t i ⟹ t i ⋅ n r ≤ t q ⟹ H (t i ⋅ t r) x i ⟹ H p (while r inv i do x od) q"
  by (metis H_cons H_loop test_mult while_inv_def)

text ‹Finally we prove a frame rule.›

lemma H_frame: "H p x p ⟹ H q x r ⟹ H (t p ⋅ t q) x (t p ⋅ t r)"
proof -
  assume "H p x p" and a: "H q x r"
  hence b: "t p ⋅ x ≤ x ⋅ t p" and "t q ⋅ x ≤ x ⋅ t r"
    using H_def apply blast using H_def a by blast
  hence "t p ⋅ t q ⋅ x ≤ t p ⋅ x ⋅ t r"
    by (simp add: mult_assoc mult_isol)
  also have "... ≤ x ⋅ t p ⋅ t r"
    by (simp add: b mult_isor)
  finally show ?thesis
    by (metis H_def mult_assoc test_mult)
qed
    
end

subsubsection ‹Store and Assignment›

text ‹The proper verification component starts here.›

type_synonym 'a store = "string  ⇒ 'a"

lemma t_p2r [simp]: "rel_dioid_tests.t ⌈P⌉ = ⌈P⌉"
  by (auto simp: p2r_def)

lemma impl_prop [simp]: "⌈P⌉ ⊆ ⌈Q⌉ ⟷ (∀s. P s ⟶  Q s)"
  by (auto simp: p2r_def)

lemma Id_simp [simp]: "Id ∩ (- Id ∪ X) = Id ∩ X" 
  by auto

lemma Id_p2r [simp]: "Id ∩ ⌈P⌉ = ⌈P⌉"
  by (auto simp: Id_def p2r_def)

lemma Id_p2r_simp [simp]: "Id ∩ (- Id ∪ ⌈P⌉) = ⌈P⌉"
  by simp 

text ‹Next we derive the assignment command and assignment rules.›

definition gets :: "string ⇒ ('a store ⇒ 'a) ⇒ 'a store rel" ("_ ::= _" [70, 65] 61) where 
  "v ::= e = {(s,s (v := e s)) |s. True}"

lemma H_assign_prop: "⌈λs. P (s (v := e s))⌉ ; (v ::= e) = (v ::= e) ; ⌈P⌉"
  by (auto simp: p2r_def gets_def)

lemma H_assign: "rel_kat.H ⌈λs. P (s (v := e s))⌉ (v ::= e) ⌈P⌉"
  by (auto simp add: rel_kat.H_def gets_def p2r_def)

lemma H_assign_var: "(∀s. P s ⟶ Q (s (v := e s))) ⟹ rel_kat.H ⌈P⌉ (v ::= e) ⌈Q⌉"
  by (auto simp: p2r_def gets_def rel_kat.H_def)

lemma H_assign_iff [simp]: "rel_kat.H ⌈P⌉ (v ::= e) ⌈Q⌉ ⟷ (∀s. P s ⟶ Q (s (v := e s)))"
  by (auto simp: p2r_def gets_def rel_kat.H_def)

lemma H_assign_floyd: " rel_kat.H ⌈P⌉ (v ::= e) ⌈λs. ∃w. s v = e (s(v := w)) ∧ P (s(v := w))⌉"
  by (rule H_assign_var, metis fun_upd_same fun_upd_triv fun_upd_upd)

subsubsection ‹Simplified Hoare Rules›

lemma sH_cons_1: "∀s. P s ⟶ P' s ⟹ rel_kat.H ⌈P'⌉ X ⌈Q⌉ ⟹ rel_kat.H ⌈P⌉ X ⌈Q⌉"
  by (rule rel_kat.H_cons_1, auto simp only: p2r_def)

lemma sH_cons_2: "∀s. Q' s ⟶ Q s ⟹ rel_kat.H ⌈P⌉ X ⌈Q'⌉ ⟹ rel_kat.H ⌈P⌉ X ⌈Q⌉"
  by (rule rel_kat.H_cons_2, auto simp only: p2r_def)

lemma sH_cons: "∀s. P s ⟶ P' s ⟹ ∀s. Q' s ⟶ Q s ⟹ rel_kat.H ⌈P'⌉ X ⌈Q'⌉ ⟹ rel_kat.H ⌈P⌉ X ⌈Q⌉"
  by (simp add: sH_cons_1 sH_cons_2)
  
lemma sH_cond: "rel_kat.H ⌈P ⊓ T⌉ X ⌈Q⌉ ⟹ rel_kat.H ⌈P ⊓ - T⌉ Y ⌈Q⌉  ⟹ rel_kat.H ⌈P⌉ (rel_kat.ifthenelse ⌈T⌉ X Y) ⌈Q⌉"
  by (rule rel_kat.H_cond, auto simp add: rel_kat.H_def p2r_def, blast+)

lemma sH_cond_iff: "rel_kat.H ⌈P⌉ (rel_kat.ifthenelse ⌈T⌉ X Y) ⌈Q⌉ ⟷ (rel_kat.H ⌈P ⊓ T⌉ X ⌈Q⌉ ∧ rel_kat.H ⌈P ⊓ - T⌉ Y ⌈Q⌉)"
  by (simp add: rel_kat.H_cond_iff)

lemma sH_while_inv: "∀s. P s ⟶ I s ⟹ ∀s. I s ∧ ¬ R s ⟶ Q s ⟹ rel_kat.H ⌈I ⊓ R⌉ X ⌈I⌉ 
                     ⟹ rel_kat.H ⌈P⌉ (rel_kat.while_inv ⌈R⌉ ⌈I⌉ X) ⌈Q⌉"
  by (rule rel_kat.H_while_inv, auto simp: p2r_def rel_kat.H_def, fastforce)

lemma sH_H: "rel_kat.H ⌈P⌉ X ⌈Q⌉ ⟷ (∀s s'. P s ⟶ (s,s') ∈ X ⟶ Q s')"
  by (simp add: rel_kat.H_def, auto simp add: p2r_def)

text ‹Finally we provide additional syntax for specifications and commands.›
 
abbreviation H_sugar :: "'a pred ⇒ 'a rel ⇒ 'a pred ⇒ bool" ("PRE _ _ POST _" [64,64,64] 63) where
  "PRE P X POST Q ≡ rel_kat.H ⌈P⌉ X ⌈Q⌉"

abbreviation if_then_else_sugar :: "'a pred ⇒ 'a rel ⇒ 'a rel ⇒ 'a rel" ("IF _ THEN _ ELSE _ FI" [64,64,64] 63) where
  "IF P THEN X ELSE Y FI ≡ rel_kat.ifthenelse ⌈P⌉ X Y"

abbreviation while_sugar :: "'a pred ⇒ 'a rel ⇒ 'a rel" ("WHILE _ DO _ OD" [64,64] 63) where
  "WHILE P  DO X OD ≡ rel_kat.while ⌈P⌉ X"

abbreviation while_inv_sugar :: "'a pred ⇒ 'a pred ⇒ 'a rel ⇒ 'a rel" ("WHILE _ INV _ DO _ OD" [64,64,64] 63) where
  "WHILE P INV I DO X OD ≡ rel_kat.while_inv ⌈P⌉ ⌈I⌉ X"

lemma H_cond_iff2[simp]: "PRE p (IF r THEN x ELSE y FI) POST q ⟷ (PRE (p ⊓ r) x POST q) ∧ (PRE (p ⊓ - r) y POST q)"
  by (simp add: rel_kat.H_cond_iff)

end