Theory Hoare_Clean

(******************************************************************************
 * 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.
 ******************************************************************************)

(*
 * A Hoare Calculus for Clean
 *
 * Author : Burkhart Wolff
 * 
 *)

theory Hoare_Clean
  imports Hoare_MonadSE
          Clean
begin


subsection‹Clean Control Rules›

lemma break1: 
  "⦃λσ.  P (σ ⦇ break_status := True ⦈) ⦄ break ⦃λr σ.  P σ ∧ break_status σ ⦄"
  unfolding    hoare⇩₃_def break_def unit_SE_def by auto

lemma unset_break1: 
  "⦃λσ.  P (σ ⦇ break_status := False ⦈) ⦄ unset_break_status ⦃λr σ. P σ ∧ ¬ break_status σ ⦄"
  unfolding    hoare⇩₃_def unset_break_status_def unit_SE_def by auto

lemma set_return1: 
  "⦃λσ.  P (σ ⦇ return_status := True ⦈) ⦄ set_return_status ⦃λr σ. P σ ∧ return_status σ ⦄"
  unfolding    hoare⇩₃_def set_return_status_def unit_SE_def by auto

lemma unset_return1: 
  "⦃λσ.  P (σ ⦇ return_status := False ⦈) ⦄ unset_return_status ⦃λr σ. P σ ∧ ¬return_status σ ⦄"
  unfolding    hoare⇩₃_def unset_return_status_def unit_SE_def by auto


subsection‹Clean Skip Rules›

lemma assign_global_skip:
"⦃λσ.   exec_stop σ ∧ P σ ⦄  upd :==⇩_G rhs  ⦃λr σ. exec_stop σ ∧ P σ ⦄"
  unfolding    hoare⇩₃_def skip⇩_S⇩_E_def unit_SE_def
  by (simp add: assign_def assign_global_def)

lemma assign_local_skip:
"⦃λσ.   exec_stop σ ∧ P σ ⦄ upd :==⇩_L rhs  ⦃λr σ. exec_stop σ ∧ P σ ⦄"
  unfolding    hoare⇩₃_def skip⇩_S⇩_E_def unit_SE_def
  by (simp add: assign_def assign_local_def)

lemma return_skip:
"⦃λσ.  exec_stop σ ∧ P σ ⦄ return⇩_C upd rhs ⦃λr σ. exec_stop σ ∧ P σ ⦄"
  unfolding hoare⇩₃_def return⇩_C_def return⇩_C0_def unit_SE_def assign_local_def assign_def
            bind_SE'_def bind_SE_def
  by auto

lemma assign_clean_skip:
"⦃λσ.   exec_stop σ ∧ P σ ⦄  assign tr  ⦃λr σ. exec_stop σ ∧ P σ ⦄"
  unfolding    hoare⇩₃_def skip⇩_S⇩_E_def unit_SE_def
  by (simp add: assign_def assign_def)

lemma if_clean_skip:
"⦃λσ.   exec_stop σ ∧ P σ ⦄  if⇩_C C then E else F fi ⦃λr σ. exec_stop σ ∧ P σ ⦄"
  unfolding    hoare⇩₃_def skip⇩_S⇩_E_def unit_SE_def if_SE_def
  by (simp add: if_C_def)

lemma while_clean_skip:
"⦃λσ.   exec_stop σ ∧ P σ ⦄  while⇩_C cond do body od  ⦃λr σ. exec_stop σ ∧ P σ ⦄"
  unfolding    hoare⇩₃_def skip⇩_S⇩_E_def unit_SE_def while_C_def 
  by auto

lemma if_opcall_skip:
"⦃λσ.   exec_stop σ ∧ P σ⦄ (call⇩_C M A⇩₁) ⦃λr σ. exec_stop σ ∧ P σ⦄"
  unfolding    hoare⇩₃_def skip⇩_S⇩_E_def unit_SE_def call⇩_C_def
  by simp

lemma if_funcall_skip:
"⦃λσ. exec_stop σ ∧ P σ⦄(p⇩_t⇩_m⇩_p ← call⇩_C fun E ; assign_local upd (λσ. p⇩_t⇩_m⇩_p)) ⦃λr σ. exec_stop σ ∧ P σ⦄"
  unfolding    hoare⇩₃_def skip⇩_S⇩_E_def unit_SE_def call⇩_C_def assign_local_def assign_def
  by (simp add: bind_SE_def)

