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) processptick›
  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 DFSKIPS :: ‹'a set ⇒ 'r set ⇒ ('a,'r) processptick›
  where ‹DFSKIPS A R ≡ μ X. (⊓a ∈ A → X) ⊓ SKIPS R›

lemma DFSKIPS_unfold : ‹DFSKIPS A R = (⊓a ∈ A → DFSKIPS A R) ⊓ SKIPS R›
  by (simp add: DFSKIPS_def, rule trans, rule fix_eq, simp)


definition RUN :: ‹'a set ⇒ ('a,'r) processptick›
  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) processptick› 
  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 CHAOSSKIPS :: ‹'a set ⇒ 'r set ⇒ ('a,'r) processptick›
  where ‹CHAOSSKIPS A R ≡ μ X. SKIPS R ⊓ STOP ⊓ (□a∈A → X)›

lemma CHAOSSKIPS_unfold: ‹CHAOSSKIPS A R = SKIPS R ⊓ STOP ⊓ (□a ∈ A → CHAOSSKIPS A R)›
  by (simp add: CHAOSSKIPS_def, rule trans, rule fix_eq, simp)



section ‹Assertions›

definition deadlock_free :: ‹('a,'r) processptick ⇒ bool›
  where ‹deadlock_free P ≡ DF UNIV ⊑FD P›


definition deadlock_freeSKIPS :: ‹('a, 'r) processptick ⇒ bool›
  where ‹deadlock_freeSKIPS P ≡ DFSKIPS UNIV UNIV ⊑F P›


definition lifelock_free :: ‹('a,'r) processptick ⇒ bool›
  where ‹lifelock_free P ≡ CHAOS UNIV ⊑FD P›


definition lifelock_freeSKIPS :: ‹('a,'r) processptick ⇒ bool›
  where ‹lifelock_freeSKIPS P ≡ CHAOSSKIPS UNIV UNIV ⊑FD P›


definition non_terminating :: ‹('a,'r) processptick ⇒ bool›
  where ‹non_terminating P ≡ RUN UNIV ⊑T P›


fun RUNk :: ‹nat ⇒ 'a set ⇒ 'b set ⇒ ('a, 'b) processptick› 
  where ‹RUNk 0 A R = SKIPS R›
      | ‹RUNk (Suc n) A R =  □a∈A → RUNk n A R›

text‹In contrast to the assertion term‹non_terminating›, which reauires
a process to terminate ∗‹nowhere›, term‹strictly_terminating› requires a process
to terminate ∗‹everywhere›.›

definition strictly_terminating where ‹strictly_terminating P ≡ (∃ n. RUNk n UNIV UNIV ⊑FD P )›


section ‹Properties›

lemma deadlock_free_mono_FD : ‹deadlock_free P ⟹ P ⊑FD Q ⟹ deadlock_free Q›
  by (meson deadlock_free_def trans_FD)

lemma DFSKIPS_FD_DF : ‹DFSKIPS A R ⊑FD DF A›
proof (subst DFSKIPS_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) processptick›
    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 DFSKIPS_subset : ‹DFSKIPS B S ⊑FD DFSKIPS A R›
  if ‹A ≠ {}› ‹A ⊆ B› ‹R ≠ {}› ‹R ⊆ S›
proof (subst DFSKIPS_def, induct rule: fix_ind)
  show ‹adm (λa. a ⊑FD DFSKIPS A R)› by simp
next
  show ‹⊥ ⊑FD DFSKIPS A R› by simp
