Theory Hoare_MonadSE

(******************************************************************************
 * Clean
 *
 * Copyright (c) 2018-2019 Université Paris-Saclay, Univ. Paris-Sud, France
 *
 * All rights reserved.
 *
 * Redistribution and use in source and binary forms, with or without
 * modification, are permitted provided that the following conditions are
 * met:
 *
 *     * Redistributions of source code must retain the above copyright
 *       notice, this list of conditions and the following disclaimer.
 *
 *     * Redistributions in binary form must reproduce the above
 *       copyright notice, this list of conditions and the following
 *       disclaimer in the documentation and/or other materials provided
 *       with the distribution.
 *
 *     * Neither the name of the copyright holders nor the names of its
 *       contributors may be used to endorse or promote products derived
 *       from this software without specific prior written permission.
 *
 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
 * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
 * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
 * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
 * OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
 * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
 * LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
 * DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
 * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
 * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
 * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 ******************************************************************************)

(*
 * Basic Hoare Calculus for the State Exception Monad 
 *
 * Authors : Burkhart Wolff
 *)

theory Hoare_MonadSE
  imports Symbex_MonadSE
begin
  


section‹Hoare›


definition hoare⇩₃ :: "('σ ⇒ bool) ⇒ ('α, 'σ)MON⇩_S⇩_E ⇒ ('α ⇒ 'σ ⇒ bool) ⇒ bool" (‹(⦃(1_)⦄/ (_)/ ⦃(1_)⦄)› 50)
where   "⦃P⦄ M ⦃Q⦄ ≡ (∀σ. P σ ⟶ (case M σ of None => False | Some(x, σ') => Q x σ'))" 

definition hoare⇩₃' :: "('σ ⇒ bool) ⇒ ('α, 'σ)MON⇩_S⇩_E ⇒ bool" (‹(⦃(1_)⦄/ (_)/†)› 50)
where   "⦃P⦄ M † ≡ (∀σ. P σ ⟶ (case M σ of None => True | _ => False))" 

subsection‹Basic rules› 
  
lemma skip: " ⦃P⦄ skip⇩_S⇩_E ⦃λ_. P⦄"
  unfolding hoare⇩₃_def skip⇩_S⇩_E_def unit_SE_def
  by auto
    
lemma fail: "⦃P⦄ fail⇩_S⇩_E †"
  unfolding hoare⇩₃'_def fail_SE_def unit_SE_def by auto

lemma assert: "⦃P⦄ assert⇩_S⇩_E P ⦃λ _ _. True⦄"    
  unfolding hoare⇩₃_def assert_SE_def unit_SE_def
  by auto

lemma assert_conseq: "Collect P ⊆ Collect Q ⟹ ⦃P⦄ assert⇩_S⇩_E Q ⦃λ _ _. True⦄"    
  unfolding hoare⇩₃_def assert_SE_def unit_SE_def
  by auto

lemma assume_conseq: 
  assumes "∃ σ. Q σ"
  shows   "⦃P⦄ assume⇩_S⇩_E Q ⦃λ _ . Q⦄"    
  unfolding hoare⇩₃_def assume_SE_def unit_SE_def
  apply (auto simp : someI2)
  using assms by auto

    
text ‹assignment missing in the calculus because this is viewed as a state specific  
       operation, definable for concrete instances of @{typ "'σ"}.›  

subsection ‹Generalized and special sequence rules› 
text‹The decisive idea is to factor out the post-condition on the results of @{term M} :›
lemma sequence : 
  "    ⦃P⦄ M ⦃λx σ. x∈A ∧ Q x σ⦄
   ⟹ ∀x∈A. ⦃Q x⦄ M' x ⦃R⦄ 
   ⟹ ⦃P⦄ x ← M; M' x ⦃R⦄" 
  unfolding hoare⇩₃_def bind_SE_def 
  by(auto,erule_tac x="σ" in allE, auto split: Option.option.split_asm Option.option.split)

lemma sequence_irpt_l : "⦃P⦄ M †  ⟹ ⦃P⦄ x ← M; M' x †" 
  unfolding hoare⇩₃'_def bind_SE_def 
  by(auto,erule_tac x="σ" in allE, auto split: Option.option.split_asm Option.option.split)

