Theory Synchronization_Product_Generalized_Commutativity

(***********************************************************************************
 * Copyright (c) 2025 Université Paris-Saclay
 *
 * Author: Benoît Ballenghien, Université Paris-Saclay,
 *         CNRS, ENS Paris-Saclay, LMF
 *
 * 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
 *
 * * 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.
 *
 * 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 HOLDER 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.
 *
 * SPDX-License-Identifier: BSD-2-Clause
 ***********************************************************************************)


chapter ‹Commutativity and Associativity of Synchronization›

section ‹Commutativity›

(*<*)
theory Synchronization_Product_Generalized_Commutativity
  imports CSP_PTick_Renaming
begin
  (*>*)

subsection ‹Motivation›

text (in Synchroptick) ‹
The classical synchronization product is commutative: @{thm Sync_commute[of P A Q]}
but in our generalization such a law cannot be obtained in all generality.
Imagine for example that the term‹tj› parameter is actually term‹λr s. ⌊(r, s)⌋›:
we easily figure out that in this case the corresponding law should
be something like ‹P ⟦A⟧✓Pair Q = TickSwap (Q ⟦A⟧✓Pair P)›.
More generally, in the ⬚‹locale›, when writing term‹P ⟦A⟧✓ Q›,
term‹P› is of type typ‹('a, 'r) processptick› while term‹Q› is of type typ‹('a, 's) processptick›
so we want to find an abstract setup in which we can establish a quasi-commutativity.
This is done in the next subsection.
›


subsection ‹Formalization›

locale Synchroptick_comm =
  Synchroptick ‹(⊗✓)› for tj :: ‹'r ⇒ 's ⇒ 't option› (infixl ‹⊗✓› 100) +
fixes tj_dual      :: ‹'s ⇒ 'r ⇒ 'u option› (infixl ‹⊗✓dual› 100)
  and tj_conv      :: ‹'t ⇒ 'u› (‹⊗✓⇒⊗✓dual›)
  and tj_dual_conv :: ‹'u ⇒ 't› (‹⊗✓dual⇒⊗✓›)
assumes tj_None_iff :
  ‹r ⊗✓ s = ◇ ⟷ s ⊗✓dual r = ◇›
  and tj_Some_imp :
  ‹r ⊗✓ s = ⌊r_s⌋ ⟹ s ⊗✓dual r = ⌊⊗✓⇒⊗✓dual r_s⌋›
  and tj_dual_Some_imp :
  ‹s ⊗✓dual r = ⌊s_r⌋ ⟹ r ⊗✓ s = ⌊⊗✓dual⇒⊗✓ s_r⌋›
begin


text ‹There is an obvious symmetry over the variables.›

sublocale Synchroptick_comm_dual :
  Synchroptick_comm ‹(⊗✓dual)› ‹(⊗✓)› ‹⊗✓dual⇒⊗✓› ‹⊗✓⇒⊗✓dual›
proof unfold_locales
  show ‹s ⊗✓dual r = ⌊s_r⌋ ⟹ s' ⊗✓dual r' = ⌊s_r⌋
        ⟹ s' = s ∧ r' = r› for s r s_r s' r'
    using inj_tj tj_dual_Some_imp by blast
next
  show ‹s ⊗✓dual r = ◇ ⟷ r ⊗✓ s = ◇› for s r
    by (simp add: tj_None_iff)
next
  show ‹s ⊗✓dual r = ⌊s_r⌋ ⟹ r ⊗✓ s = ⌊⊗✓dual⇒⊗✓ s_r⌋› for s r s_r
    by (simp add: tj_dual_Some_imp)
next
  show ‹r ⊗✓ s = ⌊r_s⌋ ⟹ s ⊗✓dual r = ⌊⊗✓⇒⊗✓dual r_s⌋› for r s r_s
    by (simp add: tj_Some_imp)
qed


