Theory CSPM_Deadlock_Results

(*<*)
―‹ ********************************************************************
 * Project         : HOL-CSPM - Architectural operators for HOL-CSP
 *
 * Author          : Benoît Ballenghien, Safouan Taha, Burkhart Wolff.
 *
 * This file       : Powerful results on DF and deadlock freeness
 *
 * Copyright (c) 2025 Université Paris-Saclay, France
 *
 * All rights reserved.
 *
 * Redistribution and use in source and binary forms, with or without
 * modification, are permitted provided that the following conditions are
 * met:
 *
 *     * Redistributions of source code must retain the above copyright
 *       notice, this list of conditions and the following disclaimer.
 *
 *     * Redistributions in binary form must reproduce the above
 *       copyright notice, this list of conditions and the following
 *       disclaimer in the documentation and/or other materials provided
 *       with the distribution.
 *
 *     * Neither the name of the copyright holders nor the names of its
 *       contributors may be used to endorse or promote products derived
 *       from this software without specific prior written permission.
 *
 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
 * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
 * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
 * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
 * OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
 * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
 * LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
 * DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
 * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
 * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
 * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 ******************************************************************************›
(*>*)


chapter ‹ Deadlock results ›

(*<*)
theory CSPM_Deadlock_Results
  imports CSPM_Laws CSPM_Monotonies
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⇩S››

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

      @{thm deadlock_free_def[of P] deadlock_free⇩S⇩K⇩I⇩P⇩S_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 (⋃a∈A. {[]} × {X. ev a ∉ X} ∪ {(ev a # s, X)| s X. (s, X) ∈ ℱ (DF A)}))›
  by (subst DF_unfold) (auto simp add: F_STOP F_Mndetprefix write0_def F_Mprefix)


lemma F_DF⇩S⇩K⇩I⇩P⇩S: 
  ‹ℱ (DF⇩S⇩K⇩I⇩P⇩S A R) =
   (  if A = {} then {(s, X). s = [] ∨ (∃r∈R. s = [✓(r)])}
    else (⋃a∈A. {[]} × {X. ev a ∉ X} ∪ 
                 {(ev a # s, X)| s X. (s, X) ∈ ℱ (DF⇩S⇩K⇩I⇩P⇩S A R)}) ∪
         (  if R = {} then {(s, X). s = []}
          else {([], X) |X. ∃r∈R. ✓(r) ∉ X} ∪ {(s, X). ∃r∈R. s = [✓(r)]}))›
  by (subst DF⇩S⇩K⇩I⇩P⇩S_unfold, simp add: F_Ndet F_STOP F_SKIPS F_Mndetprefix write0_def F_Mprefix, safe, simp_all)


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


lemma D_DF: ‹𝒟 (DF A) = (if A = {} then {} else {ev a # s| a s. a ∈ A ∧ s ∈ 𝒟 (DF A)})›
  and D_DF⇩S⇩K⇩I⇩P⇩S: ‹𝒟 (DF⇩S⇩K⇩I⇩P⇩S A R) = (if A = {} then {} else {ev a # s| a s. a ∈ A ∧ s ∈ 𝒟 (DF⇩S⇩K⇩I⇩P⇩S A R)})›
  by (subst DF_unfold DF⇩S⇩K⇩I⇩P⇩S_unfold; 
      auto simp add: D_Mndetprefix D_Mprefix write0_def D_Ndet D_SKIPS)+

lemma T_DF: 
  ‹𝒯 (DF A) = (if A = {} then {[]} else insert [] {ev a # s| a s. a ∈ A ∧ s ∈ 𝒯 (DF A)})›
  and T_DF⇩S⇩K⇩I⇩P⇩S: 
  ‹𝒯 (DF⇩S⇩K⇩I⇩P⇩S A R) = (if A = {} then insert [] {[✓(r)] |r. r ∈ R}
    else {s. s = [] ∨ (∃r∈R. s = [✓(r)]) ∨ 
             s ≠ [] ∧ (∃a∈A. hd s = ev a ∧ tl s ∈ 𝒯 (DF⇩S⇩K⇩I⇩P⇩S A R))})›
  by (subst DF_unfold DF⇩S⇩K⇩I⇩P⇩S_unfold;
      auto simp add: T_STOP T_Mndetprefix write0_def T_Mprefix T_Ndet T_SKIPS)+
    (metis list.collapse)


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

text ‹We want more results like @{thm deadlock_free_Ndet_iff[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⇩S P ≡ DF⇩S⇩K⇩I⇩P⇩S UNIV UNIV ⊑⇩F P›
  by (fact deadlock_free⇩S⇩K⇩I⇩P⇩S_def)

lemma deadlock_free_F: ‹deadlock_free P ⟷ DF UNIV ⊑⇩F P›
  by (auto simp add: deadlock_free_def refine_defs F_subset_imp_T_subset
      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⇩S_Mprefix_iff: ‹deadlock_free⇩S⇩K⇩I⇩P⇩S (Mprefix A P) ⟷ 
                                     A ≠ {} ∧ (∀a ∈ A. deadlock_free⇩S⇩K⇩I⇩P⇩S (P a))›
  unfolding deadlock_free_F deadlock_free⇩S⇩K⇩I⇩P⇩S_def failure_refine_def
   apply (all ‹subst F_DF F_DF⇩S⇩K⇩I⇩P⇩S›,
      auto simp add: div_free_DF F_Mprefix D_Mprefix subset_iff)
  by blast+


lemma deadlock_free_read_iff :
  ‹deadlock_free (c❙?a∈A → P a) ⟷ A ≠ {} ∧ (∀a∈c ` A. deadlock_free ((P ∘ inv_into A c) a))›
  and deadlock_free⇩S⇩K⇩I⇩P⇩S_read_iff :
  ‹deadlock_free⇩S⇩K⇩I⇩P⇩S (c❙?a∈A → P a) ⟷ A ≠ {} ∧ (∀a∈c ` A. deadlock_free⇩S⇩K⇩I⇩P⇩S ((P ∘ inv_into A c) a))›
  by (simp_all add: read_def deadlock_free_Mprefix_iff deadlock_free⇩S⇩K⇩I⇩P⇩S_Mprefix_iff) 

lemma deadlock_free_read_inj_on_iff :
  ‹inj_on c A ⟹ deadlock_free (c❙?a∈A → P a) ⟷ A ≠ {} ∧ (∀a∈A. deadlock_free (P a))›
  and deadlock_free⇩S⇩K⇩I⇩P⇩S_read_inj_on_iff :
  ‹inj_on c A ⟹ deadlock_free⇩S⇩K⇩I⇩P⇩S (c❙?a∈A → P a) ⟷ A ≠ {} ∧ (∀a∈A. deadlock_free⇩S⇩K⇩I⇩P⇩S (P a))›
  by (simp_all add: deadlock_free_read_iff deadlock_free⇩S⇩K⇩I⇩P⇩S_read_iff)

lemma deadlock_free_write_iff :
  ‹deadlock_free (c❙!a → P) ⟷ deadlock_free P›
  and deadlock_free⇩S⇩K⇩I⇩P⇩S_write_iff :
  ‹deadlock_free⇩S⇩K⇩I⇩P⇩S (c❙!a → P) ⟷ deadlock_free⇩S⇩K⇩I⇩P⇩S P›
  by (simp_all add: deadlock_free_Mprefix_iff deadlock_free⇩S⇩K⇩I⇩P⇩S_Mprefix_iff write_def)

lemma deadlock_free_write0_iff :
  ‹deadlock_free (a → P) ⟷ deadlock_free P›
  and deadlock_free⇩S⇩K⇩I⇩P⇩S_write0_iff :
  ‹deadlock_free⇩S⇩K⇩I⇩P⇩S (a → P) ⟷ deadlock_free⇩S⇩K⇩I⇩P⇩S P›
  by (simp_all add: deadlock_free_Mprefix_iff deadlock_free⇩S⇩K⇩I⇩P⇩S_Mprefix_iff write0_def)

(* TODO: see what we declare simp *)


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⇩S_GlobalNdet_iff: ‹deadlock_free⇩S⇩K⇩I⇩P⇩S (⊓ a ∈ A. P a) ⟷
                                        A ≠ {} ∧ (∀ a ∈ A. deadlock_free⇩S⇩K⇩I⇩P⇩S (P a))›
  by (metis (mono_tags, lifting) GlobalNdet_refine_FD deadlock_free_def trans_FD
      mono_GlobalNdet_FD_const non_deadlock_free_STOP GlobalNdet_empty)
    (metis (mono_tags, lifting) GlobalNdet_refine_FD deadlock_free⇩S⇩K⇩I⇩P⇩S_FD trans_FD
      mono_GlobalNdet_FD_const non_deadlock_free⇩S⇩K⇩I⇩P⇩S_STOP GlobalNdet_empty)



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⇩S_Mndetprefix_iff: ‹deadlock_free⇩S⇩K⇩I⇩P⇩S (⊓ a ∈ A → P a) ⟷ 
                                         A ≠ {} ∧ (∀a∈A. deadlock_free⇩S⇩K⇩I⇩P⇩S (P a))›
  by (simp_all add: Mndetprefix_GlobalNdet
      deadlock_free_GlobalNdet_iff deadlock_free⇩S⇩K⇩I⇩P⇩S_GlobalNdet_iff
      deadlock_free_write0_iff deadlock_free⇩S⇩K⇩I⇩P⇩S_write0_iff)


(* TODO: remove this from here *)
lemma deadlock_free_Ndet_iff: ‹deadlock_free (P ⊓ Q) ⟷ 
                               deadlock_free P ∧ deadlock_free Q› 
  and deadlock_free⇩S⇩K⇩I⇩P⇩S_Ndet_iff: ‹deadlock_free⇩S⇩K⇩I⇩P⇩S (P ⊓ Q) ⟷
                                  deadlock_free⇩S⇩K⇩I⇩P⇩S P ∧ deadlock_free⇩S⇩K⇩I⇩P⇩S Q›
  unfolding deadlock_free_F deadlock_free⇩S⇩K⇩I⇩P⇩S_def failure_refine_def
  by (simp_all add: F_Ndet)



lemma deadlock_free_is_right: (* see OpSem *)
  ‹deadlock_free (P :: ('a, 'r) process⇩p⇩t⇩i⇩c⇩k) ⟷ (∀s ∈ 𝒯 P. tickFree s ∧ (s,      UNIV) ∉ ℱ P)›
  ‹deadlock_free  P                ⟷ (∀s ∈ 𝒯 P. tickFree s ∧ (s, ev ` UNIV) ∉ ℱ P)›
  oops


(* TODO: do something here *)

lemma ‹deadlock_free (P □ Q) ⟷ P = STOP ∧ deadlock_free Q ∨ deadlock_free P ∧ Q = STOP›
  (*  apply (simp add: deadlock_free_is_right(2))
  apply (simp add: Det_projs, safe)
                      apply simp_all *)
  oops



lemma deadlock_free_GlobalDet :
  ‹⟦A ≠ {}; ⋀a. a ∈ A ⟹ deadlock_free (P a)⟧ ⟹ deadlock_free (□a ∈ A. P a)›
  and deadlock_free⇩S⇩K⇩I⇩P⇩S_GlobalDet:
  ‹⟦A ≠ {}; ⋀a. a ∈ A ⟹ deadlock_free⇩S⇩K⇩I⇩P⇩S (P a)⟧ ⟹ deadlock_free⇩S⇩K⇩I⇩P⇩S (□a ∈ A. P a)›
  by (metis GlobalNdet_FD_GlobalDet deadlock_free_GlobalNdet_iff deadlock_free_def trans_FD)
    (metis GlobalNdet_FD_GlobalDet deadlock_free⇩S⇩K⇩I⇩P⇩S_FD deadlock_free⇩S⇩K⇩I⇩P⇩S_GlobalNdet_iff trans_FD)



lemma deadlock_free_Det:
  ‹deadlock_free    P ⟹ deadlock_free    Q ⟹ deadlock_free    (P □ Q)›
  and deadlock_free⇩S⇩K⇩I⇩P⇩S_Det:
  ‹deadlock_free⇩S⇩K⇩I⇩P⇩S P ⟹ deadlock_free⇩S⇩K⇩I⇩P⇩S Q ⟹ deadlock_free⇩S⇩K⇩I⇩P⇩S (P □ Q)›
  by (metis deadlock_free_Ndet_iff Ndet_FD_Det deadlock_free_def trans_FD)
    (metis deadlock_free⇩S⇩K⇩I⇩P⇩S_Ndet_iff Ndet_F_Det deadlock_free⇩S⇩K⇩I⇩P⇩S_def trans_F)



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⇩S P ∧ ¬ deadlock_free⇩S⇩K⇩I⇩P⇩S Q ∧ 
         deadlock_free⇩S⇩K⇩I⇩P⇩S (P □ Q)›
  by (rule_tac x = ‹DF UNIV› in exI, rule_tac x = STOP in exI, 
      simp add: non_deadlock_free_STOP, simp add: deadlock_free_def)
    (rule_tac x = ‹DF⇩S⇩K⇩I⇩P⇩S UNIV UNIV› in exI, rule_tac x = STOP in exI,
      simp add: non_deadlock_free⇩S⇩K⇩I⇩P⇩S_STOP, simp add: deadlock_free⇩S⇩K⇩I⇩P⇩S_FD)




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 failure_refine_def divergence_refine_def
      subset_iff D_Mndetprefix F_Mndetprefix write0_def D_Mprefix F_Mprefix)


lemma Mndetprefix_FD: ‹(∃a ∈ A. (a → Q) ⊑⇩F⇩D P) ⟹ ⊓ a ∈ A → Q ⊑⇩F⇩D P›
  by (metis FD_Mndetprefix_iff ex_in_conv idem_FD 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
    by (elim disjE, all ‹subst Mprefix_Sync_Mprefix_bis[OF assms(2-5)]›)
      (use assms(6-8) in ‹auto intro!: deadlock_free_Det deadlock_free_Mprefix_iff[THEN iffD2]›)
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.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 g›
proof (subst DF_def, induct rule: fix_ind)
  show ‹adm (λa. a ⊑⇩F⇩D Renaming (DF A) f g)› by (simp add: monofun_def)
next
  show ‹⊥ ⊑⇩F⇩D Renaming (DF A) f g› by simp
next
  show ‹(Λ x. ⊓a ∈ f ` A →  x)⋅x ⊑⇩F⇩D Renaming (DF A) f g›
    if ‹x ⊑⇩F⇩D Renaming (DF A) f g› for x
    apply simp
    apply (subst DF_unfold)
    apply (subst Renaming_Mndetprefix)
    by (auto simp add: that intro!: mono_Mndetprefix_FD)
qed

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


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

(* TODO: move this *)


lemma Renaming_SKIPS [simp] : ‹Renaming (SKIPS R) f g = SKIPS (g ` R)›
  by (simp add: SKIPS_def Renaming_distrib_GlobalNdet)
    (metis mono_GlobalNdet_eq2)


lemma DF⇩S⇩K⇩I⇩P⇩S_FD_Renaming_DF⇩S⇩K⇩I⇩P⇩S:
  ‹DF⇩S⇩K⇩I⇩P⇩S (f ` A) (g ` R) ⊑⇩F⇩D Renaming (DF⇩S⇩K⇩I⇩P⇩S A R) f g›
proof (subst DF⇩S⇩K⇩I⇩P⇩S_def, induct rule: fix_ind)
  show ‹adm (λa. a ⊑⇩F⇩D Renaming (DF⇩S⇩K⇩I⇩P⇩S A R) f g)› by (simp add: monofun_def)
next
  show ‹⊥ ⊑⇩F⇩D Renaming (DF⇩S⇩K⇩I⇩P⇩S A R) f g› by simp
next
  show ‹(Λ x. (⊓ a∈f ` A →  x) ⊓ SKIPS (g ` R))⋅x ⊑⇩F⇩D Renaming (DF⇩S⇩K⇩I⇩P⇩S A R) f g›
    if ‹x ⊑⇩F⇩D Renaming (DF⇩S⇩K⇩I⇩P⇩S A R) f g› for x
    by (subst DF⇩S⇩K⇩I⇩P⇩S_unfold)
      (auto simp add: Renaming_Ndet Renaming_Mndetprefix
        intro!: mono_Ndet_FD mono_Mndetprefix_FD that)
qed

lemma Renaming_DF⇩S⇩K⇩I⇩P⇩S_FD_DF⇩S⇩K⇩I⇩P⇩S:
  ‹Renaming (DF⇩S⇩K⇩I⇩P⇩S A R) f g ⊑⇩F⇩D DF⇩S⇩K⇩I⇩P⇩S (f ` A) (g ` R)›
  if finitary: ‹finitary f› ‹finitary g›
proof (subst DF⇩S⇩K⇩I⇩P⇩S_def, induct rule: fix_ind)
  show ‹adm (λa. Renaming a f g ⊑⇩F⇩D DF⇩S⇩K⇩I⇩P⇩S (f ` A) (g ` R))›
    by (simp add: finitary monofun_def)
next
  show ‹Renaming ⊥ f g ⊑⇩F⇩D DF⇩S⇩K⇩I⇩P⇩S (f ` A) (g ` R)› by simp
next
  show ‹Renaming ((Λ x. (⊓a ∈ A →  x) ⊓ SKIPS R)⋅x) f g ⊑⇩F⇩D DF⇩S⇩K⇩I⇩P⇩S (f ` A) (g ` R)›
    if ‹Renaming x f g ⊑⇩F⇩D DF⇩S⇩K⇩I⇩P⇩S (f ` A) (g ` R)› for x
    by (subst DF⇩S⇩K⇩I⇩P⇩S_unfold)
      (auto simp add: Renaming_Ndet Renaming_Mndetprefix
        intro!: mono_Ndet_FD mono_Mndetprefix_FD that)
qed



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

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

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


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

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

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


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

lemma CHAOS⇩S⇩K⇩I⇩P⇩S_FD_Renaming_CHAOS⇩S⇩K⇩I⇩P⇩S:
  ‹CHAOS⇩S⇩K⇩I⇩P⇩S (f ` A) (g ` R) ⊑⇩F⇩D Renaming (CHAOS⇩S⇩K⇩I⇩P⇩S A R) f g›
proof (subst CHAOS⇩S⇩K⇩I⇩P⇩S_def, induct rule: fix_ind)
  show ‹adm (λa. a ⊑⇩F⇩D Renaming (CHAOS⇩S⇩K⇩I⇩P⇩S A R) f g)›
    by (simp add: monofun_def)
next
  show ‹⊥ ⊑⇩F⇩D Renaming (CHAOS⇩S⇩K⇩I⇩P⇩S A R) f g› by simp
next
  show ‹(Λ x. SKIPS (g ` R) ⊓ STOP ⊓ (□xa∈f ` A → x))⋅x ⊑⇩F⇩D 
        Renaming (CHAOS⇩S⇩K⇩I⇩P⇩S A R) f g›
    if ‹x ⊑⇩F⇩D Renaming (CHAOS⇩S⇩K⇩I⇩P⇩S A R) f g› for x
    by (subst CHAOS⇩S⇩K⇩I⇩P⇩S_unfold)
      (auto simp add: Renaming_Ndet Renaming_Mprefix
        intro!: mono_Ndet_FD mono_Mprefix_FD that)
qed

lemma Renaming_CHAOS⇩S⇩K⇩I⇩P⇩S_FD_CHAOS⇩S⇩K⇩I⇩P⇩S:
  ‹Renaming (CHAOS⇩S⇩K⇩I⇩P⇩S A R) f g ⊑⇩F⇩D CHAOS⇩S⇩K⇩I⇩P⇩S (f ` A) (g ` R)›
  if finitary: ‹finitary f› ‹finitary g›
proof (subst CHAOS⇩S⇩K⇩I⇩P⇩S_def, induct rule: fix_ind)
  show ‹adm (λa. Renaming a f g ⊑⇩F⇩D CHAOS⇩S⇩K⇩I⇩P⇩S (f ` A) (g ` R))›
    by (simp add: finitary monofun_def)
next
  show ‹Renaming ⊥ f g ⊑⇩F⇩D CHAOS⇩S⇩K⇩I⇩P⇩S (f ` A) (g ` R)› by simp
next
  show ‹ Renaming ((Λ x. SKIPS R ⊓ STOP ⊓ (□xa∈A → x))⋅x) f g ⊑⇩F⇩D CHAOS⇩S⇩K⇩I⇩P⇩S (f ` A) (g ` R)›
    if ‹Renaming x f g ⊑⇩F⇩D CHAOS⇩S⇩K⇩I⇩P⇩S (f ` A) (g ` R)› for x
    by (subst CHAOS⇩S⇩K⇩I⇩P⇩S_unfold)
      (auto simp add: Renaming_Ndet Renaming_Mprefix
        intro!: mono_Ndet_FD mono_Mprefix_FD that)
qed



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

lemmas Renaming_DF = 
  FD_antisym[OF Renaming_DF_FD_DF DF_FD_Renaming_DF]
  and Renaming_DF⇩S⇩K⇩I⇩P⇩S =
  FD_antisym[OF Renaming_DF⇩S⇩K⇩I⇩P⇩S_FD_DF⇩S⇩K⇩I⇩P⇩S DF⇩S⇩K⇩I⇩P⇩S_FD_Renaming_DF⇩S⇩K⇩I⇩P⇩S]
  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⇩S =
  FD_antisym[OF Renaming_CHAOS⇩S⇩K⇩I⇩P⇩S_FD_CHAOS⇩S⇩K⇩I⇩P⇩S
    CHAOS⇩S⇩K⇩I⇩P⇩S_FD_Renaming_CHAOS⇩S⇩K⇩I⇩P⇩S]



lemma deadlock_free_imp_deadlock_free_Renaming: ‹deadlock_free (Renaming P f g)›
  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])

(* TODO: should be true without inj g since no tick in the traces *)
lemma deadlock_free_Renaming_imp_deadlock_free: ‹deadlock_free P›
  if ‹inj f› and ‹inj g› and ‹deadlock_free (Renaming P f g)›
  apply (subst Renaming_inv[OF that(1, 2), symmetric])
  apply (rule deadlock_free_imp_deadlock_free_Renaming)
  by (rule that(3))

corollary deadlock_free_Renaming_iff:
  ‹inj f ⟹ inj g ⟹ deadlock_free (Renaming P f g) ⟷ 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⇩S_imp_deadlock_free⇩S⇩K⇩I⇩P⇩S_Renaming:
  ‹deadlock_free⇩S⇩K⇩I⇩P⇩S P ⟹ deadlock_free⇩S⇩K⇩I⇩P⇩S (Renaming P f g)›
  unfolding deadlock_free⇩S⇩K⇩I⇩P⇩S_FD
  apply (rule trans_FD[of _ ‹DF⇩S⇩K⇩I⇩P⇩S (f ` UNIV) (g ` UNIV)›])
  by (simp add: DF⇩S⇩K⇩I⇩P⇩S_subset) (meson DF⇩S⇩K⇩I⇩P⇩S_FD_Renaming_DF⇩S⇩K⇩I⇩P⇩S mono_Renaming_FD trans_FD)


lemma deadlock_free⇩S⇩K⇩I⇩P⇩S_Renaming_imp_deadlock_free⇩S⇩K⇩I⇩P⇩S:
  ‹deadlock_free⇩S⇩K⇩I⇩P⇩S P› if ‹inj f› and ‹inj g› and ‹deadlock_free⇩S⇩K⇩I⇩P⇩S (Renaming P f g)›
  apply (subst Renaming_inv[OF that(1, 2), symmetric])
  apply (rule deadlock_free⇩S⇩K⇩I⇩P⇩S_imp_deadlock_free⇩S⇩K⇩I⇩P⇩S_Renaming)
  by (rule that(3))

corollary deadlock_free⇩S⇩K⇩I⇩P⇩S_Renaming_iff:
  ‹inj f ⟹ inj g ⟹ deadlock_free⇩S⇩K⇩I⇩P⇩S (Renaming P f g) ⟷ deadlock_free⇩S⇩K⇩I⇩P⇩S P›
  using deadlock_free⇩S⇩K⇩I⇩P⇩S_Renaming_imp_deadlock_free⇩S⇩K⇩I⇩P⇩S
    deadlock_free⇩S⇩K⇩I⇩P⇩S_imp_deadlock_free⇩S⇩K⇩I⇩P⇩S_Renaming by blast







section ‹The big results›

subsection ‹An interesting equivalence›

lemma deadlock_free_of_Sync_iff_DF_FD_DF_Sync_DF:
  ‹(∀P Q. deadlock_free (P::('a, 'r) process⇩p⇩t⇩i⇩c⇩k) ⟶ deadlock_free Q ⟶
          deadlock_free (P ⟦S⟧ Q))
   ⟷ (DF UNIV :: ('a, 'r) process⇩p⇩t⇩i⇩c⇩k) ⊑⇩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 r›
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)
        (* TODO: write lemmas with Sync Mprefix and STOP  *)
       apply (simp add: write0_def, subst Mprefix_empty[symmetric])
       apply (subst Mprefix_Sync_Mprefix_right, (simp_all add: f2)[3])
      by (subst DF_unfold, simp add: f2 write0_Sync_SKIP)
    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[of r] 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] that show ?thesis
        by (auto simp add: fix_const)
    next
      assume a3: ‹A ≠ {}›
      from a1 show ?thesis
        unfolding failure_divergence_refine_def failure_refine_def divergence_refine_def
      proof (auto simp add: F_Sync D_Sync D_P div_free_DF subset_iff, goal_cases)
        case (1 a t u X Y)
        then show ?case
        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.prems(1, 2, 4) F_T F_imp_front_tickFree Int_iff TickLeftSync
                append_T_imp_tickFree inf_sup_absorb is_processT5_S7 list.distinct(1)
                non_tickFree_tick rangeI setinterleaving_sym tickFree_Cons_iff tickFree_Nil tickFree_butlast)
          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) setinterleaving_sym
                SyncTlEmpty emptyLeftProperty f1 list.sel(3))
        qed
      qed
    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 r› 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)
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 Mndetprefix_FD_subset
              [of ‹{a}›, simplified, OF that] idem_FD]])
      apply (rule disjE[OF P_disj], simp_all)
       apply (subst Mprefix_Sync_Mprefix_left
          [of ‹{a}› _ ‹{}› ‹λa. x›, simplified, folded write0_def])
      using empty_inter that apply blast
      using "3" mono_write0_FD apply fast
      by (metis "3" disjoint_iff empty_inter mono_write0_FD that write0_Sync_SKIP)
    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 r›, 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 r›, simplified] for r



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

theorem DF_F_DF_Sync_DF: ‹(DF (A ∪ B) :: ('a, 'r) process⇩p⇩t⇩i⇩c⇩k) ⊑⇩F DF A ⟦S⟧ DF B›
  if  nonempty: ‹A ≠ {} ∧ B ≠ {}›
    and intersect_hyp: ‹B ∩ S = {} ∨ (∃y. B ∩ S = {y} ∧ A ∩ S ⊆ {y})›
proof -
  let ?Z = ‹range tick ∪ ev ` S :: ('a, 'r) event⇩p⇩t⇩i⇩c⇩k set›
  have ‹⟦(t, X) ∈ ℱ (DF A); (u, Y) ∈ ℱ (DF B); v setinterleaves ((t, u), ?Z)⟧
        ⟹ (v, (X ∪ Y) ∩ ?Z ∪ X ∩ Y) ∈ ℱ (DF (A ∪ B))› for v t u :: ‹('a, 'r) trace⇩p⇩t⇩i⇩c⇩k› and X Y
  proof (induct ‹(t, ?Z, u)› arbitrary: t u v rule: setinterleaving.induct)
    case (1 v)
    from "1.prems"(3) emptyLeftProperty have ‹v = []› by blast
    with intersect_hyp "1.prems"(1, 2) show ?case
      by (subst (asm) (1 2) F_DF, subst F_DF) 
        (simp add: nonempty image_iff subset_iff, metis IntI empty_iff insertE)
  next
    case (2 y u)
    from "2.prems"(3) emptyLeftProperty obtain b
      where ‹b ∉ S› ‹y = ev b› ‹v = y # u› ‹u setinterleaves (([], u), ?Z)›
      by (cases y) (auto simp add: image_iff split: if_split_asm)
    from "2.prems"(2) have ‹b ∈ B› ‹(u, Y) ∈ ℱ (DF B)›
      by (subst (asm) F_DF; simp add: ‹y = ev b› nonempty)+
    have ‹(u, (X ∪ Y) ∩ ?Z ∪ X ∩ Y) ∈ ℱ (DF (A ∪ B))›
      by (rule "2.hyps")
        (simp_all add: "2.prems"(1) ‹(u, Y) ∈ ℱ (DF B)› ‹b ∉ S› ‹y = ev b›
          ‹u setinterleaves (([], u), ?Z)› image_iff)
    thus ?case by (subst F_DF) (simp add: nonempty ‹v = y # u› ‹y = ev b› ‹b ∈ B›)
  next
    case (3 x t)
    from "3.prems"(3) emptyRightProperty obtain a
      where ‹a ∉ S› ‹x = ev a› ‹v = x # t› ‹t setinterleaves ((t, []), ?Z)›
      by (cases x) (auto simp add: image_iff split: if_split_asm)
    from "3.prems"(1) have ‹a ∈ A› ‹(t, X) ∈ ℱ (DF A)›
      by (subst (asm) F_DF; simp add: ‹x = ev a› nonempty)+
    have ‹(t, (X ∪ Y) ∩ ?Z ∪ X ∩ Y) ∈ ℱ (DF (A ∪ B))›
      by (rule "3.hyps")
        (simp_all add: "3.prems"(2) ‹(t, X) ∈ ℱ (DF A)› ‹a ∉ S› ‹x = ev a›
          ‹t setinterleaves ((t, []), ?Z)› image_iff)
    thus ?case by (subst F_DF) (simp add: nonempty ‹v = x # t› ‹x = ev a› ‹a ∈ A›)
  next
    case (4 x t y u)
    from "4.prems"(1) obtain a where ‹a ∈ A› ‹x = ev a› ‹(t, X) ∈ ℱ (DF A)›
      by (subst (asm) F_DF) (auto simp add: nonempty)
    from "4.prems"(2) obtain b where ‹b ∈ B› ‹y = ev b› ‹(u, Y) ∈ ℱ (DF B)›
      by (subst (asm) F_DF) (auto simp add: nonempty)
    consider ‹x ∈ ?Z› ‹y ∈ ?Z› | ‹x ∈ ?Z› ‹y ∉ ?Z›
      | ‹x ∉ ?Z› ‹y ∈ ?Z› | ‹x ∉ ?Z› ‹y ∉ ?Z› by blast
    thus ?case
    proof cases
      assume ‹x ∈ ?Z› ‹y ∈ ?Z›
      with "4.prems"(3) obtain v'
        where ‹x = y› ‹v = y # v'› ‹v' setinterleaves ((t, u), ?Z)›
        by (simp split: if_split_asm) blast
      from "4.hyps"(1)[OF ‹x ∈ ?Z› ‹y ∈ ?Z› ‹x = y›
          ‹(t, X) ∈ ℱ (DF A)› ‹(u, Y) ∈ ℱ (DF B)› this(3)]
      have ‹(v', (X ∪ Y) ∩ ?Z ∪ X ∩ Y) ∈ ℱ (DF (A ∪ B))› .
      thus ?case by (subst F_DF) (simp add: nonempty ‹v = y # v'› ‹y = ev b› ‹b ∈ B›)
    next
      assume ‹x ∈ ?Z› ‹y ∉ ?Z›
      with "4.prems"(3) obtain v'
        where ‹v = y # v'› ‹v' setinterleaves ((x # t, u), ?Z)›
        by (simp split: if_split_asm) blast
      from "4.hyps"(2)[OF ‹x ∈ ?Z› ‹y ∉ ?Z› "4.prems"(1) ‹(u, Y) ∈ ℱ (DF B)› this(2)]
      have ‹(v', (X ∪ Y) ∩ ?Z ∪ X ∩ Y) ∈ ℱ (DF (A ∪ B))› .
      thus ?case by (subst F_DF) (simp add: nonempty ‹v = y # v'› ‹y = ev b› ‹b ∈ B›)
    next
      assume ‹x ∉ ?Z› ‹y ∈ ?Z›
      with "4.prems"(3) obtain v'
        where ‹v = x # v'› ‹v' setinterleaves ((t, y # u), ?Z)›
        by (simp split: if_split_asm) blast
      from "4.prems"(2) "4.hyps"(5) ‹x ∉ ?Z› ‹y ∈ ?Z› ‹(t, X) ∈ ℱ (DF A)› this(2)
      have ‹(v', (X ∪ Y) ∩ ?Z ∪ X ∩ Y) ∈ ℱ (DF (A ∪ B))› by simp
      thus ?case by (subst F_DF) (simp add: nonempty ‹v = x # v'› ‹x = ev a› ‹a ∈ A›)
    next
      assume ‹x ∉ ?Z› ‹y ∉ ?Z›
      with "4.prems"(3) obtain v'
        where ‹v = x # v' ∧ v' setinterleaves ((t, y # u), ?Z) ∨
               v = y # v' ∧ v' setinterleaves ((x # t, u), ?Z)› by auto
      thus ?case
      proof (elim disjE conjE)
        assume ‹v = x # v'› ‹v' setinterleaves ((t, y # u), ?Z)›
        from "4.hyps"(3)[OF ‹x ∉ ?Z› ‹y ∉ ?Z› ‹(t, X) ∈ ℱ (DF A)› "4.prems"(2) this(2)]
        have ‹(v', (X ∪ Y) ∩ ?Z ∪ X ∩ Y) ∈ ℱ (DF (A ∪ B))› .
        thus ?case by (subst F_DF) (simp add: nonempty ‹v = x # v'› ‹x = ev a› ‹a ∈ A›)
      next
        assume ‹v = y # v'› ‹v' setinterleaves ((x # t, u), ?Z)›
        from "4.hyps"(4)[OF ‹x ∉ ?Z› ‹y ∉ ?Z› "4.prems"(1) ‹(u, Y) ∈ ℱ (DF B)› this(2)]
        have ‹(v', (X ∪ Y) ∩ ?Z ∪ X ∩ Y) ∈ ℱ (DF (A ∪ B))› .
        thus ?case by (subst F_DF) (simp add: nonempty ‹v = y # v'› ‹y = ev b› ‹b ∈ B›)
      qed
    qed
  qed

  thus ‹(DF (A ∪ B) :: ('a, 'r) process⇩p⇩t⇩i⇩c⇩k) ⊑⇩F DF A ⟦S⟧ DF B›
    by (auto simp add: failure_refine_def F_Sync div_free_DF)
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 failure_refine_def divergence_refine_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)›)

  apply (cases ‹A = {}›, simp,
      metis DF_FD_DF_Sync_STOP_iff DF_unfold Sync_commute Mndetprefix_empty)
  apply (cases ‹B = {}›, simp,
      metis DF_FD_DF_Sync_STOP_iff DF_unfold Sync_commute Mndetprefix_empty)
proof (simp, intro iffI)
  { 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, meson Mndetprefix_FD_write0 ‹a ∈ A› ‹b ∈ B›)
    also have ‹… = STOP› by (simp add: ‹a ∈ S› ‹a ≠ b› ‹b ∈ S› write0_Sync_write0_subset)
    finally have False
      by (metis DF_Univ_freeness Un_empty ‹A ≠ {}›
          trans_FD[OF ‹?FD_ref›] non_deadlock_free_STOP)}
  thus ‹A ≠ {} ⟹ B ≠ {} ⟹ ?FD_ref ⟹ ?cases› by fast
qed (metis Sync_commute Un_commute DF_FD_DF_Sync_DF)





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) :: ('a, 'r) process⇩p⇩t⇩i⇩c⇩k) ⊑⇩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}›

  apply (rule conjunct1[where Q = ‹∀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) :: ('a, 'r) process⇩p⇩t⇩i⇩c⇩k)›
      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



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 (subst DF_unfold, simp)
  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 (no_types, lifting) DF_unfold Diff_disjoint Diff_eq_empty_iff Int_commute
      Int_insert_left Mndetprefix_Sync_STOP Mndetprefix_is_STOP_iff
      Ndet_is_STOP_iff empty_not_insert inf_le2)


corollary DF_FD_DF_Inter_DF: ‹DF A ⊑⇩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 ≠ {#}; ⋀m. m ∈# M ⟹ deadlock_free (P m)⟧ ⟹
   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) with Inter_deadlock_free show ?case by auto
qed

(*<*)
end
  (*>*)