next
  show ‹(Λ X. (⊓b∈B → X) ⊓ SKIPS S)⋅X ⊑FD DFSKIPS A R› if ‹X ⊑FD DFSKIPS A R› for X
  proof (subst DFSKIPS_unfold, subst beta_cfun)
    show ‹cont (λX. (⊓b∈B →  X) ⊓ SKIPS S)› by simp
  next
    show ‹(⊓b∈B →  X) ⊓ SKIPS S ⊑FD (⊓a∈A →  DFSKIPS A R) ⊓ SKIPS R›
    proof (rule mono_Ndet_FD)
      show ‹⊓b∈B →  X ⊑FD ⊓a∈A →  DFSKIPS A R›
        by (meson Mndetprefix_FD_subset ‹A ≠ {}› ‹A ⊆ B›
            mono_Mndetprefix_FD ‹X ⊑FD DFSKIPS 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 DFSKIPS_Univ_freeness : ‹⟦A ≠ {}; R ≠ {}; DFSKIPS A R ⊑FD P⟧ ⟹ deadlock_freeSKIPS P›
  by (meson DFSKIPS_subset deadlock_freeSKIPS_def leFD_imp_leF subset_UNIV trans_F)

lemma deadlock_freeSKIPS_Ndet_iff :
  ‹deadlock_freeSKIPS (P ⊓ Q) ⟷ deadlock_freeSKIPS P ∧ deadlock_freeSKIPS Q›
  by (simp add: F_Ndet deadlock_freeSKIPS_def failure_refine_def)


lemma div_free_DFSKIPS: ‹𝒟 (DFSKIPS A R) = {}›
proof (rule equals0I)
  show ‹s ∈ 𝒟 (DFSKIPS A R) ⟹ False› for s
    by (induct s; subst (asm) DFSKIPS_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 DFSKIPS_FD_DF div_free_DFSKIPS 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 eventptick.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) processptick)›
  then obtain t :: ‹('a, 'r) traceptick› 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_DFSKIPS : ‹α(DFSKIPS A R) = A›
proof (intro subset_antisym subsetI)
  fix a assume ‹a ∈ A›
  hence ‹[ev a] ∈ 𝒯 (DFSKIPS A R)›
    by (subst DFSKIPS_unfold) (auto simp add: T_Ndet T_Mndetprefix write0_def T_Mprefix)
  thus ‹a ∈ α(DFSKIPS A R)› by (force simp add: events_of_def)
next
  fix a assume ‹a ∈ α(DFSKIPS A R)›
  then obtain t where ‹ev a ∈ set t› ‹t ∈ 𝒯 (DFSKIPS A R)›
    by (auto simp add: events_of_def)
  thus ‹a ∈ A›
    by (induct t, simp, subst (asm) DFSKIPS_unfold)
      (auto simp add: T_Ndet T_SKIPS T_Mndetprefix write0_def T_Mprefix split: if_split_asm)
qed

lemma ticks_DFSKIPS : ‹✓s(DFSKIPS A R) = R›
proof (intro subset_antisym subsetI)
  fix r assume ‹r ∈ R›
  hence ‹[✓(r)] ∈ 𝒯 (DFSKIPS A R)› by (subst DFSKIPS_unfold) (simp add: T_Ndet T_SKIPS)
  thus ‹r ∈ ✓s(DFSKIPS A R)›
    unfolding ticks_of_def by (metis (no_types, lifting) CollectI append_self_conv2)
next
  fix r assume ‹r ∈ ✓s(DFSKIPS A R)›
  then obtain s where ‹s @ [✓(r)] ∈ 𝒯 (DFSKIPS A R)› unfolding ticks_of_def by blast
  thus ‹r ∈ R›
    by (induct s; subst (asm) DFSKIPS_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) processptick)›
  then obtain t :: ‹('a, 'r) traceptick› 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) processptick)›
  then obtain t :: ‹('a, 'r) traceptick› 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_CHAOSSKIPS : ‹α(CHAOSSKIPS A R) = A›
proof (intro subset_antisym subsetI)
  fix a assume ‹a ∈ A›
  hence ‹[ev a] ∈ 𝒯 (CHAOSSKIPS A R)›
    by (subst CHAOSSKIPS_unfold) (auto simp add: T_Ndet T_Mprefix)
  thus ‹a ∈ α(CHAOSSKIPS A R)› by (force simp add: events_of_def)
next
  fix a assume ‹a ∈ α(CHAOSSKIPS A R)›
  then obtain t where ‹ev a ∈ set t› ‹t ∈ 𝒯 (CHAOSSKIPS A R)›
    by (auto simp add: events_of_def)
  thus ‹a ∈ A›
    by (induct t, simp, subst (asm) CHAOSSKIPS_unfold)
      (auto simp add: T_Ndet T_STOP T_SKIPS T_Mprefix)
qed

