Theory utp_sp

(*************************************************************************************************)
(* Project: The Isabelle/UTP Proof System                                                        *)
(* File: utp_sp.thy                                                                              *)
(* Authors: Yakoub Nemouchi (Virginia Tech, USA) and Simon Foster (University of York, UK)       *)
(* Emails: nemouchi@vt.edu and simon.foster@york.ac.uk                                           *)
(*************************************************************************************************)

section ‹ Strong Postcondition Calculus›

theory utp_sp
imports utp_wp
begin

named_theorems sp

method sp_tac = (simp add: sp)

consts
  usp :: "'a ⇒ 'b ⇒ 'c" (infix "sp" 60)
  
definition sp_upred :: "'α cond ⇒ ('α, 'β) urel ⇒ 'β cond" where
"sp_upred p Q = ⌊(⌈p⌉⇩> ;; Q) :: ('α, 'β) urel⌋⇩>"

adhoc_overloading
  usp sp_upred

declare sp_upred_def [upred_defs]

lemma sp_false [sp]: "p sp false = false"
  by (rel_simp) 

lemma sp_true [sp]: "q ≠ false ⟹ q sp true = true"
  by (rel_auto) 
    
lemma sp_assigns_r [sp]: 
  "vwb_lens x ⟹ (p sp x := e ) = (❙∃v ∙ p⟦«v»/x⟧ ∧ &x =⇩u e⟦«v»/x⟧)"
  by (rel_auto, metis vwb_lens_wb wb_lens.get_put, metis vwb_lens.put_eq) 

lemma sp_it_is_post_condition:
  "⦃p⦄C⦃p sp C⦄⇩u"
  by rel_blast
    
lemma sp_it_is_the_strongest_post:
  "`p sp C ⇒ Q`⟹⦃p⦄C⦃Q⦄⇩u"
  by rel_blast
    
lemma sp_so:
  "`p sp C ⇒ Q` = ⦃p⦄C⦃Q⦄⇩u"
  by rel_blast
    
theorem sp_hoare_link:
  "⦃p⦄Q⦃r⦄⇩u ⟷ (r ⊑ p sp Q)"
  by rel_auto   
                             
lemma sp_while_r [sp]: 
   assumes ‹`pre ⇒ I`› and ‹⦃I ∧ b⦄C⦃I'⦄⇩u› and ‹`I' ⇒ I`›
   shows "(pre sp invar I while⇩⊥ b do C od) = (¬b ∧ I)"
   unfolding sp_upred_def     
   oops  
     
theorem sp_eq_intro: "⟦⋀r. r sp P = r sp Q⟧ ⟹ P = Q"
  by (rel_auto robust, fastforce+)  
    
lemma wp_sp_sym:
  "`prog wp (true sp prog)`"
  by rel_auto
     
lemma it_is_pre_condition:"⦃C wp Q⦄C⦃Q⦄⇩u"
  by rel_blast    

lemma it_is_the_weakest_pre:"`P ⇒ C wp Q` = ⦃P⦄C⦃Q⦄⇩u"
  by rel_blast  

lemma s_pre:"`P ⇒ C wp Q`=⦃P⦄C⦃Q⦄⇩u"
  by rel_blast     

end