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. (⊓xa∈A →  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 ∈ 𝒯 (⊓z∈A →  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 ∈ 𝒯 ((⊓z∈A →  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 ∈ 𝒯 (□z∈A →  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:"((⊓xa∈A →  x) ⊓ SKIP) = (SKIP ⊓ SKIP ⊓ (⊓xa∈A →  x))" 
      by (simp add: Ndet_commute Ndet_id)
    from 1 have b:"(SKIP ⊓ SKIP ⊓ (⊓xa∈A →  x)) ⊑D (SKIP ⊓ STOP ⊓ (□xa∈A → CHAOSSKIP A))"
      by (meson Mprefix_refines_Mndetprefix_D idem_D leD_STOP mono_Mprefix_D mono_Ndet_D trans_D)
    from a b show "((⊓xa∈A →  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 ⟹ ∃aa∈UNIV. 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 ‹const‹deadlock_free› and const‹deadlock_free_v2› with const‹SKIP› and const‹STOP››

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