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    hoare3_def break_def unit_SE_def by auto

lemma unset_break1: 
  "λσ.  P (σ  break_status := False )  unset_break_status λr σ. P σ  ¬ break_status σ "
  unfolding    hoare3_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    hoare3_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    hoare3_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    hoare3_def skipSE_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    hoare3_def skipSE_def unit_SE_def
  by (simp add: assign_def assign_local_def)

lemma return_skip:
"λσ.  exec_stop σ  P σ  returnC upd rhs λr σ. exec_stop σ  P σ "
  unfolding hoare3_def returnC_def returnC0_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    hoare3_def skipSE_def unit_SE_def
  by (simp add: assign_def assign_def)

lemma if_clean_skip:
"λσ.   exec_stop σ  P σ   ifC C then E else F fi λr σ. exec_stop σ  P σ "
  unfolding    hoare3_def skipSE_def unit_SE_def if_SE_def
  by (simp add: if_C_def)

lemma while_clean_skip:
"λσ.   exec_stop σ  P σ   whileC cond do body od  λr σ. exec_stop σ  P σ "
  unfolding    hoare3_def skipSE_def unit_SE_def while_C_def 
  by auto

lemma if_opcall_skip:
"λσ.   exec_stop σ  P σ (callC M A1) λr σ. exec_stop σ  P σ"
  unfolding    hoare3_def skipSE_def unit_SE_def callC_def
  by simp

lemma if_funcall_skip:
"λσ. exec_stop σ  P σ(ptmp  callC fun E ; assign_local upd (λσ. ptmp)) λr σ. exec_stop σ  P σ"
  unfolding    hoare3_def skipSE_def unit_SE_def callC_def assign_local_def assign_def
  by (simp add: bind_SE_def)

lemma if_funcall_skip':
"λσ. exec_stop σ  P σ (ptmp  callC fun E ; assign_global upd (λσ. ptmp)) λr σ. exec_stop σ  P σ "
  unfolding    hoare3_def skipSE_def unit_SE_def callC_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    hoare3_def skipSE_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    hoare3_def skipSE_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 )) 
               returnupd(rhs)
               λr σ. P σ  return_status σ "
  unfolding returnC_def returnC0_def hoare3_def skipSE_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 σ ifC cond then M else M' fiQ"
  unfolding hoare3_def hoare3'_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 σ 
                whileC cond do M od 
                λ_ σ. (return_status σ  ¬ cond σ)  ¬ break_status σ  P σ"
                (is "?pre whileC cond do M od λ_ σ. ?post1 σ  ?post2 σ")  
  unfolding while_C_def hoare3_def hoare3'_def
  proof (simp add: hoare3_def[symmetric],rule sequence') 
    show "?pre 
          whileSE (λσ.   σ  cond σ) do M od
          λ_ σ. ¬ (   σ  cond σ)  ¬ break_status σ  P σ"
          (is "?pre whileSE ?cond' do M od λ_ σ. ¬ ( ?cond' σ)  ?post2 σ")
      proof (rule consequence_unit) 
         fix σ show " ?pre σ  ?post2 σ"  using exec_stop1 by blast
      next
         show "?post2whileSE ?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 σ  whileC cond do M od  λ_ σ.  ¬ break_status σ  P σ"
  unfolding while_C_def hoare3_def hoare3'_def
  proof (simp add: hoare3_def[symmetric], rule sequence')
    show "λσ.  σ  P σ 
            whileSE (λσ.  σ  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