Theory DeadlockResults

(*<*)
―‹ ********************************************************************
 * Project         : HOL-CSPM - Architectural operators for HOL-CSP
 *
 * Author          : Benoît Ballenghien, Safouan Taha, Burkhart Wolff
 *
 * This file       : Powerful results on DF and deadlock_free
 *
 * 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 ‹ Deadlock Results ›

theory DeadlockResults
  imports CSPM
begin

text ‹When working with the interleaving \<^term>‹P ||| Q›, we intuitively expect it to be
      \<^const>‹deadlock_free› when both \<^term>‹P› and \<^term>‹Q› are.

      This chapter contains several results about deadlock notion, and concludes
      with a proof of the theorem we just mentioned.›



section ‹Unfolding Lemmas for the Projections of \<^const>‹DF› and \<^const>‹DF⇩S⇩K⇩I⇩P››

text ‹\<^const>‹DF› and \<^const>‹DF⇩S⇩K⇩I⇩P› naturally appear when we work around \<^const>‹deadlock_free›
      and \<^const>‹deadlock_free⇩S⇩K⇩I⇩P› notions (because

      @{thm deadlock_free_def[of P] deadlock_free⇩S⇩K⇩I⇩P_def[of P]}).

      It is therefore convenient to have the following rules for unfolding the projections.›

lemma F_DF: 
  ‹ℱ (DF A) =
   (if A = {} then {(s, X). s = []}
    else (⋃x∈A. {[]} × {ref. ev x ∉ ref} ∪ 
                 {(tr, ref). tr ≠ [] ∧ hd tr = ev x ∧ (tl tr, ref) ∈ ℱ (DF A)}))›
  and F_DF⇩S⇩K⇩I⇩P: 
  ‹ℱ (DF⇩S⇩K⇩I⇩P A) =
   (if A = {} then {(s, X). s = [] ∨ s = [tick]}
    else {(s, X)| s X. s = [] ∧ tick ∉ X ∨ s = [tick]} ∪
         (⋃x∈A. {[]} × {ref. ev x ∉ ref} ∪ 
                 {(tr, ref). tr ≠ [] ∧ hd tr = ev x ∧ (tl tr, ref) ∈ ℱ (DF⇩S⇩K⇩I⇩P A)}))›
  by (subst DF_unfold DF⇩S⇩K⇩I⇩P_unfold;
      auto simp add: F_STOP F_Mprefix F_Mndetprefix write0_def F_SKIP F_Ndet)+


