Theory CSPM

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

theory CSPM
  imports MultiDet MultiNdet MultiSync MultiSeq GlobalNdet "HOL-CSP.Assertions"
begin

text ‹From the binary laws of \<^session>‹HOL-CSP›, we immediately obtain refinement results
      and lemmas about the combination of multi-operators.›

section ‹Refinements Results›

lemma mono_MultiDet_F:
  ‹finite A ⟹ ∀x ∈ A. P x ⊑⇩F Q x ⟹ MultiDet A P ⊑⇩F MultiDet A Q›
  apply (induct A rule: induct_subset_empty_single; simp)
  oops


lemma mono_MultiDet_D[simp, elim]:
  ‹finite A ⟹ ∀x ∈ A. P x ⊑⇩D Q x ⟹ MultiDet A P ⊑⇩D MultiDet A Q›
  and mono_MultiDet_T[simp, elim]:
  ‹finite A ⟹ ∀x ∈ A. P x ⊑⇩T Q x ⟹ MultiDet A P ⊑⇩T MultiDet A Q›
  and mono_MultiDet_DT[simp, elim]:
  ‹finite A ⟹ ∀x ∈ A. P x ⊑⇩D⇩T Q x ⟹ MultiDet A P ⊑⇩D⇩T MultiDet A Q›
  and mono_MultiDet_FD[simp, elim]:
  ‹finite A ⟹ ∀x ∈ A. P x ⊑⇩F⇩D Q x ⟹ MultiDet A P ⊑⇩F⇩D MultiDet A Q›
  by (induct A rule: induct_subset_empty_single; simp del: MultiDet_insert)+



lemma mono_MultiNdet_F[simp, elim]:
  ‹finite A ⟹ ∀x ∈ A. P x ⊑⇩F Q x ⟹ MultiNdet A P ⊑⇩F MultiNdet A Q›
  and mono_MultiNdet_D[simp, elim]:
  ‹finite A ⟹ ∀x ∈ A. P x ⊑⇩D Q x ⟹ MultiNdet A P ⊑⇩D MultiNdet A Q›
  and mono_MultiNdet_T[simp, elim]:
  ‹finite A ⟹ ∀x ∈ A. P x ⊑⇩T Q x ⟹ MultiNdet A P ⊑⇩T MultiNdet A Q›
  and mono_MultiNdet_DT[simp, elim]:
  ‹finite A ⟹ ∀x ∈ A. P x ⊑⇩D⇩T Q x ⟹ MultiNdet A P ⊑⇩D⇩T MultiNdet A Q›
  and mono_MultiNdet_FD[simp, elim]:
  ‹finite A ⟹ ∀x ∈ A. P x ⊑⇩F⇩D Q x ⟹ MultiNdet A P ⊑⇩F⇩D MultiNdet A Q›
  by (induct A rule: induct_subset_empty_single; simp)+



lemma  mono_MultiNdet_F_single:
  ‹A ≠ {} ⟹ finite A ⟹ ∀a ∈ A. P ⊑⇩F Q a  ⟹ P ⊑⇩F MultiNdet A Q›
  and  mono_MultiNdet_D_single:
  ‹A ≠ {} ⟹ finite A ⟹ ∀a ∈ A. P ⊑⇩D Q a  ⟹ P ⊑⇩D MultiNdet A Q›
  and  mono_MultiNdet_T_single:
  ‹A ≠ {} ⟹ finite A ⟹ ∀a ∈ A. P ⊑⇩T Q a  ⟹ P ⊑⇩T MultiNdet A Q›
  and mono_MultiNdet_DT_single:
  ‹A ≠ {} ⟹ finite A ⟹ ∀a ∈ A. P ⊑⇩D⇩T Q a ⟹ P ⊑⇩D⇩T MultiNdet A Q›
  and mono_MultiNdet_FD_single:
  ‹A ≠ {} ⟹ finite A ⟹ ∀a ∈ A. P ⊑⇩F⇩D Q a ⟹ P ⊑⇩F⇩D MultiNdet A Q›
  by (subst MultiNdet_id[where A = A, symmetric], simp_all)+



