Theory Events_Ticks_CSPM_Laws

(*<*)
―‹ ********************************************************************
 * Project         : HOL-CSPM - Architectural operators for HOL-CSP
 *
 * Author          : Benoît Ballenghien, Safouan Taha, Burkhart Wolff.
 *
 * This file       : Results on events and ticks
 *
 * Copyright (c) 2025 Université Paris-Saclay, France
 *
 * 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 list of conditions and the following disclaimer.
 *
 *     * 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.
 *
 *     * Neither the name of the copyright holders nor the names of its
 *       contributors may be used to endorse or promote products derived
 *       from this software without specific prior written permission.
 *
 * 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
 * OWNER 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.
 ******************************************************************************›
(*>*)


chapter ‹Results on ‹events_of› and ‹ticks_of››

(*<*)
theory Events_Ticks_CSPM_Laws
  imports CSPM_Laws
begin
  (*>*)

section ‹Events›


lemma events_of_GlobalDet :
  ‹α(□a ∈ A. P a) = (⋃a∈A. α(P a))›
  by (simp add: events_of_def T_GlobalDet)

lemma strict_events_of_GlobalDet_subset : ‹❙α(□a ∈ A. P a) ⊆ (⋃a∈A. ❙α(P a))›
  by (auto simp add: strict_events_of_def GlobalDet_projs)

lemma events_of_MultiSeq_subset :
  ‹α(SEQ l ∈@ L. P l) ⊆ (⋃l ∈ set L. ⋃r. α(P l))›
  by (induct L rule: rev_induct) (auto simp add: events_of_Seq)

lemma strict_events_of_MultiSeq_subset :
  ‹❙α(SEQ l ∈@ L. P l) ⊆ (⋃l ∈ set L. ⋃r. ❙α(P l))›
  by (induct L rule: rev_induct)
    (auto intro!: subset_trans[OF strict_events_of_Seq_subset]
      split: if_split_asm)



