Theory CSP_PTick_Deadlock_Results

(***********************************************************************************
 * Copyright (c) 2025 Université Paris-Saclay
 *
 * Author: Benoît Ballenghien, Université Paris-Saclay,
 *         CNRS, ENS Paris-Saclay, LMF
 *
 * 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
 *
 * * 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.
 *
 * 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 HOLDER 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.
 *
 * SPDX-License-Identifier: BSD-2-Clause
 ***********************************************************************************)


chapter ‹Deadlock Results›

(*<*)
theory CSP_PTick_Deadlock_Results
  imports "HOL-CSP_RS" Read_Write_CSP_PTick_Laws CSP_PTick_Monotonicities
    "HOL-CSP_OpSem" Events_Ticks_CSP_PTick_Laws
begin                                                                      
  (*>*)


section ‹First Results›

subsection ‹Non Terminating›

text ‹Keep in mind @{thm lifelock_free⇩S⇩K⇩I⇩P⇩S_iff_div_free[no_vars]}.›

subsubsection ‹Sequential Composition›

lemma ‹non_terminating P ⟹ P ❙;⇩✓ Q = RenamingTick P g›
  ― ‹Already proven earlier.›
  by (fact non_terminating_Seq⇩p⇩t⇩i⇩c⇩k)



subsubsection ‹Synchronization Product›

lemma (in Sync⇩p⇩t⇩i⇩c⇩k_locale) non_terminating_Sync⇩p⇩t⇩i⇩c⇩k :
  ‹non_terminating P ⟹ lifelock_free⇩S⇩K⇩I⇩P⇩S Q ⟹ non_terminating (P ⟦A⟧⇩✓ Q)›
  ‹lifelock_free⇩S⇩K⇩I⇩P⇩S P ⟹ non_terminating Q ⟹ non_terminating (P ⟦A⟧⇩✓ Q)›
  by (simp add: lifelock_free⇩S⇩K⇩I⇩P⇩S_iff_div_free T_Sync⇩p⇩t⇩i⇩c⇩k
      non_terminating_is_right nonterminating_implies_div_free,
      use setinterleaves⇩p⇩t⇩i⇩c⇩k_tickFree_imp in blast)+



subsection ‹Deadlock Free›

subsubsection ‹Sequential Composition›

lemma ‹deadlock_free P ⟹ deadlock_free (P ❙;⇩✓ Q)›
  by (metis deadlock_free_imp_deadlock_free_Renaming deadlock_free_implies_lifelock_free
            lifelock_free_is_non_terminating non_terminating_Seq⇩p⇩t⇩i⇩c⇩k)


text ‹The next lemma is of course more interesting.›

lemma deadlock_free⇩S⇩K⇩I⇩P⇩S_Seq⇩p⇩t⇩i⇩c⇩k :
  ‹deadlock_free⇩S⇩K⇩I⇩P⇩S (P ❙;⇩✓ Q)›
  if df_assms : ‹deadlock_free⇩S⇩K⇩I⇩P⇩S P› ‹⋀r. r ∈ ❙✓❙s(P) ⟹ deadlock_free⇩S⇩K⇩I⇩P⇩S (Q r)›
proof (unfold deadlock_free⇩S⇩K⇩I⇩P⇩S_is_right, intro ballI impI)
  show ‹t ∈ 𝒯 (P ❙;⇩✓ Q) ⟹ tF t ⟹ (t, UNIV) ∉ ℱ (P ❙;⇩✓ Q)› for t
  proof (induct t rule: rev_induct)
    from df_assms show ‹([], UNIV) ∉ ℱ (P ❙;⇩✓ Q)›
      by (simp add: Seq⇩p⇩t⇩i⇩c⇩k_projs deadlock_free⇩S⇩K⇩I⇩P⇩S_implies_div_free deadlock_free⇩S⇩K⇩I⇩P⇩S_is_right ref_Seq⇩p⇩t⇩i⇩c⇩k_UNIV)
        (metis F_T append_Nil deadlock_free⇩S⇩K⇩I⇩P⇩S_implies_div_free
               deadlock_free⇩S⇩K⇩I⇩P⇩S_is_right empty_iff strict_ticks_of_memI tickFree_Nil)
  next
    from df_assms(1) have ‹𝒟 P = {}›
      by (simp add: deadlock_free⇩S⇩K⇩I⇩P⇩S_implies_div_free)
    fix t e assume hyp : ‹t ∈ 𝒯 (P ❙;⇩✓ Q) ⟹ tF t ⟹ (t, UNIV) ∉ ℱ (P ❙;⇩✓ Q)›
    assume ‹t @ [e] ∈ 𝒯 (P ❙;⇩✓ Q)› ‹tF (t @ [e])›
    then consider u v where ‹t @ [e] = map (ev ∘ of_ev) u› ‹u ∈ 𝒯 P› ‹tF u›
      | u r v where ‹t @ [e] = map (ev ∘ of_ev) u @ v› ‹u @ [✓(r)] ∈ 𝒯 P› ‹tF u› ‹v ∈ 𝒯 (Q r)›
      by (auto simp add: Seq⇩p⇩t⇩i⇩c⇩k_projs ‹𝒟 P = {}›)
    thus ‹(t @ [e], UNIV) ∉ ℱ (P ❙;⇩✓ Q)›
      by (cases; simp_all add: Seq⇩p⇩t⇩i⇩c⇩k_projs ref_Seq⇩p⇩t⇩i⇩c⇩k_UNIV)
        (metis (no_types) F_T ‹𝒟 P = {}› ‹tF (t @ [e])› deadlock_free⇩S⇩K⇩I⇩P⇩S_is_right
                          empty_iff strict_ticks_of_memI that tickFree_append_iff)+
  qed