lemma ticks_CHAOSSKIPS : ‹✓s(CHAOSSKIPS A R) = R›
proof (intro subset_antisym subsetI)
  fix r assume ‹r ∈ R›
  hence ‹[✓(r)] ∈ 𝒯 (CHAOSSKIPS A R)› by (subst CHAOSSKIPS_unfold) (simp add: T_Ndet T_SKIPS)
  thus ‹r ∈ ✓s(CHAOSSKIPS A R)› by (metis append_Nil ticks_of_memI)
next
  fix r assume ‹r ∈ ✓s(CHAOSSKIPS A R)›
  then obtain s where ‹s @ [✓(r)] ∈ 𝒯 (CHAOSSKIPS A R)› unfolding ticks_of_def by blast
  thus ‹r ∈ R›
    by (induct s; subst (asm) CHAOSSKIPS_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) processptick›
    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) processptick›
    by (subst CHAOS_unfold)
      (auto simp add: refine_defs Mprefix_projs Ndet_projs F_STOP D_STOP)
qed


lemma CHAOSSKIPS_subset_FD : ‹CHAOSSKIPS B S ⊑FD CHAOSSKIPS A R›
  if ‹A ⊆ B› ‹R ≠ {}› ‹R ⊆ S›
proof (subst CHAOSSKIPS_def, induct rule: fix_ind)
  show ‹adm (λa. a ⊑FD CHAOSSKIPS A R)› by simp
next
  show ‹⊥ ⊑FD CHAOSSKIPS A R› by simp
next
  from ‹A ⊆ B› ‹R ≠ {}› ‹R ⊆ S›
  show ‹X ⊑FD CHAOSSKIPS A R ⟹ (Λ X. SKIPS S ⊓ STOP ⊓ (□a∈B → X))⋅X ⊑FD CHAOSSKIPS A R› for X
    by (subst CHAOSSKIPS_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 CHAOSSKIPS_superset_events_of_ticks_of_leF : 
  ‹CHAOSSKIPS 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) ∈ ℱ (CHAOSSKIPS A R)› for s X
  proof (induct s)
    show ‹([], X) ∈ ℱ (CHAOSSKIPS A R)›
      by (subst CHAOSSKIPS_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) ∈ ℱ (CHAOSSKIPS A R)›
    show ‹(e # s, X) ∈ ℱ (CHAOSSKIPS 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) ∈ ℱ (CHAOSSKIPS A R)› by (fact hyp)
      thus ‹(e # s, X) ∈ ℱ (CHAOSSKIPS A R)›
        by (subst CHAOSSKIPS_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) ∈ ℱ (CHAOSSKIPS A R)›
        by (subst CHAOSSKIPS_unfold) (auto simp add: F_Ndet F_SKIPS ‹e = ✓(r)›)
    qed
  qed
  thus ‹ℱ P ⊆ ℱ (CHAOSSKIPS A R)› by (meson F_T F_imp_front_tickFree SUP_upper subrelI)
qed


corollary CHAOSSKIPS_events_of_ticks_of_leF: ‹CHAOSSKIPS α(P) ✓s(P) ⊑F P› 
  and CHAOSSKIPS_UNIV_UNIV_leF: ‹CHAOSSKIPS UNIV UNIV ⊑F P›
  by (simp_all add: CHAOSSKIPS_superset_events_of_ticks_of_leF)


lemma DFSKIPS_F_DF : ‹DFSKIPS A R ⊑F DF A›
  by (simp add: DFSKIPS_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) processptick›
    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) traceptick› 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) traceptick› and X
    by (drule F_T) (use events_of_DF[of A] in ‹auto simp add: events_of_def›)
qed

corollary CHAOSSKIPS_F_CHAOS : ‹CHAOSSKIPS A R ⊑F CHAOS A›
  and CHAOSSKIPS_F_DFSKIPS : ‹CHAOSSKIPS A R ⊑F DFSKIPS A R›
  by (rule CHAOSSKIPS_superset_events_of_ticks_of_leF;
      simp add: events_of_CHAOS ticks_CHAOS events_of_DFSKIPS ticks_DFSKIPS)+




