Theory Synchronization_Product_Generalized_Cont

(***********************************************************************************
 * 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
 ***********************************************************************************)

(*<*)
theory Synchronization_Product_Generalized_Cont
  imports Multi_Synchronization_Product_Generalized
begin
  (*>*)


section ‹Synchronization Product›


context Synchro⇩p⇩t⇩i⇩c⇩k begin


subsection ‹Monotonicity›

lemma mono_Sync⇩p⇩t⇩i⇩c⇩k : ‹P ⟦A⟧⇩✓ Q ⊑ P' ⟦A⟧⇩✓ Q'› if ‹P ⊑ P'› and ‹Q ⊑ Q'›
proof (unfold le_approx_def Refusals_after_def, safe)
  from le_approxD(1)[OF ‹P ⊑ P'›] le_approx_lemma_T[OF ‹P ⊑ P'›]
    le_approxD(1)[OF ‹Q ⊑ Q'›] le_approx_lemma_T[OF ‹Q ⊑ Q'›]
  show ‹t ∈ 𝒟 (P' ⟦A⟧⇩✓ Q') ⟹ t ∈ 𝒟 (P ⟦A⟧⇩✓ Q)› for t
    by (simp add: D_Sync⇩p⇩t⇩i⇩c⇩k) fast
next
  from le_approxD(2)[OF ‹P ⊑ P'›] le_approxD(2)[OF ‹Q ⊑ Q'›]
  show ‹t ∉ 𝒟 (P ⟦A⟧⇩✓ Q) ⟹ (t, X) ∈ ℱ (P ⟦A⟧⇩✓ Q) ⟹
        (t, X) ∈ ℱ (P' ⟦A⟧⇩✓ Q')› for t X
    by (simp add: Sync⇩p⇩t⇩i⇩c⇩k_projs', elim disjE)
      (metis F_T ftF_Nil self_append_conv, metis)
next
  from le_approx_lemma_F[OF ‹P ⊑ P'›] le_approx_lemma_F[OF ‹Q ⊑ Q'›]
    le_approxD(1)[OF ‹P ⊑ P'›] le_approx_lemma_T[OF ‹P ⊑ P'›] 
    le_approxD(1)[OF ‹Q ⊑ Q'›] le_approx_lemma_T[OF ‹Q ⊑ Q'›]
  show ‹t ∉ 𝒟 (P ⟦A⟧⇩✓ Q) ⟹ (t, X) ∈ ℱ (P' ⟦A⟧⇩✓ Q') ⟹
        (t, X) ∈ ℱ (P ⟦A⟧⇩✓ Q)› for t X
    by (simp add: Sync⇩p⇩t⇩i⇩c⇩k_projs subset_iff, elim disjE) metis+
next
  from that[THEN le_approxD(3)] that[THEN le_approxD2_T]
  show ‹t ∈ 𝒟⇩m⇩i⇩n (P ⟦A⟧⇩✓ Q) ⟹ t ∈ 𝒯 (P' ⟦A⟧⇩✓ Q')› for t
    by (force dest!: D⇩m⇩i⇩n_Sync⇩p⇩t⇩i⇩c⇩k_subset[THEN set_mp] simp add: Sync⇩p⇩t⇩i⇩c⇩k_projs)
qed



subsection ‹Preliminaries›

lemma chain_Sync⇩p⇩t⇩i⇩c⇩k_left  : ‹chain Y ⟹ chain (λi. Y i ⟦A⟧⇩✓ Q)›
  and chain_Sync⇩p⇩t⇩i⇩c⇩k_right : ‹chain Z ⟹ chain (λi. P ⟦A⟧⇩✓ Z i)›
  by (simp_all add: chain_def mono_Sync⇩p⇩t⇩i⇩c⇩k) 


lemma cont_left_prem_Sync⇩p⇩t⇩i⇩c⇩k :
  ‹(⨆i. Y i) ⟦A⟧⇩✓ Q = (⨆i. Y i ⟦A⟧⇩✓ Q)› if chain: ‹chain Y›
proof (rule Process_eq_optimizedI)
  show ‹t ∈ 𝒟 ((⨆i. Y i) ⟦A⟧⇩✓ Q) ⟹ t ∈ 𝒟 (⨆i. Y i ⟦A⟧⇩✓ Q)› for t
    by (simp add: limproc_is_thelub chain chain_Sync⇩p⇩t⇩i⇩c⇩k_left D_Sync⇩p⇩t⇩i⇩c⇩k D_LUB T_LUB) blast
next
  show ‹(t, X) ∈ ℱ ((⨆i. Y i) ⟦A⟧⇩✓ Q) ⟹ (t, X) ∈ ℱ (⨆i. Y i ⟦A⟧⇩✓ Q)› for t X
    by (simp add: limproc_is_thelub chain chain_Sync⇩p⇩t⇩i⇩c⇩k_left F_Sync⇩p⇩t⇩i⇩c⇩k D_LUB T_LUB F_LUB) blast
next
  fix t
  assume ‹t ∈ 𝒟 (⨆i. Y i ⟦A⟧⇩✓ Q)›
  define S
    where ‹S i ≡ {(t_Y, t_Q, u). ∃v. tF u ∧ ftF v ∧ t = u @ v ∧
                                      u setinterleaves⇩✓⇘tj⇙ ((t_Y, t_Q), A) ∧
                                      (t_Y ∈ 𝒟 (Y i) ∧ t_Q ∈ 𝒯 Q ∨ t_Y ∈ 𝒯 (Y i) ∧ t_Q ∈ 𝒟 Q)}› for i
  from ‹t ∈ 𝒟 (⨆i. Y i ⟦A⟧⇩✓ Q)› have ‹S i ≠ {}› for i
    by (simp add: S_def limproc_is_thelub chain chain_Sync⇩p⇩t⇩i⇩c⇩k_left D_Sync⇩p⇩t⇩i⇩c⇩k D_LUB) fast
  moreover have ‹finite (S 0)›
    by (rule finite_subset[OF _ finite_setinterleaves⇩p⇩t⇩i⇩c⇩k_tj_Sync⇩p⇩t⇩i⇩c⇩k])
      (auto simp add: S_def)
  moreover from le_approxD(1)[OF po_class.chainE[OF chain]] D_T
    le_approxD2_T[OF po_class.chainE[OF chain]]
  have ‹S (Suc i) ⊆ S i› for i by (simp add: S_def) blast
  ultimately have ‹(⋂i. S i) ≠ {}› by (rule Inter_nonempty_finite_chained_sets)
  then obtain t_Y t_Q u where ‹(t_Y, t_Q, u) ∈ (⋂i. S i)› by auto
  hence ‹tF u ∧ ftF (drop (length u) t) ∧
         t = u @ drop (length u) t ∧ u setinterleaves⇩✓⇘tj⇙ ((t_Y, t_Q), A) ∧ 
         ((∀i. t_Y ∈ 𝒟 (Y i)) ∧ t_Q ∈ 𝒯 Q ∨ (∀i. t_Y ∈ 𝒯 (Y i)) ∧ t_Q ∈ 𝒟 Q)›
    by (auto simp add: S_def) (meson chain_lemma le_approxD(1) le_approx_lemma_T subsetD chain)
  show ‹t ∈ 𝒟 ((⨆i. Y i) ⟦A⟧⇩✓ Q)›
    by (simp add: limproc_is_thelub chain D_Sync⇩p⇩t⇩i⇩c⇩k T_LUB D_LUB)
      (use ‹?this› in blast)
next
  fix t X assume ‹(t, X) ∈ ℱ (⨆i. Y i ⟦A⟧⇩✓ Q)› ‹t ∉ 𝒟(⨆i. Y i ⟦A⟧⇩✓ Q)›
  have ‹Y i ⊑ (⨆i. Y i)› for i by (simp add: is_ub_thelub ‹chain Y›)
  moreover from ‹t ∉ 𝒟(⨆i. Y i ⟦A⟧⇩✓ Q)› obtain j where ‹t ∉ 𝒟 (Y j ⟦A⟧⇩✓ Q)›
    by (auto simp add: limproc_is_thelub chain_Sync⇩p⇩t⇩i⇩c⇩k_left ‹chain Y› D_LUB)
  moreover from ‹(t, X) ∈ ℱ (⨆i. Y i ⟦A⟧⇩✓ Q)› have ‹(t, X) ∈ ℱ (Y j ⟦A⟧⇩✓ Q)›
    by (simp add: limproc_is_thelub chain_Sync⇩p⇩t⇩i⇩c⇩k_left ‹chain Y› F_LUB)
  ultimately show ‹(t, X) ∈ ℱ ((⨆i. Y i) ⟦A⟧⇩✓ Q)›
    by (metis (mono_tags, lifting) below_refl le_approxD(2) mono_Sync⇩p⇩t⇩i⇩c⇩k)
qed


lemma (in Synchro⇩p⇩t⇩i⇩c⇩k) cont_right_prem_Sync⇩p⇩t⇩i⇩c⇩k :
  ‹P ⟦A⟧⇩✓ (⨆i. Z i) = (⨆i. P ⟦A⟧⇩✓ Z i)› if ‹chain Z›
  by (subst (1 2) Synchro⇩p⇩t⇩i⇩c⇩k_dual.Sync⇩p⇩t⇩i⇩c⇩k_dual)
    (simp add: Synchro⇩p⇩t⇩i⇩c⇩k_dual.cont_left_prem_Sync⇩p⇩t⇩i⇩c⇩k[OF ‹chain Z›])



subsection ‹Continuity›

lemma Sync⇩p⇩t⇩i⇩c⇩k_cont[simp]: ‹cont (λx. f x ⟦A⟧⇩✓ g x)› if ‹cont f› ‹cont g›
proof (rule cont_apply[where f = ‹λx y. y ⟦A⟧⇩✓ g x›])
  from ‹cont f› show ‹cont f› .
next
  show ‹cont (λy. y ⟦A⟧⇩✓ g x)› for x
  proof (rule contI2)
    show ‹monofun (λy. y ⟦A⟧⇩✓ g x)› by (simp add: monofunI mono_Sync⇩p⇩t⇩i⇩c⇩k)
  next
    show ‹chain Y ⟹ (⨆i. Y i) ⟦A⟧⇩✓ g x ⊑ (⨆i. Y i ⟦A⟧⇩✓ g x)› for Y
      by (simp add: cont_left_prem_Sync⇩p⇩t⇩i⇩c⇩k)
  qed
next
  show ‹cont (λx. y ⟦A⟧⇩✓ g x)› for y
  proof (rule cont_compose[of ‹λx. y ⟦A⟧⇩✓ x›])
    show ‹cont (λx. y ⟦A⟧⇩✓ x)›
    proof (rule contI2)
      show ‹monofun (Sync⇩p⇩t⇩i⇩c⇩k y A)› by (simp add: monofunI mono_Sync⇩p⇩t⇩i⇩c⇩k)
    next
      show ‹chain Z ⟹ y ⟦A⟧⇩✓ (⨆i. Z i) ⊑ (⨆i. y ⟦A⟧⇩✓ Z i)› for Z
        by (simp add: cont_right_prem_Sync⇩p⇩t⇩i⇩c⇩k)
    qed
  next
    from ‹cont g› show ‹cont g› .
  qed
qed

end



lemma MultiSync⇩p⇩t⇩i⇩c⇩k_cont [simp] :
  ‹(⋀l. l ∈ set L ⟹ cont (P l)) ⟹ cont (λx. ❙⟦S❙⟧⇩✓ l ∈@ L. P l x)›
  by (induct L rule: induct_list012)
    (auto intro: RenamingTick_cont inj_imp_finitary injI)



(*<*)
end
  (*>*)