lemma if_funcall_skip':
"⦃λσ. exec_stop σ ∧ P σ ⦄(p⇩_t⇩_m⇩_p ← call⇩_C fun E ; assign_global upd (λσ. p⇩_t⇩_m⇩_p)) ⦃λr σ. exec_stop σ ∧ P σ ⦄"
  unfolding    hoare⇩₃_def skip⇩_S⇩_E_def unit_SE_def call⇩_C_def assign_global_def assign_def
  by (simp add: bind_SE_def)




subsection‹Clean Assign Rules›


lemma assign_global:
  assumes * : "♯ upd"
  shows       "⦃λσ. ▹ σ ∧ P (upd (λ_. rhs σ) σ) ⦄ upd :==⇩_G rhs ⦃λr σ. ▹ σ ∧ P σ ⦄"
  unfolding    hoare⇩₃_def skip⇩_S⇩_E_def unit_SE_def assign_global_def  assign_def
  by(auto simp: assms)

find_theorems "♯ _ "

lemma assign_local:
  assumes * : "♯ (upd ∘ upd_hd)"
  shows       "⦃λσ. ▹ σ ∧ P ((upd ∘ upd_hd) (λ_. rhs σ) σ) ⦄ upd :==⇩_L rhs  ⦃λr σ. ▹ σ ∧ P σ ⦄"
  unfolding    hoare⇩₃_def skip⇩_S⇩_E_def unit_SE_def assign_local_def  assign_def
  using assms exec_stop_vs_control_independence by fastforce

lemma return_assign:
  assumes * : "♯ (upd ∘ upd_hd)"
  shows       "⦃λ σ. ▹ σ ∧ P ((upd ∘ upd_hd) (λ_. rhs σ) (σ ⦇ return_status := True ⦈))⦄ 
               return⇘upd⇙(rhs)
               ⦃λr σ. P σ ∧ return_status σ ⦄"
  unfolding return⇩_C_def return⇩_C0_def hoare⇩₃_def skip⇩_S⇩_E_def unit_SE_def assign_local_def assign_def 
            set_return_status_def bind_SE'_def bind_SE_def 
proof (auto)
  fix σ :: "'b control_state_scheme"
    assume a1: "P (upd (upd_hd (λ_. rhs σ)) (σ⦇return_status := True⦈))"
    assume "▹ σ"
    show "P (upd (upd_hd (λ_. rhs σ)) σ⦇return_status := True⦈)"
      using a1 assms exec_stop_vs_control_independence' by fastforce
qed
  (* do we need independence of rhs ? Not really. 'Normal' programs would never
     be control-state dependent, and 'artificial' ones would still be correct ...*)


subsection‹Clean Construct Rules›

lemma cond_clean : 
  "    ⦃λσ. ▹ σ ∧ P σ ∧ cond σ⦄ M ⦃Q⦄
   ⟹ ⦃λσ. ▹ σ ∧ P σ ∧ ¬ cond σ⦄ M' ⦃Q⦄  
   ⟹ ⦃λσ. ▹ σ ∧ P σ⦄ if⇩_C cond then M else M' fi⦃Q⦄"
  unfolding hoare⇩₃_def hoare⇩₃'_def bind_SE_def if_SE_def
  by (simp add: if_C_def)