qed


corollary deadlock_free_Seq⇩p⇩t⇩i⇩c⇩k :
  ‹⟦deadlock_free⇩S⇩K⇩I⇩P⇩S P; ⋀r. r ∈ ❙✓❙s(P) ⟹ deadlock_free (Q r)⟧
   ⟹ deadlock_free (P ❙;⇩✓ Q)›
  by (simp add: AfterExt.deadlock_free_iff_empty_ticks_of_and_deadlock_free⇩S⇩K⇩I⇩P⇩S ticks_of_Seq⇩p⇩t⇩i⇩c⇩k)
    (meson deadlock_free⇩S⇩K⇩I⇩P⇩S_Seq⇩p⇩t⇩i⇩c⇩k deadlock_free⇩S⇩K⇩I⇩P⇩S_implies_div_free)



subsubsection ‹Synchronization Product›

context Sync⇩p⇩t⇩i⇩c⇩k_locale begin

lemma deadlock_free_Det_bis :
  ‹P = STOP ∧ Q ≠ STOP ∨ deadlock_free P ⟹
   Q = STOP ∧ P ≠ STOP ∨ deadlock_free Q ⟹ deadlock_free (P □ Q)›
  using deadlock_free_Det by auto

lemma deadlock_free_Mprefix_Sync⇩p⇩t⇩i⇩c⇩k_Mprefix :
  assumes not_all_empty: ‹¬ A ⊆ S ∨ ¬ B ⊆ S ∨ A ∩ B ∩ S ≠ {}›
    and ‹⋀a. a ∈ A - S ⟹ deadlock_free (P a ⟦S⟧⇩✓ □b∈B → Q b)›
    and ‹⋀b. b ∈ B - S ⟹ deadlock_free (□a∈A → P a ⟦S⟧⇩✓ Q b)›
    and ‹⋀x. x ∈ A ∩ B ∩ S ⟹ deadlock_free (P x ⟦S⟧⇩✓ Q x)› 
  shows ‹deadlock_free (□a∈A → P a ⟦S⟧⇩✓ □b ∈ B → Q b)›
  unfolding Mprefix_Sync⇩p⇩t⇩i⇩c⇩k_Mprefix using not_all_empty
  by (auto intro!: deadlock_free_Det_bis
      simp add: Mprefix_is_STOP_iff Det_is_STOP_iff deadlock_free_Mprefix_iff assms(2-4))


lemma deadlock_free_Mprefix_Sync⇩p⇩t⇩i⇩c⇩k_Mprefix_subset :
  ‹⟦A ⊆ S; B ⊆ S; A ∩ B ≠ {};
    ⋀x. x ∈ A ∩ B ∩ S ⟹ deadlock_free (P x ⟦S⟧⇩✓ Q x)⟧
   ⟹ deadlock_free (□a∈A → P a ⟦S⟧⇩✓ □b∈B → Q b)›
  and deadlock_free_Mprefix_Sync⇩p⇩t⇩i⇩c⇩k_Mprefix_indep :
  ‹⟦A ∩ S = {}; B ∩ S = {}; A ≠ {} ∨ B ≠ {};
    ⋀a. a ∈ A - S ⟹ deadlock_free (P a ⟦S⟧⇩✓ □b∈B → Q b);
    ⋀b. b ∈ B - S ⟹ deadlock_free (□a∈A → P a ⟦S⟧⇩✓ Q b)⟧
   ⟹ deadlock_free (□a∈A → P a ⟦S⟧⇩✓ □b∈B → Q b)›
  and deadlock_free_Mprefix_Sync⇩p⇩t⇩i⇩c⇩k_Mprefix_right :
  ‹⟦A ⊆ S; B ∩ S = {}; B ≠ {};
    ⋀b. b ∈ B - S ⟹ deadlock_free (□a∈A → P a ⟦S⟧⇩✓ Q b)⟧
   ⟹ deadlock_free (□a∈A → P a ⟦S⟧⇩✓ □b∈B → Q b)›
  and deadlock_free_Mprefix_Sync⇩p⇩t⇩i⇩c⇩k_Mprefix_left :
  ‹⟦A ∩ S = {}; B ⊆ S; A ≠ {};
    ⋀a. a ∈ A - S ⟹ deadlock_free (P a ⟦S⟧⇩✓ □b∈B → Q b)⟧
   ⟹ deadlock_free (□a∈A → P a ⟦S⟧⇩✓ □b∈B → Q b)›
  by (auto intro!: deadlock_free_Mprefix_Sync⇩p⇩t⇩i⇩c⇩k_Mprefix)


