Theory Multi_Synchronization_Product

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


section ‹Multiple Synchronization Product›

(*<*)
theory Multi_Synchronization_Product
  imports Induction_Rules_CSPM "HOL-CSP.CSP"
begin
  (*>*)


subsection ‹Definition›

text ‹As in the \<^const>‹Ndet› case, we have no neutral element so we will also have to go through lists
first. But the binary operator \<^const>‹Sync› is not idempotent either, so the generalization will be done
on \<^typ>‹'b multiset› and not on \<^typ>‹'b set›.›

text ‹Note that a \<^typ>‹'b multiset› is by construction finite (cf. theorem
      @{thm Multiset.finite_set_mset[no_vars]}).›

fun MultiSync_list :: ‹['a set, 'b list, 'b ⇒ ('a, 'r) process⇩p⇩t⇩i⇩c⇩k] ⇒ ('a, 'r) process⇩p⇩t⇩i⇩c⇩k›
  where ‹MultiSync_list S   []    P = STOP›
  |     ‹MultiSync_list S (l # L) P = fold (λx r. r ⟦S⟧ P x) L (P l)› 
    (* 

syntax "_MultiSync_list" :: ‹[pttrn, 'a set, 'b list, ('a, 'r) process⇩p⇩t⇩i⇩c⇩k] ⇒ ('a, 'r) process⇩p⇩t⇩i⇩c⇩k›
  (‹(3❙⟦_❙⟧⇩l_∈_./ _)› 63)
translations  "❙⟦S❙⟧⇩l p ∈ L. P " ⇌ "CONST MultiSync_list S L (λp. P)"
 *)

interpretation MultiSync: comp_fun_commute where f = ‹λx r. r ⟦E⟧ P x›
  unfolding comp_fun_commute_def comp_fun_idem_axioms_def comp_def
  by (metis Sync_assoc Sync_commute)


lemma MultiSync_list_mset:
  ‹mset L = mset L' ⟹ MultiSync_list S L P = MultiSync_list S L' P› 
proof (cases L, simp_all)
  fix a l
  assume * : ‹add_mset a (mset l) = mset L'›  and  ** : ‹L = a # l›
  then obtain a' l' where *** : ‹ L' = a' # l'›
    by (metis list.exhaust mset.simps(2) mset_zero_iff)
  note **** = *[simplified ***, simplified]
  have a0: ‹a ≠ a' ⟹ MultiSync_list S L P = 
                       fold (λx r. r ⟦S⟧ P x) (a' # (remove1 a' l)) (P a)›
    apply (subst fold_multiset_equiv[where ys = ‹l›])
      apply (metis MultiSync.comp_fun_commute_axioms comp_fun_commute_def)
     apply (simp_all add: * ** ***) 
    by (metis **** insert_DiffM insert_noteq_member)
  have a1: ‹a ≠ a' ⟹ MultiSync_list S L' P =
                       fold (λx r. r ⟦S⟧ P x) (a # (remove1 a l')) (P a')›   
    apply (subst fold_multiset_equiv[where ys = ‹l'›])
      apply (metis MultiSync.comp_fun_commute_axioms comp_fun_commute_def)
     apply (simp_all add: * ** ***)
    by (metis **** insert_DiffM insert_noteq_member)
  from **** ** *** a0 a1 
  show ‹fold (λx r. r ⟦S⟧ P x) l (P a) = MultiSync_list S L' P›
    apply (cases ‹a = a'›, simp)
     apply (subst fold_multiset_equiv[where ys = l'])      
       apply (metis MultiSync.comp_fun_commute_axioms comp_fun_commute_def)
      apply (simp_all)
    apply (subst fold_multiset_equiv[where ys = ‹remove1 a l'›],
        simp_all add: Sync_commute)
     apply (metis MultiSync.comp_fun_commute_axioms
        comp_fun_commute.comp_fun_commute) 
    by (metis add_mset_commute add_mset_diff_bothsides)
qed


definition MultiSync :: ‹['a set, 'b multiset, 'b ⇒ ('a, 'r) process⇩p⇩t⇩i⇩c⇩k] ⇒ ('a, 'r) process⇩p⇩t⇩i⇩c⇩k›
  where ‹MultiSync S M P = MultiSync_list S (SOME L. mset L = M) P› 

syntax "_MultiSync" :: ‹['a set,pttrn,'b multiset,('a, 'r) process⇩p⇩t⇩i⇩c⇩k] ⇒ ('a, 'r) process⇩p⇩t⇩i⇩c⇩k›
  (‹(3❙⟦_❙⟧ _∈#_./ _)› [78,78,78,77] 77)
syntax_consts "_MultiSync" ⇌ MultiSync
translations "❙⟦S❙⟧ p ∈# M. P " ⇌ "CONST MultiSync S M (λp. P)"




text ‹Special case of \<^term>‹MultiSync E P› when \<^term>‹E = {}›.›

abbreviation MultiInter :: ‹['b multiset, 'b ⇒ ('a, 'r) process⇩p⇩t⇩i⇩c⇩k] ⇒ ('a, 'r) process⇩p⇩t⇩i⇩c⇩k›
  where ‹MultiInter M P ≡ MultiSync {} M P› 

syntax "_MultiInter" :: ‹[pttrn, 'b multiset, ('a, 'r) process⇩p⇩t⇩i⇩c⇩k] ⇒ ('a, 'r) process⇩p⇩t⇩i⇩c⇩k›
  (‹(3❙|❙|❙| _∈#_./ _)› [78,78,77] 77)
syntax_consts "_MultiInter" ⇌ MultiInter
translations "❙|❙|❙| p ∈# M. P" ⇌ "CONST MultiInter M (λp. P)"



text ‹Special case of \<^term>‹MultiSync E P› when \<^term>‹E = UNIV›.›

abbreviation MultiPar :: ‹['b multiset, 'b ⇒ ('a, 'r) process⇩p⇩t⇩i⇩c⇩k] ⇒ ('a, 'r) process⇩p⇩t⇩i⇩c⇩k›
  where ‹MultiPar M P ≡ MultiSync UNIV M P› 

syntax "_MultiPar" :: ‹[pttrn, 'b multiset, ('a, 'r) process⇩p⇩t⇩i⇩c⇩k] ⇒ ('a, 'r) process⇩p⇩t⇩i⇩c⇩k›
  (‹(3❙|❙| _∈#_. / _)› [78,78,77] 77)
syntax_consts "_MultiPar" ⇌ MultiPar
translations "❙|❙| p ∈# M. P" ⇌ "CONST MultiPar M (λp. P)"



subsection ‹First properties›

lemma MultiSync_rec0[simp]: ‹(❙⟦S❙⟧ p ∈# {#}. P p) = STOP›
  unfolding MultiSync_def by simp


lemma MultiSync_rec1[simp]: ‹(❙⟦S❙⟧ p ∈# {#a#}. P p) = P a› 
  unfolding MultiSync_def apply(rule someI2_ex) by simp_all


lemma MultiSync_add[simp]:   
  ‹M ≠ {#} ⟹ (❙⟦S❙⟧ p ∈# add_mset m M. P p) = P m ⟦S⟧ (❙⟦S❙⟧ p ∈# M. P p)›
  unfolding MultiSync_def
  apply(rule someI2_ex, simp add: ex_mset)+
proof(goal_cases)
  case (1 x x')
  thus ‹MultiSync_list S x' P = P m ⟦S⟧ MultiSync_list S x P›
    apply (subst MultiSync_list_mset[where L = ‹x'› and L' = ‹x @ [m]›], simp) 
    by (cases x) (simp_all add: Sync_commute)
qed


lemma mono_MultiSync_eq:
  ‹(⋀x. x ∈# M ⟹ P x = Q x) ⟹ MultiSync S M P = MultiSync S M Q›
  by (cases ‹M = {#}›, simp, induct_tac rule: mset_induct_nonempty) auto

lemma mono_MultiSync_eq2:
  ‹(⋀x. x ∈# M ⟹ P (f x) = Q x) ⟹ MultiSync S (image_mset f M) P = MultiSync S M Q›
  by (cases ‹M = {#}›, simp, induct_tac rule: mset_induct_nonempty) auto


lemmas MultiInter_rec0 = MultiSync_rec0[where S = ‹{}›]
  and MultiPar_rec0 = MultiSync_rec0[where S = ‹UNIV›]
  and MultiInter_rec1 = MultiSync_rec1[where S = ‹{}›]
  and MultiPar_rec1 = MultiSync_rec1[where S = ‹UNIV›]
  and MultiInter_add  =  MultiSync_add[where S = ‹{}›]
  and MultiPar_add  =  MultiSync_add[where S = ‹UNIV›]
  and mono_MultiInter_eq = mono_MultiSync_eq[where S = ‹{}›]
  and mono_MultiPar_eq = mono_MultiSync_eq[where S = ‹UNIV›]
  and mono_MultiInter_eq2 = mono_MultiSync_eq2[where S = ‹{}›]
  and mono_MultiPar_eq2 = mono_MultiSync_eq2[where S = ‹UNIV›]



subsection ‹Some Tests›


lemma ‹MultiSync_list S [] P = STOP› 
  and ‹MultiSync_list S [a] P = P a› 
  and ‹MultiSync_list S [a, b] P = P a ⟦S⟧ P b›  
  and ‹MultiSync_list S [a, b, c] P = P a ⟦S⟧ P b ⟦S⟧ P c›    
  by simp+


lemma test_MultiSync: 
  ‹(❙⟦S❙⟧ p ∈# mset []. P p) = STOP›
  ‹(❙⟦S❙⟧ p ∈# mset [a]. P p) = P a›
  ‹(❙⟦S❙⟧ p ∈# mset [a, b]. P p) = P a ⟦S⟧ P b›
  ‹(❙⟦S❙⟧ p ∈# mset [a, b, c]. P p) = P a ⟦S⟧ P b ⟦S⟧ P c›
  by (simp_all add: Sync_assoc)


lemma MultiSync_set1: ‹MultiSync S (mset_set {k::nat..<k}) P = STOP›
  by fastforce


lemma MultiSync_set2: ‹MultiSync S (mset_set {k..<Suc k}) P = P k›
  by fastforce


lemma MultiSync_set3:
  ‹l <  k ⟹ MultiSync S (mset_set {l ..< Suc k}) P =
   P l ⟦S⟧ (MultiSync S (mset_set {Suc l ..< Suc k}) P)›
  by (simp add: Icc_eq_insert_lb_nat atLeastLessThanSuc_atLeastAtMost)


lemma test_MultiSync':
  ‹(❙⟦S❙⟧ p ∈# mset_set {1::int .. 3}. P p) = P 1 ⟦S⟧ P 2 ⟦S⟧ P 3›
proof -
  have ‹{1::int .. 3} = insert 1 (insert 2 (insert 3 {}))› by fastforce
  thus ‹(❙⟦S❙⟧ p ∈# mset_set {1::int .. 3}. P p) = P 1 ⟦S⟧ P 2 ⟦S⟧ P 3› by (simp add: Sync_assoc)
qed


lemma test_MultiSync'':
  ‹(❙⟦S❙⟧ p ∈# mset_set {0::nat .. a}. P p) =
    ❙⟦S❙⟧ p ∈# mset_set ({a} ∪ {1 .. a} ∪ {0}) . P p›
  by (metis Un_insert_right atMost_atLeast0 boolean_algebra_cancel.sup0
      image_Suc_lessThan insert_absorb2 insert_is_Un lessThan_Suc
      lessThan_Suc_atMost lessThan_Suc_eq_insert_0)



lemmas   test_MultiInter =   test_MultiSync[where S = ‹{}›]
  and   test_MultiPar =   test_MultiSync[where S = ‹UNIV›]
  and   MultiInter_set1 =   MultiSync_set1[where S = ‹{}›]
  and   MultiPar_set1 =   MultiSync_set1[where S = ‹UNIV›]
  and   MultiInter_set2 =   MultiSync_set2[where S = ‹{}›]
  and   MultiPar_set2 =   MultiSync_set2[where S = ‹UNIV›]
  and   MultiInter_set3 =   MultiSync_set3[where S = ‹{}›]
  and   MultiPar_set3 =   MultiSync_set3[where S = ‹UNIV›]
  and  test_MultiInter' =  test_MultiSync'[where S = ‹{}›]
  and  test_MultiPar' =  test_MultiSync'[where S = ‹UNIV›]
  and test_MultiInter'' = test_MultiSync''[where S = ‹{}›]
  and test_MultiPar'' = test_MultiSync''[where S = ‹UNIV›]



subsection ‹Continuity›

lemma mono_MultiSync :
  ‹(⋀x. x ∈# M ⟹ P x ⊑ Q x) ⟹ (❙⟦S❙⟧ m ∈# M. P m) ⊑ (❙⟦S❙⟧ m ∈# M. Q m)›
  by (cases ‹M = {#}›, simp, erule mset_induct_nonempty, simp_all add: mono_Sync)

lemmas mono_MultiInter = mono_MultiSync[where S = ‹{}›]
  and mono_MultiPar = mono_MultiSync[where S = UNIV]


lemma MultiSync_cont[simp]:
  ‹(⋀x. x ∈# M ⟹ cont (P x)) ⟹ cont (λy. ❙⟦S❙⟧ z ∈# M. P z y)›
  by (cases ‹M = {#}›, simp, erule mset_induct_nonempty, simp+)

lemmas MultiInter_cont[simp] = MultiSync_cont[where S = ‹{}›]
  and   MultiPar_cont[simp] = MultiSync_cont[where S = ‹UNIV›]



subsection ‹Factorization of \<^const>‹Sync› in front of \<^const>‹MultiSync››

lemma MultiSync_factorization_union:
  ‹⟦M ≠ {#}; N ≠ {#}⟧ ⟹
   (❙⟦S❙⟧ z ∈# M. P z) ⟦S⟧ (❙⟦S❙⟧ z ∈# N. P z) = ❙⟦S❙⟧ z∈# (M + N). P z›
  by (erule mset_induct_nonempty, simp_all add: Sync_assoc[symmetric])


lemmas MultiInter_factorization_union =
  MultiSync_factorization_union[where S = ‹{}›]
  and   MultiPar_factorization_union =
  MultiSync_factorization_union[where S = ‹UNIV›]



subsection ‹\<^term>‹⊥› Absorbtion›

lemma MultiSync_BOT_absorb:
  ‹m ∈# M ⟹ P m = ⊥ ⟹ (❙⟦S❙⟧ z ∈# M. P z) = ⊥›
  by (metis MultiSync_add MultiSync_rec1 mset_add Sync_BOT Sync_commute)


lemmas MultiInter_BOT_absorb = MultiSync_BOT_absorb[where S =  ‹{}› ]
  and   MultiPar_BOT_absorb = MultiSync_BOT_absorb[where S = ‹UNIV›]


lemma MultiSync_is_BOT_iff:
  ‹(❙⟦S❙⟧ m ∈# M. P m) = ⊥ ⟷ (∃m ∈# M. P m = ⊥)›
  apply (cases ‹M = {#}›, simp add: BOT_iff_Nil_D D_STOP)
  by (rotate_tac, induct M rule: mset_induct_nonempty, auto simp add: Sync_is_BOT_iff)


lemmas MultiInter_is_BOT_iff = MultiSync_is_BOT_iff[where S =  ‹{}› ]
  and   MultiPar_is_BOT_iff = MultiSync_is_BOT_iff[where S = ‹UNIV›]



subsection ‹Other Properties›

lemma MultiSync_SKIP_id:
  ‹(❙⟦S❙⟧ r ∈# M. SKIP r) = (if ∃r. set_mset M = {r} then SKIP (THE r. set_mset M = {r}) else STOP)›
  apply (cases ‹M = {#}›, simp)
  apply (induct M rule: mset_induct_nonempty, simp)
  by (simp add: subset_singleton_iff split: if_splits)


lemmas     MultiInter_SKIP_id = MultiSync_SKIP_id[where S = ‹{}›]
  and       MultiPar_SKIP_id = MultiSync_SKIP_id[where S = ‹UNIV›]



lemma MultiPar_prefix_two_distincts_STOP:
  assumes ‹m ∈# M› and ‹m' ∈# M› and ‹fst m ≠ fst m'›
  shows ‹(❙|❙| a ∈# M. (fst a → P (snd a))) = STOP›
proof -
  obtain M' where f2: ‹M = add_mset m (add_mset m' M')›
    by (metis diff_union_swap insert_DiffM assms)
  show ‹(❙|❙| x ∈# M. (fst x → P (snd x))) = STOP›
    apply (simp add: f2, cases ‹M' = {#}›, simp add: assms(3) write0_Par_write0)
    apply (induct M' rule: mset_induct_nonempty)
     apply (simp add: Sync_commute assms(3) write0_Par_write0)
    by simp (metis (no_types, lifting) STOP_Sync_write0 Sync_assoc Sync_commute UNIV_I)
qed    


lemma MultiPar_prefix_two_distincts_STOP':
  ‹⟦(m, n) ∈# M; (m', n') ∈# M; m ≠ m'⟧ ⟹ 
   (❙|❙| (m, n) ∈# M. (m → P n)) = STOP›
  apply (subst cond_case_prod_eta[where g = ‹λ x. (fst x → P (snd x))›])
  by (simp_all add: MultiPar_prefix_two_distincts_STOP)



subsection ‹Behaviour of \<^const>‹MultiSync› with \<^const>‹Sync››

lemma MultiSync_Sync:
  ‹(❙⟦S❙⟧ z ∈# M. P z) ⟦S⟧ (❙⟦S❙⟧ z ∈# M. P' z) = ❙⟦S❙⟧ z ∈# M. (P z ⟦S⟧ P' z)›
  apply (cases ‹M = {#}›, simp)
  apply (induct M rule: mset_induct_nonempty)
  by simp_all (metis (no_types, lifting) Sync_assoc Sync_commute)


lemmas MultiInter_Inter = MultiSync_Sync[where S = ‹{}›]
  and     MultiPar_Par = MultiSync_Sync[where S = ‹UNIV›]



subsection ‹Commutativity›

lemma MultiSync_sets_commute:
  ‹(❙⟦S❙⟧ a ∈# M. ❙⟦S❙⟧ b ∈# N. P a b) = ❙⟦S❙⟧ b ∈# N. ❙⟦S❙⟧ a ∈# M. P a b›
  apply (cases ‹N = {#}›, induct M, simp_all, 
      metis MultiSync_add MultiSync_rec1 STOP_Sync_STOP)
  apply (induct N rule: mset_induct_nonempty, fastforce)
  by simp (metis MultiSync_Sync)


lemmas MultiInter_sets_commute = MultiSync_sets_commute[where S = ‹{}›]
  and   MultiPar_sets_commute = MultiSync_sets_commute[where S = ‹UNIV›]



subsection ‹Behaviour with Injectivity›

lemma inj_on_mapping_over_MultiSync:
  ‹inj_on f (set_mset M) ⟹ 
   (❙⟦S❙⟧ x ∈# M. P x) = ❙⟦S❙⟧ x ∈# image_mset f M. P (inv_into (set_mset M) f x)›
proof (induct M rule: induct_subset_mset_empty_single, simp, simp)
  case (3 N a)
  hence f1: ‹inv_into (insert a (set_mset N)) f (f a) = a› by force
  show ?case
    apply (simp add: "3.hyps"(2) "3.hyps"(3) f1,
        rule arg_cong[where f = ‹λx. P a ⟦S⟧ x›])
    apply (subst "3.hyps"(4), rule inj_on_subset[OF "3.prems"],
        simp add: subset_insertI)
    apply (rule mono_MultiSync_eq)
    using "3.prems" by fastforce
qed


lemmas inj_on_mapping_over_MultiInter =
  inj_on_mapping_over_MultiSync[where S = ‹{}›]
  and inj_on_mapping_over_MultiPar   =
  inj_on_mapping_over_MultiSync[where S = ‹UNIV›]

(*<*)
end
  (*>*)