lemma  
  assumes ‹A ≠ {}› and ‹finite B› and ‹A ⊆ B›
  shows   mono_MultiNdet_F_left_absorb_subset: 
          ‹∀x ∈ A. P x ⊑⇩F Q x ⟹ MultiNdet B P ⊑⇩F MultiNdet A Q›
      and  mono_MultiNdet_D_left_absorb_subset:
          ‹∀x ∈ A. P x ⊑⇩D Q x ⟹ MultiNdet B P ⊑⇩D MultiNdet A Q›
      and  mono_MultiNdet_T_left_absorb_subset:
          ‹∀x ∈ A. P x ⊑⇩T Q x ⟹ MultiNdet B P ⊑⇩T MultiNdet A Q›
      and mono_MultiNdet_FD_left_absorb_subset:
          ‹∀x ∈ A. P x ⊑⇩F⇩D Q x ⟹ MultiNdet B P ⊑⇩F⇩D MultiNdet A Q›
      and mono_MultiNdet_DT_left_absorb_subset:
          ‹∀x ∈ A. P x ⊑⇩D⇩T Q x ⟹ MultiNdet B P ⊑⇩D⇩T MultiNdet A Q›
  supply finiteA = finite_subset[OF ‹A ⊆ B› ‹finite B›]
     and B_eq = Un_absorb1[OF ‹A ⊆ B›, symmetric,
                           simplified Un_Diff_cancel[of A B, symmetric]]
     and results = Diff_cancel MultiNdet_factorization_union Un_Diff_cancel assms(1, 2)
      apply (metis mono_MultiNdet_F mono_Ndet_F_left results finiteA B_eq)
     apply (metis mono_MultiNdet_D mono_Ndet_D_left results finiteA B_eq)
    apply (metis mono_MultiNdet_T mono_Ndet_T_left results finiteA B_eq)
   apply (metis mono_MultiNdet_FD mono_Ndet_FD_left results finiteA B_eq)
  by (metis mono_MultiNdet_DT mono_Ndet_DT_left results finiteA B_eq)


corollary  mono_MultiNdet_F_left_absorb[simp]:
          ‹finite A ⟹ x ∈ A ⟹ P x ⊑⇩F Q ⟹ MultiNdet A P ⊑⇩F Q›
      and  mono_MultiNdet_D_left_absorb[simp]:
          ‹finite A ⟹ x ∈ A ⟹ P x ⊑⇩D Q ⟹ MultiNdet A P ⊑⇩D Q›
      and  mono_MultiNdet_T_left_absorb[simp]:
          ‹finite A ⟹ x ∈ A ⟹ P x ⊑⇩T Q ⟹ MultiNdet A P ⊑⇩T Q›
      and mono_MultiNdet_FD_left_absorb[simp]:
          ‹finite A ⟹ x ∈ A ⟹ P x ⊑⇩F⇩D Q ⟹ MultiNdet A P ⊑⇩F⇩D Q›
      and mono_MultiNdet_DT_left_absorb[simp]:
          ‹finite A ⟹ x ∈ A ⟹ P x ⊑⇩D⇩T Q ⟹ MultiNdet A P ⊑⇩D⇩T Q›
      apply (rule trans_F [OF mono_MultiNdet_F_left_absorb_subset
                              [where A = ‹{x}›, simplified]]; simp) 
     apply (rule trans_D [OF mono_MultiNdet_D_left_absorb_subset
                             [where A = ‹{x}›, simplified]]; simp)
    apply (rule trans_T [OF mono_MultiNdet_T_left_absorb_subset
                            [where A = ‹{x}›, simplified]]; simp)
   apply (rule trans_FD[OF mono_MultiNdet_FD_left_absorb_subset
                           [where A = ‹{x}›, simplified]]; simp)
  by (rule trans_DT[OF mono_MultiNdet_DT_left_absorb_subset
                       [where A = ‹{x}›, simplified]]; simp)



lemma  mono_MultiNdet_MultiDet_F[simp, elim]:
      ‹finite A ⟹ MultiNdet A P ⊑⇩F MultiDet A P›
  and  mono_MultiNdet_MultiDet_D[simp, elim]:
      ‹finite A ⟹ MultiNdet A P ⊑⇩D MultiDet A P›
  and  mono_MultiNdet_MultiDet_T[simp, elim]:
      ‹finite A ⟹ MultiNdet A P ⊑⇩T MultiDet A P›
  and mono_MultiNdet_MultiDet_FD[simp, elim]:
      ‹finite A ⟹ MultiNdet A P ⊑⇩F⇩D MultiDet A P›
  and mono_MultiNdet_MultiDet_DT[simp, elim]:
      ‹finite A ⟹ MultiNdet A P ⊑⇩D⇩T MultiDet A P›
  by (induct A rule: induct_subset_empty_single;
      simp del: MultiDet_insert;
      meson idem_F  mono_Ndet_F  mono_Ndet_Det_F  trans_F
            idem_D  mono_Ndet_D  mono_Ndet_Det_D  trans_D
            idem_T  mono_Ndet_T  mono_Ndet_Det_T  trans_T 
            idem_FD mono_Ndet_FD mono_Ndet_Det_FD trans_FD
            idem_DT mono_Ndet_DT mono_Ndet_Det_DT trans_DT)+


