Theory Events_Ticks_CSP_PTick_Laws

(***********************************************************************************
 * 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 ‹Events and Ticks›

(*<*)
theory Events_Ticks_CSP_PTick_Laws
  imports Multi_Sequential_Composition_Generalized
    Multi_Synchronization_Product_Generalized
begin
  (*>*)


section ‹Sequential Composition›

subsection ‹Events›

lemma events_of_Seq⇩p⇩t⇩i⇩c⇩k : ‹α(P ❙;⇩✓ Q) = α(P) ∪ (⋃r ∈ ❙✓❙s(P). α(Q r))›
proof (intro subset_antisym subsetI)
  show ‹a ∈ α(P ❙;⇩✓ Q) ⟹ a ∈ α(P) ∪ (⋃r ∈ ❙✓❙s(P). α(Q r))› for a
  proof (elim events_of_memE)
    fix t assume ‹t ∈ 𝒯 (P ❙;⇩✓ Q)› ‹ev a ∈ set t›
    from this(1) consider (T_P) t' where ‹t = map (ev ∘ of_ev) t'› ‹t' ∈ 𝒯 P› ‹tF t'›
      | (T_Q) t' r u where ‹t = map (ev ∘ of_ev) t' @ u› ‹t' @ [✓(r)] ∈ 𝒯 P› ‹tF t'› ‹u ∈ 𝒯 (Q r)›
      | (D_P) t' u where ‹t = map (ev ∘ of_ev) t' @ u› ‹t' ∈ 𝒟 P› ‹tF t'› ‹ftF u›
      unfolding Seq⇩p⇩t⇩i⇩c⇩k_projs by blast
    thus ‹a ∈ α(P) ∪ (⋃r ∈ ❙✓❙s(P). α(Q r))›
    proof cases
      case T_P
      from T_P(1, 3) ‹ev a ∈ set t› have ‹ev a ∈ set t'›
        by (meson tF_map_ev_of_ev_eq_imp_ev_mem_iff)
      with T_P(2) have ‹a ∈ α(P)› by (rule events_of_memI)
      thus ‹a ∈ α(P) ∪ (⋃r ∈ ❙✓❙s(P). α(Q r))› by simp
    next
      case T_Q
      have ‹r ∈ ❙✓❙s(P) ∨ 𝒟 P ≠ {}›
        by (metis T_Q(2) empty_iff strict_ticks_of_memI)
      thus ‹a ∈ α(P) ∪ (⋃r ∈ ❙✓❙s(P). α(Q r))›
      proof (elim disjE)
        from T_Q
        show ‹r ∈ ❙✓❙s(P) ⟹ a ∈ α(P) ∪ (⋃r ∈ ❙✓❙s(P). α(Q r))›
          by simp (metis Un_iff ‹ev a ∈ set t› events_of_memI set_append
              tF_map_ev_of_ev_eq_imp_ev_mem_iff)
      next
        assume ‹𝒟 P ≠ {}›
        hence ‹α(P) = UNIV› by (simp add: events_of_is_strict_events_of_or_UNIV)
        thus ‹a ∈ α(P) ∪ (⋃r ∈ ❙✓❙s(P). α(Q r))› by simp
      qed
    next
      case D_P
      have ‹α(P) = UNIV›
        by (metis D_P(2) empty_iff events_of_is_strict_events_of_or_UNIV)
      thus ‹a ∈ α(P) ∪ (⋃r ∈ ❙✓❙s(P). α(Q r))› by simp
    qed
  qed
next
  show ‹a ∈ α(P) ∪ (⋃r ∈ ❙✓❙s(P). α(Q r)) ⟹ a ∈ α(P ❙;⇩✓ Q)› for a
  proof (elim UnE UnionE events_of_memE, safe)
    fix t assume ‹t ∈ 𝒯 P› ‹ev a ∈ set t›
    then obtain t' where ‹t' ∈ 𝒯 P› ‹tF t'› ‹ev a ∈ set t'›
      by (cases t rule: rev_cases, simp_all)
        (metis prefixI ‹ev a ∈ set t› append_T_imp_tF event⇩p⇩t⇩i⇩c⇩k.disc(1) is_processT3_TR
          not_Cons_self2 tF_Cons_iff tF_Nil tF_append_iff)
    thus ‹a ∈ α(P ❙;⇩✓ Q)› by (auto simp add: Seq⇩p⇩t⇩i⇩c⇩k_projs rev_image_eqI intro!: events_of_memI)
  next
    fix a r assume ‹a ∈ α(Q r)› ‹r ∈ ❙✓❙s(P)›
    from ‹r ∈ ❙✓❙s(P)› obtain t where ‹t @ [✓(r)] ∈ 𝒯 P› by (meson strict_ticks_of_memD)
    moreover from ‹a ∈ α(Q r)› obtain u
      where ‹u ∈ 𝒯 (Q r)› ‹ev a ∈ set u› by (meson events_of_memD)
    ultimately have ‹map (ev ∘ of_ev) t @ u ∈ 𝒯 (P ❙;⇩✓ Q)› ‹ev a ∈ set (map (ev ∘ of_ev) t @ u)›
      by (auto simp add: Seq⇩p⇩t⇩i⇩c⇩k_projs) (metis append_T_imp_tF not_Cons_self2)
    thus ‹a ∈ α(P ❙;⇩✓ Q)› by (simp add: events_of_memI)
  qed
qed

― ‹Big approximation.›
lemma events_of_Seq⇩p⇩t⇩i⇩c⇩k_subset : ‹α(P ❙;⇩✓ Q) ⊆ α(P) ∪ (⋃r. α(Q r))›
  by (auto simp add: events_of_Seq⇩p⇩t⇩i⇩c⇩k)


― ‹Big approximation.›
corollary events_of_Seq_subset : ‹α(P ❙; Q) ⊆ α(P) ∪ α(Q)›
  by (simp add: events_of_Seq)


lemma strict_events_of_Seq⇩p⇩t⇩i⇩c⇩k_subset : ‹❙α(P ❙;⇩✓ Q) ⊆ ❙α(P) ∪ (⋃r ∈ ❙✓❙s(P).❙α(Q r))›
proof (rule subsetI)
  show ‹a ∈ ❙α(P ❙;⇩✓ Q) ⟹ a ∈ ❙α(P) ∪ (⋃r ∈ ❙✓❙s(P).❙α(Q r))› for a
  proof (elim strict_events_of_memE)
    fix t assume ‹t ∈ 𝒯 (P ❙;⇩✓ Q)› ‹t ∉ 𝒟 (P ❙;⇩✓ Q)› ‹ev a ∈ set t›
    from this(1, 2) consider (T_P) t' where ‹t = map (ev ∘ of_ev) t'› ‹t' ∈ 𝒯 P› ‹t' ∉ 𝒟 P› ‹tF t'›
      | (T_Q) t' r u where ‹t = map (ev ∘ of_ev) t' @ u› ‹t' @ [✓(r)] ∈ 𝒯 P› ‹t' ∉ 𝒟 P› ‹tF t'› ‹u ∈ 𝒯 (Q r)› ‹u ∉ 𝒟 (Q r)›
      by (auto simp add: Seq⇩p⇩t⇩i⇩c⇩k_projs) (metis T_imp_ftF)
    thus ‹a ∈ ❙α(P) ∪ (⋃r ∈ ❙✓❙s(P).❙α(Q r))›
    proof cases
      case T_P
      have ‹ev a ∈ set t'›
        by (metis T_P(1, 4) ‹ev a ∈ set t› tF_map_ev_of_ev_eq_imp_ev_mem_iff)
      have ‹a ∈ ❙α(P)›
        by (meson T_P(2, 3) ‹ev a ∈ set t'› strict_events_of_memI)
      thus ‹a ∈ ❙α(P) ∪ (⋃r ∈ ❙✓❙s(P).❙α(Q r))› by simp
    next
      case T_Q
      have ‹r ∈ ❙✓❙s(P)› by (meson T_Q(2, 3) is_processT9 strict_ticks_of_memI)
      thus ‹a ∈ ❙α(P) ∪ (⋃r ∈ ❙✓❙s(P).❙α(Q r))›
        by simp (metis T_Q UnE ‹ev a ∈ set t› is_processT3_TR_append set_append
            strict_events_of_memI tF_map_ev_of_ev_eq_imp_ev_mem_iff)
    qed
  qed
qed


lemma minimal_events_of_Seq⇩p⇩t⇩i⇩c⇩k_subset : ‹α⇩m⇩i⇩n(P ❙;⇩✓ Q) ⊆ α⇩m⇩i⇩n(P) ∪ (⋃r∈❙✓❙s(P). α⇩m⇩i⇩n(Q r))›
  by (auto simp add: minimal_events_of_def append_eq_map_conv
      dest!: strict_events_of_Seq⇩p⇩t⇩i⇩c⇩k_subset[THEN set_mp] D⇩m⇩i⇩n_Seq⇩p⇩t⇩i⇩c⇩k_subset[THEN set_mp])
    (metis event⇩p⇩t⇩i⇩c⇩k.collapse(1) in_set_conv_decomp tF_Cons_iff tF_append_iff,
      metis T_imp_ftF event⇩p⇩t⇩i⇩c⇩k.collapse(1) ftF_append_iff
      in_set_conv_decomp is_processT3_TR_append is_processT7 not_Cons_self2 strict_events_of_memI
      tF_Cons_iff tF_append_iff, meson strict_ticks_of_memI)

corollary minimal_events_of_Seq_subset : ‹α⇩m⇩i⇩n(P ❙; Q) ⊆ α⇩m⇩i⇩n(P) ∪ (⋃r∈❙✓❙s(P). α⇩m⇩i⇩n(Q))›
  by (metis (no_types, lifting) ext Seq⇩p⇩t⇩i⇩c⇩k_const minimal_events_of_Seq⇩p⇩t⇩i⇩c⇩k_subset)



subsection ‹Ticks›

lemma ticks_of_Seq⇩p⇩t⇩i⇩c⇩k :
  ‹✓s(P ❙;⇩✓ Q) = (if 𝒟 P = {} then (⋃r ∈ ❙✓❙s(P). ✓s(Q r)) else UNIV)›
proof (split if_split, intro conjI impI)
  show ‹𝒟 P ≠ {} ⟹ ✓s(P ❙;⇩✓ Q) = UNIV›
    by (simp add: Seq⇩p⇩t⇩i⇩c⇩k_projs ticks_of_is_strict_ticks_of_or_UNIV)
      (metis ftF_Nil nonempty_divE)
next
  show ‹𝒟 P = {} ⟹ ✓s(P ❙;⇩✓ Q) = (⋃r∈❙✓❙s(P). ✓s(Q r))› if ‹𝒟 P = {}›
  proof (intro subset_antisym subsetI)
    from ‹𝒟 P = {}› ticks_of_memI[of _ _ ‹Q _›]
    show ‹s ∈ ✓s(P ❙;⇩✓ Q) ⟹ s ∈ (⋃r∈❙✓❙s(P). ✓s(Q r))› for s
      by (auto simp add: Seq⇩p⇩t⇩i⇩c⇩k_projs strict_ticks_of_def append_eq_map_conv
          append_eq_append_conv2 Cons_eq_append_conv elim!: ticks_of_memE)
        (blast, metis append_Nil)
  next
    show ‹s ∈ (⋃r∈❙✓❙s(P). ✓s(Q r)) ⟹ s ∈ ✓s(P ❙;⇩✓ Q)› for s
      by (auto simp add: Seq⇩p⇩t⇩i⇩c⇩k_projs ticks_of_def elim!: strict_ticks_of_memE)
        (meson append.assoc append_T_imp_tF not_Cons_self2)
  qed
qed


lemma ‹❙✓❙s(P ❙;⇩✓ Q) ⊆ ⋃ {❙✓❙s(Q r) |r. r ∈ ❙✓❙s(P)}›
  ― ‹Already proven earlier in the construction.›
  by (fact strict_ticks_of_Seq⇩p⇩t⇩i⇩c⇩k_subset)




section ‹Synchronization Product›

subsection ‹Events›

lemma (in Synchro⇩p⇩t⇩i⇩c⇩k) events_of_Sync⇩p⇩t⇩i⇩c⇩k_subset : ‹α(P ⟦S⟧⇩✓ Q) ⊆ α(P) ∪ α(Q)›
  by (subst events_of_def, simp add: T_Sync⇩p⇩t⇩i⇩c⇩k subset_iff)
    (metis UNIV_I empty_iff events_of_is_strict_events_of_or_UNIV
      events_of_memI setinterleaves⇩p⇩t⇩i⇩c⇩k_ev_in_set_iff)

lemma (in Synchro⇩p⇩t⇩i⇩c⇩k) events_of_Inter⇩p⇩t⇩i⇩c⇩k: ‹α(P |||⇩✓ Q) = α(P) ∪ α(Q)›
proof (rule subset_antisym[OF events_of_Sync⇩p⇩t⇩i⇩c⇩k_subset])
  show ‹α(P) ∪ α(Q) ⊆ α(P |||⇩✓ Q)›
  proof (rule subsetI, elim UnE)
    fix a assume ‹a ∈ α(P)›
    then obtain t_P where ‹tF t_P› ‹ev a ∈ set t_P› ‹t_P ∈ 𝒯 P›
      by (meson events_of_memE_optimized_tF)
    have ‹map ev (map of_ev t_P) setinterleaves⇩✓⇘tj⇙ ((t_P, []), {})›
      by (simp add: ‹tF t_P› setinterleaves⇩p⇩t⇩i⇩c⇩k_NilR_iff)
    hence ‹map ev (map of_ev t_P) ∈ 𝒯 (P |||⇩✓ Q)›
      by (simp add: T_Sync⇩p⇩t⇩i⇩c⇩k) (metis ‹t_P ∈ 𝒯 P› is_processT1_TR)
    moreover from ‹ev a ∈ set t_P› have ‹ev a ∈ set (map ev (map of_ev t_P))› by force
    ultimately show ‹a ∈ α(P |||⇩✓ Q)› by (metis events_of_memI)
  next
    fix a assume ‹a ∈ α(Q)›
    then obtain t_Q where ‹tF t_Q› ‹ev a ∈ set t_Q› ‹t_Q ∈ 𝒯 Q›
      by (meson events_of_memE_optimized_tF)
    have ‹map ev (map of_ev t_Q) setinterleaves⇩✓⇘tj⇙ (([], t_Q), {})›
      by (simp add: ‹tF t_Q› setinterleaves⇩p⇩t⇩i⇩c⇩k_NilL_iff)
    hence ‹map ev (map of_ev t_Q) ∈ 𝒯 (P |||⇩✓ Q)›
      by (simp add: T_Sync⇩p⇩t⇩i⇩c⇩k) (metis ‹t_Q ∈ 𝒯 Q› is_processT1_TR)
    moreover from ‹ev a ∈ set t_Q› have ‹ev a ∈ set (map ev (map of_ev t_Q))› by force
    ultimately show ‹a ∈ α(P |||⇩✓ Q)› by (metis events_of_memI)
  qed
qed


lemma (in Synchro⇩p⇩t⇩i⇩c⇩k) strict_events_of_Sync⇩p⇩t⇩i⇩c⇩k_subset :
  ‹❙α(P ⟦S⟧⇩✓ Q) ⊆ (❙α(P) - S) ∪ (❙α(Q) - S) ∪ ❙α(P) ∩ ❙α(Q) ∩ S›
proof (rule subsetI)
  fix a assume ‹a ∈ ❙α(P ⟦S⟧⇩✓ Q)›
  then obtain t where ‹t ∈ 𝒯 (P ⟦S⟧⇩✓ Q)› ‹ev a ∈ set t› ‹tF t› ‹t ∉ 𝒟 (P ⟦S⟧⇩✓ Q)›
    by (blast elim: strict_events_of_memE_optimized_tF)
  from ‹t ∈ 𝒯 (P ⟦S⟧⇩✓ Q)› ‹t ∉ 𝒟 (P ⟦S⟧⇩✓ Q)›
  obtain t_P t_Q where ‹t_P ∈ 𝒯 P› ‹t_Q ∈ 𝒯 Q› ‹t_P ∉ 𝒟 P› ‹t_Q ∉ 𝒟 Q›
    and setinter : ‹t setinterleaves⇩✓⇘tj⇙ ((t_P, t_Q), S)›
    by (simp add: Sync⇩p⇩t⇩i⇩c⇩k_projs) (use ‹tF t› ftF_Nil in blast)
  with setinterleaves⇩p⇩t⇩i⇩c⇩k_imp_ev_mem_set_imp_mem_Un_Diff_Int[OF setinter ‹ev a ∈ set t›]
  show ‹a ∈ ❙α(P) - S ∪ (❙α(Q) - S) ∪ ❙α(P) ∩ ❙α(Q) ∩ S›
    by (blast intro: strict_events_of_memI)
qed


lemma (in Synchro⇩p⇩t⇩i⇩c⇩k) minimal_events_of_Sync⇩p⇩t⇩i⇩c⇩k_subset :
  ‹α⇩m⇩i⇩n(P ⟦S⟧⇩✓ Q) ⊆ (α⇩m⇩i⇩n(P) - S) ∪ (α⇩m⇩i⇩n(Q) - S) ∪ α⇩m⇩i⇩n(P) ∩ α⇩m⇩i⇩n(Q) ∩ S›
proof (rule subsetI, elim minimal_events_of_memE)
  fix a t assume ‹t ∈ 𝒯 (P ⟦S⟧⇩✓ Q)› ‹t ∉ 𝒟 (P ⟦S⟧⇩✓ Q)› ‹ev a ∈ set t›
  hence ‹a ∈ ❙α(P ⟦S⟧⇩✓ Q)› by (simp add: strict_events_of_memI)
  thus ‹a ∈ α⇩m⇩i⇩n(P) - S ∪ (α⇩m⇩i⇩n(Q) - S) ∪ α⇩m⇩i⇩n(P) ∩ α⇩m⇩i⇩n(Q) ∩ S›
    by (auto dest!: strict_events_of_Sync⇩p⇩t⇩i⇩c⇩k_subset[THEN set_mp]
        intro: minimal_events_of_memI dest: strict_events_of_memD)
next
  fix a t assume ‹tF t› ‹t ∈ 𝒟⇩m⇩i⇩n (P ⟦S⟧⇩✓ Q)› ‹ev a ∈ set t›
  from this(2) D⇩m⇩i⇩n_Sync⇩p⇩t⇩i⇩c⇩k_subset obtain t_P t_Q
    where * : ‹tF t› ‹t setinterleaves⇩✓⇘(⊗✓)⇙ ((t_P, t_Q), S)›
      ‹t_P ∈ 𝒟⇩m⇩i⇩n P ∧ t_Q ∈ 𝒟⇩m⇩i⇩n Q ∨ t_P ∈ 𝒟⇩m⇩i⇩n P ∧ t_Q ∈ 𝒯 Q - 𝒟 Q ∨ t_Q ∈ 𝒟⇩m⇩i⇩n Q ∧ t_P ∈ 𝒯 P - 𝒟 P› by blast
  from "*"(3) setinterleaves⇩p⇩t⇩i⇩c⇩k_imp_ev_mem_set_imp_mem_Un_Diff_Int[OF "*"(2) ‹ev a ∈ set t›]
  show ‹a ∈ (α⇩m⇩i⇩n(P) - S) ∪ (α⇩m⇩i⇩n(Q) - S) ∪ α⇩m⇩i⇩n(P) ∩ α⇩m⇩i⇩n(Q) ∩ S›
    by (auto intro: minimal_events_of_memI)
qed


corollary minimal_events_of_Sync_subset :
  ‹α⇩m⇩i⇩n(P ⟦S⟧ Q) ⊆ (α⇩m⇩i⇩n(P) - S) ∪ (α⇩m⇩i⇩n(Q) - S) ∪ α⇩m⇩i⇩n(P) ∩ α⇩m⇩i⇩n(Q) ∩ S›
  by (metis Sync⇩C⇩l⇩a⇩s⇩s⇩i⇩c.minimal_events_of_Sync⇩p⇩t⇩i⇩c⇩k_subset Sync⇩C⇩l⇩a⇩s⇩s⇩i⇩c_is_Sync)

corollary ‹α⇩m⇩i⇩n(P ⟦S⟧ Q) ⊆ α⇩m⇩i⇩n(P) ∪ α⇩m⇩i⇩n(Q)›
  using minimal_events_of_Sync_subset by fastforce



subsection ‹Ticks›

lemma (in Synchro⇩p⇩t⇩i⇩c⇩k)
  ‹❙✓❙s(P ⟦S⟧⇩✓ Q) ⊆ {r_s |r_s r s. r ⊗✓ s = Some r_s ∧ r ∈ ❙✓❙s(P) ∧ s ∈ ❙✓❙s(Q)}›
  ― ‹Already proven earlier in the construction.›
  by (fact strict_ticks_of_Sync⇩p⇩t⇩i⇩c⇩k_subset)

lemma (in Synchro⇩p⇩t⇩i⇩c⇩k) ticks_of_no_div_Sync⇩p⇩t⇩i⇩c⇩k_subset :
  ‹𝒟 (P ⟦S⟧⇩✓ Q) = {} ⟹
   ✓s(P ⟦S⟧⇩✓ Q) ⊆ {r_s |r_s r s. tj r s = Some r_s ∧ r ∈ ✓s(P) ∧ s ∈ ✓s(Q)}›
  using strict_ticks_of_Sync⇩p⇩t⇩i⇩c⇩k_subset
  by (simp add: ticks_of_is_strict_ticks_of_or_UNIV subset_iff) blast



section ‹Architectural Operators›

subsection ‹Events›

lemma minimal_events_of_MultiSeq_subset :
  ‹α⇩m⇩i⇩n(SEQ l ∈@ L. P l) ⊆ (⋃l ∈ set L. α⇩m⇩i⇩n(P l))›
  by (induct L rule: rev_induct)
    (auto intro!: subset_trans[OF minimal_events_of_Seq_subset]
      split: if_split_asm)


lemma events_of_MultiSeq⇩p⇩t⇩i⇩c⇩k_subset :
  ‹α((SEQ⇩✓ l ∈@ L. P l) r) ⊆ (⋃l ∈ set L. ⋃r. α(P l r))›
  by (induct L arbitrary: r)
    (auto intro!: subset_trans[OF events_of_Seq⇩p⇩t⇩i⇩c⇩k_subset])

lemma strict_events_of_MultiSeq⇩p⇩t⇩i⇩c⇩k_subset :
  ‹❙α((SEQ⇩✓ l ∈@ L. P l) r) ⊆ (⋃l ∈ set L. ⋃r. ❙α(P l r))›
  by (induct L arbitrary: r, simp)
    (auto intro!: subset_trans[OF strict_events_of_Seq⇩p⇩t⇩i⇩c⇩k_subset])

lemma minimal_events_of_MultiSeq⇩p⇩t⇩i⇩c⇩k_subset :
  ‹α⇩m⇩i⇩n((SEQ⇩✓ l ∈@ L. P l) r) ⊆ (⋃l ∈ set L. ⋃r. α⇩m⇩i⇩n(P l r))›
  by (induct L arbitrary: r, simp)
    (auto intro!: subset_trans[OF minimal_events_of_Seq⇩p⇩t⇩i⇩c⇩k_subset])



lemma minimal_events_of_MultiSync_subset : 
  ‹α⇩m⇩i⇩n(❙⟦S❙⟧ a ∈# M. P a) ⊆
   (⋃l ∈ set_mset M. α⇩m⇩i⇩n(P l)) - S ∪ ((⋂l ∈ set_mset M. α⇩m⇩i⇩n(P l)) ∩ S)›
  by (induct M rule: induct_subset_mset_empty_single, simp_all)
    (auto intro!: subset_trans[OF minimal_events_of_Sync_subset])


lemma events_of_MultiSync⇩p⇩t⇩i⇩c⇩k_subset :
  ‹α(❙⟦S❙⟧⇩✓ l ∈@ L. P l) ⊆ (⋃l∈set L. α(P l))›
  by (induct L rule: induct_list012, simp_all)
    (metis eq_id_iff events_of_Renaming order.order_iff_strict
      image_id events_of_is_strict_events_of_or_UNIV, 
      use Sync⇩R⇩l⇩i⇩s⇩t.events_of_Sync⇩p⇩t⇩i⇩c⇩k_subset in fastforce)

lemma events_of_MultiInter⇩p⇩t⇩i⇩c⇩k :
  ‹α(❙|❙|❙|⇩✓ l ∈@ L. P l) = (⋃l ∈ set L. α(P l))›
  by (induct L rule: induct_list012,
      simp_all add: Sync⇩R⇩l⇩i⇩s⇩t.events_of_Inter⇩p⇩t⇩i⇩c⇩k)
    (metis events_of_Renaming events_of_is_strict_events_of_or_UNIV id_apply image_id)


lemma strict_events_of_MultiSync⇩p⇩t⇩i⇩c⇩k_subset : 
  ‹❙α(❙⟦S❙⟧⇩✓ l ∈@ L. P l) ⊆ (⋃l∈set L. ❙α(P l)) - S ∪ (⋂l∈set L. ❙α(P l)) ∩ S›
  by (induct L rule: induct_list012, simp_all add: strict_events_of_inj_on_Renaming)
    (auto intro!: subset_trans[OF Sync⇩R⇩l⇩i⇩s⇩t.strict_events_of_Sync⇩p⇩t⇩i⇩c⇩k_subset])

lemma minimal_events_of_MultiSync⇩p⇩t⇩i⇩c⇩k_subset : 
  ‹α⇩m⇩i⇩n(❙⟦S❙⟧⇩✓ l ∈@ L. P l) ⊆ (⋃l∈set L. α⇩m⇩i⇩n(P l)) - S ∪ (⋂l∈set L. α⇩m⇩i⇩n(P l)) ∩ S›
  by (induct L rule: induct_list012, simp_all add: strict_events_of_inj_on_Renaming)
    (auto intro!: subset_trans[OF Sync⇩R⇩l⇩i⇩s⇩t.minimal_events_of_Sync⇩p⇩t⇩i⇩c⇩k_subset]
      dest: minimal_events_of_Renaming_subset[THEN set_mp])


subsection ‹Ticks›

text ‹
We only look at \<^const>‹strict_ticks_of› lemmas: \<^const>‹ticks_of› is harder
to deal with because it requires more control on the divergences. 
›

lemma strict_ticks_of_MultiSeq⇩p⇩t⇩i⇩c⇩k_subset :
  ‹❙✓❙s((SEQ⇩✓ l ∈@ L. P l) r) ⊆ (if L = [] then {r} else (⋃r. ❙✓❙s(P (last L) r)))›
proof (induct L arbitrary: r)
  case Nil show ?case by simp
next
  case (Cons l L)
  have ‹(SEQ⇩✓ m ∈@ (l # L). P m) r = P l r ❙;⇩✓ SEQ⇩✓ l ∈@ L. P l› by simp
  also have ‹❙✓❙s(…) ⊆ ⋃ {❙✓❙s((SEQ⇩✓ l ∈@ L. P l) r') |r'. r' ∈ ❙✓❙s(P l r)}›
    by (fact strict_ticks_of_Seq⇩p⇩t⇩i⇩c⇩k_subset)
  also have ‹… ⊆ ⋃ {if L = [] then {r'} else ⋃r. ❙✓❙s(P (last L) r) |r'. r' ∈ ❙✓❙s(P l r)}›
    using Cons.hyps by (blast intro: Union_subsetI)
  also have ‹… ⊆ (if l # L = [] then {r} else ⋃r. ❙✓❙s(P (last (l # L)) r))› by auto
  finally show ?case .
qed

lemma strict_ticks_of_MultiSeq_subset :
  ‹❙✓❙s(SEQ l ∈@ L. P l) ⊆ (if L = [] then {undefined} else (⋃r. ❙✓❙s(P (last L))))›
  using strict_ticks_of_MultiSeq⇩p⇩t⇩i⇩c⇩k_subset[of L ‹λl r. P l›]
  unfolding MultiSeq⇩p⇩t⇩i⇩c⇩k_const by auto



lemma strict_ticks_of_MultiSync⇩p⇩t⇩i⇩c⇩k_subset : 
  ‹❙✓❙s(❙⟦S❙⟧⇩✓ l ∈@ L. P l) ⊆
   {l. length l = length L ∧ (∀i < length L. l ! i ∈ ❙✓❙s(P (L ! i)))}›
proof (induct L rule: induct_list012)
  case 1 show ?case by simp
next
  case (2 l0) show ?case
    by (auto intro!: subset_trans[OF strict_ticks_of_RenamingTick_subset])
next
  case (3 l0 l1 L)
  have ‹❙⟦S❙⟧⇩✓ l ∈@ (l0 # l1 # L). P l = P l0 ⟦S⟧⇩✓⇩R⇩l⇩i⇩s⇩t ❙⟦S❙⟧⇩✓ l ∈@ (l1 # L). P l› by simp
  also have ‹❙✓❙s(…) ⊆ {r # s |r s. r ∈ ❙✓❙s(P l0) ∧ s ∈ ❙✓❙s(❙⟦S❙⟧⇩✓ l ∈@ (l1 # L). P l)}›
    by (auto intro!: subset_trans[OF Sync⇩R⇩l⇩i⇩s⇩t.strict_ticks_of_Sync⇩p⇩t⇩i⇩c⇩k_subset]
        simp add: Sync⇩R⇩l⇩i⇩s⇩t_tj_def)
  also have ‹… ⊆
    {r # s |r s. r ∈ ❙✓❙s(P l0) ∧
                 s ∈ {l. length l = length (l1 # L) ∧
                          (∀i<length (l1 # L). l ! i ∈ ❙✓❙s(P ((l1 # L) ! i)))}}›
    using "3.hyps"(2) by blast
  also have ‹… = {l. length l = length (l0 # l1 # L) ∧
                      (∀i<length (l0 # l1 # L). l ! i ∈ ❙✓❙s(P ((l0 # l1 # L) ! i)))}›
    (is ‹?S1 = ?S2›)
  proof (unfold set_eq_iff, intro allI)
    show ‹l ∈ ?S1 ⟷ l ∈ ?S2› for l
      by (cases l, auto, metis less_Suc_eq_0_disj nth_Cons_0 nth_Cons_Suc)
  qed
  finally show ?case .
qed



section ‹Restriction of the Events›

subsection ‹Synchronization Product›

lemma setinterleaves⇩p⇩t⇩i⇩c⇩k_is_restrictable_on_superset_events_of :
  ‹{a. ev a ∈ set u ∨ ev a ∈ set v} ⊆ A ⟹
   t setinterleaves⇩✓⇘tj⇙ ((u, v), S) ⟷
   t setinterleaves⇩✓⇘tj⇙ ((u, v), S ∩ A)›
  by (induct ‹(tj, u, S, v)› arbitrary: t u v)
    (auto simp add: subset_iff split: option.split_asm)


lemma (in Synchro⇩p⇩t⇩i⇩c⇩k) Sync⇩p⇩t⇩i⇩c⇩k_is_restrictable_on_minimal_events_of :
  ‹P ⟦S⟧⇩✓ Q = P ⟦S ∩ (α⇩m⇩i⇩n(P) ∪ α⇩m⇩i⇩n(Q))⟧⇩✓ Q›
proof -
  have $ : ‹t_P ∈ 𝒟⇩m⇩i⇩n P ∧ t_Q ∈ 𝒟⇩m⇩i⇩n Q ∨ t_P ∈ 𝒟⇩m⇩i⇩n P ∧ t_Q ∈ 𝒯 Q - 𝒟 Q ∨ t_Q ∈ 𝒟⇩m⇩i⇩n Q ∧ t_P ∈ 𝒯 P - 𝒟 P ⟹
    {a. ev a ∈ set t_P ∨ ev a ∈ set t_Q} ⊆ α⇩m⇩i⇩n(P) ∪ α⇩m⇩i⇩n(Q)›
    ‹t_P ∈ 𝒯 P - 𝒟 P ⟹ t_Q ∈ 𝒯 Q - 𝒟 Q ⟹ {a. ev a ∈ set t_P ∨ ev a ∈ set t_Q} ⊆ α⇩m⇩i⇩n(P) ∪ α⇩m⇩i⇩n(Q)› for t_P t_Q
    by (auto intro: minimal_events_of_memI)
  show ‹P ⟦S⟧⇩✓ Q = P ⟦S ∩ (α⇩m⇩i⇩n(P) ∪ α⇩m⇩i⇩n(Q))⟧⇩✓ Q›
  proof (rule Process_eqI_D⇩m⇩i⇩n_version)
    fix t assume ‹t ∈ 𝒟⇩m⇩i⇩n (P ⟦S⟧⇩✓ Q)›
    with D⇩m⇩i⇩n_Sync⇩p⇩t⇩i⇩c⇩k_subset obtain t_P t_Q
      where * : ‹tF t› ‹t setinterleaves⇩✓⇘(⊗✓)⇙ ((t_P, t_Q), S)›
        ‹t_P ∈ 𝒟⇩m⇩i⇩n P ∧ t_Q ∈ 𝒟⇩m⇩i⇩n Q ∨ t_P ∈ 𝒟⇩m⇩i⇩n P ∧ t_Q ∈ 𝒯 Q - 𝒟 Q ∨ t_Q ∈ 𝒟⇩m⇩i⇩n Q ∧ t_P ∈ 𝒯 P - 𝒟 P› by blast
    from setinterleaves⇩p⇩t⇩i⇩c⇩k_is_restrictable_on_superset_events_of[THEN iffD1, OF "$"(1)[OF "*"(3)] "*"(2)]
    have ‹t setinterleaves⇩✓⇘(⊗✓)⇙ ((t_P, t_Q), S ∩ (α⇩m⇩i⇩n(P) ∪ α⇩m⇩i⇩n(Q)))› .
    moreover from "*"(3) have ‹t_P ∈ 𝒟 P ∧ t_Q ∈ 𝒯 Q ∨ t_P ∈ 𝒯 P ∧ t_Q ∈ 𝒟 Q›
      by (metis D_T Diff_iff Divergences⇩m⇩i⇩n_def elem_min_elems)
    ultimately show ‹t ∈ 𝒟 (P ⟦S ∩ (α⇩m⇩i⇩n(P) ∪ α⇩m⇩i⇩n(Q))⟧⇩✓ Q)›
      using "*"(1) append.right_neutral ftF_Nil unfolding Sync⇩p⇩t⇩i⇩c⇩k_projs by blast
  next
    fix t assume ‹t ∈ 𝒟⇩m⇩i⇩n (P ⟦S ∩ (α⇩m⇩i⇩n(P) ∪ α⇩m⇩i⇩n(Q))⟧⇩✓ Q)›
    with D⇩m⇩i⇩n_Sync⇩p⇩t⇩i⇩c⇩k_subset obtain t_P t_Q
      where * : ‹tF t› ‹t setinterleaves⇩✓⇘(⊗✓)⇙ ((t_P, t_Q), S ∩ (α⇩m⇩i⇩n(P) ∪ α⇩m⇩i⇩n(Q)))›
        ‹t_P ∈ 𝒟⇩m⇩i⇩n P ∧ t_Q ∈ 𝒟⇩m⇩i⇩n Q ∨ t_P ∈ 𝒟⇩m⇩i⇩n P ∧ t_Q ∈ 𝒯 Q - 𝒟 Q ∨ t_Q ∈ 𝒟⇩m⇩i⇩n Q ∧ t_P ∈ 𝒯 P - 𝒟 P› by blast
    from setinterleaves⇩p⇩t⇩i⇩c⇩k_is_restrictable_on_superset_events_of[THEN iffD2, OF "$"(1)[OF "*"(3)] "*"(2)]
    have ‹t setinterleaves⇩✓⇘(⊗✓)⇙ ((t_P, t_Q), S)› .
    moreover from "*"(3) have ‹t_P ∈ 𝒟 P ∧ t_Q ∈ 𝒯 Q ∨ t_P ∈ 𝒯 P ∧ t_Q ∈ 𝒟 Q›
      by (metis D_T Diff_iff Divergences⇩m⇩i⇩n_def elem_min_elems)
    ultimately show ‹t ∈ 𝒟 (P ⟦S⟧⇩✓ Q)›
      using "*"(1) append.right_neutral ftF_Nil unfolding Sync⇩p⇩t⇩i⇩c⇩k_projs by blast
  next
    fix t X assume ‹(t, X) ∈ ℱ (P ⟦S⟧⇩✓ Q)› ‹t ∉ 𝒟 (P ⟦S⟧⇩✓ Q)›
    then obtain t_P t_Q X_P X_Q
      where * : ‹(t_P, X_P) ∈ ℱ P› ‹t_P ∉ 𝒟 P› ‹(t_Q, X_Q) ∈ ℱ Q› ‹t_Q ∉ 𝒟 Q›
        ‹t setinterleaves⇩✓⇘tj⇙ ((t_P, t_Q), S)›
        ‹X ⊆ super_ref_Sync⇩p⇩t⇩i⇩c⇩k tj X_P S X_Q›
      by (simp add: F_Sync⇩p⇩t⇩i⇩c⇩k D_Sync⇩p⇩t⇩i⇩c⇩k') (metis (no_types) F_T ftF_Nil self_append_conv)
    from "*"(1-4) have ‹t_P ∈ 𝒯 P - 𝒟 P› ‹t_Q ∈ 𝒯 Q - 𝒟 Q› by (auto dest: F_T)
    from setinterleaves⇩p⇩t⇩i⇩c⇩k_is_restrictable_on_superset_events_of[THEN iffD1, OF "$"(2)[OF this] "*"(5)]
    have ‹t setinterleaves⇩✓⇘(⊗✓)⇙ ((t_P, t_Q), S ∩ (α⇩m⇩i⇩n(P) ∪ α⇩m⇩i⇩n(Q)))› .
    moreover from "*"(1, 2) have ‹(t_P, X_P ∪ {ev a |a. a ∉ α⇩m⇩i⇩n(P)}) ∈ ℱ P›
      by (auto intro!: is_processT5 simp add: minimal_events_of_def strict_events_of_def)
        (metis D⇩m⇩i⇩n_memI Diff_iff F_T append_is_Nil_conv butlast_snoc last_in_set last_snoc not_Cons_self2)
    moreover from "*"(3, 4) have ‹(t_Q, X_Q ∪ {ev a |a. a ∉ α⇩m⇩i⇩n(Q)}) ∈ ℱ Q›
      by (auto intro!: is_processT5 simp add: minimal_events_of_def strict_events_of_def)
        (metis D⇩m⇩i⇩n_memI Diff_iff F_T append_is_Nil_conv butlast_snoc last_in_set last_snoc not_Cons_self2)
    moreover from "*"(6)
    have ‹X ⊆ super_ref_Sync⇩p⇩t⇩i⇩c⇩k
              tj (X_P ∪ {ev a |a. a ∉ α⇩m⇩i⇩n(P)})
              (S ∩ (α⇩m⇩i⇩n(P) ∪ α⇩m⇩i⇩n(Q))) (X_Q ∪ {ev a |a. a ∉ α⇩m⇩i⇩n(Q)})›
      by (auto simp add: super_ref_Sync⇩p⇩t⇩i⇩c⇩k_def)
    ultimately show ‹(t, X) ∈ ℱ (P ⟦S ∩ (α⇩m⇩i⇩n(P) ∪ α⇩m⇩i⇩n(Q))⟧⇩✓ Q)›
      by (auto simp add: F_Sync⇩p⇩t⇩i⇩c⇩k)
  next
    fix t X assume ‹(t, X) ∈ ℱ (P ⟦S ∩ (α⇩m⇩i⇩n(P) ∪ α⇩m⇩i⇩n(Q))⟧⇩✓ Q)›
      ‹t ∉ 𝒟 (P ⟦S ∩ (α⇩m⇩i⇩n(P) ∪ α⇩m⇩i⇩n(Q))⟧⇩✓ Q)›
    then obtain t_P t_Q X_P X_Q
      where * : ‹(t_P, X_P) ∈ ℱ P› ‹t_P ∉ 𝒟 P› ‹(t_Q, X_Q) ∈ ℱ Q› ‹t_Q ∉ 𝒟 Q›
        ‹t setinterleaves⇩✓⇘tj⇙ ((t_P, t_Q), S ∩ (α⇩m⇩i⇩n(P) ∪ α⇩m⇩i⇩n(Q)))›
        ‹X ⊆ super_ref_Sync⇩p⇩t⇩i⇩c⇩k tj X_P (S ∩ (α⇩m⇩i⇩n(P) ∪ α⇩m⇩i⇩n(Q))) X_Q›
      by (simp add: F_Sync⇩p⇩t⇩i⇩c⇩k D_Sync⇩p⇩t⇩i⇩c⇩k') (metis (no_types) F_T ftF_Nil self_append_conv)
    from "*"(1-4) have ‹t_P ∈ 𝒯 P - 𝒟 P› ‹t_Q ∈ 𝒯 Q - 𝒟 Q› by (auto dest: F_T)
    from setinterleaves⇩p⇩t⇩i⇩c⇩k_is_restrictable_on_superset_events_of[THEN iffD2, OF "$"(2)[OF this] "*"(5)]
    have ‹t setinterleaves⇩✓⇘(⊗✓)⇙ ((t_P, t_Q), S)› .
    moreover from "*"(6) have ‹X ⊆ super_ref_Sync⇩p⇩t⇩i⇩c⇩k tj X_P S X_Q›
      by (meson Int_lower1 in_mono subsetI super_ref_Sync⇩p⇩t⇩i⇩c⇩k_mono)
    ultimately show ‹(t, X) ∈ ℱ (P ⟦S⟧⇩✓ Q)›
      using "*"(1, 3) by (auto simp add: F_Sync⇩p⇩t⇩i⇩c⇩k)
  qed
qed

corollary (in Synchro⇩p⇩t⇩i⇩c⇩k) Sync⇩p⇩t⇩i⇩c⇩k_is_restrictable_on_superset_minimal_events_of :
  ‹P ⟦S⟧⇩✓ Q = P ⟦S ∩ A⟧⇩✓ Q› if ‹α⇩m⇩i⇩n(P) ∪ α⇩m⇩i⇩n(Q) ⊆ A›
proof (rule trans[OF Sync⇩p⇩t⇩i⇩c⇩k_is_restrictable_on_minimal_events_of],
    rule trans[OF _ Sync⇩p⇩t⇩i⇩c⇩k_is_restrictable_on_minimal_events_of[symmetric]])
  show ‹P ⟦S ∩ (α⇩m⇩i⇩n(P) ∪ α⇩m⇩i⇩n(Q))⟧⇩✓ Q = P ⟦S ∩ A ∩ (α⇩m⇩i⇩n(P) ∪ α⇩m⇩i⇩n(Q))⟧⇩✓ Q›
    using ‹α⇩m⇩i⇩n(P) ∪ α⇩m⇩i⇩n(Q) ⊆ A› by (auto intro: arg_cong[where f = ‹λS. P ⟦S⟧⇩✓ Q›])
qed


corollary Sync_is_restrictable_on_minimal_events_of :
  ‹P ⟦S⟧ Q = P ⟦S ∩ (α⇩m⇩i⇩n(P) ∪ α⇩m⇩i⇩n(Q))⟧ Q›
  by (metis Sync⇩C⇩l⇩a⇩s⇩s⇩i⇩c.Sync⇩p⇩t⇩i⇩c⇩k_is_restrictable_on_minimal_events_of Sync⇩C⇩l⇩a⇩s⇩s⇩i⇩c_is_Sync)

corollary Sync_is_restrictable_on_superset_minimal_events_of :
  ‹α⇩m⇩i⇩n(P) ∪ α⇩m⇩i⇩n(Q) ⊆ A ⟹ P ⟦S⟧ Q = P ⟦S ∩ A⟧ Q›
  by (metis Sync⇩C⇩l⇩a⇩s⇩s⇩i⇩c.Sync⇩p⇩t⇩i⇩c⇩k_is_restrictable_on_superset_minimal_events_of Sync⇩C⇩l⇩a⇩s⇩s⇩i⇩c_is_Sync)



corollary MultiSync⇩p⇩t⇩i⇩c⇩k_is_restrictable_on_superset_minimal_events_of :
  ‹(⋃l ∈ set L. α⇩m⇩i⇩n(P l)) ⊆ A ⟹ ❙⟦S❙⟧⇩✓ l ∈@ L. P l = ❙⟦S ∩ A❙⟧⇩✓ l ∈@ L. P l›
proof (induct L rule: induct_list012)
  case 1 show ?case by simp
next
  case (2 l0) show ?case by simp
next
  case (3 l0 l1 L)
  from "3.prems" show ?case
    by (simp, subst "3.hyps"(2))
      (auto intro!: Sync⇩R⇩l⇩i⇩s⇩t.Sync⇩p⇩t⇩i⇩c⇩k_is_restrictable_on_superset_minimal_events_of
        dest!: minimal_events_of_MultiSync⇩p⇩t⇩i⇩c⇩k_subset[THEN set_mp])+
qed

corollary MultiSync⇩p⇩t⇩i⇩c⇩k_is_restrictable_on_minimal_events_of :
  ‹❙⟦S❙⟧⇩✓ l ∈@ L. P l = ❙⟦S ∩ (⋃l ∈ set L. α⇩m⇩i⇩n(P l))❙⟧⇩✓ l ∈@ L. P l›
  using MultiSync⇩p⇩t⇩i⇩c⇩k_is_restrictable_on_superset_minimal_events_of by blast


corollary MultiSync_is_restrictable_on_superset_minimal_events_of:
  ‹(⋃m ∈ set_mset M. α⇩m⇩i⇩n(P m)) ⊆ B ⟹ ❙⟦A❙⟧ m ∈# M. P m = ❙⟦A ∩ B❙⟧ m ∈# M. P m›
  by (induct M rule: induct_subset_mset_empty_single)
    (auto intro!: Sync_is_restrictable_on_superset_minimal_events_of
      dest!: minimal_events_of_MultiSync_subset[THEN set_mp])

corollary MultiSync_is_restrictable_on_minimal_events_of:
  ‹❙⟦A❙⟧ m ∈# M. P m = ❙⟦A ∩ ((⋃m ∈ set_mset M. α⇩m⇩i⇩n(P m)))❙⟧ m ∈# M. P m›
  by (metis MultiSync_is_restrictable_on_superset_minimal_events_of subsetI)


(*<*)
end
  (*>*)