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 Sync⇩p⇩t⇩i⇩c⇩k_locale 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_approx1[OF ‹P ⊑ P'›] le_approx_lemma_T[OF ‹P ⊑ P'›]
    le_approx1[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_approx2[OF ‹P ⊑ P'›] le_approx2[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 front_tickFree_Nil self_append_conv, metis)
next
  from le_approx_lemma_F[OF ‹P ⊑ P'›] le_approx_lemma_F[OF ‹Q ⊑ Q'›]
    le_approx1[OF ‹P ⊑ P'›] le_approx_lemma_T[OF ‹P ⊑ P'›] 
    le_approx1[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
  fix t assume ‹t ∈ min_elems (𝒟 (P ⟦A⟧⇩✓ Q))›
  hence ‹t ∈ 𝒟 (P ⟦A⟧⇩✓ Q)› by (fact elem_min_elems)
  then obtain u v t_P t_Q
    where * : ‹t = u @ v› ‹tF u› ‹ftF v›
      ‹u setinterleaves⇩✓⇘tick_join⇙ ((t_P, t_Q), A)›
      ‹t_P ∈ 𝒟 P ∧ t_Q ∈ 𝒯 Q ∨ t_P ∈ 𝒯 P ∧ t_Q ∈ 𝒟 Q›
    unfolding D_Sync⇩p⇩t⇩i⇩c⇩k by blast
  have ‹v = []›
  proof (rule ccontr)
    assume ‹v ≠ []›
    with "*"(1) have ‹u < t› by (simp add: dual_order.strict_iff_not)
    moreover from "*"(2,4,5) have ‹u ∈ 𝒟 (P ⟦A⟧⇩✓ Q)›
      by (simp add: D_Sync⇩p⇩t⇩i⇩c⇩k) (use front_tickFree_Nil in blast)
    ultimately show False
      using ‹t ∈ min_elems (𝒟 (P ⟦A⟧⇩✓ Q))› min_elems_no order_less_imp_le by blast
  qed

  have ‹t_P ∈ min_elems (𝒟 P)› if ‹t_P ∈ 𝒟 P›
  proof (rule ccontr)
    assume ‹t_P ∉ min_elems (𝒟 P)›
    with ‹t_P ∈ 𝒟 P› obtain t_P' where ‹t_P' < t_P› ‹t_P' ∈ 𝒟 P›
      by (metis antisym_conv2 elem_min_elems min_elems5)
    from setinterleaves⇩p⇩t⇩i⇩c⇩k_less_prefixL[OF "*"(4) ‹t_P' < t_P›]
    obtain u' t_Q'
      where $ : ‹u' < u› ‹t_Q' ≤ t_Q›
        ‹u' setinterleaves⇩✓⇘tick_join⇙ ((t_P', t_Q'), A)› by blast
    from "*"(5) D_T have ‹t_Q ∈ 𝒯 Q› by blast
    with "$"(2,3) ‹t_P' ∈ 𝒟 P› have ‹u' ∈ 𝒟 (P ⟦A⟧⇩✓ Q)›
      by (simp add: D_Sync⇩p⇩t⇩i⇩c⇩k')
        (metis append.right_neutral front_tickFree_Nil is_processT3_TR)
    moreover from ‹u' < u› have ‹u' < t›
      by (simp add: "*"(1)) (meson Prefix_Order.prefixI dual_order.strict_trans1)
    ultimately show False
      using ‹t ∈ min_elems (𝒟 (P ⟦A⟧⇩✓ Q))› min_elems_no nless_le by blast
  qed
  with "*"(5) have ‹t_P ∈ 𝒯 P'›
    by (meson in_mono le_approx2T le_approx3 ‹P ⊑ P'›)

  have ‹t_Q ∈ min_elems (𝒟 Q)› if ‹t_Q ∈ 𝒟 Q›
  proof (rule ccontr)
    assume ‹t_Q ∉ min_elems (𝒟 Q)›
    with ‹t_Q ∈ 𝒟 Q› obtain t_Q' where ‹t_Q' < t_Q› ‹t_Q' ∈ 𝒟 Q›
      by (metis antisym_conv2 elem_min_elems min_elems5)
    from setinterleaves⇩p⇩t⇩i⇩c⇩k_less_prefixR[OF "*"(4) ‹t_Q' < t_Q›]
    obtain u' t_P'
      where $ : ‹u' < u› ‹t_P' ≤ t_P›
        ‹u' setinterleaves⇩✓⇘tick_join⇙ ((t_P', t_Q'), A)› by blast
    from "*"(5) D_T have ‹t_P ∈ 𝒯 P› by blast
    with "$"(2,3) ‹t_Q' ∈ 𝒟 Q› have ‹u' ∈ 𝒟 (P ⟦A⟧⇩✓ Q)›
      by (simp add: D_Sync⇩p⇩t⇩i⇩c⇩k')
        (metis append.right_neutral front_tickFree_Nil is_processT3_TR)
    moreover from ‹u' < u› have ‹u' < t›
      by (simp add: "*"(1)) (meson Prefix_Order.prefixI dual_order.strict_trans1)
    ultimately show False
      using ‹t ∈ min_elems (𝒟 (P ⟦A⟧⇩✓ Q))› min_elems_no nless_le by blast
  qed
  with "*"(5) have ‹t_Q ∈ 𝒯 Q'›
    by (meson in_mono le_approx2T le_approx3 ‹Q ⊑ Q'›)

  from ‹t_P ∈ 𝒯 P'› ‹t_Q ∈ 𝒯 Q'› "*"(4) show ‹t ∈ 𝒯 (P' ⟦A⟧⇩✓ Q')›
    by (auto simp add: "*"(1) ‹v = []› T_Sync⇩p⇩t⇩i⇩c⇩k)
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⇩✓⇘tick_join⇙ ((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_tick_join_Sync⇩p⇩t⇩i⇩c⇩k])
      (auto simp add: S_def)
  moreover from le_approx1[OF po_class.chainE[OF chain]] D_T
    le_approx2T[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⇩✓⇘tick_join⇙ ((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_approx1 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_approx2 mono_Sync⇩p⇩t⇩i⇩c⇩k)
qed


lemma (in Sync⇩p⇩t⇩i⇩c⇩k_locale) 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) Sync⇩p⇩t⇩i⇩c⇩k_locale_sym.Sync⇩p⇩t⇩i⇩c⇩k_sym)
    (simp add: Sync⇩p⇩t⇩i⇩c⇩k_locale_sym.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
  (*>*)