Theory Step_CSPM_Laws

(*<*)
―‹ ********************************************************************
 * Project         : HOL-CSPM - Architectural operators for HOL-CSP
 *
 * Author          : Benoît Ballenghien, Safouan Taha, Burkhart Wolff.
 *
 * This file       : Step Laws
 *
 * 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.
 ******************************************************************************›
(*>*)

section‹ The Step-Laws ›

(*<*)
theory Step_CSPM_Laws                                            
  imports Global_Deterministic_Choice Multi_Synchronization_Product
    Multi_Sequential_Composition Interrupt Throw
begin 
  (*>*)

text ‹The step-laws describe the behaviour of the operators wrt. the multi-prefix choice.›

subsection ‹The Throw Operator›

lemma Throw_Mprefix: 
  ‹(□a ∈ A → P a) Θ b ∈ B. Q b =
    □a ∈ A → (if a ∈ B then Q a else P a Θ b ∈ B. Q b)›
  (is ‹?lhs = ?rhs›)
proof (subst Process_eq_spec_optimized, safe)
  fix s
  assume ‹s ∈ 𝒟 ?lhs›
  then consider t1 t2 where ‹s = t1 @ t2› ‹t1 ∈ 𝒟 (□a ∈ A → P a)› ‹tF t1› 
    ‹set t1 ∩ ev ` B = {}› ‹ftF t2›
  | t1 b t2 where ‹s = t1 @ ev b # t2› ‹t1 @ [ev b] ∈ 𝒯 (□a∈A → P a)›
    ‹set t1 ∩ ev ` B = {}› ‹b ∈ B› ‹t2 ∈ 𝒟 (Q b)›
    by (simp add: D_Throw) blast
  thus ‹s ∈ 𝒟 ?rhs›
  proof cases
    fix t1 t2 assume * : ‹s = t1 @ t2› ‹t1 ∈ 𝒟 (□a∈A → P a)› ‹tF t1› 
      ‹set t1 ∩ ev ` B = {}› ‹ftF t2›
    from "*"(2) obtain a t1' where ** : ‹t1 = ev a # t1'› ‹a ∈ A› ‹t1' ∈ 𝒟 (P a)›
      by (auto simp add: D_Mprefix)
    from "*"(4) "**"(1) have *** : ‹a ∉ B› by (simp add: image_iff)
    have ‹t1' @ t2 ∈ 𝒟 (Throw (P a) B Q)›
      using "*"(3, 4, 5) "**"(1, 3) by (auto simp add: D_Throw)
    with "***" show ‹s ∈ 𝒟 ?rhs›
      by (simp add: D_Mprefix "*"(1) "**"(1, 2))
  next
    fix t1 b t2 assume * : ‹s = t1 @ ev b # t2› ‹t1 @ [ev b] ∈ 𝒯 (□a∈A → P a)›
      ‹set t1 ∩ ev ` B = {}› ‹b ∈ B› ‹t2 ∈ 𝒟 (Q b)›
    show ‹s ∈ 𝒟 ?rhs›
    proof (cases ‹t1›)
      from "*"(2) show ‹t1 = [] ⟹ s ∈ 𝒟 ?rhs›
        by (simp add: D_Mprefix T_Mprefix "*"(1, 4, 5))
    next
      fix a t1'
      assume ‹t1 = a # t1'›
      then obtain a' where ‹t1 = ev a' # t1'› (* a = ev a' *)
        by (metis "*"(2) append_Cons append_Nil append_T_imp_tickFree
            event⇩p⇩t⇩i⇩c⇩k.exhaust non_tickFree_tick not_Cons_self tickFree_append_iff)
      with "*"(2, 3, 4, 5) show ‹s ∈ 𝒟 ?rhs›
        by (auto simp add: "*"(1) D_Mprefix T_Mprefix D_Throw)
    qed
  qed
