(******************************************************************************
 * 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_{SE_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_{SE_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_{SE_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_{SE_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_{SE_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_{SE_def} unit_SE_def call_{C_def}
  by simp

lemma if_funcall_skip:
"{λσ. exec_stop σ ∧ P σ}(p_tmp ← call_C fun E ; assign_local upd (λσ. p_tmp)) {λr σ. exec_stop σ ∧ P σ}"
  unfolding    hoare₃_def skip_{SE_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_tmp ← call_C fun E ; assign_global upd (λσ. p_tmp)) {λr σ. exec_stop σ ∧ P σ }"
  unfolding    hoare₃_def skip_{SE_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_{SE_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_{SE_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(rhs)
               {λr σ. P σ ∧ return_status σ }"
  unfolding return_{C_def} return_{C0_def} hoare₃_def skip_{SE_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
  a Hoare-logic for a language involving break. The first is, that break is not used
  the toplevel of a body of a loop (there might be breaks inside an inner loop, though).
  scheme is covered by the rule below, which is a generalisation of the classical
  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_SE (λσ. ▹ σ ∧ cond σ) do M od
          {λ_ σ. ¬ ( ▹ σ ∧ cond σ) ∧ ¬ break_status σ ∧ P σ}"
          (is "{?pre} while_SE ?cond' do M od {λ_ σ. ¬ ( ?cond' σ) ∧ ?post2 σ}")
      proof (rule consequence_unit) 
         fix σ show " ?pre σ ⟶ ?post2 σ"  using exec_stop1 by blast
      next
         show "{?post2}while_SE ?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_SE (λσ. ▹ σ ∧ 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