lemma events_of_MultiSync_subset :
  ‹α(❙⟦S❙⟧ a ∈# M. P a) ⊆ (⋃a ∈ set_mset M. α(P a))›
  by (induct M rule: induct_subset_mset_empty_single, simp_all)
    (meson Diff_subset_conv dual_order.trans events_of_Sync_subset)

lemma events_of_MultiInter :
  ‹α(❙|❙|❙| a ∈# M. P a) = (⋃a ∈ set_mset M. α(P a))›
  by (induct M rule: induct_subset_mset_empty_single)
    (simp_all add: events_of_Inter)

lemma strict_events_of_MultiSync_subset : 
  ‹❙α(❙⟦S❙⟧ a ∈# M. P a) ⊆ (⋃a ∈ set_mset M. ❙α(P a))›
  by (induct M rule: induct_subset_mset_empty_single, simp_all)
    (metis (no_types, lifting) inf_sup_aci(7) le_supI2 strict_events_of_Sync_subset sup.orderE)


lemma events_of_Throw_subset :
  ‹α(P Θ a ∈ A. Q a) ⊆ α(P) ∪ (⋃a ∈ A ∩ α(P). α(Q a))›
proof (intro subsetI)
  fix e assume ‹e ∈ α(P Θ a ∈ A. Q a)›
  then obtain s where * : ‹ev e ∈ set s› ‹s ∈ 𝒯 (P Θ a ∈ A. Q a)›
    by (simp add: events_of_def) blast
  from "*"(2) consider ‹s ∈ 𝒯 P› ‹set s ∩ ev ` A = {}›
    | t1 t2   where ‹s = t1 @ t2› ‹t1 ∈ 𝒟 P› ‹tF t1› ‹set t1 ∩ ev ` A = {}› ‹ftF t2›
    | t1 a t2 where ‹s = t1 @ ev a # t2› ‹t1 @ [ev a] ∈ 𝒯 P›
      ‹set t1 ∩ ev ` A = {}› ‹a ∈ A› ‹t2 ∈ 𝒯 (Q a)›
    by (simp add: T_Throw) blast
  thus ‹e ∈ α(P) ∪ (⋃a ∈ A ∩ α(P). α(Q a))›
  proof cases
    from "*"(1) show ‹s ∈ 𝒯 P ⟹ set s ∩ ev ` A = {} ⟹
                      e ∈ α(P) ∪ (⋃a ∈ A ∩ α(P). α(Q a))›
      by (simp add: events_of_def) blast
  next
    show ‹⟦s = t1 @ t2; t1 ∈ 𝒟 P; tF t1; set t1 ∩ ev ` A = {}; ftF t2⟧ ⟹
          e ∈ α(P) ∪ (⋃a ∈ A ∩ α(P). α(Q a))› for t1 t2
      by (metis "*"(1) D_T UnI1 events_of_memI is_processT7)
  next
    fix t1 a t2
    assume ** : ‹s = t1 @ ev a # t2› ‹t1 @ [ev a] ∈ 𝒯 P›
      ‹set t1 ∩ ev ` A = {}› ‹a ∈ A› ‹t2 ∈ 𝒯 (Q a)›
    from "*"(1) "**"(1) have ‹ev e ∈ set (t1 @ [ev a]) ∨ ev e ∈ set t2› by simp
    thus ‹e ∈ α(P) ∪ (⋃a ∈ A ∩ α(P). α(Q a))›
    proof (elim disjE)
      show ‹ev e ∈ set (t1 @ [ev a]) ⟹ e ∈ α(P) ∪ (⋃a ∈ A ∩ α(P). α(Q a))›
        by (metis "**"(2) UnI1 events_of_memI)
    next
      show ‹ev e ∈ set t2 ⟹ e ∈ α(P) ∪ (⋃a ∈ A ∩ α(P). α(Q a))›
        by (metis (no_types, lifting) "**"(2, 4, 5) Int_iff UN_iff UnI2
            events_of_memI list.set_intros(1) set_append)
    qed
  qed
qed

(* TODO: strict_events_of *)

lemma events_of_Interrupt : ‹α(P △ Q) = α(P) ∪ α(Q)›
  by (safe elim!: events_of_memE,
      auto simp add: events_of_def Interrupt_projs)
    (metis append_Nil is_processT1_TR tF_Nil)

lemma strict_events_of_Interrupt_subset : ‹❙α(P △ Q) ⊆ ❙α(P) ∪ ❙α(Q)›
  by (safe elim!:strict_events_of_memE,
      auto simp add: strict_events_of_def Interrupt_projs)
    (metis DiffI T_imp_ftF is_processT7)




(* TODO: see about the generalization of that *)
(* lemma events_MultiSeq:
  ‹events_of (SEQ a ∈@ L. P a) =
   (⋃a ∈ set (take (Suc (first_elem (λa. non_terminating (P a)) L)) L). 
    events_of (P a))›
  by (subst non_terminating_MultiSeq, induct L; simp add: events_SKIP events_Seq)

lemma events_MultiSeq_subset:
  ‹events_of (SEQ a ∈@ L. P a) ⊆ (⋃a ∈ set L. events_of (P a))›
  using in_set_takeD by (subst events_MultiSeq) fastforce *)






section ‹Ticks›

lemma ticks_of_GlobalDet:
  ‹ticks_of (□a ∈ A. P a) = (⋃a∈A. ticks_of (P a))›
  by (auto simp add: ticks_of_def T_GlobalDet)

lemma strict_ticks_of_GlobalDet_subset : ‹❙✓❙s(□a ∈ A. P a) ⊆ (⋃a∈A. ❙✓❙s(P a))›
  by (auto simp add: strict_ticks_of_def GlobalDet_projs)







lemma ticks_of_MultiSync_subset :
  ‹✓s(❙⟦S❙⟧ a ∈# M. P a) ⊆ (⋃a ∈ set_mset M. ✓s(P a))›
  by (induct M rule: induct_subset_mset_empty_single, simp_all)
    (meson Diff_subset_conv dual_order.trans ticks_of_Sync_subset)

lemma strict_ticks_of_MultiSync_subset :
  ‹❙✓❙s(❙⟦S❙⟧ a ∈# M. P a) ⊆ (⋂a ∈ set_mset M. ❙✓❙s(P a))›
  by (induct M rule: induct_subset_mset_empty_single, simp_all)
    (use strict_ticks_of_Sync_subset in fastforce)




lemma ticks_Throw_subset :
  ‹✓s(P Θ a∈A. Q a) ⊆ ✓s(P) ∪ (⋃a∈A ∩ α(P). ✓s(Q a))›
proof (rule subsetI, elim ticks_of_memE)
  fix t r assume ‹t @ [✓(r)] ∈ 𝒯 (P Θ a∈A. Q a)›
  from ‹t @ [✓(r)] ∈ 𝒯 (P Θ a∈A. Q a)› consider ‹t @ [✓(r)] ∈ 𝒯 P›
    | t1 t2   where ‹t @ [✓(r)] = t1 @ t2› ‹t1 ∈ 𝒟 P› ‹tF t1› ‹ftF t2›
    | t1 a t2 where ‹t @ [✓(r)] = t1 @ ev a # t2› ‹t1 @ [ev a] ∈ 𝒯 P› ‹a ∈ A› ‹t2 ∈ 𝒯 (Q a)›
    unfolding T_Throw by blast
  thus ‹r ∈ ✓s(P) ∪ (⋃a∈A ∩ α(P). ✓s(Q a))›
  proof cases
    show ‹t @ [✓(r)] ∈ 𝒯 P ⟹ r ∈ ✓s(P) ∪ (⋃a∈A ∩ α(P). ✓s(Q a))›
      by (simp add: ticks_of_memI)
  next
    show ‹⟦t @ [✓(r)] = t1 @ t2; t1 ∈ 𝒟 P; tF t1; ftF t2⟧
          ⟹ r ∈ ✓s(P) ∪ (⋃a∈A ∩ α(P). ✓s(Q a))› for t1 t2
      by (cases t2 rule: rev_cases, auto)
        (metis D_T append_assoc is_processT7 ticks_of_memI)
  next
    show ‹⟦t @ [✓(r)] = t1 @ ev a # t2; t1 @ [ev a] ∈ 𝒯 P; a ∈ A; t2 ∈ 𝒯 (Q a)⟧
          ⟹ r ∈ ✓s(P) ∪ (⋃a∈A ∩ α(P). ✓s(Q a))› for t1 a t2
      by (cases t2 rule: rev_cases, simp_all)
        (meson IntI events_of_memI in_set_conv_decomp ticks_of_memI)
  qed
qed


(* TODO: strict_ticks_of *)

lemma ticks_of_Interrupt : ‹✓s(P △ Q) = ✓s(P) ∪ ✓s(Q)›
  by (safe elim!: ticks_of_memE,
      auto simp add: ticks_of_def Interrupt_projs)
    (metis append.right_neutral last_appendR snoc_eq_iff_butlast,
      metis append_Nil is_processT1_TR tF_Nil)

lemma strict_ticks_of_Interrupt_subset : ‹❙✓❙s(P △ Q) ⊆ ❙✓❙s(P) ∪ ❙✓❙s(Q)›
  by (safe elim!: strict_ticks_of_memE,
      auto simp add: strict_ticks_of_def Interrupt_projs)
    (meson is_processT9,
      metis (no_types, opaque_lifting) Nil_is_append_conv append_assoc
      append_butlast_last_id butlast_snoc is_processT9 last_appendR list.distinct(1))




text ‹\<^const>‹events_of› and \<^const>‹deadlock_free››

lemma nonempty_events_of_if_deadlock_free: ‹deadlock_free P ⟹ α(P) ≠ {}›
  unfolding deadlock_free_def events_of_def failure_divergence_refine_def
    failure_refine_def divergence_refine_def 
  apply (simp add: div_free_DF, subst (asm) DF_unfold)
  apply (auto simp add: F_Mndetprefix write0_def F_Mprefix subset_iff)
  by (metis (full_types) Nil_elem_T T_F is_processT5_S7
      list.set_intros(1) rangeI snoc_eq_iff_butlast)

lemma nonempty_strict_events_of_if_deadlock_free: ‹deadlock_free P ⟹ ❙α(P) ≠ {}›
  by (metis deadlock_free_implies_div_free events_of_is_strict_events_of_or_UNIV nonempty_events_of_if_deadlock_free)

lemma events_of_in_DF: ‹DF A ⊑⇩F⇩D P ⟹ α(P) ⊆ A›
  by (metis anti_mono_events_of_FD events_of_DF)


lemma nonempty_events_of_if_deadlock_free⇩S⇩K⇩I⇩P:
  ‹deadlock_free⇩S⇩K⇩I⇩P⇩S P ⟹ (∃r. [✓(r)] ∈ 𝒯 P) ∨ α(P) ≠ {}›
  unfolding deadlock_free⇩S⇩K⇩I⇩P⇩S_def events_of_def failure_refine_def 
  apply (subst (asm) DF⇩S⇩K⇩I⇩P⇩S_unfold)
  apply (auto simp add: F_Mndetprefix write0_def F_Mprefix subset_iff F_Ndet F_SKIPS)
  by (metis event⇩p⇩t⇩i⇩c⇩k.exhaust is_processT1_TR is_processT5_S7 iso_tuple_UNIV_I list.set_intros(1) self_append_conv2)


lemma events_of_in_DF⇩S⇩K⇩I⇩P: ‹DF⇩S⇩K⇩I⇩P⇩S A R ⊑⇩F⇩D P ⟹ α(P) ⊆ A›
  by (metis anti_mono_events_of_FD events_of_DF⇩S⇩K⇩I⇩P⇩S)

lemma ‹¬ α(P) ⊆ A ⟹ ¬ DF A ⊑⇩F⇩D P›
  and ‹¬ α(P) ⊆ A ⟹ ¬ DF⇩S⇩K⇩I⇩P⇩S A R ⊑⇩F⇩D P›
  by (metis anti_mono_events_of_FD events_of_DF)
    (metis anti_mono_events_of_FD events_of_DF⇩S⇩K⇩I⇩P⇩S)



section ‹Minimal Events›

text ‹New in Isabelle26.›

lemma minimal_events_of_GlobalDet_subset : ‹α⇩m⇩i⇩n(□a ∈ A. P a) ⊆ (⋃a∈A. α⇩m⇩i⇩n(P a))›
  by (auto simp add: minimal_events_of_def
      dest!: strict_events_of_GlobalDet_subset[THEN set_mp] D⇩m⇩i⇩n_GlobalDet_subset[THEN set_mp])


lemma minimal_events_of_Interrupt_subset : ‹α⇩m⇩i⇩n(P △ Q) ⊆ α⇩m⇩i⇩n(P) ∪ α⇩m⇩i⇩n(Q)›
proof (rule subsetI)
  fix a assume ‹a ∈ α⇩m⇩i⇩n(P △ Q)›
  then consider ‹a ∈ ❙α(P △ Q)›
    | t where ‹t ∈ 𝒟⇩m⇩i⇩n(P △ Q)› ‹ev a ∈ set t›
    by (blast dest: minimal_events_of_memD intro: strict_events_of_memI)
  thus ‹a ∈ α⇩m⇩i⇩n(P) ∪ α⇩m⇩i⇩n(Q)›
  proof cases
    show ‹a ∈ ❙α(P △ Q) ⟹ a ∈ α⇩m⇩i⇩n(P) ∪ α⇩m⇩i⇩n(Q)›
      by (metis (no_types, lifting) Un_iff minimal_events_of_def_bis
          strict_events_of_Interrupt_subset subset_iff)
  next
    fix t assume ‹t ∈ 𝒟⇩m⇩i⇩n(P △ Q)› ‹ev a ∈ set t›
    from this(1) consider ‹t ∈ 𝒟⇩m⇩i⇩n P›
      | t1 t2 where ‹t = t1 @ t2› ‹t1 ∈ 𝒯 P› ‹t1 ∉ 𝒟 P› ‹tF t1› ‹t2 ∈ 𝒟⇩m⇩i⇩n Q›
      by (blast dest: D⇩m⇩i⇩n_Interrupt_subset[THEN set_mp])
    thus ‹a ∈ α⇩m⇩i⇩n(P) ∪ α⇩m⇩i⇩n(Q)›
    proof cases
      from ‹ev a ∈ set t› show ‹t ∈ 𝒟⇩m⇩i⇩n P ⟹ a ∈ α⇩m⇩i⇩n(P) ∪ α⇩m⇩i⇩n(Q)›
        by (simp add: minimal_events_of_memI(2))
    next
      fix t1 t2 assume ‹t = t1 @ t2› ‹t1 ∈ 𝒯 P› ‹t1 ∉ 𝒟 P› ‹tF t1› ‹t2 ∈ 𝒟⇩m⇩i⇩n Q›
      with ‹ev a ∈ set t› show ‹a ∈ α⇩m⇩i⇩n(P) ∪ α⇩m⇩i⇩n(Q)›
        by (auto intro: Un_iff minimal_events_of_memI)
    qed
  qed
qed


lemma minimal_events_of_Throw_subset :
  ‹α⇩m⇩i⇩n(P Θ a ∈ A. Q a) ⊆ α⇩m⇩i⇩n(P) ∪ (⋃a ∈ A ∩ α⇩m⇩i⇩n(P). α⇩m⇩i⇩n(Q a))›
  (is ‹α⇩m⇩i⇩n(?P) ⊆ ?rhs›)
proof (rule subsetI)
  fix a assume ‹a ∈ α⇩m⇩i⇩n(?P)›
  then consider t where ‹t ∈ 𝒟⇩m⇩i⇩n ?P› ‹ev a ∈ set t›
    | t where ‹t ∈ 𝒯 ?P - 𝒟 ?P› ‹ev a ∈ set t›
    by (blast dest: minimal_events_of_memD)
  thus ‹a ∈ ?rhs›
  proof cases
    fix t assume ‹t ∈ 𝒟⇩m⇩i⇩n ?P› ‹ev a ∈ set t›
    from this(1) consider ‹t ∈ 𝒟⇩m⇩i⇩n P›
      | (D_Q) t1 b t2 where ‹t = t1 @ ev b # t2› ‹t1 @ [ev b] ∈ 𝒯 P› ‹t1 ∉ 𝒟 P›
        ‹set t1 ∩ ev ` A = {}› ‹b ∈ A› ‹t2 ∈ 𝒟⇩m⇩i⇩n (Q b)›
      by (blast dest: D⇩m⇩i⇩n_Throw_subset[THEN set_mp])
    thus ‹a ∈ ?rhs›
    proof cases
      from ‹ev a ∈ set t› show ‹t ∈ 𝒟⇩m⇩i⇩n P ⟹ a ∈ ?rhs›
        by (simp add: minimal_events_of_memI(2))
    next
      case D_Q
      have ‹t1 @ [ev b] ∈ 𝒟⇩m⇩i⇩n P ∪ (𝒯 P - 𝒟 P)›
        by (metis D_Q(2, 3) UnCI min_elems3 DiffI)
      from mem_D⇩m⇩i⇩n_Un_T_Diff_D_imp_set_subset[OF this] D_Q(2)[THEN T_imp_ftF]
      have ‹set (t1 @ [ev b]) ⊆ ev ` α⇩m⇩i⇩n(P)›
        by (auto simp add: ftF_append_iff tickFree_def disjoint_iff)
      with ‹ev a ∈ set t› D_Q(1, 5, 6) show ‹a ∈ ?rhs›
        by (auto intro: minimal_events_of_memI)
    qed
  next
    fix t assume ‹t ∈ 𝒯 ?P - 𝒟 ?P› ‹ev a ∈ set t›
    from this(1) consider (T_P) ‹t ∈ 𝒯 P› ‹set t ∩ ev ` A = {}›
      | (T_Q) t1 b t2 where ‹t = t1 @ ev b # t2› ‹t1 @ [ev b] ∈ 𝒯 P›
        ‹set t1 ∩ ev ` A = {}› ‹b ∈ A› ‹t2 ∈ 𝒯 (Q b)›
      by (auto simp add: Throw_projs)
    thus ‹a ∈ ?rhs›
    proof cases
      case T_P
      from T_P(1)[THEN T_imp_ftF] T_P(2) ‹t ∈ 𝒯 ?P - 𝒟 ?P› have ‹t ∉ 𝒟 P›
        by (elim ftF_E, simp_all add: D_Throw)
          (fastforce, metis ftF_single is_processT9)
      with T_P(1) ‹ev a ∈ set t› show ‹a ∈ ?rhs›
        by (simp add: minimal_events_of_memI(1))
    next
      case T_Q
      with ‹t ∈ 𝒯 ?P - 𝒟 ?P› have ‹t1 @ [ev b] ∈ 𝒟⇩m⇩i⇩n P ∪ (𝒯 P - 𝒟 P)›
        by (simp add: Throw_projs)
          (metis T_imp_ftF event⇩p⇩t⇩i⇩c⇩k.disc(1) not_Cons_self2
            ftF_Cons_iff ftF_nonempty_append_imp min_elems3)
      from mem_D⇩m⇩i⇩n_Un_T_Diff_D_imp_set_subset[OF this] T_Q(2)[THEN T_imp_ftF]
      have ‹set (t1 @ [ev b]) ⊆ ev ` α⇩m⇩i⇩n(P)›
        by (auto simp add: ftF_append_iff tickFree_def disjoint_iff)
      from T_Q(1-4) ‹t ∈ 𝒯 ?P - 𝒟 ?P› have ‹t2 ∉ 𝒟 (Q b)›
        by (simp add: D_Throw)
      with T_Q(5) have ‹set t2 ⊆ ev ` α⇩m⇩i⇩n(Q b) ∪ tick ` ❙✓❙s(Q b)›
        by (simp add: mem_D⇩m⇩i⇩n_Un_T_Diff_D_imp_set_subset)
      with ‹set (t1 @ [ev b]) ⊆ ev ` α⇩m⇩i⇩n(P)› ‹ev a ∈ set t› T_Q(1, 4)
      show ‹a ∈ ?rhs› by auto
    qed
  qed
qed




section ‹Restriction of the Events›

subsection ‹Throw›

lemma Throw_is_restrictable_on_minimal_events_of :
  ‹P Θ a ∈ A. Q a = P Θ a ∈ (A ∩ α⇩m⇩i⇩n(P)). Q a› (is ‹?lhs = ?rhs›)
proof -
  have $ : ‹t ∈ 𝒟⇩m⇩i⇩n P ∪ (𝒯 P - 𝒟 P) ⟹ set t ∩ ev ` (A ∩ α⇩m⇩i⇩n(P)) = {} ⟷ set t ∩ ev ` A = {}› for t
    by (drule mem_D⇩m⇩i⇩n_Un_T_Diff_D_imp_set_subset) blast
  show ‹?lhs = ?rhs›
  proof (rule Process_eqI_D⇩m⇩i⇩n_version)
    fix t assume ‹t ∈ 𝒟⇩m⇩i⇩n ?lhs›
    then consider (D_P) ‹t ∈ 𝒟⇩m⇩i⇩n P› ‹tF t› ‹set t ∩ ev ` A = {}›
      | (D_Q) t1 a t2 where ‹t = t1 @ ev a # t2› ‹t1 @ [ev a] ∈ 𝒯 P›
        ‹t1 ∉ 𝒟 P› ‹set t1 ∩ ev ` A = {}› ‹a ∈ A› ‹t2 ∈ 𝒟⇩m⇩i⇩n (Q a)›
      by (blast dest: D⇩m⇩i⇩n_Throw_subset[THEN set_mp])
    thus ‹t ∈ 𝒟 ?rhs›
    proof cases
      case D_P thus ‹t ∈ 𝒟 ?rhs›
        by (auto simp add: D_Throw intro: D⇩m⇩i⇩n_D ftF_Nil)
    next
      case D_Q
      have ‹t1 @ [ev a] ∈ 𝒟⇩m⇩i⇩n P ∪ (𝒯 P - 𝒟 P)›
        by (metis D_Q(2, 3) Diff_iff Un_iff min_elems3)
      from "$"[OF this] D_Q(4, 5) have ‹set t1 ∩ ev ` (A ∩ α⇩m⇩i⇩n(P)) = {}› ‹a ∈ A ∩ α⇩m⇩i⇩n(P)› by auto
      with D_Q(1, 2, 6) show ‹t ∈ 𝒟 ?rhs› by (simp add: D_Throw) (metis D⇩m⇩i⇩n_D)
    qed
  next
    fix t assume ‹t ∈ 𝒟⇩m⇩i⇩n ?rhs›
    then consider (D_P) ‹t ∈ 𝒟⇩m⇩i⇩n P› ‹tF t› ‹set t ∩ ev ` (A ∩ α⇩m⇩i⇩n(P)) = {}›
      | (D_Q) t1 a t2 where ‹t = t1 @ ev a # t2› ‹t1 @ [ev a] ∈ 𝒯 P›
        ‹t1 ∉ 𝒟 P› ‹set t1 ∩ ev ` (A ∩ α⇩m⇩i⇩n(P)) = {}› ‹a ∈ A ∩ α⇩m⇩i⇩n(P)› ‹t2 ∈ 𝒟⇩m⇩i⇩n (Q a)›
      by (blast dest: D⇩m⇩i⇩n_Throw_subset[THEN set_mp])
    thus ‹t ∈ 𝒟 ?lhs›
    proof cases
      case D_P thus ‹t ∈ 𝒟 ?lhs›
        by (auto simp add: D_Throw "$" intro: D⇩m⇩i⇩n_D ftF_Nil)
    next
      case D_Q
      have ‹t1 @ [ev a] ∈ 𝒟⇩m⇩i⇩n P ∪ (𝒯 P - 𝒟 P)›
        by (metis D_Q(2, 3) Diff_iff Un_iff min_elems3)
      from "$"[OF this] D_Q(2, 3, 4, 5) have ‹set t1 ∩ ev ` A = {}› ‹a ∈ A›
        by (auto dest: is_processT3_TR_append intro: minimal_events_of_memI(1))
      with D_Q(1, 2, 6) show ‹t ∈ 𝒟 ?lhs› by (simp add: D_Throw) (metis D⇩m⇩i⇩n_D)
    qed
  next
    fix t X assume ‹(t, X) ∈ ℱ ?lhs› ‹t ∉ 𝒟 ?lhs›
    then consider (F_P) ‹(t, X) ∈ ℱ P› ‹set t ∩ ev ` A = {}›
      | (F_Q) t1 a t2 where ‹t = t1 @ ev a # t2› ‹t1 @ [ev a] ∈ 𝒯 P›
        ‹set t1 ∩ ev ` A = {}› ‹a ∈ A› ‹(t2, X) ∈ ℱ (Q a)›
      by (auto simp add: Throw_projs)
    thus ‹(t, X) ∈ ℱ ?rhs›
    proof cases
      case F_P thus ‹(t, X) ∈ ℱ ?rhs› by (auto simp add: F_Throw)
    next
      case F_Q
      from ‹(t, X) ∈ ℱ ?lhs›[THEN F_imp_ftF] ‹t ∉ 𝒟 ?lhs› F_Q(1, 3) have ‹t1 ∉ 𝒟 P›
        by (simp add: D_Throw)
          (metis ftF_nonempty_append_imp list.distinct(1))
      hence ‹t1 @ [ev a] ∈ 𝒟⇩m⇩i⇩n P ∪ (𝒯 P - 𝒟 P)›
        by (metis F_Q(2) Un_iff min_elems3 Un_Diff_cancel)
      from "$"[OF this] F_Q(3, 4) have ‹set t1 ∩ ev ` (A ∩ α⇩m⇩i⇩n(P)) = {}› ‹a ∈ A ∩ α⇩m⇩i⇩n(P)› by auto
      with F_Q(1, 2, 5) show ‹(t, X) ∈ ℱ ?rhs› by (auto simp add: F_Throw)
    qed
  next
    fix t X assume ‹(t, X) ∈ ℱ ?rhs› ‹t ∉ 𝒟 ?rhs›
    then consider (F_P) ‹(t, X) ∈ ℱ P› ‹set t ∩ ev ` (A ∩ α⇩m⇩i⇩n(P)) = {}›
      | (F_Q) t1 a t2 where ‹t = t1 @ ev a # t2› ‹t1 @ [ev a] ∈ 𝒯 P›
        ‹set t1 ∩ ev ` (A ∩ α⇩m⇩i⇩n(P)) = {}› ‹a ∈ A ∩ α⇩m⇩i⇩n(P)› ‹(t2, X) ∈ ℱ (Q a)›
      by (auto simp add: Throw_projs)
    thus ‹(t, X) ∈ ℱ ?lhs›
    proof cases
      case F_P
      from ‹(t, X) ∈ ℱ ?rhs›[THEN F_imp_ftF] ‹t ∉ 𝒟 ?rhs› F_P(2) have ‹t ∉ 𝒟 P›
        by (elim ftF_E, simp_all add: D_Throw)
          (fastforce, metis ftF_single is_processT9)
      with F_P(1) have ‹t ∈ 𝒟⇩m⇩i⇩n P ∪ (𝒯 P - 𝒟 P)› by (blast intro: F_T)
      from "$"[OF this] F_P(2) have ‹set t ∩ ev ` A = {}› by simp
      with F_P(1) show ‹(t, X) ∈ ℱ ?lhs› by (simp add: F_Throw)
    next
      case F_Q
      from ‹(t, X) ∈ ℱ ?rhs›[THEN F_imp_ftF] ‹t ∉ 𝒟 ?rhs› F_Q(1, 3) have ‹t1 ∉ 𝒟 P›
        by (simp add: D_Throw)
          (metis ftF_nonempty_append_imp list.distinct(1))
      hence ‹t1 @ [ev a] ∈ 𝒟⇩m⇩i⇩n P ∪ (𝒯 P - 𝒟 P)›
        by (metis F_Q(2) Un_iff min_elems3 Un_Diff_cancel)
      from "$"[OF this] F_Q(2, 3, 4) ‹t1 ∉ 𝒟 P› have ‹set t1 ∩ ev ` A = {}› ‹a ∈ A›
        by (auto dest: is_processT3_TR_append intro: minimal_events_of_memI(1))
      with F_Q(1, 2, 5) show ‹(t, X) ∈ ℱ ?lhs› by (auto simp add: F_Throw)
    qed
  qed
qed

corollary Throw_is_restrictable_on_superset_minimal_events_of :
  ‹α⇩m⇩i⇩n(P) ⊆ A ⟹ P Θ a ∈ S. Q a = P Θ a ∈ (S ∩ A). Q a›
  by (metis Throw_is_restrictable_on_minimal_events_of inf.absorb_iff2 inf_assoc)

corollary Throw_disjoint_minimal_events_of: ‹A ∩ α⇩m⇩i⇩n(P) = {} ⟹ P Θ a ∈ A. Q a = P›
  by (metis Throw_empty_set Throw_is_restrictable_on_minimal_events_of)





(*<*)
end
  (*>*)