Theory Assertions

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

theory Assertions
  imports CSP
begin



default_sort "type"

section‹CSP Assertions›

definition DF :: "'a set  'a process"
  where   "DF A  μ X.  x  A  X"

lemma DF_unfold : "DF A = ( z  A  DF A)"
 by(simp add: DF_def, rule trans, rule fix_eq, simp)

definition deadlock_free :: "'a process  bool"
  where   "deadlock_free P  DF UNIV FD P"

definition DFSKIP :: "'a set  'a process"
  where   "DFSKIP A  μ X. (( x  A  X)  SKIP)"

(* TO DO: rename this in deadlock_freeSKIP *)
definition deadlock_free_v2 :: "'a process  bool"
  where   "deadlock_free_v2 P  DFSKIP UNIV F P"


section‹Some deadlock freeness laws›

lemma DF_subset: "A  {}  A  B  DF B FD DF A" 
  apply(subst DF_def, rule fix_ind) 
  apply(rule le_FD_adm, simp_all add: monofunI, subst DF_unfold)
  by (meson mono_Mndetprefix_FD mono_Mndetprefix_FD_set trans_FD)

lemma DF_Univ_freeness: "A  {}  (DF A) FD P   deadlock_free P"
  by (meson deadlock_free_def DF_subset failure_divergence_refine_def order.trans subset_UNIV)

lemma deadlock_free_Ndet: "deadlock_free P  deadlock_free Q  deadlock_free (P  Q)"
  by (simp add: D_Ndet F_Ndet deadlock_free_def failure_divergence_refine_def le_ref_def)



section ‹Preliminaries›

lemma DFSKIP_unfold : "DFSKIP A = (( z  A  DFSKIP A)  SKIP)"
  by(simp add: DFSKIP_def, rule trans, rule fix_eq, simp)


section ‹Deadlock Free›

lemma div_free_DFSKIP: "𝒟(DFSKIP A) = {}"
proof(simp add:DFSKIP_def fix_def) 
  define Y where "Y  λi. iterate i(Λ x. (xaA   x)  SKIP)"
  hence a:"chain Y" by simp
  have "𝒟 (Y (Suc i)) = {d. d  []  hd d   (ev ` A)  tl d  𝒟(Y i)}" for i
    by (cases "A={}", auto simp add:Y_def D_STOP D_SKIP D_Mndetprefix write0_def D_Mprefix D_Ndet) 
  hence b:"d  𝒟(Y i)  length d  i" for d i
    by (induct i arbitrary:d, simp_all add: Nitpick.size_list_simp(2))
  { fix x
    assume c:" i. x  𝒟 (Y i)"
    from b have "x  𝒟 (Y (Suc (length x)))" using Suc_n_not_le_n by blast
    with c have False by simp
  }
  with a show "𝒟 (i. Y i) = {}"
  using D_LUB[OF a] limproc_is_thelub[OF a] by auto
qed

lemma div_free_DF: "𝒟(DF A) = {}"
proof - 
  have "DFSKIP A  D DF A"
    apply (simp add:DFSKIP_def)
    by(rule fix_ind, simp_all add: monofunI, subst DF_unfold, simp)
  then show ?thesis using divergence_refine_def div_free_DFSKIP by blast 
qed

lemma deadlock_free_implies_div_free: "deadlock_free P  𝒟 P = {}"
  by (simp add: deadlock_free_def div_free_DF failure_divergence_refine_def le_ref_def)




section ‹Run›

definition RUN :: "'a set  'a process"
  where   "RUN A  μ X.  x  A  X"

definition CHAOS :: "'a set  'a process" 
  where   "CHAOS A  μ X. (STOP  ( x  A  X))"

definition lifelock_free :: "'a process  bool"
  where   "lifelock_free P  CHAOS UNIV FD P"




section ‹Reference processes and their unfolding rules›


definition CHAOSSKIP :: "'a set  'a process" 
  where   "CHAOSSKIP A  μ X. (SKIP  STOP  ( x  A  X))"


lemma RUN_unfold : "RUN A = ( z  A  RUN A)"
  by(simp add: RUN_def, rule trans, rule fix_eq, simp)