lemma sequence_irpt_r : "⦃P⦄ M ⦃λx σ. x∈A ∧ Q x σ⦄ ⟹ ∀x∈A. ⦃Q x⦄ M' x †  ⟹ ⦃P⦄ x ← M; M' x †" 
  unfolding hoare⇩₃'_def hoare⇩₃_def bind_SE_def 
  by(auto,erule_tac x="σ" in allE, auto split: Option.option.split_asm Option.option.split)
        
lemma sequence' : "⦃P⦄ M ⦃λ_. Q ⦄ ⟹ ⦃Q⦄ M' ⦃R⦄ ⟹ ⦃P⦄ M;- M' ⦃R⦄"     
  unfolding hoare⇩₃_def hoare⇩₃_def bind_SE_def bind_SE'_def
  by(auto,erule_tac x="σ" in allE, auto split: Option.option.split_asm Option.option.split)

lemma sequence_irpt_l' : "⦃P⦄ M † ⟹ ⦃P⦄ M;- M' †" 
  unfolding hoare⇩₃'_def bind_SE_def bind_SE'_def
  by(auto,erule_tac x="σ" in allE, auto split: Option.option.split_asm Option.option.split)
    
lemma sequence_irpt_r' : "⦃P⦄ M ⦃λ_. Q ⦄ ⟹ ⦃Q⦄ M' † ⟹ ⦃P⦄ M;- M' †" 
  unfolding hoare⇩₃'_def hoare⇩₃_def bind_SE_def bind_SE'_def
  by(auto,erule_tac x="σ" in allE, auto split: Option.option.split_asm Option.option.split)