lemma div_free_CHAOSSKIPS: ‹𝒟 (CHAOSSKIPS A R) = {}›
proof (rule equals0I)
  show ‹s ∈ 𝒟 (CHAOSSKIPS A R) ⟹ False› for s
    by (induct s; subst (asm) CHAOSSKIPS_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) traceptick›
    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) traceptick›
    by (induct s; subst (asm) RUN_unfold) (auto simp add: D_Mprefix)
qed

(* DFSKIPS_FD_DF : "DFSKIPS A R ⊑FD DF A" *)

corollary DF_FD_RUN : ‹DF A  ⊑FD RUN A›
  and CHAOS_FD_DF : ‹CHAOS A  ⊑FD DF A›
  and CHAOSSKIPS_FD_CHAOS : ‹CHAOSSKIPS A R ⊑FD CHAOS A›
  and CHAOSSKIPS_FD_DFSKIPS : ‹CHAOSSKIPS A R ⊑FD DFSKIPS A R›
  by (simp_all add: DF_F_RUN div_free_RUN CHAOS_F_DF div_free_DF CHAOSSKIPS_F_CHAOS div_free_CHAOS
      CHAOSSKIPS_F_DFSKIPS div_free_DFSKIPS 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) traceptick›
    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) traceptick›
    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 eventptick.exhaust)+


lemma traces_CHAOSSKIPS_subset :
  ‹𝒯 (CHAOSSKIPS A R) ⊆ {s. ftF s ∧ set s ⊆ ev ` A ∪ tick ` R}›
proof (rule subsetI)
  show ‹s ∈ 𝒯 (CHAOSSKIPS A R) ⟹ s ∈ {s. ftF s ∧ set s ⊆ ev ` A ∪ tick ` R}› for s
    by (induct s; subst (asm) CHAOSSKIPS_unfold)
      (auto simp add: T_Ndet T_STOP T_SKIPS T_Mprefix front_tickFree_Cons_iff)
qed


lemma traces_DFSKIPS_superset : 
  ‹{s. ftF s ∧ set s ⊆ ev ` A ∪ tick ` R} ⊆ 𝒯 (DFSKIPS A R)›
proof (rule subsetI)
  show ‹s ∈ {s. ftF s ∧ set s ⊆ ev ` A ∪ tick ` R} ⟹ s ∈ 𝒯 (DFSKIPS A R) › for s
    by (induct s; subst DFSKIPS_unfold)
      (auto simp add: T_Ndet T_SKIPS T_Mndetprefix write0_def T_Mprefix front_tickFree_Cons_iff)
qed



corollary DFSKIPS_all_front_tickfree_traces1: 
  ‹𝒯 (DFSKIPS A R) = {s. ftF s ∧ set s ⊆ ev ` A ∪ tick ` R}›
  and CHAOSSKIPS_all_front_tickfree_traces1: 
  ‹𝒯 (CHAOSSKIPS A R) = {s. ftF s ∧ set s ⊆ ev ` A ∪ tick ` R}›
  using CHAOSSKIPS_F_DFSKIPS[THEN leF_imp_leT, simplified trace_refine_def]
    traces_CHAOSSKIPS_subset traces_DFSKIPS_superset by blast+


corollary DFSKIPS_all_front_tickfree_traces2   : ‹s ∈ 𝒯 (DFSKIPS UNIV UNIV)›
  and CHAOSSKIPS_all_front_tickfree_traces2: ‹s ∈ 𝒯 (CHAOSSKIPS UNIV UNIV)›
  if ‹ftF s›
  using ‹ftF s›
  by (simp add: tickFree_def DFSKIPS_all_front_tickfree_traces1 CHAOSSKIPS_all_front_tickfree_traces1;
      metis UnCI eventptick.exhaust rangeI subsetI)+