lemma mono_MultiSync_F: ‹∀x ∈# M. P x ⊑⇩F Q x ⟹ MultiSync S M P ⊑⇩F MultiSync S M Q›
 apply (induct M rule: induct_subset_mset_empty_single; simp)
  oops


lemma mono_MultiSync_D: ‹∀x ∈# M. P x ⊑⇩D Q x ⟹ MultiSync S M P ⊑⇩D MultiSync S M Q›
  apply (induct M rule: induct_subset_mset_empty_single; simp)
  oops

lemma mono_MultiSync_T: ‹∀x ∈# M. P x ⊑⇩T Q x ⟹ MultiSync S M P ⊑⇩T MultiSync S M Q›
  apply (induct M rule: induct_subset_mset_empty_single; simp)
  oops

lemma mono_MultiSync_DT[simp, elim]:
  ‹∀x ∈# M. P x ⊑⇩D⇩T Q x ⟹ MultiSync S M P ⊑⇩D⇩T MultiSync S M Q›
  and mono_MultiSync_FD[simp, elim]:
  ‹∀x ∈# M. P x ⊑⇩F⇩D Q x ⟹ MultiSync S M P ⊑⇩F⇩D MultiSync S M Q›
  by (induct M rule: induct_subset_mset_empty_single; simp)+


find_theorems name: mset name: ind
lemmas mono_MultiInter_DT[simp, elim] = mono_MultiSync_DT[where S = ‹{}›]
   and mono_MultiInter_FD[simp, elim] = mono_MultiSync_FD[where S = ‹{}›]
   and   mono_MultiPar_DT[simp, elim] = mono_MultiSync_DT[where S = ‹UNIV›]
   and   mono_MultiPar_FD[simp, elim] = mono_MultiSync_FD[where S = ‹UNIV›]



lemma mono_MultiSeq_F:
  ‹∀x ∈ set L. P x ⊑⇩F Q x ⟹ MultiSeq L P ⊑⇩F MultiSeq L Q›
  apply (induct L, fastforce) apply simp oops
 
lemma mono_MultiSeq_D:
  ‹∀x ∈ set L. P x ⊑⇩D Q x ⟹ MultiSeq L P ⊑⇩D MultiSeq L Q›
  apply (induct L, fastforce) apply simp oops

lemma mono_MultiSeq_T:
  ‹∀x ∈ set L. P x ⊑⇩T Q x ⟹ MultiSeq L P ⊑⇩T MultiSeq L Q›
  apply (induct L, fastforce) apply simp oops

lemma mono_MultiSeq_DT[simp, elim]:
  ‹∀x ∈ set L. P x ⊑⇩D⇩T Q x ⟹ MultiSeq L P ⊑⇩D⇩T MultiSeq L Q›
  and mono_MultiSeq_FD[simp, elim]:
  ‹∀x ∈ set L. P x ⊑⇩F⇩D Q x ⟹ MultiSeq L P ⊑⇩F⇩D MultiSeq L Q›
  by (induct L) fastforce+




lemma mono_GlobalNdet[simp] : ‹GlobalNdet A P ⊑ GlobalNdet A Q›
  if ‹∀x ∈ A. P x ⊑ Q x› 
proof (cases ‹A = {}›)
  show ‹A = {} ⟹ GlobalNdet A P ⊑ GlobalNdet A Q› by simp
