Theory Patch

(*<*)
―‹ ********************************************************************
 * Project         : HOL-CSPM - Architectural operators for HOL-CSP
 *
 * Author          : Benoît Ballenghien, Safouan Taha, Burkhart Wolff
 *
 * This file       : Patch
 *
 * Copyright (c) 2023 Université Paris-Saclay, 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.
 ******************************************************************************›
(*>*)

chapter ‹Patch for Compatibility›
theory Patch
  imports "HOL-CSP.Assertions"
begin


text ‹\<^session>‹HOL-CSP› significantly changed during the past months, but not all
      the modifications appear in the current version on the AFP.
      This theory fixes the incompatibilities and will be removed in the next release.›


section ‹Results›

―‹This one is very easy›
lemma Mprefix_Det_distr:
  ‹(□ a ∈ A → P a) □ (□ b ∈ B → Q b) = 
   □ x ∈ A ∪ B → (  if x ∈ A ∩ B then P x ⊓ Q x 
                    else if x ∈ A then P x else Q x)›
  (is ‹?lhs = ?rhs›)
proof (subst Process_eq_spec, safe)
  show ‹(s, X) ∈ ℱ ?lhs ⟹ (s, X) ∈ ℱ ?rhs› for s X
    by (simp add: F_Det F_Mprefix F_Ndet disjoint_iff, safe, auto)
next
  show ‹(s, X) ∈ ℱ ?rhs ⟹ (s, X) ∈ ℱ ?lhs› for s X
    by (auto simp add: F_Mprefix F_Ndet F_Det split: if_split_asm)
next
  show ‹s ∈ 𝒟 ?lhs ⟹ s ∈ 𝒟 ?rhs› for s
    by (simp add: D_Det D_Mprefix D_Ndet, safe, auto)
next
  show ‹s ∈ 𝒟 ?rhs ⟹ s ∈ 𝒟 ?lhs› for s
    by (auto simp add: D_Mprefix D_Ndet D_Det split: if_split_asm)
qed 

lemma D_expand : 
  ‹𝒟 P = {t1 @ t2| t1 t2. t1 ∈ 𝒟 P ∧ tickFree t1 ∧ front_tickFree t2}›
  (is ‹𝒟 P = ?rhs›)
proof (intro subset_antisym subsetI)
  show ‹s ∈ 𝒟 P ⟹ s ∈ ?rhs› for s
    apply (simp, cases ‹tickFree s›)
     apply (rule_tac x = s in exI, rule_tac x = ‹[]› in exI, simp)
    apply (rule_tac x = ‹butlast s› in exI, rule_tac x = ‹[tick]› in exI, simp)
    by (metis front_tickFree_implies_tickFree nonTickFree_n_frontTickFree
              process_charn snoc_eq_iff_butlast)
next
  show ‹s ∈ ?rhs ⟹ s ∈ 𝒟 P› for s
    using is_processT7 by blast
qed



subsection‹Continuity Rule›

subsubsection ‹Monotonicity of \<^const>‹Renaming›.›

lemma mono_Renaming[simp] : ‹(Renaming P f) ⊑ (Renaming Q f)› if ‹P ⊑ Q›
proof (unfold le_approx_def, intro conjI subset_antisym subsetI allI impI)
  show ‹s ∈ 𝒟 (Renaming Q f) ⟹ s ∈ 𝒟 (Renaming P f)› for s
    using that[THEN le_approx1] by (auto simp add: D_Renaming)
next
  show ‹s ∉ 𝒟 (Renaming P f) ⟹ 
        X ∈ ℛ⇩a (Renaming P f) s ⟹ X ∈ ℛ⇩a (Renaming Q f) s› for s X
    using that[THEN le_approx2] apply (simp add: Ra_def D_Renaming F_Renaming)
    by (metis (no_types, opaque_lifting)  append.right_neutral butlast.simps(2) 
              front_tickFree_butlast front_tickFree_mono list.distinct(1) 
              map_EvExt_tick map_append nonTickFree_n_frontTickFree process_charn)
next
  show ‹s ∉ 𝒟 (Renaming P f) ⟹
        X ∈ ℛ⇩a (Renaming Q f) s ⟹ X ∈ ℛ⇩a (Renaming P f) s› for s X
    using that[THEN le_approx2] that[THEN le_approx1]
    by (simp add: Ra_def D_Renaming F_Renaming subset_iff)
       (metis is_processT8_S)
