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 Syncptick_locale) ‹
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‹tick_join› 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 Syncptick_comm_locale =
  Syncptick_locale ‹(⊗✓)› for tick_join :: ‹'r ⇒ 's ⇒ 't option› (infixl ‹⊗✓› 100) +
fixes tick_join_rev      :: ‹'s ⇒ 'r ⇒ 'u option› (infixl ‹⊗✓rev› 100)
  and tick_join_conv     :: ‹'t ⇒ 'u› (‹⊗✓⇒⊗✓rev›)
  and tick_join_rev_conv :: ‹'u ⇒ 't› (‹⊗✓rev⇒⊗✓›)
assumes tick_join_None_iff :
  ‹r ⊗✓ s = ◇ ⟷ s ⊗✓rev r = ◇›
  and tick_join_Some_imp :
  ‹r ⊗✓ s = ⌊r_s⌋ ⟹ s ⊗✓rev r = ⌊⊗✓⇒⊗✓rev r_s⌋›
  and tick_join_rev_Some_imp :
  ‹s ⊗✓rev r = ⌊s_r⌋ ⟹ r ⊗✓ s = ⌊⊗✓rev⇒⊗✓ s_r⌋›
begin


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

sublocale Syncptick_comm_locale_sym :
  Syncptick_comm_locale ‹(⊗✓rev)› ‹(⊗✓)› ‹⊗✓rev⇒⊗✓› ‹⊗✓⇒⊗✓rev›
proof unfold_locales
  show ‹s ⊗✓rev r = ⌊s_r⌋ ⟹ s' ⊗✓rev r' = ⌊s_r⌋
        ⟹ s' = s ∧ r' = r› for s r s_r s' r'
    using inj_tick_join tick_join_rev_Some_imp by blast
next
  show ‹s ⊗✓rev r = ◇ ⟷ r ⊗✓ s = ◇› for s r
    by (simp add: tick_join_None_iff)
next
  show ‹s ⊗✓rev r = ⌊s_r⌋ ⟹ r ⊗✓ s = ⌊⊗✓rev⇒⊗✓ s_r⌋› for s r s_r
    by (simp add: tick_join_rev_Some_imp)
next
  show ‹r ⊗✓ s = ⌊r_s⌋ ⟹ s ⊗✓rev r = ⌊⊗✓⇒⊗✓rev r_s⌋› for r s r_s
    by (simp add: tick_join_Some_imp)
qed


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



subsection ‹First Properties›

lemma tick_join_conv_image_range_tick_join :
  ‹⊗✓⇒⊗✓rev ` range_tick_join = Syncptick_comm_locale_sym.range_tick_join›
  by (simp add: set_eq_iff flip: setcompr_eq_image)
    (metis option.inject tick_join_Some_imp tick_join_rev_Some_imp)

lemma tick_join_rev_conv_comp_tick_join_conv [simp] :
  ‹r_s ∈ range_tick_join ⟹ ⊗✓rev⇒⊗✓ (⊗✓⇒⊗✓rev r_s) = r_s›
  using tick_join_Some_imp tick_join_rev_Some_imp by fastforce

lemma inj_on_tick_join_conv : ‹inj_on ⊗✓⇒⊗✓rev range_tick_join›
  by (rule inj_onI, simp)
    (metis option.inject tick_join_Some_imp tick_join_rev_Some_imp)

lemma bij_betw_tick_join_conv :
  ‹bij_betw ⊗✓⇒⊗✓rev range_tick_join Syncptick_comm_locale_sym.range_tick_join›
proof (rule bij_betw_imageI)
  show ‹inj_on ⊗✓⇒⊗✓rev range_tick_join›
    by (fact inj_on_tick_join_conv)
next
  show ‹⊗✓⇒⊗✓rev ` range_tick_join = Syncptick_comm_locale_sym.range_tick_join›
    using tick_join_conv_image_range_tick_join by blast
qed



lemma map_tick_join_rev_conv_map_tick_join_conv :
  ‹{r_s. ✓(r_s) ∈ set t} ⊆ range_tick_join ⟹
   map (map_eventptick id ⊗✓rev⇒⊗✓) (map (map_eventptick id ⊗✓⇒⊗✓rev) t) = t›
