(*************************************************************************************************)
(* 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 ) = (\<exists>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_\<bottom> 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