corollary Cons_F_DF:
  ‹(x # t, X) ∈ ℱ (DF A) ⟹ (t, X) ∈ ℱ (DF A)›
      and Cons_F_DF⇩S⇩K⇩I⇩P:
  ‹x ≠ tick ⟹ (x # t, X) ∈ ℱ (DF⇩S⇩K⇩I⇩P A) ⟹ (t, X) ∈ ℱ (DF⇩S⇩K⇩I⇩P A)›
  by (subst (asm) F_DF F_DF⇩S⇩K⇩I⇩P; auto split: if_split_asm)+


lemma D_DF: ‹𝒟 (DF A) = (if A = {} then {}
             else {s. s ≠ [] ∧ (∃x ∈ A. hd s = ev x ∧ tl s ∈ 𝒟 (DF A))})›
  and D_DF⇩S⇩K⇩I⇩P: ‹𝒟 (DF⇩S⇩K⇩I⇩P A) = (if A = {} then {}
                else {s. s ≠ [] ∧ (∃x ∈ A. hd s = ev x ∧ tl s ∈ 𝒟 (DF⇩S⇩K⇩I⇩P A))})›
  by (subst DF_unfold DF⇩S⇩K⇩I⇩P_unfold; 
      auto simp add: D_Mndetprefix D_Mprefix write0_def D_Ndet D_SKIP)+


lemma T_DF: 
  ‹𝒯 (DF A) = 
   (if A = {} then {[]}
    else {s. s = [] ∨ s ≠ [] ∧ (∃x ∈ A. hd s = ev x ∧ tl s ∈ 𝒯 (DF A))})›
  and T_DF⇩S⇩K⇩I⇩P: 
  ‹𝒯 (DF⇩S⇩K⇩I⇩P A) =
   (if A = {} then {[], [tick]}
    else {s. s = [] ∨ s = [tick] ∨ 
             s ≠ [] ∧ (∃x ∈ A. hd s = ev x ∧ tl s ∈ 𝒯 (DF⇩S⇩K⇩I⇩P A))})›
  by (subst DF_unfold DF⇩S⇩K⇩I⇩P_unfold; 
      auto simp add: T_STOP T_Mndetprefix write0_def T_Mprefix T_Ndet T_SKIP)+



section ‹Characterizations for \<^const>‹deadlock_free›, \<^const>‹deadlock_free⇩S⇩K⇩I⇩P››

text ‹We want more results like @{thm deadlock_free_Ndet[of P Q]},
      and we want to add the reciprocal when possible.›

text ‹The first thing we notice is that we only have to care about the failures›
lemma ‹deadlock_free⇩S⇩K⇩I⇩P P ≡ DF⇩S⇩K⇩I⇩P UNIV ⊑⇩F P›
  by (fact deadlock_free⇩S⇩K⇩I⇩P_def)

lemma deadlock_free_F: ‹deadlock_free P ⟷ DF UNIV ⊑⇩F P›
  by (metis deadlock_free_def div_free_divergence_refine(5) leFD_imp_leF
            leF_imp_leT leF_leD_imp_leFD non_terminating_refine_DF
            nonterminating_implies_div_free)
 


lemma deadlock_free_Mprefix_iff: ‹deadlock_free (□ a ∈ A → P a) ⟷ 
                                  A ≠ {} ∧ (∀a ∈ A. deadlock_free (P a))›
  and deadlock_free⇩S⇩K⇩I⇩P_Mprefix_iff: ‹deadlock_free⇩S⇩K⇩I⇩P (Mprefix A P) ⟷ 
                                     A ≠ {} ∧ (∀a ∈ A. deadlock_free⇩S⇩K⇩I⇩P (P a))›
  unfolding deadlock_free_F deadlock_free⇩S⇩K⇩I⇩P_def failure_refine_def
   apply (all ‹subst F_DF F_DF⇩S⇩K⇩I⇩P›,
          auto simp add: div_free_DF F_Mprefix D_Mprefix subset_iff)
  by (metis imageI list.distinct(1) list.sel(1, 3))
     (metis (no_types, lifting) event.distinct(1) image_eqI list.sel(1, 3) neq_Nil_conv)
  

lemmas deadlock_free_prefix_iff = 
       deadlock_free_Mprefix_iff   [of ‹{a}› ‹λa. P›, folded write0_def, simplified]
   and deadlock_free⇩S⇩K⇩I⇩P_prefix_iff = 
       deadlock_free⇩S⇩K⇩I⇩P_Mprefix_iff[of ‹{a}› ‹λa. P›, folded write0_def, simplified]
   for a P


lemma deadlock_free_Mndetprefix_iff: ‹deadlock_free (⊓ a ∈ A → P a) ⟷
                                      A ≠ {} ∧ (∀a∈A. deadlock_free (P a))›
  and deadlock_free⇩S⇩K⇩I⇩P_Mndetprefix_iff: ‹deadlock_free⇩S⇩K⇩I⇩P (⊓ a ∈ A → P a) ⟷ 
                                         A ≠ {} ∧ (∀a∈A. deadlock_free⇩S⇩K⇩I⇩P (P a))›
   apply (all ‹intro iffI conjI›)
  using non_deadlock_free_STOP 
       apply force
      apply (meson Mprefix_refines_Mndetprefix_FD 
      deadlock_free_Mprefix_iff deadlock_free_def trans_FD)
     apply (metis (no_types, lifting) Mndetprefix_GlobalNdet 
      deadlock_free_def deadlock_free_prefix_iff mono_GlobalNdet_FD_const)
  using non_deadlock_free_v2_STOP 
    apply force
   apply (meson Mprefix_refines_Mndetprefix_FD deadlock_free⇩S⇩K⇩I⇩P_FD
      deadlock_free⇩S⇩K⇩I⇩P_Mprefix_iff trans_FD)
  by (metis (no_types, lifting) Mndetprefix_GlobalNdet deadlock_free⇩S⇩K⇩I⇩P_prefix_iff
            deadlock_free_v2_FD mono_GlobalNdet_FD_const)





lemma deadlock_free_Ndet_iff: ‹deadlock_free (P ⊓ Q) ⟷ 
                               deadlock_free P ∧ deadlock_free Q› 
  and deadlock_free⇩S⇩K⇩I⇩P_Ndet_iff: ‹deadlock_free⇩S⇩K⇩I⇩P (P ⊓ Q) ⟷
                                  deadlock_free⇩S⇩K⇩I⇩P P ∧ deadlock_free⇩S⇩K⇩I⇩P Q›
  unfolding deadlock_free_F deadlock_free⇩S⇩K⇩I⇩P_def failure_refine_def
  by (simp_all add: F_Ndet)



lemma deadlock_free_GlobalNdet_iff: ‹deadlock_free (⊓ a ∈ A. P a) ⟷
                                     A ≠ {} ∧ (∀ a ∈ A. deadlock_free (P a))› 
  and deadlock_free⇩S⇩K⇩I⇩P_GlobalNdet_iff: ‹deadlock_free⇩S⇩K⇩I⇩P (⊓ a ∈ A. P a) ⟷
                                        A ≠ {} ∧ (∀ a ∈ A. deadlock_free⇩S⇩K⇩I⇩P (P a))›
  by (metis (mono_tags, lifting) GlobalNdet_refine_FD deadlock_free_def trans_FD
            mono_GlobalNdet_FD_const non_deadlock_free_STOP empty_GlobalNdet)
     (metis (mono_tags, lifting) GlobalNdet_refine_FD deadlock_free⇩S⇩K⇩I⇩P_FD trans_FD
            mono_GlobalNdet_FD_const non_deadlock_free⇩S⇩K⇩I⇩P_STOP empty_GlobalNdet)


lemma deadlock_free_MultiNdet_iff: ‹deadlock_free (⨅ a ∈ A. P a) ⟷
                                    A ≠ {} ∧ (∀ a ∈ A. deadlock_free (P a))› 
  and deadlock_free⇩S⇩K⇩I⇩P_MultiNdet_iff: ‹deadlock_free⇩S⇩K⇩I⇩P (⨅ a ∈ A. P a) ⟷ 
                                       A ≠ {} ∧ (∀ a ∈ A. deadlock_free⇩S⇩K⇩I⇩P (P a))›
   if fin: ‹finite A›
  by (metis deadlock_free_GlobalNdet_iff    finite_GlobalNdet_is_MultiNdet that)
     (metis deadlock_free⇩S⇩K⇩I⇩P_GlobalNdet_iff finite_GlobalNdet_is_MultiNdet that)




lemma deadlock_free_MultiDet:
  ‹⟦A ≠ {}; finite A; ∀a∈A. deadlock_free (P a)⟧ ⟹ deadlock_free (❙□a ∈ A. P a)›
  and deadlock_free⇩S⇩K⇩I⇩P_MultiDet:
  ‹⟦A ≠ {}; finite A; ∀a∈A. deadlock_free⇩S⇩K⇩I⇩P (P a)⟧ ⟹ deadlock_free⇩S⇩K⇩I⇩P (❙□a ∈ A. P a)›
  by (metis deadlock_free_MultiNdet_iff deadlock_free_def
            mono_MultiNdet_MultiDet_FD trans_FD)
     (metis deadlock_free⇩S⇩K⇩I⇩P_FD deadlock_free⇩S⇩K⇩I⇩P_MultiNdet_iff
            mono_MultiNdet_MultiDet_FD trans_FD)


lemma deadlock_free_Det:
  ‹deadlock_free    P ⟹ deadlock_free    Q ⟹ deadlock_free    (P □ Q)›
  and deadlock_free⇩S⇩K⇩I⇩P_Det:
  ‹deadlock_free⇩S⇩K⇩I⇩P P ⟹ deadlock_free⇩S⇩K⇩I⇩P Q ⟹ deadlock_free⇩S⇩K⇩I⇩P (P □ Q)›
  by (meson deadlock_free_Ndet deadlock_free_def mono_Ndet_Det_FD trans_FD)
     (metis deadlock_free⇩S⇩K⇩I⇩P_FD deadlock_free⇩S⇩K⇩I⇩P_Ndet_iff mono_Ndet_Det_FD trans_FD)



text ‹For \<^term>‹P □ Q›, we can not expect more:›

lemma
  ‹∃P Q. deadlock_free    P ∧ ¬ deadlock_free    Q ∧
         deadlock_free     (P □ Q)›
  ‹∃P Q. deadlock_free⇩S⇩K⇩I⇩P P ∧ ¬ deadlock_free⇩S⇩K⇩I⇩P Q ∧
         deadlock_free⇩S⇩K⇩I⇩P (P □ Q)›
  by (metis Det_STOP deadlock_free_def idem_FD non_deadlock_free_STOP)
     (metis Det_STOP deadlock_free⇩S⇩K⇩I⇩P_FD idem_FD non_deadlock_free⇩S⇩K⇩I⇩P_STOP)

 


lemma FD_Mndetprefix_iff:
  ‹A ≠ {} ⟹ P ⊑⇩F⇩D ⊓ a ∈ A → Q ⟷ (∀a ∈ A. P ⊑⇩F⇩D (a → Q))›
  by (auto simp: failure_divergence_refine_def le_ref_def subset_iff
                 D_Mndetprefix F_Mndetprefix write0_def D_Mprefix F_Mprefix) blast


lemma Mndetprefix_FD: ‹(∃a ∈ A. (a → Q) ⊑⇩F⇩D P) ⟹ ⊓ a ∈ A → Q ⊑⇩F⇩D P›
  by (meson Mndetprefix_refine_FD failure_divergence_refine_def trans_FD)




text ‹\<^const>‹Mprefix›, \<^const>‹Sync› and \<^const>‹deadlock_free››

lemma Mprefix_Sync_deadlock_free:
  assumes not_all_empty: ‹A ≠ {} ∨ B ≠ {} ∨ A' ∩ B' ≠ {}›
      and ‹A ∩ S = {}› and ‹A' ⊆ S› and ‹B ∩ S = {}› and ‹B' ⊆ S›
      and ‹∀x∈A. deadlock_free (P x ⟦S⟧ Mprefix (B ∪ B') Q)›
      and ‹∀y∈B. deadlock_free (Mprefix (A ∪ A') P ⟦S⟧ Q y)›
      and ‹∀x∈A' ∩ B'. deadlock_free ((P x ⟦S⟧ Q x))› 
  shows ‹deadlock_free (Mprefix (A ∪ A') P ⟦S⟧ Mprefix (B ∪ B') Q)› 
proof -
  have ‹A = {} ∧ B ≠ {} ∧ A' ∩ B' ≠ {} ∨ A ≠ {} ∧ B = {} ∧ A' ∩ B' = {} ∨
        A ≠ {} ∧ B = {} ∧ A' ∩ B' ≠ {} ∨ A = {} ∧ B ≠ {} ∧ A' ∩ B' = {} ∨ 
        A ≠ {} ∧ B ≠ {} ∧ A' ∩ B' = {} ∨ A = {} ∧ B = {} ∧ A' ∩ B' ≠ {} ∨
        A ≠ {} ∧ B ≠ {} ∧ A' ∩ B' ≠ {}› by (meson not_all_empty)
  thus ?thesis
    apply (subst Mprefix_Sync_distr; simp add: assms Mprefix_STOP) 
    by (metis (no_types, lifting) Det_STOP Det_commute Mprefix_STOP
              assms(6, 7, 8) deadlock_free_Det deadlock_free_Mprefix_iff)
qed



lemmas Mprefix_Sync_subset_deadlock_free = Mprefix_Sync_deadlock_free
                                           [where A  = ‹{}› and B  = ‹{}›, simplified]
   and Mprefix_Sync_indep_deadlock_free  = Mprefix_Sync_deadlock_free
                                           [where A' = ‹{}› and B' = ‹{}›, simplified]
   and Mprefix_Sync_right_deadlock_free  = Mprefix_Sync_deadlock_free
                                           [where A  = ‹{}› and B' = ‹{}›, simplified]
   and Mprefix_Sync_left_deadlock_free   = Mprefix_Sync_deadlock_free
                                           [where A' = ‹{}› and B  = ‹{}›, simplified]




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

text ‹The \<^const>‹Renaming› operator is new (release of 2023), so here are its properties
      on reference processes from \<^theory>‹HOL-CSP.Assertions›, and deadlock notion.›

subsection ‹Behaviour with References Processes›

text ‹For \<^const>‹DF››

lemma DF_FD_Renaming_DF: ‹DF (f ` A) ⊑⇩F⇩D Renaming (DF A) f›
proof (subst DF_def, induct rule: fix_ind)
  show ‹adm (λa. a ⊑⇩F⇩D Renaming (DF A) f)› by (simp add: monofun_def)
next
  show ‹⊥ ⊑⇩F⇩D Renaming (DF A) f› by simp
next
  show ‹(Λ x. ⊓a ∈ f ` A →  x)⋅x ⊑⇩F⇩D Renaming (DF A) f›
    if ‹x ⊑⇩F⇩D Renaming (DF A) f› for x
    apply simp
    apply (subst DF_unfold)
    apply (subst Renaming_Mndetprefix)
    by (rule mono_Mndetprefix_FD[rule_format, OF that])
qed

lemma Renaming_DF_FD_DF: ‹Renaming (DF A) f ⊑⇩F⇩D DF (f ` A)›
  if finitary: ‹finitary f›
proof (subst DF_def, induct rule: fix_ind)
  show ‹adm (λa. Renaming a f ⊑⇩F⇩D DF (f ` A))›
    by (simp add: finitary monofun_def)
next
  show ‹Renaming ⊥ f ⊑⇩F⇩D DF (f ` A)› by (simp add: Renaming_BOT)
next
  show ‹Renaming ((Λ x. ⊓a ∈ A →  x)⋅x) f ⊑⇩F⇩D DF (f ` A)›
    if ‹Renaming x f ⊑⇩F⇩D DF (f ` A)› for x
    apply simp
    apply (subst Renaming_Mndetprefix)
    apply (subst DF_unfold)
    by (rule mono_Mndetprefix_FD[rule_format, OF that])
qed


text ‹For \<^const>‹DF⇩S⇩K⇩I⇩P››

lemma DF⇩S⇩K⇩I⇩P_FD_Renaming_DF⇩S⇩K⇩I⇩P:
  ‹DF⇩S⇩K⇩I⇩P (f ` A) ⊑⇩F⇩D Renaming (DF⇩S⇩K⇩I⇩P A) f›
proof (subst DF⇩S⇩K⇩I⇩P_def, induct rule: fix_ind)
  show ‹adm (λa. a ⊑⇩F⇩D Renaming (DF⇩S⇩K⇩I⇩P A) f)› by (simp add: monofun_def)
next
  show ‹⊥ ⊑⇩F⇩D Renaming (DF⇩S⇩K⇩I⇩P A) f› by simp
next
  show ‹(Λ x. (⊓ a∈f ` A →  x) ⊓ SKIP)⋅x ⊑⇩F⇩D Renaming (DF⇩S⇩K⇩I⇩P A) f›
    if ‹x ⊑⇩F⇩D Renaming (DF⇩S⇩K⇩I⇩P A) f› for x
    apply simp
    apply (subst DF⇩S⇩K⇩I⇩P_unfold)
    apply (simp add: Renaming_Ndet Renaming_SKIP)
    apply (subst Renaming_Mndetprefix)
    apply (rule mono_Ndet_FD [OF _ idem_FD])
    by (rule mono_Mndetprefix_FD[rule_format, OF that])
qed

lemma Renaming_DF⇩S⇩K⇩I⇩P_FD_DF⇩S⇩K⇩I⇩P:
  ‹Renaming (DF⇩S⇩K⇩I⇩P A) f ⊑⇩F⇩D DF⇩S⇩K⇩I⇩P (f ` A)›
  if finitary: ‹finitary f›
proof (subst DF⇩S⇩K⇩I⇩P_def, induct rule: fix_ind)
  show ‹adm (λa. Renaming a f ⊑⇩F⇩D DF⇩S⇩K⇩I⇩P (f ` A))›
    by (simp add: finitary monofun_def)
next
  show ‹Renaming ⊥ f ⊑⇩F⇩D DF⇩S⇩K⇩I⇩P (f ` A)› by (simp add: Renaming_BOT)
next
  show ‹Renaming ((Λ x. (⊓a ∈ A →  x) ⊓ SKIP)⋅x) f ⊑⇩F⇩D DF⇩S⇩K⇩I⇩P (f ` A)›
    if ‹Renaming x f ⊑⇩F⇩D DF⇩S⇩K⇩I⇩P (f ` A)› for x
    apply simp
    apply (simp add: Renaming_Ndet Renaming_SKIP)
    apply (subst Renaming_Mndetprefix)
    apply (subst DF⇩S⇩K⇩I⇩P_unfold)
    apply (rule mono_Ndet_FD [OF _ idem_FD])
    by (rule mono_Mndetprefix_FD[rule_format, OF that])
qed



text ‹For \<^const>‹RUN››

lemma RUN_FD_Renaming_RUN: ‹RUN (f ` A) ⊑⇩F⇩D Renaming (RUN A) f›
proof (subst RUN_def, induct rule: fix_ind)
  show ‹adm (λa. a ⊑⇩F⇩D Renaming (RUN A) f)› by (simp add: monofun_def)
next
  show ‹⊥ ⊑⇩F⇩D Renaming (RUN A) f› by simp
next
  show ‹(Λ x. □a ∈ f ` A →  x)⋅x ⊑⇩F⇩D Renaming (RUN A) f›
    if ‹x ⊑⇩F⇩D Renaming (RUN A) f› for x
    apply simp
    apply (subst RUN_unfold)
    apply (subst Renaming_Mprefix)
    by (rule mono_Mprefix_FD[rule_format, OF that])
qed

lemma Renaming_RUN_FD_RUN: ‹Renaming (RUN A) f ⊑⇩F⇩D RUN (f ` A)›
  if finitary: ‹finitary f›
proof (subst RUN_def, induct rule: fix_ind)
  show ‹adm (λa. Renaming a f ⊑⇩F⇩D RUN (f ` A))›
    by (simp add: finitary monofun_def)
next
  show ‹Renaming ⊥ f ⊑⇩F⇩D RUN (f ` A)› by (simp add: Renaming_BOT)
next
  show ‹Renaming ((Λ x. □a ∈ A →  x)⋅x) f ⊑⇩F⇩D RUN (f ` A)›
    if ‹Renaming x f ⊑⇩F⇩D RUN (f ` A)› for x
    apply simp
    apply (subst Renaming_Mprefix)
    apply (subst RUN_unfold)
    by (rule mono_Mprefix_FD[rule_format, OF that])
qed


text ‹For \<^const>‹CHAOS››

lemma CHAOS_FD_Renaming_CHAOS:
  ‹CHAOS (f ` A) ⊑⇩F⇩D Renaming (CHAOS A) f›
proof (subst CHAOS_def, induct rule: fix_ind)
  show ‹adm (λa. a ⊑⇩F⇩D Renaming (CHAOS A) f)› by (simp add: monofun_def)
next
  show ‹⊥ ⊑⇩F⇩D Renaming (CHAOS A) f› by simp
next
  show ‹(Λ x. STOP ⊓ (□a∈f ` A → x))⋅x ⊑⇩F⇩D Renaming (CHAOS A) f›
    if ‹x ⊑⇩F⇩D Renaming (CHAOS A) f› for x
    apply simp
    apply (subst CHAOS_unfold)
    apply (simp add: Renaming_Ndet Renaming_STOP)
    apply (rule mono_Ndet_FD[OF idem_FD])
    apply (subst Renaming_Mprefix)
    by (rule mono_Mprefix_FD[rule_format, OF that])
qed

lemma Renaming_CHAOS_FD_CHAOS:
  ‹Renaming (CHAOS A) f ⊑⇩F⇩D CHAOS (f ` A)›
  if finitary: ‹finitary f›
proof (subst CHAOS_def, induct rule: fix_ind)
  show ‹adm (λa. Renaming a f ⊑⇩F⇩D CHAOS (f ` A))›
    by (simp add: finitary monofun_def)
next
  show ‹Renaming ⊥ f ⊑⇩F⇩D CHAOS (f ` A)› by (simp add: Renaming_BOT)
next
  show ‹Renaming ((Λ x. STOP ⊓ (□xa∈A → x))⋅x) f ⊑⇩F⇩D CHAOS (f ` A)›
    if ‹Renaming x f ⊑⇩F⇩D CHAOS (f ` A)› for x
    apply simp
    apply (simp add: Renaming_Ndet Renaming_STOP)
    apply (subst CHAOS_unfold)
    apply (subst Renaming_Mprefix)
    apply (rule mono_Ndet_FD[OF idem_FD])
    by (rule mono_Mprefix_FD[rule_format, OF that])
qed


text ‹For \<^const>‹CHAOS⇩S⇩K⇩I⇩P››

lemma CHAOS⇩S⇩K⇩I⇩P_FD_Renaming_CHAOS⇩S⇩K⇩I⇩P:
  ‹CHAOS⇩S⇩K⇩I⇩P (f ` A) ⊑⇩F⇩D Renaming (CHAOS⇩S⇩K⇩I⇩P A) f›
proof (subst CHAOS⇩S⇩K⇩I⇩P_def, induct rule: fix_ind)
  show ‹adm (λa. a ⊑⇩F⇩D Renaming (CHAOS⇩S⇩K⇩I⇩P A) f)›
    by (simp add: monofun_def)
next
  show ‹⊥ ⊑⇩F⇩D Renaming (CHAOS⇩S⇩K⇩I⇩P A) f› by simp
next
  show ‹(Λ x. SKIP ⊓ STOP ⊓ (□xa∈f ` A → x))⋅x ⊑⇩F⇩D 
        Renaming (CHAOS⇩S⇩K⇩I⇩P A) f›
    if ‹x ⊑⇩F⇩D Renaming (CHAOS⇩S⇩K⇩I⇩P A) f› for x
    apply simp
    apply (subst CHAOS⇩S⇩K⇩I⇩P_unfold)
    apply (simp add: Renaming_Ndet Renaming_STOP Renaming_SKIP)
    apply (rule mono_Ndet_FD[OF idem_FD])
    apply (subst Renaming_Mprefix)
    by (rule mono_Mprefix_FD[rule_format, OF that])
qed

lemma Renaming_CHAOS⇩S⇩K⇩I⇩P_FD_CHAOS⇩S⇩K⇩I⇩P:
  ‹Renaming (CHAOS⇩S⇩K⇩I⇩P A) f ⊑⇩F⇩D CHAOS⇩S⇩K⇩I⇩P (f ` A)›
  if finitary: ‹finitary f›
proof (subst CHAOS⇩S⇩K⇩I⇩P_def, induct rule: fix_ind)
  show ‹adm (λa. Renaming a f ⊑⇩F⇩D CHAOS⇩S⇩K⇩I⇩P (f ` A))›
    by (simp add: finitary monofun_def)
next
  show ‹Renaming ⊥ f ⊑⇩F⇩D CHAOS⇩S⇩K⇩I⇩P (f ` A)› by (simp add: Renaming_BOT)
next
  show ‹Renaming ((Λ x. SKIP ⊓ STOP ⊓ (□xa∈A → x))⋅x) f ⊑⇩F⇩D CHAOS⇩S⇩K⇩I⇩P (f ` A)›
    if ‹Renaming x f ⊑⇩F⇩D CHAOS⇩S⇩K⇩I⇩P (f ` A)› for x
    apply simp
    apply (simp add: Renaming_Ndet Renaming_STOP Renaming_SKIP)
    apply (subst CHAOS⇩S⇩K⇩I⇩P_unfold)
    apply (subst Renaming_Mprefix)
    apply (rule mono_Ndet_FD[OF idem_FD])
    by (rule mono_Mprefix_FD[rule_format, OF that])
qed



subsection ‹Corollaries on \<^const>‹deadlock_free› and \<^const>‹deadlock_free⇩S⇩K⇩I⇩P››

lemmas Renaming_DF = 
       FD_antisym[OF Renaming_DF_FD_DF DF_FD_Renaming_DF]
   and Renaming_DF⇩S⇩K⇩I⇩P =
      FD_antisym[OF Renaming_DF⇩S⇩K⇩I⇩P_FD_DF⇩S⇩K⇩I⇩P DF⇩S⇩K⇩I⇩P_FD_Renaming_DF⇩S⇩K⇩I⇩P]
   and Renaming_RUN =
       FD_antisym[OF Renaming_RUN_FD_RUN RUN_FD_Renaming_RUN]
   and Renaming_CHAOS =
       FD_antisym[OF Renaming_CHAOS_FD_CHAOS CHAOS_FD_Renaming_CHAOS]
   and Renaming_CHAOS⇩S⇩K⇩I⇩P =
       FD_antisym[OF Renaming_CHAOS⇩S⇩K⇩I⇩P_FD_CHAOS⇩S⇩K⇩I⇩P
                     CHAOS⇩S⇩K⇩I⇩P_FD_Renaming_CHAOS⇩S⇩K⇩I⇩P]
    


lemma deadlock_free_imp_deadlock_free_Renaming: ‹deadlock_free (Renaming P f)›
  if ‹deadlock_free P›
  apply (rule DF_Univ_freeness[of ‹range f›], simp)
  apply (rule trans_FD[OF DF_FD_Renaming_DF])
  apply (rule mono_Renaming_FD)
  by (rule that[unfolded deadlock_free_def])

lemma deadlock_free_Renaming_imp_deadlock_free: ‹deadlock_free P›
  if ‹inj f› and ‹deadlock_free (Renaming P f)›
  apply (subst Renaming_inv[OF that(1), symmetric])
  apply (rule deadlock_free_imp_deadlock_free_Renaming)
  by (rule that(2))

corollary deadlock_free_Renaming_iff:
  ‹inj f ⟹ deadlock_free (Renaming P f) ⟷ deadlock_free P›
  using deadlock_free_Renaming_imp_deadlock_free
        deadlock_free_imp_deadlock_free_Renaming by blast



lemma deadlock_free⇩S⇩K⇩I⇩P_imp_deadlock_free⇩S⇩K⇩I⇩P_Renaming:
  ‹deadlock_free⇩S⇩K⇩I⇩P (Renaming P f)› if ‹deadlock_free⇩S⇩K⇩I⇩P P›
  unfolding deadlock_free⇩S⇩K⇩I⇩P_FD
  apply (rule trans_FD[OF DF⇩S⇩K⇩I⇩P_subset_FD[of ‹range f›]], simp_all)
  apply (rule trans_FD[OF DF⇩S⇩K⇩I⇩P_FD_Renaming_DF⇩S⇩K⇩I⇩P])
  by (rule mono_Renaming_FD[OF that[unfolded deadlock_free⇩S⇩K⇩I⇩P_FD]])
 
lemma deadlock_free⇩S⇩K⇩I⇩P_Renaming_imp_deadlock_free⇩S⇩K⇩I⇩P:
  ‹deadlock_free⇩S⇩K⇩I⇩P P› if ‹inj f› and ‹deadlock_free⇩S⇩K⇩I⇩P (Renaming P f)›
  apply (subst Renaming_inv[OF that(1), symmetric])
  apply (rule deadlock_free⇩S⇩K⇩I⇩P_imp_deadlock_free⇩S⇩K⇩I⇩P_Renaming)
  by (rule that(2))

corollary deadlock_free⇩S⇩K⇩I⇩P_Renaming_iff:
  ‹inj f ⟹ deadlock_free⇩S⇩K⇩I⇩P (Renaming P f) ⟷ deadlock_free⇩S⇩K⇩I⇩P P›
  using deadlock_free⇩S⇩K⇩I⇩P_Renaming_imp_deadlock_free⇩S⇩K⇩I⇩P
        deadlock_free⇩S⇩K⇩I⇩P_imp_deadlock_free⇩S⇩K⇩I⇩P_Renaming by blast







section ‹Big Results›

subsection ‹Interesting Equivalence›

lemma deadlock_free_of_Sync_iff_DF_FD_DF_Sync_DF:
  ‹(∀P Q. deadlock_free (P::'α process) ⟶ deadlock_free Q ⟶
          deadlock_free (P ⟦S⟧ Q))
   ⟷ (DF (UNIV::'α set) ⊑⇩F⇩D (DF UNIV ⟦S⟧ DF UNIV))› (is ‹?lhs ⟷ ?rhs›)
proof (rule iffI)
  assume ?lhs
  show ?rhs by (fold deadlock_free_def, rule ‹?lhs›[rule_format])
               (simp_all add: deadlock_free_def)
next
  assume ?rhs
  show ?lhs unfolding deadlock_free_def
            by (intro allI impI trans_FD[OF ‹?rhs›]) (rule mono_Sync_FD)
qed

text ‹From this general equivalence on \<^const>‹Sync›, we immediately obtain the equivalence
      on \<^term>‹(A ||| B)›: @{thm deadlock_free_of_Sync_iff_DF_FD_DF_Sync_DF[of ‹{}›]}.›


subsection ‹\<^const>‹STOP› and \<^const>‹SKIP› Synchronized with \<^term>‹DF A››

lemma DF_FD_DF_Sync_STOP_or_SKIP_iff: 
  ‹(DF A ⊑⇩F⇩D DF A ⟦S⟧ P) ⟷ A ∩ S = {}›
  if P_disj: ‹P = STOP ∨ P = SKIP›
proof
  { assume a1: ‹DF A ⊑⇩F⇩D DF A ⟦S⟧ P› and a2: ‹A ∩ S ≠ {}›
    from a2 obtain x where f1: ‹x ∈ A› and f2: ‹x ∈ S› by blast
    have ‹DF A ⟦S⟧ P ⊑⇩F⇩D DF {x} ⟦S⟧ P›
      by (intro mono_Sync_FD[OF _ idem_FD]) (simp add: DF_subset f1)
    also have ‹… = STOP›
      apply (subst DF_unfold)
      using P_disj 
      apply (rule disjE; simp add: Mndetprefix_unit)
       apply (simp add: write0_def, subst Mprefix_STOP[symmetric],
              subst Mprefix_Sync_distr_right, (simp_all add: f2 Mprefix_STOP)[3])
      by (subst DF_unfold, simp add: Mndetprefix_unit f2 prefix_Sync_SKIP2)
      finally have False
        by (metis DF_Univ_freeness a1 empty_not_insert f1
                  insert_absorb non_deadlock_free_STOP trans_FD)
  }
  thus ‹DF A ⊑⇩F⇩D DF A ⟦S⟧ P ⟹ A ∩ S = {}› by blast
next
  have D_P: ‹𝒟 P = {}› using D_SKIP D_STOP P_disj by blast
  note F_T_P = F_STOP T_STOP F_SKIP D_SKIP
  { assume a1: ‹¬ DF A ⊑⇩F⇩D DF A ⟦S⟧ P› and a2: ‹A ∩ S = {}›
    have False
    proof (cases ‹A = {}›)
      assume ‹A = {}›
      with a1[unfolded DF_def] show False
        by (simp add: fix_const)
           (metis Sync_SKIP_STOP Sync_STOP_STOP Sync_commute idem_FD that)
    next
      assume a3: ‹A ≠ {}›
      have falsify: ‹(a, (X ∪ Y) ∩ insert tick (ev ` S) ∪ X ∩ Y) ∉ ℱ (DF A) ⟹
                     (t, X) ∈ ℱ (DF A) ⟹ (u, Y) ∈ ℱ P ⟹ 
                     a setinterleaves ((t, u), insert tick (ev ` S)) ⟹ False› for a t u X Y
      proof (induct t arbitrary: a)
        case Nil
        show ?case by (rule disjE[OF P_disj], insert Nil a2)
                      (subst (asm) F_DF, auto simp add: a3 F_T_P)+
      next
        case (Cons x t)
        from Cons(4) have f1: ‹u = []›
          apply (subst disjE[OF P_disj], simp_all add: F_T_P) 
          by (metis Cons(2, 3, 5) F_T Sync.sym TickLeftSync empty_iff
                    ftf_Sync21 insertI1 nonTickFree_n_frontTickFree 
                    non_tickFree_tick process_charn tickFree_def tick_T_F)
        from Cons(2, 3) show False
          apply (subst (asm) (1 2) F_DF, auto simp add: a3)
          by (metis Cons.hyps Cons.prems(3, 4) Sync.sym SyncTlEmpty 
                    emptyLeftProperty f1 list.distinct(1) list.sel(1, 3))
      qed
      from a1 show False
        unfolding failure_divergence_refine_def le_ref_def
        by (auto simp add: F_Sync D_Sync D_P div_free_DF subset_iff intro: falsify)
    qed
  }
  thus ‹A ∩ S = {} ⟹ DF A ⊑⇩F⇩D DF A ⟦S⟧ P› by blast
qed



lemma DF_Sync_STOP_or_SKIP_FD_DF: ‹DF A ⟦S⟧ P ⊑⇩F⇩D DF A› 
  if P_disj: ‹P = STOP ∨ P = SKIP› and empty_inter: ‹A ∩ S = {}›
proof (cases ‹A = {}›)
  from P_disj show ‹A = {} ⟹ DF A ⟦S⟧ P ⊑⇩F⇩D DF A›
    by (rule disjE) (simp_all add: DF_def fix_const Sync_SKIP_STOP
                                   Sync_STOP_STOP Sync_commute)
next
  assume ‹A ≠ {}›
  show ?thesis
  proof (subst DF_def, induct rule: fix_ind)
    show ‹adm (λa. a ⟦S⟧ P ⊑⇩F⇩D DF A)› by (simp add: cont2mono)
  next
    show ‹⊥ ⟦S⟧ P ⊑⇩F⇩D DF A› by (metis BOT_leFD Sync_BOT Sync_commute)
  next
    case (3 x)
    have ‹(⊓a ∈ A → x) ⟦S⟧ P ⊑⇩F⇩D (a → DF A)› if ‹a ∈ A› for a
      apply (rule trans_FD[OF mono_Sync_FD
                  [OF mono_Mndetprefix_FD_set
                      [of ‹{a}›, simplified, OF that] idem_FD]])
      apply (rule disjE[OF P_disj], simp_all add: Mndetprefix_unit)
       apply (subst Mprefix_Sync_distr_left
                    [of ‹{a}› _ ‹{}› ‹λa. x›, 
                     simplified Mprefix_STOP, folded write0_def],
              (insert empty_inter that "3", auto)[3])
      by (subst prefix_Sync_SKIP1, (insert empty_inter that "3", auto)[2])
    thus ?case by (subst DF_unfold, subst FD_Mndetprefix_iff; simp add: ‹A ≠ {}›)
  qed
qed



lemmas DF_FD_DF_Sync_STOP_iff = 
       DF_FD_DF_Sync_STOP_or_SKIP_iff[of STOP, simplified]
   and DF_FD_DF_Sync_SKIP_iff =
       DF_FD_DF_Sync_STOP_or_SKIP_iff[of SKIP, simplified]
   and DF_Sync_STOP_FD_DF =
       DF_Sync_STOP_or_SKIP_FD_DF[of STOP, simplified]
   and DF_Sync_SKIP_FD_DF = 
       DF_Sync_STOP_or_SKIP_FD_DF[of SKIP, simplified]



subsection ‹Finally, \<^term>‹deadlock_free (P ||| Q)››

theorem DF_F_DF_Sync_DF: ‹DF (A ∪ B::'α set) ⊑⇩F DF A ⟦S⟧ DF B›
  if  nonempty: ‹A ≠ {} ∧ B ≠ {}›
 and intersect_hyp: ‹B ∩ S = {} ∨ (∃y. B ∩ S = {y} ∧ A ∩ S ⊆ {y})›
  unfolding failure_refine_def apply (simp add: F_Sync div_free_DF, safe)
proof -
  fix v t u X Y
  assume * : ‹(t, X) ∈ ℱ (DF A)› ‹(u, Y) ∈ ℱ (DF B)› 
             ‹v setinterleaves ((t, u), insert tick (ev ` S))›
  define β where ‹β ≡ (t, insert tick (ev ` S), u)›
  with * have ‹(fst β, X) ∈ ℱ (DF A)› ‹(snd (snd β), Y) ∈ ℱ (DF B)›
              ‹v ∈ setinterleaving β› by simp_all

  thus ‹(v, (X ∪ Y) ∩ insert tick (ev ` S) ∪ X ∩ Y) ∈ ℱ (DF (A ∪ B))›
    apply (subst F_DF, simp add: nonempty)
  proof (induct arbitrary: v rule: setinterleaving.induct)

    case (1 Z)
    hence mt_a: ‹v = []› using emptyLeftProperty by blast
    from intersect_hyp
    consider ‹B ∩ S = {}› | ‹∃y. B ∩ S = {y} ∧ A ∩ S ⊆ {y}› by blast
    thus ?case
    proof cases
      case 11: 1
      with "1"(2) show ?thesis by (subst (asm) F_DF)
                                  (auto simp add: nonempty mt_a)
    next
      case 12: 2
      then obtain y where f12: ‹B ∩ S = {y}› and ‹A ∩ S ⊆ {y}› by blast
      from this(2) consider ‹A ∩ S = {}› | ‹A ∩ S = {y}› by blast
      thus ?thesis
      proof cases
        case 121: 1
        with "1"(1) show ?thesis by (subst (asm) F_DF)
                                    (auto simp add: nonempty mt_a)
      next
        case 122: 2
        with "1"(1, 2) f12 nonempty mt_a mk_disjoint_insert show ?thesis
          by (subst (asm) (1 2) F_DF) (auto, fastforce)
      qed
    qed
  next

    case (2 Z y u)
    have * : ‹y ∉ Z› ‹([], X) ∈ ℱ (DF A)› ‹(u, Y) ∈ ℱ (DF B)› ‹v = y # u›
      using "2.prems" Cons_F_DF by (auto simp add: emptyLeftProperty)
    have ** : ‹u setinterleaves (([], u), Z)›
      by (metis "*"(4) "2.prems"(3) SyncTlEmpty list.sel(3))
    from "2.prems"(2) obtain b where  *** : ‹b ∈ B› ‹y = ev b›
      by (subst (asm) F_DF, simp split: if_split_asm) blast
    show ?case
      apply (rule disjI2, rule_tac x = b in bexI)
      using "2.hyps"[simplified, OF *(1, 2, 3) **] 
      by (subst F_DF) (auto simp add: *(4) ***)
  next

    case (3 x t Z)
    have * : ‹x ∉ Z› ‹(t, X) ∈ ℱ (DF A)› ‹([], Y) ∈ ℱ (DF B)› ‹v = x # t›
      using "3.prems" Cons_F_DF by (auto simp add: Sync.sym emptyLeftProperty)
    have ** : ‹t setinterleaves ((t, []), Z)›
      by (metis "*"(4) "3.prems"(3) Sync.sym SyncTlEmpty list.sel(3))
    from "3.prems"(1) obtain a where  *** : ‹a ∈ A› ‹x = ev a›
      by (subst (asm) F_DF, simp split: if_split_asm) blast
    show ?case
      apply (rule disjI1, rule_tac x = a in bexI)
      using "3.hyps"[simplified, OF *(1, 2, 3) **] 
      by (subst F_DF) (auto simp add: *(4) ***)
  next

    case (4 x t Z y u)
    consider ‹x ∈ Z› ‹y ∈ Z› | ‹x ∈ Z› ‹y ∉ Z›
          |  ‹x ∉ Z› ‹y ∈ Z› | ‹x ∉ Z› ‹y ∉ Z› by blast
    then show ?case
    proof (cases)
      assume hyps: ‹x ∈ Z› ‹y ∈ Z›
      obtain v' where * : ‹x = y› ‹(t, X) ∈ ℱ (DF A)›
                          ‹(u, Y) ∈ ℱ (DF B)› ‹v = x # v'›
        using "4.prems" Cons_F_DF by (simp add: hyps split: if_split_asm) blast
      have ** : ‹v' setinterleaves ((t, u), Z)›
        using "*"(1, 4) "4.prems"(3) hyps(1) by force
      from "4.prems"(1) obtain a where  *** : ‹a ∈ A› ‹x = ev a›
        by (subst (asm) F_DF, simp split: if_split_asm) blast
      show ?case
        apply (rule disjI1, rule_tac x = a in bexI)
        using "4.hyps"(1)[simplified, OF hyps(2) *(1, 2, 3) **] 
        by (subst F_DF) (auto simp add: *(4) ***)
    next
      assume hyps: ‹x ∈ Z› ‹y ∉ Z›
      obtain v' where * : ‹(x # t, X) ∈ ℱ (DF A)› ‹(u, Y) ∈ ℱ (DF B)›
                          ‹v = y # v'› ‹v' setinterleaves ((x # t, u), Z)›
        using "4.prems" Cons_F_DF by (simp add: hyps split: if_split_asm) blast
      from "4.prems"(2) "4.hyps"(2)[simplified, OF hyps *(1, 2, 4)]
      show ?case by (subst (asm) F_DF, subst F_DF) 
                      (auto simp add: nonempty *(3))
    next
      assume hyps: ‹x ∉ Z› ‹y ∈ Z›
      obtain v' where * : ‹(t, X) ∈ ℱ (DF A)› ‹(y # u, Y) ∈ ℱ (DF B)›
                          ‹v = x # v'› ‹v' setinterleaves ((t, y # u), Z)›
        using "4.prems" Cons_F_DF by (simp add: hyps split: if_split_asm) blast
      from "4.prems"(1) "4.hyps"(5)[simplified, OF hyps *(1, 2, 4)]
      show ?case by (subst (asm) F_DF, subst F_DF) 
                      (auto simp add: nonempty *(3))
    next
      assume hyps: ‹x ∉ Z› ‹y ∉ Z›
      note f4 = "4"[simplified, simplified hyps, simplified]
      from f4(8) obtain v' v''
        where ‹v = x # v'  ∧ v'  setinterleaves ((t, y # u), Z) ∨ 
               v = y # v'' ∧ v'' setinterleaves ((x # t, u), Z)›
              (is ‹?left ∨ ?right›) by blast
      then consider ‹?left› | ‹?right› by fast
      then show ?thesis 
      proof cases
        assume ‹?left›
        from f4(6) f4(3)[OF f4(6)[THEN Cons_F_DF] f4(7)
             ‹?left›[THEN conjunct2]]
        show ?thesis by (subst (asm) F_DF, subst F_DF)
                        (auto simp add:  ‹?left› nonempty)
      next
        assume ‹?right›
        from f4(7) f4(4)[OF f4(6) f4(7)[THEN Cons_F_DF] 
             ‹?right›[THEN conjunct2]]
        show ?thesis by (subst (asm) F_DF, subst F_DF)
                        (auto simp add: ‹?right› nonempty)
      qed
    qed
  qed
qed


lemma DF_FD_DF_Sync_DF:
  ‹A ≠ {} ∧ B ≠ {} ⟹ B ∩ S = {} ∨ (∃y. B ∩ S = {y} ∧ A ∩ S ⊆ {y}) ⟹ 
   DF (A ∪ B) ⊑⇩F⇩D DF A ⟦S⟧ DF B›
  unfolding failure_divergence_refine_def le_ref_def 
  by (simp add: div_free_DF D_Sync)
     (simp add: DF_F_DF_Sync_DF[unfolded failure_refine_def])

theorem DF_FD_DF_Sync_DF_iff:
  ‹DF (A ∪ B) ⊑⇩F⇩D DF A ⟦S⟧ DF B ⟷ 
   (     if A = {} then B ∩ S = {}
    else if B = {} then A ∩ S = {}
    else A ∩ S = {} ∨ (∃a. A ∩ S = {a} ∧ B ∩ S ⊆ {a}) ∨
         B ∩ S = {} ∨ (∃b. B ∩ S = {b} ∧ A ∩ S ⊆ {b}))›
  (is ‹?FD_ref ⟷ (     if A = {} then B ∩ S = {}
                    else if B = {} then A ∩ S = {} 
                    else ?cases)›)
proof -
  { assume ‹A ≠ {}› and ‹B ≠ {}› and ?FD_ref and ‹¬ ?cases›
    from ‹¬ ?cases›[simplified] 
    obtain a and b where ‹a ∈ A› ‹a ∈ S› ‹b ∈ B› ‹b ∈ S› ‹a ≠ b› by blast
    have ‹DF A ⟦S⟧ DF B ⊑⇩F⇩D (a → DF A) ⟦S⟧ (b → DF B)›
      by (intro mono_Sync_FD; subst DF_unfold,
          subst Mndetprefix_unit[symmetric], simp add: ‹a ∈ A› ‹b ∈ B›)
    also have ‹… = STOP› by (simp add: ‹a ∈ S› ‹a ≠ b› ‹b ∈ S› prefix_Sync1)
    finally have False
      by (metis DF_Univ_freeness Un_empty ‹A ≠ {}›
                trans_FD[OF ‹?FD_ref›] non_deadlock_free_STOP)
  }
  thus ?thesis
    apply (cases ‹A = {}›, simp,
           metis DF_FD_DF_Sync_STOP_iff DF_unfold Sync_commute mt_Mndetprefix)
    apply (cases ‹B = {}›, simp,
           metis DF_FD_DF_Sync_STOP_iff DF_unfold Sync_commute mt_Mndetprefix)
    by (metis Sync_commute Un_commute DF_FD_DF_Sync_DF)
qed 

  



lemma
  ‹(∀a ∈ A. X a ∩ S = {} ∨ (∀b ∈ A. ∃y. X a ∩ S = {y} ∧ X b ∩ S ⊆ {y}))
   ⟷ (∀a ∈ A. ∀b ∈ A. ∃y. (X a ∪ X b) ∩ S ⊆ {y})›
 ― ‹this is the reason we write ugly\_hyp this way›
  apply (subst Int_Un_distrib2, auto)
  by (metis subset_insertI) blast


lemma DF_FD_DF_MultiSync_DF:
  ‹DF (⋃ x ∈ (insert a A). X x) ⊑⇩F⇩D ❙⟦S❙⟧ x ∈# mset_set (insert a A). DF (X x)›
  if fin: ‹finite A› and nonempty: ‹X a ≠ {}› ‹∀b ∈ A. X b ≠ {}›
 and ugly_hyp: ‹∀b ∈ A. X b ∩ S = {} ∨ (∃y. X b ∩ S = {y} ∧ X a ∩ S ⊆ {y})›
               ‹∀b ∈ A. ∀c ∈ A. ∃y. (X b ∪ X c) ∩ S ⊆ {y}›
proof -
  have ‹DF (⋃ (X ` insert a A)) ⊑⇩F⇩D (❙⟦S❙⟧ x ∈# mset_set (insert a A). DF (X x)) ∧
        (∀b∈A. X b ∩ S = {} ∨ (∃y. X b ∩ S = {y} ∧ ⋃ (X ` insert a A) ∩ S ⊆ {y}))›
  ― ‹We need to add this in our induction›
  proof (induct rule: finite_subset_induct_singleton'
                      [of a ‹insert a A›, simplified, OF fin, 
                       simplified subset_insertI, simplified])
    case 1
    show ?case by (simp add: ugly_hyp)
  next
    case (2 b A') 
    show ?case
    proof (rule conjI; subst image_insert, subst Union_insert)
      show ‹DF (X b ∪ ⋃ (X ` insert a A')) ⊑⇩F⇩D
            ❙⟦S❙⟧ a∈#mset_set (insert b (insert a A')).  DF (X a)›
        apply (subst Un_commute)
        apply (rule trans_FD[OF DF_FD_DF_Sync_DF[where S = S]])
          apply (simp add: "2.hyps"(2) nonempty ugly_hyp(1))
        using "2.hyps"(2, 5) 
         apply blast
        apply (subst Sync_commute,
               rule trans_FD[OF mono_Sync_FD
                                [OF idem_FD "2.hyps"(5)[THEN conjunct1]]])
        by (simp add: "2.hyps"(1, 4) mset_set_empty_iff)
    next
      show ‹∀c ∈ A. X c ∩ S = {} ∨ (∃y. X c ∩ S = {y} ∧ 
                    (X b ∪ ⋃ (X ` insert a A')) ∩ S ⊆ {y})›
        apply (subst Int_Un_distrib2, subst Un_subset_iff)
        by (metis "2.hyps"(2, 5) Int_Un_distrib2 Un_subset_iff 
                  subset_singleton_iff ugly_hyp(2))
    qed
  qed
  thus ?thesis by (rule conjunct1)
qed



lemma DF_FD_DF_MultiSync_DF':
  ‹⟦finite A; ∀a ∈ A. X a ≠ {}; ∀a ∈ A. ∀b ∈ A. ∃y. (X a ∪ X b) ∩ S ⊆ {y}⟧
   ⟹ DF (⋃ a ∈ A. X a) ⊑⇩F⇩D ❙⟦S❙⟧ a ∈# mset_set A. DF (X a)›
  apply (cases A rule: finite.cases, assumption)
   apply (metis DF_unfold MultiSync_rec0 UN_empty idem_FD
                mset_set.empty mt_Mndetprefix)
  apply clarify
  apply (rule DF_FD_DF_MultiSync_DF)
  by simp_all (metis Int_Un_distrib2 Un_subset_iff subset_singleton_iff)


  
lemmas DF_FD_DF_MultiInter_DF  = 
       DF_FD_DF_MultiSync_DF'[where S = ‹{}›, simplified]
   and   DF_FD_DF_MultiPar_DF  = 
       DF_FD_DF_MultiSync_DF [where S = UNIV, simplified]
   and   DF_FD_DF_MultiPar_DF' = 
       DF_FD_DF_MultiSync_DF'[where S = UNIV, simplified]



lemma ‹DF {a} = DF {a} ⟦S⟧ STOP ⟷ a ∉ S›
  by (metis DF_FD_DF_Sync_STOP_iff DF_Sync_STOP_FD_DF Diff_disjoint 
            Diff_insert_absorb FD_antisym insert_disjoint(2))

lemma ‹DF {a} ⟦S⟧ STOP = STOP ⟷ a ∈ S› 
  by (metis DF_FD_DF_Sync_STOP_iff DF_unfold Diff_disjoint Sync_SKIP_STOP
            Diff_insert_absorb Mndetprefix_unit Sync_STOP_STOP
            Sync_assoc UNIV_I insert_disjoint(2) prefix_Sync_SKIP2)
 

corollary DF_FD_DF_Inter_DF: ‹DF (A::'α set) ⊑⇩F⇩D DF A ||| DF A›
  by (metis DF_FD_DF_Sync_DF_iff inf_bot_right sup.idem)

corollary DF_UNIV_FD_DF_UNIV_Inter_DF_UNIV:
  ‹DF UNIV ⊑⇩F⇩D DF UNIV ||| DF UNIV›
  by (fact DF_FD_DF_Inter_DF)

corollary Inter_deadlock_free:
  ‹deadlock_free P ⟹ deadlock_free Q ⟹ deadlock_free (P ||| Q)›
  using DF_FD_DF_Inter_DF deadlock_free_of_Sync_iff_DF_FD_DF_Sync_DF by blast


theorem MultiInter_deadlock_free:
  ‹M ≠ {#} ⟹ ∀p ∈# M. deadlock_free (P p) ⟹
   deadlock_free (❙|❙|❙| p ∈# M. P p)›
proof (induct rule: mset_induct_nonempty)
  case (m_singleton a)
  thus ?case by simp
next
  case (add x F)
  thus ?case using Inter_deadlock_free by auto
qed


end