lemma CHAOS_unfold : "CHAOS A = (STOP  ( z  A  CHAOS A))"
  by(simp add: CHAOS_def, rule trans, rule fix_eq, simp)
                                              
lemma CHAOSSKIP_unfold: "CHAOSSKIP A  SKIP  STOP  ( x  A  CHAOSSKIP A)"
  unfolding CHAOSSKIP_def using fix_eq[of "Λ X. (SKIP  STOP  ( x  A  X))"] by simp

section ‹Process events and reference processes events›

definition events_of where "events_of P  (t𝒯 P. {a. ev a  set t})"

lemma events_DF: "events_of (DF A) = A"
proof(auto simp add:events_of_def)
  fix x t
  show "t  𝒯 (DF A)  ev x  set t  x  A"
  proof(induct t)
    case Nil
    then show ?case by simp
  next
    case (Cons a t)
    from Cons(2) have "a # t  𝒯 (zA   DF A)" using DF_unfold by metis
    then obtain aa where "a = ev aa  aa  A  t  𝒯 (DF A)" 
      by (cases "A={}", auto simp add: T_Mndetprefix write0_def T_Mprefix T_STOP)
    with Cons show ?case by auto
  qed
next
  fix x
  show "x  A  xa𝒯 (DF A). ev x  set xa"
    apply(subst DF_unfold, cases "A={}", auto simp add:T_Mndetprefix write0_def T_Mprefix)
    by (metis Nil_elem_T list.sel(1) list.sel(3) list.set_intros(1))
qed

lemma events_DFSKIP: "events_of (DFSKIP A) = A"
proof(auto simp add:events_of_def)
  fix x t
  show "t  𝒯 (DFSKIP A)  ev x  set t  x  A"
  proof(induct t)
    case Nil
    then show ?case by simp
  next
    case (Cons a t)
    from Cons(2) have "a # t  𝒯 ((zA   DFSKIP A)  SKIP)" using DFSKIP_unfold by metis
    with Cons obtain aa where "a = ev aa  aa  A  t  𝒯 (DFSKIP A)" 
      by (cases "A={}", auto simp add:T_Mndetprefix write0_def T_Mprefix T_STOP T_SKIP T_Ndet)  
    with Cons show ?case by auto
  qed
next
  fix x
  show "x  A  xa𝒯 (DFSKIP A). ev x  set xa"
    apply(subst DFSKIP_unfold, cases "A={}")
     apply(auto simp add:T_Mndetprefix write0_def T_Mprefix T_SKIP T_Ndet)
    by (metis Nil_elem_T list.sel(1) list.sel(3) list.set_intros(1))
qed

lemma events_RUN: "events_of (RUN A) = A"
proof(auto simp add:events_of_def)
  fix x t
  show "t  𝒯 (RUN A)  ev x  set t  x  A"
  proof(induct t)
    case Nil
    then show ?case by simp
  next
    case (Cons a t)
    from Cons(2) have "a # t  𝒯 (zA   RUN A)" using RUN_unfold by metis
    then obtain aa where "a = ev aa  aa  A  t  𝒯 (RUN A)" by (auto simp add:T_Mprefix)
    with Cons show ?case by auto
  qed
next
  fix x
  show "x  A  xa  𝒯(RUN A). ev x  set xa"
    apply(subst RUN_unfold, simp add: T_Mprefix)
    by (metis Nil_elem_T list.sel(1) list.sel(3) list.set_intros(1))
qed

lemma events_CHAOS: "events_of (CHAOS A) = A"
proof(auto simp add:events_of_def)
  fix x t
  show "t  𝒯 (CHAOS A)  ev x  set t  x  A"
  proof(induct t)
    case Nil
    then show ?case by simp
  next
    case (Cons a t)
    from Cons(2) have "a # t  𝒯 (STOP  ( z  A  CHAOS A))" using CHAOS_unfold by metis
    then obtain aa where "a = ev aa  aa  A  t  𝒯 (CHAOS A)" 
      by (auto simp add:T_Ndet T_Mprefix T_STOP)
    with Cons show ?case by auto
  qed
