(*<*)
―‹ ********************************************************************
 * 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_ptick›
  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_SKIPS :: ‹'a set → 'r set → ('a,'r) process_ptick›
  where ‹DF_SKIPS A R ≡ μ X. (⊓a ∈ A → X) ⊓ SKIPS R›

lemma DF_{SKIPS_unfold} : ‹DF_SKIPS A R = (⊓a ∈ A → DF_SKIPS A R) ⊓ SKIPS R›
  by (simp add: DF_{SKIPS_def}, rule trans, rule fix_eq, simp)


definition RUN :: ‹'a set → ('a,'r) process_ptick›
  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_ptick›
  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_SKIPS :: ‹'a set → 'r set → ('a,'r) process_ptick›
  where ‹CHAOS_SKIPS A R ≡ μ X. SKIPS R ⊓ STOP ⊓ (◻a∈A → X)›

lemma CHAOS_{SKIPS_unfold}: ‹CHAOS_SKIPS A R = SKIPS R ⊓ STOP ⊓ (◻a ∈ A → CHAOS_SKIPS A R)›
  by (simp add: CHAOS_{SKIPS_def}, rule trans, rule fix_eq, simp)



section ‹Assertions›

definition deadlock_free :: ‹('a,'r) process_ptick → bool›
  where ‹deadlock_free P ≡ DF UNIV ⊑_FD P›


definition deadlock_free_SKIPS :: ‹('a, 'r) process_ptick → bool›
  where ‹deadlock_free_SKIPS P ≡ DF_SKIPS UNIV UNIV ⊑_F P›


definition lifelock_free :: ‹('a,'r) process_ptick → bool›
  where ‹lifelock_free P ≡ CHAOS UNIV ⊑_FD P›


definition lifelock_free_SKIPS :: ‹('a,'r) process_ptick → bool›
  where ‹lifelock_free_SKIPS P ≡ CHAOS_SKIPS UNIV UNIV ⊑_FD P›


definition non_terminating :: ‹('a,'r) process_ptick → bool›
  where ‹non_terminating P ≡ RUN UNIV ⊑_T P›



section ‹Properties›

lemma DF_{SKIPS_FD_DF} : ‹DF_SKIPS A R ⊑_FD DF A›
proof (subst DF_{SKIPS_def}, induct rule: fix_ind)
  show ‹adm (λa. a ⊑_FD DF A)› by simp
next
  show ‹⊥ ⊑_FD DF A› by simp
next
  show ‹X ⊑_FD DF A ==> (Λ X. (⊓a∈A → X) ⊓ SKIPS R)⋅X ⊑_FD 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 ⊑_FD 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 ⊑_FD DF A› if ‹A ≠ {}› ‹A ⊆ B› for A B :: ‹'a set›
proof (subst DF_def, induct rule: fix_ind)
  show ‹adm (λa. a ⊑_FD DF A)› by simp
next
  show ‹⊥ ⊑_FD DF A› by simp
next
  show ‹X ⊑_FD DF A ==> (Λ X. ⊓b∈B → X)⋅X ⊑_FD DF A› for X :: ‹('a, 'r) process_ptick›
    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 ⊑_FD 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_{SKIPS_subset} : ‹DF_SKIPS B S ⊑_FD DF_SKIPS A R›
  if ‹A ≠ {}› ‹A ⊆ B› ‹R ≠ {}› ‹R ⊆ S›
proof (subst DF_{SKIPS_def}, induct rule: fix_ind)
  show ‹adm (λa. a ⊑_FD DF_SKIPS A R)› by simp
next
  show ‹⊥ ⊑_FD DF_SKIPS A R› by simp
