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›

definition distinct_mset :: ‹'a multiset ⇒ bool›
  where ‹distinct_mset M ≡ ∀m ∈# M. ∀n ∈# M - {#m#}. m ≠ n›

lemma distinct_mset_iff_count :
  ‹distinct_mset M ⟷ (∀m ∈# M. count M m = 1)›
  unfolding distinct_mset_def
  by (induct M, simp_all, metis not_in_iff)

lemma distinct_mset_iff_mset_distinct :
  ‹distinct_mset M ⟷ (∀L. M = mset L ⟶ distinct L)›
  by (metis count_mset_0_iff distinct_count_atmost_1 distinct_mset_iff_count ex_mset set_mset_mset)

lemma distinct_mset_iff_mset_set :
  ‹distinct_mset M ⟷ (∃S. finite S ∧ M = mset_set S)›
  by (metis count_mset_set(1) distinct_mset_iff_count distinct_mset_iff_mset_distinct
            ex_mset finite_set_mset finite_set_mset_mset_set mset_set_set set_mset_mset)



lemma MultiSync_Mprefix_subset :
  ‹(⋀m. m ∈# M ⟹ A m ⊆ S) ⟹
   (❙⟦S❙⟧ m ∈# M. □a ∈ A m → P m a) = (if M = {#} then STOP else
   □a ∈ (⋂m ∈ set_mset M. A m) → (❙⟦S❙⟧ m ∈# M. P m a))›
proof (induct M rule: induct_subset_mset_empty_single)
  case 1 show ?case by simp
next
  case (2 m) show ?case by simp
next
  case (3 M m)
  have ‹❙⟦S❙⟧ m∈#add_mset m M. Mprefix (A m) (P m) =
        Mprefix (A m) (P m) ⟦S⟧ ❙⟦S❙⟧ m'∈# M. Mprefix (A m') (P m')›
    by (simp add: ‹M ≠ {#}›)
  also have ‹… = Mprefix (A m) (P m) ⟦S⟧ □a ∈ (⋂m' ∈ set_mset M. A m') → (❙⟦S❙⟧ n ∈# M. P n a)›
    by (simp add: "3.hyps"(3, 4) "3.prems")
  also have ‹… = □a∈(⋂ (A ` set_mset (add_mset m M))) → (P m a ⟦S⟧ ❙⟦S❙⟧ n∈#M. P n a)›
    by (subst Mprefix_Sync_Mprefix_subset, simp_all add: "3.prems")
      (metis "3.hyps"(3) "3.prems" INF_lower2 insertI2 multiset_nonemptyE set_mset_add_mset_insert)
  also have ‹… = □a∈(⋂ (A ` set_mset (add_mset m M))) → (❙⟦S❙⟧ n∈#add_mset m M. P n a)›
    by (simp add: ‹M ≠ {#}›)
  finally show ?case by simp
qed


lemmas MultiPar_Mprefix_subset = MultiSync_Mprefix_subset[where S = UNIV, simplified]


lemma MultiSync_Mprefix_indep :
  ‹⟦finite M; ⋀m. m ∈ M ⟹ A m ∩ S = {}⟧ ⟹
   ❙⟦S❙⟧ m ∈# mset_set M. □a ∈ (A m) → P m a =
   □a ∈ (⋃m ∈ M. A m) → ⊓m ∈ {m ∈ M. a ∈ A m}. (❙⟦S❙⟧ n ∈# mset_set M. (if n = m then P m a else □b ∈ (A n) → P n b))›
proof (induct M rule: induct_subset_empty_single)
  case 1 show ?case by simp
next
  case (2 m)
  have ‹a ∈ A m ⟹ {n. n = m ∧ a ∈ A n} = {m}› for a by auto 
  thus ?case by (auto intro: mono_Mprefix_eq)
next
  case (3 M m)
  let ?f = ‹λn m x. if n = m then P m x else □a ∈ (A n) → P n a›
  have * : ‹mset_set (insert m M) = add_mset m (mset_set M)› ‹mset_set M ≠ {#}›
    by (simp_all add: "3"(2, 3, 5) mset_set_empty_iff)
  have ‹❙⟦S❙⟧ m∈#mset_set (insert m M). Mprefix (A m) (P m) =
         □a ∈ A m → P m a ⟦S⟧ ❙⟦S❙⟧ m∈#mset_set M. Mprefix (A m) (P m)›
    by (simp add: "*")
  also have ‹… = (□a∈A m → (P m a ⟦S⟧ □a∈⋃ (A ` M) → ⊓m'∈{m' ∈ M. a ∈ A m'}. ❙⟦S❙⟧ n∈#mset_set M. ?f n m' a)) □
                  (□b∈⋃ (A ` M) → (Mprefix (A m) (P m) ⟦S⟧ ⊓m'∈{m' ∈ M. b ∈ A m'}. ❙⟦S❙⟧ n∈#mset_set M. ?f n m' b))›
    (is ‹_ = (□a∈A m → ?rhs1 a) □ (□b∈⋃ (A ` M) → ?rhs2 b)›)
    by (subst Mprefix_Sync_Mprefix_indep[symmetric])
      (use "3"(6, 7) in ‹auto simp flip: Mprefix_Sync_Mprefix_indep›)
  also have ‹… = □x∈(⋃ (A ` insert m M)) → (if x ∈ A m ∩ ⋃ (A ` M) then ?rhs1 x ⊓ ?rhs2 x
                                            else if x ∈ A m then ?rhs1 x else ?rhs2 x)›
    by (simp add: Mprefix_Det_Mprefix)
  also have ‹… = □a∈⋃ (A ` insert m M)
                     → ⊓m'∈{m' ∈ insert m M. a ∈ A m'}. ❙⟦S❙⟧ n∈#mset_set (insert m M). ?f n m' a›
  proof (rule mono_Mprefix_eq)
    fix x assume $ : ‹x ∈ ⋃ (A ` insert m M)›
    have $$ : ‹{m' ∈ insert m M. x ∈ A m'} =
               (if x ∈ A m then insert m {m' ∈ M. x ∈ A m'} else {m' ∈ M. x ∈ A m'})› by auto
    have $$$ : ‹∀m∈M. x ∉ A m ⟹ {m' ∈ M. x ∈ A m'} = {}› by auto
    have $$$$ : ‹{m' ∈ M. x ∈ A m'} - {m} = {m' ∈ M. x ∈ A m'}› by (simp add: "3.hyps"(2))
    from "$"
    show ‹(if x ∈ A m ∩ ⋃ (A ` M) then ?rhs1 x ⊓ ?rhs2 x
           else if x ∈ A m then ?rhs1 x else ?rhs2 x) =
          ⊓m'∈{m' ∈ insert m M. x ∈ A m'}. ❙⟦S❙⟧ n∈#mset_set (insert m M). ?f n m' x›
      by (subst (1 2) "3"(6)[symmetric], use "3.prems" in blast, unfold "$$")
        (auto simp add: "$$$" "$$$$" "*"(2) "3"(2, 3)
                        GlobalNdet_distrib_unit_bis Sync_distrib_GlobalNdet_left
                intro!: mono_GlobalNdet_eq mono_MultiSync_eq
                        arg_cong[where f = ‹λP. _ ⟦S⟧ P›] arg_cong2[where f = ‹(⊓)›] )
  qed
  finally show ?case .
qed


lemmas MultiInter_Mprefix_indep = MultiSync_Mprefix_indep[where S = ‹{}›, simplified]



(*<*)
end
  (*>*)