notation Synchroptick_comm_dual.Syncptick (‹(_ ⟦_⟧✓dual _)› [70, 0, 71] 70)
notation Synchroptick_comm_dual.Interptick (‹(_ |||✓dual _)› [72, 73] 72)
notation Synchroptick_comm_dual.Parptick (‹(_ ||✓dual _)› [74, 75] 74)



subsection ‹First Properties›

lemma tj_conv_image_range_tj :
  ‹⊗✓⇒⊗✓dual ` range_tj = Synchroptick_comm_dual.range_tj›
  by (simp add: set_eq_iff flip: setcompr_eq_image)
    (metis option.inject tj_Some_imp tj_dual_Some_imp)

lemma tj_dual_conv_comp_tj_conv [simp] :
  ‹r_s ∈ range_tj ⟹ ⊗✓dual⇒⊗✓ (⊗✓⇒⊗✓dual r_s) = r_s›
  using tj_Some_imp tj_dual_Some_imp by fastforce

lemma inj_on_tj_conv : ‹inj_on ⊗✓⇒⊗✓dual range_tj›
  by (rule inj_onI, simp)
    (metis option.inject tj_Some_imp tj_dual_Some_imp)

lemma bij_betw_tj_conv :
  ‹bij_betw ⊗✓⇒⊗✓dual range_tj Synchroptick_comm_dual.range_tj›
proof (rule bij_betw_imageI)
  show ‹inj_on ⊗✓⇒⊗✓dual range_tj›
    by (fact inj_on_tj_conv)
next
  show ‹⊗✓⇒⊗✓dual ` range_tj = Synchroptick_comm_dual.range_tj›
    using tj_conv_image_range_tj by blast
qed



lemma map_tj_dual_conv_map_tj_conv :
  ‹{r_s. ✓(r_s) ∈ set t} ⊆ range_tj ⟹
   map (map_eventptick id ⊗✓dual⇒⊗✓) (map (map_eventptick id ⊗✓⇒⊗✓dual) t) = t›
proof (induct t)
  case Nil show ?case by simp