next
  fix x
  show "x  A  xa𝒯 (CHAOS A). ev x  set xa"
    apply(subst CHAOS_unfold, simp add:T_Ndet T_Mprefix T_STOP)
    by (metis Nil_elem_T list.sel(1) list.sel(3) list.set_intros(1))
qed

lemma events_CHAOSSKIP: "events_of (CHAOSSKIP A) = A"
proof(auto simp add:events_of_def)
  fix x t
  show "t  𝒯 (CHAOSSKIP A)  ev x  set t  x  A"
  proof(induct t)
    case Nil
    then show ?case by simp
  next
    case (Cons a t)
    from Cons(2) have "a # t  𝒯 (SKIP  STOP  ( z  A  CHAOSSKIP A))" 
      using CHAOSSKIP_unfold by metis
    with Cons obtain aa where "a = ev aa  aa  A  t  𝒯 (CHAOSSKIP A)" 
      by (auto simp add:T_Ndet T_Mprefix T_STOP T_SKIP)
    with Cons show ?case by auto
  qed
next
  fix x
  show "x  A  xa𝒯 (CHAOSSKIP A). ev x  set xa"
    apply(subst CHAOSSKIP_unfold, simp add:T_Ndet T_Mprefix T_STOP T_SKIP)
    by (metis Nil_elem_T list.sel(1) list.sel(3) list.set_intros(1))
qed

lemma events_div: "𝒟(P)  {}   events_of (P) = UNIV"
proof(auto simp add:events_of_def)
  fix x xa
  assume 1: "x  𝒟 P"
  show "x𝒯 P. ev xa  set x"
  proof(cases "tickFree x")
    case True  
    hence "x@[ev xa]  𝒯 P"
      using 1 NT_ND front_tickFree_single is_processT7 by blast   
    then show ?thesis by force 
  next
    case False
    hence "(butlast x)@[ev xa]  𝒯 P"
      by (metis "1" D_T D_imp_front_tickFree append_single_T_imp_tickFree butlast_snoc 
                front_tickFree_single nonTickFree_n_frontTickFree process_charn) 
    then show ?thesis by force
  qed
qed



lemma DFSKIP_subset_FD: "A  {}  A  B  DFSKIP B FD DFSKIP A"
  apply(subst DFSKIP_def, rule fix_ind, rule le_FD_adm, simp_all add:monofunI, subst DFSKIP_unfold)
  by (rule mono_Ndet_FD, simp_all) (meson mono_Mndetprefix_FD mono_Mndetprefix_FD_set trans_FD) 

lemma RUN_subset_DT: "A  B  RUN B DT RUN A"
  apply(subst RUN_def, rule fix_ind, rule le_DT_adm, simp_all add:monofunI, subst RUN_unfold)
  by (meson mono_Mprefix_DT mono_Mprefix_DT_set trans_DT)

lemma CHAOS_subset_FD: "A  B  CHAOS B FD CHAOS A"
  apply(subst CHAOS_def, rule fix_ind, rule le_FD_adm, simp_all add:monofunI, subst CHAOS_unfold)
  by (auto simp add: failure_divergence_refine_def le_ref_def 
                     D_Mprefix D_Ndet F_STOP F_Mprefix F_Ndet) 

lemma CHAOSSKIP_subset_FD: "A  B  CHAOSSKIP B FD CHAOSSKIP A"
  apply(subst CHAOSSKIP_def, rule fix_ind, rule le_FD_adm) 
     apply(simp_all add:monofunI, subst CHAOSSKIP_unfold)
  by (auto simp add: failure_divergence_refine_def le_ref_def 
                     D_Mprefix D_Ndet F_STOP F_Mprefix F_Ndet)

section ‹Relations between refinements on reference processes›

lemma CHAOS_has_all_tickFree_failures: 
      "tickFree a  {x. ev x  set a}  A  (a,b)   (CHAOS A)"
proof(induct a)
  case Nil
  then show ?case 
    by (subst CHAOS_unfold, simp add:F_Ndet F_STOP)
