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›
    apply (auto simp add: read_def "*" intro!: mono_Mprefix_eq mono_GlobalNdet_eq)
    by (metis (lifting) UN_I UN_upper inj_on_subset inv_into_f_eq that)
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›

lemma MultiSync_read_subset :
  ‹(❙⟦S❙⟧ m ∈# M. c❙?a ∈ A m → P m a) = (if M = {#} then STOP else
   c❙?a ∈ (⋂m ∈ set_mset M. A m) → (❙⟦S❙⟧ m ∈# M. P m a))› (is ‹?lhs = ?rhs›)
  if ‹inj_on c (⋃m ∈ set_mset M. A m)› ‹⋀m. m ∈# M ⟹ c ` A m ⊆ S›
proof -
  have * : ‹M ≠ {#} ⟹ (⋂m∈set_mset M. c ` A m) = c ` ⋂ (A ` set_mset M)›
    by (metis SUP_upper image_INT multiset_nonemptyE that(1))
  have ‹?lhs = (if M = {#} then STOP else
                □a∈(⋂m∈set_mset M. c ` A m) → ❙⟦S❙⟧ m∈#M. (P m ∘ inv_into (A m) c) a)›
    by (simp add: read_def MultiSync_Mprefix_subset that(2))
  also have ‹… = ?rhs›
    apply (auto simp add: read_def "*" intro!: mono_Mprefix_eq mono_MultiSync_eq) 
    by (metis (full_types) INF_lower2 INT_I UN_upper inj_on_subset inv_into_f_f that(1))
  finally show ‹?lhs = ?rhs› .
qed

lemmas MultiPar_read_subset = MultiSync_read_subset[where S = UNIV, simplified]


lemma MultiSync_read_indep :
  ‹❙⟦S❙⟧ m ∈# mset_set M. c❙?a ∈ (A m) → P m a =
   c❙?a ∈ (⋃m ∈ M. A m) → ⊓m ∈ {m ∈ M. a ∈ A m}. (❙⟦S❙⟧ n ∈# mset_set M. (if n = m then P m a else c❙?b ∈ (A n) → P n b))›
  (is ‹?lhs = ?rhs›) if ‹inj_on c (⋃m ∈ M. A m)› ‹finite M› ‹⋀m. m ∈ M ⟹ c ` A m ∩ S = {}›
proof -
  have * : ‹(⋃x∈M. c ` A x) = c ` ⋃ (A ` M)› by auto
  have ** : ‹m ∈ M ⟹ a ∈ A m ⟹ {m ∈ M. c a ∈ c ` A m} = {m ∈ M. inv_into (⋃ (A ` M)) c (c a) ∈ A m}› for a m
    by (auto simp add: image_iff) (metis UN_I inv_into_f_f that(1))+
  have ‹?lhs = □a∈(⋃x∈M. c ` A x)
       → ⊓m∈{m ∈ M. a ∈ c ` A m}.
             ❙⟦S❙⟧ n∈#mset_set M. (if n = m then (P m ∘ inv_into (A m) c) a else Mprefix (c ` A n) (P n ∘ inv_into (A n) c))›
    by (simp add: read_def MultiSync_Mprefix_indep that(2, 3))
  also have ‹… = ?rhs›
    by (auto simp add: read_def "*" "**" intro!: mono_Mprefix_eq mono_GlobalNdet_eq mono_MultiSync_eq)
      (metis UN_upper UnionI imageI inj_on_subset inv_into_f_eq that(1))
  finally show ‹?lhs = ?rhs› .
qed

lemmas MultiInter_read_indep = MultiSync_read_indep[where S = ‹{}›, simplified]


lemma inv_into_eq_inv_into :
  ‹inj_on f A ⟹ B ⊆ A ⟹ C ⊆ A ⟹ a ∈ B ⟹ a ∈ C ⟹
   inv_into B f (f a) = inv_into C f (f a)›
  by (metis inj_on_subset inv_into_f_f)



lemma MultiSync_ndet_write_subset :
  ‹❙⟦S❙⟧ m ∈# M. c❙!❙!a ∈ A m → P m a = (if M = {#} then STOP else
      if ∃a. ∀m m'. m ∈# M ⟶ m' ∈# M - {#m#} ⟶ A m = {a} ∧ A m' = {a}
    then  c❙!❙!a ∈ (⋂m ∈ set_mset M. A m) → (❙⟦S❙⟧ m ∈# M. P m a)
    else (c❙!❙!a ∈ (⋂m ∈ set_mset M. A m) → (❙⟦S❙⟧ m ∈# M. P m a)) ⊓ STOP)›
  (is ‹?lhs M = (if M = {#} then STOP else if ?cond M then ?rhs M else ?rhs M ⊓ STOP)›)
  if ‹inj_on c (⋃m ∈ set_mset M. A m)› ‹⋀m. m ∈# M ⟹ c ` A m ⊆ S›
proof (induct M rule: induct_subset_mset_empty_single)
  case 1 show ?case by simp
next
  case (2 m) show ?case by simp
next
  case (3 M' m)
  from "3"(1-3) that(2) have subset_props : ‹A m ⊆ (⋃m ∈ set_mset M. A m)›
    ‹⋂ (A ` set_mset M') ⊆ (⋃m ∈ set_mset M. A m)›
    ‹⋂ (A ` set_mset (add_mset m M')) ⊆ (⋃m ∈ set_mset M. A m)›
    ‹c ` (⋃m ∈ set_mset M. A m) ⊆ S›
    by auto (meson mset_subset_eqD multiset_nonemptyE)
  note inj_props = subset_props(1, 2)[THEN inj_on_subset[OF that(1)]]
  
  have $ : ‹c ` A m = c ` ⋂ (A ` set_mset M') ⟷ A m = ⋂ (A ` set_mset M')›
    by (simp only: inj_on_image_eq_iff[OF that(1) subset_props(1, 2)])
  have $$ : ‹c ` (A m ∩ ⋂ (A ` set_mset M')) = c ` A m ∩ c ` (⋂ (A ` set_mset M'))›
    by (fact inj_on_image_Int[OF that(1) subset_props(1, 2)])
  from "3"(1, 2)
  have * : ‹ndet_write c (A m) (P m) ⟦S⟧ ?rhs M' =
            (if ∃a. A m = {a} ∧ ⋂ (A ` set_mset M') = {a}
             then c❙!(THE a. ⋂ (A ` set_mset M') = {a}) →
                  (P m (THE a. A m = {a}) ⟦S⟧
                   ❙⟦S❙⟧ m∈#M'. P m (THE a. ⋂ (A ` set_mset M') = {a}))
             else (c❙!❙!x∈(⋂ (A ` set_mset (add_mset m M'))) → ❙⟦S❙⟧ m∈#add_mset m M'. P m x) ⊓ STOP)›
    unfolding ndet_write_Sync_ndet_write_subset
              [OF subset_props(1, 2)[THEN image_mono, THEN subset_trans[OF _ subset_props(4)]]]
    by (auto simp add: "3"(3) write_is_write0 ndet_write_def "$$"
           intro!: arg_cong[where f = ‹λP. P ⊓ STOP›] mono_Mndetprefix_eq
                   arg_cong2[where f = ‹λP Q. P ⟦S⟧ Q›] mono_MultiSync_eq arg_cong[where f = ‹λa. P _ a›]
                   inv_into_eq_inv_into[OF that(1) subset_props(1, 3), simplified]
                   inv_into_eq_inv_into[OF that(1) subset_props(2, 3), simplified])
      (metis "$" empty_is_image image_insert inj_props(1) inv_into_image_cancel subset_iff,
       ((metis INT_I inv_into_f_f subset_iff subset_props(1, 2) that(1))+)[2],
        metis UN_I inj_onD mset_subset_eqD that(1))
  have ** : ‹?cond (add_mset m M') ⟷
             (if size M' = 1 then ∃a. A m = {a} ∧ A (THE m. M' = {#m#}) = {a}
              else ?cond M' ∧ (∃a. A m = {a} ∧ ⋂ (A ` set_mset M') = {a}))›
    by (cases M', auto simp add: "3"(3) split: if_split_asm)
      (metis Int_absorb all_not_in_conv insertI1 set_mset_eq_empty_iff singletonD)
  from "3.hyps"(1) that(2) have *** : ‹ndet_write c (A m) (P m) ⟦S⟧ STOP = STOP›
    by (auto simp add: ndet_write_Sync_STOP inj_props(1) ndet_write_is_STOP_iff Ndet_is_STOP_iff Int_absorb2)
  have ‹?lhs (add_mset m M') = ndet_write c (A m) (P m) ⟦S⟧ ❙⟦S❙⟧ m'∈# M'. ndet_write c (A m') (P m')›
    by (simp add: "3"(3))
  also have ‹… = ndet_write c (A m) (P m) ⟦S⟧
                  (if ?cond M' then ?rhs M' else ?rhs M' ⊓ STOP)›
    by (simp add: "3"(3, 4))
  also have ‹… = (if ?cond (add_mset m M') then ?rhs (add_mset m M')
                   else ?rhs (add_mset m M') ⊓ STOP)› (is ‹?lhs' m M' = ?rhs' m M'›)
  proof (split if_split, intro conjI impI)
    show ‹?cond (add_mset m M') ⟹ ?lhs' m M' = ?rhs (add_mset m M')›
      unfolding "**"
      by (cases M', auto simp add: "3"(3) write_Sync_write split: if_split_asm)
        (metis "3.hyps"(1) image_insert insert_subset that(2))+
  next
    show ‹¬ ?cond (add_mset m M') ⟹ ?lhs' m M' = ?rhs (add_mset m M') ⊓ STOP›
      unfolding "**"
      by (cases ‹size M' = 1›, simp_all add: "*")
        (cases M', auto simp add: "*" "***" ndet_write_Sync_STOP Sync_distrib_Ndet_left
                        write_Sync_STOP "3"(3) write_Sync_write_subset Ndet_aci(1-4))
  qed
  also have ‹… = (  if add_mset m M' = {#} then STOP 
                   else   if ?cond (add_mset m M') then ?rhs (add_mset m M')
                        else ?rhs (add_mset m M')  ⊓ STOP)› by simp
  finally show ?case .
qed

lemmas MultiPar_ndet_write_subset = MultiSync_ndet_write_subset[where S = UNIV, simplified]


(*<*)
end
  (*>*)