next
  let ?f1 = ‹map_eventptick id ⊗✓⇒⊗✓dual›
  let ?f2 = ‹map_eventptick id ⊗✓dual⇒⊗✓›
  case (Cons e t)
  have ‹map ?f2 (map ?f1 (e # t)) = ?f2 (?f1 e) # map ?f2 (map ?f1 t)› by simp
  also have ‹?f2 (?f1 e) = e›
  proof (cases e)
    show ‹e = ev a ⟹ ?f2 (?f1 e) = e› for a by simp
  next
    fix r_s assume ‹e = ✓(r_s)›
    with Cons.prems have ‹r_s ∈ range_tj› by auto
    with ‹e = ✓(r_s)› inj_on_tj_conv
    show ‹?f2 (?f1 e) = e› by simp
  qed
  also have ‹map ?f2 (map ?f1 t) = t›
    by (rule Cons.hyps) (use Cons.prems in auto)
  finally show ‹map ?f2 (map ?f1 (e # t)) = e # t› .
qed

end



subsection ‹Commutativity›

context Synchroptick_comm begin

lemma setinterleavesptick_imp_setinterleavesptick_dual :
  ‹t setinterleaves✓⇘(⊗✓)⇙ ((u, v), A) ⟹
   map (map_eventptick id ⊗✓⇒⊗✓dual) t
   setinterleaves✓⇘(⊗✓dual)⇙ ((v, u), A)›
  ― ‹Finally not used, and probably obtainable as a corollary of
      @{thm inj_on_map_map_eventptick_setinterleavesptick[OF inj_on_tj_conv, of t u A v]}›
proof (induct ‹((⊗✓), u, A, v)› arbitrary: t u v)
  case (tick_setinterleavingptick_tick r u s v)
  from tick_setinterleavingptick_tick.prems
  obtain r_s t'
    where * : ‹r ⊗✓ s = ⌊r_s⌋› ‹t = ✓(r_s) # t'›
      ‹t' setinterleaves✓⇘(⊗✓)⇙ ((u, v), A)›
    by (auto split: option.split_asm)
  from tick_setinterleavingptick_tick.hyps[OF "*"(1), OF "*"(3)]
  have ‹map (map_eventptick id ⊗✓⇒⊗✓dual) t'
        setinterleaves✓⇘(⊗✓dual)⇙ ((v, u), A)› .
  moreover from tj_Some_imp[OF "*"(1)]
  have ‹s ⊗✓dual r = ⌊⊗✓⇒⊗✓dual r_s⌋› .
  ultimately show ‹map (map_eventptick id ⊗✓⇒⊗✓dual) t
                   setinterleaves✓⇘(⊗✓dual)⇙ ((✓(s) # v, ✓(r) # u), A)›
    by (simp add: "*"(1, 2))
qed auto

lemma vimage_tj_dual_conv_subset_super_ref_Syncptick_iff :
  ‹map_eventptick id ⊗✓dual⇒⊗✓ -` X ⊆ super_ref_Syncptick (⊗✓dual) X_Q A X_P
   ⟷ X ⊆ super_ref_Syncptick (⊗✓) X_P A X_Q›
  (is ‹?lhs1 ⊆ ?lhs2 ⟷ X ⊆ ?rhs›)
  ― ‹Same: finally not used, and probably obtainable as a corollary of
      @{thm Synchroptick_comm_dual.vimage_inj_on_subset_super_ref_Syncptick_iff
            [OF Synchroptick_comm_dual.inj_on_tj_conv]}.›
proof -
  have * : ‹(λr s. case r ⊗✓dual s of ◇ ⇒ ◇ | ⌊r_s⌋ ⇒ ⌊⊗✓dual⇒⊗✓ r_s⌋) =
            (λs r. r ⊗✓ s)›
    by (intro ext, simp split: option.split)
      (metis tj_None_iff tj_dual_Some_imp)
  show ?thesis
  proof (subst Synchroptick_comm_dual.vimage_inj_on_subset_super_ref_Syncptick_iff)
    show ‹inj_on ⊗✓dual⇒⊗✓ Synchroptick_comm_dual.range_tj›
      by (fact Synchroptick_comm_dual.inj_on_tj_conv)
  next
    show ‹X ⊆ super_ref_Syncptick
               (λr s. case r ⊗✓dual s of ◇ ⇒ ◇ | ⌊r_s⌋ ⇒ ⌊⊗✓dual⇒⊗✓ r_s⌋) X_Q A X_P
          ⟷ X ⊆ super_ref_Syncptick (⊗✓) X_P A X_Q›
      using super_ref_Syncptick_dual by (simp add: "*") blast
  qed
qed



text ‹
In the end, the proof is quite simple: mainly a corollary
of @{thm inj_on_RenamingTick_Syncptick[no_vars]}.
›

theorem Syncptick_commute :
  ‹RenamingTick (P ⟦A⟧✓ Q) ⊗✓⇒⊗✓dual = Q ⟦A⟧✓dual P›
proof -
  from inj_on_RenamingTick_Syncptick[OF inj_on_tj_conv]
  have ‹RenamingTick (P ⟦A⟧✓ Q) ⊗✓⇒⊗✓dual =
        Synchroptick.Syncptick
        (λr s. case r ⊗✓ s of ◇ ⇒ ◇ | ⌊r_s⌋ ⇒ ⌊⊗✓⇒⊗✓dual r_s⌋) P A Q›
    (is ‹_ = Synchroptick.Syncptick ?tj' P A Q›) .
  also have ‹?tj' = (λr s. s ⊗✓dual r)›
    by (intro ext)
      (simp add: Synchroptick_comm_dual.tj_dual_Some_imp
        tj_None_iff split: option.split)
  finally show ‹RenamingTick (P ⟦A⟧✓ Q) ⊗✓⇒⊗✓dual = Q ⟦A⟧✓dual P›
    by (metis Synchroptick_comm_dual.Syncptick_dual)
qed


end


(*<*)
end
  (*>*)