text‹There is a particular difficulty with a verification of (terminating) while rules
in a Hoare-logic for a language involving break. The first is, that break is not used
in the toplevel of a body of a loop (there might be breaks inside an inner loop, though).
This scheme is covered by the rule below, which is a generalisation of the classical 
while loop (as presented by @{thm while}.›


lemma while_clean_no_break :
  assumes  * : "⦃λσ. ¬ break_status σ ∧ cond σ ∧ P σ⦄  M ⦃λ_. λσ.  ¬ break_status σ ∧ P σ ⦄"
  and measure: "∀σ. ¬ exec_stop σ ∧ cond σ ∧ P σ 
                    ⟶ M σ ≠ None ∧ f(snd(the(M σ))) < ((f σ)::nat) "
               (is "∀σ. _ ∧ cond σ ∧ P σ ⟶ ?decrease σ")
  shows        "⦃λσ. ▹ σ ∧ P σ⦄ 
                while⇩_C cond do M od 
                ⦃λ_ σ. (return_status σ ∨ ¬ cond σ) ∧ ¬ break_status σ ∧ P σ⦄"
                (is "⦃?pre⦄ while⇩_C cond do M od ⦃λ_ σ. ?post1 σ ∧ ?post2 σ⦄")  
  unfolding while_C_def hoare⇩₃_def hoare⇩₃'_def
  proof (simp add: hoare⇩₃_def[symmetric],rule sequence') 
    show "⦃?pre⦄ 
          while⇩_S⇩_E (λσ.  ▹ σ ∧ cond σ) do M od
          ⦃λ_ σ. ¬ ( ▹  σ ∧ cond σ) ∧ ¬ break_status σ ∧ P σ⦄"
          (is "⦃?pre⦄ while⇩_S⇩_E ?cond' do M od ⦃λ_ σ. ¬ ( ?cond' σ) ∧ ?post2 σ⦄")
      proof (rule consequence_unit) 
         fix σ show " ?pre σ ⟶ ?post2 σ"  using exec_stop1 by blast
      next
         show "⦃?post2⦄while⇩_S⇩_E ?cond' do M od⦃λx σ. ¬(?cond' σ) ∧ ?post2 σ⦄"
         proof (rule_tac f = "f" in while, rule consequence_unit)
           fix σ show "?cond' σ ∧ ?post2 σ ⟶ ¬break_status σ ∧ cond σ ∧ P σ" by simp
         next
           show "⦃λσ. ¬ break_status σ ∧ cond σ ∧ P σ⦄ M ⦃λx σ. ?post2 σ⦄" using "*" by blast
         next 
           fix σ  show "?post2 σ ⟶ ?post2 σ" by blast
         next 
           show "∀σ.?cond' σ ∧ ?post2 σ ⟶ ?decrease σ" using measure by blast
         qed
      next
         fix σ show " ¬?cond' σ ∧ ?post2 σ ⟶ ¬?cond' σ ∧ ?post2 σ"  by blast
      qed
  next
    show "⦃λσ. ¬ (▹ σ ∧ cond σ) ∧ ?post2 σ⦄ unset_break_status
          ⦃λ_ σ'. (return_status σ' ∨ ¬ cond σ') ∧ ?post2 σ'⦄"
         (is "⦃λσ. ¬ (?cond'' σ) ∧ ?post2 σ⦄ unset_break_status ⦃λ_ σ'. ?post3 σ' ∧ ?post2 σ' ⦄")
      proof (rule consequence_unit) 
        fix σ  
        show "¬ ?cond'' σ ∧ ?post2 σ ⟶ (λσ. P σ ∧ ?post3 σ) (σ⦇break_status := False⦈)"
              by (metis (full_types) exec_stop_def surjective update_convs(1))
      next
        show "⦃λσ. (λσ. P σ ∧ ?post3 σ) (σ⦇break_status := False⦈)⦄
              unset_break_status 
              ⦃λx σ. ?post3 σ ∧ ¬ break_status σ ∧ P σ⦄"    
             apply(subst (2) conj_commute,subst conj_assoc,subst (2) conj_commute)
             by(rule unset_break1)
      next 
         fix σ show  "?post3 σ ∧ ?post2 σ ⟶ ?post3 σ ∧ ?post2 σ"  by simp
      qed
qed 


text‹In the following we present a version allowing a break inside the body, which implies that the 
     invariant has been established at the break-point and the condition is irrelevant. 
     A return may occur, but the @{term "break_status"} is guaranteed to be true
     after leaving the loop.›



lemma while_clean':
  assumes  M_inv   : "⦃λσ. ▹ σ ∧ cond σ ∧ P σ⦄  M ⦃λ_. P⦄"
  and cond_idpc    : "∀x σ.  (cond (σ⦇break_status := x⦈)) = cond σ "
  and inv_idpc     : "∀x σ.  (P (σ⦇break_status := x⦈)) = P σ "
  and f_is_measure : "∀σ. ▹ σ ∧ cond σ ∧ P σ ⟶  M σ ≠ None ∧ f(snd(the(M σ))) < ((f σ)::nat)"
shows    "⦃λσ. ▹ σ ∧ P σ⦄  while⇩_C cond do M od  ⦃λ_ σ.  ¬ break_status σ ∧ P σ⦄"
  unfolding while_C_def hoare⇩₃_def hoare⇩₃'_def
  proof (simp add: hoare⇩₃_def[symmetric], rule sequence')
    show "⦃λσ. ▹ σ ∧ P σ⦄ 
            while⇩_S⇩_E (λσ. ▹ σ ∧ cond σ) do M od
          ⦃λ_ σ. P (σ⦇break_status := False⦈)⦄"
          apply(rule consequence_unit, rule impI, erule conjunct2)
          apply(rule_tac f = "f" in while)
          using M_inv f_is_measure inv_idpc by auto
  next
    show "⦃λσ. P (σ⦇break_status := False⦈)⦄ unset_break_status 
          ⦃λx σ. ¬ break_status σ ∧ P σ⦄"
          apply(subst conj_commute)
          by(rule  Hoare_Clean.unset_break1)
  qed


text‹Consequence and Sequence rules where inherited from the underlying Hoare-Monad theory.›


end