Theory CSP_Assertions

(*<*)
―‹ ********************************************************************
 * Project         : HOL-CSP - A Shallow Embedding of CSP in Isabelle/HOL
 * Version         : 2.0
 *
 * Author          : Benoît Ballenghien, Safouan Taha, Burkhart Wolff, Lina Ye.
 *                   (Based on HOL-CSP 1.0 by Haykal Tej and Burkhart Wolff)
 *
 * This file       : Reference processes and properties
 *
 * Copyright (c) 2009 Université Paris-Sud, France
 * 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‹CSP Assertions›

(*<*)
theory CSP_Assertions
  imports Basic_CSP_Laws CSP_Monotonies Events_Ticks_CSP_Laws
begin
  (*>*)


section ‹Reference Processes›

definition DF :: ‹'a set ⇒ ('a, 'r) process⇩p⇩t⇩i⇩c⇩k›
  where   ‹DF A ≡ μ X. ⊓a∈A → X›

lemma DF_unfold : ‹DF A = ⊓a∈A → DF A›
  by (simp add: DF_def, rule trans, rule fix_eq, simp)


definition DF⇩S⇩K⇩I⇩P⇩S :: ‹'a set ⇒ 'r set ⇒ ('a,'r) process⇩p⇩t⇩i⇩c⇩k›
  where ‹DF⇩S⇩K⇩I⇩P⇩S A R ≡ μ X. (⊓a ∈ A → X) ⊓ SKIPS R›

lemma DF⇩S⇩K⇩I⇩P⇩S_unfold : ‹DF⇩S⇩K⇩I⇩P⇩S A R = (⊓a ∈ A → DF⇩S⇩K⇩I⇩P⇩S A R) ⊓ SKIPS R›
  by (simp add: DF⇩S⇩K⇩I⇩P⇩S_def, rule trans, rule fix_eq, simp)


definition RUN :: ‹'a set ⇒ ('a,'r) process⇩p⇩t⇩i⇩c⇩k›
  where ‹RUN A ≡ μ X. □x∈A → X›

lemma RUN_unfold : ‹RUN A = □a∈A → RUN A›
  by (simp add: RUN_def, rule trans, rule fix_eq, simp)


definition CHAOS :: ‹'a set ⇒ ('a,'r) process⇩p⇩t⇩i⇩c⇩k› 
  where ‹CHAOS A ≡ μ X. STOP ⊓ (□a ∈ A → X)›

lemma CHAOS_unfold : ‹CHAOS A = STOP ⊓ (□a∈A → CHAOS A)›
  by (simp add: CHAOS_def, rule trans, rule fix_eq, simp)


definition CHAOS⇩S⇩K⇩I⇩P⇩S :: ‹'a set ⇒ 'r set ⇒ ('a,'r) process⇩p⇩t⇩i⇩c⇩k›
  where ‹CHAOS⇩S⇩K⇩I⇩P⇩S A R ≡ μ X. SKIPS R ⊓ STOP ⊓ (□a∈A → X)›

lemma CHAOS⇩S⇩K⇩I⇩P⇩S_unfold: ‹CHAOS⇩S⇩K⇩I⇩P⇩S A R = SKIPS R ⊓ STOP ⊓ (□a ∈ A → CHAOS⇩S⇩K⇩I⇩P⇩S A R)›
  by (simp add: CHAOS⇩S⇩K⇩I⇩P⇩S_def, rule trans, rule fix_eq, simp)



section ‹Assertions›

definition deadlock_free :: ‹('a,'r) process⇩p⇩t⇩i⇩c⇩k ⇒ bool›
  where ‹deadlock_free P ≡ DF UNIV ⊑⇩F⇩D P›


definition deadlock_free⇩S⇩K⇩I⇩P⇩S :: ‹('a, 'r) process⇩p⇩t⇩i⇩c⇩k ⇒ bool›
  where ‹deadlock_free⇩S⇩K⇩I⇩P⇩S P ≡ DF⇩S⇩K⇩I⇩P⇩S UNIV UNIV ⊑⇩F P›


definition lifelock_free :: ‹('a,'r) process⇩p⇩t⇩i⇩c⇩k ⇒ bool›
  where ‹lifelock_free P ≡ CHAOS UNIV ⊑⇩F⇩D P›


definition lifelock_free⇩S⇩K⇩I⇩P⇩S :: ‹('a,'r) process⇩p⇩t⇩i⇩c⇩k ⇒ bool›
  where ‹lifelock_free⇩S⇩K⇩I⇩P⇩S P ≡ CHAOS⇩S⇩K⇩I⇩P⇩S UNIV UNIV ⊑⇩F⇩D P›


definition non_terminating :: ‹('a,'r) process⇩p⇩t⇩i⇩c⇩k ⇒ bool›
  where ‹non_terminating P ≡ RUN UNIV ⊑⇩T P›



section ‹Properties›

lemma DF⇩S⇩K⇩I⇩P⇩S_FD_DF : ‹DF⇩S⇩K⇩I⇩P⇩S A R ⊑⇩F⇩D DF A›
proof (subst DF⇩S⇩K⇩I⇩P⇩S_def, induct rule: fix_ind)
  show ‹adm (λa. a ⊑⇩F⇩D DF A)› by simp
next
  show ‹⊥ ⊑⇩F⇩D DF A› by simp
next
  show ‹X ⊑⇩F⇩D DF A ⟹ (Λ X. (⊓a∈A → X) ⊓ SKIPS R)⋅X ⊑⇩F⇩D DF A› for X
    by (subst DF_unfold, simp)
      (meson Ndet_FD_self_left mono_Mndetprefix_FD trans_FD)
qed



lemma SKIPS_FD_SKIPS_iff :
  ‹SKIPS S ⊑⇩F⇩D SKIPS R ⟷ (if R = {} then S = {} else R ⊆ S)›
  by (auto simp add: failure_divergence_refine_def failure_refine_def
      divergence_refine_def F_SKIPS D_SKIPS)

lemma SKIPS_F_SKIPS_iff :
  ‹SKIPS S ⊑⇩F SKIPS R ⟷ (if R = {} then S = {} else R ⊆ S)›
  by (auto simp add: failure_refine_def F_SKIPS)

lemma SKIPS_T_SKIPS_iff : ‹SKIPS S ⊑⇩T SKIPS R ⟷ (R ⊆ S)›
  by (auto simp add: trace_refine_def T_SKIPS subset_iff)



lemma DF_subset : ‹DF B ⊑⇩F⇩D DF A› if ‹A ≠ {}› ‹A ⊆ B› for A B :: ‹'a set›
proof (subst DF_def, induct rule: fix_ind)
  show ‹adm (λa. a ⊑⇩F⇩D DF A)› by simp
next
  show ‹⊥ ⊑⇩F⇩D DF A› by simp
next
  show ‹X ⊑⇩F⇩D DF A ⟹ (Λ X. ⊓b∈B → X)⋅X ⊑⇩F⇩D DF A› for X :: ‹('a, 'r) process⇩p⇩t⇩i⇩c⇩k›
    by (subst DF_unfold, simp)
      (meson ‹A ≠ {}› ‹A ⊆ B›  Mndetprefix_FD_subset mono_Mndetprefix_FD trans_FD)
qed

lemma DF_Univ_freeness : ‹A ≠ {} ⟹ DF A ⊑⇩F⇩D P ⟹ deadlock_free P›
  by (meson DF_subset deadlock_free_def subset_UNIV trans_FD)