corollary DFSKIPS_UNIV_UNIV_leT :    ‹DFSKIPS UNIV UNIV ⊑T P›
  and  CHAOSSKIPS_UNIV_UNIV_leT : ‹CHAOSSKIPS UNIV UNIV ⊑T P›
  by (simp add:trace_refine_def DFSKIPS_all_front_tickfree_traces2 is_processT2_TR subsetI) 
    (simp add:trace_refine_def CHAOSSKIPS_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_freeSKIPS_is_right: 
  ‹deadlock_freeSKIPS (P :: ('a, 'r) processptick) ⟷
   (∀s∈𝒯 P. tF s ⟶ (s, UNIV :: ('a, 'r) eventptick set) ∉ ℱ P)›
proof (intro iffI ballI impI)
  have ‹tF s ⟹ (s, UNIV) ∉ ℱ (DFSKIPS UNIV UNIV)› for s :: ‹('a, 'r) eventptick list›
    by (induct s; subst DFSKIPS_unfold)
      (auto simp add: F_Ndet F_SKIPS F_Mndetprefix write0_def F_Mprefix)
  thus ‹deadlock_freeSKIPS P ⟹ s ∈ 𝒯 P ⟹ tF s ⟹ (s, UNIV) ∉ ℱ P› for s
    using deadlock_freeSKIPS_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) ∈ ℱ (DFSKIPS UNIV UNIV)› for s :: ‹('a, 'r) traceptick› and X
  proof(induct s)
    case Nil
    then show ?case
      by (subst DFSKIPS_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: DFSKIPS_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 eventptick.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 eventptick.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_freeSKIPS P"
  proof(unfold deadlock_freeSKIPS_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) ∈ ℱ (DFSKIPS 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 DFSKIPS_all_front_tickfree_traces2 FT_True UNIV_I UNIV_eq_I a1(2) as2 as3
            eventptick.exhaust is_processT6_TR_notin tickFree_imp_front_tickFree_snoc)
    next
      case FT_False: False                                                                 
      then show ?thesis 
        by (metis DFSKIPS_all_front_tickfree_traces2 a1(2) front_tickFree_append_iff
            is_processT2_TR is_processT5_S7 list.distinct(1))
    qed 
  qed
qed 

lemma deadlock_freeSKIPS_implies_div_free: ‹deadlock_freeSKIPS P ⟹ 𝒟 P = {}›
  by (metis D_T D_imp_front_tickFree T_nonTickFree_imp_decomp all_not_in_conv butlast_snoc
      deadlock_freeSKIPS_is_right front_tickFree_iff_tickFree_butlast is_processT8 is_processT9)

corollary deadlock_freeSKIPS_FD: ‹deadlock_freeSKIPS P ⟷ DFSKIPS UNIV UNIV ⊑FD P›
  by (metis deadlock_freeSKIPS_def deadlock_freeSKIPS_implies_div_free
      less_eq_processptick_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_freeSKIPS_is_right_wrt_events:
  ‹deadlock_freeSKIPS P ⟷ 
   (∀s∈𝒯 P. tF s ⟶ (s, tick ` ✓s(P) ∪ ev ` α(P)) ∉ ℱ P)›
  unfolding deadlock_freeSKIPS_is_right using all_events_ticks_refusal is_processT4 by blast


lemma deadlock_free_imp_deadlock_freeSKIPS: ‹deadlock_free P ⟹ deadlock_freeSKIPS P›
  using DFSKIPS_FD_DF deadlock_freeSKIPS_FD deadlock_free_def trans_FD by blast




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

lemma non_deadlock_freeSKIPS_STOP: ‹¬ deadlock_freeSKIPS STOP›
  by (unfold deadlock_freeSKIPS_def, subst DFSKIPS_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_freeSKIPS non_deadlock_freeSKIPS_STOP by blast


lemma deadlock_freeSKIPS_SKIPS : ‹deadlock_freeSKIPS (SKIPS R) ⟷ R ≠ {}›
proof (rule iffI)
  show ‹deadlock_freeSKIPS (SKIPS R) ⟹ R ≠ {}›
    by (rule ccontr, simp add: SKIPS_def)
      (use non_deadlock_freeSKIPS_STOP in blast)
next
  show ‹R ≠ {} ⟹ deadlock_freeSKIPS (SKIPS R)›
    by (unfold deadlock_freeSKIPS_def, subst DFSKIPS_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_freeSKIPS_SKIP: ‹deadlock_freeSKIPS (SKIP r)›
  by (metis SKIPS_singl_is_SKIP deadlock_freeSKIPS_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 ⊑FD P›
  by (metis failure_refine_def less_eq_processptick_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 :
  ‹CHAOSSKIPS UNIV UNIV ⊑D P ⟷ 𝒟 P = {}›
  ‹CHAOS UNIV ⊑D P         ⟷ 𝒟 P = {}›
  ‹RUN UNIV ⊑D P           ⟷ 𝒟 P = {}› 
  ‹DFSKIPS 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_DFSKIPS
      div_free_CHAOSSKIPS divergence_refine_def)



lemma lifelock_freeSKIPS_iff_div_free : ‹lifelock_freeSKIPS P ⟷ 𝒟 P = {}›
  by (simp add: CHAOSSKIPS_UNIV_UNIV_leF divergence_refine_div_free(1)
      failure_divergence_refine_def lifelock_freeSKIPS_def)

lemma lifelock_free_imp_lifelock_freeSKIPS : ‹lifelock_free P ⟹ lifelock_freeSKIPS P›
  by (simp add: lifelock_freeSKIPS_iff_div_free lifelock_free_is_non_terminating
      nonterminating_implies_div_free)

corollary deadlock_freeSKIPS_imp_lifelock_freeSKIPS: ‹deadlock_freeSKIPS P ⟹ lifelock_freeSKIPS P›
  by (simp add: deadlock_freeSKIPS_implies_div_free lifelock_freeSKIPS_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_freeSKIPS Q ⟹ non_terminating (P ⟦A⟧ Q)›
  by (simp add: lifelock_freeSKIPS_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 = ‹{}›]


section‹Derived co-induction principles›

lemma lasso_equiv_gen_n :
  ‹DF A = (μ x. ((λX. ⊓a∈A → X) ^^ Suc n) x)›
  unfolding DF_def
  by (rule fix_funpow_eq[where f = ‹λX. ⊓a∈A → X›, symmetric]) simp

text‹Example instance of the lasso-scheme: a lasso of length 3.
     This also explains why this repetition of non-deterministic
     choices is called a ``lasso'' following the intuition from
     the operational semantics:›
lemma deadlock_free_3_coinduct :
 ‹ (⋀x. x ⊑FD P ⟹ ⊓a∈UNIV → ⊓a∈UNIV → ⊓a∈UNIV → x ⊑FD P)
         ⟹ deadlock_free (P::('α, 'δ) processptick)›
  apply(rule DF_Univ_freeness[of UNIV], simp_all add: lasso_equiv_gen_n[where n = 2])
  by (rule fix_ind) (simp_all add: eval_nat_numeral)

text‹And now the general case: ›


lemma deadlock_free_n_coinduct :
 ‹ (⋀x. x ⊑FD P ⟹ ⊓a∈UNIV → ((λ X. ⊓a∈UNIV → X)^^n) x ⊑FD P)
   ⟹ deadlock_free (P::('α, 'δ) processptick)›
  apply(rule DF_Univ_freeness[of UNIV], simp_all add: lasso_equiv_gen_n[where n = n])
  by (rule fix_ind) simp_all

text‹... or even more general: ›
lemma deadlock_free_gen_n_coinduct :
 ‹ A ≠ {} ⟹ (⋀x. x ⊑FD P ⟹ ⊓a∈A → ((λ X. ⊓a∈A → X)^^n) x ⊑FD P)
          ⟹ deadlock_free (P::('α, 'δ) processptick)›
  apply (rule DF_Univ_freeness[of A], assumption)
  apply (simp add: lasso_equiv_gen_n[where n = n])
  by (rule fix_ind) simp_all


text‹The very same argument applies verbatim to the potentially terminating reference
process const‹DFSKIPS› and its assertion const‹deadlock_freeSKIPS›: term‹fix_funpow_eq›
only needs continuity of the recursive step function, and
term‹λX. (⊓a∈UNIV → X) ⊓ SKIPS UNIV› is continuous just like term‹λX. ⊓a∈UNIV → X› is.
Note that, as for ‹DFSKIPS_Univ_freeness›, the coinduction hypothesis is still
phrased with term‹(⊑FD)›, only the concluding assertion const‹deadlock_freeSKIPS›
is the coarser term‹(⊑F)›-based one.›

lemma lasso_equivSKIPS_n :
  ‹DFSKIPS UNIV UNIV = (μ x. ((λX. (⊓a∈UNIV → X) ⊓ SKIPS UNIV) ^^ Suc n) x)›
  unfolding DFSKIPS_def
  by (rule fix_funpow_eq[where f = ‹λX. (⊓a∈UNIV → X) ⊓ SKIPS UNIV›, symmetric]) simp

lemma deadlock_freeSKIPS_n_coinduct :
 ‹ (⋀x. x ⊑FD P ⟹
       (⊓a∈UNIV → ((λX. (⊓a∈UNIV → X) ⊓ SKIPS UNIV) ^^ n) x) ⊓ SKIPS UNIV ⊑FD P)
         ⟹ deadlock_freeSKIPS (P::('α, 'δ) processptick)›
  apply(rule DFSKIPS_Univ_freeness[of UNIV UNIV], simp_all add: lasso_equivSKIPS_n[where n = n])
  by (rule fix_ind) simp_all

text‹Once more, the same domain-theoretic fact term‹fix_funpow_eq› yields the
analogous coinduction schemes for the liveness (livelock-freeness) assertions,
whose reference process is const‹CHAOS› instead of const‹DF›. Since both
const‹lifelock_free› and const‹lifelock_freeSKIPS› are already stated with
term‹(⊑FD)› (unlike const‹deadlock_freeSKIPS›, which is term‹(⊑F)›-based), no
‹_Univ_freeness›-style bridging lemma is needed: we may unfold the assertion directly.›

lemma lasso_equiv_CHAOS_n :
  ‹CHAOS UNIV = (μ x. ((λX. STOP ⊓ (□a∈UNIV → X)) ^^ Suc n) x)›
  unfolding CHAOS_def
  by (rule fix_funpow_eq[where f = ‹λX. STOP ⊓ (□a∈UNIV → X)›, symmetric]) simp

lemma lifelock_free_n_coinduct :
 ‹ (⋀x. x ⊑FD P ⟹
       STOP ⊓ (□a∈UNIV → ((λX. STOP ⊓ (□a∈UNIV → X)) ^^ n) x) ⊑FD P)
         ⟹ lifelock_free (P::('α, 'δ) processptick)›
  unfolding lifelock_free_def
  apply (simp add: lasso_equiv_CHAOS_n[where n = n])
  by (rule fix_ind) simp_all



text‹Since const‹lifelock_free› and const‹non_terminating› are already known to be the
very same predicate (term‹lifelock_free_is_non_terminating› : term‹lifelock_free P = non_terminating P›,
both being term‹CHAOS UNIV ⊑FD P› in disguise), term‹lifelock_free_n_coinduct› transports
verbatim into a coinduction scheme for const‹non_terminating›: no new domain-theoretic
argument is required, only the substitution of the assertion via this equivalence.›

lemma non_terminating_n_coinduct :
 ‹ (⋀x. x ⊑FD P ⟹
       STOP ⊓ (□a∈UNIV → ((λX. STOP ⊓ (□a∈UNIV → X)) ^^ n) x) ⊑FD P)
         ⟹ non_terminating (P::('α, 'δ) processptick)›
  using lifelock_free_n_coinduct[of P n] lifelock_free_is_non_terminating[of P] by blast

lemma lasso_equiv_CHAOSSKIPS_n :
  ‹CHAOSSKIPS UNIV UNIV =
   (μ x. ((λX. SKIPS UNIV ⊓ STOP ⊓ (□a∈UNIV → X)) ^^ Suc n) x)›
  unfolding CHAOSSKIPS_def
  by (rule fix_funpow_eq[where f = ‹λX. SKIPS UNIV ⊓ STOP ⊓ (□a∈UNIV → X)›, symmetric]) simp

lemma lifelock_freeSKIPS_n_coinduct :
 ‹ (⋀x. x ⊑FD P ⟹
       SKIPS UNIV ⊓ STOP ⊓ (□a∈UNIV → ((λX. SKIPS UNIV ⊓ STOP ⊓ (□a∈UNIV → X)) ^^ n) x)
         ⊑FD P)
         ⟹ lifelock_freeSKIPS (P::('α, 'δ) processptick)›
  unfolding lifelock_freeSKIPS_def
  apply (simp add: lasso_equiv_CHAOSSKIPS_n[where n = n])
  by (rule fix_ind) simp_all






(*<*)
end
(*>*)