next
  case (Cons a0 al)
  hence "tickFree al"
    by (metis append.left_neutral append_Cons front_tickFree_charn front_tickFree_mono)
  with Cons show ?case 
    apply (subst CHAOS_unfold, simp add:F_Ndet F_STOP F_Mprefix events_of_def)
    using event_set by blast
qed

lemma CHAOSSKIP_has_all_failures: 
  assumes as:"(events_of P)  A" 
  shows "CHAOSSKIP A F P"
proof -
  have "front_tickFree a  set a  (t𝒯 P. set t)  (a,b)   (CHAOSSKIP A)" for a b
  proof(induct a)
    case Nil
    then show ?case 
      by (subst CHAOSSKIP_unfold, simp add:F_Ndet F_STOP)
  next
    case (Cons a0 al)
    hence "front_tickFree al"
      by (metis append.left_neutral append_Cons front_tickFree_charn front_tickFree_mono)
    with Cons show ?case 
      apply (subst CHAOSSKIP_unfold, simp add:F_Ndet F_STOP F_SKIP F_Mprefix events_of_def as)
      apply(cases "a0=tick")
       apply (metis append.simps(2) front_tickFree_charn 
                    front_tickFree_mono list.distinct(1) tickFree_Cons)
      using event_set image_iff as[simplified events_of_def] by fastforce
  qed
  thus ?thesis 
    by (simp add: F_T SUP_upper failure_refine_def process_charn subrelI) 
qed

corollary CHAOSSKIP_has_all_failures_ev: "CHAOSSKIP (events_of P) F P" 
      and CHAOSSKIP_has_all_failures_Un: "CHAOSSKIP UNIV F P"
  by (simp_all add: CHAOSSKIP_has_all_failures)


lemma DFSKIP_DF_refine_F: "DFSKIP A  F DF A"
  by (simp add:DFSKIP_def, rule fix_ind, simp_all add: monofunI, subst DF_unfold, simp) 

lemma DF_RUN_refine_F: "DF A  F RUN A"
  apply (simp add:DF_def, rule fix_ind, simp_all add: monofunI, subst RUN_unfold)
  by (meson Mprefix_refines_Mndetprefix_F mono_Mndetprefix_F trans_F)

lemma CHAOS_DF_refine_F: "CHAOS A  F DF A"
  apply (simp add:CHAOS_def DF_def, rule parallel_fix_ind, simp_all add: monofunI)
   apply (rule le_F_adm, simp_all add: monofun_snd)
  by (cases "A={}", auto simp add:adm_def failure_refine_def F_Mndetprefix 
                                  F_Mprefix write0_def F_Ndet F_STOP)

corollary CHAOSSKIP_CHAOS_refine_F: "CHAOSSKIP A  F CHAOS A"
      and CHAOSSKIP_DFSKIP_refine_F: "CHAOSSKIP A  F DFSKIP A"
  by (simp_all add: CHAOSSKIP_has_all_failures events_CHAOS events_DFSKIP 
                    trans_F[OF CHAOS_DF_refine_F DF_RUN_refine_F])




lemma div_free_CHAOSSKIP: "𝒟 (CHAOSSKIP A) = {}"
proof -
  have "DFSKIP A  D CHAOSSKIP A"
  proof (simp add:DFSKIP_def, rule fix_ind, simp_all add: monofunI, subst CHAOSSKIP_unfold)
    fix x
    assume 1:"x D CHAOSSKIP A"
    have a:"((xaA   x)  SKIP) = (SKIP  SKIP  (xaA   x))" 
      by (simp add: Ndet_commute Ndet_id)
    from 1 have b:"(SKIP  SKIP  (xaA   x)) D (SKIP  STOP  (xaA  CHAOSSKIP A))"
      by (meson Mprefix_refines_Mndetprefix_D idem_D leD_STOP mono_Mprefix_D mono_Ndet_D trans_D)
    from a b show "((xaA   x) |-| SKIP) D (SKIP |-| STOP |-| Mprefix A (λx. CHAOSSKIP A))" 
      by simp
  qed
  then show ?thesis using divergence_refine_def div_free_DFSKIP by blast 
qed