lemma deadlock_free_Ndet_iff :
  ‹deadlock_free (P ⊓ Q) ⟷ deadlock_free P ∧ deadlock_free Q›
  by (auto simp add: F_Ndet D_Ndet deadlock_free_def refine_defs)


lemma DF⇩S⇩K⇩I⇩P⇩S_subset : ‹DF⇩S⇩K⇩I⇩P⇩S B S ⊑⇩F⇩D DF⇩S⇩K⇩I⇩P⇩S A R›
  if ‹A ≠ {}› ‹A ⊆ B› ‹R ≠ {}› ‹R ⊆ S›
proof (subst DF⇩S⇩K⇩I⇩P⇩S_def, induct rule: fix_ind)
  show ‹adm (λa. a ⊑⇩F⇩D DF⇩S⇩K⇩I⇩P⇩S A R)› by simp
next
  show ‹⊥ ⊑⇩F⇩D DF⇩S⇩K⇩I⇩P⇩S A R› by simp
next
  show ‹(Λ X. (⊓b∈B → X) ⊓ SKIPS S)⋅X ⊑⇩F⇩D DF⇩S⇩K⇩I⇩P⇩S A R› if ‹X ⊑⇩F⇩D DF⇩S⇩K⇩I⇩P⇩S A R› for X
  proof (subst DF⇩S⇩K⇩I⇩P⇩S_unfold, subst beta_cfun)
    show ‹cont (λX. (⊓b∈B →  X) ⊓ SKIPS S)› by simp
  next
    show ‹(⊓b∈B →  X) ⊓ SKIPS S ⊑⇩F⇩D (⊓a∈A →  DF⇩S⇩K⇩I⇩P⇩S A R) ⊓ SKIPS R›
    proof (rule mono_Ndet_FD)
      show ‹⊓b∈B →  X ⊑⇩F⇩D ⊓a∈A →  DF⇩S⇩K⇩I⇩P⇩S A R›
        by (meson Mndetprefix_FD_subset ‹A ≠ {}› ‹A ⊆ B›
            mono_Mndetprefix_FD ‹X ⊑⇩F⇩D DF⇩S⇩K⇩I⇩P⇩S A R› trans_FD)
    next
      show ‹SKIPS S ⊑⇩F⇩D SKIPS R›
        by (simp add: SKIPS_FD_SKIPS_iff ‹R ≠ {}› ‹R ⊆ S›)
    qed
  qed
qed


lemma DF⇩S⇩K⇩I⇩P⇩S_Univ_freeness : ‹⟦A ≠ {}; R ≠ {}; DF⇩S⇩K⇩I⇩P⇩S A R ⊑⇩F⇩D P⟧ ⟹ deadlock_free⇩S⇩K⇩I⇩P⇩S P›
  by (meson DF⇩S⇩K⇩I⇩P⇩S_subset deadlock_free⇩S⇩K⇩I⇩P⇩S_def leFD_imp_leF subset_UNIV trans_F)

lemma 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›
  by (simp add: F_Ndet deadlock_free⇩S⇩K⇩I⇩P⇩S_def failure_refine_def)


lemma div_free_DF⇩S⇩K⇩I⇩P⇩S: ‹𝒟 (DF⇩S⇩K⇩I⇩P⇩S A R) = {}›
proof (rule equals0I)
  show ‹s ∈ 𝒟 (DF⇩S⇩K⇩I⇩P⇩S A R) ⟹ False› for s
    by (induct s; subst (asm) DF⇩S⇩K⇩I⇩P⇩S_unfold)
      (auto simp add: D_Ndet D_SKIPS D_Mndetprefix write0_def D_Mprefix split: if_split_asm)
qed


lemma div_free_DF: ‹𝒟 (DF A) = {}›
  by (metis DF⇩S⇩K⇩I⇩P⇩S_FD_DF div_free_DF⇩S⇩K⇩I⇩P⇩S empty_subsetI subset_antisym le_ref1)


lemma deadlock_free_implies_div_free: ‹deadlock_free P ⟹ 𝒟 P = {}›
  by (simp add: deadlock_free_def div_free_DF refine_defs)



section ‹Events and Ticks of Reference Processes›

lemma events_of_SKIPS : ‹α(SKIPS R) = {}›
  and  ticks_of_SKIPS : ‹✓s(SKIPS R) = R›
  by (auto simp add: events_of_def ticks_of_def T_SKIPS)


lemma no_ticks_imp_tickFree_T : ‹✓s(P) = {} ⟹ s ∈ 𝒯 P ⟹ tF s›
  by (simp add: ticks_of_def tickFree_def disjoint_iff image_iff)
    (metis T_nonTickFree_imp_decomp event⇩p⇩t⇩i⇩c⇩k.disc(2) split_list tickFree_Cons_iff tickFree_append_iff)


lemma events_of_DF : ‹α(DF A) = A›
proof (intro subset_antisym subsetI)
  fix a assume ‹a ∈ A›
  hence ‹[ev a] ∈ 𝒯 (DF A)›
    by (subst DF_unfold) (auto simp add: T_Mndetprefix write0_def T_Mprefix)
  thus ‹a ∈ α(DF A)› by (force simp add: events_of_def)
next
  fix a assume ‹a ∈ α((DF A) :: ('a, 'r) process⇩p⇩t⇩i⇩c⇩k)›
  then obtain t :: ‹('a, 'r) trace⇩p⇩t⇩i⇩c⇩k› where ‹ev a ∈ set t› ‹t ∈ 𝒯 (DF A)›
    by (auto simp add: events_of_def)
  thus ‹a ∈ A›
    by (induct t, simp, subst (asm) DF_unfold)
      (auto simp add: T_Mndetprefix write0_def T_Mprefix split: if_split_asm)
qed

lemma ticks_DF : ‹✓s(DF A) = {}›
proof (rule equals0I)
  fix r :: 'r assume ‹r ∈ ✓s(DF A)›
  then obtain s where ‹s @ [✓(r)] ∈ 𝒯 (DF A)› unfolding ticks_of_def by blast
  thus False
    by (induct s; subst (asm) DF_unfold)
      (simp_all add: T_Mndetprefix write0_def T_Mprefix split: if_split_asm)
qed


lemma events_of_DF⇩S⇩K⇩I⇩P⇩S : ‹α(DF⇩S⇩K⇩I⇩P⇩S A R) = A›
proof (intro subset_antisym subsetI)
  fix a assume ‹a ∈ A›
  hence ‹[ev a] ∈ 𝒯 (DF⇩S⇩K⇩I⇩P⇩S A R)›
    by (subst DF⇩S⇩K⇩I⇩P⇩S_unfold) (auto simp add: T_Ndet T_Mndetprefix write0_def T_Mprefix)
  thus ‹a ∈ α(DF⇩S⇩K⇩I⇩P⇩S A R)› by (force simp add: events_of_def)
next
  fix a assume ‹a ∈ α(DF⇩S⇩K⇩I⇩P⇩S A R)›
  then obtain t where ‹ev a ∈ set t› ‹t ∈ 𝒯 (DF⇩S⇩K⇩I⇩P⇩S A R)›
    by (auto simp add: events_of_def)
  thus ‹a ∈ A›
    by (induct t, simp, subst (asm) DF⇩S⇩K⇩I⇩P⇩S_unfold)
      (auto simp add: T_Ndet T_SKIPS T_Mndetprefix write0_def T_Mprefix split: if_split_asm)