end



section ‹Renaming and reference Processes›

― ‹Should have been declared simp earlier.›
lemma DF_empty        [simp] : ‹DF {} = STOP›
  and DF⇩S⇩K⇩I⇩P⇩S_empty    [simp] : ‹DF⇩S⇩K⇩I⇩P⇩S {} {} = STOP›
  and RUN_empty       [simp] : ‹RUN {} = STOP›
  and CHAOS_empty     [simp] : ‹CHAOS {} = STOP›
  and CHAOS⇩S⇩K⇩I⇩P⇩S_empty [simp] : ‹CHAOS⇩S⇩K⇩I⇩P⇩S {} {} = STOP›
  by (subst DF_unfold DF⇩S⇩K⇩I⇩P⇩S_unfold RUN_unfold CHAOS_unfold CHAOS⇩S⇩K⇩I⇩P⇩S_unfold, simp)+



subsection ‹Alternative Definitions with restriction fixed-point Operator›

text ‹
For now, we have lemmas such as @{thm DF_FD_Renaming_DF[no_vars]}, but the other refinement is
requiring \<^const>‹finitary› assumptions (@{thm Renaming_DF_FD_DF[no_vars]}).
›

lemma DF_restriction_fix_def : ‹DF A = (υ X. ⊓a ∈ A → X)›
  unfolding DF_def by (rule restriction_fix_is_fix[symmetric]) simp_all

lemma DF⇩S⇩K⇩I⇩P⇩S_restriction_fix_def : ‹DF⇩S⇩K⇩I⇩P⇩S A R = (υ X. (⊓a ∈ A → X) ⊓ SKIPS R)›
  unfolding DF⇩S⇩K⇩I⇩P⇩S_def by (rule restriction_fix_is_fix[symmetric]) simp_all

lemma RUN_restriction_fix_def : ‹RUN A = (υ X. □a ∈ A → X)›
  unfolding RUN_def by (rule restriction_fix_is_fix[symmetric]) simp_all

lemma CHAOS_restriction_fix_def : ‹CHAOS A = (υ X. STOP ⊓ (□a ∈ A → X))›
  unfolding CHAOS_def by (rule restriction_fix_is_fix[symmetric]) simp_all

lemma CHAOS⇩S⇩K⇩I⇩P⇩S_restriction_fix_def : ‹CHAOS⇩S⇩K⇩I⇩P⇩S A R = (υ X. SKIPS R ⊓ STOP ⊓ (□a ∈ A → X))›
  unfolding CHAOS⇩S⇩K⇩I⇩P⇩S_def by (rule restriction_fix_is_fix[symmetric]) simp_all



subsection ‹Stronger Results›

text ‹With \<^const>‹restriction_fix› induction, removing these assumptions is trivial.›

lemma Renaming_DF : ‹Renaming (DF A) f g = DF (f ` A)›
proof (unfold DF_restriction_fix_def, induct rule: parallel_restriction_fix_ind)
  show ‹Renaming STOP f g = STOP› by simp
qed (auto simp add: Renaming_Mndetprefix intro!: mono_Mndetprefix_eq)

lemma Renaming_DF⇩S⇩K⇩I⇩P⇩S : ‹Renaming (DF⇩S⇩K⇩I⇩P⇩S A R) f g = DF⇩S⇩K⇩I⇩P⇩S (f ` A) (g ` R)›
proof (unfold DF⇩S⇩K⇩I⇩P⇩S_restriction_fix_def, induct rule: parallel_restriction_fix_ind)
  show ‹Renaming STOP f g = STOP› by simp
qed (auto simp add: Renaming_Mndetprefix Renaming_Ndet
    intro!: mono_Mndetprefix_eq arg_cong2[where f = ‹(⊓)›])

lemma Renaming_RUN : ‹Renaming (RUN A) f g = RUN (f ` A)›
proof (unfold RUN_restriction_fix_def, induct rule: parallel_restriction_fix_ind)
  show ‹Renaming STOP f g = STOP› by simp
qed (auto simp add: Renaming_Mprefix intro!: mono_Mprefix_eq)