lemma div_free_CHAOS: "𝒟(CHAOS A) = {}"
proof - 
  have "CHAOSSKIP A  D CHAOS A"
    apply (simp add:CHAOSSKIP_def, rule fix_ind)
    by (simp_all add: monofunI, subst CHAOS_unfold, simp) 
  then show ?thesis using divergence_refine_def div_free_CHAOSSKIP by blast 
qed

lemma div_free_RUN: "𝒟(RUN A) = {}"
proof - 
  have "CHAOS A  D RUN A"
    by (simp add:CHAOS_def, rule fix_ind, simp_all add: monofunI, subst RUN_unfold, simp) 
  then show ?thesis using divergence_refine_def div_free_CHAOS by blast 
qed

corollary DFSKIP_DF_refine_FD: "DFSKIP A  FD DF A"
      and DF_RUN_refine_FD: "DF A  FD RUN A"
      and CHAOS_DF_refine_FD: "CHAOS A  FD DF A"
      and CHAOSSKIP_CHAOS_refine_FD: "CHAOSSKIP A  FD CHAOS A"
      and CHAOSSKIP_DFSKIP_refine_FD: "CHAOSSKIP A  FD DFSKIP A"
  using div_free_DFSKIP[of A] div_free_CHAOSSKIP[of A] div_free_DF[of A] div_free_RUN[of A] 
        div_free_CHAOS[of A] 
        leF_leD_imp_leFD[OF DFSKIP_DF_refine_F, of A] leF_leD_imp_leFD[OF DF_RUN_refine_F, of A] 
        leF_leD_imp_leFD[OF CHAOS_DF_refine_F, of A] leF_leD_imp_leFD[OF CHAOSSKIP_CHAOS_refine_F, of A] 
        leF_leD_imp_leFD[OF CHAOSSKIP_DFSKIP_refine_F, of A]
  by (auto simp add:divergence_refine_def) 


lemma traces_CHAOS_sub: "𝒯(CHAOS A)  {s. set s  ev ` A}"
proof(auto)
  fix s sa
  assume "s  𝒯 (CHAOS A)" and "sa  set s"
  then show "sa  ev ` A"
    apply (induct s, simp) 
    by (subst (asm) (2) CHAOS_unfold, cases "A={}", auto simp add:T_Ndet T_STOP T_Mprefix)  
qed