qed

lemma ticks_DF⇩S⇩K⇩I⇩P⇩S : ‹✓s(DF⇩S⇩K⇩I⇩P⇩S A R) = R›
proof (intro subset_antisym subsetI)
  fix r assume ‹r ∈ R›
  hence ‹[✓(r)] ∈ 𝒯 (DF⇩S⇩K⇩I⇩P⇩S A R)› by (subst DF⇩S⇩K⇩I⇩P⇩S_unfold) (simp add: T_Ndet T_SKIPS)
  thus ‹r ∈ ✓s(DF⇩S⇩K⇩I⇩P⇩S A R)›
    unfolding ticks_of_def by (metis (no_types, lifting) CollectI append_self_conv2)
next
  fix r assume ‹r ∈ ✓s(DF⇩S⇩K⇩I⇩P⇩S A R)›
  then obtain s where ‹s @ [✓(r)] ∈ 𝒯 (DF⇩S⇩K⇩I⇩P⇩S A R)› unfolding ticks_of_def by blast
  thus ‹r ∈ R›
    by (induct s; subst (asm) DF⇩S⇩K⇩I⇩P⇩S_unfold)
      (simp_all add: T_Ndet T_SKIPS T_Mndetprefix write0_def T_Mprefix split: if_split_asm)
qed



lemma events_of_RUN : ‹α(RUN A) = A›
proof (intro subset_antisym subsetI)
  fix a assume ‹a ∈ A›
  hence ‹[ev a] ∈ 𝒯 (RUN A)›
    by (subst RUN_unfold) (auto simp add: T_Mprefix)
  thus ‹a ∈ α(RUN A)› by (force simp add: events_of_def)
next
  fix a assume ‹a ∈ α((RUN A) :: ('a, 'r) process⇩p⇩t⇩i⇩c⇩k)›
  then obtain t :: ‹('a, 'r) trace⇩p⇩t⇩i⇩c⇩k› where ‹ev a ∈ set t› ‹t ∈ 𝒯 (RUN A)›
    by (auto simp add: events_of_def)
  thus ‹a ∈ A›
    by (induct t, simp, subst (asm) RUN_unfold) (auto simp add: T_Mprefix)
qed

lemma ticks_RUN : ‹✓s(RUN A) = {}›
proof (rule equals0I)
  fix r :: 'r assume ‹r ∈ ✓s(RUN A)›
  then obtain s where ‹s @ [✓(r)] ∈ 𝒯 (RUN A)› unfolding ticks_of_def by blast
  thus False
    by (induct s; subst (asm) RUN_unfold)
      (auto simp add: T_Mprefix split: if_split_asm)
qed




lemma events_of_CHAOS : ‹α(CHAOS A) = A›
proof (intro subset_antisym subsetI)
  fix a assume ‹a ∈ A›
  hence ‹[ev a] ∈ 𝒯 (CHAOS A)›
    by (subst CHAOS_unfold) (auto simp add: T_Ndet T_Mprefix)
  thus ‹a ∈ α(CHAOS A)› by (force simp add: events_of_def)
next
  fix a assume ‹a ∈ α((CHAOS A) :: ('a, 'r) process⇩p⇩t⇩i⇩c⇩k)›
  then obtain t :: ‹('a, 'r) trace⇩p⇩t⇩i⇩c⇩k› where ‹ev a ∈ set t› ‹t ∈ 𝒯 (CHAOS A)›
    by (auto simp add: events_of_def)
  thus ‹a ∈ A›
    by (induct t, simp, subst (asm) CHAOS_unfold) (auto simp add: T_Ndet T_STOP T_Mprefix)
qed

lemma ticks_CHAOS : ‹✓s(CHAOS A) = {}›
proof (rule equals0I)
  fix r :: 'r assume ‹r ∈ ✓s(CHAOS A)›
  then obtain s where ‹s @ [✓(r)] ∈ 𝒯 (CHAOS A)› unfolding ticks_of_def by blast
  thus False
    by (induct s; subst (asm) CHAOS_unfold)
      (auto simp add: T_Ndet T_STOP T_Mprefix split: if_split_asm)
qed


lemma events_of_CHAOS⇩S⇩K⇩I⇩P⇩S : ‹α(CHAOS⇩S⇩K⇩I⇩P⇩S A R) = A›
proof (intro subset_antisym subsetI)
  fix a assume ‹a ∈ A›
  hence ‹[ev a] ∈ 𝒯 (CHAOS⇩S⇩K⇩I⇩P⇩S A R)›
    by (subst CHAOS⇩S⇩K⇩I⇩P⇩S_unfold) (auto simp add: T_Ndet T_Mprefix)
  thus ‹a ∈ α(CHAOS⇩S⇩K⇩I⇩P⇩S A R)› by (force simp add: events_of_def)
next
  fix a assume ‹a ∈ α(CHAOS⇩S⇩K⇩I⇩P⇩S A R)›
  then obtain t where ‹ev a ∈ set t› ‹t ∈ 𝒯 (CHAOS⇩S⇩K⇩I⇩P⇩S A R)›
    by (auto simp add: events_of_def)
  thus ‹a ∈ A›
    by (induct t, simp, subst (asm) CHAOS⇩S⇩K⇩I⇩P⇩S_unfold)
      (auto simp add: T_Ndet T_STOP T_SKIPS T_Mprefix)
qed

lemma ticks_CHAOS⇩S⇩K⇩I⇩P⇩S : ‹✓s(CHAOS⇩S⇩K⇩I⇩P⇩S A R) = R›
proof (intro subset_antisym subsetI)
  fix r assume ‹r ∈ R›
  hence ‹[✓(r)] ∈ 𝒯 (CHAOS⇩S⇩K⇩I⇩P⇩S A R)› by (subst CHAOS⇩S⇩K⇩I⇩P⇩S_unfold) (simp add: T_Ndet T_SKIPS)
  thus ‹r ∈ ✓s(CHAOS⇩S⇩K⇩I⇩P⇩S A R)› by (metis append_Nil ticks_of_memI)
next
  fix r assume ‹r ∈ ✓s(CHAOS⇩S⇩K⇩I⇩P⇩S A R)›
  then obtain s where ‹s @ [✓(r)] ∈ 𝒯 (CHAOS⇩S⇩K⇩I⇩P⇩S A R)› unfolding ticks_of_def by blast
  thus ‹r ∈ R›
    by (induct s; subst (asm) CHAOS⇩S⇩K⇩I⇩P⇩S_unfold)
      (auto simp add: T_Ndet T_STOP T_SKIPS T_Mprefix)
qed


lemma RUN_subset_DT: ‹RUN B ⊑⇩D⇩T RUN A›
  if ‹A ⊆ B› for A B :: ‹'a set›
proof (subst RUN_def, induct rule: fix_ind)
  show ‹adm (λa. a ⊑⇩D⇩T RUN A)› by simp
next
  show ‹⊥ ⊑⇩D⇩T RUN A› by simp
next
  show ‹X ⊑⇩D⇩T RUN A ⟹ (Λ X. □b∈B → X)⋅X ⊑⇩D⇩T RUN A› for X :: ‹('a, 'r) process⇩p⇩t⇩i⇩c⇩k›
    by (subst RUN_unfold, simp)
      (meson Mprefix_DT_subset mono_Mprefix_DT ‹A ⊆ B› trans_DT)
qed