next
  assume ‹A ≠ {}›
  show ‹GlobalNdet A P ⊑ GlobalNdet A Q›
    unfolding le_approx_def
  proof (intro conjI impI allI subsetI)
    show ‹s ∈ 𝒟 (GlobalNdet A Q) ⟹ s ∈ 𝒟 (GlobalNdet A P)› for s
      using that[rule_format, THEN le_approx1] by (auto simp add: D_GlobalNdet ‹A ≠ {}›)
  next
    show ‹s ∉ 𝒟 (GlobalNdet A P) ⟹ ℛ⇩a (GlobalNdet A P) s = ℛ⇩a (GlobalNdet A Q) s› for s
      using that[rule_format, THEN le_approx2] 
      by (auto simp add: D_GlobalNdet Ra_def F_GlobalNdet ‹A ≠ {}›)
  next
    show ‹s ∈ min_elems (𝒟 (GlobalNdet A P)) ⟹ s ∈ 𝒯 (GlobalNdet A Q)› for s
      using that[rule_format, THEN le_approx3]
      by (simp add: D_GlobalNdet T_GlobalNdet ‹A ≠ {}› min_elems_def) blast
  qed
qed

lemma mono_GlobalNdet_F[simp, elim]:
  ‹∀x ∈ A. P x ⊑⇩F Q x ⟹ GlobalNdet A P ⊑⇩F GlobalNdet A Q›
  and mono_GlobalNdet_D[simp, elim]:
  ‹∀x ∈ A. P x ⊑⇩D Q x ⟹ GlobalNdet A P ⊑⇩D GlobalNdet A Q›
  and mono_GlobalNdet_T[simp, elim]:
  ‹∀x ∈ A. P x ⊑⇩T Q x ⟹ GlobalNdet A P ⊑⇩T GlobalNdet A Q›
  and mono_GlobalNdet_DT[simp, elim]:
  ‹∀x ∈ A. P x ⊑⇩D⇩T Q x ⟹ GlobalNdet A P ⊑⇩D⇩T GlobalNdet A Q›
  and mono_GlobalNdet_FD[simp, elim]:
  ‹∀x ∈ A. P x ⊑⇩F⇩D Q x ⟹ GlobalNdet A P ⊑⇩F⇩D GlobalNdet A Q›
  unfolding failure_refine_def divergence_refine_def trace_refine_def
    trace_divergence_refine_def failure_divergence_refine_def le_ref_def
  by (auto simp add: F_GlobalNdet D_GlobalNdet T_GlobalNdet)


lemma GlobalNdet_refine_FD_subset:
  ‹A ≠ {} ⟹ A ⊆ B ⟹ GlobalNdet B P ⊑⇩F⇩D GlobalNdet A P› 
  by (metis mono_Ndet_FD_left GlobalNdet_factorization_union
            bot.extremum_uniqueI idem_FD le_iff_sup)

lemma GlobalNdet_refine_F_subset:
  ‹A ≠ {} ⟹ A ⊆ B ⟹ GlobalNdet B P ⊑⇩F GlobalNdet A P›
  by (simp add: GlobalNdet_refine_FD_subset leFD_imp_leF)

lemma GlobalNdet_refine_FD: ‹a ∈ A ⟹ GlobalNdet A P ⊑⇩F⇩D P a› 
  using GlobalNdet_refine_FD_subset[of ‹{a}› A] by simp

lemma GlobalNdet_refine_F: ‹a ∈ A ⟹ GlobalNdet A P ⊑⇩F P a›
  by (simp add: GlobalNdet_refine_FD leFD_imp_leF)

lemma mono_GlobalNdet_FD_const:
  ‹A ≠ {} ⟹ ∀x ∈ A. P ⊑⇩F⇩D Q x ⟹ P ⊑⇩F⇩D GlobalNdet A Q›
  by (metis GlobalNdet_id mono_GlobalNdet_FD)

lemma mono_GlobalNdet_F_const:
  ‹A ≠ {} ⟹ ∀x ∈ A. P ⊑⇩F Q x ⟹ P ⊑⇩F GlobalNdet A Q›
  by (metis GlobalNdet_id mono_GlobalNdet_F)



section ‹Combination of Multi-Operators Laws›

lemma finite_Mprefix_is_MultiDet:
  ‹finite A ⟹ (□ p ∈ A → P p) = ❙□ p ∈ A. (p → P p)›
  by (induct rule: finite_induct, simp_all add: Mprefix_STOP)
     (metis Mprefix_Un_distrib Mprefix_singl insert_is_Un)

lemma finite_Mndetprefix_is_MultiNdet:
  ‹finite A ⟹ Mndetprefix A P = ⨅ p ∈ A. (p → P p)›
  by (cases ‹A = {}›, simp, rotate_tac, induct rule: finite_set_induct_nonempty)
     (simp_all add: Mndetprefix_unit Mndetprefix_distrib_unit)