proof (induct t)
  case Nil show ?case by simp
next
  let ?f1 = ‹map_eventptick id ⊗✓⇒⊗✓rev›
  let ?f2 = ‹map_eventptick id ⊗✓rev⇒⊗✓›
  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_tick_join› by auto
    with ‹e = ✓(r_s)› inj_on_tick_join_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 Syncptick_comm_locale begin

lemma setinterleavesptick_imp_setinterleavesptick_rev :
  ‹t setinterleaves✓⇘(⊗✓)⇙ ((u, v), A) ⟹
   map (map_eventptick id ⊗✓⇒⊗✓rev) t
   setinterleaves✓⇘(⊗✓rev)⇙ ((v, u), A)›
  ― ‹Finally not used, and probably obtainable as a corollary of
      @{thm inj_on_map_map_eventptick_setinterleavesptick[OF inj_on_tick_join_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 ⊗✓⇒⊗✓rev) t'
        setinterleaves✓⇘(⊗✓rev)⇙ ((v, u), A)› .
  moreover from tick_join_Some_imp[OF "*"(1)]
  have ‹s ⊗✓rev r = ⌊⊗✓⇒⊗✓rev r_s⌋› .
  ultimately show ‹map (map_eventptick id ⊗✓⇒⊗✓rev) t
                   setinterleaves✓⇘(⊗✓rev)⇙ ((✓(s) # v, ✓(r) # u), A)›
    by (simp add: "*"(1, 2))
qed auto

lemma vimage_tick_join_rev_conv_subset_super_ref_Syncptick_iff :
  ‹map_eventptick id ⊗✓rev⇒⊗✓ -` X ⊆ super_ref_Syncptick (⊗✓rev) 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 Syncptick_comm_locale_sym.vimage_inj_on_subset_super_ref_Syncptick_iff
            [OF Syncptick_comm_locale_sym.inj_on_tick_join_conv]}.›
proof -
  have * : ‹(λr s. case r ⊗✓rev s of ◇ ⇒ ◇ | ⌊r_s⌋ ⇒ ⌊⊗✓rev⇒⊗✓ r_s⌋) =
            (λs r. r ⊗✓ s)›
    by (intro ext, simp split: option.split)
      (metis tick_join_None_iff tick_join_rev_Some_imp)
  show ?thesis
  proof (subst Syncptick_comm_locale_sym.vimage_inj_on_subset_super_ref_Syncptick_iff)
    show ‹inj_on ⊗✓rev⇒⊗✓ Syncptick_comm_locale_sym.range_tick_join›
      by (fact Syncptick_comm_locale_sym.inj_on_tick_join_conv)
  next
    show ‹X ⊆ super_ref_Syncptick
               (λr s. case r ⊗✓rev s of ◇ ⇒ ◇ | ⌊r_s⌋ ⇒ ⌊⊗✓rev⇒⊗✓ r_s⌋) X_Q A X_P
          ⟷ X ⊆ super_ref_Syncptick (⊗✓) X_P A X_Q›
      using super_ref_Syncptick_sym 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) ⊗✓⇒⊗✓rev = Q ⟦A⟧✓rev P›
proof -
  from inj_on_RenamingTick_Syncptick[OF inj_on_tick_join_conv]
  have ‹RenamingTick (P ⟦A⟧✓ Q) ⊗✓⇒⊗✓rev =
        Syncptick_locale.Syncptick
        (λr s. case r ⊗✓ s of ◇ ⇒ ◇ | ⌊r_s⌋ ⇒ ⌊⊗✓⇒⊗✓rev r_s⌋) P A Q›
    (is ‹_ = Syncptick_locale.Syncptick ?tick_join' P A Q›) .
  also have ‹?tick_join' = (λr s. s ⊗✓rev r)›
    by (intro ext)
      (simp add: Syncptick_comm_locale_sym.tick_join_rev_Some_imp
        tick_join_None_iff split: option.split)
  finally show ‹RenamingTick (P ⟦A⟧✓ Q) ⊗✓⇒⊗✓rev = Q ⟦A⟧✓rev P›
    by (metis Syncptick_comm_locale_sym.Syncptick_sym)
qed


end


(*<*)
end
  (*>*)