lemma CHAOS_subset_FD : ‹CHAOS B ⊑⇩F⇩D CHAOS A›
  if ‹A ⊆ B› for A B :: ‹'a set›
proof (subst CHAOS_def, induct rule: fix_ind)
  show ‹adm (λa. a ⊑⇩F⇩D CHAOS A)› by simp
next
  show ‹⊥ ⊑⇩F⇩D CHAOS A› by simp
next
  from ‹A ⊆ B› show ‹X ⊑⇩F⇩D CHAOS A ⟹ (Λ X. STOP ⊓ (□b∈B → X))⋅X ⊑⇩F⇩D CHAOS A›
    for X :: ‹('a, 'r) process⇩p⇩t⇩i⇩c⇩k›
    by (subst CHAOS_unfold)
      (auto simp add: refine_defs Mprefix_projs Ndet_projs F_STOP D_STOP)
qed


lemma CHAOS⇩S⇩K⇩I⇩P⇩S_subset_FD : ‹CHAOS⇩S⇩K⇩I⇩P⇩S B S ⊑⇩F⇩D CHAOS⇩S⇩K⇩I⇩P⇩S A R›
  if ‹A ⊆ B› ‹R ≠ {}› ‹R ⊆ S›
proof (subst CHAOS⇩S⇩K⇩I⇩P⇩S_def, induct rule: fix_ind)
  show ‹adm (λa. a ⊑⇩F⇩D CHAOS⇩S⇩K⇩I⇩P⇩S A R)› by simp
next
  show ‹⊥ ⊑⇩F⇩D CHAOS⇩S⇩K⇩I⇩P⇩S A R› by simp
next
  from ‹A ⊆ B› ‹R ≠ {}› ‹R ⊆ S›
  show ‹X ⊑⇩F⇩D CHAOS⇩S⇩K⇩I⇩P⇩S A R ⟹ (Λ X. SKIPS S ⊓ STOP ⊓ (□a∈B → X))⋅X ⊑⇩F⇩D CHAOS⇩S⇩K⇩I⇩P⇩S A R› for X
    by (subst CHAOS⇩S⇩K⇩I⇩P⇩S_unfold)
      (auto simp add: refine_defs Mprefix_projs Ndet_projs F_STOP D_STOP F_SKIPS D_SKIPS)
qed



section ‹Relations between refinements on reference processes›

lemma CHAOS_has_all_tickFree_failures : 
  ‹tF s ⟹ {a. ev a ∈ set s} ⊆ A ⟹ (s, X) ∈ ℱ (CHAOS A)›
proof (induct s)
  show ‹([], X) ∈ ℱ (CHAOS A)›
    by (subst CHAOS_unfold) (simp add: F_Ndet F_STOP)