subsection‹Generalized and special consequence rules›  
lemma consequence : 
  "    Collect P ⊆ Collect P'
   ⟹ ⦃P'⦄ M ⦃λx σ. x∈A ∧ Q' x σ⦄ 
   ⟹ ∀ x∈A. Collect(Q' x) ⊆ Collect (Q x)
   ⟹ ⦃P⦄ M ⦃λx σ. x∈A ∧ Q x σ⦄"
  unfolding hoare⇩₃_def bind_SE_def 
  by(auto,erule_tac x="σ" in allE,auto split: Option.option.split_asm Option.option.split)

lemma consequence_unit : 
  assumes "(⋀ σ. P σ ⟶ P' σ)" 
   and  "⦃P'⦄ M ⦃λx::unit. λ σ.  Q' σ⦄" 
   and  " (⋀ σ. Q'  σ ⟶ Q  σ)" 
   shows "⦃P⦄ M ⦃λx σ. Q σ⦄"
proof -
  have * : "(λx σ. Q  σ) = (λx::unit. λ σ. x∈UNIV ∧ Q  σ) " by auto
  show ?thesis
    apply(subst *)
    apply(rule_tac  P' = "P'" and Q' = "%_. Q'" in consequence)
    apply (simp add: Collect_mono assms(1))
    using assms(2) apply auto[1]
    by (simp add: Collect_mono assms(3))
qed


lemma consequence_irpt : 
  "    Collect P ⊆ Collect P'
   ⟹ ⦃P'⦄ M †
   ⟹ ⦃P⦄  M †"
  unfolding hoare⇩₃_def hoare⇩₃'_def bind_SE_def  
  by(auto)

lemma consequence_mt_swap : 
  "(⦃λ_. False⦄ M †) = (⦃λ_. False⦄ M ⦃P⦄)" 
  unfolding hoare⇩₃_def hoare⇩₃'_def bind_SE_def 
  by auto
    
subsection‹Condition rules› 
  
lemma cond : 
  "    ⦃λσ. P σ ∧ cond σ⦄ M ⦃Q⦄
   ⟹ ⦃λσ. P σ ∧ ¬ cond σ⦄ M' ⦃Q⦄  
   ⟹ ⦃P⦄if⇩_S⇩_E cond then M else M' fi⦃Q⦄"
  unfolding hoare⇩₃_def hoare⇩₃'_def bind_SE_def if_SE_def
  by auto
  
lemma cond_irpt : 
  "    ⦃λσ. P σ ∧ cond σ⦄ M †
   ⟹ ⦃λσ. P σ ∧ ¬ cond σ⦄ M' †  
   ⟹ ⦃P⦄if⇩_S⇩_E cond then M else M' fi †"
  unfolding hoare⇩₃_def hoare⇩₃'_def bind_SE_def if_SE_def
  by auto

text‹ Note that the other four combinations can be directly derived via
       the @{thm consequence_mt_swap} rule.›
  
subsection‹While rules› 
text‹The only non-trivial proof is, of course, the while loop rule. Note
that non-terminating loops were mapped to @{term None} following the principle
that our monadic state-transformers represent partial functions in the mathematical 
sense.›
  
lemma while :
  assumes  * : "⦃λσ. cond σ ∧ P σ⦄  M ⦃λ_. P⦄"
  and measure: "∀σ. cond σ ∧ P σ ⟶ M σ ≠ None ∧ f(snd(the(M σ))) < ((f σ)::nat) "
  shows        "⦃P⦄while⇩_S⇩_E cond do M od ⦃λ_ σ. ¬cond σ ∧ P σ⦄"

unfolding hoare⇩₃_def hoare⇩₃'_def bind_SE_def if_SE_def
proof auto
  have * : "∀n. ∀ σ. P σ ∧ f σ ≤ n ⟶  
                     (case (while⇩_S⇩_E cond do M od) σ of 
                          None ⇒ False
                        | Some (x, σ') ⇒ ¬ cond σ' ∧ P σ')" (is "∀n. ?P n")
     proof (rule allI, rename_tac n, induct_tac n)
       fix n show "?P 0"
         apply(auto)
         apply(subst while_SE_unfold)
         by (metis (no_types, lifting) gr_implies_not0 if_SE_def  measure option.case_eq_if 
                     option.sel option.simps(3) prod.sel(2) split_def unit_SE_def)
     next
       fix n  show " ?P n ⟹ ?P (Suc n)"
        apply(auto,subst while_SE_unfold)
         apply(case_tac "¬cond σ")
        apply (simp add: if_SE_def unit_SE_def)
        apply(simp add: if_SE_def)
        apply(case_tac "M σ = None")
         using measure apply blast
        proof (auto simp: bind_SE'_def bind_SE_def)
          fix σ σ'
          assume 1 : "cond σ"
            and  2 : "M σ = Some ((), σ')"
            and  3 : " P σ"
            and  4 : " f σ ≤ Suc n"
            and  hyp : "?P n"
          have 5 : "P σ'" 
            by (metis (no_types, lifting) * 1 2 3 case_prodD hoare⇩₃_def option.simps(5))
          have 6 : "snd(the(M σ)) = σ'" 
            by (simp add: 2)
          have 7 : "cond σ' ⟹ f σ' ≤ n" 
            using 1 3 4 6 leD measure by auto
          show   "case (while⇩_S⇩_E cond do M od) σ' of None ⇒ False
                                                  | Some (xa, σ') ⇒ ¬ cond σ' ∧ P σ'"
          using 1 3 4 5 6 hyp measure by auto
        qed
      qed
  show "⋀σ. P σ ⟹
         case (while⇩_S⇩_E cond do M od) σ of None ⇒ False
         | Some (x, σ') ⇒ ¬ cond σ' ∧ P σ'"
  using "*" by blast
qed
  

lemma while_irpt :
  assumes  * : "⦃λσ. cond σ ∧ P σ⦄  M ⦃λ_. P⦄ ∨ ⦃λσ. cond σ ∧ P σ⦄  M  †"
  and measure: "∀σ. cond σ ∧ P σ ⟶ M σ = None ∨ f(snd(the(M σ))) < ((f σ)::nat)"
  and enabled: "∀σ. P σ ⟶ cond σ"
  shows        "⦃P⦄while⇩_S⇩_E cond do M od †"
unfolding hoare⇩₃_def hoare⇩₃'_def bind_SE_def if_SE_def
proof auto
  have * : "∀n. ∀ σ. P σ ∧ f σ ≤ n ⟶  
                     (case (while⇩_S⇩_E cond do M od) σ of None ⇒ True | Some a ⇒ False)" 
            (is "∀n. ?P n ")
    proof (rule allI, rename_tac n, induct_tac n)
      fix n 
         have 1 : "⋀σ. P σ ⟹ cond σ" 
          by (simp add: enabled * )
      show "?P 0 "
        apply(auto,frule 1)
        by (metis assms(2) bind_SE'_def bind_SE_def gr_implies_not0 if_SE_def option.case(1) 
                           option.case_eq_if  while_SE_unfold)
    next
      fix k n 
      assume hyp : "?P n"
         have 1 : "⋀σ. P σ ⟹ cond σ" 
          by (simp add: enabled * )
      show "?P (Suc n) "
        apply(auto, frule 1)
        apply(subst while_SE_unfold, auto simp: if_SE_def)
      proof(insert *,simp_all add: hoare⇩₃_def hoare⇩₃'_def, erule disjE)
        fix σ
        assume "P σ"
         and   "f σ ≤ Suc n"
         and   "cond σ"
         and   ** : "∀σ. cond σ ∧ P σ ⟶ (case M σ of None ⇒ False | Some (x, σ') ⇒ P σ')"
         obtain "(case M σ of None ⇒ False | Some (x, σ') ⇒ P σ')" 
               by (simp add: "**" ‹P σ› ‹cond σ›)
        then 
        show "case (M ;- (while⇩_S⇩_E cond do M od)) σ of None ⇒ True | Some a ⇒ False"
             apply(case_tac "M σ", auto, rename_tac σ', simp add: bind_SE'_def bind_SE_def)
             proof - 
               fix σ' 
               assume "P σ'"
                and "M σ = Some ((), σ')"
                have "cond σ'"  by (simp add: ‹P σ'› enabled)
                have "f σ' ≤ n" 
                  using ‹M σ = Some ((), σ')› ‹P σ› ‹cond σ› ‹f σ ≤ Suc n› measure by fastforce   
               show "case (while⇩_S⇩_E cond do M od) σ' of None ⇒ True | Some a ⇒ False"
                  using hyp  by (simp add: ‹P σ'› ‹f σ' ≤ n›)
              qed
      next
        fix σ
        assume "P σ"
         and   "f σ ≤ Suc n"
         and   "cond σ"  
         and * : "∀σ. cond σ ∧ P σ ⟶ (case M σ of None ⇒ True | Some a ⇒ False)"
        obtain ** : "(case M σ of None ⇒ True | Some a ⇒ False)" 
          by (simp add: "*" ‹P σ› ‹cond σ›)
        have "M σ = None" 
          by (simp add: "**" option.disc_eq_case(1))
        show "case (M ;- (while⇩_S⇩_E cond do M od)) σ of None ⇒ True | Some a ⇒ False"          
          by (simp add: ‹M σ = None› bind_SE'_def bind_SE_def)
      qed      
    qed
show "⋀σ. P σ ⟹ case (while⇩_S⇩_E cond do M od) σ of None ⇒ True | Some a ⇒ False" using * by blast
qed
  

subsection‹Experimental Alternative Definitions (Transformer-Style Rely-Guarantee)›

definition  hoare⇩₁ :: "('σ ⇒ bool) ⇒ ('α, 'σ)MON⇩_S⇩_E ⇒ ('α ⇒ 'σ ⇒ bool) ⇒ bool" (‹⊢⇩₁ ({(1_)}/ (_)/ {(1_)})› 50)
where  "(⊢⇩₁{P} M {Q} ) = (∀σ. (σ ⊨ (_  ← assume⇩_S⇩_E P ; x  ← M; assert⇩_S⇩_E (Q x))))"

(* Problem: Severe Deviation for the case of an unsatisfyable precondition *)

definition  hoare⇩₂ :: "('σ ⇒ bool) ⇒ ('α, 'σ)MON⇩_S⇩_E ⇒ ('α ⇒ 'σ ⇒ bool) ⇒ bool" (‹⊢⇩₂ ({(1_)}/ (_)/ {(1_)})› 50)
where  "(⊢⇩₂{P} M {Q} ) = (∀σ. P σ ⟶ (σ ⊨  (x ← M; assert⇩_S⇩_E (Q x))))"

  
end