next
  fix s
  assume * : ‹s ∈ min_elems (𝒟 (Renaming P f))›
  from elem_min_elems[OF "*"] obtain s1 s2
    where ** : ‹tickFree s1› ‹front_tickFree s2›
               ‹s = map (EvExt f) s1 @ s2› ‹s1 ∈ 𝒟 P›
               ‹front_tickFree s›
    using D_imp_front_tickFree D_Renaming by blast
  with min_elems_no[OF "*", of ‹butlast s›] have ‹s2 = []›
    by (cases s rule: rev_cases; simp add: D_Renaming)
       (metis butlast_append butlast_snoc front_tickFree_butlast less_self 
              nless_le tickFree_implies_front_tickFree)
  with "**" min_elems_no[OF "*", of ‹butlast s›] have ‹s1 ∈ min_elems (𝒟 P)›
    apply (cases s; simp add: D_Renaming Nil_min_elems)
    by (metis (no_types, lifting) D_imp_front_tickFree append.right_neutral butlast_snoc
                                  front_tickFree_charn less_self list.discI
                                  list.map_disc_iff map_butlast min_elems1 nless_le)
  hence ‹s1 ∈ 𝒯 Q› using that[THEN le_approx3] by blast
  show ‹s ∈ 𝒯 (Renaming Q f)›
    apply (simp add: "**"(3) ‹s2 = []› T_Renaming)
    using ‹s1 ∈ 𝒯 Q› by blast
qed




subsubsection ‹Useful Results about \<^const>‹finitary›, and Preliminaries Lemmas for Continuity.›


lemma le_snoc_is : ‹t ≤ s @ [x] ⟷ t = s @ [x] ∨ t ≤ s›
  by (metis append_eq_first_pref_spec le_list_def order.trans self_append_conv)