next
  fix e s
  assume   hyp : ‹tF s ⟹ {a. ev a ∈ set s} ⊆ A ⟹ (s, X) ∈ ℱ (CHAOS A)›
  assume prems : ‹tF (e # s)› ‹{a. ev a ∈ set (e # s)} ⊆ A›
  from prems have ‹tF s› ‹{a. ev a ∈ set s} ⊆ A› by auto
  hence ‹(s, X) ∈ ℱ (CHAOS A)› by (fact hyp)
  with prems show ‹(e # s, X) ∈ ℱ (CHAOS A)›
    by (subst CHAOS_unfold, cases e) (auto simp add: F_Ndet F_Mprefix)
qed



lemma CHAOS⇩S⇩K⇩I⇩P⇩S_superset_events_of_ticks_of_leF : 
  ‹CHAOS⇩S⇩K⇩I⇩P⇩S A R ⊑⇩F P› if ‹α(P) ⊆ A› and ‹✓s(P) ⊆ R›
proof (unfold failure_refine_def)
  have ‹ftF s ⟹ set s ⊆ (⋃t∈𝒯 P. set t) ⟹ (s, X) ∈ ℱ (CHAOS⇩S⇩K⇩I⇩P⇩S A R)› for s X
  proof (induct s)
    show ‹([], X) ∈ ℱ (CHAOS⇩S⇩K⇩I⇩P⇩S A R)›
      by (subst CHAOS⇩S⇩K⇩I⇩P⇩S_unfold) (simp add: F_Ndet F_STOP)
  next
    fix e s
    assume prems : ‹ftF (e # s)› ‹set (e # s) ⊆ ⋃ (set ` 𝒯 P)›
    assume   hyp : ‹ftF s ⟹ set s ⊆ ⋃ (set ` 𝒯 P) ⟹ (s, X) ∈ ℱ (CHAOS⇩S⇩K⇩I⇩P⇩S A R)›
    show ‹(e # s, X) ∈ ℱ (CHAOS⇩S⇩K⇩I⇩P⇩S A R)›
    proof (cases e)
      fix a assume ‹e = ev a›
      with prems(2) have ‹a ∈ α(P)› by (auto simp add: events_of_def)
      with ‹α(P) ⊆ A› have ‹a ∈ A› by fast
      from prems have ‹ftF s› ‹set s ⊆ ⋃ (set ` 𝒯 P)›
        by auto (metis front_tickFree_Cons_iff front_tickFree_Nil)
      hence ‹(s, X) ∈ ℱ (CHAOS⇩S⇩K⇩I⇩P⇩S A R)› by (fact hyp)
      thus ‹(e # s, X) ∈ ℱ (CHAOS⇩S⇩K⇩I⇩P⇩S A R)›
        by (subst CHAOS⇩S⇩K⇩I⇩P⇩S_unfold) (simp add: F_Ndet F_Mprefix ‹e = ev a› ‹a ∈ A›)
    next
      fix r assume ‹e = ✓(r)›
      with prems(2) have ‹r ∈ ✓s(P)›
        by (simp add: ticks_of_def)
          (metis T_imp_front_tickFree front_tickFree_Cons_iff front_tickFree_append_iff
            in_set_conv_decomp non_tickFree_tick tickFree_Cons_iff tickFree_Nil)
      with ‹✓s(P) ⊆ R› have ‹r ∈ R› by fast
      moreover from ‹e = ✓(r)› prems(1) have ‹s = []› by (simp add: front_tickFree_Cons_iff)
      ultimately show ‹(e # s, X) ∈ ℱ (CHAOS⇩S⇩K⇩I⇩P⇩S A R)›
        by (subst CHAOS⇩S⇩K⇩I⇩P⇩S_unfold) (auto simp add: F_Ndet F_SKIPS ‹e = ✓(r)›)
    qed
  qed
  thus ‹ℱ P ⊆ ℱ (CHAOS⇩S⇩K⇩I⇩P⇩S A R)› by (meson F_T F_imp_front_tickFree SUP_upper subrelI)
qed


corollary CHAOS⇩S⇩K⇩I⇩P⇩S_events_of_ticks_of_leF: ‹CHAOS⇩S⇩K⇩I⇩P⇩S α(P) ✓s(P) ⊑⇩F P› 
  and CHAOS⇩S⇩K⇩I⇩P⇩S_UNIV_UNIV_leF: ‹CHAOS⇩S⇩K⇩I⇩P⇩S UNIV UNIV ⊑⇩F P›
  by (simp_all add: CHAOS⇩S⇩K⇩I⇩P⇩S_superset_events_of_ticks_of_leF)


lemma DF⇩S⇩K⇩I⇩P⇩S_F_DF : ‹DF⇩S⇩K⇩I⇩P⇩S A R ⊑⇩F DF A›
  by (simp add: DF⇩S⇩K⇩I⇩P⇩S_FD_DF leFD_imp_leF)

lemma DF_F_RUN : ‹DF A ⊑⇩F RUN A› for A :: ‹'a set›
proof (unfold DF_def, induct rule: fix_ind)
  show ‹adm (λa. a ⊑⇩F RUN A)› by simp
next
  show ‹⊥ ⊑⇩F RUN A› by simp
next
  show ‹X ⊑⇩F RUN A ⟹ (Λ X. ⊓a∈A → X)⋅X ⊑⇩F RUN A› for X :: ‹('a, 'r) process⇩p⇩t⇩i⇩c⇩k›
    by (subst RUN_unfold, simp)    
      (meson Mndetprefix_F_Mprefix mono_Mprefix_F trans_F)
qed

lemma CHAOS_F_DF : ‹CHAOS A ⊑⇩F DF A›
proof (unfold failure_refine_def, safe, rule CHAOS_has_all_tickFree_failures)
  show ‹(s, X) ∈ ℱ (DF A) ⟹ tF s› for s :: ‹('a, 'r) trace⇩p⇩t⇩i⇩c⇩k› and X
    by (metis F_T no_ticks_imp_tickFree_T ticks_DF)
next
  show ‹(s, X) ∈ ℱ (DF A) ⟹ {a. ev a ∈ set s} ⊆ A› for s :: ‹('a, 'r) trace⇩p⇩t⇩i⇩c⇩k› and X
    by (drule F_T) (use events_of_DF[of A] in ‹auto simp add: events_of_def›)
qed

corollary CHAOS⇩S⇩K⇩I⇩P⇩S_F_CHAOS : ‹CHAOS⇩S⇩K⇩I⇩P⇩S A R ⊑⇩F CHAOS A›
  and CHAOS⇩S⇩K⇩I⇩P⇩S_F_DF⇩S⇩K⇩I⇩P⇩S : ‹CHAOS⇩S⇩K⇩I⇩P⇩S A R ⊑⇩F DF⇩S⇩K⇩I⇩P⇩S A R›
  by (rule CHAOS⇩S⇩K⇩I⇩P⇩S_superset_events_of_ticks_of_leF;
      simp add: events_of_CHAOS ticks_CHAOS events_of_DF⇩S⇩K⇩I⇩P⇩S ticks_DF⇩S⇩K⇩I⇩P⇩S)+




lemma div_free_CHAOS⇩S⇩K⇩I⇩P⇩S: ‹𝒟 (CHAOS⇩S⇩K⇩I⇩P⇩S A R) = {}›
proof (rule equals0I)
  show ‹s ∈ 𝒟 (CHAOS⇩S⇩K⇩I⇩P⇩S A R) ⟹ False› for s
    by (induct s; subst (asm) CHAOS⇩S⇩K⇩I⇩P⇩S_unfold)
      (auto simp add: D_Ndet D_STOP D_SKIPS D_Mprefix)
qed


lemma div_free_CHAOS: ‹𝒟 (CHAOS A) = {}›
proof (rule equals0I)
  show ‹s ∈ 𝒟 (CHAOS A) ⟹ False› for s :: ‹('a, 'r) trace⇩p⇩t⇩i⇩c⇩k›
    by (induct s; subst (asm) CHAOS_unfold)
      (auto simp add: D_Ndet D_STOP D_Mprefix)
qed


lemma div_free_RUN: ‹𝒟 (RUN A) = {}›
proof (rule equals0I)
  show ‹s ∈ 𝒟 (RUN A) ⟹ False› for s :: ‹('a, 'r) trace⇩p⇩t⇩i⇩c⇩k›
    by (induct s; subst (asm) RUN_unfold) (auto simp add: D_Mprefix)
qed

(* DF⇩S⇩K⇩I⇩P⇩S_FD_DF : "DF⇩S⇩K⇩I⇩P⇩S A R ⊑⇩F⇩D DF A" *)

corollary DF_FD_RUN : ‹DF A  ⊑⇩F⇩D RUN A›
  and CHAOS_FD_DF : ‹CHAOS A  ⊑⇩F⇩D DF A›
  and CHAOS⇩S⇩K⇩I⇩P⇩S_FD_CHAOS : ‹CHAOS⇩S⇩K⇩I⇩P⇩S A R ⊑⇩F⇩D CHAOS A›
  and CHAOS⇩S⇩K⇩I⇩P⇩S_FD_DF⇩S⇩K⇩I⇩P⇩S : ‹CHAOS⇩S⇩K⇩I⇩P⇩S A R ⊑⇩F⇩D DF⇩S⇩K⇩I⇩P⇩S A R›
  by (simp_all add: DF_F_RUN div_free_RUN CHAOS_F_DF div_free_DF CHAOS⇩S⇩K⇩I⇩P⇩S_F_CHAOS div_free_CHAOS
      CHAOS⇩S⇩K⇩I⇩P⇩S_F_DF⇩S⇩K⇩I⇩P⇩S div_free_DF⇩S⇩K⇩I⇩P⇩S divergence_refine_def leF_leD_imp_leFD)



lemma traces_CHAOS_subset : ‹𝒯 (CHAOS A) ⊆ {s. set s ⊆ ev ` A}›
proof (rule subsetI)
  show ‹s ∈ 𝒯 (CHAOS A) ⟹ s ∈ {s. set s ⊆ ev ` A}› for s :: ‹('a, 'r) trace⇩p⇩t⇩i⇩c⇩k›
    by (induct s; subst (asm) CHAOS_unfold) (auto simp add: T_Ndet T_STOP T_Mprefix)
qed

lemma traces_RUN_superset : ‹{s. set s ⊆ ev ` A} ⊆ 𝒯 (RUN A)›
proof (rule subsetI)
  show ‹s ∈ {s. set s ⊆ ev ` A} ⟹ s ∈ 𝒯 (RUN A)› for s :: ‹('a, 'r) trace⇩p⇩t⇩i⇩c⇩k›
    by (induct s, simp) (subst RUN_unfold, auto simp add: T_Mprefix)
qed

corollary RUN_all_tickfree_traces1   : ‹𝒯 (RUN   A) = {s. set s ⊆ ev ` A}› 
  and     DF_all_tickfree_traces1    : ‹𝒯 (DF    A) = {s. set s ⊆ ev ` A}›
  and     CHAOS_all_tickfree_traces1 : ‹𝒯 (CHAOS A) = {s. set s ⊆ ev ` A}›
  using DF_F_RUN[THEN leF_imp_leT, simplified trace_refine_def]
    CHAOS_F_DF[THEN leF_imp_leT,simplified trace_refine_def] 
    traces_CHAOS_subset traces_RUN_superset by blast+

corollary RUN_all_tickfree_traces2  : ‹s ∈ 𝒯 (RUN   UNIV)› 
  and     DF_all_tickfree_traces2   : ‹s ∈ 𝒯 (DF    UNIV)› 
  and     CHAOS_all_tickfree_trace2 : ‹s ∈ 𝒯 (CHAOS UNIV)› if ‹tF s›
  using ‹tF s›
  by (simp add: tickFree_def RUN_all_tickfree_traces1 DF_all_tickfree_traces1
      CHAOS_all_tickfree_traces1 disjoint_iff image_iff subset_iff; metis event⇩p⇩t⇩i⇩c⇩k.exhaust)+


lemma traces_CHAOS⇩S⇩K⇩I⇩P⇩S_subset :
  ‹𝒯 (CHAOS⇩S⇩K⇩I⇩P⇩S A R) ⊆ {s. ftF s ∧ set s ⊆ ev ` A ∪ tick ` R}›
proof (rule subsetI)
  show ‹s ∈ 𝒯 (CHAOS⇩S⇩K⇩I⇩P⇩S A R) ⟹ s ∈ {s. ftF s ∧ set s ⊆ ev ` A ∪ tick ` R}› for s
    by (induct s; subst (asm) CHAOS⇩S⇩K⇩I⇩P⇩S_unfold)
      (auto simp add: T_Ndet T_STOP T_SKIPS T_Mprefix front_tickFree_Cons_iff)
qed


lemma traces_DF⇩S⇩K⇩I⇩P⇩S_superset : 
  ‹{s. ftF s ∧ set s ⊆ ev ` A ∪ tick ` R} ⊆ 𝒯 (DF⇩S⇩K⇩I⇩P⇩S A R)›
proof (rule subsetI)
  show ‹s ∈ {s. ftF s ∧ set s ⊆ ev ` A ∪ tick ` R} ⟹ s ∈ 𝒯 (DF⇩S⇩K⇩I⇩P⇩S A R) › for s
    by (induct s; subst DF⇩S⇩K⇩I⇩P⇩S_unfold)
      (auto simp add: T_Ndet T_SKIPS T_Mndetprefix write0_def T_Mprefix front_tickFree_Cons_iff)
qed



corollary DF⇩S⇩K⇩I⇩P⇩S_all_front_tickfree_traces1: 
  ‹𝒯 (DF⇩S⇩K⇩I⇩P⇩S A R) = {s. ftF s ∧ set s ⊆ ev ` A ∪ tick ` R}›
  and CHAOS⇩S⇩K⇩I⇩P⇩S_all_front_tickfree_traces1: 
  ‹𝒯 (CHAOS⇩S⇩K⇩I⇩P⇩S A R) = {s. ftF s ∧ set s ⊆ ev ` A ∪ tick ` R}›
  using CHAOS⇩S⇩K⇩I⇩P⇩S_F_DF⇩S⇩K⇩I⇩P⇩S[THEN leF_imp_leT, simplified trace_refine_def]
    traces_CHAOS⇩S⇩K⇩I⇩P⇩S_subset traces_DF⇩S⇩K⇩I⇩P⇩S_superset by blast+


corollary DF⇩S⇩K⇩I⇩P⇩S_all_front_tickfree_traces2   : ‹s ∈ 𝒯 (DF⇩S⇩K⇩I⇩P⇩S UNIV UNIV)›
  and CHAOS⇩S⇩K⇩I⇩P⇩S_all_front_tickfree_traces2: ‹s ∈ 𝒯 (CHAOS⇩S⇩K⇩I⇩P⇩S UNIV UNIV)›
  if ‹ftF s›
  using ‹ftF s›
  by (simp add: tickFree_def DF⇩S⇩K⇩I⇩P⇩S_all_front_tickfree_traces1 CHAOS⇩S⇩K⇩I⇩P⇩S_all_front_tickfree_traces1;
      metis UnCI event⇩p⇩t⇩i⇩c⇩k.exhaust rangeI subsetI)+


corollary DF⇩S⇩K⇩I⇩P⇩S_UNIV_UNIV_leT :    ‹DF⇩S⇩K⇩I⇩P⇩S UNIV UNIV ⊑⇩T P›
  and  CHAOS⇩S⇩K⇩I⇩P⇩S_UNIV_UNIV_leT : ‹CHAOS⇩S⇩K⇩I⇩P⇩S UNIV UNIV ⊑⇩T P›
  by (simp add:trace_refine_def DF⇩S⇩K⇩I⇩P⇩S_all_front_tickfree_traces2 is_processT2_TR subsetI) 
    (simp add:trace_refine_def CHAOS⇩S⇩K⇩I⇩P⇩S_all_front_tickfree_traces2 is_processT2_TR subsetI)

lemma deadlock_free_implies_lifelock_free: ‹deadlock_free P ⟹ lifelock_free P›
  unfolding deadlock_free_def lifelock_free_def
  using CHAOS_FD_DF trans_FD by blast

lemma deadlock_free_implies_non_terminating:
  ‹tF s› if ‹deadlock_free P› ‹s ∈ 𝒯 P›
proof -
  from ‹deadlock_free P› have ‹𝒯 P ⊆ 𝒯 (DF UNIV)›
    by (simp add: deadlock_free_def le_ref2T)
  with ‹s ∈ 𝒯 P› show ‹tF s›
    by (meson no_ticks_imp_tickFree_T subsetD ticks_DF)
qed



lemma deadlock_free⇩S⇩K⇩I⇩P⇩S_is_right: 
  ‹deadlock_free⇩S⇩K⇩I⇩P⇩S (P :: ('a, 'r) process⇩p⇩t⇩i⇩c⇩k) ⟷
   (∀s∈𝒯 P. tF s ⟶ (s, UNIV :: ('a, 'r) event⇩p⇩t⇩i⇩c⇩k set) ∉ ℱ P)›
proof (intro iffI ballI impI)
  have ‹tF s ⟹ (s, UNIV) ∉ ℱ (DF⇩S⇩K⇩I⇩P⇩S UNIV UNIV)› for s :: ‹('a, 'r) event⇩p⇩t⇩i⇩c⇩k list›
    by (induct s; subst DF⇩S⇩K⇩I⇩P⇩S_unfold)
      (auto simp add: F_Ndet F_SKIPS F_Mndetprefix write0_def F_Mprefix)
  thus ‹deadlock_free⇩S⇩K⇩I⇩P⇩S P ⟹ s ∈ 𝒯 P ⟹ tF s ⟹ (s, UNIV) ∉ ℱ P› for s
    using deadlock_free⇩S⇩K⇩I⇩P⇩S_def failure_refine_def by blast
next
  assume as1 : ‹∀s∈𝒯 P. tF s ⟶ (s, UNIV) ∉ ℱ P›
  have as2 : ‹ftF s ⟹ (∃a ∈ UNIV. ev a ∉ X) ⟹
              (s, X) ∈ ℱ (DF⇩S⇩K⇩I⇩P⇩S UNIV UNIV)› for s :: ‹('a, 'r) trace⇩p⇩t⇩i⇩c⇩k› and X
  proof(induct s)
    case Nil
    then show ?case
      by (subst DF⇩S⇩K⇩I⇩P⇩S_unfold, auto simp add:F_Mndetprefix write0_def F_Mprefix F_Ndet F_SKIP)
  next
    case (Cons hds tls)
    then show ?case 
    proof (simp add: DF⇩S⇩K⇩I⇩P⇩S_def fix_def)
      define Y where "Y ≡ λi. iterate i⋅(Λ x. (⊓xa∈(UNIV :: 'a set) →  x) ⊓ SKIPS (UNIV :: 'r set))⋅⊥"
      assume a:"ftF (hds # tls)" and b:"ftF tls ⟹ (tls, X) ∈ ℱ (⨆i. Y i)"
        and c:"∃a. ev a ∉ X"
      from Y_def have cc:"chain Y" by simp
      from b have d:"ftF tls ⟹ ∃a∈UNIV. ev a ∉ X ⟹(tls, X) ∈ ℱ (Y i)" for i 
        using F_LUB[OF cc] limproc_is_thelub[OF cc] by simp
      from Y_def have e:"ℱ(Mndetprefix UNIV (λx. Y i) ⊓ SKIPS UNIV) ⊆ ℱ (Y (Suc i))" for i by(simp)
      from a have f:"tls ≠ [] ⟹ hds ∉ range tick" "ftF tls"
        by (metis event⇩p⇩t⇩i⇩c⇩k.disc(2) front_tickFree_Cons_iff imageE)
          (metis a front_tickFree_Cons_iff front_tickFree_Nil)
      have g:"(hds#tls, X) ∈ ℱ (Y (Suc i))" for i
        using f c e[of i] d[of i] 
        by (auto simp: F_Mndetprefix write0_def F_Mprefix Y_def F_Ndet F_SKIPS image_iff)
          (meson event⇩p⇩t⇩i⇩c⇩k.exhaust)+
      have h:"(hds#tls, X) ∈ ℱ (Y 0)"
        using D_F cc g po_class.chainE proc_ord2a by blast
      from a b c show "(hds#tls, X) ∈ ℱ (⨆i. Y i)"
        using F_LUB[OF cc] is_ub_thelub[OF cc] 
        by (metis D_LUB_2 cc g limproc_is_thelub po_class.chainE proc_ord2a process_charn) 
    qed   
  qed
  show "deadlock_free⇩S⇩K⇩I⇩P⇩S P"
  proof(unfold deadlock_free⇩S⇩K⇩I⇩P⇩S_def failure_refine_def, safe)
    fix s X
    assume as3:"(s, X) ∈ ℱ P"
    hence a1:"s ∈ 𝒯 P" "ftF s" 
      using F_T as3 is_processT2 by blast+
    show "(s, X) ∈ ℱ (DF⇩S⇩K⇩I⇩P⇩S UNIV UNIV)" 
    proof(cases "tF s")
      case FT_True:True
      hence a2:"(s, UNIV) ∉ ℱ P"
        using a1 as1 by blast
      then show ?thesis 
        by (metis DF⇩S⇩K⇩I⇩P⇩S_all_front_tickfree_traces2 FT_True UNIV_I UNIV_eq_I a1(2) as2 as3
            event⇩p⇩t⇩i⇩c⇩k.exhaust is_processT6_TR_notin tickFree_imp_front_tickFree_snoc)
    next
      case FT_False: False                                                                 
      then show ?thesis 
        by (metis DF⇩S⇩K⇩I⇩P⇩S_all_front_tickfree_traces2 a1(2) front_tickFree_append_iff
            is_processT2_TR is_processT5_S7 list.distinct(1))
    qed 
  qed
qed 

lemma deadlock_free⇩S⇩K⇩I⇩P⇩S_implies_div_free: ‹deadlock_free⇩S⇩K⇩I⇩P⇩S P ⟹ 𝒟 P = {}›
  by (metis D_T D_imp_front_tickFree T_nonTickFree_imp_decomp all_not_in_conv butlast_snoc
      deadlock_free⇩S⇩K⇩I⇩P⇩S_is_right front_tickFree_iff_tickFree_butlast is_processT8 is_processT9)

corollary deadlock_free⇩S⇩K⇩I⇩P⇩S_FD: ‹deadlock_free⇩S⇩K⇩I⇩P⇩S P ⟷ DF⇩S⇩K⇩I⇩P⇩S UNIV UNIV ⊑⇩F⇩D P›
  by (metis deadlock_free⇩S⇩K⇩I⇩P⇩S_def deadlock_free⇩S⇩K⇩I⇩P⇩S_implies_div_free
      less_eq_process⇩p⇩t⇩i⇩c⇩k_def order_refl refine_defs(3))

lemma all_events_ticks_refusal: 
  ‹(s, tick ` ✓s(P) ∪ ev ` α(P)) ∈ ℱ P ⟹ (s, UNIV) ∈ ℱ P›
proof (rule ccontr)
  assume ‹(s, tick ` ✓s(P) ∪ ev ` α(P)) ∈ ℱ P› and ‹(s, UNIV) ∉ ℱ P›
  then obtain c where ‹c ∉ tick ` ✓s(P) ∪ ev ` α(P) ∧ s @ [c] ∈ 𝒯 P›
    using is_processT5[of s ‹tick ` ✓s(P) ∪ ev ` α(P)› P 
        ‹UNIV - (tick ` ✓s(P) ∪ ev ` α(P))›, simplified] F_T by blast
  thus False by (simp add: events_of_def ticks_of_def, cases c) fastforce+
qed

corollary deadlock_free⇩S⇩K⇩I⇩P⇩S_is_right_wrt_events:
  ‹deadlock_free⇩S⇩K⇩I⇩P⇩S P ⟷ 
   (∀s∈𝒯 P. tF s ⟶ (s, tick ` ✓s(P) ∪ ev ` α(P)) ∉ ℱ P)›
  unfolding deadlock_free⇩S⇩K⇩I⇩P⇩S_is_right using all_events_ticks_refusal is_processT4 by blast


lemma deadlock_free_imp_deadlock_free⇩S⇩K⇩I⇩P⇩S: ‹deadlock_free P ⟹ deadlock_free⇩S⇩K⇩I⇩P⇩S P›
  using DF⇩S⇩K⇩I⇩P⇩S_FD_DF deadlock_free⇩S⇩K⇩I⇩P⇩S_FD deadlock_free_def trans_FD by blast




section ‹\<^const>‹deadlock_free› and ‹deadlock_free⇩S⇩K⇩I⇩P⇩S› with \<^const>‹SKIP› and \<^const>‹STOP››

lemma non_deadlock_free⇩S⇩K⇩I⇩P⇩S_STOP: ‹¬ deadlock_free⇩S⇩K⇩I⇩P⇩S STOP›
  by (unfold deadlock_free⇩S⇩K⇩I⇩P⇩S_def, subst DF⇩S⇩K⇩I⇩P⇩S_unfold, unfold failure_refine_def)
    (auto simp add: F_Ndet F_STOP F_SKIPS F_Mndetprefix write0_def F_Mprefix)

lemma non_deadlock_free_STOP: ‹¬ deadlock_free STOP›
  using deadlock_free_imp_deadlock_free⇩S⇩K⇩I⇩P⇩S non_deadlock_free⇩S⇩K⇩I⇩P⇩S_STOP by blast


lemma deadlock_free⇩S⇩K⇩I⇩P⇩S_SKIPS : ‹deadlock_free⇩S⇩K⇩I⇩P⇩S (SKIPS R) ⟷ R ≠ {}›
proof (rule iffI)
  show ‹deadlock_free⇩S⇩K⇩I⇩P⇩S (SKIPS R) ⟹ R ≠ {}›
    by (rule ccontr, simp add: SKIPS_def)
      (use non_deadlock_free⇩S⇩K⇩I⇩P⇩S_STOP in blast)
next
  show ‹R ≠ {} ⟹ deadlock_free⇩S⇩K⇩I⇩P⇩S (SKIPS R)›
    by (unfold deadlock_free⇩S⇩K⇩I⇩P⇩S_def, subst DF⇩S⇩K⇩I⇩P⇩S_unfold, unfold failure_refine_def)
      (auto simp add: F_Ndet F_STOP F_SKIPS F_Mndetprefix write0_def F_Mprefix subset_iff)
qed


lemma deadlock_free⇩S⇩K⇩I⇩P⇩S_SKIP: ‹deadlock_free⇩S⇩K⇩I⇩P⇩S (SKIP r)›
  by (metis SKIPS_singl_is_SKIP deadlock_free⇩S⇩K⇩I⇩P⇩S_SKIPS empty_not_insert)

lemma non_deadlock_free_SKIPS : ‹¬ deadlock_free (SKIPS R)›
proof (cases ‹R = {}›)
  show ‹R = {} ⟹ ¬ deadlock_free (SKIPS R)›
    by (simp add: non_deadlock_free_STOP)
next
  assume ‹R ≠ {}›
  then obtain r where ‹r ∈ R› by blast
  hence ‹[✓(r)] ∈ 𝒯 (SKIPS R)› by (simp add: T_SKIPS)
  moreover have ‹¬ tF ([✓(r)])› by simp
  ultimately show ‹¬ deadlock_free (SKIPS R)›
    using deadlock_free_implies_non_terminating by blast
qed


lemma non_deadlock_free_SKIP: ‹¬ deadlock_free (SKIP r)›
  by (metis SKIPS_singl_is_SKIP non_deadlock_free_SKIPS)




corollary non_terminating_refine_DF : ‹non_terminating P ⟷ DF UNIV ⊑⇩T P› 
  and non_terminating_refine_CHAOS : ‹non_terminating P ⟷ CHAOS UNIV ⊑⇩T P›
  by (simp_all add: DF_all_tickfree_traces1 RUN_all_tickfree_traces1 CHAOS_all_tickfree_traces1 
      non_terminating_def trace_refine_def)

lemma non_terminating_is_right : ‹non_terminating P ⟷ (∀s∈𝒯 P. tF s)›
  by (meson RUN_all_tickfree_traces2 no_ticks_imp_tickFree_T
      non_terminating_def subset_iff ticks_RUN trace_refine_def)

lemma nonterminating_implies_div_free : ‹non_terminating P ⟹ 𝒟 P = {}›
  by (metis D_T ex_in_conv front_tickFree_single is_processT7
      non_terminating_is_right non_tickFree_tick tickFree_append_iff)

lemma non_terminating_implies_F : ‹non_terminating P ⟹ CHAOS UNIV ⊑⇩F P›
  by (meson CHAOS_has_all_tickFree_failures F_T failure_refine_def in_mono no_ticks_imp_tickFree_T
      non_terminating_refine_CHAOS subrelI ticks_CHAOS top_greatest trace_refine_def)

corollary non_terminating_F : ‹non_terminating P ⟷ CHAOS UNIV ⊑⇩F P›
  by (auto simp add:non_terminating_implies_F non_terminating_refine_CHAOS leF_imp_leT)

corollary non_terminating_FD : ‹non_terminating P ⟷ CHAOS UNIV ⊑⇩F⇩D P›
  by (metis failure_refine_def less_eq_process⇩p⇩t⇩i⇩c⇩k_def non_terminating_F
      nonterminating_implies_div_free order_refl)



corollary lifelock_free_is_non_terminating: ‹lifelock_free P = non_terminating P›
  unfolding lifelock_free_def non_terminating_FD by (fact refl)

lemma divergence_refine_div_free :
  ‹CHAOS⇩S⇩K⇩I⇩P⇩S UNIV UNIV ⊑⇩D P ⟷ 𝒟 P = {}›
  ‹CHAOS UNIV ⊑⇩D P         ⟷ 𝒟 P = {}›
  ‹RUN UNIV ⊑⇩D P           ⟷ 𝒟 P = {}› 
  ‹DF⇩S⇩K⇩I⇩P⇩S UNIV UNIV ⊑⇩D P   ⟷ 𝒟 P = {}›
  ‹DF UNIV ⊑⇩D P            ⟷ 𝒟 P = {}›
  by (simp_all add: div_free_CHAOS div_free_RUN div_free_DF div_free_DF⇩S⇩K⇩I⇩P⇩S
      div_free_CHAOS⇩S⇩K⇩I⇩P⇩S divergence_refine_def)



lemma lifelock_free⇩S⇩K⇩I⇩P⇩S_iff_div_free : ‹lifelock_free⇩S⇩K⇩I⇩P⇩S P ⟷ 𝒟 P = {}›
  by (simp add: CHAOS⇩S⇩K⇩I⇩P⇩S_UNIV_UNIV_leF divergence_refine_div_free(1)
      failure_divergence_refine_def lifelock_free⇩S⇩K⇩I⇩P⇩S_def)

lemma lifelock_free_imp_lifelock_free⇩S⇩K⇩I⇩P⇩S : ‹lifelock_free P ⟹ lifelock_free⇩S⇩K⇩I⇩P⇩S P›
  by (simp add: lifelock_free⇩S⇩K⇩I⇩P⇩S_iff_div_free lifelock_free_is_non_terminating
      nonterminating_implies_div_free)

corollary deadlock_free⇩S⇩K⇩I⇩P⇩S_imp_lifelock_free⇩S⇩K⇩I⇩P⇩S: ‹deadlock_free⇩S⇩K⇩I⇩P⇩S P ⟹ lifelock_free⇩S⇩K⇩I⇩P⇩S P›
  by (simp add: deadlock_free⇩S⇩K⇩I⇩P⇩S_implies_div_free lifelock_free⇩S⇩K⇩I⇩P⇩S_iff_div_free)



lemma non_terminating_Seq : ‹P ❙; Q = P› if ‹non_terminating P›
proof -
  from ‹non_terminating P› have * : ‹s ∈ 𝒯 P ⟹ tF s› for s
    unfolding non_terminating_is_right ..
  show ‹P ❙; Q = P›
  proof (subst Process_eq_spec_optimized, safe)
    from "*" show ‹s ∈ 𝒟 (P ❙; Q) ⟹ s ∈ 𝒟 P› for s by (force simp add: D_Seq)
  next
    show ‹s ∈ 𝒟 P ⟹ s ∈ 𝒟 (P ❙; Q)› for s by (simp add: D_Seq)
  next
    show ‹(s, X) ∈ ℱ (P ❙; Q) ⟹ (s, X) ∈ ℱ P› for s X
      by (simp add: F_Seq)
        (meson "*" is_processT4 is_processT8 non_tickFree_tick sup_ge1 tickFree_append_iff)
  next
    show ‹(s, X) ∈ ℱ P ⟹ (s, X) ∈ ℱ (P ❙; Q)› for s X
      by (simp add: F_Seq)
        (metis (mono_tags, lifting) "*" F_T f_inv_into_f is_processT5_S7'
          non_tickFree_tick tickFree_append_iff)
  qed
qed


lemma non_terminating_Sync :
  ‹non_terminating P ⟹ lifelock_free⇩S⇩K⇩I⇩P⇩S Q ⟹ non_terminating (P ⟦A⟧ Q)›
  by (simp add: lifelock_free⇩S⇩K⇩I⇩P⇩S_iff_div_free T_Sync
      non_terminating_is_right nonterminating_implies_div_free)
    (metis SyncWithTick_imp_NTF T_imp_front_tickFree ftf_Sync
      nonTickFree_n_frontTickFree non_tickFree_tick tickFree_append_iff)


lemmas non_terminating_Par = non_terminating_Sync[where A = ‹UNIV›]
  and non_terminating_Inter = non_terminating_Sync[where A = ‹{}›]



(*<*)
end
  (*>*)