next
  show ‹(Λ X. (⊓b∈B → X) ⊓ SKIPS S)⋅X ⊑_FD DF_SKIPS A R› if ‹X ⊑_FD DF_SKIPS A R› for X
  proof (subst DF_{SKIPS_unfold}, subst beta_cfun)
    show ‹cont (λX. (⊓b∈B → X) ⊓ SKIPS S)› by simp
  next
    show ‹(⊓b∈B → X) ⊓ SKIPS S ⊑_FD (⊓a∈A → DF_SKIPS A R) ⊓ SKIPS R›
    proof (rule mono_Ndet_FD)
      show ‹⊓b∈B → X ⊑_FD ⊓a∈A → DF_SKIPS A R›
        by (meson Mndetprefix_FD_subset ‹A ≠ {}› ‹A ⊆ B›
            mono_Mndetprefix_FD ‹X ⊑_FD DF_SKIPS A R› trans_FD)
    next
      show ‹SKIPS S ⊑_FD SKIPS R›
        by (simp add: SKIPS_FD_SKIPS_iff ‹R ≠ {}› ‹R ⊆ S›)
    qed
  qed
qed


lemma DF_{SKIPS_Univ_freeness} : ‹[A ≠ {}; R ≠ {}; DF_SKIPS A R ⊑_FD P] ==> deadlock_free_SKIPS P›
  by (meson DF_{SKIPS_subset} deadlock_free_{SKIPS_def} leFD_imp_leF subset_UNIV trans_F)

lemma deadlock_free_{SKIPS_Ndet_iff} :
  ‹deadlock_free_SKIPS (P ⊓ Q) ⟷ deadlock_free_SKIPS P ∧ deadlock_free_SKIPS Q›
  by (simp add: F_Ndet deadlock_free_{SKIPS_def} failure_refine_def)


lemma div_free_DF_SKIPS: ‹D (DF_SKIPS A R) = {}›
proof (rule equals0I)
  show ‹s ∈ D (DF_SKIPS A R) ==> False› for s
    by (induct s; subst (asm) DF_{SKIPS_unfold})
      (auto simp add: D_Ndet D_SKIPS D_Mndetprefix write0_def D_Mprefix split: if_split_asm)
qed


lemma div_free_DF: ‹D (DF A) = {}›
  by (metis DF_{SKIPS_FD_DF} div_free_DF_SKIPS empty_subsetI subset_antisym le_ref1)