lemma ‹Q □ (⨅ p ∈ {}. P p) = ⨅ p ∈ {}. (Q □ P p) ⟹ Q = STOP›
  by (simp add: Det_STOP)

lemma Det_MultiNdet_distrib:
  ‹A ≠ {} ⟹ finite A ⟹ M □ (⨅ p ∈ A. P p) = ⨅ p ∈ A. M □ P p›
  by (erule finite_set_induct_nonempty, simp_all add: Det_distrib)
 (* the nonempty hypothesis is necessary because 
     ‹M □ (⨅ p ∈ {}. P p) = M □ STOP = M› while ‹⨅ p ∈ {}. (M □ P p) = STOP› *)

lemma ‹M ⊓ (❙□ p ∈ {}. P p) = ❙□ p ∈ {}. (M ⊓ P p) ⟹ M ⊓ STOP = STOP› by simp

lemma Ndet_MultiDet_distrib:
  ‹A ≠ {} ⟹ finite A ⟹ M ⊓ (❙□ p ∈ A. P p) = ❙□ p ∈ A. M ⊓ P p›
  by (erule finite_set_induct_nonempty, simp_all add: Ndet_distrib)
  (* the nonempty hypothesis is necessary because 
     ‹M ⊓ (❙□ p ∈ {}. P p) = M ⊓ STOP› while ‹❙□ p ∈ {}. (M ⊓ P p) = STOP› *)




lemma MultiNdet_Sync_left_distrib: 
  ‹B ≠ {} ⟹ finite B ⟹ (⨅ a ∈ B. P a) ⟦S⟧ M = ⨅ a ∈ B. (P a ⟦S⟧ M)›
  by (induct rule: finite_set_induct_nonempty)
     (simp_all add: Sync_Ndet_left_distrib)

lemma MultiNdet_Sync_right_distrib:
  ‹B ≠ {} ⟹ finite B ⟹ M ⟦S⟧ MultiNdet B P = ⨅ a∈B. (M ⟦S⟧ P a)›
  by (subst Sync_commute, subst MultiNdet_Sync_left_distrib)
     (simp_all add: Sync_commute)



lemma Sync_MultiNdet_cartprod:
  ‹A ≠ {} ⟹ finite A ⟹ B ≠ {} ⟹ finite B ⟹ 
   (⨅ (s, t) ∈ A × B. (x s ⟦S⟧ y t)) = (⨅ s ∈ A. x s) ⟦S⟧ (⨅ t ∈ B. y t)›
  apply (subst MultiNdet_cartprod, assumption+)
  apply (subst MultiNdet_Sync_left_distrib, assumption+)
  apply (subst MultiNdet_Sync_right_distrib, assumption+)
  by presburger


lemmas Inter_MultiNdet_cartprod = Sync_MultiNdet_cartprod[where S = ‹{}›]
   and   Par_MultiNdet_cartprod = Sync_MultiNdet_cartprod[where S = UNIV]
 

lemmas MultiNdet_Inter_left_distrib =
       MultiNdet_Sync_left_distrib[where S = ‹{}›]
   and   MultiNdet_Par_left_distrib =
       MultiNdet_Sync_left_distrib[where S = ‹UNIV›]