lemma Cont_RenH5: ‹finite (⋃t ∈ {t. t ≤ (s :: 'α trace)}. {s. t=map (EvExt f) s})› if ‹finitary f›
  apply (rule finite_UN_I)
   apply (induct s rule: rev_induct)
    apply (simp; fail)
   apply (simp add: le_snoc_is; fail)
  using Cont_RenH2 Cont_RenH4 that by blast


lemma Cont_RenH7:
  ‹finite {t. ∃t2. tickFree t ∧ front_tickFree t2 ∧ s = map (EvExt f) t @ t2}›
  if ‹finitary f›
proof -
  have f1: ‹{y. map (EvExt f) y ≤ s} =
            (⋃z ∈ {z. z ≤ s}. {y. z = map (EvExt f) y})› by fast
  show ?thesis
    apply (rule finite_subset[OF Cont_RenH6])
    apply (simp add: f1)
    apply (rule finite_UN_I)
     apply (induct s rule: rev_induct)
      apply (simp; fail)
     apply (simp add: le_snoc_is; fail)
    using Cont_RenH2 Cont_RenH4 that by blast
qed


subsubsection ‹Finally, Continuity !›

lemma Cont_Renaming_prem:
  ‹(⨆ i. Renaming (Y i) f) = (Renaming (⨆ i. Y i) f)› if finitary: ‹finitary f› 
   and chain: ‹chain Y›
proof (subst Process_eq_spec, safe)
  fix s
  define S where ‹S i ≡ {s1. ∃t2. tickFree s1 ∧ front_tickFree t2 ∧
                                   s = map (EvExt f) s1 @ t2 ∧ s1 ∈ 𝒟 (Y i)}› for i
  assume ‹s ∈ 𝒟 (⨆i. Renaming (Y i) f)›
  hence ‹s ∈ 𝒟 (Renaming (Y i) f)› for i
    by (simp add: limproc_is_thelub chain chain_Renaming D_LUB)

  hence ‹∀i. S i ≠ {}› by (simp add: S_def D_Renaming) blast
  moreover have ‹finite (S 0)›
    unfolding S_def 
    by (rule finite_subset[OF _ Cont_RenH7[OF finitary, of s]], blast)
  moreover have ‹∀i. S (Suc i) ⊆ S i›
    unfolding S_def using NF_ND po_class.chainE[OF chain]
                          proc_ord2a le_approx_def by blast
  ultimately have ‹(⋂i. S i) ≠ {}›
    by (rule Inter_nonempty_finite_chained_sets)    
  
  thus ‹s ∈ 𝒟 (Renaming (Lub Y) f)›
    by (simp add: limproc_is_thelub chain D_Renaming
                  D_LUB ex_in_conv[symmetric] S_def) blast
next
  show ‹s ∈ 𝒟 (Renaming (Lub Y) f) ⟹ s ∈ 𝒟 (⨆i. Renaming (Y i) f)› for s
    by (auto simp add: limproc_is_thelub chain chain_Renaming D_Renaming D_LUB)
next
  fix s X
  define S where ‹S i ≡ {s1. (s1, EvExt f -` X) ∈ ℱ (Y i) ∧ s = map (EvExt f) s1} ∪
                         {s1. ∃t2. tickFree s1 ∧ front_tickFree t2 ∧ 
                                   s = map (EvExt f) s1 @ t2 ∧ s1 ∈ 𝒟 (Y i)}› for i
  assume ‹(s, X) ∈ ℱ (⨆i. Renaming (Y i) f)›
  hence ‹(s, X) ∈ ℱ (Renaming (Y i) f)› for i
    by (simp add: limproc_is_thelub chain_Renaming[OF chain] F_LUB)

  hence ‹∀i. S i ≠ {}› by (auto simp add: S_def F_Renaming)
  moreover have ‹finite (S 0)›
    unfolding S_def
    apply (subst finite_Un, intro conjI)
     apply (rule finite_subset[of _ ‹{s1. s = map (EvExt f) s1}›], blast)
     apply (insert Cont_RenH2 Cont_RenH4 finitary, blast)
    by (rule finite_subset[OF _ Cont_RenH7[OF finitary, of s]], blast)
  moreover have ‹∀i. S (Suc i) ⊆ S i›
    unfolding S_def using NF_ND po_class.chainE[OF chain]
                          proc_ord2a le_approx_def by safe blast+
  ultimately have ‹(⋂i. S i) ≠ {}›
    by (rule Inter_nonempty_finite_chained_sets)
   
  thus ‹(s, X) ∈ ℱ (Renaming (Lub Y) f)›
    by (simp add: F_Renaming limproc_is_thelub chain D_LUB 
                  F_LUB ex_in_conv[symmetric] S_def) (meson NF_ND)
next
  show ‹(s, X) ∈ ℱ (Renaming (Lub Y) f) ⟹ (s, X) ∈ ℱ (⨆i. Renaming (Y i) f)› for s X
    by (auto simp add: limproc_is_thelub chain chain_Renaming F_Renaming D_LUB F_LUB)  
qed


subsection ‹Nice Properties›


lemma Renaming_inv: ‹Renaming (Renaming P f) (inv f) = P› if ‹inj f›
  apply (subst Renaming_comp[symmetric])
  apply (subst inv_o_cancel[OF that])
  by (fact Renaming_id) 


subsection ‹Renaming Laws›


lemma Renaming_Mprefix_inj_on:
  ‹Renaming (Mprefix A P) f = □ b ∈ f ` A → Renaming (P (THE a. a ∈ A ∧ f a = b)) f› 
  if inj_on_f: ‹inj_on f A›
  apply (subst Renaming_Mprefix[symmetric])
  apply (intro arg_cong[where f = ‹λQ. Renaming Q f›] mono_Mprefix_eq)
  by (metis that the_inv_into_def the_inv_into_f_f)


corollary Renaming_Mprefix_inj:
  ‹Renaming (Mprefix A P) f = □ b ∈ f ` A → Renaming (P (THE a. f a = b)) f› if inj_f: ‹inj f›
  apply (subst Renaming_Mprefix_inj_on, metis inj_eq inj_onI that)
  apply (rule mono_Mprefix_eq[rule_format])
  by (metis imageE inj_eq[OF inj_f])



(* TODO: write corollaries on read and write *)


corollary Renaming_Mndetprefix_inj_on:
  ‹Renaming (Mndetprefix A P) f = ⊓ b ∈ f ` A → Renaming (P (THE a. a ∈ A ∧ f a = b)) f› 
  if inj_on_f: ‹inj_on f A›
  apply (subst Renaming_Mndetprefix[symmetric])
  apply (intro arg_cong[where f = ‹λQ. Renaming Q f›] mono_Mndetprefix_eq)
  by (metis that the_inv_into_def the_inv_into_f_f)
  


corollary Renaming_Mndetprefix_inj:
  ‹Renaming (Mndetprefix A P) f = ⊓ b ∈ f ` A →  Renaming (P (THE a. f a = b)) f› 
  if inj_f: ‹inj f›
  apply (subst Renaming_Mndetprefix_inj_on, metis inj_eq inj_onI that)
  apply (rule mono_Mndetprefix_eq[rule_format])
  by (metis imageE inj_eq[OF inj_f])

section‹Assertions›

abbreviation deadlock_free⇩S⇩K⇩I⇩P :: "'a process ⇒ bool"
  where   "deadlock_free⇩S⇩K⇩I⇩P ≡ deadlock_free_v2"


lemma deadlock_free_implies_lifelock_free: ‹deadlock_free P ⟹ lifelock_free P›
  unfolding deadlock_free_def lifelock_free_def
  using CHAOS_DF_refine_FD trans_FD by blast

lemmas deadlock_free⇩S⇩K⇩I⇩P_def = deadlock_free_v2_def
   and deadlock_free⇩S⇩K⇩I⇩P_is_right = deadlock_free_v2_is_right
   and deadlock_free⇩S⇩K⇩I⇩P_implies_div_free = deadlock_free_v2_implies_div_free
   and deadlock_free⇩S⇩K⇩I⇩P_FD = deadlock_free_v2_FD
   and deadlock_free⇩S⇩K⇩I⇩P_is_right_wrt_events = deadlock_free_v2_is_right_wrt_events
   and deadlock_free_is_deadlock_free⇩S⇩K⇩I⇩P = deadlock_free_is_deadlock_free_v2
   and deadlock_free⇩S⇩K⇩I⇩P_SKIP = deadlock_free_v2_SKIP
   and non_deadlock_free⇩S⇩K⇩I⇩P_STOP = non_deadlock_free_v2_STOP


section ‹Lifelock Freeness›

definition lifelock_free⇩S⇩K⇩I⇩P :: "'a process ⇒ bool"
  where   "lifelock_free⇩S⇩K⇩I⇩P P ≡ CHAOS⇩S⇩K⇩I⇩P UNIV ⊑⇩F⇩D P"

lemma div_free_is_lifelock_free⇩S⇩K⇩I⇩P: "lifelock_free⇩S⇩K⇩I⇩P P ⟷ 𝒟 P = {}"
  using CHAOS⇩S⇩K⇩I⇩P_has_all_failures_Un leFD_imp_leD leF_leD_imp_leFD
        div_free_divergence_refine(1) lifelock_free⇩S⇩K⇩I⇩P_def 
  by blast
  
lemma lifelock_free_is_lifelock_free⇩S⇩K⇩I⇩P: "lifelock_free P ⟹ lifelock_free⇩S⇩K⇩I⇩P P"
  by (simp add: leFD_imp_leD div_free_divergence_refine(2) div_free_is_lifelock_free⇩S⇩K⇩I⇩P lifelock_free_def)

corollary deadlock_free⇩S⇩K⇩I⇩P_is_lifelock_free⇩S⇩K⇩I⇩P: "deadlock_free⇩S⇩K⇩I⇩P P ⟹ lifelock_free⇩S⇩K⇩I⇩P P"
  by (simp add: deadlock_free⇩S⇩K⇩I⇩P_implies_div_free div_free_is_lifelock_free⇩S⇩K⇩I⇩P)


section ‹New Laws›


lemma non_terminating_Sync: 
  ‹non_terminating P ⟹ lifelock_free⇩S⇩K⇩I⇩P Q ⟹ non_terminating (P ⟦A⟧ Q)›
  apply (simp add: non_terminating_is_right div_free_is_lifelock_free⇩S⇩K⇩I⇩P T_Sync)
  apply (intro ballI, simp add: non_terminating_is_right nonterminating_implies_div_free)
  by (metis empty_iff ftf_Sync1 ftf_Sync21 insertI1 tickFree_def)


lemmas non_terminating_Par = non_terminating_Sync[where A = ‹UNIV›]
   and non_terminating_Inter = non_terminating_Sync[where A = ‹{}›]


syntax
  "_writeS"  :: "['b ⇒ 'a, pttrn, 'b set, 'a process] => 'a process"  (‹(4(_❙!_❙|_) /→ _)› [0,0,50,78] 50)
syntax_consts
  "_writeS" == Mndetprefix
translations
  "_writeS c p b P"  => "CONST Mndetprefix (c ` {p. b}) (λ_. P)"

end