lemma deadlock_free_implies_div_free: ‹deadlock_free P ==> D 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 ∈ T P ==> tF s›
  by (simp add: ticks_of_def tickFree_def disjoint_iff image_iff)
    (metis T_nonTickFree_imp_decomp event_ptick.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] ∈ T (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_ptick)›
  then obtain t :: ‹('a, 'r) trace_ptick› where ‹ev a ∈ set t› ‹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)] ∈ T (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_SKIPS : ‹α(DF_SKIPS A R) = A›
proof (intro subset_antisym subsetI)
  fix a assume ‹a ∈ A›
  hence ‹[ev a] ∈ T (DF_SKIPS A R)›
    by (subst DF_{SKIPS_unfold}) (auto simp add: T_Ndet T_Mndetprefix write0_def T_Mprefix)
  thus ‹a ∈ α(DF_SKIPS A R)› by (force simp add: events_of_def)
next
  fix a assume ‹a ∈ α(DF_SKIPS A R)›
  then obtain t where ‹ev a ∈ set t› ‹t ∈ T (DF_SKIPS A R)›
    by (auto simp add: events_of_def)
  thus ‹a ∈ A›
    by (induct t, simp, subst (asm) DF_{SKIPS_unfold})
      (auto simp add: T_Ndet T_SKIPS T_Mndetprefix write0_def T_Mprefix split: if_split_asm)
qed

lemma ticks_DF_SKIPS : ‹🚫s(DF_SKIPS A R) = R›
proof (intro subset_antisym subsetI)
  fix r assume ‹r ∈ R›
  hence ‹[🚫(r)] ∈ T (DF_SKIPS A R)› by (subst DF_{SKIPS_unfold}) (simp add: T_Ndet T_SKIPS)
  thus ‹r ∈ 🚫s(DF_SKIPS A R)›
    unfolding ticks_of_def by (metis (no_types, lifting) CollectI append_self_conv2)
next
  fix r assume ‹r ∈ 🚫s(DF_SKIPS A R)›
  then obtain s where ‹s @ [🚫(r)] ∈ T (DF_SKIPS A R)› unfolding ticks_of_def by blast
  thus ‹r ∈ R›
    by (induct s; subst (asm) DF_{SKIPS_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] ∈ T (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_ptick)›
  then obtain t :: ‹('a, 'r) trace_ptick› where ‹ev a ∈ set t› ‹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)] ∈ T (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] ∈ T (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_ptick)›
  then obtain t :: ‹('a, 'r) trace_ptick› where ‹ev a ∈ set t› ‹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)] ∈ T (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_SKIPS : ‹α(CHAOS_SKIPS A R) = A›
proof (intro subset_antisym subsetI)
  fix a assume ‹a ∈ A›
  hence ‹[ev a] ∈ T (CHAOS_SKIPS A R)›
    by (subst CHAOS_{SKIPS_unfold}) (auto simp add: T_Ndet T_Mprefix)
  thus ‹a ∈ α(CHAOS_SKIPS A R)› by (force simp add: events_of_def)
next
  fix a assume ‹a ∈ α(CHAOS_SKIPS A R)›
  then obtain t where ‹ev a ∈ set t› ‹t ∈ T (CHAOS_SKIPS A R)›
    by (auto simp add: events_of_def)
  thus ‹a ∈ A›
    by (induct t, simp, subst (asm) CHAOS_{SKIPS_unfold})
      (auto simp add: T_Ndet T_STOP T_SKIPS T_Mprefix)
qed

lemma ticks_CHAOS_SKIPS : ‹🚫s(CHAOS_SKIPS A R) = R›
proof (intro subset_antisym subsetI)
  fix r assume ‹r ∈ R›
  hence ‹[🚫(r)] ∈ T (CHAOS_SKIPS A R)› by (subst CHAOS_{SKIPS_unfold}) (simp add: T_Ndet T_SKIPS)
  thus ‹r ∈ 🚫s(CHAOS_SKIPS A R)› by (metis append_Nil ticks_of_memI)
next
  fix r assume ‹r ∈ 🚫s(CHAOS_SKIPS A R)›
  then obtain s where ‹s @ [🚫(r)] ∈ T (CHAOS_SKIPS A R)› unfolding ticks_of_def by blast
  thus ‹r ∈ R›
    by (induct s; subst (asm) CHAOS_{SKIPS_unfold})
      (auto simp add: T_Ndet T_STOP T_SKIPS T_Mprefix)
qed


lemma RUN_subset_DT: ‹RUN B ⊑_DT RUN A›
  if ‹A ⊆ B› for A B :: ‹'a set›
proof (subst RUN_def, induct rule: fix_ind)
  show ‹adm (λa. a ⊑_DT RUN A)› by simp
next
  show ‹⊥ ⊑_DT RUN A› by simp
next
  show ‹X ⊑_DT RUN A ==> (Λ X. ◻b∈B → X)⋅X ⊑_DT RUN A› for X :: ‹('a, 'r) process_ptick›
    by (subst RUN_unfold, simp)
      (meson Mprefix_DT_subset mono_Mprefix_DT ‹A ⊆ B› trans_DT)
qed


lemma CHAOS_subset_FD : ‹CHAOS B ⊑_FD CHAOS A›
  if ‹A ⊆ B› for A B :: ‹'a set›
proof (subst CHAOS_def, induct rule: fix_ind)
  show ‹adm (λa. a ⊑_FD CHAOS A)› by simp
next
  show ‹⊥ ⊑_FD CHAOS A› by simp
next
  from ‹A ⊆ B› show ‹X ⊑_FD CHAOS A ==> (Λ X. STOP ⊓ (◻b∈B → X))⋅X ⊑_FD CHAOS A›
    for X :: ‹('a, 'r) process_ptick›
    by (subst CHAOS_unfold)
      (auto simp add: refine_defs Mprefix_projs Ndet_projs F_STOP D_STOP)
qed


lemma CHAOS_{SKIPS_subset_FD} : ‹CHAOS_SKIPS B S ⊑_FD CHAOS_SKIPS A R›
  if ‹A ⊆ B› ‹R ≠ {}› ‹R ⊆ S›
proof (subst CHAOS_{SKIPS_def}, induct rule: fix_ind)
  show ‹adm (λa. a ⊑_FD CHAOS_SKIPS A R)› by simp
next
  show ‹⊥ ⊑_FD CHAOS_SKIPS A R› by simp
next
  from ‹A ⊆ B› ‹R ≠ {}› ‹R ⊆ S›
  show ‹X ⊑_FD CHAOS_SKIPS A R ==> (Λ X. SKIPS S ⊓ STOP ⊓ (◻a∈B → X))⋅X ⊑_FD CHAOS_SKIPS A R› for X
    by (subst CHAOS_{SKIPS_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) ∈ F (CHAOS A)›
proof (induct s)
  show ‹([], X) ∈ F (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) ∈ F (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) ∈ F (CHAOS A)› by (fact hyp)
  with prems show ‹(e # s, X) ∈ F (CHAOS A)›
    by (subst CHAOS_unfold, cases e) (auto simp add: F_Ndet F_Mprefix)
qed



lemma CHAOS_{SKIPS_superset_events_of_ticks_of_leF} : 
  ‹CHAOS_SKIPS A R ⊑_F P› if ‹α(P) ⊆ A› and ‹🚫s(P) ⊆ R›
proof (unfold failure_refine_def)
  have ‹ftF s ==> set s ⊆ (∪t∈T P. set t) ==> (s, X) ∈ F (CHAOS_SKIPS A R)› for s X
  proof (induct s)
    show ‹([], X) ∈ F (CHAOS_SKIPS A R)›
      by (subst CHAOS_{SKIPS_unfold}) (simp add: F_Ndet F_STOP)
  next
    fix e s
    assume prems : ‹ftF (e # s)› ‹set (e # s) ⊆ ∪ (set ` T P)›
    assume   hyp : ‹ftF s ==> set s ⊆ ∪ (set ` T P) ==> (s, X) ∈ F (CHAOS_SKIPS A R)›
    show ‹(e # s, X) ∈ F (CHAOS_SKIPS 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 ` T P)›
        by auto (metis front_tickFree_Cons_iff front_tickFree_Nil)
      hence ‹(s, X) ∈ F (CHAOS_SKIPS A R)› by (fact hyp)
      thus ‹(e # s, X) ∈ F (CHAOS_SKIPS A R)›
        by (subst CHAOS_{SKIPS_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) ∈ F (CHAOS_SKIPS A R)›
        by (subst CHAOS_{SKIPS_unfold}) (auto simp add: F_Ndet F_SKIPS ‹e = 🚫(r)›)
    qed
  qed
  thus ‹F P ⊆ F (CHAOS_SKIPS A R)› by (meson F_T F_imp_front_tickFree SUP_upper subrelI)
qed


corollary CHAOS_{SKIPS_events_of_ticks_of_leF}: ‹CHAOS_SKIPS α(P) 🚫s(P) ⊑_F P›
  and CHAOS_{SKIPS_UNIV_UNIV_leF}: ‹CHAOS_SKIPS UNIV UNIV ⊑_F P›
  by (simp_all add: CHAOS_{SKIPS_superset_events_of_ticks_of_leF})


lemma DF_{SKIPS_F_DF} : ‹DF_SKIPS A R ⊑_F DF A›
  by (simp add: DF_{SKIPS_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_ptick›
    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) ∈ F (DF A) ==> tF s› for s :: ‹('a, 'r) trace_ptick› and X
    by (metis F_T no_ticks_imp_tickFree_T ticks_DF)
next
  show ‹(s, X) ∈ F (DF A) ==> {a. ev a ∈ set s} ⊆ A› for s :: ‹('a, 'r) trace_ptick› and X
    by (drule F_T) (use events_of_DF[of A] in ‹auto simp add: events_of_def›)
qed

corollary CHAOS_{SKIPS_F_CHAOS} : ‹CHAOS_SKIPS A R ⊑_F CHAOS A›
  and CHAOS_{SKIPS_F_DFSKIPS} : ‹CHAOS_SKIPS A R ⊑_F DF_SKIPS A R›
  by (rule CHAOS_{SKIPS_superset_events_of_ticks_of_leF};
      simp add: events_of_CHAOS ticks_CHAOS events_of_DF_SKIPS ticks_DF_SKIPS)+




lemma div_free_CHAOS_SKIPS: ‹D (CHAOS_SKIPS A R) = {}›
proof (rule equals0I)
  show ‹s ∈ D (CHAOS_SKIPS A R) ==> False› for s
    by (induct s; subst (asm) CHAOS_{SKIPS_unfold})
      (auto simp add: D_Ndet D_STOP D_SKIPS D_Mprefix)
qed


lemma div_free_CHAOS: ‹D (CHAOS A) = {}›
proof (rule equals0I)
  show ‹s ∈ D (CHAOS A) ==> False› for s :: ‹('a, 'r) trace_ptick›
    by (induct s; subst (asm) CHAOS_unfold)
      (auto simp add: D_Ndet D_STOP D_Mprefix)
qed


lemma div_free_RUN: ‹D (RUN A) = {}›
proof (rule equals0I)
  show ‹s ∈ D (RUN A) ==> False› for s :: ‹('a, 'r) trace_ptick›
    by (induct s; subst (asm) RUN_unfold) (auto simp add: D_Mprefix)
qed

(* DF\<^sub>S\<^sub>K\<^sub>I\<^sub>P\<^sub>S_FD_DF : "DF\<^sub>S\<^sub>K\<^sub>I\<^sub>P\<^sub>S A R \<sqsubseteq>\<^sub>F\<^sub>D DF A" *)

corollary DF_FD_RUN : ‹DF A ⊑_FD RUN A›
  and CHAOS_FD_DF : ‹CHAOS A ⊑_FD DF A›
  and CHAOS_{SKIPS_FD_CHAOS} : ‹CHAOS_SKIPS A R ⊑_FD CHAOS A›
  and CHAOS_{SKIPS_FD_DFSKIPS} : ‹CHAOS_SKIPS A R ⊑_FD DF_SKIPS A R›
  by (simp_all add: DF_F_RUN div_free_RUN CHAOS_F_DF div_free_DF CHAOS_{SKIPS_F_CHAOS} div_free_CHAOS
      CHAOS_{SKIPS_F_DFSKIPS} div_free_DF_SKIPS divergence_refine_def leF_leD_imp_leFD)



lemma traces_CHAOS_subset : ‹T (CHAOS A) ⊆ {s. set s ⊆ ev ` A}›
proof (rule subsetI)
  show ‹s ∈ T (CHAOS A) ==> s ∈ {s. set s ⊆ ev ` A}› for s :: ‹('a, 'r) trace_ptick›
    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} ⊆ T (RUN A)›
proof (rule subsetI)
  show ‹s ∈ {s. set s ⊆ ev ` A} ==> s ∈ T (RUN A)› for s :: ‹('a, 'r) trace_ptick›
    by (induct s, simp) (subst RUN_unfold, auto simp add: T_Mprefix)
qed

corollary RUN_all_tickfree_traces1   : ‹T (RUN A) = {s. set s ⊆ ev ` A}›
  and     DF_all_tickfree_traces1    : ‹T (DF A) = {s. set s ⊆ ev ` A}›
  and     CHAOS_all_tickfree_traces1 : ‹T (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 ∈ T (RUN UNIV)›
  and     DF_all_tickfree_traces2   : ‹s ∈ T (DF UNIV)›
  and     CHAOS_all_tickfree_trace2 : ‹s ∈ T (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_ptick.exhaust)+


lemma traces_CHAOS_{SKIPS_subset} :
  ‹T (CHAOS_SKIPS A R) ⊆ {s. ftF s ∧ set s ⊆ ev ` A ∪ tick ` R}›
proof (rule subsetI)
  show ‹s ∈ T (CHAOS_SKIPS A R) ==> s ∈ {s. ftF s ∧ set s ⊆ ev ` A ∪ tick ` R}› for s
    by (induct s; subst (asm) CHAOS_{SKIPS_unfold})
      (auto simp add: T_Ndet T_STOP T_SKIPS T_Mprefix front_tickFree_Cons_iff)
qed


lemma traces_DF_{SKIPS_superset} : 
  ‹{s. ftF s ∧ set s ⊆ ev ` A ∪ tick ` R} ⊆ T (DF_SKIPS A R)›
proof (rule subsetI)
  show ‹s ∈ {s. ftF s ∧ set s ⊆ ev ` A ∪ tick ` R} ==> s ∈ T (DF_SKIPS A R) › for s
    by (induct s; subst DF_{SKIPS_unfold})
      (auto simp add: T_Ndet T_SKIPS T_Mndetprefix write0_def T_Mprefix front_tickFree_Cons_iff)
qed



corollary DF_{SKIPS_all_front_tickfree_traces1}: 
  ‹T (DF_SKIPS A R) = {s. ftF s ∧ set s ⊆ ev ` A ∪ tick ` R}›
  and CHAOS_{SKIPS_all_front_tickfree_traces1}: 
  ‹T (CHAOS_SKIPS A R) = {s. ftF s ∧ set s ⊆ ev ` A ∪ tick ` R}›
  using CHAOS_{SKIPS_F_DFSKIPS}[THEN leF_imp_leT, simplified trace_refine_def]
    traces_CHAOS_{SKIPS_subset} traces_DF_{SKIPS_superset} by blast+


corollary DF_{SKIPS_all_front_tickfree_traces2}   : ‹s ∈ T (DF_SKIPS UNIV UNIV)›
  and CHAOS_{SKIPS_all_front_tickfree_traces2}: ‹s ∈ T (CHAOS_SKIPS UNIV UNIV)›
  if ‹ftF s›
  using ‹ftF s›
  by (simp add: tickFree_def DF_{SKIPS_all_front_tickfree_traces1} CHAOS_{SKIPS_all_front_tickfree_traces1};
      metis UnCI event_ptick.exhaust rangeI subsetI)+


corollary DF_{SKIPS_UNIV_UNIV_leT} :    ‹DF_SKIPS UNIV UNIV ⊑_T P›
  and  CHAOS_{SKIPS_UNIV_UNIV_leT} : ‹CHAOS_SKIPS UNIV UNIV ⊑_T P›
  by (simp add:trace_refine_def DF_{SKIPS_all_front_tickfree_traces2} is_processT2_TR subsetI) 
    (simp add:trace_refine_def CHAOS_{SKIPS_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 ∈ T P›
proof -
  from ‹deadlock_free P› have ‹T P ⊆ T (DF UNIV)›
    by (simp add: deadlock_free_def le_ref2T)
  with ‹s ∈ T P› show ‹tF s›
    by (meson no_ticks_imp_tickFree_T subsetD ticks_DF)
qed



lemma deadlock_free_{SKIPS_is_right}: 
  ‹deadlock_free_SKIPS (P :: ('a, 'r) process_ptick) ⟷
 (∀s∈T P. tF s ⟶ (s, UNIV :: ('a, 'r) event_ptick set) ∉ F P)›
proof (intro iffI ballI impI)
  have ‹tF s ==> (s, UNIV) ∉ F (DF_SKIPS UNIV UNIV)› for s :: ‹('a, 'r) event_ptick list›
    by (induct s; subst DF_{SKIPS_unfold})
      (auto simp add: F_Ndet F_SKIPS F_Mndetprefix write0_def F_Mprefix)
  thus ‹deadlock_free_SKIPS P ==> s ∈ T P ==> tF s ==> (s, UNIV) ∉ F P› for s
    using deadlock_free_{SKIPS_def} failure_refine_def by blast
next
  assume as1 : ‹∀s∈T P. tF s ⟶ (s, UNIV) ∉ F P›
  have as2 : ‹ftF s ==> (∃a ∈ UNIV. ev a ∉ X) ==>
 (s, X) ∈ F (DF_SKIPS UNIV UNIV)› for s :: ‹('a, 'r) trace_ptick› and X
  proof(induct s)
    case Nil
    then show ?case
      by (subst DF_{SKIPS_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_{SKIPS_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) ∈ F (⊔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) ∈ F (Y i)" for i 
        using F_LUB[OF cc] limproc_is_thelub[OF cc] by simp
      from Y_def have e:"F(Mndetprefix UNIV (λx. Y i) ⊓ SKIPS UNIV) ⊆ F (Y (Suc i))" for i by(simp)
      from a have f:"tls ≠ [] ==> hds ∉ range tick" "ftF tls"
        by (metis event_ptick.disc(2) front_tickFree_Cons_iff imageE)
          (metis a front_tickFree_Cons_iff front_tickFree_Nil)
      have g:"(hds#tls, X) ∈ F (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_ptick.exhaust)+
      have h:"(hds#tls, X) ∈ F (Y 0)"
        using D_F cc g po_class.chainE proc_ord2a by blast
      from a b c show "(hds#tls, X) ∈ F (⊔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_SKIPS P"
  proof(unfold deadlock_free_{SKIPS_def} failure_refine_def, safe)
    fix s X
    assume as3:"(s, X) ∈ F P"
    hence a1:"s ∈ T P" "ftF s" 
      using F_T as3 is_processT2 by blast+
    show "(s, X) ∈ F (DF_SKIPS UNIV UNIV)" 
    proof(cases "tF s")
      case FT_True:True
      hence a2:"(s, UNIV) ∉ F P"
        using a1 as1 by blast
      then show ?thesis 
        by (metis DF_{SKIPS_all_front_tickfree_traces2} FT_True UNIV_I UNIV_eq_I a1(2) as2 as3
            event_ptick.exhaust is_processT6_TR_notin tickFree_imp_front_tickFree_snoc)
    next
      case FT_False: False                                                                 
      then show ?thesis 
        by (metis DF_{SKIPS_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_{SKIPS_implies_div_free}: ‹deadlock_free_SKIPS P ==> D P = {}›
  by (metis D_T D_imp_front_tickFree T_nonTickFree_imp_decomp all_not_in_conv butlast_snoc
      deadlock_free_{SKIPS_is_right} front_tickFree_iff_tickFree_butlast is_processT8 is_processT9)

corollary deadlock_free_{SKIPS_FD}: ‹deadlock_free_SKIPS P ⟷ DF_SKIPS UNIV UNIV ⊑_FD P›
  by (metis deadlock_free_{SKIPS_def} deadlock_free_{SKIPS_implies_div_free}
      less_eq_process_{ptick_def} order_refl refine_defs(3))

lemma all_events_ticks_refusal: 
  ‹(s, tick ` 🚫s(P) ∪ ev ` α(P)) ∈ F P ==> (s, UNIV) ∈ F P›
proof (rule ccontr)
  assume ‹(s, tick ` 🚫s(P) ∪ ev ` α(P)) ∈ F P› and ‹(s, UNIV) ∉ F P›
  then obtain c where ‹c ∉ tick ` 🚫s(P) ∪ ev ` α(P) ∧ s @ [c] ∈ T 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_{SKIPS_is_right_wrt_events}:
  ‹deadlock_free_SKIPS P ⟷
 (∀s∈T P. tF s ⟶ (s, tick ` 🚫s(P) ∪ ev ` α(P)) ∉ F P)›
  unfolding deadlock_free_{SKIPS_is_right} using all_events_ticks_refusal is_processT4 by blast


lemma deadlock_free_imp_deadlock_free_SKIPS: ‹deadlock_free P ==> deadlock_free_SKIPS P›
  using DF_{SKIPS_FD_DF} deadlock_free_{SKIPS_FD} deadlock_free_def trans_FD by blast




section ‹const‹deadlock_free› and ‹deadlock_free_SKIPS› with const‹SKIP› and const‹STOP››

lemma non_deadlock_free_{SKIPS_STOP}: ‹¬ deadlock_free_SKIPS STOP›
  by (unfold deadlock_free_{SKIPS_def}, subst DF_{SKIPS_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_SKIPS non_deadlock_free_{SKIPS_STOP} by blast


lemma deadlock_free_{SKIPS_SKIPS} : ‹deadlock_free_SKIPS (SKIPS R) ⟷ R ≠ {}›
proof (rule iffI)
  show ‹deadlock_free_SKIPS (SKIPS R) ==> R ≠ {}›
    by (rule ccontr, simp add: SKIPS_def)
      (use non_deadlock_free_{SKIPS_STOP} in blast)
next
  show ‹R ≠ {} ==> deadlock_free_SKIPS (SKIPS R)›
    by (unfold deadlock_free_{SKIPS_def}, subst DF_{SKIPS_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_{SKIPS_SKIP}: ‹deadlock_free_SKIPS (SKIP r)›
  by (metis SKIPS_singl_is_SKIP deadlock_free_{SKIPS_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)] ∈ T (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∈T 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 ==> D 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 ⊑_FD P›
  by (metis failure_refine_def less_eq_process_{ptick_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_SKIPS UNIV UNIV ⊑_D P ⟷ D P = {}›
  ‹CHAOS UNIV ⊑_D P ⟷ D P = {}›
  ‹RUN UNIV ⊑_D P ⟷ D P = {}›
  ‹DF_SKIPS UNIV UNIV ⊑_D P ⟷ D P = {}›
  ‹DF UNIV ⊑_D P ⟷ D P = {}›
  by (simp_all add: div_free_CHAOS div_free_RUN div_free_DF div_free_DF_SKIPS
      div_free_CHAOS_SKIPS divergence_refine_def)



lemma lifelock_free_{SKIPS_iff_div_free} : ‹lifelock_free_SKIPS P ⟷ D P = {}›
  by (simp add: CHAOS_{SKIPS_UNIV_UNIV_leF} divergence_refine_div_free(1)
      failure_divergence_refine_def lifelock_free_{SKIPS_def})

lemma lifelock_free_imp_lifelock_free_SKIPS : ‹lifelock_free P ==> lifelock_free_SKIPS P›
  by (simp add: lifelock_free_{SKIPS_iff_div_free} lifelock_free_is_non_terminating
      nonterminating_implies_div_free)

corollary deadlock_free_{SKIPS_imp_lifelock_freeSKIPS}: ‹deadlock_free_SKIPS P ==> lifelock_free_SKIPS P›
  by (simp add: deadlock_free_{SKIPS_implies_div_free} lifelock_free_{SKIPS_iff_div_free})



lemma non_terminating_Seq : ‹P ; Q = P› if ‹non_terminating P›
proof -
  from ‹non_terminating P› have * : ‹s ∈ T P ==> tF s› for s
    unfolding non_terminating_is_right ..
  show ‹P ; Q = P›
  proof (subst Process_eq_spec_optimized, safe)
    from "*" show ‹s ∈ D (P ; Q) ==> s ∈ D P› for s by (force simp add: D_Seq)
  next
    show ‹s ∈ D P ==> s ∈ D (P ; Q)› for s by (simp add: D_Seq)
  next
    show ‹(s, X) ∈ F (P ; Q) ==> (s, X) ∈ F 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) ∈ F P ==> (s, X) ∈ F (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_SKIPS Q ==> non_terminating (P [A] Q)›
  by (simp add: lifelock_free_{SKIPS_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
  (*>*)