next
  fix s
  assume ‹s ∈ 𝒟 ?rhs›
  then obtain a s' where * : ‹a ∈ A› ‹s = ev a # s'›
    ‹s' ∈ 𝒟 (if a ∈ B then Q a else Throw (P a) B Q)› 
    by (auto simp add: D_Mprefix)
  show ‹s ∈ 𝒟 ?lhs›
  proof (cases ‹a ∈ B›)
    assume ‹a ∈ B›
    hence ** :  ‹[] @ [ev a] ∈ 𝒯 (□a∈A → P a) ∧ set [] ∩ ev ` B = {} ∧ s' ∈ 𝒟 (Q a)›
      using "*"(3) by (simp add: T_Mprefix "*"(1))
    show ‹s ∈ 𝒟 ?lhs› 
      by (simp add: D_Throw) (metis "*"(2) "**" ‹a ∈ B› append_Nil)
  next
    assume ‹a ∉ B›
    with "*"(2, 3)
    consider t1 t2 where ‹s = ev a # t1 @ t2› ‹t1 ∈ 𝒟 (P a)› ‹tF t1›
      ‹set t1 ∩ ev ` B = {}› ‹ftF t2›
    | t1 b t2 where ‹s = ev a # t1 @ ev b # t2› ‹t1 @ [ev b] ∈ 𝒯 (P a)›
      ‹set t1 ∩ ev ` B = {}› ‹b ∈ B› ‹t2 ∈ 𝒟 (Q b)›
      by (simp add: D_Throw) blast
    thus ‹s ∈ 𝒟 ?lhs›
    proof cases
      fix t1 t2 assume ** : ‹s = ev a # t1 @ t2› ‹t1 ∈ 𝒟 (P a)› ‹tF t1›
        ‹set t1 ∩ ev ` B = {}› ‹ftF t2›
      have *** : ‹ev a # t1 ∈ 𝒟 (□a∈A → P a) ∧ tickFree (ev a # t1) ∧
                  set (ev a # t1) ∩ ev ` B = {}›
        by (simp add: D_Mprefix image_iff "*"(1) "**"(2, 3, 4) ‹a ∉ B›)
      show ‹s ∈ 𝒟 ?lhs›
        by (simp add: D_Throw) (metis "**"(1, 5) "***" append_Cons)
    next
      fix t1 b t2
      assume ** :  ‹s = ev a # t1 @ ev b # t2› ‹t1 @ [ev b] ∈ 𝒯 (P a)›
        ‹set t1 ∩ ev ` B = {}› ‹b ∈ B› ‹t2 ∈ 𝒟 (Q b)›
      have *** : ‹(ev a # t1) @ [ev b] ∈ 𝒯 (□a∈A → P a) ∧ set (ev a # t1) ∩ ev ` B = {}›
        by (simp add: T_Mprefix image_iff "*"(1) "**"(2, 3) ‹a ∉ B›)
      show ‹s ∈ 𝒟 ?lhs›
        by (simp add: D_Throw) (metis "**"(1, 4, 5) "***" append_Cons)
    qed
  qed
next
  fix s X
  assume same_div : ‹𝒟 ?lhs = 𝒟 ?rhs›
  assume ‹(s, X) ∈ ℱ ?lhs›
  then consider ‹(s, X) ∈ ℱ (□a∈A → P a)› ‹set s ∩ ev ` B = {}›
    | ‹s ∈ 𝒟 ?lhs›
    | t1 b t2 where ‹s = t1 @ ev b # t2› ‹t1 @ [ev b] ∈ 𝒯 (□a∈A → P a)›
      ‹set t1 ∩ ev ` B = {}› ‹b ∈ B› ‹(t2, X) ∈ ℱ (Q b)›
    by (simp add: F_Throw D_Throw) blast
  thus ‹(s, X) ∈ ℱ ?rhs›
  proof cases
    show ‹(s, X) ∈ ℱ (□a∈A → P a) ⟹ set s ∩ ev ` B = {} ⟹ (s, X) ∈ ℱ ?rhs›
      by (simp add: F_Mprefix F_Throw)
        (metis image_eqI insert_disjoint(1) list.simps(15))
  next
    show ‹s ∈ 𝒟 ?lhs ⟹ (s, X) ∈ ℱ ?rhs›
      using same_div D_F by blast
  next
    fix t1 b t2 assume * : ‹s = t1 @ ev b # t2› ‹t1 @ [ev b] ∈ 𝒯 (□a∈A → P a)›
      ‹set t1 ∩ ev ` B = {}› ‹b ∈ B› ‹(t2, X) ∈ ℱ (Q b)›
    show ‹(s, X) ∈ ℱ ?rhs›
    proof (cases t1) 
      from "*"(2) show ‹t1 = [] ⟹ (s, X) ∈ ℱ ?rhs›
        by (auto simp add: F_Mprefix T_Mprefix F_Throw "*"(1, 4, 5))
    next
      fix a t1'
      assume ‹t1 = a # t1'›
      then obtain a' where ‹t1 = ev a' # t1'› (* a = ev a' *)
        by (metis "*"(2) append_Cons append_Nil append_T_imp_tickFree
            event⇩p⇩t⇩i⇩c⇩k.exhaust non_tickFree_tick not_Cons_self tickFree_append_iff)
      with "*"(2, 3, 5) show ‹(s, X) ∈ ℱ ?rhs›
        by (auto simp add: F_Mprefix T_Mprefix F_Throw "*"(1, 4))
    qed
  qed
next
  show ‹(s, X) ∈ ℱ ?rhs ⟹ (s, X) ∈ ℱ ?lhs› for s X
  proof (cases s)
    show ‹s = [] ⟹ (s, X) ∈ ℱ ?rhs ⟹ (s, X) ∈ ℱ ?lhs›
      by (simp add: F_Mprefix F_Throw)
  next
    fix a s'
    assume assms : ‹s = a # s'› ‹(s, X) ∈ ℱ ?rhs›
    from assms(2) obtain a'
      where * : ‹a' ∈ A› ‹s = ev a' # s'›
        ‹(s', X) ∈ ℱ (if a' ∈ B then Q a' else Throw (P a') B Q)›
      by (simp add: assms(1) F_Mprefix) blast
    show ‹(s, X) ∈ ℱ ?lhs›
    proof (cases ‹a' ∈ B›) 
      assume ‹a' ∈ B›
      hence ** : ‹[] @ [ev a'] ∈ 𝒯 (□a∈A → P a) ∧
                 set [] ∩ ev ` B = {} ∧ (s', X) ∈ ℱ (Q a')›
        using "*"(3) by (simp add: T_Mprefix "*"(1))
      show ‹(s, X) ∈ ℱ ?lhs›
        by (simp add: F_Throw) (metis "*"(2) "**" ‹a' ∈ B› append_Nil)
    next
      assume ‹a' ∉ B›
      then consider  ‹(s', X) ∈ ℱ (P a')› ‹set s' ∩ ev ` B = {}›
        | t1 t2   where ‹s' = t1 @ t2› ‹t1 ∈ 𝒟 (P a')› ‹tF t1›
          ‹set t1 ∩ ev ` B = {}› ‹ftF t2›
        | t1 b t2 where ‹s' = t1 @ ev b # t2› ‹t1 @ [ev b] ∈ 𝒯 (P a')›
          ‹set t1 ∩ ev ` B = {}› ‹b ∈ B› ‹(t2, X) ∈ ℱ (Q b)›
        using "*"(3) by (simp add: F_Throw D_Throw) blast
      thus ‹(s, X) ∈ ℱ ?lhs›
      proof cases
        show ‹(s', X) ∈ ℱ (P a') ⟹ set s' ∩ ev ` B = {} ⟹ (s, X) ∈ ℱ ?lhs›
          by (simp add: F_Mprefix F_Throw "*"(1, 2) ‹a' ∉ B› image_iff)
      next
        fix t1 t2 assume ** : ‹s' = t1 @ t2› ‹t1 ∈ 𝒟 (P a')› ‹tF t1›
          ‹set t1 ∩ ev ` B = {}› ‹ftF t2›
        have *** : ‹s = (ev a' # t1) @ t2 ∧ ev a' # t1 ∈ 𝒟 (□a∈A → P a) ∧
                    tickFree (ev a' # t1) ∧ set (ev a' # t1) ∩ ev ` B = {}›
          by (simp add: D_Mprefix ‹a' ∉ B› image_iff "*"(1, 2) "**"(1, 2, 3, 4))
        show ‹(s, X) ∈ ℱ ?lhs›
          by (simp add: F_Throw F_Mprefix) (metis "**"(5) "***")
      next
        fix t1 b t2
        assume ** : ‹s' = t1 @ ev b # t2› ‹t1 @ [ev b] ∈ 𝒯 (P a')›
          ‹set t1 ∩ ev ` B = {}› ‹b ∈ B› ‹(t2, X) ∈ ℱ (Q b)›
        have *** : ‹s = (ev a' # t1) @ ev b # t2 ∧ set (ev a' # t1) ∩ ev ` B = {} ∧
                    (ev a' # t1) @ [ev b] ∈ 𝒯 (□a∈A → P a)›
          by (simp add: T_Mprefix ‹a' ∉ B› image_iff "*"(1, 2) "**"(1, 2, 3))
        show ‹(s, X) ∈ ℱ ?lhs›
          by (simp add: F_Throw F_Mprefix) (metis "**"(4, 5) "***")
      qed
    qed
  qed
qed



subsection ‹The Interrupt Operator›

lemma Interrupt_Mprefix:
  ‹(□a ∈ A → P a) △ Q = Q □ (□a ∈ A → P a △ Q)› (is ‹?lhs = ?rhs›)
proof (subst Process_eq_spec_optimized, safe)
  fix s
  assume ‹s ∈ 𝒟 ?lhs›
  then consider ‹s ∈ 𝒟 (□a ∈ A → P a)›
    | ‹∃t1 t2. s = t1 @ t2 ∧ t1 ∈ 𝒯 (□a ∈ A → P a) ∧ tF t1 ∧ t2 ∈ 𝒟 Q›
    by (simp add: D_Interrupt) blast
  thus ‹s ∈ 𝒟 ?rhs›
  proof cases
    show ‹s ∈ 𝒟 (□a ∈ A → P a) ⟹ s ∈ 𝒟 ?rhs›
      by (auto simp add: D_Det D_Mprefix D_Interrupt)
  next
    assume ‹∃t1 t2. s = t1 @ t2 ∧ t1 ∈ 𝒯 (□a ∈ A → P a) ∧ tF t1 ∧ t2 ∈ 𝒟 Q›
    then obtain t1 t2
      where ‹s = t1 @ t2› ‹t1 ∈ 𝒯 (□a ∈ A → P a)› ‹tF t1› ‹t2 ∈ 𝒟 Q› by blast
    thus ‹s ∈ 𝒟 ?rhs› by (fastforce simp add: D_Det Mprefix_projs D_Interrupt)
  qed
next
  fix s
  assume ‹s ∈ 𝒟 ?rhs›
  then consider ‹s ∈ 𝒟 Q› | a s' where ‹s = ev a # s'› ‹a ∈ A› ‹s' ∈ 𝒟 (P a △ Q)›
    by (auto simp add: D_Det D_Mprefix image_iff)
  thus ‹s ∈ 𝒟 ?lhs›
  proof cases
    show ‹s ∈ 𝒟 Q ⟹ s ∈ 𝒟 ?lhs›
      by (simp add: D_Interrupt) (use Nil_elem_T tickFree_Nil in blast)
  next
    fix a s' assume ‹s = ev a # s'› ‹a ∈ A› ‹s' ∈ 𝒟 (P a △ Q)›
    from this(3) consider ‹s' ∈ 𝒟 (P a)›
      | t1 t2 where ‹s' = t1 @ t2› ‹t1 ∈ 𝒯 (P a)› ‹tF t1› ‹t2 ∈ 𝒟 Q›
      by (auto simp add: D_Interrupt)
    thus ‹s ∈ 𝒟 ?lhs›
    proof cases
      show ‹s' ∈ 𝒟 (P a) ⟹ s ∈ 𝒟 ?lhs›
        by (simp add: D_Interrupt D_Mprefix ‹a ∈ A› ‹s = ev a # s'›)
    next
      show ‹⟦s' = t1 @ t2; t1 ∈ 𝒯 (P a); tF t1; t2 ∈ 𝒟 Q⟧ ⟹ s ∈ 𝒟 ?lhs› for t1 t2
        by (simp add: ‹s = ev a # s'› D_Interrupt T_Mprefix)
          (metis Cons_eq_appendI ‹a ∈ A› event⇩p⇩t⇩i⇩c⇩k.disc(1) tickFree_Cons_iff)
    qed
  qed
next
  fix s X
  assume same_div : ‹𝒟 ?lhs = 𝒟 ?rhs›
  assume ‹(s, X) ∈ ℱ ?lhs›
  then consider ‹s ∈ 𝒟 ?lhs› 
    | t1 r where ‹s = t1 @ [✓(r)]› ‹t1 @ [✓(r)] ∈ 𝒯 (Mprefix A P)›
    | r where ‹s @ [✓(r)] ∈ 𝒯 (Mprefix A P)› ‹✓(r) ∉ X›
    | ‹(s, X) ∈ ℱ (Mprefix A P)› ‹tickFree s› ‹([], X) ∈ ℱ Q›
    | t1 t2 where ‹s = t1 @ t2› ‹t1 ∈ 𝒯 (Mprefix A P)› ‹tickFree t1› ‹(t2, X) ∈ ℱ Q› ‹t2 ≠ []›
    | r where ‹s ∈ 𝒯 (Mprefix A P)› ‹tickFree s› ‹[✓(r)] ∈ 𝒯 Q› ‹✓(r) ∉ X›
    by (simp add: F_Interrupt D_Interrupt) blast
  thus ‹(s, X) ∈ ℱ ?rhs›
  proof cases
    from D_F same_div show ‹s ∈ 𝒟 ?lhs ⟹ (s, X) ∈ ℱ ?rhs› by blast
  next
    show ‹s = t1 @ [✓(r)] ⟹ t1 @ [✓(r)] ∈ 𝒯 (Mprefix A P) ⟹ (s, X) ∈ ℱ ?rhs› for t1 r
      by (simp add: F_Det T_Mprefix F_Mprefix F_Interrupt image_iff)
        (metis append_Nil event⇩p⇩t⇩i⇩c⇩k.distinct(1) list.inject list.sel(3) tl_append2)
  next
    show ‹s @ [✓(r)] ∈ 𝒯 (Mprefix A P) ⟹ ✓(r) ∉ X ⟹ (s, X) ∈ ℱ ?rhs› for r
      by (simp add: F_Det T_Mprefix F_Mprefix F_Interrupt image_iff)
        (metis (no_types, opaque_lifting) Diff_insert_absorb append_Nil
          event⇩p⇩t⇩i⇩c⇩k.distinct(1) hd_append2 list.sel(1, 3) neq_Nil_conv tl_append2)
  next
    show ‹(s, X) ∈ ℱ (Mprefix A P) ⟹ tickFree s ⟹ ([], X) ∈ ℱ Q ⟹ (s, X) ∈ ℱ ?rhs›
      by (simp add: F_Det F_Mprefix F_Interrupt image_iff) (metis tickFree_Cons_iff)
  next
    show ‹s = t1 @ t2 ⟹ t1 ∈ 𝒯 (Mprefix A P) ⟹ tickFree t1 ⟹ (t2, X) ∈ ℱ Q ⟹
          t2 ≠ [] ⟹ (s, X) ∈ ℱ ?rhs› for t1 t2
      by (simp add: F_Det T_Mprefix F_Mprefix F_Interrupt image_iff)
        (metis append_Cons append_Nil tickFree_Cons_iff)
  next
    show ‹s ∈ 𝒯 (Mprefix A P) ⟹ tickFree s ⟹ [✓(r)] ∈ 𝒯 Q ⟹
          ✓(r) ∉ X ⟹ (s, X) ∈ ℱ ?rhs› for r
      by (simp add: F_Det T_Mprefix F_Mprefix F_Interrupt image_iff)
        (metis Diff_insert_absorb tickFree_Cons_iff)
  qed
next
  fix s X
  assume same_div : ‹𝒟 ?lhs = 𝒟 ?rhs›
  assume assm : ‹(s, X) ∈ ℱ ?rhs›
  show ‹(s, X) ∈ ℱ ?lhs›
  proof (cases ‹s = []›)
    from assm show ‹s = [] ⟹ (s, X) ∈ ℱ ?lhs›
      by (simp add: F_Det F_Mprefix F_Interrupt) blast
  next 
    assume ‹s ≠ []›
    with assm consider ‹(s, X) ∈ ℱ Q›
      | ‹∃a s'. s = ev a # s' ∧ a ∈ A ∧ (s', X) ∈ ℱ (P a △ Q)›
      by (auto simp add: F_Det F_Mprefix image_iff)
    thus ‹(s, X) ∈ ℱ ?lhs›
    proof cases
      show ‹(s, X) ∈ ℱ Q ⟹ (s, X) ∈ ℱ ?lhs›
        by (simp add: F_Interrupt)
          (metis Nil_elem_T ‹s ≠ []› append_Nil tickFree_Nil)
    next
      assume ‹∃a s'. s = ev a # s' ∧ a ∈ A ∧ (s', X) ∈ ℱ (P a △ Q)›
      then obtain a s'
        where * : ‹s = ev a # s'› ‹a ∈ A› ‹(s', X) ∈ ℱ (P a △ Q)› by blast
      from "*"(3) consider ‹s' ∈ 𝒟 (P a △ Q)›
        | t1 r where ‹s' = t1 @ [✓(r)]› ‹t1 @ [✓(r)] ∈ 𝒯 (P a)›
        | r where ‹s' @ [✓(r)] ∈ 𝒯 (P a)› ‹✓(r) ∉ X›
        | ‹(s', X) ∈ ℱ (P a)› ‹tickFree s'› ‹([], X) ∈ ℱ Q›
        | t1 t2 where ‹s' = t1 @ t2› ‹t1 ∈ 𝒯 (P a)› ‹tickFree t1› ‹(t2, X) ∈ ℱ Q› ‹t2 ≠ []›
        | r where ‹s' ∈ 𝒯 (P a)› ‹tickFree s'› ‹[✓(r)] ∈ 𝒯 Q› ‹✓(r) ∉ X›
        by (simp add: F_Interrupt D_Interrupt) blast
      thus ‹(s, X) ∈ ℱ ?lhs›
      proof cases
        assume ‹s' ∈ 𝒟 (P a △ Q)›
        hence ‹s ∈ 𝒟 ?lhs›
          apply (simp add: D_Interrupt D_Mprefix T_Mprefix "*"(1, 2) image_iff)
          apply (elim disjE exE conjE; simp)
          by (metis "*"(2) Cons_eq_appendI event⇩p⇩t⇩i⇩c⇩k.disc(1) tickFree_Cons_iff)
        with D_F same_div show ‹(s, X) ∈ ℱ ?lhs› by blast 
      next
        show ‹s' = t1 @ [✓(r)] ⟹ t1 @ [✓(r)] ∈ 𝒯 (P a) ⟹ (s, X) ∈ ℱ ?lhs› for t1 r
          by (simp add: "*"(1, 2) F_Interrupt T_Mprefix)
      next
        show ‹s' @ [✓(r)] ∈ 𝒯 (P a) ⟹ ✓(r) ∉ X ⟹ (s, X) ∈ ℱ ?lhs› for r
          by (simp add: "*"(1, 2) F_Interrupt T_Mprefix) blast
      next
        show ‹(s', X) ∈ ℱ (P a) ⟹ tickFree s' ⟹ ([], X) ∈ ℱ Q ⟹ (s, X) ∈ ℱ ?lhs›
          by (simp add: "*"(1, 2) F_Interrupt F_Mprefix image_iff)
      next
        show ‹s' = t1 @ t2 ⟹ t1 ∈ 𝒯 (P a) ⟹ tickFree t1 ⟹ (t2, X) ∈ ℱ Q ⟹
              t2 ≠ [] ⟹ (s, X) ∈ ℱ ?lhs› for t1 t2
          apply (simp add: F_Interrupt T_Mprefix "*"(1))
          by (metis (no_types, lifting) "*"(1, 2) Cons_eq_appendI F_imp_front_tickFree
              append_is_Nil_conv assm front_tickFree_Cons_iff tickFree_Cons_iff)
      next
        show ‹s' ∈ 𝒯 (P a) ⟹ tickFree s' ⟹ [✓(r)] ∈ 𝒯 Q ⟹ ✓(r) ∉ X ⟹ (s, X) ∈ ℱ ?lhs› for r
          by (simp add: F_Interrupt T_Mprefix "*"(1, 2) image_iff) blast
      qed
    qed
  qed
qed



subsection ‹Global Deterministic Choice›

lemma GlobalDet_Mprefix :
  ‹(□a ∈ A. □b ∈ B a → P a b) =
   □b ∈ (⋃a ∈ A. B a) → ⊓a ∈ {a ∈ A. b ∈ B a}. P a b› (is ‹?lhs = ?rhs›)
proof (subst Process_eq_spec, safe)
  show ‹s ∈ 𝒟 ?lhs ⟹ s ∈ 𝒟 ?rhs›
    and ‹s ∈ 𝒟 ?rhs ⟹ s ∈ 𝒟 ?lhs› for s
    by (auto simp add: D_Mprefix D_GlobalDet D_GlobalNdet)
next
  show ‹(s, X) ∈ ℱ ?lhs ⟹ (s, X) ∈ ℱ ?rhs› for s X
    by (simp add: F_Mprefix F_GlobalDet F_GlobalNdet D_Mprefix) blast
next
  show ‹(s, X) ∈ ℱ ?rhs ⟹ (s, X) ∈ ℱ ?lhs› for s X
    by (auto simp add: F_Mprefix F_GlobalDet F_GlobalNdet split: if_split_asm)
qed



subsection ‹Multiple Synchronization Product›

lemma MultiSync_Mprefix_pseudo_distrib:
  ‹(❙⟦S❙⟧ B ∈# M. □ x ∈ B → P B x) =
   □ x ∈ (⋂B ∈ set_mset M. B) → (❙⟦S❙⟧ B ∈# M. P B x)›
  if nonempty: ‹M ≠ {#}› and hyp: ‹⋀B. B ∈# M ⟹ B ⊆ S›
proof-
  from nonempty obtain b M' where ‹b ∈# M - M'›
    ‹ M = add_mset b M'› ‹M' ⊆# M›
    by (metis add_diff_cancel_left' diff_subset_eq_self insert_DiffM
        insert_DiffM2 multi_member_last multiset_nonemptyE)
  show ?thesis
    apply (subst (1 2 3) ‹M = add_mset b M'›)
    using ‹b ∈# M - M'› ‹M' ⊆# M›
  proof (induct rule: msubset_induct_singleton')
    case m_singleton show ?case by fastforce
  next
    case (add x F) show ?case
      apply (simp, subst Mprefix_Sync_Mprefix_subset[symmetric])
      apply (meson add.hyps(1) hyp in_diffD,
          metis ‹b ∈# M - M'› hyp in_diffD le_infI1)
      using add.hyps(3) by fastforce
  qed
qed


lemmas MultiPar_Mprefix_pseudo_distrib =
  MultiSync_Mprefix_pseudo_distrib[where S = ‹UNIV›, simplified]





(*<*)
end
  (*>*)