lemma traces_RUN_sub: "{s. set s  ev ` A}  𝒯(RUN A)"
proof(auto)
  fix s
  assume "set s  ev ` A"
  then show "s  𝒯 (RUN A)"
    by (induct s, simp add: Nil_elem_T) (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_RUN_refine_F[THEN leF_imp_leT, simplified trace_refine_def]
        CHAOS_DF_refine_F[THEN leF_imp_leT,simplified trace_refine_def] 
        traces_CHAOS_sub traces_RUN_sub by blast+

corollary RUN_all_tickfree_traces2: "tickFree s  s  𝒯(RUN UNIV)" 
      and DF_all_tickfree_traces2: "tickFree s  s  𝒯(DF UNIV)" 
      and CHAOS_all_tickfree_trace2: "tickFree s  s  𝒯(CHAOS UNIV)"
    apply(simp_all add:tickFree_def RUN_all_tickfree_traces1 
                       DF_all_tickfree_traces1 CHAOS_all_tickfree_traces1)
  by (metis event_set insertE subsetI)+

lemma traces_CHAOSSKIP_sub: "𝒯(CHAOSSKIP A)  {s. front_tickFree s  set s  (ev ` A  {tick})}"
proof(auto simp add:is_processT2_TR)
  fix s sa
  assume "s  𝒯 (CHAOSSKIP A)" and "sa  set s" and "sa  ev ` A"
  then show "sa = tick"
    apply (induct s, simp) 
    by (subst (asm) (2) CHAOSSKIP_unfold, cases "A={}", auto simp add:T_Ndet T_STOP T_SKIP T_Mprefix)  
qed

lemma traces_DFSKIP_sub: 
  "{s. front_tickFree s  set s  (ev ` A  {tick})}  𝒯(DFSKIP A::'a process)"
proof(auto)
  fix s
  assume a:"front_tickFree s" and b:"set s  insert tick (ev ` A)"
  have c:"front_tickFree ((tick::'a event) # s)  s = []" for s
    by (metis butlast.simps(2) butlast_snoc front_tickFree_charn list.distinct(1) tickFree_Cons) 
  with a b show "s  𝒯 (DFSKIP A)"
    apply (induct s, simp add: Nil_elem_T, subst DFSKIP_unfold, cases "A={}") 
     apply (subst DFSKIP_unfold, cases "A={}")
      apply(auto simp add:T_Mprefix T_Mndetprefix write0_def T_SKIP T_Ndet T_STOP)
    apply (metis append_Cons append_Nil front_tickFree_charn front_tickFree_mono)
    by (metis append_Cons append_Nil front_tickFree_mono)
  qed

corollary DFSKIP_all_front_tickfree_traces1: 
                              "𝒯(DFSKIP A) = {s. front_tickFree s  set s  (ev ` A  {tick})}" 
      and CHAOSSKIP_all_front_tickfree_traces1: 
                              "𝒯(CHAOSSKIP A) = {s. front_tickFree s  set s  (ev ` A  {tick})}"
  using CHAOSSKIP_DFSKIP_refine_F[THEN leF_imp_leT, simplified trace_refine_def]
        traces_CHAOSSKIP_sub traces_DFSKIP_sub by blast+

corollary DFSKIP_all_front_tickfree_traces2: "front_tickFree s  s  𝒯(DFSKIP UNIV)" 
      and CHAOSSKIP_all_front_tickfree_traces2: "front_tickFree s  s  𝒯(CHAOSSKIP UNIV)"
   apply(simp_all add:tickFree_def DFSKIP_all_front_tickfree_traces1 
                      CHAOSSKIP_all_front_tickfree_traces1)
  by (metis event_set subsetI)+

corollary DFSKIP_has_all_traces: "DFSKIP UNIV T P"
      and CHAOSSKIP_has_all_traces: "CHAOSSKIP UNIV T P"
  apply (simp add:trace_refine_def DFSKIP_all_front_tickfree_traces2 is_processT2_TR subsetI) 
  by (simp add:trace_refine_def CHAOSSKIP_all_front_tickfree_traces2 is_processT2_TR subsetI) 



lemma deadlock_free_implies_non_terminating: 
  "deadlock_free (P::'a process)  s𝒯 P. tickFree s"
  unfolding deadlock_free_def apply(drule leFD_imp_leF, drule leF_imp_leT) unfolding trace_refine_def 
  using DF_all_tickfree_traces1[of "(UNIV::'a set)"] tickFree_def by fastforce 

lemma deadlock_free_v2_is_right: 
  "deadlock_free_v2 (P::'a process)  (s𝒯 P. tickFree s  (s, UNIV::'a event set)   P)"
proof
  assume a:"deadlock_free_v2 P"
  have "tickFree s  (s, UNIV)   (DFSKIP UNIV)" for s::"'a event list"
  proof(induct s)
    case Nil
    then show ?case by (subst DFSKIP_unfold, simp add:F_Mndetprefix write0_def F_Mprefix F_Ndet F_SKIP)
  next
    case (Cons a s)
    then show ?case 
      by (subst DFSKIP_unfold, simp add:F_Mndetprefix write0_def F_Mprefix F_Ndet F_SKIP)
  qed
  with a show "s𝒯 P. tickFree s  (s, UNIV)   P"
    using deadlock_free_v2_def failure_refine_def by blast
next 
  assume as1:"s𝒯 P. tickFree s  (s, UNIV)   P"
  have as2:"front_tickFree s  (aa  UNIV. ev aa  b)  (s, b)   (DFSKIP (UNIV::'a set))" 
       for s b
  proof(induct s)
    case Nil
    then show ?case
      by (subst DFSKIP_unfold, auto simp add:F_Mndetprefix write0_def F_Mprefix F_Ndet F_SKIP)
  next
    case (Cons hda tla)
    then show ?case 
    proof(simp add:DFSKIP_def fix_def)
      define Y where "Y  λi. iterate i(Λ x. (xa(UNIV::'a set)   x)  SKIP)"
      assume a:"front_tickFree (hda # tla)" and b:"front_tickFree tla  (tla, b)   (i. Y i)"
             and c:"aa. ev aa  b"
      from Y_def have cc:"chain Y" by simp
      from b have d:"front_tickFree tla  aaUNIV. ev aa  b (tla, b)   (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)  SKIP)   (Y (Suc i))" for i by(simp)
      from a have f:"tla  []  hda  tick" "front_tickFree tla"
        apply (metis butlast.simps(2) butlast_snoc front_tickFree_charn 
                      list.distinct(1) tickFree_Cons)
        by (metis a append_Cons append_Nil front_tickFree_Nil front_tickFree_mono) 
      have g:"(hda#tla, b)   (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_SKIP) (metis event.exhaust)+ 
      have h:"(hda#tla, b)   (Y 0)"
        using NF_ND cc g po_class.chainE proc_ord2a by blast
      from a b c show "(hda#tla, b)   (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_v2 P"
  proof(auto simp add:deadlock_free_v2_def failure_refine_def)
    fix s b
    assume as3:"(s, b)   P"
    hence a1:"s  𝒯 P" "front_tickFree s" 
       using F_T apply blast
      using as3 is_processT2 by blast
    show "(s, b)   (DFSKIP UNIV)" 
    proof(cases "tickFree s")
      case FT_True:True
      hence a2:"(s, UNIV)   P"
        using a1 as1 by blast
      then show ?thesis 
        by (metis FT_True UNIV_I UNIV_eq_I a1(2) as2 as3 emptyE event.exhaust 
                  is_processT6_S1 tickFree_implies_front_tickFree_single) 
    next
      case FT_False: False                                                                 
      then show ?thesis 
        by (meson T_F_spec UNIV_witness a1(2) append_single_T_imp_tickFree 
                  as2 emptyE is_processT5_S7)
    qed 
  qed
qed  

lemma deadlock_free_v2_implies_div_free: "deadlock_free_v2 P  𝒟 P = {}"
  by (metis F_T append_single_T_imp_tickFree deadlock_free_v2_is_right ex_in_conv 
            nonTickFree_n_frontTickFree process_charn)

corollary deadlock_free_v2_FD: "deadlock_free_v2 P = DFSKIP UNIV FD P"
  unfolding deadlock_free_v2_def 
  using deadlock_free_v2_implies_div_free leFD_imp_leF leF_leD_imp_leFD 
        deadlock_free_v2_def divergence_refine_def 
  by fastforce 

lemma all_events_refusal: 
   "(s, {tick}  ev ` (events_of P))   P  (s, UNIV::'a event set)   P"
proof -
  assume a1:"(s, {tick}  ev ` events_of P)   P"
  { assume "(s, UNIV)   P"
    then obtain c where "c  {tick}  ev ` events_of P  s @ [c]  𝒯 P"
      using is_processT5_S1[of s "{tick}  ev ` events_of P" P 
            "UNIV - ({tick}  ev ` events_of P)", simplified] F_T a1 by auto
    hence False by (simp add:events_of_def, cases c) fastforce+
  }  
  with a1 show "(s, UNIV)   P" by blast 
qed

corollary deadlock_free_v2_is_right_wrt_events:
  "deadlock_free_v2 (P::'a process)  
      (s𝒯 P. tickFree s  (s, {tick}  ev ` (events_of P))   P)"
  unfolding deadlock_free_v2_is_right using all_events_refusal apply auto 
  using is_processT4 by blast 

lemma deadlock_free_is_deadlock_free_v2:
  "deadlock_free P  deadlock_free_v2 P"
  using DFSKIP_DF_refine_FD deadlock_free_def deadlock_free_v2_FD trans_FD by blast 



section constdeadlock_free and constdeadlock_free_v2 with constSKIP and constSTOP

lemma deadlock_free_v2_SKIP: "deadlock_free_v2 SKIP"
  unfolding deadlock_free_v2_FD by (subst DFSKIP_unfold) simp
 
lemma non_deadlock_free_SKIP: ¬ deadlock_free SKIP 
  by (metis T_SKIP deadlock_free_implies_non_terminating insertCI non_tickFree_tick)

lemma non_deadlock_free_v2_STOP: ¬ deadlock_free_v2 STOP
  by (simp add: F_STOP Nil_elem_T deadlock_free_v2_is_right)

lemma non_deadlock_free_STOP: ¬ deadlock_free STOP
  using deadlock_free_is_deadlock_free_v2 non_deadlock_free_v2_STOP by blast



section ‹Non-terminating Runs›

definition non_terminating  :: "'a process  bool"
  where   "non_terminating P  RUN UNIV T P"

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::'a process)  (s𝒯 P. tickFree s)"
  apply (rule iffI)
  by (auto simp add:non_terminating_def trace_refine_def tickFree_def RUN_all_tickfree_traces1)[1]
     (auto simp add:non_terminating_def trace_refine_def RUN_all_tickfree_traces2)

lemma nonterminating_implies_div_free: "non_terminating P  𝒟 P = {}"
  unfolding non_terminating_is_right
  by (metis NT_ND equals0I front_tickFree_charn process_charn tickFree_Cons tickFree_append) 

lemma non_terminating_implies_F: "non_terminating P  CHAOS UNIV F P"
  apply(auto simp add: non_terminating_is_right failure_refine_def)
  using CHAOS_has_all_tickFree_failures F_T by blast 

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"
  unfolding non_terminating_F
  using div_free_CHAOS nonterminating_implies_div_free leFD_imp_leF
        leF_leD_imp_leFD divergence_refine_def non_terminating_F 
  by fastforce 


section ‹Lifelock Freeness›

thm lifelock_free_def

corollary lifelock_free_is_non_terminating: "lifelock_free P = non_terminating P"
  unfolding lifelock_free_def non_terminating_FD by rule

lemma div_free_divergence_refine:
  "𝒟 P = {}  CHAOSSKIP UNIV D P" 
  "𝒟 P = {}  CHAOS UNIV    D P" 
  "𝒟 P = {}  RUN UNIV      D P" 
  "𝒟 P = {}  DFSKIP UNIV    D P" 
  "𝒟 P = {}  DF UNIV       D P" 
  by (simp_all add: div_free_CHAOSSKIP div_free_CHAOS div_free_RUN div_free_DF 
                    div_free_DFSKIP divergence_refine_def)

definition lifelock_free_v2 :: "'a process  bool"
  where   "lifelock_free_v2 P  CHAOSSKIP UNIV FD P"

lemma div_free_is_lifelock_free_v2: "lifelock_free_v2 P  𝒟 P = {}"
  using CHAOSSKIP_has_all_failures_Un leFD_imp_leD leF_leD_imp_leFD
        div_free_divergence_refine(1) lifelock_free_v2_def 
  by blast
  
lemma lifelock_free_is_lifelock_free_v2: "lifelock_free P  lifelock_free_v2 P"
  by (simp add: leFD_imp_leD div_free_divergence_refine(2) div_free_is_lifelock_free_v2 lifelock_free_def)

corollary deadlock_free_v2_is_lifelock_free_v2: "deadlock_free_v2 P  lifelock_free_v2 P"
  by (simp add: deadlock_free_v2_implies_div_free div_free_is_lifelock_free_v2)


section ‹New laws›

lemma non_terminating_Seq: 
  "non_terminating P  (P ; Q) = P"
  apply(auto simp add: non_terminating_is_right Process_eq_spec D_Seq F_Seq F_T is_processT7)
      using process_charn apply blast
    using process_charn apply blast
   using F_T is_processT5_S2a by fastforce

lemma non_terminating_Sync: 
  "non_terminating P  lifelock_free_v2 Q  non_terminating (P A Q)"
  apply(auto simp add: non_terminating_is_right div_free_is_lifelock_free_v2 T_Sync) 
  apply (metis equals0D ftf_Sync1 ftf_Sync21 insertI1 tickFree_def)
  apply (meson NT_ND is_processT7_S tickFree_append)
  by (metis D_T empty_iff ftf_Sync1 ftf_Sync21 insertI1 tickFree_def)

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




end