lemma Renaming_CHAOS : ‹Renaming (CHAOS A) f g = CHAOS (f ` A)›
proof (unfold CHAOS_restriction_fix_def, induct rule: parallel_restriction_fix_ind)
  show ‹Renaming STOP f g = STOP› by simp
qed (auto simp add: Renaming_Mprefix Renaming_Ndet
    intro!: mono_Mprefix_eq arg_cong2[where f = ‹(⊓)›])

lemma Renaming_CHAOS⇩S⇩K⇩I⇩P⇩S : ‹Renaming (CHAOS⇩S⇩K⇩I⇩P⇩S A R) f g = CHAOS⇩S⇩K⇩I⇩P⇩S (f ` A) (g ` R)›
proof (unfold CHAOS⇩S⇩K⇩I⇩P⇩S_restriction_fix_def, induct rule: parallel_restriction_fix_ind)
  show ‹Renaming STOP f g = STOP› by simp
qed (auto simp add: Renaming_Mprefix Renaming_Ndet
    intro!: mono_Mprefix_eq arg_cong2[where f = ‹(⊓)›])



section ‹Data Independence›

text (in Sync⇩p⇩t⇩i⇩c⇩k_locale) ‹
When working with the new interleaving \<^term>‹P |||⇩✓ Q›, we intuitively expect it to be
\<^const>‹deadlock_free› when both \<^term>‹P› and \<^term>‹Q› are.
The purpose of this section is to prove it.
›

subsection ‹An interesting equivalence›

lemma (in Sync⇩p⇩t⇩i⇩c⇩k_locale) deadlock_free_of_Sync⇩p⇩t⇩i⇩c⇩k_iff_DF_FD_DF_Sync⇩p⇩t⇩i⇩c⇩k_DF:
  ‹(∀P Q. deadlock_free P ⟶ deadlock_free Q ⟶ deadlock_free (P ⟦S⟧⇩✓ Q))
   ⟷ DF UNIV ⊑⇩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⇩p⇩t⇩i⇩c⇩k_FD)
qed



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

text ‹The two results below form a stronger (and generalized)
      version of @{thm DF_FD_DF_Sync_SKIP_iff[of r s A S]}.›

context Sync⇩p⇩t⇩i⇩c⇩k_locale begin

lemma (in Sync⇩p⇩t⇩i⇩c⇩k_locale) DF_FD_DF_Sync⇩p⇩t⇩i⇩c⇩k_SKIPS_imp_disjoint :
  ‹A ∩ S = {}› if ‹DF A ⊑⇩F⇩D DF A ⟦S⟧⇩✓ SKIPS R›
proof (rule ccontr)
  assume ‹A ∩ S ≠ {}›
  then obtain a where ‹a ∈ A› and ‹a ∈ S› by blast
  have ‹DF A ⟦S⟧⇩✓ SKIPS R ⊑⇩F⇩D DF {a} ⟦S⟧⇩✓ SKIPS R›
    by (intro mono_Sync⇩p⇩t⇩i⇩c⇩k_FD[OF _ idem_FD]) (simp add: DF_subset ‹a ∈ A›)
  also have ‹… = STOP›
    by (subst DF_unfold)
      (simp add: ‹a ∈ S› SKIPS_def Sync⇩p⇩t⇩i⇩c⇩k_distrib_GlobalNdet_left
        write0_Sync⇩p⇩t⇩i⇩c⇩k_STOP write0_Sync⇩p⇩t⇩i⇩c⇩k_SKIP)
  finally show False
    by (metis that ‹a ∈ A› DF_Univ_freeness empty_iff non_deadlock_free_STOP trans_FD)
qed


lemma disjoint_imp_DF_eq_DF_Sync⇩p⇩t⇩i⇩c⇩k_SKIPS :
  ‹DF A = DF A ⟦S⟧⇩✓ SKIPS R› if ‹A ∩ S = {}›
proof (subst DF_restriction_fix_def, induct rule: restriction_fix_ind)
  show ‹X = DF A ⟦S⟧⇩✓ SKIPS R ⟹ ⊓a∈A → X = DF A ⟦S⟧⇩✓ SKIPS R› for X
    by (subst DF_unfold)
      (auto simp add: SKIPS_def Sync⇩p⇩t⇩i⇩c⇩k_distrib_GlobalNdet_left
        Mndetprefix_Sync⇩p⇩t⇩i⇩c⇩k_SKIP Mndetprefix_Sync⇩p⇩t⇩i⇩c⇩k_STOP
        ‹A ∩ S = {}› Mndetprefix_distrib_GlobalNdet)
qed simp_all


corollary DF_FD_DF_Sync⇩p⇩t⇩i⇩c⇩k_STOP_imp_disjoint :
  ‹DF A ⊑⇩F⇩D DF A ⟦S⟧⇩✓ STOP ⟹ A ∩ S = {}›
  and DF_FD_DF_Sync⇩p⇩t⇩i⇩c⇩k_SKIP_imp_disjoint :
  ‹DF A ⊑⇩F⇩D DF A ⟦S⟧⇩✓ SKIP r ⟹ A ∩ S = {}›
  and disjoint_imp_DF_eq_DF_Sync⇩p⇩t⇩i⇩c⇩k_STOP :
  ‹A ∩ S = {} ⟹ DF A = DF A ⟦S⟧⇩✓ STOP›
  and disjoint_imp_DF_eq_DF_Sync⇩p⇩t⇩i⇩c⇩k_SKIP :
  ‹A ∩ S = {} ⟹ DF A = DF A ⟦S⟧⇩✓ SKIP r›
  by (fact DF_FD_DF_Sync⇩p⇩t⇩i⇩c⇩k_SKIPS_imp_disjoint[where R = ‹{}›, simplified]
      DF_FD_DF_Sync⇩p⇩t⇩i⇩c⇩k_SKIPS_imp_disjoint[where R = ‹{r}›, simplified]
      disjoint_imp_DF_eq_DF_Sync⇩p⇩t⇩i⇩c⇩k_SKIPS[where R = ‹{}›, simplified]
      disjoint_imp_DF_eq_DF_Sync⇩p⇩t⇩i⇩c⇩k_SKIPS[where R = ‹{r}›, simplified])+


end

corollary (in Sync⇩p⇩t⇩i⇩c⇩k_locale) DF_FD_SKIPS_Sync⇩p⇩t⇩i⇩c⇩k_DF_imp_disjoint :
  ‹DF A ⊑⇩F⇩D SKIPS R ⟦S⟧⇩✓ DF A ⟹ A ∩ S = {}›
  by (metis Sync⇩p⇩t⇩i⇩c⇩k_locale_sym.DF_FD_DF_Sync⇩p⇩t⇩i⇩c⇩k_SKIPS_imp_disjoint Sync⇩p⇩t⇩i⇩c⇩k_sym)


lemma (in Sync⇩p⇩t⇩i⇩c⇩k_locale) disjoint_imp_DF_eq_SKIPS_Sync⇩p⇩t⇩i⇩c⇩k_DF :
  ‹A ∩ S = {} ⟹ DF A = SKIPS R ⟦S⟧⇩✓ DF A›
  by (metis Sync⇩p⇩t⇩i⇩c⇩k_locale_sym.disjoint_imp_DF_eq_DF_Sync⇩p⇩t⇩i⇩c⇩k_SKIPS Sync⇩p⇩t⇩i⇩c⇩k_sym)


corollary (in Sync⇩p⇩t⇩i⇩c⇩k_locale) DF_FD_STOP_Sync⇩p⇩t⇩i⇩c⇩k_DF_imp_disjoint :
  ‹DF A ⊑⇩F⇩D STOP ⟦S⟧⇩✓ DF A ⟹ A ∩ S = {}›
  and DF_FD_SKIP_Sync⇩p⇩t⇩i⇩c⇩k_DF_imp_disjoint :
  ‹DF A ⊑⇩F⇩D SKIP r ⟦S⟧⇩✓ DF A ⟹ A ∩ S = {}›
  and disjoint_imp_DF_eq_STOP_Sync⇩p⇩t⇩i⇩c⇩k_DF :
  ‹A ∩ S = {} ⟹ DF A = STOP ⟦S⟧⇩✓ DF A›
  and disjoint_imp_DF_eq_SKIP_Sync⇩p⇩t⇩i⇩c⇩k_DF :
  ‹A ∩ S = {} ⟹ DF A = SKIP r ⟦S⟧⇩✓ DF A›
  by (fact DF_FD_SKIPS_Sync⇩p⇩t⇩i⇩c⇩k_DF_imp_disjoint[where R = ‹{}›, simplified]
      DF_FD_SKIPS_Sync⇩p⇩t⇩i⇩c⇩k_DF_imp_disjoint[where R = ‹{r}›, simplified]
      disjoint_imp_DF_eq_SKIPS_Sync⇩p⇩t⇩i⇩c⇩k_DF[where R = ‹{}›, simplified]
      disjoint_imp_DF_eq_SKIPS_Sync⇩p⇩t⇩i⇩c⇩k_DF[where R = ‹{r}›, simplified])+




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

theorem (in Sync⇩p⇩t⇩i⇩c⇩k_locale) DF_F_DF_Sync⇩p⇩t⇩i⇩c⇩k_DF_weak : ‹DF (A ∪ B) ⊑⇩F DF A ⟦S⟧⇩✓ DF B›
  if nonempty: ‹A ≠ {}› ‹B ≠ {}›
    and intersect_hyp: ‹B ∩ S = {} ∨ (∃y. B ∩ S = {y} ∧ A ∩ S ⊆ {y})›
proof -
  have ‹⟦(u, X) ∈ ℱ (DF A); (v, Y) ∈ ℱ (DF B); t setinterleaves⇩✓⇘(⊗✓)⇙ ((u, v), S)⟧
        ⟹ (t, super_ref_Sync⇩p⇩t⇩i⇩c⇩k (⊗✓) X S Y) ∈ ℱ (DF (A ∪ B))› for v t u X Y
  proof (induct t arbitrary: u v)
    case Nil
    from Nil.prems(3) have ‹u = []› ‹v = []› by (simp_all add: Nil_setinterleaves⇩p⇩t⇩i⇩c⇩k)
    from Nil.prems(1) obtain a where ‹a ∈ A› ‹ev a ∉ X›
      by (subst (asm) F_DF) (auto simp add: nonempty ‹u = []›)
    moreover from Nil.prems(2) obtain b where ‹b ∈ B› ‹ev b ∉ Y›
      by (subst (asm) F_DF) (auto simp add: nonempty ‹v = []›)
    ultimately show ?case
      using intersect_hyp
      by (subst F_DF, simp add: nonempty super_ref_Sync⇩p⇩t⇩i⇩c⇩k_def subset_iff)
        (metis Int_iff empty_iff insert_iff)
  next
    case (Cons e t)
    from Cons.prems(3) consider (mv_left) a u' where ‹a ∉ S› ‹e = ev a› ‹u = ev a # u'›
      ‹t setinterleaves⇩✓⇘(⊗✓)⇙ ((u', v), S)›
    | (mv_right) b v' where ‹b ∉ S› ‹e = ev b› ‹v = ev b # v'›
      ‹t setinterleaves⇩✓⇘(⊗✓)⇙ ((u, v'), S)›
    | (mv_both_ev) a u' v' where ‹a ∈ S› ‹e = ev a› ‹u = ev a # u'› ‹v = ev a # v'›
      ‹t setinterleaves⇩✓⇘(⊗✓)⇙ ((u', v'), S)›
    | (mv_both_tick) r s r_s u' v' where ‹r ⊗✓ s = Some r_s› ‹e = ✓(r_s)›
      ‹u = ✓(r) # u'› ‹v = ✓(s) # v'› ‹t setinterleaves⇩✓⇘(⊗✓)⇙ ((u', v'), S)›
      by (cases e) (auto elim: Cons_ev_setinterleaves⇩p⇩t⇩i⇩c⇩kE Cons_tick_setinterleaves⇩p⇩t⇩i⇩c⇩kE)
    thus ?case
    proof cases
      case mv_left
      from Cons.prems(1) have ‹a ∈ A›
        by (subst (asm) F_DF) (simp add: mv_left(3) split: if_split_asm)
      from Cons.prems(1)[unfolded mv_left(3), THEN Cons_F_DF] have ‹(u', X) ∈ ℱ (DF A)› .
      from Cons.hyps[OF this Cons.prems(2) mv_left(4)] show ?thesis
        by (subst F_DF) (simp add: nonempty ‹e = ev a› ‹a ∈ A›)
    next
      case mv_right
      from Cons.prems(2) have ‹b ∈ B›
        by (subst (asm) F_DF) (simp add: mv_right(3) split: if_split_asm)
      from Cons.prems(2)[unfolded mv_right(3), THEN Cons_F_DF] have ‹(v', Y) ∈ ℱ (DF B)› .
      from Cons.hyps[OF Cons.prems(1) this mv_right(4)] show ?thesis
        by (subst F_DF) (simp add: nonempty ‹e = ev b› ‹b ∈ B›)
    next
      case mv_both_ev
      from Cons.prems(1) have ‹a ∈ A›
        by (subst (asm) F_DF) (simp add: mv_both_ev(3) split: if_split_asm)
      from Cons.prems(1)[unfolded mv_both_ev(3), THEN Cons_F_DF]
        Cons.prems(2)[unfolded mv_both_ev(4), THEN Cons_F_DF]
      have ‹(u', X) ∈ ℱ (DF A)› ‹(v', Y) ∈ ℱ (DF B)› .
      from Cons.hyps[OF this mv_both_ev(5)] show ?thesis
        by (subst F_DF) (simp add: nonempty ‹e = ev a› ‹a ∈ A›)
    next
      case mv_both_tick
      from Cons.prems(1) have False
        by (subst (asm) F_DF) (simp add: mv_both_tick(3) split: if_split_asm)
      thus ?thesis ..
    qed
  qed
  thus ‹DF (A ∪ B) ⊑⇩F DF A ⟦S⟧⇩✓ DF B›
    by (simp add: failure_refine_def F_Sync⇩p⇩t⇩i⇩c⇩k div_free_DF)
      (use is_processT4 in blast)
qed


theorem (in Sync⇩p⇩t⇩i⇩c⇩k_locale) DF_F_DF_Sync⇩p⇩t⇩i⇩c⇩k_DF :
  ‹DF (A ∪ B) ⊑⇩F DF A ⟦S⟧⇩✓ DF B› if ‹A ≠ {}› ‹B ≠ {}›
  and ‹A ∩ S = {} ∨ (∃a. A ∩ S = {a} ∧ B ∩ S ⊆ {a}) ∨
       B ∩ S = {} ∨ (∃b. B ∩ S = {b} ∧ A ∩ S ⊆ {b})›
proof -
  from that(3) consider ‹A ∩ S = {} ∨ (∃a. A ∩ S = {a} ∧ B ∩ S ⊆ {a})›
    | ‹B ∩ S = {} ∨ (∃b. B ∩ S = {b} ∧ A ∩ S ⊆ {b})› by metis
  thus ‹DF (A ∪ B) ⊑⇩F DF A ⟦S⟧⇩✓ DF B›
  proof cases
    from that(1, 2) show ‹B ∩ S = {} ∨ (∃b. B ∩ S = {b} ∧ A ∩ S ⊆ {b}) ⟹
                          DF (A ∪ B) ⊑⇩F DF A ⟦S⟧⇩✓ DF B›
      by (rule DF_F_DF_Sync⇩p⇩t⇩i⇩c⇩k_DF_weak)
  next
    from that(1, 2) show ‹A ∩ S = {} ∨ (∃a. A ∩ S = {a} ∧ B ∩ S ⊆ {a}) ⟹
                          DF (A ∪ B) ⊑⇩F DF A ⟦S⟧⇩✓ DF B›
      by (fold Sync⇩p⇩t⇩i⇩c⇩k_sym, subst Un_commute)
        (simp add: Sync⇩p⇩t⇩i⇩c⇩k_locale_sym.DF_F_DF_Sync⇩p⇩t⇩i⇩c⇩k_DF_weak)
  qed
qed


lemma (in Sync⇩p⇩t⇩i⇩c⇩k_locale) DF_FD_DF_Sync⇩p⇩t⇩i⇩c⇩k_DF :
  ‹DF (A ∪ B) ⊑⇩F⇩D DF A ⟦S⟧⇩✓ DF B› if ‹A ≠ {}› ‹B ≠ {}›
  and ‹A ∩ S = {} ∨ (∃a. A ∩ S = {a} ∧ B ∩ S ⊆ {a}) ∨
       B ∩ S = {} ∨ (∃b. B ∩ S = {b} ∧ A ∩ S ⊆ {b})›
  using DF_F_DF_Sync⇩p⇩t⇩i⇩c⇩k_DF[OF that]
  by (simp add: refine_defs div_free_DF D_Sync⇩p⇩t⇩i⇩c⇩k)


theorem (in Sync⇩p⇩t⇩i⇩c⇩k_locale) DF_FD_DF_Sync⇩p⇩t⇩i⇩c⇩k_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⇩p⇩t⇩i⇩c⇩k_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⇩p⇩t⇩i⇩c⇩k_write0_subset)
    finally have False
      by (metis DF_Univ_freeness Un_empty ‹A ≠ {}›
          trans_FD[OF ‹?FD_ref›] non_deadlock_free_STOP)
  } note * = this
  show ?thesis
  proof (cases ‹A = {}›; cases ‹B = {}›)
    show ‹A = {} ⟹ B = {} ⟹ ?thesis› by simp
  next
    show ‹A = {} ⟹ B ≠ {} ⟹ ?thesis›
      by simp (metis DF_FD_STOP_Sync⇩p⇩t⇩i⇩c⇩k_DF_imp_disjoint
          disjoint_imp_DF_eq_STOP_Sync⇩p⇩t⇩i⇩c⇩k_DF order_refl)
  next
    show ‹A ≠ {} ⟹ B = {} ⟹ ?thesis›
      by simp (metis DF_FD_DF_Sync⇩p⇩t⇩i⇩c⇩k_STOP_imp_disjoint
          disjoint_imp_DF_eq_DF_Sync⇩p⇩t⇩i⇩c⇩k_STOP order_refl)
  next
    show ‹A ≠ {} ⟹ B ≠ {} ⟹ ?thesis›
      by simp (metis "*" DF_FD_DF_Sync⇩p⇩t⇩i⇩c⇩k_DF)
  qed
qed



lemma DF_FD_DF_MultiSync⇩p⇩t⇩i⇩c⇩k_DF :
  ‹⟦⋀l. l ∈ set L ⟹ X l ≠ {}; ∃s. (⋃ l ∈ set L. X l) ∩ S ⊆ {s}⟧
   ⟹ DF (⋃ l ∈ set L. X l) ⊑⇩F⇩D ❙⟦S❙⟧⇩✓ l ∈@ L. (DF (X l) :: ('a, 'r) process⇩p⇩t⇩i⇩c⇩k)›
proof (induct L rule: induct_list012)
  case 1 show ?case by simp
next
  case (2 l0) show ?case by (simp add: Renaming_DF)
next
  case (3 l0 l1 L)
  have ‹(DF (⋃ l ∈ set (l0 # l1 # L). X l) :: ('a, 'r list) process⇩p⇩t⇩i⇩c⇩k) =
        DF (X l0 ∪ (⋃ l ∈ set (l1 # L). X l))› by simp
  also have ‹… ⊑⇩F⇩D DF (X l0) ⟦S⟧⇩✓⇩R⇩l⇩i⇩s⇩t DF (⋃ l ∈ set (l1 # L). X l)›
    by (rule Sync⇩R⇩l⇩i⇩s⇩t.DF_FD_DF_Sync⇩p⇩t⇩i⇩c⇩k_DF_iff[THEN iffD2])
      (use "3.prems"(2) in ‹simp add: "3.prems"(1) subset_singleton_iff
                                      Int_Un_distrib2 Un_singleton_iff, safe, simp_all›)
  also have ‹… ⊑⇩F⇩D DF (X l0) ⟦S⟧⇩✓⇩R⇩l⇩i⇩s⇩t ❙⟦S❙⟧⇩✓ l∈@(l1 # L). (DF (X l))›
    by (intro Sync⇩R⇩l⇩i⇩s⇩t.mono_Sync⇩p⇩t⇩i⇩c⇩k_FD[OF idem_FD] "3.hyps"(2))
      (use "3.prems" in auto)
  also have ‹… = ❙⟦S❙⟧⇩✓ l∈@(l0 # l1 # L). DF (X l)› by simp
  finally show ?case .
qed





lemma (in Sync⇩p⇩t⇩i⇩c⇩k_locale) ‹DF {a} = DF {a} ⟦S⟧⇩✓ STOP ⟷ a ∉ S›
  by (metis DF_FD_DF_Sync⇩p⇩t⇩i⇩c⇩k_STOP_imp_disjoint boolean_algebra.conj_zero_left
      disjoint_imp_DF_eq_DF_Sync⇩p⇩t⇩i⇩c⇩k_STOP insert_disjoint(1) order_refl)

lemma (in Sync⇩p⇩t⇩i⇩c⇩k_locale) ‹DF {a} ⟦S⟧⇩✓ STOP = STOP ⟷ a ∈ S›
  by (metis DF_unfold Diff_eq_empty_iff Diff_triv Int_empty_left Int_insert_left
      Mndetprefix_Sync⇩p⇩t⇩i⇩c⇩k_Mprefix_right Mndetprefix_Sync⇩p⇩t⇩i⇩c⇩k_STOP
      Mndetprefix_is_STOP_iff Mprefix_empty empty_not_insert insert_Diff1)


corollary (in Sync⇩p⇩t⇩i⇩c⇩k_locale) DF_FD_DF_Inter⇩p⇩t⇩i⇩c⇩k_DF : ‹DF A ⊑⇩F⇩D DF A |||⇩✓ DF A›
  by (metis DF_FD_DF_Sync⇩p⇩t⇩i⇩c⇩k_DF_iff inf_bot_right sup.idem)

corollary (in Sync⇩p⇩t⇩i⇩c⇩k_locale) DF_UNIV_FD_DF_UNIV_Inter⇩p⇩t⇩i⇩c⇩k_DF_UNIV:
  ‹DF UNIV ⊑⇩F⇩D DF UNIV |||⇩✓ DF UNIV›
  by (fact DF_FD_DF_Inter⇩p⇩t⇩i⇩c⇩k_DF)

corollary (in Sync⇩p⇩t⇩i⇩c⇩k_locale) Inter⇩p⇩t⇩i⇩c⇩k_deadlock_free :
  ‹deadlock_free P ⟹ deadlock_free Q ⟹ deadlock_free (P |||⇩✓ Q)›
  using DF_FD_DF_Inter⇩p⇩t⇩i⇩c⇩k_DF deadlock_free_of_Sync⇩p⇩t⇩i⇩c⇩k_iff_DF_FD_DF_Sync⇩p⇩t⇩i⇩c⇩k_DF by blast


theorem MultiInter⇩p⇩t⇩i⇩c⇩k_deadlock_free :
  ‹⟦L ≠ []; ⋀l. l ∈ set L ⟹ deadlock_free (P l)⟧ ⟹
   deadlock_free (❙|❙|❙|⇩✓ l ∈@ L. P l)›
proof (induct L rule: induct_list012)
  case 1
  from "1.prems"(1) have False by simp
  thus ?case ..
next
  case (2 l0)
  from "2.prems"(2) show ?case
    by (simp add: deadlock_free_imp_deadlock_free_Renaming)
next
  case (3 l0 l1 L)
  have ‹❙|❙|❙|⇩✓ l ∈@ (l0 # l1 # L). P l = P l0 |||⇩✓⇩R⇩l⇩i⇩s⇩t ❙|❙|❙|⇩✓ l ∈@ (l1 # L). P l› by simp
  moreover have ‹deadlock_free (P l0)› by (simp add: "3.prems"(2))
  moreover have ‹deadlock_free (❙|❙|❙|⇩✓ l ∈@ (l1 # L). P l)›
    by (rule "3.hyps"(2)) (simp_all add: "3.prems"(2))
  ultimately show ?case
    by (simp add: Sync⇩R⇩l⇩i⇩s⇩t.Inter⇩p⇩t⇩i⇩c⇩k_deadlock_free)
qed



(*<*)
end
  (*>*)