Theory Read_Write_CSPM_Laws

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

(*<*)
theory Read_Write_CSPM_Laws
  imports Step_CSPM_Laws_Extended
begin
  (*>*)


subsection ‹The Throw Operator›

lemma Throw_read :
  ‹inj_on c A ⟹ (c❙?a ∈ A → P a) Θ a ∈ B. Q a =
                  c❙?a ∈ A → (if c a ∈ B then Q (c a) else P a Θ a ∈ B. Q a)›
  by (auto simp add: read_def Throw_Mprefix intro: mono_Mprefix_eq)

lemma Throw_ndet_write :
  ‹inj_on c A ⟹ (c❙!❙!a ∈ A → P a) Θ a ∈ B. Q a =
                  c❙!❙!a ∈ A → (if c a ∈ B then Q (c a) else P a Θ a ∈ B. Q a)›
  by (auto simp add: ndet_write_def Throw_Mndetprefix intro: mono_Mndetprefix_eq)

lemma Throw_write :
  ‹(c❙!a → P) Θ a ∈ B. Q a = c❙!a → (if c a ∈ B then Q (c a) else P Θ a ∈ B. Q a)›
  by (auto simp add: write_def Throw_Mprefix intro: mono_Mprefix_eq)

lemma Throw_write0 :
  ‹(a → P) Θ a ∈ B. Q a = a → (if a ∈ B then Q a else P Θ a ∈ B. Q a)›
  by (auto simp add: write0_def Throw_Mprefix intro: mono_Mprefix_eq)



subsection ‹The Interrupt Operator›

lemma Interrupt_read :
  ‹(c❙?a ∈ A → P a) △ Q = Q □ (c❙?a ∈ A → P a △ Q)›
  by (auto simp add: read_def Interrupt_Mprefix
      intro!: mono_Mprefix_eq arg_cong[where f = ‹λP. Q □ P›])

lemma Interrupt_ndet_write :
  ‹(c❙!❙!a ∈ A → P a) △ Q = Q □ (c❙!❙!a ∈ A → P a △ Q)›
  by (auto simp add: ndet_write_def Interrupt_Mndetprefix
      intro!: mono_Mndetprefix_eq arg_cong[where f = ‹λP. Q □ P›])

lemma Interrupt_write : ‹(c❙!a → P) △ Q = Q □ (c❙!a → P △ Q)›
  by (auto simp add: write_def Interrupt_Mprefix intro: mono_Mprefix_eq)

lemma Interrupt_write0 : ‹(a → P) △ Q = Q □ (a → P △ Q)›
  by (auto simp add: write0_def Interrupt_Mprefix intro: mono_Mprefix_eq)



subsection ‹Global Deterministic Choice›

lemma GlobalDet_read :  
  ‹□a ∈ A. c❙?b ∈ B a → P a b = c❙?b ∈ (⋃a∈A. B a) → ⊓a∈{a ∈ A. b ∈ B a}. P a b›
  if ‹inj_on c (⋃a∈A. B a)›
proof -
  have * : ‹a ∈ A ⟹ b ∈ B a ⟹
            {a ∈ A. inv_into (⋃ (B ` A)) c (c b) ∈ B a} = {a ∈ A. c b ∈ c ` B a}› for a b
    by (metis (no_types, opaque_lifting) SUP_upper UN_iff
        inj_on_image_mem_iff inv_into_f_eq ‹inj_on c (⋃a∈A. B a)›)
  have ‹□a ∈ A. c❙?b ∈ B a → P a b =
        □b∈(⋃x∈A. c ` B x) → ⊓a∈{a ∈ A. b ∈ c ` B a}. P a (inv_into (B a) c b)›
    by (simp add: read_def GlobalDet_Mprefix)
  also have ‹(⋃x∈A. c ` B x) = c ` (⋃a∈A. B a)› by blast
  finally show ‹□a ∈ A. c❙?b ∈ B a → P a b = c❙?b ∈ (⋃a∈A. B a) → ⊓a∈{a ∈ A. b ∈ B a}. P a b›
    by (auto simp add: read_def "*" intro!: mono_Mprefix_eq mono_GlobalNdet_eq)
      (metis (lifting) SUP_upper UN_I inv_into_f_eq subset_inj_on ‹inj_on c (⋃a∈A. B a)›)
qed


lemma GlobalDet_write :  
  ‹□a ∈ A. c❙!(b a) → P a = c❙?x ∈ b ` A → ⊓a∈{a ∈ A. x = b a}. P a› if ‹inj_on c (b ` A)›
proof -
  from ‹inj_on c (b ` A)› have * : ‹x ∈ A ⟹ {a ∈ A. inv_into (b ` A) c (c (b x)) = b a} =
                                              {a ∈ A. c (b x) = c (b a)}› for x
    by (auto simp add: inj_on_eq_iff)
  have ‹□a ∈ A. c❙!(b a) → P a = □x∈(⋃a∈A. {c (b a)}) → GlobalNdet {a ∈ A. x = c (b a)} P›
    by (simp add: write_def GlobalDet_Mprefix)
  also have ‹(⋃a∈A. {c (b a)}) = c ` b ` A› by blast
  finally show ‹□a ∈ A. c❙!(b a) → P a = c❙?x ∈ b ` A → ⊓a∈{a ∈ A. x = b a}. P a›
    by (auto simp add: read_def "*" intro: mono_Mprefix_eq)
qed


lemma GlobalDet_write0 :  
  ‹□a∈A. b a → P a = □x ∈ (b ` A) → ⊓a ∈ {a ∈ A. x = b a}. P a›
  by (auto simp add: GlobalDet_write[where c = ‹λx. x›, simplified write_is_write0] read_def
      intro!: mono_Mprefix_eq) (metis (lifting) f_inv_into_f image_eqI)



subsection ‹Multiple Synchronization Product›

(* TODO: add read laws  *)




(*<*)
end
  (*>*)