lemma Seq_MultiNdet_distribR:
  ‹finite A ⟹ (⨅ p ∈ A. P p) ❙; S = (⨅ p ∈ A. (P p ❙; S))›
  by (induct A rule: finite_induct, simp add: STOP_Seq)
     (metis MultiNdet_insert' MultiNdet_rec1 Seq_Ndet_distrR)


lemma Seq_MultiNdet_distribL:
  ‹A  ≠ {} ⟹ finite A ⟹ S ❙; (⨅ p ∈ A. P p) = (⨅ p ∈ A. (S ❙; P p))›
  by (induct A rule: finite_set_induct_nonempty, simp_all add: Seq_Ndet_distrL)


lemma prefix_MultiNdet_distrib:
  ‹A ≠ {} ⟹ finite A ⟹ (a → (⨅ p ∈ A. P p) = ⨅ p ∈ A. (a → P p))›
  by (induct A rule: finite_set_induct_nonempty, simp_all add: write0_Ndet)


lemma Mndetprefix_MultiNdet_distrib:
  ‹(⊓ q ∈ B → (⨅ p ∈ A. P p q)) = ⨅ p ∈ A. ⊓ q ∈ B → P p q›
  if finB: ‹finite B› and nonemptyA: ‹A ≠ {}› and finA: ‹finite A›
proof (cases ‹B = {}›)
  case True thus ?thesis by (simp add: MultiNdet_STOP_id finA)
next
  case False thus ?thesis
  proof (insert finB, induct B rule: finite_set_induct_nonempty)
    case (singleton a)
    thus ?case
      by (simp add: Mndetprefix_unit finA prefix_MultiNdet_distrib nonemptyA)
  next  
    case (insertion x F)
    show ?case
      apply (subst Mndetprefix_Un_distrib[of ‹{x}›, simplified, OF ‹F ≠ {}›])
      apply (subst Mndetprefix_unit,
             subst prefix_MultiNdet_distrib[OF nonemptyA finA])
      apply (subst insertion.hyps(5))
      apply (subst MultiNdet_Ndet[OF finA])
      by (insert ‹F ≠ {}› ‹x ∉ F›, subst Mndetprefix_distrib_unit) force+
  qed
qed


lemma MultiDet_Mprefix:
  ‹finite A ⟹ (❙□a ∈ A. □x ∈ S a → P a x) =
                □x ∈ (⋃a ∈ A. S a) → ⨅ a ∈ {a ∈ A. x ∈ S a}. P a x›
proof (induct A rule: induct_subset_empty_single)
  case 1
  show ?case by (simp add: Mprefix_STOP)
next
  case 2
  show ?case
    by (simp, intro ballI mono_Mprefix_eq)
       (simp add: Collect_conv_if) 
next
  case (3 F a)
  show ?case
    apply (simp del: MultiDet_insert add: ‹finite F›) 
    apply (subst "3.hyps")
    apply (subst Mprefix_Det_distr)
    apply (intro mono_Mprefix_eq ballI)
    using ‹finite F› by (auto simp add: Process_eq_spec F_MultiNdet F_Ndet D_MultiNdet D_Ndet)
qed
 

lemma MultiDet_prefix_is_MultiNdet_prefix:
  ‹finite A ⟹ (❙□ p ∈ A. (a → P p)) = ⨅ p ∈ A. (a → P p)›
  by (induct A rule: induct_subset_empty_single, simp, simp)
     (metis MultiDet_insert' MultiNdet_insert' prefix_MultiNdet_distrib write0_Det_Ndet)
 

lemma prefix_MultiNdet_is_MultiDet_prefix:
  ‹A ≠ {} ⟹ finite A ⟹ (a → (⨅ p ∈ A. P p) = ❙□ p ∈ A. (a → P p))›
  by (simp add: MultiDet_prefix_is_MultiNdet_prefix prefix_MultiNdet_distrib)



lemma Mprefix_MultiNdet_distrib':
  ‹finite B ⟹ A ≠ {} ⟹ finite A ⟹ 
   (□ q ∈ B → ⨅ p ∈ A. P p q) = ❙□ p ∈ A. □ q ∈ B → P p q›
proof (induct B rule: finite_induct)
  case empty
  thus ?case by (simp add: Mprefix_STOP MultiDet_STOP_id)
next
  case (insert x F)
  show ?case
    apply (subst (1 2) Mprefix_Un_distrib[of ‹{x}› F, simplified])
    apply (subst Mprefix_singl, subst prefix_MultiNdet_distrib[OF insert.prems])
    apply (subst MultiDet_prefix_is_MultiNdet_prefix[symmetric, OF ‹finite A›])
    apply (subst insert.hyps(3)[OF insert.prems])
    apply (subst MultiDet_Det[OF ‹finite A›],
           rule mono_MultiDet_eq[OF ‹finite A›])
    by (subst Mprefix_singl) fast
qed


lemma MultiSync_Hiding_pseudo_distrib:
  ‹finite B ⟹ B ∩ S = {} ⟹ 
   (❙⟦S❙⟧ p ∈# M. ((P p) \ B)) = (❙⟦S❙⟧ p ∈# M. P p) \ B›
  by (induct M, simp add: Hiding_set_STOP)
     (metis MultiSync_add MultiSync_rec1 Hiding_Sync)


lemma MultiSync_prefix_pseudo_distrib:
  ‹M ≠ {#} ⟹ a ∈ S ⟹
   ((❙⟦S❙⟧ p ∈# M. (a → P p)) = (a → (❙⟦S❙⟧ p ∈# M. P p)))›
  by (induct M rule: mset_induct_nonempty) (simp_all add: prefix_Sync2)

lemmas MultiInter_Hiding_pseudo_distrib =
       MultiSync_Hiding_pseudo_distrib[where S = ‹{}›, simplified]
   and MultiPar_prefix_pseudo_distrib =
       MultiSync_prefix_pseudo_distrib[where S = ‹UNIV›, simplified]



lemma Hiding_MultiNdet_distrib:
  ‹finite A ⟹ (⨅ p ∈ A. P p) \ B = (⨅ p ∈ A. (P p \ B))›
  by (cases ‹A = {}›, simp add: Hiding_set_STOP, rotate_tac)
     (induct A rule: finite_set_induct_nonempty, simp_all add: Hiding_Ndet)


lemma Mndetprefix_Hiding_is_MultiNdet_prefix_Hiding:
  ‹finite A ⟹ ⊓ p ∈ A - B → ((P p) \ B) = ⨅ p ∈ A - B. (p → ((P p) \ B))›
proof (induct A rule: finite_induct)
  case empty
  thus ?case by fastforce
next
  show ‹finite F ⟹ x ∉ F ⟹ 
        ⊓ p ∈ F - B →  (P p \ B) = ⨅ p ∈ F - B.  (p → (P p \ B)) ⟹
        ⊓ p ∈ insert x F - B → (P p \ B) =
        ⨅ p ∈ insert x F - B.  (p → (P p \ B))› for x F
    apply (cases ‹x ∈ B›, simp)
    apply (cases ‹F - B = {}›,
           metis (no_types, lifting) Mndetprefix_unit MultiNdet_rec1 insert_Diff_if)
    by (simp add: Mndetprefix_distrib_unit insert_Diff_if)
qed


lemma Hiding_Mndetprefix_is_MultiNdet_Hiding:
  ‹finite A ⟹ A ⊆ B ⟹ (⊓ a ∈ A → P) \ B = ⨅ a ∈ A. (P \ B)›
  by (cases ‹A = {}›, simp add: Hiding_set_STOP, rotate_tac 2)
     (induct A rule: finite_set_induct_nonempty,
      simp_all add: Mndetprefix_unit Hiding_Ndet Hiding_write0
                    Mndetprefix_distrib_unit)



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 ∈# 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_distr_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]



text ‹A result on Mndetprefix and Sync.›

lemma Mndetprefix_Sync_distr: ‹A ≠ {} ⟹ B ≠ {} ⟹ 
       (⊓ a ∈ A → P a) ⟦S⟧ (⊓ b ∈ B → Q b) =
        ⊓ a∈A. ⊓ b∈B. (□c ∈ {a} - S → (P a ⟦S⟧ (b → Q b))) □ 
                       (□d ∈ {b} - S → ((a → P a) ⟦S⟧ Q b)) □
                       (□c∈{a} ∩ {b} ∩ S → (P a ⟦S⟧ Q b))›
  apply (subst (1 2) Mndetprefix_GlobalNdet) 
  apply (subst GlobalNdet_Sync_distr, assumption)
  apply (subst Sync_commute)
  apply (subst GlobalNdet_Sync_distr, assumption)
  apply (subst Sync_commute)
  apply (unfold write0_def)
  apply (subst Mprefix_Sync_distr_bis)
  by (fold write0_def) blast



text ‹A result on \<^const>‹MultiSeq› with \<^const>‹non_terminating›.›

lemma non_terminating_MultiSeq: 
  ‹(SEQ a ∈@ L. P a) =
   SEQ a ∈@ take (Suc (first_elem (λa. non_terminating (P a)) L)) L. P a›
  by (induct L; simp add: non_terminating_Seq)



section ‹Results on \<^const>‹Renaming››

lemma Renaming_GlobalNdet:
  ‹Renaming (⊓ a ∈ A. P (f a)) f = ⊓ b ∈ f ` A. Renaming (P b) f›
  by (subst Process_eq_spec)
     (auto simp add: F_Renaming D_Renaming F_GlobalNdet D_GlobalNdet)

lemma Renaming_GlobalNdet_inj_on:
  ‹Renaming (⊓ a ∈ A. P a) f =
   ⊓ b ∈ f ` A. Renaming (P (THE a. a ∈ A ∧ f a = b)) f›
  if inj_on_f: ‹inj_on f A›
  apply (subst Renaming_GlobalNdet[symmetric])
  apply (intro arg_cong[where f = ‹λQ. Renaming Q f›] mono_GlobalNdet_eq)
  by (metis inj_on_f the_inv_into_def the_inv_into_f_f)

corollary Renaming_GlobalNdet_inj:
  ‹Renaming (⊓ a ∈ A. P a) f =
   ⊓ b ∈ f ` A. Renaming (P (THE a. f a = b)) f› if inj_f: ‹inj f›
  apply (subst Renaming_GlobalNdet_inj_on, metis inj_eq inj_onI inj_f)
  apply (rule mono_GlobalNdet_eq[rule_format])
  by (metis imageE inj_eq[OF inj_f])



lemma Renaming_MultiNdet: ‹finite A ⟹ Renaming (⨅ a ∈ A. P (f a)) f =
                                        ⨅ b ∈ f ` A. Renaming (P b) f›
  by (subst (1 2) finite_GlobalNdet_is_MultiNdet[symmetric])
     (simp_all add: Renaming_GlobalNdet)
  

lemma Renaming_MultiNdet_inj_on:
  ‹finite A ⟹ inj_on f A ⟹
   Renaming (⨅ a ∈ A. P a) f = 
   ⨅ b ∈ f ` A. Renaming (P (THE a. a ∈ A ∧ f a = b)) f› 
  by (subst (1 2) finite_GlobalNdet_is_MultiNdet[symmetric])
     (simp_all add: Renaming_GlobalNdet_inj_on)
 

corollary Renaming_MultiNdet_inj:
  ‹finite A ⟹ inj f ⟹
   Renaming (⨅ a ∈ A. P a) f = ⨅ b ∈ f ` A. Renaming (P (THE a. f a = b)) f›
  by (subst (1 2) finite_GlobalNdet_is_MultiNdet[symmetric])
     (simp_all add: Renaming_GlobalNdet_inj)



lemma Renaming_MultiDet:
  ‹finite A ⟹ Renaming (❙□ a ∈ A. P (f a)) f = 
                ❙□ b ∈ f ` A. Renaming (P b) f›
  apply (induct A rule: finite_induct)
  by (simp_all add: Renaming_STOP Renaming_Det del: MultiDet_insert)

lemma Renaming_MultiDet_inj_on:
  ‹Renaming (❙□ a ∈ A. P a) f =
   ❙□ b ∈ f ` A. Renaming (P (THE a. a ∈ A ∧ f a = b)) f›
  if finite_A: ‹finite A› and inj_on_f: ‹inj_on f A›
  apply (subst Renaming_MultiDet[OF finite_A, symmetric])
  apply (intro arg_cong[where f = ‹λQ. Renaming Q f›]
               mono_MultiDet_eq finite_A)
  by (metis inj_on_f the_inv_into_def the_inv_into_f_f)

corollary Renaming_MultiDet_inj:
  ‹Renaming (❙□ a ∈ A. P a) f = ❙□ b ∈ f ` A. Renaming (P (THE a. f a = b)) f›
  if finite_A: ‹finite A› and inj_f: ‹inj f›
  apply (subst Renaming_MultiDet_inj_on[OF finite_A], metis inj_eq inj_onI inj_f)
  apply (rule mono_MultiDet_eq[rule_format], fact finite_imageI[OF finite_A])
  by (metis imageE inj_eq[OF inj_f])



lemma Renaming_MultiSeq:
  ‹Renaming (SEQ l ∈@ L. P (f l)) f = SEQ m ∈@ map f L. Renaming (P m) f›
  by (induct L, simp_all add: Renaming_SKIP Renaming_Seq)

lemma Renaming_MultiSeq_inj_on:
  ‹Renaming (SEQ l ∈@ L. P l) f =
   SEQ m ∈@ map f L. Renaming (P (THE l. l ∈ set L ∧ f l = m)) f›
  if inj_on_f: ‹inj_on f (set L)›
  apply (subst Renaming_MultiSeq[symmetric])
  apply (intro arg_cong[where f = ‹λQ. Renaming Q f›] mono_MultiSeq_eq)
  by (metis that the_inv_into_def the_inv_into_f_f)

corollary Renaming_MultiSeq_inj:
  ‹Renaming (SEQ l ∈@ L. P l) f = 
   SEQ m ∈@ map f L. Renaming (P (THE l. f l = m)) f› if inj_f: ‹inj f›
  apply (subst Renaming_MultiSeq_inj_on, metis inj_eq inj_onI inj_f)
  apply (rule mono_MultiSeq_eq[rule_format])
  by (metis (mono_tags, opaque_lifting) inj_image_mem_iff list.set_map inj_f)



end